1446 lines
52 KiB
Plaintext
1446 lines
52 KiB
Plaintext
INFO Running translator.
|
|
INFO translator input: ['/home/pluehne/Documents/ASP/pddl-instances/ipc-2011/domains/elevator-sequential-satisficing/domain.pddl', '/home/pluehne/Documents/ASP/pddl-instances/ipc-2011/domains/elevator-sequential-satisficing/instances/instance-8.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/elevator-sequential-satisficing/domain.pddl /home/pluehne/Documents/ASP/pddl-instances/ipc-2011/domains/elevator-sequential-satisficing/instances/instance-8.pddl
|
|
Parsing...
|
|
Parsing: [0.080s CPU, 0.071s wall-clock]
|
|
Normalizing task... [0.000s CPU, 0.003s wall-clock]
|
|
Instantiating...
|
|
Generating Datalog program... [0.020s CPU, 0.018s wall-clock]
|
|
Normalizing Datalog program...
|
|
Normalizing Datalog program: [0.020s CPU, 0.027s wall-clock]
|
|
Preparing model... [0.050s CPU, 0.053s wall-clock]
|
|
Generated 46 rules.
|
|
Computing model... [1.650s CPU, 1.653s wall-clock]
|
|
14616 relevant atoms
|
|
6960 auxiliary atoms
|
|
21576 final queue length
|
|
46203 total queue pushes
|
|
Completing instantiation... [4.780s CPU, 4.771s wall-clock]
|
|
Instantiating: [6.540s CPU, 6.542s wall-clock]
|
|
Computing fact groups...
|
|
Finding invariants...
|
|
12 initial candidates
|
|
Finding invariants: [0.080s CPU, 0.082s wall-clock]
|
|
Checking invariant weight... [0.010s CPU, 0.004s wall-clock]
|
|
Instantiating groups... [0.060s CPU, 0.064s wall-clock]
|
|
Collecting mutex groups... [0.010s CPU, 0.007s wall-clock]
|
|
Choosing groups...
|
|
0 uncovered facts
|
|
Choosing groups: [0.020s CPU, 0.020s wall-clock]
|
|
Building translation key... [0.010s CPU, 0.012s wall-clock]
|
|
Computing fact groups: [0.240s CPU, 0.241s wall-clock]
|
|
Building STRIPS to SAS dictionary... [0.010s CPU, 0.006s wall-clock]
|
|
Building dictionary for full mutex groups... [0.000s CPU, 0.008s wall-clock]
|
|
Building mutex information...
|
|
Building mutex information: [0.010s CPU, 0.006s wall-clock]
|
|
Translating task...
|
|
Processing axioms...
|
|
Simplifying axioms... [0.000s CPU, 0.000s wall-clock]
|
|
Processing axioms: [0.220s CPU, 0.216s wall-clock]
|
|
Translating task: [4.170s CPU, 4.163s wall-clock]
|
|
0 effect conditions simplified
|
|
0 implied preconditions added
|
|
Detecting unreachable propositions...
|
|
0 operators removed
|
|
0 axioms removed
|
|
43 propositions removed
|
|
Detecting unreachable propositions: [2.110s CPU, 2.103s wall-clock]
|
|
Reordering and filtering variables...
|
|
43 of 43 variables necessary.
|
|
0 of 43 mutex groups necessary.
|
|
12972 of 12972 operators necessary.
|
|
0 of 0 axiom rules necessary.
|
|
Reordering and filtering variables: [0.610s CPU, 0.613s wall-clock]
|
|
Translator variables: 43
|
|
Translator derived variables: 0
|
|
Translator facts: 1060
|
|
Translator goal facts: 33
|
|
Translator mutex groups: 0
|
|
Translator total mutex groups size: 0
|
|
Translator operators: 12972
|
|
Translator axioms: 0
|
|
Translator task size: 78068
|
|
Translator peak memory: 86988 KB
|
|
Writing output... [1.370s CPU, 1.475s wall-clock]
|
|
Done! [15.310s CPU, 15.407s wall-clock]
|
|
planner.py version 0.0.1
|
|
|
|
Time: 3.25s
|
|
Memory: 265MB
|
|
|
|
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 : 3.737s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
|
|
CPU Time : 3.272s
|
|
|
|
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 : 235886
|
|
Atoms : 235886
|
|
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 : 401MB
|
|
Max. Length : 0 steps
|
|
Models : 0
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 0.02s
|
|
Memory: 337MB (+72MB)
|
|
UNSAT
|
|
Iteration Time: 0.02s
|
|
|
|
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: 337MB
|
|
Grounding... [('step', [1]), ('step', [2]), ('step', [3]), ('step', [4]), ('step', [5]), ('check', [5])]
|
|
Grounding Time: 1.06s
|
|
Memory: 337MB (+0MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0
|
|
Calls : 2
|
|
Time : 5.605s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
|
|
CPU Time : 5.140s
|
|
|
|
Choices : 0
|
|
Conflicts : 0 (Analyzed: 0)
|
|
Restarts : 0
|
|
Problems : 2 (Average Length: 4.50 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 : 235886
|
|
Atoms : 235886
|
|
Bodies : 1 (Original: 0)
|
|
Tight : Yes
|
|
Variables : 61661 (Eliminated: 0 Frozen: 4221)
|
|
Constraints : 107675 (Binary: 96.8% Ternary: 1.5% Other: 1.7%)
|
|
|
|
Memory Peak : 401MB
|
|
Max. Length : 0 steps
|
|
Models : 0
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 0.19s
|
|
Memory: 350MB (+13MB)
|
|
UNSAT
|
|
Iteration Time: 1.87s
|
|
|
|
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: 363.0MB
|
|
Grounding... [('step', [6]), ('step', [7]), ('step', [8]), ('step', [9]), ('step', [10]), ('check', [10])]
|
|
Grounding Time: 1.22s
|
|
Memory: 360MB (+10MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 3
|
|
Time : 10.293s (Solving: 2.82s 1st Model: 0.00s Unsat: 0.00s)
|
|
CPU Time : 9.832s
|
|
|
|
Choices : 87257 (Domain: 87257)
|
|
Conflicts : 10326 (Analyzed: 10326)
|
|
Restarts : 100 (Average: 103.26 Last: 103)
|
|
Problems : 3 (Average Length: 7.00 Splits: 0)
|
|
Lemmas : 10326 (Deleted: 6063)
|
|
Binary : 247 (Ratio: 2.39%)
|
|
Ternary : 121 (Ratio: 1.17%)
|
|
Conflict : 10326 (Average Length: 441.5 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 10326 (Average: 7.91 Max: 398 Sum: 81642)
|
|
Executed : 10325 (Average: 7.91 Max: 398 Sum: 81641 Ratio: 100.00%)
|
|
Bounded : 1 (Average: 1.00 Max: 1 Sum: 1 Ratio: 0.00%)
|
|
|
|
Rules : 235886
|
|
Atoms : 235886
|
|
Bodies : 1 (Original: 0)
|
|
Tight : Yes
|
|
Variables : 134789 (Eliminated: 0 Frozen: 9342)
|
|
Constraints : 666499 (Binary: 97.9% Ternary: 1.0% Other: 1.1%)
|
|
|
|
Memory Peak : 401MB
|
|
Max. Length : 5 steps
|
|
Models : 0
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 2.89s
|
|
Memory: 399MB (+39MB)
|
|
UNKNOWN
|
|
Iteration Time: 4.70s
|
|
|
|
Iteration 4
|
|
Queue: [(3,15,0,True), (4,20,0,True), (5,25,0,True), (6,30,0,True)]
|
|
Grounded Until: 10
|
|
Expected Memory: 448.0MB
|
|
Grounding... [('step', [11]), ('step', [12]), ('step', [13]), ('step', [14]), ('step', [15]), ('check', [15])]
|
|
Grounding Time: 1.08s
|
|
Memory: 419MB (+20MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 4
|
|
Time : 16.571s (Solving: 7.35s 1st Model: 0.00s Unsat: 0.00s)
|
|
CPU Time : 16.116s
|
|
|
|
Choices : 245213 (Domain: 245213)
|
|
Conflicts : 20914 (Analyzed: 20914)
|
|
Restarts : 200 (Average: 104.57 Last: 103)
|
|
Problems : 4 (Average Length: 9.50 Splits: 0)
|
|
Lemmas : 20914 (Deleted: 15675)
|
|
Binary : 384 (Ratio: 1.84%)
|
|
Ternary : 223 (Ratio: 1.07%)
|
|
Conflict : 20914 (Average Length: 534.0 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 20914 (Average: 10.37 Max: 592 Sum: 216806)
|
|
Executed : 20909 (Average: 10.37 Max: 592 Sum: 216801 Ratio: 100.00%)
|
|
Bounded : 5 (Average: 1.00 Max: 1 Sum: 5 Ratio: 0.00%)
|
|
|
|
Rules : 235886
|
|
Atoms : 235886
|
|
Bodies : 1 (Original: 0)
|
|
Tight : Yes
|
|
Variables : 210475 (Eliminated: 0 Frozen: 14567)
|
|
Constraints : 1255414 (Binary: 98.0% Ternary: 1.0% Other: 1.1%)
|
|
|
|
Memory Peak : 468MB
|
|
Max. Length : 10 steps
|
|
Models : 0
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 4.60s
|
|
Memory: 468MB (+49MB)
|
|
UNKNOWN
|
|
Iteration Time: 6.29s
|
|
|
|
Iteration 5
|
|
Queue: [(4,20,0,True), (5,25,0,True), (6,30,0,True)]
|
|
Grounded Until: 15
|
|
Expected Memory: 537.0MB
|
|
Grounding... [('step', [16]), ('step', [17]), ('step', [18]), ('step', [19]), ('step', [20]), ('check', [20])]
|
|
Grounding Time: 1.10s
|
|
Memory: 491MB (+23MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 5
|
|
Time : 25.394s (Solving: 14.37s 1st Model: 0.00s Unsat: 0.00s)
|
|
CPU Time : 24.944s
|
|
|
|
Choices : 592270 (Domain: 592270)
|
|
Conflicts : 32290 (Analyzed: 32290)
|
|
Restarts : 300 (Average: 107.63 Last: 103)
|
|
Problems : 5 (Average Length: 12.00 Splits: 0)
|
|
Lemmas : 32290 (Deleted: 26257)
|
|
Binary : 482 (Ratio: 1.49%)
|
|
Ternary : 328 (Ratio: 1.02%)
|
|
Conflict : 32290 (Average Length: 563.8 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 32290 (Average: 15.53 Max: 1990 Sum: 501341)
|
|
Executed : 32278 (Average: 15.53 Max: 1990 Sum: 501329 Ratio: 100.00%)
|
|
Bounded : 12 (Average: 1.00 Max: 1 Sum: 12 Ratio: 0.00%)
|
|
|
|
Rules : 235886
|
|
Atoms : 235886
|
|
Bodies : 1 (Original: 0)
|
|
Tight : Yes
|
|
Variables : 286161 (Eliminated: 0 Frozen: 19792)
|
|
Constraints : 1844329 (Binary: 98.0% Ternary: 0.9% Other: 1.0%)
|
|
|
|
Memory Peak : 540MB
|
|
Max. Length : 15 steps
|
|
Models : 0
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 7.11s
|
|
Memory: 516MB (+25MB)
|
|
UNKNOWN
|
|
Iteration Time: 8.84s
|
|
|
|
Iteration 6
|
|
Queue: [(5,25,0,True), (6,30,0,True)]
|
|
Grounded Until: 20
|
|
Expected Memory: 585.0MB
|
|
Grounding... [('step', [21]), ('step', [22]), ('step', [23]), ('step', [24]), ('step', [25]), ('check', [25])]
|
|
Grounding Time: 1.15s
|
|
Memory: 552MB (+36MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 1+
|
|
Calls : 6
|
|
Time : 38.156s (Solving: 25.23s 1st Model: 10.83s Unsat: 0.00s)
|
|
CPU Time : 37.712s
|
|
|
|
Choices : 1170975 (Domain: 1170939)
|
|
Conflicts : 42440 (Analyzed: 42440)
|
|
Restarts : 392 (Average: 108.27 Last: 103)
|
|
Model-Level : 2556.0
|
|
Problems : 6 (Average Length: 14.50 Splits: 0)
|
|
Lemmas : 42440 (Deleted: 33910)
|
|
Binary : 593 (Ratio: 1.40%)
|
|
Ternary : 401 (Ratio: 0.94%)
|
|
Conflict : 42440 (Average Length: 612.1 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 42440 (Average: 23.30 Max: 2539 Sum: 988953)
|
|
Executed : 42416 (Average: 23.30 Max: 2539 Sum: 988929 Ratio: 100.00%)
|
|
Bounded : 24 (Average: 1.00 Max: 1 Sum: 24 Ratio: 0.00%)
|
|
|
|
Rules : 235886
|
|
Atoms : 235886
|
|
Bodies : 1 (Original: 0)
|
|
Tight : Yes
|
|
Variables : 361847 (Eliminated: 0 Frozen: 25017)
|
|
Constraints : 2433244 (Binary: 98.1% Ternary: 0.9% Other: 1.0%)
|
|
|
|
Memory Peak : 609MB
|
|
Max. Length : 20 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 10.97s
|
|
Memory: 607MB (+55MB)
|
|
SAT
|
|
Testing...
|
|
NOT SERIALIZABLE
|
|
Testing Time: 5.39s
|
|
Memory: 733MB (+126MB)
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 7
|
|
Time : 81.864s (Solving: 65.77s 1st Model: 10.83s Unsat: 0.00s)
|
|
CPU Time : 81.436s
|
|
|
|
Choices : 3093068 (Domain: 3093032)
|
|
Conflicts : 52384 (Analyzed: 52384)
|
|
Restarts : 492 (Average: 106.47 Last: 120)
|
|
Model-Level : 2556.0
|
|
Problems : 7 (Average Length: 16.29 Splits: 0)
|
|
Lemmas : 52384 (Deleted: 42816)
|
|
Binary : 675 (Ratio: 1.29%)
|
|
Ternary : 491 (Ratio: 0.94%)
|
|
Conflict : 52384 (Average Length: 652.0 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 52384 (Average: 54.19 Max: 2907 Sum: 2838701)
|
|
Executed : 52338 (Average: 54.18 Max: 2907 Sum: 2838083 Ratio: 99.98%)
|
|
Bounded : 46 (Average: 13.43 Max: 27 Sum: 618 Ratio: 0.02%)
|
|
|
|
Rules : 1053757 (Original: 1053711)
|
|
Atoms : 263807
|
|
Bodies : 531222 (Original: 531175)
|
|
Count : 1005 (Original: 1013)
|
|
Equivalences : 269260 (Atom=Atom: 36 Body=Body: 0 Other: 269224)
|
|
Tight : Yes
|
|
Variables : 363963 (Eliminated: 0 Frozen: 294147)
|
|
Constraints : 3226526 (Binary: 98.5% Ternary: 0.7% Other: 0.8%)
|
|
|
|
Memory Peak : 733MB
|
|
Max. Length : 20 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 41.14s
|
|
Memory: 689MB (+-44MB)
|
|
UNKNOWN
|
|
Iteration Time: 59.31s
|
|
|
|
Iteration 7
|
|
Queue: [(6,30,0,True)]
|
|
Grounded Until: 25
|
|
Expected Memory: 780.0MB
|
|
Grounding... [('step', [26]), ('step', [27]), ('step', [28]), ('step', [29]), ('step', [30]), ('check', [30])]
|
|
Grounding Time: 2.22s
|
|
Memory: 739MB (+50MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 8
|
|
Time : 98.640s (Solving: 79.43s 1st Model: 10.83s Unsat: 0.00s)
|
|
CPU Time : 98.220s
|
|
|
|
Choices : 3576018 (Domain: 3575982)
|
|
Conflicts : 61498 (Analyzed: 61498)
|
|
Restarts : 592 (Average: 103.88 Last: 120)
|
|
Model-Level : 2556.0
|
|
Problems : 8 (Average Length: 18.25 Splits: 0)
|
|
Lemmas : 61498 (Deleted: 52468)
|
|
Binary : 829 (Ratio: 1.35%)
|
|
Ternary : 530 (Ratio: 0.86%)
|
|
Conflict : 61498 (Average Length: 818.5 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 61498 (Average: 52.23 Max: 2907 Sum: 3212060)
|
|
Executed : 61374 (Average: 52.18 Max: 2907 Sum: 3208946 Ratio: 99.90%)
|
|
Bounded : 124 (Average: 25.11 Max: 32 Sum: 3114 Ratio: 0.10%)
|
|
|
|
Rules : 1053757 (Original: 1053711)
|
|
Atoms : 263807
|
|
Bodies : 531222 (Original: 531175)
|
|
Count : 1005 (Original: 1013)
|
|
Equivalences : 269260 (Atom=Atom: 36 Body=Body: 0 Other: 269224)
|
|
Tight : Yes
|
|
Variables : 440079 (Eliminated: 0 Frozen: 364447)
|
|
Constraints : 4003977 (Binary: 98.5% Ternary: 0.7% Other: 0.8%)
|
|
|
|
Memory Peak : 814MB
|
|
Max. Length : 25 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 13.78s
|
|
Memory: 814MB (+75MB)
|
|
UNKNOWN
|
|
Iteration Time: 16.79s
|
|
|
|
Iteration 8
|
|
Queue: [(2,10,1,True), (3,15,1,True), (4,20,1,True), (5,25,1,True), (6,30,1,True), (7,35,0,True), (8,40,0,True), (9,45,0,True), (10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True)]
|
|
Grounded Until: 30
|
|
Blocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0
|
|
Calls : 9
|
|
Time : 105.528s (Solving: 86.19s 1st Model: 10.83s Unsat: 6.75s)
|
|
CPU Time : 105.112s
|
|
|
|
Choices : 3797973 (Domain: 3797937)
|
|
Conflicts : 69553 (Analyzed: 69552)
|
|
Restarts : 676 (Average: 102.89 Last: 120)
|
|
Model-Level : 2556.0
|
|
Problems : 9 (Average Length: 19.78 Splits: 0)
|
|
Lemmas : 69552 (Deleted: 58923)
|
|
Binary : 994 (Ratio: 1.43%)
|
|
Ternary : 705 (Ratio: 1.01%)
|
|
Conflict : 69552 (Average Length: 754.1 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 69552 (Average: 49.35 Max: 2907 Sum: 3432364)
|
|
Executed : 69357 (Average: 49.27 Max: 2907 Sum: 3427133 Ratio: 99.85%)
|
|
Bounded : 195 (Average: 26.83 Max: 32 Sum: 5231 Ratio: 0.15%)
|
|
|
|
Rules : 1053757 (Original: 1053711)
|
|
Atoms : 263807
|
|
Bodies : 531222 (Original: 531175)
|
|
Count : 1005 (Original: 1013)
|
|
Equivalences : 269260 (Atom=Atom: 36 Body=Body: 0 Other: 269224)
|
|
Tight : Yes
|
|
Variables : 440079 (Eliminated: 0 Frozen: 364447)
|
|
Constraints : 3951492 (Binary: 98.5% Ternary: 0.7% Other: 0.8%)
|
|
|
|
Memory Peak : 814MB
|
|
Max. Length : 30 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 6.83s
|
|
Memory: 814MB (+0MB)
|
|
UNSAT
|
|
Iteration Time: 6.89s
|
|
|
|
Iteration 9
|
|
Queue: [(3,15,1,True), (4,20,1,True), (5,25,1,True), (6,30,1,True), (7,35,0,True), (8,40,0,True), (9,45,0,True), (10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True)]
|
|
Grounded Until: 30
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 10
|
|
Time : 122.837s (Solving: 103.39s 1st Model: 10.83s Unsat: 6.75s)
|
|
CPU Time : 122.432s
|
|
|
|
Choices : 4311252 (Domain: 4311216)
|
|
Conflicts : 79696 (Analyzed: 79695)
|
|
Restarts : 776 (Average: 102.70 Last: 170)
|
|
Model-Level : 2556.0
|
|
Problems : 10 (Average Length: 21.00 Splits: 0)
|
|
Lemmas : 79695 (Deleted: 67031)
|
|
Binary : 1106 (Ratio: 1.39%)
|
|
Ternary : 820 (Ratio: 1.03%)
|
|
Conflict : 79695 (Average Length: 707.1 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 79695 (Average: 49.38 Max: 2907 Sum: 3935461)
|
|
Executed : 79460 (Average: 49.30 Max: 2907 Sum: 3928950 Ratio: 99.83%)
|
|
Bounded : 235 (Average: 27.71 Max: 32 Sum: 6511 Ratio: 0.17%)
|
|
|
|
Rules : 1053757 (Original: 1053711)
|
|
Atoms : 263807
|
|
Bodies : 531222 (Original: 531175)
|
|
Count : 1005 (Original: 1013)
|
|
Equivalences : 269260 (Atom=Atom: 36 Body=Body: 0 Other: 269224)
|
|
Tight : Yes
|
|
Variables : 440079 (Eliminated: 0 Frozen: 364447)
|
|
Constraints : 3934565 (Binary: 98.5% Ternary: 0.7% Other: 0.8%)
|
|
|
|
Memory Peak : 814MB
|
|
Max. Length : 30 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 17.28s
|
|
Memory: 814MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 17.32s
|
|
|
|
Iteration 10
|
|
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)]
|
|
Grounded Until: 30
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 11
|
|
Time : 148.524s (Solving: 128.95s 1st Model: 10.83s Unsat: 6.75s)
|
|
CPU Time : 148.128s
|
|
|
|
Choices : 5132459 (Domain: 5132423)
|
|
Conflicts : 90667 (Analyzed: 90666)
|
|
Restarts : 876 (Average: 103.50 Last: 170)
|
|
Model-Level : 2556.0
|
|
Problems : 11 (Average Length: 22.00 Splits: 0)
|
|
Lemmas : 90666 (Deleted: 75818)
|
|
Binary : 1186 (Ratio: 1.31%)
|
|
Ternary : 921 (Ratio: 1.02%)
|
|
Conflict : 90666 (Average Length: 731.9 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 90666 (Average: 52.06 Max: 2907 Sum: 4720078)
|
|
Executed : 90419 (Average: 51.98 Max: 2907 Sum: 4713183 Ratio: 99.85%)
|
|
Bounded : 247 (Average: 27.91 Max: 32 Sum: 6895 Ratio: 0.15%)
|
|
|
|
Rules : 1053757 (Original: 1053711)
|
|
Atoms : 263807
|
|
Bodies : 531222 (Original: 531175)
|
|
Count : 1005 (Original: 1013)
|
|
Equivalences : 269260 (Atom=Atom: 36 Body=Body: 0 Other: 269224)
|
|
Tight : Yes
|
|
Variables : 440079 (Eliminated: 0 Frozen: 364447)
|
|
Constraints : 3916842 (Binary: 98.5% Ternary: 0.7% Other: 0.8%)
|
|
|
|
Memory Peak : 814MB
|
|
Max. Length : 30 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 25.64s
|
|
Memory: 814MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 25.70s
|
|
|
|
Iteration 11
|
|
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)]
|
|
Grounded Until: 30
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 12
|
|
Time : 178.423s (Solving: 158.72s 1st Model: 10.83s Unsat: 6.75s)
|
|
CPU Time : 178.040s
|
|
|
|
Choices : 6391806 (Domain: 6391770)
|
|
Conflicts : 100683 (Analyzed: 100682)
|
|
Restarts : 976 (Average: 103.16 Last: 170)
|
|
Model-Level : 2556.0
|
|
Problems : 12 (Average Length: 22.83 Splits: 0)
|
|
Lemmas : 100682 (Deleted: 86447)
|
|
Binary : 1245 (Ratio: 1.24%)
|
|
Ternary : 992 (Ratio: 0.99%)
|
|
Conflict : 100682 (Average Length: 752.3 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 100682 (Average: 58.62 Max: 2907 Sum: 5902110)
|
|
Executed : 100422 (Average: 58.55 Max: 2907 Sum: 5894799 Ratio: 99.88%)
|
|
Bounded : 260 (Average: 28.12 Max: 32 Sum: 7311 Ratio: 0.12%)
|
|
|
|
Rules : 1053757 (Original: 1053711)
|
|
Atoms : 263807
|
|
Bodies : 531222 (Original: 531175)
|
|
Count : 1005 (Original: 1013)
|
|
Equivalences : 269260 (Atom=Atom: 36 Body=Body: 0 Other: 269224)
|
|
Tight : Yes
|
|
Variables : 440079 (Eliminated: 0 Frozen: 364447)
|
|
Constraints : 3915564 (Binary: 98.5% Ternary: 0.7% Other: 0.8%)
|
|
|
|
Memory Peak : 814MB
|
|
Max. Length : 30 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 29.86s
|
|
Memory: 814MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 29.91s
|
|
|
|
Iteration 12
|
|
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)]
|
|
Grounded Until: 30
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 13
|
|
Time : 221.900s (Solving: 202.09s 1st Model: 10.83s Unsat: 6.75s)
|
|
CPU Time : 221.536s
|
|
|
|
Choices : 7541638 (Domain: 7541602)
|
|
Conflicts : 110564 (Analyzed: 110563)
|
|
Restarts : 1076 (Average: 102.75 Last: 170)
|
|
Model-Level : 2556.0
|
|
Problems : 13 (Average Length: 23.54 Splits: 0)
|
|
Lemmas : 110563 (Deleted: 95505)
|
|
Binary : 1339 (Ratio: 1.21%)
|
|
Ternary : 1058 (Ratio: 0.96%)
|
|
Conflict : 110563 (Average Length: 787.1 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 110563 (Average: 63.42 Max: 5071 Sum: 7011410)
|
|
Executed : 110299 (Average: 63.35 Max: 5071 Sum: 7003971 Ratio: 99.89%)
|
|
Bounded : 264 (Average: 28.18 Max: 32 Sum: 7439 Ratio: 0.11%)
|
|
|
|
Rules : 1053757 (Original: 1053711)
|
|
Atoms : 263807
|
|
Bodies : 531222 (Original: 531175)
|
|
Count : 1005 (Original: 1013)
|
|
Equivalences : 269260 (Atom=Atom: 36 Body=Body: 0 Other: 269224)
|
|
Tight : Yes
|
|
Variables : 440079 (Eliminated: 0 Frozen: 364447)
|
|
Constraints : 3915130 (Binary: 98.5% Ternary: 0.7% Other: 0.8%)
|
|
|
|
Memory Peak : 942MB
|
|
Max. Length : 30 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 43.46s
|
|
Memory: 878MB (+64MB)
|
|
UNKNOWN
|
|
Iteration Time: 43.50s
|
|
|
|
Iteration 13
|
|
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)]
|
|
Grounded Until: 30
|
|
Expected Memory: 1003.0MB
|
|
Grounding... [('step', [31]), ('step', [32]), ('step', [33]), ('step', [34]), ('step', [35]), ('check', [35])]
|
|
Grounding Time: 1.91s
|
|
Memory: 878MB (+0MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 14
|
|
Time : 255.212s (Solving: 232.53s 1st Model: 10.83s Unsat: 6.75s)
|
|
CPU Time : 254.860s
|
|
|
|
Choices : 8295022 (Domain: 8294986)
|
|
Conflicts : 120707 (Analyzed: 120706)
|
|
Restarts : 1176 (Average: 102.64 Last: 170)
|
|
Model-Level : 2556.0
|
|
Problems : 14 (Average Length: 24.50 Splits: 0)
|
|
Lemmas : 120706 (Deleted: 106370)
|
|
Binary : 1374 (Ratio: 1.14%)
|
|
Ternary : 1095 (Ratio: 0.91%)
|
|
Conflict : 120706 (Average Length: 899.8 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 120706 (Average: 63.85 Max: 5071 Sum: 7706744)
|
|
Executed : 120413 (Average: 63.78 Max: 5071 Sum: 7698232 Ratio: 99.89%)
|
|
Bounded : 293 (Average: 29.05 Max: 37 Sum: 8512 Ratio: 0.11%)
|
|
|
|
Rules : 1053757 (Original: 1053711)
|
|
Atoms : 263807
|
|
Bodies : 531222 (Original: 531175)
|
|
Count : 1005 (Original: 1013)
|
|
Equivalences : 269260 (Atom=Atom: 36 Body=Body: 0 Other: 269224)
|
|
Tight : Yes
|
|
Variables : 516195 (Eliminated: 0 Frozen: 434747)
|
|
Constraints : 4696135 (Binary: 98.5% Ternary: 0.7% Other: 0.8%)
|
|
|
|
Memory Peak : 952MB
|
|
Max. Length : 30 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 30.58s
|
|
Memory: 945MB (+67MB)
|
|
UNKNOWN
|
|
Iteration Time: 33.34s
|
|
|
|
Iteration 14
|
|
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)]
|
|
Grounded Until: 35
|
|
Expected Memory: 1070.0MB
|
|
Grounding... [('step', [36]), ('step', [37]), ('step', [38]), ('step', [39]), ('step', [40]), ('check', [40])]
|
|
Grounding Time: 1.94s
|
|
Memory: 955MB (+10MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 15
|
|
Time : 283.097s (Solving: 257.45s 1st Model: 10.83s Unsat: 6.75s)
|
|
CPU Time : 282.756s
|
|
|
|
Choices : 9147251 (Domain: 9147215)
|
|
Conflicts : 130961 (Analyzed: 130960)
|
|
Restarts : 1276 (Average: 102.63 Last: 170)
|
|
Model-Level : 2556.0
|
|
Problems : 15 (Average Length: 25.67 Splits: 0)
|
|
Lemmas : 130960 (Deleted: 114360)
|
|
Binary : 1396 (Ratio: 1.07%)
|
|
Ternary : 1117 (Ratio: 0.85%)
|
|
Conflict : 130960 (Average Length: 965.6 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 130960 (Average: 64.60 Max: 5071 Sum: 8459482)
|
|
Executed : 130651 (Average: 64.53 Max: 5071 Sum: 8450298 Ratio: 99.89%)
|
|
Bounded : 309 (Average: 29.72 Max: 42 Sum: 9184 Ratio: 0.11%)
|
|
|
|
Rules : 1053757 (Original: 1053711)
|
|
Atoms : 263807
|
|
Bodies : 531222 (Original: 531175)
|
|
Count : 1005 (Original: 1013)
|
|
Equivalences : 269260 (Atom=Atom: 36 Body=Body: 0 Other: 269224)
|
|
Tight : Yes
|
|
Variables : 592311 (Eliminated: 0 Frozen: 505047)
|
|
Constraints : 5469571 (Binary: 98.5% Ternary: 0.7% Other: 0.8%)
|
|
|
|
Memory Peak : 1057MB
|
|
Max. Length : 35 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 25.08s
|
|
Memory: 1001MB (+46MB)
|
|
UNKNOWN
|
|
Iteration Time: 27.91s
|
|
|
|
Iteration 15
|
|
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)]
|
|
Grounded Until: 40
|
|
Expected Memory: 1126.0MB
|
|
Grounding... [('step', [41]), ('step', [42]), ('step', [43]), ('step', [44]), ('step', [45]), ('check', [45])]
|
|
Grounding Time: 2.00s
|
|
Memory: 1039MB (+38MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 16
|
|
Time : 330.460s (Solving: 301.77s 1st Model: 10.83s Unsat: 6.75s)
|
|
CPU Time : 330.140s
|
|
|
|
Choices : 10064112 (Domain: 10064076)
|
|
Conflicts : 140836 (Analyzed: 140835)
|
|
Restarts : 1376 (Average: 102.35 Last: 170)
|
|
Model-Level : 2556.0
|
|
Problems : 16 (Average Length: 27.00 Splits: 0)
|
|
Lemmas : 140835 (Deleted: 125302)
|
|
Binary : 1410 (Ratio: 1.00%)
|
|
Ternary : 1142 (Ratio: 0.81%)
|
|
Conflict : 140835 (Average Length: 1020.1 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 140835 (Average: 66.03 Max: 5071 Sum: 9299247)
|
|
Executed : 140526 (Average: 65.96 Max: 5071 Sum: 9290063 Ratio: 99.90%)
|
|
Bounded : 309 (Average: 29.72 Max: 42 Sum: 9184 Ratio: 0.10%)
|
|
|
|
Rules : 1053757 (Original: 1053711)
|
|
Atoms : 263807
|
|
Bodies : 531222 (Original: 531175)
|
|
Count : 1005 (Original: 1013)
|
|
Equivalences : 269260 (Atom=Atom: 36 Body=Body: 0 Other: 269224)
|
|
Tight : Yes
|
|
Variables : 668427 (Eliminated: 0 Frozen: 575347)
|
|
Constraints : 6247655 (Binary: 98.5% Ternary: 0.7% Other: 0.8%)
|
|
|
|
Memory Peak : 1144MB
|
|
Max. Length : 40 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 44.49s
|
|
Memory: 1089MB (+50MB)
|
|
UNKNOWN
|
|
Iteration Time: 47.39s
|
|
|
|
Iteration 16
|
|
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)]
|
|
Grounded Until: 45
|
|
Expected Memory: 1214.0MB
|
|
Grounding... [('step', [46]), ('step', [47]), ('step', [48]), ('step', [49]), ('step', [50]), ('check', [50])]
|
|
Grounding Time: 1.97s
|
|
Memory: 1106MB (+17MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 17
|
|
Time : 364.437s (Solving: 332.66s 1st Model: 10.83s Unsat: 6.75s)
|
|
CPU Time : 364.132s
|
|
|
|
Choices : 10837279 (Domain: 10837243)
|
|
Conflicts : 150161 (Analyzed: 150160)
|
|
Restarts : 1476 (Average: 101.73 Last: 170)
|
|
Model-Level : 2556.0
|
|
Problems : 17 (Average Length: 28.47 Splits: 0)
|
|
Lemmas : 150160 (Deleted: 135673)
|
|
Binary : 1429 (Ratio: 0.95%)
|
|
Ternary : 1154 (Ratio: 0.77%)
|
|
Conflict : 150160 (Average Length: 1099.9 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 150160 (Average: 66.44 Max: 5071 Sum: 9977237)
|
|
Executed : 149846 (Average: 66.38 Max: 5071 Sum: 9967793 Ratio: 99.91%)
|
|
Bounded : 314 (Average: 30.08 Max: 52 Sum: 9444 Ratio: 0.09%)
|
|
|
|
Rules : 1053757 (Original: 1053711)
|
|
Atoms : 263807
|
|
Bodies : 531222 (Original: 531175)
|
|
Count : 1005 (Original: 1013)
|
|
Equivalences : 269260 (Atom=Atom: 36 Body=Body: 0 Other: 269224)
|
|
Tight : Yes
|
|
Variables : 744543 (Eliminated: 0 Frozen: 645647)
|
|
Constraints : 7028795 (Binary: 98.5% Ternary: 0.7% Other: 0.8%)
|
|
|
|
Memory Peak : 1220MB
|
|
Max. Length : 45 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 31.07s
|
|
Memory: 1183MB (+77MB)
|
|
UNKNOWN
|
|
Iteration Time: 34.00s
|
|
|
|
Iteration 17
|
|
Queue: [(11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True)]
|
|
Grounded Until: 50
|
|
Expected Memory: 1308.0MB
|
|
Grounding... [('step', [51]), ('step', [52]), ('step', [53]), ('step', [54]), ('step', [55]), ('check', [55])]
|
|
Grounding Time: 2.00s
|
|
Memory: 1203MB (+20MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 18
|
|
Time : 419.458s (Solving: 384.56s 1st Model: 10.83s Unsat: 6.75s)
|
|
CPU Time : 419.176s
|
|
|
|
Choices : 12031258 (Domain: 12031222)
|
|
Conflicts : 160232 (Analyzed: 160231)
|
|
Restarts : 1576 (Average: 101.67 Last: 170)
|
|
Model-Level : 2556.0
|
|
Problems : 18 (Average Length: 30.06 Splits: 0)
|
|
Lemmas : 160231 (Deleted: 143538)
|
|
Binary : 1466 (Ratio: 0.91%)
|
|
Ternary : 1190 (Ratio: 0.74%)
|
|
Conflict : 160231 (Average Length: 1138.4 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 160231 (Average: 69.21 Max: 5071 Sum: 11090301)
|
|
Executed : 159912 (Average: 69.15 Max: 5071 Sum: 11080572 Ratio: 99.91%)
|
|
Bounded : 319 (Average: 30.50 Max: 57 Sum: 9729 Ratio: 0.09%)
|
|
|
|
Rules : 1053757 (Original: 1053711)
|
|
Atoms : 263807
|
|
Bodies : 531222 (Original: 531175)
|
|
Count : 1005 (Original: 1013)
|
|
Equivalences : 269260 (Atom=Atom: 36 Body=Body: 0 Other: 269224)
|
|
Tight : Yes
|
|
Variables : 820659 (Eliminated: 0 Frozen: 715947)
|
|
Constraints : 7809723 (Binary: 98.5% Ternary: 0.7% Other: 0.8%)
|
|
|
|
Memory Peak : 1327MB
|
|
Max. Length : 50 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 52.10s
|
|
Memory: 1244MB (+41MB)
|
|
UNKNOWN
|
|
Iteration Time: 55.05s
|
|
|
|
Iteration 18
|
|
Queue: [(12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True)]
|
|
Grounded Until: 55
|
|
Expected Memory: 1369.0MB
|
|
Grounding... [('step', [56]), ('step', [57]), ('step', [58]), ('step', [59]), ('step', [60]), ('check', [60])]
|
|
Grounding Time: 2.65s
|
|
Memory: 1322MB (+78MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 19
|
|
Time : 467.972s (Solving: 429.25s 1st Model: 10.83s Unsat: 6.75s)
|
|
CPU Time : 467.712s
|
|
|
|
Choices : 13335550 (Domain: 13335514)
|
|
Conflicts : 170442 (Analyzed: 170441)
|
|
Restarts : 1676 (Average: 101.70 Last: 170)
|
|
Model-Level : 2556.0
|
|
Problems : 19 (Average Length: 31.74 Splits: 0)
|
|
Lemmas : 170441 (Deleted: 152211)
|
|
Binary : 1483 (Ratio: 0.87%)
|
|
Ternary : 1205 (Ratio: 0.71%)
|
|
Conflict : 170441 (Average Length: 1175.0 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 170441 (Average: 71.74 Max: 5071 Sum: 12227141)
|
|
Executed : 170117 (Average: 71.68 Max: 5071 Sum: 12217102 Ratio: 99.92%)
|
|
Bounded : 324 (Average: 30.98 Max: 62 Sum: 10039 Ratio: 0.08%)
|
|
|
|
Rules : 1053757 (Original: 1053711)
|
|
Atoms : 263807
|
|
Bodies : 531222 (Original: 531175)
|
|
Count : 1005 (Original: 1013)
|
|
Equivalences : 269260 (Atom=Atom: 36 Body=Body: 0 Other: 269224)
|
|
Tight : Yes
|
|
Variables : 896775 (Eliminated: 0 Frozen: 786247)
|
|
Constraints : 8590578 (Binary: 98.5% Ternary: 0.7% Other: 0.8%)
|
|
|
|
Memory Peak : 1471MB
|
|
Max. Length : 55 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 44.89s
|
|
Memory: 1371MB (+49MB)
|
|
UNKNOWN
|
|
Iteration Time: 48.54s
|
|
|
|
Iteration 19
|
|
Queue: [(13,65,0,True), (14,70,0,True), (15,75,0,True)]
|
|
Grounded Until: 60
|
|
Expected Memory: 1498.0MB
|
|
Grounding... [('step', [61]), ('step', [62]), ('step', [63]), ('step', [64]), ('step', [65]), ('check', [65])]
|
|
Grounding Time: 1.93s
|
|
Memory: 1402MB (+31MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 20
|
|
Time : 525.357s (Solving: 483.47s 1st Model: 10.83s Unsat: 6.75s)
|
|
CPU Time : 525.120s
|
|
|
|
Choices : 14842556 (Domain: 14842520)
|
|
Conflicts : 180796 (Analyzed: 180795)
|
|
Restarts : 1776 (Average: 101.80 Last: 170)
|
|
Model-Level : 2556.0
|
|
Problems : 20 (Average Length: 33.50 Splits: 0)
|
|
Lemmas : 180795 (Deleted: 162491)
|
|
Binary : 1511 (Ratio: 0.84%)
|
|
Ternary : 1225 (Ratio: 0.68%)
|
|
Conflict : 180795 (Average Length: 1241.4 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 180795 (Average: 75.19 Max: 5071 Sum: 13593234)
|
|
Executed : 180465 (Average: 75.13 Max: 5071 Sum: 13582793 Ratio: 99.92%)
|
|
Bounded : 330 (Average: 31.64 Max: 67 Sum: 10441 Ratio: 0.08%)
|
|
|
|
Rules : 1053757 (Original: 1053711)
|
|
Atoms : 263807
|
|
Bodies : 531222 (Original: 531175)
|
|
Count : 1005 (Original: 1013)
|
|
Equivalences : 269260 (Atom=Atom: 36 Body=Body: 0 Other: 269224)
|
|
Tight : Yes
|
|
Variables : 972891 (Eliminated: 0 Frozen: 856547)
|
|
Constraints : 9371646 (Binary: 98.5% Ternary: 0.7% Other: 0.8%)
|
|
|
|
Memory Peak : 1544MB
|
|
Max. Length : 60 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 54.44s
|
|
Memory: 1443MB (+41MB)
|
|
UNKNOWN
|
|
Iteration Time: 57.42s
|
|
|
|
Iteration 20
|
|
Queue: [(14,70,0,True), (15,75,0,True)]
|
|
Grounded Until: 65
|
|
Expected Memory: 1570.0MB
|
|
Grounding... [('step', [66]), ('step', [67]), ('step', [68]), ('step', [69]), ('step', [70]), ('check', [70])]
|
|
Grounding Time: 1.92s
|
|
Memory: 1468MB (+25MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 21
|
|
Time : 571.418s (Solving: 526.33s 1st Model: 10.83s Unsat: 6.75s)
|
|
CPU Time : 571.200s
|
|
|
|
Choices : 16032472 (Domain: 16032436)
|
|
Conflicts : 190440 (Analyzed: 190439)
|
|
Restarts : 1876 (Average: 101.51 Last: 170)
|
|
Model-Level : 2556.0
|
|
Problems : 21 (Average Length: 35.33 Splits: 0)
|
|
Lemmas : 190439 (Deleted: 172971)
|
|
Binary : 1532 (Ratio: 0.80%)
|
|
Ternary : 1240 (Ratio: 0.65%)
|
|
Conflict : 190439 (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 : 190439 (Average: 76.67 Max: 5071 Sum: 14601042)
|
|
Executed : 190109 (Average: 76.62 Max: 5071 Sum: 14590601 Ratio: 99.93%)
|
|
Bounded : 330 (Average: 31.64 Max: 67 Sum: 10441 Ratio: 0.07%)
|
|
|
|
Rules : 1053757 (Original: 1053711)
|
|
Atoms : 263807
|
|
Bodies : 531222 (Original: 531175)
|
|
Count : 1005 (Original: 1013)
|
|
Equivalences : 269260 (Atom=Atom: 36 Body=Body: 0 Other: 269224)
|
|
Tight : Yes
|
|
Variables : 1049007 (Eliminated: 0 Frozen: 926847)
|
|
Constraints : 10152279 (Binary: 98.5% Ternary: 0.7% Other: 0.8%)
|
|
|
|
Memory Peak : 1631MB
|
|
Max. Length : 65 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 43.10s
|
|
Memory: 1531MB (+63MB)
|
|
UNKNOWN
|
|
Iteration Time: 46.09s
|
|
|
|
Iteration 21
|
|
Queue: [(15,75,0,True)]
|
|
Grounded Until: 70
|
|
Expected Memory: 1658.0MB
|
|
Grounding... [('step', [71]), ('step', [72]), ('step', [73]), ('step', [74]), ('step', [75]), ('check', [75])]
|
|
Grounding Time: 1.93s
|
|
Memory: 1536MB (+5MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 22
|
|
Time : 675.621s (Solving: 627.25s 1st Model: 10.83s Unsat: 6.75s)
|
|
CPU Time : 675.444s
|
|
|
|
Choices : 17932130 (Domain: 17932094)
|
|
Conflicts : 200799 (Analyzed: 200798)
|
|
Restarts : 1976 (Average: 101.62 Last: 170)
|
|
Model-Level : 2556.0
|
|
Problems : 22 (Average Length: 37.23 Splits: 0)
|
|
Lemmas : 200798 (Deleted: 182387)
|
|
Binary : 1541 (Ratio: 0.77%)
|
|
Ternary : 1254 (Ratio: 0.62%)
|
|
Conflict : 200798 (Average Length: 1355.0 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 200798 (Average: 81.66 Max: 5071 Sum: 16397963)
|
|
Executed : 200466 (Average: 81.61 Max: 5071 Sum: 16387368 Ratio: 99.94%)
|
|
Bounded : 332 (Average: 31.91 Max: 77 Sum: 10595 Ratio: 0.06%)
|
|
|
|
Rules : 1053757 (Original: 1053711)
|
|
Atoms : 263807
|
|
Bodies : 531222 (Original: 531175)
|
|
Count : 1005 (Original: 1013)
|
|
Equivalences : 269260 (Atom=Atom: 36 Body=Body: 0 Other: 269224)
|
|
Tight : Yes
|
|
Variables : 1125123 (Eliminated: 0 Frozen: 997147)
|
|
Constraints : 10933419 (Binary: 98.5% Ternary: 0.7% Other: 0.8%)
|
|
|
|
Memory Peak : 1698MB
|
|
Max. Length : 70 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 101.19s
|
|
Memory: 1639MB (+103MB)
|
|
UNKNOWN
|
|
Iteration Time: 104.25s
|
|
|
|
Iteration 22
|
|
Queue: [(3,15,2,True), (4,20,2,True), (5,25,2,True), (6,30,2,True), (7,35,1,True), (8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,0,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True)]
|
|
Grounded Until: 75
|
|
Blocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 23
|
|
Time : 687.310s (Solving: 638.66s 1st Model: 10.83s Unsat: 6.75s)
|
|
CPU Time : 687.140s
|
|
|
|
Choices : 17975585 (Domain: 17975549)
|
|
Conflicts : 210000 (Analyzed: 209999)
|
|
Restarts : 2076 (Average: 101.16 Last: 170)
|
|
Model-Level : 2556.0
|
|
Problems : 23 (Average Length: 38.96 Splits: 0)
|
|
Lemmas : 209999 (Deleted: 192770)
|
|
Binary : 1573 (Ratio: 0.75%)
|
|
Ternary : 1290 (Ratio: 0.61%)
|
|
Conflict : 209999 (Average Length: 1363.4 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 209999 (Average: 78.25 Max: 5071 Sum: 16431732)
|
|
Executed : 209666 (Average: 78.20 Max: 5071 Sum: 16421060 Ratio: 99.94%)
|
|
Bounded : 333 (Average: 32.05 Max: 77 Sum: 10672 Ratio: 0.06%)
|
|
|
|
Rules : 1053757 (Original: 1053711)
|
|
Atoms : 263807
|
|
Bodies : 531222 (Original: 531175)
|
|
Count : 1005 (Original: 1013)
|
|
Equivalences : 269260 (Atom=Atom: 36 Body=Body: 0 Other: 269224)
|
|
Tight : Yes
|
|
Variables : 1125123 (Eliminated: 0 Frozen: 997147)
|
|
Constraints : 10933395 (Binary: 98.5% Ternary: 0.7% Other: 0.8%)
|
|
|
|
Memory Peak : 1698MB
|
|
Max. Length : 75 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 11.60s
|
|
Memory: 1650MB (+11MB)
|
|
UNKNOWN
|
|
Iteration Time: 11.70s
|
|
|
|
Iteration 23
|
|
Queue: [(4,20,2,True), (5,25,2,True), (6,30,2,True), (7,35,1,True), (8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,0,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True)]
|
|
Grounded Until: 75
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 24
|
|
Time : 707.066s (Solving: 658.13s 1st Model: 10.83s Unsat: 6.75s)
|
|
CPU Time : 706.904s
|
|
|
|
Choices : 18183796 (Domain: 18183760)
|
|
Conflicts : 220591 (Analyzed: 220590)
|
|
Restarts : 2176 (Average: 101.37 Last: 170)
|
|
Model-Level : 2556.0
|
|
Problems : 24 (Average Length: 40.54 Splits: 0)
|
|
Lemmas : 220590 (Deleted: 201593)
|
|
Binary : 1611 (Ratio: 0.73%)
|
|
Ternary : 1330 (Ratio: 0.60%)
|
|
Conflict : 220590 (Average Length: 1423.2 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 220590 (Average: 75.32 Max: 5071 Sum: 16614543)
|
|
Executed : 220256 (Average: 75.27 Max: 5071 Sum: 16603794 Ratio: 99.94%)
|
|
Bounded : 334 (Average: 32.18 Max: 77 Sum: 10749 Ratio: 0.06%)
|
|
|
|
Rules : 1053757 (Original: 1053711)
|
|
Atoms : 263807
|
|
Bodies : 531222 (Original: 531175)
|
|
Count : 1005 (Original: 1013)
|
|
Equivalences : 269260 (Atom=Atom: 36 Body=Body: 0 Other: 269224)
|
|
Tight : Yes
|
|
Variables : 1125123 (Eliminated: 0 Frozen: 997147)
|
|
Constraints : 10933383 (Binary: 98.5% Ternary: 0.7% Other: 0.8%)
|
|
|
|
Memory Peak : 1698MB
|
|
Max. Length : 75 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 19.66s
|
|
Memory: 1650MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 19.77s
|
|
|
|
Iteration 24
|
|
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,0,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True)]
|
|
Grounded Until: 75
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 25
|
|
Time : 734.565s (Solving: 685.31s 1st Model: 10.83s Unsat: 6.75s)
|
|
CPU Time : 734.416s
|
|
|
|
Choices : 18936641 (Domain: 18936605)
|
|
Conflicts : 231055 (Analyzed: 231054)
|
|
Restarts : 2276 (Average: 101.52 Last: 170)
|
|
Model-Level : 2556.0
|
|
Problems : 25 (Average Length: 42.00 Splits: 0)
|
|
Lemmas : 231054 (Deleted: 209391)
|
|
Binary : 1664 (Ratio: 0.72%)
|
|
Ternary : 1378 (Ratio: 0.60%)
|
|
Conflict : 231054 (Average Length: 1402.7 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 231054 (Average: 74.93 Max: 5071 Sum: 17313587)
|
|
Executed : 230713 (Average: 74.88 Max: 5071 Sum: 17302299 Ratio: 99.93%)
|
|
Bounded : 341 (Average: 33.10 Max: 77 Sum: 11288 Ratio: 0.07%)
|
|
|
|
Rules : 1053757 (Original: 1053711)
|
|
Atoms : 263807
|
|
Bodies : 531222 (Original: 531175)
|
|
Count : 1005 (Original: 1013)
|
|
Equivalences : 269260 (Atom=Atom: 36 Body=Body: 0 Other: 269224)
|
|
Tight : Yes
|
|
Variables : 1125123 (Eliminated: 0 Frozen: 997147)
|
|
Constraints : 10933371 (Binary: 98.5% Ternary: 0.7% Other: 0.8%)
|
|
|
|
Memory Peak : 1698MB
|
|
Max. Length : 75 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 27.38s
|
|
Memory: 1650MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 27.51s
|
|
|
|
Iteration 25
|
|
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,0,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True)]
|
|
Grounded Until: 75
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 26
|
|
Time : 773.802s (Solving: 724.25s 1st Model: 10.83s Unsat: 6.75s)
|
|
CPU Time : 773.668s
|
|
|
|
Choices : 19923804 (Domain: 19923768)
|
|
Conflicts : 241680 (Analyzed: 241679)
|
|
Restarts : 2376 (Average: 101.72 Last: 170)
|
|
Model-Level : 2556.0
|
|
Problems : 26 (Average Length: 43.35 Splits: 0)
|
|
Lemmas : 241679 (Deleted: 219076)
|
|
Binary : 1785 (Ratio: 0.74%)
|
|
Ternary : 1441 (Ratio: 0.60%)
|
|
Conflict : 241679 (Average Length: 1392.7 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 241679 (Average: 75.49 Max: 5071 Sum: 18243708)
|
|
Executed : 241326 (Average: 75.44 Max: 5071 Sum: 18231496 Ratio: 99.93%)
|
|
Bounded : 353 (Average: 34.59 Max: 77 Sum: 12212 Ratio: 0.07%)
|
|
|
|
Rules : 1053757 (Original: 1053711)
|
|
Atoms : 263807
|
|
Bodies : 531222 (Original: 531175)
|
|
Count : 1005 (Original: 1013)
|
|
Equivalences : 269260 (Atom=Atom: 36 Body=Body: 0 Other: 269224)
|
|
Tight : Yes
|
|
Variables : 1125123 (Eliminated: 0 Frozen: 997147)
|
|
Constraints : 10933289 (Binary: 98.5% Ternary: 0.7% Other: 0.8%)
|
|
|
|
Memory Peak : 1698MB
|
|
Max. Length : 75 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 39.14s
|
|
Memory: 1650MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 39.26s
|
|
|
|
Iteration 26
|
|
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,0,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True)]
|
|
Grounded Until: 75
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 27
|
|
Time : 810.279s (Solving: 760.41s 1st Model: 10.83s Unsat: 6.75s)
|
|
CPU Time : 810.164s
|
|
|
|
Choices : 20816028 (Domain: 20815992)
|
|
Conflicts : 251696 (Analyzed: 251695)
|
|
Restarts : 2476 (Average: 101.65 Last: 170)
|
|
Model-Level : 2556.0
|
|
Problems : 27 (Average Length: 44.59 Splits: 0)
|
|
Lemmas : 251695 (Deleted: 228996)
|
|
Binary : 1832 (Ratio: 0.73%)
|
|
Ternary : 1472 (Ratio: 0.58%)
|
|
Conflict : 251695 (Average Length: 1408.5 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 251695 (Average: 75.75 Max: 5071 Sum: 19066434)
|
|
Executed : 251341 (Average: 75.70 Max: 5071 Sum: 19054145 Ratio: 99.94%)
|
|
Bounded : 354 (Average: 34.71 Max: 77 Sum: 12289 Ratio: 0.06%)
|
|
|
|
Rules : 1053757 (Original: 1053711)
|
|
Atoms : 263807
|
|
Bodies : 531222 (Original: 531175)
|
|
Count : 1005 (Original: 1013)
|
|
Equivalences : 269260 (Atom=Atom: 36 Body=Body: 0 Other: 269224)
|
|
Tight : Yes
|
|
Variables : 1125123 (Eliminated: 0 Frozen: 997147)
|
|
Constraints : 10932334 (Binary: 98.5% Ternary: 0.7% Other: 0.8%)
|
|
|
|
Memory Peak : 1698MB
|
|
Max. Length : 75 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 36.36s
|
|
Memory: 1650MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 36.50s
|
|
|
|
Iteration 27
|
|
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,0,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True)]
|
|
Grounded Until: 75
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 28
|
|
Time : 868.732s (Solving: 818.56s 1st Model: 10.83s Unsat: 6.75s)
|
|
CPU Time : 868.644s
|
|
|
|
Choices : 21903744 (Domain: 21903708)
|
|
Conflicts : 261870 (Analyzed: 261869)
|
|
Restarts : 2576 (Average: 101.66 Last: 170)
|
|
Model-Level : 2556.0
|
|
Problems : 28 (Average Length: 45.75 Splits: 0)
|
|
Lemmas : 261869 (Deleted: 238219)
|
|
Binary : 1883 (Ratio: 0.72%)
|
|
Ternary : 1494 (Ratio: 0.57%)
|
|
Conflict : 261869 (Average Length: 1409.0 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 261869 (Average: 76.70 Max: 5071 Sum: 20085513)
|
|
Executed : 261512 (Average: 76.65 Max: 5071 Sum: 20072993 Ratio: 99.94%)
|
|
Bounded : 357 (Average: 35.07 Max: 77 Sum: 12520 Ratio: 0.06%)
|
|
|
|
Rules : 1053757 (Original: 1053711)
|
|
Atoms : 263807
|
|
Bodies : 531222 (Original: 531175)
|
|
Count : 1005 (Original: 1013)
|
|
Equivalences : 269260 (Atom=Atom: 36 Body=Body: 0 Other: 269224)
|
|
Tight : Yes
|
|
Variables : 1125123 (Eliminated: 0 Frozen: 997147)
|
|
Constraints : 10932284 (Binary: 98.5% Ternary: 0.7% Other: 0.8%)
|
|
|
|
Memory Peak : 1698MB
|
|
Max. Length : 75 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 58.36s
|
|
Memory: 1650MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 58.48s
|
|
|
|
Iteration 28
|
|
Queue: [(9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,0,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True)]
|
|
Grounded Until: 75
|
|
Unblocking actions...
|
|
Solving...
|
|
*** Info : (planner): INTERRUPTED by signal!
|
|
UNKNOWN
|
|
|
|
INTERRUPTED : 1
|
|
|
|
Models : 0+
|
|
Calls : 29
|
|
Time : 879.617s (Solving: 829.17s 1st Model: 10.83s Unsat: 6.75s)
|
|
CPU Time : 879.516s
|
|
|
|
Choices : 22144188 (Domain: 22144152)
|
|
Conflicts : 263533 (Analyzed: 263532)
|
|
Restarts : 2590 (Average: 101.75 Last: 170)
|
|
Model-Level : 2556.0
|
|
Problems : 29 (Average Length: 46.83 Splits: 0)
|
|
Lemmas : 263532 (Deleted: 238219)
|
|
Binary : 1902 (Ratio: 0.72%)
|
|
Ternary : 1504 (Ratio: 0.57%)
|
|
Conflict : 263532 (Average Length: 1404.9 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 263532 (Average: 77.10 Max: 5071 Sum: 20317886)
|
|
Executed : 263174 (Average: 77.05 Max: 5071 Sum: 20305289 Ratio: 99.94%)
|
|
Bounded : 358 (Average: 35.19 Max: 77 Sum: 12597 Ratio: 0.06%)
|
|
|
|
Rules : 1053757 (Original: 1053711)
|
|
Atoms : 263807
|
|
Bodies : 531222 (Original: 531175)
|
|
Count : 1005 (Original: 1013)
|
|
Equivalences : 269260 (Atom=Atom: 36 Body=Body: 0 Other: 269224)
|
|
Tight : Yes
|
|
Variables : 1125123 (Eliminated: 0 Frozen: 997147)
|
|
Constraints : 10932250 (Binary: 98.5% Ternary: 0.7% Other: 0.8%)
|
|
|
|
Memory Peak : 1698MB
|
|
Max. Length : 75 steps
|
|
Models : 1
|
|
|
|
|