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.037s wall-clock] Normalizing task... [0.000s CPU, 0.003s wall-clock] Instantiating... Generating Datalog program... [0.010s CPU, 0.009s wall-clock] Normalizing Datalog program... Normalizing Datalog program: [0.050s CPU, 0.049s wall-clock] Preparing model... [0.020s CPU, 0.025s wall-clock] Generated 115 rules. Computing model... [0.330s CPU, 0.330s 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.010s CPU, 1.018s wall-clock] Computing fact groups... Finding invariants... 24 initial candidates Finding invariants: [0.100s CPU, 0.097s 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.130s CPU, 0.130s 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.657s 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.207s 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.271s wall-clock] Done! [2.640s CPU, 2.663s wall-clock] planner.py version 0.0.1 Time: 0.57s 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.658s (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 : 1+ Calls : 2 Time : 0.982s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s) CPU Time : 0.892s 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.58s Memory: 178MB (+18MB) Solving... [start: stats after solve call] Models : 0 Calls : 3 Time : 1.081s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s) CPU Time : 0.992s 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.02s Memory: 178MB (+0MB) UNSAT Iteration Time: 0.93s 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.170s (Solving: 0.38s 1st Model: 0.00s Unsat: 0.38s) CPU Time : 2.080s Choices : 12799 (Domain: 10798) Conflicts : 1643 (Analyzed: 1641) Restarts : 10 (Average: 164.10 Last: 20) Model-Level : 147.0 Problems : 4 (Average Length: 7.00 Splits: 0) Lemmas : 1641 (Deleted: 0) Binary : 185 (Ratio: 11.27%) Ternary : 187 (Ratio: 11.40%) Conflict : 1641 (Average Length: 27.6 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 1641 (Average: 7.73 Max: 79 Sum: 12687) Executed : 1623 (Average: 7.62 Max: 79 Sum: 12504 Ratio: 98.56%) Bounded : 18 (Average: 10.17 Max: 12 Sum: 183 Ratio: 1.44%) 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.70s Memory: 189MB (+11MB) UNSAT Iteration Time: 1.10s 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.38s Memory: 195MB (+6MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0 Calls : 5 Time : 6.807s (Solving: 4.20s 1st Model: 0.00s Unsat: 4.20s) CPU Time : 6.720s Choices : 95323 (Domain: 72132) Conflicts : 13704 (Analyzed: 13701) Restarts : 61 (Average: 224.61 Last: 168) Model-Level : 147.0 Problems : 5 (Average Length: 9.00 Splits: 0) Lemmas : 13701 (Deleted: 7320) Binary : 884 (Ratio: 6.45%) Ternary : 495 (Ratio: 3.61%) Conflict : 13701 (Average Length: 196.3 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 13701 (Average: 6.83 Max: 380 Sum: 93639) Executed : 13664 (Average: 6.80 Max: 380 Sum: 93177 Ratio: 99.51%) Bounded : 37 (Average: 12.49 Max: 17 Sum: 462 Ratio: 0.49%) 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 : 381121 (Binary: 91.6% Ternary: 6.3% Other: 2.1%) Memory Peak : 222MB Max. Length : 10 steps Models : 1 [endof: stats after solve call] Solving Time: 4.14s Memory: 209MB (+14MB) UNSAT Iteration Time: 4.65s 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 : 21.097s (Solving: 17.72s 1st Model: 0.00s Unsat: 4.20s) CPU Time : 21.012s Choices : 318692 (Domain: 274484) Conflicts : 41885 (Analyzed: 41882) Restarts : 161 (Average: 260.14 Last: 200) Model-Level : 147.0 Problems : 6 (Average Length: 11.17 Splits: 0) Lemmas : 41882 (Deleted: 27757) Binary : 2114 (Ratio: 5.05%) Ternary : 772 (Ratio: 1.84%) Conflict : 41882 (Average Length: 420.1 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 41882 (Average: 7.36 Max: 431 Sum: 308320) Executed : 41843 (Average: 7.35 Max: 431 Sum: 307814 Ratio: 99.84%) Bounded : 39 (Average: 12.97 Max: 22 Sum: 506 Ratio: 0.16%) 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 : 538293 (Binary: 91.6% Ternary: 6.4% Other: 2.1%) Memory Peak : 227MB Max. Length : 15 steps Models : 1 [endof: stats after solve call] Solving Time: 13.86s Memory: 227MB (+15MB) UNKNOWN Iteration Time: 14.30s 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 : 38.488s (Solving: 34.32s 1st Model: 0.00s Unsat: 4.20s) CPU Time : 38.412s Choices : 544925 (Domain: 486198) Conflicts : 70044 (Analyzed: 70041) Restarts : 261 (Average: 268.36 Last: 203) Model-Level : 147.0 Problems : 7 (Average Length: 13.43 Splits: 0) Lemmas : 70041 (Deleted: 53675) Binary : 3314 (Ratio: 4.73%) Ternary : 972 (Ratio: 1.39%) Conflict : 70041 (Average Length: 595.2 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 70041 (Average: 7.41 Max: 431 Sum: 518924) Executed : 70002 (Average: 7.40 Max: 431 Sum: 518418 Ratio: 99.90%) Bounded : 39 (Average: 12.97 Max: 22 Sum: 506 Ratio: 0.10%) 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 : 711310 (Binary: 91.6% Ternary: 6.4% Other: 2.0%) Memory Peak : 246MB Max. Length : 20 steps Models : 1 [endof: stats after solve call] Solving Time: 16.94s Memory: 242MB (+12MB) UNKNOWN Iteration Time: 17.40s Iteration 7 Queue: [(6,30,0,True)] Grounded Until: 25 Expected Memory: 262.0MB Grounding... [('step', [26]), ('step', [27]), ('step', [28]), ('step', [29]), ('step', [30]), ('check', [30])] Grounding Time: 0.36s Memory: 244MB (+2MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 8 Time : 58.835s (Solving: 53.79s 1st Model: 0.00s Unsat: 4.20s) CPU Time : 58.768s Choices : 795479 (Domain: 727093) Conflicts : 98170 (Analyzed: 98167) Restarts : 361 (Average: 271.93 Last: 203) Model-Level : 147.0 Problems : 8 (Average Length: 15.75 Splits: 0) Lemmas : 98167 (Deleted: 80033) Binary : 4642 (Ratio: 4.73%) Ternary : 1200 (Ratio: 1.22%) Conflict : 98167 (Average Length: 701.2 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 98167 (Average: 7.65 Max: 431 Sum: 751388) Executed : 98127 (Average: 7.65 Max: 431 Sum: 750850 Ratio: 99.93%) Bounded : 40 (Average: 13.45 Max: 32 Sum: 538 Ratio: 0.07%) 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 : 884355 (Binary: 91.6% Ternary: 6.4% Other: 2.0%) Memory Peak : 390MB Max. Length : 25 steps Models : 1 [endof: stats after solve call] Solving Time: 19.83s Memory: 326MB (+82MB) UNKNOWN Iteration Time: 20.36s 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 : 73.429s (Solving: 68.35s 1st Model: 0.00s Unsat: 4.20s) CPU Time : 73.368s Choices : 908988 (Domain: 840602) Conflicts : 126350 (Analyzed: 126347) Restarts : 461 (Average: 274.07 Last: 203) Model-Level : 147.0 Problems : 9 (Average Length: 17.56 Splits: 0) Lemmas : 126347 (Deleted: 107054) Binary : 5110 (Ratio: 4.04%) Ternary : 1272 (Ratio: 1.01%) Conflict : 126347 (Average Length: 680.7 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 126347 (Average: 6.80 Max: 431 Sum: 859482) Executed : 126306 (Average: 6.80 Max: 431 Sum: 858912 Ratio: 99.93%) Bounded : 41 (Average: 13.90 Max: 32 Sum: 570 Ratio: 0.07%) 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 : 884341 (Binary: 91.6% Ternary: 6.4% Other: 2.0%) Memory Peak : 390MB Max. Length : 30 steps Models : 1 [endof: stats after solve call] Solving Time: 14.58s Memory: 326MB (+0MB) UNKNOWN Iteration Time: 14.60s 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 : 98.747s (Solving: 93.63s 1st Model: 0.00s Unsat: 4.20s) CPU Time : 98.696s Choices : 1039074 (Domain: 970650) Conflicts : 154469 (Analyzed: 154466) Restarts : 561 (Average: 275.34 Last: 204) Model-Level : 147.0 Problems : 10 (Average Length: 19.00 Splits: 0) Lemmas : 154466 (Deleted: 134626) Binary : 5352 (Ratio: 3.46%) Ternary : 1336 (Ratio: 0.86%) Conflict : 154466 (Average Length: 791.7 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 154466 (Average: 6.32 Max: 431 Sum: 976481) Executed : 154424 (Average: 6.32 Max: 431 Sum: 975879 Ratio: 99.94%) Bounded : 42 (Average: 14.33 Max: 32 Sum: 602 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 : 125615 (Eliminated: 1464 Frozen: 124151) Constraints : 884328 (Binary: 91.6% Ternary: 6.4% Other: 2.0%) Memory Peak : 390MB Max. Length : 30 steps Models : 1 [endof: stats after solve call] Solving Time: 25.32s Memory: 326MB (+0MB) UNKNOWN Iteration Time: 25.33s 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 : 121.765s (Solving: 116.61s 1st Model: 0.00s Unsat: 4.20s) CPU Time : 121.724s Choices : 1259852 (Domain: 1190405) Conflicts : 182648 (Analyzed: 182645) Restarts : 661 (Average: 276.32 Last: 204) Model-Level : 147.0 Problems : 11 (Average Length: 20.18 Splits: 0) Lemmas : 182645 (Deleted: 161750) Binary : 5826 (Ratio: 3.19%) Ternary : 1427 (Ratio: 0.78%) Conflict : 182645 (Average Length: 840.8 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 182645 (Average: 6.46 Max: 431 Sum: 1180686) Executed : 182602 (Average: 6.46 Max: 431 Sum: 1180052 Ratio: 99.95%) Bounded : 43 (Average: 14.74 Max: 32 Sum: 634 Ratio: 0.05%) 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 : 884314 (Binary: 91.6% Ternary: 6.4% Other: 2.0%) Memory Peak : 390MB Max. Length : 30 steps Models : 1 [endof: stats after solve call] Solving Time: 23.01s Memory: 326MB (+0MB) UNKNOWN Iteration Time: 23.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: 410.0MB Grounding... [('step', [31]), ('step', [32]), ('step', [33]), ('step', [34]), ('step', [35]), ('check', [35])] Grounding Time: 0.32s Memory: 327MB (+1MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 12 Time : 140.038s (Solving: 134.04s 1st Model: 0.00s Unsat: 4.20s) CPU Time : 140.004s Choices : 1469681 (Domain: 1393123) Conflicts : 210833 (Analyzed: 210830) Restarts : 761 (Average: 277.04 Last: 204) Model-Level : 147.0 Problems : 12 (Average Length: 21.58 Splits: 0) Lemmas : 210830 (Deleted: 188096) Binary : 6845 (Ratio: 3.25%) Ternary : 1557 (Ratio: 0.74%) Conflict : 210830 (Average Length: 847.9 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 210830 (Average: 6.49 Max: 431 Sum: 1369029) Executed : 210786 (Average: 6.49 Max: 431 Sum: 1368358 Ratio: 99.95%) Bounded : 44 (Average: 15.25 Max: 37 Sum: 671 Ratio: 0.05%) 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 : 1057342 (Binary: 91.6% Ternary: 6.5% Other: 2.0%) Memory Peak : 390MB Max. Length : 30 steps Models : 1 [endof: stats after solve call] Solving Time: 17.78s Memory: 341MB (+14MB) UNKNOWN Iteration Time: 18.29s 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: 425.0MB Grounding... [('step', [36]), ('step', [37]), ('step', [38]), ('step', [39]), ('step', [40]), ('check', [40])] Grounding Time: 0.42s Memory: 348MB (+7MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 13 Time : 158.318s (Solving: 151.36s 1st Model: 0.00s Unsat: 4.20s) CPU Time : 158.292s Choices : 1722991 (Domain: 1639840) Conflicts : 239049 (Analyzed: 239046) Restarts : 861 (Average: 277.64 Last: 204) Model-Level : 147.0 Problems : 13 (Average Length: 23.15 Splits: 0) Lemmas : 239046 (Deleted: 215086) Binary : 7595 (Ratio: 3.18%) Ternary : 1618 (Ratio: 0.68%) Conflict : 239046 (Average Length: 840.7 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 239046 (Average: 6.70 Max: 431 Sum: 1600769) Executed : 239002 (Average: 6.69 Max: 431 Sum: 1600098 Ratio: 99.96%) Bounded : 44 (Average: 15.25 Max: 37 Sum: 671 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 : 170767 (Eliminated: 1464 Frozen: 161773) Constraints : 1230373 (Binary: 91.6% Ternary: 6.5% Other: 2.0%) Memory Peak : 390MB Max. Length : 35 steps Models : 1 [endof: stats after solve call] Solving Time: 17.68s Memory: 362MB (+14MB) UNKNOWN Iteration Time: 18.29s 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: 446.0MB Grounding... [('step', [41]), ('step', [42]), ('step', [43]), ('step', [44]), ('step', [45]), ('check', [45])] Grounding Time: 0.31s Memory: 366MB (+4MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 14 Time : 175.477s (Solving: 167.66s 1st Model: 0.00s Unsat: 4.20s) CPU Time : 175.456s Choices : 1976070 (Domain: 1888390) Conflicts : 267225 (Analyzed: 267222) Restarts : 961 (Average: 278.07 Last: 204) Model-Level : 147.0 Problems : 14 (Average Length: 24.86 Splits: 0) Lemmas : 267222 (Deleted: 241788) Binary : 8210 (Ratio: 3.07%) Ternary : 1715 (Ratio: 0.64%) Conflict : 267222 (Average Length: 830.5 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 267222 (Average: 6.86 Max: 431 Sum: 1833630) Executed : 267178 (Average: 6.86 Max: 431 Sum: 1832959 Ratio: 99.96%) Bounded : 44 (Average: 15.25 Max: 37 Sum: 671 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 : 193343 (Eliminated: 1464 Frozen: 184349) Constraints : 1403418 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) Memory Peak : 391MB Max. Length : 40 steps Models : 1 [endof: stats after solve call] Solving Time: 16.67s Memory: 389MB (+23MB) UNKNOWN Iteration Time: 17.18s 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: 473.0MB Grounding... [('step', [46]), ('step', [47]), ('step', [48]), ('step', [49]), ('step', [50]), ('check', [50])] Grounding Time: 0.32s Memory: 389MB (+0MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 15 Time : 193.509s (Solving: 184.81s 1st Model: 0.00s Unsat: 4.20s) CPU Time : 193.496s Choices : 2212664 (Domain: 2122911) Conflicts : 295414 (Analyzed: 295411) Restarts : 1061 (Average: 278.43 Last: 204) Model-Level : 147.0 Problems : 15 (Average Length: 26.67 Splits: 0) Lemmas : 295411 (Deleted: 268828) Binary : 8624 (Ratio: 2.92%) Ternary : 1761 (Ratio: 0.60%) Conflict : 295411 (Average Length: 827.8 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 295411 (Average: 6.94 Max: 431 Sum: 2050016) Executed : 295365 (Average: 6.94 Max: 431 Sum: 2049241 Ratio: 99.96%) Bounded : 46 (Average: 16.85 Max: 52 Sum: 775 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 : 215919 (Eliminated: 1464 Frozen: 206925) Constraints : 1576463 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) Memory Peak : 419MB Max. Length : 45 steps Models : 1 [endof: stats after solve call] Solving Time: 17.51s Memory: 403MB (+14MB) UNKNOWN Iteration Time: 18.05s 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: 487.0MB Grounding... [('step', [51]), ('step', [52]), ('step', [53]), ('step', [54]), ('step', [55]), ('check', [55])] Grounding Time: 0.32s Memory: 403MB (+0MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 16 Time : 212.232s (Solving: 202.65s 1st Model: 0.00s Unsat: 4.20s) CPU Time : 212.228s Choices : 2583279 (Domain: 2479786) Conflicts : 323565 (Analyzed: 323562) Restarts : 1161 (Average: 278.69 Last: 204) Model-Level : 147.0 Problems : 16 (Average Length: 28.56 Splits: 0) Lemmas : 323562 (Deleted: 295387) Binary : 9565 (Ratio: 2.96%) Ternary : 1916 (Ratio: 0.59%) Conflict : 323562 (Average Length: 836.5 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 323562 (Average: 7.38 Max: 431 Sum: 2387890) Executed : 323516 (Average: 7.38 Max: 431 Sum: 2387115 Ratio: 99.97%) Bounded : 46 (Average: 16.85 Max: 52 Sum: 775 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 : 238495 (Eliminated: 1464 Frozen: 229501) Constraints : 1749480 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) Memory Peak : 437MB Max. Length : 50 steps Models : 1 [endof: stats after solve call] Solving Time: 18.21s Memory: 417MB (+14MB) UNKNOWN Iteration Time: 18.74s 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: 501.0MB Grounding... [('step', [56]), ('step', [57]), ('step', [58]), ('step', [59]), ('step', [60]), ('check', [60])] Grounding Time: 0.36s Memory: 417MB (+0MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 17 Time : 231.016s (Solving: 220.49s 1st Model: 0.00s Unsat: 4.20s) CPU Time : 231.020s Choices : 2835214 (Domain: 2730967) Conflicts : 351769 (Analyzed: 351766) Restarts : 1261 (Average: 278.96 Last: 204) Model-Level : 147.0 Problems : 17 (Average Length: 30.53 Splits: 0) Lemmas : 351766 (Deleted: 322486) Binary : 9951 (Ratio: 2.83%) Ternary : 1978 (Ratio: 0.56%) Conflict : 351766 (Average Length: 825.1 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 351766 (Average: 7.44 Max: 431 Sum: 2618009) Executed : 351719 (Average: 7.44 Max: 431 Sum: 2617172 Ratio: 99.97%) Bounded : 47 (Average: 17.81 Max: 62 Sum: 837 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 : 261071 (Eliminated: 1464 Frozen: 252077) Constraints : 1922525 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) Memory Peak : 454MB Max. Length : 55 steps Models : 1 [endof: stats after solve call] Solving Time: 18.21s Memory: 432MB (+15MB) UNKNOWN Iteration Time: 18.80s 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.35s Memory: 432MB (+0MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 18 Time : 251.557s (Solving: 240.07s 1st Model: 0.00s Unsat: 4.20s) CPU Time : 251.568s Choices : 3279607 (Domain: 3169584) Conflicts : 379925 (Analyzed: 379922) Restarts : 1361 (Average: 279.15 Last: 204) Model-Level : 147.0 Problems : 18 (Average Length: 32.56 Splits: 0) Lemmas : 379922 (Deleted: 348956) Binary : 11063 (Ratio: 2.91%) Ternary : 2142 (Ratio: 0.56%) Conflict : 379922 (Average Length: 826.5 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 379922 (Average: 7.96 Max: 431 Sum: 3025976) Executed : 379875 (Average: 7.96 Max: 431 Sum: 3025139 Ratio: 99.97%) Bounded : 47 (Average: 17.81 Max: 62 Sum: 837 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 : 283647 (Eliminated: 1464 Frozen: 274653) Constraints : 2095556 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) Memory Peak : 471MB Max. Length : 60 steps Models : 1 [endof: stats after solve call] Solving Time: 19.96s Memory: 465MB (+33MB) UNKNOWN Iteration Time: 20.56s Iteration 18 Queue: [(14,70,0,True), (15,75,0,True), (16,80,0,True), (17,85,0,True)] Grounded Until: 65 Expected Memory: 549.0MB Grounding... [('step', [66]), ('step', [67]), ('step', [68]), ('step', [69]), ('step', [70]), ('check', [70])] Grounding Time: 0.33s Memory: 465MB (+0MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 19 Time : 273.683s (Solving: 261.27s 1st Model: 0.00s Unsat: 4.20s) CPU Time : 273.704s Choices : 3620280 (Domain: 3509710) Conflicts : 408106 (Analyzed: 408103) Restarts : 1461 (Average: 279.33 Last: 204) Model-Level : 147.0 Problems : 19 (Average Length: 34.63 Splits: 0) Lemmas : 408103 (Deleted: 375917) Binary : 11570 (Ratio: 2.84%) Ternary : 2226 (Ratio: 0.55%) Conflict : 408103 (Average Length: 829.8 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 408103 (Average: 8.18 Max: 431 Sum: 3337540) Executed : 408056 (Average: 8.18 Max: 431 Sum: 3336703 Ratio: 99.97%) Bounded : 47 (Average: 17.81 Max: 62 Sum: 837 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 : 306223 (Eliminated: 1464 Frozen: 297229) Constraints : 2268601 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) Memory Peak : 503MB Max. Length : 65 steps Models : 1 [endof: stats after solve call] Solving Time: 21.57s Memory: 477MB (+12MB) UNKNOWN Iteration Time: 22.14s Iteration 19 Queue: [(15,75,0,True), (16,80,0,True), (17,85,0,True)] Grounded Until: 70 Expected Memory: 561.0MB Grounding... [('step', [71]), ('step', [72]), ('step', [73]), ('step', [74]), ('step', [75]), ('check', [75])] Grounding Time: 0.34s Memory: 477MB (+0MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 20 Time : 294.476s (Solving: 281.11s 1st Model: 0.00s Unsat: 4.20s) CPU Time : 294.504s Choices : 4030873 (Domain: 3916810) Conflicts : 436313 (Analyzed: 436310) Restarts : 1561 (Average: 279.51 Last: 204) Model-Level : 147.0 Problems : 20 (Average Length: 36.75 Splits: 0) Lemmas : 436310 (Deleted: 401371) Binary : 12272 (Ratio: 2.81%) Ternary : 2334 (Ratio: 0.53%) Conflict : 436310 (Average Length: 833.3 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 436310 (Average: 8.51 Max: 431 Sum: 3714399) Executed : 436263 (Average: 8.51 Max: 431 Sum: 3713562 Ratio: 99.98%) Bounded : 47 (Average: 17.81 Max: 62 Sum: 837 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 : 328799 (Eliminated: 1464 Frozen: 319805) Constraints : 2441646 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) Memory Peak : 518MB Max. Length : 70 steps Models : 1 [endof: stats after solve call] Solving Time: 20.23s Memory: 492MB (+15MB) UNKNOWN Iteration Time: 20.81s Iteration 20 Queue: [(16,80,0,True), (17,85,0,True)] Grounded Until: 75 Expected Memory: 576.0MB Grounding... [('step', [76]), ('step', [77]), ('step', [78]), ('step', [79]), ('step', [80]), ('check', [80])] Grounding Time: 0.48s Memory: 507MB (+15MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 21 Time : 316.121s (Solving: 301.64s 1st Model: 0.00s Unsat: 4.20s) CPU Time : 316.156s Choices : 4363980 (Domain: 4249676) Conflicts : 464504 (Analyzed: 464501) Restarts : 1661 (Average: 279.65 Last: 204) Model-Level : 147.0 Problems : 21 (Average Length: 38.90 Splits: 0) Lemmas : 464501 (Deleted: 429631) Binary : 12709 (Ratio: 2.74%) Ternary : 2409 (Ratio: 0.52%) Conflict : 464501 (Average Length: 830.6 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 464501 (Average: 8.65 Max: 431 Sum: 4016299) Executed : 464453 (Average: 8.64 Max: 431 Sum: 4015380 Ratio: 99.98%) Bounded : 48 (Average: 19.15 Max: 82 Sum: 919 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 : 351375 (Eliminated: 1464 Frozen: 342381) Constraints : 2614691 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) Memory Peak : 554MB Max. Length : 75 steps Models : 1 [endof: stats after solve call] Solving Time: 20.92s Memory: 521MB (+14MB) UNKNOWN Iteration Time: 21.66s Iteration 21 Queue: [(17,85,0,True)] Grounded Until: 80 Expected Memory: 605.0MB Grounding... [('step', [81]), ('step', [82]), ('step', [83]), ('step', [84]), ('step', [85]), ('check', [85])] Grounding Time: 0.32s Memory: 521MB (+0MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 22 Time : 339.079s (Solving: 323.63s 1st Model: 0.00s Unsat: 4.20s) CPU Time : 339.124s Choices : 4698272 (Domain: 4583605) Conflicts : 492648 (Analyzed: 492645) Restarts : 1761 (Average: 279.75 Last: 204) Model-Level : 147.0 Problems : 22 (Average Length: 41.09 Splits: 0) Lemmas : 492645 (Deleted: 456973) Binary : 13120 (Ratio: 2.66%) Ternary : 2458 (Ratio: 0.50%) Conflict : 492645 (Average Length: 839.4 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 492645 (Average: 8.75 Max: 431 Sum: 4309179) Executed : 492597 (Average: 8.75 Max: 431 Sum: 4308260 Ratio: 99.98%) Bounded : 48 (Average: 19.15 Max: 82 Sum: 919 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 : 373951 (Eliminated: 1464 Frozen: 364957) Constraints : 2787722 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) Memory Peak : 570MB Max. Length : 80 steps Models : 1 [endof: stats after solve call] Solving Time: 22.39s Memory: 535MB (+14MB) UNKNOWN Iteration Time: 22.97s 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 : 350.517s (Solving: 334.98s 1st Model: 0.00s Unsat: 4.20s) CPU Time : 350.568s Choices : 4813255 (Domain: 4698588) Conflicts : 520838 (Analyzed: 520835) Restarts : 1861 (Average: 279.87 Last: 204) Model-Level : 147.0 Problems : 23 (Average Length: 43.09 Splits: 0) Lemmas : 520835 (Deleted: 484258) Binary : 13398 (Ratio: 2.57%) Ternary : 2506 (Ratio: 0.48%) Conflict : 520835 (Average Length: 826.3 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 520835 (Average: 8.48 Max: 431 Sum: 4417398) Executed : 520786 (Average: 8.48 Max: 431 Sum: 4416392 Ratio: 99.98%) Bounded : 49 (Average: 20.53 Max: 87 Sum: 1006 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 : 373951 (Eliminated: 1464 Frozen: 372487) Constraints : 2787722 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) Memory Peak : 570MB Max. Length : 85 steps Models : 1 [endof: stats after solve call] Solving Time: 11.41s Memory: 537MB (+2MB) UNKNOWN Iteration Time: 11.45s 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 : 376.151s (Solving: 360.52s 1st Model: 0.00s Unsat: 4.20s) CPU Time : 376.216s Choices : 4911678 (Domain: 4797011) Conflicts : 548996 (Analyzed: 548993) Restarts : 1961 (Average: 279.96 Last: 204) Model-Level : 147.0 Problems : 24 (Average Length: 44.92 Splits: 0) Lemmas : 548993 (Deleted: 511889) Binary : 13480 (Ratio: 2.46%) Ternary : 2531 (Ratio: 0.46%) Conflict : 548993 (Average Length: 846.1 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 548993 (Average: 8.21 Max: 431 Sum: 4506436) Executed : 548943 (Average: 8.21 Max: 431 Sum: 4505343 Ratio: 99.98%) Bounded : 50 (Average: 21.86 Max: 87 Sum: 1093 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 : 373951 (Eliminated: 1464 Frozen: 372487) Constraints : 2787708 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) Memory Peak : 570MB Max. Length : 85 steps Models : 1 [endof: stats after solve call] Solving Time: 25.61s Memory: 537MB (+0MB) UNKNOWN Iteration Time: 25.65s 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 : 395.354s (Solving: 379.63s 1st Model: 0.00s Unsat: 4.20s) CPU Time : 395.428s Choices : 5101516 (Domain: 4986849) Conflicts : 577235 (Analyzed: 577232) Restarts : 2061 (Average: 280.07 Last: 204) Model-Level : 147.0 Problems : 25 (Average Length: 46.60 Splits: 0) Lemmas : 577232 (Deleted: 539550) Binary : 13703 (Ratio: 2.37%) Ternary : 2558 (Ratio: 0.44%) Conflict : 577232 (Average Length: 861.7 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 577232 (Average: 8.11 Max: 431 Sum: 4678791) Executed : 577182 (Average: 8.10 Max: 431 Sum: 4677698 Ratio: 99.98%) Bounded : 50 (Average: 21.86 Max: 87 Sum: 1093 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 : 373951 (Eliminated: 1464 Frozen: 372487) Constraints : 2787694 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) Memory Peak : 570MB Max. Length : 85 steps Models : 1 [endof: stats after solve call] Solving Time: 19.18s Memory: 537MB (+0MB) UNKNOWN Iteration Time: 19.22s 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 : 413.248s (Solving: 397.41s 1st Model: 0.00s Unsat: 4.20s) CPU Time : 413.328s Choices : 5288141 (Domain: 5173473) Conflicts : 605398 (Analyzed: 605395) Restarts : 2161 (Average: 280.15 Last: 204) Model-Level : 147.0 Problems : 26 (Average Length: 48.15 Splits: 0) Lemmas : 605395 (Deleted: 566903) Binary : 13934 (Ratio: 2.30%) Ternary : 2601 (Ratio: 0.43%) Conflict : 605395 (Average Length: 864.4 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 605395 (Average: 8.01 Max: 431 Sum: 4847208) Executed : 605345 (Average: 8.00 Max: 431 Sum: 4846115 Ratio: 99.98%) Bounded : 50 (Average: 21.86 Max: 87 Sum: 1093 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 : 373951 (Eliminated: 1464 Frozen: 372487) Constraints : 2787694 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) Memory Peak : 570MB Max. Length : 85 steps Models : 1 [endof: stats after solve call] Solving Time: 17.85s Memory: 537MB (+0MB) UNKNOWN Iteration Time: 17.90s 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 : 434.403s (Solving: 418.46s 1st Model: 0.00s Unsat: 4.20s) CPU Time : 434.492s Choices : 5485373 (Domain: 5370691) Conflicts : 633582 (Analyzed: 633579) Restarts : 2261 (Average: 280.22 Last: 204) Model-Level : 147.0 Problems : 27 (Average Length: 49.59 Splits: 0) Lemmas : 633579 (Deleted: 594155) Binary : 14225 (Ratio: 2.25%) Ternary : 2658 (Ratio: 0.42%) Conflict : 633579 (Average Length: 875.0 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 633579 (Average: 7.93 Max: 431 Sum: 5022002) Executed : 633529 (Average: 7.92 Max: 431 Sum: 5020909 Ratio: 99.98%) Bounded : 50 (Average: 21.86 Max: 87 Sum: 1093 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 : 373951 (Eliminated: 1464 Frozen: 372487) Constraints : 2787694 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) Memory Peak : 570MB Max. Length : 85 steps Models : 1 [endof: stats after solve call] Solving Time: 21.12s Memory: 537MB (+0MB) UNKNOWN Iteration Time: 21.17s 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 : 451.839s (Solving: 435.81s 1st Model: 0.00s Unsat: 4.20s) CPU Time : 451.932s Choices : 5700364 (Domain: 5584170) Conflicts : 661765 (Analyzed: 661762) Restarts : 2361 (Average: 280.29 Last: 204) Model-Level : 147.0 Problems : 28 (Average Length: 50.93 Splits: 0) Lemmas : 661762 (Deleted: 621439) Binary : 14657 (Ratio: 2.21%) Ternary : 2708 (Ratio: 0.41%) Conflict : 661762 (Average Length: 872.9 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 661762 (Average: 7.88 Max: 431 Sum: 5212706) Executed : 661712 (Average: 7.88 Max: 431 Sum: 5211613 Ratio: 99.98%) Bounded : 50 (Average: 21.86 Max: 87 Sum: 1093 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 : 373951 (Eliminated: 1464 Frozen: 372487) Constraints : 2787694 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) Memory Peak : 570MB Max. Length : 85 steps Models : 1 [endof: stats after solve call] Solving Time: 17.41s Memory: 537MB (+0MB) UNKNOWN Iteration Time: 17.45s 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 : 468.754s (Solving: 452.63s 1st Model: 0.00s Unsat: 4.20s) CPU Time : 468.856s Choices : 5892645 (Domain: 5776369) Conflicts : 689962 (Analyzed: 689959) Restarts : 2461 (Average: 280.36 Last: 204) Model-Level : 147.0 Problems : 29 (Average Length: 52.17 Splits: 0) Lemmas : 689959 (Deleted: 647517) Binary : 14908 (Ratio: 2.16%) Ternary : 2759 (Ratio: 0.40%) Conflict : 689959 (Average Length: 871.6 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 689959 (Average: 7.80 Max: 431 Sum: 5382814) Executed : 689909 (Average: 7.80 Max: 431 Sum: 5381721 Ratio: 99.98%) Bounded : 50 (Average: 21.86 Max: 87 Sum: 1093 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 : 373951 (Eliminated: 1464 Frozen: 372487) Constraints : 2787694 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) Memory Peak : 570MB Max. Length : 85 steps Models : 1 [endof: stats after solve call] Solving Time: 16.89s Memory: 537MB (+0MB) UNKNOWN Iteration Time: 16.93s 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 : 489.515s (Solving: 473.27s 1st Model: 0.00s Unsat: 4.20s) CPU Time : 489.628s Choices : 6121052 (Domain: 6004694) Conflicts : 718096 (Analyzed: 718093) Restarts : 2561 (Average: 280.40 Last: 204) Model-Level : 147.0 Problems : 30 (Average Length: 53.33 Splits: 0) Lemmas : 718093 (Deleted: 676101) Binary : 15186 (Ratio: 2.11%) Ternary : 2806 (Ratio: 0.39%) Conflict : 718093 (Average Length: 878.1 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 718093 (Average: 7.78 Max: 431 Sum: 5583729) Executed : 718043 (Average: 7.77 Max: 431 Sum: 5582636 Ratio: 99.98%) Bounded : 50 (Average: 21.86 Max: 87 Sum: 1093 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 : 373951 (Eliminated: 1464 Frozen: 372487) Constraints : 2787694 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) Memory Peak : 570MB Max. Length : 85 steps Models : 1 [endof: stats after solve call] Solving Time: 20.72s Memory: 537MB (+0MB) UNKNOWN Iteration Time: 20.77s 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 : 508.521s (Solving: 492.15s 1st Model: 0.00s Unsat: 4.20s) CPU Time : 508.640s Choices : 6340515 (Domain: 6223979) Conflicts : 746262 (Analyzed: 746259) Restarts : 2661 (Average: 280.44 Last: 204) Model-Level : 147.0 Problems : 31 (Average Length: 54.42 Splits: 0) Lemmas : 746259 (Deleted: 703489) Binary : 15397 (Ratio: 2.06%) Ternary : 2842 (Ratio: 0.38%) Conflict : 746259 (Average Length: 881.2 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 746259 (Average: 7.74 Max: 431 Sum: 5774391) Executed : 746208 (Average: 7.74 Max: 431 Sum: 5773211 Ratio: 99.98%) Bounded : 51 (Average: 23.14 Max: 87 Sum: 1180 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 : 373951 (Eliminated: 1464 Frozen: 372487) Constraints : 2787694 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) Memory Peak : 570MB Max. Length : 85 steps Models : 1 [endof: stats after solve call] Solving Time: 18.96s Memory: 537MB (+0MB) UNKNOWN Iteration Time: 19.02s 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 : 527.510s (Solving: 511.05s 1st Model: 0.00s Unsat: 4.20s) CPU Time : 527.636s Choices : 6600559 (Domain: 6482924) Conflicts : 774478 (Analyzed: 774475) Restarts : 2761 (Average: 280.51 Last: 204) Model-Level : 147.0 Problems : 32 (Average Length: 55.44 Splits: 0) Lemmas : 774475 (Deleted: 730698) Binary : 15878 (Ratio: 2.05%) Ternary : 2908 (Ratio: 0.38%) Conflict : 774475 (Average Length: 883.2 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 774475 (Average: 7.75 Max: 431 Sum: 6000830) Executed : 774424 (Average: 7.75 Max: 431 Sum: 5999650 Ratio: 99.98%) Bounded : 51 (Average: 23.14 Max: 87 Sum: 1180 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 : 373951 (Eliminated: 1464 Frozen: 372487) Constraints : 2787687 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) Memory Peak : 570MB Max. Length : 85 steps Models : 1 [endof: stats after solve call] Solving Time: 18.96s Memory: 537MB (+0MB) UNKNOWN Iteration Time: 19.00s 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 : 547.765s (Solving: 531.21s 1st Model: 0.00s Unsat: 4.20s) CPU Time : 547.900s Choices : 6914199 (Domain: 6794643) Conflicts : 802630 (Analyzed: 802627) Restarts : 2861 (Average: 280.54 Last: 204) Model-Level : 147.0 Problems : 33 (Average Length: 56.39 Splits: 0) Lemmas : 802627 (Deleted: 757893) Binary : 16327 (Ratio: 2.03%) Ternary : 2968 (Ratio: 0.37%) Conflict : 802627 (Average Length: 885.7 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 802627 (Average: 7.82 Max: 431 Sum: 6279139) Executed : 802576 (Average: 7.82 Max: 431 Sum: 6277959 Ratio: 99.98%) Bounded : 51 (Average: 23.14 Max: 87 Sum: 1180 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 : 373951 (Eliminated: 1464 Frozen: 372487) Constraints : 2787687 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) Memory Peak : 570MB Max. Length : 85 steps Models : 1 [endof: stats after solve call] Solving Time: 20.22s Memory: 537MB (+0MB) UNKNOWN Iteration Time: 20.27s 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 : 568.390s (Solving: 551.74s 1st Model: 0.00s Unsat: 4.20s) CPU Time : 568.536s Choices : 7151395 (Domain: 7031757) Conflicts : 830822 (Analyzed: 830819) Restarts : 2961 (Average: 280.59 Last: 204) Model-Level : 147.0 Problems : 34 (Average Length: 57.29 Splits: 0) Lemmas : 830819 (Deleted: 785308) Binary : 16566 (Ratio: 1.99%) Ternary : 3004 (Ratio: 0.36%) Conflict : 830819 (Average Length: 889.3 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 830819 (Average: 7.81 Max: 431 Sum: 6485634) Executed : 830768 (Average: 7.80 Max: 431 Sum: 6484454 Ratio: 99.98%) Bounded : 51 (Average: 23.14 Max: 87 Sum: 1180 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 : 373951 (Eliminated: 1464 Frozen: 372487) Constraints : 2787687 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) Memory Peak : 570MB Max. Length : 85 steps Models : 1 [endof: stats after solve call] Solving Time: 20.60s Memory: 537MB (+0MB) UNKNOWN Iteration Time: 20.64s 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 : 589.267s (Solving: 572.51s 1st Model: 0.00s Unsat: 4.20s) CPU Time : 589.420s Choices : 7441227 (Domain: 7316328) Conflicts : 858998 (Analyzed: 858995) Restarts : 3061 (Average: 280.63 Last: 204) Model-Level : 147.0 Problems : 35 (Average Length: 58.14 Splits: 0) Lemmas : 858995 (Deleted: 812298) Binary : 17110 (Ratio: 1.99%) Ternary : 3091 (Ratio: 0.36%) Conflict : 858995 (Average Length: 892.4 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 858995 (Average: 7.85 Max: 431 Sum: 6741586) Executed : 858944 (Average: 7.85 Max: 431 Sum: 6740406 Ratio: 99.98%) Bounded : 51 (Average: 23.14 Max: 87 Sum: 1180 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 : 373951 (Eliminated: 1464 Frozen: 372487) Constraints : 2787687 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) Memory Peak : 570MB Max. Length : 85 steps Models : 1 [endof: stats after solve call] Solving Time: 20.85s Memory: 537MB (+0MB) UNKNOWN Iteration Time: 20.89s 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 : 611.139s (Solving: 594.28s 1st Model: 0.00s Unsat: 4.20s) CPU Time : 611.300s Choices : 7717670 (Domain: 7592616) Conflicts : 887211 (Analyzed: 887208) Restarts : 3161 (Average: 280.67 Last: 204) Model-Level : 147.0 Problems : 36 (Average Length: 58.94 Splits: 0) Lemmas : 887208 (Deleted: 839899) Binary : 17380 (Ratio: 1.96%) Ternary : 3137 (Ratio: 0.35%) Conflict : 887208 (Average Length: 893.9 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 887208 (Average: 7.87 Max: 493 Sum: 6983010) Executed : 887157 (Average: 7.87 Max: 493 Sum: 6981830 Ratio: 99.98%) Bounded : 51 (Average: 23.14 Max: 87 Sum: 1180 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 : 373951 (Eliminated: 1464 Frozen: 372487) Constraints : 2787687 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) Memory Peak : 570MB Max. Length : 85 steps Models : 1 [endof: stats after solve call] Solving Time: 21.84s Memory: 537MB (+0MB) UNKNOWN Iteration Time: 21.88s 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: 537MB (+0MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 37 Time : 632.985s (Solving: 615.15s 1st Model: 0.00s Unsat: 4.20s) CPU Time : 633.156s Choices : 7997616 (Domain: 7872364) Conflicts : 915441 (Analyzed: 915438) Restarts : 3261 (Average: 280.72 Last: 204) Model-Level : 147.0 Problems : 37 (Average Length: 59.84 Splits: 0) Lemmas : 915438 (Deleted: 867282) Binary : 17707 (Ratio: 1.93%) Ternary : 3182 (Ratio: 0.35%) Conflict : 915438 (Average Length: 893.9 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 915438 (Average: 7.89 Max: 493 Sum: 7226121) Executed : 915387 (Average: 7.89 Max: 493 Sum: 7224941 Ratio: 99.98%) Bounded : 51 (Average: 23.14 Max: 87 Sum: 1180 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 : 396527 (Eliminated: 1464 Frozen: 387533) Constraints : 2960732 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) Memory Peak : 587MB Max. Length : 85 steps Models : 1 [endof: stats after solve call] Solving Time: 21.26s Memory: 549MB (+12MB) UNKNOWN Iteration Time: 21.86s 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.32s Memory: 549MB (+0MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 38 Time : 654.789s (Solving: 635.95s 1st Model: 0.00s Unsat: 4.20s) CPU Time : 654.972s Choices : 8272236 (Domain: 8146669) Conflicts : 943641 (Analyzed: 943638) Restarts : 3361 (Average: 280.76 Last: 204) Model-Level : 147.0 Problems : 38 (Average Length: 60.82 Splits: 0) Lemmas : 943638 (Deleted: 894728) Binary : 17930 (Ratio: 1.90%) Ternary : 3210 (Ratio: 0.34%) Conflict : 943638 (Average Length: 889.7 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 943638 (Average: 7.92 Max: 493 Sum: 7469400) Executed : 943587 (Average: 7.91 Max: 493 Sum: 7468220 Ratio: 99.98%) Bounded : 51 (Average: 23.14 Max: 87 Sum: 1180 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 : 419103 (Eliminated: 1464 Frozen: 410109) Constraints : 3133777 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) Memory Peak : 607MB Max. Length : 90 steps Models : 1 [endof: stats after solve call] Solving Time: 21.20s Memory: 596MB (+47MB) UNKNOWN Iteration Time: 21.82s Iteration 38 Queue: [(20,100,0,True), (21,105,0,True)] Grounded Until: 95 Expected Memory: 680.0MB Grounding... [('step', [96]), ('step', [97]), ('step', [98]), ('step', [99]), ('step', [100]), ('check', [100])] Grounding Time: 0.33s Memory: 596MB (+0MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 39 Time : 678.370s (Solving: 658.52s 1st Model: 0.00s Unsat: 4.20s) CPU Time : 678.564s Choices : 8579392 (Domain: 8453731) Conflicts : 971840 (Analyzed: 971837) Restarts : 3461 (Average: 280.80 Last: 204) Model-Level : 147.0 Problems : 39 (Average Length: 61.87 Splits: 0) Lemmas : 971837 (Deleted: 922125) Binary : 18257 (Ratio: 1.88%) Ternary : 3262 (Ratio: 0.34%) Conflict : 971837 (Average Length: 888.9 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 971837 (Average: 7.96 Max: 493 Sum: 7736535) Executed : 971786 (Average: 7.96 Max: 493 Sum: 7735355 Ratio: 99.98%) Bounded : 51 (Average: 23.14 Max: 87 Sum: 1180 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 : 441679 (Eliminated: 1464 Frozen: 432685) Constraints : 3306822 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) Memory Peak : 650MB Max. Length : 95 steps Models : 1 [endof: stats after solve call] Solving Time: 22.97s Memory: 612MB (+16MB) UNKNOWN Iteration Time: 23.60s Iteration 39 Queue: [(21,105,0,True)] Grounded Until: 100 Expected Memory: 696.0MB Grounding... [('step', [101]), ('step', [102]), ('step', [103]), ('step', [104]), ('step', [105]), ('check', [105])] Grounding Time: 0.32s Memory: 612MB (+0MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 40 Time : 700.801s (Solving: 679.93s 1st Model: 0.00s Unsat: 4.20s) CPU Time : 701.004s Choices : 8853119 (Domain: 8727423) Conflicts : 1000007 (Analyzed: 1000004) Restarts : 3561 (Average: 280.82 Last: 204) Model-Level : 147.0 Problems : 40 (Average Length: 63.00 Splits: 0) Lemmas : 1000004 (Deleted: 946111) Binary : 18417 (Ratio: 1.84%) Ternary : 3291 (Ratio: 0.33%) Conflict : 1000004 (Average Length: 887.8 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 1000004 (Average: 7.97 Max: 493 Sum: 7973347) Executed : 999953 (Average: 7.97 Max: 493 Sum: 7972167 Ratio: 99.99%) Bounded : 51 (Average: 23.14 Max: 87 Sum: 1180 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 : 464255 (Eliminated: 1464 Frozen: 455261) Constraints : 3479867 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) Memory Peak : 669MB Max. Length : 100 steps Models : 1 [endof: stats after solve call] Solving Time: 21.82s Memory: 616MB (+4MB) UNKNOWN Iteration Time: 22.45s 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 : 713.054s (Solving: 692.05s 1st Model: 0.00s Unsat: 4.20s) CPU Time : 713.264s Choices : 9003898 (Domain: 8878202) Conflicts : 1028184 (Analyzed: 1028181) Restarts : 3661 (Average: 280.85 Last: 204) Model-Level : 147.0 Problems : 41 (Average Length: 64.07 Splits: 0) Lemmas : 1028181 (Deleted: 977173) Binary : 18547 (Ratio: 1.80%) Ternary : 3325 (Ratio: 0.32%) Conflict : 1028181 (Average Length: 876.5 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 1028181 (Average: 7.89 Max: 493 Sum: 8117468) Executed : 1028130 (Average: 7.89 Max: 493 Sum: 8116288 Ratio: 99.99%) Bounded : 51 (Average: 23.14 Max: 87 Sum: 1180 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 : 464255 (Eliminated: 1464 Frozen: 462791) Constraints : 3479867 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) Memory Peak : 669MB Max. Length : 105 steps Models : 1 [endof: stats after solve call] Solving Time: 12.20s Memory: 616MB (+0MB) UNKNOWN Iteration Time: 12.26s 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 : 738.564s (Solving: 717.46s 1st Model: 0.00s Unsat: 4.20s) CPU Time : 738.784s Choices : 9105606 (Domain: 8979910) Conflicts : 1056370 (Analyzed: 1056367) Restarts : 3761 (Average: 280.87 Last: 204) Model-Level : 147.0 Problems : 42 (Average Length: 65.10 Splits: 0) Lemmas : 1056367 (Deleted: 1004871) Binary : 18597 (Ratio: 1.76%) Ternary : 3363 (Ratio: 0.32%) Conflict : 1056367 (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 : 1056367 (Average: 7.77 Max: 493 Sum: 8209915) Executed : 1056316 (Average: 7.77 Max: 493 Sum: 8208735 Ratio: 99.99%) Bounded : 51 (Average: 23.14 Max: 87 Sum: 1180 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 : 464255 (Eliminated: 1464 Frozen: 462791) Constraints : 3479867 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) Memory Peak : 669MB Max. Length : 105 steps Models : 1 [endof: stats after solve call] Solving Time: 25.48s Memory: 616MB (+0MB) UNKNOWN Iteration Time: 25.52s 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 : 764.452s (Solving: 743.24s 1st Model: 0.00s Unsat: 4.20s) CPU Time : 764.680s Choices : 9282110 (Domain: 9156414) Conflicts : 1084555 (Analyzed: 1084552) Restarts : 3861 (Average: 280.90 Last: 204) Model-Level : 147.0 Problems : 43 (Average Length: 66.07 Splits: 0) Lemmas : 1084552 (Deleted: 1032580) Binary : 18721 (Ratio: 1.73%) Ternary : 3384 (Ratio: 0.31%) Conflict : 1084552 (Average Length: 891.5 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 1084552 (Average: 7.72 Max: 493 Sum: 8370316) Executed : 1084501 (Average: 7.72 Max: 493 Sum: 8369136 Ratio: 99.99%) Bounded : 51 (Average: 23.14 Max: 87 Sum: 1180 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 : 464255 (Eliminated: 1464 Frozen: 462791) Constraints : 3479867 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) Memory Peak : 744MB Max. Length : 105 steps Models : 1 [endof: stats after solve call] Solving Time: 25.86s Memory: 680MB (+64MB) UNKNOWN Iteration Time: 25.90s 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 : 784.115s (Solving: 762.79s 1st Model: 0.00s Unsat: 4.20s) CPU Time : 784.352s Choices : 9451213 (Domain: 9325517) Conflicts : 1112727 (Analyzed: 1112724) Restarts : 3961 (Average: 280.92 Last: 204) Model-Level : 147.0 Problems : 44 (Average Length: 67.00 Splits: 0) Lemmas : 1112724 (Deleted: 1060159) Binary : 18869 (Ratio: 1.70%) Ternary : 3425 (Ratio: 0.31%) Conflict : 1112724 (Average Length: 894.9 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 1112724 (Average: 7.66 Max: 493 Sum: 8519634) Executed : 1112673 (Average: 7.66 Max: 493 Sum: 8518454 Ratio: 99.99%) Bounded : 51 (Average: 23.14 Max: 87 Sum: 1180 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 : 464255 (Eliminated: 1464 Frozen: 462791) Constraints : 3479867 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) Memory Peak : 744MB Max. Length : 105 steps Models : 1 [endof: stats after solve call] Solving Time: 19.63s Memory: 680MB (+0MB) UNKNOWN Iteration Time: 19.67s 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 : 803.797s (Solving: 782.37s 1st Model: 0.00s Unsat: 4.20s) CPU Time : 804.040s Choices : 9629811 (Domain: 9504115) Conflicts : 1140953 (Analyzed: 1140950) Restarts : 4061 (Average: 280.95 Last: 204) Model-Level : 147.0 Problems : 45 (Average Length: 67.89 Splits: 0) Lemmas : 1140950 (Deleted: 1087827) Binary : 19015 (Ratio: 1.67%) Ternary : 3450 (Ratio: 0.30%) Conflict : 1140950 (Average Length: 897.3 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 1140950 (Average: 7.60 Max: 493 Sum: 8675794) Executed : 1140899 (Average: 7.60 Max: 493 Sum: 8674614 Ratio: 99.99%) Bounded : 51 (Average: 23.14 Max: 87 Sum: 1180 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 : 464255 (Eliminated: 1464 Frozen: 462791) Constraints : 3479867 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) Memory Peak : 744MB Max. Length : 105 steps Models : 1 [endof: stats after solve call] Solving Time: 19.65s Memory: 680MB (+0MB) UNKNOWN Iteration Time: 19.69s 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 : 825.313s (Solving: 803.76s 1st Model: 0.00s Unsat: 4.20s) CPU Time : 825.564s Choices : 9823417 (Domain: 9697580) Conflicts : 1169150 (Analyzed: 1169147) Restarts : 4161 (Average: 280.98 Last: 204) Model-Level : 147.0 Problems : 46 (Average Length: 68.74 Splits: 0) Lemmas : 1169147 (Deleted: 1115335) Binary : 19295 (Ratio: 1.65%) Ternary : 3485 (Ratio: 0.30%) Conflict : 1169147 (Average Length: 904.0 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 1169147 (Average: 7.56 Max: 493 Sum: 8842595) Executed : 1169096 (Average: 7.56 Max: 493 Sum: 8841415 Ratio: 99.99%) Bounded : 51 (Average: 23.14 Max: 87 Sum: 1180 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 : 464255 (Eliminated: 1464 Frozen: 462791) Constraints : 3479867 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) Memory Peak : 744MB Max. Length : 105 steps Models : 1 [endof: stats after solve call] Solving Time: 21.47s Memory: 680MB (+0MB) UNKNOWN Iteration Time: 21.53s 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 : 844.567s (Solving: 822.91s 1st Model: 0.00s Unsat: 4.20s) CPU Time : 844.828s Choices : 10033085 (Domain: 9907237) Conflicts : 1197341 (Analyzed: 1197338) Restarts : 4261 (Average: 281.00 Last: 204) Model-Level : 147.0 Problems : 47 (Average Length: 69.55 Splits: 0) Lemmas : 1197338 (Deleted: 1142902) Binary : 19440 (Ratio: 1.62%) Ternary : 3518 (Ratio: 0.29%) Conflict : 1197338 (Average Length: 903.7 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 1197338 (Average: 7.54 Max: 493 Sum: 9026213) Executed : 1197287 (Average: 7.54 Max: 493 Sum: 9025033 Ratio: 99.99%) Bounded : 51 (Average: 23.14 Max: 87 Sum: 1180 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 : 464255 (Eliminated: 1464 Frozen: 462791) Constraints : 3479867 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) Memory Peak : 744MB Max. Length : 105 steps Models : 1 [endof: stats after solve call] Solving Time: 19.22s Memory: 680MB (+0MB) UNKNOWN Iteration Time: 19.26s 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 : 863.330s (Solving: 841.57s 1st Model: 0.00s Unsat: 4.20s) CPU Time : 863.600s Choices : 10251284 (Domain: 10125432) Conflicts : 1225502 (Analyzed: 1225499) Restarts : 4361 (Average: 281.01 Last: 204) Model-Level : 147.0 Problems : 48 (Average Length: 70.33 Splits: 0) Lemmas : 1225499 (Deleted: 1170396) Binary : 19701 (Ratio: 1.61%) Ternary : 3549 (Ratio: 0.29%) Conflict : 1225499 (Average Length: 904.6 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 1225499 (Average: 7.52 Max: 493 Sum: 9214105) Executed : 1225448 (Average: 7.52 Max: 493 Sum: 9212925 Ratio: 99.99%) Bounded : 51 (Average: 23.14 Max: 87 Sum: 1180 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 : 464255 (Eliminated: 1464 Frozen: 462791) Constraints : 3479867 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) Memory Peak : 744MB Max. Length : 105 steps Models : 1 [endof: stats after solve call] Solving Time: 18.73s Memory: 680MB (+0MB) UNKNOWN Iteration Time: 18.77s 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 : 881.523s (Solving: 859.66s 1st Model: 0.00s Unsat: 4.20s) CPU Time : 881.800s Choices : 10489316 (Domain: 10363047) Conflicts : 1253686 (Analyzed: 1253683) Restarts : 4461 (Average: 281.03 Last: 204) Model-Level : 147.0 Problems : 49 (Average Length: 71.08 Splits: 0) Lemmas : 1253683 (Deleted: 1197683) Binary : 19958 (Ratio: 1.59%) Ternary : 3584 (Ratio: 0.29%) Conflict : 1253683 (Average Length: 903.4 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 1253683 (Average: 7.51 Max: 493 Sum: 9421101) Executed : 1253631 (Average: 7.51 Max: 493 Sum: 9419814 Ratio: 99.99%) Bounded : 52 (Average: 24.75 Max: 107 Sum: 1287 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 : 464255 (Eliminated: 1464 Frozen: 462791) Constraints : 3479867 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) Memory Peak : 744MB Max. Length : 105 steps Models : 1 [endof: stats after solve call] Solving Time: 18.16s Memory: 680MB (+0MB) UNKNOWN Iteration Time: 18.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... *** Info : (planner): INTERRUPTED by signal! UNKNOWN INTERRUPTED : 1 Models : 0+ Calls : 50 Time : 900.347s (Solving: 878.37s 1st Model: 0.00s Unsat: 4.20s) CPU Time : 900.616s Choices : 10729648 (Domain: 10602630) Conflicts : 1281834 (Analyzed: 1281831) Restarts : 4561 (Average: 281.04 Last: 204) Model-Level : 147.0 Problems : 50 (Average Length: 71.80 Splits: 0) Lemmas : 1281831 (Deleted: 1225188) Binary : 20176 (Ratio: 1.57%) Ternary : 3624 (Ratio: 0.28%) Conflict : 1281831 (Average Length: 903.4 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 1281831 (Average: 7.51 Max: 493 Sum: 9629023) Executed : 1281779 (Average: 7.51 Max: 493 Sum: 9627736 Ratio: 99.99%) Bounded : 52 (Average: 24.75 Max: 107 Sum: 1287 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 : 464255 (Eliminated: 1464 Frozen: 462791) Constraints : 3479853 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) Memory Peak : 744MB Max. Length : 105 steps Models : 1