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