diff --git a/gc-ta1-tt1/ipc-2011_barman-sequential-satisficing_16.env b/gc-ta1-tt1/ipc-2011_barman-sequential-satisficing_16.env new file mode 100644 index 000000000..239b96e68 --- /dev/null +++ b/gc-ta1-tt1/ipc-2011_barman-sequential-satisficing_16.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-16.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: 16 + 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_16.err b/gc-ta1-tt1/ipc-2011_barman-sequential-satisficing_16.err new file mode 100644 index 000000000..5783cb4ea --- /dev/null +++ b/gc-ta1-tt1/ipc-2011_barman-sequential-satisficing_16.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': 16} +# 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-16.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.10 MEM 988288 MAXMEM 1079808 STALE 0 MAXMEM_RSS 903108 + + diff --git a/gc-ta1-tt1/ipc-2011_barman-sequential-satisficing_16.out b/gc-ta1-tt1/ipc-2011_barman-sequential-satisficing_16.out new file mode 100644 index 000000000..2c4702856 --- /dev/null +++ b/gc-ta1-tt1/ipc-2011_barman-sequential-satisficing_16.out @@ -0,0 +1,5488 @@ +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-16.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-16.pddl +Parsing... +Parsing: [0.040s CPU, 0.033s wall-clock] +Normalizing task... [0.000s CPU, 0.003s wall-clock] +Instantiating... +Generating Datalog program... [0.010s CPU, 0.009s wall-clock] +Normalizing Datalog program... +Normalizing Datalog program: [0.040s CPU, 0.044s wall-clock] +Preparing model... [0.020s CPU, 0.026s wall-clock] +Generated 115 rules. +Computing model... [0.510s CPU, 0.503s 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.540s CPU, 1.553s wall-clock] +Computing fact groups... +Finding invariants... +24 initial candidates +Finding invariants: [0.130s CPU, 0.125s 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.180s CPU, 0.175s wall-clock] +Building STRIPS to SAS dictionary... [0.000s CPU, 0.003s wall-clock] +Building dictionary for full mutex groups... [0.000s CPU, 0.003s wall-clock] +Building mutex information... +Building mutex information: [0.010s CPU, 0.003s wall-clock] +Translating task... +Processing axioms... +Simplifying axioms... [0.000s CPU, 0.000s wall-clock] +Processing axioms: [0.050s CPU, 0.053s wall-clock] +Translating task: [1.000s CPU, 1.004s 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.489s 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.410s 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: 48588 KB +Writing output... [0.390s CPU, 0.410s wall-clock] +Done! [4.090s CPU, 4.119s wall-clock] +planner.py version 0.0.1 + +Time: 0.85s +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.002s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s) +CPU Time : 0.856s + +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.410s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s) +CPU Time : 1.264s + +Choices : 327 (Domain: 271) +Conflicts : 52 (Analyzed: 51) +Restarts : 0 +Problems : 2 (Average Length: 4.50 Splits: 0) +Lemmas : 51 (Deleted: 0) + Binary : 20 (Ratio: 39.22%) + Ternary : 2 (Ratio: 3.92%) + Conflict : 51 (Average Length: 5.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 51 (Average: 6.43 Max: 37 Sum: 328) + Executed : 50 (Average: 6.41 Max: 37 Sum: 327 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.907s (Solving: 0.04s 1st Model: 0.03s Unsat: 0.00s) +CPU Time : 1.760s + +Choices : 1633 (Domain: 1519) +Conflicts : 160 (Analyzed: 159) +Restarts : 1 (Average: 159.00 Last: 51) +Model-Level : 342.0 +Problems : 3 (Average Length: 7.00 Splits: 0) +Lemmas : 159 (Deleted: 0) + Binary : 38 (Ratio: 23.90%) + Ternary : 7 (Ratio: 4.40%) + Conflict : 159 (Average Length: 76.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 159 (Average: 7.93 Max: 123 Sum: 1261) + Executed : 158 (Average: 7.92 Max: 123 Sum: 1260 Ratio: 99.92%) + Bounded : 1 (Average: 1.00 Max: 1 Sum: 1 Ratio: 0.08%) + +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.06s +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 : 4.173s (Solving: 1.98s 1st Model: 0.03s Unsat: 1.94s) +CPU Time : 4.028s + +Choices : 35781 (Domain: 31405) +Conflicts : 4799 (Analyzed: 4797) +Restarts : 58 (Average: 82.71 Last: 51) +Model-Level : 342.0 +Problems : 4 (Average Length: 8.25 Splits: 0) +Lemmas : 4797 (Deleted: 2190) + Binary : 465 (Ratio: 9.69%) + Ternary : 256 (Ratio: 5.34%) + Conflict : 4797 (Average Length: 92.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 4797 (Average: 7.24 Max: 130 Sum: 34711) + Executed : 4777 (Average: 7.19 Max: 130 Sum: 34495 Ratio: 99.38%) + Bounded : 20 (Average: 10.80 Max: 12 Sum: 216 Ratio: 0.62%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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: 2.02s +Memory: 229MB (+-3MB) +UNSAT +Iteration Time: 3.64s + +Iteration 4 +Queue: [(3,15,0,True), (4,20,0,True), (5,25,0,True), (6,30,0,True)] +Grounded Until: 10 +Expected Memory: 244.0MB +Grounding... [('step', [11]), ('step', [12]), ('step', [13]), ('step', [14]), ('step', [15]), ('check', [15])] +Grounding Time: 0.50s +Memory: 233MB (+4MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 5 +Time : 9.504s (Solving: 6.57s 1st Model: 0.03s Unsat: 1.94s) +CPU Time : 9.360s + +Choices : 110768 (Domain: 94150) +Conflicts : 13201 (Analyzed: 13199) +Restarts : 158 (Average: 83.54 Last: 90) +Model-Level : 342.0 +Problems : 5 (Average Length: 10.00 Splits: 0) +Lemmas : 13199 (Deleted: 6805) + Binary : 1431 (Ratio: 10.84%) + Ternary : 770 (Ratio: 5.83%) + Conflict : 13199 (Average Length: 130.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 13199 (Average: 8.11 Max: 266 Sum: 107097) + Executed : 13162 (Average: 8.08 Max: 266 Sum: 106607 Ratio: 99.54%) + Bounded : 37 (Average: 13.24 Max: 17 Sum: 490 Ratio: 0.46%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 610590 (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.63s +Memory: 256MB (+23MB) +UNKNOWN +Iteration Time: 5.34s + +Iteration 5 +Queue: [(4,20,0,True), (5,25,0,True), (6,30,0,True)] +Grounded Until: 15 +Expected Memory: 283.0MB +Grounding... [('step', [16]), ('step', [17]), ('step', [18]), ('step', [19]), ('step', [20]), ('check', [20])] +Grounding Time: 0.52s +Memory: 259MB (+3MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 6 +Time : 16.237s (Solving: 12.52s 1st Model: 0.03s Unsat: 1.94s) +CPU Time : 16.096s + +Choices : 218107 (Domain: 177435) +Conflicts : 22443 (Analyzed: 22441) +Restarts : 258 (Average: 86.98 Last: 131) +Model-Level : 342.0 +Problems : 6 (Average Length: 12.00 Splits: 0) +Lemmas : 22441 (Deleted: 15993) + Binary : 1993 (Ratio: 8.88%) + Ternary : 908 (Ratio: 4.05%) + Conflict : 22441 (Average Length: 513.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 22441 (Average: 9.20 Max: 326 Sum: 206459) + Executed : 22404 (Average: 9.18 Max: 326 Sum: 205969 Ratio: 99.76%) + Bounded : 37 (Average: 13.24 Max: 17 Sum: 490 Ratio: 0.24%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 864766 (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.99s +Memory: 277MB (+18MB) +UNKNOWN +Iteration Time: 6.74s + +Iteration 6 +Queue: [(5,25,0,True), (6,30,0,True)] +Grounded Until: 20 +Expected Memory: 304.0MB +Grounding... [('step', [21]), ('step', [22]), ('step', [23]), ('step', [24]), ('step', [25]), ('check', [25])] +Grounding Time: 0.58s +Memory: 296MB (+19MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 7 +Time : 25.139s (Solving: 20.55s 1st Model: 0.03s Unsat: 1.94s) +CPU Time : 25.000s + +Choices : 389341 (Domain: 335148) +Conflicts : 31381 (Analyzed: 31379) +Restarts : 358 (Average: 87.65 Last: 170) +Model-Level : 342.0 +Problems : 7 (Average Length: 14.14 Splits: 0) +Lemmas : 31379 (Deleted: 24166) + Binary : 2851 (Ratio: 9.09%) + Ternary : 1106 (Ratio: 3.52%) + Conflict : 31379 (Average Length: 688.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 31379 (Average: 11.65 Max: 425 Sum: 365613) + Executed : 31339 (Average: 11.63 Max: 425 Sum: 365042 Ratio: 99.84%) + Bounded : 40 (Average: 14.28 Max: 27 Sum: 571 Ratio: 0.16%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 1147226 (Binary: 91.3% Ternary: 6.9% Other: 1.8%) + +Memory Peak : 321MB +Max. Length : 20 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.09s +Memory: 308MB (+12MB) +UNKNOWN +Iteration Time: 8.92s + +Iteration 7 +Queue: [(6,30,0,True)] +Grounded Until: 25 +Expected Memory: 339.0MB +Grounding... [('step', [26]), ('step', [27]), ('step', [28]), ('step', [29]), ('step', [30]), ('check', [30])] +Grounding Time: 0.54s +Memory: 319MB (+11MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 8 +Time : 35.953s (Solving: 30.51s 1st Model: 0.03s Unsat: 1.94s) +CPU Time : 35.820s + +Choices : 608576 (Domain: 551026) +Conflicts : 39741 (Analyzed: 39739) +Restarts : 458 (Average: 86.77 Last: 170) +Model-Level : 342.0 +Problems : 8 (Average Length: 16.38 Splits: 0) +Lemmas : 39739 (Deleted: 29608) + Binary : 4016 (Ratio: 10.11%) + Ternary : 1246 (Ratio: 3.14%) + Conflict : 39739 (Average Length: 710.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 39739 (Average: 14.45 Max: 425 Sum: 574373) + Executed : 39699 (Average: 14.44 Max: 425 Sum: 573802 Ratio: 99.90%) + Bounded : 40 (Average: 14.28 Max: 27 Sum: 571 Ratio: 0.10%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 1427051 (Binary: 91.3% Ternary: 6.9% Other: 1.8%) + +Memory Peak : 350MB +Max. Length : 25 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 10.02s +Memory: 350MB (+31MB) +UNKNOWN +Iteration Time: 10.83s + +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 : 36.465s (Solving: 30.98s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 36.332s + +Choices : 613829 (Domain: 556279) +Conflicts : 40158 (Analyzed: 40155) +Restarts : 462 (Average: 86.92 Last: 170) +Model-Level : 342.0 +Problems : 9 (Average Length: 18.11 Splits: 0) +Lemmas : 40155 (Deleted: 29608) + Binary : 4051 (Ratio: 10.09%) + Ternary : 1252 (Ratio: 3.12%) + Conflict : 40155 (Average Length: 704.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 40155 (Average: 14.43 Max: 425 Sum: 579610) + Executed : 40112 (Average: 14.42 Max: 425 Sum: 579036 Ratio: 99.90%) + Bounded : 43 (Average: 13.35 Max: 27 Sum: 574 Ratio: 0.10%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 1427051 (Binary: 91.3% Ternary: 6.9% Other: 1.8%) + +Memory Peak : 350MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 0.50s +Memory: 350MB (+0MB) +UNSAT +Iteration Time: 0.52s + +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 : 45.593s (Solving: 40.05s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 45.464s + +Choices : 798312 (Domain: 740164) +Conflicts : 48753 (Analyzed: 48750) +Restarts : 562 (Average: 86.74 Last: 170) +Model-Level : 342.0 +Problems : 10 (Average Length: 19.50 Splits: 0) +Lemmas : 48750 (Deleted: 36945) + Binary : 4457 (Ratio: 9.14%) + Ternary : 1345 (Ratio: 2.76%) + Conflict : 48750 (Average Length: 618.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 48750 (Average: 15.54 Max: 425 Sum: 757512) + Executed : 48702 (Average: 15.52 Max: 425 Sum: 756783 Ratio: 99.90%) + Bounded : 48 (Average: 15.19 Max: 32 Sum: 729 Ratio: 0.10%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 1427051 (Binary: 91.3% Ternary: 6.9% Other: 1.8%) + +Memory Peak : 350MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.11s +Memory: 350MB (+0MB) +UNKNOWN +Iteration Time: 9.13s + +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 : 55.642s (Solving: 50.05s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 55.516s + +Choices : 1016661 (Domain: 954156) +Conflicts : 57638 (Analyzed: 57635) +Restarts : 662 (Average: 87.06 Last: 170) +Model-Level : 342.0 +Problems : 11 (Average Length: 20.64 Splits: 0) +Lemmas : 57635 (Deleted: 45039) + Binary : 4924 (Ratio: 8.54%) + Ternary : 1413 (Ratio: 2.45%) + Conflict : 57635 (Average Length: 546.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 57635 (Average: 16.81 Max: 425 Sum: 968595) + Executed : 57580 (Average: 16.79 Max: 425 Sum: 967652 Ratio: 99.90%) + Bounded : 55 (Average: 17.15 Max: 32 Sum: 943 Ratio: 0.10%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 1419174 (Binary: 91.3% Ternary: 6.9% Other: 1.8%) + +Memory Peak : 350MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 10.04s +Memory: 350MB (+0MB) +UNKNOWN +Iteration Time: 10.06s + +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 : 62.902s (Solving: 57.25s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 62.780s + +Choices : 1161152 (Domain: 1096552) +Conflicts : 66008 (Analyzed: 66005) +Restarts : 762 (Average: 86.62 Last: 170) +Model-Level : 342.0 +Problems : 12 (Average Length: 21.58 Splits: 0) +Lemmas : 66005 (Deleted: 51094) + Binary : 5203 (Ratio: 7.88%) + Ternary : 1448 (Ratio: 2.19%) + Conflict : 66005 (Average Length: 507.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 66005 (Average: 16.75 Max: 425 Sum: 1105601) + Executed : 65949 (Average: 16.74 Max: 425 Sum: 1104626 Ratio: 99.91%) + Bounded : 56 (Average: 17.41 Max: 32 Sum: 975 Ratio: 0.09%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 1413716 (Binary: 91.3% Ternary: 6.9% Other: 1.8%) + +Memory Peak : 350MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.24s +Memory: 350MB (+0MB) +UNKNOWN +Iteration Time: 7.27s + +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: 392.0MB +Grounding... [('step', [31]), ('step', [32]), ('step', [33]), ('step', [34]), ('step', [35]), ('check', [35])] +Grounding Time: 0.51s +Memory: 350MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 13 +Time : 70.971s (Solving: 64.47s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 70.852s + +Choices : 1284768 (Domain: 1219461) +Conflicts : 74785 (Analyzed: 74782) +Restarts : 862 (Average: 86.75 Last: 170) +Model-Level : 342.0 +Problems : 13 (Average Length: 22.77 Splits: 0) +Lemmas : 74782 (Deleted: 63176) + Binary : 5453 (Ratio: 7.29%) + Ternary : 1463 (Ratio: 1.96%) + Conflict : 74782 (Average Length: 545.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 74782 (Average: 16.26 Max: 425 Sum: 1216217) + Executed : 74726 (Average: 16.25 Max: 425 Sum: 1215242 Ratio: 99.92%) + Bounded : 56 (Average: 17.41 Max: 32 Sum: 975 Ratio: 0.08%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 1693728 (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: 7.29s +Memory: 365MB (+15MB) +UNKNOWN +Iteration Time: 8.08s + +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: 407.0MB +Grounding... [('step', [36]), ('step', [37]), ('step', [38]), ('step', [39]), ('step', [40]), ('check', [40])] +Grounding Time: 0.52s +Memory: 373MB (+8MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 14 +Time : 78.870s (Solving: 71.50s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 78.752s + +Choices : 1415316 (Domain: 1348961) +Conflicts : 83332 (Analyzed: 83329) +Restarts : 962 (Average: 86.62 Last: 170) +Model-Level : 342.0 +Problems : 14 (Average Length: 24.14 Splits: 0) +Lemmas : 83329 (Deleted: 69478) + Binary : 5644 (Ratio: 6.77%) + Ternary : 1469 (Ratio: 1.76%) + Conflict : 83329 (Average Length: 577.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 83329 (Average: 15.97 Max: 425 Sum: 1331150) + Executed : 83273 (Average: 15.96 Max: 425 Sum: 1330175 Ratio: 99.93%) + Bounded : 56 (Average: 17.41 Max: 32 Sum: 975 Ratio: 0.07%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 1976188 (Binary: 91.3% Ternary: 6.9% Other: 1.8%) + +Memory Peak : 412MB +Max. Length : 35 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.10s +Memory: 388MB (+15MB) +UNKNOWN +Iteration Time: 7.91s + +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.53s +Memory: 398MB (+10MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 15 +Time : 86.505s (Solving: 78.22s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 86.392s + +Choices : 1528948 (Domain: 1462297) +Conflicts : 91782 (Analyzed: 91779) +Restarts : 1062 (Average: 86.42 Last: 172) +Model-Level : 342.0 +Problems : 15 (Average Length: 25.67 Splits: 0) +Lemmas : 91779 (Deleted: 77702) + Binary : 5782 (Ratio: 6.30%) + Ternary : 1485 (Ratio: 1.62%) + Conflict : 91779 (Average Length: 617.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 91779 (Average: 15.56 Max: 425 Sum: 1428419) + Executed : 91723 (Average: 15.55 Max: 425 Sum: 1427444 Ratio: 99.93%) + Bounded : 56 (Average: 17.41 Max: 32 Sum: 975 Ratio: 0.07%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 2258648 (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: 6.80s +Memory: 443MB (+45MB) +UNKNOWN +Iteration Time: 7.65s + +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.67s +Memory: 455MB (+12MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 16 +Time : 95.178s (Solving: 85.82s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 95.068s + +Choices : 1719237 (Domain: 1649561) +Conflicts : 100439 (Analyzed: 100436) +Restarts : 1162 (Average: 86.43 Last: 172) +Model-Level : 342.0 +Problems : 16 (Average Length: 27.31 Splits: 0) +Lemmas : 100436 (Deleted: 88118) + Binary : 5890 (Ratio: 5.86%) + Ternary : 1497 (Ratio: 1.49%) + Conflict : 100436 (Average Length: 661.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 100436 (Average: 15.93 Max: 445 Sum: 1599481) + Executed : 100380 (Average: 15.92 Max: 445 Sum: 1598506 Ratio: 99.94%) + Bounded : 56 (Average: 17.41 Max: 32 Sum: 975 Ratio: 0.06%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 2541108 (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.69s +Memory: 466MB (+11MB) +UNKNOWN +Iteration Time: 8.69s + +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.52s +Memory: 470MB (+4MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 17 +Time : 104.734s (Solving: 94.44s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 104.632s + +Choices : 1955773 (Domain: 1882361) +Conflicts : 108751 (Analyzed: 108748) +Restarts : 1262 (Average: 86.17 Last: 191) +Model-Level : 342.0 +Problems : 17 (Average Length: 29.06 Splits: 0) +Lemmas : 108748 (Deleted: 94301) + Binary : 5959 (Ratio: 5.48%) + Ternary : 1504 (Ratio: 1.38%) + Conflict : 108748 (Average Length: 707.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 108748 (Average: 16.68 Max: 492 Sum: 1813597) + Executed : 108692 (Average: 16.67 Max: 492 Sum: 1812622 Ratio: 99.95%) + Bounded : 56 (Average: 17.41 Max: 32 Sum: 975 Ratio: 0.05%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 2823568 (Binary: 91.3% Ternary: 6.9% Other: 1.8%) + +Memory Peak : 527MB +Max. Length : 50 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.70s +Memory: 489MB (+19MB) +UNKNOWN +Iteration Time: 9.57s + +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.52s +Memory: 494MB (+5MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 18 +Time : 114.629s (Solving: 103.37s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 114.532s + +Choices : 2176886 (Domain: 2100994) +Conflicts : 116955 (Analyzed: 116952) +Restarts : 1362 (Average: 85.87 Last: 191) +Model-Level : 342.0 +Problems : 18 (Average Length: 30.89 Splits: 0) +Lemmas : 116952 (Deleted: 102395) + Binary : 6037 (Ratio: 5.16%) + Ternary : 1504 (Ratio: 1.29%) + Conflict : 116952 (Average Length: 758.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 116952 (Average: 17.21 Max: 550 Sum: 2012615) + Executed : 116896 (Average: 17.20 Max: 550 Sum: 2011640 Ratio: 99.95%) + Bounded : 56 (Average: 17.41 Max: 32 Sum: 975 Ratio: 0.05%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 3106028 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 557MB +Max. Length : 55 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.03s +Memory: 552MB (+58MB) +UNKNOWN +Iteration Time: 9.91s + +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.52s +Memory: 552MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 19 +Time : 125.073s (Solving: 112.84s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 124.984s + +Choices : 2481337 (Domain: 2401648) +Conflicts : 124928 (Analyzed: 124925) +Restarts : 1462 (Average: 85.45 Last: 191) +Model-Level : 342.0 +Problems : 19 (Average Length: 32.79 Splits: 0) +Lemmas : 124925 (Deleted: 110421) + Binary : 6100 (Ratio: 4.88%) + Ternary : 1508 (Ratio: 1.21%) + Conflict : 124925 (Average Length: 788.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 124925 (Average: 18.35 Max: 623 Sum: 2292004) + Executed : 124869 (Average: 18.34 Max: 623 Sum: 2291029 Ratio: 99.96%) + Bounded : 56 (Average: 17.41 Max: 32 Sum: 975 Ratio: 0.04%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 3388488 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 609MB +Max. Length : 60 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.57s +Memory: 557MB (+5MB) +UNKNOWN +Iteration Time: 10.46s + +Iteration 19 +Queue: [(14,70,0,True), (15,75,0,True), (16,80,0,True)] +Grounded Until: 65 +Expected Memory: 620.0MB +Grounding... [('step', [66]), ('step', [67]), ('step', [68]), ('step', [69]), ('step', [70]), ('check', [70])] +Grounding Time: 0.54s +Memory: 562MB (+5MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 20 +Time : 136.349s (Solving: 123.09s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 136.264s + +Choices : 2807665 (Domain: 2723879) +Conflicts : 133654 (Analyzed: 133651) +Restarts : 1562 (Average: 85.56 Last: 191) +Model-Level : 342.0 +Problems : 20 (Average Length: 34.75 Splits: 0) +Lemmas : 133651 (Deleted: 120457) + Binary : 6133 (Ratio: 4.59%) + Ternary : 1520 (Ratio: 1.14%) + Conflict : 133651 (Average Length: 819.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 133651 (Average: 19.38 Max: 700 Sum: 2590670) + Executed : 133595 (Average: 19.38 Max: 700 Sum: 2589695 Ratio: 99.96%) + Bounded : 56 (Average: 17.41 Max: 32 Sum: 975 Ratio: 0.04%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 3670948 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 633MB +Max. Length : 65 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 10.36s +Memory: 583MB (+21MB) +UNKNOWN +Iteration Time: 11.29s + +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.55s +Memory: 584MB (+1MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 21 +Time : 147.638s (Solving: 133.32s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 147.556s + +Choices : 3071576 (Domain: 2985221) +Conflicts : 141582 (Analyzed: 141579) +Restarts : 1662 (Average: 85.19 Last: 191) +Model-Level : 342.0 +Problems : 21 (Average Length: 36.76 Splits: 0) +Lemmas : 141579 (Deleted: 126812) + Binary : 6157 (Ratio: 4.35%) + Ternary : 1524 (Ratio: 1.08%) + Conflict : 141579 (Average Length: 844.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 141579 (Average: 19.96 Max: 742 Sum: 2825891) + Executed : 141523 (Average: 19.95 Max: 742 Sum: 2824916 Ratio: 99.97%) + Bounded : 56 (Average: 17.41 Max: 32 Sum: 975 Ratio: 0.03%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 3953408 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 666MB +Max. Length : 70 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 10.35s +Memory: 609MB (+25MB) +UNKNOWN +Iteration Time: 11.30s + +Iteration 21 +Queue: [(16,80,0,True)] +Grounded Until: 75 +Expected Memory: 672.0MB +Grounding... [('step', [76]), ('step', [77]), ('step', [78]), ('step', [79]), ('step', [80]), ('check', [80])] +Grounding Time: 0.54s +Memory: 609MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 22 +Time : 158.577s (Solving: 143.20s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 158.500s + +Choices : 3358238 (Domain: 3269826) +Conflicts : 149238 (Analyzed: 149235) +Restarts : 1762 (Average: 84.70 Last: 191) +Model-Level : 342.0 +Problems : 22 (Average Length: 38.82 Splits: 0) +Lemmas : 149235 (Deleted: 134589) + Binary : 6234 (Ratio: 4.18%) + Ternary : 1530 (Ratio: 1.03%) + Conflict : 149235 (Average Length: 869.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 149235 (Average: 20.66 Max: 754 Sum: 3083604) + Executed : 149179 (Average: 20.66 Max: 754 Sum: 3082629 Ratio: 99.97%) + Bounded : 56 (Average: 17.41 Max: 32 Sum: 975 Ratio: 0.03%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 4235868 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 694MB +Max. Length : 75 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.99s +Memory: 633MB (+24MB) +UNKNOWN +Iteration Time: 10.96s + +Iteration 22 +Queue: [(4,20,2,True), (5,25,2,True), (6,30,2,True), (7,35,1,True), (8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 80 +Blocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 23 +Time : 169.482s (Solving: 153.97s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 169.412s + +Choices : 3516804 (Domain: 3428390) +Conflicts : 158059 (Analyzed: 158056) +Restarts : 1862 (Average: 84.89 Last: 191) +Model-Level : 342.0 +Problems : 23 (Average Length: 40.70 Splits: 0) +Lemmas : 158056 (Deleted: 142842) + Binary : 6355 (Ratio: 4.02%) + Ternary : 1548 (Ratio: 0.98%) + Conflict : 158056 (Average Length: 846.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 158056 (Average: 20.50 Max: 754 Sum: 3240772) + Executed : 157999 (Average: 20.50 Max: 754 Sum: 3239720 Ratio: 99.97%) + Bounded : 57 (Average: 18.46 Max: 77 Sum: 1052 Ratio: 0.03%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 4235868 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 694MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 10.86s +Memory: 633MB (+0MB) +UNKNOWN +Iteration Time: 10.91s + +Iteration 23 +Queue: [(5,25,2,True), (6,30,2,True), (7,35,1,True), (8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 80 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 24 +Time : 177.205s (Solving: 161.58s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 177.140s + +Choices : 3640654 (Domain: 3551789) +Conflicts : 166015 (Analyzed: 166012) +Restarts : 1962 (Average: 84.61 Last: 191) +Model-Level : 342.0 +Problems : 24 (Average Length: 42.42 Splits: 0) +Lemmas : 166012 (Deleted: 148147) + Binary : 6662 (Ratio: 4.01%) + Ternary : 1582 (Ratio: 0.95%) + Conflict : 166012 (Average Length: 816.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 166012 (Average: 20.22 Max: 754 Sum: 3357497) + Executed : 165954 (Average: 20.22 Max: 754 Sum: 3356368 Ratio: 99.97%) + Bounded : 58 (Average: 19.47 Max: 77 Sum: 1129 Ratio: 0.03%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 4235868 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 694MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.69s +Memory: 633MB (+0MB) +UNKNOWN +Iteration Time: 7.73s + +Iteration 24 +Queue: [(6,30,2,True), (7,35,1,True), (8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 80 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 25 +Time : 181.641s (Solving: 165.87s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 181.580s + +Choices : 3697616 (Domain: 3608652) +Conflicts : 173456 (Analyzed: 173453) +Restarts : 2062 (Average: 84.12 Last: 191) +Model-Level : 342.0 +Problems : 25 (Average Length: 44.00 Splits: 0) +Lemmas : 173453 (Deleted: 155618) + Binary : 6823 (Ratio: 3.93%) + Ternary : 1599 (Ratio: 0.92%) + Conflict : 173453 (Average Length: 792.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 173453 (Average: 19.64 Max: 754 Sum: 3406806) + Executed : 173392 (Average: 19.63 Max: 754 Sum: 3405441 Ratio: 99.96%) + Bounded : 61 (Average: 22.38 Max: 82 Sum: 1365 Ratio: 0.04%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 4235868 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 694MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 4.39s +Memory: 633MB (+0MB) +UNKNOWN +Iteration Time: 4.44s + +Iteration 25 +Queue: [(7,35,1,True), (8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 80 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 26 +Time : 186.551s (Solving: 170.66s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 186.496s + +Choices : 3760793 (Domain: 3671784) +Conflicts : 180842 (Analyzed: 180839) +Restarts : 2162 (Average: 83.64 Last: 191) +Model-Level : 342.0 +Problems : 26 (Average Length: 45.46 Splits: 0) +Lemmas : 180839 (Deleted: 162775) + Binary : 6937 (Ratio: 3.84%) + Ternary : 1611 (Ratio: 0.89%) + Conflict : 180839 (Average Length: 769.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 180839 (Average: 19.15 Max: 754 Sum: 3462225) + Executed : 180775 (Average: 19.14 Max: 754 Sum: 3460619 Ratio: 99.95%) + Bounded : 64 (Average: 25.09 Max: 82 Sum: 1606 Ratio: 0.05%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 4235854 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 694MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 4.87s +Memory: 633MB (+0MB) +UNKNOWN +Iteration Time: 4.91s + +Iteration 26 +Queue: [(8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 80 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 27 +Time : 191.978s (Solving: 175.97s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 191.924s + +Choices : 3832809 (Domain: 3743762) +Conflicts : 188535 (Analyzed: 188532) +Restarts : 2262 (Average: 83.35 Last: 191) +Model-Level : 342.0 +Problems : 27 (Average Length: 46.81 Splits: 0) +Lemmas : 188532 (Deleted: 169800) + Binary : 7065 (Ratio: 3.75%) + Ternary : 1629 (Ratio: 0.86%) + Conflict : 188532 (Average Length: 745.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 188532 (Average: 18.71 Max: 754 Sum: 3526550) + Executed : 188466 (Average: 18.70 Max: 754 Sum: 3524788 Ratio: 99.95%) + Bounded : 66 (Average: 26.70 Max: 82 Sum: 1762 Ratio: 0.05%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 4228448 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 694MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 5.39s +Memory: 633MB (+0MB) +UNKNOWN +Iteration Time: 5.43s + +Iteration 27 +Queue: [(9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 80 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 28 +Time : 198.430s (Solving: 182.29s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 198.376s + +Choices : 3955460 (Domain: 3866354) +Conflicts : 196207 (Analyzed: 196204) +Restarts : 2362 (Average: 83.07 Last: 191) +Model-Level : 342.0 +Problems : 28 (Average Length: 48.07 Splits: 0) +Lemmas : 196204 (Deleted: 177120) + Binary : 7231 (Ratio: 3.69%) + Ternary : 1659 (Ratio: 0.85%) + Conflict : 196204 (Average Length: 724.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 196204 (Average: 18.55 Max: 754 Sum: 3638806) + Executed : 196136 (Average: 18.54 Max: 754 Sum: 3636888 Ratio: 99.95%) + Bounded : 68 (Average: 28.21 Max: 82 Sum: 1918 Ratio: 0.05%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 4228448 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 694MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.41s +Memory: 633MB (+0MB) +UNKNOWN +Iteration Time: 6.46s + +Iteration 28 +Queue: [(10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 80 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 29 +Time : 204.720s (Solving: 188.45s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 204.668s + +Choices : 4043753 (Domain: 3954602) +Conflicts : 203794 (Analyzed: 203791) +Restarts : 2462 (Average: 82.77 Last: 191) +Model-Level : 342.0 +Problems : 29 (Average Length: 49.24 Splits: 0) +Lemmas : 203791 (Deleted: 184401) + Binary : 7386 (Ratio: 3.62%) + Ternary : 1686 (Ratio: 0.83%) + Conflict : 203791 (Average Length: 704.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 203791 (Average: 18.25 Max: 754 Sum: 3718420) + Executed : 203718 (Average: 18.23 Max: 754 Sum: 3716109 Ratio: 99.94%) + Bounded : 73 (Average: 31.66 Max: 82 Sum: 2311 Ratio: 0.06%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 4228448 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 694MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.25s +Memory: 633MB (+0MB) +UNKNOWN +Iteration Time: 6.30s + +Iteration 29 +Queue: [(11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 80 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 30 +Time : 213.451s (Solving: 197.07s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 213.404s + +Choices : 4249555 (Domain: 4159913) +Conflicts : 211503 (Analyzed: 211500) +Restarts : 2562 (Average: 82.55 Last: 191) +Model-Level : 342.0 +Problems : 30 (Average Length: 50.33 Splits: 0) +Lemmas : 211500 (Deleted: 191496) + Binary : 7652 (Ratio: 3.62%) + Ternary : 1714 (Ratio: 0.81%) + Conflict : 211500 (Average Length: 687.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 211500 (Average: 18.50 Max: 754 Sum: 3912642) + Executed : 211425 (Average: 18.49 Max: 754 Sum: 3910177 Ratio: 99.94%) + Bounded : 75 (Average: 32.87 Max: 82 Sum: 2465 Ratio: 0.06%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 4225816 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 694MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.69s +Memory: 633MB (+0MB) +UNKNOWN +Iteration Time: 8.74s + +Iteration 30 +Queue: [(12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 80 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 31 +Time : 224.467s (Solving: 207.97s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 224.424s + +Choices : 4653740 (Domain: 4561248) +Conflicts : 220294 (Analyzed: 220291) +Restarts : 2662 (Average: 82.75 Last: 191) +Model-Level : 342.0 +Problems : 31 (Average Length: 51.35 Splits: 0) +Lemmas : 220291 (Deleted: 200210) + Binary : 8250 (Ratio: 3.75%) + Ternary : 1882 (Ratio: 0.85%) + Conflict : 220291 (Average Length: 670.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 220291 (Average: 19.52 Max: 754 Sum: 4300710) + Executed : 220215 (Average: 19.51 Max: 754 Sum: 4298168 Ratio: 99.94%) + Bounded : 76 (Average: 33.45 Max: 82 Sum: 2542 Ratio: 0.06%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 4225816 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 694MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 10.98s +Memory: 633MB (+0MB) +UNKNOWN +Iteration Time: 11.02s + +Iteration 31 +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), (21,105,0,True)] +Grounded Until: 80 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 32 +Time : 233.236s (Solving: 216.62s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 233.200s + +Choices : 4953085 (Domain: 4859154) +Conflicts : 228715 (Analyzed: 228712) +Restarts : 2762 (Average: 82.81 Last: 191) +Model-Level : 342.0 +Problems : 32 (Average Length: 52.31 Splits: 0) +Lemmas : 228712 (Deleted: 206107) + Binary : 8628 (Ratio: 3.77%) + Ternary : 2070 (Ratio: 0.91%) + Conflict : 228712 (Average Length: 654.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 228712 (Average: 20.04 Max: 754 Sum: 4584277) + Executed : 228635 (Average: 20.03 Max: 754 Sum: 4581658 Ratio: 99.94%) + Bounded : 77 (Average: 34.01 Max: 82 Sum: 2619 Ratio: 0.06%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 4225816 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 694MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.73s +Memory: 633MB (+0MB) +UNKNOWN +Iteration Time: 8.78s + +Iteration 32 +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), (21,105,0,True)] +Grounded Until: 80 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 33 +Time : 240.028s (Solving: 223.28s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 239.996s + +Choices : 5132538 (Domain: 5037344) +Conflicts : 236773 (Analyzed: 236770) +Restarts : 2862 (Average: 82.73 Last: 191) +Model-Level : 342.0 +Problems : 33 (Average Length: 53.21 Splits: 0) +Lemmas : 236770 (Deleted: 213808) + Binary : 8898 (Ratio: 3.76%) + Ternary : 2124 (Ratio: 0.90%) + Conflict : 236770 (Average Length: 641.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 236770 (Average: 20.07 Max: 754 Sum: 4750832) + Executed : 236691 (Average: 20.05 Max: 754 Sum: 4748059 Ratio: 99.94%) + Bounded : 79 (Average: 35.10 Max: 82 Sum: 2773 Ratio: 0.06%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 4225816 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 694MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.75s +Memory: 633MB (+0MB) +UNKNOWN +Iteration Time: 6.80s + +Iteration 33 +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), (21,105,0,True)] +Grounded Until: 80 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 34 +Time : 249.882s (Solving: 233.02s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 249.852s + +Choices : 5566152 (Domain: 5467660) +Conflicts : 245591 (Analyzed: 245588) +Restarts : 2962 (Average: 82.91 Last: 191) +Model-Level : 342.0 +Problems : 34 (Average Length: 54.06 Splits: 0) +Lemmas : 245588 (Deleted: 223282) + Binary : 9070 (Ratio: 3.69%) + Ternary : 2174 (Ratio: 0.89%) + Conflict : 245588 (Average Length: 629.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 245588 (Average: 21.02 Max: 754 Sum: 5163003) + Executed : 245509 (Average: 21.01 Max: 754 Sum: 5160230 Ratio: 99.95%) + Bounded : 79 (Average: 35.10 Max: 82 Sum: 2773 Ratio: 0.05%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 4225816 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 694MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.82s +Memory: 633MB (+0MB) +UNKNOWN +Iteration Time: 9.86s + +Iteration 34 +Queue: [(16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 80 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 35 +Time : 263.288s (Solving: 246.28s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 263.264s + +Choices : 6273833 (Domain: 6170450) +Conflicts : 254477 (Analyzed: 254474) +Restarts : 3062 (Average: 83.11 Last: 191) +Model-Level : 342.0 +Problems : 35 (Average Length: 54.86 Splits: 0) +Lemmas : 254474 (Deleted: 231326) + Binary : 9423 (Ratio: 3.70%) + Ternary : 2221 (Ratio: 0.87%) + Conflict : 254474 (Average Length: 626.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 254474 (Average: 22.96 Max: 754 Sum: 5843531) + Executed : 254395 (Average: 22.95 Max: 754 Sum: 5840758 Ratio: 99.95%) + Bounded : 79 (Average: 35.10 Max: 82 Sum: 2773 Ratio: 0.05%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 4225816 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 694MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 13.36s +Memory: 633MB (+0MB) +UNKNOWN +Iteration Time: 13.41s + +Iteration 35 +Queue: [(17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 80 +Expected Memory: 696.0MB +Grounding... [('step', [81]), ('step', [82]), ('step', [83]), ('step', [84]), ('step', [85]), ('check', [85])] +Grounding Time: 0.54s +Memory: 633MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 36 +Time : 272.194s (Solving: 254.11s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 272.176s + +Choices : 6398657 (Domain: 6295114) +Conflicts : 263018 (Analyzed: 263015) +Restarts : 3162 (Average: 83.18 Last: 191) +Model-Level : 342.0 +Problems : 36 (Average Length: 55.75 Splits: 0) +Lemmas : 263015 (Deleted: 239359) + Binary : 9500 (Ratio: 3.61%) + Ternary : 2234 (Ratio: 0.85%) + Conflict : 263015 (Average Length: 631.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 263015 (Average: 22.59 Max: 764 Sum: 5941465) + Executed : 262936 (Average: 22.58 Max: 764 Sum: 5938692 Ratio: 99.95%) + Bounded : 79 (Average: 35.10 Max: 82 Sum: 2773 Ratio: 0.05%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 4508276 (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: 7.95s +Memory: 655MB (+22MB) +UNKNOWN +Iteration Time: 8.92s + +Iteration 36 +Queue: [(18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 85 +Expected Memory: 718.0MB +Grounding... [('step', [86]), ('step', [87]), ('step', [88]), ('step', [89]), ('step', [90]), ('check', [90])] +Grounding Time: 0.56s +Memory: 655MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 37 +Time : 283.287s (Solving: 264.05s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 283.276s + +Choices : 6562852 (Domain: 6459050) +Conflicts : 271179 (Analyzed: 271176) +Restarts : 3262 (Average: 83.13 Last: 191) +Model-Level : 342.0 +Problems : 37 (Average Length: 56.73 Splits: 0) +Lemmas : 271176 (Deleted: 248170) + Binary : 9622 (Ratio: 3.55%) + Ternary : 2239 (Ratio: 0.83%) + Conflict : 271176 (Average Length: 637.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 271176 (Average: 22.41 Max: 876 Sum: 6075811) + Executed : 271097 (Average: 22.40 Max: 876 Sum: 6073038 Ratio: 99.95%) + Bounded : 79 (Average: 35.10 Max: 82 Sum: 2773 Ratio: 0.05%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 4790736 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 748MB +Max. Length : 85 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 10.07s +Memory: 736MB (+81MB) +UNKNOWN +Iteration Time: 11.11s + +Iteration 37 +Queue: [(19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 90 +Expected Memory: 817.0MB +Grounding... [('step', [91]), ('step', [92]), ('step', [93]), ('step', [94]), ('step', [95]), ('check', [95])] +Grounding Time: 0.55s +Memory: 736MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 38 +Time : 293.840s (Solving: 273.48s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 293.836s + +Choices : 6671866 (Domain: 6568005) +Conflicts : 279124 (Analyzed: 279121) +Restarts : 3362 (Average: 83.02 Last: 191) +Model-Level : 342.0 +Problems : 38 (Average Length: 57.79 Splits: 0) +Lemmas : 279121 (Deleted: 256127) + Binary : 9674 (Ratio: 3.47%) + Ternary : 2257 (Ratio: 0.81%) + Conflict : 279121 (Average Length: 646.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 279121 (Average: 22.04 Max: 876 Sum: 6152398) + Executed : 279042 (Average: 22.03 Max: 876 Sum: 6149625 Ratio: 99.95%) + Bounded : 79 (Average: 35.10 Max: 82 Sum: 2773 Ratio: 0.05%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 5073196 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 820MB +Max. Length : 90 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.56s +Memory: 740MB (+4MB) +UNKNOWN +Iteration Time: 10.57s + +Iteration 38 +Queue: [(20,100,0,True), (21,105,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 (+51MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 39 +Time : 304.286s (Solving: 282.43s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 304.288s + +Choices : 6760726 (Domain: 6656831) +Conflicts : 286455 (Analyzed: 286452) +Restarts : 3462 (Average: 82.74 Last: 191) +Model-Level : 342.0 +Problems : 39 (Average Length: 58.92 Splits: 0) +Lemmas : 286452 (Deleted: 263088) + Binary : 9687 (Ratio: 3.38%) + Ternary : 2263 (Ratio: 0.79%) + Conflict : 286452 (Average Length: 656.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 286452 (Average: 21.67 Max: 876 Sum: 6207146) + Executed : 286373 (Average: 21.66 Max: 876 Sum: 6204373 Ratio: 99.96%) + Bounded : 79 (Average: 35.10 Max: 82 Sum: 2773 Ratio: 0.04%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 5355656 (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: 9.09s +Memory: 795MB (+4MB) +UNKNOWN +Iteration Time: 10.46s + +Iteration 39 +Queue: [(21,105,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.53s +Memory: 795MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 40 +Time : 315.068s (Solving: 292.06s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 315.076s + +Choices : 6864512 (Domain: 6760467) +Conflicts : 293985 (Analyzed: 293982) +Restarts : 3562 (Average: 82.53 Last: 191) +Model-Level : 342.0 +Problems : 40 (Average Length: 60.12 Splits: 0) +Lemmas : 293982 (Deleted: 270697) + Binary : 9715 (Ratio: 3.30%) + Ternary : 2270 (Ratio: 0.77%) + Conflict : 293982 (Average Length: 666.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 293982 (Average: 21.35 Max: 876 Sum: 6275058) + Executed : 293903 (Average: 21.34 Max: 876 Sum: 6272285 Ratio: 99.96%) + Bounded : 79 (Average: 35.10 Max: 82 Sum: 2773 Ratio: 0.04%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 5638116 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 890MB +Max. Length : 100 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.77s +Memory: 805MB (+10MB) +UNKNOWN +Iteration Time: 10.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,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Blocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 41 +Time : 318.659s (Solving: 295.48s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 318.668s + +Choices : 6934107 (Domain: 6830062) +Conflicts : 301791 (Analyzed: 301788) +Restarts : 3662 (Average: 82.41 Last: 191) +Model-Level : 342.0 +Problems : 41 (Average Length: 61.27 Splits: 0) +Lemmas : 301788 (Deleted: 276515) + Binary : 9822 (Ratio: 3.25%) + Ternary : 2275 (Ratio: 0.75%) + Conflict : 301788 (Average Length: 655.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 301788 (Average: 20.99 Max: 876 Sum: 6335269) + Executed : 301703 (Average: 20.98 Max: 876 Sum: 6332278 Ratio: 99.95%) + Bounded : 85 (Average: 35.19 Max: 107 Sum: 2991 Ratio: 0.05%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 5638116 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 890MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 3.53s +Memory: 809MB (+4MB) +UNKNOWN +Iteration Time: 3.59s + +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,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 42 +Time : 323.684s (Solving: 300.35s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 323.696s + +Choices : 6974685 (Domain: 6870640) +Conflicts : 309686 (Analyzed: 309683) +Restarts : 3762 (Average: 82.32 Last: 191) +Model-Level : 342.0 +Problems : 42 (Average Length: 62.36 Splits: 0) +Lemmas : 309683 (Deleted: 283974) + Binary : 9891 (Ratio: 3.19%) + Ternary : 2299 (Ratio: 0.74%) + Conflict : 309683 (Average Length: 644.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 309683 (Average: 20.57 Max: 876 Sum: 6369390) + Executed : 309597 (Average: 20.56 Max: 876 Sum: 6366292 Ratio: 99.95%) + Bounded : 86 (Average: 36.02 Max: 107 Sum: 3098 Ratio: 0.05%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 5638088 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 890MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 4.98s +Memory: 809MB (+0MB) +UNKNOWN +Iteration Time: 5.03s + +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,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 43 +Time : 330.216s (Solving: 306.70s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 330.228s + +Choices : 7068227 (Domain: 6963140) +Conflicts : 317567 (Analyzed: 317564) +Restarts : 3862 (Average: 82.23 Last: 191) +Model-Level : 342.0 +Problems : 43 (Average Length: 63.40 Splits: 0) +Lemmas : 317564 (Deleted: 291677) + Binary : 10079 (Ratio: 3.17%) + Ternary : 2318 (Ratio: 0.73%) + Conflict : 317564 (Average Length: 638.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 317564 (Average: 20.31 Max: 876 Sum: 6450697) + Executed : 317478 (Average: 20.30 Max: 876 Sum: 6447599 Ratio: 99.95%) + Bounded : 86 (Average: 36.02 Max: 107 Sum: 3098 Ratio: 0.05%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 5638074 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 890MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.47s +Memory: 809MB (+0MB) +UNKNOWN +Iteration Time: 6.54s + +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,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 44 +Time : 338.125s (Solving: 314.45s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 338.140s + +Choices : 7173391 (Domain: 7065161) +Conflicts : 326614 (Analyzed: 326611) +Restarts : 3962 (Average: 82.44 Last: 191) +Model-Level : 342.0 +Problems : 44 (Average Length: 64.39 Splits: 0) +Lemmas : 326611 (Deleted: 301106) + Binary : 10290 (Ratio: 3.15%) + Ternary : 2368 (Ratio: 0.73%) + Conflict : 326611 (Average Length: 634.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 326611 (Average: 20.03 Max: 876 Sum: 6541415) + Executed : 326525 (Average: 20.02 Max: 876 Sum: 6538317 Ratio: 99.95%) + Bounded : 86 (Average: 36.02 Max: 107 Sum: 3098 Ratio: 0.05%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 5638074 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 890MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.85s +Memory: 809MB (+0MB) +UNKNOWN +Iteration Time: 7.92s + +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,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 45 +Time : 345.040s (Solving: 321.19s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 345.056s + +Choices : 7264614 (Domain: 7155447) +Conflicts : 334719 (Analyzed: 334716) +Restarts : 4062 (Average: 82.40 Last: 191) +Model-Level : 342.0 +Problems : 45 (Average Length: 65.33 Splits: 0) +Lemmas : 334716 (Deleted: 307557) + Binary : 10432 (Ratio: 3.12%) + Ternary : 2392 (Ratio: 0.71%) + Conflict : 334716 (Average Length: 639.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 334716 (Average: 19.77 Max: 876 Sum: 6616656) + Executed : 334628 (Average: 19.76 Max: 876 Sum: 6613354 Ratio: 99.95%) + Bounded : 88 (Average: 37.52 Max: 107 Sum: 3302 Ratio: 0.05%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 5638074 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 890MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.86s +Memory: 809MB (+0MB) +UNKNOWN +Iteration Time: 6.92s + +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,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 46 +Time : 351.600s (Solving: 327.60s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 351.620s + +Choices : 7343800 (Domain: 7234337) +Conflicts : 342685 (Analyzed: 342682) +Restarts : 4162 (Average: 82.34 Last: 191) +Model-Level : 342.0 +Problems : 46 (Average Length: 66.24 Splits: 0) +Lemmas : 342682 (Deleted: 315338) + Binary : 10544 (Ratio: 3.08%) + Ternary : 2424 (Ratio: 0.71%) + Conflict : 342682 (Average Length: 631.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 342682 (Average: 19.51 Max: 876 Sum: 6685436) + Executed : 342592 (Average: 19.50 Max: 876 Sum: 6681925 Ratio: 99.95%) + Bounded : 90 (Average: 39.01 Max: 107 Sum: 3511 Ratio: 0.05%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 5638074 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 890MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.51s +Memory: 809MB (+0MB) +UNKNOWN +Iteration Time: 6.57s + +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,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 47 +Time : 358.120s (Solving: 333.95s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 358.144s + +Choices : 7438404 (Domain: 7328731) +Conflicts : 350923 (Analyzed: 350920) +Restarts : 4262 (Average: 82.34 Last: 191) +Model-Level : 342.0 +Problems : 47 (Average Length: 67.11 Splits: 0) +Lemmas : 350920 (Deleted: 322985) + Binary : 10662 (Ratio: 3.04%) + Ternary : 2447 (Ratio: 0.70%) + Conflict : 350920 (Average Length: 626.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 350920 (Average: 19.28 Max: 876 Sum: 6767402) + Executed : 350827 (Average: 19.27 Max: 876 Sum: 6763580 Ratio: 99.94%) + Bounded : 93 (Average: 41.10 Max: 107 Sum: 3822 Ratio: 0.06%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 5638061 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 890MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.46s +Memory: 809MB (+0MB) +UNKNOWN +Iteration Time: 6.53s + +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,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 48 +Time : 365.547s (Solving: 341.22s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 365.572s + +Choices : 7593049 (Domain: 7482577) +Conflicts : 359307 (Analyzed: 359304) +Restarts : 4362 (Average: 82.37 Last: 191) +Model-Level : 342.0 +Problems : 48 (Average Length: 67.94 Splits: 0) +Lemmas : 359304 (Deleted: 330845) + Binary : 10802 (Ratio: 3.01%) + Ternary : 2461 (Ratio: 0.68%) + Conflict : 359304 (Average Length: 625.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 359304 (Average: 19.22 Max: 876 Sum: 6904978) + Executed : 359211 (Average: 19.21 Max: 876 Sum: 6901156 Ratio: 99.94%) + Bounded : 93 (Average: 41.10 Max: 107 Sum: 3822 Ratio: 0.06%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 5638035 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 890MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.38s +Memory: 809MB (+0MB) +UNKNOWN +Iteration Time: 7.43s + +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,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 49 +Time : 371.428s (Solving: 346.95s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 371.456s + +Choices : 7732992 (Domain: 7622100) +Conflicts : 367502 (Analyzed: 367499) +Restarts : 4462 (Average: 82.36 Last: 191) +Model-Level : 342.0 +Problems : 49 (Average Length: 68.73 Splits: 0) +Lemmas : 367499 (Deleted: 338933) + Binary : 10884 (Ratio: 2.96%) + Ternary : 2473 (Ratio: 0.67%) + Conflict : 367499 (Average Length: 619.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 367499 (Average: 19.13 Max: 876 Sum: 7030450) + Executed : 367406 (Average: 19.12 Max: 876 Sum: 7026628 Ratio: 99.95%) + Bounded : 93 (Average: 41.10 Max: 107 Sum: 3822 Ratio: 0.05%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 5638035 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 890MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 5.83s +Memory: 809MB (+0MB) +UNKNOWN +Iteration Time: 5.89s + +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,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 50 +Time : 382.756s (Solving: 358.12s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 382.784s + +Choices : 8053244 (Domain: 7940877) +Conflicts : 377078 (Analyzed: 377075) +Restarts : 4562 (Average: 82.66 Last: 191) +Model-Level : 342.0 +Problems : 50 (Average Length: 69.50 Splits: 0) +Lemmas : 377075 (Deleted: 348779) + Binary : 11155 (Ratio: 2.96%) + Ternary : 2499 (Ratio: 0.66%) + Conflict : 377075 (Average Length: 631.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 377075 (Average: 19.42 Max: 876 Sum: 7323736) + Executed : 376981 (Average: 19.41 Max: 876 Sum: 7319807 Ratio: 99.95%) + Bounded : 94 (Average: 41.80 Max: 107 Sum: 3929 Ratio: 0.05%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 5638035 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 890MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 11.27s +Memory: 809MB (+0MB) +UNKNOWN +Iteration Time: 11.33s + +Iteration 50 +Queue: [(17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 51 +Time : 389.628s (Solving: 364.81s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 389.660s + +Choices : 8221669 (Domain: 8109017) +Conflicts : 385439 (Analyzed: 385436) +Restarts : 4662 (Average: 82.68 Last: 191) +Model-Level : 342.0 +Problems : 51 (Average Length: 70.24 Splits: 0) +Lemmas : 385436 (Deleted: 355906) + Binary : 11225 (Ratio: 2.91%) + Ternary : 2517 (Ratio: 0.65%) + Conflict : 385436 (Average Length: 629.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 385436 (Average: 19.38 Max: 876 Sum: 7471539) + Executed : 385340 (Average: 19.37 Max: 876 Sum: 7467399 Ratio: 99.94%) + Bounded : 96 (Average: 43.12 Max: 107 Sum: 4140 Ratio: 0.06%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 5638009 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 937MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.81s +Memory: 873MB (+64MB) +UNKNOWN +Iteration Time: 6.88s + +Iteration 51 +Queue: [(18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 52 +Time : 397.575s (Solving: 372.59s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 397.608s + +Choices : 8449254 (Domain: 8336166) +Conflicts : 394414 (Analyzed: 394411) +Restarts : 4762 (Average: 82.82 Last: 191) +Model-Level : 342.0 +Problems : 52 (Average Length: 70.94 Splits: 0) +Lemmas : 394411 (Deleted: 366122) + Binary : 11344 (Ratio: 2.88%) + Ternary : 2540 (Ratio: 0.64%) + Conflict : 394411 (Average Length: 628.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 394411 (Average: 19.47 Max: 876 Sum: 7677831) + Executed : 394315 (Average: 19.46 Max: 876 Sum: 7673691 Ratio: 99.95%) + Bounded : 96 (Average: 43.12 Max: 107 Sum: 4140 Ratio: 0.05%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 5637995 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 937MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.89s +Memory: 873MB (+0MB) +UNKNOWN +Iteration Time: 7.95s + +Iteration 52 +Queue: [(19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 53 +Time : 408.083s (Solving: 382.91s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 408.116s + +Choices : 8800252 (Domain: 8686603) +Conflicts : 403782 (Analyzed: 403779) +Restarts : 4862 (Average: 83.05 Last: 191) +Model-Level : 342.0 +Problems : 53 (Average Length: 71.62 Splits: 0) +Lemmas : 403779 (Deleted: 374741) + Binary : 11463 (Ratio: 2.84%) + Ternary : 2551 (Ratio: 0.63%) + Conflict : 403779 (Average Length: 633.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 403779 (Average: 19.81 Max: 876 Sum: 7999561) + Executed : 403683 (Average: 19.80 Max: 876 Sum: 7995421 Ratio: 99.95%) + Bounded : 96 (Average: 43.12 Max: 107 Sum: 4140 Ratio: 0.05%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 5637995 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 937MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 10.43s +Memory: 873MB (+0MB) +UNKNOWN +Iteration Time: 10.51s + +Iteration 53 +Queue: [(20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 54 +Time : 418.869s (Solving: 393.52s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 418.908s + +Choices : 9118399 (Domain: 9004398) +Conflicts : 412694 (Analyzed: 412691) +Restarts : 4962 (Average: 83.17 Last: 191) +Model-Level : 342.0 +Problems : 54 (Average Length: 72.28 Splits: 0) +Lemmas : 412691 (Deleted: 383736) + Binary : 11611 (Ratio: 2.81%) + Ternary : 2564 (Ratio: 0.62%) + Conflict : 412691 (Average Length: 640.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 412691 (Average: 20.08 Max: 920 Sum: 8284933) + Executed : 412595 (Average: 20.07 Max: 920 Sum: 8280793 Ratio: 99.95%) + Bounded : 96 (Average: 43.12 Max: 107 Sum: 4140 Ratio: 0.05%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 5637995 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 937MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 10.72s +Memory: 873MB (+0MB) +UNKNOWN +Iteration Time: 10.79s + +Iteration 54 +Queue: [(21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 55 +Time : 425.655s (Solving: 400.12s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 425.696s + +Choices : 9238131 (Domain: 9124106) +Conflicts : 420661 (Analyzed: 420658) +Restarts : 5062 (Average: 83.10 Last: 191) +Model-Level : 342.0 +Problems : 55 (Average Length: 72.91 Splits: 0) +Lemmas : 420658 (Deleted: 390241) + Binary : 11654 (Ratio: 2.77%) + Ternary : 2607 (Ratio: 0.62%) + Conflict : 420658 (Average Length: 637.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 420658 (Average: 19.93 Max: 974 Sum: 8384958) + Executed : 420559 (Average: 19.92 Max: 974 Sum: 8380507 Ratio: 99.95%) + Bounded : 99 (Average: 44.96 Max: 107 Sum: 4451 Ratio: 0.05%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 5637995 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 937MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.72s +Memory: 873MB (+0MB) +UNKNOWN +Iteration Time: 6.79s + +Iteration 55 +Queue: [(22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Expected Memory: 954.0MB +Grounding... [('step', [106]), ('step', [107]), ('step', [108]), ('step', [109]), ('step', [110]), ('check', [110])] +Grounding Time: 0.74s +Memory: 875MB (+2MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 56 +Time : 437.079s (Solving: 409.98s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 437.124s + +Choices : 9432728 (Domain: 9318191) +Conflicts : 428948 (Analyzed: 428945) +Restarts : 5162 (Average: 83.10 Last: 191) +Model-Level : 342.0 +Problems : 56 (Average Length: 73.61 Splits: 0) +Lemmas : 428945 (Deleted: 397969) + Binary : 11739 (Ratio: 2.74%) + Ternary : 2618 (Ratio: 0.61%) + Conflict : 428945 (Average Length: 638.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 428945 (Average: 19.92 Max: 974 Sum: 8544519) + Executed : 428846 (Average: 19.91 Max: 974 Sum: 8540068 Ratio: 99.95%) + Bounded : 99 (Average: 44.96 Max: 107 Sum: 4451 Ratio: 0.05%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 5920441 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 988MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 10.05s +Memory: 903MB (+28MB) +UNKNOWN +Iteration Time: 11.44s + +Iteration 56 +Queue: [(23,115,0,True)] +Grounded Until: 110 +Expected Memory: 984.0MB +Grounding... [('step', [111]), ('step', [112]), ('step', [113]), ('step', [114]), ('step', [115]), ('check', [115])] +Grounding Time: 0.52s +Memory: 903MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 57 +Time : 446.775s (Solving: 418.49s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 446.824s + +Choices : 9543995 (Domain: 9428603) +Conflicts : 437071 (Analyzed: 437068) +Restarts : 5262 (Average: 83.06 Last: 191) +Model-Level : 342.0 +Problems : 57 (Average Length: 74.37 Splits: 0) +Lemmas : 437068 (Deleted: 406357) + Binary : 11771 (Ratio: 2.69%) + Ternary : 2623 (Ratio: 0.60%) + Conflict : 437068 (Average Length: 642.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 437068 (Average: 19.72 Max: 974 Sum: 8617371) + Executed : 436969 (Average: 19.71 Max: 974 Sum: 8612920 Ratio: 99.95%) + Bounded : 99 (Average: 44.96 Max: 107 Sum: 4451 Ratio: 0.05%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 6202901 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1017MB +Max. Length : 110 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.66s +Memory: 918MB (+15MB) +UNKNOWN +Iteration Time: 9.71s + +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,2,False), (22,110,1,True), (23,115,1,True)] +Grounded Until: 115 +Blocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 58 +Time : 450.531s (Solving: 422.07s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 450.580s + +Choices : 9601215 (Domain: 9485823) +Conflicts : 444891 (Analyzed: 444888) +Restarts : 5362 (Average: 82.97 Last: 191) +Model-Level : 342.0 +Problems : 58 (Average Length: 75.10 Splits: 0) +Lemmas : 444888 (Deleted: 413835) + Binary : 11851 (Ratio: 2.66%) + Ternary : 2636 (Ratio: 0.59%) + Conflict : 444888 (Average Length: 641.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 444888 (Average: 19.48 Max: 974 Sum: 8665755) + Executed : 444789 (Average: 19.47 Max: 974 Sum: 8661304 Ratio: 99.95%) + Bounded : 99 (Average: 44.96 Max: 107 Sum: 4451 Ratio: 0.05%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 6202901 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1017MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 3.70s +Memory: 927MB (+9MB) +UNKNOWN +Iteration Time: 3.76s + +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,2,False), (22,110,1,True), (23,115,1,True)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 59 +Time : 454.490s (Solving: 425.86s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 454.540s + +Choices : 9639038 (Domain: 9523646) +Conflicts : 452642 (Analyzed: 452639) +Restarts : 5462 (Average: 82.87 Last: 191) +Model-Level : 342.0 +Problems : 59 (Average Length: 75.81 Splits: 0) +Lemmas : 452639 (Deleted: 421448) + Binary : 11869 (Ratio: 2.62%) + Ternary : 2650 (Ratio: 0.59%) + Conflict : 452639 (Average Length: 635.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 452639 (Average: 19.21 Max: 974 Sum: 8694769) + Executed : 452540 (Average: 19.20 Max: 974 Sum: 8690318 Ratio: 99.95%) + Bounded : 99 (Average: 44.96 Max: 107 Sum: 4451 Ratio: 0.05%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 6202901 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1017MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 3.90s +Memory: 927MB (+0MB) +UNKNOWN +Iteration Time: 3.96s + +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,2,False), (22,110,1,True), (23,115,1,True)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 60 +Time : 462.950s (Solving: 434.15s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 463.008s + +Choices : 9725676 (Domain: 9609888) +Conflicts : 462715 (Analyzed: 462712) +Restarts : 5562 (Average: 83.19 Last: 191) +Model-Level : 342.0 +Problems : 60 (Average Length: 76.50 Splits: 0) +Lemmas : 462712 (Deleted: 431217) + Binary : 11917 (Ratio: 2.58%) + Ternary : 2665 (Ratio: 0.58%) + Conflict : 462712 (Average Length: 639.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 462712 (Average: 18.94 Max: 974 Sum: 8762533) + Executed : 462613 (Average: 18.93 Max: 974 Sum: 8758082 Ratio: 99.95%) + Bounded : 99 (Average: 44.96 Max: 107 Sum: 4451 Ratio: 0.05%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 6202901 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1017MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.41s +Memory: 927MB (+0MB) +UNKNOWN +Iteration Time: 8.47s + +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,2,False), (22,110,1,True), (23,115,1,True)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 61 +Time : 471.235s (Solving: 442.27s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 471.296s + +Choices : 9827425 (Domain: 9711160) +Conflicts : 471845 (Analyzed: 471842) +Restarts : 5662 (Average: 83.33 Last: 191) +Model-Level : 342.0 +Problems : 61 (Average Length: 77.16 Splits: 0) +Lemmas : 471842 (Deleted: 441016) + Binary : 11985 (Ratio: 2.54%) + Ternary : 2683 (Ratio: 0.57%) + Conflict : 471842 (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 : 471842 (Average: 18.74 Max: 974 Sum: 8843958) + Executed : 471743 (Average: 18.73 Max: 974 Sum: 8839507 Ratio: 99.95%) + Bounded : 99 (Average: 44.96 Max: 107 Sum: 4451 Ratio: 0.05%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 6202901 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1017MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.23s +Memory: 927MB (+0MB) +UNKNOWN +Iteration Time: 8.29s + +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,2,False), (22,110,1,True), (23,115,1,True)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 62 +Time : 480.423s (Solving: 451.29s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 480.488s + +Choices : 9968143 (Domain: 9851084) +Conflicts : 481343 (Analyzed: 481340) +Restarts : 5762 (Average: 83.54 Last: 191) +Model-Level : 342.0 +Problems : 62 (Average Length: 77.81 Splits: 0) +Lemmas : 481340 (Deleted: 449867) + Binary : 12093 (Ratio: 2.51%) + Ternary : 2691 (Ratio: 0.56%) + Conflict : 481340 (Average Length: 654.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 481340 (Average: 18.62 Max: 974 Sum: 8961896) + Executed : 481240 (Average: 18.61 Max: 974 Sum: 8957328 Ratio: 99.95%) + Bounded : 100 (Average: 45.68 Max: 117 Sum: 4568 Ratio: 0.05%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 6202901 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1017MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.14s +Memory: 927MB (+0MB) +UNKNOWN +Iteration Time: 9.20s + +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,2,False), (22,110,1,True), (23,115,1,True)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 63 +Time : 484.507s (Solving: 455.20s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 484.572s + +Choices : 10022050 (Domain: 9904910) +Conflicts : 489231 (Analyzed: 489228) +Restarts : 5862 (Average: 83.46 Last: 191) +Model-Level : 342.0 +Problems : 63 (Average Length: 78.43 Splits: 0) +Lemmas : 489228 (Deleted: 457045) + Binary : 12117 (Ratio: 2.48%) + Ternary : 2697 (Ratio: 0.55%) + Conflict : 489228 (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 : 489228 (Average: 18.40 Max: 974 Sum: 9003371) + Executed : 489126 (Average: 18.39 Max: 974 Sum: 8998569 Ratio: 99.95%) + Bounded : 102 (Average: 47.08 Max: 117 Sum: 4802 Ratio: 0.05%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 6202875 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1017MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 4.03s +Memory: 927MB (+0MB) +UNKNOWN +Iteration Time: 4.09s + +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,2,False), (22,110,1,True), (23,115,1,True)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 64 +Time : 490.489s (Solving: 460.97s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 490.556s + +Choices : 10117467 (Domain: 10000011) +Conflicts : 497810 (Analyzed: 497807) +Restarts : 5962 (Average: 83.50 Last: 191) +Model-Level : 342.0 +Problems : 64 (Average Length: 79.03 Splits: 0) +Lemmas : 497807 (Deleted: 464698) + Binary : 12152 (Ratio: 2.44%) + Ternary : 2704 (Ratio: 0.54%) + Conflict : 497807 (Average Length: 646.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 497807 (Average: 18.25 Max: 974 Sum: 9085038) + Executed : 497705 (Average: 18.24 Max: 974 Sum: 9080236 Ratio: 99.95%) + Bounded : 102 (Average: 47.08 Max: 117 Sum: 4802 Ratio: 0.05%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 6202835 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1017MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 5.90s +Memory: 927MB (+0MB) +UNKNOWN +Iteration Time: 5.99s + +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,2,False), (22,110,1,True), (23,115,1,True)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 65 +Time : 499.873s (Solving: 470.19s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 499.948s + +Choices : 10316653 (Domain: 10198666) +Conflicts : 507252 (Analyzed: 507249) +Restarts : 6062 (Average: 83.68 Last: 191) +Model-Level : 342.0 +Problems : 65 (Average Length: 79.62 Splits: 0) +Lemmas : 507249 (Deleted: 475229) + Binary : 12202 (Ratio: 2.41%) + Ternary : 2718 (Ratio: 0.54%) + Conflict : 507249 (Average Length: 656.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 507249 (Average: 18.24 Max: 974 Sum: 9253018) + Executed : 507147 (Average: 18.23 Max: 974 Sum: 9248216 Ratio: 99.95%) + Bounded : 102 (Average: 47.08 Max: 117 Sum: 4802 Ratio: 0.05%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 6202835 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1017MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.33s +Memory: 927MB (+0MB) +UNKNOWN +Iteration Time: 9.39s + +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,2,False), (22,110,1,True), (23,115,1,True)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 66 +Time : 507.098s (Solving: 477.23s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 507.176s + +Choices : 10448903 (Domain: 10330778) +Conflicts : 516103 (Analyzed: 516100) +Restarts : 6162 (Average: 83.76 Last: 191) +Model-Level : 342.0 +Problems : 66 (Average Length: 80.18 Splits: 0) +Lemmas : 516100 (Deleted: 484491) + Binary : 12236 (Ratio: 2.37%) + Ternary : 2733 (Ratio: 0.53%) + Conflict : 516100 (Average Length: 656.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 516100 (Average: 18.14 Max: 974 Sum: 9364146) + Executed : 515998 (Average: 18.13 Max: 974 Sum: 9359344 Ratio: 99.95%) + Bounded : 102 (Average: 47.08 Max: 117 Sum: 4802 Ratio: 0.05%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 6202835 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1017MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.16s +Memory: 927MB (+0MB) +UNKNOWN +Iteration Time: 7.23s + +Iteration 66 +Queue: [(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.254s (Solving: 488.22s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 518.336s + +Choices : 10844416 (Domain: 10725687) +Conflicts : 526139 (Analyzed: 526136) +Restarts : 6262 (Average: 84.02 Last: 191) +Model-Level : 342.0 +Problems : 67 (Average Length: 80.73 Splits: 0) +Lemmas : 526136 (Deleted: 493082) + Binary : 12310 (Ratio: 2.34%) + Ternary : 2745 (Ratio: 0.52%) + Conflict : 526136 (Average Length: 662.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 526136 (Average: 18.48 Max: 1025 Sum: 9723635) + Executed : 526034 (Average: 18.47 Max: 1025 Sum: 9718833 Ratio: 99.95%) + Bounded : 102 (Average: 47.08 Max: 117 Sum: 4802 Ratio: 0.05%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 6202835 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1017MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 11.10s +Memory: 927MB (+0MB) +UNKNOWN +Iteration Time: 11.16s + +Iteration 67 +Queue: [(23,115,1,True)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 68 +Time : 528.172s (Solving: 497.97s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 528.260s + +Choices : 11146452 (Domain: 11027399) +Conflicts : 535050 (Analyzed: 535047) +Restarts : 6362 (Average: 84.10 Last: 191) +Model-Level : 342.0 +Problems : 68 (Average Length: 81.26 Splits: 0) +Lemmas : 535047 (Deleted: 502856) + Binary : 12352 (Ratio: 2.31%) + Ternary : 2754 (Ratio: 0.51%) + Conflict : 535047 (Average Length: 668.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 535047 (Average: 18.67 Max: 1087 Sum: 9989851) + Executed : 534945 (Average: 18.66 Max: 1087 Sum: 9985049 Ratio: 99.95%) + Bounded : 102 (Average: 47.08 Max: 117 Sum: 4802 Ratio: 0.05%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 6202835 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1017MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.86s +Memory: 927MB (+0MB) +UNKNOWN +Iteration Time: 9.93s + +Iteration 68 +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 : 69 +Time : 531.113s (Solving: 500.73s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 531.200s + +Choices : 11178875 (Domain: 11059822) +Conflicts : 541742 (Analyzed: 541739) +Restarts : 6462 (Average: 83.83 Last: 191) +Model-Level : 342.0 +Problems : 69 (Average Length: 81.78 Splits: 0) +Lemmas : 541739 (Deleted: 509415) + Binary : 12488 (Ratio: 2.31%) + Ternary : 2762 (Ratio: 0.51%) + Conflict : 541739 (Average Length: 665.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 541739 (Average: 18.48 Max: 1087 Sum: 10011096) + Executed : 541637 (Average: 18.47 Max: 1087 Sum: 10006294 Ratio: 99.95%) + Bounded : 102 (Average: 47.08 Max: 117 Sum: 4802 Ratio: 0.05%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 6202835 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1017MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 2.88s +Memory: 927MB (+0MB) +UNKNOWN +Iteration Time: 2.95s + +Iteration 69 +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 : 70 +Time : 539.240s (Solving: 508.66s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 539.332s + +Choices : 11259273 (Domain: 11140220) +Conflicts : 550510 (Analyzed: 550507) +Restarts : 6562 (Average: 83.89 Last: 191) +Model-Level : 342.0 +Problems : 70 (Average Length: 82.29 Splits: 0) +Lemmas : 550507 (Deleted: 517896) + Binary : 12572 (Ratio: 2.28%) + Ternary : 2779 (Ratio: 0.50%) + Conflict : 550507 (Average Length: 674.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 550507 (Average: 18.30 Max: 1087 Sum: 10075254) + Executed : 550405 (Average: 18.29 Max: 1087 Sum: 10070452 Ratio: 99.95%) + Bounded : 102 (Average: 47.08 Max: 117 Sum: 4802 Ratio: 0.05%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 6202835 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1017MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.06s +Memory: 927MB (+0MB) +UNKNOWN +Iteration Time: 8.13s + +Iteration 70 +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 : 71 +Time : 546.357s (Solving: 515.59s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 546.452s + +Choices : 11338209 (Domain: 11218843) +Conflicts : 559141 (Analyzed: 559138) +Restarts : 6662 (Average: 83.93 Last: 191) +Model-Level : 342.0 +Problems : 71 (Average Length: 82.77 Splits: 0) +Lemmas : 559138 (Deleted: 526494) + Binary : 12620 (Ratio: 2.26%) + Ternary : 2789 (Ratio: 0.50%) + Conflict : 559138 (Average Length: 679.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 559138 (Average: 18.13 Max: 1087 Sum: 10135238) + Executed : 559036 (Average: 18.12 Max: 1087 Sum: 10130436 Ratio: 99.95%) + Bounded : 102 (Average: 47.08 Max: 117 Sum: 4802 Ratio: 0.05%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 6202835 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1017MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.05s +Memory: 927MB (+0MB) +UNKNOWN +Iteration Time: 7.12s + +Iteration 71 +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 : 72 +Time : 554.175s (Solving: 523.22s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 554.276s + +Choices : 11437940 (Domain: 11317938) +Conflicts : 568111 (Analyzed: 568108) +Restarts : 6762 (Average: 84.01 Last: 191) +Model-Level : 342.0 +Problems : 72 (Average Length: 83.25 Splits: 0) +Lemmas : 568108 (Deleted: 534870) + Binary : 12679 (Ratio: 2.23%) + Ternary : 2799 (Ratio: 0.49%) + Conflict : 568108 (Average Length: 686.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 568108 (Average: 17.98 Max: 1087 Sum: 10214171) + Executed : 568006 (Average: 17.97 Max: 1087 Sum: 10209369 Ratio: 99.95%) + Bounded : 102 (Average: 47.08 Max: 117 Sum: 4802 Ratio: 0.05%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 6202835 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1017MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.75s +Memory: 927MB (+0MB) +UNKNOWN +Iteration Time: 7.82s + +Iteration 72 +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 : 73 +Time : 562.734s (Solving: 531.61s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 562.840s + +Choices : 11575230 (Domain: 11454387) +Conflicts : 577113 (Analyzed: 577110) +Restarts : 6862 (Average: 84.10 Last: 191) +Model-Level : 342.0 +Problems : 73 (Average Length: 83.71 Splits: 0) +Lemmas : 577110 (Deleted: 543604) + Binary : 12747 (Ratio: 2.21%) + Ternary : 2806 (Ratio: 0.49%) + Conflict : 577110 (Average Length: 690.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 577110 (Average: 17.90 Max: 1087 Sum: 10329332) + Executed : 577008 (Average: 17.89 Max: 1087 Sum: 10324530 Ratio: 99.95%) + Bounded : 102 (Average: 47.08 Max: 117 Sum: 4802 Ratio: 0.05%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 6202835 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1017MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.51s +Memory: 927MB (+0MB) +UNKNOWN +Iteration Time: 8.57s + +Iteration 73 +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 : 74 +Time : 569.566s (Solving: 538.27s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 569.676s + +Choices : 11667719 (Domain: 11546723) +Conflicts : 584781 (Analyzed: 584778) +Restarts : 6962 (Average: 84.00 Last: 191) +Model-Level : 342.0 +Problems : 74 (Average Length: 84.16 Splits: 0) +Lemmas : 584778 (Deleted: 550296) + Binary : 12839 (Ratio: 2.20%) + Ternary : 2812 (Ratio: 0.48%) + Conflict : 584778 (Average Length: 696.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 584778 (Average: 17.78 Max: 1087 Sum: 10398817) + Executed : 584676 (Average: 17.77 Max: 1087 Sum: 10394015 Ratio: 99.95%) + Bounded : 102 (Average: 47.08 Max: 117 Sum: 4802 Ratio: 0.05%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 6202835 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1017MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.78s +Memory: 927MB (+0MB) +UNKNOWN +Iteration Time: 6.84s + +Iteration 74 +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 : 75 +Time : 578.069s (Solving: 546.60s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 578.184s + +Choices : 11829637 (Domain: 11708080) +Conflicts : 593828 (Analyzed: 593825) +Restarts : 7062 (Average: 84.09 Last: 191) +Model-Level : 342.0 +Problems : 75 (Average Length: 84.60 Splits: 0) +Lemmas : 593825 (Deleted: 559919) + Binary : 12883 (Ratio: 2.17%) + Ternary : 2818 (Ratio: 0.47%) + Conflict : 593825 (Average Length: 700.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 593825 (Average: 17.74 Max: 1087 Sum: 10535313) + Executed : 593723 (Average: 17.73 Max: 1087 Sum: 10530511 Ratio: 99.95%) + Bounded : 102 (Average: 47.08 Max: 117 Sum: 4802 Ratio: 0.05%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 6202835 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1017MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.45s +Memory: 927MB (+0MB) +UNKNOWN +Iteration Time: 8.51s + +Iteration 75 +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 : 76 +Time : 586.253s (Solving: 554.61s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 586.372s + +Choices : 11991213 (Domain: 11868864) +Conflicts : 602844 (Analyzed: 602841) +Restarts : 7162 (Average: 84.17 Last: 191) +Model-Level : 342.0 +Problems : 76 (Average Length: 85.03 Splits: 0) +Lemmas : 602841 (Deleted: 568774) + Binary : 12966 (Ratio: 2.15%) + Ternary : 2831 (Ratio: 0.47%) + Conflict : 602841 (Average Length: 704.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 602841 (Average: 17.71 Max: 1087 Sum: 10673619) + Executed : 602739 (Average: 17.70 Max: 1087 Sum: 10668817 Ratio: 99.96%) + Bounded : 102 (Average: 47.08 Max: 117 Sum: 4802 Ratio: 0.04%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 6202835 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1017MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.13s +Memory: 927MB (+0MB) +UNKNOWN +Iteration Time: 8.19s + +Iteration 76 +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 : 77 +Time : 595.689s (Solving: 563.84s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 595.812s + +Choices : 12199626 (Domain: 12077029) +Conflicts : 611830 (Analyzed: 611827) +Restarts : 7262 (Average: 84.25 Last: 191) +Model-Level : 342.0 +Problems : 77 (Average Length: 85.44 Splits: 0) +Lemmas : 611827 (Deleted: 577560) + Binary : 13008 (Ratio: 2.13%) + Ternary : 2846 (Ratio: 0.47%) + Conflict : 611827 (Average Length: 707.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 611827 (Average: 17.74 Max: 1087 Sum: 10853169) + Executed : 611725 (Average: 17.73 Max: 1087 Sum: 10848367 Ratio: 99.96%) + Bounded : 102 (Average: 47.08 Max: 117 Sum: 4802 Ratio: 0.04%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 6202835 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1017MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.36s +Memory: 927MB (+0MB) +UNKNOWN +Iteration Time: 9.44s + +Iteration 77 +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 : 78 +Time : 603.253s (Solving: 571.22s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 603.376s + +Choices : 12375860 (Domain: 12252959) +Conflicts : 620065 (Analyzed: 620062) +Restarts : 7362 (Average: 84.22 Last: 191) +Model-Level : 342.0 +Problems : 78 (Average Length: 85.85 Splits: 0) +Lemmas : 620062 (Deleted: 584170) + Binary : 13054 (Ratio: 2.11%) + Ternary : 2852 (Ratio: 0.46%) + Conflict : 620062 (Average Length: 709.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 620062 (Average: 17.75 Max: 1087 Sum: 11004851) + Executed : 619960 (Average: 17.74 Max: 1087 Sum: 11000049 Ratio: 99.96%) + Bounded : 102 (Average: 47.08 Max: 117 Sum: 4802 Ratio: 0.04%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 6202835 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1017MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.50s +Memory: 927MB (+0MB) +UNKNOWN +Iteration Time: 7.57s + +Iteration 78 +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 : 79 +Time : 607.253s (Solving: 575.03s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 607.376s + +Choices : 12422308 (Domain: 12299407) +Conflicts : 627957 (Analyzed: 627954) +Restarts : 7462 (Average: 84.15 Last: 191) +Model-Level : 342.0 +Problems : 79 (Average Length: 86.24 Splits: 0) +Lemmas : 627954 (Deleted: 592408) + Binary : 13087 (Ratio: 2.08%) + Ternary : 2875 (Ratio: 0.46%) + Conflict : 627954 (Average Length: 705.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 627954 (Average: 17.59 Max: 1087 Sum: 11045651) + Executed : 627852 (Average: 17.58 Max: 1087 Sum: 11040849 Ratio: 99.96%) + Bounded : 102 (Average: 47.08 Max: 117 Sum: 4802 Ratio: 0.04%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 6202835 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1017MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 3.93s +Memory: 927MB (+0MB) +UNKNOWN +Iteration Time: 4.00s + +Iteration 79 +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 : 80 +Time : 612.597s (Solving: 580.21s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 612.724s + +Choices : 12464597 (Domain: 12341696) +Conflicts : 635434 (Analyzed: 635431) +Restarts : 7562 (Average: 84.03 Last: 191) +Model-Level : 342.0 +Problems : 80 (Average Length: 86.62 Splits: 0) +Lemmas : 635431 (Deleted: 599898) + Binary : 13106 (Ratio: 2.06%) + Ternary : 2881 (Ratio: 0.45%) + Conflict : 635431 (Average Length: 704.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 635431 (Average: 17.43 Max: 1087 Sum: 11077275) + Executed : 635328 (Average: 17.42 Max: 1087 Sum: 11072356 Ratio: 99.96%) + Bounded : 103 (Average: 47.76 Max: 117 Sum: 4919 Ratio: 0.04%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 6202835 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1017MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 5.29s +Memory: 927MB (+0MB) +UNKNOWN +Iteration Time: 5.35s + +Iteration 80 +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 : 81 +Time : 620.046s (Solving: 587.47s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 620.176s + +Choices : 12543123 (Domain: 12419913) +Conflicts : 644383 (Analyzed: 644380) +Restarts : 7662 (Average: 84.10 Last: 191) +Model-Level : 342.0 +Problems : 81 (Average Length: 87.00 Splits: 0) +Lemmas : 644380 (Deleted: 609427) + Binary : 13130 (Ratio: 2.04%) + Ternary : 2886 (Ratio: 0.45%) + Conflict : 644380 (Average Length: 704.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 644380 (Average: 17.29 Max: 1087 Sum: 11139349) + Executed : 644277 (Average: 17.28 Max: 1087 Sum: 11134430 Ratio: 99.96%) + Bounded : 103 (Average: 47.76 Max: 117 Sum: 4919 Ratio: 0.04%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 6202822 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1017MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.38s +Memory: 927MB (+0MB) +UNKNOWN +Iteration Time: 7.46s + +Iteration 81 +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 : 82 +Time : 628.121s (Solving: 595.33s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 628.252s + +Choices : 12656454 (Domain: 12532395) +Conflicts : 653270 (Analyzed: 653267) +Restarts : 7762 (Average: 84.16 Last: 191) +Model-Level : 342.0 +Problems : 82 (Average Length: 87.37 Splits: 0) +Lemmas : 653267 (Deleted: 618139) + Binary : 13214 (Ratio: 2.02%) + Ternary : 2888 (Ratio: 0.44%) + Conflict : 653267 (Average Length: 707.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 653267 (Average: 17.19 Max: 1087 Sum: 11232751) + Executed : 653164 (Average: 17.19 Max: 1087 Sum: 11227832 Ratio: 99.96%) + Bounded : 103 (Average: 47.76 Max: 117 Sum: 4919 Ratio: 0.04%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 6202822 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1017MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.00s +Memory: 927MB (+0MB) +UNKNOWN +Iteration Time: 8.08s + +Iteration 82 +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 : 83 +Time : 635.601s (Solving: 602.64s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 635.736s + +Choices : 12769605 (Domain: 12645041) +Conflicts : 661801 (Analyzed: 661798) +Restarts : 7862 (Average: 84.18 Last: 191) +Model-Level : 342.0 +Problems : 83 (Average Length: 87.72 Splits: 0) +Lemmas : 661798 (Deleted: 624669) + Binary : 13264 (Ratio: 2.00%) + Ternary : 2901 (Ratio: 0.44%) + Conflict : 661798 (Average Length: 708.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 661798 (Average: 17.12 Max: 1087 Sum: 11326856) + Executed : 661695 (Average: 17.11 Max: 1087 Sum: 11321937 Ratio: 99.96%) + Bounded : 103 (Average: 47.76 Max: 117 Sum: 4919 Ratio: 0.04%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 6202822 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1017MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.42s +Memory: 927MB (+0MB) +UNKNOWN +Iteration Time: 7.49s + +Iteration 83 +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 : 84 +Time : 644.372s (Solving: 611.25s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 644.508s + +Choices : 12952727 (Domain: 12827391) +Conflicts : 670878 (Analyzed: 670875) +Restarts : 7962 (Average: 84.26 Last: 191) +Model-Level : 342.0 +Problems : 84 (Average Length: 88.07 Splits: 0) +Lemmas : 670875 (Deleted: 635122) + Binary : 13333 (Ratio: 1.99%) + Ternary : 2904 (Ratio: 0.43%) + Conflict : 670875 (Average Length: 711.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 670875 (Average: 17.12 Max: 1087 Sum: 11486751) + Executed : 670771 (Average: 17.11 Max: 1087 Sum: 11481715 Ratio: 99.96%) + Bounded : 104 (Average: 48.42 Max: 117 Sum: 5036 Ratio: 0.04%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 6202822 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1017MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.72s +Memory: 927MB (+0MB) +UNKNOWN +Iteration Time: 8.78s + +Iteration 84 +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 : 85 +Time : 653.225s (Solving: 619.90s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 653.368s + +Choices : 13154440 (Domain: 13028645) +Conflicts : 679321 (Analyzed: 679318) +Restarts : 8062 (Average: 84.26 Last: 191) +Model-Level : 342.0 +Problems : 85 (Average Length: 88.41 Splits: 0) +Lemmas : 679318 (Deleted: 641856) + Binary : 13389 (Ratio: 1.97%) + Ternary : 2910 (Ratio: 0.43%) + Conflict : 679318 (Average Length: 714.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 679318 (Average: 17.17 Max: 1087 Sum: 11662155) + Executed : 679214 (Average: 17.16 Max: 1087 Sum: 11657119 Ratio: 99.96%) + Bounded : 104 (Average: 48.42 Max: 117 Sum: 5036 Ratio: 0.04%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 6202808 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1017MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.78s +Memory: 927MB (+0MB) +UNKNOWN +Iteration Time: 8.86s + +Iteration 85 +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 : 86 +Time : 665.815s (Solving: 632.32s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 665.964s + +Choices : 13637984 (Domain: 13509961) +Conflicts : 688706 (Analyzed: 688703) +Restarts : 8162 (Average: 84.38 Last: 191) +Model-Level : 342.0 +Problems : 86 (Average Length: 88.74 Splits: 0) +Lemmas : 688703 (Deleted: 652153) + Binary : 13529 (Ratio: 1.96%) + Ternary : 2919 (Ratio: 0.42%) + Conflict : 688703 (Average Length: 723.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 688703 (Average: 17.58 Max: 1087 Sum: 12108741) + Executed : 688599 (Average: 17.57 Max: 1087 Sum: 12103705 Ratio: 99.96%) + Bounded : 104 (Average: 48.42 Max: 117 Sum: 5036 Ratio: 0.04%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 6202808 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1017MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 12.53s +Memory: 927MB (+0MB) +UNKNOWN +Iteration Time: 12.60s + +Iteration 86 +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 : 87 +Time : 671.160s (Solving: 637.48s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 671.312s + +Choices : 13688194 (Domain: 13560171) +Conflicts : 697133 (Analyzed: 697130) +Restarts : 8262 (Average: 84.38 Last: 191) +Model-Level : 342.0 +Problems : 87 (Average Length: 89.07 Splits: 0) +Lemmas : 697130 (Deleted: 659644) + Binary : 13556 (Ratio: 1.94%) + Ternary : 2927 (Ratio: 0.42%) + Conflict : 697130 (Average Length: 727.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 697130 (Average: 17.43 Max: 1087 Sum: 12152402) + Executed : 697025 (Average: 17.42 Max: 1087 Sum: 12147249 Ratio: 99.96%) + Bounded : 105 (Average: 49.08 Max: 117 Sum: 5153 Ratio: 0.04%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 6202808 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1017MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 5.28s +Memory: 927MB (+0MB) +UNKNOWN +Iteration Time: 5.35s + +Iteration 87 +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 : 88 +Time : 677.219s (Solving: 643.36s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 677.376s + +Choices : 13740634 (Domain: 13612611) +Conflicts : 704596 (Analyzed: 704593) +Restarts : 8362 (Average: 84.26 Last: 191) +Model-Level : 342.0 +Problems : 88 (Average Length: 89.39 Splits: 0) +Lemmas : 704593 (Deleted: 667326) + Binary : 13584 (Ratio: 1.93%) + Ternary : 2929 (Ratio: 0.42%) + Conflict : 704593 (Average Length: 727.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 704593 (Average: 17.31 Max: 1087 Sum: 12193423) + Executed : 704486 (Average: 17.30 Max: 1087 Sum: 12188036 Ratio: 99.96%) + Bounded : 107 (Average: 50.35 Max: 117 Sum: 5387 Ratio: 0.04%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 6202794 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1017MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.00s +Memory: 927MB (+0MB) +UNKNOWN +Iteration Time: 6.06s + +Iteration 88 +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 : 89 +Time : 684.593s (Solving: 650.55s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 684.752s + +Choices : 13825244 (Domain: 13696729) +Conflicts : 712990 (Analyzed: 712987) +Restarts : 8462 (Average: 84.26 Last: 191) +Model-Level : 342.0 +Problems : 89 (Average Length: 89.70 Splits: 0) +Lemmas : 712987 (Deleted: 674637) + Binary : 13621 (Ratio: 1.91%) + Ternary : 2931 (Ratio: 0.41%) + Conflict : 712987 (Average Length: 730.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 712987 (Average: 17.19 Max: 1087 Sum: 12259017) + Executed : 712880 (Average: 17.19 Max: 1087 Sum: 12253630 Ratio: 99.96%) + Bounded : 107 (Average: 50.35 Max: 117 Sum: 5387 Ratio: 0.04%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 6202762 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1017MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.31s +Memory: 927MB (+0MB) +UNKNOWN +Iteration Time: 7.38s + +Iteration 89 +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 : 90 +Time : 693.094s (Solving: 658.86s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 693.260s + +Choices : 13939272 (Domain: 13810461) +Conflicts : 721848 (Analyzed: 721845) +Restarts : 8562 (Average: 84.31 Last: 191) +Model-Level : 342.0 +Problems : 90 (Average Length: 90.00 Splits: 0) +Lemmas : 721845 (Deleted: 685026) + Binary : 13655 (Ratio: 1.89%) + Ternary : 2937 (Ratio: 0.41%) + Conflict : 721845 (Average Length: 736.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 721845 (Average: 17.11 Max: 1087 Sum: 12351644) + Executed : 721738 (Average: 17.10 Max: 1087 Sum: 12346257 Ratio: 99.96%) + Bounded : 107 (Average: 50.35 Max: 117 Sum: 5387 Ratio: 0.04%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 6202762 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1017MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.43s +Memory: 927MB (+0MB) +UNKNOWN +Iteration Time: 8.51s + +Iteration 90 +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 : 91 +Time : 699.725s (Solving: 665.32s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 699.896s + +Choices : 14060197 (Domain: 13931002) +Conflicts : 730270 (Analyzed: 730267) +Restarts : 8662 (Average: 84.31 Last: 191) +Model-Level : 342.0 +Problems : 91 (Average Length: 90.30 Splits: 0) +Lemmas : 730267 (Deleted: 691537) + Binary : 13700 (Ratio: 1.88%) + Ternary : 2942 (Ratio: 0.40%) + Conflict : 730267 (Average Length: 735.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 730267 (Average: 17.05 Max: 1087 Sum: 12454529) + Executed : 730160 (Average: 17.05 Max: 1087 Sum: 12449142 Ratio: 99.96%) + Bounded : 107 (Average: 50.35 Max: 117 Sum: 5387 Ratio: 0.04%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 6202762 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1017MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.58s +Memory: 927MB (+0MB) +UNKNOWN +Iteration Time: 6.64s + +Iteration 91 +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 : 92 +Time : 709.691s (Solving: 675.09s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 709.868s + +Choices : 14295011 (Domain: 14165044) +Conflicts : 739079 (Analyzed: 739076) +Restarts : 8762 (Average: 84.35 Last: 191) +Model-Level : 342.0 +Problems : 92 (Average Length: 90.59 Splits: 0) +Lemmas : 739076 (Deleted: 701865) + Binary : 13761 (Ratio: 1.86%) + Ternary : 2952 (Ratio: 0.40%) + Conflict : 739076 (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 : 739076 (Average: 17.13 Max: 1087 Sum: 12661007) + Executed : 738969 (Average: 17.12 Max: 1087 Sum: 12655620 Ratio: 99.96%) + Bounded : 107 (Average: 50.35 Max: 117 Sum: 5387 Ratio: 0.04%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 6202762 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1017MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.90s +Memory: 927MB (+0MB) +UNKNOWN +Iteration Time: 9.97s + +Iteration 92 +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 : 93 +Time : 720.379s (Solving: 685.61s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 720.560s + +Choices : 14582109 (Domain: 14451573) +Conflicts : 747597 (Analyzed: 747594) +Restarts : 8862 (Average: 84.36 Last: 191) +Model-Level : 342.0 +Problems : 93 (Average Length: 90.87 Splits: 0) +Lemmas : 747594 (Deleted: 708273) + Binary : 13862 (Ratio: 1.85%) + Ternary : 2963 (Ratio: 0.40%) + Conflict : 747594 (Average Length: 748.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 747594 (Average: 17.28 Max: 1087 Sum: 12918521) + Executed : 747487 (Average: 17.27 Max: 1087 Sum: 12913134 Ratio: 99.96%) + Bounded : 107 (Average: 50.35 Max: 117 Sum: 5387 Ratio: 0.04%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 6202762 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1017MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 10.64s +Memory: 927MB (+0MB) +UNKNOWN +Iteration Time: 10.70s + +Iteration 93 +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 : 94 +Time : 725.893s (Solving: 690.96s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 726.076s + +Choices : 14642642 (Domain: 14512106) +Conflicts : 755198 (Analyzed: 755195) +Restarts : 8962 (Average: 84.27 Last: 191) +Model-Level : 342.0 +Problems : 94 (Average Length: 91.15 Splits: 0) +Lemmas : 755195 (Deleted: 716614) + Binary : 13869 (Ratio: 1.84%) + Ternary : 2967 (Ratio: 0.39%) + Conflict : 755195 (Average Length: 745.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 755195 (Average: 17.16 Max: 1087 Sum: 12960887) + Executed : 755087 (Average: 17.16 Max: 1087 Sum: 12955383 Ratio: 99.96%) + Bounded : 108 (Average: 50.96 Max: 117 Sum: 5504 Ratio: 0.04%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 6202762 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1017MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 5.46s +Memory: 927MB (+0MB) +UNKNOWN +Iteration Time: 5.52s + +Iteration 94 +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 : 95 +Time : 729.350s (Solving: 694.21s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 729.532s + +Choices : 14681961 (Domain: 14551425) +Conflicts : 762405 (Analyzed: 762402) +Restarts : 9062 (Average: 84.13 Last: 191) +Model-Level : 342.0 +Problems : 95 (Average Length: 91.42 Splits: 0) +Lemmas : 762402 (Deleted: 724079) + Binary : 13882 (Ratio: 1.82%) + Ternary : 2967 (Ratio: 0.39%) + Conflict : 762402 (Average Length: 742.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 762402 (Average: 17.04 Max: 1087 Sum: 12992723) + Executed : 762293 (Average: 17.03 Max: 1087 Sum: 12987102 Ratio: 99.96%) + Bounded : 109 (Average: 51.57 Max: 117 Sum: 5621 Ratio: 0.04%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 6202748 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1017MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 3.38s +Memory: 927MB (+0MB) +UNKNOWN +Iteration Time: 3.46s + +Iteration 95 +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 : 96 +Time : 738.241s (Solving: 702.92s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 738.424s + +Choices : 14752457 (Domain: 14621921) +Conflicts : 770831 (Analyzed: 770828) +Restarts : 9162 (Average: 84.13 Last: 191) +Model-Level : 342.0 +Problems : 96 (Average Length: 91.69 Splits: 0) +Lemmas : 770828 (Deleted: 731141) + Binary : 13968 (Ratio: 1.81%) + Ternary : 2980 (Ratio: 0.39%) + Conflict : 770828 (Average Length: 744.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 770828 (Average: 16.93 Max: 1087 Sum: 13050715) + Executed : 770719 (Average: 16.92 Max: 1087 Sum: 13045094 Ratio: 99.96%) + Bounded : 109 (Average: 51.57 Max: 117 Sum: 5621 Ratio: 0.04%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 6202734 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1017MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.83s +Memory: 927MB (+0MB) +UNKNOWN +Iteration Time: 8.90s + +Iteration 96 +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 : 97 +Time : 743.794s (Solving: 708.28s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 743.980s + +Choices : 14808089 (Domain: 14677329) +Conflicts : 778773 (Analyzed: 778770) +Restarts : 9262 (Average: 84.08 Last: 191) +Model-Level : 342.0 +Problems : 97 (Average Length: 91.95 Splits: 0) +Lemmas : 778770 (Deleted: 739298) + Binary : 13995 (Ratio: 1.80%) + Ternary : 2985 (Ratio: 0.38%) + Conflict : 778770 (Average Length: 743.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 778770 (Average: 16.81 Max: 1087 Sum: 13093204) + Executed : 778661 (Average: 16.81 Max: 1087 Sum: 13087583 Ratio: 99.96%) + Bounded : 109 (Average: 51.57 Max: 117 Sum: 5621 Ratio: 0.04%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 6202734 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1017MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 5.48s +Memory: 927MB (+0MB) +UNKNOWN +Iteration Time: 5.56s + +Iteration 97 +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 : 98 +Time : 751.870s (Solving: 716.15s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 752.060s + +Choices : 14910880 (Domain: 14779638) +Conflicts : 787235 (Analyzed: 787232) +Restarts : 9362 (Average: 84.09 Last: 191) +Model-Level : 342.0 +Problems : 98 (Average Length: 92.20 Splits: 0) +Lemmas : 787232 (Deleted: 747083) + Binary : 14046 (Ratio: 1.78%) + Ternary : 2989 (Ratio: 0.38%) + Conflict : 787232 (Average Length: 747.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 787232 (Average: 16.74 Max: 1087 Sum: 13176273) + Executed : 787123 (Average: 16.73 Max: 1087 Sum: 13170652 Ratio: 99.96%) + Bounded : 109 (Average: 51.57 Max: 117 Sum: 5621 Ratio: 0.04%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 6202734 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1017MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.00s +Memory: 927MB (+0MB) +UNKNOWN +Iteration Time: 8.08s + +Iteration 98 +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 : 99 +Time : 760.005s (Solving: 724.09s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 760.200s + +Choices : 15010433 (Domain: 14878909) +Conflicts : 795995 (Analyzed: 795992) +Restarts : 9462 (Average: 84.13 Last: 191) +Model-Level : 342.0 +Problems : 99 (Average Length: 92.45 Splits: 0) +Lemmas : 795992 (Deleted: 757517) + Binary : 14089 (Ratio: 1.77%) + Ternary : 2995 (Ratio: 0.38%) + Conflict : 795992 (Average Length: 748.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 795992 (Average: 16.66 Max: 1087 Sum: 13257552) + Executed : 795883 (Average: 16.65 Max: 1087 Sum: 13251931 Ratio: 99.96%) + Bounded : 109 (Average: 51.57 Max: 117 Sum: 5621 Ratio: 0.04%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 6202734 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1017MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.06s +Memory: 927MB (+0MB) +UNKNOWN +Iteration Time: 8.14s + +Iteration 99 +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 : 100 +Time : 767.385s (Solving: 731.29s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 767.584s + +Choices : 15158233 (Domain: 15026269) +Conflicts : 804469 (Analyzed: 804466) +Restarts : 9562 (Average: 84.13 Last: 191) +Model-Level : 342.0 +Problems : 100 (Average Length: 92.70 Splits: 0) +Lemmas : 804466 (Deleted: 763921) + Binary : 14154 (Ratio: 1.76%) + Ternary : 2997 (Ratio: 0.37%) + Conflict : 804466 (Average Length: 749.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 804466 (Average: 16.64 Max: 1087 Sum: 13386188) + Executed : 804357 (Average: 16.63 Max: 1087 Sum: 13380567 Ratio: 99.96%) + Bounded : 109 (Average: 51.57 Max: 117 Sum: 5621 Ratio: 0.04%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 6202734 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1017MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.32s +Memory: 927MB (+0MB) +UNKNOWN +Iteration Time: 7.39s + +Iteration 100 +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 : 101 +Time : 776.003s (Solving: 739.72s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 776.204s + +Choices : 15373149 (Domain: 15240531) +Conflicts : 812742 (Analyzed: 812739) +Restarts : 9662 (Average: 84.12 Last: 191) +Model-Level : 342.0 +Problems : 101 (Average Length: 92.94 Splits: 0) +Lemmas : 812739 (Deleted: 772209) + Binary : 14221 (Ratio: 1.75%) + Ternary : 3012 (Ratio: 0.37%) + Conflict : 812739 (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 : 812739 (Average: 16.70 Max: 1087 Sum: 13575764) + Executed : 812630 (Average: 16.70 Max: 1087 Sum: 13570143 Ratio: 99.96%) + Bounded : 109 (Average: 51.57 Max: 117 Sum: 5621 Ratio: 0.04%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 6202734 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1017MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.55s +Memory: 927MB (+0MB) +UNKNOWN +Iteration Time: 8.63s + +Iteration 101 +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 : 102 +Time : 786.228s (Solving: 749.74s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 786.436s + +Choices : 15581642 (Domain: 15448845) +Conflicts : 821328 (Analyzed: 821325) +Restarts : 9762 (Average: 84.13 Last: 191) +Model-Level : 342.0 +Problems : 102 (Average Length: 93.18 Splits: 0) +Lemmas : 821325 (Deleted: 780434) + Binary : 14308 (Ratio: 1.74%) + Ternary : 3017 (Ratio: 0.37%) + Conflict : 821325 (Average Length: 759.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 821325 (Average: 16.74 Max: 1087 Sum: 13753052) + Executed : 821216 (Average: 16.74 Max: 1087 Sum: 13747431 Ratio: 99.96%) + Bounded : 109 (Average: 51.57 Max: 117 Sum: 5621 Ratio: 0.04%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 6202734 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1017MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 10.14s +Memory: 927MB (+0MB) +UNKNOWN +Iteration Time: 10.23s + +Iteration 102 +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 : 103 +Time : 794.227s (Solving: 757.57s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 794.440s + +Choices : 15657492 (Domain: 15524640) +Conflicts : 829081 (Analyzed: 829078) +Restarts : 9862 (Average: 84.07 Last: 191) +Model-Level : 342.0 +Problems : 103 (Average Length: 93.41 Splits: 0) +Lemmas : 829078 (Deleted: 788700) + Binary : 14372 (Ratio: 1.73%) + Ternary : 3020 (Ratio: 0.36%) + Conflict : 829078 (Average Length: 762.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 829078 (Average: 16.64 Max: 1087 Sum: 13798584) + Executed : 828969 (Average: 16.64 Max: 1087 Sum: 13792963 Ratio: 99.96%) + Bounded : 109 (Average: 51.57 Max: 117 Sum: 5621 Ratio: 0.04%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 6202734 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1017MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.94s +Memory: 927MB (+0MB) +UNKNOWN +Iteration Time: 8.01s + +Iteration 103 +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 : 104 +Time : 804.422s (Solving: 767.60s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 804.640s + +Choices : 15928881 (Domain: 15795707) +Conflicts : 838027 (Analyzed: 838024) +Restarts : 9962 (Average: 84.12 Last: 191) +Model-Level : 342.0 +Problems : 104 (Average Length: 93.63 Splits: 0) +Lemmas : 838024 (Deleted: 798488) + Binary : 14435 (Ratio: 1.72%) + Ternary : 3029 (Ratio: 0.36%) + Conflict : 838024 (Average Length: 762.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 838024 (Average: 16.75 Max: 1087 Sum: 14038097) + Executed : 837915 (Average: 16.74 Max: 1087 Sum: 14032476 Ratio: 99.96%) + Bounded : 109 (Average: 51.57 Max: 117 Sum: 5621 Ratio: 0.04%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 6202734 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1017MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 10.14s +Memory: 927MB (+0MB) +UNKNOWN +Iteration Time: 10.20s + +Iteration 104 +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 : 105 +Time : 808.845s (Solving: 771.85s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 809.064s + +Choices : 15985205 (Domain: 15852031) +Conflicts : 846314 (Analyzed: 846311) +Restarts : 10062 (Average: 84.11 Last: 191) +Model-Level : 342.0 +Problems : 105 (Average Length: 93.86 Splits: 0) +Lemmas : 846311 (Deleted: 804931) + Binary : 14448 (Ratio: 1.71%) + Ternary : 3034 (Ratio: 0.36%) + Conflict : 846311 (Average Length: 760.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 846311 (Average: 16.65 Max: 1087 Sum: 14087764) + Executed : 846202 (Average: 16.64 Max: 1087 Sum: 14082143 Ratio: 99.96%) + Bounded : 109 (Average: 51.57 Max: 117 Sum: 5621 Ratio: 0.04%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 6202734 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1017MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 4.37s +Memory: 927MB (+0MB) +UNKNOWN +Iteration Time: 4.43s + +Iteration 105 +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 : 106 +Time : 813.477s (Solving: 776.32s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 813.696s + +Choices : 16024283 (Domain: 15891109) +Conflicts : 854062 (Analyzed: 854059) +Restarts : 10162 (Average: 84.04 Last: 191) +Model-Level : 342.0 +Problems : 106 (Average Length: 94.08 Splits: 0) +Lemmas : 854059 (Deleted: 813030) + Binary : 14506 (Ratio: 1.70%) + Ternary : 3034 (Ratio: 0.36%) + Conflict : 854059 (Average Length: 756.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 854059 (Average: 16.53 Max: 1087 Sum: 14116699) + Executed : 853950 (Average: 16.52 Max: 1087 Sum: 14111078 Ratio: 99.96%) + Bounded : 109 (Average: 51.57 Max: 117 Sum: 5621 Ratio: 0.04%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 6202734 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1017MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 4.58s +Memory: 927MB (+0MB) +UNKNOWN +Iteration Time: 4.64s + +Iteration 106 +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 : 107 +Time : 820.358s (Solving: 783.03s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 820.580s + +Choices : 16095555 (Domain: 15962134) +Conflicts : 862371 (Analyzed: 862368) +Restarts : 10262 (Average: 84.04 Last: 191) +Model-Level : 342.0 +Problems : 107 (Average Length: 94.29 Splits: 0) +Lemmas : 862368 (Deleted: 820666) + Binary : 14527 (Ratio: 1.68%) + Ternary : 3039 (Ratio: 0.35%) + Conflict : 862368 (Average Length: 756.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 862368 (Average: 16.44 Max: 1087 Sum: 14173373) + Executed : 862259 (Average: 16.43 Max: 1087 Sum: 14167752 Ratio: 99.96%) + Bounded : 109 (Average: 51.57 Max: 117 Sum: 5621 Ratio: 0.04%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 6202734 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1017MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.83s +Memory: 927MB (+0MB) +UNKNOWN +Iteration Time: 6.89s + +Iteration 107 +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 : 108 +Time : 823.654s (Solving: 786.15s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 823.876s + +Choices : 16145727 (Domain: 16012248) +Conflicts : 869681 (Analyzed: 869678) +Restarts : 10362 (Average: 83.93 Last: 191) +Model-Level : 342.0 +Problems : 108 (Average Length: 94.50 Splits: 0) +Lemmas : 869678 (Deleted: 828827) + Binary : 14539 (Ratio: 1.67%) + Ternary : 3039 (Ratio: 0.35%) + Conflict : 869678 (Average Length: 752.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 869678 (Average: 16.34 Max: 1087 Sum: 14211614) + Executed : 869569 (Average: 16.33 Max: 1087 Sum: 14205993 Ratio: 99.96%) + Bounded : 109 (Average: 51.57 Max: 117 Sum: 5621 Ratio: 0.04%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 6202734 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1017MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 3.24s +Memory: 927MB (+0MB) +UNKNOWN +Iteration Time: 3.30s + +Iteration 108 +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 : 109 +Time : 833.001s (Solving: 795.31s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 833.228s + +Choices : 16293709 (Domain: 16159887) +Conflicts : 878836 (Analyzed: 878833) +Restarts : 10462 (Average: 84.00 Last: 191) +Model-Level : 342.0 +Problems : 109 (Average Length: 94.71 Splits: 0) +Lemmas : 878833 (Deleted: 838196) + Binary : 14586 (Ratio: 1.66%) + Ternary : 3041 (Ratio: 0.35%) + Conflict : 878833 (Average Length: 757.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 878833 (Average: 16.31 Max: 1087 Sum: 14335805) + Executed : 878724 (Average: 16.31 Max: 1087 Sum: 14330184 Ratio: 99.96%) + Bounded : 109 (Average: 51.57 Max: 117 Sum: 5621 Ratio: 0.04%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 6202734 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1017MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.28s +Memory: 927MB (+0MB) +UNKNOWN +Iteration Time: 9.35s + +Iteration 109 +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 : 110 +Time : 844.649s (Solving: 806.76s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 844.880s + +Choices : 16660601 (Domain: 16520422) +Conflicts : 888528 (Analyzed: 888525) +Restarts : 10562 (Average: 84.12 Last: 191) +Model-Level : 342.0 +Problems : 110 (Average Length: 94.91 Splits: 0) +Lemmas : 888525 (Deleted: 846385) + Binary : 15448 (Ratio: 1.74%) + Ternary : 3284 (Ratio: 0.37%) + Conflict : 888525 (Average Length: 760.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 888525 (Average: 16.51 Max: 1087 Sum: 14666917) + Executed : 888416 (Average: 16.50 Max: 1087 Sum: 14661296 Ratio: 99.96%) + Bounded : 109 (Average: 51.57 Max: 117 Sum: 5621 Ratio: 0.04%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 6202734 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1017MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 11.58s +Memory: 927MB (+0MB) +UNKNOWN +Iteration Time: 11.66s + +Iteration 110 +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 : 111 +Time : 854.438s (Solving: 816.38s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 854.672s + +Choices : 16847541 (Domain: 16706803) +Conflicts : 896819 (Analyzed: 896816) +Restarts : 10662 (Average: 84.11 Last: 191) +Model-Level : 342.0 +Problems : 111 (Average Length: 95.11 Splits: 0) +Lemmas : 896816 (Deleted: 853057) + Binary : 15616 (Ratio: 1.74%) + Ternary : 3300 (Ratio: 0.37%) + Conflict : 896816 (Average Length: 765.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 896816 (Average: 16.53 Max: 1087 Sum: 14824806) + Executed : 896707 (Average: 16.52 Max: 1087 Sum: 14819185 Ratio: 99.96%) + Bounded : 109 (Average: 51.57 Max: 117 Sum: 5621 Ratio: 0.04%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 6202734 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1017MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.74s +Memory: 927MB (+0MB) +UNKNOWN +Iteration Time: 9.80s + +Iteration 111 +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 : 112 +Time : 866.713s (Solving: 828.47s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 866.936s + +Choices : 17271254 (Domain: 17129114) +Conflicts : 905968 (Analyzed: 905965) +Restarts : 10762 (Average: 84.18 Last: 191) +Model-Level : 342.0 +Problems : 112 (Average Length: 95.30 Splits: 0) +Lemmas : 905965 (Deleted: 863141) + Binary : 15977 (Ratio: 1.76%) + Ternary : 3410 (Ratio: 0.38%) + Conflict : 905965 (Average Length: 767.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 905965 (Average: 16.79 Max: 1087 Sum: 15213891) + Executed : 905856 (Average: 16.79 Max: 1087 Sum: 15208270 Ratio: 99.96%) + Bounded : 109 (Average: 51.57 Max: 117 Sum: 5621 Ratio: 0.04%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 6202734 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1017MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 12.19s +Memory: 927MB (+0MB) +UNKNOWN +Iteration Time: 12.27s + +Iteration 112 +Queue: [(22,110,2,True), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 113 +Time : 876.838s (Solving: 838.41s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 877.064s + +Choices : 17551183 (Domain: 17408690) +Conflicts : 914678 (Analyzed: 914675) +Restarts : 10862 (Average: 84.21 Last: 191) +Model-Level : 342.0 +Problems : 113 (Average Length: 95.50 Splits: 0) +Lemmas : 914675 (Deleted: 871025) + Binary : 16221 (Ratio: 1.77%) + Ternary : 3530 (Ratio: 0.39%) + Conflict : 914675 (Average Length: 767.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 914675 (Average: 16.91 Max: 1087 Sum: 15463933) + Executed : 914566 (Average: 16.90 Max: 1087 Sum: 15458312 Ratio: 99.96%) + Bounded : 109 (Average: 51.57 Max: 117 Sum: 5621 Ratio: 0.04%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 6202734 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1017MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 10.06s +Memory: 927MB (+0MB) +UNKNOWN +Iteration Time: 10.13s + +Iteration 113 +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 : 114 +Time : 880.362s (Solving: 841.75s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 880.588s + +Choices : 17596154 (Domain: 17453661) +Conflicts : 921935 (Analyzed: 921932) +Restarts : 10962 (Average: 84.10 Last: 191) +Model-Level : 342.0 +Problems : 114 (Average Length: 95.68 Splits: 0) +Lemmas : 921932 (Deleted: 877294) + Binary : 16229 (Ratio: 1.76%) + Ternary : 3538 (Ratio: 0.38%) + Conflict : 921932 (Average Length: 764.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 921932 (Average: 16.81 Max: 1087 Sum: 15502134) + Executed : 921823 (Average: 16.81 Max: 1087 Sum: 15496513 Ratio: 99.96%) + Bounded : 109 (Average: 51.57 Max: 117 Sum: 5621 Ratio: 0.04%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 6202734 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1017MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 3.46s +Memory: 927MB (+0MB) +UNKNOWN +Iteration Time: 3.53s + +Iteration 114 +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 : 115 +Time : 886.832s (Solving: 848.05s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 887.060s + +Choices : 17653132 (Domain: 17510639) +Conflicts : 929828 (Analyzed: 929825) +Restarts : 11062 (Average: 84.06 Last: 191) +Model-Level : 342.0 +Problems : 115 (Average Length: 95.87 Splits: 0) +Lemmas : 929825 (Deleted: 884567) + Binary : 16256 (Ratio: 1.75%) + Ternary : 3540 (Ratio: 0.38%) + Conflict : 929825 (Average Length: 762.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 929825 (Average: 16.72 Max: 1087 Sum: 15549143) + Executed : 929716 (Average: 16.72 Max: 1087 Sum: 15543522 Ratio: 99.96%) + Bounded : 109 (Average: 51.57 Max: 117 Sum: 5621 Ratio: 0.04%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 6202734 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1017MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.41s +Memory: 927MB (+0MB) +UNKNOWN +Iteration Time: 6.48s + +Iteration 115 +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... +*** Info : (planner): INTERRUPTED by signal! +UNKNOWN + +INTERRUPTED : 1 + +Models : 0+ +Calls : 116 +Time : 892.862s (Solving: 853.91s 1st Model: 0.03s Unsat: 2.41s) +CPU Time : 893.072s + +Choices : 17710333 (Domain: 17567833) +Conflicts : 935517 (Analyzed: 935514) +Restarts : 11124 (Average: 84.10 Last: 191) +Model-Level : 342.0 +Problems : 116 (Average Length: 96.05 Splits: 0) +Lemmas : 935514 (Deleted: 890006) + Binary : 16292 (Ratio: 1.74%) + Ternary : 3553 (Ratio: 0.38%) + Conflict : 935514 (Average Length: 765.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 935514 (Average: 16.67 Max: 1087 Sum: 15592173) + Executed : 935405 (Average: 16.66 Max: 1087 Sum: 15586552 Ratio: 99.96%) + Bounded : 109 (Average: 51.57 Max: 117 Sum: 5621 Ratio: 0.04%) + +Rules : 150282 (Original: 135817) +Atoms : 72364 +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 : 6202734 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1017MB +Max. Length : 115 steps +Models : 1 + +