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-13.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-13.pddl Parsing... Parsing: [0.050s CPU, 0.048s wall-clock] Normalizing task... [0.000s CPU, 0.004s wall-clock] Instantiating... Generating Datalog program... [0.010s CPU, 0.013s wall-clock] Normalizing Datalog program... Normalizing Datalog program: [0.070s CPU, 0.070s wall-clock] Preparing model... [0.040s CPU, 0.037s wall-clock] Generated 115 rules. Computing model... [0.510s CPU, 0.520s wall-clock] 3094 relevant atoms 3221 auxiliary atoms 6315 final queue length 10878 total queue pushes Completing instantiation... [0.960s CPU, 0.964s wall-clock] Instantiating: [1.600s CPU, 1.610s wall-clock] Computing fact groups... Finding invariants... 24 initial candidates Finding invariants: [0.120s CPU, 0.115s wall-clock] Checking invariant weight... [0.000s CPU, 0.001s wall-clock] Instantiating groups... [0.010s CPU, 0.009s wall-clock] Collecting mutex groups... [0.000s CPU, 0.001s wall-clock] Choosing groups... 328 uncovered facts Choosing groups: [0.000s CPU, 0.002s wall-clock] Building translation key... [0.010s CPU, 0.012s wall-clock] Computing fact groups: [0.170s CPU, 0.166s wall-clock] Building STRIPS to SAS dictionary... [0.000s CPU, 0.003s wall-clock] Building dictionary for full mutex groups... [0.010s CPU, 0.003s wall-clock] Building mutex information... Building mutex information: [0.000s CPU, 0.003s wall-clock] Translating task... Processing axioms... Simplifying axioms... [0.000s CPU, 0.000s wall-clock] Processing axioms: [0.050s CPU, 0.052s wall-clock] Translating task: [1.000s CPU, 1.000s wall-clock] 3672 effect conditions simplified 0 implied preconditions added Detecting unreachable propositions... 0 operators removed 0 axioms removed 3 propositions removed Detecting unreachable propositions: [0.490s CPU, 0.491s wall-clock] Reordering and filtering variables... 331 of 331 variables necessary. 15 of 18 mutex groups necessary. 2194 of 2194 operators necessary. 0 of 0 axiom rules necessary. Reordering and filtering variables: [0.400s CPU, 0.403s wall-clock] Translator variables: 331 Translator derived variables: 0 Translator facts: 691 Translator goal facts: 13 Translator mutex groups: 15 Translator total mutex groups size: 45 Translator operators: 2194 Translator axioms: 0 Translator task size: 21018 Translator peak memory: 48332 KB Writing output... [0.430s CPU, 0.460s wall-clock] Done! [4.190s CPU, 4.231s wall-clock] planner.py version 0.0.1 Time: 0.86s Memory: 107MB 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 : 1.030s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s) CPU Time : 0.860s 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 : 60629 Atoms : 60629 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 : 243MB Max. Length : 0 steps Models : 0 [endof: stats after solve call] Solving Time: 0.01s Memory: 179MB (+72MB) UNSAT Iteration Time: 0.01s 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: 179MB Grounding... [('step', [1]), ('step', [2]), ('step', [3]), ('step', [4]), ('step', [5]), ('check', [5])] Grounding Time: 0.26s Memory: 179MB (+0MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0 Calls : 2 Time : 1.433s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s) CPU Time : 1.260s Choices : 335 (Domain: 109) Conflicts : 40 (Analyzed: 39) Restarts : 0 Problems : 2 (Average Length: 4.50 Splits: 0) Lemmas : 39 (Deleted: 0) Binary : 6 (Ratio: 15.38%) Ternary : 2 (Ratio: 5.13%) Conflict : 39 (Average Length: 5.9 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 39 (Average: 8.62 Max: 215 Sum: 336) Executed : 38 (Average: 8.59 Max: 215 Sum: 335 Ratio: 99.70%) Bounded : 1 (Average: 1.00 Max: 1 Sum: 1 Ratio: 0.30%) Rules : 60629 Atoms : 60629 Bodies : 1 (Original: 0) Tight : Yes Variables : 16256 (Eliminated: 0 Frozen: 160) Constraints : 53667 (Binary: 95.3% Ternary: 3.3% Other: 1.4%) Memory Peak : 243MB Max. Length : 0 steps Models : 0 [endof: stats after solve call] Solving Time: 0.02s Memory: 183MB (+4MB) UNSAT Iteration Time: 0.41s 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: 187.0MB Grounding... [('step', [6]), ('step', [7]), ('step', [8]), ('step', [9]), ('step', [10]), ('check', [10])] Grounding Time: 0.31s Memory: 190MB (+7MB) Unblocking actions... Solving... [start: stats after solve call] Models : 1+ Calls : 3 Time : 1.940s (Solving: 0.05s 1st Model: 0.05s Unsat: 0.00s) CPU Time : 1.768s Choices : 2722 (Domain: 2398) Conflicts : 259 (Analyzed: 258) Restarts : 1 (Average: 258.00 Last: 88) Model-Level : 232.0 Problems : 3 (Average Length: 7.00 Splits: 0) Lemmas : 258 (Deleted: 0) Binary : 49 (Ratio: 18.99%) Ternary : 10 (Ratio: 3.88%) Conflict : 258 (Average Length: 141.4 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 258 (Average: 9.59 Max: 215 Sum: 2474) Executed : 257 (Average: 9.59 Max: 215 Sum: 2473 Ratio: 99.96%) Bounded : 1 (Average: 1.00 Max: 1 Sum: 1 Ratio: 0.04%) Rules : 60629 Atoms : 60629 Bodies : 1 (Original: 0) Tight : Yes Variables : 35632 (Eliminated: 0 Frozen: 320) Constraints : 211962 (Binary: 95.6% Ternary: 3.2% Other: 1.2%) Memory Peak : 243MB Max. Length : 5 steps Models : 1 [endof: stats after solve call] Solving Time: 0.07s Memory: 198MB (+8MB) SAT Testing... NOT SERIALIZABLE Testing Time: 1.11s Memory: 232MB (+34MB) Solving... [start: stats after solve call] Models : 0 Calls : 4 Time : 3.474s (Solving: 1.26s 1st Model: 0.05s Unsat: 1.21s) CPU Time : 3.304s Choices : 30145 (Domain: 22365) Conflicts : 3230 (Analyzed: 3228) Restarts : 34 (Average: 94.94 Last: 88) Model-Level : 232.0 Problems : 4 (Average Length: 8.25 Splits: 0) Lemmas : 3228 (Deleted: 881) Binary : 397 (Ratio: 12.30%) Ternary : 151 (Ratio: 4.68%) Conflict : 3228 (Average Length: 107.7 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 3228 (Average: 9.19 Max: 279 Sum: 29664) Executed : 3210 (Average: 9.14 Max: 279 Sum: 29492 Ratio: 99.42%) Bounded : 18 (Average: 9.56 Max: 12 Sum: 172 Ratio: 0.58%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 56254 (Eliminated: 0 Frozen: 15821) Constraints : 347145 (Binary: 91.4% Ternary: 7.0% Other: 1.7%) Memory Peak : 243MB Max. Length : 5 steps Models : 1 [endof: stats after solve call] Solving Time: 1.29s Memory: 232MB (+0MB) UNSAT Iteration Time: 2.92s Iteration 4 Queue: [(3,15,0,True), (4,20,0,True), (5,25,0,True), (6,30,0,True)] Grounded Until: 10 Expected Memory: 247.0MB Grounding... [('step', [11]), ('step', [12]), ('step', [13]), ('step', [14]), ('step', [15]), ('check', [15])] Grounding Time: 0.53s Memory: 233MB (+1MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 5 Time : 8.845s (Solving: 5.86s 1st Model: 0.05s Unsat: 1.21s) CPU Time : 8.676s Choices : 103836 (Domain: 87068) Conflicts : 12512 (Analyzed: 12510) Restarts : 134 (Average: 93.36 Last: 88) Model-Level : 232.0 Problems : 5 (Average Length: 10.00 Splits: 0) Lemmas : 12510 (Deleted: 7749) Binary : 1063 (Ratio: 8.50%) Ternary : 432 (Ratio: 3.45%) Conflict : 12510 (Average Length: 252.0 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 12510 (Average: 7.94 Max: 279 Sum: 99386) Executed : 12486 (Average: 7.92 Max: 279 Sum: 99128 Ratio: 99.74%) Bounded : 24 (Average: 10.75 Max: 17 Sum: 258 Ratio: 0.26%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 93745 (Eliminated: 0 Frozen: 27481) Constraints : 616110 (Binary: 91.4% Ternary: 6.9% Other: 1.7%) Memory Peak : 256MB Max. Length : 10 steps Models : 1 [endof: stats after solve call] Solving Time: 4.64s Memory: 256MB (+23MB) UNKNOWN Iteration Time: 5.38s Iteration 5 Queue: [(4,20,0,True), (5,25,0,True), (6,30,0,True)] Grounded Until: 15 Expected Memory: 280.0MB Grounding... [('step', [16]), ('step', [17]), ('step', [18]), ('step', [19]), ('step', [20]), ('check', [20])] Grounding Time: 0.52s Memory: 260MB (+4MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 6 Time : 14.658s (Solving: 10.90s 1st Model: 0.05s Unsat: 1.21s) CPU Time : 14.492s Choices : 211303 (Domain: 180150) Conflicts : 21112 (Analyzed: 21110) Restarts : 234 (Average: 90.21 Last: 88) Model-Level : 232.0 Problems : 6 (Average Length: 12.00 Splits: 0) Lemmas : 21110 (Deleted: 13943) Binary : 1736 (Ratio: 8.22%) Ternary : 559 (Ratio: 2.65%) Conflict : 21110 (Average Length: 469.1 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 21110 (Average: 9.38 Max: 279 Sum: 198058) Executed : 21086 (Average: 9.37 Max: 279 Sum: 197800 Ratio: 99.87%) Bounded : 24 (Average: 10.75 Max: 17 Sum: 258 Ratio: 0.13%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 131236 (Eliminated: 0 Frozen: 39141) Constraints : 895929 (Binary: 91.3% Ternary: 6.9% Other: 1.8%) Memory Peak : 279MB Max. Length : 15 steps Models : 1 [endof: stats after solve call] Solving Time: 5.08s Memory: 276MB (+16MB) UNKNOWN Iteration Time: 5.82s Iteration 6 Queue: [(5,25,0,True), (6,30,0,True)] Grounded Until: 20 Expected Memory: 300.0MB Grounding... [('step', [21]), ('step', [22]), ('step', [23]), ('step', [24]), ('step', [25]), ('check', [25])] Grounding Time: 0.59s Memory: 297MB (+21MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 7 Time : 22.194s (Solving: 17.55s 1st Model: 0.05s Unsat: 1.21s) CPU Time : 22.032s Choices : 342485 (Domain: 297737) Conflicts : 30164 (Analyzed: 30162) Restarts : 334 (Average: 90.31 Last: 140) Model-Level : 232.0 Problems : 7 (Average Length: 14.14 Splits: 0) Lemmas : 30162 (Deleted: 23746) Binary : 2202 (Ratio: 7.30%) Ternary : 639 (Ratio: 2.12%) Conflict : 30162 (Average Length: 754.0 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 30162 (Average: 10.51 Max: 279 Sum: 317028) Executed : 30138 (Average: 10.50 Max: 279 Sum: 316770 Ratio: 99.92%) Bounded : 24 (Average: 10.75 Max: 17 Sum: 258 Ratio: 0.08%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 168727 (Eliminated: 0 Frozen: 50801) Constraints : 1178389 (Binary: 91.3% Ternary: 7.0% Other: 1.8%) Memory Peak : 321MB Max. Length : 20 steps Models : 1 [endof: stats after solve call] Solving Time: 6.70s Memory: 309MB (+12MB) UNKNOWN Iteration Time: 7.55s Iteration 7 Queue: [(6,30,0,True)] Grounded Until: 25 Expected Memory: 342.0MB Grounding... [('step', [26]), ('step', [27]), ('step', [28]), ('step', [29]), ('step', [30]), ('check', [30])] Grounding Time: 0.51s Memory: 320MB (+11MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 8 Time : 29.950s (Solving: 24.48s 1st Model: 0.05s Unsat: 1.21s) CPU Time : 29.792s Choices : 512179 (Domain: 456274) Conflicts : 39563 (Analyzed: 39561) Restarts : 434 (Average: 91.15 Last: 140) Model-Level : 232.0 Problems : 8 (Average Length: 16.38 Splits: 0) Lemmas : 39561 (Deleted: 31975) Binary : 2733 (Ratio: 6.91%) Ternary : 842 (Ratio: 2.13%) Conflict : 39561 (Average Length: 835.8 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 39561 (Average: 12.00 Max: 376 Sum: 474587) Executed : 39537 (Average: 11.99 Max: 376 Sum: 474329 Ratio: 99.95%) Bounded : 24 (Average: 10.75 Max: 17 Sum: 258 Ratio: 0.05%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 206218 (Eliminated: 0 Frozen: 62461) Constraints : 1460849 (Binary: 91.3% Ternary: 7.0% Other: 1.8%) Memory Peak : 351MB Max. Length : 25 steps Models : 1 [endof: stats after solve call] Solving Time: 6.99s Memory: 351MB (+31MB) UNKNOWN Iteration Time: 7.77s Iteration 8 Queue: [(3,15,1,True), (4,20,1,True), (5,25,1,True), (6,30,1,True), (7,35,0,True), (8,40,0,True), (9,45,0,True), (10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True)] Grounded Until: 30 Blocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 9 Time : 35.005s (Solving: 29.48s 1st Model: 0.05s Unsat: 1.21s) CPU Time : 34.848s Choices : 572468 (Domain: 513333) Conflicts : 48077 (Analyzed: 48075) Restarts : 534 (Average: 90.03 Last: 140) Model-Level : 232.0 Problems : 9 (Average Length: 18.11 Splits: 0) Lemmas : 48075 (Deleted: 38492) Binary : 3056 (Ratio: 6.36%) Ternary : 952 (Ratio: 1.98%) Conflict : 48075 (Average Length: 744.5 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 48075 (Average: 11.05 Max: 376 Sum: 531408) Executed : 48042 (Average: 11.04 Max: 376 Sum: 530893 Ratio: 99.90%) Bounded : 33 (Average: 15.61 Max: 32 Sum: 515 Ratio: 0.10%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 206218 (Eliminated: 0 Frozen: 62461) Constraints : 1460849 (Binary: 91.3% Ternary: 7.0% Other: 1.8%) Memory Peak : 351MB Max. Length : 30 steps Models : 1 [endof: stats after solve call] Solving Time: 5.04s Memory: 351MB (+0MB) UNKNOWN Iteration Time: 5.06s Iteration 9 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)] Grounded Until: 30 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 10 Time : 41.742s (Solving: 36.16s 1st Model: 0.05s Unsat: 1.21s) CPU Time : 41.588s Choices : 691097 (Domain: 625619) Conflicts : 57169 (Analyzed: 57167) Restarts : 634 (Average: 90.17 Last: 140) Model-Level : 232.0 Problems : 10 (Average Length: 19.50 Splits: 0) Lemmas : 57167 (Deleted: 47025) Binary : 3594 (Ratio: 6.29%) Ternary : 1037 (Ratio: 1.81%) Conflict : 57167 (Average Length: 653.0 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 57167 (Average: 11.29 Max: 376 Sum: 645285) Executed : 57116 (Average: 11.27 Max: 376 Sum: 644194 Ratio: 99.83%) Bounded : 51 (Average: 21.39 Max: 32 Sum: 1091 Ratio: 0.17%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 206218 (Eliminated: 0 Frozen: 62461) Constraints : 1447526 (Binary: 91.3% Ternary: 6.9% Other: 1.8%) Memory Peak : 351MB Max. Length : 30 steps Models : 1 [endof: stats after solve call] Solving Time: 6.72s Memory: 351MB (+0MB) UNKNOWN Iteration Time: 6.74s Iteration 10 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)] Grounded Until: 30 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 11 Time : 48.237s (Solving: 42.60s 1st Model: 0.05s Unsat: 1.21s) CPU Time : 48.084s Choices : 813665 (Domain: 742103) Conflicts : 65982 (Analyzed: 65980) Restarts : 734 (Average: 89.89 Last: 140) Model-Level : 232.0 Problems : 11 (Average Length: 20.64 Splits: 0) Lemmas : 65980 (Deleted: 55101) Binary : 3910 (Ratio: 5.93%) Ternary : 1091 (Ratio: 1.65%) Conflict : 65980 (Average Length: 594.0 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 65980 (Average: 11.54 Max: 376 Sum: 761486) Executed : 65928 (Average: 11.52 Max: 376 Sum: 760363 Ratio: 99.85%) Bounded : 52 (Average: 21.60 Max: 32 Sum: 1123 Ratio: 0.15%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 206218 (Eliminated: 0 Frozen: 62461) Constraints : 1421367 (Binary: 91.3% Ternary: 6.9% Other: 1.8%) Memory Peak : 351MB Max. Length : 30 steps Models : 1 [endof: stats after solve call] Solving Time: 6.48s Memory: 351MB (+0MB) UNKNOWN Iteration Time: 6.50s Iteration 11 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)] Grounded Until: 30 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 12 Time : 54.791s (Solving: 49.10s 1st Model: 0.05s Unsat: 1.21s) CPU Time : 54.640s Choices : 975683 (Domain: 896919) Conflicts : 75075 (Analyzed: 75073) Restarts : 834 (Average: 90.02 Last: 140) Model-Level : 232.0 Problems : 12 (Average Length: 21.58 Splits: 0) Lemmas : 75073 (Deleted: 63176) Binary : 4079 (Ratio: 5.43%) Ternary : 1153 (Ratio: 1.54%) Conflict : 75073 (Average Length: 548.0 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 75073 (Average: 12.21 Max: 379 Sum: 916690) Executed : 75011 (Average: 12.19 Max: 379 Sum: 915267 Ratio: 99.84%) Bounded : 62 (Average: 22.95 Max: 32 Sum: 1423 Ratio: 0.16%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 206218 (Eliminated: 0 Frozen: 62461) Constraints : 1421353 (Binary: 91.3% Ternary: 6.9% Other: 1.8%) Memory Peak : 351MB Max. Length : 30 steps Models : 1 [endof: stats after solve call] Solving Time: 6.54s Memory: 351MB (+0MB) UNKNOWN Iteration Time: 6.56s Iteration 12 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)] Grounded Until: 30 Expected Memory: 393.0MB Grounding... [('step', [31]), ('step', [32]), ('step', [33]), ('step', [34]), ('step', [35]), ('check', [35])] Grounding Time: 0.51s Memory: 351MB (+0MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 13 Time : 62.263s (Solving: 55.73s 1st Model: 0.05s Unsat: 1.21s) CPU Time : 62.116s Choices : 1166383 (Domain: 1081139) Conflicts : 83872 (Analyzed: 83870) Restarts : 934 (Average: 89.80 Last: 140) Model-Level : 232.0 Problems : 13 (Average Length: 22.77 Splits: 0) Lemmas : 83870 (Deleted: 73543) Binary : 4283 (Ratio: 5.11%) Ternary : 1158 (Ratio: 1.38%) Conflict : 83870 (Average Length: 577.9 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 83870 (Average: 13.07 Max: 379 Sum: 1095790) Executed : 83808 (Average: 13.05 Max: 379 Sum: 1094367 Ratio: 99.87%) Bounded : 62 (Average: 22.95 Max: 32 Sum: 1423 Ratio: 0.13%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 243709 (Eliminated: 0 Frozen: 74121) Constraints : 1698855 (Binary: 91.3% Ternary: 6.9% Other: 1.8%) Memory Peak : 387MB Max. Length : 30 steps Models : 1 [endof: stats after solve call] Solving Time: 6.69s Memory: 366MB (+15MB) UNKNOWN Iteration Time: 7.49s Iteration 13 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)] Grounded Until: 35 Expected Memory: 408.0MB Grounding... [('step', [36]), ('step', [37]), ('step', [38]), ('step', [39]), ('step', [40]), ('check', [40])] Grounding Time: 0.52s Memory: 373MB (+7MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 14 Time : 70.787s (Solving: 63.38s 1st Model: 0.05s Unsat: 1.21s) CPU Time : 70.644s Choices : 1441455 (Domain: 1349673) Conflicts : 93173 (Analyzed: 93171) Restarts : 1034 (Average: 90.11 Last: 171) Model-Level : 232.0 Problems : 14 (Average Length: 24.14 Splits: 0) Lemmas : 93171 (Deleted: 81922) Binary : 4510 (Ratio: 4.84%) Ternary : 1170 (Ratio: 1.26%) Conflict : 93171 (Average Length: 591.7 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 93171 (Average: 14.57 Max: 379 Sum: 1357385) Executed : 93109 (Average: 14.55 Max: 379 Sum: 1355962 Ratio: 99.90%) Bounded : 62 (Average: 22.95 Max: 32 Sum: 1423 Ratio: 0.10%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 281200 (Eliminated: 0 Frozen: 85781) Constraints : 1981315 (Binary: 91.3% Ternary: 6.9% Other: 1.8%) Memory Peak : 413MB Max. Length : 35 steps Models : 1 [endof: stats after solve call] Solving Time: 7.72s Memory: 388MB (+15MB) UNKNOWN Iteration Time: 8.54s Iteration 14 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)] Grounded Until: 40 Expected Memory: 430.0MB Grounding... [('step', [41]), ('step', [42]), ('step', [43]), ('step', [44]), ('step', [45]), ('check', [45])] Grounding Time: 0.55s Memory: 398MB (+10MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 15 Time : 78.832s (Solving: 70.49s 1st Model: 0.05s Unsat: 1.21s) CPU Time : 78.692s Choices : 1705836 (Domain: 1608291) Conflicts : 101908 (Analyzed: 101906) Restarts : 1134 (Average: 89.86 Last: 171) Model-Level : 232.0 Problems : 15 (Average Length: 25.67 Splits: 0) Lemmas : 101906 (Deleted: 90852) Binary : 4725 (Ratio: 4.64%) Ternary : 1182 (Ratio: 1.16%) Conflict : 101906 (Average Length: 611.1 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 101906 (Average: 15.76 Max: 379 Sum: 1606482) Executed : 101844 (Average: 15.75 Max: 379 Sum: 1605059 Ratio: 99.91%) Bounded : 62 (Average: 22.95 Max: 32 Sum: 1423 Ratio: 0.09%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 318691 (Eliminated: 0 Frozen: 97441) Constraints : 2263775 (Binary: 91.3% Ternary: 6.9% Other: 1.8%) Memory Peak : 444MB Max. Length : 40 steps Models : 1 [endof: stats after solve call] Solving Time: 7.19s Memory: 443MB (+45MB) UNKNOWN Iteration Time: 8.06s Iteration 15 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)] Grounded Until: 45 Expected Memory: 498.0MB Grounding... [('step', [46]), ('step', [47]), ('step', [48]), ('step', [49]), ('step', [50]), ('check', [50])] Grounding Time: 0.71s Memory: 455MB (+12MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 16 Time : 87.817s (Solving: 78.36s 1st Model: 0.05s Unsat: 1.21s) CPU Time : 87.684s Choices : 2055917 (Domain: 1950118) Conflicts : 111026 (Analyzed: 111024) Restarts : 1234 (Average: 89.97 Last: 171) Model-Level : 232.0 Problems : 16 (Average Length: 27.31 Splits: 0) Lemmas : 111024 (Deleted: 99174) Binary : 4895 (Ratio: 4.41%) Ternary : 1192 (Ratio: 1.07%) Conflict : 111024 (Average Length: 621.7 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 111024 (Average: 17.46 Max: 446 Sum: 1938272) Executed : 110962 (Average: 17.45 Max: 446 Sum: 1936849 Ratio: 99.93%) Bounded : 62 (Average: 22.95 Max: 32 Sum: 1423 Ratio: 0.07%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 356182 (Eliminated: 0 Frozen: 109101) Constraints : 2546235 (Binary: 91.3% Ternary: 6.9% Other: 1.8%) Memory Peak : 503MB Max. Length : 45 steps Models : 1 [endof: stats after solve call] Solving Time: 7.95s Memory: 466MB (+11MB) UNKNOWN Iteration Time: 9.00s Iteration 16 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)] Grounded Until: 50 Expected Memory: 521.0MB Grounding... [('step', [51]), ('step', [52]), ('step', [53]), ('step', [54]), ('step', [55]), ('check', [55])] Grounding Time: 0.51s Memory: 470MB (+4MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 17 Time : 97.681s (Solving: 87.30s 1st Model: 0.05s Unsat: 1.21s) CPU Time : 97.552s Choices : 2398484 (Domain: 2284416) Conflicts : 119941 (Analyzed: 119939) Restarts : 1334 (Average: 89.91 Last: 171) Model-Level : 232.0 Problems : 17 (Average Length: 29.06 Splits: 0) Lemmas : 119939 (Deleted: 107938) Binary : 5014 (Ratio: 4.18%) Ternary : 1207 (Ratio: 1.01%) Conflict : 119939 (Average Length: 645.7 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 119939 (Average: 18.85 Max: 499 Sum: 2260480) Executed : 119877 (Average: 18.84 Max: 499 Sum: 2259057 Ratio: 99.94%) Bounded : 62 (Average: 22.95 Max: 32 Sum: 1423 Ratio: 0.06%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 393673 (Eliminated: 0 Frozen: 120761) Constraints : 2828695 (Binary: 91.3% Ternary: 7.0% Other: 1.8%) Memory Peak : 526MB Max. Length : 50 steps Models : 1 [endof: stats after solve call] Solving Time: 9.03s Memory: 489MB (+19MB) UNKNOWN Iteration Time: 9.88s Iteration 17 Queue: [(12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True)] Grounded Until: 55 Expected Memory: 544.0MB Grounding... [('step', [56]), ('step', [57]), ('step', [58]), ('step', [59]), ('step', [60]), ('check', [60])] Grounding Time: 0.51s Memory: 495MB (+6MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 18 Time : 106.588s (Solving: 95.26s 1st Model: 0.05s Unsat: 1.21s) CPU Time : 106.464s Choices : 2642560 (Domain: 2523631) Conflicts : 127720 (Analyzed: 127718) Restarts : 1434 (Average: 89.06 Last: 171) Model-Level : 232.0 Problems : 18 (Average Length: 30.89 Splits: 0) Lemmas : 127718 (Deleted: 114420) Binary : 5093 (Ratio: 3.99%) Ternary : 1214 (Ratio: 0.95%) Conflict : 127718 (Average Length: 676.0 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 127718 (Average: 19.44 Max: 569 Sum: 2482581) Executed : 127656 (Average: 19.43 Max: 569 Sum: 2481158 Ratio: 99.94%) Bounded : 62 (Average: 22.95 Max: 32 Sum: 1423 Ratio: 0.06%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 431164 (Eliminated: 0 Frozen: 132421) Constraints : 3111155 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 556MB Max. Length : 55 steps Models : 1 [endof: stats after solve call] Solving Time: 8.05s Memory: 552MB (+57MB) UNKNOWN Iteration Time: 8.92s Iteration 18 Queue: [(13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True)] Grounded Until: 60 Expected Memory: 615.0MB Grounding... [('step', [61]), ('step', [62]), ('step', [63]), ('step', [64]), ('step', [65]), ('check', [65])] Grounding Time: 0.55s Memory: 552MB (+0MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 19 Time : 116.529s (Solving: 104.18s 1st Model: 0.05s Unsat: 1.21s) CPU Time : 116.408s Choices : 2932709 (Domain: 2808890) Conflicts : 135866 (Analyzed: 135864) Restarts : 1534 (Average: 88.57 Last: 171) Model-Level : 232.0 Problems : 19 (Average Length: 32.79 Splits: 0) Lemmas : 135864 (Deleted: 121994) Binary : 5150 (Ratio: 3.79%) Ternary : 1221 (Ratio: 0.90%) Conflict : 135864 (Average Length: 710.5 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 135864 (Average: 20.22 Max: 611 Sum: 2747824) Executed : 135802 (Average: 20.21 Max: 611 Sum: 2746401 Ratio: 99.95%) Bounded : 62 (Average: 22.95 Max: 32 Sum: 1423 Ratio: 0.05%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 468655 (Eliminated: 0 Frozen: 144081) Constraints : 3393615 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 610MB Max. Length : 60 steps Models : 1 [endof: stats after solve call] Solving Time: 9.02s Memory: 558MB (+6MB) UNKNOWN Iteration Time: 9.95s Iteration 19 Queue: [(14,70,0,True), (15,75,0,True), (16,80,0,True)] Grounded Until: 65 Expected Memory: 621.0MB Grounding... [('step', [66]), ('step', [67]), ('step', [68]), ('step', [69]), ('step', [70]), ('check', [70])] Grounding Time: 0.69s Memory: 562MB (+4MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 20 Time : 127.471s (Solving: 113.82s 1st Model: 0.05s Unsat: 1.21s) CPU Time : 127.356s Choices : 3303866 (Domain: 3174338) Conflicts : 144117 (Analyzed: 144115) Restarts : 1634 (Average: 88.20 Last: 171) Model-Level : 232.0 Problems : 20 (Average Length: 34.75 Splits: 0) Lemmas : 144115 (Deleted: 129925) Binary : 5189 (Ratio: 3.60%) Ternary : 1228 (Ratio: 0.85%) Conflict : 144115 (Average Length: 754.2 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 144115 (Average: 21.46 Max: 635 Sum: 3093045) Executed : 144053 (Average: 21.45 Max: 635 Sum: 3091622 Ratio: 99.95%) Bounded : 62 (Average: 22.95 Max: 32 Sum: 1423 Ratio: 0.05%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 506146 (Eliminated: 0 Frozen: 155741) Constraints : 3676075 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 632MB Max. Length : 65 steps Models : 1 [endof: stats after solve call] Solving Time: 9.77s Memory: 583MB (+21MB) UNKNOWN Iteration Time: 10.96s Iteration 20 Queue: [(15,75,0,True), (16,80,0,True)] Grounded Until: 70 Expected Memory: 646.0MB Grounding... [('step', [71]), ('step', [72]), ('step', [73]), ('step', [74]), ('step', [75]), ('check', [75])] Grounding Time: 0.52s Memory: 586MB (+3MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 21 Time : 138.933s (Solving: 124.26s 1st Model: 0.05s Unsat: 1.21s) CPU Time : 138.824s Choices : 3707054 (Domain: 3571644) Conflicts : 152100 (Analyzed: 152098) Restarts : 1734 (Average: 87.72 Last: 171) Model-Level : 232.0 Problems : 21 (Average Length: 36.76 Splits: 0) Lemmas : 152098 (Deleted: 137993) Binary : 5235 (Ratio: 3.44%) Ternary : 1231 (Ratio: 0.81%) Conflict : 152098 (Average Length: 787.1 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 152098 (Average: 22.81 Max: 738 Sum: 3468709) Executed : 152036 (Average: 22.80 Max: 738 Sum: 3467286 Ratio: 99.96%) Bounded : 62 (Average: 22.95 Max: 32 Sum: 1423 Ratio: 0.04%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 543637 (Eliminated: 0 Frozen: 167401) Constraints : 3958535 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 667MB Max. Length : 70 steps Models : 1 [endof: stats after solve call] Solving Time: 10.55s Memory: 612MB (+26MB) UNKNOWN Iteration Time: 11.48s Iteration 21 Queue: [(16,80,0,True)] Grounded Until: 75 Expected Memory: 675.0MB Grounding... [('step', [76]), ('step', [77]), ('step', [78]), ('step', [79]), ('step', [80]), ('check', [80])] Grounding Time: 0.55s Memory: 612MB (+0MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 22 Time : 149.974s (Solving: 134.21s 1st Model: 0.05s Unsat: 1.21s) CPU Time : 149.872s Choices : 4059006 (Domain: 3920012) Conflicts : 160160 (Analyzed: 160158) Restarts : 1834 (Average: 87.33 Last: 171) Model-Level : 232.0 Problems : 22 (Average Length: 38.82 Splits: 0) Lemmas : 160158 (Deleted: 145865) Binary : 5268 (Ratio: 3.29%) Ternary : 1232 (Ratio: 0.77%) Conflict : 160158 (Average Length: 816.9 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 160158 (Average: 23.68 Max: 757 Sum: 3792366) Executed : 160096 (Average: 23.67 Max: 757 Sum: 3790943 Ratio: 99.96%) Bounded : 62 (Average: 22.95 Max: 32 Sum: 1423 Ratio: 0.04%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 581128 (Eliminated: 0 Frozen: 179061) Constraints : 4240995 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 693MB Max. Length : 75 steps Models : 1 [endof: stats after solve call] Solving Time: 10.07s Memory: 634MB (+22MB) UNKNOWN Iteration Time: 11.06s Iteration 22 Queue: [(3,15,2,True), (4,20,2,True), (5,25,2,True), (6,30,2,True), (7,35,1,True), (8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True)] Grounded Until: 80 Blocking actions... Solving... [start: stats after solve call] Models : 0 Calls : 23 Time : 153.223s (Solving: 137.32s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 153.120s Choices : 4102110 (Domain: 3956848) Conflicts : 165846 (Analyzed: 165843) Restarts : 1896 (Average: 87.47 Last: 171) Model-Level : 232.0 Problems : 23 (Average Length: 40.70 Splits: 0) Lemmas : 165843 (Deleted: 151150) Binary : 5391 (Ratio: 3.25%) Ternary : 1260 (Ratio: 0.76%) Conflict : 165843 (Average Length: 798.8 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 165843 (Average: 23.11 Max: 757 Sum: 3832765) Executed : 165780 (Average: 23.10 Max: 757 Sum: 3831341 Ratio: 99.96%) Bounded : 63 (Average: 22.60 Max: 32 Sum: 1424 Ratio: 0.04%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 581128 (Eliminated: 0 Frozen: 179061) Constraints : 4240995 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 693MB Max. Length : 80 steps Models : 1 [endof: stats after solve call] Solving Time: 3.20s Memory: 634MB (+0MB) UNSAT Iteration Time: 3.25s Iteration 23 Queue: [(4,20,2,True), (5,25,2,True), (6,30,2,True), (7,35,1,True), (8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True)] Grounded Until: 80 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 24 Time : 159.643s (Solving: 143.60s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 159.544s Choices : 4185039 (Domain: 4034081) Conflicts : 175012 (Analyzed: 175009) Restarts : 1996 (Average: 87.68 Last: 171) Model-Level : 232.0 Problems : 24 (Average Length: 42.42 Splits: 0) Lemmas : 175009 (Deleted: 158813) Binary : 5520 (Ratio: 3.15%) Ternary : 1305 (Ratio: 0.75%) Conflict : 175009 (Average Length: 768.9 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 175009 (Average: 22.34 Max: 757 Sum: 3909668) Executed : 174941 (Average: 22.33 Max: 757 Sum: 3907844 Ratio: 99.95%) Bounded : 68 (Average: 26.82 Max: 82 Sum: 1824 Ratio: 0.05%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 581128 (Eliminated: 0 Frozen: 179061) Constraints : 4240995 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 693MB Max. Length : 80 steps Models : 1 [endof: stats after solve call] Solving Time: 6.37s Memory: 634MB (+0MB) UNKNOWN Iteration Time: 6.43s Iteration 24 Queue: [(5,25,2,True), (6,30,2,True), (7,35,1,True), (8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True)] Grounded Until: 80 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 25 Time : 165.668s (Solving: 149.50s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 165.572s Choices : 4286134 (Domain: 4130555) Conflicts : 183460 (Analyzed: 183457) Restarts : 2096 (Average: 87.53 Last: 171) Model-Level : 232.0 Problems : 25 (Average Length: 44.00 Splits: 0) Lemmas : 183457 (Deleted: 165507) Binary : 5683 (Ratio: 3.10%) Ternary : 1337 (Ratio: 0.73%) Conflict : 183457 (Average Length: 742.2 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 183457 (Average: 21.82 Max: 757 Sum: 4003175) Executed : 183385 (Average: 21.81 Max: 757 Sum: 4001028 Ratio: 99.95%) Bounded : 72 (Average: 29.82 Max: 82 Sum: 2147 Ratio: 0.05%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 581128 (Eliminated: 0 Frozen: 179061) Constraints : 4238341 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 693MB Max. Length : 80 steps Models : 1 [endof: stats after solve call] Solving Time: 5.98s Memory: 634MB (+0MB) UNKNOWN Iteration Time: 6.03s Iteration 25 Queue: [(6,30,2,True), (7,35,1,True), (8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True)] Grounded Until: 80 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 26 Time : 173.591s (Solving: 157.30s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 173.500s Choices : 4427678 (Domain: 4268820) Conflicts : 192474 (Analyzed: 192471) Restarts : 2196 (Average: 87.65 Last: 171) Model-Level : 232.0 Problems : 26 (Average Length: 45.46 Splits: 0) Lemmas : 192471 (Deleted: 175226) Binary : 5896 (Ratio: 3.06%) Ternary : 1418 (Ratio: 0.74%) Conflict : 192471 (Average Length: 715.8 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 192471 (Average: 21.50 Max: 757 Sum: 4138345) Executed : 192393 (Average: 21.49 Max: 757 Sum: 4135707 Ratio: 99.94%) Bounded : 78 (Average: 33.82 Max: 82 Sum: 2638 Ratio: 0.06%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 581128 (Eliminated: 0 Frozen: 179061) Constraints : 4235686 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 693MB Max. Length : 80 steps Models : 1 [endof: stats after solve call] Solving Time: 7.88s Memory: 634MB (+0MB) UNKNOWN Iteration Time: 7.93s Iteration 26 Queue: [(7,35,1,True), (8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True)] Grounded Until: 80 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 27 Time : 181.098s (Solving: 164.69s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 181.012s Choices : 4592519 (Domain: 4428597) Conflicts : 201935 (Analyzed: 201932) Restarts : 2296 (Average: 87.95 Last: 171) Model-Level : 232.0 Problems : 27 (Average Length: 46.81 Splits: 0) Lemmas : 201932 (Deleted: 183642) Binary : 6076 (Ratio: 3.01%) Ternary : 1447 (Ratio: 0.72%) Conflict : 201932 (Average Length: 693.3 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 201932 (Average: 21.26 Max: 757 Sum: 4293207) Executed : 201850 (Average: 21.25 Max: 757 Sum: 4290246 Ratio: 99.93%) Bounded : 82 (Average: 36.11 Max: 82 Sum: 2961 Ratio: 0.07%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 581128 (Eliminated: 0 Frozen: 179061) Constraints : 4235616 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 693MB Max. Length : 80 steps Models : 1 [endof: stats after solve call] Solving Time: 7.47s Memory: 634MB (+0MB) UNKNOWN Iteration Time: 7.51s Iteration 27 Queue: [(8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True)] Grounded Until: 80 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 28 Time : 187.709s (Solving: 171.19s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 187.624s Choices : 4727569 (Domain: 4561362) Conflicts : 210487 (Analyzed: 210484) Restarts : 2396 (Average: 87.85 Last: 171) Model-Level : 232.0 Problems : 28 (Average Length: 48.07 Splits: 0) Lemmas : 210484 (Deleted: 190748) Binary : 6158 (Ratio: 2.93%) Ternary : 1477 (Ratio: 0.70%) Conflict : 210484 (Average Length: 679.1 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 210484 (Average: 20.97 Max: 757 Sum: 4414229) Executed : 210402 (Average: 20.96 Max: 757 Sum: 4411268 Ratio: 99.93%) Bounded : 82 (Average: 36.11 Max: 82 Sum: 2961 Ratio: 0.07%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 581128 (Eliminated: 0 Frozen: 179061) Constraints : 4233123 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 693MB Max. Length : 80 steps Models : 1 [endof: stats after solve call] Solving Time: 6.57s Memory: 634MB (+0MB) UNKNOWN Iteration Time: 6.62s Iteration 28 Queue: [(9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True)] Grounded Until: 80 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 29 Time : 195.681s (Solving: 179.05s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 195.600s Choices : 4887925 (Domain: 4719575) Conflicts : 219292 (Analyzed: 219289) Restarts : 2496 (Average: 87.86 Last: 171) Model-Level : 232.0 Problems : 29 (Average Length: 49.24 Splits: 0) Lemmas : 219289 (Deleted: 200807) Binary : 6237 (Ratio: 2.84%) Ternary : 1495 (Ratio: 0.68%) Conflict : 219289 (Average Length: 664.0 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 219289 (Average: 20.81 Max: 757 Sum: 4562664) Executed : 219206 (Average: 20.79 Max: 757 Sum: 4559621 Ratio: 99.93%) Bounded : 83 (Average: 36.66 Max: 82 Sum: 3043 Ratio: 0.07%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 581128 (Eliminated: 0 Frozen: 179061) Constraints : 4233123 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 693MB Max. Length : 80 steps Models : 1 [endof: stats after solve call] Solving Time: 7.94s Memory: 634MB (+0MB) UNKNOWN Iteration Time: 7.98s Iteration 29 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,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True)] Grounded Until: 80 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 30 Time : 203.399s (Solving: 186.63s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 203.316s Choices : 5071989 (Domain: 4901353) Conflicts : 228260 (Analyzed: 228257) Restarts : 2596 (Average: 87.93 Last: 171) Model-Level : 232.0 Problems : 30 (Average Length: 50.33 Splits: 0) Lemmas : 228257 (Deleted: 209279) Binary : 6308 (Ratio: 2.76%) Ternary : 1518 (Ratio: 0.67%) Conflict : 228257 (Average Length: 651.1 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 228257 (Average: 20.74 Max: 757 Sum: 4733668) Executed : 228171 (Average: 20.72 Max: 757 Sum: 4730379 Ratio: 99.93%) Bounded : 86 (Average: 38.24 Max: 82 Sum: 3289 Ratio: 0.07%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 581128 (Eliminated: 0 Frozen: 179061) Constraints : 4233109 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 693MB Max. Length : 80 steps Models : 1 [endof: stats after solve call] Solving Time: 7.66s Memory: 634MB (+0MB) UNKNOWN Iteration Time: 7.72s Iteration 30 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,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True)] Grounded Until: 80 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 31 Time : 211.840s (Solving: 194.95s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 211.764s Choices : 5313058 (Domain: 5140075) Conflicts : 236990 (Analyzed: 236987) Restarts : 2696 (Average: 87.90 Last: 171) Model-Level : 232.0 Problems : 31 (Average Length: 51.35 Splits: 0) Lemmas : 236987 (Deleted: 217931) Binary : 6370 (Ratio: 2.69%) Ternary : 1537 (Ratio: 0.65%) Conflict : 236987 (Average Length: 639.4 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 236987 (Average: 20.93 Max: 757 Sum: 4959477) Executed : 236898 (Average: 20.91 Max: 757 Sum: 4955942 Ratio: 99.93%) Bounded : 89 (Average: 39.72 Max: 82 Sum: 3535 Ratio: 0.07%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 581128 (Eliminated: 0 Frozen: 179061) Constraints : 4225687 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 693MB Max. Length : 80 steps Models : 1 [endof: stats after solve call] Solving Time: 8.41s Memory: 634MB (+0MB) UNKNOWN Iteration Time: 8.45s Iteration 31 Queue: [(12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True)] Grounded Until: 80 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 32 Time : 221.004s (Solving: 203.98s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 220.932s Choices : 5542471 (Domain: 5367579) Conflicts : 246068 (Analyzed: 246065) Restarts : 2796 (Average: 88.01 Last: 171) Model-Level : 232.0 Problems : 32 (Average Length: 52.31 Splits: 0) Lemmas : 246065 (Deleted: 226327) Binary : 6435 (Ratio: 2.62%) Ternary : 1552 (Ratio: 0.63%) Conflict : 246065 (Average Length: 626.1 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 246065 (Average: 21.03 Max: 757 Sum: 5175088) Executed : 245976 (Average: 21.02 Max: 757 Sum: 5171553 Ratio: 99.93%) Bounded : 89 (Average: 39.72 Max: 82 Sum: 3535 Ratio: 0.07%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 581128 (Eliminated: 0 Frozen: 179061) Constraints : 4225645 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 693MB Max. Length : 80 steps Models : 1 [endof: stats after solve call] Solving Time: 9.12s Memory: 634MB (+0MB) UNKNOWN Iteration Time: 9.17s Iteration 32 Queue: [(13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True)] Grounded Until: 80 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 33 Time : 229.704s (Solving: 212.56s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 229.636s Choices : 5750754 (Domain: 5573773) Conflicts : 255157 (Analyzed: 255154) Restarts : 2896 (Average: 88.11 Last: 171) Model-Level : 232.0 Problems : 33 (Average Length: 53.21 Splits: 0) Lemmas : 255154 (Deleted: 235100) Binary : 6488 (Ratio: 2.54%) Ternary : 1566 (Ratio: 0.61%) Conflict : 255154 (Average Length: 614.5 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 255154 (Average: 21.03 Max: 838 Sum: 5366586) Executed : 255064 (Average: 21.02 Max: 838 Sum: 5362969 Ratio: 99.93%) Bounded : 90 (Average: 40.19 Max: 82 Sum: 3617 Ratio: 0.07%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 581128 (Eliminated: 0 Frozen: 179061) Constraints : 4225645 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 693MB Max. Length : 80 steps Models : 1 [endof: stats after solve call] Solving Time: 8.67s Memory: 634MB (+0MB) UNKNOWN Iteration Time: 8.71s Iteration 33 Queue: [(14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True)] Grounded Until: 80 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 34 Time : 239.332s (Solving: 222.04s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 239.268s Choices : 6060054 (Domain: 5880820) Conflicts : 264307 (Analyzed: 264304) Restarts : 2996 (Average: 88.22 Last: 171) Model-Level : 232.0 Problems : 34 (Average Length: 54.06 Splits: 0) Lemmas : 264304 (Deleted: 243919) Binary : 6557 (Ratio: 2.48%) Ternary : 1576 (Ratio: 0.60%) Conflict : 264304 (Average Length: 605.5 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 264304 (Average: 21.40 Max: 838 Sum: 5655935) Executed : 264212 (Average: 21.39 Max: 838 Sum: 5652154 Ratio: 99.93%) Bounded : 92 (Average: 41.10 Max: 82 Sum: 3781 Ratio: 0.07%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 581128 (Eliminated: 0 Frozen: 179061) Constraints : 4225619 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 693MB Max. Length : 80 steps Models : 1 [endof: stats after solve call] Solving Time: 9.58s Memory: 634MB (+0MB) UNKNOWN Iteration Time: 9.64s Iteration 34 Queue: [(15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True)] Grounded Until: 80 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 35 Time : 249.187s (Solving: 231.77s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 249.128s Choices : 6410855 (Domain: 6229173) Conflicts : 273012 (Analyzed: 273009) Restarts : 3096 (Average: 88.18 Last: 171) Model-Level : 232.0 Problems : 35 (Average Length: 54.86 Splits: 0) Lemmas : 273009 (Deleted: 252778) Binary : 6645 (Ratio: 2.43%) Ternary : 1588 (Ratio: 0.58%) Conflict : 273009 (Average Length: 596.4 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 273009 (Average: 21.94 Max: 838 Sum: 5989657) Executed : 272916 (Average: 21.93 Max: 838 Sum: 5985794 Ratio: 99.94%) Bounded : 93 (Average: 41.54 Max: 82 Sum: 3863 Ratio: 0.06%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 581128 (Eliminated: 0 Frozen: 179061) Constraints : 4225591 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 693MB Max. Length : 80 steps Models : 1 [endof: stats after solve call] Solving Time: 9.81s Memory: 634MB (+0MB) UNKNOWN Iteration Time: 9.86s Iteration 35 Queue: [(16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True)] Grounded Until: 80 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 36 Time : 260.772s (Solving: 243.21s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 260.716s Choices : 6824452 (Domain: 6640165) Conflicts : 282018 (Analyzed: 282015) Restarts : 3196 (Average: 88.24 Last: 171) Model-Level : 232.0 Problems : 36 (Average Length: 55.61 Splits: 0) Lemmas : 282015 (Deleted: 261088) Binary : 6710 (Ratio: 2.38%) Ternary : 1606 (Ratio: 0.57%) Conflict : 282015 (Average Length: 588.9 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 282015 (Average: 22.64 Max: 858 Sum: 6385189) Executed : 281919 (Average: 22.63 Max: 858 Sum: 6381080 Ratio: 99.94%) Bounded : 96 (Average: 42.80 Max: 82 Sum: 4109 Ratio: 0.06%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 581128 (Eliminated: 0 Frozen: 179061) Constraints : 4225577 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 693MB Max. Length : 80 steps Models : 1 [endof: stats after solve call] Solving Time: 11.53s Memory: 634MB (+0MB) UNKNOWN Iteration Time: 11.59s Iteration 36 Queue: [(17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True)] Grounded Until: 80 Expected Memory: 697.0MB Grounding... [('step', [81]), ('step', [82]), ('step', [83]), ('step', [84]), ('step', [85]), ('check', [85])] Grounding Time: 0.54s Memory: 634MB (+0MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 37 Time : 271.623s (Solving: 252.97s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 271.572s Choices : 7411320 (Domain: 7222276) Conflicts : 291091 (Analyzed: 291088) Restarts : 3296 (Average: 88.32 Last: 171) Model-Level : 232.0 Problems : 37 (Average Length: 56.46 Splits: 0) Lemmas : 291088 (Deleted: 271360) Binary : 6802 (Ratio: 2.34%) Ternary : 1620 (Ratio: 0.56%) Conflict : 291088 (Average Length: 592.6 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 291088 (Average: 23.86 Max: 858 Sum: 6944736) Executed : 290992 (Average: 23.84 Max: 858 Sum: 6940627 Ratio: 99.94%) Bounded : 96 (Average: 42.80 Max: 82 Sum: 4109 Ratio: 0.06%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 618619 (Eliminated: 0 Frozen: 190721) Constraints : 4507997 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 721MB Max. Length : 80 steps Models : 1 [endof: stats after solve call] Solving Time: 9.88s Memory: 656MB (+22MB) UNKNOWN Iteration Time: 10.86s Iteration 37 Queue: [(18,90,0,True), (19,95,0,True), (20,100,0,True)] Grounded Until: 85 Expected Memory: 719.0MB Grounding... [('step', [86]), ('step', [87]), ('step', [88]), ('step', [89]), ('step', [90]), ('check', [90])] Grounding Time: 0.54s Memory: 656MB (+0MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 38 Time : 282.965s (Solving: 263.19s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 282.920s Choices : 7871747 (Domain: 7678415) Conflicts : 300144 (Analyzed: 300141) Restarts : 3396 (Average: 88.38 Last: 171) Model-Level : 232.0 Problems : 38 (Average Length: 57.39 Splits: 0) Lemmas : 300141 (Deleted: 279896) Binary : 6830 (Ratio: 2.28%) Ternary : 1624 (Ratio: 0.54%) Conflict : 300141 (Average Length: 607.1 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 300141 (Average: 24.57 Max: 872 Sum: 7372975) Executed : 300045 (Average: 24.55 Max: 872 Sum: 7368866 Ratio: 99.94%) Bounded : 96 (Average: 42.80 Max: 82 Sum: 4109 Ratio: 0.06%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 656110 (Eliminated: 0 Frozen: 202381) Constraints : 4790457 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 747MB Max. Length : 85 steps Models : 1 [endof: stats after solve call] Solving Time: 10.35s Memory: 736MB (+80MB) UNKNOWN Iteration Time: 11.36s Iteration 38 Queue: [(19,95,0,True), (20,100,0,True)] Grounded Until: 90 Expected Memory: 816.0MB Grounding... [('step', [91]), ('step', [92]), ('step', [93]), ('step', [94]), ('step', [95]), ('check', [95])] Grounding Time: 0.57s Memory: 736MB (+0MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 39 Time : 294.377s (Solving: 273.45s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 294.336s Choices : 8308208 (Domain: 8111509) Conflicts : 308200 (Analyzed: 308197) Restarts : 3496 (Average: 88.16 Last: 171) Model-Level : 232.0 Problems : 39 (Average Length: 58.41 Splits: 0) Lemmas : 308197 (Deleted: 287291) Binary : 6860 (Ratio: 2.23%) Ternary : 1625 (Ratio: 0.53%) Conflict : 308197 (Average Length: 622.1 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 308197 (Average: 25.23 Max: 908 Sum: 7776203) Executed : 308101 (Average: 25.22 Max: 908 Sum: 7772094 Ratio: 99.95%) Bounded : 96 (Average: 42.80 Max: 82 Sum: 4109 Ratio: 0.05%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 693601 (Eliminated: 0 Frozen: 214041) Constraints : 5072917 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 821MB Max. Length : 90 steps Models : 1 [endof: stats after solve call] Solving Time: 10.39s Memory: 741MB (+5MB) UNKNOWN Iteration Time: 11.43s Iteration 39 Queue: [(20,100,0,True)] Grounded Until: 95 Expected Memory: 821.0MB Grounding... [('step', [96]), ('step', [97]), ('step', [98]), ('step', [99]), ('step', [100]), ('check', [100])] Grounding Time: 0.89s Memory: 791MB (+50MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 40 Time : 306.163s (Solving: 283.74s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 306.128s Choices : 8710733 (Domain: 8511380) Conflicts : 316103 (Analyzed: 316100) Restarts : 3596 (Average: 87.90 Last: 171) Model-Level : 232.0 Problems : 40 (Average Length: 59.50 Splits: 0) Lemmas : 316100 (Deleted: 295218) Binary : 6901 (Ratio: 2.18%) Ternary : 1637 (Ratio: 0.52%) Conflict : 316100 (Average Length: 638.8 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 316100 (Average: 25.76 Max: 976 Sum: 8144273) Executed : 316004 (Average: 25.75 Max: 976 Sum: 8140164 Ratio: 99.95%) Bounded : 96 (Average: 42.80 Max: 82 Sum: 4109 Ratio: 0.05%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 731092 (Eliminated: 0 Frozen: 225701) Constraints : 5355377 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 880MB Max. Length : 95 steps Models : 1 [endof: stats after solve call] Solving Time: 10.43s Memory: 796MB (+5MB) UNKNOWN Iteration Time: 11.80s 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,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,0,True), (22,110,0,True), (23,115,0,True)] Grounded Until: 100 Blocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 41 Time : 312.207s (Solving: 289.62s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 312.176s Choices : 8779008 (Domain: 8577752) Conflicts : 324510 (Analyzed: 324507) Restarts : 3696 (Average: 87.80 Last: 171) Model-Level : 232.0 Problems : 41 (Average Length: 60.54 Splits: 0) Lemmas : 324507 (Deleted: 301177) Binary : 6958 (Ratio: 2.14%) Ternary : 1650 (Ratio: 0.51%) Conflict : 324507 (Average Length: 627.9 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 324507 (Average: 25.28 Max: 976 Sum: 8204966) Executed : 324410 (Average: 25.27 Max: 976 Sum: 8200755 Ratio: 99.95%) Bounded : 97 (Average: 43.41 Max: 102 Sum: 4211 Ratio: 0.05%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 731092 (Eliminated: 0 Frozen: 225701) Constraints : 5355377 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 880MB Max. Length : 100 steps Models : 1 [endof: stats after solve call] Solving Time: 5.99s Memory: 796MB (+0MB) UNKNOWN Iteration Time: 6.05s 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,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,0,True), (22,110,0,True), (23,115,0,True)] Grounded Until: 100 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 42 Time : 318.722s (Solving: 295.99s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 318.692s Choices : 8860079 (Domain: 8657179) Conflicts : 332935 (Analyzed: 332932) Restarts : 3796 (Average: 87.71 Last: 171) Model-Level : 232.0 Problems : 42 (Average Length: 61.52 Splits: 0) Lemmas : 332932 (Deleted: 308970) Binary : 7018 (Ratio: 2.11%) Ternary : 1657 (Ratio: 0.50%) Conflict : 332932 (Average Length: 618.5 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 332932 (Average: 24.86 Max: 976 Sum: 8278011) Executed : 332835 (Average: 24.85 Max: 976 Sum: 8273800 Ratio: 99.95%) Bounded : 97 (Average: 43.41 Max: 102 Sum: 4211 Ratio: 0.05%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 731092 (Eliminated: 0 Frozen: 225701) Constraints : 5352748 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 880MB Max. Length : 100 steps Models : 1 [endof: stats after solve call] Solving Time: 6.47s Memory: 796MB (+0MB) UNKNOWN Iteration Time: 6.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,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,0,True), (22,110,0,True), (23,115,0,True)] Grounded Until: 100 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 43 Time : 326.155s (Solving: 303.28s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 326.128s Choices : 8969018 (Domain: 8764164) Conflicts : 341388 (Analyzed: 341385) Restarts : 3896 (Average: 87.62 Last: 171) Model-Level : 232.0 Problems : 43 (Average Length: 62.47 Splits: 0) Lemmas : 341385 (Deleted: 317209) Binary : 7071 (Ratio: 2.07%) Ternary : 1684 (Ratio: 0.49%) Conflict : 341385 (Average Length: 609.6 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 341385 (Average: 24.54 Max: 976 Sum: 8377527) Executed : 341288 (Average: 24.53 Max: 976 Sum: 8373316 Ratio: 99.95%) Bounded : 97 (Average: 43.41 Max: 102 Sum: 4211 Ratio: 0.05%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 731092 (Eliminated: 0 Frozen: 225701) Constraints : 5352748 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 880MB Max. Length : 100 steps Models : 1 [endof: stats after solve call] Solving Time: 7.38s Memory: 796MB (+0MB) UNKNOWN Iteration Time: 7.44s 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,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,0,True), (22,110,0,True), (23,115,0,True)] Grounded Until: 100 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 44 Time : 333.597s (Solving: 310.58s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 333.576s Choices : 9054468 (Domain: 8848518) Conflicts : 349464 (Analyzed: 349461) Restarts : 3996 (Average: 87.45 Last: 171) Model-Level : 232.0 Problems : 44 (Average Length: 63.36 Splits: 0) Lemmas : 349461 (Deleted: 325382) Binary : 7126 (Ratio: 2.04%) Ternary : 1707 (Ratio: 0.49%) Conflict : 349461 (Average Length: 602.0 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 349461 (Average: 24.19 Max: 976 Sum: 8453195) Executed : 349363 (Average: 24.18 Max: 976 Sum: 8448882 Ratio: 99.95%) Bounded : 98 (Average: 44.01 Max: 102 Sum: 4313 Ratio: 0.05%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 731092 (Eliminated: 0 Frozen: 225701) Constraints : 5352748 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 880MB Max. Length : 100 steps Models : 1 [endof: stats after solve call] Solving Time: 7.40s Memory: 796MB (+0MB) UNKNOWN Iteration Time: 7.45s 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,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,0,True), (22,110,0,True), (23,115,0,True)] Grounded Until: 100 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 45 Time : 340.901s (Solving: 317.71s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 340.868s Choices : 9186967 (Domain: 8978634) Conflicts : 357687 (Analyzed: 357684) Restarts : 4096 (Average: 87.33 Last: 171) Model-Level : 232.0 Problems : 45 (Average Length: 64.22 Splits: 0) Lemmas : 357684 (Deleted: 333183) Binary : 7178 (Ratio: 2.01%) Ternary : 1714 (Ratio: 0.48%) Conflict : 357684 (Average Length: 592.7 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 357684 (Average: 23.98 Max: 976 Sum: 8575597) Executed : 357586 (Average: 23.96 Max: 976 Sum: 8571284 Ratio: 99.95%) Bounded : 98 (Average: 44.01 Max: 102 Sum: 4313 Ratio: 0.05%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 731092 (Eliminated: 0 Frozen: 225701) Constraints : 5352722 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 880MB Max. Length : 100 steps Models : 1 [endof: stats after solve call] Solving Time: 7.23s Memory: 796MB (+0MB) UNKNOWN Iteration Time: 7.30s 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,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,0,True), (22,110,0,True), (23,115,0,True)] Grounded Until: 100 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 46 Time : 348.726s (Solving: 325.35s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 348.696s Choices : 9343737 (Domain: 9133438) Conflicts : 365581 (Analyzed: 365578) Restarts : 4196 (Average: 87.13 Last: 171) Model-Level : 232.0 Problems : 46 (Average Length: 65.04 Splits: 0) Lemmas : 365578 (Deleted: 341177) Binary : 7228 (Ratio: 1.98%) Ternary : 1721 (Ratio: 0.47%) Conflict : 365578 (Average Length: 585.0 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 365578 (Average: 23.86 Max: 976 Sum: 8721816) Executed : 365479 (Average: 23.85 Max: 976 Sum: 8717401 Ratio: 99.95%) Bounded : 99 (Average: 44.60 Max: 102 Sum: 4415 Ratio: 0.05%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 731092 (Eliminated: 0 Frozen: 225701) Constraints : 5352722 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 880MB Max. Length : 100 steps Models : 1 [endof: stats after solve call] Solving Time: 7.76s Memory: 796MB (+0MB) UNKNOWN Iteration Time: 7.83s 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,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,0,True), (22,110,0,True), (23,115,0,True)] Grounded Until: 100 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 47 Time : 355.707s (Solving: 332.16s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 355.680s Choices : 9427166 (Domain: 9216582) Conflicts : 373489 (Analyzed: 373486) Restarts : 4296 (Average: 86.94 Last: 171) Model-Level : 232.0 Problems : 47 (Average Length: 65.83 Splits: 0) Lemmas : 373486 (Deleted: 348809) Binary : 7263 (Ratio: 1.94%) Ternary : 1733 (Ratio: 0.46%) Conflict : 373486 (Average Length: 577.1 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 373486 (Average: 23.55 Max: 976 Sum: 8796662) Executed : 373386 (Average: 23.54 Max: 976 Sum: 8792150 Ratio: 99.95%) Bounded : 100 (Average: 45.12 Max: 102 Sum: 4512 Ratio: 0.05%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 731092 (Eliminated: 0 Frozen: 225701) Constraints : 5352708 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 880MB Max. Length : 100 steps Models : 1 [endof: stats after solve call] Solving Time: 6.92s Memory: 796MB (+0MB) UNKNOWN Iteration Time: 6.99s 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,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,0,True), (22,110,0,True), (23,115,0,True)] Grounded Until: 100 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 48 Time : 362.947s (Solving: 339.25s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 362.924s Choices : 9586802 (Domain: 9374669) Conflicts : 381596 (Analyzed: 381593) Restarts : 4396 (Average: 86.80 Last: 171) Model-Level : 232.0 Problems : 48 (Average Length: 66.58 Splits: 0) Lemmas : 381593 (Deleted: 356383) Binary : 7368 (Ratio: 1.93%) Ternary : 1762 (Ratio: 0.46%) Conflict : 381593 (Average Length: 569.0 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 381593 (Average: 23.44 Max: 976 Sum: 8945143) Executed : 381492 (Average: 23.43 Max: 976 Sum: 8940534 Ratio: 99.95%) Bounded : 101 (Average: 45.63 Max: 102 Sum: 4609 Ratio: 0.05%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 731092 (Eliminated: 0 Frozen: 225701) Constraints : 5352708 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 880MB Max. Length : 100 steps Models : 1 [endof: stats after solve call] Solving Time: 7.19s Memory: 796MB (+0MB) UNKNOWN Iteration Time: 7.25s 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,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,0,True), (22,110,0,True), (23,115,0,True)] Grounded Until: 100 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 49 Time : 369.737s (Solving: 345.90s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 369.716s Choices : 9713904 (Domain: 9500881) Conflicts : 389120 (Analyzed: 389117) Restarts : 4496 (Average: 86.55 Last: 171) Model-Level : 232.0 Problems : 49 (Average Length: 67.31 Splits: 0) Lemmas : 389117 (Deleted: 364193) Binary : 7472 (Ratio: 1.92%) Ternary : 1770 (Ratio: 0.45%) Conflict : 389117 (Average Length: 562.5 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 389117 (Average: 23.29 Max: 976 Sum: 9061016) Executed : 389014 (Average: 23.27 Max: 976 Sum: 9056208 Ratio: 99.95%) Bounded : 103 (Average: 46.68 Max: 102 Sum: 4808 Ratio: 0.05%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 731092 (Eliminated: 0 Frozen: 225701) Constraints : 5352708 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 880MB Max. Length : 100 steps Models : 1 [endof: stats after solve call] Solving Time: 6.75s Memory: 796MB (+0MB) UNKNOWN Iteration Time: 6.80s Iteration 49 Queue: [(13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,0,True), (22,110,0,True), (23,115,0,True)] Grounded Until: 100 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 50 Time : 377.489s (Solving: 353.49s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 377.472s Choices : 9909629 (Domain: 9693884) Conflicts : 397372 (Analyzed: 397369) Restarts : 4596 (Average: 86.46 Last: 171) Model-Level : 232.0 Problems : 50 (Average Length: 68.00 Splits: 0) Lemmas : 397369 (Deleted: 371429) Binary : 7533 (Ratio: 1.90%) Ternary : 1790 (Ratio: 0.45%) Conflict : 397369 (Average Length: 555.6 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 397369 (Average: 23.25 Max: 976 Sum: 9238811) Executed : 397266 (Average: 23.24 Max: 976 Sum: 9234003 Ratio: 99.95%) Bounded : 103 (Average: 46.68 Max: 102 Sum: 4808 Ratio: 0.05%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 731092 (Eliminated: 0 Frozen: 225701) Constraints : 5352694 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 880MB Max. Length : 100 steps Models : 1 [endof: stats after solve call] Solving Time: 7.70s Memory: 796MB (+0MB) UNKNOWN Iteration Time: 7.76s Iteration 50 Queue: [(17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,0,True), (22,110,0,True), (23,115,0,True)] Grounded Until: 100 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 51 Time : 386.707s (Solving: 362.55s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 386.692s Choices : 10247994 (Domain: 10029074) Conflicts : 406075 (Analyzed: 406072) Restarts : 4696 (Average: 86.47 Last: 171) Model-Level : 232.0 Problems : 51 (Average Length: 68.67 Splits: 0) Lemmas : 406072 (Deleted: 381556) Binary : 7597 (Ratio: 1.87%) Ternary : 1803 (Ratio: 0.44%) Conflict : 406072 (Average Length: 548.5 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 406072 (Average: 23.54 Max: 1125 Sum: 9557408) Executed : 405967 (Average: 23.52 Max: 1125 Sum: 9552396 Ratio: 99.95%) Bounded : 105 (Average: 47.73 Max: 102 Sum: 5012 Ratio: 0.05%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 731092 (Eliminated: 0 Frozen: 225701) Constraints : 5352694 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 880MB Max. Length : 100 steps Models : 1 [endof: stats after solve call] Solving Time: 9.16s Memory: 796MB (+0MB) UNKNOWN Iteration Time: 9.22s Iteration 51 Queue: [(18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,0,True), (22,110,0,True), (23,115,0,True)] Grounded Until: 100 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 52 Time : 395.291s (Solving: 370.96s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 395.280s Choices : 10468451 (Domain: 10248704) Conflicts : 414573 (Analyzed: 414570) Restarts : 4796 (Average: 86.44 Last: 171) Model-Level : 232.0 Problems : 52 (Average Length: 69.31 Splits: 0) Lemmas : 414570 (Deleted: 387835) Binary : 7631 (Ratio: 1.84%) Ternary : 1818 (Ratio: 0.44%) Conflict : 414570 (Average Length: 541.9 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 414570 (Average: 23.55 Max: 1125 Sum: 9761448) Executed : 414465 (Average: 23.53 Max: 1125 Sum: 9756436 Ratio: 99.95%) Bounded : 105 (Average: 47.73 Max: 102 Sum: 5012 Ratio: 0.05%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 731092 (Eliminated: 0 Frozen: 225701) Constraints : 5352654 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 880MB Max. Length : 100 steps Models : 1 [endof: stats after solve call] Solving Time: 8.53s Memory: 796MB (+0MB) UNKNOWN Iteration Time: 8.59s Iteration 52 Queue: [(19,95,1,True), (20,100,1,True), (21,105,0,True), (22,110,0,True), (23,115,0,True)] Grounded Until: 100 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 53 Time : 402.682s (Solving: 378.21s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 402.676s Choices : 10655507 (Domain: 10435367) Conflicts : 422518 (Analyzed: 422515) Restarts : 4896 (Average: 86.30 Last: 171) Model-Level : 232.0 Problems : 53 (Average Length: 69.92 Splits: 0) Lemmas : 422515 (Deleted: 396161) Binary : 7676 (Ratio: 1.82%) Ternary : 1827 (Ratio: 0.43%) Conflict : 422515 (Average Length: 536.1 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 422515 (Average: 23.51 Max: 1125 Sum: 9933522) Executed : 422409 (Average: 23.50 Max: 1125 Sum: 9928413 Ratio: 99.95%) Bounded : 106 (Average: 48.20 Max: 102 Sum: 5109 Ratio: 0.05%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 731092 (Eliminated: 0 Frozen: 225701) Constraints : 5352654 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 880MB Max. Length : 100 steps Models : 1 [endof: stats after solve call] Solving Time: 7.35s Memory: 796MB (+0MB) UNKNOWN Iteration Time: 7.40s Iteration 53 Queue: [(20,100,1,True), (21,105,0,True), (22,110,0,True), (23,115,0,True)] Grounded Until: 100 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 54 Time : 411.744s (Solving: 387.10s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 411.740s Choices : 10904706 (Domain: 10683252) Conflicts : 430740 (Analyzed: 430737) Restarts : 4996 (Average: 86.22 Last: 171) Model-Level : 232.0 Problems : 54 (Average Length: 70.52 Splits: 0) Lemmas : 430737 (Deleted: 403890) Binary : 7708 (Ratio: 1.79%) Ternary : 1839 (Ratio: 0.43%) Conflict : 430737 (Average Length: 530.0 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 430737 (Average: 23.61 Max: 1255 Sum: 10167548) Executed : 430629 (Average: 23.59 Max: 1255 Sum: 10162235 Ratio: 99.95%) Bounded : 108 (Average: 49.19 Max: 102 Sum: 5313 Ratio: 0.05%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 731092 (Eliminated: 0 Frozen: 225701) Constraints : 5352654 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 880MB Max. Length : 100 steps Models : 1 [endof: stats after solve call] Solving Time: 9.00s Memory: 796MB (+0MB) UNKNOWN Iteration Time: 9.07s Iteration 54 Queue: [(21,105,0,True), (22,110,0,True), (23,115,0,True)] Grounded Until: 100 Expected Memory: 876.0MB Grounding... [('step', [101]), ('step', [102]), ('step', [103]), ('step', [104]), ('step', [105]), ('check', [105])] Grounding Time: 0.52s Memory: 796MB (+0MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 55 Time : 423.335s (Solving: 397.54s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 423.336s Choices : 11691607 (Domain: 11464606) Conflicts : 439636 (Analyzed: 439633) Restarts : 5096 (Average: 86.27 Last: 171) Model-Level : 232.0 Problems : 55 (Average Length: 71.18 Splits: 0) Lemmas : 439633 (Deleted: 415679) Binary : 7765 (Ratio: 1.77%) Ternary : 1842 (Ratio: 0.42%) Conflict : 439633 (Average Length: 532.2 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 439633 (Average: 24.84 Max: 1255 Sum: 10920793) Executed : 439525 (Average: 24.83 Max: 1255 Sum: 10915480 Ratio: 99.95%) Bounded : 108 (Average: 49.19 Max: 102 Sum: 5313 Ratio: 0.05%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 768583 (Eliminated: 0 Frozen: 237361) Constraints : 5635087 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 891MB Max. Length : 100 steps Models : 1 [endof: stats after solve call] Solving Time: 10.58s Memory: 805MB (+9MB) UNKNOWN Iteration Time: 11.60s Iteration 55 Queue: [(22,110,0,True), (23,115,0,True)] Grounded Until: 105 Expected Memory: 885.0MB Grounding... [('step', [106]), ('step', [107]), ('step', [108]), ('step', [109]), ('step', [110]), ('check', [110])] Grounding Time: 0.52s Memory: 811MB (+6MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 56 Time : 436.034s (Solving: 409.08s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 436.040s Choices : 12226711 (Domain: 11996210) Conflicts : 448542 (Analyzed: 448539) Restarts : 5196 (Average: 86.32 Last: 171) Model-Level : 232.0 Problems : 56 (Average Length: 71.91 Splits: 0) Lemmas : 448539 (Deleted: 424246) Binary : 7795 (Ratio: 1.74%) Ternary : 1842 (Ratio: 0.41%) Conflict : 448539 (Average Length: 539.8 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 448539 (Average: 25.46 Max: 1255 Sum: 11418465) Executed : 448431 (Average: 25.45 Max: 1255 Sum: 11413152 Ratio: 99.95%) Bounded : 108 (Average: 49.19 Max: 102 Sum: 5313 Ratio: 0.05%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 806074 (Eliminated: 0 Frozen: 249021) Constraints : 5917547 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 925MB Max. Length : 105 steps Models : 1 [endof: stats after solve call] Solving Time: 11.69s Memory: 831MB (+20MB) UNKNOWN Iteration Time: 12.71s Iteration 56 Queue: [(23,115,0,True)] Grounded Until: 110 Expected Memory: 911.0MB Grounding... [('step', [111]), ('step', [112]), ('step', [113]), ('step', [114]), ('step', [115]), ('check', [115])] Grounding Time: 0.52s Memory: 831MB (+0MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 57 Time : 448.553s (Solving: 420.41s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 448.564s Choices : 12777819 (Domain: 12543726) Conflicts : 456698 (Analyzed: 456695) Restarts : 5296 (Average: 86.23 Last: 171) Model-Level : 232.0 Problems : 57 (Average Length: 72.70 Splits: 0) Lemmas : 456695 (Deleted: 431287) Binary : 7812 (Ratio: 1.71%) Ternary : 1844 (Ratio: 0.40%) Conflict : 456695 (Average Length: 551.1 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 456695 (Average: 26.12 Max: 1255 Sum: 11930574) Executed : 456587 (Average: 26.11 Max: 1255 Sum: 11925261 Ratio: 99.96%) Bounded : 108 (Average: 49.19 Max: 102 Sum: 5313 Ratio: 0.04%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 843565 (Eliminated: 0 Frozen: 260681) Constraints : 6200007 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 954MB Max. Length : 110 steps Models : 1 [endof: stats after solve call] Solving Time: 11.49s Memory: 855MB (+24MB) UNKNOWN Iteration Time: 12.53s Iteration 57 Queue: [(4,20,4,True), (5,25,4,True), (6,30,4,True), (7,35,3,True), (8,40,3,True), (9,45,3,True), (10,50,3,True), (11,55,3,False), (12,60,3,False), (13,65,3,False), (14,70,2,True), (15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,1,True), (22,110,1,True), (23,115,1,True)] Grounded Until: 115 Blocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 58 Time : 454.666s (Solving: 426.36s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 454.680s Choices : 12837631 (Domain: 12602369) Conflicts : 464801 (Analyzed: 464798) Restarts : 5396 (Average: 86.14 Last: 171) Model-Level : 232.0 Problems : 58 (Average Length: 73.47 Splits: 0) Lemmas : 464798 (Deleted: 437188) Binary : 7850 (Ratio: 1.69%) Ternary : 1848 (Ratio: 0.40%) Conflict : 464798 (Average Length: 544.8 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 464798 (Average: 25.78 Max: 1255 Sum: 11982730) Executed : 464690 (Average: 25.77 Max: 1255 Sum: 11977417 Ratio: 99.96%) Bounded : 108 (Average: 49.19 Max: 102 Sum: 5313 Ratio: 0.04%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 843565 (Eliminated: 0 Frozen: 260681) Constraints : 6200007 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 954MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 6.06s Memory: 864MB (+9MB) UNKNOWN Iteration Time: 6.12s Iteration 58 Queue: [(5,25,4,True), (6,30,4,True), (7,35,3,True), (8,40,3,True), (9,45,3,True), (10,50,3,True), (11,55,3,False), (12,60,3,False), (13,65,3,False), (14,70,2,True), (15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,1,True), (22,110,1,True), (23,115,1,True)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 59 Time : 459.614s (Solving: 431.11s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 459.632s Choices : 12889429 (Domain: 12653674) Conflicts : 472760 (Analyzed: 472757) Restarts : 5496 (Average: 86.02 Last: 171) Model-Level : 232.0 Problems : 59 (Average Length: 74.20 Splits: 0) Lemmas : 472757 (Deleted: 445115) Binary : 7873 (Ratio: 1.67%) Ternary : 1862 (Ratio: 0.39%) Conflict : 472757 (Average Length: 539.1 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 472757 (Average: 25.44 Max: 1255 Sum: 12027384) Executed : 472648 (Average: 25.43 Max: 1255 Sum: 12021954 Ratio: 99.95%) Bounded : 109 (Average: 49.82 Max: 117 Sum: 5430 Ratio: 0.05%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 843565 (Eliminated: 0 Frozen: 260681) Constraints : 6200007 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 954MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 4.88s Memory: 864MB (+0MB) UNKNOWN Iteration Time: 4.95s Iteration 59 Queue: [(6,30,4,True), (7,35,3,True), (8,40,3,True), (9,45,3,True), (10,50,3,True), (11,55,3,False), (12,60,3,False), (13,65,3,False), (14,70,2,True), (15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,1,True), (22,110,1,True), (23,115,1,True)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 60 Time : 465.895s (Solving: 437.23s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 465.916s Choices : 12967705 (Domain: 12730950) Conflicts : 480690 (Analyzed: 480687) Restarts : 5596 (Average: 85.90 Last: 171) Model-Level : 232.0 Problems : 60 (Average Length: 74.92 Splits: 0) Lemmas : 480687 (Deleted: 452891) Binary : 7896 (Ratio: 1.64%) Ternary : 1870 (Ratio: 0.39%) Conflict : 480687 (Average Length: 533.5 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 480687 (Average: 25.17 Max: 1255 Sum: 12098432) Executed : 480576 (Average: 25.16 Max: 1255 Sum: 12092768 Ratio: 99.95%) Bounded : 111 (Average: 51.03 Max: 117 Sum: 5664 Ratio: 0.05%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 843565 (Eliminated: 0 Frozen: 260681) Constraints : 6199981 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 954MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 6.23s Memory: 864MB (+0MB) UNKNOWN Iteration Time: 6.29s Iteration 60 Queue: [(7,35,3,True), (8,40,3,True), (9,45,3,True), (10,50,3,True), (11,55,3,False), (12,60,3,False), (13,65,3,False), (14,70,2,True), (15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,1,True), (22,110,1,True), (23,115,1,True)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 61 Time : 472.239s (Solving: 443.39s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 472.260s Choices : 13061292 (Domain: 12823535) Conflicts : 489048 (Analyzed: 489045) Restarts : 5696 (Average: 85.86 Last: 171) Model-Level : 232.0 Problems : 61 (Average Length: 75.61 Splits: 0) Lemmas : 489045 (Deleted: 460661) Binary : 7926 (Ratio: 1.62%) Ternary : 1876 (Ratio: 0.38%) Conflict : 489045 (Average Length: 528.1 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 489045 (Average: 24.91 Max: 1255 Sum: 12183637) Executed : 488934 (Average: 24.90 Max: 1255 Sum: 12177973 Ratio: 99.95%) Bounded : 111 (Average: 51.03 Max: 117 Sum: 5664 Ratio: 0.05%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 843565 (Eliminated: 0 Frozen: 260681) Constraints : 6199953 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 954MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 6.28s Memory: 864MB (+0MB) UNKNOWN Iteration Time: 6.35s Iteration 61 Queue: [(8,40,3,True), (9,45,3,True), (10,50,3,True), (11,55,3,False), (12,60,3,False), (13,65,3,False), (14,70,2,True), (15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,1,True), (22,110,1,True), (23,115,1,True)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 62 Time : 479.138s (Solving: 450.13s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 479.164s Choices : 13173458 (Domain: 12934492) Conflicts : 497517 (Analyzed: 497514) Restarts : 5796 (Average: 85.84 Last: 171) Model-Level : 232.0 Problems : 62 (Average Length: 76.27 Splits: 0) Lemmas : 497514 (Deleted: 468817) Binary : 7948 (Ratio: 1.60%) Ternary : 1885 (Ratio: 0.38%) Conflict : 497514 (Average Length: 523.0 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 497514 (Average: 24.69 Max: 1255 Sum: 12284824) Executed : 497403 (Average: 24.68 Max: 1255 Sum: 12279160 Ratio: 99.95%) Bounded : 111 (Average: 51.03 Max: 117 Sum: 5664 Ratio: 0.05%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 843565 (Eliminated: 0 Frozen: 260681) Constraints : 6199953 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 954MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 6.85s Memory: 864MB (+0MB) UNKNOWN Iteration Time: 6.90s Iteration 62 Queue: [(9,45,3,True), (10,50,3,True), (11,55,3,False), (12,60,3,False), (13,65,3,False), (14,70,2,True), (15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,1,True), (22,110,1,True), (23,115,1,True)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 63 Time : 485.927s (Solving: 456.73s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 485.956s Choices : 13300298 (Domain: 13057486) Conflicts : 506050 (Analyzed: 506047) Restarts : 5896 (Average: 85.83 Last: 171) Model-Level : 232.0 Problems : 63 (Average Length: 76.92 Splits: 0) Lemmas : 506047 (Deleted: 477031) Binary : 7986 (Ratio: 1.58%) Ternary : 1894 (Ratio: 0.37%) Conflict : 506047 (Average Length: 518.8 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 506047 (Average: 24.50 Max: 1255 Sum: 12398827) Executed : 505935 (Average: 24.49 Max: 1255 Sum: 12393046 Ratio: 99.95%) Bounded : 112 (Average: 51.62 Max: 117 Sum: 5781 Ratio: 0.05%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 843565 (Eliminated: 0 Frozen: 260681) Constraints : 6199953 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 954MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 6.72s Memory: 864MB (+0MB) UNKNOWN Iteration Time: 6.79s Iteration 63 Queue: [(10,50,3,True), (11,55,3,False), (12,60,3,False), (13,65,3,False), (14,70,2,True), (15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,1,True), (22,110,1,True), (23,115,1,True)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 64 Time : 493.510s (Solving: 464.14s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 493.540s Choices : 13421584 (Domain: 13177905) Conflicts : 514137 (Analyzed: 514134) Restarts : 5996 (Average: 85.75 Last: 171) Model-Level : 232.0 Problems : 64 (Average Length: 77.55 Splits: 0) Lemmas : 514134 (Deleted: 485398) Binary : 8014 (Ratio: 1.56%) Ternary : 1902 (Ratio: 0.37%) Conflict : 514134 (Average Length: 514.0 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 514134 (Average: 24.33 Max: 1255 Sum: 12508768) Executed : 514021 (Average: 24.32 Max: 1255 Sum: 12502870 Ratio: 99.95%) Bounded : 113 (Average: 52.19 Max: 117 Sum: 5898 Ratio: 0.05%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 843565 (Eliminated: 0 Frozen: 260681) Constraints : 6199939 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 954MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 7.53s Memory: 864MB (+0MB) UNKNOWN Iteration Time: 7.59s Iteration 64 Queue: [(14,70,2,True), (15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,1,True), (22,110,1,True), (23,115,1,True)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 65 Time : 501.235s (Solving: 471.70s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 501.268s Choices : 13608120 (Domain: 13363769) Conflicts : 522146 (Analyzed: 522143) Restarts : 6096 (Average: 85.65 Last: 171) Model-Level : 232.0 Problems : 65 (Average Length: 78.15 Splits: 0) Lemmas : 522143 (Deleted: 493183) Binary : 8127 (Ratio: 1.56%) Ternary : 1939 (Ratio: 0.37%) Conflict : 522143 (Average Length: 509.3 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 522143 (Average: 24.29 Max: 1255 Sum: 12682648) Executed : 522028 (Average: 24.28 Max: 1255 Sum: 12676526 Ratio: 99.95%) Bounded : 115 (Average: 53.23 Max: 117 Sum: 6122 Ratio: 0.05%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 843565 (Eliminated: 0 Frozen: 260681) Constraints : 6199925 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 954MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 7.67s Memory: 864MB (+0MB) UNKNOWN Iteration Time: 7.73s Iteration 65 Queue: [(15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,1,True), (22,110,1,True), (23,115,1,True)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 66 Time : 510.193s (Solving: 480.49s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 510.228s Choices : 13859353 (Domain: 13613977) Conflicts : 530618 (Analyzed: 530615) Restarts : 6196 (Average: 85.64 Last: 171) Model-Level : 232.0 Problems : 66 (Average Length: 78.74 Splits: 0) Lemmas : 530615 (Deleted: 500870) Binary : 8147 (Ratio: 1.54%) Ternary : 1955 (Ratio: 0.37%) Conflict : 530615 (Average Length: 504.5 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 530615 (Average: 24.35 Max: 1255 Sum: 12919187) Executed : 530500 (Average: 24.34 Max: 1255 Sum: 12913065 Ratio: 99.95%) Bounded : 115 (Average: 53.23 Max: 117 Sum: 6122 Ratio: 0.05%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 843565 (Eliminated: 0 Frozen: 260681) Constraints : 6199925 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 954MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 8.90s Memory: 864MB (+0MB) UNKNOWN Iteration Time: 8.96s Iteration 66 Queue: [(21,105,1,True), (22,110,1,True), (23,115,1,True)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 67 Time : 518.956s (Solving: 489.08s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 518.996s Choices : 14022844 (Domain: 13777305) Conflicts : 538772 (Analyzed: 538769) Restarts : 6296 (Average: 85.57 Last: 171) Model-Level : 232.0 Problems : 67 (Average Length: 79.31 Splits: 0) Lemmas : 538769 (Deleted: 509149) Binary : 8176 (Ratio: 1.52%) Ternary : 1966 (Ratio: 0.36%) Conflict : 538769 (Average Length: 500.5 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 538769 (Average: 24.25 Max: 1255 Sum: 13066793) Executed : 538654 (Average: 24.24 Max: 1255 Sum: 13060671 Ratio: 99.95%) Bounded : 115 (Average: 53.23 Max: 117 Sum: 6122 Ratio: 0.05%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 843565 (Eliminated: 0 Frozen: 260681) Constraints : 6199925 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 954MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 8.71s Memory: 864MB (+0MB) UNKNOWN Iteration Time: 8.77s Iteration 67 Queue: [(22,110,1,True), (23,115,1,True)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 68 Time : 528.763s (Solving: 498.72s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 528.804s Choices : 14246213 (Domain: 14000272) Conflicts : 547115 (Analyzed: 547112) Restarts : 6396 (Average: 85.54 Last: 171) Model-Level : 232.0 Problems : 68 (Average Length: 79.87 Splits: 0) Lemmas : 547112 (Deleted: 517088) Binary : 8199 (Ratio: 1.50%) Ternary : 1972 (Ratio: 0.36%) Conflict : 547112 (Average Length: 496.6 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 547112 (Average: 24.26 Max: 1255 Sum: 13273255) Executed : 546995 (Average: 24.25 Max: 1255 Sum: 13266899 Ratio: 99.95%) Bounded : 117 (Average: 54.32 Max: 117 Sum: 6356 Ratio: 0.05%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 843565 (Eliminated: 0 Frozen: 260681) Constraints : 6199925 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 954MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 9.76s Memory: 864MB (+0MB) UNKNOWN Iteration Time: 9.81s Iteration 68 Queue: [(23,115,1,True)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 69 Time : 536.753s (Solving: 506.52s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 536.796s Choices : 14430681 (Domain: 14183957) Conflicts : 555430 (Analyzed: 555427) Restarts : 6496 (Average: 85.50 Last: 171) Model-Level : 232.0 Problems : 69 (Average Length: 80.41 Splits: 0) Lemmas : 555427 (Deleted: 525178) Binary : 8268 (Ratio: 1.49%) Ternary : 1992 (Ratio: 0.36%) Conflict : 555427 (Average Length: 492.3 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 555427 (Average: 24.20 Max: 1255 Sum: 13440856) Executed : 555307 (Average: 24.19 Max: 1255 Sum: 13434154 Ratio: 99.95%) Bounded : 120 (Average: 55.85 Max: 117 Sum: 6702 Ratio: 0.05%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 843565 (Eliminated: 0 Frozen: 260681) Constraints : 6199897 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 954MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 7.92s Memory: 864MB (+0MB) UNKNOWN Iteration Time: 7.99s Iteration 69 Queue: [(4,20,5,True), (5,25,5,True), (6,30,5,True), (7,35,4,True), (8,40,4,True), (9,45,4,True), (10,50,4,False), (11,55,3,True), (12,60,3,True), (13,65,3,False), (14,70,3,False), (15,75,3,False), (16,80,2,True), (17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] Grounded Until: 115 Blocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 70 Time : 542.749s (Solving: 512.35s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 542.796s Choices : 14476363 (Domain: 14229056) Conflicts : 563997 (Analyzed: 563994) Restarts : 6596 (Average: 85.51 Last: 171) Model-Level : 232.0 Problems : 70 (Average Length: 80.93 Splits: 0) Lemmas : 563994 (Deleted: 533282) Binary : 8326 (Ratio: 1.48%) Ternary : 2004 (Ratio: 0.36%) Conflict : 563994 (Average Length: 488.9 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 563994 (Average: 23.90 Max: 1255 Sum: 13480190) Executed : 563872 (Average: 23.89 Max: 1255 Sum: 13473255 Ratio: 99.95%) Bounded : 122 (Average: 56.84 Max: 117 Sum: 6935 Ratio: 0.05%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 843565 (Eliminated: 0 Frozen: 260681) Constraints : 6199869 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 954MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 5.94s Memory: 864MB (+0MB) UNKNOWN Iteration Time: 6.00s Iteration 70 Queue: [(5,25,5,True), (6,30,5,True), (7,35,4,True), (8,40,4,True), (9,45,4,True), (10,50,4,False), (11,55,3,True), (12,60,3,True), (13,65,3,False), (14,70,3,False), (15,75,3,False), (16,80,2,True), (17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 71 Time : 548.770s (Solving: 518.18s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 548.820s Choices : 14543972 (Domain: 14296189) Conflicts : 572433 (Analyzed: 572430) Restarts : 6696 (Average: 85.49 Last: 171) Model-Level : 232.0 Problems : 71 (Average Length: 81.44 Splits: 0) Lemmas : 572430 (Deleted: 541649) Binary : 8412 (Ratio: 1.47%) Ternary : 2034 (Ratio: 0.36%) Conflict : 572430 (Average Length: 485.2 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 572430 (Average: 23.65 Max: 1255 Sum: 13539606) Executed : 572308 (Average: 23.64 Max: 1255 Sum: 13532671 Ratio: 99.95%) Bounded : 122 (Average: 56.84 Max: 117 Sum: 6935 Ratio: 0.05%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 843565 (Eliminated: 0 Frozen: 260681) Constraints : 6199851 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 954MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 5.95s Memory: 864MB (+0MB) UNKNOWN Iteration Time: 6.03s Iteration 71 Queue: [(6,30,5,True), (7,35,4,True), (8,40,4,True), (9,45,4,True), (10,50,4,False), (11,55,3,True), (12,60,3,True), (13,65,3,False), (14,70,3,False), (15,75,3,False), (16,80,2,True), (17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 72 Time : 554.809s (Solving: 524.05s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 554.864s Choices : 14603441 (Domain: 14355082) Conflicts : 580793 (Analyzed: 580790) Restarts : 6796 (Average: 85.46 Last: 171) Model-Level : 232.0 Problems : 72 (Average Length: 81.93 Splits: 0) Lemmas : 580790 (Deleted: 549752) Binary : 8433 (Ratio: 1.45%) Ternary : 2046 (Ratio: 0.35%) Conflict : 580790 (Average Length: 481.3 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 580790 (Average: 23.40 Max: 1255 Sum: 13591492) Executed : 580666 (Average: 23.39 Max: 1255 Sum: 13584323 Ratio: 99.95%) Bounded : 124 (Average: 57.81 Max: 117 Sum: 7169 Ratio: 0.05%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 843565 (Eliminated: 0 Frozen: 260681) Constraints : 6199851 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 954MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 5.98s Memory: 864MB (+0MB) UNKNOWN Iteration Time: 6.05s Iteration 72 Queue: [(7,35,4,True), (8,40,4,True), (9,45,4,True), (10,50,4,False), (11,55,3,True), (12,60,3,True), (13,65,3,False), (14,70,3,False), (15,75,3,False), (16,80,2,True), (17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 73 Time : 560.984s (Solving: 530.04s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 561.040s Choices : 14648334 (Domain: 14399718) Conflicts : 588764 (Analyzed: 588761) Restarts : 6896 (Average: 85.38 Last: 171) Model-Level : 232.0 Problems : 73 (Average Length: 82.41 Splits: 0) Lemmas : 588761 (Deleted: 557942) Binary : 8451 (Ratio: 1.44%) Ternary : 2055 (Ratio: 0.35%) Conflict : 588761 (Average Length: 477.8 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 588761 (Average: 23.15 Max: 1255 Sum: 13628719) Executed : 588636 (Average: 23.14 Max: 1255 Sum: 13621433 Ratio: 99.95%) Bounded : 125 (Average: 58.29 Max: 117 Sum: 7286 Ratio: 0.05%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 843565 (Eliminated: 0 Frozen: 260681) Constraints : 6199811 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 954MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 6.11s Memory: 864MB (+0MB) UNKNOWN Iteration Time: 6.18s Iteration 73 Queue: [(8,40,4,True), (9,45,4,True), (10,50,4,False), (11,55,3,True), (12,60,3,True), (13,65,3,False), (14,70,3,False), (15,75,3,False), (16,80,2,True), (17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 74 Time : 568.288s (Solving: 537.16s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 568.344s Choices : 14766229 (Domain: 14514654) Conflicts : 597013 (Analyzed: 597010) Restarts : 6996 (Average: 85.34 Last: 171) Model-Level : 232.0 Problems : 74 (Average Length: 82.88 Splits: 0) Lemmas : 597010 (Deleted: 565679) Binary : 8486 (Ratio: 1.42%) Ternary : 2094 (Ratio: 0.35%) Conflict : 597010 (Average Length: 474.5 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 597010 (Average: 23.01 Max: 1255 Sum: 13735053) Executed : 596885 (Average: 22.99 Max: 1255 Sum: 13727767 Ratio: 99.95%) Bounded : 125 (Average: 58.29 Max: 117 Sum: 7286 Ratio: 0.05%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 843565 (Eliminated: 0 Frozen: 260681) Constraints : 6199798 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 954MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 7.24s Memory: 864MB (+0MB) UNKNOWN Iteration Time: 7.31s Iteration 74 Queue: [(9,45,4,True), (10,50,4,False), (11,55,3,True), (12,60,3,True), (13,65,3,False), (14,70,3,False), (15,75,3,False), (16,80,2,True), (17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 75 Time : 575.591s (Solving: 544.28s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 575.648s Choices : 14857657 (Domain: 14605739) Conflicts : 605469 (Analyzed: 605466) Restarts : 7096 (Average: 85.32 Last: 171) Model-Level : 232.0 Problems : 75 (Average Length: 83.33 Splits: 0) Lemmas : 605466 (Deleted: 573690) Binary : 8514 (Ratio: 1.41%) Ternary : 2099 (Ratio: 0.35%) Conflict : 605466 (Average Length: 471.1 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 605466 (Average: 22.82 Max: 1255 Sum: 13817027) Executed : 605340 (Average: 22.81 Max: 1255 Sum: 13809624 Ratio: 99.95%) Bounded : 126 (Average: 58.75 Max: 117 Sum: 7403 Ratio: 0.05%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 843565 (Eliminated: 0 Frozen: 260681) Constraints : 6199798 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 954MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 7.24s Memory: 864MB (+0MB) UNKNOWN Iteration Time: 7.31s Iteration 75 Queue: [(11,55,3,True), (12,60,3,True), (13,65,3,False), (14,70,3,False), (15,75,3,False), (16,80,2,True), (17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 76 Time : 584.071s (Solving: 552.57s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 584.132s Choices : 15009738 (Domain: 14755250) Conflicts : 614692 (Analyzed: 614689) Restarts : 7196 (Average: 85.42 Last: 171) Model-Level : 232.0 Problems : 76 (Average Length: 83.78 Splits: 0) Lemmas : 614689 (Deleted: 583961) Binary : 8604 (Ratio: 1.40%) Ternary : 2146 (Ratio: 0.35%) Conflict : 614689 (Average Length: 468.9 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 614689 (Average: 22.69 Max: 1255 Sum: 13949496) Executed : 614561 (Average: 22.68 Max: 1255 Sum: 13941859 Ratio: 99.95%) Bounded : 128 (Average: 59.66 Max: 117 Sum: 7637 Ratio: 0.05%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 843565 (Eliminated: 0 Frozen: 260681) Constraints : 6199772 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 954MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 8.42s Memory: 864MB (+0MB) UNKNOWN Iteration Time: 8.49s Iteration 76 Queue: [(12,60,3,True), (13,65,3,False), (14,70,3,False), (15,75,3,False), (16,80,2,True), (17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 77 Time : 593.492s (Solving: 561.82s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 593.556s Choices : 15218644 (Domain: 14961012) Conflicts : 623205 (Analyzed: 623202) Restarts : 7296 (Average: 85.42 Last: 171) Model-Level : 232.0 Problems : 77 (Average Length: 84.21 Splits: 0) Lemmas : 623202 (Deleted: 590712) Binary : 8679 (Ratio: 1.39%) Ternary : 2167 (Ratio: 0.35%) Conflict : 623202 (Average Length: 467.8 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 623202 (Average: 22.68 Max: 1255 Sum: 14132954) Executed : 623071 (Average: 22.67 Max: 1255 Sum: 14124976 Ratio: 99.94%) Bounded : 131 (Average: 60.90 Max: 117 Sum: 7978 Ratio: 0.06%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 843565 (Eliminated: 0 Frozen: 260681) Constraints : 6199745 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 954MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 9.37s Memory: 864MB (+0MB) UNKNOWN Iteration Time: 9.43s Iteration 77 Queue: [(16,80,2,True), (17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 78 Time : 600.937s (Solving: 569.11s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 601.004s Choices : 15408713 (Domain: 15150060) Conflicts : 631232 (Analyzed: 631229) Restarts : 7396 (Average: 85.35 Last: 171) Model-Level : 232.0 Problems : 78 (Average Length: 84.63 Splits: 0) Lemmas : 631229 (Deleted: 598987) Binary : 8746 (Ratio: 1.39%) Ternary : 2178 (Ratio: 0.35%) Conflict : 631229 (Average Length: 465.2 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 631229 (Average: 22.66 Max: 1255 Sum: 14306296) Executed : 631098 (Average: 22.65 Max: 1255 Sum: 14298318 Ratio: 99.94%) Bounded : 131 (Average: 60.90 Max: 117 Sum: 7978 Ratio: 0.06%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 843565 (Eliminated: 0 Frozen: 260681) Constraints : 6199731 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 954MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 7.39s Memory: 864MB (+0MB) UNKNOWN Iteration Time: 7.45s Iteration 78 Queue: [(17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 79 Time : 612.785s (Solving: 580.77s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 612.860s Choices : 16008986 (Domain: 15746727) Conflicts : 640420 (Analyzed: 640417) Restarts : 7496 (Average: 85.43 Last: 171) Model-Level : 232.0 Problems : 79 (Average Length: 85.04 Splits: 0) Lemmas : 640417 (Deleted: 608932) Binary : 8888 (Ratio: 1.39%) Ternary : 2183 (Ratio: 0.34%) Conflict : 640417 (Average Length: 463.9 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 640417 (Average: 23.24 Max: 1255 Sum: 14884055) Executed : 640286 (Average: 23.23 Max: 1255 Sum: 14876077 Ratio: 99.95%) Bounded : 131 (Average: 60.90 Max: 117 Sum: 7978 Ratio: 0.05%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 843565 (Eliminated: 0 Frozen: 260681) Constraints : 6199731 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 954MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 11.79s Memory: 864MB (+0MB) UNKNOWN Iteration Time: 11.86s Iteration 79 Queue: [(4,20,6,True), (5,25,6,True), (6,30,6,True), (7,35,5,True), (8,40,5,True), (9,45,5,False), (10,50,4,True), (11,55,4,False), (12,60,4,False), (13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,3,False), (17,85,3,False), (18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] Grounded Until: 115 Blocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 80 Time : 620.247s (Solving: 588.06s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 620.324s Choices : 16048282 (Domain: 15786023) Conflicts : 648780 (Analyzed: 648777) Restarts : 7596 (Average: 85.41 Last: 171) Model-Level : 232.0 Problems : 80 (Average Length: 85.44 Splits: 0) Lemmas : 648777 (Deleted: 615663) Binary : 8909 (Ratio: 1.37%) Ternary : 2194 (Ratio: 0.34%) Conflict : 648777 (Average Length: 461.5 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 648777 (Average: 22.99 Max: 1255 Sum: 14918338) Executed : 648644 (Average: 22.98 Max: 1255 Sum: 14910136 Ratio: 99.95%) Bounded : 133 (Average: 61.67 Max: 117 Sum: 8202 Ratio: 0.05%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 843565 (Eliminated: 0 Frozen: 260681) Constraints : 6199731 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 954MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 7.40s Memory: 864MB (+0MB) UNKNOWN Iteration Time: 7.47s Iteration 80 Queue: [(5,25,6,True), (6,30,6,True), (7,35,5,True), (8,40,5,True), (9,45,5,False), (10,50,4,True), (11,55,4,False), (12,60,4,False), (13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,3,False), (17,85,3,False), (18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 81 Time : 626.545s (Solving: 594.16s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 626.624s Choices : 16137076 (Domain: 15873284) Conflicts : 656802 (Analyzed: 656799) Restarts : 7696 (Average: 85.34 Last: 171) Model-Level : 232.0 Problems : 81 (Average Length: 85.83 Splits: 0) Lemmas : 656799 (Deleted: 623811) Binary : 8968 (Ratio: 1.37%) Ternary : 2205 (Ratio: 0.34%) Conflict : 656799 (Average Length: 459.3 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 656799 (Average: 22.84 Max: 1255 Sum: 14999276) Executed : 656665 (Average: 22.82 Max: 1255 Sum: 14990957 Ratio: 99.94%) Bounded : 134 (Average: 62.08 Max: 117 Sum: 8319 Ratio: 0.06%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 843565 (Eliminated: 0 Frozen: 260681) Constraints : 6199731 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 954MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 6.22s Memory: 864MB (+0MB) UNKNOWN Iteration Time: 6.30s Iteration 81 Queue: [(6,30,6,True), (7,35,5,True), (8,40,5,True), (9,45,5,False), (10,50,4,True), (11,55,4,False), (12,60,4,False), (13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,3,False), (17,85,3,False), (18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 82 Time : 632.132s (Solving: 599.57s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 632.212s Choices : 16206027 (Domain: 15940612) Conflicts : 664955 (Analyzed: 664952) Restarts : 7796 (Average: 85.29 Last: 171) Model-Level : 232.0 Problems : 82 (Average Length: 86.21 Splits: 0) Lemmas : 664952 (Deleted: 631579) Binary : 9003 (Ratio: 1.35%) Ternary : 2210 (Ratio: 0.33%) Conflict : 664952 (Average Length: 456.4 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 664952 (Average: 22.65 Max: 1255 Sum: 15060121) Executed : 664817 (Average: 22.64 Max: 1255 Sum: 15051685 Ratio: 99.94%) Bounded : 135 (Average: 62.49 Max: 117 Sum: 8436 Ratio: 0.06%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 843565 (Eliminated: 0 Frozen: 260681) Constraints : 6199713 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 954MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 5.52s Memory: 864MB (+0MB) UNKNOWN Iteration Time: 5.59s Iteration 82 Queue: [(7,35,5,True), (8,40,5,True), (9,45,5,False), (10,50,4,True), (11,55,4,False), (12,60,4,False), (13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,3,False), (17,85,3,False), (18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 83 Time : 638.816s (Solving: 606.07s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 638.900s Choices : 16282916 (Domain: 16016607) Conflicts : 673108 (Analyzed: 673105) Restarts : 7896 (Average: 85.25 Last: 171) Model-Level : 232.0 Problems : 83 (Average Length: 86.58 Splits: 0) Lemmas : 673105 (Deleted: 639552) Binary : 9041 (Ratio: 1.34%) Ternary : 2218 (Ratio: 0.33%) Conflict : 673105 (Average Length: 453.4 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 673105 (Average: 22.48 Max: 1255 Sum: 15129881) Executed : 672969 (Average: 22.47 Max: 1255 Sum: 15121328 Ratio: 99.94%) Bounded : 136 (Average: 62.89 Max: 117 Sum: 8553 Ratio: 0.06%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 843565 (Eliminated: 0 Frozen: 260681) Constraints : 6199699 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 954MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 6.62s Memory: 864MB (+0MB) UNKNOWN Iteration Time: 6.69s Iteration 83 Queue: [(8,40,5,True), (9,45,5,False), (10,50,4,True), (11,55,4,False), (12,60,4,False), (13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,3,False), (17,85,3,False), (18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 84 Time : 645.906s (Solving: 613.00s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 645.992s Choices : 16363245 (Domain: 16094472) Conflicts : 681207 (Analyzed: 681204) Restarts : 7996 (Average: 85.19 Last: 171) Model-Level : 232.0 Problems : 84 (Average Length: 86.94 Splits: 0) Lemmas : 681204 (Deleted: 647474) Binary : 9072 (Ratio: 1.33%) Ternary : 2237 (Ratio: 0.33%) Conflict : 681204 (Average Length: 450.8 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 681204 (Average: 22.31 Max: 1255 Sum: 15200981) Executed : 681067 (Average: 22.30 Max: 1255 Sum: 15192311 Ratio: 99.94%) Bounded : 137 (Average: 63.28 Max: 117 Sum: 8670 Ratio: 0.06%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 843565 (Eliminated: 0 Frozen: 260681) Constraints : 6199686 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 954MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 7.04s Memory: 864MB (+0MB) UNKNOWN Iteration Time: 7.10s Iteration 84 Queue: [(10,50,4,True), (11,55,4,False), (12,60,4,False), (13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,3,False), (17,85,3,False), (18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 85 Time : 653.672s (Solving: 620.60s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 653.760s Choices : 16517040 (Domain: 16247104) Conflicts : 689478 (Analyzed: 689475) Restarts : 8096 (Average: 85.16 Last: 171) Model-Level : 232.0 Problems : 85 (Average Length: 87.29 Splits: 0) Lemmas : 689475 (Deleted: 655346) Binary : 9100 (Ratio: 1.32%) Ternary : 2243 (Ratio: 0.33%) Conflict : 689475 (Average Length: 448.4 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 689475 (Average: 22.25 Max: 1255 Sum: 15343975) Executed : 689337 (Average: 22.24 Max: 1255 Sum: 15335193 Ratio: 99.94%) Bounded : 138 (Average: 63.64 Max: 117 Sum: 8782 Ratio: 0.06%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 843565 (Eliminated: 0 Frozen: 260681) Constraints : 6199672 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 954MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 7.72s Memory: 864MB (+0MB) UNKNOWN Iteration Time: 7.77s Iteration 85 Queue: [(13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,3,False), (17,85,3,False), (18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 86 Time : 661.244s (Solving: 627.99s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 661.336s Choices : 16663361 (Domain: 16393175) Conflicts : 697585 (Analyzed: 697582) Restarts : 8196 (Average: 85.11 Last: 171) Model-Level : 232.0 Problems : 86 (Average Length: 87.64 Splits: 0) Lemmas : 697582 (Deleted: 663440) Binary : 9110 (Ratio: 1.31%) Ternary : 2248 (Ratio: 0.32%) Conflict : 697582 (Average Length: 446.1 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 697582 (Average: 22.19 Max: 1255 Sum: 15478518) Executed : 697444 (Average: 22.18 Max: 1255 Sum: 15469736 Ratio: 99.94%) Bounded : 138 (Average: 63.64 Max: 117 Sum: 8782 Ratio: 0.06%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 843565 (Eliminated: 0 Frozen: 260681) Constraints : 6199672 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 954MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 7.51s Memory: 864MB (+0MB) UNKNOWN Iteration Time: 7.58s Iteration 86 Queue: [(18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 87 Time : 669.860s (Solving: 636.44s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 669.956s Choices : 16967845 (Domain: 16696168) Conflicts : 706302 (Analyzed: 706299) Restarts : 8296 (Average: 85.14 Last: 171) Model-Level : 232.0 Problems : 87 (Average Length: 87.98 Splits: 0) Lemmas : 706299 (Deleted: 673596) Binary : 9147 (Ratio: 1.30%) Ternary : 2259 (Ratio: 0.32%) Conflict : 706299 (Average Length: 443.7 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 706299 (Average: 22.32 Max: 1255 Sum: 15766043) Executed : 706161 (Average: 22.31 Max: 1255 Sum: 15757261 Ratio: 99.94%) Bounded : 138 (Average: 63.64 Max: 117 Sum: 8782 Ratio: 0.06%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 843565 (Eliminated: 0 Frozen: 260681) Constraints : 6199672 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 954MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 8.57s Memory: 864MB (+0MB) UNKNOWN Iteration Time: 8.62s Iteration 87 Queue: [(4,20,7,True), (5,25,7,True), (6,30,7,False), (7,35,6,True), (8,40,6,False), (9,45,5,True), (10,50,5,False), (11,55,4,True), (12,60,4,False), (13,65,4,False), (14,70,3,True), (15,75,3,True), (16,80,3,False), (17,85,3,False), (18,90,3,False), (19,95,2,True), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] Grounded Until: 115 Blocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 88 Time : 678.540s (Solving: 644.95s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 678.640s Choices : 17023325 (Domain: 16751648) Conflicts : 714224 (Analyzed: 714221) Restarts : 8396 (Average: 85.07 Last: 171) Model-Level : 232.0 Problems : 88 (Average Length: 88.31 Splits: 0) Lemmas : 714221 (Deleted: 680251) Binary : 9211 (Ratio: 1.29%) Ternary : 2273 (Ratio: 0.32%) Conflict : 714221 (Average Length: 447.3 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 714221 (Average: 22.14 Max: 1255 Sum: 15815875) Executed : 714081 (Average: 22.13 Max: 1255 Sum: 15807091 Ratio: 99.94%) Bounded : 140 (Average: 62.74 Max: 117 Sum: 8784 Ratio: 0.06%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 843565 (Eliminated: 0 Frozen: 260681) Constraints : 6199672 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 954MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 8.62s Memory: 864MB (+0MB) UNKNOWN Iteration Time: 8.69s Iteration 88 Queue: [(5,25,7,True), (6,30,7,False), (7,35,6,True), (8,40,6,False), (9,45,5,True), (10,50,5,False), (11,55,4,True), (12,60,4,False), (13,65,4,False), (14,70,3,True), (15,75,3,True), (16,80,3,False), (17,85,3,False), (18,90,3,False), (19,95,2,True), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 89 Time : 684.332s (Solving: 650.57s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 684.432s Choices : 17085073 (Domain: 16812824) Conflicts : 722111 (Analyzed: 722108) Restarts : 8496 (Average: 84.99 Last: 171) Model-Level : 232.0 Problems : 89 (Average Length: 88.63 Splits: 0) Lemmas : 722108 (Deleted: 687535) Binary : 9264 (Ratio: 1.28%) Ternary : 2282 (Ratio: 0.32%) Conflict : 722108 (Average Length: 445.0 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 722108 (Average: 21.98 Max: 1255 Sum: 15870681) Executed : 721967 (Average: 21.97 Max: 1255 Sum: 15861785 Ratio: 99.94%) Bounded : 141 (Average: 63.09 Max: 117 Sum: 8896 Ratio: 0.06%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 843565 (Eliminated: 0 Frozen: 260681) Constraints : 6199672 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 954MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 5.74s Memory: 864MB (+0MB) UNKNOWN Iteration Time: 5.80s Iteration 89 Queue: [(7,35,6,True), (8,40,6,False), (9,45,5,True), (10,50,5,False), (11,55,4,True), (12,60,4,False), (13,65,4,False), (14,70,3,True), (15,75,3,True), (16,80,3,False), (17,85,3,False), (18,90,3,False), (19,95,2,True), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 90 Time : 689.861s (Solving: 655.90s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 689.964s Choices : 17172619 (Domain: 16899545) Conflicts : 730083 (Analyzed: 730080) Restarts : 8596 (Average: 84.93 Last: 171) Model-Level : 232.0 Problems : 90 (Average Length: 88.94 Splits: 0) Lemmas : 730080 (Deleted: 695234) Binary : 9312 (Ratio: 1.28%) Ternary : 2295 (Ratio: 0.31%) Conflict : 730080 (Average Length: 442.7 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 730080 (Average: 21.85 Max: 1255 Sum: 15949579) Executed : 729939 (Average: 21.83 Max: 1255 Sum: 15940683 Ratio: 99.94%) Bounded : 141 (Average: 63.09 Max: 117 Sum: 8896 Ratio: 0.06%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 843565 (Eliminated: 0 Frozen: 260681) Constraints : 6199672 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 954MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 5.45s Memory: 864MB (+0MB) UNKNOWN Iteration Time: 5.53s Iteration 90 Queue: [(9,45,5,True), (10,50,5,False), (11,55,4,True), (12,60,4,False), (13,65,4,False), (14,70,3,True), (15,75,3,True), (16,80,3,False), (17,85,3,False), (18,90,3,False), (19,95,2,True), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 91 Time : 696.333s (Solving: 662.19s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 696.440s Choices : 17283931 (Domain: 17009930) Conflicts : 738257 (Analyzed: 738254) Restarts : 8696 (Average: 84.90 Last: 171) Model-Level : 232.0 Problems : 91 (Average Length: 89.25 Splits: 0) Lemmas : 738254 (Deleted: 702930) Binary : 9374 (Ratio: 1.27%) Ternary : 2313 (Ratio: 0.31%) Conflict : 738254 (Average Length: 440.7 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 738254 (Average: 21.74 Max: 1255 Sum: 16051813) Executed : 738113 (Average: 21.73 Max: 1255 Sum: 16042917 Ratio: 99.94%) Bounded : 141 (Average: 63.09 Max: 117 Sum: 8896 Ratio: 0.06%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 843565 (Eliminated: 0 Frozen: 260681) Constraints : 6199672 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 954MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 6.41s Memory: 864MB (+0MB) UNKNOWN Iteration Time: 6.48s Iteration 91 Queue: [(11,55,4,True), (12,60,4,False), (13,65,4,False), (14,70,3,True), (15,75,3,True), (16,80,3,False), (17,85,3,False), (18,90,3,False), (19,95,2,True), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 92 Time : 704.865s (Solving: 670.53s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 704.980s Choices : 17490762 (Domain: 17213696) Conflicts : 746898 (Analyzed: 746895) Restarts : 8796 (Average: 84.91 Last: 171) Model-Level : 232.0 Problems : 92 (Average Length: 89.55 Splits: 0) Lemmas : 746895 (Deleted: 713000) Binary : 9483 (Ratio: 1.27%) Ternary : 2341 (Ratio: 0.31%) Conflict : 746895 (Average Length: 439.5 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 746895 (Average: 21.75 Max: 1255 Sum: 16245810) Executed : 746753 (Average: 21.74 Max: 1255 Sum: 16236797 Ratio: 99.94%) Bounded : 142 (Average: 63.47 Max: 117 Sum: 9013 Ratio: 0.06%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 843565 (Eliminated: 0 Frozen: 260681) Constraints : 6199672 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 954MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 8.47s Memory: 864MB (+0MB) UNKNOWN Iteration Time: 8.54s Iteration 92 Queue: [(14,70,3,True), (15,75,3,True), (16,80,3,False), (17,85,3,False), (18,90,3,False), (19,95,2,True), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 93 Time : 711.574s (Solving: 677.08s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 711.692s Choices : 17643841 (Domain: 17366195) Conflicts : 754994 (Analyzed: 754991) Restarts : 8896 (Average: 84.87 Last: 171) Model-Level : 232.0 Problems : 93 (Average Length: 89.85 Splits: 0) Lemmas : 754991 (Deleted: 719198) Binary : 9522 (Ratio: 1.26%) Ternary : 2350 (Ratio: 0.31%) Conflict : 754991 (Average Length: 437.4 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 754991 (Average: 21.70 Max: 1255 Sum: 16385754) Executed : 754849 (Average: 21.69 Max: 1255 Sum: 16376741 Ratio: 99.94%) Bounded : 142 (Average: 63.47 Max: 117 Sum: 9013 Ratio: 0.06%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 843565 (Eliminated: 0 Frozen: 260681) Constraints : 6199658 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 954MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 6.66s Memory: 864MB (+0MB) UNKNOWN Iteration Time: 6.71s Iteration 93 Queue: [(15,75,3,True), (16,80,3,False), (17,85,3,False), (18,90,3,False), (19,95,2,True), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 94 Time : 718.441s (Solving: 683.78s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 718.564s Choices : 17829841 (Domain: 17550556) Conflicts : 763031 (Analyzed: 763028) Restarts : 8996 (Average: 84.82 Last: 171) Model-Level : 232.0 Problems : 94 (Average Length: 90.14 Splits: 0) Lemmas : 763028 (Deleted: 727001) Binary : 9604 (Ratio: 1.26%) Ternary : 2392 (Ratio: 0.31%) Conflict : 763028 (Average Length: 435.0 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 763028 (Average: 21.70 Max: 1255 Sum: 16558880) Executed : 762886 (Average: 21.69 Max: 1255 Sum: 16549867 Ratio: 99.95%) Bounded : 142 (Average: 63.47 Max: 117 Sum: 9013 Ratio: 0.05%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 843565 (Eliminated: 0 Frozen: 260681) Constraints : 6199658 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 954MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 6.82s Memory: 864MB (+0MB) UNKNOWN Iteration Time: 6.87s Iteration 94 Queue: [(19,95,2,True), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 95 Time : 725.122s (Solving: 690.29s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 725.248s Choices : 18029566 (Domain: 17749953) Conflicts : 771173 (Analyzed: 771170) Restarts : 9096 (Average: 84.78 Last: 171) Model-Level : 232.0 Problems : 95 (Average Length: 90.42 Splits: 0) Lemmas : 771170 (Deleted: 734817) Binary : 9652 (Ratio: 1.25%) Ternary : 2410 (Ratio: 0.31%) Conflict : 771170 (Average Length: 433.1 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 771170 (Average: 21.71 Max: 1255 Sum: 16743421) Executed : 771027 (Average: 21.70 Max: 1255 Sum: 16734291 Ratio: 99.95%) Bounded : 143 (Average: 63.85 Max: 117 Sum: 9130 Ratio: 0.05%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 843565 (Eliminated: 0 Frozen: 260681) Constraints : 6199658 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 954MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 6.62s Memory: 864MB (+0MB) UNKNOWN Iteration Time: 6.69s Iteration 95 Queue: [(4,20,8,True), (5,25,8,True), (6,30,7,True), (7,35,7,True), (8,40,6,True), (9,45,6,False), (10,50,5,True), (11,55,5,False), (12,60,4,True), (13,65,4,False), (14,70,4,False), (15,75,4,False), (16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,True), (22,110,2,False), (23,115,2,False)] Grounded Until: 115 Blocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 96 Time : 729.522s (Solving: 694.50s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 729.648s Choices : 18078479 (Domain: 17798866) Conflicts : 778962 (Analyzed: 778959) Restarts : 9196 (Average: 84.71 Last: 171) Model-Level : 232.0 Problems : 96 (Average Length: 90.70 Splits: 0) Lemmas : 778959 (Deleted: 742711) Binary : 9718 (Ratio: 1.25%) Ternary : 2416 (Ratio: 0.31%) Conflict : 778959 (Average Length: 433.5 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 778959 (Average: 21.55 Max: 1255 Sum: 16786341) Executed : 778815 (Average: 21.54 Max: 1255 Sum: 16777210 Ratio: 99.95%) Bounded : 144 (Average: 63.41 Max: 117 Sum: 9131 Ratio: 0.05%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 843565 (Eliminated: 0 Frozen: 260681) Constraints : 6199632 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 954MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 4.33s Memory: 864MB (+0MB) UNKNOWN Iteration Time: 4.41s Iteration 96 Queue: [(5,25,8,True), (6,30,7,True), (7,35,7,True), (8,40,6,True), (9,45,6,False), (10,50,5,True), (11,55,5,False), (12,60,4,True), (13,65,4,False), (14,70,4,False), (15,75,4,False), (16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,True), (22,110,2,False), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 97 Time : 735.184s (Solving: 699.99s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 735.312s Choices : 18151359 (Domain: 17868891) Conflicts : 787251 (Analyzed: 787248) Restarts : 9296 (Average: 84.69 Last: 171) Model-Level : 232.0 Problems : 97 (Average Length: 90.97 Splits: 0) Lemmas : 787248 (Deleted: 750207) Binary : 9900 (Ratio: 1.26%) Ternary : 2449 (Ratio: 0.31%) Conflict : 787248 (Average Length: 434.6 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 787248 (Average: 21.40 Max: 1255 Sum: 16848464) Executed : 787103 (Average: 21.39 Max: 1255 Sum: 16839216 Ratio: 99.95%) Bounded : 145 (Average: 63.78 Max: 117 Sum: 9248 Ratio: 0.05%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 843565 (Eliminated: 0 Frozen: 260681) Constraints : 6199632 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 992MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 5.61s Memory: 928MB (+64MB) UNKNOWN Iteration Time: 5.67s Iteration 97 Queue: [(6,30,7,True), (7,35,7,True), (8,40,6,True), (9,45,6,False), (10,50,5,True), (11,55,5,False), (12,60,4,True), (13,65,4,False), (14,70,4,False), (15,75,4,False), (16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,True), (22,110,2,False), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 98 Time : 740.519s (Solving: 705.13s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 740.648s Choices : 18232293 (Domain: 17948471) Conflicts : 795773 (Analyzed: 795770) Restarts : 9396 (Average: 84.69 Last: 171) Model-Level : 232.0 Problems : 98 (Average Length: 91.23 Splits: 0) Lemmas : 795770 (Deleted: 757967) Binary : 10039 (Ratio: 1.26%) Ternary : 2478 (Ratio: 0.31%) Conflict : 795770 (Average Length: 432.5 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 795770 (Average: 21.26 Max: 1255 Sum: 16919453) Executed : 795624 (Average: 21.25 Max: 1255 Sum: 16910093 Ratio: 99.94%) Bounded : 146 (Average: 64.11 Max: 117 Sum: 9360 Ratio: 0.06%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 843565 (Eliminated: 0 Frozen: 260681) Constraints : 6199618 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 992MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 5.26s Memory: 928MB (+0MB) UNKNOWN Iteration Time: 5.34s Iteration 98 Queue: [(7,35,7,True), (8,40,6,True), (9,45,6,False), (10,50,5,True), (11,55,5,False), (12,60,4,True), (13,65,4,False), (14,70,4,False), (15,75,4,False), (16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,True), (22,110,2,False), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 99 Time : 746.059s (Solving: 710.49s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 746.192s Choices : 18312744 (Domain: 18028258) Conflicts : 803882 (Analyzed: 803879) Restarts : 9496 (Average: 84.65 Last: 171) Model-Level : 232.0 Problems : 99 (Average Length: 91.49 Splits: 0) Lemmas : 803879 (Deleted: 766153) Binary : 10163 (Ratio: 1.26%) Ternary : 2503 (Ratio: 0.31%) Conflict : 803879 (Average Length: 430.7 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 803879 (Average: 21.14 Max: 1255 Sum: 16991304) Executed : 803733 (Average: 21.13 Max: 1255 Sum: 16981944 Ratio: 99.94%) Bounded : 146 (Average: 64.11 Max: 117 Sum: 9360 Ratio: 0.06%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 843565 (Eliminated: 0 Frozen: 260681) Constraints : 6199618 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 992MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 5.48s Memory: 928MB (+0MB) UNKNOWN Iteration Time: 5.55s Iteration 99 Queue: [(8,40,6,True), (9,45,6,False), (10,50,5,True), (11,55,5,False), (12,60,4,True), (13,65,4,False), (14,70,4,False), (15,75,4,False), (16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,True), (22,110,2,False), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 100 Time : 752.945s (Solving: 717.21s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 753.080s Choices : 18413605 (Domain: 18127692) Conflicts : 812225 (Analyzed: 812222) Restarts : 9596 (Average: 84.64 Last: 171) Model-Level : 232.0 Problems : 100 (Average Length: 91.75 Splits: 0) Lemmas : 812222 (Deleted: 774009) Binary : 10330 (Ratio: 1.27%) Ternary : 2531 (Ratio: 0.31%) Conflict : 812222 (Average Length: 429.1 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 812222 (Average: 21.03 Max: 1255 Sum: 17082239) Executed : 812076 (Average: 21.02 Max: 1255 Sum: 17072879 Ratio: 99.95%) Bounded : 146 (Average: 64.11 Max: 117 Sum: 9360 Ratio: 0.05%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 843565 (Eliminated: 0 Frozen: 260681) Constraints : 6199618 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 992MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 6.83s Memory: 928MB (+0MB) UNKNOWN Iteration Time: 6.89s Iteration 100 Queue: [(10,50,5,True), (11,55,5,False), (12,60,4,True), (13,65,4,False), (14,70,4,False), (15,75,4,False), (16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,True), (22,110,2,False), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 101 Time : 761.264s (Solving: 725.36s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 761.400s Choices : 18595494 (Domain: 18308080) Conflicts : 821264 (Analyzed: 821261) Restarts : 9696 (Average: 84.70 Last: 171) Model-Level : 232.0 Problems : 101 (Average Length: 92.00 Splits: 0) Lemmas : 821261 (Deleted: 783859) Binary : 10613 (Ratio: 1.29%) Ternary : 2570 (Ratio: 0.31%) Conflict : 821261 (Average Length: 427.9 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 821261 (Average: 21.01 Max: 1255 Sum: 17250844) Executed : 821114 (Average: 20.99 Max: 1255 Sum: 17241373 Ratio: 99.95%) Bounded : 147 (Average: 64.43 Max: 117 Sum: 9471 Ratio: 0.05%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 843565 (Eliminated: 0 Frozen: 260681) Constraints : 6199618 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 992MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 8.27s Memory: 928MB (+0MB) UNKNOWN Iteration Time: 8.32s Iteration 101 Queue: [(12,60,4,True), (13,65,4,False), (14,70,4,False), (15,75,4,False), (16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,True), (22,110,2,False), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 102 Time : 770.505s (Solving: 734.42s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 770.644s Choices : 18918807 (Domain: 18625022) Conflicts : 830335 (Analyzed: 830332) Restarts : 9796 (Average: 84.76 Last: 171) Model-Level : 232.0 Problems : 102 (Average Length: 92.25 Splits: 0) Lemmas : 830332 (Deleted: 792218) Binary : 10950 (Ratio: 1.32%) Ternary : 2589 (Ratio: 0.31%) Conflict : 830332 (Average Length: 430.6 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 830332 (Average: 21.14 Max: 1255 Sum: 17551481) Executed : 830185 (Average: 21.13 Max: 1255 Sum: 17542010 Ratio: 99.95%) Bounded : 147 (Average: 64.43 Max: 117 Sum: 9471 Ratio: 0.05%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 843565 (Eliminated: 0 Frozen: 260681) Constraints : 6199618 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 992MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 9.18s Memory: 928MB (+0MB) UNKNOWN Iteration Time: 9.25s Iteration 102 Queue: [(16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,True), (22,110,2,False), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 103 Time : 777.723s (Solving: 741.45s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 777.864s Choices : 19124132 (Domain: 18828510) Conflicts : 838825 (Analyzed: 838822) Restarts : 9896 (Average: 84.76 Last: 171) Model-Level : 232.0 Problems : 103 (Average Length: 92.49 Splits: 0) Lemmas : 838822 (Deleted: 798859) Binary : 11053 (Ratio: 1.32%) Ternary : 2599 (Ratio: 0.31%) Conflict : 838822 (Average Length: 429.3 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 838822 (Average: 21.15 Max: 1255 Sum: 17741113) Executed : 838675 (Average: 21.14 Max: 1255 Sum: 17731642 Ratio: 99.95%) Bounded : 147 (Average: 64.43 Max: 117 Sum: 9471 Ratio: 0.05%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 843565 (Eliminated: 0 Frozen: 260681) Constraints : 6199618 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 992MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 7.15s Memory: 928MB (+0MB) UNKNOWN Iteration Time: 7.22s Iteration 103 Queue: [(20,100,2,True), (21,105,2,True), (22,110,2,False), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 104 Time : 788.463s (Solving: 752.00s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 788.612s Choices : 19701381 (Domain: 19402290) Conflicts : 848031 (Analyzed: 848028) Restarts : 9996 (Average: 84.84 Last: 171) Model-Level : 232.0 Problems : 104 (Average Length: 92.72 Splits: 0) Lemmas : 848028 (Deleted: 809121) Binary : 11317 (Ratio: 1.33%) Ternary : 2641 (Ratio: 0.31%) Conflict : 848028 (Average Length: 431.2 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 848028 (Average: 21.57 Max: 1255 Sum: 18290718) Executed : 847880 (Average: 21.56 Max: 1255 Sum: 18281130 Ratio: 99.95%) Bounded : 148 (Average: 64.78 Max: 117 Sum: 9588 Ratio: 0.05%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 843565 (Eliminated: 0 Frozen: 260681) Constraints : 6199618 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 992MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 10.67s Memory: 928MB (+0MB) UNKNOWN Iteration Time: 10.75s Iteration 104 Queue: [(21,105,2,True), (22,110,2,False), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 105 Time : 795.621s (Solving: 758.99s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 795.772s Choices : 19895402 (Domain: 19594792) Conflicts : 856218 (Analyzed: 856215) Restarts : 10096 (Average: 84.81 Last: 171) Model-Level : 232.0 Problems : 105 (Average Length: 92.95 Splits: 0) Lemmas : 856215 (Deleted: 815791) Binary : 11376 (Ratio: 1.33%) Ternary : 2652 (Ratio: 0.31%) Conflict : 856215 (Average Length: 430.1 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 856215 (Average: 21.57 Max: 1255 Sum: 18464797) Executed : 856067 (Average: 21.55 Max: 1255 Sum: 18455209 Ratio: 99.95%) Bounded : 148 (Average: 64.78 Max: 117 Sum: 9588 Ratio: 0.05%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 843565 (Eliminated: 0 Frozen: 260681) Constraints : 6199592 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 992MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 7.10s Memory: 928MB (+0MB) UNKNOWN Iteration Time: 7.16s Iteration 105 Queue: [(4,20,9,True), (5,25,9,True), (6,30,8,True), (7,35,8,False), (8,40,7,True), (9,45,6,True), (10,50,6,False), (11,55,5,True), (12,60,5,False), (13,65,4,True), (14,70,4,False), (15,75,4,False), (16,80,4,False), (17,85,3,True), (18,90,3,False), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,2,True), (23,115,2,False)] Grounded Until: 115 Blocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 106 Time : 801.352s (Solving: 764.54s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 801.504s Choices : 19944559 (Domain: 19643949) Conflicts : 864440 (Analyzed: 864437) Restarts : 10196 (Average: 84.78 Last: 171) Model-Level : 232.0 Problems : 106 (Average Length: 93.18 Splits: 0) Lemmas : 864437 (Deleted: 823762) Binary : 11406 (Ratio: 1.32%) Ternary : 2658 (Ratio: 0.31%) Conflict : 864437 (Average Length: 433.5 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 864437 (Average: 21.41 Max: 1255 Sum: 18507477) Executed : 864289 (Average: 21.40 Max: 1255 Sum: 18497889 Ratio: 99.95%) Bounded : 148 (Average: 64.78 Max: 117 Sum: 9588 Ratio: 0.05%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 843565 (Eliminated: 0 Frozen: 260681) Constraints : 6199592 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 992MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 5.67s Memory: 928MB (+0MB) UNKNOWN Iteration Time: 5.74s Iteration 106 Queue: [(5,25,9,True), (6,30,8,True), (7,35,8,False), (8,40,7,True), (9,45,6,True), (10,50,6,False), (11,55,5,True), (12,60,5,False), (13,65,4,True), (14,70,4,False), (15,75,4,False), (16,80,4,False), (17,85,3,True), (18,90,3,False), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,2,True), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 107 Time : 805.448s (Solving: 768.47s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 805.600s Choices : 19988885 (Domain: 19688274) Conflicts : 872178 (Analyzed: 872175) Restarts : 10296 (Average: 84.71 Last: 171) Model-Level : 232.0 Problems : 107 (Average Length: 93.40 Splits: 0) Lemmas : 872175 (Deleted: 831768) Binary : 11418 (Ratio: 1.31%) Ternary : 2662 (Ratio: 0.31%) Conflict : 872175 (Average Length: 431.6 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 872175 (Average: 21.26 Max: 1255 Sum: 18545209) Executed : 872027 (Average: 21.25 Max: 1255 Sum: 18535621 Ratio: 99.95%) Bounded : 148 (Average: 64.78 Max: 117 Sum: 9588 Ratio: 0.05%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 843565 (Eliminated: 0 Frozen: 260681) Constraints : 6199592 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 992MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 4.04s Memory: 928MB (+0MB) UNKNOWN Iteration Time: 4.10s Iteration 107 Queue: [(6,30,8,True), (7,35,8,False), (8,40,7,True), (9,45,6,True), (10,50,6,False), (11,55,5,True), (12,60,5,False), (13,65,4,True), (14,70,4,False), (15,75,4,False), (16,80,4,False), (17,85,3,True), (18,90,3,False), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,2,True), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 108 Time : 810.421s (Solving: 773.24s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 810.576s Choices : 20037491 (Domain: 19736863) Conflicts : 880181 (Analyzed: 880178) Restarts : 10396 (Average: 84.67 Last: 171) Model-Level : 232.0 Problems : 108 (Average Length: 93.62 Splits: 0) Lemmas : 880178 (Deleted: 839406) Binary : 11459 (Ratio: 1.30%) Ternary : 2665 (Ratio: 0.30%) Conflict : 880178 (Average Length: 430.4 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 880178 (Average: 21.12 Max: 1255 Sum: 18585904) Executed : 880030 (Average: 21.11 Max: 1255 Sum: 18576316 Ratio: 99.95%) Bounded : 148 (Average: 64.78 Max: 117 Sum: 9588 Ratio: 0.05%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 843565 (Eliminated: 0 Frozen: 260681) Constraints : 6199592 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 992MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 4.90s Memory: 928MB (+0MB) UNKNOWN Iteration Time: 4.98s Iteration 108 Queue: [(8,40,7,True), (9,45,6,True), (10,50,6,False), (11,55,5,True), (12,60,5,False), (13,65,4,True), (14,70,4,False), (15,75,4,False), (16,80,4,False), (17,85,3,True), (18,90,3,False), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,2,True), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 109 Time : 815.883s (Solving: 778.53s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 816.040s Choices : 20115050 (Domain: 19813758) Conflicts : 888846 (Analyzed: 888843) Restarts : 10496 (Average: 84.68 Last: 171) Model-Level : 232.0 Problems : 109 (Average Length: 93.83 Splits: 0) Lemmas : 888843 (Deleted: 849414) Binary : 11526 (Ratio: 1.30%) Ternary : 2672 (Ratio: 0.30%) Conflict : 888843 (Average Length: 429.1 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 888843 (Average: 20.99 Max: 1255 Sum: 18653657) Executed : 888694 (Average: 20.98 Max: 1255 Sum: 18643952 Ratio: 99.95%) Bounded : 149 (Average: 65.13 Max: 117 Sum: 9705 Ratio: 0.05%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 843565 (Eliminated: 0 Frozen: 260681) Constraints : 6199592 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 992MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 5.40s Memory: 928MB (+0MB) UNKNOWN Iteration Time: 5.47s Iteration 109 Queue: [(9,45,6,True), (10,50,6,False), (11,55,5,True), (12,60,5,False), (13,65,4,True), (14,70,4,False), (15,75,4,False), (16,80,4,False), (17,85,3,True), (18,90,3,False), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,2,True), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 110 Time : 821.560s (Solving: 784.04s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 821.720s Choices : 20198480 (Domain: 19896292) Conflicts : 897392 (Analyzed: 897389) Restarts : 10596 (Average: 84.69 Last: 171) Model-Level : 232.0 Problems : 110 (Average Length: 94.05 Splits: 0) Lemmas : 897389 (Deleted: 855689) Binary : 11593 (Ratio: 1.29%) Ternary : 2680 (Ratio: 0.30%) Conflict : 897389 (Average Length: 428.6 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 897389 (Average: 20.87 Max: 1255 Sum: 18724903) Executed : 897239 (Average: 20.86 Max: 1255 Sum: 18715087 Ratio: 99.95%) Bounded : 150 (Average: 65.44 Max: 117 Sum: 9816 Ratio: 0.05%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 843565 (Eliminated: 0 Frozen: 260681) Constraints : 6199578 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 992MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 5.62s Memory: 928MB (+0MB) UNKNOWN Iteration Time: 5.68s Iteration 110 Queue: [(11,55,5,True), (12,60,5,False), (13,65,4,True), (14,70,4,False), (15,75,4,False), (16,80,4,False), (17,85,3,True), (18,90,3,False), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,2,True), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 111 Time : 827.783s (Solving: 790.10s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 827.944s Choices : 20306281 (Domain: 20003331) Conflicts : 906318 (Analyzed: 906315) Restarts : 10696 (Average: 84.73 Last: 171) Model-Level : 232.0 Problems : 111 (Average Length: 94.25 Splits: 0) Lemmas : 906315 (Deleted: 866143) Binary : 11663 (Ratio: 1.29%) Ternary : 2685 (Ratio: 0.30%) Conflict : 906315 (Average Length: 428.2 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 906315 (Average: 20.76 Max: 1255 Sum: 18819535) Executed : 906165 (Average: 20.75 Max: 1255 Sum: 18809719 Ratio: 99.95%) Bounded : 150 (Average: 65.44 Max: 117 Sum: 9816 Ratio: 0.05%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 843565 (Eliminated: 0 Frozen: 260681) Constraints : 6199578 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 992MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 6.17s Memory: 928MB (+0MB) UNKNOWN Iteration Time: 6.23s Iteration 111 Queue: [(13,65,4,True), (14,70,4,False), (15,75,4,False), (16,80,4,False), (17,85,3,True), (18,90,3,False), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,2,True), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 112 Time : 834.747s (Solving: 796.88s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 834.912s Choices : 20478106 (Domain: 20173609) Conflicts : 915300 (Analyzed: 915297) Restarts : 10796 (Average: 84.78 Last: 171) Model-Level : 232.0 Problems : 112 (Average Length: 94.46 Splits: 0) Lemmas : 915297 (Deleted: 874724) Binary : 11740 (Ratio: 1.28%) Ternary : 2693 (Ratio: 0.29%) Conflict : 915297 (Average Length: 428.1 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 915297 (Average: 20.73 Max: 1255 Sum: 18974143) Executed : 915147 (Average: 20.72 Max: 1255 Sum: 18964327 Ratio: 99.95%) Bounded : 150 (Average: 65.44 Max: 117 Sum: 9816 Ratio: 0.05%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 843565 (Eliminated: 0 Frozen: 260681) Constraints : 6199578 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 992MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 6.91s Memory: 928MB (+0MB) UNKNOWN Iteration Time: 6.97s Iteration 112 Queue: [(17,85,3,True), (18,90,3,False), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,2,True), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 113 Time : 842.427s (Solving: 804.35s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 842.596s Choices : 20711753 (Domain: 20405971) Conflicts : 923784 (Analyzed: 923781) Restarts : 10896 (Average: 84.78 Last: 171) Model-Level : 232.0 Problems : 113 (Average Length: 94.65 Splits: 0) Lemmas : 923781 (Deleted: 881314) Binary : 11799 (Ratio: 1.28%) Ternary : 2694 (Ratio: 0.29%) Conflict : 923781 (Average Length: 428.1 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 923781 (Average: 20.77 Max: 1255 Sum: 19188706) Executed : 923631 (Average: 20.76 Max: 1255 Sum: 19178890 Ratio: 99.95%) Bounded : 150 (Average: 65.44 Max: 117 Sum: 9816 Ratio: 0.05%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 843565 (Eliminated: 0 Frozen: 260681) Constraints : 6199578 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 992MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 7.61s Memory: 928MB (+0MB) UNKNOWN Iteration Time: 7.69s Iteration 113 Queue: [(22,110,2,True), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 114 Time : 851.828s (Solving: 813.59s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 851.988s Choices : 21189121 (Domain: 20881118) Conflicts : 932545 (Analyzed: 932542) Restarts : 10996 (Average: 84.81 Last: 171) Model-Level : 232.0 Problems : 114 (Average Length: 94.85 Splits: 0) Lemmas : 932542 (Deleted: 891689) Binary : 11872 (Ratio: 1.27%) Ternary : 2702 (Ratio: 0.29%) Conflict : 932542 (Average Length: 428.4 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 932542 (Average: 21.06 Max: 1255 Sum: 19640168) Executed : 932392 (Average: 21.05 Max: 1255 Sum: 19630352 Ratio: 99.95%) Bounded : 150 (Average: 65.44 Max: 117 Sum: 9816 Ratio: 0.05%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 843565 (Eliminated: 0 Frozen: 260681) Constraints : 6199578 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 992MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 9.33s Memory: 928MB (+0MB) UNKNOWN Iteration Time: 9.39s Iteration 114 Queue: [(4,20,10,True), (5,25,10,True), (6,30,9,True), (7,35,8,True), (8,40,8,False), (9,45,7,False), (10,50,6,True), (11,55,6,False), (12,60,5,True), (13,65,5,False), (14,70,4,True), (15,75,4,False), (16,80,4,False), (17,85,4,False), (18,90,3,True), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,2,False)] Grounded Until: 115 Blocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 115 Time : 858.081s (Solving: 819.64s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 858.244s Choices : 21237814 (Domain: 20929811) Conflicts : 940422 (Analyzed: 940419) Restarts : 11096 (Average: 84.75 Last: 171) Model-Level : 232.0 Problems : 115 (Average Length: 95.04 Splits: 0) Lemmas : 940419 (Deleted: 898064) Binary : 11895 (Ratio: 1.26%) Ternary : 2711 (Ratio: 0.29%) Conflict : 940419 (Average Length: 432.1 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 940419 (Average: 20.93 Max: 1255 Sum: 19683560) Executed : 940269 (Average: 20.92 Max: 1255 Sum: 19673744 Ratio: 99.95%) Bounded : 150 (Average: 65.44 Max: 117 Sum: 9816 Ratio: 0.05%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 843565 (Eliminated: 0 Frozen: 260681) Constraints : 6199578 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 992MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 6.18s Memory: 928MB (+0MB) UNKNOWN Iteration Time: 6.26s Iteration 115 Queue: [(5,25,10,True), (6,30,9,True), (7,35,8,True), (8,40,8,False), (9,45,7,False), (10,50,6,True), (11,55,6,False), (12,60,5,True), (13,65,5,False), (14,70,4,True), (15,75,4,False), (16,80,4,False), (17,85,4,False), (18,90,3,True), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 116 Time : 862.634s (Solving: 824.01s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 862.800s Choices : 21283934 (Domain: 20975706) Conflicts : 948329 (Analyzed: 948326) Restarts : 11196 (Average: 84.70 Last: 171) Model-Level : 232.0 Problems : 116 (Average Length: 95.23 Splits: 0) Lemmas : 948326 (Deleted: 905749) Binary : 11918 (Ratio: 1.26%) Ternary : 2716 (Ratio: 0.29%) Conflict : 948326 (Average Length: 430.8 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 948326 (Average: 20.80 Max: 1255 Sum: 19722535) Executed : 948176 (Average: 20.79 Max: 1255 Sum: 19712719 Ratio: 99.95%) Bounded : 150 (Average: 65.44 Max: 117 Sum: 9816 Ratio: 0.05%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 843565 (Eliminated: 0 Frozen: 260681) Constraints : 6199578 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 992MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 4.49s Memory: 928MB (+0MB) UNKNOWN Iteration Time: 4.56s Iteration 116 Queue: [(6,30,9,True), (7,35,8,True), (8,40,8,False), (9,45,7,False), (10,50,6,True), (11,55,6,False), (12,60,5,True), (13,65,5,False), (14,70,4,True), (15,75,4,False), (16,80,4,False), (17,85,4,False), (18,90,3,True), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 117 Time : 867.156s (Solving: 828.36s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 867.324s Choices : 21344350 (Domain: 21035360) Conflicts : 956539 (Analyzed: 956536) Restarts : 11296 (Average: 84.68 Last: 171) Model-Level : 232.0 Problems : 117 (Average Length: 95.42 Splits: 0) Lemmas : 956536 (Deleted: 913462) Binary : 11977 (Ratio: 1.25%) Ternary : 2720 (Ratio: 0.28%) Conflict : 956536 (Average Length: 429.7 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 956536 (Average: 20.67 Max: 1255 Sum: 19773460) Executed : 956386 (Average: 20.66 Max: 1255 Sum: 19763644 Ratio: 99.95%) Bounded : 150 (Average: 65.44 Max: 117 Sum: 9816 Ratio: 0.05%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 843565 (Eliminated: 0 Frozen: 260681) Constraints : 6199578 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 992MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 4.47s Memory: 928MB (+0MB) UNKNOWN Iteration Time: 4.53s Iteration 117 Queue: [(7,35,8,True), (8,40,8,False), (9,45,7,False), (10,50,6,True), (11,55,6,False), (12,60,5,True), (13,65,5,False), (14,70,4,True), (15,75,4,False), (16,80,4,False), (17,85,4,False), (18,90,3,True), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 118 Time : 873.554s (Solving: 834.56s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 873.728s Choices : 21446233 (Domain: 21135993) Conflicts : 965893 (Analyzed: 965890) Restarts : 11396 (Average: 84.76 Last: 176) Model-Level : 232.0 Problems : 118 (Average Length: 95.60 Splits: 0) Lemmas : 965890 (Deleted: 923594) Binary : 12124 (Ratio: 1.26%) Ternary : 2726 (Ratio: 0.28%) Conflict : 965890 (Average Length: 430.0 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 965890 (Average: 20.56 Max: 1255 Sum: 19862055) Executed : 965740 (Average: 20.55 Max: 1255 Sum: 19852239 Ratio: 99.95%) Bounded : 150 (Average: 65.44 Max: 117 Sum: 9816 Ratio: 0.05%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 843565 (Eliminated: 0 Frozen: 260681) Constraints : 6199578 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 992MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 6.32s Memory: 928MB (+0MB) UNKNOWN Iteration Time: 6.40s Iteration 118 Queue: [(10,50,6,True), (11,55,6,False), (12,60,5,True), (13,65,5,False), (14,70,4,True), (15,75,4,False), (16,80,4,False), (17,85,4,False), (18,90,3,True), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 119 Time : 880.387s (Solving: 841.21s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 880.564s Choices : 21576988 (Domain: 21265977) Conflicts : 974504 (Analyzed: 974501) Restarts : 11496 (Average: 84.77 Last: 176) Model-Level : 232.0 Problems : 119 (Average Length: 95.78 Splits: 0) Lemmas : 974501 (Deleted: 932636) Binary : 12188 (Ratio: 1.25%) Ternary : 2732 (Ratio: 0.28%) Conflict : 974501 (Average Length: 430.4 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 974501 (Average: 20.50 Max: 1255 Sum: 19978233) Executed : 974351 (Average: 20.49 Max: 1255 Sum: 19968417 Ratio: 99.95%) Bounded : 150 (Average: 65.44 Max: 117 Sum: 9816 Ratio: 0.05%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 843565 (Eliminated: 0 Frozen: 260681) Constraints : 6199578 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 992MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 6.77s Memory: 928MB (+0MB) UNKNOWN Iteration Time: 6.84s Iteration 119 Queue: [(12,60,5,True), (13,65,5,False), (14,70,4,True), (15,75,4,False), (16,80,4,False), (17,85,4,False), (18,90,3,True), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 120 Time : 887.424s (Solving: 848.08s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 887.604s Choices : 21753795 (Domain: 21441284) Conflicts : 983478 (Analyzed: 983475) Restarts : 11596 (Average: 84.81 Last: 176) Model-Level : 232.0 Problems : 120 (Average Length: 95.96 Splits: 0) Lemmas : 983475 (Deleted: 941030) Binary : 12258 (Ratio: 1.25%) Ternary : 2742 (Ratio: 0.28%) Conflict : 983475 (Average Length: 430.2 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 983475 (Average: 20.48 Max: 1255 Sum: 20139125) Executed : 983325 (Average: 20.47 Max: 1255 Sum: 20129309 Ratio: 99.95%) Bounded : 150 (Average: 65.44 Max: 117 Sum: 9816 Ratio: 0.05%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 843565 (Eliminated: 0 Frozen: 260681) Constraints : 6199578 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 992MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 6.99s Memory: 928MB (+0MB) UNKNOWN Iteration Time: 7.04s Iteration 120 Queue: [(14,70,4,True), (15,75,4,False), (16,80,4,False), (17,85,4,False), (18,90,3,True), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... *** Info : (planner): INTERRUPTED by signal! UNKNOWN INTERRUPTED : 1 Models : 0+ Calls : 121 Time : 892.630s (Solving: 853.08s 1st Model: 0.05s Unsat: 4.31s) CPU Time : 892.792s Choices : 21924673 (Domain: 21611322) Conflicts : 989110 (Analyzed: 989107) Restarts : 11656 (Average: 84.86 Last: 176) Model-Level : 232.0 Problems : 121 (Average Length: 96.13 Splits: 0) Lemmas : 989107 (Deleted: 945509) Binary : 12327 (Ratio: 1.25%) Ternary : 2742 (Ratio: 0.28%) Conflict : 989107 (Average Length: 430.7 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 989107 (Average: 20.52 Max: 1255 Sum: 20298469) Executed : 988957 (Average: 20.51 Max: 1255 Sum: 20288653 Ratio: 99.95%) Bounded : 150 (Average: 65.44 Max: 117 Sum: 9816 Ratio: 0.05%) Rules : 150283 (Original: 135818) Atoms : 72365 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 843565 (Eliminated: 0 Frozen: 260681) Constraints : 6199578 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 992MB Max. Length : 115 steps Models : 1