1194 lines
42 KiB
Plaintext
1194 lines
42 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-10.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-10.pddl
|
|
Parsing...
|
|
Parsing: [0.040s CPU, 0.046s wall-clock]
|
|
Normalizing task... [0.010s CPU, 0.004s wall-clock]
|
|
Instantiating...
|
|
Generating Datalog program... [0.010s CPU, 0.012s wall-clock]
|
|
Normalizing Datalog program...
|
|
Normalizing Datalog program: [0.050s CPU, 0.054s wall-clock]
|
|
Preparing model... [0.030s CPU, 0.029s wall-clock]
|
|
Generated 115 rules.
|
|
Computing model... [0.460s CPU, 0.454s wall-clock]
|
|
2784 relevant atoms
|
|
2893 auxiliary atoms
|
|
5677 final queue length
|
|
9793 total queue pushes
|
|
Completing instantiation... [0.860s CPU, 0.861s wall-clock]
|
|
Instantiating: [1.420s CPU, 1.417s wall-clock]
|
|
Computing fact groups...
|
|
Finding invariants...
|
|
24 initial candidates
|
|
Finding invariants: [0.120s CPU, 0.122s wall-clock]
|
|
Checking invariant weight... [0.000s CPU, 0.001s wall-clock]
|
|
Instantiating groups... [0.000s CPU, 0.008s wall-clock]
|
|
Collecting mutex groups... [0.000s CPU, 0.001s wall-clock]
|
|
Choosing groups...
|
|
292 uncovered facts
|
|
Choosing groups: [0.000s CPU, 0.002s wall-clock]
|
|
Building translation key... [0.010s CPU, 0.011s wall-clock]
|
|
Computing fact groups: [0.160s CPU, 0.168s wall-clock]
|
|
Building STRIPS to SAS dictionary... [0.000s CPU, 0.002s wall-clock]
|
|
Building dictionary for full mutex groups... [0.010s CPU, 0.005s wall-clock]
|
|
Building mutex information...
|
|
Building mutex information: [0.000s CPU, 0.003s wall-clock]
|
|
Translating task...
|
|
Processing axioms...
|
|
Simplifying axioms... [0.000s CPU, 0.000s wall-clock]
|
|
Processing axioms: [0.050s CPU, 0.046s wall-clock]
|
|
Translating task: [0.890s CPU, 0.885s wall-clock]
|
|
3276 effect conditions simplified
|
|
0 implied preconditions added
|
|
Detecting unreachable propositions...
|
|
0 operators removed
|
|
0 axioms removed
|
|
3 propositions removed
|
|
Detecting unreachable propositions: [0.430s CPU, 0.433s wall-clock]
|
|
Reordering and filtering variables...
|
|
295 of 295 variables necessary.
|
|
14 of 17 mutex groups necessary.
|
|
1958 of 1958 operators necessary.
|
|
0 of 0 axiom rules necessary.
|
|
Reordering and filtering variables: [0.310s CPU, 0.302s wall-clock]
|
|
Translator variables: 295
|
|
Translator derived variables: 0
|
|
Translator facts: 617
|
|
Translator goal facts: 12
|
|
Translator mutex groups: 14
|
|
Translator total mutex groups size: 42
|
|
Translator operators: 1958
|
|
Translator axioms: 0
|
|
Translator task size: 18764
|
|
Translator peak memory: 47308 KB
|
|
Writing output... [0.360s CPU, 0.390s wall-clock]
|
|
Done! [3.660s CPU, 3.692s wall-clock]
|
|
planner.py version 0.0.1
|
|
|
|
Time: 0.75s
|
|
Memory: 101MB
|
|
|
|
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.884s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
|
|
CPU Time : 0.756s
|
|
|
|
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 : 54149
|
|
Atoms : 54149
|
|
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 : 237MB
|
|
Max. Length : 0 steps
|
|
Models : 0
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 0.01s
|
|
Memory: 173MB (+72MB)
|
|
UNSAT
|
|
Iteration Time: 0.01s
|
|
|
|
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: 173MB
|
|
Grounding... [('step', [1]), ('step', [2]), ('step', [3]), ('step', [4]), ('step', [5]), ('check', [5])]
|
|
Grounding Time: 0.23s
|
|
Memory: 173MB (+0MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 1+
|
|
Calls : 2
|
|
Time : 1.399s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
|
|
CPU Time : 1.272s
|
|
|
|
Choices : 220 (Domain: 94)
|
|
Conflicts : 2 (Analyzed: 2)
|
|
Restarts : 0
|
|
Model-Level : 212.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: 28.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: 7.50 Max: 14 Sum: 15)
|
|
Executed : 2 (Average: 7.50 Max: 14 Sum: 15 Ratio: 100.00%)
|
|
Bounded : 0 (Average: 0.00 Max: 0 Sum: 0 Ratio: 0.00%)
|
|
|
|
Rules : 54149
|
|
Atoms : 54149
|
|
Bodies : 1 (Original: 0)
|
|
Tight : Yes
|
|
Variables : 14506 (Eliminated: 0 Frozen: 14506)
|
|
Constraints : 48947 (Binary: 95.2% Ternary: 3.3% Other: 1.4%)
|
|
|
|
Memory Peak : 237MB
|
|
Max. Length : 0 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 0.18s
|
|
Memory: 176MB (+3MB)
|
|
SAT
|
|
Testing...
|
|
NOT SERIALIZABLE
|
|
Testing Time: 0.76s
|
|
Memory: 202MB (+26MB)
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0
|
|
Calls : 3
|
|
Time : 1.539s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
|
|
CPU Time : 1.416s
|
|
|
|
Choices : 233 (Domain: 99)
|
|
Conflicts : 8 (Analyzed: 7)
|
|
Restarts : 0
|
|
Model-Level : 212.0
|
|
Problems : 3 (Average Length: 5.33 Splits: 0)
|
|
Lemmas : 7 (Deleted: 0)
|
|
Binary : 3 (Ratio: 42.86%)
|
|
Ternary : 2 (Ratio: 28.57%)
|
|
Conflict : 7 (Average Length: 9.7 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 7 (Average: 4.43 Max: 14 Sum: 31)
|
|
Executed : 4 (Average: 4.00 Max: 14 Sum: 28 Ratio: 90.32%)
|
|
Bounded : 3 (Average: 1.00 Max: 1 Sum: 3 Ratio: 9.68%)
|
|
|
|
Rules : 76935 (Original: 75225)
|
|
Atoms : 61653
|
|
Bodies : 14003 (Original: 12292)
|
|
Count : 291 (Original: 633)
|
|
Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813)
|
|
Tight : Yes
|
|
Variables : 17794 (Eliminated: 2052 Frozen: 15742)
|
|
Constraints : 68211 (Binary: 90.3% Ternary: 5.8% Other: 3.9%)
|
|
|
|
Memory Peak : 237MB
|
|
Max. Length : 0 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 0.04s
|
|
Memory: 202MB (+0MB)
|
|
UNSAT
|
|
Iteration Time: 1.32s
|
|
|
|
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: 205.0MB
|
|
Grounding... [('step', [6]), ('step', [7]), ('step', [8]), ('step', [9]), ('step', [10]), ('check', [10])]
|
|
Grounding Time: 0.46s
|
|
Memory: 202MB (+0MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0
|
|
Calls : 4
|
|
Time : 3.192s (Solving: 0.48s 1st Model: 0.00s Unsat: 0.48s)
|
|
CPU Time : 3.072s
|
|
|
|
Choices : 22339 (Domain: 15348)
|
|
Conflicts : 1931 (Analyzed: 1929)
|
|
Restarts : 6 (Average: 321.50 Last: 609)
|
|
Model-Level : 212.0
|
|
Problems : 4 (Average Length: 7.00 Splits: 0)
|
|
Lemmas : 1929 (Deleted: 0)
|
|
Binary : 256 (Ratio: 13.27%)
|
|
Ternary : 256 (Ratio: 13.27%)
|
|
Conflict : 1929 (Average Length: 47.0 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 1929 (Average: 11.51 Max: 138 Sum: 22198)
|
|
Executed : 1903 (Average: 11.37 Max: 138 Sum: 21930 Ratio: 98.79%)
|
|
Bounded : 26 (Average: 10.31 Max: 12 Sum: 268 Ratio: 1.21%)
|
|
|
|
Rules : 76935 (Original: 75225)
|
|
Atoms : 61653
|
|
Bodies : 14003 (Original: 12292)
|
|
Count : 291 (Original: 633)
|
|
Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813)
|
|
Tight : Yes
|
|
Variables : 50740 (Eliminated: 2052 Frozen: 36958)
|
|
Constraints : 317796 (Binary: 91.1% Ternary: 6.7% Other: 2.3%)
|
|
|
|
Memory Peak : 237MB
|
|
Max. Length : 5 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 1.03s
|
|
Memory: 216MB (+14MB)
|
|
UNSAT
|
|
Iteration Time: 1.66s
|
|
|
|
Iteration 4
|
|
Queue: [(3,15,0,True), (4,20,0,True), (5,25,0,True), (6,30,0,True)]
|
|
Grounded Until: 10
|
|
Expected Memory: 230.0MB
|
|
Grounding... [('step', [11]), ('step', [12]), ('step', [13]), ('step', [14]), ('step', [15]), ('check', [15])]
|
|
Grounding Time: 0.43s
|
|
Memory: 223MB (+7MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0
|
|
Calls : 5
|
|
Time : 10.060s (Solving: 6.19s 1st Model: 0.00s Unsat: 6.19s)
|
|
CPU Time : 9.944s
|
|
|
|
Choices : 166935 (Domain: 119013)
|
|
Conflicts : 18691 (Analyzed: 18688)
|
|
Restarts : 48 (Average: 389.33 Last: 2758)
|
|
Model-Level : 212.0
|
|
Problems : 5 (Average Length: 9.00 Splits: 0)
|
|
Lemmas : 18688 (Deleted: 5004)
|
|
Binary : 1076 (Ratio: 5.76%)
|
|
Ternary : 535 (Ratio: 2.86%)
|
|
Conflict : 18688 (Average Length: 179.1 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 18688 (Average: 8.77 Max: 539 Sum: 163918)
|
|
Executed : 18631 (Average: 8.73 Max: 539 Sum: 163197 Ratio: 99.56%)
|
|
Bounded : 57 (Average: 12.65 Max: 17 Sum: 721 Ratio: 0.44%)
|
|
|
|
Rules : 76935 (Original: 75225)
|
|
Atoms : 61653
|
|
Bodies : 14003 (Original: 12292)
|
|
Count : 291 (Original: 633)
|
|
Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813)
|
|
Tight : Yes
|
|
Variables : 83686 (Eliminated: 2052 Frozen: 69904)
|
|
Constraints : 535212 (Binary: 91.4% Ternary: 6.6% Other: 2.0%)
|
|
|
|
Memory Peak : 243MB
|
|
Max. Length : 10 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 6.26s
|
|
Memory: 243MB (+20MB)
|
|
UNSAT
|
|
Iteration Time: 6.88s
|
|
|
|
Iteration 5
|
|
Queue: [(4,20,0,True), (5,25,0,True), (6,30,0,True)]
|
|
Grounded Until: 15
|
|
Expected Memory: 270.0MB
|
|
Grounding... [('step', [16]), ('step', [17]), ('step', [18]), ('step', [19]), ('step', [20]), ('check', [20])]
|
|
Grounding Time: 0.44s
|
|
Memory: 247MB (+4MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0
|
|
Calls : 6
|
|
Time : 53.521s (Solving: 48.43s 1st Model: 0.00s Unsat: 48.43s)
|
|
CPU Time : 53.424s
|
|
|
|
Choices : 480680 (Domain: 402891)
|
|
Conflicts : 67011 (Analyzed: 67007)
|
|
Restarts : 93 (Average: 720.51 Last: 6556)
|
|
Model-Level : 212.0
|
|
Problems : 6 (Average Length: 11.17 Splits: 0)
|
|
Lemmas : 67007 (Deleted: 37889)
|
|
Binary : 2345 (Ratio: 3.50%)
|
|
Ternary : 1077 (Ratio: 1.61%)
|
|
Conflict : 67007 (Average Length: 511.1 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 67007 (Average: 7.03 Max: 539 Sum: 471307)
|
|
Executed : 66933 (Average: 7.02 Max: 539 Sum: 470323 Ratio: 99.79%)
|
|
Bounded : 74 (Average: 13.30 Max: 22 Sum: 984 Ratio: 0.21%)
|
|
|
|
Rules : 76935 (Original: 75225)
|
|
Atoms : 61653
|
|
Bodies : 14003 (Original: 12292)
|
|
Count : 291 (Original: 633)
|
|
Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813)
|
|
Tight : Yes
|
|
Variables : 116632 (Eliminated: 2052 Frozen: 102850)
|
|
Constraints : 757133 (Binary: 91.3% Ternary: 6.7% Other: 2.0%)
|
|
|
|
Memory Peak : 398MB
|
|
Max. Length : 15 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 42.84s
|
|
Memory: 334MB (+87MB)
|
|
UNSAT
|
|
Iteration Time: 43.49s
|
|
|
|
Iteration 6
|
|
Queue: [(5,25,0,True), (6,30,0,True)]
|
|
Grounded Until: 20
|
|
Expected Memory: 425.0MB
|
|
Grounding... [('step', [21]), ('step', [22]), ('step', [23]), ('step', [24]), ('step', [25]), ('check', [25])]
|
|
Grounding Time: 0.68s
|
|
Memory: 347MB (+13MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 7
|
|
Time : 95.929s (Solving: 89.08s 1st Model: 0.00s Unsat: 48.43s)
|
|
CPU Time : 95.852s
|
|
|
|
Choices : 881977 (Domain: 751212)
|
|
Conflicts : 114209 (Analyzed: 114205)
|
|
Restarts : 193 (Average: 591.74 Last: 6556)
|
|
Model-Level : 212.0
|
|
Problems : 7 (Average Length: 13.43 Splits: 0)
|
|
Lemmas : 114205 (Deleted: 82191)
|
|
Binary : 3844 (Ratio: 3.37%)
|
|
Ternary : 1478 (Ratio: 1.29%)
|
|
Conflict : 114205 (Average Length: 797.5 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 114205 (Average: 7.47 Max: 561 Sum: 853548)
|
|
Executed : 114119 (Average: 7.46 Max: 561 Sum: 852260 Ratio: 99.85%)
|
|
Bounded : 86 (Average: 14.98 Max: 27 Sum: 1288 Ratio: 0.15%)
|
|
|
|
Rules : 76935 (Original: 75225)
|
|
Atoms : 61653
|
|
Bodies : 14003 (Original: 12292)
|
|
Count : 291 (Original: 633)
|
|
Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813)
|
|
Tight : Yes
|
|
Variables : 149578 (Eliminated: 2052 Frozen: 135796)
|
|
Constraints : 1006620 (Binary: 91.3% Ternary: 6.7% Other: 2.0%)
|
|
|
|
Memory Peak : 424MB
|
|
Max. Length : 20 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 41.45s
|
|
Memory: 424MB (+77MB)
|
|
UNKNOWN
|
|
Iteration Time: 42.44s
|
|
|
|
Iteration 7
|
|
Queue: [(6,30,0,True)]
|
|
Grounded Until: 25
|
|
Expected Memory: 515.0MB
|
|
Grounding... [('step', [26]), ('step', [27]), ('step', [28]), ('step', [29]), ('step', [30]), ('check', [30])]
|
|
Grounding Time: 0.46s
|
|
Memory: 428MB (+4MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 8
|
|
Time : 131.961s (Solving: 123.77s 1st Model: 0.00s Unsat: 48.43s)
|
|
CPU Time : 131.900s
|
|
|
|
Choices : 1276998 (Domain: 1120172)
|
|
Conflicts : 152105 (Analyzed: 152101)
|
|
Restarts : 293 (Average: 519.12 Last: 6556)
|
|
Model-Level : 212.0
|
|
Problems : 8 (Average Length: 15.75 Splits: 0)
|
|
Lemmas : 152101 (Deleted: 126483)
|
|
Binary : 5375 (Ratio: 3.53%)
|
|
Ternary : 1850 (Ratio: 1.22%)
|
|
Conflict : 152101 (Average Length: 897.4 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 152101 (Average: 8.08 Max: 584 Sum: 1228309)
|
|
Executed : 152008 (Average: 8.07 Max: 584 Sum: 1226822 Ratio: 99.88%)
|
|
Bounded : 93 (Average: 15.99 Max: 32 Sum: 1487 Ratio: 0.12%)
|
|
|
|
Rules : 76935 (Original: 75225)
|
|
Atoms : 61653
|
|
Bodies : 14003 (Original: 12292)
|
|
Count : 291 (Original: 633)
|
|
Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813)
|
|
Tight : Yes
|
|
Variables : 182524 (Eliminated: 2052 Frozen: 168742)
|
|
Constraints : 1256093 (Binary: 91.3% Ternary: 6.8% Other: 1.9%)
|
|
|
|
Memory Peak : 455MB
|
|
Max. Length : 25 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 35.32s
|
|
Memory: 455MB (+27MB)
|
|
UNKNOWN
|
|
Iteration Time: 36.06s
|
|
|
|
Iteration 8
|
|
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), (18,90,0,True)]
|
|
Grounded Until: 30
|
|
Blocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 9
|
|
Time : 236.512s (Solving: 228.26s 1st Model: 0.00s Unsat: 48.43s)
|
|
CPU Time : 236.496s
|
|
|
|
Choices : 1574118 (Domain: 1414916)
|
|
Conflicts : 223083 (Analyzed: 223079)
|
|
Restarts : 393 (Average: 567.63 Last: 6556)
|
|
Model-Level : 212.0
|
|
Problems : 9 (Average Length: 17.56 Splits: 0)
|
|
Lemmas : 223079 (Deleted: 194712)
|
|
Binary : 5749 (Ratio: 2.58%)
|
|
Ternary : 1935 (Ratio: 0.87%)
|
|
Conflict : 223079 (Average Length: 1249.8 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 223079 (Average: 6.78 Max: 584 Sum: 1512566)
|
|
Executed : 222983 (Average: 6.77 Max: 584 Sum: 1510988 Ratio: 99.90%)
|
|
Bounded : 96 (Average: 16.44 Max: 32 Sum: 1578 Ratio: 0.10%)
|
|
|
|
Rules : 76935 (Original: 75225)
|
|
Atoms : 61653
|
|
Bodies : 14003 (Original: 12292)
|
|
Count : 291 (Original: 633)
|
|
Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813)
|
|
Tight : Yes
|
|
Variables : 182524 (Eliminated: 2052 Frozen: 180472)
|
|
Constraints : 1256065 (Binary: 91.3% Ternary: 6.8% Other: 1.9%)
|
|
|
|
Memory Peak : 583MB
|
|
Max. Length : 30 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 104.57s
|
|
Memory: 583MB (+128MB)
|
|
UNKNOWN
|
|
Iteration Time: 104.60s
|
|
|
|
Iteration 9
|
|
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), (18,90,0,True)]
|
|
Grounded Until: 30
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 10
|
|
Time : 279.217s (Solving: 270.88s 1st Model: 0.00s Unsat: 48.43s)
|
|
CPU Time : 279.220s
|
|
|
|
Choices : 2016831 (Domain: 1837992)
|
|
Conflicts : 270169 (Analyzed: 270165)
|
|
Restarts : 493 (Average: 548.00 Last: 6556)
|
|
Model-Level : 212.0
|
|
Problems : 10 (Average Length: 19.00 Splits: 0)
|
|
Lemmas : 270165 (Deleted: 241176)
|
|
Binary : 6838 (Ratio: 2.53%)
|
|
Ternary : 2089 (Ratio: 0.77%)
|
|
Conflict : 270165 (Average Length: 1275.6 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 270165 (Average: 7.15 Max: 584 Sum: 1931861)
|
|
Executed : 270064 (Average: 7.14 Max: 584 Sum: 1930134 Ratio: 99.91%)
|
|
Bounded : 101 (Average: 17.10 Max: 32 Sum: 1727 Ratio: 0.09%)
|
|
|
|
Rules : 76935 (Original: 75225)
|
|
Atoms : 61653
|
|
Bodies : 14003 (Original: 12292)
|
|
Count : 291 (Original: 633)
|
|
Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813)
|
|
Tight : Yes
|
|
Variables : 182524 (Eliminated: 2052 Frozen: 180472)
|
|
Constraints : 1256034 (Binary: 91.3% Ternary: 6.8% Other: 1.9%)
|
|
|
|
Memory Peak : 583MB
|
|
Max. Length : 30 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 42.67s
|
|
Memory: 583MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 42.73s
|
|
|
|
Iteration 10
|
|
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), (18,90,0,True)]
|
|
Grounded Until: 30
|
|
Expected Memory: 674.0MB
|
|
Grounding... [('step', [31]), ('step', [32]), ('step', [33]), ('step', [34]), ('step', [35]), ('check', [35])]
|
|
Grounding Time: 0.45s
|
|
Memory: 584MB (+1MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 11
|
|
Time : 322.243s (Solving: 312.60s 1st Model: 0.00s Unsat: 48.43s)
|
|
CPU Time : 322.264s
|
|
|
|
Choices : 2450156 (Domain: 2254044)
|
|
Conflicts : 316597 (Analyzed: 316593)
|
|
Restarts : 593 (Average: 533.88 Last: 6556)
|
|
Model-Level : 212.0
|
|
Problems : 11 (Average Length: 20.64 Splits: 0)
|
|
Lemmas : 316593 (Deleted: 278646)
|
|
Binary : 8059 (Ratio: 2.55%)
|
|
Ternary : 2395 (Ratio: 0.76%)
|
|
Conflict : 316593 (Average Length: 1281.8 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 316593 (Average: 7.39 Max: 584 Sum: 2340269)
|
|
Executed : 316490 (Average: 7.39 Max: 584 Sum: 2338468 Ratio: 99.92%)
|
|
Bounded : 103 (Average: 17.49 Max: 37 Sum: 1801 Ratio: 0.08%)
|
|
|
|
Rules : 76935 (Original: 75225)
|
|
Atoms : 61653
|
|
Bodies : 14003 (Original: 12292)
|
|
Count : 291 (Original: 633)
|
|
Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813)
|
|
Tight : Yes
|
|
Variables : 215470 (Eliminated: 2052 Frozen: 201688)
|
|
Constraints : 1505591 (Binary: 91.3% Ternary: 6.8% Other: 1.9%)
|
|
|
|
Memory Peak : 616MB
|
|
Max. Length : 30 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 42.34s
|
|
Memory: 604MB (+20MB)
|
|
UNKNOWN
|
|
Iteration Time: 43.05s
|
|
|
|
Iteration 11
|
|
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), (18,90,0,True)]
|
|
Grounded Until: 35
|
|
Expected Memory: 695.0MB
|
|
Grounding... [('step', [36]), ('step', [37]), ('step', [38]), ('step', [39]), ('step', [40]), ('check', [40])]
|
|
Grounding Time: 0.46s
|
|
Memory: 604MB (+0MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 12
|
|
Time : 368.547s (Solving: 357.56s 1st Model: 0.00s Unsat: 48.43s)
|
|
CPU Time : 368.584s
|
|
|
|
Choices : 2872143 (Domain: 2662461)
|
|
Conflicts : 364596 (Analyzed: 364592)
|
|
Restarts : 693 (Average: 526.11 Last: 6556)
|
|
Model-Level : 212.0
|
|
Problems : 12 (Average Length: 22.42 Splits: 0)
|
|
Lemmas : 364592 (Deleted: 321756)
|
|
Binary : 9720 (Ratio: 2.67%)
|
|
Ternary : 2819 (Ratio: 0.77%)
|
|
Conflict : 364592 (Average Length: 1313.3 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 364592 (Average: 7.50 Max: 584 Sum: 2735201)
|
|
Executed : 364489 (Average: 7.50 Max: 584 Sum: 2733400 Ratio: 99.93%)
|
|
Bounded : 103 (Average: 17.49 Max: 37 Sum: 1801 Ratio: 0.07%)
|
|
|
|
Rules : 76935 (Original: 75225)
|
|
Atoms : 61653
|
|
Bodies : 14003 (Original: 12292)
|
|
Count : 291 (Original: 633)
|
|
Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813)
|
|
Tight : Yes
|
|
Variables : 248416 (Eliminated: 2052 Frozen: 234634)
|
|
Constraints : 1755148 (Binary: 91.3% Ternary: 6.8% Other: 1.9%)
|
|
|
|
Memory Peak : 639MB
|
|
Max. Length : 35 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 45.58s
|
|
Memory: 625MB (+21MB)
|
|
UNKNOWN
|
|
Iteration Time: 46.34s
|
|
|
|
Iteration 12
|
|
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), (18,90,0,True)]
|
|
Grounded Until: 40
|
|
Expected Memory: 716.0MB
|
|
Grounding... [('step', [41]), ('step', [42]), ('step', [43]), ('step', [44]), ('step', [45]), ('check', [45])]
|
|
Grounding Time: 0.47s
|
|
Memory: 625MB (+0MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 13
|
|
Time : 426.226s (Solving: 413.84s 1st Model: 0.00s Unsat: 48.43s)
|
|
CPU Time : 426.284s
|
|
|
|
Choices : 3449985 (Domain: 3223950)
|
|
Conflicts : 422956 (Analyzed: 422952)
|
|
Restarts : 793 (Average: 533.36 Last: 6556)
|
|
Model-Level : 212.0
|
|
Problems : 13 (Average Length: 24.31 Splits: 0)
|
|
Lemmas : 422952 (Deleted: 381589)
|
|
Binary : 11338 (Ratio: 2.68%)
|
|
Ternary : 3087 (Ratio: 0.73%)
|
|
Conflict : 422952 (Average Length: 1331.3 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 422952 (Average: 7.76 Max: 584 Sum: 3281145)
|
|
Executed : 422849 (Average: 7.75 Max: 584 Sum: 3279344 Ratio: 99.95%)
|
|
Bounded : 103 (Average: 17.49 Max: 37 Sum: 1801 Ratio: 0.05%)
|
|
|
|
Rules : 76935 (Original: 75225)
|
|
Atoms : 61653
|
|
Bodies : 14003 (Original: 12292)
|
|
Count : 291 (Original: 633)
|
|
Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813)
|
|
Tight : Yes
|
|
Variables : 281362 (Eliminated: 2052 Frozen: 267580)
|
|
Constraints : 2004733 (Binary: 91.3% Ternary: 6.8% Other: 1.9%)
|
|
|
|
Memory Peak : 665MB
|
|
Max. Length : 40 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 56.93s
|
|
Memory: 659MB (+34MB)
|
|
UNKNOWN
|
|
Iteration Time: 57.72s
|
|
|
|
Iteration 13
|
|
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), (18,90,0,True)]
|
|
Grounded Until: 45
|
|
Expected Memory: 750.0MB
|
|
Grounding... [('step', [46]), ('step', [47]), ('step', [48]), ('step', [49]), ('step', [50]), ('check', [50])]
|
|
Grounding Time: 0.50s
|
|
Memory: 659MB (+0MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 14
|
|
Time : 470.863s (Solving: 457.05s 1st Model: 0.00s Unsat: 48.43s)
|
|
CPU Time : 470.936s
|
|
|
|
Choices : 3973235 (Domain: 3732797)
|
|
Conflicts : 468077 (Analyzed: 468073)
|
|
Restarts : 893 (Average: 524.16 Last: 6556)
|
|
Model-Level : 212.0
|
|
Problems : 14 (Average Length: 26.29 Splits: 0)
|
|
Lemmas : 468073 (Deleted: 423318)
|
|
Binary : 12562 (Ratio: 2.68%)
|
|
Ternary : 3303 (Ratio: 0.71%)
|
|
Conflict : 468073 (Average Length: 1344.0 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 468073 (Average: 8.06 Max: 584 Sum: 3773761)
|
|
Executed : 467969 (Average: 8.06 Max: 584 Sum: 3771908 Ratio: 99.95%)
|
|
Bounded : 104 (Average: 17.82 Max: 52 Sum: 1853 Ratio: 0.05%)
|
|
|
|
Rules : 76935 (Original: 75225)
|
|
Atoms : 61653
|
|
Bodies : 14003 (Original: 12292)
|
|
Count : 291 (Original: 633)
|
|
Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813)
|
|
Tight : Yes
|
|
Variables : 314308 (Eliminated: 2052 Frozen: 300526)
|
|
Constraints : 2254318 (Binary: 91.3% Ternary: 6.8% Other: 1.9%)
|
|
|
|
Memory Peak : 704MB
|
|
Max. Length : 45 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 43.84s
|
|
Memory: 680MB (+21MB)
|
|
UNKNOWN
|
|
Iteration Time: 44.66s
|
|
|
|
Iteration 14
|
|
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), (18,90,0,True)]
|
|
Grounded Until: 50
|
|
Expected Memory: 771.0MB
|
|
Grounding... [('step', [51]), ('step', [52]), ('step', [53]), ('step', [54]), ('step', [55]), ('check', [55])]
|
|
Grounding Time: 0.62s
|
|
Memory: 692MB (+12MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 15
|
|
Time : 522.558s (Solving: 507.20s 1st Model: 0.00s Unsat: 48.43s)
|
|
CPU Time : 522.652s
|
|
|
|
Choices : 4533941 (Domain: 4290629)
|
|
Conflicts : 519435 (Analyzed: 519431)
|
|
Restarts : 993 (Average: 523.09 Last: 6556)
|
|
Model-Level : 212.0
|
|
Problems : 15 (Average Length: 28.33 Splits: 0)
|
|
Lemmas : 519431 (Deleted: 466616)
|
|
Binary : 13618 (Ratio: 2.62%)
|
|
Ternary : 3425 (Ratio: 0.66%)
|
|
Conflict : 519431 (Average Length: 1355.9 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 519431 (Average: 8.29 Max: 584 Sum: 4307333)
|
|
Executed : 519327 (Average: 8.29 Max: 584 Sum: 4305480 Ratio: 99.96%)
|
|
Bounded : 104 (Average: 17.82 Max: 52 Sum: 1853 Ratio: 0.04%)
|
|
|
|
Rules : 76935 (Original: 75225)
|
|
Atoms : 61653
|
|
Bodies : 14003 (Original: 12292)
|
|
Count : 291 (Original: 633)
|
|
Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813)
|
|
Tight : Yes
|
|
Variables : 347254 (Eliminated: 2052 Frozen: 333472)
|
|
Constraints : 2503889 (Binary: 91.3% Ternary: 6.8% Other: 1.9%)
|
|
|
|
Memory Peak : 741MB
|
|
Max. Length : 50 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 50.80s
|
|
Memory: 714MB (+22MB)
|
|
UNKNOWN
|
|
Iteration Time: 51.73s
|
|
|
|
Iteration 15
|
|
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), (18,90,0,True)]
|
|
Grounded Until: 55
|
|
Expected Memory: 805.0MB
|
|
Grounding... [('step', [56]), ('step', [57]), ('step', [58]), ('step', [59]), ('step', [60]), ('check', [60])]
|
|
Grounding Time: 0.47s
|
|
Memory: 714MB (+0MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 16
|
|
Time : 568.648s (Solving: 551.85s 1st Model: 0.00s Unsat: 48.43s)
|
|
CPU Time : 568.760s
|
|
|
|
Choices : 5111517 (Domain: 4860847)
|
|
Conflicts : 564810 (Analyzed: 564806)
|
|
Restarts : 1093 (Average: 516.75 Last: 6556)
|
|
Model-Level : 212.0
|
|
Problems : 16 (Average Length: 30.44 Splits: 0)
|
|
Lemmas : 564806 (Deleted: 515272)
|
|
Binary : 14861 (Ratio: 2.63%)
|
|
Ternary : 3632 (Ratio: 0.64%)
|
|
Conflict : 564806 (Average Length: 1356.6 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 564806 (Average: 8.59 Max: 584 Sum: 4854015)
|
|
Executed : 564702 (Average: 8.59 Max: 584 Sum: 4852162 Ratio: 99.96%)
|
|
Bounded : 104 (Average: 17.82 Max: 52 Sum: 1853 Ratio: 0.04%)
|
|
|
|
Rules : 76935 (Original: 75225)
|
|
Atoms : 61653
|
|
Bodies : 14003 (Original: 12292)
|
|
Count : 291 (Original: 633)
|
|
Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813)
|
|
Tight : Yes
|
|
Variables : 380200 (Eliminated: 2052 Frozen: 366418)
|
|
Constraints : 2753474 (Binary: 91.3% Ternary: 6.8% Other: 1.9%)
|
|
|
|
Memory Peak : 766MB
|
|
Max. Length : 55 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 45.30s
|
|
Memory: 736MB (+22MB)
|
|
UNKNOWN
|
|
Iteration Time: 46.12s
|
|
|
|
Iteration 16
|
|
Queue: [(13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True), (17,85,0,True), (18,90,0,True)]
|
|
Grounded Until: 60
|
|
Expected Memory: 827.0MB
|
|
Grounding... [('step', [61]), ('step', [62]), ('step', [63]), ('step', [64]), ('step', [65]), ('check', [65])]
|
|
Grounding Time: 0.47s
|
|
Memory: 736MB (+0MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 17
|
|
Time : 626.166s (Solving: 607.92s 1st Model: 0.00s Unsat: 48.43s)
|
|
CPU Time : 626.304s
|
|
|
|
Choices : 5976521 (Domain: 5716549)
|
|
Conflicts : 625442 (Analyzed: 625438)
|
|
Restarts : 1193 (Average: 524.26 Last: 6556)
|
|
Model-Level : 212.0
|
|
Problems : 17 (Average Length: 32.59 Splits: 0)
|
|
Lemmas : 625438 (Deleted: 573134)
|
|
Binary : 16821 (Ratio: 2.69%)
|
|
Ternary : 4007 (Ratio: 0.64%)
|
|
Conflict : 625438 (Average Length: 1339.8 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 625438 (Average: 9.09 Max: 678 Sum: 5687043)
|
|
Executed : 625333 (Average: 9.09 Max: 678 Sum: 5685123 Ratio: 99.97%)
|
|
Bounded : 105 (Average: 18.29 Max: 67 Sum: 1920 Ratio: 0.03%)
|
|
|
|
Rules : 76935 (Original: 75225)
|
|
Atoms : 61653
|
|
Bodies : 14003 (Original: 12292)
|
|
Count : 291 (Original: 633)
|
|
Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813)
|
|
Tight : Yes
|
|
Variables : 413146 (Eliminated: 2052 Frozen: 399364)
|
|
Constraints : 3003059 (Binary: 91.3% Ternary: 6.8% Other: 1.9%)
|
|
|
|
Memory Peak : 792MB
|
|
Max. Length : 60 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 56.72s
|
|
Memory: 783MB (+47MB)
|
|
UNKNOWN
|
|
Iteration Time: 57.55s
|
|
|
|
Iteration 17
|
|
Queue: [(14,70,0,True), (15,75,0,True), (16,80,0,True), (17,85,0,True), (18,90,0,True)]
|
|
Grounded Until: 65
|
|
Expected Memory: 874.0MB
|
|
Grounding... [('step', [66]), ('step', [67]), ('step', [68]), ('step', [69]), ('step', [70]), ('check', [70])]
|
|
Grounding Time: 0.49s
|
|
Memory: 783MB (+0MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 18
|
|
Time : 672.036s (Solving: 652.30s 1st Model: 0.00s Unsat: 48.43s)
|
|
CPU Time : 672.192s
|
|
|
|
Choices : 6613763 (Domain: 6350686)
|
|
Conflicts : 673848 (Analyzed: 673844)
|
|
Restarts : 1293 (Average: 521.15 Last: 6556)
|
|
Model-Level : 212.0
|
|
Problems : 18 (Average Length: 34.78 Splits: 0)
|
|
Lemmas : 673844 (Deleted: 614613)
|
|
Binary : 18005 (Ratio: 2.67%)
|
|
Ternary : 4270 (Ratio: 0.63%)
|
|
Conflict : 673844 (Average Length: 1329.5 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 673844 (Average: 9.34 Max: 678 Sum: 6295176)
|
|
Executed : 673735 (Average: 9.34 Max: 678 Sum: 6292968 Ratio: 99.96%)
|
|
Bounded : 109 (Average: 20.26 Max: 72 Sum: 2208 Ratio: 0.04%)
|
|
|
|
Rules : 76935 (Original: 75225)
|
|
Atoms : 61653
|
|
Bodies : 14003 (Original: 12292)
|
|
Count : 291 (Original: 633)
|
|
Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813)
|
|
Tight : Yes
|
|
Variables : 446092 (Eliminated: 2052 Frozen: 432310)
|
|
Constraints : 3252630 (Binary: 91.3% Ternary: 6.8% Other: 1.9%)
|
|
|
|
Memory Peak : 838MB
|
|
Max. Length : 65 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 45.04s
|
|
Memory: 801MB (+18MB)
|
|
UNKNOWN
|
|
Iteration Time: 45.90s
|
|
|
|
Iteration 18
|
|
Queue: [(15,75,0,True), (16,80,0,True), (17,85,0,True), (18,90,0,True)]
|
|
Grounded Until: 70
|
|
Expected Memory: 892.0MB
|
|
Grounding... [('step', [71]), ('step', [72]), ('step', [73]), ('step', [74]), ('step', [75]), ('check', [75])]
|
|
Grounding Time: 0.48s
|
|
Memory: 801MB (+0MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 19
|
|
Time : 721.960s (Solving: 700.72s 1st Model: 0.00s Unsat: 48.43s)
|
|
CPU Time : 722.136s
|
|
|
|
Choices : 7343206 (Domain: 7077794)
|
|
Conflicts : 722608 (Analyzed: 722604)
|
|
Restarts : 1393 (Average: 518.74 Last: 6556)
|
|
Model-Level : 212.0
|
|
Problems : 19 (Average Length: 37.00 Splits: 0)
|
|
Lemmas : 722604 (Deleted: 660141)
|
|
Binary : 19478 (Ratio: 2.70%)
|
|
Ternary : 4524 (Ratio: 0.63%)
|
|
Conflict : 722604 (Average Length: 1315.0 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 722604 (Average: 9.67 Max: 678 Sum: 6984308)
|
|
Executed : 722495 (Average: 9.66 Max: 678 Sum: 6982100 Ratio: 99.97%)
|
|
Bounded : 109 (Average: 20.26 Max: 72 Sum: 2208 Ratio: 0.03%)
|
|
|
|
Rules : 76935 (Original: 75225)
|
|
Atoms : 61653
|
|
Bodies : 14003 (Original: 12292)
|
|
Count : 291 (Original: 633)
|
|
Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813)
|
|
Tight : Yes
|
|
Variables : 479038 (Eliminated: 2052 Frozen: 465256)
|
|
Constraints : 3502157 (Binary: 91.3% Ternary: 6.8% Other: 1.9%)
|
|
|
|
Memory Peak : 863MB
|
|
Max. Length : 70 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 49.10s
|
|
Memory: 820MB (+19MB)
|
|
UNKNOWN
|
|
Iteration Time: 49.96s
|
|
|
|
Iteration 19
|
|
Queue: [(16,80,0,True), (17,85,0,True), (18,90,0,True)]
|
|
Grounded Until: 75
|
|
Expected Memory: 911.0MB
|
|
Grounding... [('step', [76]), ('step', [77]), ('step', [78]), ('step', [79]), ('step', [80]), ('check', [80])]
|
|
Grounding Time: 0.46s
|
|
Memory: 820MB (+0MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 20
|
|
Time : 774.130s (Solving: 751.41s 1st Model: 0.00s Unsat: 48.43s)
|
|
CPU Time : 774.328s
|
|
|
|
Choices : 7918028 (Domain: 7651768)
|
|
Conflicts : 774028 (Analyzed: 774024)
|
|
Restarts : 1493 (Average: 518.44 Last: 6556)
|
|
Model-Level : 212.0
|
|
Problems : 20 (Average Length: 39.25 Splits: 0)
|
|
Lemmas : 774024 (Deleted: 706795)
|
|
Binary : 20297 (Ratio: 2.62%)
|
|
Ternary : 4649 (Ratio: 0.60%)
|
|
Conflict : 774024 (Average Length: 1322.7 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 774024 (Average: 9.72 Max: 678 Sum: 7523929)
|
|
Executed : 773914 (Average: 9.72 Max: 678 Sum: 7521639 Ratio: 99.97%)
|
|
Bounded : 110 (Average: 20.82 Max: 82 Sum: 2290 Ratio: 0.03%)
|
|
|
|
Rules : 76935 (Original: 75225)
|
|
Atoms : 61653
|
|
Bodies : 14003 (Original: 12292)
|
|
Count : 291 (Original: 633)
|
|
Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813)
|
|
Tight : Yes
|
|
Variables : 511984 (Eliminated: 2052 Frozen: 498202)
|
|
Constraints : 3751742 (Binary: 91.3% Ternary: 6.8% Other: 1.9%)
|
|
|
|
Memory Peak : 888MB
|
|
Max. Length : 75 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 51.36s
|
|
Memory: 843MB (+23MB)
|
|
UNKNOWN
|
|
Iteration Time: 52.20s
|
|
|
|
Iteration 20
|
|
Queue: [(17,85,0,True), (18,90,0,True)]
|
|
Grounded Until: 80
|
|
Expected Memory: 934.0MB
|
|
Grounding... [('step', [81]), ('step', [82]), ('step', [83]), ('step', [84]), ('step', [85]), ('check', [85])]
|
|
Grounding Time: 0.47s
|
|
Memory: 843MB (+0MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 21
|
|
Time : 820.785s (Solving: 796.54s 1st Model: 0.00s Unsat: 48.43s)
|
|
CPU Time : 821.000s
|
|
|
|
Choices : 8415116 (Domain: 8148281)
|
|
Conflicts : 820437 (Analyzed: 820433)
|
|
Restarts : 1593 (Average: 515.02 Last: 6556)
|
|
Model-Level : 212.0
|
|
Problems : 21 (Average Length: 41.52 Splits: 0)
|
|
Lemmas : 820433 (Deleted: 756590)
|
|
Binary : 20842 (Ratio: 2.54%)
|
|
Ternary : 4743 (Ratio: 0.58%)
|
|
Conflict : 820433 (Average Length: 1328.1 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 820433 (Average: 9.73 Max: 678 Sum: 7986310)
|
|
Executed : 820322 (Average: 9.73 Max: 678 Sum: 7983938 Ratio: 99.97%)
|
|
Bounded : 111 (Average: 21.37 Max: 82 Sum: 2372 Ratio: 0.03%)
|
|
|
|
Rules : 76935 (Original: 75225)
|
|
Atoms : 61653
|
|
Bodies : 14003 (Original: 12292)
|
|
Count : 291 (Original: 633)
|
|
Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813)
|
|
Tight : Yes
|
|
Variables : 544930 (Eliminated: 2052 Frozen: 531148)
|
|
Constraints : 4001308 (Binary: 91.3% Ternary: 6.8% Other: 1.9%)
|
|
|
|
Memory Peak : 915MB
|
|
Max. Length : 80 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 45.82s
|
|
Memory: 864MB (+21MB)
|
|
UNKNOWN
|
|
Iteration Time: 46.69s
|
|
|
|
Iteration 21
|
|
Queue: [(18,90,0,True)]
|
|
Grounded Until: 85
|
|
Expected Memory: 955.0MB
|
|
Grounding... [('step', [86]), ('step', [87]), ('step', [88]), ('step', [89]), ('step', [90]), ('check', [90])]
|
|
Grounding Time: 0.47s
|
|
Memory: 864MB (+0MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 22
|
|
Time : 869.186s (Solving: 843.40s 1st Model: 0.00s Unsat: 48.43s)
|
|
CPU Time : 869.424s
|
|
|
|
Choices : 8796028 (Domain: 8529193)
|
|
Conflicts : 865716 (Analyzed: 865712)
|
|
Restarts : 1693 (Average: 511.35 Last: 6556)
|
|
Model-Level : 212.0
|
|
Problems : 22 (Average Length: 43.82 Splits: 0)
|
|
Lemmas : 865712 (Deleted: 801138)
|
|
Binary : 21262 (Ratio: 2.46%)
|
|
Ternary : 4810 (Ratio: 0.56%)
|
|
Conflict : 865712 (Average Length: 1341.2 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 865712 (Average: 9.62 Max: 678 Sum: 8326350)
|
|
Executed : 865600 (Average: 9.62 Max: 678 Sum: 8323886 Ratio: 99.97%)
|
|
Bounded : 112 (Average: 22.00 Max: 92 Sum: 2464 Ratio: 0.03%)
|
|
|
|
Rules : 76935 (Original: 75225)
|
|
Atoms : 61653
|
|
Bodies : 14003 (Original: 12292)
|
|
Count : 291 (Original: 633)
|
|
Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813)
|
|
Tight : Yes
|
|
Variables : 577876 (Eliminated: 2052 Frozen: 564094)
|
|
Constraints : 4250893 (Binary: 91.3% Ternary: 6.8% Other: 1.8%)
|
|
|
|
Memory Peak : 940MB
|
|
Max. Length : 85 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 47.54s
|
|
Memory: 890MB (+26MB)
|
|
UNKNOWN
|
|
Iteration Time: 48.43s
|
|
|
|
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,1,True), (19,95,0,True), (20,100,0,True), (21,105,0,True), (22,110,0,True)]
|
|
Grounded Until: 90
|
|
Blocking actions...
|
|
Solving...
|
|
*** Info : (planner): INTERRUPTED by signal!
|
|
UNKNOWN
|
|
|
|
INTERRUPTED : 1
|
|
|
|
Models : 0+
|
|
Calls : 23
|
|
Time : 893.798s (Solving: 867.86s 1st Model: 0.00s Unsat: 48.43s)
|
|
CPU Time : 894.028s
|
|
|
|
Choices : 8861867 (Domain: 8595032)
|
|
Conflicts : 880634 (Analyzed: 880630)
|
|
Restarts : 1713 (Average: 514.09 Last: 6556)
|
|
Model-Level : 212.0
|
|
Problems : 23 (Average Length: 45.91 Splits: 0)
|
|
Lemmas : 880630 (Deleted: 819906)
|
|
Binary : 21307 (Ratio: 2.42%)
|
|
Ternary : 4818 (Ratio: 0.55%)
|
|
Conflict : 880630 (Average Length: 1360.6 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 880630 (Average: 9.53 Max: 678 Sum: 8388770)
|
|
Executed : 880518 (Average: 9.52 Max: 678 Sum: 8386306 Ratio: 99.97%)
|
|
Bounded : 112 (Average: 22.00 Max: 92 Sum: 2464 Ratio: 0.03%)
|
|
|
|
Rules : 76935 (Original: 75225)
|
|
Atoms : 61653
|
|
Bodies : 14003 (Original: 12292)
|
|
Count : 291 (Original: 633)
|
|
Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813)
|
|
Tight : Yes
|
|
Variables : 577876 (Eliminated: 2052 Frozen: 575824)
|
|
Constraints : 4250874 (Binary: 91.3% Ternary: 6.8% Other: 1.8%)
|
|
|
|
Memory Peak : 940MB
|
|
Max. Length : 90 steps
|
|
Models : 1
|
|
|
|
|