1328 lines
48 KiB
Plaintext
1328 lines
48 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-2.pddl']
|
||
|
|
INFO translator arguments: []
|
||
|
|
INFO translator time limit: None
|
||
|
|
INFO translator memory limit: None
|
||
|
|
INFO callstring: /home/pluehne/.usr/bin/python /home/wv/bin/linux/64/fast-downward-10997/builds/release64/bin/translate/translate.py /home/pluehne/Documents/ASP/pddl-instances/ipc-2011/domains/barman-sequential-satisficing/domain.pddl /home/pluehne/Documents/ASP/pddl-instances/ipc-2011/domains/barman-sequential-satisficing/instances/instance-2.pddl
|
||
|
|
Parsing...
|
||
|
|
Parsing: [0.040s CPU, 0.045s wall-clock]
|
||
|
|
Normalizing task... [0.010s CPU, 0.003s wall-clock]
|
||
|
|
Instantiating...
|
||
|
|
Generating Datalog program... [0.000s CPU, 0.011s wall-clock]
|
||
|
|
Normalizing Datalog program...
|
||
|
|
Normalizing Datalog program: [0.060s CPU, 0.053s wall-clock]
|
||
|
|
Preparing model... [0.020s CPU, 0.027s wall-clock]
|
||
|
|
Generated 115 rules.
|
||
|
|
Computing model... [0.340s CPU, 0.335s wall-clock]
|
||
|
|
2025 relevant atoms
|
||
|
|
2105 auxiliary atoms
|
||
|
|
4130 final queue length
|
||
|
|
7122 total queue pushes
|
||
|
|
Completing instantiation... [0.600s CPU, 0.598s wall-clock]
|
||
|
|
Instantiating: [1.020s CPU, 1.030s wall-clock]
|
||
|
|
Computing fact groups...
|
||
|
|
Finding invariants...
|
||
|
|
24 initial candidates
|
||
|
|
Finding invariants: [0.110s CPU, 0.109s wall-clock]
|
||
|
|
Checking invariant weight... [0.000s CPU, 0.001s wall-clock]
|
||
|
|
Instantiating groups... [0.010s CPU, 0.006s wall-clock]
|
||
|
|
Collecting mutex groups... [0.000s CPU, 0.000s wall-clock]
|
||
|
|
Choosing groups...
|
||
|
|
207 uncovered facts
|
||
|
|
Choosing groups: [0.000s CPU, 0.001s wall-clock]
|
||
|
|
Building translation key... [0.010s CPU, 0.008s wall-clock]
|
||
|
|
Computing fact groups: [0.140s CPU, 0.142s 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.010s CPU, 0.002s wall-clock]
|
||
|
|
Translating task...
|
||
|
|
Processing axioms...
|
||
|
|
Simplifying axioms... [0.000s CPU, 0.000s wall-clock]
|
||
|
|
Processing axioms: [0.030s CPU, 0.033s wall-clock]
|
||
|
|
Translating task: [0.650s CPU, 0.655s 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.308s 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.260s CPU, 0.275s wall-clock]
|
||
|
|
Done! [2.670s CPU, 2.696s 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.654s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
|
||
|
|
CPU Time : 0.560s
|
||
|
|
|
||
|
|
Choices : 0
|
||
|
|
Conflicts : 0 (Analyzed: 0)
|
||
|
|
Restarts : 0
|
||
|
|
Problems : 1 (Average Length: 2.00 Splits: 0)
|
||
|
|
Lemmas : 0 (Deleted: 0)
|
||
|
|
Binary : 0 (Ratio: 0.00%)
|
||
|
|
Ternary : 0 (Ratio: 0.00%)
|
||
|
|
Conflict : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 0 (Average: 0.00 Max: 0 Sum: 0)
|
||
|
|
Executed : 0 (Average: 0.00 Max: 0 Sum: 0 Ratio: 0.00%)
|
||
|
|
Bounded : 0 (Average: 0.00 Max: 0 Sum: 0 Ratio: 100.00%)
|
||
|
|
|
||
|
|
Rules : 38518
|
||
|
|
Atoms : 38518
|
||
|
|
Bodies : 1 (Original: 0)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 0 (Eliminated: 0 Frozen: 0)
|
||
|
|
Constraints : 0 (Binary: 0.0% Ternary: 0.0% Other: 0.0%)
|
||
|
|
|
||
|
|
Memory Peak : 222MB
|
||
|
|
Max. Length : 0 steps
|
||
|
|
Models : 0
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 0.00s
|
||
|
|
Memory: 158MB (+72MB)
|
||
|
|
UNSAT
|
||
|
|
Iteration Time: 0.00s
|
||
|
|
|
||
|
|
Iteration 2
|
||
|
|
Queue: [(1,5,0,True), (2,10,0,True), (3,15,0,True), (4,20,0,True), (5,25,0,True), (6,30,0,True)]
|
||
|
|
Grounded Until: 0
|
||
|
|
Expected Memory: 158MB
|
||
|
|
Grounding... [('step', [1]), ('step', [2]), ('step', [3]), ('step', [4]), ('step', [5]), ('check', [5])]
|
||
|
|
Grounding Time: 0.15s
|
||
|
|
Memory: 158MB (+0MB)
|
||
|
|
Unblocking actions...
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 1+
|
||
|
|
Calls : 2
|
||
|
|
Time : 0.980s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
|
||
|
|
CPU Time : 0.884s
|
||
|
|
|
||
|
|
Choices : 152 (Domain: 73)
|
||
|
|
Conflicts : 2 (Analyzed: 2)
|
||
|
|
Restarts : 0
|
||
|
|
Model-Level : 147.0
|
||
|
|
Problems : 2 (Average Length: 4.50 Splits: 0)
|
||
|
|
Lemmas : 2 (Deleted: 0)
|
||
|
|
Binary : 0 (Ratio: 0.00%)
|
||
|
|
Ternary : 0 (Ratio: 0.00%)
|
||
|
|
Conflict : 2 (Average Length: 23.0 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 2 (Average: 6.00 Max: 11 Sum: 12)
|
||
|
|
Executed : 2 (Average: 6.00 Max: 11 Sum: 12 Ratio: 100.00%)
|
||
|
|
Bounded : 0 (Average: 0.00 Max: 0 Sum: 0 Ratio: 0.00%)
|
||
|
|
|
||
|
|
Rules : 38518
|
||
|
|
Atoms : 38518
|
||
|
|
Bodies : 1 (Original: 0)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 10322 (Eliminated: 0 Frozen: 10322)
|
||
|
|
Constraints : 36431 (Binary: 95.0% Ternary: 3.5% Other: 1.5%)
|
||
|
|
|
||
|
|
Memory Peak : 222MB
|
||
|
|
Max. Length : 0 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 0.10s
|
||
|
|
Memory: 160MB (+2MB)
|
||
|
|
SAT
|
||
|
|
Testing...
|
||
|
|
NOT SERIALIZABLE
|
||
|
|
Testing Time: 0.62s
|
||
|
|
Memory: 178MB (+18MB)
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0
|
||
|
|
Calls : 3
|
||
|
|
Time : 1.079s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
|
||
|
|
CPU Time : 0.984s
|
||
|
|
|
||
|
|
Choices : 161 (Domain: 78)
|
||
|
|
Conflicts : 9 (Analyzed: 8)
|
||
|
|
Restarts : 0
|
||
|
|
Model-Level : 147.0
|
||
|
|
Problems : 3 (Average Length: 5.33 Splits: 0)
|
||
|
|
Lemmas : 8 (Deleted: 0)
|
||
|
|
Binary : 1 (Ratio: 12.50%)
|
||
|
|
Ternary : 2 (Ratio: 25.00%)
|
||
|
|
Conflict : 8 (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 : 8 (Average: 2.75 Max: 11 Sum: 22)
|
||
|
|
Executed : 7 (Average: 2.62 Max: 11 Sum: 21 Ratio: 95.45%)
|
||
|
|
Bounded : 1 (Average: 1.00 Max: 1 Sum: 1 Ratio: 4.55%)
|
||
|
|
|
||
|
|
Rules : 55133 (Original: 53913)
|
||
|
|
Atoms : 43853
|
||
|
|
Bodies : 10280 (Original: 9059)
|
||
|
|
Count : 232 (Original: 476)
|
||
|
|
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 12735 (Eliminated: 1464 Frozen: 11271)
|
||
|
|
Constraints : 50631 (Binary: 90.2% Ternary: 5.9% Other: 3.9%)
|
||
|
|
|
||
|
|
Memory Peak : 222MB
|
||
|
|
Max. Length : 0 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 0.03s
|
||
|
|
Memory: 178MB (+0MB)
|
||
|
|
UNSAT
|
||
|
|
Iteration Time: 0.97s
|
||
|
|
|
||
|
|
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: 180.0MB
|
||
|
|
Grounding... [('step', [6]), ('step', [7]), ('step', [8]), ('step', [9]), ('step', [10]), ('check', [10])]
|
||
|
|
Grounding Time: 0.29s
|
||
|
|
Memory: 178MB (+0MB)
|
||
|
|
Unblocking actions...
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0
|
||
|
|
Calls : 4
|
||
|
|
Time : 2.238s (Solving: 0.46s 1st Model: 0.00s Unsat: 0.46s)
|
||
|
|
CPU Time : 2.144s
|
||
|
|
|
||
|
|
Choices : 16216 (Domain: 12582)
|
||
|
|
Conflicts : 1864 (Analyzed: 1862)
|
||
|
|
Restarts : 6 (Average: 310.33 Last: 87)
|
||
|
|
Model-Level : 147.0
|
||
|
|
Problems : 4 (Average Length: 7.00 Splits: 0)
|
||
|
|
Lemmas : 1862 (Deleted: 0)
|
||
|
|
Binary : 210 (Ratio: 11.28%)
|
||
|
|
Ternary : 280 (Ratio: 15.04%)
|
||
|
|
Conflict : 1862 (Average Length: 24.8 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 1862 (Average: 8.69 Max: 184 Sum: 16185)
|
||
|
|
Executed : 1840 (Average: 8.57 Max: 184 Sum: 15954 Ratio: 98.57%)
|
||
|
|
Bounded : 22 (Average: 10.50 Max: 12 Sum: 231 Ratio: 1.43%)
|
||
|
|
|
||
|
|
Rules : 55133 (Original: 53913)
|
||
|
|
Atoms : 43853
|
||
|
|
Bodies : 10280 (Original: 9059)
|
||
|
|
Count : 232 (Original: 476)
|
||
|
|
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 35311 (Eliminated: 1464 Frozen: 26317)
|
||
|
|
Constraints : 223676 (Binary: 91.3% Ternary: 6.4% Other: 2.3%)
|
||
|
|
|
||
|
|
Memory Peak : 222MB
|
||
|
|
Max. Length : 5 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 0.77s
|
||
|
|
Memory: 189MB (+11MB)
|
||
|
|
UNSAT
|
||
|
|
Iteration Time: 1.16s
|
||
|
|
|
||
|
|
Iteration 4
|
||
|
|
Queue: [(3,15,0,True), (4,20,0,True), (5,25,0,True), (6,30,0,True)]
|
||
|
|
Grounded Until: 10
|
||
|
|
Expected Memory: 200.0MB
|
||
|
|
Grounding... [('step', [11]), ('step', [12]), ('step', [13]), ('step', [14]), ('step', [15]), ('check', [15])]
|
||
|
|
Grounding Time: 0.33s
|
||
|
|
Memory: 195MB (+6MB)
|
||
|
|
Unblocking actions...
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0
|
||
|
|
Calls : 5
|
||
|
|
Time : 10.101s (Solving: 7.55s 1st Model: 0.00s Unsat: 7.55s)
|
||
|
|
CPU Time : 10.008s
|
||
|
|
|
||
|
|
Choices : 169527 (Domain: 131701)
|
||
|
|
Conflicts : 25187 (Analyzed: 25184)
|
||
|
|
Restarts : 64 (Average: 393.50 Last: 646)
|
||
|
|
Model-Level : 147.0
|
||
|
|
Problems : 5 (Average Length: 9.00 Splits: 0)
|
||
|
|
Lemmas : 25184 (Deleted: 13000)
|
||
|
|
Binary : 1242 (Ratio: 4.93%)
|
||
|
|
Ternary : 544 (Ratio: 2.16%)
|
||
|
|
Conflict : 25184 (Average Length: 261.4 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 25184 (Average: 6.56 Max: 810 Sum: 165120)
|
||
|
|
Executed : 25150 (Average: 6.54 Max: 810 Sum: 164701 Ratio: 99.75%)
|
||
|
|
Bounded : 34 (Average: 12.32 Max: 17 Sum: 419 Ratio: 0.25%)
|
||
|
|
|
||
|
|
Rules : 55133 (Original: 53913)
|
||
|
|
Atoms : 43853
|
||
|
|
Bodies : 10280 (Original: 9059)
|
||
|
|
Count : 232 (Original: 476)
|
||
|
|
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 57887 (Eliminated: 1464 Frozen: 48893)
|
||
|
|
Constraints : 380813 (Binary: 91.5% Ternary: 6.3% Other: 2.1%)
|
||
|
|
|
||
|
|
Memory Peak : 222MB
|
||
|
|
Max. Length : 10 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 7.42s
|
||
|
|
Memory: 209MB (+14MB)
|
||
|
|
UNSAT
|
||
|
|
Iteration Time: 7.87s
|
||
|
|
|
||
|
|
Iteration 5
|
||
|
|
Queue: [(4,20,0,True), (5,25,0,True), (6,30,0,True)]
|
||
|
|
Grounded Until: 15
|
||
|
|
Expected Memory: 229.0MB
|
||
|
|
Grounding... [('step', [16]), ('step', [17]), ('step', [18]), ('step', [19]), ('step', [20]), ('check', [20])]
|
||
|
|
Grounding Time: 0.30s
|
||
|
|
Memory: 212MB (+3MB)
|
||
|
|
Unblocking actions...
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 6
|
||
|
|
Time : 22.348s (Solving: 19.03s 1st Model: 0.00s Unsat: 7.55s)
|
||
|
|
CPU Time : 22.264s
|
||
|
|
|
||
|
|
Choices : 374743 (Domain: 319885)
|
||
|
|
Conflicts : 47955 (Analyzed: 47952)
|
||
|
|
Restarts : 164 (Average: 292.39 Last: 646)
|
||
|
|
Model-Level : 147.0
|
||
|
|
Problems : 6 (Average Length: 11.17 Splits: 0)
|
||
|
|
Lemmas : 47952 (Deleted: 32192)
|
||
|
|
Binary : 2387 (Ratio: 4.98%)
|
||
|
|
Ternary : 898 (Ratio: 1.87%)
|
||
|
|
Conflict : 47952 (Average Length: 334.7 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 47952 (Average: 7.49 Max: 810 Sum: 359221)
|
||
|
|
Executed : 47918 (Average: 7.48 Max: 810 Sum: 358802 Ratio: 99.88%)
|
||
|
|
Bounded : 34 (Average: 12.32 Max: 17 Sum: 419 Ratio: 0.12%)
|
||
|
|
|
||
|
|
Rules : 55133 (Original: 53913)
|
||
|
|
Atoms : 43853
|
||
|
|
Bodies : 10280 (Original: 9059)
|
||
|
|
Count : 232 (Original: 476)
|
||
|
|
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 80463 (Eliminated: 1464 Frozen: 71469)
|
||
|
|
Constraints : 538208 (Binary: 91.6% Ternary: 6.3% Other: 2.0%)
|
||
|
|
|
||
|
|
Memory Peak : 227MB
|
||
|
|
Max. Length : 15 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 11.82s
|
||
|
|
Memory: 227MB (+15MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 12.26s
|
||
|
|
|
||
|
|
Iteration 6
|
||
|
|
Queue: [(5,25,0,True), (6,30,0,True)]
|
||
|
|
Grounded Until: 20
|
||
|
|
Expected Memory: 247.0MB
|
||
|
|
Grounding... [('step', [21]), ('step', [22]), ('step', [23]), ('step', [24]), ('step', [25]), ('check', [25])]
|
||
|
|
Grounding Time: 0.31s
|
||
|
|
Memory: 230MB (+3MB)
|
||
|
|
Unblocking actions...
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 7
|
||
|
|
Time : 80.558s (Solving: 76.46s 1st Model: 0.00s Unsat: 7.55s)
|
||
|
|
CPU Time : 80.500s
|
||
|
|
|
||
|
|
Choices : 815840 (Domain: 723921)
|
||
|
|
Conflicts : 125928 (Analyzed: 125925)
|
||
|
|
Restarts : 264 (Average: 476.99 Last: 715)
|
||
|
|
Model-Level : 147.0
|
||
|
|
Problems : 7 (Average Length: 13.43 Splits: 0)
|
||
|
|
Lemmas : 125925 (Deleted: 94595)
|
||
|
|
Binary : 4155 (Ratio: 3.30%)
|
||
|
|
Ternary : 1257 (Ratio: 1.00%)
|
||
|
|
Conflict : 125925 (Average Length: 861.5 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 125925 (Average: 6.23 Max: 810 Sum: 784831)
|
||
|
|
Executed : 125890 (Average: 6.23 Max: 810 Sum: 784385 Ratio: 99.94%)
|
||
|
|
Bounded : 35 (Average: 12.74 Max: 27 Sum: 446 Ratio: 0.06%)
|
||
|
|
|
||
|
|
Rules : 55133 (Original: 53913)
|
||
|
|
Atoms : 43853
|
||
|
|
Bodies : 10280 (Original: 9059)
|
||
|
|
Count : 232 (Original: 476)
|
||
|
|
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 103039 (Eliminated: 1464 Frozen: 94045)
|
||
|
|
Constraints : 711253 (Binary: 91.6% Ternary: 6.4% Other: 2.0%)
|
||
|
|
|
||
|
|
Memory Peak : 434MB
|
||
|
|
Max. Length : 20 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 57.78s
|
||
|
|
Memory: 370MB (+140MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 58.24s
|
||
|
|
|
||
|
|
Iteration 7
|
||
|
|
Queue: [(6,30,0,True)]
|
||
|
|
Grounded Until: 25
|
||
|
|
Expected Memory: 513.0MB
|
||
|
|
Grounding... [('step', [26]), ('step', [27]), ('step', [28]), ('step', [29]), ('step', [30]), ('check', [30])]
|
||
|
|
Grounding Time: 0.33s
|
||
|
|
Memory: 372MB (+2MB)
|
||
|
|
Unblocking actions...
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 8
|
||
|
|
Time : 105.603s (Solving: 100.63s 1st Model: 0.00s Unsat: 7.55s)
|
||
|
|
CPU Time : 105.556s
|
||
|
|
|
||
|
|
Choices : 1076248 (Domain: 975350)
|
||
|
|
Conflicts : 158464 (Analyzed: 158461)
|
||
|
|
Restarts : 364 (Average: 435.33 Last: 715)
|
||
|
|
Model-Level : 147.0
|
||
|
|
Problems : 8 (Average Length: 15.75 Splits: 0)
|
||
|
|
Lemmas : 158461 (Deleted: 124965)
|
||
|
|
Binary : 5202 (Ratio: 3.28%)
|
||
|
|
Ternary : 1554 (Ratio: 0.98%)
|
||
|
|
Conflict : 158461 (Average Length: 893.0 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 158461 (Average: 6.48 Max: 810 Sum: 1026131)
|
||
|
|
Executed : 158426 (Average: 6.47 Max: 810 Sum: 1025685 Ratio: 99.96%)
|
||
|
|
Bounded : 35 (Average: 12.74 Max: 27 Sum: 446 Ratio: 0.04%)
|
||
|
|
|
||
|
|
Rules : 55133 (Original: 53913)
|
||
|
|
Atoms : 43853
|
||
|
|
Bodies : 10280 (Original: 9059)
|
||
|
|
Count : 232 (Original: 476)
|
||
|
|
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 125615 (Eliminated: 1464 Frozen: 116621)
|
||
|
|
Constraints : 884284 (Binary: 91.6% Ternary: 6.4% Other: 2.0%)
|
||
|
|
|
||
|
|
Memory Peak : 434MB
|
||
|
|
Max. Length : 25 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 24.53s
|
||
|
|
Memory: 390MB (+18MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 25.06s
|
||
|
|
|
||
|
|
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 : 117.385s (Solving: 112.37s 1st Model: 0.00s Unsat: 19.29s)
|
||
|
|
CPU Time : 117.344s
|
||
|
|
|
||
|
|
Choices : 1183703 (Domain: 1082805)
|
||
|
|
Conflicts : 181734 (Analyzed: 181730)
|
||
|
|
Restarts : 453 (Average: 401.17 Last: 2225)
|
||
|
|
Model-Level : 147.0
|
||
|
|
Problems : 9 (Average Length: 17.56 Splits: 0)
|
||
|
|
Lemmas : 181730 (Deleted: 156271)
|
||
|
|
Binary : 5462 (Ratio: 3.01%)
|
||
|
|
Ternary : 1596 (Ratio: 0.88%)
|
||
|
|
Conflict : 181730 (Average Length: 832.0 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 181730 (Average: 6.20 Max: 810 Sum: 1126824)
|
||
|
|
Executed : 181693 (Average: 6.20 Max: 810 Sum: 1126345 Ratio: 99.96%)
|
||
|
|
Bounded : 37 (Average: 12.95 Max: 32 Sum: 479 Ratio: 0.04%)
|
||
|
|
|
||
|
|
Rules : 55133 (Original: 53913)
|
||
|
|
Atoms : 43853
|
||
|
|
Bodies : 10280 (Original: 9059)
|
||
|
|
Count : 232 (Original: 476)
|
||
|
|
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 125615 (Eliminated: 1464 Frozen: 124151)
|
||
|
|
Constraints : 884284 (Binary: 91.6% Ternary: 6.4% Other: 2.0%)
|
||
|
|
|
||
|
|
Memory Peak : 434MB
|
||
|
|
Max. Length : 30 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 11.76s
|
||
|
|
Memory: 390MB (+0MB)
|
||
|
|
UNSAT
|
||
|
|
Iteration Time: 11.79s
|
||
|
|
|
||
|
|
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 : 215.633s (Solving: 210.58s 1st Model: 0.00s Unsat: 19.29s)
|
||
|
|
CPU Time : 215.632s
|
||
|
|
|
||
|
|
Choices : 1445562 (Domain: 1343837)
|
||
|
|
Conflicts : 271751 (Analyzed: 271747)
|
||
|
|
Restarts : 553 (Average: 491.41 Last: 2225)
|
||
|
|
Model-Level : 147.0
|
||
|
|
Problems : 10 (Average Length: 19.00 Splits: 0)
|
||
|
|
Lemmas : 271747 (Deleted: 225148)
|
||
|
|
Binary : 5774 (Ratio: 2.12%)
|
||
|
|
Ternary : 1677 (Ratio: 0.62%)
|
||
|
|
Conflict : 271747 (Average Length: 1005.5 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 271747 (Average: 5.06 Max: 810 Sum: 1375959)
|
||
|
|
Executed : 271710 (Average: 5.06 Max: 810 Sum: 1375480 Ratio: 99.97%)
|
||
|
|
Bounded : 37 (Average: 12.95 Max: 32 Sum: 479 Ratio: 0.03%)
|
||
|
|
|
||
|
|
Rules : 55133 (Original: 53913)
|
||
|
|
Atoms : 43853
|
||
|
|
Bodies : 10280 (Original: 9059)
|
||
|
|
Count : 232 (Original: 476)
|
||
|
|
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 125615 (Eliminated: 1464 Frozen: 124151)
|
||
|
|
Constraints : 884270 (Binary: 91.6% Ternary: 6.4% Other: 2.0%)
|
||
|
|
|
||
|
|
Memory Peak : 434MB
|
||
|
|
Max. Length : 30 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 98.28s
|
||
|
|
Memory: 390MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 98.29s
|
||
|
|
|
||
|
|
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 : 246.089s (Solving: 240.98s 1st Model: 0.00s Unsat: 19.29s)
|
||
|
|
CPU Time : 246.100s
|
||
|
|
|
||
|
|
Choices : 1735384 (Domain: 1628814)
|
||
|
|
Conflicts : 312268 (Analyzed: 312264)
|
||
|
|
Restarts : 653 (Average: 478.20 Last: 2225)
|
||
|
|
Model-Level : 147.0
|
||
|
|
Problems : 11 (Average Length: 20.18 Splits: 0)
|
||
|
|
Lemmas : 312264 (Deleted: 280698)
|
||
|
|
Binary : 6447 (Ratio: 2.06%)
|
||
|
|
Ternary : 1812 (Ratio: 0.58%)
|
||
|
|
Conflict : 312264 (Average Length: 1009.1 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 312264 (Average: 5.27 Max: 810 Sum: 1646666)
|
||
|
|
Executed : 312227 (Average: 5.27 Max: 810 Sum: 1646187 Ratio: 99.97%)
|
||
|
|
Bounded : 37 (Average: 12.95 Max: 32 Sum: 479 Ratio: 0.03%)
|
||
|
|
|
||
|
|
Rules : 55133 (Original: 53913)
|
||
|
|
Atoms : 43853
|
||
|
|
Bodies : 10280 (Original: 9059)
|
||
|
|
Count : 232 (Original: 476)
|
||
|
|
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 125615 (Eliminated: 1464 Frozen: 124151)
|
||
|
|
Constraints : 884270 (Binary: 91.6% Ternary: 6.4% Other: 2.0%)
|
||
|
|
|
||
|
|
Memory Peak : 454MB
|
||
|
|
Max. Length : 30 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 30.43s
|
||
|
|
Memory: 454MB (+64MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 30.47s
|
||
|
|
|
||
|
|
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: 597.0MB
|
||
|
|
Grounding... [('step', [31]), ('step', [32]), ('step', [33]), ('step', [34]), ('step', [35]), ('check', [35])]
|
||
|
|
Grounding Time: 0.38s
|
||
|
|
Memory: 455MB (+1MB)
|
||
|
|
Unblocking actions...
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 12
|
||
|
|
Time : 285.188s (Solving: 279.16s 1st Model: 0.00s Unsat: 19.29s)
|
||
|
|
CPU Time : 285.216s
|
||
|
|
|
||
|
|
Choices : 2020824 (Domain: 1901625)
|
||
|
|
Conflicts : 365309 (Analyzed: 365305)
|
||
|
|
Restarts : 753 (Average: 485.13 Last: 2225)
|
||
|
|
Model-Level : 147.0
|
||
|
|
Problems : 12 (Average Length: 21.58 Splits: 0)
|
||
|
|
Lemmas : 365305 (Deleted: 336429)
|
||
|
|
Binary : 7448 (Ratio: 2.04%)
|
||
|
|
Ternary : 1978 (Ratio: 0.54%)
|
||
|
|
Conflict : 365305 (Average Length: 1025.4 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 365305 (Average: 5.24 Max: 810 Sum: 1912959)
|
||
|
|
Executed : 365268 (Average: 5.24 Max: 810 Sum: 1912480 Ratio: 99.97%)
|
||
|
|
Bounded : 37 (Average: 12.95 Max: 32 Sum: 479 Ratio: 0.03%)
|
||
|
|
|
||
|
|
Rules : 55133 (Original: 53913)
|
||
|
|
Atoms : 43853
|
||
|
|
Bodies : 10280 (Original: 9059)
|
||
|
|
Count : 232 (Original: 476)
|
||
|
|
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 148191 (Eliminated: 1464 Frozen: 139197)
|
||
|
|
Constraints : 1057315 (Binary: 91.6% Ternary: 6.4% Other: 2.0%)
|
||
|
|
|
||
|
|
Memory Peak : 476MB
|
||
|
|
Max. Length : 30 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 38.55s
|
||
|
|
Memory: 469MB (+14MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 39.12s
|
||
|
|
|
||
|
|
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: 612.0MB
|
||
|
|
Grounding... [('step', [36]), ('step', [37]), ('step', [38]), ('step', [39]), ('step', [40]), ('check', [40])]
|
||
|
|
Grounding Time: 0.40s
|
||
|
|
Memory: 476MB (+7MB)
|
||
|
|
Unblocking actions...
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 13
|
||
|
|
Time : 312.484s (Solving: 305.51s 1st Model: 0.00s Unsat: 19.29s)
|
||
|
|
CPU Time : 312.524s
|
||
|
|
|
||
|
|
Choices : 2324390 (Domain: 2192754)
|
||
|
|
Conflicts : 406897 (Analyzed: 406893)
|
||
|
|
Restarts : 853 (Average: 477.01 Last: 2225)
|
||
|
|
Model-Level : 147.0
|
||
|
|
Problems : 13 (Average Length: 23.15 Splits: 0)
|
||
|
|
Lemmas : 406893 (Deleted: 373689)
|
||
|
|
Binary : 8553 (Ratio: 2.10%)
|
||
|
|
Ternary : 2158 (Ratio: 0.53%)
|
||
|
|
Conflict : 406893 (Average Length: 1003.8 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 406893 (Average: 5.39 Max: 810 Sum: 2194438)
|
||
|
|
Executed : 406856 (Average: 5.39 Max: 810 Sum: 2193959 Ratio: 99.98%)
|
||
|
|
Bounded : 37 (Average: 12.95 Max: 32 Sum: 479 Ratio: 0.02%)
|
||
|
|
|
||
|
|
Rules : 55133 (Original: 53913)
|
||
|
|
Atoms : 43853
|
||
|
|
Bodies : 10280 (Original: 9059)
|
||
|
|
Count : 232 (Original: 476)
|
||
|
|
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 170767 (Eliminated: 1464 Frozen: 161773)
|
||
|
|
Constraints : 1230360 (Binary: 91.6% Ternary: 6.4% Other: 2.0%)
|
||
|
|
|
||
|
|
Memory Peak : 502MB
|
||
|
|
Max. Length : 35 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 26.73s
|
||
|
|
Memory: 490MB (+14MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 27.32s
|
||
|
|
|
||
|
|
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: 633.0MB
|
||
|
|
Grounding... [('step', [41]), ('step', [42]), ('step', [43]), ('step', [44]), ('step', [45]), ('check', [45])]
|
||
|
|
Grounding Time: 0.34s
|
||
|
|
Memory: 493MB (+3MB)
|
||
|
|
Unblocking actions...
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 14
|
||
|
|
Time : 370.087s (Solving: 362.23s 1st Model: 0.00s Unsat: 19.29s)
|
||
|
|
CPU Time : 370.152s
|
||
|
|
|
||
|
|
Choices : 3040085 (Domain: 2888738)
|
||
|
|
Conflicts : 497748 (Analyzed: 497744)
|
||
|
|
Restarts : 953 (Average: 522.29 Last: 2225)
|
||
|
|
Model-Level : 147.0
|
||
|
|
Problems : 14 (Average Length: 24.86 Splits: 0)
|
||
|
|
Lemmas : 497744 (Deleted: 460723)
|
||
|
|
Binary : 11080 (Ratio: 2.23%)
|
||
|
|
Ternary : 2479 (Ratio: 0.50%)
|
||
|
|
Conflict : 497744 (Average Length: 973.4 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 497744 (Average: 5.80 Max: 810 Sum: 2884928)
|
||
|
|
Executed : 497707 (Average: 5.80 Max: 810 Sum: 2884449 Ratio: 99.98%)
|
||
|
|
Bounded : 37 (Average: 12.95 Max: 32 Sum: 479 Ratio: 0.02%)
|
||
|
|
|
||
|
|
Rules : 55133 (Original: 53913)
|
||
|
|
Atoms : 43853
|
||
|
|
Bodies : 10280 (Original: 9059)
|
||
|
|
Count : 232 (Original: 476)
|
||
|
|
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 193343 (Eliminated: 1464 Frozen: 184349)
|
||
|
|
Constraints : 1403405 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
|
||
|
|
|
||
|
|
Memory Peak : 519MB
|
||
|
|
Max. Length : 40 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 57.09s
|
||
|
|
Memory: 516MB (+23MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 57.64s
|
||
|
|
|
||
|
|
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: 659.0MB
|
||
|
|
Grounding... [('step', [46]), ('step', [47]), ('step', [48]), ('step', [49]), ('step', [50]), ('check', [50])]
|
||
|
|
Grounding Time: 0.33s
|
||
|
|
Memory: 516MB (+0MB)
|
||
|
|
Unblocking actions...
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 15
|
||
|
|
Time : 409.616s (Solving: 400.86s 1st Model: 0.00s Unsat: 19.29s)
|
||
|
|
CPU Time : 409.696s
|
||
|
|
|
||
|
|
Choices : 3521524 (Domain: 3359301)
|
||
|
|
Conflicts : 565727 (Analyzed: 565723)
|
||
|
|
Restarts : 1053 (Average: 537.25 Last: 2225)
|
||
|
|
Model-Level : 147.0
|
||
|
|
Problems : 15 (Average Length: 26.67 Splits: 0)
|
||
|
|
Lemmas : 565723 (Deleted: 514457)
|
||
|
|
Binary : 12917 (Ratio: 2.28%)
|
||
|
|
Ternary : 2714 (Ratio: 0.48%)
|
||
|
|
Conflict : 565723 (Average Length: 951.3 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 565723 (Average: 5.90 Max: 810 Sum: 3339149)
|
||
|
|
Executed : 565686 (Average: 5.90 Max: 810 Sum: 3338670 Ratio: 99.99%)
|
||
|
|
Bounded : 37 (Average: 12.95 Max: 32 Sum: 479 Ratio: 0.01%)
|
||
|
|
|
||
|
|
Rules : 55133 (Original: 53913)
|
||
|
|
Atoms : 43853
|
||
|
|
Bodies : 10280 (Original: 9059)
|
||
|
|
Count : 232 (Original: 476)
|
||
|
|
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 215919 (Eliminated: 1464 Frozen: 206925)
|
||
|
|
Constraints : 1576450 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
|
||
|
|
|
||
|
|
Memory Peak : 545MB
|
||
|
|
Max. Length : 45 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 39.02s
|
||
|
|
Memory: 529MB (+13MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 39.55s
|
||
|
|
|
||
|
|
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: 672.0MB
|
||
|
|
Grounding... [('step', [51]), ('step', [52]), ('step', [53]), ('step', [54]), ('step', [55]), ('check', [55])]
|
||
|
|
Grounding Time: 0.31s
|
||
|
|
Memory: 529MB (+0MB)
|
||
|
|
Unblocking actions...
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 16
|
||
|
|
Time : 442.973s (Solving: 433.32s 1st Model: 0.00s Unsat: 19.29s)
|
||
|
|
CPU Time : 443.068s
|
||
|
|
|
||
|
|
Choices : 3985594 (Domain: 3807049)
|
||
|
|
Conflicts : 620781 (Analyzed: 620777)
|
||
|
|
Restarts : 1153 (Average: 538.40 Last: 2225)
|
||
|
|
Model-Level : 147.0
|
||
|
|
Problems : 16 (Average Length: 28.56 Splits: 0)
|
||
|
|
Lemmas : 620777 (Deleted: 578386)
|
||
|
|
Binary : 14427 (Ratio: 2.32%)
|
||
|
|
Ternary : 2968 (Ratio: 0.48%)
|
||
|
|
Conflict : 620777 (Average Length: 930.6 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 620777 (Average: 6.08 Max: 810 Sum: 3775604)
|
||
|
|
Executed : 620740 (Average: 6.08 Max: 810 Sum: 3775125 Ratio: 99.99%)
|
||
|
|
Bounded : 37 (Average: 12.95 Max: 32 Sum: 479 Ratio: 0.01%)
|
||
|
|
|
||
|
|
Rules : 55133 (Original: 53913)
|
||
|
|
Atoms : 43853
|
||
|
|
Bodies : 10280 (Original: 9059)
|
||
|
|
Count : 232 (Original: 476)
|
||
|
|
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 238495 (Eliminated: 1464 Frozen: 229501)
|
||
|
|
Constraints : 1749495 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
|
||
|
|
|
||
|
|
Memory Peak : 563MB
|
||
|
|
Max. Length : 50 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 32.84s
|
||
|
|
Memory: 544MB (+15MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 33.38s
|
||
|
|
|
||
|
|
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: 687.0MB
|
||
|
|
Grounding... [('step', [56]), ('step', [57]), ('step', [58]), ('step', [59]), ('step', [60]), ('check', [60])]
|
||
|
|
Grounding Time: 0.32s
|
||
|
|
Memory: 544MB (+0MB)
|
||
|
|
Unblocking actions...
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 17
|
||
|
|
Time : 492.674s (Solving: 482.12s 1st Model: 0.00s Unsat: 19.29s)
|
||
|
|
CPU Time : 492.792s
|
||
|
|
|
||
|
|
Choices : 4646244 (Domain: 4460949)
|
||
|
|
Conflicts : 705016 (Analyzed: 705012)
|
||
|
|
Restarts : 1253 (Average: 562.66 Last: 2225)
|
||
|
|
Model-Level : 147.0
|
||
|
|
Problems : 17 (Average Length: 30.53 Splits: 0)
|
||
|
|
Lemmas : 705012 (Deleted: 647271)
|
||
|
|
Binary : 16178 (Ratio: 2.29%)
|
||
|
|
Ternary : 3175 (Ratio: 0.45%)
|
||
|
|
Conflict : 705012 (Average Length: 911.2 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 705012 (Average: 6.25 Max: 810 Sum: 4407725)
|
||
|
|
Executed : 704974 (Average: 6.25 Max: 810 Sum: 4407184 Ratio: 99.99%)
|
||
|
|
Bounded : 38 (Average: 14.24 Max: 62 Sum: 541 Ratio: 0.01%)
|
||
|
|
|
||
|
|
Rules : 55133 (Original: 53913)
|
||
|
|
Atoms : 43853
|
||
|
|
Bodies : 10280 (Original: 9059)
|
||
|
|
Count : 232 (Original: 476)
|
||
|
|
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 261071 (Eliminated: 1464 Frozen: 252077)
|
||
|
|
Constraints : 1922540 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
|
||
|
|
|
||
|
|
Memory Peak : 580MB
|
||
|
|
Max. Length : 55 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 49.19s
|
||
|
|
Memory: 559MB (+15MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 49.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: 702.0MB
|
||
|
|
Grounding... [('step', [61]), ('step', [62]), ('step', [63]), ('step', [64]), ('step', [65]), ('check', [65])]
|
||
|
|
Grounding Time: 0.32s
|
||
|
|
Memory: 559MB (+0MB)
|
||
|
|
Unblocking actions...
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 18
|
||
|
|
Time : 532.870s (Solving: 521.39s 1st Model: 0.00s Unsat: 19.29s)
|
||
|
|
CPU Time : 533.008s
|
||
|
|
|
||
|
|
Choices : 5219606 (Domain: 5022359)
|
||
|
|
Conflicts : 779482 (Analyzed: 779478)
|
||
|
|
Restarts : 1353 (Average: 576.11 Last: 2225)
|
||
|
|
Model-Level : 147.0
|
||
|
|
Problems : 18 (Average Length: 32.56 Splits: 0)
|
||
|
|
Lemmas : 779478 (Deleted: 726205)
|
||
|
|
Binary : 17910 (Ratio: 2.30%)
|
||
|
|
Ternary : 3441 (Ratio: 0.44%)
|
||
|
|
Conflict : 779478 (Average Length: 893.8 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 779478 (Average: 6.35 Max: 810 Sum: 4951879)
|
||
|
|
Executed : 779440 (Average: 6.35 Max: 810 Sum: 4951338 Ratio: 99.99%)
|
||
|
|
Bounded : 38 (Average: 14.24 Max: 62 Sum: 541 Ratio: 0.01%)
|
||
|
|
|
||
|
|
Rules : 55133 (Original: 53913)
|
||
|
|
Atoms : 43853
|
||
|
|
Bodies : 10280 (Original: 9059)
|
||
|
|
Count : 232 (Original: 476)
|
||
|
|
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 283647 (Eliminated: 1464 Frozen: 274653)
|
||
|
|
Constraints : 2095571 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
|
||
|
|
|
||
|
|
Memory Peak : 597MB
|
||
|
|
Max. Length : 60 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 39.66s
|
||
|
|
Memory: 591MB (+32MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 40.22s
|
||
|
|
|
||
|
|
Iteration 18
|
||
|
|
Queue: [(14,70,0,True), (15,75,0,True), (16,80,0,True), (17,85,0,True)]
|
||
|
|
Grounded Until: 65
|
||
|
|
Expected Memory: 734.0MB
|
||
|
|
Grounding... [('step', [66]), ('step', [67]), ('step', [68]), ('step', [69]), ('step', [70]), ('check', [70])]
|
||
|
|
Grounding Time: 0.34s
|
||
|
|
Memory: 591MB (+0MB)
|
||
|
|
Unblocking actions...
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 19
|
||
|
|
Time : 564.796s (Solving: 552.36s 1st Model: 0.00s Unsat: 19.29s)
|
||
|
|
CPU Time : 564.948s
|
||
|
|
|
||
|
|
Choices : 5653911 (Domain: 5454075)
|
||
|
|
Conflicts : 831295 (Analyzed: 831291)
|
||
|
|
Restarts : 1453 (Average: 572.12 Last: 2225)
|
||
|
|
Model-Level : 147.0
|
||
|
|
Problems : 19 (Average Length: 34.63 Splits: 0)
|
||
|
|
Lemmas : 831291 (Deleted: 764176)
|
||
|
|
Binary : 18968 (Ratio: 2.28%)
|
||
|
|
Ternary : 3613 (Ratio: 0.43%)
|
||
|
|
Conflict : 831291 (Average Length: 886.1 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 831291 (Average: 6.45 Max: 810 Sum: 5357766)
|
||
|
|
Executed : 831253 (Average: 6.44 Max: 810 Sum: 5357225 Ratio: 99.99%)
|
||
|
|
Bounded : 38 (Average: 14.24 Max: 62 Sum: 541 Ratio: 0.01%)
|
||
|
|
|
||
|
|
Rules : 55133 (Original: 53913)
|
||
|
|
Atoms : 43853
|
||
|
|
Bodies : 10280 (Original: 9059)
|
||
|
|
Count : 232 (Original: 476)
|
||
|
|
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 306223 (Eliminated: 1464 Frozen: 297229)
|
||
|
|
Constraints : 2268616 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
|
||
|
|
|
||
|
|
Memory Peak : 629MB
|
||
|
|
Max. Length : 65 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 31.36s
|
||
|
|
Memory: 603MB (+12MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 31.95s
|
||
|
|
|
||
|
|
Iteration 19
|
||
|
|
Queue: [(15,75,0,True), (16,80,0,True), (17,85,0,True)]
|
||
|
|
Grounded Until: 70
|
||
|
|
Expected Memory: 746.0MB
|
||
|
|
Grounding... [('step', [71]), ('step', [72]), ('step', [73]), ('step', [74]), ('step', [75]), ('check', [75])]
|
||
|
|
Grounding Time: 0.34s
|
||
|
|
Memory: 603MB (+0MB)
|
||
|
|
Unblocking actions...
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 20
|
||
|
|
Time : 617.165s (Solving: 603.75s 1st Model: 0.00s Unsat: 19.29s)
|
||
|
|
CPU Time : 617.340s
|
||
|
|
|
||
|
|
Choices : 6324741 (Domain: 6124740)
|
||
|
|
Conflicts : 910938 (Analyzed: 910934)
|
||
|
|
Restarts : 1553 (Average: 586.56 Last: 2225)
|
||
|
|
Model-Level : 147.0
|
||
|
|
Problems : 20 (Average Length: 36.75 Splits: 0)
|
||
|
|
Lemmas : 910934 (Deleted: 845824)
|
||
|
|
Binary : 20287 (Ratio: 2.23%)
|
||
|
|
Ternary : 3786 (Ratio: 0.42%)
|
||
|
|
Conflict : 910934 (Average Length: 878.7 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 910934 (Average: 6.58 Max: 810 Sum: 5995248)
|
||
|
|
Executed : 910896 (Average: 6.58 Max: 810 Sum: 5994707 Ratio: 99.99%)
|
||
|
|
Bounded : 38 (Average: 14.24 Max: 62 Sum: 541 Ratio: 0.01%)
|
||
|
|
|
||
|
|
Rules : 55133 (Original: 53913)
|
||
|
|
Atoms : 43853
|
||
|
|
Bodies : 10280 (Original: 9059)
|
||
|
|
Count : 232 (Original: 476)
|
||
|
|
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 328799 (Eliminated: 1464 Frozen: 319805)
|
||
|
|
Constraints : 2441661 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
|
||
|
|
|
||
|
|
Memory Peak : 643MB
|
||
|
|
Max. Length : 70 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 51.79s
|
||
|
|
Memory: 617MB (+14MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 52.40s
|
||
|
|
|
||
|
|
Iteration 20
|
||
|
|
Queue: [(16,80,0,True), (17,85,0,True)]
|
||
|
|
Grounded Until: 75
|
||
|
|
Expected Memory: 760.0MB
|
||
|
|
Grounding... [('step', [76]), ('step', [77]), ('step', [78]), ('step', [79]), ('step', [80]), ('check', [80])]
|
||
|
|
Grounding Time: 0.48s
|
||
|
|
Memory: 633MB (+16MB)
|
||
|
|
Unblocking actions...
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 21
|
||
|
|
Time : 656.065s (Solving: 641.53s 1st Model: 0.00s Unsat: 19.29s)
|
||
|
|
CPU Time : 656.260s
|
||
|
|
|
||
|
|
Choices : 6830979 (Domain: 6625457)
|
||
|
|
Conflicts : 971635 (Analyzed: 971631)
|
||
|
|
Restarts : 1653 (Average: 587.80 Last: 2225)
|
||
|
|
Model-Level : 147.0
|
||
|
|
Problems : 21 (Average Length: 38.90 Splits: 0)
|
||
|
|
Lemmas : 971631 (Deleted: 904777)
|
||
|
|
Binary : 21300 (Ratio: 2.19%)
|
||
|
|
Ternary : 3935 (Ratio: 0.40%)
|
||
|
|
Conflict : 971631 (Average Length: 876.7 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 971631 (Average: 6.66 Max: 810 Sum: 6468366)
|
||
|
|
Executed : 971593 (Average: 6.66 Max: 810 Sum: 6467825 Ratio: 99.99%)
|
||
|
|
Bounded : 38 (Average: 14.24 Max: 62 Sum: 541 Ratio: 0.01%)
|
||
|
|
|
||
|
|
Rules : 55133 (Original: 53913)
|
||
|
|
Atoms : 43853
|
||
|
|
Bodies : 10280 (Original: 9059)
|
||
|
|
Count : 232 (Original: 476)
|
||
|
|
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 351375 (Eliminated: 1464 Frozen: 342381)
|
||
|
|
Constraints : 2614706 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
|
||
|
|
|
||
|
|
Memory Peak : 679MB
|
||
|
|
Max. Length : 75 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 38.18s
|
||
|
|
Memory: 646MB (+13MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 38.92s
|
||
|
|
|
||
|
|
Iteration 21
|
||
|
|
Queue: [(17,85,0,True)]
|
||
|
|
Grounded Until: 80
|
||
|
|
Expected Memory: 789.0MB
|
||
|
|
Grounding... [('step', [81]), ('step', [82]), ('step', [83]), ('step', [84]), ('step', [85]), ('check', [85])]
|
||
|
|
Grounding Time: 0.32s
|
||
|
|
Memory: 646MB (+0MB)
|
||
|
|
Unblocking actions...
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 22
|
||
|
|
Time : 695.874s (Solving: 680.36s 1st Model: 0.00s Unsat: 19.29s)
|
||
|
|
CPU Time : 696.088s
|
||
|
|
|
||
|
|
Choices : 7358251 (Domain: 7150785)
|
||
|
|
Conflicts : 1030352 (Analyzed: 1030348)
|
||
|
|
Restarts : 1753 (Average: 587.76 Last: 2225)
|
||
|
|
Model-Level : 147.0
|
||
|
|
Problems : 22 (Average Length: 41.09 Splits: 0)
|
||
|
|
Lemmas : 1030348 (Deleted: 961806)
|
||
|
|
Binary : 22392 (Ratio: 2.17%)
|
||
|
|
Ternary : 4092 (Ratio: 0.40%)
|
||
|
|
Conflict : 1030348 (Average Length: 874.4 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 1030348 (Average: 6.75 Max: 810 Sum: 6956440)
|
||
|
|
Executed : 1030310 (Average: 6.75 Max: 810 Sum: 6955899 Ratio: 99.99%)
|
||
|
|
Bounded : 38 (Average: 14.24 Max: 62 Sum: 541 Ratio: 0.01%)
|
||
|
|
|
||
|
|
Rules : 55133 (Original: 53913)
|
||
|
|
Atoms : 43853
|
||
|
|
Bodies : 10280 (Original: 9059)
|
||
|
|
Count : 232 (Original: 476)
|
||
|
|
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 373951 (Eliminated: 1464 Frozen: 364957)
|
||
|
|
Constraints : 2787751 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
|
||
|
|
|
||
|
|
Memory Peak : 695MB
|
||
|
|
Max. Length : 80 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 39.24s
|
||
|
|
Memory: 660MB (+14MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 39.84s
|
||
|
|
|
||
|
|
Iteration 22
|
||
|
|
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), (22,110,0,True)]
|
||
|
|
Grounded Until: 85
|
||
|
|
Blocking actions...
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 23
|
||
|
|
Time : 784.181s (Solving: 768.56s 1st Model: 0.00s Unsat: 19.29s)
|
||
|
|
CPU Time : 784.432s
|
||
|
|
|
||
|
|
Choices : 7583190 (Domain: 7375724)
|
||
|
|
Conflicts : 1111482 (Analyzed: 1111478)
|
||
|
|
Restarts : 1853 (Average: 599.83 Last: 2225)
|
||
|
|
Model-Level : 147.0
|
||
|
|
Problems : 23 (Average Length: 43.09 Splits: 0)
|
||
|
|
Lemmas : 1111478 (Deleted: 1037390)
|
||
|
|
Binary : 22557 (Ratio: 2.03%)
|
||
|
|
Ternary : 4130 (Ratio: 0.37%)
|
||
|
|
Conflict : 1111478 (Average Length: 913.5 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 1111478 (Average: 6.45 Max: 810 Sum: 7170472)
|
||
|
|
Executed : 1111440 (Average: 6.45 Max: 810 Sum: 7169931 Ratio: 99.99%)
|
||
|
|
Bounded : 38 (Average: 14.24 Max: 62 Sum: 541 Ratio: 0.01%)
|
||
|
|
|
||
|
|
Rules : 55133 (Original: 53913)
|
||
|
|
Atoms : 43853
|
||
|
|
Bodies : 10280 (Original: 9059)
|
||
|
|
Count : 232 (Original: 476)
|
||
|
|
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 373951 (Eliminated: 1464 Frozen: 372487)
|
||
|
|
Constraints : 2787751 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
|
||
|
|
|
||
|
|
Memory Peak : 695MB
|
||
|
|
Max. Length : 85 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 88.30s
|
||
|
|
Memory: 662MB (+2MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 88.35s
|
||
|
|
|
||
|
|
Iteration 23
|
||
|
|
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), (22,110,0,True)]
|
||
|
|
Grounded Until: 85
|
||
|
|
Unblocking actions...
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 24
|
||
|
|
Time : 827.747s (Solving: 812.03s 1st Model: 0.00s Unsat: 19.29s)
|
||
|
|
CPU Time : 828.016s
|
||
|
|
|
||
|
|
Choices : 7863730 (Domain: 7656264)
|
||
|
|
Conflicts : 1160129 (Analyzed: 1160125)
|
||
|
|
Restarts : 1953 (Average: 594.02 Last: 2225)
|
||
|
|
Model-Level : 147.0
|
||
|
|
Problems : 24 (Average Length: 44.92 Splits: 0)
|
||
|
|
Lemmas : 1160125 (Deleted: 1083829)
|
||
|
|
Binary : 22746 (Ratio: 1.96%)
|
||
|
|
Ternary : 4163 (Ratio: 0.36%)
|
||
|
|
Conflict : 1160125 (Average Length: 930.7 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 1160125 (Average: 6.41 Max: 810 Sum: 7432623)
|
||
|
|
Executed : 1160087 (Average: 6.41 Max: 810 Sum: 7432082 Ratio: 99.99%)
|
||
|
|
Bounded : 38 (Average: 14.24 Max: 62 Sum: 541 Ratio: 0.01%)
|
||
|
|
|
||
|
|
Rules : 55133 (Original: 53913)
|
||
|
|
Atoms : 43853
|
||
|
|
Bodies : 10280 (Original: 9059)
|
||
|
|
Count : 232 (Original: 476)
|
||
|
|
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 373951 (Eliminated: 1464 Frozen: 372487)
|
||
|
|
Constraints : 2787751 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
|
||
|
|
|
||
|
|
Memory Peak : 695MB
|
||
|
|
Max. Length : 85 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 43.55s
|
||
|
|
Memory: 662MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 43.59s
|
||
|
|
|
||
|
|
Iteration 24
|
||
|
|
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), (22,110,0,True)]
|
||
|
|
Grounded Until: 85
|
||
|
|
Unblocking actions...
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 25
|
||
|
|
Time : 879.751s (Solving: 863.89s 1st Model: 0.00s Unsat: 19.29s)
|
||
|
|
CPU Time : 880.044s
|
||
|
|
|
||
|
|
Choices : 8128841 (Domain: 7921375)
|
||
|
|
Conflicts : 1220760 (Analyzed: 1220756)
|
||
|
|
Restarts : 2053 (Average: 594.62 Last: 2225)
|
||
|
|
Model-Level : 147.0
|
||
|
|
Problems : 25 (Average Length: 46.60 Splits: 0)
|
||
|
|
Lemmas : 1220756 (Deleted: 1147275)
|
||
|
|
Binary : 22983 (Ratio: 1.88%)
|
||
|
|
Ternary : 4224 (Ratio: 0.35%)
|
||
|
|
Conflict : 1220756 (Average Length: 941.9 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 1220756 (Average: 6.29 Max: 810 Sum: 7678134)
|
||
|
|
Executed : 1220718 (Average: 6.29 Max: 810 Sum: 7677593 Ratio: 99.99%)
|
||
|
|
Bounded : 38 (Average: 14.24 Max: 62 Sum: 541 Ratio: 0.01%)
|
||
|
|
|
||
|
|
Rules : 55133 (Original: 53913)
|
||
|
|
Atoms : 43853
|
||
|
|
Bodies : 10280 (Original: 9059)
|
||
|
|
Count : 232 (Original: 476)
|
||
|
|
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 373951 (Eliminated: 1464 Frozen: 372487)
|
||
|
|
Constraints : 2787751 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
|
||
|
|
|
||
|
|
Memory Peak : 695MB
|
||
|
|
Max. Length : 85 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 51.96s
|
||
|
|
Memory: 662MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 52.03s
|
||
|
|
|
||
|
|
Iteration 25
|
||
|
|
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), (22,110,0,True)]
|
||
|
|
Grounded Until: 85
|
||
|
|
Unblocking actions...
|
||
|
|
Solving...
|
||
|
|
*** Info : (planner): INTERRUPTED by signal!
|
||
|
|
UNKNOWN
|
||
|
|
|
||
|
|
INTERRUPTED : 1
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 26
|
||
|
|
Time : 895.001s (Solving: 879.05s 1st Model: 0.00s Unsat: 19.29s)
|
||
|
|
CPU Time : 895.284s
|
||
|
|
|
||
|
|
Choices : 8289380 (Domain: 8081914)
|
||
|
|
Conflicts : 1245722 (Analyzed: 1245718)
|
||
|
|
Restarts : 2111 (Average: 590.11 Last: 2225)
|
||
|
|
Model-Level : 147.0
|
||
|
|
Problems : 26 (Average Length: 48.15 Splits: 0)
|
||
|
|
Lemmas : 1245718 (Deleted: 1177076)
|
||
|
|
Binary : 23249 (Ratio: 1.87%)
|
||
|
|
Ternary : 4273 (Ratio: 0.34%)
|
||
|
|
Conflict : 1245718 (Average Length: 936.6 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 1245718 (Average: 6.28 Max: 810 Sum: 7825992)
|
||
|
|
Executed : 1245680 (Average: 6.28 Max: 810 Sum: 7825451 Ratio: 99.99%)
|
||
|
|
Bounded : 38 (Average: 14.24 Max: 62 Sum: 541 Ratio: 0.01%)
|
||
|
|
|
||
|
|
Rules : 55133 (Original: 53913)
|
||
|
|
Atoms : 43853
|
||
|
|
Bodies : 10280 (Original: 9059)
|
||
|
|
Count : 232 (Original: 476)
|
||
|
|
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 373951 (Eliminated: 1464 Frozen: 372487)
|
||
|
|
Constraints : 2787751 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
|
||
|
|
|
||
|
|
Memory Peak : 695MB
|
||
|
|
Max. Length : 85 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
|