INFO Running translator. INFO translator input: ['/home/pluehne/Documents/ASP/pddl-instances/ipc-2011/domains/barman-sequential-satisficing/domain.pddl', '/home/pluehne/Documents/ASP/pddl-instances/ipc-2011/domains/barman-sequential-satisficing/instances/instance-2.pddl'] INFO translator arguments: [] INFO translator time limit: None INFO translator memory limit: None INFO callstring: /home/pluehne/.usr/bin/python /home/wv/bin/linux/64/fast-downward-10997/builds/release64/bin/translate/translate.py /home/pluehne/Documents/ASP/pddl-instances/ipc-2011/domains/barman-sequential-satisficing/domain.pddl /home/pluehne/Documents/ASP/pddl-instances/ipc-2011/domains/barman-sequential-satisficing/instances/instance-2.pddl Parsing... Parsing: [0.040s CPU, 0.045s wall-clock] Normalizing task... [0.010s CPU, 0.003s wall-clock] Instantiating... Generating Datalog program... [0.000s CPU, 0.011s wall-clock] Normalizing Datalog program... Normalizing Datalog program: [0.060s CPU, 0.053s wall-clock] Preparing model... [0.020s CPU, 0.027s wall-clock] Generated 115 rules. Computing model... [0.340s CPU, 0.335s wall-clock] 2025 relevant atoms 2105 auxiliary atoms 4130 final queue length 7122 total queue pushes Completing instantiation... [0.600s CPU, 0.598s wall-clock] Instantiating: [1.020s CPU, 1.030s wall-clock] Computing fact groups... Finding invariants... 24 initial candidates Finding invariants: [0.110s CPU, 0.109s wall-clock] Checking invariant weight... [0.000s CPU, 0.001s wall-clock] Instantiating groups... [0.010s CPU, 0.006s wall-clock] Collecting mutex groups... [0.000s CPU, 0.000s wall-clock] Choosing groups... 207 uncovered facts Choosing groups: [0.000s CPU, 0.001s wall-clock] Building translation key... [0.010s CPU, 0.008s wall-clock] Computing fact groups: [0.140s CPU, 0.142s wall-clock] Building STRIPS to SAS dictionary... [0.000s CPU, 0.002s wall-clock] Building dictionary for full mutex groups... [0.000s CPU, 0.002s wall-clock] Building mutex information... Building mutex information: [0.010s CPU, 0.002s wall-clock] Translating task... Processing axioms... Simplifying axioms... [0.000s CPU, 0.000s wall-clock] Processing axioms: [0.030s CPU, 0.033s wall-clock] Translating task: [0.650s CPU, 0.655s wall-clock] 2326 effect conditions simplified 0 implied preconditions added Detecting unreachable propositions... 0 operators removed 0 axioms removed 3 propositions removed Detecting unreachable propositions: [0.310s CPU, 0.308s wall-clock] Reordering and filtering variables... 210 of 210 variables necessary. 11 of 14 mutex groups necessary. 1390 of 1390 operators necessary. 0 of 0 axiom rules necessary. Reordering and filtering variables: [0.210s CPU, 0.206s wall-clock] Translator variables: 210 Translator derived variables: 0 Translator facts: 441 Translator goal facts: 9 Translator mutex groups: 11 Translator total mutex groups size: 33 Translator operators: 1390 Translator axioms: 0 Translator task size: 13333 Translator peak memory: 43980 KB Writing output... [0.260s CPU, 0.275s wall-clock] Done! [2.670s CPU, 2.696s wall-clock] planner.py version 0.0.1 Time: 0.56s Memory: 86MB Iteration 1 Queue: [(0,0,0,True), (1,5,0,True), (2,10,0,True), (3,15,0,True), (4,20,0,True), (5,25,0,True), (6,30,0,True)] Grounded Until: 0 Solving... [start: stats after solve call] Models : 0 Calls : 1 Time : 0.654s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s) CPU Time : 0.560s 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 : 38518 Atoms : 38518 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 : 222MB Max. Length : 0 steps Models : 0 [endof: stats after solve call] Solving Time: 0.00s Memory: 158MB (+72MB) UNSAT Iteration Time: 0.00s 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: 158MB Grounding... [('step', [1]), ('step', [2]), ('step', [3]), ('step', [4]), ('step', [5]), ('check', [5])] Grounding Time: 0.15s Memory: 158MB (+0MB) Unblocking actions... Solving... [start: stats after solve call] Models : 1+ Calls : 2 Time : 0.980s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s) CPU Time : 0.884s Choices : 152 (Domain: 73) Conflicts : 2 (Analyzed: 2) Restarts : 0 Model-Level : 147.0 Problems : 2 (Average Length: 4.50 Splits: 0) Lemmas : 2 (Deleted: 0) Binary : 0 (Ratio: 0.00%) Ternary : 0 (Ratio: 0.00%) Conflict : 2 (Average Length: 23.0 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 2 (Average: 6.00 Max: 11 Sum: 12) Executed : 2 (Average: 6.00 Max: 11 Sum: 12 Ratio: 100.00%) Bounded : 0 (Average: 0.00 Max: 0 Sum: 0 Ratio: 0.00%) Rules : 38518 Atoms : 38518 Bodies : 1 (Original: 0) Tight : Yes Variables : 10322 (Eliminated: 0 Frozen: 10322) Constraints : 36431 (Binary: 95.0% Ternary: 3.5% Other: 1.5%) Memory Peak : 222MB Max. Length : 0 steps Models : 1 [endof: stats after solve call] Solving Time: 0.10s Memory: 160MB (+2MB) SAT Testing... NOT SERIALIZABLE Testing Time: 0.62s Memory: 178MB (+18MB) Solving... [start: stats after solve call] Models : 0 Calls : 3 Time : 1.079s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s) CPU Time : 0.984s Choices : 161 (Domain: 78) Conflicts : 9 (Analyzed: 8) Restarts : 0 Model-Level : 147.0 Problems : 3 (Average Length: 5.33 Splits: 0) Lemmas : 8 (Deleted: 0) Binary : 1 (Ratio: 12.50%) Ternary : 2 (Ratio: 25.00%) Conflict : 8 (Average Length: 8.4 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 8 (Average: 2.75 Max: 11 Sum: 22) Executed : 7 (Average: 2.62 Max: 11 Sum: 21 Ratio: 95.45%) Bounded : 1 (Average: 1.00 Max: 1 Sum: 1 Ratio: 4.55%) Rules : 55133 (Original: 53913) Atoms : 43853 Bodies : 10280 (Original: 9059) Count : 232 (Original: 476) Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) Tight : Yes Variables : 12735 (Eliminated: 1464 Frozen: 11271) Constraints : 50631 (Binary: 90.2% Ternary: 5.9% Other: 3.9%) Memory Peak : 222MB Max. Length : 0 steps Models : 1 [endof: stats after solve call] Solving Time: 0.03s Memory: 178MB (+0MB) UNSAT Iteration Time: 0.97s 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: 180.0MB Grounding... [('step', [6]), ('step', [7]), ('step', [8]), ('step', [9]), ('step', [10]), ('check', [10])] Grounding Time: 0.29s Memory: 178MB (+0MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0 Calls : 4 Time : 2.238s (Solving: 0.46s 1st Model: 0.00s Unsat: 0.46s) CPU Time : 2.144s Choices : 16216 (Domain: 12582) Conflicts : 1864 (Analyzed: 1862) Restarts : 6 (Average: 310.33 Last: 87) Model-Level : 147.0 Problems : 4 (Average Length: 7.00 Splits: 0) Lemmas : 1862 (Deleted: 0) Binary : 210 (Ratio: 11.28%) Ternary : 280 (Ratio: 15.04%) Conflict : 1862 (Average Length: 24.8 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 1862 (Average: 8.69 Max: 184 Sum: 16185) Executed : 1840 (Average: 8.57 Max: 184 Sum: 15954 Ratio: 98.57%) Bounded : 22 (Average: 10.50 Max: 12 Sum: 231 Ratio: 1.43%) Rules : 55133 (Original: 53913) Atoms : 43853 Bodies : 10280 (Original: 9059) Count : 232 (Original: 476) Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) Tight : Yes Variables : 35311 (Eliminated: 1464 Frozen: 26317) Constraints : 223676 (Binary: 91.3% Ternary: 6.4% Other: 2.3%) Memory Peak : 222MB Max. Length : 5 steps Models : 1 [endof: stats after solve call] Solving Time: 0.77s Memory: 189MB (+11MB) UNSAT Iteration Time: 1.16s Iteration 4 Queue: [(3,15,0,True), (4,20,0,True), (5,25,0,True), (6,30,0,True)] Grounded Until: 10 Expected Memory: 200.0MB Grounding... [('step', [11]), ('step', [12]), ('step', [13]), ('step', [14]), ('step', [15]), ('check', [15])] Grounding Time: 0.33s Memory: 195MB (+6MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0 Calls : 5 Time : 10.101s (Solving: 7.55s 1st Model: 0.00s Unsat: 7.55s) CPU Time : 10.008s Choices : 169527 (Domain: 131701) Conflicts : 25187 (Analyzed: 25184) Restarts : 64 (Average: 393.50 Last: 646) Model-Level : 147.0 Problems : 5 (Average Length: 9.00 Splits: 0) Lemmas : 25184 (Deleted: 13000) Binary : 1242 (Ratio: 4.93%) Ternary : 544 (Ratio: 2.16%) Conflict : 25184 (Average Length: 261.4 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 25184 (Average: 6.56 Max: 810 Sum: 165120) Executed : 25150 (Average: 6.54 Max: 810 Sum: 164701 Ratio: 99.75%) Bounded : 34 (Average: 12.32 Max: 17 Sum: 419 Ratio: 0.25%) Rules : 55133 (Original: 53913) Atoms : 43853 Bodies : 10280 (Original: 9059) Count : 232 (Original: 476) Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) Tight : Yes Variables : 57887 (Eliminated: 1464 Frozen: 48893) Constraints : 380813 (Binary: 91.5% Ternary: 6.3% Other: 2.1%) Memory Peak : 222MB Max. Length : 10 steps Models : 1 [endof: stats after solve call] Solving Time: 7.42s Memory: 209MB (+14MB) UNSAT Iteration Time: 7.87s Iteration 5 Queue: [(4,20,0,True), (5,25,0,True), (6,30,0,True)] Grounded Until: 15 Expected Memory: 229.0MB Grounding... [('step', [16]), ('step', [17]), ('step', [18]), ('step', [19]), ('step', [20]), ('check', [20])] Grounding Time: 0.30s Memory: 212MB (+3MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 6 Time : 22.348s (Solving: 19.03s 1st Model: 0.00s Unsat: 7.55s) CPU Time : 22.264s Choices : 374743 (Domain: 319885) Conflicts : 47955 (Analyzed: 47952) Restarts : 164 (Average: 292.39 Last: 646) Model-Level : 147.0 Problems : 6 (Average Length: 11.17 Splits: 0) Lemmas : 47952 (Deleted: 32192) Binary : 2387 (Ratio: 4.98%) Ternary : 898 (Ratio: 1.87%) Conflict : 47952 (Average Length: 334.7 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 47952 (Average: 7.49 Max: 810 Sum: 359221) Executed : 47918 (Average: 7.48 Max: 810 Sum: 358802 Ratio: 99.88%) Bounded : 34 (Average: 12.32 Max: 17 Sum: 419 Ratio: 0.12%) Rules : 55133 (Original: 53913) Atoms : 43853 Bodies : 10280 (Original: 9059) Count : 232 (Original: 476) Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) Tight : Yes Variables : 80463 (Eliminated: 1464 Frozen: 71469) Constraints : 538208 (Binary: 91.6% Ternary: 6.3% Other: 2.0%) Memory Peak : 227MB Max. Length : 15 steps Models : 1 [endof: stats after solve call] Solving Time: 11.82s Memory: 227MB (+15MB) UNKNOWN Iteration Time: 12.26s Iteration 6 Queue: [(5,25,0,True), (6,30,0,True)] Grounded Until: 20 Expected Memory: 247.0MB Grounding... [('step', [21]), ('step', [22]), ('step', [23]), ('step', [24]), ('step', [25]), ('check', [25])] Grounding Time: 0.31s Memory: 230MB (+3MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 7 Time : 80.558s (Solving: 76.46s 1st Model: 0.00s Unsat: 7.55s) CPU Time : 80.500s Choices : 815840 (Domain: 723921) Conflicts : 125928 (Analyzed: 125925) Restarts : 264 (Average: 476.99 Last: 715) Model-Level : 147.0 Problems : 7 (Average Length: 13.43 Splits: 0) Lemmas : 125925 (Deleted: 94595) Binary : 4155 (Ratio: 3.30%) Ternary : 1257 (Ratio: 1.00%) Conflict : 125925 (Average Length: 861.5 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 125925 (Average: 6.23 Max: 810 Sum: 784831) Executed : 125890 (Average: 6.23 Max: 810 Sum: 784385 Ratio: 99.94%) Bounded : 35 (Average: 12.74 Max: 27 Sum: 446 Ratio: 0.06%) Rules : 55133 (Original: 53913) Atoms : 43853 Bodies : 10280 (Original: 9059) Count : 232 (Original: 476) Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) Tight : Yes Variables : 103039 (Eliminated: 1464 Frozen: 94045) Constraints : 711253 (Binary: 91.6% Ternary: 6.4% Other: 2.0%) Memory Peak : 434MB Max. Length : 20 steps Models : 1 [endof: stats after solve call] Solving Time: 57.78s Memory: 370MB (+140MB) UNKNOWN Iteration Time: 58.24s Iteration 7 Queue: [(6,30,0,True)] Grounded Until: 25 Expected Memory: 513.0MB Grounding... [('step', [26]), ('step', [27]), ('step', [28]), ('step', [29]), ('step', [30]), ('check', [30])] Grounding Time: 0.33s Memory: 372MB (+2MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 8 Time : 105.603s (Solving: 100.63s 1st Model: 0.00s Unsat: 7.55s) CPU Time : 105.556s Choices : 1076248 (Domain: 975350) Conflicts : 158464 (Analyzed: 158461) Restarts : 364 (Average: 435.33 Last: 715) Model-Level : 147.0 Problems : 8 (Average Length: 15.75 Splits: 0) Lemmas : 158461 (Deleted: 124965) Binary : 5202 (Ratio: 3.28%) Ternary : 1554 (Ratio: 0.98%) Conflict : 158461 (Average Length: 893.0 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 158461 (Average: 6.48 Max: 810 Sum: 1026131) Executed : 158426 (Average: 6.47 Max: 810 Sum: 1025685 Ratio: 99.96%) Bounded : 35 (Average: 12.74 Max: 27 Sum: 446 Ratio: 0.04%) Rules : 55133 (Original: 53913) Atoms : 43853 Bodies : 10280 (Original: 9059) Count : 232 (Original: 476) Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) Tight : Yes Variables : 125615 (Eliminated: 1464 Frozen: 116621) Constraints : 884284 (Binary: 91.6% Ternary: 6.4% Other: 2.0%) Memory Peak : 434MB Max. Length : 25 steps Models : 1 [endof: stats after solve call] Solving Time: 24.53s Memory: 390MB (+18MB) UNKNOWN Iteration Time: 25.06s Iteration 8 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), (16,80,0,True), (17,85,0,True)] Grounded Until: 30 Blocking actions... Solving... [start: stats after solve call] Models : 0 Calls : 9 Time : 117.385s (Solving: 112.37s 1st Model: 0.00s Unsat: 19.29s) CPU Time : 117.344s Choices : 1183703 (Domain: 1082805) Conflicts : 181734 (Analyzed: 181730) Restarts : 453 (Average: 401.17 Last: 2225) Model-Level : 147.0 Problems : 9 (Average Length: 17.56 Splits: 0) Lemmas : 181730 (Deleted: 156271) Binary : 5462 (Ratio: 3.01%) Ternary : 1596 (Ratio: 0.88%) Conflict : 181730 (Average Length: 832.0 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 181730 (Average: 6.20 Max: 810 Sum: 1126824) Executed : 181693 (Average: 6.20 Max: 810 Sum: 1126345 Ratio: 99.96%) Bounded : 37 (Average: 12.95 Max: 32 Sum: 479 Ratio: 0.04%) Rules : 55133 (Original: 53913) Atoms : 43853 Bodies : 10280 (Original: 9059) Count : 232 (Original: 476) Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) Tight : Yes Variables : 125615 (Eliminated: 1464 Frozen: 124151) Constraints : 884284 (Binary: 91.6% Ternary: 6.4% Other: 2.0%) Memory Peak : 434MB Max. Length : 30 steps Models : 1 [endof: stats after solve call] Solving Time: 11.76s Memory: 390MB (+0MB) UNSAT Iteration Time: 11.79s Iteration 9 Queue: [(5,25,1,True), (6,30,1,True), (7,35,0,True), (8,40,0,True), (9,45,0,True), (10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True), (17,85,0,True)] Grounded Until: 30 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 10 Time : 215.633s (Solving: 210.58s 1st Model: 0.00s Unsat: 19.29s) CPU Time : 215.632s Choices : 1445562 (Domain: 1343837) Conflicts : 271751 (Analyzed: 271747) Restarts : 553 (Average: 491.41 Last: 2225) Model-Level : 147.0 Problems : 10 (Average Length: 19.00 Splits: 0) Lemmas : 271747 (Deleted: 225148) Binary : 5774 (Ratio: 2.12%) Ternary : 1677 (Ratio: 0.62%) Conflict : 271747 (Average Length: 1005.5 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 271747 (Average: 5.06 Max: 810 Sum: 1375959) Executed : 271710 (Average: 5.06 Max: 810 Sum: 1375480 Ratio: 99.97%) Bounded : 37 (Average: 12.95 Max: 32 Sum: 479 Ratio: 0.03%) Rules : 55133 (Original: 53913) Atoms : 43853 Bodies : 10280 (Original: 9059) Count : 232 (Original: 476) Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) Tight : Yes Variables : 125615 (Eliminated: 1464 Frozen: 124151) Constraints : 884270 (Binary: 91.6% Ternary: 6.4% Other: 2.0%) Memory Peak : 434MB Max. Length : 30 steps Models : 1 [endof: stats after solve call] Solving Time: 98.28s Memory: 390MB (+0MB) UNKNOWN Iteration Time: 98.29s Iteration 10 Queue: [(6,30,1,True), (7,35,0,True), (8,40,0,True), (9,45,0,True), (10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True), (17,85,0,True)] Grounded Until: 30 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 11 Time : 246.089s (Solving: 240.98s 1st Model: 0.00s Unsat: 19.29s) CPU Time : 246.100s Choices : 1735384 (Domain: 1628814) Conflicts : 312268 (Analyzed: 312264) Restarts : 653 (Average: 478.20 Last: 2225) Model-Level : 147.0 Problems : 11 (Average Length: 20.18 Splits: 0) Lemmas : 312264 (Deleted: 280698) Binary : 6447 (Ratio: 2.06%) Ternary : 1812 (Ratio: 0.58%) Conflict : 312264 (Average Length: 1009.1 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 312264 (Average: 5.27 Max: 810 Sum: 1646666) Executed : 312227 (Average: 5.27 Max: 810 Sum: 1646187 Ratio: 99.97%) Bounded : 37 (Average: 12.95 Max: 32 Sum: 479 Ratio: 0.03%) Rules : 55133 (Original: 53913) Atoms : 43853 Bodies : 10280 (Original: 9059) Count : 232 (Original: 476) Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) Tight : Yes Variables : 125615 (Eliminated: 1464 Frozen: 124151) Constraints : 884270 (Binary: 91.6% Ternary: 6.4% Other: 2.0%) Memory Peak : 454MB Max. Length : 30 steps Models : 1 [endof: stats after solve call] Solving Time: 30.43s Memory: 454MB (+64MB) UNKNOWN Iteration Time: 30.47s Iteration 11 Queue: [(7,35,0,True), (8,40,0,True), (9,45,0,True), (10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True), (17,85,0,True)] Grounded Until: 30 Expected Memory: 597.0MB Grounding... [('step', [31]), ('step', [32]), ('step', [33]), ('step', [34]), ('step', [35]), ('check', [35])] Grounding Time: 0.38s Memory: 455MB (+1MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 12 Time : 285.188s (Solving: 279.16s 1st Model: 0.00s Unsat: 19.29s) CPU Time : 285.216s Choices : 2020824 (Domain: 1901625) Conflicts : 365309 (Analyzed: 365305) Restarts : 753 (Average: 485.13 Last: 2225) Model-Level : 147.0 Problems : 12 (Average Length: 21.58 Splits: 0) Lemmas : 365305 (Deleted: 336429) Binary : 7448 (Ratio: 2.04%) Ternary : 1978 (Ratio: 0.54%) Conflict : 365305 (Average Length: 1025.4 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 365305 (Average: 5.24 Max: 810 Sum: 1912959) Executed : 365268 (Average: 5.24 Max: 810 Sum: 1912480 Ratio: 99.97%) Bounded : 37 (Average: 12.95 Max: 32 Sum: 479 Ratio: 0.03%) Rules : 55133 (Original: 53913) Atoms : 43853 Bodies : 10280 (Original: 9059) Count : 232 (Original: 476) Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) Tight : Yes Variables : 148191 (Eliminated: 1464 Frozen: 139197) Constraints : 1057315 (Binary: 91.6% Ternary: 6.4% Other: 2.0%) Memory Peak : 476MB Max. Length : 30 steps Models : 1 [endof: stats after solve call] Solving Time: 38.55s Memory: 469MB (+14MB) UNKNOWN Iteration Time: 39.12s Iteration 12 Queue: [(8,40,0,True), (9,45,0,True), (10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True), (17,85,0,True)] Grounded Until: 35 Expected Memory: 612.0MB Grounding... [('step', [36]), ('step', [37]), ('step', [38]), ('step', [39]), ('step', [40]), ('check', [40])] Grounding Time: 0.40s Memory: 476MB (+7MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 13 Time : 312.484s (Solving: 305.51s 1st Model: 0.00s Unsat: 19.29s) CPU Time : 312.524s Choices : 2324390 (Domain: 2192754) Conflicts : 406897 (Analyzed: 406893) Restarts : 853 (Average: 477.01 Last: 2225) Model-Level : 147.0 Problems : 13 (Average Length: 23.15 Splits: 0) Lemmas : 406893 (Deleted: 373689) Binary : 8553 (Ratio: 2.10%) Ternary : 2158 (Ratio: 0.53%) Conflict : 406893 (Average Length: 1003.8 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 406893 (Average: 5.39 Max: 810 Sum: 2194438) Executed : 406856 (Average: 5.39 Max: 810 Sum: 2193959 Ratio: 99.98%) Bounded : 37 (Average: 12.95 Max: 32 Sum: 479 Ratio: 0.02%) Rules : 55133 (Original: 53913) Atoms : 43853 Bodies : 10280 (Original: 9059) Count : 232 (Original: 476) Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) Tight : Yes Variables : 170767 (Eliminated: 1464 Frozen: 161773) Constraints : 1230360 (Binary: 91.6% Ternary: 6.4% Other: 2.0%) Memory Peak : 502MB Max. Length : 35 steps Models : 1 [endof: stats after solve call] Solving Time: 26.73s Memory: 490MB (+14MB) UNKNOWN Iteration Time: 27.32s Iteration 13 Queue: [(9,45,0,True), (10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True), (17,85,0,True)] Grounded Until: 40 Expected Memory: 633.0MB Grounding... [('step', [41]), ('step', [42]), ('step', [43]), ('step', [44]), ('step', [45]), ('check', [45])] Grounding Time: 0.34s Memory: 493MB (+3MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 14 Time : 370.087s (Solving: 362.23s 1st Model: 0.00s Unsat: 19.29s) CPU Time : 370.152s Choices : 3040085 (Domain: 2888738) Conflicts : 497748 (Analyzed: 497744) Restarts : 953 (Average: 522.29 Last: 2225) Model-Level : 147.0 Problems : 14 (Average Length: 24.86 Splits: 0) Lemmas : 497744 (Deleted: 460723) Binary : 11080 (Ratio: 2.23%) Ternary : 2479 (Ratio: 0.50%) Conflict : 497744 (Average Length: 973.4 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 497744 (Average: 5.80 Max: 810 Sum: 2884928) Executed : 497707 (Average: 5.80 Max: 810 Sum: 2884449 Ratio: 99.98%) Bounded : 37 (Average: 12.95 Max: 32 Sum: 479 Ratio: 0.02%) Rules : 55133 (Original: 53913) Atoms : 43853 Bodies : 10280 (Original: 9059) Count : 232 (Original: 476) Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) Tight : Yes Variables : 193343 (Eliminated: 1464 Frozen: 184349) Constraints : 1403405 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) Memory Peak : 519MB Max. Length : 40 steps Models : 1 [endof: stats after solve call] Solving Time: 57.09s Memory: 516MB (+23MB) UNKNOWN Iteration Time: 57.64s Iteration 14 Queue: [(10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True), (17,85,0,True)] Grounded Until: 45 Expected Memory: 659.0MB Grounding... [('step', [46]), ('step', [47]), ('step', [48]), ('step', [49]), ('step', [50]), ('check', [50])] Grounding Time: 0.33s Memory: 516MB (+0MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 15 Time : 409.616s (Solving: 400.86s 1st Model: 0.00s Unsat: 19.29s) CPU Time : 409.696s Choices : 3521524 (Domain: 3359301) Conflicts : 565727 (Analyzed: 565723) Restarts : 1053 (Average: 537.25 Last: 2225) Model-Level : 147.0 Problems : 15 (Average Length: 26.67 Splits: 0) Lemmas : 565723 (Deleted: 514457) Binary : 12917 (Ratio: 2.28%) Ternary : 2714 (Ratio: 0.48%) Conflict : 565723 (Average Length: 951.3 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 565723 (Average: 5.90 Max: 810 Sum: 3339149) Executed : 565686 (Average: 5.90 Max: 810 Sum: 3338670 Ratio: 99.99%) Bounded : 37 (Average: 12.95 Max: 32 Sum: 479 Ratio: 0.01%) Rules : 55133 (Original: 53913) Atoms : 43853 Bodies : 10280 (Original: 9059) Count : 232 (Original: 476) Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) Tight : Yes Variables : 215919 (Eliminated: 1464 Frozen: 206925) Constraints : 1576450 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) Memory Peak : 545MB Max. Length : 45 steps Models : 1 [endof: stats after solve call] Solving Time: 39.02s Memory: 529MB (+13MB) UNKNOWN Iteration Time: 39.55s Iteration 15 Queue: [(11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True), (17,85,0,True)] Grounded Until: 50 Expected Memory: 672.0MB Grounding... [('step', [51]), ('step', [52]), ('step', [53]), ('step', [54]), ('step', [55]), ('check', [55])] Grounding Time: 0.31s Memory: 529MB (+0MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 16 Time : 442.973s (Solving: 433.32s 1st Model: 0.00s Unsat: 19.29s) CPU Time : 443.068s Choices : 3985594 (Domain: 3807049) Conflicts : 620781 (Analyzed: 620777) Restarts : 1153 (Average: 538.40 Last: 2225) Model-Level : 147.0 Problems : 16 (Average Length: 28.56 Splits: 0) Lemmas : 620777 (Deleted: 578386) Binary : 14427 (Ratio: 2.32%) Ternary : 2968 (Ratio: 0.48%) Conflict : 620777 (Average Length: 930.6 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 620777 (Average: 6.08 Max: 810 Sum: 3775604) Executed : 620740 (Average: 6.08 Max: 810 Sum: 3775125 Ratio: 99.99%) Bounded : 37 (Average: 12.95 Max: 32 Sum: 479 Ratio: 0.01%) Rules : 55133 (Original: 53913) Atoms : 43853 Bodies : 10280 (Original: 9059) Count : 232 (Original: 476) Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) Tight : Yes Variables : 238495 (Eliminated: 1464 Frozen: 229501) Constraints : 1749495 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) Memory Peak : 563MB Max. Length : 50 steps Models : 1 [endof: stats after solve call] Solving Time: 32.84s Memory: 544MB (+15MB) UNKNOWN Iteration Time: 33.38s Iteration 16 Queue: [(12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True), (17,85,0,True)] Grounded Until: 55 Expected Memory: 687.0MB Grounding... [('step', [56]), ('step', [57]), ('step', [58]), ('step', [59]), ('step', [60]), ('check', [60])] Grounding Time: 0.32s Memory: 544MB (+0MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 17 Time : 492.674s (Solving: 482.12s 1st Model: 0.00s Unsat: 19.29s) CPU Time : 492.792s Choices : 4646244 (Domain: 4460949) Conflicts : 705016 (Analyzed: 705012) Restarts : 1253 (Average: 562.66 Last: 2225) Model-Level : 147.0 Problems : 17 (Average Length: 30.53 Splits: 0) Lemmas : 705012 (Deleted: 647271) Binary : 16178 (Ratio: 2.29%) Ternary : 3175 (Ratio: 0.45%) Conflict : 705012 (Average Length: 911.2 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 705012 (Average: 6.25 Max: 810 Sum: 4407725) Executed : 704974 (Average: 6.25 Max: 810 Sum: 4407184 Ratio: 99.99%) Bounded : 38 (Average: 14.24 Max: 62 Sum: 541 Ratio: 0.01%) Rules : 55133 (Original: 53913) Atoms : 43853 Bodies : 10280 (Original: 9059) Count : 232 (Original: 476) Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) Tight : Yes Variables : 261071 (Eliminated: 1464 Frozen: 252077) Constraints : 1922540 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) Memory Peak : 580MB Max. Length : 55 steps Models : 1 [endof: stats after solve call] Solving Time: 49.19s Memory: 559MB (+15MB) UNKNOWN Iteration Time: 49.73s Iteration 17 Queue: [(13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True), (17,85,0,True)] Grounded Until: 60 Expected Memory: 702.0MB Grounding... [('step', [61]), ('step', [62]), ('step', [63]), ('step', [64]), ('step', [65]), ('check', [65])] Grounding Time: 0.32s Memory: 559MB (+0MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 18 Time : 532.870s (Solving: 521.39s 1st Model: 0.00s Unsat: 19.29s) CPU Time : 533.008s Choices : 5219606 (Domain: 5022359) Conflicts : 779482 (Analyzed: 779478) Restarts : 1353 (Average: 576.11 Last: 2225) Model-Level : 147.0 Problems : 18 (Average Length: 32.56 Splits: 0) Lemmas : 779478 (Deleted: 726205) Binary : 17910 (Ratio: 2.30%) Ternary : 3441 (Ratio: 0.44%) Conflict : 779478 (Average Length: 893.8 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 779478 (Average: 6.35 Max: 810 Sum: 4951879) Executed : 779440 (Average: 6.35 Max: 810 Sum: 4951338 Ratio: 99.99%) Bounded : 38 (Average: 14.24 Max: 62 Sum: 541 Ratio: 0.01%) Rules : 55133 (Original: 53913) Atoms : 43853 Bodies : 10280 (Original: 9059) Count : 232 (Original: 476) Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) Tight : Yes Variables : 283647 (Eliminated: 1464 Frozen: 274653) Constraints : 2095571 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) Memory Peak : 597MB Max. Length : 60 steps Models : 1 [endof: stats after solve call] Solving Time: 39.66s Memory: 591MB (+32MB) UNKNOWN Iteration Time: 40.22s Iteration 18 Queue: [(14,70,0,True), (15,75,0,True), (16,80,0,True), (17,85,0,True)] Grounded Until: 65 Expected Memory: 734.0MB Grounding... [('step', [66]), ('step', [67]), ('step', [68]), ('step', [69]), ('step', [70]), ('check', [70])] Grounding Time: 0.34s Memory: 591MB (+0MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 19 Time : 564.796s (Solving: 552.36s 1st Model: 0.00s Unsat: 19.29s) CPU Time : 564.948s Choices : 5653911 (Domain: 5454075) Conflicts : 831295 (Analyzed: 831291) Restarts : 1453 (Average: 572.12 Last: 2225) Model-Level : 147.0 Problems : 19 (Average Length: 34.63 Splits: 0) Lemmas : 831291 (Deleted: 764176) Binary : 18968 (Ratio: 2.28%) Ternary : 3613 (Ratio: 0.43%) Conflict : 831291 (Average Length: 886.1 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 831291 (Average: 6.45 Max: 810 Sum: 5357766) Executed : 831253 (Average: 6.44 Max: 810 Sum: 5357225 Ratio: 99.99%) Bounded : 38 (Average: 14.24 Max: 62 Sum: 541 Ratio: 0.01%) Rules : 55133 (Original: 53913) Atoms : 43853 Bodies : 10280 (Original: 9059) Count : 232 (Original: 476) Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) Tight : Yes Variables : 306223 (Eliminated: 1464 Frozen: 297229) Constraints : 2268616 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) Memory Peak : 629MB Max. Length : 65 steps Models : 1 [endof: stats after solve call] Solving Time: 31.36s Memory: 603MB (+12MB) UNKNOWN Iteration Time: 31.95s Iteration 19 Queue: [(15,75,0,True), (16,80,0,True), (17,85,0,True)] Grounded Until: 70 Expected Memory: 746.0MB Grounding... [('step', [71]), ('step', [72]), ('step', [73]), ('step', [74]), ('step', [75]), ('check', [75])] Grounding Time: 0.34s Memory: 603MB (+0MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 20 Time : 617.165s (Solving: 603.75s 1st Model: 0.00s Unsat: 19.29s) CPU Time : 617.340s Choices : 6324741 (Domain: 6124740) Conflicts : 910938 (Analyzed: 910934) Restarts : 1553 (Average: 586.56 Last: 2225) Model-Level : 147.0 Problems : 20 (Average Length: 36.75 Splits: 0) Lemmas : 910934 (Deleted: 845824) Binary : 20287 (Ratio: 2.23%) Ternary : 3786 (Ratio: 0.42%) Conflict : 910934 (Average Length: 878.7 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 910934 (Average: 6.58 Max: 810 Sum: 5995248) Executed : 910896 (Average: 6.58 Max: 810 Sum: 5994707 Ratio: 99.99%) Bounded : 38 (Average: 14.24 Max: 62 Sum: 541 Ratio: 0.01%) Rules : 55133 (Original: 53913) Atoms : 43853 Bodies : 10280 (Original: 9059) Count : 232 (Original: 476) Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) Tight : Yes Variables : 328799 (Eliminated: 1464 Frozen: 319805) Constraints : 2441661 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) Memory Peak : 643MB Max. Length : 70 steps Models : 1 [endof: stats after solve call] Solving Time: 51.79s Memory: 617MB (+14MB) UNKNOWN Iteration Time: 52.40s Iteration 20 Queue: [(16,80,0,True), (17,85,0,True)] Grounded Until: 75 Expected Memory: 760.0MB Grounding... [('step', [76]), ('step', [77]), ('step', [78]), ('step', [79]), ('step', [80]), ('check', [80])] Grounding Time: 0.48s Memory: 633MB (+16MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 21 Time : 656.065s (Solving: 641.53s 1st Model: 0.00s Unsat: 19.29s) CPU Time : 656.260s Choices : 6830979 (Domain: 6625457) Conflicts : 971635 (Analyzed: 971631) Restarts : 1653 (Average: 587.80 Last: 2225) Model-Level : 147.0 Problems : 21 (Average Length: 38.90 Splits: 0) Lemmas : 971631 (Deleted: 904777) Binary : 21300 (Ratio: 2.19%) Ternary : 3935 (Ratio: 0.40%) Conflict : 971631 (Average Length: 876.7 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 971631 (Average: 6.66 Max: 810 Sum: 6468366) Executed : 971593 (Average: 6.66 Max: 810 Sum: 6467825 Ratio: 99.99%) Bounded : 38 (Average: 14.24 Max: 62 Sum: 541 Ratio: 0.01%) Rules : 55133 (Original: 53913) Atoms : 43853 Bodies : 10280 (Original: 9059) Count : 232 (Original: 476) Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) Tight : Yes Variables : 351375 (Eliminated: 1464 Frozen: 342381) Constraints : 2614706 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) Memory Peak : 679MB Max. Length : 75 steps Models : 1 [endof: stats after solve call] Solving Time: 38.18s Memory: 646MB (+13MB) UNKNOWN Iteration Time: 38.92s Iteration 21 Queue: [(17,85,0,True)] Grounded Until: 80 Expected Memory: 789.0MB Grounding... [('step', [81]), ('step', [82]), ('step', [83]), ('step', [84]), ('step', [85]), ('check', [85])] Grounding Time: 0.32s Memory: 646MB (+0MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 22 Time : 695.874s (Solving: 680.36s 1st Model: 0.00s Unsat: 19.29s) CPU Time : 696.088s Choices : 7358251 (Domain: 7150785) Conflicts : 1030352 (Analyzed: 1030348) Restarts : 1753 (Average: 587.76 Last: 2225) Model-Level : 147.0 Problems : 22 (Average Length: 41.09 Splits: 0) Lemmas : 1030348 (Deleted: 961806) Binary : 22392 (Ratio: 2.17%) Ternary : 4092 (Ratio: 0.40%) Conflict : 1030348 (Average Length: 874.4 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 1030348 (Average: 6.75 Max: 810 Sum: 6956440) Executed : 1030310 (Average: 6.75 Max: 810 Sum: 6955899 Ratio: 99.99%) Bounded : 38 (Average: 14.24 Max: 62 Sum: 541 Ratio: 0.01%) Rules : 55133 (Original: 53913) Atoms : 43853 Bodies : 10280 (Original: 9059) Count : 232 (Original: 476) Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) Tight : Yes Variables : 373951 (Eliminated: 1464 Frozen: 364957) Constraints : 2787751 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) Memory Peak : 695MB Max. Length : 80 steps Models : 1 [endof: stats after solve call] Solving Time: 39.24s Memory: 660MB (+14MB) UNKNOWN Iteration Time: 39.84s Iteration 22 Queue: [(5,25,2,True), (6,30,2,True), (7,35,1,True), (8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True), (22,110,0,True)] Grounded Until: 85 Blocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 23 Time : 784.181s (Solving: 768.56s 1st Model: 0.00s Unsat: 19.29s) CPU Time : 784.432s Choices : 7583190 (Domain: 7375724) Conflicts : 1111482 (Analyzed: 1111478) Restarts : 1853 (Average: 599.83 Last: 2225) Model-Level : 147.0 Problems : 23 (Average Length: 43.09 Splits: 0) Lemmas : 1111478 (Deleted: 1037390) Binary : 22557 (Ratio: 2.03%) Ternary : 4130 (Ratio: 0.37%) Conflict : 1111478 (Average Length: 913.5 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 1111478 (Average: 6.45 Max: 810 Sum: 7170472) Executed : 1111440 (Average: 6.45 Max: 810 Sum: 7169931 Ratio: 99.99%) Bounded : 38 (Average: 14.24 Max: 62 Sum: 541 Ratio: 0.01%) Rules : 55133 (Original: 53913) Atoms : 43853 Bodies : 10280 (Original: 9059) Count : 232 (Original: 476) Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) Tight : Yes Variables : 373951 (Eliminated: 1464 Frozen: 372487) Constraints : 2787751 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) Memory Peak : 695MB Max. Length : 85 steps Models : 1 [endof: stats after solve call] Solving Time: 88.30s Memory: 662MB (+2MB) UNKNOWN Iteration Time: 88.35s Iteration 23 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,1,True), (17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True), (22,110,0,True)] Grounded Until: 85 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 24 Time : 827.747s (Solving: 812.03s 1st Model: 0.00s Unsat: 19.29s) CPU Time : 828.016s Choices : 7863730 (Domain: 7656264) Conflicts : 1160129 (Analyzed: 1160125) Restarts : 1953 (Average: 594.02 Last: 2225) Model-Level : 147.0 Problems : 24 (Average Length: 44.92 Splits: 0) Lemmas : 1160125 (Deleted: 1083829) Binary : 22746 (Ratio: 1.96%) Ternary : 4163 (Ratio: 0.36%) Conflict : 1160125 (Average Length: 930.7 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 1160125 (Average: 6.41 Max: 810 Sum: 7432623) Executed : 1160087 (Average: 6.41 Max: 810 Sum: 7432082 Ratio: 99.99%) Bounded : 38 (Average: 14.24 Max: 62 Sum: 541 Ratio: 0.01%) Rules : 55133 (Original: 53913) Atoms : 43853 Bodies : 10280 (Original: 9059) Count : 232 (Original: 476) Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) Tight : Yes Variables : 373951 (Eliminated: 1464 Frozen: 372487) Constraints : 2787751 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) Memory Peak : 695MB Max. Length : 85 steps Models : 1 [endof: stats after solve call] Solving Time: 43.55s Memory: 662MB (+0MB) UNKNOWN Iteration Time: 43.59s Iteration 24 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,1,True), (17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True), (22,110,0,True)] Grounded Until: 85 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 25 Time : 879.751s (Solving: 863.89s 1st Model: 0.00s Unsat: 19.29s) CPU Time : 880.044s Choices : 8128841 (Domain: 7921375) Conflicts : 1220760 (Analyzed: 1220756) Restarts : 2053 (Average: 594.62 Last: 2225) Model-Level : 147.0 Problems : 25 (Average Length: 46.60 Splits: 0) Lemmas : 1220756 (Deleted: 1147275) Binary : 22983 (Ratio: 1.88%) Ternary : 4224 (Ratio: 0.35%) Conflict : 1220756 (Average Length: 941.9 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 1220756 (Average: 6.29 Max: 810 Sum: 7678134) Executed : 1220718 (Average: 6.29 Max: 810 Sum: 7677593 Ratio: 99.99%) Bounded : 38 (Average: 14.24 Max: 62 Sum: 541 Ratio: 0.01%) Rules : 55133 (Original: 53913) Atoms : 43853 Bodies : 10280 (Original: 9059) Count : 232 (Original: 476) Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) Tight : Yes Variables : 373951 (Eliminated: 1464 Frozen: 372487) Constraints : 2787751 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) Memory Peak : 695MB Max. Length : 85 steps Models : 1 [endof: stats after solve call] Solving Time: 51.96s Memory: 662MB (+0MB) UNKNOWN Iteration Time: 52.03s Iteration 25 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,1,True), (17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True), (22,110,0,True)] Grounded Until: 85 Unblocking actions... Solving... *** Info : (planner): INTERRUPTED by signal! UNKNOWN INTERRUPTED : 1 Models : 0+ Calls : 26 Time : 895.001s (Solving: 879.05s 1st Model: 0.00s Unsat: 19.29s) CPU Time : 895.284s Choices : 8289380 (Domain: 8081914) Conflicts : 1245722 (Analyzed: 1245718) Restarts : 2111 (Average: 590.11 Last: 2225) Model-Level : 147.0 Problems : 26 (Average Length: 48.15 Splits: 0) Lemmas : 1245718 (Deleted: 1177076) Binary : 23249 (Ratio: 1.87%) Ternary : 4273 (Ratio: 0.34%) Conflict : 1245718 (Average Length: 936.6 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 1245718 (Average: 6.28 Max: 810 Sum: 7825992) Executed : 1245680 (Average: 6.28 Max: 810 Sum: 7825451 Ratio: 99.99%) Bounded : 38 (Average: 14.24 Max: 62 Sum: 541 Ratio: 0.01%) Rules : 55133 (Original: 53913) Atoms : 43853 Bodies : 10280 (Original: 9059) Count : 232 (Original: 476) Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) Tight : Yes Variables : 373951 (Eliminated: 1464 Frozen: 372487) Constraints : 2787751 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) Memory Peak : 695MB Max. Length : 85 steps Models : 1