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-10.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-10.pddl
Parsing...
Parsing: [0.030s CPU, 0.035s wall-clock]
Normalizing task... [0.000s CPU, 0.003s wall-clock]
Instantiating...
Generating Datalog program... [0.010s CPU, 0.009s wall-clock]
Normalizing Datalog program...
Normalizing Datalog program: [0.040s CPU, 0.044s wall-clock]
Preparing model... [0.030s CPU, 0.025s wall-clock]
Generated 115 rules.
Computing model... [0.450s CPU, 0.450s wall-clock]
2784 relevant atoms
2893 auxiliary atoms
5677 final queue length
9793 total queue pushes
Completing instantiation... [0.870s CPU, 0.867s wall-clock]
Instantiating: [1.400s CPU, 1.401s wall-clock]
Computing fact groups...
Finding invariants...
24 initial candidates
Finding invariants: [0.130s CPU, 0.131s wall-clock]
Checking invariant weight... [0.010s CPU, 0.001s wall-clock]
Instantiating groups... [0.000s CPU, 0.008s wall-clock]
Collecting mutex groups... [0.000s CPU, 0.001s wall-clock]
Choosing groups...
292 uncovered facts
Choosing groups: [0.010s CPU, 0.002s wall-clock]
Building translation key... [0.010s CPU, 0.011s wall-clock]
Computing fact groups: [0.180s CPU, 0.176s wall-clock]
Building STRIPS to SAS dictionary... [0.000s CPU, 0.003s wall-clock]
Building dictionary for full mutex groups... [0.010s CPU, 0.006s wall-clock]
Building mutex information...
Building mutex information: [0.000s CPU, 0.003s wall-clock]
Translating task...
Processing axioms...
Simplifying axioms... [0.000s CPU, 0.000s wall-clock]
Processing axioms: [0.050s CPU, 0.047s wall-clock]
Translating task: [0.890s CPU, 0.890s wall-clock]
3276 effect conditions simplified
0 implied preconditions added
Detecting unreachable propositions...
0 operators removed
0 axioms removed
3 propositions removed
Detecting unreachable propositions: [0.440s CPU, 0.437s wall-clock]
Reordering and filtering variables...
295 of 295 variables necessary.
14 of 17 mutex groups necessary.
1958 of 1958 operators necessary.
0 of 0 axiom rules necessary.
Reordering and filtering variables: [0.300s CPU, 0.304s wall-clock]
Translator variables: 295
Translator derived variables: 0
Translator facts: 617
Translator goal facts: 12
Translator mutex groups: 14
Translator total mutex groups size: 42
Translator operators: 1958
Translator axioms: 0
Translator task size: 18764
Translator peak memory: 47052 KB
Writing output... [0.310s CPU, 0.342s wall-clock]
Done! [3.600s CPU, 3.635s wall-clock]
planner.py version 0.0.1

Time:	 0.76s
Memory: 101MB

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

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

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

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

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

Choices      : 158      (Domain: 32)
Conflicts    : 4        (Analyzed: 4)
Restarts     : 0       
Model-Level  : 148.0   
Problems     : 2        (Average Length: 4.50 Splits: 0)
Lemmas       : 4        (Deleted: 0)
  Binary     : 2        (Ratio:  50.00%)
  Ternary    : 0        (Ratio:   0.00%)
  Conflict   : 4        (Average Length:   15.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 4        (Average:  4.50 Max:  14 Sum:     18)
  Executed   : 3        (Average:  4.25 Max:  14 Sum:     17 Ratio:  94.44%)
  Bounded    : 1        (Average:  1.00 Max:   1 Sum:      1 Ratio:   5.56%)

Rules        : 54149   
Atoms        : 54149   
Bodies       : 1        (Original: 0)
Tight        : Yes
Variables    : 14506    (Eliminated:    0 Frozen:  150)
Constraints  : 48947    (Binary:  95.2% Ternary:   3.3% Other:   1.4%)

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

[endof: stats after solve call]
Solving Time:	 0.02s
Memory:		 176MB (+3MB)
SAT
Testing...
NOT SERIALIZABLE
Testing Time:	 0.76s
Memory:		 203MB (+27MB)
Solving...
[start: stats after solve call]

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

Choices      : 176      (Domain: 33)
Conflicts    : 13       (Analyzed: 12)
Restarts     : 0       
Model-Level  : 148.0   
Problems     : 3        (Average Length: 5.33 Splits: 0)
Lemmas       : 12       (Deleted: 0)
  Binary     : 4        (Ratio:  33.33%)
  Ternary    : 4        (Ratio:  33.33%)
  Conflict   : 12       (Average Length:    7.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 12       (Average:  3.17 Max:  14 Sum:     38)
  Executed   : 9        (Average:  2.92 Max:  14 Sum:     35 Ratio:  92.11%)
  Bounded    : 3        (Average:  1.00 Max:   1 Sum:      3 Ratio:   7.89%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 17794    (Eliminated:    0 Frozen: 3815)
Constraints  : 73341    (Binary:  92.3% Ternary:   5.4% Other:   2.2%)

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

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

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

Models       : 0
Calls        : 4
Time         : 2.723s (Solving: 0.69s 1st Model: 0.00s Unsat: 0.69s)
CPU Time     : 2.580s

Choices      : 14860    (Domain: 14099)
Conflicts    : 2048     (Analyzed: 2046)
Restarts     : 22       (Average: 93.00 Last: 11)
Model-Level  : 148.0   
Problems     : 4        (Average Length: 7.00 Splits: 0)
Lemmas       : 2046     (Deleted: 625)
  Binary     : 226      (Ratio:  11.05%)
  Ternary    : 305      (Ratio:  14.91%)
  Conflict   : 2046     (Average Length:   21.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 2046     (Average:  7.27 Max:  66 Sum:  14884)
  Executed   : 2016     (Average:  7.13 Max:  66 Sum:  14590 Ratio:  98.02%)
  Bounded    : 30       (Average:  9.80 Max:  12 Sum:    294 Ratio:   1.98%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 50740    (Eliminated:    0 Frozen: 14250)
Constraints  : 322926   (Binary:  91.5% Ternary:   6.6% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 0.71s
Memory:		 213MB (+10MB)
UNSAT
Iteration Time:	 1.34s

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

Models       : 0+
Calls        : 5
Time         : 7.300s (Solving: 4.63s 1st Model: 0.00s Unsat: 0.69s)
CPU Time     : 7.160s

Choices      : 78060    (Domain: 68959)
Conflicts    : 10619    (Analyzed: 10617)
Restarts     : 122      (Average: 87.02 Last: 78)
Model-Level  : 148.0   
Problems     : 5        (Average Length: 9.00 Splits: 0)
Lemmas       : 10617    (Deleted: 4869)
  Binary     : 643      (Ratio:   6.06%)
  Ternary    : 500      (Ratio:   4.71%)
  Conflict   : 10617    (Average Length:  235.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 10617    (Average:  7.08 Max: 149 Sum:  75198)
  Executed   : 10576    (Average:  7.04 Max: 149 Sum:  74721 Ratio:  99.37%)
  Bounded    : 41       (Average: 11.63 Max:  17 Sum:    477 Ratio:   0.63%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 83686    (Eliminated:    0 Frozen: 24685)
Constraints  : 554156   (Binary:  91.5% Ternary:   6.6% Other:   1.9%)

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

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

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

Models       : 0+
Calls        : 6
Time         : 12.209s (Solving: 8.81s 1st Model: 0.00s Unsat: 0.69s)
CPU Time     : 12.072s

Choices      : 170091   (Domain: 148240)
Conflicts    : 19840    (Analyzed: 19838)
Restarts     : 222      (Average: 89.36 Last: 104)
Model-Level  : 148.0   
Problems     : 6        (Average Length: 11.17 Splits: 0)
Lemmas       : 19838    (Deleted: 14254)
  Binary     : 1032     (Ratio:   5.20%)
  Ternary    : 614      (Ratio:   3.10%)
  Conflict   : 19838    (Average Length:  256.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 19838    (Average:  8.14 Max: 277 Sum: 161445)
  Executed   : 19776    (Average:  8.09 Max: 277 Sum: 160511 Ratio:  99.42%)
  Bounded    : 62       (Average: 15.06 Max:  22 Sum:    934 Ratio:   0.58%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 116632   (Eliminated:    0 Frozen: 35120)
Constraints  : 795856   (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 4.23s
Memory:		 265MB (+18MB)
UNKNOWN
Iteration Time:	 4.92s

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

Models       : 0+
Calls        : 7
Time         : 18.329s (Solving: 14.13s 1st Model: 0.00s Unsat: 0.69s)
CPU Time     : 18.196s

Choices      : 311716   (Domain: 276263)
Conflicts    : 28786    (Analyzed: 28784)
Restarts     : 322      (Average: 89.39 Last: 104)
Model-Level  : 148.0   
Problems     : 7        (Average Length: 13.43 Splits: 0)
Lemmas       : 28784    (Deleted: 21060)
  Binary     : 1876     (Ratio:   6.52%)
  Ternary    : 957      (Ratio:   3.32%)
  Conflict   : 28784    (Average Length:  297.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 28784    (Average: 10.18 Max: 376 Sum: 292956)
  Executed   : 28710    (Average: 10.13 Max: 376 Sum: 291700 Ratio:  99.57%)
  Bounded    : 74       (Average: 16.97 Max:  27 Sum:   1256 Ratio:   0.43%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 149578   (Eliminated:    0 Frozen: 45555)
Constraints  : 1034643  (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 5.37s
Memory:		 289MB (+11MB)
UNKNOWN
Iteration Time:	 6.14s

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

Models       : 0+
Calls        : 8
Time         : 27.454s (Solving: 22.22s 1st Model: 0.00s Unsat: 0.69s)
CPU Time     : 27.324s

Choices      : 435256   (Domain: 387472)
Conflicts    : 38279    (Analyzed: 38277)
Restarts     : 422      (Average: 90.70 Last: 111)
Model-Level  : 148.0   
Problems     : 8        (Average Length: 15.75 Splits: 0)
Lemmas       : 38277    (Deleted: 28680)
  Binary     : 2260     (Ratio:   5.90%)
  Ternary    : 1145     (Ratio:   2.99%)
  Conflict   : 38277    (Average Length:  322.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 38277    (Average: 10.64 Max: 509 Sum: 407200)
  Executed   : 38198    (Average: 10.60 Max: 509 Sum: 405785 Ratio:  99.65%)
  Bounded    : 79       (Average: 17.91 Max:  32 Sum:   1415 Ratio:   0.35%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 182524   (Eliminated:    0 Frozen: 55990)
Constraints  : 1263687  (Binary:  91.4% Ternary:   6.7% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 8.16s
Memory:		 324MB (+24MB)
UNKNOWN
Iteration Time:	 9.14s

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

Models       : 0
Calls        : 9
Time         : 29.090s (Solving: 23.82s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 28.960s

Choices      : 444161   (Domain: 394803)
Conflicts    : 40170    (Analyzed: 40167)
Restarts     : 443      (Average: 90.67 Last: 111)
Model-Level  : 148.0   
Problems     : 9        (Average Length: 17.56 Splits: 0)
Lemmas       : 40167    (Deleted: 28680)
  Binary     : 2339     (Ratio:   5.82%)
  Ternary    : 1176     (Ratio:   2.93%)
  Conflict   : 40167    (Average Length:  317.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 40167    (Average: 10.35 Max: 509 Sum: 415921)
  Executed   : 40087    (Average: 10.32 Max: 509 Sum: 414505 Ratio:  99.66%)
  Bounded    : 80       (Average: 17.70 Max:  32 Sum:   1416 Ratio:   0.34%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 182524   (Eliminated:    0 Frozen: 55990)
Constraints  : 1263631  (Binary:  91.4% Ternary:   6.7% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 1.62s
Memory:		 324MB (+0MB)
UNSAT
Iteration Time:	 1.64s

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

Models       : 0+
Calls        : 10
Time         : 36.964s (Solving: 31.64s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 36.836s

Choices      : 493744   (Domain: 435637)
Conflicts    : 48914    (Analyzed: 48911)
Restarts     : 543      (Average: 90.08 Last: 111)
Model-Level  : 148.0   
Problems     : 10       (Average Length: 19.00 Splits: 0)
Lemmas       : 48911    (Deleted: 38023)
  Binary     : 2522     (Ratio:   5.16%)
  Ternary    : 1328     (Ratio:   2.72%)
  Conflict   : 48911    (Average Length:  422.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 48911    (Average:  9.43 Max: 509 Sum: 461331)
  Executed   : 48830    (Average:  9.40 Max: 509 Sum: 459883 Ratio:  99.69%)
  Bounded    : 81       (Average: 17.88 Max:  32 Sum:   1448 Ratio:   0.31%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 182524   (Eliminated:    0 Frozen: 55990)
Constraints  : 1263631  (Binary:  91.4% Ternary:   6.7% Other:   1.9%)

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

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

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

Models       : 0+
Calls        : 11
Time         : 43.964s (Solving: 38.60s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 43.836s

Choices      : 572132   (Domain: 505239)
Conflicts    : 57534    (Analyzed: 57531)
Restarts     : 643      (Average: 89.47 Last: 111)
Model-Level  : 148.0   
Problems     : 11       (Average Length: 20.18 Splits: 0)
Lemmas       : 57531    (Deleted: 45329)
  Binary     : 2890     (Ratio:   5.02%)
  Ternary    : 1461     (Ratio:   2.54%)
  Conflict   : 57531    (Average Length:  436.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 57531    (Average:  9.27 Max: 509 Sum: 533081)
  Executed   : 57445    (Average:  9.24 Max: 509 Sum: 531473 Ratio:  99.70%)
  Bounded    : 86       (Average: 18.70 Max:  32 Sum:   1608 Ratio:   0.30%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 182524   (Eliminated:    0 Frozen: 55990)
Constraints  : 1263617  (Binary:  91.4% Ternary:   6.7% Other:   1.9%)

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

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

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

Models       : 0+
Calls        : 12
Time         : 49.704s (Solving: 44.30s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 49.580s

Choices      : 651504   (Domain: 575594)
Conflicts    : 65352    (Analyzed: 65349)
Restarts     : 743      (Average: 87.95 Last: 111)
Model-Level  : 148.0   
Problems     : 12       (Average Length: 21.17 Splits: 0)
Lemmas       : 65349    (Deleted: 51225)
  Binary     : 3148     (Ratio:   4.82%)
  Ternary    : 1555     (Ratio:   2.38%)
  Conflict   : 65349    (Average Length:  437.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 65349    (Average:  9.22 Max: 509 Sum: 602562)
  Executed   : 65260    (Average:  9.19 Max: 509 Sum: 600858 Ratio:  99.72%)
  Bounded    : 89       (Average: 19.15 Max:  32 Sum:   1704 Ratio:   0.28%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 182524   (Eliminated:    0 Frozen: 55990)
Constraints  : 1263547  (Binary:  91.4% Ternary:   6.7% Other:   1.9%)

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

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

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

Models       : 0+
Calls        : 13
Time         : 56.267s (Solving: 50.08s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 56.144s

Choices      : 735656   (Domain: 654916)
Conflicts    : 73377    (Analyzed: 73374)
Restarts     : 843      (Average: 87.04 Last: 111)
Model-Level  : 148.0   
Problems     : 13       (Average Length: 22.38 Splits: 0)
Lemmas       : 73374    (Deleted: 57875)
  Binary     : 3467     (Ratio:   4.73%)
  Ternary    : 1760     (Ratio:   2.40%)
  Conflict   : 73374    (Average Length:  448.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 73374    (Average:  9.21 Max: 509 Sum: 676140)
  Executed   : 73283    (Average:  9.19 Max: 509 Sum: 674362 Ratio:  99.74%)
  Bounded    : 91       (Average: 19.54 Max:  37 Sum:   1778 Ratio:   0.26%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 215470   (Eliminated:    0 Frozen: 66425)
Constraints  : 1513090  (Binary:  91.4% Ternary:   6.7% Other:   1.9%)

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

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

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

Models       : 0+
Calls        : 14
Time         : 63.027s (Solving: 56.03s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 62.908s

Choices      : 789742   (Domain: 708818)
Conflicts    : 81495    (Analyzed: 81492)
Restarts     : 943      (Average: 86.42 Last: 111)
Model-Level  : 148.0   
Problems     : 14       (Average Length: 23.79 Splits: 0)
Lemmas       : 81492    (Deleted: 65195)
  Binary     : 3580     (Ratio:   4.39%)
  Ternary    : 1786     (Ratio:   2.19%)
  Conflict   : 81492    (Average Length:  432.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 81492    (Average:  8.87 Max: 517 Sum: 722840)
  Executed   : 81401    (Average:  8.85 Max: 517 Sum: 721062 Ratio:  99.75%)
  Bounded    : 91       (Average: 19.54 Max:  37 Sum:   1778 Ratio:   0.25%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 248416   (Eliminated:    0 Frozen: 76860)
Constraints  : 1762647  (Binary:  91.4% Ternary:   6.8% Other:   1.9%)

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

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

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

Models       : 0+
Calls        : 15
Time         : 71.119s (Solving: 63.32s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 71.000s

Choices      : 948263   (Domain: 862777)
Conflicts    : 89765    (Analyzed: 89762)
Restarts     : 1043     (Average: 86.06 Last: 111)
Model-Level  : 148.0   
Problems     : 15       (Average Length: 25.33 Splits: 0)
Lemmas       : 89762    (Deleted: 72415)
  Binary     : 3941     (Ratio:   4.39%)
  Ternary    : 1936     (Ratio:   2.16%)
  Conflict   : 89762    (Average Length:  411.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 89762    (Average:  9.65 Max: 774 Sum: 865953)
  Executed   : 89669    (Average:  9.63 Max: 774 Sum: 864081 Ratio:  99.78%)
  Bounded    : 93       (Average: 20.13 Max:  47 Sum:   1872 Ratio:   0.22%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 281362   (Eliminated:    0 Frozen: 87295)
Constraints  : 2012232  (Binary:  91.4% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 7.35s
Memory:		 404MB (+34MB)
UNKNOWN
Iteration Time:	 8.11s

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

Models       : 0+
Calls        : 16
Time         : 78.561s (Solving: 69.91s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 78.448s

Choices      : 1055346  (Domain: 961782)
Conflicts    : 97974    (Analyzed: 97971)
Restarts     : 1143     (Average: 85.71 Last: 111)
Model-Level  : 148.0   
Problems     : 16       (Average Length: 27.00 Splits: 0)
Lemmas       : 97971    (Deleted: 79839)
  Binary     : 4086     (Ratio:   4.17%)
  Ternary    : 1991     (Ratio:   2.03%)
  Conflict   : 97971    (Average Length:  403.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 97971    (Average:  9.74 Max: 774 Sum: 954678)
  Executed   : 97878    (Average:  9.73 Max: 774 Sum: 952806 Ratio:  99.80%)
  Bounded    : 93       (Average: 20.13 Max:  47 Sum:   1872 Ratio:   0.20%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 314308   (Eliminated:    0 Frozen: 97730)
Constraints  : 2261777  (Binary:  91.4% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 6.67s
Memory:		 418MB (+14MB)
UNKNOWN
Iteration Time:	 7.45s

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

Models       : 0+
Calls        : 17
Time         : 87.749s (Solving: 78.10s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 87.640s

Choices      : 1191783  (Domain: 1094372)
Conflicts    : 106343   (Analyzed: 106340)
Restarts     : 1243     (Average: 85.55 Last: 111)
Model-Level  : 148.0   
Problems     : 17       (Average Length: 28.76 Splits: 0)
Lemmas       : 106340   (Deleted: 87384)
  Binary     : 4313     (Ratio:   4.06%)
  Ternary    : 2093     (Ratio:   1.97%)
  Conflict   : 106340   (Average Length:  400.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 106340   (Average: 10.09 Max: 774 Sum: 1072670)
  Executed   : 106247   (Average: 10.07 Max: 774 Sum: 1070798 Ratio:  99.83%)
  Bounded    : 93       (Average: 20.13 Max:  47 Sum:   1872 Ratio:   0.17%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 347254   (Eliminated:    0 Frozen: 108165)
Constraints  : 2511362  (Binary:  91.4% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 8.28s
Memory:		 452MB (+17MB)
UNKNOWN
Iteration Time:	 9.20s

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

Models       : 0+
Calls        : 18
Time         : 95.959s (Solving: 85.47s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 95.852s

Choices      : 1323325  (Domain: 1222605)
Conflicts    : 114010   (Analyzed: 114007)
Restarts     : 1343     (Average: 84.89 Last: 111)
Model-Level  : 148.0   
Problems     : 18       (Average Length: 30.61 Splits: 0)
Lemmas       : 114007   (Deleted: 95286)
  Binary     : 4470     (Ratio:   3.92%)
  Ternary    : 2135     (Ratio:   1.87%)
  Conflict   : 114007   (Average Length:  394.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 114007   (Average: 10.39 Max: 774 Sum: 1184382)
  Executed   : 113913   (Average: 10.37 Max: 774 Sum: 1182448 Ratio:  99.84%)
  Bounded    : 94       (Average: 20.57 Max:  62 Sum:   1934 Ratio:   0.16%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 380200   (Eliminated:    0 Frozen: 118600)
Constraints  : 2760947  (Binary:  91.4% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 7.45s
Memory:		 471MB (+15MB)
UNKNOWN
Iteration Time:	 8.22s

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

Models       : 0+
Calls        : 19
Time         : 104.064s (Solving: 92.71s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 103.960s

Choices      : 1427277  (Domain: 1324028)
Conflicts    : 121551   (Analyzed: 121548)
Restarts     : 1443     (Average: 84.23 Last: 159)
Model-Level  : 148.0   
Problems     : 19       (Average Length: 32.53 Splits: 0)
Lemmas       : 121548   (Deleted: 102495)
  Binary     : 4555     (Ratio:   3.75%)
  Ternary    : 2169     (Ratio:   1.78%)
  Conflict   : 121548   (Average Length:  387.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 121548   (Average: 10.46 Max: 774 Sum: 1270979)
  Executed   : 121451   (Average: 10.44 Max: 774 Sum: 1268844 Ratio:  99.83%)
  Bounded    : 97       (Average: 22.01 Max:  67 Sum:   2135 Ratio:   0.17%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 413146   (Eliminated:    0 Frozen: 129035)
Constraints  : 3010506  (Binary:  91.4% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 7.33s
Memory:		 528MB (+49MB)
UNKNOWN
Iteration Time:	 8.12s

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

Models       : 0+
Calls        : 20
Time         : 111.037s (Solving: 98.81s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 110.936s

Choices      : 1500972  (Domain: 1396939)
Conflicts    : 128890   (Analyzed: 128887)
Restarts     : 1543     (Average: 83.53 Last: 159)
Model-Level  : 148.0   
Problems     : 20       (Average Length: 34.50 Splits: 0)
Lemmas       : 128887   (Deleted: 109718)
  Binary     : 4607     (Ratio:   3.57%)
  Ternary    : 2193     (Ratio:   1.70%)
  Conflict   : 128887   (Average Length:  380.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 128887   (Average: 10.32 Max: 774 Sum: 1329866)
  Executed   : 128789   (Average: 10.30 Max: 774 Sum: 1327659 Ratio:  99.83%)
  Bounded    : 98       (Average: 22.52 Max:  72 Sum:   2207 Ratio:   0.17%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 446092   (Eliminated:    0 Frozen: 139470)
Constraints  : 3260041  (Binary:  91.4% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 6.19s
Memory:		 532MB (+4MB)
UNKNOWN
Iteration Time:	 6.99s

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

Models       : 0+
Calls        : 21
Time         : 118.947s (Solving: 105.80s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 118.848s

Choices      : 1589971  (Domain: 1483795)
Conflicts    : 136496   (Analyzed: 136493)
Restarts     : 1643     (Average: 83.08 Last: 159)
Model-Level  : 148.0   
Problems     : 21       (Average Length: 36.52 Splits: 0)
Lemmas       : 136493   (Deleted: 116783)
  Binary     : 4692     (Ratio:   3.44%)
  Ternary    : 2209     (Ratio:   1.62%)
  Conflict   : 136493   (Average Length:  376.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 136493   (Average: 10.26 Max: 775 Sum: 1401023)
  Executed   : 136395   (Average: 10.25 Max: 775 Sum: 1398816 Ratio:  99.84%)
  Bounded    : 98       (Average: 22.52 Max:  72 Sum:   2207 Ratio:   0.16%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 479038   (Eliminated:    0 Frozen: 149905)
Constraints  : 3509601  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 7.09s
Memory:		 558MB (+23MB)
UNKNOWN
Iteration Time:	 7.92s

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

Models       : 0+
Calls        : 22
Time         : 129.516s (Solving: 115.44s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 129.420s

Choices      : 1780958  (Domain: 1670882)
Conflicts    : 144738   (Analyzed: 144735)
Restarts     : 1743     (Average: 83.04 Last: 159)
Model-Level  : 148.0   
Problems     : 22       (Average Length: 38.59 Splits: 0)
Lemmas       : 144735   (Deleted: 123899)
  Binary     : 4911     (Ratio:   3.39%)
  Ternary    : 2305     (Ratio:   1.59%)
  Conflict   : 144735   (Average Length:  384.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 144735   (Average: 10.80 Max: 775 Sum: 1562709)
  Executed   : 144637   (Average: 10.78 Max: 775 Sum: 1560502 Ratio:  99.86%)
  Bounded    : 98       (Average: 22.52 Max:  72 Sum:   2207 Ratio:   0.14%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 511984   (Eliminated:    0 Frozen: 160340)
Constraints  : 3759186  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 9.74s
Memory:		 581MB (+23MB)
UNKNOWN
Iteration Time:	 10.58s

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

Models       : 0+
Calls        : 23
Time         : 133.071s (Solving: 118.89s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 132.976s

Choices      : 1807843  (Domain: 1697767)
Conflicts    : 151929   (Analyzed: 151926)
Restarts     : 1843     (Average: 82.43 Last: 159)
Model-Level  : 148.0   
Problems     : 23       (Average Length: 40.48 Splits: 0)
Lemmas       : 151926   (Deleted: 131781)
  Binary     : 4944     (Ratio:   3.25%)
  Ternary    : 2325     (Ratio:   1.53%)
  Conflict   : 151926   (Average Length:  378.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 151926   (Average: 10.42 Max: 775 Sum: 1583713)
  Executed   : 151828   (Average: 10.41 Max: 775 Sum: 1581506 Ratio:  99.86%)
  Bounded    : 98       (Average: 22.52 Max:  72 Sum:   2207 Ratio:   0.14%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 511984   (Eliminated:    0 Frozen: 160340)
Constraints  : 3759186  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 3.52s
Memory:		 583MB (+2MB)
UNKNOWN
Iteration Time:	 3.56s

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

Models       : 0+
Calls        : 24
Time         : 138.723s (Solving: 124.40s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 138.628s

Choices      : 1851780  (Domain: 1741704)
Conflicts    : 159791   (Analyzed: 159788)
Restarts     : 1943     (Average: 82.24 Last: 159)
Model-Level  : 148.0   
Problems     : 24       (Average Length: 42.21 Splits: 0)
Lemmas       : 159788   (Deleted: 138644)
  Binary     : 5011     (Ratio:   3.14%)
  Ternary    : 2350     (Ratio:   1.47%)
  Conflict   : 159788   (Average Length:  375.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 159788   (Average: 10.15 Max: 775 Sum: 1621953)
  Executed   : 159690   (Average: 10.14 Max: 775 Sum: 1619746 Ratio:  99.86%)
  Bounded    : 98       (Average: 22.52 Max:  72 Sum:   2207 Ratio:   0.14%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 511984   (Eliminated:    0 Frozen: 160340)
Constraints  : 3759186  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 25
Time         : 143.338s (Solving: 128.88s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 143.244s

Choices      : 1889488  (Domain: 1778476)
Conflicts    : 167541   (Analyzed: 167538)
Restarts     : 2043     (Average: 82.01 Last: 159)
Model-Level  : 148.0   
Problems     : 25       (Average Length: 43.80 Splits: 0)
Lemmas       : 167538   (Deleted: 145932)
  Binary     : 5058     (Ratio:   3.02%)
  Ternary    : 2366     (Ratio:   1.41%)
  Conflict   : 167538   (Average Length:  369.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 167538   (Average:  9.87 Max: 775 Sum: 1653157)
  Executed   : 167439   (Average:  9.85 Max: 775 Sum: 1650868 Ratio:  99.86%)
  Bounded    : 99       (Average: 23.12 Max:  82 Sum:   2289 Ratio:   0.14%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 511984   (Eliminated:    0 Frozen: 160340)
Constraints  : 3759186  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 4.57s
Memory:		 583MB (+0MB)
UNKNOWN
Iteration Time:	 4.62s

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

Models       : 0+
Calls        : 26
Time         : 149.287s (Solving: 134.73s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 149.196s

Choices      : 1938816  (Domain: 1827394)
Conflicts    : 175116   (Analyzed: 175113)
Restarts     : 2143     (Average: 81.71 Last: 159)
Model-Level  : 148.0   
Problems     : 26       (Average Length: 45.27 Splits: 0)
Lemmas       : 175113   (Deleted: 153237)
  Binary     : 5168     (Ratio:   2.95%)
  Ternary    : 2380     (Ratio:   1.36%)
  Conflict   : 175113   (Average Length:  365.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 175113   (Average:  9.68 Max: 775 Sum: 1694488)
  Executed   : 175013   (Average:  9.66 Max: 775 Sum: 1692117 Ratio:  99.86%)
  Bounded    : 100      (Average: 23.71 Max:  82 Sum:   2371 Ratio:   0.14%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 511984   (Eliminated:    0 Frozen: 160340)
Constraints  : 3759172  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 5.92s
Memory:		 583MB (+0MB)
UNKNOWN
Iteration Time:	 5.95s

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

Models       : 0+
Calls        : 27
Time         : 156.184s (Solving: 141.52s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 156.096s

Choices      : 2013412  (Domain: 1898919)
Conflicts    : 183283   (Analyzed: 183280)
Restarts     : 2243     (Average: 81.71 Last: 159)
Model-Level  : 148.0   
Problems     : 27       (Average Length: 46.63 Splits: 0)
Lemmas       : 183280   (Deleted: 160499)
  Binary     : 5220     (Ratio:   2.85%)
  Ternary    : 2401     (Ratio:   1.31%)
  Conflict   : 183280   (Average Length:  363.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 183280   (Average:  9.57 Max: 775 Sum: 1754389)
  Executed   : 183180   (Average:  9.56 Max: 775 Sum: 1752018 Ratio:  99.86%)
  Bounded    : 100      (Average: 23.71 Max:  82 Sum:   2371 Ratio:   0.14%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 511984   (Eliminated:    0 Frozen: 160340)
Constraints  : 3759158  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 6.86s
Memory:		 583MB (+0MB)
UNKNOWN
Iteration Time:	 6.90s

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

Models       : 0+
Calls        : 28
Time         : 163.639s (Solving: 148.86s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 163.552s

Choices      : 2088124  (Domain: 1971219)
Conflicts    : 191612   (Analyzed: 191609)
Restarts     : 2343     (Average: 81.78 Last: 159)
Model-Level  : 148.0   
Problems     : 28       (Average Length: 47.89 Splits: 0)
Lemmas       : 191609   (Deleted: 168451)
  Binary     : 5293     (Ratio:   2.76%)
  Ternary    : 2438     (Ratio:   1.27%)
  Conflict   : 191609   (Average Length:  360.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 191609   (Average:  9.49 Max: 814 Sum: 1818021)
  Executed   : 191506   (Average:  9.47 Max: 814 Sum: 1815404 Ratio:  99.86%)
  Bounded    : 103      (Average: 25.41 Max:  82 Sum:   2617 Ratio:   0.14%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 511984   (Eliminated:    0 Frozen: 160340)
Constraints  : 3759158  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 29
Time         : 170.568s (Solving: 155.66s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 170.484s

Choices      : 2167260  (Domain: 2046633)
Conflicts    : 199585   (Analyzed: 199582)
Restarts     : 2443     (Average: 81.70 Last: 159)
Model-Level  : 148.0   
Problems     : 29       (Average Length: 49.07 Splits: 0)
Lemmas       : 199582   (Deleted: 176144)
  Binary     : 5407     (Ratio:   2.71%)
  Ternary    : 2505     (Ratio:   1.26%)
  Conflict   : 199582   (Average Length:  360.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 199582   (Average:  9.42 Max: 814 Sum: 1880690)
  Executed   : 199479   (Average:  9.41 Max: 814 Sum: 1878073 Ratio:  99.86%)
  Bounded    : 103      (Average: 25.41 Max:  82 Sum:   2617 Ratio:   0.14%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 511984   (Eliminated:    0 Frozen: 160340)
Constraints  : 3759105  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 30
Time         : 178.816s (Solving: 163.80s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 178.736s

Choices      : 2283872  (Domain: 2158631)
Conflicts    : 207741   (Analyzed: 207738)
Restarts     : 2543     (Average: 81.69 Last: 159)
Model-Level  : 148.0   
Problems     : 30       (Average Length: 50.17 Splits: 0)
Lemmas       : 207738   (Deleted: 183732)
  Binary     : 5513     (Ratio:   2.65%)
  Ternary    : 2537     (Ratio:   1.22%)
  Conflict   : 207738   (Average Length:  364.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 207738   (Average:  9.51 Max: 814 Sum: 1976605)
  Executed   : 207635   (Average:  9.50 Max: 814 Sum: 1973988 Ratio:  99.87%)
  Bounded    : 103      (Average: 25.41 Max:  82 Sum:   2617 Ratio:   0.13%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 511984   (Eliminated:    0 Frozen: 160340)
Constraints  : 3759105  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 31
Time         : 186.116s (Solving: 171.00s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 186.040s

Choices      : 2368951  (Domain: 2241125)
Conflicts    : 215177   (Analyzed: 215174)
Restarts     : 2643     (Average: 81.41 Last: 159)
Model-Level  : 148.0   
Problems     : 31       (Average Length: 51.19 Splits: 0)
Lemmas       : 215174   (Deleted: 191445)
  Binary     : 5592     (Ratio:   2.60%)
  Ternary    : 2553     (Ratio:   1.19%)
  Conflict   : 215174   (Average Length:  364.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 215174   (Average:  9.51 Max: 814 Sum: 2045576)
  Executed   : 215071   (Average:  9.49 Max: 814 Sum: 2042959 Ratio:  99.87%)
  Bounded    : 103      (Average: 25.41 Max:  82 Sum:   2617 Ratio:   0.13%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 511984   (Eliminated:    0 Frozen: 160340)
Constraints  : 3759105  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 32
Time         : 193.432s (Solving: 178.21s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 193.360s

Choices      : 2470796  (Domain: 2340598)
Conflicts    : 222452   (Analyzed: 222449)
Restarts     : 2743     (Average: 81.10 Last: 159)
Model-Level  : 148.0   
Problems     : 32       (Average Length: 52.16 Splits: 0)
Lemmas       : 222449   (Deleted: 198753)
  Binary     : 5655     (Ratio:   2.54%)
  Ternary    : 2592     (Ratio:   1.17%)
  Conflict   : 222449   (Average Length:  363.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 222449   (Average:  9.58 Max: 814 Sum: 2131554)
  Executed   : 222346   (Average:  9.57 Max: 814 Sum: 2128937 Ratio:  99.88%)
  Bounded    : 103      (Average: 25.41 Max:  82 Sum:   2617 Ratio:   0.12%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 511984   (Eliminated:    0 Frozen: 160340)
Constraints  : 3759105  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 7.28s
Memory:		 583MB (+0MB)
UNKNOWN
Iteration Time:	 7.32s

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

Models       : 0+
Calls        : 33
Time         : 202.132s (Solving: 186.78s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 202.064s

Choices      : 2587643  (Domain: 2454056)
Conflicts    : 230202   (Analyzed: 230199)
Restarts     : 2843     (Average: 80.97 Last: 159)
Model-Level  : 148.0   
Problems     : 33       (Average Length: 53.06 Splits: 0)
Lemmas       : 230199   (Deleted: 205662)
  Binary     : 5740     (Ratio:   2.49%)
  Ternary    : 2607     (Ratio:   1.13%)
  Conflict   : 230199   (Average Length:  364.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 230199   (Average:  9.69 Max: 814 Sum: 2230931)
  Executed   : 230095   (Average:  9.68 Max: 814 Sum: 2228232 Ratio:  99.88%)
  Bounded    : 104      (Average: 25.95 Max:  82 Sum:   2699 Ratio:   0.12%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 511984   (Eliminated:    0 Frozen: 160340)
Constraints  : 3759105  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 34
Time         : 210.489s (Solving: 195.01s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 210.424s

Choices      : 2716130  (Domain: 2580743)
Conflicts    : 238017   (Analyzed: 238014)
Restarts     : 2943     (Average: 80.87 Last: 159)
Model-Level  : 148.0   
Problems     : 34       (Average Length: 53.91 Splits: 0)
Lemmas       : 238014   (Deleted: 213024)
  Binary     : 5810     (Ratio:   2.44%)
  Ternary    : 2645     (Ratio:   1.11%)
  Conflict   : 238014   (Average Length:  362.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 238014   (Average:  9.84 Max: 814 Sum: 2343046)
  Executed   : 237909   (Average:  9.83 Max: 814 Sum: 2340265 Ratio:  99.88%)
  Bounded    : 105      (Average: 26.49 Max:  82 Sum:   2781 Ratio:   0.12%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 511984   (Eliminated:    0 Frozen: 160340)
Constraints  : 3759091  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 8.31s
Memory:		 583MB (+0MB)
UNKNOWN
Iteration Time:	 8.36s

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

Models       : 0+
Calls        : 35
Time         : 219.175s (Solving: 203.57s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 219.112s

Choices      : 2850433  (Domain: 2712692)
Conflicts    : 245867   (Analyzed: 245864)
Restarts     : 3043     (Average: 80.80 Last: 159)
Model-Level  : 148.0   
Problems     : 35       (Average Length: 54.71 Splits: 0)
Lemmas       : 245864   (Deleted: 220430)
  Binary     : 5881     (Ratio:   2.39%)
  Ternary    : 2685     (Ratio:   1.09%)
  Conflict   : 245864   (Average Length:  361.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 245864   (Average: 10.00 Max: 814 Sum: 2459789)
  Executed   : 245759   (Average:  9.99 Max: 814 Sum: 2457008 Ratio:  99.89%)
  Bounded    : 105      (Average: 26.49 Max:  82 Sum:   2781 Ratio:   0.11%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 511984   (Eliminated:    0 Frozen: 160340)
Constraints  : 3759073  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 36
Time         : 228.559s (Solving: 211.99s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 228.496s

Choices      : 2998710  (Domain: 2859367)
Conflicts    : 253634   (Analyzed: 253631)
Restarts     : 3143     (Average: 80.70 Last: 159)
Model-Level  : 148.0   
Problems     : 36       (Average Length: 55.61 Splits: 0)
Lemmas       : 253631   (Deleted: 228078)
  Binary     : 5971     (Ratio:   2.35%)
  Ternary    : 2732     (Ratio:   1.08%)
  Conflict   : 253631   (Average Length:  359.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 253631   (Average: 10.21 Max: 882 Sum: 2590441)
  Executed   : 253526   (Average: 10.20 Max: 882 Sum: 2587660 Ratio:  99.89%)
  Bounded    : 105      (Average: 26.49 Max:  82 Sum:   2781 Ratio:   0.11%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 544930   (Eliminated:    0 Frozen: 170775)
Constraints  : 4008658  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 8.53s
Memory:		 601MB (+18MB)
UNKNOWN
Iteration Time:	 9.40s

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

Models       : 0+
Calls        : 37
Time         : 238.252s (Solving: 220.69s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 238.192s

Choices      : 3170212  (Domain: 3028736)
Conflicts    : 261445   (Analyzed: 261442)
Restarts     : 3243     (Average: 80.62 Last: 159)
Model-Level  : 148.0   
Problems     : 37       (Average Length: 56.59 Splits: 0)
Lemmas       : 261442   (Deleted: 235399)
  Binary     : 6129     (Ratio:   2.34%)
  Ternary    : 2798     (Ratio:   1.07%)
  Conflict   : 261442   (Average Length:  355.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 261442   (Average: 10.50 Max: 882 Sum: 2745941)
  Executed   : 261336   (Average: 10.49 Max: 882 Sum: 2743068 Ratio:  99.90%)
  Bounded    : 106      (Average: 27.10 Max:  92 Sum:   2873 Ratio:   0.10%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 577876   (Eliminated:    0 Frozen: 181210)
Constraints  : 4258243  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 8.82s
Memory:		 621MB (+20MB)
UNKNOWN
Iteration Time:	 9.70s

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

Models       : 0+
Calls        : 38
Time         : 249.715s (Solving: 231.14s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 249.660s

Choices      : 3474637  (Domain: 3329889)
Conflicts    : 269142   (Analyzed: 269139)
Restarts     : 3343     (Average: 80.51 Last: 159)
Model-Level  : 148.0   
Problems     : 38       (Average Length: 57.66 Splits: 0)
Lemmas       : 269139   (Deleted: 242452)
  Binary     : 6477     (Ratio:   2.41%)
  Ternary    : 2896     (Ratio:   1.08%)
  Conflict   : 269139   (Average Length:  353.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 269139   (Average: 11.26 Max: 944 Sum: 3029192)
  Executed   : 269033   (Average: 11.24 Max: 944 Sum: 3026319 Ratio:  99.91%)
  Bounded    : 106      (Average: 27.10 Max:  92 Sum:   2873 Ratio:   0.09%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 610822   (Eliminated:    0 Frozen: 191645)
Constraints  : 4507814  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 10.56s
Memory:		 693MB (+71MB)
UNKNOWN
Iteration Time:	 11.48s

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

Models       : 0+
Calls        : 39
Time         : 262.040s (Solving: 242.45s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 261.992s

Choices      : 3858341  (Domain: 3711317)
Conflicts    : 277514   (Analyzed: 277511)
Restarts     : 3443     (Average: 80.60 Last: 159)
Model-Level  : 148.0   
Problems     : 39       (Average Length: 58.79 Splits: 0)
Lemmas       : 277511   (Deleted: 249318)
  Binary     : 6875     (Ratio:   2.48%)
  Ternary    : 3036     (Ratio:   1.09%)
  Conflict   : 277511   (Average Length:  353.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 277511   (Average: 12.21 Max: 1035 Sum: 3388836)
  Executed   : 277404   (Average: 12.20 Max: 1035 Sum: 3385861 Ratio:  99.91%)
  Bounded    : 107      (Average: 27.80 Max: 102 Sum:   2975 Ratio:   0.09%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 643768   (Eliminated:    0 Frozen: 202080)
Constraints  : 4757399  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 11.44s
Memory:		 697MB (+4MB)
UNKNOWN
Iteration Time:	 12.34s

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

Models       : 0+
Calls        : 40
Time         : 281.093s (Solving: 260.42s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 281.052s

Choices      : 4362555  (Domain: 4214068)
Conflicts    : 286424   (Analyzed: 286421)
Restarts     : 3543     (Average: 80.84 Last: 159)
Model-Level  : 148.0   
Problems     : 40       (Average Length: 60.00 Splits: 0)
Lemmas       : 286421   (Deleted: 258618)
  Binary     : 7425     (Ratio:   2.59%)
  Ternary    : 3146     (Ratio:   1.10%)
  Conflict   : 286421   (Average Length:  367.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 286421   (Average: 13.47 Max: 1058 Sum: 3857690)
  Executed   : 286314   (Average: 13.46 Max: 1058 Sum: 3854715 Ratio:  99.92%)
  Bounded    : 107      (Average: 27.80 Max: 102 Sum:   2975 Ratio:   0.08%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 676714   (Eliminated:    0 Frozen: 212515)
Constraints  : 5006970  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 18.11s
Memory:		 706MB (+9MB)
UNKNOWN
Iteration Time:	 19.07s

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

Models       : 0+
Calls        : 41
Time         : 286.687s (Solving: 265.86s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 286.648s

Choices      : 4412771  (Domain: 4264266)
Conflicts    : 294294   (Analyzed: 294291)
Restarts     : 3643     (Average: 80.78 Last: 159)
Model-Level  : 148.0   
Problems     : 41       (Average Length: 61.15 Splits: 0)
Lemmas       : 294291   (Deleted: 264978)
  Binary     : 7473     (Ratio:   2.54%)
  Ternary    : 3171     (Ratio:   1.08%)
  Conflict   : 294291   (Average Length:  369.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 294291   (Average: 13.26 Max: 1058 Sum: 3901585)
  Executed   : 294183   (Average: 13.25 Max: 1058 Sum: 3898503 Ratio:  99.92%)
  Bounded    : 108      (Average: 28.54 Max: 107 Sum:   3082 Ratio:   0.08%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 676714   (Eliminated:    0 Frozen: 212515)
Constraints  : 5006970  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 5.54s
Memory:		 770MB (+64MB)
UNKNOWN
Iteration Time:	 5.60s

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

Models       : 0+
Calls        : 42
Time         : 294.358s (Solving: 273.38s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 294.324s

Choices      : 4470707  (Domain: 4322198)
Conflicts    : 302299   (Analyzed: 302296)
Restarts     : 3743     (Average: 80.76 Last: 159)
Model-Level  : 148.0   
Problems     : 42       (Average Length: 62.24 Splits: 0)
Lemmas       : 302296   (Deleted: 272551)
  Binary     : 7521     (Ratio:   2.49%)
  Ternary    : 3183     (Ratio:   1.05%)
  Conflict   : 302296   (Average Length:  371.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 302296   (Average: 13.08 Max: 1058 Sum: 3952952)
  Executed   : 302188   (Average: 13.07 Max: 1058 Sum: 3949870 Ratio:  99.92%)
  Bounded    : 108      (Average: 28.54 Max: 107 Sum:   3082 Ratio:   0.08%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 676714   (Eliminated:    0 Frozen: 212515)
Constraints  : 5006958  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 43
Time         : 301.150s (Solving: 280.03s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 301.120s

Choices      : 4520875  (Domain: 4372366)
Conflicts    : 310145   (Analyzed: 310142)
Restarts     : 3843     (Average: 80.70 Last: 159)
Model-Level  : 148.0   
Problems     : 43       (Average Length: 63.28 Splits: 0)
Lemmas       : 310142   (Deleted: 280197)
  Binary     : 7589     (Ratio:   2.45%)
  Ternary    : 3192     (Ratio:   1.03%)
  Conflict   : 310142   (Average Length:  372.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 310142   (Average: 12.88 Max: 1058 Sum: 3994814)
  Executed   : 310034   (Average: 12.87 Max: 1058 Sum: 3991732 Ratio:  99.92%)
  Bounded    : 108      (Average: 28.54 Max: 107 Sum:   3082 Ratio:   0.08%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 676714   (Eliminated:    0 Frozen: 212515)
Constraints  : 5006958  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 6.74s
Memory:		 770MB (+0MB)
UNKNOWN
Iteration Time:	 6.80s

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

Models       : 0+
Calls        : 44
Time         : 309.503s (Solving: 288.22s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 309.476s

Choices      : 4598441  (Domain: 4449093)
Conflicts    : 318441   (Analyzed: 318438)
Restarts     : 3943     (Average: 80.76 Last: 159)
Model-Level  : 148.0   
Problems     : 44       (Average Length: 64.27 Splits: 0)
Lemmas       : 318438   (Deleted: 287749)
  Binary     : 7772     (Ratio:   2.44%)
  Ternary    : 3226     (Ratio:   1.01%)
  Conflict   : 318438   (Average Length:  377.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 318438   (Average: 12.75 Max: 1058 Sum: 4059205)
  Executed   : 318330   (Average: 12.74 Max: 1058 Sum: 4056123 Ratio:  99.92%)
  Bounded    : 108      (Average: 28.54 Max: 107 Sum:   3082 Ratio:   0.08%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 676714   (Eliminated:    0 Frozen: 212515)
Constraints  : 5006958  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 8.30s
Memory:		 770MB (+0MB)
UNKNOWN
Iteration Time:	 8.36s

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

Models       : 0+
Calls        : 45
Time         : 319.446s (Solving: 298.02s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 319.424s

Choices      : 4732995  (Domain: 4582672)
Conflicts    : 326695   (Analyzed: 326692)
Restarts     : 4043     (Average: 80.80 Last: 159)
Model-Level  : 148.0   
Problems     : 45       (Average Length: 65.22 Splits: 0)
Lemmas       : 326692   (Deleted: 295501)
  Binary     : 8041     (Ratio:   2.46%)
  Ternary    : 3252     (Ratio:   1.00%)
  Conflict   : 326692   (Average Length:  388.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 326692   (Average: 12.78 Max: 1058 Sum: 4176320)
  Executed   : 326583   (Average: 12.77 Max: 1058 Sum: 4173131 Ratio:  99.92%)
  Bounded    : 109      (Average: 29.26 Max: 107 Sum:   3189 Ratio:   0.08%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 676714   (Eliminated:    0 Frozen: 212515)
Constraints  : 5006958  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 46
Time         : 331.242s (Solving: 309.66s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 331.224s

Choices      : 4883441  (Domain: 4732585)
Conflicts    : 335451   (Analyzed: 335448)
Restarts     : 4143     (Average: 80.97 Last: 159)
Model-Level  : 148.0   
Problems     : 46       (Average Length: 66.13 Splits: 0)
Lemmas       : 335448   (Deleted: 305236)
  Binary     : 8337     (Ratio:   2.49%)
  Ternary    : 3302     (Ratio:   0.98%)
  Conflict   : 335448   (Average Length:  400.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 335448   (Average: 12.84 Max: 1058 Sum: 4307898)
  Executed   : 335339   (Average: 12.83 Max: 1058 Sum: 4304709 Ratio:  99.93%)
  Bounded    : 109      (Average: 29.26 Max: 107 Sum:   3189 Ratio:   0.07%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 676714   (Eliminated:    0 Frozen: 212515)
Constraints  : 5006944  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 11.74s
Memory:		 770MB (+0MB)
UNKNOWN
Iteration Time:	 11.80s

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

Models       : 0+
Calls        : 47
Time         : 339.375s (Solving: 317.65s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 339.364s

Choices      : 4979210  (Domain: 4828005)
Conflicts    : 343943   (Analyzed: 343940)
Restarts     : 4243     (Average: 81.06 Last: 199)
Model-Level  : 148.0   
Problems     : 47       (Average Length: 67.00 Splits: 0)
Lemmas       : 343940   (Deleted: 311472)
  Binary     : 8484     (Ratio:   2.47%)
  Ternary    : 3342     (Ratio:   0.97%)
  Conflict   : 343940   (Average Length:  407.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 343940   (Average: 12.76 Max: 1058 Sum: 4388239)
  Executed   : 343831   (Average: 12.75 Max: 1058 Sum: 4385050 Ratio:  99.93%)
  Bounded    : 109      (Average: 29.26 Max: 107 Sum:   3189 Ratio:   0.07%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 676714   (Eliminated:    0 Frozen: 212515)
Constraints  : 5006944  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

Models       : 0+
Calls        : 48
Time         : 353.249s (Solving: 331.35s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 353.244s

Choices      : 5215039  (Domain: 5061950)
Conflicts    : 352840   (Analyzed: 352837)
Restarts     : 4343     (Average: 81.24 Last: 199)
Model-Level  : 148.0   
Problems     : 48       (Average Length: 67.83 Splits: 0)
Lemmas       : 352837   (Deleted: 321529)
  Binary     : 8912     (Ratio:   2.53%)
  Ternary    : 3411     (Ratio:   0.97%)
  Conflict   : 352837   (Average Length:  420.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 352837   (Average: 13.04 Max: 1058 Sum: 4600970)
  Executed   : 352728   (Average: 13.03 Max: 1058 Sum: 4597781 Ratio:  99.93%)
  Bounded    : 109      (Average: 29.26 Max: 107 Sum:   3189 Ratio:   0.07%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 676714   (Eliminated:    0 Frozen: 212515)
Constraints  : 5006944  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 13.81s
Memory:		 770MB (+0MB)
UNKNOWN
Iteration Time:	 13.88s

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

Models       : 0+
Calls        : 49
Time         : 361.821s (Solving: 339.78s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 361.820s

Choices      : 5339492  (Domain: 5185899)
Conflicts    : 360999   (Analyzed: 360996)
Restarts     : 4443     (Average: 81.25 Last: 199)
Model-Level  : 148.0   
Problems     : 49       (Average Length: 68.63 Splits: 0)
Lemmas       : 360996   (Deleted: 327811)
  Binary     : 9061     (Ratio:   2.51%)
  Ternary    : 3440     (Ratio:   0.95%)
  Conflict   : 360996   (Average Length:  425.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 360996   (Average: 13.04 Max: 1058 Sum: 4706779)
  Executed   : 360887   (Average: 13.03 Max: 1058 Sum: 4703590 Ratio:  99.93%)
  Bounded    : 109      (Average: 29.26 Max: 107 Sum:   3189 Ratio:   0.07%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 676714   (Eliminated:    0 Frozen: 212515)
Constraints  : 5006944  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 50
Time         : 371.561s (Solving: 349.36s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 371.564s

Choices      : 5442711  (Domain: 5288677)
Conflicts    : 369661   (Analyzed: 369658)
Restarts     : 4543     (Average: 81.37 Last: 199)
Model-Level  : 148.0   
Problems     : 50       (Average Length: 69.40 Splits: 0)
Lemmas       : 369658   (Deleted: 337659)
  Binary     : 9134     (Ratio:   2.47%)
  Ternary    : 3472     (Ratio:   0.94%)
  Conflict   : 369658   (Average Length:  429.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 369658   (Average: 12.97 Max: 1058 Sum: 4794376)
  Executed   : 369549   (Average: 12.96 Max: 1058 Sum: 4791187 Ratio:  99.93%)
  Bounded    : 109      (Average: 29.26 Max: 107 Sum:   3189 Ratio:   0.07%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 676714   (Eliminated:    0 Frozen: 212515)
Constraints  : 5006944  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 51
Time         : 379.915s (Solving: 357.54s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 379.920s

Choices      : 5511291  (Domain: 5357243)
Conflicts    : 377449   (Analyzed: 377446)
Restarts     : 4643     (Average: 81.29 Last: 199)
Model-Level  : 148.0   
Problems     : 51       (Average Length: 70.14 Splits: 0)
Lemmas       : 377446   (Deleted: 343925)
  Binary     : 9154     (Ratio:   2.43%)
  Ternary    : 3477     (Ratio:   0.92%)
  Conflict   : 377446   (Average Length:  431.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 377446   (Average: 12.84 Max: 1058 Sum: 4845498)
  Executed   : 377337   (Average: 12.83 Max: 1058 Sum: 4842309 Ratio:  99.93%)
  Bounded    : 109      (Average: 29.26 Max: 107 Sum:   3189 Ratio:   0.07%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 676714   (Eliminated:    0 Frozen: 212515)
Constraints  : 5006944  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 8.29s
Memory:		 770MB (+0MB)
UNKNOWN
Iteration Time:	 8.36s

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

Models       : 0+
Calls        : 52
Time         : 387.856s (Solving: 365.33s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 387.864s

Choices      : 5608591  (Domain: 5453833)
Conflicts    : 385686   (Analyzed: 385683)
Restarts     : 4743     (Average: 81.32 Last: 199)
Model-Level  : 148.0   
Problems     : 52       (Average Length: 70.85 Splits: 0)
Lemmas       : 385683   (Deleted: 351500)
  Binary     : 9255     (Ratio:   2.40%)
  Ternary    : 3490     (Ratio:   0.90%)
  Conflict   : 385683   (Average Length:  434.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 385683   (Average: 12.76 Max: 1058 Sum: 4923227)
  Executed   : 385574   (Average: 12.76 Max: 1058 Sum: 4920038 Ratio:  99.94%)
  Bounded    : 109      (Average: 29.26 Max: 107 Sum:   3189 Ratio:   0.06%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 676714   (Eliminated:    0 Frozen: 212515)
Constraints  : 5006944  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 53
Time         : 395.982s (Solving: 373.32s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 395.996s

Choices      : 5710949  (Domain: 5555752)
Conflicts    : 393815   (Analyzed: 393812)
Restarts     : 4843     (Average: 81.32 Last: 199)
Model-Level  : 148.0   
Problems     : 53       (Average Length: 71.53 Splits: 0)
Lemmas       : 393812   (Deleted: 359513)
  Binary     : 9388     (Ratio:   2.38%)
  Ternary    : 3493     (Ratio:   0.89%)
  Conflict   : 393812   (Average Length:  439.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 393812   (Average: 12.71 Max: 1058 Sum: 5005431)
  Executed   : 393703   (Average: 12.70 Max: 1058 Sum: 5002242 Ratio:  99.94%)
  Bounded    : 109      (Average: 29.26 Max: 107 Sum:   3189 Ratio:   0.06%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 676714   (Eliminated:    0 Frozen: 212515)
Constraints  : 5006944  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 54
Time         : 404.039s (Solving: 381.24s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 404.056s

Choices      : 5776284  (Domain: 5621085)
Conflicts    : 401720   (Analyzed: 401717)
Restarts     : 4943     (Average: 81.27 Last: 199)
Model-Level  : 148.0   
Problems     : 54       (Average Length: 72.19 Splits: 0)
Lemmas       : 401717   (Deleted: 367390)
  Binary     : 9431     (Ratio:   2.35%)
  Ternary    : 3503     (Ratio:   0.87%)
  Conflict   : 401717   (Average Length:  441.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 401717   (Average: 12.58 Max: 1058 Sum: 5053258)
  Executed   : 401607   (Average: 12.57 Max: 1058 Sum: 5049962 Ratio:  99.93%)
  Bounded    : 110      (Average: 29.96 Max: 107 Sum:   3296 Ratio:   0.07%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 676714   (Eliminated:    0 Frozen: 212515)
Constraints  : 5006944  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 55
Time         : 411.421s (Solving: 388.49s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 411.440s

Choices      : 5860546  (Domain: 5705341)
Conflicts    : 409665   (Analyzed: 409662)
Restarts     : 5043     (Average: 81.23 Last: 199)
Model-Level  : 148.0   
Problems     : 55       (Average Length: 72.82 Splits: 0)
Lemmas       : 409662   (Deleted: 375188)
  Binary     : 9463     (Ratio:   2.31%)
  Ternary    : 3508     (Ratio:   0.86%)
  Conflict   : 409662   (Average Length:  443.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 409662   (Average: 12.49 Max: 1058 Sum: 5117575)
  Executed   : 409551   (Average: 12.48 Max: 1058 Sum: 5114172 Ratio:  99.93%)
  Bounded    : 111      (Average: 30.66 Max: 107 Sum:   3403 Ratio:   0.07%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 676714   (Eliminated:    0 Frozen: 212515)
Constraints  : 5006930  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 56
Time         : 423.459s (Solving: 399.46s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 423.480s

Choices      : 6095255  (Domain: 5938570)
Conflicts    : 417514   (Analyzed: 417511)
Restarts     : 5143     (Average: 81.18 Last: 199)
Model-Level  : 148.0   
Problems     : 56       (Average Length: 73.52 Splits: 0)
Lemmas       : 417511   (Deleted: 382970)
  Binary     : 9683     (Ratio:   2.32%)
  Ternary    : 3582     (Ratio:   0.86%)
  Conflict   : 417511   (Average Length:  453.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 417511   (Average: 12.74 Max: 1058 Sum: 5319045)
  Executed   : 417400   (Average: 12.73 Max: 1058 Sum: 5315642 Ratio:  99.94%)
  Bounded    : 111      (Average: 30.66 Max: 107 Sum:   3403 Ratio:   0.06%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 709660   (Eliminated:    0 Frozen: 222950)
Constraints  : 5256489  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 11.10s
Memory:		 802MB (+32MB)
UNKNOWN
Iteration Time:	 12.05s

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

Models       : 0+
Calls        : 57
Time         : 433.449s (Solving: 408.05s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 433.472s

Choices      : 6169695  (Domain: 6013009)
Conflicts    : 425778   (Analyzed: 425775)
Restarts     : 5243     (Average: 81.21 Last: 199)
Model-Level  : 148.0   
Problems     : 57       (Average Length: 74.28 Splits: 0)
Lemmas       : 425775   (Deleted: 390387)
  Binary     : 9704     (Ratio:   2.28%)
  Ternary    : 3584     (Ratio:   0.84%)
  Conflict   : 425775   (Average Length:  453.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 425775   (Average: 12.62 Max: 1058 Sum: 5372357)
  Executed   : 425664   (Average: 12.61 Max: 1058 Sum: 5368954 Ratio:  99.94%)
  Bounded    : 111      (Average: 30.66 Max: 107 Sum:   3403 Ratio:   0.06%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 742606   (Eliminated:    0 Frozen: 233385)
Constraints  : 5506074  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 8.73s
Memory:		 857MB (+4MB)
UNKNOWN
Iteration Time:	 10.00s

Iteration 57
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        : 58
Time         : 438.137s (Solving: 412.59s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 438.164s

Choices      : 6202218  (Domain: 6045532)
Conflicts    : 433386   (Analyzed: 433383)
Restarts     : 5343     (Average: 81.11 Last: 199)
Model-Level  : 148.0   
Problems     : 58       (Average Length: 75.02 Splits: 0)
Lemmas       : 433383   (Deleted: 398473)
  Binary     : 9732     (Ratio:   2.25%)
  Ternary    : 3589     (Ratio:   0.83%)
  Conflict   : 433383   (Average Length:  451.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 433383   (Average: 12.46 Max: 1058 Sum: 5399873)
  Executed   : 433271   (Average: 12.45 Max: 1058 Sum: 5396353 Ratio:  99.93%)
  Bounded    : 112      (Average: 31.43 Max: 117 Sum:   3520 Ratio:   0.07%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 742606   (Eliminated:    0 Frozen: 233385)
Constraints  : 5506074  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

Iteration 58
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        : 59
Time         : 444.999s (Solving: 419.29s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 445.028s

Choices      : 6240550  (Domain: 6083864)
Conflicts    : 441543   (Analyzed: 441540)
Restarts     : 5443     (Average: 81.12 Last: 199)
Model-Level  : 148.0   
Problems     : 59       (Average Length: 75.73 Splits: 0)
Lemmas       : 441540   (Deleted: 405905)
  Binary     : 9761     (Ratio:   2.21%)
  Ternary    : 3592     (Ratio:   0.81%)
  Conflict   : 441540   (Average Length:  450.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 441540   (Average: 12.30 Max: 1058 Sum: 5431406)
  Executed   : 441428   (Average: 12.29 Max: 1058 Sum: 5427886 Ratio:  99.94%)
  Bounded    : 112      (Average: 31.43 Max: 117 Sum:   3520 Ratio:   0.06%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 742606   (Eliminated:    0 Frozen: 233385)
Constraints  : 5506061  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 6.81s
Memory:		 857MB (+0MB)
UNKNOWN
Iteration Time:	 6.87s

Iteration 59
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        : 60
Time         : 451.503s (Solving: 425.65s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 451.536s

Choices      : 6302523  (Domain: 6145837)
Conflicts    : 449969   (Analyzed: 449966)
Restarts     : 5543     (Average: 81.18 Last: 199)
Model-Level  : 148.0   
Problems     : 60       (Average Length: 76.42 Splits: 0)
Lemmas       : 449966   (Deleted: 413770)
  Binary     : 9826     (Ratio:   2.18%)
  Ternary    : 3606     (Ratio:   0.80%)
  Conflict   : 449966   (Average Length:  453.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 449966   (Average: 12.18 Max: 1058 Sum: 5482244)
  Executed   : 449854   (Average: 12.18 Max: 1058 Sum: 5478724 Ratio:  99.94%)
  Bounded    : 112      (Average: 31.43 Max: 117 Sum:   3520 Ratio:   0.06%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 742606   (Eliminated:    0 Frozen: 233385)
Constraints  : 5506061  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

Iteration 60
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        : 61
Time         : 459.521s (Solving: 433.50s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 459.560s

Choices      : 6368446  (Domain: 6211751)
Conflicts    : 458324   (Analyzed: 458321)
Restarts     : 5643     (Average: 81.22 Last: 199)
Model-Level  : 148.0   
Problems     : 61       (Average Length: 77.08 Splits: 0)
Lemmas       : 458321   (Deleted: 421968)
  Binary     : 9920     (Ratio:   2.16%)
  Ternary    : 3614     (Ratio:   0.79%)
  Conflict   : 458321   (Average Length:  468.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 458321   (Average: 12.06 Max: 1058 Sum: 5528485)
  Executed   : 458209   (Average: 12.05 Max: 1058 Sum: 5524965 Ratio:  99.94%)
  Bounded    : 112      (Average: 31.43 Max: 117 Sum:   3520 Ratio:   0.06%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 742606   (Eliminated:    0 Frozen: 233385)
Constraints  : 5506061  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

Iteration 61
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        : 62
Time         : 467.796s (Solving: 441.63s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 467.840s

Choices      : 6423923  (Domain: 6267183)
Conflicts    : 466042   (Analyzed: 466039)
Restarts     : 5743     (Average: 81.15 Last: 199)
Model-Level  : 148.0   
Problems     : 62       (Average Length: 77.73 Splits: 0)
Lemmas       : 466039   (Deleted: 430119)
  Binary     : 9967     (Ratio:   2.14%)
  Ternary    : 3621     (Ratio:   0.78%)
  Conflict   : 466039   (Average Length:  486.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 466039   (Average: 11.93 Max: 1058 Sum: 5560681)
  Executed   : 465927   (Average: 11.92 Max: 1058 Sum: 5557161 Ratio:  99.94%)
  Bounded    : 112      (Average: 31.43 Max: 117 Sum:   3520 Ratio:   0.06%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 742606   (Eliminated:    0 Frozen: 233385)
Constraints  : 5506061  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

Iteration 62
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        : 63
Time         : 473.874s (Solving: 447.55s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 473.920s

Choices      : 6483121  (Domain: 6325618)
Conflicts    : 473770   (Analyzed: 473767)
Restarts     : 5843     (Average: 81.08 Last: 199)
Model-Level  : 148.0   
Problems     : 63       (Average Length: 78.35 Splits: 0)
Lemmas       : 473767   (Deleted: 437651)
  Binary     : 10000    (Ratio:   2.11%)
  Ternary    : 3626     (Ratio:   0.77%)
  Conflict   : 473767   (Average Length:  486.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 473767   (Average: 11.83 Max: 1058 Sum: 5606098)
  Executed   : 473655   (Average: 11.83 Max: 1058 Sum: 5602578 Ratio:  99.94%)
  Bounded    : 112      (Average: 31.43 Max: 117 Sum:   3520 Ratio:   0.06%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 742606   (Eliminated:    0 Frozen: 233385)
Constraints  : 5506061  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

Iteration 63
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        : 64
Time         : 481.677s (Solving: 455.16s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 481.724s

Choices      : 6569867  (Domain: 6412264)
Conflicts    : 482429   (Analyzed: 482426)
Restarts     : 5943     (Average: 81.18 Last: 199)
Model-Level  : 148.0   
Problems     : 64       (Average Length: 78.95 Splits: 0)
Lemmas       : 482426   (Deleted: 447280)
  Binary     : 10091    (Ratio:   2.09%)
  Ternary    : 3643     (Ratio:   0.76%)
  Conflict   : 482426   (Average Length:  493.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 482426   (Average: 11.76 Max: 1058 Sum: 5673538)
  Executed   : 482314   (Average: 11.75 Max: 1058 Sum: 5670018 Ratio:  99.94%)
  Bounded    : 112      (Average: 31.43 Max: 117 Sum:   3520 Ratio:   0.06%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 742606   (Eliminated:    0 Frozen: 233385)
Constraints  : 5506061  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

Iteration 64
Queue:		 [(14,70,2,True), (15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,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         : 490.031s (Solving: 463.35s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 490.080s

Choices      : 6660411  (Domain: 6502426)
Conflicts    : 490907   (Analyzed: 490904)
Restarts     : 6043     (Average: 81.24 Last: 199)
Model-Level  : 148.0   
Problems     : 65       (Average Length: 79.54 Splits: 0)
Lemmas       : 490904   (Deleted: 453451)
  Binary     : 10187    (Ratio:   2.08%)
  Ternary    : 3671     (Ratio:   0.75%)
  Conflict   : 490904   (Average Length:  499.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 490904   (Average: 11.69 Max: 1058 Sum: 5741051)
  Executed   : 490792   (Average: 11.69 Max: 1058 Sum: 5737531 Ratio:  99.94%)
  Bounded    : 112      (Average: 31.43 Max: 117 Sum:   3520 Ratio:   0.06%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 742606   (Eliminated:    0 Frozen: 233385)
Constraints  : 5506061  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 8.30s
Memory:		 857MB (+0MB)
UNKNOWN
Iteration Time:	 8.36s

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

Models       : 0+
Calls        : 66
Time         : 498.612s (Solving: 471.77s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 498.656s

Choices      : 6750029  (Domain: 6590608)
Conflicts    : 499206   (Analyzed: 499203)
Restarts     : 6143     (Average: 81.26 Last: 199)
Model-Level  : 148.0   
Problems     : 66       (Average Length: 80.11 Splits: 0)
Lemmas       : 499203   (Deleted: 461699)
  Binary     : 10243    (Ratio:   2.05%)
  Ternary    : 3694     (Ratio:   0.74%)
  Conflict   : 499203   (Average Length:  498.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 499203   (Average: 11.64 Max: 1058 Sum: 5812823)
  Executed   : 499090   (Average: 11.64 Max: 1058 Sum: 5809186 Ratio:  99.94%)
  Bounded    : 113      (Average: 32.19 Max: 117 Sum:   3637 Ratio:   0.06%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 742606   (Eliminated:    0 Frozen: 233385)
Constraints  : 5506061  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 67
Time         : 508.112s (Solving: 481.12s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 508.160s

Choices      : 6838515  (Domain: 6679092)
Conflicts    : 507401   (Analyzed: 507398)
Restarts     : 6243     (Average: 81.27 Last: 199)
Model-Level  : 148.0   
Problems     : 67       (Average Length: 80.66 Splits: 0)
Lemmas       : 507398   (Deleted: 469898)
  Binary     : 10285    (Ratio:   2.03%)
  Ternary    : 3703     (Ratio:   0.73%)
  Conflict   : 507398   (Average Length:  502.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 507398   (Average: 11.57 Max: 1058 Sum: 5872503)
  Executed   : 507285   (Average: 11.57 Max: 1058 Sum: 5868866 Ratio:  99.94%)
  Bounded    : 113      (Average: 32.19 Max: 117 Sum:   3637 Ratio:   0.06%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 742606   (Eliminated:    0 Frozen: 233385)
Constraints  : 5506047  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 68
Time         : 516.589s (Solving: 489.41s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 516.640s

Choices      : 6927122  (Domain: 6767680)
Conflicts    : 515786   (Analyzed: 515783)
Restarts     : 6343     (Average: 81.32 Last: 199)
Model-Level  : 148.0   
Problems     : 68       (Average Length: 81.19 Splits: 0)
Lemmas       : 515783   (Deleted: 477840)
  Binary     : 10306    (Ratio:   2.00%)
  Ternary    : 3717     (Ratio:   0.72%)
  Conflict   : 515783   (Average Length:  503.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 515783   (Average: 11.51 Max: 1058 Sum: 5938286)
  Executed   : 515670   (Average: 11.51 Max: 1058 Sum: 5934649 Ratio:  99.94%)
  Bounded    : 113      (Average: 32.19 Max: 117 Sum:   3637 Ratio:   0.06%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 742606   (Eliminated:    0 Frozen: 233385)
Constraints  : 5506047  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

Iteration 68
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        : 69
Time         : 521.638s (Solving: 494.29s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 521.688s

Choices      : 6972117  (Domain: 6812675)
Conflicts    : 523446   (Analyzed: 523443)
Restarts     : 6443     (Average: 81.24 Last: 199)
Model-Level  : 148.0   
Problems     : 69       (Average Length: 81.71 Splits: 0)
Lemmas       : 523443   (Deleted: 486016)
  Binary     : 10394    (Ratio:   1.99%)
  Ternary    : 3727     (Ratio:   0.71%)
  Conflict   : 523443   (Average Length:  501.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 523443   (Average: 11.42 Max: 1058 Sum: 5977673)
  Executed   : 523330   (Average: 11.41 Max: 1058 Sum: 5974036 Ratio:  99.94%)
  Bounded    : 113      (Average: 32.19 Max: 117 Sum:   3637 Ratio:   0.06%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 742606   (Eliminated:    0 Frozen: 233385)
Constraints  : 5506047  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

Iteration 69
Queue:		 [(5,25,5,True), (6,30,5,True), (7,35,4,True), (8,40,4,True), (9,45,4,True), (10,50,4,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         : 532.270s (Solving: 504.74s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 532.324s

Choices      : 7024016  (Domain: 6864574)
Conflicts    : 532564   (Analyzed: 532561)
Restarts     : 6543     (Average: 81.39 Last: 199)
Model-Level  : 148.0   
Problems     : 70       (Average Length: 82.21 Splits: 0)
Lemmas       : 532561   (Deleted: 495546)
  Binary     : 10420    (Ratio:   1.96%)
  Ternary    : 3730     (Ratio:   0.70%)
  Conflict   : 532561   (Average Length:  510.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 532561   (Average: 11.30 Max: 1058 Sum: 6017997)
  Executed   : 532448   (Average: 11.29 Max: 1058 Sum: 6014360 Ratio:  99.94%)
  Bounded    : 113      (Average: 32.19 Max: 117 Sum:   3637 Ratio:   0.06%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 742606   (Eliminated:    0 Frozen: 233385)
Constraints  : 5506047  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 10.57s
Memory:		 857MB (+0MB)
UNKNOWN
Iteration Time:	 10.64s

Iteration 70
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        : 71
Time         : 539.480s (Solving: 511.78s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 539.536s

Choices      : 7075739  (Domain: 6916297)
Conflicts    : 541125   (Analyzed: 541122)
Restarts     : 6643     (Average: 81.46 Last: 199)
Model-Level  : 148.0   
Problems     : 71       (Average Length: 82.70 Splits: 0)
Lemmas       : 541122   (Deleted: 502319)
  Binary     : 10467    (Ratio:   1.93%)
  Ternary    : 3744     (Ratio:   0.69%)
  Conflict   : 541122   (Average Length:  509.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 541122   (Average: 11.20 Max: 1058 Sum: 6058554)
  Executed   : 541009   (Average: 11.19 Max: 1058 Sum: 6054917 Ratio:  99.94%)
  Bounded    : 113      (Average: 32.19 Max: 117 Sum:   3637 Ratio:   0.06%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 742606   (Eliminated:    0 Frozen: 233385)
Constraints  : 5506047  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

Iteration 71
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        : 72
Time         : 546.729s (Solving: 518.88s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 546.788s

Choices      : 7141225  (Domain: 6981783)
Conflicts    : 549648   (Analyzed: 549645)
Restarts     : 6743     (Average: 81.51 Last: 199)
Model-Level  : 148.0   
Problems     : 72       (Average Length: 83.18 Splits: 0)
Lemmas       : 549645   (Deleted: 510685)
  Binary     : 10534    (Ratio:   1.92%)
  Ternary    : 3757     (Ratio:   0.68%)
  Conflict   : 549645   (Average Length:  516.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 549645   (Average: 11.11 Max: 1058 Sum: 6104837)
  Executed   : 549532   (Average: 11.10 Max: 1058 Sum: 6101200 Ratio:  99.94%)
  Bounded    : 113      (Average: 32.19 Max: 117 Sum:   3637 Ratio:   0.06%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 742606   (Eliminated:    0 Frozen: 233385)
Constraints  : 5506047  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

Iteration 72
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        : 73
Time         : 555.168s (Solving: 527.13s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 555.232s

Choices      : 7224004  (Domain: 7063798)
Conflicts    : 557776   (Analyzed: 557773)
Restarts     : 6843     (Average: 81.51 Last: 199)
Model-Level  : 148.0   
Problems     : 73       (Average Length: 83.64 Splits: 0)
Lemmas       : 557773   (Deleted: 518948)
  Binary     : 10660    (Ratio:   1.91%)
  Ternary    : 3779     (Ratio:   0.68%)
  Conflict   : 557773   (Average Length:  526.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 557773   (Average: 11.05 Max: 1058 Sum: 6165088)
  Executed   : 557660   (Average: 11.05 Max: 1058 Sum: 6161451 Ratio:  99.94%)
  Bounded    : 113      (Average: 32.19 Max: 117 Sum:   3637 Ratio:   0.06%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 742606   (Eliminated:    0 Frozen: 233385)
Constraints  : 5506047  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 8.37s
Memory:		 857MB (+0MB)
UNKNOWN
Iteration Time:	 8.44s

Iteration 73
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        : 74
Time         : 561.209s (Solving: 533.00s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 561.280s

Choices      : 7285602  (Domain: 7125365)
Conflicts    : 565760   (Analyzed: 565757)
Restarts     : 6943     (Average: 81.49 Last: 199)
Model-Level  : 148.0   
Problems     : 74       (Average Length: 84.09 Splits: 0)
Lemmas       : 565757   (Deleted: 526870)
  Binary     : 10682    (Ratio:   1.89%)
  Ternary    : 3786     (Ratio:   0.67%)
  Conflict   : 565757   (Average Length:  530.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 565757   (Average: 10.98 Max: 1058 Sum: 6211042)
  Executed   : 565644   (Average: 10.97 Max: 1058 Sum: 6207405 Ratio:  99.94%)
  Bounded    : 113      (Average: 32.19 Max: 117 Sum:   3637 Ratio:   0.06%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 742606   (Eliminated:    0 Frozen: 233385)
Constraints  : 5506047  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

Iteration 74
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        : 75
Time         : 567.239s (Solving: 538.86s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 567.312s

Choices      : 7351056  (Domain: 7190796)
Conflicts    : 573593   (Analyzed: 573590)
Restarts     : 7043     (Average: 81.44 Last: 199)
Model-Level  : 148.0   
Problems     : 75       (Average Length: 84.53 Splits: 0)
Lemmas       : 573590   (Deleted: 534658)
  Binary     : 10689    (Ratio:   1.86%)
  Ternary    : 3793     (Ratio:   0.66%)
  Conflict   : 573590   (Average Length:  532.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 573590   (Average: 10.92 Max: 1058 Sum: 6261502)
  Executed   : 573477   (Average: 10.91 Max: 1058 Sum: 6257865 Ratio:  99.94%)
  Bounded    : 113      (Average: 32.19 Max: 117 Sum:   3637 Ratio:   0.06%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 742606   (Eliminated:    0 Frozen: 233385)
Constraints  : 5506047  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

Iteration 75
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        : 76
Time         : 573.962s (Solving: 545.41s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 574.036s

Choices      : 7423032  (Domain: 7262757)
Conflicts    : 582261   (Analyzed: 582258)
Restarts     : 7143     (Average: 81.51 Last: 199)
Model-Level  : 148.0   
Problems     : 76       (Average Length: 84.96 Splits: 0)
Lemmas       : 582258   (Deleted: 544502)
  Binary     : 10722    (Ratio:   1.84%)
  Ternary    : 3805     (Ratio:   0.65%)
  Conflict   : 582258   (Average Length:  536.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 582258   (Average: 10.85 Max: 1058 Sum: 6315671)
  Executed   : 582145   (Average: 10.84 Max: 1058 Sum: 6312034 Ratio:  99.94%)
  Bounded    : 113      (Average: 32.19 Max: 117 Sum:   3637 Ratio:   0.06%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 742606   (Eliminated:    0 Frozen: 233385)
Constraints  : 5506047  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

Iteration 76
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        : 77
Time         : 583.396s (Solving: 554.68s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 583.472s

Choices      : 7546732  (Domain: 7386230)
Conflicts    : 590685   (Analyzed: 590682)
Restarts     : 7243     (Average: 81.55 Last: 199)
Model-Level  : 148.0   
Problems     : 77       (Average Length: 85.38 Splits: 0)
Lemmas       : 590682   (Deleted: 550812)
  Binary     : 10855    (Ratio:   1.84%)
  Ternary    : 3822     (Ratio:   0.65%)
  Conflict   : 590682   (Average Length:  544.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 590682   (Average: 10.86 Max: 1058 Sum: 6412052)
  Executed   : 590569   (Average: 10.85 Max: 1058 Sum: 6408415 Ratio:  99.94%)
  Bounded    : 113      (Average: 32.19 Max: 117 Sum:   3637 Ratio:   0.06%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 742606   (Eliminated:    0 Frozen: 233385)
Constraints  : 5506047  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 9.38s
Memory:		 857MB (+0MB)
UNKNOWN
Iteration Time:	 9.44s

Iteration 77
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        : 78
Time         : 592.007s (Solving: 563.14s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 592.084s

Choices      : 7639224  (Domain: 7478679)
Conflicts    : 599022   (Analyzed: 599019)
Restarts     : 7343     (Average: 81.58 Last: 199)
Model-Level  : 148.0   
Problems     : 78       (Average Length: 85.78 Splits: 0)
Lemmas       : 599019   (Deleted: 558937)
  Binary     : 10897    (Ratio:   1.82%)
  Ternary    : 3833     (Ratio:   0.64%)
  Conflict   : 599019   (Average Length:  545.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 599019   (Average: 10.82 Max: 1058 Sum: 6483134)
  Executed   : 598906   (Average: 10.82 Max: 1058 Sum: 6479497 Ratio:  99.94%)
  Bounded    : 113      (Average: 32.19 Max: 117 Sum:   3637 Ratio:   0.06%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 742606   (Eliminated:    0 Frozen: 233385)
Constraints  : 5506047  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 8.56s
Memory:		 857MB (+0MB)
UNKNOWN
Iteration Time:	 8.62s

Iteration 78
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        : 79
Time         : 598.408s (Solving: 569.37s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 598.488s

Choices      : 7701168  (Domain: 7540622)
Conflicts    : 606830   (Analyzed: 606827)
Restarts     : 7443     (Average: 81.53 Last: 199)
Model-Level  : 148.0   
Problems     : 79       (Average Length: 86.18 Splits: 0)
Lemmas       : 606827   (Deleted: 567084)
  Binary     : 10970    (Ratio:   1.81%)
  Ternary    : 3849     (Ratio:   0.63%)
  Conflict   : 606827   (Average Length:  545.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 606827   (Average: 10.77 Max: 1058 Sum: 6536396)
  Executed   : 606714   (Average: 10.77 Max: 1058 Sum: 6532759 Ratio:  99.94%)
  Bounded    : 113      (Average: 32.19 Max: 117 Sum:   3637 Ratio:   0.06%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 742606   (Eliminated:    0 Frozen: 233385)
Constraints  : 5506047  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

Iteration 79
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        : 80
Time         : 607.848s (Solving: 578.65s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 607.932s

Choices      : 7750646  (Domain: 7590100)
Conflicts    : 615547   (Analyzed: 615544)
Restarts     : 7543     (Average: 81.60 Last: 199)
Model-Level  : 148.0   
Problems     : 80       (Average Length: 86.56 Splits: 0)
Lemmas       : 615544   (Deleted: 576756)
  Binary     : 11003    (Ratio:   1.79%)
  Ternary    : 3854     (Ratio:   0.63%)
  Conflict   : 615544   (Average Length:  550.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 615544   (Average: 10.68 Max: 1058 Sum: 6575957)
  Executed   : 615431   (Average: 10.68 Max: 1058 Sum: 6572320 Ratio:  99.94%)
  Bounded    : 113      (Average: 32.19 Max: 117 Sum:   3637 Ratio:   0.06%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 742606   (Eliminated:    0 Frozen: 233385)
Constraints  : 5506047  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

Iteration 80
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        : 81
Time         : 614.123s (Solving: 584.78s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 614.208s

Choices      : 7804164  (Domain: 7643618)
Conflicts    : 623754   (Analyzed: 623751)
Restarts     : 7643     (Average: 81.61 Last: 199)
Model-Level  : 148.0   
Problems     : 81       (Average Length: 86.94 Splits: 0)
Lemmas       : 623751   (Deleted: 583195)
  Binary     : 11019    (Ratio:   1.77%)
  Ternary    : 3862     (Ratio:   0.62%)
  Conflict   : 623751   (Average Length:  549.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 623751   (Average: 10.61 Max: 1058 Sum: 6616578)
  Executed   : 623638   (Average: 10.60 Max: 1058 Sum: 6612941 Ratio:  99.95%)
  Bounded    : 113      (Average: 32.19 Max: 117 Sum:   3637 Ratio:   0.05%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 742606   (Eliminated:    0 Frozen: 233385)
Constraints  : 5506047  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

Iteration 81
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        : 82
Time         : 622.288s (Solving: 592.78s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 622.380s

Choices      : 7869664  (Domain: 7708891)
Conflicts    : 632230   (Analyzed: 632227)
Restarts     : 7743     (Average: 81.65 Last: 199)
Model-Level  : 148.0   
Problems     : 82       (Average Length: 87.30 Splits: 0)
Lemmas       : 632227   (Deleted: 591220)
  Binary     : 11073    (Ratio:   1.75%)
  Ternary    : 3869     (Ratio:   0.61%)
  Conflict   : 632227   (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    : 632227   (Average: 10.54 Max: 1058 Sum: 6661979)
  Executed   : 632114   (Average: 10.53 Max: 1058 Sum: 6658342 Ratio:  99.95%)
  Bounded    : 113      (Average: 32.19 Max: 117 Sum:   3637 Ratio:   0.05%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 742606   (Eliminated:    0 Frozen: 233385)
Constraints  : 5506047  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

Iteration 82
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        : 83
Time         : 628.508s (Solving: 598.84s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 628.604s

Choices      : 7924346  (Domain: 7763559)
Conflicts    : 640076   (Analyzed: 640073)
Restarts     : 7843     (Average: 81.61 Last: 199)
Model-Level  : 148.0   
Problems     : 83       (Average Length: 87.66 Splits: 0)
Lemmas       : 640073   (Deleted: 599476)
  Binary     : 11104    (Ratio:   1.73%)
  Ternary    : 3891     (Ratio:   0.61%)
  Conflict   : 640073   (Average Length:  557.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 640073   (Average: 10.48 Max: 1058 Sum: 6705046)
  Executed   : 639960   (Average: 10.47 Max: 1058 Sum: 6701409 Ratio:  99.95%)
  Bounded    : 113      (Average: 32.19 Max: 117 Sum:   3637 Ratio:   0.05%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 742606   (Eliminated:    0 Frozen: 233385)
Constraints  : 5506047  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

Iteration 83
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        : 84
Time         : 637.078s (Solving: 607.25s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 637.176s

Choices      : 8001331  (Domain: 7840540)
Conflicts    : 648455   (Analyzed: 648452)
Restarts     : 7943     (Average: 81.64 Last: 199)
Model-Level  : 148.0   
Problems     : 84       (Average Length: 88.01 Splits: 0)
Lemmas       : 648452   (Deleted: 607111)
  Binary     : 11153    (Ratio:   1.72%)
  Ternary    : 3897     (Ratio:   0.60%)
  Conflict   : 648452   (Average Length:  565.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 648452   (Average: 10.42 Max: 1058 Sum: 6759738)
  Executed   : 648339   (Average: 10.42 Max: 1058 Sum: 6756101 Ratio:  99.95%)
  Bounded    : 113      (Average: 32.19 Max: 117 Sum:   3637 Ratio:   0.05%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 742606   (Eliminated:    0 Frozen: 233385)
Constraints  : 5506047  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

Iteration 84
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        : 85
Time         : 645.136s (Solving: 615.13s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 645.236s

Choices      : 8064931  (Domain: 7904133)
Conflicts    : 656449   (Analyzed: 656446)
Restarts     : 8043     (Average: 81.62 Last: 199)
Model-Level  : 148.0   
Problems     : 85       (Average Length: 88.35 Splits: 0)
Lemmas       : 656446   (Deleted: 615346)
  Binary     : 11172    (Ratio:   1.70%)
  Ternary    : 3900     (Ratio:   0.59%)
  Conflict   : 656446   (Average Length:  565.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 656446   (Average: 10.37 Max: 1058 Sum: 6807063)
  Executed   : 656333   (Average: 10.36 Max: 1058 Sum: 6803426 Ratio:  99.95%)
  Bounded    : 113      (Average: 32.19 Max: 117 Sum:   3637 Ratio:   0.05%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 742606   (Eliminated:    0 Frozen: 233385)
Constraints  : 5506047  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

Iteration 85
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        : 86
Time         : 655.553s (Solving: 625.38s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 655.656s

Choices      : 8162962  (Domain: 8002144)
Conflicts    : 664960   (Analyzed: 664957)
Restarts     : 8143     (Average: 81.66 Last: 199)
Model-Level  : 148.0   
Problems     : 86       (Average Length: 88.69 Splits: 0)
Lemmas       : 664957   (Deleted: 623180)
  Binary     : 11209    (Ratio:   1.69%)
  Ternary    : 3904     (Ratio:   0.59%)
  Conflict   : 664957   (Average Length:  574.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 664957   (Average: 10.34 Max: 1058 Sum: 6874599)
  Executed   : 664844   (Average: 10.33 Max: 1058 Sum: 6870962 Ratio:  99.95%)
  Bounded    : 113      (Average: 32.19 Max: 117 Sum:   3637 Ratio:   0.05%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 742606   (Eliminated:    0 Frozen: 233385)
Constraints  : 5506047  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

Iteration 86
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        : 87
Time         : 660.441s (Solving: 630.07s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 660.544s

Choices      : 8213787  (Domain: 8052969)
Conflicts    : 672654   (Analyzed: 672651)
Restarts     : 8243     (Average: 81.60 Last: 199)
Model-Level  : 148.0   
Problems     : 87       (Average Length: 89.01 Splits: 0)
Lemmas       : 672651   (Deleted: 631493)
  Binary     : 11263    (Ratio:   1.67%)
  Ternary    : 3911     (Ratio:   0.58%)
  Conflict   : 672651   (Average Length:  575.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 672651   (Average: 10.28 Max: 1058 Sum: 6917793)
  Executed   : 672537   (Average: 10.28 Max: 1058 Sum: 6914039 Ratio:  99.95%)
  Bounded    : 114      (Average: 32.93 Max: 117 Sum:   3754 Ratio:   0.05%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 742606   (Eliminated:    0 Frozen: 233385)
Constraints  : 5506047  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

Iteration 87
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        : 88
Time         : 670.337s (Solving: 639.78s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 670.444s

Choices      : 8255021  (Domain: 8094203)
Conflicts    : 681563   (Analyzed: 681560)
Restarts     : 8343     (Average: 81.69 Last: 199)
Model-Level  : 148.0   
Problems     : 88       (Average Length: 89.33 Splits: 0)
Lemmas       : 681560   (Deleted: 641187)
  Binary     : 11282    (Ratio:   1.66%)
  Ternary    : 3915     (Ratio:   0.57%)
  Conflict   : 681560   (Average Length:  582.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 681560   (Average: 10.20 Max: 1058 Sum: 6948663)
  Executed   : 681446   (Average: 10.19 Max: 1058 Sum: 6944909 Ratio:  99.95%)
  Bounded    : 114      (Average: 32.93 Max: 117 Sum:   3754 Ratio:   0.05%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 742606   (Eliminated:    0 Frozen: 233385)
Constraints  : 5506021  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

Iteration 88
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        : 89
Time         : 677.573s (Solving: 646.85s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 677.684s

Choices      : 8313740  (Domain: 8152922)
Conflicts    : 689779   (Analyzed: 689776)
Restarts     : 8443     (Average: 81.70 Last: 199)
Model-Level  : 148.0   
Problems     : 89       (Average Length: 89.64 Splits: 0)
Lemmas       : 689776   (Deleted: 647830)
  Binary     : 11326    (Ratio:   1.64%)
  Ternary    : 3920     (Ratio:   0.57%)
  Conflict   : 689776   (Average Length:  586.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 689776   (Average: 10.13 Max: 1058 Sum: 6988292)
  Executed   : 689662   (Average: 10.13 Max: 1058 Sum: 6984538 Ratio:  99.95%)
  Bounded    : 114      (Average: 32.93 Max: 117 Sum:   3754 Ratio:   0.05%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 742606   (Eliminated:    0 Frozen: 233385)
Constraints  : 5506021  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

Iteration 89
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        : 90
Time         : 684.716s (Solving: 653.83s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 684.832s

Choices      : 8377164  (Domain: 8216341)
Conflicts    : 698142   (Analyzed: 698139)
Restarts     : 8543     (Average: 81.72 Last: 199)
Model-Level  : 148.0   
Problems     : 90       (Average Length: 89.94 Splits: 0)
Lemmas       : 698139   (Deleted: 655884)
  Binary     : 11352    (Ratio:   1.63%)
  Ternary    : 3924     (Ratio:   0.56%)
  Conflict   : 698139   (Average Length:  587.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 698139   (Average: 10.08 Max: 1058 Sum: 7038067)
  Executed   : 698025   (Average: 10.08 Max: 1058 Sum: 7034313 Ratio:  99.95%)
  Bounded    : 114      (Average: 32.93 Max: 117 Sum:   3754 Ratio:   0.05%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 742606   (Eliminated:    0 Frozen: 233385)
Constraints  : 5506021  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

Iteration 90
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        : 91
Time         : 692.954s (Solving: 661.89s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 693.076s

Choices      : 8443070  (Domain: 8282247)
Conflicts    : 706403   (Analyzed: 706400)
Restarts     : 8643     (Average: 81.73 Last: 199)
Model-Level  : 148.0   
Problems     : 91       (Average Length: 90.24 Splits: 0)
Lemmas       : 706400   (Deleted: 664086)
  Binary     : 11374    (Ratio:   1.61%)
  Ternary    : 3926     (Ratio:   0.56%)
  Conflict   : 706400   (Average Length:  586.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 706400   (Average: 10.03 Max: 1058 Sum: 7088156)
  Executed   : 706286   (Average: 10.03 Max: 1058 Sum: 7084402 Ratio:  99.95%)
  Bounded    : 114      (Average: 32.93 Max: 117 Sum:   3754 Ratio:   0.05%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 742606   (Eliminated:    0 Frozen: 233385)
Constraints  : 5506021  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

Iteration 91
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        : 92
Time         : 701.785s (Solving: 670.54s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 701.908s

Choices      : 8518957  (Domain: 8358110)
Conflicts    : 714658   (Analyzed: 714655)
Restarts     : 8743     (Average: 81.74 Last: 199)
Model-Level  : 148.0   
Problems     : 92       (Average Length: 90.53 Splits: 0)
Lemmas       : 714655   (Deleted: 672195)
  Binary     : 11403    (Ratio:   1.60%)
  Ternary    : 3935     (Ratio:   0.55%)
  Conflict   : 714655   (Average Length:  588.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 714655   (Average: 10.00 Max: 1058 Sum: 7144264)
  Executed   : 714541   (Average:  9.99 Max: 1058 Sum: 7140510 Ratio:  99.95%)
  Bounded    : 114      (Average: 32.93 Max: 117 Sum:   3754 Ratio:   0.05%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 742606   (Eliminated:    0 Frozen: 233385)
Constraints  : 5506021  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

Iteration 92
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        : 93
Time         : 709.638s (Solving: 678.20s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 709.764s

Choices      : 8603940  (Domain: 8443037)
Conflicts    : 722921   (Analyzed: 722918)
Restarts     : 8843     (Average: 81.75 Last: 199)
Model-Level  : 148.0   
Problems     : 93       (Average Length: 90.82 Splits: 0)
Lemmas       : 722918   (Deleted: 680248)
  Binary     : 11430    (Ratio:   1.58%)
  Ternary    : 3940     (Ratio:   0.55%)
  Conflict   : 722918   (Average Length:  589.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 722918   (Average:  9.97 Max: 1058 Sum: 7209996)
  Executed   : 722804   (Average:  9.97 Max: 1058 Sum: 7206242 Ratio:  99.95%)
  Bounded    : 114      (Average: 32.93 Max: 117 Sum:   3754 Ratio:   0.05%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 742606   (Eliminated:    0 Frozen: 233385)
Constraints  : 5506021  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 7.78s
Memory:		 857MB (+0MB)
UNKNOWN
Iteration Time:	 7.86s

Iteration 93
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        : 94
Time         : 718.195s (Solving: 686.58s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 718.324s

Choices      : 8706565  (Domain: 8545601)
Conflicts    : 731785   (Analyzed: 731782)
Restarts     : 8943     (Average: 81.83 Last: 199)
Model-Level  : 148.0   
Problems     : 94       (Average Length: 91.10 Splits: 0)
Lemmas       : 731782   (Deleted: 690497)
  Binary     : 11482    (Ratio:   1.57%)
  Ternary    : 3948     (Ratio:   0.54%)
  Conflict   : 731782   (Average Length:  594.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 731782   (Average:  9.95 Max: 1058 Sum: 7282683)
  Executed   : 731668   (Average:  9.95 Max: 1058 Sum: 7278929 Ratio:  99.95%)
  Bounded    : 114      (Average: 32.93 Max: 117 Sum:   3754 Ratio:   0.05%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 742606   (Eliminated:    0 Frozen: 233385)
Constraints  : 5506021  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

Iteration 94
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        : 95
Time         : 722.369s (Solving: 690.59s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 722.500s

Choices      : 8755018  (Domain: 8594054)
Conflicts    : 739296   (Analyzed: 739293)
Restarts     : 9043     (Average: 81.75 Last: 199)
Model-Level  : 148.0   
Problems     : 95       (Average Length: 91.37 Splits: 0)
Lemmas       : 739293   (Deleted: 696877)
  Binary     : 11550    (Ratio:   1.56%)
  Ternary    : 3961     (Ratio:   0.54%)
  Conflict   : 739293   (Average Length:  592.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 739293   (Average:  9.91 Max: 1058 Sum: 7325039)
  Executed   : 739179   (Average:  9.90 Max: 1058 Sum: 7321285 Ratio:  99.95%)
  Bounded    : 114      (Average: 32.93 Max: 117 Sum:   3754 Ratio:   0.05%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 742606   (Eliminated:    0 Frozen: 233385)
Constraints  : 5506021  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 4.12s
Memory:		 857MB (+0MB)
UNKNOWN
Iteration Time:	 4.18s

Iteration 95
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        : 96
Time         : 731.443s (Solving: 699.49s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 731.576s

Choices      : 8810270  (Domain: 8649306)
Conflicts    : 748234   (Analyzed: 748231)
Restarts     : 9143     (Average: 81.84 Last: 199)
Model-Level  : 148.0   
Problems     : 96       (Average Length: 91.64 Splits: 0)
Lemmas       : 748231   (Deleted: 706419)
  Binary     : 11585    (Ratio:   1.55%)
  Ternary    : 3966     (Ratio:   0.53%)
  Conflict   : 748231   (Average Length:  596.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 748231   (Average:  9.85 Max: 1058 Sum: 7369842)
  Executed   : 748117   (Average:  9.84 Max: 1058 Sum: 7366088 Ratio:  99.95%)
  Bounded    : 114      (Average: 32.93 Max: 117 Sum:   3754 Ratio:   0.05%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 742606   (Eliminated:    0 Frozen: 233385)
Constraints  : 5506021  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

Iteration 96
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        : 97
Time         : 740.986s (Solving: 708.88s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 741.124s

Choices      : 8902891  (Domain: 8741927)
Conflicts    : 756805   (Analyzed: 756802)
Restarts     : 9243     (Average: 81.88 Last: 199)
Model-Level  : 148.0   
Problems     : 97       (Average Length: 91.90 Splits: 0)
Lemmas       : 756802   (Deleted: 713026)
  Binary     : 11633    (Ratio:   1.54%)
  Ternary    : 3976     (Ratio:   0.53%)
  Conflict   : 756802   (Average Length:  601.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 756802   (Average:  9.83 Max: 1058 Sum: 7440639)
  Executed   : 756688   (Average:  9.83 Max: 1058 Sum: 7436885 Ratio:  99.95%)
  Bounded    : 114      (Average: 32.93 Max: 117 Sum:   3754 Ratio:   0.05%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 742606   (Eliminated:    0 Frozen: 233385)
Constraints  : 5506021  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 9.50s
Memory:		 857MB (+0MB)
UNKNOWN
Iteration Time:	 9.55s

Iteration 97
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        : 98
Time         : 748.422s (Solving: 716.16s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 748.564s

Choices      : 8972295  (Domain: 8811308)
Conflicts    : 765418   (Analyzed: 765415)
Restarts     : 9343     (Average: 81.92 Last: 199)
Model-Level  : 148.0   
Problems     : 98       (Average Length: 92.15 Splits: 0)
Lemmas       : 765415   (Deleted: 723528)
  Binary     : 11685    (Ratio:   1.53%)
  Ternary    : 3993     (Ratio:   0.52%)
  Conflict   : 765415   (Average Length:  606.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 765415   (Average:  9.79 Max: 1058 Sum: 7490848)
  Executed   : 765301   (Average:  9.78 Max: 1058 Sum: 7487094 Ratio:  99.95%)
  Bounded    : 114      (Average: 32.93 Max: 117 Sum:   3754 Ratio:   0.05%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 742606   (Eliminated:    0 Frozen: 233385)
Constraints  : 5506021  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

Iteration 98
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        : 99
Time         : 756.504s (Solving: 724.09s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 756.652s

Choices      : 9048323  (Domain: 8887241)
Conflicts    : 773738   (Analyzed: 773735)
Restarts     : 9443     (Average: 81.94 Last: 199)
Model-Level  : 148.0   
Problems     : 99       (Average Length: 92.40 Splits: 0)
Lemmas       : 773735   (Deleted: 729839)
  Binary     : 11754    (Ratio:   1.52%)
  Ternary    : 4004     (Ratio:   0.52%)
  Conflict   : 773735   (Average Length:  614.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 773735   (Average:  9.75 Max: 1058 Sum: 7545457)
  Executed   : 773621   (Average:  9.75 Max: 1058 Sum: 7541703 Ratio:  99.95%)
  Bounded    : 114      (Average: 32.93 Max: 117 Sum:   3754 Ratio:   0.05%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 742606   (Eliminated:    0 Frozen: 233385)
Constraints  : 5506021  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

Iteration 99
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        : 100
Time         : 765.667s (Solving: 733.10s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 765.820s

Choices      : 9130864  (Domain: 8969757)
Conflicts    : 782471   (Analyzed: 782468)
Restarts     : 9543     (Average: 81.99 Last: 199)
Model-Level  : 148.0   
Problems     : 100      (Average Length: 92.65 Splits: 0)
Lemmas       : 782468   (Deleted: 740075)
  Binary     : 11778    (Ratio:   1.51%)
  Ternary    : 4008     (Ratio:   0.51%)
  Conflict   : 782468   (Average Length:  622.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 782468   (Average:  9.72 Max: 1058 Sum: 7603314)
  Executed   : 782354   (Average:  9.71 Max: 1058 Sum: 7599560 Ratio:  99.95%)
  Bounded    : 114      (Average: 32.93 Max: 117 Sum:   3754 Ratio:   0.05%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 742606   (Eliminated:    0 Frozen: 233385)
Constraints  : 5506021  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

Iteration 100
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        : 101
Time         : 774.653s (Solving: 741.92s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 774.808s

Choices      : 9191976  (Domain: 9030867)
Conflicts    : 791222   (Analyzed: 791219)
Restarts     : 9643     (Average: 82.05 Last: 199)
Model-Level  : 148.0   
Problems     : 101      (Average Length: 92.89 Splits: 0)
Lemmas       : 791219   (Deleted: 748661)
  Binary     : 11784    (Ratio:   1.49%)
  Ternary    : 4009     (Ratio:   0.51%)
  Conflict   : 791219   (Average Length:  622.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 791219   (Average:  9.67 Max: 1058 Sum: 7649071)
  Executed   : 791105   (Average:  9.66 Max: 1058 Sum: 7645317 Ratio:  99.95%)
  Bounded    : 114      (Average: 32.93 Max: 117 Sum:   3754 Ratio:   0.05%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 742606   (Eliminated:    0 Frozen: 233385)
Constraints  : 5506021  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

Iteration 101
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        : 102
Time         : 782.524s (Solving: 749.62s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 782.684s

Choices      : 9267875  (Domain: 9106764)
Conflicts    : 799718   (Analyzed: 799715)
Restarts     : 9743     (Average: 82.08 Last: 199)
Model-Level  : 148.0   
Problems     : 102      (Average Length: 93.13 Splits: 0)
Lemmas       : 799715   (Deleted: 755133)
  Binary     : 11797    (Ratio:   1.48%)
  Ternary    : 4017     (Ratio:   0.50%)
  Conflict   : 799715   (Average Length:  622.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 799715   (Average:  9.64 Max: 1058 Sum: 7706284)
  Executed   : 799601   (Average:  9.63 Max: 1058 Sum: 7702530 Ratio:  99.95%)
  Bounded    : 114      (Average: 32.93 Max: 117 Sum:   3754 Ratio:   0.05%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 742606   (Eliminated:    0 Frozen: 233385)
Constraints  : 5506021  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

Iteration 102
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        : 103
Time         : 790.891s (Solving: 757.83s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 791.056s

Choices      : 9353756  (Domain: 9192645)
Conflicts    : 808956   (Analyzed: 808953)
Restarts     : 9843     (Average: 82.19 Last: 199)
Model-Level  : 148.0   
Problems     : 103      (Average Length: 93.36 Splits: 0)
Lemmas       : 808953   (Deleted: 765640)
  Binary     : 11814    (Ratio:   1.46%)
  Ternary    : 4023     (Ratio:   0.50%)
  Conflict   : 808953   (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    : 808953   (Average:  9.60 Max: 1058 Sum: 7765927)
  Executed   : 808838   (Average:  9.60 Max: 1058 Sum: 7762056 Ratio:  99.95%)
  Bounded    : 115      (Average: 33.66 Max: 117 Sum:   3871 Ratio:   0.05%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 742606   (Eliminated:    0 Frozen: 233385)
Constraints  : 5506021  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 8.31s
Memory:		 857MB (+0MB)
UNKNOWN
Iteration Time:	 8.37s

Iteration 103
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        : 104
Time         : 799.335s (Solving: 766.11s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 799.504s

Choices      : 9435298  (Domain: 9274181)
Conflicts    : 816954   (Analyzed: 816951)
Restarts     : 9943     (Average: 82.16 Last: 199)
Model-Level  : 148.0   
Problems     : 104      (Average Length: 93.59 Splits: 0)
Lemmas       : 816951   (Deleted: 772601)
  Binary     : 11822    (Ratio:   1.45%)
  Ternary    : 4029     (Ratio:   0.49%)
  Conflict   : 816951   (Average Length:  624.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 816951   (Average:  9.58 Max: 1058 Sum: 7826602)
  Executed   : 816836   (Average:  9.58 Max: 1058 Sum: 7822731 Ratio:  99.95%)
  Bounded    : 115      (Average: 33.66 Max: 117 Sum:   3871 Ratio:   0.05%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 742606   (Eliminated:    0 Frozen: 233385)
Constraints  : 5506007  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

Iteration 104
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        : 105
Time         : 805.119s (Solving: 771.74s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 805.292s

Choices      : 9483454  (Domain: 9322337)
Conflicts    : 825009   (Analyzed: 825006)
Restarts     : 10043    (Average: 82.15 Last: 199)
Model-Level  : 148.0   
Problems     : 105      (Average Length: 93.81 Splits: 0)
Lemmas       : 825006   (Deleted: 780339)
  Binary     : 11871    (Ratio:   1.44%)
  Ternary    : 4039     (Ratio:   0.49%)
  Conflict   : 825006   (Average Length:  624.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 825006   (Average:  9.54 Max: 1058 Sum: 7868631)
  Executed   : 824891   (Average:  9.53 Max: 1058 Sum: 7864760 Ratio:  99.95%)
  Bounded    : 115      (Average: 33.66 Max: 117 Sum:   3871 Ratio:   0.05%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 742606   (Eliminated:    0 Frozen: 233385)
Constraints  : 5506007  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

Iteration 105
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        : 106
Time         : 816.483s (Solving: 782.95s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 816.660s

Choices      : 9536234  (Domain: 9375117)
Conflicts    : 834315   (Analyzed: 834312)
Restarts     : 10143    (Average: 82.25 Last: 199)
Model-Level  : 148.0   
Problems     : 106      (Average Length: 94.03 Splits: 0)
Lemmas       : 834312   (Deleted: 790395)
  Binary     : 11883    (Ratio:   1.42%)
  Ternary    : 4044     (Ratio:   0.48%)
  Conflict   : 834312   (Average Length:  632.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 834312   (Average:  9.48 Max: 1058 Sum: 7909082)
  Executed   : 834197   (Average:  9.48 Max: 1058 Sum: 7905211 Ratio:  99.95%)
  Bounded    : 115      (Average: 33.66 Max: 117 Sum:   3871 Ratio:   0.05%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 742606   (Eliminated:    0 Frozen: 233385)
Constraints  : 5506007  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

Iteration 106
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        : 107
Time         : 821.661s (Solving: 787.96s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 821.840s

Choices      : 9580412  (Domain: 9419295)
Conflicts    : 841863   (Analyzed: 841860)
Restarts     : 10243    (Average: 82.19 Last: 199)
Model-Level  : 148.0   
Problems     : 107      (Average Length: 94.24 Splits: 0)
Lemmas       : 841860   (Deleted: 797354)
  Binary     : 11902    (Ratio:   1.41%)
  Ternary    : 4048     (Ratio:   0.48%)
  Conflict   : 841860   (Average Length:  631.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 841860   (Average:  9.43 Max: 1058 Sum: 7941299)
  Executed   : 841745   (Average:  9.43 Max: 1058 Sum: 7937428 Ratio:  99.95%)
  Bounded    : 115      (Average: 33.66 Max: 117 Sum:   3871 Ratio:   0.05%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 742606   (Eliminated:    0 Frozen: 233385)
Constraints  : 5506007  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 5.12s
Memory:		 857MB (+0MB)
UNKNOWN
Iteration Time:	 5.18s

Iteration 107
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        : 108
Time         : 828.554s (Solving: 794.68s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 828.736s

Choices      : 9656002  (Domain: 9494786)
Conflicts    : 850202   (Analyzed: 850199)
Restarts     : 10343    (Average: 82.20 Last: 199)
Model-Level  : 148.0   
Problems     : 108      (Average Length: 94.45 Splits: 0)
Lemmas       : 850199   (Deleted: 804818)
  Binary     : 11959    (Ratio:   1.41%)
  Ternary    : 4063     (Ratio:   0.48%)
  Conflict   : 850199   (Average Length:  633.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 850199   (Average:  9.41 Max: 1058 Sum: 7998333)
  Executed   : 850084   (Average:  9.40 Max: 1058 Sum: 7994462 Ratio:  99.95%)
  Bounded    : 115      (Average: 33.66 Max: 117 Sum:   3871 Ratio:   0.05%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 742606   (Eliminated:    0 Frozen: 233385)
Constraints  : 5506007  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 6.83s
Memory:		 857MB (+0MB)
UNKNOWN
Iteration Time:	 6.90s

Iteration 108
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        : 109
Time         : 835.431s (Solving: 801.39s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 835.616s

Choices      : 9727918  (Domain: 9566701)
Conflicts    : 858819   (Analyzed: 858816)
Restarts     : 10443    (Average: 82.24 Last: 199)
Model-Level  : 148.0   
Problems     : 109      (Average Length: 94.66 Splits: 0)
Lemmas       : 858816   (Deleted: 815156)
  Binary     : 11975    (Ratio:   1.39%)
  Ternary    : 4064     (Ratio:   0.47%)
  Conflict   : 858816   (Average Length:  636.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 858816   (Average:  9.37 Max: 1058 Sum: 8050938)
  Executed   : 858701   (Average:  9.37 Max: 1058 Sum: 8047067 Ratio:  99.95%)
  Bounded    : 115      (Average: 33.66 Max: 117 Sum:   3871 Ratio:   0.05%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 742606   (Eliminated:    0 Frozen: 233385)
Constraints  : 5506007  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

Iteration 109
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        : 110
Time         : 842.347s (Solving: 808.12s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 842.532s

Choices      : 9797223  (Domain: 9636001)
Conflicts    : 867543   (Analyzed: 867540)
Restarts     : 10543    (Average: 82.29 Last: 199)
Model-Level  : 148.0   
Problems     : 110      (Average Length: 94.86 Splits: 0)
Lemmas       : 867540   (Deleted: 823646)
  Binary     : 11991    (Ratio:   1.38%)
  Ternary    : 4066     (Ratio:   0.47%)
  Conflict   : 867540   (Average Length:  638.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 867540   (Average:  9.34 Max: 1058 Sum: 8102047)
  Executed   : 867425   (Average:  9.33 Max: 1058 Sum: 8098176 Ratio:  99.95%)
  Bounded    : 115      (Average: 33.66 Max: 117 Sum:   3871 Ratio:   0.05%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 742606   (Eliminated:    0 Frozen: 233385)
Constraints  : 5506007  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

Iteration 110
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        : 111
Time         : 853.659s (Solving: 819.28s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 853.848s

Choices      : 9949967  (Domain: 9785794)
Conflicts    : 876581   (Analyzed: 876578)
Restarts     : 10643    (Average: 82.36 Last: 199)
Model-Level  : 148.0   
Problems     : 111      (Average Length: 95.06 Splits: 0)
Lemmas       : 876578   (Deleted: 832232)
  Binary     : 12158    (Ratio:   1.39%)
  Ternary    : 4113     (Ratio:   0.47%)
  Conflict   : 876578   (Average Length:  645.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 876578   (Average:  9.38 Max: 1058 Sum: 8225712)
  Executed   : 876463   (Average:  9.38 Max: 1058 Sum: 8221841 Ratio:  99.95%)
  Bounded    : 115      (Average: 33.66 Max: 117 Sum:   3871 Ratio:   0.05%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 742606   (Eliminated:    0 Frozen: 233385)
Constraints  : 5506007  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 11.27s
Memory:		 857MB (+0MB)
UNKNOWN
Iteration Time:	 11.32s

Iteration 111
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        : 112
Time         : 863.426s (Solving: 828.89s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 863.620s

Choices      : 10042502 (Domain: 9878317)
Conflicts    : 885738   (Analyzed: 885735)
Restarts     : 10743    (Average: 82.45 Last: 199)
Model-Level  : 148.0   
Problems     : 112      (Average Length: 95.26 Splits: 0)
Lemmas       : 885735   (Deleted: 840911)
  Binary     : 12184    (Ratio:   1.38%)
  Ternary    : 4119     (Ratio:   0.47%)
  Conflict   : 885735   (Average Length:  650.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 885735   (Average:  9.36 Max: 1058 Sum: 8289402)
  Executed   : 885620   (Average:  9.35 Max: 1058 Sum: 8285531 Ratio:  99.95%)
  Bounded    : 115      (Average: 33.66 Max: 117 Sum:   3871 Ratio:   0.05%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 742606   (Eliminated:    0 Frozen: 233385)
Constraints  : 5506007  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 113
Time         : 879.556s (Solving: 844.86s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 879.756s

Choices      : 10485047 (Domain: 10316374)
Conflicts    : 894880   (Analyzed: 894877)
Restarts     : 10843    (Average: 82.53 Last: 199)
Model-Level  : 148.0   
Problems     : 113      (Average Length: 95.45 Splits: 0)
Lemmas       : 894877   (Deleted: 848790)
  Binary     : 12604    (Ratio:   1.41%)
  Ternary    : 4199     (Ratio:   0.47%)
  Conflict   : 894877   (Average Length:  654.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 894877   (Average:  9.70 Max: 1105 Sum: 8684412)
  Executed   : 894762   (Average:  9.70 Max: 1105 Sum: 8680541 Ratio:  99.96%)
  Bounded    : 115      (Average: 33.66 Max: 117 Sum:   3871 Ratio:   0.04%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 742606   (Eliminated:    0 Frozen: 233385)
Constraints  : 5506007  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 16.08s
Memory:		 857MB (+0MB)
UNKNOWN
Iteration Time:	 16.14s

Iteration 113
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        : 114
Time         : 883.591s (Solving: 848.74s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 883.792s

Choices      : 10528161 (Domain: 10359488)
Conflicts    : 902448   (Analyzed: 902445)
Restarts     : 10943    (Average: 82.47 Last: 199)
Model-Level  : 148.0   
Problems     : 114      (Average Length: 95.64 Splits: 0)
Lemmas       : 902445   (Deleted: 855730)
  Binary     : 12665    (Ratio:   1.40%)
  Ternary    : 4206     (Ratio:   0.47%)
  Conflict   : 902445   (Average Length:  654.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 902445   (Average:  9.66 Max: 1105 Sum: 8721053)
  Executed   : 902330   (Average:  9.66 Max: 1105 Sum: 8717182 Ratio:  99.96%)
  Bounded    : 115      (Average: 33.66 Max: 117 Sum:   3871 Ratio:   0.04%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 742606   (Eliminated:    0 Frozen: 233385)
Constraints  : 5506007  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 3.98s
Memory:		 857MB (+0MB)
UNKNOWN
Iteration Time:	 4.04s

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

INTERRUPTED  : 1

Models       : 0+
Calls        : 115
Time         : 893.530s (Solving: 858.51s 1st Model: 0.00s Unsat: 2.29s)
CPU Time     : 893.716s

Choices      : 10567602 (Domain: 10398929)
Conflicts    : 909948   (Analyzed: 909945)
Restarts     : 11022    (Average: 82.56 Last: 199)
Model-Level  : 148.0   
Problems     : 115      (Average Length: 95.83 Splits: 0)
Lemmas       : 909945   (Deleted: 863605)
  Binary     : 12691    (Ratio:   1.39%)
  Ternary    : 4208     (Ratio:   0.46%)
  Conflict   : 909945   (Average Length:  661.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 909945   (Average:  9.61 Max: 1105 Sum: 8748557)
  Executed   : 909830   (Average:  9.61 Max: 1105 Sum: 8744686 Ratio:  99.96%)
  Bounded    : 115      (Average: 33.66 Max: 117 Sum:   3871 Ratio:   0.04%)

Rules        : 76935    (Original: 75225)
Atoms        : 61653   
Bodies       : 14003    (Original: 12292)
  Count      : 291      (Original: 633)
Equivalences : 3885     (Atom=Atom: 72 Body=Body: 0 Other: 3813)
Tight        : Yes
Variables    : 742606   (Eliminated:    0 Frozen: 233385)
Constraints  : 5506007  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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


