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-5.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-5.pddl Parsing... Parsing: [0.030s CPU, 0.031s wall-clock] Normalizing task... [0.000s CPU, 0.002s wall-clock] Instantiating... Generating Datalog program... [0.010s CPU, 0.008s wall-clock] Normalizing Datalog program... Normalizing Datalog program: [0.030s CPU, 0.041s wall-clock] Preparing model... [0.030s CPU, 0.022s wall-clock] Generated 115 rules. Computing model... [0.370s CPU, 0.373s wall-clock] 2300 relevant atoms 2393 auxiliary atoms 4693 final queue length 8087 total queue pushes Completing instantiation... [0.690s CPU, 0.690s wall-clock] Instantiating: [1.130s CPU, 1.139s wall-clock] Computing fact groups... Finding invariants... 24 initial candidates Finding invariants: [0.130s CPU, 0.131s wall-clock] Checking invariant weight... [0.000s CPU, 0.001s wall-clock] Instantiating groups... [0.010s CPU, 0.007s wall-clock] Collecting mutex groups... [0.000s CPU, 0.001s wall-clock] Choosing groups... 238 uncovered facts Choosing groups: [0.010s CPU, 0.001s wall-clock] Building translation key... [0.010s CPU, 0.009s wall-clock] Computing fact groups: [0.170s CPU, 0.167s wall-clock] Building STRIPS to SAS dictionary... [0.000s CPU, 0.002s wall-clock] Building dictionary for full mutex groups... [0.000s CPU, 0.002s wall-clock] Building mutex information... Building mutex information: [0.010s CPU, 0.003s wall-clock] Translating task... Processing axioms... Simplifying axioms... [0.000s CPU, 0.000s wall-clock] Processing axioms: [0.030s CPU, 0.039s wall-clock] Translating task: [0.730s CPU, 0.730s wall-clock] 2672 effect conditions simplified 0 implied preconditions added Detecting unreachable propositions... 0 operators removed 0 axioms removed 3 propositions removed Detecting unreachable propositions: [0.360s CPU, 0.357s wall-clock] Reordering and filtering variables... 241 of 241 variables necessary. 12 of 15 mutex groups necessary. 1596 of 1596 operators necessary. 0 of 0 axiom rules necessary. Reordering and filtering variables: [0.240s CPU, 0.242s wall-clock] Translator variables: 241 Translator derived variables: 0 Translator facts: 505 Translator goal facts: 10 Translator mutex groups: 12 Translator total mutex groups size: 36 Translator operators: 1596 Translator axioms: 0 Translator task size: 15302 Translator peak memory: 45004 KB Writing output... [0.300s CPU, 0.321s wall-clock] Done! [2.990s CPU, 3.026s wall-clock] planner.py version 0.0.1 Time: 0.61s Memory: 91MB Iteration 1 Queue: [(0,0,0,True), (1,5,0,True), (2,10,0,True), (3,15,0,True), (4,20,0,True), (5,25,0,True), (6,30,0,True)] Grounded Until: 0 Solving... [start: stats after solve call] Models : 0 Calls : 1 Time : 0.713s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s) CPU Time : 0.616s 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 : 44183 Atoms : 44183 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 : 227MB Max. Length : 0 steps Models : 0 [endof: stats after solve call] Solving Time: 0.00s Memory: 163MB (+72MB) UNSAT Iteration Time: 0.00s Iteration 2 Queue: [(1,5,0,True), (2,10,0,True), (3,15,0,True), (4,20,0,True), (5,25,0,True), (6,30,0,True)] Grounded Until: 0 Expected Memory: 163MB Grounding... [('step', [1]), ('step', [2]), ('step', [3]), ('step', [4]), ('step', [5]), ('check', [5])] Grounding Time: 0.19s Memory: 163MB (+0MB) Unblocking actions... Solving... [start: stats after solve call] Models : 1+ Calls : 2 Time : 1.005s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s) CPU Time : 0.908s Choices : 367 (Domain: 28) Conflicts : 8 (Analyzed: 8) Restarts : 0 Model-Level : 115.0 Problems : 2 (Average Length: 4.50 Splits: 0) Lemmas : 8 (Deleted: 0) Binary : 6 (Ratio: 75.00%) Ternary : 0 (Ratio: 0.00%) Conflict : 8 (Average Length: 10.0 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 8 (Average: 32.62 Max: 84 Sum: 261) Executed : 6 (Average: 32.38 Max: 84 Sum: 259 Ratio: 99.23%) Bounded : 2 (Average: 1.00 Max: 1 Sum: 2 Ratio: 0.77%) Rules : 44183 Atoms : 44183 Bodies : 1 (Original: 0) Tight : Yes Variables : 11842 (Eliminated: 0 Frozen: 130) Constraints : 40811 (Binary: 95.1% Ternary: 3.4% Other: 1.4%) Memory Peak : 227MB Max. Length : 0 steps Models : 1 [endof: stats after solve call] Solving Time: 0.02s Memory: 165MB (+2MB) SAT Testing... NOT SERIALIZABLE Testing Time: 0.62s Memory: 188MB (+23MB) Solving... [start: stats after solve call] Models : 0 Calls : 3 Time : 1.102s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s) CPU Time : 1.004s Choices : 368 (Domain: 28) Conflicts : 10 (Analyzed: 9) Restarts : 0 Model-Level : 115.0 Problems : 3 (Average Length: 5.33 Splits: 0) Lemmas : 9 (Deleted: 0) Binary : 7 (Ratio: 77.78%) Ternary : 0 (Ratio: 0.00%) Conflict : 9 (Average Length: 9.1 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 9 (Average: 29.22 Max: 84 Sum: 263) Executed : 6 (Average: 28.89 Max: 84 Sum: 260 Ratio: 98.86%) Bounded : 3 (Average: 1.00 Max: 1 Sum: 3 Ratio: 1.14%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 14564 (Eliminated: 0 Frozen: 3202) Constraints : 60980 (Binary: 92.3% Ternary: 5.5% Other: 2.3%) Memory Peak : 227MB Max. Length : 0 steps Models : 1 [endof: stats after solve call] Solving Time: 0.01s Memory: 188MB (+0MB) UNSAT Iteration Time: 0.93s Iteration 3 Queue: [(2,10,0,True), (3,15,0,True), (4,20,0,True), (5,25,0,True), (6,30,0,True)] Grounded Until: 5 Expected Memory: 190.0MB Grounding... [('step', [6]), ('step', [7]), ('step', [8]), ('step', [9]), ('step', [10]), ('check', [10])] Grounding Time: 0.34s Memory: 188MB (+0MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0 Calls : 4 Time : 2.227s (Solving: 0.64s 1st Model: 0.00s Unsat: 0.64s) CPU Time : 2.128s Choices : 20428 (Domain: 19268) Conflicts : 2400 (Analyzed: 2398) Restarts : 30 (Average: 79.93 Last: 10) Model-Level : 115.0 Problems : 4 (Average Length: 7.00 Splits: 0) Lemmas : 2398 (Deleted: 589) Binary : 334 (Ratio: 13.93%) Ternary : 293 (Ratio: 12.22%) Conflict : 2398 (Average Length: 30.3 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 2398 (Average: 8.56 Max: 84 Sum: 20522) Executed : 2365 (Average: 8.42 Max: 84 Sum: 20181 Ratio: 98.34%) Bounded : 33 (Average: 10.33 Max: 12 Sum: 341 Ratio: 1.66%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 40960 (Eliminated: 0 Frozen: 11742) Constraints : 262050 (Binary: 91.6% Ternary: 6.4% Other: 1.9%) Memory Peak : 227MB Max. Length : 5 steps Models : 1 [endof: stats after solve call] Solving Time: 0.66s Memory: 197MB (+9MB) UNSAT Iteration Time: 1.13s Iteration 4 Queue: [(3,15,0,True), (4,20,0,True), (5,25,0,True), (6,30,0,True)] Grounded Until: 10 Expected Memory: 206.0MB Grounding... [('step', [11]), ('step', [12]), ('step', [13]), ('step', [14]), ('step', [15]), ('check', [15])] Grounding Time: 0.38s Memory: 203MB (+6MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0 Calls : 5 Time : 5.613s (Solving: 3.47s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 5.516s Choices : 83668 (Domain: 80839) Conflicts : 9035 (Analyzed: 9032) Restarts : 102 (Average: 88.55 Last: 20) Model-Level : 115.0 Problems : 5 (Average Length: 9.00 Splits: 0) Lemmas : 9032 (Deleted: 4942) Binary : 1008 (Ratio: 11.16%) Ternary : 545 (Ratio: 6.03%) Conflict : 9032 (Average Length: 125.9 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 9032 (Average: 9.18 Max: 95 Sum: 82898) Executed : 8982 (Average: 9.11 Max: 95 Sum: 82286 Ratio: 99.26%) Bounded : 50 (Average: 12.24 Max: 17 Sum: 612 Ratio: 0.74%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 67356 (Eliminated: 0 Frozen: 20282) Constraints : 425655 (Binary: 91.7% Ternary: 6.4% Other: 2.0%) Memory Peak : 227MB Max. Length : 10 steps Models : 1 [endof: stats after solve call] Solving Time: 2.86s Memory: 216MB (+13MB) UNSAT Iteration Time: 3.40s Iteration 5 Queue: [(4,20,0,True), (5,25,0,True), (6,30,0,True)] Grounded Until: 15 Expected Memory: 235.0MB Grounding... [('step', [16]), ('step', [17]), ('step', [18]), ('step', [19]), ('step', [20]), ('check', [20])] Grounding Time: 0.40s Memory: 223MB (+7MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 6 Time : 11.145s (Solving: 8.41s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 11.048s Choices : 194835 (Domain: 179881) Conflicts : 18138 (Analyzed: 18135) Restarts : 202 (Average: 89.78 Last: 101) Model-Level : 115.0 Problems : 6 (Average Length: 11.17 Splits: 0) Lemmas : 18135 (Deleted: 12424) Binary : 1624 (Ratio: 8.96%) Ternary : 778 (Ratio: 4.29%) Conflict : 18135 (Average Length: 297.3 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 18135 (Average: 10.37 Max: 302 Sum: 188090) Executed : 18076 (Average: 10.33 Max: 302 Sum: 187289 Ratio: 99.57%) Bounded : 59 (Average: 13.58 Max: 22 Sum: 801 Ratio: 0.43%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 93752 (Eliminated: 0 Frozen: 28822) Constraints : 621350 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) Memory Peak : 239MB Max. Length : 15 steps Models : 1 [endof: stats after solve call] Solving Time: 4.97s Memory: 239MB (+16MB) UNKNOWN Iteration Time: 5.54s Iteration 6 Queue: [(5,25,0,True), (6,30,0,True)] Grounded Until: 20 Expected Memory: 262.0MB Grounding... [('step', [21]), ('step', [22]), ('step', [23]), ('step', [24]), ('step', [25]), ('check', [25])] Grounding Time: 0.37s Memory: 244MB (+5MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 7 Time : 17.906s (Solving: 14.59s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 17.812s Choices : 327156 (Domain: 302805) Conflicts : 26901 (Analyzed: 26898) Restarts : 302 (Average: 89.07 Last: 101) Model-Level : 115.0 Problems : 7 (Average Length: 13.43 Splits: 0) Lemmas : 26898 (Deleted: 18459) Binary : 2330 (Ratio: 8.66%) Ternary : 962 (Ratio: 3.58%) Conflict : 26898 (Average Length: 278.8 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 26898 (Average: 11.69 Max: 357 Sum: 314445) Executed : 26829 (Average: 11.65 Max: 357 Sum: 313374 Ratio: 99.66%) Bounded : 69 (Average: 15.52 Max: 27 Sum: 1071 Ratio: 0.34%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 120148 (Eliminated: 0 Frozen: 37362) Constraints : 815724 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) Memory Peak : 263MB Max. Length : 20 steps Models : 1 [endof: stats after solve call] Solving Time: 6.22s Memory: 253MB (+9MB) UNKNOWN Iteration Time: 6.77s Iteration 7 Queue: [(6,30,0,True)] Grounded Until: 25 Expected Memory: 276.0MB Grounding... [('step', [26]), ('step', [27]), ('step', [28]), ('step', [29]), ('step', [30]), ('check', [30])] Grounding Time: 0.45s Memory: 267MB (+14MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 8 Time : 25.353s (Solving: 21.36s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 25.264s Choices : 455849 (Domain: 424072) Conflicts : 36045 (Analyzed: 36042) Restarts : 402 (Average: 89.66 Last: 101) Model-Level : 115.0 Problems : 8 (Average Length: 15.75 Splits: 0) Lemmas : 36042 (Deleted: 26452) Binary : 2666 (Ratio: 7.40%) Ternary : 1049 (Ratio: 2.91%) Conflict : 36042 (Average Length: 306.0 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 36042 (Average: 12.05 Max: 357 Sum: 434442) Executed : 35970 (Average: 12.02 Max: 357 Sum: 433275 Ratio: 99.73%) Bounded : 72 (Average: 16.21 Max: 32 Sum: 1167 Ratio: 0.27%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 146544 (Eliminated: 0 Frozen: 45902) Constraints : 1012058 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) Memory Peak : 291MB Max. Length : 25 steps Models : 1 [endof: stats after solve call] Solving Time: 6.81s Memory: 291MB (+24MB) UNKNOWN Iteration Time: 7.46s Iteration 8 Queue: [(4,20,1,True), (5,25,1,True), (6,30,1,True), (7,35,0,True), (8,40,0,True), (9,45,0,True), (10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True), (17,85,0,True)] Grounded Until: 30 Blocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 9 Time : 29.288s (Solving: 25.26s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 29.204s Choices : 495709 (Domain: 462324) Conflicts : 43610 (Analyzed: 43607) Restarts : 502 (Average: 86.87 Last: 101) Model-Level : 115.0 Problems : 9 (Average Length: 17.56 Splits: 0) Lemmas : 43607 (Deleted: 34188) Binary : 2830 (Ratio: 6.49%) Ternary : 1098 (Ratio: 2.52%) Conflict : 43607 (Average Length: 347.1 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 43607 (Average: 10.73 Max: 357 Sum: 467733) Executed : 43535 (Average: 10.70 Max: 357 Sum: 466566 Ratio: 99.75%) Bounded : 72 (Average: 16.21 Max: 32 Sum: 1167 Ratio: 0.25%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 146544 (Eliminated: 0 Frozen: 45902) Constraints : 1012016 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) Memory Peak : 291MB Max. Length : 30 steps Models : 1 [endof: stats after solve call] Solving Time: 3.93s Memory: 291MB (+0MB) UNKNOWN Iteration Time: 3.94s Iteration 9 Queue: [(5,25,1,True), (6,30,1,True), (7,35,0,True), (8,40,0,True), (9,45,0,True), (10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True), (17,85,0,True)] Grounded Until: 30 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 10 Time : 34.868s (Solving: 30.80s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 34.784s Choices : 585465 (Domain: 547882) Conflicts : 52309 (Analyzed: 52306) Restarts : 602 (Average: 86.89 Last: 101) Model-Level : 115.0 Problems : 10 (Average Length: 19.00 Splits: 0) Lemmas : 52306 (Deleted: 41407) Binary : 3164 (Ratio: 6.05%) Ternary : 1154 (Ratio: 2.21%) Conflict : 52306 (Average Length: 342.5 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 52306 (Average: 10.49 Max: 357 Sum: 548691) Executed : 52232 (Average: 10.47 Max: 357 Sum: 547465 Ratio: 99.78%) Bounded : 74 (Average: 16.57 Max: 32 Sum: 1226 Ratio: 0.22%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 146544 (Eliminated: 0 Frozen: 45902) Constraints : 1012016 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) Memory Peak : 291MB Max. Length : 30 steps Models : 1 [endof: stats after solve call] Solving Time: 5.57s Memory: 291MB (+0MB) UNKNOWN Iteration Time: 5.59s Iteration 10 Queue: [(6,30,1,True), (7,35,0,True), (8,40,0,True), (9,45,0,True), (10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True), (17,85,0,True)] Grounded Until: 30 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 11 Time : 40.323s (Solving: 36.23s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 40.240s Choices : 678499 (Domain: 638387) Conflicts : 61022 (Analyzed: 61019) Restarts : 702 (Average: 86.92 Last: 101) Model-Level : 115.0 Problems : 11 (Average Length: 20.18 Splits: 0) Lemmas : 61019 (Deleted: 49566) Binary : 3372 (Ratio: 5.53%) Ternary : 1184 (Ratio: 1.94%) Conflict : 61019 (Average Length: 343.5 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 61019 (Average: 10.37 Max: 357 Sum: 632788) Executed : 60943 (Average: 10.35 Max: 357 Sum: 631498 Ratio: 99.80%) Bounded : 76 (Average: 16.97 Max: 32 Sum: 1290 Ratio: 0.20%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 146544 (Eliminated: 0 Frozen: 45902) Constraints : 1012003 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) Memory Peak : 291MB Max. Length : 30 steps Models : 1 [endof: stats after solve call] Solving Time: 5.45s Memory: 291MB (+0MB) UNKNOWN Iteration Time: 5.46s Iteration 11 Queue: [(7,35,0,True), (8,40,0,True), (9,45,0,True), (10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True), (17,85,0,True)] Grounded Until: 30 Expected Memory: 329.0MB Grounding... [('step', [31]), ('step', [32]), ('step', [33]), ('step', [34]), ('step', [35]), ('check', [35])] Grounding Time: 0.40s Memory: 291MB (+0MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 12 Time : 45.860s (Solving: 41.12s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 45.780s Choices : 779563 (Domain: 736842) Conflicts : 69781 (Analyzed: 69778) Restarts : 802 (Average: 87.00 Last: 101) Model-Level : 115.0 Problems : 12 (Average Length: 21.58 Splits: 0) Lemmas : 69778 (Deleted: 57819) Binary : 3502 (Ratio: 5.02%) Ternary : 1233 (Ratio: 1.77%) Conflict : 69778 (Average Length: 342.0 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 69778 (Average: 10.38 Max: 357 Sum: 724277) Executed : 69699 (Average: 10.36 Max: 357 Sum: 722876 Ratio: 99.81%) Bounded : 79 (Average: 17.73 Max: 37 Sum: 1401 Ratio: 0.19%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 172940 (Eliminated: 0 Frozen: 54442) Constraints : 1210969 (Binary: 91.5% Ternary: 6.6% Other: 1.9%) Memory Peak : 316MB Max. Length : 30 steps Models : 1 [endof: stats after solve call] Solving Time: 4.94s Memory: 301MB (+10MB) UNKNOWN Iteration Time: 5.55s Iteration 12 Queue: [(8,40,0,True), (9,45,0,True), (10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True), (17,85,0,True)] Grounded Until: 35 Expected Memory: 339.0MB Grounding... [('step', [36]), ('step', [37]), ('step', [38]), ('step', [39]), ('step', [40]), ('check', [40])] Grounding Time: 0.39s Memory: 307MB (+6MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 13 Time : 51.131s (Solving: 45.74s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 51.052s Choices : 867707 (Domain: 823138) Conflicts : 78104 (Analyzed: 78101) Restarts : 902 (Average: 86.59 Last: 107) Model-Level : 115.0 Problems : 13 (Average Length: 23.15 Splits: 0) Lemmas : 78101 (Deleted: 64093) Binary : 3639 (Ratio: 4.66%) Ternary : 1263 (Ratio: 1.62%) Conflict : 78101 (Average Length: 339.2 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 78101 (Average: 10.28 Max: 357 Sum: 802547) Executed : 78022 (Average: 10.26 Max: 357 Sum: 801146 Ratio: 99.83%) Bounded : 79 (Average: 17.73 Max: 37 Sum: 1401 Ratio: 0.17%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 199336 (Eliminated: 0 Frozen: 62982) Constraints : 1411993 (Binary: 91.5% Ternary: 6.6% Other: 1.9%) Memory Peak : 337MB Max. Length : 35 steps Models : 1 [endof: stats after solve call] Solving Time: 4.67s Memory: 320MB (+13MB) UNKNOWN Iteration Time: 5.28s Iteration 13 Queue: [(9,45,0,True), (10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True), (17,85,0,True)] Grounded Until: 40 Expected Memory: 358.0MB Grounding... [('step', [41]), ('step', [42]), ('step', [43]), ('step', [44]), ('step', [45]), ('check', [45])] Grounding Time: 0.40s Memory: 326MB (+6MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 14 Time : 56.198s (Solving: 50.12s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 56.112s Choices : 979870 (Domain: 934167) Conflicts : 86377 (Analyzed: 86374) Restarts : 1002 (Average: 86.20 Last: 110) Model-Level : 115.0 Problems : 14 (Average Length: 24.86 Splits: 0) Lemmas : 86374 (Deleted: 71864) Binary : 3834 (Ratio: 4.44%) Ternary : 1306 (Ratio: 1.51%) Conflict : 86374 (Average Length: 327.5 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 86374 (Average: 10.49 Max: 423 Sum: 906136) Executed : 86293 (Average: 10.47 Max: 423 Sum: 904651 Ratio: 99.84%) Bounded : 81 (Average: 18.33 Max: 42 Sum: 1485 Ratio: 0.16%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 225732 (Eliminated: 0 Frozen: 71522) Constraints : 1613063 (Binary: 91.5% Ternary: 6.6% Other: 1.9%) Memory Peak : 359MB Max. Length : 40 steps Models : 1 [endof: stats after solve call] Solving Time: 4.43s Memory: 354MB (+28MB) UNKNOWN Iteration Time: 5.07s Iteration 14 Queue: [(10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True), (17,85,0,True)] Grounded Until: 45 Expected Memory: 392.0MB Grounding... [('step', [46]), ('step', [47]), ('step', [48]), ('step', [49]), ('step', [50]), ('check', [50])] Grounding Time: 0.37s Memory: 354MB (+0MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 15 Time : 61.629s (Solving: 54.90s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 61.544s Choices : 1103188 (Domain: 1055956) Conflicts : 94165 (Analyzed: 94162) Restarts : 1102 (Average: 85.45 Last: 110) Model-Level : 115.0 Problems : 15 (Average Length: 26.67 Splits: 0) Lemmas : 94162 (Deleted: 79983) Binary : 3911 (Ratio: 4.15%) Ternary : 1326 (Ratio: 1.41%) Conflict : 94162 (Average Length: 331.4 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 94162 (Average: 10.79 Max: 423 Sum: 1016477) Executed : 94081 (Average: 10.78 Max: 423 Sum: 1014992 Ratio: 99.85%) Bounded : 81 (Average: 18.33 Max: 42 Sum: 1485 Ratio: 0.15%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 252128 (Eliminated: 0 Frozen: 80062) Constraints : 1814133 (Binary: 91.5% Ternary: 6.6% Other: 1.9%) Memory Peak : 387MB Max. Length : 45 steps Models : 1 [endof: stats after solve call] Solving Time: 4.83s Memory: 362MB (+8MB) UNKNOWN Iteration Time: 5.44s Iteration 15 Queue: [(11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True), (17,85,0,True)] Grounded Until: 50 Expected Memory: 400.0MB Grounding... [('step', [51]), ('step', [52]), ('step', [53]), ('step', [54]), ('step', [55]), ('check', [55])] Grounding Time: 0.38s Memory: 367MB (+5MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 16 Time : 67.229s (Solving: 59.82s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 67.148s Choices : 1220676 (Domain: 1172081) Conflicts : 102486 (Analyzed: 102483) Restarts : 1202 (Average: 85.26 Last: 110) Model-Level : 115.0 Problems : 16 (Average Length: 28.56 Splits: 0) Lemmas : 102483 (Deleted: 87348) Binary : 4006 (Ratio: 3.91%) Ternary : 1342 (Ratio: 1.31%) Conflict : 102483 (Average Length: 327.5 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 102483 (Average: 10.95 Max: 533 Sum: 1122544) Executed : 102399 (Average: 10.94 Max: 533 Sum: 1120893 Ratio: 99.85%) Bounded : 84 (Average: 19.65 Max: 57 Sum: 1651 Ratio: 0.15%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 278524 (Eliminated: 0 Frozen: 88602) Constraints : 2015203 (Binary: 91.5% Ternary: 6.6% Other: 1.9%) Memory Peak : 410MB Max. Length : 50 steps Models : 1 [endof: stats after solve call] Solving Time: 4.99s Memory: 382MB (+15MB) UNKNOWN Iteration Time: 5.61s Iteration 16 Queue: [(12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True), (17,85,0,True)] Grounded Until: 55 Expected Memory: 420.0MB Grounding... [('step', [56]), ('step', [57]), ('step', [58]), ('step', [59]), ('step', [60]), ('check', [60])] Grounding Time: 0.39s Memory: 383MB (+1MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 17 Time : 72.326s (Solving: 64.21s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 72.248s Choices : 1366534 (Domain: 1315690) Conflicts : 110475 (Analyzed: 110472) Restarts : 1302 (Average: 84.85 Last: 110) Model-Level : 115.0 Problems : 17 (Average Length: 30.53 Splits: 0) Lemmas : 110472 (Deleted: 95163) Binary : 4123 (Ratio: 3.73%) Ternary : 1359 (Ratio: 1.23%) Conflict : 110472 (Average Length: 325.6 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 110472 (Average: 11.37 Max: 533 Sum: 1256134) Executed : 110386 (Average: 11.35 Max: 533 Sum: 1254364 Ratio: 99.86%) Bounded : 86 (Average: 20.58 Max: 62 Sum: 1770 Ratio: 0.14%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 304920 (Eliminated: 0 Frozen: 97142) Constraints : 2216234 (Binary: 91.5% Ternary: 6.6% Other: 1.9%) Memory Peak : 429MB Max. Length : 55 steps Models : 1 [endof: stats after solve call] Solving Time: 4.45s Memory: 400MB (+17MB) UNKNOWN Iteration Time: 5.11s Iteration 17 Queue: [(13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True), (17,85,0,True)] Grounded Until: 60 Expected Memory: 438.0MB Grounding... [('step', [61]), ('step', [62]), ('step', [63]), ('step', [64]), ('step', [65]), ('check', [65])] Grounding Time: 0.39s Memory: 404MB (+4MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 18 Time : 78.486s (Solving: 69.64s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 78.412s Choices : 1582259 (Domain: 1528281) Conflicts : 119385 (Analyzed: 119382) Restarts : 1402 (Average: 85.15 Last: 110) Model-Level : 115.0 Problems : 18 (Average Length: 32.56 Splits: 0) Lemmas : 119382 (Deleted: 104860) Binary : 4250 (Ratio: 3.56%) Ternary : 1388 (Ratio: 1.16%) Conflict : 119382 (Average Length: 332.3 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 119382 (Average: 12.19 Max: 533 Sum: 1455416) Executed : 119296 (Average: 12.18 Max: 533 Sum: 1453646 Ratio: 99.88%) Bounded : 86 (Average: 20.58 Max: 62 Sum: 1770 Ratio: 0.12%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 331316 (Eliminated: 0 Frozen: 105682) Constraints : 2413082 (Binary: 91.5% Ternary: 6.6% Other: 1.9%) Memory Peak : 450MB Max. Length : 60 steps Models : 1 [endof: stats after solve call] Solving Time: 5.51s Memory: 448MB (+44MB) UNKNOWN Iteration Time: 6.17s Iteration 18 Queue: [(14,70,0,True), (15,75,0,True), (16,80,0,True), (17,85,0,True)] Grounded Until: 65 Expected Memory: 496.0MB Grounding... [('step', [66]), ('step', [67]), ('step', [68]), ('step', [69]), ('step', [70]), ('check', [70])] Grounding Time: 0.53s Memory: 460MB (+12MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 19 Time : 85.932s (Solving: 76.22s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 85.860s Choices : 1785835 (Domain: 1729631) Conflicts : 127765 (Analyzed: 127762) Restarts : 1502 (Average: 85.06 Last: 110) Model-Level : 115.0 Problems : 19 (Average Length: 34.63 Splits: 0) Lemmas : 127762 (Deleted: 111723) Binary : 4439 (Ratio: 3.47%) Ternary : 1427 (Ratio: 1.12%) Conflict : 127762 (Average Length: 356.0 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 127762 (Average: 12.82 Max: 641 Sum: 1638063) Executed : 127673 (Average: 12.81 Max: 641 Sum: 1636080 Ratio: 99.88%) Bounded : 89 (Average: 22.28 Max: 72 Sum: 1983 Ratio: 0.12%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 357712 (Eliminated: 0 Frozen: 114222) Constraints : 2614152 (Binary: 91.5% Ternary: 6.6% Other: 1.9%) Memory Peak : 504MB Max. Length : 65 steps Models : 1 [endof: stats after solve call] Solving Time: 6.65s Memory: 463MB (+3MB) UNKNOWN Iteration Time: 7.46s Iteration 19 Queue: [(15,75,0,True), (16,80,0,True), (17,85,0,True)] Grounded Until: 70 Expected Memory: 511.0MB Grounding... [('step', [71]), ('step', [72]), ('step', [73]), ('step', [74]), ('step', [75]), ('check', [75])] Grounding Time: 0.37s Memory: 463MB (+0MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 20 Time : 93.510s (Solving: 83.07s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 93.440s Choices : 2058865 (Domain: 1999152) Conflicts : 136710 (Analyzed: 136707) Restarts : 1602 (Average: 85.34 Last: 110) Model-Level : 115.0 Problems : 20 (Average Length: 36.75 Splits: 0) Lemmas : 136707 (Deleted: 121778) Binary : 4652 (Ratio: 3.40%) Ternary : 1445 (Ratio: 1.06%) Conflict : 136707 (Average Length: 377.8 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 136707 (Average: 13.82 Max: 671 Sum: 1889318) Executed : 136616 (Average: 13.80 Max: 671 Sum: 1887181 Ratio: 99.89%) Bounded : 91 (Average: 23.48 Max: 77 Sum: 2137 Ratio: 0.11%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 384108 (Eliminated: 0 Frozen: 122762) Constraints : 2815194 (Binary: 91.5% Ternary: 6.6% Other: 1.9%) Memory Peak : 515MB Max. Length : 70 steps Models : 1 [endof: stats after solve call] Solving Time: 6.93s Memory: 476MB (+13MB) UNKNOWN Iteration Time: 7.59s Iteration 20 Queue: [(16,80,0,True), (17,85,0,True)] Grounded Until: 75 Expected Memory: 524.0MB Grounding... [('step', [76]), ('step', [77]), ('step', [78]), ('step', [79]), ('step', [80]), ('check', [80])] Grounding Time: 0.39s Memory: 479MB (+3MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 21 Time : 101.077s (Solving: 89.87s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 101.008s Choices : 2377079 (Domain: 2314344) Conflicts : 145552 (Analyzed: 145549) Restarts : 1702 (Average: 85.52 Last: 110) Model-Level : 115.0 Problems : 21 (Average Length: 38.90 Splits: 0) Lemmas : 145549 (Deleted: 129958) Binary : 4745 (Ratio: 3.26%) Ternary : 1465 (Ratio: 1.01%) Conflict : 145549 (Average Length: 382.5 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 145549 (Average: 15.03 Max: 671 Sum: 2186977) Executed : 145456 (Average: 15.01 Max: 671 Sum: 2184676 Ratio: 99.89%) Bounded : 93 (Average: 24.74 Max: 82 Sum: 2301 Ratio: 0.11%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 410504 (Eliminated: 0 Frozen: 131302) Constraints : 3016224 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 537MB Max. Length : 75 steps Models : 1 [endof: stats after solve call] Solving Time: 6.88s Memory: 498MB (+19MB) UNKNOWN Iteration Time: 7.58s Iteration 21 Queue: [(17,85,0,True)] Grounded Until: 80 Expected Memory: 546.0MB Grounding... [('step', [81]), ('step', [82]), ('step', [83]), ('step', [84]), ('step', [85]), ('check', [85])] Grounding Time: 0.38s Memory: 498MB (+0MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 22 Time : 106.918s (Solving: 94.94s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 106.852s Choices : 2626934 (Domain: 2561282) Conflicts : 153897 (Analyzed: 153894) Restarts : 1802 (Average: 85.40 Last: 110) Model-Level : 115.0 Problems : 22 (Average Length: 41.09 Splits: 0) Lemmas : 153894 (Deleted: 136518) Binary : 4815 (Ratio: 3.13%) Ternary : 1475 (Ratio: 0.96%) Conflict : 153894 (Average Length: 382.6 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 153894 (Average: 15.71 Max: 671 Sum: 2418322) Executed : 153801 (Average: 15.70 Max: 671 Sum: 2416021 Ratio: 99.90%) Bounded : 93 (Average: 24.74 Max: 82 Sum: 2301 Ratio: 0.10%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 436900 (Eliminated: 0 Frozen: 139842) Constraints : 3217244 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 558MB Max. Length : 80 steps Models : 1 [endof: stats after solve call] Solving Time: 5.17s Memory: 516MB (+18MB) UNKNOWN Iteration Time: 5.86s Iteration 22 Queue: [(4,20,2,True), (5,25,2,True), (6,30,2,True), (7,35,1,True), (8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] Grounded Until: 85 Blocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 23 Time : 112.628s (Solving: 100.53s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 112.556s Choices : 2666289 (Domain: 2600637) Conflicts : 161814 (Analyzed: 161811) Restarts : 1902 (Average: 85.07 Last: 110) Model-Level : 115.0 Problems : 23 (Average Length: 43.09 Splits: 0) Lemmas : 161811 (Deleted: 145241) Binary : 4883 (Ratio: 3.02%) Ternary : 1486 (Ratio: 0.92%) Conflict : 161811 (Average Length: 393.6 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 161811 (Average: 15.14 Max: 671 Sum: 2450229) Executed : 161716 (Average: 15.13 Max: 671 Sum: 2447754 Ratio: 99.90%) Bounded : 95 (Average: 26.05 Max: 87 Sum: 2475 Ratio: 0.10%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 436900 (Eliminated: 0 Frozen: 139842) Constraints : 3217244 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 558MB Max. Length : 85 steps Models : 1 [endof: stats after solve call] Solving Time: 5.66s Memory: 517MB (+1MB) UNKNOWN Iteration Time: 5.71s Iteration 23 Queue: [(5,25,2,True), (6,30,2,True), (7,35,1,True), (8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] Grounded Until: 85 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 24 Time : 117.957s (Solving: 105.77s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 117.888s Choices : 2734738 (Domain: 2666366) Conflicts : 171421 (Analyzed: 171418) Restarts : 2002 (Average: 85.62 Last: 110) Model-Level : 115.0 Problems : 24 (Average Length: 44.92 Splits: 0) Lemmas : 171418 (Deleted: 154283) Binary : 4986 (Ratio: 2.91%) Ternary : 1509 (Ratio: 0.88%) Conflict : 171418 (Average Length: 394.5 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 171418 (Average: 14.63 Max: 671 Sum: 2507902) Executed : 171323 (Average: 14.62 Max: 671 Sum: 2505427 Ratio: 99.90%) Bounded : 95 (Average: 26.05 Max: 87 Sum: 2475 Ratio: 0.10%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 436900 (Eliminated: 0 Frozen: 139842) Constraints : 3214748 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 558MB Max. Length : 85 steps Models : 1 [endof: stats after solve call] Solving Time: 5.30s Memory: 517MB (+0MB) UNKNOWN Iteration Time: 5.33s Iteration 24 Queue: [(6,30,2,True), (7,35,1,True), (8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] Grounded Until: 85 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 25 Time : 123.006s (Solving: 110.73s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 122.940s Choices : 2815441 (Domain: 2743992) Conflicts : 180219 (Analyzed: 180216) Restarts : 2102 (Average: 85.74 Last: 110) Model-Level : 115.0 Problems : 25 (Average Length: 46.60 Splits: 0) Lemmas : 180216 (Deleted: 163467) Binary : 5101 (Ratio: 2.83%) Ternary : 1532 (Ratio: 0.85%) Conflict : 180216 (Average Length: 400.4 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 180216 (Average: 14.29 Max: 671 Sum: 2575753) Executed : 180121 (Average: 14.28 Max: 671 Sum: 2573278 Ratio: 99.90%) Bounded : 95 (Average: 26.05 Max: 87 Sum: 2475 Ratio: 0.10%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 436900 (Eliminated: 0 Frozen: 139842) Constraints : 3214748 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 558MB Max. Length : 85 steps Models : 1 [endof: stats after solve call] Solving Time: 5.02s Memory: 517MB (+0MB) UNKNOWN Iteration Time: 5.05s Iteration 25 Queue: [(7,35,1,True), (8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] Grounded Until: 85 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 26 Time : 127.926s (Solving: 115.54s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 127.864s Choices : 2911485 (Domain: 2837581) Conflicts : 188654 (Analyzed: 188651) Restarts : 2202 (Average: 85.67 Last: 115) Model-Level : 115.0 Problems : 26 (Average Length: 48.15 Splits: 0) Lemmas : 188651 (Deleted: 170310) Binary : 5219 (Ratio: 2.77%) Ternary : 1536 (Ratio: 0.81%) Conflict : 188651 (Average Length: 407.0 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 188651 (Average: 14.09 Max: 671 Sum: 2658216) Executed : 188555 (Average: 14.08 Max: 671 Sum: 2655654 Ratio: 99.90%) Bounded : 96 (Average: 26.69 Max: 87 Sum: 2562 Ratio: 0.10%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 436900 (Eliminated: 0 Frozen: 139842) Constraints : 3214748 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 558MB Max. Length : 85 steps Models : 1 [endof: stats after solve call] Solving Time: 4.88s Memory: 517MB (+0MB) UNKNOWN Iteration Time: 4.92s Iteration 26 Queue: [(8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] Grounded Until: 85 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 27 Time : 135.092s (Solving: 122.60s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 135.036s Choices : 3062444 (Domain: 2980038) Conflicts : 197708 (Analyzed: 197705) Restarts : 2302 (Average: 85.88 Last: 115) Model-Level : 115.0 Problems : 27 (Average Length: 49.59 Splits: 0) Lemmas : 197705 (Deleted: 179876) Binary : 5554 (Ratio: 2.81%) Ternary : 1614 (Ratio: 0.82%) Conflict : 197705 (Average Length: 427.8 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 197705 (Average: 14.10 Max: 671 Sum: 2788038) Executed : 197609 (Average: 14.09 Max: 671 Sum: 2785476 Ratio: 99.91%) Bounded : 96 (Average: 26.69 Max: 87 Sum: 2562 Ratio: 0.09%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 436900 (Eliminated: 0 Frozen: 139842) Constraints : 3214722 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 558MB Max. Length : 85 steps Models : 1 [endof: stats after solve call] Solving Time: 7.13s Memory: 517MB (+0MB) UNKNOWN Iteration Time: 7.17s Iteration 27 Queue: [(9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] Grounded Until: 85 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 28 Time : 140.467s (Solving: 127.87s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 140.408s Choices : 3192312 (Domain: 3107985) Conflicts : 206567 (Analyzed: 206564) Restarts : 2402 (Average: 86.00 Last: 158) Model-Level : 115.0 Problems : 28 (Average Length: 50.93 Splits: 0) Lemmas : 206564 (Deleted: 188498) Binary : 5755 (Ratio: 2.79%) Ternary : 1656 (Ratio: 0.80%) Conflict : 206564 (Average Length: 433.6 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 206564 (Average: 14.05 Max: 671 Sum: 2901654) Executed : 206468 (Average: 14.03 Max: 671 Sum: 2899092 Ratio: 99.91%) Bounded : 96 (Average: 26.69 Max: 87 Sum: 2562 Ratio: 0.09%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 436900 (Eliminated: 0 Frozen: 139842) Constraints : 3214722 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 558MB Max. Length : 85 steps Models : 1 [endof: stats after solve call] Solving Time: 5.33s Memory: 517MB (+0MB) UNKNOWN Iteration Time: 5.37s Iteration 28 Queue: [(10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] Grounded Until: 85 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 29 Time : 146.792s (Solving: 134.08s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 146.736s Choices : 3370471 (Domain: 3279277) Conflicts : 215484 (Analyzed: 215481) Restarts : 2502 (Average: 86.12 Last: 170) Model-Level : 115.0 Problems : 29 (Average Length: 52.17 Splits: 0) Lemmas : 215481 (Deleted: 196820) Binary : 6004 (Ratio: 2.79%) Ternary : 1741 (Ratio: 0.81%) Conflict : 215481 (Average Length: 441.3 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 215481 (Average: 14.20 Max: 671 Sum: 3059677) Executed : 215385 (Average: 14.19 Max: 671 Sum: 3057115 Ratio: 99.92%) Bounded : 96 (Average: 26.69 Max: 87 Sum: 2562 Ratio: 0.08%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 436900 (Eliminated: 0 Frozen: 139842) Constraints : 3214722 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 558MB Max. Length : 85 steps Models : 1 [endof: stats after solve call] Solving Time: 6.29s Memory: 517MB (+0MB) UNKNOWN Iteration Time: 6.33s Iteration 29 Queue: [(11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] Grounded Until: 85 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 30 Time : 152.466s (Solving: 139.67s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 152.412s Choices : 3523031 (Domain: 3430715) Conflicts : 224460 (Analyzed: 224457) Restarts : 2602 (Average: 86.26 Last: 170) Model-Level : 115.0 Problems : 30 (Average Length: 53.33 Splits: 0) Lemmas : 224457 (Deleted: 205177) Binary : 6136 (Ratio: 2.73%) Ternary : 1758 (Ratio: 0.78%) Conflict : 224457 (Average Length: 442.9 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 224457 (Average: 14.24 Max: 671 Sum: 3195230) Executed : 224361 (Average: 14.22 Max: 671 Sum: 3192668 Ratio: 99.92%) Bounded : 96 (Average: 26.69 Max: 87 Sum: 2562 Ratio: 0.08%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 436900 (Eliminated: 0 Frozen: 139842) Constraints : 3214722 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 558MB Max. Length : 85 steps Models : 1 [endof: stats after solve call] Solving Time: 5.65s Memory: 517MB (+0MB) UNKNOWN Iteration Time: 5.68s Iteration 30 Queue: [(12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] Grounded Until: 85 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 31 Time : 159.614s (Solving: 146.73s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 159.564s Choices : 3763227 (Domain: 3660922) Conflicts : 233518 (Analyzed: 233515) Restarts : 2702 (Average: 86.42 Last: 170) Model-Level : 115.0 Problems : 31 (Average Length: 54.42 Splits: 0) Lemmas : 233515 (Deleted: 213793) Binary : 6399 (Ratio: 2.74%) Ternary : 1833 (Ratio: 0.78%) Conflict : 233515 (Average Length: 451.0 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 233515 (Average: 14.60 Max: 671 Sum: 3408356) Executed : 233419 (Average: 14.58 Max: 671 Sum: 3405794 Ratio: 99.92%) Bounded : 96 (Average: 26.69 Max: 87 Sum: 2562 Ratio: 0.08%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 436900 (Eliminated: 0 Frozen: 139842) Constraints : 3214722 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 558MB Max. Length : 85 steps Models : 1 [endof: stats after solve call] Solving Time: 7.12s Memory: 517MB (+0MB) UNKNOWN Iteration Time: 7.15s Iteration 31 Queue: [(13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] Grounded Until: 85 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 32 Time : 165.808s (Solving: 152.82s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 165.764s Choices : 3968183 (Domain: 3865263) Conflicts : 242078 (Analyzed: 242075) Restarts : 2802 (Average: 86.39 Last: 170) Model-Level : 115.0 Problems : 32 (Average Length: 55.44 Splits: 0) Lemmas : 242075 (Deleted: 220761) Binary : 6554 (Ratio: 2.71%) Ternary : 1852 (Ratio: 0.77%) Conflict : 242075 (Average Length: 453.3 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 242075 (Average: 14.85 Max: 671 Sum: 3593818) Executed : 241979 (Average: 14.84 Max: 671 Sum: 3591256 Ratio: 99.93%) Bounded : 96 (Average: 26.69 Max: 87 Sum: 2562 Ratio: 0.07%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 436900 (Eliminated: 0 Frozen: 139842) Constraints : 3214722 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 558MB Max. Length : 85 steps Models : 1 [endof: stats after solve call] Solving Time: 6.16s Memory: 517MB (+0MB) UNKNOWN Iteration Time: 6.20s Iteration 32 Queue: [(14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] Grounded Until: 85 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 33 Time : 172.520s (Solving: 159.43s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 172.480s Choices : 4167486 (Domain: 4063718) Conflicts : 250408 (Analyzed: 250405) Restarts : 2902 (Average: 86.29 Last: 170) Model-Level : 115.0 Problems : 33 (Average Length: 56.39 Splits: 0) Lemmas : 250405 (Deleted: 228428) Binary : 6708 (Ratio: 2.68%) Ternary : 1869 (Ratio: 0.75%) Conflict : 250405 (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 : 250405 (Average: 15.07 Max: 671 Sum: 3774797) Executed : 250309 (Average: 15.06 Max: 671 Sum: 3772235 Ratio: 99.93%) Bounded : 96 (Average: 26.69 Max: 87 Sum: 2562 Ratio: 0.07%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 436900 (Eliminated: 0 Frozen: 139842) Constraints : 3214722 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 558MB Max. Length : 85 steps Models : 1 [endof: stats after solve call] Solving Time: 6.68s Memory: 517MB (+0MB) UNKNOWN Iteration Time: 6.72s Iteration 33 Queue: [(15,75,1,True), (16,80,1,True), (17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] Grounded Until: 85 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 34 Time : 180.578s (Solving: 167.39s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 180.544s Choices : 4486419 (Domain: 4380037) Conflicts : 259607 (Analyzed: 259604) Restarts : 3002 (Average: 86.48 Last: 170) Model-Level : 115.0 Problems : 34 (Average Length: 57.29 Splits: 0) Lemmas : 259604 (Deleted: 238658) Binary : 6852 (Ratio: 2.64%) Ternary : 1890 (Ratio: 0.73%) Conflict : 259604 (Average Length: 464.1 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 259604 (Average: 15.67 Max: 671 Sum: 4067138) Executed : 259508 (Average: 15.66 Max: 671 Sum: 4064576 Ratio: 99.94%) Bounded : 96 (Average: 26.69 Max: 87 Sum: 2562 Ratio: 0.06%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 436900 (Eliminated: 0 Frozen: 139842) Constraints : 3214722 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 558MB Max. Length : 85 steps Models : 1 [endof: stats after solve call] Solving Time: 8.02s Memory: 517MB (+0MB) UNKNOWN Iteration Time: 8.06s Iteration 34 Queue: [(16,80,1,True), (17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] Grounded Until: 85 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 35 Time : 189.102s (Solving: 175.83s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 189.072s Choices : 4720405 (Domain: 4608522) Conflicts : 268308 (Analyzed: 268305) Restarts : 3102 (Average: 86.49 Last: 170) Model-Level : 115.0 Problems : 35 (Average Length: 58.14 Splits: 0) Lemmas : 268305 (Deleted: 247041) Binary : 7140 (Ratio: 2.66%) Ternary : 1925 (Ratio: 0.72%) Conflict : 268305 (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 : 268305 (Average: 15.92 Max: 671 Sum: 4271683) Executed : 268209 (Average: 15.91 Max: 671 Sum: 4269121 Ratio: 99.94%) Bounded : 96 (Average: 26.69 Max: 87 Sum: 2562 Ratio: 0.06%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 436900 (Eliminated: 0 Frozen: 139842) Constraints : 3214722 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 558MB Max. Length : 85 steps Models : 1 [endof: stats after solve call] Solving Time: 8.50s Memory: 517MB (+0MB) UNKNOWN Iteration Time: 8.53s Iteration 35 Queue: [(17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] Grounded Until: 85 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 36 Time : 197.636s (Solving: 184.27s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 197.608s Choices : 4994690 (Domain: 4881787) Conflicts : 277279 (Analyzed: 277276) Restarts : 3202 (Average: 86.59 Last: 170) Model-Level : 115.0 Problems : 36 (Average Length: 58.94 Splits: 0) Lemmas : 277276 (Deleted: 255140) Binary : 7259 (Ratio: 2.62%) Ternary : 1953 (Ratio: 0.70%) Conflict : 277276 (Average Length: 492.0 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 277276 (Average: 16.31 Max: 671 Sum: 4521069) Executed : 277180 (Average: 16.30 Max: 671 Sum: 4518507 Ratio: 99.94%) Bounded : 96 (Average: 26.69 Max: 87 Sum: 2562 Ratio: 0.06%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 436900 (Eliminated: 0 Frozen: 139842) Constraints : 3214722 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 558MB Max. Length : 85 steps Models : 1 [endof: stats after solve call] Solving Time: 8.51s Memory: 517MB (+0MB) UNKNOWN Iteration Time: 8.54s Iteration 36 Queue: [(18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] Grounded Until: 85 Expected Memory: 565.0MB Grounding... [('step', [86]), ('step', [87]), ('step', [88]), ('step', [89]), ('step', [90]), ('check', [90])] Grounding Time: 0.37s Memory: 517MB (+0MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 37 Time : 208.934s (Solving: 194.79s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 208.908s Choices : 5343023 (Domain: 5228839) Conflicts : 287148 (Analyzed: 287145) Restarts : 3302 (Average: 86.96 Last: 170) Model-Level : 115.0 Problems : 37 (Average Length: 59.84 Splits: 0) Lemmas : 287145 (Deleted: 263928) Binary : 7392 (Ratio: 2.57%) Ternary : 1987 (Ratio: 0.69%) Conflict : 287145 (Average Length: 506.8 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 287145 (Average: 16.85 Max: 671 Sum: 4839070) Executed : 287049 (Average: 16.84 Max: 671 Sum: 4836508 Ratio: 99.95%) Bounded : 96 (Average: 26.69 Max: 87 Sum: 2562 Ratio: 0.05%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 463296 (Eliminated: 0 Frozen: 148382) Constraints : 3415792 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 580MB Max. Length : 85 steps Models : 1 [endof: stats after solve call] Solving Time: 10.62s Memory: 534MB (+17MB) UNKNOWN Iteration Time: 11.31s Iteration 37 Queue: [(19,95,0,True), (20,100,0,True), (21,105,0,True)] Grounded Until: 90 Expected Memory: 582.0MB Grounding... [('step', [91]), ('step', [92]), ('step', [93]), ('step', [94]), ('step', [95]), ('check', [95])] Grounding Time: 0.39s Memory: 534MB (+0MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 38 Time : 218.549s (Solving: 203.58s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 218.528s Choices : 5669012 (Domain: 5553843) Conflicts : 296063 (Analyzed: 296060) Restarts : 3402 (Average: 87.03 Last: 170) Model-Level : 115.0 Problems : 38 (Average Length: 60.82 Splits: 0) Lemmas : 296060 (Deleted: 273205) Binary : 7498 (Ratio: 2.53%) Ternary : 2002 (Ratio: 0.68%) Conflict : 296060 (Average Length: 512.7 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 296060 (Average: 17.35 Max: 671 Sum: 5136959) Executed : 295964 (Average: 17.34 Max: 671 Sum: 5134397 Ratio: 99.95%) Bounded : 96 (Average: 26.69 Max: 87 Sum: 2562 Ratio: 0.05%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 489692 (Eliminated: 0 Frozen: 156922) Constraints : 3616862 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 600MB Max. Length : 90 steps Models : 1 [endof: stats after solve call] Solving Time: 8.89s Memory: 590MB (+56MB) UNKNOWN Iteration Time: 9.63s Iteration 38 Queue: [(20,100,0,True), (21,105,0,True)] Grounded Until: 95 Expected Memory: 646.0MB Grounding... [('step', [96]), ('step', [97]), ('step', [98]), ('step', [99]), ('step', [100]), ('check', [100])] Grounding Time: 0.39s Memory: 590MB (+0MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 39 Time : 229.487s (Solving: 213.68s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 229.468s Choices : 6023692 (Domain: 5903315) Conflicts : 304951 (Analyzed: 304948) Restarts : 3502 (Average: 87.08 Last: 170) Model-Level : 115.0 Problems : 39 (Average Length: 61.87 Splits: 0) Lemmas : 304948 (Deleted: 281699) Binary : 7742 (Ratio: 2.54%) Ternary : 2044 (Ratio: 0.67%) Conflict : 304948 (Average Length: 532.8 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 304948 (Average: 17.88 Max: 804 Sum: 5451933) Executed : 304852 (Average: 17.87 Max: 804 Sum: 5449371 Ratio: 99.95%) Bounded : 96 (Average: 26.69 Max: 87 Sum: 2562 Ratio: 0.05%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 516088 (Eliminated: 0 Frozen: 165462) Constraints : 3817932 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 653MB Max. Length : 95 steps Models : 1 [endof: stats after solve call] Solving Time: 10.21s Memory: 593MB (+3MB) UNKNOWN Iteration Time: 10.95s Iteration 39 Queue: [(21,105,0,True)] Grounded Until: 100 Expected Memory: 649.0MB Grounding... [('step', [101]), ('step', [102]), ('step', [103]), ('step', [104]), ('step', [105]), ('check', [105])] Grounding Time: 0.39s Memory: 593MB (+0MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 40 Time : 240.042s (Solving: 223.38s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 240.024s Choices : 6379244 (Domain: 6257912) Conflicts : 314000 (Analyzed: 313997) Restarts : 3602 (Average: 87.17 Last: 170) Model-Level : 115.0 Problems : 40 (Average Length: 63.00 Splits: 0) Lemmas : 313997 (Deleted: 290078) Binary : 7969 (Ratio: 2.54%) Ternary : 2063 (Ratio: 0.66%) Conflict : 313997 (Average Length: 537.7 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 313997 (Average: 18.40 Max: 804 Sum: 5776888) Executed : 313901 (Average: 18.39 Max: 804 Sum: 5774326 Ratio: 99.96%) Bounded : 96 (Average: 26.69 Max: 87 Sum: 2562 Ratio: 0.04%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 542484 (Eliminated: 0 Frozen: 174002) Constraints : 4019002 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 664MB Max. Length : 100 steps Models : 1 [endof: stats after solve call] Solving Time: 9.80s Memory: 601MB (+8MB) UNKNOWN Iteration Time: 10.56s Iteration 40 Queue: [(4,20,3,True), (5,25,3,True), (6,30,3,True), (7,35,2,True), (8,40,2,True), (9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,2,False), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] Grounded Until: 105 Blocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 41 Time : 243.410s (Solving: 226.62s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 243.396s Choices : 6430841 (Domain: 6309509) Conflicts : 321968 (Analyzed: 321965) Restarts : 3702 (Average: 86.97 Last: 170) Model-Level : 115.0 Problems : 41 (Average Length: 64.07 Splits: 0) Lemmas : 321965 (Deleted: 296652) Binary : 8159 (Ratio: 2.53%) Ternary : 2097 (Ratio: 0.65%) Conflict : 321965 (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 : 321965 (Average: 18.09 Max: 804 Sum: 5822997) Executed : 321869 (Average: 18.08 Max: 804 Sum: 5820435 Ratio: 99.96%) Bounded : 96 (Average: 26.69 Max: 87 Sum: 2562 Ratio: 0.04%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 542484 (Eliminated: 0 Frozen: 174002) Constraints : 4019002 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 664MB Max. Length : 105 steps Models : 1 [endof: stats after solve call] Solving Time: 3.32s Memory: 607MB (+6MB) UNKNOWN Iteration Time: 3.37s Iteration 41 Queue: [(5,25,3,True), (6,30,3,True), (7,35,2,True), (8,40,2,True), (9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,2,False), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] Grounded Until: 105 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 42 Time : 251.218s (Solving: 234.30s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 251.208s Choices : 6495553 (Domain: 6374179) Conflicts : 331081 (Analyzed: 331078) Restarts : 3802 (Average: 87.08 Last: 170) Model-Level : 115.0 Problems : 42 (Average Length: 65.10 Splits: 0) Lemmas : 331078 (Deleted: 306175) Binary : 8297 (Ratio: 2.51%) Ternary : 2135 (Ratio: 0.64%) Conflict : 331078 (Average Length: 542.2 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 331078 (Average: 17.75 Max: 804 Sum: 5876081) Executed : 330981 (Average: 17.74 Max: 804 Sum: 5873416 Ratio: 99.95%) Bounded : 97 (Average: 27.47 Max: 103 Sum: 2665 Ratio: 0.05%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 542484 (Eliminated: 0 Frozen: 174002) Constraints : 4019002 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 664MB Max. Length : 105 steps Models : 1 [endof: stats after solve call] Solving Time: 7.77s Memory: 607MB (+0MB) UNKNOWN Iteration Time: 7.81s Iteration 42 Queue: [(6,30,3,True), (7,35,2,True), (8,40,2,True), (9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,2,False), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] Grounded Until: 105 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 43 Time : 259.001s (Solving: 241.96s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 258.996s Choices : 6594146 (Domain: 6472016) Conflicts : 340237 (Analyzed: 340234) Restarts : 3902 (Average: 87.19 Last: 170) Model-Level : 115.0 Problems : 43 (Average Length: 66.07 Splits: 0) Lemmas : 340234 (Deleted: 315492) Binary : 8513 (Ratio: 2.50%) Ternary : 2196 (Ratio: 0.65%) Conflict : 340234 (Average Length: 558.7 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 340234 (Average: 17.50 Max: 804 Sum: 5954361) Executed : 340137 (Average: 17.49 Max: 804 Sum: 5951696 Ratio: 99.96%) Bounded : 97 (Average: 27.47 Max: 103 Sum: 2665 Ratio: 0.04%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 542484 (Eliminated: 0 Frozen: 174002) Constraints : 4019002 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 664MB Max. Length : 105 steps Models : 1 [endof: stats after solve call] Solving Time: 7.74s Memory: 607MB (+0MB) UNKNOWN Iteration Time: 7.79s Iteration 43 Queue: [(7,35,2,True), (8,40,2,True), (9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,2,False), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] Grounded Until: 105 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 44 Time : 266.714s (Solving: 249.54s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 266.712s Choices : 6710814 (Domain: 6584758) Conflicts : 349303 (Analyzed: 349300) Restarts : 4002 (Average: 87.28 Last: 170) Model-Level : 115.0 Problems : 44 (Average Length: 67.00 Splits: 0) Lemmas : 349300 (Deleted: 323636) Binary : 8739 (Ratio: 2.50%) Ternary : 2291 (Ratio: 0.66%) Conflict : 349300 (Average Length: 564.4 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 349300 (Average: 17.32 Max: 804 Sum: 6050827) Executed : 349203 (Average: 17.32 Max: 804 Sum: 6048162 Ratio: 99.96%) Bounded : 97 (Average: 27.47 Max: 103 Sum: 2665 Ratio: 0.04%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 542484 (Eliminated: 0 Frozen: 174002) Constraints : 4019002 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 664MB Max. Length : 105 steps Models : 1 [endof: stats after solve call] Solving Time: 7.67s Memory: 607MB (+0MB) UNKNOWN Iteration Time: 7.72s Iteration 44 Queue: [(8,40,2,True), (9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,2,False), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] Grounded Until: 105 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 45 Time : 274.357s (Solving: 257.07s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 274.356s Choices : 6830088 (Domain: 6703845) Conflicts : 358717 (Analyzed: 358714) Restarts : 4102 (Average: 87.45 Last: 170) Model-Level : 115.0 Problems : 45 (Average Length: 67.89 Splits: 0) Lemmas : 358714 (Deleted: 332178) Binary : 8867 (Ratio: 2.47%) Ternary : 2311 (Ratio: 0.64%) Conflict : 358714 (Average Length: 566.4 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 358714 (Average: 17.15 Max: 804 Sum: 6150549) Executed : 358617 (Average: 17.14 Max: 804 Sum: 6147884 Ratio: 99.96%) Bounded : 97 (Average: 27.47 Max: 103 Sum: 2665 Ratio: 0.04%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 542484 (Eliminated: 0 Frozen: 174002) Constraints : 4019002 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 664MB Max. Length : 105 steps Models : 1 [endof: stats after solve call] Solving Time: 7.61s Memory: 607MB (+0MB) UNKNOWN Iteration Time: 7.65s Iteration 45 Queue: [(9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,2,False), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] Grounded Until: 105 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 46 Time : 281.607s (Solving: 264.20s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 281.612s Choices : 6925774 (Domain: 6799473) Conflicts : 368019 (Analyzed: 368016) Restarts : 4202 (Average: 87.58 Last: 170) Model-Level : 115.0 Problems : 46 (Average Length: 68.74 Splits: 0) Lemmas : 368016 (Deleted: 341260) Binary : 8922 (Ratio: 2.42%) Ternary : 2321 (Ratio: 0.63%) Conflict : 368016 (Average Length: 570.0 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 368016 (Average: 16.92 Max: 804 Sum: 6226794) Executed : 367919 (Average: 16.91 Max: 804 Sum: 6224129 Ratio: 99.96%) Bounded : 97 (Average: 27.47 Max: 103 Sum: 2665 Ratio: 0.04%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 542484 (Eliminated: 0 Frozen: 174002) Constraints : 4019002 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 664MB Max. Length : 105 steps Models : 1 [endof: stats after solve call] Solving Time: 7.21s Memory: 607MB (+0MB) UNKNOWN Iteration Time: 7.26s Iteration 46 Queue: [(10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,2,False), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] Grounded Until: 105 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 47 Time : 289.739s (Solving: 272.19s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 289.748s Choices : 7038639 (Domain: 6911918) Conflicts : 377264 (Analyzed: 377261) Restarts : 4302 (Average: 87.69 Last: 170) Model-Level : 115.0 Problems : 47 (Average Length: 69.55 Splits: 0) Lemmas : 377261 (Deleted: 350265) Binary : 8987 (Ratio: 2.38%) Ternary : 2340 (Ratio: 0.62%) Conflict : 377261 (Average Length: 574.5 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 377261 (Average: 16.75 Max: 804 Sum: 6318417) Executed : 377164 (Average: 16.74 Max: 804 Sum: 6315752 Ratio: 99.96%) Bounded : 97 (Average: 27.47 Max: 103 Sum: 2665 Ratio: 0.04%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 542484 (Eliminated: 0 Frozen: 174002) Constraints : 4019002 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 664MB Max. Length : 105 steps Models : 1 [endof: stats after solve call] Solving Time: 8.08s Memory: 607MB (+0MB) UNKNOWN Iteration Time: 8.14s Iteration 47 Queue: [(11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,2,False), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] Grounded Until: 105 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 48 Time : 297.757s (Solving: 280.06s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 297.768s Choices : 7160939 (Domain: 7033822) Conflicts : 386539 (Analyzed: 386536) Restarts : 4402 (Average: 87.81 Last: 170) Model-Level : 115.0 Problems : 48 (Average Length: 70.33 Splits: 0) Lemmas : 386536 (Deleted: 359257) Binary : 9080 (Ratio: 2.35%) Ternary : 2363 (Ratio: 0.61%) Conflict : 386536 (Average Length: 580.4 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 386536 (Average: 16.60 Max: 804 Sum: 6417714) Executed : 386439 (Average: 16.60 Max: 804 Sum: 6415049 Ratio: 99.96%) Bounded : 97 (Average: 27.47 Max: 103 Sum: 2665 Ratio: 0.04%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 542484 (Eliminated: 0 Frozen: 174002) Constraints : 4019002 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 664MB Max. Length : 105 steps Models : 1 [endof: stats after solve call] Solving Time: 7.97s Memory: 607MB (+0MB) UNKNOWN Iteration Time: 8.02s Iteration 48 Queue: [(12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,2,False), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] Grounded Until: 105 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 49 Time : 305.694s (Solving: 287.89s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 305.708s Choices : 7303106 (Domain: 7175841) Conflicts : 395708 (Analyzed: 395705) Restarts : 4502 (Average: 87.90 Last: 170) Model-Level : 115.0 Problems : 49 (Average Length: 71.08 Splits: 0) Lemmas : 395705 (Deleted: 368259) Binary : 9116 (Ratio: 2.30%) Ternary : 2370 (Ratio: 0.60%) Conflict : 395705 (Average Length: 583.1 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 395705 (Average: 16.52 Max: 804 Sum: 6537132) Executed : 395608 (Average: 16.51 Max: 804 Sum: 6534467 Ratio: 99.96%) Bounded : 97 (Average: 27.47 Max: 103 Sum: 2665 Ratio: 0.04%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 542484 (Eliminated: 0 Frozen: 174002) Constraints : 4019002 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 664MB Max. Length : 105 steps Models : 1 [endof: stats after solve call] Solving Time: 7.90s Memory: 607MB (+0MB) UNKNOWN Iteration Time: 7.94s Iteration 49 Queue: [(13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,2,False), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] Grounded Until: 105 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 50 Time : 313.828s (Solving: 295.89s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 313.844s Choices : 7504335 (Domain: 7375013) Conflicts : 404707 (Analyzed: 404704) Restarts : 4602 (Average: 87.94 Last: 170) Model-Level : 115.0 Problems : 50 (Average Length: 71.80 Splits: 0) Lemmas : 404704 (Deleted: 377119) Binary : 9336 (Ratio: 2.31%) Ternary : 2454 (Ratio: 0.61%) Conflict : 404704 (Average Length: 585.9 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 404704 (Average: 16.58 Max: 804 Sum: 6709035) Executed : 404607 (Average: 16.57 Max: 804 Sum: 6706370 Ratio: 99.96%) Bounded : 97 (Average: 27.47 Max: 103 Sum: 2665 Ratio: 0.04%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 542484 (Eliminated: 0 Frozen: 174002) Constraints : 4019002 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 664MB Max. Length : 105 steps Models : 1 [endof: stats after solve call] Solving Time: 8.09s Memory: 607MB (+0MB) UNKNOWN Iteration Time: 8.14s Iteration 50 Queue: [(18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] Grounded Until: 105 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 51 Time : 322.691s (Solving: 304.63s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 322.700s Choices : 7621989 (Domain: 7492407) Conflicts : 413223 (Analyzed: 413220) Restarts : 4702 (Average: 87.88 Last: 170) Model-Level : 115.0 Problems : 51 (Average Length: 72.49 Splits: 0) Lemmas : 413220 (Deleted: 384332) Binary : 9393 (Ratio: 2.27%) Ternary : 2460 (Ratio: 0.60%) Conflict : 413220 (Average Length: 597.4 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 413220 (Average: 16.45 Max: 804 Sum: 6795908) Executed : 413123 (Average: 16.44 Max: 804 Sum: 6793243 Ratio: 99.96%) Bounded : 97 (Average: 27.47 Max: 103 Sum: 2665 Ratio: 0.04%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 542484 (Eliminated: 0 Frozen: 174002) Constraints : 4019002 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 664MB Max. Length : 105 steps Models : 1 [endof: stats after solve call] Solving Time: 8.81s Memory: 607MB (+0MB) UNKNOWN Iteration Time: 8.86s Iteration 51 Queue: [(19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] Grounded Until: 105 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 52 Time : 331.604s (Solving: 313.40s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 331.616s Choices : 7799647 (Domain: 7669964) Conflicts : 422499 (Analyzed: 422496) Restarts : 4802 (Average: 87.98 Last: 170) Model-Level : 115.0 Problems : 52 (Average Length: 73.15 Splits: 0) Lemmas : 422496 (Deleted: 394032) Binary : 9435 (Ratio: 2.23%) Ternary : 2470 (Ratio: 0.58%) Conflict : 422496 (Average Length: 599.9 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 422496 (Average: 16.43 Max: 804 Sum: 6943636) Executed : 422399 (Average: 16.43 Max: 804 Sum: 6940971 Ratio: 99.96%) Bounded : 97 (Average: 27.47 Max: 103 Sum: 2665 Ratio: 0.04%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 542484 (Eliminated: 0 Frozen: 174002) Constraints : 4019002 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 664MB Max. Length : 105 steps Models : 1 [endof: stats after solve call] Solving Time: 8.86s Memory: 607MB (+0MB) UNKNOWN Iteration Time: 8.92s Iteration 52 Queue: [(20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] Grounded Until: 105 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 53 Time : 341.232s (Solving: 322.92s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 341.248s Choices : 7985443 (Domain: 7854970) Conflicts : 431998 (Analyzed: 431995) Restarts : 4902 (Average: 88.13 Last: 170) Model-Level : 115.0 Problems : 53 (Average Length: 73.79 Splits: 0) Lemmas : 431995 (Deleted: 403120) Binary : 9499 (Ratio: 2.20%) Ternary : 2479 (Ratio: 0.57%) Conflict : 431995 (Average Length: 604.5 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 431995 (Average: 16.42 Max: 804 Sum: 7094388) Executed : 431898 (Average: 16.42 Max: 804 Sum: 7091723 Ratio: 99.96%) Bounded : 97 (Average: 27.47 Max: 103 Sum: 2665 Ratio: 0.04%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 542484 (Eliminated: 0 Frozen: 174002) Constraints : 4019002 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 664MB Max. Length : 105 steps Models : 1 [endof: stats after solve call] Solving Time: 9.59s Memory: 607MB (+0MB) UNKNOWN Iteration Time: 9.64s Iteration 53 Queue: [(21,105,1,True), (22,110,0,True), (23,115,0,True)] Grounded Until: 105 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 54 Time : 350.764s (Solving: 332.33s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 350.784s Choices : 8163807 (Domain: 8032808) Conflicts : 441246 (Analyzed: 441243) Restarts : 5002 (Average: 88.21 Last: 170) Model-Level : 115.0 Problems : 54 (Average Length: 74.41 Splits: 0) Lemmas : 441243 (Deleted: 412313) Binary : 9593 (Ratio: 2.17%) Ternary : 2505 (Ratio: 0.57%) Conflict : 441243 (Average Length: 606.9 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 441243 (Average: 16.41 Max: 804 Sum: 7239497) Executed : 441146 (Average: 16.40 Max: 804 Sum: 7236832 Ratio: 99.96%) Bounded : 97 (Average: 27.47 Max: 103 Sum: 2665 Ratio: 0.04%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 542484 (Eliminated: 0 Frozen: 174002) Constraints : 4019002 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 664MB Max. Length : 105 steps Models : 1 [endof: stats after solve call] Solving Time: 9.49s Memory: 607MB (+0MB) UNKNOWN Iteration Time: 9.54s Iteration 54 Queue: [(22,110,0,True), (23,115,0,True)] Grounded Until: 105 Expected Memory: 663.0MB Grounding... [('step', [106]), ('step', [107]), ('step', [108]), ('step', [109]), ('step', [110]), ('check', [110])] Grounding Time: 0.38s Memory: 607MB (+0MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 55 Time : 360.243s (Solving: 340.96s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 360.268s Choices : 8299406 (Domain: 8168390) Conflicts : 450657 (Analyzed: 450654) Restarts : 5102 (Average: 88.33 Last: 170) Model-Level : 115.0 Problems : 55 (Average Length: 75.09 Splits: 0) Lemmas : 450654 (Deleted: 421286) Binary : 9645 (Ratio: 2.14%) Ternary : 2509 (Ratio: 0.56%) Conflict : 450654 (Average Length: 609.2 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 450654 (Average: 16.30 Max: 804 Sum: 7343702) Executed : 450557 (Average: 16.29 Max: 804 Sum: 7341037 Ratio: 99.96%) Bounded : 97 (Average: 27.47 Max: 103 Sum: 2665 Ratio: 0.04%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 568880 (Eliminated: 0 Frozen: 182542) Constraints : 4220072 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 680MB Max. Length : 105 steps Models : 1 [endof: stats after solve call] Solving Time: 8.74s Memory: 621MB (+14MB) UNKNOWN Iteration Time: 9.49s Iteration 55 Queue: [(23,115,0,True)] Grounded Until: 110 Expected Memory: 677.0MB Grounding... [('step', [111]), ('step', [112]), ('step', [113]), ('step', [114]), ('step', [115]), ('check', [115])] Grounding Time: 0.38s Memory: 621MB (+0MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 56 Time : 371.728s (Solving: 351.59s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 371.760s Choices : 8452358 (Domain: 8321303) Conflicts : 460582 (Analyzed: 460579) Restarts : 5202 (Average: 88.54 Last: 170) Model-Level : 115.0 Problems : 56 (Average Length: 75.84 Splits: 0) Lemmas : 460579 (Deleted: 430544) Binary : 9673 (Ratio: 2.10%) Ternary : 2521 (Ratio: 0.55%) Conflict : 460579 (Average Length: 613.2 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 460579 (Average: 16.20 Max: 804 Sum: 7460145) Executed : 460482 (Average: 16.19 Max: 804 Sum: 7457480 Ratio: 99.96%) Bounded : 97 (Average: 27.47 Max: 103 Sum: 2665 Ratio: 0.04%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 595276 (Eliminated: 0 Frozen: 191082) Constraints : 4421142 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 706MB Max. Length : 110 steps Models : 1 [endof: stats after solve call] Solving Time: 10.74s Memory: 637MB (+16MB) UNKNOWN Iteration Time: 11.50s Iteration 56 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,2,False), (22,110,1,True), (23,115,1,True)] Grounded Until: 115 Blocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 57 Time : 374.767s (Solving: 354.48s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 374.796s Choices : 8496233 (Domain: 8365178) Conflicts : 468049 (Analyzed: 468046) Restarts : 5302 (Average: 88.28 Last: 170) Model-Level : 115.0 Problems : 57 (Average Length: 76.56 Splits: 0) Lemmas : 468046 (Deleted: 438008) Binary : 9722 (Ratio: 2.08%) Ternary : 2533 (Ratio: 0.54%) Conflict : 468046 (Average Length: 607.5 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 468046 (Average: 16.02 Max: 804 Sum: 7496619) Executed : 467948 (Average: 16.01 Max: 804 Sum: 7493837 Ratio: 99.96%) Bounded : 98 (Average: 28.39 Max: 117 Sum: 2782 Ratio: 0.04%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 595276 (Eliminated: 0 Frozen: 191082) Constraints : 4421142 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 706MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 2.99s Memory: 637MB (+0MB) UNKNOWN Iteration Time: 3.04s Iteration 57 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,2,False), (22,110,1,True), (23,115,1,True)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 58 Time : 383.726s (Solving: 363.31s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 383.760s Choices : 8542421 (Domain: 8411366) Conflicts : 476684 (Analyzed: 476681) Restarts : 5402 (Average: 88.24 Last: 170) Model-Level : 115.0 Problems : 58 (Average Length: 77.26 Splits: 0) Lemmas : 476681 (Deleted: 447362) Binary : 9760 (Ratio: 2.05%) Ternary : 2544 (Ratio: 0.53%) Conflict : 476681 (Average Length: 617.1 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 476681 (Average: 15.80 Max: 804 Sum: 7529934) Executed : 476583 (Average: 15.79 Max: 804 Sum: 7527152 Ratio: 99.96%) Bounded : 98 (Average: 28.39 Max: 117 Sum: 2782 Ratio: 0.04%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 595276 (Eliminated: 0 Frozen: 191082) Constraints : 4421128 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 706MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 8.92s Memory: 637MB (+0MB) UNKNOWN Iteration Time: 8.97s Iteration 58 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,2,False), (22,110,1,True), (23,115,1,True)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 59 Time : 391.228s (Solving: 370.68s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 391.264s Choices : 8618700 (Domain: 8487645) Conflicts : 485737 (Analyzed: 485734) Restarts : 5502 (Average: 88.28 Last: 170) Model-Level : 115.0 Problems : 59 (Average Length: 77.93 Splits: 0) Lemmas : 485734 (Deleted: 455742) Binary : 9883 (Ratio: 2.03%) Ternary : 2566 (Ratio: 0.53%) Conflict : 485734 (Average Length: 621.4 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 485734 (Average: 15.62 Max: 804 Sum: 7587479) Executed : 485636 (Average: 15.61 Max: 804 Sum: 7584697 Ratio: 99.96%) Bounded : 98 (Average: 28.39 Max: 117 Sum: 2782 Ratio: 0.04%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 595276 (Eliminated: 0 Frozen: 191082) Constraints : 4421128 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 706MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 7.46s Memory: 637MB (+0MB) UNKNOWN Iteration Time: 7.51s Iteration 59 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,2,False), (22,110,1,True), (23,115,1,True)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 60 Time : 398.492s (Solving: 377.82s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 398.532s Choices : 8689250 (Domain: 8557293) Conflicts : 494574 (Analyzed: 494571) Restarts : 5602 (Average: 88.28 Last: 170) Model-Level : 115.0 Problems : 60 (Average Length: 78.58 Splits: 0) Lemmas : 494571 (Deleted: 464538) Binary : 9965 (Ratio: 2.01%) Ternary : 2573 (Ratio: 0.52%) Conflict : 494571 (Average Length: 625.1 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 494571 (Average: 15.44 Max: 804 Sum: 7637879) Executed : 494473 (Average: 15.44 Max: 804 Sum: 7635097 Ratio: 99.96%) Bounded : 98 (Average: 28.39 Max: 117 Sum: 2782 Ratio: 0.04%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 595276 (Eliminated: 0 Frozen: 191082) Constraints : 4421128 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 706MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 7.23s Memory: 637MB (+0MB) UNKNOWN Iteration Time: 7.27s Iteration 60 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,2,False), (22,110,1,True), (23,115,1,True)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 61 Time : 405.756s (Solving: 384.97s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 405.800s Choices : 8797588 (Domain: 8660669) Conflicts : 503822 (Analyzed: 503819) Restarts : 5702 (Average: 88.36 Last: 170) Model-Level : 115.0 Problems : 61 (Average Length: 79.21 Splits: 0) Lemmas : 503819 (Deleted: 472749) Binary : 10220 (Ratio: 2.03%) Ternary : 2595 (Ratio: 0.52%) Conflict : 503819 (Average Length: 627.7 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 503819 (Average: 15.32 Max: 804 Sum: 7718391) Executed : 503721 (Average: 15.31 Max: 804 Sum: 7715609 Ratio: 99.96%) Bounded : 98 (Average: 28.39 Max: 117 Sum: 2782 Ratio: 0.04%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 595276 (Eliminated: 0 Frozen: 191082) Constraints : 4421128 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 706MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 7.23s Memory: 637MB (+0MB) UNKNOWN Iteration Time: 7.27s Iteration 61 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,2,False), (22,110,1,True), (23,115,1,True)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 62 Time : 413.314s (Solving: 392.40s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 413.360s Choices : 8880447 (Domain: 8743518) Conflicts : 512942 (Analyzed: 512939) Restarts : 5802 (Average: 88.41 Last: 170) Model-Level : 115.0 Problems : 62 (Average Length: 79.82 Splits: 0) Lemmas : 512939 (Deleted: 481710) Binary : 10279 (Ratio: 2.00%) Ternary : 2607 (Ratio: 0.51%) Conflict : 512939 (Average Length: 632.2 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 512939 (Average: 15.17 Max: 804 Sum: 7780418) Executed : 512841 (Average: 15.16 Max: 804 Sum: 7777636 Ratio: 99.96%) Bounded : 98 (Average: 28.39 Max: 117 Sum: 2782 Ratio: 0.04%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 595276 (Eliminated: 0 Frozen: 191082) Constraints : 4421128 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 706MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 7.52s Memory: 637MB (+0MB) UNKNOWN Iteration Time: 7.56s Iteration 62 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,2,False), (22,110,1,True), (23,115,1,True)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 63 Time : 420.951s (Solving: 399.89s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 421.000s Choices : 8967467 (Domain: 8830526) Conflicts : 522172 (Analyzed: 522169) Restarts : 5902 (Average: 88.47 Last: 170) Model-Level : 115.0 Problems : 63 (Average Length: 80.41 Splits: 0) Lemmas : 522169 (Deleted: 490655) Binary : 10305 (Ratio: 1.97%) Ternary : 2609 (Ratio: 0.50%) Conflict : 522169 (Average Length: 632.9 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 522169 (Average: 15.03 Max: 804 Sum: 7846405) Executed : 522071 (Average: 15.02 Max: 804 Sum: 7843623 Ratio: 99.96%) Bounded : 98 (Average: 28.39 Max: 117 Sum: 2782 Ratio: 0.04%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 595276 (Eliminated: 0 Frozen: 191082) Constraints : 4421128 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 706MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 7.58s Memory: 637MB (+0MB) UNKNOWN Iteration Time: 7.64s Iteration 63 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,2,False), (22,110,1,True), (23,115,1,True)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 64 Time : 429.223s (Solving: 408.02s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 429.276s Choices : 9059058 (Domain: 8922095) Conflicts : 531500 (Analyzed: 531497) Restarts : 6002 (Average: 88.55 Last: 170) Model-Level : 115.0 Problems : 64 (Average Length: 80.98 Splits: 0) Lemmas : 531497 (Deleted: 499685) Binary : 10323 (Ratio: 1.94%) Ternary : 2611 (Ratio: 0.49%) Conflict : 531497 (Average Length: 634.4 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 531497 (Average: 14.89 Max: 804 Sum: 7913250) Executed : 531399 (Average: 14.88 Max: 804 Sum: 7910468 Ratio: 99.96%) Bounded : 98 (Average: 28.39 Max: 117 Sum: 2782 Ratio: 0.04%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 595276 (Eliminated: 0 Frozen: 191082) Constraints : 4421128 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 706MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 8.22s Memory: 637MB (+0MB) UNKNOWN Iteration Time: 8.28s Iteration 64 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,2,False), (22,110,1,True), (23,115,1,True)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 65 Time : 437.536s (Solving: 416.21s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 437.592s Choices : 9153270 (Domain: 9016300) Conflicts : 540952 (Analyzed: 540949) Restarts : 6102 (Average: 88.65 Last: 172) Model-Level : 115.0 Problems : 65 (Average Length: 81.54 Splits: 0) Lemmas : 540949 (Deleted: 508794) Binary : 10347 (Ratio: 1.91%) Ternary : 2614 (Ratio: 0.48%) Conflict : 540949 (Average Length: 636.4 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 540949 (Average: 14.75 Max: 804 Sum: 7981558) Executed : 540851 (Average: 14.75 Max: 804 Sum: 7978776 Ratio: 99.97%) Bounded : 98 (Average: 28.39 Max: 117 Sum: 2782 Ratio: 0.03%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 595276 (Eliminated: 0 Frozen: 191082) Constraints : 4421128 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 706MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 8.27s Memory: 637MB (+0MB) UNKNOWN Iteration Time: 8.32s Iteration 65 Queue: [(22,110,1,True), (23,115,1,True)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 66 Time : 447.483s (Solving: 426.01s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 447.540s Choices : 9264003 (Domain: 9126961) Conflicts : 550781 (Analyzed: 550778) Restarts : 6202 (Average: 88.81 Last: 172) Model-Level : 115.0 Problems : 66 (Average Length: 82.08 Splits: 0) Lemmas : 550778 (Deleted: 518071) Binary : 10367 (Ratio: 1.88%) Ternary : 2621 (Ratio: 0.48%) Conflict : 550778 (Average Length: 640.3 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 550778 (Average: 14.63 Max: 804 Sum: 8058202) Executed : 550680 (Average: 14.63 Max: 804 Sum: 8055420 Ratio: 99.97%) Bounded : 98 (Average: 28.39 Max: 117 Sum: 2782 Ratio: 0.03%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 595276 (Eliminated: 0 Frozen: 191082) Constraints : 4421128 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 706MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 9.90s Memory: 637MB (+0MB) UNKNOWN Iteration Time: 9.95s Iteration 66 Queue: [(23,115,1,True)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 67 Time : 456.370s (Solving: 434.76s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 456.432s Choices : 9380536 (Domain: 9243485) Conflicts : 560063 (Analyzed: 560060) Restarts : 6302 (Average: 88.87 Last: 172) Model-Level : 115.0 Problems : 67 (Average Length: 82.60 Splits: 0) Lemmas : 560060 (Deleted: 527755) Binary : 10416 (Ratio: 1.86%) Ternary : 2622 (Ratio: 0.47%) Conflict : 560060 (Average Length: 642.7 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 560060 (Average: 14.54 Max: 804 Sum: 8141773) Executed : 559962 (Average: 14.53 Max: 804 Sum: 8138991 Ratio: 99.97%) Bounded : 98 (Average: 28.39 Max: 117 Sum: 2782 Ratio: 0.03%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 595276 (Eliminated: 0 Frozen: 191082) Constraints : 4421128 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 706MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 8.84s Memory: 637MB (+0MB) UNKNOWN Iteration Time: 8.89s Iteration 67 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 : 68 Time : 459.552s (Solving: 437.79s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 459.616s Choices : 9434154 (Domain: 9297103) Conflicts : 567639 (Analyzed: 567636) Restarts : 6402 (Average: 88.67 Last: 172) Model-Level : 115.0 Problems : 68 (Average Length: 83.10 Splits: 0) Lemmas : 567636 (Deleted: 534523) Binary : 10500 (Ratio: 1.85%) Ternary : 2643 (Ratio: 0.47%) Conflict : 567636 (Average Length: 637.7 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 567636 (Average: 14.43 Max: 804 Sum: 8190438) Executed : 567535 (Average: 14.42 Max: 804 Sum: 8187305 Ratio: 99.96%) Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.04%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 595276 (Eliminated: 0 Frozen: 191082) Constraints : 4421128 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 706MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 3.13s Memory: 637MB (+0MB) UNKNOWN Iteration Time: 3.19s Iteration 68 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 : 69 Time : 470.051s (Solving: 448.16s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 470.116s Choices : 9482131 (Domain: 9345080) Conflicts : 576664 (Analyzed: 576661) Restarts : 6502 (Average: 88.69 Last: 172) Model-Level : 115.0 Problems : 69 (Average Length: 83.59 Splits: 0) Lemmas : 576661 (Deleted: 543859) Binary : 10552 (Ratio: 1.83%) Ternary : 2651 (Ratio: 0.46%) Conflict : 576661 (Average Length: 650.6 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 576661 (Average: 14.26 Max: 804 Sum: 8224004) Executed : 576560 (Average: 14.26 Max: 804 Sum: 8220871 Ratio: 99.96%) Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.04%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 595276 (Eliminated: 0 Frozen: 191082) Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 765MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 10.45s Memory: 701MB (+64MB) UNKNOWN Iteration Time: 10.51s Iteration 69 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 : 70 Time : 476.594s (Solving: 454.55s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 476.660s Choices : 9557144 (Domain: 9420093) Conflicts : 585502 (Analyzed: 585499) Restarts : 6602 (Average: 88.69 Last: 172) Model-Level : 115.0 Problems : 70 (Average Length: 84.07 Splits: 0) Lemmas : 585499 (Deleted: 552610) Binary : 10648 (Ratio: 1.82%) Ternary : 2662 (Ratio: 0.45%) Conflict : 585499 (Average Length: 653.3 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 585499 (Average: 14.14 Max: 804 Sum: 8280709) Executed : 585398 (Average: 14.14 Max: 804 Sum: 8277576 Ratio: 99.96%) Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.04%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 595276 (Eliminated: 0 Frozen: 191082) Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 765MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 6.49s Memory: 701MB (+0MB) UNKNOWN Iteration Time: 6.55s Iteration 70 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 : 71 Time : 484.082s (Solving: 461.92s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 484.152s Choices : 9635294 (Domain: 9497946) Conflicts : 595789 (Analyzed: 595786) Restarts : 6702 (Average: 88.90 Last: 172) Model-Level : 115.0 Problems : 71 (Average Length: 84.54 Splits: 0) Lemmas : 595786 (Deleted: 561289) Binary : 10713 (Ratio: 1.80%) Ternary : 2669 (Ratio: 0.45%) Conflict : 595786 (Average Length: 653.8 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 595786 (Average: 14.00 Max: 804 Sum: 8340737) Executed : 595685 (Average: 13.99 Max: 804 Sum: 8337604 Ratio: 99.96%) Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.04%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 595276 (Eliminated: 0 Frozen: 191082) Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 765MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 7.45s Memory: 701MB (+0MB) UNKNOWN Iteration Time: 7.49s Iteration 71 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 : 72 Time : 491.756s (Solving: 469.45s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 491.828s Choices : 9707894 (Domain: 9570482) Conflicts : 605018 (Analyzed: 605015) Restarts : 6802 (Average: 88.95 Last: 172) Model-Level : 115.0 Problems : 72 (Average Length: 84.99 Splits: 0) Lemmas : 605015 (Deleted: 571311) Binary : 10761 (Ratio: 1.78%) Ternary : 2675 (Ratio: 0.44%) Conflict : 605015 (Average Length: 657.2 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 605015 (Average: 13.87 Max: 804 Sum: 8391385) Executed : 604914 (Average: 13.86 Max: 804 Sum: 8388252 Ratio: 99.96%) Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.04%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 595276 (Eliminated: 0 Frozen: 191082) Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 765MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 7.63s Memory: 701MB (+0MB) UNKNOWN Iteration Time: 7.68s Iteration 72 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 : 73 Time : 499.479s (Solving: 477.02s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 499.552s Choices : 9782772 (Domain: 9645348) Conflicts : 615176 (Analyzed: 615173) Restarts : 6902 (Average: 89.13 Last: 172) Model-Level : 115.0 Problems : 73 (Average Length: 85.42 Splits: 0) Lemmas : 615173 (Deleted: 580367) Binary : 10788 (Ratio: 1.75%) Ternary : 2675 (Ratio: 0.43%) Conflict : 615173 (Average Length: 657.4 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 615173 (Average: 13.73 Max: 804 Sum: 8445699) Executed : 615072 (Average: 13.72 Max: 804 Sum: 8442566 Ratio: 99.96%) Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.04%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 595276 (Eliminated: 0 Frozen: 191082) Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 765MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 7.67s Memory: 701MB (+0MB) UNKNOWN Iteration Time: 7.73s Iteration 73 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 : 74 Time : 507.094s (Solving: 484.51s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 507.168s Choices : 9855687 (Domain: 9718221) Conflicts : 624144 (Analyzed: 624141) Restarts : 7002 (Average: 89.14 Last: 172) Model-Level : 115.0 Problems : 74 (Average Length: 85.85 Splits: 0) Lemmas : 624141 (Deleted: 590302) Binary : 10814 (Ratio: 1.73%) Ternary : 2685 (Ratio: 0.43%) Conflict : 624141 (Average Length: 660.6 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 624141 (Average: 13.61 Max: 804 Sum: 8495389) Executed : 624040 (Average: 13.61 Max: 804 Sum: 8492256 Ratio: 99.96%) Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.04%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 595276 (Eliminated: 0 Frozen: 191082) Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 765MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 7.58s Memory: 701MB (+0MB) UNKNOWN Iteration Time: 7.62s Iteration 74 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 : 75 Time : 514.984s (Solving: 492.28s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 515.060s Choices : 9923181 (Domain: 9785715) Conflicts : 633437 (Analyzed: 633434) Restarts : 7102 (Average: 89.19 Last: 172) Model-Level : 115.0 Problems : 75 (Average Length: 86.27 Splits: 0) Lemmas : 633434 (Deleted: 599117) Binary : 10832 (Ratio: 1.71%) Ternary : 2689 (Ratio: 0.42%) Conflict : 633434 (Average Length: 663.0 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 633434 (Average: 13.48 Max: 804 Sum: 8537864) Executed : 633333 (Average: 13.47 Max: 804 Sum: 8534731 Ratio: 99.96%) Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.04%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 595276 (Eliminated: 0 Frozen: 191082) Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 765MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 7.85s Memory: 701MB (+0MB) UNKNOWN Iteration Time: 7.90s Iteration 75 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 : 76 Time : 523.361s (Solving: 500.52s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 523.440s Choices : 10023275 (Domain: 9885660) Conflicts : 643207 (Analyzed: 643204) Restarts : 7202 (Average: 89.31 Last: 172) Model-Level : 115.0 Problems : 76 (Average Length: 86.67 Splits: 0) Lemmas : 643204 (Deleted: 608177) Binary : 10876 (Ratio: 1.69%) Ternary : 2695 (Ratio: 0.42%) Conflict : 643204 (Average Length: 665.3 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 643204 (Average: 13.38 Max: 804 Sum: 8609242) Executed : 643103 (Average: 13.38 Max: 804 Sum: 8606109 Ratio: 99.96%) Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.04%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 595276 (Eliminated: 0 Frozen: 191082) Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 765MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 8.33s Memory: 701MB (+0MB) UNKNOWN Iteration Time: 8.38s Iteration 76 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 : 77 Time : 531.762s (Solving: 508.78s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 531.844s Choices : 10107051 (Domain: 9969435) Conflicts : 652228 (Analyzed: 652225) Restarts : 7302 (Average: 89.32 Last: 172) Model-Level : 115.0 Problems : 77 (Average Length: 87.06 Splits: 0) Lemmas : 652225 (Deleted: 617783) Binary : 10887 (Ratio: 1.67%) Ternary : 2699 (Ratio: 0.41%) Conflict : 652225 (Average Length: 669.3 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 652225 (Average: 13.29 Max: 804 Sum: 8665447) Executed : 652124 (Average: 13.28 Max: 804 Sum: 8662314 Ratio: 99.96%) Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.04%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 595276 (Eliminated: 0 Frozen: 191082) Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 765MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 8.35s Memory: 701MB (+0MB) UNKNOWN Iteration Time: 8.41s Iteration 77 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 : 78 Time : 534.891s (Solving: 511.78s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 534.972s Choices : 10158302 (Domain: 10020686) Conflicts : 659798 (Analyzed: 659795) Restarts : 7402 (Average: 89.14 Last: 172) Model-Level : 115.0 Problems : 78 (Average Length: 87.45 Splits: 0) Lemmas : 659795 (Deleted: 624374) Binary : 10965 (Ratio: 1.66%) Ternary : 2706 (Ratio: 0.41%) Conflict : 659795 (Average Length: 663.9 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 659795 (Average: 13.19 Max: 804 Sum: 8702473) Executed : 659694 (Average: 13.18 Max: 804 Sum: 8699340 Ratio: 99.96%) Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.04%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 595276 (Eliminated: 0 Frozen: 191082) Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 765MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 3.08s Memory: 701MB (+0MB) UNKNOWN Iteration Time: 3.13s Iteration 78 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 : 79 Time : 544.334s (Solving: 521.10s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 544.420s Choices : 10197256 (Domain: 10059640) Conflicts : 667894 (Analyzed: 667891) Restarts : 7502 (Average: 89.03 Last: 172) Model-Level : 115.0 Problems : 79 (Average Length: 87.82 Splits: 0) Lemmas : 667891 (Deleted: 631853) Binary : 10983 (Ratio: 1.64%) Ternary : 2717 (Ratio: 0.41%) Conflict : 667891 (Average Length: 675.0 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 667891 (Average: 13.07 Max: 804 Sum: 8731224) Executed : 667790 (Average: 13.07 Max: 804 Sum: 8728091 Ratio: 99.96%) Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.04%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 595276 (Eliminated: 0 Frozen: 191082) Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 765MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 9.41s Memory: 701MB (+0MB) UNKNOWN Iteration Time: 9.45s Iteration 79 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 : 80 Time : 552.480s (Solving: 529.09s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 552.568s Choices : 10271487 (Domain: 10133871) Conflicts : 676239 (Analyzed: 676236) Restarts : 7602 (Average: 88.96 Last: 172) Model-Level : 115.0 Problems : 80 (Average Length: 88.19 Splits: 0) Lemmas : 676236 (Deleted: 639948) Binary : 11038 (Ratio: 1.63%) Ternary : 2728 (Ratio: 0.40%) Conflict : 676236 (Average Length: 679.6 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 676236 (Average: 13.00 Max: 804 Sum: 8788265) Executed : 676135 (Average: 12.99 Max: 804 Sum: 8785132 Ratio: 99.96%) Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.04%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 595276 (Eliminated: 0 Frozen: 191082) Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 765MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 8.08s Memory: 701MB (+0MB) UNKNOWN Iteration Time: 8.15s Iteration 80 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 : 81 Time : 559.310s (Solving: 535.80s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 559.400s Choices : 10337609 (Domain: 10199947) Conflicts : 685769 (Analyzed: 685766) Restarts : 7702 (Average: 89.04 Last: 172) Model-Level : 115.0 Problems : 81 (Average Length: 88.54 Splits: 0) Lemmas : 685766 (Deleted: 649978) Binary : 11077 (Ratio: 1.62%) Ternary : 2735 (Ratio: 0.40%) Conflict : 685766 (Average Length: 679.3 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 685766 (Average: 12.89 Max: 804 Sum: 8837229) Executed : 685665 (Average: 12.88 Max: 804 Sum: 8834096 Ratio: 99.96%) Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.04%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 595276 (Eliminated: 0 Frozen: 191082) Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 765MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 6.79s Memory: 701MB (+0MB) UNKNOWN Iteration Time: 6.84s Iteration 81 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 : 82 Time : 566.491s (Solving: 542.86s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 566.584s Choices : 10402205 (Domain: 10264543) Conflicts : 694775 (Analyzed: 694772) Restarts : 7802 (Average: 89.05 Last: 172) Model-Level : 115.0 Problems : 82 (Average Length: 88.89 Splits: 0) Lemmas : 694772 (Deleted: 659325) Binary : 11104 (Ratio: 1.60%) Ternary : 2740 (Ratio: 0.39%) Conflict : 694772 (Average Length: 682.5 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 694772 (Average: 12.78 Max: 804 Sum: 8882600) Executed : 694671 (Average: 12.78 Max: 804 Sum: 8879467 Ratio: 99.96%) Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.04%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 595276 (Eliminated: 0 Frozen: 191082) Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 765MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 7.14s Memory: 701MB (+0MB) UNKNOWN Iteration Time: 7.19s Iteration 82 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 : 83 Time : 573.665s (Solving: 549.90s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 573.760s Choices : 10471274 (Domain: 10333596) Conflicts : 703729 (Analyzed: 703726) Restarts : 7902 (Average: 89.06 Last: 172) Model-Level : 115.0 Problems : 83 (Average Length: 89.23 Splits: 0) Lemmas : 703726 (Deleted: 668164) Binary : 11147 (Ratio: 1.58%) Ternary : 2742 (Ratio: 0.39%) Conflict : 703726 (Average Length: 685.6 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 703726 (Average: 12.69 Max: 804 Sum: 8929593) Executed : 703625 (Average: 12.68 Max: 804 Sum: 8926460 Ratio: 99.96%) Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.04%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 595276 (Eliminated: 0 Frozen: 191082) Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 765MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 7.13s Memory: 701MB (+0MB) UNKNOWN Iteration Time: 7.18s Iteration 83 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 : 84 Time : 581.706s (Solving: 557.82s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 581.804s Choices : 10551647 (Domain: 10413967) Conflicts : 713098 (Analyzed: 713095) Restarts : 8002 (Average: 89.11 Last: 172) Model-Level : 115.0 Problems : 84 (Average Length: 89.56 Splits: 0) Lemmas : 713095 (Deleted: 676932) Binary : 11170 (Ratio: 1.57%) Ternary : 2753 (Ratio: 0.39%) Conflict : 713095 (Average Length: 687.2 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 713095 (Average: 12.60 Max: 804 Sum: 8986082) Executed : 712994 (Average: 12.60 Max: 804 Sum: 8982949 Ratio: 99.97%) Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.03%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 595276 (Eliminated: 0 Frozen: 191082) Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 765MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 8.00s Memory: 701MB (+0MB) UNKNOWN Iteration Time: 8.05s Iteration 84 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 : 85 Time : 590.176s (Solving: 566.16s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 590.276s Choices : 10649622 (Domain: 10511921) Conflicts : 722224 (Analyzed: 722221) Restarts : 8102 (Average: 89.14 Last: 172) Model-Level : 115.0 Problems : 85 (Average Length: 89.88 Splits: 0) Lemmas : 722221 (Deleted: 686115) Binary : 11200 (Ratio: 1.55%) Ternary : 2758 (Ratio: 0.38%) Conflict : 722221 (Average Length: 688.3 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 722221 (Average: 12.54 Max: 804 Sum: 9055371) Executed : 722120 (Average: 12.53 Max: 804 Sum: 9052238 Ratio: 99.97%) Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.03%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 595276 (Eliminated: 0 Frozen: 191082) Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 765MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 8.43s Memory: 701MB (+0MB) UNKNOWN Iteration Time: 8.48s Iteration 85 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 : 86 Time : 593.536s (Solving: 569.38s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 593.636s Choices : 10709382 (Domain: 10571681) Conflicts : 730159 (Analyzed: 730156) Restarts : 8202 (Average: 89.02 Last: 172) Model-Level : 115.0 Problems : 86 (Average Length: 90.20 Splits: 0) Lemmas : 730156 (Deleted: 692780) Binary : 11262 (Ratio: 1.54%) Ternary : 2768 (Ratio: 0.38%) Conflict : 730156 (Average Length: 683.0 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 730156 (Average: 12.47 Max: 804 Sum: 9106231) Executed : 730055 (Average: 12.47 Max: 804 Sum: 9103098 Ratio: 99.97%) Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.03%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 595276 (Eliminated: 0 Frozen: 191082) Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 765MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 3.31s Memory: 701MB (+0MB) UNKNOWN Iteration Time: 3.37s Iteration 86 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 : 87 Time : 602.390s (Solving: 578.09s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 602.496s Choices : 10752690 (Domain: 10614989) Conflicts : 738328 (Analyzed: 738325) Restarts : 8302 (Average: 88.93 Last: 172) Model-Level : 115.0 Problems : 87 (Average Length: 90.51 Splits: 0) Lemmas : 738325 (Deleted: 700549) Binary : 11278 (Ratio: 1.53%) Ternary : 2776 (Ratio: 0.38%) Conflict : 738325 (Average Length: 688.4 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 738325 (Average: 12.38 Max: 804 Sum: 9139428) Executed : 738224 (Average: 12.37 Max: 804 Sum: 9136295 Ratio: 99.97%) Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.03%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 595276 (Eliminated: 0 Frozen: 191082) Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 765MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 8.81s Memory: 701MB (+0MB) UNKNOWN Iteration Time: 8.86s Iteration 87 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 : 88 Time : 608.995s (Solving: 584.56s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 609.108s Choices : 10813516 (Domain: 10675815) Conflicts : 746953 (Analyzed: 746950) Restarts : 8402 (Average: 88.90 Last: 172) Model-Level : 115.0 Problems : 88 (Average Length: 90.81 Splits: 0) Lemmas : 746950 (Deleted: 710805) Binary : 11291 (Ratio: 1.51%) Ternary : 2780 (Ratio: 0.37%) Conflict : 746950 (Average Length: 689.3 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 746950 (Average: 12.29 Max: 804 Sum: 9180716) Executed : 746849 (Average: 12.29 Max: 804 Sum: 9177583 Ratio: 99.97%) Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.03%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 595276 (Eliminated: 0 Frozen: 191082) Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 765MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 6.56s Memory: 701MB (+0MB) UNKNOWN Iteration Time: 6.61s Iteration 88 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 : 89 Time : 615.995s (Solving: 591.44s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 616.112s Choices : 10890578 (Domain: 10752791) Conflicts : 755509 (Analyzed: 755506) Restarts : 8502 (Average: 88.86 Last: 172) Model-Level : 115.0 Problems : 89 (Average Length: 91.10 Splits: 0) Lemmas : 755506 (Deleted: 717125) Binary : 11326 (Ratio: 1.50%) Ternary : 2804 (Ratio: 0.37%) Conflict : 755506 (Average Length: 691.3 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 755506 (Average: 12.22 Max: 804 Sum: 9234773) Executed : 755405 (Average: 12.22 Max: 804 Sum: 9231640 Ratio: 99.97%) Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.03%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 595276 (Eliminated: 0 Frozen: 191082) Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 765MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 6.96s Memory: 701MB (+0MB) UNKNOWN Iteration Time: 7.01s Iteration 89 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 : 90 Time : 623.170s (Solving: 598.47s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 623.292s Choices : 10962157 (Domain: 10824370) Conflicts : 764947 (Analyzed: 764944) Restarts : 8602 (Average: 88.93 Last: 172) Model-Level : 115.0 Problems : 90 (Average Length: 91.39 Splits: 0) Lemmas : 764944 (Deleted: 727704) Binary : 11341 (Ratio: 1.48%) Ternary : 2805 (Ratio: 0.37%) Conflict : 764944 (Average Length: 692.2 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 764944 (Average: 12.14 Max: 804 Sum: 9284631) Executed : 764843 (Average: 12.13 Max: 804 Sum: 9281498 Ratio: 99.97%) Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.03%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 595276 (Eliminated: 0 Frozen: 191082) Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 765MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 7.12s Memory: 701MB (+0MB) UNKNOWN Iteration Time: 7.18s Iteration 90 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 : 91 Time : 632.132s (Solving: 607.28s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 632.256s Choices : 11167284 (Domain: 11026963) Conflicts : 774502 (Analyzed: 774499) Restarts : 8702 (Average: 89.00 Last: 172) Model-Level : 115.0 Problems : 91 (Average Length: 91.67 Splits: 0) Lemmas : 774499 (Deleted: 736613) Binary : 11533 (Ratio: 1.49%) Ternary : 2817 (Ratio: 0.36%) Conflict : 774499 (Average Length: 693.2 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 774499 (Average: 12.21 Max: 804 Sum: 9454212) Executed : 774398 (Average: 12.20 Max: 804 Sum: 9451079 Ratio: 99.97%) Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.03%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 595276 (Eliminated: 0 Frozen: 191082) Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 765MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 8.91s Memory: 701MB (+0MB) UNKNOWN Iteration Time: 8.97s Iteration 91 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 : 92 Time : 640.000s (Solving: 614.98s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 640.128s Choices : 11248145 (Domain: 11107823) Conflicts : 783668 (Analyzed: 783665) Restarts : 8802 (Average: 89.03 Last: 184) Model-Level : 115.0 Problems : 92 (Average Length: 91.95 Splits: 0) Lemmas : 783665 (Deleted: 746031) Binary : 11547 (Ratio: 1.47%) Ternary : 2818 (Ratio: 0.36%) Conflict : 783665 (Average Length: 693.2 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 783665 (Average: 12.13 Max: 804 Sum: 9509243) Executed : 783564 (Average: 12.13 Max: 804 Sum: 9506110 Ratio: 99.97%) Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.03%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 595276 (Eliminated: 0 Frozen: 191082) Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 765MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 7.81s Memory: 701MB (+0MB) UNKNOWN Iteration Time: 7.88s Iteration 92 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 : 93 Time : 649.676s (Solving: 624.50s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 649.804s Choices : 11356158 (Domain: 11215833) Conflicts : 793553 (Analyzed: 793550) Restarts : 8902 (Average: 89.14 Last: 184) Model-Level : 115.0 Problems : 93 (Average Length: 92.22 Splits: 0) Lemmas : 793550 (Deleted: 755022) Binary : 11594 (Ratio: 1.46%) Ternary : 2832 (Ratio: 0.36%) Conflict : 793550 (Average Length: 693.8 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 793550 (Average: 12.08 Max: 804 Sum: 9587789) Executed : 793449 (Average: 12.08 Max: 804 Sum: 9584656 Ratio: 99.97%) Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.03%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 595276 (Eliminated: 0 Frozen: 191082) Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 765MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 9.62s Memory: 701MB (+0MB) UNKNOWN Iteration Time: 9.68s Iteration 93 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 : 94 Time : 652.896s (Solving: 627.60s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 653.028s Choices : 11405512 (Domain: 11265187) Conflicts : 801159 (Analyzed: 801156) Restarts : 9002 (Average: 89.00 Last: 184) Model-Level : 115.0 Problems : 94 (Average Length: 92.48 Splits: 0) Lemmas : 801156 (Deleted: 762483) Binary : 11661 (Ratio: 1.46%) Ternary : 2841 (Ratio: 0.35%) Conflict : 801156 (Average Length: 689.0 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 801156 (Average: 12.02 Max: 804 Sum: 9630252) Executed : 801055 (Average: 12.02 Max: 804 Sum: 9627119 Ratio: 99.97%) Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.03%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 595276 (Eliminated: 0 Frozen: 191082) Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 765MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 3.18s Memory: 701MB (+0MB) UNKNOWN Iteration Time: 3.22s Iteration 94 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 : 95 Time : 663.475s (Solving: 638.06s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 663.612s Choices : 11460353 (Domain: 11320028) Conflicts : 810194 (Analyzed: 810191) Restarts : 9102 (Average: 89.01 Last: 184) Model-Level : 115.0 Problems : 95 (Average Length: 92.74 Splits: 0) Lemmas : 810191 (Deleted: 772040) Binary : 11690 (Ratio: 1.44%) Ternary : 2856 (Ratio: 0.35%) Conflict : 810191 (Average Length: 698.6 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 810191 (Average: 11.94 Max: 804 Sum: 9673989) Executed : 810090 (Average: 11.94 Max: 804 Sum: 9670856 Ratio: 99.97%) Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.03%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 595276 (Eliminated: 0 Frozen: 191082) Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 765MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 10.54s Memory: 701MB (+0MB) UNKNOWN Iteration Time: 10.59s Iteration 95 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 : 96 Time : 671.564s (Solving: 645.99s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 671.704s Choices : 11542933 (Domain: 11402608) Conflicts : 818906 (Analyzed: 818903) Restarts : 9202 (Average: 88.99 Last: 184) Model-Level : 115.0 Problems : 96 (Average Length: 92.99 Splits: 0) Lemmas : 818903 (Deleted: 780806) Binary : 11741 (Ratio: 1.43%) Ternary : 2872 (Ratio: 0.35%) Conflict : 818903 (Average Length: 701.0 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 818903 (Average: 11.89 Max: 804 Sum: 9739410) Executed : 818802 (Average: 11.89 Max: 804 Sum: 9736277 Ratio: 99.97%) Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.03%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 595276 (Eliminated: 0 Frozen: 191082) Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 765MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 8.03s Memory: 701MB (+0MB) UNKNOWN Iteration Time: 8.09s Iteration 96 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 : 97 Time : 678.129s (Solving: 652.42s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 678.268s Choices : 11604353 (Domain: 11464028) Conflicts : 828070 (Analyzed: 828067) Restarts : 9302 (Average: 89.02 Last: 184) Model-Level : 115.0 Problems : 97 (Average Length: 93.24 Splits: 0) Lemmas : 828067 (Deleted: 789353) Binary : 11764 (Ratio: 1.42%) Ternary : 2873 (Ratio: 0.35%) Conflict : 828067 (Average Length: 701.5 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 828067 (Average: 11.81 Max: 804 Sum: 9781652) Executed : 827966 (Average: 11.81 Max: 804 Sum: 9778519 Ratio: 99.97%) Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.03%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 595276 (Eliminated: 0 Frozen: 191082) Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 765MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 6.52s Memory: 701MB (+0MB) UNKNOWN Iteration Time: 6.57s Iteration 97 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 : 98 Time : 685.727s (Solving: 659.89s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 685.868s Choices : 11670203 (Domain: 11529878) Conflicts : 837340 (Analyzed: 837337) Restarts : 9402 (Average: 89.06 Last: 184) Model-Level : 115.0 Problems : 98 (Average Length: 93.48 Splits: 0) Lemmas : 837337 (Deleted: 798391) Binary : 11790 (Ratio: 1.41%) Ternary : 2878 (Ratio: 0.34%) Conflict : 837337 (Average Length: 705.9 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 837337 (Average: 11.74 Max: 804 Sum: 9826639) Executed : 837236 (Average: 11.73 Max: 804 Sum: 9823506 Ratio: 99.97%) Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.03%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 595276 (Eliminated: 0 Frozen: 191082) Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 765MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 7.56s Memory: 701MB (+0MB) UNKNOWN Iteration Time: 7.60s Iteration 98 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 : 99 Time : 693.616s (Solving: 667.62s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 693.764s Choices : 11743501 (Domain: 11603168) Conflicts : 846866 (Analyzed: 846863) Restarts : 9502 (Average: 89.12 Last: 184) Model-Level : 115.0 Problems : 99 (Average Length: 93.72 Splits: 0) Lemmas : 846863 (Deleted: 807535) Binary : 11813 (Ratio: 1.39%) Ternary : 2879 (Ratio: 0.34%) Conflict : 846863 (Average Length: 706.9 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 846863 (Average: 11.67 Max: 804 Sum: 9878846) Executed : 846762 (Average: 11.66 Max: 804 Sum: 9875713 Ratio: 99.97%) Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.03%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 595276 (Eliminated: 0 Frozen: 191082) Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 765MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 7.83s Memory: 701MB (+0MB) UNKNOWN Iteration Time: 7.90s Iteration 99 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 : 100 Time : 702.056s (Solving: 675.93s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 702.208s Choices : 11827741 (Domain: 11687407) Conflicts : 856967 (Analyzed: 856964) Restarts : 9602 (Average: 89.25 Last: 184) Model-Level : 115.0 Problems : 100 (Average Length: 93.95 Splits: 0) Lemmas : 856964 (Deleted: 816890) Binary : 11828 (Ratio: 1.38%) Ternary : 2882 (Ratio: 0.34%) Conflict : 856964 (Average Length: 708.2 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 856964 (Average: 11.60 Max: 804 Sum: 9940425) Executed : 856863 (Average: 11.60 Max: 804 Sum: 9937292 Ratio: 99.97%) Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.03%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 595276 (Eliminated: 0 Frozen: 191082) Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 765MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 8.40s Memory: 701MB (+0MB) UNKNOWN Iteration Time: 8.45s Iteration 100 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 : 101 Time : 710.878s (Solving: 684.61s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 711.032s Choices : 11924133 (Domain: 11783530) Conflicts : 866234 (Analyzed: 866231) Restarts : 9702 (Average: 89.28 Last: 184) Model-Level : 115.0 Problems : 101 (Average Length: 94.18 Splits: 0) Lemmas : 866231 (Deleted: 826877) Binary : 11848 (Ratio: 1.37%) Ternary : 2889 (Ratio: 0.33%) Conflict : 866231 (Average Length: 709.9 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 866231 (Average: 11.56 Max: 804 Sum: 10009326) Executed : 866130 (Average: 11.55 Max: 804 Sum: 10006193 Ratio: 99.97%) Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.03%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 595276 (Eliminated: 0 Frozen: 191082) Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 765MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 8.77s Memory: 701MB (+0MB) UNKNOWN Iteration Time: 8.83s Iteration 101 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 : 102 Time : 720.063s (Solving: 693.67s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 720.220s Choices : 12024984 (Domain: 11884377) Conflicts : 876018 (Analyzed: 876015) Restarts : 9802 (Average: 89.37 Last: 184) Model-Level : 115.0 Problems : 102 (Average Length: 94.40 Splits: 0) Lemmas : 876015 (Deleted: 836030) Binary : 11857 (Ratio: 1.35%) Ternary : 2892 (Ratio: 0.33%) Conflict : 876015 (Average Length: 709.6 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 876015 (Average: 11.51 Max: 804 Sum: 10081329) Executed : 875914 (Average: 11.50 Max: 804 Sum: 10078196 Ratio: 99.97%) Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.03%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 595276 (Eliminated: 0 Frozen: 191082) Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 765MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 9.15s Memory: 701MB (+0MB) UNKNOWN Iteration Time: 9.19s Iteration 102 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 : 103 Time : 729.881s (Solving: 703.35s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 730.040s Choices : 12380022 (Domain: 12236675) Conflicts : 884930 (Analyzed: 884927) Restarts : 9902 (Average: 89.37 Last: 184) Model-Level : 115.0 Problems : 103 (Average Length: 94.62 Splits: 0) Lemmas : 884927 (Deleted: 845293) Binary : 12077 (Ratio: 1.36%) Ternary : 2911 (Ratio: 0.33%) Conflict : 884927 (Average Length: 713.3 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 884927 (Average: 11.74 Max: 804 Sum: 10387706) Executed : 884826 (Average: 11.73 Max: 804 Sum: 10384573 Ratio: 99.97%) Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.03%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 595276 (Eliminated: 0 Frozen: 191082) Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 765MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 9.77s Memory: 701MB (+0MB) UNKNOWN Iteration Time: 9.82s Iteration 103 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 : 104 Time : 732.460s (Solving: 705.81s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 732.620s Choices : 12414794 (Domain: 12271447) Conflicts : 892338 (Analyzed: 892335) Restarts : 10002 (Average: 89.22 Last: 184) Model-Level : 115.0 Problems : 104 (Average Length: 94.84 Splits: 0) Lemmas : 892335 (Deleted: 851570) Binary : 12115 (Ratio: 1.36%) Ternary : 2915 (Ratio: 0.33%) Conflict : 892335 (Average Length: 708.4 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 892335 (Average: 11.67 Max: 804 Sum: 10413513) Executed : 892234 (Average: 11.67 Max: 804 Sum: 10410380 Ratio: 99.97%) Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.03%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 595276 (Eliminated: 0 Frozen: 191082) Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 765MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 2.54s Memory: 701MB (+0MB) UNKNOWN Iteration Time: 2.58s Iteration 104 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 : 105 Time : 742.371s (Solving: 715.57s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 742.536s Choices : 12485724 (Domain: 12342377) Conflicts : 901675 (Analyzed: 901672) Restarts : 10102 (Average: 89.26 Last: 184) Model-Level : 115.0 Problems : 105 (Average Length: 95.05 Splits: 0) Lemmas : 901672 (Deleted: 861412) Binary : 12151 (Ratio: 1.35%) Ternary : 2921 (Ratio: 0.32%) Conflict : 901672 (Average Length: 717.4 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 901672 (Average: 11.61 Max: 804 Sum: 10470229) Executed : 901571 (Average: 11.61 Max: 804 Sum: 10467096 Ratio: 99.97%) Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.03%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 595276 (Eliminated: 0 Frozen: 191082) Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 765MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 9.86s Memory: 701MB (+0MB) UNKNOWN Iteration Time: 9.92s Iteration 105 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 : 106 Time : 751.446s (Solving: 724.50s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 751.616s Choices : 12572967 (Domain: 12429620) Conflicts : 910932 (Analyzed: 910929) Restarts : 10202 (Average: 89.29 Last: 184) Model-Level : 115.0 Problems : 106 (Average Length: 95.25 Splits: 0) Lemmas : 910929 (Deleted: 871578) Binary : 12217 (Ratio: 1.34%) Ternary : 2928 (Ratio: 0.32%) Conflict : 910929 (Average Length: 724.9 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 910929 (Average: 11.57 Max: 804 Sum: 10538307) Executed : 910828 (Average: 11.57 Max: 804 Sum: 10535174 Ratio: 99.97%) Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.03%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 595276 (Eliminated: 0 Frozen: 191082) Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 765MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 9.03s Memory: 701MB (+0MB) UNKNOWN Iteration Time: 9.08s Iteration 106 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 : 107 Time : 758.286s (Solving: 731.21s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 758.460s Choices : 12635599 (Domain: 12492247) Conflicts : 920355 (Analyzed: 920352) Restarts : 10302 (Average: 89.34 Last: 184) Model-Level : 115.0 Problems : 107 (Average Length: 95.46 Splits: 0) Lemmas : 920352 (Deleted: 879581) Binary : 12233 (Ratio: 1.33%) Ternary : 2928 (Ratio: 0.32%) Conflict : 920352 (Average Length: 724.9 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 920352 (Average: 11.50 Max: 804 Sum: 10581898) Executed : 920251 (Average: 11.49 Max: 804 Sum: 10578765 Ratio: 99.97%) Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.03%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 595276 (Eliminated: 0 Frozen: 191082) Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 765MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 6.79s Memory: 701MB (+0MB) UNKNOWN Iteration Time: 6.85s Iteration 107 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 : 108 Time : 765.679s (Solving: 738.45s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 765.856s Choices : 12704465 (Domain: 12561104) Conflicts : 929262 (Analyzed: 929259) Restarts : 10402 (Average: 89.33 Last: 184) Model-Level : 115.0 Problems : 108 (Average Length: 95.66 Splits: 0) Lemmas : 929259 (Deleted: 888870) Binary : 12254 (Ratio: 1.32%) Ternary : 2936 (Ratio: 0.32%) Conflict : 929259 (Average Length: 726.8 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 929259 (Average: 11.44 Max: 804 Sum: 10629083) Executed : 929158 (Average: 11.43 Max: 804 Sum: 10625950 Ratio: 99.97%) Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.03%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 595276 (Eliminated: 0 Frozen: 191082) Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 765MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 7.34s Memory: 701MB (+0MB) UNKNOWN Iteration Time: 7.40s Iteration 108 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 : 109 Time : 773.496s (Solving: 746.11s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 773.676s Choices : 12791375 (Domain: 12647820) Conflicts : 938134 (Analyzed: 938131) Restarts : 10502 (Average: 89.33 Last: 184) Model-Level : 115.0 Problems : 109 (Average Length: 95.85 Splits: 0) Lemmas : 938131 (Deleted: 897595) Binary : 12348 (Ratio: 1.32%) Ternary : 2947 (Ratio: 0.31%) Conflict : 938131 (Average Length: 726.7 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 938131 (Average: 11.40 Max: 804 Sum: 10692359) Executed : 938030 (Average: 11.39 Max: 804 Sum: 10689226 Ratio: 99.97%) Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.03%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 595276 (Eliminated: 0 Frozen: 191082) Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 765MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 7.76s Memory: 701MB (+0MB) UNKNOWN Iteration Time: 7.82s Iteration 109 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 : 110 Time : 781.078s (Solving: 753.54s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 781.260s Choices : 12865902 (Domain: 12722324) Conflicts : 947574 (Analyzed: 947571) Restarts : 10602 (Average: 89.38 Last: 184) Model-Level : 115.0 Problems : 110 (Average Length: 96.05 Splits: 0) Lemmas : 947571 (Deleted: 906268) Binary : 12356 (Ratio: 1.30%) Ternary : 2949 (Ratio: 0.31%) Conflict : 947571 (Average Length: 727.0 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 947571 (Average: 11.34 Max: 804 Sum: 10742954) Executed : 947470 (Average: 11.33 Max: 804 Sum: 10739821 Ratio: 99.97%) Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.03%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 595276 (Eliminated: 0 Frozen: 191082) Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 765MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 7.53s Memory: 701MB (+0MB) UNKNOWN Iteration Time: 7.59s Iteration 110 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 : 111 Time : 788.621s (Solving: 760.96s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 788.804s Choices : 12943246 (Domain: 12799668) Conflicts : 956305 (Analyzed: 956302) Restarts : 10702 (Average: 89.36 Last: 184) Model-Level : 115.0 Problems : 111 (Average Length: 96.23 Splits: 0) Lemmas : 956302 (Deleted: 915504) Binary : 12373 (Ratio: 1.29%) Ternary : 2955 (Ratio: 0.31%) Conflict : 956302 (Average Length: 729.7 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 956302 (Average: 11.28 Max: 804 Sum: 10789739) Executed : 956201 (Average: 11.28 Max: 804 Sum: 10786606 Ratio: 99.97%) Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.03%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 595276 (Eliminated: 0 Frozen: 191082) Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 765MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 7.51s Memory: 701MB (+0MB) UNKNOWN Iteration Time: 7.55s Iteration 111 Queue: [(22,110,2,True), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 112 Time : 798.694s (Solving: 770.88s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 798.880s Choices : 13040307 (Domain: 12896729) Conflicts : 966555 (Analyzed: 966552) Restarts : 10802 (Average: 89.48 Last: 184) Model-Level : 115.0 Problems : 112 (Average Length: 96.42 Splits: 0) Lemmas : 966552 (Deleted: 924115) Binary : 12395 (Ratio: 1.28%) Ternary : 2957 (Ratio: 0.31%) Conflict : 966552 (Average Length: 731.9 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 966552 (Average: 11.23 Max: 804 Sum: 10854853) Executed : 966451 (Average: 11.23 Max: 804 Sum: 10851720 Ratio: 99.97%) Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.03%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 595276 (Eliminated: 0 Frozen: 191082) Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 765MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 10.02s Memory: 701MB (+0MB) UNKNOWN Iteration Time: 10.08s Iteration 112 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 : 113 Time : 802.753s (Solving: 774.81s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 802.940s Choices : 13111674 (Domain: 12968096) Conflicts : 974599 (Analyzed: 974596) Restarts : 10902 (Average: 89.40 Last: 184) Model-Level : 115.0 Problems : 113 (Average Length: 96.60 Splits: 0) Lemmas : 974596 (Deleted: 931881) Binary : 12454 (Ratio: 1.28%) Ternary : 2975 (Ratio: 0.31%) Conflict : 974596 (Average Length: 728.0 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 974596 (Average: 11.21 Max: 804 Sum: 10920351) Executed : 974495 (Average: 11.20 Max: 804 Sum: 10917218 Ratio: 99.97%) Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.03%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 595276 (Eliminated: 0 Frozen: 191082) Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 765MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 4.02s Memory: 701MB (+0MB) UNKNOWN Iteration Time: 4.06s Iteration 113 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 : 114 Time : 812.869s (Solving: 784.81s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 813.064s Choices : 13185537 (Domain: 13041959) Conflicts : 983518 (Analyzed: 983515) Restarts : 11002 (Average: 89.39 Last: 184) Model-Level : 115.0 Problems : 114 (Average Length: 96.78 Splits: 0) Lemmas : 983515 (Deleted: 941911) Binary : 12505 (Ratio: 1.27%) Ternary : 2986 (Ratio: 0.30%) Conflict : 983515 (Average Length: 737.3 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 983515 (Average: 11.16 Max: 804 Sum: 10979427) Executed : 983414 (Average: 11.16 Max: 804 Sum: 10976294 Ratio: 99.97%) Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.03%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 595276 (Eliminated: 0 Frozen: 191082) Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 765MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 10.08s Memory: 701MB (+0MB) UNKNOWN Iteration Time: 10.12s Iteration 114 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 : 115 Time : 820.835s (Solving: 792.64s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 821.036s Choices : 13255710 (Domain: 13112132) Conflicts : 992455 (Analyzed: 992452) Restarts : 11102 (Average: 89.39 Last: 184) Model-Level : 115.0 Problems : 115 (Average Length: 96.96 Splits: 0) Lemmas : 992452 (Deleted: 950714) Binary : 12552 (Ratio: 1.26%) Ternary : 3001 (Ratio: 0.30%) Conflict : 992452 (Average Length: 740.7 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 992452 (Average: 11.12 Max: 804 Sum: 11032012) Executed : 992351 (Average: 11.11 Max: 804 Sum: 11028879 Ratio: 99.97%) Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.03%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 595276 (Eliminated: 0 Frozen: 191082) Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 765MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 7.92s Memory: 701MB (+0MB) UNKNOWN Iteration Time: 7.97s Iteration 115 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 : 116 Time : 827.584s (Solving: 799.26s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 827.788s Choices : 13320597 (Domain: 13177016) Conflicts : 1001486 (Analyzed: 1001483) Restarts : 11202 (Average: 89.40 Last: 184) Model-Level : 115.0 Problems : 116 (Average Length: 97.13 Splits: 0) Lemmas : 1001483 (Deleted: 959507) Binary : 12570 (Ratio: 1.26%) Ternary : 3008 (Ratio: 0.30%) Conflict : 1001483 (Average Length: 740.9 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 1001483 (Average: 11.06 Max: 804 Sum: 11079040) Executed : 1001382 (Average: 11.06 Max: 804 Sum: 11075907 Ratio: 99.97%) Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.03%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 595276 (Eliminated: 0 Frozen: 191082) Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 765MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 6.71s Memory: 701MB (+0MB) UNKNOWN Iteration Time: 6.75s Iteration 116 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 : 117 Time : 836.118s (Solving: 807.67s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 836.324s Choices : 13400827 (Domain: 13257219) Conflicts : 1011715 (Analyzed: 1011712) Restarts : 11302 (Average: 89.52 Last: 184) Model-Level : 115.0 Problems : 117 (Average Length: 97.30 Splits: 0) Lemmas : 1011712 (Deleted: 968327) Binary : 12615 (Ratio: 1.25%) Ternary : 3012 (Ratio: 0.30%) Conflict : 1011712 (Average Length: 742.9 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 1011712 (Average: 11.01 Max: 804 Sum: 11136699) Executed : 1011611 (Average: 11.00 Max: 804 Sum: 11133566 Ratio: 99.97%) Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.03%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 595276 (Eliminated: 0 Frozen: 191082) Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 765MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 8.49s Memory: 701MB (+0MB) UNKNOWN Iteration Time: 8.54s Iteration 117 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 : 118 Time : 843.607s (Solving: 815.01s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 843.812s Choices : 13473329 (Domain: 13329698) Conflicts : 1020876 (Analyzed: 1020873) Restarts : 11402 (Average: 89.53 Last: 184) Model-Level : 115.0 Problems : 118 (Average Length: 97.47 Splits: 0) Lemmas : 1020873 (Deleted: 978408) Binary : 12634 (Ratio: 1.24%) Ternary : 3018 (Ratio: 0.30%) Conflict : 1020873 (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 : 1020873 (Average: 10.96 Max: 804 Sum: 11186313) Executed : 1020772 (Average: 10.95 Max: 804 Sum: 11183180 Ratio: 99.97%) Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.03%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 595276 (Eliminated: 0 Frozen: 191082) Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 765MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 7.44s Memory: 701MB (+0MB) UNKNOWN Iteration Time: 7.49s Iteration 118 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... [start: stats after solve call] Models : 0+ Calls : 119 Time : 851.708s (Solving: 822.96s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 851.916s Choices : 13557863 (Domain: 13414212) Conflicts : 1030146 (Analyzed: 1030143) Restarts : 11502 (Average: 89.56 Last: 184) Model-Level : 115.0 Problems : 119 (Average Length: 97.63 Splits: 0) Lemmas : 1030143 (Deleted: 987414) Binary : 12652 (Ratio: 1.23%) Ternary : 3032 (Ratio: 0.29%) Conflict : 1030143 (Average Length: 745.8 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 1030143 (Average: 10.92 Max: 804 Sum: 11244412) Executed : 1030042 (Average: 10.91 Max: 804 Sum: 11241279 Ratio: 99.97%) Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.03%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 595276 (Eliminated: 0 Frozen: 191082) Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 765MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 8.05s Memory: 701MB (+0MB) UNKNOWN Iteration Time: 8.11s Iteration 119 Queue: [(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 : 860.236s (Solving: 831.34s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 860.448s Choices : 13712973 (Domain: 13568567) Conflicts : 1039314 (Analyzed: 1039311) Restarts : 11602 (Average: 89.58 Last: 184) Model-Level : 115.0 Problems : 120 (Average Length: 97.79 Splits: 0) Lemmas : 1039311 (Deleted: 996426) Binary : 12746 (Ratio: 1.23%) Ternary : 3043 (Ratio: 0.29%) Conflict : 1039311 (Average Length: 746.0 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 1039311 (Average: 10.94 Max: 804 Sum: 11366683) Executed : 1039210 (Average: 10.93 Max: 804 Sum: 11363550 Ratio: 99.97%) Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.03%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 595276 (Eliminated: 0 Frozen: 191082) Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 765MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 8.47s Memory: 701MB (+0MB) UNKNOWN Iteration Time: 8.53s Iteration 120 Queue: [(4,20,11,True), (5,25,11,True), (6,30,10,True), (7,35,9,True), (8,40,8,True), (9,45,7,True), (10,50,7,False), (11,55,6,True), (12,60,6,False), (13,65,5,True), (14,70,5,False), (15,75,4,True), (16,80,4,False), (17,85,4,False), (18,90,4,False), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,2,True)] Grounded Until: 115 Blocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 121 Time : 862.239s (Solving: 833.19s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 862.452s Choices : 13745614 (Domain: 13601208) Conflicts : 1046538 (Analyzed: 1046535) Restarts : 11702 (Average: 89.43 Last: 184) Model-Level : 115.0 Problems : 121 (Average Length: 97.95 Splits: 0) Lemmas : 1046535 (Deleted: 1002872) Binary : 12779 (Ratio: 1.22%) Ternary : 3048 (Ratio: 0.29%) Conflict : 1046535 (Average Length: 741.8 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 1046535 (Average: 10.88 Max: 804 Sum: 11389452) Executed : 1046434 (Average: 10.88 Max: 804 Sum: 11386319 Ratio: 99.97%) Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.03%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 595276 (Eliminated: 0 Frozen: 191082) Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 765MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 1.95s Memory: 701MB (+0MB) UNKNOWN Iteration Time: 2.01s Iteration 121 Queue: [(5,25,11,True), (6,30,10,True), (7,35,9,True), (8,40,8,True), (9,45,7,True), (10,50,7,False), (11,55,6,True), (12,60,6,False), (13,65,5,True), (14,70,5,False), (15,75,4,True), (16,80,4,False), (17,85,4,False), (18,90,4,False), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,2,True)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 122 Time : 870.750s (Solving: 841.55s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 870.968s Choices : 13808870 (Domain: 13664464) Conflicts : 1054704 (Analyzed: 1054701) Restarts : 11802 (Average: 89.37 Last: 184) Model-Level : 115.0 Problems : 122 (Average Length: 98.11 Splits: 0) Lemmas : 1054701 (Deleted: 1010599) Binary : 12848 (Ratio: 1.22%) Ternary : 3058 (Ratio: 0.29%) Conflict : 1054701 (Average Length: 751.8 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 1054701 (Average: 10.84 Max: 804 Sum: 11436954) Executed : 1054600 (Average: 10.84 Max: 804 Sum: 11433821 Ratio: 99.97%) Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.03%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 595276 (Eliminated: 0 Frozen: 191082) Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 765MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 8.46s Memory: 701MB (+0MB) UNKNOWN Iteration Time: 8.52s Iteration 122 Queue: [(6,30,10,True), (7,35,9,True), (8,40,8,True), (9,45,7,True), (10,50,7,False), (11,55,6,True), (12,60,6,False), (13,65,5,True), (14,70,5,False), (15,75,4,True), (16,80,4,False), (17,85,4,False), (18,90,4,False), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,2,True)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 123 Time : 879.378s (Solving: 850.03s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 879.600s Choices : 13884685 (Domain: 13740279) Conflicts : 1063387 (Analyzed: 1063384) Restarts : 11902 (Average: 89.34 Last: 184) Model-Level : 115.0 Problems : 123 (Average Length: 98.26 Splits: 0) Lemmas : 1063384 (Deleted: 1020841) Binary : 12891 (Ratio: 1.21%) Ternary : 3083 (Ratio: 0.29%) Conflict : 1063384 (Average Length: 757.6 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 1063384 (Average: 10.81 Max: 804 Sum: 11494856) Executed : 1063283 (Average: 10.81 Max: 804 Sum: 11491723 Ratio: 99.97%) Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.03%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 595276 (Eliminated: 0 Frozen: 191082) Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 765MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 8.57s Memory: 701MB (+0MB) UNKNOWN Iteration Time: 8.63s Iteration 123 Queue: [(7,35,9,True), (8,40,8,True), (9,45,7,True), (10,50,7,False), (11,55,6,True), (12,60,6,False), (13,65,5,True), (14,70,5,False), (15,75,4,True), (16,80,4,False), (17,85,4,False), (18,90,4,False), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,2,True)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 124 Time : 885.866s (Solving: 856.36s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 886.092s Choices : 13950526 (Domain: 13806057) Conflicts : 1072375 (Analyzed: 1072372) Restarts : 12002 (Average: 89.35 Last: 184) Model-Level : 115.0 Problems : 124 (Average Length: 98.41 Splits: 0) Lemmas : 1072372 (Deleted: 1029078) Binary : 12910 (Ratio: 1.20%) Ternary : 3093 (Ratio: 0.29%) Conflict : 1072372 (Average Length: 757.7 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 1072372 (Average: 10.76 Max: 804 Sum: 11541621) Executed : 1072271 (Average: 10.76 Max: 804 Sum: 11538488 Ratio: 99.97%) Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.03%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 595276 (Eliminated: 0 Frozen: 191082) Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 765MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 6.43s Memory: 701MB (+0MB) UNKNOWN Iteration Time: 6.49s Iteration 124 Queue: [(8,40,8,True), (9,45,7,True), (10,50,7,False), (11,55,6,True), (12,60,6,False), (13,65,5,True), (14,70,5,False), (15,75,4,True), (16,80,4,False), (17,85,4,False), (18,90,4,False), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,2,True)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 125 Time : 894.113s (Solving: 864.48s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 894.344s Choices : 14023841 (Domain: 13879370) Conflicts : 1081352 (Analyzed: 1081349) Restarts : 12102 (Average: 89.35 Last: 184) Model-Level : 115.0 Problems : 125 (Average Length: 98.56 Splits: 0) Lemmas : 1081349 (Deleted: 1037874) Binary : 12991 (Ratio: 1.20%) Ternary : 3108 (Ratio: 0.29%) Conflict : 1081349 (Average Length: 760.8 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 1081349 (Average: 10.72 Max: 804 Sum: 11595129) Executed : 1081248 (Average: 10.72 Max: 804 Sum: 11591996 Ratio: 99.97%) Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.03%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 595276 (Eliminated: 0 Frozen: 191082) Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 765MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 8.21s Memory: 701MB (+0MB) UNKNOWN Iteration Time: 8.25s Iteration 125 Queue: [(9,45,7,True), (10,50,7,False), (11,55,6,True), (12,60,6,False), (13,65,5,True), (14,70,5,False), (15,75,4,True), (16,80,4,False), (17,85,4,False), (18,90,4,False), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,2,True)] Grounded Until: 115 Unblocking actions... Solving... *** Info : (planner): INTERRUPTED by signal! UNKNOWN INTERRUPTED : 1 Models : 0+ Calls : 126 Time : 894.335s (Solving: 864.58s 1st Model: 0.00s Unsat: 3.47s) CPU Time : 894.544s Choices : 14024340 (Domain: 13879869) Conflicts : 1081471 (Analyzed: 1081468) Restarts : 12103 (Average: 89.36 Last: 184) Model-Level : 115.0 Problems : 126 (Average Length: 98.71 Splits: 0) Lemmas : 1081468 (Deleted: 1037874) Binary : 12991 (Ratio: 1.20%) Ternary : 3108 (Ratio: 0.29%) Conflict : 1081468 (Average Length: 760.7 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 1081468 (Average: 10.72 Max: 804 Sum: 11595494) Executed : 1081367 (Average: 10.72 Max: 804 Sum: 11592361 Ratio: 99.97%) Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.03%) Rules : 62994 (Original: 61599) Atoms : 50308 Bodies : 11595 (Original: 10199) Count : 252 (Original: 531) Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) Tight : Yes Variables : 595276 (Eliminated: 0 Frozen: 191082) Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) Memory Peak : 765MB Max. Length : 115 steps Models : 1