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-20.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-20.pddl
Parsing...
Parsing: [0.040s CPU, 0.043s wall-clock]
Normalizing task... [0.000s CPU, 0.003s wall-clock]
Instantiating...
Generating Datalog program... [0.010s CPU, 0.012s wall-clock]
Normalizing Datalog program...
Normalizing Datalog program: [0.050s CPU, 0.053s wall-clock]
Preparing model... [0.030s CPU, 0.030s wall-clock]
Generated 115 rules.
Computing model... [0.540s CPU, 0.544s wall-clock]
3296 relevant atoms
3425 auxiliary atoms
6721 final queue length
11595 total queue pushes
Completing instantiation... [1.030s CPU, 1.030s wall-clock]
Instantiating: [1.680s CPU, 1.676s wall-clock]
Computing fact groups...
Finding invariants...
24 initial candidates
Finding invariants: [0.140s CPU, 0.142s wall-clock]
Checking invariant weight... [0.000s CPU, 0.001s wall-clock]
Instantiating groups... [0.010s CPU, 0.010s wall-clock]
Collecting mutex groups... [0.000s CPU, 0.001s wall-clock]
Choosing groups...
350 uncovered facts
Choosing groups: [0.000s CPU, 0.002s wall-clock]
Building translation key... [0.010s CPU, 0.014s wall-clock]
Computing fact groups: [0.190s CPU, 0.197s wall-clock]
Building STRIPS to SAS dictionary... [0.010s CPU, 0.006s wall-clock]
Building dictionary for full mutex groups... [0.000s CPU, 0.003s wall-clock]
Building mutex information...
Building mutex information: [0.010s CPU, 0.004s wall-clock]
Translating task...
Processing axioms...
Simplifying axioms... [0.000s CPU, 0.000s wall-clock]
Processing axioms: [0.050s CPU, 0.056s wall-clock]
Translating task: [1.060s CPU, 1.070s wall-clock]
3920 effect conditions simplified
0 implied preconditions added
Detecting unreachable propositions...
0 operators removed
0 axioms removed
3 propositions removed
Detecting unreachable propositions: [0.590s CPU, 0.591s wall-clock]
Reordering and filtering variables...
353 of 353 variables necessary.
16 of 19 mutex groups necessary.
2344 of 2344 operators necessary.
0 of 0 axiom rules necessary.
Reordering and filtering variables: [0.380s CPU, 0.379s wall-clock]
Translator variables: 353
Translator derived variables: 0
Translator facts: 737
Translator goal facts: 14
Translator mutex groups: 16
Translator total mutex groups size: 48
Translator operators: 2344
Translator axioms: 0
Translator task size: 22454
Translator peak memory: 49100 KB
Writing output... [0.370s CPU, 0.407s wall-clock]
Done! [4.380s CPU, 4.422s wall-clock]
planner.py version 0.0.1

Time:	 0.92s
Memory: 111MB

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

Models       : 0
Calls        : 1
Time         : 1.109s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
CPU Time     : 0.924s

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

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

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

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

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

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

Choices      : 195      (Domain: 36)
Conflicts    : 4        (Analyzed: 4)
Restarts     : 0       
Model-Level  : 183.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:   16.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 4        (Average:  5.00 Max:  16 Sum:     20)
  Executed   : 3        (Average:  4.75 Max:  16 Sum:     19 Ratio:  95.00%)
  Bounded    : 1        (Average:  1.00 Max:   1 Sum:      1 Ratio:   5.00%)

Rules        : 64767   
Atoms        : 64767   
Bodies       : 1        (Original: 0)
Tight        : Yes
Variables    : 17354    (Eliminated:    0 Frozen:  170)
Constraints  : 57355    (Binary:  95.3% Ternary:   3.3% Other:   1.4%)

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

[endof: stats after solve call]
Solving Time:	 0.02s
Memory:		 187MB (+4MB)
SAT
Testing...
NOT SERIALIZABLE
Testing Time:	 1.00s
Memory:		 218MB (+31MB)
Solving...
[start: stats after solve call]

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

Choices      : 212      (Domain: 37)
Conflicts    : 13       (Analyzed: 12)
Restarts     : 0       
Model-Level  : 183.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.5 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.25 Max:  16 Sum:     39)
  Executed   : 9        (Average:  3.00 Max:  16 Sum:     36 Ratio:  92.31%)
  Bounded    : 3        (Average:  1.00 Max:   1 Sum:      3 Ratio:   7.69%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 21236    (Eliminated:    0 Frozen: 4444)
Constraints  : 86170    (Binary:  92.4% Ternary:   5.4% Other:   2.2%)

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

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

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

Models       : 0
Calls        : 4
Time         : 3.582s (Solving: 1.11s 1st Model: 0.00s Unsat: 1.11s)
CPU Time     : 3.408s

Choices      : 36338    (Domain: 29490)
Conflicts    : 3123     (Analyzed: 3121)
Restarts     : 36       (Average: 86.69 Last: 26)
Model-Level  : 183.0   
Problems     : 4        (Average Length: 7.00 Splits: 0)
Lemmas       : 3121     (Deleted: 570)
  Binary     : 325      (Ratio:  10.41%)
  Ternary    : 504      (Ratio:  16.15%)
  Conflict   : 3121     (Average Length:   42.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 3121     (Average: 11.58 Max: 265 Sum:  36155)
  Executed   : 3080     (Average: 11.44 Max: 265 Sum:  35707 Ratio:  98.76%)
  Bounded    : 41       (Average: 10.93 Max:  12 Sum:    448 Ratio:   1.24%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 61312    (Eliminated:    0 Frozen: 16894)
Constraints  : 388150   (Binary:  91.5% Ternary:   6.7% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 1.14s
Memory:		 230MB (+12MB)
UNSAT
Iteration Time:	 1.89s

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

Models       : 0+
Calls        : 5
Time         : 8.918s (Solving: 5.65s 1st Model: 0.00s Unsat: 1.11s)
CPU Time     : 8.748s

Choices      : 115133   (Domain: 89050)
Conflicts    : 12082    (Analyzed: 12080)
Restarts     : 136      (Average: 88.82 Last: 101)
Model-Level  : 183.0   
Problems     : 5        (Average Length: 9.00 Splits: 0)
Lemmas       : 12080    (Deleted: 7160)
  Binary     : 775      (Ratio:   6.42%)
  Ternary    : 845      (Ratio:   7.00%)
  Conflict   : 12080    (Average Length:  130.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 12080    (Average:  9.19 Max: 265 Sum: 110997)
  Executed   : 12022    (Average:  9.13 Max: 265 Sum: 110262 Ratio:  99.34%)
  Bounded    : 58       (Average: 12.67 Max:  17 Sum:    735 Ratio:   0.66%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 101388   (Eliminated:    0 Frozen: 29344)
Constraints  : 645808   (Binary:  91.4% Ternary:   6.7% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 4.58s
Memory:		 262MB (+20MB)
UNKNOWN
Iteration Time:	 5.35s

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

Models       : 0+
Calls        : 6
Time         : 14.138s (Solving: 9.94s 1st Model: 0.00s Unsat: 1.11s)
CPU Time     : 13.968s

Choices      : 157868   (Domain: 131138)
Conflicts    : 19485    (Analyzed: 19483)
Restarts     : 236      (Average: 82.56 Last: 101)
Model-Level  : 183.0   
Problems     : 6        (Average Length: 11.17 Splits: 0)
Lemmas       : 19483    (Deleted: 13053)
  Binary     : 1076     (Ratio:   5.52%)
  Ternary    : 912      (Ratio:   4.68%)
  Conflict   : 19483    (Average Length:  181.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 19483    (Average:  7.64 Max: 265 Sum: 148779)
  Executed   : 19423    (Average:  7.60 Max: 265 Sum: 148003 Ratio:  99.48%)
  Bounded    : 60       (Average: 12.93 Max:  22 Sum:    776 Ratio:   0.52%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 141464   (Eliminated:    0 Frozen: 41794)
Constraints  : 941310   (Binary:  91.3% Ternary:   6.8% Other:   1.9%)

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

[endof: stats after solve call]
Solving Time:	 4.33s
Memory:		 302MB (+26MB)
UNKNOWN
Iteration Time:	 5.23s

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

Models       : 0+
Calls        : 7
Time         : 20.394s (Solving: 15.35s 1st Model: 0.00s Unsat: 1.11s)
CPU Time     : 20.224s

Choices      : 331212   (Domain: 285212)
Conflicts    : 28062    (Analyzed: 28060)
Restarts     : 336      (Average: 83.51 Last: 131)
Model-Level  : 183.0   
Problems     : 7        (Average Length: 13.43 Splits: 0)
Lemmas       : 28060    (Deleted: 18557)
  Binary     : 1903     (Ratio:   6.78%)
  Ternary    : 1288     (Ratio:   4.59%)
  Conflict   : 28060    (Average Length:  175.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 28060    (Average: 11.25 Max: 782 Sum: 315796)
  Executed   : 27986    (Average: 11.21 Max: 782 Sum: 314642 Ratio:  99.63%)
  Bounded    : 74       (Average: 15.59 Max:  27 Sum:   1154 Ratio:   0.37%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 181540   (Eliminated:    0 Frozen: 54244)
Constraints  : 1240231  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 5.47s
Memory:		 322MB (+14MB)
UNKNOWN
Iteration Time:	 6.27s

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

Models       : 0+
Calls        : 8
Time         : 27.275s (Solving: 21.30s 1st Model: 0.00s Unsat: 1.11s)
CPU Time     : 27.108s

Choices      : 464738   (Domain: 402252)
Conflicts    : 36744    (Analyzed: 36742)
Restarts     : 436      (Average: 84.27 Last: 131)
Model-Level  : 183.0   
Problems     : 8        (Average Length: 15.75 Splits: 0)
Lemmas       : 36742    (Deleted: 27143)
  Binary     : 2231     (Ratio:   6.07%)
  Ternary    : 1421     (Ratio:   3.87%)
  Conflict   : 36742    (Average Length:  201.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 36742    (Average: 11.94 Max: 782 Sum: 438868)
  Executed   : 36653    (Average: 11.90 Max: 782 Sum: 437244 Ratio:  99.63%)
  Bounded    : 89       (Average: 18.25 Max:  32 Sum:   1624 Ratio:   0.37%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 221616   (Eliminated:    0 Frozen: 66694)
Constraints  : 1520780  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 6.02s
Memory:		 368MB (+34MB)
UNKNOWN
Iteration Time:	 6.89s

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         : 28.615s (Solving: 22.59s 1st Model: 0.00s Unsat: 2.40s)
CPU Time     : 28.448s

Choices      : 467550   (Domain: 405060)
Conflicts    : 37906    (Analyzed: 37903)
Restarts     : 450      (Average: 84.23 Last: 131)
Model-Level  : 183.0   
Problems     : 9        (Average Length: 17.56 Splits: 0)
Lemmas       : 37903    (Deleted: 27143)
  Binary     : 2261     (Ratio:   5.97%)
  Ternary    : 1439     (Ratio:   3.80%)
  Conflict   : 37903    (Average Length:  202.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 37903    (Average: 11.65 Max: 782 Sum: 441640)
  Executed   : 37813    (Average: 11.61 Max: 782 Sum: 440015 Ratio:  99.63%)
  Bounded    : 90       (Average: 18.06 Max:  32 Sum:   1625 Ratio:   0.37%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 221616   (Eliminated:    0 Frozen: 66694)
Constraints  : 1503174  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 1.32s
Memory:		 368MB (+0MB)
UNSAT
Iteration Time:	 1.34s

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         : 34.297s (Solving: 28.21s 1st Model: 0.00s Unsat: 2.40s)
CPU Time     : 34.132s

Choices      : 529904   (Domain: 452412)
Conflicts    : 46631    (Analyzed: 46628)
Restarts     : 550      (Average: 84.78 Last: 131)
Model-Level  : 183.0   
Problems     : 10       (Average Length: 19.00 Splits: 0)
Lemmas       : 46628    (Deleted: 36484)
  Binary     : 2472     (Ratio:   5.30%)
  Ternary    : 1508     (Ratio:   3.23%)
  Conflict   : 46628    (Average Length:  244.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 46628    (Average: 10.67 Max: 782 Sum: 497348)
  Executed   : 46537    (Average: 10.63 Max: 782 Sum: 495696 Ratio:  99.67%)
  Bounded    : 91       (Average: 18.15 Max:  32 Sum:   1652 Ratio:   0.33%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 221616   (Eliminated:    0 Frozen: 66694)
Constraints  : 1503174  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

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

Models       : 0+
Calls        : 11
Time         : 41.774s (Solving: 35.64s 1st Model: 0.00s Unsat: 2.40s)
CPU Time     : 41.612s

Choices      : 633897   (Domain: 541048)
Conflicts    : 55908    (Analyzed: 55905)
Restarts     : 650      (Average: 86.01 Last: 131)
Model-Level  : 183.0   
Problems     : 11       (Average Length: 20.18 Splits: 0)
Lemmas       : 55905    (Deleted: 42997)
  Binary     : 3035     (Ratio:   5.43%)
  Ternary    : 1728     (Ratio:   3.09%)
  Conflict   : 55905    (Average Length:  289.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 55905    (Average: 10.58 Max: 782 Sum: 591368)
  Executed   : 55806    (Average: 10.54 Max: 782 Sum: 589465 Ratio:  99.68%)
  Bounded    : 99       (Average: 19.22 Max:  32 Sum:   1903 Ratio:   0.32%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 221616   (Eliminated:    0 Frozen: 66694)
Constraints  : 1503174  (Binary:  91.3% Ternary:   6.8% Other:   1.8%)

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

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

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.815s (Solving: 43.63s 1st Model: 0.00s Unsat: 2.40s)
CPU Time     : 49.656s

Choices      : 743498   (Domain: 635142)
Conflicts    : 65194    (Analyzed: 65191)
Restarts     : 750      (Average: 86.92 Last: 131)
Model-Level  : 183.0   
Problems     : 12       (Average Length: 21.17 Splits: 0)
Lemmas       : 65191    (Deleted: 51200)
  Binary     : 3305     (Ratio:   5.07%)
  Ternary    : 1857     (Ratio:   2.85%)
  Conflict   : 65191    (Average Length:  330.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 65191    (Average: 10.52 Max: 782 Sum: 685498)
  Executed   : 65090    (Average: 10.49 Max: 782 Sum: 683531 Ratio:  99.71%)
  Bounded    : 101      (Average: 19.48 Max:  32 Sum:   1967 Ratio:   0.29%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 221616   (Eliminated:    0 Frozen: 66694)
Constraints  : 1497569  (Binary:  91.3% Ternary:   6.8% Other:   1.9%)

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

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

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: 414.0MB
Grounding...	 [('step', [31]), ('step', [32]), ('step', [33]), ('step', [34]), ('step', [35]), ('check', [35])]
Grounding Time:	 0.56s
Memory:		 368MB (+0MB)
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 13
Time         : 59.310s (Solving: 52.21s 1st Model: 0.00s Unsat: 2.40s)
CPU Time     : 59.156s

Choices      : 881351   (Domain: 756871)
Conflicts    : 74031    (Analyzed: 74028)
Restarts     : 850      (Average: 87.09 Last: 157)
Model-Level  : 183.0   
Problems     : 13       (Average Length: 22.38 Splits: 0)
Lemmas       : 74028    (Deleted: 59920)
  Binary     : 3488     (Ratio:   4.71%)
  Ternary    : 1914     (Ratio:   2.59%)
  Conflict   : 74028    (Average Length:  407.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 74028    (Average: 10.85 Max: 782 Sum: 803239)
  Executed   : 73919    (Average: 10.82 Max: 782 Sum: 800976 Ratio:  99.72%)
  Bounded    : 109      (Average: 20.76 Max:  37 Sum:   2263 Ratio:   0.28%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 261692   (Eliminated:    0 Frozen: 79144)
Constraints  : 1799341  (Binary:  91.3% Ternary:   6.9% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 8.65s
Memory:		 381MB (+13MB)
UNKNOWN
Iteration Time:	 9.51s

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: 427.0MB
Grounding...	 [('step', [36]), ('step', [37]), ('step', [38]), ('step', [39]), ('step', [40]), ('check', [40])]
Grounding Time:	 0.57s
Memory:		 392MB (+11MB)
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 14
Time         : 68.733s (Solving: 60.68s 1st Model: 0.00s Unsat: 2.40s)
CPU Time     : 68.584s

Choices      : 1039739  (Domain: 899452)
Conflicts    : 82621    (Analyzed: 82618)
Restarts     : 950      (Average: 86.97 Last: 157)
Model-Level  : 183.0   
Problems     : 14       (Average Length: 23.79 Splits: 0)
Lemmas       : 82618    (Deleted: 66758)
  Binary     : 3639     (Ratio:   4.40%)
  Ternary    : 1978     (Ratio:   2.39%)
  Conflict   : 82618    (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    : 82618    (Average: 11.38 Max: 782 Sum: 940232)
  Executed   : 82507    (Average: 11.35 Max: 782 Sum: 937886 Ratio:  99.75%)
  Bounded    : 111      (Average: 21.14 Max:  42 Sum:   2346 Ratio:   0.25%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 301768   (Eliminated:    0 Frozen: 91594)
Constraints  : 2101210  (Binary:  91.3% Ternary:   6.9% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 8.55s
Memory:		 407MB (+15MB)
UNKNOWN
Iteration Time:	 9.44s

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: 453.0MB
Grounding...	 [('step', [41]), ('step', [42]), ('step', [43]), ('step', [44]), ('step', [45]), ('check', [45])]
Grounding Time:	 0.72s
Memory:		 431MB (+24MB)
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 15
Time         : 79.407s (Solving: 70.22s 1st Model: 0.00s Unsat: 2.40s)
CPU Time     : 79.264s

Choices      : 1223417  (Domain: 1070592)
Conflicts    : 91188    (Analyzed: 91185)
Restarts     : 1050     (Average: 86.84 Last: 157)
Model-Level  : 183.0   
Problems     : 15       (Average Length: 25.33 Splits: 0)
Lemmas       : 91185    (Deleted: 74522)
  Binary     : 3852     (Ratio:   4.22%)
  Ternary    : 2045     (Ratio:   2.24%)
  Conflict   : 91185    (Average Length:  444.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 91185    (Average: 12.09 Max: 794 Sum: 1102182)
  Executed   : 91068    (Average: 12.06 Max: 794 Sum: 1099554 Ratio:  99.76%)
  Bounded    : 117      (Average: 22.46 Max:  47 Sum:   2628 Ratio:   0.24%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 341844   (Eliminated:    0 Frozen: 104044)
Constraints  : 2403164  (Binary:  91.3% Ternary:   6.9% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 9.63s
Memory:		 481MB (+50MB)
UNKNOWN
Iteration Time:	 10.69s

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

Models       : 0+
Calls        : 16
Time         : 90.472s (Solving: 80.24s 1st Model: 0.00s Unsat: 2.40s)
CPU Time     : 90.336s

Choices      : 1429024  (Domain: 1264883)
Conflicts    : 100027   (Analyzed: 100024)
Restarts     : 1150     (Average: 86.98 Last: 157)
Model-Level  : 183.0   
Problems     : 16       (Average Length: 27.00 Splits: 0)
Lemmas       : 100024   (Deleted: 84018)
  Binary     : 3987     (Ratio:   3.99%)
  Ternary    : 2087     (Ratio:   2.09%)
  Conflict   : 100024   (Average Length:  472.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 100024   (Average: 12.81 Max: 794 Sum: 1281367)
  Executed   : 99905    (Average: 12.78 Max: 794 Sum: 1278640 Ratio:  99.79%)
  Bounded    : 119      (Average: 22.92 Max:  52 Sum:   2727 Ratio:   0.21%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 381920   (Eliminated:    0 Frozen: 116494)
Constraints  : 2702017  (Binary:  91.3% Ternary:   6.9% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 10.12s
Memory:		 490MB (+9MB)
UNKNOWN
Iteration Time:	 11.08s

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

Models       : 0+
Calls        : 17
Time         : 100.209s (Solving: 88.95s 1st Model: 0.00s Unsat: 2.40s)
CPU Time     : 100.076s

Choices      : 1577246  (Domain: 1405775)
Conflicts    : 108978   (Analyzed: 108975)
Restarts     : 1250     (Average: 87.18 Last: 157)
Model-Level  : 183.0   
Problems     : 17       (Average Length: 28.76 Splits: 0)
Lemmas       : 108975   (Deleted: 93155)
  Binary     : 4109     (Ratio:   3.77%)
  Ternary    : 2118     (Ratio:   1.94%)
  Conflict   : 108975   (Average Length:  513.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 108975   (Average: 12.71 Max: 794 Sum: 1384883)
  Executed   : 108856   (Average: 12.68 Max: 794 Sum: 1382156 Ratio:  99.80%)
  Bounded    : 119      (Average: 22.92 Max:  52 Sum:   2727 Ratio:   0.20%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 421996   (Eliminated:    0 Frozen: 128944)
Constraints  : 3003983  (Binary:  91.3% Ternary:   6.9% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 8.80s
Memory:		 513MB (+20MB)
UNKNOWN
Iteration Time:	 9.75s

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

Models       : 0+
Calls        : 18
Time         : 110.217s (Solving: 97.92s 1st Model: 0.00s Unsat: 2.40s)
CPU Time     : 110.088s

Choices      : 1776257  (Domain: 1595430)
Conflicts    : 117090   (Analyzed: 117087)
Restarts     : 1350     (Average: 86.73 Last: 157)
Model-Level  : 183.0   
Problems     : 18       (Average Length: 30.61 Splits: 0)
Lemmas       : 117087   (Deleted: 99028)
  Binary     : 4216     (Ratio:   3.60%)
  Ternary    : 2159     (Ratio:   1.84%)
  Conflict   : 117087   (Average Length:  523.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 117087   (Average: 13.30 Max: 910 Sum: 1557696)
  Executed   : 116968   (Average: 13.28 Max: 910 Sum: 1554969 Ratio:  99.82%)
  Bounded    : 119      (Average: 22.92 Max:  52 Sum:   2727 Ratio:   0.18%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 462072   (Eliminated:    0 Frozen: 141394)
Constraints  : 3305963  (Binary:  91.2% Ternary:   6.9% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 9.07s
Memory:		 542MB (+24MB)
UNKNOWN
Iteration Time:	 10.02s

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

Models       : 0+
Calls        : 19
Time         : 120.307s (Solving: 106.94s 1st Model: 0.00s Unsat: 2.40s)
CPU Time     : 120.184s

Choices      : 1952515  (Domain: 1767971)
Conflicts    : 125373   (Analyzed: 125370)
Restarts     : 1450     (Average: 86.46 Last: 157)
Model-Level  : 183.0   
Problems     : 19       (Average Length: 32.53 Splits: 0)
Lemmas       : 125370   (Deleted: 107415)
  Binary     : 4297     (Ratio:   3.43%)
  Ternary    : 2186     (Ratio:   1.74%)
  Conflict   : 125370   (Average Length:  544.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 125370   (Average: 13.53 Max: 910 Sum: 1696732)
  Executed   : 125248   (Average: 13.51 Max: 910 Sum: 1693804 Ratio:  99.83%)
  Bounded    : 122      (Average: 24.00 Max:  67 Sum:   2928 Ratio:   0.17%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 502148   (Eliminated:    0 Frozen: 153844)
Constraints  : 3607943  (Binary:  91.2% Ternary:   6.9% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 9.13s
Memory:		 610MB (+61MB)
UNKNOWN
Iteration Time:	 10.11s

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

Models       : 0+
Calls        : 20
Time         : 130.946s (Solving: 116.50s 1st Model: 0.00s Unsat: 2.40s)
CPU Time     : 130.828s

Choices      : 2197548  (Domain: 2008753)
Conflicts    : 133633   (Analyzed: 133630)
Restarts     : 1550     (Average: 86.21 Last: 157)
Model-Level  : 183.0   
Problems     : 20       (Average Length: 34.50 Splits: 0)
Lemmas       : 133630   (Deleted: 114772)
  Binary     : 4403     (Ratio:   3.29%)
  Ternary    : 2221     (Ratio:   1.66%)
  Conflict   : 133630   (Average Length:  539.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 133630   (Average: 14.40 Max: 910 Sum: 1924414)
  Executed   : 133505   (Average: 14.38 Max: 910 Sum: 1921270 Ratio:  99.84%)
  Bounded    : 125      (Average: 25.15 Max:  72 Sum:   3144 Ratio:   0.16%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 542224   (Eliminated:    0 Frozen: 166294)
Constraints  : 3909881  (Binary:  91.2% Ternary:   6.9% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 9.67s
Memory:		 615MB (+5MB)
UNKNOWN
Iteration Time:	 10.66s

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

Models       : 0+
Calls        : 21
Time         : 143.234s (Solving: 127.68s 1st Model: 0.00s Unsat: 2.40s)
CPU Time     : 143.120s

Choices      : 2401935  (Domain: 2211433)
Conflicts    : 141844   (Analyzed: 141841)
Restarts     : 1650     (Average: 85.96 Last: 157)
Model-Level  : 183.0   
Problems     : 21       (Average Length: 36.52 Splits: 0)
Lemmas       : 141841   (Deleted: 122531)
  Binary     : 4527     (Ratio:   3.19%)
  Ternary    : 2257     (Ratio:   1.59%)
  Conflict   : 141841   (Average Length:  531.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 141841   (Average: 14.90 Max: 910 Sum: 2113516)
  Executed   : 141713   (Average: 14.88 Max: 910 Sum: 2110141 Ratio:  99.84%)
  Bounded    : 128      (Average: 26.37 Max:  77 Sum:   3375 Ratio:   0.16%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 582300   (Eliminated:    0 Frozen: 178744)
Constraints  : 4211821  (Binary:  91.2% Ternary:   6.9% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 11.29s
Memory:		 643MB (+27MB)
UNKNOWN
Iteration Time:	 12.30s

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

Models       : 0+
Calls        : 22
Time         : 153.637s (Solving: 136.96s 1st Model: 0.00s Unsat: 2.40s)
CPU Time     : 153.528s

Choices      : 2605196  (Domain: 2410332)
Conflicts    : 150017   (Analyzed: 150014)
Restarts     : 1750     (Average: 85.72 Last: 157)
Model-Level  : 183.0   
Problems     : 22       (Average Length: 38.59 Splits: 0)
Lemmas       : 150014   (Deleted: 130452)
  Binary     : 4621     (Ratio:   3.08%)
  Ternary    : 2282     (Ratio:   1.52%)
  Conflict   : 150014   (Average Length:  525.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 150014   (Average: 15.26 Max: 1010 Sum: 2289293)
  Executed   : 149883   (Average: 15.24 Max: 1010 Sum: 2285672 Ratio:  99.84%)
  Bounded    : 131      (Average: 27.64 Max:  82 Sum:   3621 Ratio:   0.16%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 622376   (Eliminated:    0 Frozen: 191194)
Constraints  : 4513760  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 9.41s
Memory:		 668MB (+25MB)
UNKNOWN
Iteration Time:	 10.42s

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         : 162.246s (Solving: 145.43s 1st Model: 0.00s Unsat: 2.40s)
CPU Time     : 162.144s

Choices      : 2670865  (Domain: 2470369)
Conflicts    : 158594   (Analyzed: 158591)
Restarts     : 1850     (Average: 85.72 Last: 157)
Model-Level  : 183.0   
Problems     : 23       (Average Length: 40.48 Splits: 0)
Lemmas       : 158591   (Deleted: 138588)
  Binary     : 4772     (Ratio:   3.01%)
  Ternary    : 2342     (Ratio:   1.48%)
  Conflict   : 158591   (Average Length:  525.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 158591   (Average: 14.81 Max: 1010 Sum: 2348653)
  Executed   : 158458   (Average: 14.79 Max: 1010 Sum: 2344949 Ratio:  99.84%)
  Bounded    : 133      (Average: 27.85 Max:  82 Sum:   3704 Ratio:   0.16%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 622376   (Eliminated:    0 Frozen: 191194)
Constraints  : 4513718  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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         : 169.973s (Solving: 153.03s 1st Model: 0.00s Unsat: 2.40s)
CPU Time     : 169.876s

Choices      : 2743021  (Domain: 2537527)
Conflicts    : 167336   (Analyzed: 167333)
Restarts     : 1950     (Average: 85.81 Last: 157)
Model-Level  : 183.0   
Problems     : 24       (Average Length: 42.21 Splits: 0)
Lemmas       : 167333   (Deleted: 148243)
  Binary     : 4901     (Ratio:   2.93%)
  Ternary    : 2416     (Ratio:   1.44%)
  Conflict   : 167333   (Average Length:  533.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 167333   (Average: 14.39 Max: 1010 Sum: 2407912)
  Executed   : 167200   (Average: 14.37 Max: 1010 Sum: 2404208 Ratio:  99.85%)
  Bounded    : 133      (Average: 27.85 Max:  82 Sum:   3704 Ratio:   0.15%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 622376   (Eliminated:    0 Frozen: 191194)
Constraints  : 4513705  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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         : 176.838s (Solving: 159.75s 1st Model: 0.00s Unsat: 2.40s)
CPU Time     : 176.748s

Choices      : 2793194  (Domain: 2586360)
Conflicts    : 175654   (Analyzed: 175651)
Restarts     : 2050     (Average: 85.68 Last: 157)
Model-Level  : 183.0   
Problems     : 25       (Average Length: 43.80 Splits: 0)
Lemmas       : 175651   (Deleted: 154469)
  Binary     : 4994     (Ratio:   2.84%)
  Ternary    : 2449     (Ratio:   1.39%)
  Conflict   : 175651   (Average Length:  523.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 175651   (Average: 13.95 Max: 1010 Sum: 2449845)
  Executed   : 175518   (Average: 13.93 Max: 1010 Sum: 2446141 Ratio:  99.85%)
  Bounded    : 133      (Average: 27.85 Max:  82 Sum:   3704 Ratio:   0.15%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 622376   (Eliminated:    0 Frozen: 191194)
Constraints  : 4513705  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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         : 184.556s (Solving: 167.33s 1st Model: 0.00s Unsat: 2.40s)
CPU Time     : 184.468s

Choices      : 2881735  (Domain: 2673125)
Conflicts    : 183975   (Analyzed: 183972)
Restarts     : 2150     (Average: 85.57 Last: 157)
Model-Level  : 183.0   
Problems     : 26       (Average Length: 45.27 Splits: 0)
Lemmas       : 183972   (Deleted: 162565)
  Binary     : 5040     (Ratio:   2.74%)
  Ternary    : 2464     (Ratio:   1.34%)
  Conflict   : 183972   (Average Length:  518.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 183972   (Average: 13.72 Max: 1010 Sum: 2524861)
  Executed   : 183837   (Average: 13.70 Max: 1010 Sum: 2520998 Ratio:  99.85%)
  Bounded    : 135      (Average: 28.61 Max:  82 Sum:   3863 Ratio:   0.15%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 622376   (Eliminated:    0 Frozen: 191194)
Constraints  : 4513705  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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         : 192.272s (Solving: 174.90s 1st Model: 0.00s Unsat: 2.40s)
CPU Time     : 192.188s

Choices      : 2993870  (Domain: 2779772)
Conflicts    : 192077   (Analyzed: 192074)
Restarts     : 2250     (Average: 85.37 Last: 157)
Model-Level  : 183.0   
Problems     : 27       (Average Length: 46.63 Splits: 0)
Lemmas       : 192074   (Deleted: 170725)
  Binary     : 5110     (Ratio:   2.66%)
  Ternary    : 2477     (Ratio:   1.29%)
  Conflict   : 192074   (Average Length:  519.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 192074   (Average: 13.64 Max: 1010 Sum: 2620085)
  Executed   : 191939   (Average: 13.62 Max: 1010 Sum: 2616222 Ratio:  99.85%)
  Bounded    : 135      (Average: 28.61 Max:  82 Sum:   3863 Ratio:   0.15%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 622376   (Eliminated:    0 Frozen: 191194)
Constraints  : 4513691  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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         : 204.351s (Solving: 186.86s 1st Model: 0.00s Unsat: 2.40s)
CPU Time     : 204.272s

Choices      : 3317666  (Domain: 3078914)
Conflicts    : 201174   (Analyzed: 201171)
Restarts     : 2350     (Average: 85.60 Last: 157)
Model-Level  : 183.0   
Problems     : 28       (Average Length: 47.89 Splits: 0)
Lemmas       : 201171   (Deleted: 180087)
  Binary     : 5501     (Ratio:   2.73%)
  Ternary    : 2562     (Ratio:   1.27%)
  Conflict   : 201171   (Average Length:  536.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 201171   (Average: 14.49 Max: 1010 Sum: 2915539)
  Executed   : 201036   (Average: 14.47 Max: 1010 Sum: 2911676 Ratio:  99.87%)
  Bounded    : 135      (Average: 28.61 Max:  82 Sum:   3863 Ratio:   0.13%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 622376   (Eliminated:    0 Frozen: 191194)
Constraints  : 4513691  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 12.04s
Memory:		 668MB (+0MB)
UNKNOWN
Iteration Time:	 12.09s

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         : 211.665s (Solving: 194.04s 1st Model: 0.00s Unsat: 2.40s)
CPU Time     : 211.588s

Choices      : 3439190  (Domain: 3199143)
Conflicts    : 208925   (Analyzed: 208922)
Restarts     : 2450     (Average: 85.27 Last: 157)
Model-Level  : 183.0   
Problems     : 29       (Average Length: 49.07 Splits: 0)
Lemmas       : 208922   (Deleted: 186770)
  Binary     : 5579     (Ratio:   2.67%)
  Ternary    : 2572     (Ratio:   1.23%)
  Conflict   : 208922   (Average Length:  528.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 208922   (Average: 14.47 Max: 1010 Sum: 3023317)
  Executed   : 208787   (Average: 14.45 Max: 1010 Sum: 3019454 Ratio:  99.87%)
  Bounded    : 135      (Average: 28.61 Max:  82 Sum:   3863 Ratio:   0.13%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 622376   (Eliminated:    0 Frozen: 191194)
Constraints  : 4513691  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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         : 217.857s (Solving: 200.09s 1st Model: 0.00s Unsat: 2.40s)
CPU Time     : 217.784s

Choices      : 3520051  (Domain: 3279560)
Conflicts    : 216107   (Analyzed: 216104)
Restarts     : 2550     (Average: 84.75 Last: 157)
Model-Level  : 183.0   
Problems     : 30       (Average Length: 50.17 Splits: 0)
Lemmas       : 216104   (Deleted: 194246)
  Binary     : 5641     (Ratio:   2.61%)
  Ternary    : 2593     (Ratio:   1.20%)
  Conflict   : 216104   (Average Length:  523.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 216104   (Average: 14.31 Max: 1010 Sum: 3091425)
  Executed   : 215969   (Average: 14.29 Max: 1010 Sum: 3087562 Ratio:  99.88%)
  Bounded    : 135      (Average: 28.61 Max:  82 Sum:   3863 Ratio:   0.12%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 622376   (Eliminated:    0 Frozen: 191194)
Constraints  : 4513691  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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         : 224.621s (Solving: 206.70s 1st Model: 0.00s Unsat: 2.40s)
CPU Time     : 224.548s

Choices      : 3585219  (Domain: 3344599)
Conflicts    : 224007   (Analyzed: 224004)
Restarts     : 2650     (Average: 84.53 Last: 157)
Model-Level  : 183.0   
Problems     : 31       (Average Length: 51.19 Splits: 0)
Lemmas       : 224004   (Deleted: 201238)
  Binary     : 5663     (Ratio:   2.53%)
  Ternary    : 2601     (Ratio:   1.16%)
  Conflict   : 224004   (Average Length:  515.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 224004   (Average: 14.05 Max: 1010 Sum: 3146534)
  Executed   : 223868   (Average: 14.03 Max: 1010 Sum: 3142594 Ratio:  99.87%)
  Bounded    : 136      (Average: 28.97 Max:  82 Sum:   3940 Ratio:   0.13%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 622376   (Eliminated:    0 Frozen: 191194)
Constraints  : 4513691  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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         : 233.395s (Solving: 215.32s 1st Model: 0.00s Unsat: 2.40s)
CPU Time     : 233.328s

Choices      : 3731353  (Domain: 3489030)
Conflicts    : 232313   (Analyzed: 232310)
Restarts     : 2750     (Average: 84.48 Last: 157)
Model-Level  : 183.0   
Problems     : 32       (Average Length: 52.16 Splits: 0)
Lemmas       : 232310   (Deleted: 208952)
  Binary     : 5741     (Ratio:   2.47%)
  Ternary    : 2619     (Ratio:   1.13%)
  Conflict   : 232310   (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    : 232310   (Average: 14.11 Max: 1010 Sum: 3277720)
  Executed   : 232173   (Average: 14.09 Max: 1010 Sum: 3273698 Ratio:  99.88%)
  Bounded    : 137      (Average: 29.36 Max:  82 Sum:   4022 Ratio:   0.12%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 622376   (Eliminated:    0 Frozen: 191194)
Constraints  : 4513691  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 8.72s
Memory:		 668MB (+0MB)
UNKNOWN
Iteration Time:	 8.78s

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         : 243.720s (Solving: 225.52s 1st Model: 0.00s Unsat: 2.40s)
CPU Time     : 243.660s

Choices      : 3939332  (Domain: 3695182)
Conflicts    : 240640   (Analyzed: 240637)
Restarts     : 2850     (Average: 84.43 Last: 157)
Model-Level  : 183.0   
Problems     : 33       (Average Length: 53.06 Splits: 0)
Lemmas       : 240637   (Deleted: 216962)
  Binary     : 5848     (Ratio:   2.43%)
  Ternary    : 2635     (Ratio:   1.10%)
  Conflict   : 240637   (Average Length:  505.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 240637   (Average: 14.41 Max: 1010 Sum: 3468650)
  Executed   : 240499   (Average: 14.40 Max: 1010 Sum: 3464546 Ratio:  99.88%)
  Bounded    : 138      (Average: 29.74 Max:  82 Sum:   4104 Ratio:   0.12%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 622376   (Eliminated:    0 Frozen: 191194)
Constraints  : 4513693  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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         : 252.404s (Solving: 234.05s 1st Model: 0.00s Unsat: 2.40s)
CPU Time     : 252.348s

Choices      : 4104662  (Domain: 3859160)
Conflicts    : 248722   (Analyzed: 248719)
Restarts     : 2950     (Average: 84.31 Last: 157)
Model-Level  : 183.0   
Problems     : 34       (Average Length: 53.91 Splits: 0)
Lemmas       : 248719   (Deleted: 224964)
  Binary     : 5921     (Ratio:   2.38%)
  Ternary    : 2653     (Ratio:   1.07%)
  Conflict   : 248719   (Average Length:  500.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 248719   (Average: 14.54 Max: 1044 Sum: 3617011)
  Executed   : 248579   (Average: 14.53 Max: 1044 Sum: 3612747 Ratio:  99.88%)
  Bounded    : 140      (Average: 30.46 Max:  82 Sum:   4264 Ratio:   0.12%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 622376   (Eliminated:    0 Frozen: 191194)
Constraints  : 4513679  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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         : 260.213s (Solving: 241.73s 1st Model: 0.00s Unsat: 2.40s)
CPU Time     : 260.160s

Choices      : 4269250  (Domain: 4022750)
Conflicts    : 256518   (Analyzed: 256515)
Restarts     : 3050     (Average: 84.10 Last: 157)
Model-Level  : 183.0   
Problems     : 35       (Average Length: 54.71 Splits: 0)
Lemmas       : 256515   (Deleted: 232812)
  Binary     : 5995     (Ratio:   2.34%)
  Ternary    : 2672     (Ratio:   1.04%)
  Conflict   : 256515   (Average Length:  496.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 256515   (Average: 14.68 Max: 1044 Sum: 3765684)
  Executed   : 256374   (Average: 14.66 Max: 1044 Sum: 3761338 Ratio:  99.88%)
  Bounded    : 141      (Average: 30.82 Max:  82 Sum:   4346 Ratio:   0.12%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 622376   (Eliminated:    0 Frozen: 191194)
Constraints  : 4513665  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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: 742.0MB
Grounding...	 [('step', [81]), ('step', [82]), ('step', [83]), ('step', [84]), ('step', [85]), ('check', [85])]
Grounding Time:	 0.60s
Memory:		 668MB (+0MB)
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 36
Time         : 267.786s (Solving: 248.11s 1st Model: 0.00s Unsat: 2.40s)
CPU Time     : 267.736s

Choices      : 4348686  (Domain: 4101788)
Conflicts    : 264283   (Analyzed: 264280)
Restarts     : 3150     (Average: 83.90 Last: 157)
Model-Level  : 183.0   
Problems     : 36       (Average Length: 55.61 Splits: 0)
Lemmas       : 264280   (Deleted: 240259)
  Binary     : 6036     (Ratio:   2.28%)
  Ternary    : 2685     (Ratio:   1.02%)
  Conflict   : 264280   (Average Length:  490.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 264280   (Average: 14.49 Max: 1044 Sum: 3830386)
  Executed   : 264137   (Average: 14.48 Max: 1044 Sum: 3825871 Ratio:  99.88%)
  Bounded    : 143      (Average: 31.57 Max:  87 Sum:   4515 Ratio:   0.12%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 662452   (Eliminated:    0 Frozen: 203644)
Constraints  : 4815631  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 6.51s
Memory:		 691MB (+23MB)
UNKNOWN
Iteration Time:	 7.59s

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

Models       : 0+
Calls        : 37
Time         : 280.324s (Solving: 259.44s 1st Model: 0.00s Unsat: 2.40s)
CPU Time     : 280.280s

Choices      : 4806070  (Domain: 4550562)
Conflicts    : 272656   (Analyzed: 272653)
Restarts     : 3250     (Average: 83.89 Last: 157)
Model-Level  : 183.0   
Problems     : 37       (Average Length: 56.59 Splits: 0)
Lemmas       : 272653   (Deleted: 247693)
  Binary     : 6270     (Ratio:   2.30%)
  Ternary    : 2729     (Ratio:   1.00%)
  Conflict   : 272653   (Average Length:  500.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 272653   (Average: 15.62 Max: 1044 Sum: 4257604)
  Executed   : 272510   (Average: 15.60 Max: 1044 Sum: 4253089 Ratio:  99.89%)
  Bounded    : 143      (Average: 31.57 Max:  87 Sum:   4515 Ratio:   0.11%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 702528   (Eliminated:    0 Frozen: 216094)
Constraints  : 5114549  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 11.47s
Memory:		 763MB (+72MB)
UNKNOWN
Iteration Time:	 12.56s

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

Models       : 0+
Calls        : 38
Time         : 296.936s (Solving: 274.46s 1st Model: 0.00s Unsat: 2.40s)
CPU Time     : 296.896s

Choices      : 5382955  (Domain: 5117111)
Conflicts    : 281712   (Analyzed: 281709)
Restarts     : 3350     (Average: 84.09 Last: 157)
Model-Level  : 183.0   
Problems     : 38       (Average Length: 57.66 Splits: 0)
Lemmas       : 281709   (Deleted: 257600)
  Binary     : 6538     (Ratio:   2.32%)
  Ternary    : 2790     (Ratio:   0.99%)
  Conflict   : 281709   (Average Length:  525.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 281709   (Average: 17.02 Max: 1044 Sum: 4793424)
  Executed   : 281566   (Average: 17.00 Max: 1044 Sum: 4788909 Ratio:  99.91%)
  Bounded    : 143      (Average: 31.57 Max:  87 Sum:   4515 Ratio:   0.09%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 742604   (Eliminated:    0 Frozen: 228544)
Constraints  : 5416529  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 15.16s
Memory:		 882MB (+69MB)
UNKNOWN
Iteration Time:	 16.63s

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

Models       : 0+
Calls        : 39
Time         : 305.801s (Solving: 282.12s 1st Model: 0.00s Unsat: 2.40s)
CPU Time     : 305.764s

Choices      : 5562451  (Domain: 5295760)
Conflicts    : 289712   (Analyzed: 289709)
Restarts     : 3450     (Average: 83.97 Last: 157)
Model-Level  : 183.0   
Problems     : 39       (Average Length: 58.79 Splits: 0)
Lemmas       : 289709   (Deleted: 264065)
  Binary     : 6653     (Ratio:   2.30%)
  Ternary    : 2806     (Ratio:   0.97%)
  Conflict   : 289709   (Average Length:  519.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 289709   (Average: 17.11 Max: 1273 Sum: 4955544)
  Executed   : 289565   (Average: 17.09 Max: 1273 Sum: 4950927 Ratio:  99.91%)
  Bounded    : 144      (Average: 32.06 Max: 102 Sum:   4617 Ratio:   0.09%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 782680   (Eliminated:    0 Frozen: 240994)
Constraints  : 5718509  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 7.81s
Memory:		 888MB (+6MB)
UNKNOWN
Iteration Time:	 8.88s

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

Models       : 0+
Calls        : 40
Time         : 314.321s (Solving: 289.43s 1st Model: 0.00s Unsat: 2.40s)
CPU Time     : 314.288s

Choices      : 5768001  (Domain: 5500320)
Conflicts    : 297542   (Analyzed: 297539)
Restarts     : 3550     (Average: 83.81 Last: 157)
Model-Level  : 183.0   
Problems     : 40       (Average Length: 60.00 Splits: 0)
Lemmas       : 297539   (Deleted: 271686)
  Binary     : 6728     (Ratio:   2.26%)
  Ternary    : 2824     (Ratio:   0.95%)
  Conflict   : 297539   (Average Length:  515.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 297539   (Average: 17.28 Max: 1374 Sum: 5142263)
  Executed   : 297394   (Average: 17.27 Max: 1374 Sum: 5137542 Ratio:  99.91%)
  Bounded    : 145      (Average: 32.56 Max: 104 Sum:   4721 Ratio:   0.09%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 822756   (Eliminated:    0 Frozen: 253444)
Constraints  : 6020476  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 7.46s
Memory:		 914MB (+25MB)
UNKNOWN
Iteration Time:	 8.54s

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         : 321.643s (Solving: 296.58s 1st Model: 0.00s Unsat: 2.40s)
CPU Time     : 321.616s

Choices      : 5826604  (Domain: 5558923)
Conflicts    : 305230   (Analyzed: 305227)
Restarts     : 3650     (Average: 83.62 Last: 157)
Model-Level  : 183.0   
Problems     : 41       (Average Length: 61.15 Splits: 0)
Lemmas       : 305227   (Deleted: 279254)
  Binary     : 6823     (Ratio:   2.24%)
  Ternary    : 2826     (Ratio:   0.93%)
  Conflict   : 305227   (Average Length:  512.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 305227   (Average: 17.02 Max: 1374 Sum: 5195791)
  Executed   : 305082   (Average: 17.01 Max: 1374 Sum: 5191070 Ratio:  99.91%)
  Bounded    : 145      (Average: 32.56 Max: 104 Sum:   4721 Ratio:   0.09%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 822756   (Eliminated:    0 Frozen: 253444)
Constraints  : 6020476  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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         : 330.430s (Solving: 305.20s 1st Model: 0.00s Unsat: 2.40s)
CPU Time     : 330.408s

Choices      : 5896868  (Domain: 5623680)
Conflicts    : 313655   (Analyzed: 313652)
Restarts     : 3750     (Average: 83.64 Last: 157)
Model-Level  : 183.0   
Problems     : 42       (Average Length: 62.24 Splits: 0)
Lemmas       : 313652   (Deleted: 286601)
  Binary     : 6949     (Ratio:   2.22%)
  Ternary    : 2855     (Ratio:   0.91%)
  Conflict   : 313652   (Average Length:  518.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 313652   (Average: 16.75 Max: 1374 Sum: 5252391)
  Executed   : 313507   (Average: 16.73 Max: 1374 Sum: 5247670 Ratio:  99.91%)
  Bounded    : 145      (Average: 32.56 Max: 104 Sum:   4721 Ratio:   0.09%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 822756   (Eliminated:    0 Frozen: 253444)
Constraints  : 6020476  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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         : 335.159s (Solving: 309.74s 1st Model: 0.00s Unsat: 2.40s)
CPU Time     : 335.140s

Choices      : 5947391  (Domain: 5673356)
Conflicts    : 321491   (Analyzed: 321488)
Restarts     : 3850     (Average: 83.50 Last: 157)
Model-Level  : 183.0   
Problems     : 43       (Average Length: 63.28 Splits: 0)
Lemmas       : 321488   (Deleted: 294702)
  Binary     : 6992     (Ratio:   2.17%)
  Ternary    : 2866     (Ratio:   0.89%)
  Conflict   : 321488   (Average Length:  514.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 321488   (Average: 16.47 Max: 1374 Sum: 5294129)
  Executed   : 321343   (Average: 16.45 Max: 1374 Sum: 5289408 Ratio:  99.91%)
  Bounded    : 145      (Average: 32.56 Max: 104 Sum:   4721 Ratio:   0.09%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 822756   (Eliminated:    0 Frozen: 253444)
Constraints  : 6020476  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 4.66s
Memory:		 914MB (+0MB)
UNKNOWN
Iteration Time:	 4.74s

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         : 342.312s (Solving: 316.69s 1st Model: 0.00s Unsat: 2.40s)
CPU Time     : 342.296s

Choices      : 6036512  (Domain: 5760556)
Conflicts    : 329836   (Analyzed: 329833)
Restarts     : 3950     (Average: 83.50 Last: 185)
Model-Level  : 183.0   
Problems     : 44       (Average Length: 64.27 Splits: 0)
Lemmas       : 329833   (Deleted: 302258)
  Binary     : 7076     (Ratio:   2.15%)
  Ternary    : 2884     (Ratio:   0.87%)
  Conflict   : 329833   (Average Length:  510.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 329833   (Average: 16.29 Max: 1374 Sum: 5372439)
  Executed   : 329685   (Average: 16.27 Max: 1374 Sum: 5367404 Ratio:  99.91%)
  Bounded    : 148      (Average: 34.02 Max: 107 Sum:   5035 Ratio:   0.09%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 822756   (Eliminated:    0 Frozen: 253444)
Constraints  : 6020476  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 7.08s
Memory:		 914MB (+0MB)
UNKNOWN
Iteration Time:	 7.16s

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         : 350.390s (Solving: 324.61s 1st Model: 0.00s Unsat: 2.40s)
CPU Time     : 350.380s

Choices      : 6168437  (Domain: 5888804)
Conflicts    : 338780   (Analyzed: 338777)
Restarts     : 4050     (Average: 83.65 Last: 185)
Model-Level  : 183.0   
Problems     : 45       (Average Length: 65.22 Splits: 0)
Lemmas       : 338777   (Deleted: 312440)
  Binary     : 7165     (Ratio:   2.11%)
  Ternary    : 2895     (Ratio:   0.85%)
  Conflict   : 338777   (Average Length:  510.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 338777   (Average: 16.20 Max: 1374 Sum: 5488988)
  Executed   : 338629   (Average: 16.19 Max: 1374 Sum: 5483953 Ratio:  99.91%)
  Bounded    : 148      (Average: 34.02 Max: 107 Sum:   5035 Ratio:   0.09%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 822756   (Eliminated:    0 Frozen: 253444)
Constraints  : 6020462  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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         : 357.056s (Solving: 331.11s 1st Model: 0.00s Unsat: 2.40s)
CPU Time     : 357.048s

Choices      : 6280639  (Domain: 5999286)
Conflicts    : 346955   (Analyzed: 346952)
Restarts     : 4150     (Average: 83.60 Last: 185)
Model-Level  : 183.0   
Problems     : 46       (Average Length: 66.13 Splits: 0)
Lemmas       : 346952   (Deleted: 318946)
  Binary     : 7213     (Ratio:   2.08%)
  Ternary    : 2904     (Ratio:   0.84%)
  Conflict   : 346952   (Average Length:  509.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 346952   (Average: 16.10 Max: 1374 Sum: 5586987)
  Executed   : 346804   (Average: 16.09 Max: 1374 Sum: 5581952 Ratio:  99.91%)
  Bounded    : 148      (Average: 34.02 Max: 107 Sum:   5035 Ratio:   0.09%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 822756   (Eliminated:    0 Frozen: 253444)
Constraints  : 6020462  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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         : 364.389s (Solving: 338.29s 1st Model: 0.00s Unsat: 2.40s)
CPU Time     : 364.384s

Choices      : 6439253  (Domain: 6155618)
Conflicts    : 355230   (Analyzed: 355227)
Restarts     : 4250     (Average: 83.58 Last: 185)
Model-Level  : 183.0   
Problems     : 47       (Average Length: 67.00 Splits: 0)
Lemmas       : 355227   (Deleted: 326815)
  Binary     : 7410     (Ratio:   2.09%)
  Ternary    : 3010     (Ratio:   0.85%)
  Conflict   : 355227   (Average Length:  506.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 355227   (Average: 16.13 Max: 1374 Sum: 5731234)
  Executed   : 355078   (Average: 16.12 Max: 1374 Sum: 5726095 Ratio:  99.91%)
  Bounded    : 149      (Average: 34.49 Max: 107 Sum:   5139 Ratio:   0.09%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 822756   (Eliminated:    0 Frozen: 253444)
Constraints  : 6020462  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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         : 372.105s (Solving: 345.82s 1st Model: 0.00s Unsat: 2.40s)
CPU Time     : 372.104s

Choices      : 6631973  (Domain: 6346310)
Conflicts    : 363365   (Analyzed: 363362)
Restarts     : 4350     (Average: 83.53 Last: 185)
Model-Level  : 183.0   
Problems     : 48       (Average Length: 67.83 Splits: 0)
Lemmas       : 363362   (Deleted: 334432)
  Binary     : 7577     (Ratio:   2.09%)
  Ternary    : 3087     (Ratio:   0.85%)
  Conflict   : 363362   (Average Length:  504.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 363362   (Average: 16.26 Max: 1374 Sum: 5907978)
  Executed   : 363212   (Average: 16.24 Max: 1374 Sum: 5902732 Ratio:  99.91%)
  Bounded    : 150      (Average: 34.97 Max: 107 Sum:   5246 Ratio:   0.09%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 822756   (Eliminated:    0 Frozen: 253444)
Constraints  : 6020462  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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         : 379.766s (Solving: 353.29s 1st Model: 0.00s Unsat: 2.40s)
CPU Time     : 379.768s

Choices      : 6831592  (Domain: 6541482)
Conflicts    : 371683   (Analyzed: 371680)
Restarts     : 4450     (Average: 83.52 Last: 185)
Model-Level  : 183.0   
Problems     : 49       (Average Length: 68.63 Splits: 0)
Lemmas       : 371680   (Deleted: 342205)
  Binary     : 7672     (Ratio:   2.06%)
  Ternary    : 3104     (Ratio:   0.84%)
  Conflict   : 371680   (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    : 371680   (Average: 16.37 Max: 1374 Sum: 6084055)
  Executed   : 371530   (Average: 16.35 Max: 1374 Sum: 6078809 Ratio:  99.91%)
  Bounded    : 150      (Average: 34.97 Max: 107 Sum:   5246 Ratio:   0.09%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 822756   (Eliminated:    0 Frozen: 253444)
Constraints  : 6020448  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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         : 389.333s (Solving: 362.66s 1st Model: 0.00s Unsat: 2.40s)
CPU Time     : 389.340s

Choices      : 7114481  (Domain: 6821255)
Conflicts    : 380450   (Analyzed: 380447)
Restarts     : 4550     (Average: 83.61 Last: 185)
Model-Level  : 183.0   
Problems     : 50       (Average Length: 69.40 Splits: 0)
Lemmas       : 380447   (Deleted: 352305)
  Binary     : 7803     (Ratio:   2.05%)
  Ternary    : 3142     (Ratio:   0.83%)
  Conflict   : 380447   (Average Length:  502.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 380447   (Average: 16.68 Max: 1374 Sum: 6346973)
  Executed   : 380297   (Average: 16.67 Max: 1374 Sum: 6341727 Ratio:  99.92%)
  Bounded    : 150      (Average: 34.97 Max: 107 Sum:   5246 Ratio:   0.08%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 822756   (Eliminated:    0 Frozen: 253444)
Constraints  : 6020448  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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         : 399.271s (Solving: 372.43s 1st Model: 0.00s Unsat: 2.40s)
CPU Time     : 399.276s

Choices      : 7405815  (Domain: 7110612)
Conflicts    : 388712   (Analyzed: 388709)
Restarts     : 4650     (Average: 83.59 Last: 185)
Model-Level  : 183.0   
Problems     : 51       (Average Length: 70.14 Splits: 0)
Lemmas       : 388709   (Deleted: 358623)
  Binary     : 7858     (Ratio:   2.02%)
  Ternary    : 3160     (Ratio:   0.81%)
  Conflict   : 388709   (Average Length:  504.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 388709   (Average: 17.02 Max: 1374 Sum: 6614005)
  Executed   : 388559   (Average: 17.00 Max: 1374 Sum: 6608759 Ratio:  99.92%)
  Bounded    : 150      (Average: 34.97 Max: 107 Sum:   5246 Ratio:   0.08%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 822756   (Eliminated:    0 Frozen: 253444)
Constraints  : 6020448  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 9.88s
Memory:		 914MB (+0MB)
UNKNOWN
Iteration Time:	 9.94s

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         : 412.928s (Solving: 385.89s 1st Model: 0.00s Unsat: 2.40s)
CPU Time     : 412.936s

Choices      : 7920513  (Domain: 7620183)
Conflicts    : 397908   (Analyzed: 397905)
Restarts     : 4750     (Average: 83.77 Last: 185)
Model-Level  : 183.0   
Problems     : 52       (Average Length: 70.85 Splits: 0)
Lemmas       : 397905   (Deleted: 368777)
  Binary     : 8035     (Ratio:   2.02%)
  Ternary    : 3185     (Ratio:   0.80%)
  Conflict   : 397905   (Average Length:  510.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 397905   (Average: 17.84 Max: 1374 Sum: 7097953)
  Executed   : 397755   (Average: 17.83 Max: 1374 Sum: 7092707 Ratio:  99.93%)
  Bounded    : 150      (Average: 34.97 Max: 107 Sum:   5246 Ratio:   0.07%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 822756   (Eliminated:    0 Frozen: 253444)
Constraints  : 6020448  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 13.58s
Memory:		 914MB (+0MB)
UNKNOWN
Iteration Time:	 13.67s

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         : 420.742s (Solving: 393.51s 1st Model: 0.00s Unsat: 2.40s)
CPU Time     : 420.752s

Choices      : 8140639  (Domain: 7838774)
Conflicts    : 405543   (Analyzed: 405540)
Restarts     : 4850     (Average: 83.62 Last: 185)
Model-Level  : 183.0   
Problems     : 53       (Average Length: 71.53 Splits: 0)
Lemmas       : 405540   (Deleted: 375482)
  Binary     : 8079     (Ratio:   1.99%)
  Ternary    : 3192     (Ratio:   0.79%)
  Conflict   : 405540   (Average Length:  509.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 405540   (Average: 18.00 Max: 1374 Sum: 7298202)
  Executed   : 405390   (Average: 17.98 Max: 1374 Sum: 7292956 Ratio:  99.93%)
  Bounded    : 150      (Average: 34.97 Max: 107 Sum:   5246 Ratio:   0.07%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 822756   (Eliminated:    0 Frozen: 253444)
Constraints  : 6020448  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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         : 428.666s (Solving: 401.27s 1st Model: 0.00s Unsat: 2.40s)
CPU Time     : 428.676s

Choices      : 8438795  (Domain: 8135512)
Conflicts    : 413601   (Analyzed: 413598)
Restarts     : 4950     (Average: 83.56 Last: 185)
Model-Level  : 183.0   
Problems     : 54       (Average Length: 72.19 Splits: 0)
Lemmas       : 413598   (Deleted: 382895)
  Binary     : 8130     (Ratio:   1.97%)
  Ternary    : 3219     (Ratio:   0.78%)
  Conflict   : 413598   (Average Length:  507.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 413598   (Average: 18.30 Max: 1374 Sum: 7570763)
  Executed   : 413448   (Average: 18.29 Max: 1374 Sum: 7565517 Ratio:  99.93%)
  Bounded    : 150      (Average: 34.97 Max: 107 Sum:   5246 Ratio:   0.07%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 822756   (Eliminated:    0 Frozen: 253444)
Constraints  : 6020448  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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         : 440.515s (Solving: 412.95s 1st Model: 0.00s Unsat: 2.40s)
CPU Time     : 440.516s

Choices      : 9046151  (Domain: 8739101)
Conflicts    : 422005   (Analyzed: 422002)
Restarts     : 5050     (Average: 83.56 Last: 185)
Model-Level  : 183.0   
Problems     : 55       (Average Length: 72.82 Splits: 0)
Lemmas       : 422002   (Deleted: 390171)
  Binary     : 8341     (Ratio:   1.98%)
  Ternary    : 3405     (Ratio:   0.81%)
  Conflict   : 422002   (Average Length:  505.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 422002   (Average: 19.31 Max: 1374 Sum: 8148974)
  Executed   : 421852   (Average: 19.30 Max: 1374 Sum: 8143728 Ratio:  99.94%)
  Bounded    : 150      (Average: 34.97 Max: 107 Sum:   5246 Ratio:   0.06%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 822756   (Eliminated:    0 Frozen: 253444)
Constraints  : 6020448  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 11.77s
Memory:		 914MB (+0MB)
UNKNOWN
Iteration Time:	 11.84s

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

Models       : 0+
Calls        : 56
Time         : 453.155s (Solving: 424.33s 1st Model: 0.00s Unsat: 2.40s)
CPU Time     : 453.164s

Choices      : 9387514  (Domain: 9078824)
Conflicts    : 430106   (Analyzed: 430103)
Restarts     : 5150     (Average: 83.52 Last: 185)
Model-Level  : 183.0   
Problems     : 56       (Average Length: 73.52 Splits: 0)
Lemmas       : 430103   (Deleted: 397920)
  Binary     : 8438     (Ratio:   1.96%)
  Ternary    : 3434     (Ratio:   0.80%)
  Conflict   : 430103   (Average Length:  503.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 430103   (Average: 19.67 Max: 1374 Sum: 8461648)
  Executed   : 429953   (Average: 19.66 Max: 1374 Sum: 8456402 Ratio:  99.94%)
  Bounded    : 150      (Average: 34.97 Max: 107 Sum:   5246 Ratio:   0.06%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 862832   (Eliminated:    0 Frozen: 265894)
Constraints  : 6322428  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 11.54s
Memory:		 946MB (+32MB)
UNKNOWN
Iteration Time:	 12.66s

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

Models       : 0+
Calls        : 57
Time         : 477.954s (Solving: 447.85s 1st Model: 0.00s Unsat: 2.40s)
CPU Time     : 477.940s

Choices      : 10831659 (Domain: 10511735)
Conflicts    : 440818   (Analyzed: 440815)
Restarts     : 5250     (Average: 83.96 Last: 185)
Model-Level  : 183.0   
Problems     : 57       (Average Length: 74.28 Splits: 0)
Lemmas       : 440815   (Deleted: 406854)
  Binary     : 9271     (Ratio:   2.10%)
  Ternary    : 3822     (Ratio:   0.87%)
  Conflict   : 440815   (Average Length:  505.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 440815   (Average: 22.35 Max: 1455 Sum: 9854382)
  Executed   : 440665   (Average: 22.34 Max: 1455 Sum: 9849136 Ratio:  99.95%)
  Bounded    : 150      (Average: 34.97 Max: 107 Sum:   5246 Ratio:   0.05%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 902908   (Eliminated:    0 Frozen: 278344)
Constraints  : 6624408  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 23.66s
Memory:		 975MB (+29MB)
UNKNOWN
Iteration Time:	 24.79s

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         : 484.554s (Solving: 454.27s 1st Model: 0.00s Unsat: 2.40s)
CPU Time     : 484.544s

Choices      : 10879063 (Domain: 10559139)
Conflicts    : 448316   (Analyzed: 448313)
Restarts     : 5350     (Average: 83.80 Last: 185)
Model-Level  : 183.0   
Problems     : 58       (Average Length: 75.02 Splits: 0)
Lemmas       : 448313   (Deleted: 413945)
  Binary     : 9333     (Ratio:   2.08%)
  Ternary    : 3831     (Ratio:   0.85%)
  Conflict   : 448313   (Average Length:  501.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 448313   (Average: 22.07 Max: 1455 Sum: 9895935)
  Executed   : 448161   (Average: 22.06 Max: 1455 Sum: 9890455 Ratio:  99.94%)
  Bounded    : 152      (Average: 36.05 Max: 117 Sum:   5480 Ratio:   0.06%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 902908   (Eliminated:    0 Frozen: 278344)
Constraints  : 6624408  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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         : 490.556s (Solving: 460.05s 1st Model: 0.00s Unsat: 2.40s)
CPU Time     : 490.548s

Choices      : 10924947 (Domain: 10605023)
Conflicts    : 456079   (Analyzed: 456076)
Restarts     : 5450     (Average: 83.68 Last: 185)
Model-Level  : 183.0   
Problems     : 59       (Average Length: 75.73 Splits: 0)
Lemmas       : 456076   (Deleted: 421159)
  Binary     : 9367     (Ratio:   2.05%)
  Ternary    : 3833     (Ratio:   0.84%)
  Conflict   : 456076   (Average Length:  501.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 456076   (Average: 21.78 Max: 1455 Sum: 9932435)
  Executed   : 455924   (Average: 21.77 Max: 1455 Sum: 9926955 Ratio:  99.94%)
  Bounded    : 152      (Average: 36.05 Max: 117 Sum:   5480 Ratio:   0.06%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 902908   (Eliminated:    0 Frozen: 278344)
Constraints  : 6624381  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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         : 496.094s (Solving: 465.39s 1st Model: 0.00s Unsat: 2.40s)
CPU Time     : 496.088s

Choices      : 10986705 (Domain: 10665581)
Conflicts    : 463289   (Analyzed: 463286)
Restarts     : 5550     (Average: 83.47 Last: 185)
Model-Level  : 183.0   
Problems     : 60       (Average Length: 76.42 Splits: 0)
Lemmas       : 463286   (Deleted: 428631)
  Binary     : 9475     (Ratio:   2.05%)
  Ternary    : 3846     (Ratio:   0.83%)
  Conflict   : 463286   (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    : 463286   (Average: 21.55 Max: 1455 Sum: 9982573)
  Executed   : 463134   (Average: 21.54 Max: 1455 Sum: 9977093 Ratio:  99.95%)
  Bounded    : 152      (Average: 36.05 Max: 117 Sum:   5480 Ratio:   0.05%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 902908   (Eliminated:    0 Frozen: 278344)
Constraints  : 6624381  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 5.47s
Memory:		 975MB (+0MB)
UNKNOWN
Iteration Time:	 5.54s

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         : 501.089s (Solving: 470.18s 1st Model: 0.00s Unsat: 2.40s)
CPU Time     : 501.084s

Choices      : 11030102 (Domain: 10708956)
Conflicts    : 470556   (Analyzed: 470553)
Restarts     : 5650     (Average: 83.28 Last: 185)
Model-Level  : 183.0   
Problems     : 61       (Average Length: 77.08 Splits: 0)
Lemmas       : 470553   (Deleted: 435488)
  Binary     : 9548     (Ratio:   2.03%)
  Ternary    : 3868     (Ratio:   0.82%)
  Conflict   : 470553   (Average Length:  497.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 470553   (Average: 21.29 Max: 1455 Sum: 10017916)
  Executed   : 470400   (Average: 21.28 Max: 1455 Sum: 10012323 Ratio:  99.94%)
  Bounded    : 153      (Average: 36.56 Max: 117 Sum:   5593 Ratio:   0.06%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 902908   (Eliminated:    0 Frozen: 278344)
Constraints  : 6624381  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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         : 514.305s (Solving: 483.22s 1st Model: 0.00s Unsat: 2.40s)
CPU Time     : 514.304s

Choices      : 11142025 (Domain: 10817712)
Conflicts    : 479227   (Analyzed: 479224)
Restarts     : 5750     (Average: 83.34 Last: 185)
Model-Level  : 183.0   
Problems     : 62       (Average Length: 77.73 Splits: 0)
Lemmas       : 479224   (Deleted: 444388)
  Binary     : 9753     (Ratio:   2.04%)
  Ternary    : 3905     (Ratio:   0.81%)
  Conflict   : 479224   (Average Length:  509.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 479224   (Average: 21.08 Max: 1455 Sum: 10102920)
  Executed   : 479071   (Average: 21.07 Max: 1455 Sum: 10097327 Ratio:  99.94%)
  Bounded    : 153      (Average: 36.56 Max: 117 Sum:   5593 Ratio:   0.06%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 902908   (Eliminated:    0 Frozen: 278344)
Constraints  : 6624381  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 13.16s
Memory:		 975MB (+0MB)
UNKNOWN
Iteration Time:	 13.22s

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         : 521.554s (Solving: 490.28s 1st Model: 0.00s Unsat: 2.40s)
CPU Time     : 521.548s

Choices      : 11217424 (Domain: 10892754)
Conflicts    : 486729   (Analyzed: 486726)
Restarts     : 5850     (Average: 83.20 Last: 185)
Model-Level  : 183.0   
Problems     : 63       (Average Length: 78.35 Splits: 0)
Lemmas       : 486726   (Deleted: 450665)
  Binary     : 9882     (Ratio:   2.03%)
  Ternary    : 3947     (Ratio:   0.81%)
  Conflict   : 486726   (Average Length:  506.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 486726   (Average: 20.89 Max: 1455 Sum: 10166930)
  Executed   : 486569   (Average: 20.88 Max: 1455 Sum: 10160874 Ratio:  99.94%)
  Bounded    : 157      (Average: 38.57 Max: 117 Sum:   6056 Ratio:   0.06%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 902908   (Eliminated:    0 Frozen: 278344)
Constraints  : 6624381  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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         : 532.779s (Solving: 501.29s 1st Model: 0.00s Unsat: 2.40s)
CPU Time     : 532.780s

Choices      : 11414476 (Domain: 11087229)
Conflicts    : 495018   (Analyzed: 495015)
Restarts     : 5950     (Average: 83.20 Last: 185)
Model-Level  : 183.0   
Problems     : 64       (Average Length: 78.95 Splits: 0)
Lemmas       : 495015   (Deleted: 457334)
  Binary     : 10090    (Ratio:   2.04%)
  Ternary    : 4014     (Ratio:   0.81%)
  Conflict   : 495015   (Average Length:  511.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 495015   (Average: 20.89 Max: 1455 Sum: 10341849)
  Executed   : 494858   (Average: 20.88 Max: 1455 Sum: 10335793 Ratio:  99.94%)
  Bounded    : 157      (Average: 38.57 Max: 117 Sum:   6056 Ratio:   0.06%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 902908   (Eliminated:    0 Frozen: 278344)
Constraints  : 6624341  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 11.14s
Memory:		 975MB (+0MB)
UNKNOWN
Iteration Time:	 11.23s

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         : 544.248s (Solving: 512.57s 1st Model: 0.00s Unsat: 2.40s)
CPU Time     : 544.256s

Choices      : 11668016 (Domain: 11339143)
Conflicts    : 503596   (Analyzed: 503593)
Restarts     : 6050     (Average: 83.24 Last: 185)
Model-Level  : 183.0   
Problems     : 65       (Average Length: 79.54 Splits: 0)
Lemmas       : 503593   (Deleted: 465102)
  Binary     : 10213    (Ratio:   2.03%)
  Ternary    : 4053     (Ratio:   0.80%)
  Conflict   : 503593   (Average Length:  512.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 503593   (Average: 20.99 Max: 1455 Sum: 10572702)
  Executed   : 503436   (Average: 20.98 Max: 1455 Sum: 10566646 Ratio:  99.94%)
  Bounded    : 157      (Average: 38.57 Max: 117 Sum:   6056 Ratio:   0.06%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 902908   (Eliminated:    0 Frozen: 278344)
Constraints  : 6624341  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 11.41s
Memory:		 975MB (+0MB)
UNKNOWN
Iteration Time:	 11.48s

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         : 555.128s (Solving: 523.24s 1st Model: 0.00s Unsat: 2.40s)
CPU Time     : 555.144s

Choices      : 11937161 (Domain: 11606955)
Conflicts    : 512151   (Analyzed: 512148)
Restarts     : 6150     (Average: 83.28 Last: 185)
Model-Level  : 183.0   
Problems     : 66       (Average Length: 80.11 Splits: 0)
Lemmas       : 512148   (Deleted: 473103)
  Binary     : 10319    (Ratio:   2.01%)
  Ternary    : 4077     (Ratio:   0.80%)
  Conflict   : 512148   (Average Length:  514.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 512148   (Average: 21.12 Max: 1455 Sum: 10816985)
  Executed   : 511991   (Average: 21.11 Max: 1455 Sum: 10810929 Ratio:  99.94%)
  Bounded    : 157      (Average: 38.57 Max: 117 Sum:   6056 Ratio:   0.06%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 902908   (Eliminated:    0 Frozen: 278344)
Constraints  : 6624341  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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         : 565.666s (Solving: 533.58s 1st Model: 0.00s Unsat: 2.40s)
CPU Time     : 565.688s

Choices      : 12317914 (Domain: 11986494)
Conflicts    : 520221   (Analyzed: 520218)
Restarts     : 6250     (Average: 83.23 Last: 185)
Model-Level  : 183.0   
Problems     : 67       (Average Length: 80.66 Splits: 0)
Lemmas       : 520218   (Deleted: 481326)
  Binary     : 10396    (Ratio:   2.00%)
  Ternary    : 4130     (Ratio:   0.79%)
  Conflict   : 520218   (Average Length:  517.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 520218   (Average: 21.47 Max: 1455 Sum: 11168194)
  Executed   : 520061   (Average: 21.46 Max: 1455 Sum: 11162138 Ratio:  99.95%)
  Bounded    : 157      (Average: 38.57 Max: 117 Sum:   6056 Ratio:   0.05%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 902908   (Eliminated:    0 Frozen: 278344)
Constraints  : 6624341  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 10.47s
Memory:		 975MB (+0MB)
UNKNOWN
Iteration Time:	 10.55s

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

Models       : 0+
Calls        : 68
Time         : 582.335s (Solving: 550.02s 1st Model: 0.00s Unsat: 2.40s)
CPU Time     : 582.364s

Choices      : 13088569 (Domain: 12752469)
Conflicts    : 528948   (Analyzed: 528945)
Restarts     : 6350     (Average: 83.30 Last: 185)
Model-Level  : 183.0   
Problems     : 68       (Average Length: 81.19 Splits: 0)
Lemmas       : 528945   (Deleted: 490920)
  Binary     : 10750    (Ratio:   2.03%)
  Ternary    : 4323     (Ratio:   0.82%)
  Conflict   : 528945   (Average Length:  519.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 528945   (Average: 22.49 Max: 1562 Sum: 11896548)
  Executed   : 528788   (Average: 22.48 Max: 1562 Sum: 11890492 Ratio:  99.95%)
  Bounded    : 157      (Average: 38.57 Max: 117 Sum:   6056 Ratio:   0.05%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 902908   (Eliminated:    0 Frozen: 278344)
Constraints  : 6624341  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 16.59s
Memory:		 975MB (+0MB)
UNKNOWN
Iteration Time:	 16.68s

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         : 588.065s (Solving: 555.53s 1st Model: 0.00s Unsat: 2.40s)
CPU Time     : 588.088s

Choices      : 13146278 (Domain: 12810178)
Conflicts    : 536554   (Analyzed: 536551)
Restarts     : 6450     (Average: 83.19 Last: 185)
Model-Level  : 183.0   
Problems     : 69       (Average Length: 81.71 Splits: 0)
Lemmas       : 536551   (Deleted: 496486)
  Binary     : 10836    (Ratio:   2.02%)
  Ternary    : 4334     (Ratio:   0.81%)
  Conflict   : 536551   (Average Length:  518.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 536551   (Average: 22.27 Max: 1562 Sum: 11946514)
  Executed   : 536393   (Average: 22.25 Max: 1562 Sum: 11940342 Ratio:  99.95%)
  Bounded    : 158      (Average: 39.06 Max: 117 Sum:   6172 Ratio:   0.05%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 902908   (Eliminated:    0 Frozen: 278344)
Constraints  : 6624341  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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         : 592.454s (Solving: 559.74s 1st Model: 0.00s Unsat: 2.40s)
CPU Time     : 592.476s

Choices      : 13186477 (Domain: 12850377)
Conflicts    : 544160   (Analyzed: 544157)
Restarts     : 6550     (Average: 83.08 Last: 185)
Model-Level  : 183.0   
Problems     : 70       (Average Length: 82.21 Splits: 0)
Lemmas       : 544157   (Deleted: 503845)
  Binary     : 10858    (Ratio:   2.00%)
  Ternary    : 4336     (Ratio:   0.80%)
  Conflict   : 544157   (Average Length:  517.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 544157   (Average: 22.01 Max: 1562 Sum: 11978079)
  Executed   : 543999   (Average: 22.00 Max: 1562 Sum: 11971907 Ratio:  99.95%)
  Bounded    : 158      (Average: 39.06 Max: 117 Sum:   6172 Ratio:   0.05%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 902908   (Eliminated:    0 Frozen: 278344)
Constraints  : 6624341  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 4.33s
Memory:		 975MB (+0MB)
UNKNOWN
Iteration Time:	 4.39s

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         : 600.560s (Solving: 567.65s 1st Model: 0.00s Unsat: 2.40s)
CPU Time     : 600.584s

Choices      : 13260918 (Domain: 12920098)
Conflicts    : 552886   (Analyzed: 552883)
Restarts     : 6650     (Average: 83.14 Last: 185)
Model-Level  : 183.0   
Problems     : 71       (Average Length: 82.70 Splits: 0)
Lemmas       : 552883   (Deleted: 513368)
  Binary     : 10965    (Ratio:   1.98%)
  Ternary    : 4358     (Ratio:   0.79%)
  Conflict   : 552883   (Average Length:  520.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 552883   (Average: 21.77 Max: 1562 Sum: 12034743)
  Executed   : 552725   (Average: 21.76 Max: 1562 Sum: 12028571 Ratio:  99.95%)
  Bounded    : 158      (Average: 39.06 Max: 117 Sum:   6172 Ratio:   0.05%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 902908   (Eliminated:    0 Frozen: 278344)
Constraints  : 6624341  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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         : 605.272s (Solving: 572.15s 1st Model: 0.00s Unsat: 2.40s)
CPU Time     : 605.296s

Choices      : 13317430 (Domain: 12975523)
Conflicts    : 560480   (Analyzed: 560477)
Restarts     : 6750     (Average: 83.03 Last: 185)
Model-Level  : 183.0   
Problems     : 72       (Average Length: 83.18 Splits: 0)
Lemmas       : 560477   (Deleted: 519465)
  Binary     : 11030    (Ratio:   1.97%)
  Ternary    : 4396     (Ratio:   0.78%)
  Conflict   : 560477   (Average Length:  517.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 560477   (Average: 21.55 Max: 1562 Sum: 12080644)
  Executed   : 560319   (Average: 21.54 Max: 1562 Sum: 12074472 Ratio:  99.95%)
  Bounded    : 158      (Average: 39.06 Max: 117 Sum:   6172 Ratio:   0.05%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 902908   (Eliminated:    0 Frozen: 278344)
Constraints  : 6624341  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 4.63s
Memory:		 975MB (+0MB)
UNKNOWN
Iteration Time:	 4.72s

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         : 612.491s (Solving: 579.19s 1st Model: 0.00s Unsat: 2.40s)
CPU Time     : 612.516s

Choices      : 13399866 (Domain: 13057114)
Conflicts    : 568275   (Analyzed: 568272)
Restarts     : 6850     (Average: 82.96 Last: 185)
Model-Level  : 183.0   
Problems     : 73       (Average Length: 83.64 Splits: 0)
Lemmas       : 568272   (Deleted: 526626)
  Binary     : 11227    (Ratio:   1.98%)
  Ternary    : 4486     (Ratio:   0.79%)
  Conflict   : 568272   (Average Length:  517.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 568272   (Average: 21.38 Max: 1562 Sum: 12150356)
  Executed   : 568113   (Average: 21.37 Max: 1562 Sum: 12144071 Ratio:  99.95%)
  Bounded    : 159      (Average: 39.53 Max: 117 Sum:   6285 Ratio:   0.05%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 902908   (Eliminated:    0 Frozen: 278344)
Constraints  : 6624341  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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         : 624.730s (Solving: 591.24s 1st Model: 0.00s Unsat: 2.40s)
CPU Time     : 624.756s

Choices      : 13550436 (Domain: 13206308)
Conflicts    : 576763   (Analyzed: 576760)
Restarts     : 6950     (Average: 82.99 Last: 185)
Model-Level  : 183.0   
Problems     : 74       (Average Length: 84.09 Splits: 0)
Lemmas       : 576760   (Deleted: 533795)
  Binary     : 11402    (Ratio:   1.98%)
  Ternary    : 4562     (Ratio:   0.79%)
  Conflict   : 576760   (Average Length:  523.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 576760   (Average: 21.29 Max: 1562 Sum: 12278204)
  Executed   : 576601   (Average: 21.28 Max: 1562 Sum: 12271919 Ratio:  99.95%)
  Bounded    : 159      (Average: 39.53 Max: 117 Sum:   6285 Ratio:   0.05%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 902908   (Eliminated:    0 Frozen: 278344)
Constraints  : 6624341  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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         : 639.378s (Solving: 605.69s 1st Model: 0.00s Unsat: 2.40s)
CPU Time     : 639.408s

Choices      : 13754428 (Domain: 13408461)
Conflicts    : 585767   (Analyzed: 585764)
Restarts     : 7050     (Average: 83.09 Last: 185)
Model-Level  : 183.0   
Problems     : 75       (Average Length: 84.53 Splits: 0)
Lemmas       : 585764   (Deleted: 543773)
  Binary     : 11646    (Ratio:   1.99%)
  Ternary    : 4656     (Ratio:   0.79%)
  Conflict   : 585764   (Average Length:  531.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 585764   (Average: 21.26 Max: 1562 Sum: 12452649)
  Executed   : 585605   (Average: 21.25 Max: 1562 Sum: 12446364 Ratio:  99.95%)
  Bounded    : 159      (Average: 39.53 Max: 117 Sum:   6285 Ratio:   0.05%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 902908   (Eliminated:    0 Frozen: 278344)
Constraints  : 6624341  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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         : 653.162s (Solving: 619.29s 1st Model: 0.00s Unsat: 2.40s)
CPU Time     : 653.196s

Choices      : 13957281 (Domain: 13609805)
Conflicts    : 594135   (Analyzed: 594132)
Restarts     : 7150     (Average: 83.10 Last: 185)
Model-Level  : 183.0   
Problems     : 76       (Average Length: 84.96 Splits: 0)
Lemmas       : 594132   (Deleted: 550302)
  Binary     : 11820    (Ratio:   1.99%)
  Ternary    : 4704     (Ratio:   0.79%)
  Conflict   : 594132   (Average Length:  541.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 594132   (Average: 21.25 Max: 1562 Sum: 12625961)
  Executed   : 593973   (Average: 21.24 Max: 1562 Sum: 12619676 Ratio:  99.95%)
  Bounded    : 159      (Average: 39.53 Max: 117 Sum:   6285 Ratio:   0.05%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 902908   (Eliminated:    0 Frozen: 278344)
Constraints  : 6624341  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 13.73s
Memory:		 975MB (+0MB)
UNKNOWN
Iteration Time:	 13.79s

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         : 667.620s (Solving: 633.54s 1st Model: 0.00s Unsat: 2.40s)
CPU Time     : 667.660s

Choices      : 14229081 (Domain: 13878957)
Conflicts    : 602414   (Analyzed: 602411)
Restarts     : 7250     (Average: 83.09 Last: 185)
Model-Level  : 183.0   
Problems     : 77       (Average Length: 85.38 Splits: 0)
Lemmas       : 602411   (Deleted: 558174)
  Binary     : 12049    (Ratio:   2.00%)
  Ternary    : 4758     (Ratio:   0.79%)
  Conflict   : 602411   (Average Length:  551.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 602411   (Average: 21.36 Max: 1562 Sum: 12866776)
  Executed   : 602252   (Average: 21.35 Max: 1562 Sum: 12860491 Ratio:  99.95%)
  Bounded    : 159      (Average: 39.53 Max: 117 Sum:   6285 Ratio:   0.05%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 902908   (Eliminated:    0 Frozen: 278344)
Constraints  : 6624341  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 14.38s
Memory:		 975MB (+0MB)
UNKNOWN
Iteration Time:	 14.47s

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         : 688.445s (Solving: 654.18s 1st Model: 0.00s Unsat: 2.40s)
CPU Time     : 688.492s

Choices      : 14711711 (Domain: 14353351)
Conflicts    : 611580   (Analyzed: 611577)
Restarts     : 7350     (Average: 83.21 Last: 185)
Model-Level  : 183.0   
Problems     : 78       (Average Length: 85.78 Splits: 0)
Lemmas       : 611577   (Deleted: 567670)
  Binary     : 12557    (Ratio:   2.05%)
  Ternary    : 4895     (Ratio:   0.80%)
  Conflict   : 611577   (Average Length:  564.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 611577   (Average: 21.74 Max: 1562 Sum: 13295201)
  Executed   : 611418   (Average: 21.73 Max: 1562 Sum: 13288916 Ratio:  99.95%)
  Bounded    : 159      (Average: 39.53 Max: 117 Sum:   6285 Ratio:   0.05%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 902908   (Eliminated:    0 Frozen: 278344)
Constraints  : 6624341  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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         : 694.262s (Solving: 659.80s 1st Model: 0.00s Unsat: 2.40s)
CPU Time     : 694.312s

Choices      : 14768725 (Domain: 14410365)
Conflicts    : 620106   (Analyzed: 620103)
Restarts     : 7450     (Average: 83.24 Last: 185)
Model-Level  : 183.0   
Problems     : 79       (Average Length: 86.18 Splits: 0)
Lemmas       : 620103   (Deleted: 574044)
  Binary     : 12611    (Ratio:   2.03%)
  Ternary    : 4906     (Ratio:   0.79%)
  Conflict   : 620103   (Average Length:  561.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 620103   (Average: 21.52 Max: 1562 Sum: 13342839)
  Executed   : 619944   (Average: 21.51 Max: 1562 Sum: 13336554 Ratio:  99.95%)
  Bounded    : 159      (Average: 39.53 Max: 117 Sum:   6285 Ratio:   0.05%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 902908   (Eliminated:    0 Frozen: 278344)
Constraints  : 6624341  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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         : 697.964s (Solving: 663.32s 1st Model: 0.00s Unsat: 2.40s)
CPU Time     : 698.016s

Choices      : 14803436 (Domain: 14445076)
Conflicts    : 627340   (Analyzed: 627337)
Restarts     : 7550     (Average: 83.09 Last: 185)
Model-Level  : 183.0   
Problems     : 80       (Average Length: 86.56 Splits: 0)
Lemmas       : 627337   (Deleted: 582303)
  Binary     : 12618    (Ratio:   2.01%)
  Ternary    : 4907     (Ratio:   0.78%)
  Conflict   : 627337   (Average Length:  561.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 627337   (Average: 21.31 Max: 1562 Sum: 13368084)
  Executed   : 627177   (Average: 21.30 Max: 1562 Sum: 13361682 Ratio:  99.95%)
  Bounded    : 160      (Average: 40.01 Max: 117 Sum:   6402 Ratio:   0.05%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 902908   (Eliminated:    0 Frozen: 278344)
Constraints  : 6624341  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 3.64s
Memory:		 975MB (+0MB)
UNKNOWN
Iteration Time:	 3.71s

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         : 705.316s (Solving: 670.46s 1st Model: 0.00s Unsat: 2.40s)
CPU Time     : 705.372s

Choices      : 14876037 (Domain: 14517677)
Conflicts    : 635476   (Analyzed: 635473)
Restarts     : 7650     (Average: 83.07 Last: 185)
Model-Level  : 183.0   
Problems     : 81       (Average Length: 86.94 Splits: 0)
Lemmas       : 635473   (Deleted: 589436)
  Binary     : 12660    (Ratio:   1.99%)
  Ternary    : 4927     (Ratio:   0.78%)
  Conflict   : 635473   (Average Length:  561.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 635473   (Average: 21.13 Max: 1562 Sum: 13427038)
  Executed   : 635312   (Average: 21.12 Max: 1562 Sum: 13420519 Ratio:  99.95%)
  Bounded    : 161      (Average: 40.49 Max: 117 Sum:   6519 Ratio:   0.05%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 902908   (Eliminated:    0 Frozen: 278344)
Constraints  : 6624315  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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         : 714.196s (Solving: 679.16s 1st Model: 0.00s Unsat: 2.40s)
CPU Time     : 714.240s

Choices      : 14964621 (Domain: 14606225)
Conflicts    : 644276   (Analyzed: 644273)
Restarts     : 7750     (Average: 83.13 Last: 185)
Model-Level  : 183.0   
Problems     : 82       (Average Length: 87.30 Splits: 0)
Lemmas       : 644273   (Deleted: 598824)
  Binary     : 12774    (Ratio:   1.98%)
  Ternary    : 4948     (Ratio:   0.77%)
  Conflict   : 644273   (Average Length:  560.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 644273   (Average: 20.95 Max: 1562 Sum: 13499468)
  Executed   : 644112   (Average: 20.94 Max: 1562 Sum: 13492949 Ratio:  99.95%)
  Bounded    : 161      (Average: 40.49 Max: 117 Sum:   6519 Ratio:   0.05%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 902908   (Eliminated:    0 Frozen: 278344)
Constraints  : 6624301  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 8.80s
Memory:		 975MB (+0MB)
UNKNOWN
Iteration Time:	 8.87s

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         : 721.282s (Solving: 686.07s 1st Model: 0.00s Unsat: 2.40s)
CPU Time     : 721.328s

Choices      : 15037395 (Domain: 14677670)
Conflicts    : 652050   (Analyzed: 652047)
Restarts     : 7850     (Average: 83.06 Last: 185)
Model-Level  : 183.0   
Problems     : 83       (Average Length: 87.66 Splits: 0)
Lemmas       : 652047   (Deleted: 605184)
  Binary     : 12879    (Ratio:   1.98%)
  Ternary    : 4985     (Ratio:   0.76%)
  Conflict   : 652047   (Average Length:  564.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 652047   (Average: 20.79 Max: 1562 Sum: 13555664)
  Executed   : 651885   (Average: 20.78 Max: 1562 Sum: 13549032 Ratio:  99.95%)
  Bounded    : 162      (Average: 40.94 Max: 117 Sum:   6632 Ratio:   0.05%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 902908   (Eliminated:    0 Frozen: 278344)
Constraints  : 6624301  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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         : 735.705s (Solving: 700.30s 1st Model: 0.00s Unsat: 2.40s)
CPU Time     : 735.756s

Choices      : 15211825 (Domain: 14851226)
Conflicts    : 660424   (Analyzed: 660421)
Restarts     : 7950     (Average: 83.07 Last: 185)
Model-Level  : 183.0   
Problems     : 84       (Average Length: 88.01 Splits: 0)
Lemmas       : 660421   (Deleted: 612860)
  Binary     : 13052    (Ratio:   1.98%)
  Ternary    : 5021     (Ratio:   0.76%)
  Conflict   : 660421   (Average Length:  574.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 660421   (Average: 20.75 Max: 1562 Sum: 13701359)
  Executed   : 660259   (Average: 20.74 Max: 1562 Sum: 13694727 Ratio:  99.95%)
  Bounded    : 162      (Average: 40.94 Max: 117 Sum:   6632 Ratio:   0.05%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 902908   (Eliminated:    0 Frozen: 278344)
Constraints  : 6624301  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 14.36s
Memory:		 975MB (+0MB)
UNKNOWN
Iteration Time:	 14.43s

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         : 749.084s (Solving: 713.49s 1st Model: 0.00s Unsat: 2.40s)
CPU Time     : 749.124s

Choices      : 15373876 (Domain: 15012894)
Conflicts    : 668679   (Analyzed: 668676)
Restarts     : 8050     (Average: 83.07 Last: 185)
Model-Level  : 183.0   
Problems     : 85       (Average Length: 88.35 Splits: 0)
Lemmas       : 668676   (Deleted: 620912)
  Binary     : 13146    (Ratio:   1.97%)
  Ternary    : 5041     (Ratio:   0.75%)
  Conflict   : 668676   (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    : 668676   (Average: 20.69 Max: 1562 Sum: 13833507)
  Executed   : 668514   (Average: 20.68 Max: 1562 Sum: 13826875 Ratio:  99.95%)
  Bounded    : 162      (Average: 40.94 Max: 117 Sum:   6632 Ratio:   0.05%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 902908   (Eliminated:    0 Frozen: 278344)
Constraints  : 6624301  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 13.30s
Memory:		 975MB (+0MB)
UNKNOWN
Iteration Time:	 13.37s

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         : 763.386s (Solving: 727.61s 1st Model: 0.00s Unsat: 2.40s)
CPU Time     : 763.432s

Choices      : 15536270 (Domain: 15175157)
Conflicts    : 677036   (Analyzed: 677033)
Restarts     : 8150     (Average: 83.07 Last: 185)
Model-Level  : 183.0   
Problems     : 86       (Average Length: 88.69 Splits: 0)
Lemmas       : 677033   (Deleted: 628936)
  Binary     : 13199    (Ratio:   1.95%)
  Ternary    : 5046     (Ratio:   0.75%)
  Conflict   : 677033   (Average Length:  605.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 677033   (Average: 20.62 Max: 1562 Sum: 13957955)
  Executed   : 676871   (Average: 20.61 Max: 1562 Sum: 13951323 Ratio:  99.95%)
  Bounded    : 162      (Average: 40.94 Max: 117 Sum:   6632 Ratio:   0.05%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 902908   (Eliminated:    0 Frozen: 278344)
Constraints  : 6624301  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 14.24s
Memory:		 975MB (+0MB)
UNKNOWN
Iteration Time:	 14.31s

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         : 769.775s (Solving: 733.81s 1st Model: 0.00s Unsat: 2.40s)
CPU Time     : 769.828s

Choices      : 15591549 (Domain: 15230434)
Conflicts    : 684391   (Analyzed: 684388)
Restarts     : 8250     (Average: 82.96 Last: 185)
Model-Level  : 183.0   
Problems     : 87       (Average Length: 89.01 Splits: 0)
Lemmas       : 684388   (Deleted: 637148)
  Binary     : 13249    (Ratio:   1.94%)
  Ternary    : 5048     (Ratio:   0.74%)
  Conflict   : 684388   (Average Length:  601.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 684388   (Average: 20.44 Max: 1562 Sum: 13987653)
  Executed   : 684226   (Average: 20.43 Max: 1562 Sum: 13981021 Ratio:  99.95%)
  Bounded    : 162      (Average: 40.94 Max: 117 Sum:   6632 Ratio:   0.05%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 902908   (Eliminated:    0 Frozen: 278344)
Constraints  : 6624301  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 6.32s
Memory:		 975MB (+0MB)
UNKNOWN
Iteration Time:	 6.40s

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         : 773.674s (Solving: 737.53s 1st Model: 0.00s Unsat: 2.40s)
CPU Time     : 773.728s

Choices      : 15625291 (Domain: 15264176)
Conflicts    : 691658   (Analyzed: 691655)
Restarts     : 8350     (Average: 82.83 Last: 185)
Model-Level  : 183.0   
Problems     : 88       (Average Length: 89.33 Splits: 0)
Lemmas       : 691655   (Deleted: 644095)
  Binary     : 13256    (Ratio:   1.92%)
  Ternary    : 5049     (Ratio:   0.73%)
  Conflict   : 691655   (Average Length:  599.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 691655   (Average: 20.26 Max: 1562 Sum: 14012397)
  Executed   : 691493   (Average: 20.25 Max: 1562 Sum: 14005765 Ratio:  99.95%)
  Bounded    : 162      (Average: 40.94 Max: 117 Sum:   6632 Ratio:   0.05%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 902908   (Eliminated:    0 Frozen: 278344)
Constraints  : 6624301  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 3.84s
Memory:		 975MB (+0MB)
UNKNOWN
Iteration Time:	 3.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         : 783.702s (Solving: 747.38s 1st Model: 0.00s Unsat: 2.40s)
CPU Time     : 783.760s

Choices      : 15701115 (Domain: 15340000)
Conflicts    : 700133   (Analyzed: 700130)
Restarts     : 8450     (Average: 82.86 Last: 185)
Model-Level  : 183.0   
Problems     : 89       (Average Length: 89.64 Splits: 0)
Lemmas       : 700130   (Deleted: 651507)
  Binary     : 13411    (Ratio:   1.92%)
  Ternary    : 5069     (Ratio:   0.72%)
  Conflict   : 700130   (Average Length:  605.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 700130   (Average: 20.10 Max: 1562 Sum: 14069643)
  Executed   : 699968   (Average: 20.09 Max: 1562 Sum: 14063011 Ratio:  99.95%)
  Bounded    : 162      (Average: 40.94 Max: 117 Sum:   6632 Ratio:   0.05%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 902908   (Eliminated:    0 Frozen: 278344)
Constraints  : 6624301  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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         : 798.822s (Solving: 762.31s 1st Model: 0.00s Unsat: 2.40s)
CPU Time     : 798.888s

Choices      : 15834625 (Domain: 15472834)
Conflicts    : 708742   (Analyzed: 708739)
Restarts     : 8550     (Average: 82.89 Last: 185)
Model-Level  : 183.0   
Problems     : 90       (Average Length: 89.94 Splits: 0)
Lemmas       : 708739   (Deleted: 659396)
  Binary     : 13646    (Ratio:   1.93%)
  Ternary    : 5096     (Ratio:   0.72%)
  Conflict   : 708739   (Average Length:  620.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 708739   (Average: 20.00 Max: 1562 Sum: 14174053)
  Executed   : 708577   (Average: 19.99 Max: 1562 Sum: 14167421 Ratio:  99.95%)
  Bounded    : 162      (Average: 40.94 Max: 117 Sum:   6632 Ratio:   0.05%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 902908   (Eliminated:    0 Frozen: 278344)
Constraints  : 6624301  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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         : 810.135s (Solving: 773.44s 1st Model: 0.00s Unsat: 2.40s)
CPU Time     : 810.204s

Choices      : 16005985 (Domain: 15642429)
Conflicts    : 717486   (Analyzed: 717483)
Restarts     : 8650     (Average: 82.95 Last: 185)
Model-Level  : 183.0   
Problems     : 91       (Average Length: 90.24 Splits: 0)
Lemmas       : 717483   (Deleted: 669731)
  Binary     : 13747    (Ratio:   1.92%)
  Ternary    : 5143     (Ratio:   0.72%)
  Conflict   : 717483   (Average Length:  620.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 717483   (Average: 19.96 Max: 1562 Sum: 14324454)
  Executed   : 717321   (Average: 19.96 Max: 1562 Sum: 14317822 Ratio:  99.95%)
  Bounded    : 162      (Average: 40.94 Max: 117 Sum:   6632 Ratio:   0.05%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 902908   (Eliminated:    0 Frozen: 278344)
Constraints  : 6624301  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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         : 819.691s (Solving: 782.77s 1st Model: 0.00s Unsat: 2.40s)
CPU Time     : 819.764s

Choices      : 16161851 (Domain: 15797917)
Conflicts    : 725743   (Analyzed: 725740)
Restarts     : 8750     (Average: 82.94 Last: 185)
Model-Level  : 183.0   
Problems     : 92       (Average Length: 90.53 Splits: 0)
Lemmas       : 725740   (Deleted: 676141)
  Binary     : 13781    (Ratio:   1.90%)
  Ternary    : 5172     (Ratio:   0.71%)
  Conflict   : 725740   (Average Length:  621.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 725740   (Average: 19.92 Max: 1562 Sum: 14457524)
  Executed   : 725578   (Average: 19.91 Max: 1562 Sum: 14450892 Ratio:  99.95%)
  Bounded    : 162      (Average: 40.94 Max: 117 Sum:   6632 Ratio:   0.05%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 902908   (Eliminated:    0 Frozen: 278344)
Constraints  : 6624301  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 9.47s
Memory:		 975MB (+0MB)
UNKNOWN
Iteration Time:	 9.56s

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         : 826.658s (Solving: 789.53s 1st Model: 0.00s Unsat: 2.40s)
CPU Time     : 826.736s

Choices      : 16291240 (Domain: 15926314)
Conflicts    : 733422   (Analyzed: 733419)
Restarts     : 8850     (Average: 82.87 Last: 185)
Model-Level  : 183.0   
Problems     : 93       (Average Length: 90.82 Splits: 0)
Lemmas       : 733419   (Deleted: 684072)
  Binary     : 13809    (Ratio:   1.88%)
  Ternary    : 5182     (Ratio:   0.71%)
  Conflict   : 733419   (Average Length:  619.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 733419   (Average: 19.86 Max: 1562 Sum: 14566457)
  Executed   : 733257   (Average: 19.85 Max: 1562 Sum: 14559825 Ratio:  99.95%)
  Bounded    : 162      (Average: 40.94 Max: 117 Sum:   6632 Ratio:   0.05%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 902908   (Eliminated:    0 Frozen: 278344)
Constraints  : 6624301  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 6.89s
Memory:		 975MB (+0MB)
UNKNOWN
Iteration Time:	 6.97s

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         : 835.736s (Solving: 798.43s 1st Model: 0.00s Unsat: 2.40s)
CPU Time     : 835.808s

Choices      : 16464509 (Domain: 16099110)
Conflicts    : 741679   (Analyzed: 741676)
Restarts     : 8950     (Average: 82.87 Last: 185)
Model-Level  : 183.0   
Problems     : 94       (Average Length: 91.10 Splits: 0)
Lemmas       : 741676   (Deleted: 691616)
  Binary     : 13833    (Ratio:   1.87%)
  Ternary    : 5187     (Ratio:   0.70%)
  Conflict   : 741676   (Average Length:  620.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 741676   (Average: 19.84 Max: 1562 Sum: 14715303)
  Executed   : 741513   (Average: 19.83 Max: 1562 Sum: 14708554 Ratio:  99.95%)
  Bounded    : 163      (Average: 41.40 Max: 117 Sum:   6749 Ratio:   0.05%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 902908   (Eliminated:    0 Frozen: 278344)
Constraints  : 6624301  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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         : 843.746s (Solving: 806.25s 1st Model: 0.00s Unsat: 10.22s)
CPU Time     : 843.820s

Choices      : 16496702 (Domain: 16131303)
Conflicts    : 746118   (Analyzed: 746114)
Restarts     : 9002     (Average: 82.88 Last: 185)
Model-Level  : 183.0   
Problems     : 95       (Average Length: 91.37 Splits: 0)
Lemmas       : 746114   (Deleted: 696156)
  Binary     : 13909    (Ratio:   1.86%)
  Ternary    : 5196     (Ratio:   0.70%)
  Conflict   : 746114   (Average Length:  618.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 746114   (Average: 19.76 Max: 1562 Sum: 14746605)
  Executed   : 745949   (Average: 19.76 Max: 1562 Sum: 14739854 Ratio:  99.95%)
  Bounded    : 165      (Average: 40.92 Max: 117 Sum:   6751 Ratio:   0.05%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 902908   (Eliminated:    0 Frozen: 278344)
Constraints  : 6624275  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 7.94s
Memory:		 975MB (+0MB)
UNSAT
Iteration Time:	 8.02s

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         : 846.967s (Solving: 809.29s 1st Model: 0.00s Unsat: 10.22s)
CPU Time     : 847.044s

Choices      : 16532716 (Domain: 16167317)
Conflicts    : 753267   (Analyzed: 753263)
Restarts     : 9102     (Average: 82.76 Last: 185)
Model-Level  : 183.0   
Problems     : 96       (Average Length: 91.64 Splits: 0)
Lemmas       : 753263   (Deleted: 703244)
  Binary     : 13916    (Ratio:   1.85%)
  Ternary    : 5197     (Ratio:   0.69%)
  Conflict   : 753263   (Average Length:  615.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 753263   (Average: 19.61 Max: 1562 Sum: 14773887)
  Executed   : 753098   (Average: 19.60 Max: 1562 Sum: 14767136 Ratio:  99.95%)
  Bounded    : 165      (Average: 40.92 Max: 117 Sum:   6751 Ratio:   0.05%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 902908   (Eliminated:    0 Frozen: 278344)
Constraints  : 6624275  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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         : 860.534s (Solving: 822.67s 1st Model: 0.00s Unsat: 10.22s)
CPU Time     : 860.616s

Choices      : 16617579 (Domain: 16252173)
Conflicts    : 761752   (Analyzed: 761748)
Restarts     : 9202     (Average: 82.78 Last: 185)
Model-Level  : 183.0   
Problems     : 97       (Average Length: 91.90 Splits: 0)
Lemmas       : 761748   (Deleted: 710889)
  Binary     : 13978    (Ratio:   1.83%)
  Ternary    : 5219     (Ratio:   0.69%)
  Conflict   : 761748   (Average Length:  623.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 761748   (Average: 19.48 Max: 1562 Sum: 14839853)
  Executed   : 761583   (Average: 19.47 Max: 1562 Sum: 14833102 Ratio:  99.95%)
  Bounded    : 165      (Average: 40.92 Max: 117 Sum:   6751 Ratio:   0.05%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 902908   (Eliminated:    0 Frozen: 278344)
Constraints  : 6624275  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 13.50s
Memory:		 975MB (+0MB)
UNKNOWN
Iteration Time:	 13.57s

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         : 866.128s (Solving: 828.05s 1st Model: 0.00s Unsat: 10.22s)
CPU Time     : 866.212s

Choices      : 16671064 (Domain: 16305658)
Conflicts    : 769396   (Analyzed: 769392)
Restarts     : 9302     (Average: 82.71 Last: 185)
Model-Level  : 183.0   
Problems     : 98       (Average Length: 92.15 Splits: 0)
Lemmas       : 769392   (Deleted: 719004)
  Binary     : 13992    (Ratio:   1.82%)
  Ternary    : 5225     (Ratio:   0.68%)
  Conflict   : 769392   (Average Length:  621.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 769392   (Average: 19.34 Max: 1562 Sum: 14878825)
  Executed   : 769227   (Average: 19.33 Max: 1562 Sum: 14872074 Ratio:  99.95%)
  Bounded    : 165      (Average: 40.92 Max: 117 Sum:   6751 Ratio:   0.05%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 902908   (Eliminated:    0 Frozen: 278344)
Constraints  : 6624275  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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         : 874.300s (Solving: 836.02s 1st Model: 0.00s Unsat: 10.22s)
CPU Time     : 874.388s

Choices      : 16771158 (Domain: 16405189)
Conflicts    : 777657   (Analyzed: 777653)
Restarts     : 9402     (Average: 82.71 Last: 185)
Model-Level  : 183.0   
Problems     : 99       (Average Length: 92.40 Splits: 0)
Lemmas       : 777653   (Deleted: 726455)
  Binary     : 14083    (Ratio:   1.81%)
  Ternary    : 5235     (Ratio:   0.67%)
  Conflict   : 777653   (Average Length:  621.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 777653   (Average: 19.23 Max: 1562 Sum: 14957932)
  Executed   : 777488   (Average: 19.23 Max: 1562 Sum: 14951181 Ratio:  99.95%)
  Bounded    : 165      (Average: 40.92 Max: 117 Sum:   6751 Ratio:   0.05%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 902908   (Eliminated:    0 Frozen: 278344)
Constraints  : 6624275  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

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

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         : 888.923s (Solving: 850.46s 1st Model: 0.00s Unsat: 10.22s)
CPU Time     : 889.016s

Choices      : 16945498 (Domain: 16578149)
Conflicts    : 786145   (Analyzed: 786141)
Restarts     : 9502     (Average: 82.73 Last: 185)
Model-Level  : 183.0   
Problems     : 100      (Average Length: 92.65 Splits: 0)
Lemmas       : 786141   (Deleted: 734313)
  Binary     : 14299    (Ratio:   1.82%)
  Ternary    : 5281     (Ratio:   0.67%)
  Conflict   : 786141   (Average Length:  624.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 786141   (Average: 19.21 Max: 1562 Sum: 15101934)
  Executed   : 785976   (Average: 19.20 Max: 1562 Sum: 15095183 Ratio:  99.96%)
  Bounded    : 165      (Average: 40.92 Max: 117 Sum:   6751 Ratio:   0.04%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 902908   (Eliminated:    0 Frozen: 278344)
Constraints  : 6624275  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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

[endof: stats after solve call]
Solving Time:	 14.56s
Memory:		 975MB (+0MB)
UNKNOWN
Iteration Time:	 14.63s

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

INTERRUPTED  : 1

Models       : 0+
Calls        : 101
Time         : 892.583s (Solving: 853.91s 1st Model: 0.00s Unsat: 10.22s)
CPU Time     : 892.652s

Choices      : 16998304 (Domain: 16630745)
Conflicts    : 788629   (Analyzed: 788625)
Restarts     : 9529     (Average: 82.76 Last: 185)
Model-Level  : 183.0   
Problems     : 101      (Average Length: 92.89 Splits: 0)
Lemmas       : 788625   (Deleted: 738218)
  Binary     : 14320    (Ratio:   1.82%)
  Ternary    : 5287     (Ratio:   0.67%)
  Conflict   : 788625   (Average Length:  624.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 788625   (Average: 19.21 Max: 1562 Sum: 15147547)
  Executed   : 788460   (Average: 19.20 Max: 1562 Sum: 15140796 Ratio:  99.96%)
  Bounded    : 165      (Average: 40.92 Max: 117 Sum:   6751 Ratio:   0.04%)

Rules        : 91724    (Original: 89679)
Atoms        : 73746   
Bodies       : 16519    (Original: 14473)
  Count      : 330      (Original: 739)
Equivalences : 4525     (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight        : Yes
Variables    : 902908   (Eliminated:    0 Frozen: 278344)
Constraints  : 6624275  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

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


