2629 lines
95 KiB
Plaintext
2629 lines
95 KiB
Plaintext
INFO Running translator.
|
|
INFO translator input: ['/home/pluehne/Documents/ASP/pddl-instances/ipc-2011/domains/barman-sequential-satisficing/domain.pddl', '/home/pluehne/Documents/ASP/pddl-instances/ipc-2011/domains/barman-sequential-satisficing/instances/instance-3.pddl']
|
|
INFO translator arguments: []
|
|
INFO translator time limit: None
|
|
INFO translator memory limit: None
|
|
INFO callstring: /home/pluehne/.usr/bin/python /home/wv/bin/linux/64/fast-downward-10997/builds/release64/bin/translate/translate.py /home/pluehne/Documents/ASP/pddl-instances/ipc-2011/domains/barman-sequential-satisficing/domain.pddl /home/pluehne/Documents/ASP/pddl-instances/ipc-2011/domains/barman-sequential-satisficing/instances/instance-3.pddl
|
|
Parsing...
|
|
Parsing: [0.040s CPU, 0.039s wall-clock]
|
|
Normalizing task... [0.000s CPU, 0.003s wall-clock]
|
|
Instantiating...
|
|
Generating Datalog program... [0.010s CPU, 0.010s wall-clock]
|
|
Normalizing Datalog program...
|
|
Normalizing Datalog program: [0.050s CPU, 0.050s wall-clock]
|
|
Preparing model... [0.030s CPU, 0.025s wall-clock]
|
|
Generated 115 rules.
|
|
Computing model... [0.320s CPU, 0.327s wall-clock]
|
|
2025 relevant atoms
|
|
2105 auxiliary atoms
|
|
4130 final queue length
|
|
7122 total queue pushes
|
|
Completing instantiation... [0.600s CPU, 0.600s wall-clock]
|
|
Instantiating: [1.010s CPU, 1.016s wall-clock]
|
|
Computing fact groups...
|
|
Finding invariants...
|
|
24 initial candidates
|
|
Finding invariants: [0.100s CPU, 0.090s wall-clock]
|
|
Checking invariant weight... [0.000s CPU, 0.001s wall-clock]
|
|
Instantiating groups... [0.000s CPU, 0.006s wall-clock]
|
|
Collecting mutex groups... [0.000s CPU, 0.000s wall-clock]
|
|
Choosing groups...
|
|
207 uncovered facts
|
|
Choosing groups: [0.000s CPU, 0.001s wall-clock]
|
|
Building translation key... [0.010s CPU, 0.008s wall-clock]
|
|
Computing fact groups: [0.130s CPU, 0.121s wall-clock]
|
|
Building STRIPS to SAS dictionary... [0.000s CPU, 0.002s wall-clock]
|
|
Building dictionary for full mutex groups... [0.000s CPU, 0.002s wall-clock]
|
|
Building mutex information...
|
|
Building mutex information: [0.000s CPU, 0.002s wall-clock]
|
|
Translating task...
|
|
Processing axioms...
|
|
Simplifying axioms... [0.000s CPU, 0.000s wall-clock]
|
|
Processing axioms: [0.040s CPU, 0.033s wall-clock]
|
|
Translating task: [0.660s CPU, 0.658s wall-clock]
|
|
2326 effect conditions simplified
|
|
0 implied preconditions added
|
|
Detecting unreachable propositions...
|
|
0 operators removed
|
|
0 axioms removed
|
|
3 propositions removed
|
|
Detecting unreachable propositions: [0.310s CPU, 0.311s wall-clock]
|
|
Reordering and filtering variables...
|
|
210 of 210 variables necessary.
|
|
11 of 14 mutex groups necessary.
|
|
1390 of 1390 operators necessary.
|
|
0 of 0 axiom rules necessary.
|
|
Reordering and filtering variables: [0.210s CPU, 0.206s 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.240s CPU, 0.255s wall-clock]
|
|
Done! [2.620s CPU, 2.641s wall-clock]
|
|
planner.py version 0.0.1
|
|
|
|
Time: 0.56s
|
|
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.653s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
|
|
CPU Time : 0.568s
|
|
|
|
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 : 0
|
|
Calls : 2
|
|
Time : 0.981s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
|
|
CPU Time : 0.896s
|
|
|
|
Choices : 87 (Domain: 79)
|
|
Conflicts : 41 (Analyzed: 40)
|
|
Restarts : 0
|
|
Problems : 2 (Average Length: 4.50 Splits: 0)
|
|
Lemmas : 40 (Deleted: 0)
|
|
Binary : 5 (Ratio: 12.50%)
|
|
Ternary : 0 (Ratio: 0.00%)
|
|
Conflict : 40 (Average Length: 8.4 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 40 (Average: 2.20 Max: 11 Sum: 88)
|
|
Executed : 39 (Average: 2.17 Max: 11 Sum: 87 Ratio: 98.86%)
|
|
Bounded : 1 (Average: 1.00 Max: 1 Sum: 1 Ratio: 1.14%)
|
|
|
|
Rules : 38518
|
|
Atoms : 38518
|
|
Bodies : 1 (Original: 0)
|
|
Tight : Yes
|
|
Variables : 10318 (Eliminated: 0 Frozen: 10318)
|
|
Constraints : 36429 (Binary: 95.1% Ternary: 3.5% Other: 1.5%)
|
|
|
|
Memory Peak : 222MB
|
|
Max. Length : 0 steps
|
|
Models : 0
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 0.10s
|
|
Memory: 160MB (+2MB)
|
|
UNSAT
|
|
Iteration Time: 0.33s
|
|
|
|
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: 162.0MB
|
|
Grounding... [('step', [6]), ('step', [7]), ('step', [8]), ('step', [9]), ('step', [10]), ('check', [10])]
|
|
Grounding Time: 0.18s
|
|
Memory: 164MB (+4MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 1+
|
|
Calls : 3
|
|
Time : 1.409s (Solving: 0.01s 1st Model: 0.00s Unsat: 0.00s)
|
|
CPU Time : 1.324s
|
|
|
|
Choices : 554 (Domain: 518)
|
|
Conflicts : 55 (Analyzed: 54)
|
|
Restarts : 0
|
|
Model-Level : 212.0
|
|
Problems : 3 (Average Length: 7.00 Splits: 0)
|
|
Lemmas : 54 (Deleted: 0)
|
|
Binary : 10 (Ratio: 18.52%)
|
|
Ternary : 2 (Ratio: 3.70%)
|
|
Conflict : 54 (Average Length: 12.4 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 54 (Average: 6.57 Max: 65 Sum: 355)
|
|
Executed : 53 (Average: 6.56 Max: 65 Sum: 354 Ratio: 99.72%)
|
|
Bounded : 1 (Average: 1.00 Max: 1 Sum: 1 Ratio: 0.28%)
|
|
|
|
Rules : 38518
|
|
Atoms : 38518
|
|
Bodies : 1 (Original: 0)
|
|
Tight : Yes
|
|
Variables : 22604 (Eliminated: 0 Frozen: 22604)
|
|
Constraints : 136839 (Binary: 95.5% Ternary: 3.2% Other: 1.2%)
|
|
|
|
Memory Peak : 222MB
|
|
Max. Length : 5 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 0.17s
|
|
Memory: 171MB (+7MB)
|
|
SAT
|
|
Testing...
|
|
NOT SERIALIZABLE
|
|
Testing Time: 0.65s
|
|
Memory: 191MB (+20MB)
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0
|
|
Calls : 4
|
|
Time : 1.943s (Solving: 0.27s 1st Model: 0.00s Unsat: 0.26s)
|
|
CPU Time : 1.856s
|
|
|
|
Choices : 8046 (Domain: 7436)
|
|
Conflicts : 961 (Analyzed: 959)
|
|
Restarts : 6 (Average: 159.83 Last: 98)
|
|
Model-Level : 212.0
|
|
Problems : 4 (Average Length: 8.25 Splits: 0)
|
|
Lemmas : 959 (Deleted: 0)
|
|
Binary : 286 (Ratio: 29.82%)
|
|
Ternary : 161 (Ratio: 16.79%)
|
|
Conflict : 959 (Average Length: 34.6 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 959 (Average: 8.24 Max: 89 Sum: 7898)
|
|
Executed : 945 (Average: 8.14 Max: 89 Sum: 7807 Ratio: 98.85%)
|
|
Bounded : 14 (Average: 6.50 Max: 12 Sum: 91 Ratio: 1.15%)
|
|
|
|
Rules : 94613 (Original: 86518)
|
|
Atoms : 45936
|
|
Bodies : 40692 (Original: 32596)
|
|
Count : 619 (Original: 1518)
|
|
Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209)
|
|
Tight : Yes
|
|
Variables : 34632 (Eliminated: 8994 Frozen: 25638)
|
|
Constraints : 194982 (Binary: 88.9% Ternary: 7.3% Other: 3.8%)
|
|
|
|
Memory Peak : 222MB
|
|
Max. Length : 5 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 0.39s
|
|
Memory: 188MB (+-3MB)
|
|
UNSAT
|
|
Iteration Time: 1.47s
|
|
|
|
Iteration 4
|
|
Queue: [(3,15,0,True), (4,20,0,True), (5,25,0,True), (6,30,0,True)]
|
|
Grounded Until: 10
|
|
Expected Memory: 199.0MB
|
|
Grounding... [('step', [11]), ('step', [12]), ('step', [13]), ('step', [14]), ('step', [15]), ('check', [15])]
|
|
Grounding Time: 0.34s
|
|
Memory: 195MB (+7MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0
|
|
Calls : 5
|
|
Time : 9.858s (Solving: 7.40s 1st Model: 0.00s Unsat: 7.40s)
|
|
CPU Time : 9.776s
|
|
|
|
Choices : 178625 (Domain: 143317)
|
|
Conflicts : 25090 (Analyzed: 25087)
|
|
Restarts : 94 (Average: 266.88 Last: 98)
|
|
Model-Level : 212.0
|
|
Problems : 5 (Average Length: 10.00 Splits: 0)
|
|
Lemmas : 25087 (Deleted: 16452)
|
|
Binary : 1522 (Ratio: 6.07%)
|
|
Ternary : 479 (Ratio: 1.91%)
|
|
Conflict : 25087 (Average Length: 288.1 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 25087 (Average: 6.95 Max: 401 Sum: 174374)
|
|
Executed : 25056 (Average: 6.94 Max: 401 Sum: 174016 Ratio: 99.79%)
|
|
Bounded : 31 (Average: 11.55 Max: 17 Sum: 358 Ratio: 0.21%)
|
|
|
|
Rules : 94613 (Original: 86518)
|
|
Atoms : 45936
|
|
Bodies : 40692 (Original: 32596)
|
|
Count : 619 (Original: 1518)
|
|
Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209)
|
|
Tight : Yes
|
|
Variables : 57193 (Eliminated: 8994 Frozen: 40669)
|
|
Constraints : 363350 (Binary: 90.3% Ternary: 6.9% Other: 2.9%)
|
|
|
|
Memory Peak : 222MB
|
|
Max. Length : 10 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 7.46s
|
|
Memory: 206MB (+11MB)
|
|
UNSAT
|
|
Iteration Time: 7.93s
|
|
|
|
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.35s
|
|
Memory: 213MB (+7MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 6
|
|
Time : 24.515s (Solving: 21.24s 1st Model: 0.00s Unsat: 7.40s)
|
|
CPU Time : 24.440s
|
|
|
|
Choices : 450104 (Domain: 398284)
|
|
Conflicts : 53216 (Analyzed: 53213)
|
|
Restarts : 194 (Average: 274.29 Last: 201)
|
|
Model-Level : 212.0
|
|
Problems : 6 (Average Length: 12.00 Splits: 0)
|
|
Lemmas : 53213 (Deleted: 38381)
|
|
Binary : 2964 (Ratio: 5.57%)
|
|
Ternary : 766 (Ratio: 1.44%)
|
|
Conflict : 53213 (Average Length: 476.5 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 53213 (Average: 8.17 Max: 401 Sum: 435006)
|
|
Executed : 53170 (Average: 8.16 Max: 401 Sum: 434408 Ratio: 99.86%)
|
|
Bounded : 43 (Average: 13.91 Max: 22 Sum: 598 Ratio: 0.14%)
|
|
|
|
Rules : 94613 (Original: 86518)
|
|
Atoms : 45936
|
|
Bodies : 40692 (Original: 32596)
|
|
Count : 619 (Original: 1518)
|
|
Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209)
|
|
Tight : Yes
|
|
Variables : 79754 (Eliminated: 8994 Frozen: 63230)
|
|
Constraints : 517735 (Binary: 90.8% Ternary: 6.7% Other: 2.5%)
|
|
|
|
Memory Peak : 225MB
|
|
Max. Length : 15 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 14.18s
|
|
Memory: 225MB (+12MB)
|
|
UNKNOWN
|
|
Iteration Time: 14.67s
|
|
|
|
Iteration 6
|
|
Queue: [(5,25,0,True), (6,30,0,True)]
|
|
Grounded Until: 20
|
|
Expected Memory: 244.0MB
|
|
Grounding... [('step', [21]), ('step', [22]), ('step', [23]), ('step', [24]), ('step', [25]), ('check', [25])]
|
|
Grounding Time: 0.36s
|
|
Memory: 227MB (+2MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 7
|
|
Time : 41.662s (Solving: 37.54s 1st Model: 0.00s Unsat: 7.40s)
|
|
CPU Time : 41.596s
|
|
|
|
Choices : 644218 (Domain: 583497)
|
|
Conflicts : 81366 (Analyzed: 81363)
|
|
Restarts : 294 (Average: 276.74 Last: 202)
|
|
Model-Level : 212.0
|
|
Problems : 7 (Average Length: 14.14 Splits: 0)
|
|
Lemmas : 81363 (Deleted: 64324)
|
|
Binary : 4084 (Ratio: 5.02%)
|
|
Ternary : 955 (Ratio: 1.17%)
|
|
Conflict : 81363 (Average Length: 724.4 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 81363 (Average: 7.56 Max: 401 Sum: 614802)
|
|
Executed : 81318 (Average: 7.55 Max: 401 Sum: 614150 Ratio: 99.89%)
|
|
Bounded : 45 (Average: 14.49 Max: 27 Sum: 652 Ratio: 0.11%)
|
|
|
|
Rules : 94613 (Original: 86518)
|
|
Atoms : 45936
|
|
Bodies : 40692 (Original: 32596)
|
|
Count : 619 (Original: 1518)
|
|
Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209)
|
|
Tight : Yes
|
|
Variables : 102315 (Eliminated: 8994 Frozen: 85791)
|
|
Constraints : 684819 (Binary: 91.1% Ternary: 6.6% Other: 2.3%)
|
|
|
|
Memory Peak : 371MB
|
|
Max. Length : 20 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 16.64s
|
|
Memory: 307MB (+80MB)
|
|
UNKNOWN
|
|
Iteration Time: 17.16s
|
|
|
|
Iteration 7
|
|
Queue: [(6,30,0,True)]
|
|
Grounded Until: 25
|
|
Expected Memory: 389.0MB
|
|
Grounding... [('step', [26]), ('step', [27]), ('step', [28]), ('step', [29]), ('step', [30]), ('check', [30])]
|
|
Grounding Time: 0.31s
|
|
Memory: 309MB (+2MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 8
|
|
Time : 59.418s (Solving: 54.48s 1st Model: 0.00s Unsat: 7.40s)
|
|
CPU Time : 59.364s
|
|
|
|
Choices : 877843 (Domain: 807962)
|
|
Conflicts : 109490 (Analyzed: 109487)
|
|
Restarts : 394 (Average: 277.89 Last: 202)
|
|
Model-Level : 212.0
|
|
Problems : 8 (Average Length: 16.38 Splits: 0)
|
|
Lemmas : 109487 (Deleted: 90819)
|
|
Binary : 5308 (Ratio: 4.85%)
|
|
Ternary : 1262 (Ratio: 1.15%)
|
|
Conflict : 109487 (Average Length: 786.0 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 109487 (Average: 7.61 Max: 401 Sum: 833224)
|
|
Executed : 109442 (Average: 7.60 Max: 401 Sum: 832572 Ratio: 99.92%)
|
|
Bounded : 45 (Average: 14.49 Max: 27 Sum: 652 Ratio: 0.08%)
|
|
|
|
Rules : 94613 (Original: 86518)
|
|
Atoms : 45936
|
|
Bodies : 40692 (Original: 32596)
|
|
Count : 619 (Original: 1518)
|
|
Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209)
|
|
Tight : Yes
|
|
Variables : 124876 (Eliminated: 8994 Frozen: 108352)
|
|
Constraints : 851268 (Binary: 91.2% Ternary: 6.6% Other: 2.2%)
|
|
|
|
Memory Peak : 371MB
|
|
Max. Length : 25 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 17.29s
|
|
Memory: 322MB (+13MB)
|
|
UNKNOWN
|
|
Iteration Time: 17.77s
|
|
|
|
Iteration 8
|
|
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), (17,85,0,True)]
|
|
Grounded Until: 30
|
|
Blocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 9
|
|
Time : 68.575s (Solving: 63.60s 1st Model: 0.00s Unsat: 7.40s)
|
|
CPU Time : 68.524s
|
|
|
|
Choices : 967961 (Domain: 898080)
|
|
Conflicts : 137673 (Analyzed: 137670)
|
|
Restarts : 494 (Average: 278.68 Last: 202)
|
|
Model-Level : 212.0
|
|
Problems : 9 (Average Length: 18.11 Splits: 0)
|
|
Lemmas : 137670 (Deleted: 117901)
|
|
Binary : 5569 (Ratio: 4.05%)
|
|
Ternary : 1305 (Ratio: 0.95%)
|
|
Conflict : 137670 (Average Length: 706.8 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 137670 (Average: 6.66 Max: 401 Sum: 917259)
|
|
Executed : 137622 (Average: 6.66 Max: 401 Sum: 916516 Ratio: 99.92%)
|
|
Bounded : 48 (Average: 15.48 Max: 32 Sum: 743 Ratio: 0.08%)
|
|
|
|
Rules : 94613 (Original: 86518)
|
|
Atoms : 45936
|
|
Bodies : 40692 (Original: 32596)
|
|
Count : 619 (Original: 1518)
|
|
Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209)
|
|
Tight : Yes
|
|
Variables : 124876 (Eliminated: 8994 Frozen: 115882)
|
|
Constraints : 851268 (Binary: 91.2% Ternary: 6.6% Other: 2.2%)
|
|
|
|
Memory Peak : 371MB
|
|
Max. Length : 30 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 9.15s
|
|
Memory: 322MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 9.16s
|
|
|
|
Iteration 9
|
|
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), (17,85,0,True)]
|
|
Grounded Until: 30
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 10
|
|
Time : 93.661s (Solving: 88.65s 1st Model: 0.00s Unsat: 7.40s)
|
|
CPU Time : 93.620s
|
|
|
|
Choices : 1092316 (Domain: 1022396)
|
|
Conflicts : 165767 (Analyzed: 165764)
|
|
Restarts : 594 (Average: 279.06 Last: 202)
|
|
Model-Level : 212.0
|
|
Problems : 10 (Average Length: 19.50 Splits: 0)
|
|
Lemmas : 165764 (Deleted: 145297)
|
|
Binary : 5831 (Ratio: 3.52%)
|
|
Ternary : 1370 (Ratio: 0.83%)
|
|
Conflict : 165764 (Average Length: 807.6 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 165764 (Average: 6.21 Max: 401 Sum: 1028957)
|
|
Executed : 165715 (Average: 6.20 Max: 401 Sum: 1028182 Ratio: 99.92%)
|
|
Bounded : 49 (Average: 15.82 Max: 32 Sum: 775 Ratio: 0.08%)
|
|
|
|
Rules : 94613 (Original: 86518)
|
|
Atoms : 45936
|
|
Bodies : 40692 (Original: 32596)
|
|
Count : 619 (Original: 1518)
|
|
Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209)
|
|
Tight : Yes
|
|
Variables : 124876 (Eliminated: 8994 Frozen: 115882)
|
|
Constraints : 851240 (Binary: 91.2% Ternary: 6.6% Other: 2.2%)
|
|
|
|
Memory Peak : 371MB
|
|
Max. Length : 30 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 25.09s
|
|
Memory: 322MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 25.10s
|
|
|
|
Iteration 10
|
|
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), (17,85,0,True)]
|
|
Grounded Until: 30
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 11
|
|
Time : 114.674s (Solving: 109.62s 1st Model: 0.00s Unsat: 7.40s)
|
|
CPU Time : 114.644s
|
|
|
|
Choices : 1339062 (Domain: 1266460)
|
|
Conflicts : 193889 (Analyzed: 193886)
|
|
Restarts : 694 (Average: 279.37 Last: 202)
|
|
Model-Level : 212.0
|
|
Problems : 11 (Average Length: 20.64 Splits: 0)
|
|
Lemmas : 193886 (Deleted: 172108)
|
|
Binary : 6429 (Ratio: 3.32%)
|
|
Ternary : 1486 (Ratio: 0.77%)
|
|
Conflict : 193886 (Average Length: 813.8 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 193886 (Average: 6.49 Max: 401 Sum: 1259166)
|
|
Executed : 193837 (Average: 6.49 Max: 401 Sum: 1258391 Ratio: 99.94%)
|
|
Bounded : 49 (Average: 15.82 Max: 32 Sum: 775 Ratio: 0.06%)
|
|
|
|
Rules : 94613 (Original: 86518)
|
|
Atoms : 45936
|
|
Bodies : 40692 (Original: 32596)
|
|
Count : 619 (Original: 1518)
|
|
Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209)
|
|
Tight : Yes
|
|
Variables : 124876 (Eliminated: 8994 Frozen: 115882)
|
|
Constraints : 849719 (Binary: 91.2% Ternary: 6.6% Other: 2.2%)
|
|
|
|
Memory Peak : 371MB
|
|
Max. Length : 30 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 21.00s
|
|
Memory: 322MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 21.03s
|
|
|
|
Iteration 11
|
|
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), (17,85,0,True)]
|
|
Grounded Until: 30
|
|
Expected Memory: 404.0MB
|
|
Grounding... [('step', [31]), ('step', [32]), ('step', [33]), ('step', [34]), ('step', [35]), ('check', [35])]
|
|
Grounding Time: 0.32s
|
|
Memory: 324MB (+2MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 12
|
|
Time : 129.744s (Solving: 123.86s 1st Model: 0.00s Unsat: 7.40s)
|
|
CPU Time : 129.720s
|
|
|
|
Choices : 1533857 (Domain: 1454042)
|
|
Conflicts : 222078 (Analyzed: 222075)
|
|
Restarts : 794 (Average: 279.69 Last: 202)
|
|
Model-Level : 212.0
|
|
Problems : 12 (Average Length: 22.00 Splits: 0)
|
|
Lemmas : 222075 (Deleted: 198986)
|
|
Binary : 7350 (Ratio: 3.31%)
|
|
Ternary : 1575 (Ratio: 0.71%)
|
|
Conflict : 222075 (Average Length: 769.1 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 222075 (Average: 6.49 Max: 401 Sum: 1440214)
|
|
Executed : 222025 (Average: 6.48 Max: 401 Sum: 1439402 Ratio: 99.94%)
|
|
Bounded : 50 (Average: 16.24 Max: 37 Sum: 812 Ratio: 0.06%)
|
|
|
|
Rules : 94613 (Original: 86518)
|
|
Atoms : 45936
|
|
Bodies : 40692 (Original: 32596)
|
|
Count : 619 (Original: 1518)
|
|
Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209)
|
|
Tight : Yes
|
|
Variables : 147437 (Eliminated: 8994 Frozen: 130913)
|
|
Constraints : 1022744 (Binary: 91.3% Ternary: 6.6% Other: 2.2%)
|
|
|
|
Memory Peak : 371MB
|
|
Max. Length : 30 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 14.59s
|
|
Memory: 344MB (+20MB)
|
|
UNKNOWN
|
|
Iteration Time: 15.09s
|
|
|
|
Iteration 12
|
|
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), (17,85,0,True)]
|
|
Grounded Until: 35
|
|
Expected Memory: 426.0MB
|
|
Grounding... [('step', [36]), ('step', [37]), ('step', [38]), ('step', [39]), ('step', [40]), ('check', [40])]
|
|
Grounding Time: 0.42s
|
|
Memory: 357MB (+13MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 13
|
|
Time : 145.922s (Solving: 139.08s 1st Model: 0.00s Unsat: 7.40s)
|
|
CPU Time : 145.904s
|
|
|
|
Choices : 1767987 (Domain: 1676424)
|
|
Conflicts : 250245 (Analyzed: 250242)
|
|
Restarts : 894 (Average: 279.91 Last: 206)
|
|
Model-Level : 212.0
|
|
Problems : 13 (Average Length: 23.54 Splits: 0)
|
|
Lemmas : 250242 (Deleted: 225054)
|
|
Binary : 8412 (Ratio: 3.36%)
|
|
Ternary : 1719 (Ratio: 0.69%)
|
|
Conflict : 250242 (Average Length: 767.3 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 250242 (Average: 6.60 Max: 401 Sum: 1652594)
|
|
Executed : 250191 (Average: 6.60 Max: 401 Sum: 1651740 Ratio: 99.95%)
|
|
Bounded : 51 (Average: 16.75 Max: 42 Sum: 854 Ratio: 0.05%)
|
|
|
|
Rules : 94613 (Original: 86518)
|
|
Atoms : 45936
|
|
Bodies : 40692 (Original: 32596)
|
|
Count : 619 (Original: 1518)
|
|
Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209)
|
|
Tight : Yes
|
|
Variables : 169998 (Eliminated: 8994 Frozen: 153474)
|
|
Constraints : 1195759 (Binary: 91.3% Ternary: 6.6% Other: 2.1%)
|
|
|
|
Memory Peak : 377MB
|
|
Max. Length : 35 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 15.59s
|
|
Memory: 366MB (+9MB)
|
|
UNKNOWN
|
|
Iteration Time: 16.20s
|
|
|
|
Iteration 13
|
|
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), (17,85,0,True)]
|
|
Grounded Until: 40
|
|
Expected Memory: 448.0MB
|
|
Grounding... [('step', [41]), ('step', [42]), ('step', [43]), ('step', [44]), ('step', [45]), ('check', [45])]
|
|
Grounding Time: 0.31s
|
|
Memory: 367MB (+1MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 14
|
|
Time : 162.860s (Solving: 155.16s 1st Model: 0.00s Unsat: 7.40s)
|
|
CPU Time : 162.848s
|
|
|
|
Choices : 2012899 (Domain: 1917846)
|
|
Conflicts : 278412 (Analyzed: 278409)
|
|
Restarts : 994 (Average: 280.09 Last: 206)
|
|
Model-Level : 212.0
|
|
Problems : 14 (Average Length: 25.21 Splits: 0)
|
|
Lemmas : 278409 (Deleted: 251719)
|
|
Binary : 9241 (Ratio: 3.32%)
|
|
Ternary : 1798 (Ratio: 0.65%)
|
|
Conflict : 278409 (Average Length: 767.5 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 278409 (Average: 6.73 Max: 401 Sum: 1873261)
|
|
Executed : 278358 (Average: 6.73 Max: 401 Sum: 1872407 Ratio: 99.95%)
|
|
Bounded : 51 (Average: 16.75 Max: 42 Sum: 854 Ratio: 0.05%)
|
|
|
|
Rules : 94613 (Original: 86518)
|
|
Atoms : 45936
|
|
Bodies : 40692 (Original: 32596)
|
|
Count : 619 (Original: 1518)
|
|
Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209)
|
|
Tight : Yes
|
|
Variables : 192559 (Eliminated: 8994 Frozen: 176035)
|
|
Constraints : 1368767 (Binary: 91.3% Ternary: 6.6% Other: 2.1%)
|
|
|
|
Memory Peak : 393MB
|
|
Max. Length : 40 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 16.44s
|
|
Memory: 381MB (+14MB)
|
|
UNKNOWN
|
|
Iteration Time: 16.95s
|
|
|
|
Iteration 14
|
|
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), (17,85,0,True)]
|
|
Grounded Until: 45
|
|
Expected Memory: 463.0MB
|
|
Grounding... [('step', [46]), ('step', [47]), ('step', [48]), ('step', [49]), ('step', [50]), ('check', [50])]
|
|
Grounding Time: 0.31s
|
|
Memory: 381MB (+0MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 15
|
|
Time : 178.759s (Solving: 170.19s 1st Model: 0.00s Unsat: 7.40s)
|
|
CPU Time : 178.752s
|
|
|
|
Choices : 2307695 (Domain: 2197417)
|
|
Conflicts : 306536 (Analyzed: 306533)
|
|
Restarts : 1094 (Average: 280.19 Last: 208)
|
|
Model-Level : 212.0
|
|
Problems : 15 (Average Length: 27.00 Splits: 0)
|
|
Lemmas : 306533 (Deleted: 278324)
|
|
Binary : 10317 (Ratio: 3.37%)
|
|
Ternary : 1985 (Ratio: 0.65%)
|
|
Conflict : 306533 (Average Length: 750.2 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 306533 (Average: 6.98 Max: 401 Sum: 2139960)
|
|
Executed : 306482 (Average: 6.98 Max: 401 Sum: 2139106 Ratio: 99.96%)
|
|
Bounded : 51 (Average: 16.75 Max: 42 Sum: 854 Ratio: 0.04%)
|
|
|
|
Rules : 94613 (Original: 86518)
|
|
Atoms : 45936
|
|
Bodies : 40692 (Original: 32596)
|
|
Count : 619 (Original: 1518)
|
|
Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209)
|
|
Tight : Yes
|
|
Variables : 215120 (Eliminated: 8994 Frozen: 198596)
|
|
Constraints : 1541792 (Binary: 91.4% Ternary: 6.6% Other: 2.1%)
|
|
|
|
Memory Peak : 412MB
|
|
Max. Length : 45 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 15.40s
|
|
Memory: 410MB (+29MB)
|
|
UNKNOWN
|
|
Iteration Time: 15.91s
|
|
|
|
Iteration 15
|
|
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), (17,85,0,True)]
|
|
Grounded Until: 50
|
|
Expected Memory: 492.0MB
|
|
Grounding... [('step', [51]), ('step', [52]), ('step', [53]), ('step', [54]), ('step', [55]), ('check', [55])]
|
|
Grounding Time: 0.31s
|
|
Memory: 410MB (+0MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 16
|
|
Time : 196.304s (Solving: 186.86s 1st Model: 0.00s Unsat: 7.40s)
|
|
CPU Time : 196.304s
|
|
|
|
Choices : 2586997 (Domain: 2474559)
|
|
Conflicts : 334700 (Analyzed: 334697)
|
|
Restarts : 1194 (Average: 280.32 Last: 208)
|
|
Model-Level : 212.0
|
|
Problems : 16 (Average Length: 28.88 Splits: 0)
|
|
Lemmas : 334697 (Deleted: 304977)
|
|
Binary : 11080 (Ratio: 3.31%)
|
|
Ternary : 2047 (Ratio: 0.61%)
|
|
Conflict : 334697 (Average Length: 761.1 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 334697 (Average: 7.14 Max: 401 Sum: 2391390)
|
|
Executed : 334646 (Average: 7.14 Max: 401 Sum: 2390536 Ratio: 99.96%)
|
|
Bounded : 51 (Average: 16.75 Max: 42 Sum: 854 Ratio: 0.04%)
|
|
|
|
Rules : 94613 (Original: 86518)
|
|
Atoms : 45936
|
|
Bodies : 40692 (Original: 32596)
|
|
Count : 619 (Original: 1518)
|
|
Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209)
|
|
Tight : Yes
|
|
Variables : 237681 (Eliminated: 8994 Frozen: 221157)
|
|
Constraints : 1714817 (Binary: 91.4% Ternary: 6.6% Other: 2.0%)
|
|
|
|
Memory Peak : 439MB
|
|
Max. Length : 50 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 17.03s
|
|
Memory: 420MB (+10MB)
|
|
UNKNOWN
|
|
Iteration Time: 17.56s
|
|
|
|
Iteration 16
|
|
Queue: [(12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True), (17,85,0,True)]
|
|
Grounded Until: 55
|
|
Expected Memory: 502.0MB
|
|
Grounding... [('step', [56]), ('step', [57]), ('step', [58]), ('step', [59]), ('step', [60]), ('check', [60])]
|
|
Grounding Time: 0.34s
|
|
Memory: 420MB (+0MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 17
|
|
Time : 212.017s (Solving: 201.64s 1st Model: 0.00s Unsat: 7.40s)
|
|
CPU Time : 212.024s
|
|
|
|
Choices : 2773336 (Domain: 2660889)
|
|
Conflicts : 362908 (Analyzed: 362905)
|
|
Restarts : 1294 (Average: 280.45 Last: 208)
|
|
Model-Level : 212.0
|
|
Problems : 17 (Average Length: 30.82 Splits: 0)
|
|
Lemmas : 362905 (Deleted: 332355)
|
|
Binary : 11510 (Ratio: 3.17%)
|
|
Ternary : 2097 (Ratio: 0.58%)
|
|
Conflict : 362905 (Average Length: 755.0 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 362905 (Average: 7.05 Max: 401 Sum: 2556974)
|
|
Executed : 362854 (Average: 7.04 Max: 401 Sum: 2556120 Ratio: 99.97%)
|
|
Bounded : 51 (Average: 16.75 Max: 42 Sum: 854 Ratio: 0.03%)
|
|
|
|
Rules : 94613 (Original: 86518)
|
|
Atoms : 45936
|
|
Bodies : 40692 (Original: 32596)
|
|
Count : 619 (Original: 1518)
|
|
Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209)
|
|
Tight : Yes
|
|
Variables : 260242 (Eliminated: 8994 Frozen: 243718)
|
|
Constraints : 1887842 (Binary: 91.4% Ternary: 6.6% Other: 2.0%)
|
|
|
|
Memory Peak : 455MB
|
|
Max. Length : 55 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 15.15s
|
|
Memory: 434MB (+14MB)
|
|
UNKNOWN
|
|
Iteration Time: 15.73s
|
|
|
|
Iteration 17
|
|
Queue: [(13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True), (17,85,0,True)]
|
|
Grounded Until: 60
|
|
Expected Memory: 516.0MB
|
|
Grounding... [('step', [61]), ('step', [62]), ('step', [63]), ('step', [64]), ('step', [65]), ('check', [65])]
|
|
Grounding Time: 0.32s
|
|
Memory: 434MB (+0MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 18
|
|
Time : 231.824s (Solving: 220.52s 1st Model: 0.00s Unsat: 7.40s)
|
|
CPU Time : 231.840s
|
|
|
|
Choices : 3047628 (Domain: 2934473)
|
|
Conflicts : 391041 (Analyzed: 391038)
|
|
Restarts : 1394 (Average: 280.52 Last: 208)
|
|
Model-Level : 212.0
|
|
Problems : 18 (Average Length: 32.83 Splits: 0)
|
|
Lemmas : 391038 (Deleted: 359574)
|
|
Binary : 11990 (Ratio: 3.07%)
|
|
Ternary : 2151 (Ratio: 0.55%)
|
|
Conflict : 391038 (Average Length: 753.6 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 391038 (Average: 7.17 Max: 401 Sum: 2805345)
|
|
Executed : 390987 (Average: 7.17 Max: 401 Sum: 2804491 Ratio: 99.97%)
|
|
Bounded : 51 (Average: 16.75 Max: 42 Sum: 854 Ratio: 0.03%)
|
|
|
|
Rules : 94613 (Original: 86518)
|
|
Atoms : 45936
|
|
Bodies : 40692 (Original: 32596)
|
|
Count : 619 (Original: 1518)
|
|
Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209)
|
|
Tight : Yes
|
|
Variables : 282803 (Eliminated: 8994 Frozen: 266279)
|
|
Constraints : 2060867 (Binary: 91.4% Ternary: 6.6% Other: 2.0%)
|
|
|
|
Memory Peak : 473MB
|
|
Max. Length : 60 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 19.27s
|
|
Memory: 452MB (+18MB)
|
|
UNKNOWN
|
|
Iteration Time: 19.82s
|
|
|
|
Iteration 18
|
|
Queue: [(14,70,0,True), (15,75,0,True), (16,80,0,True), (17,85,0,True)]
|
|
Grounded Until: 65
|
|
Expected Memory: 534.0MB
|
|
Grounding... [('step', [66]), ('step', [67]), ('step', [68]), ('step', [69]), ('step', [70]), ('check', [70])]
|
|
Grounding Time: 0.33s
|
|
Memory: 452MB (+0MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 19
|
|
Time : 249.390s (Solving: 237.13s 1st Model: 0.00s Unsat: 7.40s)
|
|
CPU Time : 249.416s
|
|
|
|
Choices : 3272129 (Domain: 3158615)
|
|
Conflicts : 419210 (Analyzed: 419207)
|
|
Restarts : 1494 (Average: 280.59 Last: 208)
|
|
Model-Level : 212.0
|
|
Problems : 19 (Average Length: 34.89 Splits: 0)
|
|
Lemmas : 419207 (Deleted: 385854)
|
|
Binary : 12459 (Ratio: 2.97%)
|
|
Ternary : 2197 (Ratio: 0.52%)
|
|
Conflict : 419207 (Average Length: 752.3 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 419207 (Average: 7.16 Max: 401 Sum: 3002607)
|
|
Executed : 419156 (Average: 7.16 Max: 401 Sum: 3001753 Ratio: 99.97%)
|
|
Bounded : 51 (Average: 16.75 Max: 42 Sum: 854 Ratio: 0.03%)
|
|
|
|
Rules : 94613 (Original: 86518)
|
|
Atoms : 45936
|
|
Bodies : 40692 (Original: 32596)
|
|
Count : 619 (Original: 1518)
|
|
Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209)
|
|
Tight : Yes
|
|
Variables : 305364 (Eliminated: 8994 Frozen: 288840)
|
|
Constraints : 2233892 (Binary: 91.4% Ternary: 6.6% Other: 2.0%)
|
|
|
|
Memory Peak : 491MB
|
|
Max. Length : 65 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 17.00s
|
|
Memory: 490MB (+38MB)
|
|
UNKNOWN
|
|
Iteration Time: 17.58s
|
|
|
|
Iteration 19
|
|
Queue: [(15,75,0,True), (16,80,0,True), (17,85,0,True)]
|
|
Grounded Until: 70
|
|
Expected Memory: 572.0MB
|
|
Grounding... [('step', [71]), ('step', [72]), ('step', [73]), ('step', [74]), ('step', [75]), ('check', [75])]
|
|
Grounding Time: 0.34s
|
|
Memory: 490MB (+0MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 20
|
|
Time : 270.819s (Solving: 257.60s 1st Model: 0.00s Unsat: 7.40s)
|
|
CPU Time : 270.856s
|
|
|
|
Choices : 3640853 (Domain: 3525454)
|
|
Conflicts : 447391 (Analyzed: 447388)
|
|
Restarts : 1594 (Average: 280.67 Last: 208)
|
|
Model-Level : 212.0
|
|
Problems : 20 (Average Length: 37.00 Splits: 0)
|
|
Lemmas : 447388 (Deleted: 413840)
|
|
Binary : 13149 (Ratio: 2.94%)
|
|
Ternary : 2305 (Ratio: 0.52%)
|
|
Conflict : 447388 (Average Length: 767.3 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 447388 (Average: 7.46 Max: 411 Sum: 3339733)
|
|
Executed : 447337 (Average: 7.46 Max: 411 Sum: 3338879 Ratio: 99.97%)
|
|
Bounded : 51 (Average: 16.75 Max: 42 Sum: 854 Ratio: 0.03%)
|
|
|
|
Rules : 94613 (Original: 86518)
|
|
Atoms : 45936
|
|
Bodies : 40692 (Original: 32596)
|
|
Count : 619 (Original: 1518)
|
|
Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209)
|
|
Tight : Yes
|
|
Variables : 327925 (Eliminated: 8994 Frozen: 311401)
|
|
Constraints : 2406917 (Binary: 91.4% Ternary: 6.6% Other: 2.0%)
|
|
|
|
Memory Peak : 530MB
|
|
Max. Length : 70 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 20.86s
|
|
Memory: 503MB (+13MB)
|
|
UNKNOWN
|
|
Iteration Time: 21.45s
|
|
|
|
Iteration 20
|
|
Queue: [(16,80,0,True), (17,85,0,True)]
|
|
Grounded Until: 75
|
|
Expected Memory: 585.0MB
|
|
Grounding... [('step', [76]), ('step', [77]), ('step', [78]), ('step', [79]), ('step', [80]), ('check', [80])]
|
|
Grounding Time: 0.48s
|
|
Memory: 518MB (+15MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 21
|
|
Time : 289.759s (Solving: 275.43s 1st Model: 0.00s Unsat: 7.40s)
|
|
CPU Time : 289.804s
|
|
|
|
Choices : 3919967 (Domain: 3804120)
|
|
Conflicts : 475574 (Analyzed: 475571)
|
|
Restarts : 1694 (Average: 280.74 Last: 208)
|
|
Model-Level : 212.0
|
|
Problems : 21 (Average Length: 39.14 Splits: 0)
|
|
Lemmas : 475571 (Deleted: 441027)
|
|
Binary : 13579 (Ratio: 2.86%)
|
|
Ternary : 2347 (Ratio: 0.49%)
|
|
Conflict : 475571 (Average Length: 769.3 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 475571 (Average: 7.53 Max: 411 Sum: 3583315)
|
|
Executed : 475520 (Average: 7.53 Max: 411 Sum: 3582461 Ratio: 99.98%)
|
|
Bounded : 51 (Average: 16.75 Max: 42 Sum: 854 Ratio: 0.02%)
|
|
|
|
Rules : 94613 (Original: 86518)
|
|
Atoms : 45936
|
|
Bodies : 40692 (Original: 32596)
|
|
Count : 619 (Original: 1518)
|
|
Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209)
|
|
Tight : Yes
|
|
Variables : 350486 (Eliminated: 8994 Frozen: 333962)
|
|
Constraints : 2579942 (Binary: 91.5% Ternary: 6.6% Other: 2.0%)
|
|
|
|
Memory Peak : 561MB
|
|
Max. Length : 75 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 18.22s
|
|
Memory: 521MB (+3MB)
|
|
UNKNOWN
|
|
Iteration Time: 18.96s
|
|
|
|
Iteration 21
|
|
Queue: [(17,85,0,True)]
|
|
Grounded Until: 80
|
|
Expected Memory: 603.0MB
|
|
Grounding... [('step', [81]), ('step', [82]), ('step', [83]), ('step', [84]), ('step', [85]), ('check', [85])]
|
|
Grounding Time: 0.35s
|
|
Memory: 521MB (+0MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 22
|
|
Time : 308.599s (Solving: 293.27s 1st Model: 0.00s Unsat: 7.40s)
|
|
CPU Time : 308.652s
|
|
|
|
Choices : 4144295 (Domain: 4028411)
|
|
Conflicts : 503747 (Analyzed: 503744)
|
|
Restarts : 1794 (Average: 280.79 Last: 208)
|
|
Model-Level : 212.0
|
|
Problems : 22 (Average Length: 41.32 Splits: 0)
|
|
Lemmas : 503744 (Deleted: 468601)
|
|
Binary : 13902 (Ratio: 2.76%)
|
|
Ternary : 2400 (Ratio: 0.48%)
|
|
Conflict : 503744 (Average Length: 769.0 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 503744 (Average: 7.50 Max: 422 Sum: 3776949)
|
|
Executed : 503693 (Average: 7.50 Max: 422 Sum: 3776095 Ratio: 99.98%)
|
|
Bounded : 51 (Average: 16.75 Max: 42 Sum: 854 Ratio: 0.02%)
|
|
|
|
Rules : 94613 (Original: 86518)
|
|
Atoms : 45936
|
|
Bodies : 40692 (Original: 32596)
|
|
Count : 619 (Original: 1518)
|
|
Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209)
|
|
Tight : Yes
|
|
Variables : 373047 (Eliminated: 8994 Frozen: 356523)
|
|
Constraints : 2752967 (Binary: 91.5% Ternary: 6.6% Other: 2.0%)
|
|
|
|
Memory Peak : 570MB
|
|
Max. Length : 80 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 18.23s
|
|
Memory: 538MB (+17MB)
|
|
UNKNOWN
|
|
Iteration Time: 18.86s
|
|
|
|
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,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
|
|
Grounded Until: 85
|
|
Blocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 23
|
|
Time : 318.795s (Solving: 303.36s 1st Model: 0.00s Unsat: 7.40s)
|
|
CPU Time : 318.852s
|
|
|
|
Choices : 4279001 (Domain: 4163117)
|
|
Conflicts : 531936 (Analyzed: 531933)
|
|
Restarts : 1894 (Average: 280.85 Last: 208)
|
|
Model-Level : 212.0
|
|
Problems : 23 (Average Length: 43.30 Splits: 0)
|
|
Lemmas : 531933 (Deleted: 495516)
|
|
Binary : 14207 (Ratio: 2.67%)
|
|
Ternary : 2487 (Ratio: 0.47%)
|
|
Conflict : 531933 (Average Length: 746.7 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 531933 (Average: 7.34 Max: 422 Sum: 3904971)
|
|
Executed : 531877 (Average: 7.34 Max: 422 Sum: 3903854 Ratio: 99.97%)
|
|
Bounded : 56 (Average: 19.95 Max: 87 Sum: 1117 Ratio: 0.03%)
|
|
|
|
Rules : 94613 (Original: 86518)
|
|
Atoms : 45936
|
|
Bodies : 40692 (Original: 32596)
|
|
Count : 619 (Original: 1518)
|
|
Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209)
|
|
Tight : Yes
|
|
Variables : 373047 (Eliminated: 8994 Frozen: 364053)
|
|
Constraints : 2752967 (Binary: 91.5% Ternary: 6.6% Other: 2.0%)
|
|
|
|
Memory Peak : 570MB
|
|
Max. Length : 85 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 10.16s
|
|
Memory: 539MB (+1MB)
|
|
UNKNOWN
|
|
Iteration Time: 10.20s
|
|
|
|
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,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
|
|
Grounded Until: 85
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 24
|
|
Time : 341.990s (Solving: 326.47s 1st Model: 0.00s Unsat: 7.40s)
|
|
CPU Time : 342.056s
|
|
|
|
Choices : 4445936 (Domain: 4330052)
|
|
Conflicts : 560051 (Analyzed: 560048)
|
|
Restarts : 1994 (Average: 280.87 Last: 208)
|
|
Model-Level : 212.0
|
|
Problems : 24 (Average Length: 45.12 Splits: 0)
|
|
Lemmas : 560048 (Deleted: 523095)
|
|
Binary : 14316 (Ratio: 2.56%)
|
|
Ternary : 2508 (Ratio: 0.45%)
|
|
Conflict : 560048 (Average Length: 770.6 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 560048 (Average: 7.25 Max: 422 Sum: 4058898)
|
|
Executed : 559992 (Average: 7.25 Max: 422 Sum: 4057781 Ratio: 99.97%)
|
|
Bounded : 56 (Average: 19.95 Max: 87 Sum: 1117 Ratio: 0.03%)
|
|
|
|
Rules : 94613 (Original: 86518)
|
|
Atoms : 45936
|
|
Bodies : 40692 (Original: 32596)
|
|
Count : 619 (Original: 1518)
|
|
Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209)
|
|
Tight : Yes
|
|
Variables : 373047 (Eliminated: 8994 Frozen: 364053)
|
|
Constraints : 2752926 (Binary: 91.5% Ternary: 6.6% Other: 2.0%)
|
|
|
|
Memory Peak : 570MB
|
|
Max. Length : 85 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 23.17s
|
|
Memory: 539MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 23.21s
|
|
|
|
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,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
|
|
Grounded Until: 85
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 25
|
|
Time : 363.254s (Solving: 347.64s 1st Model: 0.00s Unsat: 7.40s)
|
|
CPU Time : 363.328s
|
|
|
|
Choices : 4644807 (Domain: 4528923)
|
|
Conflicts : 588257 (Analyzed: 588254)
|
|
Restarts : 2094 (Average: 280.92 Last: 208)
|
|
Model-Level : 212.0
|
|
Problems : 25 (Average Length: 46.80 Splits: 0)
|
|
Lemmas : 588254 (Deleted: 550824)
|
|
Binary : 14516 (Ratio: 2.47%)
|
|
Ternary : 2528 (Ratio: 0.43%)
|
|
Conflict : 588254 (Average Length: 784.9 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 588254 (Average: 7.21 Max: 422 Sum: 4239616)
|
|
Executed : 588198 (Average: 7.21 Max: 422 Sum: 4238499 Ratio: 99.97%)
|
|
Bounded : 56 (Average: 19.95 Max: 87 Sum: 1117 Ratio: 0.03%)
|
|
|
|
Rules : 94613 (Original: 86518)
|
|
Atoms : 45936
|
|
Bodies : 40692 (Original: 32596)
|
|
Count : 619 (Original: 1518)
|
|
Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209)
|
|
Tight : Yes
|
|
Variables : 373047 (Eliminated: 8994 Frozen: 364053)
|
|
Constraints : 2752926 (Binary: 91.5% Ternary: 6.6% Other: 2.0%)
|
|
|
|
Memory Peak : 570MB
|
|
Max. Length : 85 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 21.24s
|
|
Memory: 539MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 21.27s
|
|
|
|
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,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
|
|
Grounded Until: 85
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 26
|
|
Time : 382.171s (Solving: 366.47s 1st Model: 0.00s Unsat: 7.40s)
|
|
CPU Time : 382.252s
|
|
|
|
Choices : 4830241 (Domain: 4714316)
|
|
Conflicts : 616452 (Analyzed: 616449)
|
|
Restarts : 2194 (Average: 280.97 Last: 208)
|
|
Model-Level : 212.0
|
|
Problems : 26 (Average Length: 48.35 Splits: 0)
|
|
Lemmas : 616449 (Deleted: 578167)
|
|
Binary : 14789 (Ratio: 2.40%)
|
|
Ternary : 2561 (Ratio: 0.42%)
|
|
Conflict : 616449 (Average Length: 796.1 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 616449 (Average: 7.14 Max: 422 Sum: 4404496)
|
|
Executed : 616393 (Average: 7.14 Max: 422 Sum: 4403379 Ratio: 99.97%)
|
|
Bounded : 56 (Average: 19.95 Max: 87 Sum: 1117 Ratio: 0.03%)
|
|
|
|
Rules : 94613 (Original: 86518)
|
|
Atoms : 45936
|
|
Bodies : 40692 (Original: 32596)
|
|
Count : 619 (Original: 1518)
|
|
Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209)
|
|
Tight : Yes
|
|
Variables : 373047 (Eliminated: 8994 Frozen: 364053)
|
|
Constraints : 2752926 (Binary: 91.5% Ternary: 6.6% Other: 2.0%)
|
|
|
|
Memory Peak : 570MB
|
|
Max. Length : 85 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 18.89s
|
|
Memory: 539MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 18.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,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
|
|
Grounded Until: 85
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 27
|
|
Time : 401.087s (Solving: 385.29s 1st Model: 0.00s Unsat: 7.40s)
|
|
CPU Time : 401.176s
|
|
|
|
Choices : 5047045 (Domain: 4930963)
|
|
Conflicts : 644660 (Analyzed: 644657)
|
|
Restarts : 2294 (Average: 281.02 Last: 208)
|
|
Model-Level : 212.0
|
|
Problems : 27 (Average Length: 49.78 Splits: 0)
|
|
Lemmas : 644657 (Deleted: 605343)
|
|
Binary : 15109 (Ratio: 2.34%)
|
|
Ternary : 2628 (Ratio: 0.41%)
|
|
Conflict : 644657 (Average Length: 801.5 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 644657 (Average: 7.13 Max: 422 Sum: 4599188)
|
|
Executed : 644601 (Average: 7.13 Max: 422 Sum: 4598071 Ratio: 99.98%)
|
|
Bounded : 56 (Average: 19.95 Max: 87 Sum: 1117 Ratio: 0.02%)
|
|
|
|
Rules : 94613 (Original: 86518)
|
|
Atoms : 45936
|
|
Bodies : 40692 (Original: 32596)
|
|
Count : 619 (Original: 1518)
|
|
Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209)
|
|
Tight : Yes
|
|
Variables : 373047 (Eliminated: 8994 Frozen: 364053)
|
|
Constraints : 2752926 (Binary: 91.5% Ternary: 6.6% Other: 2.0%)
|
|
|
|
Memory Peak : 570MB
|
|
Max. Length : 85 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 18.88s
|
|
Memory: 539MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 18.93s
|
|
|
|
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,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
|
|
Grounded Until: 85
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 28
|
|
Time : 418.204s (Solving: 402.31s 1st Model: 0.00s Unsat: 7.40s)
|
|
CPU Time : 418.300s
|
|
|
|
Choices : 5239786 (Domain: 5123692)
|
|
Conflicts : 672866 (Analyzed: 672863)
|
|
Restarts : 2394 (Average: 281.06 Last: 208)
|
|
Model-Level : 212.0
|
|
Problems : 28 (Average Length: 51.11 Splits: 0)
|
|
Lemmas : 672863 (Deleted: 629204)
|
|
Binary : 15390 (Ratio: 2.29%)
|
|
Ternary : 2662 (Ratio: 0.40%)
|
|
Conflict : 672863 (Average Length: 807.9 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 672863 (Average: 7.09 Max: 422 Sum: 4768425)
|
|
Executed : 672806 (Average: 7.08 Max: 422 Sum: 4767221 Ratio: 99.97%)
|
|
Bounded : 57 (Average: 21.12 Max: 87 Sum: 1204 Ratio: 0.03%)
|
|
|
|
Rules : 94613 (Original: 86518)
|
|
Atoms : 45936
|
|
Bodies : 40692 (Original: 32596)
|
|
Count : 619 (Original: 1518)
|
|
Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209)
|
|
Tight : Yes
|
|
Variables : 373047 (Eliminated: 8994 Frozen: 364053)
|
|
Constraints : 2752926 (Binary: 91.5% Ternary: 6.6% Other: 2.0%)
|
|
|
|
Memory Peak : 570MB
|
|
Max. Length : 85 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 17.09s
|
|
Memory: 539MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 17.13s
|
|
|
|
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,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
|
|
Grounded Until: 85
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 29
|
|
Time : 436.448s (Solving: 420.46s 1st Model: 0.00s Unsat: 7.40s)
|
|
CPU Time : 436.556s
|
|
|
|
Choices : 5467858 (Domain: 5351680)
|
|
Conflicts : 701060 (Analyzed: 701057)
|
|
Restarts : 2494 (Average: 281.10 Last: 208)
|
|
Model-Level : 212.0
|
|
Problems : 29 (Average Length: 52.34 Splits: 0)
|
|
Lemmas : 701057 (Deleted: 660279)
|
|
Binary : 15680 (Ratio: 2.24%)
|
|
Ternary : 2715 (Ratio: 0.39%)
|
|
Conflict : 701057 (Average Length: 812.9 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 701057 (Average: 7.09 Max: 422 Sum: 4970877)
|
|
Executed : 701000 (Average: 7.09 Max: 422 Sum: 4969673 Ratio: 99.98%)
|
|
Bounded : 57 (Average: 21.12 Max: 87 Sum: 1204 Ratio: 0.02%)
|
|
|
|
Rules : 94613 (Original: 86518)
|
|
Atoms : 45936
|
|
Bodies : 40692 (Original: 32596)
|
|
Count : 619 (Original: 1518)
|
|
Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209)
|
|
Tight : Yes
|
|
Variables : 373047 (Eliminated: 8994 Frozen: 364053)
|
|
Constraints : 2752943 (Binary: 91.5% Ternary: 6.6% Other: 2.0%)
|
|
|
|
Memory Peak : 570MB
|
|
Max. Length : 85 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 18.21s
|
|
Memory: 539MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 18.25s
|
|
|
|
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,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
|
|
Grounded Until: 85
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 30
|
|
Time : 454.565s (Solving: 438.46s 1st Model: 0.00s Unsat: 7.40s)
|
|
CPU Time : 454.680s
|
|
|
|
Choices : 5730727 (Domain: 5611371)
|
|
Conflicts : 729232 (Analyzed: 729229)
|
|
Restarts : 2594 (Average: 281.12 Last: 208)
|
|
Model-Level : 212.0
|
|
Problems : 30 (Average Length: 53.50 Splits: 0)
|
|
Lemmas : 729229 (Deleted: 687180)
|
|
Binary : 16233 (Ratio: 2.23%)
|
|
Ternary : 2797 (Ratio: 0.38%)
|
|
Conflict : 729229 (Average Length: 817.1 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 729229 (Average: 7.13 Max: 422 Sum: 5202937)
|
|
Executed : 729172 (Average: 7.13 Max: 422 Sum: 5201733 Ratio: 99.98%)
|
|
Bounded : 57 (Average: 21.12 Max: 87 Sum: 1204 Ratio: 0.02%)
|
|
|
|
Rules : 94613 (Original: 86518)
|
|
Atoms : 45936
|
|
Bodies : 40692 (Original: 32596)
|
|
Count : 619 (Original: 1518)
|
|
Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209)
|
|
Tight : Yes
|
|
Variables : 373047 (Eliminated: 8994 Frozen: 364053)
|
|
Constraints : 2752943 (Binary: 91.5% Ternary: 6.6% Other: 2.0%)
|
|
|
|
Memory Peak : 570MB
|
|
Max. Length : 85 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 18.08s
|
|
Memory: 539MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 18.13s
|
|
|
|
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,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
|
|
Grounded Until: 85
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 31
|
|
Time : 473.320s (Solving: 457.13s 1st Model: 0.00s Unsat: 7.40s)
|
|
CPU Time : 473.444s
|
|
|
|
Choices : 5981872 (Domain: 5862089)
|
|
Conflicts : 757399 (Analyzed: 757396)
|
|
Restarts : 2694 (Average: 281.14 Last: 208)
|
|
Model-Level : 212.0
|
|
Problems : 31 (Average Length: 54.58 Splits: 0)
|
|
Lemmas : 757396 (Deleted: 714426)
|
|
Binary : 16612 (Ratio: 2.19%)
|
|
Ternary : 2876 (Ratio: 0.38%)
|
|
Conflict : 757396 (Average Length: 824.6 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 757396 (Average: 7.16 Max: 422 Sum: 5421783)
|
|
Executed : 757339 (Average: 7.16 Max: 422 Sum: 5420579 Ratio: 99.98%)
|
|
Bounded : 57 (Average: 21.12 Max: 87 Sum: 1204 Ratio: 0.02%)
|
|
|
|
Rules : 94613 (Original: 86518)
|
|
Atoms : 45936
|
|
Bodies : 40692 (Original: 32596)
|
|
Count : 619 (Original: 1518)
|
|
Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209)
|
|
Tight : Yes
|
|
Variables : 373047 (Eliminated: 8994 Frozen: 364053)
|
|
Constraints : 2752943 (Binary: 91.5% Ternary: 6.6% Other: 2.0%)
|
|
|
|
Memory Peak : 570MB
|
|
Max. Length : 85 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 18.73s
|
|
Memory: 539MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 18.77s
|
|
|
|
Iteration 31
|
|
Queue: [(13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
|
|
Grounded Until: 85
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 32
|
|
Time : 492.304s (Solving: 476.02s 1st Model: 0.00s Unsat: 7.40s)
|
|
CPU Time : 492.436s
|
|
|
|
Choices : 6228255 (Domain: 6106842)
|
|
Conflicts : 785595 (Analyzed: 785592)
|
|
Restarts : 2794 (Average: 281.17 Last: 208)
|
|
Model-Level : 212.0
|
|
Problems : 32 (Average Length: 55.59 Splits: 0)
|
|
Lemmas : 785592 (Deleted: 741922)
|
|
Binary : 16886 (Ratio: 2.15%)
|
|
Ternary : 2920 (Ratio: 0.37%)
|
|
Conflict : 785592 (Average Length: 824.3 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 785592 (Average: 7.18 Max: 422 Sum: 5638165)
|
|
Executed : 785535 (Average: 7.18 Max: 422 Sum: 5636961 Ratio: 99.98%)
|
|
Bounded : 57 (Average: 21.12 Max: 87 Sum: 1204 Ratio: 0.02%)
|
|
|
|
Rules : 94613 (Original: 86518)
|
|
Atoms : 45936
|
|
Bodies : 40692 (Original: 32596)
|
|
Count : 619 (Original: 1518)
|
|
Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209)
|
|
Tight : Yes
|
|
Variables : 373047 (Eliminated: 8994 Frozen: 364053)
|
|
Constraints : 2752943 (Binary: 91.5% Ternary: 6.6% Other: 2.0%)
|
|
|
|
Memory Peak : 570MB
|
|
Max. Length : 85 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 18.96s
|
|
Memory: 539MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 18.99s
|
|
|
|
Iteration 32
|
|
Queue: [(14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
|
|
Grounded Until: 85
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 33
|
|
Time : 510.250s (Solving: 493.88s 1st Model: 0.00s Unsat: 7.40s)
|
|
CPU Time : 510.388s
|
|
|
|
Choices : 6411718 (Domain: 6290301)
|
|
Conflicts : 813772 (Analyzed: 813769)
|
|
Restarts : 2894 (Average: 281.19 Last: 208)
|
|
Model-Level : 212.0
|
|
Problems : 33 (Average Length: 56.55 Splits: 0)
|
|
Lemmas : 813769 (Deleted: 769442)
|
|
Binary : 17087 (Ratio: 2.10%)
|
|
Ternary : 2949 (Ratio: 0.36%)
|
|
Conflict : 813769 (Average Length: 824.7 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 813769 (Average: 7.12 Max: 422 Sum: 5794406)
|
|
Executed : 813712 (Average: 7.12 Max: 422 Sum: 5793202 Ratio: 99.98%)
|
|
Bounded : 57 (Average: 21.12 Max: 87 Sum: 1204 Ratio: 0.02%)
|
|
|
|
Rules : 94613 (Original: 86518)
|
|
Atoms : 45936
|
|
Bodies : 40692 (Original: 32596)
|
|
Count : 619 (Original: 1518)
|
|
Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209)
|
|
Tight : Yes
|
|
Variables : 373047 (Eliminated: 8994 Frozen: 364053)
|
|
Constraints : 2752943 (Binary: 91.5% Ternary: 6.6% Other: 2.0%)
|
|
|
|
Memory Peak : 570MB
|
|
Max. Length : 85 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 17.92s
|
|
Memory: 539MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 17.96s
|
|
|
|
Iteration 33
|
|
Queue: [(15,75,1,True), (16,80,1,True), (17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
|
|
Grounded Until: 85
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 34
|
|
Time : 528.226s (Solving: 511.78s 1st Model: 0.00s Unsat: 7.40s)
|
|
CPU Time : 528.372s
|
|
|
|
Choices : 6782170 (Domain: 6651138)
|
|
Conflicts : 841921 (Analyzed: 841918)
|
|
Restarts : 2994 (Average: 281.20 Last: 208)
|
|
Model-Level : 212.0
|
|
Problems : 34 (Average Length: 57.44 Splits: 0)
|
|
Lemmas : 841918 (Deleted: 796005)
|
|
Binary : 17873 (Ratio: 2.12%)
|
|
Ternary : 3072 (Ratio: 0.36%)
|
|
Conflict : 841918 (Average Length: 818.9 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 841918 (Average: 7.28 Max: 422 Sum: 6127115)
|
|
Executed : 841861 (Average: 7.28 Max: 422 Sum: 6125911 Ratio: 99.98%)
|
|
Bounded : 57 (Average: 21.12 Max: 87 Sum: 1204 Ratio: 0.02%)
|
|
|
|
Rules : 94613 (Original: 86518)
|
|
Atoms : 45936
|
|
Bodies : 40692 (Original: 32596)
|
|
Count : 619 (Original: 1518)
|
|
Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209)
|
|
Tight : Yes
|
|
Variables : 373047 (Eliminated: 8994 Frozen: 364053)
|
|
Constraints : 2752943 (Binary: 91.5% Ternary: 6.6% Other: 2.0%)
|
|
|
|
Memory Peak : 570MB
|
|
Max. Length : 85 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 17.96s
|
|
Memory: 539MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 17.99s
|
|
|
|
Iteration 34
|
|
Queue: [(16,80,1,True), (17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
|
|
Grounded Until: 85
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 35
|
|
Time : 548.030s (Solving: 531.50s 1st Model: 0.00s Unsat: 7.40s)
|
|
CPU Time : 548.184s
|
|
|
|
Choices : 7064505 (Domain: 6933096)
|
|
Conflicts : 870060 (Analyzed: 870057)
|
|
Restarts : 3094 (Average: 281.21 Last: 208)
|
|
Model-Level : 212.0
|
|
Problems : 35 (Average Length: 58.29 Splits: 0)
|
|
Lemmas : 870057 (Deleted: 823431)
|
|
Binary : 18171 (Ratio: 2.09%)
|
|
Ternary : 3117 (Ratio: 0.36%)
|
|
Conflict : 870057 (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 : 870057 (Average: 7.32 Max: 422 Sum: 6371425)
|
|
Executed : 870000 (Average: 7.32 Max: 422 Sum: 6370221 Ratio: 99.98%)
|
|
Bounded : 57 (Average: 21.12 Max: 87 Sum: 1204 Ratio: 0.02%)
|
|
|
|
Rules : 94613 (Original: 86518)
|
|
Atoms : 45936
|
|
Bodies : 40692 (Original: 32596)
|
|
Count : 619 (Original: 1518)
|
|
Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209)
|
|
Tight : Yes
|
|
Variables : 373047 (Eliminated: 8994 Frozen: 364053)
|
|
Constraints : 2752943 (Binary: 91.5% Ternary: 6.6% Other: 2.0%)
|
|
|
|
Memory Peak : 570MB
|
|
Max. Length : 85 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 19.78s
|
|
Memory: 539MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 19.81s
|
|
|
|
Iteration 35
|
|
Queue: [(17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
|
|
Grounded Until: 85
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 36
|
|
Time : 566.296s (Solving: 549.68s 1st Model: 0.00s Unsat: 7.40s)
|
|
CPU Time : 566.460s
|
|
|
|
Choices : 7461431 (Domain: 7325234)
|
|
Conflicts : 898209 (Analyzed: 898206)
|
|
Restarts : 3194 (Average: 281.22 Last: 208)
|
|
Model-Level : 212.0
|
|
Problems : 36 (Average Length: 59.08 Splits: 0)
|
|
Lemmas : 898206 (Deleted: 850370)
|
|
Binary : 18778 (Ratio: 2.09%)
|
|
Ternary : 3193 (Ratio: 0.36%)
|
|
Conflict : 898206 (Average Length: 822.2 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 898206 (Average: 7.49 Max: 422 Sum: 6724056)
|
|
Executed : 898149 (Average: 7.48 Max: 422 Sum: 6722852 Ratio: 99.98%)
|
|
Bounded : 57 (Average: 21.12 Max: 87 Sum: 1204 Ratio: 0.02%)
|
|
|
|
Rules : 94613 (Original: 86518)
|
|
Atoms : 45936
|
|
Bodies : 40692 (Original: 32596)
|
|
Count : 619 (Original: 1518)
|
|
Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209)
|
|
Tight : Yes
|
|
Variables : 373047 (Eliminated: 8994 Frozen: 364053)
|
|
Constraints : 2752943 (Binary: 91.5% Ternary: 6.6% Other: 2.0%)
|
|
|
|
Memory Peak : 570MB
|
|
Max. Length : 85 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 18.24s
|
|
Memory: 539MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 18.28s
|
|
|
|
Iteration 36
|
|
Queue: [(18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
|
|
Grounded Until: 85
|
|
Expected Memory: 621.0MB
|
|
Grounding... [('step', [86]), ('step', [87]), ('step', [88]), ('step', [89]), ('step', [90]), ('check', [90])]
|
|
Grounding Time: 0.32s
|
|
Memory: 539MB (+0MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 37
|
|
Time : 582.807s (Solving: 565.20s 1st Model: 0.00s Unsat: 7.40s)
|
|
CPU Time : 582.980s
|
|
|
|
Choices : 7643277 (Domain: 7507080)
|
|
Conflicts : 926448 (Analyzed: 926445)
|
|
Restarts : 3294 (Average: 281.25 Last: 208)
|
|
Model-Level : 212.0
|
|
Problems : 37 (Average Length: 59.97 Splits: 0)
|
|
Lemmas : 926445 (Deleted: 874406)
|
|
Binary : 18949 (Ratio: 2.05%)
|
|
Ternary : 3224 (Ratio: 0.35%)
|
|
Conflict : 926445 (Average Length: 811.3 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 926445 (Average: 7.42 Max: 422 Sum: 6878725)
|
|
Executed : 926388 (Average: 7.42 Max: 422 Sum: 6877521 Ratio: 99.98%)
|
|
Bounded : 57 (Average: 21.12 Max: 87 Sum: 1204 Ratio: 0.02%)
|
|
|
|
Rules : 94613 (Original: 86518)
|
|
Atoms : 45936
|
|
Bodies : 40692 (Original: 32596)
|
|
Count : 619 (Original: 1518)
|
|
Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209)
|
|
Tight : Yes
|
|
Variables : 395608 (Eliminated: 8994 Frozen: 379084)
|
|
Constraints : 2925968 (Binary: 91.5% Ternary: 6.6% Other: 2.0%)
|
|
|
|
Memory Peak : 589MB
|
|
Max. Length : 85 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 15.92s
|
|
Memory: 551MB (+12MB)
|
|
UNKNOWN
|
|
Iteration Time: 16.53s
|
|
|
|
Iteration 37
|
|
Queue: [(19,95,0,True), (20,100,0,True), (21,105,0,True)]
|
|
Grounded Until: 90
|
|
Expected Memory: 633.0MB
|
|
Grounding... [('step', [91]), ('step', [92]), ('step', [93]), ('step', [94]), ('step', [95]), ('check', [95])]
|
|
Grounding Time: 0.31s
|
|
Memory: 551MB (+0MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 38
|
|
Time : 604.129s (Solving: 585.54s 1st Model: 0.00s Unsat: 7.40s)
|
|
CPU Time : 604.308s
|
|
|
|
Choices : 7887991 (Domain: 7751790)
|
|
Conflicts : 954605 (Analyzed: 954602)
|
|
Restarts : 3394 (Average: 281.26 Last: 208)
|
|
Model-Level : 212.0
|
|
Problems : 38 (Average Length: 60.95 Splits: 0)
|
|
Lemmas : 954602 (Deleted: 905607)
|
|
Binary : 19248 (Ratio: 2.02%)
|
|
Ternary : 3267 (Ratio: 0.34%)
|
|
Conflict : 954602 (Average Length: 818.0 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 954602 (Average: 7.42 Max: 426 Sum: 7083953)
|
|
Executed : 954545 (Average: 7.42 Max: 426 Sum: 7082749 Ratio: 99.98%)
|
|
Bounded : 57 (Average: 21.12 Max: 87 Sum: 1204 Ratio: 0.02%)
|
|
|
|
Rules : 94613 (Original: 86518)
|
|
Atoms : 45936
|
|
Bodies : 40692 (Original: 32596)
|
|
Count : 619 (Original: 1518)
|
|
Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209)
|
|
Tight : Yes
|
|
Variables : 418169 (Eliminated: 8994 Frozen: 401645)
|
|
Constraints : 3098993 (Binary: 91.5% Ternary: 6.6% Other: 2.0%)
|
|
|
|
Memory Peak : 609MB
|
|
Max. Length : 90 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 20.74s
|
|
Memory: 573MB (+22MB)
|
|
UNKNOWN
|
|
Iteration Time: 21.34s
|
|
|
|
Iteration 38
|
|
Queue: [(20,100,0,True), (21,105,0,True)]
|
|
Grounded Until: 95
|
|
Expected Memory: 655.0MB
|
|
Grounding... [('step', [96]), ('step', [97]), ('step', [98]), ('step', [99]), ('step', [100]), ('check', [100])]
|
|
Grounding Time: 0.34s
|
|
Memory: 573MB (+0MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 39
|
|
Time : 622.153s (Solving: 602.52s 1st Model: 0.00s Unsat: 7.40s)
|
|
CPU Time : 622.340s
|
|
|
|
Choices : 8085108 (Domain: 7948889)
|
|
Conflicts : 982843 (Analyzed: 982840)
|
|
Restarts : 3494 (Average: 281.29 Last: 208)
|
|
Model-Level : 212.0
|
|
Problems : 39 (Average Length: 62.00 Splits: 0)
|
|
Lemmas : 982840 (Deleted: 933407)
|
|
Binary : 19431 (Ratio: 1.98%)
|
|
Ternary : 3289 (Ratio: 0.33%)
|
|
Conflict : 982840 (Average Length: 809.3 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 982840 (Average: 7.37 Max: 426 Sum: 7248294)
|
|
Executed : 982782 (Average: 7.37 Max: 426 Sum: 7246988 Ratio: 99.98%)
|
|
Bounded : 58 (Average: 22.52 Max: 102 Sum: 1306 Ratio: 0.02%)
|
|
|
|
Rules : 94613 (Original: 86518)
|
|
Atoms : 45936
|
|
Bodies : 40692 (Original: 32596)
|
|
Count : 619 (Original: 1518)
|
|
Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209)
|
|
Tight : Yes
|
|
Variables : 440730 (Eliminated: 8994 Frozen: 424206)
|
|
Constraints : 3272018 (Binary: 91.5% Ternary: 6.6% Other: 2.0%)
|
|
|
|
Memory Peak : 627MB
|
|
Max. Length : 95 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 17.39s
|
|
Memory: 626MB (+53MB)
|
|
UNKNOWN
|
|
Iteration Time: 18.04s
|
|
|
|
Iteration 39
|
|
Queue: [(21,105,0,True)]
|
|
Grounded Until: 100
|
|
Expected Memory: 708.0MB
|
|
Grounding... [('step', [101]), ('step', [102]), ('step', [103]), ('step', [104]), ('step', [105]), ('check', [105])]
|
|
Grounding Time: 0.35s
|
|
Memory: 626MB (+0MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 40
|
|
Time : 640.838s (Solving: 620.15s 1st Model: 0.00s Unsat: 7.40s)
|
|
CPU Time : 641.032s
|
|
|
|
Choices : 8299964 (Domain: 8163588)
|
|
Conflicts : 1011054 (Analyzed: 1011051)
|
|
Restarts : 3594 (Average: 281.32 Last: 208)
|
|
Model-Level : 212.0
|
|
Problems : 40 (Average Length: 63.12 Splits: 0)
|
|
Lemmas : 1011051 (Deleted: 960990)
|
|
Binary : 19575 (Ratio: 1.94%)
|
|
Ternary : 3324 (Ratio: 0.33%)
|
|
Conflict : 1011051 (Average Length: 803.4 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 1011051 (Average: 7.35 Max: 426 Sum: 7430291)
|
|
Executed : 1010993 (Average: 7.35 Max: 426 Sum: 7428985 Ratio: 99.98%)
|
|
Bounded : 58 (Average: 22.52 Max: 102 Sum: 1306 Ratio: 0.02%)
|
|
|
|
Rules : 94613 (Original: 86518)
|
|
Atoms : 45936
|
|
Bodies : 40692 (Original: 32596)
|
|
Count : 619 (Original: 1518)
|
|
Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209)
|
|
Tight : Yes
|
|
Variables : 463291 (Eliminated: 8994 Frozen: 446767)
|
|
Constraints : 3445029 (Binary: 91.5% Ternary: 6.6% Other: 2.0%)
|
|
|
|
Memory Peak : 682MB
|
|
Max. Length : 100 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 18.04s
|
|
Memory: 629MB (+3MB)
|
|
UNKNOWN
|
|
Iteration Time: 18.70s
|
|
|
|
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,2,False), (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 : 650.250s (Solving: 629.43s 1st Model: 0.00s Unsat: 16.67s)
|
|
CPU Time : 650.448s
|
|
|
|
Choices : 8456222 (Domain: 8319846)
|
|
Conflicts : 1039175 (Analyzed: 1039171)
|
|
Restarts : 3693 (Average: 281.39 Last: 208)
|
|
Model-Level : 212.0
|
|
Problems : 41 (Average Length: 64.20 Splits: 0)
|
|
Lemmas : 1039171 (Deleted: 988171)
|
|
Binary : 19785 (Ratio: 1.90%)
|
|
Ternary : 3407 (Ratio: 0.33%)
|
|
Conflict : 1039171 (Average Length: 789.2 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 1039171 (Average: 7.29 Max: 426 Sum: 7580351)
|
|
Executed : 1039111 (Average: 7.29 Max: 426 Sum: 7578937 Ratio: 99.98%)
|
|
Bounded : 60 (Average: 23.57 Max: 107 Sum: 1414 Ratio: 0.02%)
|
|
|
|
Rules : 94613 (Original: 86518)
|
|
Atoms : 45936
|
|
Bodies : 40692 (Original: 32596)
|
|
Count : 619 (Original: 1518)
|
|
Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209)
|
|
Tight : Yes
|
|
Variables : 463291 (Eliminated: 8994 Frozen: 454297)
|
|
Constraints : 3445029 (Binary: 91.5% Ternary: 6.6% Other: 2.0%)
|
|
|
|
Memory Peak : 682MB
|
|
Max. Length : 105 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 9.36s
|
|
Memory: 629MB (+0MB)
|
|
UNSAT
|
|
Iteration Time: 9.42s
|
|
|
|
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,2,False), (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 : 675.013s (Solving: 654.09s 1st Model: 0.00s Unsat: 16.67s)
|
|
CPU Time : 675.224s
|
|
|
|
Choices : 8601062 (Domain: 8464686)
|
|
Conflicts : 1067320 (Analyzed: 1067316)
|
|
Restarts : 3793 (Average: 281.39 Last: 208)
|
|
Model-Level : 212.0
|
|
Problems : 42 (Average Length: 65.21 Splits: 0)
|
|
Lemmas : 1067316 (Deleted: 1015695)
|
|
Binary : 19938 (Ratio: 1.87%)
|
|
Ternary : 3428 (Ratio: 0.32%)
|
|
Conflict : 1067316 (Average Length: 793.8 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 1067316 (Average: 7.23 Max: 426 Sum: 7714494)
|
|
Executed : 1067255 (Average: 7.23 Max: 426 Sum: 7712973 Ratio: 99.98%)
|
|
Bounded : 61 (Average: 24.93 Max: 107 Sum: 1521 Ratio: 0.02%)
|
|
|
|
Rules : 94613 (Original: 86518)
|
|
Atoms : 45936
|
|
Bodies : 40692 (Original: 32596)
|
|
Count : 619 (Original: 1518)
|
|
Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209)
|
|
Tight : Yes
|
|
Variables : 463291 (Eliminated: 8994 Frozen: 454297)
|
|
Constraints : 3445015 (Binary: 91.5% Ternary: 6.6% Other: 2.0%)
|
|
|
|
Memory Peak : 682MB
|
|
Max. Length : 105 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 24.74s
|
|
Memory: 629MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 24.78s
|
|
|
|
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,2,False), (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 : 700.352s (Solving: 679.31s 1st Model: 0.00s Unsat: 16.67s)
|
|
CPU Time : 700.576s
|
|
|
|
Choices : 8769209 (Domain: 8632833)
|
|
Conflicts : 1095491 (Analyzed: 1095487)
|
|
Restarts : 3893 (Average: 281.40 Last: 208)
|
|
Model-Level : 212.0
|
|
Problems : 43 (Average Length: 66.19 Splits: 0)
|
|
Lemmas : 1095487 (Deleted: 1043519)
|
|
Binary : 20111 (Ratio: 1.84%)
|
|
Ternary : 3439 (Ratio: 0.31%)
|
|
Conflict : 1095487 (Average Length: 818.0 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 1095487 (Average: 7.18 Max: 426 Sum: 7864412)
|
|
Executed : 1095426 (Average: 7.18 Max: 426 Sum: 7862891 Ratio: 99.98%)
|
|
Bounded : 61 (Average: 24.93 Max: 107 Sum: 1521 Ratio: 0.02%)
|
|
|
|
Rules : 94613 (Original: 86518)
|
|
Atoms : 45936
|
|
Bodies : 40692 (Original: 32596)
|
|
Count : 619 (Original: 1518)
|
|
Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209)
|
|
Tight : Yes
|
|
Variables : 463291 (Eliminated: 8994 Frozen: 454297)
|
|
Constraints : 3445001 (Binary: 91.5% Ternary: 6.6% Other: 2.0%)
|
|
|
|
Memory Peak : 693MB
|
|
Max. Length : 105 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 25.30s
|
|
Memory: 693MB (+64MB)
|
|
UNKNOWN
|
|
Iteration Time: 25.35s
|
|
|
|
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,2,False), (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 : 718.784s (Solving: 697.64s 1st Model: 0.00s Unsat: 16.67s)
|
|
CPU Time : 719.016s
|
|
|
|
Choices : 8947892 (Domain: 8811516)
|
|
Conflicts : 1123688 (Analyzed: 1123684)
|
|
Restarts : 3993 (Average: 281.41 Last: 208)
|
|
Model-Level : 212.0
|
|
Problems : 44 (Average Length: 67.11 Splits: 0)
|
|
Lemmas : 1123684 (Deleted: 1071211)
|
|
Binary : 20240 (Ratio: 1.80%)
|
|
Ternary : 3456 (Ratio: 0.31%)
|
|
Conflict : 1123684 (Average Length: 820.5 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 1123684 (Average: 7.14 Max: 426 Sum: 8021804)
|
|
Executed : 1123623 (Average: 7.14 Max: 426 Sum: 8020283 Ratio: 99.98%)
|
|
Bounded : 61 (Average: 24.93 Max: 107 Sum: 1521 Ratio: 0.02%)
|
|
|
|
Rules : 94613 (Original: 86518)
|
|
Atoms : 45936
|
|
Bodies : 40692 (Original: 32596)
|
|
Count : 619 (Original: 1518)
|
|
Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209)
|
|
Tight : Yes
|
|
Variables : 463291 (Eliminated: 8994 Frozen: 454297)
|
|
Constraints : 3445001 (Binary: 91.5% Ternary: 6.6% Other: 2.0%)
|
|
|
|
Memory Peak : 693MB
|
|
Max. Length : 105 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 18.40s
|
|
Memory: 693MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 18.44s
|
|
|
|
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,2,False), (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 : 736.806s (Solving: 715.53s 1st Model: 0.00s Unsat: 16.67s)
|
|
CPU Time : 737.048s
|
|
|
|
Choices : 9151203 (Domain: 9014827)
|
|
Conflicts : 1151869 (Analyzed: 1151865)
|
|
Restarts : 4093 (Average: 281.42 Last: 208)
|
|
Model-Level : 212.0
|
|
Problems : 45 (Average Length: 68.00 Splits: 0)
|
|
Lemmas : 1151865 (Deleted: 1098669)
|
|
Binary : 20406 (Ratio: 1.77%)
|
|
Ternary : 3501 (Ratio: 0.30%)
|
|
Conflict : 1151865 (Average Length: 819.5 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 1151865 (Average: 7.12 Max: 426 Sum: 8200967)
|
|
Executed : 1151804 (Average: 7.12 Max: 426 Sum: 8199446 Ratio: 99.98%)
|
|
Bounded : 61 (Average: 24.93 Max: 107 Sum: 1521 Ratio: 0.02%)
|
|
|
|
Rules : 94613 (Original: 86518)
|
|
Atoms : 45936
|
|
Bodies : 40692 (Original: 32596)
|
|
Count : 619 (Original: 1518)
|
|
Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209)
|
|
Tight : Yes
|
|
Variables : 463291 (Eliminated: 8994 Frozen: 454297)
|
|
Constraints : 3445001 (Binary: 91.5% Ternary: 6.6% Other: 2.0%)
|
|
|
|
Memory Peak : 693MB
|
|
Max. Length : 105 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 17.98s
|
|
Memory: 693MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 18.03s
|
|
|
|
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,2,False), (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 : 754.954s (Solving: 733.57s 1st Model: 0.00s Unsat: 16.67s)
|
|
CPU Time : 755.204s
|
|
|
|
Choices : 9352554 (Domain: 9215956)
|
|
Conflicts : 1180060 (Analyzed: 1180056)
|
|
Restarts : 4193 (Average: 281.43 Last: 208)
|
|
Model-Level : 212.0
|
|
Problems : 46 (Average Length: 68.85 Splits: 0)
|
|
Lemmas : 1180056 (Deleted: 1126024)
|
|
Binary : 20672 (Ratio: 1.75%)
|
|
Ternary : 3546 (Ratio: 0.30%)
|
|
Conflict : 1180056 (Average Length: 820.8 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 1180056 (Average: 7.10 Max: 426 Sum: 8376547)
|
|
Executed : 1179995 (Average: 7.10 Max: 426 Sum: 8375026 Ratio: 99.98%)
|
|
Bounded : 61 (Average: 24.93 Max: 107 Sum: 1521 Ratio: 0.02%)
|
|
|
|
Rules : 94613 (Original: 86518)
|
|
Atoms : 45936
|
|
Bodies : 40692 (Original: 32596)
|
|
Count : 619 (Original: 1518)
|
|
Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209)
|
|
Tight : Yes
|
|
Variables : 463291 (Eliminated: 8994 Frozen: 454297)
|
|
Constraints : 3445001 (Binary: 91.5% Ternary: 6.6% Other: 2.0%)
|
|
|
|
Memory Peak : 693MB
|
|
Max. Length : 105 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 18.12s
|
|
Memory: 693MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 18.16s
|
|
|
|
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,2,False), (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 : 772.790s (Solving: 751.28s 1st Model: 0.00s Unsat: 16.67s)
|
|
CPU Time : 773.048s
|
|
|
|
Choices : 9572653 (Domain: 9435574)
|
|
Conflicts : 1208245 (Analyzed: 1208241)
|
|
Restarts : 4293 (Average: 281.44 Last: 208)
|
|
Model-Level : 212.0
|
|
Problems : 47 (Average Length: 69.66 Splits: 0)
|
|
Lemmas : 1208241 (Deleted: 1153476)
|
|
Binary : 20930 (Ratio: 1.73%)
|
|
Ternary : 3599 (Ratio: 0.30%)
|
|
Conflict : 1208241 (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 : 1208241 (Average: 7.09 Max: 426 Sum: 8566212)
|
|
Executed : 1208180 (Average: 7.09 Max: 426 Sum: 8564691 Ratio: 99.98%)
|
|
Bounded : 61 (Average: 24.93 Max: 107 Sum: 1521 Ratio: 0.02%)
|
|
|
|
Rules : 94613 (Original: 86518)
|
|
Atoms : 45936
|
|
Bodies : 40692 (Original: 32596)
|
|
Count : 619 (Original: 1518)
|
|
Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209)
|
|
Tight : Yes
|
|
Variables : 463291 (Eliminated: 8994 Frozen: 454297)
|
|
Constraints : 3445001 (Binary: 91.5% Ternary: 6.6% Other: 2.0%)
|
|
|
|
Memory Peak : 693MB
|
|
Max. Length : 105 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 17.79s
|
|
Memory: 693MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 17.85s
|
|
|
|
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,2,False), (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 : 790.010s (Solving: 768.37s 1st Model: 0.00s Unsat: 16.67s)
|
|
CPU Time : 790.276s
|
|
|
|
Choices : 9786609 (Domain: 9649467)
|
|
Conflicts : 1236454 (Analyzed: 1236450)
|
|
Restarts : 4393 (Average: 281.46 Last: 208)
|
|
Model-Level : 212.0
|
|
Problems : 48 (Average Length: 70.44 Splits: 0)
|
|
Lemmas : 1236450 (Deleted: 1181052)
|
|
Binary : 21219 (Ratio: 1.72%)
|
|
Ternary : 3640 (Ratio: 0.29%)
|
|
Conflict : 1236450 (Average Length: 824.1 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 1236450 (Average: 7.08 Max: 426 Sum: 8748483)
|
|
Executed : 1236389 (Average: 7.07 Max: 426 Sum: 8746962 Ratio: 99.98%)
|
|
Bounded : 61 (Average: 24.93 Max: 107 Sum: 1521 Ratio: 0.02%)
|
|
|
|
Rules : 94613 (Original: 86518)
|
|
Atoms : 45936
|
|
Bodies : 40692 (Original: 32596)
|
|
Count : 619 (Original: 1518)
|
|
Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209)
|
|
Tight : Yes
|
|
Variables : 463291 (Eliminated: 8994 Frozen: 454297)
|
|
Constraints : 3445001 (Binary: 91.5% Ternary: 6.6% Other: 2.0%)
|
|
|
|
Memory Peak : 693MB
|
|
Max. Length : 105 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 17.18s
|
|
Memory: 693MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 17.23s
|
|
|
|
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,2,False), (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 : 806.202s (Solving: 784.44s 1st Model: 0.00s Unsat: 16.67s)
|
|
CPU Time : 806.472s
|
|
|
|
Choices : 10026136 (Domain: 9888329)
|
|
Conflicts : 1264633 (Analyzed: 1264629)
|
|
Restarts : 4493 (Average: 281.47 Last: 208)
|
|
Model-Level : 212.0
|
|
Problems : 49 (Average Length: 71.18 Splits: 0)
|
|
Lemmas : 1264629 (Deleted: 1208327)
|
|
Binary : 21668 (Ratio: 1.71%)
|
|
Ternary : 3674 (Ratio: 0.29%)
|
|
Conflict : 1264629 (Average Length: 824.8 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 1264629 (Average: 7.08 Max: 426 Sum: 8948813)
|
|
Executed : 1264568 (Average: 7.08 Max: 426 Sum: 8947292 Ratio: 99.98%)
|
|
Bounded : 61 (Average: 24.93 Max: 107 Sum: 1521 Ratio: 0.02%)
|
|
|
|
Rules : 94613 (Original: 86518)
|
|
Atoms : 45936
|
|
Bodies : 40692 (Original: 32596)
|
|
Count : 619 (Original: 1518)
|
|
Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209)
|
|
Tight : Yes
|
|
Variables : 463291 (Eliminated: 8994 Frozen: 454297)
|
|
Constraints : 3445001 (Binary: 91.5% Ternary: 6.6% Other: 2.0%)
|
|
|
|
Memory Peak : 693MB
|
|
Max. Length : 105 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 16.15s
|
|
Memory: 693MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 16.20s
|
|
|
|
Iteration 49
|
|
Queue: [(13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,2,False), (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 : 823.151s (Solving: 801.27s 1st Model: 0.00s Unsat: 16.67s)
|
|
CPU Time : 823.428s
|
|
|
|
Choices : 10216776 (Domain: 10078969)
|
|
Conflicts : 1292793 (Analyzed: 1292789)
|
|
Restarts : 4593 (Average: 281.47 Last: 208)
|
|
Model-Level : 212.0
|
|
Problems : 50 (Average Length: 71.90 Splits: 0)
|
|
Lemmas : 1292789 (Deleted: 1235993)
|
|
Binary : 21766 (Ratio: 1.68%)
|
|
Ternary : 3686 (Ratio: 0.29%)
|
|
Conflict : 1292789 (Average Length: 824.2 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 1292789 (Average: 7.05 Max: 426 Sum: 9110026)
|
|
Executed : 1292728 (Average: 7.05 Max: 426 Sum: 9108505 Ratio: 99.98%)
|
|
Bounded : 61 (Average: 24.93 Max: 107 Sum: 1521 Ratio: 0.02%)
|
|
|
|
Rules : 94613 (Original: 86518)
|
|
Atoms : 45936
|
|
Bodies : 40692 (Original: 32596)
|
|
Count : 619 (Original: 1518)
|
|
Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209)
|
|
Tight : Yes
|
|
Variables : 463291 (Eliminated: 8994 Frozen: 454297)
|
|
Constraints : 3445001 (Binary: 91.5% Ternary: 6.6% Other: 2.0%)
|
|
|
|
Memory Peak : 693MB
|
|
Max. Length : 105 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 16.91s
|
|
Memory: 693MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 16.96s
|
|
|
|
Iteration 50
|
|
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 : 51
|
|
Time : 843.238s (Solving: 821.23s 1st Model: 0.00s Unsat: 16.67s)
|
|
CPU Time : 843.524s
|
|
|
|
Choices : 10496385 (Domain: 10358552)
|
|
Conflicts : 1320996 (Analyzed: 1320992)
|
|
Restarts : 4693 (Average: 281.48 Last: 208)
|
|
Model-Level : 212.0
|
|
Problems : 51 (Average Length: 72.59 Splits: 0)
|
|
Lemmas : 1320992 (Deleted: 1263506)
|
|
Binary : 22044 (Ratio: 1.67%)
|
|
Ternary : 3737 (Ratio: 0.28%)
|
|
Conflict : 1320992 (Average Length: 826.7 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 1320992 (Average: 7.08 Max: 426 Sum: 9351586)
|
|
Executed : 1320931 (Average: 7.08 Max: 426 Sum: 9350065 Ratio: 99.98%)
|
|
Bounded : 61 (Average: 24.93 Max: 107 Sum: 1521 Ratio: 0.02%)
|
|
|
|
Rules : 94613 (Original: 86518)
|
|
Atoms : 45936
|
|
Bodies : 40692 (Original: 32596)
|
|
Count : 619 (Original: 1518)
|
|
Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209)
|
|
Tight : Yes
|
|
Variables : 463291 (Eliminated: 8994 Frozen: 454297)
|
|
Constraints : 3445001 (Binary: 91.5% Ternary: 6.6% Other: 2.0%)
|
|
|
|
Memory Peak : 693MB
|
|
Max. Length : 105 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 20.05s
|
|
Memory: 693MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 20.10s
|
|
|
|
Iteration 51
|
|
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 : 52
|
|
Time : 862.265s (Solving: 840.15s 1st Model: 0.00s Unsat: 16.67s)
|
|
CPU Time : 862.560s
|
|
|
|
Choices : 10764696 (Domain: 10626340)
|
|
Conflicts : 1349196 (Analyzed: 1349192)
|
|
Restarts : 4793 (Average: 281.49 Last: 208)
|
|
Model-Level : 212.0
|
|
Problems : 52 (Average Length: 73.25 Splits: 0)
|
|
Lemmas : 1349192 (Deleted: 1291046)
|
|
Binary : 22249 (Ratio: 1.65%)
|
|
Ternary : 3767 (Ratio: 0.28%)
|
|
Conflict : 1349192 (Average Length: 828.5 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 1349192 (Average: 7.10 Max: 426 Sum: 9578947)
|
|
Executed : 1349131 (Average: 7.10 Max: 426 Sum: 9577426 Ratio: 99.98%)
|
|
Bounded : 61 (Average: 24.93 Max: 107 Sum: 1521 Ratio: 0.02%)
|
|
|
|
Rules : 94613 (Original: 86518)
|
|
Atoms : 45936
|
|
Bodies : 40692 (Original: 32596)
|
|
Count : 619 (Original: 1518)
|
|
Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209)
|
|
Tight : Yes
|
|
Variables : 463291 (Eliminated: 8994 Frozen: 454297)
|
|
Constraints : 3445001 (Binary: 91.5% Ternary: 6.6% Other: 2.0%)
|
|
|
|
Memory Peak : 693MB
|
|
Max. Length : 105 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 19.00s
|
|
Memory: 693MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 19.04s
|
|
|
|
Iteration 52
|
|
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 : 53
|
|
Time : 883.700s (Solving: 861.48s 1st Model: 0.00s Unsat: 16.67s)
|
|
CPU Time : 884.004s
|
|
|
|
Choices : 11013874 (Domain: 10875518)
|
|
Conflicts : 1377434 (Analyzed: 1377430)
|
|
Restarts : 4893 (Average: 281.51 Last: 208)
|
|
Model-Level : 212.0
|
|
Problems : 53 (Average Length: 73.89 Splits: 0)
|
|
Lemmas : 1377430 (Deleted: 1318807)
|
|
Binary : 22405 (Ratio: 1.63%)
|
|
Ternary : 3804 (Ratio: 0.28%)
|
|
Conflict : 1377430 (Average Length: 834.0 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 1377430 (Average: 7.10 Max: 426 Sum: 9783579)
|
|
Executed : 1377369 (Average: 7.10 Max: 426 Sum: 9782058 Ratio: 99.98%)
|
|
Bounded : 61 (Average: 24.93 Max: 107 Sum: 1521 Ratio: 0.02%)
|
|
|
|
Rules : 94613 (Original: 86518)
|
|
Atoms : 45936
|
|
Bodies : 40692 (Original: 32596)
|
|
Count : 619 (Original: 1518)
|
|
Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209)
|
|
Tight : Yes
|
|
Variables : 463291 (Eliminated: 8994 Frozen: 454297)
|
|
Constraints : 3445001 (Binary: 91.5% Ternary: 6.6% Other: 2.0%)
|
|
|
|
Memory Peak : 693MB
|
|
Max. Length : 105 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 21.41s
|
|
Memory: 693MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 21.45s
|
|
|
|
Iteration 53
|
|
Queue: [(21,105,1,True), (22,110,0,True), (23,115,0,True)]
|
|
Grounded Until: 105
|
|
Unblocking actions...
|
|
Solving...
|
|
*** Info : (planner): INTERRUPTED by signal!
|
|
UNKNOWN
|
|
|
|
INTERRUPTED : 1
|
|
|
|
Models : 0+
|
|
Calls : 54
|
|
Time : 894.855s (Solving: 872.53s 1st Model: 0.00s Unsat: 16.67s)
|
|
CPU Time : 895.144s
|
|
|
|
Choices : 11145256 (Domain: 11006899)
|
|
Conflicts : 1391952 (Analyzed: 1391948)
|
|
Restarts : 4954 (Average: 280.97 Last: 208)
|
|
Model-Level : 212.0
|
|
Problems : 54 (Average Length: 74.50 Splits: 0)
|
|
Lemmas : 1391948 (Deleted: 1335497)
|
|
Binary : 22457 (Ratio: 1.61%)
|
|
Ternary : 3815 (Ratio: 0.27%)
|
|
Conflict : 1391948 (Average Length: 833.6 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 1391948 (Average: 7.11 Max: 426 Sum: 9892370)
|
|
Executed : 1391887 (Average: 7.11 Max: 426 Sum: 9890849 Ratio: 99.98%)
|
|
Bounded : 61 (Average: 24.93 Max: 107 Sum: 1521 Ratio: 0.02%)
|
|
|
|
Rules : 94613 (Original: 86518)
|
|
Atoms : 45936
|
|
Bodies : 40692 (Original: 32596)
|
|
Count : 619 (Original: 1518)
|
|
Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209)
|
|
Tight : Yes
|
|
Variables : 463291 (Eliminated: 8994 Frozen: 454297)
|
|
Constraints : 3445001 (Binary: 91.5% Ternary: 6.6% Other: 2.0%)
|
|
|
|
Memory Peak : 693MB
|
|
Max. Length : 105 steps
|
|
Models : 1
|
|
|
|
|