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-12.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-12.pddl
Parsing...
Parsing: [0.030s CPU, 0.033s wall-clock]
Normalizing task... [0.010s CPU, 0.003s wall-clock]
Instantiating...
Generating Datalog program... [0.010s CPU, 0.009s wall-clock]
Normalizing Datalog program...
Normalizing Datalog program: [0.040s CPU, 0.043s wall-clock]
Preparing model... [0.030s CPU, 0.025s wall-clock]
Generated 115 rules.
Computing model... [0.450s CPU, 0.452s wall-clock]
2784 relevant atoms
2893 auxiliary atoms
5677 final queue length
9793 total queue pushes
Completing instantiation... [0.880s CPU, 0.875s wall-clock]
Instantiating: [1.410s CPU, 1.411s wall-clock]
Computing fact groups...
Finding invariants...
24 initial candidates
Finding invariants: [0.110s CPU, 0.110s wall-clock]
Checking invariant weight... [0.000s CPU, 0.001s wall-clock]
Instantiating groups... [0.010s CPU, 0.008s wall-clock]
Collecting mutex groups... [0.000s CPU, 0.001s wall-clock]
Choosing groups...
292 uncovered facts
Choosing groups: [0.010s CPU, 0.002s wall-clock]
Building translation key... [0.000s CPU, 0.011s wall-clock]
Computing fact groups: [0.150s CPU, 0.153s wall-clock]
Building STRIPS to SAS dictionary... [0.010s CPU, 0.003s wall-clock]
Building dictionary for full mutex groups... [0.010s CPU, 0.006s wall-clock]
Building mutex information...
Building mutex information: [0.000s CPU, 0.003s wall-clock]
Translating task...
Processing axioms...
Simplifying axioms... [0.000s CPU, 0.000s wall-clock]
Processing axioms: [0.040s CPU, 0.048s wall-clock]
Translating task: [0.910s CPU, 0.909s wall-clock]
3276 effect conditions simplified
0 implied preconditions added
Detecting unreachable propositions...
0 operators removed
0 axioms removed
3 propositions removed
Detecting unreachable propositions: [0.430s CPU, 0.439s wall-clock]
Reordering and filtering variables...
295 of 295 variables necessary.
14 of 17 mutex groups necessary.
1958 of 1958 operators necessary.
0 of 0 axiom rules necessary.
Reordering and filtering variables: [0.310s CPU, 0.306s wall-clock]
Translator variables: 295
Translator derived variables: 0
Translator facts: 617
Translator goal facts: 12
Translator mutex groups: 14
Translator total mutex groups size: 42
Translator operators: 1958
Translator axioms: 0
Translator task size: 18764
Translator peak memory: 47052 KB
Writing output... [0.390s CPU, 0.403s wall-clock]
Done! [3.690s CPU, 3.705s wall-clock]
planner.py version 0.0.1

Time:	 0.75s
Memory: 101MB

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

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        : 54149   
Atoms        : 54149   
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  : 237MB
Max. Length  : 0 steps
Models       : 0

[endof: stats after solve call]
Solving Time:	 0.00s
Memory:		 173MB (+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: 173MB
Grounding...	 [('step', [1]), ('step', [2]), ('step', [3]), ('step', [4]), ('step', [5]), ('check', [5])]
Grounding Time:	 0.23s
Memory:		 173MB (+0MB)
Unblocking actions...
Solving...
[start: stats after solve call]

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

Choices      : 87       (Domain: 78)
Conflicts    : 32       (Analyzed: 31)
Restarts     : 0       
Problems     : 2        (Average Length: 4.50 Splits: 0)
Lemmas       : 31       (Deleted: 0)
  Binary     : 9        (Ratio:  29.03%)
  Ternary    : 1        (Ratio:   3.23%)
  Conflict   : 31       (Average Length:    6.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 31       (Average:  2.84 Max:  24 Sum:     88)
  Executed   : 30       (Average:  2.81 Max:  24 Sum:     87 Ratio:  98.86%)
  Bounded    : 1        (Average:  1.00 Max:   1 Sum:      1 Ratio:   1.14%)

Rules        : 54149   
Atoms        : 54149   
Bodies       : 1        (Original: 0)
Tight        : Yes
Variables    : 14506    (Eliminated:    0 Frozen:  150)
Constraints  : 48947    (Binary:  95.2% Ternary:   3.3% Other:   1.4%)

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

[endof: stats after solve call]
Solving Time:	 0.02s
Memory:		 176MB (+3MB)
UNSAT
Iteration Time:	 0.36s

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: 179.0MB
Grounding...	 [('step', [6]), ('step', [7]), ('step', [8]), ('step', [9]), ('step', [10]), ('check', [10])]
Grounding Time:	 0.28s
Memory:		 183MB (+7MB)
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 1+
Calls        : 3
Time         : 1.653s (Solving: 0.01s 1st Model: 0.01s Unsat: 0.00s)
CPU Time     : 1.536s

Choices      : 939      (Domain: 865)
Conflicts    : 86       (Analyzed: 85)
Restarts     : 0       
Model-Level  : 291.0   
Problems     : 3        (Average Length: 7.00 Splits: 0)
Lemmas       : 85       (Deleted: 0)
  Binary     : 15       (Ratio:  17.65%)
  Ternary    : 3        (Ratio:   3.53%)
  Conflict   : 85       (Average Length:   27.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 85       (Average:  7.78 Max: 112 Sum:    661)
  Executed   : 84       (Average:  7.76 Max: 112 Sum:    660 Ratio:  99.85%)
  Bounded    : 1        (Average:  1.00 Max:   1 Sum:      1 Ratio:   0.15%)

Rules        : 54149   
Atoms        : 54149   
Bodies       : 1        (Original: 0)
Tight        : Yes
Variables    : 31792    (Eliminated:    0 Frozen:  300)
Constraints  : 190267   (Binary:  95.6% Ternary:   3.2% Other:   1.2%)

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

[endof: stats after solve call]
Solving Time:	 0.03s
Memory:		 190MB (+7MB)
SAT
Testing...
NOT SERIALIZABLE
Testing Time:	 0.89s
Memory:		 221MB (+31MB)
Solving...
[start: stats after solve call]

Models       : 0
Calls        : 4
Time         : 2.571s (Solving: 0.64s 1st Model: 0.01s Unsat: 0.63s)
CPU Time     : 2.456s

Choices      : 25297    (Domain: 14285)
Conflicts    : 2976     (Analyzed: 2974)
Restarts     : 34       (Average: 87.47 Last: 54)
Model-Level  : 291.0   
Problems     : 4        (Average Length: 8.25 Splits: 0)
Lemmas       : 2974     (Deleted: 800)
  Binary     : 295      (Ratio:   9.92%)
  Ternary    : 122      (Ratio:   4.10%)
  Conflict   : 2974     (Average Length:   97.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 2974     (Average:  8.19 Max: 172 Sum:  24361)
  Executed   : 2963     (Average:  8.15 Max: 172 Sum:  24251 Ratio:  99.55%)
  Bounded    : 11       (Average: 10.00 Max:  12 Sum:    110 Ratio:   0.45%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 49760    (Eliminated:    0 Frozen: 14250)
Constraints  : 309236   (Binary:  91.5% Ternary:   6.8% Other:   1.7%)

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

[endof: stats after solve call]
Solving Time:	 0.70s
Memory:		 221MB (+0MB)
UNSAT
Iteration Time:	 2.02s

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

Models       : 0+
Calls        : 5
Time         : 7.270s (Solving: 4.65s 1st Model: 0.01s Unsat: 0.63s)
CPU Time     : 7.156s

Choices      : 106976   (Domain: 74498)
Conflicts    : 12217    (Analyzed: 12215)
Restarts     : 134      (Average: 91.16 Last: 70)
Model-Level  : 291.0   
Problems     : 5        (Average Length: 10.00 Splits: 0)
Lemmas       : 12215    (Deleted: 7986)
  Binary     : 1029     (Ratio:   8.42%)
  Ternary    : 285      (Ratio:   2.33%)
  Conflict   : 12215    (Average Length:  435.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 12215    (Average:  8.42 Max: 199 Sum: 102796)
  Executed   : 12200    (Average:  8.40 Max: 199 Sum: 102618 Ratio:  99.83%)
  Bounded    : 15       (Average: 11.87 Max:  17 Sum:    178 Ratio:   0.17%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 82706    (Eliminated:    0 Frozen: 24685)
Constraints  : 541641   (Binary:  91.5% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 4.04s
Memory:		 243MB (+22MB)
UNKNOWN
Iteration Time:	 4.71s

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

Models       : 0+
Calls        : 6
Time         : 12.913s (Solving: 9.57s 1st Model: 0.01s Unsat: 0.63s)
CPU Time     : 12.800s

Choices      : 195524   (Domain: 147967)
Conflicts    : 21645    (Analyzed: 21643)
Restarts     : 234      (Average: 92.49 Last: 125)
Model-Level  : 291.0   
Problems     : 6        (Average Length: 12.00 Splits: 0)
Lemmas       : 21643    (Deleted: 16420)
  Binary     : 1398     (Ratio:   6.46%)
  Ternary    : 353      (Ratio:   1.63%)
  Conflict   : 21643    (Average Length:  600.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 21643    (Average:  8.52 Max: 214 Sum: 184314)
  Executed   : 21628    (Average:  8.51 Max: 214 Sum: 184136 Ratio:  99.90%)
  Bounded    : 15       (Average: 11.87 Max:  17 Sum:    178 Ratio:   0.10%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 115652   (Eliminated:    0 Frozen: 35120)
Constraints  : 788581   (Binary:  91.4% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 4.95s
Memory:		 260MB (+14MB)
UNKNOWN
Iteration Time:	 5.65s

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

Models       : 0+
Calls        : 7
Time         : 18.458s (Solving: 14.29s 1st Model: 0.01s Unsat: 0.63s)
CPU Time     : 18.348s

Choices      : 282830   (Domain: 225231)
Conflicts    : 30138    (Analyzed: 30136)
Restarts     : 334      (Average: 90.23 Last: 125)
Model-Level  : 291.0   
Problems     : 7        (Average Length: 14.14 Splits: 0)
Lemmas       : 30136    (Deleted: 23186)
  Binary     : 1616     (Ratio:   5.36%)
  Ternary    : 384      (Ratio:   1.27%)
  Conflict   : 30136    (Average Length:  711.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 30136    (Average:  8.65 Max: 219 Sum: 260819)
  Executed   : 30121    (Average:  8.65 Max: 219 Sum: 260641 Ratio:  99.93%)
  Bounded    : 15       (Average: 11.87 Max:  17 Sum:    178 Ratio:   0.07%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 148598   (Eliminated:    0 Frozen: 45555)
Constraints  : 1038166  (Binary:  91.4% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 4.77s
Memory:		 288MB (+11MB)
UNKNOWN
Iteration Time:	 5.56s

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

Models       : 0+
Calls        : 8
Time         : 24.625s (Solving: 19.73s 1st Model: 0.01s Unsat: 0.63s)
CPU Time     : 24.516s

Choices      : 391741   (Domain: 324130)
Conflicts    : 39030    (Analyzed: 39028)
Restarts     : 434      (Average: 89.93 Last: 125)
Model-Level  : 291.0   
Problems     : 8        (Average Length: 16.38 Splits: 0)
Lemmas       : 39028    (Deleted: 33446)
  Binary     : 1784     (Ratio:   4.57%)
  Ternary    : 403      (Ratio:   1.03%)
  Conflict   : 39028    (Average Length:  821.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 39028    (Average:  9.13 Max: 298 Sum: 356392)
  Executed   : 39013    (Average:  9.13 Max: 298 Sum: 356214 Ratio:  99.95%)
  Bounded    : 15       (Average: 11.87 Max:  17 Sum:    178 Ratio:   0.05%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 181544   (Eliminated:    0 Frozen: 55990)
Constraints  : 1287751  (Binary:  91.4% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 5.50s
Memory:		 324MB (+24MB)
UNKNOWN
Iteration Time:	 6.18s

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         : 28.500s (Solving: 23.56s 1st Model: 0.01s Unsat: 0.63s)
CPU Time     : 28.392s

Choices      : 458584   (Domain: 380067)
Conflicts    : 47909    (Analyzed: 47907)
Restarts     : 534      (Average: 89.71 Last: 125)
Model-Level  : 291.0   
Problems     : 9        (Average Length: 18.11 Splits: 0)
Lemmas       : 47907    (Deleted: 41564)
  Binary     : 2191     (Ratio:   4.57%)
  Ternary    : 506      (Ratio:   1.06%)
  Conflict   : 47907    (Average Length:  703.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 47907    (Average:  8.75 Max: 298 Sum: 419268)
  Executed   : 47879    (Average:  8.74 Max: 298 Sum: 418679 Ratio:  99.86%)
  Bounded    : 28       (Average: 21.04 Max:  32 Sum:    589 Ratio:   0.14%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 181544   (Eliminated:    0 Frozen: 55990)
Constraints  : 1287751  (Binary:  91.4% Ternary:   6.8% Other:   1.8%)

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

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

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         : 34.309s (Solving: 29.31s 1st Model: 0.01s Unsat: 0.63s)
CPU Time     : 34.204s

Choices      : 602790   (Domain: 514674)
Conflicts    : 57025    (Analyzed: 57023)
Restarts     : 634      (Average: 89.94 Last: 125)
Model-Level  : 291.0   
Problems     : 10       (Average Length: 19.50 Splits: 0)
Lemmas       : 57023    (Deleted: 48408)
  Binary     : 2861     (Ratio:   5.02%)
  Ternary    : 726      (Ratio:   1.27%)
  Conflict   : 57023    (Average Length:  619.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 57023    (Average:  9.82 Max: 298 Sum: 560074)
  Executed   : 56980    (Average:  9.80 Max: 298 Sum: 559005 Ratio:  99.81%)
  Bounded    : 43       (Average: 24.86 Max:  32 Sum:   1069 Ratio:   0.19%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 181544   (Eliminated:    0 Frozen: 55990)
Constraints  : 1263328  (Binary:  91.4% Ternary:   6.8% Other:   1.8%)

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

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

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         : 40.368s (Solving: 35.32s 1st Model: 0.01s Unsat: 0.63s)
CPU Time     : 40.264s

Choices      : 714191   (Domain: 623976)
Conflicts    : 65746    (Analyzed: 65744)
Restarts     : 734      (Average: 89.57 Last: 139)
Model-Level  : 291.0   
Problems     : 11       (Average Length: 20.64 Splits: 0)
Lemmas       : 65744    (Deleted: 55969)
  Binary     : 3251     (Ratio:   4.94%)
  Ternary    : 840      (Ratio:   1.28%)
  Conflict   : 65744    (Average Length:  570.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 65744    (Average: 10.13 Max: 312 Sum: 665760)
  Executed   : 65696    (Average: 10.11 Max: 312 Sum: 664531 Ratio:  99.82%)
  Bounded    : 48       (Average: 25.60 Max:  32 Sum:   1229 Ratio:   0.18%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 181544   (Eliminated:    0 Frozen: 55990)
Constraints  : 1245925  (Binary:  91.4% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 6.04s
Memory:		 324MB (+0MB)
UNKNOWN
Iteration Time:	 6.06s

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         : 45.166s (Solving: 40.08s 1st Model: 0.01s Unsat: 0.63s)
CPU Time     : 45.064s

Choices      : 784778   (Domain: 693921)
Conflicts    : 73720    (Analyzed: 73718)
Restarts     : 834      (Average: 88.39 Last: 139)
Model-Level  : 291.0   
Problems     : 12       (Average Length: 21.58 Splits: 0)
Lemmas       : 73718    (Deleted: 62373)
  Binary     : 3447     (Ratio:   4.68%)
  Ternary    : 896      (Ratio:   1.22%)
  Conflict   : 73718    (Average Length:  535.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 73718    (Average:  9.89 Max: 346 Sum: 728761)
  Executed   : 73667    (Average:  9.87 Max: 346 Sum: 727436 Ratio:  99.82%)
  Bounded    : 51       (Average: 25.98 Max:  32 Sum:   1325 Ratio:   0.18%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 181544   (Eliminated:    0 Frozen: 55990)
Constraints  : 1238757  (Binary:  91.4% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 4.79s
Memory:		 324MB (+0MB)
UNKNOWN
Iteration Time:	 4.80s

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: 360.0MB
Grounding...	 [('step', [31]), ('step', [32]), ('step', [33]), ('step', [34]), ('step', [35]), ('check', [35])]
Grounding Time:	 0.45s
Memory:		 326MB (+2MB)
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 13
Time         : 51.617s (Solving: 45.79s 1st Model: 0.01s Unsat: 0.63s)
CPU Time     : 51.516s

Choices      : 934408   (Domain: 837865)
Conflicts    : 82546    (Analyzed: 82544)
Restarts     : 934      (Average: 88.38 Last: 139)
Model-Level  : 291.0   
Problems     : 13       (Average Length: 22.77 Splits: 0)
Lemmas       : 82544    (Deleted: 72569)
  Binary     : 3652     (Ratio:   4.42%)
  Ternary    : 910      (Ratio:   1.10%)
  Conflict   : 82544    (Average Length:  510.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 82544    (Average: 10.52 Max: 346 Sum: 868541)
  Executed   : 82493    (Average: 10.51 Max: 346 Sum: 867216 Ratio:  99.85%)
  Bounded    : 51       (Average: 25.98 Max:  32 Sum:   1325 Ratio:   0.15%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 214490   (Eliminated:    0 Frozen: 66425)
Constraints  : 1483609  (Binary:  91.4% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 5.77s
Memory:		 340MB (+14MB)
UNKNOWN
Iteration Time:	 6.47s

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

Models       : 0+
Calls        : 14
Time         : 57.561s (Solving: 50.94s 1st Model: 0.01s Unsat: 0.63s)
CPU Time     : 57.464s

Choices      : 1069000  (Domain: 968514)
Conflicts    : 90579    (Analyzed: 90577)
Restarts     : 1034     (Average: 87.60 Last: 160)
Model-Level  : 291.0   
Problems     : 14       (Average Length: 24.14 Splits: 0)
Lemmas       : 90577    (Deleted: 79180)
  Binary     : 3781     (Ratio:   4.17%)
  Ternary    : 921      (Ratio:   1.02%)
  Conflict   : 90577    (Average Length:  497.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 90577    (Average: 10.94 Max: 377 Sum: 990674)
  Executed   : 90526    (Average: 10.92 Max: 377 Sum: 989349 Ratio:  99.87%)
  Bounded    : 51       (Average: 25.98 Max:  32 Sum:   1325 Ratio:   0.13%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 247436   (Eliminated:    0 Frozen: 76860)
Constraints  : 1733194  (Binary:  91.4% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 5.22s
Memory:		 361MB (+14MB)
UNKNOWN
Iteration Time:	 5.96s

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: 397.0MB
Grounding...	 [('step', [41]), ('step', [42]), ('step', [43]), ('step', [44]), ('step', [45]), ('check', [45])]
Grounding Time:	 0.50s
Memory:		 369MB (+8MB)
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 15
Time         : 63.848s (Solving: 56.39s 1st Model: 0.01s Unsat: 0.63s)
CPU Time     : 63.752s

Choices      : 1226884  (Domain: 1120339)
Conflicts    : 98450    (Analyzed: 98448)
Restarts     : 1134     (Average: 86.81 Last: 160)
Model-Level  : 291.0   
Problems     : 15       (Average Length: 25.67 Splits: 0)
Lemmas       : 98448    (Deleted: 86956)
  Binary     : 3885     (Ratio:   3.95%)
  Ternary    : 927      (Ratio:   0.94%)
  Conflict   : 98448    (Average Length:  487.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 98448    (Average: 11.51 Max: 422 Sum: 1133024)
  Executed   : 98397    (Average: 11.50 Max: 422 Sum: 1131699 Ratio:  99.88%)
  Bounded    : 51       (Average: 25.98 Max:  32 Sum:   1325 Ratio:   0.12%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 280382   (Eliminated:    0 Frozen: 87295)
Constraints  : 1982779  (Binary:  91.4% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 5.51s
Memory:		 403MB (+34MB)
UNKNOWN
Iteration Time:	 6.30s

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

Models       : 0+
Calls        : 16
Time         : 72.324s (Solving: 64.03s 1st Model: 0.01s Unsat: 0.63s)
CPU Time     : 72.232s

Choices      : 1435796  (Domain: 1322524)
Conflicts    : 106907   (Analyzed: 106905)
Restarts     : 1234     (Average: 86.63 Last: 160)
Model-Level  : 291.0   
Problems     : 16       (Average Length: 27.31 Splits: 0)
Lemmas       : 106905   (Deleted: 94659)
  Binary     : 4134     (Ratio:   3.87%)
  Ternary    : 997      (Ratio:   0.93%)
  Conflict   : 106905   (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    : 106905   (Average: 12.39 Max: 462 Sum: 1324212)
  Executed   : 106854   (Average: 12.37 Max: 462 Sum: 1322887 Ratio:  99.90%)
  Bounded    : 51       (Average: 25.98 Max:  32 Sum:   1325 Ratio:   0.10%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 313328   (Eliminated:    0 Frozen: 97730)
Constraints  : 2232364  (Binary:  91.4% Ternary:   6.8% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 17
Time         : 79.625s (Solving: 70.33s 1st Model: 0.01s Unsat: 0.63s)
CPU Time     : 79.532s

Choices      : 1546741  (Domain: 1432858)
Conflicts    : 114606   (Analyzed: 114604)
Restarts     : 1334     (Average: 85.91 Last: 160)
Model-Level  : 291.0   
Problems     : 17       (Average Length: 29.06 Splits: 0)
Lemmas       : 114604   (Deleted: 102936)
  Binary     : 4223     (Ratio:   3.68%)
  Ternary    : 1009     (Ratio:   0.88%)
  Conflict   : 114604   (Average Length:  495.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 114604   (Average: 12.38 Max: 499 Sum: 1418921)
  Executed   : 114553   (Average: 12.37 Max: 499 Sum: 1417596 Ratio:  99.91%)
  Bounded    : 51       (Average: 25.98 Max:  32 Sum:   1325 Ratio:   0.09%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 346274   (Eliminated:    0 Frozen: 108165)
Constraints  : 2481949  (Binary:  91.4% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 6.38s
Memory:		 452MB (+18MB)
UNKNOWN
Iteration Time:	 7.31s

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

Models       : 0+
Calls        : 18
Time         : 87.805s (Solving: 77.67s 1st Model: 0.01s Unsat: 0.63s)
CPU Time     : 87.716s

Choices      : 1637998  (Domain: 1523581)
Conflicts    : 121831   (Analyzed: 121829)
Restarts     : 1434     (Average: 84.96 Last: 160)
Model-Level  : 291.0   
Problems     : 18       (Average Length: 30.89 Splits: 0)
Lemmas       : 121829   (Deleted: 110454)
  Binary     : 4297     (Ratio:   3.53%)
  Ternary    : 1016     (Ratio:   0.83%)
  Conflict   : 121829   (Average Length:  498.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 121829   (Average: 12.25 Max: 518 Sum: 1492986)
  Executed   : 121778   (Average: 12.24 Max: 518 Sum: 1491661 Ratio:  99.91%)
  Bounded    : 51       (Average: 25.98 Max:  32 Sum:   1325 Ratio:   0.09%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 379220   (Eliminated:    0 Frozen: 118600)
Constraints  : 2731534  (Binary:  91.4% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 7.42s
Memory:		 507MB (+52MB)
UNKNOWN
Iteration Time:	 8.19s

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

Models       : 0+
Calls        : 19
Time         : 95.725s (Solving: 84.72s 1st Model: 0.01s Unsat: 0.63s)
CPU Time     : 95.640s

Choices      : 1717839  (Domain: 1603246)
Conflicts    : 129118   (Analyzed: 129116)
Restarts     : 1534     (Average: 84.17 Last: 160)
Model-Level  : 291.0   
Problems     : 19       (Average Length: 32.79 Splits: 0)
Lemmas       : 129116   (Deleted: 117640)
  Binary     : 4332     (Ratio:   3.36%)
  Ternary    : 1020     (Ratio:   0.79%)
  Conflict   : 129116   (Average Length:  499.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 129116   (Average: 12.05 Max: 539 Sum: 1555243)
  Executed   : 129065   (Average: 12.04 Max: 539 Sum: 1553918 Ratio:  99.91%)
  Bounded    : 51       (Average: 25.98 Max:  32 Sum:   1325 Ratio:   0.09%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 412166   (Eliminated:    0 Frozen: 129035)
Constraints  : 2981119  (Binary:  91.4% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 7.14s
Memory:		 511MB (+4MB)
UNKNOWN
Iteration Time:	 7.93s

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

Models       : 0+
Calls        : 20
Time         : 103.990s (Solving: 92.11s 1st Model: 0.01s Unsat: 0.63s)
CPU Time     : 103.908s

Choices      : 1798781  (Domain: 1684030)
Conflicts    : 136483   (Analyzed: 136481)
Restarts     : 1634     (Average: 83.53 Last: 160)
Model-Level  : 291.0   
Problems     : 20       (Average Length: 34.75 Splits: 0)
Lemmas       : 136481   (Deleted: 124817)
  Binary     : 4363     (Ratio:   3.20%)
  Ternary    : 1024     (Ratio:   0.75%)
  Conflict   : 136481   (Average Length:  497.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 136481   (Average: 11.85 Max: 609 Sum: 1617905)
  Executed   : 136430   (Average: 11.84 Max: 609 Sum: 1616580 Ratio:  99.92%)
  Bounded    : 51       (Average: 25.98 Max:  32 Sum:   1325 Ratio:   0.08%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 445112   (Eliminated:    0 Frozen: 139470)
Constraints  : 3230704  (Binary:  91.4% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 7.49s
Memory:		 531MB (+17MB)
UNKNOWN
Iteration Time:	 8.28s

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

Models       : 0+
Calls        : 21
Time         : 112.384s (Solving: 99.55s 1st Model: 0.01s Unsat: 0.63s)
CPU Time     : 112.304s

Choices      : 1896040  (Domain: 1781176)
Conflicts    : 144054   (Analyzed: 144052)
Restarts     : 1734     (Average: 83.07 Last: 160)
Model-Level  : 291.0   
Problems     : 21       (Average Length: 36.76 Splits: 0)
Lemmas       : 144052   (Deleted: 131924)
  Binary     : 4409     (Ratio:   3.06%)
  Ternary    : 1026     (Ratio:   0.71%)
  Conflict   : 144052   (Average Length:  495.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 144052   (Average: 11.77 Max: 621 Sum: 1695535)
  Executed   : 144001   (Average: 11.76 Max: 621 Sum: 1694210 Ratio:  99.92%)
  Bounded    : 51       (Average: 25.98 Max:  32 Sum:   1325 Ratio:   0.08%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 478058   (Eliminated:    0 Frozen: 149905)
Constraints  : 3480289  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 7.54s
Memory:		 558MB (+24MB)
UNKNOWN
Iteration Time:	 8.41s

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

Models       : 0+
Calls        : 22
Time         : 120.922s (Solving: 107.11s 1st Model: 0.01s Unsat: 0.63s)
CPU Time     : 120.844s

Choices      : 1996895  (Domain: 1881917)
Conflicts    : 152072   (Analyzed: 152070)
Restarts     : 1834     (Average: 82.92 Last: 160)
Model-Level  : 291.0   
Problems     : 22       (Average Length: 38.82 Splits: 0)
Lemmas       : 152070   (Deleted: 139117)
  Binary     : 4461     (Ratio:   2.93%)
  Ternary    : 1030     (Ratio:   0.68%)
  Conflict   : 152070   (Average Length:  495.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 152070   (Average: 11.67 Max: 780 Sum: 1774727)
  Executed   : 152019   (Average: 11.66 Max: 780 Sum: 1773402 Ratio:  99.93%)
  Bounded    : 51       (Average: 25.98 Max:  32 Sum:   1325 Ratio:   0.07%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 511004   (Eliminated:    0 Frozen: 160340)
Constraints  : 3729874  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 7.67s
Memory:		 582MB (+24MB)
UNKNOWN
Iteration Time:	 8.55s

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

Models       : 0
Calls        : 23
Time         : 121.763s (Solving: 107.85s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 121.688s

Choices      : 2005388  (Domain: 1890410)
Conflicts    : 153340   (Analyzed: 153337)
Restarts     : 1849     (Average: 82.93 Last: 160)
Model-Level  : 291.0   
Problems     : 23       (Average Length: 40.70 Splits: 0)
Lemmas       : 153337   (Deleted: 139117)
  Binary     : 4498     (Ratio:   2.93%)
  Ternary    : 1042     (Ratio:   0.68%)
  Conflict   : 153337   (Average Length:  493.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 153337   (Average: 11.63 Max: 780 Sum: 1782771)
  Executed   : 153279   (Average: 11.62 Max: 780 Sum: 1781439 Ratio:  99.93%)
  Bounded    : 58       (Average: 22.97 Max:  32 Sum:   1332 Ratio:   0.07%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 511004   (Eliminated:    0 Frozen: 160340)
Constraints  : 3729874  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 0.81s
Memory:		 582MB (+0MB)
UNSAT
Iteration Time:	 0.84s

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

Models       : 0+
Calls        : 24
Time         : 126.431s (Solving: 112.42s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 126.360s

Choices      : 2062972  (Domain: 1946477)
Conflicts    : 161590   (Analyzed: 161587)
Restarts     : 1949     (Average: 82.91 Last: 160)
Model-Level  : 291.0   
Problems     : 24       (Average Length: 42.42 Splits: 0)
Lemmas       : 161587   (Deleted: 146746)
  Binary     : 4640     (Ratio:   2.87%)
  Ternary    : 1077     (Ratio:   0.67%)
  Conflict   : 161587   (Average Length:  478.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 161587   (Average: 11.35 Max: 780 Sum: 1834184)
  Executed   : 161529   (Average: 11.34 Max: 780 Sum: 1832852 Ratio:  99.93%)
  Bounded    : 58       (Average: 22.97 Max:  32 Sum:   1332 Ratio:   0.07%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 511004   (Eliminated:    0 Frozen: 160340)
Constraints  : 3729874  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 4.64s
Memory:		 582MB (+0MB)
UNKNOWN
Iteration Time:	 4.67s

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

Models       : 0+
Calls        : 25
Time         : 131.525s (Solving: 117.41s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 131.460s

Choices      : 2122045  (Domain: 2005227)
Conflicts    : 169433   (Analyzed: 169430)
Restarts     : 2049     (Average: 82.69 Last: 160)
Model-Level  : 291.0   
Problems     : 25       (Average Length: 44.00 Splits: 0)
Lemmas       : 169430   (Deleted: 154617)
  Binary     : 4747     (Ratio:   2.80%)
  Ternary    : 1130     (Ratio:   0.67%)
  Conflict   : 169430   (Average Length:  469.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 169430   (Average: 11.14 Max: 780 Sum: 1887070)
  Executed   : 169372   (Average: 11.13 Max: 780 Sum: 1885738 Ratio:  99.93%)
  Bounded    : 58       (Average: 22.97 Max:  32 Sum:   1332 Ratio:   0.07%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 511004   (Eliminated:    0 Frozen: 160340)
Constraints  : 3729874  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 26
Time         : 136.134s (Solving: 121.89s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 136.072s

Choices      : 2176038  (Domain: 2058993)
Conflicts    : 177233   (Analyzed: 177230)
Restarts     : 2149     (Average: 82.47 Last: 160)
Model-Level  : 291.0   
Problems     : 26       (Average Length: 45.46 Splits: 0)
Lemmas       : 177230   (Deleted: 161742)
  Binary     : 4845     (Ratio:   2.73%)
  Ternary    : 1167     (Ratio:   0.66%)
  Conflict   : 177230   (Average Length:  459.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 177230   (Average: 10.91 Max: 780 Sum: 1933259)
  Executed   : 177172   (Average: 10.90 Max: 780 Sum: 1931927 Ratio:  99.93%)
  Bounded    : 58       (Average: 22.97 Max:  32 Sum:   1332 Ratio:   0.07%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 511004   (Eliminated:    0 Frozen: 160340)
Constraints  : 3729874  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 4.57s
Memory:		 582MB (+0MB)
UNKNOWN
Iteration Time:	 4.61s

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

Models       : 0+
Calls        : 27
Time         : 140.721s (Solving: 126.37s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 140.660s

Choices      : 2234218  (Domain: 2116994)
Conflicts    : 184583   (Analyzed: 184580)
Restarts     : 2249     (Average: 82.07 Last: 160)
Model-Level  : 291.0   
Problems     : 27       (Average Length: 46.81 Splits: 0)
Lemmas       : 184580   (Deleted: 169170)
  Binary     : 4900     (Ratio:   2.65%)
  Ternary    : 1179     (Ratio:   0.64%)
  Conflict   : 184580   (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    : 184580   (Average: 10.74 Max: 780 Sum: 1982862)
  Executed   : 184522   (Average: 10.74 Max: 780 Sum: 1981530 Ratio:  99.93%)
  Bounded    : 58       (Average: 22.97 Max:  32 Sum:   1332 Ratio:   0.07%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 511004   (Eliminated:    0 Frozen: 160340)
Constraints  : 3729874  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 4.55s
Memory:		 582MB (+0MB)
UNKNOWN
Iteration Time:	 4.59s

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

Models       : 0+
Calls        : 28
Time         : 145.191s (Solving: 130.70s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 145.128s

Choices      : 2286412  (Domain: 2169041)
Conflicts    : 192110   (Analyzed: 192107)
Restarts     : 2349     (Average: 81.78 Last: 160)
Model-Level  : 291.0   
Problems     : 28       (Average Length: 48.07 Splits: 0)
Lemmas       : 192107   (Deleted: 176310)
  Binary     : 4931     (Ratio:   2.57%)
  Ternary    : 1189     (Ratio:   0.62%)
  Conflict   : 192107   (Average Length:  447.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 192107   (Average: 10.55 Max: 780 Sum: 2025996)
  Executed   : 192049   (Average: 10.54 Max: 780 Sum: 2024664 Ratio:  99.93%)
  Bounded    : 58       (Average: 22.97 Max:  32 Sum:   1332 Ratio:   0.07%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 511004   (Eliminated:    0 Frozen: 160340)
Constraints  : 3729874  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 4.42s
Memory:		 582MB (+0MB)
UNKNOWN
Iteration Time:	 4.48s

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

Models       : 0+
Calls        : 29
Time         : 149.156s (Solving: 134.55s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 149.096s

Choices      : 2327784  (Domain: 2210322)
Conflicts    : 199786   (Analyzed: 199783)
Restarts     : 2449     (Average: 81.58 Last: 160)
Model-Level  : 291.0   
Problems     : 29       (Average Length: 49.24 Splits: 0)
Lemmas       : 199783   (Deleted: 183812)
  Binary     : 4963     (Ratio:   2.48%)
  Ternary    : 1216     (Ratio:   0.61%)
  Conflict   : 199783   (Average Length:  441.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 199783   (Average: 10.31 Max: 780 Sum: 2058952)
  Executed   : 199725   (Average: 10.30 Max: 780 Sum: 2057620 Ratio:  99.94%)
  Bounded    : 58       (Average: 22.97 Max:  32 Sum:   1332 Ratio:   0.06%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 511004   (Eliminated:    0 Frozen: 160340)
Constraints  : 3729874  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 30
Time         : 155.062s (Solving: 140.35s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 155.004s

Choices      : 2433908  (Domain: 2315834)
Conflicts    : 207495   (Analyzed: 207492)
Restarts     : 2549     (Average: 81.40 Last: 160)
Model-Level  : 291.0   
Problems     : 30       (Average Length: 50.33 Splits: 0)
Lemmas       : 207492   (Deleted: 191265)
  Binary     : 4992     (Ratio:   2.41%)
  Ternary    : 1231     (Ratio:   0.59%)
  Conflict   : 207492   (Average Length:  434.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 207492   (Average: 10.38 Max: 780 Sum: 2154451)
  Executed   : 207434   (Average: 10.38 Max: 780 Sum: 2153119 Ratio:  99.94%)
  Bounded    : 58       (Average: 22.97 Max:  32 Sum:   1332 Ratio:   0.06%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 511004   (Eliminated:    0 Frozen: 160340)
Constraints  : 3729874  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 5.88s
Memory:		 582MB (+0MB)
UNKNOWN
Iteration Time:	 5.91s

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

Models       : 0+
Calls        : 31
Time         : 159.967s (Solving: 145.14s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 159.912s

Choices      : 2498978  (Domain: 2380736)
Conflicts    : 215028   (Analyzed: 215025)
Restarts     : 2649     (Average: 81.17 Last: 160)
Model-Level  : 291.0   
Problems     : 31       (Average Length: 51.35 Splits: 0)
Lemmas       : 215025   (Deleted: 198648)
  Binary     : 5038     (Ratio:   2.34%)
  Ternary    : 1238     (Ratio:   0.58%)
  Conflict   : 215025   (Average Length:  428.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 215025   (Average: 10.28 Max: 780 Sum: 2209710)
  Executed   : 214967   (Average: 10.27 Max: 780 Sum: 2208378 Ratio:  99.94%)
  Bounded    : 58       (Average: 22.97 Max:  32 Sum:   1332 Ratio:   0.06%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 511004   (Eliminated:    0 Frozen: 160340)
Constraints  : 3729874  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 32
Time         : 164.779s (Solving: 149.84s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 164.724s

Choices      : 2559155  (Domain: 2440791)
Conflicts    : 222534   (Analyzed: 222531)
Restarts     : 2749     (Average: 80.95 Last: 160)
Model-Level  : 291.0   
Problems     : 32       (Average Length: 52.31 Splits: 0)
Lemmas       : 222531   (Deleted: 205945)
  Binary     : 5100     (Ratio:   2.29%)
  Ternary    : 1274     (Ratio:   0.57%)
  Conflict   : 222531   (Average Length:  421.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 222531   (Average: 10.16 Max: 780 Sum: 2260193)
  Executed   : 222470   (Average: 10.15 Max: 780 Sum: 2258620 Ratio:  99.93%)
  Bounded    : 61       (Average: 25.79 Max:  82 Sum:   1573 Ratio:   0.07%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 511004   (Eliminated:    0 Frozen: 160340)
Constraints  : 3729874  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 4.78s
Memory:		 582MB (+0MB)
UNKNOWN
Iteration Time:	 4.82s

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

Models       : 0+
Calls        : 33
Time         : 170.875s (Solving: 155.80s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 170.824s

Choices      : 2647568  (Domain: 2528726)
Conflicts    : 230317   (Analyzed: 230314)
Restarts     : 2849     (Average: 80.84 Last: 160)
Model-Level  : 291.0   
Problems     : 33       (Average Length: 53.21 Splits: 0)
Lemmas       : 230314   (Deleted: 213172)
  Binary     : 5143     (Ratio:   2.23%)
  Ternary    : 1283     (Ratio:   0.56%)
  Conflict   : 230314   (Average Length:  416.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 230314   (Average: 10.15 Max: 780 Sum: 2337510)
  Executed   : 230251   (Average: 10.14 Max: 780 Sum: 2335778 Ratio:  99.93%)
  Bounded    : 63       (Average: 27.49 Max:  82 Sum:   1732 Ratio:   0.07%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 511004   (Eliminated:    0 Frozen: 160340)
Constraints  : 3729846  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 34
Time         : 176.457s (Solving: 161.28s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 176.408s

Choices      : 2717048  (Domain: 2598009)
Conflicts    : 238011   (Analyzed: 238008)
Restarts     : 2949     (Average: 80.71 Last: 160)
Model-Level  : 291.0   
Problems     : 34       (Average Length: 54.06 Splits: 0)
Lemmas       : 238008   (Deleted: 220695)
  Binary     : 5201     (Ratio:   2.19%)
  Ternary    : 1302     (Ratio:   0.55%)
  Conflict   : 238008   (Average Length:  410.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 238008   (Average: 10.07 Max: 780 Sum: 2397063)
  Executed   : 237944   (Average: 10.06 Max: 780 Sum: 2395254 Ratio:  99.92%)
  Bounded    : 64       (Average: 28.27 Max:  82 Sum:   1809 Ratio:   0.08%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 511004   (Eliminated:    0 Frozen: 160340)
Constraints  : 3729832  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 35
Time         : 181.862s (Solving: 166.56s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 181.816s

Choices      : 2788662  (Domain: 2669482)
Conflicts    : 245419   (Analyzed: 245416)
Restarts     : 3049     (Average: 80.49 Last: 160)
Model-Level  : 291.0   
Problems     : 35       (Average Length: 54.86 Splits: 0)
Lemmas       : 245416   (Deleted: 228150)
  Binary     : 5236     (Ratio:   2.13%)
  Ternary    : 1323     (Ratio:   0.54%)
  Conflict   : 245416   (Average Length:  404.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 245416   (Average: 10.02 Max: 780 Sum: 2458385)
  Executed   : 245348   (Average: 10.01 Max: 780 Sum: 2456260 Ratio:  99.91%)
  Bounded    : 68       (Average: 31.25 Max:  82 Sum:   2125 Ratio:   0.09%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 511004   (Eliminated:    0 Frozen: 160340)
Constraints  : 3729832  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 36
Time         : 186.788s (Solving: 171.38s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 186.748s

Choices      : 2893793  (Domain: 2774504)
Conflicts    : 253167   (Analyzed: 253164)
Restarts     : 3149     (Average: 80.40 Last: 160)
Model-Level  : 291.0   
Problems     : 36       (Average Length: 55.61 Splits: 0)
Lemmas       : 253164   (Deleted: 235330)
  Binary     : 5283     (Ratio:   2.09%)
  Ternary    : 1337     (Ratio:   0.53%)
  Conflict   : 253164   (Average Length:  398.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 253164   (Average: 10.08 Max: 780 Sum: 2550984)
  Executed   : 253093   (Average: 10.07 Max: 780 Sum: 2548622 Ratio:  99.91%)
  Bounded    : 71       (Average: 33.27 Max:  82 Sum:   2362 Ratio:   0.09%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 511004   (Eliminated:    0 Frozen: 160340)
Constraints  : 3727560  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 4.89s
Memory:		 582MB (+0MB)
UNKNOWN
Iteration Time:	 4.93s

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

Models       : 0+
Calls        : 37
Time         : 193.920s (Solving: 177.57s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 193.884s

Choices      : 3002206  (Domain: 2882841)
Conflicts    : 261207   (Analyzed: 261204)
Restarts     : 3249     (Average: 80.40 Last: 160)
Model-Level  : 291.0   
Problems     : 37       (Average Length: 56.46 Splits: 0)
Lemmas       : 261204   (Deleted: 243748)
  Binary     : 5327     (Ratio:   2.04%)
  Ternary    : 1343     (Ratio:   0.51%)
  Conflict   : 261204   (Average Length:  396.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 261204   (Average: 10.10 Max: 834 Sum: 2638743)
  Executed   : 261133   (Average: 10.09 Max: 834 Sum: 2636381 Ratio:  99.91%)
  Bounded    : 71       (Average: 33.27 Max:  82 Sum:   2362 Ratio:   0.09%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 543950   (Eliminated:    0 Frozen: 170775)
Constraints  : 3974876  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 6.30s
Memory:		 602MB (+20MB)
UNKNOWN
Iteration Time:	 7.14s

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

Models       : 0+
Calls        : 38
Time         : 200.445s (Solving: 183.13s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 200.412s

Choices      : 3086288  (Domain: 2966896)
Conflicts    : 268997   (Analyzed: 268994)
Restarts     : 3349     (Average: 80.32 Last: 160)
Model-Level  : 291.0   
Problems     : 38       (Average Length: 57.39 Splits: 0)
Lemmas       : 268994   (Deleted: 251843)
  Binary     : 5370     (Ratio:   2.00%)
  Ternary    : 1350     (Ratio:   0.50%)
  Conflict   : 268994   (Average Length:  394.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 268994   (Average: 10.04 Max: 834 Sum: 2700626)
  Executed   : 268923   (Average: 10.03 Max: 834 Sum: 2698264 Ratio:  99.91%)
  Bounded    : 71       (Average: 33.27 Max:  82 Sum:   2362 Ratio:   0.09%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 576896   (Eliminated:    0 Frozen: 181210)
Constraints  : 4224461  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 5.66s
Memory:		 673MB (+71MB)
UNKNOWN
Iteration Time:	 6.54s

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

Models       : 0+
Calls        : 39
Time         : 207.525s (Solving: 189.20s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 207.496s

Choices      : 3173307  (Domain: 3053894)
Conflicts    : 276902   (Analyzed: 276899)
Restarts     : 3449     (Average: 80.28 Last: 160)
Model-Level  : 291.0   
Problems     : 39       (Average Length: 58.41 Splits: 0)
Lemmas       : 276899   (Deleted: 259574)
  Binary     : 5401     (Ratio:   1.95%)
  Ternary    : 1354     (Ratio:   0.49%)
  Conflict   : 276899   (Average Length:  392.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 276899   (Average:  9.99 Max: 834 Sum: 2764854)
  Executed   : 276828   (Average:  9.98 Max: 834 Sum: 2762492 Ratio:  99.91%)
  Bounded    : 71       (Average: 33.27 Max:  82 Sum:   2362 Ratio:   0.09%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 609842   (Eliminated:    0 Frozen: 191645)
Constraints  : 4474046  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 6.18s
Memory:		 677MB (+4MB)
UNKNOWN
Iteration Time:	 7.09s

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

Models       : 0+
Calls        : 40
Time         : 214.956s (Solving: 195.62s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 214.928s

Choices      : 3268235  (Domain: 3148762)
Conflicts    : 284218   (Analyzed: 284215)
Restarts     : 3549     (Average: 80.08 Last: 160)
Model-Level  : 291.0   
Problems     : 40       (Average Length: 59.50 Splits: 0)
Lemmas       : 284215   (Deleted: 267153)
  Binary     : 5431     (Ratio:   1.91%)
  Ternary    : 1363     (Ratio:   0.48%)
  Conflict   : 284215   (Average Length:  390.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 284215   (Average:  9.98 Max: 999 Sum: 2835144)
  Executed   : 284144   (Average:  9.97 Max: 999 Sum: 2832782 Ratio:  99.92%)
  Bounded    : 71       (Average: 33.27 Max:  82 Sum:   2362 Ratio:   0.08%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 642788   (Eliminated:    0 Frozen: 202080)
Constraints  : 4723631  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 6.54s
Memory:		 685MB (+8MB)
UNKNOWN
Iteration Time:	 7.44s

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

Models       : 0+
Calls        : 41
Time         : 218.963s (Solving: 199.46s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 218.936s

Choices      : 3322702  (Domain: 3202872)
Conflicts    : 291860   (Analyzed: 291857)
Restarts     : 3649     (Average: 79.98 Last: 160)
Model-Level  : 291.0   
Problems     : 41       (Average Length: 60.54 Splits: 0)
Lemmas       : 291857   (Deleted: 273285)
  Binary     : 5534     (Ratio:   1.90%)
  Ternary    : 1380     (Ratio:   0.47%)
  Conflict   : 291857   (Average Length:  387.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 291857   (Average:  9.88 Max: 999 Sum: 2884584)
  Executed   : 291784   (Average:  9.87 Max: 999 Sum: 2882022 Ratio:  99.91%)
  Bounded    : 73       (Average: 35.10 Max: 102 Sum:   2562 Ratio:   0.09%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 642788   (Eliminated:    0 Frozen: 202080)
Constraints  : 4723631  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 42
Time         : 224.566s (Solving: 204.93s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 224.540s

Choices      : 3400764  (Domain: 3278639)
Conflicts    : 300194   (Analyzed: 300191)
Restarts     : 3749     (Average: 80.07 Last: 160)
Model-Level  : 291.0   
Problems     : 42       (Average Length: 61.52 Splits: 0)
Lemmas       : 300191   (Deleted: 279573)
  Binary     : 5941     (Ratio:   1.98%)
  Ternary    : 1517     (Ratio:   0.51%)
  Conflict   : 300191   (Average Length:  383.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 300191   (Average:  9.84 Max: 999 Sum: 2954167)
  Executed   : 300116   (Average:  9.83 Max: 999 Sum: 2951406 Ratio:  99.91%)
  Bounded    : 75       (Average: 36.81 Max: 102 Sum:   2761 Ratio:   0.09%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 642788   (Eliminated:    0 Frozen: 202080)
Constraints  : 4721173  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 5.56s
Memory:		 685MB (+0MB)
UNKNOWN
Iteration Time:	 5.61s

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

Models       : 0+
Calls        : 43
Time         : 229.374s (Solving: 209.61s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 229.348s

Choices      : 3462633  (Domain: 3337740)
Conflicts    : 308354   (Analyzed: 308351)
Restarts     : 3849     (Average: 80.11 Last: 160)
Model-Level  : 291.0   
Problems     : 43       (Average Length: 62.47 Splits: 0)
Lemmas       : 308351   (Deleted: 287354)
  Binary     : 6011     (Ratio:   1.95%)
  Ternary    : 1530     (Ratio:   0.50%)
  Conflict   : 308351   (Average Length:  379.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 308351   (Average:  9.76 Max: 999 Sum: 3008037)
  Executed   : 308276   (Average:  9.75 Max: 999 Sum: 3005276 Ratio:  99.91%)
  Bounded    : 75       (Average: 36.81 Max: 102 Sum:   2761 Ratio:   0.09%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 642788   (Eliminated:    0 Frozen: 202080)
Constraints  : 4721148  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 4.77s
Memory:		 685MB (+0MB)
UNKNOWN
Iteration Time:	 4.81s

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

Models       : 0+
Calls        : 44
Time         : 234.338s (Solving: 214.41s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 234.316s

Choices      : 3571308  (Domain: 3442777)
Conflicts    : 316527   (Analyzed: 316524)
Restarts     : 3949     (Average: 80.15 Last: 160)
Model-Level  : 291.0   
Problems     : 44       (Average Length: 63.36 Splits: 0)
Lemmas       : 316524   (Deleted: 295197)
  Binary     : 6210     (Ratio:   1.96%)
  Ternary    : 1568     (Ratio:   0.50%)
  Conflict   : 316524   (Average Length:  377.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 316524   (Average:  9.82 Max: 999 Sum: 3106768)
  Executed   : 316447   (Average:  9.81 Max: 999 Sum: 3103808 Ratio:  99.90%)
  Bounded    : 77       (Average: 38.44 Max: 102 Sum:   2960 Ratio:   0.10%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 642788   (Eliminated:    0 Frozen: 202080)
Constraints  : 4721148  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 45
Time         : 240.395s (Solving: 220.33s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 240.376s

Choices      : 3737668  (Domain: 3605453)
Conflicts    : 325048   (Analyzed: 325045)
Restarts     : 4049     (Average: 80.28 Last: 160)
Model-Level  : 291.0   
Problems     : 45       (Average Length: 64.22 Splits: 0)
Lemmas       : 325045   (Deleted: 302821)
  Binary     : 6414     (Ratio:   1.97%)
  Ternary    : 1582     (Ratio:   0.49%)
  Conflict   : 325045   (Average Length:  378.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 325045   (Average: 10.03 Max: 999 Sum: 3258654)
  Executed   : 324966   (Average: 10.02 Max: 999 Sum: 3255493 Ratio:  99.90%)
  Bounded    : 79       (Average: 40.01 Max: 102 Sum:   3161 Ratio:   0.10%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 642788   (Eliminated:    0 Frozen: 202080)
Constraints  : 4721134  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 6.01s
Memory:		 685MB (+0MB)
UNKNOWN
Iteration Time:	 6.06s

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

Models       : 0+
Calls        : 46
Time         : 245.337s (Solving: 225.14s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 245.320s

Choices      : 3839694  (Domain: 3704901)
Conflicts    : 332966   (Analyzed: 332963)
Restarts     : 4149     (Average: 80.25 Last: 160)
Model-Level  : 291.0   
Problems     : 46       (Average Length: 65.04 Splits: 0)
Lemmas       : 332963   (Deleted: 310905)
  Binary     : 6504     (Ratio:   1.95%)
  Ternary    : 1595     (Ratio:   0.48%)
  Conflict   : 332963   (Average Length:  378.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 332963   (Average: 10.06 Max: 999 Sum: 3350068)
  Executed   : 332882   (Average: 10.05 Max: 999 Sum: 3346708 Ratio:  99.90%)
  Bounded    : 81       (Average: 41.48 Max: 102 Sum:   3360 Ratio:   0.10%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 642788   (Eliminated:    0 Frozen: 202080)
Constraints  : 4721108  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 47
Time         : 250.797s (Solving: 230.47s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 250.780s

Choices      : 4003165  (Domain: 3865782)
Conflicts    : 341409   (Analyzed: 341406)
Restarts     : 4249     (Average: 80.35 Last: 160)
Model-Level  : 291.0   
Problems     : 47       (Average Length: 65.83 Splits: 0)
Lemmas       : 341406   (Deleted: 318260)
  Binary     : 6595     (Ratio:   1.93%)
  Ternary    : 1604     (Ratio:   0.47%)
  Conflict   : 341406   (Average Length:  378.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 341406   (Average: 10.25 Max: 999 Sum: 3499927)
  Executed   : 341324   (Average: 10.24 Max: 999 Sum: 3496465 Ratio:  99.90%)
  Bounded    : 82       (Average: 42.22 Max: 102 Sum:   3462 Ratio:   0.10%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 642788   (Eliminated:    0 Frozen: 202080)
Constraints  : 4718476  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 48
Time         : 257.083s (Solving: 236.63s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 257.068s

Choices      : 4216056  (Domain: 4075086)
Conflicts    : 349802   (Analyzed: 349799)
Restarts     : 4349     (Average: 80.43 Last: 160)
Model-Level  : 291.0   
Problems     : 48       (Average Length: 66.58 Splits: 0)
Lemmas       : 349799   (Deleted: 326358)
  Binary     : 6713     (Ratio:   1.92%)
  Ternary    : 1621     (Ratio:   0.46%)
  Conflict   : 349799   (Average Length:  380.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 349799   (Average: 10.57 Max: 999 Sum: 3697875)
  Executed   : 349717   (Average: 10.56 Max: 999 Sum: 3694413 Ratio:  99.91%)
  Bounded    : 82       (Average: 42.22 Max: 102 Sum:   3462 Ratio:   0.09%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 642788   (Eliminated:    0 Frozen: 202080)
Constraints  : 4711606  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 49
Time         : 264.847s (Solving: 244.24s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 264.836s

Choices      : 4579634  (Domain: 4433566)
Conflicts    : 358983   (Analyzed: 358980)
Restarts     : 4449     (Average: 80.69 Last: 160)
Model-Level  : 291.0   
Problems     : 49       (Average Length: 67.31 Splits: 0)
Lemmas       : 358980   (Deleted: 336510)
  Binary     : 6889     (Ratio:   1.92%)
  Ternary    : 1633     (Ratio:   0.45%)
  Conflict   : 358980   (Average Length:  384.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 358980   (Average: 11.26 Max: 999 Sum: 4042190)
  Executed   : 358898   (Average: 11.25 Max: 999 Sum: 4038728 Ratio:  99.91%)
  Bounded    : 82       (Average: 42.22 Max: 102 Sum:   3462 Ratio:   0.09%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 642788   (Eliminated:    0 Frozen: 202080)
Constraints  : 4711606  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 50
Time         : 272.755s (Solving: 252.01s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 272.744s

Choices      : 4887110  (Domain: 4737114)
Conflicts    : 367818   (Analyzed: 367815)
Restarts     : 4549     (Average: 80.86 Last: 160)
Model-Level  : 291.0   
Problems     : 50       (Average Length: 68.00 Splits: 0)
Lemmas       : 367815   (Deleted: 345276)
  Binary     : 7042     (Ratio:   1.91%)
  Ternary    : 1642     (Ratio:   0.45%)
  Conflict   : 367815   (Average Length:  390.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 367815   (Average: 11.77 Max: 999 Sum: 4329157)
  Executed   : 367733   (Average: 11.76 Max: 999 Sum: 4325695 Ratio:  99.92%)
  Bounded    : 82       (Average: 42.22 Max: 102 Sum:   3462 Ratio:   0.08%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 642788   (Eliminated:    0 Frozen: 202080)
Constraints  : 4711606  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 7.86s
Memory:		 685MB (+0MB)
UNKNOWN
Iteration Time:	 7.91s

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

Models       : 0+
Calls        : 51
Time         : 281.145s (Solving: 260.25s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 281.140s

Choices      : 5278719  (Domain: 5126310)
Conflicts    : 376400   (Analyzed: 376397)
Restarts     : 4649     (Average: 80.96 Last: 160)
Model-Level  : 291.0   
Problems     : 51       (Average Length: 68.67 Splits: 0)
Lemmas       : 376397   (Deleted: 351696)
  Binary     : 7189     (Ratio:   1.91%)
  Ternary    : 1647     (Ratio:   0.44%)
  Conflict   : 376397   (Average Length:  394.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 376397   (Average: 12.48 Max: 999 Sum: 4698314)
  Executed   : 376315   (Average: 12.47 Max: 999 Sum: 4694852 Ratio:  99.93%)
  Bounded    : 82       (Average: 42.22 Max: 102 Sum:   3462 Ratio:   0.07%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 642788   (Eliminated:    0 Frozen: 202080)
Constraints  : 4711606  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 8.34s
Memory:		 685MB (+0MB)
UNKNOWN
Iteration Time:	 8.40s

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

Models       : 0+
Calls        : 52
Time         : 287.720s (Solving: 266.70s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 287.716s

Choices      : 5592757  (Domain: 5438631)
Conflicts    : 385304   (Analyzed: 385301)
Restarts     : 4749     (Average: 81.13 Last: 160)
Model-Level  : 291.0   
Problems     : 52       (Average Length: 69.31 Splits: 0)
Lemmas       : 385301   (Deleted: 362085)
  Binary     : 7250     (Ratio:   1.88%)
  Ternary    : 1652     (Ratio:   0.43%)
  Conflict   : 385301   (Average Length:  395.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 385301   (Average: 12.96 Max: 999 Sum: 4992285)
  Executed   : 385219   (Average: 12.95 Max: 999 Sum: 4988823 Ratio:  99.93%)
  Bounded    : 82       (Average: 42.22 Max: 102 Sum:   3462 Ratio:   0.07%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 642788   (Eliminated:    0 Frozen: 202080)
Constraints  : 4711606  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 53
Time         : 294.478s (Solving: 273.32s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 294.476s

Choices      : 5925413  (Domain: 5769233)
Conflicts    : 393631   (Analyzed: 393628)
Restarts     : 4849     (Average: 81.18 Last: 160)
Model-Level  : 291.0   
Problems     : 53       (Average Length: 69.92 Splits: 0)
Lemmas       : 393628   (Deleted: 368593)
  Binary     : 7321     (Ratio:   1.86%)
  Ternary    : 1658     (Ratio:   0.42%)
  Conflict   : 393628   (Average Length:  395.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 393628   (Average: 13.48 Max: 999 Sum: 5305288)
  Executed   : 393546   (Average: 13.47 Max: 999 Sum: 5301826 Ratio:  99.93%)
  Bounded    : 82       (Average: 42.22 Max: 102 Sum:   3462 Ratio:   0.07%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 642788   (Eliminated:    0 Frozen: 202080)
Constraints  : 4711606  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 54
Time         : 303.854s (Solving: 282.55s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 303.856s

Choices      : 6453685  (Domain: 6294411)
Conflicts    : 403180   (Analyzed: 403177)
Restarts     : 4949     (Average: 81.47 Last: 160)
Model-Level  : 291.0   
Problems     : 54       (Average Length: 70.52 Splits: 0)
Lemmas       : 403177   (Deleted: 378716)
  Binary     : 7477     (Ratio:   1.85%)
  Ternary    : 1673     (Ratio:   0.41%)
  Conflict   : 403177   (Average Length:  398.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 403177   (Average: 14.41 Max: 999 Sum: 5807895)
  Executed   : 403095   (Average: 14.40 Max: 999 Sum: 5804433 Ratio:  99.94%)
  Bounded    : 82       (Average: 42.22 Max: 102 Sum:   3462 Ratio:   0.06%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 642788   (Eliminated:    0 Frozen: 202080)
Constraints  : 4711606  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 55
Time         : 309.710s (Solving: 287.37s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 309.716s

Choices      : 6509455  (Domain: 6350179)
Conflicts    : 410906   (Analyzed: 410903)
Restarts     : 5049     (Average: 81.38 Last: 160)
Model-Level  : 291.0   
Problems     : 55       (Average Length: 71.18 Splits: 0)
Lemmas       : 410903   (Deleted: 385999)
  Binary     : 7482     (Ratio:   1.82%)
  Ternary    : 1675     (Ratio:   0.41%)
  Conflict   : 410903   (Average Length:  396.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 410903   (Average: 14.21 Max: 999 Sum: 5838750)
  Executed   : 410821   (Average: 14.20 Max: 999 Sum: 5835288 Ratio:  99.94%)
  Bounded    : 82       (Average: 42.22 Max: 102 Sum:   3462 Ratio:   0.06%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 675734   (Eliminated:    0 Frozen: 212515)
Constraints  : 4961191  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 4.95s
Memory:		 704MB (+19MB)
UNKNOWN
Iteration Time:	 5.87s

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

Models       : 0+
Calls        : 56
Time         : 317.999s (Solving: 294.29s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 318.012s

Choices      : 6572964  (Domain: 6413684)
Conflicts    : 418307   (Analyzed: 418304)
Restarts     : 5149     (Average: 81.24 Last: 160)
Model-Level  : 291.0   
Problems     : 56       (Average Length: 71.91 Splits: 0)
Lemmas       : 418304   (Deleted: 393682)
  Binary     : 7519     (Ratio:   1.80%)
  Ternary    : 1679     (Ratio:   0.40%)
  Conflict   : 418304   (Average Length:  396.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 418304   (Average: 14.05 Max: 999 Sum: 5875974)
  Executed   : 418222   (Average: 14.04 Max: 999 Sum: 5872512 Ratio:  99.94%)
  Bounded    : 82       (Average: 42.22 Max: 102 Sum:   3462 Ratio:   0.06%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 708680   (Eliminated:    0 Frozen: 222950)
Constraints  : 5210776  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 7.09s
Memory:		 738MB (+34MB)
UNKNOWN
Iteration Time:	 8.30s

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

Models       : 0+
Calls        : 57
Time         : 326.279s (Solving: 301.15s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 326.296s

Choices      : 6625028  (Domain: 6465748)
Conflicts    : 425698   (Analyzed: 425695)
Restarts     : 5249     (Average: 81.10 Last: 160)
Model-Level  : 291.0   
Problems     : 57       (Average Length: 72.70 Splits: 0)
Lemmas       : 425695   (Deleted: 400866)
  Binary     : 7534     (Ratio:   1.77%)
  Ternary    : 1685     (Ratio:   0.40%)
  Conflict   : 425695   (Average Length:  395.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 425695   (Average: 13.86 Max: 999 Sum: 5900939)
  Executed   : 425613   (Average: 13.85 Max: 999 Sum: 5897477 Ratio:  99.94%)
  Bounded    : 82       (Average: 42.22 Max: 102 Sum:   3462 Ratio:   0.06%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 741626   (Eliminated:    0 Frozen: 233385)
Constraints  : 5460361  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 7.00s
Memory:		 792MB (+4MB)
UNKNOWN
Iteration Time:	 8.29s

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

Models       : 0+
Calls        : 58
Time         : 330.279s (Solving: 305.00s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 330.296s

Choices      : 6675325  (Domain: 6516045)
Conflicts    : 433094   (Analyzed: 433091)
Restarts     : 5349     (Average: 80.97 Last: 160)
Model-Level  : 291.0   
Problems     : 58       (Average Length: 73.47 Splits: 0)
Lemmas       : 433091   (Deleted: 407881)
  Binary     : 7576     (Ratio:   1.75%)
  Ternary    : 1713     (Ratio:   0.40%)
  Conflict   : 433091   (Average Length:  392.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 433091   (Average: 13.72 Max: 999 Sum: 5943287)
  Executed   : 433005   (Average: 13.71 Max: 999 Sum: 5939821 Ratio:  99.94%)
  Bounded    : 86       (Average: 40.30 Max: 102 Sum:   3466 Ratio:   0.06%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 741626   (Eliminated:    0 Frozen: 233385)
Constraints  : 5460361  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 59
Time         : 334.243s (Solving: 308.80s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 334.264s

Choices      : 6718310  (Domain: 6558335)
Conflicts    : 440448   (Analyzed: 440445)
Restarts     : 5449     (Average: 80.83 Last: 160)
Model-Level  : 291.0   
Problems     : 59       (Average Length: 74.20 Splits: 0)
Lemmas       : 440445   (Deleted: 415167)
  Binary     : 7666     (Ratio:   1.74%)
  Ternary    : 1719     (Ratio:   0.39%)
  Conflict   : 440445   (Average Length:  393.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 440445   (Average: 13.56 Max: 999 Sum: 5974257)
  Executed   : 440359   (Average: 13.56 Max: 999 Sum: 5970791 Ratio:  99.94%)
  Bounded    : 86       (Average: 40.30 Max: 102 Sum:   3466 Ratio:   0.06%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 741626   (Eliminated:    0 Frozen: 233385)
Constraints  : 5460361  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 3.90s
Memory:		 792MB (+0MB)
UNKNOWN
Iteration Time:	 3.97s

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

Models       : 0+
Calls        : 60
Time         : 341.250s (Solving: 315.62s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 341.276s

Choices      : 6810511  (Domain: 6648160)
Conflicts    : 449717   (Analyzed: 449714)
Restarts     : 5549     (Average: 81.04 Last: 160)
Model-Level  : 291.0   
Problems     : 60       (Average Length: 74.92 Splits: 0)
Lemmas       : 449714   (Deleted: 424314)
  Binary     : 7791     (Ratio:   1.73%)
  Ternary    : 1726     (Ratio:   0.38%)
  Conflict   : 449714   (Average Length:  397.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 449714   (Average: 13.46 Max: 999 Sum: 6053861)
  Executed   : 449628   (Average: 13.45 Max: 999 Sum: 6050395 Ratio:  99.94%)
  Bounded    : 86       (Average: 40.30 Max: 102 Sum:   3466 Ratio:   0.06%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 741626   (Eliminated:    0 Frozen: 233385)
Constraints  : 5460361  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 6.94s
Memory:		 792MB (+0MB)
UNKNOWN
Iteration Time:	 7.01s

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

Models       : 0+
Calls        : 61
Time         : 343.603s (Solving: 317.83s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 343.632s

Choices      : 6841195  (Domain: 6678841)
Conflicts    : 456450   (Analyzed: 456447)
Restarts     : 5649     (Average: 80.80 Last: 160)
Model-Level  : 291.0   
Problems     : 61       (Average Length: 75.61 Splits: 0)
Lemmas       : 456447   (Deleted: 431239)
  Binary     : 7798     (Ratio:   1.71%)
  Ternary    : 1727     (Ratio:   0.38%)
  Conflict   : 456447   (Average Length:  394.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 456447   (Average: 13.31 Max: 999 Sum: 6074305)
  Executed   : 456361   (Average: 13.30 Max: 999 Sum: 6070839 Ratio:  99.94%)
  Bounded    : 86       (Average: 40.30 Max: 102 Sum:   3466 Ratio:   0.06%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 741626   (Eliminated:    0 Frozen: 233385)
Constraints  : 5460361  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 2.31s
Memory:		 792MB (+0MB)
UNKNOWN
Iteration Time:	 2.36s

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

Models       : 0+
Calls        : 62
Time         : 346.526s (Solving: 320.59s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 346.556s

Choices      : 6883798  (Domain: 6721135)
Conflicts    : 463753   (Analyzed: 463750)
Restarts     : 5749     (Average: 80.67 Last: 160)
Model-Level  : 291.0   
Problems     : 62       (Average Length: 76.27 Splits: 0)
Lemmas       : 463750   (Deleted: 437831)
  Binary     : 7817     (Ratio:   1.69%)
  Ternary    : 1732     (Ratio:   0.37%)
  Conflict   : 463750   (Average Length:  392.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 463750   (Average: 13.16 Max: 999 Sum: 6104616)
  Executed   : 463664   (Average: 13.16 Max: 999 Sum: 6101150 Ratio:  99.94%)
  Bounded    : 86       (Average: 40.30 Max: 102 Sum:   3466 Ratio:   0.06%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 741626   (Eliminated:    0 Frozen: 233385)
Constraints  : 5460361  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 2.87s
Memory:		 792MB (+0MB)
UNKNOWN
Iteration Time:	 2.93s

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

Models       : 0+
Calls        : 63
Time         : 350.705s (Solving: 324.60s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 350.736s

Choices      : 6970240  (Domain: 6806554)
Conflicts    : 471555   (Analyzed: 471552)
Restarts     : 5849     (Average: 80.62 Last: 160)
Model-Level  : 291.0   
Problems     : 63       (Average Length: 76.92 Splits: 0)
Lemmas       : 471552   (Deleted: 445025)
  Binary     : 7857     (Ratio:   1.67%)
  Ternary    : 1737     (Ratio:   0.37%)
  Conflict   : 471552   (Average Length:  390.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 471552   (Average: 13.11 Max: 999 Sum: 6179749)
  Executed   : 471466   (Average: 13.10 Max: 999 Sum: 6176283 Ratio:  99.94%)
  Bounded    : 86       (Average: 40.30 Max: 102 Sum:   3466 Ratio:   0.06%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 741626   (Eliminated:    0 Frozen: 233385)
Constraints  : 5460361  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 64
Time         : 357.813s (Solving: 331.52s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 357.848s

Choices      : 7149889  (Domain: 6983497)
Conflicts    : 480712   (Analyzed: 480709)
Restarts     : 5949     (Average: 80.81 Last: 160)
Model-Level  : 291.0   
Problems     : 64       (Average Length: 77.55 Splits: 0)
Lemmas       : 480709   (Deleted: 454790)
  Binary     : 7957     (Ratio:   1.66%)
  Ternary    : 1743     (Ratio:   0.36%)
  Conflict   : 480709   (Average Length:  392.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 480709   (Average: 13.20 Max: 999 Sum: 6343691)
  Executed   : 480623   (Average: 13.19 Max: 999 Sum: 6340225 Ratio:  99.95%)
  Bounded    : 86       (Average: 40.30 Max: 102 Sum:   3466 Ratio:   0.05%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 741626   (Eliminated:    0 Frozen: 233385)
Constraints  : 5460361  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 65
Time         : 366.578s (Solving: 340.13s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 366.616s

Choices      : 7451847  (Domain: 7282618)
Conflicts    : 490146   (Analyzed: 490143)
Restarts     : 6049     (Average: 81.03 Last: 160)
Model-Level  : 291.0   
Problems     : 65       (Average Length: 78.15 Splits: 0)
Lemmas       : 490143   (Deleted: 463646)
  Binary     : 8048     (Ratio:   1.64%)
  Ternary    : 1747     (Ratio:   0.36%)
  Conflict   : 490143   (Average Length:  396.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 490143   (Average: 13.52 Max: 999 Sum: 6625230)
  Executed   : 490057   (Average: 13.51 Max: 999 Sum: 6621764 Ratio:  99.95%)
  Bounded    : 86       (Average: 40.30 Max: 102 Sum:   3466 Ratio:   0.05%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 741626   (Eliminated:    0 Frozen: 233385)
Constraints  : 5460361  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 66
Time         : 375.273s (Solving: 348.68s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 375.316s

Choices      : 7729037  (Domain: 7557139)
Conflicts    : 499249   (Analyzed: 499246)
Restarts     : 6149     (Average: 81.19 Last: 160)
Model-Level  : 291.0   
Problems     : 66       (Average Length: 78.74 Splits: 0)
Lemmas       : 499246   (Deleted: 472822)
  Binary     : 8160     (Ratio:   1.63%)
  Ternary    : 1761     (Ratio:   0.35%)
  Conflict   : 499246   (Average Length:  401.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 499246   (Average: 13.78 Max: 999 Sum: 6880690)
  Executed   : 499160   (Average: 13.78 Max: 999 Sum: 6877224 Ratio:  99.95%)
  Bounded    : 86       (Average: 40.30 Max: 102 Sum:   3466 Ratio:   0.05%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 741626   (Eliminated:    0 Frozen: 233385)
Constraints  : 5460361  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 67
Time         : 384.974s (Solving: 358.20s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 385.020s

Choices      : 8135624  (Domain: 7961275)
Conflicts    : 508186   (Analyzed: 508183)
Restarts     : 6249     (Average: 81.32 Last: 160)
Model-Level  : 291.0   
Problems     : 67       (Average Length: 79.31 Splits: 0)
Lemmas       : 508183   (Deleted: 481658)
  Binary     : 8253     (Ratio:   1.62%)
  Ternary    : 1772     (Ratio:   0.35%)
  Conflict   : 508183   (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    : 508183   (Average: 14.29 Max: 999 Sum: 7261035)
  Executed   : 508097   (Average: 14.28 Max: 999 Sum: 7257569 Ratio:  99.95%)
  Bounded    : 86       (Average: 40.30 Max: 102 Sum:   3466 Ratio:   0.05%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 741626   (Eliminated:    0 Frozen: 233385)
Constraints  : 5460361  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 68
Time         : 391.283s (Solving: 364.36s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 391.332s

Choices      : 8358891  (Domain: 8183719)
Conflicts    : 516394   (Analyzed: 516391)
Restarts     : 6349     (Average: 81.33 Last: 160)
Model-Level  : 291.0   
Problems     : 68       (Average Length: 79.87 Splits: 0)
Lemmas       : 516391   (Deleted: 488392)
  Binary     : 8299     (Ratio:   1.61%)
  Ternary    : 1778     (Ratio:   0.34%)
  Conflict   : 516391   (Average Length:  409.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 516391   (Average: 14.45 Max: 999 Sum: 7460567)
  Executed   : 516305   (Average: 14.44 Max: 999 Sum: 7457101 Ratio:  99.95%)
  Bounded    : 86       (Average: 40.30 Max: 102 Sum:   3466 Ratio:   0.05%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 741626   (Eliminated:    0 Frozen: 233385)
Constraints  : 5460361  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 69
Time         : 395.456s (Solving: 368.35s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 395.508s

Choices      : 8547374  (Domain: 8371653)
Conflicts    : 523606   (Analyzed: 523603)
Restarts     : 6449     (Average: 81.19 Last: 160)
Model-Level  : 291.0   
Problems     : 69       (Average Length: 80.41 Splits: 0)
Lemmas       : 523603   (Deleted: 496282)
  Binary     : 8319     (Ratio:   1.59%)
  Ternary    : 1781     (Ratio:   0.34%)
  Conflict   : 523603   (Average Length:  408.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 523603   (Average: 14.57 Max: 1011 Sum: 7628564)
  Executed   : 523516   (Average: 14.56 Max: 1011 Sum: 7624981 Ratio:  99.95%)
  Bounded    : 87       (Average: 41.18 Max: 117 Sum:   3583 Ratio:   0.05%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 741626   (Eliminated:    0 Frozen: 233385)
Constraints  : 5460361  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 4.11s
Memory:		 792MB (+0MB)
UNKNOWN
Iteration Time:	 4.18s

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

Models       : 0+
Calls        : 70
Time         : 398.495s (Solving: 371.24s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 398.548s

Choices      : 8584425  (Domain: 8408704)
Conflicts    : 530809   (Analyzed: 530806)
Restarts     : 6549     (Average: 81.05 Last: 160)
Model-Level  : 291.0   
Problems     : 70       (Average Length: 80.93 Splits: 0)
Lemmas       : 530806   (Deleted: 503414)
  Binary     : 8324     (Ratio:   1.57%)
  Ternary    : 1789     (Ratio:   0.34%)
  Conflict   : 530806   (Average Length:  406.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 530806   (Average: 14.43 Max: 1011 Sum: 7660285)
  Executed   : 530719   (Average: 14.42 Max: 1011 Sum: 7656702 Ratio:  99.95%)
  Bounded    : 87       (Average: 41.18 Max: 117 Sum:   3583 Ratio:   0.05%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 741626   (Eliminated:    0 Frozen: 233385)
Constraints  : 5460347  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 2.99s
Memory:		 792MB (+0MB)
UNKNOWN
Iteration Time:	 3.04s

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

Models       : 0+
Calls        : 71
Time         : 400.798s (Solving: 373.40s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 400.852s

Choices      : 8616205  (Domain: 8440405)
Conflicts    : 537599   (Analyzed: 537596)
Restarts     : 6649     (Average: 80.85 Last: 160)
Model-Level  : 291.0   
Problems     : 71       (Average Length: 81.44 Splits: 0)
Lemmas       : 537596   (Deleted: 510494)
  Binary     : 8352     (Ratio:   1.55%)
  Ternary    : 1790     (Ratio:   0.33%)
  Conflict   : 537596   (Average Length:  403.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 537596   (Average: 14.29 Max: 1011 Sum: 7683308)
  Executed   : 537509   (Average: 14.29 Max: 1011 Sum: 7679725 Ratio:  99.95%)
  Bounded    : 87       (Average: 41.18 Max: 117 Sum:   3583 Ratio:   0.05%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 741626   (Eliminated:    0 Frozen: 233385)
Constraints  : 5460347  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 2.26s
Memory:		 792MB (+0MB)
UNKNOWN
Iteration Time:	 2.31s

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

Models       : 0+
Calls        : 72
Time         : 407.600s (Solving: 380.02s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 407.656s

Choices      : 8706632  (Domain: 8527482)
Conflicts    : 547139   (Analyzed: 547136)
Restarts     : 6749     (Average: 81.07 Last: 160)
Model-Level  : 291.0   
Problems     : 72       (Average Length: 81.93 Splits: 0)
Lemmas       : 547136   (Deleted: 519319)
  Binary     : 8401     (Ratio:   1.54%)
  Ternary    : 1800     (Ratio:   0.33%)
  Conflict   : 547136   (Average Length:  406.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 547136   (Average: 14.18 Max: 1011 Sum: 7760999)
  Executed   : 547049   (Average: 14.18 Max: 1011 Sum: 7757416 Ratio:  99.95%)
  Bounded    : 87       (Average: 41.18 Max: 117 Sum:   3583 Ratio:   0.05%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 741626   (Eliminated:    0 Frozen: 233385)
Constraints  : 5460347  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 73
Time         : 411.199s (Solving: 383.45s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 411.256s

Choices      : 8764610  (Domain: 8584645)
Conflicts    : 554711   (Analyzed: 554708)
Restarts     : 6849     (Average: 80.99 Last: 160)
Model-Level  : 291.0   
Problems     : 73       (Average Length: 82.41 Splits: 0)
Lemmas       : 554708   (Deleted: 526509)
  Binary     : 8433     (Ratio:   1.52%)
  Ternary    : 1802     (Ratio:   0.32%)
  Conflict   : 554708   (Average Length:  405.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 554708   (Average: 14.08 Max: 1011 Sum: 7807926)
  Executed   : 554621   (Average: 14.07 Max: 1011 Sum: 7804343 Ratio:  99.95%)
  Bounded    : 87       (Average: 41.18 Max: 117 Sum:   3583 Ratio:   0.05%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 741626   (Eliminated:    0 Frozen: 233385)
Constraints  : 5460347  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 3.54s
Memory:		 792MB (+0MB)
UNKNOWN
Iteration Time:	 3.60s

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

Models       : 0+
Calls        : 74
Time         : 417.590s (Solving: 389.66s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 417.652s

Choices      : 8897162  (Domain: 8715434)
Conflicts    : 563285   (Analyzed: 563282)
Restarts     : 6949     (Average: 81.06 Last: 160)
Model-Level  : 291.0   
Problems     : 74       (Average Length: 82.88 Splits: 0)
Lemmas       : 563282   (Deleted: 533925)
  Binary     : 8499     (Ratio:   1.51%)
  Ternary    : 1808     (Ratio:   0.32%)
  Conflict   : 563282   (Average Length:  407.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 563282   (Average: 14.07 Max: 1011 Sum: 7926001)
  Executed   : 563195   (Average: 14.06 Max: 1011 Sum: 7922418 Ratio:  99.95%)
  Bounded    : 87       (Average: 41.18 Max: 117 Sum:   3583 Ratio:   0.05%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 741626   (Eliminated:    0 Frozen: 233385)
Constraints  : 5460347  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 75
Time         : 424.295s (Solving: 396.20s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 424.360s

Choices      : 9041944  (Domain: 8857895)
Conflicts    : 572071   (Analyzed: 572068)
Restarts     : 7049     (Average: 81.16 Last: 160)
Model-Level  : 291.0   
Problems     : 75       (Average Length: 83.33 Splits: 0)
Lemmas       : 572068   (Deleted: 544407)
  Binary     : 8644     (Ratio:   1.51%)
  Ternary    : 1835     (Ratio:   0.32%)
  Conflict   : 572068   (Average Length:  411.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 572068   (Average: 14.08 Max: 1011 Sum: 8054083)
  Executed   : 571981   (Average: 14.07 Max: 1011 Sum: 8050500 Ratio:  99.96%)
  Bounded    : 87       (Average: 41.18 Max: 117 Sum:   3583 Ratio:   0.04%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 741626   (Eliminated:    0 Frozen: 233385)
Constraints  : 5460347  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 76
Time         : 428.017s (Solving: 399.76s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 428.084s

Choices      : 9118337  (Domain: 8933854)
Conflicts    : 579483   (Analyzed: 579480)
Restarts     : 7149     (Average: 81.06 Last: 160)
Model-Level  : 291.0   
Problems     : 76       (Average Length: 83.78 Splits: 0)
Lemmas       : 579480   (Deleted: 550812)
  Binary     : 8676     (Ratio:   1.50%)
  Ternary    : 1838     (Ratio:   0.32%)
  Conflict   : 579480   (Average Length:  410.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 579480   (Average: 14.01 Max: 1011 Sum: 8117614)
  Executed   : 579393   (Average: 14.00 Max: 1011 Sum: 8114031 Ratio:  99.96%)
  Bounded    : 87       (Average: 41.18 Max: 117 Sum:   3583 Ratio:   0.04%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 741626   (Eliminated:    0 Frozen: 233385)
Constraints  : 5460347  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 77
Time         : 432.608s (Solving: 404.19s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 432.676s

Choices      : 9227423  (Domain: 9042205)
Conflicts    : 587171   (Analyzed: 587168)
Restarts     : 7249     (Average: 81.00 Last: 160)
Model-Level  : 291.0   
Problems     : 77       (Average Length: 84.21 Splits: 0)
Lemmas       : 587168   (Deleted: 558093)
  Binary     : 8701     (Ratio:   1.48%)
  Ternary    : 1842     (Ratio:   0.31%)
  Conflict   : 587168   (Average Length:  409.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 587168   (Average: 13.99 Max: 1011 Sum: 8211810)
  Executed   : 587081   (Average: 13.98 Max: 1011 Sum: 8208227 Ratio:  99.96%)
  Bounded    : 87       (Average: 41.18 Max: 117 Sum:   3583 Ratio:   0.04%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 741626   (Eliminated:    0 Frozen: 233385)
Constraints  : 5460347  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 4.54s
Memory:		 792MB (+0MB)
UNKNOWN
Iteration Time:	 4.60s

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

Models       : 0+
Calls        : 78
Time         : 441.808s (Solving: 413.22s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 441.880s

Choices      : 9506943  (Domain: 9319925)
Conflicts    : 596145   (Analyzed: 596142)
Restarts     : 7349     (Average: 81.12 Last: 160)
Model-Level  : 291.0   
Problems     : 78       (Average Length: 84.63 Splits: 0)
Lemmas       : 596142   (Deleted: 567685)
  Binary     : 8838     (Ratio:   1.48%)
  Ternary    : 1848     (Ratio:   0.31%)
  Conflict   : 596142   (Average Length:  421.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 596142   (Average: 14.20 Max: 1011 Sum: 8464809)
  Executed   : 596055   (Average: 14.19 Max: 1011 Sum: 8461226 Ratio:  99.96%)
  Bounded    : 87       (Average: 41.18 Max: 117 Sum:   3583 Ratio:   0.04%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 741626   (Eliminated:    0 Frozen: 233385)
Constraints  : 5460347  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 9.14s
Memory:		 856MB (+64MB)
UNKNOWN
Iteration Time:	 9.21s

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

Models       : 0+
Calls        : 79
Time         : 451.370s (Solving: 422.59s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 451.444s

Choices      : 9854230  (Domain: 9665127)
Conflicts    : 605072   (Analyzed: 605069)
Restarts     : 7449     (Average: 81.23 Last: 160)
Model-Level  : 291.0   
Problems     : 79       (Average Length: 85.04 Splits: 0)
Lemmas       : 605069   (Deleted: 576375)
  Binary     : 8936     (Ratio:   1.48%)
  Ternary    : 1853     (Ratio:   0.31%)
  Conflict   : 605069   (Average Length:  428.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 605069   (Average: 14.52 Max: 1011 Sum: 8784142)
  Executed   : 604981   (Average: 14.51 Max: 1011 Sum: 8780442 Ratio:  99.96%)
  Bounded    : 88       (Average: 42.05 Max: 117 Sum:   3700 Ratio:   0.04%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 741626   (Eliminated:    0 Frozen: 233385)
Constraints  : 5460347  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 9.49s
Memory:		 856MB (+0MB)
UNKNOWN
Iteration Time:	 9.57s

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

Models       : 0+
Calls        : 80
Time         : 455.077s (Solving: 426.11s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 455.152s

Choices      : 9897383  (Domain: 9708280)
Conflicts    : 612414   (Analyzed: 612411)
Restarts     : 7549     (Average: 81.12 Last: 160)
Model-Level  : 291.0   
Problems     : 80       (Average Length: 85.44 Splits: 0)
Lemmas       : 612411   (Deleted: 582888)
  Binary     : 8959     (Ratio:   1.46%)
  Ternary    : 1875     (Ratio:   0.31%)
  Conflict   : 612411   (Average Length:  427.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 612411   (Average: 14.40 Max: 1011 Sum: 8821549)
  Executed   : 612323   (Average: 14.40 Max: 1011 Sum: 8817849 Ratio:  99.96%)
  Bounded    : 88       (Average: 42.05 Max: 117 Sum:   3700 Ratio:   0.04%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 741626   (Eliminated:    0 Frozen: 233385)
Constraints  : 5460333  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 3.64s
Memory:		 856MB (+0MB)
UNKNOWN
Iteration Time:	 3.71s

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

Models       : 0+
Calls        : 81
Time         : 462.462s (Solving: 433.31s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 462.540s

Choices      : 9960799  (Domain: 9770143)
Conflicts    : 621002   (Analyzed: 620999)
Restarts     : 7649     (Average: 81.19 Last: 160)
Model-Level  : 291.0   
Problems     : 81       (Average Length: 85.83 Splits: 0)
Lemmas       : 620999   (Deleted: 589991)
  Binary     : 9092     (Ratio:   1.46%)
  Ternary    : 1896     (Ratio:   0.31%)
  Conflict   : 620999   (Average Length:  439.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 620999   (Average: 14.28 Max: 1011 Sum: 8867117)
  Executed   : 620911   (Average: 14.27 Max: 1011 Sum: 8863417 Ratio:  99.96%)
  Bounded    : 88       (Average: 42.05 Max: 117 Sum:   3700 Ratio:   0.04%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 741626   (Eliminated:    0 Frozen: 233385)
Constraints  : 5460333  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 82
Time         : 469.534s (Solving: 440.24s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 469.612s

Choices      : 10049717 (Domain: 9857539)
Conflicts    : 629809   (Analyzed: 629806)
Restarts     : 7749     (Average: 81.28 Last: 160)
Model-Level  : 291.0   
Problems     : 82       (Average Length: 86.21 Splits: 0)
Lemmas       : 629806   (Deleted: 600554)
  Binary     : 9177     (Ratio:   1.46%)
  Ternary    : 1906     (Ratio:   0.30%)
  Conflict   : 629806   (Average Length:  444.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 629806   (Average: 14.19 Max: 1011 Sum: 8939387)
  Executed   : 629718   (Average: 14.19 Max: 1011 Sum: 8935687 Ratio:  99.96%)
  Bounded    : 88       (Average: 42.05 Max: 117 Sum:   3700 Ratio:   0.04%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 741626   (Eliminated:    0 Frozen: 233385)
Constraints  : 5460333  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 7.02s
Memory:		 856MB (+0MB)
UNKNOWN
Iteration Time:	 7.08s

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

Models       : 0+
Calls        : 83
Time         : 477.447s (Solving: 448.00s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 477.528s

Choices      : 10177612 (Domain: 9983303)
Conflicts    : 638976   (Analyzed: 638973)
Restarts     : 7849     (Average: 81.41 Last: 160)
Model-Level  : 291.0   
Problems     : 83       (Average Length: 86.58 Splits: 0)
Lemmas       : 638973   (Deleted: 609110)
  Binary     : 9413     (Ratio:   1.47%)
  Ternary    : 1944     (Ratio:   0.30%)
  Conflict   : 638973   (Average Length:  449.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 638973   (Average: 14.16 Max: 1011 Sum: 9047965)
  Executed   : 638885   (Average: 14.15 Max: 1011 Sum: 9044265 Ratio:  99.96%)
  Bounded    : 88       (Average: 42.05 Max: 117 Sum:   3700 Ratio:   0.04%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 741626   (Eliminated:    0 Frozen: 233385)
Constraints  : 5460333  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 84
Time         : 484.447s (Solving: 454.85s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 484.528s

Choices      : 10310834 (Domain: 10115443)
Conflicts    : 647724   (Analyzed: 647721)
Restarts     : 7949     (Average: 81.48 Last: 160)
Model-Level  : 291.0   
Problems     : 84       (Average Length: 86.94 Splits: 0)
Lemmas       : 647721   (Deleted: 617435)
  Binary     : 9784     (Ratio:   1.51%)
  Ternary    : 2093     (Ratio:   0.32%)
  Conflict   : 647721   (Average Length:  450.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 647721   (Average: 14.15 Max: 1011 Sum: 9166079)
  Executed   : 647633   (Average: 14.15 Max: 1011 Sum: 9162379 Ratio:  99.96%)
  Bounded    : 88       (Average: 42.05 Max: 117 Sum:   3700 Ratio:   0.04%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 741626   (Eliminated:    0 Frozen: 233385)
Constraints  : 5460333  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 6.95s
Memory:		 856MB (+0MB)
UNKNOWN
Iteration Time:	 7.00s

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

Models       : 0+
Calls        : 85
Time         : 494.590s (Solving: 464.85s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 494.676s

Choices      : 10510928 (Domain: 10314430)
Conflicts    : 657264   (Analyzed: 657261)
Restarts     : 8049     (Average: 81.66 Last: 160)
Model-Level  : 291.0   
Problems     : 85       (Average Length: 87.29 Splits: 0)
Lemmas       : 657261   (Deleted: 625298)
  Binary     : 10100    (Ratio:   1.54%)
  Ternary    : 2203     (Ratio:   0.34%)
  Conflict   : 657261   (Average Length:  456.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 657261   (Average: 14.22 Max: 1011 Sum: 9344389)
  Executed   : 657173   (Average: 14.21 Max: 1011 Sum: 9340689 Ratio:  99.96%)
  Bounded    : 88       (Average: 42.05 Max: 117 Sum:   3700 Ratio:   0.04%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 741626   (Eliminated:    0 Frozen: 233385)
Constraints  : 5460333  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 10.10s
Memory:		 856MB (+0MB)
UNKNOWN
Iteration Time:	 10.15s

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

Models       : 0+
Calls        : 86
Time         : 504.375s (Solving: 474.47s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 504.464s

Choices      : 10749514 (Domain: 10551627)
Conflicts    : 666247   (Analyzed: 666244)
Restarts     : 8149     (Average: 81.76 Last: 160)
Model-Level  : 291.0   
Problems     : 86       (Average Length: 87.64 Splits: 0)
Lemmas       : 666244   (Deleted: 634420)
  Binary     : 10225    (Ratio:   1.53%)
  Ternary    : 2247     (Ratio:   0.34%)
  Conflict   : 666244   (Average Length:  458.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 666244   (Average: 14.35 Max: 1011 Sum: 9560961)
  Executed   : 666156   (Average: 14.34 Max: 1011 Sum: 9557261 Ratio:  99.96%)
  Bounded    : 88       (Average: 42.05 Max: 117 Sum:   3700 Ratio:   0.04%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 741626   (Eliminated:    0 Frozen: 233385)
Constraints  : 5460333  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 9.73s
Memory:		 856MB (+0MB)
UNKNOWN
Iteration Time:	 9.79s

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

Models       : 0+
Calls        : 87
Time         : 514.712s (Solving: 484.66s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 514.804s

Choices      : 11042831 (Domain: 10843692)
Conflicts    : 675338   (Analyzed: 675335)
Restarts     : 8249     (Average: 81.87 Last: 160)
Model-Level  : 291.0   
Problems     : 87       (Average Length: 87.98 Splits: 0)
Lemmas       : 675335   (Deleted: 643102)
  Binary     : 10284    (Ratio:   1.52%)
  Ternary    : 2257     (Ratio:   0.33%)
  Conflict   : 675335   (Average Length:  462.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 675335   (Average: 14.55 Max: 1011 Sum: 9828195)
  Executed   : 675247   (Average: 14.55 Max: 1011 Sum: 9824495 Ratio:  99.96%)
  Bounded    : 88       (Average: 42.05 Max: 117 Sum:   3700 Ratio:   0.04%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 741626   (Eliminated:    0 Frozen: 233385)
Constraints  : 5460333  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 88
Time         : 519.142s (Solving: 488.90s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 519.236s

Choices      : 11080804 (Domain: 10881665)
Conflicts    : 682633   (Analyzed: 682630)
Restarts     : 8349     (Average: 81.76 Last: 160)
Model-Level  : 291.0   
Problems     : 88       (Average Length: 88.31 Splits: 0)
Lemmas       : 682630   (Deleted: 649897)
  Binary     : 10292    (Ratio:   1.51%)
  Ternary    : 2262     (Ratio:   0.33%)
  Conflict   : 682630   (Average Length:  461.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 682630   (Average: 14.44 Max: 1011 Sum: 9859342)
  Executed   : 682542   (Average: 14.44 Max: 1011 Sum: 9855642 Ratio:  99.96%)
  Bounded    : 88       (Average: 42.05 Max: 117 Sum:   3700 Ratio:   0.04%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 741626   (Eliminated:    0 Frozen: 233385)
Constraints  : 5460333  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 89
Time         : 529.047s (Solving: 498.66s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 529.144s

Choices      : 11143974 (Domain: 10943606)
Conflicts    : 691456   (Analyzed: 691453)
Restarts     : 8449     (Average: 81.84 Last: 160)
Model-Level  : 291.0   
Problems     : 89       (Average Length: 88.63 Splits: 0)
Lemmas       : 691453   (Deleted: 658902)
  Binary     : 10373    (Ratio:   1.50%)
  Ternary    : 2275     (Ratio:   0.33%)
  Conflict   : 691453   (Average Length:  470.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 691453   (Average: 14.33 Max: 1011 Sum: 9909459)
  Executed   : 691365   (Average: 14.33 Max: 1011 Sum: 9905759 Ratio:  99.96%)
  Bounded    : 88       (Average: 42.05 Max: 117 Sum:   3700 Ratio:   0.04%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 741626   (Eliminated:    0 Frozen: 233385)
Constraints  : 5460333  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 90
Time         : 535.933s (Solving: 505.36s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 536.032s

Choices      : 11212850 (Domain: 11011853)
Conflicts    : 699889   (Analyzed: 699886)
Restarts     : 8549     (Average: 81.87 Last: 160)
Model-Level  : 291.0   
Problems     : 90       (Average Length: 88.94 Splits: 0)
Lemmas       : 699886   (Deleted: 665326)
  Binary     : 10501    (Ratio:   1.50%)
  Ternary    : 2307     (Ratio:   0.33%)
  Conflict   : 699886   (Average Length:  472.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 699886   (Average: 14.24 Max: 1011 Sum: 9963003)
  Executed   : 699798   (Average: 14.23 Max: 1011 Sum: 9959303 Ratio:  99.96%)
  Bounded    : 88       (Average: 42.05 Max: 117 Sum:   3700 Ratio:   0.04%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 741626   (Eliminated:    0 Frozen: 233385)
Constraints  : 5460333  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 91
Time         : 545.574s (Solving: 514.82s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 545.680s

Choices      : 11375401 (Domain: 11172801)
Conflicts    : 709223   (Analyzed: 709220)
Restarts     : 8649     (Average: 82.00 Last: 160)
Model-Level  : 291.0   
Problems     : 91       (Average Length: 89.25 Splits: 0)
Lemmas       : 709220   (Deleted: 675591)
  Binary     : 10656    (Ratio:   1.50%)
  Ternary    : 2415     (Ratio:   0.34%)
  Conflict   : 709220   (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    : 709220   (Average: 14.25 Max: 1011 Sum: 10107810)
  Executed   : 709132   (Average: 14.25 Max: 1011 Sum: 10104110 Ratio:  99.96%)
  Bounded    : 88       (Average: 42.05 Max: 117 Sum:   3700 Ratio:   0.04%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 741626   (Eliminated:    0 Frozen: 233385)
Constraints  : 5460333  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 9.57s
Memory:		 856MB (+0MB)
UNKNOWN
Iteration Time:	 9.65s

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

Models       : 0+
Calls        : 92
Time         : 554.607s (Solving: 523.70s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 554.720s

Choices      : 11561438 (Domain: 11356988)
Conflicts    : 717858   (Analyzed: 717855)
Restarts     : 8749     (Average: 82.05 Last: 160)
Model-Level  : 291.0   
Problems     : 92       (Average Length: 89.55 Splits: 0)
Lemmas       : 717855   (Deleted: 684312)
  Binary     : 10791    (Ratio:   1.50%)
  Ternary    : 2467     (Ratio:   0.34%)
  Conflict   : 717855   (Average Length:  475.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 717855   (Average: 14.31 Max: 1011 Sum: 10273399)
  Executed   : 717767   (Average: 14.31 Max: 1011 Sum: 10269699 Ratio:  99.96%)
  Bounded    : 88       (Average: 42.05 Max: 117 Sum:   3700 Ratio:   0.04%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 741626   (Eliminated:    0 Frozen: 233385)
Constraints  : 5460333  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 8.99s
Memory:		 856MB (+0MB)
UNKNOWN
Iteration Time:	 9.04s

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

Models       : 0+
Calls        : 93
Time         : 565.471s (Solving: 534.42s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 565.588s

Choices      : 11779344 (Domain: 11572995)
Conflicts    : 726834   (Analyzed: 726831)
Restarts     : 8849     (Average: 82.14 Last: 160)
Model-Level  : 291.0   
Problems     : 93       (Average Length: 89.85 Splits: 0)
Lemmas       : 726831   (Deleted: 692563)
  Binary     : 10879    (Ratio:   1.50%)
  Ternary    : 2497     (Ratio:   0.34%)
  Conflict   : 726831   (Average Length:  482.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 726831   (Average: 14.40 Max: 1011 Sum: 10464371)
  Executed   : 726743   (Average: 14.39 Max: 1011 Sum: 10460671 Ratio:  99.96%)
  Bounded    : 88       (Average: 42.05 Max: 117 Sum:   3700 Ratio:   0.04%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 741626   (Eliminated:    0 Frozen: 233385)
Constraints  : 5460333  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 10.82s
Memory:		 856MB (+0MB)
UNKNOWN
Iteration Time:	 10.87s

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

Models       : 0+
Calls        : 94
Time         : 576.077s (Solving: 544.87s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 576.200s

Choices      : 12036160 (Domain: 11828443)
Conflicts    : 735893   (Analyzed: 735890)
Restarts     : 8949     (Average: 82.23 Last: 160)
Model-Level  : 291.0   
Problems     : 94       (Average Length: 90.14 Splits: 0)
Lemmas       : 735890   (Deleted: 701314)
  Binary     : 10992    (Ratio:   1.49%)
  Ternary    : 2551     (Ratio:   0.35%)
  Conflict   : 735890   (Average Length:  485.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 735890   (Average: 14.54 Max: 1011 Sum: 10698226)
  Executed   : 735802   (Average: 14.53 Max: 1011 Sum: 10694526 Ratio:  99.97%)
  Bounded    : 88       (Average: 42.05 Max: 117 Sum:   3700 Ratio:   0.03%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 741626   (Eliminated:    0 Frozen: 233385)
Constraints  : 5460333  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 10.56s
Memory:		 856MB (+0MB)
UNKNOWN
Iteration Time:	 10.61s

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

Models       : 0+
Calls        : 95
Time         : 588.776s (Solving: 557.40s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 588.908s

Choices      : 12383285 (Domain: 12173633)
Conflicts    : 744817   (Analyzed: 744814)
Restarts     : 9049     (Average: 82.31 Last: 160)
Model-Level  : 291.0   
Problems     : 95       (Average Length: 90.42 Splits: 0)
Lemmas       : 744814   (Deleted: 709739)
  Binary     : 11242    (Ratio:   1.51%)
  Ternary    : 2655     (Ratio:   0.36%)
  Conflict   : 744814   (Average Length:  493.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 744814   (Average: 14.79 Max: 1011 Sum: 11012693)
  Executed   : 744726   (Average: 14.78 Max: 1011 Sum: 11008993 Ratio:  99.97%)
  Bounded    : 88       (Average: 42.05 Max: 117 Sum:   3700 Ratio:   0.03%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 741626   (Eliminated:    0 Frozen: 233385)
Constraints  : 5460333  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 12.64s
Memory:		 856MB (+0MB)
UNKNOWN
Iteration Time:	 12.71s

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

Models       : 0+
Calls        : 96
Time         : 592.571s (Solving: 561.04s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 592.704s

Choices      : 12425344 (Domain: 12215692)
Conflicts    : 752440   (Analyzed: 752437)
Restarts     : 9149     (Average: 82.24 Last: 160)
Model-Level  : 291.0   
Problems     : 96       (Average Length: 90.70 Splits: 0)
Lemmas       : 752437   (Deleted: 716260)
  Binary     : 11255    (Ratio:   1.50%)
  Ternary    : 2662     (Ratio:   0.35%)
  Conflict   : 752437   (Average Length:  490.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 752437   (Average: 14.68 Max: 1011 Sum: 11048080)
  Executed   : 752349   (Average: 14.68 Max: 1011 Sum: 11044380 Ratio:  99.97%)
  Bounded    : 88       (Average: 42.05 Max: 117 Sum:   3700 Ratio:   0.03%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 741626   (Eliminated:    0 Frozen: 233385)
Constraints  : 5460333  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 3.74s
Memory:		 856MB (+0MB)
UNKNOWN
Iteration Time:	 3.80s

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

Models       : 0+
Calls        : 97
Time         : 602.953s (Solving: 571.25s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 603.092s

Choices      : 12476217 (Domain: 12266565)
Conflicts    : 761194   (Analyzed: 761191)
Restarts     : 9249     (Average: 82.30 Last: 160)
Model-Level  : 291.0   
Problems     : 97       (Average Length: 90.97 Splits: 0)
Lemmas       : 761191   (Deleted: 725648)
  Binary     : 11324    (Ratio:   1.49%)
  Ternary    : 2672     (Ratio:   0.35%)
  Conflict   : 761191   (Average Length:  500.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 761191   (Average: 14.56 Max: 1011 Sum: 11086706)
  Executed   : 761103   (Average: 14.56 Max: 1011 Sum: 11083006 Ratio:  99.97%)
  Bounded    : 88       (Average: 42.05 Max: 117 Sum:   3700 Ratio:   0.03%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 741626   (Eliminated:    0 Frozen: 233385)
Constraints  : 5460333  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 10.32s
Memory:		 856MB (+0MB)
UNKNOWN
Iteration Time:	 10.39s

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

Models       : 0+
Calls        : 98
Time         : 612.194s (Solving: 580.30s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 612.336s

Choices      : 12550464 (Domain: 12340471)
Conflicts    : 769814   (Analyzed: 769811)
Restarts     : 9349     (Average: 82.34 Last: 160)
Model-Level  : 291.0   
Problems     : 98       (Average Length: 91.23 Splits: 0)
Lemmas       : 769811   (Deleted: 733929)
  Binary     : 11434    (Ratio:   1.49%)
  Ternary    : 2696     (Ratio:   0.35%)
  Conflict   : 769811   (Average Length:  504.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 769811   (Average: 14.47 Max: 1011 Sum: 11142794)
  Executed   : 769723   (Average: 14.47 Max: 1011 Sum: 11139094 Ratio:  99.97%)
  Bounded    : 88       (Average: 42.05 Max: 117 Sum:   3700 Ratio:   0.03%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 741626   (Eliminated:    0 Frozen: 233385)
Constraints  : 5460333  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 99
Time         : 622.266s (Solving: 590.23s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 622.412s

Choices      : 12634890 (Domain: 12423829)
Conflicts    : 778392   (Analyzed: 778389)
Restarts     : 9449     (Average: 82.38 Last: 185)
Model-Level  : 291.0   
Problems     : 99       (Average Length: 91.49 Splits: 0)
Lemmas       : 778389   (Deleted: 740178)
  Binary     : 11528    (Ratio:   1.48%)
  Ternary    : 2713     (Ratio:   0.35%)
  Conflict   : 778389   (Average Length:  512.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 778389   (Average: 14.40 Max: 1011 Sum: 11206701)
  Executed   : 778301   (Average: 14.39 Max: 1011 Sum: 11203001 Ratio:  99.97%)
  Bounded    : 88       (Average: 42.05 Max: 117 Sum:   3700 Ratio:   0.03%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 741626   (Eliminated:    0 Frozen: 233385)
Constraints  : 5460333  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 10.02s
Memory:		 856MB (+0MB)
UNKNOWN
Iteration Time:	 10.08s

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

Models       : 0+
Calls        : 100
Time         : 631.332s (Solving: 599.13s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 631.480s

Choices      : 12731011 (Domain: 12518941)
Conflicts    : 787336   (Analyzed: 787333)
Restarts     : 9549     (Average: 82.45 Last: 185)
Model-Level  : 291.0   
Problems     : 100      (Average Length: 91.75 Splits: 0)
Lemmas       : 787333   (Deleted: 750632)
  Binary     : 11609    (Ratio:   1.47%)
  Ternary    : 2747     (Ratio:   0.35%)
  Conflict   : 787333   (Average Length:  516.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 787333   (Average: 14.34 Max: 1011 Sum: 11286470)
  Executed   : 787245   (Average: 14.33 Max: 1011 Sum: 11282770 Ratio:  99.97%)
  Bounded    : 88       (Average: 42.05 Max: 117 Sum:   3700 Ratio:   0.03%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 741626   (Eliminated:    0 Frozen: 233385)
Constraints  : 5460333  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 101
Time         : 642.988s (Solving: 610.62s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 643.140s

Choices      : 12889554 (Domain: 12676127)
Conflicts    : 796225   (Analyzed: 796222)
Restarts     : 9649     (Average: 82.52 Last: 185)
Model-Level  : 291.0   
Problems     : 101      (Average Length: 92.00 Splits: 0)
Lemmas       : 796222   (Deleted: 759241)
  Binary     : 11711    (Ratio:   1.47%)
  Ternary    : 2775     (Ratio:   0.35%)
  Conflict   : 796222   (Average Length:  521.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 796222   (Average: 14.35 Max: 1011 Sum: 11424823)
  Executed   : 796134   (Average: 14.34 Max: 1011 Sum: 11421123 Ratio:  99.97%)
  Bounded    : 88       (Average: 42.05 Max: 117 Sum:   3700 Ratio:   0.03%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 741626   (Eliminated:    0 Frozen: 233385)
Constraints  : 5460333  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 11.60s
Memory:		 856MB (+0MB)
UNKNOWN
Iteration Time:	 11.66s

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

Models       : 0+
Calls        : 102
Time         : 654.984s (Solving: 622.45s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 655.140s

Choices      : 13073395 (Domain: 12858242)
Conflicts    : 805509   (Analyzed: 805506)
Restarts     : 9749     (Average: 82.62 Last: 185)
Model-Level  : 291.0   
Problems     : 102      (Average Length: 92.25 Splits: 0)
Lemmas       : 805506   (Deleted: 767849)
  Binary     : 11784    (Ratio:   1.46%)
  Ternary    : 2791     (Ratio:   0.35%)
  Conflict   : 805506   (Average Length:  527.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 805506   (Average: 14.38 Max: 1011 Sum: 11585898)
  Executed   : 805418   (Average: 14.38 Max: 1011 Sum: 11582198 Ratio:  99.97%)
  Bounded    : 88       (Average: 42.05 Max: 117 Sum:   3700 Ratio:   0.03%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 741626   (Eliminated:    0 Frozen: 233385)
Constraints  : 5460333  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 11.94s
Memory:		 856MB (+0MB)
UNKNOWN
Iteration Time:	 12.01s

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

Models       : 0+
Calls        : 103
Time         : 665.806s (Solving: 633.08s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 665.968s

Choices      : 13298341 (Domain: 13082225)
Conflicts    : 814277   (Analyzed: 814274)
Restarts     : 9849     (Average: 82.68 Last: 185)
Model-Level  : 291.0   
Problems     : 103      (Average Length: 92.49 Splits: 0)
Lemmas       : 814274   (Deleted: 776875)
  Binary     : 11846    (Ratio:   1.45%)
  Ternary    : 2806     (Ratio:   0.34%)
  Conflict   : 814274   (Average Length:  530.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 814274   (Average: 14.48 Max: 1011 Sum: 11786709)
  Executed   : 814186   (Average: 14.47 Max: 1011 Sum: 11783009 Ratio:  99.97%)
  Bounded    : 88       (Average: 42.05 Max: 117 Sum:   3700 Ratio:   0.03%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 741626   (Eliminated:    0 Frozen: 233385)
Constraints  : 5460333  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 104
Time         : 679.764s (Solving: 646.88s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 679.932s

Choices      : 13601067 (Domain: 13383496)
Conflicts    : 824182   (Analyzed: 824179)
Restarts     : 9949     (Average: 82.84 Last: 185)
Model-Level  : 291.0   
Problems     : 104      (Average Length: 92.72 Splits: 0)
Lemmas       : 824179   (Deleted: 785382)
  Binary     : 11918    (Ratio:   1.45%)
  Ternary    : 2831     (Ratio:   0.34%)
  Conflict   : 824179   (Average Length:  536.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 824179   (Average: 14.63 Max: 1011 Sum: 12058041)
  Executed   : 824091   (Average: 14.63 Max: 1011 Sum: 12054341 Ratio:  99.97%)
  Bounded    : 88       (Average: 42.05 Max: 117 Sum:   3700 Ratio:   0.03%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 741626   (Eliminated:    0 Frozen: 233385)
Constraints  : 5460333  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 13.90s
Memory:		 856MB (+0MB)
UNKNOWN
Iteration Time:	 13.97s

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

Models       : 0+
Calls        : 105
Time         : 694.155s (Solving: 661.12s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 694.328s

Choices      : 14136061 (Domain: 13914727)
Conflicts    : 833065   (Analyzed: 833062)
Restarts     : 10049    (Average: 82.90 Last: 185)
Model-Level  : 291.0   
Problems     : 105      (Average Length: 92.95 Splits: 0)
Lemmas       : 833062   (Deleted: 794675)
  Binary     : 12313    (Ratio:   1.48%)
  Ternary    : 2921     (Ratio:   0.35%)
  Conflict   : 833062   (Average Length:  541.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 833062   (Average: 15.06 Max: 1011 Sum: 12549862)
  Executed   : 832974   (Average: 15.06 Max: 1011 Sum: 12546162 Ratio:  99.97%)
  Bounded    : 88       (Average: 42.05 Max: 117 Sum:   3700 Ratio:   0.03%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 741626   (Eliminated:    0 Frozen: 233385)
Constraints  : 5460333  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 14.35s
Memory:		 856MB (+0MB)
UNKNOWN
Iteration Time:	 14.40s

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

Models       : 0+
Calls        : 106
Time         : 699.212s (Solving: 666.00s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 699.388s

Choices      : 14189950 (Domain: 13968616)
Conflicts    : 841389   (Analyzed: 841386)
Restarts     : 10149    (Average: 82.90 Last: 185)
Model-Level  : 291.0   
Problems     : 106      (Average Length: 93.18 Splits: 0)
Lemmas       : 841386   (Deleted: 800892)
  Binary     : 12367    (Ratio:   1.47%)
  Ternary    : 2949     (Ratio:   0.35%)
  Conflict   : 841386   (Average Length:  541.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 841386   (Average: 14.98 Max: 1011 Sum: 12599839)
  Executed   : 841298   (Average: 14.97 Max: 1011 Sum: 12596139 Ratio:  99.97%)
  Bounded    : 88       (Average: 42.05 Max: 117 Sum:   3700 Ratio:   0.03%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 741626   (Eliminated:    0 Frozen: 233385)
Constraints  : 5460333  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 107
Time         : 702.570s (Solving: 669.19s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 702.748s

Choices      : 14220017 (Domain: 13998683)
Conflicts    : 848489   (Analyzed: 848486)
Restarts     : 10249    (Average: 82.79 Last: 185)
Model-Level  : 291.0   
Problems     : 107      (Average Length: 93.40 Splits: 0)
Lemmas       : 848486   (Deleted: 809062)
  Binary     : 12367    (Ratio:   1.46%)
  Ternary    : 2951     (Ratio:   0.35%)
  Conflict   : 848486   (Average Length:  539.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 848486   (Average: 14.87 Max: 1011 Sum: 12619752)
  Executed   : 848398   (Average: 14.87 Max: 1011 Sum: 12616052 Ratio:  99.97%)
  Bounded    : 88       (Average: 42.05 Max: 117 Sum:   3700 Ratio:   0.03%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 741626   (Eliminated:    0 Frozen: 233385)
Constraints  : 5460333  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 3.30s
Memory:		 856MB (+0MB)
UNKNOWN
Iteration Time:	 3.36s

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

Models       : 0+
Calls        : 108
Time         : 714.444s (Solving: 680.90s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 714.628s

Choices      : 14289903 (Domain: 14068569)
Conflicts    : 856754   (Analyzed: 856751)
Restarts     : 10349    (Average: 82.79 Last: 185)
Model-Level  : 291.0   
Problems     : 108      (Average Length: 93.62 Splits: 0)
Lemmas       : 856751   (Deleted: 815914)
  Binary     : 12436    (Ratio:   1.45%)
  Ternary    : 2974     (Ratio:   0.35%)
  Conflict   : 856751   (Average Length:  544.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 856751   (Average: 14.79 Max: 1011 Sum: 12675086)
  Executed   : 856663   (Average: 14.79 Max: 1011 Sum: 12671386 Ratio:  99.97%)
  Bounded    : 88       (Average: 42.05 Max: 117 Sum:   3700 Ratio:   0.03%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 741626   (Eliminated:    0 Frozen: 233385)
Constraints  : 5460333  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 11.82s
Memory:		 856MB (+0MB)
UNKNOWN
Iteration Time:	 11.88s

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

Models       : 0+
Calls        : 109
Time         : 723.411s (Solving: 689.71s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 723.600s

Choices      : 14389096 (Domain: 14167023)
Conflicts    : 865079   (Analyzed: 865076)
Restarts     : 10449    (Average: 82.79 Last: 185)
Model-Level  : 291.0   
Problems     : 109      (Average Length: 93.83 Splits: 0)
Lemmas       : 865076   (Deleted: 823890)
  Binary     : 12515    (Ratio:   1.45%)
  Ternary    : 2985     (Ratio:   0.35%)
  Conflict   : 865076   (Average Length:  546.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 865076   (Average: 14.75 Max: 1011 Sum: 12759112)
  Executed   : 864987   (Average: 14.74 Max: 1011 Sum: 12755295 Ratio:  99.97%)
  Bounded    : 89       (Average: 42.89 Max: 117 Sum:   3817 Ratio:   0.03%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 741626   (Eliminated:    0 Frozen: 233385)
Constraints  : 5460333  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 110
Time         : 734.020s (Solving: 700.14s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 734.216s

Choices      : 14518003 (Domain: 14294805)
Conflicts    : 873984   (Analyzed: 873981)
Restarts     : 10549    (Average: 82.85 Last: 185)
Model-Level  : 291.0   
Problems     : 110      (Average Length: 94.05 Splits: 0)
Lemmas       : 873981   (Deleted: 834005)
  Binary     : 12639    (Ratio:   1.45%)
  Ternary    : 3011     (Ratio:   0.34%)
  Conflict   : 873981   (Average Length:  549.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 873981   (Average: 14.73 Max: 1011 Sum: 12869610)
  Executed   : 873892   (Average: 14.72 Max: 1011 Sum: 12865793 Ratio:  99.97%)
  Bounded    : 89       (Average: 42.89 Max: 117 Sum:   3817 Ratio:   0.03%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 741626   (Eliminated:    0 Frozen: 233385)
Constraints  : 5460319  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 10.55s
Memory:		 856MB (+0MB)
UNKNOWN
Iteration Time:	 10.62s

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

Models       : 0+
Calls        : 111
Time         : 744.111s (Solving: 710.08s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 744.308s

Choices      : 14669582 (Domain: 14445763)
Conflicts    : 882288   (Analyzed: 882285)
Restarts     : 10649    (Average: 82.85 Last: 185)
Model-Level  : 291.0   
Problems     : 111      (Average Length: 94.25 Splits: 0)
Lemmas       : 882285   (Deleted: 840536)
  Binary     : 12749    (Ratio:   1.44%)
  Ternary    : 3035     (Ratio:   0.34%)
  Conflict   : 882285   (Average Length:  551.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 882285   (Average: 14.74 Max: 1011 Sum: 13001583)
  Executed   : 882196   (Average: 14.73 Max: 1011 Sum: 12997766 Ratio:  99.97%)
  Bounded    : 89       (Average: 42.89 Max: 117 Sum:   3817 Ratio:   0.03%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 741626   (Eliminated:    0 Frozen: 233385)
Constraints  : 5460319  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 10.04s
Memory:		 856MB (+0MB)
UNKNOWN
Iteration Time:	 10.10s

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

Models       : 0+
Calls        : 112
Time         : 755.204s (Solving: 720.98s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 755.404s

Choices      : 14869182 (Domain: 14643769)
Conflicts    : 891259   (Analyzed: 891256)
Restarts     : 10749    (Average: 82.92 Last: 185)
Model-Level  : 291.0   
Problems     : 112      (Average Length: 94.46 Splits: 0)
Lemmas       : 891256   (Deleted: 850601)
  Binary     : 12882    (Ratio:   1.45%)
  Ternary    : 3061     (Ratio:   0.34%)
  Conflict   : 891256   (Average Length:  553.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 891256   (Average: 14.79 Max: 1011 Sum: 13178928)
  Executed   : 891167   (Average: 14.78 Max: 1011 Sum: 13175111 Ratio:  99.97%)
  Bounded    : 89       (Average: 42.89 Max: 117 Sum:   3817 Ratio:   0.03%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 741626   (Eliminated:    0 Frozen: 233385)
Constraints  : 5460319  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 11.02s
Memory:		 856MB (+0MB)
UNKNOWN
Iteration Time:	 11.10s

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

Models       : 0+
Calls        : 113
Time         : 767.032s (Solving: 732.66s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 767.236s

Choices      : 15074052 (Domain: 14847857)
Conflicts    : 899942   (Analyzed: 899939)
Restarts     : 10849    (Average: 82.95 Last: 185)
Model-Level  : 291.0   
Problems     : 113      (Average Length: 94.65 Splits: 0)
Lemmas       : 899939   (Deleted: 859207)
  Binary     : 12985    (Ratio:   1.44%)
  Ternary    : 3073     (Ratio:   0.34%)
  Conflict   : 899939   (Average Length:  560.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 899939   (Average: 14.84 Max: 1011 Sum: 13351913)
  Executed   : 899850   (Average: 14.83 Max: 1011 Sum: 13348096 Ratio:  99.97%)
  Bounded    : 89       (Average: 42.89 Max: 117 Sum:   3817 Ratio:   0.03%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 741626   (Eliminated:    0 Frozen: 233385)
Constraints  : 5460319  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 11.78s
Memory:		 856MB (+0MB)
UNKNOWN
Iteration Time:	 11.84s

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

Models       : 0+
Calls        : 114
Time         : 778.057s (Solving: 743.50s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 778.264s

Choices      : 15313699 (Domain: 15087153)
Conflicts    : 908982   (Analyzed: 908979)
Restarts     : 10949    (Average: 83.02 Last: 185)
Model-Level  : 291.0   
Problems     : 114      (Average Length: 94.85 Splits: 0)
Lemmas       : 908979   (Deleted: 867719)
  Binary     : 13019    (Ratio:   1.43%)
  Ternary    : 3084     (Ratio:   0.34%)
  Conflict   : 908979   (Average Length:  561.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 908979   (Average: 14.92 Max: 1011 Sum: 13564208)
  Executed   : 908890   (Average: 14.92 Max: 1011 Sum: 13560391 Ratio:  99.97%)
  Bounded    : 89       (Average: 42.89 Max: 117 Sum:   3817 Ratio:   0.03%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 741626   (Eliminated:    0 Frozen: 233385)
Constraints  : 5460319  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 10.96s
Memory:		 856MB (+0MB)
UNKNOWN
Iteration Time:	 11.03s

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

Models       : 0+
Calls        : 115
Time         : 783.137s (Solving: 748.42s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 783.348s

Choices      : 15369340 (Domain: 15142794)
Conflicts    : 917429   (Analyzed: 917426)
Restarts     : 11049    (Average: 83.03 Last: 185)
Model-Level  : 291.0   
Problems     : 115      (Average Length: 95.04 Splits: 0)
Lemmas       : 917426   (Deleted: 874288)
  Binary     : 13082    (Ratio:   1.43%)
  Ternary    : 3106     (Ratio:   0.34%)
  Conflict   : 917426   (Average Length:  559.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 917426   (Average: 14.84 Max: 1011 Sum: 13613318)
  Executed   : 917337   (Average: 14.83 Max: 1011 Sum: 13609501 Ratio:  99.97%)
  Bounded    : 89       (Average: 42.89 Max: 117 Sum:   3817 Ratio:   0.03%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 741626   (Eliminated:    0 Frozen: 233385)
Constraints  : 5460319  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 5.02s
Memory:		 856MB (+0MB)
UNKNOWN
Iteration Time:	 5.08s

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

Models       : 0+
Calls        : 116
Time         : 796.581s (Solving: 761.72s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 796.800s

Choices      : 15417683 (Domain: 15191137)
Conflicts    : 926415   (Analyzed: 926412)
Restarts     : 11149    (Average: 83.09 Last: 185)
Model-Level  : 291.0   
Problems     : 116      (Average Length: 95.23 Splits: 0)
Lemmas       : 926412   (Deleted: 884648)
  Binary     : 13147    (Ratio:   1.42%)
  Ternary    : 3111     (Ratio:   0.34%)
  Conflict   : 926412   (Average Length:  568.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 926412   (Average: 14.73 Max: 1011 Sum: 13648016)
  Executed   : 926323   (Average: 14.73 Max: 1011 Sum: 13644199 Ratio:  99.97%)
  Bounded    : 89       (Average: 42.89 Max: 117 Sum:   3817 Ratio:   0.03%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 741626   (Eliminated:    0 Frozen: 233385)
Constraints  : 5460319  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 13.40s
Memory:		 856MB (+0MB)
UNKNOWN
Iteration Time:	 13.45s

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

Models       : 0+
Calls        : 117
Time         : 812.311s (Solving: 777.26s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 812.540s

Choices      : 15491498 (Domain: 15264952)
Conflicts    : 935369   (Analyzed: 935366)
Restarts     : 11249    (Average: 83.15 Last: 185)
Model-Level  : 291.0   
Problems     : 117      (Average Length: 95.42 Splits: 0)
Lemmas       : 935366   (Deleted: 893274)
  Binary     : 13217    (Ratio:   1.41%)
  Ternary    : 3119     (Ratio:   0.33%)
  Conflict   : 935366   (Average Length:  581.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 935366   (Average: 14.65 Max: 1011 Sum: 13705304)
  Executed   : 935277   (Average: 14.65 Max: 1011 Sum: 13701487 Ratio:  99.97%)
  Bounded    : 89       (Average: 42.89 Max: 117 Sum:   3817 Ratio:   0.03%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 741626   (Eliminated:    0 Frozen: 233385)
Constraints  : 5460319  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 15.66s
Memory:		 856MB (+0MB)
UNKNOWN
Iteration Time:	 15.74s

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

Models       : 0+
Calls        : 118
Time         : 819.230s (Solving: 784.01s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 819.464s

Choices      : 15566960 (Domain: 15340102)
Conflicts    : 943188   (Analyzed: 943185)
Restarts     : 11349    (Average: 83.11 Last: 185)
Model-Level  : 291.0   
Problems     : 118      (Average Length: 95.60 Splits: 0)
Lemmas       : 943185   (Deleted: 899758)
  Binary     : 13308    (Ratio:   1.41%)
  Ternary    : 3128     (Ratio:   0.33%)
  Conflict   : 943185   (Average Length:  584.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 943185   (Average: 14.59 Max: 1011 Sum: 13759682)
  Executed   : 943096   (Average: 14.58 Max: 1011 Sum: 13755865 Ratio:  99.97%)
  Bounded    : 89       (Average: 42.89 Max: 117 Sum:   3817 Ratio:   0.03%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 741626   (Eliminated:    0 Frozen: 233385)
Constraints  : 5460319  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 119
Time         : 830.505s (Solving: 795.10s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 830.748s

Choices      : 15741388 (Domain: 15513188)
Conflicts    : 952533   (Analyzed: 952530)
Restarts     : 11449    (Average: 83.20 Last: 185)
Model-Level  : 291.0   
Problems     : 119      (Average Length: 95.78 Splits: 0)
Lemmas       : 952530   (Deleted: 909477)
  Binary     : 13505    (Ratio:   1.42%)
  Ternary    : 3189     (Ratio:   0.33%)
  Conflict   : 952530   (Average Length:  585.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 952530   (Average: 14.61 Max: 1011 Sum: 13914452)
  Executed   : 952441   (Average: 14.60 Max: 1011 Sum: 13910635 Ratio:  99.97%)
  Bounded    : 89       (Average: 42.89 Max: 117 Sum:   3817 Ratio:   0.03%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 741626   (Eliminated:    0 Frozen: 233385)
Constraints  : 5460319  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 11.21s
Memory:		 856MB (+0MB)
UNKNOWN
Iteration Time:	 11.28s

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

Models       : 0+
Calls        : 120
Time         : 840.488s (Solving: 804.92s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 840.736s

Choices      : 15891254 (Domain: 15661644)
Conflicts    : 960833   (Analyzed: 960830)
Restarts     : 11549    (Average: 83.20 Last: 185)
Model-Level  : 291.0   
Problems     : 120      (Average Length: 95.96 Splits: 0)
Lemmas       : 960830   (Deleted: 916280)
  Binary     : 13668    (Ratio:   1.42%)
  Ternary    : 3209     (Ratio:   0.33%)
  Conflict   : 960830   (Average Length:  588.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 960830   (Average: 14.61 Max: 1011 Sum: 14039943)
  Executed   : 960741   (Average: 14.61 Max: 1011 Sum: 14036126 Ratio:  99.97%)
  Bounded    : 89       (Average: 42.89 Max: 117 Sum:   3817 Ratio:   0.03%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 741626   (Eliminated:    0 Frozen: 233385)
Constraints  : 5460319  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 9.93s
Memory:		 856MB (+0MB)
UNKNOWN
Iteration Time:	 9.99s

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

Models       : 0+
Calls        : 121
Time         : 851.035s (Solving: 815.29s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 851.288s

Choices      : 16070283 (Domain: 15840248)
Conflicts    : 969760   (Analyzed: 969757)
Restarts     : 11649    (Average: 83.25 Last: 185)
Model-Level  : 291.0   
Problems     : 121      (Average Length: 96.13 Splits: 0)
Lemmas       : 969757   (Deleted: 926447)
  Binary     : 13742    (Ratio:   1.42%)
  Ternary    : 3219     (Ratio:   0.33%)
  Conflict   : 969757   (Average Length:  591.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 969757   (Average: 14.64 Max: 1011 Sum: 14196737)
  Executed   : 969668   (Average: 14.64 Max: 1011 Sum: 14192920 Ratio:  99.97%)
  Bounded    : 89       (Average: 42.89 Max: 117 Sum:   3817 Ratio:   0.03%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 741626   (Eliminated:    0 Frozen: 233385)
Constraints  : 5460319  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 10.48s
Memory:		 856MB (+0MB)
UNKNOWN
Iteration Time:	 10.55s

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

Models       : 0+
Calls        : 122
Time         : 862.234s (Solving: 826.32s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 862.492s

Choices      : 16274017 (Domain: 16043486)
Conflicts    : 978109   (Analyzed: 978106)
Restarts     : 11749    (Average: 83.25 Last: 185)
Model-Level  : 291.0   
Problems     : 122      (Average Length: 96.30 Splits: 0)
Lemmas       : 978106   (Deleted: 933003)
  Binary     : 13827    (Ratio:   1.41%)
  Ternary    : 3229     (Ratio:   0.33%)
  Conflict   : 978106   (Average Length:  594.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 978106   (Average: 14.70 Max: 1011 Sum: 14373972)
  Executed   : 978017   (Average: 14.69 Max: 1011 Sum: 14370155 Ratio:  99.97%)
  Bounded    : 89       (Average: 42.89 Max: 117 Sum:   3817 Ratio:   0.03%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 741626   (Eliminated:    0 Frozen: 233385)
Constraints  : 5460319  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 11.14s
Memory:		 856MB (+0MB)
UNKNOWN
Iteration Time:	 11.21s

Iteration 122
Queue:		 [(4,20,11,True), (5,25,11,True), (6,30,10,True), (7,35,9,True), (8,40,8,True), (9,45,7,True), (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,False), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,2,True)]
Grounded Until:	 115
Blocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 123
Time         : 867.444s (Solving: 831.33s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 867.704s

Choices      : 16326291 (Domain: 16095760)
Conflicts    : 986456   (Analyzed: 986453)
Restarts     : 11849    (Average: 83.25 Last: 185)
Model-Level  : 291.0   
Problems     : 123      (Average Length: 96.47 Splits: 0)
Lemmas       : 986453   (Deleted: 941027)
  Binary     : 13876    (Ratio:   1.41%)
  Ternary    : 3256     (Ratio:   0.33%)
  Conflict   : 986453   (Average Length:  592.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 986453   (Average: 14.62 Max: 1011 Sum: 14421559)
  Executed   : 986364   (Average: 14.62 Max: 1011 Sum: 14417742 Ratio:  99.97%)
  Bounded    : 89       (Average: 42.89 Max: 117 Sum:   3817 Ratio:   0.03%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 741626   (Eliminated:    0 Frozen: 233385)
Constraints  : 5460319  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 5.14s
Memory:		 856MB (+0MB)
UNKNOWN
Iteration Time:	 5.22s

Iteration 123
Queue:		 [(5,25,11,True), (6,30,10,True), (7,35,9,True), (8,40,8,True), (9,45,7,True), (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,False), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,2,True)]
Grounded Until:	 115
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 124
Time         : 878.767s (Solving: 842.48s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 879.032s

Choices      : 16371989 (Domain: 16141458)
Conflicts    : 994745   (Analyzed: 994742)
Restarts     : 11949    (Average: 83.25 Last: 185)
Model-Level  : 291.0   
Problems     : 124      (Average Length: 96.64 Splits: 0)
Lemmas       : 994742   (Deleted: 949188)
  Binary     : 13923    (Ratio:   1.40%)
  Ternary    : 3263     (Ratio:   0.33%)
  Conflict   : 994742   (Average Length:  598.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 994742   (Average: 14.53 Max: 1011 Sum: 14454589)
  Executed   : 994653   (Average: 14.53 Max: 1011 Sum: 14450772 Ratio:  99.97%)
  Bounded    : 89       (Average: 42.89 Max: 117 Sum:   3817 Ratio:   0.03%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 741626   (Eliminated:    0 Frozen: 233385)
Constraints  : 5460319  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 11.26s
Memory:		 856MB (+0MB)
UNKNOWN
Iteration Time:	 11.33s

Iteration 124
Queue:		 [(6,30,10,True), (7,35,9,True), (8,40,8,True), (9,45,7,True), (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,False), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,2,True)]
Grounded Until:	 115
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 125
Time         : 890.398s (Solving: 853.92s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 890.668s

Choices      : 16436567 (Domain: 16206036)
Conflicts    : 1003594  (Analyzed: 1003591)
Restarts     : 12049    (Average: 83.29 Last: 185)
Model-Level  : 291.0   
Problems     : 125      (Average Length: 96.80 Splits: 0)
Lemmas       : 1003591  (Deleted: 959446)
  Binary     : 14001    (Ratio:   1.40%)
  Ternary    : 3267     (Ratio:   0.33%)
  Conflict   : 1003591  (Average Length:  607.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 1003591  (Average: 14.45 Max: 1011 Sum: 14497817)
  Executed   : 1003502  (Average: 14.44 Max: 1011 Sum: 14494000 Ratio:  99.97%)
  Bounded    : 89       (Average: 42.89 Max: 117 Sum:   3817 Ratio:   0.03%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 741626   (Eliminated:    0 Frozen: 233385)
Constraints  : 5460319  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 11.56s
Memory:		 856MB (+0MB)
UNKNOWN
Iteration Time:	 11.64s

Iteration 125
Queue:		 [(7,35,9,True), (8,40,8,True), (9,45,7,True), (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,False), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,2,True)]
Grounded Until:	 115
Unblocking actions...
Solving...
*** Info : (planner): INTERRUPTED by signal!
UNKNOWN

INTERRUPTED  : 1

Models       : 0+
Calls        : 126
Time         : 893.374s (Solving: 856.73s 1st Model: 0.01s Unsat: 1.37s)
CPU Time     : 893.628s

Choices      : 16460551 (Domain: 16230018)
Conflicts    : 1006634  (Analyzed: 1006631)
Restarts     : 12088    (Average: 83.28 Last: 185)
Model-Level  : 291.0   
Problems     : 126      (Average Length: 96.96 Splits: 0)
Lemmas       : 1006631  (Deleted: 962491)
  Binary     : 14018    (Ratio:   1.39%)
  Ternary    : 3268     (Ratio:   0.32%)
  Conflict   : 1006631  (Average Length:  608.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 1006631  (Average: 14.42 Max: 1011 Sum: 14513936)
  Executed   : 1006542  (Average: 14.41 Max: 1011 Sum: 14510119 Ratio:  99.97%)
  Bounded    : 89       (Average: 42.89 Max: 117 Sum:   3817 Ratio:   0.03%)

Rules        : 133871   (Original: 121411)
Atoms        : 64609   
Bodies       : 58138    (Original: 45677)
  Count      : 786      (Original: 2108)
Equivalences : 14175    (Atom=Atom: 77 Body=Body: 0 Other: 14098)
Tight        : Yes
Variables    : 741626   (Eliminated:    0 Frozen: 233385)
Constraints  : 5460319  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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


