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-15.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-15.pddl
Parsing...
Parsing: [0.030s CPU, 0.031s wall-clock]
Normalizing task... [0.000s CPU, 0.002s wall-clock]
Instantiating...
Generating Datalog program... [0.010s CPU, 0.008s wall-clock]
Normalizing Datalog program...
Normalizing Datalog program: [0.040s CPU, 0.041s wall-clock]
Preparing model... [0.030s CPU, 0.024s wall-clock]
Generated 115 rules.
Computing model... [0.500s CPU, 0.504s wall-clock]
3094 relevant atoms
3221 auxiliary atoms
6315 final queue length
10878 total queue pushes
Completing instantiation... [0.960s CPU, 0.962s wall-clock]
Instantiating: [1.550s CPU, 1.547s wall-clock]
Computing fact groups...
Finding invariants...
24 initial candidates
Finding invariants: [0.110s CPU, 0.112s wall-clock]
Checking invariant weight... [0.000s CPU, 0.001s wall-clock]
Instantiating groups... [0.010s CPU, 0.009s wall-clock]
Collecting mutex groups... [0.010s CPU, 0.001s wall-clock]
Choosing groups...
328 uncovered facts
Choosing groups: [0.000s CPU, 0.002s wall-clock]
Building translation key... [0.010s CPU, 0.012s wall-clock]
Computing fact groups: [0.160s CPU, 0.163s wall-clock]
Building STRIPS to SAS dictionary... [0.010s CPU, 0.003s wall-clock]
Building dictionary for full mutex groups... [0.000s CPU, 0.003s wall-clock]
Building mutex information...
Building mutex information: [0.000s CPU, 0.003s wall-clock]
Translating task...
Processing axioms...
Simplifying axioms... [0.000s CPU, 0.000s wall-clock]
Processing axioms: [0.050s CPU, 0.051s wall-clock]
Translating task: [1.000s CPU, 0.996s wall-clock]
3672 effect conditions simplified
0 implied preconditions added
Detecting unreachable propositions...
0 operators removed
0 axioms removed
3 propositions removed
Detecting unreachable propositions: [0.490s CPU, 0.490s wall-clock]
Reordering and filtering variables...
331 of 331 variables necessary.
15 of 18 mutex groups necessary.
2194 of 2194 operators necessary.
0 of 0 axiom rules necessary.
Reordering and filtering variables: [0.400s CPU, 0.401s wall-clock]
Translator variables: 331
Translator derived variables: 0
Translator facts: 691
Translator goal facts: 13
Translator mutex groups: 15
Translator total mutex groups size: 45
Translator operators: 2194
Translator axioms: 0
Translator task size: 21018
Translator peak memory: 48332 KB
Writing output... [0.400s CPU, 0.441s wall-clock]
Done! [4.080s CPU, 4.121s wall-clock]
planner.py version 0.0.1

Time:	 0.85s
Memory: 107MB

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

Models       : 0
Calls        : 1
Time         : 0.985s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
CPU Time     : 0.852s

Choices      : 0       
Conflicts    : 0        (Analyzed: 0)
Restarts     : 0       
Problems     : 1        (Average Length: 2.00 Splits: 0)
Lemmas       : 0        (Deleted: 0)
  Binary     : 0        (Ratio:   0.00%)
  Ternary    : 0        (Ratio:   0.00%)
  Conflict   : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 0        (Average:  0.00 Max:   0 Sum:      0)
  Executed   : 0        (Average:  0.00 Max:   0 Sum:      0 Ratio:   0.00%)
  Bounded    : 0        (Average:  0.00 Max:   0 Sum:      0 Ratio: 100.00%)

Rules        : 60629   
Atoms        : 60629   
Bodies       : 1        (Original: 0)
Tight        : Yes
Variables    : 0        (Eliminated:    0 Frozen:    0)
Constraints  : 0        (Binary:   0.0% Ternary:   0.0% Other:   0.0%)

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

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

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

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

Choices      : 328      (Domain: 271)
Conflicts    : 52       (Analyzed: 51)
Restarts     : 0       
Problems     : 2        (Average Length: 4.50 Splits: 0)
Lemmas       : 51       (Deleted: 0)
  Binary     : 20       (Ratio:  39.22%)
  Ternary    : 2        (Ratio:   3.92%)
  Conflict   : 51       (Average Length:    5.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 51       (Average:  6.47 Max:  37 Sum:    330)
  Executed   : 49       (Average:  6.43 Max:  37 Sum:    328 Ratio:  99.39%)
  Bounded    : 2        (Average:  1.00 Max:   1 Sum:      2 Ratio:   0.61%)

Rules        : 60629   
Atoms        : 60629   
Bodies       : 1        (Original: 0)
Tight        : Yes
Variables    : 16256    (Eliminated:    0 Frozen:  160)
Constraints  : 53667    (Binary:  95.3% Ternary:   3.3% Other:   1.4%)

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

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

Iteration 3
Queue:		 [(2,10,0,True), (3,15,0,True), (4,20,0,True), (5,25,0,True), (6,30,0,True)]
Grounded Until:	 5
Expected Memory: 187.0MB
Grounding...	 [('step', [6]), ('step', [7]), ('step', [8]), ('step', [9]), ('step', [10]), ('check', [10])]
Grounding Time:	 0.31s
Memory:		 190MB (+7MB)
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 1+
Calls        : 3
Time         : 1.924s (Solving: 0.08s 1st Model: 0.07s Unsat: 0.00s)
CPU Time     : 1.788s

Choices      : 2349     (Domain: 2154)
Conflicts    : 334      (Analyzed: 333)
Restarts     : 2        (Average: 166.50 Last: 62)
Model-Level  : 251.0   
Problems     : 3        (Average Length: 7.00 Splits: 0)
Lemmas       : 333      (Deleted: 0)
  Binary     : 70       (Ratio:  21.02%)
  Ternary    : 10       (Ratio:   3.00%)
  Conflict   : 333      (Average Length:  182.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 333      (Average:  6.20 Max: 132 Sum:   2065)
  Executed   : 331      (Average:  6.20 Max: 132 Sum:   2063 Ratio:  99.90%)
  Bounded    : 2        (Average:  1.00 Max:   1 Sum:      2 Ratio:   0.10%)

Rules        : 60629   
Atoms        : 60629   
Bodies       : 1        (Original: 0)
Tight        : Yes
Variables    : 35632    (Eliminated:    0 Frozen:  320)
Constraints  : 211962   (Binary:  95.6% Ternary:   3.2% Other:   1.2%)

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

[endof: stats after solve call]
Solving Time:	 0.09s
Memory:		 198MB (+8MB)
SAT
Testing...
NOT SERIALIZABLE
Testing Time:	 1.08s
Memory:		 232MB (+34MB)
Solving...
[start: stats after solve call]

Models       : 0
Calls        : 4
Time         : 2.542s (Solving: 0.36s 1st Model: 0.07s Unsat: 0.29s)
CPU Time     : 2.408s

Choices      : 9441     (Domain: 7693)
Conflicts    : 972      (Analyzed: 970)
Restarts     : 10       (Average: 97.00 Last: 62)
Model-Level  : 251.0   
Problems     : 4        (Average Length: 8.25 Splits: 0)
Lemmas       : 970      (Deleted: 0)
  Binary     : 215      (Ratio:  22.16%)
  Ternary    : 73       (Ratio:   7.53%)
  Conflict   : 970      (Average Length:   87.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 970      (Average:  9.43 Max: 132 Sum:   9151)
  Executed   : 963      (Average:  9.39 Max: 132 Sum:   9111 Ratio:  99.56%)
  Bounded    : 7        (Average:  5.71 Max:  12 Sum:     40 Ratio:   0.44%)

Rules        : 150286   (Original: 135821)
Atoms        : 72368   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 56254    (Eliminated:    0 Frozen: 15821)
Constraints  : 347145   (Binary:  91.4% Ternary:   7.0% Other:   1.7%)

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

[endof: stats after solve call]
Solving Time:	 0.37s
Memory:		 232MB (+0MB)
UNSAT
Iteration Time:	 1.99s

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

Models       : 0+
Calls        : 5
Time         : 7.321s (Solving: 4.40s 1st Model: 0.07s Unsat: 0.29s)
CPU Time     : 7.188s

Choices      : 103274   (Domain: 83893)
Conflicts    : 10049    (Analyzed: 10047)
Restarts     : 110      (Average: 91.34 Last: 82)
Model-Level  : 251.0   
Problems     : 5        (Average Length: 10.00 Splits: 0)
Lemmas       : 10047    (Deleted: 5861)
  Binary     : 934      (Ratio:   9.30%)
  Ternary    : 431      (Ratio:   4.29%)
  Conflict   : 10047    (Average Length:  173.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 10047    (Average:  9.91 Max: 328 Sum:  99516)
  Executed   : 10030    (Average:  9.88 Max: 328 Sum:  99309 Ratio:  99.79%)
  Bounded    : 17       (Average: 12.18 Max:  17 Sum:    207 Ratio:   0.21%)

Rules        : 150286   (Original: 135821)
Atoms        : 72368   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 93745    (Eliminated:    0 Frozen: 27481)
Constraints  : 624347   (Binary:  91.3% Ternary:   7.0% Other:   1.7%)

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

[endof: stats after solve call]
Solving Time:	 4.07s
Memory:		 257MB (+23MB)
UNKNOWN
Iteration Time:	 4.79s

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

Models       : 0+
Calls        : 6
Time         : 13.330s (Solving: 9.64s 1st Model: 0.07s Unsat: 0.29s)
CPU Time     : 13.196s

Choices      : 195626   (Domain: 161158)
Conflicts    : 18931    (Analyzed: 18929)
Restarts     : 210      (Average: 90.14 Last: 147)
Model-Level  : 251.0   
Problems     : 6        (Average Length: 12.00 Splits: 0)
Lemmas       : 18929    (Deleted: 13925)
  Binary     : 1451     (Ratio:   7.67%)
  Ternary    : 525      (Ratio:   2.77%)
  Conflict   : 18929    (Average Length:  627.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 18929    (Average:  9.70 Max: 328 Sum: 183697)
  Executed   : 18912    (Average:  9.69 Max: 328 Sum: 183490 Ratio:  99.89%)
  Bounded    : 17       (Average: 12.18 Max:  17 Sum:    207 Ratio:   0.11%)

Rules        : 150286   (Original: 135821)
Atoms        : 72368   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 131236   (Eliminated:    0 Frozen: 39141)
Constraints  : 896242   (Binary:  91.3% Ternary:   6.9% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 5.27s
Memory:		 276MB (+16MB)
UNKNOWN
Iteration Time:	 6.02s

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

Models       : 0+
Calls        : 7
Time         : 20.219s (Solving: 15.46s 1st Model: 0.07s Unsat: 0.29s)
CPU Time     : 20.088s

Choices      : 312221   (Domain: 262527)
Conflicts    : 27833    (Analyzed: 27831)
Restarts     : 310      (Average: 89.78 Last: 147)
Model-Level  : 251.0   
Problems     : 7        (Average Length: 14.14 Splits: 0)
Lemmas       : 27831    (Deleted: 22272)
  Binary     : 1738     (Ratio:   6.24%)
  Ternary    : 551      (Ratio:   1.98%)
  Conflict   : 27831    (Average Length:  876.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 27831    (Average: 10.39 Max: 328 Sum: 289195)
  Executed   : 27814    (Average: 10.38 Max: 328 Sum: 288988 Ratio:  99.93%)
  Bounded    : 17       (Average: 12.18 Max:  17 Sum:    207 Ratio:   0.07%)

Rules        : 150286   (Original: 135821)
Atoms        : 72368   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 168727   (Eliminated:    0 Frozen: 50801)
Constraints  : 1178702  (Binary:  91.3% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 8
Time         : 27.651s (Solving: 22.03s 1st Model: 0.07s Unsat: 0.29s)
CPU Time     : 27.524s

Choices      : 479799   (Domain: 417037)
Conflicts    : 37022    (Analyzed: 37020)
Restarts     : 410      (Average: 90.29 Last: 147)
Model-Level  : 251.0   
Problems     : 8        (Average Length: 16.38 Splits: 0)
Lemmas       : 37020    (Deleted: 30710)
  Binary     : 2027     (Ratio:   5.48%)
  Ternary    : 575      (Ratio:   1.55%)
  Conflict   : 37020    (Average Length:  983.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 37020    (Average: 12.01 Max: 328 Sum: 444719)
  Executed   : 37003    (Average: 12.01 Max: 328 Sum: 444512 Ratio:  99.95%)
  Bounded    : 17       (Average: 12.18 Max:  17 Sum:    207 Ratio:   0.05%)

Rules        : 150286   (Original: 135821)
Atoms        : 72368   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 206218   (Eliminated:    0 Frozen: 62461)
Constraints  : 1461162  (Binary:  91.3% Ternary:   7.0% Other:   1.8%)

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

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

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         : 33.602s (Solving: 27.92s 1st Model: 0.07s Unsat: 6.19s)
CPU Time     : 33.476s

Choices      : 572044   (Domain: 497302)
Conflicts    : 45447    (Analyzed: 45444)
Restarts     : 507      (Average: 89.63 Last: 147)
Model-Level  : 251.0   
Problems     : 9        (Average Length: 18.11 Splits: 0)
Lemmas       : 45444    (Deleted: 36473)
  Binary     : 2700     (Ratio:   5.94%)
  Ternary    : 694      (Ratio:   1.53%)
  Conflict   : 45444    (Average Length:  832.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 45444    (Average: 11.77 Max: 328 Sum: 534686)
  Executed   : 45406    (Average: 11.75 Max: 328 Sum: 533812 Ratio:  99.84%)
  Bounded    : 38       (Average: 23.00 Max:  32 Sum:    874 Ratio:   0.16%)

Rules        : 150286   (Original: 135821)
Atoms        : 72368   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 206218   (Eliminated:    0 Frozen: 62461)
Constraints  : 1461162  (Binary:  91.3% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 5.94s
Memory:		 351MB (+0MB)
UNSAT
Iteration Time:	 5.96s

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         : 40.287s (Solving: 34.56s 1st Model: 0.07s Unsat: 6.19s)
CPU Time     : 40.164s

Choices      : 683784   (Domain: 598350)
Conflicts    : 54404    (Analyzed: 54401)
Restarts     : 607      (Average: 89.62 Last: 147)
Model-Level  : 251.0   
Problems     : 10       (Average Length: 19.50 Splits: 0)
Lemmas       : 54401    (Deleted: 44132)
  Binary     : 3401     (Ratio:   6.25%)
  Ternary    : 902      (Ratio:   1.66%)
  Conflict   : 54401    (Average Length:  721.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 54401    (Average: 11.81 Max: 328 Sum: 642270)
  Executed   : 54339    (Average: 11.78 Max: 328 Sum: 640633 Ratio:  99.75%)
  Bounded    : 62       (Average: 26.40 Max:  32 Sum:   1637 Ratio:   0.25%)

Rules        : 150286   (Original: 135821)
Atoms        : 72368   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 206218   (Eliminated:    0 Frozen: 62461)
Constraints  : 1421811  (Binary:  91.3% Ternary:   6.9% Other:   1.8%)

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

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

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         : 46.293s (Solving: 40.52s 1st Model: 0.07s Unsat: 6.19s)
CPU Time     : 46.176s

Choices      : 781906   (Domain: 687551)
Conflicts    : 62886    (Analyzed: 62883)
Restarts     : 707      (Average: 88.94 Last: 147)
Model-Level  : 251.0   
Problems     : 11       (Average Length: 20.64 Splits: 0)
Lemmas       : 62883    (Deleted: 50567)
  Binary     : 3689     (Ratio:   5.87%)
  Ternary    : 961      (Ratio:   1.53%)
  Conflict   : 62883    (Average Length:  655.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 62883    (Average: 11.65 Max: 328 Sum: 732627)
  Executed   : 62808    (Average: 11.62 Max: 328 Sum: 730579 Ratio:  99.72%)
  Bounded    : 75       (Average: 27.31 Max:  32 Sum:   2048 Ratio:   0.28%)

Rules        : 150286   (Original: 135821)
Atoms        : 72368   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 206218   (Eliminated:    0 Frozen: 62461)
Constraints  : 1395626  (Binary:  91.3% Ternary:   6.9% Other:   1.8%)

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

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

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         : 52.276s (Solving: 46.46s 1st Model: 0.07s Unsat: 6.19s)
CPU Time     : 52.160s

Choices      : 909194   (Domain: 808893)
Conflicts    : 71442    (Analyzed: 71439)
Restarts     : 807      (Average: 88.52 Last: 147)
Model-Level  : 251.0   
Problems     : 12       (Average Length: 21.58 Splits: 0)
Lemmas       : 71439    (Deleted: 58311)
  Binary     : 4029     (Ratio:   5.64%)
  Ternary    : 1035     (Ratio:   1.45%)
  Conflict   : 71439    (Average Length:  611.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 71439    (Average: 11.91 Max: 335 Sum: 850558)
  Executed   : 71357    (Average: 11.87 Max: 335 Sum: 848286 Ratio:  99.73%)
  Bounded    : 82       (Average: 27.71 Max:  32 Sum:   2272 Ratio:   0.27%)

Rules        : 150286   (Original: 135821)
Atoms        : 72368   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 206218   (Eliminated:    0 Frozen: 62461)
Constraints  : 1395295  (Binary:  91.3% Ternary:   6.9% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 5.97s
Memory:		 351MB (+0MB)
UNKNOWN
Iteration Time:	 5.99s

Iteration 12
Queue:		 [(7,35,0,True), (8,40,0,True), (9,45,0,True), (10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True)]
Grounded Until:	 30
Expected Memory: 393.0MB
Grounding...	 [('step', [31]), ('step', [32]), ('step', [33]), ('step', [34]), ('step', [35]), ('check', [35])]
Grounding Time:	 0.56s
Memory:		 351MB (+0MB)
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 13
Time         : 60.308s (Solving: 53.58s 1st Model: 0.07s Unsat: 6.19s)
CPU Time     : 60.196s

Choices      : 1157175  (Domain: 1048177)
Conflicts    : 80479    (Analyzed: 80476)
Restarts     : 907      (Average: 88.73 Last: 156)
Model-Level  : 251.0   
Problems     : 13       (Average Length: 22.77 Splits: 0)
Lemmas       : 80476    (Deleted: 69453)
  Binary     : 4441     (Ratio:   5.52%)
  Ternary    : 1051     (Ratio:   1.31%)
  Conflict   : 80476    (Average Length:  617.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 80476    (Average: 13.49 Max: 335 Sum: 1085595)
  Executed   : 80394    (Average: 13.46 Max: 335 Sum: 1083323 Ratio:  99.79%)
  Bounded    : 82       (Average: 27.71 Max:  32 Sum:   2272 Ratio:   0.21%)

Rules        : 150286   (Original: 135821)
Atoms        : 72368   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 243709   (Eliminated:    0 Frozen: 74121)
Constraints  : 1672459  (Binary:  91.3% Ternary:   6.9% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 7.19s
Memory:		 365MB (+14MB)
UNKNOWN
Iteration Time:	 8.05s

Iteration 13
Queue:		 [(8,40,0,True), (9,45,0,True), (10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True)]
Grounded Until:	 35
Expected Memory: 407.0MB
Grounding...	 [('step', [36]), ('step', [37]), ('step', [38]), ('step', [39]), ('step', [40]), ('check', [40])]
Grounding Time:	 0.55s
Memory:		 373MB (+8MB)
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 14
Time         : 67.826s (Solving: 60.19s 1st Model: 0.07s Unsat: 6.19s)
CPU Time     : 67.716s

Choices      : 1371177  (Domain: 1254940)
Conflicts    : 89370    (Analyzed: 89367)
Restarts     : 1007     (Average: 88.75 Last: 156)
Model-Level  : 251.0   
Problems     : 14       (Average Length: 24.14 Splits: 0)
Lemmas       : 89367    (Deleted: 78148)
  Binary     : 4597     (Ratio:   5.14%)
  Ternary    : 1053     (Ratio:   1.18%)
  Conflict   : 89367    (Average Length:  640.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 89367    (Average: 14.37 Max: 335 Sum: 1283888)
  Executed   : 89285    (Average: 14.34 Max: 335 Sum: 1281616 Ratio:  99.82%)
  Bounded    : 82       (Average: 27.71 Max:  32 Sum:   2272 Ratio:   0.18%)

Rules        : 150286   (Original: 135821)
Atoms        : 72368   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 281200   (Eliminated:    0 Frozen: 85781)
Constraints  : 1954919  (Binary:  91.3% Ternary:   6.9% Other:   1.8%)

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

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

Iteration 14
Queue:		 [(9,45,0,True), (10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True)]
Grounded Until:	 40
Expected Memory: 430.0MB
Grounding...	 [('step', [41]), ('step', [42]), ('step', [43]), ('step', [44]), ('step', [45]), ('check', [45])]
Grounding Time:	 0.54s
Memory:		 398MB (+10MB)
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 15
Time         : 75.260s (Solving: 66.71s 1st Model: 0.07s Unsat: 6.19s)
CPU Time     : 75.152s

Choices      : 1571613  (Domain: 1449993)
Conflicts    : 97515    (Analyzed: 97512)
Restarts     : 1107     (Average: 88.09 Last: 156)
Model-Level  : 251.0   
Problems     : 15       (Average Length: 25.67 Splits: 0)
Lemmas       : 97512    (Deleted: 84548)
  Binary     : 4675     (Ratio:   4.79%)
  Ternary    : 1057     (Ratio:   1.08%)
  Conflict   : 97512    (Average Length:  667.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 97512    (Average: 15.04 Max: 396 Sum: 1466301)
  Executed   : 97430    (Average: 15.01 Max: 396 Sum: 1464029 Ratio:  99.85%)
  Bounded    : 82       (Average: 27.71 Max:  32 Sum:   2272 Ratio:   0.15%)

Rules        : 150286   (Original: 135821)
Atoms        : 72368   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 318691   (Eliminated:    0 Frozen: 97441)
Constraints  : 2237379  (Binary:  91.3% Ternary:   6.9% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 6.60s
Memory:		 443MB (+45MB)
UNKNOWN
Iteration Time:	 7.45s

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

Models       : 0+
Calls        : 16
Time         : 83.220s (Solving: 73.58s 1st Model: 0.07s Unsat: 6.19s)
CPU Time     : 83.116s

Choices      : 1827366  (Domain: 1699900)
Conflicts    : 106260   (Analyzed: 106257)
Restarts     : 1207     (Average: 88.03 Last: 156)
Model-Level  : 251.0   
Problems     : 16       (Average Length: 27.31 Splits: 0)
Lemmas       : 106257   (Deleted: 94747)
  Binary     : 4743     (Ratio:   4.46%)
  Ternary    : 1058     (Ratio:   1.00%)
  Conflict   : 106257   (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    : 106257   (Average: 16.03 Max: 415 Sum: 1703438)
  Executed   : 106175   (Average: 16.01 Max: 415 Sum: 1701166 Ratio:  99.87%)
  Bounded    : 82       (Average: 27.71 Max:  32 Sum:   2272 Ratio:   0.13%)

Rules        : 150286   (Original: 135821)
Atoms        : 72368   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 356182   (Eliminated:    0 Frozen: 109101)
Constraints  : 2519839  (Binary:  91.3% Ternary:   6.9% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 17
Time         : 91.545s (Solving: 80.96s 1st Model: 0.07s Unsat: 6.19s)
CPU Time     : 91.448s

Choices      : 2131193  (Domain: 1996576)
Conflicts    : 114823   (Analyzed: 114820)
Restarts     : 1307     (Average: 87.85 Last: 156)
Model-Level  : 251.0   
Problems     : 17       (Average Length: 29.06 Splits: 0)
Lemmas       : 114820   (Deleted: 100990)
  Binary     : 4792     (Ratio:   4.17%)
  Ternary    : 1059     (Ratio:   0.92%)
  Conflict   : 114820   (Average Length:  713.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 114820   (Average: 17.30 Max: 490 Sum: 1986954)
  Executed   : 114738   (Average: 17.29 Max: 490 Sum: 1984682 Ratio:  99.89%)
  Bounded    : 82       (Average: 27.71 Max:  32 Sum:   2272 Ratio:   0.11%)

Rules        : 150286   (Original: 135821)
Atoms        : 72368   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 393673   (Eliminated:    0 Frozen: 120761)
Constraints  : 2802299  (Binary:  91.3% Ternary:   6.9% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 7.47s
Memory:		 489MB (+19MB)
UNKNOWN
Iteration Time:	 8.34s

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

Models       : 0+
Calls        : 18
Time         : 99.920s (Solving: 88.38s 1st Model: 0.07s Unsat: 6.19s)
CPU Time     : 99.828s

Choices      : 2424475  (Domain: 2284371)
Conflicts    : 123053   (Analyzed: 123050)
Restarts     : 1407     (Average: 87.46 Last: 156)
Model-Level  : 251.0   
Problems     : 18       (Average Length: 30.89 Splits: 0)
Lemmas       : 123050   (Deleted: 109356)
  Binary     : 4830     (Ratio:   3.93%)
  Ternary    : 1060     (Ratio:   0.86%)
  Conflict   : 123050   (Average Length:  740.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 123050   (Average: 18.35 Max: 543 Sum: 2257534)
  Executed   : 122968   (Average: 18.33 Max: 543 Sum: 2255262 Ratio:  99.90%)
  Bounded    : 82       (Average: 27.71 Max:  32 Sum:   2272 Ratio:   0.10%)

Rules        : 150286   (Original: 135821)
Atoms        : 72368   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 431164   (Eliminated:    0 Frozen: 132421)
Constraints  : 3084759  (Binary:  91.2% Ternary:   6.9% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 7.51s
Memory:		 552MB (+58MB)
UNKNOWN
Iteration Time:	 8.39s

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

Models       : 0+
Calls        : 19
Time         : 108.976s (Solving: 96.44s 1st Model: 0.07s Unsat: 6.19s)
CPU Time     : 108.888s

Choices      : 2742954  (Domain: 2597685)
Conflicts    : 131174   (Analyzed: 131171)
Restarts     : 1507     (Average: 87.04 Last: 156)
Model-Level  : 251.0   
Problems     : 19       (Average Length: 32.79 Splits: 0)
Lemmas       : 131171   (Deleted: 117422)
  Binary     : 4855     (Ratio:   3.70%)
  Ternary    : 1062     (Ratio:   0.81%)
  Conflict   : 131171   (Average Length:  764.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 131171   (Average: 19.46 Max: 581 Sum: 2552228)
  Executed   : 131089   (Average: 19.44 Max: 581 Sum: 2549956 Ratio:  99.91%)
  Bounded    : 82       (Average: 27.71 Max:  32 Sum:   2272 Ratio:   0.09%)

Rules        : 150286   (Original: 135821)
Atoms        : 72368   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 468655   (Eliminated:    0 Frozen: 144081)
Constraints  : 3367219  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 20
Time         : 118.280s (Solving: 104.72s 1st Model: 0.07s Unsat: 6.19s)
CPU Time     : 118.196s

Choices      : 3075555  (Domain: 2925291)
Conflicts    : 139318   (Analyzed: 139315)
Restarts     : 1607     (Average: 86.69 Last: 156)
Model-Level  : 251.0   
Problems     : 20       (Average Length: 34.75 Splits: 0)
Lemmas       : 139315   (Deleted: 125364)
  Binary     : 4891     (Ratio:   3.51%)
  Ternary    : 1064     (Ratio:   0.76%)
  Conflict   : 139315   (Average Length:  786.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 139315   (Average: 20.53 Max: 627 Sum: 2860030)
  Executed   : 139233   (Average: 20.51 Max: 627 Sum: 2857758 Ratio:  99.92%)
  Bounded    : 82       (Average: 27.71 Max:  32 Sum:   2272 Ratio:   0.08%)

Rules        : 150286   (Original: 135821)
Atoms        : 72368   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 506146   (Eliminated:    0 Frozen: 155741)
Constraints  : 3649679  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 8.39s
Memory:		 583MB (+21MB)
UNKNOWN
Iteration Time:	 9.32s

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

Models       : 0+
Calls        : 21
Time         : 127.830s (Solving: 113.25s 1st Model: 0.07s Unsat: 6.19s)
CPU Time     : 127.752s

Choices      : 3463794  (Domain: 3308410)
Conflicts    : 147563   (Analyzed: 147560)
Restarts     : 1707     (Average: 86.44 Last: 156)
Model-Level  : 251.0   
Problems     : 21       (Average Length: 36.76 Splits: 0)
Lemmas       : 147560   (Deleted: 133359)
  Binary     : 4921     (Ratio:   3.33%)
  Ternary    : 1064     (Ratio:   0.72%)
  Conflict   : 147560   (Average Length:  801.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 147560   (Average: 21.84 Max: 682 Sum: 3222187)
  Executed   : 147478   (Average: 21.82 Max: 682 Sum: 3219915 Ratio:  99.93%)
  Bounded    : 82       (Average: 27.71 Max:  32 Sum:   2272 Ratio:   0.07%)

Rules        : 150286   (Original: 135821)
Atoms        : 72368   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 543637   (Eliminated:    0 Frozen: 167401)
Constraints  : 3932139  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 22
Time         : 137.655s (Solving: 122.02s 1st Model: 0.07s Unsat: 6.19s)
CPU Time     : 137.584s

Choices      : 3861148  (Domain: 3700237)
Conflicts    : 155896   (Analyzed: 155893)
Restarts     : 1807     (Average: 86.27 Last: 156)
Model-Level  : 251.0   
Problems     : 22       (Average Length: 38.82 Splits: 0)
Lemmas       : 155893   (Deleted: 141480)
  Binary     : 4942     (Ratio:   3.17%)
  Ternary    : 1065     (Ratio:   0.68%)
  Conflict   : 155893   (Average Length:  818.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 155893   (Average: 23.04 Max: 732 Sum: 3592289)
  Executed   : 155811   (Average: 23.03 Max: 732 Sum: 3590017 Ratio:  99.94%)
  Bounded    : 82       (Average: 27.71 Max:  32 Sum:   2272 Ratio:   0.06%)

Rules        : 150286   (Original: 135821)
Atoms        : 72368   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 581128   (Eliminated:    0 Frozen: 179061)
Constraints  : 4214599  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 8.89s
Memory:		 633MB (+24MB)
UNKNOWN
Iteration Time:	 9.84s

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

Models       : 0+
Calls        : 23
Time         : 143.128s (Solving: 127.37s 1st Model: 0.07s Unsat: 6.19s)
CPU Time     : 143.056s

Choices      : 3944840  (Domain: 3778004)
Conflicts    : 164803   (Analyzed: 164800)
Restarts     : 1907     (Average: 86.42 Last: 156)
Model-Level  : 251.0   
Problems     : 23       (Average Length: 40.70 Splits: 0)
Lemmas       : 164800   (Deleted: 149207)
  Binary     : 5344     (Ratio:   3.24%)
  Ternary    : 1201     (Ratio:   0.73%)
  Conflict   : 164800   (Average Length:  790.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 164800   (Average: 22.26 Max: 732 Sum: 3667764)
  Executed   : 164713   (Average: 22.24 Max: 732 Sum: 3665082 Ratio:  99.93%)
  Bounded    : 87       (Average: 30.83 Max:  82 Sum:   2682 Ratio:   0.07%)

Rules        : 150286   (Original: 135821)
Atoms        : 72368   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 581128   (Eliminated:    0 Frozen: 179061)
Constraints  : 4214599  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 24
Time         : 151.500s (Solving: 135.62s 1st Model: 0.07s Unsat: 6.19s)
CPU Time     : 151.432s

Choices      : 4073315  (Domain: 3899978)
Conflicts    : 174025   (Analyzed: 174022)
Restarts     : 2007     (Average: 86.71 Last: 156)
Model-Level  : 251.0   
Problems     : 24       (Average Length: 42.42 Splits: 0)
Lemmas       : 174022   (Deleted: 157070)
  Binary     : 5843     (Ratio:   3.36%)
  Ternary    : 1372     (Ratio:   0.79%)
  Conflict   : 174022   (Average Length:  762.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 174022   (Average: 21.76 Max: 732 Sum: 3786698)
  Executed   : 173930   (Average: 21.74 Max: 732 Sum: 3783606 Ratio:  99.92%)
  Bounded    : 92       (Average: 33.61 Max:  82 Sum:   3092 Ratio:   0.08%)

Rules        : 150286   (Original: 135821)
Atoms        : 72368   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 581128   (Eliminated:    0 Frozen: 179061)
Constraints  : 4214529  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 8.33s
Memory:		 633MB (+0MB)
UNKNOWN
Iteration Time:	 8.38s

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

Models       : 0+
Calls        : 25
Time         : 160.748s (Solving: 144.71s 1st Model: 0.07s Unsat: 6.19s)
CPU Time     : 160.684s

Choices      : 4206834  (Domain: 4026174)
Conflicts    : 183158   (Analyzed: 183155)
Restarts     : 2107     (Average: 86.93 Last: 156)
Model-Level  : 251.0   
Problems     : 25       (Average Length: 44.00 Splits: 0)
Lemmas       : 183155   (Deleted: 165457)
  Binary     : 6112     (Ratio:   3.34%)
  Ternary    : 1447     (Ratio:   0.79%)
  Conflict   : 183155   (Average Length:  742.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 183155   (Average: 21.34 Max: 732 Sum: 3909028)
  Executed   : 183061   (Average: 21.32 Max: 732 Sum: 3905772 Ratio:  99.92%)
  Bounded    : 94       (Average: 34.64 Max:  82 Sum:   3256 Ratio:   0.08%)

Rules        : 150286   (Original: 135821)
Atoms        : 72368   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 581128   (Eliminated:    0 Frozen: 179061)
Constraints  : 4214460  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 9.20s
Memory:		 633MB (+0MB)
UNKNOWN
Iteration Time:	 9.26s

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

Models       : 0+
Calls        : 26
Time         : 169.942s (Solving: 153.78s 1st Model: 0.07s Unsat: 6.19s)
CPU Time     : 169.884s

Choices      : 4339020  (Domain: 4152862)
Conflicts    : 192009   (Analyzed: 192006)
Restarts     : 2207     (Average: 87.00 Last: 156)
Model-Level  : 251.0   
Problems     : 26       (Average Length: 45.46 Splits: 0)
Lemmas       : 192006   (Deleted: 174050)
  Binary     : 6269     (Ratio:   3.27%)
  Ternary    : 1477     (Ratio:   0.77%)
  Conflict   : 192006   (Average Length:  724.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 192006   (Average: 20.98 Max: 732 Sum: 4028203)
  Executed   : 191909   (Average: 20.96 Max: 732 Sum: 4024701 Ratio:  99.91%)
  Bounded    : 97       (Average: 36.10 Max:  82 Sum:   3502 Ratio:   0.09%)

Rules        : 150286   (Original: 135821)
Atoms        : 72368   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 581128   (Eliminated:    0 Frozen: 179061)
Constraints  : 4214421  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 27
Time         : 178.563s (Solving: 162.28s 1st Model: 0.07s Unsat: 6.19s)
CPU Time     : 178.508s

Choices      : 4483150  (Domain: 4294988)
Conflicts    : 200250   (Analyzed: 200247)
Restarts     : 2307     (Average: 86.80 Last: 156)
Model-Level  : 251.0   
Problems     : 27       (Average Length: 46.81 Splits: 0)
Lemmas       : 200247   (Deleted: 180348)
  Binary     : 6424     (Ratio:   3.21%)
  Ternary    : 1518     (Ratio:   0.76%)
  Conflict   : 200247   (Average Length:  706.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 200247   (Average: 20.79 Max: 732 Sum: 4162747)
  Executed   : 200150   (Average: 20.77 Max: 732 Sum: 4159245 Ratio:  99.92%)
  Bounded    : 97       (Average: 36.10 Max:  82 Sum:   3502 Ratio:   0.08%)

Rules        : 150286   (Original: 135821)
Atoms        : 72368   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 581128   (Eliminated:    0 Frozen: 179061)
Constraints  : 4214383  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 8.58s
Memory:		 633MB (+0MB)
UNKNOWN
Iteration Time:	 8.63s

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

Models       : 0+
Calls        : 28
Time         : 188.806s (Solving: 172.39s 1st Model: 0.07s Unsat: 6.19s)
CPU Time     : 188.756s

Choices      : 4710857  (Domain: 4518979)
Conflicts    : 209443   (Analyzed: 209440)
Restarts     : 2407     (Average: 87.01 Last: 156)
Model-Level  : 251.0   
Problems     : 28       (Average Length: 48.07 Splits: 0)
Lemmas       : 209440   (Deleted: 190144)
  Binary     : 6772     (Ratio:   3.23%)
  Ternary    : 1671     (Ratio:   0.80%)
  Conflict   : 209440   (Average Length:  690.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 209440   (Average: 20.90 Max: 732 Sum: 4377404)
  Executed   : 209340   (Average: 20.88 Max: 732 Sum: 4373661 Ratio:  99.91%)
  Bounded    : 100      (Average: 37.43 Max:  82 Sum:   3743 Ratio:   0.09%)

Rules        : 150286   (Original: 135821)
Atoms        : 72368   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 581128   (Eliminated:    0 Frozen: 179061)
Constraints  : 4214383  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 29
Time         : 198.772s (Solving: 182.24s 1st Model: 0.07s Unsat: 6.19s)
CPU Time     : 198.724s

Choices      : 4942110  (Domain: 4746373)
Conflicts    : 218428   (Analyzed: 218425)
Restarts     : 2507     (Average: 87.13 Last: 156)
Model-Level  : 251.0   
Problems     : 29       (Average Length: 49.24 Splits: 0)
Lemmas       : 218425   (Deleted: 198382)
  Binary     : 7052     (Ratio:   3.23%)
  Ternary    : 1758     (Ratio:   0.80%)
  Conflict   : 218425   (Average Length:  672.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 218425   (Average: 21.04 Max: 732 Sum: 4594966)
  Executed   : 218324   (Average: 21.02 Max: 732 Sum: 4591141 Ratio:  99.92%)
  Bounded    : 101      (Average: 37.87 Max:  82 Sum:   3825 Ratio:   0.08%)

Rules        : 150286   (Original: 135821)
Atoms        : 72368   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 581128   (Eliminated:    0 Frozen: 179061)
Constraints  : 4214355  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 30
Time         : 213.776s (Solving: 197.13s 1st Model: 0.07s Unsat: 6.19s)
CPU Time     : 213.736s

Choices      : 5543602  (Domain: 5335717)
Conflicts    : 228019   (Analyzed: 228016)
Restarts     : 2607     (Average: 87.46 Last: 156)
Model-Level  : 251.0   
Problems     : 30       (Average Length: 50.33 Splits: 0)
Lemmas       : 228016   (Deleted: 206371)
  Binary     : 7863     (Ratio:   3.45%)
  Ternary    : 1962     (Ratio:   0.86%)
  Conflict   : 228016   (Average Length:  655.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 228016   (Average: 22.71 Max: 732 Sum: 5177436)
  Executed   : 227915   (Average: 22.69 Max: 732 Sum: 5173611 Ratio:  99.93%)
  Bounded    : 101      (Average: 37.87 Max:  82 Sum:   3825 Ratio:   0.07%)

Rules        : 150286   (Original: 135821)
Atoms        : 72368   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 581128   (Eliminated:    0 Frozen: 179061)
Constraints  : 4214341  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 14.97s
Memory:		 633MB (+0MB)
UNKNOWN
Iteration Time:	 15.01s

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

Models       : 0+
Calls        : 31
Time         : 230.104s (Solving: 213.33s 1st Model: 0.07s Unsat: 6.19s)
CPU Time     : 230.072s

Choices      : 5912692  (Domain: 5701705)
Conflicts    : 237089   (Analyzed: 237086)
Restarts     : 2707     (Average: 87.58 Last: 156)
Model-Level  : 251.0   
Problems     : 31       (Average Length: 51.35 Splits: 0)
Lemmas       : 237086   (Deleted: 214344)
  Binary     : 8345     (Ratio:   3.52%)
  Ternary    : 2067     (Ratio:   0.87%)
  Conflict   : 237086   (Average Length:  642.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 237086   (Average: 23.32 Max: 732 Sum: 5529510)
  Executed   : 236985   (Average: 23.31 Max: 732 Sum: 5525685 Ratio:  99.93%)
  Bounded    : 101      (Average: 37.87 Max:  82 Sum:   3825 Ratio:   0.07%)

Rules        : 150286   (Original: 135821)
Atoms        : 72368   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 581128   (Eliminated:    0 Frozen: 179061)
Constraints  : 4214341  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 16.29s
Memory:		 633MB (+0MB)
UNKNOWN
Iteration Time:	 16.34s

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

Models       : 0+
Calls        : 32
Time         : 247.661s (Solving: 230.77s 1st Model: 0.07s Unsat: 6.19s)
CPU Time     : 247.640s

Choices      : 6355466  (Domain: 6140328)
Conflicts    : 246112   (Analyzed: 246109)
Restarts     : 2807     (Average: 87.68 Last: 156)
Model-Level  : 251.0   
Problems     : 32       (Average Length: 52.31 Splits: 0)
Lemmas       : 246109   (Deleted: 222644)
  Binary     : 8751     (Ratio:   3.56%)
  Ternary    : 2149     (Ratio:   0.87%)
  Conflict   : 246109   (Average Length:  631.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 246109   (Average: 24.18 Max: 732 Sum: 5951293)
  Executed   : 246008   (Average: 24.17 Max: 732 Sum: 5947468 Ratio:  99.94%)
  Bounded    : 101      (Average: 37.87 Max:  82 Sum:   3825 Ratio:   0.06%)

Rules        : 150286   (Original: 135821)
Atoms        : 72368   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 581128   (Eliminated:    0 Frozen: 179061)
Constraints  : 4214341  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 17.53s
Memory:		 633MB (+0MB)
UNKNOWN
Iteration Time:	 17.57s

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

Models       : 0+
Calls        : 33
Time         : 262.904s (Solving: 245.88s 1st Model: 0.07s Unsat: 6.19s)
CPU Time     : 262.888s

Choices      : 6768299  (Domain: 6550555)
Conflicts    : 254644   (Analyzed: 254641)
Restarts     : 2907     (Average: 87.60 Last: 156)
Model-Level  : 251.0   
Problems     : 33       (Average Length: 53.21 Splits: 0)
Lemmas       : 254641   (Deleted: 228922)
  Binary     : 9085     (Ratio:   3.57%)
  Ternary    : 2205     (Ratio:   0.87%)
  Conflict   : 254641   (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    : 254641   (Average: 24.91 Max: 781 Sum: 6342905)
  Executed   : 254540   (Average: 24.89 Max: 781 Sum: 6339080 Ratio:  99.94%)
  Bounded    : 101      (Average: 37.87 Max:  82 Sum:   3825 Ratio:   0.06%)

Rules        : 150286   (Original: 135821)
Atoms        : 72368   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 581128   (Eliminated:    0 Frozen: 179061)
Constraints  : 4214341  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 15.20s
Memory:		 633MB (+0MB)
UNKNOWN
Iteration Time:	 15.25s

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

Models       : 0+
Calls        : 34
Time         : 277.295s (Solving: 260.16s 1st Model: 0.07s Unsat: 6.19s)
CPU Time     : 277.284s

Choices      : 7147633  (Domain: 6925074)
Conflicts    : 263491   (Analyzed: 263488)
Restarts     : 3007     (Average: 87.62 Last: 156)
Model-Level  : 251.0   
Problems     : 34       (Average Length: 54.06 Splits: 0)
Lemmas       : 263488   (Deleted: 238764)
  Binary     : 9400     (Ratio:   3.57%)
  Ternary    : 2238     (Ratio:   0.85%)
  Conflict   : 263488   (Average Length:  640.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 263488   (Average: 25.39 Max: 781 Sum: 6690109)
  Executed   : 263387   (Average: 25.38 Max: 781 Sum: 6686284 Ratio:  99.94%)
  Bounded    : 101      (Average: 37.87 Max:  82 Sum:   3825 Ratio:   0.06%)

Rules        : 150286   (Original: 135821)
Atoms        : 72368   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 581128   (Eliminated:    0 Frozen: 179061)
Constraints  : 4214341  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 14.36s
Memory:		 697MB (+64MB)
UNKNOWN
Iteration Time:	 14.40s

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

Models       : 0+
Calls        : 35
Time         : 288.086s (Solving: 270.81s 1st Model: 0.07s Unsat: 6.19s)
CPU Time     : 288.076s

Choices      : 7331654  (Domain: 7108520)
Conflicts    : 271441   (Analyzed: 271438)
Restarts     : 3107     (Average: 87.36 Last: 156)
Model-Level  : 251.0   
Problems     : 35       (Average Length: 54.86 Splits: 0)
Lemmas       : 271438   (Deleted: 245100)
  Binary     : 9510     (Ratio:   3.50%)
  Ternary    : 2261     (Ratio:   0.83%)
  Conflict   : 271438   (Average Length:  628.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 271438   (Average: 25.28 Max: 781 Sum: 6860706)
  Executed   : 271336   (Average: 25.26 Max: 781 Sum: 6856799 Ratio:  99.94%)
  Bounded    : 102      (Average: 38.30 Max:  82 Sum:   3907 Ratio:   0.06%)

Rules        : 150286   (Original: 135821)
Atoms        : 72368   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 581128   (Eliminated:    0 Frozen: 179061)
Constraints  : 4214341  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 10.74s
Memory:		 697MB (+0MB)
UNKNOWN
Iteration Time:	 10.80s

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

Models       : 0+
Calls        : 36
Time         : 304.557s (Solving: 286.20s 1st Model: 0.07s Unsat: 6.19s)
CPU Time     : 304.556s

Choices      : 7852212  (Domain: 7625348)
Conflicts    : 281214   (Analyzed: 281211)
Restarts     : 3207     (Average: 87.69 Last: 156)
Model-Level  : 251.0   
Problems     : 36       (Average Length: 55.75 Splits: 0)
Lemmas       : 281211   (Deleted: 255259)
  Binary     : 9793     (Ratio:   3.48%)
  Ternary    : 2331     (Ratio:   0.83%)
  Conflict   : 281211   (Average Length:  630.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 281211   (Average: 26.14 Max: 859 Sum: 7351427)
  Executed   : 281109   (Average: 26.13 Max: 859 Sum: 7347520 Ratio:  99.95%)
  Bounded    : 102      (Average: 38.30 Max:  82 Sum:   3907 Ratio:   0.05%)

Rules        : 150286   (Original: 135821)
Atoms        : 72368   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 618619   (Eliminated:    0 Frozen: 190721)
Constraints  : 4496787  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 15.52s
Memory:		 719MB (+22MB)
UNKNOWN
Iteration Time:	 16.49s

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

Models       : 0+
Calls        : 37
Time         : 319.373s (Solving: 299.88s 1st Model: 0.07s Unsat: 6.19s)
CPU Time     : 319.376s

Choices      : 8188396  (Domain: 7959985)
Conflicts    : 289503   (Analyzed: 289500)
Restarts     : 3307     (Average: 87.54 Last: 156)
Model-Level  : 251.0   
Problems     : 37       (Average Length: 56.73 Splits: 0)
Lemmas       : 289500   (Deleted: 263146)
  Binary     : 9950     (Ratio:   3.44%)
  Ternary    : 2354     (Ratio:   0.81%)
  Conflict   : 289500   (Average Length:  641.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 289500   (Average: 26.44 Max: 886 Sum: 7653554)
  Executed   : 289398   (Average: 26.42 Max: 886 Sum: 7649647 Ratio:  99.95%)
  Bounded    : 102      (Average: 38.30 Max:  82 Sum:   3907 Ratio:   0.05%)

Rules        : 150286   (Original: 135821)
Atoms        : 72368   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 656110   (Eliminated:    0 Frozen: 202381)
Constraints  : 4779247  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 13.81s
Memory:		 799MB (+80MB)
UNKNOWN
Iteration Time:	 14.83s

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

Models       : 0+
Calls        : 38
Time         : 333.411s (Solving: 312.75s 1st Model: 0.07s Unsat: 6.19s)
CPU Time     : 333.420s

Choices      : 8440963  (Domain: 8211293)
Conflicts    : 297935   (Analyzed: 297932)
Restarts     : 3407     (Average: 87.45 Last: 156)
Model-Level  : 251.0   
Problems     : 38       (Average Length: 57.79 Splits: 0)
Lemmas       : 297932   (Deleted: 271843)
  Binary     : 10074    (Ratio:   3.38%)
  Ternary    : 2387     (Ratio:   0.80%)
  Conflict   : 297932   (Average Length:  655.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 297932   (Average: 26.42 Max: 1023 Sum: 7872147)
  Executed   : 297830   (Average: 26.41 Max: 1023 Sum: 7868240 Ratio:  99.95%)
  Bounded    : 102      (Average: 38.30 Max:  82 Sum:   3907 Ratio:   0.05%)

Rules        : 150286   (Original: 135821)
Atoms        : 72368   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 693601   (Eliminated:    0 Frozen: 214041)
Constraints  : 5061707  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 13.01s
Memory:		 803MB (+4MB)
UNKNOWN
Iteration Time:	 14.05s

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

Models       : 0+
Calls        : 39
Time         : 347.630s (Solving: 325.49s 1st Model: 0.07s Unsat: 6.19s)
CPU Time     : 347.644s

Choices      : 8659704  (Domain: 8429461)
Conflicts    : 306292   (Analyzed: 306289)
Restarts     : 3507     (Average: 87.34 Last: 156)
Model-Level  : 251.0   
Problems     : 39       (Average Length: 58.92 Splits: 0)
Lemmas       : 306289   (Deleted: 280030)
  Binary     : 10188    (Ratio:   3.33%)
  Ternary    : 2407     (Ratio:   0.79%)
  Conflict   : 306289   (Average Length:  666.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 306289   (Average: 26.30 Max: 1023 Sum: 8055366)
  Executed   : 306187   (Average: 26.29 Max: 1023 Sum: 8051459 Ratio:  99.95%)
  Bounded    : 102      (Average: 38.30 Max:  82 Sum:   3907 Ratio:   0.05%)

Rules        : 150286   (Original: 135821)
Atoms        : 72368   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 731092   (Eliminated:    0 Frozen: 225701)
Constraints  : 5344167  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 12.87s
Memory:		 858MB (+4MB)
UNKNOWN
Iteration Time:	 14.24s

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

Models       : 0+
Calls        : 40
Time         : 359.992s (Solving: 336.71s 1st Model: 0.07s Unsat: 6.19s)
CPU Time     : 360.012s

Choices      : 8821634  (Domain: 8591315)
Conflicts    : 314575   (Analyzed: 314572)
Restarts     : 3607     (Average: 87.21 Last: 156)
Model-Level  : 251.0   
Problems     : 40       (Average Length: 60.12 Splits: 0)
Lemmas       : 314572   (Deleted: 288205)
  Binary     : 10258    (Ratio:   3.26%)
  Ternary    : 2414     (Ratio:   0.77%)
  Conflict   : 314572   (Average Length:  681.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 314572   (Average: 26.01 Max: 1023 Sum: 8181575)
  Executed   : 314470   (Average: 26.00 Max: 1023 Sum: 8177668 Ratio:  99.95%)
  Bounded    : 102      (Average: 38.30 Max:  82 Sum:   3907 Ratio:   0.05%)

Rules        : 150286   (Original: 135821)
Atoms        : 72368   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 768583   (Eliminated:    0 Frozen: 237361)
Constraints  : 5626627  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 11.37s
Memory:		 868MB (+10MB)
UNKNOWN
Iteration Time:	 12.38s

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

Models       : 0
Calls        : 41
Time         : 365.716s (Solving: 342.26s 1st Model: 0.07s Unsat: 11.73s)
CPU Time     : 365.740s

Choices      : 8873173  (Domain: 8642854)
Conflicts    : 319882   (Analyzed: 319878)
Restarts     : 3672     (Average: 87.11 Last: 156)
Model-Level  : 251.0   
Problems     : 41       (Average Length: 61.27 Splits: 0)
Lemmas       : 319878   (Deleted: 293629)
  Binary     : 10410    (Ratio:   3.25%)
  Ternary    : 2446     (Ratio:   0.76%)
  Conflict   : 319878   (Average Length:  675.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 319878   (Average: 25.73 Max: 1023 Sum: 8232011)
  Executed   : 319768   (Average: 25.72 Max: 1023 Sum: 8227990 Ratio:  99.95%)
  Bounded    : 110      (Average: 36.55 Max: 107 Sum:   4021 Ratio:   0.05%)

Rules        : 150286   (Original: 135821)
Atoms        : 72368   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 768583   (Eliminated:    0 Frozen: 237361)
Constraints  : 5626627  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 5.66s
Memory:		 872MB (+4MB)
UNSAT
Iteration Time:	 5.73s

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

Models       : 0+
Calls        : 42
Time         : 370.558s (Solving: 346.95s 1st Model: 0.07s Unsat: 11.73s)
CPU Time     : 370.580s

Choices      : 8920227  (Domain: 8689908)
Conflicts    : 327253   (Analyzed: 327249)
Restarts     : 3772     (Average: 86.76 Last: 156)
Model-Level  : 251.0   
Problems     : 42       (Average Length: 62.36 Splits: 0)
Lemmas       : 327249   (Deleted: 298682)
  Binary     : 10504    (Ratio:   3.21%)
  Ternary    : 2480     (Ratio:   0.76%)
  Conflict   : 327249   (Average Length:  667.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 327249   (Average: 25.28 Max: 1023 Sum: 8272642)
  Executed   : 327137   (Average: 25.27 Max: 1023 Sum: 8268407 Ratio:  99.95%)
  Bounded    : 112      (Average: 37.81 Max: 107 Sum:   4235 Ratio:   0.05%)

Rules        : 150286   (Original: 135821)
Atoms        : 72368   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 768583   (Eliminated:    0 Frozen: 237361)
Constraints  : 5626613  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 43
Time         : 376.030s (Solving: 352.27s 1st Model: 0.07s Unsat: 11.73s)
CPU Time     : 376.056s

Choices      : 8957184  (Domain: 8726865)
Conflicts    : 335518   (Analyzed: 335514)
Restarts     : 3872     (Average: 86.65 Last: 156)
Model-Level  : 251.0   
Problems     : 43       (Average Length: 63.40 Splits: 0)
Lemmas       : 335514   (Deleted: 305695)
  Binary     : 10555    (Ratio:   3.15%)
  Ternary    : 2501     (Ratio:   0.75%)
  Conflict   : 335514   (Average Length:  657.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 335514   (Average: 24.75 Max: 1023 Sum: 8302817)
  Executed   : 335399   (Average: 24.73 Max: 1023 Sum: 8298267 Ratio:  99.95%)
  Bounded    : 115      (Average: 39.57 Max: 107 Sum:   4550 Ratio:   0.05%)

Rules        : 150286   (Original: 135821)
Atoms        : 72368   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 768583   (Eliminated:    0 Frozen: 237361)
Constraints  : 5626573  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 44
Time         : 382.072s (Solving: 358.13s 1st Model: 0.07s Unsat: 11.73s)
CPU Time     : 382.100s

Choices      : 9012585  (Domain: 8781888)
Conflicts    : 343292   (Analyzed: 343288)
Restarts     : 3972     (Average: 86.43 Last: 156)
Model-Level  : 251.0   
Problems     : 44       (Average Length: 64.39 Splits: 0)
Lemmas       : 343288   (Deleted: 313547)
  Binary     : 10635    (Ratio:   3.10%)
  Ternary    : 2523     (Ratio:   0.73%)
  Conflict   : 343288   (Average Length:  649.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 343288   (Average: 24.33 Max: 1023 Sum: 8350864)
  Executed   : 343171   (Average: 24.31 Max: 1023 Sum: 8346105 Ratio:  99.94%)
  Bounded    : 117      (Average: 40.68 Max: 107 Sum:   4759 Ratio:   0.06%)

Rules        : 150286   (Original: 135821)
Atoms        : 72368   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 768583   (Eliminated:    0 Frozen: 237361)
Constraints  : 5626545  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 45
Time         : 389.462s (Solving: 365.37s 1st Model: 0.07s Unsat: 11.73s)
CPU Time     : 389.492s

Choices      : 9099779  (Domain: 8867922)
Conflicts    : 351879   (Analyzed: 351875)
Restarts     : 4072     (Average: 86.41 Last: 156)
Model-Level  : 251.0   
Problems     : 45       (Average Length: 65.33 Splits: 0)
Lemmas       : 351875   (Deleted: 320980)
  Binary     : 10718    (Ratio:   3.05%)
  Ternary    : 2524     (Ratio:   0.72%)
  Conflict   : 351875   (Average Length:  639.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 351875   (Average: 23.95 Max: 1023 Sum: 8427989)
  Executed   : 351758   (Average: 23.94 Max: 1023 Sum: 8423230 Ratio:  99.94%)
  Bounded    : 117      (Average: 40.68 Max: 107 Sum:   4759 Ratio:   0.06%)

Rules        : 150286   (Original: 135821)
Atoms        : 72368   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 768583   (Eliminated:    0 Frozen: 237361)
Constraints  : 5626532  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 46
Time         : 397.083s (Solving: 372.84s 1st Model: 0.07s Unsat: 11.73s)
CPU Time     : 397.116s

Choices      : 9175045  (Domain: 8942781)
Conflicts    : 359970   (Analyzed: 359966)
Restarts     : 4172     (Average: 86.28 Last: 156)
Model-Level  : 251.0   
Problems     : 46       (Average Length: 66.24 Splits: 0)
Lemmas       : 359966   (Deleted: 329350)
  Binary     : 10809    (Ratio:   3.00%)
  Ternary    : 2532     (Ratio:   0.70%)
  Conflict   : 359966   (Average Length:  630.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 359966   (Average: 23.59 Max: 1023 Sum: 8491221)
  Executed   : 359848   (Average: 23.58 Max: 1023 Sum: 8486355 Ratio:  99.94%)
  Bounded    : 118      (Average: 41.24 Max: 107 Sum:   4866 Ratio:   0.06%)

Rules        : 150286   (Original: 135821)
Atoms        : 72368   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 768583   (Eliminated:    0 Frozen: 237361)
Constraints  : 5626532  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 7.58s
Memory:		 872MB (+0MB)
UNKNOWN
Iteration Time:	 7.63s

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

Models       : 0+
Calls        : 47
Time         : 404.461s (Solving: 380.07s 1st Model: 0.07s Unsat: 11.73s)
CPU Time     : 404.496s

Choices      : 9267150  (Domain: 9034455)
Conflicts    : 368151   (Analyzed: 368147)
Restarts     : 4272     (Average: 86.18 Last: 156)
Model-Level  : 251.0   
Problems     : 47       (Average Length: 67.11 Splits: 0)
Lemmas       : 368147   (Deleted: 337169)
  Binary     : 10863    (Ratio:   2.95%)
  Ternary    : 2547     (Ratio:   0.69%)
  Conflict   : 368147   (Average Length:  622.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 368147   (Average: 23.29 Max: 1023 Sum: 8572935)
  Executed   : 368029   (Average: 23.27 Max: 1023 Sum: 8568069 Ratio:  99.94%)
  Bounded    : 118      (Average: 41.24 Max: 107 Sum:   4866 Ratio:   0.06%)

Rules        : 150286   (Original: 135821)
Atoms        : 72368   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 768583   (Eliminated:    0 Frozen: 237361)
Constraints  : 5626519  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 48
Time         : 412.856s (Solving: 388.31s 1st Model: 0.07s Unsat: 11.73s)
CPU Time     : 412.892s

Choices      : 9404999  (Domain: 9171074)
Conflicts    : 376181   (Analyzed: 376177)
Restarts     : 4372     (Average: 86.04 Last: 156)
Model-Level  : 251.0   
Problems     : 48       (Average Length: 67.94 Splits: 0)
Lemmas       : 376177   (Deleted: 344901)
  Binary     : 10984    (Ratio:   2.92%)
  Ternary    : 2581     (Ratio:   0.69%)
  Conflict   : 376177   (Average Length:  613.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 376177   (Average: 23.12 Max: 1023 Sum: 8698808)
  Executed   : 376058   (Average: 23.11 Max: 1023 Sum: 8693835 Ratio:  99.94%)
  Bounded    : 119      (Average: 41.79 Max: 107 Sum:   4973 Ratio:   0.06%)

Rules        : 150286   (Original: 135821)
Atoms        : 72368   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 768583   (Eliminated:    0 Frozen: 237361)
Constraints  : 5626519  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 49
Time         : 420.928s (Solving: 396.23s 1st Model: 0.07s Unsat: 11.73s)
CPU Time     : 420.968s

Choices      : 9505662  (Domain: 9271445)
Conflicts    : 384278   (Analyzed: 384274)
Restarts     : 4472     (Average: 85.93 Last: 156)
Model-Level  : 251.0   
Problems     : 49       (Average Length: 68.73 Splits: 0)
Lemmas       : 384274   (Deleted: 352566)
  Binary     : 11089    (Ratio:   2.89%)
  Ternary    : 2603     (Ratio:   0.68%)
  Conflict   : 384274   (Average Length:  606.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 384274   (Average: 22.87 Max: 1023 Sum: 8788887)
  Executed   : 384154   (Average: 22.86 Max: 1023 Sum: 8783810 Ratio:  99.94%)
  Bounded    : 120      (Average: 42.31 Max: 107 Sum:   5077 Ratio:   0.06%)

Rules        : 150286   (Original: 135821)
Atoms        : 72368   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 768583   (Eliminated:    0 Frozen: 237361)
Constraints  : 5624066  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 50
Time         : 427.806s (Solving: 402.93s 1st Model: 0.07s Unsat: 11.73s)
CPU Time     : 427.848s

Choices      : 9625963  (Domain: 9391270)
Conflicts    : 392459   (Analyzed: 392455)
Restarts     : 4572     (Average: 85.84 Last: 156)
Model-Level  : 251.0   
Problems     : 50       (Average Length: 69.50 Splits: 0)
Lemmas       : 392455   (Deleted: 360317)
  Binary     : 11167    (Ratio:   2.85%)
  Ternary    : 2619     (Ratio:   0.67%)
  Conflict   : 392455   (Average Length:  598.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 392455   (Average: 22.67 Max: 1023 Sum: 8896777)
  Executed   : 392334   (Average: 22.66 Max: 1023 Sum: 8891593 Ratio:  99.94%)
  Bounded    : 121      (Average: 42.84 Max: 107 Sum:   5184 Ratio:   0.06%)

Rules        : 150286   (Original: 135821)
Atoms        : 72368   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 768583   (Eliminated:    0 Frozen: 237361)
Constraints  : 5624066  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 51
Time         : 435.846s (Solving: 410.82s 1st Model: 0.07s Unsat: 11.73s)
CPU Time     : 435.892s

Choices      : 9779433  (Domain: 9544044)
Conflicts    : 400194   (Analyzed: 400190)
Restarts     : 4672     (Average: 85.66 Last: 156)
Model-Level  : 251.0   
Problems     : 51       (Average Length: 70.24 Splits: 0)
Lemmas       : 400190   (Deleted: 368168)
  Binary     : 11259    (Ratio:   2.81%)
  Ternary    : 2634     (Ratio:   0.66%)
  Conflict   : 400190   (Average Length:  591.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 400190   (Average: 22.58 Max: 1023 Sum: 9035408)
  Executed   : 400069   (Average: 22.56 Max: 1023 Sum: 9030224 Ratio:  99.94%)
  Bounded    : 121      (Average: 42.84 Max: 107 Sum:   5184 Ratio:   0.06%)

Rules        : 150286   (Original: 135821)
Atoms        : 72368   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 768583   (Eliminated:    0 Frozen: 237361)
Constraints  : 5624052  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 7.99s
Memory:		 872MB (+0MB)
UNKNOWN
Iteration Time:	 8.05s

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

Models       : 0+
Calls        : 52
Time         : 446.075s (Solving: 420.90s 1st Model: 0.07s Unsat: 11.73s)
CPU Time     : 446.116s

Choices      : 9905268  (Domain: 9669814)
Conflicts    : 408173   (Analyzed: 408169)
Restarts     : 4772     (Average: 85.53 Last: 156)
Model-Level  : 251.0   
Problems     : 52       (Average Length: 70.94 Splits: 0)
Lemmas       : 408169   (Deleted: 375638)
  Binary     : 11366    (Ratio:   2.78%)
  Ternary    : 2653     (Ratio:   0.65%)
  Conflict   : 408169   (Average Length:  585.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 408169   (Average: 22.40 Max: 1023 Sum: 9142549)
  Executed   : 408048   (Average: 22.39 Max: 1023 Sum: 9137365 Ratio:  99.94%)
  Bounded    : 121      (Average: 42.84 Max: 107 Sum:   5184 Ratio:   0.06%)

Rules        : 150286   (Original: 135821)
Atoms        : 72368   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 768583   (Eliminated:    0 Frozen: 237361)
Constraints  : 5624052  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 10.17s
Memory:		 872MB (+0MB)
UNKNOWN
Iteration Time:	 10.22s

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

Models       : 0+
Calls        : 53
Time         : 455.758s (Solving: 430.39s 1st Model: 0.07s Unsat: 11.73s)
CPU Time     : 455.804s

Choices      : 10158880 (Domain: 9921926)
Conflicts    : 416559   (Analyzed: 416555)
Restarts     : 4872     (Average: 85.50 Last: 156)
Model-Level  : 251.0   
Problems     : 53       (Average Length: 71.62 Splits: 0)
Lemmas       : 416555   (Deleted: 383356)
  Binary     : 11464    (Ratio:   2.75%)
  Ternary    : 2698     (Ratio:   0.65%)
  Conflict   : 416555   (Average Length:  579.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 416555   (Average: 22.51 Max: 1023 Sum: 9377370)
  Executed   : 416434   (Average: 22.50 Max: 1023 Sum: 9372186 Ratio:  99.94%)
  Bounded    : 121      (Average: 42.84 Max: 107 Sum:   5184 Ratio:   0.06%)

Rules        : 150286   (Original: 135821)
Atoms        : 72368   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 768583   (Eliminated:    0 Frozen: 237361)
Constraints  : 5624052  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 9.61s
Memory:		 872MB (+0MB)
UNKNOWN
Iteration Time:	 9.69s

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

Models       : 0+
Calls        : 54
Time         : 463.893s (Solving: 438.34s 1st Model: 0.07s Unsat: 11.73s)
CPU Time     : 463.940s

Choices      : 10300002 (Domain: 10061882)
Conflicts    : 424673   (Analyzed: 424669)
Restarts     : 4972     (Average: 85.41 Last: 156)
Model-Level  : 251.0   
Problems     : 54       (Average Length: 72.28 Splits: 0)
Lemmas       : 424669   (Deleted: 391322)
  Binary     : 11509    (Ratio:   2.71%)
  Ternary    : 2711     (Ratio:   0.64%)
  Conflict   : 424669   (Average Length:  573.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 424669   (Average: 22.38 Max: 1023 Sum: 9502950)
  Executed   : 424546   (Average: 22.36 Max: 1023 Sum: 9497557 Ratio:  99.94%)
  Bounded    : 123      (Average: 43.85 Max: 107 Sum:   5393 Ratio:   0.06%)

Rules        : 150286   (Original: 135821)
Atoms        : 72368   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 768583   (Eliminated:    0 Frozen: 237361)
Constraints  : 5624052  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 55
Time         : 470.272s (Solving: 444.57s 1st Model: 0.07s Unsat: 11.73s)
CPU Time     : 470.320s

Choices      : 10426836 (Domain: 10188457)
Conflicts    : 432581   (Analyzed: 432577)
Restarts     : 5072     (Average: 85.29 Last: 156)
Model-Level  : 251.0   
Problems     : 55       (Average Length: 72.91 Splits: 0)
Lemmas       : 432577   (Deleted: 399214)
  Binary     : 11536    (Ratio:   2.67%)
  Ternary    : 2722     (Ratio:   0.63%)
  Conflict   : 432577   (Average Length:  568.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 432577   (Average: 22.23 Max: 1023 Sum: 9614354)
  Executed   : 432453   (Average: 22.21 Max: 1023 Sum: 9608857 Ratio:  99.94%)
  Bounded    : 124      (Average: 44.33 Max: 107 Sum:   5497 Ratio:   0.06%)

Rules        : 150286   (Original: 135821)
Atoms        : 72368   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 768583   (Eliminated:    0 Frozen: 237361)
Constraints  : 5624038  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 56
Time         : 484.717s (Solving: 457.82s 1st Model: 0.07s Unsat: 11.73s)
CPU Time     : 484.772s

Choices      : 10668740 (Domain: 10429909)
Conflicts    : 441287   (Analyzed: 441283)
Restarts     : 5172     (Average: 85.32 Last: 156)
Model-Level  : 251.0   
Problems     : 56       (Average Length: 73.61 Splits: 0)
Lemmas       : 441283   (Deleted: 409052)
  Binary     : 11634    (Ratio:   2.64%)
  Ternary    : 2724     (Ratio:   0.62%)
  Conflict   : 441283   (Average Length:  572.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 441283   (Average: 22.25 Max: 1075 Sum: 9820081)
  Executed   : 441159   (Average: 22.24 Max: 1075 Sum: 9814584 Ratio:  99.94%)
  Bounded    : 124      (Average: 44.33 Max: 107 Sum:   5497 Ratio:   0.06%)

Rules        : 150286   (Original: 135821)
Atoms        : 72368   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 806074   (Eliminated:    0 Frozen: 249021)
Constraints  : 5906498  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 13.41s
Memory:		 902MB (+28MB)
UNKNOWN
Iteration Time:	 14.46s

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

Models       : 0+
Calls        : 57
Time         : 495.871s (Solving: 467.77s 1st Model: 0.07s Unsat: 11.73s)
CPU Time     : 495.916s

Choices      : 10772507 (Domain: 10533671)
Conflicts    : 449452   (Analyzed: 449448)
Restarts     : 5272     (Average: 85.25 Last: 156)
Model-Level  : 251.0   
Problems     : 57       (Average Length: 74.37 Splits: 0)
Lemmas       : 449448   (Deleted: 416419)
  Binary     : 11660    (Ratio:   2.59%)
  Ternary    : 2727     (Ratio:   0.61%)
  Conflict   : 449448   (Average Length:  582.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 449448   (Average: 21.99 Max: 1075 Sum: 9884708)
  Executed   : 449324   (Average: 21.98 Max: 1075 Sum: 9879211 Ratio:  99.94%)
  Bounded    : 124      (Average: 44.33 Max: 107 Sum:   5497 Ratio:   0.06%)

Rules        : 150286   (Original: 135821)
Atoms        : 72368   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 843565   (Eliminated:    0 Frozen: 260681)
Constraints  : 6188958  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 10.08s
Memory:		 917MB (+15MB)
UNKNOWN
Iteration Time:	 11.16s

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

Models       : 0+
Calls        : 58
Time         : 499.255s (Solving: 470.95s 1st Model: 0.07s Unsat: 11.73s)
CPU Time     : 499.300s

Choices      : 10812374 (Domain: 10573538)
Conflicts    : 456821   (Analyzed: 456817)
Restarts     : 5372     (Average: 85.04 Last: 156)
Model-Level  : 251.0   
Problems     : 58       (Average Length: 75.10 Splits: 0)
Lemmas       : 456817   (Deleted: 423390)
  Binary     : 11706    (Ratio:   2.56%)
  Ternary    : 2735     (Ratio:   0.60%)
  Conflict   : 456817   (Average Length:  576.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 456817   (Average: 21.71 Max: 1075 Sum: 9919018)
  Executed   : 456692   (Average: 21.70 Max: 1075 Sum: 9913409 Ratio:  99.94%)
  Bounded    : 125      (Average: 44.87 Max: 112 Sum:   5609 Ratio:   0.06%)

Rules        : 150286   (Original: 135821)
Atoms        : 72368   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 843565   (Eliminated:    0 Frozen: 260681)
Constraints  : 6188958  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 3.31s
Memory:		 927MB (+10MB)
UNKNOWN
Iteration Time:	 3.39s

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

Models       : 0+
Calls        : 59
Time         : 503.796s (Solving: 475.31s 1st Model: 0.07s Unsat: 11.73s)
CPU Time     : 503.844s

Choices      : 10858072 (Domain: 10619236)
Conflicts    : 464736   (Analyzed: 464732)
Restarts     : 5472     (Average: 84.93 Last: 156)
Model-Level  : 251.0   
Problems     : 59       (Average Length: 75.81 Splits: 0)
Lemmas       : 464732   (Deleted: 430527)
  Binary     : 11723    (Ratio:   2.52%)
  Ternary    : 2749     (Ratio:   0.59%)
  Conflict   : 464732   (Average Length:  571.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 464732   (Average: 21.43 Max: 1075 Sum: 9957893)
  Executed   : 464605   (Average: 21.41 Max: 1075 Sum: 9952058 Ratio:  99.94%)
  Bounded    : 127      (Average: 45.94 Max: 114 Sum:   5835 Ratio:   0.06%)

Rules        : 150286   (Original: 135821)
Atoms        : 72368   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 843565   (Eliminated:    0 Frozen: 260681)
Constraints  : 6188958  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 60
Time         : 509.698s (Solving: 481.03s 1st Model: 0.07s Unsat: 11.73s)
CPU Time     : 509.748s

Choices      : 10938343 (Domain: 10698726)
Conflicts    : 473005   (Analyzed: 473001)
Restarts     : 5572     (Average: 84.89 Last: 156)
Model-Level  : 251.0   
Problems     : 60       (Average Length: 76.50 Splits: 0)
Lemmas       : 473001   (Deleted: 438128)
  Binary     : 11839    (Ratio:   2.50%)
  Ternary    : 2762     (Ratio:   0.58%)
  Conflict   : 473001   (Average Length:  566.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 473001   (Average: 21.20 Max: 1075 Sum: 10029310)
  Executed   : 472874   (Average: 21.19 Max: 1075 Sum: 10023475 Ratio:  99.94%)
  Bounded    : 127      (Average: 45.94 Max: 114 Sum:   5835 Ratio:   0.06%)

Rules        : 150286   (Original: 135821)
Atoms        : 72368   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 843565   (Eliminated:    0 Frozen: 260681)
Constraints  : 6188958  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 61
Time         : 517.744s (Solving: 488.91s 1st Model: 0.07s Unsat: 11.73s)
CPU Time     : 517.800s

Choices      : 11034827 (Domain: 10794716)
Conflicts    : 481513   (Analyzed: 481509)
Restarts     : 5672     (Average: 84.89 Last: 156)
Model-Level  : 251.0   
Problems     : 61       (Average Length: 77.16 Splits: 0)
Lemmas       : 481509   (Deleted: 446167)
  Binary     : 11939    (Ratio:   2.48%)
  Ternary    : 2780     (Ratio:   0.58%)
  Conflict   : 481509   (Average Length:  561.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 481509   (Average: 21.01 Max: 1075 Sum: 10115598)
  Executed   : 481382   (Average: 21.00 Max: 1075 Sum: 10109763 Ratio:  99.94%)
  Bounded    : 127      (Average: 45.94 Max: 114 Sum:   5835 Ratio:   0.06%)

Rules        : 150286   (Original: 135821)
Atoms        : 72368   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 843565   (Eliminated:    0 Frozen: 260681)
Constraints  : 6188958  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 7.99s
Memory:		 927MB (+0MB)
UNKNOWN
Iteration Time:	 8.05s

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

Models       : 0+
Calls        : 62
Time         : 521.594s (Solving: 492.59s 1st Model: 0.07s Unsat: 11.73s)
CPU Time     : 521.652s

Choices      : 11082265 (Domain: 10842139)
Conflicts    : 488820   (Analyzed: 488816)
Restarts     : 5772     (Average: 84.69 Last: 156)
Model-Level  : 251.0   
Problems     : 62       (Average Length: 77.81 Splits: 0)
Lemmas       : 488816   (Deleted: 454353)
  Binary     : 11995    (Ratio:   2.45%)
  Ternary    : 2789     (Ratio:   0.57%)
  Conflict   : 488816   (Average Length:  556.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 488816   (Average: 20.77 Max: 1075 Sum: 10152675)
  Executed   : 488689   (Average: 20.76 Max: 1075 Sum: 10146840 Ratio:  99.94%)
  Bounded    : 127      (Average: 45.94 Max: 114 Sum:   5835 Ratio:   0.06%)

Rules        : 150286   (Original: 135821)
Atoms        : 72368   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 843565   (Eliminated:    0 Frozen: 260681)
Constraints  : 6188958  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 63
Time         : 530.749s (Solving: 501.56s 1st Model: 0.07s Unsat: 11.73s)
CPU Time     : 530.812s

Choices      : 11222325 (Domain: 10981354)
Conflicts    : 497837   (Analyzed: 497833)
Restarts     : 5872     (Average: 84.78 Last: 156)
Model-Level  : 251.0   
Problems     : 63       (Average Length: 78.43 Splits: 0)
Lemmas       : 497833   (Deleted: 463546)
  Binary     : 12171    (Ratio:   2.44%)
  Ternary    : 2808     (Ratio:   0.56%)
  Conflict   : 497833   (Average Length:  552.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 497833   (Average: 20.65 Max: 1075 Sum: 10278415)
  Executed   : 497706   (Average: 20.63 Max: 1075 Sum: 10272580 Ratio:  99.94%)
  Bounded    : 127      (Average: 45.94 Max: 114 Sum:   5835 Ratio:   0.06%)

Rules        : 150286   (Original: 135821)
Atoms        : 72368   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 843565   (Eliminated:    0 Frozen: 260681)
Constraints  : 6188958  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 64
Time         : 537.295s (Solving: 507.89s 1st Model: 0.07s Unsat: 11.73s)
CPU Time     : 537.360s

Choices      : 11306159 (Domain: 11064750)
Conflicts    : 506280   (Analyzed: 506276)
Restarts     : 5972     (Average: 84.77 Last: 156)
Model-Level  : 251.0   
Problems     : 64       (Average Length: 79.03 Splits: 0)
Lemmas       : 506276   (Deleted: 470056)
  Binary     : 12234    (Ratio:   2.42%)
  Ternary    : 2820     (Ratio:   0.56%)
  Conflict   : 506276   (Average Length:  548.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 506276   (Average: 20.44 Max: 1075 Sum: 10350693)
  Executed   : 506148   (Average: 20.43 Max: 1075 Sum: 10344741 Ratio:  99.94%)
  Bounded    : 128      (Average: 46.50 Max: 117 Sum:   5952 Ratio:   0.06%)

Rules        : 150286   (Original: 135821)
Atoms        : 72368   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 843565   (Eliminated:    0 Frozen: 260681)
Constraints  : 6188958  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 65
Time         : 544.810s (Solving: 515.24s 1st Model: 0.07s Unsat: 11.73s)
CPU Time     : 544.880s

Choices      : 11455247 (Domain: 11212748)
Conflicts    : 514387   (Analyzed: 514383)
Restarts     : 6072     (Average: 84.71 Last: 156)
Model-Level  : 251.0   
Problems     : 65       (Average Length: 79.62 Splits: 0)
Lemmas       : 514383   (Deleted: 478195)
  Binary     : 12351    (Ratio:   2.40%)
  Ternary    : 2841     (Ratio:   0.55%)
  Conflict   : 514383   (Average Length:  545.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 514383   (Average: 20.38 Max: 1075 Sum: 10484475)
  Executed   : 514255   (Average: 20.37 Max: 1075 Sum: 10478523 Ratio:  99.94%)
  Bounded    : 128      (Average: 46.50 Max: 117 Sum:   5952 Ratio:   0.06%)

Rules        : 150286   (Original: 135821)
Atoms        : 72368   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 843565   (Eliminated:    0 Frozen: 260681)
Constraints  : 6188944  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 7.46s
Memory:		 927MB (+0MB)
UNKNOWN
Iteration Time:	 7.52s

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

Models       : 0+
Calls        : 66
Time         : 550.994s (Solving: 521.22s 1st Model: 0.07s Unsat: 11.73s)
CPU Time     : 551.056s

Choices      : 11541864 (Domain: 11299167)
Conflicts    : 522560   (Analyzed: 522556)
Restarts     : 6172     (Average: 84.67 Last: 156)
Model-Level  : 251.0   
Problems     : 66       (Average Length: 80.18 Splits: 0)
Lemmas       : 522556   (Deleted: 485968)
  Binary     : 12433    (Ratio:   2.38%)
  Ternary    : 2858     (Ratio:   0.55%)
  Conflict   : 522556   (Average Length:  542.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 522556   (Average: 20.20 Max: 1075 Sum: 10556947)
  Executed   : 522428   (Average: 20.19 Max: 1075 Sum: 10550995 Ratio:  99.94%)
  Bounded    : 128      (Average: 46.50 Max: 117 Sum:   5952 Ratio:   0.06%)

Rules        : 150286   (Original: 135821)
Atoms        : 72368   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 843565   (Eliminated:    0 Frozen: 260681)
Constraints  : 6188944  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 67
Time         : 559.177s (Solving: 529.20s 1st Model: 0.07s Unsat: 11.73s)
CPU Time     : 559.244s

Choices      : 11708081 (Domain: 11465007)
Conflicts    : 530676   (Analyzed: 530672)
Restarts     : 6272     (Average: 84.61 Last: 156)
Model-Level  : 251.0   
Problems     : 67       (Average Length: 80.73 Splits: 0)
Lemmas       : 530672   (Deleted: 493893)
  Binary     : 12530    (Ratio:   2.36%)
  Ternary    : 2875     (Ratio:   0.54%)
  Conflict   : 530672   (Average Length:  538.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 530672   (Average: 20.17 Max: 1075 Sum: 10705980)
  Executed   : 530544   (Average: 20.16 Max: 1075 Sum: 10700028 Ratio:  99.94%)
  Bounded    : 128      (Average: 46.50 Max: 117 Sum:   5952 Ratio:   0.06%)

Rules        : 150286   (Original: 135821)
Atoms        : 72368   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 843565   (Eliminated:    0 Frozen: 260681)
Constraints  : 6188944  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 68
Time         : 568.017s (Solving: 537.87s 1st Model: 0.07s Unsat: 11.73s)
CPU Time     : 568.088s

Choices      : 11908051 (Domain: 11664762)
Conflicts    : 539322   (Analyzed: 539318)
Restarts     : 6372     (Average: 84.64 Last: 156)
Model-Level  : 251.0   
Problems     : 68       (Average Length: 81.26 Splits: 0)
Lemmas       : 539318   (Deleted: 503888)
  Binary     : 12638    (Ratio:   2.34%)
  Ternary    : 2884     (Ratio:   0.53%)
  Conflict   : 539318   (Average Length:  534.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 539318   (Average: 20.19 Max: 1075 Sum: 10886391)
  Executed   : 539189   (Average: 20.17 Max: 1075 Sum: 10880327 Ratio:  99.94%)
  Bounded    : 129      (Average: 47.01 Max: 117 Sum:   6064 Ratio:   0.06%)

Rules        : 150286   (Original: 135821)
Atoms        : 72368   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 843565   (Eliminated:    0 Frozen: 260681)
Constraints  : 6188944  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 69
Time         : 574.518s (Solving: 544.16s 1st Model: 0.07s Unsat: 11.73s)
CPU Time     : 574.592s

Choices      : 12047760 (Domain: 11804381)
Conflicts    : 548179   (Analyzed: 548175)
Restarts     : 6472     (Average: 84.70 Last: 156)
Model-Level  : 251.0   
Problems     : 69       (Average Length: 81.78 Splits: 0)
Lemmas       : 548175   (Deleted: 512269)
  Binary     : 12742    (Ratio:   2.32%)
  Ternary    : 2894     (Ratio:   0.53%)
  Conflict   : 548175   (Average Length:  531.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 548175   (Average: 20.08 Max: 1075 Sum: 11006343)
  Executed   : 548046   (Average: 20.07 Max: 1075 Sum: 11000279 Ratio:  99.94%)
  Bounded    : 129      (Average: 47.01 Max: 117 Sum:   6064 Ratio:   0.06%)

Rules        : 150286   (Original: 135821)
Atoms        : 72368   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 843565   (Eliminated:    0 Frozen: 260681)
Constraints  : 6188944  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 70
Time         : 587.844s (Solving: 556.24s 1st Model: 0.07s Unsat: 11.73s)
CPU Time     : 587.924s

Choices      : 12230896 (Domain: 11987474)
Conflicts    : 557651   (Analyzed: 557647)
Restarts     : 6572     (Average: 84.85 Last: 156)
Model-Level  : 251.0   
Problems     : 70       (Average Length: 82.36 Splits: 0)
Lemmas       : 557647   (Deleted: 520972)
  Binary     : 12795    (Ratio:   2.29%)
  Ternary    : 2897     (Ratio:   0.52%)
  Conflict   : 557647   (Average Length:  535.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 557647   (Average: 19.99 Max: 1251 Sum: 11149909)
  Executed   : 557518   (Average: 19.98 Max: 1251 Sum: 11143845 Ratio:  99.95%)
  Bounded    : 129      (Average: 47.01 Max: 117 Sum:   6064 Ratio:   0.05%)

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

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

[endof: stats after solve call]
Solving Time:	 12.23s
Memory:		 945MB (+18MB)
UNKNOWN
Iteration Time:	 13.34s

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

Models       : 0+
Calls        : 71
Time         : 592.054s (Solving: 560.24s 1st Model: 0.07s Unsat: 11.73s)
CPU Time     : 592.136s

Choices      : 12274419 (Domain: 12030997)
Conflicts    : 565316   (Analyzed: 565312)
Restarts     : 6672     (Average: 84.73 Last: 156)
Model-Level  : 251.0   
Problems     : 71       (Average Length: 82.92 Splits: 0)
Lemmas       : 565312   (Deleted: 528048)
  Binary     : 12842    (Ratio:   2.27%)
  Ternary    : 2901     (Ratio:   0.51%)
  Conflict   : 565312   (Average Length:  531.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 565312   (Average: 19.79 Max: 1251 Sum: 11187560)
  Executed   : 565182   (Average: 19.78 Max: 1251 Sum: 11181379 Ratio:  99.94%)
  Bounded    : 130      (Average: 47.55 Max: 117 Sum:   6181 Ratio:   0.06%)

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

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

[endof: stats after solve call]
Solving Time:	 4.13s
Memory:		 951MB (+6MB)
UNKNOWN
Iteration Time:	 4.22s

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

Models       : 0+
Calls        : 72
Time         : 599.780s (Solving: 567.79s 1st Model: 0.07s Unsat: 11.73s)
CPU Time     : 599.864s

Choices      : 12331284 (Domain: 12087862)
Conflicts    : 573401   (Analyzed: 573397)
Restarts     : 6772     (Average: 84.67 Last: 156)
Model-Level  : 251.0   
Problems     : 72       (Average Length: 83.46 Splits: 0)
Lemmas       : 573397   (Deleted: 535492)
  Binary     : 12961    (Ratio:   2.26%)
  Ternary    : 2915     (Ratio:   0.51%)
  Conflict   : 573397   (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    : 573397   (Average: 19.58 Max: 1251 Sum: 11228500)
  Executed   : 573265   (Average: 19.57 Max: 1251 Sum: 11222075 Ratio:  99.94%)
  Bounded    : 132      (Average: 48.67 Max: 122 Sum:   6425 Ratio:   0.06%)

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

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

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

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

Models       : 0+
Calls        : 73
Time         : 604.310s (Solving: 572.14s 1st Model: 0.07s Unsat: 11.73s)
CPU Time     : 604.396s

Choices      : 12388157 (Domain: 12143984)
Conflicts    : 581175   (Analyzed: 581171)
Restarts     : 6872     (Average: 84.57 Last: 156)
Model-Level  : 251.0   
Problems     : 73       (Average Length: 83.99 Splits: 0)
Lemmas       : 581171   (Deleted: 543337)
  Binary     : 13009    (Ratio:   2.24%)
  Ternary    : 2922     (Ratio:   0.50%)
  Conflict   : 581171   (Average Length:  539.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 581171   (Average: 19.40 Max: 1251 Sum: 11275940)
  Executed   : 581039   (Average: 19.39 Max: 1251 Sum: 11269515 Ratio:  99.94%)
  Bounded    : 132      (Average: 48.67 Max: 122 Sum:   6425 Ratio:   0.06%)

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

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

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

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

Models       : 0+
Calls        : 74
Time         : 609.227s (Solving: 576.85s 1st Model: 0.07s Unsat: 11.73s)
CPU Time     : 609.316s

Choices      : 12450398 (Domain: 12206165)
Conflicts    : 589246   (Analyzed: 589242)
Restarts     : 6972     (Average: 84.52 Last: 156)
Model-Level  : 251.0   
Problems     : 74       (Average Length: 84.50 Splits: 0)
Lemmas       : 589242   (Deleted: 550901)
  Binary     : 13068    (Ratio:   2.22%)
  Ternary    : 2941     (Ratio:   0.50%)
  Conflict   : 589242   (Average Length:  536.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 589242   (Average: 19.23 Max: 1251 Sum: 11328485)
  Executed   : 589110   (Average: 19.21 Max: 1251 Sum: 11322060 Ratio:  99.94%)
  Bounded    : 132      (Average: 48.67 Max: 122 Sum:   6425 Ratio:   0.06%)

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

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

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

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

Models       : 0+
Calls        : 75
Time         : 615.467s (Solving: 582.91s 1st Model: 0.07s Unsat: 11.73s)
CPU Time     : 615.560s

Choices      : 12534348 (Domain: 12289844)
Conflicts    : 597354   (Analyzed: 597350)
Restarts     : 7072     (Average: 84.47 Last: 156)
Model-Level  : 251.0   
Problems     : 75       (Average Length: 85.00 Splits: 0)
Lemmas       : 597350   (Deleted: 558717)
  Binary     : 13138    (Ratio:   2.20%)
  Ternary    : 2943     (Ratio:   0.49%)
  Conflict   : 597350   (Average Length:  534.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 597350   (Average: 19.09 Max: 1251 Sum: 11400868)
  Executed   : 597217   (Average: 19.07 Max: 1251 Sum: 11394321 Ratio:  99.94%)
  Bounded    : 133      (Average: 49.23 Max: 122 Sum:   6547 Ratio:   0.06%)

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

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

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

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

Models       : 0+
Calls        : 76
Time         : 621.430s (Solving: 588.68s 1st Model: 0.07s Unsat: 11.73s)
CPU Time     : 621.524s

Choices      : 12606874 (Domain: 12362239)
Conflicts    : 605822   (Analyzed: 605818)
Restarts     : 7172     (Average: 84.47 Last: 156)
Model-Level  : 251.0   
Problems     : 76       (Average Length: 85.49 Splits: 0)
Lemmas       : 605818   (Deleted: 566586)
  Binary     : 13230    (Ratio:   2.18%)
  Ternary    : 2953     (Ratio:   0.49%)
  Conflict   : 605818   (Average Length:  530.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 605818   (Average: 18.92 Max: 1251 Sum: 11462312)
  Executed   : 605684   (Average: 18.91 Max: 1251 Sum: 11455643 Ratio:  99.94%)
  Bounded    : 134      (Average: 49.77 Max: 122 Sum:   6669 Ratio:   0.06%)

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

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

[endof: stats after solve call]
Solving Time:	 5.90s
Memory:		 951MB (+0MB)
UNKNOWN
Iteration Time:	 5.97s

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

Models       : 0+
Calls        : 77
Time         : 631.348s (Solving: 598.39s 1st Model: 0.07s Unsat: 11.73s)
CPU Time     : 631.444s

Choices      : 12745085 (Domain: 12500208)
Conflicts    : 615251   (Analyzed: 615247)
Restarts     : 7272     (Average: 84.60 Last: 156)
Model-Level  : 251.0   
Problems     : 77       (Average Length: 85.96 Splits: 0)
Lemmas       : 615247   (Deleted: 576945)
  Binary     : 13385    (Ratio:   2.18%)
  Ternary    : 2968     (Ratio:   0.48%)
  Conflict   : 615247   (Average Length:  529.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 615247   (Average: 18.83 Max: 1251 Sum: 11584576)
  Executed   : 615113   (Average: 18.82 Max: 1251 Sum: 11577907 Ratio:  99.94%)
  Bounded    : 134      (Average: 49.77 Max: 122 Sum:   6669 Ratio:   0.06%)

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

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

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

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

Models       : 0+
Calls        : 78
Time         : 637.526s (Solving: 604.40s 1st Model: 0.07s Unsat: 11.73s)
CPU Time     : 637.616s

Choices      : 12840301 (Domain: 12595227)
Conflicts    : 623777   (Analyzed: 623773)
Restarts     : 7372     (Average: 84.61 Last: 156)
Model-Level  : 251.0   
Problems     : 78       (Average Length: 86.42 Splits: 0)
Lemmas       : 623773   (Deleted: 583858)
  Binary     : 13468    (Ratio:   2.16%)
  Ternary    : 2973     (Ratio:   0.48%)
  Conflict   : 623773   (Average Length:  527.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 623773   (Average: 18.70 Max: 1251 Sum: 11665137)
  Executed   : 623639   (Average: 18.69 Max: 1251 Sum: 11658468 Ratio:  99.94%)
  Bounded    : 134      (Average: 49.77 Max: 122 Sum:   6669 Ratio:   0.06%)

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

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

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

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

Models       : 0+
Calls        : 79
Time         : 644.934s (Solving: 611.63s 1st Model: 0.07s Unsat: 11.73s)
CPU Time     : 645.024s

Choices      : 12990926 (Domain: 12745618)
Conflicts    : 632710   (Analyzed: 632706)
Restarts     : 7472     (Average: 84.68 Last: 156)
Model-Level  : 251.0   
Problems     : 79       (Average Length: 86.87 Splits: 0)
Lemmas       : 632706   (Deleted: 594227)
  Binary     : 13570    (Ratio:   2.14%)
  Ternary    : 2988     (Ratio:   0.47%)
  Conflict   : 632706   (Average Length:  525.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 632706   (Average: 18.65 Max: 1251 Sum: 11798054)
  Executed   : 632571   (Average: 18.64 Max: 1251 Sum: 11791263 Ratio:  99.94%)
  Bounded    : 135      (Average: 50.30 Max: 122 Sum:   6791 Ratio:   0.06%)

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

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

[endof: stats after solve call]
Solving Time:	 7.35s
Memory:		 951MB (+0MB)
UNKNOWN
Iteration Time:	 7.41s

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

Models       : 0+
Calls        : 80
Time         : 651.915s (Solving: 618.41s 1st Model: 0.07s Unsat: 11.73s)
CPU Time     : 652.008s

Choices      : 13064093 (Domain: 12818779)
Conflicts    : 640944   (Analyzed: 640940)
Restarts     : 7572     (Average: 84.65 Last: 156)
Model-Level  : 251.0   
Problems     : 80       (Average Length: 87.31 Splits: 0)
Lemmas       : 640940   (Deleted: 600744)
  Binary     : 13612    (Ratio:   2.12%)
  Ternary    : 2991     (Ratio:   0.47%)
  Conflict   : 640940   (Average Length:  522.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 640940   (Average: 18.50 Max: 1251 Sum: 11856447)
  Executed   : 640804   (Average: 18.49 Max: 1251 Sum: 11849534 Ratio:  99.94%)
  Bounded    : 136      (Average: 50.83 Max: 122 Sum:   6913 Ratio:   0.06%)

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

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

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

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

Models       : 0+
Calls        : 81
Time         : 662.305s (Solving: 628.62s 1st Model: 0.07s Unsat: 11.73s)
CPU Time     : 662.400s

Choices      : 13283271 (Domain: 13037641)
Conflicts    : 649889   (Analyzed: 649885)
Restarts     : 7672     (Average: 84.71 Last: 156)
Model-Level  : 251.0   
Problems     : 81       (Average Length: 87.74 Splits: 0)
Lemmas       : 649885   (Deleted: 610894)
  Binary     : 13715    (Ratio:   2.11%)
  Ternary    : 3007     (Ratio:   0.46%)
  Conflict   : 649885   (Average Length:  521.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 649885   (Average: 18.55 Max: 1251 Sum: 12052144)
  Executed   : 649749   (Average: 18.53 Max: 1251 Sum: 12045231 Ratio:  99.94%)
  Bounded    : 136      (Average: 50.83 Max: 122 Sum:   6913 Ratio:   0.06%)

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

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

[endof: stats after solve call]
Solving Time:	 10.33s
Memory:		 951MB (+0MB)
UNKNOWN
Iteration Time:	 10.40s

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

Models       : 0+
Calls        : 82
Time         : 672.185s (Solving: 638.32s 1st Model: 0.07s Unsat: 11.73s)
CPU Time     : 672.284s

Choices      : 13337257 (Domain: 13091627)
Conflicts    : 658070   (Analyzed: 658066)
Restarts     : 7772     (Average: 84.67 Last: 156)
Model-Level  : 251.0   
Problems     : 82       (Average Length: 88.16 Splits: 0)
Lemmas       : 658066   (Deleted: 617231)
  Binary     : 13785    (Ratio:   2.09%)
  Ternary    : 3023     (Ratio:   0.46%)
  Conflict   : 658066   (Average Length:  527.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 658066   (Average: 18.38 Max: 1251 Sum: 12092844)
  Executed   : 657930   (Average: 18.37 Max: 1251 Sum: 12085931 Ratio:  99.94%)
  Bounded    : 136      (Average: 50.83 Max: 122 Sum:   6913 Ratio:   0.06%)

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

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

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

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

Models       : 0+
Calls        : 83
Time         : 675.796s (Solving: 641.71s 1st Model: 0.07s Unsat: 11.73s)
CPU Time     : 675.896s

Choices      : 13377378 (Domain: 13131748)
Conflicts    : 665295   (Analyzed: 665291)
Restarts     : 7872     (Average: 84.51 Last: 156)
Model-Level  : 251.0   
Problems     : 83       (Average Length: 88.57 Splits: 0)
Lemmas       : 665291   (Deleted: 625249)
  Binary     : 13809    (Ratio:   2.08%)
  Ternary    : 3024     (Ratio:   0.45%)
  Conflict   : 665291   (Average Length:  524.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 665291   (Average: 18.23 Max: 1251 Sum: 12125089)
  Executed   : 665155   (Average: 18.21 Max: 1251 Sum: 12118176 Ratio:  99.94%)
  Bounded    : 136      (Average: 50.83 Max: 122 Sum:   6913 Ratio:   0.06%)

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

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

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

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

Models       : 0+
Calls        : 84
Time         : 679.353s (Solving: 645.09s 1st Model: 0.07s Unsat: 11.73s)
CPU Time     : 679.456s

Choices      : 13425656 (Domain: 13179993)
Conflicts    : 672988   (Analyzed: 672984)
Restarts     : 7972     (Average: 84.42 Last: 156)
Model-Level  : 251.0   
Problems     : 84       (Average Length: 88.96 Splits: 0)
Lemmas       : 672984   (Deleted: 632372)
  Binary     : 13826    (Ratio:   2.05%)
  Ternary    : 3026     (Ratio:   0.45%)
  Conflict   : 672984   (Average Length:  520.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 672984   (Average: 18.08 Max: 1251 Sum: 12165299)
  Executed   : 672848   (Average: 18.07 Max: 1251 Sum: 12158386 Ratio:  99.94%)
  Bounded    : 136      (Average: 50.83 Max: 122 Sum:   6913 Ratio:   0.06%)

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

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

[endof: stats after solve call]
Solving Time:	 3.50s
Memory:		 951MB (+0MB)
UNKNOWN
Iteration Time:	 3.56s

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

Models       : 0+
Calls        : 85
Time         : 686.314s (Solving: 651.85s 1st Model: 0.07s Unsat: 11.73s)
CPU Time     : 686.412s

Choices      : 13499104 (Domain: 13252923)
Conflicts    : 681243   (Analyzed: 681239)
Restarts     : 8072     (Average: 84.40 Last: 156)
Model-Level  : 251.0   
Problems     : 85       (Average Length: 89.35 Splits: 0)
Lemmas       : 681239   (Deleted: 639894)
  Binary     : 13918    (Ratio:   2.04%)
  Ternary    : 3036     (Ratio:   0.45%)
  Conflict   : 681239   (Average Length:  519.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 681239   (Average: 17.95 Max: 1251 Sum: 12227614)
  Executed   : 681103   (Average: 17.94 Max: 1251 Sum: 12220701 Ratio:  99.94%)
  Bounded    : 136      (Average: 50.83 Max: 122 Sum:   6913 Ratio:   0.06%)

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

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

[endof: stats after solve call]
Solving Time:	 6.88s
Memory:		 951MB (+0MB)
UNKNOWN
Iteration Time:	 6.96s

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

Models       : 0+
Calls        : 86
Time         : 693.390s (Solving: 658.75s 1st Model: 0.07s Unsat: 11.73s)
CPU Time     : 693.480s

Choices      : 13598005 (Domain: 13351528)
Conflicts    : 689711   (Analyzed: 689707)
Restarts     : 8172     (Average: 84.40 Last: 156)
Model-Level  : 251.0   
Problems     : 86       (Average Length: 89.73 Splits: 0)
Lemmas       : 689707   (Deleted: 647946)
  Binary     : 13991    (Ratio:   2.03%)
  Ternary    : 3050     (Ratio:   0.44%)
  Conflict   : 689707   (Average Length:  517.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 689707   (Average: 17.85 Max: 1251 Sum: 12312506)
  Executed   : 689571   (Average: 17.84 Max: 1251 Sum: 12305593 Ratio:  99.94%)
  Bounded    : 136      (Average: 50.83 Max: 122 Sum:   6913 Ratio:   0.06%)

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

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

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

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

Models       : 0+
Calls        : 87
Time         : 702.439s (Solving: 667.62s 1st Model: 0.07s Unsat: 11.73s)
CPU Time     : 702.532s

Choices      : 13725705 (Domain: 13478968)
Conflicts    : 698962   (Analyzed: 698958)
Restarts     : 8272     (Average: 84.50 Last: 156)
Model-Level  : 251.0   
Problems     : 87       (Average Length: 90.10 Splits: 0)
Lemmas       : 698958   (Deleted: 658186)
  Binary     : 14086    (Ratio:   2.02%)
  Ternary    : 3069     (Ratio:   0.44%)
  Conflict   : 698958   (Average Length:  517.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 698958   (Average: 17.78 Max: 1251 Sum: 12424271)
  Executed   : 698822   (Average: 17.77 Max: 1251 Sum: 12417358 Ratio:  99.94%)
  Bounded    : 136      (Average: 50.83 Max: 122 Sum:   6913 Ratio:   0.06%)

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

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

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

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

Models       : 0+
Calls        : 88
Time         : 711.949s (Solving: 676.95s 1st Model: 0.07s Unsat: 11.73s)
CPU Time     : 712.044s

Choices      : 13886763 (Domain: 13639450)
Conflicts    : 707595   (Analyzed: 707591)
Restarts     : 8372     (Average: 84.52 Last: 156)
Model-Level  : 251.0   
Problems     : 88       (Average Length: 90.47 Splits: 0)
Lemmas       : 707591   (Deleted: 667058)
  Binary     : 14222    (Ratio:   2.01%)
  Ternary    : 3077     (Ratio:   0.43%)
  Conflict   : 707591   (Average Length:  516.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 707591   (Average: 17.76 Max: 1251 Sum: 12567182)
  Executed   : 707455   (Average: 17.75 Max: 1251 Sum: 12560269 Ratio:  99.94%)
  Bounded    : 136      (Average: 50.83 Max: 122 Sum:   6913 Ratio:   0.06%)

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

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

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

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

Models       : 0+
Calls        : 89
Time         : 721.091s (Solving: 685.92s 1st Model: 0.07s Unsat: 11.73s)
CPU Time     : 721.192s

Choices      : 14059637 (Domain: 13812265)
Conflicts    : 716080   (Analyzed: 716076)
Restarts     : 8472     (Average: 84.52 Last: 156)
Model-Level  : 251.0   
Problems     : 89       (Average Length: 90.82 Splits: 0)
Lemmas       : 716076   (Deleted: 673327)
  Binary     : 14329    (Ratio:   2.00%)
  Ternary    : 3090     (Ratio:   0.43%)
  Conflict   : 716076   (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    : 716076   (Average: 17.76 Max: 1251 Sum: 12720490)
  Executed   : 715940   (Average: 17.75 Max: 1251 Sum: 12713577 Ratio:  99.95%)
  Bounded    : 136      (Average: 50.83 Max: 122 Sum:   6913 Ratio:   0.05%)

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

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

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

Iteration 89
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        : 90
Time         : 732.579s (Solving: 697.20s 1st Model: 0.07s Unsat: 11.73s)
CPU Time     : 732.684s

Choices      : 14100867 (Domain: 13853495)
Conflicts    : 724077   (Analyzed: 724073)
Restarts     : 8572     (Average: 84.47 Last: 156)
Model-Level  : 251.0   
Problems     : 90       (Average Length: 91.17 Splits: 0)
Lemmas       : 724073   (Deleted: 681409)
  Binary     : 14360    (Ratio:   1.98%)
  Ternary    : 3100     (Ratio:   0.43%)
  Conflict   : 724073   (Average Length:  525.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 724073   (Average: 17.60 Max: 1251 Sum: 12747146)
  Executed   : 723937   (Average: 17.60 Max: 1251 Sum: 12740233 Ratio:  99.95%)
  Bounded    : 136      (Average: 50.83 Max: 122 Sum:   6913 Ratio:   0.05%)

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

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

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

Iteration 90
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        : 91
Time         : 743.153s (Solving: 707.60s 1st Model: 0.07s Unsat: 11.73s)
CPU Time     : 743.264s

Choices      : 14181205 (Domain: 13933833)
Conflicts    : 732907   (Analyzed: 732903)
Restarts     : 8672     (Average: 84.51 Last: 156)
Model-Level  : 251.0   
Problems     : 91       (Average Length: 91.51 Splits: 0)
Lemmas       : 732903   (Deleted: 691313)
  Binary     : 14488    (Ratio:   1.98%)
  Ternary    : 3115     (Ratio:   0.43%)
  Conflict   : 732903   (Average Length:  534.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 732903   (Average: 17.48 Max: 1251 Sum: 12810514)
  Executed   : 732767   (Average: 17.47 Max: 1251 Sum: 12803601 Ratio:  99.95%)
  Bounded    : 136      (Average: 50.83 Max: 122 Sum:   6913 Ratio:   0.05%)

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

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

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

Iteration 91
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        : 92
Time         : 751.909s (Solving: 716.15s 1st Model: 0.07s Unsat: 11.73s)
CPU Time     : 752.024s

Choices      : 14274384 (Domain: 14025315)
Conflicts    : 741979   (Analyzed: 741975)
Restarts     : 8772     (Average: 84.58 Last: 156)
Model-Level  : 251.0   
Problems     : 92       (Average Length: 91.84 Splits: 0)
Lemmas       : 741975   (Deleted: 699712)
  Binary     : 14683    (Ratio:   1.98%)
  Ternary    : 3138     (Ratio:   0.42%)
  Conflict   : 741975   (Average Length:  536.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 741975   (Average: 17.36 Max: 1251 Sum: 12884042)
  Executed   : 741839   (Average: 17.36 Max: 1251 Sum: 12877129 Ratio:  99.95%)
  Bounded    : 136      (Average: 50.83 Max: 122 Sum:   6913 Ratio:   0.05%)

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

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

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

Iteration 92
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        : 93
Time         : 760.968s (Solving: 725.03s 1st Model: 0.07s Unsat: 11.73s)
CPU Time     : 761.084s

Choices      : 14345501 (Domain: 14096386)
Conflicts    : 749879   (Analyzed: 749875)
Restarts     : 8872     (Average: 84.52 Last: 156)
Model-Level  : 251.0   
Problems     : 93       (Average Length: 92.16 Splits: 0)
Lemmas       : 749875   (Deleted: 706140)
  Binary     : 14752    (Ratio:   1.97%)
  Ternary    : 3145     (Ratio:   0.42%)
  Conflict   : 749875   (Average Length:  540.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 749875   (Average: 17.26 Max: 1251 Sum: 12939485)
  Executed   : 749739   (Average: 17.25 Max: 1251 Sum: 12932572 Ratio:  99.95%)
  Bounded    : 136      (Average: 50.83 Max: 122 Sum:   6913 Ratio:   0.05%)

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

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

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

Iteration 93
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        : 94
Time         : 765.766s (Solving: 729.65s 1st Model: 0.07s Unsat: 11.73s)
CPU Time     : 765.880s

Choices      : 14413522 (Domain: 14164389)
Conflicts    : 758025   (Analyzed: 758021)
Restarts     : 8972     (Average: 84.49 Last: 156)
Model-Level  : 251.0   
Problems     : 94       (Average Length: 92.48 Splits: 0)
Lemmas       : 758021   (Deleted: 713728)
  Binary     : 14787    (Ratio:   1.95%)
  Ternary    : 3160     (Ratio:   0.42%)
  Conflict   : 758021   (Average Length:  537.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 758021   (Average: 17.15 Max: 1251 Sum: 12997739)
  Executed   : 757882   (Average: 17.14 Max: 1251 Sum: 12990466 Ratio:  99.94%)
  Bounded    : 139      (Average: 52.32 Max: 122 Sum:   7273 Ratio:   0.06%)

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

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

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

Iteration 94
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        : 95
Time         : 771.423s (Solving: 735.10s 1st Model: 0.07s Unsat: 11.73s)
CPU Time     : 771.532s

Choices      : 14498861 (Domain: 14249452)
Conflicts    : 766363   (Analyzed: 766359)
Restarts     : 9072     (Average: 84.48 Last: 156)
Model-Level  : 251.0   
Problems     : 95       (Average Length: 92.79 Splits: 0)
Lemmas       : 766359   (Deleted: 721649)
  Binary     : 14850    (Ratio:   1.94%)
  Ternary    : 3190     (Ratio:   0.42%)
  Conflict   : 766359   (Average Length:  535.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 766359   (Average: 17.05 Max: 1251 Sum: 13070078)
  Executed   : 766220   (Average: 17.05 Max: 1251 Sum: 13062805 Ratio:  99.94%)
  Bounded    : 139      (Average: 52.32 Max: 122 Sum:   7273 Ratio:   0.06%)

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

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

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

Iteration 95
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        : 96
Time         : 780.173s (Solving: 743.65s 1st Model: 0.07s Unsat: 11.73s)
CPU Time     : 780.272s

Choices      : 14675328 (Domain: 14425529)
Conflicts    : 775282   (Analyzed: 775278)
Restarts     : 9172     (Average: 84.53 Last: 156)
Model-Level  : 251.0   
Problems     : 96       (Average Length: 93.09 Splits: 0)
Lemmas       : 775278   (Deleted: 731774)
  Binary     : 14940    (Ratio:   1.93%)
  Ternary    : 3241     (Ratio:   0.42%)
  Conflict   : 775278   (Average Length:  533.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 775278   (Average: 17.06 Max: 1251 Sum: 13226041)
  Executed   : 775138   (Average: 17.05 Max: 1251 Sum: 13218646 Ratio:  99.94%)
  Bounded    : 140      (Average: 52.82 Max: 122 Sum:   7395 Ratio:   0.06%)

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

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

[endof: stats after solve call]
Solving Time:	 8.67s
Memory:		 951MB (+0MB)
UNKNOWN
Iteration Time:	 8.74s

Iteration 96
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        : 97
Time         : 787.232s (Solving: 750.51s 1st Model: 0.07s Unsat: 11.73s)
CPU Time     : 787.332s

Choices      : 14784362 (Domain: 14534491)
Conflicts    : 784058   (Analyzed: 784054)
Restarts     : 9272     (Average: 84.56 Last: 175)
Model-Level  : 251.0   
Problems     : 97       (Average Length: 93.39 Splits: 0)
Lemmas       : 784054   (Deleted: 740441)
  Binary     : 14984    (Ratio:   1.91%)
  Ternary    : 3242     (Ratio:   0.41%)
  Conflict   : 784054   (Average Length:  532.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 784054   (Average: 16.99 Max: 1251 Sum: 13317516)
  Executed   : 783913   (Average: 16.98 Max: 1251 Sum: 13310001 Ratio:  99.94%)
  Bounded    : 141      (Average: 53.30 Max: 122 Sum:   7515 Ratio:   0.06%)

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

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

[endof: stats after solve call]
Solving Time:	 6.99s
Memory:		 951MB (+0MB)
UNKNOWN
Iteration Time:	 7.06s

Iteration 97
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        : 98
Time         : 796.625s (Solving: 759.73s 1st Model: 0.07s Unsat: 11.73s)
CPU Time     : 796.728s

Choices      : 14965365 (Domain: 14715389)
Conflicts    : 792908   (Analyzed: 792904)
Restarts     : 9372     (Average: 84.60 Last: 175)
Model-Level  : 251.0   
Problems     : 98       (Average Length: 93.68 Splits: 0)
Lemmas       : 792904   (Deleted: 749033)
  Binary     : 15063    (Ratio:   1.90%)
  Ternary    : 3255     (Ratio:   0.41%)
  Conflict   : 792904   (Average Length:  532.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 792904   (Average: 16.99 Max: 1251 Sum: 13475352)
  Executed   : 792763   (Average: 16.99 Max: 1251 Sum: 13467837 Ratio:  99.94%)
  Bounded    : 141      (Average: 53.30 Max: 122 Sum:   7515 Ratio:   0.06%)

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

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

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

Iteration 98
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        : 99
Time         : 808.948s (Solving: 771.88s 1st Model: 0.07s Unsat: 11.73s)
CPU Time     : 809.056s

Choices      : 15007662 (Domain: 14757686)
Conflicts    : 801451   (Analyzed: 801447)
Restarts     : 9472     (Average: 84.61 Last: 175)
Model-Level  : 251.0   
Problems     : 99       (Average Length: 93.97 Splits: 0)
Lemmas       : 801447   (Deleted: 755408)
  Binary     : 15082    (Ratio:   1.88%)
  Ternary    : 3261     (Ratio:   0.41%)
  Conflict   : 801447   (Average Length:  541.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 801447   (Average: 16.85 Max: 1251 Sum: 13502815)
  Executed   : 801306   (Average: 16.84 Max: 1251 Sum: 13495300 Ratio:  99.94%)
  Bounded    : 141      (Average: 53.30 Max: 122 Sum:   7515 Ratio:   0.06%)

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

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

[endof: stats after solve call]
Solving Time:	 12.27s
Memory:		 951MB (+0MB)
UNKNOWN
Iteration Time:	 12.33s

Iteration 99
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        : 100
Time         : 814.343s (Solving: 777.09s 1st Model: 0.07s Unsat: 11.73s)
CPU Time     : 814.452s

Choices      : 15064033 (Domain: 14814057)
Conflicts    : 809315   (Analyzed: 809311)
Restarts     : 9572     (Average: 84.55 Last: 175)
Model-Level  : 251.0   
Problems     : 100      (Average Length: 94.25 Splits: 0)
Lemmas       : 809311   (Deleted: 763810)
  Binary     : 15137    (Ratio:   1.87%)
  Ternary    : 3265     (Ratio:   0.40%)
  Conflict   : 809311   (Average Length:  543.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 809311   (Average: 16.74 Max: 1251 Sum: 13544713)
  Executed   : 809170   (Average: 16.73 Max: 1251 Sum: 13537198 Ratio:  99.94%)
  Bounded    : 141      (Average: 53.30 Max: 122 Sum:   7515 Ratio:   0.06%)

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

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

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

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

Models       : 0+
Calls        : 101
Time         : 820.053s (Solving: 782.59s 1st Model: 0.07s Unsat: 11.73s)
CPU Time     : 820.164s

Choices      : 15122775 (Domain: 14872505)
Conflicts    : 817152   (Analyzed: 817148)
Restarts     : 9672     (Average: 84.49 Last: 175)
Model-Level  : 251.0   
Problems     : 101      (Average Length: 94.52 Splits: 0)
Lemmas       : 817148   (Deleted: 771503)
  Binary     : 15204    (Ratio:   1.86%)
  Ternary    : 3276     (Ratio:   0.40%)
  Conflict   : 817148   (Average Length:  543.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 817148   (Average: 16.63 Max: 1251 Sum: 13589349)
  Executed   : 817007   (Average: 16.62 Max: 1251 Sum: 13581834 Ratio:  99.94%)
  Bounded    : 141      (Average: 53.30 Max: 122 Sum:   7515 Ratio:   0.06%)

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

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

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

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

Models       : 0+
Calls        : 102
Time         : 825.353s (Solving: 787.70s 1st Model: 0.07s Unsat: 11.73s)
CPU Time     : 825.464s

Choices      : 15190386 (Domain: 14939890)
Conflicts    : 825719   (Analyzed: 825715)
Restarts     : 9772     (Average: 84.50 Last: 175)
Model-Level  : 251.0   
Problems     : 102      (Average Length: 94.79 Splits: 0)
Lemmas       : 825715   (Deleted: 779081)
  Binary     : 15222    (Ratio:   1.84%)
  Ternary    : 3277     (Ratio:   0.40%)
  Conflict   : 825715   (Average Length:  541.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 825715   (Average: 16.53 Max: 1251 Sum: 13646282)
  Executed   : 825574   (Average: 16.52 Max: 1251 Sum: 13638767 Ratio:  99.94%)
  Bounded    : 141      (Average: 53.30 Max: 122 Sum:   7515 Ratio:   0.06%)

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

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

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

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

Models       : 0+
Calls        : 103
Time         : 832.837s (Solving: 795.00s 1st Model: 0.07s Unsat: 11.73s)
CPU Time     : 832.952s

Choices      : 15274880 (Domain: 15023207)
Conflicts    : 834297   (Analyzed: 834293)
Restarts     : 9872     (Average: 84.51 Last: 175)
Model-Level  : 251.0   
Problems     : 103      (Average Length: 95.06 Splits: 0)
Lemmas       : 834293   (Deleted: 787437)
  Binary     : 15292    (Ratio:   1.83%)
  Ternary    : 3293     (Ratio:   0.39%)
  Conflict   : 834293   (Average Length:  540.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 834293   (Average: 16.44 Max: 1251 Sum: 13716372)
  Executed   : 834152   (Average: 16.43 Max: 1251 Sum: 13708857 Ratio:  99.95%)
  Bounded    : 141      (Average: 53.30 Max: 122 Sum:   7515 Ratio:   0.05%)

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

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

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

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

Models       : 0+
Calls        : 104
Time         : 840.410s (Solving: 802.36s 1st Model: 0.07s Unsat: 11.73s)
CPU Time     : 840.528s

Choices      : 15372997 (Domain: 15121000)
Conflicts    : 843061   (Analyzed: 843057)
Restarts     : 9972     (Average: 84.54 Last: 175)
Model-Level  : 251.0   
Problems     : 104      (Average Length: 95.32 Splits: 0)
Lemmas       : 843057   (Deleted: 797996)
  Binary     : 15355    (Ratio:   1.82%)
  Ternary    : 3305     (Ratio:   0.39%)
  Conflict   : 843057   (Average Length:  539.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 843057   (Average: 16.37 Max: 1251 Sum: 13798070)
  Executed   : 842916   (Average: 16.36 Max: 1251 Sum: 13790555 Ratio:  99.95%)
  Bounded    : 141      (Average: 53.30 Max: 122 Sum:   7515 Ratio:   0.05%)

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

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

[endof: stats after solve call]
Solving Time:	 7.49s
Memory:		 951MB (+0MB)
UNKNOWN
Iteration Time:	 7.58s

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

Models       : 0+
Calls        : 105
Time         : 848.750s (Solving: 810.52s 1st Model: 0.07s Unsat: 11.73s)
CPU Time     : 848.872s

Choices      : 15494748 (Domain: 15242114)
Conflicts    : 852032   (Analyzed: 852028)
Restarts     : 10072    (Average: 84.59 Last: 175)
Model-Level  : 251.0   
Problems     : 105      (Average Length: 95.57 Splits: 0)
Lemmas       : 852028   (Deleted: 806503)
  Binary     : 15417    (Ratio:   1.81%)
  Ternary    : 3320     (Ratio:   0.39%)
  Conflict   : 852028   (Average Length:  540.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 852028   (Average: 16.31 Max: 1251 Sum: 13899546)
  Executed   : 851887   (Average: 16.30 Max: 1251 Sum: 13892031 Ratio:  99.95%)
  Bounded    : 141      (Average: 53.30 Max: 122 Sum:   7515 Ratio:   0.05%)

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

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

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

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

Models       : 0+
Calls        : 106
Time         : 858.788s (Solving: 820.38s 1st Model: 0.07s Unsat: 11.73s)
CPU Time     : 858.916s

Choices      : 15654408 (Domain: 15401376)
Conflicts    : 861696   (Analyzed: 861692)
Restarts     : 10172    (Average: 84.71 Last: 175)
Model-Level  : 251.0   
Problems     : 106      (Average Length: 95.82 Splits: 0)
Lemmas       : 861692   (Deleted: 815289)
  Binary     : 15459    (Ratio:   1.79%)
  Ternary    : 3334     (Ratio:   0.39%)
  Conflict   : 861692   (Average Length:  541.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 861692   (Average: 16.29 Max: 1251 Sum: 14037007)
  Executed   : 861551   (Average: 16.28 Max: 1251 Sum: 14029492 Ratio:  99.95%)
  Bounded    : 141      (Average: 53.30 Max: 122 Sum:   7515 Ratio:   0.05%)

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

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

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

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

Models       : 0+
Calls        : 107
Time         : 865.664s (Solving: 827.09s 1st Model: 0.07s Unsat: 11.73s)
CPU Time     : 865.796s

Choices      : 15772191 (Domain: 15518880)
Conflicts    : 870232   (Analyzed: 870228)
Restarts     : 10272    (Average: 84.72 Last: 175)
Model-Level  : 251.0   
Problems     : 107      (Average Length: 96.07 Splits: 0)
Lemmas       : 870228   (Deleted: 822590)
  Binary     : 15473    (Ratio:   1.78%)
  Ternary    : 3353     (Ratio:   0.39%)
  Conflict   : 870228   (Average Length:  539.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 870228   (Average: 16.24 Max: 1251 Sum: 14135261)
  Executed   : 870087   (Average: 16.23 Max: 1251 Sum: 14127746 Ratio:  99.95%)
  Bounded    : 141      (Average: 53.30 Max: 122 Sum:   7515 Ratio:   0.05%)

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

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

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

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

Models       : 0+
Calls        : 108
Time         : 874.352s (Solving: 835.60s 1st Model: 0.07s Unsat: 11.73s)
CPU Time     : 874.484s

Choices      : 15910592 (Domain: 15657216)
Conflicts    : 878853   (Analyzed: 878849)
Restarts     : 10372    (Average: 84.73 Last: 175)
Model-Level  : 251.0   
Problems     : 108      (Average Length: 96.31 Splits: 0)
Lemmas       : 878849   (Deleted: 833073)
  Binary     : 15500    (Ratio:   1.76%)
  Ternary    : 3364     (Ratio:   0.38%)
  Conflict   : 878849   (Average Length:  540.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 878849   (Average: 16.21 Max: 1251 Sum: 14248228)
  Executed   : 878708   (Average: 16.20 Max: 1251 Sum: 14240713 Ratio:  99.95%)
  Bounded    : 141      (Average: 53.30 Max: 122 Sum:   7515 Ratio:   0.05%)

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

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

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

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

Models       : 0+
Calls        : 109
Time         : 881.451s (Solving: 842.51s 1st Model: 0.07s Unsat: 11.73s)
CPU Time     : 881.584s

Choices      : 15955076 (Domain: 15701700)
Conflicts    : 886877   (Analyzed: 886873)
Restarts     : 10472    (Average: 84.69 Last: 175)
Model-Level  : 251.0   
Problems     : 109      (Average Length: 96.54 Splits: 0)
Lemmas       : 886873   (Deleted: 839363)
  Binary     : 15547    (Ratio:   1.75%)
  Ternary    : 3369     (Ratio:   0.38%)
  Conflict   : 886873   (Average Length:  541.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 886873   (Average: 16.10 Max: 1251 Sum: 14282515)
  Executed   : 886732   (Average: 16.10 Max: 1251 Sum: 14275000 Ratio:  99.95%)
  Bounded    : 141      (Average: 53.30 Max: 122 Sum:   7515 Ratio:   0.05%)

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

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

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

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

Models       : 0+
Calls        : 110
Time         : 887.574s (Solving: 848.41s 1st Model: 0.07s Unsat: 11.73s)
CPU Time     : 887.712s

Choices      : 16017591 (Domain: 15764215)
Conflicts    : 895202   (Analyzed: 895198)
Restarts     : 10572    (Average: 84.68 Last: 175)
Model-Level  : 251.0   
Problems     : 110      (Average Length: 96.77 Splits: 0)
Lemmas       : 895198   (Deleted: 847259)
  Binary     : 15578    (Ratio:   1.74%)
  Ternary    : 3386     (Ratio:   0.38%)
  Conflict   : 895198   (Average Length:  541.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 895198   (Average: 16.01 Max: 1251 Sum: 14331417)
  Executed   : 895057   (Average: 16.00 Max: 1251 Sum: 14323902 Ratio:  99.95%)
  Bounded    : 141      (Average: 53.30 Max: 122 Sum:   7515 Ratio:   0.05%)

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

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

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

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

INTERRUPTED  : 1

Models       : 0+
Calls        : 111
Time         : 893.084s (Solving: 853.74s 1st Model: 0.07s Unsat: 11.73s)
CPU Time     : 893.204s

Choices      : 16072168 (Domain: 15818777)
Conflicts    : 902178   (Analyzed: 902174)
Restarts     : 10652    (Average: 84.70 Last: 175)
Model-Level  : 251.0   
Problems     : 111      (Average Length: 97.00 Splits: 0)
Lemmas       : 902174   (Deleted: 855390)
  Binary     : 15640    (Ratio:   1.73%)
  Ternary    : 3406     (Ratio:   0.38%)
  Conflict   : 902174   (Average Length:  541.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 902174   (Average: 15.93 Max: 1251 Sum: 14373564)
  Executed   : 902033   (Average: 15.92 Max: 1251 Sum: 14366049 Ratio:  99.95%)
  Bounded    : 141      (Average: 53.30 Max: 122 Sum:   7515 Ratio:   0.05%)

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

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


