1
0
tplp-planning-benchmark/gc-ta1-tt1/ipc-2011_barman-sequential-satisficing_2.out

6370 lines
234 KiB
Plaintext
Raw Normal View History

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-2.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-2.pddl
Parsing...
Parsing: [0.030s CPU, 0.033s wall-clock]
Normalizing task... [0.000s CPU, 0.003s wall-clock]
Instantiating...
Generating Datalog program... [0.010s CPU, 0.008s wall-clock]
Normalizing Datalog program...
Normalizing Datalog program: [0.040s CPU, 0.045s wall-clock]
Preparing model... [0.020s CPU, 0.023s wall-clock]
Generated 115 rules.
Computing model... [0.340s CPU, 0.330s wall-clock]
2025 relevant atoms
2105 auxiliary atoms
4130 final queue length
7122 total queue pushes
Completing instantiation... [0.600s CPU, 0.599s wall-clock]
Instantiating: [1.010s CPU, 1.011s wall-clock]
Computing fact groups...
Finding invariants...
24 initial candidates
Finding invariants: [0.110s CPU, 0.112s wall-clock]
Checking invariant weight... [0.000s CPU, 0.001s wall-clock]
Instantiating groups... [0.010s CPU, 0.006s wall-clock]
Collecting mutex groups... [0.000s CPU, 0.000s wall-clock]
Choosing groups...
207 uncovered facts
Choosing groups: [0.000s CPU, 0.001s wall-clock]
Building translation key... [0.000s CPU, 0.007s wall-clock]
Computing fact groups: [0.140s CPU, 0.143s wall-clock]
Building STRIPS to SAS dictionary... [0.000s CPU, 0.002s wall-clock]
Building dictionary for full mutex groups... [0.010s CPU, 0.002s wall-clock]
Building mutex information...
Building mutex information: [0.000s CPU, 0.002s wall-clock]
Translating task...
Processing axioms...
Simplifying axioms... [0.000s CPU, 0.000s wall-clock]
Processing axioms: [0.030s CPU, 0.034s wall-clock]
Translating task: [0.660s CPU, 0.661s 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.309s 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.208s 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.270s CPU, 0.295s wall-clock]
Done! [2.670s CPU, 2.697s wall-clock]
planner.py version 0.0.1
Time: 0.58s
Memory: 86MB
Iteration 1
Queue: [(0,0,0,True), (1,5,0,True), (2,10,0,True), (3,15,0,True), (4,20,0,True), (5,25,0,True), (6,30,0,True)]
Grounded Until: 0
Solving...
[start: stats after solve call]
Models : 0
Calls : 1
Time : 0.665s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
CPU Time : 0.580s
Choices : 0
Conflicts : 0 (Analyzed: 0)
Restarts : 0
Problems : 1 (Average Length: 2.00 Splits: 0)
Lemmas : 0 (Deleted: 0)
Binary : 0 (Ratio: 0.00%)
Ternary : 0 (Ratio: 0.00%)
Conflict : 0 (Average Length: 0.0 Ratio: 0.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 0 (Average: 0.00 Max: 0 Sum: 0)
Executed : 0 (Average: 0.00 Max: 0 Sum: 0 Ratio: 0.00%)
Bounded : 0 (Average: 0.00 Max: 0 Sum: 0 Ratio: 100.00%)
Rules : 38518
Atoms : 38518
Bodies : 1 (Original: 0)
Tight : Yes
Variables : 0 (Eliminated: 0 Frozen: 0)
Constraints : 0 (Binary: 0.0% Ternary: 0.0% Other: 0.0%)
Memory Peak : 222MB
Max. Length : 0 steps
Models : 0
[endof: stats after solve call]
Solving Time: 0.00s
Memory: 158MB (+72MB)
UNSAT
Iteration Time: 0.00s
Iteration 2
Queue: [(1,5,0,True), (2,10,0,True), (3,15,0,True), (4,20,0,True), (5,25,0,True), (6,30,0,True)]
Grounded Until: 0
Expected Memory: 158MB
Grounding... [('step', [1]), ('step', [2]), ('step', [3]), ('step', [4]), ('step', [5]), ('check', [5])]
Grounding Time: 0.15s
Memory: 158MB (+0MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 1+
Calls : 2
Time : 0.906s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
CPU Time : 0.820s
Choices : 105 (Domain: 26)
Conflicts : 4 (Analyzed: 4)
Restarts : 0
Model-Level : 98.0
Problems : 2 (Average Length: 4.50 Splits: 0)
Lemmas : 4 (Deleted: 0)
Binary : 2 (Ratio: 50.00%)
Ternary : 0 (Ratio: 0.00%)
Conflict : 4 (Average Length: 12.5 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 4 (Average: 3.75 Max: 11 Sum: 15)
Executed : 3 (Average: 3.50 Max: 11 Sum: 14 Ratio: 93.33%)
Bounded : 1 (Average: 1.00 Max: 1 Sum: 1 Ratio: 6.67%)
Rules : 38518
Atoms : 38518
Bodies : 1 (Original: 0)
Tight : Yes
Variables : 10322 (Eliminated: 0 Frozen: 120)
Constraints : 36431 (Binary: 95.0% Ternary: 3.5% Other: 1.5%)
Memory Peak : 222MB
Max. Length : 0 steps
Models : 1
[endof: stats after solve call]
Solving Time: 0.01s
Memory: 160MB (+2MB)
SAT
Testing...
NOT SERIALIZABLE
Testing Time: 0.59s
Memory: 179MB (+19MB)
Solving...
[start: stats after solve call]
Models : 0
Calls : 3
Time : 0.989s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
CPU Time : 0.904s
Choices : 122 (Domain: 27)
Conflicts : 13 (Analyzed: 12)
Restarts : 0
Model-Level : 98.0
Problems : 3 (Average Length: 5.33 Splits: 0)
Lemmas : 12 (Deleted: 0)
Binary : 4 (Ratio: 33.33%)
Ternary : 4 (Ratio: 33.33%)
Conflict : 12 (Average Length: 6.2 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 12 (Average: 2.83 Max: 11 Sum: 34)
Executed : 9 (Average: 2.58 Max: 11 Sum: 31 Ratio: 91.18%)
Bounded : 3 (Average: 1.00 Max: 1 Sum: 3 Ratio: 8.82%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 12735 (Eliminated: 0 Frozen: 2876)
Constraints : 54291 (Binary: 92.2% Ternary: 5.5% Other: 2.3%)
Memory Peak : 222MB
Max. Length : 0 steps
Models : 1
[endof: stats after solve call]
Solving Time: 0.01s
Memory: 179MB (+0MB)
UNSAT
Iteration Time: 0.85s
Iteration 3
Queue: [(2,10,0,True), (3,15,0,True), (4,20,0,True), (5,25,0,True), (6,30,0,True)]
Grounded Until: 5
Expected Memory: 181.0MB
Grounding... [('step', [6]), ('step', [7]), ('step', [8]), ('step', [9]), ('step', [10]), ('check', [10])]
Grounding Time: 0.29s
Memory: 179MB (+0MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0
Calls : 4
Time : 1.949s (Solving: 0.55s 1st Model: 0.00s Unsat: 0.55s)
CPU Time : 1.864s
Choices : 14957 (Domain: 14257)
Conflicts : 2036 (Analyzed: 2034)
Restarts : 23 (Average: 88.43 Last: 42)
Model-Level : 98.0
Problems : 4 (Average Length: 7.00 Splits: 0)
Lemmas : 2034 (Deleted: 675)
Binary : 219 (Ratio: 10.77%)
Ternary : 248 (Ratio: 12.19%)
Conflict : 2034 (Average Length: 40.8 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 2034 (Average: 7.41 Max: 81 Sum: 15075)
Executed : 1998 (Average: 7.24 Max: 81 Sum: 14720 Ratio: 97.65%)
Bounded : 36 (Average: 9.86 Max: 12 Sum: 355 Ratio: 2.35%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 35311 (Eliminated: 0 Frozen: 10341)
Constraints : 227336 (Binary: 91.7% Ternary: 6.3% Other: 2.0%)
Memory Peak : 222MB
Max. Length : 5 steps
Models : 1
[endof: stats after solve call]
Solving Time: 0.57s
Memory: 186MB (+7MB)
UNSAT
Iteration Time: 0.97s
Iteration 4
Queue: [(3,15,0,True), (4,20,0,True), (5,25,0,True), (6,30,0,True)]
Grounded Until: 10
Expected Memory: 193.0MB
Grounding... [('step', [11]), ('step', [12]), ('step', [13]), ('step', [14]), ('step', [15]), ('check', [15])]
Grounding Time: 0.37s
Memory: 195MB (+9MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 5
Time : 5.280s (Solving: 3.36s 1st Model: 0.00s Unsat: 0.55s)
CPU Time : 5.200s
Choices : 71007 (Domain: 69067)
Conflicts : 10342 (Analyzed: 10340)
Restarts : 123 (Average: 84.07 Last: 63)
Model-Level : 98.0
Problems : 5 (Average Length: 9.00 Splits: 0)
Lemmas : 10340 (Deleted: 5208)
Binary : 537 (Ratio: 5.19%)
Ternary : 360 (Ratio: 3.48%)
Conflict : 10340 (Average Length: 156.0 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 10340 (Average: 6.63 Max: 121 Sum: 68512)
Executed : 10284 (Average: 6.56 Max: 121 Sum: 67829 Ratio: 99.00%)
Bounded : 56 (Average: 12.20 Max: 17 Sum: 683 Ratio: 1.00%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 57887 (Eliminated: 0 Frozen: 17806)
Constraints : 376285 (Binary: 91.7% Ternary: 6.3% Other: 2.0%)
Memory Peak : 222MB
Max. Length : 10 steps
Models : 1
[endof: stats after solve call]
Solving Time: 2.83s
Memory: 205MB (+10MB)
UNKNOWN
Iteration Time: 3.34s
Iteration 5
Queue: [(4,20,0,True), (5,25,0,True), (6,30,0,True)]
Grounded Until: 15
Expected Memory: 224.0MB
Grounding... [('step', [16]), ('step', [17]), ('step', [18]), ('step', [19]), ('step', [20]), ('check', [20])]
Grounding Time: 0.31s
Memory: 212MB (+7MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 6
Time : 9.376s (Solving: 6.99s 1st Model: 0.00s Unsat: 0.55s)
CPU Time : 9.300s
Choices : 208136 (Domain: 202075)
Conflicts : 19417 (Analyzed: 19415)
Restarts : 223 (Average: 87.06 Last: 64)
Model-Level : 98.0
Problems : 6 (Average Length: 11.17 Splits: 0)
Lemmas : 19415 (Deleted: 12302)
Binary : 1319 (Ratio: 6.79%)
Ternary : 750 (Ratio: 3.86%)
Conflict : 19415 (Average Length: 168.3 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 19415 (Average: 10.46 Max: 166 Sum: 203156)
Executed : 19334 (Average: 10.40 Max: 166 Sum: 201983 Ratio: 99.42%)
Bounded : 81 (Average: 14.48 Max: 22 Sum: 1173 Ratio: 0.58%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 80463 (Eliminated: 0 Frozen: 25271)
Constraints : 546975 (Binary: 91.7% Ternary: 6.4% Other: 2.0%)
Memory Peak : 224MB
Max. Length : 15 steps
Models : 1
[endof: stats after solve call]
Solving Time: 3.66s
Memory: 224MB (+12MB)
UNKNOWN
Iteration Time: 4.11s
Iteration 6
Queue: [(5,25,0,True), (6,30,0,True)]
Grounded Until: 20
Expected Memory: 243.0MB
Grounding... [('step', [21]), ('step', [22]), ('step', [23]), ('step', [24]), ('step', [25]), ('check', [25])]
Grounding Time: 0.32s
Memory: 229MB (+5MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 7
Time : 14.854s (Solving: 11.98s 1st Model: 0.00s Unsat: 0.55s)
CPU Time : 14.780s
Choices : 296587 (Domain: 277643)
Conflicts : 28944 (Analyzed: 28942)
Restarts : 323 (Average: 89.60 Last: 64)
Model-Level : 98.0
Problems : 7 (Average Length: 13.43 Splits: 0)
Lemmas : 28942 (Deleted: 21584)
Binary : 1591 (Ratio: 5.50%)
Ternary : 905 (Ratio: 3.13%)
Conflict : 28942 (Average Length: 348.3 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 28942 (Average: 9.72 Max: 385 Sum: 281352)
Executed : 28860 (Average: 9.68 Max: 385 Sum: 280152 Ratio: 99.57%)
Bounded : 82 (Average: 14.63 Max: 27 Sum: 1200 Ratio: 0.43%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 103039 (Eliminated: 0 Frozen: 32736)
Constraints : 705988 (Binary: 91.6% Ternary: 6.4% Other: 1.9%)
Memory Peak : 245MB
Max. Length : 20 steps
Models : 1
[endof: stats after solve call]
Solving Time: 5.02s
Memory: 238MB (+9MB)
UNKNOWN
Iteration Time: 5.49s
Iteration 7
Queue: [(6,30,0,True)]
Grounded Until: 25
Expected Memory: 257.0MB
Grounding... [('step', [26]), ('step', [27]), ('step', [28]), ('step', [29]), ('step', [30]), ('check', [30])]
Grounding Time: 0.32s
Memory: 244MB (+6MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 8
Time : 20.601s (Solving: 17.21s 1st Model: 0.00s Unsat: 0.55s)
CPU Time : 20.528s
Choices : 410110 (Domain: 382274)
Conflicts : 38125 (Analyzed: 38123)
Restarts : 423 (Average: 90.13 Last: 110)
Model-Level : 98.0
Problems : 8 (Average Length: 15.75 Splits: 0)
Lemmas : 38123 (Deleted: 28645)
Binary : 2040 (Ratio: 5.35%)
Ternary : 1179 (Ratio: 3.09%)
Conflict : 38123 (Average Length: 378.5 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 38123 (Average: 10.08 Max: 385 Sum: 384215)
Executed : 38039 (Average: 10.05 Max: 385 Sum: 382955 Ratio: 99.67%)
Bounded : 84 (Average: 15.00 Max: 32 Sum: 1260 Ratio: 0.33%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 125615 (Eliminated: 0 Frozen: 40201)
Constraints : 879032 (Binary: 91.6% Ternary: 6.4% Other: 1.9%)
Memory Peak : 262MB
Max. Length : 25 steps
Models : 1
[endof: stats after solve call]
Solving Time: 5.28s
Memory: 262MB (+18MB)
UNKNOWN
Iteration Time: 5.76s
Iteration 8
Queue: [(3,15,1,True), (4,20,1,True), (5,25,1,True), (6,30,1,True), (7,35,0,True), (8,40,0,True), (9,45,0,True), (10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True)]
Grounded Until: 30
Blocking actions...
Solving...
[start: stats after solve call]
Models : 0
Calls : 9
Time : 21.025s (Solving: 17.60s 1st Model: 0.00s Unsat: 0.93s)
CPU Time : 20.952s
Choices : 412817 (Domain: 384908)
Conflicts : 38881 (Analyzed: 38878)
Restarts : 432 (Average: 90.00 Last: 110)
Model-Level : 98.0
Problems : 9 (Average Length: 17.56 Splits: 0)
Lemmas : 38878 (Deleted: 28645)
Binary : 2075 (Ratio: 5.34%)
Ternary : 1188 (Ratio: 3.06%)
Conflict : 38878 (Average Length: 375.7 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 38878 (Average: 9.95 Max: 385 Sum: 386889)
Executed : 38793 (Average: 9.92 Max: 385 Sum: 385628 Ratio: 99.67%)
Bounded : 85 (Average: 14.84 Max: 32 Sum: 1261 Ratio: 0.33%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 125615 (Eliminated: 0 Frozen: 40201)
Constraints : 879006 (Binary: 91.6% Ternary: 6.4% Other: 1.9%)
Memory Peak : 262MB
Max. Length : 30 steps
Models : 1
[endof: stats after solve call]
Solving Time: 0.41s
Memory: 262MB (+0MB)
UNSAT
Iteration Time: 0.43s
Iteration 9
Queue: [(4,20,1,True), (5,25,1,True), (6,30,1,True), (7,35,0,True), (8,40,0,True), (9,45,0,True), (10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True)]
Grounded Until: 30
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 10
Time : 26.960s (Solving: 23.50s 1st Model: 0.00s Unsat: 0.93s)
CPU Time : 26.892s
Choices : 503603 (Domain: 474265)
Conflicts : 47956 (Analyzed: 47953)
Restarts : 532 (Average: 90.14 Last: 110)
Model-Level : 98.0
Problems : 10 (Average Length: 19.00 Splits: 0)
Lemmas : 47953 (Deleted: 36581)
Binary : 2293 (Ratio: 4.78%)
Ternary : 1287 (Ratio: 2.68%)
Conflict : 47953 (Average Length: 382.3 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 47953 (Average: 9.91 Max: 385 Sum: 475353)
Executed : 47866 (Average: 9.89 Max: 385 Sum: 474059 Ratio: 99.73%)
Bounded : 87 (Average: 14.87 Max: 32 Sum: 1294 Ratio: 0.27%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 125615 (Eliminated: 0 Frozen: 40201)
Constraints : 879006 (Binary: 91.6% Ternary: 6.4% Other: 1.9%)
Memory Peak : 262MB
Max. Length : 30 steps
Models : 1
[endof: stats after solve call]
Solving Time: 5.92s
Memory: 262MB (+0MB)
UNKNOWN
Iteration Time: 5.94s
Iteration 10
Queue: [(5,25,1,True), (6,30,1,True), (7,35,0,True), (8,40,0,True), (9,45,0,True), (10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True)]
Grounded Until: 30
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 11
Time : 32.653s (Solving: 29.16s 1st Model: 0.00s Unsat: 0.93s)
CPU Time : 32.588s
Choices : 584823 (Domain: 546475)
Conflicts : 57197 (Analyzed: 57194)
Restarts : 632 (Average: 90.50 Last: 110)
Model-Level : 98.0
Problems : 11 (Average Length: 20.18 Splits: 0)
Lemmas : 57194 (Deleted: 44583)
Binary : 2650 (Ratio: 4.63%)
Ternary : 1394 (Ratio: 2.44%)
Conflict : 57194 (Average Length: 421.1 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 57194 (Average: 9.55 Max: 385 Sum: 546391)
Executed : 57107 (Average: 9.53 Max: 385 Sum: 545097 Ratio: 99.76%)
Bounded : 87 (Average: 14.87 Max: 32 Sum: 1294 Ratio: 0.24%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 125615 (Eliminated: 0 Frozen: 40201)
Constraints : 878992 (Binary: 91.6% Ternary: 6.4% Other: 1.9%)
Memory Peak : 262MB
Max. Length : 30 steps
Models : 1
[endof: stats after solve call]
Solving Time: 5.69s
Memory: 262MB (+0MB)
UNKNOWN
Iteration Time: 5.70s
Iteration 11
Queue: [(6,30,1,True), (7,35,0,True), (8,40,0,True), (9,45,0,True), (10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True)]
Grounded Until: 30
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 12
Time : 37.757s (Solving: 34.23s 1st Model: 0.00s Unsat: 0.93s)
CPU Time : 37.696s
Choices : 673308 (Domain: 626418)
Conflicts : 66081 (Analyzed: 66078)
Restarts : 732 (Average: 90.27 Last: 110)
Model-Level : 98.0
Problems : 12 (Average Length: 21.17 Splits: 0)
Lemmas : 66078 (Deleted: 52974)
Binary : 2999 (Ratio: 4.54%)
Ternary : 1489 (Ratio: 2.25%)
Conflict : 66078 (Average Length: 466.5 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 66078 (Average: 9.41 Max: 385 Sum: 622095)
Executed : 65991 (Average: 9.39 Max: 385 Sum: 620801 Ratio: 99.79%)
Bounded : 87 (Average: 14.87 Max: 32 Sum: 1294 Ratio: 0.21%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 125615 (Eliminated: 0 Frozen: 40201)
Constraints : 878992 (Binary: 91.6% Ternary: 6.4% Other: 1.9%)
Memory Peak : 262MB
Max. Length : 30 steps
Models : 1
[endof: stats after solve call]
Solving Time: 5.09s
Memory: 262MB (+0MB)
UNKNOWN
Iteration Time: 5.11s
Iteration 12
Queue: [(7,35,0,True), (8,40,0,True), (9,45,0,True), (10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True)]
Grounded Until: 30
Expected Memory: 286.0MB
Grounding... [('step', [31]), ('step', [32]), ('step', [33]), ('step', [34]), ('step', [35]), ('check', [35])]
Grounding Time: 0.33s
Memory: 263MB (+1MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 13
Time : 43.443s (Solving: 39.38s 1st Model: 0.00s Unsat: 0.93s)
CPU Time : 43.384s
Choices : 783397 (Domain: 734217)
Conflicts : 74990 (Analyzed: 74987)
Restarts : 832 (Average: 90.13 Last: 110)
Model-Level : 98.0
Problems : 13 (Average Length: 22.38 Splits: 0)
Lemmas : 74987 (Deleted: 61195)
Binary : 3460 (Ratio: 4.61%)
Ternary : 1576 (Ratio: 2.10%)
Conflict : 74987 (Average Length: 459.2 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 74987 (Average: 9.64 Max: 385 Sum: 722637)
Executed : 74900 (Average: 9.62 Max: 385 Sum: 721343 Ratio: 99.82%)
Bounded : 87 (Average: 14.87 Max: 32 Sum: 1294 Ratio: 0.18%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 148191 (Eliminated: 0 Frozen: 47666)
Constraints : 1052037 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 285MB
Max. Length : 30 steps
Models : 1
[endof: stats after solve call]
Solving Time: 5.19s
Memory: 272MB (+9MB)
UNKNOWN
Iteration Time: 5.70s
Iteration 13
Queue: [(8,40,0,True), (9,45,0,True), (10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True)]
Grounded Until: 35
Expected Memory: 296.0MB
Grounding... [('step', [36]), ('step', [37]), ('step', [38]), ('step', [39]), ('step', [40]), ('check', [40])]
Grounding Time: 0.39s
Memory: 284MB (+12MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 14
Time : 50.813s (Solving: 46.14s 1st Model: 0.00s Unsat: 0.93s)
CPU Time : 50.760s
Choices : 935138 (Domain: 882335)
Conflicts : 84765 (Analyzed: 84762)
Restarts : 932 (Average: 90.95 Last: 168)
Model-Level : 98.0
Problems : 14 (Average Length: 23.79 Splits: 0)
Lemmas : 84762 (Deleted: 69086)
Binary : 3920 (Ratio: 4.62%)
Ternary : 1628 (Ratio: 1.92%)
Conflict : 84762 (Average Length: 488.4 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 84762 (Average: 10.13 Max: 385 Sum: 858836)
Executed : 84675 (Average: 10.12 Max: 385 Sum: 857542 Ratio: 99.85%)
Bounded : 87 (Average: 14.87 Max: 32 Sum: 1294 Ratio: 0.15%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 170767 (Eliminated: 0 Frozen: 55131)
Constraints : 1225082 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 310MB
Max. Length : 35 steps
Models : 1
[endof: stats after solve call]
Solving Time: 6.80s
Memory: 294MB (+10MB)
UNKNOWN
Iteration Time: 7.38s
Iteration 14
Queue: [(9,45,0,True), (10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True)]
Grounded Until: 40
Expected Memory: 318.0MB
Grounding... [('step', [41]), ('step', [42]), ('step', [43]), ('step', [44]), ('step', [45]), ('check', [45])]
Grounding Time: 0.32s
Memory: 302MB (+8MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 15
Time : 58.316s (Solving: 53.10s 1st Model: 0.00s Unsat: 0.93s)
CPU Time : 58.268s
Choices : 1063270 (Domain: 1009088)
Conflicts : 94449 (Analyzed: 94446)
Restarts : 1032 (Average: 91.52 Last: 168)
Model-Level : 98.0
Problems : 15 (Average Length: 25.33 Splits: 0)
Lemmas : 94446 (Deleted: 78368)
Binary : 4126 (Ratio: 4.37%)
Ternary : 1675 (Ratio: 1.77%)
Conflict : 94446 (Average Length: 522.2 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 94446 (Average: 10.27 Max: 387 Sum: 970288)
Executed : 94359 (Average: 10.26 Max: 387 Sum: 968994 Ratio: 99.87%)
Bounded : 87 (Average: 14.87 Max: 32 Sum: 1294 Ratio: 0.13%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 193343 (Eliminated: 0 Frozen: 62596)
Constraints : 1398127 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 327MB
Max. Length : 40 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.00s
Memory: 325MB (+23MB)
UNKNOWN
Iteration Time: 7.51s
Iteration 15
Queue: [(10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True)]
Grounded Until: 45
Expected Memory: 356.0MB
Grounding... [('step', [46]), ('step', [47]), ('step', [48]), ('step', [49]), ('step', [50]), ('check', [50])]
Grounding Time: 0.32s
Memory: 325MB (+0MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 16
Time : 64.720s (Solving: 58.94s 1st Model: 0.00s Unsat: 0.93s)
CPU Time : 64.672s
Choices : 1176855 (Domain: 1121639)
Conflicts : 103168 (Analyzed: 103165)
Restarts : 1132 (Average: 91.14 Last: 168)
Model-Level : 98.0
Problems : 16 (Average Length: 27.00 Splits: 0)
Lemmas : 103165 (Deleted: 87524)
Binary : 4310 (Ratio: 4.18%)
Ternary : 1730 (Ratio: 1.68%)
Conflict : 103165 (Average Length: 543.2 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 103165 (Average: 10.35 Max: 387 Sum: 1067948)
Executed : 103078 (Average: 10.34 Max: 387 Sum: 1066654 Ratio: 99.88%)
Bounded : 87 (Average: 14.87 Max: 32 Sum: 1294 Ratio: 0.12%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 215919 (Eliminated: 0 Frozen: 70061)
Constraints : 1571172 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 353MB
Max. Length : 45 steps
Models : 1
[endof: stats after solve call]
Solving Time: 5.90s
Memory: 333MB (+8MB)
UNKNOWN
Iteration Time: 6.42s
Iteration 16
Queue: [(11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True)]
Grounded Until: 50
Expected Memory: 364.0MB
Grounding... [('step', [51]), ('step', [52]), ('step', [53]), ('step', [54]), ('step', [55]), ('check', [55])]
Grounding Time: 0.36s
Memory: 337MB (+4MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 17
Time : 72.034s (Solving: 65.64s 1st Model: 0.00s Unsat: 0.93s)
CPU Time : 71.988s
Choices : 1318818 (Domain: 1261192)
Conflicts : 111961 (Analyzed: 111958)
Restarts : 1232 (Average: 90.88 Last: 168)
Model-Level : 98.0
Problems : 17 (Average Length: 28.76 Splits: 0)
Lemmas : 111958 (Deleted: 95917)
Binary : 4549 (Ratio: 4.06%)
Ternary : 1783 (Ratio: 1.59%)
Conflict : 111958 (Average Length: 575.8 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 111958 (Average: 10.63 Max: 387 Sum: 1190578)
Executed : 111870 (Average: 10.62 Max: 387 Sum: 1189227 Ratio: 99.89%)
Bounded : 88 (Average: 15.35 Max: 57 Sum: 1351 Ratio: 0.11%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 238495 (Eliminated: 0 Frozen: 77526)
Constraints : 1744217 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 372MB
Max. Length : 50 steps
Models : 1
[endof: stats after solve call]
Solving Time: 6.75s
Memory: 349MB (+12MB)
UNKNOWN
Iteration Time: 7.32s
Iteration 17
Queue: [(12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True)]
Grounded Until: 55
Expected Memory: 380.0MB
Grounding... [('step', [56]), ('step', [57]), ('step', [58]), ('step', [59]), ('step', [60]), ('check', [60])]
Grounding Time: 0.32s
Memory: 352MB (+3MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 18
Time : 78.561s (Solving: 71.57s 1st Model: 0.00s Unsat: 0.93s)
CPU Time : 78.516s
Choices : 1439378 (Domain: 1380543)
Conflicts : 120420 (Analyzed: 120417)
Restarts : 1332 (Average: 90.40 Last: 168)
Model-Level : 98.0
Problems : 18 (Average Length: 30.61 Splits: 0)
Lemmas : 120417 (Deleted: 102156)
Binary : 4686 (Ratio: 3.89%)
Ternary : 1820 (Ratio: 1.51%)
Conflict : 120417 (Average Length: 580.4 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 120417 (Average: 10.75 Max: 387 Sum: 1294401)
Executed : 120329 (Average: 10.74 Max: 387 Sum: 1293050 Ratio: 99.90%)
Bounded : 88 (Average: 15.35 Max: 57 Sum: 1351 Ratio: 0.10%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 261071 (Eliminated: 0 Frozen: 84991)
Constraints : 1917248 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 389MB
Max. Length : 55 steps
Models : 1
[endof: stats after solve call]
Solving Time: 6.00s
Memory: 364MB (+12MB)
UNKNOWN
Iteration Time: 6.54s
Iteration 18
Queue: [(13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True)]
Grounded Until: 60
Expected Memory: 395.0MB
Grounding... [('step', [61]), ('step', [62]), ('step', [63]), ('step', [64]), ('step', [65]), ('check', [65])]
Grounding Time: 0.32s
Memory: 367MB (+3MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 19
Time : 85.507s (Solving: 77.91s 1st Model: 0.00s Unsat: 0.93s)
CPU Time : 85.464s
Choices : 1572375 (Domain: 1511607)
Conflicts : 128689 (Analyzed: 128686)
Restarts : 1432 (Average: 89.86 Last: 168)
Model-Level : 98.0
Problems : 19 (Average Length: 32.53 Splits: 0)
Lemmas : 128686 (Deleted: 110513)
Binary : 4795 (Ratio: 3.73%)
Ternary : 1847 (Ratio: 1.44%)
Conflict : 128686 (Average Length: 597.2 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 128686 (Average: 10.93 Max: 387 Sum: 1407040)
Executed : 128598 (Average: 10.92 Max: 387 Sum: 1405689 Ratio: 99.90%)
Bounded : 88 (Average: 15.35 Max: 57 Sum: 1351 Ratio: 0.10%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 283647 (Eliminated: 0 Frozen: 92456)
Constraints : 2090293 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 407MB
Max. Length : 60 steps
Models : 1
[endof: stats after solve call]
Solving Time: 6.40s
Memory: 401MB (+34MB)
UNKNOWN
Iteration Time: 6.96s
Iteration 19
Queue: [(14,70,0,True), (15,75,0,True), (16,80,0,True)]
Grounded Until: 65
Expected Memory: 438.0MB
Grounding... [('step', [66]), ('step', [67]), ('step', [68]), ('step', [69]), ('step', [70]), ('check', [70])]
Grounding Time: 0.37s
Memory: 401MB (+0MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 20
Time : 92.791s (Solving: 84.53s 1st Model: 0.00s Unsat: 0.93s)
CPU Time : 92.752s
Choices : 1711181 (Domain: 1648766)
Conflicts : 137454 (Analyzed: 137451)
Restarts : 1532 (Average: 89.72 Last: 168)
Model-Level : 98.0
Problems : 20 (Average Length: 34.50 Splits: 0)
Lemmas : 137451 (Deleted: 120278)
Binary : 4877 (Ratio: 3.55%)
Ternary : 1866 (Ratio: 1.36%)
Conflict : 137451 (Average Length: 612.9 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 137451 (Average: 11.09 Max: 444 Sum: 1524316)
Executed : 137363 (Average: 11.08 Max: 444 Sum: 1522965 Ratio: 99.91%)
Bounded : 88 (Average: 15.35 Max: 57 Sum: 1351 Ratio: 0.09%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 306223 (Eliminated: 0 Frozen: 99921)
Constraints : 2263338 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 439MB
Max. Length : 65 steps
Models : 1
[endof: stats after solve call]
Solving Time: 6.69s
Memory: 407MB (+6MB)
UNKNOWN
Iteration Time: 7.29s
Iteration 20
Queue: [(15,75,0,True), (16,80,0,True)]
Grounded Until: 70
Expected Memory: 444.0MB
Grounding... [('step', [71]), ('step', [72]), ('step', [73]), ('step', [74]), ('step', [75]), ('check', [75])]
Grounding Time: 0.34s
Memory: 408MB (+1MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 21
Time : 102.229s (Solving: 93.32s 1st Model: 0.00s Unsat: 0.93s)
CPU Time : 102.192s
Choices : 1986878 (Domain: 1919957)
Conflicts : 146622 (Analyzed: 146619)
Restarts : 1632 (Average: 89.84 Last: 168)
Model-Level : 98.0
Problems : 21 (Average Length: 36.52 Splits: 0)
Lemmas : 146619 (Deleted: 128698)
Binary : 5164 (Ratio: 3.52%)
Ternary : 1925 (Ratio: 1.31%)
Conflict : 146619 (Average Length: 628.0 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 146619 (Average: 12.08 Max: 475 Sum: 1771517)
Executed : 146531 (Average: 12.07 Max: 475 Sum: 1770166 Ratio: 99.92%)
Bounded : 88 (Average: 15.35 Max: 57 Sum: 1351 Ratio: 0.08%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 328799 (Eliminated: 0 Frozen: 107386)
Constraints : 2436383 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 453MB
Max. Length : 70 steps
Models : 1
[endof: stats after solve call]
Solving Time: 8.87s
Memory: 421MB (+13MB)
UNKNOWN
Iteration Time: 9.45s
Iteration 21
Queue: [(16,80,0,True)]
Grounded Until: 75
Expected Memory: 458.0MB
Grounding... [('step', [76]), ('step', [77]), ('step', [78]), ('step', [79]), ('step', [80]), ('check', [80])]
Grounding Time: 0.49s
Memory: 441MB (+20MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 22
Time : 111.454s (Solving: 101.73s 1st Model: 0.00s Unsat: 0.93s)
CPU Time : 111.420s
Choices : 2308177 (Domain: 2234336)
Conflicts : 155910 (Analyzed: 155907)
Restarts : 1732 (Average: 90.02 Last: 168)
Model-Level : 98.0
Problems : 22 (Average Length: 38.59 Splits: 0)
Lemmas : 155907 (Deleted: 136803)
Binary : 5710 (Ratio: 3.66%)
Ternary : 2018 (Ratio: 1.29%)
Conflict : 155907 (Average Length: 636.6 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 155907 (Average: 13.21 Max: 485 Sum: 2059462)
Executed : 155819 (Average: 13.20 Max: 485 Sum: 2058111 Ratio: 99.93%)
Bounded : 88 (Average: 15.35 Max: 57 Sum: 1351 Ratio: 0.07%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 351375 (Eliminated: 0 Frozen: 114851)
Constraints : 2609428 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 488MB
Max. Length : 75 steps
Models : 1
[endof: stats after solve call]
Solving Time: 8.49s
Memory: 453MB (+12MB)
UNKNOWN
Iteration Time: 9.24s
Iteration 22
Queue: [(4,20,2,True), (5,25,2,True), (6,30,2,True), (7,35,1,True), (8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
Grounded Until: 80
Blocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 23
Time : 115.885s (Solving: 106.07s 1st Model: 0.00s Unsat: 0.93s)
CPU Time : 115.852s
Choices : 2363026 (Domain: 2289185)
Conflicts : 163570 (Analyzed: 163567)
Restarts : 1832 (Average: 89.28 Last: 168)
Model-Level : 98.0
Problems : 23 (Average Length: 40.48 Splits: 0)
Lemmas : 163567 (Deleted: 143731)
Binary : 5814 (Ratio: 3.55%)
Ternary : 2039 (Ratio: 1.25%)
Conflict : 163567 (Average Length: 629.3 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 163567 (Average: 12.90 Max: 485 Sum: 2110449)
Executed : 163475 (Average: 12.89 Max: 485 Sum: 2109013 Ratio: 99.93%)
Bounded : 92 (Average: 15.61 Max: 82 Sum: 1436 Ratio: 0.07%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 351375 (Eliminated: 0 Frozen: 114851)
Constraints : 2609428 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 488MB
Max. Length : 80 steps
Models : 1
[endof: stats after solve call]
Solving Time: 4.40s
Memory: 455MB (+2MB)
UNKNOWN
Iteration Time: 4.44s
Iteration 23
Queue: [(5,25,2,True), (6,30,2,True), (7,35,1,True), (8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
Grounded Until: 80
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 24
Time : 121.833s (Solving: 111.91s 1st Model: 0.00s Unsat: 0.93s)
CPU Time : 121.804s
Choices : 2420387 (Domain: 2346538)
Conflicts : 172222 (Analyzed: 172219)
Restarts : 1932 (Average: 89.14 Last: 168)
Model-Level : 98.0
Problems : 24 (Average Length: 42.21 Splits: 0)
Lemmas : 172219 (Deleted: 152891)
Binary : 5885 (Ratio: 3.42%)
Ternary : 2062 (Ratio: 1.20%)
Conflict : 172219 (Average Length: 640.1 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 172219 (Average: 12.53 Max: 485 Sum: 2157317)
Executed : 172126 (Average: 12.52 Max: 485 Sum: 2155799 Ratio: 99.93%)
Bounded : 93 (Average: 16.32 Max: 82 Sum: 1518 Ratio: 0.07%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 351375 (Eliminated: 0 Frozen: 114851)
Constraints : 2609414 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 488MB
Max. Length : 80 steps
Models : 1
[endof: stats after solve call]
Solving Time: 5.91s
Memory: 455MB (+0MB)
UNKNOWN
Iteration Time: 5.95s
Iteration 24
Queue: [(6,30,2,True), (7,35,1,True), (8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
Grounded Until: 80
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 25
Time : 126.879s (Solving: 116.88s 1st Model: 0.00s Unsat: 0.93s)
CPU Time : 126.852s
Choices : 2486335 (Domain: 2411647)
Conflicts : 180365 (Analyzed: 180362)
Restarts : 2032 (Average: 88.76 Last: 168)
Model-Level : 98.0
Problems : 25 (Average Length: 43.80 Splits: 0)
Lemmas : 180362 (Deleted: 159111)
Binary : 5979 (Ratio: 3.31%)
Ternary : 2080 (Ratio: 1.15%)
Conflict : 180362 (Average Length: 645.8 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 180362 (Average: 12.25 Max: 485 Sum: 2208661)
Executed : 180269 (Average: 12.24 Max: 485 Sum: 2207143 Ratio: 99.93%)
Bounded : 93 (Average: 16.32 Max: 82 Sum: 1518 Ratio: 0.07%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 351375 (Eliminated: 0 Frozen: 114851)
Constraints : 2609400 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 488MB
Max. Length : 80 steps
Models : 1
[endof: stats after solve call]
Solving Time: 5.02s
Memory: 455MB (+0MB)
UNKNOWN
Iteration Time: 5.05s
Iteration 25
Queue: [(7,35,1,True), (8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
Grounded Until: 80
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 26
Time : 132.800s (Solving: 122.73s 1st Model: 0.00s Unsat: 0.93s)
CPU Time : 132.776s
Choices : 2564170 (Domain: 2489244)
Conflicts : 189148 (Analyzed: 189145)
Restarts : 2132 (Average: 88.72 Last: 168)
Model-Level : 98.0
Problems : 26 (Average Length: 45.27 Splits: 0)
Lemmas : 189145 (Deleted: 169096)
Binary : 6075 (Ratio: 3.21%)
Ternary : 2095 (Ratio: 1.11%)
Conflict : 189145 (Average Length: 653.4 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 189145 (Average: 12.01 Max: 485 Sum: 2270921)
Executed : 189052 (Average: 12.00 Max: 485 Sum: 2269403 Ratio: 99.93%)
Bounded : 93 (Average: 16.32 Max: 82 Sum: 1518 Ratio: 0.07%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 351375 (Eliminated: 0 Frozen: 114851)
Constraints : 2609400 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 488MB
Max. Length : 80 steps
Models : 1
[endof: stats after solve call]
Solving Time: 5.90s
Memory: 455MB (+0MB)
UNKNOWN
Iteration Time: 5.93s
Iteration 26
Queue: [(8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
Grounded Until: 80
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 27
Time : 139.089s (Solving: 128.94s 1st Model: 0.00s Unsat: 0.93s)
CPU Time : 139.056s
Choices : 2672210 (Domain: 2593751)
Conflicts : 198058 (Analyzed: 198055)
Restarts : 2232 (Average: 88.73 Last: 168)
Model-Level : 98.0
Problems : 27 (Average Length: 46.63 Splits: 0)
Lemmas : 198055 (Deleted: 177285)
Binary : 6370 (Ratio: 3.22%)
Ternary : 2135 (Ratio: 1.08%)
Conflict : 198055 (Average Length: 655.5 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 198055 (Average: 11.90 Max: 485 Sum: 2356814)
Executed : 197962 (Average: 11.89 Max: 485 Sum: 2355296 Ratio: 99.94%)
Bounded : 93 (Average: 16.32 Max: 82 Sum: 1518 Ratio: 0.06%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 351375 (Eliminated: 0 Frozen: 114851)
Constraints : 2609400 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 488MB
Max. Length : 80 steps
Models : 1
[endof: stats after solve call]
Solving Time: 6.25s
Memory: 455MB (+0MB)
UNKNOWN
Iteration Time: 6.28s
Iteration 27
Queue: [(9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
Grounded Until: 80
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 28
Time : 145.617s (Solving: 135.38s 1st Model: 0.00s Unsat: 0.93s)
CPU Time : 145.588s
Choices : 2760976 (Domain: 2682427)
Conflicts : 207181 (Analyzed: 207178)
Restarts : 2332 (Average: 88.84 Last: 168)
Model-Level : 98.0
Problems : 28 (Average Length: 47.89 Splits: 0)
Lemmas : 207178 (Deleted: 185904)
Binary : 6447 (Ratio: 3.11%)
Ternary : 2143 (Ratio: 1.03%)
Conflict : 207178 (Average Length: 660.0 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 207178 (Average: 11.72 Max: 485 Sum: 2427947)
Executed : 207085 (Average: 11.71 Max: 485 Sum: 2426429 Ratio: 99.94%)
Bounded : 93 (Average: 16.32 Max: 82 Sum: 1518 Ratio: 0.06%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 351375 (Eliminated: 0 Frozen: 114851)
Constraints : 2609400 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 488MB
Max. Length : 80 steps
Models : 1
[endof: stats after solve call]
Solving Time: 6.50s
Memory: 455MB (+0MB)
UNKNOWN
Iteration Time: 6.53s
Iteration 28
Queue: [(10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
Grounded Until: 80
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 29
Time : 152.470s (Solving: 142.16s 1st Model: 0.00s Unsat: 0.93s)
CPU Time : 152.444s
Choices : 2848061 (Domain: 2769480)
Conflicts : 215987 (Analyzed: 215984)
Restarts : 2432 (Average: 88.81 Last: 168)
Model-Level : 98.0
Problems : 29 (Average Length: 49.07 Splits: 0)
Lemmas : 215984 (Deleted: 194760)
Binary : 6534 (Ratio: 3.03%)
Ternary : 2156 (Ratio: 1.00%)
Conflict : 215984 (Average Length: 669.3 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 215984 (Average: 11.55 Max: 485 Sum: 2495002)
Executed : 215891 (Average: 11.54 Max: 485 Sum: 2493484 Ratio: 99.94%)
Bounded : 93 (Average: 16.32 Max: 82 Sum: 1518 Ratio: 0.06%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 351375 (Eliminated: 0 Frozen: 114851)
Constraints : 2609400 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 488MB
Max. Length : 80 steps
Models : 1
[endof: stats after solve call]
Solving Time: 6.83s
Memory: 455MB (+0MB)
UNKNOWN
Iteration Time: 6.86s
Iteration 29
Queue: [(11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
Grounded Until: 80
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 30
Time : 159.550s (Solving: 149.14s 1st Model: 0.00s Unsat: 0.93s)
CPU Time : 159.528s
Choices : 2942157 (Domain: 2863541)
Conflicts : 224571 (Analyzed: 224568)
Restarts : 2532 (Average: 88.69 Last: 168)
Model-Level : 98.0
Problems : 30 (Average Length: 50.17 Splits: 0)
Lemmas : 224568 (Deleted: 201840)
Binary : 6664 (Ratio: 2.97%)
Ternary : 2182 (Ratio: 0.97%)
Conflict : 224568 (Average Length: 689.6 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 224568 (Average: 11.43 Max: 485 Sum: 2566700)
Executed : 224475 (Average: 11.42 Max: 485 Sum: 2565182 Ratio: 99.94%)
Bounded : 93 (Average: 16.32 Max: 82 Sum: 1518 Ratio: 0.06%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 351375 (Eliminated: 0 Frozen: 114851)
Constraints : 2609400 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 488MB
Max. Length : 80 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.05s
Memory: 455MB (+0MB)
UNKNOWN
Iteration Time: 7.09s
Iteration 30
Queue: [(12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
Grounded Until: 80
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 31
Time : 164.639s (Solving: 154.14s 1st Model: 0.00s Unsat: 0.93s)
CPU Time : 164.620s
Choices : 3020414 (Domain: 2941740)
Conflicts : 232996 (Analyzed: 232993)
Restarts : 2632 (Average: 88.52 Last: 168)
Model-Level : 98.0
Problems : 31 (Average Length: 51.19 Splits: 0)
Lemmas : 232993 (Deleted: 209931)
Binary : 6707 (Ratio: 2.88%)
Ternary : 2189 (Ratio: 0.94%)
Conflict : 232993 (Average Length: 688.5 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 232993 (Average: 11.28 Max: 485 Sum: 2629041)
Executed : 232900 (Average: 11.28 Max: 485 Sum: 2627523 Ratio: 99.94%)
Bounded : 93 (Average: 16.32 Max: 82 Sum: 1518 Ratio: 0.06%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 351375 (Eliminated: 0 Frozen: 114851)
Constraints : 2609400 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 488MB
Max. Length : 80 steps
Models : 1
[endof: stats after solve call]
Solving Time: 5.06s
Memory: 455MB (+0MB)
UNKNOWN
Iteration Time: 5.09s
Iteration 31
Queue: [(13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
Grounded Until: 80
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 32
Time : 171.668s (Solving: 161.10s 1st Model: 0.00s Unsat: 0.93s)
CPU Time : 171.652s
Choices : 3112502 (Domain: 3033822)
Conflicts : 241725 (Analyzed: 241722)
Restarts : 2732 (Average: 88.48 Last: 168)
Model-Level : 98.0
Problems : 32 (Average Length: 52.16 Splits: 0)
Lemmas : 241722 (Deleted: 219897)
Binary : 6792 (Ratio: 2.81%)
Ternary : 2201 (Ratio: 0.91%)
Conflict : 241722 (Average Length: 700.2 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 241722 (Average: 11.16 Max: 485 Sum: 2697292)
Executed : 241629 (Average: 11.15 Max: 485 Sum: 2695774 Ratio: 99.94%)
Bounded : 93 (Average: 16.32 Max: 82 Sum: 1518 Ratio: 0.06%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 351375 (Eliminated: 0 Frozen: 114851)
Constraints : 2609400 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 488MB
Max. Length : 80 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.01s
Memory: 455MB (+0MB)
UNKNOWN
Iteration Time: 7.03s
Iteration 32
Queue: [(14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
Grounded Until: 80
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 33
Time : 178.388s (Solving: 167.75s 1st Model: 0.00s Unsat: 0.93s)
CPU Time : 178.376s
Choices : 3217082 (Domain: 3138145)
Conflicts : 250203 (Analyzed: 250200)
Restarts : 2832 (Average: 88.35 Last: 168)
Model-Level : 98.0
Problems : 33 (Average Length: 53.06 Splits: 0)
Lemmas : 250200 (Deleted: 226545)
Binary : 6878 (Ratio: 2.75%)
Ternary : 2217 (Ratio: 0.89%)
Conflict : 250200 (Average Length: 709.9 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 250200 (Average: 11.11 Max: 485 Sum: 2778890)
Executed : 250106 (Average: 11.10 Max: 485 Sum: 2777290 Ratio: 99.94%)
Bounded : 94 (Average: 17.02 Max: 82 Sum: 1600 Ratio: 0.06%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 351375 (Eliminated: 0 Frozen: 114851)
Constraints : 2609400 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 488MB
Max. Length : 80 steps
Models : 1
[endof: stats after solve call]
Solving Time: 6.70s
Memory: 455MB (+0MB)
UNKNOWN
Iteration Time: 6.72s
Iteration 33
Queue: [(15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
Grounded Until: 80
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 34
Time : 185.905s (Solving: 175.19s 1st Model: 0.00s Unsat: 0.93s)
CPU Time : 185.896s
Choices : 3314669 (Domain: 3235496)
Conflicts : 258535 (Analyzed: 258532)
Restarts : 2932 (Average: 88.18 Last: 168)
Model-Level : 98.0
Problems : 34 (Average Length: 53.91 Splits: 0)
Lemmas : 258532 (Deleted: 235253)
Binary : 7003 (Ratio: 2.71%)
Ternary : 2236 (Ratio: 0.86%)
Conflict : 258532 (Average Length: 737.8 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 258532 (Average: 11.03 Max: 504 Sum: 2850733)
Executed : 258438 (Average: 11.02 Max: 504 Sum: 2849133 Ratio: 99.94%)
Bounded : 94 (Average: 17.02 Max: 82 Sum: 1600 Ratio: 0.06%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 351375 (Eliminated: 0 Frozen: 114851)
Constraints : 2609386 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 488MB
Max. Length : 80 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.49s
Memory: 455MB (+0MB)
UNKNOWN
Iteration Time: 7.52s
Iteration 34
Queue: [(16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
Grounded Until: 80
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 35
Time : 193.223s (Solving: 182.43s 1st Model: 0.00s Unsat: 0.93s)
CPU Time : 193.216s
Choices : 3418438 (Domain: 3339243)
Conflicts : 267487 (Analyzed: 267484)
Restarts : 3032 (Average: 88.22 Last: 168)
Model-Level : 98.0
Problems : 35 (Average Length: 54.71 Splits: 0)
Lemmas : 267484 (Deleted: 244668)
Binary : 7055 (Ratio: 2.64%)
Ternary : 2243 (Ratio: 0.84%)
Conflict : 267484 (Average Length: 743.3 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 267484 (Average: 10.95 Max: 504 Sum: 2929334)
Executed : 267390 (Average: 10.95 Max: 504 Sum: 2927734 Ratio: 99.95%)
Bounded : 94 (Average: 17.02 Max: 82 Sum: 1600 Ratio: 0.05%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 351375 (Eliminated: 0 Frozen: 114851)
Constraints : 2609386 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 488MB
Max. Length : 80 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.29s
Memory: 455MB (+0MB)
UNKNOWN
Iteration Time: 7.32s
Iteration 35
Queue: [(17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
Grounded Until: 80
Expected Memory: 492.0MB
Grounding... [('step', [81]), ('step', [82]), ('step', [83]), ('step', [84]), ('step', [85]), ('check', [85])]
Grounding Time: 0.34s
Memory: 455MB (+0MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 36
Time : 200.223s (Solving: 188.75s 1st Model: 0.00s Unsat: 0.93s)
CPU Time : 200.216s
Choices : 3512014 (Domain: 3432739)
Conflicts : 276011 (Analyzed: 276008)
Restarts : 3132 (Average: 88.13 Last: 168)
Model-Level : 98.0
Problems : 36 (Average Length: 55.61 Splits: 0)
Lemmas : 276008 (Deleted: 251663)
Binary : 7146 (Ratio: 2.59%)
Ternary : 2250 (Ratio: 0.82%)
Conflict : 276008 (Average Length: 744.5 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 276008 (Average: 10.86 Max: 554 Sum: 2998154)
Executed : 275914 (Average: 10.86 Max: 554 Sum: 2996554 Ratio: 99.95%)
Bounded : 94 (Average: 17.02 Max: 82 Sum: 1600 Ratio: 0.05%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 373951 (Eliminated: 0 Frozen: 122316)
Constraints : 2782431 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 505MB
Max. Length : 80 steps
Models : 1
[endof: stats after solve call]
Solving Time: 6.40s
Memory: 466MB (+11MB)
UNKNOWN
Iteration Time: 7.01s
Iteration 36
Queue: [(18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
Grounded Until: 85
Expected Memory: 503.0MB
Grounding... [('step', [86]), ('step', [87]), ('step', [88]), ('step', [89]), ('step', [90]), ('check', [90])]
Grounding Time: 0.32s
Memory: 466MB (+0MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 37
Time : 208.215s (Solving: 196.08s 1st Model: 0.00s Unsat: 0.93s)
CPU Time : 208.212s
Choices : 3621553 (Domain: 3541733)
Conflicts : 284583 (Analyzed: 284580)
Restarts : 3232 (Average: 88.05 Last: 191)
Model-Level : 98.0
Problems : 37 (Average Length: 56.59 Splits: 0)
Lemmas : 284580 (Deleted: 260087)
Binary : 7220 (Ratio: 2.54%)
Ternary : 2263 (Ratio: 0.80%)
Conflict : 284580 (Average Length: 751.3 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 284580 (Average: 10.82 Max: 554 Sum: 3080470)
Executed : 284486 (Average: 10.82 Max: 554 Sum: 3078870 Ratio: 99.95%)
Bounded : 94 (Average: 17.02 Max: 82 Sum: 1600 Ratio: 0.05%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 396527 (Eliminated: 0 Frozen: 129781)
Constraints : 2955476 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 523MB
Max. Length : 85 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.41s
Memory: 481MB (+15MB)
UNKNOWN
Iteration Time: 8.01s
Iteration 37
Queue: [(19,95,0,True), (20,100,0,True), (21,105,0,True)]
Grounded Until: 90
Expected Memory: 518.0MB
Grounding... [('step', [91]), ('step', [92]), ('step', [93]), ('step', [94]), ('step', [95]), ('check', [95])]
Grounding Time: 0.33s
Memory: 482MB (+1MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 38
Time : 215.966s (Solving: 203.12s 1st Model: 0.00s Unsat: 0.93s)
CPU Time : 215.968s
Choices : 3712527 (Domain: 3632707)
Conflicts : 293083 (Analyzed: 293080)
Restarts : 3332 (Average: 87.96 Last: 191)
Model-Level : 98.0
Problems : 38 (Average Length: 57.66 Splits: 0)
Lemmas : 293080 (Deleted: 268443)
Binary : 7267 (Ratio: 2.48%)
Ternary : 2273 (Ratio: 0.78%)
Conflict : 293080 (Average Length: 753.2 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 293080 (Average: 10.73 Max: 554 Sum: 3144070)
Executed : 292986 (Average: 10.72 Max: 554 Sum: 3142470 Ratio: 99.95%)
Bounded : 94 (Average: 17.02 Max: 82 Sum: 1600 Ratio: 0.05%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 419103 (Eliminated: 0 Frozen: 137246)
Constraints : 3128521 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 542MB
Max. Length : 90 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.13s
Memory: 531MB (+49MB)
UNKNOWN
Iteration Time: 7.76s
Iteration 38
Queue: [(20,100,0,True), (21,105,0,True)]
Grounded Until: 95
Expected Memory: 581.0MB
Grounding... [('step', [96]), ('step', [97]), ('step', [98]), ('step', [99]), ('step', [100]), ('check', [100])]
Grounding Time: 0.32s
Memory: 531MB (+0MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 39
Time : 223.254s (Solving: 209.73s 1st Model: 0.00s Unsat: 0.93s)
CPU Time : 223.256s
Choices : 3809181 (Domain: 3729345)
Conflicts : 301909 (Analyzed: 301906)
Restarts : 3432 (Average: 87.97 Last: 191)
Model-Level : 98.0
Problems : 39 (Average Length: 58.79 Splits: 0)
Lemmas : 301906 (Deleted: 278408)
Binary : 7308 (Ratio: 2.42%)
Ternary : 2282 (Ratio: 0.76%)
Conflict : 301906 (Average Length: 756.3 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 301906 (Average: 10.65 Max: 598 Sum: 3214321)
Executed : 301812 (Average: 10.64 Max: 598 Sum: 3212721 Ratio: 99.95%)
Bounded : 94 (Average: 17.02 Max: 82 Sum: 1600 Ratio: 0.05%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 441679 (Eliminated: 0 Frozen: 144711)
Constraints : 3301566 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 585MB
Max. Length : 95 steps
Models : 1
[endof: stats after solve call]
Solving Time: 6.69s
Memory: 534MB (+3MB)
UNKNOWN
Iteration Time: 7.30s
Iteration 39
Queue: [(21,105,0,True)]
Grounded Until: 100
Expected Memory: 584.0MB
Grounding... [('step', [101]), ('step', [102]), ('step', [103]), ('step', [104]), ('step', [105]), ('check', [105])]
Grounding Time: 0.36s
Memory: 534MB (+0MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 40
Time : 231.320s (Solving: 217.04s 1st Model: 0.00s Unsat: 0.93s)
CPU Time : 231.324s
Choices : 3904487 (Domain: 3824650)
Conflicts : 310719 (Analyzed: 310716)
Restarts : 3532 (Average: 87.97 Last: 191)
Model-Level : 98.0
Problems : 40 (Average Length: 60.00 Splits: 0)
Lemmas : 310716 (Deleted: 287047)
Binary : 7355 (Ratio: 2.37%)
Ternary : 2302 (Ratio: 0.74%)
Conflict : 310716 (Average Length: 758.3 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 310716 (Average: 10.56 Max: 598 Sum: 3280415)
Executed : 310622 (Average: 10.55 Max: 598 Sum: 3278815 Ratio: 99.95%)
Bounded : 94 (Average: 17.02 Max: 82 Sum: 1600 Ratio: 0.05%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 464255 (Eliminated: 0 Frozen: 152176)
Constraints : 3474611 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 595MB
Max. Length : 100 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.40s
Memory: 543MB (+9MB)
UNKNOWN
Iteration Time: 8.08s
Iteration 40
Queue: [(4,20,3,True), (5,25,3,True), (6,30,3,True), (7,35,2,True), (8,40,2,True), (9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)]
Grounded Until: 105
Blocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 41
Time : 234.426s (Solving: 220.04s 1st Model: 0.00s Unsat: 0.93s)
CPU Time : 234.432s
Choices : 3935457 (Domain: 3855620)
Conflicts : 318065 (Analyzed: 318062)
Restarts : 3632 (Average: 87.57 Last: 191)
Model-Level : 98.0
Problems : 41 (Average Length: 61.15 Splits: 0)
Lemmas : 318062 (Deleted: 293511)
Binary : 7422 (Ratio: 2.33%)
Ternary : 2318 (Ratio: 0.73%)
Conflict : 318062 (Average Length: 752.7 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 318062 (Average: 10.39 Max: 598 Sum: 3305523)
Executed : 317967 (Average: 10.39 Max: 598 Sum: 3303816 Ratio: 99.95%)
Bounded : 95 (Average: 17.97 Max: 107 Sum: 1707 Ratio: 0.05%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 464255 (Eliminated: 0 Frozen: 152176)
Constraints : 3474611 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 595MB
Max. Length : 105 steps
Models : 1
[endof: stats after solve call]
Solving Time: 3.07s
Memory: 543MB (+0MB)
UNKNOWN
Iteration Time: 3.11s
Iteration 41
Queue: [(5,25,3,True), (6,30,3,True), (7,35,2,True), (8,40,2,True), (9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)]
Grounded Until: 105
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 42
Time : 240.594s (Solving: 226.07s 1st Model: 0.00s Unsat: 0.93s)
CPU Time : 240.604s
Choices : 3984447 (Domain: 3904610)
Conflicts : 326115 (Analyzed: 326112)
Restarts : 3732 (Average: 87.38 Last: 191)
Model-Level : 98.0
Problems : 42 (Average Length: 62.24 Splits: 0)
Lemmas : 326112 (Deleted: 300852)
Binary : 7461 (Ratio: 2.29%)
Ternary : 2328 (Ratio: 0.71%)
Conflict : 326112 (Average Length: 766.9 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 326112 (Average: 10.25 Max: 598 Sum: 3343660)
Executed : 326016 (Average: 10.25 Max: 598 Sum: 3341850 Ratio: 99.95%)
Bounded : 96 (Average: 18.85 Max: 107 Sum: 1810 Ratio: 0.05%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 464255 (Eliminated: 0 Frozen: 152176)
Constraints : 3474597 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 671MB
Max. Length : 105 steps
Models : 1
[endof: stats after solve call]
Solving Time: 6.12s
Memory: 607MB (+64MB)
UNKNOWN
Iteration Time: 6.17s
Iteration 42
Queue: [(6,30,3,True), (7,35,2,True), (8,40,2,True), (9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)]
Grounded Until: 105
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 43
Time : 246.964s (Solving: 232.34s 1st Model: 0.00s Unsat: 0.93s)
CPU Time : 246.976s
Choices : 4051552 (Domain: 3971715)
Conflicts : 334403 (Analyzed: 334400)
Restarts : 3832 (Average: 87.27 Last: 191)
Model-Level : 98.0
Problems : 43 (Average Length: 63.28 Splits: 0)
Lemmas : 334400 (Deleted: 309484)
Binary : 7571 (Ratio: 2.26%)
Ternary : 2342 (Ratio: 0.70%)
Conflict : 334400 (Average Length: 781.3 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 334400 (Average: 10.14 Max: 598 Sum: 3390993)
Executed : 334304 (Average: 10.14 Max: 598 Sum: 3389183 Ratio: 99.95%)
Bounded : 96 (Average: 18.85 Max: 107 Sum: 1810 Ratio: 0.05%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 464255 (Eliminated: 0 Frozen: 152176)
Constraints : 3474597 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 671MB
Max. Length : 105 steps
Models : 1
[endof: stats after solve call]
Solving Time: 6.34s
Memory: 607MB (+0MB)
UNKNOWN
Iteration Time: 6.38s
Iteration 43
Queue: [(7,35,2,True), (8,40,2,True), (9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)]
Grounded Until: 105
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 44
Time : 253.337s (Solving: 238.62s 1st Model: 0.00s Unsat: 0.93s)
CPU Time : 253.352s
Choices : 4132781 (Domain: 4049838)
Conflicts : 343332 (Analyzed: 343329)
Restarts : 3932 (Average: 87.32 Last: 191)
Model-Level : 98.0
Problems : 44 (Average Length: 64.27 Splits: 0)
Lemmas : 343329 (Deleted: 318183)
Binary : 7831 (Ratio: 2.28%)
Ternary : 2358 (Ratio: 0.69%)
Conflict : 343329 (Average Length: 783.0 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 343329 (Average: 10.04 Max: 598 Sum: 3447205)
Executed : 343233 (Average: 10.04 Max: 598 Sum: 3445395 Ratio: 99.95%)
Bounded : 96 (Average: 18.85 Max: 107 Sum: 1810 Ratio: 0.05%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 464255 (Eliminated: 0 Frozen: 152176)
Constraints : 3474597 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 671MB
Max. Length : 105 steps
Models : 1
[endof: stats after solve call]
Solving Time: 6.34s
Memory: 607MB (+0MB)
UNKNOWN
Iteration Time: 6.38s
Iteration 44
Queue: [(8,40,2,True), (9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)]
Grounded Until: 105
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 45
Time : 259.329s (Solving: 244.50s 1st Model: 0.00s Unsat: 0.93s)
CPU Time : 259.348s
Choices : 4204373 (Domain: 4121381)
Conflicts : 351629 (Analyzed: 351626)
Restarts : 4032 (Average: 87.21 Last: 191)
Model-Level : 98.0
Problems : 45 (Average Length: 65.22 Splits: 0)
Lemmas : 351626 (Deleted: 324850)
Binary : 7889 (Ratio: 2.24%)
Ternary : 2361 (Ratio: 0.67%)
Conflict : 351626 (Average Length: 786.5 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 351626 (Average: 9.96 Max: 598 Sum: 3501222)
Executed : 351530 (Average: 9.95 Max: 598 Sum: 3499412 Ratio: 99.95%)
Bounded : 96 (Average: 18.85 Max: 107 Sum: 1810 Ratio: 0.05%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 464255 (Eliminated: 0 Frozen: 152176)
Constraints : 3474597 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 671MB
Max. Length : 105 steps
Models : 1
[endof: stats after solve call]
Solving Time: 5.95s
Memory: 607MB (+0MB)
UNKNOWN
Iteration Time: 6.00s
Iteration 45
Queue: [(9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)]
Grounded Until: 105
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 46
Time : 265.584s (Solving: 250.64s 1st Model: 0.00s Unsat: 0.93s)
CPU Time : 265.608s
Choices : 4276343 (Domain: 4193282)
Conflicts : 360234 (Analyzed: 360231)
Restarts : 4132 (Average: 87.18 Last: 191)
Model-Level : 98.0
Problems : 46 (Average Length: 66.13 Splits: 0)
Lemmas : 360231 (Deleted: 333143)
Binary : 7929 (Ratio: 2.20%)
Ternary : 2365 (Ratio: 0.66%)
Conflict : 360231 (Average Length: 790.0 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 360231 (Average: 9.87 Max: 598 Sum: 3555815)
Executed : 360135 (Average: 9.87 Max: 598 Sum: 3554005 Ratio: 99.95%)
Bounded : 96 (Average: 18.85 Max: 107 Sum: 1810 Ratio: 0.05%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 464255 (Eliminated: 0 Frozen: 152176)
Constraints : 3474597 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 671MB
Max. Length : 105 steps
Models : 1
[endof: stats after solve call]
Solving Time: 6.21s
Memory: 607MB (+0MB)
UNKNOWN
Iteration Time: 6.26s
Iteration 46
Queue: [(10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)]
Grounded Until: 105
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 47
Time : 272.856s (Solving: 257.81s 1st Model: 0.00s Unsat: 0.93s)
CPU Time : 272.880s
Choices : 4372979 (Domain: 4288505)
Conflicts : 369523 (Analyzed: 369520)
Restarts : 4232 (Average: 87.32 Last: 191)
Model-Level : 98.0
Problems : 47 (Average Length: 67.00 Splits: 0)
Lemmas : 369520 (Deleted: 343266)
Binary : 8100 (Ratio: 2.19%)
Ternary : 2384 (Ratio: 0.65%)
Conflict : 369520 (Average Length: 796.9 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 369520 (Average: 9.81 Max: 598 Sum: 3624440)
Executed : 369424 (Average: 9.80 Max: 598 Sum: 3622630 Ratio: 99.95%)
Bounded : 96 (Average: 18.85 Max: 107 Sum: 1810 Ratio: 0.05%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 464255 (Eliminated: 0 Frozen: 152176)
Constraints : 3474597 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 671MB
Max. Length : 105 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.24s
Memory: 607MB (+0MB)
UNKNOWN
Iteration Time: 7.28s
Iteration 47
Queue: [(11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)]
Grounded Until: 105
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 48
Time : 279.412s (Solving: 264.24s 1st Model: 0.00s Unsat: 0.93s)
CPU Time : 279.436s
Choices : 4475817 (Domain: 4390668)
Conflicts : 378272 (Analyzed: 378269)
Restarts : 4332 (Average: 87.32 Last: 193)
Model-Level : 98.0
Problems : 48 (Average Length: 67.83 Splits: 0)
Lemmas : 378269 (Deleted: 352334)
Binary : 8194 (Ratio: 2.17%)
Ternary : 2399 (Ratio: 0.63%)
Conflict : 378269 (Average Length: 799.1 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 378269 (Average: 9.78 Max: 598 Sum: 3700656)
Executed : 378173 (Average: 9.78 Max: 598 Sum: 3698846 Ratio: 99.95%)
Bounded : 96 (Average: 18.85 Max: 107 Sum: 1810 Ratio: 0.05%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 464255 (Eliminated: 0 Frozen: 152176)
Constraints : 3474597 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 671MB
Max. Length : 105 steps
Models : 1
[endof: stats after solve call]
Solving Time: 6.51s
Memory: 607MB (+0MB)
UNKNOWN
Iteration Time: 6.56s
Iteration 48
Queue: [(12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)]
Grounded Until: 105
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 49
Time : 286.604s (Solving: 271.31s 1st Model: 0.00s Unsat: 0.93s)
CPU Time : 286.632s
Choices : 4567595 (Domain: 4482422)
Conflicts : 387396 (Analyzed: 387393)
Restarts : 4432 (Average: 87.41 Last: 193)
Model-Level : 98.0
Problems : 49 (Average Length: 68.63 Splits: 0)
Lemmas : 387393 (Deleted: 360788)
Binary : 8238 (Ratio: 2.13%)
Ternary : 2411 (Ratio: 0.62%)
Conflict : 387393 (Average Length: 801.9 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 387393 (Average: 9.73 Max: 598 Sum: 3770248)
Executed : 387297 (Average: 9.73 Max: 598 Sum: 3768438 Ratio: 99.95%)
Bounded : 96 (Average: 18.85 Max: 107 Sum: 1810 Ratio: 0.05%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 464255 (Eliminated: 0 Frozen: 152176)
Constraints : 3474597 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 671MB
Max. Length : 105 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.15s
Memory: 607MB (+0MB)
UNKNOWN
Iteration Time: 7.20s
Iteration 49
Queue: [(13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)]
Grounded Until: 105
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 50
Time : 293.569s (Solving: 278.16s 1st Model: 0.00s Unsat: 0.93s)
CPU Time : 293.600s
Choices : 4652365 (Domain: 4567061)
Conflicts : 396218 (Analyzed: 396215)
Restarts : 4532 (Average: 87.43 Last: 193)
Model-Level : 98.0
Problems : 50 (Average Length: 69.40 Splits: 0)
Lemmas : 396215 (Deleted: 369777)
Binary : 8283 (Ratio: 2.09%)
Ternary : 2416 (Ratio: 0.61%)
Conflict : 396215 (Average Length: 805.5 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 396215 (Average: 9.67 Max: 598 Sum: 3831002)
Executed : 396119 (Average: 9.66 Max: 598 Sum: 3829192 Ratio: 99.95%)
Bounded : 96 (Average: 18.85 Max: 107 Sum: 1810 Ratio: 0.05%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 464255 (Eliminated: 0 Frozen: 152176)
Constraints : 3474597 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 671MB
Max. Length : 105 steps
Models : 1
[endof: stats after solve call]
Solving Time: 6.92s
Memory: 607MB (+0MB)
UNKNOWN
Iteration Time: 6.97s
Iteration 50
Queue: [(17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)]
Grounded Until: 105
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 51
Time : 301.116s (Solving: 285.61s 1st Model: 0.00s Unsat: 0.93s)
CPU Time : 301.152s
Choices : 4787055 (Domain: 4701341)
Conflicts : 404603 (Analyzed: 404600)
Restarts : 4632 (Average: 87.35 Last: 193)
Model-Level : 98.0
Problems : 51 (Average Length: 70.14 Splits: 0)
Lemmas : 404600 (Deleted: 376122)
Binary : 8442 (Ratio: 2.09%)
Ternary : 2449 (Ratio: 0.61%)
Conflict : 404600 (Average Length: 816.7 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 404600 (Average: 9.70 Max: 598 Sum: 3925303)
Executed : 404504 (Average: 9.70 Max: 598 Sum: 3923493 Ratio: 99.95%)
Bounded : 96 (Average: 18.85 Max: 107 Sum: 1810 Ratio: 0.05%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 464255 (Eliminated: 0 Frozen: 152176)
Constraints : 3474597 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 671MB
Max. Length : 105 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.52s
Memory: 607MB (+0MB)
UNKNOWN
Iteration Time: 7.55s
Iteration 51
Queue: [(18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)]
Grounded Until: 105
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 52
Time : 308.935s (Solving: 293.33s 1st Model: 0.00s Unsat: 0.93s)
CPU Time : 308.976s
Choices : 4887987 (Domain: 4802232)
Conflicts : 413541 (Analyzed: 413538)
Restarts : 4732 (Average: 87.39 Last: 193)
Model-Level : 98.0
Problems : 52 (Average Length: 70.85 Splits: 0)
Lemmas : 413538 (Deleted: 386431)
Binary : 8488 (Ratio: 2.05%)
Ternary : 2456 (Ratio: 0.59%)
Conflict : 413538 (Average Length: 817.5 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 413538 (Average: 9.67 Max: 598 Sum: 3998917)
Executed : 413442 (Average: 9.67 Max: 598 Sum: 3997107 Ratio: 99.95%)
Bounded : 96 (Average: 18.85 Max: 107 Sum: 1810 Ratio: 0.05%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 464255 (Eliminated: 0 Frozen: 152176)
Constraints : 3474597 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 671MB
Max. Length : 105 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.79s
Memory: 607MB (+0MB)
UNKNOWN
Iteration Time: 7.82s
Iteration 52
Queue: [(19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)]
Grounded Until: 105
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 53
Time : 316.753s (Solving: 301.03s 1st Model: 0.00s Unsat: 0.93s)
CPU Time : 316.800s
Choices : 4983188 (Domain: 4897391)
Conflicts : 422335 (Analyzed: 422332)
Restarts : 4832 (Average: 87.40 Last: 193)
Model-Level : 98.0
Problems : 53 (Average Length: 71.53 Splits: 0)
Lemmas : 422332 (Deleted: 395155)
Binary : 8566 (Ratio: 2.03%)
Ternary : 2462 (Ratio: 0.58%)
Conflict : 422332 (Average Length: 823.0 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 422332 (Average: 9.62 Max: 598 Sum: 4062213)
Executed : 422236 (Average: 9.61 Max: 598 Sum: 4060403 Ratio: 99.96%)
Bounded : 96 (Average: 18.85 Max: 107 Sum: 1810 Ratio: 0.04%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 464255 (Eliminated: 0 Frozen: 152176)
Constraints : 3474597 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 671MB
Max. Length : 105 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.78s
Memory: 607MB (+0MB)
UNKNOWN
Iteration Time: 7.82s
Iteration 53
Queue: [(20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)]
Grounded Until: 105
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 54
Time : 324.207s (Solving: 308.36s 1st Model: 0.00s Unsat: 0.93s)
CPU Time : 324.256s
Choices : 5085311 (Domain: 4999482)
Conflicts : 431030 (Analyzed: 431027)
Restarts : 4932 (Average: 87.39 Last: 193)
Model-Level : 98.0
Problems : 54 (Average Length: 72.19 Splits: 0)
Lemmas : 431027 (Deleted: 403776)
Binary : 8606 (Ratio: 2.00%)
Ternary : 2474 (Ratio: 0.57%)
Conflict : 431027 (Average Length: 823.4 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 431027 (Average: 9.59 Max: 598 Sum: 4135203)
Executed : 430931 (Average: 9.59 Max: 598 Sum: 4133393 Ratio: 99.96%)
Bounded : 96 (Average: 18.85 Max: 107 Sum: 1810 Ratio: 0.04%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 464255 (Eliminated: 0 Frozen: 152176)
Constraints : 3474597 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 671MB
Max. Length : 105 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.41s
Memory: 607MB (+0MB)
UNKNOWN
Iteration Time: 7.46s
Iteration 54
Queue: [(21,105,1,True), (22,110,0,True), (23,115,0,True)]
Grounded Until: 105
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 55
Time : 331.947s (Solving: 315.99s 1st Model: 0.00s Unsat: 0.93s)
CPU Time : 332.000s
Choices : 5237207 (Domain: 5150928)
Conflicts : 439413 (Analyzed: 439410)
Restarts : 5032 (Average: 87.32 Last: 193)
Model-Level : 98.0
Problems : 55 (Average Length: 72.82 Splits: 0)
Lemmas : 439410 (Deleted: 410132)
Binary : 8724 (Ratio: 1.99%)
Ternary : 2484 (Ratio: 0.57%)
Conflict : 439410 (Average Length: 830.0 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 439410 (Average: 9.65 Max: 598 Sum: 4241376)
Executed : 439314 (Average: 9.65 Max: 598 Sum: 4239566 Ratio: 99.96%)
Bounded : 96 (Average: 18.85 Max: 107 Sum: 1810 Ratio: 0.04%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 464255 (Eliminated: 0 Frozen: 152176)
Constraints : 3474597 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 671MB
Max. Length : 105 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.70s
Memory: 607MB (+0MB)
UNKNOWN
Iteration Time: 7.74s
Iteration 55
Queue: [(22,110,0,True), (23,115,0,True)]
Grounded Until: 105
Expected Memory: 657.0MB
Grounding... [('step', [106]), ('step', [107]), ('step', [108]), ('step', [109]), ('step', [110]), ('check', [110])]
Grounding Time: 0.32s
Memory: 607MB (+0MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 56
Time : 339.716s (Solving: 323.03s 1st Model: 0.00s Unsat: 0.93s)
CPU Time : 339.772s
Choices : 5336101 (Domain: 5249800)
Conflicts : 448387 (Analyzed: 448384)
Restarts : 5132 (Average: 87.37 Last: 193)
Model-Level : 98.0
Problems : 56 (Average Length: 73.52 Splits: 0)
Lemmas : 448384 (Deleted: 420553)
Binary : 8751 (Ratio: 1.95%)
Ternary : 2488 (Ratio: 0.55%)
Conflict : 448384 (Average Length: 827.9 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 448384 (Average: 9.62 Max: 598 Sum: 4312946)
Executed : 448287 (Average: 9.61 Max: 598 Sum: 4311024 Ratio: 99.96%)
Bounded : 97 (Average: 19.81 Max: 112 Sum: 1922 Ratio: 0.04%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 486831 (Eliminated: 0 Frozen: 159641)
Constraints : 3647642 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 673MB
Max. Length : 105 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.14s
Memory: 622MB (+15MB)
UNKNOWN
Iteration Time: 7.78s
Iteration 56
Queue: [(23,115,0,True)]
Grounded Until: 110
Expected Memory: 672.0MB
Grounding... [('step', [111]), ('step', [112]), ('step', [113]), ('step', [114]), ('step', [115]), ('check', [115])]
Grounding Time: 0.35s
Memory: 622MB (+0MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 57
Time : 348.381s (Solving: 330.92s 1st Model: 0.00s Unsat: 0.93s)
CPU Time : 348.432s
Choices : 5522900 (Domain: 5436158)
Conflicts : 457541 (Analyzed: 457538)
Restarts : 5232 (Average: 87.45 Last: 193)
Model-Level : 98.0
Problems : 57 (Average Length: 74.28 Splits: 0)
Lemmas : 457538 (Deleted: 429307)
Binary : 8895 (Ratio: 1.94%)
Ternary : 2518 (Ratio: 0.55%)
Conflict : 457538 (Average Length: 827.3 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 457538 (Average: 9.75 Max: 598 Sum: 4458992)
Executed : 457441 (Average: 9.74 Max: 598 Sum: 4457070 Ratio: 99.96%)
Bounded : 97 (Average: 19.81 Max: 112 Sum: 1922 Ratio: 0.04%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 509407 (Eliminated: 0 Frozen: 167106)
Constraints : 3820673 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 693MB
Max. Length : 110 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.99s
Memory: 637MB (+15MB)
UNKNOWN
Iteration Time: 8.67s
Iteration 57
Queue: [(4,20,4,True), (5,25,4,True), (6,30,4,True), (7,35,3,True), (8,40,3,True), (9,45,3,True), (10,50,3,True), (11,55,3,False), (12,60,3,False), (13,65,3,False), (14,70,2,True), (15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,1,True), (23,115,1,True)]
Grounded Until: 115
Blocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 58
Time : 352.466s (Solving: 334.87s 1st Model: 0.00s Unsat: 0.93s)
CPU Time : 352.520s
Choices : 5571904 (Domain: 5485162)
Conflicts : 465354 (Analyzed: 465351)
Restarts : 5332 (Average: 87.28 Last: 193)
Model-Level : 98.0
Problems : 58 (Average Length: 75.02 Splits: 0)
Lemmas : 465351 (Deleted: 435940)
Binary : 8948 (Ratio: 1.92%)
Ternary : 2536 (Ratio: 0.54%)
Conflict : 465351 (Average Length: 820.4 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 465351 (Average: 9.68 Max: 598 Sum: 4503233)
Executed : 465253 (Average: 9.67 Max: 598 Sum: 4501310 Ratio: 99.96%)
Bounded : 98 (Average: 19.62 Max: 112 Sum: 1923 Ratio: 0.04%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 509407 (Eliminated: 0 Frozen: 167106)
Constraints : 3820673 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 693MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 4.04s
Memory: 637MB (+0MB)
UNKNOWN
Iteration Time: 4.09s
Iteration 58
Queue: [(5,25,4,True), (6,30,4,True), (7,35,3,True), (8,40,3,True), (9,45,3,True), (10,50,3,True), (11,55,3,False), (12,60,3,False), (13,65,3,False), (14,70,2,True), (15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,1,True), (23,115,1,True)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 59
Time : 360.352s (Solving: 342.62s 1st Model: 0.00s Unsat: 0.93s)
CPU Time : 360.408s
Choices : 5639845 (Domain: 5553103)
Conflicts : 474162 (Analyzed: 474159)
Restarts : 5432 (Average: 87.29 Last: 193)
Model-Level : 98.0
Problems : 59 (Average Length: 75.73 Splits: 0)
Lemmas : 474159 (Deleted: 445590)
Binary : 8991 (Ratio: 1.90%)
Ternary : 2543 (Ratio: 0.54%)
Conflict : 474159 (Average Length: 835.4 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 474159 (Average: 9.61 Max: 598 Sum: 4557642)
Executed : 474061 (Average: 9.61 Max: 598 Sum: 4555719 Ratio: 99.96%)
Bounded : 98 (Average: 19.62 Max: 112 Sum: 1923 Ratio: 0.04%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 509407 (Eliminated: 0 Frozen: 167106)
Constraints : 3820673 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 693MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.84s
Memory: 637MB (+0MB)
UNKNOWN
Iteration Time: 7.89s
Iteration 59
Queue: [(6,30,4,True), (7,35,3,True), (8,40,3,True), (9,45,3,True), (10,50,3,True), (11,55,3,False), (12,60,3,False), (13,65,3,False), (14,70,2,True), (15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,1,True), (23,115,1,True)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 60
Time : 366.570s (Solving: 348.73s 1st Model: 0.00s Unsat: 0.93s)
CPU Time : 366.628s
Choices : 5700652 (Domain: 5613910)
Conflicts : 482448 (Analyzed: 482445)
Restarts : 5532 (Average: 87.21 Last: 193)
Model-Level : 98.0
Problems : 60 (Average Length: 76.42 Splits: 0)
Lemmas : 482445 (Deleted: 452222)
Binary : 9033 (Ratio: 1.87%)
Ternary : 2545 (Ratio: 0.53%)
Conflict : 482445 (Average Length: 843.0 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 482445 (Average: 9.53 Max: 598 Sum: 4599574)
Executed : 482347 (Average: 9.53 Max: 598 Sum: 4597651 Ratio: 99.96%)
Bounded : 98 (Average: 19.62 Max: 112 Sum: 1923 Ratio: 0.04%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 509407 (Eliminated: 0 Frozen: 167106)
Constraints : 3820673 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 693MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 6.18s
Memory: 637MB (+0MB)
UNKNOWN
Iteration Time: 6.22s
Iteration 60
Queue: [(7,35,3,True), (8,40,3,True), (9,45,3,True), (10,50,3,True), (11,55,3,False), (12,60,3,False), (13,65,3,False), (14,70,2,True), (15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,1,True), (23,115,1,True)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 61
Time : 372.863s (Solving: 354.90s 1st Model: 0.00s Unsat: 0.93s)
CPU Time : 372.924s
Choices : 5769640 (Domain: 5682834)
Conflicts : 491628 (Analyzed: 491625)
Restarts : 5632 (Average: 87.29 Last: 193)
Model-Level : 98.0
Problems : 61 (Average Length: 77.08 Splits: 0)
Lemmas : 491625 (Deleted: 462495)
Binary : 9051 (Ratio: 1.84%)
Ternary : 2552 (Ratio: 0.52%)
Conflict : 491625 (Average Length: 844.3 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 491625 (Average: 9.46 Max: 598 Sum: 4651795)
Executed : 491527 (Average: 9.46 Max: 598 Sum: 4649872 Ratio: 99.96%)
Bounded : 98 (Average: 19.62 Max: 112 Sum: 1923 Ratio: 0.04%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 509407 (Eliminated: 0 Frozen: 167106)
Constraints : 3820673 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 693MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 6.25s
Memory: 637MB (+0MB)
UNKNOWN
Iteration Time: 6.30s
Iteration 61
Queue: [(8,40,3,True), (9,45,3,True), (10,50,3,True), (11,55,3,False), (12,60,3,False), (13,65,3,False), (14,70,2,True), (15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,1,True), (23,115,1,True)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 62
Time : 378.781s (Solving: 360.69s 1st Model: 0.00s Unsat: 0.93s)
CPU Time : 378.844s
Choices : 5835330 (Domain: 5748522)
Conflicts : 500852 (Analyzed: 500849)
Restarts : 5732 (Average: 87.38 Last: 193)
Model-Level : 98.0
Problems : 62 (Average Length: 77.73 Splits: 0)
Lemmas : 500849 (Deleted: 471526)
Binary : 9069 (Ratio: 1.81%)
Ternary : 2556 (Ratio: 0.51%)
Conflict : 500849 (Average Length: 846.2 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 500849 (Average: 9.39 Max: 598 Sum: 4701685)
Executed : 500751 (Average: 9.38 Max: 598 Sum: 4699762 Ratio: 99.96%)
Bounded : 98 (Average: 19.62 Max: 112 Sum: 1923 Ratio: 0.04%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 509407 (Eliminated: 0 Frozen: 167106)
Constraints : 3820673 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 693MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 5.87s
Memory: 637MB (+0MB)
UNKNOWN
Iteration Time: 5.92s
Iteration 62
Queue: [(9,45,3,True), (10,50,3,True), (11,55,3,False), (12,60,3,False), (13,65,3,False), (14,70,2,True), (15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,1,True), (23,115,1,True)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 63
Time : 385.834s (Solving: 367.64s 1st Model: 0.00s Unsat: 0.93s)
CPU Time : 385.900s
Choices : 5912050 (Domain: 5825155)
Conflicts : 510175 (Analyzed: 510172)
Restarts : 5832 (Average: 87.48 Last: 193)
Model-Level : 98.0
Problems : 63 (Average Length: 78.35 Splits: 0)
Lemmas : 510172 (Deleted: 480613)
Binary : 9123 (Ratio: 1.79%)
Ternary : 2566 (Ratio: 0.50%)
Conflict : 510172 (Average Length: 848.9 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 510172 (Average: 9.33 Max: 598 Sum: 4758215)
Executed : 510074 (Average: 9.32 Max: 598 Sum: 4756292 Ratio: 99.96%)
Bounded : 98 (Average: 19.62 Max: 112 Sum: 1923 Ratio: 0.04%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 509407 (Eliminated: 0 Frozen: 167106)
Constraints : 3820673 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 693MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.02s
Memory: 637MB (+0MB)
UNKNOWN
Iteration Time: 7.06s
Iteration 63
Queue: [(10,50,3,True), (11,55,3,False), (12,60,3,False), (13,65,3,False), (14,70,2,True), (15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,1,True), (23,115,1,True)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 64
Time : 392.772s (Solving: 374.44s 1st Model: 0.00s Unsat: 0.93s)
CPU Time : 392.840s
Choices : 5987122 (Domain: 5900201)
Conflicts : 519364 (Analyzed: 519361)
Restarts : 5932 (Average: 87.55 Last: 209)
Model-Level : 98.0
Problems : 64 (Average Length: 78.95 Splits: 0)
Lemmas : 519361 (Deleted: 489738)
Binary : 9167 (Ratio: 1.77%)
Ternary : 2576 (Ratio: 0.50%)
Conflict : 519361 (Average Length: 852.9 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 519361 (Average: 9.26 Max: 598 Sum: 4811630)
Executed : 519263 (Average: 9.26 Max: 598 Sum: 4809707 Ratio: 99.96%)
Bounded : 98 (Average: 19.62 Max: 112 Sum: 1923 Ratio: 0.04%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 509407 (Eliminated: 0 Frozen: 167106)
Constraints : 3820673 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 693MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 6.89s
Memory: 637MB (+0MB)
UNKNOWN
Iteration Time: 6.94s
Iteration 64
Queue: [(14,70,2,True), (15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,1,True), (23,115,1,True)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 65
Time : 400.169s (Solving: 381.73s 1st Model: 0.00s Unsat: 0.93s)
CPU Time : 400.240s
Choices : 6102811 (Domain: 6015128)
Conflicts : 528034 (Analyzed: 528031)
Restarts : 6032 (Average: 87.54 Last: 209)
Model-Level : 98.0
Problems : 65 (Average Length: 79.54 Splits: 0)
Lemmas : 528031 (Deleted: 498633)
Binary : 9285 (Ratio: 1.76%)
Ternary : 2612 (Ratio: 0.49%)
Conflict : 528031 (Average Length: 857.1 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 528031 (Average: 9.26 Max: 598 Sum: 4892146)
Executed : 527933 (Average: 9.26 Max: 598 Sum: 4890223 Ratio: 99.96%)
Bounded : 98 (Average: 19.62 Max: 112 Sum: 1923 Ratio: 0.04%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 509407 (Eliminated: 0 Frozen: 167106)
Constraints : 3820673 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 693MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.36s
Memory: 637MB (+0MB)
UNKNOWN
Iteration Time: 7.40s
Iteration 65
Queue: [(15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,1,True), (23,115,1,True)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 66
Time : 408.031s (Solving: 389.48s 1st Model: 0.00s Unsat: 0.93s)
CPU Time : 408.104s
Choices : 6243201 (Domain: 6154767)
Conflicts : 537194 (Analyzed: 537191)
Restarts : 6132 (Average: 87.60 Last: 209)
Model-Level : 98.0
Problems : 66 (Average Length: 80.11 Splits: 0)
Lemmas : 537191 (Deleted: 507040)
Binary : 9398 (Ratio: 1.75%)
Ternary : 2631 (Ratio: 0.49%)
Conflict : 537191 (Average Length: 857.4 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 537191 (Average: 9.31 Max: 598 Sum: 5000280)
Executed : 537093 (Average: 9.30 Max: 598 Sum: 4998357 Ratio: 99.96%)
Bounded : 98 (Average: 19.62 Max: 112 Sum: 1923 Ratio: 0.04%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 509407 (Eliminated: 0 Frozen: 167106)
Constraints : 3820673 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 693MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.83s
Memory: 637MB (+0MB)
UNKNOWN
Iteration Time: 7.87s
Iteration 66
Queue: [(22,110,1,True), (23,115,1,True)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 67
Time : 415.550s (Solving: 396.89s 1st Model: 0.00s Unsat: 0.93s)
CPU Time : 415.624s
Choices : 6340880 (Domain: 6252441)
Conflicts : 546330 (Analyzed: 546327)
Restarts : 6232 (Average: 87.66 Last: 209)
Model-Level : 98.0
Problems : 67 (Average Length: 80.66 Splits: 0)
Lemmas : 546327 (Deleted: 516011)
Binary : 9424 (Ratio: 1.72%)
Ternary : 2638 (Ratio: 0.48%)
Conflict : 546327 (Average Length: 853.3 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 546327 (Average: 9.28 Max: 598 Sum: 5070734)
Executed : 546229 (Average: 9.28 Max: 598 Sum: 5068811 Ratio: 99.96%)
Bounded : 98 (Average: 19.62 Max: 112 Sum: 1923 Ratio: 0.04%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 509407 (Eliminated: 0 Frozen: 167106)
Constraints : 3820673 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 693MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.49s
Memory: 637MB (+0MB)
UNKNOWN
Iteration Time: 7.52s
Iteration 67
Queue: [(23,115,1,True)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 68
Time : 424.202s (Solving: 405.43s 1st Model: 0.00s Unsat: 0.93s)
CPU Time : 424.272s
Choices : 6428694 (Domain: 6340253)
Conflicts : 555007 (Analyzed: 555004)
Restarts : 6332 (Average: 87.65 Last: 209)
Model-Level : 98.0
Problems : 68 (Average Length: 81.19 Splits: 0)
Lemmas : 555004 (Deleted: 524932)
Binary : 9478 (Ratio: 1.71%)
Ternary : 2647 (Ratio: 0.48%)
Conflict : 555004 (Average Length: 857.1 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 555004 (Average: 9.23 Max: 598 Sum: 5123831)
Executed : 554906 (Average: 9.23 Max: 598 Sum: 5121908 Ratio: 99.96%)
Bounded : 98 (Average: 19.62 Max: 112 Sum: 1923 Ratio: 0.04%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 509407 (Eliminated: 0 Frozen: 167106)
Constraints : 3820673 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 693MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 8.61s
Memory: 637MB (+0MB)
UNKNOWN
Iteration Time: 8.65s
Iteration 68
Queue: [(4,20,5,True), (5,25,5,True), (6,30,5,True), (7,35,4,True), (8,40,4,True), (9,45,4,True), (10,50,4,False), (11,55,3,True), (12,60,3,True), (13,65,3,False), (14,70,3,False), (15,75,3,False), (16,80,2,True), (17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
Grounded Until: 115
Blocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 69
Time : 429.929s (Solving: 411.02s 1st Model: 0.00s Unsat: 0.93s)
CPU Time : 430.000s
Choices : 6472799 (Domain: 6384358)
Conflicts : 563173 (Analyzed: 563170)
Restarts : 6432 (Average: 87.56 Last: 209)
Model-Level : 98.0
Problems : 69 (Average Length: 81.71 Splits: 0)
Lemmas : 563170 (Deleted: 531089)
Binary : 9538 (Ratio: 1.69%)
Ternary : 2668 (Ratio: 0.47%)
Conflict : 563170 (Average Length: 851.5 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 563170 (Average: 9.17 Max: 598 Sum: 5165931)
Executed : 563070 (Average: 9.17 Max: 598 Sum: 5164006 Ratio: 99.96%)
Bounded : 100 (Average: 19.25 Max: 112 Sum: 1925 Ratio: 0.04%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 509407 (Eliminated: 0 Frozen: 167106)
Constraints : 3820673 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 693MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 5.68s
Memory: 637MB (+0MB)
UNKNOWN
Iteration Time: 5.73s
Iteration 69
Queue: [(5,25,5,True), (6,30,5,True), (7,35,4,True), (8,40,4,True), (9,45,4,True), (10,50,4,False), (11,55,3,True), (12,60,3,True), (13,65,3,False), (14,70,3,False), (15,75,3,False), (16,80,2,True), (17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 70
Time : 438.487s (Solving: 419.47s 1st Model: 0.00s Unsat: 0.93s)
CPU Time : 438.560s
Choices : 6530488 (Domain: 6442047)
Conflicts : 572091 (Analyzed: 572088)
Restarts : 6532 (Average: 87.58 Last: 209)
Model-Level : 98.0
Problems : 70 (Average Length: 82.21 Splits: 0)
Lemmas : 572088 (Deleted: 541169)
Binary : 9558 (Ratio: 1.67%)
Ternary : 2678 (Ratio: 0.47%)
Conflict : 572088 (Average Length: 863.2 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 572088 (Average: 9.11 Max: 598 Sum: 5210765)
Executed : 571988 (Average: 9.10 Max: 598 Sum: 5208840 Ratio: 99.96%)
Bounded : 100 (Average: 19.25 Max: 112 Sum: 1925 Ratio: 0.04%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 509407 (Eliminated: 0 Frozen: 167106)
Constraints : 3820673 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 693MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 8.53s
Memory: 637MB (+0MB)
UNKNOWN
Iteration Time: 8.56s
Iteration 70
Queue: [(6,30,5,True), (7,35,4,True), (8,40,4,True), (9,45,4,True), (10,50,4,False), (11,55,3,True), (12,60,3,True), (13,65,3,False), (14,70,3,False), (15,75,3,False), (16,80,2,True), (17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 71
Time : 445.822s (Solving: 426.68s 1st Model: 0.00s Unsat: 0.93s)
CPU Time : 445.900s
Choices : 6586094 (Domain: 6497653)
Conflicts : 580365 (Analyzed: 580362)
Restarts : 6632 (Average: 87.51 Last: 209)
Model-Level : 98.0
Problems : 71 (Average Length: 82.70 Splits: 0)
Lemmas : 580362 (Deleted: 548959)
Binary : 9593 (Ratio: 1.65%)
Ternary : 2685 (Ratio: 0.46%)
Conflict : 580362 (Average Length: 870.2 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 580362 (Average: 9.04 Max: 598 Sum: 5245610)
Executed : 580262 (Average: 9.04 Max: 598 Sum: 5243685 Ratio: 99.96%)
Bounded : 100 (Average: 19.25 Max: 112 Sum: 1925 Ratio: 0.04%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 509407 (Eliminated: 0 Frozen: 167106)
Constraints : 3820673 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 693MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.29s
Memory: 637MB (+0MB)
UNKNOWN
Iteration Time: 7.34s
Iteration 71
Queue: [(7,35,4,True), (8,40,4,True), (9,45,4,True), (10,50,4,False), (11,55,3,True), (12,60,3,True), (13,65,3,False), (14,70,3,False), (15,75,3,False), (16,80,2,True), (17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 72
Time : 452.051s (Solving: 432.78s 1st Model: 0.00s Unsat: 0.93s)
CPU Time : 452.132s
Choices : 6651279 (Domain: 6562838)
Conflicts : 589484 (Analyzed: 589481)
Restarts : 6732 (Average: 87.56 Last: 209)
Model-Level : 98.0
Problems : 72 (Average Length: 83.18 Splits: 0)
Lemmas : 589481 (Deleted: 558131)
Binary : 9616 (Ratio: 1.63%)
Ternary : 2691 (Ratio: 0.46%)
Conflict : 589481 (Average Length: 868.7 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 589481 (Average: 8.98 Max: 598 Sum: 5295181)
Executed : 589381 (Average: 8.98 Max: 598 Sum: 5293256 Ratio: 99.96%)
Bounded : 100 (Average: 19.25 Max: 112 Sum: 1925 Ratio: 0.04%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 509407 (Eliminated: 0 Frozen: 167106)
Constraints : 3820673 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 693MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 6.19s
Memory: 637MB (+0MB)
UNKNOWN
Iteration Time: 6.23s
Iteration 72
Queue: [(8,40,4,True), (9,45,4,True), (10,50,4,False), (11,55,3,True), (12,60,3,True), (13,65,3,False), (14,70,3,False), (15,75,3,False), (16,80,2,True), (17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 73
Time : 458.908s (Solving: 439.51s 1st Model: 0.00s Unsat: 0.93s)
CPU Time : 458.992s
Choices : 6717871 (Domain: 6629430)
Conflicts : 599011 (Analyzed: 599008)
Restarts : 6832 (Average: 87.68 Last: 209)
Model-Level : 98.0
Problems : 73 (Average Length: 83.64 Splits: 0)
Lemmas : 599008 (Deleted: 567096)
Binary : 9635 (Ratio: 1.61%)
Ternary : 2700 (Ratio: 0.45%)
Conflict : 599008 (Average Length: 869.2 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 599008 (Average: 8.92 Max: 598 Sum: 5343591)
Executed : 598908 (Average: 8.92 Max: 598 Sum: 5341666 Ratio: 99.96%)
Bounded : 100 (Average: 19.25 Max: 112 Sum: 1925 Ratio: 0.04%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 509407 (Eliminated: 0 Frozen: 167106)
Constraints : 3820673 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 693MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 6.81s
Memory: 637MB (+0MB)
UNKNOWN
Iteration Time: 6.86s
Iteration 73
Queue: [(9,45,4,True), (10,50,4,False), (11,55,3,True), (12,60,3,True), (13,65,3,False), (14,70,3,False), (15,75,3,False), (16,80,2,True), (17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 74
Time : 465.847s (Solving: 446.33s 1st Model: 0.00s Unsat: 0.93s)
CPU Time : 465.932s
Choices : 6807348 (Domain: 6718225)
Conflicts : 608070 (Analyzed: 608067)
Restarts : 6932 (Average: 87.72 Last: 209)
Model-Level : 98.0
Problems : 74 (Average Length: 84.09 Splits: 0)
Lemmas : 608067 (Deleted: 576413)
Binary : 9725 (Ratio: 1.60%)
Ternary : 2717 (Ratio: 0.45%)
Conflict : 608067 (Average Length: 870.9 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 608067 (Average: 8.89 Max: 598 Sum: 5408420)
Executed : 607967 (Average: 8.89 Max: 598 Sum: 5406495 Ratio: 99.96%)
Bounded : 100 (Average: 19.25 Max: 112 Sum: 1925 Ratio: 0.04%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 509407 (Eliminated: 0 Frozen: 167106)
Constraints : 3820673 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 693MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 6.90s
Memory: 637MB (+0MB)
UNKNOWN
Iteration Time: 6.95s
Iteration 74
Queue: [(11,55,3,True), (12,60,3,True), (13,65,3,False), (14,70,3,False), (15,75,3,False), (16,80,2,True), (17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 75
Time : 472.657s (Solving: 453.04s 1st Model: 0.00s Unsat: 0.93s)
CPU Time : 472.744s
Choices : 6882427 (Domain: 6793304)
Conflicts : 617394 (Analyzed: 617391)
Restarts : 7032 (Average: 87.80 Last: 209)
Model-Level : 98.0
Problems : 75 (Average Length: 84.53 Splits: 0)
Lemmas : 617391 (Deleted: 585307)
Binary : 9741 (Ratio: 1.58%)
Ternary : 2725 (Ratio: 0.44%)
Conflict : 617391 (Average Length: 870.6 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 617391 (Average: 8.85 Max: 598 Sum: 5463161)
Executed : 617291 (Average: 8.85 Max: 598 Sum: 5461236 Ratio: 99.96%)
Bounded : 100 (Average: 19.25 Max: 112 Sum: 1925 Ratio: 0.04%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 509407 (Eliminated: 0 Frozen: 167106)
Constraints : 3820673 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 693MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 6.78s
Memory: 637MB (+0MB)
UNKNOWN
Iteration Time: 6.82s
Iteration 75
Queue: [(12,60,3,True), (13,65,3,False), (14,70,3,False), (15,75,3,False), (16,80,2,True), (17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 76
Time : 479.910s (Solving: 460.16s 1st Model: 0.00s Unsat: 0.93s)
CPU Time : 480.000s
Choices : 6961035 (Domain: 6871899)
Conflicts : 626965 (Analyzed: 626962)
Restarts : 7132 (Average: 87.91 Last: 209)
Model-Level : 98.0
Problems : 76 (Average Length: 84.96 Splits: 0)
Lemmas : 626962 (Deleted: 594486)
Binary : 9786 (Ratio: 1.56%)
Ternary : 2730 (Ratio: 0.44%)
Conflict : 626962 (Average Length: 870.4 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 626962 (Average: 8.80 Max: 598 Sum: 5518510)
Executed : 626862 (Average: 8.80 Max: 598 Sum: 5516585 Ratio: 99.97%)
Bounded : 100 (Average: 19.25 Max: 112 Sum: 1925 Ratio: 0.03%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 509407 (Eliminated: 0 Frozen: 167106)
Constraints : 3820673 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 693MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.21s
Memory: 637MB (+0MB)
UNKNOWN
Iteration Time: 7.26s
Iteration 76
Queue: [(16,80,2,True), (17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 77
Time : 486.930s (Solving: 467.07s 1st Model: 0.00s Unsat: 0.93s)
CPU Time : 487.020s
Choices : 7038394 (Domain: 6949258)
Conflicts : 635875 (Analyzed: 635872)
Restarts : 7232 (Average: 87.92 Last: 209)
Model-Level : 98.0
Problems : 77 (Average Length: 85.38 Splits: 0)
Lemmas : 635872 (Deleted: 603913)
Binary : 9791 (Ratio: 1.54%)
Ternary : 2736 (Ratio: 0.43%)
Conflict : 635872 (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 : 635872 (Average: 8.76 Max: 598 Sum: 5572681)
Executed : 635772 (Average: 8.76 Max: 598 Sum: 5570756 Ratio: 99.97%)
Bounded : 100 (Average: 19.25 Max: 112 Sum: 1925 Ratio: 0.03%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 509407 (Eliminated: 0 Frozen: 167106)
Constraints : 3820673 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 693MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 6.98s
Memory: 637MB (+0MB)
UNKNOWN
Iteration Time: 7.03s
Iteration 77
Queue: [(17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 78
Time : 495.331s (Solving: 475.35s 1st Model: 0.00s Unsat: 0.93s)
CPU Time : 495.424s
Choices : 7123422 (Domain: 7034286)
Conflicts : 645815 (Analyzed: 645812)
Restarts : 7332 (Average: 88.08 Last: 209)
Model-Level : 98.0
Problems : 78 (Average Length: 85.78 Splits: 0)
Lemmas : 645812 (Deleted: 612739)
Binary : 9805 (Ratio: 1.52%)
Ternary : 2743 (Ratio: 0.42%)
Conflict : 645812 (Average Length: 871.3 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 645812 (Average: 8.72 Max: 598 Sum: 5630627)
Executed : 645712 (Average: 8.72 Max: 598 Sum: 5628702 Ratio: 99.97%)
Bounded : 100 (Average: 19.25 Max: 112 Sum: 1925 Ratio: 0.03%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 509407 (Eliminated: 0 Frozen: 167106)
Constraints : 3820673 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 693MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 8.36s
Memory: 637MB (+0MB)
UNKNOWN
Iteration Time: 8.41s
Iteration 78
Queue: [(4,20,6,True), (5,25,6,True), (6,30,6,True), (7,35,5,True), (8,40,5,True), (9,45,5,False), (10,50,4,True), (11,55,4,False), (12,60,4,False), (13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,3,False), (17,85,3,False), (18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
Grounded Until: 115
Blocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 79
Time : 499.159s (Solving: 479.03s 1st Model: 0.00s Unsat: 0.93s)
CPU Time : 499.252s
Choices : 7159631 (Domain: 7070495)
Conflicts : 653661 (Analyzed: 653658)
Restarts : 7432 (Average: 87.95 Last: 209)
Model-Level : 98.0
Problems : 79 (Average Length: 86.18 Splits: 0)
Lemmas : 653658 (Deleted: 620300)
Binary : 9843 (Ratio: 1.51%)
Ternary : 2752 (Ratio: 0.42%)
Conflict : 653658 (Average Length: 867.0 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 653658 (Average: 8.66 Max: 598 Sum: 5662032)
Executed : 653558 (Average: 8.66 Max: 598 Sum: 5660107 Ratio: 99.97%)
Bounded : 100 (Average: 19.25 Max: 112 Sum: 1925 Ratio: 0.03%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 509407 (Eliminated: 0 Frozen: 167106)
Constraints : 3820673 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 693MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 3.77s
Memory: 637MB (+0MB)
UNKNOWN
Iteration Time: 3.83s
Iteration 79
Queue: [(5,25,6,True), (6,30,6,True), (7,35,5,True), (8,40,5,True), (9,45,5,False), (10,50,4,True), (11,55,4,False), (12,60,4,False), (13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,3,False), (17,85,3,False), (18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 80
Time : 507.997s (Solving: 487.73s 1st Model: 0.00s Unsat: 0.93s)
CPU Time : 508.096s
Choices : 7219333 (Domain: 7130197)
Conflicts : 662838 (Analyzed: 662835)
Restarts : 7532 (Average: 88.00 Last: 209)
Model-Level : 98.0
Problems : 80 (Average Length: 86.56 Splits: 0)
Lemmas : 662835 (Deleted: 630085)
Binary : 9879 (Ratio: 1.49%)
Ternary : 2761 (Ratio: 0.42%)
Conflict : 662835 (Average Length: 876.4 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 662835 (Average: 8.61 Max: 598 Sum: 5708341)
Executed : 662735 (Average: 8.61 Max: 598 Sum: 5706416 Ratio: 99.97%)
Bounded : 100 (Average: 19.25 Max: 112 Sum: 1925 Ratio: 0.03%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 509407 (Eliminated: 0 Frozen: 167106)
Constraints : 3820673 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 693MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 8.79s
Memory: 637MB (+0MB)
UNKNOWN
Iteration Time: 8.85s
Iteration 80
Queue: [(6,30,6,True), (7,35,5,True), (8,40,5,True), (9,45,5,False), (10,50,4,True), (11,55,4,False), (12,60,4,False), (13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,3,False), (17,85,3,False), (18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 81
Time : 515.883s (Solving: 495.49s 1st Model: 0.00s Unsat: 0.93s)
CPU Time : 515.988s
Choices : 7273855 (Domain: 7184719)
Conflicts : 671072 (Analyzed: 671069)
Restarts : 7632 (Average: 87.93 Last: 209)
Model-Level : 98.0
Problems : 81 (Average Length: 86.94 Splits: 0)
Lemmas : 671069 (Deleted: 638696)
Binary : 9917 (Ratio: 1.48%)
Ternary : 2765 (Ratio: 0.41%)
Conflict : 671069 (Average Length: 884.6 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 671069 (Average: 8.56 Max: 598 Sum: 5742962)
Executed : 670969 (Average: 8.56 Max: 598 Sum: 5741037 Ratio: 99.97%)
Bounded : 100 (Average: 19.25 Max: 112 Sum: 1925 Ratio: 0.03%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 509407 (Eliminated: 0 Frozen: 167106)
Constraints : 3820673 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 693MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.84s
Memory: 637MB (+0MB)
UNKNOWN
Iteration Time: 7.89s
Iteration 81
Queue: [(7,35,5,True), (8,40,5,True), (9,45,5,False), (10,50,4,True), (11,55,4,False), (12,60,4,False), (13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,3,False), (17,85,3,False), (18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 82
Time : 522.219s (Solving: 501.70s 1st Model: 0.00s Unsat: 0.93s)
CPU Time : 522.328s
Choices : 7338585 (Domain: 7249449)
Conflicts : 680322 (Analyzed: 680319)
Restarts : 7732 (Average: 87.99 Last: 209)
Model-Level : 98.0
Problems : 82 (Average Length: 87.30 Splits: 0)
Lemmas : 680319 (Deleted: 647309)
Binary : 9933 (Ratio: 1.46%)
Ternary : 2769 (Ratio: 0.41%)
Conflict : 680319 (Average Length: 884.7 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 680319 (Average: 8.51 Max: 598 Sum: 5788703)
Executed : 680219 (Average: 8.51 Max: 598 Sum: 5786778 Ratio: 99.97%)
Bounded : 100 (Average: 19.25 Max: 112 Sum: 1925 Ratio: 0.03%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 509407 (Eliminated: 0 Frozen: 167106)
Constraints : 3820673 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 693MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 6.28s
Memory: 637MB (+0MB)
UNKNOWN
Iteration Time: 6.34s
Iteration 82
Queue: [(8,40,5,True), (9,45,5,False), (10,50,4,True), (11,55,4,False), (12,60,4,False), (13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,3,False), (17,85,3,False), (18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 83
Time : 528.837s (Solving: 508.21s 1st Model: 0.00s Unsat: 0.93s)
CPU Time : 528.952s
Choices : 7411387 (Domain: 7322167)
Conflicts : 689944 (Analyzed: 689941)
Restarts : 7832 (Average: 88.09 Last: 209)
Model-Level : 98.0
Problems : 83 (Average Length: 87.66 Splits: 0)
Lemmas : 689941 (Deleted: 656401)
Binary : 9953 (Ratio: 1.44%)
Ternary : 2780 (Ratio: 0.40%)
Conflict : 689941 (Average Length: 883.9 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 689941 (Average: 8.47 Max: 598 Sum: 5843665)
Executed : 689841 (Average: 8.47 Max: 598 Sum: 5841740 Ratio: 99.97%)
Bounded : 100 (Average: 19.25 Max: 112 Sum: 1925 Ratio: 0.03%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 509407 (Eliminated: 0 Frozen: 167106)
Constraints : 3820673 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 693MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 6.58s
Memory: 637MB (+0MB)
UNKNOWN
Iteration Time: 6.62s
Iteration 83
Queue: [(10,50,4,True), (11,55,4,False), (12,60,4,False), (13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,3,False), (17,85,3,False), (18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 84
Time : 535.551s (Solving: 514.79s 1st Model: 0.00s Unsat: 0.93s)
CPU Time : 535.672s
Choices : 7501009 (Domain: 7411212)
Conflicts : 698681 (Analyzed: 698678)
Restarts : 7932 (Average: 88.08 Last: 209)
Model-Level : 98.0
Problems : 84 (Average Length: 88.01 Splits: 0)
Lemmas : 698678 (Deleted: 665747)
Binary : 10052 (Ratio: 1.44%)
Ternary : 2800 (Ratio: 0.40%)
Conflict : 698678 (Average Length: 884.1 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 698678 (Average: 8.45 Max: 598 Sum: 5906045)
Executed : 698578 (Average: 8.45 Max: 598 Sum: 5904120 Ratio: 99.97%)
Bounded : 100 (Average: 19.25 Max: 112 Sum: 1925 Ratio: 0.03%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 509407 (Eliminated: 0 Frozen: 167106)
Constraints : 3820673 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 693MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 6.67s
Memory: 637MB (+0MB)
UNKNOWN
Iteration Time: 6.72s
Iteration 84
Queue: [(13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,3,False), (17,85,3,False), (18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 85
Time : 543.185s (Solving: 522.29s 1st Model: 0.00s Unsat: 0.93s)
CPU Time : 543.308s
Choices : 7597665 (Domain: 7507818)
Conflicts : 708129 (Analyzed: 708126)
Restarts : 8032 (Average: 88.16 Last: 209)
Model-Level : 98.0
Problems : 85 (Average Length: 88.35 Splits: 0)
Lemmas : 708126 (Deleted: 674332)
Binary : 10102 (Ratio: 1.43%)
Ternary : 2816 (Ratio: 0.40%)
Conflict : 708126 (Average Length: 882.4 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 708126 (Average: 8.44 Max: 598 Sum: 5978801)
Executed : 708026 (Average: 8.44 Max: 598 Sum: 5976876 Ratio: 99.97%)
Bounded : 100 (Average: 19.25 Max: 112 Sum: 1925 Ratio: 0.03%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 509407 (Eliminated: 0 Frozen: 167106)
Constraints : 3820673 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 693MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.59s
Memory: 637MB (+0MB)
UNKNOWN
Iteration Time: 7.64s
Iteration 85
Queue: [(18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 86
Time : 551.310s (Solving: 530.30s 1st Model: 0.00s Unsat: 0.93s)
CPU Time : 551.440s
Choices : 7693624 (Domain: 7603747)
Conflicts : 717189 (Analyzed: 717186)
Restarts : 8132 (Average: 88.19 Last: 209)
Model-Level : 98.0
Problems : 86 (Average Length: 88.69 Splits: 0)
Lemmas : 717186 (Deleted: 683610)
Binary : 10126 (Ratio: 1.41%)
Ternary : 2820 (Ratio: 0.39%)
Conflict : 717186 (Average Length: 882.3 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 717186 (Average: 8.43 Max: 598 Sum: 6047099)
Executed : 717086 (Average: 8.43 Max: 598 Sum: 6045174 Ratio: 99.97%)
Bounded : 100 (Average: 19.25 Max: 112 Sum: 1925 Ratio: 0.03%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 509407 (Eliminated: 0 Frozen: 167106)
Constraints : 3820673 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 693MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 8.09s
Memory: 637MB (+0MB)
UNKNOWN
Iteration Time: 8.13s
Iteration 86
Queue: [(4,20,7,True), (5,25,7,True), (6,30,7,False), (7,35,6,True), (8,40,6,False), (9,45,5,True), (10,50,5,False), (11,55,4,True), (12,60,4,False), (13,65,4,False), (14,70,3,True), (15,75,3,True), (16,80,3,False), (17,85,3,False), (18,90,3,False), (19,95,2,True), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
Grounded Until: 115
Blocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 87
Time : 554.781s (Solving: 533.64s 1st Model: 0.00s Unsat: 0.93s)
CPU Time : 554.912s
Choices : 7718191 (Domain: 7628314)
Conflicts : 724757 (Analyzed: 724754)
Restarts : 8232 (Average: 88.04 Last: 209)
Model-Level : 98.0
Problems : 87 (Average Length: 89.01 Splits: 0)
Lemmas : 724754 (Deleted: 690345)
Binary : 10150 (Ratio: 1.40%)
Ternary : 2826 (Ratio: 0.39%)
Conflict : 724754 (Average Length: 878.0 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 724754 (Average: 8.37 Max: 598 Sum: 6066735)
Executed : 724654 (Average: 8.37 Max: 598 Sum: 6064810 Ratio: 99.97%)
Bounded : 100 (Average: 19.25 Max: 112 Sum: 1925 Ratio: 0.03%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 509407 (Eliminated: 0 Frozen: 167106)
Constraints : 3820673 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 693MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 3.42s
Memory: 637MB (+0MB)
UNKNOWN
Iteration Time: 3.48s
Iteration 87
Queue: [(5,25,7,True), (6,30,7,False), (7,35,6,True), (8,40,6,False), (9,45,5,True), (10,50,5,False), (11,55,4,True), (12,60,4,False), (13,65,4,False), (14,70,3,True), (15,75,3,True), (16,80,3,False), (17,85,3,False), (18,90,3,False), (19,95,2,True), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 88
Time : 562.973s (Solving: 541.72s 1st Model: 0.00s Unsat: 0.93s)
CPU Time : 563.104s
Choices : 7768872 (Domain: 7678995)
Conflicts : 733384 (Analyzed: 733381)
Restarts : 8332 (Average: 88.02 Last: 209)
Model-Level : 98.0
Problems : 88 (Average Length: 89.33 Splits: 0)
Lemmas : 733381 (Deleted: 699888)
Binary : 10207 (Ratio: 1.39%)
Ternary : 2841 (Ratio: 0.39%)
Conflict : 733381 (Average Length: 881.9 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 733381 (Average: 8.33 Max: 598 Sum: 6105439)
Executed : 733281 (Average: 8.32 Max: 598 Sum: 6103514 Ratio: 99.97%)
Bounded : 100 (Average: 19.25 Max: 112 Sum: 1925 Ratio: 0.03%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 509407 (Eliminated: 0 Frozen: 167106)
Constraints : 3820673 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 693MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 8.16s
Memory: 637MB (+0MB)
UNKNOWN
Iteration Time: 8.20s
Iteration 88
Queue: [(7,35,6,True), (8,40,6,False), (9,45,5,True), (10,50,5,False), (11,55,4,True), (12,60,4,False), (13,65,4,False), (14,70,3,True), (15,75,3,True), (16,80,3,False), (17,85,3,False), (18,90,3,False), (19,95,2,True), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 89
Time : 568.657s (Solving: 547.28s 1st Model: 0.00s Unsat: 0.93s)
CPU Time : 568.792s
Choices : 7827324 (Domain: 7737447)
Conflicts : 742115 (Analyzed: 742112)
Restarts : 8432 (Average: 88.01 Last: 209)
Model-Level : 98.0
Problems : 89 (Average Length: 89.64 Splits: 0)
Lemmas : 742112 (Deleted: 708348)
Binary : 10214 (Ratio: 1.38%)
Ternary : 2843 (Ratio: 0.38%)
Conflict : 742112 (Average Length: 880.8 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 742112 (Average: 8.28 Max: 598 Sum: 6147154)
Executed : 742012 (Average: 8.28 Max: 598 Sum: 6145229 Ratio: 99.97%)
Bounded : 100 (Average: 19.25 Max: 112 Sum: 1925 Ratio: 0.03%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 509407 (Eliminated: 0 Frozen: 167106)
Constraints : 3820673 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 693MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 5.64s
Memory: 637MB (+0MB)
UNKNOWN
Iteration Time: 5.69s
Iteration 89
Queue: [(9,45,5,True), (10,50,5,False), (11,55,4,True), (12,60,4,False), (13,65,4,False), (14,70,3,True), (15,75,3,True), (16,80,3,False), (17,85,3,False), (18,90,3,False), (19,95,2,True), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 90
Time : 575.320s (Solving: 553.82s 1st Model: 0.00s Unsat: 0.93s)
CPU Time : 575.448s
Choices : 7892623 (Domain: 7802743)
Conflicts : 751112 (Analyzed: 751109)
Restarts : 8532 (Average: 88.03 Last: 209)
Model-Level : 98.0
Problems : 90 (Average Length: 89.94 Splits: 0)
Lemmas : 751109 (Deleted: 716971)
Binary : 10228 (Ratio: 1.36%)
Ternary : 2851 (Ratio: 0.38%)
Conflict : 751109 (Average Length: 882.1 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 751109 (Average: 8.25 Max: 598 Sum: 6193140)
Executed : 751008 (Average: 8.24 Max: 598 Sum: 6191098 Ratio: 99.97%)
Bounded : 101 (Average: 20.22 Max: 117 Sum: 2042 Ratio: 0.03%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 509407 (Eliminated: 0 Frozen: 167106)
Constraints : 3820673 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 693MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 6.61s
Memory: 637MB (+0MB)
UNKNOWN
Iteration Time: 6.66s
Iteration 90
Queue: [(11,55,4,True), (12,60,4,False), (13,65,4,False), (14,70,3,True), (15,75,3,True), (16,80,3,False), (17,85,3,False), (18,90,3,False), (19,95,2,True), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 91
Time : 582.377s (Solving: 560.74s 1st Model: 0.00s Unsat: 0.93s)
CPU Time : 582.508s
Choices : 7963613 (Domain: 7873726)
Conflicts : 759637 (Analyzed: 759634)
Restarts : 8632 (Average: 88.00 Last: 209)
Model-Level : 98.0
Problems : 91 (Average Length: 90.24 Splits: 0)
Lemmas : 759634 (Deleted: 723966)
Binary : 10266 (Ratio: 1.35%)
Ternary : 2858 (Ratio: 0.38%)
Conflict : 759634 (Average Length: 883.9 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 759634 (Average: 8.22 Max: 598 Sum: 6241844)
Executed : 759533 (Average: 8.21 Max: 598 Sum: 6239802 Ratio: 99.97%)
Bounded : 101 (Average: 20.22 Max: 117 Sum: 2042 Ratio: 0.03%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 509407 (Eliminated: 0 Frozen: 167106)
Constraints : 3820659 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 693MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.01s
Memory: 637MB (+0MB)
UNKNOWN
Iteration Time: 7.06s
Iteration 91
Queue: [(14,70,3,True), (15,75,3,True), (16,80,3,False), (17,85,3,False), (18,90,3,False), (19,95,2,True), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 92
Time : 589.622s (Solving: 567.86s 1st Model: 0.00s Unsat: 0.93s)
CPU Time : 589.756s
Choices : 8039764 (Domain: 7949877)
Conflicts : 768735 (Analyzed: 768732)
Restarts : 8732 (Average: 88.04 Last: 209)
Model-Level : 98.0
Problems : 92 (Average Length: 90.53 Splits: 0)
Lemmas : 768732 (Deleted: 734162)
Binary : 10282 (Ratio: 1.34%)
Ternary : 2864 (Ratio: 0.37%)
Conflict : 768732 (Average Length: 883.9 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 768732 (Average: 8.19 Max: 598 Sum: 6295444)
Executed : 768631 (Average: 8.19 Max: 598 Sum: 6293402 Ratio: 99.97%)
Bounded : 101 (Average: 20.22 Max: 117 Sum: 2042 Ratio: 0.03%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 509407 (Eliminated: 0 Frozen: 167106)
Constraints : 3820659 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 693MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.20s
Memory: 637MB (+0MB)
UNKNOWN
Iteration Time: 7.25s
Iteration 92
Queue: [(15,75,3,True), (16,80,3,False), (17,85,3,False), (18,90,3,False), (19,95,2,True), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 93
Time : 596.841s (Solving: 574.94s 1st Model: 0.00s Unsat: 0.93s)
CPU Time : 596.976s
Choices : 8152180 (Domain: 8062006)
Conflicts : 777365 (Analyzed: 777362)
Restarts : 8832 (Average: 88.02 Last: 209)
Model-Level : 98.0
Problems : 93 (Average Length: 90.82 Splits: 0)
Lemmas : 777362 (Deleted: 743065)
Binary : 10338 (Ratio: 1.33%)
Ternary : 2878 (Ratio: 0.37%)
Conflict : 777362 (Average Length: 883.6 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 777362 (Average: 8.21 Max: 598 Sum: 6378263)
Executed : 777261 (Average: 8.20 Max: 598 Sum: 6376221 Ratio: 99.97%)
Bounded : 101 (Average: 20.22 Max: 117 Sum: 2042 Ratio: 0.03%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 509407 (Eliminated: 0 Frozen: 167106)
Constraints : 3820659 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 693MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.17s
Memory: 637MB (+0MB)
UNKNOWN
Iteration Time: 7.22s
Iteration 93
Queue: [(19,95,2,True), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 94
Time : 605.009s (Solving: 583.00s 1st Model: 0.00s Unsat: 0.93s)
CPU Time : 605.148s
Choices : 8272788 (Domain: 8182388)
Conflicts : 786486 (Analyzed: 786483)
Restarts : 8932 (Average: 88.05 Last: 209)
Model-Level : 98.0
Problems : 94 (Average Length: 91.10 Splits: 0)
Lemmas : 786483 (Deleted: 751577)
Binary : 10387 (Ratio: 1.32%)
Ternary : 2893 (Ratio: 0.37%)
Conflict : 786483 (Average Length: 883.7 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 786483 (Average: 8.23 Max: 598 Sum: 6469068)
Executed : 786382 (Average: 8.22 Max: 598 Sum: 6467026 Ratio: 99.97%)
Bounded : 101 (Average: 20.22 Max: 117 Sum: 2042 Ratio: 0.03%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 509407 (Eliminated: 0 Frozen: 167106)
Constraints : 3820659 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 693MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 8.13s
Memory: 637MB (+0MB)
UNKNOWN
Iteration Time: 8.17s
Iteration 94
Queue: [(4,20,8,True), (5,25,8,True), (6,30,7,True), (7,35,7,True), (8,40,6,True), (9,45,6,False), (10,50,5,True), (11,55,5,False), (12,60,4,True), (13,65,4,False), (14,70,4,False), (15,75,4,False), (16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,True), (22,110,2,False), (23,115,2,False)]
Grounded Until: 115
Blocking actions...
Solving...
[start: stats after solve call]
Models : 0
Calls : 95
Time : 607.458s (Solving: 585.31s 1st Model: 0.00s Unsat: 3.24s)
CPU Time : 607.596s
Choices : 8283688 (Domain: 8193288)
Conflicts : 788809 (Analyzed: 788805)
Restarts : 8957 (Average: 88.07 Last: 209)
Model-Level : 98.0
Problems : 95 (Average Length: 91.37 Splits: 0)
Lemmas : 788805 (Deleted: 754276)
Binary : 10407 (Ratio: 1.32%)
Ternary : 2897 (Ratio: 0.37%)
Conflict : 788805 (Average Length: 882.4 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 788805 (Average: 8.21 Max: 598 Sum: 6479792)
Executed : 788700 (Average: 8.21 Max: 598 Sum: 6477522 Ratio: 99.96%)
Bounded : 105 (Average: 21.62 Max: 117 Sum: 2270 Ratio: 0.04%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 509407 (Eliminated: 0 Frozen: 167106)
Constraints : 3820659 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 693MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 2.39s
Memory: 637MB (+0MB)
UNSAT
Iteration Time: 2.45s
Iteration 95
Queue: [(5,25,8,True), (6,30,7,True), (7,35,7,True), (8,40,6,True), (9,45,6,False), (10,50,5,True), (11,55,5,False), (12,60,4,True), (13,65,4,False), (14,70,4,False), (15,75,4,False), (16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,True), (22,110,2,False), (23,115,2,False)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 96
Time : 615.523s (Solving: 593.27s 1st Model: 0.00s Unsat: 3.24s)
CPU Time : 615.664s
Choices : 8331151 (Domain: 8240751)
Conflicts : 797446 (Analyzed: 797442)
Restarts : 9057 (Average: 88.05 Last: 209)
Model-Level : 98.0
Problems : 96 (Average Length: 91.64 Splits: 0)
Lemmas : 797442 (Deleted: 762712)
Binary : 10431 (Ratio: 1.31%)
Ternary : 2915 (Ratio: 0.37%)
Conflict : 797442 (Average Length: 885.4 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 797442 (Average: 8.17 Max: 598 Sum: 6515993)
Executed : 797337 (Average: 8.17 Max: 598 Sum: 6513723 Ratio: 99.97%)
Bounded : 105 (Average: 21.62 Max: 117 Sum: 2270 Ratio: 0.03%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 509407 (Eliminated: 0 Frozen: 167106)
Constraints : 3820659 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 693MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 8.03s
Memory: 637MB (+0MB)
UNKNOWN
Iteration Time: 8.07s
Iteration 96
Queue: [(6,30,7,True), (7,35,7,True), (8,40,6,True), (9,45,6,False), (10,50,5,True), (11,55,5,False), (12,60,4,True), (13,65,4,False), (14,70,4,False), (15,75,4,False), (16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,True), (22,110,2,False), (23,115,2,False)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 97
Time : 622.222s (Solving: 599.86s 1st Model: 0.00s Unsat: 3.24s)
CPU Time : 622.364s
Choices : 8395803 (Domain: 8305403)
Conflicts : 805331 (Analyzed: 805327)
Restarts : 9157 (Average: 87.95 Last: 209)
Model-Level : 98.0
Problems : 97 (Average Length: 91.90 Splits: 0)
Lemmas : 805327 (Deleted: 769174)
Binary : 10457 (Ratio: 1.30%)
Ternary : 2920 (Ratio: 0.36%)
Conflict : 805327 (Average Length: 889.9 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 805327 (Average: 8.15 Max: 598 Sum: 6563153)
Executed : 805222 (Average: 8.15 Max: 598 Sum: 6560883 Ratio: 99.97%)
Bounded : 105 (Average: 21.62 Max: 117 Sum: 2270 Ratio: 0.03%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 509407 (Eliminated: 0 Frozen: 167106)
Constraints : 3820659 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 693MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 6.67s
Memory: 637MB (+0MB)
UNKNOWN
Iteration Time: 6.71s
Iteration 97
Queue: [(7,35,7,True), (8,40,6,True), (9,45,6,False), (10,50,5,True), (11,55,5,False), (12,60,4,True), (13,65,4,False), (14,70,4,False), (15,75,4,False), (16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,True), (22,110,2,False), (23,115,2,False)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 98
Time : 628.687s (Solving: 606.18s 1st Model: 0.00s Unsat: 3.24s)
CPU Time : 628.824s
Choices : 8456439 (Domain: 8366039)
Conflicts : 814442 (Analyzed: 814438)
Restarts : 9257 (Average: 87.98 Last: 209)
Model-Level : 98.0
Problems : 98 (Average Length: 92.15 Splits: 0)
Lemmas : 814438 (Deleted: 779042)
Binary : 10468 (Ratio: 1.29%)
Ternary : 2927 (Ratio: 0.36%)
Conflict : 814438 (Average Length: 890.4 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 814438 (Average: 8.11 Max: 598 Sum: 6607040)
Executed : 814333 (Average: 8.11 Max: 598 Sum: 6604770 Ratio: 99.97%)
Bounded : 105 (Average: 21.62 Max: 117 Sum: 2270 Ratio: 0.03%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 509407 (Eliminated: 0 Frozen: 167106)
Constraints : 3820659 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 693MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 6.40s
Memory: 637MB (+0MB)
UNKNOWN
Iteration Time: 6.46s
Iteration 98
Queue: [(8,40,6,True), (9,45,6,False), (10,50,5,True), (11,55,5,False), (12,60,4,True), (13,65,4,False), (14,70,4,False), (15,75,4,False), (16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,True), (22,110,2,False), (23,115,2,False)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 99
Time : 634.852s (Solving: 612.24s 1st Model: 0.00s Unsat: 3.24s)
CPU Time : 634.992s
Choices : 8525976 (Domain: 8435337)
Conflicts : 823225 (Analyzed: 823221)
Restarts : 9357 (Average: 87.98 Last: 209)
Model-Level : 98.0
Problems : 99 (Average Length: 92.40 Splits: 0)
Lemmas : 823221 (Deleted: 788019)
Binary : 10514 (Ratio: 1.28%)
Ternary : 2939 (Ratio: 0.36%)
Conflict : 823221 (Average Length: 890.4 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 823221 (Average: 8.09 Max: 598 Sum: 6656281)
Executed : 823116 (Average: 8.08 Max: 598 Sum: 6654011 Ratio: 99.97%)
Bounded : 105 (Average: 21.62 Max: 117 Sum: 2270 Ratio: 0.03%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 509407 (Eliminated: 0 Frozen: 167106)
Constraints : 3820659 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 693MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 6.13s
Memory: 637MB (+0MB)
UNKNOWN
Iteration Time: 6.17s
Iteration 99
Queue: [(10,50,5,True), (11,55,5,False), (12,60,4,True), (13,65,4,False), (14,70,4,False), (15,75,4,False), (16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,True), (22,110,2,False), (23,115,2,False)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 100
Time : 642.263s (Solving: 619.52s 1st Model: 0.00s Unsat: 3.24s)
CPU Time : 642.404s
Choices : 8600906 (Domain: 8510267)
Conflicts : 833096 (Analyzed: 833092)
Restarts : 9457 (Average: 88.09 Last: 209)
Model-Level : 98.0
Problems : 100 (Average Length: 92.65 Splits: 0)
Lemmas : 833092 (Deleted: 796623)
Binary : 10529 (Ratio: 1.26%)
Ternary : 2944 (Ratio: 0.35%)
Conflict : 833092 (Average Length: 889.2 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 833092 (Average: 8.05 Max: 598 Sum: 6710446)
Executed : 832987 (Average: 8.05 Max: 598 Sum: 6708176 Ratio: 99.97%)
Bounded : 105 (Average: 21.62 Max: 117 Sum: 2270 Ratio: 0.03%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 509407 (Eliminated: 0 Frozen: 167106)
Constraints : 3820659 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 693MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.36s
Memory: 637MB (+0MB)
UNKNOWN
Iteration Time: 7.42s
Iteration 100
Queue: [(12,60,4,True), (13,65,4,False), (14,70,4,False), (15,75,4,False), (16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,True), (22,110,2,False), (23,115,2,False)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 101
Time : 649.347s (Solving: 626.49s 1st Model: 0.00s Unsat: 3.24s)
CPU Time : 649.480s
Choices : 8672819 (Domain: 8582158)
Conflicts : 842020 (Analyzed: 842016)
Restarts : 9557 (Average: 88.10 Last: 209)
Model-Level : 98.0
Problems : 101 (Average Length: 92.89 Splits: 0)
Lemmas : 842016 (Deleted: 806414)
Binary : 10547 (Ratio: 1.25%)
Ternary : 2948 (Ratio: 0.35%)
Conflict : 842016 (Average Length: 889.1 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 842016 (Average: 8.03 Max: 598 Sum: 6758349)
Executed : 841911 (Average: 8.02 Max: 598 Sum: 6756079 Ratio: 99.97%)
Bounded : 105 (Average: 21.62 Max: 117 Sum: 2270 Ratio: 0.03%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 509407 (Eliminated: 0 Frozen: 167106)
Constraints : 3820659 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 693MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.03s
Memory: 637MB (+0MB)
UNKNOWN
Iteration Time: 7.08s
Iteration 101
Queue: [(16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,True), (22,110,2,False), (23,115,2,False)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 102
Time : 657.501s (Solving: 634.50s 1st Model: 0.00s Unsat: 3.24s)
CPU Time : 657.640s
Choices : 8773054 (Domain: 8682305)
Conflicts : 851788 (Analyzed: 851784)
Restarts : 9657 (Average: 88.20 Last: 209)
Model-Level : 98.0
Problems : 102 (Average Length: 93.13 Splits: 0)
Lemmas : 851784 (Deleted: 815156)
Binary : 10590 (Ratio: 1.24%)
Ternary : 2954 (Ratio: 0.35%)
Conflict : 851784 (Average Length: 890.4 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 851784 (Average: 8.02 Max: 598 Sum: 6830039)
Executed : 851679 (Average: 8.02 Max: 598 Sum: 6827769 Ratio: 99.97%)
Bounded : 105 (Average: 21.62 Max: 117 Sum: 2270 Ratio: 0.03%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 509407 (Eliminated: 0 Frozen: 167106)
Constraints : 3820659 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 693MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 8.10s
Memory: 637MB (+0MB)
UNKNOWN
Iteration Time: 8.16s
Iteration 102
Queue: [(20,100,2,True), (21,105,2,True), (22,110,2,False), (23,115,2,False)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 103
Time : 665.585s (Solving: 642.46s 1st Model: 0.00s Unsat: 3.24s)
CPU Time : 665.728s
Choices : 8907766 (Domain: 8816506)
Conflicts : 860500 (Analyzed: 860496)
Restarts : 9757 (Average: 88.19 Last: 209)
Model-Level : 98.0
Problems : 103 (Average Length: 93.36 Splits: 0)
Lemmas : 860496 (Deleted: 824688)
Binary : 10659 (Ratio: 1.24%)
Ternary : 2958 (Ratio: 0.34%)
Conflict : 860496 (Average Length: 892.4 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 860496 (Average: 8.05 Max: 598 Sum: 6924863)
Executed : 860391 (Average: 8.04 Max: 598 Sum: 6922593 Ratio: 99.97%)
Bounded : 105 (Average: 21.62 Max: 117 Sum: 2270 Ratio: 0.03%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 509407 (Eliminated: 0 Frozen: 167106)
Constraints : 3820659 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 693MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 8.04s
Memory: 637MB (+0MB)
UNKNOWN
Iteration Time: 8.09s
Iteration 103
Queue: [(21,105,2,True), (22,110,2,False), (23,115,2,False)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 104
Time : 674.337s (Solving: 651.11s 1st Model: 0.00s Unsat: 3.24s)
CPU Time : 674.472s
Choices : 9048449 (Domain: 8956908)
Conflicts : 870120 (Analyzed: 870116)
Restarts : 9857 (Average: 88.27 Last: 209)
Model-Level : 98.0
Problems : 104 (Average Length: 93.59 Splits: 0)
Lemmas : 870116 (Deleted: 833288)
Binary : 10688 (Ratio: 1.23%)
Ternary : 2962 (Ratio: 0.34%)
Conflict : 870116 (Average Length: 891.1 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 870116 (Average: 8.08 Max: 598 Sum: 7033092)
Executed : 870011 (Average: 8.08 Max: 598 Sum: 7030822 Ratio: 99.97%)
Bounded : 105 (Average: 21.62 Max: 117 Sum: 2270 Ratio: 0.03%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 509407 (Eliminated: 0 Frozen: 167106)
Constraints : 3820659 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 693MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 8.71s
Memory: 637MB (+0MB)
UNKNOWN
Iteration Time: 8.75s
Iteration 104
Queue: [(5,25,9,True), (6,30,8,True), (7,35,8,True), (8,40,7,True), (9,45,6,True), (10,50,6,True), (11,55,5,True), (12,60,5,True), (13,65,4,True), (14,70,4,True), (15,75,4,False), (16,80,4,False), (17,85,3,True), (18,90,3,True), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,2,True), (23,115,2,True), (24,120,0,True)]
Grounded Until: 115
Blocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 105
Time : 682.157s (Solving: 658.82s 1st Model: 0.00s Unsat: 3.24s)
CPU Time : 682.296s
Choices : 9088847 (Domain: 8997306)
Conflicts : 878437 (Analyzed: 878433)
Restarts : 9957 (Average: 88.22 Last: 209)
Model-Level : 98.0
Problems : 105 (Average Length: 93.81 Splits: 0)
Lemmas : 878433 (Deleted: 840600)
Binary : 10708 (Ratio: 1.22%)
Ternary : 2970 (Ratio: 0.34%)
Conflict : 878433 (Average Length: 893.4 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 878433 (Average: 8.04 Max: 598 Sum: 7063820)
Executed : 878328 (Average: 8.04 Max: 598 Sum: 7061550 Ratio: 99.97%)
Bounded : 105 (Average: 21.62 Max: 117 Sum: 2270 Ratio: 0.03%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 509407 (Eliminated: 0 Frozen: 167106)
Constraints : 3820659 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 693MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.78s
Memory: 637MB (+0MB)
UNKNOWN
Iteration Time: 7.83s
Iteration 105
Queue: [(6,30,8,True), (7,35,8,True), (8,40,7,True), (9,45,6,True), (10,50,6,True), (11,55,5,True), (12,60,5,True), (13,65,4,True), (14,70,4,True), (15,75,4,False), (16,80,4,False), (17,85,3,True), (18,90,3,True), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,2,True), (23,115,2,True), (24,120,0,True)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 106
Time : 690.784s (Solving: 667.33s 1st Model: 0.00s Unsat: 3.24s)
CPU Time : 690.928s
Choices : 9169703 (Domain: 9078162)
Conflicts : 887224 (Analyzed: 887220)
Restarts : 10057 (Average: 88.22 Last: 209)
Model-Level : 98.0
Problems : 106 (Average Length: 94.03 Splits: 0)
Lemmas : 887220 (Deleted: 850912)
Binary : 10755 (Ratio: 1.21%)
Ternary : 2977 (Ratio: 0.34%)
Conflict : 887220 (Average Length: 899.8 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 887220 (Average: 8.03 Max: 598 Sum: 7128050)
Executed : 887115 (Average: 8.03 Max: 598 Sum: 7125780 Ratio: 99.97%)
Bounded : 105 (Average: 21.62 Max: 117 Sum: 2270 Ratio: 0.03%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 509407 (Eliminated: 0 Frozen: 167106)
Constraints : 3820659 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 693MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 8.59s
Memory: 637MB (+0MB)
UNKNOWN
Iteration Time: 8.63s
Iteration 106
Queue: [(7,35,8,True), (8,40,7,True), (9,45,6,True), (10,50,6,True), (11,55,5,True), (12,60,5,True), (13,65,4,True), (14,70,4,True), (15,75,4,False), (16,80,4,False), (17,85,3,True), (18,90,3,True), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,2,True), (23,115,2,True), (24,120,0,True)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 107
Time : 697.206s (Solving: 673.63s 1st Model: 0.00s Unsat: 3.24s)
CPU Time : 697.352s
Choices : 9237257 (Domain: 9145693)
Conflicts : 896428 (Analyzed: 896424)
Restarts : 10157 (Average: 88.26 Last: 209)
Model-Level : 98.0
Problems : 107 (Average Length: 94.24 Splits: 0)
Lemmas : 896424 (Deleted: 859578)
Binary : 10770 (Ratio: 1.20%)
Ternary : 2992 (Ratio: 0.33%)
Conflict : 896424 (Average Length: 899.2 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 896424 (Average: 8.01 Max: 598 Sum: 7177195)
Executed : 896319 (Average: 8.00 Max: 598 Sum: 7174925 Ratio: 99.97%)
Bounded : 105 (Average: 21.62 Max: 117 Sum: 2270 Ratio: 0.03%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 509407 (Eliminated: 0 Frozen: 167106)
Constraints : 3820659 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 693MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 6.38s
Memory: 637MB (+0MB)
UNKNOWN
Iteration Time: 6.43s
Iteration 107
Queue: [(8,40,7,True), (9,45,6,True), (10,50,6,True), (11,55,5,True), (12,60,5,True), (13,65,4,True), (14,70,4,True), (15,75,4,False), (16,80,4,False), (17,85,3,True), (18,90,3,True), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,2,True), (23,115,2,True), (24,120,0,True)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 108
Time : 703.673s (Solving: 679.99s 1st Model: 0.00s Unsat: 3.24s)
CPU Time : 703.820s
Choices : 9324950 (Domain: 9232778)
Conflicts : 905813 (Analyzed: 905809)
Restarts : 10257 (Average: 88.31 Last: 209)
Model-Level : 98.0
Problems : 108 (Average Length: 94.45 Splits: 0)
Lemmas : 905809 (Deleted: 868464)
Binary : 10867 (Ratio: 1.20%)
Ternary : 3012 (Ratio: 0.33%)
Conflict : 905809 (Average Length: 899.2 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 905809 (Average: 7.99 Max: 598 Sum: 7238615)
Executed : 905704 (Average: 7.99 Max: 598 Sum: 7236345 Ratio: 99.97%)
Bounded : 105 (Average: 21.62 Max: 117 Sum: 2270 Ratio: 0.03%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 509407 (Eliminated: 0 Frozen: 167106)
Constraints : 3820659 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 693MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 6.43s
Memory: 637MB (+0MB)
UNKNOWN
Iteration Time: 6.47s
Iteration 108
Queue: [(9,45,6,True), (10,50,6,True), (11,55,5,True), (12,60,5,True), (13,65,4,True), (14,70,4,True), (15,75,4,False), (16,80,4,False), (17,85,3,True), (18,90,3,True), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,2,True), (23,115,2,True), (24,120,0,True)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 109
Time : 710.612s (Solving: 686.81s 1st Model: 0.00s Unsat: 3.24s)
CPU Time : 710.764s
Choices : 9406404 (Domain: 9313484)
Conflicts : 914641 (Analyzed: 914637)
Restarts : 10357 (Average: 88.31 Last: 209)
Model-Level : 98.0
Problems : 109 (Average Length: 94.66 Splits: 0)
Lemmas : 914637 (Deleted: 877698)
Binary : 10924 (Ratio: 1.19%)
Ternary : 3024 (Ratio: 0.33%)
Conflict : 914637 (Average Length: 900.3 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 914637 (Average: 7.98 Max: 598 Sum: 7295608)
Executed : 914532 (Average: 7.97 Max: 598 Sum: 7293338 Ratio: 99.97%)
Bounded : 105 (Average: 21.62 Max: 117 Sum: 2270 Ratio: 0.03%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 509407 (Eliminated: 0 Frozen: 167106)
Constraints : 3820659 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 693MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 6.90s
Memory: 637MB (+0MB)
UNKNOWN
Iteration Time: 6.94s
Iteration 109
Queue: [(10,50,6,True), (11,55,5,True), (12,60,5,True), (13,65,4,True), (14,70,4,True), (15,75,4,False), (16,80,4,False), (17,85,3,True), (18,90,3,True), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,2,True), (23,115,2,True), (24,120,0,True)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 110
Time : 717.137s (Solving: 693.20s 1st Model: 0.00s Unsat: 3.24s)
CPU Time : 717.292s
Choices : 9492711 (Domain: 9399462)
Conflicts : 923033 (Analyzed: 923029)
Restarts : 10457 (Average: 88.27 Last: 209)
Model-Level : 98.0
Problems : 110 (Average Length: 94.86 Splits: 0)
Lemmas : 923029 (Deleted: 884219)
Binary : 10988 (Ratio: 1.19%)
Ternary : 3035 (Ratio: 0.33%)
Conflict : 923029 (Average Length: 899.3 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 923029 (Average: 7.97 Max: 598 Sum: 7355043)
Executed : 922924 (Average: 7.97 Max: 598 Sum: 7352773 Ratio: 99.97%)
Bounded : 105 (Average: 21.62 Max: 117 Sum: 2270 Ratio: 0.03%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 509407 (Eliminated: 0 Frozen: 167106)
Constraints : 3820659 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 693MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 6.48s
Memory: 637MB (+0MB)
UNKNOWN
Iteration Time: 6.53s
Iteration 110
Queue: [(11,55,5,True), (12,60,5,True), (13,65,4,True), (14,70,4,True), (15,75,4,False), (16,80,4,False), (17,85,3,True), (18,90,3,True), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,2,True), (23,115,2,True), (24,120,0,True)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 111
Time : 723.863s (Solving: 699.81s 1st Model: 0.00s Unsat: 3.24s)
CPU Time : 724.020s
Choices : 9560666 (Domain: 9467416)
Conflicts : 931976 (Analyzed: 931972)
Restarts : 10557 (Average: 88.28 Last: 209)
Model-Level : 98.0
Problems : 111 (Average Length: 95.06 Splits: 0)
Lemmas : 931972 (Deleted: 894605)
Binary : 10997 (Ratio: 1.18%)
Ternary : 3039 (Ratio: 0.33%)
Conflict : 931972 (Average Length: 898.0 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 931972 (Average: 7.94 Max: 598 Sum: 7402269)
Executed : 931867 (Average: 7.94 Max: 598 Sum: 7399999 Ratio: 99.97%)
Bounded : 105 (Average: 21.62 Max: 117 Sum: 2270 Ratio: 0.03%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 509407 (Eliminated: 0 Frozen: 167106)
Constraints : 3820659 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 693MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 6.68s
Memory: 637MB (+0MB)
UNKNOWN
Iteration Time: 6.73s
Iteration 111
Queue: [(12,60,5,True), (13,65,4,True), (14,70,4,True), (15,75,4,False), (16,80,4,False), (17,85,3,True), (18,90,3,True), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,2,True), (23,115,2,True), (24,120,0,True)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 112
Time : 730.417s (Solving: 706.26s 1st Model: 0.00s Unsat: 3.24s)
CPU Time : 730.576s
Choices : 9653777 (Domain: 9560405)
Conflicts : 940589 (Analyzed: 940585)
Restarts : 10657 (Average: 88.26 Last: 209)
Model-Level : 98.0
Problems : 112 (Average Length: 95.26 Splits: 0)
Lemmas : 940585 (Deleted: 903332)
Binary : 11072 (Ratio: 1.18%)
Ternary : 3052 (Ratio: 0.32%)
Conflict : 940585 (Average Length: 897.3 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 940585 (Average: 7.94 Max: 598 Sum: 7466352)
Executed : 940480 (Average: 7.94 Max: 598 Sum: 7464082 Ratio: 99.97%)
Bounded : 105 (Average: 21.62 Max: 117 Sum: 2270 Ratio: 0.03%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 509407 (Eliminated: 0 Frozen: 167106)
Constraints : 3820659 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 693MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 6.52s
Memory: 637MB (+0MB)
UNKNOWN
Iteration Time: 6.56s
Iteration 112
Queue: [(13,65,4,True), (14,70,4,True), (15,75,4,False), (16,80,4,False), (17,85,3,True), (18,90,3,True), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,2,True), (23,115,2,True), (24,120,0,True)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 113
Time : 737.751s (Solving: 713.46s 1st Model: 0.00s Unsat: 3.24s)
CPU Time : 737.912s
Choices : 9729101 (Domain: 9635729)
Conflicts : 950263 (Analyzed: 950259)
Restarts : 10757 (Average: 88.34 Last: 209)
Model-Level : 98.0
Problems : 113 (Average Length: 95.45 Splits: 0)
Lemmas : 950259 (Deleted: 911802)
Binary : 11079 (Ratio: 1.17%)
Ternary : 3053 (Ratio: 0.32%)
Conflict : 950259 (Average Length: 895.9 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 950259 (Average: 7.91 Max: 598 Sum: 7519681)
Executed : 950154 (Average: 7.91 Max: 598 Sum: 7517411 Ratio: 99.97%)
Bounded : 105 (Average: 21.62 Max: 117 Sum: 2270 Ratio: 0.03%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 509407 (Eliminated: 0 Frozen: 167106)
Constraints : 3820659 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 693MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.29s
Memory: 637MB (+0MB)
UNKNOWN
Iteration Time: 7.34s
Iteration 113
Queue: [(14,70,4,True), (15,75,4,False), (16,80,4,False), (17,85,3,True), (18,90,3,True), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,2,True), (23,115,2,True), (24,120,0,True)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 114
Time : 745.092s (Solving: 720.67s 1st Model: 0.00s Unsat: 3.24s)
CPU Time : 745.256s
Choices : 9868124 (Domain: 9773698)
Conflicts : 959263 (Analyzed: 959259)
Restarts : 10857 (Average: 88.35 Last: 209)
Model-Level : 98.0
Problems : 114 (Average Length: 95.64 Splits: 0)
Lemmas : 959259 (Deleted: 921185)
Binary : 11197 (Ratio: 1.17%)
Ternary : 3072 (Ratio: 0.32%)
Conflict : 959259 (Average Length: 896.8 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 959259 (Average: 7.95 Max: 598 Sum: 7621725)
Executed : 959154 (Average: 7.94 Max: 598 Sum: 7619455 Ratio: 99.97%)
Bounded : 105 (Average: 21.62 Max: 117 Sum: 2270 Ratio: 0.03%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 509407 (Eliminated: 0 Frozen: 167106)
Constraints : 3820659 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 693MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.30s
Memory: 637MB (+0MB)
UNKNOWN
Iteration Time: 7.35s
Iteration 114
Queue: [(17,85,3,True), (18,90,3,True), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,2,True), (23,115,2,True), (24,120,0,True)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 115
Time : 752.539s (Solving: 727.98s 1st Model: 0.00s Unsat: 3.24s)
CPU Time : 752.704s
Choices : 9987879 (Domain: 9893217)
Conflicts : 968347 (Analyzed: 968343)
Restarts : 10957 (Average: 88.38 Last: 209)
Model-Level : 98.0
Problems : 115 (Average Length: 95.83 Splits: 0)
Lemmas : 968343 (Deleted: 929943)
Binary : 11273 (Ratio: 1.16%)
Ternary : 3088 (Ratio: 0.32%)
Conflict : 968343 (Average Length: 897.6 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 968343 (Average: 7.96 Max: 598 Sum: 7710797)
Executed : 968238 (Average: 7.96 Max: 598 Sum: 7708527 Ratio: 99.97%)
Bounded : 105 (Average: 21.62 Max: 117 Sum: 2270 Ratio: 0.03%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 509407 (Eliminated: 0 Frozen: 167106)
Constraints : 3820659 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 693MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.39s
Memory: 637MB (+0MB)
UNKNOWN
Iteration Time: 7.45s
Iteration 115
Queue: [(18,90,3,True), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,2,True), (23,115,2,True), (24,120,0,True)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 116
Time : 761.267s (Solving: 736.58s 1st Model: 0.00s Unsat: 3.24s)
CPU Time : 761.436s
Choices : 10208715 (Domain: 10111874)
Conflicts : 978170 (Analyzed: 978166)
Restarts : 11057 (Average: 88.47 Last: 209)
Model-Level : 98.0
Problems : 116 (Average Length: 96.01 Splits: 0)
Lemmas : 978166 (Deleted: 938620)
Binary : 11427 (Ratio: 1.17%)
Ternary : 3123 (Ratio: 0.32%)
Conflict : 978166 (Average Length: 896.5 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 978166 (Average: 8.07 Max: 598 Sum: 7892595)
Executed : 978061 (Average: 8.07 Max: 598 Sum: 7890325 Ratio: 99.97%)
Bounded : 105 (Average: 21.62 Max: 117 Sum: 2270 Ratio: 0.03%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 509407 (Eliminated: 0 Frozen: 167106)
Constraints : 3820659 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 693MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 8.68s
Memory: 637MB (+0MB)
UNKNOWN
Iteration Time: 8.73s
Iteration 116
Queue: [(22,110,2,True), (23,115,2,True), (24,120,0,True)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 117
Time : 769.067s (Solving: 744.27s 1st Model: 0.00s Unsat: 3.24s)
CPU Time : 769.240s
Choices : 10332477 (Domain: 10235472)
Conflicts : 986501 (Analyzed: 986497)
Restarts : 11157 (Average: 88.42 Last: 209)
Model-Level : 98.0
Problems : 117 (Average Length: 96.19 Splits: 0)
Lemmas : 986497 (Deleted: 946109)
Binary : 11456 (Ratio: 1.16%)
Ternary : 3129 (Ratio: 0.32%)
Conflict : 986497 (Average Length: 896.5 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 986497 (Average: 8.09 Max: 598 Sum: 7980321)
Executed : 986392 (Average: 8.09 Max: 598 Sum: 7978051 Ratio: 99.97%)
Bounded : 105 (Average: 21.62 Max: 117 Sum: 2270 Ratio: 0.03%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 509407 (Eliminated: 0 Frozen: 167106)
Constraints : 3820659 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 693MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.76s
Memory: 637MB (+0MB)
UNKNOWN
Iteration Time: 7.81s
Iteration 117
Queue: [(23,115,2,True), (24,120,0,True)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 118
Time : 778.884s (Solving: 753.98s 1st Model: 0.00s Unsat: 3.24s)
CPU Time : 779.060s
Choices : 10591180 (Domain: 10492807)
Conflicts : 995348 (Analyzed: 995344)
Restarts : 11257 (Average: 88.42 Last: 209)
Model-Level : 98.0
Problems : 118 (Average Length: 96.36 Splits: 0)
Lemmas : 995344 (Deleted: 956302)
Binary : 11614 (Ratio: 1.17%)
Ternary : 3179 (Ratio: 0.32%)
Conflict : 995344 (Average Length: 898.6 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 995344 (Average: 8.23 Max: 621 Sum: 8196266)
Executed : 995239 (Average: 8.23 Max: 621 Sum: 8193996 Ratio: 99.97%)
Bounded : 105 (Average: 21.62 Max: 117 Sum: 2270 Ratio: 0.03%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 509407 (Eliminated: 0 Frozen: 167106)
Constraints : 3820659 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 693MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 9.78s
Memory: 637MB (+0MB)
UNKNOWN
Iteration Time: 9.82s
Iteration 118
Queue: [(24,120,0,True)]
Grounded Until: 115
Expected Memory: 687.0MB
Grounding... [('step', [116]), ('step', [117]), ('step', [118]), ('step', [119]), ('step', [120]), ('check', [120])]
Grounding Time: 0.33s
Memory: 637MB (+0MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 119
Time : 788.406s (Solving: 762.75s 1st Model: 0.00s Unsat: 3.24s)
CPU Time : 788.584s
Choices : 10756833 (Domain: 10658059)
Conflicts : 1004893 (Analyzed: 1004889)
Restarts : 11357 (Average: 88.48 Last: 209)
Model-Level : 98.0
Problems : 119 (Average Length: 96.58 Splits: 0)
Lemmas : 1004889 (Deleted: 964837)
Binary : 11662 (Ratio: 1.16%)
Ternary : 3192 (Ratio: 0.32%)
Conflict : 1004889 (Average Length: 897.7 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 1004889 (Average: 8.28 Max: 621 Sum: 8321660)
Executed : 1004784 (Average: 8.28 Max: 621 Sum: 8319390 Ratio: 99.97%)
Bounded : 105 (Average: 21.62 Max: 117 Sum: 2270 Ratio: 0.03%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 531983 (Eliminated: 0 Frozen: 174571)
Constraints : 3993704 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 714MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 8.88s
Memory: 652MB (+15MB)
UNKNOWN
Iteration Time: 9.54s
Iteration 119
Queue: [(5,25,10,True), (6,30,9,True), (7,35,9,True), (8,40,8,True), (9,45,7,True), (10,50,7,False), (11,55,6,True), (12,60,6,False), (13,65,5,True), (14,70,5,False), (15,75,4,True), (16,80,4,False), (17,85,4,False), (18,90,4,False), (19,95,3,True), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,3,False), (24,120,1,True)]
Grounded Until: 120
Blocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 120
Time : 794.901s (Solving: 769.13s 1st Model: 0.00s Unsat: 3.24s)
CPU Time : 795.084s
Choices : 10794030 (Domain: 10695256)
Conflicts : 1012662 (Analyzed: 1012658)
Restarts : 11457 (Average: 88.39 Last: 209)
Model-Level : 98.0
Problems : 120 (Average Length: 96.79 Splits: 0)
Lemmas : 1012658 (Deleted: 972102)
Binary : 11719 (Ratio: 1.16%)
Ternary : 3207 (Ratio: 0.32%)
Conflict : 1012658 (Average Length: 898.3 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 1012658 (Average: 8.25 Max: 621 Sum: 8350565)
Executed : 1012553 (Average: 8.24 Max: 621 Sum: 8348295 Ratio: 99.97%)
Bounded : 105 (Average: 21.62 Max: 117 Sum: 2270 Ratio: 0.03%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 531983 (Eliminated: 0 Frozen: 174571)
Constraints : 3993704 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 714MB
Max. Length : 120 steps
Models : 1
[endof: stats after solve call]
Solving Time: 6.46s
Memory: 660MB (+8MB)
UNKNOWN
Iteration Time: 6.50s
Iteration 120
Queue: [(6,30,9,True), (7,35,9,True), (8,40,8,True), (9,45,7,True), (10,50,7,False), (11,55,6,True), (12,60,6,False), (13,65,5,True), (14,70,5,False), (15,75,4,True), (16,80,4,False), (17,85,4,False), (18,90,4,False), (19,95,3,True), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,3,False), (24,120,1,True)]
Grounded Until: 120
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 121
Time : 801.398s (Solving: 775.49s 1st Model: 0.00s Unsat: 3.24s)
CPU Time : 801.580s
Choices : 10861487 (Domain: 10762713)
Conflicts : 1021189 (Analyzed: 1021185)
Restarts : 11557 (Average: 88.36 Last: 209)
Model-Level : 98.0
Problems : 121 (Average Length: 97.00 Splits: 0)
Lemmas : 1021185 (Deleted: 980005)
Binary : 11744 (Ratio: 1.15%)
Ternary : 3210 (Ratio: 0.31%)
Conflict : 1021185 (Average Length: 899.3 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 1021185 (Average: 8.23 Max: 621 Sum: 8400408)
Executed : 1021080 (Average: 8.22 Max: 621 Sum: 8398138 Ratio: 99.97%)
Bounded : 105 (Average: 21.62 Max: 117 Sum: 2270 Ratio: 0.03%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 531983 (Eliminated: 0 Frozen: 174571)
Constraints : 3993704 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 714MB
Max. Length : 120 steps
Models : 1
[endof: stats after solve call]
Solving Time: 6.45s
Memory: 660MB (+0MB)
UNKNOWN
Iteration Time: 6.50s
Iteration 121
Queue: [(7,35,9,True), (8,40,8,True), (9,45,7,True), (10,50,7,False), (11,55,6,True), (12,60,6,False), (13,65,5,True), (14,70,5,False), (15,75,4,True), (16,80,4,False), (17,85,4,False), (18,90,4,False), (19,95,3,True), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,3,False), (24,120,1,True)]
Grounded Until: 120
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 122
Time : 807.266s (Solving: 781.25s 1st Model: 0.00s Unsat: 3.24s)
CPU Time : 807.452s
Choices : 10933201 (Domain: 10834124)
Conflicts : 1030048 (Analyzed: 1030044)
Restarts : 11657 (Average: 88.36 Last: 209)
Model-Level : 98.0
Problems : 122 (Average Length: 97.20 Splits: 0)
Lemmas : 1030044 (Deleted: 990148)
Binary : 11795 (Ratio: 1.15%)
Ternary : 3227 (Ratio: 0.31%)
Conflict : 1030044 (Average Length: 897.4 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 1030044 (Average: 8.21 Max: 621 Sum: 8453541)
Executed : 1029938 (Average: 8.20 Max: 621 Sum: 8451149 Ratio: 99.97%)
Bounded : 106 (Average: 22.57 Max: 122 Sum: 2392 Ratio: 0.03%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 531983 (Eliminated: 0 Frozen: 174571)
Constraints : 3993704 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 714MB
Max. Length : 120 steps
Models : 1
[endof: stats after solve call]
Solving Time: 5.83s
Memory: 660MB (+0MB)
UNKNOWN
Iteration Time: 5.87s
Iteration 122
Queue: [(8,40,8,True), (9,45,7,True), (10,50,7,False), (11,55,6,True), (12,60,6,False), (13,65,5,True), (14,70,5,False), (15,75,4,True), (16,80,4,False), (17,85,4,False), (18,90,4,False), (19,95,3,True), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,3,False), (24,120,1,True)]
Grounded Until: 120
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 123
Time : 814.071s (Solving: 787.94s 1st Model: 0.00s Unsat: 3.24s)
CPU Time : 814.256s
Choices : 11016430 (Domain: 10916879)
Conflicts : 1039087 (Analyzed: 1039083)
Restarts : 11757 (Average: 88.38 Last: 209)
Model-Level : 98.0
Problems : 123 (Average Length: 97.41 Splits: 0)
Lemmas : 1039083 (Deleted: 998725)
Binary : 11909 (Ratio: 1.15%)
Ternary : 3243 (Ratio: 0.31%)
Conflict : 1039083 (Average Length: 896.7 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 1039083 (Average: 8.19 Max: 621 Sum: 8509339)
Executed : 1038977 (Average: 8.19 Max: 621 Sum: 8506947 Ratio: 99.97%)
Bounded : 106 (Average: 22.57 Max: 122 Sum: 2392 Ratio: 0.03%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 531983 (Eliminated: 0 Frozen: 174571)
Constraints : 3993690 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 714MB
Max. Length : 120 steps
Models : 1
[endof: stats after solve call]
Solving Time: 6.77s
Memory: 660MB (+0MB)
UNKNOWN
Iteration Time: 6.81s
Iteration 123
Queue: [(9,45,7,True), (10,50,7,False), (11,55,6,True), (12,60,6,False), (13,65,5,True), (14,70,5,False), (15,75,4,True), (16,80,4,False), (17,85,4,False), (18,90,4,False), (19,95,3,True), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,3,False), (24,120,1,True)]
Grounded Until: 120
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 124
Time : 820.798s (Solving: 794.56s 1st Model: 0.00s Unsat: 3.24s)
CPU Time : 820.988s
Choices : 11095686 (Domain: 10995917)
Conflicts : 1048524 (Analyzed: 1048520)
Restarts : 11857 (Average: 88.43 Last: 209)
Model-Level : 98.0
Problems : 124 (Average Length: 97.60 Splits: 0)
Lemmas : 1048520 (Deleted: 1007552)
Binary : 11961 (Ratio: 1.14%)
Ternary : 3251 (Ratio: 0.31%)
Conflict : 1048520 (Average Length: 895.6 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 1048520 (Average: 8.17 Max: 621 Sum: 8566605)
Executed : 1048414 (Average: 8.17 Max: 621 Sum: 8564213 Ratio: 99.97%)
Bounded : 106 (Average: 22.57 Max: 122 Sum: 2392 Ratio: 0.03%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 531983 (Eliminated: 0 Frozen: 174571)
Constraints : 3993690 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 714MB
Max. Length : 120 steps
Models : 1
[endof: stats after solve call]
Solving Time: 6.69s
Memory: 660MB (+0MB)
UNKNOWN
Iteration Time: 6.73s
Iteration 124
Queue: [(11,55,6,True), (12,60,6,False), (13,65,5,True), (14,70,5,False), (15,75,4,True), (16,80,4,False), (17,85,4,False), (18,90,4,False), (19,95,3,True), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,3,False), (24,120,1,True)]
Grounded Until: 120
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 125
Time : 827.886s (Solving: 801.52s 1st Model: 0.00s Unsat: 3.24s)
CPU Time : 828.080s
Choices : 11167778 (Domain: 11068004)
Conflicts : 1057546 (Analyzed: 1057542)
Restarts : 11957 (Average: 88.45 Last: 209)
Model-Level : 98.0
Problems : 125 (Average Length: 97.80 Splits: 0)
Lemmas : 1057542 (Deleted: 1016840)
Binary : 11993 (Ratio: 1.13%)
Ternary : 3254 (Ratio: 0.31%)
Conflict : 1057542 (Average Length: 895.6 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 1057542 (Average: 8.15 Max: 621 Sum: 8615159)
Executed : 1057436 (Average: 8.14 Max: 621 Sum: 8612767 Ratio: 99.97%)
Bounded : 106 (Average: 22.57 Max: 122 Sum: 2392 Ratio: 0.03%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 531983 (Eliminated: 0 Frozen: 174571)
Constraints : 3993690 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 714MB
Max. Length : 120 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.05s
Memory: 660MB (+0MB)
UNKNOWN
Iteration Time: 7.09s
Iteration 125
Queue: [(13,65,5,True), (14,70,5,False), (15,75,4,True), (16,80,4,False), (17,85,4,False), (18,90,4,False), (19,95,3,True), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,3,False), (24,120,1,True)]
Grounded Until: 120
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 126
Time : 835.353s (Solving: 808.85s 1st Model: 0.00s Unsat: 3.24s)
CPU Time : 835.552s
Choices : 11256395 (Domain: 11156524)
Conflicts : 1066835 (Analyzed: 1066831)
Restarts : 12057 (Average: 88.48 Last: 209)
Model-Level : 98.0
Problems : 126 (Average Length: 97.99 Splits: 0)
Lemmas : 1066831 (Deleted: 1025683)
Binary : 12042 (Ratio: 1.13%)
Ternary : 3262 (Ratio: 0.31%)
Conflict : 1066831 (Average Length: 896.0 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 1066831 (Average: 8.13 Max: 621 Sum: 8677006)
Executed : 1066725 (Average: 8.13 Max: 621 Sum: 8674614 Ratio: 99.97%)
Bounded : 106 (Average: 22.57 Max: 122 Sum: 2392 Ratio: 0.03%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 531983 (Eliminated: 0 Frozen: 174571)
Constraints : 3993690 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 714MB
Max. Length : 120 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.42s
Memory: 660MB (+0MB)
UNKNOWN
Iteration Time: 7.47s
Iteration 126
Queue: [(15,75,4,True), (16,80,4,False), (17,85,4,False), (18,90,4,False), (19,95,3,True), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,3,False), (24,120,1,True)]
Grounded Until: 120
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 127
Time : 842.955s (Solving: 816.34s 1st Model: 0.00s Unsat: 3.24s)
CPU Time : 843.156s
Choices : 11332429 (Domain: 11232556)
Conflicts : 1076242 (Analyzed: 1076238)
Restarts : 12157 (Average: 88.53 Last: 209)
Model-Level : 98.0
Problems : 127 (Average Length: 98.18 Splits: 0)
Lemmas : 1076238 (Deleted: 1034857)
Binary : 12057 (Ratio: 1.12%)
Ternary : 3264 (Ratio: 0.30%)
Conflict : 1076238 (Average Length: 895.1 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 1076238 (Average: 8.11 Max: 621 Sum: 8728421)
Executed : 1076132 (Average: 8.11 Max: 621 Sum: 8726029 Ratio: 99.97%)
Bounded : 106 (Average: 22.57 Max: 122 Sum: 2392 Ratio: 0.03%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 531983 (Eliminated: 0 Frozen: 174571)
Constraints : 3993690 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 714MB
Max. Length : 120 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.56s
Memory: 660MB (+0MB)
UNKNOWN
Iteration Time: 7.61s
Iteration 127
Queue: [(19,95,3,True), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,3,False), (24,120,1,True)]
Grounded Until: 120
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 128
Time : 851.375s (Solving: 824.65s 1st Model: 0.00s Unsat: 3.24s)
CPU Time : 851.580s
Choices : 11418690 (Domain: 11318811)
Conflicts : 1085981 (Analyzed: 1085977)
Restarts : 12257 (Average: 88.60 Last: 209)
Model-Level : 98.0
Problems : 128 (Average Length: 98.37 Splits: 0)
Lemmas : 1085977 (Deleted: 1044115)
Binary : 12067 (Ratio: 1.11%)
Ternary : 3267 (Ratio: 0.30%)
Conflict : 1085977 (Average Length: 893.7 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 1085977 (Average: 8.09 Max: 621 Sum: 8784369)
Executed : 1085871 (Average: 8.09 Max: 621 Sum: 8781977 Ratio: 99.97%)
Bounded : 106 (Average: 22.57 Max: 122 Sum: 2392 Ratio: 0.03%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 531983 (Eliminated: 0 Frozen: 174571)
Constraints : 3993690 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 714MB
Max. Length : 120 steps
Models : 1
[endof: stats after solve call]
Solving Time: 8.38s
Memory: 660MB (+0MB)
UNKNOWN
Iteration Time: 8.43s
Iteration 128
Queue: [(24,120,1,True)]
Grounded Until: 120
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 129
Time : 860.086s (Solving: 833.24s 1st Model: 0.00s Unsat: 3.24s)
CPU Time : 860.292s
Choices : 11582859 (Domain: 11482745)
Conflicts : 1095605 (Analyzed: 1095601)
Restarts : 12357 (Average: 88.66 Last: 209)
Model-Level : 98.0
Problems : 129 (Average Length: 98.55 Splits: 0)
Lemmas : 1095601 (Deleted: 1053678)
Binary : 12156 (Ratio: 1.11%)
Ternary : 3281 (Ratio: 0.30%)
Conflict : 1095601 (Average Length: 891.9 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 1095601 (Average: 8.13 Max: 621 Sum: 8907162)
Executed : 1095495 (Average: 8.13 Max: 621 Sum: 8904770 Ratio: 99.97%)
Bounded : 106 (Average: 22.57 Max: 122 Sum: 2392 Ratio: 0.03%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 531983 (Eliminated: 0 Frozen: 174571)
Constraints : 3993690 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 714MB
Max. Length : 120 steps
Models : 1
[endof: stats after solve call]
Solving Time: 8.68s
Memory: 660MB (+0MB)
UNKNOWN
Iteration Time: 8.72s
Iteration 129
Queue: [(5,25,11,True), (6,30,10,True), (7,35,10,True), (8,40,9,True), (9,45,8,True), (10,50,7,True), (11,55,7,False), (12,60,6,True), (13,65,6,False), (14,70,5,True), (15,75,5,False), (16,80,4,True), (17,85,4,False), (18,90,4,False), (19,95,4,False), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,3,False), (24,120,2,True)]
Grounded Until: 120
Blocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 130
Time : 868.250s (Solving: 841.29s 1st Model: 0.00s Unsat: 3.24s)
CPU Time : 868.460s
Choices : 11637484 (Domain: 11537370)
Conflicts : 1104162 (Analyzed: 1104158)
Restarts : 12457 (Average: 88.64 Last: 209)
Model-Level : 98.0
Problems : 130 (Average Length: 98.73 Splits: 0)
Lemmas : 1104158 (Deleted: 1060938)
Binary : 12202 (Ratio: 1.11%)
Ternary : 3287 (Ratio: 0.30%)
Conflict : 1104158 (Average Length: 895.9 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 1104158 (Average: 8.10 Max: 621 Sum: 8948562)
Executed : 1104052 (Average: 8.10 Max: 621 Sum: 8946170 Ratio: 99.97%)
Bounded : 106 (Average: 22.57 Max: 122 Sum: 2392 Ratio: 0.03%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 531983 (Eliminated: 0 Frozen: 174571)
Constraints : 3993690 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 714MB
Max. Length : 120 steps
Models : 1
[endof: stats after solve call]
Solving Time: 8.13s
Memory: 660MB (+0MB)
UNKNOWN
Iteration Time: 8.17s
Iteration 130
Queue: [(6,30,10,True), (7,35,10,True), (8,40,9,True), (9,45,8,True), (10,50,7,True), (11,55,7,False), (12,60,6,True), (13,65,6,False), (14,70,5,True), (15,75,5,False), (16,80,4,True), (17,85,4,False), (18,90,4,False), (19,95,4,False), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,3,False), (24,120,2,True)]
Grounded Until: 120
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 131
Time : 875.025s (Solving: 847.95s 1st Model: 0.00s Unsat: 3.24s)
CPU Time : 875.240s
Choices : 11701739 (Domain: 11601625)
Conflicts : 1113302 (Analyzed: 1113298)
Restarts : 12557 (Average: 88.66 Last: 209)
Model-Level : 98.0
Problems : 131 (Average Length: 98.91 Splits: 0)
Lemmas : 1113298 (Deleted: 1071517)
Binary : 12220 (Ratio: 1.10%)
Ternary : 3293 (Ratio: 0.30%)
Conflict : 1113298 (Average Length: 896.7 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 1113298 (Average: 8.08 Max: 621 Sum: 8995364)
Executed : 1113192 (Average: 8.08 Max: 621 Sum: 8992972 Ratio: 99.97%)
Bounded : 106 (Average: 22.57 Max: 122 Sum: 2392 Ratio: 0.03%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 531983 (Eliminated: 0 Frozen: 174571)
Constraints : 3993690 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 714MB
Max. Length : 120 steps
Models : 1
[endof: stats after solve call]
Solving Time: 6.74s
Memory: 660MB (+0MB)
UNKNOWN
Iteration Time: 6.78s
Iteration 131
Queue: [(7,35,10,True), (8,40,9,True), (9,45,8,True), (10,50,7,True), (11,55,7,False), (12,60,6,True), (13,65,6,False), (14,70,5,True), (15,75,5,False), (16,80,4,True), (17,85,4,False), (18,90,4,False), (19,95,4,False), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,3,False), (24,120,2,True)]
Grounded Until: 120
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 132
Time : 880.473s (Solving: 853.28s 1st Model: 0.00s Unsat: 3.24s)
CPU Time : 880.692s
Choices : 11768250 (Domain: 11667804)
Conflicts : 1122005 (Analyzed: 1122001)
Restarts : 12657 (Average: 88.65 Last: 209)
Model-Level : 98.0
Problems : 132 (Average Length: 99.08 Splits: 0)
Lemmas : 1122001 (Deleted: 1080484)
Binary : 12272 (Ratio: 1.09%)
Ternary : 3305 (Ratio: 0.29%)
Conflict : 1122001 (Average Length: 894.9 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 1122001 (Average: 8.06 Max: 621 Sum: 9040899)
Executed : 1121895 (Average: 8.06 Max: 621 Sum: 9038507 Ratio: 99.97%)
Bounded : 106 (Average: 22.57 Max: 122 Sum: 2392 Ratio: 0.03%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 531983 (Eliminated: 0 Frozen: 174571)
Constraints : 3993690 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 714MB
Max. Length : 120 steps
Models : 1
[endof: stats after solve call]
Solving Time: 5.41s
Memory: 660MB (+0MB)
UNKNOWN
Iteration Time: 5.45s
Iteration 132
Queue: [(8,40,9,True), (9,45,8,True), (10,50,7,True), (11,55,7,False), (12,60,6,True), (13,65,6,False), (14,70,5,True), (15,75,5,False), (16,80,4,True), (17,85,4,False), (18,90,4,False), (19,95,4,False), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,3,False), (24,120,2,True)]
Grounded Until: 120
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 133
Time : 886.826s (Solving: 859.52s 1st Model: 0.00s Unsat: 3.24s)
CPU Time : 887.048s
Choices : 11828155 (Domain: 11727709)
Conflicts : 1131072 (Analyzed: 1131068)
Restarts : 12757 (Average: 88.66 Last: 209)
Model-Level : 98.0
Problems : 133 (Average Length: 99.26 Splits: 0)
Lemmas : 1131068 (Deleted: 1089023)
Binary : 12282 (Ratio: 1.09%)
Ternary : 3307 (Ratio: 0.29%)
Conflict : 1131068 (Average Length: 893.4 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 1131068 (Average: 8.03 Max: 621 Sum: 9082345)
Executed : 1130962 (Average: 8.03 Max: 621 Sum: 9079953 Ratio: 99.97%)
Bounded : 106 (Average: 22.57 Max: 122 Sum: 2392 Ratio: 0.03%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 531983 (Eliminated: 0 Frozen: 174571)
Constraints : 3993690 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 714MB
Max. Length : 120 steps
Models : 1
[endof: stats after solve call]
Solving Time: 6.31s
Memory: 660MB (+0MB)
UNKNOWN
Iteration Time: 6.36s
Iteration 133
Queue: [(9,45,8,True), (10,50,7,True), (11,55,7,False), (12,60,6,True), (13,65,6,False), (14,70,5,True), (15,75,5,False), (16,80,4,True), (17,85,4,False), (18,90,4,False), (19,95,4,False), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,3,False), (24,120,2,True)]
Grounded Until: 120
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 134
Time : 893.017s (Solving: 865.58s 1st Model: 0.00s Unsat: 3.24s)
CPU Time : 893.240s
Choices : 11897743 (Domain: 11797252)
Conflicts : 1139499 (Analyzed: 1139495)
Restarts : 12857 (Average: 88.63 Last: 209)
Model-Level : 98.0
Problems : 134 (Average Length: 99.43 Splits: 0)
Lemmas : 1139495 (Deleted: 1095816)
Binary : 12306 (Ratio: 1.08%)
Ternary : 3312 (Ratio: 0.29%)
Conflict : 1139495 (Average Length: 892.9 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 1139495 (Average: 8.01 Max: 621 Sum: 9128988)
Executed : 1139389 (Average: 8.01 Max: 621 Sum: 9126596 Ratio: 99.97%)
Bounded : 106 (Average: 22.57 Max: 122 Sum: 2392 Ratio: 0.03%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 531983 (Eliminated: 0 Frozen: 174571)
Constraints : 3993690 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 714MB
Max. Length : 120 steps
Models : 1
[endof: stats after solve call]
Solving Time: 6.14s
Memory: 660MB (+0MB)
UNKNOWN
Iteration Time: 6.20s
Iteration 134
Queue: [(10,50,7,True), (11,55,7,False), (12,60,6,True), (13,65,6,False), (14,70,5,True), (15,75,5,False), (16,80,4,True), (17,85,4,False), (18,90,4,False), (19,95,4,False), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,3,False), (24,120,2,True)]
Grounded Until: 120
Unblocking actions...
Solving...
*** Info : (planner): INTERRUPTED by signal!
UNKNOWN
INTERRUPTED : 1
Models : 0+
Calls : 135
Time : 899.864s (Solving: 872.31s 1st Model: 0.00s Unsat: 3.24s)
CPU Time : 900.068s
Choices : 11961894 (Domain: 11861397)
Conflicts : 1148750 (Analyzed: 1148746)
Restarts : 12957 (Average: 88.66 Last: 209)
Model-Level : 98.0
Problems : 135 (Average Length: 99.59 Splits: 0)
Lemmas : 1148746 (Deleted: 1106280)
Binary : 12316 (Ratio: 1.07%)
Ternary : 3315 (Ratio: 0.29%)
Conflict : 1148746 (Average Length: 893.1 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 1148746 (Average: 7.98 Max: 621 Sum: 9172421)
Executed : 1148640 (Average: 7.98 Max: 621 Sum: 9170029 Ratio: 99.97%)
Bounded : 106 (Average: 22.57 Max: 122 Sum: 2392 Ratio: 0.03%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 531983 (Eliminated: 0 Frozen: 174571)
Constraints : 3993690 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 714MB
Max. Length : 120 steps
Models : 1