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-3.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-3.pddl
Parsing...
Parsing: [0.030s CPU, 0.035s wall-clock]
Normalizing task... [0.010s CPU, 0.003s wall-clock]
Instantiating...
Generating Datalog program... [0.010s CPU, 0.009s wall-clock]
Normalizing Datalog program...
Normalizing Datalog program: [0.040s CPU, 0.046s wall-clock]
Preparing model... [0.030s CPU, 0.024s wall-clock]
Generated 115 rules.
Computing model... [0.330s CPU, 0.326s wall-clock]
2025 relevant atoms
2105 auxiliary atoms
4130 final queue length
7122 total queue pushes
Completing instantiation... [0.600s CPU, 0.600s wall-clock]
Instantiating: [1.010s CPU, 1.010s wall-clock]
Computing fact groups...
Finding invariants...
24 initial candidates
Finding invariants: [0.100s CPU, 0.106s wall-clock]
Checking invariant weight... [0.010s CPU, 0.001s wall-clock]
Instantiating groups... [0.000s CPU, 0.006s wall-clock]
Collecting mutex groups... [0.000s CPU, 0.000s wall-clock]
Choosing groups...
207 uncovered facts
Choosing groups: [0.010s CPU, 0.001s wall-clock]
Building translation key... [0.010s CPU, 0.008s wall-clock]
Computing fact groups: [0.140s CPU, 0.137s 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.002s wall-clock]
Translating task...
Processing axioms...
Simplifying axioms... [0.000s CPU, 0.000s wall-clock]
Processing axioms: [0.040s CPU, 0.034s wall-clock]
Translating task: [0.660s CPU, 0.657s wall-clock]
2326 effect conditions simplified
0 implied preconditions added
Detecting unreachable propositions...
0 operators removed
0 axioms removed
3 propositions removed
Detecting unreachable propositions: [0.310s CPU, 0.311s wall-clock]
Reordering and filtering variables...
210 of 210 variables necessary.
11 of 14 mutex groups necessary.
1390 of 1390 operators necessary.
0 of 0 axiom rules necessary.
Reordering and filtering variables: [0.210s CPU, 0.205s wall-clock]
Translator variables: 210
Translator derived variables: 0
Translator facts: 441
Translator goal facts: 9
Translator mutex groups: 11
Translator total mutex groups size: 33
Translator operators: 1390
Translator axioms: 0
Translator task size: 13333
Translator peak memory: 43980 KB
Writing output... [0.220s CPU, 0.241s wall-clock]
Done! [2.610s CPU, 2.632s wall-clock]
planner.py version 0.0.1

Time:	 0.56s
Memory: 86MB

Iteration 1
Queue:		 [(0,100,0,True)]
Grounded Until:	 0
Expected Memory: 86MB
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]), ('check', [100])]
Grounding Time:	 4.01s
Memory:		 457MB (+371MB)
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 1+
Calls        : 1
Time         : 7.089s (Solving: 0.17s 1st Model: 0.15s Unsat: 0.00s)
CPU Time     : 7.004s

Choices      : 27940    (Domain: 27632)
Conflicts    : 155      (Analyzed: 155)
Restarts     : 1        (Average: 155.00 Last: 12)
Model-Level  : 3600.0  
Problems     : 1        (Average Length: 102.00 Splits: 0)
Lemmas       : 155      (Deleted: 0)
  Binary     : 42       (Ratio:  27.10%)
  Ternary    : 0        (Ratio:   0.00%)
  Conflict   : 155      (Average Length:   56.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 155      (Average: 156.45 Max: 1444 Sum:  24249)
  Executed   : 155      (Average: 156.45 Max: 1444 Sum:  24249 Ratio: 100.00%)
  Bounded    : 0        (Average:  0.00 Max:   0 Sum:      0 Ratio:   0.00%)

Rules        : 0       
Atoms        : 0       
Bodies       : 0       
Tight        : Yes
Variables    : 243733   (Eliminated:    0 Frozen: 2400)
Constraints  : 1944219  (Binary:  95.7% Ternary:   3.2% Other:   1.1%)

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

[endof: stats after solve call]
Solving Time:	 0.32s
Memory:		 617MB (+160MB)
SAT
Testing...
NOT SERIALIZABLE
Testing Time:	 2.12s
Memory:		 619MB (+2MB)
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 2
Time         : 29.598s (Solving: 20.42s 1st Model: 0.15s Unsat: 0.00s)
CPU Time     : 29.524s

Choices      : 1381721  (Domain: 1332192)
Conflicts    : 24162    (Analyzed: 24162)
Restarts     : 101      (Average: 239.23 Last: 145)
Model-Level  : 3600.0  
Problems     : 2        (Average Length: 102.00 Splits: 0)
Lemmas       : 24162    (Deleted: 16813)
  Binary     : 1895     (Ratio:   7.84%)
  Ternary    : 480      (Ratio:   1.99%)
  Conflict   : 24162    (Average Length:  455.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 24162    (Average: 56.14 Max: 1444 Sum: 1356436)
  Executed   : 24137    (Average: 56.03 Max: 1444 Sum: 1353901 Ratio:  99.81%)
  Bounded    : 25       (Average: 101.40 Max: 102 Sum:   2535 Ratio:   0.19%)

Rules        : 766922   (Original: 635077)
Atoms        : 45135   
Bodies       : 588251   (Original: 456406)
  Count      : 7639     (Original: 20328)
Equivalences : 142481   (Atom=Atom: 152 Body=Body: 0 Other: 142329)
Tight        : Yes
Variables    : 428921   (Eliminated:    0 Frozen: 144613)
Constraints  : 3173797  (Binary:  91.5% Ternary:   6.9% Other:   1.6%)

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

[endof: stats after solve call]
Solving Time:	 20.98s
Memory:		 713MB (+94MB)
UNKNOWN
Iteration Time:	 29.58s

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

Models       : 0+
Calls        : 3
Time         : 49.273s (Solving: 39.99s 1st Model: 0.15s Unsat: 0.00s)
CPU Time     : 49.208s

Choices      : 2254694  (Domain: 2197484)
Conflicts    : 47711    (Analyzed: 47711)
Restarts     : 201      (Average: 237.37 Last: 145)
Model-Level  : 3600.0  
Problems     : 3        (Average Length: 102.00 Splits: 0)
Lemmas       : 47711    (Deleted: 38665)
  Binary     : 2882     (Ratio:   6.04%)
  Ternary    : 673      (Ratio:   1.41%)
  Conflict   : 47711    (Average Length:  335.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 47711    (Average: 46.48 Max: 1444 Sum: 2217714)
  Executed   : 47675    (Average: 46.41 Max: 1444 Sum: 2214077 Ratio:  99.84%)
  Bounded    : 36       (Average: 101.03 Max: 102 Sum:   3637 Ratio:   0.16%)

Rules        : 766922   (Original: 635077)
Atoms        : 45135   
Bodies       : 588251   (Original: 456406)
  Count      : 7639     (Original: 20328)
Equivalences : 142481   (Atom=Atom: 152 Body=Body: 0 Other: 142329)
Tight        : Yes
Variables    : 428921   (Eliminated:    0 Frozen: 144613)
Constraints  : 3146858  (Binary:  91.5% Ternary:   6.9% Other:   1.6%)

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

[endof: stats after solve call]
Solving Time:	 19.69s
Memory:		 714MB (+1MB)
UNKNOWN
Iteration Time:	 19.69s

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

Models       : 0+
Calls        : 4
Time         : 62.453s (Solving: 53.09s 1st Model: 0.15s Unsat: 0.00s)
CPU Time     : 62.392s

Choices      : 2554911  (Domain: 2495383)
Conflicts    : 69234    (Analyzed: 69234)
Restarts     : 301      (Average: 230.01 Last: 184)
Model-Level  : 3600.0  
Problems     : 4        (Average Length: 102.00 Splits: 0)
Lemmas       : 69234    (Deleted: 57026)
  Binary     : 3120     (Ratio:   4.51%)
  Ternary    : 765      (Ratio:   1.10%)
  Conflict   : 69234    (Average Length:  293.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 69234    (Average: 36.22 Max: 1444 Sum: 2507787)
  Executed   : 69184    (Average: 36.15 Max: 1444 Sum: 2502774 Ratio:  99.80%)
  Bounded    : 50       (Average: 100.26 Max: 102 Sum:   5013 Ratio:   0.20%)

Rules        : 766922   (Original: 635077)
Atoms        : 45135   
Bodies       : 588251   (Original: 456406)
  Count      : 7639     (Original: 20328)
Equivalences : 142481   (Atom=Atom: 152 Body=Body: 0 Other: 142329)
Tight        : Yes
Variables    : 428921   (Eliminated:    0 Frozen: 144613)
Constraints  : 3141047  (Binary:  91.6% Ternary:   6.9% Other:   1.6%)

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

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

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

Models       : 0+
Calls        : 5
Time         : 80.332s (Solving: 70.90s 1st Model: 0.15s Unsat: 0.00s)
CPU Time     : 80.280s

Choices      : 3534932  (Domain: 3459513)
Conflicts    : 95735    (Analyzed: 95735)
Restarts     : 401      (Average: 238.74 Last: 184)
Model-Level  : 3600.0  
Problems     : 5        (Average Length: 102.00 Splits: 0)
Lemmas       : 95735    (Deleted: 81780)
  Binary     : 3896     (Ratio:   4.07%)
  Ternary    : 902      (Ratio:   0.94%)
  Conflict   : 95735    (Average Length:  286.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 95735    (Average: 36.29 Max: 1444 Sum: 3473858)
  Executed   : 95682    (Average: 36.23 Max: 1444 Sum: 3468545 Ratio:  99.85%)
  Bounded    : 53       (Average: 100.25 Max: 102 Sum:   5313 Ratio:   0.15%)

Rules        : 766922   (Original: 635077)
Atoms        : 45135   
Bodies       : 588251   (Original: 456406)
  Count      : 7639     (Original: 20328)
Equivalences : 142481   (Atom=Atom: 152 Body=Body: 0 Other: 142329)
Tight        : Yes
Variables    : 428921   (Eliminated:    0 Frozen: 144613)
Constraints  : 3141047  (Binary:  91.6% Ternary:   6.9% Other:   1.6%)

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

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

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

Models       : 0+
Calls        : 6
Time         : 97.347s (Solving: 87.83s 1st Model: 0.15s Unsat: 0.00s)
CPU Time     : 97.300s

Choices      : 4486841  (Domain: 4398171)
Conflicts    : 121562   (Analyzed: 121562)
Restarts     : 501      (Average: 242.64 Last: 184)
Model-Level  : 3600.0  
Problems     : 6        (Average Length: 102.00 Splits: 0)
Lemmas       : 121562   (Deleted: 106320)
  Binary     : 4688     (Ratio:   3.86%)
  Ternary    : 1001     (Ratio:   0.82%)
  Conflict   : 121562   (Average Length:  372.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 121562   (Average: 36.20 Max: 1444 Sum: 4400670)
  Executed   : 121506   (Average: 36.15 Max: 1444 Sum: 4395061 Ratio:  99.87%)
  Bounded    : 56       (Average: 100.16 Max: 102 Sum:   5609 Ratio:   0.13%)

Rules        : 766922   (Original: 635077)
Atoms        : 45135   
Bodies       : 588251   (Original: 456406)
  Count      : 7639     (Original: 20328)
Equivalences : 142481   (Atom=Atom: 152 Body=Body: 0 Other: 142329)
Tight        : Yes
Variables    : 428921   (Eliminated:    0 Frozen: 144613)
Constraints  : 3141033  (Binary:  91.6% Ternary:   6.9% Other:   1.6%)

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

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

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

Models       : 0+
Calls        : 7
Time         : 112.695s (Solving: 103.10s 1st Model: 0.15s Unsat: 0.00s)
CPU Time     : 112.652s

Choices      : 5217881  (Domain: 5121161)
Conflicts    : 146967   (Analyzed: 146967)
Restarts     : 601      (Average: 244.54 Last: 211)
Model-Level  : 3600.0  
Problems     : 7        (Average Length: 102.00 Splits: 0)
Lemmas       : 146967   (Deleted: 131105)
  Binary     : 5170     (Ratio:   3.52%)
  Ternary    : 1043     (Ratio:   0.71%)
  Conflict   : 146967   (Average Length:  406.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 146967   (Average: 34.77 Max: 1444 Sum: 5110700)
  Executed   : 146909   (Average: 34.73 Max: 1444 Sum: 5104888 Ratio:  99.89%)
  Bounded    : 58       (Average: 100.21 Max: 102 Sum:   5812 Ratio:   0.11%)

Rules        : 766922   (Original: 635077)
Atoms        : 45135   
Bodies       : 588251   (Original: 456406)
  Count      : 7639     (Original: 20328)
Equivalences : 142481   (Atom=Atom: 152 Body=Body: 0 Other: 142329)
Tight        : Yes
Variables    : 428921   (Eliminated:    0 Frozen: 144613)
Constraints  : 3141019  (Binary:  91.6% Ternary:   6.9% Other:   1.6%)

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

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

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

Models       : 0+
Calls        : 8
Time         : 131.318s (Solving: 121.62s 1st Model: 0.15s Unsat: 0.00s)
CPU Time     : 131.284s

Choices      : 6181664  (Domain: 6076184)
Conflicts    : 176389   (Analyzed: 176389)
Restarts     : 701      (Average: 251.62 Last: 211)
Model-Level  : 3600.0  
Problems     : 8        (Average Length: 102.00 Splits: 0)
Lemmas       : 176389   (Deleted: 159940)
  Binary     : 5702     (Ratio:   3.23%)
  Ternary    : 1085     (Ratio:   0.62%)
  Conflict   : 176389   (Average Length:  459.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 176389   (Average: 34.31 Max: 1444 Sum: 6052589)
  Executed   : 176331   (Average: 34.28 Max: 1444 Sum: 6046777 Ratio:  99.90%)
  Bounded    : 58       (Average: 100.21 Max: 102 Sum:   5812 Ratio:   0.10%)

Rules        : 766922   (Original: 635077)
Atoms        : 45135   
Bodies       : 588251   (Original: 456406)
  Count      : 7639     (Original: 20328)
Equivalences : 142481   (Atom=Atom: 152 Body=Body: 0 Other: 142329)
Tight        : Yes
Variables    : 428921   (Eliminated:    0 Frozen: 144613)
Constraints  : 3141006  (Binary:  91.6% Ternary:   6.9% Other:   1.6%)

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

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

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

Models       : 0+
Calls        : 9
Time         : 146.209s (Solving: 136.43s 1st Model: 0.15s Unsat: 0.00s)
CPU Time     : 146.180s

Choices      : 6965489  (Domain: 6850983)
Conflicts    : 200090   (Analyzed: 200090)
Restarts     : 801      (Average: 249.80 Last: 211)
Model-Level  : 3600.0  
Problems     : 9        (Average Length: 102.00 Splits: 0)
Lemmas       : 200090   (Deleted: 180150)
  Binary     : 6739     (Ratio:   3.37%)
  Ternary    : 1253     (Ratio:   0.63%)
  Conflict   : 200090   (Average Length:  482.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 200090   (Average: 34.01 Max: 1444 Sum: 6805127)
  Executed   : 200032   (Average: 33.98 Max: 1444 Sum: 6799315 Ratio:  99.91%)
  Bounded    : 58       (Average: 100.21 Max: 102 Sum:   5812 Ratio:   0.09%)

Rules        : 766922   (Original: 635077)
Atoms        : 45135   
Bodies       : 588251   (Original: 456406)
  Count      : 7639     (Original: 20328)
Equivalences : 142481   (Atom=Atom: 152 Body=Body: 0 Other: 142329)
Tight        : Yes
Variables    : 428921   (Eliminated:    0 Frozen: 144613)
Constraints  : 3141006  (Binary:  91.6% Ternary:   6.9% Other:   1.6%)

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

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

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

Models       : 0+
Calls        : 10
Time         : 167.261s (Solving: 157.41s 1st Model: 0.15s Unsat: 0.00s)
CPU Time     : 167.240s

Choices      : 8340451  (Domain: 8203231)
Conflicts    : 230101   (Analyzed: 230101)
Restarts     : 901      (Average: 255.38 Last: 211)
Model-Level  : 3600.0  
Problems     : 10       (Average Length: 102.00 Splits: 0)
Lemmas       : 230101   (Deleted: 207195)
  Binary     : 7947     (Ratio:   3.45%)
  Ternary    : 1491     (Ratio:   0.65%)
  Conflict   : 230101   (Average Length:  517.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 230101   (Average: 35.39 Max: 1444 Sum: 8143039)
  Executed   : 230043   (Average: 35.36 Max: 1444 Sum: 8137227 Ratio:  99.93%)
  Bounded    : 58       (Average: 100.21 Max: 102 Sum:   5812 Ratio:   0.07%)

Rules        : 766922   (Original: 635077)
Atoms        : 45135   
Bodies       : 588251   (Original: 456406)
  Count      : 7639     (Original: 20328)
Equivalences : 142481   (Atom=Atom: 152 Body=Body: 0 Other: 142329)
Tight        : Yes
Variables    : 428921   (Eliminated:    0 Frozen: 144613)
Constraints  : 3141006  (Binary:  91.6% Ternary:   6.9% Other:   1.6%)

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

[endof: stats after solve call]
Solving Time:	 21.06s
Memory:		 714MB (+0MB)
UNKNOWN
Iteration Time:	 21.07s

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

Models       : 0+
Calls        : 11
Time         : 186.450s (Solving: 176.51s 1st Model: 0.15s Unsat: 0.00s)
CPU Time     : 186.436s

Choices      : 8922276  (Domain: 8782702)
Conflicts    : 256216   (Analyzed: 256216)
Restarts     : 1001     (Average: 255.96 Last: 211)
Model-Level  : 3600.0  
Problems     : 11       (Average Length: 102.00 Splits: 0)
Lemmas       : 256216   (Deleted: 233914)
  Binary     : 8501     (Ratio:   3.32%)
  Ternary    : 1580     (Ratio:   0.62%)
  Conflict   : 256216   (Average Length:  584.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 256216   (Average: 33.94 Max: 1444 Sum: 8694781)
  Executed   : 256158   (Average: 33.91 Max: 1444 Sum: 8688969 Ratio:  99.93%)
  Bounded    : 58       (Average: 100.21 Max: 102 Sum:   5812 Ratio:   0.07%)

Rules        : 766922   (Original: 635077)
Atoms        : 45135   
Bodies       : 588251   (Original: 456406)
  Count      : 7639     (Original: 20328)
Equivalences : 142481   (Atom=Atom: 152 Body=Body: 0 Other: 142329)
Tight        : Yes
Variables    : 428921   (Eliminated:    0 Frozen: 144613)
Constraints  : 3141006  (Binary:  91.6% Ternary:   6.9% Other:   1.6%)

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

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

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

Models       : 0+
Calls        : 12
Time         : 208.468s (Solving: 198.43s 1st Model: 0.15s Unsat: 0.00s)
CPU Time     : 208.464s

Choices      : 9753489  (Domain: 9611894)
Conflicts    : 286065   (Analyzed: 286065)
Restarts     : 1101     (Average: 259.82 Last: 211)
Model-Level  : 3600.0  
Problems     : 12       (Average Length: 102.00 Splits: 0)
Lemmas       : 286065   (Deleted: 260189)
  Binary     : 9147     (Ratio:   3.20%)
  Ternary    : 1727     (Ratio:   0.60%)
  Conflict   : 286065   (Average Length:  598.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 286065   (Average: 33.20 Max: 1444 Sum: 9498036)
  Executed   : 286007   (Average: 33.18 Max: 1444 Sum: 9492224 Ratio:  99.94%)
  Bounded    : 58       (Average: 100.21 Max: 102 Sum:   5812 Ratio:   0.06%)

Rules        : 766922   (Original: 635077)
Atoms        : 45135   
Bodies       : 588251   (Original: 456406)
  Count      : 7639     (Original: 20328)
Equivalences : 142481   (Atom=Atom: 152 Body=Body: 0 Other: 142329)
Tight        : Yes
Variables    : 428921   (Eliminated:    0 Frozen: 144613)
Constraints  : 3141006  (Binary:  91.6% Ternary:   6.9% Other:   1.6%)

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

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

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

Models       : 0+
Calls        : 13
Time         : 229.441s (Solving: 219.33s 1st Model: 0.15s Unsat: 0.00s)
CPU Time     : 229.448s

Choices      : 10540089 (Domain: 10391157)
Conflicts    : 314671   (Analyzed: 314671)
Restarts     : 1201     (Average: 262.01 Last: 211)
Model-Level  : 3600.0  
Problems     : 13       (Average Length: 102.00 Splits: 0)
Lemmas       : 314671   (Deleted: 288420)
  Binary     : 10015    (Ratio:   3.18%)
  Ternary    : 1849     (Ratio:   0.59%)
  Conflict   : 314671   (Average Length:  636.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 314671   (Average: 32.58 Max: 1444 Sum: 10250555)
  Executed   : 314613   (Average: 32.56 Max: 1444 Sum: 10244743 Ratio:  99.94%)
  Bounded    : 58       (Average: 100.21 Max: 102 Sum:   5812 Ratio:   0.06%)

Rules        : 766922   (Original: 635077)
Atoms        : 45135   
Bodies       : 588251   (Original: 456406)
  Count      : 7639     (Original: 20328)
Equivalences : 142481   (Atom=Atom: 152 Body=Body: 0 Other: 142329)
Tight        : Yes
Variables    : 428921   (Eliminated:    0 Frozen: 144613)
Constraints  : 3141006  (Binary:  91.6% Ternary:   6.9% Other:   1.6%)

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

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

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

Models       : 0+
Calls        : 14
Time         : 246.777s (Solving: 236.59s 1st Model: 0.15s Unsat: 0.00s)
CPU Time     : 246.792s

Choices      : 11207122 (Domain: 11055150)
Conflicts    : 340211   (Analyzed: 340211)
Restarts     : 1301     (Average: 261.50 Last: 211)
Model-Level  : 3600.0  
Problems     : 14       (Average Length: 102.00 Splits: 0)
Lemmas       : 340211   (Deleted: 312522)
  Binary     : 10748    (Ratio:   3.16%)
  Ternary    : 1950     (Ratio:   0.57%)
  Conflict   : 340211   (Average Length:  648.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 340211   (Average: 31.97 Max: 1444 Sum: 10875158)
  Executed   : 340153   (Average: 31.95 Max: 1444 Sum: 10869346 Ratio:  99.95%)
  Bounded    : 58       (Average: 100.21 Max: 102 Sum:   5812 Ratio:   0.05%)

Rules        : 766922   (Original: 635077)
Atoms        : 45135   
Bodies       : 588251   (Original: 456406)
  Count      : 7639     (Original: 20328)
Equivalences : 142481   (Atom=Atom: 152 Body=Body: 0 Other: 142329)
Tight        : Yes
Variables    : 428921   (Eliminated:    0 Frozen: 144613)
Constraints  : 3141006  (Binary:  91.6% Ternary:   6.9% Other:   1.6%)

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

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

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

Models       : 0+
Calls        : 15
Time         : 266.463s (Solving: 256.16s 1st Model: 0.15s Unsat: 0.00s)
CPU Time     : 266.488s

Choices      : 11792813 (Domain: 11639210)
Conflicts    : 371602   (Analyzed: 371602)
Restarts     : 1401     (Average: 265.24 Last: 238)
Model-Level  : 3600.0  
Problems     : 15       (Average Length: 102.00 Splits: 0)
Lemmas       : 371602   (Deleted: 342715)
  Binary     : 11390    (Ratio:   3.07%)
  Ternary    : 2010     (Ratio:   0.54%)
  Conflict   : 371602   (Average Length:  658.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 371602   (Average: 30.76 Max: 1444 Sum: 11428791)
  Executed   : 371543   (Average: 30.74 Max: 1444 Sum: 11422877 Ratio:  99.95%)
  Bounded    : 59       (Average: 100.24 Max: 102 Sum:   5914 Ratio:   0.05%)

Rules        : 766922   (Original: 635077)
Atoms        : 45135   
Bodies       : 588251   (Original: 456406)
  Count      : 7639     (Original: 20328)
Equivalences : 142481   (Atom=Atom: 152 Body=Body: 0 Other: 142329)
Tight        : Yes
Variables    : 428921   (Eliminated:    0 Frozen: 144613)
Constraints  : 3141006  (Binary:  91.6% Ternary:   6.9% Other:   1.6%)

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

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

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

Models       : 0+
Calls        : 16
Time         : 283.336s (Solving: 272.95s 1st Model: 0.15s Unsat: 0.00s)
CPU Time     : 283.368s

Choices      : 12163506 (Domain: 12005658)
Conflicts    : 395693   (Analyzed: 395693)
Restarts     : 1501     (Average: 263.62 Last: 498)
Model-Level  : 3600.0  
Problems     : 16       (Average Length: 102.00 Splits: 0)
Lemmas       : 395693   (Deleted: 364567)
  Binary     : 11843    (Ratio:   2.99%)
  Ternary    : 2079     (Ratio:   0.53%)
  Conflict   : 395693   (Average Length:  698.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 395693   (Average: 29.72 Max: 1444 Sum: 11760766)
  Executed   : 395634   (Average: 29.71 Max: 1444 Sum: 11754852 Ratio:  99.95%)
  Bounded    : 59       (Average: 100.24 Max: 102 Sum:   5914 Ratio:   0.05%)

Rules        : 766922   (Original: 635077)
Atoms        : 45135   
Bodies       : 588251   (Original: 456406)
  Count      : 7639     (Original: 20328)
Equivalences : 142481   (Atom=Atom: 152 Body=Body: 0 Other: 142329)
Tight        : Yes
Variables    : 428921   (Eliminated:    0 Frozen: 144613)
Constraints  : 3140992  (Binary:  91.6% Ternary:   6.9% Other:   1.6%)

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

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

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

Models       : 0+
Calls        : 17
Time         : 301.413s (Solving: 290.93s 1st Model: 0.15s Unsat: 0.00s)
CPU Time     : 301.452s

Choices      : 12579338 (Domain: 12420758)
Conflicts    : 423949   (Analyzed: 423949)
Restarts     : 1601     (Average: 264.80 Last: 498)
Model-Level  : 3600.0  
Problems     : 17       (Average Length: 102.00 Splits: 0)
Lemmas       : 423949   (Deleted: 393444)
  Binary     : 12239    (Ratio:   2.89%)
  Ternary    : 2122     (Ratio:   0.50%)
  Conflict   : 423949   (Average Length:  700.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 423949   (Average: 28.65 Max: 1444 Sum: 12144496)
  Executed   : 423890   (Average: 28.63 Max: 1444 Sum: 12138582 Ratio:  99.95%)
  Bounded    : 59       (Average: 100.24 Max: 102 Sum:   5914 Ratio:   0.05%)

Rules        : 766922   (Original: 635077)
Atoms        : 45135   
Bodies       : 588251   (Original: 456406)
  Count      : 7639     (Original: 20328)
Equivalences : 142481   (Atom=Atom: 152 Body=Body: 0 Other: 142329)
Tight        : Yes
Variables    : 428921   (Eliminated:    0 Frozen: 144613)
Constraints  : 3140992  (Binary:  91.6% Ternary:   6.9% Other:   1.6%)

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

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

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

Models       : 0+
Calls        : 18
Time         : 320.019s (Solving: 309.45s 1st Model: 0.15s Unsat: 0.00s)
CPU Time     : 320.064s

Choices      : 13185444 (Domain: 13023926)
Conflicts    : 452726   (Analyzed: 452726)
Restarts     : 1701     (Average: 266.15 Last: 498)
Model-Level  : 3600.0  
Problems     : 18       (Average Length: 102.00 Splits: 0)
Lemmas       : 452726   (Deleted: 420170)
  Binary     : 12961    (Ratio:   2.86%)
  Ternary    : 2224     (Ratio:   0.49%)
  Conflict   : 452726   (Average Length:  707.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 452726   (Average: 28.08 Max: 1444 Sum: 12712028)
  Executed   : 452667   (Average: 28.07 Max: 1444 Sum: 12706114 Ratio:  99.95%)
  Bounded    : 59       (Average: 100.24 Max: 102 Sum:   5914 Ratio:   0.05%)

Rules        : 766922   (Original: 635077)
Atoms        : 45135   
Bodies       : 588251   (Original: 456406)
  Count      : 7639     (Original: 20328)
Equivalences : 142481   (Atom=Atom: 152 Body=Body: 0 Other: 142329)
Tight        : Yes
Variables    : 428921   (Eliminated:    0 Frozen: 144613)
Constraints  : 3140992  (Binary:  91.6% Ternary:   6.9% Other:   1.6%)

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

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

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

Models       : 0+
Calls        : 19
Time         : 335.875s (Solving: 325.23s 1st Model: 0.15s Unsat: 0.00s)
CPU Time     : 335.928s

Choices      : 13625361 (Domain: 13462628)
Conflicts    : 477895   (Analyzed: 477895)
Restarts     : 1801     (Average: 265.35 Last: 498)
Model-Level  : 3600.0  
Problems     : 19       (Average Length: 102.00 Splits: 0)
Lemmas       : 477895   (Deleted: 445198)
  Binary     : 13306    (Ratio:   2.78%)
  Ternary    : 2292     (Ratio:   0.48%)
  Conflict   : 477895   (Average Length:  718.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 477895   (Average: 27.44 Max: 1444 Sum: 13112912)
  Executed   : 477836   (Average: 27.43 Max: 1444 Sum: 13106998 Ratio:  99.95%)
  Bounded    : 59       (Average: 100.24 Max: 102 Sum:   5914 Ratio:   0.05%)

Rules        : 766922   (Original: 635077)
Atoms        : 45135   
Bodies       : 588251   (Original: 456406)
  Count      : 7639     (Original: 20328)
Equivalences : 142481   (Atom=Atom: 152 Body=Body: 0 Other: 142329)
Tight        : Yes
Variables    : 428921   (Eliminated:    0 Frozen: 144613)
Constraints  : 3140992  (Binary:  91.6% Ternary:   6.9% Other:   1.6%)

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

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

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

Models       : 0+
Calls        : 20
Time         : 351.416s (Solving: 340.69s 1st Model: 0.15s Unsat: 0.00s)
CPU Time     : 351.476s

Choices      : 14034374 (Domain: 13871096)
Conflicts    : 502808   (Analyzed: 502808)
Restarts     : 1901     (Average: 264.50 Last: 498)
Model-Level  : 3600.0  
Problems     : 20       (Average Length: 102.00 Splits: 0)
Lemmas       : 502808   (Deleted: 469519)
  Binary     : 13670    (Ratio:   2.72%)
  Ternary    : 2349     (Ratio:   0.47%)
  Conflict   : 502808   (Average Length:  717.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 502808   (Average: 26.82 Max: 1444 Sum: 13484583)
  Executed   : 502749   (Average: 26.81 Max: 1444 Sum: 13478669 Ratio:  99.96%)
  Bounded    : 59       (Average: 100.24 Max: 102 Sum:   5914 Ratio:   0.04%)

Rules        : 766922   (Original: 635077)
Atoms        : 45135   
Bodies       : 588251   (Original: 456406)
  Count      : 7639     (Original: 20328)
Equivalences : 142481   (Atom=Atom: 152 Body=Body: 0 Other: 142329)
Tight        : Yes
Variables    : 428921   (Eliminated:    0 Frozen: 144613)
Constraints  : 3140992  (Binary:  91.6% Ternary:   6.9% Other:   1.6%)

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

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

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

Models       : 0+
Calls        : 21
Time         : 368.396s (Solving: 357.56s 1st Model: 0.15s Unsat: 0.00s)
CPU Time     : 368.464s

Choices      : 14412349 (Domain: 14248814)
Conflicts    : 529237   (Analyzed: 529237)
Restarts     : 2001     (Average: 264.49 Last: 498)
Model-Level  : 3600.0  
Problems     : 21       (Average Length: 102.00 Splits: 0)
Lemmas       : 529237   (Deleted: 493651)
  Binary     : 14000    (Ratio:   2.65%)
  Ternary    : 2414     (Ratio:   0.46%)
  Conflict   : 529237   (Average Length:  715.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 529237   (Average: 26.12 Max: 1444 Sum: 13826035)
  Executed   : 529178   (Average: 26.11 Max: 1444 Sum: 13820121 Ratio:  99.96%)
  Bounded    : 59       (Average: 100.24 Max: 102 Sum:   5914 Ratio:   0.04%)

Rules        : 766922   (Original: 635077)
Atoms        : 45135   
Bodies       : 588251   (Original: 456406)
  Count      : 7639     (Original: 20328)
Equivalences : 142481   (Atom=Atom: 152 Body=Body: 0 Other: 142329)
Tight        : Yes
Variables    : 428921   (Eliminated:    0 Frozen: 144613)
Constraints  : 3140992  (Binary:  91.6% Ternary:   6.9% Other:   1.6%)

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

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

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

Models       : 0+
Calls        : 22
Time         : 384.597s (Solving: 373.69s 1st Model: 0.15s Unsat: 0.00s)
CPU Time     : 384.672s

Choices      : 14795745 (Domain: 14631942)
Conflicts    : 555208   (Analyzed: 555208)
Restarts     : 2101     (Average: 264.26 Last: 498)
Model-Level  : 3600.0  
Problems     : 22       (Average Length: 102.00 Splits: 0)
Lemmas       : 555208   (Deleted: 519162)
  Binary     : 14360    (Ratio:   2.59%)
  Ternary    : 2469     (Ratio:   0.44%)
  Conflict   : 555208   (Average Length:  719.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 555208   (Average: 25.52 Max: 1444 Sum: 14171326)
  Executed   : 555149   (Average: 25.51 Max: 1444 Sum: 14165412 Ratio:  99.96%)
  Bounded    : 59       (Average: 100.24 Max: 102 Sum:   5914 Ratio:   0.04%)

Rules        : 766922   (Original: 635077)
Atoms        : 45135   
Bodies       : 588251   (Original: 456406)
  Count      : 7639     (Original: 20328)
Equivalences : 142481   (Atom=Atom: 152 Body=Body: 0 Other: 142329)
Tight        : Yes
Variables    : 428921   (Eliminated:    0 Frozen: 144613)
Constraints  : 3140992  (Binary:  91.6% Ternary:   6.9% Other:   1.6%)

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

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

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

Models       : 0+
Calls        : 23
Time         : 401.605s (Solving: 390.59s 1st Model: 0.15s Unsat: 0.00s)
CPU Time     : 401.684s

Choices      : 15183421 (Domain: 15019076)
Conflicts    : 582670   (Analyzed: 582670)
Restarts     : 2201     (Average: 264.73 Last: 498)
Model-Level  : 3600.0  
Problems     : 23       (Average Length: 102.00 Splits: 0)
Lemmas       : 582670   (Deleted: 544408)
  Binary     : 14714    (Ratio:   2.53%)
  Ternary    : 2529     (Ratio:   0.43%)
  Conflict   : 582670   (Average Length:  720.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 582670   (Average: 24.93 Max: 1444 Sum: 14526072)
  Executed   : 582611   (Average: 24.92 Max: 1444 Sum: 14520158 Ratio:  99.96%)
  Bounded    : 59       (Average: 100.24 Max: 102 Sum:   5914 Ratio:   0.04%)

Rules        : 766922   (Original: 635077)
Atoms        : 45135   
Bodies       : 588251   (Original: 456406)
  Count      : 7639     (Original: 20328)
Equivalences : 142481   (Atom=Atom: 152 Body=Body: 0 Other: 142329)
Tight        : Yes
Variables    : 428921   (Eliminated:    0 Frozen: 144613)
Constraints  : 3140992  (Binary:  91.6% Ternary:   6.9% Other:   1.6%)

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

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

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

Models       : 0+
Calls        : 24
Time         : 420.188s (Solving: 409.10s 1st Model: 0.15s Unsat: 0.00s)
CPU Time     : 420.276s

Choices      : 15540170 (Domain: 15375749)
Conflicts    : 612215   (Analyzed: 612215)
Restarts     : 2301     (Average: 266.06 Last: 498)
Model-Level  : 3600.0  
Problems     : 24       (Average Length: 102.00 Splits: 0)
Lemmas       : 612215   (Deleted: 573866)
  Binary     : 15020    (Ratio:   2.45%)
  Ternary    : 2576     (Ratio:   0.42%)
  Conflict   : 612215   (Average Length:  729.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 612215   (Average: 24.25 Max: 1444 Sum: 14846406)
  Executed   : 612156   (Average: 24.24 Max: 1444 Sum: 14840492 Ratio:  99.96%)
  Bounded    : 59       (Average: 100.24 Max: 102 Sum:   5914 Ratio:   0.04%)

Rules        : 766922   (Original: 635077)
Atoms        : 45135   
Bodies       : 588251   (Original: 456406)
  Count      : 7639     (Original: 20328)
Equivalences : 142481   (Atom=Atom: 152 Body=Body: 0 Other: 142329)
Tight        : Yes
Variables    : 428921   (Eliminated:    0 Frozen: 144613)
Constraints  : 3140992  (Binary:  91.6% Ternary:   6.9% Other:   1.6%)

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

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

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

Models       : 0+
Calls        : 25
Time         : 436.093s (Solving: 424.90s 1st Model: 0.15s Unsat: 0.00s)
CPU Time     : 436.188s

Choices      : 15879545 (Domain: 15713316)
Conflicts    : 636685   (Analyzed: 636685)
Restarts     : 2401     (Average: 265.17 Last: 498)
Model-Level  : 3600.0  
Problems     : 25       (Average Length: 102.00 Splits: 0)
Lemmas       : 636685   (Deleted: 597126)
  Binary     : 15297    (Ratio:   2.40%)
  Ternary    : 2652     (Ratio:   0.42%)
  Conflict   : 636685   (Average Length:  737.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 636685   (Average: 23.79 Max: 1444 Sum: 15146422)
  Executed   : 636625   (Average: 23.78 Max: 1444 Sum: 15140406 Ratio:  99.96%)
  Bounded    : 60       (Average: 100.27 Max: 102 Sum:   6016 Ratio:   0.04%)

Rules        : 766922   (Original: 635077)
Atoms        : 45135   
Bodies       : 588251   (Original: 456406)
  Count      : 7639     (Original: 20328)
Equivalences : 142481   (Atom=Atom: 152 Body=Body: 0 Other: 142329)
Tight        : Yes
Variables    : 428921   (Eliminated:    0 Frozen: 144613)
Constraints  : 3140992  (Binary:  91.6% Ternary:   6.9% Other:   1.6%)

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

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

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

Models       : 0+
Calls        : 26
Time         : 450.482s (Solving: 439.20s 1st Model: 0.15s Unsat: 0.00s)
CPU Time     : 450.584s

Choices      : 16244228 (Domain: 16077299)
Conflicts    : 662982   (Analyzed: 662982)
Restarts     : 2501     (Average: 265.09 Last: 498)
Model-Level  : 3600.0  
Problems     : 26       (Average Length: 102.00 Splits: 0)
Lemmas       : 662982   (Deleted: 623716)
  Binary     : 15605    (Ratio:   2.35%)
  Ternary    : 2704     (Ratio:   0.41%)
  Conflict   : 662982   (Average Length:  737.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 662982   (Average: 23.34 Max: 1444 Sum: 15471738)
  Executed   : 662922   (Average: 23.33 Max: 1444 Sum: 15465722 Ratio:  99.96%)
  Bounded    : 60       (Average: 100.27 Max: 102 Sum:   6016 Ratio:   0.04%)

Rules        : 766922   (Original: 635077)
Atoms        : 45135   
Bodies       : 588251   (Original: 456406)
  Count      : 7639     (Original: 20328)
Equivalences : 142481   (Atom=Atom: 152 Body=Body: 0 Other: 142329)
Tight        : Yes
Variables    : 428921   (Eliminated:    0 Frozen: 144613)
Constraints  : 3140978  (Binary:  91.6% Ternary:   6.9% Other:   1.6%)

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

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

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

Models       : 0+
Calls        : 27
Time         : 467.374s (Solving: 456.02s 1st Model: 0.15s Unsat: 0.00s)
CPU Time     : 467.484s

Choices      : 16563121 (Domain: 16396013)
Conflicts    : 691496   (Analyzed: 691496)
Restarts     : 2601     (Average: 265.86 Last: 498)
Model-Level  : 3600.0  
Problems     : 27       (Average Length: 102.00 Splits: 0)
Lemmas       : 691496   (Deleted: 652015)
  Binary     : 15865    (Ratio:   2.29%)
  Ternary    : 2760     (Ratio:   0.40%)
  Conflict   : 691496   (Average Length:  741.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 691496   (Average: 22.78 Max: 1444 Sum: 15751966)
  Executed   : 691436   (Average: 22.77 Max: 1444 Sum: 15745950 Ratio:  99.96%)
  Bounded    : 60       (Average: 100.27 Max: 102 Sum:   6016 Ratio:   0.04%)

Rules        : 766922   (Original: 635077)
Atoms        : 45135   
Bodies       : 588251   (Original: 456406)
  Count      : 7639     (Original: 20328)
Equivalences : 142481   (Atom=Atom: 152 Body=Body: 0 Other: 142329)
Tight        : Yes
Variables    : 428921   (Eliminated:    0 Frozen: 144613)
Constraints  : 3140978  (Binary:  91.6% Ternary:   6.9% Other:   1.6%)

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

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

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

Models       : 0+
Calls        : 28
Time         : 483.807s (Solving: 472.37s 1st Model: 0.15s Unsat: 0.00s)
CPU Time     : 483.924s

Choices      : 16885633 (Domain: 16718519)
Conflicts    : 719637   (Analyzed: 719637)
Restarts     : 2701     (Average: 266.43 Last: 498)
Model-Level  : 3600.0  
Problems     : 28       (Average Length: 102.00 Splits: 0)
Lemmas       : 719637   (Deleted: 680132)
  Binary     : 16064    (Ratio:   2.23%)
  Ternary    : 2782     (Ratio:   0.39%)
  Conflict   : 719637   (Average Length:  731.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 719637   (Average: 22.30 Max: 1444 Sum: 16045823)
  Executed   : 719577   (Average: 22.29 Max: 1444 Sum: 16039807 Ratio:  99.96%)
  Bounded    : 60       (Average: 100.27 Max: 102 Sum:   6016 Ratio:   0.04%)

Rules        : 766922   (Original: 635077)
Atoms        : 45135   
Bodies       : 588251   (Original: 456406)
  Count      : 7639     (Original: 20328)
Equivalences : 142481   (Atom=Atom: 152 Body=Body: 0 Other: 142329)
Tight        : Yes
Variables    : 428921   (Eliminated:    0 Frozen: 144613)
Constraints  : 3140978  (Binary:  91.6% Ternary:   6.9% Other:   1.6%)

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

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

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

Models       : 0+
Calls        : 29
Time         : 501.787s (Solving: 490.25s 1st Model: 0.15s Unsat: 0.00s)
CPU Time     : 501.912s

Choices      : 17277580 (Domain: 17110205)
Conflicts    : 749583   (Analyzed: 749583)
Restarts     : 2801     (Average: 267.61 Last: 498)
Model-Level  : 3600.0  
Problems     : 29       (Average Length: 102.00 Splits: 0)
Lemmas       : 749583   (Deleted: 707395)
  Binary     : 16335    (Ratio:   2.18%)
  Ternary    : 2855     (Ratio:   0.38%)
  Conflict   : 749583   (Average Length:  729.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 749583   (Average: 21.88 Max: 1444 Sum: 16403110)
  Executed   : 749523   (Average: 21.87 Max: 1444 Sum: 16397094 Ratio:  99.96%)
  Bounded    : 60       (Average: 100.27 Max: 102 Sum:   6016 Ratio:   0.04%)

Rules        : 766922   (Original: 635077)
Atoms        : 45135   
Bodies       : 588251   (Original: 456406)
  Count      : 7639     (Original: 20328)
Equivalences : 142481   (Atom=Atom: 152 Body=Body: 0 Other: 142329)
Tight        : Yes
Variables    : 428921   (Eliminated:    0 Frozen: 144613)
Constraints  : 3140978  (Binary:  91.6% Ternary:   6.9% Other:   1.6%)

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

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

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

Models       : 0+
Calls        : 30
Time         : 517.120s (Solving: 505.48s 1st Model: 0.15s Unsat: 0.00s)
CPU Time     : 517.252s

Choices      : 17621725 (Domain: 17454003)
Conflicts    : 776067   (Analyzed: 776067)
Restarts     : 2901     (Average: 267.52 Last: 498)
Model-Level  : 3600.0  
Problems     : 30       (Average Length: 102.00 Splits: 0)
Lemmas       : 776067   (Deleted: 733741)
  Binary     : 16516    (Ratio:   2.13%)
  Ternary    : 2893     (Ratio:   0.37%)
  Conflict   : 776067   (Average Length:  726.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 776067   (Average: 21.53 Max: 1444 Sum: 16707662)
  Executed   : 776007   (Average: 21.52 Max: 1444 Sum: 16701646 Ratio:  99.96%)
  Bounded    : 60       (Average: 100.27 Max: 102 Sum:   6016 Ratio:   0.04%)

Rules        : 766922   (Original: 635077)
Atoms        : 45135   
Bodies       : 588251   (Original: 456406)
  Count      : 7639     (Original: 20328)
Equivalences : 142481   (Atom=Atom: 152 Body=Body: 0 Other: 142329)
Tight        : Yes
Variables    : 428921   (Eliminated:    0 Frozen: 144613)
Constraints  : 3140978  (Binary:  91.6% Ternary:   6.9% Other:   1.6%)

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

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

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

Models       : 0+
Calls        : 31
Time         : 533.380s (Solving: 521.63s 1st Model: 0.15s Unsat: 0.00s)
CPU Time     : 533.520s

Choices      : 17863044 (Domain: 17695310)
Conflicts    : 803310   (Analyzed: 803310)
Restarts     : 3001     (Average: 267.68 Last: 498)
Model-Level  : 3600.0  
Problems     : 31       (Average Length: 102.00 Splits: 0)
Lemmas       : 803310   (Deleted: 759725)
  Binary     : 16649    (Ratio:   2.07%)
  Ternary    : 2922     (Ratio:   0.36%)
  Conflict   : 803310   (Average Length:  722.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 803310   (Average: 21.05 Max: 1444 Sum: 16913240)
  Executed   : 803250   (Average: 21.05 Max: 1444 Sum: 16907224 Ratio:  99.96%)
  Bounded    : 60       (Average: 100.27 Max: 102 Sum:   6016 Ratio:   0.04%)

Rules        : 766922   (Original: 635077)
Atoms        : 45135   
Bodies       : 588251   (Original: 456406)
  Count      : 7639     (Original: 20328)
Equivalences : 142481   (Atom=Atom: 152 Body=Body: 0 Other: 142329)
Tight        : Yes
Variables    : 428921   (Eliminated:    0 Frozen: 144613)
Constraints  : 3140978  (Binary:  91.6% Ternary:   6.9% Other:   1.6%)

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

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

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

Models       : 0+
Calls        : 32
Time         : 550.533s (Solving: 538.68s 1st Model: 0.15s Unsat: 0.00s)
CPU Time     : 550.680s

Choices      : 18226174 (Domain: 18058026)
Conflicts    : 832145   (Analyzed: 832145)
Restarts     : 3101     (Average: 268.35 Last: 498)
Model-Level  : 3600.0  
Problems     : 32       (Average Length: 102.00 Splits: 0)
Lemmas       : 832145   (Deleted: 789003)
  Binary     : 16899    (Ratio:   2.03%)
  Ternary    : 2985     (Ratio:   0.36%)
  Conflict   : 832145   (Average Length:  720.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 832145   (Average: 20.72 Max: 1444 Sum: 17241208)
  Executed   : 832085   (Average: 20.71 Max: 1444 Sum: 17235192 Ratio:  99.97%)
  Bounded    : 60       (Average: 100.27 Max: 102 Sum:   6016 Ratio:   0.03%)

Rules        : 766922   (Original: 635077)
Atoms        : 45135   
Bodies       : 588251   (Original: 456406)
  Count      : 7639     (Original: 20328)
Equivalences : 142481   (Atom=Atom: 152 Body=Body: 0 Other: 142329)
Tight        : Yes
Variables    : 428921   (Eliminated:    0 Frozen: 144613)
Constraints  : 3140978  (Binary:  91.6% Ternary:   6.9% Other:   1.6%)

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

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

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

Models       : 0+
Calls        : 33
Time         : 566.364s (Solving: 554.44s 1st Model: 0.15s Unsat: 0.00s)
CPU Time     : 566.520s

Choices      : 18555345 (Domain: 18386890)
Conflicts    : 859565   (Analyzed: 859565)
Restarts     : 3201     (Average: 268.53 Last: 498)
Model-Level  : 3600.0  
Problems     : 33       (Average Length: 102.00 Splits: 0)
Lemmas       : 859565   (Deleted: 814349)
  Binary     : 17098    (Ratio:   1.99%)
  Ternary    : 3031     (Ratio:   0.35%)
  Conflict   : 859565   (Average Length:  721.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 859565   (Average: 20.40 Max: 1444 Sum: 17531579)
  Executed   : 859505   (Average: 20.39 Max: 1444 Sum: 17525563 Ratio:  99.97%)
  Bounded    : 60       (Average: 100.27 Max: 102 Sum:   6016 Ratio:   0.03%)

Rules        : 766922   (Original: 635077)
Atoms        : 45135   
Bodies       : 588251   (Original: 456406)
  Count      : 7639     (Original: 20328)
Equivalences : 142481   (Atom=Atom: 152 Body=Body: 0 Other: 142329)
Tight        : Yes
Variables    : 428921   (Eliminated:    0 Frozen: 144613)
Constraints  : 3140978  (Binary:  91.6% Ternary:   6.9% Other:   1.6%)

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

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

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

Models       : 0+
Calls        : 34
Time         : 582.397s (Solving: 570.39s 1st Model: 0.15s Unsat: 0.00s)
CPU Time     : 582.560s

Choices      : 18867074 (Domain: 18698521)
Conflicts    : 886504   (Analyzed: 886504)
Restarts     : 3301     (Average: 268.56 Last: 498)
Model-Level  : 3600.0  
Problems     : 34       (Average Length: 102.00 Splits: 0)
Lemmas       : 886504   (Deleted: 841221)
  Binary     : 17269    (Ratio:   1.95%)
  Ternary    : 3097     (Ratio:   0.35%)
  Conflict   : 886504   (Average Length:  720.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 886504   (Average: 20.09 Max: 1444 Sum: 17809942)
  Executed   : 886444   (Average: 20.08 Max: 1444 Sum: 17803926 Ratio:  99.97%)
  Bounded    : 60       (Average: 100.27 Max: 102 Sum:   6016 Ratio:   0.03%)

Rules        : 766922   (Original: 635077)
Atoms        : 45135   
Bodies       : 588251   (Original: 456406)
  Count      : 7639     (Original: 20328)
Equivalences : 142481   (Atom=Atom: 152 Body=Body: 0 Other: 142329)
Tight        : Yes
Variables    : 428921   (Eliminated:    0 Frozen: 144613)
Constraints  : 3140978  (Binary:  91.6% Ternary:   6.9% Other:   1.6%)

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

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

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

Models       : 0+
Calls        : 35
Time         : 598.449s (Solving: 586.36s 1st Model: 0.15s Unsat: 0.00s)
CPU Time     : 598.616s

Choices      : 19121985 (Domain: 18953414)
Conflicts    : 914091   (Analyzed: 914091)
Restarts     : 3401     (Average: 268.77 Last: 498)
Model-Level  : 3600.0  
Problems     : 35       (Average Length: 102.00 Splits: 0)
Lemmas       : 914091   (Deleted: 870446)
  Binary     : 17350    (Ratio:   1.90%)
  Ternary    : 3139     (Ratio:   0.34%)
  Conflict   : 914091   (Average Length:  722.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 914091   (Average: 19.72 Max: 1444 Sum: 18022751)
  Executed   : 914031   (Average: 19.71 Max: 1444 Sum: 18016735 Ratio:  99.97%)
  Bounded    : 60       (Average: 100.27 Max: 102 Sum:   6016 Ratio:   0.03%)

Rules        : 766922   (Original: 635077)
Atoms        : 45135   
Bodies       : 588251   (Original: 456406)
  Count      : 7639     (Original: 20328)
Equivalences : 142481   (Atom=Atom: 152 Body=Body: 0 Other: 142329)
Tight        : Yes
Variables    : 428921   (Eliminated:    0 Frozen: 144613)
Constraints  : 3140978  (Binary:  91.6% Ternary:   6.9% Other:   1.6%)

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

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

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

Models       : 0+
Calls        : 36
Time         : 615.698s (Solving: 603.53s 1st Model: 0.15s Unsat: 0.00s)
CPU Time     : 615.872s

Choices      : 19462035 (Domain: 19293118)
Conflicts    : 941514   (Analyzed: 941514)
Restarts     : 3501     (Average: 268.93 Last: 498)
Model-Level  : 3600.0  
Problems     : 36       (Average Length: 102.00 Splits: 0)
Lemmas       : 941514   (Deleted: 894779)
  Binary     : 17492    (Ratio:   1.86%)
  Ternary    : 3180     (Ratio:   0.34%)
  Conflict   : 941514   (Average Length:  722.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 941514   (Average: 19.47 Max: 1444 Sum: 18327868)
  Executed   : 941454   (Average: 19.46 Max: 1444 Sum: 18321852 Ratio:  99.97%)
  Bounded    : 60       (Average: 100.27 Max: 102 Sum:   6016 Ratio:   0.03%)

Rules        : 766922   (Original: 635077)
Atoms        : 45135   
Bodies       : 588251   (Original: 456406)
  Count      : 7639     (Original: 20328)
Equivalences : 142481   (Atom=Atom: 152 Body=Body: 0 Other: 142329)
Tight        : Yes
Variables    : 428921   (Eliminated:    0 Frozen: 144613)
Constraints  : 3140978  (Binary:  91.6% Ternary:   6.9% Other:   1.6%)

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

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

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

Models       : 0+
Calls        : 37
Time         : 630.527s (Solving: 618.28s 1st Model: 0.15s Unsat: 0.00s)
CPU Time     : 630.708s

Choices      : 19774617 (Domain: 19605605)
Conflicts    : 969684   (Analyzed: 969684)
Restarts     : 3601     (Average: 269.28 Last: 498)
Model-Level  : 3600.0  
Problems     : 37       (Average Length: 102.00 Splits: 0)
Lemmas       : 969684   (Deleted: 924418)
  Binary     : 17657    (Ratio:   1.82%)
  Ternary    : 3236     (Ratio:   0.33%)
  Conflict   : 969684   (Average Length:  720.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 969684   (Average: 19.18 Max: 1444 Sum: 18600105)
  Executed   : 969624   (Average: 19.18 Max: 1444 Sum: 18594089 Ratio:  99.97%)
  Bounded    : 60       (Average: 100.27 Max: 102 Sum:   6016 Ratio:   0.03%)

Rules        : 766922   (Original: 635077)
Atoms        : 45135   
Bodies       : 588251   (Original: 456406)
  Count      : 7639     (Original: 20328)
Equivalences : 142481   (Atom=Atom: 152 Body=Body: 0 Other: 142329)
Tight        : Yes
Variables    : 428921   (Eliminated:    0 Frozen: 144613)
Constraints  : 3140978  (Binary:  91.6% Ternary:   6.9% Other:   1.6%)

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

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

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

Models       : 0+
Calls        : 38
Time         : 647.665s (Solving: 635.31s 1st Model: 0.15s Unsat: 0.00s)
CPU Time     : 647.856s

Choices      : 20040839 (Domain: 19871728)
Conflicts    : 998592   (Analyzed: 998592)
Restarts     : 3701     (Average: 269.82 Last: 498)
Model-Level  : 3600.0  
Problems     : 38       (Average Length: 102.00 Splits: 0)
Lemmas       : 998592   (Deleted: 951972)
  Binary     : 17757    (Ratio:   1.78%)
  Ternary    : 3277     (Ratio:   0.33%)
  Conflict   : 998592   (Average Length:  723.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 998592   (Average: 18.86 Max: 1444 Sum: 18834071)
  Executed   : 998532   (Average: 18.85 Max: 1444 Sum: 18828055 Ratio:  99.97%)
  Bounded    : 60       (Average: 100.27 Max: 102 Sum:   6016 Ratio:   0.03%)

Rules        : 766922   (Original: 635077)
Atoms        : 45135   
Bodies       : 588251   (Original: 456406)
  Count      : 7639     (Original: 20328)
Equivalences : 142481   (Atom=Atom: 152 Body=Body: 0 Other: 142329)
Tight        : Yes
Variables    : 428921   (Eliminated:    0 Frozen: 144613)
Constraints  : 3140978  (Binary:  91.6% Ternary:   6.9% Other:   1.6%)

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

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

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

Models       : 0+
Calls        : 39
Time         : 663.340s (Solving: 650.91s 1st Model: 0.15s Unsat: 0.00s)
CPU Time     : 663.536s

Choices      : 20271142 (Domain: 20102028)
Conflicts    : 1024470  (Analyzed: 1024470)
Restarts     : 3801     (Average: 269.53 Last: 498)
Model-Level  : 3600.0  
Problems     : 39       (Average Length: 102.00 Splits: 0)
Lemmas       : 1024470  (Deleted: 977616)
  Binary     : 17854    (Ratio:   1.74%)
  Ternary    : 3303     (Ratio:   0.32%)
  Conflict   : 1024470  (Average Length:  724.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 1024470  (Average: 18.57 Max: 1444 Sum: 19023668)
  Executed   : 1024410  (Average: 18.56 Max: 1444 Sum: 19017652 Ratio:  99.97%)
  Bounded    : 60       (Average: 100.27 Max: 102 Sum:   6016 Ratio:   0.03%)

Rules        : 766922   (Original: 635077)
Atoms        : 45135   
Bodies       : 588251   (Original: 456406)
  Count      : 7639     (Original: 20328)
Equivalences : 142481   (Atom=Atom: 152 Body=Body: 0 Other: 142329)
Tight        : Yes
Variables    : 428921   (Eliminated:    0 Frozen: 144613)
Constraints  : 3140978  (Binary:  91.6% Ternary:   6.9% Other:   1.6%)

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

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

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

Models       : 0+
Calls        : 40
Time         : 678.082s (Solving: 665.58s 1st Model: 0.15s Unsat: 0.00s)
CPU Time     : 678.284s

Choices      : 20747406 (Domain: 20567960)
Conflicts    : 1048424  (Analyzed: 1048424)
Restarts     : 3901     (Average: 268.76 Last: 498)
Model-Level  : 3600.0  
Problems     : 40       (Average Length: 102.00 Splits: 0)
Lemmas       : 1048424  (Deleted: 999412)
  Binary     : 18352    (Ratio:   1.75%)
  Ternary    : 3376     (Ratio:   0.32%)
  Conflict   : 1048424  (Average Length:  725.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 1048424  (Average: 18.56 Max: 1444 Sum: 19454338)
  Executed   : 1048363  (Average: 18.55 Max: 1444 Sum: 19448220 Ratio:  99.97%)
  Bounded    : 61       (Average: 100.30 Max: 102 Sum:   6118 Ratio:   0.03%)

Rules        : 766922   (Original: 635077)
Atoms        : 45135   
Bodies       : 588251   (Original: 456406)
  Count      : 7639     (Original: 20328)
Equivalences : 142481   (Atom=Atom: 152 Body=Body: 0 Other: 142329)
Tight        : Yes
Variables    : 428921   (Eliminated:    0 Frozen: 144613)
Constraints  : 3140978  (Binary:  91.6% Ternary:   6.9% Other:   1.6%)

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

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

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

Models       : 0+
Calls        : 41
Time         : 695.098s (Solving: 682.51s 1st Model: 0.15s Unsat: 0.00s)
CPU Time     : 695.308s

Choices      : 21033077 (Domain: 20853591)
Conflicts    : 1077826  (Analyzed: 1077826)
Restarts     : 4001     (Average: 269.39 Last: 498)
Model-Level  : 3600.0  
Problems     : 41       (Average Length: 102.00 Splits: 0)
Lemmas       : 1077826  (Deleted: 1028610)
  Binary     : 18491    (Ratio:   1.72%)
  Ternary    : 3405     (Ratio:   0.32%)
  Conflict   : 1077826  (Average Length:  725.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 1077826  (Average: 18.29 Max: 1444 Sum: 19709302)
  Executed   : 1077765  (Average: 18.28 Max: 1444 Sum: 19703184 Ratio:  99.97%)
  Bounded    : 61       (Average: 100.30 Max: 102 Sum:   6118 Ratio:   0.03%)

Rules        : 766922   (Original: 635077)
Atoms        : 45135   
Bodies       : 588251   (Original: 456406)
  Count      : 7639     (Original: 20328)
Equivalences : 142481   (Atom=Atom: 152 Body=Body: 0 Other: 142329)
Tight        : Yes
Variables    : 428921   (Eliminated:    0 Frozen: 144613)
Constraints  : 3140965  (Binary:  91.6% Ternary:   6.9% Other:   1.6%)

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

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

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

Models       : 0+
Calls        : 42
Time         : 711.417s (Solving: 698.72s 1st Model: 0.15s Unsat: 0.00s)
CPU Time     : 711.632s

Choices      : 21410876 (Domain: 21231226)
Conflicts    : 1104377  (Analyzed: 1104377)
Restarts     : 4101     (Average: 269.29 Last: 498)
Model-Level  : 3600.0  
Problems     : 42       (Average Length: 102.00 Splits: 0)
Lemmas       : 1104377  (Deleted: 1054385)
  Binary     : 18729    (Ratio:   1.70%)
  Ternary    : 3476     (Ratio:   0.31%)
  Conflict   : 1104377  (Average Length:  724.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 1104377  (Average: 18.15 Max: 1444 Sum: 20047880)
  Executed   : 1104316  (Average: 18.15 Max: 1444 Sum: 20041762 Ratio:  99.97%)
  Bounded    : 61       (Average: 100.30 Max: 102 Sum:   6118 Ratio:   0.03%)

Rules        : 766922   (Original: 635077)
Atoms        : 45135   
Bodies       : 588251   (Original: 456406)
  Count      : 7639     (Original: 20328)
Equivalences : 142481   (Atom=Atom: 152 Body=Body: 0 Other: 142329)
Tight        : Yes
Variables    : 428921   (Eliminated:    0 Frozen: 144613)
Constraints  : 3140965  (Binary:  91.6% Ternary:   6.9% Other:   1.6%)

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

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

Iteration 42
Queue:		 [(0,100,41,True)]
Grounded Until:	 100
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 43
Time         : 728.654s (Solving: 715.88s 1st Model: 0.15s Unsat: 0.00s)
CPU Time     : 728.876s

Choices      : 21714873 (Domain: 21535184)
Conflicts    : 1134370  (Analyzed: 1134370)
Restarts     : 4201     (Average: 270.02 Last: 498)
Model-Level  : 3600.0  
Problems     : 43       (Average Length: 102.00 Splits: 0)
Lemmas       : 1134370  (Deleted: 1083075)
  Binary     : 18869    (Ratio:   1.66%)
  Ternary    : 3511     (Ratio:   0.31%)
  Conflict   : 1134370  (Average Length:  721.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 1134370  (Average: 17.91 Max: 1444 Sum: 20320687)
  Executed   : 1134309  (Average: 17.91 Max: 1444 Sum: 20314569 Ratio:  99.97%)
  Bounded    : 61       (Average: 100.30 Max: 102 Sum:   6118 Ratio:   0.03%)

Rules        : 766922   (Original: 635077)
Atoms        : 45135   
Bodies       : 588251   (Original: 456406)
  Count      : 7639     (Original: 20328)
Equivalences : 142481   (Atom=Atom: 152 Body=Body: 0 Other: 142329)
Tight        : Yes
Variables    : 428921   (Eliminated:    0 Frozen: 144613)
Constraints  : 3140965  (Binary:  91.6% Ternary:   6.9% Other:   1.6%)

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

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

Iteration 43
Queue:		 [(0,100,42,True)]
Grounded Until:	 100
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 44
Time         : 746.499s (Solving: 733.65s 1st Model: 0.15s Unsat: 0.00s)
CPU Time     : 746.728s

Choices      : 22006825 (Domain: 21827123)
Conflicts    : 1165100  (Analyzed: 1165100)
Restarts     : 4301     (Average: 270.89 Last: 498)
Model-Level  : 3600.0  
Problems     : 44       (Average Length: 102.00 Splits: 0)
Lemmas       : 1165100  (Deleted: 1115378)
  Binary     : 18992    (Ratio:   1.63%)
  Ternary    : 3559     (Ratio:   0.31%)
  Conflict   : 1165100  (Average Length:  720.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 1165100  (Average: 17.66 Max: 1444 Sum: 20578305)
  Executed   : 1165039  (Average: 17.66 Max: 1444 Sum: 20572187 Ratio:  99.97%)
  Bounded    : 61       (Average: 100.30 Max: 102 Sum:   6118 Ratio:   0.03%)

Rules        : 766922   (Original: 635077)
Atoms        : 45135   
Bodies       : 588251   (Original: 456406)
  Count      : 7639     (Original: 20328)
Equivalences : 142481   (Atom=Atom: 152 Body=Body: 0 Other: 142329)
Tight        : Yes
Variables    : 428921   (Eliminated:    0 Frozen: 144613)
Constraints  : 3140965  (Binary:  91.6% Ternary:   6.9% Other:   1.6%)

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

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

Iteration 44
Queue:		 [(0,100,43,True)]
Grounded Until:	 100
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 45
Time         : 762.121s (Solving: 749.19s 1st Model: 0.15s Unsat: 0.00s)
CPU Time     : 762.356s

Choices      : 22292740 (Domain: 22112987)
Conflicts    : 1195210  (Analyzed: 1195210)
Restarts     : 4401     (Average: 271.58 Last: 498)
Model-Level  : 3600.0  
Problems     : 45       (Average Length: 102.00 Splits: 0)
Lemmas       : 1195210  (Deleted: 1142642)
  Binary     : 19107    (Ratio:   1.60%)
  Ternary    : 3593     (Ratio:   0.30%)
  Conflict   : 1195210  (Average Length:  719.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 1195210  (Average: 17.42 Max: 1444 Sum: 20823583)
  Executed   : 1195149  (Average: 17.42 Max: 1444 Sum: 20817465 Ratio:  99.97%)
  Bounded    : 61       (Average: 100.30 Max: 102 Sum:   6118 Ratio:   0.03%)

Rules        : 766922   (Original: 635077)
Atoms        : 45135   
Bodies       : 588251   (Original: 456406)
  Count      : 7639     (Original: 20328)
Equivalences : 142481   (Atom=Atom: 152 Body=Body: 0 Other: 142329)
Tight        : Yes
Variables    : 428921   (Eliminated:    0 Frozen: 144613)
Constraints  : 3140965  (Binary:  91.6% Ternary:   6.9% Other:   1.6%)

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

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

Iteration 45
Queue:		 [(0,100,44,True)]
Grounded Until:	 100
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 46
Time         : 775.983s (Solving: 762.98s 1st Model: 0.15s Unsat: 0.00s)
CPU Time     : 776.224s

Choices      : 22527978 (Domain: 22348208)
Conflicts    : 1222722  (Analyzed: 1222722)
Restarts     : 4501     (Average: 271.66 Last: 498)
Model-Level  : 3600.0  
Problems     : 46       (Average Length: 102.00 Splits: 0)
Lemmas       : 1222722  (Deleted: 1169222)
  Binary     : 19240    (Ratio:   1.57%)
  Ternary    : 3625     (Ratio:   0.30%)
  Conflict   : 1222722  (Average Length:  716.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 1222722  (Average: 17.19 Max: 1444 Sum: 21023907)
  Executed   : 1222661  (Average: 17.19 Max: 1444 Sum: 21017789 Ratio:  99.97%)
  Bounded    : 61       (Average: 100.30 Max: 102 Sum:   6118 Ratio:   0.03%)

Rules        : 766922   (Original: 635077)
Atoms        : 45135   
Bodies       : 588251   (Original: 456406)
  Count      : 7639     (Original: 20328)
Equivalences : 142481   (Atom=Atom: 152 Body=Body: 0 Other: 142329)
Tight        : Yes
Variables    : 428921   (Eliminated:    0 Frozen: 144613)
Constraints  : 3140965  (Binary:  91.6% Ternary:   6.9% Other:   1.6%)

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

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

Iteration 46
Queue:		 [(0,100,45,True)]
Grounded Until:	 100
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 47
Time         : 792.091s (Solving: 778.99s 1st Model: 0.15s Unsat: 0.00s)
CPU Time     : 792.340s

Choices      : 22824289 (Domain: 22644384)
Conflicts    : 1250246  (Analyzed: 1250246)
Restarts     : 4601     (Average: 271.73 Last: 498)
Model-Level  : 3600.0  
Problems     : 47       (Average Length: 102.00 Splits: 0)
Lemmas       : 1250246  (Deleted: 1199153)
  Binary     : 19388    (Ratio:   1.55%)
  Ternary    : 3665     (Ratio:   0.29%)
  Conflict   : 1250246  (Average Length:  714.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 1250246  (Average: 17.02 Max: 1444 Sum: 21282328)
  Executed   : 1250184  (Average: 17.02 Max: 1444 Sum: 21276108 Ratio:  99.97%)
  Bounded    : 62       (Average: 100.32 Max: 102 Sum:   6220 Ratio:   0.03%)

Rules        : 766922   (Original: 635077)
Atoms        : 45135   
Bodies       : 588251   (Original: 456406)
  Count      : 7639     (Original: 20328)
Equivalences : 142481   (Atom=Atom: 152 Body=Body: 0 Other: 142329)
Tight        : Yes
Variables    : 428921   (Eliminated:    0 Frozen: 144613)
Constraints  : 3140965  (Binary:  91.6% Ternary:   6.9% Other:   1.6%)

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

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

Iteration 47
Queue:		 [(0,100,46,True)]
Grounded Until:	 100
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 48
Time         : 808.371s (Solving: 795.17s 1st Model: 0.15s Unsat: 0.00s)
CPU Time     : 808.624s

Choices      : 23194309 (Domain: 23013711)
Conflicts    : 1278361  (Analyzed: 1278361)
Restarts     : 4701     (Average: 271.93 Last: 498)
Model-Level  : 3600.0  
Problems     : 48       (Average Length: 102.00 Splits: 0)
Lemmas       : 1278361  (Deleted: 1225846)
  Binary     : 19650    (Ratio:   1.54%)
  Ternary    : 3736     (Ratio:   0.29%)
  Conflict   : 1278361  (Average Length:  711.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 1278361  (Average: 16.91 Max: 1444 Sum: 21611323)
  Executed   : 1278299  (Average: 16.90 Max: 1444 Sum: 21605103 Ratio:  99.97%)
  Bounded    : 62       (Average: 100.32 Max: 102 Sum:   6220 Ratio:   0.03%)

Rules        : 766922   (Original: 635077)
Atoms        : 45135   
Bodies       : 588251   (Original: 456406)
  Count      : 7639     (Original: 20328)
Equivalences : 142481   (Atom=Atom: 152 Body=Body: 0 Other: 142329)
Tight        : Yes
Variables    : 428921   (Eliminated:    0 Frozen: 144613)
Constraints  : 3140951  (Binary:  91.6% Ternary:   6.9% Other:   1.6%)

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

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

Iteration 48
Queue:		 [(0,100,47,True)]
Grounded Until:	 100
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 49
Time         : 825.603s (Solving: 812.30s 1st Model: 0.15s Unsat: 0.00s)
CPU Time     : 825.864s

Choices      : 23491981 (Domain: 23311306)
Conflicts    : 1307593  (Analyzed: 1307593)
Restarts     : 4801     (Average: 272.36 Last: 498)
Model-Level  : 3600.0  
Problems     : 49       (Average Length: 102.00 Splits: 0)
Lemmas       : 1307593  (Deleted: 1253474)
  Binary     : 19841    (Ratio:   1.52%)
  Ternary    : 3764     (Ratio:   0.29%)
  Conflict   : 1307593  (Average Length:  710.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 1307593  (Average: 16.72 Max: 1444 Sum: 21868520)
  Executed   : 1307531  (Average: 16.72 Max: 1444 Sum: 21862300 Ratio:  99.97%)
  Bounded    : 62       (Average: 100.32 Max: 102 Sum:   6220 Ratio:   0.03%)

Rules        : 766922   (Original: 635077)
Atoms        : 45135   
Bodies       : 588251   (Original: 456406)
  Count      : 7639     (Original: 20328)
Equivalences : 142481   (Atom=Atom: 152 Body=Body: 0 Other: 142329)
Tight        : Yes
Variables    : 428921   (Eliminated:    0 Frozen: 144613)
Constraints  : 3140951  (Binary:  91.6% Ternary:   6.9% Other:   1.6%)

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

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

Iteration 49
Queue:		 [(0,100,48,True)]
Grounded Until:	 100
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 50
Time         : 841.103s (Solving: 827.71s 1st Model: 0.15s Unsat: 0.00s)
CPU Time     : 841.372s

Choices      : 23741141 (Domain: 23560455)
Conflicts    : 1334367  (Analyzed: 1334367)
Restarts     : 4901     (Average: 272.26 Last: 498)
Model-Level  : 3600.0  
Problems     : 50       (Average Length: 102.00 Splits: 0)
Lemmas       : 1334367  (Deleted: 1279365)
  Binary     : 19926    (Ratio:   1.49%)
  Ternary    : 3783     (Ratio:   0.28%)
  Conflict   : 1334367  (Average Length:  709.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 1334367  (Average: 16.55 Max: 1444 Sum: 22082545)
  Executed   : 1334305  (Average: 16.54 Max: 1444 Sum: 22076325 Ratio:  99.97%)
  Bounded    : 62       (Average: 100.32 Max: 102 Sum:   6220 Ratio:   0.03%)

Rules        : 766922   (Original: 635077)
Atoms        : 45135   
Bodies       : 588251   (Original: 456406)
  Count      : 7639     (Original: 20328)
Equivalences : 142481   (Atom=Atom: 152 Body=Body: 0 Other: 142329)
Tight        : Yes
Variables    : 428921   (Eliminated:    0 Frozen: 144613)
Constraints  : 3140951  (Binary:  91.6% Ternary:   6.9% Other:   1.6%)

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

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

Iteration 50
Queue:		 [(0,100,49,True)]
Grounded Until:	 100
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 51
Time         : 855.265s (Solving: 841.77s 1st Model: 0.15s Unsat: 0.00s)
CPU Time     : 855.540s

Choices      : 23972039 (Domain: 23791339)
Conflicts    : 1361386  (Analyzed: 1361386)
Restarts     : 5001     (Average: 272.22 Last: 498)
Model-Level  : 3600.0  
Problems     : 51       (Average Length: 102.00 Splits: 0)
Lemmas       : 1361386  (Deleted: 1304363)
  Binary     : 20204    (Ratio:   1.48%)
  Ternary    : 3818     (Ratio:   0.28%)
  Conflict   : 1361386  (Average Length:  705.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 1361386  (Average: 16.36 Max: 1444 Sum: 22278386)
  Executed   : 1361324  (Average: 16.36 Max: 1444 Sum: 22272166 Ratio:  99.97%)
  Bounded    : 62       (Average: 100.32 Max: 102 Sum:   6220 Ratio:   0.03%)

Rules        : 766922   (Original: 635077)
Atoms        : 45135   
Bodies       : 588251   (Original: 456406)
  Count      : 7639     (Original: 20328)
Equivalences : 142481   (Atom=Atom: 152 Body=Body: 0 Other: 142329)
Tight        : Yes
Variables    : 428921   (Eliminated:    0 Frozen: 144613)
Constraints  : 3140951  (Binary:  91.6% Ternary:   6.9% Other:   1.6%)

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

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

Iteration 51
Queue:		 [(0,100,50,True)]
Grounded Until:	 100
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 52
Time         : 869.081s (Solving: 855.48s 1st Model: 0.15s Unsat: 0.00s)
CPU Time     : 869.360s

Choices      : 24153558 (Domain: 23972858)
Conflicts    : 1384588  (Analyzed: 1384588)
Restarts     : 5101     (Average: 271.43 Last: 498)
Model-Level  : 3600.0  
Problems     : 52       (Average Length: 102.00 Splits: 0)
Lemmas       : 1384588  (Deleted: 1327358)
  Binary     : 20332    (Ratio:   1.47%)
  Ternary    : 3836     (Ratio:   0.28%)
  Conflict   : 1384588  (Average Length:  701.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 1384588  (Average: 16.20 Max: 1444 Sum: 22434554)
  Executed   : 1384526  (Average: 16.20 Max: 1444 Sum: 22428334 Ratio:  99.97%)
  Bounded    : 62       (Average: 100.32 Max: 102 Sum:   6220 Ratio:   0.03%)

Rules        : 766922   (Original: 635077)
Atoms        : 45135   
Bodies       : 588251   (Original: 456406)
  Count      : 7639     (Original: 20328)
Equivalences : 142481   (Atom=Atom: 152 Body=Body: 0 Other: 142329)
Tight        : Yes
Variables    : 428921   (Eliminated:    0 Frozen: 144613)
Constraints  : 3140951  (Binary:  91.6% Ternary:   6.9% Other:   1.6%)

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

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

Iteration 52
Queue:		 [(0,100,51,True)]
Grounded Until:	 100
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 53
Time         : 887.234s (Solving: 873.52s 1st Model: 0.15s Unsat: 0.00s)
CPU Time     : 887.520s

Choices      : 24410147 (Domain: 24229447)
Conflicts    : 1416087  (Analyzed: 1416087)
Restarts     : 5201     (Average: 272.27 Last: 498)
Model-Level  : 3600.0  
Problems     : 53       (Average Length: 102.00 Splits: 0)
Lemmas       : 1416087  (Deleted: 1360698)
  Binary     : 20447    (Ratio:   1.44%)
  Ternary    : 3865     (Ratio:   0.27%)
  Conflict   : 1416087  (Average Length:  700.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 1416087  (Average: 16.00 Max: 1444 Sum: 22662902)
  Executed   : 1416025  (Average: 16.00 Max: 1444 Sum: 22656682 Ratio:  99.97%)
  Bounded    : 62       (Average: 100.32 Max: 102 Sum:   6220 Ratio:   0.03%)

Rules        : 766922   (Original: 635077)
Atoms        : 45135   
Bodies       : 588251   (Original: 456406)
  Count      : 7639     (Original: 20328)
Equivalences : 142481   (Atom=Atom: 152 Body=Body: 0 Other: 142329)
Tight        : Yes
Variables    : 428921   (Eliminated:    0 Frozen: 144613)
Constraints  : 3140951  (Binary:  91.6% Ternary:   6.9% Other:   1.6%)

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

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

Iteration 53
Queue:		 [(0,100,52,True)]
Grounded Until:	 100
Solving...
*** Info : (planner): INTERRUPTED by signal!
UNKNOWN

INTERRUPTED  : 1

Models       : 0+
Calls        : 54
Time         : 894.963s (Solving: 881.18s 1st Model: 0.15s Unsat: 0.00s)
CPU Time     : 895.236s

Choices      : 24539614 (Domain: 24358911)
Conflicts    : 1429852  (Analyzed: 1429852)
Restarts     : 5262     (Average: 271.73 Last: 519)
Model-Level  : 3600.0  
Problems     : 54       (Average Length: 102.00 Splits: 0)
Lemmas       : 1429852  (Deleted: 1375535)
  Binary     : 20493    (Ratio:   1.43%)
  Ternary    : 3870     (Ratio:   0.27%)
  Conflict   : 1429852  (Average Length:  699.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 1429852  (Average: 15.92 Max: 1444 Sum: 22766577)
  Executed   : 1429790  (Average: 15.92 Max: 1444 Sum: 22760357 Ratio:  99.97%)
  Bounded    : 62       (Average: 100.32 Max: 102 Sum:   6220 Ratio:   0.03%)

Rules        : 766922   (Original: 635077)
Atoms        : 45135   
Bodies       : 588251   (Original: 456406)
  Count      : 7639     (Original: 20328)
Equivalences : 142481   (Atom=Atom: 152 Body=Body: 0 Other: 142329)
Tight        : Yes
Variables    : 428921   (Eliminated:    0 Frozen: 144613)
Constraints  : 3140951  (Binary:  91.6% Ternary:   6.9% Other:   1.6%)

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


