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-7.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-7.pddl
Parsing...
Parsing: [0.040s CPU, 0.041s wall-clock]
Normalizing task... [0.000s CPU, 0.003s wall-clock]
Instantiating...
Generating Datalog program... [0.010s CPU, 0.010s wall-clock]
Normalizing Datalog program...
Normalizing Datalog program: [0.050s CPU, 0.052s wall-clock]
Preparing model... [0.030s CPU, 0.026s wall-clock]
Generated 115 rules.
Computing model... [0.370s CPU, 0.374s wall-clock]
2300 relevant atoms
2393 auxiliary atoms
4693 final queue length
8087 total queue pushes
Completing instantiation... [0.690s CPU, 0.687s wall-clock]
Instantiating: [1.150s CPU, 1.155s wall-clock]
Computing fact groups...
Finding invariants...
24 initial candidates
Finding invariants: [0.120s CPU, 0.117s wall-clock]
Checking invariant weight... [0.000s CPU, 0.001s wall-clock]
Instantiating groups... [0.010s CPU, 0.007s wall-clock]
Collecting mutex groups... [0.000s CPU, 0.001s wall-clock]
Choosing groups...
238 uncovered facts
Choosing groups: [0.000s CPU, 0.001s wall-clock]
Building translation key... [0.000s CPU, 0.009s wall-clock]
Computing fact groups: [0.150s CPU, 0.152s wall-clock]
Building STRIPS to SAS dictionary... [0.000s CPU, 0.002s wall-clock]
Building dictionary for full mutex groups... [0.010s CPU, 0.002s wall-clock]
Building mutex information...
Building mutex information: [0.000s CPU, 0.003s wall-clock]
Translating task...
Processing axioms...
Simplifying axioms... [0.000s CPU, 0.000s wall-clock]
Processing axioms: [0.040s CPU, 0.040s wall-clock]
Translating task: [0.730s CPU, 0.725s wall-clock]
2672 effect conditions simplified
0 implied preconditions added
Detecting unreachable propositions...
0 operators removed
0 axioms removed
3 propositions removed
Detecting unreachable propositions: [0.350s CPU, 0.356s wall-clock]
Reordering and filtering variables...
241 of 241 variables necessary.
12 of 15 mutex groups necessary.
1596 of 1596 operators necessary.
0 of 0 axiom rules necessary.
Reordering and filtering variables: [0.250s CPU, 0.241s wall-clock]
Translator variables: 241
Translator derived variables: 0
Translator facts: 505
Translator goal facts: 10
Translator mutex groups: 12
Translator total mutex groups size: 36
Translator operators: 1596
Translator axioms: 0
Translator task size: 15302
Translator peak memory: 45260 KB
Writing output... [0.260s CPU, 0.277s wall-clock]
Done! [2.960s CPU, 2.986s wall-clock]
planner.py version 0.0.1

Time:	 0.61s
Memory: 91MB

Iteration 1
Queue:		 [(0,115,0,True)]
Grounded Until:	 0
Expected Memory: 91MB
Grounding...	 [('step', [1]), ('step', [2]), ('step', [3]), ('step', [4]), ('step', [5]), ('step', [6]), ('step', [7]), ('step', [8]), ('step', [9]), ('step', [10]), ('step', [11]), ('step', [12]), ('step', [13]), ('step', [14]), ('step', [15]), ('step', [16]), ('step', [17]), ('step', [18]), ('step', [19]), ('step', [20]), ('step', [21]), ('step', [22]), ('step', [23]), ('step', [24]), ('step', [25]), ('step', [26]), ('step', [27]), ('step', [28]), ('step', [29]), ('step', [30]), ('step', [31]), ('step', [32]), ('step', [33]), ('step', [34]), ('step', [35]), ('step', [36]), ('step', [37]), ('step', [38]), ('step', [39]), ('step', [40]), ('step', [41]), ('step', [42]), ('step', [43]), ('step', [44]), ('step', [45]), ('step', [46]), ('step', [47]), ('step', [48]), ('step', [49]), ('step', [50]), ('step', [51]), ('step', [52]), ('step', [53]), ('step', [54]), ('step', [55]), ('step', [56]), ('step', [57]), ('step', [58]), ('step', [59]), ('step', [60]), ('step', [61]), ('step', [62]), ('step', [63]), ('step', [64]), ('step', [65]), ('step', [66]), ('step', [67]), ('step', [68]), ('step', [69]), ('step', [70]), ('step', [71]), ('step', [72]), ('step', [73]), ('step', [74]), ('step', [75]), ('step', [76]), ('step', [77]), ('step', [78]), ('step', [79]), ('step', [80]), ('step', [81]), ('step', [82]), ('step', [83]), ('step', [84]), ('step', [85]), ('step', [86]), ('step', [87]), ('step', [88]), ('step', [89]), ('step', [90]), ('step', [91]), ('step', [92]), ('step', [93]), ('step', [94]), ('step', [95]), ('step', [96]), ('step', [97]), ('step', [98]), ('step', [99]), ('step', [100]), ('step', [101]), ('step', [102]), ('step', [103]), ('step', [104]), ('step', [105]), ('step', [106]), ('step', [107]), ('step', [108]), ('step', [109]), ('step', [110]), ('step', [111]), ('step', [112]), ('step', [113]), ('step', [114]), ('step', [115]), ('check', [115])]
Grounding Time:	 5.31s
Memory:		 572MB (+481MB)
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 1+
Calls        : 1
Time         : 9.213s (Solving: 0.13s 1st Model: 0.11s Unsat: 0.00s)
CPU Time     : 9.112s

Choices      : 21092    (Domain: 20732)
Conflicts    : 67       (Analyzed: 67)
Restarts     : 0       
Model-Level  : 4372.0  
Problems     : 1        (Average Length: 117.00 Splits: 0)
Lemmas       : 67       (Deleted: 0)
  Binary     : 15       (Ratio:  22.39%)
  Ternary    : 0        (Ratio:   0.00%)
  Conflict   : 67       (Average Length:   47.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 67       (Average: 251.30 Max: 1731 Sum:  16837)
  Executed   : 67       (Average: 251.30 Max: 1731 Sum:  16837 Ratio: 100.00%)
  Bounded    : 0        (Average:  0.00 Max:   0 Sum:      0 Ratio:   0.00%)

Rules        : 0       
Atoms        : 0       
Bodies       : 0       
Tight        : Yes
Variables    : 322038   (Eliminated:    0 Frozen: 2990)
Constraints  : 2575755  (Binary:  95.7% Ternary:   3.2% Other:   1.1%)

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

[endof: stats after solve call]
Solving Time:	 0.35s
Memory:		 752MB (+180MB)
SAT
Testing...
NOT SERIALIZABLE
Testing Time:	 2.79s
Memory:		 765MB (+13MB)
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 2
Time         : 35.326s (Solving: 23.14s 1st Model: 0.11s Unsat: 0.00s)
CPU Time     : 35.236s

Choices      : 2048966  (Domain: 2018629)
Conflicts    : 24887    (Analyzed: 24887)
Restarts     : 100      (Average: 248.87 Last: 191)
Model-Level  : 4372.0  
Problems     : 2        (Average Length: 117.00 Splits: 0)
Lemmas       : 24887    (Deleted: 19122)
  Binary     : 1894     (Ratio:   7.61%)
  Ternary    : 557      (Ratio:   2.24%)
  Conflict   : 24887    (Average Length:  326.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 24887    (Average: 81.42 Max: 1731 Sum: 2026194)
  Executed   : 24853    (Average: 81.26 Max: 1731 Sum: 2022241 Ratio:  99.80%)
  Bounded    : 34       (Average: 116.26 Max: 117 Sum:   3953 Ratio:   0.20%)

Rules        : 1028283  (Original: 843628)
Atoms        : 59257   
Bodies       : 791604   (Original: 606949)
  Count      : 9712     (Original: 27041)
Equivalences : 188391   (Atom=Atom: 172 Body=Body: 0 Other: 188219)
Tight        : Yes
Variables    : 578090   (Eliminated:    0 Frozen: 191082)
Constraints  : 4249774  (Binary:  91.4% Ternary:   7.1% Other:   1.5%)

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

[endof: stats after solve call]
Solving Time:	 24.00s
Memory:		 872MB (+107MB)
UNKNOWN
Iteration Time:	 35.34s

Iteration 2
Queue:		 [(0,115,1,True)]
Grounded Until:	 115
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 3
Time         : 60.556s (Solving: 48.23s 1st Model: 0.11s Unsat: 0.00s)
CPU Time     : 60.476s

Choices      : 3872517  (Domain: 3816021)
Conflicts    : 51173    (Analyzed: 51173)
Restarts     : 200      (Average: 255.87 Last: 325)
Model-Level  : 4372.0  
Problems     : 3        (Average Length: 117.00 Splits: 0)
Lemmas       : 51173    (Deleted: 40835)
  Binary     : 3546     (Ratio:   6.93%)
  Ternary    : 967      (Ratio:   1.89%)
  Conflict   : 51173    (Average Length:  306.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 51173    (Average: 74.73 Max: 1786 Sum: 3824095)
  Executed   : 51131    (Average: 74.63 Max: 1786 Sum: 3819223 Ratio:  99.87%)
  Bounded    : 42       (Average: 116.00 Max: 117 Sum:   4872 Ratio:   0.13%)

Rules        : 1028283  (Original: 843628)
Atoms        : 59257   
Bodies       : 791604   (Original: 606949)
  Count      : 9712     (Original: 27041)
Equivalences : 188391   (Atom=Atom: 172 Body=Body: 0 Other: 188219)
Tight        : Yes
Variables    : 578090   (Eliminated:    0 Frozen: 191082)
Constraints  : 4207579  (Binary:  91.4% Ternary:   7.1% Other:   1.6%)

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

[endof: stats after solve call]
Solving Time:	 25.24s
Memory:		 875MB (+3MB)
UNKNOWN
Iteration Time:	 25.24s

Iteration 3
Queue:		 [(0,115,2,True)]
Grounded Until:	 115
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 4
Time         : 78.821s (Solving: 66.40s 1st Model: 0.11s Unsat: 0.00s)
CPU Time     : 78.748s

Choices      : 4511056  (Domain: 4451872)
Conflicts    : 76087    (Analyzed: 76087)
Restarts     : 300      (Average: 253.62 Last: 325)
Model-Level  : 4372.0  
Problems     : 4        (Average Length: 117.00 Splits: 0)
Lemmas       : 76087    (Deleted: 63602)
  Binary     : 4163     (Ratio:   5.47%)
  Ternary    : 1077     (Ratio:   1.42%)
  Conflict   : 76087    (Average Length:  295.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 76087    (Average: 58.46 Max: 1786 Sum: 4448159)
  Executed   : 76039    (Average: 58.39 Max: 1786 Sum: 4442600 Ratio:  99.88%)
  Bounded    : 48       (Average: 115.81 Max: 117 Sum:   5559 Ratio:   0.12%)

Rules        : 1028283  (Original: 843628)
Atoms        : 59257   
Bodies       : 791604   (Original: 606949)
  Count      : 9712     (Original: 27041)
Equivalences : 188391   (Atom=Atom: 172 Body=Body: 0 Other: 188219)
Tight        : Yes
Variables    : 578090   (Eliminated:    0 Frozen: 191082)
Constraints  : 4207523  (Binary:  91.4% Ternary:   7.1% Other:   1.6%)

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

[endof: stats after solve call]
Solving Time:	 18.28s
Memory:		 875MB (+0MB)
UNKNOWN
Iteration Time:	 18.28s

Iteration 4
Queue:		 [(0,115,3,True)]
Grounded Until:	 115
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 5
Time         : 100.912s (Solving: 88.38s 1st Model: 0.11s Unsat: 0.00s)
CPU Time     : 100.848s

Choices      : 5900171  (Domain: 5832014)
Conflicts    : 102155   (Analyzed: 102155)
Restarts     : 400      (Average: 255.39 Last: 325)
Model-Level  : 4372.0  
Problems     : 5        (Average Length: 117.00 Splits: 0)
Lemmas       : 102155   (Deleted: 86695)
  Binary     : 5112     (Ratio:   5.00%)
  Ternary    : 1234     (Ratio:   1.21%)
  Conflict   : 102155   (Average Length:  349.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 102155   (Average: 56.91 Max: 1786 Sum: 5814040)
  Executed   : 102102   (Average: 56.85 Max: 1786 Sum: 5807905 Ratio:  99.89%)
  Bounded    : 53       (Average: 115.75 Max: 117 Sum:   6135 Ratio:   0.11%)

Rules        : 1028283  (Original: 843628)
Atoms        : 59257   
Bodies       : 791604   (Original: 606949)
  Count      : 9712     (Original: 27041)
Equivalences : 188391   (Atom=Atom: 172 Body=Body: 0 Other: 188219)
Tight        : Yes
Variables    : 578090   (Eliminated:    0 Frozen: 191082)
Constraints  : 4201702  (Binary:  91.4% Ternary:   7.1% Other:   1.6%)

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

[endof: stats after solve call]
Solving Time:	 22.10s
Memory:		 875MB (+0MB)
UNKNOWN
Iteration Time:	 22.10s

Iteration 5
Queue:		 [(0,115,4,True)]
Grounded Until:	 115
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 6
Time         : 121.772s (Solving: 109.12s 1st Model: 0.11s Unsat: 0.00s)
CPU Time     : 121.716s

Choices      : 7050553  (Domain: 6975388)
Conflicts    : 128140   (Analyzed: 128140)
Restarts     : 500      (Average: 256.28 Last: 325)
Model-Level  : 4372.0  
Problems     : 6        (Average Length: 117.00 Splits: 0)
Lemmas       : 128140   (Deleted: 113807)
  Binary     : 5766     (Ratio:   4.50%)
  Ternary    : 1295     (Ratio:   1.01%)
  Conflict   : 128140   (Average Length:  452.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 128140   (Average: 54.16 Max: 1786 Sum: 6940222)
  Executed   : 128085   (Average: 54.11 Max: 1786 Sum: 6933860 Ratio:  99.91%)
  Bounded    : 55       (Average: 115.67 Max: 117 Sum:   6362 Ratio:   0.09%)

Rules        : 1028283  (Original: 843628)
Atoms        : 59257   
Bodies       : 791604   (Original: 606949)
  Count      : 9712     (Original: 27041)
Equivalences : 188391   (Atom=Atom: 172 Body=Body: 0 Other: 188219)
Tight        : Yes
Variables    : 578090   (Eliminated:    0 Frozen: 191082)
Constraints  : 4201661  (Binary:  91.4% Ternary:   7.1% Other:   1.6%)

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

[endof: stats after solve call]
Solving Time:	 20.87s
Memory:		 875MB (+0MB)
UNKNOWN
Iteration Time:	 20.87s

Iteration 6
Queue:		 [(0,115,5,True)]
Grounded Until:	 115
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 7
Time         : 145.498s (Solving: 132.72s 1st Model: 0.11s Unsat: 0.00s)
CPU Time     : 145.452s

Choices      : 8489902  (Domain: 8406773)
Conflicts    : 154622   (Analyzed: 154622)
Restarts     : 600      (Average: 257.70 Last: 325)
Model-Level  : 4372.0  
Problems     : 7        (Average Length: 117.00 Splits: 0)
Lemmas       : 154622   (Deleted: 135874)
  Binary     : 6316     (Ratio:   4.08%)
  Ternary    : 1344     (Ratio:   0.87%)
  Conflict   : 154622   (Average Length:  520.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 154622   (Average: 54.02 Max: 1786 Sum: 8353059)
  Executed   : 154565   (Average: 53.98 Max: 1786 Sum: 8346468 Ratio:  99.92%)
  Bounded    : 57       (Average: 115.63 Max: 117 Sum:   6591 Ratio:   0.08%)

Rules        : 1028283  (Original: 843628)
Atoms        : 59257   
Bodies       : 791604   (Original: 606949)
  Count      : 9712     (Original: 27041)
Equivalences : 188391   (Atom=Atom: 172 Body=Body: 0 Other: 188219)
Tight        : Yes
Variables    : 578090   (Eliminated:    0 Frozen: 191082)
Constraints  : 4201661  (Binary:  91.4% Ternary:   7.1% Other:   1.6%)

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

[endof: stats after solve call]
Solving Time:	 23.74s
Memory:		 875MB (+0MB)
UNKNOWN
Iteration Time:	 23.74s

Iteration 7
Queue:		 [(0,115,6,True)]
Grounded Until:	 115
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 8
Time         : 166.501s (Solving: 153.61s 1st Model: 0.11s Unsat: 0.00s)
CPU Time     : 166.464s

Choices      : 9706875  (Domain: 9618258)
Conflicts    : 180223   (Analyzed: 180223)
Restarts     : 700      (Average: 257.46 Last: 325)
Model-Level  : 4372.0  
Problems     : 8        (Average Length: 117.00 Splits: 0)
Lemmas       : 180223   (Deleted: 161738)
  Binary     : 6797     (Ratio:   3.77%)
  Ternary    : 1400     (Ratio:   0.78%)
  Conflict   : 180223   (Average Length:  558.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 180223   (Average: 52.96 Max: 1786 Sum: 9545229)
  Executed   : 180165   (Average: 52.93 Max: 1786 Sum: 9538522 Ratio:  99.93%)
  Bounded    : 58       (Average: 115.64 Max: 117 Sum:   6707 Ratio:   0.07%)

Rules        : 1028283  (Original: 843628)
Atoms        : 59257   
Bodies       : 791604   (Original: 606949)
  Count      : 9712     (Original: 27041)
Equivalences : 188391   (Atom=Atom: 172 Body=Body: 0 Other: 188219)
Tight        : Yes
Variables    : 578090   (Eliminated:    0 Frozen: 191082)
Constraints  : 4201647  (Binary:  91.4% Ternary:   7.1% Other:   1.6%)

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

[endof: stats after solve call]
Solving Time:	 21.01s
Memory:		 875MB (+0MB)
UNKNOWN
Iteration Time:	 21.01s

Iteration 8
Queue:		 [(0,115,7,True)]
Grounded Until:	 115
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 9
Time         : 187.845s (Solving: 174.84s 1st Model: 0.11s Unsat: 0.00s)
CPU Time     : 187.816s

Choices      : 10959778 (Domain: 10864511)
Conflicts    : 206844   (Analyzed: 206844)
Restarts     : 800      (Average: 258.56 Last: 325)
Model-Level  : 4372.0  
Problems     : 9        (Average Length: 117.00 Splits: 0)
Lemmas       : 206844   (Deleted: 186023)
  Binary     : 7209     (Ratio:   3.49%)
  Ternary    : 1470     (Ratio:   0.71%)
  Conflict   : 206844   (Average Length:  591.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 206844   (Average: 52.07 Max: 1786 Sum: 10770502)
  Executed   : 206786   (Average: 52.04 Max: 1786 Sum: 10763795 Ratio:  99.94%)
  Bounded    : 58       (Average: 115.64 Max: 117 Sum:   6707 Ratio:   0.06%)

Rules        : 1028283  (Original: 843628)
Atoms        : 59257   
Bodies       : 791604   (Original: 606949)
  Count      : 9712     (Original: 27041)
Equivalences : 188391   (Atom=Atom: 172 Body=Body: 0 Other: 188219)
Tight        : Yes
Variables    : 578090   (Eliminated:    0 Frozen: 191082)
Constraints  : 4201647  (Binary:  91.4% Ternary:   7.1% Other:   1.6%)

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

[endof: stats after solve call]
Solving Time:	 21.36s
Memory:		 875MB (+0MB)
UNKNOWN
Iteration Time:	 21.36s

Iteration 9
Queue:		 [(0,115,8,True)]
Grounded Until:	 115
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 10
Time         : 212.388s (Solving: 199.26s 1st Model: 0.11s Unsat: 0.00s)
CPU Time     : 212.368s

Choices      : 12421955 (Domain: 12315304)
Conflicts    : 234047   (Analyzed: 234047)
Restarts     : 900      (Average: 260.05 Last: 325)
Model-Level  : 4372.0  
Problems     : 10       (Average Length: 117.00 Splits: 0)
Lemmas       : 234047   (Deleted: 210236)
  Binary     : 8240     (Ratio:   3.52%)
  Ternary    : 1663     (Ratio:   0.71%)
  Conflict   : 234047   (Average Length:  635.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 234047   (Average: 52.12 Max: 1786 Sum: 12199350)
  Executed   : 233989   (Average: 52.09 Max: 1786 Sum: 12192643 Ratio:  99.95%)
  Bounded    : 58       (Average: 115.64 Max: 117 Sum:   6707 Ratio:   0.05%)

Rules        : 1028283  (Original: 843628)
Atoms        : 59257   
Bodies       : 791604   (Original: 606949)
  Count      : 9712     (Original: 27041)
Equivalences : 188391   (Atom=Atom: 172 Body=Body: 0 Other: 188219)
Tight        : Yes
Variables    : 578090   (Eliminated:    0 Frozen: 191082)
Constraints  : 4201647  (Binary:  91.4% Ternary:   7.1% Other:   1.6%)

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

[endof: stats after solve call]
Solving Time:	 24.56s
Memory:		 875MB (+0MB)
UNKNOWN
Iteration Time:	 24.56s

Iteration 10
Queue:		 [(0,115,9,True)]
Grounded Until:	 115
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 11
Time         : 235.434s (Solving: 222.18s 1st Model: 0.11s Unsat: 0.00s)
CPU Time     : 235.424s

Choices      : 13783875 (Domain: 13670603)
Conflicts    : 260263   (Analyzed: 260263)
Restarts     : 1000     (Average: 260.26 Last: 325)
Model-Level  : 4372.0  
Problems     : 11       (Average Length: 117.00 Splits: 0)
Lemmas       : 260263   (Deleted: 235996)
  Binary     : 8858     (Ratio:   3.40%)
  Ternary    : 1738     (Ratio:   0.67%)
  Conflict   : 260263   (Average Length:  643.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 260263   (Average: 51.99 Max: 1786 Sum: 13530807)
  Executed   : 260205   (Average: 51.96 Max: 1786 Sum: 13524100 Ratio:  99.95%)
  Bounded    : 58       (Average: 115.64 Max: 117 Sum:   6707 Ratio:   0.05%)

Rules        : 1028283  (Original: 843628)
Atoms        : 59257   
Bodies       : 791604   (Original: 606949)
  Count      : 9712     (Original: 27041)
Equivalences : 188391   (Atom=Atom: 172 Body=Body: 0 Other: 188219)
Tight        : Yes
Variables    : 578090   (Eliminated:    0 Frozen: 191082)
Constraints  : 4201647  (Binary:  91.4% Ternary:   7.1% Other:   1.6%)

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

[endof: stats after solve call]
Solving Time:	 23.06s
Memory:		 875MB (+0MB)
UNKNOWN
Iteration Time:	 23.06s

Iteration 11
Queue:		 [(0,115,10,True)]
Grounded Until:	 115
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 12
Time         : 259.698s (Solving: 246.34s 1st Model: 0.11s Unsat: 0.00s)
CPU Time     : 259.696s

Choices      : 14913066 (Domain: 14795788)
Conflicts    : 285329   (Analyzed: 285329)
Restarts     : 1100     (Average: 259.39 Last: 325)
Model-Level  : 4372.0  
Problems     : 12       (Average Length: 117.00 Splits: 0)
Lemmas       : 285329   (Deleted: 260059)
  Binary     : 9956     (Ratio:   3.49%)
  Ternary    : 1947     (Ratio:   0.68%)
  Conflict   : 285329   (Average Length:  677.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 285329   (Average: 51.26 Max: 1786 Sum: 14625644)
  Executed   : 285271   (Average: 51.24 Max: 1786 Sum: 14618937 Ratio:  99.95%)
  Bounded    : 58       (Average: 115.64 Max: 117 Sum:   6707 Ratio:   0.05%)

Rules        : 1028283  (Original: 843628)
Atoms        : 59257   
Bodies       : 791604   (Original: 606949)
  Count      : 9712     (Original: 27041)
Equivalences : 188391   (Atom=Atom: 172 Body=Body: 0 Other: 188219)
Tight        : Yes
Variables    : 578090   (Eliminated:    0 Frozen: 191082)
Constraints  : 4201647  (Binary:  91.4% Ternary:   7.1% Other:   1.6%)

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

[endof: stats after solve call]
Solving Time:	 24.28s
Memory:		 939MB (+64MB)
UNKNOWN
Iteration Time:	 24.28s

Iteration 12
Queue:		 [(0,115,11,True)]
Grounded Until:	 115
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 13
Time         : 285.601s (Solving: 272.15s 1st Model: 0.11s Unsat: 0.00s)
CPU Time     : 285.612s

Choices      : 15585244 (Domain: 15467219)
Conflicts    : 314350   (Analyzed: 314350)
Restarts     : 1200     (Average: 261.96 Last: 325)
Model-Level  : 4372.0  
Problems     : 13       (Average Length: 117.00 Splits: 0)
Lemmas       : 314350   (Deleted: 286524)
  Binary     : 10677    (Ratio:   3.40%)
  Ternary    : 2113     (Ratio:   0.67%)
  Conflict   : 314350   (Average Length:  704.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 314350   (Average: 48.56 Max: 1786 Sum: 15264949)
  Executed   : 314292   (Average: 48.54 Max: 1786 Sum: 15258242 Ratio:  99.96%)
  Bounded    : 58       (Average: 115.64 Max: 117 Sum:   6707 Ratio:   0.04%)

Rules        : 1028283  (Original: 843628)
Atoms        : 59257   
Bodies       : 791604   (Original: 606949)
  Count      : 9712     (Original: 27041)
Equivalences : 188391   (Atom=Atom: 172 Body=Body: 0 Other: 188219)
Tight        : Yes
Variables    : 578090   (Eliminated:    0 Frozen: 191082)
Constraints  : 4201647  (Binary:  91.4% Ternary:   7.1% Other:   1.6%)

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

[endof: stats after solve call]
Solving Time:	 25.92s
Memory:		 939MB (+0MB)
UNKNOWN
Iteration Time:	 25.92s

Iteration 13
Queue:		 [(0,115,12,True)]
Grounded Until:	 115
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 14
Time         : 310.394s (Solving: 296.82s 1st Model: 0.11s Unsat: 0.00s)
CPU Time     : 310.416s

Choices      : 16324755 (Domain: 16205525)
Conflicts    : 343275   (Analyzed: 343275)
Restarts     : 1300     (Average: 264.06 Last: 325)
Model-Level  : 4372.0  
Problems     : 14       (Average Length: 117.00 Splits: 0)
Lemmas       : 343275   (Deleted: 313472)
  Binary     : 11623    (Ratio:   3.39%)
  Ternary    : 2287     (Ratio:   0.67%)
  Conflict   : 343275   (Average Length:  731.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 343275   (Average: 46.50 Max: 1786 Sum: 15963772)
  Executed   : 343217   (Average: 46.48 Max: 1786 Sum: 15957065 Ratio:  99.96%)
  Bounded    : 58       (Average: 115.64 Max: 117 Sum:   6707 Ratio:   0.04%)

Rules        : 1028283  (Original: 843628)
Atoms        : 59257   
Bodies       : 791604   (Original: 606949)
  Count      : 9712     (Original: 27041)
Equivalences : 188391   (Atom=Atom: 172 Body=Body: 0 Other: 188219)
Tight        : Yes
Variables    : 578090   (Eliminated:    0 Frozen: 191082)
Constraints  : 4201647  (Binary:  91.4% Ternary:   7.1% Other:   1.6%)

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

[endof: stats after solve call]
Solving Time:	 24.81s
Memory:		 939MB (+0MB)
UNKNOWN
Iteration Time:	 24.81s

Iteration 14
Queue:		 [(0,115,13,True)]
Grounded Until:	 115
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 15
Time         : 333.377s (Solving: 319.68s 1st Model: 0.11s Unsat: 0.00s)
CPU Time     : 333.408s

Choices      : 16838907 (Domain: 16718886)
Conflicts    : 370547   (Analyzed: 370547)
Restarts     : 1400     (Average: 264.68 Last: 325)
Model-Level  : 4372.0  
Problems     : 15       (Average Length: 117.00 Splits: 0)
Lemmas       : 370547   (Deleted: 338590)
  Binary     : 12054    (Ratio:   3.25%)
  Ternary    : 2361     (Ratio:   0.64%)
  Conflict   : 370547   (Average Length:  743.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 370547   (Average: 44.38 Max: 1786 Sum: 16443188)
  Executed   : 370489   (Average: 44.36 Max: 1786 Sum: 16436481 Ratio:  99.96%)
  Bounded    : 58       (Average: 115.64 Max: 117 Sum:   6707 Ratio:   0.04%)

Rules        : 1028283  (Original: 843628)
Atoms        : 59257   
Bodies       : 791604   (Original: 606949)
  Count      : 9712     (Original: 27041)
Equivalences : 188391   (Atom=Atom: 172 Body=Body: 0 Other: 188219)
Tight        : Yes
Variables    : 578090   (Eliminated:    0 Frozen: 191082)
Constraints  : 4201647  (Binary:  91.4% Ternary:   7.1% Other:   1.6%)

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

[endof: stats after solve call]
Solving Time:	 23.00s
Memory:		 939MB (+0MB)
UNKNOWN
Iteration Time:	 23.00s

Iteration 15
Queue:		 [(0,115,14,True)]
Grounded Until:	 115
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 16
Time         : 357.105s (Solving: 343.27s 1st Model: 0.11s Unsat: 0.00s)
CPU Time     : 357.148s

Choices      : 17484833 (Domain: 17362930)
Conflicts    : 400960   (Analyzed: 400960)
Restarts     : 1500     (Average: 267.31 Last: 325)
Model-Level  : 4372.0  
Problems     : 16       (Average Length: 117.00 Splits: 0)
Lemmas       : 400960   (Deleted: 367039)
  Binary     : 12857    (Ratio:   3.21%)
  Ternary    : 2521     (Ratio:   0.63%)
  Conflict   : 400960   (Average Length:  766.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 400960   (Average: 42.50 Max: 1786 Sum: 17042678)
  Executed   : 400902   (Average: 42.49 Max: 1786 Sum: 17035971 Ratio:  99.96%)
  Bounded    : 58       (Average: 115.64 Max: 117 Sum:   6707 Ratio:   0.04%)

Rules        : 1028283  (Original: 843628)
Atoms        : 59257   
Bodies       : 791604   (Original: 606949)
  Count      : 9712     (Original: 27041)
Equivalences : 188391   (Atom=Atom: 172 Body=Body: 0 Other: 188219)
Tight        : Yes
Variables    : 578090   (Eliminated:    0 Frozen: 191082)
Constraints  : 4201647  (Binary:  91.4% Ternary:   7.1% Other:   1.6%)

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

[endof: stats after solve call]
Solving Time:	 23.74s
Memory:		 939MB (+0MB)
UNKNOWN
Iteration Time:	 23.74s

Iteration 16
Queue:		 [(0,115,15,True)]
Grounded Until:	 115
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 17
Time         : 379.318s (Solving: 365.38s 1st Model: 0.11s Unsat: 0.00s)
CPU Time     : 379.368s

Choices      : 17981886 (Domain: 17859175)
Conflicts    : 428497   (Analyzed: 428497)
Restarts     : 1600     (Average: 267.81 Last: 325)
Model-Level  : 4372.0  
Problems     : 17       (Average Length: 117.00 Splits: 0)
Lemmas       : 428497   (Deleted: 393449)
  Binary     : 13283    (Ratio:   3.10%)
  Ternary    : 2579     (Ratio:   0.60%)
  Conflict   : 428497   (Average Length:  773.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 428497   (Average: 40.85 Max: 1786 Sum: 17502949)
  Executed   : 428439   (Average: 40.83 Max: 1786 Sum: 17496242 Ratio:  99.96%)
  Bounded    : 58       (Average: 115.64 Max: 117 Sum:   6707 Ratio:   0.04%)

Rules        : 1028283  (Original: 843628)
Atoms        : 59257   
Bodies       : 791604   (Original: 606949)
  Count      : 9712     (Original: 27041)
Equivalences : 188391   (Atom=Atom: 172 Body=Body: 0 Other: 188219)
Tight        : Yes
Variables    : 578090   (Eliminated:    0 Frozen: 191082)
Constraints  : 4201647  (Binary:  91.4% Ternary:   7.1% Other:   1.6%)

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

[endof: stats after solve call]
Solving Time:	 22.22s
Memory:		 939MB (+0MB)
UNKNOWN
Iteration Time:	 22.23s

Iteration 17
Queue:		 [(0,115,16,True)]
Grounded Until:	 115
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 18
Time         : 402.993s (Solving: 388.95s 1st Model: 0.11s Unsat: 0.00s)
CPU Time     : 403.052s

Choices      : 18639848 (Domain: 18515837)
Conflicts    : 457858   (Analyzed: 457858)
Restarts     : 1700     (Average: 269.33 Last: 325)
Model-Level  : 4372.0  
Problems     : 18       (Average Length: 117.00 Splits: 0)
Lemmas       : 457858   (Deleted: 422353)
  Binary     : 13992    (Ratio:   3.06%)
  Ternary    : 2713     (Ratio:   0.59%)
  Conflict   : 457858   (Average Length:  799.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 457858   (Average: 39.57 Max: 1786 Sum: 18116027)
  Executed   : 457800   (Average: 39.55 Max: 1786 Sum: 18109320 Ratio:  99.96%)
  Bounded    : 58       (Average: 115.64 Max: 117 Sum:   6707 Ratio:   0.04%)

Rules        : 1028283  (Original: 843628)
Atoms        : 59257   
Bodies       : 791604   (Original: 606949)
  Count      : 9712     (Original: 27041)
Equivalences : 188391   (Atom=Atom: 172 Body=Body: 0 Other: 188219)
Tight        : Yes
Variables    : 578090   (Eliminated:    0 Frozen: 191082)
Constraints  : 4201647  (Binary:  91.4% Ternary:   7.1% Other:   1.6%)

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

[endof: stats after solve call]
Solving Time:	 23.69s
Memory:		 939MB (+0MB)
UNKNOWN
Iteration Time:	 23.69s

Iteration 18
Queue:		 [(0,115,17,True)]
Grounded Until:	 115
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 19
Time         : 423.787s (Solving: 409.63s 1st Model: 0.11s Unsat: 0.00s)
CPU Time     : 423.856s

Choices      : 19101847 (Domain: 18977218)
Conflicts    : 482691   (Analyzed: 482691)
Restarts     : 1800     (Average: 268.16 Last: 325)
Model-Level  : 4372.0  
Problems     : 19       (Average Length: 117.00 Splits: 0)
Lemmas       : 482691   (Deleted: 447512)
  Binary     : 14510    (Ratio:   3.01%)
  Ternary    : 2801     (Ratio:   0.58%)
  Conflict   : 482691   (Average Length:  821.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 482691   (Average: 38.39 Max: 1786 Sum: 18532192)
  Executed   : 482633   (Average: 38.38 Max: 1786 Sum: 18525485 Ratio:  99.96%)
  Bounded    : 58       (Average: 115.64 Max: 117 Sum:   6707 Ratio:   0.04%)

Rules        : 1028283  (Original: 843628)
Atoms        : 59257   
Bodies       : 791604   (Original: 606949)
  Count      : 9712     (Original: 27041)
Equivalences : 188391   (Atom=Atom: 172 Body=Body: 0 Other: 188219)
Tight        : Yes
Variables    : 578090   (Eliminated:    0 Frozen: 191082)
Constraints  : 4201647  (Binary:  91.4% Ternary:   7.1% Other:   1.6%)

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

[endof: stats after solve call]
Solving Time:	 20.81s
Memory:		 939MB (+0MB)
UNKNOWN
Iteration Time:	 20.81s

Iteration 19
Queue:		 [(0,115,18,True)]
Grounded Until:	 115
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 20
Time         : 446.358s (Solving: 432.06s 1st Model: 0.11s Unsat: 0.00s)
CPU Time     : 446.436s

Choices      : 19727025 (Domain: 19601443)
Conflicts    : 511410   (Analyzed: 511410)
Restarts     : 1900     (Average: 269.16 Last: 325)
Model-Level  : 4372.0  
Problems     : 20       (Average Length: 117.00 Splits: 0)
Lemmas       : 511410   (Deleted: 473835)
  Binary     : 15075    (Ratio:   2.95%)
  Ternary    : 2971     (Ratio:   0.58%)
  Conflict   : 511410   (Average Length:  833.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 511410   (Average: 37.37 Max: 1786 Sum: 19110808)
  Executed   : 511352   (Average: 37.36 Max: 1786 Sum: 19104101 Ratio:  99.96%)
  Bounded    : 58       (Average: 115.64 Max: 117 Sum:   6707 Ratio:   0.04%)

Rules        : 1028283  (Original: 843628)
Atoms        : 59257   
Bodies       : 791604   (Original: 606949)
  Count      : 9712     (Original: 27041)
Equivalences : 188391   (Atom=Atom: 172 Body=Body: 0 Other: 188219)
Tight        : Yes
Variables    : 578090   (Eliminated:    0 Frozen: 191082)
Constraints  : 4201647  (Binary:  91.4% Ternary:   7.1% Other:   1.6%)

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

[endof: stats after solve call]
Solving Time:	 22.58s
Memory:		 939MB (+0MB)
UNKNOWN
Iteration Time:	 22.58s

Iteration 20
Queue:		 [(0,115,19,True)]
Grounded Until:	 115
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 21
Time         : 466.661s (Solving: 452.27s 1st Model: 0.11s Unsat: 0.00s)
CPU Time     : 466.748s

Choices      : 20253628 (Domain: 20127111)
Conflicts    : 537402   (Analyzed: 537402)
Restarts     : 2000     (Average: 268.70 Last: 325)
Model-Level  : 4372.0  
Problems     : 21       (Average Length: 117.00 Splits: 0)
Lemmas       : 537402   (Deleted: 498510)
  Binary     : 15567    (Ratio:   2.90%)
  Ternary    : 3104     (Ratio:   0.58%)
  Conflict   : 537402   (Average Length:  845.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 537402   (Average: 36.45 Max: 1786 Sum: 19587778)
  Executed   : 537344   (Average: 36.44 Max: 1786 Sum: 19581071 Ratio:  99.97%)
  Bounded    : 58       (Average: 115.64 Max: 117 Sum:   6707 Ratio:   0.03%)

Rules        : 1028283  (Original: 843628)
Atoms        : 59257   
Bodies       : 791604   (Original: 606949)
  Count      : 9712     (Original: 27041)
Equivalences : 188391   (Atom=Atom: 172 Body=Body: 0 Other: 188219)
Tight        : Yes
Variables    : 578090   (Eliminated:    0 Frozen: 191082)
Constraints  : 4201647  (Binary:  91.4% Ternary:   7.1% Other:   1.6%)

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

[endof: stats after solve call]
Solving Time:	 20.31s
Memory:		 939MB (+0MB)
UNKNOWN
Iteration Time:	 20.31s

Iteration 21
Queue:		 [(0,115,20,True)]
Grounded Until:	 115
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 22
Time         : 488.409s (Solving: 473.91s 1st Model: 0.11s Unsat: 0.00s)
CPU Time     : 488.508s

Choices      : 20680606 (Domain: 20553451)
Conflicts    : 564339   (Analyzed: 564339)
Restarts     : 2100     (Average: 268.73 Last: 325)
Model-Level  : 4372.0  
Problems     : 22       (Average Length: 117.00 Splits: 0)
Lemmas       : 564339   (Deleted: 523616)
  Binary     : 15907    (Ratio:   2.82%)
  Ternary    : 3187     (Ratio:   0.56%)
  Conflict   : 564339   (Average Length:  860.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 564339   (Average: 35.38 Max: 1786 Sum: 19966992)
  Executed   : 564281   (Average: 35.37 Max: 1786 Sum: 19960285 Ratio:  99.97%)
  Bounded    : 58       (Average: 115.64 Max: 117 Sum:   6707 Ratio:   0.03%)

Rules        : 1028283  (Original: 843628)
Atoms        : 59257   
Bodies       : 791604   (Original: 606949)
  Count      : 9712     (Original: 27041)
Equivalences : 188391   (Atom=Atom: 172 Body=Body: 0 Other: 188219)
Tight        : Yes
Variables    : 578090   (Eliminated:    0 Frozen: 191082)
Constraints  : 4201647  (Binary:  91.4% Ternary:   7.1% Other:   1.6%)

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

[endof: stats after solve call]
Solving Time:	 21.76s
Memory:		 939MB (+0MB)
UNKNOWN
Iteration Time:	 21.76s

Iteration 22
Queue:		 [(0,115,21,True)]
Grounded Until:	 115
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 23
Time         : 509.601s (Solving: 494.96s 1st Model: 0.11s Unsat: 0.00s)
CPU Time     : 509.708s

Choices      : 21157210 (Domain: 21028550)
Conflicts    : 590789   (Analyzed: 590789)
Restarts     : 2200     (Average: 268.54 Last: 325)
Model-Level  : 4372.0  
Problems     : 23       (Average Length: 117.00 Splits: 0)
Lemmas       : 590789   (Deleted: 549647)
  Binary     : 16276    (Ratio:   2.75%)
  Ternary    : 3277     (Ratio:   0.55%)
  Conflict   : 590789   (Average Length:  876.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 590789   (Average: 34.53 Max: 1786 Sum: 20397175)
  Executed   : 590731   (Average: 34.51 Max: 1786 Sum: 20390468 Ratio:  99.97%)
  Bounded    : 58       (Average: 115.64 Max: 117 Sum:   6707 Ratio:   0.03%)

Rules        : 1028283  (Original: 843628)
Atoms        : 59257   
Bodies       : 791604   (Original: 606949)
  Count      : 9712     (Original: 27041)
Equivalences : 188391   (Atom=Atom: 172 Body=Body: 0 Other: 188219)
Tight        : Yes
Variables    : 578090   (Eliminated:    0 Frozen: 191082)
Constraints  : 4201647  (Binary:  91.4% Ternary:   7.1% Other:   1.6%)

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

[endof: stats after solve call]
Solving Time:	 21.20s
Memory:		 939MB (+0MB)
UNKNOWN
Iteration Time:	 21.20s

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

Models       : 0+
Calls        : 24
Time         : 530.103s (Solving: 515.37s 1st Model: 0.11s Unsat: 0.00s)
CPU Time     : 530.216s

Choices      : 21566865 (Domain: 21437541)
Conflicts    : 619802   (Analyzed: 619802)
Restarts     : 2300     (Average: 269.48 Last: 325)
Model-Level  : 4372.0  
Problems     : 24       (Average Length: 117.00 Splits: 0)
Lemmas       : 619802   (Deleted: 578266)
  Binary     : 16575    (Ratio:   2.67%)
  Ternary    : 3362     (Ratio:   0.54%)
  Conflict   : 619802   (Average Length:  891.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 619802   (Average: 33.51 Max: 1786 Sum: 20768694)
  Executed   : 619744   (Average: 33.50 Max: 1786 Sum: 20761987 Ratio:  99.97%)
  Bounded    : 58       (Average: 115.64 Max: 117 Sum:   6707 Ratio:   0.03%)

Rules        : 1028283  (Original: 843628)
Atoms        : 59257   
Bodies       : 791604   (Original: 606949)
  Count      : 9712     (Original: 27041)
Equivalences : 188391   (Atom=Atom: 172 Body=Body: 0 Other: 188219)
Tight        : Yes
Variables    : 578090   (Eliminated:    0 Frozen: 191082)
Constraints  : 4201647  (Binary:  91.4% Ternary:   7.1% Other:   1.6%)

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

[endof: stats after solve call]
Solving Time:	 20.51s
Memory:		 939MB (+0MB)
UNKNOWN
Iteration Time:	 20.51s

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

Models       : 0+
Calls        : 25
Time         : 550.333s (Solving: 535.48s 1st Model: 0.11s Unsat: 0.00s)
CPU Time     : 550.456s

Choices      : 21982303 (Domain: 21851647)
Conflicts    : 646020   (Analyzed: 646020)
Restarts     : 2400     (Average: 269.18 Last: 325)
Model-Level  : 4372.0  
Problems     : 25       (Average Length: 117.00 Splits: 0)
Lemmas       : 646020   (Deleted: 603231)
  Binary     : 16982    (Ratio:   2.63%)
  Ternary    : 3418     (Ratio:   0.53%)
  Conflict   : 646020   (Average Length:  900.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 646020   (Average: 32.72 Max: 1786 Sum: 21137360)
  Executed   : 645962   (Average: 32.71 Max: 1786 Sum: 21130653 Ratio:  99.97%)
  Bounded    : 58       (Average: 115.64 Max: 117 Sum:   6707 Ratio:   0.03%)

Rules        : 1028283  (Original: 843628)
Atoms        : 59257   
Bodies       : 791604   (Original: 606949)
  Count      : 9712     (Original: 27041)
Equivalences : 188391   (Atom=Atom: 172 Body=Body: 0 Other: 188219)
Tight        : Yes
Variables    : 578090   (Eliminated:    0 Frozen: 191082)
Constraints  : 4201647  (Binary:  91.4% Ternary:   7.1% Other:   1.6%)

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

[endof: stats after solve call]
Solving Time:	 20.24s
Memory:		 939MB (+0MB)
UNKNOWN
Iteration Time:	 20.24s

Iteration 25
Queue:		 [(0,115,24,True)]
Grounded Until:	 115
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 26
Time         : 569.096s (Solving: 554.14s 1st Model: 0.11s Unsat: 0.00s)
CPU Time     : 569.228s

Choices      : 22425207 (Domain: 22294014)
Conflicts    : 670462   (Analyzed: 670462)
Restarts     : 2500     (Average: 268.18 Last: 325)
Model-Level  : 4372.0  
Problems     : 26       (Average Length: 117.00 Splits: 0)
Lemmas       : 670462   (Deleted: 625776)
  Binary     : 17232    (Ratio:   2.57%)
  Ternary    : 3491     (Ratio:   0.52%)
  Conflict   : 670462   (Average Length:  900.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 670462   (Average: 32.11 Max: 1786 Sum: 21531352)
  Executed   : 670404   (Average: 32.10 Max: 1786 Sum: 21524645 Ratio:  99.97%)
  Bounded    : 58       (Average: 115.64 Max: 117 Sum:   6707 Ratio:   0.03%)

Rules        : 1028283  (Original: 843628)
Atoms        : 59257   
Bodies       : 791604   (Original: 606949)
  Count      : 9712     (Original: 27041)
Equivalences : 188391   (Atom=Atom: 172 Body=Body: 0 Other: 188219)
Tight        : Yes
Variables    : 578090   (Eliminated:    0 Frozen: 191082)
Constraints  : 4201647  (Binary:  91.4% Ternary:   7.1% Other:   1.6%)

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

[endof: stats after solve call]
Solving Time:	 18.77s
Memory:		 939MB (+0MB)
UNKNOWN
Iteration Time:	 18.77s

Iteration 26
Queue:		 [(0,115,25,True)]
Grounded Until:	 115
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 27
Time         : 587.844s (Solving: 572.77s 1st Model: 0.11s Unsat: 0.00s)
CPU Time     : 587.984s

Choices      : 22777286 (Domain: 22645410)
Conflicts    : 695275   (Analyzed: 695275)
Restarts     : 2600     (Average: 267.41 Last: 325)
Model-Level  : 4372.0  
Problems     : 27       (Average Length: 117.00 Splits: 0)
Lemmas       : 695275   (Deleted: 652305)
  Binary     : 17448    (Ratio:   2.51%)
  Ternary    : 3540     (Ratio:   0.51%)
  Conflict   : 695275   (Average Length:  903.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 695275   (Average: 31.41 Max: 1786 Sum: 21841035)
  Executed   : 695217   (Average: 31.40 Max: 1786 Sum: 21834328 Ratio:  99.97%)
  Bounded    : 58       (Average: 115.64 Max: 117 Sum:   6707 Ratio:   0.03%)

Rules        : 1028283  (Original: 843628)
Atoms        : 59257   
Bodies       : 791604   (Original: 606949)
  Count      : 9712     (Original: 27041)
Equivalences : 188391   (Atom=Atom: 172 Body=Body: 0 Other: 188219)
Tight        : Yes
Variables    : 578090   (Eliminated:    0 Frozen: 191082)
Constraints  : 4201647  (Binary:  91.4% Ternary:   7.1% Other:   1.6%)

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

[endof: stats after solve call]
Solving Time:	 18.76s
Memory:		 939MB (+0MB)
UNKNOWN
Iteration Time:	 18.76s

Iteration 27
Queue:		 [(0,115,26,True)]
Grounded Until:	 115
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 28
Time         : 610.776s (Solving: 595.57s 1st Model: 0.11s Unsat: 0.00s)
CPU Time     : 610.928s

Choices      : 23214111 (Domain: 23081639)
Conflicts    : 726046   (Analyzed: 726046)
Restarts     : 2700     (Average: 268.91 Last: 325)
Model-Level  : 4372.0  
Problems     : 28       (Average Length: 117.00 Splits: 0)
Lemmas       : 726046   (Deleted: 682038)
  Binary     : 17753    (Ratio:   2.45%)
  Ternary    : 3653     (Ratio:   0.50%)
  Conflict   : 726046   (Average Length:  906.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 726046   (Average: 30.63 Max: 1786 Sum: 22239299)
  Executed   : 725988   (Average: 30.62 Max: 1786 Sum: 22232592 Ratio:  99.97%)
  Bounded    : 58       (Average: 115.64 Max: 117 Sum:   6707 Ratio:   0.03%)

Rules        : 1028283  (Original: 843628)
Atoms        : 59257   
Bodies       : 791604   (Original: 606949)
  Count      : 9712     (Original: 27041)
Equivalences : 188391   (Atom=Atom: 172 Body=Body: 0 Other: 188219)
Tight        : Yes
Variables    : 578090   (Eliminated:    0 Frozen: 191082)
Constraints  : 4201647  (Binary:  91.4% Ternary:   7.1% Other:   1.6%)

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

[endof: stats after solve call]
Solving Time:	 22.94s
Memory:		 939MB (+0MB)
UNKNOWN
Iteration Time:	 22.95s

Iteration 28
Queue:		 [(0,115,27,True)]
Grounded Until:	 115
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 29
Time         : 632.385s (Solving: 617.03s 1st Model: 0.11s Unsat: 0.00s)
CPU Time     : 632.548s

Choices      : 23667160 (Domain: 23533806)
Conflicts    : 753519   (Analyzed: 753519)
Restarts     : 2800     (Average: 269.11 Last: 325)
Model-Level  : 4372.0  
Problems     : 29       (Average Length: 117.00 Splits: 0)
Lemmas       : 753519   (Deleted: 706206)
  Binary     : 18045    (Ratio:   2.39%)
  Ternary    : 3715     (Ratio:   0.49%)
  Conflict   : 753519   (Average Length:  910.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 753519   (Average: 30.06 Max: 1786 Sum: 22648817)
  Executed   : 753461   (Average: 30.05 Max: 1786 Sum: 22642110 Ratio:  99.97%)
  Bounded    : 58       (Average: 115.64 Max: 117 Sum:   6707 Ratio:   0.03%)

Rules        : 1028283  (Original: 843628)
Atoms        : 59257   
Bodies       : 791604   (Original: 606949)
  Count      : 9712     (Original: 27041)
Equivalences : 188391   (Atom=Atom: 172 Body=Body: 0 Other: 188219)
Tight        : Yes
Variables    : 578090   (Eliminated:    0 Frozen: 191082)
Constraints  : 4201647  (Binary:  91.4% Ternary:   7.1% Other:   1.6%)

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

[endof: stats after solve call]
Solving Time:	 21.62s
Memory:		 939MB (+0MB)
UNKNOWN
Iteration Time:	 21.62s

Iteration 29
Queue:		 [(0,115,28,True)]
Grounded Until:	 115
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 30
Time         : 652.470s (Solving: 637.01s 1st Model: 0.11s Unsat: 0.00s)
CPU Time     : 652.644s

Choices      : 24122919 (Domain: 23988579)
Conflicts    : 779721   (Analyzed: 779721)
Restarts     : 2900     (Average: 268.87 Last: 325)
Model-Level  : 4372.0  
Problems     : 30       (Average Length: 117.00 Splits: 0)
Lemmas       : 779721   (Deleted: 732791)
  Binary     : 18282    (Ratio:   2.34%)
  Ternary    : 3769     (Ratio:   0.48%)
  Conflict   : 779721   (Average Length:  906.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 779721   (Average: 29.57 Max: 1786 Sum: 23054411)
  Executed   : 779663   (Average: 29.56 Max: 1786 Sum: 23047704 Ratio:  99.97%)
  Bounded    : 58       (Average: 115.64 Max: 117 Sum:   6707 Ratio:   0.03%)

Rules        : 1028283  (Original: 843628)
Atoms        : 59257   
Bodies       : 791604   (Original: 606949)
  Count      : 9712     (Original: 27041)
Equivalences : 188391   (Atom=Atom: 172 Body=Body: 0 Other: 188219)
Tight        : Yes
Variables    : 578090   (Eliminated:    0 Frozen: 191082)
Constraints  : 4201647  (Binary:  91.4% Ternary:   7.1% Other:   1.6%)

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

[endof: stats after solve call]
Solving Time:	 20.10s
Memory:		 939MB (+0MB)
UNKNOWN
Iteration Time:	 20.10s

Iteration 30
Queue:		 [(0,115,29,True)]
Grounded Until:	 115
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 31
Time         : 676.046s (Solving: 660.47s 1st Model: 0.11s Unsat: 0.00s)
CPU Time     : 676.228s

Choices      : 24597842 (Domain: 24462468)
Conflicts    : 811224   (Analyzed: 811224)
Restarts     : 3000     (Average: 270.41 Last: 326)
Model-Level  : 4372.0  
Problems     : 31       (Average Length: 117.00 Splits: 0)
Lemmas       : 811224   (Deleted: 764109)
  Binary     : 18542    (Ratio:   2.29%)
  Ternary    : 3826     (Ratio:   0.47%)
  Conflict   : 811224   (Average Length:  907.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 811224   (Average: 28.95 Max: 1786 Sum: 23488210)
  Executed   : 811166   (Average: 28.95 Max: 1786 Sum: 23481503 Ratio:  99.97%)
  Bounded    : 58       (Average: 115.64 Max: 117 Sum:   6707 Ratio:   0.03%)

Rules        : 1028283  (Original: 843628)
Atoms        : 59257   
Bodies       : 791604   (Original: 606949)
  Count      : 9712     (Original: 27041)
Equivalences : 188391   (Atom=Atom: 172 Body=Body: 0 Other: 188219)
Tight        : Yes
Variables    : 578090   (Eliminated:    0 Frozen: 191082)
Constraints  : 4201647  (Binary:  91.4% Ternary:   7.1% Other:   1.6%)

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

[endof: stats after solve call]
Solving Time:	 23.59s
Memory:		 939MB (+0MB)
UNKNOWN
Iteration Time:	 23.59s

Iteration 31
Queue:		 [(0,115,30,True)]
Grounded Until:	 115
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 32
Time         : 697.320s (Solving: 681.63s 1st Model: 0.11s Unsat: 0.00s)
CPU Time     : 697.512s

Choices      : 24938437 (Domain: 24802939)
Conflicts    : 839742   (Analyzed: 839742)
Restarts     : 3100     (Average: 270.88 Last: 326)
Model-Level  : 4372.0  
Problems     : 32       (Average Length: 117.00 Splits: 0)
Lemmas       : 839742   (Deleted: 791748)
  Binary     : 18814    (Ratio:   2.24%)
  Ternary    : 3884     (Ratio:   0.46%)
  Conflict   : 839742   (Average Length:  911.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 839742   (Average: 28.33 Max: 1786 Sum: 23790263)
  Executed   : 839684   (Average: 28.32 Max: 1786 Sum: 23783556 Ratio:  99.97%)
  Bounded    : 58       (Average: 115.64 Max: 117 Sum:   6707 Ratio:   0.03%)

Rules        : 1028283  (Original: 843628)
Atoms        : 59257   
Bodies       : 791604   (Original: 606949)
  Count      : 9712     (Original: 27041)
Equivalences : 188391   (Atom=Atom: 172 Body=Body: 0 Other: 188219)
Tight        : Yes
Variables    : 578090   (Eliminated:    0 Frozen: 191082)
Constraints  : 4201647  (Binary:  91.4% Ternary:   7.1% Other:   1.6%)

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

[endof: stats after solve call]
Solving Time:	 21.28s
Memory:		 939MB (+0MB)
UNKNOWN
Iteration Time:	 21.28s

Iteration 32
Queue:		 [(0,115,31,True)]
Grounded Until:	 115
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 33
Time         : 718.490s (Solving: 702.69s 1st Model: 0.11s Unsat: 0.00s)
CPU Time     : 718.692s

Choices      : 25366137 (Domain: 25230264)
Conflicts    : 868660   (Analyzed: 868660)
Restarts     : 3200     (Average: 271.46 Last: 326)
Model-Level  : 4372.0  
Problems     : 33       (Average Length: 117.00 Splits: 0)
Lemmas       : 868660   (Deleted: 819464)
  Binary     : 19051    (Ratio:   2.19%)
  Ternary    : 3928     (Ratio:   0.45%)
  Conflict   : 868660   (Average Length:  911.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 868660   (Average: 27.83 Max: 1786 Sum: 24175966)
  Executed   : 868602   (Average: 27.82 Max: 1786 Sum: 24169259 Ratio:  99.97%)
  Bounded    : 58       (Average: 115.64 Max: 117 Sum:   6707 Ratio:   0.03%)

Rules        : 1028283  (Original: 843628)
Atoms        : 59257   
Bodies       : 791604   (Original: 606949)
  Count      : 9712     (Original: 27041)
Equivalences : 188391   (Atom=Atom: 172 Body=Body: 0 Other: 188219)
Tight        : Yes
Variables    : 578090   (Eliminated:    0 Frozen: 191082)
Constraints  : 4201647  (Binary:  91.4% Ternary:   7.1% Other:   1.6%)

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

[endof: stats after solve call]
Solving Time:	 21.18s
Memory:		 939MB (+0MB)
UNKNOWN
Iteration Time:	 21.18s

Iteration 33
Queue:		 [(0,115,32,True)]
Grounded Until:	 115
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 34
Time         : 740.215s (Solving: 724.31s 1st Model: 0.11s Unsat: 0.00s)
CPU Time     : 740.424s

Choices      : 25730893 (Domain: 25594878)
Conflicts    : 897958   (Analyzed: 897958)
Restarts     : 3300     (Average: 272.11 Last: 326)
Model-Level  : 4372.0  
Problems     : 34       (Average Length: 117.00 Splits: 0)
Lemmas       : 897958   (Deleted: 847731)
  Binary     : 19266    (Ratio:   2.15%)
  Ternary    : 3993     (Ratio:   0.44%)
  Conflict   : 897958   (Average Length:  913.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 897958   (Average: 27.28 Max: 1786 Sum: 24499836)
  Executed   : 897900   (Average: 27.28 Max: 1786 Sum: 24493129 Ratio:  99.97%)
  Bounded    : 58       (Average: 115.64 Max: 117 Sum:   6707 Ratio:   0.03%)

Rules        : 1028283  (Original: 843628)
Atoms        : 59257   
Bodies       : 791604   (Original: 606949)
  Count      : 9712     (Original: 27041)
Equivalences : 188391   (Atom=Atom: 172 Body=Body: 0 Other: 188219)
Tight        : Yes
Variables    : 578090   (Eliminated:    0 Frozen: 191082)
Constraints  : 4201647  (Binary:  91.4% Ternary:   7.1% Other:   1.6%)

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

[endof: stats after solve call]
Solving Time:	 21.74s
Memory:		 939MB (+0MB)
UNKNOWN
Iteration Time:	 21.74s

Iteration 34
Queue:		 [(0,115,33,True)]
Grounded Until:	 115
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 35
Time         : 761.098s (Solving: 745.08s 1st Model: 0.11s Unsat: 0.00s)
CPU Time     : 761.316s

Choices      : 26170326 (Domain: 26033413)
Conflicts    : 926147   (Analyzed: 926147)
Restarts     : 3400     (Average: 272.40 Last: 326)
Model-Level  : 4372.0  
Problems     : 35       (Average Length: 117.00 Splits: 0)
Lemmas       : 926147   (Deleted: 876371)
  Binary     : 19483    (Ratio:   2.10%)
  Ternary    : 4055     (Ratio:   0.44%)
  Conflict   : 926147   (Average Length:  916.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 926147   (Average: 26.88 Max: 1786 Sum: 24896913)
  Executed   : 926089   (Average: 26.88 Max: 1786 Sum: 24890206 Ratio:  99.97%)
  Bounded    : 58       (Average: 115.64 Max: 117 Sum:   6707 Ratio:   0.03%)

Rules        : 1028283  (Original: 843628)
Atoms        : 59257   
Bodies       : 791604   (Original: 606949)
  Count      : 9712     (Original: 27041)
Equivalences : 188391   (Atom=Atom: 172 Body=Body: 0 Other: 188219)
Tight        : Yes
Variables    : 578090   (Eliminated:    0 Frozen: 191082)
Constraints  : 4201647  (Binary:  91.4% Ternary:   7.1% Other:   1.6%)

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

[endof: stats after solve call]
Solving Time:	 20.89s
Memory:		 939MB (+0MB)
UNKNOWN
Iteration Time:	 20.89s

Iteration 35
Queue:		 [(0,115,34,True)]
Grounded Until:	 115
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 36
Time         : 781.678s (Solving: 765.56s 1st Model: 0.11s Unsat: 0.00s)
CPU Time     : 781.904s

Choices      : 26554069 (Domain: 26416150)
Conflicts    : 951483   (Analyzed: 951483)
Restarts     : 3500     (Average: 271.85 Last: 326)
Model-Level  : 4372.0  
Problems     : 36       (Average Length: 117.00 Splits: 0)
Lemmas       : 951483   (Deleted: 900418)
  Binary     : 19900    (Ratio:   2.09%)
  Ternary    : 4159     (Ratio:   0.44%)
  Conflict   : 951483   (Average Length:  912.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 951483   (Average: 26.53 Max: 1786 Sum: 25243389)
  Executed   : 951425   (Average: 26.52 Max: 1786 Sum: 25236682 Ratio:  99.97%)
  Bounded    : 58       (Average: 115.64 Max: 117 Sum:   6707 Ratio:   0.03%)

Rules        : 1028283  (Original: 843628)
Atoms        : 59257   
Bodies       : 791604   (Original: 606949)
  Count      : 9712     (Original: 27041)
Equivalences : 188391   (Atom=Atom: 172 Body=Body: 0 Other: 188219)
Tight        : Yes
Variables    : 578090   (Eliminated:    0 Frozen: 191082)
Constraints  : 4201647  (Binary:  91.4% Ternary:   7.1% Other:   1.6%)

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

[endof: stats after solve call]
Solving Time:	 20.59s
Memory:		 939MB (+0MB)
UNKNOWN
Iteration Time:	 20.59s

Iteration 36
Queue:		 [(0,115,35,True)]
Grounded Until:	 115
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 37
Time         : 801.127s (Solving: 784.90s 1st Model: 0.11s Unsat: 0.00s)
CPU Time     : 801.364s

Choices      : 26892139 (Domain: 26753297)
Conflicts    : 979217   (Analyzed: 979217)
Restarts     : 3600     (Average: 272.00 Last: 326)
Model-Level  : 4372.0  
Problems     : 37       (Average Length: 117.00 Splits: 0)
Lemmas       : 979217   (Deleted: 928036)
  Binary     : 20098    (Ratio:   2.05%)
  Ternary    : 4198     (Ratio:   0.43%)
  Conflict   : 979217   (Average Length:  912.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 979217   (Average: 26.09 Max: 1786 Sum: 25546029)
  Executed   : 979159   (Average: 26.08 Max: 1786 Sum: 25539322 Ratio:  99.97%)
  Bounded    : 58       (Average: 115.64 Max: 117 Sum:   6707 Ratio:   0.03%)

Rules        : 1028283  (Original: 843628)
Atoms        : 59257   
Bodies       : 791604   (Original: 606949)
  Count      : 9712     (Original: 27041)
Equivalences : 188391   (Atom=Atom: 172 Body=Body: 0 Other: 188219)
Tight        : Yes
Variables    : 578090   (Eliminated:    0 Frozen: 191082)
Constraints  : 4201647  (Binary:  91.4% Ternary:   7.1% Other:   1.6%)

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

[endof: stats after solve call]
Solving Time:	 19.46s
Memory:		 939MB (+0MB)
UNKNOWN
Iteration Time:	 19.46s

Iteration 37
Queue:		 [(0,115,36,True)]
Grounded Until:	 115
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 38
Time         : 818.601s (Solving: 802.27s 1st Model: 0.11s Unsat: 0.00s)
CPU Time     : 818.848s

Choices      : 27181636 (Domain: 27042680)
Conflicts    : 1007186  (Analyzed: 1007186)
Restarts     : 3700     (Average: 272.21 Last: 326)
Model-Level  : 4372.0  
Problems     : 38       (Average Length: 117.00 Splits: 0)
Lemmas       : 1007186  (Deleted: 955194)
  Binary     : 20322    (Ratio:   2.02%)
  Ternary    : 4254     (Ratio:   0.42%)
  Conflict   : 1007186  (Average Length:  909.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 1007186  (Average: 25.61 Max: 1786 Sum: 25796334)
  Executed   : 1007128  (Average: 25.61 Max: 1786 Sum: 25789627 Ratio:  99.97%)
  Bounded    : 58       (Average: 115.64 Max: 117 Sum:   6707 Ratio:   0.03%)

Rules        : 1028283  (Original: 843628)
Atoms        : 59257   
Bodies       : 791604   (Original: 606949)
  Count      : 9712     (Original: 27041)
Equivalences : 188391   (Atom=Atom: 172 Body=Body: 0 Other: 188219)
Tight        : Yes
Variables    : 578090   (Eliminated:    0 Frozen: 191082)
Constraints  : 4201647  (Binary:  91.4% Ternary:   7.1% Other:   1.6%)

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

[endof: stats after solve call]
Solving Time:	 17.48s
Memory:		 939MB (+0MB)
UNKNOWN
Iteration Time:	 17.48s

Iteration 38
Queue:		 [(0,115,37,True)]
Grounded Until:	 115
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 39
Time         : 838.181s (Solving: 821.75s 1st Model: 0.11s Unsat: 0.00s)
CPU Time     : 838.436s

Choices      : 27479457 (Domain: 27340496)
Conflicts    : 1034205  (Analyzed: 1034205)
Restarts     : 3800     (Average: 272.16 Last: 326)
Model-Level  : 4372.0  
Problems     : 39       (Average Length: 117.00 Splits: 0)
Lemmas       : 1034205  (Deleted: 979655)
  Binary     : 20519    (Ratio:   1.98%)
  Ternary    : 4287     (Ratio:   0.41%)
  Conflict   : 1034205  (Average Length:  909.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 1034205  (Average: 25.20 Max: 1786 Sum: 26058309)
  Executed   : 1034147  (Average: 25.19 Max: 1786 Sum: 26051602 Ratio:  99.97%)
  Bounded    : 58       (Average: 115.64 Max: 117 Sum:   6707 Ratio:   0.03%)

Rules        : 1028283  (Original: 843628)
Atoms        : 59257   
Bodies       : 791604   (Original: 606949)
  Count      : 9712     (Original: 27041)
Equivalences : 188391   (Atom=Atom: 172 Body=Body: 0 Other: 188219)
Tight        : Yes
Variables    : 578090   (Eliminated:    0 Frozen: 191082)
Constraints  : 4201647  (Binary:  91.4% Ternary:   7.1% Other:   1.6%)

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

[endof: stats after solve call]
Solving Time:	 19.59s
Memory:		 939MB (+0MB)
UNKNOWN
Iteration Time:	 19.59s

Iteration 39
Queue:		 [(0,115,38,True)]
Grounded Until:	 115
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 40
Time         : 860.478s (Solving: 843.93s 1st Model: 0.11s Unsat: 0.00s)
CPU Time     : 860.744s

Choices      : 27848665 (Domain: 27709206)
Conflicts    : 1065225  (Analyzed: 1065225)
Restarts     : 3900     (Average: 273.13 Last: 326)
Model-Level  : 4372.0  
Problems     : 40       (Average Length: 117.00 Splits: 0)
Lemmas       : 1065225  (Deleted: 1012000)
  Binary     : 20669    (Ratio:   1.94%)
  Ternary    : 4323     (Ratio:   0.41%)
  Conflict   : 1065225  (Average Length:  908.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 1065225  (Average: 24.77 Max: 1786 Sum: 26390596)
  Executed   : 1065167  (Average: 24.77 Max: 1786 Sum: 26383889 Ratio:  99.97%)
  Bounded    : 58       (Average: 115.64 Max: 117 Sum:   6707 Ratio:   0.03%)

Rules        : 1028283  (Original: 843628)
Atoms        : 59257   
Bodies       : 791604   (Original: 606949)
  Count      : 9712     (Original: 27041)
Equivalences : 188391   (Atom=Atom: 172 Body=Body: 0 Other: 188219)
Tight        : Yes
Variables    : 578090   (Eliminated:    0 Frozen: 191082)
Constraints  : 4201647  (Binary:  91.4% Ternary:   7.1% Other:   1.6%)

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

[endof: stats after solve call]
Solving Time:	 22.31s
Memory:		 939MB (+0MB)
UNKNOWN
Iteration Time:	 22.31s

Iteration 40
Queue:		 [(0,115,39,True)]
Grounded Until:	 115
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 41
Time         : 882.690s (Solving: 866.04s 1st Model: 0.11s Unsat: 0.00s)
CPU Time     : 882.964s

Choices      : 28246722 (Domain: 28106873)
Conflicts    : 1094300  (Analyzed: 1094300)
Restarts     : 4000     (Average: 273.57 Last: 326)
Model-Level  : 4372.0  
Problems     : 41       (Average Length: 117.00 Splits: 0)
Lemmas       : 1094300  (Deleted: 1039235)
  Binary     : 20793    (Ratio:   1.90%)
  Ternary    : 4351     (Ratio:   0.40%)
  Conflict   : 1094300  (Average Length:  905.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 1094300  (Average: 24.45 Max: 1786 Sum: 26750286)
  Executed   : 1094242  (Average: 24.44 Max: 1786 Sum: 26743579 Ratio:  99.97%)
  Bounded    : 58       (Average: 115.64 Max: 117 Sum:   6707 Ratio:   0.03%)

Rules        : 1028283  (Original: 843628)
Atoms        : 59257   
Bodies       : 791604   (Original: 606949)
  Count      : 9712     (Original: 27041)
Equivalences : 188391   (Atom=Atom: 172 Body=Body: 0 Other: 188219)
Tight        : Yes
Variables    : 578090   (Eliminated:    0 Frozen: 191082)
Constraints  : 4201647  (Binary:  91.4% Ternary:   7.1% Other:   1.6%)

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

[endof: stats after solve call]
Solving Time:	 22.22s
Memory:		 939MB (+0MB)
UNKNOWN
Iteration Time:	 22.22s

Iteration 41
Queue:		 [(0,115,40,True)]
Grounded Until:	 115
Solving...
*** Info : (planner): INTERRUPTED by signal!
UNKNOWN

INTERRUPTED  : 1

Models       : 0+
Calls        : 42
Time         : 894.406s (Solving: 877.62s 1st Model: 0.11s Unsat: 0.00s)
CPU Time     : 894.664s

Choices      : 28389015 (Domain: 28249163)
Conflicts    : 1107975  (Analyzed: 1107975)
Restarts     : 4057     (Average: 273.10 Last: 326)
Model-Level  : 4372.0  
Problems     : 42       (Average Length: 117.00 Splits: 0)
Lemmas       : 1107975  (Deleted: 1054557)
  Binary     : 20823    (Ratio:   1.88%)
  Ternary    : 4364     (Ratio:   0.39%)
  Conflict   : 1107975  (Average Length:  906.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 1107975  (Average: 24.25 Max: 1786 Sum: 26871982)
  Executed   : 1107917  (Average: 24.25 Max: 1786 Sum: 26865275 Ratio:  99.98%)
  Bounded    : 58       (Average: 115.64 Max: 117 Sum:   6707 Ratio:   0.02%)

Rules        : 1028283  (Original: 843628)
Atoms        : 59257   
Bodies       : 791604   (Original: 606949)
  Count      : 9712     (Original: 27041)
Equivalences : 188391   (Atom=Atom: 172 Body=Body: 0 Other: 188219)
Tight        : Yes
Variables    : 578090   (Eliminated:    0 Frozen: 191082)
Constraints  : 4201647  (Binary:  91.4% Ternary:   7.1% Other:   1.6%)

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


