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-5.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-5.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.030s CPU, 0.041s wall-clock]
Preparing model... [0.030s CPU, 0.022s wall-clock]
Generated 115 rules.
Computing model... [0.370s CPU, 0.373s wall-clock]
2300 relevant atoms
2393 auxiliary atoms
4693 final queue length
8087 total queue pushes
Completing instantiation... [0.690s CPU, 0.690s wall-clock]
Instantiating: [1.130s CPU, 1.139s wall-clock]
Computing fact groups...
Finding invariants...
24 initial candidates
Finding invariants: [0.130s CPU, 0.131s wall-clock]
Checking invariant weight... [0.000s CPU, 0.001s wall-clock]
Instantiating groups... [0.010s CPU, 0.007s wall-clock]
Collecting mutex groups... [0.000s CPU, 0.001s wall-clock]
Choosing groups...
238 uncovered facts
Choosing groups: [0.010s CPU, 0.001s wall-clock]
Building translation key... [0.010s CPU, 0.009s wall-clock]
Computing fact groups: [0.170s CPU, 0.167s wall-clock]
Building STRIPS to SAS dictionary... [0.000s CPU, 0.002s wall-clock]
Building dictionary for full mutex groups... [0.000s CPU, 0.002s wall-clock]
Building mutex information...
Building mutex information: [0.010s CPU, 0.003s wall-clock]
Translating task...
Processing axioms...
Simplifying axioms... [0.000s CPU, 0.000s wall-clock]
Processing axioms: [0.030s CPU, 0.039s wall-clock]
Translating task: [0.730s CPU, 0.730s wall-clock]
2672 effect conditions simplified
0 implied preconditions added
Detecting unreachable propositions...
0 operators removed
0 axioms removed
3 propositions removed
Detecting unreachable propositions: [0.360s CPU, 0.357s wall-clock]
Reordering and filtering variables...
241 of 241 variables necessary.
12 of 15 mutex groups necessary.
1596 of 1596 operators necessary.
0 of 0 axiom rules necessary.
Reordering and filtering variables: [0.240s CPU, 0.242s wall-clock]
Translator variables: 241
Translator derived variables: 0
Translator facts: 505
Translator goal facts: 10
Translator mutex groups: 12
Translator total mutex groups size: 36
Translator operators: 1596
Translator axioms: 0
Translator task size: 15302
Translator peak memory: 45004 KB
Writing output... [0.300s CPU, 0.321s wall-clock]
Done! [2.990s CPU, 3.026s wall-clock]
planner.py version 0.0.1

Time:	 0.61s
Memory: 91MB

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

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

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

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

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

Choices      : 367      (Domain: 28)
Conflicts    : 8        (Analyzed: 8)
Restarts     : 0       
Model-Level  : 115.0   
Problems     : 2        (Average Length: 4.50 Splits: 0)
Lemmas       : 8        (Deleted: 0)
  Binary     : 6        (Ratio:  75.00%)
  Ternary    : 0        (Ratio:   0.00%)
  Conflict   : 8        (Average Length:   10.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 8        (Average: 32.62 Max:  84 Sum:    261)
  Executed   : 6        (Average: 32.38 Max:  84 Sum:    259 Ratio:  99.23%)
  Bounded    : 2        (Average:  1.00 Max:   1 Sum:      2 Ratio:   0.77%)

Rules        : 44183   
Atoms        : 44183   
Bodies       : 1        (Original: 0)
Tight        : Yes
Variables    : 11842    (Eliminated:    0 Frozen:  130)
Constraints  : 40811    (Binary:  95.1% Ternary:   3.4% Other:   1.4%)

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

[endof: stats after solve call]
Solving Time:	 0.02s
Memory:		 165MB (+2MB)
SAT
Testing...
NOT SERIALIZABLE
Testing Time:	 0.62s
Memory:		 188MB (+23MB)
Solving...
[start: stats after solve call]

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

Choices      : 368      (Domain: 28)
Conflicts    : 10       (Analyzed: 9)
Restarts     : 0       
Model-Level  : 115.0   
Problems     : 3        (Average Length: 5.33 Splits: 0)
Lemmas       : 9        (Deleted: 0)
  Binary     : 7        (Ratio:  77.78%)
  Ternary    : 0        (Ratio:   0.00%)
  Conflict   : 9        (Average Length:    9.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 9        (Average: 29.22 Max:  84 Sum:    263)
  Executed   : 6        (Average: 28.89 Max:  84 Sum:    260 Ratio:  98.86%)
  Bounded    : 3        (Average:  1.00 Max:   1 Sum:      3 Ratio:   1.14%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 14564    (Eliminated:    0 Frozen: 3202)
Constraints  : 60980    (Binary:  92.3% Ternary:   5.5% Other:   2.3%)

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

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

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

Models       : 0
Calls        : 4
Time         : 2.227s (Solving: 0.64s 1st Model: 0.00s Unsat: 0.64s)
CPU Time     : 2.128s

Choices      : 20428    (Domain: 19268)
Conflicts    : 2400     (Analyzed: 2398)
Restarts     : 30       (Average: 79.93 Last: 10)
Model-Level  : 115.0   
Problems     : 4        (Average Length: 7.00 Splits: 0)
Lemmas       : 2398     (Deleted: 589)
  Binary     : 334      (Ratio:  13.93%)
  Ternary    : 293      (Ratio:  12.22%)
  Conflict   : 2398     (Average Length:   30.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 2398     (Average:  8.56 Max:  84 Sum:  20522)
  Executed   : 2365     (Average:  8.42 Max:  84 Sum:  20181 Ratio:  98.34%)
  Bounded    : 33       (Average: 10.33 Max:  12 Sum:    341 Ratio:   1.66%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 40960    (Eliminated:    0 Frozen: 11742)
Constraints  : 262050   (Binary:  91.6% Ternary:   6.4% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 0.66s
Memory:		 197MB (+9MB)
UNSAT
Iteration Time:	 1.13s

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

Models       : 0
Calls        : 5
Time         : 5.613s (Solving: 3.47s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 5.516s

Choices      : 83668    (Domain: 80839)
Conflicts    : 9035     (Analyzed: 9032)
Restarts     : 102      (Average: 88.55 Last: 20)
Model-Level  : 115.0   
Problems     : 5        (Average Length: 9.00 Splits: 0)
Lemmas       : 9032     (Deleted: 4942)
  Binary     : 1008     (Ratio:  11.16%)
  Ternary    : 545      (Ratio:   6.03%)
  Conflict   : 9032     (Average Length:  125.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 9032     (Average:  9.18 Max:  95 Sum:  82898)
  Executed   : 8982     (Average:  9.11 Max:  95 Sum:  82286 Ratio:  99.26%)
  Bounded    : 50       (Average: 12.24 Max:  17 Sum:    612 Ratio:   0.74%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 67356    (Eliminated:    0 Frozen: 20282)
Constraints  : 425655   (Binary:  91.7% Ternary:   6.4% Other:   2.0%)

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

[endof: stats after solve call]
Solving Time:	 2.86s
Memory:		 216MB (+13MB)
UNSAT
Iteration Time:	 3.40s

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

Models       : 0+
Calls        : 6
Time         : 11.145s (Solving: 8.41s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 11.048s

Choices      : 194835   (Domain: 179881)
Conflicts    : 18138    (Analyzed: 18135)
Restarts     : 202      (Average: 89.78 Last: 101)
Model-Level  : 115.0   
Problems     : 6        (Average Length: 11.17 Splits: 0)
Lemmas       : 18135    (Deleted: 12424)
  Binary     : 1624     (Ratio:   8.96%)
  Ternary    : 778      (Ratio:   4.29%)
  Conflict   : 18135    (Average Length:  297.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 18135    (Average: 10.37 Max: 302 Sum: 188090)
  Executed   : 18076    (Average: 10.33 Max: 302 Sum: 187289 Ratio:  99.57%)
  Bounded    : 59       (Average: 13.58 Max:  22 Sum:    801 Ratio:   0.43%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 93752    (Eliminated:    0 Frozen: 28822)
Constraints  : 621350   (Binary:  91.6% Ternary:   6.5% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 4.97s
Memory:		 239MB (+16MB)
UNKNOWN
Iteration Time:	 5.54s

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

Models       : 0+
Calls        : 7
Time         : 17.906s (Solving: 14.59s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 17.812s

Choices      : 327156   (Domain: 302805)
Conflicts    : 26901    (Analyzed: 26898)
Restarts     : 302      (Average: 89.07 Last: 101)
Model-Level  : 115.0   
Problems     : 7        (Average Length: 13.43 Splits: 0)
Lemmas       : 26898    (Deleted: 18459)
  Binary     : 2330     (Ratio:   8.66%)
  Ternary    : 962      (Ratio:   3.58%)
  Conflict   : 26898    (Average Length:  278.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 26898    (Average: 11.69 Max: 357 Sum: 314445)
  Executed   : 26829    (Average: 11.65 Max: 357 Sum: 313374 Ratio:  99.66%)
  Bounded    : 69       (Average: 15.52 Max:  27 Sum:   1071 Ratio:   0.34%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 120148   (Eliminated:    0 Frozen: 37362)
Constraints  : 815724   (Binary:  91.6% Ternary:   6.5% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 6.22s
Memory:		 253MB (+9MB)
UNKNOWN
Iteration Time:	 6.77s

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

Models       : 0+
Calls        : 8
Time         : 25.353s (Solving: 21.36s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 25.264s

Choices      : 455849   (Domain: 424072)
Conflicts    : 36045    (Analyzed: 36042)
Restarts     : 402      (Average: 89.66 Last: 101)
Model-Level  : 115.0   
Problems     : 8        (Average Length: 15.75 Splits: 0)
Lemmas       : 36042    (Deleted: 26452)
  Binary     : 2666     (Ratio:   7.40%)
  Ternary    : 1049     (Ratio:   2.91%)
  Conflict   : 36042    (Average Length:  306.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 36042    (Average: 12.05 Max: 357 Sum: 434442)
  Executed   : 35970    (Average: 12.02 Max: 357 Sum: 433275 Ratio:  99.73%)
  Bounded    : 72       (Average: 16.21 Max:  32 Sum:   1167 Ratio:   0.27%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 146544   (Eliminated:    0 Frozen: 45902)
Constraints  : 1012058  (Binary:  91.6% Ternary:   6.5% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 6.81s
Memory:		 291MB (+24MB)
UNKNOWN
Iteration Time:	 7.46s

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

Models       : 0+
Calls        : 9
Time         : 29.288s (Solving: 25.26s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 29.204s

Choices      : 495709   (Domain: 462324)
Conflicts    : 43610    (Analyzed: 43607)
Restarts     : 502      (Average: 86.87 Last: 101)
Model-Level  : 115.0   
Problems     : 9        (Average Length: 17.56 Splits: 0)
Lemmas       : 43607    (Deleted: 34188)
  Binary     : 2830     (Ratio:   6.49%)
  Ternary    : 1098     (Ratio:   2.52%)
  Conflict   : 43607    (Average Length:  347.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 43607    (Average: 10.73 Max: 357 Sum: 467733)
  Executed   : 43535    (Average: 10.70 Max: 357 Sum: 466566 Ratio:  99.75%)
  Bounded    : 72       (Average: 16.21 Max:  32 Sum:   1167 Ratio:   0.25%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 146544   (Eliminated:    0 Frozen: 45902)
Constraints  : 1012016  (Binary:  91.6% Ternary:   6.5% Other:   1.9%)

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

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

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

Models       : 0+
Calls        : 10
Time         : 34.868s (Solving: 30.80s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 34.784s

Choices      : 585465   (Domain: 547882)
Conflicts    : 52309    (Analyzed: 52306)
Restarts     : 602      (Average: 86.89 Last: 101)
Model-Level  : 115.0   
Problems     : 10       (Average Length: 19.00 Splits: 0)
Lemmas       : 52306    (Deleted: 41407)
  Binary     : 3164     (Ratio:   6.05%)
  Ternary    : 1154     (Ratio:   2.21%)
  Conflict   : 52306    (Average Length:  342.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 52306    (Average: 10.49 Max: 357 Sum: 548691)
  Executed   : 52232    (Average: 10.47 Max: 357 Sum: 547465 Ratio:  99.78%)
  Bounded    : 74       (Average: 16.57 Max:  32 Sum:   1226 Ratio:   0.22%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 146544   (Eliminated:    0 Frozen: 45902)
Constraints  : 1012016  (Binary:  91.6% Ternary:   6.5% Other:   1.9%)

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

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

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

Models       : 0+
Calls        : 11
Time         : 40.323s (Solving: 36.23s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 40.240s

Choices      : 678499   (Domain: 638387)
Conflicts    : 61022    (Analyzed: 61019)
Restarts     : 702      (Average: 86.92 Last: 101)
Model-Level  : 115.0   
Problems     : 11       (Average Length: 20.18 Splits: 0)
Lemmas       : 61019    (Deleted: 49566)
  Binary     : 3372     (Ratio:   5.53%)
  Ternary    : 1184     (Ratio:   1.94%)
  Conflict   : 61019    (Average Length:  343.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 61019    (Average: 10.37 Max: 357 Sum: 632788)
  Executed   : 60943    (Average: 10.35 Max: 357 Sum: 631498 Ratio:  99.80%)
  Bounded    : 76       (Average: 16.97 Max:  32 Sum:   1290 Ratio:   0.20%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 146544   (Eliminated:    0 Frozen: 45902)
Constraints  : 1012003  (Binary:  91.6% Ternary:   6.5% Other:   1.9%)

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

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

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

Models       : 0+
Calls        : 12
Time         : 45.860s (Solving: 41.12s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 45.780s

Choices      : 779563   (Domain: 736842)
Conflicts    : 69781    (Analyzed: 69778)
Restarts     : 802      (Average: 87.00 Last: 101)
Model-Level  : 115.0   
Problems     : 12       (Average Length: 21.58 Splits: 0)
Lemmas       : 69778    (Deleted: 57819)
  Binary     : 3502     (Ratio:   5.02%)
  Ternary    : 1233     (Ratio:   1.77%)
  Conflict   : 69778    (Average Length:  342.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 69778    (Average: 10.38 Max: 357 Sum: 724277)
  Executed   : 69699    (Average: 10.36 Max: 357 Sum: 722876 Ratio:  99.81%)
  Bounded    : 79       (Average: 17.73 Max:  37 Sum:   1401 Ratio:   0.19%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 172940   (Eliminated:    0 Frozen: 54442)
Constraints  : 1210969  (Binary:  91.5% Ternary:   6.6% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 4.94s
Memory:		 301MB (+10MB)
UNKNOWN
Iteration Time:	 5.55s

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

Models       : 0+
Calls        : 13
Time         : 51.131s (Solving: 45.74s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 51.052s

Choices      : 867707   (Domain: 823138)
Conflicts    : 78104    (Analyzed: 78101)
Restarts     : 902      (Average: 86.59 Last: 107)
Model-Level  : 115.0   
Problems     : 13       (Average Length: 23.15 Splits: 0)
Lemmas       : 78101    (Deleted: 64093)
  Binary     : 3639     (Ratio:   4.66%)
  Ternary    : 1263     (Ratio:   1.62%)
  Conflict   : 78101    (Average Length:  339.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 78101    (Average: 10.28 Max: 357 Sum: 802547)
  Executed   : 78022    (Average: 10.26 Max: 357 Sum: 801146 Ratio:  99.83%)
  Bounded    : 79       (Average: 17.73 Max:  37 Sum:   1401 Ratio:   0.17%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 199336   (Eliminated:    0 Frozen: 62982)
Constraints  : 1411993  (Binary:  91.5% Ternary:   6.6% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 4.67s
Memory:		 320MB (+13MB)
UNKNOWN
Iteration Time:	 5.28s

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

Models       : 0+
Calls        : 14
Time         : 56.198s (Solving: 50.12s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 56.112s

Choices      : 979870   (Domain: 934167)
Conflicts    : 86377    (Analyzed: 86374)
Restarts     : 1002     (Average: 86.20 Last: 110)
Model-Level  : 115.0   
Problems     : 14       (Average Length: 24.86 Splits: 0)
Lemmas       : 86374    (Deleted: 71864)
  Binary     : 3834     (Ratio:   4.44%)
  Ternary    : 1306     (Ratio:   1.51%)
  Conflict   : 86374    (Average Length:  327.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 86374    (Average: 10.49 Max: 423 Sum: 906136)
  Executed   : 86293    (Average: 10.47 Max: 423 Sum: 904651 Ratio:  99.84%)
  Bounded    : 81       (Average: 18.33 Max:  42 Sum:   1485 Ratio:   0.16%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 225732   (Eliminated:    0 Frozen: 71522)
Constraints  : 1613063  (Binary:  91.5% Ternary:   6.6% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 4.43s
Memory:		 354MB (+28MB)
UNKNOWN
Iteration Time:	 5.07s

Iteration 14
Queue:		 [(10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True), (17,85,0,True)]
Grounded Until:	 45
Expected Memory: 392.0MB
Grounding...	 [('step', [46]), ('step', [47]), ('step', [48]), ('step', [49]), ('step', [50]), ('check', [50])]
Grounding Time:	 0.37s
Memory:		 354MB (+0MB)
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 15
Time         : 61.629s (Solving: 54.90s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 61.544s

Choices      : 1103188  (Domain: 1055956)
Conflicts    : 94165    (Analyzed: 94162)
Restarts     : 1102     (Average: 85.45 Last: 110)
Model-Level  : 115.0   
Problems     : 15       (Average Length: 26.67 Splits: 0)
Lemmas       : 94162    (Deleted: 79983)
  Binary     : 3911     (Ratio:   4.15%)
  Ternary    : 1326     (Ratio:   1.41%)
  Conflict   : 94162    (Average Length:  331.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 94162    (Average: 10.79 Max: 423 Sum: 1016477)
  Executed   : 94081    (Average: 10.78 Max: 423 Sum: 1014992 Ratio:  99.85%)
  Bounded    : 81       (Average: 18.33 Max:  42 Sum:   1485 Ratio:   0.15%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 252128   (Eliminated:    0 Frozen: 80062)
Constraints  : 1814133  (Binary:  91.5% Ternary:   6.6% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 4.83s
Memory:		 362MB (+8MB)
UNKNOWN
Iteration Time:	 5.44s

Iteration 15
Queue:		 [(11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True), (17,85,0,True)]
Grounded Until:	 50
Expected Memory: 400.0MB
Grounding...	 [('step', [51]), ('step', [52]), ('step', [53]), ('step', [54]), ('step', [55]), ('check', [55])]
Grounding Time:	 0.38s
Memory:		 367MB (+5MB)
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 16
Time         : 67.229s (Solving: 59.82s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 67.148s

Choices      : 1220676  (Domain: 1172081)
Conflicts    : 102486   (Analyzed: 102483)
Restarts     : 1202     (Average: 85.26 Last: 110)
Model-Level  : 115.0   
Problems     : 16       (Average Length: 28.56 Splits: 0)
Lemmas       : 102483   (Deleted: 87348)
  Binary     : 4006     (Ratio:   3.91%)
  Ternary    : 1342     (Ratio:   1.31%)
  Conflict   : 102483   (Average Length:  327.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 102483   (Average: 10.95 Max: 533 Sum: 1122544)
  Executed   : 102399   (Average: 10.94 Max: 533 Sum: 1120893 Ratio:  99.85%)
  Bounded    : 84       (Average: 19.65 Max:  57 Sum:   1651 Ratio:   0.15%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 278524   (Eliminated:    0 Frozen: 88602)
Constraints  : 2015203  (Binary:  91.5% Ternary:   6.6% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 4.99s
Memory:		 382MB (+15MB)
UNKNOWN
Iteration Time:	 5.61s

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

Models       : 0+
Calls        : 17
Time         : 72.326s (Solving: 64.21s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 72.248s

Choices      : 1366534  (Domain: 1315690)
Conflicts    : 110475   (Analyzed: 110472)
Restarts     : 1302     (Average: 84.85 Last: 110)
Model-Level  : 115.0   
Problems     : 17       (Average Length: 30.53 Splits: 0)
Lemmas       : 110472   (Deleted: 95163)
  Binary     : 4123     (Ratio:   3.73%)
  Ternary    : 1359     (Ratio:   1.23%)
  Conflict   : 110472   (Average Length:  325.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 110472   (Average: 11.37 Max: 533 Sum: 1256134)
  Executed   : 110386   (Average: 11.35 Max: 533 Sum: 1254364 Ratio:  99.86%)
  Bounded    : 86       (Average: 20.58 Max:  62 Sum:   1770 Ratio:   0.14%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 304920   (Eliminated:    0 Frozen: 97142)
Constraints  : 2216234  (Binary:  91.5% Ternary:   6.6% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 4.45s
Memory:		 400MB (+17MB)
UNKNOWN
Iteration Time:	 5.11s

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

Models       : 0+
Calls        : 18
Time         : 78.486s (Solving: 69.64s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 78.412s

Choices      : 1582259  (Domain: 1528281)
Conflicts    : 119385   (Analyzed: 119382)
Restarts     : 1402     (Average: 85.15 Last: 110)
Model-Level  : 115.0   
Problems     : 18       (Average Length: 32.56 Splits: 0)
Lemmas       : 119382   (Deleted: 104860)
  Binary     : 4250     (Ratio:   3.56%)
  Ternary    : 1388     (Ratio:   1.16%)
  Conflict   : 119382   (Average Length:  332.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 119382   (Average: 12.19 Max: 533 Sum: 1455416)
  Executed   : 119296   (Average: 12.18 Max: 533 Sum: 1453646 Ratio:  99.88%)
  Bounded    : 86       (Average: 20.58 Max:  62 Sum:   1770 Ratio:   0.12%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 331316   (Eliminated:    0 Frozen: 105682)
Constraints  : 2413082  (Binary:  91.5% Ternary:   6.6% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 5.51s
Memory:		 448MB (+44MB)
UNKNOWN
Iteration Time:	 6.17s

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

Models       : 0+
Calls        : 19
Time         : 85.932s (Solving: 76.22s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 85.860s

Choices      : 1785835  (Domain: 1729631)
Conflicts    : 127765   (Analyzed: 127762)
Restarts     : 1502     (Average: 85.06 Last: 110)
Model-Level  : 115.0   
Problems     : 19       (Average Length: 34.63 Splits: 0)
Lemmas       : 127762   (Deleted: 111723)
  Binary     : 4439     (Ratio:   3.47%)
  Ternary    : 1427     (Ratio:   1.12%)
  Conflict   : 127762   (Average Length:  356.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 127762   (Average: 12.82 Max: 641 Sum: 1638063)
  Executed   : 127673   (Average: 12.81 Max: 641 Sum: 1636080 Ratio:  99.88%)
  Bounded    : 89       (Average: 22.28 Max:  72 Sum:   1983 Ratio:   0.12%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 357712   (Eliminated:    0 Frozen: 114222)
Constraints  : 2614152  (Binary:  91.5% Ternary:   6.6% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 6.65s
Memory:		 463MB (+3MB)
UNKNOWN
Iteration Time:	 7.46s

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

Models       : 0+
Calls        : 20
Time         : 93.510s (Solving: 83.07s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 93.440s

Choices      : 2058865  (Domain: 1999152)
Conflicts    : 136710   (Analyzed: 136707)
Restarts     : 1602     (Average: 85.34 Last: 110)
Model-Level  : 115.0   
Problems     : 20       (Average Length: 36.75 Splits: 0)
Lemmas       : 136707   (Deleted: 121778)
  Binary     : 4652     (Ratio:   3.40%)
  Ternary    : 1445     (Ratio:   1.06%)
  Conflict   : 136707   (Average Length:  377.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 136707   (Average: 13.82 Max: 671 Sum: 1889318)
  Executed   : 136616   (Average: 13.80 Max: 671 Sum: 1887181 Ratio:  99.89%)
  Bounded    : 91       (Average: 23.48 Max:  77 Sum:   2137 Ratio:   0.11%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 384108   (Eliminated:    0 Frozen: 122762)
Constraints  : 2815194  (Binary:  91.5% Ternary:   6.6% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 6.93s
Memory:		 476MB (+13MB)
UNKNOWN
Iteration Time:	 7.59s

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

Models       : 0+
Calls        : 21
Time         : 101.077s (Solving: 89.87s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 101.008s

Choices      : 2377079  (Domain: 2314344)
Conflicts    : 145552   (Analyzed: 145549)
Restarts     : 1702     (Average: 85.52 Last: 110)
Model-Level  : 115.0   
Problems     : 21       (Average Length: 38.90 Splits: 0)
Lemmas       : 145549   (Deleted: 129958)
  Binary     : 4745     (Ratio:   3.26%)
  Ternary    : 1465     (Ratio:   1.01%)
  Conflict   : 145549   (Average Length:  382.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 145549   (Average: 15.03 Max: 671 Sum: 2186977)
  Executed   : 145456   (Average: 15.01 Max: 671 Sum: 2184676 Ratio:  99.89%)
  Bounded    : 93       (Average: 24.74 Max:  82 Sum:   2301 Ratio:   0.11%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 410504   (Eliminated:    0 Frozen: 131302)
Constraints  : 3016224  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 6.88s
Memory:		 498MB (+19MB)
UNKNOWN
Iteration Time:	 7.58s

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

Models       : 0+
Calls        : 22
Time         : 106.918s (Solving: 94.94s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 106.852s

Choices      : 2626934  (Domain: 2561282)
Conflicts    : 153897   (Analyzed: 153894)
Restarts     : 1802     (Average: 85.40 Last: 110)
Model-Level  : 115.0   
Problems     : 22       (Average Length: 41.09 Splits: 0)
Lemmas       : 153894   (Deleted: 136518)
  Binary     : 4815     (Ratio:   3.13%)
  Ternary    : 1475     (Ratio:   0.96%)
  Conflict   : 153894   (Average Length:  382.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 153894   (Average: 15.71 Max: 671 Sum: 2418322)
  Executed   : 153801   (Average: 15.70 Max: 671 Sum: 2416021 Ratio:  99.90%)
  Bounded    : 93       (Average: 24.74 Max:  82 Sum:   2301 Ratio:   0.10%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 436900   (Eliminated:    0 Frozen: 139842)
Constraints  : 3217244  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 5.17s
Memory:		 516MB (+18MB)
UNKNOWN
Iteration Time:	 5.86s

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

Models       : 0+
Calls        : 23
Time         : 112.628s (Solving: 100.53s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 112.556s

Choices      : 2666289  (Domain: 2600637)
Conflicts    : 161814   (Analyzed: 161811)
Restarts     : 1902     (Average: 85.07 Last: 110)
Model-Level  : 115.0   
Problems     : 23       (Average Length: 43.09 Splits: 0)
Lemmas       : 161811   (Deleted: 145241)
  Binary     : 4883     (Ratio:   3.02%)
  Ternary    : 1486     (Ratio:   0.92%)
  Conflict   : 161811   (Average Length:  393.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 161811   (Average: 15.14 Max: 671 Sum: 2450229)
  Executed   : 161716   (Average: 15.13 Max: 671 Sum: 2447754 Ratio:  99.90%)
  Bounded    : 95       (Average: 26.05 Max:  87 Sum:   2475 Ratio:   0.10%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 436900   (Eliminated:    0 Frozen: 139842)
Constraints  : 3217244  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 5.66s
Memory:		 517MB (+1MB)
UNKNOWN
Iteration Time:	 5.71s

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

Models       : 0+
Calls        : 24
Time         : 117.957s (Solving: 105.77s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 117.888s

Choices      : 2734738  (Domain: 2666366)
Conflicts    : 171421   (Analyzed: 171418)
Restarts     : 2002     (Average: 85.62 Last: 110)
Model-Level  : 115.0   
Problems     : 24       (Average Length: 44.92 Splits: 0)
Lemmas       : 171418   (Deleted: 154283)
  Binary     : 4986     (Ratio:   2.91%)
  Ternary    : 1509     (Ratio:   0.88%)
  Conflict   : 171418   (Average Length:  394.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 171418   (Average: 14.63 Max: 671 Sum: 2507902)
  Executed   : 171323   (Average: 14.62 Max: 671 Sum: 2505427 Ratio:  99.90%)
  Bounded    : 95       (Average: 26.05 Max:  87 Sum:   2475 Ratio:   0.10%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 436900   (Eliminated:    0 Frozen: 139842)
Constraints  : 3214748  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

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

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

Models       : 0+
Calls        : 25
Time         : 123.006s (Solving: 110.73s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 122.940s

Choices      : 2815441  (Domain: 2743992)
Conflicts    : 180219   (Analyzed: 180216)
Restarts     : 2102     (Average: 85.74 Last: 110)
Model-Level  : 115.0   
Problems     : 25       (Average Length: 46.60 Splits: 0)
Lemmas       : 180216   (Deleted: 163467)
  Binary     : 5101     (Ratio:   2.83%)
  Ternary    : 1532     (Ratio:   0.85%)
  Conflict   : 180216   (Average Length:  400.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 180216   (Average: 14.29 Max: 671 Sum: 2575753)
  Executed   : 180121   (Average: 14.28 Max: 671 Sum: 2573278 Ratio:  99.90%)
  Bounded    : 95       (Average: 26.05 Max:  87 Sum:   2475 Ratio:   0.10%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 436900   (Eliminated:    0 Frozen: 139842)
Constraints  : 3214748  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

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

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

Models       : 0+
Calls        : 26
Time         : 127.926s (Solving: 115.54s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 127.864s

Choices      : 2911485  (Domain: 2837581)
Conflicts    : 188654   (Analyzed: 188651)
Restarts     : 2202     (Average: 85.67 Last: 115)
Model-Level  : 115.0   
Problems     : 26       (Average Length: 48.15 Splits: 0)
Lemmas       : 188651   (Deleted: 170310)
  Binary     : 5219     (Ratio:   2.77%)
  Ternary    : 1536     (Ratio:   0.81%)
  Conflict   : 188651   (Average Length:  407.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 188651   (Average: 14.09 Max: 671 Sum: 2658216)
  Executed   : 188555   (Average: 14.08 Max: 671 Sum: 2655654 Ratio:  99.90%)
  Bounded    : 96       (Average: 26.69 Max:  87 Sum:   2562 Ratio:   0.10%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 436900   (Eliminated:    0 Frozen: 139842)
Constraints  : 3214748  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

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

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

Models       : 0+
Calls        : 27
Time         : 135.092s (Solving: 122.60s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 135.036s

Choices      : 3062444  (Domain: 2980038)
Conflicts    : 197708   (Analyzed: 197705)
Restarts     : 2302     (Average: 85.88 Last: 115)
Model-Level  : 115.0   
Problems     : 27       (Average Length: 49.59 Splits: 0)
Lemmas       : 197705   (Deleted: 179876)
  Binary     : 5554     (Ratio:   2.81%)
  Ternary    : 1614     (Ratio:   0.82%)
  Conflict   : 197705   (Average Length:  427.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 197705   (Average: 14.10 Max: 671 Sum: 2788038)
  Executed   : 197609   (Average: 14.09 Max: 671 Sum: 2785476 Ratio:  99.91%)
  Bounded    : 96       (Average: 26.69 Max:  87 Sum:   2562 Ratio:   0.09%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 436900   (Eliminated:    0 Frozen: 139842)
Constraints  : 3214722  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

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

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

Models       : 0+
Calls        : 28
Time         : 140.467s (Solving: 127.87s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 140.408s

Choices      : 3192312  (Domain: 3107985)
Conflicts    : 206567   (Analyzed: 206564)
Restarts     : 2402     (Average: 86.00 Last: 158)
Model-Level  : 115.0   
Problems     : 28       (Average Length: 50.93 Splits: 0)
Lemmas       : 206564   (Deleted: 188498)
  Binary     : 5755     (Ratio:   2.79%)
  Ternary    : 1656     (Ratio:   0.80%)
  Conflict   : 206564   (Average Length:  433.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 206564   (Average: 14.05 Max: 671 Sum: 2901654)
  Executed   : 206468   (Average: 14.03 Max: 671 Sum: 2899092 Ratio:  99.91%)
  Bounded    : 96       (Average: 26.69 Max:  87 Sum:   2562 Ratio:   0.09%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 436900   (Eliminated:    0 Frozen: 139842)
Constraints  : 3214722  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

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

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

Models       : 0+
Calls        : 29
Time         : 146.792s (Solving: 134.08s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 146.736s

Choices      : 3370471  (Domain: 3279277)
Conflicts    : 215484   (Analyzed: 215481)
Restarts     : 2502     (Average: 86.12 Last: 170)
Model-Level  : 115.0   
Problems     : 29       (Average Length: 52.17 Splits: 0)
Lemmas       : 215481   (Deleted: 196820)
  Binary     : 6004     (Ratio:   2.79%)
  Ternary    : 1741     (Ratio:   0.81%)
  Conflict   : 215481   (Average Length:  441.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 215481   (Average: 14.20 Max: 671 Sum: 3059677)
  Executed   : 215385   (Average: 14.19 Max: 671 Sum: 3057115 Ratio:  99.92%)
  Bounded    : 96       (Average: 26.69 Max:  87 Sum:   2562 Ratio:   0.08%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 436900   (Eliminated:    0 Frozen: 139842)
Constraints  : 3214722  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

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

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

Models       : 0+
Calls        : 30
Time         : 152.466s (Solving: 139.67s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 152.412s

Choices      : 3523031  (Domain: 3430715)
Conflicts    : 224460   (Analyzed: 224457)
Restarts     : 2602     (Average: 86.26 Last: 170)
Model-Level  : 115.0   
Problems     : 30       (Average Length: 53.33 Splits: 0)
Lemmas       : 224457   (Deleted: 205177)
  Binary     : 6136     (Ratio:   2.73%)
  Ternary    : 1758     (Ratio:   0.78%)
  Conflict   : 224457   (Average Length:  442.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 224457   (Average: 14.24 Max: 671 Sum: 3195230)
  Executed   : 224361   (Average: 14.22 Max: 671 Sum: 3192668 Ratio:  99.92%)
  Bounded    : 96       (Average: 26.69 Max:  87 Sum:   2562 Ratio:   0.08%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 436900   (Eliminated:    0 Frozen: 139842)
Constraints  : 3214722  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

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

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

Models       : 0+
Calls        : 31
Time         : 159.614s (Solving: 146.73s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 159.564s

Choices      : 3763227  (Domain: 3660922)
Conflicts    : 233518   (Analyzed: 233515)
Restarts     : 2702     (Average: 86.42 Last: 170)
Model-Level  : 115.0   
Problems     : 31       (Average Length: 54.42 Splits: 0)
Lemmas       : 233515   (Deleted: 213793)
  Binary     : 6399     (Ratio:   2.74%)
  Ternary    : 1833     (Ratio:   0.78%)
  Conflict   : 233515   (Average Length:  451.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 233515   (Average: 14.60 Max: 671 Sum: 3408356)
  Executed   : 233419   (Average: 14.58 Max: 671 Sum: 3405794 Ratio:  99.92%)
  Bounded    : 96       (Average: 26.69 Max:  87 Sum:   2562 Ratio:   0.08%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 436900   (Eliminated:    0 Frozen: 139842)
Constraints  : 3214722  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

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

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

Models       : 0+
Calls        : 32
Time         : 165.808s (Solving: 152.82s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 165.764s

Choices      : 3968183  (Domain: 3865263)
Conflicts    : 242078   (Analyzed: 242075)
Restarts     : 2802     (Average: 86.39 Last: 170)
Model-Level  : 115.0   
Problems     : 32       (Average Length: 55.44 Splits: 0)
Lemmas       : 242075   (Deleted: 220761)
  Binary     : 6554     (Ratio:   2.71%)
  Ternary    : 1852     (Ratio:   0.77%)
  Conflict   : 242075   (Average Length:  453.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 242075   (Average: 14.85 Max: 671 Sum: 3593818)
  Executed   : 241979   (Average: 14.84 Max: 671 Sum: 3591256 Ratio:  99.93%)
  Bounded    : 96       (Average: 26.69 Max:  87 Sum:   2562 Ratio:   0.07%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 436900   (Eliminated:    0 Frozen: 139842)
Constraints  : 3214722  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

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

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

Models       : 0+
Calls        : 33
Time         : 172.520s (Solving: 159.43s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 172.480s

Choices      : 4167486  (Domain: 4063718)
Conflicts    : 250408   (Analyzed: 250405)
Restarts     : 2902     (Average: 86.29 Last: 170)
Model-Level  : 115.0   
Problems     : 33       (Average Length: 56.39 Splits: 0)
Lemmas       : 250405   (Deleted: 228428)
  Binary     : 6708     (Ratio:   2.68%)
  Ternary    : 1869     (Ratio:   0.75%)
  Conflict   : 250405   (Average Length:  456.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 250405   (Average: 15.07 Max: 671 Sum: 3774797)
  Executed   : 250309   (Average: 15.06 Max: 671 Sum: 3772235 Ratio:  99.93%)
  Bounded    : 96       (Average: 26.69 Max:  87 Sum:   2562 Ratio:   0.07%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 436900   (Eliminated:    0 Frozen: 139842)
Constraints  : 3214722  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

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

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

Models       : 0+
Calls        : 34
Time         : 180.578s (Solving: 167.39s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 180.544s

Choices      : 4486419  (Domain: 4380037)
Conflicts    : 259607   (Analyzed: 259604)
Restarts     : 3002     (Average: 86.48 Last: 170)
Model-Level  : 115.0   
Problems     : 34       (Average Length: 57.29 Splits: 0)
Lemmas       : 259604   (Deleted: 238658)
  Binary     : 6852     (Ratio:   2.64%)
  Ternary    : 1890     (Ratio:   0.73%)
  Conflict   : 259604   (Average Length:  464.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 259604   (Average: 15.67 Max: 671 Sum: 4067138)
  Executed   : 259508   (Average: 15.66 Max: 671 Sum: 4064576 Ratio:  99.94%)
  Bounded    : 96       (Average: 26.69 Max:  87 Sum:   2562 Ratio:   0.06%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 436900   (Eliminated:    0 Frozen: 139842)
Constraints  : 3214722  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

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

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

Models       : 0+
Calls        : 35
Time         : 189.102s (Solving: 175.83s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 189.072s

Choices      : 4720405  (Domain: 4608522)
Conflicts    : 268308   (Analyzed: 268305)
Restarts     : 3102     (Average: 86.49 Last: 170)
Model-Level  : 115.0   
Problems     : 35       (Average Length: 58.14 Splits: 0)
Lemmas       : 268305   (Deleted: 247041)
  Binary     : 7140     (Ratio:   2.66%)
  Ternary    : 1925     (Ratio:   0.72%)
  Conflict   : 268305   (Average Length:  488.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 268305   (Average: 15.92 Max: 671 Sum: 4271683)
  Executed   : 268209   (Average: 15.91 Max: 671 Sum: 4269121 Ratio:  99.94%)
  Bounded    : 96       (Average: 26.69 Max:  87 Sum:   2562 Ratio:   0.06%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 436900   (Eliminated:    0 Frozen: 139842)
Constraints  : 3214722  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

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

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

Models       : 0+
Calls        : 36
Time         : 197.636s (Solving: 184.27s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 197.608s

Choices      : 4994690  (Domain: 4881787)
Conflicts    : 277279   (Analyzed: 277276)
Restarts     : 3202     (Average: 86.59 Last: 170)
Model-Level  : 115.0   
Problems     : 36       (Average Length: 58.94 Splits: 0)
Lemmas       : 277276   (Deleted: 255140)
  Binary     : 7259     (Ratio:   2.62%)
  Ternary    : 1953     (Ratio:   0.70%)
  Conflict   : 277276   (Average Length:  492.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 277276   (Average: 16.31 Max: 671 Sum: 4521069)
  Executed   : 277180   (Average: 16.30 Max: 671 Sum: 4518507 Ratio:  99.94%)
  Bounded    : 96       (Average: 26.69 Max:  87 Sum:   2562 Ratio:   0.06%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 436900   (Eliminated:    0 Frozen: 139842)
Constraints  : 3214722  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

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

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

Models       : 0+
Calls        : 37
Time         : 208.934s (Solving: 194.79s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 208.908s

Choices      : 5343023  (Domain: 5228839)
Conflicts    : 287148   (Analyzed: 287145)
Restarts     : 3302     (Average: 86.96 Last: 170)
Model-Level  : 115.0   
Problems     : 37       (Average Length: 59.84 Splits: 0)
Lemmas       : 287145   (Deleted: 263928)
  Binary     : 7392     (Ratio:   2.57%)
  Ternary    : 1987     (Ratio:   0.69%)
  Conflict   : 287145   (Average Length:  506.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 287145   (Average: 16.85 Max: 671 Sum: 4839070)
  Executed   : 287049   (Average: 16.84 Max: 671 Sum: 4836508 Ratio:  99.95%)
  Bounded    : 96       (Average: 26.69 Max:  87 Sum:   2562 Ratio:   0.05%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 463296   (Eliminated:    0 Frozen: 148382)
Constraints  : 3415792  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 10.62s
Memory:		 534MB (+17MB)
UNKNOWN
Iteration Time:	 11.31s

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

Models       : 0+
Calls        : 38
Time         : 218.549s (Solving: 203.58s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 218.528s

Choices      : 5669012  (Domain: 5553843)
Conflicts    : 296063   (Analyzed: 296060)
Restarts     : 3402     (Average: 87.03 Last: 170)
Model-Level  : 115.0   
Problems     : 38       (Average Length: 60.82 Splits: 0)
Lemmas       : 296060   (Deleted: 273205)
  Binary     : 7498     (Ratio:   2.53%)
  Ternary    : 2002     (Ratio:   0.68%)
  Conflict   : 296060   (Average Length:  512.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 296060   (Average: 17.35 Max: 671 Sum: 5136959)
  Executed   : 295964   (Average: 17.34 Max: 671 Sum: 5134397 Ratio:  99.95%)
  Bounded    : 96       (Average: 26.69 Max:  87 Sum:   2562 Ratio:   0.05%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 489692   (Eliminated:    0 Frozen: 156922)
Constraints  : 3616862  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 8.89s
Memory:		 590MB (+56MB)
UNKNOWN
Iteration Time:	 9.63s

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

Models       : 0+
Calls        : 39
Time         : 229.487s (Solving: 213.68s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 229.468s

Choices      : 6023692  (Domain: 5903315)
Conflicts    : 304951   (Analyzed: 304948)
Restarts     : 3502     (Average: 87.08 Last: 170)
Model-Level  : 115.0   
Problems     : 39       (Average Length: 61.87 Splits: 0)
Lemmas       : 304948   (Deleted: 281699)
  Binary     : 7742     (Ratio:   2.54%)
  Ternary    : 2044     (Ratio:   0.67%)
  Conflict   : 304948   (Average Length:  532.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 304948   (Average: 17.88 Max: 804 Sum: 5451933)
  Executed   : 304852   (Average: 17.87 Max: 804 Sum: 5449371 Ratio:  99.95%)
  Bounded    : 96       (Average: 26.69 Max:  87 Sum:   2562 Ratio:   0.05%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 516088   (Eliminated:    0 Frozen: 165462)
Constraints  : 3817932  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 10.21s
Memory:		 593MB (+3MB)
UNKNOWN
Iteration Time:	 10.95s

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

Models       : 0+
Calls        : 40
Time         : 240.042s (Solving: 223.38s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 240.024s

Choices      : 6379244  (Domain: 6257912)
Conflicts    : 314000   (Analyzed: 313997)
Restarts     : 3602     (Average: 87.17 Last: 170)
Model-Level  : 115.0   
Problems     : 40       (Average Length: 63.00 Splits: 0)
Lemmas       : 313997   (Deleted: 290078)
  Binary     : 7969     (Ratio:   2.54%)
  Ternary    : 2063     (Ratio:   0.66%)
  Conflict   : 313997   (Average Length:  537.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 313997   (Average: 18.40 Max: 804 Sum: 5776888)
  Executed   : 313901   (Average: 18.39 Max: 804 Sum: 5774326 Ratio:  99.96%)
  Bounded    : 96       (Average: 26.69 Max:  87 Sum:   2562 Ratio:   0.04%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 542484   (Eliminated:    0 Frozen: 174002)
Constraints  : 4019002  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 9.80s
Memory:		 601MB (+8MB)
UNKNOWN
Iteration Time:	 10.56s

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

Models       : 0+
Calls        : 41
Time         : 243.410s (Solving: 226.62s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 243.396s

Choices      : 6430841  (Domain: 6309509)
Conflicts    : 321968   (Analyzed: 321965)
Restarts     : 3702     (Average: 86.97 Last: 170)
Model-Level  : 115.0   
Problems     : 41       (Average Length: 64.07 Splits: 0)
Lemmas       : 321965   (Deleted: 296652)
  Binary     : 8159     (Ratio:   2.53%)
  Ternary    : 2097     (Ratio:   0.65%)
  Conflict   : 321965   (Average Length:  532.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 321965   (Average: 18.09 Max: 804 Sum: 5822997)
  Executed   : 321869   (Average: 18.08 Max: 804 Sum: 5820435 Ratio:  99.96%)
  Bounded    : 96       (Average: 26.69 Max:  87 Sum:   2562 Ratio:   0.04%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 542484   (Eliminated:    0 Frozen: 174002)
Constraints  : 4019002  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 3.32s
Memory:		 607MB (+6MB)
UNKNOWN
Iteration Time:	 3.37s

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

Models       : 0+
Calls        : 42
Time         : 251.218s (Solving: 234.30s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 251.208s

Choices      : 6495553  (Domain: 6374179)
Conflicts    : 331081   (Analyzed: 331078)
Restarts     : 3802     (Average: 87.08 Last: 170)
Model-Level  : 115.0   
Problems     : 42       (Average Length: 65.10 Splits: 0)
Lemmas       : 331078   (Deleted: 306175)
  Binary     : 8297     (Ratio:   2.51%)
  Ternary    : 2135     (Ratio:   0.64%)
  Conflict   : 331078   (Average Length:  542.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 331078   (Average: 17.75 Max: 804 Sum: 5876081)
  Executed   : 330981   (Average: 17.74 Max: 804 Sum: 5873416 Ratio:  99.95%)
  Bounded    : 97       (Average: 27.47 Max: 103 Sum:   2665 Ratio:   0.05%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 542484   (Eliminated:    0 Frozen: 174002)
Constraints  : 4019002  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

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

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

Models       : 0+
Calls        : 43
Time         : 259.001s (Solving: 241.96s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 258.996s

Choices      : 6594146  (Domain: 6472016)
Conflicts    : 340237   (Analyzed: 340234)
Restarts     : 3902     (Average: 87.19 Last: 170)
Model-Level  : 115.0   
Problems     : 43       (Average Length: 66.07 Splits: 0)
Lemmas       : 340234   (Deleted: 315492)
  Binary     : 8513     (Ratio:   2.50%)
  Ternary    : 2196     (Ratio:   0.65%)
  Conflict   : 340234   (Average Length:  558.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 340234   (Average: 17.50 Max: 804 Sum: 5954361)
  Executed   : 340137   (Average: 17.49 Max: 804 Sum: 5951696 Ratio:  99.96%)
  Bounded    : 97       (Average: 27.47 Max: 103 Sum:   2665 Ratio:   0.04%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 542484   (Eliminated:    0 Frozen: 174002)
Constraints  : 4019002  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

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

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

Models       : 0+
Calls        : 44
Time         : 266.714s (Solving: 249.54s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 266.712s

Choices      : 6710814  (Domain: 6584758)
Conflicts    : 349303   (Analyzed: 349300)
Restarts     : 4002     (Average: 87.28 Last: 170)
Model-Level  : 115.0   
Problems     : 44       (Average Length: 67.00 Splits: 0)
Lemmas       : 349300   (Deleted: 323636)
  Binary     : 8739     (Ratio:   2.50%)
  Ternary    : 2291     (Ratio:   0.66%)
  Conflict   : 349300   (Average Length:  564.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 349300   (Average: 17.32 Max: 804 Sum: 6050827)
  Executed   : 349203   (Average: 17.32 Max: 804 Sum: 6048162 Ratio:  99.96%)
  Bounded    : 97       (Average: 27.47 Max: 103 Sum:   2665 Ratio:   0.04%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 542484   (Eliminated:    0 Frozen: 174002)
Constraints  : 4019002  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

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

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

Models       : 0+
Calls        : 45
Time         : 274.357s (Solving: 257.07s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 274.356s

Choices      : 6830088  (Domain: 6703845)
Conflicts    : 358717   (Analyzed: 358714)
Restarts     : 4102     (Average: 87.45 Last: 170)
Model-Level  : 115.0   
Problems     : 45       (Average Length: 67.89 Splits: 0)
Lemmas       : 358714   (Deleted: 332178)
  Binary     : 8867     (Ratio:   2.47%)
  Ternary    : 2311     (Ratio:   0.64%)
  Conflict   : 358714   (Average Length:  566.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 358714   (Average: 17.15 Max: 804 Sum: 6150549)
  Executed   : 358617   (Average: 17.14 Max: 804 Sum: 6147884 Ratio:  99.96%)
  Bounded    : 97       (Average: 27.47 Max: 103 Sum:   2665 Ratio:   0.04%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 542484   (Eliminated:    0 Frozen: 174002)
Constraints  : 4019002  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 7.61s
Memory:		 607MB (+0MB)
UNKNOWN
Iteration Time:	 7.65s

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

Models       : 0+
Calls        : 46
Time         : 281.607s (Solving: 264.20s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 281.612s

Choices      : 6925774  (Domain: 6799473)
Conflicts    : 368019   (Analyzed: 368016)
Restarts     : 4202     (Average: 87.58 Last: 170)
Model-Level  : 115.0   
Problems     : 46       (Average Length: 68.74 Splits: 0)
Lemmas       : 368016   (Deleted: 341260)
  Binary     : 8922     (Ratio:   2.42%)
  Ternary    : 2321     (Ratio:   0.63%)
  Conflict   : 368016   (Average Length:  570.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 368016   (Average: 16.92 Max: 804 Sum: 6226794)
  Executed   : 367919   (Average: 16.91 Max: 804 Sum: 6224129 Ratio:  99.96%)
  Bounded    : 97       (Average: 27.47 Max: 103 Sum:   2665 Ratio:   0.04%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 542484   (Eliminated:    0 Frozen: 174002)
Constraints  : 4019002  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 7.21s
Memory:		 607MB (+0MB)
UNKNOWN
Iteration Time:	 7.26s

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

Models       : 0+
Calls        : 47
Time         : 289.739s (Solving: 272.19s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 289.748s

Choices      : 7038639  (Domain: 6911918)
Conflicts    : 377264   (Analyzed: 377261)
Restarts     : 4302     (Average: 87.69 Last: 170)
Model-Level  : 115.0   
Problems     : 47       (Average Length: 69.55 Splits: 0)
Lemmas       : 377261   (Deleted: 350265)
  Binary     : 8987     (Ratio:   2.38%)
  Ternary    : 2340     (Ratio:   0.62%)
  Conflict   : 377261   (Average Length:  574.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 377261   (Average: 16.75 Max: 804 Sum: 6318417)
  Executed   : 377164   (Average: 16.74 Max: 804 Sum: 6315752 Ratio:  99.96%)
  Bounded    : 97       (Average: 27.47 Max: 103 Sum:   2665 Ratio:   0.04%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 542484   (Eliminated:    0 Frozen: 174002)
Constraints  : 4019002  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

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

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

Models       : 0+
Calls        : 48
Time         : 297.757s (Solving: 280.06s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 297.768s

Choices      : 7160939  (Domain: 7033822)
Conflicts    : 386539   (Analyzed: 386536)
Restarts     : 4402     (Average: 87.81 Last: 170)
Model-Level  : 115.0   
Problems     : 48       (Average Length: 70.33 Splits: 0)
Lemmas       : 386536   (Deleted: 359257)
  Binary     : 9080     (Ratio:   2.35%)
  Ternary    : 2363     (Ratio:   0.61%)
  Conflict   : 386536   (Average Length:  580.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 386536   (Average: 16.60 Max: 804 Sum: 6417714)
  Executed   : 386439   (Average: 16.60 Max: 804 Sum: 6415049 Ratio:  99.96%)
  Bounded    : 97       (Average: 27.47 Max: 103 Sum:   2665 Ratio:   0.04%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 542484   (Eliminated:    0 Frozen: 174002)
Constraints  : 4019002  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

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

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

Models       : 0+
Calls        : 49
Time         : 305.694s (Solving: 287.89s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 305.708s

Choices      : 7303106  (Domain: 7175841)
Conflicts    : 395708   (Analyzed: 395705)
Restarts     : 4502     (Average: 87.90 Last: 170)
Model-Level  : 115.0   
Problems     : 49       (Average Length: 71.08 Splits: 0)
Lemmas       : 395705   (Deleted: 368259)
  Binary     : 9116     (Ratio:   2.30%)
  Ternary    : 2370     (Ratio:   0.60%)
  Conflict   : 395705   (Average Length:  583.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 395705   (Average: 16.52 Max: 804 Sum: 6537132)
  Executed   : 395608   (Average: 16.51 Max: 804 Sum: 6534467 Ratio:  99.96%)
  Bounded    : 97       (Average: 27.47 Max: 103 Sum:   2665 Ratio:   0.04%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 542484   (Eliminated:    0 Frozen: 174002)
Constraints  : 4019002  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

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

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

Models       : 0+
Calls        : 50
Time         : 313.828s (Solving: 295.89s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 313.844s

Choices      : 7504335  (Domain: 7375013)
Conflicts    : 404707   (Analyzed: 404704)
Restarts     : 4602     (Average: 87.94 Last: 170)
Model-Level  : 115.0   
Problems     : 50       (Average Length: 71.80 Splits: 0)
Lemmas       : 404704   (Deleted: 377119)
  Binary     : 9336     (Ratio:   2.31%)
  Ternary    : 2454     (Ratio:   0.61%)
  Conflict   : 404704   (Average Length:  585.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 404704   (Average: 16.58 Max: 804 Sum: 6709035)
  Executed   : 404607   (Average: 16.57 Max: 804 Sum: 6706370 Ratio:  99.96%)
  Bounded    : 97       (Average: 27.47 Max: 103 Sum:   2665 Ratio:   0.04%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 542484   (Eliminated:    0 Frozen: 174002)
Constraints  : 4019002  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

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

Iteration 50
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        : 51
Time         : 322.691s (Solving: 304.63s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 322.700s

Choices      : 7621989  (Domain: 7492407)
Conflicts    : 413223   (Analyzed: 413220)
Restarts     : 4702     (Average: 87.88 Last: 170)
Model-Level  : 115.0   
Problems     : 51       (Average Length: 72.49 Splits: 0)
Lemmas       : 413220   (Deleted: 384332)
  Binary     : 9393     (Ratio:   2.27%)
  Ternary    : 2460     (Ratio:   0.60%)
  Conflict   : 413220   (Average Length:  597.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 413220   (Average: 16.45 Max: 804 Sum: 6795908)
  Executed   : 413123   (Average: 16.44 Max: 804 Sum: 6793243 Ratio:  99.96%)
  Bounded    : 97       (Average: 27.47 Max: 103 Sum:   2665 Ratio:   0.04%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 542484   (Eliminated:    0 Frozen: 174002)
Constraints  : 4019002  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 8.81s
Memory:		 607MB (+0MB)
UNKNOWN
Iteration Time:	 8.86s

Iteration 51
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        : 52
Time         : 331.604s (Solving: 313.40s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 331.616s

Choices      : 7799647  (Domain: 7669964)
Conflicts    : 422499   (Analyzed: 422496)
Restarts     : 4802     (Average: 87.98 Last: 170)
Model-Level  : 115.0   
Problems     : 52       (Average Length: 73.15 Splits: 0)
Lemmas       : 422496   (Deleted: 394032)
  Binary     : 9435     (Ratio:   2.23%)
  Ternary    : 2470     (Ratio:   0.58%)
  Conflict   : 422496   (Average Length:  599.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 422496   (Average: 16.43 Max: 804 Sum: 6943636)
  Executed   : 422399   (Average: 16.43 Max: 804 Sum: 6940971 Ratio:  99.96%)
  Bounded    : 97       (Average: 27.47 Max: 103 Sum:   2665 Ratio:   0.04%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 542484   (Eliminated:    0 Frozen: 174002)
Constraints  : 4019002  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 8.86s
Memory:		 607MB (+0MB)
UNKNOWN
Iteration Time:	 8.92s

Iteration 52
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        : 53
Time         : 341.232s (Solving: 322.92s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 341.248s

Choices      : 7985443  (Domain: 7854970)
Conflicts    : 431998   (Analyzed: 431995)
Restarts     : 4902     (Average: 88.13 Last: 170)
Model-Level  : 115.0   
Problems     : 53       (Average Length: 73.79 Splits: 0)
Lemmas       : 431995   (Deleted: 403120)
  Binary     : 9499     (Ratio:   2.20%)
  Ternary    : 2479     (Ratio:   0.57%)
  Conflict   : 431995   (Average Length:  604.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 431995   (Average: 16.42 Max: 804 Sum: 7094388)
  Executed   : 431898   (Average: 16.42 Max: 804 Sum: 7091723 Ratio:  99.96%)
  Bounded    : 97       (Average: 27.47 Max: 103 Sum:   2665 Ratio:   0.04%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 542484   (Eliminated:    0 Frozen: 174002)
Constraints  : 4019002  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

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

Iteration 53
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        : 54
Time         : 350.764s (Solving: 332.33s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 350.784s

Choices      : 8163807  (Domain: 8032808)
Conflicts    : 441246   (Analyzed: 441243)
Restarts     : 5002     (Average: 88.21 Last: 170)
Model-Level  : 115.0   
Problems     : 54       (Average Length: 74.41 Splits: 0)
Lemmas       : 441243   (Deleted: 412313)
  Binary     : 9593     (Ratio:   2.17%)
  Ternary    : 2505     (Ratio:   0.57%)
  Conflict   : 441243   (Average Length:  606.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 441243   (Average: 16.41 Max: 804 Sum: 7239497)
  Executed   : 441146   (Average: 16.40 Max: 804 Sum: 7236832 Ratio:  99.96%)
  Bounded    : 97       (Average: 27.47 Max: 103 Sum:   2665 Ratio:   0.04%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 542484   (Eliminated:    0 Frozen: 174002)
Constraints  : 4019002  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

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

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

Models       : 0+
Calls        : 55
Time         : 360.243s (Solving: 340.96s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 360.268s

Choices      : 8299406  (Domain: 8168390)
Conflicts    : 450657   (Analyzed: 450654)
Restarts     : 5102     (Average: 88.33 Last: 170)
Model-Level  : 115.0   
Problems     : 55       (Average Length: 75.09 Splits: 0)
Lemmas       : 450654   (Deleted: 421286)
  Binary     : 9645     (Ratio:   2.14%)
  Ternary    : 2509     (Ratio:   0.56%)
  Conflict   : 450654   (Average Length:  609.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 450654   (Average: 16.30 Max: 804 Sum: 7343702)
  Executed   : 450557   (Average: 16.29 Max: 804 Sum: 7341037 Ratio:  99.96%)
  Bounded    : 97       (Average: 27.47 Max: 103 Sum:   2665 Ratio:   0.04%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 568880   (Eliminated:    0 Frozen: 182542)
Constraints  : 4220072  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 8.74s
Memory:		 621MB (+14MB)
UNKNOWN
Iteration Time:	 9.49s

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

Models       : 0+
Calls        : 56
Time         : 371.728s (Solving: 351.59s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 371.760s

Choices      : 8452358  (Domain: 8321303)
Conflicts    : 460582   (Analyzed: 460579)
Restarts     : 5202     (Average: 88.54 Last: 170)
Model-Level  : 115.0   
Problems     : 56       (Average Length: 75.84 Splits: 0)
Lemmas       : 460579   (Deleted: 430544)
  Binary     : 9673     (Ratio:   2.10%)
  Ternary    : 2521     (Ratio:   0.55%)
  Conflict   : 460579   (Average Length:  613.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 460579   (Average: 16.20 Max: 804 Sum: 7460145)
  Executed   : 460482   (Average: 16.19 Max: 804 Sum: 7457480 Ratio:  99.96%)
  Bounded    : 97       (Average: 27.47 Max: 103 Sum:   2665 Ratio:   0.04%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 595276   (Eliminated:    0 Frozen: 191082)
Constraints  : 4421142  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 10.74s
Memory:		 637MB (+16MB)
UNKNOWN
Iteration Time:	 11.50s

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

Models       : 0+
Calls        : 57
Time         : 374.767s (Solving: 354.48s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 374.796s

Choices      : 8496233  (Domain: 8365178)
Conflicts    : 468049   (Analyzed: 468046)
Restarts     : 5302     (Average: 88.28 Last: 170)
Model-Level  : 115.0   
Problems     : 57       (Average Length: 76.56 Splits: 0)
Lemmas       : 468046   (Deleted: 438008)
  Binary     : 9722     (Ratio:   2.08%)
  Ternary    : 2533     (Ratio:   0.54%)
  Conflict   : 468046   (Average Length:  607.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 468046   (Average: 16.02 Max: 804 Sum: 7496619)
  Executed   : 467948   (Average: 16.01 Max: 804 Sum: 7493837 Ratio:  99.96%)
  Bounded    : 98       (Average: 28.39 Max: 117 Sum:   2782 Ratio:   0.04%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 595276   (Eliminated:    0 Frozen: 191082)
Constraints  : 4421142  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

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

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

Models       : 0+
Calls        : 58
Time         : 383.726s (Solving: 363.31s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 383.760s

Choices      : 8542421  (Domain: 8411366)
Conflicts    : 476684   (Analyzed: 476681)
Restarts     : 5402     (Average: 88.24 Last: 170)
Model-Level  : 115.0   
Problems     : 58       (Average Length: 77.26 Splits: 0)
Lemmas       : 476681   (Deleted: 447362)
  Binary     : 9760     (Ratio:   2.05%)
  Ternary    : 2544     (Ratio:   0.53%)
  Conflict   : 476681   (Average Length:  617.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 476681   (Average: 15.80 Max: 804 Sum: 7529934)
  Executed   : 476583   (Average: 15.79 Max: 804 Sum: 7527152 Ratio:  99.96%)
  Bounded    : 98       (Average: 28.39 Max: 117 Sum:   2782 Ratio:   0.04%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 595276   (Eliminated:    0 Frozen: 191082)
Constraints  : 4421128  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

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

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

Models       : 0+
Calls        : 59
Time         : 391.228s (Solving: 370.68s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 391.264s

Choices      : 8618700  (Domain: 8487645)
Conflicts    : 485737   (Analyzed: 485734)
Restarts     : 5502     (Average: 88.28 Last: 170)
Model-Level  : 115.0   
Problems     : 59       (Average Length: 77.93 Splits: 0)
Lemmas       : 485734   (Deleted: 455742)
  Binary     : 9883     (Ratio:   2.03%)
  Ternary    : 2566     (Ratio:   0.53%)
  Conflict   : 485734   (Average Length:  621.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 485734   (Average: 15.62 Max: 804 Sum: 7587479)
  Executed   : 485636   (Average: 15.61 Max: 804 Sum: 7584697 Ratio:  99.96%)
  Bounded    : 98       (Average: 28.39 Max: 117 Sum:   2782 Ratio:   0.04%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 595276   (Eliminated:    0 Frozen: 191082)
Constraints  : 4421128  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

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

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

Models       : 0+
Calls        : 60
Time         : 398.492s (Solving: 377.82s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 398.532s

Choices      : 8689250  (Domain: 8557293)
Conflicts    : 494574   (Analyzed: 494571)
Restarts     : 5602     (Average: 88.28 Last: 170)
Model-Level  : 115.0   
Problems     : 60       (Average Length: 78.58 Splits: 0)
Lemmas       : 494571   (Deleted: 464538)
  Binary     : 9965     (Ratio:   2.01%)
  Ternary    : 2573     (Ratio:   0.52%)
  Conflict   : 494571   (Average Length:  625.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 494571   (Average: 15.44 Max: 804 Sum: 7637879)
  Executed   : 494473   (Average: 15.44 Max: 804 Sum: 7635097 Ratio:  99.96%)
  Bounded    : 98       (Average: 28.39 Max: 117 Sum:   2782 Ratio:   0.04%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 595276   (Eliminated:    0 Frozen: 191082)
Constraints  : 4421128  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

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

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

Models       : 0+
Calls        : 61
Time         : 405.756s (Solving: 384.97s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 405.800s

Choices      : 8797588  (Domain: 8660669)
Conflicts    : 503822   (Analyzed: 503819)
Restarts     : 5702     (Average: 88.36 Last: 170)
Model-Level  : 115.0   
Problems     : 61       (Average Length: 79.21 Splits: 0)
Lemmas       : 503819   (Deleted: 472749)
  Binary     : 10220    (Ratio:   2.03%)
  Ternary    : 2595     (Ratio:   0.52%)
  Conflict   : 503819   (Average Length:  627.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 503819   (Average: 15.32 Max: 804 Sum: 7718391)
  Executed   : 503721   (Average: 15.31 Max: 804 Sum: 7715609 Ratio:  99.96%)
  Bounded    : 98       (Average: 28.39 Max: 117 Sum:   2782 Ratio:   0.04%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 595276   (Eliminated:    0 Frozen: 191082)
Constraints  : 4421128  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

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

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

Models       : 0+
Calls        : 62
Time         : 413.314s (Solving: 392.40s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 413.360s

Choices      : 8880447  (Domain: 8743518)
Conflicts    : 512942   (Analyzed: 512939)
Restarts     : 5802     (Average: 88.41 Last: 170)
Model-Level  : 115.0   
Problems     : 62       (Average Length: 79.82 Splits: 0)
Lemmas       : 512939   (Deleted: 481710)
  Binary     : 10279    (Ratio:   2.00%)
  Ternary    : 2607     (Ratio:   0.51%)
  Conflict   : 512939   (Average Length:  632.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 512939   (Average: 15.17 Max: 804 Sum: 7780418)
  Executed   : 512841   (Average: 15.16 Max: 804 Sum: 7777636 Ratio:  99.96%)
  Bounded    : 98       (Average: 28.39 Max: 117 Sum:   2782 Ratio:   0.04%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 595276   (Eliminated:    0 Frozen: 191082)
Constraints  : 4421128  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

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

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

Models       : 0+
Calls        : 63
Time         : 420.951s (Solving: 399.89s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 421.000s

Choices      : 8967467  (Domain: 8830526)
Conflicts    : 522172   (Analyzed: 522169)
Restarts     : 5902     (Average: 88.47 Last: 170)
Model-Level  : 115.0   
Problems     : 63       (Average Length: 80.41 Splits: 0)
Lemmas       : 522169   (Deleted: 490655)
  Binary     : 10305    (Ratio:   1.97%)
  Ternary    : 2609     (Ratio:   0.50%)
  Conflict   : 522169   (Average Length:  632.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 522169   (Average: 15.03 Max: 804 Sum: 7846405)
  Executed   : 522071   (Average: 15.02 Max: 804 Sum: 7843623 Ratio:  99.96%)
  Bounded    : 98       (Average: 28.39 Max: 117 Sum:   2782 Ratio:   0.04%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 595276   (Eliminated:    0 Frozen: 191082)
Constraints  : 4421128  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

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

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

Models       : 0+
Calls        : 64
Time         : 429.223s (Solving: 408.02s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 429.276s

Choices      : 9059058  (Domain: 8922095)
Conflicts    : 531500   (Analyzed: 531497)
Restarts     : 6002     (Average: 88.55 Last: 170)
Model-Level  : 115.0   
Problems     : 64       (Average Length: 80.98 Splits: 0)
Lemmas       : 531497   (Deleted: 499685)
  Binary     : 10323    (Ratio:   1.94%)
  Ternary    : 2611     (Ratio:   0.49%)
  Conflict   : 531497   (Average Length:  634.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 531497   (Average: 14.89 Max: 804 Sum: 7913250)
  Executed   : 531399   (Average: 14.88 Max: 804 Sum: 7910468 Ratio:  99.96%)
  Bounded    : 98       (Average: 28.39 Max: 117 Sum:   2782 Ratio:   0.04%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 595276   (Eliminated:    0 Frozen: 191082)
Constraints  : 4421128  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

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

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

Models       : 0+
Calls        : 65
Time         : 437.536s (Solving: 416.21s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 437.592s

Choices      : 9153270  (Domain: 9016300)
Conflicts    : 540952   (Analyzed: 540949)
Restarts     : 6102     (Average: 88.65 Last: 172)
Model-Level  : 115.0   
Problems     : 65       (Average Length: 81.54 Splits: 0)
Lemmas       : 540949   (Deleted: 508794)
  Binary     : 10347    (Ratio:   1.91%)
  Ternary    : 2614     (Ratio:   0.48%)
  Conflict   : 540949   (Average Length:  636.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 540949   (Average: 14.75 Max: 804 Sum: 7981558)
  Executed   : 540851   (Average: 14.75 Max: 804 Sum: 7978776 Ratio:  99.97%)
  Bounded    : 98       (Average: 28.39 Max: 117 Sum:   2782 Ratio:   0.03%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 595276   (Eliminated:    0 Frozen: 191082)
Constraints  : 4421128  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

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

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

Models       : 0+
Calls        : 66
Time         : 447.483s (Solving: 426.01s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 447.540s

Choices      : 9264003  (Domain: 9126961)
Conflicts    : 550781   (Analyzed: 550778)
Restarts     : 6202     (Average: 88.81 Last: 172)
Model-Level  : 115.0   
Problems     : 66       (Average Length: 82.08 Splits: 0)
Lemmas       : 550778   (Deleted: 518071)
  Binary     : 10367    (Ratio:   1.88%)
  Ternary    : 2621     (Ratio:   0.48%)
  Conflict   : 550778   (Average Length:  640.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 550778   (Average: 14.63 Max: 804 Sum: 8058202)
  Executed   : 550680   (Average: 14.63 Max: 804 Sum: 8055420 Ratio:  99.97%)
  Bounded    : 98       (Average: 28.39 Max: 117 Sum:   2782 Ratio:   0.03%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 595276   (Eliminated:    0 Frozen: 191082)
Constraints  : 4421128  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

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

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

Models       : 0+
Calls        : 67
Time         : 456.370s (Solving: 434.76s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 456.432s

Choices      : 9380536  (Domain: 9243485)
Conflicts    : 560063   (Analyzed: 560060)
Restarts     : 6302     (Average: 88.87 Last: 172)
Model-Level  : 115.0   
Problems     : 67       (Average Length: 82.60 Splits: 0)
Lemmas       : 560060   (Deleted: 527755)
  Binary     : 10416    (Ratio:   1.86%)
  Ternary    : 2622     (Ratio:   0.47%)
  Conflict   : 560060   (Average Length:  642.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 560060   (Average: 14.54 Max: 804 Sum: 8141773)
  Executed   : 559962   (Average: 14.53 Max: 804 Sum: 8138991 Ratio:  99.97%)
  Bounded    : 98       (Average: 28.39 Max: 117 Sum:   2782 Ratio:   0.03%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 595276   (Eliminated:    0 Frozen: 191082)
Constraints  : 4421128  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 8.84s
Memory:		 637MB (+0MB)
UNKNOWN
Iteration Time:	 8.89s

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

Models       : 0+
Calls        : 68
Time         : 459.552s (Solving: 437.79s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 459.616s

Choices      : 9434154  (Domain: 9297103)
Conflicts    : 567639   (Analyzed: 567636)
Restarts     : 6402     (Average: 88.67 Last: 172)
Model-Level  : 115.0   
Problems     : 68       (Average Length: 83.10 Splits: 0)
Lemmas       : 567636   (Deleted: 534523)
  Binary     : 10500    (Ratio:   1.85%)
  Ternary    : 2643     (Ratio:   0.47%)
  Conflict   : 567636   (Average Length:  637.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 567636   (Average: 14.43 Max: 804 Sum: 8190438)
  Executed   : 567535   (Average: 14.42 Max: 804 Sum: 8187305 Ratio:  99.96%)
  Bounded    : 101      (Average: 31.02 Max: 117 Sum:   3133 Ratio:   0.04%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 595276   (Eliminated:    0 Frozen: 191082)
Constraints  : 4421128  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 3.13s
Memory:		 637MB (+0MB)
UNKNOWN
Iteration Time:	 3.19s

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

Models       : 0+
Calls        : 69
Time         : 470.051s (Solving: 448.16s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 470.116s

Choices      : 9482131  (Domain: 9345080)
Conflicts    : 576664   (Analyzed: 576661)
Restarts     : 6502     (Average: 88.69 Last: 172)
Model-Level  : 115.0   
Problems     : 69       (Average Length: 83.59 Splits: 0)
Lemmas       : 576661   (Deleted: 543859)
  Binary     : 10552    (Ratio:   1.83%)
  Ternary    : 2651     (Ratio:   0.46%)
  Conflict   : 576661   (Average Length:  650.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 576661   (Average: 14.26 Max: 804 Sum: 8224004)
  Executed   : 576560   (Average: 14.26 Max: 804 Sum: 8220871 Ratio:  99.96%)
  Bounded    : 101      (Average: 31.02 Max: 117 Sum:   3133 Ratio:   0.04%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 595276   (Eliminated:    0 Frozen: 191082)
Constraints  : 4421087  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

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

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

Models       : 0+
Calls        : 70
Time         : 476.594s (Solving: 454.55s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 476.660s

Choices      : 9557144  (Domain: 9420093)
Conflicts    : 585502   (Analyzed: 585499)
Restarts     : 6602     (Average: 88.69 Last: 172)
Model-Level  : 115.0   
Problems     : 70       (Average Length: 84.07 Splits: 0)
Lemmas       : 585499   (Deleted: 552610)
  Binary     : 10648    (Ratio:   1.82%)
  Ternary    : 2662     (Ratio:   0.45%)
  Conflict   : 585499   (Average Length:  653.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 585499   (Average: 14.14 Max: 804 Sum: 8280709)
  Executed   : 585398   (Average: 14.14 Max: 804 Sum: 8277576 Ratio:  99.96%)
  Bounded    : 101      (Average: 31.02 Max: 117 Sum:   3133 Ratio:   0.04%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 595276   (Eliminated:    0 Frozen: 191082)
Constraints  : 4421087  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

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

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

Models       : 0+
Calls        : 71
Time         : 484.082s (Solving: 461.92s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 484.152s

Choices      : 9635294  (Domain: 9497946)
Conflicts    : 595789   (Analyzed: 595786)
Restarts     : 6702     (Average: 88.90 Last: 172)
Model-Level  : 115.0   
Problems     : 71       (Average Length: 84.54 Splits: 0)
Lemmas       : 595786   (Deleted: 561289)
  Binary     : 10713    (Ratio:   1.80%)
  Ternary    : 2669     (Ratio:   0.45%)
  Conflict   : 595786   (Average Length:  653.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 595786   (Average: 14.00 Max: 804 Sum: 8340737)
  Executed   : 595685   (Average: 13.99 Max: 804 Sum: 8337604 Ratio:  99.96%)
  Bounded    : 101      (Average: 31.02 Max: 117 Sum:   3133 Ratio:   0.04%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 595276   (Eliminated:    0 Frozen: 191082)
Constraints  : 4421087  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

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

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

Models       : 0+
Calls        : 72
Time         : 491.756s (Solving: 469.45s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 491.828s

Choices      : 9707894  (Domain: 9570482)
Conflicts    : 605018   (Analyzed: 605015)
Restarts     : 6802     (Average: 88.95 Last: 172)
Model-Level  : 115.0   
Problems     : 72       (Average Length: 84.99 Splits: 0)
Lemmas       : 605015   (Deleted: 571311)
  Binary     : 10761    (Ratio:   1.78%)
  Ternary    : 2675     (Ratio:   0.44%)
  Conflict   : 605015   (Average Length:  657.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 605015   (Average: 13.87 Max: 804 Sum: 8391385)
  Executed   : 604914   (Average: 13.86 Max: 804 Sum: 8388252 Ratio:  99.96%)
  Bounded    : 101      (Average: 31.02 Max: 117 Sum:   3133 Ratio:   0.04%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 595276   (Eliminated:    0 Frozen: 191082)
Constraints  : 4421087  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

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

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

Models       : 0+
Calls        : 73
Time         : 499.479s (Solving: 477.02s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 499.552s

Choices      : 9782772  (Domain: 9645348)
Conflicts    : 615176   (Analyzed: 615173)
Restarts     : 6902     (Average: 89.13 Last: 172)
Model-Level  : 115.0   
Problems     : 73       (Average Length: 85.42 Splits: 0)
Lemmas       : 615173   (Deleted: 580367)
  Binary     : 10788    (Ratio:   1.75%)
  Ternary    : 2675     (Ratio:   0.43%)
  Conflict   : 615173   (Average Length:  657.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 615173   (Average: 13.73 Max: 804 Sum: 8445699)
  Executed   : 615072   (Average: 13.72 Max: 804 Sum: 8442566 Ratio:  99.96%)
  Bounded    : 101      (Average: 31.02 Max: 117 Sum:   3133 Ratio:   0.04%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 595276   (Eliminated:    0 Frozen: 191082)
Constraints  : 4421087  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

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

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

Models       : 0+
Calls        : 74
Time         : 507.094s (Solving: 484.51s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 507.168s

Choices      : 9855687  (Domain: 9718221)
Conflicts    : 624144   (Analyzed: 624141)
Restarts     : 7002     (Average: 89.14 Last: 172)
Model-Level  : 115.0   
Problems     : 74       (Average Length: 85.85 Splits: 0)
Lemmas       : 624141   (Deleted: 590302)
  Binary     : 10814    (Ratio:   1.73%)
  Ternary    : 2685     (Ratio:   0.43%)
  Conflict   : 624141   (Average Length:  660.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 624141   (Average: 13.61 Max: 804 Sum: 8495389)
  Executed   : 624040   (Average: 13.61 Max: 804 Sum: 8492256 Ratio:  99.96%)
  Bounded    : 101      (Average: 31.02 Max: 117 Sum:   3133 Ratio:   0.04%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 595276   (Eliminated:    0 Frozen: 191082)
Constraints  : 4421087  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

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

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

Models       : 0+
Calls        : 75
Time         : 514.984s (Solving: 492.28s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 515.060s

Choices      : 9923181  (Domain: 9785715)
Conflicts    : 633437   (Analyzed: 633434)
Restarts     : 7102     (Average: 89.19 Last: 172)
Model-Level  : 115.0   
Problems     : 75       (Average Length: 86.27 Splits: 0)
Lemmas       : 633434   (Deleted: 599117)
  Binary     : 10832    (Ratio:   1.71%)
  Ternary    : 2689     (Ratio:   0.42%)
  Conflict   : 633434   (Average Length:  663.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 633434   (Average: 13.48 Max: 804 Sum: 8537864)
  Executed   : 633333   (Average: 13.47 Max: 804 Sum: 8534731 Ratio:  99.96%)
  Bounded    : 101      (Average: 31.02 Max: 117 Sum:   3133 Ratio:   0.04%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 595276   (Eliminated:    0 Frozen: 191082)
Constraints  : 4421087  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 7.85s
Memory:		 701MB (+0MB)
UNKNOWN
Iteration Time:	 7.90s

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

Models       : 0+
Calls        : 76
Time         : 523.361s (Solving: 500.52s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 523.440s

Choices      : 10023275 (Domain: 9885660)
Conflicts    : 643207   (Analyzed: 643204)
Restarts     : 7202     (Average: 89.31 Last: 172)
Model-Level  : 115.0   
Problems     : 76       (Average Length: 86.67 Splits: 0)
Lemmas       : 643204   (Deleted: 608177)
  Binary     : 10876    (Ratio:   1.69%)
  Ternary    : 2695     (Ratio:   0.42%)
  Conflict   : 643204   (Average Length:  665.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 643204   (Average: 13.38 Max: 804 Sum: 8609242)
  Executed   : 643103   (Average: 13.38 Max: 804 Sum: 8606109 Ratio:  99.96%)
  Bounded    : 101      (Average: 31.02 Max: 117 Sum:   3133 Ratio:   0.04%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 595276   (Eliminated:    0 Frozen: 191082)
Constraints  : 4421087  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

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

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

Models       : 0+
Calls        : 77
Time         : 531.762s (Solving: 508.78s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 531.844s

Choices      : 10107051 (Domain: 9969435)
Conflicts    : 652228   (Analyzed: 652225)
Restarts     : 7302     (Average: 89.32 Last: 172)
Model-Level  : 115.0   
Problems     : 77       (Average Length: 87.06 Splits: 0)
Lemmas       : 652225   (Deleted: 617783)
  Binary     : 10887    (Ratio:   1.67%)
  Ternary    : 2699     (Ratio:   0.41%)
  Conflict   : 652225   (Average Length:  669.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 652225   (Average: 13.29 Max: 804 Sum: 8665447)
  Executed   : 652124   (Average: 13.28 Max: 804 Sum: 8662314 Ratio:  99.96%)
  Bounded    : 101      (Average: 31.02 Max: 117 Sum:   3133 Ratio:   0.04%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 595276   (Eliminated:    0 Frozen: 191082)
Constraints  : 4421087  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

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

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

Models       : 0+
Calls        : 78
Time         : 534.891s (Solving: 511.78s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 534.972s

Choices      : 10158302 (Domain: 10020686)
Conflicts    : 659798   (Analyzed: 659795)
Restarts     : 7402     (Average: 89.14 Last: 172)
Model-Level  : 115.0   
Problems     : 78       (Average Length: 87.45 Splits: 0)
Lemmas       : 659795   (Deleted: 624374)
  Binary     : 10965    (Ratio:   1.66%)
  Ternary    : 2706     (Ratio:   0.41%)
  Conflict   : 659795   (Average Length:  663.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 659795   (Average: 13.19 Max: 804 Sum: 8702473)
  Executed   : 659694   (Average: 13.18 Max: 804 Sum: 8699340 Ratio:  99.96%)
  Bounded    : 101      (Average: 31.02 Max: 117 Sum:   3133 Ratio:   0.04%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 595276   (Eliminated:    0 Frozen: 191082)
Constraints  : 4421087  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 3.08s
Memory:		 701MB (+0MB)
UNKNOWN
Iteration Time:	 3.13s

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

Models       : 0+
Calls        : 79
Time         : 544.334s (Solving: 521.10s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 544.420s

Choices      : 10197256 (Domain: 10059640)
Conflicts    : 667894   (Analyzed: 667891)
Restarts     : 7502     (Average: 89.03 Last: 172)
Model-Level  : 115.0   
Problems     : 79       (Average Length: 87.82 Splits: 0)
Lemmas       : 667891   (Deleted: 631853)
  Binary     : 10983    (Ratio:   1.64%)
  Ternary    : 2717     (Ratio:   0.41%)
  Conflict   : 667891   (Average Length:  675.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 667891   (Average: 13.07 Max: 804 Sum: 8731224)
  Executed   : 667790   (Average: 13.07 Max: 804 Sum: 8728091 Ratio:  99.96%)
  Bounded    : 101      (Average: 31.02 Max: 117 Sum:   3133 Ratio:   0.04%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 595276   (Eliminated:    0 Frozen: 191082)
Constraints  : 4421087  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

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

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

Models       : 0+
Calls        : 80
Time         : 552.480s (Solving: 529.09s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 552.568s

Choices      : 10271487 (Domain: 10133871)
Conflicts    : 676239   (Analyzed: 676236)
Restarts     : 7602     (Average: 88.96 Last: 172)
Model-Level  : 115.0   
Problems     : 80       (Average Length: 88.19 Splits: 0)
Lemmas       : 676236   (Deleted: 639948)
  Binary     : 11038    (Ratio:   1.63%)
  Ternary    : 2728     (Ratio:   0.40%)
  Conflict   : 676236   (Average Length:  679.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 676236   (Average: 13.00 Max: 804 Sum: 8788265)
  Executed   : 676135   (Average: 12.99 Max: 804 Sum: 8785132 Ratio:  99.96%)
  Bounded    : 101      (Average: 31.02 Max: 117 Sum:   3133 Ratio:   0.04%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 595276   (Eliminated:    0 Frozen: 191082)
Constraints  : 4421087  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

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

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

Models       : 0+
Calls        : 81
Time         : 559.310s (Solving: 535.80s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 559.400s

Choices      : 10337609 (Domain: 10199947)
Conflicts    : 685769   (Analyzed: 685766)
Restarts     : 7702     (Average: 89.04 Last: 172)
Model-Level  : 115.0   
Problems     : 81       (Average Length: 88.54 Splits: 0)
Lemmas       : 685766   (Deleted: 649978)
  Binary     : 11077    (Ratio:   1.62%)
  Ternary    : 2735     (Ratio:   0.40%)
  Conflict   : 685766   (Average Length:  679.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 685766   (Average: 12.89 Max: 804 Sum: 8837229)
  Executed   : 685665   (Average: 12.88 Max: 804 Sum: 8834096 Ratio:  99.96%)
  Bounded    : 101      (Average: 31.02 Max: 117 Sum:   3133 Ratio:   0.04%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 595276   (Eliminated:    0 Frozen: 191082)
Constraints  : 4421087  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 6.79s
Memory:		 701MB (+0MB)
UNKNOWN
Iteration Time:	 6.84s

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

Models       : 0+
Calls        : 82
Time         : 566.491s (Solving: 542.86s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 566.584s

Choices      : 10402205 (Domain: 10264543)
Conflicts    : 694775   (Analyzed: 694772)
Restarts     : 7802     (Average: 89.05 Last: 172)
Model-Level  : 115.0   
Problems     : 82       (Average Length: 88.89 Splits: 0)
Lemmas       : 694772   (Deleted: 659325)
  Binary     : 11104    (Ratio:   1.60%)
  Ternary    : 2740     (Ratio:   0.39%)
  Conflict   : 694772   (Average Length:  682.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 694772   (Average: 12.78 Max: 804 Sum: 8882600)
  Executed   : 694671   (Average: 12.78 Max: 804 Sum: 8879467 Ratio:  99.96%)
  Bounded    : 101      (Average: 31.02 Max: 117 Sum:   3133 Ratio:   0.04%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 595276   (Eliminated:    0 Frozen: 191082)
Constraints  : 4421087  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

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

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

Models       : 0+
Calls        : 83
Time         : 573.665s (Solving: 549.90s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 573.760s

Choices      : 10471274 (Domain: 10333596)
Conflicts    : 703729   (Analyzed: 703726)
Restarts     : 7902     (Average: 89.06 Last: 172)
Model-Level  : 115.0   
Problems     : 83       (Average Length: 89.23 Splits: 0)
Lemmas       : 703726   (Deleted: 668164)
  Binary     : 11147    (Ratio:   1.58%)
  Ternary    : 2742     (Ratio:   0.39%)
  Conflict   : 703726   (Average Length:  685.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 703726   (Average: 12.69 Max: 804 Sum: 8929593)
  Executed   : 703625   (Average: 12.68 Max: 804 Sum: 8926460 Ratio:  99.96%)
  Bounded    : 101      (Average: 31.02 Max: 117 Sum:   3133 Ratio:   0.04%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 595276   (Eliminated:    0 Frozen: 191082)
Constraints  : 4421087  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 7.13s
Memory:		 701MB (+0MB)
UNKNOWN
Iteration Time:	 7.18s

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

Models       : 0+
Calls        : 84
Time         : 581.706s (Solving: 557.82s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 581.804s

Choices      : 10551647 (Domain: 10413967)
Conflicts    : 713098   (Analyzed: 713095)
Restarts     : 8002     (Average: 89.11 Last: 172)
Model-Level  : 115.0   
Problems     : 84       (Average Length: 89.56 Splits: 0)
Lemmas       : 713095   (Deleted: 676932)
  Binary     : 11170    (Ratio:   1.57%)
  Ternary    : 2753     (Ratio:   0.39%)
  Conflict   : 713095   (Average Length:  687.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 713095   (Average: 12.60 Max: 804 Sum: 8986082)
  Executed   : 712994   (Average: 12.60 Max: 804 Sum: 8982949 Ratio:  99.97%)
  Bounded    : 101      (Average: 31.02 Max: 117 Sum:   3133 Ratio:   0.03%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 595276   (Eliminated:    0 Frozen: 191082)
Constraints  : 4421087  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

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

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

Models       : 0+
Calls        : 85
Time         : 590.176s (Solving: 566.16s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 590.276s

Choices      : 10649622 (Domain: 10511921)
Conflicts    : 722224   (Analyzed: 722221)
Restarts     : 8102     (Average: 89.14 Last: 172)
Model-Level  : 115.0   
Problems     : 85       (Average Length: 89.88 Splits: 0)
Lemmas       : 722221   (Deleted: 686115)
  Binary     : 11200    (Ratio:   1.55%)
  Ternary    : 2758     (Ratio:   0.38%)
  Conflict   : 722221   (Average Length:  688.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 722221   (Average: 12.54 Max: 804 Sum: 9055371)
  Executed   : 722120   (Average: 12.53 Max: 804 Sum: 9052238 Ratio:  99.97%)
  Bounded    : 101      (Average: 31.02 Max: 117 Sum:   3133 Ratio:   0.03%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 595276   (Eliminated:    0 Frozen: 191082)
Constraints  : 4421087  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 8.43s
Memory:		 701MB (+0MB)
UNKNOWN
Iteration Time:	 8.48s

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

Models       : 0+
Calls        : 86
Time         : 593.536s (Solving: 569.38s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 593.636s

Choices      : 10709382 (Domain: 10571681)
Conflicts    : 730159   (Analyzed: 730156)
Restarts     : 8202     (Average: 89.02 Last: 172)
Model-Level  : 115.0   
Problems     : 86       (Average Length: 90.20 Splits: 0)
Lemmas       : 730156   (Deleted: 692780)
  Binary     : 11262    (Ratio:   1.54%)
  Ternary    : 2768     (Ratio:   0.38%)
  Conflict   : 730156   (Average Length:  683.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 730156   (Average: 12.47 Max: 804 Sum: 9106231)
  Executed   : 730055   (Average: 12.47 Max: 804 Sum: 9103098 Ratio:  99.97%)
  Bounded    : 101      (Average: 31.02 Max: 117 Sum:   3133 Ratio:   0.03%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 595276   (Eliminated:    0 Frozen: 191082)
Constraints  : 4421087  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 3.31s
Memory:		 701MB (+0MB)
UNKNOWN
Iteration Time:	 3.37s

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

Models       : 0+
Calls        : 87
Time         : 602.390s (Solving: 578.09s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 602.496s

Choices      : 10752690 (Domain: 10614989)
Conflicts    : 738328   (Analyzed: 738325)
Restarts     : 8302     (Average: 88.93 Last: 172)
Model-Level  : 115.0   
Problems     : 87       (Average Length: 90.51 Splits: 0)
Lemmas       : 738325   (Deleted: 700549)
  Binary     : 11278    (Ratio:   1.53%)
  Ternary    : 2776     (Ratio:   0.38%)
  Conflict   : 738325   (Average Length:  688.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 738325   (Average: 12.38 Max: 804 Sum: 9139428)
  Executed   : 738224   (Average: 12.37 Max: 804 Sum: 9136295 Ratio:  99.97%)
  Bounded    : 101      (Average: 31.02 Max: 117 Sum:   3133 Ratio:   0.03%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 595276   (Eliminated:    0 Frozen: 191082)
Constraints  : 4421087  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 8.81s
Memory:		 701MB (+0MB)
UNKNOWN
Iteration Time:	 8.86s

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

Models       : 0+
Calls        : 88
Time         : 608.995s (Solving: 584.56s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 609.108s

Choices      : 10813516 (Domain: 10675815)
Conflicts    : 746953   (Analyzed: 746950)
Restarts     : 8402     (Average: 88.90 Last: 172)
Model-Level  : 115.0   
Problems     : 88       (Average Length: 90.81 Splits: 0)
Lemmas       : 746950   (Deleted: 710805)
  Binary     : 11291    (Ratio:   1.51%)
  Ternary    : 2780     (Ratio:   0.37%)
  Conflict   : 746950   (Average Length:  689.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 746950   (Average: 12.29 Max: 804 Sum: 9180716)
  Executed   : 746849   (Average: 12.29 Max: 804 Sum: 9177583 Ratio:  99.97%)
  Bounded    : 101      (Average: 31.02 Max: 117 Sum:   3133 Ratio:   0.03%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 595276   (Eliminated:    0 Frozen: 191082)
Constraints  : 4421087  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

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

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

Models       : 0+
Calls        : 89
Time         : 615.995s (Solving: 591.44s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 616.112s

Choices      : 10890578 (Domain: 10752791)
Conflicts    : 755509   (Analyzed: 755506)
Restarts     : 8502     (Average: 88.86 Last: 172)
Model-Level  : 115.0   
Problems     : 89       (Average Length: 91.10 Splits: 0)
Lemmas       : 755506   (Deleted: 717125)
  Binary     : 11326    (Ratio:   1.50%)
  Ternary    : 2804     (Ratio:   0.37%)
  Conflict   : 755506   (Average Length:  691.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 755506   (Average: 12.22 Max: 804 Sum: 9234773)
  Executed   : 755405   (Average: 12.22 Max: 804 Sum: 9231640 Ratio:  99.97%)
  Bounded    : 101      (Average: 31.02 Max: 117 Sum:   3133 Ratio:   0.03%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 595276   (Eliminated:    0 Frozen: 191082)
Constraints  : 4421087  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

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

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

Models       : 0+
Calls        : 90
Time         : 623.170s (Solving: 598.47s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 623.292s

Choices      : 10962157 (Domain: 10824370)
Conflicts    : 764947   (Analyzed: 764944)
Restarts     : 8602     (Average: 88.93 Last: 172)
Model-Level  : 115.0   
Problems     : 90       (Average Length: 91.39 Splits: 0)
Lemmas       : 764944   (Deleted: 727704)
  Binary     : 11341    (Ratio:   1.48%)
  Ternary    : 2805     (Ratio:   0.37%)
  Conflict   : 764944   (Average Length:  692.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 764944   (Average: 12.14 Max: 804 Sum: 9284631)
  Executed   : 764843   (Average: 12.13 Max: 804 Sum: 9281498 Ratio:  99.97%)
  Bounded    : 101      (Average: 31.02 Max: 117 Sum:   3133 Ratio:   0.03%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 595276   (Eliminated:    0 Frozen: 191082)
Constraints  : 4421087  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

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

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

Models       : 0+
Calls        : 91
Time         : 632.132s (Solving: 607.28s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 632.256s

Choices      : 11167284 (Domain: 11026963)
Conflicts    : 774502   (Analyzed: 774499)
Restarts     : 8702     (Average: 89.00 Last: 172)
Model-Level  : 115.0   
Problems     : 91       (Average Length: 91.67 Splits: 0)
Lemmas       : 774499   (Deleted: 736613)
  Binary     : 11533    (Ratio:   1.49%)
  Ternary    : 2817     (Ratio:   0.36%)
  Conflict   : 774499   (Average Length:  693.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 774499   (Average: 12.21 Max: 804 Sum: 9454212)
  Executed   : 774398   (Average: 12.20 Max: 804 Sum: 9451079 Ratio:  99.97%)
  Bounded    : 101      (Average: 31.02 Max: 117 Sum:   3133 Ratio:   0.03%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 595276   (Eliminated:    0 Frozen: 191082)
Constraints  : 4421087  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

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

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

Models       : 0+
Calls        : 92
Time         : 640.000s (Solving: 614.98s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 640.128s

Choices      : 11248145 (Domain: 11107823)
Conflicts    : 783668   (Analyzed: 783665)
Restarts     : 8802     (Average: 89.03 Last: 184)
Model-Level  : 115.0   
Problems     : 92       (Average Length: 91.95 Splits: 0)
Lemmas       : 783665   (Deleted: 746031)
  Binary     : 11547    (Ratio:   1.47%)
  Ternary    : 2818     (Ratio:   0.36%)
  Conflict   : 783665   (Average Length:  693.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 783665   (Average: 12.13 Max: 804 Sum: 9509243)
  Executed   : 783564   (Average: 12.13 Max: 804 Sum: 9506110 Ratio:  99.97%)
  Bounded    : 101      (Average: 31.02 Max: 117 Sum:   3133 Ratio:   0.03%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 595276   (Eliminated:    0 Frozen: 191082)
Constraints  : 4421087  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 7.81s
Memory:		 701MB (+0MB)
UNKNOWN
Iteration Time:	 7.88s

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

Models       : 0+
Calls        : 93
Time         : 649.676s (Solving: 624.50s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 649.804s

Choices      : 11356158 (Domain: 11215833)
Conflicts    : 793553   (Analyzed: 793550)
Restarts     : 8902     (Average: 89.14 Last: 184)
Model-Level  : 115.0   
Problems     : 93       (Average Length: 92.22 Splits: 0)
Lemmas       : 793550   (Deleted: 755022)
  Binary     : 11594    (Ratio:   1.46%)
  Ternary    : 2832     (Ratio:   0.36%)
  Conflict   : 793550   (Average Length:  693.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 793550   (Average: 12.08 Max: 804 Sum: 9587789)
  Executed   : 793449   (Average: 12.08 Max: 804 Sum: 9584656 Ratio:  99.97%)
  Bounded    : 101      (Average: 31.02 Max: 117 Sum:   3133 Ratio:   0.03%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 595276   (Eliminated:    0 Frozen: 191082)
Constraints  : 4421087  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

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

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

Models       : 0+
Calls        : 94
Time         : 652.896s (Solving: 627.60s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 653.028s

Choices      : 11405512 (Domain: 11265187)
Conflicts    : 801159   (Analyzed: 801156)
Restarts     : 9002     (Average: 89.00 Last: 184)
Model-Level  : 115.0   
Problems     : 94       (Average Length: 92.48 Splits: 0)
Lemmas       : 801156   (Deleted: 762483)
  Binary     : 11661    (Ratio:   1.46%)
  Ternary    : 2841     (Ratio:   0.35%)
  Conflict   : 801156   (Average Length:  689.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 801156   (Average: 12.02 Max: 804 Sum: 9630252)
  Executed   : 801055   (Average: 12.02 Max: 804 Sum: 9627119 Ratio:  99.97%)
  Bounded    : 101      (Average: 31.02 Max: 117 Sum:   3133 Ratio:   0.03%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 595276   (Eliminated:    0 Frozen: 191082)
Constraints  : 4421087  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 3.18s
Memory:		 701MB (+0MB)
UNKNOWN
Iteration Time:	 3.22s

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

Models       : 0+
Calls        : 95
Time         : 663.475s (Solving: 638.06s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 663.612s

Choices      : 11460353 (Domain: 11320028)
Conflicts    : 810194   (Analyzed: 810191)
Restarts     : 9102     (Average: 89.01 Last: 184)
Model-Level  : 115.0   
Problems     : 95       (Average Length: 92.74 Splits: 0)
Lemmas       : 810191   (Deleted: 772040)
  Binary     : 11690    (Ratio:   1.44%)
  Ternary    : 2856     (Ratio:   0.35%)
  Conflict   : 810191   (Average Length:  698.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 810191   (Average: 11.94 Max: 804 Sum: 9673989)
  Executed   : 810090   (Average: 11.94 Max: 804 Sum: 9670856 Ratio:  99.97%)
  Bounded    : 101      (Average: 31.02 Max: 117 Sum:   3133 Ratio:   0.03%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 595276   (Eliminated:    0 Frozen: 191082)
Constraints  : 4421087  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 10.54s
Memory:		 701MB (+0MB)
UNKNOWN
Iteration Time:	 10.59s

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

Models       : 0+
Calls        : 96
Time         : 671.564s (Solving: 645.99s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 671.704s

Choices      : 11542933 (Domain: 11402608)
Conflicts    : 818906   (Analyzed: 818903)
Restarts     : 9202     (Average: 88.99 Last: 184)
Model-Level  : 115.0   
Problems     : 96       (Average Length: 92.99 Splits: 0)
Lemmas       : 818903   (Deleted: 780806)
  Binary     : 11741    (Ratio:   1.43%)
  Ternary    : 2872     (Ratio:   0.35%)
  Conflict   : 818903   (Average Length:  701.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 818903   (Average: 11.89 Max: 804 Sum: 9739410)
  Executed   : 818802   (Average: 11.89 Max: 804 Sum: 9736277 Ratio:  99.97%)
  Bounded    : 101      (Average: 31.02 Max: 117 Sum:   3133 Ratio:   0.03%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 595276   (Eliminated:    0 Frozen: 191082)
Constraints  : 4421087  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 8.03s
Memory:		 701MB (+0MB)
UNKNOWN
Iteration Time:	 8.09s

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

Models       : 0+
Calls        : 97
Time         : 678.129s (Solving: 652.42s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 678.268s

Choices      : 11604353 (Domain: 11464028)
Conflicts    : 828070   (Analyzed: 828067)
Restarts     : 9302     (Average: 89.02 Last: 184)
Model-Level  : 115.0   
Problems     : 97       (Average Length: 93.24 Splits: 0)
Lemmas       : 828067   (Deleted: 789353)
  Binary     : 11764    (Ratio:   1.42%)
  Ternary    : 2873     (Ratio:   0.35%)
  Conflict   : 828067   (Average Length:  701.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 828067   (Average: 11.81 Max: 804 Sum: 9781652)
  Executed   : 827966   (Average: 11.81 Max: 804 Sum: 9778519 Ratio:  99.97%)
  Bounded    : 101      (Average: 31.02 Max: 117 Sum:   3133 Ratio:   0.03%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 595276   (Eliminated:    0 Frozen: 191082)
Constraints  : 4421087  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 6.52s
Memory:		 701MB (+0MB)
UNKNOWN
Iteration Time:	 6.57s

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

Models       : 0+
Calls        : 98
Time         : 685.727s (Solving: 659.89s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 685.868s

Choices      : 11670203 (Domain: 11529878)
Conflicts    : 837340   (Analyzed: 837337)
Restarts     : 9402     (Average: 89.06 Last: 184)
Model-Level  : 115.0   
Problems     : 98       (Average Length: 93.48 Splits: 0)
Lemmas       : 837337   (Deleted: 798391)
  Binary     : 11790    (Ratio:   1.41%)
  Ternary    : 2878     (Ratio:   0.34%)
  Conflict   : 837337   (Average Length:  705.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 837337   (Average: 11.74 Max: 804 Sum: 9826639)
  Executed   : 837236   (Average: 11.73 Max: 804 Sum: 9823506 Ratio:  99.97%)
  Bounded    : 101      (Average: 31.02 Max: 117 Sum:   3133 Ratio:   0.03%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 595276   (Eliminated:    0 Frozen: 191082)
Constraints  : 4421087  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

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

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

Models       : 0+
Calls        : 99
Time         : 693.616s (Solving: 667.62s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 693.764s

Choices      : 11743501 (Domain: 11603168)
Conflicts    : 846866   (Analyzed: 846863)
Restarts     : 9502     (Average: 89.12 Last: 184)
Model-Level  : 115.0   
Problems     : 99       (Average Length: 93.72 Splits: 0)
Lemmas       : 846863   (Deleted: 807535)
  Binary     : 11813    (Ratio:   1.39%)
  Ternary    : 2879     (Ratio:   0.34%)
  Conflict   : 846863   (Average Length:  706.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 846863   (Average: 11.67 Max: 804 Sum: 9878846)
  Executed   : 846762   (Average: 11.66 Max: 804 Sum: 9875713 Ratio:  99.97%)
  Bounded    : 101      (Average: 31.02 Max: 117 Sum:   3133 Ratio:   0.03%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 595276   (Eliminated:    0 Frozen: 191082)
Constraints  : 4421087  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 7.83s
Memory:		 701MB (+0MB)
UNKNOWN
Iteration Time:	 7.90s

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

Models       : 0+
Calls        : 100
Time         : 702.056s (Solving: 675.93s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 702.208s

Choices      : 11827741 (Domain: 11687407)
Conflicts    : 856967   (Analyzed: 856964)
Restarts     : 9602     (Average: 89.25 Last: 184)
Model-Level  : 115.0   
Problems     : 100      (Average Length: 93.95 Splits: 0)
Lemmas       : 856964   (Deleted: 816890)
  Binary     : 11828    (Ratio:   1.38%)
  Ternary    : 2882     (Ratio:   0.34%)
  Conflict   : 856964   (Average Length:  708.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 856964   (Average: 11.60 Max: 804 Sum: 9940425)
  Executed   : 856863   (Average: 11.60 Max: 804 Sum: 9937292 Ratio:  99.97%)
  Bounded    : 101      (Average: 31.02 Max: 117 Sum:   3133 Ratio:   0.03%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 595276   (Eliminated:    0 Frozen: 191082)
Constraints  : 4421087  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

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

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

Models       : 0+
Calls        : 101
Time         : 710.878s (Solving: 684.61s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 711.032s

Choices      : 11924133 (Domain: 11783530)
Conflicts    : 866234   (Analyzed: 866231)
Restarts     : 9702     (Average: 89.28 Last: 184)
Model-Level  : 115.0   
Problems     : 101      (Average Length: 94.18 Splits: 0)
Lemmas       : 866231   (Deleted: 826877)
  Binary     : 11848    (Ratio:   1.37%)
  Ternary    : 2889     (Ratio:   0.33%)
  Conflict   : 866231   (Average Length:  709.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 866231   (Average: 11.56 Max: 804 Sum: 10009326)
  Executed   : 866130   (Average: 11.55 Max: 804 Sum: 10006193 Ratio:  99.97%)
  Bounded    : 101      (Average: 31.02 Max: 117 Sum:   3133 Ratio:   0.03%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 595276   (Eliminated:    0 Frozen: 191082)
Constraints  : 4421087  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

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

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

Models       : 0+
Calls        : 102
Time         : 720.063s (Solving: 693.67s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 720.220s

Choices      : 12024984 (Domain: 11884377)
Conflicts    : 876018   (Analyzed: 876015)
Restarts     : 9802     (Average: 89.37 Last: 184)
Model-Level  : 115.0   
Problems     : 102      (Average Length: 94.40 Splits: 0)
Lemmas       : 876015   (Deleted: 836030)
  Binary     : 11857    (Ratio:   1.35%)
  Ternary    : 2892     (Ratio:   0.33%)
  Conflict   : 876015   (Average Length:  709.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 876015   (Average: 11.51 Max: 804 Sum: 10081329)
  Executed   : 875914   (Average: 11.50 Max: 804 Sum: 10078196 Ratio:  99.97%)
  Bounded    : 101      (Average: 31.02 Max: 117 Sum:   3133 Ratio:   0.03%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 595276   (Eliminated:    0 Frozen: 191082)
Constraints  : 4421087  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

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

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

Models       : 0+
Calls        : 103
Time         : 729.881s (Solving: 703.35s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 730.040s

Choices      : 12380022 (Domain: 12236675)
Conflicts    : 884930   (Analyzed: 884927)
Restarts     : 9902     (Average: 89.37 Last: 184)
Model-Level  : 115.0   
Problems     : 103      (Average Length: 94.62 Splits: 0)
Lemmas       : 884927   (Deleted: 845293)
  Binary     : 12077    (Ratio:   1.36%)
  Ternary    : 2911     (Ratio:   0.33%)
  Conflict   : 884927   (Average Length:  713.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 884927   (Average: 11.74 Max: 804 Sum: 10387706)
  Executed   : 884826   (Average: 11.73 Max: 804 Sum: 10384573 Ratio:  99.97%)
  Bounded    : 101      (Average: 31.02 Max: 117 Sum:   3133 Ratio:   0.03%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 595276   (Eliminated:    0 Frozen: 191082)
Constraints  : 4421087  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

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

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

Models       : 0+
Calls        : 104
Time         : 732.460s (Solving: 705.81s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 732.620s

Choices      : 12414794 (Domain: 12271447)
Conflicts    : 892338   (Analyzed: 892335)
Restarts     : 10002    (Average: 89.22 Last: 184)
Model-Level  : 115.0   
Problems     : 104      (Average Length: 94.84 Splits: 0)
Lemmas       : 892335   (Deleted: 851570)
  Binary     : 12115    (Ratio:   1.36%)
  Ternary    : 2915     (Ratio:   0.33%)
  Conflict   : 892335   (Average Length:  708.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 892335   (Average: 11.67 Max: 804 Sum: 10413513)
  Executed   : 892234   (Average: 11.67 Max: 804 Sum: 10410380 Ratio:  99.97%)
  Bounded    : 101      (Average: 31.02 Max: 117 Sum:   3133 Ratio:   0.03%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 595276   (Eliminated:    0 Frozen: 191082)
Constraints  : 4421087  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

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

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

Models       : 0+
Calls        : 105
Time         : 742.371s (Solving: 715.57s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 742.536s

Choices      : 12485724 (Domain: 12342377)
Conflicts    : 901675   (Analyzed: 901672)
Restarts     : 10102    (Average: 89.26 Last: 184)
Model-Level  : 115.0   
Problems     : 105      (Average Length: 95.05 Splits: 0)
Lemmas       : 901672   (Deleted: 861412)
  Binary     : 12151    (Ratio:   1.35%)
  Ternary    : 2921     (Ratio:   0.32%)
  Conflict   : 901672   (Average Length:  717.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 901672   (Average: 11.61 Max: 804 Sum: 10470229)
  Executed   : 901571   (Average: 11.61 Max: 804 Sum: 10467096 Ratio:  99.97%)
  Bounded    : 101      (Average: 31.02 Max: 117 Sum:   3133 Ratio:   0.03%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 595276   (Eliminated:    0 Frozen: 191082)
Constraints  : 4421087  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

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

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

Models       : 0+
Calls        : 106
Time         : 751.446s (Solving: 724.50s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 751.616s

Choices      : 12572967 (Domain: 12429620)
Conflicts    : 910932   (Analyzed: 910929)
Restarts     : 10202    (Average: 89.29 Last: 184)
Model-Level  : 115.0   
Problems     : 106      (Average Length: 95.25 Splits: 0)
Lemmas       : 910929   (Deleted: 871578)
  Binary     : 12217    (Ratio:   1.34%)
  Ternary    : 2928     (Ratio:   0.32%)
  Conflict   : 910929   (Average Length:  724.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 910929   (Average: 11.57 Max: 804 Sum: 10538307)
  Executed   : 910828   (Average: 11.57 Max: 804 Sum: 10535174 Ratio:  99.97%)
  Bounded    : 101      (Average: 31.02 Max: 117 Sum:   3133 Ratio:   0.03%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 595276   (Eliminated:    0 Frozen: 191082)
Constraints  : 4421087  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 9.03s
Memory:		 701MB (+0MB)
UNKNOWN
Iteration Time:	 9.08s

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

Models       : 0+
Calls        : 107
Time         : 758.286s (Solving: 731.21s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 758.460s

Choices      : 12635599 (Domain: 12492247)
Conflicts    : 920355   (Analyzed: 920352)
Restarts     : 10302    (Average: 89.34 Last: 184)
Model-Level  : 115.0   
Problems     : 107      (Average Length: 95.46 Splits: 0)
Lemmas       : 920352   (Deleted: 879581)
  Binary     : 12233    (Ratio:   1.33%)
  Ternary    : 2928     (Ratio:   0.32%)
  Conflict   : 920352   (Average Length:  724.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 920352   (Average: 11.50 Max: 804 Sum: 10581898)
  Executed   : 920251   (Average: 11.49 Max: 804 Sum: 10578765 Ratio:  99.97%)
  Bounded    : 101      (Average: 31.02 Max: 117 Sum:   3133 Ratio:   0.03%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 595276   (Eliminated:    0 Frozen: 191082)
Constraints  : 4421087  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 6.79s
Memory:		 701MB (+0MB)
UNKNOWN
Iteration Time:	 6.85s

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

Models       : 0+
Calls        : 108
Time         : 765.679s (Solving: 738.45s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 765.856s

Choices      : 12704465 (Domain: 12561104)
Conflicts    : 929262   (Analyzed: 929259)
Restarts     : 10402    (Average: 89.33 Last: 184)
Model-Level  : 115.0   
Problems     : 108      (Average Length: 95.66 Splits: 0)
Lemmas       : 929259   (Deleted: 888870)
  Binary     : 12254    (Ratio:   1.32%)
  Ternary    : 2936     (Ratio:   0.32%)
  Conflict   : 929259   (Average Length:  726.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 929259   (Average: 11.44 Max: 804 Sum: 10629083)
  Executed   : 929158   (Average: 11.43 Max: 804 Sum: 10625950 Ratio:  99.97%)
  Bounded    : 101      (Average: 31.02 Max: 117 Sum:   3133 Ratio:   0.03%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 595276   (Eliminated:    0 Frozen: 191082)
Constraints  : 4421087  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

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

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

Models       : 0+
Calls        : 109
Time         : 773.496s (Solving: 746.11s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 773.676s

Choices      : 12791375 (Domain: 12647820)
Conflicts    : 938134   (Analyzed: 938131)
Restarts     : 10502    (Average: 89.33 Last: 184)
Model-Level  : 115.0   
Problems     : 109      (Average Length: 95.85 Splits: 0)
Lemmas       : 938131   (Deleted: 897595)
  Binary     : 12348    (Ratio:   1.32%)
  Ternary    : 2947     (Ratio:   0.31%)
  Conflict   : 938131   (Average Length:  726.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 938131   (Average: 11.40 Max: 804 Sum: 10692359)
  Executed   : 938030   (Average: 11.39 Max: 804 Sum: 10689226 Ratio:  99.97%)
  Bounded    : 101      (Average: 31.02 Max: 117 Sum:   3133 Ratio:   0.03%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 595276   (Eliminated:    0 Frozen: 191082)
Constraints  : 4421087  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

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

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

Models       : 0+
Calls        : 110
Time         : 781.078s (Solving: 753.54s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 781.260s

Choices      : 12865902 (Domain: 12722324)
Conflicts    : 947574   (Analyzed: 947571)
Restarts     : 10602    (Average: 89.38 Last: 184)
Model-Level  : 115.0   
Problems     : 110      (Average Length: 96.05 Splits: 0)
Lemmas       : 947571   (Deleted: 906268)
  Binary     : 12356    (Ratio:   1.30%)
  Ternary    : 2949     (Ratio:   0.31%)
  Conflict   : 947571   (Average Length:  727.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 947571   (Average: 11.34 Max: 804 Sum: 10742954)
  Executed   : 947470   (Average: 11.33 Max: 804 Sum: 10739821 Ratio:  99.97%)
  Bounded    : 101      (Average: 31.02 Max: 117 Sum:   3133 Ratio:   0.03%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 595276   (Eliminated:    0 Frozen: 191082)
Constraints  : 4421087  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 7.53s
Memory:		 701MB (+0MB)
UNKNOWN
Iteration Time:	 7.59s

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

Models       : 0+
Calls        : 111
Time         : 788.621s (Solving: 760.96s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 788.804s

Choices      : 12943246 (Domain: 12799668)
Conflicts    : 956305   (Analyzed: 956302)
Restarts     : 10702    (Average: 89.36 Last: 184)
Model-Level  : 115.0   
Problems     : 111      (Average Length: 96.23 Splits: 0)
Lemmas       : 956302   (Deleted: 915504)
  Binary     : 12373    (Ratio:   1.29%)
  Ternary    : 2955     (Ratio:   0.31%)
  Conflict   : 956302   (Average Length:  729.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 956302   (Average: 11.28 Max: 804 Sum: 10789739)
  Executed   : 956201   (Average: 11.28 Max: 804 Sum: 10786606 Ratio:  99.97%)
  Bounded    : 101      (Average: 31.02 Max: 117 Sum:   3133 Ratio:   0.03%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 595276   (Eliminated:    0 Frozen: 191082)
Constraints  : 4421087  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 7.51s
Memory:		 701MB (+0MB)
UNKNOWN
Iteration Time:	 7.55s

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

Models       : 0+
Calls        : 112
Time         : 798.694s (Solving: 770.88s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 798.880s

Choices      : 13040307 (Domain: 12896729)
Conflicts    : 966555   (Analyzed: 966552)
Restarts     : 10802    (Average: 89.48 Last: 184)
Model-Level  : 115.0   
Problems     : 112      (Average Length: 96.42 Splits: 0)
Lemmas       : 966552   (Deleted: 924115)
  Binary     : 12395    (Ratio:   1.28%)
  Ternary    : 2957     (Ratio:   0.31%)
  Conflict   : 966552   (Average Length:  731.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 966552   (Average: 11.23 Max: 804 Sum: 10854853)
  Executed   : 966451   (Average: 11.23 Max: 804 Sum: 10851720 Ratio:  99.97%)
  Bounded    : 101      (Average: 31.02 Max: 117 Sum:   3133 Ratio:   0.03%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 595276   (Eliminated:    0 Frozen: 191082)
Constraints  : 4421087  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

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

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

Models       : 0+
Calls        : 113
Time         : 802.753s (Solving: 774.81s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 802.940s

Choices      : 13111674 (Domain: 12968096)
Conflicts    : 974599   (Analyzed: 974596)
Restarts     : 10902    (Average: 89.40 Last: 184)
Model-Level  : 115.0   
Problems     : 113      (Average Length: 96.60 Splits: 0)
Lemmas       : 974596   (Deleted: 931881)
  Binary     : 12454    (Ratio:   1.28%)
  Ternary    : 2975     (Ratio:   0.31%)
  Conflict   : 974596   (Average Length:  728.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 974596   (Average: 11.21 Max: 804 Sum: 10920351)
  Executed   : 974495   (Average: 11.20 Max: 804 Sum: 10917218 Ratio:  99.97%)
  Bounded    : 101      (Average: 31.02 Max: 117 Sum:   3133 Ratio:   0.03%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 595276   (Eliminated:    0 Frozen: 191082)
Constraints  : 4421087  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 4.02s
Memory:		 701MB (+0MB)
UNKNOWN
Iteration Time:	 4.06s

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

Models       : 0+
Calls        : 114
Time         : 812.869s (Solving: 784.81s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 813.064s

Choices      : 13185537 (Domain: 13041959)
Conflicts    : 983518   (Analyzed: 983515)
Restarts     : 11002    (Average: 89.39 Last: 184)
Model-Level  : 115.0   
Problems     : 114      (Average Length: 96.78 Splits: 0)
Lemmas       : 983515   (Deleted: 941911)
  Binary     : 12505    (Ratio:   1.27%)
  Ternary    : 2986     (Ratio:   0.30%)
  Conflict   : 983515   (Average Length:  737.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 983515   (Average: 11.16 Max: 804 Sum: 10979427)
  Executed   : 983414   (Average: 11.16 Max: 804 Sum: 10976294 Ratio:  99.97%)
  Bounded    : 101      (Average: 31.02 Max: 117 Sum:   3133 Ratio:   0.03%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 595276   (Eliminated:    0 Frozen: 191082)
Constraints  : 4421087  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

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

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

Models       : 0+
Calls        : 115
Time         : 820.835s (Solving: 792.64s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 821.036s

Choices      : 13255710 (Domain: 13112132)
Conflicts    : 992455   (Analyzed: 992452)
Restarts     : 11102    (Average: 89.39 Last: 184)
Model-Level  : 115.0   
Problems     : 115      (Average Length: 96.96 Splits: 0)
Lemmas       : 992452   (Deleted: 950714)
  Binary     : 12552    (Ratio:   1.26%)
  Ternary    : 3001     (Ratio:   0.30%)
  Conflict   : 992452   (Average Length:  740.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 992452   (Average: 11.12 Max: 804 Sum: 11032012)
  Executed   : 992351   (Average: 11.11 Max: 804 Sum: 11028879 Ratio:  99.97%)
  Bounded    : 101      (Average: 31.02 Max: 117 Sum:   3133 Ratio:   0.03%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 595276   (Eliminated:    0 Frozen: 191082)
Constraints  : 4421087  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

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

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

Models       : 0+
Calls        : 116
Time         : 827.584s (Solving: 799.26s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 827.788s

Choices      : 13320597 (Domain: 13177016)
Conflicts    : 1001486  (Analyzed: 1001483)
Restarts     : 11202    (Average: 89.40 Last: 184)
Model-Level  : 115.0   
Problems     : 116      (Average Length: 97.13 Splits: 0)
Lemmas       : 1001483  (Deleted: 959507)
  Binary     : 12570    (Ratio:   1.26%)
  Ternary    : 3008     (Ratio:   0.30%)
  Conflict   : 1001483  (Average Length:  740.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 1001483  (Average: 11.06 Max: 804 Sum: 11079040)
  Executed   : 1001382  (Average: 11.06 Max: 804 Sum: 11075907 Ratio:  99.97%)
  Bounded    : 101      (Average: 31.02 Max: 117 Sum:   3133 Ratio:   0.03%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 595276   (Eliminated:    0 Frozen: 191082)
Constraints  : 4421087  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

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

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

Models       : 0+
Calls        : 117
Time         : 836.118s (Solving: 807.67s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 836.324s

Choices      : 13400827 (Domain: 13257219)
Conflicts    : 1011715  (Analyzed: 1011712)
Restarts     : 11302    (Average: 89.52 Last: 184)
Model-Level  : 115.0   
Problems     : 117      (Average Length: 97.30 Splits: 0)
Lemmas       : 1011712  (Deleted: 968327)
  Binary     : 12615    (Ratio:   1.25%)
  Ternary    : 3012     (Ratio:   0.30%)
  Conflict   : 1011712  (Average Length:  742.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 1011712  (Average: 11.01 Max: 804 Sum: 11136699)
  Executed   : 1011611  (Average: 11.00 Max: 804 Sum: 11133566 Ratio:  99.97%)
  Bounded    : 101      (Average: 31.02 Max: 117 Sum:   3133 Ratio:   0.03%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 595276   (Eliminated:    0 Frozen: 191082)
Constraints  : 4421087  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 8.49s
Memory:		 701MB (+0MB)
UNKNOWN
Iteration Time:	 8.54s

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

Models       : 0+
Calls        : 118
Time         : 843.607s (Solving: 815.01s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 843.812s

Choices      : 13473329 (Domain: 13329698)
Conflicts    : 1020876  (Analyzed: 1020873)
Restarts     : 11402    (Average: 89.53 Last: 184)
Model-Level  : 115.0   
Problems     : 118      (Average Length: 97.47 Splits: 0)
Lemmas       : 1020873  (Deleted: 978408)
  Binary     : 12634    (Ratio:   1.24%)
  Ternary    : 3018     (Ratio:   0.30%)
  Conflict   : 1020873  (Average Length:  744.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 1020873  (Average: 10.96 Max: 804 Sum: 11186313)
  Executed   : 1020772  (Average: 10.95 Max: 804 Sum: 11183180 Ratio:  99.97%)
  Bounded    : 101      (Average: 31.02 Max: 117 Sum:   3133 Ratio:   0.03%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 595276   (Eliminated:    0 Frozen: 191082)
Constraints  : 4421087  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

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

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

Models       : 0+
Calls        : 119
Time         : 851.708s (Solving: 822.96s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 851.916s

Choices      : 13557863 (Domain: 13414212)
Conflicts    : 1030146  (Analyzed: 1030143)
Restarts     : 11502    (Average: 89.56 Last: 184)
Model-Level  : 115.0   
Problems     : 119      (Average Length: 97.63 Splits: 0)
Lemmas       : 1030143  (Deleted: 987414)
  Binary     : 12652    (Ratio:   1.23%)
  Ternary    : 3032     (Ratio:   0.29%)
  Conflict   : 1030143  (Average Length:  745.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 1030143  (Average: 10.92 Max: 804 Sum: 11244412)
  Executed   : 1030042  (Average: 10.91 Max: 804 Sum: 11241279 Ratio:  99.97%)
  Bounded    : 101      (Average: 31.02 Max: 117 Sum:   3133 Ratio:   0.03%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 595276   (Eliminated:    0 Frozen: 191082)
Constraints  : 4421087  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

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

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

Models       : 0+
Calls        : 120
Time         : 860.236s (Solving: 831.34s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 860.448s

Choices      : 13712973 (Domain: 13568567)
Conflicts    : 1039314  (Analyzed: 1039311)
Restarts     : 11602    (Average: 89.58 Last: 184)
Model-Level  : 115.0   
Problems     : 120      (Average Length: 97.79 Splits: 0)
Lemmas       : 1039311  (Deleted: 996426)
  Binary     : 12746    (Ratio:   1.23%)
  Ternary    : 3043     (Ratio:   0.29%)
  Conflict   : 1039311  (Average Length:  746.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 1039311  (Average: 10.94 Max: 804 Sum: 11366683)
  Executed   : 1039210  (Average: 10.93 Max: 804 Sum: 11363550 Ratio:  99.97%)
  Bounded    : 101      (Average: 31.02 Max: 117 Sum:   3133 Ratio:   0.03%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 595276   (Eliminated:    0 Frozen: 191082)
Constraints  : 4421087  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

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

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

Models       : 0+
Calls        : 121
Time         : 862.239s (Solving: 833.19s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 862.452s

Choices      : 13745614 (Domain: 13601208)
Conflicts    : 1046538  (Analyzed: 1046535)
Restarts     : 11702    (Average: 89.43 Last: 184)
Model-Level  : 115.0   
Problems     : 121      (Average Length: 97.95 Splits: 0)
Lemmas       : 1046535  (Deleted: 1002872)
  Binary     : 12779    (Ratio:   1.22%)
  Ternary    : 3048     (Ratio:   0.29%)
  Conflict   : 1046535  (Average Length:  741.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 1046535  (Average: 10.88 Max: 804 Sum: 11389452)
  Executed   : 1046434  (Average: 10.88 Max: 804 Sum: 11386319 Ratio:  99.97%)
  Bounded    : 101      (Average: 31.02 Max: 117 Sum:   3133 Ratio:   0.03%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 595276   (Eliminated:    0 Frozen: 191082)
Constraints  : 4421087  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 1.95s
Memory:		 701MB (+0MB)
UNKNOWN
Iteration Time:	 2.01s

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

Models       : 0+
Calls        : 122
Time         : 870.750s (Solving: 841.55s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 870.968s

Choices      : 13808870 (Domain: 13664464)
Conflicts    : 1054704  (Analyzed: 1054701)
Restarts     : 11802    (Average: 89.37 Last: 184)
Model-Level  : 115.0   
Problems     : 122      (Average Length: 98.11 Splits: 0)
Lemmas       : 1054701  (Deleted: 1010599)
  Binary     : 12848    (Ratio:   1.22%)
  Ternary    : 3058     (Ratio:   0.29%)
  Conflict   : 1054701  (Average Length:  751.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 1054701  (Average: 10.84 Max: 804 Sum: 11436954)
  Executed   : 1054600  (Average: 10.84 Max: 804 Sum: 11433821 Ratio:  99.97%)
  Bounded    : 101      (Average: 31.02 Max: 117 Sum:   3133 Ratio:   0.03%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 595276   (Eliminated:    0 Frozen: 191082)
Constraints  : 4421087  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 8.46s
Memory:		 701MB (+0MB)
UNKNOWN
Iteration Time:	 8.52s

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

Models       : 0+
Calls        : 123
Time         : 879.378s (Solving: 850.03s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 879.600s

Choices      : 13884685 (Domain: 13740279)
Conflicts    : 1063387  (Analyzed: 1063384)
Restarts     : 11902    (Average: 89.34 Last: 184)
Model-Level  : 115.0   
Problems     : 123      (Average Length: 98.26 Splits: 0)
Lemmas       : 1063384  (Deleted: 1020841)
  Binary     : 12891    (Ratio:   1.21%)
  Ternary    : 3083     (Ratio:   0.29%)
  Conflict   : 1063384  (Average Length:  757.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 1063384  (Average: 10.81 Max: 804 Sum: 11494856)
  Executed   : 1063283  (Average: 10.81 Max: 804 Sum: 11491723 Ratio:  99.97%)
  Bounded    : 101      (Average: 31.02 Max: 117 Sum:   3133 Ratio:   0.03%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 595276   (Eliminated:    0 Frozen: 191082)
Constraints  : 4421087  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

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

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

Models       : 0+
Calls        : 124
Time         : 885.866s (Solving: 856.36s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 886.092s

Choices      : 13950526 (Domain: 13806057)
Conflicts    : 1072375  (Analyzed: 1072372)
Restarts     : 12002    (Average: 89.35 Last: 184)
Model-Level  : 115.0   
Problems     : 124      (Average Length: 98.41 Splits: 0)
Lemmas       : 1072372  (Deleted: 1029078)
  Binary     : 12910    (Ratio:   1.20%)
  Ternary    : 3093     (Ratio:   0.29%)
  Conflict   : 1072372  (Average Length:  757.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 1072372  (Average: 10.76 Max: 804 Sum: 11541621)
  Executed   : 1072271  (Average: 10.76 Max: 804 Sum: 11538488 Ratio:  99.97%)
  Bounded    : 101      (Average: 31.02 Max: 117 Sum:   3133 Ratio:   0.03%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 595276   (Eliminated:    0 Frozen: 191082)
Constraints  : 4421087  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

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

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

Models       : 0+
Calls        : 125
Time         : 894.113s (Solving: 864.48s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 894.344s

Choices      : 14023841 (Domain: 13879370)
Conflicts    : 1081352  (Analyzed: 1081349)
Restarts     : 12102    (Average: 89.35 Last: 184)
Model-Level  : 115.0   
Problems     : 125      (Average Length: 98.56 Splits: 0)
Lemmas       : 1081349  (Deleted: 1037874)
  Binary     : 12991    (Ratio:   1.20%)
  Ternary    : 3108     (Ratio:   0.29%)
  Conflict   : 1081349  (Average Length:  760.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 1081349  (Average: 10.72 Max: 804 Sum: 11595129)
  Executed   : 1081248  (Average: 10.72 Max: 804 Sum: 11591996 Ratio:  99.97%)
  Bounded    : 101      (Average: 31.02 Max: 117 Sum:   3133 Ratio:   0.03%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 595276   (Eliminated:    0 Frozen: 191082)
Constraints  : 4421087  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 8.21s
Memory:		 701MB (+0MB)
UNKNOWN
Iteration Time:	 8.25s

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

INTERRUPTED  : 1

Models       : 0+
Calls        : 126
Time         : 894.335s (Solving: 864.58s 1st Model: 0.00s Unsat: 3.47s)
CPU Time     : 894.544s

Choices      : 14024340 (Domain: 13879869)
Conflicts    : 1081471  (Analyzed: 1081468)
Restarts     : 12103    (Average: 89.36 Last: 184)
Model-Level  : 115.0   
Problems     : 126      (Average Length: 98.71 Splits: 0)
Lemmas       : 1081468  (Deleted: 1037874)
  Binary     : 12991    (Ratio:   1.20%)
  Ternary    : 3108     (Ratio:   0.29%)
  Conflict   : 1081468  (Average Length:  760.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 1081468  (Average: 10.72 Max: 804 Sum: 11595494)
  Executed   : 1081367  (Average: 10.72 Max: 804 Sum: 11592361 Ratio:  99.97%)
  Bounded    : 101      (Average: 31.02 Max: 117 Sum:   3133 Ratio:   0.03%)

Rules        : 62994    (Original: 61599)
Atoms        : 50308   
Bodies       : 11595    (Original: 10199)
  Count      : 252      (Original: 531)
Equivalences : 3261     (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight        : Yes
Variables    : 595276   (Eliminated:    0 Frozen: 191082)
Constraints  : 4421087  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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


