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-3.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-3.pddl Parsing... Parsing: [0.040s CPU, 0.039s wall-clock] Normalizing task... [0.000s CPU, 0.003s wall-clock] Instantiating... Generating Datalog program... [0.010s CPU, 0.010s wall-clock] Normalizing Datalog program... Normalizing Datalog program: [0.050s CPU, 0.050s wall-clock] Preparing model... [0.030s CPU, 0.025s wall-clock] Generated 115 rules. Computing model... [0.320s CPU, 0.327s wall-clock] 2025 relevant atoms 2105 auxiliary atoms 4130 final queue length 7122 total queue pushes Completing instantiation... [0.600s CPU, 0.600s wall-clock] Instantiating: [1.010s CPU, 1.016s wall-clock] Computing fact groups... Finding invariants... 24 initial candidates Finding invariants: [0.100s CPU, 0.090s wall-clock] Checking invariant weight... [0.000s CPU, 0.001s wall-clock] Instantiating groups... [0.000s 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.130s CPU, 0.121s 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.000s CPU, 0.002s wall-clock] Translating task... Processing axioms... Simplifying axioms... [0.000s CPU, 0.000s wall-clock] Processing axioms: [0.040s CPU, 0.033s wall-clock] Translating task: [0.660s CPU, 0.658s 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.311s 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.240s CPU, 0.255s wall-clock] Done! [2.620s CPU, 2.641s 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.653s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s) CPU Time : 0.568s 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 : 0 Calls : 2 Time : 0.981s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s) CPU Time : 0.896s Choices : 87 (Domain: 79) Conflicts : 41 (Analyzed: 40) Restarts : 0 Problems : 2 (Average Length: 4.50 Splits: 0) Lemmas : 40 (Deleted: 0) Binary : 5 (Ratio: 12.50%) Ternary : 0 (Ratio: 0.00%) Conflict : 40 (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 : 40 (Average: 2.20 Max: 11 Sum: 88) Executed : 39 (Average: 2.17 Max: 11 Sum: 87 Ratio: 98.86%) Bounded : 1 (Average: 1.00 Max: 1 Sum: 1 Ratio: 1.14%) Rules : 38518 Atoms : 38518 Bodies : 1 (Original: 0) Tight : Yes Variables : 10318 (Eliminated: 0 Frozen: 10318) Constraints : 36429 (Binary: 95.1% Ternary: 3.5% Other: 1.5%) Memory Peak : 222MB Max. Length : 0 steps Models : 0 [endof: stats after solve call] Solving Time: 0.10s Memory: 160MB (+2MB) UNSAT Iteration Time: 0.33s 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: 162.0MB Grounding... [('step', [6]), ('step', [7]), ('step', [8]), ('step', [9]), ('step', [10]), ('check', [10])] Grounding Time: 0.18s Memory: 164MB (+4MB) Unblocking actions... Solving... [start: stats after solve call] Models : 1+ Calls : 3 Time : 1.409s (Solving: 0.01s 1st Model: 0.00s Unsat: 0.00s) CPU Time : 1.324s Choices : 554 (Domain: 518) Conflicts : 55 (Analyzed: 54) Restarts : 0 Model-Level : 212.0 Problems : 3 (Average Length: 7.00 Splits: 0) Lemmas : 54 (Deleted: 0) Binary : 10 (Ratio: 18.52%) Ternary : 2 (Ratio: 3.70%) Conflict : 54 (Average Length: 12.4 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 54 (Average: 6.57 Max: 65 Sum: 355) Executed : 53 (Average: 6.56 Max: 65 Sum: 354 Ratio: 99.72%) Bounded : 1 (Average: 1.00 Max: 1 Sum: 1 Ratio: 0.28%) Rules : 38518 Atoms : 38518 Bodies : 1 (Original: 0) Tight : Yes Variables : 22604 (Eliminated: 0 Frozen: 22604) Constraints : 136839 (Binary: 95.5% Ternary: 3.2% Other: 1.2%) Memory Peak : 222MB Max. Length : 5 steps Models : 1 [endof: stats after solve call] Solving Time: 0.17s Memory: 171MB (+7MB) SAT Testing... NOT SERIALIZABLE Testing Time: 0.65s Memory: 191MB (+20MB) Solving... [start: stats after solve call] Models : 0 Calls : 4 Time : 1.943s (Solving: 0.27s 1st Model: 0.00s Unsat: 0.26s) CPU Time : 1.856s Choices : 8046 (Domain: 7436) Conflicts : 961 (Analyzed: 959) Restarts : 6 (Average: 159.83 Last: 98) Model-Level : 212.0 Problems : 4 (Average Length: 8.25 Splits: 0) Lemmas : 959 (Deleted: 0) Binary : 286 (Ratio: 29.82%) Ternary : 161 (Ratio: 16.79%) Conflict : 959 (Average Length: 34.6 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 959 (Average: 8.24 Max: 89 Sum: 7898) Executed : 945 (Average: 8.14 Max: 89 Sum: 7807 Ratio: 98.85%) Bounded : 14 (Average: 6.50 Max: 12 Sum: 91 Ratio: 1.15%) Rules : 94613 (Original: 86518) Atoms : 45936 Bodies : 40692 (Original: 32596) Count : 619 (Original: 1518) Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) Tight : Yes Variables : 34632 (Eliminated: 8994 Frozen: 25638) Constraints : 194982 (Binary: 88.9% Ternary: 7.3% Other: 3.8%) Memory Peak : 222MB Max. Length : 5 steps Models : 1 [endof: stats after solve call] Solving Time: 0.39s Memory: 188MB (+-3MB) UNSAT Iteration Time: 1.47s Iteration 4 Queue: [(3,15,0,True), (4,20,0,True), (5,25,0,True), (6,30,0,True)] Grounded Until: 10 Expected Memory: 199.0MB Grounding... [('step', [11]), ('step', [12]), ('step', [13]), ('step', [14]), ('step', [15]), ('check', [15])] Grounding Time: 0.34s Memory: 195MB (+7MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0 Calls : 5 Time : 9.858s (Solving: 7.40s 1st Model: 0.00s Unsat: 7.40s) CPU Time : 9.776s Choices : 178625 (Domain: 143317) Conflicts : 25090 (Analyzed: 25087) Restarts : 94 (Average: 266.88 Last: 98) Model-Level : 212.0 Problems : 5 (Average Length: 10.00 Splits: 0) Lemmas : 25087 (Deleted: 16452) Binary : 1522 (Ratio: 6.07%) Ternary : 479 (Ratio: 1.91%) Conflict : 25087 (Average Length: 288.1 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 25087 (Average: 6.95 Max: 401 Sum: 174374) Executed : 25056 (Average: 6.94 Max: 401 Sum: 174016 Ratio: 99.79%) Bounded : 31 (Average: 11.55 Max: 17 Sum: 358 Ratio: 0.21%) Rules : 94613 (Original: 86518) Atoms : 45936 Bodies : 40692 (Original: 32596) Count : 619 (Original: 1518) Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) Tight : Yes Variables : 57193 (Eliminated: 8994 Frozen: 40669) Constraints : 363350 (Binary: 90.3% Ternary: 6.9% Other: 2.9%) Memory Peak : 222MB Max. Length : 10 steps Models : 1 [endof: stats after solve call] Solving Time: 7.46s Memory: 206MB (+11MB) UNSAT Iteration Time: 7.93s Iteration 5 Queue: [(4,20,0,True), (5,25,0,True), (6,30,0,True)] Grounded Until: 15 Expected Memory: 224.0MB Grounding... [('step', [16]), ('step', [17]), ('step', [18]), ('step', [19]), ('step', [20]), ('check', [20])] Grounding Time: 0.35s Memory: 213MB (+7MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 6 Time : 24.515s (Solving: 21.24s 1st Model: 0.00s Unsat: 7.40s) CPU Time : 24.440s Choices : 450104 (Domain: 398284) Conflicts : 53216 (Analyzed: 53213) Restarts : 194 (Average: 274.29 Last: 201) Model-Level : 212.0 Problems : 6 (Average Length: 12.00 Splits: 0) Lemmas : 53213 (Deleted: 38381) Binary : 2964 (Ratio: 5.57%) Ternary : 766 (Ratio: 1.44%) Conflict : 53213 (Average Length: 476.5 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 53213 (Average: 8.17 Max: 401 Sum: 435006) Executed : 53170 (Average: 8.16 Max: 401 Sum: 434408 Ratio: 99.86%) Bounded : 43 (Average: 13.91 Max: 22 Sum: 598 Ratio: 0.14%) Rules : 94613 (Original: 86518) Atoms : 45936 Bodies : 40692 (Original: 32596) Count : 619 (Original: 1518) Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) Tight : Yes Variables : 79754 (Eliminated: 8994 Frozen: 63230) Constraints : 517735 (Binary: 90.8% Ternary: 6.7% Other: 2.5%) Memory Peak : 225MB Max. Length : 15 steps Models : 1 [endof: stats after solve call] Solving Time: 14.18s Memory: 225MB (+12MB) UNKNOWN Iteration Time: 14.67s Iteration 6 Queue: [(5,25,0,True), (6,30,0,True)] Grounded Until: 20 Expected Memory: 244.0MB Grounding... [('step', [21]), ('step', [22]), ('step', [23]), ('step', [24]), ('step', [25]), ('check', [25])] Grounding Time: 0.36s Memory: 227MB (+2MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 7 Time : 41.662s (Solving: 37.54s 1st Model: 0.00s Unsat: 7.40s) CPU Time : 41.596s Choices : 644218 (Domain: 583497) Conflicts : 81366 (Analyzed: 81363) Restarts : 294 (Average: 276.74 Last: 202) Model-Level : 212.0 Problems : 7 (Average Length: 14.14 Splits: 0) Lemmas : 81363 (Deleted: 64324) Binary : 4084 (Ratio: 5.02%) Ternary : 955 (Ratio: 1.17%) Conflict : 81363 (Average Length: 724.4 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 81363 (Average: 7.56 Max: 401 Sum: 614802) Executed : 81318 (Average: 7.55 Max: 401 Sum: 614150 Ratio: 99.89%) Bounded : 45 (Average: 14.49 Max: 27 Sum: 652 Ratio: 0.11%) Rules : 94613 (Original: 86518) Atoms : 45936 Bodies : 40692 (Original: 32596) Count : 619 (Original: 1518) Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) Tight : Yes Variables : 102315 (Eliminated: 8994 Frozen: 85791) Constraints : 684819 (Binary: 91.1% Ternary: 6.6% Other: 2.3%) Memory Peak : 371MB Max. Length : 20 steps Models : 1 [endof: stats after solve call] Solving Time: 16.64s Memory: 307MB (+80MB) UNKNOWN Iteration Time: 17.16s Iteration 7 Queue: [(6,30,0,True)] Grounded Until: 25 Expected Memory: 389.0MB Grounding... [('step', [26]), ('step', [27]), ('step', [28]), ('step', [29]), ('step', [30]), ('check', [30])] Grounding Time: 0.31s Memory: 309MB (+2MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 8 Time : 59.418s (Solving: 54.48s 1st Model: 0.00s Unsat: 7.40s) CPU Time : 59.364s Choices : 877843 (Domain: 807962) Conflicts : 109490 (Analyzed: 109487) Restarts : 394 (Average: 277.89 Last: 202) Model-Level : 212.0 Problems : 8 (Average Length: 16.38 Splits: 0) Lemmas : 109487 (Deleted: 90819) Binary : 5308 (Ratio: 4.85%) Ternary : 1262 (Ratio: 1.15%) Conflict : 109487 (Average Length: 786.0 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 109487 (Average: 7.61 Max: 401 Sum: 833224) Executed : 109442 (Average: 7.60 Max: 401 Sum: 832572 Ratio: 99.92%) Bounded : 45 (Average: 14.49 Max: 27 Sum: 652 Ratio: 0.08%) Rules : 94613 (Original: 86518) Atoms : 45936 Bodies : 40692 (Original: 32596) Count : 619 (Original: 1518) Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) Tight : Yes Variables : 124876 (Eliminated: 8994 Frozen: 108352) Constraints : 851268 (Binary: 91.2% Ternary: 6.6% Other: 2.2%) Memory Peak : 371MB Max. Length : 25 steps Models : 1 [endof: stats after solve call] Solving Time: 17.29s Memory: 322MB (+13MB) UNKNOWN Iteration Time: 17.77s 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 : 68.575s (Solving: 63.60s 1st Model: 0.00s Unsat: 7.40s) CPU Time : 68.524s Choices : 967961 (Domain: 898080) Conflicts : 137673 (Analyzed: 137670) Restarts : 494 (Average: 278.68 Last: 202) Model-Level : 212.0 Problems : 9 (Average Length: 18.11 Splits: 0) Lemmas : 137670 (Deleted: 117901) Binary : 5569 (Ratio: 4.05%) Ternary : 1305 (Ratio: 0.95%) Conflict : 137670 (Average Length: 706.8 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 137670 (Average: 6.66 Max: 401 Sum: 917259) Executed : 137622 (Average: 6.66 Max: 401 Sum: 916516 Ratio: 99.92%) Bounded : 48 (Average: 15.48 Max: 32 Sum: 743 Ratio: 0.08%) Rules : 94613 (Original: 86518) Atoms : 45936 Bodies : 40692 (Original: 32596) Count : 619 (Original: 1518) Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) Tight : Yes Variables : 124876 (Eliminated: 8994 Frozen: 115882) Constraints : 851268 (Binary: 91.2% Ternary: 6.6% Other: 2.2%) Memory Peak : 371MB Max. Length : 30 steps Models : 1 [endof: stats after solve call] Solving Time: 9.15s Memory: 322MB (+0MB) UNKNOWN Iteration Time: 9.16s 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 : 93.661s (Solving: 88.65s 1st Model: 0.00s Unsat: 7.40s) CPU Time : 93.620s Choices : 1092316 (Domain: 1022396) Conflicts : 165767 (Analyzed: 165764) Restarts : 594 (Average: 279.06 Last: 202) Model-Level : 212.0 Problems : 10 (Average Length: 19.50 Splits: 0) Lemmas : 165764 (Deleted: 145297) Binary : 5831 (Ratio: 3.52%) Ternary : 1370 (Ratio: 0.83%) Conflict : 165764 (Average Length: 807.6 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 165764 (Average: 6.21 Max: 401 Sum: 1028957) Executed : 165715 (Average: 6.20 Max: 401 Sum: 1028182 Ratio: 99.92%) Bounded : 49 (Average: 15.82 Max: 32 Sum: 775 Ratio: 0.08%) Rules : 94613 (Original: 86518) Atoms : 45936 Bodies : 40692 (Original: 32596) Count : 619 (Original: 1518) Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) Tight : Yes Variables : 124876 (Eliminated: 8994 Frozen: 115882) Constraints : 851240 (Binary: 91.2% Ternary: 6.6% Other: 2.2%) Memory Peak : 371MB Max. Length : 30 steps Models : 1 [endof: stats after solve call] Solving Time: 25.09s Memory: 322MB (+0MB) UNKNOWN Iteration Time: 25.10s 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 : 114.674s (Solving: 109.62s 1st Model: 0.00s Unsat: 7.40s) CPU Time : 114.644s Choices : 1339062 (Domain: 1266460) Conflicts : 193889 (Analyzed: 193886) Restarts : 694 (Average: 279.37 Last: 202) Model-Level : 212.0 Problems : 11 (Average Length: 20.64 Splits: 0) Lemmas : 193886 (Deleted: 172108) Binary : 6429 (Ratio: 3.32%) Ternary : 1486 (Ratio: 0.77%) Conflict : 193886 (Average Length: 813.8 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 193886 (Average: 6.49 Max: 401 Sum: 1259166) Executed : 193837 (Average: 6.49 Max: 401 Sum: 1258391 Ratio: 99.94%) Bounded : 49 (Average: 15.82 Max: 32 Sum: 775 Ratio: 0.06%) Rules : 94613 (Original: 86518) Atoms : 45936 Bodies : 40692 (Original: 32596) Count : 619 (Original: 1518) Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) Tight : Yes Variables : 124876 (Eliminated: 8994 Frozen: 115882) Constraints : 849719 (Binary: 91.2% Ternary: 6.6% Other: 2.2%) Memory Peak : 371MB Max. Length : 30 steps Models : 1 [endof: stats after solve call] Solving Time: 21.00s Memory: 322MB (+0MB) UNKNOWN Iteration Time: 21.03s 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: 404.0MB Grounding... [('step', [31]), ('step', [32]), ('step', [33]), ('step', [34]), ('step', [35]), ('check', [35])] Grounding Time: 0.32s Memory: 324MB (+2MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 12 Time : 129.744s (Solving: 123.86s 1st Model: 0.00s Unsat: 7.40s) CPU Time : 129.720s Choices : 1533857 (Domain: 1454042) Conflicts : 222078 (Analyzed: 222075) Restarts : 794 (Average: 279.69 Last: 202) Model-Level : 212.0 Problems : 12 (Average Length: 22.00 Splits: 0) Lemmas : 222075 (Deleted: 198986) Binary : 7350 (Ratio: 3.31%) Ternary : 1575 (Ratio: 0.71%) Conflict : 222075 (Average Length: 769.1 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 222075 (Average: 6.49 Max: 401 Sum: 1440214) Executed : 222025 (Average: 6.48 Max: 401 Sum: 1439402 Ratio: 99.94%) Bounded : 50 (Average: 16.24 Max: 37 Sum: 812 Ratio: 0.06%) Rules : 94613 (Original: 86518) Atoms : 45936 Bodies : 40692 (Original: 32596) Count : 619 (Original: 1518) Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) Tight : Yes Variables : 147437 (Eliminated: 8994 Frozen: 130913) Constraints : 1022744 (Binary: 91.3% Ternary: 6.6% Other: 2.2%) Memory Peak : 371MB Max. Length : 30 steps Models : 1 [endof: stats after solve call] Solving Time: 14.59s Memory: 344MB (+20MB) UNKNOWN Iteration Time: 15.09s 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: 426.0MB Grounding... [('step', [36]), ('step', [37]), ('step', [38]), ('step', [39]), ('step', [40]), ('check', [40])] Grounding Time: 0.42s Memory: 357MB (+13MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 13 Time : 145.922s (Solving: 139.08s 1st Model: 0.00s Unsat: 7.40s) CPU Time : 145.904s Choices : 1767987 (Domain: 1676424) Conflicts : 250245 (Analyzed: 250242) Restarts : 894 (Average: 279.91 Last: 206) Model-Level : 212.0 Problems : 13 (Average Length: 23.54 Splits: 0) Lemmas : 250242 (Deleted: 225054) Binary : 8412 (Ratio: 3.36%) Ternary : 1719 (Ratio: 0.69%) Conflict : 250242 (Average Length: 767.3 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 250242 (Average: 6.60 Max: 401 Sum: 1652594) Executed : 250191 (Average: 6.60 Max: 401 Sum: 1651740 Ratio: 99.95%) Bounded : 51 (Average: 16.75 Max: 42 Sum: 854 Ratio: 0.05%) Rules : 94613 (Original: 86518) Atoms : 45936 Bodies : 40692 (Original: 32596) Count : 619 (Original: 1518) Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) Tight : Yes Variables : 169998 (Eliminated: 8994 Frozen: 153474) Constraints : 1195759 (Binary: 91.3% Ternary: 6.6% Other: 2.1%) Memory Peak : 377MB Max. Length : 35 steps Models : 1 [endof: stats after solve call] Solving Time: 15.59s Memory: 366MB (+9MB) UNKNOWN Iteration Time: 16.20s 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: 448.0MB Grounding... [('step', [41]), ('step', [42]), ('step', [43]), ('step', [44]), ('step', [45]), ('check', [45])] Grounding Time: 0.31s Memory: 367MB (+1MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 14 Time : 162.860s (Solving: 155.16s 1st Model: 0.00s Unsat: 7.40s) CPU Time : 162.848s Choices : 2012899 (Domain: 1917846) Conflicts : 278412 (Analyzed: 278409) Restarts : 994 (Average: 280.09 Last: 206) Model-Level : 212.0 Problems : 14 (Average Length: 25.21 Splits: 0) Lemmas : 278409 (Deleted: 251719) Binary : 9241 (Ratio: 3.32%) Ternary : 1798 (Ratio: 0.65%) Conflict : 278409 (Average Length: 767.5 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 278409 (Average: 6.73 Max: 401 Sum: 1873261) Executed : 278358 (Average: 6.73 Max: 401 Sum: 1872407 Ratio: 99.95%) Bounded : 51 (Average: 16.75 Max: 42 Sum: 854 Ratio: 0.05%) Rules : 94613 (Original: 86518) Atoms : 45936 Bodies : 40692 (Original: 32596) Count : 619 (Original: 1518) Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) Tight : Yes Variables : 192559 (Eliminated: 8994 Frozen: 176035) Constraints : 1368767 (Binary: 91.3% Ternary: 6.6% Other: 2.1%) Memory Peak : 393MB Max. Length : 40 steps Models : 1 [endof: stats after solve call] Solving Time: 16.44s Memory: 381MB (+14MB) UNKNOWN Iteration Time: 16.95s 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: 463.0MB Grounding... [('step', [46]), ('step', [47]), ('step', [48]), ('step', [49]), ('step', [50]), ('check', [50])] Grounding Time: 0.31s Memory: 381MB (+0MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 15 Time : 178.759s (Solving: 170.19s 1st Model: 0.00s Unsat: 7.40s) CPU Time : 178.752s Choices : 2307695 (Domain: 2197417) Conflicts : 306536 (Analyzed: 306533) Restarts : 1094 (Average: 280.19 Last: 208) Model-Level : 212.0 Problems : 15 (Average Length: 27.00 Splits: 0) Lemmas : 306533 (Deleted: 278324) Binary : 10317 (Ratio: 3.37%) Ternary : 1985 (Ratio: 0.65%) Conflict : 306533 (Average Length: 750.2 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 306533 (Average: 6.98 Max: 401 Sum: 2139960) Executed : 306482 (Average: 6.98 Max: 401 Sum: 2139106 Ratio: 99.96%) Bounded : 51 (Average: 16.75 Max: 42 Sum: 854 Ratio: 0.04%) Rules : 94613 (Original: 86518) Atoms : 45936 Bodies : 40692 (Original: 32596) Count : 619 (Original: 1518) Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) Tight : Yes Variables : 215120 (Eliminated: 8994 Frozen: 198596) Constraints : 1541792 (Binary: 91.4% Ternary: 6.6% Other: 2.1%) Memory Peak : 412MB Max. Length : 45 steps Models : 1 [endof: stats after solve call] Solving Time: 15.40s Memory: 410MB (+29MB) UNKNOWN Iteration Time: 15.91s 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: 492.0MB Grounding... [('step', [51]), ('step', [52]), ('step', [53]), ('step', [54]), ('step', [55]), ('check', [55])] Grounding Time: 0.31s Memory: 410MB (+0MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 16 Time : 196.304s (Solving: 186.86s 1st Model: 0.00s Unsat: 7.40s) CPU Time : 196.304s Choices : 2586997 (Domain: 2474559) Conflicts : 334700 (Analyzed: 334697) Restarts : 1194 (Average: 280.32 Last: 208) Model-Level : 212.0 Problems : 16 (Average Length: 28.88 Splits: 0) Lemmas : 334697 (Deleted: 304977) Binary : 11080 (Ratio: 3.31%) Ternary : 2047 (Ratio: 0.61%) Conflict : 334697 (Average Length: 761.1 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 334697 (Average: 7.14 Max: 401 Sum: 2391390) Executed : 334646 (Average: 7.14 Max: 401 Sum: 2390536 Ratio: 99.96%) Bounded : 51 (Average: 16.75 Max: 42 Sum: 854 Ratio: 0.04%) Rules : 94613 (Original: 86518) Atoms : 45936 Bodies : 40692 (Original: 32596) Count : 619 (Original: 1518) Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) Tight : Yes Variables : 237681 (Eliminated: 8994 Frozen: 221157) Constraints : 1714817 (Binary: 91.4% Ternary: 6.6% Other: 2.0%) Memory Peak : 439MB Max. Length : 50 steps Models : 1 [endof: stats after solve call] Solving Time: 17.03s Memory: 420MB (+10MB) UNKNOWN Iteration Time: 17.56s 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: 502.0MB Grounding... [('step', [56]), ('step', [57]), ('step', [58]), ('step', [59]), ('step', [60]), ('check', [60])] Grounding Time: 0.34s Memory: 420MB (+0MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 17 Time : 212.017s (Solving: 201.64s 1st Model: 0.00s Unsat: 7.40s) CPU Time : 212.024s Choices : 2773336 (Domain: 2660889) Conflicts : 362908 (Analyzed: 362905) Restarts : 1294 (Average: 280.45 Last: 208) Model-Level : 212.0 Problems : 17 (Average Length: 30.82 Splits: 0) Lemmas : 362905 (Deleted: 332355) Binary : 11510 (Ratio: 3.17%) Ternary : 2097 (Ratio: 0.58%) Conflict : 362905 (Average Length: 755.0 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 362905 (Average: 7.05 Max: 401 Sum: 2556974) Executed : 362854 (Average: 7.04 Max: 401 Sum: 2556120 Ratio: 99.97%) Bounded : 51 (Average: 16.75 Max: 42 Sum: 854 Ratio: 0.03%) Rules : 94613 (Original: 86518) Atoms : 45936 Bodies : 40692 (Original: 32596) Count : 619 (Original: 1518) Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) Tight : Yes Variables : 260242 (Eliminated: 8994 Frozen: 243718) Constraints : 1887842 (Binary: 91.4% Ternary: 6.6% Other: 2.0%) Memory Peak : 455MB Max. Length : 55 steps Models : 1 [endof: stats after solve call] Solving Time: 15.15s Memory: 434MB (+14MB) UNKNOWN Iteration Time: 15.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: 516.0MB Grounding... [('step', [61]), ('step', [62]), ('step', [63]), ('step', [64]), ('step', [65]), ('check', [65])] Grounding Time: 0.32s Memory: 434MB (+0MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 18 Time : 231.824s (Solving: 220.52s 1st Model: 0.00s Unsat: 7.40s) CPU Time : 231.840s Choices : 3047628 (Domain: 2934473) Conflicts : 391041 (Analyzed: 391038) Restarts : 1394 (Average: 280.52 Last: 208) Model-Level : 212.0 Problems : 18 (Average Length: 32.83 Splits: 0) Lemmas : 391038 (Deleted: 359574) Binary : 11990 (Ratio: 3.07%) Ternary : 2151 (Ratio: 0.55%) Conflict : 391038 (Average Length: 753.6 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 391038 (Average: 7.17 Max: 401 Sum: 2805345) Executed : 390987 (Average: 7.17 Max: 401 Sum: 2804491 Ratio: 99.97%) Bounded : 51 (Average: 16.75 Max: 42 Sum: 854 Ratio: 0.03%) Rules : 94613 (Original: 86518) Atoms : 45936 Bodies : 40692 (Original: 32596) Count : 619 (Original: 1518) Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) Tight : Yes Variables : 282803 (Eliminated: 8994 Frozen: 266279) Constraints : 2060867 (Binary: 91.4% Ternary: 6.6% Other: 2.0%) Memory Peak : 473MB Max. Length : 60 steps Models : 1 [endof: stats after solve call] Solving Time: 19.27s Memory: 452MB (+18MB) UNKNOWN Iteration Time: 19.82s Iteration 18 Queue: [(14,70,0,True), (15,75,0,True), (16,80,0,True), (17,85,0,True)] Grounded Until: 65 Expected Memory: 534.0MB Grounding... [('step', [66]), ('step', [67]), ('step', [68]), ('step', [69]), ('step', [70]), ('check', [70])] Grounding Time: 0.33s Memory: 452MB (+0MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 19 Time : 249.390s (Solving: 237.13s 1st Model: 0.00s Unsat: 7.40s) CPU Time : 249.416s Choices : 3272129 (Domain: 3158615) Conflicts : 419210 (Analyzed: 419207) Restarts : 1494 (Average: 280.59 Last: 208) Model-Level : 212.0 Problems : 19 (Average Length: 34.89 Splits: 0) Lemmas : 419207 (Deleted: 385854) Binary : 12459 (Ratio: 2.97%) Ternary : 2197 (Ratio: 0.52%) Conflict : 419207 (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 : 419207 (Average: 7.16 Max: 401 Sum: 3002607) Executed : 419156 (Average: 7.16 Max: 401 Sum: 3001753 Ratio: 99.97%) Bounded : 51 (Average: 16.75 Max: 42 Sum: 854 Ratio: 0.03%) Rules : 94613 (Original: 86518) Atoms : 45936 Bodies : 40692 (Original: 32596) Count : 619 (Original: 1518) Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) Tight : Yes Variables : 305364 (Eliminated: 8994 Frozen: 288840) Constraints : 2233892 (Binary: 91.4% Ternary: 6.6% Other: 2.0%) Memory Peak : 491MB Max. Length : 65 steps Models : 1 [endof: stats after solve call] Solving Time: 17.00s Memory: 490MB (+38MB) UNKNOWN Iteration Time: 17.58s Iteration 19 Queue: [(15,75,0,True), (16,80,0,True), (17,85,0,True)] Grounded Until: 70 Expected Memory: 572.0MB Grounding... [('step', [71]), ('step', [72]), ('step', [73]), ('step', [74]), ('step', [75]), ('check', [75])] Grounding Time: 0.34s Memory: 490MB (+0MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 20 Time : 270.819s (Solving: 257.60s 1st Model: 0.00s Unsat: 7.40s) CPU Time : 270.856s Choices : 3640853 (Domain: 3525454) Conflicts : 447391 (Analyzed: 447388) Restarts : 1594 (Average: 280.67 Last: 208) Model-Level : 212.0 Problems : 20 (Average Length: 37.00 Splits: 0) Lemmas : 447388 (Deleted: 413840) Binary : 13149 (Ratio: 2.94%) Ternary : 2305 (Ratio: 0.52%) Conflict : 447388 (Average Length: 767.3 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 447388 (Average: 7.46 Max: 411 Sum: 3339733) Executed : 447337 (Average: 7.46 Max: 411 Sum: 3338879 Ratio: 99.97%) Bounded : 51 (Average: 16.75 Max: 42 Sum: 854 Ratio: 0.03%) Rules : 94613 (Original: 86518) Atoms : 45936 Bodies : 40692 (Original: 32596) Count : 619 (Original: 1518) Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) Tight : Yes Variables : 327925 (Eliminated: 8994 Frozen: 311401) Constraints : 2406917 (Binary: 91.4% Ternary: 6.6% Other: 2.0%) Memory Peak : 530MB Max. Length : 70 steps Models : 1 [endof: stats after solve call] Solving Time: 20.86s Memory: 503MB (+13MB) UNKNOWN Iteration Time: 21.45s Iteration 20 Queue: [(16,80,0,True), (17,85,0,True)] Grounded Until: 75 Expected Memory: 585.0MB Grounding... [('step', [76]), ('step', [77]), ('step', [78]), ('step', [79]), ('step', [80]), ('check', [80])] Grounding Time: 0.48s Memory: 518MB (+15MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 21 Time : 289.759s (Solving: 275.43s 1st Model: 0.00s Unsat: 7.40s) CPU Time : 289.804s Choices : 3919967 (Domain: 3804120) Conflicts : 475574 (Analyzed: 475571) Restarts : 1694 (Average: 280.74 Last: 208) Model-Level : 212.0 Problems : 21 (Average Length: 39.14 Splits: 0) Lemmas : 475571 (Deleted: 441027) Binary : 13579 (Ratio: 2.86%) Ternary : 2347 (Ratio: 0.49%) Conflict : 475571 (Average Length: 769.3 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 475571 (Average: 7.53 Max: 411 Sum: 3583315) Executed : 475520 (Average: 7.53 Max: 411 Sum: 3582461 Ratio: 99.98%) Bounded : 51 (Average: 16.75 Max: 42 Sum: 854 Ratio: 0.02%) Rules : 94613 (Original: 86518) Atoms : 45936 Bodies : 40692 (Original: 32596) Count : 619 (Original: 1518) Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) Tight : Yes Variables : 350486 (Eliminated: 8994 Frozen: 333962) Constraints : 2579942 (Binary: 91.5% Ternary: 6.6% Other: 2.0%) Memory Peak : 561MB Max. Length : 75 steps Models : 1 [endof: stats after solve call] Solving Time: 18.22s Memory: 521MB (+3MB) UNKNOWN Iteration Time: 18.96s Iteration 21 Queue: [(17,85,0,True)] Grounded Until: 80 Expected Memory: 603.0MB Grounding... [('step', [81]), ('step', [82]), ('step', [83]), ('step', [84]), ('step', [85]), ('check', [85])] Grounding Time: 0.35s Memory: 521MB (+0MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 22 Time : 308.599s (Solving: 293.27s 1st Model: 0.00s Unsat: 7.40s) CPU Time : 308.652s Choices : 4144295 (Domain: 4028411) Conflicts : 503747 (Analyzed: 503744) Restarts : 1794 (Average: 280.79 Last: 208) Model-Level : 212.0 Problems : 22 (Average Length: 41.32 Splits: 0) Lemmas : 503744 (Deleted: 468601) Binary : 13902 (Ratio: 2.76%) Ternary : 2400 (Ratio: 0.48%) Conflict : 503744 (Average Length: 769.0 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 503744 (Average: 7.50 Max: 422 Sum: 3776949) Executed : 503693 (Average: 7.50 Max: 422 Sum: 3776095 Ratio: 99.98%) Bounded : 51 (Average: 16.75 Max: 42 Sum: 854 Ratio: 0.02%) Rules : 94613 (Original: 86518) Atoms : 45936 Bodies : 40692 (Original: 32596) Count : 619 (Original: 1518) Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) Tight : Yes Variables : 373047 (Eliminated: 8994 Frozen: 356523) Constraints : 2752967 (Binary: 91.5% Ternary: 6.6% Other: 2.0%) Memory Peak : 570MB Max. Length : 80 steps Models : 1 [endof: stats after solve call] Solving Time: 18.23s Memory: 538MB (+17MB) UNKNOWN Iteration Time: 18.86s Iteration 22 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,1,True), (17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] Grounded Until: 85 Blocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 23 Time : 318.795s (Solving: 303.36s 1st Model: 0.00s Unsat: 7.40s) CPU Time : 318.852s Choices : 4279001 (Domain: 4163117) Conflicts : 531936 (Analyzed: 531933) Restarts : 1894 (Average: 280.85 Last: 208) Model-Level : 212.0 Problems : 23 (Average Length: 43.30 Splits: 0) Lemmas : 531933 (Deleted: 495516) Binary : 14207 (Ratio: 2.67%) Ternary : 2487 (Ratio: 0.47%) Conflict : 531933 (Average Length: 746.7 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 531933 (Average: 7.34 Max: 422 Sum: 3904971) Executed : 531877 (Average: 7.34 Max: 422 Sum: 3903854 Ratio: 99.97%) Bounded : 56 (Average: 19.95 Max: 87 Sum: 1117 Ratio: 0.03%) Rules : 94613 (Original: 86518) Atoms : 45936 Bodies : 40692 (Original: 32596) Count : 619 (Original: 1518) Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) Tight : Yes Variables : 373047 (Eliminated: 8994 Frozen: 364053) Constraints : 2752967 (Binary: 91.5% Ternary: 6.6% Other: 2.0%) Memory Peak : 570MB Max. Length : 85 steps Models : 1 [endof: stats after solve call] Solving Time: 10.16s Memory: 539MB (+1MB) UNKNOWN Iteration Time: 10.20s Iteration 23 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)] Grounded Until: 85 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 24 Time : 341.990s (Solving: 326.47s 1st Model: 0.00s Unsat: 7.40s) CPU Time : 342.056s Choices : 4445936 (Domain: 4330052) Conflicts : 560051 (Analyzed: 560048) Restarts : 1994 (Average: 280.87 Last: 208) Model-Level : 212.0 Problems : 24 (Average Length: 45.12 Splits: 0) Lemmas : 560048 (Deleted: 523095) Binary : 14316 (Ratio: 2.56%) Ternary : 2508 (Ratio: 0.45%) Conflict : 560048 (Average Length: 770.6 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 560048 (Average: 7.25 Max: 422 Sum: 4058898) Executed : 559992 (Average: 7.25 Max: 422 Sum: 4057781 Ratio: 99.97%) Bounded : 56 (Average: 19.95 Max: 87 Sum: 1117 Ratio: 0.03%) Rules : 94613 (Original: 86518) Atoms : 45936 Bodies : 40692 (Original: 32596) Count : 619 (Original: 1518) Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) Tight : Yes Variables : 373047 (Eliminated: 8994 Frozen: 364053) Constraints : 2752926 (Binary: 91.5% Ternary: 6.6% Other: 2.0%) Memory Peak : 570MB Max. Length : 85 steps Models : 1 [endof: stats after solve call] Solving Time: 23.17s Memory: 539MB (+0MB) UNKNOWN Iteration Time: 23.21s Iteration 24 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)] Grounded Until: 85 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 25 Time : 363.254s (Solving: 347.64s 1st Model: 0.00s Unsat: 7.40s) CPU Time : 363.328s Choices : 4644807 (Domain: 4528923) Conflicts : 588257 (Analyzed: 588254) Restarts : 2094 (Average: 280.92 Last: 208) Model-Level : 212.0 Problems : 25 (Average Length: 46.80 Splits: 0) Lemmas : 588254 (Deleted: 550824) Binary : 14516 (Ratio: 2.47%) Ternary : 2528 (Ratio: 0.43%) Conflict : 588254 (Average Length: 784.9 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 588254 (Average: 7.21 Max: 422 Sum: 4239616) Executed : 588198 (Average: 7.21 Max: 422 Sum: 4238499 Ratio: 99.97%) Bounded : 56 (Average: 19.95 Max: 87 Sum: 1117 Ratio: 0.03%) Rules : 94613 (Original: 86518) Atoms : 45936 Bodies : 40692 (Original: 32596) Count : 619 (Original: 1518) Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) Tight : Yes Variables : 373047 (Eliminated: 8994 Frozen: 364053) Constraints : 2752926 (Binary: 91.5% Ternary: 6.6% Other: 2.0%) Memory Peak : 570MB Max. Length : 85 steps Models : 1 [endof: stats after solve call] Solving Time: 21.24s Memory: 539MB (+0MB) UNKNOWN Iteration Time: 21.27s Iteration 25 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)] Grounded Until: 85 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 26 Time : 382.171s (Solving: 366.47s 1st Model: 0.00s Unsat: 7.40s) CPU Time : 382.252s Choices : 4830241 (Domain: 4714316) Conflicts : 616452 (Analyzed: 616449) Restarts : 2194 (Average: 280.97 Last: 208) Model-Level : 212.0 Problems : 26 (Average Length: 48.35 Splits: 0) Lemmas : 616449 (Deleted: 578167) Binary : 14789 (Ratio: 2.40%) Ternary : 2561 (Ratio: 0.42%) Conflict : 616449 (Average Length: 796.1 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 616449 (Average: 7.14 Max: 422 Sum: 4404496) Executed : 616393 (Average: 7.14 Max: 422 Sum: 4403379 Ratio: 99.97%) Bounded : 56 (Average: 19.95 Max: 87 Sum: 1117 Ratio: 0.03%) Rules : 94613 (Original: 86518) Atoms : 45936 Bodies : 40692 (Original: 32596) Count : 619 (Original: 1518) Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) Tight : Yes Variables : 373047 (Eliminated: 8994 Frozen: 364053) Constraints : 2752926 (Binary: 91.5% Ternary: 6.6% Other: 2.0%) Memory Peak : 570MB Max. Length : 85 steps Models : 1 [endof: stats after solve call] Solving Time: 18.89s Memory: 539MB (+0MB) UNKNOWN Iteration Time: 18.93s Iteration 26 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)] Grounded Until: 85 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 27 Time : 401.087s (Solving: 385.29s 1st Model: 0.00s Unsat: 7.40s) CPU Time : 401.176s Choices : 5047045 (Domain: 4930963) Conflicts : 644660 (Analyzed: 644657) Restarts : 2294 (Average: 281.02 Last: 208) Model-Level : 212.0 Problems : 27 (Average Length: 49.78 Splits: 0) Lemmas : 644657 (Deleted: 605343) Binary : 15109 (Ratio: 2.34%) Ternary : 2628 (Ratio: 0.41%) Conflict : 644657 (Average Length: 801.5 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 644657 (Average: 7.13 Max: 422 Sum: 4599188) Executed : 644601 (Average: 7.13 Max: 422 Sum: 4598071 Ratio: 99.98%) Bounded : 56 (Average: 19.95 Max: 87 Sum: 1117 Ratio: 0.02%) Rules : 94613 (Original: 86518) Atoms : 45936 Bodies : 40692 (Original: 32596) Count : 619 (Original: 1518) Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) Tight : Yes Variables : 373047 (Eliminated: 8994 Frozen: 364053) Constraints : 2752926 (Binary: 91.5% Ternary: 6.6% Other: 2.0%) Memory Peak : 570MB Max. Length : 85 steps Models : 1 [endof: stats after solve call] Solving Time: 18.88s Memory: 539MB (+0MB) UNKNOWN Iteration Time: 18.93s Iteration 27 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,1,True), (17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] Grounded Until: 85 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 28 Time : 418.204s (Solving: 402.31s 1st Model: 0.00s Unsat: 7.40s) CPU Time : 418.300s Choices : 5239786 (Domain: 5123692) Conflicts : 672866 (Analyzed: 672863) Restarts : 2394 (Average: 281.06 Last: 208) Model-Level : 212.0 Problems : 28 (Average Length: 51.11 Splits: 0) Lemmas : 672863 (Deleted: 629204) Binary : 15390 (Ratio: 2.29%) Ternary : 2662 (Ratio: 0.40%) Conflict : 672863 (Average Length: 807.9 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 672863 (Average: 7.09 Max: 422 Sum: 4768425) Executed : 672806 (Average: 7.08 Max: 422 Sum: 4767221 Ratio: 99.97%) Bounded : 57 (Average: 21.12 Max: 87 Sum: 1204 Ratio: 0.03%) Rules : 94613 (Original: 86518) Atoms : 45936 Bodies : 40692 (Original: 32596) Count : 619 (Original: 1518) Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) Tight : Yes Variables : 373047 (Eliminated: 8994 Frozen: 364053) Constraints : 2752926 (Binary: 91.5% Ternary: 6.6% Other: 2.0%) Memory Peak : 570MB Max. Length : 85 steps Models : 1 [endof: stats after solve call] Solving Time: 17.09s Memory: 539MB (+0MB) UNKNOWN Iteration Time: 17.13s Iteration 28 Queue: [(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)] Grounded Until: 85 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 29 Time : 436.448s (Solving: 420.46s 1st Model: 0.00s Unsat: 7.40s) CPU Time : 436.556s Choices : 5467858 (Domain: 5351680) Conflicts : 701060 (Analyzed: 701057) Restarts : 2494 (Average: 281.10 Last: 208) Model-Level : 212.0 Problems : 29 (Average Length: 52.34 Splits: 0) Lemmas : 701057 (Deleted: 660279) Binary : 15680 (Ratio: 2.24%) Ternary : 2715 (Ratio: 0.39%) Conflict : 701057 (Average Length: 812.9 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 701057 (Average: 7.09 Max: 422 Sum: 4970877) Executed : 701000 (Average: 7.09 Max: 422 Sum: 4969673 Ratio: 99.98%) Bounded : 57 (Average: 21.12 Max: 87 Sum: 1204 Ratio: 0.02%) Rules : 94613 (Original: 86518) Atoms : 45936 Bodies : 40692 (Original: 32596) Count : 619 (Original: 1518) Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) Tight : Yes Variables : 373047 (Eliminated: 8994 Frozen: 364053) Constraints : 2752943 (Binary: 91.5% Ternary: 6.6% Other: 2.0%) Memory Peak : 570MB Max. Length : 85 steps Models : 1 [endof: stats after solve call] Solving Time: 18.21s Memory: 539MB (+0MB) UNKNOWN Iteration Time: 18.25s Iteration 29 Queue: [(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)] Grounded Until: 85 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 30 Time : 454.565s (Solving: 438.46s 1st Model: 0.00s Unsat: 7.40s) CPU Time : 454.680s Choices : 5730727 (Domain: 5611371) Conflicts : 729232 (Analyzed: 729229) Restarts : 2594 (Average: 281.12 Last: 208) Model-Level : 212.0 Problems : 30 (Average Length: 53.50 Splits: 0) Lemmas : 729229 (Deleted: 687180) Binary : 16233 (Ratio: 2.23%) Ternary : 2797 (Ratio: 0.38%) Conflict : 729229 (Average Length: 817.1 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 729229 (Average: 7.13 Max: 422 Sum: 5202937) Executed : 729172 (Average: 7.13 Max: 422 Sum: 5201733 Ratio: 99.98%) Bounded : 57 (Average: 21.12 Max: 87 Sum: 1204 Ratio: 0.02%) Rules : 94613 (Original: 86518) Atoms : 45936 Bodies : 40692 (Original: 32596) Count : 619 (Original: 1518) Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) Tight : Yes Variables : 373047 (Eliminated: 8994 Frozen: 364053) Constraints : 2752943 (Binary: 91.5% Ternary: 6.6% Other: 2.0%) Memory Peak : 570MB Max. Length : 85 steps Models : 1 [endof: stats after solve call] Solving Time: 18.08s Memory: 539MB (+0MB) UNKNOWN Iteration Time: 18.13s Iteration 30 Queue: [(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)] Grounded Until: 85 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 31 Time : 473.320s (Solving: 457.13s 1st Model: 0.00s Unsat: 7.40s) CPU Time : 473.444s Choices : 5981872 (Domain: 5862089) Conflicts : 757399 (Analyzed: 757396) Restarts : 2694 (Average: 281.14 Last: 208) Model-Level : 212.0 Problems : 31 (Average Length: 54.58 Splits: 0) Lemmas : 757396 (Deleted: 714426) Binary : 16612 (Ratio: 2.19%) Ternary : 2876 (Ratio: 0.38%) Conflict : 757396 (Average Length: 824.6 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 757396 (Average: 7.16 Max: 422 Sum: 5421783) Executed : 757339 (Average: 7.16 Max: 422 Sum: 5420579 Ratio: 99.98%) Bounded : 57 (Average: 21.12 Max: 87 Sum: 1204 Ratio: 0.02%) Rules : 94613 (Original: 86518) Atoms : 45936 Bodies : 40692 (Original: 32596) Count : 619 (Original: 1518) Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) Tight : Yes Variables : 373047 (Eliminated: 8994 Frozen: 364053) Constraints : 2752943 (Binary: 91.5% Ternary: 6.6% Other: 2.0%) Memory Peak : 570MB Max. Length : 85 steps Models : 1 [endof: stats after solve call] Solving Time: 18.73s Memory: 539MB (+0MB) UNKNOWN Iteration Time: 18.77s Iteration 31 Queue: [(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)] Grounded Until: 85 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 32 Time : 492.304s (Solving: 476.02s 1st Model: 0.00s Unsat: 7.40s) CPU Time : 492.436s Choices : 6228255 (Domain: 6106842) Conflicts : 785595 (Analyzed: 785592) Restarts : 2794 (Average: 281.17 Last: 208) Model-Level : 212.0 Problems : 32 (Average Length: 55.59 Splits: 0) Lemmas : 785592 (Deleted: 741922) Binary : 16886 (Ratio: 2.15%) Ternary : 2920 (Ratio: 0.37%) Conflict : 785592 (Average Length: 824.3 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 785592 (Average: 7.18 Max: 422 Sum: 5638165) Executed : 785535 (Average: 7.18 Max: 422 Sum: 5636961 Ratio: 99.98%) Bounded : 57 (Average: 21.12 Max: 87 Sum: 1204 Ratio: 0.02%) Rules : 94613 (Original: 86518) Atoms : 45936 Bodies : 40692 (Original: 32596) Count : 619 (Original: 1518) Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) Tight : Yes Variables : 373047 (Eliminated: 8994 Frozen: 364053) Constraints : 2752943 (Binary: 91.5% Ternary: 6.6% Other: 2.0%) Memory Peak : 570MB Max. Length : 85 steps Models : 1 [endof: stats after solve call] Solving Time: 18.96s Memory: 539MB (+0MB) UNKNOWN Iteration Time: 18.99s Iteration 32 Queue: [(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)] Grounded Until: 85 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 33 Time : 510.250s (Solving: 493.88s 1st Model: 0.00s Unsat: 7.40s) CPU Time : 510.388s Choices : 6411718 (Domain: 6290301) Conflicts : 813772 (Analyzed: 813769) Restarts : 2894 (Average: 281.19 Last: 208) Model-Level : 212.0 Problems : 33 (Average Length: 56.55 Splits: 0) Lemmas : 813769 (Deleted: 769442) Binary : 17087 (Ratio: 2.10%) Ternary : 2949 (Ratio: 0.36%) Conflict : 813769 (Average Length: 824.7 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 813769 (Average: 7.12 Max: 422 Sum: 5794406) Executed : 813712 (Average: 7.12 Max: 422 Sum: 5793202 Ratio: 99.98%) Bounded : 57 (Average: 21.12 Max: 87 Sum: 1204 Ratio: 0.02%) Rules : 94613 (Original: 86518) Atoms : 45936 Bodies : 40692 (Original: 32596) Count : 619 (Original: 1518) Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) Tight : Yes Variables : 373047 (Eliminated: 8994 Frozen: 364053) Constraints : 2752943 (Binary: 91.5% Ternary: 6.6% Other: 2.0%) Memory Peak : 570MB Max. Length : 85 steps Models : 1 [endof: stats after solve call] Solving Time: 17.92s Memory: 539MB (+0MB) UNKNOWN Iteration Time: 17.96s Iteration 33 Queue: [(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)] Grounded Until: 85 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 34 Time : 528.226s (Solving: 511.78s 1st Model: 0.00s Unsat: 7.40s) CPU Time : 528.372s Choices : 6782170 (Domain: 6651138) Conflicts : 841921 (Analyzed: 841918) Restarts : 2994 (Average: 281.20 Last: 208) Model-Level : 212.0 Problems : 34 (Average Length: 57.44 Splits: 0) Lemmas : 841918 (Deleted: 796005) Binary : 17873 (Ratio: 2.12%) Ternary : 3072 (Ratio: 0.36%) Conflict : 841918 (Average Length: 818.9 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 841918 (Average: 7.28 Max: 422 Sum: 6127115) Executed : 841861 (Average: 7.28 Max: 422 Sum: 6125911 Ratio: 99.98%) Bounded : 57 (Average: 21.12 Max: 87 Sum: 1204 Ratio: 0.02%) Rules : 94613 (Original: 86518) Atoms : 45936 Bodies : 40692 (Original: 32596) Count : 619 (Original: 1518) Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) Tight : Yes Variables : 373047 (Eliminated: 8994 Frozen: 364053) Constraints : 2752943 (Binary: 91.5% Ternary: 6.6% Other: 2.0%) Memory Peak : 570MB Max. Length : 85 steps Models : 1 [endof: stats after solve call] Solving Time: 17.96s Memory: 539MB (+0MB) UNKNOWN Iteration Time: 17.99s Iteration 34 Queue: [(16,80,1,True), (17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] Grounded Until: 85 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 35 Time : 548.030s (Solving: 531.50s 1st Model: 0.00s Unsat: 7.40s) CPU Time : 548.184s Choices : 7064505 (Domain: 6933096) Conflicts : 870060 (Analyzed: 870057) Restarts : 3094 (Average: 281.21 Last: 208) Model-Level : 212.0 Problems : 35 (Average Length: 58.29 Splits: 0) Lemmas : 870057 (Deleted: 823431) Binary : 18171 (Ratio: 2.09%) Ternary : 3117 (Ratio: 0.36%) Conflict : 870057 (Average Length: 820.4 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 870057 (Average: 7.32 Max: 422 Sum: 6371425) Executed : 870000 (Average: 7.32 Max: 422 Sum: 6370221 Ratio: 99.98%) Bounded : 57 (Average: 21.12 Max: 87 Sum: 1204 Ratio: 0.02%) Rules : 94613 (Original: 86518) Atoms : 45936 Bodies : 40692 (Original: 32596) Count : 619 (Original: 1518) Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) Tight : Yes Variables : 373047 (Eliminated: 8994 Frozen: 364053) Constraints : 2752943 (Binary: 91.5% Ternary: 6.6% Other: 2.0%) Memory Peak : 570MB Max. Length : 85 steps Models : 1 [endof: stats after solve call] Solving Time: 19.78s Memory: 539MB (+0MB) UNKNOWN Iteration Time: 19.81s Iteration 35 Queue: [(17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] Grounded Until: 85 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 36 Time : 566.296s (Solving: 549.68s 1st Model: 0.00s Unsat: 7.40s) CPU Time : 566.460s Choices : 7461431 (Domain: 7325234) Conflicts : 898209 (Analyzed: 898206) Restarts : 3194 (Average: 281.22 Last: 208) Model-Level : 212.0 Problems : 36 (Average Length: 59.08 Splits: 0) Lemmas : 898206 (Deleted: 850370) Binary : 18778 (Ratio: 2.09%) Ternary : 3193 (Ratio: 0.36%) Conflict : 898206 (Average Length: 822.2 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 898206 (Average: 7.49 Max: 422 Sum: 6724056) Executed : 898149 (Average: 7.48 Max: 422 Sum: 6722852 Ratio: 99.98%) Bounded : 57 (Average: 21.12 Max: 87 Sum: 1204 Ratio: 0.02%) Rules : 94613 (Original: 86518) Atoms : 45936 Bodies : 40692 (Original: 32596) Count : 619 (Original: 1518) Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) Tight : Yes Variables : 373047 (Eliminated: 8994 Frozen: 364053) Constraints : 2752943 (Binary: 91.5% Ternary: 6.6% Other: 2.0%) Memory Peak : 570MB Max. Length : 85 steps Models : 1 [endof: stats after solve call] Solving Time: 18.24s Memory: 539MB (+0MB) UNKNOWN Iteration Time: 18.28s Iteration 36 Queue: [(18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] Grounded Until: 85 Expected Memory: 621.0MB Grounding... [('step', [86]), ('step', [87]), ('step', [88]), ('step', [89]), ('step', [90]), ('check', [90])] Grounding Time: 0.32s Memory: 539MB (+0MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 37 Time : 582.807s (Solving: 565.20s 1st Model: 0.00s Unsat: 7.40s) CPU Time : 582.980s Choices : 7643277 (Domain: 7507080) Conflicts : 926448 (Analyzed: 926445) Restarts : 3294 (Average: 281.25 Last: 208) Model-Level : 212.0 Problems : 37 (Average Length: 59.97 Splits: 0) Lemmas : 926445 (Deleted: 874406) Binary : 18949 (Ratio: 2.05%) Ternary : 3224 (Ratio: 0.35%) Conflict : 926445 (Average Length: 811.3 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 926445 (Average: 7.42 Max: 422 Sum: 6878725) Executed : 926388 (Average: 7.42 Max: 422 Sum: 6877521 Ratio: 99.98%) Bounded : 57 (Average: 21.12 Max: 87 Sum: 1204 Ratio: 0.02%) Rules : 94613 (Original: 86518) Atoms : 45936 Bodies : 40692 (Original: 32596) Count : 619 (Original: 1518) Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) Tight : Yes Variables : 395608 (Eliminated: 8994 Frozen: 379084) Constraints : 2925968 (Binary: 91.5% Ternary: 6.6% Other: 2.0%) Memory Peak : 589MB Max. Length : 85 steps Models : 1 [endof: stats after solve call] Solving Time: 15.92s Memory: 551MB (+12MB) UNKNOWN Iteration Time: 16.53s Iteration 37 Queue: [(19,95,0,True), (20,100,0,True), (21,105,0,True)] Grounded Until: 90 Expected Memory: 633.0MB Grounding... [('step', [91]), ('step', [92]), ('step', [93]), ('step', [94]), ('step', [95]), ('check', [95])] Grounding Time: 0.31s Memory: 551MB (+0MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 38 Time : 604.129s (Solving: 585.54s 1st Model: 0.00s Unsat: 7.40s) CPU Time : 604.308s Choices : 7887991 (Domain: 7751790) Conflicts : 954605 (Analyzed: 954602) Restarts : 3394 (Average: 281.26 Last: 208) Model-Level : 212.0 Problems : 38 (Average Length: 60.95 Splits: 0) Lemmas : 954602 (Deleted: 905607) Binary : 19248 (Ratio: 2.02%) Ternary : 3267 (Ratio: 0.34%) Conflict : 954602 (Average Length: 818.0 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 954602 (Average: 7.42 Max: 426 Sum: 7083953) Executed : 954545 (Average: 7.42 Max: 426 Sum: 7082749 Ratio: 99.98%) Bounded : 57 (Average: 21.12 Max: 87 Sum: 1204 Ratio: 0.02%) Rules : 94613 (Original: 86518) Atoms : 45936 Bodies : 40692 (Original: 32596) Count : 619 (Original: 1518) Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) Tight : Yes Variables : 418169 (Eliminated: 8994 Frozen: 401645) Constraints : 3098993 (Binary: 91.5% Ternary: 6.6% Other: 2.0%) Memory Peak : 609MB Max. Length : 90 steps Models : 1 [endof: stats after solve call] Solving Time: 20.74s Memory: 573MB (+22MB) UNKNOWN Iteration Time: 21.34s Iteration 38 Queue: [(20,100,0,True), (21,105,0,True)] Grounded Until: 95 Expected Memory: 655.0MB Grounding... [('step', [96]), ('step', [97]), ('step', [98]), ('step', [99]), ('step', [100]), ('check', [100])] Grounding Time: 0.34s Memory: 573MB (+0MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 39 Time : 622.153s (Solving: 602.52s 1st Model: 0.00s Unsat: 7.40s) CPU Time : 622.340s Choices : 8085108 (Domain: 7948889) Conflicts : 982843 (Analyzed: 982840) Restarts : 3494 (Average: 281.29 Last: 208) Model-Level : 212.0 Problems : 39 (Average Length: 62.00 Splits: 0) Lemmas : 982840 (Deleted: 933407) Binary : 19431 (Ratio: 1.98%) Ternary : 3289 (Ratio: 0.33%) Conflict : 982840 (Average Length: 809.3 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 982840 (Average: 7.37 Max: 426 Sum: 7248294) Executed : 982782 (Average: 7.37 Max: 426 Sum: 7246988 Ratio: 99.98%) Bounded : 58 (Average: 22.52 Max: 102 Sum: 1306 Ratio: 0.02%) Rules : 94613 (Original: 86518) Atoms : 45936 Bodies : 40692 (Original: 32596) Count : 619 (Original: 1518) Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) Tight : Yes Variables : 440730 (Eliminated: 8994 Frozen: 424206) Constraints : 3272018 (Binary: 91.5% Ternary: 6.6% Other: 2.0%) Memory Peak : 627MB Max. Length : 95 steps Models : 1 [endof: stats after solve call] Solving Time: 17.39s Memory: 626MB (+53MB) UNKNOWN Iteration Time: 18.04s Iteration 39 Queue: [(21,105,0,True)] Grounded Until: 100 Expected Memory: 708.0MB Grounding... [('step', [101]), ('step', [102]), ('step', [103]), ('step', [104]), ('step', [105]), ('check', [105])] Grounding Time: 0.35s Memory: 626MB (+0MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 40 Time : 640.838s (Solving: 620.15s 1st Model: 0.00s Unsat: 7.40s) CPU Time : 641.032s Choices : 8299964 (Domain: 8163588) Conflicts : 1011054 (Analyzed: 1011051) Restarts : 3594 (Average: 281.32 Last: 208) Model-Level : 212.0 Problems : 40 (Average Length: 63.12 Splits: 0) Lemmas : 1011051 (Deleted: 960990) Binary : 19575 (Ratio: 1.94%) Ternary : 3324 (Ratio: 0.33%) Conflict : 1011051 (Average Length: 803.4 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 1011051 (Average: 7.35 Max: 426 Sum: 7430291) Executed : 1010993 (Average: 7.35 Max: 426 Sum: 7428985 Ratio: 99.98%) Bounded : 58 (Average: 22.52 Max: 102 Sum: 1306 Ratio: 0.02%) Rules : 94613 (Original: 86518) Atoms : 45936 Bodies : 40692 (Original: 32596) Count : 619 (Original: 1518) Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) Tight : Yes Variables : 463291 (Eliminated: 8994 Frozen: 446767) Constraints : 3445029 (Binary: 91.5% Ternary: 6.6% Other: 2.0%) Memory Peak : 682MB Max. Length : 100 steps Models : 1 [endof: stats after solve call] Solving Time: 18.04s Memory: 629MB (+3MB) UNKNOWN Iteration Time: 18.70s Iteration 40 Queue: [(4,20,3,True), (5,25,3,True), (6,30,3,True), (7,35,2,True), (8,40,2,True), (9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,2,False), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] Grounded Until: 105 Blocking actions... Solving... [start: stats after solve call] Models : 0 Calls : 41 Time : 650.250s (Solving: 629.43s 1st Model: 0.00s Unsat: 16.67s) CPU Time : 650.448s Choices : 8456222 (Domain: 8319846) Conflicts : 1039175 (Analyzed: 1039171) Restarts : 3693 (Average: 281.39 Last: 208) Model-Level : 212.0 Problems : 41 (Average Length: 64.20 Splits: 0) Lemmas : 1039171 (Deleted: 988171) Binary : 19785 (Ratio: 1.90%) Ternary : 3407 (Ratio: 0.33%) Conflict : 1039171 (Average Length: 789.2 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 1039171 (Average: 7.29 Max: 426 Sum: 7580351) Executed : 1039111 (Average: 7.29 Max: 426 Sum: 7578937 Ratio: 99.98%) Bounded : 60 (Average: 23.57 Max: 107 Sum: 1414 Ratio: 0.02%) Rules : 94613 (Original: 86518) Atoms : 45936 Bodies : 40692 (Original: 32596) Count : 619 (Original: 1518) Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) Tight : Yes Variables : 463291 (Eliminated: 8994 Frozen: 454297) Constraints : 3445029 (Binary: 91.5% Ternary: 6.6% Other: 2.0%) Memory Peak : 682MB Max. Length : 105 steps Models : 1 [endof: stats after solve call] Solving Time: 9.36s Memory: 629MB (+0MB) UNSAT Iteration Time: 9.42s Iteration 41 Queue: [(5,25,3,True), (6,30,3,True), (7,35,2,True), (8,40,2,True), (9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,2,False), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] Grounded Until: 105 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 42 Time : 675.013s (Solving: 654.09s 1st Model: 0.00s Unsat: 16.67s) CPU Time : 675.224s Choices : 8601062 (Domain: 8464686) Conflicts : 1067320 (Analyzed: 1067316) Restarts : 3793 (Average: 281.39 Last: 208) Model-Level : 212.0 Problems : 42 (Average Length: 65.21 Splits: 0) Lemmas : 1067316 (Deleted: 1015695) Binary : 19938 (Ratio: 1.87%) Ternary : 3428 (Ratio: 0.32%) Conflict : 1067316 (Average Length: 793.8 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 1067316 (Average: 7.23 Max: 426 Sum: 7714494) Executed : 1067255 (Average: 7.23 Max: 426 Sum: 7712973 Ratio: 99.98%) Bounded : 61 (Average: 24.93 Max: 107 Sum: 1521 Ratio: 0.02%) Rules : 94613 (Original: 86518) Atoms : 45936 Bodies : 40692 (Original: 32596) Count : 619 (Original: 1518) Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) Tight : Yes Variables : 463291 (Eliminated: 8994 Frozen: 454297) Constraints : 3445015 (Binary: 91.5% Ternary: 6.6% Other: 2.0%) Memory Peak : 682MB Max. Length : 105 steps Models : 1 [endof: stats after solve call] Solving Time: 24.74s Memory: 629MB (+0MB) UNKNOWN Iteration Time: 24.78s Iteration 42 Queue: [(6,30,3,True), (7,35,2,True), (8,40,2,True), (9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,2,False), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] Grounded Until: 105 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 43 Time : 700.352s (Solving: 679.31s 1st Model: 0.00s Unsat: 16.67s) CPU Time : 700.576s Choices : 8769209 (Domain: 8632833) Conflicts : 1095491 (Analyzed: 1095487) Restarts : 3893 (Average: 281.40 Last: 208) Model-Level : 212.0 Problems : 43 (Average Length: 66.19 Splits: 0) Lemmas : 1095487 (Deleted: 1043519) Binary : 20111 (Ratio: 1.84%) Ternary : 3439 (Ratio: 0.31%) Conflict : 1095487 (Average Length: 818.0 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 1095487 (Average: 7.18 Max: 426 Sum: 7864412) Executed : 1095426 (Average: 7.18 Max: 426 Sum: 7862891 Ratio: 99.98%) Bounded : 61 (Average: 24.93 Max: 107 Sum: 1521 Ratio: 0.02%) Rules : 94613 (Original: 86518) Atoms : 45936 Bodies : 40692 (Original: 32596) Count : 619 (Original: 1518) Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) Tight : Yes Variables : 463291 (Eliminated: 8994 Frozen: 454297) Constraints : 3445001 (Binary: 91.5% Ternary: 6.6% Other: 2.0%) Memory Peak : 693MB Max. Length : 105 steps Models : 1 [endof: stats after solve call] Solving Time: 25.30s Memory: 693MB (+64MB) UNKNOWN Iteration Time: 25.35s Iteration 43 Queue: [(7,35,2,True), (8,40,2,True), (9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,2,False), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] Grounded Until: 105 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 44 Time : 718.784s (Solving: 697.64s 1st Model: 0.00s Unsat: 16.67s) CPU Time : 719.016s Choices : 8947892 (Domain: 8811516) Conflicts : 1123688 (Analyzed: 1123684) Restarts : 3993 (Average: 281.41 Last: 208) Model-Level : 212.0 Problems : 44 (Average Length: 67.11 Splits: 0) Lemmas : 1123684 (Deleted: 1071211) Binary : 20240 (Ratio: 1.80%) Ternary : 3456 (Ratio: 0.31%) Conflict : 1123684 (Average Length: 820.5 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 1123684 (Average: 7.14 Max: 426 Sum: 8021804) Executed : 1123623 (Average: 7.14 Max: 426 Sum: 8020283 Ratio: 99.98%) Bounded : 61 (Average: 24.93 Max: 107 Sum: 1521 Ratio: 0.02%) Rules : 94613 (Original: 86518) Atoms : 45936 Bodies : 40692 (Original: 32596) Count : 619 (Original: 1518) Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) Tight : Yes Variables : 463291 (Eliminated: 8994 Frozen: 454297) Constraints : 3445001 (Binary: 91.5% Ternary: 6.6% Other: 2.0%) Memory Peak : 693MB Max. Length : 105 steps Models : 1 [endof: stats after solve call] Solving Time: 18.40s Memory: 693MB (+0MB) UNKNOWN Iteration Time: 18.44s Iteration 44 Queue: [(8,40,2,True), (9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,2,False), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] Grounded Until: 105 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 45 Time : 736.806s (Solving: 715.53s 1st Model: 0.00s Unsat: 16.67s) CPU Time : 737.048s Choices : 9151203 (Domain: 9014827) Conflicts : 1151869 (Analyzed: 1151865) Restarts : 4093 (Average: 281.42 Last: 208) Model-Level : 212.0 Problems : 45 (Average Length: 68.00 Splits: 0) Lemmas : 1151865 (Deleted: 1098669) Binary : 20406 (Ratio: 1.77%) Ternary : 3501 (Ratio: 0.30%) Conflict : 1151865 (Average Length: 819.5 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 1151865 (Average: 7.12 Max: 426 Sum: 8200967) Executed : 1151804 (Average: 7.12 Max: 426 Sum: 8199446 Ratio: 99.98%) Bounded : 61 (Average: 24.93 Max: 107 Sum: 1521 Ratio: 0.02%) Rules : 94613 (Original: 86518) Atoms : 45936 Bodies : 40692 (Original: 32596) Count : 619 (Original: 1518) Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) Tight : Yes Variables : 463291 (Eliminated: 8994 Frozen: 454297) Constraints : 3445001 (Binary: 91.5% Ternary: 6.6% Other: 2.0%) Memory Peak : 693MB Max. Length : 105 steps Models : 1 [endof: stats after solve call] Solving Time: 17.98s Memory: 693MB (+0MB) UNKNOWN Iteration Time: 18.03s Iteration 45 Queue: [(9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,2,False), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] Grounded Until: 105 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 46 Time : 754.954s (Solving: 733.57s 1st Model: 0.00s Unsat: 16.67s) CPU Time : 755.204s Choices : 9352554 (Domain: 9215956) Conflicts : 1180060 (Analyzed: 1180056) Restarts : 4193 (Average: 281.43 Last: 208) Model-Level : 212.0 Problems : 46 (Average Length: 68.85 Splits: 0) Lemmas : 1180056 (Deleted: 1126024) Binary : 20672 (Ratio: 1.75%) Ternary : 3546 (Ratio: 0.30%) Conflict : 1180056 (Average Length: 820.8 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 1180056 (Average: 7.10 Max: 426 Sum: 8376547) Executed : 1179995 (Average: 7.10 Max: 426 Sum: 8375026 Ratio: 99.98%) Bounded : 61 (Average: 24.93 Max: 107 Sum: 1521 Ratio: 0.02%) Rules : 94613 (Original: 86518) Atoms : 45936 Bodies : 40692 (Original: 32596) Count : 619 (Original: 1518) Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) Tight : Yes Variables : 463291 (Eliminated: 8994 Frozen: 454297) Constraints : 3445001 (Binary: 91.5% Ternary: 6.6% Other: 2.0%) Memory Peak : 693MB Max. Length : 105 steps Models : 1 [endof: stats after solve call] Solving Time: 18.12s Memory: 693MB (+0MB) UNKNOWN Iteration Time: 18.16s Iteration 46 Queue: [(10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,2,False), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] Grounded Until: 105 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 47 Time : 772.790s (Solving: 751.28s 1st Model: 0.00s Unsat: 16.67s) CPU Time : 773.048s Choices : 9572653 (Domain: 9435574) Conflicts : 1208245 (Analyzed: 1208241) Restarts : 4293 (Average: 281.44 Last: 208) Model-Level : 212.0 Problems : 47 (Average Length: 69.66 Splits: 0) Lemmas : 1208241 (Deleted: 1153476) Binary : 20930 (Ratio: 1.73%) Ternary : 3599 (Ratio: 0.30%) Conflict : 1208241 (Average Length: 823.0 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 1208241 (Average: 7.09 Max: 426 Sum: 8566212) Executed : 1208180 (Average: 7.09 Max: 426 Sum: 8564691 Ratio: 99.98%) Bounded : 61 (Average: 24.93 Max: 107 Sum: 1521 Ratio: 0.02%) Rules : 94613 (Original: 86518) Atoms : 45936 Bodies : 40692 (Original: 32596) Count : 619 (Original: 1518) Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) Tight : Yes Variables : 463291 (Eliminated: 8994 Frozen: 454297) Constraints : 3445001 (Binary: 91.5% Ternary: 6.6% Other: 2.0%) Memory Peak : 693MB Max. Length : 105 steps Models : 1 [endof: stats after solve call] Solving Time: 17.79s Memory: 693MB (+0MB) UNKNOWN Iteration Time: 17.85s Iteration 47 Queue: [(11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,2,False), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] Grounded Until: 105 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 48 Time : 790.010s (Solving: 768.37s 1st Model: 0.00s Unsat: 16.67s) CPU Time : 790.276s Choices : 9786609 (Domain: 9649467) Conflicts : 1236454 (Analyzed: 1236450) Restarts : 4393 (Average: 281.46 Last: 208) Model-Level : 212.0 Problems : 48 (Average Length: 70.44 Splits: 0) Lemmas : 1236450 (Deleted: 1181052) Binary : 21219 (Ratio: 1.72%) Ternary : 3640 (Ratio: 0.29%) Conflict : 1236450 (Average Length: 824.1 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 1236450 (Average: 7.08 Max: 426 Sum: 8748483) Executed : 1236389 (Average: 7.07 Max: 426 Sum: 8746962 Ratio: 99.98%) Bounded : 61 (Average: 24.93 Max: 107 Sum: 1521 Ratio: 0.02%) Rules : 94613 (Original: 86518) Atoms : 45936 Bodies : 40692 (Original: 32596) Count : 619 (Original: 1518) Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) Tight : Yes Variables : 463291 (Eliminated: 8994 Frozen: 454297) Constraints : 3445001 (Binary: 91.5% Ternary: 6.6% Other: 2.0%) Memory Peak : 693MB Max. Length : 105 steps Models : 1 [endof: stats after solve call] Solving Time: 17.18s Memory: 693MB (+0MB) UNKNOWN Iteration Time: 17.23s Iteration 48 Queue: [(12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,2,False), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] Grounded Until: 105 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 49 Time : 806.202s (Solving: 784.44s 1st Model: 0.00s Unsat: 16.67s) CPU Time : 806.472s Choices : 10026136 (Domain: 9888329) Conflicts : 1264633 (Analyzed: 1264629) Restarts : 4493 (Average: 281.47 Last: 208) Model-Level : 212.0 Problems : 49 (Average Length: 71.18 Splits: 0) Lemmas : 1264629 (Deleted: 1208327) Binary : 21668 (Ratio: 1.71%) Ternary : 3674 (Ratio: 0.29%) Conflict : 1264629 (Average Length: 824.8 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 1264629 (Average: 7.08 Max: 426 Sum: 8948813) Executed : 1264568 (Average: 7.08 Max: 426 Sum: 8947292 Ratio: 99.98%) Bounded : 61 (Average: 24.93 Max: 107 Sum: 1521 Ratio: 0.02%) Rules : 94613 (Original: 86518) Atoms : 45936 Bodies : 40692 (Original: 32596) Count : 619 (Original: 1518) Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) Tight : Yes Variables : 463291 (Eliminated: 8994 Frozen: 454297) Constraints : 3445001 (Binary: 91.5% Ternary: 6.6% Other: 2.0%) Memory Peak : 693MB Max. Length : 105 steps Models : 1 [endof: stats after solve call] Solving Time: 16.15s Memory: 693MB (+0MB) UNKNOWN Iteration Time: 16.20s Iteration 49 Queue: [(13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,2,False), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] Grounded Until: 105 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 50 Time : 823.151s (Solving: 801.27s 1st Model: 0.00s Unsat: 16.67s) CPU Time : 823.428s Choices : 10216776 (Domain: 10078969) Conflicts : 1292793 (Analyzed: 1292789) Restarts : 4593 (Average: 281.47 Last: 208) Model-Level : 212.0 Problems : 50 (Average Length: 71.90 Splits: 0) Lemmas : 1292789 (Deleted: 1235993) Binary : 21766 (Ratio: 1.68%) Ternary : 3686 (Ratio: 0.29%) Conflict : 1292789 (Average Length: 824.2 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 1292789 (Average: 7.05 Max: 426 Sum: 9110026) Executed : 1292728 (Average: 7.05 Max: 426 Sum: 9108505 Ratio: 99.98%) Bounded : 61 (Average: 24.93 Max: 107 Sum: 1521 Ratio: 0.02%) Rules : 94613 (Original: 86518) Atoms : 45936 Bodies : 40692 (Original: 32596) Count : 619 (Original: 1518) Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) Tight : Yes Variables : 463291 (Eliminated: 8994 Frozen: 454297) Constraints : 3445001 (Binary: 91.5% Ternary: 6.6% Other: 2.0%) Memory Peak : 693MB Max. Length : 105 steps Models : 1 [endof: stats after solve call] Solving Time: 16.91s Memory: 693MB (+0MB) UNKNOWN Iteration Time: 16.96s Iteration 50 Queue: [(18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] Grounded Until: 105 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 51 Time : 843.238s (Solving: 821.23s 1st Model: 0.00s Unsat: 16.67s) CPU Time : 843.524s Choices : 10496385 (Domain: 10358552) Conflicts : 1320996 (Analyzed: 1320992) Restarts : 4693 (Average: 281.48 Last: 208) Model-Level : 212.0 Problems : 51 (Average Length: 72.59 Splits: 0) Lemmas : 1320992 (Deleted: 1263506) Binary : 22044 (Ratio: 1.67%) Ternary : 3737 (Ratio: 0.28%) Conflict : 1320992 (Average Length: 826.7 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 1320992 (Average: 7.08 Max: 426 Sum: 9351586) Executed : 1320931 (Average: 7.08 Max: 426 Sum: 9350065 Ratio: 99.98%) Bounded : 61 (Average: 24.93 Max: 107 Sum: 1521 Ratio: 0.02%) Rules : 94613 (Original: 86518) Atoms : 45936 Bodies : 40692 (Original: 32596) Count : 619 (Original: 1518) Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) Tight : Yes Variables : 463291 (Eliminated: 8994 Frozen: 454297) Constraints : 3445001 (Binary: 91.5% Ternary: 6.6% Other: 2.0%) Memory Peak : 693MB Max. Length : 105 steps Models : 1 [endof: stats after solve call] Solving Time: 20.05s Memory: 693MB (+0MB) UNKNOWN Iteration Time: 20.10s Iteration 51 Queue: [(19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] Grounded Until: 105 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 52 Time : 862.265s (Solving: 840.15s 1st Model: 0.00s Unsat: 16.67s) CPU Time : 862.560s Choices : 10764696 (Domain: 10626340) Conflicts : 1349196 (Analyzed: 1349192) Restarts : 4793 (Average: 281.49 Last: 208) Model-Level : 212.0 Problems : 52 (Average Length: 73.25 Splits: 0) Lemmas : 1349192 (Deleted: 1291046) Binary : 22249 (Ratio: 1.65%) Ternary : 3767 (Ratio: 0.28%) Conflict : 1349192 (Average Length: 828.5 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 1349192 (Average: 7.10 Max: 426 Sum: 9578947) Executed : 1349131 (Average: 7.10 Max: 426 Sum: 9577426 Ratio: 99.98%) Bounded : 61 (Average: 24.93 Max: 107 Sum: 1521 Ratio: 0.02%) Rules : 94613 (Original: 86518) Atoms : 45936 Bodies : 40692 (Original: 32596) Count : 619 (Original: 1518) Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) Tight : Yes Variables : 463291 (Eliminated: 8994 Frozen: 454297) Constraints : 3445001 (Binary: 91.5% Ternary: 6.6% Other: 2.0%) Memory Peak : 693MB Max. Length : 105 steps Models : 1 [endof: stats after solve call] Solving Time: 19.00s Memory: 693MB (+0MB) UNKNOWN Iteration Time: 19.04s Iteration 52 Queue: [(20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] Grounded Until: 105 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 53 Time : 883.700s (Solving: 861.48s 1st Model: 0.00s Unsat: 16.67s) CPU Time : 884.004s Choices : 11013874 (Domain: 10875518) Conflicts : 1377434 (Analyzed: 1377430) Restarts : 4893 (Average: 281.51 Last: 208) Model-Level : 212.0 Problems : 53 (Average Length: 73.89 Splits: 0) Lemmas : 1377430 (Deleted: 1318807) Binary : 22405 (Ratio: 1.63%) Ternary : 3804 (Ratio: 0.28%) Conflict : 1377430 (Average Length: 834.0 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 1377430 (Average: 7.10 Max: 426 Sum: 9783579) Executed : 1377369 (Average: 7.10 Max: 426 Sum: 9782058 Ratio: 99.98%) Bounded : 61 (Average: 24.93 Max: 107 Sum: 1521 Ratio: 0.02%) Rules : 94613 (Original: 86518) Atoms : 45936 Bodies : 40692 (Original: 32596) Count : 619 (Original: 1518) Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) Tight : Yes Variables : 463291 (Eliminated: 8994 Frozen: 454297) Constraints : 3445001 (Binary: 91.5% Ternary: 6.6% Other: 2.0%) Memory Peak : 693MB Max. Length : 105 steps Models : 1 [endof: stats after solve call] Solving Time: 21.41s Memory: 693MB (+0MB) UNKNOWN Iteration Time: 21.45s Iteration 53 Queue: [(21,105,1,True), (22,110,0,True), (23,115,0,True)] Grounded Until: 105 Unblocking actions... Solving... *** Info : (planner): INTERRUPTED by signal! UNKNOWN INTERRUPTED : 1 Models : 0+ Calls : 54 Time : 894.855s (Solving: 872.53s 1st Model: 0.00s Unsat: 16.67s) CPU Time : 895.144s Choices : 11145256 (Domain: 11006899) Conflicts : 1391952 (Analyzed: 1391948) Restarts : 4954 (Average: 280.97 Last: 208) Model-Level : 212.0 Problems : 54 (Average Length: 74.50 Splits: 0) Lemmas : 1391948 (Deleted: 1335497) Binary : 22457 (Ratio: 1.61%) Ternary : 3815 (Ratio: 0.27%) Conflict : 1391948 (Average Length: 833.6 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 1391948 (Average: 7.11 Max: 426 Sum: 9892370) Executed : 1391887 (Average: 7.11 Max: 426 Sum: 9890849 Ratio: 99.98%) Bounded : 61 (Average: 24.93 Max: 107 Sum: 1521 Ratio: 0.02%) Rules : 94613 (Original: 86518) Atoms : 45936 Bodies : 40692 (Original: 32596) Count : 619 (Original: 1518) Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) Tight : Yes Variables : 463291 (Eliminated: 8994 Frozen: 454297) Constraints : 3445001 (Binary: 91.5% Ternary: 6.6% Other: 2.0%) Memory Peak : 693MB Max. Length : 105 steps Models : 1