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-6.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-6.pddl
Parsing...
Parsing: [0.030s CPU, 0.028s wall-clock]
Normalizing task... [0.010s CPU, 0.002s wall-clock]
Instantiating...
Generating Datalog program... [0.000s CPU, 0.008s wall-clock]
Normalizing Datalog program...
Normalizing Datalog program: [0.040s CPU, 0.041s wall-clock]
Preparing model... [0.020s CPU, 0.023s wall-clock]
Generated 115 rules.
Computing model... [0.370s CPU, 0.370s wall-clock]
2300 relevant atoms
2393 auxiliary atoms
4693 final queue length
8087 total queue pushes
Completing instantiation... [0.680s CPU, 0.686s wall-clock]
Instantiating: [1.130s CPU, 1.133s wall-clock]
Computing fact groups...
Finding invariants...
24 initial candidates
Finding invariants: [0.110s 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.010s 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.000s 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.039s wall-clock]
Translating task: [0.730s CPU, 0.726s wall-clock]
2672 effect conditions simplified
0 implied preconditions added
Detecting unreachable propositions...
0 operators removed
0 axioms removed
3 propositions removed
Detecting unreachable propositions: [0.360s CPU, 0.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.240s CPU, 0.242s wall-clock]
Translator variables: 241
Translator derived variables: 0
Translator facts: 505
Translator goal facts: 10
Translator mutex groups: 12
Translator total mutex groups size: 36
Translator operators: 1596
Translator axioms: 0
Translator task size: 15302
Translator peak memory: 45004 KB
Writing output... [0.260s CPU, 0.278s wall-clock]
Done! [2.940s CPU, 2.955s wall-clock]
planner.py version 0.0.1

Time:	 0.81s
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.29s
Memory:		 572MB (+481MB)
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 1+
Calls        : 1
Time         : 9.394s (Solving: 0.14s 1st Model: 0.12s Unsat: 0.00s)
CPU Time     : 9.284s

Choices      : 13748    (Domain: 13642)
Conflicts    : 48       (Analyzed: 48)
Restarts     : 0       
Model-Level  : 4458.0  
Problems     : 1        (Average Length: 117.00 Splits: 0)
Lemmas       : 48       (Deleted: 0)
  Binary     : 13       (Ratio:  27.08%)
  Ternary    : 0        (Ratio:   0.00%)
  Conflict   : 48       (Average Length:   39.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 48       (Average: 195.98 Max: 1710 Sum:   9407)
  Executed   : 48       (Average: 195.98 Max: 1710 Sum:   9407 Ratio: 100.00%)
  Bounded    : 0        (Average:  0.00 Max:   0 Sum:      0 Ratio:   0.00%)

Rules        : 0       
Atoms        : 0       
Bodies       : 0       
Tight        : Yes
Variables    : 322152   (Eliminated:    0 Frozen: 2990)
Constraints  : 2576091  (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.81s
Memory:		 765MB (+13MB)
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 2
Time         : 39.387s (Solving: 27.03s 1st Model: 0.12s Unsat: 0.00s)
CPU Time     : 39.292s

Choices      : 2210340  (Domain: 2166906)
Conflicts    : 26616    (Analyzed: 26616)
Restarts     : 100      (Average: 266.16 Last: 122)
Model-Level  : 4458.0  
Problems     : 2        (Average Length: 117.00 Splits: 0)
Lemmas       : 26616    (Deleted: 19232)
  Binary     : 1779     (Ratio:   6.68%)
  Ternary    : 563      (Ratio:   2.12%)
  Conflict   : 26616    (Average Length:  428.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 26616    (Average: 81.92 Max: 1710 Sum: 2180286)
  Executed   : 26607    (Average: 81.88 Max: 1710 Sum: 2179237 Ratio:  99.95%)
  Bounded    : 9        (Average: 116.56 Max: 117 Sum:   1049 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    : 578204   (Eliminated:    0 Frozen: 191082)
Constraints  : 4250110  (Binary:  91.4% Ternary:   7.1% Other:   1.6%)

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

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

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

Models       : 0+
Calls        : 3
Time         : 64.617s (Solving: 52.13s 1st Model: 0.12s Unsat: 0.00s)
CPU Time     : 64.532s

Choices      : 3819039  (Domain: 3764204)
Conflicts    : 52153    (Analyzed: 52153)
Restarts     : 200      (Average: 260.76 Last: 122)
Model-Level  : 4458.0  
Problems     : 3        (Average Length: 117.00 Splits: 0)
Lemmas       : 52153    (Deleted: 40057)
  Binary     : 3369     (Ratio:   6.46%)
  Ternary    : 1040     (Ratio:   1.99%)
  Conflict   : 52153    (Average Length:  355.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 52153    (Average: 72.23 Max: 1710 Sum: 3766925)
  Executed   : 52127    (Average: 72.17 Max: 1710 Sum: 3763903 Ratio:  99.92%)
  Bounded    : 26       (Average: 116.23 Max: 117 Sum:   3022 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    : 578204   (Eliminated:    0 Frozen: 191082)
Constraints  : 4245825  (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         : 88.718s (Solving: 76.10s 1st Model: 0.12s Unsat: 0.00s)
CPU Time     : 88.644s

Choices      : 4860106  (Domain: 4798622)
Conflicts    : 74369    (Analyzed: 74369)
Restarts     : 300      (Average: 247.90 Last: 335)
Model-Level  : 4458.0  
Problems     : 4        (Average Length: 117.00 Splits: 0)
Lemmas       : 74369    (Deleted: 60954)
  Binary     : 4120     (Ratio:   5.54%)
  Ternary    : 1231     (Ratio:   1.66%)
  Conflict   : 74369    (Average Length:  336.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 74369    (Average: 64.40 Max: 1710 Sum: 4789607)
  Executed   : 74331    (Average: 64.34 Max: 1710 Sum: 4785186 Ratio:  99.91%)
  Bounded    : 38       (Average: 116.34 Max: 117 Sum:   4421 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    : 578204   (Eliminated:    0 Frozen: 191082)
Constraints  : 4220244  (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.11s
Memory:		 875MB (+0MB)
UNKNOWN
Iteration Time:	 24.11s

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

Models       : 0+
Calls        : 5
Time         : 112.919s (Solving: 100.19s 1st Model: 0.12s Unsat: 0.00s)
CPU Time     : 112.852s

Choices      : 5683276  (Domain: 5615233)
Conflicts    : 100776   (Analyzed: 100776)
Restarts     : 400      (Average: 251.94 Last: 335)
Model-Level  : 4458.0  
Problems     : 5        (Average Length: 117.00 Splits: 0)
Lemmas       : 100776   (Deleted: 83756)
  Binary     : 4829     (Ratio:   4.79%)
  Ternary    : 1386     (Ratio:   1.38%)
  Conflict   : 100776   (Average Length:  355.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 100776   (Average: 55.55 Max: 1710 Sum: 5598037)
  Executed   : 100725   (Average: 55.49 Max: 1710 Sum: 5592104 Ratio:  99.89%)
  Bounded    : 51       (Average: 116.33 Max: 117 Sum:   5933 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    : 578204   (Eliminated:    0 Frozen: 191082)
Constraints  : 4198205  (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.21s
Memory:		 875MB (+0MB)
UNKNOWN
Iteration Time:	 24.21s

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

Models       : 0+
Calls        : 6
Time         : 135.445s (Solving: 122.61s 1st Model: 0.12s Unsat: 0.00s)
CPU Time     : 135.388s

Choices      : 6244930  (Domain: 6174877)
Conflicts    : 125294   (Analyzed: 125294)
Restarts     : 500      (Average: 250.59 Last: 335)
Model-Level  : 4458.0  
Problems     : 6        (Average Length: 117.00 Splits: 0)
Lemmas       : 125294   (Deleted: 106000)
  Binary     : 5400     (Ratio:   4.31%)
  Ternary    : 1474     (Ratio:   1.18%)
  Conflict   : 125294   (Average Length:  347.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 125294   (Average: 49.03 Max: 1710 Sum: 6142896)
  Executed   : 125238   (Average: 48.98 Max: 1710 Sum: 6136388 Ratio:  99.89%)
  Bounded    : 56       (Average: 116.21 Max: 117 Sum:   6508 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    : 578204   (Eliminated:    0 Frozen: 191082)
Constraints  : 4191670  (Binary:  91.4% Ternary:   7.0% Other:   1.6%)

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

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

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

Models       : 0+
Calls        : 7
Time         : 151.101s (Solving: 138.16s 1st Model: 0.12s Unsat: 0.00s)
CPU Time     : 151.048s

Choices      : 6497853  (Domain: 6427179)
Conflicts    : 148196   (Analyzed: 148196)
Restarts     : 600      (Average: 246.99 Last: 335)
Model-Level  : 4458.0  
Problems     : 7        (Average Length: 117.00 Splits: 0)
Lemmas       : 148196   (Deleted: 129346)
  Binary     : 5617     (Ratio:   3.79%)
  Ternary    : 1536     (Ratio:   1.04%)
  Conflict   : 148196   (Average Length:  332.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 148196   (Average: 43.06 Max: 1710 Sum: 6380692)
  Executed   : 148135   (Average: 43.01 Max: 1710 Sum: 6373611 Ratio:  99.89%)
  Bounded    : 61       (Average: 116.08 Max: 117 Sum:   7081 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    : 578204   (Eliminated:    0 Frozen: 191082)
Constraints  : 4189699  (Binary:  91.4% Ternary:   7.0% Other:   1.6%)

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

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

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

Models       : 0+
Calls        : 8
Time         : 169.842s (Solving: 156.80s 1st Model: 0.12s Unsat: 0.00s)
CPU Time     : 169.800s

Choices      : 7164741  (Domain: 7091037)
Conflicts    : 175296   (Analyzed: 175296)
Restarts     : 700      (Average: 250.42 Last: 335)
Model-Level  : 4458.0  
Problems     : 8        (Average Length: 117.00 Splits: 0)
Lemmas       : 175296   (Deleted: 154010)
  Binary     : 6036     (Ratio:   3.44%)
  Ternary    : 1584     (Ratio:   0.90%)
  Conflict   : 175296   (Average Length:  360.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 175296   (Average: 40.10 Max: 1710 Sum: 7029169)
  Executed   : 175232   (Average: 40.06 Max: 1710 Sum: 7021740 Ratio:  99.89%)
  Bounded    : 64       (Average: 116.08 Max: 117 Sum:   7429 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    : 578204   (Eliminated:    0 Frozen: 191082)
Constraints  : 4189662  (Binary:  91.4% Ternary:   7.0% Other:   1.6%)

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

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

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

Models       : 0+
Calls        : 9
Time         : 188.198s (Solving: 175.04s 1st Model: 0.12s Unsat: 0.00s)
CPU Time     : 188.164s

Choices      : 7869223  (Domain: 7792044)
Conflicts    : 200448   (Analyzed: 200448)
Restarts     : 800      (Average: 250.56 Last: 335)
Model-Level  : 4458.0  
Problems     : 9        (Average Length: 117.00 Splits: 0)
Lemmas       : 200448   (Deleted: 180130)
  Binary     : 6389     (Ratio:   3.19%)
  Ternary    : 1622     (Ratio:   0.81%)
  Conflict   : 200448   (Average Length:  382.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 200448   (Average: 38.49 Max: 1710 Sum: 7715735)
  Executed   : 200382   (Average: 38.45 Max: 1710 Sum: 7708072 Ratio:  99.90%)
  Bounded    : 66       (Average: 116.11 Max: 117 Sum:   7663 Ratio:   0.10%)

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    : 578204   (Eliminated:    0 Frozen: 191082)
Constraints  : 4187549  (Binary:  91.4% Ternary:   7.0% Other:   1.6%)

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

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

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

Models       : 0+
Calls        : 10
Time         : 205.841s (Solving: 192.59s 1st Model: 0.12s Unsat: 0.00s)
CPU Time     : 205.816s

Choices      : 8378722  (Domain: 8299408)
Conflicts    : 226118   (Analyzed: 226118)
Restarts     : 900      (Average: 251.24 Last: 335)
Model-Level  : 4458.0  
Problems     : 10       (Average Length: 117.00 Splits: 0)
Lemmas       : 226118   (Deleted: 204527)
  Binary     : 6609     (Ratio:   2.92%)
  Ternary    : 1659     (Ratio:   0.73%)
  Conflict   : 226118   (Average Length:  387.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 226118   (Average: 36.30 Max: 1710 Sum: 8208004)
  Executed   : 226049   (Average: 36.26 Max: 1710 Sum: 8199995 Ratio:  99.90%)
  Bounded    : 69       (Average: 116.07 Max: 117 Sum:   8009 Ratio:   0.10%)

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    : 578204   (Eliminated:    0 Frozen: 191082)
Constraints  : 4187509  (Binary:  91.4% Ternary:   7.0% Other:   1.6%)

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

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

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

Models       : 0+
Calls        : 11
Time         : 224.861s (Solving: 211.50s 1st Model: 0.12s Unsat: 0.00s)
CPU Time     : 224.844s

Choices      : 9021688  (Domain: 8939280)
Conflicts    : 252081   (Analyzed: 252081)
Restarts     : 1000     (Average: 252.08 Last: 335)
Model-Level  : 4458.0  
Problems     : 11       (Average Length: 117.00 Splits: 0)
Lemmas       : 252081   (Deleted: 229333)
  Binary     : 6854     (Ratio:   2.72%)
  Ternary    : 1699     (Ratio:   0.67%)
  Conflict   : 252081   (Average Length:  400.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 252081   (Average: 35.04 Max: 1710 Sum: 8831845)
  Executed   : 252012   (Average: 35.00 Max: 1710 Sum: 8823836 Ratio:  99.91%)
  Bounded    : 69       (Average: 116.07 Max: 117 Sum:   8009 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    : 578204   (Eliminated:    0 Frozen: 191082)
Constraints  : 4187481  (Binary:  91.4% Ternary:   7.0% Other:   1.6%)

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

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

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

Models       : 0+
Calls        : 12
Time         : 248.529s (Solving: 235.05s 1st Model: 0.12s Unsat: 0.00s)
CPU Time     : 248.520s

Choices      : 10009482 (Domain: 9920282)
Conflicts    : 280696   (Analyzed: 280696)
Restarts     : 1100     (Average: 255.18 Last: 335)
Model-Level  : 4458.0  
Problems     : 12       (Average Length: 117.00 Splits: 0)
Lemmas       : 280696   (Deleted: 257172)
  Binary     : 7236     (Ratio:   2.58%)
  Ternary    : 1755     (Ratio:   0.63%)
  Conflict   : 280696   (Average Length:  431.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 280696   (Average: 34.90 Max: 1710 Sum: 9796138)
  Executed   : 280627   (Average: 34.87 Max: 1710 Sum: 9788129 Ratio:  99.92%)
  Bounded    : 69       (Average: 116.07 Max: 117 Sum:   8009 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    : 578204   (Eliminated:    0 Frozen: 191082)
Constraints  : 4187481  (Binary:  91.4% Ternary:   7.0% Other:   1.6%)

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

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

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

Models       : 0+
Calls        : 13
Time         : 272.861s (Solving: 259.25s 1st Model: 0.12s Unsat: 0.00s)
CPU Time     : 272.860s

Choices      : 10892764 (Domain: 10798224)
Conflicts    : 306210   (Analyzed: 306210)
Restarts     : 1200     (Average: 255.18 Last: 335)
Model-Level  : 4458.0  
Problems     : 13       (Average Length: 117.00 Splits: 0)
Lemmas       : 306210   (Deleted: 281774)
  Binary     : 7752     (Ratio:   2.53%)
  Ternary    : 1790     (Ratio:   0.58%)
  Conflict   : 306210   (Average Length:  518.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 306210   (Average: 34.77 Max: 1710 Sum: 10648444)
  Executed   : 306141   (Average: 34.75 Max: 1710 Sum: 10640435 Ratio:  99.92%)
  Bounded    : 69       (Average: 116.07 Max: 117 Sum:   8009 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    : 578204   (Eliminated:    0 Frozen: 191082)
Constraints  : 4187481  (Binary:  91.4% Ternary:   7.0% Other:   1.6%)

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

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

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

Models       : 0+
Calls        : 14
Time         : 291.993s (Solving: 278.28s 1st Model: 0.12s Unsat: 0.00s)
CPU Time     : 292.000s

Choices      : 11550113 (Domain: 11451772)
Conflicts    : 331154   (Analyzed: 331154)
Restarts     : 1300     (Average: 254.73 Last: 335)
Model-Level  : 4458.0  
Problems     : 14       (Average Length: 117.00 Splits: 0)
Lemmas       : 331154   (Deleted: 305989)
  Binary     : 8249     (Ratio:   2.49%)
  Ternary    : 1878     (Ratio:   0.57%)
  Conflict   : 331154   (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    : 331154   (Average: 34.08 Max: 1710 Sum: 11285334)
  Executed   : 331085   (Average: 34.05 Max: 1710 Sum: 11277325 Ratio:  99.93%)
  Bounded    : 69       (Average: 116.07 Max: 117 Sum:   8009 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    : 578204   (Eliminated:    0 Frozen: 191082)
Constraints  : 4187481  (Binary:  91.4% Ternary:   7.0% Other:   1.6%)

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

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

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

Models       : 0+
Calls        : 15
Time         : 314.623s (Solving: 300.78s 1st Model: 0.12s Unsat: 0.00s)
CPU Time     : 314.640s

Choices      : 12434998 (Domain: 12330302)
Conflicts    : 355478   (Analyzed: 355478)
Restarts     : 1400     (Average: 253.91 Last: 335)
Model-Level  : 4458.0  
Problems     : 15       (Average Length: 117.00 Splits: 0)
Lemmas       : 355478   (Deleted: 327131)
  Binary     : 8814     (Ratio:   2.48%)
  Ternary    : 1941     (Ratio:   0.55%)
  Conflict   : 355478   (Average Length:  568.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 355478   (Average: 34.14 Max: 1710 Sum: 12136324)
  Executed   : 355409   (Average: 34.12 Max: 1710 Sum: 12128315 Ratio:  99.93%)
  Bounded    : 69       (Average: 116.07 Max: 117 Sum:   8009 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    : 578204   (Eliminated:    0 Frozen: 191082)
Constraints  : 4187481  (Binary:  91.4% Ternary:   7.0% Other:   1.6%)

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

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

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

Models       : 0+
Calls        : 16
Time         : 338.118s (Solving: 324.17s 1st Model: 0.12s Unsat: 0.00s)
CPU Time     : 338.148s

Choices      : 13679846 (Domain: 13564018)
Conflicts    : 382290   (Analyzed: 382290)
Restarts     : 1500     (Average: 254.86 Last: 335)
Model-Level  : 4458.0  
Problems     : 16       (Average Length: 117.00 Splits: 0)
Lemmas       : 382290   (Deleted: 351722)
  Binary     : 10054    (Ratio:   2.63%)
  Ternary    : 2177     (Ratio:   0.57%)
  Conflict   : 382290   (Average Length:  592.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 382290   (Average: 34.91 Max: 1710 Sum: 13346994)
  Executed   : 382220   (Average: 34.89 Max: 1710 Sum: 13338868 Ratio:  99.94%)
  Bounded    : 70       (Average: 116.09 Max: 117 Sum:   8126 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    : 578204   (Eliminated:    0 Frozen: 191082)
Constraints  : 4187481  (Binary:  91.4% Ternary:   7.0% Other:   1.6%)

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

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

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

Models       : 0+
Calls        : 17
Time         : 364.905s (Solving: 350.86s 1st Model: 0.12s Unsat: 0.00s)
CPU Time     : 364.948s

Choices      : 14898108 (Domain: 14772169)
Conflicts    : 411052   (Analyzed: 411052)
Restarts     : 1600     (Average: 256.91 Last: 335)
Model-Level  : 4458.0  
Problems     : 17       (Average Length: 117.00 Splits: 0)
Lemmas       : 411052   (Deleted: 378185)
  Binary     : 11725    (Ratio:   2.85%)
  Ternary    : 2578     (Ratio:   0.63%)
  Conflict   : 411052   (Average Length:  601.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 411052   (Average: 35.34 Max: 1710 Sum: 14527797)
  Executed   : 410982   (Average: 35.32 Max: 1710 Sum: 14519671 Ratio:  99.94%)
  Bounded    : 70       (Average: 116.09 Max: 117 Sum:   8126 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    : 578204   (Eliminated:    0 Frozen: 191082)
Constraints  : 4187456  (Binary:  91.4% Ternary:   7.0% Other:   1.6%)

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

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

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

Models       : 0+
Calls        : 18
Time         : 390.409s (Solving: 376.27s 1st Model: 0.12s Unsat: 0.00s)
CPU Time     : 390.460s

Choices      : 15646539 (Domain: 15519362)
Conflicts    : 438334   (Analyzed: 438334)
Restarts     : 1700     (Average: 257.84 Last: 335)
Model-Level  : 4458.0  
Problems     : 18       (Average Length: 117.00 Splits: 0)
Lemmas       : 438334   (Deleted: 402729)
  Binary     : 12404    (Ratio:   2.83%)
  Ternary    : 2734     (Ratio:   0.62%)
  Conflict   : 438334   (Average Length:  616.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 438334   (Average: 34.79 Max: 1710 Sum: 15248427)
  Executed   : 438263   (Average: 34.77 Max: 1710 Sum: 15240184 Ratio:  99.95%)
  Bounded    : 71       (Average: 116.10 Max: 117 Sum:   8243 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    : 578204   (Eliminated:    0 Frozen: 191082)
Constraints  : 4187456  (Binary:  91.4% Ternary:   7.0% Other:   1.6%)

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

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

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

Models       : 0+
Calls        : 19
Time         : 416.010s (Solving: 401.76s 1st Model: 0.12s Unsat: 0.00s)
CPU Time     : 416.072s

Choices      : 16425618 (Domain: 16296146)
Conflicts    : 463808   (Analyzed: 463808)
Restarts     : 1800     (Average: 257.67 Last: 335)
Model-Level  : 4458.0  
Problems     : 19       (Average Length: 117.00 Splits: 0)
Lemmas       : 463808   (Deleted: 428032)
  Binary     : 13200    (Ratio:   2.85%)
  Ternary    : 2889     (Ratio:   0.62%)
  Conflict   : 463808   (Average Length:  633.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 463808   (Average: 34.47 Max: 1710 Sum: 15986081)
  Executed   : 463737   (Average: 34.45 Max: 1710 Sum: 15977838 Ratio:  99.95%)
  Bounded    : 71       (Average: 116.10 Max: 117 Sum:   8243 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    : 578204   (Eliminated:    0 Frozen: 191082)
Constraints  : 4187442  (Binary:  91.4% Ternary:   7.0% Other:   1.6%)

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

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

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

Models       : 0+
Calls        : 20
Time         : 438.430s (Solving: 424.05s 1st Model: 0.12s Unsat: 0.00s)
CPU Time     : 438.504s

Choices      : 16926726 (Domain: 16796831)
Conflicts    : 489123   (Analyzed: 489123)
Restarts     : 1900     (Average: 257.43 Last: 335)
Model-Level  : 4458.0  
Problems     : 20       (Average Length: 117.00 Splits: 0)
Lemmas       : 489123   (Deleted: 452281)
  Binary     : 13727    (Ratio:   2.81%)
  Ternary    : 2974     (Ratio:   0.61%)
  Conflict   : 489123   (Average Length:  669.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 489123   (Average: 33.63 Max: 1710 Sum: 16451179)
  Executed   : 489051   (Average: 33.62 Max: 1710 Sum: 16442819 Ratio:  99.95%)
  Bounded    : 72       (Average: 116.11 Max: 117 Sum:   8360 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    : 578204   (Eliminated:    0 Frozen: 191082)
Constraints  : 4187442  (Binary:  91.4% Ternary:   7.0% Other:   1.6%)

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

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

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

Models       : 0+
Calls        : 21
Time         : 461.173s (Solving: 446.69s 1st Model: 0.12s Unsat: 0.00s)
CPU Time     : 461.256s

Choices      : 17539629 (Domain: 17409196)
Conflicts    : 515162   (Analyzed: 515162)
Restarts     : 2000     (Average: 257.58 Last: 335)
Model-Level  : 4458.0  
Problems     : 21       (Average Length: 117.00 Splits: 0)
Lemmas       : 515162   (Deleted: 476141)
  Binary     : 14307    (Ratio:   2.78%)
  Ternary    : 3145     (Ratio:   0.61%)
  Conflict   : 515162   (Average Length:  679.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 515162   (Average: 33.05 Max: 1710 Sum: 17028320)
  Executed   : 515090   (Average: 33.04 Max: 1710 Sum: 17019960 Ratio:  99.95%)
  Bounded    : 72       (Average: 116.11 Max: 117 Sum:   8360 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    : 578204   (Eliminated:    0 Frozen: 191082)
Constraints  : 4187428  (Binary:  91.4% Ternary:   7.0% Other:   1.6%)

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

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

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

Models       : 0+
Calls        : 22
Time         : 483.634s (Solving: 469.05s 1st Model: 0.12s Unsat: 0.00s)
CPU Time     : 483.728s

Choices      : 17917058 (Domain: 17786352)
Conflicts    : 540847   (Analyzed: 540847)
Restarts     : 2100     (Average: 257.55 Last: 335)
Model-Level  : 4458.0  
Problems     : 22       (Average Length: 117.00 Splits: 0)
Lemmas       : 540847   (Deleted: 501401)
  Binary     : 14721    (Ratio:   2.72%)
  Ternary    : 3201     (Ratio:   0.59%)
  Conflict   : 540847   (Average Length:  712.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 540847   (Average: 32.12 Max: 1710 Sum: 17372376)
  Executed   : 540775   (Average: 32.11 Max: 1710 Sum: 17364016 Ratio:  99.95%)
  Bounded    : 72       (Average: 116.11 Max: 117 Sum:   8360 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    : 578204   (Eliminated:    0 Frozen: 191082)
Constraints  : 4187428  (Binary:  91.4% Ternary:   7.0% Other:   1.6%)

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

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

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

Models       : 0+
Calls        : 23
Time         : 506.268s (Solving: 491.57s 1st Model: 0.12s Unsat: 0.00s)
CPU Time     : 506.372s

Choices      : 18439874 (Domain: 18308790)
Conflicts    : 566838   (Analyzed: 566838)
Restarts     : 2200     (Average: 257.65 Last: 335)
Model-Level  : 4458.0  
Problems     : 23       (Average Length: 117.00 Splits: 0)
Lemmas       : 566838   (Deleted: 525976)
  Binary     : 15257    (Ratio:   2.69%)
  Ternary    : 3301     (Ratio:   0.58%)
  Conflict   : 566838   (Average Length:  723.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 566838   (Average: 31.50 Max: 1710 Sum: 17855877)
  Executed   : 566766   (Average: 31.49 Max: 1710 Sum: 17847517 Ratio:  99.95%)
  Bounded    : 72       (Average: 116.11 Max: 117 Sum:   8360 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    : 578204   (Eliminated:    0 Frozen: 191082)
Constraints  : 4187428  (Binary:  91.4% Ternary:   7.0% Other:   1.6%)

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

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

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

Models       : 0+
Calls        : 24
Time         : 527.311s (Solving: 512.51s 1st Model: 0.12s Unsat: 0.00s)
CPU Time     : 527.424s

Choices      : 18770678 (Domain: 18639456)
Conflicts    : 592502   (Analyzed: 592502)
Restarts     : 2300     (Average: 257.61 Last: 335)
Model-Level  : 4458.0  
Problems     : 24       (Average Length: 117.00 Splits: 0)
Lemmas       : 592502   (Deleted: 551135)
  Binary     : 15548    (Ratio:   2.62%)
  Ternary    : 3363     (Ratio:   0.57%)
  Conflict   : 592502   (Average Length:  729.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 592502   (Average: 30.65 Max: 1710 Sum: 18157293)
  Executed   : 592429   (Average: 30.63 Max: 1710 Sum: 18148816 Ratio:  99.95%)
  Bounded    : 73       (Average: 116.12 Max: 117 Sum:   8477 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    : 578204   (Eliminated:    0 Frozen: 191082)
Constraints  : 4187428  (Binary:  91.4% Ternary:   7.0% Other:   1.6%)

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

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

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

Models       : 0+
Calls        : 25
Time         : 550.172s (Solving: 535.26s 1st Model: 0.12s Unsat: 0.00s)
CPU Time     : 550.296s

Choices      : 19223509 (Domain: 19092031)
Conflicts    : 619550   (Analyzed: 619550)
Restarts     : 2400     (Average: 258.15 Last: 335)
Model-Level  : 4458.0  
Problems     : 25       (Average Length: 117.00 Splits: 0)
Lemmas       : 619550   (Deleted: 575711)
  Binary     : 16121    (Ratio:   2.60%)
  Ternary    : 3455     (Ratio:   0.56%)
  Conflict   : 619550   (Average Length:  748.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 619550   (Average: 29.96 Max: 1710 Sum: 18562270)
  Executed   : 619477   (Average: 29.95 Max: 1710 Sum: 18553793 Ratio:  99.95%)
  Bounded    : 73       (Average: 116.12 Max: 117 Sum:   8477 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    : 578204   (Eliminated:    0 Frozen: 191082)
Constraints  : 4187414  (Binary:  91.4% Ternary:   7.0% Other:   1.6%)

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

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

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

Models       : 0+
Calls        : 26
Time         : 568.589s (Solving: 553.58s 1st Model: 0.12s Unsat: 0.00s)
CPU Time     : 568.720s

Choices      : 19572211 (Domain: 19440436)
Conflicts    : 644862   (Analyzed: 644862)
Restarts     : 2500     (Average: 257.94 Last: 335)
Model-Level  : 4458.0  
Problems     : 26       (Average Length: 117.00 Splits: 0)
Lemmas       : 644862   (Deleted: 601679)
  Binary     : 16512    (Ratio:   2.56%)
  Ternary    : 3522     (Ratio:   0.55%)
  Conflict   : 644862   (Average Length:  757.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 644862   (Average: 29.27 Max: 1710 Sum: 18871991)
  Executed   : 644789   (Average: 29.25 Max: 1710 Sum: 18863514 Ratio:  99.96%)
  Bounded    : 73       (Average: 116.12 Max: 117 Sum:   8477 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    : 578204   (Eliminated:    0 Frozen: 191082)
Constraints  : 4187414  (Binary:  91.4% Ternary:   7.0% Other:   1.6%)

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

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

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

Models       : 0+
Calls        : 27
Time         : 589.964s (Solving: 574.82s 1st Model: 0.12s Unsat: 0.00s)
CPU Time     : 590.108s

Choices      : 19992543 (Domain: 19860490)
Conflicts    : 671146   (Analyzed: 671146)
Restarts     : 2600     (Average: 258.13 Last: 335)
Model-Level  : 4458.0  
Problems     : 27       (Average Length: 117.00 Splits: 0)
Lemmas       : 671146   (Deleted: 626135)
  Binary     : 16880    (Ratio:   2.52%)
  Ternary    : 3591     (Ratio:   0.54%)
  Conflict   : 671146   (Average Length:  765.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 671146   (Average: 28.69 Max: 1710 Sum: 19251930)
  Executed   : 671073   (Average: 28.67 Max: 1710 Sum: 19243453 Ratio:  99.96%)
  Bounded    : 73       (Average: 116.12 Max: 117 Sum:   8477 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    : 578204   (Eliminated:    0 Frozen: 191082)
Constraints  : 4187414  (Binary:  91.4% Ternary:   7.0% Other:   1.6%)

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

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

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

Models       : 0+
Calls        : 28
Time         : 613.256s (Solving: 597.98s 1st Model: 0.12s Unsat: 0.00s)
CPU Time     : 613.412s

Choices      : 20394313 (Domain: 20261983)
Conflicts    : 699850   (Analyzed: 699850)
Restarts     : 2700     (Average: 259.20 Last: 335)
Model-Level  : 4458.0  
Problems     : 28       (Average Length: 117.00 Splits: 0)
Lemmas       : 699850   (Deleted: 654322)
  Binary     : 17244    (Ratio:   2.46%)
  Ternary    : 3645     (Ratio:   0.52%)
  Conflict   : 699850   (Average Length:  793.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 699850   (Average: 28.03 Max: 1710 Sum: 19614959)
  Executed   : 699777   (Average: 28.02 Max: 1710 Sum: 19606482 Ratio:  99.96%)
  Bounded    : 73       (Average: 116.12 Max: 117 Sum:   8477 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    : 578204   (Eliminated:    0 Frozen: 191082)
Constraints  : 4187414  (Binary:  91.4% Ternary:   7.0% Other:   1.6%)

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

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

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

Models       : 0+
Calls        : 29
Time         : 635.069s (Solving: 619.67s 1st Model: 0.12s Unsat: 0.00s)
CPU Time     : 635.236s

Choices      : 20713984 (Domain: 20581584)
Conflicts    : 728406   (Analyzed: 728406)
Restarts     : 2800     (Average: 260.14 Last: 335)
Model-Level  : 4458.0  
Problems     : 29       (Average Length: 117.00 Splits: 0)
Lemmas       : 728406   (Deleted: 682154)
  Binary     : 17500    (Ratio:   2.40%)
  Ternary    : 3696     (Ratio:   0.51%)
  Conflict   : 728406   (Average Length:  811.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 728406   (Average: 27.32 Max: 1710 Sum: 19897452)
  Executed   : 728333   (Average: 27.30 Max: 1710 Sum: 19888975 Ratio:  99.96%)
  Bounded    : 73       (Average: 116.12 Max: 117 Sum:   8477 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    : 578204   (Eliminated:    0 Frozen: 191082)
Constraints  : 4187414  (Binary:  91.4% Ternary:   7.0% Other:   1.6%)

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

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

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

Models       : 0+
Calls        : 30
Time         : 656.134s (Solving: 640.64s 1st Model: 0.12s Unsat: 0.00s)
CPU Time     : 656.308s

Choices      : 21056953 (Domain: 20924422)
Conflicts    : 754225   (Analyzed: 754225)
Restarts     : 2900     (Average: 260.08 Last: 335)
Model-Level  : 4458.0  
Problems     : 30       (Average Length: 117.00 Splits: 0)
Lemmas       : 754225   (Deleted: 707069)
  Binary     : 17800    (Ratio:   2.36%)
  Ternary    : 3757     (Ratio:   0.50%)
  Conflict   : 754225   (Average Length:  820.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 754225   (Average: 26.78 Max: 1710 Sum: 20194849)
  Executed   : 754152   (Average: 26.76 Max: 1710 Sum: 20186372 Ratio:  99.96%)
  Bounded    : 73       (Average: 116.12 Max: 117 Sum:   8477 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    : 578204   (Eliminated:    0 Frozen: 191082)
Constraints  : 4187414  (Binary:  91.4% Ternary:   7.0% Other:   1.6%)

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

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

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

Models       : 0+
Calls        : 31
Time         : 675.464s (Solving: 659.83s 1st Model: 0.12s Unsat: 0.00s)
CPU Time     : 675.648s

Choices      : 21417583 (Domain: 21284892)
Conflicts    : 778962   (Analyzed: 778962)
Restarts     : 3000     (Average: 259.65 Last: 335)
Model-Level  : 4458.0  
Problems     : 31       (Average Length: 117.00 Splits: 0)
Lemmas       : 778962   (Deleted: 732240)
  Binary     : 18040    (Ratio:   2.32%)
  Ternary    : 3807     (Ratio:   0.49%)
  Conflict   : 778962   (Average Length:  830.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 778962   (Average: 26.33 Max: 1710 Sum: 20509406)
  Executed   : 778889   (Average: 26.32 Max: 1710 Sum: 20500929 Ratio:  99.96%)
  Bounded    : 73       (Average: 116.12 Max: 117 Sum:   8477 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    : 578204   (Eliminated:    0 Frozen: 191082)
Constraints  : 4187414  (Binary:  91.4% Ternary:   7.0% Other:   1.6%)

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

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

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

Models       : 0+
Calls        : 32
Time         : 689.932s (Solving: 674.20s 1st Model: 0.12s Unsat: 0.00s)
CPU Time     : 690.124s

Choices      : 21641120 (Domain: 21508429)
Conflicts    : 803546   (Analyzed: 803546)
Restarts     : 3100     (Average: 259.21 Last: 335)
Model-Level  : 4458.0  
Problems     : 32       (Average Length: 117.00 Splits: 0)
Lemmas       : 803546   (Deleted: 756419)
  Binary     : 18319    (Ratio:   2.28%)
  Ternary    : 3836     (Ratio:   0.48%)
  Conflict   : 803546   (Average Length:  820.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 803546   (Average: 25.77 Max: 1710 Sum: 20704788)
  Executed   : 803473   (Average: 25.76 Max: 1710 Sum: 20696311 Ratio:  99.96%)
  Bounded    : 73       (Average: 116.12 Max: 117 Sum:   8477 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    : 578204   (Eliminated:    0 Frozen: 191082)
Constraints  : 4187414  (Binary:  91.4% Ternary:   7.0% Other:   1.6%)

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

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

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

Models       : 0+
Calls        : 33
Time         : 710.255s (Solving: 694.42s 1st Model: 0.12s Unsat: 0.00s)
CPU Time     : 710.452s

Choices      : 22002113 (Domain: 21869313)
Conflicts    : 829441   (Analyzed: 829441)
Restarts     : 3200     (Average: 259.20 Last: 335)
Model-Level  : 4458.0  
Problems     : 33       (Average Length: 117.00 Splits: 0)
Lemmas       : 829441   (Deleted: 780249)
  Binary     : 18547    (Ratio:   2.24%)
  Ternary    : 3907     (Ratio:   0.47%)
  Conflict   : 829441   (Average Length:  826.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 829441   (Average: 25.35 Max: 1710 Sum: 21024639)
  Executed   : 829368   (Average: 25.34 Max: 1710 Sum: 21016162 Ratio:  99.96%)
  Bounded    : 73       (Average: 116.12 Max: 117 Sum:   8477 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    : 578204   (Eliminated:    0 Frozen: 191082)
Constraints  : 4187414  (Binary:  91.4% Ternary:   7.0% Other:   1.6%)

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

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

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

Models       : 0+
Calls        : 34
Time         : 731.868s (Solving: 715.93s 1st Model: 0.12s Unsat: 0.00s)
CPU Time     : 732.072s

Choices      : 22389575 (Domain: 22256714)
Conflicts    : 856248   (Analyzed: 856248)
Restarts     : 3300     (Average: 259.47 Last: 335)
Model-Level  : 4458.0  
Problems     : 34       (Average Length: 117.00 Splits: 0)
Lemmas       : 856248   (Deleted: 805335)
  Binary     : 18808    (Ratio:   2.20%)
  Ternary    : 3975     (Ratio:   0.46%)
  Conflict   : 856248   (Average Length:  832.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 856248   (Average: 24.95 Max: 1710 Sum: 21366030)
  Executed   : 856175   (Average: 24.94 Max: 1710 Sum: 21357553 Ratio:  99.96%)
  Bounded    : 73       (Average: 116.12 Max: 117 Sum:   8477 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    : 578204   (Eliminated:    0 Frozen: 191082)
Constraints  : 4187414  (Binary:  91.4% Ternary:   7.0% Other:   1.6%)

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

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

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

Models       : 0+
Calls        : 35
Time         : 754.049s (Solving: 737.98s 1st Model: 0.12s Unsat: 0.00s)
CPU Time     : 754.260s

Choices      : 22816093 (Domain: 22683070)
Conflicts    : 885216   (Analyzed: 885216)
Restarts     : 3400     (Average: 260.36 Last: 335)
Model-Level  : 4458.0  
Problems     : 35       (Average Length: 117.00 Splits: 0)
Lemmas       : 885216   (Deleted: 834218)
  Binary     : 19158    (Ratio:   2.16%)
  Ternary    : 4052     (Ratio:   0.46%)
  Conflict   : 885216   (Average Length:  836.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 885216   (Average: 24.58 Max: 1710 Sum: 21756417)
  Executed   : 885143   (Average: 24.57 Max: 1710 Sum: 21747940 Ratio:  99.96%)
  Bounded    : 73       (Average: 116.12 Max: 117 Sum:   8477 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    : 578204   (Eliminated:    0 Frozen: 191082)
Constraints  : 4187414  (Binary:  91.4% Ternary:   7.0% Other:   1.6%)

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

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

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

Models       : 0+
Calls        : 36
Time         : 774.501s (Solving: 758.32s 1st Model: 0.12s Unsat: 0.00s)
CPU Time     : 774.724s

Choices      : 23246323 (Domain: 23112798)
Conflicts    : 911945   (Analyzed: 911945)
Restarts     : 3500     (Average: 260.56 Last: 335)
Model-Level  : 4458.0  
Problems     : 36       (Average Length: 117.00 Splits: 0)
Lemmas       : 911945   (Deleted: 859399)
  Binary     : 19452    (Ratio:   2.13%)
  Ternary    : 4136     (Ratio:   0.45%)
  Conflict   : 911945   (Average Length:  836.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 911945   (Average: 24.28 Max: 1710 Sum: 22140215)
  Executed   : 911872   (Average: 24.27 Max: 1710 Sum: 22131738 Ratio:  99.96%)
  Bounded    : 73       (Average: 116.12 Max: 117 Sum:   8477 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    : 578204   (Eliminated:    0 Frozen: 191082)
Constraints  : 4187414  (Binary:  91.4% Ternary:   7.0% Other:   1.6%)

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

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

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

Models       : 0+
Calls        : 37
Time         : 795.112s (Solving: 778.83s 1st Model: 0.12s Unsat: 0.00s)
CPU Time     : 795.344s

Choices      : 23656159 (Domain: 23520947)
Conflicts    : 937577   (Analyzed: 937577)
Restarts     : 3600     (Average: 260.44 Last: 335)
Model-Level  : 4458.0  
Problems     : 37       (Average Length: 117.00 Splits: 0)
Lemmas       : 937577   (Deleted: 885155)
  Binary     : 19800    (Ratio:   2.11%)
  Ternary    : 4192     (Ratio:   0.45%)
  Conflict   : 937577   (Average Length:  843.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 937577   (Average: 24.00 Max: 1710 Sum: 22504848)
  Executed   : 937504   (Average: 23.99 Max: 1710 Sum: 22496371 Ratio:  99.96%)
  Bounded    : 73       (Average: 116.12 Max: 117 Sum:   8477 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    : 578204   (Eliminated:    0 Frozen: 191082)
Constraints  : 4187414  (Binary:  91.4% Ternary:   7.0% Other:   1.6%)

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

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

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

Models       : 0+
Calls        : 38
Time         : 818.720s (Solving: 802.31s 1st Model: 0.12s Unsat: 0.00s)
CPU Time     : 818.964s

Choices      : 24038771 (Domain: 23903490)
Conflicts    : 965333   (Analyzed: 965333)
Restarts     : 3700     (Average: 260.90 Last: 335)
Model-Level  : 4458.0  
Problems     : 38       (Average Length: 117.00 Splits: 0)
Lemmas       : 965333   (Deleted: 913023)
  Binary     : 20061    (Ratio:   2.08%)
  Ternary    : 4248     (Ratio:   0.44%)
  Conflict   : 965333   (Average Length:  855.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 965333   (Average: 23.67 Max: 1710 Sum: 22845683)
  Executed   : 965260   (Average: 23.66 Max: 1710 Sum: 22837206 Ratio:  99.96%)
  Bounded    : 73       (Average: 116.12 Max: 117 Sum:   8477 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    : 578204   (Eliminated:    0 Frozen: 191082)
Constraints  : 4187414  (Binary:  91.4% Ternary:   7.0% Other:   1.6%)

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

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

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

Models       : 0+
Calls        : 39
Time         : 839.848s (Solving: 823.33s 1st Model: 0.12s Unsat: 0.00s)
CPU Time     : 840.104s

Choices      : 24319911 (Domain: 24184626)
Conflicts    : 994656   (Analyzed: 994656)
Restarts     : 3800     (Average: 261.75 Last: 335)
Model-Level  : 4458.0  
Problems     : 39       (Average Length: 117.00 Splits: 0)
Lemmas       : 994656   (Deleted: 940366)
  Binary     : 20169    (Ratio:   2.03%)
  Ternary    : 4268     (Ratio:   0.43%)
  Conflict   : 994656   (Average Length:  859.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 994656   (Average: 23.21 Max: 1710 Sum: 23089388)
  Executed   : 994583   (Average: 23.20 Max: 1710 Sum: 23080911 Ratio:  99.96%)
  Bounded    : 73       (Average: 116.12 Max: 117 Sum:   8477 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    : 578204   (Eliminated:    0 Frozen: 191082)
Constraints  : 4187414  (Binary:  91.4% Ternary:   7.0% Other:   1.6%)

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

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

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

Models       : 0+
Calls        : 40
Time         : 862.662s (Solving: 846.04s 1st Model: 0.12s Unsat: 0.00s)
CPU Time     : 862.928s

Choices      : 24658649 (Domain: 24523278)
Conflicts    : 1023941  (Analyzed: 1023941)
Restarts     : 3900     (Average: 262.55 Last: 335)
Model-Level  : 4458.0  
Problems     : 40       (Average Length: 117.00 Splits: 0)
Lemmas       : 1023941  (Deleted: 969213)
  Binary     : 20503    (Ratio:   2.00%)
  Ternary    : 4322     (Ratio:   0.42%)
  Conflict   : 1023941  (Average Length:  864.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 1023941  (Average: 22.85 Max: 1710 Sum: 23393856)
  Executed   : 1023868  (Average: 22.84 Max: 1710 Sum: 23385379 Ratio:  99.96%)
  Bounded    : 73       (Average: 116.12 Max: 117 Sum:   8477 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    : 578204   (Eliminated:    0 Frozen: 191082)
Constraints  : 4187414  (Binary:  91.4% Ternary:   7.0% Other:   1.6%)

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

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

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

Models       : 0+
Calls        : 41
Time         : 883.322s (Solving: 866.61s 1st Model: 0.12s Unsat: 0.00s)
CPU Time     : 883.596s

Choices      : 25026216 (Domain: 24890755)
Conflicts    : 1051088  (Analyzed: 1051088)
Restarts     : 4000     (Average: 262.77 Last: 335)
Model-Level  : 4458.0  
Problems     : 41       (Average Length: 117.00 Splits: 0)
Lemmas       : 1051088  (Deleted: 994797)
  Binary     : 20659    (Ratio:   1.97%)
  Ternary    : 4381     (Ratio:   0.42%)
  Conflict   : 1051088  (Average Length:  870.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 1051088  (Average: 22.56 Max: 1710 Sum: 23716095)
  Executed   : 1051015  (Average: 22.56 Max: 1710 Sum: 23707618 Ratio:  99.96%)
  Bounded    : 73       (Average: 116.12 Max: 117 Sum:   8477 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    : 578204   (Eliminated:    0 Frozen: 191082)
Constraints  : 4187414  (Binary:  91.4% Ternary:   7.0% Other:   1.6%)

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

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

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

INTERRUPTED  : 1

Models       : 0+
Calls        : 42
Time         : 903.443s (Solving: 886.63s 1st Model: 0.12s Unsat: 0.00s)
CPU Time     : 903.708s

Choices      : 25370116 (Domain: 25233987)
Conflicts    : 1078441  (Analyzed: 1078441)
Restarts     : 4100     (Average: 263.03 Last: 335)
Model-Level  : 4458.0  
Problems     : 42       (Average Length: 117.00 Splits: 0)
Lemmas       : 1078441  (Deleted: 1021140)
  Binary     : 20950    (Ratio:   1.94%)
  Ternary    : 4428     (Ratio:   0.41%)
  Conflict   : 1078441  (Average Length:  876.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 1078441  (Average: 22.27 Max: 1710 Sum: 24015180)
  Executed   : 1078367  (Average: 22.26 Max: 1710 Sum: 24006586 Ratio:  99.96%)
  Bounded    : 74       (Average: 116.14 Max: 117 Sum:   8594 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    : 578204   (Eliminated:    0 Frozen: 191082)
Constraints  : 4187414  (Binary:  91.4% Ternary:   7.0% Other:   1.6%)

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