1234 lines
42 KiB
Plaintext
1234 lines
42 KiB
Plaintext
INFO Running translator.
|
|
INFO translator input: ['/home/pluehne/Documents/ASP/pddl-instances/ipc-2000/domains/blocks-strips-typed/domain.pddl', '/home/pluehne/Documents/ASP/pddl-instances/ipc-2000/domains/blocks-strips-typed/instances/instance-81.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-2000/domains/blocks-strips-typed/domain.pddl /home/pluehne/Documents/ASP/pddl-instances/ipc-2000/domains/blocks-strips-typed/instances/instance-81.pddl
|
|
Parsing...
|
|
Parsing: [0.020s CPU, 0.020s wall-clock]
|
|
Normalizing task... [0.000s CPU, 0.002s wall-clock]
|
|
Instantiating...
|
|
Generating Datalog program... [0.010s CPU, 0.007s wall-clock]
|
|
Normalizing Datalog program...
|
|
Normalizing Datalog program: [0.000s CPU, 0.011s wall-clock]
|
|
Preparing model... [0.020s CPU, 0.016s wall-clock]
|
|
Generated 21 rules.
|
|
Computing model... [0.610s CPU, 0.606s wall-clock]
|
|
5122 relevant atoms
|
|
3400 auxiliary atoms
|
|
8522 final queue length
|
|
15008 total queue pushes
|
|
Completing instantiation... [1.080s CPU, 1.081s wall-clock]
|
|
Instantiating: [1.730s CPU, 1.729s wall-clock]
|
|
Computing fact groups...
|
|
Finding invariants...
|
|
10 initial candidates
|
|
Finding invariants: [0.020s CPU, 0.027s wall-clock]
|
|
Checking invariant weight... [0.010s CPU, 0.006s wall-clock]
|
|
Instantiating groups... [0.060s CPU, 0.059s wall-clock]
|
|
Collecting mutex groups... [0.010s CPU, 0.013s wall-clock]
|
|
Choosing groups...
|
|
41 uncovered facts
|
|
Choosing groups: [0.070s CPU, 0.071s wall-clock]
|
|
Building translation key... [0.020s CPU, 0.021s wall-clock]
|
|
Computing fact groups: [0.350s CPU, 0.356s wall-clock]
|
|
Building STRIPS to SAS dictionary... [0.010s CPU, 0.010s wall-clock]
|
|
Building dictionary for full mutex groups... [0.030s CPU, 0.025s wall-clock]
|
|
Building mutex information...
|
|
Building mutex information: [0.030s CPU, 0.037s wall-clock]
|
|
Translating task...
|
|
Processing axioms...
|
|
Simplifying axioms... [0.000s CPU, 0.000s wall-clock]
|
|
Processing axioms: [0.060s CPU, 0.053s wall-clock]
|
|
Translating task: [1.330s CPU, 1.320s wall-clock]
|
|
4760 effect conditions simplified
|
|
0 implied preconditions added
|
|
Detecting unreachable propositions...
|
|
0 operators removed
|
|
0 axioms removed
|
|
80 propositions removed
|
|
Detecting unreachable propositions: [0.690s CPU, 0.685s wall-clock]
|
|
Reordering and filtering variables...
|
|
81 of 81 variables necessary.
|
|
41 of 81 mutex groups necessary.
|
|
3200 of 3200 operators necessary.
|
|
0 of 0 axiom rules necessary.
|
|
Reordering and filtering variables: [0.390s CPU, 0.395s wall-clock]
|
|
Translator variables: 81
|
|
Translator derived variables: 0
|
|
Translator facts: 1722
|
|
Translator goal facts: 39
|
|
Translator mutex groups: 41
|
|
Translator total mutex groups size: 1681
|
|
Translator operators: 3200
|
|
Translator axioms: 0
|
|
Translator task size: 27403
|
|
Translator peak memory: 52684 KB
|
|
Writing output... [0.460s CPU, 0.489s wall-clock]
|
|
Done! [5.100s CPU, 5.125s wall-clock]
|
|
planner.py version 0.0.1
|
|
|
|
Time: 0.93s
|
|
Memory: 107MB
|
|
|
|
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 : 1.055s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
|
|
CPU Time : 0.932s
|
|
|
|
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 : 83982
|
|
Atoms : 83982
|
|
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 : 243MB
|
|
Max. Length : 0 steps
|
|
Models : 0
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 0.01s
|
|
Memory: 179MB (+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: 179MB
|
|
Grounding... [('step', [1]), ('step', [2]), ('step', [3]), ('step', [4]), ('step', [5]), ('check', [5])]
|
|
Grounding Time: 0.42s
|
|
Memory: 189MB (+10MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0
|
|
Calls : 2
|
|
Time : 1.886s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
|
|
CPU Time : 1.764s
|
|
|
|
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 : 83982
|
|
Atoms : 83982
|
|
Bodies : 1 (Original: 0)
|
|
Tight : Yes
|
|
Variables : 22255 (Eliminated: 0 Frozen: 22255)
|
|
Constraints : 8959 (Binary: 92.7% Ternary: 4.4% Other: 2.9%)
|
|
|
|
Memory Peak : 243MB
|
|
Max. Length : 0 steps
|
|
Models : 0
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 0.26s
|
|
Memory: 196MB (+7MB)
|
|
UNSAT
|
|
Iteration Time: 0.84s
|
|
|
|
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: 213.0MB
|
|
Grounding... [('step', [6]), ('step', [7]), ('step', [8]), ('step', [9]), ('step', [10]), ('check', [10])]
|
|
Grounding Time: 0.41s
|
|
Memory: 210MB (+14MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0
|
|
Calls : 3
|
|
Time : 2.772s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
|
|
CPU Time : 2.652s
|
|
|
|
Choices : 0
|
|
Conflicts : 0 (Analyzed: 0)
|
|
Restarts : 0
|
|
Problems : 3 (Average Length: 7.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 : 83982
|
|
Atoms : 83982
|
|
Bodies : 1 (Original: 0)
|
|
Tight : Yes
|
|
Variables : 44962 (Eliminated: 0 Frozen: 44962)
|
|
Constraints : 45102 (Binary: 93.8% Ternary: 4.4% Other: 1.8%)
|
|
|
|
Memory Peak : 243MB
|
|
Max. Length : 5 steps
|
|
Models : 0
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 0.29s
|
|
Memory: 219MB (+9MB)
|
|
UNSAT
|
|
Iteration Time: 0.89s
|
|
|
|
Iteration 4
|
|
Queue: [(3,15,0,True), (4,20,0,True), (5,25,0,True), (6,30,0,True)]
|
|
Grounded Until: 10
|
|
Expected Memory: 242.0MB
|
|
Grounding... [('step', [11]), ('step', [12]), ('step', [13]), ('step', [14]), ('step', [15]), ('check', [15])]
|
|
Grounding Time: 0.51s
|
|
Memory: 235MB (+16MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0
|
|
Calls : 4
|
|
Time : 3.828s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
|
|
CPU Time : 3.708s
|
|
|
|
Choices : 0
|
|
Conflicts : 0 (Analyzed: 0)
|
|
Restarts : 0
|
|
Problems : 4 (Average Length: 9.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 : 83982
|
|
Atoms : 83982
|
|
Bodies : 1 (Original: 0)
|
|
Tight : Yes
|
|
Variables : 68103 (Eliminated: 0 Frozen: 68103)
|
|
Constraints : 106654 (Binary: 94.2% Ternary: 4.4% Other: 1.4%)
|
|
|
|
Memory Peak : 247MB
|
|
Max. Length : 10 steps
|
|
Models : 0
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 0.34s
|
|
Memory: 247MB (+12MB)
|
|
UNSAT
|
|
Iteration Time: 1.06s
|
|
|
|
Iteration 5
|
|
Queue: [(4,20,0,True), (5,25,0,True), (6,30,0,True)]
|
|
Grounded Until: 15
|
|
Expected Memory: 275.0MB
|
|
Grounding... [('step', [16]), ('step', [17]), ('step', [18]), ('step', [19]), ('step', [20]), ('check', [20])]
|
|
Grounding Time: 0.44s
|
|
Memory: 257MB (+10MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0
|
|
Calls : 5
|
|
Time : 4.905s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
|
|
CPU Time : 4.784s
|
|
|
|
Choices : 0
|
|
Conflicts : 0 (Analyzed: 0)
|
|
Restarts : 0
|
|
Problems : 5 (Average Length: 12.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 : 83982
|
|
Atoms : 83982
|
|
Bodies : 1 (Original: 0)
|
|
Tight : Yes
|
|
Variables : 91719 (Eliminated: 0 Frozen: 91719)
|
|
Constraints : 198956 (Binary: 94.5% Ternary: 4.3% Other: 1.2%)
|
|
|
|
Memory Peak : 271MB
|
|
Max. Length : 15 steps
|
|
Models : 0
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 0.40s
|
|
Memory: 271MB (+14MB)
|
|
UNSAT
|
|
Iteration Time: 1.08s
|
|
|
|
Iteration 6
|
|
Queue: [(5,25,0,True), (6,30,0,True)]
|
|
Grounded Until: 20
|
|
Expected Memory: 299.0MB
|
|
Grounding... [('step', [21]), ('step', [22]), ('step', [23]), ('step', [24]), ('step', [25]), ('check', [25])]
|
|
Grounding Time: 0.46s
|
|
Memory: 280MB (+9MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0
|
|
Calls : 6
|
|
Time : 6.114s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
|
|
CPU Time : 5.992s
|
|
|
|
Choices : 0
|
|
Conflicts : 0 (Analyzed: 0)
|
|
Restarts : 0
|
|
Problems : 6 (Average Length: 14.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 : 83982
|
|
Atoms : 83982
|
|
Bodies : 1 (Original: 0)
|
|
Tight : Yes
|
|
Variables : 115910 (Eliminated: 0 Frozen: 115910)
|
|
Constraints : 328258 (Binary: 94.7% Ternary: 4.3% Other: 1.0%)
|
|
|
|
Memory Peak : 301MB
|
|
Max. Length : 20 steps
|
|
Models : 0
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 0.50s
|
|
Memory: 301MB (+21MB)
|
|
UNSAT
|
|
Iteration Time: 1.22s
|
|
|
|
Iteration 7
|
|
Queue: [(6,30,0,True)]
|
|
Grounded Until: 25
|
|
Expected Memory: 331.0MB
|
|
Grounding... [('step', [26]), ('step', [27]), ('step', [28]), ('step', [29]), ('step', [30]), ('check', [30])]
|
|
Grounding Time: 0.63s
|
|
Memory: 318MB (+17MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0
|
|
Calls : 7
|
|
Time : 7.647s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
|
|
CPU Time : 7.528s
|
|
|
|
Choices : 0
|
|
Conflicts : 0 (Analyzed: 0)
|
|
Restarts : 0
|
|
Problems : 7 (Average Length: 17.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 : 83982
|
|
Atoms : 83982
|
|
Bodies : 1 (Original: 0)
|
|
Tight : Yes
|
|
Variables : 140776 (Eliminated: 0 Frozen: 140776)
|
|
Constraints : 500803 (Binary: 94.8% Ternary: 4.3% Other: 0.9%)
|
|
|
|
Memory Peak : 339MB
|
|
Max. Length : 25 steps
|
|
Models : 0
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 0.64s
|
|
Memory: 329MB (+11MB)
|
|
UNSAT
|
|
Iteration Time: 1.54s
|
|
|
|
Iteration 8
|
|
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)]
|
|
Grounded Until: 30
|
|
Expected Memory: 359.0MB
|
|
Grounding... [('step', [31]), ('step', [32]), ('step', [33]), ('step', [34]), ('step', [35]), ('check', [35])]
|
|
Grounding Time: 0.45s
|
|
Memory: 339MB (+10MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0
|
|
Calls : 8
|
|
Time : 9.072s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
|
|
CPU Time : 8.952s
|
|
|
|
Choices : 0
|
|
Conflicts : 1 (Analyzed: 0)
|
|
Restarts : 0
|
|
Problems : 8 (Average Length: 19.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 : 83982
|
|
Atoms : 83982
|
|
Bodies : 1 (Original: 0)
|
|
Tight : Yes
|
|
Variables : 166372 (Eliminated: 0 Frozen: 166372)
|
|
Constraints : 701578 (Binary: 94.9% Ternary: 4.3% Other: 0.8%)
|
|
|
|
Memory Peak : 366MB
|
|
Max. Length : 30 steps
|
|
Models : 0
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 0.76s
|
|
Memory: 354MB (+15MB)
|
|
UNSAT
|
|
Iteration Time: 1.43s
|
|
|
|
Iteration 9
|
|
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)]
|
|
Grounded Until: 35
|
|
Expected Memory: 384.0MB
|
|
Grounding... [('step', [36]), ('step', [37]), ('step', [38]), ('step', [39]), ('step', [40]), ('check', [40])]
|
|
Grounding Time: 0.45s
|
|
Memory: 364MB (+10MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0
|
|
Calls : 9
|
|
Time : 10.526s (Solving: 0.01s 1st Model: 0.00s Unsat: 0.01s)
|
|
CPU Time : 10.408s
|
|
|
|
Choices : 0
|
|
Conflicts : 2 (Analyzed: 0)
|
|
Restarts : 0
|
|
Problems : 9 (Average Length: 22.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 : 83982
|
|
Atoms : 83982
|
|
Bodies : 1 (Original: 0)
|
|
Tight : Yes
|
|
Variables : 192008 (Eliminated: 0 Frozen: 192008)
|
|
Constraints : 902823 (Binary: 95.0% Ternary: 4.3% Other: 0.8%)
|
|
|
|
Memory Peak : 392MB
|
|
Max. Length : 35 steps
|
|
Models : 0
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 0.77s
|
|
Memory: 388MB (+24MB)
|
|
UNSAT
|
|
Iteration Time: 1.46s
|
|
|
|
Iteration 10
|
|
Queue: [(9,45,0,True), (10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True)]
|
|
Grounded Until: 40
|
|
Expected Memory: 422.0MB
|
|
Grounding... [('step', [41]), ('step', [42]), ('step', [43]), ('step', [44]), ('step', [45]), ('check', [45])]
|
|
Grounding Time: 0.46s
|
|
Memory: 396MB (+8MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0
|
|
Calls : 10
|
|
Time : 12.010s (Solving: 0.03s 1st Model: 0.00s Unsat: 0.03s)
|
|
CPU Time : 11.892s
|
|
|
|
Choices : 0
|
|
Conflicts : 3 (Analyzed: 0)
|
|
Restarts : 0
|
|
Problems : 10 (Average Length: 24.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 : 83982
|
|
Atoms : 83982
|
|
Bodies : 1 (Original: 0)
|
|
Tight : Yes
|
|
Variables : 217644 (Eliminated: 0 Frozen: 217644)
|
|
Constraints : 1104068 (Binary: 95.0% Ternary: 4.3% Other: 0.7%)
|
|
|
|
Memory Peak : 427MB
|
|
Max. Length : 40 steps
|
|
Models : 0
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 0.78s
|
|
Memory: 410MB (+14MB)
|
|
UNSAT
|
|
Iteration Time: 1.49s
|
|
|
|
Iteration 11
|
|
Queue: [(10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True)]
|
|
Grounded Until: 45
|
|
Expected Memory: 444.0MB
|
|
Grounding... [('step', [46]), ('step', [47]), ('step', [48]), ('step', [49]), ('step', [50]), ('check', [50])]
|
|
Grounding Time: 0.47s
|
|
Memory: 418MB (+8MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0
|
|
Calls : 11
|
|
Time : 13.514s (Solving: 0.04s 1st Model: 0.00s Unsat: 0.04s)
|
|
CPU Time : 13.396s
|
|
|
|
Choices : 0
|
|
Conflicts : 4 (Analyzed: 0)
|
|
Restarts : 0
|
|
Problems : 11 (Average Length: 27.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 : 83982
|
|
Atoms : 83982
|
|
Bodies : 1 (Original: 0)
|
|
Tight : Yes
|
|
Variables : 243280 (Eliminated: 0 Frozen: 243280)
|
|
Constraints : 1305313 (Binary: 95.0% Ternary: 4.3% Other: 0.7%)
|
|
|
|
Memory Peak : 456MB
|
|
Max. Length : 45 steps
|
|
Models : 0
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 0.79s
|
|
Memory: 436MB (+18MB)
|
|
UNSAT
|
|
Iteration Time: 1.51s
|
|
|
|
Iteration 12
|
|
Queue: [(11,55,0,True), (12,60,0,True), (13,65,0,True)]
|
|
Grounded Until: 50
|
|
Expected Memory: 470.0MB
|
|
Grounding... [('step', [51]), ('step', [52]), ('step', [53]), ('step', [54]), ('step', [55]), ('check', [55])]
|
|
Grounding Time: 0.47s
|
|
Memory: 441MB (+5MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0
|
|
Calls : 12
|
|
Time : 15.048s (Solving: 0.07s 1st Model: 0.00s Unsat: 0.07s)
|
|
CPU Time : 14.932s
|
|
|
|
Choices : 0
|
|
Conflicts : 5 (Analyzed: 0)
|
|
Restarts : 0
|
|
Problems : 12 (Average Length: 29.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 : 83982
|
|
Atoms : 83982
|
|
Bodies : 1 (Original: 0)
|
|
Tight : Yes
|
|
Variables : 268916 (Eliminated: 0 Frozen: 268916)
|
|
Constraints : 1506558 (Binary: 95.0% Ternary: 4.3% Other: 0.7%)
|
|
|
|
Memory Peak : 479MB
|
|
Max. Length : 50 steps
|
|
Models : 0
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 0.80s
|
|
Memory: 474MB (+33MB)
|
|
UNSAT
|
|
Iteration Time: 1.55s
|
|
|
|
Iteration 13
|
|
Queue: [(12,60,0,True), (13,65,0,True)]
|
|
Grounded Until: 55
|
|
Expected Memory: 512.0MB
|
|
Grounding... [('step', [56]), ('step', [57]), ('step', [58]), ('step', [59]), ('step', [60]), ('check', [60])]
|
|
Grounding Time: 0.49s
|
|
Memory: 474MB (+0MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0
|
|
Calls : 13
|
|
Time : 16.634s (Solving: 0.10s 1st Model: 0.00s Unsat: 0.10s)
|
|
CPU Time : 16.520s
|
|
|
|
Choices : 23 (Domain: 23)
|
|
Conflicts : 7 (Analyzed: 1)
|
|
Restarts : 0
|
|
Problems : 13 (Average Length: 32.00 Splits: 0)
|
|
Lemmas : 1 (Deleted: 0)
|
|
Binary : 0 (Ratio: 0.00%)
|
|
Ternary : 0 (Ratio: 0.00%)
|
|
Conflict : 1 (Average Length: 1.0 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 1 (Average: 85.00 Max: 85 Sum: 85)
|
|
Executed : 0 (Average: 23.00 Max: 23 Sum: 23 Ratio: 27.06%)
|
|
Bounded : 1 (Average: 62.00 Max: 62 Sum: 62 Ratio: 72.94%)
|
|
|
|
Rules : 83982
|
|
Atoms : 83982
|
|
Bodies : 1 (Original: 0)
|
|
Tight : Yes
|
|
Variables : 294552 (Eliminated: 0 Frozen: 294552)
|
|
Constraints : 1707803 (Binary: 95.0% Ternary: 4.3% Other: 0.7%)
|
|
|
|
Memory Peak : 515MB
|
|
Max. Length : 55 steps
|
|
Models : 0
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 0.82s
|
|
Memory: 490MB (+16MB)
|
|
UNSAT
|
|
Iteration Time: 1.60s
|
|
|
|
Iteration 14
|
|
Queue: [(13,65,0,True)]
|
|
Grounded Until: 60
|
|
Expected Memory: 528.0MB
|
|
Grounding... [('step', [61]), ('step', [62]), ('step', [63]), ('step', [64]), ('step', [65]), ('check', [65])]
|
|
Grounding Time: 0.82s
|
|
Memory: 520MB (+30MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0
|
|
Calls : 14
|
|
Time : 18.607s (Solving: 0.15s 1st Model: 0.00s Unsat: 0.15s)
|
|
CPU Time : 18.492s
|
|
|
|
Choices : 293 (Domain: 293)
|
|
Conflicts : 28 (Analyzed: 21)
|
|
Restarts : 0
|
|
Problems : 14 (Average Length: 34.50 Splits: 0)
|
|
Lemmas : 21 (Deleted: 0)
|
|
Binary : 0 (Ratio: 0.00%)
|
|
Ternary : 0 (Ratio: 0.00%)
|
|
Conflict : 21 (Average Length: 1.0 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 21 (Average: 80.71 Max: 85 Sum: 1695)
|
|
Executed : 0 (Average: 13.95 Max: 23 Sum: 293 Ratio: 17.29%)
|
|
Bounded : 21 (Average: 66.76 Max: 67 Sum: 1402 Ratio: 82.71%)
|
|
|
|
Rules : 83982
|
|
Atoms : 83982
|
|
Bodies : 1 (Original: 0)
|
|
Tight : Yes
|
|
Variables : 320188 (Eliminated: 0 Frozen: 320188)
|
|
Constraints : 1875727 (Binary: 95.0% Ternary: 4.3% Other: 0.7%)
|
|
|
|
Memory Peak : 564MB
|
|
Max. Length : 60 steps
|
|
Models : 0
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 0.85s
|
|
Memory: 538MB (+18MB)
|
|
UNSAT
|
|
Iteration Time: 1.99s
|
|
|
|
Iteration 15
|
|
Queue: [(14,70,0,True), (15,75,0,True), (16,80,0,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True)]
|
|
Grounded Until: 65
|
|
Expected Memory: 586.0MB
|
|
Grounding... [('step', [66]), ('step', [67]), ('step', [68]), ('step', [69]), ('step', [70]), ('check', [70])]
|
|
Grounding Time: 0.47s
|
|
Memory: 540MB (+2MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0
|
|
Calls : 15
|
|
Time : 20.450s (Solving: 0.35s 1st Model: 0.00s Unsat: 0.35s)
|
|
CPU Time : 20.336s
|
|
|
|
Choices : 682 (Domain: 682)
|
|
Conflicts : 133 (Analyzed: 125)
|
|
Restarts : 0
|
|
Problems : 15 (Average Length: 37.00 Splits: 0)
|
|
Lemmas : 125 (Deleted: 0)
|
|
Binary : 7 (Ratio: 5.60%)
|
|
Ternary : 0 (Ratio: 0.00%)
|
|
Conflict : 125 (Average Length: 710.6 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 125 (Average: 17.84 Max: 105 Sum: 2230)
|
|
Executed : 100 (Average: 5.46 Max: 105 Sum: 682 Ratio: 30.58%)
|
|
Bounded : 25 (Average: 61.92 Max: 72 Sum: 1548 Ratio: 69.42%)
|
|
|
|
Rules : 83982
|
|
Atoms : 83982
|
|
Bodies : 1 (Original: 0)
|
|
Tight : Yes
|
|
Variables : 345824 (Eliminated: 0 Frozen: 345824)
|
|
Constraints : 1899723 (Binary: 95.0% Ternary: 4.3% Other: 0.7%)
|
|
|
|
Memory Peak : 593MB
|
|
Max. Length : 65 steps
|
|
Models : 0
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 1.01s
|
|
Memory: 563MB (+23MB)
|
|
UNSAT
|
|
Iteration Time: 1.86s
|
|
|
|
Iteration 16
|
|
Queue: [(15,75,0,True), (16,80,0,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True)]
|
|
Grounded Until: 70
|
|
Expected Memory: 611.0MB
|
|
Grounding... [('step', [71]), ('step', [72]), ('step', [73]), ('step', [74]), ('step', [75]), ('check', [75])]
|
|
Grounding Time: 0.48s
|
|
Memory: 564MB (+1MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0
|
|
Calls : 16
|
|
Time : 22.697s (Solving: 0.99s 1st Model: 0.00s Unsat: 0.99s)
|
|
CPU Time : 22.584s
|
|
|
|
Choices : 3281 (Domain: 3281)
|
|
Conflicts : 593 (Analyzed: 584)
|
|
Restarts : 3 (Average: 194.67 Last: 104)
|
|
Problems : 16 (Average Length: 39.50 Splits: 0)
|
|
Lemmas : 584 (Deleted: 0)
|
|
Binary : 15 (Ratio: 2.57%)
|
|
Ternary : 2 (Ratio: 0.34%)
|
|
Conflict : 584 (Average Length: 1869.3 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 584 (Average: 10.05 Max: 143 Sum: 5867)
|
|
Executed : 542 (Average: 5.31 Max: 143 Sum: 3103 Ratio: 52.89%)
|
|
Bounded : 42 (Average: 65.81 Max: 77 Sum: 2764 Ratio: 47.11%)
|
|
|
|
Rules : 83982
|
|
Atoms : 83982
|
|
Bodies : 1 (Original: 0)
|
|
Tight : Yes
|
|
Variables : 371460 (Eliminated: 0 Frozen: 371460)
|
|
Constraints : 2098572 (Binary: 95.0% Ternary: 4.3% Other: 0.7%)
|
|
|
|
Memory Peak : 616MB
|
|
Max. Length : 70 steps
|
|
Models : 0
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 1.45s
|
|
Memory: 583MB (+19MB)
|
|
UNSAT
|
|
Iteration Time: 2.27s
|
|
|
|
Iteration 17
|
|
Queue: [(16,80,0,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True)]
|
|
Grounded Until: 75
|
|
Expected Memory: 631.0MB
|
|
Grounding... [('step', [76]), ('step', [77]), ('step', [78]), ('step', [79]), ('step', [80]), ('check', [80])]
|
|
Grounding Time: 0.49s
|
|
Memory: 591MB (+8MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0
|
|
Calls : 17
|
|
Time : 36.906s (Solving: 13.55s 1st Model: 0.00s Unsat: 13.55s)
|
|
CPU Time : 36.800s
|
|
|
|
Choices : 47015 (Domain: 47015)
|
|
Conflicts : 5422 (Analyzed: 5412)
|
|
Restarts : 27 (Average: 200.44 Last: 173)
|
|
Problems : 17 (Average Length: 42.00 Splits: 0)
|
|
Lemmas : 5412 (Deleted: 0)
|
|
Binary : 54 (Ratio: 1.00%)
|
|
Ternary : 4 (Ratio: 0.07%)
|
|
Conflict : 5412 (Average Length: 3326.0 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 5412 (Average: 8.97 Max: 240 Sum: 48545)
|
|
Executed : 5364 (Average: 8.40 Max: 240 Sum: 45452 Ratio: 93.63%)
|
|
Bounded : 48 (Average: 64.44 Max: 82 Sum: 3093 Ratio: 6.37%)
|
|
|
|
Rules : 83982
|
|
Atoms : 83982
|
|
Bodies : 1 (Original: 0)
|
|
Tight : Yes
|
|
Variables : 397096 (Eliminated: 0 Frozen: 397096)
|
|
Constraints : 2297454 (Binary: 95.0% Ternary: 4.3% Other: 0.7%)
|
|
|
|
Memory Peak : 765MB
|
|
Max. Length : 75 steps
|
|
Models : 0
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 13.38s
|
|
Memory: 701MB (+110MB)
|
|
UNSAT
|
|
Iteration Time: 14.23s
|
|
|
|
Iteration 18
|
|
Queue: [(17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True)]
|
|
Grounded Until: 80
|
|
Expected Memory: 819.0MB
|
|
Grounding... [('step', [81]), ('step', [82]), ('step', [83]), ('step', [84]), ('step', [85]), ('check', [85])]
|
|
Grounding Time: 0.48s
|
|
Memory: 701MB (+0MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0
|
|
Calls : 18
|
|
Time : 62.220s (Solving: 37.18s 1st Model: 0.00s Unsat: 37.18s)
|
|
CPU Time : 62.128s
|
|
|
|
Choices : 96601 (Domain: 96601)
|
|
Conflicts : 12905 (Analyzed: 12894)
|
|
Restarts : 57 (Average: 226.21 Last: 1008)
|
|
Problems : 18 (Average Length: 44.50 Splits: 0)
|
|
Lemmas : 12894 (Deleted: 0)
|
|
Binary : 100 (Ratio: 0.78%)
|
|
Ternary : 4 (Ratio: 0.03%)
|
|
Conflict : 12894 (Average Length: 4316.0 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 12894 (Average: 7.42 Max: 243 Sum: 95645)
|
|
Executed : 12845 (Average: 7.18 Max: 243 Sum: 92551 Ratio: 96.77%)
|
|
Bounded : 49 (Average: 63.14 Max: 82 Sum: 3094 Ratio: 3.23%)
|
|
|
|
Rules : 83982
|
|
Atoms : 83982
|
|
Bodies : 1 (Original: 0)
|
|
Tight : Yes
|
|
Variables : 422732 (Eliminated: 0 Frozen: 422732)
|
|
Constraints : 2498624 (Binary: 95.0% Ternary: 4.3% Other: 0.7%)
|
|
|
|
Memory Peak : 845MB
|
|
Max. Length : 80 steps
|
|
Models : 0
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 24.48s
|
|
Memory: 845MB (+144MB)
|
|
UNSAT
|
|
Iteration Time: 25.34s
|
|
|
|
Iteration 19
|
|
Queue: [(18,90,0,True), (19,95,0,True), (20,100,0,True)]
|
|
Grounded Until: 85
|
|
Expected Memory: 989.0MB
|
|
Grounding... [('step', [86]), ('step', [87]), ('step', [88]), ('step', [89]), ('step', [90]), ('check', [90])]
|
|
Grounding Time: 0.47s
|
|
Memory: 845MB (+0MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0
|
|
Calls : 19
|
|
Time : 75.257s (Solving: 48.47s 1st Model: 0.00s Unsat: 48.47s)
|
|
CPU Time : 75.168s
|
|
|
|
Choices : 130168 (Domain: 130168)
|
|
Conflicts : 16040 (Analyzed: 16028)
|
|
Restarts : 71 (Average: 225.75 Last: 1008)
|
|
Problems : 19 (Average Length: 47.00 Splits: 0)
|
|
Lemmas : 16028 (Deleted: 0)
|
|
Binary : 144 (Ratio: 0.90%)
|
|
Ternary : 4 (Ratio: 0.02%)
|
|
Conflict : 16028 (Average Length: 4599.9 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 16028 (Average: 7.96 Max: 313 Sum: 127533)
|
|
Executed : 15977 (Average: 7.76 Max: 313 Sum: 124437 Ratio: 97.57%)
|
|
Bounded : 51 (Average: 60.71 Max: 82 Sum: 3096 Ratio: 2.43%)
|
|
|
|
Rules : 83982
|
|
Atoms : 83982
|
|
Bodies : 1 (Original: 0)
|
|
Tight : Yes
|
|
Variables : 448368 (Eliminated: 0 Frozen: 448368)
|
|
Constraints : 2699869 (Binary: 95.0% Ternary: 4.3% Other: 0.7%)
|
|
|
|
Memory Peak : 992MB
|
|
Max. Length : 85 steps
|
|
Models : 0
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 12.16s
|
|
Memory: 928MB (+83MB)
|
|
UNSAT
|
|
Iteration Time: 13.05s
|
|
|
|
Iteration 20
|
|
Queue: [(19,95,0,True), (20,100,0,True)]
|
|
Grounded Until: 90
|
|
Expected Memory: 1072.0MB
|
|
Grounding... [('step', [91]), ('step', [92]), ('step', [93]), ('step', [94]), ('step', [95]), ('check', [95])]
|
|
Grounding Time: 0.50s
|
|
Memory: 933MB (+5MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 20
|
|
Time : 208.168s (Solving: 179.52s 1st Model: 0.00s Unsat: 48.47s)
|
|
CPU Time : 208.136s
|
|
|
|
Choices : 493764 (Domain: 493764)
|
|
Conflicts : 44215 (Analyzed: 44203)
|
|
Restarts : 171 (Average: 258.50 Last: 1008)
|
|
Problems : 20 (Average Length: 49.50 Splits: 0)
|
|
Lemmas : 44203 (Deleted: 31305)
|
|
Binary : 321 (Ratio: 0.73%)
|
|
Ternary : 4 (Ratio: 0.01%)
|
|
Conflict : 44203 (Average Length: 7180.6 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 44203 (Average: 10.45 Max: 1930 Sum: 461828)
|
|
Executed : 44151 (Average: 10.38 Max: 1930 Sum: 458731 Ratio: 99.33%)
|
|
Bounded : 52 (Average: 59.56 Max: 82 Sum: 3097 Ratio: 0.67%)
|
|
|
|
Rules : 83982
|
|
Atoms : 83982
|
|
Bodies : 1 (Original: 0)
|
|
Tight : Yes
|
|
Variables : 474004 (Eliminated: 0 Frozen: 474004)
|
|
Constraints : 2901114 (Binary: 95.1% Ternary: 4.3% Other: 0.7%)
|
|
|
|
Memory Peak : 1338MB
|
|
Max. Length : 90 steps
|
|
Models : 0
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 132.00s
|
|
Memory: 1274MB (+341MB)
|
|
UNKNOWN
|
|
Iteration Time: 132.98s
|
|
|
|
Iteration 21
|
|
Queue: [(20,100,0,True)]
|
|
Grounded Until: 95
|
|
Expected Memory: 1620.0MB
|
|
Grounding... [('step', [96]), ('step', [97]), ('step', [98]), ('step', [99]), ('step', [100]), ('check', [100])]
|
|
Grounding Time: 0.47s
|
|
Memory: 1274MB (+0MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 21
|
|
Time : 358.012s (Solving: 327.44s 1st Model: 0.00s Unsat: 48.47s)
|
|
CPU Time : 358.048s
|
|
|
|
Choices : 1146473 (Domain: 1146473)
|
|
Conflicts : 72502 (Analyzed: 72490)
|
|
Restarts : 271 (Average: 267.49 Last: 1008)
|
|
Problems : 21 (Average Length: 52.00 Splits: 0)
|
|
Lemmas : 72490 (Deleted: 60275)
|
|
Binary : 509 (Ratio: 0.70%)
|
|
Ternary : 9 (Ratio: 0.01%)
|
|
Conflict : 72490 (Average Length: 10260.5 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 72490 (Average: 14.42 Max: 1930 Sum: 1045121)
|
|
Executed : 72436 (Average: 14.37 Max: 1930 Sum: 1042022 Ratio: 99.70%)
|
|
Bounded : 54 (Average: 57.39 Max: 82 Sum: 3099 Ratio: 0.30%)
|
|
|
|
Rules : 83982
|
|
Atoms : 83982
|
|
Bodies : 1 (Original: 0)
|
|
Tight : Yes
|
|
Variables : 499640 (Eliminated: 0 Frozen: 499640)
|
|
Constraints : 3102359 (Binary: 95.1% Ternary: 4.3% Other: 0.7%)
|
|
|
|
Memory Peak : 1749MB
|
|
Max. Length : 95 steps
|
|
Models : 0
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 148.92s
|
|
Memory: 1685MB (+411MB)
|
|
UNKNOWN
|
|
Iteration Time: 149.92s
|
|
|
|
Iteration 22
|
|
Queue: [(19,95,1,True), (20,100,1,True), (21,105,0,True), (22,110,0,True), (23,115,0,True), (24,120,0,True), (25,125,0,True), (26,130,0,True), (27,135,0,True), (28,140,0,True), (29,145,0,True), (30,150,0,True), (31,155,0,True), (32,160,0,True)]
|
|
Grounded Until: 100
|
|
Blocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 22
|
|
Time : 536.310s (Solving: 505.43s 1st Model: 0.00s Unsat: 48.47s)
|
|
CPU Time : 536.424s
|
|
|
|
Choices : 1613442 (Domain: 1613442)
|
|
Conflicts : 100695 (Analyzed: 100683)
|
|
Restarts : 371 (Average: 271.38 Last: 1008)
|
|
Problems : 22 (Average Length: 54.27 Splits: 0)
|
|
Lemmas : 100683 (Deleted: 88316)
|
|
Binary : 599 (Ratio: 0.59%)
|
|
Ternary : 12 (Ratio: 0.01%)
|
|
Conflict : 100683 (Average Length: 10617.3 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 100683 (Average: 14.43 Max: 2469 Sum: 1453282)
|
|
Executed : 100624 (Average: 14.40 Max: 2469 Sum: 1450178 Ratio: 99.79%)
|
|
Bounded : 59 (Average: 52.61 Max: 82 Sum: 3104 Ratio: 0.21%)
|
|
|
|
Rules : 83982
|
|
Atoms : 83982
|
|
Bodies : 1 (Original: 0)
|
|
Tight : Yes
|
|
Variables : 499640 (Eliminated: 0 Frozen: 499640)
|
|
Constraints : 3102359 (Binary: 95.1% Ternary: 4.3% Other: 0.7%)
|
|
|
|
Memory Peak : 1877MB
|
|
Max. Length : 100 steps
|
|
Models : 0
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 178.16s
|
|
Memory: 1877MB (+192MB)
|
|
UNKNOWN
|
|
Iteration Time: 178.38s
|
|
|
|
Iteration 23
|
|
Queue: [(20,100,1,True), (21,105,0,True), (22,110,0,True), (23,115,0,True), (24,120,0,True), (25,125,0,True), (26,130,0,True), (27,135,0,True), (28,140,0,True), (29,145,0,True), (30,150,0,True), (31,155,0,True), (32,160,0,True)]
|
|
Grounded Until: 100
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 23
|
|
Time : 719.421s (Solving: 688.26s 1st Model: 0.00s Unsat: 48.47s)
|
|
CPU Time : 719.612s
|
|
|
|
Choices : 2035676 (Domain: 2035676)
|
|
Conflicts : 128978 (Analyzed: 128966)
|
|
Restarts : 471 (Average: 273.81 Last: 1008)
|
|
Problems : 23 (Average Length: 56.35 Splits: 0)
|
|
Lemmas : 128966 (Deleted: 116395)
|
|
Binary : 640 (Ratio: 0.50%)
|
|
Ternary : 15 (Ratio: 0.01%)
|
|
Conflict : 128966 (Average Length: 12095.4 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 128966 (Average: 14.25 Max: 2469 Sum: 1838086)
|
|
Executed : 128907 (Average: 14.23 Max: 2469 Sum: 1834982 Ratio: 99.83%)
|
|
Bounded : 59 (Average: 52.61 Max: 82 Sum: 3104 Ratio: 0.17%)
|
|
|
|
Rules : 83982
|
|
Atoms : 83982
|
|
Bodies : 1 (Original: 0)
|
|
Tight : Yes
|
|
Variables : 499640 (Eliminated: 0 Frozen: 499640)
|
|
Constraints : 3102359 (Binary: 95.1% Ternary: 4.3% Other: 0.7%)
|
|
|
|
Memory Peak : 2005MB
|
|
Max. Length : 100 steps
|
|
Models : 0
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 182.99s
|
|
Memory: 1941MB (+64MB)
|
|
UNKNOWN
|
|
Iteration Time: 183.19s
|
|
|
|
Iteration 24
|
|
Queue: [(21,105,0,True), (22,110,0,True), (23,115,0,True), (24,120,0,True), (25,125,0,True), (26,130,0,True), (27,135,0,True), (28,140,0,True), (29,145,0,True), (30,150,0,True), (31,155,0,True), (32,160,0,True)]
|
|
Grounded Until: 100
|
|
Expected Memory: 2352.0MB
|
|
Grounding... [('step', [101]), ('step', [102]), ('step', [103]), ('step', [104]), ('step', [105]), ('check', [105])]
|
|
Grounding Time: 0.49s
|
|
Memory: 1941MB (+0MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 24
|
|
Time : 875.984s (Solving: 842.84s 1st Model: 0.00s Unsat: 48.47s)
|
|
CPU Time : 876.244s
|
|
|
|
Choices : 2866949 (Domain: 2866949)
|
|
Conflicts : 157222 (Analyzed: 157210)
|
|
Restarts : 571 (Average: 275.32 Last: 1008)
|
|
Problems : 24 (Average Length: 58.46 Splits: 0)
|
|
Lemmas : 157210 (Deleted: 144315)
|
|
Binary : 799 (Ratio: 0.51%)
|
|
Ternary : 19 (Ratio: 0.01%)
|
|
Conflict : 157210 (Average Length: 13577.6 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 157210 (Average: 16.11 Max: 3401 Sum: 2533408)
|
|
Executed : 157150 (Average: 16.10 Max: 3401 Sum: 2530303 Ratio: 99.88%)
|
|
Bounded : 60 (Average: 51.75 Max: 82 Sum: 3105 Ratio: 0.12%)
|
|
|
|
Rules : 83982
|
|
Atoms : 83982
|
|
Bodies : 1 (Original: 0)
|
|
Tight : Yes
|
|
Variables : 525276 (Eliminated: 0 Frozen: 525276)
|
|
Constraints : 3303604 (Binary: 95.1% Ternary: 4.3% Other: 0.7%)
|
|
|
|
Memory Peak : 2164MB
|
|
Max. Length : 100 steps
|
|
Models : 0
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 155.61s
|
|
Memory: 2100MB (+159MB)
|
|
UNKNOWN
|
|
Iteration Time: 156.64s
|
|
|
|
Iteration 25
|
|
Queue: [(22,110,0,True), (23,115,0,True), (24,120,0,True), (25,125,0,True), (26,130,0,True), (27,135,0,True), (28,140,0,True), (29,145,0,True), (30,150,0,True), (31,155,0,True), (32,160,0,True)]
|
|
Grounded Until: 105
|
|
Expected Memory: 2511.0MB
|
|
Grounding... [('step', [106]), ('step', [107]), ('step', [108]), ('step', [109]), ('step', [110]), ('check', [110])]
|
|
Grounding Time: 0.49s
|
|
Memory: 2100MB (+0MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
*** Info : (planner): INTERRUPTED by signal!
|
|
UNKNOWN
|
|
|
|
INTERRUPTED : 1
|
|
|
|
Models : 0+
|
|
Calls : 25
|
|
Time : 893.032s (Solving: 857.75s 1st Model: 0.00s Unsat: 48.47s)
|
|
CPU Time : 893.284s
|
|
|
|
Choices : 3064152 (Domain: 3064152)
|
|
Conflicts : 159824 (Analyzed: 159812)
|
|
Restarts : 585 (Average: 273.18 Last: 1008)
|
|
Problems : 25 (Average Length: 60.60 Splits: 0)
|
|
Lemmas : 159812 (Deleted: 144315)
|
|
Binary : 856 (Ratio: 0.54%)
|
|
Ternary : 19 (Ratio: 0.01%)
|
|
Conflict : 159812 (Average Length: 13635.6 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 159812 (Average: 16.87 Max: 6431 Sum: 2695372)
|
|
Executed : 159751 (Average: 16.85 Max: 6431 Sum: 2692266 Ratio: 99.88%)
|
|
Bounded : 61 (Average: 50.92 Max: 82 Sum: 3106 Ratio: 0.12%)
|
|
|
|
Rules : 83982
|
|
Atoms : 83982
|
|
Bodies : 1 (Original: 0)
|
|
Tight : Yes
|
|
Variables : 550912 (Eliminated: 0 Frozen: 550912)
|
|
Constraints : 3504849 (Binary: 95.1% Ternary: 4.3% Other: 0.7%)
|
|
|
|
Memory Peak : 2169MB
|
|
Max. Length : 105 steps
|
|
Models : 0
|
|
|
|
|