1056 lines
37 KiB
Plaintext
1056 lines
37 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-16.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-16.pddl
|
||
|
|
Parsing...
|
||
|
|
Parsing: [0.110s CPU, 0.110s wall-clock]
|
||
|
|
Normalizing task... [0.010s CPU, 0.004s wall-clock]
|
||
|
|
Instantiating...
|
||
|
|
Generating Datalog program... [0.020s CPU, 0.029s wall-clock]
|
||
|
|
Normalizing Datalog program...
|
||
|
|
Normalizing Datalog program: [0.020s CPU, 0.023s wall-clock]
|
||
|
|
Preparing model... [0.090s CPU, 0.094s wall-clock]
|
||
|
|
Generated 46 rules.
|
||
|
|
Computing model... [4.090s CPU, 4.094s wall-clock]
|
||
|
|
35432 relevant atoms
|
||
|
|
16424 auxiliary atoms
|
||
|
|
51856 final queue length
|
||
|
|
113272 total queue pushes
|
||
|
|
Completing instantiation... [13.090s CPU, 13.081s wall-clock]
|
||
|
|
Instantiating: [17.370s CPU, 17.369s wall-clock]
|
||
|
|
Computing fact groups...
|
||
|
|
Finding invariants...
|
||
|
|
12 initial candidates
|
||
|
|
Finding invariants: [0.170s CPU, 0.174s wall-clock]
|
||
|
|
Checking invariant weight... [0.010s CPU, 0.007s wall-clock]
|
||
|
|
Instantiating groups... [0.110s CPU, 0.115s wall-clock]
|
||
|
|
Collecting mutex groups... [0.020s CPU, 0.013s wall-clock]
|
||
|
|
Choosing groups...
|
||
|
|
0 uncovered facts
|
||
|
|
Choosing groups: [0.040s CPU, 0.041s wall-clock]
|
||
|
|
Building translation key... [0.020s CPU, 0.024s wall-clock]
|
||
|
|
Computing fact groups: [0.490s CPU, 0.498s wall-clock]
|
||
|
|
Building STRIPS to SAS dictionary... [0.020s CPU, 0.011s wall-clock]
|
||
|
|
Building dictionary for full mutex groups... [0.010s CPU, 0.011s wall-clock]
|
||
|
|
Building mutex information...
|
||
|
|
Building mutex information: [0.010s CPU, 0.013s wall-clock]
|
||
|
|
Translating task...
|
||
|
|
Processing axioms...
|
||
|
|
Simplifying axioms... [0.000s CPU, 0.000s wall-clock]
|
||
|
|
Processing axioms: [0.530s CPU, 0.531s wall-clock]
|
||
|
|
Translating task: [9.940s CPU, 9.929s wall-clock]
|
||
|
|
0 effect conditions simplified
|
||
|
|
0 implied preconditions added
|
||
|
|
Detecting unreachable propositions...
|
||
|
|
0 operators removed
|
||
|
|
0 axioms removed
|
||
|
|
56 propositions removed
|
||
|
|
Detecting unreachable propositions: [5.140s CPU, 5.142s wall-clock]
|
||
|
|
Reordering and filtering variables...
|
||
|
|
56 of 56 variables necessary.
|
||
|
|
0 of 56 mutex groups necessary.
|
||
|
|
32088 of 32088 operators necessary.
|
||
|
|
0 of 0 axiom rules necessary.
|
||
|
|
Reordering and filtering variables: [1.510s CPU, 1.511s wall-clock]
|
||
|
|
Translator variables: 56
|
||
|
|
Translator derived variables: 0
|
||
|
|
Translator facts: 2088
|
||
|
|
Translator goal facts: 40
|
||
|
|
Translator mutex groups: 0
|
||
|
|
Translator total mutex groups size: 0
|
||
|
|
Translator operators: 32088
|
||
|
|
Translator axioms: 0
|
||
|
|
Translator task size: 192528
|
||
|
|
Translator peak memory: 162824 KB
|
||
|
|
Writing output... [3.350s CPU, 3.586s wall-clock]
|
||
|
|
Done! [38.390s CPU, 38.618s wall-clock]
|
||
|
|
planner.py version 0.0.1
|
||
|
|
|
||
|
|
Time: 8.31s
|
||
|
|
Memory: 583MB
|
||
|
|
|
||
|
|
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 : 9.614s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
|
||
|
|
CPU Time : 8.348s
|
||
|
|
|
||
|
|
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 : 581162
|
||
|
|
Atoms : 581162
|
||
|
|
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 : 719MB
|
||
|
|
Max. Length : 0 steps
|
||
|
|
Models : 0
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 0.04s
|
||
|
|
Memory: 655MB (+72MB)
|
||
|
|
UNSAT
|
||
|
|
Iteration Time: 0.04s
|
||
|
|
|
||
|
|
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: 655MB
|
||
|
|
Grounding... [('step', [1]), ('step', [2]), ('step', [3]), ('step', [4]), ('step', [5]), ('check', [5])]
|
||
|
|
Grounding Time: 2.64s
|
||
|
|
Memory: 655MB (+0MB)
|
||
|
|
Unblocking actions...
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0
|
||
|
|
Calls : 2
|
||
|
|
Time : 15.117s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
|
||
|
|
CPU Time : 13.852s
|
||
|
|
|
||
|
|
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 : 581162
|
||
|
|
Atoms : 581162
|
||
|
|
Bodies : 1 (Original: 0)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 147475 (Eliminated: 0 Frozen: 8356)
|
||
|
|
Constraints : 251204 (Binary: 97.6% Ternary: 1.0% Other: 1.3%)
|
||
|
|
|
||
|
|
Memory Peak : 719MB
|
||
|
|
Max. Length : 0 steps
|
||
|
|
Models : 0
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 0.91s
|
||
|
|
Memory: 690MB (+35MB)
|
||
|
|
UNSAT
|
||
|
|
Iteration Time: 5.51s
|
||
|
|
|
||
|
|
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: 725.0MB
|
||
|
|
Grounding... [('step', [6]), ('step', [7]), ('step', [8]), ('step', [9]), ('step', [10]), ('check', [10])]
|
||
|
|
Grounding Time: 3.10s
|
||
|
|
Memory: 719MB (+29MB)
|
||
|
|
Unblocking actions...
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 3
|
||
|
|
Time : 24.500s (Solving: 4.45s 1st Model: 0.00s Unsat: 0.00s)
|
||
|
|
CPU Time : 23.240s
|
||
|
|
|
||
|
|
Choices : 181924 (Domain: 181924)
|
||
|
|
Conflicts : 9668 (Analyzed: 9668)
|
||
|
|
Restarts : 100 (Average: 96.68 Last: 67)
|
||
|
|
Problems : 3 (Average Length: 7.00 Splits: 0)
|
||
|
|
Lemmas : 9668 (Deleted: 5948)
|
||
|
|
Binary : 392 (Ratio: 4.05%)
|
||
|
|
Ternary : 202 (Ratio: 2.09%)
|
||
|
|
Conflict : 9668 (Average Length: 334.3 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 9668 (Average: 17.47 Max: 1024 Sum: 168874)
|
||
|
|
Executed : 9667 (Average: 17.47 Max: 1024 Sum: 168862 Ratio: 99.99%)
|
||
|
|
Bounded : 1 (Average: 12.00 Max: 12 Sum: 12 Ratio: 0.01%)
|
||
|
|
|
||
|
|
Rules : 581162
|
||
|
|
Atoms : 581162
|
||
|
|
Bodies : 1 (Original: 0)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 322160 (Eliminated: 0 Frozen: 18318)
|
||
|
|
Constraints : 1622570 (Binary: 98.4% Ternary: 0.8% Other: 0.9%)
|
||
|
|
|
||
|
|
Memory Peak : 801MB
|
||
|
|
Max. Length : 5 steps
|
||
|
|
Models : 0
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 4.62s
|
||
|
|
Memory: 801MB (+82MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 9.40s
|
||
|
|
|
||
|
|
Iteration 4
|
||
|
|
Queue: [(3,15,0,True), (4,20,0,True), (5,25,0,True), (6,30,0,True)]
|
||
|
|
Grounded Until: 10
|
||
|
|
Expected Memory: 912.0MB
|
||
|
|
Grounding... [('step', [11]), ('step', [12]), ('step', [13]), ('step', [14]), ('step', [15]), ('check', [15])]
|
||
|
|
Grounding Time: 2.79s
|
||
|
|
Memory: 840MB (+39MB)
|
||
|
|
Unblocking actions...
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 4
|
||
|
|
Time : 38.386s (Solving: 13.87s 1st Model: 0.00s Unsat: 0.00s)
|
||
|
|
CPU Time : 37.132s
|
||
|
|
|
||
|
|
Choices : 468525 (Domain: 468525)
|
||
|
|
Conflicts : 21313 (Analyzed: 21313)
|
||
|
|
Restarts : 200 (Average: 106.56 Last: 192)
|
||
|
|
Problems : 4 (Average Length: 9.50 Splits: 0)
|
||
|
|
Lemmas : 21313 (Deleted: 16824)
|
||
|
|
Binary : 580 (Ratio: 2.72%)
|
||
|
|
Ternary : 276 (Ratio: 1.29%)
|
||
|
|
Conflict : 21313 (Average Length: 777.4 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 21313 (Average: 19.29 Max: 1236 Sum: 411134)
|
||
|
|
Executed : 21310 (Average: 19.29 Max: 1236 Sum: 411120 Ratio: 100.00%)
|
||
|
|
Bounded : 3 (Average: 4.67 Max: 12 Sum: 14 Ratio: 0.00%)
|
||
|
|
|
||
|
|
Rules : 581162
|
||
|
|
Atoms : 581162
|
||
|
|
Bodies : 1 (Original: 0)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 503771 (Eliminated: 0 Frozen: 28658)
|
||
|
|
Constraints : 3073591 (Binary: 98.5% Ternary: 0.7% Other: 0.8%)
|
||
|
|
|
||
|
|
Memory Peak : 974MB
|
||
|
|
Max. Length : 10 steps
|
||
|
|
Models : 0
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 9.60s
|
||
|
|
Memory: 974MB (+134MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 13.91s
|
||
|
|
|
||
|
|
Iteration 5
|
||
|
|
Queue: [(4,20,0,True), (5,25,0,True), (6,30,0,True)]
|
||
|
|
Grounded Until: 15
|
||
|
|
Expected Memory: 1147.0MB
|
||
|
|
Grounding... [('step', [16]), ('step', [17]), ('step', [18]), ('step', [19]), ('step', [20]), ('check', [20])]
|
||
|
|
Grounding Time: 2.94s
|
||
|
|
Memory: 1019MB (+45MB)
|
||
|
|
Unblocking actions...
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 5
|
||
|
|
Time : 56.802s (Solving: 27.62s 1st Model: 0.00s Unsat: 0.00s)
|
||
|
|
CPU Time : 55.556s
|
||
|
|
|
||
|
|
Choices : 943226 (Domain: 943226)
|
||
|
|
Conflicts : 33421 (Analyzed: 33421)
|
||
|
|
Restarts : 300 (Average: 111.40 Last: 192)
|
||
|
|
Problems : 5 (Average Length: 12.00 Splits: 0)
|
||
|
|
Lemmas : 33421 (Deleted: 24934)
|
||
|
|
Binary : 726 (Ratio: 2.17%)
|
||
|
|
Ternary : 366 (Ratio: 1.10%)
|
||
|
|
Conflict : 33421 (Average Length: 759.0 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 33421 (Average: 23.73 Max: 2503 Sum: 792994)
|
||
|
|
Executed : 33414 (Average: 23.73 Max: 2503 Sum: 792976 Ratio: 100.00%)
|
||
|
|
Bounded : 7 (Average: 2.57 Max: 12 Sum: 18 Ratio: 0.00%)
|
||
|
|
|
||
|
|
Rules : 581162
|
||
|
|
Atoms : 581162
|
||
|
|
Bodies : 1 (Original: 0)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 685382 (Eliminated: 0 Frozen: 38998)
|
||
|
|
Constraints : 4524621 (Binary: 98.5% Ternary: 0.7% Other: 0.8%)
|
||
|
|
|
||
|
|
Memory Peak : 1138MB
|
||
|
|
Max. Length : 15 steps
|
||
|
|
Models : 0
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 13.95s
|
||
|
|
Memory: 1079MB (+60MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 18.44s
|
||
|
|
|
||
|
|
Iteration 6
|
||
|
|
Queue: [(5,25,0,True), (6,30,0,True)]
|
||
|
|
Grounded Until: 20
|
||
|
|
Expected Memory: 1252.0MB
|
||
|
|
Grounding... [('step', [21]), ('step', [22]), ('step', [23]), ('step', [24]), ('step', [25]), ('check', [25])]
|
||
|
|
Grounding Time: 3.43s
|
||
|
|
Memory: 1203MB (+124MB)
|
||
|
|
Unblocking actions...
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 6
|
||
|
|
Time : 81.322s (Solving: 46.86s 1st Model: 0.00s Unsat: 0.00s)
|
||
|
|
CPU Time : 80.088s
|
||
|
|
|
||
|
|
Choices : 1425922 (Domain: 1425922)
|
||
|
|
Conflicts : 42783 (Analyzed: 42783)
|
||
|
|
Restarts : 400 (Average: 106.96 Last: 192)
|
||
|
|
Problems : 6 (Average Length: 14.50 Splits: 0)
|
||
|
|
Lemmas : 42783 (Deleted: 35573)
|
||
|
|
Binary : 810 (Ratio: 1.89%)
|
||
|
|
Ternary : 414 (Ratio: 0.97%)
|
||
|
|
Conflict : 42783 (Average Length: 1651.2 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 42783 (Average: 25.97 Max: 2503 Sum: 1110995)
|
||
|
|
Executed : 42775 (Average: 25.97 Max: 2503 Sum: 1110950 Ratio: 100.00%)
|
||
|
|
Bounded : 8 (Average: 5.62 Max: 27 Sum: 45 Ratio: 0.00%)
|
||
|
|
|
||
|
|
Rules : 581162
|
||
|
|
Atoms : 581162
|
||
|
|
Bodies : 1 (Original: 0)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 866993 (Eliminated: 0 Frozen: 49338)
|
||
|
|
Constraints : 5975651 (Binary: 98.5% Ternary: 0.7% Other: 0.8%)
|
||
|
|
|
||
|
|
Memory Peak : 1436MB
|
||
|
|
Max. Length : 20 steps
|
||
|
|
Models : 0
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 19.48s
|
||
|
|
Memory: 1372MB (+169MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 24.55s
|
||
|
|
|
||
|
|
Iteration 7
|
||
|
|
Queue: [(6,30,0,True)]
|
||
|
|
Grounded Until: 25
|
||
|
|
Expected Memory: 1665.0MB
|
||
|
|
Grounding... [('step', [26]), ('step', [27]), ('step', [28]), ('step', [29]), ('step', [30]), ('check', [30])]
|
||
|
|
Grounding Time: 2.81s
|
||
|
|
Memory: 1440MB (+68MB)
|
||
|
|
Unblocking actions...
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 7
|
||
|
|
Time : 106.484s (Solving: 67.30s 1st Model: 0.00s Unsat: 0.00s)
|
||
|
|
CPU Time : 105.260s
|
||
|
|
|
||
|
|
Choices : 2056508 (Domain: 2056508)
|
||
|
|
Conflicts : 52315 (Analyzed: 52315)
|
||
|
|
Restarts : 500 (Average: 104.63 Last: 192)
|
||
|
|
Problems : 7 (Average Length: 17.00 Splits: 0)
|
||
|
|
Lemmas : 52315 (Deleted: 45210)
|
||
|
|
Binary : 867 (Ratio: 1.66%)
|
||
|
|
Ternary : 452 (Ratio: 0.86%)
|
||
|
|
Conflict : 52315 (Average Length: 2067.0 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 52315 (Average: 30.12 Max: 2503 Sum: 1575823)
|
||
|
|
Executed : 52306 (Average: 30.12 Max: 2503 Sum: 1575746 Ratio: 100.00%)
|
||
|
|
Bounded : 9 (Average: 8.56 Max: 32 Sum: 77 Ratio: 0.00%)
|
||
|
|
|
||
|
|
Rules : 581162
|
||
|
|
Atoms : 581162
|
||
|
|
Bodies : 1 (Original: 0)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 1048604 (Eliminated: 0 Frozen: 59678)
|
||
|
|
Constraints : 7426672 (Binary: 98.5% Ternary: 0.7% Other: 0.8%)
|
||
|
|
|
||
|
|
Memory Peak : 1599MB
|
||
|
|
Max. Length : 25 steps
|
||
|
|
Models : 0
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 20.68s
|
||
|
|
Memory: 1504MB (+64MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 25.19s
|
||
|
|
|
||
|
|
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 : 8
|
||
|
|
Time : 113.654s (Solving: 74.19s 1st Model: 0.00s Unsat: 0.00s)
|
||
|
|
CPU Time : 112.436s
|
||
|
|
|
||
|
|
Choices : 2129639 (Domain: 2129639)
|
||
|
|
Conflicts : 63013 (Analyzed: 63013)
|
||
|
|
Restarts : 600 (Average: 105.02 Last: 192)
|
||
|
|
Problems : 8 (Average Length: 18.88 Splits: 0)
|
||
|
|
Lemmas : 63013 (Deleted: 52925)
|
||
|
|
Binary : 949 (Ratio: 1.51%)
|
||
|
|
Ternary : 531 (Ratio: 0.84%)
|
||
|
|
Conflict : 63013 (Average Length: 1830.4 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 63013 (Average: 26.08 Max: 2503 Sum: 1643200)
|
||
|
|
Executed : 62998 (Average: 26.07 Max: 2503 Sum: 1643024 Ratio: 99.99%)
|
||
|
|
Bounded : 15 (Average: 11.73 Max: 32 Sum: 176 Ratio: 0.01%)
|
||
|
|
|
||
|
|
Rules : 581162
|
||
|
|
Atoms : 581162
|
||
|
|
Bodies : 1 (Original: 0)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 1048604 (Eliminated: 0 Frozen: 59678)
|
||
|
|
Constraints : 7426663 (Binary: 98.5% Ternary: 0.7% Other: 0.8%)
|
||
|
|
|
||
|
|
Memory Peak : 1599MB
|
||
|
|
Max. Length : 30 steps
|
||
|
|
Models : 0
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 7.07s
|
||
|
|
Memory: 1515MB (+11MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 7.18s
|
||
|
|
|
||
|
|
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 : 9
|
||
|
|
Time : 123.546s (Solving: 83.83s 1st Model: 0.00s Unsat: 0.00s)
|
||
|
|
CPU Time : 122.332s
|
||
|
|
|
||
|
|
Choices : 2312478 (Domain: 2312478)
|
||
|
|
Conflicts : 73764 (Analyzed: 73764)
|
||
|
|
Restarts : 700 (Average: 105.38 Last: 192)
|
||
|
|
Problems : 9 (Average Length: 20.33 Splits: 0)
|
||
|
|
Lemmas : 73764 (Deleted: 61848)
|
||
|
|
Binary : 977 (Ratio: 1.32%)
|
||
|
|
Ternary : 572 (Ratio: 0.78%)
|
||
|
|
Conflict : 73764 (Average Length: 1703.5 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 73764 (Average: 24.37 Max: 2503 Sum: 1797839)
|
||
|
|
Executed : 73746 (Average: 24.37 Max: 2503 Sum: 1797660 Ratio: 99.99%)
|
||
|
|
Bounded : 18 (Average: 9.94 Max: 32 Sum: 179 Ratio: 0.01%)
|
||
|
|
|
||
|
|
Rules : 581162
|
||
|
|
Atoms : 581162
|
||
|
|
Bodies : 1 (Original: 0)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 1048604 (Eliminated: 0 Frozen: 59678)
|
||
|
|
Constraints : 7426636 (Binary: 98.5% Ternary: 0.7% Other: 0.8%)
|
||
|
|
|
||
|
|
Memory Peak : 1599MB
|
||
|
|
Max. Length : 30 steps
|
||
|
|
Models : 0
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 9.80s
|
||
|
|
Memory: 1515MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 9.90s
|
||
|
|
|
||
|
|
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 : 10
|
||
|
|
Time : 140.173s (Solving: 100.23s 1st Model: 0.00s Unsat: 0.00s)
|
||
|
|
CPU Time : 138.968s
|
||
|
|
|
||
|
|
Choices : 2904667 (Domain: 2904667)
|
||
|
|
Conflicts : 85083 (Analyzed: 85083)
|
||
|
|
Restarts : 800 (Average: 106.35 Last: 192)
|
||
|
|
Problems : 10 (Average Length: 21.50 Splits: 0)
|
||
|
|
Lemmas : 85083 (Deleted: 73301)
|
||
|
|
Binary : 1056 (Ratio: 1.24%)
|
||
|
|
Ternary : 623 (Ratio: 0.73%)
|
||
|
|
Conflict : 85083 (Average Length: 1617.5 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 85083 (Average: 26.85 Max: 2503 Sum: 2284291)
|
||
|
|
Executed : 85047 (Average: 26.85 Max: 2503 Sum: 2284063 Ratio: 99.99%)
|
||
|
|
Bounded : 36 (Average: 6.33 Max: 32 Sum: 228 Ratio: 0.01%)
|
||
|
|
|
||
|
|
Rules : 581162
|
||
|
|
Atoms : 581162
|
||
|
|
Bodies : 1 (Original: 0)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 1048604 (Eliminated: 0 Frozen: 59678)
|
||
|
|
Constraints : 7426636 (Binary: 98.5% Ternary: 0.7% Other: 0.8%)
|
||
|
|
|
||
|
|
Memory Peak : 1599MB
|
||
|
|
Max. Length : 30 steps
|
||
|
|
Models : 0
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 16.56s
|
||
|
|
Memory: 1515MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 16.64s
|
||
|
|
|
||
|
|
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 : 11
|
||
|
|
Time : 162.939s (Solving: 122.76s 1st Model: 0.00s Unsat: 0.00s)
|
||
|
|
CPU Time : 161.728s
|
||
|
|
|
||
|
|
Choices : 3724621 (Domain: 3724621)
|
||
|
|
Conflicts : 95507 (Analyzed: 95507)
|
||
|
|
Restarts : 900 (Average: 106.12 Last: 192)
|
||
|
|
Problems : 11 (Average Length: 22.45 Splits: 0)
|
||
|
|
Lemmas : 95507 (Deleted: 81554)
|
||
|
|
Binary : 1183 (Ratio: 1.24%)
|
||
|
|
Ternary : 733 (Ratio: 0.77%)
|
||
|
|
Conflict : 95507 (Average Length: 1543.0 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 95507 (Average: 30.98 Max: 3323 Sum: 2959017)
|
||
|
|
Executed : 95463 (Average: 30.98 Max: 3323 Sum: 2958657 Ratio: 99.99%)
|
||
|
|
Bounded : 44 (Average: 8.18 Max: 32 Sum: 360 Ratio: 0.01%)
|
||
|
|
|
||
|
|
Rules : 581162
|
||
|
|
Atoms : 581162
|
||
|
|
Bodies : 1 (Original: 0)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 1048604 (Eliminated: 0 Frozen: 59678)
|
||
|
|
Constraints : 7426627 (Binary: 98.5% Ternary: 0.7% Other: 0.8%)
|
||
|
|
|
||
|
|
Memory Peak : 1599MB
|
||
|
|
Max. Length : 30 steps
|
||
|
|
Models : 0
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 22.68s
|
||
|
|
Memory: 1515MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 22.76s
|
||
|
|
|
||
|
|
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 : 1+
|
||
|
|
Calls : 12
|
||
|
|
Time : 172.543s (Solving: 132.13s 1st Model: 9.27s Unsat: 0.00s)
|
||
|
|
CPU Time : 171.336s
|
||
|
|
|
||
|
|
Choices : 4180360 (Domain: 4179812)
|
||
|
|
Conflicts : 98678 (Analyzed: 98678)
|
||
|
|
Restarts : 928 (Average: 106.33 Last: 192)
|
||
|
|
Model-Level : 4287.0
|
||
|
|
Problems : 12 (Average Length: 23.25 Splits: 0)
|
||
|
|
Lemmas : 98678 (Deleted: 85335)
|
||
|
|
Binary : 1229 (Ratio: 1.25%)
|
||
|
|
Ternary : 762 (Ratio: 0.77%)
|
||
|
|
Conflict : 98678 (Average Length: 1544.3 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 98678 (Average: 34.07 Max: 7166 Sum: 3361478)
|
||
|
|
Executed : 98634 (Average: 34.06 Max: 7166 Sum: 3361118 Ratio: 99.99%)
|
||
|
|
Bounded : 44 (Average: 8.18 Max: 32 Sum: 360 Ratio: 0.01%)
|
||
|
|
|
||
|
|
Rules : 581162
|
||
|
|
Atoms : 581162
|
||
|
|
Bodies : 1 (Original: 0)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 1048604 (Eliminated: 0 Frozen: 59678)
|
||
|
|
Constraints : 7426591 (Binary: 98.5% Ternary: 0.7% Other: 0.8%)
|
||
|
|
|
||
|
|
Memory Peak : 1599MB
|
||
|
|
Max. Length : 30 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 9.53s
|
||
|
|
Memory: 1515MB (+0MB)
|
||
|
|
SAT
|
||
|
|
Testing...
|
||
|
|
NOT SERIALIZABLE
|
||
|
|
Testing Time: 14.66s
|
||
|
|
Memory: 1846MB (+331MB)
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 13
|
||
|
|
Time : 267.743s (Solving: 217.74s 1st Model: 9.27s Unsat: 0.00s)
|
||
|
|
CPU Time : 266.576s
|
||
|
|
|
||
|
|
Choices : 6063122 (Domain: 6062574)
|
||
|
|
Conflicts : 108832 (Analyzed: 108832)
|
||
|
|
Restarts : 1028 (Average: 105.87 Last: 192)
|
||
|
|
Model-Level : 4287.0
|
||
|
|
Problems : 13 (Average Length: 23.92 Splits: 0)
|
||
|
|
Lemmas : 108832 (Deleted: 93969)
|
||
|
|
Binary : 1300 (Ratio: 1.19%)
|
||
|
|
Ternary : 842 (Ratio: 0.77%)
|
||
|
|
Conflict : 108832 (Average Length: 1485.9 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 108832 (Average: 47.52 Max: 7166 Sum: 5171433)
|
||
|
|
Executed : 108699 (Average: 47.49 Max: 7166 Sum: 5168225 Ratio: 99.94%)
|
||
|
|
Bounded : 133 (Average: 24.12 Max: 32 Sum: 3208 Ratio: 0.06%)
|
||
|
|
|
||
|
|
Rules : 3071167 (Original: 3071165)
|
||
|
|
Atoms : 648105
|
||
|
|
Bodies : 1625812 (Original: 1625809)
|
||
|
|
Count : 1603 (Original: 1604)
|
||
|
|
Equivalences : 823565 (Atom=Atom: 39 Body=Body: 0 Other: 823526)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 1051873 (Eliminated: 0 Frozen: 883100)
|
||
|
|
Constraints : 9854658 (Binary: 98.8% Ternary: 0.5% Other: 0.6%)
|
||
|
|
|
||
|
|
Memory Peak : 1846MB
|
||
|
|
Max. Length : 30 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 87.33s
|
||
|
|
Memory: 1730MB (+-116MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 111.60s
|
||
|
|
|
||
|
|
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: 2023.0MB
|
||
|
|
Grounding... [('step', [31]), ('step', [32]), ('step', [33]), ('step', [34]), ('step', [35]), ('check', [35])]
|
||
|
|
Grounding Time: 5.14s
|
||
|
|
Memory: 1817MB (+87MB)
|
||
|
|
Unblocking actions...
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 14
|
||
|
|
Time : 323.038s (Solving: 265.55s 1st Model: 9.27s Unsat: 0.00s)
|
||
|
|
CPU Time : 321.896s
|
||
|
|
|
||
|
|
Choices : 7771596 (Domain: 7771048)
|
||
|
|
Conflicts : 118429 (Analyzed: 118429)
|
||
|
|
Restarts : 1128 (Average: 104.99 Last: 192)
|
||
|
|
Model-Level : 4287.0
|
||
|
|
Problems : 14 (Average Length: 24.86 Splits: 0)
|
||
|
|
Lemmas : 118429 (Deleted: 103770)
|
||
|
|
Binary : 1427 (Ratio: 1.20%)
|
||
|
|
Ternary : 879 (Ratio: 0.74%)
|
||
|
|
Conflict : 118429 (Average Length: 1425.5 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 118429 (Average: 57.18 Max: 7166 Sum: 6771785)
|
||
|
|
Executed : 118135 (Average: 57.10 Max: 7166 Sum: 6762620 Ratio: 99.86%)
|
||
|
|
Bounded : 294 (Average: 31.17 Max: 37 Sum: 9165 Ratio: 0.14%)
|
||
|
|
|
||
|
|
Rules : 3071167 (Original: 3071165)
|
||
|
|
Atoms : 648105
|
||
|
|
Bodies : 1625812 (Original: 1625809)
|
||
|
|
Count : 1603 (Original: 1604)
|
||
|
|
Equivalences : 823565 (Atom=Atom: 39 Body=Body: 0 Other: 823526)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 1234044 (Eliminated: 0 Frozen: 1054160)
|
||
|
|
Constraints : 11766848 (Binary: 98.8% Ternary: 0.5% Other: 0.6%)
|
||
|
|
|
||
|
|
Memory Peak : 2107MB
|
||
|
|
Max. Length : 30 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 48.11s
|
||
|
|
Memory: 2081MB (+264MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 55.33s
|
||
|
|
|
||
|
|
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: 2432.0MB
|
||
|
|
Grounding... [('step', [36]), ('step', [37]), ('step', [38]), ('step', [39]), ('step', [40]), ('check', [40])]
|
||
|
|
Grounding Time: 5.29s
|
||
|
|
Memory: 2081MB (+0MB)
|
||
|
|
Unblocking actions...
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 15
|
||
|
|
Time : 394.130s (Solving: 328.82s 1st Model: 9.27s Unsat: 0.00s)
|
||
|
|
CPU Time : 393.016s
|
||
|
|
|
||
|
|
Choices : 9908378 (Domain: 9907830)
|
||
|
|
Conflicts : 128678 (Analyzed: 128678)
|
||
|
|
Restarts : 1228 (Average: 104.79 Last: 192)
|
||
|
|
Model-Level : 4287.0
|
||
|
|
Problems : 15 (Average Length: 26.00 Splits: 0)
|
||
|
|
Lemmas : 128678 (Deleted: 112759)
|
||
|
|
Binary : 1522 (Ratio: 1.18%)
|
||
|
|
Ternary : 952 (Ratio: 0.74%)
|
||
|
|
Conflict : 128678 (Average Length: 1365.5 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 128678 (Average: 68.23 Max: 7166 Sum: 8780324)
|
||
|
|
Executed : 128312 (Average: 68.14 Max: 7166 Sum: 8768135 Ratio: 99.86%)
|
||
|
|
Bounded : 366 (Average: 33.30 Max: 42 Sum: 12189 Ratio: 0.14%)
|
||
|
|
|
||
|
|
Rules : 3071167 (Original: 3071165)
|
||
|
|
Atoms : 648105
|
||
|
|
Bodies : 1625812 (Original: 1625809)
|
||
|
|
Count : 1603 (Original: 1604)
|
||
|
|
Equivalences : 823565 (Atom=Atom: 39 Body=Body: 0 Other: 823526)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 1416215 (Eliminated: 0 Frozen: 1225220)
|
||
|
|
Constraints : 13524310 (Binary: 98.8% Ternary: 0.5% Other: 0.6%)
|
||
|
|
|
||
|
|
Memory Peak : 2254MB
|
||
|
|
Max. Length : 35 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 63.59s
|
||
|
|
Memory: 2140MB (+59MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 71.13s
|
||
|
|
|
||
|
|
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: 2491.0MB
|
||
|
|
Grounding... [('step', [41]), ('step', [42]), ('step', [43]), ('step', [44]), ('step', [45]), ('check', [45])]
|
||
|
|
Grounding Time: 5.28s
|
||
|
|
Memory: 2200MB (+60MB)
|
||
|
|
Unblocking actions...
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 16
|
||
|
|
Time : 464.508s (Solving: 391.36s 1st Model: 9.27s Unsat: 0.00s)
|
||
|
|
CPU Time : 463.428s
|
||
|
|
|
||
|
|
Choices : 11952988 (Domain: 11952440)
|
||
|
|
Conflicts : 138296 (Analyzed: 138296)
|
||
|
|
Restarts : 1328 (Average: 104.14 Last: 192)
|
||
|
|
Model-Level : 4287.0
|
||
|
|
Problems : 16 (Average Length: 27.31 Splits: 0)
|
||
|
|
Lemmas : 138296 (Deleted: 122473)
|
||
|
|
Binary : 1590 (Ratio: 1.15%)
|
||
|
|
Ternary : 987 (Ratio: 0.71%)
|
||
|
|
Conflict : 138296 (Average Length: 1299.1 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 138296 (Average: 77.20 Max: 7204 Sum: 10676966)
|
||
|
|
Executed : 137881 (Average: 77.10 Max: 7204 Sum: 10662474 Ratio: 99.86%)
|
||
|
|
Bounded : 415 (Average: 34.92 Max: 47 Sum: 14492 Ratio: 0.14%)
|
||
|
|
|
||
|
|
Rules : 3071167 (Original: 3071165)
|
||
|
|
Atoms : 648105
|
||
|
|
Bodies : 1625812 (Original: 1625809)
|
||
|
|
Count : 1603 (Original: 1604)
|
||
|
|
Equivalences : 823565 (Atom=Atom: 39 Body=Body: 0 Other: 823526)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 1598386 (Eliminated: 0 Frozen: 1396280)
|
||
|
|
Constraints : 15401714 (Binary: 98.8% Ternary: 0.5% Other: 0.6%)
|
||
|
|
|
||
|
|
Memory Peak : 2437MB
|
||
|
|
Max. Length : 40 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 62.90s
|
||
|
|
Memory: 2302MB (+102MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 70.42s
|
||
|
|
|
||
|
|
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: 2653.0MB
|
||
|
|
Grounding... [('step', [46]), ('step', [47]), ('step', [48]), ('step', [49]), ('step', [50]), ('check', [50])]
|
||
|
|
Grounding Time: 6.50s
|
||
|
|
Memory: 2471MB (+169MB)
|
||
|
|
Unblocking actions...
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 17
|
||
|
|
Time : 546.985s (Solving: 464.60s 1st Model: 9.27s Unsat: 0.00s)
|
||
|
|
CPU Time : 545.940s
|
||
|
|
|
||
|
|
Choices : 14086942 (Domain: 14086394)
|
||
|
|
Conflicts : 147015 (Analyzed: 147015)
|
||
|
|
Restarts : 1428 (Average: 102.95 Last: 192)
|
||
|
|
Model-Level : 4287.0
|
||
|
|
Problems : 17 (Average Length: 28.76 Splits: 0)
|
||
|
|
Lemmas : 147015 (Deleted: 131466)
|
||
|
|
Binary : 1647 (Ratio: 1.12%)
|
||
|
|
Ternary : 1017 (Ratio: 0.69%)
|
||
|
|
Conflict : 147015 (Average Length: 1272.0 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 147015 (Average: 86.00 Max: 7476 Sum: 12642887)
|
||
|
|
Executed : 146583 (Average: 85.89 Max: 7476 Sum: 12627511 Ratio: 99.88%)
|
||
|
|
Bounded : 432 (Average: 35.59 Max: 52 Sum: 15376 Ratio: 0.12%)
|
||
|
|
|
||
|
|
Rules : 3071167 (Original: 3071165)
|
||
|
|
Atoms : 648105
|
||
|
|
Bodies : 1625812 (Original: 1625809)
|
||
|
|
Count : 1603 (Original: 1604)
|
||
|
|
Equivalences : 823565 (Atom=Atom: 39 Body=Body: 0 Other: 823526)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 1780557 (Eliminated: 0 Frozen: 1567340)
|
||
|
|
Constraints : 17260954 (Binary: 98.8% Ternary: 0.5% Other: 0.6%)
|
||
|
|
|
||
|
|
Memory Peak : 2728MB
|
||
|
|
Max. Length : 45 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 73.63s
|
||
|
|
Memory: 2638MB (+167MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 82.52s
|
||
|
|
|
||
|
|
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: 2989.0MB
|
||
|
|
Grounding... [('step', [51]), ('step', [52]), ('step', [53]), ('step', [54]), ('step', [55]), ('check', [55])]
|
||
|
|
Grounding Time: 5.01s
|
||
|
|
Memory: 2700MB (+62MB)
|
||
|
|
Unblocking actions...
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 18
|
||
|
|
Time : 635.143s (Solving: 545.03s 1st Model: 9.27s Unsat: 0.00s)
|
||
|
|
CPU Time : 634.136s
|
||
|
|
|
||
|
|
Choices : 15960297 (Domain: 15959749)
|
||
|
|
Conflicts : 156342 (Analyzed: 156342)
|
||
|
|
Restarts : 1528 (Average: 102.32 Last: 192)
|
||
|
|
Model-Level : 4287.0
|
||
|
|
Problems : 18 (Average Length: 30.33 Splits: 0)
|
||
|
|
Lemmas : 156342 (Deleted: 139765)
|
||
|
|
Binary : 1732 (Ratio: 1.11%)
|
||
|
|
Ternary : 1073 (Ratio: 0.69%)
|
||
|
|
Conflict : 156342 (Average Length: 1246.3 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 156342 (Average: 92.38 Max: 7476 Sum: 14442399)
|
||
|
|
Executed : 155900 (Average: 92.27 Max: 7476 Sum: 14426453 Ratio: 99.89%)
|
||
|
|
Bounded : 442 (Average: 36.08 Max: 57 Sum: 15946 Ratio: 0.11%)
|
||
|
|
|
||
|
|
Rules : 3071167 (Original: 3071165)
|
||
|
|
Atoms : 648105
|
||
|
|
Bodies : 1625812 (Original: 1625809)
|
||
|
|
Count : 1603 (Original: 1604)
|
||
|
|
Equivalences : 823565 (Atom=Atom: 39 Body=Body: 0 Other: 823526)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 1962728 (Eliminated: 0 Frozen: 1738400)
|
||
|
|
Constraints : 19181824 (Binary: 98.8% Ternary: 0.5% Other: 0.6%)
|
||
|
|
|
||
|
|
Memory Peak : 2999MB
|
||
|
|
Max. Length : 50 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 80.86s
|
||
|
|
Memory: 2840MB (+140MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 88.20s
|
||
|
|
|
||
|
|
Iteration 18
|
||
|
|
Queue: [(12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True)]
|
||
|
|
Grounded Until: 55
|
||
|
|
Expected Memory: 3191.0MB
|
||
|
|
Grounding... [('step', [56]), ('step', [57]), ('step', [58]), ('step', [59]), ('step', [60]), ('check', [60])]
|
||
|
|
Grounding Time: 5.06s
|
||
|
|
Memory: 2871MB (+31MB)
|
||
|
|
Unblocking actions...
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 19
|
||
|
|
Time : 715.804s (Solving: 617.82s 1st Model: 9.27s Unsat: 0.00s)
|
||
|
|
CPU Time : 714.832s
|
||
|
|
|
||
|
|
Choices : 18734908 (Domain: 18734360)
|
||
|
|
Conflicts : 165735 (Analyzed: 165735)
|
||
|
|
Restarts : 1628 (Average: 101.80 Last: 192)
|
||
|
|
Model-Level : 4287.0
|
||
|
|
Problems : 19 (Average Length: 32.00 Splits: 0)
|
||
|
|
Lemmas : 165735 (Deleted: 148729)
|
||
|
|
Binary : 1809 (Ratio: 1.09%)
|
||
|
|
Ternary : 1103 (Ratio: 0.67%)
|
||
|
|
Conflict : 165735 (Average Length: 1193.0 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 165735 (Average: 102.66 Max: 7476 Sum: 17014006)
|
||
|
|
Executed : 165274 (Average: 102.55 Max: 7476 Sum: 16996882 Ratio: 99.90%)
|
||
|
|
Bounded : 461 (Average: 37.15 Max: 62 Sum: 17124 Ratio: 0.10%)
|
||
|
|
|
||
|
|
Rules : 3071167 (Original: 3071165)
|
||
|
|
Atoms : 648105
|
||
|
|
Bodies : 1625812 (Original: 1625809)
|
||
|
|
Count : 1603 (Original: 1604)
|
||
|
|
Equivalences : 823565 (Atom=Atom: 39 Body=Body: 0 Other: 823526)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 2144899 (Eliminated: 0 Frozen: 1909460)
|
||
|
|
Constraints : 21107500 (Binary: 98.8% Ternary: 0.5% Other: 0.6%)
|
||
|
|
|
||
|
|
Memory Peak : 3181MB
|
||
|
|
Max. Length : 55 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 73.24s
|
||
|
|
Memory: 2995MB (+124MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 80.70s
|
||
|
|
|
||
|
|
Iteration 19
|
||
|
|
Queue: [(13,65,0,True), (14,70,0,True), (15,75,0,True)]
|
||
|
|
Grounded Until: 60
|
||
|
|
Expected Memory: 3346.0MB
|
||
|
|
Grounding... [('step', [61]), ('step', [62]), ('step', [63]), ('step', [64]), ('step', [65]), ('check', [65])]
|
||
|
|
Grounding Time: 5.14s
|
||
|
|
Memory: 3053MB (+58MB)
|
||
|
|
Unblocking actions...
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 20
|
||
|
|
Time : 835.237s (Solving: 729.19s 1st Model: 9.27s Unsat: 0.00s)
|
||
|
|
CPU Time : 834.316s
|
||
|
|
|
||
|
|
Choices : 21710675 (Domain: 21710127)
|
||
|
|
Conflicts : 174802 (Analyzed: 174802)
|
||
|
|
Restarts : 1728 (Average: 101.16 Last: 192)
|
||
|
|
Model-Level : 4287.0
|
||
|
|
Problems : 20 (Average Length: 33.75 Splits: 0)
|
||
|
|
Lemmas : 174802 (Deleted: 157540)
|
||
|
|
Binary : 1889 (Ratio: 1.08%)
|
||
|
|
Ternary : 1123 (Ratio: 0.64%)
|
||
|
|
Conflict : 174802 (Average Length: 1154.0 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 174802 (Average: 113.99 Max: 10085 Sum: 19924963)
|
||
|
|
Executed : 174333 (Average: 113.88 Max: 10085 Sum: 19907303 Ratio: 99.91%)
|
||
|
|
Bounded : 469 (Average: 37.65 Max: 67 Sum: 17660 Ratio: 0.09%)
|
||
|
|
|
||
|
|
Rules : 3071167 (Original: 3071165)
|
||
|
|
Atoms : 648105
|
||
|
|
Bodies : 1625812 (Original: 1625809)
|
||
|
|
Count : 1603 (Original: 1604)
|
||
|
|
Equivalences : 823565 (Atom=Atom: 39 Body=Body: 0 Other: 823526)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 2327070 (Eliminated: 0 Frozen: 2080520)
|
||
|
|
Constraints : 23020001 (Binary: 98.8% Ternary: 0.5% Other: 0.6%)
|
||
|
|
|
||
|
|
Memory Peak : 3385MB
|
||
|
|
Max. Length : 60 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 111.86s
|
||
|
|
Memory: 3177MB (+124MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 119.49s
|
||
|
|
|
||
|
|
Iteration 20
|
||
|
|
Queue: [(14,70,0,True), (15,75,0,True)]
|
||
|
|
Grounded Until: 65
|
||
|
|
Expected Memory: 3528.0MB
|
||
|
|
Grounding... [('step', [66]), ('step', [67]), ('step', [68]), ('step', [69]), ('step', [70]), ('check', [70])]
|
||
|
|
Grounding Time: 5.19s
|
||
|
|
Memory: 3248MB (+71MB)
|
||
|
|
Unblocking actions...
|
||
|
|
Solving...
|
||
|
|
*** Info : (planner): INTERRUPTED by signal!
|
||
|
|
UNKNOWN
|
||
|
|
|
||
|
|
INTERRUPTED : 1
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 21
|
||
|
|
Time : 996.403s (Solving: 882.14s 1st Model: 9.27s Unsat: 0.00s)
|
||
|
|
CPU Time : 995.532s
|
||
|
|
|
||
|
|
Choices : 25173436 (Domain: 25172888)
|
||
|
|
Conflicts : 184331 (Analyzed: 184331)
|
||
|
|
Restarts : 1828 (Average: 100.84 Last: 192)
|
||
|
|
Model-Level : 4287.0
|
||
|
|
Problems : 21 (Average Length: 35.57 Splits: 0)
|
||
|
|
Lemmas : 184331 (Deleted: 166222)
|
||
|
|
Binary : 1921 (Ratio: 1.04%)
|
||
|
|
Ternary : 1154 (Ratio: 0.63%)
|
||
|
|
Conflict : 184331 (Average Length: 1175.7 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 184331 (Average: 125.90 Max: 11043 Sum: 23207860)
|
||
|
|
Executed : 183857 (Average: 125.81 Max: 11043 Sum: 23189840 Ratio: 99.92%)
|
||
|
|
Bounded : 474 (Average: 38.02 Max: 72 Sum: 18020 Ratio: 0.08%)
|
||
|
|
|
||
|
|
Rules : 3071167 (Original: 3071165)
|
||
|
|
Atoms : 648105
|
||
|
|
Bodies : 1625812 (Original: 1625809)
|
||
|
|
Count : 1603 (Original: 1604)
|
||
|
|
Equivalences : 823565 (Atom=Atom: 39 Body=Body: 0 Other: 823526)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 2509241 (Eliminated: 0 Frozen: 2251580)
|
||
|
|
Constraints : 24945752 (Binary: 98.8% Ternary: 0.5% Other: 0.6%)
|
||
|
|
|
||
|
|
Memory Peak : 3607MB
|
||
|
|
Max. Length : 65 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
|