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