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-18.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-18.pddl
Parsing...
Parsing: [0.030s CPU, 0.033s wall-clock]
Normalizing task... [0.000s CPU, 0.003s wall-clock]
Instantiating...
Generating Datalog program... [0.020s CPU, 0.009s wall-clock]
Normalizing Datalog program...
Normalizing Datalog program: [0.040s CPU, 0.043s wall-clock]
Preparing model... [0.020s CPU, 0.026s wall-clock]
Generated 115 rules.
Computing model... [0.540s CPU, 0.536s wall-clock]
3296 relevant atoms
3425 auxiliary atoms
6721 final queue length
11595 total queue pushes
Completing instantiation... [1.030s CPU, 1.026s wall-clock]
Instantiating: [1.660s CPU, 1.648s wall-clock]
Computing fact groups...
Finding invariants...
24 initial candidates
Finding invariants: [0.090s CPU, 0.092s wall-clock]
Checking invariant weight... [0.000s CPU, 0.002s wall-clock]
Instantiating groups... [0.010s CPU, 0.010s wall-clock]
Collecting mutex groups... [0.000s CPU, 0.001s wall-clock]
Choosing groups...
350 uncovered facts
Choosing groups: [0.010s CPU, 0.002s wall-clock]
Building translation key... [0.010s CPU, 0.013s wall-clock]
Computing fact groups: [0.140s CPU, 0.147s wall-clock]
Building STRIPS to SAS dictionary... [0.010s CPU, 0.006s wall-clock]
Building dictionary for full mutex groups... [0.000s CPU, 0.003s wall-clock]
Building mutex information...
Building mutex information: [0.010s CPU, 0.004s wall-clock]
Translating task...
Processing axioms...
Simplifying axioms... [0.000s CPU, 0.000s wall-clock]
Processing axioms: [0.050s CPU, 0.056s wall-clock]
Translating task: [1.060s CPU, 1.068s wall-clock]
3920 effect conditions simplified
0 implied preconditions added
Detecting unreachable propositions...
0 operators removed
0 axioms removed
3 propositions removed
Detecting unreachable propositions: [0.590s CPU, 0.584s wall-clock]
Reordering and filtering variables...
353 of 353 variables necessary.
16 of 19 mutex groups necessary.
2344 of 2344 operators necessary.
0 of 0 axiom rules necessary.
Reordering and filtering variables: [0.380s CPU, 0.377s wall-clock]
Translator variables: 353
Translator derived variables: 0
Translator facts: 737
Translator goal facts: 14
Translator mutex groups: 16
Translator total mutex groups size: 48
Translator operators: 2344
Translator axioms: 0
Translator task size: 22454
Translator peak memory: 49100 KB
Writing output... [0.450s CPU, 0.485s wall-clock]
Done! [4.370s CPU, 4.400s wall-clock]
planner.py version 0.0.1

Time:	 0.91s
Memory: 111MB

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

Models       : 0
Calls        : 1
Time         : 1.066s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
CPU Time     : 0.916s

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

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

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

Choices      : 107      (Domain: 96)
Conflicts    : 33       (Analyzed: 32)
Restarts     : 0       
Problems     : 2        (Average Length: 4.50 Splits: 0)
Lemmas       : 32       (Deleted: 0)
  Binary     : 8        (Ratio:  25.00%)
  Ternary    : 2        (Ratio:   6.25%)
  Conflict   : 32       (Average Length:    7.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 32       (Average:  3.41 Max:  28 Sum:    109)
  Executed   : 30       (Average:  3.34 Max:  28 Sum:    107 Ratio:  98.17%)
  Bounded    : 2        (Average:  1.00 Max:   1 Sum:      2 Ratio:   1.83%)

Rules        : 64767   
Atoms        : 64767   
Bodies       : 1        (Original: 0)
Tight        : Yes
Variables    : 17354    (Eliminated:    0 Frozen:  170)
Constraints  : 57355    (Binary:  95.3% Ternary:   3.3% Other:   1.4%)

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

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

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

Models       : 1+
Calls        : 3
Time         : 2.012s (Solving: 0.02s 1st Model: 0.01s Unsat: 0.00s)
CPU Time     : 1.860s

Choices      : 1182     (Domain: 1127)
Conflicts    : 80       (Analyzed: 79)
Restarts     : 0       
Model-Level  : 348.0   
Problems     : 3        (Average Length: 7.00 Splits: 0)
Lemmas       : 79       (Deleted: 0)
  Binary     : 30       (Ratio:  37.97%)
  Ternary    : 6        (Ratio:   7.59%)
  Conflict   : 79       (Average Length:   25.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 79       (Average: 10.73 Max: 144 Sum:    848)
  Executed   : 77       (Average: 10.71 Max: 144 Sum:    846 Ratio:  99.76%)
  Bounded    : 2        (Average:  1.00 Max:   1 Sum:      2 Ratio:   0.24%)

Rules        : 64767   
Atoms        : 64767   
Bodies       : 1        (Original: 0)
Tight        : Yes
Variables    : 38040    (Eliminated:    0 Frozen:  340)
Constraints  : 226475   (Binary:  95.6% Ternary:   3.2% Other:   1.2%)

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

[endof: stats after solve call]
Solving Time:	 0.03s
Memory:		 205MB (+10MB)
SAT
Testing...
NOT SERIALIZABLE
Testing Time:	 1.17s
Memory:		 241MB (+36MB)
Solving...
[start: stats after solve call]

Models       : 0
Calls        : 4
Time         : 3.355s (Solving: 1.01s 1st Model: 0.01s Unsat: 0.99s)
CPU Time     : 3.204s

Choices      : 25561    (Domain: 20001)
Conflicts    : 2422     (Analyzed: 2420)
Restarts     : 27       (Average: 89.63 Last: 47)
Model-Level  : 348.0   
Problems     : 4        (Average Length: 8.25 Splits: 0)
Lemmas       : 2420     (Deleted: 612)
  Binary     : 493      (Ratio:  20.37%)
  Ternary    : 256      (Ratio:  10.58%)
  Conflict   : 2420     (Average Length:   51.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 2420     (Average: 10.40 Max: 217 Sum:  25161)
  Executed   : 2396     (Average: 10.31 Max: 217 Sum:  24939 Ratio:  99.12%)
  Bounded    : 24       (Average:  9.25 Max:  12 Sum:    222 Ratio:   0.88%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 60107    (Eliminated:    0 Frozen: 16894)
Constraints  : 371085   (Binary:  91.4% Ternary:   7.0% Other:   1.6%)

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

[endof: stats after solve call]
Solving Time:	 1.08s
Memory:		 240MB (+-1MB)
UNSAT
Iteration Time:	 2.77s

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

Models       : 0+
Calls        : 5
Time         : 8.494s (Solving: 5.36s 1st Model: 0.01s Unsat: 0.99s)
CPU Time     : 8.344s

Choices      : 97812    (Domain: 78688)
Conflicts    : 11419    (Analyzed: 11417)
Restarts     : 127      (Average: 89.90 Last: 68)
Model-Level  : 348.0   
Problems     : 5        (Average Length: 10.00 Splits: 0)
Lemmas       : 11417    (Deleted: 7290)
  Binary     : 1025     (Ratio:   8.98%)
  Ternary    : 380      (Ratio:   3.33%)
  Conflict   : 11417    (Average Length:  364.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 11417    (Average:  8.16 Max: 260 Sum:  93170)
  Executed   : 11380    (Average:  8.12 Max: 260 Sum:  92733 Ratio:  99.53%)
  Bounded    : 37       (Average: 11.81 Max:  17 Sum:    437 Ratio:   0.47%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 100183   (Eliminated:    0 Frozen: 29344)
Constraints  : 663976   (Binary:  91.3% Ternary:   6.9% Other:   1.7%)

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

[endof: stats after solve call]
Solving Time:	 4.38s
Memory:		 267MB (+26MB)
UNKNOWN
Iteration Time:	 5.15s

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

Models       : 0+
Calls        : 6
Time         : 14.941s (Solving: 10.91s 1st Model: 0.01s Unsat: 0.99s)
CPU Time     : 14.792s

Choices      : 214157   (Domain: 179476)
Conflicts    : 20604    (Analyzed: 20602)
Restarts     : 227      (Average: 90.76 Last: 72)
Model-Level  : 348.0   
Problems     : 6        (Average Length: 12.00 Splits: 0)
Lemmas       : 20602    (Deleted: 15373)
  Binary     : 1512     (Ratio:   7.34%)
  Ternary    : 462      (Ratio:   2.24%)
  Conflict   : 20602    (Average Length:  545.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 20602    (Average:  9.76 Max: 260 Sum: 201114)
  Executed   : 20565    (Average:  9.74 Max: 260 Sum: 200677 Ratio:  99.78%)
  Bounded    : 37       (Average: 11.81 Max:  17 Sum:    437 Ratio:   0.22%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 140259   (Eliminated:    0 Frozen: 41794)
Constraints  : 954833   (Binary:  91.3% Ternary:   6.9% Other:   1.7%)

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

[endof: stats after solve call]
Solving Time:	 5.60s
Memory:		 294MB (+15MB)
UNKNOWN
Iteration Time:	 6.46s

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

Models       : 0+
Calls        : 7
Time         : 22.473s (Solving: 17.57s 1st Model: 0.01s Unsat: 0.99s)
CPU Time     : 22.324s

Choices      : 336952   (Domain: 287184)
Conflicts    : 29049    (Analyzed: 29047)
Restarts     : 327      (Average: 88.83 Last: 72)
Model-Level  : 348.0   
Problems     : 7        (Average Length: 14.14 Splits: 0)
Lemmas       : 29047    (Deleted: 21843)
  Binary     : 1771     (Ratio:   6.10%)
  Ternary    : 507      (Ratio:   1.75%)
  Conflict   : 29047    (Average Length:  696.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 29047    (Average: 10.77 Max: 266 Sum: 312922)
  Executed   : 29010    (Average: 10.76 Max: 266 Sum: 312485 Ratio:  99.86%)
  Bounded    : 37       (Average: 11.81 Max:  17 Sum:    437 Ratio:   0.14%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 180335   (Eliminated:    0 Frozen: 54244)
Constraints  : 1256813  (Binary:  91.3% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 6.72s
Memory:		 321MB (+14MB)
UNKNOWN
Iteration Time:	 7.55s

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

Models       : 0+
Calls        : 8
Time         : 30.743s (Solving: 24.90s 1st Model: 0.01s Unsat: 0.99s)
CPU Time     : 30.596s

Choices      : 485165   (Domain: 426150)
Conflicts    : 37851    (Analyzed: 37849)
Restarts     : 427      (Average: 88.64 Last: 98)
Model-Level  : 348.0   
Problems     : 8        (Average Length: 16.38 Splits: 0)
Lemmas       : 37849    (Deleted: 31859)
  Binary     : 2074     (Ratio:   5.48%)
  Ternary    : 561      (Ratio:   1.48%)
  Conflict   : 37849    (Average Length:  798.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 37849    (Average: 11.88 Max: 331 Sum: 449736)
  Executed   : 37812    (Average: 11.87 Max: 331 Sum: 449299 Ratio:  99.90%)
  Bounded    : 37       (Average: 11.81 Max:  17 Sum:    437 Ratio:   0.10%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 220411   (Eliminated:    0 Frozen: 66694)
Constraints  : 1558793  (Binary:  91.3% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 7.40s
Memory:		 367MB (+34MB)
UNKNOWN
Iteration Time:	 8.29s

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

Models       : 0+
Calls        : 9
Time         : 35.968s (Solving: 30.06s 1st Model: 0.01s Unsat: 0.99s)
CPU Time     : 35.820s

Choices      : 544039   (Domain: 479251)
Conflicts    : 46451    (Analyzed: 46449)
Restarts     : 527      (Average: 88.14 Last: 98)
Model-Level  : 348.0   
Problems     : 9        (Average Length: 18.11 Splits: 0)
Lemmas       : 46449    (Deleted: 38074)
  Binary     : 2384     (Ratio:   5.13%)
  Ternary    : 645      (Ratio:   1.39%)
  Conflict   : 46449    (Average Length:  701.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 46449    (Average: 10.86 Max: 331 Sum: 504292)
  Executed   : 46395    (Average: 10.84 Max: 331 Sum: 503313 Ratio:  99.81%)
  Bounded    : 54       (Average: 18.13 Max:  32 Sum:    979 Ratio:   0.19%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 220411   (Eliminated:    0 Frozen: 66694)
Constraints  : 1558793  (Binary:  91.3% Ternary:   7.0% Other:   1.8%)

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

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

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         : 42.054s (Solving: 36.09s 1st Model: 0.01s Unsat: 0.99s)
CPU Time     : 41.900s

Choices      : 650081   (Domain: 580175)
Conflicts    : 55381    (Analyzed: 55379)
Restarts     : 627      (Average: 88.32 Last: 129)
Model-Level  : 348.0   
Problems     : 10       (Average Length: 19.50 Splits: 0)
Lemmas       : 55379    (Deleted: 46333)
  Binary     : 3040     (Ratio:   5.49%)
  Ternary    : 880      (Ratio:   1.59%)
  Conflict   : 55379    (Average Length:  617.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 55379    (Average: 10.92 Max: 331 Sum: 604627)
  Executed   : 55303    (Average: 10.89 Max: 331 Sum: 602948 Ratio:  99.72%)
  Bounded    : 76       (Average: 22.09 Max:  32 Sum:   1679 Ratio:   0.28%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 220411   (Eliminated:    0 Frozen: 66694)
Constraints  : 1536123  (Binary:  91.3% Ternary:   6.9% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 11
Time         : 48.460s (Solving: 42.44s 1st Model: 0.01s Unsat: 0.99s)
CPU Time     : 48.308s

Choices      : 759615   (Domain: 684138)
Conflicts    : 64377    (Analyzed: 64375)
Restarts     : 727      (Average: 88.55 Last: 140)
Model-Level  : 348.0   
Problems     : 11       (Average Length: 20.64 Splits: 0)
Lemmas       : 64375    (Deleted: 54189)
  Binary     : 3404     (Ratio:   5.29%)
  Ternary    : 982      (Ratio:   1.53%)
  Conflict   : 64375    (Average Length:  558.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 64375    (Average: 10.97 Max: 331 Sum: 706357)
  Executed   : 64294    (Average: 10.94 Max: 331 Sum: 704529 Ratio:  99.74%)
  Bounded    : 81       (Average: 22.57 Max:  32 Sum:   1828 Ratio:   0.26%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 220411   (Eliminated:    0 Frozen: 66694)
Constraints  : 1503130  (Binary:  91.3% Ternary:   6.9% Other:   1.8%)

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

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

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         : 55.144s (Solving: 49.07s 1st Model: 0.01s Unsat: 0.99s)
CPU Time     : 54.996s

Choices      : 871417   (Domain: 791053)
Conflicts    : 73439    (Analyzed: 73437)
Restarts     : 827      (Average: 88.80 Last: 214)
Model-Level  : 348.0   
Problems     : 12       (Average Length: 21.58 Splits: 0)
Lemmas       : 73437    (Deleted: 62485)
  Binary     : 3542     (Ratio:   4.82%)
  Ternary    : 1017     (Ratio:   1.38%)
  Conflict   : 73437    (Average Length:  516.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 73437    (Average: 11.02 Max: 331 Sum: 809253)
  Executed   : 73351    (Average: 10.99 Max: 331 Sum: 807270 Ratio:  99.75%)
  Bounded    : 86       (Average: 23.06 Max:  32 Sum:   1983 Ratio:   0.25%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 220411   (Eliminated:    0 Frozen: 66694)
Constraints  : 1495029  (Binary:  91.3% Ternary:   6.9% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 13
Time         : 63.381s (Solving: 56.35s 1st Model: 0.01s Unsat: 0.99s)
CPU Time     : 63.236s

Choices      : 1056383  (Domain: 967537)
Conflicts    : 81803    (Analyzed: 81801)
Restarts     : 927      (Average: 88.24 Last: 214)
Model-Level  : 348.0   
Problems     : 13       (Average Length: 22.77 Splits: 0)
Lemmas       : 81801    (Deleted: 69902)
  Binary     : 3748     (Ratio:   4.58%)
  Ternary    : 1051     (Ratio:   1.28%)
  Conflict   : 81801    (Average Length:  493.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 81801    (Average: 12.00 Max: 331 Sum: 981765)
  Executed   : 81715    (Average: 11.98 Max: 331 Sum: 979782 Ratio:  99.80%)
  Bounded    : 86       (Average: 23.06 Max:  32 Sum:   1983 Ratio:   0.20%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 260487   (Eliminated:    0 Frozen: 79144)
Constraints  : 1796954  (Binary:  91.3% Ternary:   6.9% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 7.35s
Memory:		 380MB (+13MB)
UNKNOWN
Iteration Time:	 8.26s

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

Models       : 0+
Calls        : 14
Time         : 72.306s (Solving: 64.27s 1st Model: 0.01s Unsat: 0.99s)
CPU Time     : 72.164s

Choices      : 1258544  (Domain: 1162758)
Conflicts    : 90386    (Analyzed: 90384)
Restarts     : 1027     (Average: 88.01 Last: 214)
Model-Level  : 348.0   
Problems     : 14       (Average Length: 24.14 Splits: 0)
Lemmas       : 90384    (Deleted: 78048)
  Binary     : 3894     (Ratio:   4.31%)
  Ternary    : 1052     (Ratio:   1.16%)
  Conflict   : 90384    (Average Length:  472.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 90384    (Average: 12.95 Max: 394 Sum: 1170911)
  Executed   : 90298    (Average: 12.93 Max: 394 Sum: 1168928 Ratio:  99.83%)
  Bounded    : 86       (Average: 23.06 Max:  32 Sum:   1983 Ratio:   0.17%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 300563   (Eliminated:    0 Frozen: 91594)
Constraints  : 2098934  (Binary:  91.3% Ternary:   6.9% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 8.00s
Memory:		 406MB (+14MB)
UNKNOWN
Iteration Time:	 8.94s

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

Models       : 0+
Calls        : 15
Time         : 80.110s (Solving: 70.89s 1st Model: 0.01s Unsat: 0.99s)
CPU Time     : 79.968s

Choices      : 1414888  (Domain: 1315573)
Conflicts    : 98119    (Analyzed: 98117)
Restarts     : 1127     (Average: 87.06 Last: 214)
Model-Level  : 348.0   
Problems     : 15       (Average Length: 25.67 Splits: 0)
Lemmas       : 98117    (Deleted: 86485)
  Binary     : 4000     (Ratio:   4.08%)
  Ternary    : 1060     (Ratio:   1.08%)
  Conflict   : 98117    (Average Length:  456.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 98117    (Average: 13.40 Max: 507 Sum: 1314279)
  Executed   : 98031    (Average: 13.37 Max: 507 Sum: 1312296 Ratio:  99.85%)
  Bounded    : 86       (Average: 23.06 Max:  32 Sum:   1983 Ratio:   0.15%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 340639   (Eliminated:    0 Frozen: 104044)
Constraints  : 2400914  (Binary:  91.3% Ternary:   6.9% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 6.70s
Memory:		 476MB (+46MB)
UNKNOWN
Iteration Time:	 7.82s

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

Models       : 0+
Calls        : 16
Time         : 88.523s (Solving: 78.32s 1st Model: 0.01s Unsat: 0.99s)
CPU Time     : 88.384s

Choices      : 1620637  (Domain: 1516697)
Conflicts    : 106238   (Analyzed: 106236)
Restarts     : 1227     (Average: 86.58 Last: 214)
Model-Level  : 348.0   
Problems     : 16       (Average Length: 27.31 Splits: 0)
Lemmas       : 106236   (Deleted: 94030)
  Binary     : 4120     (Ratio:   3.88%)
  Ternary    : 1078     (Ratio:   1.01%)
  Conflict   : 106236   (Average Length:  443.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 106236   (Average: 14.14 Max: 538 Sum: 1502682)
  Executed   : 106150   (Average: 14.13 Max: 538 Sum: 1500699 Ratio:  99.87%)
  Bounded    : 86       (Average: 23.06 Max:  32 Sum:   1983 Ratio:   0.13%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 380715   (Eliminated:    0 Frozen: 116494)
Constraints  : 2702894  (Binary:  91.3% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 7.52s
Memory:		 485MB (+9MB)
UNKNOWN
Iteration Time:	 8.43s

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

Models       : 0+
Calls        : 17
Time         : 97.826s (Solving: 86.63s 1st Model: 0.01s Unsat: 0.99s)
CPU Time     : 97.688s

Choices      : 1862404  (Domain: 1753067)
Conflicts    : 114386   (Analyzed: 114384)
Restarts     : 1327     (Average: 86.20 Last: 214)
Model-Level  : 348.0   
Problems     : 17       (Average Length: 29.06 Splits: 0)
Lemmas       : 114384   (Deleted: 101821)
  Binary     : 4298     (Ratio:   3.76%)
  Ternary    : 1124     (Ratio:   0.98%)
  Conflict   : 114384   (Average Length:  439.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 114384   (Average: 15.06 Max: 570 Sum: 1723188)
  Executed   : 114298   (Average: 15.05 Max: 570 Sum: 1721205 Ratio:  99.88%)
  Bounded    : 86       (Average: 23.06 Max:  32 Sum:   1983 Ratio:   0.12%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 420791   (Eliminated:    0 Frozen: 128944)
Constraints  : 3004874  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 8.40s
Memory:		 512MB (+20MB)
UNKNOWN
Iteration Time:	 9.32s

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

Models       : 0+
Calls        : 18
Time         : 107.586s (Solving: 95.31s 1st Model: 0.01s Unsat: 0.99s)
CPU Time     : 107.452s

Choices      : 2116038  (Domain: 2001478)
Conflicts    : 122321   (Analyzed: 122319)
Restarts     : 1427     (Average: 85.72 Last: 214)
Model-Level  : 348.0   
Problems     : 18       (Average Length: 30.89 Splits: 0)
Lemmas       : 122319   (Deleted: 109754)
  Binary     : 4432     (Ratio:   3.62%)
  Ternary    : 1140     (Ratio:   0.93%)
  Conflict   : 122319   (Average Length:  441.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 122319   (Average: 16.00 Max: 745 Sum: 1956886)
  Executed   : 122233   (Average: 15.98 Max: 745 Sum: 1954903 Ratio:  99.90%)
  Bounded    : 86       (Average: 23.06 Max:  32 Sum:   1983 Ratio:   0.10%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 460867   (Eliminated:    0 Frozen: 141394)
Constraints  : 3306854  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 8.79s
Memory:		 589MB (+72MB)
UNKNOWN
Iteration Time:	 9.78s

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

Models       : 0+
Calls        : 19
Time         : 116.108s (Solving: 102.75s 1st Model: 0.01s Unsat: 0.99s)
CPU Time     : 115.976s

Choices      : 2341685  (Domain: 2220252)
Conflicts    : 130183   (Analyzed: 130181)
Restarts     : 1527     (Average: 85.25 Last: 214)
Model-Level  : 348.0   
Problems     : 19       (Average Length: 32.79 Splits: 0)
Lemmas       : 130181   (Deleted: 116978)
  Binary     : 4531     (Ratio:   3.48%)
  Ternary    : 1155     (Ratio:   0.89%)
  Conflict   : 130181   (Average Length:  435.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 130181   (Average: 16.61 Max: 745 Sum: 2162703)
  Executed   : 130095   (Average: 16.60 Max: 745 Sum: 2160720 Ratio:  99.91%)
  Bounded    : 86       (Average: 23.06 Max:  32 Sum:   1983 Ratio:   0.09%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 500943   (Eliminated:    0 Frozen: 153844)
Constraints  : 3608834  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 7.55s
Memory:		 594MB (+5MB)
UNKNOWN
Iteration Time:	 8.54s

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

Models       : 0+
Calls        : 20
Time         : 125.798s (Solving: 111.35s 1st Model: 0.01s Unsat: 0.99s)
CPU Time     : 125.668s

Choices      : 2593202  (Domain: 2467806)
Conflicts    : 138058   (Analyzed: 138056)
Restarts     : 1627     (Average: 84.85 Last: 214)
Model-Level  : 348.0   
Problems     : 20       (Average Length: 34.75 Splits: 0)
Lemmas       : 138056   (Deleted: 124632)
  Binary     : 4652     (Ratio:   3.37%)
  Ternary    : 1176     (Ratio:   0.85%)
  Conflict   : 138056   (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    : 138056   (Average: 17.33 Max: 847 Sum: 2393137)
  Executed   : 137970   (Average: 17.32 Max: 847 Sum: 2391154 Ratio:  99.92%)
  Bounded    : 86       (Average: 23.06 Max:  32 Sum:   1983 Ratio:   0.08%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 541019   (Eliminated:    0 Frozen: 166294)
Constraints  : 3910814  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 8.71s
Memory:		 609MB (+15MB)
UNKNOWN
Iteration Time:	 9.71s

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

Models       : 0+
Calls        : 21
Time         : 135.223s (Solving: 119.63s 1st Model: 0.01s Unsat: 0.99s)
CPU Time     : 135.096s

Choices      : 2899677  (Domain: 2769594)
Conflicts    : 145916   (Analyzed: 145914)
Restarts     : 1727     (Average: 84.49 Last: 214)
Model-Level  : 348.0   
Problems     : 21       (Average Length: 36.76 Splits: 0)
Lemmas       : 145914   (Deleted: 132012)
  Binary     : 4794     (Ratio:   3.29%)
  Ternary    : 1186     (Ratio:   0.81%)
  Conflict   : 145914   (Average Length:  428.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 145914   (Average: 18.35 Max: 906 Sum: 2677987)
  Executed   : 145828   (Average: 18.34 Max: 906 Sum: 2676004 Ratio:  99.93%)
  Bounded    : 86       (Average: 23.06 Max:  32 Sum:   1983 Ratio:   0.07%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 581095   (Eliminated:    0 Frozen: 178744)
Constraints  : 4212794  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 8.40s
Memory:		 642MB (+28MB)
UNKNOWN
Iteration Time:	 9.44s

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

Models       : 0+
Calls        : 22
Time         : 144.399s (Solving: 127.68s 1st Model: 0.01s Unsat: 0.99s)
CPU Time     : 144.276s

Choices      : 3131741  (Domain: 3000152)
Conflicts    : 153706   (Analyzed: 153704)
Restarts     : 1827     (Average: 84.13 Last: 214)
Model-Level  : 348.0   
Problems     : 22       (Average Length: 38.82 Splits: 0)
Lemmas       : 153704   (Deleted: 139856)
  Binary     : 4909     (Ratio:   3.19%)
  Ternary    : 1204     (Ratio:   0.78%)
  Conflict   : 153704   (Average Length:  424.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 153704   (Average: 18.79 Max: 955 Sum: 2887396)
  Executed   : 153618   (Average: 18.77 Max: 955 Sum: 2885413 Ratio:  99.93%)
  Bounded    : 86       (Average: 23.06 Max:  32 Sum:   1983 Ratio:   0.07%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 621171   (Eliminated:    0 Frozen: 191194)
Constraints  : 4514774  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 8.17s
Memory:		 666MB (+24MB)
UNKNOWN
Iteration Time:	 9.19s

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         : 144.856s (Solving: 127.98s 1st Model: 0.01s Unsat: 1.30s)
CPU Time     : 144.732s

Choices      : 3132932  (Domain: 3001343)
Conflicts    : 153898   (Analyzed: 153895)
Restarts     : 1828     (Average: 84.19 Last: 214)
Model-Level  : 348.0   
Problems     : 23       (Average Length: 40.70 Splits: 0)
Lemmas       : 153895   (Deleted: 139856)
  Binary     : 4919     (Ratio:   3.20%)
  Ternary    : 1204     (Ratio:   0.78%)
  Conflict   : 153895   (Average Length:  424.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 153895   (Average: 18.77 Max: 955 Sum: 2888670)
  Executed   : 153805   (Average: 18.76 Max: 955 Sum: 2886603 Ratio:  99.93%)
  Bounded    : 90       (Average: 22.97 Max:  81 Sum:   2067 Ratio:   0.07%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 621171   (Eliminated:    0 Frozen: 191194)
Constraints  : 4514774  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 0.40s
Memory:		 666MB (+0MB)
UNSAT
Iteration Time:	 0.46s

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         : 151.235s (Solving: 134.20s 1st Model: 0.01s Unsat: 1.30s)
CPU Time     : 151.112s

Choices      : 3191008  (Domain: 3055676)
Conflicts    : 162446   (Analyzed: 162443)
Restarts     : 1928     (Average: 84.25 Last: 214)
Model-Level  : 348.0   
Problems     : 24       (Average Length: 42.42 Splits: 0)
Lemmas       : 162443   (Deleted: 146907)
  Binary     : 5030     (Ratio:   3.10%)
  Ternary    : 1229     (Ratio:   0.76%)
  Conflict   : 162443   (Average Length:  417.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 162443   (Average: 18.10 Max: 955 Sum: 2940236)
  Executed   : 162349   (Average: 18.09 Max: 955 Sum: 2937847 Ratio:  99.92%)
  Bounded    : 94       (Average: 25.41 Max:  82 Sum:   2389 Ratio:   0.08%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 621171   (Eliminated:    0 Frozen: 191194)
Constraints  : 4514774  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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         : 158.560s (Solving: 141.37s 1st Model: 0.01s Unsat: 1.30s)
CPU Time     : 158.440s

Choices      : 3295875  (Domain: 3152481)
Conflicts    : 171187   (Analyzed: 171184)
Restarts     : 2028     (Average: 84.41 Last: 214)
Model-Level  : 348.0   
Problems     : 25       (Average Length: 44.00 Splits: 0)
Lemmas       : 171184   (Deleted: 156227)
  Binary     : 5151     (Ratio:   3.01%)
  Ternary    : 1251     (Ratio:   0.73%)
  Conflict   : 171184   (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    : 171184   (Average: 17.73 Max: 955 Sum: 3035404)
  Executed   : 171086   (Average: 17.72 Max: 955 Sum: 3032692 Ratio:  99.91%)
  Bounded    : 98       (Average: 27.67 Max:  82 Sum:   2712 Ratio:   0.09%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 621171   (Eliminated:    0 Frozen: 191194)
Constraints  : 4514733  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 7.27s
Memory:		 666MB (+0MB)
UNKNOWN
Iteration Time:	 7.33s

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         : 166.020s (Solving: 148.66s 1st Model: 0.01s Unsat: 1.30s)
CPU Time     : 165.900s

Choices      : 3416092  (Domain: 3270367)
Conflicts    : 179813   (Analyzed: 179810)
Restarts     : 2128     (Average: 84.50 Last: 214)
Model-Level  : 348.0   
Problems     : 26       (Average Length: 45.46 Splits: 0)
Lemmas       : 179810   (Deleted: 164074)
  Binary     : 5573     (Ratio:   3.10%)
  Ternary    : 1443     (Ratio:   0.80%)
  Conflict   : 179810   (Average Length:  403.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 179810   (Average: 17.49 Max: 955 Sum: 3145617)
  Executed   : 179709   (Average: 17.48 Max: 955 Sum: 3142660 Ratio:  99.91%)
  Bounded    : 101      (Average: 29.28 Max:  82 Sum:   2957 Ratio:   0.09%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 621171   (Eliminated:    0 Frozen: 191194)
Constraints  : 4511887  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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         : 174.558s (Solving: 157.07s 1st Model: 0.01s Unsat: 1.30s)
CPU Time     : 174.444s

Choices      : 3557273  (Domain: 3407196)
Conflicts    : 188630   (Analyzed: 188627)
Restarts     : 2228     (Average: 84.66 Last: 214)
Model-Level  : 348.0   
Problems     : 27       (Average Length: 46.81 Splits: 0)
Lemmas       : 188627   (Deleted: 171617)
  Binary     : 5912     (Ratio:   3.13%)
  Ternary    : 1538     (Ratio:   0.82%)
  Conflict   : 188627   (Average Length:  396.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 188627   (Average: 17.36 Max: 955 Sum: 3275321)
  Executed   : 188522   (Average: 17.35 Max: 955 Sum: 3272043 Ratio:  99.90%)
  Bounded    : 105      (Average: 31.22 Max:  82 Sum:   3278 Ratio:   0.10%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 621171   (Eliminated:    0 Frozen: 191194)
Constraints  : 4511860  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 8.50s
Memory:		 666MB (+0MB)
UNKNOWN
Iteration Time:	 8.55s

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         : 185.062s (Solving: 167.42s 1st Model: 0.01s Unsat: 1.30s)
CPU Time     : 184.952s

Choices      : 3722286  (Domain: 3568296)
Conflicts    : 197990   (Analyzed: 197987)
Restarts     : 2328     (Average: 85.05 Last: 214)
Model-Level  : 348.0   
Problems     : 28       (Average Length: 48.07 Splits: 0)
Lemmas       : 197987   (Deleted: 179755)
  Binary     : 6251     (Ratio:   3.16%)
  Ternary    : 1610     (Ratio:   0.81%)
  Conflict   : 197987   (Average Length:  418.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 197987   (Average: 17.28 Max: 955 Sum: 3421861)
  Executed   : 197881   (Average: 17.27 Max: 955 Sum: 3418582 Ratio:  99.90%)
  Bounded    : 106      (Average: 30.93 Max:  82 Sum:   3279 Ratio:   0.10%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 621171   (Eliminated:    0 Frozen: 191194)
Constraints  : 4511846  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 10.45s
Memory:		 666MB (+0MB)
UNKNOWN
Iteration Time:	 10.51s

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         : 194.532s (Solving: 176.76s 1st Model: 0.01s Unsat: 1.30s)
CPU Time     : 194.428s

Choices      : 3925425  (Domain: 3768343)
Conflicts    : 206970   (Analyzed: 206967)
Restarts     : 2428     (Average: 85.24 Last: 214)
Model-Level  : 348.0   
Problems     : 29       (Average Length: 49.24 Splits: 0)
Lemmas       : 206967   (Deleted: 188256)
  Binary     : 6586     (Ratio:   3.18%)
  Ternary    : 1707     (Ratio:   0.82%)
  Conflict   : 206967   (Average Length:  410.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 206967   (Average: 17.45 Max: 955 Sum: 3611108)
  Executed   : 206860   (Average: 17.43 Max: 955 Sum: 3607747 Ratio:  99.91%)
  Bounded    : 107      (Average: 31.41 Max:  82 Sum:   3361 Ratio:   0.09%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 621171   (Eliminated:    0 Frozen: 191194)
Constraints  : 4511846  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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         : 204.289s (Solving: 186.38s 1st Model: 0.01s Unsat: 1.30s)
CPU Time     : 204.192s

Choices      : 4089366  (Domain: 3930511)
Conflicts    : 215737   (Analyzed: 215734)
Restarts     : 2528     (Average: 85.34 Last: 214)
Model-Level  : 348.0   
Problems     : 30       (Average Length: 50.33 Splits: 0)
Lemmas       : 215734   (Deleted: 196772)
  Binary     : 6714     (Ratio:   3.11%)
  Ternary    : 1724     (Ratio:   0.80%)
  Conflict   : 215734   (Average Length:  404.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 215734   (Average: 17.43 Max: 955 Sum: 3761158)
  Executed   : 215626   (Average: 17.42 Max: 955 Sum: 3757715 Ratio:  99.91%)
  Bounded    : 108      (Average: 31.88 Max:  82 Sum:   3443 Ratio:   0.09%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 621171   (Eliminated:    0 Frozen: 191194)
Constraints  : 4511832  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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         : 214.370s (Solving: 196.34s 1st Model: 0.01s Unsat: 1.30s)
CPU Time     : 214.280s

Choices      : 4287186  (Domain: 4126301)
Conflicts    : 224317   (Analyzed: 224314)
Restarts     : 2628     (Average: 85.36 Last: 214)
Model-Level  : 348.0   
Problems     : 31       (Average Length: 51.35 Splits: 0)
Lemmas       : 224314   (Deleted: 202994)
  Binary     : 6856     (Ratio:   3.06%)
  Ternary    : 1754     (Ratio:   0.78%)
  Conflict   : 224314   (Average Length:  399.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 224314   (Average: 17.59 Max: 955 Sum: 3946420)
  Executed   : 224205   (Average: 17.58 Max: 955 Sum: 3942895 Ratio:  99.91%)
  Bounded    : 109      (Average: 32.34 Max:  82 Sum:   3525 Ratio:   0.09%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 621171   (Eliminated:    0 Frozen: 191194)
Constraints  : 4511818  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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         : 224.367s (Solving: 206.20s 1st Model: 0.01s Unsat: 1.30s)
CPU Time     : 224.284s

Choices      : 4469383  (Domain: 4307616)
Conflicts    : 233081   (Analyzed: 233078)
Restarts     : 2728     (Average: 85.44 Last: 214)
Model-Level  : 348.0   
Problems     : 32       (Average Length: 52.31 Splits: 0)
Lemmas       : 233078   (Deleted: 213321)
  Binary     : 6991     (Ratio:   3.00%)
  Ternary    : 1780     (Ratio:   0.76%)
  Conflict   : 233078   (Average Length:  396.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 233078   (Average: 17.66 Max: 955 Sum: 4116055)
  Executed   : 232968   (Average: 17.64 Max: 955 Sum: 4112448 Ratio:  99.91%)
  Bounded    : 110      (Average: 32.79 Max:  82 Sum:   3607 Ratio:   0.09%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 621171   (Eliminated:    0 Frozen: 191194)
Constraints  : 4511804  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 9.95s
Memory:		 666MB (+0MB)
UNKNOWN
Iteration Time:	 10.01s

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         : 236.068s (Solving: 217.73s 1st Model: 0.01s Unsat: 1.30s)
CPU Time     : 235.988s

Choices      : 4686420  (Domain: 4524096)
Conflicts    : 241665   (Analyzed: 241662)
Restarts     : 2828     (Average: 85.45 Last: 214)
Model-Level  : 348.0   
Problems     : 33       (Average Length: 53.21 Splits: 0)
Lemmas       : 241662   (Deleted: 219533)
  Binary     : 7146     (Ratio:   2.96%)
  Ternary    : 1815     (Ratio:   0.75%)
  Conflict   : 241662   (Average Length:  395.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 241662   (Average: 17.87 Max: 955 Sum: 4318041)
  Executed   : 241551   (Average: 17.85 Max: 955 Sum: 4314352 Ratio:  99.91%)
  Bounded    : 111      (Average: 33.23 Max:  82 Sum:   3689 Ratio:   0.09%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 621171   (Eliminated:    0 Frozen: 191194)
Constraints  : 4511790  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 11.65s
Memory:		 666MB (+0MB)
UNKNOWN
Iteration Time:	 11.71s

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

Models       : 0+
Calls        : 34
Time         : 246.132s (Solving: 227.67s 1st Model: 0.01s Unsat: 1.30s)
CPU Time     : 246.056s

Choices      : 4868694  (Domain: 4705545)
Conflicts    : 249561   (Analyzed: 249558)
Restarts     : 2928     (Average: 85.23 Last: 214)
Model-Level  : 348.0   
Problems     : 34       (Average Length: 54.06 Splits: 0)
Lemmas       : 249558   (Deleted: 227737)
  Binary     : 7273     (Ratio:   2.91%)
  Ternary    : 1857     (Ratio:   0.74%)
  Conflict   : 249558   (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    : 249558   (Average: 17.98 Max: 955 Sum: 4485937)
  Executed   : 249447   (Average: 17.96 Max: 955 Sum: 4482248 Ratio:  99.92%)
  Bounded    : 111      (Average: 33.23 Max:  82 Sum:   3689 Ratio:   0.08%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 621171   (Eliminated:    0 Frozen: 191194)
Constraints  : 4511776  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 10.03s
Memory:		 666MB (+0MB)
UNKNOWN
Iteration Time:	 10.07s

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         : 254.410s (Solving: 235.80s 1st Model: 0.01s Unsat: 1.30s)
CPU Time     : 254.336s

Choices      : 4947095  (Domain: 4783745)
Conflicts    : 257411   (Analyzed: 257408)
Restarts     : 3028     (Average: 85.01 Last: 214)
Model-Level  : 348.0   
Problems     : 35       (Average Length: 54.86 Splits: 0)
Lemmas       : 257408   (Deleted: 235336)
  Binary     : 7319     (Ratio:   2.84%)
  Ternary    : 1874     (Ratio:   0.73%)
  Conflict   : 257408   (Average Length:  388.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 257408   (Average: 17.68 Max: 955 Sum: 4551600)
  Executed   : 257297   (Average: 17.67 Max: 955 Sum: 4547911 Ratio:  99.92%)
  Bounded    : 111      (Average: 33.23 Max:  82 Sum:   3689 Ratio:   0.08%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 621171   (Eliminated:    0 Frozen: 191194)
Constraints  : 4511776  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 8.23s
Memory:		 666MB (+0MB)
UNKNOWN
Iteration Time:	 8.28s

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         : 263.850s (Solving: 245.12s 1st Model: 0.01s Unsat: 1.30s)
CPU Time     : 263.780s

Choices      : 5197239  (Domain: 5033047)
Conflicts    : 264968   (Analyzed: 264965)
Restarts     : 3128     (Average: 84.71 Last: 214)
Model-Level  : 348.0   
Problems     : 36       (Average Length: 55.61 Splits: 0)
Lemmas       : 264965   (Deleted: 242801)
  Binary     : 7455     (Ratio:   2.81%)
  Ternary    : 1938     (Ratio:   0.73%)
  Conflict   : 264965   (Average Length:  385.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 264965   (Average: 18.06 Max: 955 Sum: 4785716)
  Executed   : 264854   (Average: 18.05 Max: 955 Sum: 4782027 Ratio:  99.92%)
  Bounded    : 111      (Average: 33.23 Max:  82 Sum:   3689 Ratio:   0.08%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 621171   (Eliminated:    0 Frozen: 191194)
Constraints  : 4511776  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 9.40s
Memory:		 666MB (+0MB)
UNKNOWN
Iteration Time:	 9.45s

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

Models       : 0+
Calls        : 37
Time         : 273.650s (Solving: 253.75s 1st Model: 0.01s Unsat: 1.30s)
CPU Time     : 273.584s

Choices      : 5314817  (Domain: 5150535)
Conflicts    : 272977   (Analyzed: 272974)
Restarts     : 3228     (Average: 84.56 Last: 214)
Model-Level  : 348.0   
Problems     : 37       (Average Length: 56.46 Splits: 0)
Lemmas       : 272974   (Deleted: 250127)
  Binary     : 7570     (Ratio:   2.77%)
  Ternary    : 1942     (Ratio:   0.71%)
  Conflict   : 272974   (Average Length:  384.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 272974   (Average: 17.88 Max: 955 Sum: 4880853)
  Executed   : 272863   (Average: 17.87 Max: 955 Sum: 4877164 Ratio:  99.92%)
  Bounded    : 111      (Average: 33.23 Max:  82 Sum:   3689 Ratio:   0.08%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 661247   (Eliminated:    0 Frozen: 203644)
Constraints  : 4813756  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 8.75s
Memory:		 688MB (+22MB)
UNKNOWN
Iteration Time:	 9.81s

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

Models       : 0+
Calls        : 38
Time         : 281.954s (Solving: 260.83s 1st Model: 0.01s Unsat: 1.30s)
CPU Time     : 281.892s

Choices      : 5387180  (Domain: 5222882)
Conflicts    : 280603   (Analyzed: 280600)
Restarts     : 3328     (Average: 84.31 Last: 214)
Model-Level  : 348.0   
Problems     : 38       (Average Length: 57.39 Splits: 0)
Lemmas       : 280600   (Deleted: 257977)
  Binary     : 7641     (Ratio:   2.72%)
  Ternary    : 1945     (Ratio:   0.69%)
  Conflict   : 280600   (Average Length:  382.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 280600   (Average: 17.57 Max: 955 Sum: 4931039)
  Executed   : 280489   (Average: 17.56 Max: 955 Sum: 4927350 Ratio:  99.93%)
  Bounded    : 111      (Average: 33.23 Max:  82 Sum:   3689 Ratio:   0.07%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 701323   (Eliminated:    0 Frozen: 216094)
Constraints  : 5115736  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 7.22s
Memory:		 791MB (+103MB)
UNKNOWN
Iteration Time:	 8.32s

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

Models       : 0+
Calls        : 39
Time         : 291.381s (Solving: 268.74s 1st Model: 0.01s Unsat: 1.30s)
CPU Time     : 291.324s

Choices      : 5498141  (Domain: 5333685)
Conflicts    : 288725   (Analyzed: 288722)
Restarts     : 3428     (Average: 84.22 Last: 214)
Model-Level  : 348.0   
Problems     : 39       (Average Length: 58.41 Splits: 0)
Lemmas       : 288722   (Deleted: 265429)
  Binary     : 7671     (Ratio:   2.66%)
  Ternary    : 1953     (Ratio:   0.68%)
  Conflict   : 288722   (Average Length:  381.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 288722   (Average: 17.38 Max: 955 Sum: 5017787)
  Executed   : 288611   (Average: 17.37 Max: 955 Sum: 5014098 Ratio:  99.93%)
  Bounded    : 111      (Average: 33.23 Max:  82 Sum:   3689 Ratio:   0.07%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 741399   (Eliminated:    0 Frozen: 228544)
Constraints  : 5417716  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 8.05s
Memory:		 797MB (+6MB)
UNKNOWN
Iteration Time:	 9.44s

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

Models       : 0+
Calls        : 40
Time         : 300.258s (Solving: 276.42s 1st Model: 0.01s Unsat: 1.30s)
CPU Time     : 300.204s

Choices      : 5641808  (Domain: 5477102)
Conflicts    : 296237   (Analyzed: 296234)
Restarts     : 3528     (Average: 83.97 Last: 214)
Model-Level  : 348.0   
Problems     : 40       (Average Length: 59.50 Splits: 0)
Lemmas       : 296234   (Deleted: 273460)
  Binary     : 7710     (Ratio:   2.60%)
  Ternary    : 1958     (Ratio:   0.66%)
  Conflict   : 296234   (Average Length:  379.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 296234   (Average: 17.34 Max: 1044 Sum: 5136594)
  Executed   : 296123   (Average: 17.33 Max: 1044 Sum: 5132905 Ratio:  99.93%)
  Bounded    : 111      (Average: 33.23 Max:  82 Sum:   3689 Ratio:   0.07%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 781475   (Eliminated:    0 Frozen: 240994)
Constraints  : 5719696  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 7.82s
Memory:		 820MB (+23MB)
UNKNOWN
Iteration Time:	 8.89s

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         : 307.794s (Solving: 283.80s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 307.744s

Choices      : 5732032  (Domain: 5567326)
Conflicts    : 302649   (Analyzed: 302645)
Restarts     : 3596     (Average: 84.16 Last: 214)
Model-Level  : 348.0   
Problems     : 41       (Average Length: 60.54 Splits: 0)
Lemmas       : 302645   (Deleted: 280427)
  Binary     : 7791     (Ratio:   2.57%)
  Ternary    : 1981     (Ratio:   0.65%)
  Conflict   : 302645   (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    : 302645   (Average: 17.26 Max: 1044 Sum: 5225165)
  Executed   : 302532   (Average: 17.25 Max: 1044 Sum: 5221474 Ratio:  99.93%)
  Bounded    : 113      (Average: 32.66 Max:  82 Sum:   3691 Ratio:   0.07%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 781475   (Eliminated:    0 Frozen: 240994)
Constraints  : 5719696  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 7.49s
Memory:		 820MB (+0MB)
UNSAT
Iteration Time:	 7.54s

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         : 312.698s (Solving: 288.54s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 312.648s

Choices      : 5776798  (Domain: 5611537)
Conflicts    : 310175   (Analyzed: 310171)
Restarts     : 3696     (Average: 83.92 Last: 214)
Model-Level  : 348.0   
Problems     : 42       (Average Length: 61.52 Splits: 0)
Lemmas       : 310171   (Deleted: 286553)
  Binary     : 7822     (Ratio:   2.52%)
  Ternary    : 1990     (Ratio:   0.64%)
  Conflict   : 310171   (Average Length:  377.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 310171   (Average: 16.97 Max: 1044 Sum: 5263328)
  Executed   : 310057   (Average: 16.96 Max: 1044 Sum: 5259540 Ratio:  99.93%)
  Bounded    : 114      (Average: 33.23 Max:  97 Sum:   3788 Ratio:   0.07%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 781475   (Eliminated:    0 Frozen: 240994)
Constraints  : 5719696  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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         : 318.465s (Solving: 294.15s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 318.416s

Choices      : 5852311  (Domain: 5684001)
Conflicts    : 318535   (Analyzed: 318531)
Restarts     : 3796     (Average: 83.91 Last: 214)
Model-Level  : 348.0   
Problems     : 43       (Average Length: 62.47 Splits: 0)
Lemmas       : 318531   (Deleted: 293777)
  Binary     : 7903     (Ratio:   2.48%)
  Ternary    : 2006     (Ratio:   0.63%)
  Conflict   : 318531   (Average Length:  373.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 318531   (Average: 16.73 Max: 1044 Sum: 5329135)
  Executed   : 318417   (Average: 16.72 Max: 1044 Sum: 5325347 Ratio:  99.93%)
  Bounded    : 114      (Average: 33.23 Max:  97 Sum:   3788 Ratio:   0.07%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 781475   (Eliminated:    0 Frozen: 240994)
Constraints  : 5719696  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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         : 324.012s (Solving: 299.51s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 323.964s

Choices      : 5915318  (Domain: 5745892)
Conflicts    : 326281   (Analyzed: 326277)
Restarts     : 3896     (Average: 83.75 Last: 214)
Model-Level  : 348.0   
Problems     : 44       (Average Length: 63.36 Splits: 0)
Lemmas       : 326277   (Deleted: 301756)
  Binary     : 8066     (Ratio:   2.47%)
  Ternary    : 2053     (Ratio:   0.63%)
  Conflict   : 326277   (Average Length:  369.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 326277   (Average: 16.50 Max: 1044 Sum: 5384011)
  Executed   : 326161   (Average: 16.49 Max: 1044 Sum: 5380024 Ratio:  99.93%)
  Bounded    : 116      (Average: 34.37 Max: 102 Sum:   3987 Ratio:   0.07%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 781475   (Eliminated:    0 Frozen: 240994)
Constraints  : 5719696  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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         : 331.191s (Solving: 306.50s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 331.148s

Choices      : 6052154  (Domain: 5879977)
Conflicts    : 334983   (Analyzed: 334979)
Restarts     : 3996     (Average: 83.83 Last: 214)
Model-Level  : 348.0   
Problems     : 45       (Average Length: 64.22 Splits: 0)
Lemmas       : 334979   (Deleted: 311087)
  Binary     : 8387     (Ratio:   2.50%)
  Ternary    : 2137     (Ratio:   0.64%)
  Conflict   : 334979   (Average Length:  367.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 334979   (Average: 16.44 Max: 1044 Sum: 5508659)
  Executed   : 334862   (Average: 16.43 Max: 1044 Sum: 5504570 Ratio:  99.93%)
  Bounded    : 117      (Average: 34.95 Max: 102 Sum:   4089 Ratio:   0.07%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 781475   (Eliminated:    0 Frozen: 240994)
Constraints  : 5717068  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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         : 337.676s (Solving: 312.80s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 337.636s

Choices      : 6130064  (Domain: 5956411)
Conflicts    : 343056   (Analyzed: 343052)
Restarts     : 4096     (Average: 83.75 Last: 214)
Model-Level  : 348.0   
Problems     : 46       (Average Length: 65.04 Splits: 0)
Lemmas       : 343052   (Deleted: 316884)
  Binary     : 8556     (Ratio:   2.49%)
  Ternary    : 2211     (Ratio:   0.64%)
  Conflict   : 343052   (Average Length:  365.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 343052   (Average: 16.26 Max: 1044 Sum: 5576384)
  Executed   : 342934   (Average: 16.24 Max: 1044 Sum: 5572198 Ratio:  99.92%)
  Bounded    : 118      (Average: 35.47 Max: 102 Sum:   4186 Ratio:   0.08%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 781475   (Eliminated:    0 Frozen: 240994)
Constraints  : 5717054  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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         : 344.275s (Solving: 319.24s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 344.240s

Choices      : 6255500  (Domain: 6080993)
Conflicts    : 351733   (Analyzed: 351729)
Restarts     : 4196     (Average: 83.82 Last: 214)
Model-Level  : 348.0   
Problems     : 47       (Average Length: 65.83 Splits: 0)
Lemmas       : 351729   (Deleted: 326456)
  Binary     : 8719     (Ratio:   2.48%)
  Ternary    : 2294     (Ratio:   0.65%)
  Conflict   : 351729   (Average Length:  361.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 351729   (Average: 16.17 Max: 1044 Sum: 5688689)
  Executed   : 351611   (Average: 16.16 Max: 1044 Sum: 5684503 Ratio:  99.93%)
  Bounded    : 118      (Average: 35.47 Max: 102 Sum:   4186 Ratio:   0.07%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 781475   (Eliminated:    0 Frozen: 240994)
Constraints  : 5717054  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 6.55s
Memory:		 820MB (+0MB)
UNKNOWN
Iteration Time:	 6.60s

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         : 349.166s (Solving: 323.96s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 349.132s

Choices      : 6350585  (Domain: 6174626)
Conflicts    : 359395   (Analyzed: 359391)
Restarts     : 4296     (Average: 83.66 Last: 214)
Model-Level  : 348.0   
Problems     : 48       (Average Length: 66.58 Splits: 0)
Lemmas       : 359391   (Deleted: 332522)
  Binary     : 8846     (Ratio:   2.46%)
  Ternary    : 2359     (Ratio:   0.66%)
  Conflict   : 359391   (Average Length:  358.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 359391   (Average: 16.06 Max: 1044 Sum: 5771957)
  Executed   : 359273   (Average: 16.05 Max: 1044 Sum: 5767771 Ratio:  99.93%)
  Bounded    : 118      (Average: 35.47 Max: 102 Sum:   4186 Ratio:   0.07%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 781475   (Eliminated:    0 Frozen: 240994)
Constraints  : 5717054  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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         : 356.395s (Solving: 331.03s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 356.364s

Choices      : 6501579  (Domain: 6324416)
Conflicts    : 367161   (Analyzed: 367157)
Restarts     : 4396     (Average: 83.52 Last: 214)
Model-Level  : 348.0   
Problems     : 49       (Average Length: 67.31 Splits: 0)
Lemmas       : 367157   (Deleted: 339681)
  Binary     : 8975     (Ratio:   2.44%)
  Ternary    : 2401     (Ratio:   0.65%)
  Conflict   : 367157   (Average Length:  356.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 367157   (Average: 16.09 Max: 1044 Sum: 5909154)
  Executed   : 367038   (Average: 16.08 Max: 1044 Sum: 5904866 Ratio:  99.93%)
  Bounded    : 119      (Average: 36.03 Max: 102 Sum:   4288 Ratio:   0.07%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 781475   (Eliminated:    0 Frozen: 240994)
Constraints  : 5717054  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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         : 363.527s (Solving: 338.00s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 363.500s

Choices      : 6624745  (Domain: 6447201)
Conflicts    : 375078   (Analyzed: 375074)
Restarts     : 4496     (Average: 83.42 Last: 214)
Model-Level  : 348.0   
Problems     : 50       (Average Length: 68.00 Splits: 0)
Lemmas       : 375074   (Deleted: 347057)
  Binary     : 9055     (Ratio:   2.41%)
  Ternary    : 2415     (Ratio:   0.64%)
  Conflict   : 375074   (Average Length:  354.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 375074   (Average: 16.05 Max: 1044 Sum: 6018956)
  Executed   : 374954   (Average: 16.04 Max: 1044 Sum: 6014566 Ratio:  99.93%)
  Bounded    : 120      (Average: 36.58 Max: 102 Sum:   4390 Ratio:   0.07%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 781475   (Eliminated:    0 Frozen: 240994)
Constraints  : 5717040  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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         : 370.247s (Solving: 344.57s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 370.220s

Choices      : 6728640  (Domain: 6550981)
Conflicts    : 382993   (Analyzed: 382989)
Restarts     : 4596     (Average: 83.33 Last: 214)
Model-Level  : 348.0   
Problems     : 51       (Average Length: 68.67 Splits: 0)
Lemmas       : 382989   (Deleted: 354634)
  Binary     : 9093     (Ratio:   2.37%)
  Ternary    : 2430     (Ratio:   0.63%)
  Conflict   : 382989   (Average Length:  351.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 382989   (Average: 15.95 Max: 1044 Sum: 6108381)
  Executed   : 382869   (Average: 15.94 Max: 1044 Sum: 6103991 Ratio:  99.93%)
  Bounded    : 120      (Average: 36.58 Max: 102 Sum:   4390 Ratio:   0.07%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 781475   (Eliminated:    0 Frozen: 240994)
Constraints  : 5717026  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 6.67s
Memory:		 820MB (+0MB)
UNKNOWN
Iteration Time:	 6.73s

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         : 378.307s (Solving: 352.48s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 378.284s

Choices      : 6768919  (Domain: 6591260)
Conflicts    : 390394   (Analyzed: 390390)
Restarts     : 4696     (Average: 83.13 Last: 214)
Model-Level  : 348.0   
Problems     : 52       (Average Length: 69.31 Splits: 0)
Lemmas       : 390390   (Deleted: 362189)
  Binary     : 9107     (Ratio:   2.33%)
  Ternary    : 2440     (Ratio:   0.63%)
  Conflict   : 390390   (Average Length:  349.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 390390   (Average: 15.72 Max: 1044 Sum: 6135235)
  Executed   : 390270   (Average: 15.70 Max: 1044 Sum: 6130845 Ratio:  99.93%)
  Bounded    : 120      (Average: 36.58 Max: 102 Sum:   4390 Ratio:   0.07%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 781475   (Eliminated:    0 Frozen: 240994)
Constraints  : 5717026  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 8.01s
Memory:		 820MB (+0MB)
UNKNOWN
Iteration Time:	 8.07s

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         : 386.409s (Solving: 360.40s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 386.388s

Choices      : 6941192  (Domain: 6763308)
Conflicts    : 398090   (Analyzed: 398086)
Restarts     : 4796     (Average: 83.00 Last: 214)
Model-Level  : 348.0   
Problems     : 53       (Average Length: 69.92 Splits: 0)
Lemmas       : 398086   (Deleted: 369309)
  Binary     : 9194     (Ratio:   2.31%)
  Ternary    : 2484     (Ratio:   0.62%)
  Conflict   : 398086   (Average Length:  348.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 398086   (Average: 15.80 Max: 1067 Sum: 6290985)
  Executed   : 397966   (Average: 15.79 Max: 1067 Sum: 6286595 Ratio:  99.93%)
  Bounded    : 120      (Average: 36.58 Max: 102 Sum:   4390 Ratio:   0.07%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 781475   (Eliminated:    0 Frozen: 240994)
Constraints  : 5717026  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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         : 396.654s (Solving: 370.50s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 396.640s

Choices      : 7110381  (Domain: 6932210)
Conflicts    : 405934   (Analyzed: 405930)
Restarts     : 4896     (Average: 82.91 Last: 214)
Model-Level  : 348.0   
Problems     : 54       (Average Length: 70.52 Splits: 0)
Lemmas       : 405930   (Deleted: 376743)
  Binary     : 9284     (Ratio:   2.29%)
  Ternary    : 2520     (Ratio:   0.62%)
  Conflict   : 405930   (Average Length:  346.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 405930   (Average: 15.87 Max: 1067 Sum: 6443025)
  Executed   : 405810   (Average: 15.86 Max: 1067 Sum: 6438635 Ratio:  99.93%)
  Bounded    : 120      (Average: 36.58 Max: 102 Sum:   4390 Ratio:   0.07%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 781475   (Eliminated:    0 Frozen: 240994)
Constraints  : 5717026  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 10.20s
Memory:		 820MB (+0MB)
UNKNOWN
Iteration Time:	 10.25s

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

Models       : 0+
Calls        : 55
Time         : 406.041s (Solving: 378.62s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 406.028s

Choices      : 7187621  (Domain: 7009435)
Conflicts    : 413721   (Analyzed: 413717)
Restarts     : 4996     (Average: 82.81 Last: 214)
Model-Level  : 348.0   
Problems     : 55       (Average Length: 71.18 Splits: 0)
Lemmas       : 413717   (Deleted: 384315)
  Binary     : 9317     (Ratio:   2.25%)
  Ternary    : 2524     (Ratio:   0.61%)
  Conflict   : 413717   (Average Length:  346.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 413717   (Average: 15.69 Max: 1067 Sum: 6492913)
  Executed   : 413597   (Average: 15.68 Max: 1067 Sum: 6488523 Ratio:  99.93%)
  Bounded    : 120      (Average: 36.58 Max: 102 Sum:   4390 Ratio:   0.07%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 821551   (Eliminated:    0 Frozen: 253444)
Constraints  : 6019006  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 8.28s
Memory:		 846MB (+25MB)
UNKNOWN
Iteration Time:	 9.41s

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

Models       : 0+
Calls        : 56
Time         : 415.389s (Solving: 386.72s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 415.380s

Choices      : 7250869  (Domain: 7072681)
Conflicts    : 421495   (Analyzed: 421491)
Restarts     : 5096     (Average: 82.71 Last: 214)
Model-Level  : 348.0   
Problems     : 56       (Average Length: 71.91 Splits: 0)
Lemmas       : 421491   (Deleted: 392012)
  Binary     : 9334     (Ratio:   2.21%)
  Ternary    : 2525     (Ratio:   0.60%)
  Conflict   : 421491   (Average Length:  347.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 421491   (Average: 15.49 Max: 1067 Sum: 6529068)
  Executed   : 421371   (Average: 15.48 Max: 1067 Sum: 6524678 Ratio:  99.93%)
  Bounded    : 120      (Average: 36.58 Max: 102 Sum:   4390 Ratio:   0.07%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 861627   (Eliminated:    0 Frozen: 265894)
Constraints  : 6320986  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 8.26s
Memory:		 880MB (+34MB)
UNKNOWN
Iteration Time:	 9.36s

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

Models       : 0+
Calls        : 57
Time         : 425.095s (Solving: 395.15s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 425.088s

Choices      : 7350756  (Domain: 7172422)
Conflicts    : 429176   (Analyzed: 429172)
Restarts     : 5196     (Average: 82.60 Last: 214)
Model-Level  : 348.0   
Problems     : 57       (Average Length: 72.70 Splits: 0)
Lemmas       : 429172   (Deleted: 399632)
  Binary     : 9379     (Ratio:   2.19%)
  Ternary    : 2528     (Ratio:   0.59%)
  Conflict   : 429172   (Average Length:  347.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 429172   (Average: 15.38 Max: 1075 Sum: 6601114)
  Executed   : 429052   (Average: 15.37 Max: 1075 Sum: 6596724 Ratio:  99.93%)
  Bounded    : 120      (Average: 36.58 Max: 102 Sum:   4390 Ratio:   0.07%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 901703   (Eliminated:    0 Frozen: 278344)
Constraints  : 6622966  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 8.59s
Memory:		 909MB (+29MB)
UNKNOWN
Iteration Time:	 9.72s

Iteration 57
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,True), (12,60,3,False), (13,65,3,False), (14,70,2,True), (15,75,2,True), (16,80,2,True), (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), (24,120,0,True)]
Grounded Until:	 115
Blocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 58
Time         : 430.901s (Solving: 400.78s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 430.896s

Choices      : 7389877  (Domain: 7211543)
Conflicts    : 437454   (Analyzed: 437450)
Restarts     : 5296     (Average: 82.60 Last: 214)
Model-Level  : 348.0   
Problems     : 58       (Average Length: 73.47 Splits: 0)
Lemmas       : 437450   (Deleted: 407203)
  Binary     : 9411     (Ratio:   2.15%)
  Ternary    : 2531     (Ratio:   0.58%)
  Conflict   : 437450   (Average Length:  345.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 437450   (Average: 15.16 Max: 1075 Sum: 6633301)
  Executed   : 437330   (Average: 15.15 Max: 1075 Sum: 6628911 Ratio:  99.93%)
  Bounded    : 120      (Average: 36.58 Max: 102 Sum:   4390 Ratio:   0.07%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 901703   (Eliminated:    0 Frozen: 278344)
Constraints  : 6622966  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

Iteration 58
Queue:		 [(6,30,4,True), (7,35,3,True), (8,40,3,True), (9,45,3,True), (10,50,3,True), (11,55,3,True), (12,60,3,False), (13,65,3,False), (14,70,2,True), (15,75,2,True), (16,80,2,True), (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), (24,120,0,True)]
Grounded Until:	 115
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 59
Time         : 437.058s (Solving: 406.74s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 437.056s

Choices      : 7448120  (Domain: 7269785)
Conflicts    : 445177   (Analyzed: 445173)
Restarts     : 5396     (Average: 82.50 Last: 214)
Model-Level  : 348.0   
Problems     : 59       (Average Length: 74.20 Splits: 0)
Lemmas       : 445173   (Deleted: 414958)
  Binary     : 9571     (Ratio:   2.15%)
  Ternary    : 2570     (Ratio:   0.58%)
  Conflict   : 445173   (Average Length:  343.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 445173   (Average: 15.02 Max: 1075 Sum: 6684607)
  Executed   : 445050   (Average: 15.01 Max: 1075 Sum: 6679880 Ratio:  99.93%)
  Bounded    : 123      (Average: 38.43 Max: 114 Sum:   4727 Ratio:   0.07%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 901703   (Eliminated:    0 Frozen: 278344)
Constraints  : 6622966  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

Iteration 59
Queue:		 [(7,35,3,True), (8,40,3,True), (9,45,3,True), (10,50,3,True), (11,55,3,True), (12,60,3,False), (13,65,3,False), (14,70,2,True), (15,75,2,True), (16,80,2,True), (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), (24,120,0,True)]
Grounded Until:	 115
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 60
Time         : 448.485s (Solving: 417.98s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 448.488s

Choices      : 7548724  (Domain: 7367917)
Conflicts    : 453930   (Analyzed: 453926)
Restarts     : 5496     (Average: 82.59 Last: 214)
Model-Level  : 348.0   
Problems     : 60       (Average Length: 74.92 Splits: 0)
Lemmas       : 453926   (Deleted: 424300)
  Binary     : 9845     (Ratio:   2.17%)
  Ternary    : 2613     (Ratio:   0.58%)
  Conflict   : 453926   (Average Length:  352.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 453926   (Average: 14.91 Max: 1075 Sum: 6767060)
  Executed   : 453801   (Average: 14.90 Max: 1075 Sum: 6762105 Ratio:  99.93%)
  Bounded    : 125      (Average: 39.64 Max: 117 Sum:   4955 Ratio:   0.07%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 901703   (Eliminated:    0 Frozen: 278344)
Constraints  : 6622966  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 11.36s
Memory:		 909MB (+0MB)
UNKNOWN
Iteration Time:	 11.43s

Iteration 60
Queue:		 [(8,40,3,True), (9,45,3,True), (10,50,3,True), (11,55,3,True), (12,60,3,False), (13,65,3,False), (14,70,2,True), (15,75,2,True), (16,80,2,True), (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), (24,120,0,True)]
Grounded Until:	 115
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 61
Time         : 454.057s (Solving: 423.37s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 454.060s

Choices      : 7613016  (Domain: 7431800)
Conflicts    : 462470   (Analyzed: 462466)
Restarts     : 5596     (Average: 82.64 Last: 214)
Model-Level  : 348.0   
Problems     : 61       (Average Length: 75.61 Splits: 0)
Lemmas       : 462466   (Deleted: 430623)
  Binary     : 9920     (Ratio:   2.15%)
  Ternary    : 2646     (Ratio:   0.57%)
  Conflict   : 462466   (Average Length:  351.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 462466   (Average: 14.75 Max: 1075 Sum: 6820827)
  Executed   : 462341   (Average: 14.74 Max: 1075 Sum: 6815872 Ratio:  99.93%)
  Bounded    : 125      (Average: 39.64 Max: 117 Sum:   4955 Ratio:   0.07%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 901703   (Eliminated:    0 Frozen: 278344)
Constraints  : 6622952  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

Iteration 61
Queue:		 [(9,45,3,True), (10,50,3,True), (11,55,3,True), (12,60,3,False), (13,65,3,False), (14,70,2,True), (15,75,2,True), (16,80,2,True), (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), (24,120,0,True)]
Grounded Until:	 115
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 62
Time         : 460.312s (Solving: 429.42s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 460.316s

Choices      : 7688868  (Domain: 7507463)
Conflicts    : 470281   (Analyzed: 470277)
Restarts     : 5696     (Average: 82.56 Last: 214)
Model-Level  : 348.0   
Problems     : 62       (Average Length: 76.27 Splits: 0)
Lemmas       : 470277   (Deleted: 438577)
  Binary     : 9986     (Ratio:   2.12%)
  Ternary    : 2687     (Ratio:   0.57%)
  Conflict   : 470277   (Average Length:  349.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 470277   (Average: 14.64 Max: 1075 Sum: 6886245)
  Executed   : 470152   (Average: 14.63 Max: 1075 Sum: 6881290 Ratio:  99.93%)
  Bounded    : 125      (Average: 39.64 Max: 117 Sum:   4955 Ratio:   0.07%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 901703   (Eliminated:    0 Frozen: 278344)
Constraints  : 6622952  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

Iteration 62
Queue:		 [(10,50,3,True), (11,55,3,True), (12,60,3,False), (13,65,3,False), (14,70,2,True), (15,75,2,True), (16,80,2,True), (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), (24,120,0,True)]
Grounded Until:	 115
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 63
Time         : 473.429s (Solving: 442.33s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 473.436s

Choices      : 7897338  (Domain: 7714318)
Conflicts    : 479315   (Analyzed: 479311)
Restarts     : 5796     (Average: 82.70 Last: 214)
Model-Level  : 348.0   
Problems     : 63       (Average Length: 76.92 Splits: 0)
Lemmas       : 479311   (Deleted: 447758)
  Binary     : 10516    (Ratio:   2.19%)
  Ternary    : 2885     (Ratio:   0.60%)
  Conflict   : 479311   (Average Length:  352.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 479311   (Average: 14.76 Max: 1075 Sum: 7074200)
  Executed   : 479186   (Average: 14.75 Max: 1075 Sum: 7069245 Ratio:  99.93%)
  Bounded    : 125      (Average: 39.64 Max: 117 Sum:   4955 Ratio:   0.07%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 901703   (Eliminated:    0 Frozen: 278344)
Constraints  : 6622952  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 13.05s
Memory:		 909MB (+0MB)
UNKNOWN
Iteration Time:	 13.13s

Iteration 63
Queue:		 [(11,55,3,True), (12,60,3,False), (13,65,3,False), (14,70,2,True), (15,75,2,True), (16,80,2,True), (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), (24,120,0,True)]
Grounded Until:	 115
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 64
Time         : 477.614s (Solving: 446.30s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 477.620s

Choices      : 7950691  (Domain: 7767431)
Conflicts    : 487565   (Analyzed: 487561)
Restarts     : 5896     (Average: 82.69 Last: 214)
Model-Level  : 348.0   
Problems     : 64       (Average Length: 77.55 Splits: 0)
Lemmas       : 487561   (Deleted: 453832)
  Binary     : 10560    (Ratio:   2.17%)
  Ternary    : 2906     (Ratio:   0.60%)
  Conflict   : 487561   (Average Length:  350.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 487561   (Average: 14.60 Max: 1075 Sum: 7117126)
  Executed   : 487436   (Average: 14.59 Max: 1075 Sum: 7112171 Ratio:  99.93%)
  Bounded    : 125      (Average: 39.64 Max: 117 Sum:   4955 Ratio:   0.07%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 901703   (Eliminated:    0 Frozen: 278344)
Constraints  : 6622952  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

Iteration 64
Queue:		 [(14,70,2,True), (15,75,2,True), (16,80,2,True), (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), (24,120,0,True)]
Grounded Until:	 115
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 65
Time         : 483.183s (Solving: 451.65s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 483.192s

Choices      : 8034044  (Domain: 7850625)
Conflicts    : 495275   (Analyzed: 495271)
Restarts     : 5996     (Average: 82.60 Last: 214)
Model-Level  : 348.0   
Problems     : 65       (Average Length: 78.15 Splits: 0)
Lemmas       : 495271   (Deleted: 461881)
  Binary     : 10585    (Ratio:   2.14%)
  Ternary    : 2918     (Ratio:   0.59%)
  Conflict   : 495271   (Average Length:  348.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 495271   (Average: 14.51 Max: 1075 Sum: 7187063)
  Executed   : 495144   (Average: 14.50 Max: 1075 Sum: 7181874 Ratio:  99.93%)
  Bounded    : 127      (Average: 40.86 Max: 117 Sum:   5189 Ratio:   0.07%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 901703   (Eliminated:    0 Frozen: 278344)
Constraints  : 6622952  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 5.49s
Memory:		 909MB (+0MB)
UNKNOWN
Iteration Time:	 5.57s

Iteration 65
Queue:		 [(15,75,2,True), (16,80,2,True), (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), (24,120,0,True)]
Grounded Until:	 115
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 66
Time         : 488.959s (Solving: 457.25s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 488.972s

Choices      : 8079573  (Domain: 7896154)
Conflicts    : 503220   (Analyzed: 503216)
Restarts     : 6096     (Average: 82.55 Last: 214)
Model-Level  : 348.0   
Problems     : 66       (Average Length: 78.74 Splits: 0)
Lemmas       : 503216   (Deleted: 469339)
  Binary     : 10626    (Ratio:   2.11%)
  Ternary    : 2925     (Ratio:   0.58%)
  Conflict   : 503216   (Average Length:  346.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 503216   (Average: 14.35 Max: 1075 Sum: 7219896)
  Executed   : 503087   (Average: 14.34 Max: 1075 Sum: 7214478 Ratio:  99.92%)
  Bounded    : 129      (Average: 42.00 Max: 117 Sum:   5418 Ratio:   0.08%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 901703   (Eliminated:    0 Frozen: 278344)
Constraints  : 6622925  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 67
Time         : 499.100s (Solving: 467.21s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 499.116s

Choices      : 8361486  (Domain: 8175976)
Conflicts    : 511095   (Analyzed: 511091)
Restarts     : 6196     (Average: 82.49 Last: 214)
Model-Level  : 348.0   
Problems     : 67       (Average Length: 79.31 Splits: 0)
Lemmas       : 511091   (Deleted: 476944)
  Binary     : 10809    (Ratio:   2.11%)
  Ternary    : 2966     (Ratio:   0.58%)
  Conflict   : 511091   (Average Length:  346.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 511091   (Average: 14.64 Max: 1075 Sum: 7480880)
  Executed   : 510962   (Average: 14.63 Max: 1075 Sum: 7475462 Ratio:  99.93%)
  Bounded    : 129      (Average: 42.00 Max: 117 Sum:   5418 Ratio:   0.07%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 901703   (Eliminated:    0 Frozen: 278344)
Constraints  : 6622911  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 68
Time         : 505.651s (Solving: 473.58s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 505.668s

Choices      : 8526783  (Domain: 8341098)
Conflicts    : 518704   (Analyzed: 518700)
Restarts     : 6296     (Average: 82.39 Last: 214)
Model-Level  : 348.0   
Problems     : 68       (Average Length: 79.87 Splits: 0)
Lemmas       : 518700   (Deleted: 484447)
  Binary     : 10863    (Ratio:   2.09%)
  Ternary    : 2980     (Ratio:   0.57%)
  Conflict   : 518700   (Average Length:  346.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 518700   (Average: 14.70 Max: 1145 Sum: 7626218)
  Executed   : 518571   (Average: 14.69 Max: 1145 Sum: 7620800 Ratio:  99.93%)
  Bounded    : 129      (Average: 42.00 Max: 117 Sum:   5418 Ratio:   0.07%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 901703   (Eliminated:    0 Frozen: 278344)
Constraints  : 6622911  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 69
Time         : 514.218s (Solving: 481.97s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 514.236s

Choices      : 8724729  (Domain: 8538678)
Conflicts    : 526756   (Analyzed: 526752)
Restarts     : 6396     (Average: 82.36 Last: 214)
Model-Level  : 348.0   
Problems     : 69       (Average Length: 80.41 Splits: 0)
Lemmas       : 526752   (Deleted: 491754)
  Binary     : 10929    (Ratio:   2.07%)
  Ternary    : 3016     (Ratio:   0.57%)
  Conflict   : 526752   (Average Length:  345.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 526752   (Average: 14.82 Max: 1228 Sum: 7805112)
  Executed   : 526623   (Average: 14.81 Max: 1228 Sum: 7799694 Ratio:  99.93%)
  Bounded    : 129      (Average: 42.00 Max: 117 Sum:   5418 Ratio:   0.07%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 901703   (Eliminated:    0 Frozen: 278344)
Constraints  : 6622911  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 70
Time         : 519.253s (Solving: 486.83s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 519.272s

Choices      : 8828960  (Domain: 8642778)
Conflicts    : 534582   (Analyzed: 534578)
Restarts     : 6496     (Average: 82.29 Last: 214)
Model-Level  : 348.0   
Problems     : 70       (Average Length: 80.93 Splits: 0)
Lemmas       : 534578   (Deleted: 499516)
  Binary     : 10949    (Ratio:   2.05%)
  Ternary    : 3029     (Ratio:   0.57%)
  Conflict   : 534578   (Average Length:  344.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 534578   (Average: 14.76 Max: 1434 Sum: 7892307)
  Executed   : 534449   (Average: 14.75 Max: 1434 Sum: 7886889 Ratio:  99.93%)
  Bounded    : 129      (Average: 42.00 Max: 117 Sum:   5418 Ratio:   0.07%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 901703   (Eliminated:    0 Frozen: 278344)
Constraints  : 6622911  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 71
Time         : 528.623s (Solving: 494.88s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 528.644s

Choices      : 8901645  (Domain: 8715459)
Conflicts    : 542542   (Analyzed: 542538)
Restarts     : 6596     (Average: 82.25 Last: 214)
Model-Level  : 348.0   
Problems     : 71       (Average Length: 81.51 Splits: 0)
Lemmas       : 542538   (Deleted: 507211)
  Binary     : 10962    (Ratio:   2.02%)
  Ternary    : 3030     (Ratio:   0.56%)
  Conflict   : 542538   (Average Length:  344.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 542538   (Average: 14.63 Max: 1434 Sum: 7935112)
  Executed   : 542409   (Average: 14.62 Max: 1434 Sum: 7929694 Ratio:  99.93%)
  Bounded    : 129      (Average: 42.00 Max: 117 Sum:   5418 Ratio:   0.07%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 941779   (Eliminated:    0 Frozen: 290794)
Constraints  : 6924891  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 8.22s
Memory:		 931MB (+22MB)
UNKNOWN
Iteration Time:	 9.39s

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

Models       : 0+
Calls        : 72
Time         : 532.063s (Solving: 498.13s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 532.084s

Choices      : 8941425  (Domain: 8755239)
Conflicts    : 549980   (Analyzed: 549976)
Restarts     : 6696     (Average: 82.14 Last: 214)
Model-Level  : 348.0   
Problems     : 72       (Average Length: 82.07 Splits: 0)
Lemmas       : 549976   (Deleted: 514987)
  Binary     : 10980    (Ratio:   2.00%)
  Ternary    : 3031     (Ratio:   0.55%)
  Conflict   : 549976   (Average Length:  342.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 549976   (Average: 14.49 Max: 1434 Sum: 7966745)
  Executed   : 549847   (Average: 14.48 Max: 1434 Sum: 7961327 Ratio:  99.93%)
  Bounded    : 129      (Average: 42.00 Max: 117 Sum:   5418 Ratio:   0.07%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 941779   (Eliminated:    0 Frozen: 290794)
Constraints  : 6924891  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 3.38s
Memory:		 931MB (+0MB)
UNKNOWN
Iteration Time:	 3.44s

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

Models       : 0+
Calls        : 73
Time         : 536.360s (Solving: 502.24s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 536.376s

Choices      : 8986103  (Domain: 8799917)
Conflicts    : 558083   (Analyzed: 558079)
Restarts     : 6796     (Average: 82.12 Last: 214)
Model-Level  : 348.0   
Problems     : 73       (Average Length: 82.62 Splits: 0)
Lemmas       : 558079   (Deleted: 522273)
  Binary     : 10995    (Ratio:   1.97%)
  Ternary    : 3036     (Ratio:   0.54%)
  Conflict   : 558079   (Average Length:  341.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 558079   (Average: 14.34 Max: 1434 Sum: 8003780)
  Executed   : 557949   (Average: 14.33 Max: 1434 Sum: 7998240 Ratio:  99.93%)
  Bounded    : 130      (Average: 42.62 Max: 122 Sum:   5540 Ratio:   0.07%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 941779   (Eliminated:    0 Frozen: 290794)
Constraints  : 6924891  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 4.23s
Memory:		 931MB (+0MB)
UNKNOWN
Iteration Time:	 4.29s

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

Models       : 0+
Calls        : 74
Time         : 541.839s (Solving: 507.51s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 541.860s

Choices      : 9041602  (Domain: 8854198)
Conflicts    : 566400   (Analyzed: 566396)
Restarts     : 6896     (Average: 82.13 Last: 214)
Model-Level  : 348.0   
Problems     : 74       (Average Length: 83.15 Splits: 0)
Lemmas       : 566396   (Deleted: 530036)
  Binary     : 11055    (Ratio:   1.95%)
  Ternary    : 3052     (Ratio:   0.54%)
  Conflict   : 566396   (Average Length:  341.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 566396   (Average: 14.21 Max: 1434 Sum: 8049061)
  Executed   : 566266   (Average: 14.20 Max: 1434 Sum: 8043521 Ratio:  99.93%)
  Bounded    : 130      (Average: 42.62 Max: 122 Sum:   5540 Ratio:   0.07%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 941779   (Eliminated:    0 Frozen: 290794)
Constraints  : 6924877  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 75
Time         : 548.594s (Solving: 514.04s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 548.620s

Choices      : 9108821  (Domain: 8920020)
Conflicts    : 574597   (Analyzed: 574593)
Restarts     : 6996     (Average: 82.13 Last: 214)
Model-Level  : 348.0   
Problems     : 75       (Average Length: 83.67 Splits: 0)
Lemmas       : 574593   (Deleted: 537997)
  Binary     : 11159    (Ratio:   1.94%)
  Ternary    : 3088     (Ratio:   0.54%)
  Conflict   : 574593   (Average Length:  342.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 574593   (Average: 14.10 Max: 1434 Sum: 8100938)
  Executed   : 574463   (Average: 14.09 Max: 1434 Sum: 8095398 Ratio:  99.93%)
  Bounded    : 130      (Average: 42.62 Max: 122 Sum:   5540 Ratio:   0.07%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 941779   (Eliminated:    0 Frozen: 290794)
Constraints  : 6924877  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 76
Time         : 555.786s (Solving: 521.03s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 555.816s

Choices      : 9177205  (Domain: 8988304)
Conflicts    : 582955   (Analyzed: 582951)
Restarts     : 7096     (Average: 82.15 Last: 214)
Model-Level  : 348.0   
Problems     : 76       (Average Length: 84.17 Splits: 0)
Lemmas       : 582951   (Deleted: 545939)
  Binary     : 11237    (Ratio:   1.93%)
  Ternary    : 3112     (Ratio:   0.53%)
  Conflict   : 582951   (Average Length:  341.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 582951   (Average: 14.00 Max: 1434 Sum: 8159376)
  Executed   : 582818   (Average: 13.99 Max: 1434 Sum: 8153476 Ratio:  99.93%)
  Bounded    : 133      (Average: 44.36 Max: 122 Sum:   5900 Ratio:   0.07%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 941779   (Eliminated:    0 Frozen: 290794)
Constraints  : 6924877  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 77
Time         : 560.989s (Solving: 526.04s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 561.024s

Choices      : 9241046  (Domain: 9052008)
Conflicts    : 590799   (Analyzed: 590795)
Restarts     : 7196     (Average: 82.10 Last: 214)
Model-Level  : 348.0   
Problems     : 77       (Average Length: 84.66 Splits: 0)
Lemmas       : 590795   (Deleted: 553934)
  Binary     : 11262    (Ratio:   1.91%)
  Ternary    : 3121     (Ratio:   0.53%)
  Conflict   : 590795   (Average Length:  340.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 590795   (Average: 13.90 Max: 1434 Sum: 8213117)
  Executed   : 590662   (Average: 13.89 Max: 1434 Sum: 8207217 Ratio:  99.93%)
  Bounded    : 133      (Average: 44.36 Max: 122 Sum:   5900 Ratio:   0.07%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 941779   (Eliminated:    0 Frozen: 290794)
Constraints  : 6924863  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 78
Time         : 565.281s (Solving: 530.14s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 565.320s

Choices      : 9306925  (Domain: 9117401)
Conflicts    : 598418   (Analyzed: 598414)
Restarts     : 7296     (Average: 82.02 Last: 214)
Model-Level  : 348.0   
Problems     : 78       (Average Length: 85.14 Splits: 0)
Lemmas       : 598414   (Deleted: 561668)
  Binary     : 11302    (Ratio:   1.89%)
  Ternary    : 3130     (Ratio:   0.52%)
  Conflict   : 598414   (Average Length:  340.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 598414   (Average: 13.81 Max: 1434 Sum: 8265315)
  Executed   : 598281   (Average: 13.80 Max: 1434 Sum: 8259415 Ratio:  99.93%)
  Bounded    : 133      (Average: 44.36 Max: 122 Sum:   5900 Ratio:   0.07%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 941779   (Eliminated:    0 Frozen: 290794)
Constraints  : 6924863  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 79
Time         : 569.080s (Solving: 533.74s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 569.120s

Choices      : 9360966  (Domain: 9171391)
Conflicts    : 606279   (Analyzed: 606275)
Restarts     : 7396     (Average: 81.97 Last: 214)
Model-Level  : 348.0   
Problems     : 79       (Average Length: 85.61 Splits: 0)
Lemmas       : 606275   (Deleted: 569078)
  Binary     : 11318    (Ratio:   1.87%)
  Ternary    : 3133     (Ratio:   0.52%)
  Conflict   : 606275   (Average Length:  338.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 606275   (Average: 13.70 Max: 1434 Sum: 8307612)
  Executed   : 606141   (Average: 13.69 Max: 1434 Sum: 8301590 Ratio:  99.93%)
  Bounded    : 134      (Average: 44.94 Max: 122 Sum:   6022 Ratio:   0.07%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 941779   (Eliminated:    0 Frozen: 290794)
Constraints  : 6924863  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 80
Time         : 572.428s (Solving: 536.88s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 572.472s

Choices      : 9406256  (Domain: 9216677)
Conflicts    : 613218   (Analyzed: 613214)
Restarts     : 7496     (Average: 81.81 Last: 214)
Model-Level  : 348.0   
Problems     : 80       (Average Length: 86.06 Splits: 0)
Lemmas       : 613214   (Deleted: 576831)
  Binary     : 11334    (Ratio:   1.85%)
  Ternary    : 3136     (Ratio:   0.51%)
  Conflict   : 613214   (Average Length:  337.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 613214   (Average: 13.60 Max: 1434 Sum: 8336923)
  Executed   : 613079   (Average: 13.59 Max: 1434 Sum: 8330779 Ratio:  99.93%)
  Bounded    : 135      (Average: 45.51 Max: 122 Sum:   6144 Ratio:   0.07%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 941779   (Eliminated:    0 Frozen: 290794)
Constraints  : 6924837  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 3.27s
Memory:		 931MB (+0MB)
UNKNOWN
Iteration Time:	 3.35s

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

Models       : 0+
Calls        : 81
Time         : 576.952s (Solving: 541.19s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 577.000s

Choices      : 9518131  (Domain: 9328170)
Conflicts    : 620523   (Analyzed: 620519)
Restarts     : 7596     (Average: 81.69 Last: 214)
Model-Level  : 348.0   
Problems     : 81       (Average Length: 86.51 Splits: 0)
Lemmas       : 620519   (Deleted: 583450)
  Binary     : 11397    (Ratio:   1.84%)
  Ternary    : 3202     (Ratio:   0.52%)
  Conflict   : 620519   (Average Length:  336.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 620519   (Average: 13.59 Max: 1434 Sum: 8433418)
  Executed   : 620384   (Average: 13.58 Max: 1434 Sum: 8427274 Ratio:  99.93%)
  Bounded    : 135      (Average: 45.51 Max: 122 Sum:   6144 Ratio:   0.07%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 941779   (Eliminated:    0 Frozen: 290794)
Constraints  : 6924823  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 82
Time         : 586.864s (Solving: 550.90s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 586.916s

Choices      : 9909997  (Domain: 9718384)
Conflicts    : 628369   (Analyzed: 628365)
Restarts     : 7696     (Average: 81.65 Last: 214)
Model-Level  : 348.0   
Problems     : 82       (Average Length: 86.94 Splits: 0)
Lemmas       : 628365   (Deleted: 590616)
  Binary     : 11581    (Ratio:   1.84%)
  Ternary    : 3321     (Ratio:   0.53%)
  Conflict   : 628365   (Average Length:  335.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 628365   (Average: 14.00 Max: 1434 Sum: 8797556)
  Executed   : 628230   (Average: 13.99 Max: 1434 Sum: 8791412 Ratio:  99.93%)
  Bounded    : 135      (Average: 45.51 Max: 122 Sum:   6144 Ratio:   0.07%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 941779   (Eliminated:    0 Frozen: 290794)
Constraints  : 6924823  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 9.84s
Memory:		 931MB (+0MB)
UNKNOWN
Iteration Time:	 9.92s

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

Models       : 0+
Calls        : 83
Time         : 591.700s (Solving: 555.52s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 591.756s

Choices      : 9953210  (Domain: 9761597)
Conflicts    : 636141   (Analyzed: 636137)
Restarts     : 7796     (Average: 81.60 Last: 214)
Model-Level  : 348.0   
Problems     : 83       (Average Length: 87.36 Splits: 0)
Lemmas       : 636137   (Deleted: 597823)
  Binary     : 11610    (Ratio:   1.83%)
  Ternary    : 3325     (Ratio:   0.52%)
  Conflict   : 636137   (Average Length:  335.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 636137   (Average: 13.89 Max: 1434 Sum: 8833375)
  Executed   : 636001   (Average: 13.88 Max: 1434 Sum: 8827109 Ratio:  99.93%)
  Bounded    : 136      (Average: 46.07 Max: 122 Sum:   6266 Ratio:   0.07%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 941779   (Eliminated:    0 Frozen: 290794)
Constraints  : 6924823  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 4.75s
Memory:		 995MB (+64MB)
UNKNOWN
Iteration Time:	 4.84s

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

Models       : 0+
Calls        : 84
Time         : 596.602s (Solving: 560.23s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 596.656s

Choices      : 9997769  (Domain: 9806156)
Conflicts    : 644177   (Analyzed: 644173)
Restarts     : 7896     (Average: 81.58 Last: 214)
Model-Level  : 348.0   
Problems     : 84       (Average Length: 87.77 Splits: 0)
Lemmas       : 644173   (Deleted: 605304)
  Binary     : 11629    (Ratio:   1.81%)
  Ternary    : 3333     (Ratio:   0.52%)
  Conflict   : 644173   (Average Length:  334.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 644173   (Average: 13.77 Max: 1434 Sum: 8870198)
  Executed   : 644037   (Average: 13.76 Max: 1434 Sum: 8863932 Ratio:  99.93%)
  Bounded    : 136      (Average: 46.07 Max: 122 Sum:   6266 Ratio:   0.07%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 941779   (Eliminated:    0 Frozen: 290794)
Constraints  : 6924809  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 85
Time         : 607.111s (Solving: 570.52s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 607.172s

Choices      : 10078777 (Domain: 9885715)
Conflicts    : 652851   (Analyzed: 652847)
Restarts     : 7996     (Average: 81.65 Last: 214)
Model-Level  : 348.0   
Problems     : 85       (Average Length: 88.18 Splits: 0)
Lemmas       : 652847   (Deleted: 615190)
  Binary     : 11841    (Ratio:   1.81%)
  Ternary    : 3351     (Ratio:   0.51%)
  Conflict   : 652847   (Average Length:  345.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 652847   (Average: 13.68 Max: 1434 Sum: 8929650)
  Executed   : 652711   (Average: 13.67 Max: 1434 Sum: 8923384 Ratio:  99.93%)
  Bounded    : 136      (Average: 46.07 Max: 122 Sum:   6266 Ratio:   0.07%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 941779   (Eliminated:    0 Frozen: 290794)
Constraints  : 6924809  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 10.43s
Memory:		 995MB (+0MB)
UNKNOWN
Iteration Time:	 10.52s

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

Models       : 0+
Calls        : 86
Time         : 612.980s (Solving: 576.20s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 613.036s

Choices      : 10137568 (Domain: 9944257)
Conflicts    : 661143   (Analyzed: 661139)
Restarts     : 8096     (Average: 81.66 Last: 214)
Model-Level  : 348.0   
Problems     : 86       (Average Length: 88.57 Splits: 0)
Lemmas       : 661139   (Deleted: 621405)
  Binary     : 11909    (Ratio:   1.80%)
  Ternary    : 3368     (Ratio:   0.51%)
  Conflict   : 661139   (Average Length:  345.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 661139   (Average: 13.58 Max: 1434 Sum: 8978213)
  Executed   : 661002   (Average: 13.57 Max: 1434 Sum: 8971825 Ratio:  99.93%)
  Bounded    : 137      (Average: 46.63 Max: 122 Sum:   6388 Ratio:   0.07%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 941779   (Eliminated:    0 Frozen: 290794)
Constraints  : 6924809  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 87
Time         : 620.987s (Solving: 584.00s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 621.044s

Choices      : 10226166 (Domain: 10032475)
Conflicts    : 669505   (Analyzed: 669501)
Restarts     : 8196     (Average: 81.69 Last: 214)
Model-Level  : 348.0   
Problems     : 87       (Average Length: 88.95 Splits: 0)
Lemmas       : 669501   (Deleted: 629315)
  Binary     : 11995    (Ratio:   1.79%)
  Ternary    : 3411     (Ratio:   0.51%)
  Conflict   : 669501   (Average Length:  344.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 669501   (Average: 13.53 Max: 1434 Sum: 9055619)
  Executed   : 669363   (Average: 13.52 Max: 1434 Sum: 9049109 Ratio:  99.93%)
  Bounded    : 138      (Average: 47.17 Max: 122 Sum:   6510 Ratio:   0.07%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 941779   (Eliminated:    0 Frozen: 290794)
Constraints  : 6924795  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

Iteration 87
Queue:		 [(11,55,4,True), (12,60,4,False), (13,65,4,False), (14,70,3,True), (15,75,3,False), (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), (24,120,2,False)]
Grounded Until:	 120
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 88
Time         : 625.361s (Solving: 588.16s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 625.420s

Choices      : 10288258 (Domain: 10094446)
Conflicts    : 676763   (Analyzed: 676759)
Restarts     : 8296     (Average: 81.58 Last: 214)
Model-Level  : 348.0   
Problems     : 88       (Average Length: 89.33 Splits: 0)
Lemmas       : 676759   (Deleted: 637510)
  Binary     : 12027    (Ratio:   1.78%)
  Ternary    : 3416     (Ratio:   0.50%)
  Conflict   : 676759   (Average Length:  343.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 676759   (Average: 13.46 Max: 1434 Sum: 9106913)
  Executed   : 676620   (Average: 13.45 Max: 1434 Sum: 9100281 Ratio:  99.93%)
  Bounded    : 139      (Average: 47.71 Max: 122 Sum:   6632 Ratio:   0.07%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 941779   (Eliminated:    0 Frozen: 290794)
Constraints  : 6924782  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 4.29s
Memory:		 995MB (+0MB)
UNKNOWN
Iteration Time:	 4.38s

Iteration 88
Queue:		 [(14,70,3,True), (15,75,3,False), (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), (24,120,2,False)]
Grounded Until:	 120
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 89
Time         : 641.492s (Solving: 604.09s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 641.548s

Choices      : 10626114 (Domain: 10429575)
Conflicts    : 685522   (Analyzed: 685518)
Restarts     : 8396     (Average: 81.65 Last: 214)
Model-Level  : 348.0   
Problems     : 89       (Average Length: 89.70 Splits: 0)
Lemmas       : 685518   (Deleted: 646177)
  Binary     : 12549    (Ratio:   1.83%)
  Ternary    : 3520     (Ratio:   0.51%)
  Conflict   : 685518   (Average Length:  346.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 685518   (Average: 13.74 Max: 1434 Sum: 9419631)
  Executed   : 685379   (Average: 13.73 Max: 1434 Sum: 9412999 Ratio:  99.93%)
  Bounded    : 139      (Average: 47.71 Max: 122 Sum:   6632 Ratio:   0.07%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 941779   (Eliminated:    0 Frozen: 290794)
Constraints  : 6924768  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 16.05s
Memory:		 995MB (+0MB)
UNKNOWN
Iteration Time:	 16.13s

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

Models       : 0+
Calls        : 90
Time         : 645.343s (Solving: 607.76s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 645.400s

Choices      : 10690617 (Domain: 10494073)
Conflicts    : 692780   (Analyzed: 692776)
Restarts     : 8496     (Average: 81.54 Last: 214)
Model-Level  : 348.0   
Problems     : 90       (Average Length: 90.06 Splits: 0)
Lemmas       : 692776   (Deleted: 652437)
  Binary     : 12568    (Ratio:   1.81%)
  Ternary    : 3535     (Ratio:   0.51%)
  Conflict   : 692776   (Average Length:  345.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 692776   (Average: 13.67 Max: 1434 Sum: 9467995)
  Executed   : 692637   (Average: 13.66 Max: 1434 Sum: 9461363 Ratio:  99.93%)
  Bounded    : 139      (Average: 47.71 Max: 122 Sum:   6632 Ratio:   0.07%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 941779   (Eliminated:    0 Frozen: 290794)
Constraints  : 6924768  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

Iteration 90
Queue:		 [(5,25,7,True), (6,30,7,True), (7,35,6,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,3,True), (16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,False), (22,110,2,False), (23,115,2,False), (24,120,2,False)]
Grounded Until:	 120
Blocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 91
Time         : 649.204s (Solving: 611.42s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 649.264s

Choices      : 10728869 (Domain: 10532325)
Conflicts    : 700125   (Analyzed: 700121)
Restarts     : 8596     (Average: 81.45 Last: 214)
Model-Level  : 348.0   
Problems     : 91       (Average Length: 90.41 Splits: 0)
Lemmas       : 700121   (Deleted: 659579)
  Binary     : 12577    (Ratio:   1.80%)
  Ternary    : 3539     (Ratio:   0.51%)
  Conflict   : 700121   (Average Length:  345.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 700121   (Average: 13.57 Max: 1434 Sum: 9497546)
  Executed   : 699982   (Average: 13.56 Max: 1434 Sum: 9490914 Ratio:  99.93%)
  Bounded    : 139      (Average: 47.71 Max: 122 Sum:   6632 Ratio:   0.07%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 941779   (Eliminated:    0 Frozen: 290794)
Constraints  : 6924768  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

Iteration 91
Queue:		 [(6,30,7,True), (7,35,6,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,3,True), (16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,False), (22,110,2,False), (23,115,2,False), (24,120,2,False)]
Grounded Until:	 120
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 92
Time         : 653.359s (Solving: 615.39s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 653.420s

Choices      : 10769102 (Domain: 10572558)
Conflicts    : 707790   (Analyzed: 707786)
Restarts     : 8696     (Average: 81.39 Last: 214)
Model-Level  : 348.0   
Problems     : 92       (Average Length: 90.75 Splits: 0)
Lemmas       : 707786   (Deleted: 666818)
  Binary     : 12591    (Ratio:   1.78%)
  Ternary    : 3548     (Ratio:   0.50%)
  Conflict   : 707786   (Average Length:  344.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 707786   (Average: 13.46 Max: 1434 Sum: 9528448)
  Executed   : 707647   (Average: 13.45 Max: 1434 Sum: 9521816 Ratio:  99.93%)
  Bounded    : 139      (Average: 47.71 Max: 122 Sum:   6632 Ratio:   0.07%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 941779   (Eliminated:    0 Frozen: 290794)
Constraints  : 6924768  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

Iteration 92
Queue:		 [(7,35,6,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,3,True), (16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,False), (22,110,2,False), (23,115,2,False), (24,120,2,False)]
Grounded Until:	 120
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 93
Time         : 657.129s (Solving: 618.97s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 657.192s

Choices      : 10810919 (Domain: 10614375)
Conflicts    : 715175   (Analyzed: 715171)
Restarts     : 8796     (Average: 81.31 Last: 214)
Model-Level  : 348.0   
Problems     : 93       (Average Length: 91.09 Splits: 0)
Lemmas       : 715171   (Deleted: 674245)
  Binary     : 12600    (Ratio:   1.76%)
  Ternary    : 3551     (Ratio:   0.50%)
  Conflict   : 715171   (Average Length:  343.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 715171   (Average: 13.37 Max: 1434 Sum: 9559648)
  Executed   : 715032   (Average: 13.36 Max: 1434 Sum: 9553016 Ratio:  99.93%)
  Bounded    : 139      (Average: 47.71 Max: 122 Sum:   6632 Ratio:   0.07%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 941779   (Eliminated:    0 Frozen: 290794)
Constraints  : 6924768  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

Iteration 93
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,3,True), (16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,False), (22,110,2,False), (23,115,2,False), (24,120,2,False)]
Grounded Until:	 120
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 94
Time         : 661.989s (Solving: 623.65s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 662.048s

Choices      : 10857049 (Domain: 10660047)
Conflicts    : 723453   (Analyzed: 723449)
Restarts     : 8896     (Average: 81.32 Last: 214)
Model-Level  : 348.0   
Problems     : 94       (Average Length: 91.41 Splits: 0)
Lemmas       : 723449   (Deleted: 681400)
  Binary     : 12642    (Ratio:   1.75%)
  Ternary    : 3576     (Ratio:   0.49%)
  Conflict   : 723449   (Average Length:  343.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 723449   (Average: 13.27 Max: 1434 Sum: 9596663)
  Executed   : 723310   (Average: 13.26 Max: 1434 Sum: 9590031 Ratio:  99.93%)
  Bounded    : 139      (Average: 47.71 Max: 122 Sum:   6632 Ratio:   0.07%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 941779   (Eliminated:    0 Frozen: 290794)
Constraints  : 6924768  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 95
Time         : 664.602s (Solving: 626.05s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 664.660s

Choices      : 10890658 (Domain: 10693656)
Conflicts    : 730304   (Analyzed: 730300)
Restarts     : 8996     (Average: 81.18 Last: 214)
Model-Level  : 348.0   
Problems     : 95       (Average Length: 91.74 Splits: 0)
Lemmas       : 730300   (Deleted: 689528)
  Binary     : 12645    (Ratio:   1.73%)
  Ternary    : 3577     (Ratio:   0.49%)
  Conflict   : 730300   (Average Length:  341.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 730300   (Average: 13.17 Max: 1434 Sum: 9616915)
  Executed   : 730161   (Average: 13.16 Max: 1434 Sum: 9610283 Ratio:  99.93%)
  Bounded    : 139      (Average: 47.71 Max: 122 Sum:   6632 Ratio:   0.07%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 941779   (Eliminated:    0 Frozen: 290794)
Constraints  : 6924768  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 96
Time         : 670.852s (Solving: 632.11s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 670.912s

Choices      : 10977013 (Domain: 10779947)
Conflicts    : 738446   (Analyzed: 738442)
Restarts     : 9096     (Average: 81.18 Last: 214)
Model-Level  : 348.0   
Problems     : 96       (Average Length: 92.05 Splits: 0)
Lemmas       : 738442   (Deleted: 696283)
  Binary     : 12693    (Ratio:   1.72%)
  Ternary    : 3590     (Ratio:   0.49%)
  Conflict   : 738442   (Average Length:  341.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 738442   (Average: 13.12 Max: 1434 Sum: 9690127)
  Executed   : 738303   (Average: 13.11 Max: 1434 Sum: 9683495 Ratio:  99.93%)
  Bounded    : 139      (Average: 47.71 Max: 122 Sum:   6632 Ratio:   0.07%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 941779   (Eliminated:    0 Frozen: 290794)
Constraints  : 6924768  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 97
Time         : 677.293s (Solving: 638.36s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 677.356s

Choices      : 11109416 (Domain: 10912207)
Conflicts    : 746568   (Analyzed: 746564)
Restarts     : 9196     (Average: 81.18 Last: 214)
Model-Level  : 348.0   
Problems     : 97       (Average Length: 92.36 Splits: 0)
Lemmas       : 746564   (Deleted: 703910)
  Binary     : 12808    (Ratio:   1.72%)
  Ternary    : 3673     (Ratio:   0.49%)
  Conflict   : 746564   (Average Length:  340.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 746564   (Average: 13.14 Max: 1434 Sum: 9806337)
  Executed   : 746424   (Average: 13.13 Max: 1434 Sum: 9799583 Ratio:  99.93%)
  Bounded    : 140      (Average: 48.24 Max: 122 Sum:   6754 Ratio:   0.07%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 941779   (Eliminated:    0 Frozen: 290794)
Constraints  : 6924768  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 6.38s
Memory:		 995MB (+0MB)
UNKNOWN
Iteration Time:	 6.45s

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

Models       : 0+
Calls        : 98
Time         : 685.502s (Solving: 646.37s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 685.568s

Choices      : 11281300 (Domain: 11083545)
Conflicts    : 754617   (Analyzed: 754613)
Restarts     : 9296     (Average: 81.18 Last: 214)
Model-Level  : 348.0   
Problems     : 98       (Average Length: 92.66 Splits: 0)
Lemmas       : 754613   (Deleted: 711606)
  Binary     : 12962    (Ratio:   1.72%)
  Ternary    : 3767     (Ratio:   0.50%)
  Conflict   : 754613   (Average Length:  340.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 754613   (Average: 13.20 Max: 1434 Sum: 9960462)
  Executed   : 754473   (Average: 13.19 Max: 1434 Sum: 9953708 Ratio:  99.93%)
  Bounded    : 140      (Average: 48.24 Max: 122 Sum:   6754 Ratio:   0.07%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 941779   (Eliminated:    0 Frozen: 290794)
Constraints  : 6924754  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 8.14s
Memory:		 995MB (+0MB)
UNKNOWN
Iteration Time:	 8.22s

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

Models       : 0+
Calls        : 99
Time         : 689.935s (Solving: 650.62s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 690.004s

Choices      : 11366188 (Domain: 11168388)
Conflicts    : 761892   (Analyzed: 761888)
Restarts     : 9396     (Average: 81.09 Last: 214)
Model-Level  : 348.0   
Problems     : 99       (Average Length: 92.96 Splits: 0)
Lemmas       : 761888   (Deleted: 719418)
  Binary     : 13008    (Ratio:   1.71%)
  Ternary    : 3787     (Ratio:   0.50%)
  Conflict   : 761888   (Average Length:  339.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 761888   (Average: 13.16 Max: 1434 Sum: 10028003)
  Executed   : 761748   (Average: 13.15 Max: 1434 Sum: 10021249 Ratio:  99.93%)
  Bounded    : 140      (Average: 48.24 Max: 122 Sum:   6754 Ratio:   0.07%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 941779   (Eliminated:    0 Frozen: 290794)
Constraints  : 6924754  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 100
Time         : 692.998s (Solving: 653.48s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 693.068s

Choices      : 11400149 (Domain: 11202349)
Conflicts    : 768857   (Analyzed: 768853)
Restarts     : 9496     (Average: 80.97 Last: 214)
Model-Level  : 348.0   
Problems     : 100      (Average Length: 93.25 Splits: 0)
Lemmas       : 768853   (Deleted: 726480)
  Binary     : 13009    (Ratio:   1.69%)
  Ternary    : 3787     (Ratio:   0.49%)
  Conflict   : 768853   (Average Length:  338.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 768853   (Average: 13.07 Max: 1434 Sum: 10052527)
  Executed   : 768713   (Average: 13.07 Max: 1434 Sum: 10045773 Ratio:  99.93%)
  Bounded    : 140      (Average: 48.24 Max: 122 Sum:   6754 Ratio:   0.07%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 941779   (Eliminated:    0 Frozen: 290794)
Constraints  : 6924754  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 3.00s
Memory:		 995MB (+0MB)
UNKNOWN
Iteration Time:	 3.07s

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

Models       : 0+
Calls        : 101
Time         : 696.929s (Solving: 657.20s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 697.000s

Choices      : 11438255 (Domain: 11240455)
Conflicts    : 776576   (Analyzed: 776572)
Restarts     : 9596     (Average: 80.93 Last: 214)
Model-Level  : 348.0   
Problems     : 101      (Average Length: 93.53 Splits: 0)
Lemmas       : 776572   (Deleted: 733400)
  Binary     : 13018    (Ratio:   1.68%)
  Ternary    : 3791     (Ratio:   0.49%)
  Conflict   : 776572   (Average Length:  337.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 776572   (Average: 12.98 Max: 1434 Sum: 10081909)
  Executed   : 776432   (Average: 12.97 Max: 1434 Sum: 10075155 Ratio:  99.93%)
  Bounded    : 140      (Average: 48.24 Max: 122 Sum:   6754 Ratio:   0.07%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 941779   (Eliminated:    0 Frozen: 290794)
Constraints  : 6924754  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 102
Time         : 706.289s (Solving: 666.34s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 706.364s

Choices      : 11532773 (Domain: 11333510)
Conflicts    : 785261   (Analyzed: 785257)
Restarts     : 9696     (Average: 80.99 Last: 214)
Model-Level  : 348.0   
Problems     : 102      (Average Length: 93.81 Splits: 0)
Lemmas       : 785257   (Deleted: 742795)
  Binary     : 13155    (Ratio:   1.68%)
  Ternary    : 3804     (Ratio:   0.48%)
  Conflict   : 785257   (Average Length:  340.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 785257   (Average: 12.93 Max: 1434 Sum: 10157223)
  Executed   : 785117   (Average: 12.93 Max: 1434 Sum: 10150469 Ratio:  99.93%)
  Bounded    : 140      (Average: 48.24 Max: 122 Sum:   6754 Ratio:   0.07%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 941779   (Eliminated:    0 Frozen: 290794)
Constraints  : 6924754  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 103
Time         : 711.098s (Solving: 670.95s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 711.176s

Choices      : 11584155 (Domain: 11383926)
Conflicts    : 792936   (Analyzed: 792932)
Restarts     : 9796     (Average: 80.94 Last: 214)
Model-Level  : 348.0   
Problems     : 103      (Average Length: 94.09 Splits: 0)
Lemmas       : 792932   (Deleted: 749112)
  Binary     : 13207    (Ratio:   1.67%)
  Ternary    : 3860     (Ratio:   0.49%)
  Conflict   : 792932   (Average Length:  340.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 792932   (Average: 12.86 Max: 1434 Sum: 10196718)
  Executed   : 792792   (Average: 12.85 Max: 1434 Sum: 10189964 Ratio:  99.93%)
  Bounded    : 140      (Average: 48.24 Max: 122 Sum:   6754 Ratio:   0.07%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 941779   (Eliminated:    0 Frozen: 290794)
Constraints  : 6924754  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 104
Time         : 719.564s (Solving: 679.22s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 719.644s

Choices      : 11694969 (Domain: 11492998)
Conflicts    : 801994   (Analyzed: 801990)
Restarts     : 9896     (Average: 81.04 Last: 214)
Model-Level  : 348.0   
Problems     : 104      (Average Length: 94.36 Splits: 0)
Lemmas       : 801990   (Deleted: 757799)
  Binary     : 13574    (Ratio:   1.69%)
  Ternary    : 4069     (Ratio:   0.51%)
  Conflict   : 801990   (Average Length:  339.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 801990   (Average: 12.83 Max: 1434 Sum: 10291160)
  Executed   : 801849   (Average: 12.82 Max: 1434 Sum: 10284284 Ratio:  99.93%)
  Bounded    : 141      (Average: 48.77 Max: 122 Sum:   6876 Ratio:   0.07%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 941779   (Eliminated:    0 Frozen: 290794)
Constraints  : 6924754  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 105
Time         : 724.070s (Solving: 683.50s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 724.152s

Choices      : 11752442 (Domain: 11550114)
Conflicts    : 809228   (Analyzed: 809224)
Restarts     : 9996     (Average: 80.95 Last: 214)
Model-Level  : 348.0   
Problems     : 105      (Average Length: 94.62 Splits: 0)
Lemmas       : 809224   (Deleted: 764510)
  Binary     : 13603    (Ratio:   1.68%)
  Ternary    : 4076     (Ratio:   0.50%)
  Conflict   : 809224   (Average Length:  339.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 809224   (Average: 12.77 Max: 1434 Sum: 10335880)
  Executed   : 809083   (Average: 12.76 Max: 1434 Sum: 10329004 Ratio:  99.93%)
  Bounded    : 141      (Average: 48.77 Max: 122 Sum:   6876 Ratio:   0.07%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 941779   (Eliminated:    0 Frozen: 290794)
Constraints  : 6924740  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 106
Time         : 730.172s (Solving: 689.39s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 730.248s

Choices      : 11835734 (Domain: 11632805)
Conflicts    : 817307   (Analyzed: 817303)
Restarts     : 10096    (Average: 80.95 Last: 214)
Model-Level  : 348.0   
Problems     : 106      (Average Length: 94.88 Splits: 0)
Lemmas       : 817303   (Deleted: 771600)
  Binary     : 13650    (Ratio:   1.67%)
  Ternary    : 4111     (Ratio:   0.50%)
  Conflict   : 817303   (Average Length:  339.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 817303   (Average: 12.73 Max: 1434 Sum: 10406063)
  Executed   : 817162   (Average: 12.72 Max: 1434 Sum: 10399187 Ratio:  99.93%)
  Bounded    : 141      (Average: 48.77 Max: 122 Sum:   6876 Ratio:   0.07%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 941779   (Eliminated:    0 Frozen: 290794)
Constraints  : 6924740  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 107
Time         : 733.997s (Solving: 693.01s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 734.072s

Choices      : 11894606 (Domain: 11691670)
Conflicts    : 824632   (Analyzed: 824628)
Restarts     : 10196    (Average: 80.88 Last: 214)
Model-Level  : 348.0   
Problems     : 107      (Average Length: 95.13 Splits: 0)
Lemmas       : 824628   (Deleted: 779321)
  Binary     : 13664    (Ratio:   1.66%)
  Ternary    : 4118     (Ratio:   0.50%)
  Conflict   : 824628   (Average Length:  338.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 824628   (Average: 12.67 Max: 1434 Sum: 10449456)
  Executed   : 824487   (Average: 12.66 Max: 1434 Sum: 10442580 Ratio:  99.93%)
  Bounded    : 141      (Average: 48.77 Max: 122 Sum:   6876 Ratio:   0.07%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 941779   (Eliminated:    0 Frozen: 290794)
Constraints  : 6924740  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 3.75s
Memory:		 995MB (+0MB)
UNKNOWN
Iteration Time:	 3.83s

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

Models       : 0+
Calls        : 108
Time         : 739.011s (Solving: 697.84s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 739.088s

Choices      : 11975748 (Domain: 11772713)
Conflicts    : 831853   (Analyzed: 831849)
Restarts     : 10296    (Average: 80.79 Last: 214)
Model-Level  : 348.0   
Problems     : 108      (Average Length: 95.38 Splits: 0)
Lemmas       : 831849   (Deleted: 786461)
  Binary     : 13700    (Ratio:   1.65%)
  Ternary    : 4125     (Ratio:   0.50%)
  Conflict   : 831849   (Average Length:  337.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 831849   (Average: 12.64 Max: 1434 Sum: 10512182)
  Executed   : 831708   (Average: 12.63 Max: 1434 Sum: 10505306 Ratio:  99.93%)
  Bounded    : 141      (Average: 48.77 Max: 122 Sum:   6876 Ratio:   0.07%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 941779   (Eliminated:    0 Frozen: 290794)
Constraints  : 6924740  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 109
Time         : 762.774s (Solving: 721.41s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 762.860s

Choices      : 12801990 (Domain: 12595996)
Conflicts    : 841881   (Analyzed: 841877)
Restarts     : 10396    (Average: 80.98 Last: 214)
Model-Level  : 348.0   
Problems     : 109      (Average Length: 95.62 Splits: 0)
Lemmas       : 841877   (Deleted: 794816)
  Binary     : 14377    (Ratio:   1.71%)
  Ternary    : 4422     (Ratio:   0.53%)
  Conflict   : 841877   (Average Length:  341.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 841877   (Average: 13.41 Max: 1434 Sum: 11292728)
  Executed   : 841735   (Average: 13.41 Max: 1434 Sum: 11285730 Ratio:  99.94%)
  Bounded    : 142      (Average: 49.28 Max: 122 Sum:   6998 Ratio:   0.06%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 941779   (Eliminated:    0 Frozen: 290794)
Constraints  : 6924740  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 23.71s
Memory:		 995MB (+0MB)
UNKNOWN
Iteration Time:	 23.77s

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

Models       : 0+
Calls        : 110
Time         : 766.515s (Solving: 724.95s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 766.604s

Choices      : 12838422 (Domain: 12632428)
Conflicts    : 849607   (Analyzed: 849603)
Restarts     : 10496    (Average: 80.95 Last: 214)
Model-Level  : 348.0   
Problems     : 110      (Average Length: 95.86 Splits: 0)
Lemmas       : 849603   (Deleted: 802088)
  Binary     : 14390    (Ratio:   1.69%)
  Ternary    : 4424     (Ratio:   0.52%)
  Conflict   : 849603   (Average Length:  340.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 849603   (Average: 13.32 Max: 1434 Sum: 11320164)
  Executed   : 849461   (Average: 13.32 Max: 1434 Sum: 11313166 Ratio:  99.94%)
  Bounded    : 142      (Average: 49.28 Max: 122 Sum:   6998 Ratio:   0.06%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 941779   (Eliminated:    0 Frozen: 290794)
Constraints  : 6924726  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 3.67s
Memory:		 995MB (+0MB)
UNKNOWN
Iteration Time:	 3.75s

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

Models       : 0+
Calls        : 111
Time         : 769.927s (Solving: 728.15s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 770.016s

Choices      : 12873765 (Domain: 12667771)
Conflicts    : 856808   (Analyzed: 856804)
Restarts     : 10596    (Average: 80.86 Last: 214)
Model-Level  : 348.0   
Problems     : 111      (Average Length: 96.10 Splits: 0)
Lemmas       : 856804   (Deleted: 809689)
  Binary     : 14390    (Ratio:   1.68%)
  Ternary    : 4426     (Ratio:   0.52%)
  Conflict   : 856804   (Average Length:  339.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 856804   (Average: 13.24 Max: 1434 Sum: 11346597)
  Executed   : 856662   (Average: 13.23 Max: 1434 Sum: 11339599 Ratio:  99.94%)
  Bounded    : 142      (Average: 49.28 Max: 122 Sum:   6998 Ratio:   0.06%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 941779   (Eliminated:    0 Frozen: 290794)
Constraints  : 6924726  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 3.33s
Memory:		 995MB (+0MB)
UNKNOWN
Iteration Time:	 3.42s

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

Models       : 0+
Calls        : 112
Time         : 775.649s (Solving: 733.68s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 775.740s

Choices      : 12923834 (Domain: 12717840)
Conflicts    : 864884   (Analyzed: 864880)
Restarts     : 10696    (Average: 80.86 Last: 214)
Model-Level  : 348.0   
Problems     : 112      (Average Length: 96.33 Splits: 0)
Lemmas       : 864880   (Deleted: 816841)
  Binary     : 14408    (Ratio:   1.67%)
  Ternary    : 4432     (Ratio:   0.51%)
  Conflict   : 864880   (Average Length:  339.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 864880   (Average: 13.17 Max: 1434 Sum: 11386170)
  Executed   : 864738   (Average: 13.16 Max: 1434 Sum: 11379172 Ratio:  99.94%)
  Bounded    : 142      (Average: 49.28 Max: 122 Sum:   6998 Ratio:   0.06%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 941779   (Eliminated:    0 Frozen: 290794)
Constraints  : 6924726  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 5.66s
Memory:		 995MB (+0MB)
UNKNOWN
Iteration Time:	 5.73s

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

Models       : 0+
Calls        : 113
Time         : 786.701s (Solving: 744.52s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 786.796s

Choices      : 13015165 (Domain: 12807859)
Conflicts    : 872957   (Analyzed: 872953)
Restarts     : 10796    (Average: 80.86 Last: 214)
Model-Level  : 348.0   
Problems     : 113      (Average Length: 96.56 Splits: 0)
Lemmas       : 872953   (Deleted: 824535)
  Binary     : 14633    (Ratio:   1.68%)
  Ternary    : 4485     (Ratio:   0.51%)
  Conflict   : 872953   (Average Length:  349.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 872953   (Average: 13.12 Max: 1434 Sum: 11455453)
  Executed   : 872811   (Average: 13.11 Max: 1434 Sum: 11448455 Ratio:  99.94%)
  Bounded    : 142      (Average: 49.28 Max: 122 Sum:   6998 Ratio:   0.06%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 941779   (Eliminated:    0 Frozen: 290794)
Constraints  : 6924726  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 10.98s
Memory:		 995MB (+0MB)
UNKNOWN
Iteration Time:	 11.06s

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

Models       : 0+
Calls        : 114
Time         : 794.197s (Solving: 751.82s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 794.296s

Choices      : 13096270 (Domain: 12888453)
Conflicts    : 881370   (Analyzed: 881366)
Restarts     : 10896    (Average: 80.89 Last: 214)
Model-Level  : 348.0   
Problems     : 114      (Average Length: 96.78 Splits: 0)
Lemmas       : 881366   (Deleted: 832220)
  Binary     : 14736    (Ratio:   1.67%)
  Ternary    : 4521     (Ratio:   0.51%)
  Conflict   : 881366   (Average Length:  351.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 881366   (Average: 13.07 Max: 1434 Sum: 11520827)
  Executed   : 881221   (Average: 13.06 Max: 1434 Sum: 11513463 Ratio:  99.94%)
  Bounded    : 145      (Average: 50.79 Max: 122 Sum:   7364 Ratio:   0.06%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 941779   (Eliminated:    0 Frozen: 290794)
Constraints  : 6924726  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 7.43s
Memory:		 995MB (+0MB)
UNKNOWN
Iteration Time:	 7.50s

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

Models       : 0+
Calls        : 115
Time         : 811.938s (Solving: 769.37s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 812.048s

Choices      : 13421258 (Domain: 13210557)
Conflicts    : 892206   (Analyzed: 892202)
Restarts     : 10996    (Average: 81.14 Last: 214)
Model-Level  : 348.0   
Problems     : 115      (Average Length: 97.00 Splits: 0)
Lemmas       : 892202   (Deleted: 840543)
  Binary     : 15759    (Ratio:   1.77%)
  Ternary    : 5045     (Ratio:   0.57%)
  Conflict   : 892202   (Average Length:  353.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 892202   (Average: 13.23 Max: 1434 Sum: 11802929)
  Executed   : 892057   (Average: 13.22 Max: 1434 Sum: 11795565 Ratio:  99.94%)
  Bounded    : 145      (Average: 50.79 Max: 122 Sum:   7364 Ratio:   0.06%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 941779   (Eliminated:    0 Frozen: 290794)
Constraints  : 6924732  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 17.68s
Memory:		 995MB (+0MB)
UNKNOWN
Iteration Time:	 17.75s

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

Models       : 0+
Calls        : 116
Time         : 823.093s (Solving: 780.30s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 823.208s

Choices      : 13565610 (Domain: 13354420)
Conflicts    : 900824   (Analyzed: 900820)
Restarts     : 11096    (Average: 81.18 Last: 214)
Model-Level  : 348.0   
Problems     : 116      (Average Length: 97.22 Splits: 0)
Lemmas       : 900820   (Deleted: 849816)
  Binary     : 16066    (Ratio:   1.78%)
  Ternary    : 5175     (Ratio:   0.57%)
  Conflict   : 900820   (Average Length:  352.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 900820   (Average: 13.24 Max: 1434 Sum: 11927684)
  Executed   : 900674   (Average: 13.23 Max: 1434 Sum: 11920204 Ratio:  99.94%)
  Bounded    : 146      (Average: 51.23 Max: 122 Sum:   7480 Ratio:   0.06%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 941779   (Eliminated:    0 Frozen: 290794)
Constraints  : 6924732  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 11.07s
Memory:		 995MB (+0MB)
UNKNOWN
Iteration Time:	 11.16s

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

Models       : 0+
Calls        : 117
Time         : 826.412s (Solving: 783.43s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 826.528s

Choices      : 13610115 (Domain: 13398924)
Conflicts    : 908084   (Analyzed: 908080)
Restarts     : 11196    (Average: 81.11 Last: 214)
Model-Level  : 348.0   
Problems     : 117      (Average Length: 97.43 Splits: 0)
Lemmas       : 908080   (Deleted: 856107)
  Binary     : 16074    (Ratio:   1.77%)
  Ternary    : 5177     (Ratio:   0.57%)
  Conflict   : 908080   (Average Length:  352.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 908080   (Average: 13.17 Max: 1434 Sum: 11956180)
  Executed   : 907934   (Average: 13.16 Max: 1434 Sum: 11948700 Ratio:  99.94%)
  Bounded    : 146      (Average: 51.23 Max: 122 Sum:   7480 Ratio:   0.06%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 941779   (Eliminated:    0 Frozen: 290794)
Constraints  : 6924732  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 3.26s
Memory:		 995MB (+0MB)
UNKNOWN
Iteration Time:	 3.32s

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

Models       : 0+
Calls        : 118
Time         : 832.898s (Solving: 789.73s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 833.016s

Choices      : 13712741 (Domain: 13501503)
Conflicts    : 915872   (Analyzed: 915868)
Restarts     : 11296    (Average: 81.08 Last: 214)
Model-Level  : 348.0   
Problems     : 118      (Average Length: 97.64 Splits: 0)
Lemmas       : 915868   (Deleted: 863780)
  Binary     : 16127    (Ratio:   1.76%)
  Ternary    : 5187     (Ratio:   0.57%)
  Conflict   : 915868   (Average Length:  351.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 915868   (Average: 13.15 Max: 1434 Sum: 12040246)
  Executed   : 915722   (Average: 13.14 Max: 1434 Sum: 12032766 Ratio:  99.94%)
  Bounded    : 146      (Average: 51.23 Max: 122 Sum:   7480 Ratio:   0.06%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 941779   (Eliminated:    0 Frozen: 290794)
Constraints  : 6924732  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 119
Time         : 837.686s (Solving: 794.33s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 837.804s

Choices      : 13753455 (Domain: 13542217)
Conflicts    : 923424   (Analyzed: 923420)
Restarts     : 11396    (Average: 81.03 Last: 214)
Model-Level  : 348.0   
Problems     : 119      (Average Length: 97.84 Splits: 0)
Lemmas       : 923420   (Deleted: 871380)
  Binary     : 16148    (Ratio:   1.75%)
  Ternary    : 5189     (Ratio:   0.56%)
  Conflict   : 923420   (Average Length:  352.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 923420   (Average: 13.07 Max: 1434 Sum: 12070983)
  Executed   : 923274   (Average: 13.06 Max: 1434 Sum: 12063503 Ratio:  99.94%)
  Bounded    : 146      (Average: 51.23 Max: 122 Sum:   7480 Ratio:   0.06%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 941779   (Eliminated:    0 Frozen: 290794)
Constraints  : 6924732  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 120
Time         : 841.351s (Solving: 797.79s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 841.472s

Choices      : 13792695 (Domain: 13581457)
Conflicts    : 930571   (Analyzed: 930567)
Restarts     : 11496    (Average: 80.95 Last: 214)
Model-Level  : 348.0   
Problems     : 120      (Average Length: 98.04 Splits: 0)
Lemmas       : 930567   (Deleted: 878283)
  Binary     : 16168    (Ratio:   1.74%)
  Ternary    : 5196     (Ratio:   0.56%)
  Conflict   : 930567   (Average Length:  352.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 930567   (Average: 13.00 Max: 1434 Sum: 12099736)
  Executed   : 930421   (Average: 12.99 Max: 1434 Sum: 12092256 Ratio:  99.94%)
  Bounded    : 146      (Average: 51.23 Max: 122 Sum:   7480 Ratio:   0.06%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 941779   (Eliminated:    0 Frozen: 290794)
Constraints  : 6924732  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 3.59s
Memory:		 995MB (+0MB)
UNKNOWN
Iteration Time:	 3.67s

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

Models       : 0+
Calls        : 121
Time         : 844.964s (Solving: 801.19s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 845.088s

Choices      : 13839916 (Domain: 13628678)
Conflicts    : 937723   (Analyzed: 937719)
Restarts     : 11596    (Average: 80.87 Last: 214)
Model-Level  : 348.0   
Problems     : 121      (Average Length: 98.24 Splits: 0)
Lemmas       : 937719   (Deleted: 885025)
  Binary     : 16182    (Ratio:   1.73%)
  Ternary    : 5198     (Ratio:   0.55%)
  Conflict   : 937719   (Average Length:  351.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 937719   (Average: 12.94 Max: 1434 Sum: 12136985)
  Executed   : 937573   (Average: 12.94 Max: 1434 Sum: 12129505 Ratio:  99.94%)
  Bounded    : 146      (Average: 51.23 Max: 122 Sum:   7480 Ratio:   0.06%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 941779   (Eliminated:    0 Frozen: 290794)
Constraints  : 6924732  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 3.53s
Memory:		 995MB (+0MB)
UNKNOWN
Iteration Time:	 3.62s

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

Models       : 0+
Calls        : 122
Time         : 849.203s (Solving: 805.24s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 849.324s

Choices      : 13889985 (Domain: 13678747)
Conflicts    : 945451   (Analyzed: 945447)
Restarts     : 11696    (Average: 80.84 Last: 214)
Model-Level  : 348.0   
Problems     : 122      (Average Length: 98.43 Splits: 0)
Lemmas       : 945447   (Deleted: 892549)
  Binary     : 16192    (Ratio:   1.71%)
  Ternary    : 5202     (Ratio:   0.55%)
  Conflict   : 945447   (Average Length:  351.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 945447   (Average: 12.88 Max: 1434 Sum: 12176012)
  Executed   : 945301   (Average: 12.87 Max: 1434 Sum: 12168532 Ratio:  99.94%)
  Bounded    : 146      (Average: 51.23 Max: 122 Sum:   7480 Ratio:   0.06%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 941779   (Eliminated:    0 Frozen: 290794)
Constraints  : 6924732  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 4.17s
Memory:		 995MB (+0MB)
UNKNOWN
Iteration Time:	 4.24s

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

Models       : 0+
Calls        : 123
Time         : 862.831s (Solving: 818.68s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 862.956s

Choices      : 14064631 (Domain: 13850494)
Conflicts    : 954420   (Analyzed: 954416)
Restarts     : 11796    (Average: 80.91 Last: 214)
Model-Level  : 348.0   
Problems     : 123      (Average Length: 98.63 Splits: 0)
Lemmas       : 954416   (Deleted: 902046)
  Binary     : 16469    (Ratio:   1.73%)
  Ternary    : 5250     (Ratio:   0.55%)
  Conflict   : 954416   (Average Length:  353.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 954416   (Average: 12.92 Max: 1434 Sum: 12328238)
  Executed   : 954270   (Average: 12.91 Max: 1434 Sum: 12320758 Ratio:  99.94%)
  Bounded    : 146      (Average: 51.23 Max: 122 Sum:   7480 Ratio:   0.06%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 941779   (Eliminated:    0 Frozen: 290794)
Constraints  : 6924732  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 13.57s
Memory:		 995MB (+0MB)
UNKNOWN
Iteration Time:	 13.64s

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

Models       : 0+
Calls        : 124
Time         : 866.460s (Solving: 822.12s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 866.588s

Choices      : 14108990 (Domain: 13894852)
Conflicts    : 961698   (Analyzed: 961694)
Restarts     : 11896    (Average: 80.84 Last: 214)
Model-Level  : 348.0   
Problems     : 124      (Average Length: 98.81 Splits: 0)
Lemmas       : 961694   (Deleted: 907979)
  Binary     : 16479    (Ratio:   1.71%)
  Ternary    : 5256     (Ratio:   0.55%)
  Conflict   : 961694   (Average Length:  353.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 961694   (Average: 12.85 Max: 1434 Sum: 12358451)
  Executed   : 961548   (Average: 12.84 Max: 1434 Sum: 12350971 Ratio:  99.94%)
  Bounded    : 146      (Average: 51.23 Max: 122 Sum:   7480 Ratio:   0.06%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 941779   (Eliminated:    0 Frozen: 290794)
Constraints  : 6924732  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 3.57s
Memory:		 995MB (+0MB)
UNKNOWN
Iteration Time:	 3.63s

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

Models       : 0+
Calls        : 125
Time         : 871.228s (Solving: 826.68s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 871.356s

Choices      : 14175927 (Domain: 13961278)
Conflicts    : 969147   (Analyzed: 969143)
Restarts     : 11996    (Average: 80.79 Last: 214)
Model-Level  : 348.0   
Problems     : 125      (Average Length: 99.00 Splits: 0)
Lemmas       : 969143   (Deleted: 915637)
  Binary     : 16516    (Ratio:   1.70%)
  Ternary    : 5264     (Ratio:   0.54%)
  Conflict   : 969143   (Average Length:  352.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 969143   (Average: 12.81 Max: 1434 Sum: 12411307)
  Executed   : 968997   (Average: 12.80 Max: 1434 Sum: 12403827 Ratio:  99.94%)
  Bounded    : 146      (Average: 51.23 Max: 122 Sum:   7480 Ratio:   0.06%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 941779   (Eliminated:    0 Frozen: 290794)
Constraints  : 6924732  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 126
Time         : 891.660s (Solving: 846.89s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 891.776s

Choices      : 14610596 (Domain: 14394720)
Conflicts    : 978824   (Analyzed: 978820)
Restarts     : 12096    (Average: 80.92 Last: 214)
Model-Level  : 348.0   
Problems     : 126      (Average Length: 99.18 Splits: 0)
Lemmas       : 978820   (Deleted: 925049)
  Binary     : 16848    (Ratio:   1.72%)
  Ternary    : 5312     (Ratio:   0.54%)
  Conflict   : 978820   (Average Length:  359.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 978820   (Average: 13.09 Max: 1434 Sum: 12809130)
  Executed   : 978674   (Average: 13.08 Max: 1434 Sum: 12801650 Ratio:  99.94%)
  Bounded    : 146      (Average: 51.23 Max: 122 Sum:   7480 Ratio:   0.06%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 941779   (Eliminated:    0 Frozen: 290794)
Constraints  : 6924732  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 20.34s
Memory:		 995MB (+0MB)
UNKNOWN
Iteration Time:	 20.43s

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

INTERRUPTED  : 1

Models       : 0+
Calls        : 127
Time         : 894.710s (Solving: 849.73s 1st Model: 0.01s Unsat: 8.68s)
CPU Time     : 894.808s

Choices      : 14648184 (Domain: 14432308)
Conflicts    : 985941   (Analyzed: 985937)
Restarts     : 12196    (Average: 80.84 Last: 214)
Model-Level  : 348.0   
Problems     : 127      (Average Length: 99.36 Splits: 0)
Lemmas       : 985937   (Deleted: 931891)
  Binary     : 16872    (Ratio:   1.71%)
  Ternary    : 5315     (Ratio:   0.54%)
  Conflict   : 985937   (Average Length:  358.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 985937   (Average: 13.02 Max: 1434 Sum: 12837202)
  Executed   : 985791   (Average: 13.01 Max: 1434 Sum: 12829722 Ratio:  99.94%)
  Bounded    : 146      (Average: 51.23 Max: 122 Sum:   7480 Ratio:   0.06%)

Rules        : 160590   (Original: 145095)
Atoms        : 77282   
Bodies       : 70054    (Original: 54558)
  Count      : 890      (Original: 2504)
Equivalences : 16810    (Atom=Atom: 87 Body=Body: 0 Other: 16723)
Tight        : Yes
Variables    : 941779   (Eliminated:    0 Frozen: 290794)
Constraints  : 6924732  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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


