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-17.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-17.pddl
Parsing...
Parsing: [0.040s CPU, 0.036s wall-clock]
Normalizing task... [0.000s CPU, 0.003s wall-clock]
Instantiating...
Generating Datalog program... [0.010s CPU, 0.010s wall-clock]
Normalizing Datalog program...
Normalizing Datalog program: [0.040s CPU, 0.045s wall-clock]
Preparing model... [0.030s CPU, 0.026s wall-clock]
Generated 115 rules.
Computing model... [0.530s 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.028s wall-clock]
Instantiating: [1.650s CPU, 1.652s wall-clock]
Computing fact groups...
Finding invariants...
24 initial candidates
Finding invariants: [0.140s CPU, 0.142s wall-clock]
Checking invariant weight... [0.000s CPU, 0.001s 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.000s CPU, 0.002s wall-clock]
Building translation key... [0.010s CPU, 0.013s wall-clock]
Computing fact groups: [0.190s CPU, 0.195s 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.057s wall-clock]
Translating task: [1.060s CPU, 1.067s 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.587s 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.378s 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.380s CPU, 0.411s wall-clock]
Done! [4.350s CPU, 4.383s 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.068s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
CPU Time     : 0.908s

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

Choices      : 171      (Domain: 108)
Conflicts    : 40       (Analyzed: 39)
Restarts     : 0       
Problems     : 2        (Average Length: 4.50 Splits: 0)
Lemmas       : 39       (Deleted: 0)
  Binary     : 11       (Ratio:  28.21%)
  Ternary    : 4        (Ratio:  10.26%)
  Conflict   : 39       (Average Length:    4.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 39       (Average:  4.41 Max:  28 Sum:    172)
  Executed   : 38       (Average:  4.38 Max:  28 Sum:    171 Ratio:  99.42%)
  Bounded    : 1        (Average:  1.00 Max:   1 Sum:      1 Ratio:   0.58%)

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

Choices      : 1028     (Domain: 926)
Conflicts    : 96       (Analyzed: 95)
Restarts     : 0       
Model-Level  : 254.0   
Problems     : 3        (Average Length: 7.00 Splits: 0)
Lemmas       : 95       (Deleted: 0)
  Binary     : 38       (Ratio:  40.00%)
  Ternary    : 6        (Ratio:   6.32%)
  Conflict   : 95       (Average Length:   59.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 95       (Average:  8.28 Max: 144 Sum:    787)
  Executed   : 94       (Average:  8.27 Max: 144 Sum:    786 Ratio:  99.87%)
  Bounded    : 1        (Average:  1.00 Max:   1 Sum:      1 Ratio:   0.13%)

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.04s
Memory:		 205MB (+10MB)
SAT
Testing...
NOT SERIALIZABLE
Testing Time:	 1.16s
Memory:		 241MB (+36MB)
Solving...
[start: stats after solve call]

Models       : 0
Calls        : 4
Time         : 3.305s (Solving: 0.95s 1st Model: 0.01s Unsat: 0.93s)
CPU Time     : 3.140s

Choices      : 30026    (Domain: 23080)
Conflicts    : 3147     (Analyzed: 3145)
Restarts     : 33       (Average: 95.30 Last: 56)
Model-Level  : 254.0   
Problems     : 4        (Average Length: 8.25 Splits: 0)
Lemmas       : 3145     (Deleted: 858)
  Binary     : 260      (Ratio:   8.27%)
  Ternary    : 82       (Ratio:   2.61%)
  Conflict   : 3145     (Average Length:  103.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 3145     (Average:  9.32 Max: 196 Sum:  29297)
  Executed   : 3134     (Average:  9.28 Max: 196 Sum:  29198 Ratio:  99.66%)
  Bounded    : 11       (Average:  9.00 Max:  12 Sum:     99 Ratio:   0.34%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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.02s
Memory:		 240MB (+-1MB)
UNSAT
Iteration Time:	 2.70s

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

Models       : 0+
Calls        : 5
Time         : 8.640s (Solving: 5.52s 1st Model: 0.01s Unsat: 0.93s)
CPU Time     : 8.480s

Choices      : 120633   (Domain: 94496)
Conflicts    : 11866    (Analyzed: 11864)
Restarts     : 133      (Average: 89.20 Last: 113)
Model-Level  : 254.0   
Problems     : 5        (Average Length: 10.00 Splits: 0)
Lemmas       : 11864    (Deleted: 8150)
  Binary     : 939      (Ratio:   7.91%)
  Ternary    : 300      (Ratio:   2.53%)
  Conflict   : 11864    (Average Length:  192.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 11864    (Average:  9.80 Max: 199 Sum: 116208)
  Executed   : 11841    (Average:  9.77 Max: 199 Sum: 115915 Ratio:  99.75%)
  Bounded    : 23       (Average: 12.74 Max:  17 Sum:    293 Ratio:   0.25%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 661845   (Binary:  91.3% Ternary:   6.9% Other:   1.7%)

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

[endof: stats after solve call]
Solving Time:	 4.60s
Memory:		 266MB (+25MB)
UNKNOWN
Iteration Time:	 5.35s

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

Models       : 0+
Calls        : 6
Time         : 15.324s (Solving: 11.29s 1st Model: 0.01s Unsat: 0.93s)
CPU Time     : 15.168s

Choices      : 228016   (Domain: 186850)
Conflicts    : 20689    (Analyzed: 20687)
Restarts     : 233      (Average: 88.79 Last: 113)
Model-Level  : 254.0   
Problems     : 6        (Average Length: 12.00 Splits: 0)
Lemmas       : 20687    (Deleted: 15856)
  Binary     : 1617     (Ratio:   7.82%)
  Ternary    : 415      (Ratio:   2.01%)
  Conflict   : 20687    (Average Length:  495.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 20687    (Average: 10.52 Max: 199 Sum: 217670)
  Executed   : 20664    (Average: 10.51 Max: 199 Sum: 217377 Ratio:  99.87%)
  Bounded    : 23       (Average: 12.74 Max:  17 Sum:    293 Ratio:   0.13%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 958119   (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.83s
Memory:		 293MB (+14MB)
UNKNOWN
Iteration Time:	 6.70s

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

Models       : 0+
Calls        : 7
Time         : 23.100s (Solving: 18.16s 1st Model: 0.01s Unsat: 0.93s)
CPU Time     : 22.948s

Choices      : 340659   (Domain: 289099)
Conflicts    : 29741    (Analyzed: 29739)
Restarts     : 333      (Average: 89.31 Last: 113)
Model-Level  : 254.0   
Problems     : 7        (Average Length: 14.14 Splits: 0)
Lemmas       : 29739    (Deleted: 24092)
  Binary     : 1976     (Ratio:   6.64%)
  Ternary    : 449      (Ratio:   1.51%)
  Conflict   : 29739    (Average Length:  822.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 29739    (Average: 10.82 Max: 248 Sum: 321843)
  Executed   : 29716    (Average: 10.81 Max: 248 Sum: 321550 Ratio:  99.91%)
  Bounded    : 23       (Average: 12.74 Max:  17 Sum:    293 Ratio:   0.09%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 1260099  (Binary:  91.3% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 8
Time         : 30.707s (Solving: 24.87s 1st Model: 0.01s Unsat: 0.93s)
CPU Time     : 30.556s

Choices      : 460469   (Domain: 402838)
Conflicts    : 37831    (Analyzed: 37829)
Restarts     : 433      (Average: 87.36 Last: 113)
Model-Level  : 254.0   
Problems     : 8        (Average Length: 16.38 Splits: 0)
Lemmas       : 37829    (Deleted: 30595)
  Binary     : 2189     (Ratio:   5.79%)
  Ternary    : 466      (Ratio:   1.23%)
  Conflict   : 37829    (Average Length: 1056.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 37829    (Average: 11.38 Max: 262 Sum: 430377)
  Executed   : 37806    (Average: 11.37 Max: 262 Sum: 430084 Ratio:  99.93%)
  Bounded    : 23       (Average: 12.74 Max:  17 Sum:    293 Ratio:   0.07%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 1562079  (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:	 6.77s
Memory:		 367MB (+34MB)
UNKNOWN
Iteration Time:	 7.62s

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

Models       : 0+
Calls        : 9
Time         : 36.604s (Solving: 30.70s 1st Model: 0.01s Unsat: 0.93s)
CPU Time     : 36.456s

Choices      : 545520   (Domain: 482044)
Conflicts    : 46602    (Analyzed: 46600)
Restarts     : 533      (Average: 87.43 Last: 113)
Model-Level  : 254.0   
Problems     : 9        (Average Length: 18.11 Splits: 0)
Lemmas       : 46600    (Deleted: 40009)
  Binary     : 2669     (Ratio:   5.73%)
  Ternary    : 563      (Ratio:   1.21%)
  Conflict   : 46600    (Average Length:  916.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 46600    (Average: 10.93 Max: 269 Sum: 509528)
  Executed   : 46563    (Average: 10.92 Max: 269 Sum: 508787 Ratio:  99.85%)
  Bounded    : 37       (Average: 20.03 Max:  32 Sum:    741 Ratio:   0.15%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 1562079  (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.88s
Memory:		 367MB (+0MB)
UNKNOWN
Iteration Time:	 5.90s

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.786s (Solving: 36.83s 1st Model: 0.01s Unsat: 0.93s)
CPU Time     : 42.640s

Choices      : 685916   (Domain: 614218)
Conflicts    : 55643    (Analyzed: 55641)
Restarts     : 633      (Average: 87.90 Last: 113)
Model-Level  : 254.0   
Problems     : 10       (Average Length: 19.50 Splits: 0)
Lemmas       : 55641    (Deleted: 47014)
  Binary     : 3310     (Ratio:   5.95%)
  Ternary    : 679      (Ratio:   1.22%)
  Conflict   : 55641    (Average Length:  796.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 55641    (Average: 11.59 Max: 282 Sum: 644675)
  Executed   : 55592    (Average: 11.57 Max: 282 Sum: 643550 Ratio:  99.83%)
  Bounded    : 49       (Average: 22.96 Max:  32 Sum:   1125 Ratio:   0.17%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 1539434  (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.17s
Memory:		 367MB (+0MB)
UNKNOWN
Iteration Time:	 6.19s

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.750s (Solving: 42.75s 1st Model: 0.01s Unsat: 0.93s)
CPU Time     : 48.604s

Choices      : 829159   (Domain: 750755)
Conflicts    : 64375    (Analyzed: 64373)
Restarts     : 733      (Average: 87.82 Last: 116)
Model-Level  : 254.0   
Problems     : 11       (Average Length: 20.64 Splits: 0)
Lemmas       : 64373    (Deleted: 54670)
  Binary     : 3548     (Ratio:   5.51%)
  Ternary    : 777      (Ratio:   1.21%)
  Conflict   : 64373    (Average Length:  715.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 64373    (Average: 12.15 Max: 307 Sum: 782285)
  Executed   : 64313    (Average: 12.13 Max: 307 Sum: 780838 Ratio:  99.82%)
  Bounded    : 60       (Average: 24.12 Max:  32 Sum:   1447 Ratio:   0.18%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 1517106  (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:	 5.95s
Memory:		 367MB (+0MB)
UNKNOWN
Iteration Time:	 5.97s

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

Models       : 0+
Calls        : 12
Time         : 54.222s (Solving: 48.16s 1st Model: 0.01s Unsat: 0.93s)
CPU Time     : 54.076s

Choices      : 990974   (Domain: 903422)
Conflicts    : 73229    (Analyzed: 73227)
Restarts     : 833      (Average: 87.91 Last: 150)
Model-Level  : 254.0   
Problems     : 12       (Average Length: 21.58 Splits: 0)
Lemmas       : 73227    (Deleted: 62428)
  Binary     : 3764     (Ratio:   5.14%)
  Ternary    : 847      (Ratio:   1.16%)
  Conflict   : 73227    (Average Length:  648.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 73227    (Average: 12.77 Max: 404 Sum: 934765)
  Executed   : 73160    (Average: 12.74 Max: 404 Sum: 933099 Ratio:  99.82%)
  Bounded    : 67       (Average: 24.87 Max:  32 Sum:   1666 Ratio:   0.18%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 1506186  (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:	 5.45s
Memory:		 367MB (+0MB)
UNKNOWN
Iteration Time:	 5.48s

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         : 61.201s (Solving: 54.18s 1st Model: 0.01s Unsat: 0.93s)
CPU Time     : 61.060s

Choices      : 1215033  (Domain: 1122075)
Conflicts    : 82083    (Analyzed: 82081)
Restarts     : 933      (Average: 87.98 Last: 150)
Model-Level  : 254.0   
Problems     : 13       (Average Length: 22.77 Splits: 0)
Lemmas       : 82081    (Deleted: 72810)
  Binary     : 4020     (Ratio:   4.90%)
  Ternary    : 860      (Ratio:   1.05%)
  Conflict   : 82081    (Average Length:  661.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 82081    (Average: 13.97 Max: 404 Sum: 1146403)
  Executed   : 82014    (Average: 13.95 Max: 404 Sum: 1144737 Ratio:  99.85%)
  Bounded    : 67       (Average: 24.87 Max:  32 Sum:   1666 Ratio:   0.15%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 1804964  (Binary:  91.3% Ternary:   6.9% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 14
Time         : 68.153s (Solving: 60.19s 1st Model: 0.01s Unsat: 0.93s)
CPU Time     : 68.016s

Choices      : 1422851  (Domain: 1322434)
Conflicts    : 90673    (Analyzed: 90671)
Restarts     : 1033     (Average: 87.77 Last: 150)
Model-Level  : 254.0   
Problems     : 14       (Average Length: 24.14 Splits: 0)
Lemmas       : 90671    (Deleted: 79068)
  Binary     : 4254     (Ratio:   4.69%)
  Ternary    : 864      (Ratio:   0.95%)
  Conflict   : 90671    (Average Length:  677.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 90671    (Average: 14.74 Max: 440 Sum: 1336710)
  Executed   : 90604    (Average: 14.72 Max: 440 Sum: 1335044 Ratio:  99.88%)
  Bounded    : 67       (Average: 24.87 Max:  32 Sum:   1666 Ratio:   0.12%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 2106944  (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:	 6.08s
Memory:		 406MB (+14MB)
UNKNOWN
Iteration Time:	 6.97s

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

Models       : 0+
Calls        : 15
Time         : 75.878s (Solving: 66.74s 1st Model: 0.01s Unsat: 0.93s)
CPU Time     : 75.744s

Choices      : 1592918  (Domain: 1489489)
Conflicts    : 99212    (Analyzed: 99210)
Restarts     : 1133     (Average: 87.56 Last: 150)
Model-Level  : 254.0   
Problems     : 15       (Average Length: 25.67 Splits: 0)
Lemmas       : 99210    (Deleted: 87296)
  Binary     : 4358     (Ratio:   4.39%)
  Ternary    : 869      (Ratio:   0.88%)
  Conflict   : 99210    (Average Length:  724.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 99210    (Average: 14.98 Max: 440 Sum: 1486626)
  Executed   : 99143    (Average: 14.97 Max: 440 Sum: 1484960 Ratio:  99.89%)
  Bounded    : 67       (Average: 24.87 Max:  32 Sum:   1666 Ratio:   0.11%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 2408924  (Binary:  91.3% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 6.64s
Memory:		 478MB (+48MB)
UNKNOWN
Iteration Time:	 7.74s

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

Models       : 0+
Calls        : 16
Time         : 83.761s (Solving: 73.63s 1st Model: 0.01s Unsat: 0.93s)
CPU Time     : 83.632s

Choices      : 1779320  (Domain: 1670641)
Conflicts    : 107288   (Analyzed: 107286)
Restarts     : 1233     (Average: 87.01 Last: 150)
Model-Level  : 254.0   
Problems     : 16       (Average Length: 27.31 Splits: 0)
Lemmas       : 107286   (Deleted: 95633)
  Binary     : 4449     (Ratio:   4.15%)
  Ternary    : 876      (Ratio:   0.82%)
  Conflict   : 107286   (Average Length:  756.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 107286   (Average: 15.37 Max: 482 Sum: 1649238)
  Executed   : 107219   (Average: 15.36 Max: 482 Sum: 1647572 Ratio:  99.90%)
  Bounded    : 67       (Average: 24.87 Max:  32 Sum:   1666 Ratio:   0.10%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 2710904  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 6.97s
Memory:		 488MB (+10MB)
UNKNOWN
Iteration Time:	 7.90s

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

Models       : 0+
Calls        : 17
Time         : 91.812s (Solving: 80.69s 1st Model: 0.01s Unsat: 0.93s)
CPU Time     : 91.684s

Choices      : 2037604  (Domain: 1924173)
Conflicts    : 115480   (Analyzed: 115478)
Restarts     : 1333     (Average: 86.63 Last: 150)
Model-Level  : 254.0   
Problems     : 17       (Average Length: 29.06 Splits: 0)
Lemmas       : 115478   (Deleted: 103546)
  Binary     : 4612     (Ratio:   3.99%)
  Ternary    : 877      (Ratio:   0.76%)
  Conflict   : 115478   (Average Length:  784.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 115478   (Average: 16.32 Max: 537 Sum: 1884467)
  Executed   : 115411   (Average: 16.30 Max: 537 Sum: 1882801 Ratio:  99.91%)
  Bounded    : 67       (Average: 24.87 Max:  32 Sum:   1666 Ratio:   0.09%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 3012884  (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:	 7.15s
Memory:		 512MB (+20MB)
UNKNOWN
Iteration Time:	 8.06s

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

Models       : 0+
Calls        : 18
Time         : 100.293s (Solving: 88.13s 1st Model: 0.01s Unsat: 0.93s)
CPU Time     : 100.168s

Choices      : 2275221  (Domain: 2158172)
Conflicts    : 123546   (Analyzed: 123544)
Restarts     : 1433     (Average: 86.21 Last: 150)
Model-Level  : 254.0   
Problems     : 18       (Average Length: 30.89 Splits: 0)
Lemmas       : 123544   (Deleted: 111469)
  Binary     : 4654     (Ratio:   3.77%)
  Ternary    : 878      (Ratio:   0.71%)
  Conflict   : 123544   (Average Length:  800.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 123544   (Average: 16.97 Max: 606 Sum: 2096708)
  Executed   : 123477   (Average: 16.96 Max: 606 Sum: 2095042 Ratio:  99.92%)
  Bounded    : 67       (Average: 24.87 Max:  32 Sum:   1666 Ratio:   0.08%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 3314864  (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:	 7.54s
Memory:		 589MB (+72MB)
UNKNOWN
Iteration Time:	 8.50s

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

Models       : 0+
Calls        : 19
Time         : 108.491s (Solving: 95.28s 1st Model: 0.01s Unsat: 0.93s)
CPU Time     : 108.368s

Choices      : 2547612  (Domain: 2426157)
Conflicts    : 131557   (Analyzed: 131555)
Restarts     : 1533     (Average: 85.82 Last: 150)
Model-Level  : 254.0   
Problems     : 19       (Average Length: 32.79 Splits: 0)
Lemmas       : 131555   (Deleted: 119386)
  Binary     : 4699     (Ratio:   3.57%)
  Ternary    : 879      (Ratio:   0.67%)
  Conflict   : 131555   (Average Length:  813.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 131555   (Average: 17.80 Max: 638 Sum: 2341876)
  Executed   : 131488   (Average: 17.79 Max: 638 Sum: 2340210 Ratio:  99.93%)
  Bounded    : 67       (Average: 24.87 Max:  32 Sum:   1666 Ratio:   0.07%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 3616844  (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.26s
Memory:		 594MB (+5MB)
UNKNOWN
Iteration Time:	 8.21s

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

Models       : 0+
Calls        : 20
Time         : 117.209s (Solving: 102.92s 1st Model: 0.01s Unsat: 0.93s)
CPU Time     : 117.092s

Choices      : 2844978  (Domain: 2719694)
Conflicts    : 139082   (Analyzed: 139080)
Restarts     : 1633     (Average: 85.17 Last: 150)
Model-Level  : 254.0   
Problems     : 20       (Average Length: 34.75 Splits: 0)
Lemmas       : 139080   (Deleted: 127229)
  Binary     : 4733     (Ratio:   3.40%)
  Ternary    : 880      (Ratio:   0.63%)
  Conflict   : 139080   (Average Length:  829.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 139080   (Average: 18.78 Max: 708 Sum: 2612039)
  Executed   : 139013   (Average: 18.77 Max: 708 Sum: 2610373 Ratio:  99.94%)
  Bounded    : 67       (Average: 24.87 Max:  32 Sum:   1666 Ratio:   0.06%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 3918824  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 7.75s
Memory:		 610MB (+16MB)
UNKNOWN
Iteration Time:	 8.73s

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

Models       : 0+
Calls        : 21
Time         : 126.455s (Solving: 111.07s 1st Model: 0.01s Unsat: 0.93s)
CPU Time     : 126.344s

Choices      : 3156384  (Domain: 3026249)
Conflicts    : 146866   (Analyzed: 146864)
Restarts     : 1733     (Average: 84.75 Last: 150)
Model-Level  : 254.0   
Problems     : 21       (Average Length: 36.76 Splits: 0)
Lemmas       : 146864   (Deleted: 134594)
  Binary     : 4775     (Ratio:   3.25%)
  Ternary    : 881      (Ratio:   0.60%)
  Conflict   : 146864   (Average Length:  841.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 146864   (Average: 19.71 Max: 746 Sum: 2894403)
  Executed   : 146797   (Average: 19.70 Max: 746 Sum: 2892737 Ratio:  99.94%)
  Bounded    : 67       (Average: 24.87 Max:  32 Sum:   1666 Ratio:   0.06%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 4220804  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 8.27s
Memory:		 642MB (+27MB)
UNKNOWN
Iteration Time:	 9.26s

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

Models       : 0+
Calls        : 22
Time         : 136.032s (Solving: 119.51s 1st Model: 0.01s Unsat: 0.93s)
CPU Time     : 135.924s

Choices      : 3453062  (Domain: 3319382)
Conflicts    : 155063   (Analyzed: 155061)
Restarts     : 1833     (Average: 84.59 Last: 150)
Model-Level  : 254.0   
Problems     : 22       (Average Length: 38.82 Splits: 0)
Lemmas       : 155061   (Deleted: 142241)
  Binary     : 4804     (Ratio:   3.10%)
  Ternary    : 882      (Ratio:   0.57%)
  Conflict   : 155061   (Average Length:  857.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 155061   (Average: 20.36 Max: 818 Sum: 3157695)
  Executed   : 154994   (Average: 20.35 Max: 818 Sum: 3156029 Ratio:  99.95%)
  Bounded    : 67       (Average: 24.87 Max:  32 Sum:   1666 Ratio:   0.05%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 4522784  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 8.56s
Memory:		 667MB (+25MB)
UNKNOWN
Iteration Time:	 9.59s

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         : 141.721s (Solving: 125.05s 1st Model: 0.01s Unsat: 0.93s)
CPU Time     : 141.616s

Choices      : 3517322  (Domain: 3372595)
Conflicts    : 163853   (Analyzed: 163851)
Restarts     : 1933     (Average: 84.77 Last: 150)
Model-Level  : 254.0   
Problems     : 23       (Average Length: 40.70 Splits: 0)
Lemmas       : 163851   (Deleted: 149929)
  Binary     : 5047     (Ratio:   3.08%)
  Ternary    : 960      (Ratio:   0.59%)
  Conflict   : 163851   (Average Length:  824.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 163851   (Average: 19.64 Max: 818 Sum: 3217490)
  Executed   : 163779   (Average: 19.63 Max: 818 Sum: 3215576 Ratio:  99.94%)
  Bounded    : 72       (Average: 26.58 Max:  82 Sum:   1914 Ratio:   0.06%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 4522784  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 5.64s
Memory:		 667MB (+0MB)
UNKNOWN
Iteration Time:	 5.70s

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         : 147.911s (Solving: 131.12s 1st Model: 0.01s Unsat: 0.93s)
CPU Time     : 147.808s

Choices      : 3616155  (Domain: 3462337)
Conflicts    : 172662   (Analyzed: 172660)
Restarts     : 2033     (Average: 84.93 Last: 150)
Model-Level  : 254.0   
Problems     : 24       (Average Length: 42.42 Splits: 0)
Lemmas       : 172660   (Deleted: 158068)
  Binary     : 5318     (Ratio:   3.08%)
  Ternary    : 1065     (Ratio:   0.62%)
  Conflict   : 172660   (Average Length:  794.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 172660   (Average: 19.17 Max: 818 Sum: 3309760)
  Executed   : 172585   (Average: 19.16 Max: 818 Sum: 3307600 Ratio:  99.93%)
  Bounded    : 75       (Average: 28.80 Max:  82 Sum:   2160 Ratio:   0.07%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 4522579  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 6.15s
Memory:		 667MB (+0MB)
UNKNOWN
Iteration Time:	 6.20s

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         : 156.601s (Solving: 139.68s 1st Model: 0.01s Unsat: 0.93s)
CPU Time     : 156.500s

Choices      : 3731283  (Domain: 3573611)
Conflicts    : 181844   (Analyzed: 181842)
Restarts     : 2133     (Average: 85.25 Last: 150)
Model-Level  : 254.0   
Problems     : 25       (Average Length: 44.00 Splits: 0)
Lemmas       : 181842   (Deleted: 165509)
  Binary     : 5874     (Ratio:   3.23%)
  Ternary    : 1244     (Ratio:   0.68%)
  Conflict   : 181842   (Average Length:  766.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 181842   (Average: 18.79 Max: 818 Sum: 3416660)
  Executed   : 181763   (Average: 18.78 Max: 818 Sum: 3414172 Ratio:  99.93%)
  Bounded    : 79       (Average: 31.49 Max:  82 Sum:   2488 Ratio:   0.07%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 4522538  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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         : 164.981s (Solving: 147.94s 1st Model: 0.01s Unsat: 0.93s)
CPU Time     : 164.884s

Choices      : 3853462  (Domain: 3689639)
Conflicts    : 190803   (Analyzed: 190801)
Restarts     : 2233     (Average: 85.45 Last: 150)
Model-Level  : 254.0   
Problems     : 26       (Average Length: 45.46 Splits: 0)
Lemmas       : 190801   (Deleted: 174103)
  Binary     : 6040     (Ratio:   3.17%)
  Ternary    : 1303     (Ratio:   0.68%)
  Conflict   : 190801   (Average Length:  746.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 190801   (Average: 18.48 Max: 818 Sum: 3526386)
  Executed   : 190721   (Average: 18.47 Max: 818 Sum: 3523816 Ratio:  99.93%)
  Bounded    : 80       (Average: 32.12 Max:  82 Sum:   2570 Ratio:   0.07%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 4519680  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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.129s (Solving: 156.97s 1st Model: 0.01s Unsat: 0.93s)
CPU Time     : 174.036s

Choices      : 4026215  (Domain: 3854302)
Conflicts    : 200213   (Analyzed: 200211)
Restarts     : 2333     (Average: 85.82 Last: 150)
Model-Level  : 254.0   
Problems     : 27       (Average Length: 46.81 Splits: 0)
Lemmas       : 200211   (Deleted: 182615)
  Binary     : 6189     (Ratio:   3.09%)
  Ternary    : 1328     (Ratio:   0.66%)
  Conflict   : 200211   (Average Length:  727.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 200211   (Average: 18.41 Max: 818 Sum: 3685588)
  Executed   : 200131   (Average: 18.40 Max: 818 Sum: 3683018 Ratio:  99.93%)
  Bounded    : 80       (Average: 32.12 Max:  82 Sum:   2570 Ratio:   0.07%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 4519667  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 9.11s
Memory:		 667MB (+0MB)
UNKNOWN
Iteration Time:	 9.15s

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         : 183.475s (Solving: 166.18s 1st Model: 0.01s Unsat: 0.93s)
CPU Time     : 183.388s

Choices      : 4188503  (Domain: 4013177)
Conflicts    : 209061   (Analyzed: 209059)
Restarts     : 2433     (Average: 85.93 Last: 150)
Model-Level  : 254.0   
Problems     : 28       (Average Length: 48.07 Splits: 0)
Lemmas       : 209059   (Deleted: 191460)
  Binary     : 6421     (Ratio:   3.07%)
  Ternary    : 1402     (Ratio:   0.67%)
  Conflict   : 209059   (Average Length:  711.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 209059   (Average: 18.34 Max: 818 Sum: 3834561)
  Executed   : 208977   (Average: 18.33 Max: 818 Sum: 3831827 Ratio:  99.93%)
  Bounded    : 82       (Average: 33.34 Max:  82 Sum:   2734 Ratio:   0.07%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 4519667  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 9.30s
Memory:		 667MB (+0MB)
UNKNOWN
Iteration Time:	 9.35s

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.149s (Solving: 176.69s 1st Model: 0.01s Unsat: 0.93s)
CPU Time     : 194.068s

Choices      : 4388056  (Domain: 4208740)
Conflicts    : 217872   (Analyzed: 217870)
Restarts     : 2533     (Average: 86.01 Last: 150)
Model-Level  : 254.0   
Problems     : 29       (Average Length: 49.24 Splits: 0)
Lemmas       : 217870   (Deleted: 199733)
  Binary     : 6576     (Ratio:   3.02%)
  Ternary    : 1444     (Ratio:   0.66%)
  Conflict   : 217870   (Average Length:  695.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 217870   (Average: 18.44 Max: 818 Sum: 4017279)
  Executed   : 217787   (Average: 18.43 Max: 818 Sum: 4014463 Ratio:  99.93%)
  Bounded    : 83       (Average: 33.93 Max:  82 Sum:   2816 Ratio:   0.07%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 4519639  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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         : 205.573s (Solving: 187.96s 1st Model: 0.01s Unsat: 0.93s)
CPU Time     : 205.496s

Choices      : 4605515  (Domain: 4423171)
Conflicts    : 226831   (Analyzed: 226829)
Restarts     : 2633     (Average: 86.15 Last: 150)
Model-Level  : 254.0   
Problems     : 30       (Average Length: 50.33 Splits: 0)
Lemmas       : 226829   (Deleted: 208173)
  Binary     : 6714     (Ratio:   2.96%)
  Ternary    : 1482     (Ratio:   0.65%)
  Conflict   : 226829   (Average Length:  679.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 226829   (Average: 18.60 Max: 818 Sum: 4219156)
  Executed   : 226744   (Average: 18.59 Max: 818 Sum: 4216176 Ratio:  99.93%)
  Bounded    : 85       (Average: 35.06 Max:  82 Sum:   2980 Ratio:   0.07%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 4519625  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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         : 215.341s (Solving: 197.60s 1st Model: 0.01s Unsat: 0.93s)
CPU Time     : 215.268s

Choices      : 4793152  (Domain: 4608690)
Conflicts    : 235198   (Analyzed: 235196)
Restarts     : 2733     (Average: 86.06 Last: 150)
Model-Level  : 254.0   
Problems     : 31       (Average Length: 51.35 Splits: 0)
Lemmas       : 235196   (Deleted: 214549)
  Binary     : 6844     (Ratio:   2.91%)
  Ternary    : 1505     (Ratio:   0.64%)
  Conflict   : 235196   (Average Length:  665.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 235196   (Average: 18.66 Max: 818 Sum: 4389743)
  Executed   : 235110   (Average: 18.65 Max: 818 Sum: 4386681 Ratio:  99.93%)
  Bounded    : 86       (Average: 35.60 Max:  82 Sum:   3062 Ratio:   0.07%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 4519599  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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         : 225.223s (Solving: 207.34s 1st Model: 0.01s Unsat: 0.93s)
CPU Time     : 225.152s

Choices      : 5007257  (Domain: 4821249)
Conflicts    : 243968   (Analyzed: 243966)
Restarts     : 2833     (Average: 86.12 Last: 175)
Model-Level  : 254.0   
Problems     : 32       (Average Length: 52.31 Splits: 0)
Lemmas       : 243966   (Deleted: 224708)
  Binary     : 6950     (Ratio:   2.85%)
  Ternary    : 1543     (Ratio:   0.63%)
  Conflict   : 243966   (Average Length:  652.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 243966   (Average: 18.81 Max: 818 Sum: 4589957)
  Executed   : 243877   (Average: 18.80 Max: 818 Sum: 4586649 Ratio:  99.93%)
  Bounded    : 89       (Average: 37.17 Max:  82 Sum:   3308 Ratio:   0.07%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 4519585  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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         : 234.701s (Solving: 216.68s 1st Model: 0.01s Unsat: 0.93s)
CPU Time     : 234.636s

Choices      : 5196384  (Domain: 5009297)
Conflicts    : 252514   (Analyzed: 252512)
Restarts     : 2933     (Average: 86.09 Last: 175)
Model-Level  : 254.0   
Problems     : 33       (Average Length: 53.21 Splits: 0)
Lemmas       : 252512   (Deleted: 230991)
  Binary     : 7049     (Ratio:   2.79%)
  Ternary    : 1572     (Ratio:   0.62%)
  Conflict   : 252512   (Average Length:  640.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 252512   (Average: 18.87 Max: 818 Sum: 4764711)
  Executed   : 252423   (Average: 18.86 Max: 818 Sum: 4761403 Ratio:  99.93%)
  Bounded    : 89       (Average: 37.17 Max:  82 Sum:   3308 Ratio:   0.07%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 4519544  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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         : 242.672s (Solving: 224.52s 1st Model: 0.01s Unsat: 0.93s)
CPU Time     : 242.612s

Choices      : 5291696  (Domain: 5104282)
Conflicts    : 260780   (Analyzed: 260778)
Restarts     : 3033     (Average: 85.98 Last: 175)
Model-Level  : 254.0   
Problems     : 34       (Average Length: 54.06 Splits: 0)
Lemmas       : 260778   (Deleted: 240360)
  Binary     : 7147     (Ratio:   2.74%)
  Ternary    : 1588     (Ratio:   0.61%)
  Conflict   : 260778   (Average Length:  631.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 260778   (Average: 18.59 Max: 818 Sum: 4846892)
  Executed   : 260689   (Average: 18.57 Max: 818 Sum: 4843584 Ratio:  99.93%)
  Bounded    : 89       (Average: 37.17 Max:  82 Sum:   3308 Ratio:   0.07%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 4519544  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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.873s (Solving: 236.60s 1st Model: 0.01s Unsat: 0.93s)
CPU Time     : 254.820s

Choices      : 5670287  (Domain: 5479652)
Conflicts    : 269812   (Analyzed: 269810)
Restarts     : 3133     (Average: 86.12 Last: 175)
Model-Level  : 254.0   
Problems     : 35       (Average Length: 54.86 Splits: 0)
Lemmas       : 269810   (Deleted: 249341)
  Binary     : 7352     (Ratio:   2.72%)
  Ternary    : 1664     (Ratio:   0.62%)
  Conflict   : 269810   (Average Length:  618.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 269810   (Average: 19.28 Max: 966 Sum: 5203281)
  Executed   : 269720   (Average: 19.27 Max: 966 Sum: 5199891 Ratio:  99.93%)
  Bounded    : 90       (Average: 37.67 Max:  82 Sum:   3390 Ratio:   0.07%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 4519544  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 12.17s
Memory:		 667MB (+0MB)
UNKNOWN
Iteration Time:	 12.21s

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         : 267.508s (Solving: 249.11s 1st Model: 0.01s Unsat: 0.93s)
CPU Time     : 267.464s

Choices      : 6035181  (Domain: 5841662)
Conflicts    : 278819   (Analyzed: 278817)
Restarts     : 3233     (Average: 86.24 Last: 175)
Model-Level  : 254.0   
Problems     : 36       (Average Length: 55.61 Splits: 0)
Lemmas       : 278817   (Deleted: 257774)
  Binary     : 7522     (Ratio:   2.70%)
  Ternary    : 1720     (Ratio:   0.62%)
  Conflict   : 278817   (Average Length:  607.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 278817   (Average: 19.89 Max: 1061 Sum: 5545315)
  Executed   : 278724   (Average: 19.88 Max: 1061 Sum: 5541679 Ratio:  99.93%)
  Bounded    : 93       (Average: 39.10 Max:  82 Sum:   3636 Ratio:   0.07%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 4519530  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 37
Time         : 278.843s (Solving: 259.27s 1st Model: 0.01s Unsat: 0.93s)
CPU Time     : 278.800s

Choices      : 6492250  (Domain: 6295822)
Conflicts    : 287420   (Analyzed: 287418)
Restarts     : 3333     (Average: 86.23 Last: 175)
Model-Level  : 254.0   
Problems     : 37       (Average Length: 56.46 Splits: 0)
Lemmas       : 287418   (Deleted: 266380)
  Binary     : 7719     (Ratio:   2.69%)
  Ternary    : 1739     (Ratio:   0.61%)
  Conflict   : 287418   (Average Length:  614.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 287418   (Average: 20.79 Max: 1061 Sum: 5974881)
  Executed   : 287325   (Average: 20.78 Max: 1061 Sum: 5971245 Ratio:  99.94%)
  Bounded    : 93       (Average: 39.10 Max:  82 Sum:   3636 Ratio:   0.06%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 4821468  (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:	 10.28s
Memory:		 689MB (+22MB)
UNKNOWN
Iteration Time:	 11.35s

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

Models       : 0+
Calls        : 38
Time         : 289.370s (Solving: 268.58s 1st Model: 0.01s Unsat: 0.93s)
CPU Time     : 289.328s

Choices      : 6925880  (Domain: 6725902)
Conflicts    : 296604   (Analyzed: 296602)
Restarts     : 3433     (Average: 86.40 Last: 175)
Model-Level  : 254.0   
Problems     : 38       (Average Length: 57.39 Splits: 0)
Lemmas       : 296602   (Deleted: 277010)
  Binary     : 7792     (Ratio:   2.63%)
  Ternary    : 1746     (Ratio:   0.59%)
  Conflict   : 296602   (Average Length:  624.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 296602   (Average: 21.49 Max: 1061 Sum: 6375261)
  Executed   : 296509   (Average: 21.48 Max: 1061 Sum: 6371625 Ratio:  99.94%)
  Bounded    : 93       (Average: 39.10 Max:  82 Sum:   3636 Ratio:   0.06%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 5123448  (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:	 9.45s
Memory:		 791MB (+102MB)
UNKNOWN
Iteration Time:	 10.54s

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

Models       : 0+
Calls        : 39
Time         : 299.836s (Solving: 277.50s 1st Model: 0.01s Unsat: 0.93s)
CPU Time     : 299.796s

Choices      : 7279684  (Domain: 7077152)
Conflicts    : 304419   (Analyzed: 304417)
Restarts     : 3533     (Average: 86.16 Last: 175)
Model-Level  : 254.0   
Problems     : 39       (Average Length: 58.41 Splits: 0)
Lemmas       : 304417   (Deleted: 283811)
  Binary     : 7827     (Ratio:   2.57%)
  Ternary    : 1750     (Ratio:   0.57%)
  Conflict   : 304417   (Average Length:  639.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 304417   (Average: 21.99 Max: 1061 Sum: 6693104)
  Executed   : 304324   (Average: 21.97 Max: 1061 Sum: 6689468 Ratio:  99.95%)
  Bounded    : 93       (Average: 39.10 Max:  82 Sum:   3636 Ratio:   0.05%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 5425428  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

Iteration 39
Queue:		 [(20,100,0,True)]
Grounded Until:	 95
Expected Memory: 899.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         : 310.789s (Solving: 287.23s 1st Model: 0.01s Unsat: 0.93s)
CPU Time     : 310.752s

Choices      : 7694764  (Domain: 7489396)
Conflicts    : 312176   (Analyzed: 312174)
Restarts     : 3633     (Average: 85.93 Last: 175)
Model-Level  : 254.0   
Problems     : 40       (Average Length: 59.50 Splits: 0)
Lemmas       : 312174   (Deleted: 291534)
  Binary     : 7854     (Ratio:   2.52%)
  Ternary    : 1754     (Ratio:   0.56%)
  Conflict   : 312174   (Average Length:  652.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 312174   (Average: 22.65 Max: 1061 Sum: 7071021)
  Executed   : 312081   (Average: 22.64 Max: 1061 Sum: 7067385 Ratio:  99.95%)
  Bounded    : 93       (Average: 39.10 Max:  82 Sum:   3636 Ratio:   0.05%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 5727408  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 9.88s
Memory:		 821MB (+24MB)
UNKNOWN
Iteration Time:	 10.97s

Iteration 40
Queue:		 [(3,15,3,True), (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,False), (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)]
Grounded Until:	 100
Blocking actions...
Solving...
[start: stats after solve call]

Models       : 0
Calls        : 41
Time         : 311.274s (Solving: 287.56s 1st Model: 0.01s Unsat: 1.26s)
CPU Time     : 311.240s

Choices      : 7695314  (Domain: 7489946)
Conflicts    : 312400   (Analyzed: 312397)
Restarts     : 3636     (Average: 85.92 Last: 175)
Model-Level  : 254.0   
Problems     : 41       (Average Length: 60.54 Splits: 0)
Lemmas       : 312397   (Deleted: 291534)
  Binary     : 7861     (Ratio:   2.52%)
  Ternary    : 1759     (Ratio:   0.56%)
  Conflict   : 312397   (Average Length:  651.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 312397   (Average: 22.64 Max: 1061 Sum: 7071567)
  Executed   : 312302   (Average: 22.62 Max: 1061 Sum: 7067929 Ratio:  99.95%)
  Bounded    : 95       (Average: 38.29 Max:  82 Sum:   3638 Ratio:   0.05%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 5727408  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 0.43s
Memory:		 821MB (+0MB)
UNSAT
Iteration Time:	 0.49s

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

Models       : 0+
Calls        : 42
Time         : 321.291s (Solving: 297.42s 1st Model: 0.01s Unsat: 1.26s)
CPU Time     : 321.264s

Choices      : 7778212  (Domain: 7572844)
Conflicts    : 320938   (Analyzed: 320935)
Restarts     : 3736     (Average: 85.90 Last: 175)
Model-Level  : 254.0   
Problems     : 42       (Average Length: 61.52 Splits: 0)
Lemmas       : 320935   (Deleted: 297578)
  Binary     : 7962     (Ratio:   2.48%)
  Ternary    : 1787     (Ratio:   0.56%)
  Conflict   : 320935   (Average Length:  648.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 320935   (Average: 22.27 Max: 1061 Sum: 7148340)
  Executed   : 320836   (Average: 22.26 Max: 1061 Sum: 7144602 Ratio:  99.95%)
  Bounded    : 99       (Average: 37.76 Max:  97 Sum:   3738 Ratio:   0.05%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 5727408  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 43
Time         : 328.910s (Solving: 304.88s 1st Model: 0.01s Unsat: 1.26s)
CPU Time     : 328.888s

Choices      : 7842415  (Domain: 7635242)
Conflicts    : 328957   (Analyzed: 328954)
Restarts     : 3836     (Average: 85.75 Last: 175)
Model-Level  : 254.0   
Problems     : 43       (Average Length: 62.47 Splits: 0)
Lemmas       : 328954   (Deleted: 305068)
  Binary     : 8032     (Ratio:   2.44%)
  Ternary    : 1809     (Ratio:   0.55%)
  Conflict   : 328954   (Average Length:  639.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 328954   (Average: 21.90 Max: 1061 Sum: 7203294)
  Executed   : 328854   (Average: 21.89 Max: 1061 Sum: 7199454 Ratio:  99.95%)
  Bounded    : 100      (Average: 38.40 Max: 102 Sum:   3840 Ratio:   0.05%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 5727408  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 44
Time         : 337.176s (Solving: 312.99s 1st Model: 0.01s Unsat: 1.26s)
CPU Time     : 337.156s

Choices      : 7925575  (Domain: 7717227)
Conflicts    : 337204   (Analyzed: 337201)
Restarts     : 3936     (Average: 85.67 Last: 175)
Model-Level  : 254.0   
Problems     : 44       (Average Length: 63.36 Splits: 0)
Lemmas       : 337201   (Deleted: 312789)
  Binary     : 8114     (Ratio:   2.41%)
  Ternary    : 1839     (Ratio:   0.55%)
  Conflict   : 337201   (Average Length:  630.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 337201   (Average: 21.58 Max: 1061 Sum: 7276712)
  Executed   : 337099   (Average: 21.57 Max: 1061 Sum: 7272668 Ratio:  99.94%)
  Bounded    : 102      (Average: 39.65 Max: 102 Sum:   4044 Ratio:   0.06%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 5727394  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 45
Time         : 345.060s (Solving: 320.70s 1st Model: 0.01s Unsat: 1.26s)
CPU Time     : 345.044s

Choices      : 7997611  (Domain: 7788740)
Conflicts    : 345433   (Analyzed: 345430)
Restarts     : 4036     (Average: 85.59 Last: 175)
Model-Level  : 254.0   
Problems     : 45       (Average Length: 64.22 Splits: 0)
Lemmas       : 345430   (Deleted: 320700)
  Binary     : 8161     (Ratio:   2.36%)
  Ternary    : 1850     (Ratio:   0.54%)
  Conflict   : 345430   (Average Length:  621.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 345430   (Average: 21.25 Max: 1061 Sum: 7339477)
  Executed   : 345328   (Average: 21.24 Max: 1061 Sum: 7335433 Ratio:  99.94%)
  Bounded    : 102      (Average: 39.65 Max: 102 Sum:   4044 Ratio:   0.06%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 5727367  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 7.82s
Memory:		 821MB (+0MB)
UNKNOWN
Iteration Time:	 7.89s

Iteration 45
Queue:		 [(8,40,2,True), (9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,False), (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)]
Grounded Until:	 100
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 46
Time         : 353.439s (Solving: 328.91s 1st Model: 0.01s Unsat: 1.26s)
CPU Time     : 353.428s

Choices      : 8100519  (Domain: 7890476)
Conflicts    : 353550   (Analyzed: 353547)
Restarts     : 4136     (Average: 85.48 Last: 175)
Model-Level  : 254.0   
Problems     : 46       (Average Length: 65.04 Splits: 0)
Lemmas       : 353547   (Deleted: 328589)
  Binary     : 8283     (Ratio:   2.34%)
  Ternary    : 1884     (Ratio:   0.53%)
  Conflict   : 353547   (Average Length:  613.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 353547   (Average: 21.02 Max: 1061 Sum: 7432066)
  Executed   : 353444   (Average: 21.01 Max: 1061 Sum: 7427925 Ratio:  99.94%)
  Bounded    : 103      (Average: 40.20 Max: 102 Sum:   4141 Ratio:   0.06%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 5727367  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

Iteration 46
Queue:		 [(9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,False), (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)]
Grounded Until:	 100
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 47
Time         : 361.667s (Solving: 336.99s 1st Model: 0.01s Unsat: 1.26s)
CPU Time     : 361.660s

Choices      : 8216292  (Domain: 8005467)
Conflicts    : 361715   (Analyzed: 361712)
Restarts     : 4236     (Average: 85.39 Last: 175)
Model-Level  : 254.0   
Problems     : 47       (Average Length: 65.83 Splits: 0)
Lemmas       : 361712   (Deleted: 336327)
  Binary     : 8344     (Ratio:   2.31%)
  Ternary    : 1906     (Ratio:   0.53%)
  Conflict   : 361712   (Average Length:  605.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 361712   (Average: 20.84 Max: 1061 Sum: 7538558)
  Executed   : 361606   (Average: 20.83 Max: 1061 Sum: 7534116 Ratio:  99.94%)
  Bounded    : 106      (Average: 41.91 Max: 102 Sum:   4442 Ratio:   0.06%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 5727367  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 8.18s
Memory:		 821MB (+0MB)
UNKNOWN
Iteration Time:	 8.24s

Iteration 47
Queue:		 [(10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,False), (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)]
Grounded Until:	 100
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 48
Time         : 369.596s (Solving: 344.74s 1st Model: 0.01s Unsat: 1.26s)
CPU Time     : 369.592s

Choices      : 8309386  (Domain: 8098255)
Conflicts    : 369874   (Analyzed: 369871)
Restarts     : 4336     (Average: 85.30 Last: 175)
Model-Level  : 254.0   
Problems     : 48       (Average Length: 66.58 Splits: 0)
Lemmas       : 369871   (Deleted: 344182)
  Binary     : 8389     (Ratio:   2.27%)
  Ternary    : 1916     (Ratio:   0.52%)
  Conflict   : 369871   (Average Length:  597.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 369871   (Average: 20.61 Max: 1061 Sum: 7622602)
  Executed   : 369762   (Average: 20.60 Max: 1061 Sum: 7617869 Ratio:  99.94%)
  Bounded    : 109      (Average: 43.42 Max: 102 Sum:   4733 Ratio:   0.06%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 5724726  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

Iteration 48
Queue:		 [(11,55,2,True), (12,60,2,True), (13,65,2,False), (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)]
Grounded Until:	 100
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 49
Time         : 376.690s (Solving: 351.69s 1st Model: 0.01s Unsat: 1.26s)
CPU Time     : 376.688s

Choices      : 8387060  (Domain: 8175628)
Conflicts    : 377753   (Analyzed: 377750)
Restarts     : 4436     (Average: 85.16 Last: 175)
Model-Level  : 254.0   
Problems     : 49       (Average Length: 67.31 Splits: 0)
Lemmas       : 377750   (Deleted: 352030)
  Binary     : 8450     (Ratio:   2.24%)
  Ternary    : 1933     (Ratio:   0.51%)
  Conflict   : 377750   (Average Length:  590.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 377750   (Average: 20.36 Max: 1061 Sum: 7690130)
  Executed   : 377637   (Average: 20.34 Max: 1061 Sum: 7684998 Ratio:  99.93%)
  Bounded    : 113      (Average: 45.42 Max: 102 Sum:   5132 Ratio:   0.07%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 5724726  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

Iteration 49
Queue:		 [(12,60,2,True), (13,65,2,False), (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)]
Grounded Until:	 100
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 50
Time         : 386.491s (Solving: 361.29s 1st Model: 0.01s Unsat: 1.26s)
CPU Time     : 386.496s

Choices      : 8718905  (Domain: 8505205)
Conflicts    : 386599   (Analyzed: 386596)
Restarts     : 4536     (Average: 85.23 Last: 175)
Model-Level  : 254.0   
Problems     : 50       (Average Length: 68.00 Splits: 0)
Lemmas       : 386596   (Deleted: 361308)
  Binary     : 8919     (Ratio:   2.31%)
  Ternary    : 2114     (Ratio:   0.55%)
  Conflict   : 386596   (Average Length:  582.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 386596   (Average: 20.71 Max: 1061 Sum: 8007308)
  Executed   : 386482   (Average: 20.70 Max: 1061 Sum: 8002079 Ratio:  99.93%)
  Bounded    : 114      (Average: 45.87 Max: 102 Sum:   5229 Ratio:   0.07%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 5724686  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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)]
Grounded Until:	 100
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 51
Time         : 394.728s (Solving: 369.36s 1st Model: 0.01s Unsat: 1.26s)
CPU Time     : 394.736s

Choices      : 9024213  (Domain: 8808303)
Conflicts    : 394396   (Analyzed: 394393)
Restarts     : 4636     (Average: 85.07 Last: 175)
Model-Level  : 254.0   
Problems     : 51       (Average Length: 68.67 Splits: 0)
Lemmas       : 394393   (Deleted: 367228)
  Binary     : 9101     (Ratio:   2.31%)
  Ternary    : 2169     (Ratio:   0.55%)
  Conflict   : 394393   (Average Length:  576.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 394393   (Average: 21.04 Max: 1061 Sum: 8296840)
  Executed   : 394279   (Average: 21.02 Max: 1061 Sum: 8291611 Ratio:  99.94%)
  Bounded    : 114      (Average: 45.87 Max: 102 Sum:   5229 Ratio:   0.06%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 5724686  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 8.18s
Memory:		 821MB (+0MB)
UNKNOWN
Iteration Time:	 8.24s

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

Models       : 0+
Calls        : 52
Time         : 404.262s (Solving: 378.74s 1st Model: 0.01s Unsat: 1.26s)
CPU Time     : 404.276s

Choices      : 9292134  (Domain: 9074978)
Conflicts    : 402431   (Analyzed: 402428)
Restarts     : 4736     (Average: 84.97 Last: 175)
Model-Level  : 254.0   
Problems     : 52       (Average Length: 69.31 Splits: 0)
Lemmas       : 402428   (Deleted: 374683)
  Binary     : 9231     (Ratio:   2.29%)
  Ternary    : 2198     (Ratio:   0.55%)
  Conflict   : 402428   (Average Length:  569.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 402428   (Average: 21.24 Max: 1075 Sum: 8547240)
  Executed   : 402314   (Average: 21.23 Max: 1075 Sum: 8542011 Ratio:  99.94%)
  Bounded    : 114      (Average: 45.87 Max: 102 Sum:   5229 Ratio:   0.06%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 5724686  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 53
Time         : 413.940s (Solving: 388.26s 1st Model: 0.01s Unsat: 1.26s)
CPU Time     : 413.960s

Choices      : 9562327  (Domain: 9344325)
Conflicts    : 410458   (Analyzed: 410455)
Restarts     : 4836     (Average: 84.87 Last: 175)
Model-Level  : 254.0   
Problems     : 53       (Average Length: 69.92 Splits: 0)
Lemmas       : 410455   (Deleted: 382351)
  Binary     : 9301     (Ratio:   2.27%)
  Ternary    : 2222     (Ratio:   0.54%)
  Conflict   : 410455   (Average Length:  564.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 410455   (Average: 21.43 Max: 1126 Sum: 8797640)
  Executed   : 410341   (Average: 21.42 Max: 1126 Sum: 8792411 Ratio:  99.94%)
  Bounded    : 114      (Average: 45.87 Max: 102 Sum:   5229 Ratio:   0.06%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 5724686  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 9.63s
Memory:		 821MB (+0MB)
UNKNOWN
Iteration Time:	 9.68s

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

Models       : 0+
Calls        : 54
Time         : 429.082s (Solving: 403.25s 1st Model: 0.01s Unsat: 1.26s)
CPU Time     : 429.108s

Choices      : 10126990 (Domain: 9906927)
Conflicts    : 419268   (Analyzed: 419265)
Restarts     : 4936     (Average: 84.94 Last: 175)
Model-Level  : 254.0   
Problems     : 54       (Average Length: 70.52 Splits: 0)
Lemmas       : 419265   (Deleted: 391947)
  Binary     : 9605     (Ratio:   2.29%)
  Ternary    : 2334     (Ratio:   0.56%)
  Conflict   : 419265   (Average Length:  558.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 419265   (Average: 22.28 Max: 1130 Sum: 9340952)
  Executed   : 419150   (Average: 22.27 Max: 1130 Sum: 9335621 Ratio:  99.94%)
  Bounded    : 115      (Average: 46.36 Max: 102 Sum:   5331 Ratio:   0.06%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 5724686  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 15.10s
Memory:		 821MB (+0MB)
UNKNOWN
Iteration Time:	 15.15s

Iteration 54
Queue:		 [(21,105,0,True), (22,110,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:		 822MB (+1MB)
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 55
Time         : 443.624s (Solving: 416.54s 1st Model: 0.01s Unsat: 1.26s)
CPU Time     : 443.656s

Choices      : 10679603 (Domain: 10455698)
Conflicts    : 428070   (Analyzed: 428067)
Restarts     : 5036     (Average: 85.00 Last: 175)
Model-Level  : 254.0   
Problems     : 55       (Average Length: 71.18 Splits: 0)
Lemmas       : 428067   (Deleted: 400883)
  Binary     : 9734     (Ratio:   2.27%)
  Ternary    : 2367     (Ratio:   0.55%)
  Conflict   : 428067   (Average Length:  563.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 428067   (Average: 23.03 Max: 1146 Sum: 9857106)
  Executed   : 427952   (Average: 23.01 Max: 1146 Sum: 9851775 Ratio:  99.95%)
  Bounded    : 115      (Average: 46.36 Max: 102 Sum:   5331 Ratio:   0.05%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 6026640  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 13.45s
Memory:		 848MB (+26MB)
UNKNOWN
Iteration Time:	 14.56s

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

Models       : 0+
Calls        : 56
Time         : 455.316s (Solving: 426.99s 1st Model: 0.01s Unsat: 1.26s)
CPU Time     : 455.352s

Choices      : 11009832 (Domain: 10784491)
Conflicts    : 435988   (Analyzed: 435985)
Restarts     : 5136     (Average: 84.89 Last: 175)
Model-Level  : 254.0   
Problems     : 56       (Average Length: 71.91 Splits: 0)
Lemmas       : 435985   (Deleted: 408670)
  Binary     : 9768     (Ratio:   2.24%)
  Ternary    : 2371     (Ratio:   0.54%)
  Conflict   : 435985   (Average Length:  571.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 435985   (Average: 23.28 Max: 1146 Sum: 10147993)
  Executed   : 435870   (Average: 23.26 Max: 1146 Sum: 10142662 Ratio:  99.95%)
  Bounded    : 115      (Average: 46.36 Max: 102 Sum:   5331 Ratio:   0.05%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 6328620  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 10.61s
Memory:		 881MB (+33MB)
UNKNOWN
Iteration Time:	 11.71s

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

Models       : 0
Calls        : 57
Time         : 466.556s (Solving: 438.01s 1st Model: 0.01s Unsat: 12.29s)
CPU Time     : 466.600s

Choices      : 11089562 (Domain: 10864221)
Conflicts    : 442558   (Analyzed: 442554)
Restarts     : 5210     (Average: 84.94 Last: 175)
Model-Level  : 254.0   
Problems     : 57       (Average Length: 72.61 Splits: 0)
Lemmas       : 442554   (Deleted: 414658)
  Binary     : 9922     (Ratio:   2.24%)
  Ternary    : 2388     (Ratio:   0.54%)
  Conflict   : 442554   (Average Length:  568.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 442554   (Average: 23.11 Max: 1146 Sum: 10226036)
  Executed   : 442431   (Average: 23.09 Max: 1146 Sum: 10220591 Ratio:  99.95%)
  Bounded    : 123      (Average: 44.27 Max: 107 Sum:   5445 Ratio:   0.05%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 6328620  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 11.16s
Memory:		 884MB (+3MB)
UNSAT
Iteration Time:	 11.25s

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,False), (12,60,3,False), (13,65,2,True), (14,70,2,True), (15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,1,True), (22,110,1,True), (23,115,0,True)]
Grounded Until:	 110
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 58
Time         : 472.195s (Solving: 443.47s 1st Model: 0.01s Unsat: 12.29s)
CPU Time     : 472.240s

Choices      : 11140666 (Domain: 10915316)
Conflicts    : 450162   (Analyzed: 450158)
Restarts     : 5310     (Average: 84.78 Last: 175)
Model-Level  : 254.0   
Problems     : 58       (Average Length: 73.29 Splits: 0)
Lemmas       : 450158   (Deleted: 420439)
  Binary     : 9993     (Ratio:   2.22%)
  Ternary    : 2417     (Ratio:   0.54%)
  Conflict   : 450158   (Average Length:  563.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 450158   (Average: 22.81 Max: 1146 Sum: 10269499)
  Executed   : 450035   (Average: 22.80 Max: 1146 Sum: 10264054 Ratio:  99.95%)
  Bounded    : 123      (Average: 44.27 Max: 107 Sum:   5445 Ratio:   0.05%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 6328620  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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,False), (12,60,3,False), (13,65,2,True), (14,70,2,True), (15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,1,True), (22,110,1,True), (23,115,0,True)]
Grounded Until:	 110
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 59
Time         : 477.975s (Solving: 449.05s 1st Model: 0.01s Unsat: 12.29s)
CPU Time     : 478.020s

Choices      : 11195924 (Domain: 10970510)
Conflicts    : 457999   (Analyzed: 457995)
Restarts     : 5410     (Average: 84.66 Last: 175)
Model-Level  : 254.0   
Problems     : 59       (Average Length: 73.95 Splits: 0)
Lemmas       : 457995   (Deleted: 427638)
  Binary     : 10078    (Ratio:   2.20%)
  Ternary    : 2438     (Ratio:   0.53%)
  Conflict   : 457995   (Average Length:  558.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 457995   (Average: 22.53 Max: 1146 Sum: 10317774)
  Executed   : 457870   (Average: 22.52 Max: 1146 Sum: 10312110 Ratio:  99.95%)
  Bounded    : 125      (Average: 45.31 Max: 112 Sum:   5664 Ratio:   0.05%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 6328620  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 60
Time         : 485.713s (Solving: 456.59s 1st Model: 0.01s Unsat: 12.29s)
CPU Time     : 485.764s

Choices      : 11299372 (Domain: 11072098)
Conflicts    : 466473   (Analyzed: 466469)
Restarts     : 5510     (Average: 84.66 Last: 175)
Model-Level  : 254.0   
Problems     : 60       (Average Length: 74.58 Splits: 0)
Lemmas       : 466469   (Deleted: 435134)
  Binary     : 10300    (Ratio:   2.21%)
  Ternary    : 2544     (Ratio:   0.55%)
  Conflict   : 466469   (Average Length:  552.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 466469   (Average: 22.32 Max: 1146 Sum: 10410869)
  Executed   : 466342   (Average: 22.31 Max: 1146 Sum: 10404986 Ratio:  99.94%)
  Bounded    : 127      (Average: 46.32 Max: 112 Sum:   5883 Ratio:   0.06%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 6328606  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 61
Time         : 493.456s (Solving: 464.11s 1st Model: 0.01s Unsat: 12.29s)
CPU Time     : 493.508s

Choices      : 11420205 (Domain: 11191068)
Conflicts    : 475017   (Analyzed: 475013)
Restarts     : 5610     (Average: 84.67 Last: 175)
Model-Level  : 254.0   
Problems     : 61       (Average Length: 75.20 Splits: 0)
Lemmas       : 475013   (Deleted: 443064)
  Binary     : 10587    (Ratio:   2.23%)
  Ternary    : 2626     (Ratio:   0.55%)
  Conflict   : 475013   (Average Length:  547.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 475013   (Average: 22.15 Max: 1146 Sum: 10520141)
  Executed   : 474886   (Average: 22.13 Max: 1146 Sum: 10514258 Ratio:  99.94%)
  Bounded    : 127      (Average: 46.32 Max: 112 Sum:   5883 Ratio:   0.06%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 6328580  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 62
Time         : 500.880s (Solving: 471.35s 1st Model: 0.01s Unsat: 12.29s)
CPU Time     : 500.936s

Choices      : 11544660 (Domain: 11313881)
Conflicts    : 482966   (Analyzed: 482962)
Restarts     : 5710     (Average: 84.58 Last: 175)
Model-Level  : 254.0   
Problems     : 62       (Average Length: 75.79 Splits: 0)
Lemmas       : 482962   (Deleted: 451002)
  Binary     : 10724    (Ratio:   2.22%)
  Ternary    : 2664     (Ratio:   0.55%)
  Conflict   : 482962   (Average Length:  543.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 482962   (Average: 22.02 Max: 1146 Sum: 10632575)
  Executed   : 482835   (Average: 22.00 Max: 1146 Sum: 10626692 Ratio:  99.94%)
  Bounded    : 127      (Average: 46.32 Max: 112 Sum:   5883 Ratio:   0.06%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 6328580  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 63
Time         : 510.227s (Solving: 480.52s 1st Model: 0.01s Unsat: 12.29s)
CPU Time     : 510.288s

Choices      : 11752698 (Domain: 11519372)
Conflicts    : 491386   (Analyzed: 491382)
Restarts     : 5810     (Average: 84.58 Last: 175)
Model-Level  : 254.0   
Problems     : 63       (Average Length: 76.37 Splits: 0)
Lemmas       : 491382   (Deleted: 458343)
  Binary     : 11120    (Ratio:   2.26%)
  Ternary    : 2838     (Ratio:   0.58%)
  Conflict   : 491382   (Average Length:  538.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 491382   (Average: 22.03 Max: 1146 Sum: 10825014)
  Executed   : 491254   (Average: 22.02 Max: 1146 Sum: 10819019 Ratio:  99.94%)
  Bounded    : 128      (Average: 46.84 Max: 112 Sum:   5995 Ratio:   0.06%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 6328580  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 9.29s
Memory:		 884MB (+0MB)
UNKNOWN
Iteration Time:	 9.35s

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

Models       : 0+
Calls        : 64
Time         : 517.566s (Solving: 487.69s 1st Model: 0.01s Unsat: 12.29s)
CPU Time     : 517.632s

Choices      : 11913679 (Domain: 11679834)
Conflicts    : 499648   (Analyzed: 499644)
Restarts     : 5910     (Average: 84.54 Last: 175)
Model-Level  : 254.0   
Problems     : 64       (Average Length: 76.92 Splits: 0)
Lemmas       : 499644   (Deleted: 465893)
  Binary     : 11349    (Ratio:   2.27%)
  Ternary    : 2891     (Ratio:   0.58%)
  Conflict   : 499644   (Average Length:  533.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 499644   (Average: 21.96 Max: 1146 Sum: 10971841)
  Executed   : 499515   (Average: 21.95 Max: 1146 Sum: 10965739 Ratio:  99.94%)
  Bounded    : 129      (Average: 47.30 Max: 112 Sum:   6102 Ratio:   0.06%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 6328554  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 7.29s
Memory:		 884MB (+0MB)
UNKNOWN
Iteration Time:	 7.34s

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

Models       : 0+
Calls        : 65
Time         : 526.309s (Solving: 496.25s 1st Model: 0.01s Unsat: 12.29s)
CPU Time     : 526.376s

Choices      : 12115412 (Domain: 11880075)
Conflicts    : 507889   (Analyzed: 507885)
Restarts     : 6010     (Average: 84.51 Last: 175)
Model-Level  : 254.0   
Problems     : 65       (Average Length: 77.46 Splits: 0)
Lemmas       : 507885   (Deleted: 473600)
  Binary     : 11555    (Ratio:   2.28%)
  Ternary    : 2941     (Ratio:   0.58%)
  Conflict   : 507885   (Average Length:  529.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 507885   (Average: 21.97 Max: 1146 Sum: 11157853)
  Executed   : 507756   (Average: 21.96 Max: 1146 Sum: 11151751 Ratio:  99.95%)
  Bounded    : 129      (Average: 47.30 Max: 112 Sum:   6102 Ratio:   0.05%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 6328554  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 8.68s
Memory:		 884MB (+0MB)
UNKNOWN
Iteration Time:	 8.75s

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

Models       : 0+
Calls        : 66
Time         : 531.173s (Solving: 500.94s 1st Model: 0.01s Unsat: 12.29s)
CPU Time     : 531.240s

Choices      : 12257399 (Domain: 12021648)
Conflicts    : 515266   (Analyzed: 515262)
Restarts     : 6110     (Average: 84.33 Last: 175)
Model-Level  : 254.0   
Problems     : 66       (Average Length: 77.98 Splits: 0)
Lemmas       : 515262   (Deleted: 481624)
  Binary     : 11680    (Ratio:   2.27%)
  Ternary    : 2981     (Ratio:   0.58%)
  Conflict   : 515262   (Average Length:  524.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 515262   (Average: 21.90 Max: 1146 Sum: 11283889)
  Executed   : 515133   (Average: 21.89 Max: 1146 Sum: 11277787 Ratio:  99.95%)
  Bounded    : 129      (Average: 47.30 Max: 112 Sum:   6102 Ratio:   0.05%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 6328554  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 67
Time         : 541.644s (Solving: 511.24s 1st Model: 0.01s Unsat: 12.29s)
CPU Time     : 541.716s

Choices      : 12611331 (Domain: 12374369)
Conflicts    : 523435   (Analyzed: 523431)
Restarts     : 6210     (Average: 84.29 Last: 175)
Model-Level  : 254.0   
Problems     : 67       (Average Length: 78.49 Splits: 0)
Lemmas       : 523431   (Deleted: 488321)
  Binary     : 12008    (Ratio:   2.29%)
  Ternary    : 3047     (Ratio:   0.58%)
  Conflict   : 523431   (Average Length:  520.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 523431   (Average: 22.19 Max: 1227 Sum: 11616138)
  Executed   : 523301   (Average: 22.18 Max: 1227 Sum: 11609924 Ratio:  99.95%)
  Bounded    : 130      (Average: 47.80 Max: 112 Sum:   6214 Ratio:   0.05%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 6328554  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 68
Time         : 553.874s (Solving: 523.30s 1st Model: 0.01s Unsat: 12.29s)
CPU Time     : 553.952s

Choices      : 12992440 (Domain: 12754027)
Conflicts    : 531758   (Analyzed: 531754)
Restarts     : 6310     (Average: 84.27 Last: 175)
Model-Level  : 254.0   
Problems     : 68       (Average Length: 78.99 Splits: 0)
Lemmas       : 531754   (Deleted: 495804)
  Binary     : 12298    (Ratio:   2.31%)
  Ternary    : 3145     (Ratio:   0.59%)
  Conflict   : 531754   (Average Length:  515.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 531754   (Average: 22.52 Max: 1313 Sum: 11973008)
  Executed   : 531624   (Average: 22.50 Max: 1313 Sum: 11966794 Ratio:  99.95%)
  Bounded    : 130      (Average: 47.80 Max: 112 Sum:   6214 Ratio:   0.05%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 6328540  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 12.18s
Memory:		 884MB (+0MB)
UNKNOWN
Iteration Time:	 12.24s

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

Models       : 0+
Calls        : 69
Time         : 570.212s (Solving: 538.31s 1st Model: 0.01s Unsat: 12.29s)
CPU Time     : 570.296s

Choices      : 13409834 (Domain: 13170777)
Conflicts    : 541304   (Analyzed: 541300)
Restarts     : 6410     (Average: 84.45 Last: 175)
Model-Level  : 254.0   
Problems     : 69       (Average Length: 79.54 Splits: 0)
Lemmas       : 541300   (Deleted: 505809)
  Binary     : 12573    (Ratio:   2.32%)
  Ternary    : 3215     (Ratio:   0.59%)
  Conflict   : 541300   (Average Length:  521.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 541300   (Average: 22.82 Max: 1313 Sum: 12349815)
  Executed   : 541170   (Average: 22.80 Max: 1313 Sum: 12343601 Ratio:  99.95%)
  Bounded    : 130      (Average: 47.80 Max: 112 Sum:   6214 Ratio:   0.05%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 6630520  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 15.18s
Memory:		 973MB (+89MB)
UNKNOWN
Iteration Time:	 16.36s

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

Models       : 0+
Calls        : 70
Time         : 574.954s (Solving: 542.86s 1st Model: 0.01s Unsat: 12.29s)
CPU Time     : 575.040s

Choices      : 13446171 (Domain: 13207114)
Conflicts    : 548635   (Analyzed: 548631)
Restarts     : 6510     (Average: 84.28 Last: 175)
Model-Level  : 254.0   
Problems     : 70       (Average Length: 80.07 Splits: 0)
Lemmas       : 548631   (Deleted: 512656)
  Binary     : 12660    (Ratio:   2.31%)
  Ternary    : 3219     (Ratio:   0.59%)
  Conflict   : 548631   (Average Length:  518.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 548631   (Average: 22.56 Max: 1313 Sum: 12377314)
  Executed   : 548501   (Average: 22.55 Max: 1313 Sum: 12371100 Ratio:  99.95%)
  Bounded    : 130      (Average: 47.80 Max: 112 Sum:   6214 Ratio:   0.05%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 6630520  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 71
Time         : 579.391s (Solving: 547.09s 1st Model: 0.01s Unsat: 12.29s)
CPU Time     : 579.480s

Choices      : 13491098 (Domain: 13252041)
Conflicts    : 556034   (Analyzed: 556030)
Restarts     : 6610     (Average: 84.12 Last: 175)
Model-Level  : 254.0   
Problems     : 71       (Average Length: 80.59 Splits: 0)
Lemmas       : 556030   (Deleted: 519769)
  Binary     : 12694    (Ratio:   2.28%)
  Ternary    : 3227     (Ratio:   0.58%)
  Conflict   : 556030   (Average Length:  514.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 556030   (Average: 22.32 Max: 1313 Sum: 12413263)
  Executed   : 555900   (Average: 22.31 Max: 1313 Sum: 12407049 Ratio:  99.95%)
  Bounded    : 130      (Average: 47.80 Max: 112 Sum:   6214 Ratio:   0.05%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 6630520  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 72
Time         : 585.615s (Solving: 553.14s 1st Model: 0.01s Unsat: 12.29s)
CPU Time     : 585.708s

Choices      : 13531946 (Domain: 13292889)
Conflicts    : 563864   (Analyzed: 563860)
Restarts     : 6710     (Average: 84.03 Last: 175)
Model-Level  : 254.0   
Problems     : 72       (Average Length: 81.10 Splits: 0)
Lemmas       : 563860   (Deleted: 526767)
  Binary     : 12787    (Ratio:   2.27%)
  Ternary    : 3256     (Ratio:   0.58%)
  Conflict   : 563860   (Average Length:  511.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 563860   (Average: 22.08 Max: 1313 Sum: 12447450)
  Executed   : 563729   (Average: 22.06 Max: 1313 Sum: 12441124 Ratio:  99.95%)
  Bounded    : 131      (Average: 48.29 Max: 112 Sum:   6326 Ratio:   0.05%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 6630520  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 73
Time         : 592.702s (Solving: 560.05s 1st Model: 0.01s Unsat: 12.29s)
CPU Time     : 592.796s

Choices      : 13614649 (Domain: 13374499)
Conflicts    : 571828   (Analyzed: 571824)
Restarts     : 6810     (Average: 83.97 Last: 175)
Model-Level  : 254.0   
Problems     : 73       (Average Length: 81.59 Splits: 0)
Lemmas       : 571824   (Deleted: 534296)
  Binary     : 12927    (Ratio:   2.26%)
  Ternary    : 3312     (Ratio:   0.58%)
  Conflict   : 571824   (Average Length:  507.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 571824   (Average: 21.89 Max: 1313 Sum: 12518622)
  Executed   : 571693   (Average: 21.88 Max: 1313 Sum: 12512296 Ratio:  99.95%)
  Bounded    : 131      (Average: 48.29 Max: 112 Sum:   6326 Ratio:   0.05%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 6630520  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 7.03s
Memory:		 973MB (+0MB)
UNKNOWN
Iteration Time:	 7.09s

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

Models       : 0+
Calls        : 74
Time         : 602.183s (Solving: 569.35s 1st Model: 0.01s Unsat: 12.29s)
CPU Time     : 602.280s

Choices      : 13776933 (Domain: 13533403)
Conflicts    : 580467   (Analyzed: 580463)
Restarts     : 6910     (Average: 84.00 Last: 175)
Model-Level  : 254.0   
Problems     : 74       (Average Length: 82.07 Splits: 0)
Lemmas       : 580463   (Deleted: 543005)
  Binary     : 13444    (Ratio:   2.32%)
  Ternary    : 3517     (Ratio:   0.61%)
  Conflict   : 580463   (Average Length:  503.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 580463   (Average: 21.82 Max: 1313 Sum: 12662988)
  Executed   : 580332   (Average: 21.80 Max: 1313 Sum: 12656662 Ratio:  99.95%)
  Bounded    : 131      (Average: 48.29 Max: 112 Sum:   6326 Ratio:   0.05%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 6630520  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 75
Time         : 612.329s (Solving: 579.32s 1st Model: 0.01s Unsat: 12.29s)
CPU Time     : 612.428s

Choices      : 13937524 (Domain: 13692561)
Conflicts    : 589145   (Analyzed: 589141)
Restarts     : 7010     (Average: 84.04 Last: 175)
Model-Level  : 254.0   
Problems     : 75       (Average Length: 82.53 Splits: 0)
Lemmas       : 589141   (Deleted: 550894)
  Binary     : 13829    (Ratio:   2.35%)
  Ternary    : 3671     (Ratio:   0.62%)
  Conflict   : 589141   (Average Length:  500.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 589141   (Average: 21.74 Max: 1313 Sum: 12805704)
  Executed   : 589010   (Average: 21.73 Max: 1313 Sum: 12799378 Ratio:  99.95%)
  Bounded    : 131      (Average: 48.29 Max: 112 Sum:   6326 Ratio:   0.05%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 6630520  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 76
Time         : 615.550s (Solving: 582.35s 1st Model: 0.01s Unsat: 12.29s)
CPU Time     : 615.648s

Choices      : 13983157 (Domain: 13737812)
Conflicts    : 596233   (Analyzed: 596229)
Restarts     : 7110     (Average: 83.86 Last: 175)
Model-Level  : 254.0   
Problems     : 76       (Average Length: 82.99 Splits: 0)
Lemmas       : 596229   (Deleted: 557136)
  Binary     : 13869    (Ratio:   2.33%)
  Ternary    : 3677     (Ratio:   0.62%)
  Conflict   : 596229   (Average Length:  497.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 596229   (Average: 21.53 Max: 1313 Sum: 12839165)
  Executed   : 596098   (Average: 21.52 Max: 1313 Sum: 12832839 Ratio:  99.95%)
  Bounded    : 131      (Average: 48.29 Max: 112 Sum:   6326 Ratio:   0.05%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 6630520  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 77
Time         : 624.307s (Solving: 590.89s 1st Model: 0.01s Unsat: 12.29s)
CPU Time     : 624.408s

Choices      : 14099868 (Domain: 13854097)
Conflicts    : 604263   (Analyzed: 604259)
Restarts     : 7210     (Average: 83.81 Last: 175)
Model-Level  : 254.0   
Problems     : 77       (Average Length: 83.43 Splits: 0)
Lemmas       : 604259   (Deleted: 563960)
  Binary     : 14006    (Ratio:   2.32%)
  Ternary    : 3718     (Ratio:   0.62%)
  Conflict   : 604259   (Average Length:  493.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 604259   (Average: 21.42 Max: 1313 Sum: 12941884)
  Executed   : 604128   (Average: 21.41 Max: 1313 Sum: 12935558 Ratio:  99.95%)
  Bounded    : 131      (Average: 48.29 Max: 112 Sum:   6326 Ratio:   0.05%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 6630520  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 8.68s
Memory:		 973MB (+0MB)
UNKNOWN
Iteration Time:	 8.76s

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

Models       : 0+
Calls        : 78
Time         : 632.869s (Solving: 599.27s 1st Model: 0.01s Unsat: 12.29s)
CPU Time     : 632.976s

Choices      : 14246362 (Domain: 13999342)
Conflicts    : 612492   (Analyzed: 612488)
Restarts     : 7310     (Average: 83.79 Last: 175)
Model-Level  : 254.0   
Problems     : 78       (Average Length: 83.86 Splits: 0)
Lemmas       : 612488   (Deleted: 571449)
  Binary     : 14232    (Ratio:   2.32%)
  Ternary    : 3802     (Ratio:   0.62%)
  Conflict   : 612488   (Average Length:  491.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 612488   (Average: 21.34 Max: 1313 Sum: 13071729)
  Executed   : 612357   (Average: 21.33 Max: 1313 Sum: 13065403 Ratio:  99.95%)
  Bounded    : 131      (Average: 48.29 Max: 112 Sum:   6326 Ratio:   0.05%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 6630520  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 79
Time         : 646.626s (Solving: 612.84s 1st Model: 0.01s Unsat: 12.29s)
CPU Time     : 646.740s

Choices      : 14610259 (Domain: 14361153)
Conflicts    : 621443   (Analyzed: 621439)
Restarts     : 7410     (Average: 83.86 Last: 175)
Model-Level  : 254.0   
Problems     : 79       (Average Length: 84.28 Splits: 0)
Lemmas       : 621439   (Deleted: 580923)
  Binary     : 14666    (Ratio:   2.36%)
  Ternary    : 3901     (Ratio:   0.63%)
  Conflict   : 621439   (Average Length:  488.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 621439   (Average: 21.58 Max: 1313 Sum: 13412106)
  Executed   : 621307   (Average: 21.57 Max: 1313 Sum: 13405668 Ratio:  99.95%)
  Bounded    : 132      (Average: 48.77 Max: 112 Sum:   6438 Ratio:   0.05%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 6630520  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 13.70s
Memory:		 973MB (+0MB)
UNKNOWN
Iteration Time:	 13.76s

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

Models       : 0+
Calls        : 80
Time         : 658.985s (Solving: 625.02s 1st Model: 0.01s Unsat: 12.29s)
CPU Time     : 659.104s

Choices      : 14911412 (Domain: 14660787)
Conflicts    : 630232   (Analyzed: 630228)
Restarts     : 7510     (Average: 83.92 Last: 175)
Model-Level  : 254.0   
Problems     : 80       (Average Length: 84.69 Splits: 0)
Lemmas       : 630228   (Deleted: 589240)
  Binary     : 14941    (Ratio:   2.37%)
  Ternary    : 3964     (Ratio:   0.63%)
  Conflict   : 630228   (Average Length:  486.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 630228   (Average: 21.73 Max: 1313 Sum: 13691843)
  Executed   : 630096   (Average: 21.72 Max: 1313 Sum: 13685405 Ratio:  99.95%)
  Bounded    : 132      (Average: 48.77 Max: 112 Sum:   6438 Ratio:   0.05%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 6630520  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 12.31s
Memory:		 973MB (+0MB)
UNKNOWN
Iteration Time:	 12.37s

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

Models       : 0+
Calls        : 81
Time         : 670.846s (Solving: 636.71s 1st Model: 0.01s Unsat: 12.29s)
CPU Time     : 670.972s

Choices      : 15197297 (Domain: 14945608)
Conflicts    : 638728   (Analyzed: 638724)
Restarts     : 7610     (Average: 83.93 Last: 175)
Model-Level  : 254.0   
Problems     : 81       (Average Length: 85.09 Splits: 0)
Lemmas       : 638724   (Deleted: 595481)
  Binary     : 15128    (Ratio:   2.37%)
  Ternary    : 4007     (Ratio:   0.63%)
  Conflict   : 638724   (Average Length:  483.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 638724   (Average: 21.85 Max: 1313 Sum: 13955446)
  Executed   : 638592   (Average: 21.84 Max: 1313 Sum: 13949008 Ratio:  99.95%)
  Bounded    : 132      (Average: 48.77 Max: 112 Sum:   6438 Ratio:   0.05%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 6630520  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 82
Time         : 683.609s (Solving: 649.27s 1st Model: 0.01s Unsat: 12.29s)
CPU Time     : 683.740s

Choices      : 15538119 (Domain: 15285849)
Conflicts    : 646852   (Analyzed: 646848)
Restarts     : 7710     (Average: 83.90 Last: 175)
Model-Level  : 254.0   
Problems     : 82       (Average Length: 85.48 Splits: 0)
Lemmas       : 646848   (Deleted: 603429)
  Binary     : 15323    (Ratio:   2.37%)
  Ternary    : 4043     (Ratio:   0.63%)
  Conflict   : 646848   (Average Length:  481.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 646848   (Average: 22.06 Max: 1313 Sum: 14271484)
  Executed   : 646716   (Average: 22.05 Max: 1313 Sum: 14265046 Ratio:  99.95%)
  Bounded    : 132      (Average: 48.77 Max: 112 Sum:   6438 Ratio:   0.05%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 6630520  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 12.69s
Memory:		 973MB (+0MB)
UNKNOWN
Iteration Time:	 12.77s

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

Models       : 0+
Calls        : 83
Time         : 698.253s (Solving: 662.61s 1st Model: 0.01s Unsat: 12.29s)
CPU Time     : 698.392s

Choices      : 15771287 (Domain: 15518801)
Conflicts    : 655429   (Analyzed: 655425)
Restarts     : 7810     (Average: 83.92 Last: 175)
Model-Level  : 254.0   
Problems     : 83       (Average Length: 85.92 Splits: 0)
Lemmas       : 655425   (Deleted: 611775)
  Binary     : 15369    (Ratio:   2.34%)
  Ternary    : 4053     (Ratio:   0.62%)
  Conflict   : 655425   (Average Length:  488.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 655425   (Average: 22.07 Max: 1313 Sum: 14463238)
  Executed   : 655293   (Average: 22.06 Max: 1313 Sum: 14456800 Ratio:  99.96%)
  Bounded    : 132      (Average: 48.77 Max: 112 Sum:   6438 Ratio:   0.04%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 6932500  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 13.51s
Memory:		 995MB (+22MB)
UNKNOWN
Iteration Time:	 14.66s

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

Models       : 0+
Calls        : 84
Time         : 703.781s (Solving: 667.94s 1st Model: 0.01s Unsat: 12.29s)
CPU Time     : 703.924s

Choices      : 15805574 (Domain: 15553088)
Conflicts    : 663000   (Analyzed: 662996)
Restarts     : 7910     (Average: 83.82 Last: 175)
Model-Level  : 254.0   
Problems     : 84       (Average Length: 86.35 Splits: 0)
Lemmas       : 662996   (Deleted: 619824)
  Binary     : 15385    (Ratio:   2.32%)
  Ternary    : 4058     (Ratio:   0.61%)
  Conflict   : 662996   (Average Length:  486.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 662996   (Average: 21.86 Max: 1313 Sum: 14489901)
  Executed   : 662864   (Average: 21.85 Max: 1313 Sum: 14483463 Ratio:  99.96%)
  Bounded    : 132      (Average: 48.77 Max: 112 Sum:   6438 Ratio:   0.04%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 6932500  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 85
Time         : 710.958s (Solving: 674.94s 1st Model: 0.01s Unsat: 12.29s)
CPU Time     : 711.108s

Choices      : 15868523 (Domain: 15616037)
Conflicts    : 671189   (Analyzed: 671185)
Restarts     : 8010     (Average: 83.79 Last: 175)
Model-Level  : 254.0   
Problems     : 85       (Average Length: 86.76 Splits: 0)
Lemmas       : 671185   (Deleted: 627106)
  Binary     : 15416    (Ratio:   2.30%)
  Ternary    : 4081     (Ratio:   0.61%)
  Conflict   : 671185   (Average Length:  484.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 671185   (Average: 21.67 Max: 1313 Sum: 14542116)
  Executed   : 671052   (Average: 21.66 Max: 1313 Sum: 14535556 Ratio:  99.95%)
  Bounded    : 133      (Average: 49.32 Max: 122 Sum:   6560 Ratio:   0.05%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 6932500  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 86
Time         : 720.193s (Solving: 683.94s 1st Model: 0.01s Unsat: 12.29s)
CPU Time     : 720.348s

Choices      : 15998224 (Domain: 15745738)
Conflicts    : 679540   (Analyzed: 679536)
Restarts     : 8110     (Average: 83.79 Last: 175)
Model-Level  : 254.0   
Problems     : 86       (Average Length: 87.17 Splits: 0)
Lemmas       : 679536   (Deleted: 634806)
  Binary     : 15514    (Ratio:   2.28%)
  Ternary    : 4107     (Ratio:   0.60%)
  Conflict   : 679536   (Average Length:  482.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 679536   (Average: 21.57 Max: 1313 Sum: 14659332)
  Executed   : 679403   (Average: 21.56 Max: 1313 Sum: 14652772 Ratio:  99.96%)
  Bounded    : 133      (Average: 49.32 Max: 122 Sum:   6560 Ratio:   0.04%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 6932486  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 87
Time         : 727.501s (Solving: 691.05s 1st Model: 0.01s Unsat: 12.29s)
CPU Time     : 727.660s

Choices      : 16054400 (Domain: 15801914)
Conflicts    : 687311   (Analyzed: 687307)
Restarts     : 8210     (Average: 83.72 Last: 175)
Model-Level  : 254.0   
Problems     : 87       (Average Length: 87.57 Splits: 0)
Lemmas       : 687307   (Deleted: 642710)
  Binary     : 15594    (Ratio:   2.27%)
  Ternary    : 4132     (Ratio:   0.60%)
  Conflict   : 687307   (Average Length:  480.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 687307   (Average: 21.40 Max: 1313 Sum: 14706257)
  Executed   : 687171   (Average: 21.39 Max: 1313 Sum: 14699336 Ratio:  99.95%)
  Bounded    : 136      (Average: 50.89 Max: 122 Sum:   6921 Ratio:   0.05%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 6932486  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 88
Time         : 734.932s (Solving: 698.28s 1st Model: 0.01s Unsat: 12.29s)
CPU Time     : 735.096s

Choices      : 16165621 (Domain: 15911533)
Conflicts    : 695340   (Analyzed: 695336)
Restarts     : 8310     (Average: 83.67 Last: 175)
Model-Level  : 254.0   
Problems     : 88       (Average Length: 87.97 Splits: 0)
Lemmas       : 695336   (Deleted: 650072)
  Binary     : 15737    (Ratio:   2.26%)
  Ternary    : 4154     (Ratio:   0.60%)
  Conflict   : 695336   (Average Length:  478.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 695336   (Average: 21.29 Max: 1313 Sum: 14803973)
  Executed   : 695200   (Average: 21.28 Max: 1313 Sum: 14797052 Ratio:  99.95%)
  Bounded    : 136      (Average: 50.89 Max: 122 Sum:   6921 Ratio:   0.05%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 6932449  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 89
Time         : 747.379s (Solving: 710.54s 1st Model: 0.01s Unsat: 12.29s)
CPU Time     : 747.548s

Choices      : 16364648 (Domain: 16109060)
Conflicts    : 703984   (Analyzed: 703980)
Restarts     : 8410     (Average: 83.71 Last: 175)
Model-Level  : 254.0   
Problems     : 89       (Average Length: 88.35 Splits: 0)
Lemmas       : 703980   (Deleted: 659522)
  Binary     : 16043    (Ratio:   2.28%)
  Ternary    : 4195     (Ratio:   0.60%)
  Conflict   : 703980   (Average Length:  476.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 703980   (Average: 21.29 Max: 1313 Sum: 14984301)
  Executed   : 703844   (Average: 21.28 Max: 1313 Sum: 14977380 Ratio:  99.95%)
  Bounded    : 136      (Average: 50.89 Max: 122 Sum:   6921 Ratio:   0.05%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 6932449  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 90
Time         : 758.875s (Solving: 721.84s 1st Model: 0.01s Unsat: 12.29s)
CPU Time     : 759.048s

Choices      : 16580047 (Domain: 16322792)
Conflicts    : 712296   (Analyzed: 712292)
Restarts     : 8510     (Average: 83.70 Last: 175)
Model-Level  : 254.0   
Problems     : 90       (Average Length: 88.72 Splits: 0)
Lemmas       : 712292   (Deleted: 665591)
  Binary     : 16346    (Ratio:   2.29%)
  Ternary    : 4260     (Ratio:   0.60%)
  Conflict   : 712292   (Average Length:  474.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 712292   (Average: 21.31 Max: 1313 Sum: 15177233)
  Executed   : 712156   (Average: 21.30 Max: 1313 Sum: 15170312 Ratio:  99.95%)
  Bounded    : 136      (Average: 50.89 Max: 122 Sum:   6921 Ratio:   0.05%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 6932449  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

Iteration 90
Queue:		 [(19,95,2,True), (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        : 91
Time         : 773.112s (Solving: 735.88s 1st Model: 0.01s Unsat: 12.29s)
CPU Time     : 773.292s

Choices      : 16853495 (Domain: 16595624)
Conflicts    : 720916   (Analyzed: 720912)
Restarts     : 8610     (Average: 83.73 Last: 175)
Model-Level  : 254.0   
Problems     : 91       (Average Length: 89.09 Splits: 0)
Lemmas       : 720912   (Deleted: 675097)
  Binary     : 16661    (Ratio:   2.31%)
  Ternary    : 4309     (Ratio:   0.60%)
  Conflict   : 720912   (Average Length:  473.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 720912   (Average: 21.40 Max: 1313 Sum: 15425534)
  Executed   : 720775   (Average: 21.39 Max: 1313 Sum: 15418491 Ratio:  99.95%)
  Bounded    : 137      (Average: 51.41 Max: 122 Sum:   7043 Ratio:   0.05%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 6932449  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 92
Time         : 788.163s (Solving: 750.74s 1st Model: 0.01s Unsat: 12.29s)
CPU Time     : 788.348s

Choices      : 17177392 (Domain: 16919325)
Conflicts    : 729150   (Analyzed: 729146)
Restarts     : 8710     (Average: 83.71 Last: 175)
Model-Level  : 254.0   
Problems     : 92       (Average Length: 89.45 Splits: 0)
Lemmas       : 729146   (Deleted: 681441)
  Binary     : 16992    (Ratio:   2.33%)
  Ternary    : 4349     (Ratio:   0.60%)
  Conflict   : 729146   (Average Length:  472.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 729146   (Average: 21.56 Max: 1456 Sum: 15718597)
  Executed   : 729009   (Average: 21.55 Max: 1456 Sum: 15711554 Ratio:  99.96%)
  Bounded    : 137      (Average: 51.41 Max: 122 Sum:   7043 Ratio:   0.04%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 6932435  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

Iteration 92
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        : 93
Time         : 792.979s (Solving: 755.37s 1st Model: 0.01s Unsat: 12.29s)
CPU Time     : 793.168s

Choices      : 17213665 (Domain: 16955598)
Conflicts    : 736679   (Analyzed: 736675)
Restarts     : 8810     (Average: 83.62 Last: 175)
Model-Level  : 254.0   
Problems     : 93       (Average Length: 89.80 Splits: 0)
Lemmas       : 736675   (Deleted: 689255)
  Binary     : 17005    (Ratio:   2.31%)
  Ternary    : 4352     (Ratio:   0.59%)
  Conflict   : 736675   (Average Length:  471.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 736675   (Average: 21.38 Max: 1456 Sum: 15746780)
  Executed   : 736538   (Average: 21.37 Max: 1456 Sum: 15739737 Ratio:  99.96%)
  Bounded    : 137      (Average: 51.41 Max: 122 Sum:   7043 Ratio:   0.04%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 6932435  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

Iteration 93
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        : 94
Time         : 802.882s (Solving: 765.08s 1st Model: 0.01s Unsat: 12.29s)
CPU Time     : 803.072s

Choices      : 17285111 (Domain: 17027044)
Conflicts    : 745231   (Analyzed: 745227)
Restarts     : 8910     (Average: 83.64 Last: 175)
Model-Level  : 254.0   
Problems     : 94       (Average Length: 90.14 Splits: 0)
Lemmas       : 745227   (Deleted: 696548)
  Binary     : 17143    (Ratio:   2.30%)
  Ternary    : 4371     (Ratio:   0.59%)
  Conflict   : 745227   (Average Length:  474.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 745227   (Average: 21.21 Max: 1456 Sum: 15803740)
  Executed   : 745089   (Average: 21.20 Max: 1456 Sum: 15796575 Ratio:  99.95%)
  Bounded    : 138      (Average: 51.92 Max: 122 Sum:   7165 Ratio:   0.05%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 6932435  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

Iteration 94
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        : 95
Time         : 808.597s (Solving: 770.57s 1st Model: 0.01s Unsat: 12.29s)
CPU Time     : 808.792s

Choices      : 17325774 (Domain: 17067707)
Conflicts    : 753155   (Analyzed: 753151)
Restarts     : 9010     (Average: 83.59 Last: 175)
Model-Level  : 254.0   
Problems     : 95       (Average Length: 90.47 Splits: 0)
Lemmas       : 753151   (Deleted: 704737)
  Binary     : 17170    (Ratio:   2.28%)
  Ternary    : 4377     (Ratio:   0.58%)
  Conflict   : 753151   (Average Length:  472.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 753151   (Average: 21.03 Max: 1456 Sum: 15836845)
  Executed   : 753009   (Average: 21.02 Max: 1456 Sum: 15829197 Ratio:  99.95%)
  Bounded    : 142      (Average: 53.86 Max: 122 Sum:   7648 Ratio:   0.05%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 6932421  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

Iteration 95
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        : 96
Time         : 814.108s (Solving: 775.88s 1st Model: 0.01s Unsat: 12.29s)
CPU Time     : 814.304s

Choices      : 17392914 (Domain: 17134799)
Conflicts    : 760999   (Analyzed: 760995)
Restarts     : 9110     (Average: 83.53 Last: 175)
Model-Level  : 254.0   
Problems     : 96       (Average Length: 90.80 Splits: 0)
Lemmas       : 760995   (Deleted: 712312)
  Binary     : 17224    (Ratio:   2.26%)
  Ternary    : 4386     (Ratio:   0.58%)
  Conflict   : 760995   (Average Length:  470.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 760995   (Average: 20.89 Max: 1456 Sum: 15893771)
  Executed   : 760853   (Average: 20.88 Max: 1456 Sum: 15886123 Ratio:  99.95%)
  Bounded    : 142      (Average: 53.86 Max: 122 Sum:   7648 Ratio:   0.05%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 6932379  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

Iteration 96
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        : 97
Time         : 825.024s (Solving: 786.61s 1st Model: 0.01s Unsat: 12.29s)
CPU Time     : 825.224s

Choices      : 17539391 (Domain: 17280896)
Conflicts    : 769512   (Analyzed: 769508)
Restarts     : 9210     (Average: 83.55 Last: 175)
Model-Level  : 254.0   
Problems     : 97       (Average Length: 91.12 Splits: 0)
Lemmas       : 769508   (Deleted: 719799)
  Binary     : 17400    (Ratio:   2.26%)
  Ternary    : 4417     (Ratio:   0.57%)
  Conflict   : 769508   (Average Length:  469.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 769508   (Average: 20.82 Max: 1456 Sum: 16023834)
  Executed   : 769366   (Average: 20.81 Max: 1456 Sum: 16016186 Ratio:  99.95%)
  Bounded    : 142      (Average: 53.86 Max: 122 Sum:   7648 Ratio:   0.05%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 6932379  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

Iteration 97
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        : 98
Time         : 836.489s (Solving: 797.87s 1st Model: 0.01s Unsat: 12.29s)
CPU Time     : 836.692s

Choices      : 17691327 (Domain: 17431589)
Conflicts    : 778275   (Analyzed: 778271)
Restarts     : 9310     (Average: 83.60 Last: 191)
Model-Level  : 254.0   
Problems     : 98       (Average Length: 91.44 Splits: 0)
Lemmas       : 778271   (Deleted: 729623)
  Binary     : 17589    (Ratio:   2.26%)
  Ternary    : 4447     (Ratio:   0.57%)
  Conflict   : 778271   (Average Length:  469.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 778271   (Average: 20.76 Max: 1456 Sum: 16157004)
  Executed   : 778128   (Average: 20.75 Max: 1456 Sum: 16149234 Ratio:  99.95%)
  Bounded    : 143      (Average: 54.34 Max: 122 Sum:   7770 Ratio:   0.05%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 6932379  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

Iteration 98
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        : 99
Time         : 845.821s (Solving: 807.01s 1st Model: 0.01s Unsat: 12.29s)
CPU Time     : 846.028s

Choices      : 17782307 (Domain: 17522479)
Conflicts    : 786276   (Analyzed: 786272)
Restarts     : 9410     (Average: 83.56 Last: 191)
Model-Level  : 254.0   
Problems     : 99       (Average Length: 91.75 Splits: 0)
Lemmas       : 786272   (Deleted: 736243)
  Binary     : 17666    (Ratio:   2.25%)
  Ternary    : 4462     (Ratio:   0.57%)
  Conflict   : 786272   (Average Length:  469.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 786272   (Average: 20.64 Max: 1456 Sum: 16231550)
  Executed   : 786129   (Average: 20.63 Max: 1456 Sum: 16223780 Ratio:  99.95%)
  Bounded    : 143      (Average: 54.34 Max: 122 Sum:   7770 Ratio:   0.05%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 6932366  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

Iteration 99
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        : 100
Time         : 856.441s (Solving: 817.44s 1st Model: 0.01s Unsat: 12.29s)
CPU Time     : 856.652s

Choices      : 17955240 (Domain: 17695244)
Conflicts    : 794744   (Analyzed: 794740)
Restarts     : 9510     (Average: 83.57 Last: 191)
Model-Level  : 254.0   
Problems     : 100      (Average Length: 92.05 Splits: 0)
Lemmas       : 794740   (Deleted: 744000)
  Binary     : 17814    (Ratio:   2.24%)
  Ternary    : 4493     (Ratio:   0.57%)
  Conflict   : 794740   (Average Length:  469.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 794740   (Average: 20.62 Max: 1456 Sum: 16385032)
  Executed   : 794597   (Average: 20.61 Max: 1456 Sum: 16377262 Ratio:  99.95%)
  Bounded    : 143      (Average: 54.34 Max: 122 Sum:   7770 Ratio:   0.05%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 6932366  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

Iteration 100
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        : 101
Time         : 865.659s (Solving: 826.47s 1st Model: 0.01s Unsat: 12.29s)
CPU Time     : 865.876s

Choices      : 18127019 (Domain: 17866821)
Conflicts    : 803129   (Analyzed: 803125)
Restarts     : 9610     (Average: 83.57 Last: 191)
Model-Level  : 254.0   
Problems     : 101      (Average Length: 92.35 Splits: 0)
Lemmas       : 803125   (Deleted: 751967)
  Binary     : 17915    (Ratio:   2.23%)
  Ternary    : 4518     (Ratio:   0.56%)
  Conflict   : 803125   (Average Length:  469.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 803125   (Average: 20.59 Max: 1456 Sum: 16535251)
  Executed   : 802982   (Average: 20.58 Max: 1456 Sum: 16527481 Ratio:  99.95%)
  Bounded    : 143      (Average: 54.34 Max: 122 Sum:   7770 Ratio:   0.05%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 6932366  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

Iteration 101
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        : 102
Time         : 871.761s (Solving: 832.37s 1st Model: 0.01s Unsat: 12.29s)
CPU Time     : 871.980s

Choices      : 18163656 (Domain: 17903458)
Conflicts    : 810860   (Analyzed: 810856)
Restarts     : 9710     (Average: 83.51 Last: 191)
Model-Level  : 254.0   
Problems     : 102      (Average Length: 92.64 Splits: 0)
Lemmas       : 810856   (Deleted: 760191)
  Binary     : 17945    (Ratio:   2.21%)
  Ternary    : 4524     (Ratio:   0.56%)
  Conflict   : 810856   (Average Length:  468.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 810856   (Average: 20.43 Max: 1456 Sum: 16563240)
  Executed   : 810713   (Average: 20.42 Max: 1456 Sum: 16555470 Ratio:  99.95%)
  Bounded    : 143      (Average: 54.34 Max: 122 Sum:   7770 Ratio:   0.05%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 6932366  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

Iteration 102
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        : 103
Time         : 887.554s (Solving: 847.97s 1st Model: 0.01s Unsat: 12.29s)
CPU Time     : 887.776s

Choices      : 18241294 (Domain: 17981096)
Conflicts    : 819330   (Analyzed: 819326)
Restarts     : 9810     (Average: 83.52 Last: 191)
Model-Level  : 254.0   
Problems     : 103      (Average Length: 92.92 Splits: 0)
Lemmas       : 819326   (Deleted: 767691)
  Binary     : 17983    (Ratio:   2.19%)
  Ternary    : 4533     (Ratio:   0.55%)
  Conflict   : 819326   (Average Length:  481.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 819326   (Average: 20.29 Max: 1456 Sum: 16625112)
  Executed   : 819183   (Average: 20.28 Max: 1456 Sum: 16617342 Ratio:  99.95%)
  Bounded    : 143      (Average: 54.34 Max: 122 Sum:   7770 Ratio:   0.05%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 6932366  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

Iteration 103
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...
*** Info : (planner): INTERRUPTED by signal!
UNKNOWN

INTERRUPTED  : 1

Models       : 0+
Calls        : 104
Time         : 892.536s (Solving: 852.76s 1st Model: 0.01s Unsat: 12.29s)
CPU Time     : 892.740s

Choices      : 18282206 (Domain: 18022008)
Conflicts    : 825524   (Analyzed: 825520)
Restarts     : 9894     (Average: 83.44 Last: 191)
Model-Level  : 254.0   
Problems     : 104      (Average Length: 93.20 Splits: 0)
Lemmas       : 825520   (Deleted: 772098)
  Binary     : 17989    (Ratio:   2.18%)
  Ternary    : 4538     (Ratio:   0.55%)
  Conflict   : 825520   (Average Length:  480.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 825520   (Average: 20.18 Max: 1456 Sum: 16658548)
  Executed   : 825377   (Average: 20.17 Max: 1456 Sum: 16650778 Ratio:  99.95%)
  Bounded    : 143      (Average: 54.34 Max: 122 Sum:   7770 Ratio:   0.05%)

Rules        : 160595   (Original: 145100)
Atoms        : 77287   
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  : 6932366  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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


