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-2.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-2.pddl
Parsing...
Parsing: [0.040s CPU, 0.037s wall-clock]
Normalizing task... [0.000s CPU, 0.003s wall-clock]
Instantiating...
Generating Datalog program... [0.010s CPU, 0.009s wall-clock]
Normalizing Datalog program...
Normalizing Datalog program: [0.050s CPU, 0.049s wall-clock]
Preparing model... [0.020s CPU, 0.025s wall-clock]
Generated 115 rules.
Computing model... [0.330s CPU, 0.330s wall-clock]
2025 relevant atoms
2105 auxiliary atoms
4130 final queue length
7122 total queue pushes
Completing instantiation... [0.600s CPU, 0.598s wall-clock]
Instantiating: [1.010s CPU, 1.018s wall-clock]
Computing fact groups...
Finding invariants...
24 initial candidates
Finding invariants: [0.100s CPU, 0.097s wall-clock]
Checking invariant weight... [0.000s CPU, 0.001s wall-clock]
Instantiating groups... [0.010s CPU, 0.006s wall-clock]
Collecting mutex groups... [0.000s CPU, 0.000s wall-clock]
Choosing groups...
207 uncovered facts
Choosing groups: [0.000s CPU, 0.001s wall-clock]
Building translation key... [0.010s CPU, 0.008s wall-clock]
Computing fact groups: [0.130s CPU, 0.130s wall-clock]
Building STRIPS to SAS dictionary... [0.000s CPU, 0.002s wall-clock]
Building dictionary for full mutex groups... [0.000s CPU, 0.002s wall-clock]
Building mutex information...
Building mutex information: [0.000s CPU, 0.002s wall-clock]
Translating task...
Processing axioms...
Simplifying axioms... [0.000s CPU, 0.000s wall-clock]
Processing axioms: [0.040s CPU, 0.033s wall-clock]
Translating task: [0.660s CPU, 0.657s wall-clock]
2326 effect conditions simplified
0 implied preconditions added
Detecting unreachable propositions...
0 operators removed
0 axioms removed
3 propositions removed
Detecting unreachable propositions: [0.310s CPU, 0.308s wall-clock]
Reordering and filtering variables...
210 of 210 variables necessary.
11 of 14 mutex groups necessary.
1390 of 1390 operators necessary.
0 of 0 axiom rules necessary.
Reordering and filtering variables: [0.210s CPU, 0.207s wall-clock]
Translator variables: 210
Translator derived variables: 0
Translator facts: 441
Translator goal facts: 9
Translator mutex groups: 11
Translator total mutex groups size: 33
Translator operators: 1390
Translator axioms: 0
Translator task size: 13333
Translator peak memory: 43980 KB
Writing output... [0.260s CPU, 0.271s wall-clock]
Done! [2.640s CPU, 2.663s wall-clock]
planner.py version 0.0.1

Time:	 0.57s
Memory: 86MB

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

Models       : 0
Calls        : 1
Time         : 0.658s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
CPU Time     : 0.568s

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

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

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

Models       : 1+
Calls        : 2
Time         : 0.982s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
CPU Time     : 0.892s

Choices      : 152      (Domain: 73)
Conflicts    : 2        (Analyzed: 2)
Restarts     : 0       
Model-Level  : 147.0   
Problems     : 2        (Average Length: 4.50 Splits: 0)
Lemmas       : 2        (Deleted: 0)
  Binary     : 0        (Ratio:   0.00%)
  Ternary    : 0        (Ratio:   0.00%)
  Conflict   : 2        (Average Length:   23.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 2        (Average:  6.00 Max:  11 Sum:     12)
  Executed   : 2        (Average:  6.00 Max:  11 Sum:     12 Ratio: 100.00%)
  Bounded    : 0        (Average:  0.00 Max:   0 Sum:      0 Ratio:   0.00%)

Rules        : 38518   
Atoms        : 38518   
Bodies       : 1        (Original: 0)
Tight        : Yes
Variables    : 10322    (Eliminated:    0 Frozen: 10322)
Constraints  : 36431    (Binary:  95.0% Ternary:   3.5% Other:   1.5%)

Memory Peak  : 222MB
Max. Length  : 0 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 0.10s
Memory:		 160MB (+2MB)
SAT
Testing...
NOT SERIALIZABLE
Testing Time:	 0.58s
Memory:		 178MB (+18MB)
Solving...
[start: stats after solve call]

Models       : 0
Calls        : 3
Time         : 1.081s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
CPU Time     : 0.992s

Choices      : 161      (Domain: 78)
Conflicts    : 9        (Analyzed: 8)
Restarts     : 0       
Model-Level  : 147.0   
Problems     : 3        (Average Length: 5.33 Splits: 0)
Lemmas       : 8        (Deleted: 0)
  Binary     : 1        (Ratio:  12.50%)
  Ternary    : 2        (Ratio:  25.00%)
  Conflict   : 8        (Average Length:    8.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 8        (Average:  2.75 Max:  11 Sum:     22)
  Executed   : 7        (Average:  2.62 Max:  11 Sum:     21 Ratio:  95.45%)
  Bounded    : 1        (Average:  1.00 Max:   1 Sum:      1 Ratio:   4.55%)

Rules        : 55133    (Original: 53913)
Atoms        : 43853   
Bodies       : 10280    (Original: 9059)
  Count      : 232      (Original: 476)
Equivalences : 2929     (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight        : Yes
Variables    : 12735    (Eliminated: 1464 Frozen: 11271)
Constraints  : 50631    (Binary:  90.2% Ternary:   5.9% Other:   3.9%)

Memory Peak  : 222MB
Max. Length  : 0 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 0.02s
Memory:		 178MB (+0MB)
UNSAT
Iteration Time:	 0.93s

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

Models       : 0
Calls        : 4
Time         : 2.170s (Solving: 0.38s 1st Model: 0.00s Unsat: 0.38s)
CPU Time     : 2.080s

Choices      : 12799    (Domain: 10798)
Conflicts    : 1643     (Analyzed: 1641)
Restarts     : 10       (Average: 164.10 Last: 20)
Model-Level  : 147.0   
Problems     : 4        (Average Length: 7.00 Splits: 0)
Lemmas       : 1641     (Deleted: 0)
  Binary     : 185      (Ratio:  11.27%)
  Ternary    : 187      (Ratio:  11.40%)
  Conflict   : 1641     (Average Length:   27.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 1641     (Average:  7.73 Max:  79 Sum:  12687)
  Executed   : 1623     (Average:  7.62 Max:  79 Sum:  12504 Ratio:  98.56%)
  Bounded    : 18       (Average: 10.17 Max:  12 Sum:    183 Ratio:   1.44%)

Rules        : 55133    (Original: 53913)
Atoms        : 43853   
Bodies       : 10280    (Original: 9059)
  Count      : 232      (Original: 476)
Equivalences : 2929     (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight        : Yes
Variables    : 35311    (Eliminated: 1464 Frozen: 26317)
Constraints  : 223676   (Binary:  91.3% Ternary:   6.4% Other:   2.3%)

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

[endof: stats after solve call]
Solving Time:	 0.70s
Memory:		 189MB (+11MB)
UNSAT
Iteration Time:	 1.10s

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

Models       : 0
Calls        : 5
Time         : 6.807s (Solving: 4.20s 1st Model: 0.00s Unsat: 4.20s)
CPU Time     : 6.720s

Choices      : 95323    (Domain: 72132)
Conflicts    : 13704    (Analyzed: 13701)
Restarts     : 61       (Average: 224.61 Last: 168)
Model-Level  : 147.0   
Problems     : 5        (Average Length: 9.00 Splits: 0)
Lemmas       : 13701    (Deleted: 7320)
  Binary     : 884      (Ratio:   6.45%)
  Ternary    : 495      (Ratio:   3.61%)
  Conflict   : 13701    (Average Length:  196.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 13701    (Average:  6.83 Max: 380 Sum:  93639)
  Executed   : 13664    (Average:  6.80 Max: 380 Sum:  93177 Ratio:  99.51%)
  Bounded    : 37       (Average: 12.49 Max:  17 Sum:    462 Ratio:   0.49%)

Rules        : 55133    (Original: 53913)
Atoms        : 43853   
Bodies       : 10280    (Original: 9059)
  Count      : 232      (Original: 476)
Equivalences : 2929     (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight        : Yes
Variables    : 57887    (Eliminated: 1464 Frozen: 48893)
Constraints  : 381121   (Binary:  91.6% Ternary:   6.3% Other:   2.1%)

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

[endof: stats after solve call]
Solving Time:	 4.14s
Memory:		 209MB (+14MB)
UNSAT
Iteration Time:	 4.65s

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

Models       : 0+
Calls        : 6
Time         : 21.097s (Solving: 17.72s 1st Model: 0.00s Unsat: 4.20s)
CPU Time     : 21.012s

Choices      : 318692   (Domain: 274484)
Conflicts    : 41885    (Analyzed: 41882)
Restarts     : 161      (Average: 260.14 Last: 200)
Model-Level  : 147.0   
Problems     : 6        (Average Length: 11.17 Splits: 0)
Lemmas       : 41882    (Deleted: 27757)
  Binary     : 2114     (Ratio:   5.05%)
  Ternary    : 772      (Ratio:   1.84%)
  Conflict   : 41882    (Average Length:  420.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 41882    (Average:  7.36 Max: 431 Sum: 308320)
  Executed   : 41843    (Average:  7.35 Max: 431 Sum: 307814 Ratio:  99.84%)
  Bounded    : 39       (Average: 12.97 Max:  22 Sum:    506 Ratio:   0.16%)

Rules        : 55133    (Original: 53913)
Atoms        : 43853   
Bodies       : 10280    (Original: 9059)
  Count      : 232      (Original: 476)
Equivalences : 2929     (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight        : Yes
Variables    : 80463    (Eliminated: 1464 Frozen: 71469)
Constraints  : 538293   (Binary:  91.6% Ternary:   6.4% Other:   2.1%)

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

[endof: stats after solve call]
Solving Time:	 13.86s
Memory:		 227MB (+15MB)
UNKNOWN
Iteration Time:	 14.30s

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

Models       : 0+
Calls        : 7
Time         : 38.488s (Solving: 34.32s 1st Model: 0.00s Unsat: 4.20s)
CPU Time     : 38.412s

Choices      : 544925   (Domain: 486198)
Conflicts    : 70044    (Analyzed: 70041)
Restarts     : 261      (Average: 268.36 Last: 203)
Model-Level  : 147.0   
Problems     : 7        (Average Length: 13.43 Splits: 0)
Lemmas       : 70041    (Deleted: 53675)
  Binary     : 3314     (Ratio:   4.73%)
  Ternary    : 972      (Ratio:   1.39%)
  Conflict   : 70041    (Average Length:  595.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 70041    (Average:  7.41 Max: 431 Sum: 518924)
  Executed   : 70002    (Average:  7.40 Max: 431 Sum: 518418 Ratio:  99.90%)
  Bounded    : 39       (Average: 12.97 Max:  22 Sum:    506 Ratio:   0.10%)

Rules        : 55133    (Original: 53913)
Atoms        : 43853   
Bodies       : 10280    (Original: 9059)
  Count      : 232      (Original: 476)
Equivalences : 2929     (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight        : Yes
Variables    : 103039   (Eliminated: 1464 Frozen: 94045)
Constraints  : 711310   (Binary:  91.6% Ternary:   6.4% Other:   2.0%)

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

[endof: stats after solve call]
Solving Time:	 16.94s
Memory:		 242MB (+12MB)
UNKNOWN
Iteration Time:	 17.40s

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

Models       : 0+
Calls        : 8
Time         : 58.835s (Solving: 53.79s 1st Model: 0.00s Unsat: 4.20s)
CPU Time     : 58.768s

Choices      : 795479   (Domain: 727093)
Conflicts    : 98170    (Analyzed: 98167)
Restarts     : 361      (Average: 271.93 Last: 203)
Model-Level  : 147.0   
Problems     : 8        (Average Length: 15.75 Splits: 0)
Lemmas       : 98167    (Deleted: 80033)
  Binary     : 4642     (Ratio:   4.73%)
  Ternary    : 1200     (Ratio:   1.22%)
  Conflict   : 98167    (Average Length:  701.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 98167    (Average:  7.65 Max: 431 Sum: 751388)
  Executed   : 98127    (Average:  7.65 Max: 431 Sum: 750850 Ratio:  99.93%)
  Bounded    : 40       (Average: 13.45 Max:  32 Sum:    538 Ratio:   0.07%)

Rules        : 55133    (Original: 53913)
Atoms        : 43853   
Bodies       : 10280    (Original: 9059)
  Count      : 232      (Original: 476)
Equivalences : 2929     (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight        : Yes
Variables    : 125615   (Eliminated: 1464 Frozen: 116621)
Constraints  : 884355   (Binary:  91.6% Ternary:   6.4% Other:   2.0%)

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

[endof: stats after solve call]
Solving Time:	 19.83s
Memory:		 326MB (+82MB)
UNKNOWN
Iteration Time:	 20.36s

Iteration 8
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), (17,85,0,True)]
Grounded Until:	 30
Blocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 9
Time         : 73.429s (Solving: 68.35s 1st Model: 0.00s Unsat: 4.20s)
CPU Time     : 73.368s

Choices      : 908988   (Domain: 840602)
Conflicts    : 126350   (Analyzed: 126347)
Restarts     : 461      (Average: 274.07 Last: 203)
Model-Level  : 147.0   
Problems     : 9        (Average Length: 17.56 Splits: 0)
Lemmas       : 126347   (Deleted: 107054)
  Binary     : 5110     (Ratio:   4.04%)
  Ternary    : 1272     (Ratio:   1.01%)
  Conflict   : 126347   (Average Length:  680.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 126347   (Average:  6.80 Max: 431 Sum: 859482)
  Executed   : 126306   (Average:  6.80 Max: 431 Sum: 858912 Ratio:  99.93%)
  Bounded    : 41       (Average: 13.90 Max:  32 Sum:    570 Ratio:   0.07%)

Rules        : 55133    (Original: 53913)
Atoms        : 43853   
Bodies       : 10280    (Original: 9059)
  Count      : 232      (Original: 476)
Equivalences : 2929     (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight        : Yes
Variables    : 125615   (Eliminated: 1464 Frozen: 124151)
Constraints  : 884341   (Binary:  91.6% Ternary:   6.4% Other:   2.0%)

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

[endof: stats after solve call]
Solving Time:	 14.58s
Memory:		 326MB (+0MB)
UNKNOWN
Iteration Time:	 14.60s

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

Models       : 0+
Calls        : 10
Time         : 98.747s (Solving: 93.63s 1st Model: 0.00s Unsat: 4.20s)
CPU Time     : 98.696s

Choices      : 1039074  (Domain: 970650)
Conflicts    : 154469   (Analyzed: 154466)
Restarts     : 561      (Average: 275.34 Last: 204)
Model-Level  : 147.0   
Problems     : 10       (Average Length: 19.00 Splits: 0)
Lemmas       : 154466   (Deleted: 134626)
  Binary     : 5352     (Ratio:   3.46%)
  Ternary    : 1336     (Ratio:   0.86%)
  Conflict   : 154466   (Average Length:  791.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 154466   (Average:  6.32 Max: 431 Sum: 976481)
  Executed   : 154424   (Average:  6.32 Max: 431 Sum: 975879 Ratio:  99.94%)
  Bounded    : 42       (Average: 14.33 Max:  32 Sum:    602 Ratio:   0.06%)

Rules        : 55133    (Original: 53913)
Atoms        : 43853   
Bodies       : 10280    (Original: 9059)
  Count      : 232      (Original: 476)
Equivalences : 2929     (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight        : Yes
Variables    : 125615   (Eliminated: 1464 Frozen: 124151)
Constraints  : 884328   (Binary:  91.6% Ternary:   6.4% Other:   2.0%)

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

[endof: stats after solve call]
Solving Time:	 25.32s
Memory:		 326MB (+0MB)
UNKNOWN
Iteration Time:	 25.33s

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

Models       : 0+
Calls        : 11
Time         : 121.765s (Solving: 116.61s 1st Model: 0.00s Unsat: 4.20s)
CPU Time     : 121.724s

Choices      : 1259852  (Domain: 1190405)
Conflicts    : 182648   (Analyzed: 182645)
Restarts     : 661      (Average: 276.32 Last: 204)
Model-Level  : 147.0   
Problems     : 11       (Average Length: 20.18 Splits: 0)
Lemmas       : 182645   (Deleted: 161750)
  Binary     : 5826     (Ratio:   3.19%)
  Ternary    : 1427     (Ratio:   0.78%)
  Conflict   : 182645   (Average Length:  840.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 182645   (Average:  6.46 Max: 431 Sum: 1180686)
  Executed   : 182602   (Average:  6.46 Max: 431 Sum: 1180052 Ratio:  99.95%)
  Bounded    : 43       (Average: 14.74 Max:  32 Sum:    634 Ratio:   0.05%)

Rules        : 55133    (Original: 53913)
Atoms        : 43853   
Bodies       : 10280    (Original: 9059)
  Count      : 232      (Original: 476)
Equivalences : 2929     (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight        : Yes
Variables    : 125615   (Eliminated: 1464 Frozen: 124151)
Constraints  : 884314   (Binary:  91.6% Ternary:   6.4% Other:   2.0%)

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

[endof: stats after solve call]
Solving Time:	 23.01s
Memory:		 326MB (+0MB)
UNKNOWN
Iteration Time:	 23.03s

Iteration 11
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), (17,85,0,True)]
Grounded Until:	 30
Expected Memory: 410.0MB
Grounding...	 [('step', [31]), ('step', [32]), ('step', [33]), ('step', [34]), ('step', [35]), ('check', [35])]
Grounding Time:	 0.32s
Memory:		 327MB (+1MB)
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 12
Time         : 140.038s (Solving: 134.04s 1st Model: 0.00s Unsat: 4.20s)
CPU Time     : 140.004s

Choices      : 1469681  (Domain: 1393123)
Conflicts    : 210833   (Analyzed: 210830)
Restarts     : 761      (Average: 277.04 Last: 204)
Model-Level  : 147.0   
Problems     : 12       (Average Length: 21.58 Splits: 0)
Lemmas       : 210830   (Deleted: 188096)
  Binary     : 6845     (Ratio:   3.25%)
  Ternary    : 1557     (Ratio:   0.74%)
  Conflict   : 210830   (Average Length:  847.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 210830   (Average:  6.49 Max: 431 Sum: 1369029)
  Executed   : 210786   (Average:  6.49 Max: 431 Sum: 1368358 Ratio:  99.95%)
  Bounded    : 44       (Average: 15.25 Max:  37 Sum:    671 Ratio:   0.05%)

Rules        : 55133    (Original: 53913)
Atoms        : 43853   
Bodies       : 10280    (Original: 9059)
  Count      : 232      (Original: 476)
Equivalences : 2929     (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight        : Yes
Variables    : 148191   (Eliminated: 1464 Frozen: 139197)
Constraints  : 1057342  (Binary:  91.6% Ternary:   6.5% Other:   2.0%)

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

[endof: stats after solve call]
Solving Time:	 17.78s
Memory:		 341MB (+14MB)
UNKNOWN
Iteration Time:	 18.29s

Iteration 12
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), (17,85,0,True)]
Grounded Until:	 35
Expected Memory: 425.0MB
Grounding...	 [('step', [36]), ('step', [37]), ('step', [38]), ('step', [39]), ('step', [40]), ('check', [40])]
Grounding Time:	 0.42s
Memory:		 348MB (+7MB)
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 13
Time         : 158.318s (Solving: 151.36s 1st Model: 0.00s Unsat: 4.20s)
CPU Time     : 158.292s

Choices      : 1722991  (Domain: 1639840)
Conflicts    : 239049   (Analyzed: 239046)
Restarts     : 861      (Average: 277.64 Last: 204)
Model-Level  : 147.0   
Problems     : 13       (Average Length: 23.15 Splits: 0)
Lemmas       : 239046   (Deleted: 215086)
  Binary     : 7595     (Ratio:   3.18%)
  Ternary    : 1618     (Ratio:   0.68%)
  Conflict   : 239046   (Average Length:  840.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 239046   (Average:  6.70 Max: 431 Sum: 1600769)
  Executed   : 239002   (Average:  6.69 Max: 431 Sum: 1600098 Ratio:  99.96%)
  Bounded    : 44       (Average: 15.25 Max:  37 Sum:    671 Ratio:   0.04%)

Rules        : 55133    (Original: 53913)
Atoms        : 43853   
Bodies       : 10280    (Original: 9059)
  Count      : 232      (Original: 476)
Equivalences : 2929     (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight        : Yes
Variables    : 170767   (Eliminated: 1464 Frozen: 161773)
Constraints  : 1230373  (Binary:  91.6% Ternary:   6.5% Other:   2.0%)

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

[endof: stats after solve call]
Solving Time:	 17.68s
Memory:		 362MB (+14MB)
UNKNOWN
Iteration Time:	 18.29s

Iteration 13
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), (17,85,0,True)]
Grounded Until:	 40
Expected Memory: 446.0MB
Grounding...	 [('step', [41]), ('step', [42]), ('step', [43]), ('step', [44]), ('step', [45]), ('check', [45])]
Grounding Time:	 0.31s
Memory:		 366MB (+4MB)
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 14
Time         : 175.477s (Solving: 167.66s 1st Model: 0.00s Unsat: 4.20s)
CPU Time     : 175.456s

Choices      : 1976070  (Domain: 1888390)
Conflicts    : 267225   (Analyzed: 267222)
Restarts     : 961      (Average: 278.07 Last: 204)
Model-Level  : 147.0   
Problems     : 14       (Average Length: 24.86 Splits: 0)
Lemmas       : 267222   (Deleted: 241788)
  Binary     : 8210     (Ratio:   3.07%)
  Ternary    : 1715     (Ratio:   0.64%)
  Conflict   : 267222   (Average Length:  830.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 267222   (Average:  6.86 Max: 431 Sum: 1833630)
  Executed   : 267178   (Average:  6.86 Max: 431 Sum: 1832959 Ratio:  99.96%)
  Bounded    : 44       (Average: 15.25 Max:  37 Sum:    671 Ratio:   0.04%)

Rules        : 55133    (Original: 53913)
Atoms        : 43853   
Bodies       : 10280    (Original: 9059)
  Count      : 232      (Original: 476)
Equivalences : 2929     (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight        : Yes
Variables    : 193343   (Eliminated: 1464 Frozen: 184349)
Constraints  : 1403418  (Binary:  91.6% Ternary:   6.5% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 16.67s
Memory:		 389MB (+23MB)
UNKNOWN
Iteration Time:	 17.18s

Iteration 14
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), (17,85,0,True)]
Grounded Until:	 45
Expected Memory: 473.0MB
Grounding...	 [('step', [46]), ('step', [47]), ('step', [48]), ('step', [49]), ('step', [50]), ('check', [50])]
Grounding Time:	 0.32s
Memory:		 389MB (+0MB)
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 15
Time         : 193.509s (Solving: 184.81s 1st Model: 0.00s Unsat: 4.20s)
CPU Time     : 193.496s

Choices      : 2212664  (Domain: 2122911)
Conflicts    : 295414   (Analyzed: 295411)
Restarts     : 1061     (Average: 278.43 Last: 204)
Model-Level  : 147.0   
Problems     : 15       (Average Length: 26.67 Splits: 0)
Lemmas       : 295411   (Deleted: 268828)
  Binary     : 8624     (Ratio:   2.92%)
  Ternary    : 1761     (Ratio:   0.60%)
  Conflict   : 295411   (Average Length:  827.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 295411   (Average:  6.94 Max: 431 Sum: 2050016)
  Executed   : 295365   (Average:  6.94 Max: 431 Sum: 2049241 Ratio:  99.96%)
  Bounded    : 46       (Average: 16.85 Max:  52 Sum:    775 Ratio:   0.04%)

Rules        : 55133    (Original: 53913)
Atoms        : 43853   
Bodies       : 10280    (Original: 9059)
  Count      : 232      (Original: 476)
Equivalences : 2929     (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight        : Yes
Variables    : 215919   (Eliminated: 1464 Frozen: 206925)
Constraints  : 1576463  (Binary:  91.6% Ternary:   6.5% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 17.51s
Memory:		 403MB (+14MB)
UNKNOWN
Iteration Time:	 18.05s

Iteration 15
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), (17,85,0,True)]
Grounded Until:	 50
Expected Memory: 487.0MB
Grounding...	 [('step', [51]), ('step', [52]), ('step', [53]), ('step', [54]), ('step', [55]), ('check', [55])]
Grounding Time:	 0.32s
Memory:		 403MB (+0MB)
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 16
Time         : 212.232s (Solving: 202.65s 1st Model: 0.00s Unsat: 4.20s)
CPU Time     : 212.228s

Choices      : 2583279  (Domain: 2479786)
Conflicts    : 323565   (Analyzed: 323562)
Restarts     : 1161     (Average: 278.69 Last: 204)
Model-Level  : 147.0   
Problems     : 16       (Average Length: 28.56 Splits: 0)
Lemmas       : 323562   (Deleted: 295387)
  Binary     : 9565     (Ratio:   2.96%)
  Ternary    : 1916     (Ratio:   0.59%)
  Conflict   : 323562   (Average Length:  836.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 323562   (Average:  7.38 Max: 431 Sum: 2387890)
  Executed   : 323516   (Average:  7.38 Max: 431 Sum: 2387115 Ratio:  99.97%)
  Bounded    : 46       (Average: 16.85 Max:  52 Sum:    775 Ratio:   0.03%)

Rules        : 55133    (Original: 53913)
Atoms        : 43853   
Bodies       : 10280    (Original: 9059)
  Count      : 232      (Original: 476)
Equivalences : 2929     (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight        : Yes
Variables    : 238495   (Eliminated: 1464 Frozen: 229501)
Constraints  : 1749480  (Binary:  91.6% Ternary:   6.5% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 18.21s
Memory:		 417MB (+14MB)
UNKNOWN
Iteration Time:	 18.74s

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

Models       : 0+
Calls        : 17
Time         : 231.016s (Solving: 220.49s 1st Model: 0.00s Unsat: 4.20s)
CPU Time     : 231.020s

Choices      : 2835214  (Domain: 2730967)
Conflicts    : 351769   (Analyzed: 351766)
Restarts     : 1261     (Average: 278.96 Last: 204)
Model-Level  : 147.0   
Problems     : 17       (Average Length: 30.53 Splits: 0)
Lemmas       : 351766   (Deleted: 322486)
  Binary     : 9951     (Ratio:   2.83%)
  Ternary    : 1978     (Ratio:   0.56%)
  Conflict   : 351766   (Average Length:  825.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 351766   (Average:  7.44 Max: 431 Sum: 2618009)
  Executed   : 351719   (Average:  7.44 Max: 431 Sum: 2617172 Ratio:  99.97%)
  Bounded    : 47       (Average: 17.81 Max:  62 Sum:    837 Ratio:   0.03%)

Rules        : 55133    (Original: 53913)
Atoms        : 43853   
Bodies       : 10280    (Original: 9059)
  Count      : 232      (Original: 476)
Equivalences : 2929     (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight        : Yes
Variables    : 261071   (Eliminated: 1464 Frozen: 252077)
Constraints  : 1922525  (Binary:  91.6% Ternary:   6.5% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 18.21s
Memory:		 432MB (+15MB)
UNKNOWN
Iteration Time:	 18.80s

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

Models       : 0+
Calls        : 18
Time         : 251.557s (Solving: 240.07s 1st Model: 0.00s Unsat: 4.20s)
CPU Time     : 251.568s

Choices      : 3279607  (Domain: 3169584)
Conflicts    : 379925   (Analyzed: 379922)
Restarts     : 1361     (Average: 279.15 Last: 204)
Model-Level  : 147.0   
Problems     : 18       (Average Length: 32.56 Splits: 0)
Lemmas       : 379922   (Deleted: 348956)
  Binary     : 11063    (Ratio:   2.91%)
  Ternary    : 2142     (Ratio:   0.56%)
  Conflict   : 379922   (Average Length:  826.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 379922   (Average:  7.96 Max: 431 Sum: 3025976)
  Executed   : 379875   (Average:  7.96 Max: 431 Sum: 3025139 Ratio:  99.97%)
  Bounded    : 47       (Average: 17.81 Max:  62 Sum:    837 Ratio:   0.03%)

Rules        : 55133    (Original: 53913)
Atoms        : 43853   
Bodies       : 10280    (Original: 9059)
  Count      : 232      (Original: 476)
Equivalences : 2929     (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight        : Yes
Variables    : 283647   (Eliminated: 1464 Frozen: 274653)
Constraints  : 2095556  (Binary:  91.6% Ternary:   6.5% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 19.96s
Memory:		 465MB (+33MB)
UNKNOWN
Iteration Time:	 20.56s

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

Models       : 0+
Calls        : 19
Time         : 273.683s (Solving: 261.27s 1st Model: 0.00s Unsat: 4.20s)
CPU Time     : 273.704s

Choices      : 3620280  (Domain: 3509710)
Conflicts    : 408106   (Analyzed: 408103)
Restarts     : 1461     (Average: 279.33 Last: 204)
Model-Level  : 147.0   
Problems     : 19       (Average Length: 34.63 Splits: 0)
Lemmas       : 408103   (Deleted: 375917)
  Binary     : 11570    (Ratio:   2.84%)
  Ternary    : 2226     (Ratio:   0.55%)
  Conflict   : 408103   (Average Length:  829.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 408103   (Average:  8.18 Max: 431 Sum: 3337540)
  Executed   : 408056   (Average:  8.18 Max: 431 Sum: 3336703 Ratio:  99.97%)
  Bounded    : 47       (Average: 17.81 Max:  62 Sum:    837 Ratio:   0.03%)

Rules        : 55133    (Original: 53913)
Atoms        : 43853   
Bodies       : 10280    (Original: 9059)
  Count      : 232      (Original: 476)
Equivalences : 2929     (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight        : Yes
Variables    : 306223   (Eliminated: 1464 Frozen: 297229)
Constraints  : 2268601  (Binary:  91.6% Ternary:   6.5% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 21.57s
Memory:		 477MB (+12MB)
UNKNOWN
Iteration Time:	 22.14s

Iteration 19
Queue:		 [(15,75,0,True), (16,80,0,True), (17,85,0,True)]
Grounded Until:	 70
Expected Memory: 561.0MB
Grounding...	 [('step', [71]), ('step', [72]), ('step', [73]), ('step', [74]), ('step', [75]), ('check', [75])]
Grounding Time:	 0.34s
Memory:		 477MB (+0MB)
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 20
Time         : 294.476s (Solving: 281.11s 1st Model: 0.00s Unsat: 4.20s)
CPU Time     : 294.504s

Choices      : 4030873  (Domain: 3916810)
Conflicts    : 436313   (Analyzed: 436310)
Restarts     : 1561     (Average: 279.51 Last: 204)
Model-Level  : 147.0   
Problems     : 20       (Average Length: 36.75 Splits: 0)
Lemmas       : 436310   (Deleted: 401371)
  Binary     : 12272    (Ratio:   2.81%)
  Ternary    : 2334     (Ratio:   0.53%)
  Conflict   : 436310   (Average Length:  833.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 436310   (Average:  8.51 Max: 431 Sum: 3714399)
  Executed   : 436263   (Average:  8.51 Max: 431 Sum: 3713562 Ratio:  99.98%)
  Bounded    : 47       (Average: 17.81 Max:  62 Sum:    837 Ratio:   0.02%)

Rules        : 55133    (Original: 53913)
Atoms        : 43853   
Bodies       : 10280    (Original: 9059)
  Count      : 232      (Original: 476)
Equivalences : 2929     (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight        : Yes
Variables    : 328799   (Eliminated: 1464 Frozen: 319805)
Constraints  : 2441646  (Binary:  91.6% Ternary:   6.5% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 20.23s
Memory:		 492MB (+15MB)
UNKNOWN
Iteration Time:	 20.81s

Iteration 20
Queue:		 [(16,80,0,True), (17,85,0,True)]
Grounded Until:	 75
Expected Memory: 576.0MB
Grounding...	 [('step', [76]), ('step', [77]), ('step', [78]), ('step', [79]), ('step', [80]), ('check', [80])]
Grounding Time:	 0.48s
Memory:		 507MB (+15MB)
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 21
Time         : 316.121s (Solving: 301.64s 1st Model: 0.00s Unsat: 4.20s)
CPU Time     : 316.156s

Choices      : 4363980  (Domain: 4249676)
Conflicts    : 464504   (Analyzed: 464501)
Restarts     : 1661     (Average: 279.65 Last: 204)
Model-Level  : 147.0   
Problems     : 21       (Average Length: 38.90 Splits: 0)
Lemmas       : 464501   (Deleted: 429631)
  Binary     : 12709    (Ratio:   2.74%)
  Ternary    : 2409     (Ratio:   0.52%)
  Conflict   : 464501   (Average Length:  830.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 464501   (Average:  8.65 Max: 431 Sum: 4016299)
  Executed   : 464453   (Average:  8.64 Max: 431 Sum: 4015380 Ratio:  99.98%)
  Bounded    : 48       (Average: 19.15 Max:  82 Sum:    919 Ratio:   0.02%)

Rules        : 55133    (Original: 53913)
Atoms        : 43853   
Bodies       : 10280    (Original: 9059)
  Count      : 232      (Original: 476)
Equivalences : 2929     (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight        : Yes
Variables    : 351375   (Eliminated: 1464 Frozen: 342381)
Constraints  : 2614691  (Binary:  91.6% Ternary:   6.5% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 20.92s
Memory:		 521MB (+14MB)
UNKNOWN
Iteration Time:	 21.66s

Iteration 21
Queue:		 [(17,85,0,True)]
Grounded Until:	 80
Expected Memory: 605.0MB
Grounding...	 [('step', [81]), ('step', [82]), ('step', [83]), ('step', [84]), ('step', [85]), ('check', [85])]
Grounding Time:	 0.32s
Memory:		 521MB (+0MB)
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 22
Time         : 339.079s (Solving: 323.63s 1st Model: 0.00s Unsat: 4.20s)
CPU Time     : 339.124s

Choices      : 4698272  (Domain: 4583605)
Conflicts    : 492648   (Analyzed: 492645)
Restarts     : 1761     (Average: 279.75 Last: 204)
Model-Level  : 147.0   
Problems     : 22       (Average Length: 41.09 Splits: 0)
Lemmas       : 492645   (Deleted: 456973)
  Binary     : 13120    (Ratio:   2.66%)
  Ternary    : 2458     (Ratio:   0.50%)
  Conflict   : 492645   (Average Length:  839.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 492645   (Average:  8.75 Max: 431 Sum: 4309179)
  Executed   : 492597   (Average:  8.75 Max: 431 Sum: 4308260 Ratio:  99.98%)
  Bounded    : 48       (Average: 19.15 Max:  82 Sum:    919 Ratio:   0.02%)

Rules        : 55133    (Original: 53913)
Atoms        : 43853   
Bodies       : 10280    (Original: 9059)
  Count      : 232      (Original: 476)
Equivalences : 2929     (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight        : Yes
Variables    : 373951   (Eliminated: 1464 Frozen: 364957)
Constraints  : 2787722  (Binary:  91.6% Ternary:   6.5% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 22.39s
Memory:		 535MB (+14MB)
UNKNOWN
Iteration Time:	 22.97s

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

Models       : 0+
Calls        : 23
Time         : 350.517s (Solving: 334.98s 1st Model: 0.00s Unsat: 4.20s)
CPU Time     : 350.568s

Choices      : 4813255  (Domain: 4698588)
Conflicts    : 520838   (Analyzed: 520835)
Restarts     : 1861     (Average: 279.87 Last: 204)
Model-Level  : 147.0   
Problems     : 23       (Average Length: 43.09 Splits: 0)
Lemmas       : 520835   (Deleted: 484258)
  Binary     : 13398    (Ratio:   2.57%)
  Ternary    : 2506     (Ratio:   0.48%)
  Conflict   : 520835   (Average Length:  826.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 520835   (Average:  8.48 Max: 431 Sum: 4417398)
  Executed   : 520786   (Average:  8.48 Max: 431 Sum: 4416392 Ratio:  99.98%)
  Bounded    : 49       (Average: 20.53 Max:  87 Sum:   1006 Ratio:   0.02%)

Rules        : 55133    (Original: 53913)
Atoms        : 43853   
Bodies       : 10280    (Original: 9059)
  Count      : 232      (Original: 476)
Equivalences : 2929     (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight        : Yes
Variables    : 373951   (Eliminated: 1464 Frozen: 372487)
Constraints  : 2787722  (Binary:  91.6% Ternary:   6.5% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 11.41s
Memory:		 537MB (+2MB)
UNKNOWN
Iteration Time:	 11.45s

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

Models       : 0+
Calls        : 24
Time         : 376.151s (Solving: 360.52s 1st Model: 0.00s Unsat: 4.20s)
CPU Time     : 376.216s

Choices      : 4911678  (Domain: 4797011)
Conflicts    : 548996   (Analyzed: 548993)
Restarts     : 1961     (Average: 279.96 Last: 204)
Model-Level  : 147.0   
Problems     : 24       (Average Length: 44.92 Splits: 0)
Lemmas       : 548993   (Deleted: 511889)
  Binary     : 13480    (Ratio:   2.46%)
  Ternary    : 2531     (Ratio:   0.46%)
  Conflict   : 548993   (Average Length:  846.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 548993   (Average:  8.21 Max: 431 Sum: 4506436)
  Executed   : 548943   (Average:  8.21 Max: 431 Sum: 4505343 Ratio:  99.98%)
  Bounded    : 50       (Average: 21.86 Max:  87 Sum:   1093 Ratio:   0.02%)

Rules        : 55133    (Original: 53913)
Atoms        : 43853   
Bodies       : 10280    (Original: 9059)
  Count      : 232      (Original: 476)
Equivalences : 2929     (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight        : Yes
Variables    : 373951   (Eliminated: 1464 Frozen: 372487)
Constraints  : 2787708  (Binary:  91.6% Ternary:   6.5% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 25.61s
Memory:		 537MB (+0MB)
UNKNOWN
Iteration Time:	 25.65s

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

Models       : 0+
Calls        : 25
Time         : 395.354s (Solving: 379.63s 1st Model: 0.00s Unsat: 4.20s)
CPU Time     : 395.428s

Choices      : 5101516  (Domain: 4986849)
Conflicts    : 577235   (Analyzed: 577232)
Restarts     : 2061     (Average: 280.07 Last: 204)
Model-Level  : 147.0   
Problems     : 25       (Average Length: 46.60 Splits: 0)
Lemmas       : 577232   (Deleted: 539550)
  Binary     : 13703    (Ratio:   2.37%)
  Ternary    : 2558     (Ratio:   0.44%)
  Conflict   : 577232   (Average Length:  861.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 577232   (Average:  8.11 Max: 431 Sum: 4678791)
  Executed   : 577182   (Average:  8.10 Max: 431 Sum: 4677698 Ratio:  99.98%)
  Bounded    : 50       (Average: 21.86 Max:  87 Sum:   1093 Ratio:   0.02%)

Rules        : 55133    (Original: 53913)
Atoms        : 43853   
Bodies       : 10280    (Original: 9059)
  Count      : 232      (Original: 476)
Equivalences : 2929     (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight        : Yes
Variables    : 373951   (Eliminated: 1464 Frozen: 372487)
Constraints  : 2787694  (Binary:  91.6% Ternary:   6.5% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 19.18s
Memory:		 537MB (+0MB)
UNKNOWN
Iteration Time:	 19.22s

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

Models       : 0+
Calls        : 26
Time         : 413.248s (Solving: 397.41s 1st Model: 0.00s Unsat: 4.20s)
CPU Time     : 413.328s

Choices      : 5288141  (Domain: 5173473)
Conflicts    : 605398   (Analyzed: 605395)
Restarts     : 2161     (Average: 280.15 Last: 204)
Model-Level  : 147.0   
Problems     : 26       (Average Length: 48.15 Splits: 0)
Lemmas       : 605395   (Deleted: 566903)
  Binary     : 13934    (Ratio:   2.30%)
  Ternary    : 2601     (Ratio:   0.43%)
  Conflict   : 605395   (Average Length:  864.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 605395   (Average:  8.01 Max: 431 Sum: 4847208)
  Executed   : 605345   (Average:  8.00 Max: 431 Sum: 4846115 Ratio:  99.98%)
  Bounded    : 50       (Average: 21.86 Max:  87 Sum:   1093 Ratio:   0.02%)

Rules        : 55133    (Original: 53913)
Atoms        : 43853   
Bodies       : 10280    (Original: 9059)
  Count      : 232      (Original: 476)
Equivalences : 2929     (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight        : Yes
Variables    : 373951   (Eliminated: 1464 Frozen: 372487)
Constraints  : 2787694  (Binary:  91.6% Ternary:   6.5% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 17.85s
Memory:		 537MB (+0MB)
UNKNOWN
Iteration Time:	 17.90s

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

Models       : 0+
Calls        : 27
Time         : 434.403s (Solving: 418.46s 1st Model: 0.00s Unsat: 4.20s)
CPU Time     : 434.492s

Choices      : 5485373  (Domain: 5370691)
Conflicts    : 633582   (Analyzed: 633579)
Restarts     : 2261     (Average: 280.22 Last: 204)
Model-Level  : 147.0   
Problems     : 27       (Average Length: 49.59 Splits: 0)
Lemmas       : 633579   (Deleted: 594155)
  Binary     : 14225    (Ratio:   2.25%)
  Ternary    : 2658     (Ratio:   0.42%)
  Conflict   : 633579   (Average Length:  875.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 633579   (Average:  7.93 Max: 431 Sum: 5022002)
  Executed   : 633529   (Average:  7.92 Max: 431 Sum: 5020909 Ratio:  99.98%)
  Bounded    : 50       (Average: 21.86 Max:  87 Sum:   1093 Ratio:   0.02%)

Rules        : 55133    (Original: 53913)
Atoms        : 43853   
Bodies       : 10280    (Original: 9059)
  Count      : 232      (Original: 476)
Equivalences : 2929     (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight        : Yes
Variables    : 373951   (Eliminated: 1464 Frozen: 372487)
Constraints  : 2787694  (Binary:  91.6% Ternary:   6.5% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 21.12s
Memory:		 537MB (+0MB)
UNKNOWN
Iteration Time:	 21.17s

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

Models       : 0+
Calls        : 28
Time         : 451.839s (Solving: 435.81s 1st Model: 0.00s Unsat: 4.20s)
CPU Time     : 451.932s

Choices      : 5700364  (Domain: 5584170)
Conflicts    : 661765   (Analyzed: 661762)
Restarts     : 2361     (Average: 280.29 Last: 204)
Model-Level  : 147.0   
Problems     : 28       (Average Length: 50.93 Splits: 0)
Lemmas       : 661762   (Deleted: 621439)
  Binary     : 14657    (Ratio:   2.21%)
  Ternary    : 2708     (Ratio:   0.41%)
  Conflict   : 661762   (Average Length:  872.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 661762   (Average:  7.88 Max: 431 Sum: 5212706)
  Executed   : 661712   (Average:  7.88 Max: 431 Sum: 5211613 Ratio:  99.98%)
  Bounded    : 50       (Average: 21.86 Max:  87 Sum:   1093 Ratio:   0.02%)

Rules        : 55133    (Original: 53913)
Atoms        : 43853   
Bodies       : 10280    (Original: 9059)
  Count      : 232      (Original: 476)
Equivalences : 2929     (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight        : Yes
Variables    : 373951   (Eliminated: 1464 Frozen: 372487)
Constraints  : 2787694  (Binary:  91.6% Ternary:   6.5% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 17.41s
Memory:		 537MB (+0MB)
UNKNOWN
Iteration Time:	 17.45s

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

Models       : 0+
Calls        : 29
Time         : 468.754s (Solving: 452.63s 1st Model: 0.00s Unsat: 4.20s)
CPU Time     : 468.856s

Choices      : 5892645  (Domain: 5776369)
Conflicts    : 689962   (Analyzed: 689959)
Restarts     : 2461     (Average: 280.36 Last: 204)
Model-Level  : 147.0   
Problems     : 29       (Average Length: 52.17 Splits: 0)
Lemmas       : 689959   (Deleted: 647517)
  Binary     : 14908    (Ratio:   2.16%)
  Ternary    : 2759     (Ratio:   0.40%)
  Conflict   : 689959   (Average Length:  871.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 689959   (Average:  7.80 Max: 431 Sum: 5382814)
  Executed   : 689909   (Average:  7.80 Max: 431 Sum: 5381721 Ratio:  99.98%)
  Bounded    : 50       (Average: 21.86 Max:  87 Sum:   1093 Ratio:   0.02%)

Rules        : 55133    (Original: 53913)
Atoms        : 43853   
Bodies       : 10280    (Original: 9059)
  Count      : 232      (Original: 476)
Equivalences : 2929     (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight        : Yes
Variables    : 373951   (Eliminated: 1464 Frozen: 372487)
Constraints  : 2787694  (Binary:  91.6% Ternary:   6.5% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 16.89s
Memory:		 537MB (+0MB)
UNKNOWN
Iteration Time:	 16.93s

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

Models       : 0+
Calls        : 30
Time         : 489.515s (Solving: 473.27s 1st Model: 0.00s Unsat: 4.20s)
CPU Time     : 489.628s

Choices      : 6121052  (Domain: 6004694)
Conflicts    : 718096   (Analyzed: 718093)
Restarts     : 2561     (Average: 280.40 Last: 204)
Model-Level  : 147.0   
Problems     : 30       (Average Length: 53.33 Splits: 0)
Lemmas       : 718093   (Deleted: 676101)
  Binary     : 15186    (Ratio:   2.11%)
  Ternary    : 2806     (Ratio:   0.39%)
  Conflict   : 718093   (Average Length:  878.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 718093   (Average:  7.78 Max: 431 Sum: 5583729)
  Executed   : 718043   (Average:  7.77 Max: 431 Sum: 5582636 Ratio:  99.98%)
  Bounded    : 50       (Average: 21.86 Max:  87 Sum:   1093 Ratio:   0.02%)

Rules        : 55133    (Original: 53913)
Atoms        : 43853   
Bodies       : 10280    (Original: 9059)
  Count      : 232      (Original: 476)
Equivalences : 2929     (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight        : Yes
Variables    : 373951   (Eliminated: 1464 Frozen: 372487)
Constraints  : 2787694  (Binary:  91.6% Ternary:   6.5% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 20.72s
Memory:		 537MB (+0MB)
UNKNOWN
Iteration Time:	 20.77s

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

Models       : 0+
Calls        : 31
Time         : 508.521s (Solving: 492.15s 1st Model: 0.00s Unsat: 4.20s)
CPU Time     : 508.640s

Choices      : 6340515  (Domain: 6223979)
Conflicts    : 746262   (Analyzed: 746259)
Restarts     : 2661     (Average: 280.44 Last: 204)
Model-Level  : 147.0   
Problems     : 31       (Average Length: 54.42 Splits: 0)
Lemmas       : 746259   (Deleted: 703489)
  Binary     : 15397    (Ratio:   2.06%)
  Ternary    : 2842     (Ratio:   0.38%)
  Conflict   : 746259   (Average Length:  881.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 746259   (Average:  7.74 Max: 431 Sum: 5774391)
  Executed   : 746208   (Average:  7.74 Max: 431 Sum: 5773211 Ratio:  99.98%)
  Bounded    : 51       (Average: 23.14 Max:  87 Sum:   1180 Ratio:   0.02%)

Rules        : 55133    (Original: 53913)
Atoms        : 43853   
Bodies       : 10280    (Original: 9059)
  Count      : 232      (Original: 476)
Equivalences : 2929     (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight        : Yes
Variables    : 373951   (Eliminated: 1464 Frozen: 372487)
Constraints  : 2787694  (Binary:  91.6% Ternary:   6.5% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 18.96s
Memory:		 537MB (+0MB)
UNKNOWN
Iteration Time:	 19.02s

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

Models       : 0+
Calls        : 32
Time         : 527.510s (Solving: 511.05s 1st Model: 0.00s Unsat: 4.20s)
CPU Time     : 527.636s

Choices      : 6600559  (Domain: 6482924)
Conflicts    : 774478   (Analyzed: 774475)
Restarts     : 2761     (Average: 280.51 Last: 204)
Model-Level  : 147.0   
Problems     : 32       (Average Length: 55.44 Splits: 0)
Lemmas       : 774475   (Deleted: 730698)
  Binary     : 15878    (Ratio:   2.05%)
  Ternary    : 2908     (Ratio:   0.38%)
  Conflict   : 774475   (Average Length:  883.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 774475   (Average:  7.75 Max: 431 Sum: 6000830)
  Executed   : 774424   (Average:  7.75 Max: 431 Sum: 5999650 Ratio:  99.98%)
  Bounded    : 51       (Average: 23.14 Max:  87 Sum:   1180 Ratio:   0.02%)

Rules        : 55133    (Original: 53913)
Atoms        : 43853   
Bodies       : 10280    (Original: 9059)
  Count      : 232      (Original: 476)
Equivalences : 2929     (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight        : Yes
Variables    : 373951   (Eliminated: 1464 Frozen: 372487)
Constraints  : 2787687  (Binary:  91.6% Ternary:   6.5% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 18.96s
Memory:		 537MB (+0MB)
UNKNOWN
Iteration Time:	 19.00s

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

Models       : 0+
Calls        : 33
Time         : 547.765s (Solving: 531.21s 1st Model: 0.00s Unsat: 4.20s)
CPU Time     : 547.900s

Choices      : 6914199  (Domain: 6794643)
Conflicts    : 802630   (Analyzed: 802627)
Restarts     : 2861     (Average: 280.54 Last: 204)
Model-Level  : 147.0   
Problems     : 33       (Average Length: 56.39 Splits: 0)
Lemmas       : 802627   (Deleted: 757893)
  Binary     : 16327    (Ratio:   2.03%)
  Ternary    : 2968     (Ratio:   0.37%)
  Conflict   : 802627   (Average Length:  885.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 802627   (Average:  7.82 Max: 431 Sum: 6279139)
  Executed   : 802576   (Average:  7.82 Max: 431 Sum: 6277959 Ratio:  99.98%)
  Bounded    : 51       (Average: 23.14 Max:  87 Sum:   1180 Ratio:   0.02%)

Rules        : 55133    (Original: 53913)
Atoms        : 43853   
Bodies       : 10280    (Original: 9059)
  Count      : 232      (Original: 476)
Equivalences : 2929     (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight        : Yes
Variables    : 373951   (Eliminated: 1464 Frozen: 372487)
Constraints  : 2787687  (Binary:  91.6% Ternary:   6.5% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 20.22s
Memory:		 537MB (+0MB)
UNKNOWN
Iteration Time:	 20.27s

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

Models       : 0+
Calls        : 34
Time         : 568.390s (Solving: 551.74s 1st Model: 0.00s Unsat: 4.20s)
CPU Time     : 568.536s

Choices      : 7151395  (Domain: 7031757)
Conflicts    : 830822   (Analyzed: 830819)
Restarts     : 2961     (Average: 280.59 Last: 204)
Model-Level  : 147.0   
Problems     : 34       (Average Length: 57.29 Splits: 0)
Lemmas       : 830819   (Deleted: 785308)
  Binary     : 16566    (Ratio:   1.99%)
  Ternary    : 3004     (Ratio:   0.36%)
  Conflict   : 830819   (Average Length:  889.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 830819   (Average:  7.81 Max: 431 Sum: 6485634)
  Executed   : 830768   (Average:  7.80 Max: 431 Sum: 6484454 Ratio:  99.98%)
  Bounded    : 51       (Average: 23.14 Max:  87 Sum:   1180 Ratio:   0.02%)

Rules        : 55133    (Original: 53913)
Atoms        : 43853   
Bodies       : 10280    (Original: 9059)
  Count      : 232      (Original: 476)
Equivalences : 2929     (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight        : Yes
Variables    : 373951   (Eliminated: 1464 Frozen: 372487)
Constraints  : 2787687  (Binary:  91.6% Ternary:   6.5% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 20.60s
Memory:		 537MB (+0MB)
UNKNOWN
Iteration Time:	 20.64s

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

Models       : 0+
Calls        : 35
Time         : 589.267s (Solving: 572.51s 1st Model: 0.00s Unsat: 4.20s)
CPU Time     : 589.420s

Choices      : 7441227  (Domain: 7316328)
Conflicts    : 858998   (Analyzed: 858995)
Restarts     : 3061     (Average: 280.63 Last: 204)
Model-Level  : 147.0   
Problems     : 35       (Average Length: 58.14 Splits: 0)
Lemmas       : 858995   (Deleted: 812298)
  Binary     : 17110    (Ratio:   1.99%)
  Ternary    : 3091     (Ratio:   0.36%)
  Conflict   : 858995   (Average Length:  892.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 858995   (Average:  7.85 Max: 431 Sum: 6741586)
  Executed   : 858944   (Average:  7.85 Max: 431 Sum: 6740406 Ratio:  99.98%)
  Bounded    : 51       (Average: 23.14 Max:  87 Sum:   1180 Ratio:   0.02%)

Rules        : 55133    (Original: 53913)
Atoms        : 43853   
Bodies       : 10280    (Original: 9059)
  Count      : 232      (Original: 476)
Equivalences : 2929     (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight        : Yes
Variables    : 373951   (Eliminated: 1464 Frozen: 372487)
Constraints  : 2787687  (Binary:  91.6% Ternary:   6.5% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 20.85s
Memory:		 537MB (+0MB)
UNKNOWN
Iteration Time:	 20.89s

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

Models       : 0+
Calls        : 36
Time         : 611.139s (Solving: 594.28s 1st Model: 0.00s Unsat: 4.20s)
CPU Time     : 611.300s

Choices      : 7717670  (Domain: 7592616)
Conflicts    : 887211   (Analyzed: 887208)
Restarts     : 3161     (Average: 280.67 Last: 204)
Model-Level  : 147.0   
Problems     : 36       (Average Length: 58.94 Splits: 0)
Lemmas       : 887208   (Deleted: 839899)
  Binary     : 17380    (Ratio:   1.96%)
  Ternary    : 3137     (Ratio:   0.35%)
  Conflict   : 887208   (Average Length:  893.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 887208   (Average:  7.87 Max: 493 Sum: 6983010)
  Executed   : 887157   (Average:  7.87 Max: 493 Sum: 6981830 Ratio:  99.98%)
  Bounded    : 51       (Average: 23.14 Max:  87 Sum:   1180 Ratio:   0.02%)

Rules        : 55133    (Original: 53913)
Atoms        : 43853   
Bodies       : 10280    (Original: 9059)
  Count      : 232      (Original: 476)
Equivalences : 2929     (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight        : Yes
Variables    : 373951   (Eliminated: 1464 Frozen: 372487)
Constraints  : 2787687  (Binary:  91.6% Ternary:   6.5% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 21.84s
Memory:		 537MB (+0MB)
UNKNOWN
Iteration Time:	 21.88s

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

Models       : 0+
Calls        : 37
Time         : 632.985s (Solving: 615.15s 1st Model: 0.00s Unsat: 4.20s)
CPU Time     : 633.156s

Choices      : 7997616  (Domain: 7872364)
Conflicts    : 915441   (Analyzed: 915438)
Restarts     : 3261     (Average: 280.72 Last: 204)
Model-Level  : 147.0   
Problems     : 37       (Average Length: 59.84 Splits: 0)
Lemmas       : 915438   (Deleted: 867282)
  Binary     : 17707    (Ratio:   1.93%)
  Ternary    : 3182     (Ratio:   0.35%)
  Conflict   : 915438   (Average Length:  893.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 915438   (Average:  7.89 Max: 493 Sum: 7226121)
  Executed   : 915387   (Average:  7.89 Max: 493 Sum: 7224941 Ratio:  99.98%)
  Bounded    : 51       (Average: 23.14 Max:  87 Sum:   1180 Ratio:   0.02%)

Rules        : 55133    (Original: 53913)
Atoms        : 43853   
Bodies       : 10280    (Original: 9059)
  Count      : 232      (Original: 476)
Equivalences : 2929     (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight        : Yes
Variables    : 396527   (Eliminated: 1464 Frozen: 387533)
Constraints  : 2960732  (Binary:  91.6% Ternary:   6.5% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 21.26s
Memory:		 549MB (+12MB)
UNKNOWN
Iteration Time:	 21.86s

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

Models       : 0+
Calls        : 38
Time         : 654.789s (Solving: 635.95s 1st Model: 0.00s Unsat: 4.20s)
CPU Time     : 654.972s

Choices      : 8272236  (Domain: 8146669)
Conflicts    : 943641   (Analyzed: 943638)
Restarts     : 3361     (Average: 280.76 Last: 204)
Model-Level  : 147.0   
Problems     : 38       (Average Length: 60.82 Splits: 0)
Lemmas       : 943638   (Deleted: 894728)
  Binary     : 17930    (Ratio:   1.90%)
  Ternary    : 3210     (Ratio:   0.34%)
  Conflict   : 943638   (Average Length:  889.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 943638   (Average:  7.92 Max: 493 Sum: 7469400)
  Executed   : 943587   (Average:  7.91 Max: 493 Sum: 7468220 Ratio:  99.98%)
  Bounded    : 51       (Average: 23.14 Max:  87 Sum:   1180 Ratio:   0.02%)

Rules        : 55133    (Original: 53913)
Atoms        : 43853   
Bodies       : 10280    (Original: 9059)
  Count      : 232      (Original: 476)
Equivalences : 2929     (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight        : Yes
Variables    : 419103   (Eliminated: 1464 Frozen: 410109)
Constraints  : 3133777  (Binary:  91.6% Ternary:   6.5% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 21.20s
Memory:		 596MB (+47MB)
UNKNOWN
Iteration Time:	 21.82s

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

Models       : 0+
Calls        : 39
Time         : 678.370s (Solving: 658.52s 1st Model: 0.00s Unsat: 4.20s)
CPU Time     : 678.564s

Choices      : 8579392  (Domain: 8453731)
Conflicts    : 971840   (Analyzed: 971837)
Restarts     : 3461     (Average: 280.80 Last: 204)
Model-Level  : 147.0   
Problems     : 39       (Average Length: 61.87 Splits: 0)
Lemmas       : 971837   (Deleted: 922125)
  Binary     : 18257    (Ratio:   1.88%)
  Ternary    : 3262     (Ratio:   0.34%)
  Conflict   : 971837   (Average Length:  888.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 971837   (Average:  7.96 Max: 493 Sum: 7736535)
  Executed   : 971786   (Average:  7.96 Max: 493 Sum: 7735355 Ratio:  99.98%)
  Bounded    : 51       (Average: 23.14 Max:  87 Sum:   1180 Ratio:   0.02%)

Rules        : 55133    (Original: 53913)
Atoms        : 43853   
Bodies       : 10280    (Original: 9059)
  Count      : 232      (Original: 476)
Equivalences : 2929     (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight        : Yes
Variables    : 441679   (Eliminated: 1464 Frozen: 432685)
Constraints  : 3306822  (Binary:  91.6% Ternary:   6.5% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 22.97s
Memory:		 612MB (+16MB)
UNKNOWN
Iteration Time:	 23.60s

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

Models       : 0+
Calls        : 40
Time         : 700.801s (Solving: 679.93s 1st Model: 0.00s Unsat: 4.20s)
CPU Time     : 701.004s

Choices      : 8853119  (Domain: 8727423)
Conflicts    : 1000007  (Analyzed: 1000004)
Restarts     : 3561     (Average: 280.82 Last: 204)
Model-Level  : 147.0   
Problems     : 40       (Average Length: 63.00 Splits: 0)
Lemmas       : 1000004  (Deleted: 946111)
  Binary     : 18417    (Ratio:   1.84%)
  Ternary    : 3291     (Ratio:   0.33%)
  Conflict   : 1000004  (Average Length:  887.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 1000004  (Average:  7.97 Max: 493 Sum: 7973347)
  Executed   : 999953   (Average:  7.97 Max: 493 Sum: 7972167 Ratio:  99.99%)
  Bounded    : 51       (Average: 23.14 Max:  87 Sum:   1180 Ratio:   0.01%)

Rules        : 55133    (Original: 53913)
Atoms        : 43853   
Bodies       : 10280    (Original: 9059)
  Count      : 232      (Original: 476)
Equivalences : 2929     (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight        : Yes
Variables    : 464255   (Eliminated: 1464 Frozen: 455261)
Constraints  : 3479867  (Binary:  91.6% Ternary:   6.5% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 21.82s
Memory:		 616MB (+4MB)
UNKNOWN
Iteration Time:	 22.45s

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,2,False), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)]
Grounded Until:	 105
Blocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 41
Time         : 713.054s (Solving: 692.05s 1st Model: 0.00s Unsat: 4.20s)
CPU Time     : 713.264s

Choices      : 9003898  (Domain: 8878202)
Conflicts    : 1028184  (Analyzed: 1028181)
Restarts     : 3661     (Average: 280.85 Last: 204)
Model-Level  : 147.0   
Problems     : 41       (Average Length: 64.07 Splits: 0)
Lemmas       : 1028181  (Deleted: 977173)
  Binary     : 18547    (Ratio:   1.80%)
  Ternary    : 3325     (Ratio:   0.32%)
  Conflict   : 1028181  (Average Length:  876.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 1028181  (Average:  7.89 Max: 493 Sum: 8117468)
  Executed   : 1028130  (Average:  7.89 Max: 493 Sum: 8116288 Ratio:  99.99%)
  Bounded    : 51       (Average: 23.14 Max:  87 Sum:   1180 Ratio:   0.01%)

Rules        : 55133    (Original: 53913)
Atoms        : 43853   
Bodies       : 10280    (Original: 9059)
  Count      : 232      (Original: 476)
Equivalences : 2929     (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight        : Yes
Variables    : 464255   (Eliminated: 1464 Frozen: 462791)
Constraints  : 3479867  (Binary:  91.6% Ternary:   6.5% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 12.20s
Memory:		 616MB (+0MB)
UNKNOWN
Iteration Time:	 12.26s

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,2,False), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)]
Grounded Until:	 105
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 42
Time         : 738.564s (Solving: 717.46s 1st Model: 0.00s Unsat: 4.20s)
CPU Time     : 738.784s

Choices      : 9105606  (Domain: 8979910)
Conflicts    : 1056370  (Analyzed: 1056367)
Restarts     : 3761     (Average: 280.87 Last: 204)
Model-Level  : 147.0   
Problems     : 42       (Average Length: 65.10 Splits: 0)
Lemmas       : 1056367  (Deleted: 1004871)
  Binary     : 18597    (Ratio:   1.76%)
  Ternary    : 3363     (Ratio:   0.32%)
  Conflict   : 1056367  (Average Length:  876.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 1056367  (Average:  7.77 Max: 493 Sum: 8209915)
  Executed   : 1056316  (Average:  7.77 Max: 493 Sum: 8208735 Ratio:  99.99%)
  Bounded    : 51       (Average: 23.14 Max:  87 Sum:   1180 Ratio:   0.01%)

Rules        : 55133    (Original: 53913)
Atoms        : 43853   
Bodies       : 10280    (Original: 9059)
  Count      : 232      (Original: 476)
Equivalences : 2929     (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight        : Yes
Variables    : 464255   (Eliminated: 1464 Frozen: 462791)
Constraints  : 3479867  (Binary:  91.6% Ternary:   6.5% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 25.48s
Memory:		 616MB (+0MB)
UNKNOWN
Iteration Time:	 25.52s

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

Models       : 0+
Calls        : 43
Time         : 764.452s (Solving: 743.24s 1st Model: 0.00s Unsat: 4.20s)
CPU Time     : 764.680s

Choices      : 9282110  (Domain: 9156414)
Conflicts    : 1084555  (Analyzed: 1084552)
Restarts     : 3861     (Average: 280.90 Last: 204)
Model-Level  : 147.0   
Problems     : 43       (Average Length: 66.07 Splits: 0)
Lemmas       : 1084552  (Deleted: 1032580)
  Binary     : 18721    (Ratio:   1.73%)
  Ternary    : 3384     (Ratio:   0.31%)
  Conflict   : 1084552  (Average Length:  891.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 1084552  (Average:  7.72 Max: 493 Sum: 8370316)
  Executed   : 1084501  (Average:  7.72 Max: 493 Sum: 8369136 Ratio:  99.99%)
  Bounded    : 51       (Average: 23.14 Max:  87 Sum:   1180 Ratio:   0.01%)

Rules        : 55133    (Original: 53913)
Atoms        : 43853   
Bodies       : 10280    (Original: 9059)
  Count      : 232      (Original: 476)
Equivalences : 2929     (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight        : Yes
Variables    : 464255   (Eliminated: 1464 Frozen: 462791)
Constraints  : 3479867  (Binary:  91.6% Ternary:   6.5% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 25.86s
Memory:		 680MB (+64MB)
UNKNOWN
Iteration Time:	 25.90s

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

Models       : 0+
Calls        : 44
Time         : 784.115s (Solving: 762.79s 1st Model: 0.00s Unsat: 4.20s)
CPU Time     : 784.352s

Choices      : 9451213  (Domain: 9325517)
Conflicts    : 1112727  (Analyzed: 1112724)
Restarts     : 3961     (Average: 280.92 Last: 204)
Model-Level  : 147.0   
Problems     : 44       (Average Length: 67.00 Splits: 0)
Lemmas       : 1112724  (Deleted: 1060159)
  Binary     : 18869    (Ratio:   1.70%)
  Ternary    : 3425     (Ratio:   0.31%)
  Conflict   : 1112724  (Average Length:  894.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 1112724  (Average:  7.66 Max: 493 Sum: 8519634)
  Executed   : 1112673  (Average:  7.66 Max: 493 Sum: 8518454 Ratio:  99.99%)
  Bounded    : 51       (Average: 23.14 Max:  87 Sum:   1180 Ratio:   0.01%)

Rules        : 55133    (Original: 53913)
Atoms        : 43853   
Bodies       : 10280    (Original: 9059)
  Count      : 232      (Original: 476)
Equivalences : 2929     (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight        : Yes
Variables    : 464255   (Eliminated: 1464 Frozen: 462791)
Constraints  : 3479867  (Binary:  91.6% Ternary:   6.5% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 19.63s
Memory:		 680MB (+0MB)
UNKNOWN
Iteration Time:	 19.67s

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,2,False), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)]
Grounded Until:	 105
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 45
Time         : 803.797s (Solving: 782.37s 1st Model: 0.00s Unsat: 4.20s)
CPU Time     : 804.040s

Choices      : 9629811  (Domain: 9504115)
Conflicts    : 1140953  (Analyzed: 1140950)
Restarts     : 4061     (Average: 280.95 Last: 204)
Model-Level  : 147.0   
Problems     : 45       (Average Length: 67.89 Splits: 0)
Lemmas       : 1140950  (Deleted: 1087827)
  Binary     : 19015    (Ratio:   1.67%)
  Ternary    : 3450     (Ratio:   0.30%)
  Conflict   : 1140950  (Average Length:  897.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 1140950  (Average:  7.60 Max: 493 Sum: 8675794)
  Executed   : 1140899  (Average:  7.60 Max: 493 Sum: 8674614 Ratio:  99.99%)
  Bounded    : 51       (Average: 23.14 Max:  87 Sum:   1180 Ratio:   0.01%)

Rules        : 55133    (Original: 53913)
Atoms        : 43853   
Bodies       : 10280    (Original: 9059)
  Count      : 232      (Original: 476)
Equivalences : 2929     (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight        : Yes
Variables    : 464255   (Eliminated: 1464 Frozen: 462791)
Constraints  : 3479867  (Binary:  91.6% Ternary:   6.5% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 19.65s
Memory:		 680MB (+0MB)
UNKNOWN
Iteration Time:	 19.69s

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,2,False), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)]
Grounded Until:	 105
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 46
Time         : 825.313s (Solving: 803.76s 1st Model: 0.00s Unsat: 4.20s)
CPU Time     : 825.564s

Choices      : 9823417  (Domain: 9697580)
Conflicts    : 1169150  (Analyzed: 1169147)
Restarts     : 4161     (Average: 280.98 Last: 204)
Model-Level  : 147.0   
Problems     : 46       (Average Length: 68.74 Splits: 0)
Lemmas       : 1169147  (Deleted: 1115335)
  Binary     : 19295    (Ratio:   1.65%)
  Ternary    : 3485     (Ratio:   0.30%)
  Conflict   : 1169147  (Average Length:  904.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 1169147  (Average:  7.56 Max: 493 Sum: 8842595)
  Executed   : 1169096  (Average:  7.56 Max: 493 Sum: 8841415 Ratio:  99.99%)
  Bounded    : 51       (Average: 23.14 Max:  87 Sum:   1180 Ratio:   0.01%)

Rules        : 55133    (Original: 53913)
Atoms        : 43853   
Bodies       : 10280    (Original: 9059)
  Count      : 232      (Original: 476)
Equivalences : 2929     (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight        : Yes
Variables    : 464255   (Eliminated: 1464 Frozen: 462791)
Constraints  : 3479867  (Binary:  91.6% Ternary:   6.5% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 21.47s
Memory:		 680MB (+0MB)
UNKNOWN
Iteration Time:	 21.53s

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,2,False), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)]
Grounded Until:	 105
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 47
Time         : 844.567s (Solving: 822.91s 1st Model: 0.00s Unsat: 4.20s)
CPU Time     : 844.828s

Choices      : 10033085 (Domain: 9907237)
Conflicts    : 1197341  (Analyzed: 1197338)
Restarts     : 4261     (Average: 281.00 Last: 204)
Model-Level  : 147.0   
Problems     : 47       (Average Length: 69.55 Splits: 0)
Lemmas       : 1197338  (Deleted: 1142902)
  Binary     : 19440    (Ratio:   1.62%)
  Ternary    : 3518     (Ratio:   0.29%)
  Conflict   : 1197338  (Average Length:  903.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 1197338  (Average:  7.54 Max: 493 Sum: 9026213)
  Executed   : 1197287  (Average:  7.54 Max: 493 Sum: 9025033 Ratio:  99.99%)
  Bounded    : 51       (Average: 23.14 Max:  87 Sum:   1180 Ratio:   0.01%)

Rules        : 55133    (Original: 53913)
Atoms        : 43853   
Bodies       : 10280    (Original: 9059)
  Count      : 232      (Original: 476)
Equivalences : 2929     (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight        : Yes
Variables    : 464255   (Eliminated: 1464 Frozen: 462791)
Constraints  : 3479867  (Binary:  91.6% Ternary:   6.5% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 19.22s
Memory:		 680MB (+0MB)
UNKNOWN
Iteration Time:	 19.26s

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,2,False), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)]
Grounded Until:	 105
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 48
Time         : 863.330s (Solving: 841.57s 1st Model: 0.00s Unsat: 4.20s)
CPU Time     : 863.600s

Choices      : 10251284 (Domain: 10125432)
Conflicts    : 1225502  (Analyzed: 1225499)
Restarts     : 4361     (Average: 281.01 Last: 204)
Model-Level  : 147.0   
Problems     : 48       (Average Length: 70.33 Splits: 0)
Lemmas       : 1225499  (Deleted: 1170396)
  Binary     : 19701    (Ratio:   1.61%)
  Ternary    : 3549     (Ratio:   0.29%)
  Conflict   : 1225499  (Average Length:  904.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 1225499  (Average:  7.52 Max: 493 Sum: 9214105)
  Executed   : 1225448  (Average:  7.52 Max: 493 Sum: 9212925 Ratio:  99.99%)
  Bounded    : 51       (Average: 23.14 Max:  87 Sum:   1180 Ratio:   0.01%)

Rules        : 55133    (Original: 53913)
Atoms        : 43853   
Bodies       : 10280    (Original: 9059)
  Count      : 232      (Original: 476)
Equivalences : 2929     (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight        : Yes
Variables    : 464255   (Eliminated: 1464 Frozen: 462791)
Constraints  : 3479867  (Binary:  91.6% Ternary:   6.5% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 18.73s
Memory:		 680MB (+0MB)
UNKNOWN
Iteration Time:	 18.77s

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,2,False), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)]
Grounded Until:	 105
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 49
Time         : 881.523s (Solving: 859.66s 1st Model: 0.00s Unsat: 4.20s)
CPU Time     : 881.800s

Choices      : 10489316 (Domain: 10363047)
Conflicts    : 1253686  (Analyzed: 1253683)
Restarts     : 4461     (Average: 281.03 Last: 204)
Model-Level  : 147.0   
Problems     : 49       (Average Length: 71.08 Splits: 0)
Lemmas       : 1253683  (Deleted: 1197683)
  Binary     : 19958    (Ratio:   1.59%)
  Ternary    : 3584     (Ratio:   0.29%)
  Conflict   : 1253683  (Average Length:  903.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 1253683  (Average:  7.51 Max: 493 Sum: 9421101)
  Executed   : 1253631  (Average:  7.51 Max: 493 Sum: 9419814 Ratio:  99.99%)
  Bounded    : 52       (Average: 24.75 Max: 107 Sum:   1287 Ratio:   0.01%)

Rules        : 55133    (Original: 53913)
Atoms        : 43853   
Bodies       : 10280    (Original: 9059)
  Count      : 232      (Original: 476)
Equivalences : 2929     (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight        : Yes
Variables    : 464255   (Eliminated: 1464 Frozen: 462791)
Constraints  : 3479867  (Binary:  91.6% Ternary:   6.5% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 18.16s
Memory:		 680MB (+0MB)
UNKNOWN
Iteration Time:	 18.20s

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

INTERRUPTED  : 1

Models       : 0+
Calls        : 50
Time         : 900.347s (Solving: 878.37s 1st Model: 0.00s Unsat: 4.20s)
CPU Time     : 900.616s

Choices      : 10729648 (Domain: 10602630)
Conflicts    : 1281834  (Analyzed: 1281831)
Restarts     : 4561     (Average: 281.04 Last: 204)
Model-Level  : 147.0   
Problems     : 50       (Average Length: 71.80 Splits: 0)
Lemmas       : 1281831  (Deleted: 1225188)
  Binary     : 20176    (Ratio:   1.57%)
  Ternary    : 3624     (Ratio:   0.28%)
  Conflict   : 1281831  (Average Length:  903.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 1281831  (Average:  7.51 Max: 493 Sum: 9629023)
  Executed   : 1281779  (Average:  7.51 Max: 493 Sum: 9627736 Ratio:  99.99%)
  Bounded    : 52       (Average: 24.75 Max: 107 Sum:   1287 Ratio:   0.01%)

Rules        : 55133    (Original: 53913)
Atoms        : 43853   
Bodies       : 10280    (Original: 9059)
  Count      : 232      (Original: 476)
Equivalences : 2929     (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight        : Yes
Variables    : 464255   (Eliminated: 1464 Frozen: 462791)
Constraints  : 3479853  (Binary:  91.6% Ternary:   6.5% Other:   1.9%)

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


