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-14.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-14.pddl
Parsing...
Parsing: [0.050s CPU, 0.049s wall-clock]
Normalizing task... [0.000s CPU, 0.004s wall-clock]
Instantiating...
Generating Datalog program... [0.020s CPU, 0.013s wall-clock]
Normalizing Datalog program...
Normalizing Datalog program: [0.050s CPU, 0.054s wall-clock]
Preparing model... [0.030s CPU, 0.031s wall-clock]
Generated 115 rules.
Computing model... [0.520s CPU, 0.514s wall-clock]
3094 relevant atoms
3221 auxiliary atoms
6315 final queue length
10878 total queue pushes
Completing instantiation... [0.960s CPU, 0.967s wall-clock]
Instantiating: [1.590s CPU, 1.587s wall-clock]
Computing fact groups...
Finding invariants...
24 initial candidates
Finding invariants: [0.110s CPU, 0.118s wall-clock]
Checking invariant weight... [0.010s 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.020s CPU, 0.013s wall-clock]
Computing fact groups: [0.170s CPU, 0.170s wall-clock]
Building STRIPS to SAS dictionary... [0.000s CPU, 0.003s wall-clock]
Building dictionary for full mutex groups... [0.000s CPU, 0.003s wall-clock]
Building mutex information...
Building mutex information: [0.010s 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, 0.998s 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.488s 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.401s 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: 48588 KB
Writing output... [0.380s CPU, 0.414s wall-clock]
Done! [4.130s CPU, 4.162s wall-clock]
planner.py version 0.0.1

Time:	 0.88s
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.025s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
CPU Time     : 0.884s

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.436s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
CPU Time     : 1.296s

Choices      : 102      (Domain: 91)
Conflicts    : 40       (Analyzed: 39)
Restarts     : 0       
Problems     : 2        (Average Length: 4.50 Splits: 0)
Lemmas       : 39       (Deleted: 0)
  Binary     : 9        (Ratio:  23.08%)
  Ternary    : 3        (Ratio:   7.69%)
  Conflict   : 39       (Average Length:    7.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 39       (Average:  2.67 Max:  26 Sum:    104)
  Executed   : 37       (Average:  2.62 Max:  26 Sum:    102 Ratio:  98.08%)
  Bounded    : 2        (Average:  1.00 Max:   1 Sum:      2 Ratio:   1.92%)

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.908s (Solving: 0.02s 1st Model: 0.01s Unsat: 0.00s)
CPU Time     : 1.768s

Choices      : 1162     (Domain: 1088)
Conflicts    : 90       (Analyzed: 89)
Restarts     : 0       
Model-Level  : 322.0   
Problems     : 3        (Average Length: 7.00 Splits: 0)
Lemmas       : 89       (Deleted: 0)
  Binary     : 20       (Ratio:  22.47%)
  Ternary    : 5        (Ratio:   5.62%)
  Conflict   : 89       (Average Length:   28.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 89       (Average:  9.60 Max: 133 Sum:    854)
  Executed   : 87       (Average:  9.57 Max: 133 Sum:    852 Ratio:  99.77%)
  Bounded    : 2        (Average:  1.00 Max:   1 Sum:      2 Ratio:   0.23%)

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.03s
Memory:		 198MB (+8MB)
SAT
Testing...
NOT SERIALIZABLE
Testing Time:	 1.08s
Memory:		 232MB (+34MB)
Solving...
[start: stats after solve call]

Models       : 0
Calls        : 4
Time         : 2.863s (Solving: 0.64s 1st Model: 0.01s Unsat: 0.62s)
CPU Time     : 2.724s

Choices      : 19344    (Domain: 14952)
Conflicts    : 1913     (Analyzed: 1911)
Restarts     : 22       (Average: 86.86 Last: 50)
Model-Level  : 322.0   
Problems     : 4        (Average Length: 8.25 Splits: 0)
Lemmas       : 1911     (Deleted: 0)
  Binary     : 277      (Ratio:  14.50%)
  Ternary    : 76       (Ratio:   3.98%)
  Conflict   : 1911     (Average Length:  129.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 1911     (Average:  9.85 Max: 136 Sum:  18817)
  Executed   : 1897     (Average:  9.78 Max: 136 Sum:  18693 Ratio:  99.34%)
  Bounded    : 14       (Average:  8.86 Max:  12 Sum:    124 Ratio:   0.66%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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:	 0.71s
Memory:		 232MB (+0MB)
UNSAT
Iteration Time:	 2.27s

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.55s
Memory:		 233MB (+1MB)
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 5
Time         : 8.130s (Solving: 5.11s 1st Model: 0.01s Unsat: 0.62s)
CPU Time     : 7.996s

Choices      : 95205    (Domain: 74477)
Conflicts    : 10749    (Analyzed: 10747)
Restarts     : 122      (Average: 88.09 Last: 68)
Model-Level  : 322.0   
Problems     : 5        (Average Length: 10.00 Splits: 0)
Lemmas       : 10747    (Deleted: 6861)
  Binary     : 977      (Ratio:   9.09%)
  Ternary    : 350      (Ratio:   3.26%)
  Conflict   : 10747    (Average Length:  283.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 10747    (Average:  8.52 Max: 153 Sum:  91613)
  Executed   : 10720    (Average:  8.49 Max: 153 Sum:  91286 Ratio:  99.64%)
  Bounded    : 27       (Average: 12.11 Max:  17 Sum:    327 Ratio:   0.36%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 613821   (Binary:  91.4% Ternary:   6.9% Other:   1.7%)

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

[endof: stats after solve call]
Solving Time:	 4.51s
Memory:		 257MB (+24MB)
UNKNOWN
Iteration Time:	 5.28s

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

Models       : 0+
Calls        : 6
Time         : 15.271s (Solving: 11.42s 1st Model: 0.01s Unsat: 0.62s)
CPU Time     : 15.140s

Choices      : 205988   (Domain: 176928)
Conflicts    : 19398    (Analyzed: 19396)
Restarts     : 222      (Average: 87.37 Last: 109)
Model-Level  : 322.0   
Problems     : 6        (Average Length: 12.00 Splits: 0)
Lemmas       : 19396    (Deleted: 14366)
  Binary     : 1627     (Ratio:   8.39%)
  Ternary    : 611      (Ratio:   3.15%)
  Conflict   : 19396    (Average Length:  336.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 19396    (Average: 10.09 Max: 656 Sum: 195760)
  Executed   : 19357    (Average: 10.06 Max: 656 Sum: 195174 Ratio:  99.70%)
  Bounded    : 39       (Average: 15.03 Max:  22 Sum:    586 Ratio:   0.30%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 890927   (Binary:  91.3% Ternary:   6.9% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 6.35s
Memory:		 277MB (+17MB)
UNKNOWN
Iteration Time:	 7.15s

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

Models       : 0+
Calls        : 7
Time         : 24.398s (Solving: 19.66s 1st Model: 0.01s Unsat: 0.62s)
CPU Time     : 24.272s

Choices      : 351959   (Domain: 310808)
Conflicts    : 28461    (Analyzed: 28459)
Restarts     : 322      (Average: 88.38 Last: 109)
Model-Level  : 322.0   
Problems     : 7        (Average Length: 14.14 Splits: 0)
Lemmas       : 28459    (Deleted: 21449)
  Binary     : 2539     (Ratio:   8.92%)
  Ternary    : 946      (Ratio:   3.32%)
  Conflict   : 28459    (Average Length:  337.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 28459    (Average: 11.72 Max: 656 Sum: 333556)
  Executed   : 28417    (Average: 11.70 Max: 656 Sum: 332889 Ratio:  99.80%)
  Bounded    : 42       (Average: 15.88 Max:  27 Sum:    667 Ratio:   0.20%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 1162658  (Binary:  91.3% Ternary:   6.9% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 8
Time         : 35.367s (Solving: 29.78s 1st Model: 0.01s Unsat: 0.62s)
CPU Time     : 35.244s

Choices      : 530378   (Domain: 479283)
Conflicts    : 37727    (Analyzed: 37725)
Restarts     : 422      (Average: 89.40 Last: 109)
Model-Level  : 322.0   
Problems     : 8        (Average Length: 16.38 Splits: 0)
Lemmas       : 37725    (Deleted: 29511)
  Binary     : 3047     (Ratio:   8.08%)
  Ternary    : 1074     (Ratio:   2.85%)
  Conflict   : 37725    (Average Length:  405.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 37725    (Average: 13.33 Max: 656 Sum: 502896)
  Executed   : 37682    (Average: 13.31 Max: 656 Sum: 502197 Ratio:  99.86%)
  Bounded    : 43       (Average: 16.26 Max:  32 Sum:    699 Ratio:   0.14%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 1445052  (Binary:  91.3% Ternary:   6.9% Other:   1.8%)

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

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

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         : 36.921s (Solving: 31.29s 1st Model: 0.01s Unsat: 2.14s)
CPU Time     : 36.800s

Choices      : 550769   (Domain: 496865)
Conflicts    : 40042    (Analyzed: 40039)
Restarts     : 445      (Average: 89.98 Last: 109)
Model-Level  : 322.0   
Problems     : 9        (Average Length: 18.11 Splits: 0)
Lemmas       : 40039    (Deleted: 31772)
  Binary     : 3189     (Ratio:   7.96%)
  Ternary    : 1111     (Ratio:   2.77%)
  Conflict   : 40039    (Average Length:  396.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 40039    (Average: 13.05 Max: 656 Sum: 522629)
  Executed   : 39990    (Average: 13.03 Max: 656 Sum: 521769 Ratio:  99.84%)
  Bounded    : 49       (Average: 17.55 Max:  32 Sum:    860 Ratio:   0.16%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 1445038  (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:	 1.54s
Memory:		 351MB (+0MB)
UNSAT
Iteration Time:	 1.56s

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         : 46.589s (Solving: 40.92s 1st Model: 0.01s Unsat: 2.14s)
CPU Time     : 46.472s

Choices      : 706696   (Domain: 651527)
Conflicts    : 48695    (Analyzed: 48692)
Restarts     : 545      (Average: 89.34 Last: 109)
Model-Level  : 322.0   
Problems     : 10       (Average Length: 19.50 Splits: 0)
Lemmas       : 48692    (Deleted: 38011)
  Binary     : 3498     (Ratio:   7.18%)
  Ternary    : 1223     (Ratio:   2.51%)
  Conflict   : 48692    (Average Length:  392.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 48692    (Average: 13.85 Max: 656 Sum: 674399)
  Executed   : 48636    (Average: 13.83 Max: 656 Sum: 673408 Ratio:  99.85%)
  Bounded    : 56       (Average: 17.70 Max:  32 Sum:    991 Ratio:   0.15%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 1436963  (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:	 9.66s
Memory:		 351MB (+0MB)
UNKNOWN
Iteration Time:	 9.67s

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         : 56.188s (Solving: 50.47s 1st Model: 0.01s Unsat: 2.14s)
CPU Time     : 56.076s

Choices      : 845728   (Domain: 783353)
Conflicts    : 57360    (Analyzed: 57357)
Restarts     : 645      (Average: 88.93 Last: 109)
Model-Level  : 322.0   
Problems     : 11       (Average Length: 20.64 Splits: 0)
Lemmas       : 57357    (Deleted: 45553)
  Binary     : 3980     (Ratio:   6.94%)
  Ternary    : 1352     (Ratio:   2.36%)
  Conflict   : 57357    (Average Length:  366.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 57357    (Average: 14.05 Max: 656 Sum: 806083)
  Executed   : 57287    (Average: 14.03 Max: 656 Sum: 804649 Ratio:  99.82%)
  Bounded    : 70       (Average: 20.49 Max:  32 Sum:   1434 Ratio:   0.18%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 1421501  (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:	 9.59s
Memory:		 351MB (+0MB)
UNKNOWN
Iteration Time:	 9.61s

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         : 63.614s (Solving: 57.85s 1st Model: 0.01s Unsat: 2.14s)
CPU Time     : 63.508s

Choices      : 961189   (Domain: 893149)
Conflicts    : 65706    (Analyzed: 65703)
Restarts     : 745      (Average: 88.19 Last: 109)
Model-Level  : 322.0   
Problems     : 12       (Average Length: 21.58 Splits: 0)
Lemmas       : 65703    (Deleted: 51297)
  Binary     : 4369     (Ratio:   6.65%)
  Ternary    : 1448     (Ratio:   2.20%)
  Conflict   : 65703    (Average Length:  346.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 65703    (Average: 13.91 Max: 656 Sum: 913684)
  Executed   : 65628    (Average: 13.88 Max: 656 Sum: 912095 Ratio:  99.83%)
  Bounded    : 75       (Average: 21.19 Max:  32 Sum:   1589 Ratio:   0.17%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 1413520  (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:	 7.41s
Memory:		 351MB (+0MB)
UNKNOWN
Iteration Time:	 7.43s

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.55s
Memory:		 351MB (+0MB)
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 13
Time         : 72.439s (Solving: 65.78s 1st Model: 0.01s Unsat: 2.14s)
CPU Time     : 72.336s

Choices      : 1061963  (Domain: 993045)
Conflicts    : 74191    (Analyzed: 74188)
Restarts     : 845      (Average: 87.80 Last: 109)
Model-Level  : 322.0   
Problems     : 13       (Average Length: 22.77 Splits: 0)
Lemmas       : 74188    (Deleted: 59295)
  Binary     : 4595     (Ratio:   6.19%)
  Ternary    : 1460     (Ratio:   1.97%)
  Conflict   : 74188    (Average Length:  345.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 74188    (Average: 13.52 Max: 656 Sum: 1003061)
  Executed   : 74113    (Average: 13.50 Max: 656 Sum: 1001472 Ratio:  99.84%)
  Bounded    : 75       (Average: 21.19 Max:  32 Sum:   1589 Ratio:   0.16%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 1695761  (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:	 7.99s
Memory:		 365MB (+14MB)
UNKNOWN
Iteration Time:	 8.84s

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: 407.0MB
Grounding...	 [('step', [36]), ('step', [37]), ('step', [38]), ('step', [39]), ('step', [40]), ('check', [40])]
Grounding Time:	 0.52s
Memory:		 373MB (+8MB)
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 14
Time         : 80.748s (Solving: 73.21s 1st Model: 0.01s Unsat: 2.14s)
CPU Time     : 80.648s

Choices      : 1162303  (Domain: 1092507)
Conflicts    : 82259    (Analyzed: 82256)
Restarts     : 945      (Average: 87.04 Last: 109)
Model-Level  : 322.0   
Problems     : 14       (Average Length: 24.14 Splits: 0)
Lemmas       : 82256    (Deleted: 67626)
  Binary     : 4832     (Ratio:   5.87%)
  Ternary    : 1479     (Ratio:   1.80%)
  Conflict   : 82256    (Average Length:  345.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 82256    (Average: 13.26 Max: 656 Sum: 1090670)
  Executed   : 82181    (Average: 13.24 Max: 656 Sum: 1089081 Ratio:  99.85%)
  Bounded    : 75       (Average: 21.19 Max:  32 Sum:   1589 Ratio:   0.15%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 1978221  (Binary:  91.3% Ternary:   6.9% Other:   1.8%)

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

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

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.54s
Memory:		 398MB (+10MB)
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 15
Time         : 88.725s (Solving: 80.26s 1st Model: 0.01s Unsat: 2.14s)
CPU Time     : 88.628s

Choices      : 1256697  (Domain: 1185607)
Conflicts    : 90042    (Analyzed: 90039)
Restarts     : 1045     (Average: 86.16 Last: 133)
Model-Level  : 322.0   
Problems     : 15       (Average Length: 25.67 Splits: 0)
Lemmas       : 90039    (Deleted: 75663)
  Binary     : 5008     (Ratio:   5.56%)
  Ternary    : 1488     (Ratio:   1.65%)
  Conflict   : 90039    (Average Length:  347.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 90039    (Average: 13.00 Max: 656 Sum: 1170466)
  Executed   : 89964    (Average: 12.98 Max: 656 Sum: 1168877 Ratio:  99.86%)
  Bounded    : 75       (Average: 21.19 Max:  32 Sum:   1589 Ratio:   0.14%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 2260681  (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.12s
Memory:		 442MB (+44MB)
UNKNOWN
Iteration Time:	 7.99s

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: 496.0MB
Grounding...	 [('step', [46]), ('step', [47]), ('step', [48]), ('step', [49]), ('step', [50]), ('check', [50])]
Grounding Time:	 0.68s
Memory:		 455MB (+13MB)
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 16
Time         : 97.093s (Solving: 87.55s 1st Model: 0.01s Unsat: 2.14s)
CPU Time     : 97.000s

Choices      : 1349814  (Domain: 1278256)
Conflicts    : 98002    (Analyzed: 97999)
Restarts     : 1145     (Average: 85.59 Last: 133)
Model-Level  : 322.0   
Problems     : 16       (Average Length: 27.31 Splits: 0)
Lemmas       : 97999    (Deleted: 83001)
  Binary     : 5139     (Ratio:   5.24%)
  Ternary    : 1495     (Ratio:   1.53%)
  Conflict   : 97999    (Average Length:  347.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 97999    (Average: 12.73 Max: 656 Sum: 1247616)
  Executed   : 97924    (Average: 12.71 Max: 656 Sum: 1246027 Ratio:  99.87%)
  Bounded    : 75       (Average: 21.19 Max:  32 Sum:   1589 Ratio:   0.13%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 2543141  (Binary:  91.3% Ternary:   6.9% Other:   1.8%)

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

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

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: 520.0MB
Grounding...	 [('step', [51]), ('step', [52]), ('step', [53]), ('step', [54]), ('step', [55]), ('check', [55])]
Grounding Time:	 0.55s
Memory:		 470MB (+4MB)
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 17
Time         : 103.405s (Solving: 92.89s 1st Model: 0.01s Unsat: 2.14s)
CPU Time     : 103.316s

Choices      : 1405544  (Domain: 1333752)
Conflicts    : 104946   (Analyzed: 104943)
Restarts     : 1245     (Average: 84.29 Last: 133)
Model-Level  : 322.0   
Problems     : 17       (Average Length: 29.06 Splits: 0)
Lemmas       : 104943   (Deleted: 90573)
  Binary     : 5188     (Ratio:   4.94%)
  Ternary    : 1503     (Ratio:   1.43%)
  Conflict   : 104943   (Average Length:  349.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 104943   (Average: 12.25 Max: 656 Sum: 1286070)
  Executed   : 104868   (Average: 12.24 Max: 656 Sum: 1284481 Ratio:  99.88%)
  Bounded    : 75       (Average: 21.19 Max:  32 Sum:   1589 Ratio:   0.12%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 2825601  (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:	 5.43s
Memory:		 489MB (+19MB)
UNKNOWN
Iteration Time:	 6.33s

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: 543.0MB
Grounding...	 [('step', [56]), ('step', [57]), ('step', [58]), ('step', [59]), ('step', [60]), ('check', [60])]
Grounding Time:	 0.55s
Memory:		 495MB (+6MB)
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 18
Time         : 109.947s (Solving: 98.43s 1st Model: 0.01s Unsat: 2.14s)
CPU Time     : 109.864s

Choices      : 1473951  (Domain: 1402039)
Conflicts    : 112262   (Analyzed: 112259)
Restarts     : 1345     (Average: 83.46 Last: 133)
Model-Level  : 322.0   
Problems     : 18       (Average Length: 30.89 Splits: 0)
Lemmas       : 112259   (Deleted: 97379)
  Binary     : 5238     (Ratio:   4.67%)
  Ternary    : 1503     (Ratio:   1.34%)
  Conflict   : 112259   (Average Length:  348.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 112259   (Average: 11.90 Max: 656 Sum: 1336368)
  Executed   : 112184   (Average: 11.89 Max: 656 Sum: 1334779 Ratio:  99.88%)
  Bounded    : 75       (Average: 21.19 Max:  32 Sum:   1589 Ratio:   0.12%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 3108061  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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.52s
Memory:		 552MB (+0MB)
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 19
Time         : 117.062s (Solving: 104.57s 1st Model: 0.01s Unsat: 2.14s)
CPU Time     : 116.984s

Choices      : 1577071  (Domain: 1504711)
Conflicts    : 119806   (Analyzed: 119803)
Restarts     : 1445     (Average: 82.91 Last: 133)
Model-Level  : 322.0   
Problems     : 19       (Average Length: 32.79 Splits: 0)
Lemmas       : 119803   (Deleted: 104537)
  Binary     : 5283     (Ratio:   4.41%)
  Ternary    : 1512     (Ratio:   1.26%)
  Conflict   : 119803   (Average Length:  347.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 119803   (Average: 11.85 Max: 656 Sum: 1420251)
  Executed   : 119728   (Average: 11.84 Max: 656 Sum: 1418662 Ratio:  99.89%)
  Bounded    : 75       (Average: 21.19 Max:  32 Sum:   1589 Ratio:   0.11%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 3390521  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 6.24s
Memory:		 557MB (+5MB)
UNKNOWN
Iteration Time:	 7.13s

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

Models       : 0+
Calls        : 20
Time         : 123.504s (Solving: 109.97s 1st Model: 0.01s Unsat: 2.14s)
CPU Time     : 123.420s

Choices      : 1647293  (Domain: 1574846)
Conflicts    : 126630   (Analyzed: 126627)
Restarts     : 1545     (Average: 81.96 Last: 133)
Model-Level  : 322.0   
Problems     : 20       (Average Length: 34.75 Splits: 0)
Lemmas       : 126627   (Deleted: 111879)
  Binary     : 5309     (Ratio:   4.19%)
  Ternary    : 1513     (Ratio:   1.19%)
  Conflict   : 126627   (Average Length:  345.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 126627   (Average: 11.61 Max: 713 Sum: 1469985)
  Executed   : 126552   (Average: 11.60 Max: 713 Sum: 1468396 Ratio:  99.89%)
  Bounded    : 75       (Average: 21.19 Max:  32 Sum:   1589 Ratio:   0.11%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 3672981  (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:	 5.50s
Memory:		 583MB (+21MB)
UNKNOWN
Iteration Time:	 6.45s

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.54s
Memory:		 584MB (+1MB)
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 21
Time         : 130.698s (Solving: 116.12s 1st Model: 0.01s Unsat: 2.14s)
CPU Time     : 130.616s

Choices      : 1745225  (Domain: 1672463)
Conflicts    : 134050   (Analyzed: 134047)
Restarts     : 1645     (Average: 81.49 Last: 133)
Model-Level  : 322.0   
Problems     : 21       (Average Length: 36.76 Splits: 0)
Lemmas       : 134047   (Deleted: 118733)
  Binary     : 5351     (Ratio:   3.99%)
  Ternary    : 1516     (Ratio:   1.13%)
  Conflict   : 134047   (Average Length:  343.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 134047   (Average: 11.54 Max: 713 Sum: 1546644)
  Executed   : 133972   (Average: 11.53 Max: 713 Sum: 1545055 Ratio:  99.90%)
  Bounded    : 75       (Average: 21.19 Max:  32 Sum:   1589 Ratio:   0.10%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 3955441  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 6.26s
Memory:		 609MB (+25MB)
UNKNOWN
Iteration Time:	 7.21s

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

Models       : 0+
Calls        : 22
Time         : 138.204s (Solving: 122.58s 1st Model: 0.01s Unsat: 2.14s)
CPU Time     : 138.128s

Choices      : 1853814  (Domain: 1780727)
Conflicts    : 141568   (Analyzed: 141565)
Restarts     : 1745     (Average: 81.13 Last: 133)
Model-Level  : 322.0   
Problems     : 22       (Average Length: 38.82 Splits: 0)
Lemmas       : 141565   (Deleted: 126317)
  Binary     : 5393     (Ratio:   3.81%)
  Ternary    : 1518     (Ratio:   1.07%)
  Conflict   : 141565   (Average Length:  340.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 141565   (Average: 11.54 Max: 867 Sum: 1633442)
  Executed   : 141490   (Average: 11.53 Max: 867 Sum: 1631853 Ratio:  99.90%)
  Bounded    : 75       (Average: 21.19 Max:  32 Sum:   1589 Ratio:   0.10%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 4237901  (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:	 6.57s
Memory:		 633MB (+24MB)
UNKNOWN
Iteration Time:	 7.52s

Iteration 22
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), (21,105,0,True)]
Grounded Until:	 80
Blocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 23
Time         : 149.765s (Solving: 134.00s 1st Model: 0.01s Unsat: 2.14s)
CPU Time     : 149.688s

Choices      : 1924144  (Domain: 1851052)
Conflicts    : 150241   (Analyzed: 150238)
Restarts     : 1845     (Average: 81.43 Last: 133)
Model-Level  : 322.0   
Problems     : 23       (Average Length: 40.70 Splits: 0)
Lemmas       : 150238   (Deleted: 135085)
  Binary     : 5490     (Ratio:   3.65%)
  Ternary    : 1539     (Ratio:   1.02%)
  Conflict   : 150238   (Average Length:  353.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 150238   (Average: 11.33 Max: 867 Sum: 1701556)
  Executed   : 150163   (Average: 11.32 Max: 867 Sum: 1699967 Ratio:  99.91%)
  Bounded    : 75       (Average: 21.19 Max:  32 Sum:   1589 Ratio:   0.09%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 4237901  (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.51s
Memory:		 633MB (+0MB)
UNKNOWN
Iteration Time:	 11.56s

Iteration 23
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), (21,105,0,True)]
Grounded Until:	 80
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 24
Time         : 158.420s (Solving: 142.52s 1st Model: 0.01s Unsat: 2.14s)
CPU Time     : 158.348s

Choices      : 2022869  (Domain: 1943588)
Conflicts    : 159084   (Analyzed: 159081)
Restarts     : 1945     (Average: 81.79 Last: 133)
Model-Level  : 322.0   
Problems     : 24       (Average Length: 42.42 Splits: 0)
Lemmas       : 159081   (Deleted: 142691)
  Binary     : 5950     (Ratio:   3.74%)
  Ternary    : 1666     (Ratio:   1.05%)
  Conflict   : 159081   (Average Length:  361.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 159081   (Average: 11.25 Max: 867 Sum: 1789586)
  Executed   : 158999   (Average: 11.24 Max: 867 Sum: 1787439 Ratio:  99.88%)
  Bounded    : 82       (Average: 26.18 Max:  82 Sum:   2147 Ratio:   0.12%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 4237901  (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.61s
Memory:		 633MB (+0MB)
UNKNOWN
Iteration Time:	 8.66s

Iteration 24
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), (21,105,0,True)]
Grounded Until:	 80
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 25
Time         : 167.520s (Solving: 151.48s 1st Model: 0.01s Unsat: 2.14s)
CPU Time     : 167.452s

Choices      : 2143047  (Domain: 2060949)
Conflicts    : 168377   (Analyzed: 168374)
Restarts     : 2045     (Average: 82.33 Last: 133)
Model-Level  : 322.0   
Problems     : 25       (Average Length: 44.00 Splits: 0)
Lemmas       : 168374   (Deleted: 149744)
  Binary     : 6736     (Ratio:   4.00%)
  Ternary    : 1944     (Ratio:   1.15%)
  Conflict   : 168374   (Average Length:  358.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 168374   (Average: 11.27 Max: 867 Sum: 1897024)
  Executed   : 168289   (Average: 11.25 Max: 867 Sum: 1894633 Ratio:  99.87%)
  Bounded    : 85       (Average: 28.13 Max:  82 Sum:   2391 Ratio:   0.13%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 4230479  (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.05s
Memory:		 633MB (+0MB)
UNKNOWN
Iteration Time:	 9.11s

Iteration 25
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), (21,105,0,True)]
Grounded Until:	 80
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 26
Time         : 175.355s (Solving: 159.20s 1st Model: 0.01s Unsat: 2.14s)
CPU Time     : 175.292s

Choices      : 2266359  (Domain: 2180970)
Conflicts    : 176772   (Analyzed: 176769)
Restarts     : 2145     (Average: 82.41 Last: 133)
Model-Level  : 322.0   
Problems     : 26       (Average Length: 45.46 Splits: 0)
Lemmas       : 176769   (Deleted: 155763)
  Binary     : 7277     (Ratio:   4.12%)
  Ternary    : 2095     (Ratio:   1.19%)
  Conflict   : 176769   (Average Length:  352.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 176769   (Average: 11.37 Max: 867 Sum: 2009586)
  Executed   : 176683   (Average: 11.35 Max: 867 Sum: 2007113 Ratio:  99.88%)
  Bounded    : 86       (Average: 28.76 Max:  82 Sum:   2473 Ratio:   0.12%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 4230466  (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.80s
Memory:		 633MB (+0MB)
UNKNOWN
Iteration Time:	 7.84s

Iteration 26
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), (21,105,0,True)]
Grounded Until:	 80
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 27
Time         : 186.813s (Solving: 170.52s 1st Model: 0.01s Unsat: 2.14s)
CPU Time     : 186.740s

Choices      : 2494373  (Domain: 2405640)
Conflicts    : 185979   (Analyzed: 185976)
Restarts     : 2245     (Average: 82.84 Last: 136)
Model-Level  : 322.0   
Problems     : 27       (Average Length: 46.81 Splits: 0)
Lemmas       : 185976   (Deleted: 164673)
  Binary     : 8173     (Ratio:   4.39%)
  Ternary    : 2398     (Ratio:   1.29%)
  Conflict   : 185976   (Average Length:  347.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 185976   (Average: 11.95 Max: 867 Sum: 2222022)
  Executed   : 185889   (Average: 11.93 Max: 867 Sum: 2219472 Ratio:  99.89%)
  Bounded    : 87       (Average: 29.31 Max:  82 Sum:   2550 Ratio:   0.11%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 4230452  (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.40s
Memory:		 633MB (+0MB)
UNKNOWN
Iteration Time:	 11.45s

Iteration 27
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), (21,105,0,True)]
Grounded Until:	 80
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 28
Time         : 200.985s (Solving: 184.57s 1st Model: 0.01s Unsat: 2.14s)
CPU Time     : 200.920s

Choices      : 2772651  (Domain: 2678983)
Conflicts    : 195478   (Analyzed: 195475)
Restarts     : 2345     (Average: 83.36 Last: 136)
Model-Level  : 322.0   
Problems     : 28       (Average Length: 48.07 Splits: 0)
Lemmas       : 195475   (Deleted: 171746)
  Binary     : 9103     (Ratio:   4.66%)
  Ternary    : 2674     (Ratio:   1.37%)
  Conflict   : 195475   (Average Length:  341.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 195475   (Average: 12.69 Max: 867 Sum: 2480700)
  Executed   : 195388   (Average: 12.68 Max: 867 Sum: 2478150 Ratio:  99.90%)
  Bounded    : 87       (Average: 29.31 Max:  82 Sum:   2550 Ratio:   0.10%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 4230452  (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:	 14.13s
Memory:		 633MB (+0MB)
UNKNOWN
Iteration Time:	 14.18s

Iteration 28
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), (21,105,0,True)]
Grounded Until:	 80
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 29
Time         : 214.178s (Solving: 197.65s 1st Model: 0.01s Unsat: 2.14s)
CPU Time     : 214.120s

Choices      : 3064867  (Domain: 2968680)
Conflicts    : 204012   (Analyzed: 204009)
Restarts     : 2445     (Average: 83.44 Last: 136)
Model-Level  : 322.0   
Problems     : 29       (Average Length: 49.24 Splits: 0)
Lemmas       : 204009   (Deleted: 177722)
  Binary     : 9776     (Ratio:   4.79%)
  Ternary    : 2812     (Ratio:   1.38%)
  Conflict   : 204009   (Average Length:  338.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 204009   (Average: 13.50 Max: 867 Sum: 2754510)
  Executed   : 203922   (Average: 13.49 Max: 867 Sum: 2751960 Ratio:  99.91%)
  Bounded    : 87       (Average: 29.31 Max:  82 Sum:   2550 Ratio:   0.09%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 4230452  (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:	 13.16s
Memory:		 633MB (+0MB)
UNKNOWN
Iteration Time:	 13.20s

Iteration 29
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), (21,105,0,True)]
Grounded Until:	 80
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 30
Time         : 230.574s (Solving: 213.93s 1st Model: 0.01s Unsat: 2.14s)
CPU Time     : 230.524s

Choices      : 3403358  (Domain: 3304589)
Conflicts    : 213049   (Analyzed: 213046)
Restarts     : 2545     (Average: 83.71 Last: 221)
Model-Level  : 322.0   
Problems     : 30       (Average Length: 50.33 Splits: 0)
Lemmas       : 213046   (Deleted: 186933)
  Binary     : 10245    (Ratio:   4.81%)
  Ternary    : 2919     (Ratio:   1.37%)
  Conflict   : 213046   (Average Length:  336.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 213046   (Average: 14.43 Max: 867 Sum: 3074752)
  Executed   : 212957   (Average: 14.42 Max: 867 Sum: 3072040 Ratio:  99.91%)
  Bounded    : 89       (Average: 30.47 Max:  82 Sum:   2712 Ratio:   0.09%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 4230452  (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:	 16.36s
Memory:		 633MB (+0MB)
UNKNOWN
Iteration Time:	 16.41s

Iteration 30
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), (21,105,0,True)]
Grounded Until:	 80
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 31
Time         : 235.207s (Solving: 218.44s 1st Model: 0.01s Unsat: 2.14s)
CPU Time     : 235.160s

Choices      : 3483369  (Domain: 3383758)
Conflicts    : 220851   (Analyzed: 220848)
Restarts     : 2645     (Average: 83.50 Last: 221)
Model-Level  : 322.0   
Problems     : 31       (Average Length: 51.35 Splits: 0)
Lemmas       : 220848   (Deleted: 193250)
  Binary     : 10371    (Ratio:   4.70%)
  Ternary    : 2952     (Ratio:   1.34%)
  Conflict   : 220848   (Average Length:  332.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 220848   (Average: 14.23 Max: 867 Sum: 3141799)
  Executed   : 220756   (Average: 14.21 Max: 867 Sum: 3138847 Ratio:  99.91%)
  Bounded    : 92       (Average: 32.09 Max:  82 Sum:   2952 Ratio:   0.09%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 4230452  (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:	 4.59s
Memory:		 633MB (+0MB)
UNKNOWN
Iteration Time:	 4.64s

Iteration 31
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), (21,105,0,True)]
Grounded Until:	 80
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 32
Time         : 249.959s (Solving: 233.07s 1st Model: 0.01s Unsat: 2.14s)
CPU Time     : 249.920s

Choices      : 3818102  (Domain: 3713808)
Conflicts    : 229584   (Analyzed: 229581)
Restarts     : 2745     (Average: 83.64 Last: 221)
Model-Level  : 322.0   
Problems     : 32       (Average Length: 52.31 Splits: 0)
Lemmas       : 229581   (Deleted: 202444)
  Binary     : 10807    (Ratio:   4.71%)
  Ternary    : 3038     (Ratio:   1.32%)
  Conflict   : 229581   (Average Length:  332.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 229581   (Average: 15.06 Max: 1019 Sum: 3456413)
  Executed   : 229488   (Average: 15.04 Max: 1019 Sum: 3453384 Ratio:  99.91%)
  Bounded    : 93       (Average: 32.57 Max:  82 Sum:   3029 Ratio:   0.09%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 4230438  (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:	 14.71s
Memory:		 633MB (+0MB)
UNKNOWN
Iteration Time:	 14.76s

Iteration 32
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), (21,105,0,True)]
Grounded Until:	 80
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 33
Time         : 265.325s (Solving: 248.32s 1st Model: 0.01s Unsat: 2.14s)
CPU Time     : 265.292s

Choices      : 4200396  (Domain: 4093469)
Conflicts    : 238586   (Analyzed: 238583)
Restarts     : 2845     (Average: 83.86 Last: 221)
Model-Level  : 322.0   
Problems     : 33       (Average Length: 53.21 Splits: 0)
Lemmas       : 238583   (Deleted: 209799)
  Binary     : 11489    (Ratio:   4.82%)
  Ternary    : 3210     (Ratio:   1.35%)
  Conflict   : 238583   (Average Length:  332.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 238583   (Average: 15.99 Max: 1019 Sum: 3814223)
  Executed   : 238490   (Average: 15.97 Max: 1019 Sum: 3811194 Ratio:  99.92%)
  Bounded    : 93       (Average: 32.57 Max:  82 Sum:   3029 Ratio:   0.08%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 4230438  (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:	 15.34s
Memory:		 633MB (+0MB)
UNKNOWN
Iteration Time:	 15.38s

Iteration 33
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), (21,105,0,True)]
Grounded Until:	 80
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 34
Time         : 279.418s (Solving: 262.30s 1st Model: 0.01s Unsat: 2.14s)
CPU Time     : 279.388s

Choices      : 4557198  (Domain: 4448232)
Conflicts    : 247881   (Analyzed: 247878)
Restarts     : 2945     (Average: 84.17 Last: 221)
Model-Level  : 322.0   
Problems     : 34       (Average Length: 54.06 Splits: 0)
Lemmas       : 247878   (Deleted: 217539)
  Binary     : 12029    (Ratio:   4.85%)
  Ternary    : 3407     (Ratio:   1.37%)
  Conflict   : 247878   (Average Length:  328.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 247878   (Average: 16.73 Max: 1019 Sum: 4147714)
  Executed   : 247784   (Average: 16.72 Max: 1019 Sum: 4144603 Ratio:  99.92%)
  Bounded    : 94       (Average: 33.10 Max:  82 Sum:   3111 Ratio:   0.08%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 4230438  (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:	 14.06s
Memory:		 633MB (+0MB)
UNKNOWN
Iteration Time:	 14.10s

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

Models       : 0+
Calls        : 35
Time         : 291.827s (Solving: 274.57s 1st Model: 0.01s Unsat: 2.14s)
CPU Time     : 291.804s

Choices      : 4830431  (Domain: 4718871)
Conflicts    : 256833   (Analyzed: 256830)
Restarts     : 3045     (Average: 84.34 Last: 221)
Model-Level  : 322.0   
Problems     : 35       (Average Length: 54.86 Splits: 0)
Lemmas       : 256830   (Deleted: 225918)
  Binary     : 12393    (Ratio:   4.83%)
  Ternary    : 3529     (Ratio:   1.37%)
  Conflict   : 256830   (Average Length:  329.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 256830   (Average: 17.13 Max: 1019 Sum: 4398576)
  Executed   : 256735   (Average: 17.11 Max: 1019 Sum: 4395383 Ratio:  99.93%)
  Bounded    : 95       (Average: 33.61 Max:  82 Sum:   3193 Ratio:   0.07%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 4230412  (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:	 12.37s
Memory:		 633MB (+0MB)
UNKNOWN
Iteration Time:	 12.42s

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

Models       : 0+
Calls        : 36
Time         : 299.651s (Solving: 281.26s 1st Model: 0.01s Unsat: 2.14s)
CPU Time     : 299.632s

Choices      : 4904399  (Domain: 4792837)
Conflicts    : 264627   (Analyzed: 264624)
Restarts     : 3145     (Average: 84.14 Last: 221)
Model-Level  : 322.0   
Problems     : 36       (Average Length: 55.75 Splits: 0)
Lemmas       : 264624   (Deleted: 232374)
  Binary     : 12438    (Ratio:   4.70%)
  Ternary    : 3535     (Ratio:   1.34%)
  Conflict   : 264624   (Average Length:  327.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 264624   (Average: 16.82 Max: 1019 Sum: 4450481)
  Executed   : 264529   (Average: 16.81 Max: 1019 Sum: 4447288 Ratio:  99.93%)
  Bounded    : 95       (Average: 33.61 Max:  82 Sum:   3193 Ratio:   0.07%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 4512865  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 6.82s
Memory:		 653MB (+20MB)
UNKNOWN
Iteration Time:	 7.84s

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

Models       : 0+
Calls        : 37
Time         : 306.403s (Solving: 286.87s 1st Model: 0.01s Unsat: 2.14s)
CPU Time     : 306.388s

Choices      : 4967031  (Domain: 4855465)
Conflicts    : 272135   (Analyzed: 272132)
Restarts     : 3245     (Average: 83.86 Last: 221)
Model-Level  : 322.0   
Problems     : 37       (Average Length: 56.73 Splits: 0)
Lemmas       : 272132   (Deleted: 240047)
  Binary     : 12474    (Ratio:   4.58%)
  Ternary    : 3541     (Ratio:   1.30%)
  Conflict   : 272132   (Average Length:  326.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 272132   (Average: 16.50 Max: 1019 Sum: 4490565)
  Executed   : 272037   (Average: 16.49 Max: 1019 Sum: 4487372 Ratio:  99.93%)
  Bounded    : 95       (Average: 33.61 Max:  82 Sum:   3193 Ratio:   0.07%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 4795325  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 5.74s
Memory:		 733MB (+80MB)
UNKNOWN
Iteration Time:	 6.77s

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

Models       : 0+
Calls        : 38
Time         : 314.164s (Solving: 293.46s 1st Model: 0.01s Unsat: 2.14s)
CPU Time     : 314.152s

Choices      : 5049179  (Domain: 4937594)
Conflicts    : 279650   (Analyzed: 279647)
Restarts     : 3345     (Average: 83.60 Last: 221)
Model-Level  : 322.0   
Problems     : 38       (Average Length: 57.79 Splits: 0)
Lemmas       : 279647   (Deleted: 247404)
  Binary     : 12512    (Ratio:   4.47%)
  Ternary    : 3542     (Ratio:   1.27%)
  Conflict   : 279647   (Average Length:  324.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 279647   (Average: 16.26 Max: 1019 Sum: 4548073)
  Executed   : 279552   (Average: 16.25 Max: 1019 Sum: 4544880 Ratio:  99.93%)
  Bounded    : 95       (Average: 33.61 Max:  82 Sum:   3193 Ratio:   0.07%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 5077785  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 6.72s
Memory:		 738MB (+5MB)
UNKNOWN
Iteration Time:	 7.78s

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

Models       : 0+
Calls        : 39
Time         : 323.239s (Solving: 301.04s 1st Model: 0.01s Unsat: 2.14s)
CPU Time     : 323.232s

Choices      : 5153025  (Domain: 5041404)
Conflicts    : 287066   (Analyzed: 287063)
Restarts     : 3445     (Average: 83.33 Last: 221)
Model-Level  : 322.0   
Problems     : 39       (Average Length: 58.92 Splits: 0)
Lemmas       : 287063   (Deleted: 254811)
  Binary     : 12540    (Ratio:   4.37%)
  Ternary    : 3551     (Ratio:   1.24%)
  Conflict   : 287063   (Average Length:  324.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 287063   (Average: 16.11 Max: 1019 Sum: 4625308)
  Executed   : 286968   (Average: 16.10 Max: 1019 Sum: 4622115 Ratio:  99.93%)
  Bounded    : 95       (Average: 33.61 Max:  82 Sum:   3193 Ratio:   0.07%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 5360245  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 7.71s
Memory:		 793MB (+5MB)
UNKNOWN
Iteration Time:	 9.09s

Iteration 39
Queue:		 [(21,105,0,True)]
Grounded Until:	 100
Expected Memory: 873.0MB
Grounding...	 [('step', [101]), ('step', [102]), ('step', [103]), ('step', [104]), ('step', [105]), ('check', [105])]
Grounding Time:	 0.52s
Memory:		 793MB (+0MB)
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 40
Time         : 331.949s (Solving: 308.60s 1st Model: 0.01s Unsat: 2.14s)
CPU Time     : 331.944s

Choices      : 5252057  (Domain: 5140424)
Conflicts    : 294641   (Analyzed: 294638)
Restarts     : 3545     (Average: 83.11 Last: 221)
Model-Level  : 322.0   
Problems     : 40       (Average Length: 60.12 Splits: 0)
Lemmas       : 294638   (Deleted: 262073)
  Binary     : 12599    (Ratio:   4.28%)
  Ternary    : 3554     (Ratio:   1.21%)
  Conflict   : 294638   (Average Length:  323.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 294638   (Average: 15.94 Max: 1019 Sum: 4696891)
  Executed   : 294543   (Average: 15.93 Max: 1019 Sum: 4693698 Ratio:  99.93%)
  Bounded    : 95       (Average: 33.61 Max:  82 Sum:   3193 Ratio:   0.07%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 5642705  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 7.71s
Memory:		 802MB (+9MB)
UNKNOWN
Iteration Time:	 8.73s

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,1,True), (22,110,0,True), (23,115,0,True)]
Grounded Until:	 105
Blocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 41
Time         : 338.872s (Solving: 315.34s 1st Model: 0.01s Unsat: 2.14s)
CPU Time     : 338.872s

Choices      : 5320538  (Domain: 5208905)
Conflicts    : 302501   (Analyzed: 302498)
Restarts     : 3645     (Average: 82.99 Last: 221)
Model-Level  : 322.0   
Problems     : 41       (Average Length: 61.27 Splits: 0)
Lemmas       : 302498   (Deleted: 269383)
  Binary     : 12729    (Ratio:   4.21%)
  Ternary    : 3570     (Ratio:   1.18%)
  Conflict   : 302498   (Average Length:  324.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 302498   (Average: 15.74 Max: 1019 Sum: 4760594)
  Executed   : 302403   (Average: 15.73 Max: 1019 Sum: 4757401 Ratio:  99.93%)
  Bounded    : 95       (Average: 33.61 Max:  82 Sum:   3193 Ratio:   0.07%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 5642705  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 6.86s
Memory:		 806MB (+4MB)
UNKNOWN
Iteration Time:	 6.93s

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,1,True), (22,110,0,True), (23,115,0,True)]
Grounded Until:	 105
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 42
Time         : 343.589s (Solving: 319.90s 1st Model: 0.01s Unsat: 2.14s)
CPU Time     : 343.592s

Choices      : 5358783  (Domain: 5247150)
Conflicts    : 310285   (Analyzed: 310282)
Restarts     : 3745     (Average: 82.85 Last: 221)
Model-Level  : 322.0   
Problems     : 42       (Average Length: 62.36 Splits: 0)
Lemmas       : 310282   (Deleted: 276897)
  Binary     : 12773    (Ratio:   4.12%)
  Ternary    : 3581     (Ratio:   1.15%)
  Conflict   : 310282   (Average Length:  323.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 310282   (Average: 15.43 Max: 1019 Sum: 4788555)
  Executed   : 310187   (Average: 15.42 Max: 1019 Sum: 4785362 Ratio:  99.93%)
  Bounded    : 95       (Average: 33.61 Max:  82 Sum:   3193 Ratio:   0.07%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 5642705  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 4.66s
Memory:		 806MB (+0MB)
UNKNOWN
Iteration Time:	 4.72s

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,1,True), (22,110,0,True), (23,115,0,True)]
Grounded Until:	 105
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 43
Time         : 348.481s (Solving: 324.61s 1st Model: 0.01s Unsat: 2.14s)
CPU Time     : 348.484s

Choices      : 5405607  (Domain: 5293974)
Conflicts    : 318083   (Analyzed: 318080)
Restarts     : 3845     (Average: 82.73 Last: 221)
Model-Level  : 322.0   
Problems     : 43       (Average Length: 63.40 Splits: 0)
Lemmas       : 318080   (Deleted: 284363)
  Binary     : 12920    (Ratio:   4.06%)
  Ternary    : 3594     (Ratio:   1.13%)
  Conflict   : 318080   (Average Length:  322.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 318080   (Average: 15.18 Max: 1019 Sum: 4827516)
  Executed   : 317984   (Average: 15.17 Max: 1019 Sum: 4824221 Ratio:  99.93%)
  Bounded    : 96       (Average: 34.32 Max: 102 Sum:   3295 Ratio:   0.07%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 5642705  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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,1,True), (22,110,0,True), (23,115,0,True)]
Grounded Until:	 105
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 44
Time         : 352.456s (Solving: 328.44s 1st Model: 0.01s Unsat: 2.14s)
CPU Time     : 352.460s

Choices      : 5441330  (Domain: 5329697)
Conflicts    : 325893   (Analyzed: 325890)
Restarts     : 3945     (Average: 82.61 Last: 221)
Model-Level  : 322.0   
Problems     : 44       (Average Length: 64.39 Splits: 0)
Lemmas       : 325890   (Deleted: 291775)
  Binary     : 12953    (Ratio:   3.97%)
  Ternary    : 3606     (Ratio:   1.11%)
  Conflict   : 325890   (Average Length:  319.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 325890   (Average: 14.89 Max: 1019 Sum: 4853019)
  Executed   : 325794   (Average: 14.88 Max: 1019 Sum: 4849724 Ratio:  99.93%)
  Bounded    : 96       (Average: 34.32 Max: 102 Sum:   3295 Ratio:   0.07%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 5642705  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 3.93s
Memory:		 806MB (+0MB)
UNKNOWN
Iteration Time:	 3.98s

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,1,True), (22,110,0,True), (23,115,0,True)]
Grounded Until:	 105
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 45
Time         : 355.739s (Solving: 331.57s 1st Model: 0.01s Unsat: 2.14s)
CPU Time     : 355.744s

Choices      : 5476252  (Domain: 5364619)
Conflicts    : 333440   (Analyzed: 333437)
Restarts     : 4045     (Average: 82.43 Last: 221)
Model-Level  : 322.0   
Problems     : 45       (Average Length: 65.33 Splits: 0)
Lemmas       : 333437   (Deleted: 299342)
  Binary     : 12978    (Ratio:   3.89%)
  Ternary    : 3623     (Ratio:   1.09%)
  Conflict   : 333437   (Average Length:  317.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 333437   (Average: 14.63 Max: 1019 Sum: 4879633)
  Executed   : 333340   (Average: 14.62 Max: 1019 Sum: 4876231 Ratio:  99.93%)
  Bounded    : 97       (Average: 35.07 Max: 107 Sum:   3402 Ratio:   0.07%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 5642705  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 3.23s
Memory:		 806MB (+0MB)
UNKNOWN
Iteration Time:	 3.29s

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,1,True), (22,110,0,True), (23,115,0,True)]
Grounded Until:	 105
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 46
Time         : 361.051s (Solving: 336.73s 1st Model: 0.01s Unsat: 2.14s)
CPU Time     : 361.060s

Choices      : 5539974  (Domain: 5428005)
Conflicts    : 341024   (Analyzed: 341021)
Restarts     : 4145     (Average: 82.27 Last: 221)
Model-Level  : 322.0   
Problems     : 46       (Average Length: 66.24 Splits: 0)
Lemmas       : 341021   (Deleted: 306439)
  Binary     : 13109    (Ratio:   3.84%)
  Ternary    : 3664     (Ratio:   1.07%)
  Conflict   : 341021   (Average Length:  315.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 341021   (Average: 14.47 Max: 1019 Sum: 4933086)
  Executed   : 340922   (Average: 14.46 Max: 1019 Sum: 4929470 Ratio:  99.93%)
  Bounded    : 99       (Average: 36.53 Max: 107 Sum:   3616 Ratio:   0.07%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 5642691  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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,1,True), (22,110,0,True), (23,115,0,True)]
Grounded Until:	 105
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 47
Time         : 364.992s (Solving: 340.51s 1st Model: 0.01s Unsat: 2.14s)
CPU Time     : 365.004s

Choices      : 5578931  (Domain: 5466962)
Conflicts    : 348577   (Analyzed: 348574)
Restarts     : 4245     (Average: 82.11 Last: 221)
Model-Level  : 322.0   
Problems     : 47       (Average Length: 67.11 Splits: 0)
Lemmas       : 348574   (Deleted: 313772)
  Binary     : 13124    (Ratio:   3.77%)
  Ternary    : 3669     (Ratio:   1.05%)
  Conflict   : 348574   (Average Length:  314.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 348574   (Average: 14.24 Max: 1019 Sum: 4962689)
  Executed   : 348475   (Average: 14.23 Max: 1019 Sum: 4959073 Ratio:  99.93%)
  Bounded    : 99       (Average: 36.53 Max: 107 Sum:   3616 Ratio:   0.07%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 5640231  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 3.89s
Memory:		 806MB (+0MB)
UNKNOWN
Iteration Time:	 3.95s

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,1,True), (22,110,0,True), (23,115,0,True)]
Grounded Until:	 105
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 48
Time         : 370.233s (Solving: 345.60s 1st Model: 0.01s Unsat: 2.14s)
CPU Time     : 370.248s

Choices      : 5664762  (Domain: 5551769)
Conflicts    : 356322   (Analyzed: 356319)
Restarts     : 4345     (Average: 82.01 Last: 221)
Model-Level  : 322.0   
Problems     : 48       (Average Length: 67.94 Splits: 0)
Lemmas       : 356319   (Deleted: 320981)
  Binary     : 13212    (Ratio:   3.71%)
  Ternary    : 3688     (Ratio:   1.04%)
  Conflict   : 356319   (Average Length:  313.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 356319   (Average: 14.14 Max: 1019 Sum: 5036926)
  Executed   : 356220   (Average: 14.13 Max: 1019 Sum: 5033310 Ratio:  99.93%)
  Bounded    : 99       (Average: 36.53 Max: 107 Sum:   3616 Ratio:   0.07%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 5640231  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 5.19s
Memory:		 806MB (+0MB)
UNKNOWN
Iteration Time:	 5.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,1,True), (22,110,0,True), (23,115,0,True)]
Grounded Until:	 105
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 49
Time         : 385.109s (Solving: 360.32s 1st Model: 0.01s Unsat: 2.14s)
CPU Time     : 385.132s

Choices      : 5907905  (Domain: 5791880)
Conflicts    : 365178   (Analyzed: 365175)
Restarts     : 4445     (Average: 82.15 Last: 221)
Model-Level  : 322.0   
Problems     : 49       (Average Length: 68.73 Splits: 0)
Lemmas       : 365175   (Deleted: 330136)
  Binary     : 13666    (Ratio:   3.74%)
  Ternary    : 3772     (Ratio:   1.03%)
  Conflict   : 365175   (Average Length:  320.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 365175   (Average: 14.40 Max: 1019 Sum: 5256709)
  Executed   : 365074   (Average: 14.38 Max: 1019 Sum: 5252885 Ratio:  99.93%)
  Bounded    : 101      (Average: 37.86 Max: 107 Sum:   3824 Ratio:   0.07%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 5640231  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 14.83s
Memory:		 806MB (+0MB)
UNKNOWN
Iteration Time:	 14.89s

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,1,True), (22,110,0,True), (23,115,0,True)]
Grounded Until:	 105
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 50
Time         : 397.779s (Solving: 372.82s 1st Model: 0.01s Unsat: 2.14s)
CPU Time     : 397.804s

Choices      : 6123015  (Domain: 6005373)
Conflicts    : 374235   (Analyzed: 374232)
Restarts     : 4545     (Average: 82.34 Last: 221)
Model-Level  : 322.0   
Problems     : 50       (Average Length: 69.50 Splits: 0)
Lemmas       : 374232   (Deleted: 338137)
  Binary     : 14011    (Ratio:   3.74%)
  Ternary    : 3835     (Ratio:   1.02%)
  Conflict   : 374232   (Average Length:  322.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 374232   (Average: 14.57 Max: 1019 Sum: 5452543)
  Executed   : 374129   (Average: 14.56 Max: 1019 Sum: 5448513 Ratio:  99.93%)
  Bounded    : 103      (Average: 39.13 Max: 107 Sum:   4030 Ratio:   0.07%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 5640231  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 12.61s
Memory:		 806MB (+0MB)
UNKNOWN
Iteration Time:	 12.68s

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

Models       : 0+
Calls        : 51
Time         : 406.189s (Solving: 381.06s 1st Model: 0.01s Unsat: 2.14s)
CPU Time     : 406.216s

Choices      : 6278943  (Domain: 6160632)
Conflicts    : 382636   (Analyzed: 382633)
Restarts     : 4645     (Average: 82.38 Last: 221)
Model-Level  : 322.0   
Problems     : 51       (Average Length: 70.24 Splits: 0)
Lemmas       : 382633   (Deleted: 344718)
  Binary     : 14158    (Ratio:   3.70%)
  Ternary    : 3866     (Ratio:   1.01%)
  Conflict   : 382633   (Average Length:  323.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 382633   (Average: 14.61 Max: 1019 Sum: 5589612)
  Executed   : 382530   (Average: 14.60 Max: 1019 Sum: 5585582 Ratio:  99.93%)
  Bounded    : 103      (Average: 39.13 Max: 107 Sum:   4030 Ratio:   0.07%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 5640231  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 52
Time         : 417.065s (Solving: 391.78s 1st Model: 0.01s Unsat: 2.14s)
CPU Time     : 417.096s

Choices      : 6491163  (Domain: 6371899)
Conflicts    : 391094   (Analyzed: 391091)
Restarts     : 4745     (Average: 82.42 Last: 221)
Model-Level  : 322.0   
Problems     : 52       (Average Length: 70.94 Splits: 0)
Lemmas       : 391091   (Deleted: 352685)
  Binary     : 14329    (Ratio:   3.66%)
  Ternary    : 3891     (Ratio:   0.99%)
  Conflict   : 391091   (Average Length:  325.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 391091   (Average: 14.78 Max: 1129 Sum: 5780982)
  Executed   : 390988   (Average: 14.77 Max: 1129 Sum: 5776952 Ratio:  99.93%)
  Bounded    : 103      (Average: 39.13 Max: 107 Sum:   4030 Ratio:   0.07%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 5640231  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 10.83s
Memory:		 806MB (+0MB)
UNKNOWN
Iteration Time:	 10.88s

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

Models       : 0+
Calls        : 53
Time         : 425.153s (Solving: 399.71s 1st Model: 0.01s Unsat: 2.14s)
CPU Time     : 425.188s

Choices      : 6626671  (Domain: 6506891)
Conflicts    : 399042   (Analyzed: 399039)
Restarts     : 4845     (Average: 82.36 Last: 221)
Model-Level  : 322.0   
Problems     : 53       (Average Length: 71.62 Splits: 0)
Lemmas       : 399039   (Deleted: 360800)
  Binary     : 14405    (Ratio:   3.61%)
  Ternary    : 3905     (Ratio:   0.98%)
  Conflict   : 399039   (Average Length:  326.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 399039   (Average: 14.78 Max: 1129 Sum: 5897383)
  Executed   : 398936   (Average: 14.77 Max: 1129 Sum: 5893353 Ratio:  99.93%)
  Bounded    : 103      (Average: 39.13 Max: 107 Sum:   4030 Ratio:   0.07%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 5640231  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 8.04s
Memory:		 806MB (+0MB)
UNKNOWN
Iteration Time:	 8.09s

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

Models       : 0+
Calls        : 54
Time         : 440.722s (Solving: 415.13s 1st Model: 0.01s Unsat: 2.14s)
CPU Time     : 440.748s

Choices      : 6958921  (Domain: 6837589)
Conflicts    : 408648   (Analyzed: 408645)
Restarts     : 4945     (Average: 82.64 Last: 221)
Model-Level  : 322.0   
Problems     : 54       (Average Length: 72.28 Splits: 0)
Lemmas       : 408645   (Deleted: 370486)
  Binary     : 14655    (Ratio:   3.59%)
  Ternary    : 3958     (Ratio:   0.97%)
  Conflict   : 408645   (Average Length:  330.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 408645   (Average: 15.17 Max: 1326 Sum: 6200199)
  Executed   : 408541   (Average: 15.16 Max: 1326 Sum: 6196062 Ratio:  99.93%)
  Bounded    : 104      (Average: 39.78 Max: 107 Sum:   4137 Ratio:   0.07%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 5640231  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 15.51s
Memory:		 806MB (+0MB)
UNKNOWN
Iteration Time:	 15.56s

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

Models       : 0+
Calls        : 55
Time         : 458.109s (Solving: 432.36s 1st Model: 0.01s Unsat: 2.14s)
CPU Time     : 458.120s

Choices      : 7237170  (Domain: 7115737)
Conflicts    : 417592   (Analyzed: 417589)
Restarts     : 5045     (Average: 82.77 Last: 221)
Model-Level  : 322.0   
Problems     : 55       (Average Length: 72.91 Splits: 0)
Lemmas       : 417589   (Deleted: 379547)
  Binary     : 15074    (Ratio:   3.61%)
  Ternary    : 3973     (Ratio:   0.95%)
  Conflict   : 417589   (Average Length:  346.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 417589   (Average: 15.43 Max: 1326 Sum: 6441418)
  Executed   : 417485   (Average: 15.42 Max: 1326 Sum: 6437281 Ratio:  99.94%)
  Bounded    : 104      (Average: 39.78 Max: 107 Sum:   4137 Ratio:   0.06%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 5640217  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 17.32s
Memory:		 870MB (+64MB)
UNKNOWN
Iteration Time:	 17.37s

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

Models       : 0+
Calls        : 56
Time         : 465.350s (Solving: 438.42s 1st Model: 0.01s Unsat: 2.14s)
CPU Time     : 465.364s

Choices      : 7315332  (Domain: 7193898)
Conflicts    : 425459   (Analyzed: 425456)
Restarts     : 5145     (Average: 82.69 Last: 221)
Model-Level  : 322.0   
Problems     : 56       (Average Length: 73.61 Splits: 0)
Lemmas       : 425456   (Deleted: 386050)
  Binary     : 15121    (Ratio:   3.55%)
  Ternary    : 3976     (Ratio:   0.93%)
  Conflict   : 425456   (Average Length:  344.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 425456   (Average: 15.26 Max: 1326 Sum: 6492710)
  Executed   : 425352   (Average: 15.25 Max: 1326 Sum: 6488573 Ratio:  99.94%)
  Bounded    : 104      (Average: 39.78 Max: 107 Sum:   4137 Ratio:   0.06%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 5922677  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 6.21s
Memory:		 901MB (+29MB)
UNKNOWN
Iteration Time:	 7.26s

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

Models       : 0+
Calls        : 57
Time         : 472.315s (Solving: 444.20s 1st Model: 0.01s Unsat: 2.14s)
CPU Time     : 472.328s

Choices      : 7373291  (Domain: 7251857)
Conflicts    : 432303   (Analyzed: 432300)
Restarts     : 5245     (Average: 82.42 Last: 221)
Model-Level  : 322.0   
Problems     : 57       (Average Length: 74.37 Splits: 0)
Lemmas       : 432300   (Deleted: 393722)
  Binary     : 15128    (Ratio:   3.50%)
  Ternary    : 3977     (Ratio:   0.92%)
  Conflict   : 432300   (Average Length:  343.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 432300   (Average: 15.09 Max: 1326 Sum: 6521908)
  Executed   : 432196   (Average: 15.08 Max: 1326 Sum: 6517771 Ratio:  99.94%)
  Bounded    : 104      (Average: 39.78 Max: 107 Sum:   4137 Ratio:   0.06%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 6205137  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 5.93s
Memory:		 921MB (+20MB)
UNKNOWN
Iteration Time:	 6.97s

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,2,False), (22,110,1,True), (23,115,1,True)]
Grounded Until:	 115
Blocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 58
Time         : 483.283s (Solving: 454.99s 1st Model: 0.01s Unsat: 2.14s)
CPU Time     : 483.300s

Choices      : 7441261  (Domain: 7319827)
Conflicts    : 440818   (Analyzed: 440815)
Restarts     : 5345     (Average: 82.47 Last: 221)
Model-Level  : 322.0   
Problems     : 58       (Average Length: 75.10 Splits: 0)
Lemmas       : 440815   (Deleted: 400351)
  Binary     : 15293    (Ratio:   3.47%)
  Ternary    : 3998     (Ratio:   0.91%)
  Conflict   : 440815   (Average Length:  349.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 440815   (Average: 14.94 Max: 1326 Sum: 6586889)
  Executed   : 440711   (Average: 14.93 Max: 1326 Sum: 6582752 Ratio:  99.94%)
  Bounded    : 104      (Average: 39.78 Max: 107 Sum:   4137 Ratio:   0.06%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 6205137  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 10.91s
Memory:		 925MB (+4MB)
UNKNOWN
Iteration Time:	 10.98s

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,2,False), (22,110,1,True), (23,115,1,True)]
Grounded Until:	 115
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 59
Time         : 488.970s (Solving: 460.51s 1st Model: 0.01s Unsat: 2.14s)
CPU Time     : 488.988s

Choices      : 7493198  (Domain: 7371764)
Conflicts    : 449370   (Analyzed: 449367)
Restarts     : 5445     (Average: 82.53 Last: 221)
Model-Level  : 322.0   
Problems     : 59       (Average Length: 75.81 Splits: 0)
Lemmas       : 449367   (Deleted: 408507)
  Binary     : 15334    (Ratio:   3.41%)
  Ternary    : 4006     (Ratio:   0.89%)
  Conflict   : 449367   (Average Length:  352.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 449367   (Average: 14.76 Max: 1326 Sum: 6630414)
  Executed   : 449262   (Average: 14.75 Max: 1326 Sum: 6626160 Ratio:  99.94%)
  Bounded    : 105      (Average: 40.51 Max: 117 Sum:   4254 Ratio:   0.06%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 6205137  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 5.63s
Memory:		 925MB (+0MB)
UNKNOWN
Iteration Time:	 5.69s

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,2,False), (22,110,1,True), (23,115,1,True)]
Grounded Until:	 115
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 60
Time         : 494.175s (Solving: 465.51s 1st Model: 0.01s Unsat: 2.14s)
CPU Time     : 494.196s

Choices      : 7543905  (Domain: 7422471)
Conflicts    : 457219   (Analyzed: 457216)
Restarts     : 5545     (Average: 82.46 Last: 221)
Model-Level  : 322.0   
Problems     : 60       (Average Length: 76.50 Splits: 0)
Lemmas       : 457216   (Deleted: 416602)
  Binary     : 15389    (Ratio:   3.37%)
  Ternary    : 4032     (Ratio:   0.88%)
  Conflict   : 457216   (Average Length:  352.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 457216   (Average: 14.59 Max: 1326 Sum: 6671356)
  Executed   : 457110   (Average: 14.58 Max: 1326 Sum: 6666985 Ratio:  99.93%)
  Bounded    : 106      (Average: 41.24 Max: 117 Sum:   4371 Ratio:   0.07%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 6205112  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 5.13s
Memory:		 925MB (+0MB)
UNKNOWN
Iteration Time:	 5.21s

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,2,False), (22,110,1,True), (23,115,1,True)]
Grounded Until:	 115
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 61
Time         : 498.319s (Solving: 469.49s 1st Model: 0.01s Unsat: 2.14s)
CPU Time     : 498.340s

Choices      : 7595569  (Domain: 7474135)
Conflicts    : 465031   (Analyzed: 465028)
Restarts     : 5645     (Average: 82.38 Last: 221)
Model-Level  : 322.0   
Problems     : 61       (Average Length: 77.16 Splits: 0)
Lemmas       : 465028   (Deleted: 424260)
  Binary     : 15426    (Ratio:   3.32%)
  Ternary    : 4052     (Ratio:   0.87%)
  Conflict   : 465028   (Average Length:  353.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 465028   (Average: 14.44 Max: 1326 Sum: 6713154)
  Executed   : 464922   (Average: 14.43 Max: 1326 Sum: 6708783 Ratio:  99.93%)
  Bounded    : 106      (Average: 41.24 Max: 117 Sum:   4371 Ratio:   0.07%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 6205086  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 4.09s
Memory:		 925MB (+0MB)
UNKNOWN
Iteration Time:	 4.15s

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,2,False), (22,110,1,True), (23,115,1,True)]
Grounded Until:	 115
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 62
Time         : 504.104s (Solving: 475.10s 1st Model: 0.01s Unsat: 2.14s)
CPU Time     : 504.120s

Choices      : 7649314  (Domain: 7527880)
Conflicts    : 472799   (Analyzed: 472796)
Restarts     : 5745     (Average: 82.30 Last: 221)
Model-Level  : 322.0   
Problems     : 62       (Average Length: 77.81 Splits: 0)
Lemmas       : 472796   (Deleted: 431704)
  Binary     : 15465    (Ratio:   3.27%)
  Ternary    : 4070     (Ratio:   0.86%)
  Conflict   : 472796   (Average Length:  358.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 472796   (Average: 14.29 Max: 1326 Sum: 6755342)
  Executed   : 472689   (Average: 14.28 Max: 1326 Sum: 6750859 Ratio:  99.93%)
  Bounded    : 107      (Average: 41.90 Max: 117 Sum:   4483 Ratio:   0.07%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 6205086  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 5.72s
Memory:		 925MB (+0MB)
UNKNOWN
Iteration Time:	 5.79s

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,2,False), (22,110,1,True), (23,115,1,True)]
Grounded Until:	 115
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 63
Time         : 511.950s (Solving: 482.78s 1st Model: 0.01s Unsat: 2.14s)
CPU Time     : 511.968s

Choices      : 7718302  (Domain: 7596868)
Conflicts    : 480807   (Analyzed: 480804)
Restarts     : 5845     (Average: 82.26 Last: 221)
Model-Level  : 322.0   
Problems     : 63       (Average Length: 78.43 Splits: 0)
Lemmas       : 480804   (Deleted: 439470)
  Binary     : 15573    (Ratio:   3.24%)
  Ternary    : 4090     (Ratio:   0.85%)
  Conflict   : 480804   (Average Length:  359.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 480804   (Average: 14.16 Max: 1326 Sum: 6809245)
  Executed   : 480697   (Average: 14.15 Max: 1326 Sum: 6804762 Ratio:  99.93%)
  Bounded    : 107      (Average: 41.90 Max: 117 Sum:   4483 Ratio:   0.07%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 6205086  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 7.79s
Memory:		 925MB (+0MB)
UNKNOWN
Iteration Time:	 7.85s

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,2,False), (22,110,1,True), (23,115,1,True)]
Grounded Until:	 115
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 64
Time         : 517.366s (Solving: 488.02s 1st Model: 0.01s Unsat: 2.14s)
CPU Time     : 517.388s

Choices      : 7766295  (Domain: 7644766)
Conflicts    : 488782   (Analyzed: 488779)
Restarts     : 5945     (Average: 82.22 Last: 221)
Model-Level  : 322.0   
Problems     : 64       (Average Length: 79.03 Splits: 0)
Lemmas       : 488779   (Deleted: 447004)
  Binary     : 15589    (Ratio:   3.19%)
  Ternary    : 4094     (Ratio:   0.84%)
  Conflict   : 488779   (Average Length:  356.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 488779   (Average: 14.01 Max: 1326 Sum: 6848655)
  Executed   : 488670   (Average: 14.00 Max: 1326 Sum: 6843943 Ratio:  99.93%)
  Bounded    : 109      (Average: 43.23 Max: 117 Sum:   4712 Ratio:   0.07%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 6205086  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 5.36s
Memory:		 925MB (+0MB)
UNKNOWN
Iteration Time:	 5.42s

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,2,False), (22,110,1,True), (23,115,1,True)]
Grounded Until:	 115
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 65
Time         : 520.789s (Solving: 491.24s 1st Model: 0.01s Unsat: 2.14s)
CPU Time     : 520.812s

Choices      : 7815837  (Domain: 7694282)
Conflicts    : 495988   (Analyzed: 495985)
Restarts     : 6045     (Average: 82.05 Last: 221)
Model-Level  : 322.0   
Problems     : 65       (Average Length: 79.62 Splits: 0)
Lemmas       : 495985   (Deleted: 454832)
  Binary     : 15602    (Ratio:   3.15%)
  Ternary    : 4100     (Ratio:   0.83%)
  Conflict   : 495985   (Average Length:  355.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 495985   (Average: 13.88 Max: 1326 Sum: 6885801)
  Executed   : 495876   (Average: 13.87 Max: 1326 Sum: 6881089 Ratio:  99.93%)
  Bounded    : 109      (Average: 43.23 Max: 117 Sum:   4712 Ratio:   0.07%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 6205072  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 3.34s
Memory:		 925MB (+0MB)
UNKNOWN
Iteration Time:	 3.43s

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,2,False), (22,110,1,True), (23,115,1,True)]
Grounded Until:	 115
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 66
Time         : 528.428s (Solving: 498.69s 1st Model: 0.01s Unsat: 2.14s)
CPU Time     : 528.456s

Choices      : 7924115  (Domain: 7802493)
Conflicts    : 504440   (Analyzed: 504437)
Restarts     : 6145     (Average: 82.09 Last: 221)
Model-Level  : 322.0   
Problems     : 66       (Average Length: 80.18 Splits: 0)
Lemmas       : 504437   (Deleted: 461924)
  Binary     : 15661    (Ratio:   3.10%)
  Ternary    : 4112     (Ratio:   0.82%)
  Conflict   : 504437   (Average Length:  357.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 504437   (Average: 13.83 Max: 1326 Sum: 6976887)
  Executed   : 504328   (Average: 13.82 Max: 1326 Sum: 6972175 Ratio:  99.93%)
  Bounded    : 109      (Average: 43.23 Max: 117 Sum:   4712 Ratio:   0.07%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 6205072  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 7.57s
Memory:		 925MB (+0MB)
UNKNOWN
Iteration Time:	 7.64s

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

Models       : 0+
Calls        : 67
Time         : 535.408s (Solving: 505.49s 1st Model: 0.01s Unsat: 2.14s)
CPU Time     : 535.436s

Choices      : 8037641  (Domain: 7916009)
Conflicts    : 512790   (Analyzed: 512787)
Restarts     : 6245     (Average: 82.11 Last: 221)
Model-Level  : 322.0   
Problems     : 67       (Average Length: 80.73 Splits: 0)
Lemmas       : 512787   (Deleted: 470277)
  Binary     : 15689    (Ratio:   3.06%)
  Ternary    : 4122     (Ratio:   0.80%)
  Conflict   : 512787   (Average Length:  360.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 512787   (Average: 13.78 Max: 1333 Sum: 7068724)
  Executed   : 512678   (Average: 13.78 Max: 1333 Sum: 7064012 Ratio:  99.93%)
  Bounded    : 109      (Average: 43.23 Max: 117 Sum:   4712 Ratio:   0.07%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 6205072  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 68
Time         : 541.339s (Solving: 511.25s 1st Model: 0.01s Unsat: 2.14s)
CPU Time     : 541.368s

Choices      : 8120587  (Domain: 7998877)
Conflicts    : 520808   (Analyzed: 520805)
Restarts     : 6345     (Average: 82.08 Last: 221)
Model-Level  : 322.0   
Problems     : 68       (Average Length: 81.26 Splits: 0)
Lemmas       : 520805   (Deleted: 478411)
  Binary     : 15766    (Ratio:   3.03%)
  Ternary    : 4132     (Ratio:   0.79%)
  Conflict   : 520805   (Average Length:  360.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 520805   (Average: 13.69 Max: 1538 Sum: 7132365)
  Executed   : 520694   (Average: 13.69 Max: 1538 Sum: 7127425 Ratio:  99.93%)
  Bounded    : 111      (Average: 44.50 Max: 117 Sum:   4940 Ratio:   0.07%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 6205072  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

Iteration 68
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        : 69
Time         : 547.634s (Solving: 517.34s 1st Model: 0.01s Unsat: 2.14s)
CPU Time     : 547.668s

Choices      : 8170795  (Domain: 8049085)
Conflicts    : 529155   (Analyzed: 529152)
Restarts     : 6445     (Average: 82.10 Last: 221)
Model-Level  : 322.0   
Problems     : 69       (Average Length: 81.78 Splits: 0)
Lemmas       : 529152   (Deleted: 486090)
  Binary     : 15808    (Ratio:   2.99%)
  Ternary    : 4142     (Ratio:   0.78%)
  Conflict   : 529152   (Average Length:  360.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 529152   (Average: 13.56 Max: 1538 Sum: 7177285)
  Executed   : 529041   (Average: 13.55 Max: 1538 Sum: 7172345 Ratio:  99.93%)
  Bounded    : 111      (Average: 44.50 Max: 117 Sum:   4940 Ratio:   0.07%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 6205072  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

Iteration 69
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        : 70
Time         : 556.489s (Solving: 526.03s 1st Model: 0.01s Unsat: 2.14s)
CPU Time     : 556.512s

Choices      : 8227207  (Domain: 8105497)
Conflicts    : 537807   (Analyzed: 537804)
Restarts     : 6545     (Average: 82.17 Last: 221)
Model-Level  : 322.0   
Problems     : 70       (Average Length: 82.29 Splits: 0)
Lemmas       : 537804   (Deleted: 495889)
  Binary     : 15863    (Ratio:   2.95%)
  Ternary    : 4159     (Ratio:   0.77%)
  Conflict   : 537804   (Average Length:  367.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 537804   (Average: 13.43 Max: 1538 Sum: 7222186)
  Executed   : 537693   (Average: 13.42 Max: 1538 Sum: 7217246 Ratio:  99.93%)
  Bounded    : 111      (Average: 44.50 Max: 117 Sum:   4940 Ratio:   0.07%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 6205072  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 8.79s
Memory:		 925MB (+0MB)
UNKNOWN
Iteration Time:	 8.85s

Iteration 70
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        : 71
Time         : 561.603s (Solving: 530.98s 1st Model: 0.01s Unsat: 2.14s)
CPU Time     : 561.628s

Choices      : 8284024  (Domain: 8162314)
Conflicts    : 545857   (Analyzed: 545854)
Restarts     : 6645     (Average: 82.15 Last: 221)
Model-Level  : 322.0   
Problems     : 71       (Average Length: 82.77 Splits: 0)
Lemmas       : 545854   (Deleted: 502523)
  Binary     : 15918    (Ratio:   2.92%)
  Ternary    : 4179     (Ratio:   0.77%)
  Conflict   : 545854   (Average Length:  371.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 545854   (Average: 13.31 Max: 1538 Sum: 7265639)
  Executed   : 545742   (Average: 13.30 Max: 1538 Sum: 7260587 Ratio:  99.93%)
  Bounded    : 112      (Average: 45.11 Max: 117 Sum:   5052 Ratio:   0.07%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 6205072  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

Iteration 71
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        : 72
Time         : 566.109s (Solving: 535.31s 1st Model: 0.01s Unsat: 2.14s)
CPU Time     : 566.136s

Choices      : 8325119  (Domain: 8203409)
Conflicts    : 553881   (Analyzed: 553878)
Restarts     : 6745     (Average: 82.12 Last: 221)
Model-Level  : 322.0   
Problems     : 72       (Average Length: 83.25 Splits: 0)
Lemmas       : 553878   (Deleted: 510065)
  Binary     : 15937    (Ratio:   2.88%)
  Ternary    : 4198     (Ratio:   0.76%)
  Conflict   : 553878   (Average Length:  369.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 553878   (Average: 13.18 Max: 1538 Sum: 7299719)
  Executed   : 553765   (Average: 13.17 Max: 1538 Sum: 7294555 Ratio:  99.93%)
  Bounded    : 113      (Average: 45.70 Max: 117 Sum:   5164 Ratio:   0.07%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 6205072  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 4.45s
Memory:		 925MB (+0MB)
UNKNOWN
Iteration Time:	 4.51s

Iteration 72
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        : 73
Time         : 576.457s (Solving: 545.49s 1st Model: 0.01s Unsat: 2.14s)
CPU Time     : 576.488s

Choices      : 8394526  (Domain: 8272816)
Conflicts    : 562265   (Analyzed: 562262)
Restarts     : 6845     (Average: 82.14 Last: 221)
Model-Level  : 322.0   
Problems     : 73       (Average Length: 83.71 Splits: 0)
Lemmas       : 562262   (Deleted: 518147)
  Binary     : 16107    (Ratio:   2.86%)
  Ternary    : 4227     (Ratio:   0.75%)
  Conflict   : 562262   (Average Length:  393.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 562262   (Average: 13.06 Max: 1538 Sum: 7343275)
  Executed   : 562149   (Average: 13.05 Max: 1538 Sum: 7338111 Ratio:  99.93%)
  Bounded    : 113      (Average: 45.70 Max: 117 Sum:   5164 Ratio:   0.07%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 6205072  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 10.30s
Memory:		 925MB (+0MB)
UNKNOWN
Iteration Time:	 10.35s

Iteration 73
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        : 74
Time         : 583.031s (Solving: 551.89s 1st Model: 0.01s Unsat: 2.14s)
CPU Time     : 583.064s

Choices      : 8453534  (Domain: 8331824)
Conflicts    : 570109   (Analyzed: 570106)
Restarts     : 6945     (Average: 82.09 Last: 221)
Model-Level  : 322.0   
Problems     : 74       (Average Length: 84.16 Splits: 0)
Lemmas       : 570106   (Deleted: 526170)
  Binary     : 16203    (Ratio:   2.84%)
  Ternary    : 4234     (Ratio:   0.74%)
  Conflict   : 570106   (Average Length:  404.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 570106   (Average: 12.95 Max: 1538 Sum: 7381640)
  Executed   : 569993   (Average: 12.94 Max: 1538 Sum: 7376476 Ratio:  99.93%)
  Bounded    : 113      (Average: 45.70 Max: 117 Sum:   5164 Ratio:   0.07%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 6205072  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

Iteration 74
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        : 75
Time         : 585.976s (Solving: 554.67s 1st Model: 0.01s Unsat: 2.14s)
CPU Time     : 586.008s

Choices      : 8491845  (Domain: 8370135)
Conflicts    : 577583   (Analyzed: 577580)
Restarts     : 7045     (Average: 81.98 Last: 221)
Model-Level  : 322.0   
Problems     : 75       (Average Length: 84.60 Splits: 0)
Lemmas       : 577580   (Deleted: 533636)
  Binary     : 16207    (Ratio:   2.81%)
  Ternary    : 4238     (Ratio:   0.73%)
  Conflict   : 577580   (Average Length:  402.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 577580   (Average: 12.83 Max: 1538 Sum: 7407895)
  Executed   : 577467   (Average: 12.82 Max: 1538 Sum: 7402731 Ratio:  99.93%)
  Bounded    : 113      (Average: 45.70 Max: 117 Sum:   5164 Ratio:   0.07%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 6205072  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 2.89s
Memory:		 925MB (+0MB)
UNKNOWN
Iteration Time:	 2.95s

Iteration 75
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        : 76
Time         : 592.477s (Solving: 560.99s 1st Model: 0.01s Unsat: 2.14s)
CPU Time     : 592.512s

Choices      : 8570220  (Domain: 8448305)
Conflicts    : 585867   (Analyzed: 585864)
Restarts     : 7145     (Average: 82.00 Last: 221)
Model-Level  : 322.0   
Problems     : 76       (Average Length: 85.03 Splits: 0)
Lemmas       : 585864   (Deleted: 541063)
  Binary     : 16253    (Ratio:   2.77%)
  Ternary    : 4257     (Ratio:   0.73%)
  Conflict   : 585864   (Average Length:  403.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 585864   (Average: 12.75 Max: 1538 Sum: 7470737)
  Executed   : 585751   (Average: 12.74 Max: 1538 Sum: 7465573 Ratio:  99.93%)
  Bounded    : 113      (Average: 45.70 Max: 117 Sum:   5164 Ratio:   0.07%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 6205072  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 6.44s
Memory:		 925MB (+0MB)
UNKNOWN
Iteration Time:	 6.51s

Iteration 76
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        : 77
Time         : 599.102s (Solving: 567.44s 1st Model: 0.01s Unsat: 2.14s)
CPU Time     : 599.136s

Choices      : 8644075  (Domain: 8522150)
Conflicts    : 594587   (Analyzed: 594584)
Restarts     : 7245     (Average: 82.07 Last: 221)
Model-Level  : 322.0   
Problems     : 77       (Average Length: 85.44 Splits: 0)
Lemmas       : 594584   (Deleted: 551026)
  Binary     : 16277    (Ratio:   2.74%)
  Ternary    : 4262     (Ratio:   0.72%)
  Conflict   : 594584   (Average Length:  406.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 594584   (Average: 12.66 Max: 1538 Sum: 7525737)
  Executed   : 594471   (Average: 12.65 Max: 1538 Sum: 7520573 Ratio:  99.93%)
  Bounded    : 113      (Average: 45.70 Max: 117 Sum:   5164 Ratio:   0.07%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 6205072  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

Iteration 77
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        : 78
Time         : 605.460s (Solving: 573.63s 1st Model: 0.01s Unsat: 2.14s)
CPU Time     : 605.496s

Choices      : 8738809  (Domain: 8616761)
Conflicts    : 602894   (Analyzed: 602891)
Restarts     : 7345     (Average: 82.08 Last: 221)
Model-Level  : 322.0   
Problems     : 78       (Average Length: 85.85 Splits: 0)
Lemmas       : 602891   (Deleted: 557724)
  Binary     : 16312    (Ratio:   2.71%)
  Ternary    : 4268     (Ratio:   0.71%)
  Conflict   : 602891   (Average Length:  407.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 602891   (Average: 12.61 Max: 1538 Sum: 7602968)
  Executed   : 602778   (Average: 12.60 Max: 1538 Sum: 7597804 Ratio:  99.93%)
  Bounded    : 113      (Average: 45.70 Max: 117 Sum:   5164 Ratio:   0.07%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 6205072  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 6.31s
Memory:		 925MB (+0MB)
UNKNOWN
Iteration Time:	 6.36s

Iteration 78
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        : 79
Time         : 613.794s (Solving: 581.79s 1st Model: 0.01s Unsat: 10.30s)
CPU Time     : 613.820s

Choices      : 8786245  (Domain: 8664197)
Conflicts    : 608177   (Analyzed: 608173)
Restarts     : 7407     (Average: 82.11 Last: 221)
Model-Level  : 322.0   
Problems     : 79       (Average Length: 86.24 Splits: 0)
Lemmas       : 608173   (Deleted: 562234)
  Binary     : 16354    (Ratio:   2.69%)
  Ternary    : 4272     (Ratio:   0.70%)
  Conflict   : 608173   (Average Length:  408.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 608173   (Average: 12.58 Max: 1538 Sum: 7648979)
  Executed   : 608059   (Average: 12.57 Max: 1538 Sum: 7643814 Ratio:  99.93%)
  Bounded    : 114      (Average: 45.31 Max: 117 Sum:   5165 Ratio:   0.07%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 6205072  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 8.27s
Memory:		 925MB (+0MB)
UNSAT
Iteration Time:	 8.33s

Iteration 79
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        : 80
Time         : 618.448s (Solving: 586.25s 1st Model: 0.01s Unsat: 10.30s)
CPU Time     : 618.476s

Choices      : 8824796  (Domain: 8702748)
Conflicts    : 615412   (Analyzed: 615408)
Restarts     : 7507     (Average: 81.98 Last: 221)
Model-Level  : 322.0   
Problems     : 80       (Average Length: 86.62 Splits: 0)
Lemmas       : 615408   (Deleted: 570985)
  Binary     : 16365    (Ratio:   2.66%)
  Ternary    : 4275     (Ratio:   0.69%)
  Conflict   : 615408   (Average Length:  408.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 615408   (Average: 12.47 Max: 1538 Sum: 7676488)
  Executed   : 615294   (Average: 12.47 Max: 1538 Sum: 7671323 Ratio:  99.93%)
  Bounded    : 114      (Average: 45.31 Max: 117 Sum:   5165 Ratio:   0.07%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 6205072  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 4.58s
Memory:		 925MB (+0MB)
UNKNOWN
Iteration Time:	 4.66s

Iteration 80
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        : 81
Time         : 621.063s (Solving: 588.68s 1st Model: 0.01s Unsat: 10.30s)
CPU Time     : 621.092s

Choices      : 8857578  (Domain: 8735530)
Conflicts    : 622382   (Analyzed: 622378)
Restarts     : 7607     (Average: 81.82 Last: 221)
Model-Level  : 322.0   
Problems     : 81       (Average Length: 87.00 Splits: 0)
Lemmas       : 622378   (Deleted: 577860)
  Binary     : 16371    (Ratio:   2.63%)
  Ternary    : 4275     (Ratio:   0.69%)
  Conflict   : 622378   (Average Length:  406.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 622378   (Average: 12.37 Max: 1538 Sum: 7700252)
  Executed   : 622264   (Average: 12.36 Max: 1538 Sum: 7695087 Ratio:  99.93%)
  Bounded    : 114      (Average: 45.31 Max: 117 Sum:   5165 Ratio:   0.07%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 6205072  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 2.55s
Memory:		 925MB (+0MB)
UNKNOWN
Iteration Time:	 2.62s

Iteration 81
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        : 82
Time         : 624.298s (Solving: 591.75s 1st Model: 0.01s Unsat: 10.30s)
CPU Time     : 624.328s

Choices      : 8896750  (Domain: 8774702)
Conflicts    : 630170   (Analyzed: 630166)
Restarts     : 7707     (Average: 81.77 Last: 221)
Model-Level  : 322.0   
Problems     : 82       (Average Length: 87.37 Splits: 0)
Lemmas       : 630166   (Deleted: 584140)
  Binary     : 16382    (Ratio:   2.60%)
  Ternary    : 4278     (Ratio:   0.68%)
  Conflict   : 630166   (Average Length:  404.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 630166   (Average: 12.27 Max: 1538 Sum: 7730547)
  Executed   : 630052   (Average: 12.26 Max: 1538 Sum: 7725382 Ratio:  99.93%)
  Bounded    : 114      (Average: 45.31 Max: 117 Sum:   5165 Ratio:   0.07%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 6205072  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 3.18s
Memory:		 925MB (+0MB)
UNKNOWN
Iteration Time:	 3.24s

Iteration 82
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        : 83
Time         : 634.155s (Solving: 601.43s 1st Model: 0.01s Unsat: 10.30s)
CPU Time     : 634.188s

Choices      : 8953417  (Domain: 8831369)
Conflicts    : 637696   (Analyzed: 637692)
Restarts     : 7807     (Average: 81.68 Last: 221)
Model-Level  : 322.0   
Problems     : 83       (Average Length: 87.72 Splits: 0)
Lemmas       : 637692   (Deleted: 592670)
  Binary     : 16476    (Ratio:   2.58%)
  Ternary    : 4282     (Ratio:   0.67%)
  Conflict   : 637692   (Average Length:  431.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 637692   (Average: 12.17 Max: 1538 Sum: 7759827)
  Executed   : 637578   (Average: 12.16 Max: 1538 Sum: 7754662 Ratio:  99.93%)
  Bounded    : 114      (Average: 45.31 Max: 117 Sum:   5165 Ratio:   0.07%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 6205072  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

Iteration 83
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        : 84
Time         : 638.343s (Solving: 605.45s 1st Model: 0.01s Unsat: 10.30s)
CPU Time     : 638.380s

Choices      : 9003489  (Domain: 8881441)
Conflicts    : 645559   (Analyzed: 645555)
Restarts     : 7907     (Average: 81.64 Last: 221)
Model-Level  : 322.0   
Problems     : 84       (Average Length: 88.07 Splits: 0)
Lemmas       : 645555   (Deleted: 599992)
  Binary     : 16490    (Ratio:   2.55%)
  Ternary    : 4286     (Ratio:   0.66%)
  Conflict   : 645555   (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    : 645555   (Average: 12.08 Max: 1538 Sum: 7797531)
  Executed   : 645441   (Average: 12.07 Max: 1538 Sum: 7792366 Ratio:  99.93%)
  Bounded    : 114      (Average: 45.31 Max: 117 Sum:   5165 Ratio:   0.07%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 6205072  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 4.13s
Memory:		 925MB (+0MB)
UNKNOWN
Iteration Time:	 4.19s

Iteration 84
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        : 85
Time         : 643.536s (Solving: 610.43s 1st Model: 0.01s Unsat: 10.30s)
CPU Time     : 643.576s

Choices      : 9065227  (Domain: 8943083)
Conflicts    : 653488   (Analyzed: 653484)
Restarts     : 8007     (Average: 81.61 Last: 221)
Model-Level  : 322.0   
Problems     : 85       (Average Length: 88.41 Splits: 0)
Lemmas       : 653484   (Deleted: 607120)
  Binary     : 16518    (Ratio:   2.53%)
  Ternary    : 4289     (Ratio:   0.66%)
  Conflict   : 653484   (Average Length:  429.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 653484   (Average: 12.01 Max: 1538 Sum: 7846610)
  Executed   : 653370   (Average: 12.00 Max: 1538 Sum: 7841445 Ratio:  99.93%)
  Bounded    : 114      (Average: 45.31 Max: 117 Sum:   5165 Ratio:   0.07%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 6205072  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 5.12s
Memory:		 925MB (+0MB)
UNKNOWN
Iteration Time:	 5.20s

Iteration 85
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        : 86
Time         : 650.169s (Solving: 616.87s 1st Model: 0.01s Unsat: 10.30s)
CPU Time     : 650.212s

Choices      : 9157798  (Domain: 9035633)
Conflicts    : 661912   (Analyzed: 661908)
Restarts     : 8107     (Average: 81.65 Last: 221)
Model-Level  : 322.0   
Problems     : 86       (Average Length: 88.74 Splits: 0)
Lemmas       : 661908   (Deleted: 615368)
  Binary     : 16550    (Ratio:   2.50%)
  Ternary    : 4291     (Ratio:   0.65%)
  Conflict   : 661908   (Average Length:  429.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 661908   (Average: 11.96 Max: 1538 Sum: 7919386)
  Executed   : 661793   (Average: 11.96 Max: 1538 Sum: 7914104 Ratio:  99.93%)
  Bounded    : 115      (Average: 45.93 Max: 117 Sum:   5282 Ratio:   0.07%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 6205072  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 87
Time         : 659.326s (Solving: 625.83s 1st Model: 0.01s Unsat: 10.30s)
CPU Time     : 659.372s

Choices      : 9200579  (Domain: 9078414)
Conflicts    : 670031   (Analyzed: 670027)
Restarts     : 8207     (Average: 81.64 Last: 221)
Model-Level  : 322.0   
Problems     : 87       (Average Length: 89.07 Splits: 0)
Lemmas       : 670027   (Deleted: 623588)
  Binary     : 16571    (Ratio:   2.47%)
  Ternary    : 4303     (Ratio:   0.64%)
  Conflict   : 670027   (Average Length:  440.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 670027   (Average: 11.86 Max: 1538 Sum: 7948739)
  Executed   : 669912   (Average: 11.86 Max: 1538 Sum: 7943457 Ratio:  99.93%)
  Bounded    : 115      (Average: 45.93 Max: 117 Sum:   5282 Ratio:   0.07%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 6205058  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 88
Time         : 666.236s (Solving: 632.57s 1st Model: 0.01s Unsat: 10.30s)
CPU Time     : 666.288s

Choices      : 9260775  (Domain: 9138610)
Conflicts    : 678016   (Analyzed: 678012)
Restarts     : 8307     (Average: 81.62 Last: 221)
Model-Level  : 322.0   
Problems     : 88       (Average Length: 89.39 Splits: 0)
Lemmas       : 678012   (Deleted: 631657)
  Binary     : 16618    (Ratio:   2.45%)
  Ternary    : 4319     (Ratio:   0.64%)
  Conflict   : 678012   (Average Length:  448.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 678012   (Average: 11.78 Max: 1538 Sum: 7989757)
  Executed   : 677897   (Average: 11.78 Max: 1538 Sum: 7984475 Ratio:  99.93%)
  Bounded    : 115      (Average: 45.93 Max: 117 Sum:   5282 Ratio:   0.07%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 6205058  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 89
Time         : 669.087s (Solving: 635.22s 1st Model: 0.01s Unsat: 10.30s)
CPU Time     : 669.140s

Choices      : 9295285  (Domain: 9173120)
Conflicts    : 685294   (Analyzed: 685290)
Restarts     : 8407     (Average: 81.51 Last: 221)
Model-Level  : 322.0   
Problems     : 89       (Average Length: 89.70 Splits: 0)
Lemmas       : 685290   (Deleted: 639252)
  Binary     : 16623    (Ratio:   2.43%)
  Ternary    : 4321     (Ratio:   0.63%)
  Conflict   : 685290   (Average Length:  446.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 685290   (Average: 11.69 Max: 1538 Sum: 8013847)
  Executed   : 685175   (Average: 11.69 Max: 1538 Sum: 8008565 Ratio:  99.93%)
  Bounded    : 115      (Average: 45.93 Max: 117 Sum:   5282 Ratio:   0.07%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 6205058  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 2.77s
Memory:		 925MB (+0MB)
UNKNOWN
Iteration Time:	 2.85s

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

Models       : 0+
Calls        : 90
Time         : 675.722s (Solving: 641.69s 1st Model: 0.01s Unsat: 10.30s)
CPU Time     : 675.776s

Choices      : 9351596  (Domain: 9229431)
Conflicts    : 693012   (Analyzed: 693008)
Restarts     : 8507     (Average: 81.46 Last: 221)
Model-Level  : 322.0   
Problems     : 90       (Average Length: 90.00 Splits: 0)
Lemmas       : 693008   (Deleted: 646523)
  Binary     : 16670    (Ratio:   2.41%)
  Ternary    : 4328     (Ratio:   0.62%)
  Conflict   : 693008   (Average Length:  453.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 693008   (Average: 11.62 Max: 1538 Sum: 8049896)
  Executed   : 692893   (Average: 11.61 Max: 1538 Sum: 8044614 Ratio:  99.93%)
  Bounded    : 115      (Average: 45.93 Max: 117 Sum:   5282 Ratio:   0.07%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 6205058  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 6.58s
Memory:		 925MB (+0MB)
UNKNOWN
Iteration Time:	 6.64s

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

Models       : 0+
Calls        : 91
Time         : 682.621s (Solving: 648.37s 1st Model: 0.01s Unsat: 10.30s)
CPU Time     : 682.680s

Choices      : 9414840  (Domain: 9292470)
Conflicts    : 701007   (Analyzed: 701003)
Restarts     : 8607     (Average: 81.45 Last: 221)
Model-Level  : 322.0   
Problems     : 91       (Average Length: 90.30 Splits: 0)
Lemmas       : 701003   (Deleted: 654099)
  Binary     : 16722    (Ratio:   2.39%)
  Ternary    : 4334     (Ratio:   0.62%)
  Conflict   : 701003   (Average Length:  455.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 701003   (Average: 11.55 Max: 1538 Sum: 8096769)
  Executed   : 700888   (Average: 11.54 Max: 1538 Sum: 8091487 Ratio:  99.93%)
  Bounded    : 115      (Average: 45.93 Max: 117 Sum:   5282 Ratio:   0.07%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 6205058  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 92
Time         : 690.489s (Solving: 656.04s 1st Model: 0.01s Unsat: 10.30s)
CPU Time     : 690.548s

Choices      : 9487054  (Domain: 9364532)
Conflicts    : 709389   (Analyzed: 709385)
Restarts     : 8707     (Average: 81.47 Last: 221)
Model-Level  : 322.0   
Problems     : 92       (Average Length: 90.59 Splits: 0)
Lemmas       : 709385   (Deleted: 661856)
  Binary     : 16794    (Ratio:   2.37%)
  Ternary    : 4348     (Ratio:   0.61%)
  Conflict   : 709385   (Average Length:  460.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 709385   (Average: 11.48 Max: 1538 Sum: 8145728)
  Executed   : 709270   (Average: 11.48 Max: 1538 Sum: 8140446 Ratio:  99.94%)
  Bounded    : 115      (Average: 45.93 Max: 117 Sum:   5282 Ratio:   0.06%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 6205058  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 7.79s
Memory:		 925MB (+0MB)
UNKNOWN
Iteration Time:	 7.87s

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

Models       : 0+
Calls        : 93
Time         : 695.803s (Solving: 661.19s 1st Model: 0.01s Unsat: 10.30s)
CPU Time     : 695.864s

Choices      : 9541488  (Domain: 9418953)
Conflicts    : 717380   (Analyzed: 717376)
Restarts     : 8807     (Average: 81.46 Last: 221)
Model-Level  : 322.0   
Problems     : 93       (Average Length: 90.87 Splits: 0)
Lemmas       : 717376   (Deleted: 670004)
  Binary     : 16807    (Ratio:   2.34%)
  Ternary    : 4354     (Ratio:   0.61%)
  Conflict   : 717376   (Average Length:  459.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 717376   (Average: 11.41 Max: 1538 Sum: 8186779)
  Executed   : 717261   (Average: 11.40 Max: 1538 Sum: 8181497 Ratio:  99.94%)
  Bounded    : 115      (Average: 45.93 Max: 117 Sum:   5282 Ratio:   0.06%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 6205058  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 94
Time         : 699.020s (Solving: 664.24s 1st Model: 0.01s Unsat: 10.30s)
CPU Time     : 699.080s

Choices      : 9590104  (Domain: 9467554)
Conflicts    : 724918   (Analyzed: 724914)
Restarts     : 8907     (Average: 81.39 Last: 221)
Model-Level  : 322.0   
Problems     : 94       (Average Length: 91.15 Splits: 0)
Lemmas       : 724914   (Deleted: 677585)
  Binary     : 16825    (Ratio:   2.32%)
  Ternary    : 4355     (Ratio:   0.60%)
  Conflict   : 724914   (Average Length:  457.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 724914   (Average: 11.34 Max: 1538 Sum: 8223663)
  Executed   : 724799   (Average: 11.34 Max: 1538 Sum: 8218381 Ratio:  99.94%)
  Bounded    : 115      (Average: 45.93 Max: 117 Sum:   5282 Ratio:   0.06%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 6205058  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 3.16s
Memory:		 925MB (+0MB)
UNKNOWN
Iteration Time:	 3.22s

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

Models       : 0+
Calls        : 95
Time         : 703.377s (Solving: 668.43s 1st Model: 0.01s Unsat: 10.30s)
CPU Time     : 703.440s

Choices      : 9642207  (Domain: 9519657)
Conflicts    : 732532   (Analyzed: 732528)
Restarts     : 9007     (Average: 81.33 Last: 221)
Model-Level  : 322.0   
Problems     : 95       (Average Length: 91.42 Splits: 0)
Lemmas       : 732528   (Deleted: 684766)
  Binary     : 16834    (Ratio:   2.30%)
  Ternary    : 4361     (Ratio:   0.60%)
  Conflict   : 732528   (Average Length:  456.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 732528   (Average: 11.28 Max: 1538 Sum: 8261426)
  Executed   : 732413   (Average: 11.27 Max: 1538 Sum: 8256144 Ratio:  99.94%)
  Bounded    : 115      (Average: 45.93 Max: 117 Sum:   5282 Ratio:   0.06%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 6205058  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 4.30s
Memory:		 925MB (+0MB)
UNKNOWN
Iteration Time:	 4.36s

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

Models       : 0+
Calls        : 96
Time         : 709.992s (Solving: 674.87s 1st Model: 0.01s Unsat: 10.30s)
CPU Time     : 710.060s

Choices      : 9743653  (Domain: 9620828)
Conflicts    : 740659   (Analyzed: 740655)
Restarts     : 9107     (Average: 81.33 Last: 221)
Model-Level  : 322.0   
Problems     : 96       (Average Length: 91.69 Splits: 0)
Lemmas       : 740655   (Deleted: 692312)
  Binary     : 16909    (Ratio:   2.28%)
  Ternary    : 4380     (Ratio:   0.59%)
  Conflict   : 740655   (Average Length:  455.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 740655   (Average: 11.27 Max: 1538 Sum: 8347406)
  Executed   : 740540   (Average: 11.26 Max: 1538 Sum: 8342124 Ratio:  99.94%)
  Bounded    : 115      (Average: 45.93 Max: 117 Sum:   5282 Ratio:   0.06%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 6205058  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 97
Time         : 716.237s (Solving: 680.95s 1st Model: 0.01s Unsat: 10.30s)
CPU Time     : 716.304s

Choices      : 9820018  (Domain: 9697193)
Conflicts    : 749142   (Analyzed: 749138)
Restarts     : 9207     (Average: 81.37 Last: 221)
Model-Level  : 322.0   
Problems     : 97       (Average Length: 91.95 Splits: 0)
Lemmas       : 749138   (Deleted: 700495)
  Binary     : 16933    (Ratio:   2.26%)
  Ternary    : 4389     (Ratio:   0.59%)
  Conflict   : 749138   (Average Length:  456.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 749138   (Average: 11.22 Max: 1538 Sum: 8405148)
  Executed   : 749022   (Average: 11.21 Max: 1538 Sum: 8399749 Ratio:  99.94%)
  Bounded    : 116      (Average: 46.54 Max: 117 Sum:   5399 Ratio:   0.06%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 6205058  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 6.19s
Memory:		 925MB (+0MB)
UNKNOWN
Iteration Time:	 6.25s

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

Models       : 0+
Calls        : 98
Time         : 722.767s (Solving: 687.31s 1st Model: 0.01s Unsat: 10.30s)
CPU Time     : 722.836s

Choices      : 9908444  (Domain: 9785569)
Conflicts    : 757333   (Analyzed: 757329)
Restarts     : 9307     (Average: 81.37 Last: 221)
Model-Level  : 322.0   
Problems     : 98       (Average Length: 92.20 Splits: 0)
Lemmas       : 757329   (Deleted: 708761)
  Binary     : 16956    (Ratio:   2.24%)
  Ternary    : 4393     (Ratio:   0.58%)
  Conflict   : 757329   (Average Length:  457.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 757329   (Average: 11.19 Max: 1538 Sum: 8473903)
  Executed   : 757213   (Average: 11.18 Max: 1538 Sum: 8468504 Ratio:  99.94%)
  Bounded    : 116      (Average: 46.54 Max: 117 Sum:   5399 Ratio:   0.06%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 6205044  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 99
Time         : 725.418s (Solving: 689.79s 1st Model: 0.01s Unsat: 10.30s)
CPU Time     : 725.488s

Choices      : 9952489  (Domain: 9829609)
Conflicts    : 764342   (Analyzed: 764338)
Restarts     : 9407     (Average: 81.25 Last: 221)
Model-Level  : 322.0   
Problems     : 99       (Average Length: 92.45 Splits: 0)
Lemmas       : 764338   (Deleted: 716366)
  Binary     : 16959    (Ratio:   2.22%)
  Ternary    : 4394     (Ratio:   0.57%)
  Conflict   : 764338   (Average Length:  454.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 764338   (Average: 11.12 Max: 1538 Sum: 8500749)
  Executed   : 764222   (Average: 11.11 Max: 1538 Sum: 8495350 Ratio:  99.94%)
  Bounded    : 116      (Average: 46.54 Max: 117 Sum:   5399 Ratio:   0.06%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
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  : 6205044  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 2.59s
Memory:		 925MB (+0MB)
UNKNOWN
Iteration Time:	 2.65s

Iteration 99
Queue:		 [(24,120,0,True)]
Grounded Until:	 115
Expected Memory: 1005.0MB
Grounding...	 [('step', [116]), ('step', [117]), ('step', [118]), ('step', [119]), ('step', [120]), ('check', [120])]
Grounding Time:	 0.52s
Memory:		 925MB (+0MB)
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 100
Time         : 731.863s (Solving: 695.02s 1st Model: 0.01s Unsat: 10.30s)
CPU Time     : 731.932s

Choices      : 10010889 (Domain: 9888009)
Conflicts    : 771907   (Analyzed: 771903)
Restarts     : 9507     (Average: 81.19 Last: 221)
Model-Level  : 322.0   
Problems     : 100      (Average Length: 92.75 Splits: 0)
Lemmas       : 771903   (Deleted: 723616)
  Binary     : 16968    (Ratio:   2.20%)
  Ternary    : 4403     (Ratio:   0.57%)
  Conflict   : 771903   (Average Length:  452.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 771903   (Average: 11.05 Max: 1538 Sum: 8529584)
  Executed   : 771787   (Average: 11.04 Max: 1538 Sum: 8524185 Ratio:  99.94%)
  Bounded    : 116      (Average: 46.54 Max: 117 Sum:   5399 Ratio:   0.06%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 881056   (Eliminated:    0 Frozen: 272341)
Constraints  : 6487504  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 5.39s
Memory:		 944MB (+19MB)
UNKNOWN
Iteration Time:	 6.46s

Iteration 100
Queue:		 [(5,25,8,True), (6,30,8,True), (7,35,7,True), (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,2,True), (22,110,2,True), (23,115,2,False), (24,120,1,True)]
Grounded Until:	 120
Blocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 101
Time         : 737.965s (Solving: 700.93s 1st Model: 0.01s Unsat: 10.30s)
CPU Time     : 738.036s

Choices      : 10051075 (Domain: 9928195)
Conflicts    : 779724   (Analyzed: 779720)
Restarts     : 9607     (Average: 81.16 Last: 221)
Model-Level  : 322.0   
Problems     : 101      (Average Length: 93.04 Splits: 0)
Lemmas       : 779720   (Deleted: 731165)
  Binary     : 16978    (Ratio:   2.18%)
  Ternary    : 4419     (Ratio:   0.57%)
  Conflict   : 779720   (Average Length:  454.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 779720   (Average: 10.98 Max: 1538 Sum: 8560304)
  Executed   : 779604   (Average: 10.97 Max: 1538 Sum: 8554905 Ratio:  99.94%)
  Bounded    : 116      (Average: 46.54 Max: 117 Sum:   5399 Ratio:   0.06%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 881056   (Eliminated:    0 Frozen: 272341)
Constraints  : 6487504  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 1047MB
Max. Length  : 120 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 6.03s
Memory:		 949MB (+5MB)
UNKNOWN
Iteration Time:	 6.11s

Iteration 101
Queue:		 [(6,30,8,True), (7,35,7,True), (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,2,True), (22,110,2,True), (23,115,2,False), (24,120,1,True)]
Grounded Until:	 120
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 102
Time         : 745.146s (Solving: 707.91s 1st Model: 0.01s Unsat: 10.30s)
CPU Time     : 745.220s

Choices      : 10105319 (Domain: 9982439)
Conflicts    : 787477   (Analyzed: 787473)
Restarts     : 9707     (Average: 81.12 Last: 221)
Model-Level  : 322.0   
Problems     : 102      (Average Length: 93.32 Splits: 0)
Lemmas       : 787473   (Deleted: 739005)
  Binary     : 17025    (Ratio:   2.16%)
  Ternary    : 4422     (Ratio:   0.56%)
  Conflict   : 787473   (Average Length:  464.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 787473   (Average: 10.91 Max: 1538 Sum: 8595072)
  Executed   : 787357   (Average: 10.91 Max: 1538 Sum: 8589673 Ratio:  99.94%)
  Bounded    : 116      (Average: 46.54 Max: 117 Sum:   5399 Ratio:   0.06%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 881056   (Eliminated:    0 Frozen: 272341)
Constraints  : 6487504  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 1047MB
Max. Length  : 120 steps
Models       : 1

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

Iteration 102
Queue:		 [(7,35,7,True), (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,2,True), (22,110,2,True), (23,115,2,False), (24,120,1,True)]
Grounded Until:	 120
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 103
Time         : 748.690s (Solving: 711.27s 1st Model: 0.01s Unsat: 10.30s)
CPU Time     : 748.764s

Choices      : 10150610 (Domain: 10027730)
Conflicts    : 795069   (Analyzed: 795065)
Restarts     : 9807     (Average: 81.07 Last: 221)
Model-Level  : 322.0   
Problems     : 103      (Average Length: 93.60 Splits: 0)
Lemmas       : 795065   (Deleted: 746406)
  Binary     : 17037    (Ratio:   2.14%)
  Ternary    : 4428     (Ratio:   0.56%)
  Conflict   : 795065   (Average Length:  463.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 795065   (Average: 10.85 Max: 1538 Sum: 8630401)
  Executed   : 794949   (Average: 10.85 Max: 1538 Sum: 8625002 Ratio:  99.94%)
  Bounded    : 116      (Average: 46.54 Max: 117 Sum:   5399 Ratio:   0.06%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 881056   (Eliminated:    0 Frozen: 272341)
Constraints  : 6487504  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 1047MB
Max. Length  : 120 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 3.48s
Memory:		 949MB (+0MB)
UNKNOWN
Iteration Time:	 3.55s

Iteration 103
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,2,True), (22,110,2,True), (23,115,2,False), (24,120,1,True)]
Grounded Until:	 120
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 104
Time         : 756.103s (Solving: 718.51s 1st Model: 0.01s Unsat: 10.30s)
CPU Time     : 756.180s

Choices      : 10212366 (Domain: 10089486)
Conflicts    : 803054   (Analyzed: 803050)
Restarts     : 9907     (Average: 81.06 Last: 221)
Model-Level  : 322.0   
Problems     : 104      (Average Length: 93.88 Splits: 0)
Lemmas       : 803050   (Deleted: 753966)
  Binary     : 17092    (Ratio:   2.13%)
  Ternary    : 4436     (Ratio:   0.55%)
  Conflict   : 803050   (Average Length:  469.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 803050   (Average: 10.80 Max: 1538 Sum: 8671434)
  Executed   : 802934   (Average: 10.79 Max: 1538 Sum: 8666035 Ratio:  99.94%)
  Bounded    : 116      (Average: 46.54 Max: 117 Sum:   5399 Ratio:   0.06%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 881056   (Eliminated:    0 Frozen: 272341)
Constraints  : 6487504  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 1047MB
Max. Length  : 120 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 7.36s
Memory:		 949MB (+0MB)
UNKNOWN
Iteration Time:	 7.42s

Iteration 104
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,2,True), (22,110,2,True), (23,115,2,False), (24,120,1,True)]
Grounded Until:	 120
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 105
Time         : 762.277s (Solving: 724.47s 1st Model: 0.01s Unsat: 10.30s)
CPU Time     : 762.356s

Choices      : 10273202 (Domain: 10150317)
Conflicts    : 811285   (Analyzed: 811281)
Restarts     : 10007    (Average: 81.07 Last: 221)
Model-Level  : 322.0   
Problems     : 105      (Average Length: 94.14 Splits: 0)
Lemmas       : 811281   (Deleted: 761685)
  Binary     : 17120    (Ratio:   2.11%)
  Ternary    : 4448     (Ratio:   0.55%)
  Conflict   : 811281   (Average Length:  471.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 811281   (Average: 10.75 Max: 1538 Sum: 8718383)
  Executed   : 811165   (Average: 10.74 Max: 1538 Sum: 8712984 Ratio:  99.94%)
  Bounded    : 116      (Average: 46.54 Max: 117 Sum:   5399 Ratio:   0.06%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 881056   (Eliminated:    0 Frozen: 272341)
Constraints  : 6487504  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 1047MB
Max. Length  : 120 steps
Models       : 1

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

Iteration 105
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,2,True), (22,110,2,True), (23,115,2,False), (24,120,1,True)]
Grounded Until:	 120
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 106
Time         : 766.222s (Solving: 728.21s 1st Model: 0.01s Unsat: 10.30s)
CPU Time     : 766.304s

Choices      : 10323793 (Domain: 10200773)
Conflicts    : 818935   (Analyzed: 818931)
Restarts     : 10107    (Average: 81.03 Last: 221)
Model-Level  : 322.0   
Problems     : 106      (Average Length: 94.41 Splits: 0)
Lemmas       : 818931   (Deleted: 769636)
  Binary     : 17131    (Ratio:   2.09%)
  Ternary    : 4449     (Ratio:   0.54%)
  Conflict   : 818931   (Average Length:  471.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 818931   (Average: 10.69 Max: 1538 Sum: 8756694)
  Executed   : 818815   (Average: 10.69 Max: 1538 Sum: 8751295 Ratio:  99.94%)
  Bounded    : 116      (Average: 46.54 Max: 117 Sum:   5399 Ratio:   0.06%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 881056   (Eliminated:    0 Frozen: 272341)
Constraints  : 6487504  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 1047MB
Max. Length  : 120 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 3.86s
Memory:		 949MB (+0MB)
UNKNOWN
Iteration Time:	 3.95s

Iteration 106
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,2,True), (22,110,2,True), (23,115,2,False), (24,120,1,True)]
Grounded Until:	 120
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 107
Time         : 773.854s (Solving: 735.64s 1st Model: 0.01s Unsat: 10.30s)
CPU Time     : 773.940s

Choices      : 10428477 (Domain: 10305428)
Conflicts    : 827604   (Analyzed: 827600)
Restarts     : 10207    (Average: 81.08 Last: 221)
Model-Level  : 322.0   
Problems     : 107      (Average Length: 94.66 Splits: 0)
Lemmas       : 827600   (Deleted: 778734)
  Binary     : 17196    (Ratio:   2.08%)
  Ternary    : 4460     (Ratio:   0.54%)
  Conflict   : 827600   (Average Length:  471.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 827600   (Average: 10.69 Max: 1538 Sum: 8844605)
  Executed   : 827484   (Average: 10.68 Max: 1538 Sum: 8839206 Ratio:  99.94%)
  Bounded    : 116      (Average: 46.54 Max: 117 Sum:   5399 Ratio:   0.06%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 881056   (Eliminated:    0 Frozen: 272341)
Constraints  : 6487504  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 1047MB
Max. Length  : 120 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 7.56s
Memory:		 949MB (+0MB)
UNKNOWN
Iteration Time:	 7.64s

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

Models       : 0+
Calls        : 108
Time         : 780.242s (Solving: 741.85s 1st Model: 0.01s Unsat: 10.30s)
CPU Time     : 780.328s

Choices      : 10520611 (Domain: 10397542)
Conflicts    : 835829   (Analyzed: 835825)
Restarts     : 10307    (Average: 81.09 Last: 221)
Model-Level  : 322.0   
Problems     : 108      (Average Length: 94.92 Splits: 0)
Lemmas       : 835825   (Deleted: 785714)
  Binary     : 17226    (Ratio:   2.06%)
  Ternary    : 4468     (Ratio:   0.53%)
  Conflict   : 835825   (Average Length:  473.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 835825   (Average: 10.67 Max: 1538 Sum: 8915957)
  Executed   : 835709   (Average: 10.66 Max: 1538 Sum: 8910558 Ratio:  99.94%)
  Bounded    : 116      (Average: 46.54 Max: 117 Sum:   5399 Ratio:   0.06%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 881056   (Eliminated:    0 Frozen: 272341)
Constraints  : 6487504  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 1047MB
Max. Length  : 120 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 6.33s
Memory:		 949MB (+0MB)
UNKNOWN
Iteration Time:	 6.39s

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

Models       : 0+
Calls        : 109
Time         : 793.031s (Solving: 754.47s 1st Model: 0.01s Unsat: 10.30s)
CPU Time     : 793.124s

Choices      : 10704330 (Domain: 10581217)
Conflicts    : 844461   (Analyzed: 844457)
Restarts     : 10407    (Average: 81.14 Last: 221)
Model-Level  : 322.0   
Problems     : 109      (Average Length: 95.17 Splits: 0)
Lemmas       : 844457   (Deleted: 795753)
  Binary     : 17337    (Ratio:   2.05%)
  Ternary    : 4484     (Ratio:   0.53%)
  Conflict   : 844457   (Average Length:  480.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 844457   (Average: 10.73 Max: 1538 Sum: 9061922)
  Executed   : 844341   (Average: 10.72 Max: 1538 Sum: 9056523 Ratio:  99.94%)
  Bounded    : 116      (Average: 46.54 Max: 117 Sum:   5399 Ratio:   0.06%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 881056   (Eliminated:    0 Frozen: 272341)
Constraints  : 6487504  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 1047MB
Max. Length  : 120 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 12.73s
Memory:		 949MB (+0MB)
UNKNOWN
Iteration Time:	 12.80s

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

Models       : 0+
Calls        : 110
Time         : 802.026s (Solving: 763.29s 1st Model: 0.01s Unsat: 10.30s)
CPU Time     : 802.124s

Choices      : 10861081 (Domain: 10737680)
Conflicts    : 853263   (Analyzed: 853259)
Restarts     : 10507    (Average: 81.21 Last: 221)
Model-Level  : 322.0   
Problems     : 110      (Average Length: 95.41 Splits: 0)
Lemmas       : 853259   (Deleted: 803692)
  Binary     : 17382    (Ratio:   2.04%)
  Ternary    : 4494     (Ratio:   0.53%)
  Conflict   : 853259   (Average Length:  480.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 853259   (Average: 10.78 Max: 1538 Sum: 9194436)
  Executed   : 853142   (Average: 10.77 Max: 1538 Sum: 9188915 Ratio:  99.94%)
  Bounded    : 117      (Average: 47.19 Max: 122 Sum:   5521 Ratio:   0.06%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 881056   (Eliminated:    0 Frozen: 272341)
Constraints  : 6487504  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 1047MB
Max. Length  : 120 steps
Models       : 1

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

Iteration 110
Queue:		 [(24,120,1,True)]
Grounded Until:	 120
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 111
Time         : 813.945s (Solving: 775.03s 1st Model: 0.01s Unsat: 10.30s)
CPU Time     : 814.052s

Choices      : 10976728 (Domain: 10853305)
Conflicts    : 861413   (Analyzed: 861409)
Restarts     : 10607    (Average: 81.21 Last: 221)
Model-Level  : 322.0   
Problems     : 111      (Average Length: 95.65 Splits: 0)
Lemmas       : 861409   (Deleted: 810720)
  Binary     : 17438    (Ratio:   2.02%)
  Ternary    : 4500     (Ratio:   0.52%)
  Conflict   : 861409   (Average Length:  491.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 861409   (Average: 10.77 Max: 1538 Sum: 9273194)
  Executed   : 861292   (Average: 10.76 Max: 1538 Sum: 9267673 Ratio:  99.94%)
  Bounded    : 117      (Average: 47.19 Max: 122 Sum:   5521 Ratio:   0.06%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 881056   (Eliminated:    0 Frozen: 272341)
Constraints  : 6487490  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 1047MB
Max. Length  : 120 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 11.87s
Memory:		 949MB (+0MB)
UNKNOWN
Iteration Time:	 11.93s

Iteration 111
Queue:		 [(5,25,9,True), (6,30,9,True), (7,35,8,True), (8,40,8,False), (9,45,7,True), (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,True), (24,120,2,False)]
Grounded Until:	 120
Blocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 112
Time         : 820.045s (Solving: 780.93s 1st Model: 0.01s Unsat: 10.30s)
CPU Time     : 820.156s

Choices      : 11030169 (Domain: 10906746)
Conflicts    : 869423   (Analyzed: 869419)
Restarts     : 10707    (Average: 81.20 Last: 221)
Model-Level  : 322.0   
Problems     : 112      (Average Length: 95.88 Splits: 0)
Lemmas       : 869419   (Deleted: 818458)
  Binary     : 17529    (Ratio:   2.02%)
  Ternary    : 4511     (Ratio:   0.52%)
  Conflict   : 869419   (Average Length:  490.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 869419   (Average: 10.72 Max: 1538 Sum: 9316138)
  Executed   : 869302   (Average: 10.71 Max: 1538 Sum: 9310617 Ratio:  99.94%)
  Bounded    : 117      (Average: 47.19 Max: 122 Sum:   5521 Ratio:   0.06%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 881056   (Eliminated:    0 Frozen: 272341)
Constraints  : 6487490  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 1047MB
Max. Length  : 120 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 6.02s
Memory:		 949MB (+0MB)
UNKNOWN
Iteration Time:	 6.10s

Iteration 112
Queue:		 [(6,30,9,True), (7,35,8,True), (8,40,8,False), (9,45,7,True), (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,True), (24,120,2,False)]
Grounded Until:	 120
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 113
Time         : 824.960s (Solving: 785.67s 1st Model: 0.01s Unsat: 10.30s)
CPU Time     : 825.076s

Choices      : 11079192 (Domain: 10955769)
Conflicts    : 877363   (Analyzed: 877359)
Restarts     : 10807    (Average: 81.18 Last: 221)
Model-Level  : 322.0   
Problems     : 113      (Average Length: 96.12 Splits: 0)
Lemmas       : 877359   (Deleted: 826158)
  Binary     : 17584    (Ratio:   2.00%)
  Ternary    : 4519     (Ratio:   0.52%)
  Conflict   : 877359   (Average Length:  489.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 877359   (Average: 10.66 Max: 1538 Sum: 9353248)
  Executed   : 877242   (Average: 10.65 Max: 1538 Sum: 9347727 Ratio:  99.94%)
  Bounded    : 117      (Average: 47.19 Max: 122 Sum:   5521 Ratio:   0.06%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 881056   (Eliminated:    0 Frozen: 272341)
Constraints  : 6487490  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 1047MB
Max. Length  : 120 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 4.86s
Memory:		 949MB (+0MB)
UNKNOWN
Iteration Time:	 4.92s

Iteration 113
Queue:		 [(7,35,8,True), (8,40,8,False), (9,45,7,True), (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,True), (24,120,2,False)]
Grounded Until:	 120
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 114
Time         : 831.447s (Solving: 791.98s 1st Model: 0.01s Unsat: 10.30s)
CPU Time     : 831.568s

Choices      : 11130361 (Domain: 11006938)
Conflicts    : 885481   (Analyzed: 885477)
Restarts     : 10907    (Average: 81.18 Last: 221)
Model-Level  : 322.0   
Problems     : 114      (Average Length: 96.34 Splits: 0)
Lemmas       : 885477   (Deleted: 834224)
  Binary     : 17608    (Ratio:   1.99%)
  Ternary    : 4520     (Ratio:   0.51%)
  Conflict   : 885477   (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    : 885477   (Average: 10.60 Max: 1538 Sum: 9385775)
  Executed   : 885360   (Average: 10.59 Max: 1538 Sum: 9380254 Ratio:  99.94%)
  Bounded    : 117      (Average: 47.19 Max: 122 Sum:   5521 Ratio:   0.06%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 881056   (Eliminated:    0 Frozen: 272341)
Constraints  : 6487490  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 1047MB
Max. Length  : 120 steps
Models       : 1

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

Iteration 114
Queue:		 [(9,45,7,True), (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,True), (24,120,2,False)]
Grounded Until:	 120
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 115
Time         : 839.361s (Solving: 799.70s 1st Model: 0.01s Unsat: 10.30s)
CPU Time     : 839.488s

Choices      : 11208399 (Domain: 11084930)
Conflicts    : 893575   (Analyzed: 893571)
Restarts     : 11007    (Average: 81.18 Last: 221)
Model-Level  : 322.0   
Problems     : 115      (Average Length: 96.57 Splits: 0)
Lemmas       : 893571   (Deleted: 842209)
  Binary     : 17686    (Ratio:   1.98%)
  Ternary    : 4530     (Ratio:   0.51%)
  Conflict   : 893571   (Average Length:  495.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 893571   (Average: 10.57 Max: 1538 Sum: 9446740)
  Executed   : 893454   (Average: 10.57 Max: 1538 Sum: 9441219 Ratio:  99.94%)
  Bounded    : 117      (Average: 47.19 Max: 122 Sum:   5521 Ratio:   0.06%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 881056   (Eliminated:    0 Frozen: 272341)
Constraints  : 6487490  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 1047MB
Max. Length  : 120 steps
Models       : 1

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

Iteration 115
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,True), (24,120,2,False)]
Grounded Until:	 120
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 116
Time         : 848.137s (Solving: 808.29s 1st Model: 0.01s Unsat: 10.30s)
CPU Time     : 848.260s

Choices      : 11277849 (Domain: 11154379)
Conflicts    : 902238   (Analyzed: 902234)
Restarts     : 11107    (Average: 81.23 Last: 221)
Model-Level  : 322.0   
Problems     : 116      (Average Length: 96.78 Splits: 0)
Lemmas       : 902234   (Deleted: 852115)
  Binary     : 17717    (Ratio:   1.96%)
  Ternary    : 4534     (Ratio:   0.50%)
  Conflict   : 902234   (Average Length:  504.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 902234   (Average: 10.52 Max: 1538 Sum: 9491547)
  Executed   : 902117   (Average: 10.51 Max: 1538 Sum: 9486026 Ratio:  99.94%)
  Bounded    : 117      (Average: 47.19 Max: 122 Sum:   5521 Ratio:   0.06%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 881056   (Eliminated:    0 Frozen: 272341)
Constraints  : 6487490  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 1047MB
Max. Length  : 120 steps
Models       : 1

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

Iteration 116
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,True), (24,120,2,False)]
Grounded Until:	 120
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 117
Time         : 852.151s (Solving: 812.09s 1st Model: 0.01s Unsat: 10.30s)
CPU Time     : 852.272s

Choices      : 11327814 (Domain: 11204344)
Conflicts    : 909713   (Analyzed: 909709)
Restarts     : 11207    (Average: 81.17 Last: 221)
Model-Level  : 322.0   
Problems     : 117      (Average Length: 97.00 Splits: 0)
Lemmas       : 909709   (Deleted: 858039)
  Binary     : 17729    (Ratio:   1.95%)
  Ternary    : 4537     (Ratio:   0.50%)
  Conflict   : 909709   (Average Length:  503.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 909709   (Average: 10.47 Max: 1538 Sum: 9529127)
  Executed   : 909591   (Average: 10.47 Max: 1538 Sum: 9523487 Ratio:  99.94%)
  Bounded    : 118      (Average: 47.80 Max: 122 Sum:   5640 Ratio:   0.06%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 881056   (Eliminated:    0 Frozen: 272341)
Constraints  : 6487490  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 1047MB
Max. Length  : 120 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 3.93s
Memory:		 949MB (+0MB)
UNKNOWN
Iteration Time:	 4.01s

Iteration 117
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,True), (24,120,2,False)]
Grounded Until:	 120
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 118
Time         : 860.243s (Solving: 819.99s 1st Model: 0.01s Unsat: 10.30s)
CPU Time     : 860.368s

Choices      : 11431765 (Domain: 11308281)
Conflicts    : 918443   (Analyzed: 918439)
Restarts     : 11307    (Average: 81.23 Last: 221)
Model-Level  : 322.0   
Problems     : 118      (Average Length: 97.21 Splits: 0)
Lemmas       : 918439   (Deleted: 867723)
  Binary     : 17771    (Ratio:   1.93%)
  Ternary    : 4551     (Ratio:   0.50%)
  Conflict   : 918439   (Average Length:  505.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 918439   (Average: 10.47 Max: 1538 Sum: 9612291)
  Executed   : 918321   (Average: 10.46 Max: 1538 Sum: 9606651 Ratio:  99.94%)
  Bounded    : 118      (Average: 47.80 Max: 122 Sum:   5640 Ratio:   0.06%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 881056   (Eliminated:    0 Frozen: 272341)
Constraints  : 6487490  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 1047MB
Max. Length  : 120 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 8.02s
Memory:		 949MB (+0MB)
UNKNOWN
Iteration Time:	 8.10s

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

Models       : 0+
Calls        : 119
Time         : 869.207s (Solving: 828.74s 1st Model: 0.01s Unsat: 10.30s)
CPU Time     : 869.336s

Choices      : 11545052 (Domain: 11421378)
Conflicts    : 927564   (Analyzed: 927560)
Restarts     : 11407    (Average: 81.31 Last: 221)
Model-Level  : 322.0   
Problems     : 119      (Average Length: 97.42 Splits: 0)
Lemmas       : 927560   (Deleted: 876211)
  Binary     : 17827    (Ratio:   1.92%)
  Ternary    : 4558     (Ratio:   0.49%)
  Conflict   : 927560   (Average Length:  508.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 927560   (Average: 10.46 Max: 1538 Sum: 9703473)
  Executed   : 927442   (Average: 10.46 Max: 1538 Sum: 9697833 Ratio:  99.94%)
  Bounded    : 118      (Average: 47.80 Max: 122 Sum:   5640 Ratio:   0.06%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 881056   (Eliminated:    0 Frozen: 272341)
Constraints  : 6487490  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 1047MB
Max. Length  : 120 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 8.88s
Memory:		 949MB (+0MB)
UNKNOWN
Iteration Time:	 8.97s

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

Models       : 0+
Calls        : 120
Time         : 878.093s (Solving: 837.41s 1st Model: 0.01s Unsat: 10.30s)
CPU Time     : 878.224s

Choices      : 11664488 (Domain: 11540813)
Conflicts    : 936261   (Analyzed: 936257)
Restarts     : 11507    (Average: 81.36 Last: 221)
Model-Level  : 322.0   
Problems     : 120      (Average Length: 97.62 Splits: 0)
Lemmas       : 936257   (Deleted: 885314)
  Binary     : 17878    (Ratio:   1.91%)
  Ternary    : 4563     (Ratio:   0.49%)
  Conflict   : 936257   (Average Length:  513.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 936257   (Average: 10.46 Max: 1538 Sum: 9789979)
  Executed   : 936139   (Average: 10.45 Max: 1538 Sum: 9784339 Ratio:  99.94%)
  Bounded    : 118      (Average: 47.80 Max: 122 Sum:   5640 Ratio:   0.06%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 881056   (Eliminated:    0 Frozen: 272341)
Constraints  : 6487490  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 1047MB
Max. Length  : 120 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 8.81s
Memory:		 949MB (+0MB)
UNKNOWN
Iteration Time:	 8.89s

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

Models       : 0+
Calls        : 121
Time         : 881.883s (Solving: 841.02s 1st Model: 0.01s Unsat: 10.30s)
CPU Time     : 882.016s

Choices      : 11703498 (Domain: 11579823)
Conflicts    : 943883   (Analyzed: 943879)
Restarts     : 11607    (Average: 81.32 Last: 221)
Model-Level  : 322.0   
Problems     : 121      (Average Length: 97.83 Splits: 0)
Lemmas       : 943879   (Deleted: 891106)
  Binary     : 17896    (Ratio:   1.90%)
  Ternary    : 4569     (Ratio:   0.48%)
  Conflict   : 943879   (Average Length:  511.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 943879   (Average: 10.40 Max: 1538 Sum: 9819477)
  Executed   : 943761   (Average: 10.40 Max: 1538 Sum: 9813837 Ratio:  99.94%)
  Bounded    : 118      (Average: 47.80 Max: 122 Sum:   5640 Ratio:   0.06%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 881056   (Eliminated:    0 Frozen: 272341)
Constraints  : 6487490  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 1047MB
Max. Length  : 120 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 3.73s
Memory:		 949MB (+0MB)
UNKNOWN
Iteration Time:	 3.79s

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

Models       : 0+
Calls        : 122
Time         : 887.458s (Solving: 846.42s 1st Model: 0.01s Unsat: 10.30s)
CPU Time     : 887.596s

Choices      : 11752054 (Domain: 11628379)
Conflicts    : 951606   (Analyzed: 951602)
Restarts     : 11707    (Average: 81.28 Last: 221)
Model-Level  : 322.0   
Problems     : 122      (Average Length: 98.02 Splits: 0)
Lemmas       : 951602   (Deleted: 899370)
  Binary     : 17915    (Ratio:   1.88%)
  Ternary    : 4571     (Ratio:   0.48%)
  Conflict   : 951602   (Average Length:  515.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 951602   (Average: 10.35 Max: 1538 Sum: 9851821)
  Executed   : 951484   (Average: 10.35 Max: 1538 Sum: 9846181 Ratio:  99.94%)
  Bounded    : 118      (Average: 47.80 Max: 122 Sum:   5640 Ratio:   0.06%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 881056   (Eliminated:    0 Frozen: 272341)
Constraints  : 6487490  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 1047MB
Max. Length  : 120 steps
Models       : 1

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

Iteration 122
Queue:		 [(7,35,9,True), (8,40,8,True), (9,45,8,False), (10,50,7,False), (11,55,6,True), (12,60,6,False), (13,65,5,True), (14,70,5,False), (15,75,4,True), (16,80,4,False), (17,85,4,False), (18,90,4,False), (19,95,3,True), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,3,False), (24,120,2,False)]
Grounded Until:	 120
Unblocking actions...
Solving...
*** Info : (planner): INTERRUPTED by signal!
UNKNOWN

INTERRUPTED  : 1

Models       : 0+
Calls        : 123
Time         : 896.026s (Solving: 854.81s 1st Model: 0.01s Unsat: 10.30s)
CPU Time     : 896.136s

Choices      : 11821970 (Domain: 11698295)
Conflicts    : 960010   (Analyzed: 960006)
Restarts     : 11807    (Average: 81.31 Last: 221)
Model-Level  : 322.0   
Problems     : 123      (Average Length: 98.22 Splits: 0)
Lemmas       : 960006   (Deleted: 906930)
  Binary     : 17953    (Ratio:   1.87%)
  Ternary    : 4581     (Ratio:   0.48%)
  Conflict   : 960006   (Average Length:  522.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 960006   (Average: 10.31 Max: 1538 Sum: 9898064)
  Executed   : 959888   (Average: 10.30 Max: 1538 Sum: 9892424 Ratio:  99.94%)
  Bounded    : 118      (Average: 47.80 Max: 122 Sum:   5640 Ratio:   0.06%)

Rules        : 150277   (Original: 135812)
Atoms        : 72359   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 881056   (Eliminated:    0 Frozen: 272341)
Constraints  : 6487490  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 1047MB
Max. Length  : 120 steps
Models       : 1


