From dee0e0420ea035cc0e33122476736d1841c1ea1b Mon Sep 17 00:00:00 2001 From: potassco-bot Date: Sun, 18 Feb 2018 14:41:44 +0100 Subject: [PATCH] Add benchmark result [gc-ta1-tt1-trendy | ipc-2011 | barman-sequential-satisficing | 2] --- ...c-2011_barman-sequential-satisficing_2.env | 59 + ...c-2011_barman-sequential-satisficing_2.err | 8 + ...c-2011_barman-sequential-satisficing_2.out | 1327 +++++++++++++++++ 3 files changed, 1394 insertions(+) create mode 100644 gc-ta1-tt1-trendy/ipc-2011_barman-sequential-satisficing_2.env create mode 100644 gc-ta1-tt1-trendy/ipc-2011_barman-sequential-satisficing_2.err create mode 100644 gc-ta1-tt1-trendy/ipc-2011_barman-sequential-satisficing_2.out diff --git a/gc-ta1-tt1-trendy/ipc-2011_barman-sequential-satisficing_2.env b/gc-ta1-tt1-trendy/ipc-2011_barman-sequential-satisficing_2.env new file mode 100644 index 000000000..13aff7230 --- /dev/null +++ b/gc-ta1-tt1-trendy/ipc-2011_barman-sequential-satisficing_2.env @@ -0,0 +1,59 @@ +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-2.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=trendy +- -i 0 +configuration: + id: gc-ta1-tt1-trendy + 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 + - --configuration=trendy + - -i 0 +exitCode: 0 +instance: + domain: barman-sequential-satisficing + instance: 2 + ipc: ipc-2011 + planLength: 105 +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-trendy/ipc-2011_barman-sequential-satisficing_2.err b/gc-ta1-tt1-trendy/ipc-2011_barman-sequential-satisficing_2.err new file mode 100644 index 000000000..492eb8986 --- /dev/null +++ b/gc-ta1-tt1-trendy/ipc-2011_barman-sequential-satisficing_2.err @@ -0,0 +1,8 @@ +# configuration: {'id': 'gc-ta1-tt1-trendy', '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', '--configuration=trendy', '-i 0'], 'instanceSets': ['rintanen-aij-2012-interesting']} +# instance: {'ipc': 'ipc-2011', 'domain': 'barman-sequential-satisficing', 'instance': 2, 'planLength': 105} +# 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-2.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=trendy', '-i 0'] +# working directory: /home/pluehne/Documents/ASP/plasp-javier/encodings/planner +# exit code: 0 +TIMEOUT CPU 900.10 MEM 716268 MAXMEM 716268 STALE 1 MAXMEM_RSS 605856 + + diff --git a/gc-ta1-tt1-trendy/ipc-2011_barman-sequential-satisficing_2.out b/gc-ta1-tt1-trendy/ipc-2011_barman-sequential-satisficing_2.out new file mode 100644 index 000000000..ad2b221db --- /dev/null +++ b/gc-ta1-tt1-trendy/ipc-2011_barman-sequential-satisficing_2.out @@ -0,0 +1,1327 @@ +INFO Running translator. +INFO translator input: ['/home/pluehne/Documents/ASP/pddl-instances/ipc-2011/domains/barman-sequential-satisficing/domain.pddl', '/home/pluehne/Documents/ASP/pddl-instances/ipc-2011/domains/barman-sequential-satisficing/instances/instance-2.pddl'] +INFO translator arguments: [] +INFO translator time limit: None +INFO translator memory limit: None +INFO callstring: /home/pluehne/.usr/bin/python /home/wv/bin/linux/64/fast-downward-10997/builds/release64/bin/translate/translate.py /home/pluehne/Documents/ASP/pddl-instances/ipc-2011/domains/barman-sequential-satisficing/domain.pddl /home/pluehne/Documents/ASP/pddl-instances/ipc-2011/domains/barman-sequential-satisficing/instances/instance-2.pddl +Parsing... +Parsing: [0.040s CPU, 0.045s wall-clock] +Normalizing task... [0.010s CPU, 0.003s wall-clock] +Instantiating... +Generating Datalog program... [0.000s CPU, 0.011s wall-clock] +Normalizing Datalog program... +Normalizing Datalog program: [0.060s CPU, 0.053s wall-clock] +Preparing model... [0.020s CPU, 0.027s wall-clock] +Generated 115 rules. +Computing model... [0.340s CPU, 0.335s wall-clock] +2025 relevant atoms +2105 auxiliary atoms +4130 final queue length +7122 total queue pushes +Completing instantiation... [0.600s CPU, 0.598s wall-clock] +Instantiating: [1.020s CPU, 1.030s wall-clock] +Computing fact groups... +Finding invariants... +24 initial candidates +Finding invariants: [0.110s CPU, 0.109s wall-clock] +Checking invariant weight... [0.000s CPU, 0.001s wall-clock] +Instantiating groups... [0.010s CPU, 0.006s wall-clock] +Collecting mutex groups... [0.000s CPU, 0.000s wall-clock] +Choosing groups... +207 uncovered facts +Choosing groups: [0.000s CPU, 0.001s wall-clock] +Building translation key... [0.010s CPU, 0.008s wall-clock] +Computing fact groups: [0.140s CPU, 0.142s wall-clock] +Building STRIPS to SAS dictionary... [0.000s CPU, 0.002s wall-clock] +Building dictionary for full mutex groups... [0.000s CPU, 0.002s wall-clock] +Building mutex information... +Building mutex information: [0.010s CPU, 0.002s wall-clock] +Translating task... +Processing axioms... +Simplifying axioms... [0.000s CPU, 0.000s wall-clock] +Processing axioms: [0.030s CPU, 0.033s wall-clock] +Translating task: [0.650s CPU, 0.655s wall-clock] +2326 effect conditions simplified +0 implied preconditions added +Detecting unreachable propositions... +0 operators removed +0 axioms removed +3 propositions removed +Detecting unreachable propositions: [0.310s CPU, 0.308s wall-clock] +Reordering and filtering variables... +210 of 210 variables necessary. +11 of 14 mutex groups necessary. +1390 of 1390 operators necessary. +0 of 0 axiom rules necessary. +Reordering and filtering variables: [0.210s CPU, 0.206s wall-clock] +Translator variables: 210 +Translator derived variables: 0 +Translator facts: 441 +Translator goal facts: 9 +Translator mutex groups: 11 +Translator total mutex groups size: 33 +Translator operators: 1390 +Translator axioms: 0 +Translator task size: 13333 +Translator peak memory: 43980 KB +Writing output... [0.260s CPU, 0.275s wall-clock] +Done! [2.670s CPU, 2.696s wall-clock] +planner.py version 0.0.1 + +Time: 0.56s +Memory: 86MB + +Iteration 1 +Queue: [(0,0,0,True), (1,5,0,True), (2,10,0,True), (3,15,0,True), (4,20,0,True), (5,25,0,True), (6,30,0,True)] +Grounded Until: 0 +Solving... +[start: stats after solve call] + +Models : 0 +Calls : 1 +Time : 0.654s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s) +CPU Time : 0.560s + +Choices : 0 +Conflicts : 0 (Analyzed: 0) +Restarts : 0 +Problems : 1 (Average Length: 2.00 Splits: 0) +Lemmas : 0 (Deleted: 0) + Binary : 0 (Ratio: 0.00%) + Ternary : 0 (Ratio: 0.00%) + Conflict : 0 (Average Length: 0.0 Ratio: 0.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 0 (Average: 0.00 Max: 0 Sum: 0) + Executed : 0 (Average: 0.00 Max: 0 Sum: 0 Ratio: 0.00%) + Bounded : 0 (Average: 0.00 Max: 0 Sum: 0 Ratio: 100.00%) + +Rules : 38518 +Atoms : 38518 +Bodies : 1 (Original: 0) +Tight : Yes +Variables : 0 (Eliminated: 0 Frozen: 0) +Constraints : 0 (Binary: 0.0% Ternary: 0.0% Other: 0.0%) + +Memory Peak : 222MB +Max. Length : 0 steps +Models : 0 + +[endof: stats after solve call] +Solving Time: 0.00s +Memory: 158MB (+72MB) +UNSAT +Iteration Time: 0.00s + +Iteration 2 +Queue: [(1,5,0,True), (2,10,0,True), (3,15,0,True), (4,20,0,True), (5,25,0,True), (6,30,0,True)] +Grounded Until: 0 +Expected Memory: 158MB +Grounding... [('step', [1]), ('step', [2]), ('step', [3]), ('step', [4]), ('step', [5]), ('check', [5])] +Grounding Time: 0.15s +Memory: 158MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 1+ +Calls : 2 +Time : 0.980s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s) +CPU Time : 0.884s + +Choices : 152 (Domain: 73) +Conflicts : 2 (Analyzed: 2) +Restarts : 0 +Model-Level : 147.0 +Problems : 2 (Average Length: 4.50 Splits: 0) +Lemmas : 2 (Deleted: 0) + Binary : 0 (Ratio: 0.00%) + Ternary : 0 (Ratio: 0.00%) + Conflict : 2 (Average Length: 23.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 2 (Average: 6.00 Max: 11 Sum: 12) + Executed : 2 (Average: 6.00 Max: 11 Sum: 12 Ratio: 100.00%) + Bounded : 0 (Average: 0.00 Max: 0 Sum: 0 Ratio: 0.00%) + +Rules : 38518 +Atoms : 38518 +Bodies : 1 (Original: 0) +Tight : Yes +Variables : 10322 (Eliminated: 0 Frozen: 10322) +Constraints : 36431 (Binary: 95.0% Ternary: 3.5% Other: 1.5%) + +Memory Peak : 222MB +Max. Length : 0 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 0.10s +Memory: 160MB (+2MB) +SAT +Testing... +NOT SERIALIZABLE +Testing Time: 0.62s +Memory: 178MB (+18MB) +Solving... +[start: stats after solve call] + +Models : 0 +Calls : 3 +Time : 1.079s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s) +CPU Time : 0.984s + +Choices : 161 (Domain: 78) +Conflicts : 9 (Analyzed: 8) +Restarts : 0 +Model-Level : 147.0 +Problems : 3 (Average Length: 5.33 Splits: 0) +Lemmas : 8 (Deleted: 0) + Binary : 1 (Ratio: 12.50%) + Ternary : 2 (Ratio: 25.00%) + Conflict : 8 (Average Length: 8.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 8 (Average: 2.75 Max: 11 Sum: 22) + Executed : 7 (Average: 2.62 Max: 11 Sum: 21 Ratio: 95.45%) + Bounded : 1 (Average: 1.00 Max: 1 Sum: 1 Ratio: 4.55%) + +Rules : 55133 (Original: 53913) +Atoms : 43853 +Bodies : 10280 (Original: 9059) + Count : 232 (Original: 476) +Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) +Tight : Yes +Variables : 12735 (Eliminated: 1464 Frozen: 11271) +Constraints : 50631 (Binary: 90.2% Ternary: 5.9% Other: 3.9%) + +Memory Peak : 222MB +Max. Length : 0 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 0.03s +Memory: 178MB (+0MB) +UNSAT +Iteration Time: 0.97s + +Iteration 3 +Queue: [(2,10,0,True), (3,15,0,True), (4,20,0,True), (5,25,0,True), (6,30,0,True)] +Grounded Until: 5 +Expected Memory: 180.0MB +Grounding... [('step', [6]), ('step', [7]), ('step', [8]), ('step', [9]), ('step', [10]), ('check', [10])] +Grounding Time: 0.29s +Memory: 178MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0 +Calls : 4 +Time : 2.238s (Solving: 0.46s 1st Model: 0.00s Unsat: 0.46s) +CPU Time : 2.144s + +Choices : 16216 (Domain: 12582) +Conflicts : 1864 (Analyzed: 1862) +Restarts : 6 (Average: 310.33 Last: 87) +Model-Level : 147.0 +Problems : 4 (Average Length: 7.00 Splits: 0) +Lemmas : 1862 (Deleted: 0) + Binary : 210 (Ratio: 11.28%) + Ternary : 280 (Ratio: 15.04%) + Conflict : 1862 (Average Length: 24.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 1862 (Average: 8.69 Max: 184 Sum: 16185) + Executed : 1840 (Average: 8.57 Max: 184 Sum: 15954 Ratio: 98.57%) + Bounded : 22 (Average: 10.50 Max: 12 Sum: 231 Ratio: 1.43%) + +Rules : 55133 (Original: 53913) +Atoms : 43853 +Bodies : 10280 (Original: 9059) + Count : 232 (Original: 476) +Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) +Tight : Yes +Variables : 35311 (Eliminated: 1464 Frozen: 26317) +Constraints : 223676 (Binary: 91.3% Ternary: 6.4% Other: 2.3%) + +Memory Peak : 222MB +Max. Length : 5 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 0.77s +Memory: 189MB (+11MB) +UNSAT +Iteration Time: 1.16s + +Iteration 4 +Queue: [(3,15,0,True), (4,20,0,True), (5,25,0,True), (6,30,0,True)] +Grounded Until: 10 +Expected Memory: 200.0MB +Grounding... [('step', [11]), ('step', [12]), ('step', [13]), ('step', [14]), ('step', [15]), ('check', [15])] +Grounding Time: 0.33s +Memory: 195MB (+6MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0 +Calls : 5 +Time : 10.101s (Solving: 7.55s 1st Model: 0.00s Unsat: 7.55s) +CPU Time : 10.008s + +Choices : 169527 (Domain: 131701) +Conflicts : 25187 (Analyzed: 25184) +Restarts : 64 (Average: 393.50 Last: 646) +Model-Level : 147.0 +Problems : 5 (Average Length: 9.00 Splits: 0) +Lemmas : 25184 (Deleted: 13000) + Binary : 1242 (Ratio: 4.93%) + Ternary : 544 (Ratio: 2.16%) + Conflict : 25184 (Average Length: 261.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 25184 (Average: 6.56 Max: 810 Sum: 165120) + Executed : 25150 (Average: 6.54 Max: 810 Sum: 164701 Ratio: 99.75%) + Bounded : 34 (Average: 12.32 Max: 17 Sum: 419 Ratio: 0.25%) + +Rules : 55133 (Original: 53913) +Atoms : 43853 +Bodies : 10280 (Original: 9059) + Count : 232 (Original: 476) +Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) +Tight : Yes +Variables : 57887 (Eliminated: 1464 Frozen: 48893) +Constraints : 380813 (Binary: 91.5% Ternary: 6.3% Other: 2.1%) + +Memory Peak : 222MB +Max. Length : 10 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.42s +Memory: 209MB (+14MB) +UNSAT +Iteration Time: 7.87s + +Iteration 5 +Queue: [(4,20,0,True), (5,25,0,True), (6,30,0,True)] +Grounded Until: 15 +Expected Memory: 229.0MB +Grounding... [('step', [16]), ('step', [17]), ('step', [18]), ('step', [19]), ('step', [20]), ('check', [20])] +Grounding Time: 0.30s +Memory: 212MB (+3MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 6 +Time : 22.348s (Solving: 19.03s 1st Model: 0.00s Unsat: 7.55s) +CPU Time : 22.264s + +Choices : 374743 (Domain: 319885) +Conflicts : 47955 (Analyzed: 47952) +Restarts : 164 (Average: 292.39 Last: 646) +Model-Level : 147.0 +Problems : 6 (Average Length: 11.17 Splits: 0) +Lemmas : 47952 (Deleted: 32192) + Binary : 2387 (Ratio: 4.98%) + Ternary : 898 (Ratio: 1.87%) + Conflict : 47952 (Average Length: 334.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 47952 (Average: 7.49 Max: 810 Sum: 359221) + Executed : 47918 (Average: 7.48 Max: 810 Sum: 358802 Ratio: 99.88%) + Bounded : 34 (Average: 12.32 Max: 17 Sum: 419 Ratio: 0.12%) + +Rules : 55133 (Original: 53913) +Atoms : 43853 +Bodies : 10280 (Original: 9059) + Count : 232 (Original: 476) +Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) +Tight : Yes +Variables : 80463 (Eliminated: 1464 Frozen: 71469) +Constraints : 538208 (Binary: 91.6% Ternary: 6.3% Other: 2.0%) + +Memory Peak : 227MB +Max. Length : 15 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 11.82s +Memory: 227MB (+15MB) +UNKNOWN +Iteration Time: 12.26s + +Iteration 6 +Queue: [(5,25,0,True), (6,30,0,True)] +Grounded Until: 20 +Expected Memory: 247.0MB +Grounding... [('step', [21]), ('step', [22]), ('step', [23]), ('step', [24]), ('step', [25]), ('check', [25])] +Grounding Time: 0.31s +Memory: 230MB (+3MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 7 +Time : 80.558s (Solving: 76.46s 1st Model: 0.00s Unsat: 7.55s) +CPU Time : 80.500s + +Choices : 815840 (Domain: 723921) +Conflicts : 125928 (Analyzed: 125925) +Restarts : 264 (Average: 476.99 Last: 715) +Model-Level : 147.0 +Problems : 7 (Average Length: 13.43 Splits: 0) +Lemmas : 125925 (Deleted: 94595) + Binary : 4155 (Ratio: 3.30%) + Ternary : 1257 (Ratio: 1.00%) + Conflict : 125925 (Average Length: 861.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 125925 (Average: 6.23 Max: 810 Sum: 784831) + Executed : 125890 (Average: 6.23 Max: 810 Sum: 784385 Ratio: 99.94%) + Bounded : 35 (Average: 12.74 Max: 27 Sum: 446 Ratio: 0.06%) + +Rules : 55133 (Original: 53913) +Atoms : 43853 +Bodies : 10280 (Original: 9059) + Count : 232 (Original: 476) +Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) +Tight : Yes +Variables : 103039 (Eliminated: 1464 Frozen: 94045) +Constraints : 711253 (Binary: 91.6% Ternary: 6.4% Other: 2.0%) + +Memory Peak : 434MB +Max. Length : 20 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 57.78s +Memory: 370MB (+140MB) +UNKNOWN +Iteration Time: 58.24s + +Iteration 7 +Queue: [(6,30,0,True)] +Grounded Until: 25 +Expected Memory: 513.0MB +Grounding... [('step', [26]), ('step', [27]), ('step', [28]), ('step', [29]), ('step', [30]), ('check', [30])] +Grounding Time: 0.33s +Memory: 372MB (+2MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 8 +Time : 105.603s (Solving: 100.63s 1st Model: 0.00s Unsat: 7.55s) +CPU Time : 105.556s + +Choices : 1076248 (Domain: 975350) +Conflicts : 158464 (Analyzed: 158461) +Restarts : 364 (Average: 435.33 Last: 715) +Model-Level : 147.0 +Problems : 8 (Average Length: 15.75 Splits: 0) +Lemmas : 158461 (Deleted: 124965) + Binary : 5202 (Ratio: 3.28%) + Ternary : 1554 (Ratio: 0.98%) + Conflict : 158461 (Average Length: 893.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 158461 (Average: 6.48 Max: 810 Sum: 1026131) + Executed : 158426 (Average: 6.47 Max: 810 Sum: 1025685 Ratio: 99.96%) + Bounded : 35 (Average: 12.74 Max: 27 Sum: 446 Ratio: 0.04%) + +Rules : 55133 (Original: 53913) +Atoms : 43853 +Bodies : 10280 (Original: 9059) + Count : 232 (Original: 476) +Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) +Tight : Yes +Variables : 125615 (Eliminated: 1464 Frozen: 116621) +Constraints : 884284 (Binary: 91.6% Ternary: 6.4% Other: 2.0%) + +Memory Peak : 434MB +Max. Length : 25 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 24.53s +Memory: 390MB (+18MB) +UNKNOWN +Iteration Time: 25.06s + +Iteration 8 +Queue: [(4,20,1,True), (5,25,1,True), (6,30,1,True), (7,35,0,True), (8,40,0,True), (9,45,0,True), (10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True), (17,85,0,True)] +Grounded Until: 30 +Blocking actions... +Solving... +[start: stats after solve call] + +Models : 0 +Calls : 9 +Time : 117.385s (Solving: 112.37s 1st Model: 0.00s Unsat: 19.29s) +CPU Time : 117.344s + +Choices : 1183703 (Domain: 1082805) +Conflicts : 181734 (Analyzed: 181730) +Restarts : 453 (Average: 401.17 Last: 2225) +Model-Level : 147.0 +Problems : 9 (Average Length: 17.56 Splits: 0) +Lemmas : 181730 (Deleted: 156271) + Binary : 5462 (Ratio: 3.01%) + Ternary : 1596 (Ratio: 0.88%) + Conflict : 181730 (Average Length: 832.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 181730 (Average: 6.20 Max: 810 Sum: 1126824) + Executed : 181693 (Average: 6.20 Max: 810 Sum: 1126345 Ratio: 99.96%) + Bounded : 37 (Average: 12.95 Max: 32 Sum: 479 Ratio: 0.04%) + +Rules : 55133 (Original: 53913) +Atoms : 43853 +Bodies : 10280 (Original: 9059) + Count : 232 (Original: 476) +Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) +Tight : Yes +Variables : 125615 (Eliminated: 1464 Frozen: 124151) +Constraints : 884284 (Binary: 91.6% Ternary: 6.4% Other: 2.0%) + +Memory Peak : 434MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 11.76s +Memory: 390MB (+0MB) +UNSAT +Iteration Time: 11.79s + +Iteration 9 +Queue: [(5,25,1,True), (6,30,1,True), (7,35,0,True), (8,40,0,True), (9,45,0,True), (10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True), (17,85,0,True)] +Grounded Until: 30 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 10 +Time : 215.633s (Solving: 210.58s 1st Model: 0.00s Unsat: 19.29s) +CPU Time : 215.632s + +Choices : 1445562 (Domain: 1343837) +Conflicts : 271751 (Analyzed: 271747) +Restarts : 553 (Average: 491.41 Last: 2225) +Model-Level : 147.0 +Problems : 10 (Average Length: 19.00 Splits: 0) +Lemmas : 271747 (Deleted: 225148) + Binary : 5774 (Ratio: 2.12%) + Ternary : 1677 (Ratio: 0.62%) + Conflict : 271747 (Average Length: 1005.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 271747 (Average: 5.06 Max: 810 Sum: 1375959) + Executed : 271710 (Average: 5.06 Max: 810 Sum: 1375480 Ratio: 99.97%) + Bounded : 37 (Average: 12.95 Max: 32 Sum: 479 Ratio: 0.03%) + +Rules : 55133 (Original: 53913) +Atoms : 43853 +Bodies : 10280 (Original: 9059) + Count : 232 (Original: 476) +Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) +Tight : Yes +Variables : 125615 (Eliminated: 1464 Frozen: 124151) +Constraints : 884270 (Binary: 91.6% Ternary: 6.4% Other: 2.0%) + +Memory Peak : 434MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 98.28s +Memory: 390MB (+0MB) +UNKNOWN +Iteration Time: 98.29s + +Iteration 10 +Queue: [(6,30,1,True), (7,35,0,True), (8,40,0,True), (9,45,0,True), (10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True), (17,85,0,True)] +Grounded Until: 30 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 11 +Time : 246.089s (Solving: 240.98s 1st Model: 0.00s Unsat: 19.29s) +CPU Time : 246.100s + +Choices : 1735384 (Domain: 1628814) +Conflicts : 312268 (Analyzed: 312264) +Restarts : 653 (Average: 478.20 Last: 2225) +Model-Level : 147.0 +Problems : 11 (Average Length: 20.18 Splits: 0) +Lemmas : 312264 (Deleted: 280698) + Binary : 6447 (Ratio: 2.06%) + Ternary : 1812 (Ratio: 0.58%) + Conflict : 312264 (Average Length: 1009.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 312264 (Average: 5.27 Max: 810 Sum: 1646666) + Executed : 312227 (Average: 5.27 Max: 810 Sum: 1646187 Ratio: 99.97%) + Bounded : 37 (Average: 12.95 Max: 32 Sum: 479 Ratio: 0.03%) + +Rules : 55133 (Original: 53913) +Atoms : 43853 +Bodies : 10280 (Original: 9059) + Count : 232 (Original: 476) +Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) +Tight : Yes +Variables : 125615 (Eliminated: 1464 Frozen: 124151) +Constraints : 884270 (Binary: 91.6% Ternary: 6.4% Other: 2.0%) + +Memory Peak : 454MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 30.43s +Memory: 454MB (+64MB) +UNKNOWN +Iteration Time: 30.47s + +Iteration 11 +Queue: [(7,35,0,True), (8,40,0,True), (9,45,0,True), (10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True), (17,85,0,True)] +Grounded Until: 30 +Expected Memory: 597.0MB +Grounding... [('step', [31]), ('step', [32]), ('step', [33]), ('step', [34]), ('step', [35]), ('check', [35])] +Grounding Time: 0.38s +Memory: 455MB (+1MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 12 +Time : 285.188s (Solving: 279.16s 1st Model: 0.00s Unsat: 19.29s) +CPU Time : 285.216s + +Choices : 2020824 (Domain: 1901625) +Conflicts : 365309 (Analyzed: 365305) +Restarts : 753 (Average: 485.13 Last: 2225) +Model-Level : 147.0 +Problems : 12 (Average Length: 21.58 Splits: 0) +Lemmas : 365305 (Deleted: 336429) + Binary : 7448 (Ratio: 2.04%) + Ternary : 1978 (Ratio: 0.54%) + Conflict : 365305 (Average Length: 1025.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 365305 (Average: 5.24 Max: 810 Sum: 1912959) + Executed : 365268 (Average: 5.24 Max: 810 Sum: 1912480 Ratio: 99.97%) + Bounded : 37 (Average: 12.95 Max: 32 Sum: 479 Ratio: 0.03%) + +Rules : 55133 (Original: 53913) +Atoms : 43853 +Bodies : 10280 (Original: 9059) + Count : 232 (Original: 476) +Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) +Tight : Yes +Variables : 148191 (Eliminated: 1464 Frozen: 139197) +Constraints : 1057315 (Binary: 91.6% Ternary: 6.4% Other: 2.0%) + +Memory Peak : 476MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 38.55s +Memory: 469MB (+14MB) +UNKNOWN +Iteration Time: 39.12s + +Iteration 12 +Queue: [(8,40,0,True), (9,45,0,True), (10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True), (17,85,0,True)] +Grounded Until: 35 +Expected Memory: 612.0MB +Grounding... [('step', [36]), ('step', [37]), ('step', [38]), ('step', [39]), ('step', [40]), ('check', [40])] +Grounding Time: 0.40s +Memory: 476MB (+7MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 13 +Time : 312.484s (Solving: 305.51s 1st Model: 0.00s Unsat: 19.29s) +CPU Time : 312.524s + +Choices : 2324390 (Domain: 2192754) +Conflicts : 406897 (Analyzed: 406893) +Restarts : 853 (Average: 477.01 Last: 2225) +Model-Level : 147.0 +Problems : 13 (Average Length: 23.15 Splits: 0) +Lemmas : 406893 (Deleted: 373689) + Binary : 8553 (Ratio: 2.10%) + Ternary : 2158 (Ratio: 0.53%) + Conflict : 406893 (Average Length: 1003.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 406893 (Average: 5.39 Max: 810 Sum: 2194438) + Executed : 406856 (Average: 5.39 Max: 810 Sum: 2193959 Ratio: 99.98%) + Bounded : 37 (Average: 12.95 Max: 32 Sum: 479 Ratio: 0.02%) + +Rules : 55133 (Original: 53913) +Atoms : 43853 +Bodies : 10280 (Original: 9059) + Count : 232 (Original: 476) +Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) +Tight : Yes +Variables : 170767 (Eliminated: 1464 Frozen: 161773) +Constraints : 1230360 (Binary: 91.6% Ternary: 6.4% Other: 2.0%) + +Memory Peak : 502MB +Max. Length : 35 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 26.73s +Memory: 490MB (+14MB) +UNKNOWN +Iteration Time: 27.32s + +Iteration 13 +Queue: [(9,45,0,True), (10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True), (17,85,0,True)] +Grounded Until: 40 +Expected Memory: 633.0MB +Grounding... [('step', [41]), ('step', [42]), ('step', [43]), ('step', [44]), ('step', [45]), ('check', [45])] +Grounding Time: 0.34s +Memory: 493MB (+3MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 14 +Time : 370.087s (Solving: 362.23s 1st Model: 0.00s Unsat: 19.29s) +CPU Time : 370.152s + +Choices : 3040085 (Domain: 2888738) +Conflicts : 497748 (Analyzed: 497744) +Restarts : 953 (Average: 522.29 Last: 2225) +Model-Level : 147.0 +Problems : 14 (Average Length: 24.86 Splits: 0) +Lemmas : 497744 (Deleted: 460723) + Binary : 11080 (Ratio: 2.23%) + Ternary : 2479 (Ratio: 0.50%) + Conflict : 497744 (Average Length: 973.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 497744 (Average: 5.80 Max: 810 Sum: 2884928) + Executed : 497707 (Average: 5.80 Max: 810 Sum: 2884449 Ratio: 99.98%) + Bounded : 37 (Average: 12.95 Max: 32 Sum: 479 Ratio: 0.02%) + +Rules : 55133 (Original: 53913) +Atoms : 43853 +Bodies : 10280 (Original: 9059) + Count : 232 (Original: 476) +Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) +Tight : Yes +Variables : 193343 (Eliminated: 1464 Frozen: 184349) +Constraints : 1403405 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) + +Memory Peak : 519MB +Max. Length : 40 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 57.09s +Memory: 516MB (+23MB) +UNKNOWN +Iteration Time: 57.64s + +Iteration 14 +Queue: [(10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True), (17,85,0,True)] +Grounded Until: 45 +Expected Memory: 659.0MB +Grounding... [('step', [46]), ('step', [47]), ('step', [48]), ('step', [49]), ('step', [50]), ('check', [50])] +Grounding Time: 0.33s +Memory: 516MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 15 +Time : 409.616s (Solving: 400.86s 1st Model: 0.00s Unsat: 19.29s) +CPU Time : 409.696s + +Choices : 3521524 (Domain: 3359301) +Conflicts : 565727 (Analyzed: 565723) +Restarts : 1053 (Average: 537.25 Last: 2225) +Model-Level : 147.0 +Problems : 15 (Average Length: 26.67 Splits: 0) +Lemmas : 565723 (Deleted: 514457) + Binary : 12917 (Ratio: 2.28%) + Ternary : 2714 (Ratio: 0.48%) + Conflict : 565723 (Average Length: 951.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 565723 (Average: 5.90 Max: 810 Sum: 3339149) + Executed : 565686 (Average: 5.90 Max: 810 Sum: 3338670 Ratio: 99.99%) + Bounded : 37 (Average: 12.95 Max: 32 Sum: 479 Ratio: 0.01%) + +Rules : 55133 (Original: 53913) +Atoms : 43853 +Bodies : 10280 (Original: 9059) + Count : 232 (Original: 476) +Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) +Tight : Yes +Variables : 215919 (Eliminated: 1464 Frozen: 206925) +Constraints : 1576450 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) + +Memory Peak : 545MB +Max. Length : 45 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 39.02s +Memory: 529MB (+13MB) +UNKNOWN +Iteration Time: 39.55s + +Iteration 15 +Queue: [(11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True), (17,85,0,True)] +Grounded Until: 50 +Expected Memory: 672.0MB +Grounding... [('step', [51]), ('step', [52]), ('step', [53]), ('step', [54]), ('step', [55]), ('check', [55])] +Grounding Time: 0.31s +Memory: 529MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 16 +Time : 442.973s (Solving: 433.32s 1st Model: 0.00s Unsat: 19.29s) +CPU Time : 443.068s + +Choices : 3985594 (Domain: 3807049) +Conflicts : 620781 (Analyzed: 620777) +Restarts : 1153 (Average: 538.40 Last: 2225) +Model-Level : 147.0 +Problems : 16 (Average Length: 28.56 Splits: 0) +Lemmas : 620777 (Deleted: 578386) + Binary : 14427 (Ratio: 2.32%) + Ternary : 2968 (Ratio: 0.48%) + Conflict : 620777 (Average Length: 930.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 620777 (Average: 6.08 Max: 810 Sum: 3775604) + Executed : 620740 (Average: 6.08 Max: 810 Sum: 3775125 Ratio: 99.99%) + Bounded : 37 (Average: 12.95 Max: 32 Sum: 479 Ratio: 0.01%) + +Rules : 55133 (Original: 53913) +Atoms : 43853 +Bodies : 10280 (Original: 9059) + Count : 232 (Original: 476) +Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) +Tight : Yes +Variables : 238495 (Eliminated: 1464 Frozen: 229501) +Constraints : 1749495 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) + +Memory Peak : 563MB +Max. Length : 50 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 32.84s +Memory: 544MB (+15MB) +UNKNOWN +Iteration Time: 33.38s + +Iteration 16 +Queue: [(12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True), (17,85,0,True)] +Grounded Until: 55 +Expected Memory: 687.0MB +Grounding... [('step', [56]), ('step', [57]), ('step', [58]), ('step', [59]), ('step', [60]), ('check', [60])] +Grounding Time: 0.32s +Memory: 544MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 17 +Time : 492.674s (Solving: 482.12s 1st Model: 0.00s Unsat: 19.29s) +CPU Time : 492.792s + +Choices : 4646244 (Domain: 4460949) +Conflicts : 705016 (Analyzed: 705012) +Restarts : 1253 (Average: 562.66 Last: 2225) +Model-Level : 147.0 +Problems : 17 (Average Length: 30.53 Splits: 0) +Lemmas : 705012 (Deleted: 647271) + Binary : 16178 (Ratio: 2.29%) + Ternary : 3175 (Ratio: 0.45%) + Conflict : 705012 (Average Length: 911.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 705012 (Average: 6.25 Max: 810 Sum: 4407725) + Executed : 704974 (Average: 6.25 Max: 810 Sum: 4407184 Ratio: 99.99%) + Bounded : 38 (Average: 14.24 Max: 62 Sum: 541 Ratio: 0.01%) + +Rules : 55133 (Original: 53913) +Atoms : 43853 +Bodies : 10280 (Original: 9059) + Count : 232 (Original: 476) +Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) +Tight : Yes +Variables : 261071 (Eliminated: 1464 Frozen: 252077) +Constraints : 1922540 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) + +Memory Peak : 580MB +Max. Length : 55 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 49.19s +Memory: 559MB (+15MB) +UNKNOWN +Iteration Time: 49.73s + +Iteration 17 +Queue: [(13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True), (17,85,0,True)] +Grounded Until: 60 +Expected Memory: 702.0MB +Grounding... [('step', [61]), ('step', [62]), ('step', [63]), ('step', [64]), ('step', [65]), ('check', [65])] +Grounding Time: 0.32s +Memory: 559MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 18 +Time : 532.870s (Solving: 521.39s 1st Model: 0.00s Unsat: 19.29s) +CPU Time : 533.008s + +Choices : 5219606 (Domain: 5022359) +Conflicts : 779482 (Analyzed: 779478) +Restarts : 1353 (Average: 576.11 Last: 2225) +Model-Level : 147.0 +Problems : 18 (Average Length: 32.56 Splits: 0) +Lemmas : 779478 (Deleted: 726205) + Binary : 17910 (Ratio: 2.30%) + Ternary : 3441 (Ratio: 0.44%) + Conflict : 779478 (Average Length: 893.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 779478 (Average: 6.35 Max: 810 Sum: 4951879) + Executed : 779440 (Average: 6.35 Max: 810 Sum: 4951338 Ratio: 99.99%) + Bounded : 38 (Average: 14.24 Max: 62 Sum: 541 Ratio: 0.01%) + +Rules : 55133 (Original: 53913) +Atoms : 43853 +Bodies : 10280 (Original: 9059) + Count : 232 (Original: 476) +Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) +Tight : Yes +Variables : 283647 (Eliminated: 1464 Frozen: 274653) +Constraints : 2095571 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) + +Memory Peak : 597MB +Max. Length : 60 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 39.66s +Memory: 591MB (+32MB) +UNKNOWN +Iteration Time: 40.22s + +Iteration 18 +Queue: [(14,70,0,True), (15,75,0,True), (16,80,0,True), (17,85,0,True)] +Grounded Until: 65 +Expected Memory: 734.0MB +Grounding... [('step', [66]), ('step', [67]), ('step', [68]), ('step', [69]), ('step', [70]), ('check', [70])] +Grounding Time: 0.34s +Memory: 591MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 19 +Time : 564.796s (Solving: 552.36s 1st Model: 0.00s Unsat: 19.29s) +CPU Time : 564.948s + +Choices : 5653911 (Domain: 5454075) +Conflicts : 831295 (Analyzed: 831291) +Restarts : 1453 (Average: 572.12 Last: 2225) +Model-Level : 147.0 +Problems : 19 (Average Length: 34.63 Splits: 0) +Lemmas : 831291 (Deleted: 764176) + Binary : 18968 (Ratio: 2.28%) + Ternary : 3613 (Ratio: 0.43%) + Conflict : 831291 (Average Length: 886.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 831291 (Average: 6.45 Max: 810 Sum: 5357766) + Executed : 831253 (Average: 6.44 Max: 810 Sum: 5357225 Ratio: 99.99%) + Bounded : 38 (Average: 14.24 Max: 62 Sum: 541 Ratio: 0.01%) + +Rules : 55133 (Original: 53913) +Atoms : 43853 +Bodies : 10280 (Original: 9059) + Count : 232 (Original: 476) +Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) +Tight : Yes +Variables : 306223 (Eliminated: 1464 Frozen: 297229) +Constraints : 2268616 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) + +Memory Peak : 629MB +Max. Length : 65 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 31.36s +Memory: 603MB (+12MB) +UNKNOWN +Iteration Time: 31.95s + +Iteration 19 +Queue: [(15,75,0,True), (16,80,0,True), (17,85,0,True)] +Grounded Until: 70 +Expected Memory: 746.0MB +Grounding... [('step', [71]), ('step', [72]), ('step', [73]), ('step', [74]), ('step', [75]), ('check', [75])] +Grounding Time: 0.34s +Memory: 603MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 20 +Time : 617.165s (Solving: 603.75s 1st Model: 0.00s Unsat: 19.29s) +CPU Time : 617.340s + +Choices : 6324741 (Domain: 6124740) +Conflicts : 910938 (Analyzed: 910934) +Restarts : 1553 (Average: 586.56 Last: 2225) +Model-Level : 147.0 +Problems : 20 (Average Length: 36.75 Splits: 0) +Lemmas : 910934 (Deleted: 845824) + Binary : 20287 (Ratio: 2.23%) + Ternary : 3786 (Ratio: 0.42%) + Conflict : 910934 (Average Length: 878.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 910934 (Average: 6.58 Max: 810 Sum: 5995248) + Executed : 910896 (Average: 6.58 Max: 810 Sum: 5994707 Ratio: 99.99%) + Bounded : 38 (Average: 14.24 Max: 62 Sum: 541 Ratio: 0.01%) + +Rules : 55133 (Original: 53913) +Atoms : 43853 +Bodies : 10280 (Original: 9059) + Count : 232 (Original: 476) +Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) +Tight : Yes +Variables : 328799 (Eliminated: 1464 Frozen: 319805) +Constraints : 2441661 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) + +Memory Peak : 643MB +Max. Length : 70 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 51.79s +Memory: 617MB (+14MB) +UNKNOWN +Iteration Time: 52.40s + +Iteration 20 +Queue: [(16,80,0,True), (17,85,0,True)] +Grounded Until: 75 +Expected Memory: 760.0MB +Grounding... [('step', [76]), ('step', [77]), ('step', [78]), ('step', [79]), ('step', [80]), ('check', [80])] +Grounding Time: 0.48s +Memory: 633MB (+16MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 21 +Time : 656.065s (Solving: 641.53s 1st Model: 0.00s Unsat: 19.29s) +CPU Time : 656.260s + +Choices : 6830979 (Domain: 6625457) +Conflicts : 971635 (Analyzed: 971631) +Restarts : 1653 (Average: 587.80 Last: 2225) +Model-Level : 147.0 +Problems : 21 (Average Length: 38.90 Splits: 0) +Lemmas : 971631 (Deleted: 904777) + Binary : 21300 (Ratio: 2.19%) + Ternary : 3935 (Ratio: 0.40%) + Conflict : 971631 (Average Length: 876.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 971631 (Average: 6.66 Max: 810 Sum: 6468366) + Executed : 971593 (Average: 6.66 Max: 810 Sum: 6467825 Ratio: 99.99%) + Bounded : 38 (Average: 14.24 Max: 62 Sum: 541 Ratio: 0.01%) + +Rules : 55133 (Original: 53913) +Atoms : 43853 +Bodies : 10280 (Original: 9059) + Count : 232 (Original: 476) +Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) +Tight : Yes +Variables : 351375 (Eliminated: 1464 Frozen: 342381) +Constraints : 2614706 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) + +Memory Peak : 679MB +Max. Length : 75 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 38.18s +Memory: 646MB (+13MB) +UNKNOWN +Iteration Time: 38.92s + +Iteration 21 +Queue: [(17,85,0,True)] +Grounded Until: 80 +Expected Memory: 789.0MB +Grounding... [('step', [81]), ('step', [82]), ('step', [83]), ('step', [84]), ('step', [85]), ('check', [85])] +Grounding Time: 0.32s +Memory: 646MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 22 +Time : 695.874s (Solving: 680.36s 1st Model: 0.00s Unsat: 19.29s) +CPU Time : 696.088s + +Choices : 7358251 (Domain: 7150785) +Conflicts : 1030352 (Analyzed: 1030348) +Restarts : 1753 (Average: 587.76 Last: 2225) +Model-Level : 147.0 +Problems : 22 (Average Length: 41.09 Splits: 0) +Lemmas : 1030348 (Deleted: 961806) + Binary : 22392 (Ratio: 2.17%) + Ternary : 4092 (Ratio: 0.40%) + Conflict : 1030348 (Average Length: 874.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 1030348 (Average: 6.75 Max: 810 Sum: 6956440) + Executed : 1030310 (Average: 6.75 Max: 810 Sum: 6955899 Ratio: 99.99%) + Bounded : 38 (Average: 14.24 Max: 62 Sum: 541 Ratio: 0.01%) + +Rules : 55133 (Original: 53913) +Atoms : 43853 +Bodies : 10280 (Original: 9059) + Count : 232 (Original: 476) +Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) +Tight : Yes +Variables : 373951 (Eliminated: 1464 Frozen: 364957) +Constraints : 2787751 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) + +Memory Peak : 695MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 39.24s +Memory: 660MB (+14MB) +UNKNOWN +Iteration Time: 39.84s + +Iteration 22 +Queue: [(5,25,2,True), (6,30,2,True), (7,35,1,True), (8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True), (22,110,0,True)] +Grounded Until: 85 +Blocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 23 +Time : 784.181s (Solving: 768.56s 1st Model: 0.00s Unsat: 19.29s) +CPU Time : 784.432s + +Choices : 7583190 (Domain: 7375724) +Conflicts : 1111482 (Analyzed: 1111478) +Restarts : 1853 (Average: 599.83 Last: 2225) +Model-Level : 147.0 +Problems : 23 (Average Length: 43.09 Splits: 0) +Lemmas : 1111478 (Deleted: 1037390) + Binary : 22557 (Ratio: 2.03%) + Ternary : 4130 (Ratio: 0.37%) + Conflict : 1111478 (Average Length: 913.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 1111478 (Average: 6.45 Max: 810 Sum: 7170472) + Executed : 1111440 (Average: 6.45 Max: 810 Sum: 7169931 Ratio: 99.99%) + Bounded : 38 (Average: 14.24 Max: 62 Sum: 541 Ratio: 0.01%) + +Rules : 55133 (Original: 53913) +Atoms : 43853 +Bodies : 10280 (Original: 9059) + Count : 232 (Original: 476) +Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) +Tight : Yes +Variables : 373951 (Eliminated: 1464 Frozen: 372487) +Constraints : 2787751 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) + +Memory Peak : 695MB +Max. Length : 85 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 88.30s +Memory: 662MB (+2MB) +UNKNOWN +Iteration Time: 88.35s + +Iteration 23 +Queue: [(6,30,2,True), (7,35,1,True), (8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True), (22,110,0,True)] +Grounded Until: 85 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 24 +Time : 827.747s (Solving: 812.03s 1st Model: 0.00s Unsat: 19.29s) +CPU Time : 828.016s + +Choices : 7863730 (Domain: 7656264) +Conflicts : 1160129 (Analyzed: 1160125) +Restarts : 1953 (Average: 594.02 Last: 2225) +Model-Level : 147.0 +Problems : 24 (Average Length: 44.92 Splits: 0) +Lemmas : 1160125 (Deleted: 1083829) + Binary : 22746 (Ratio: 1.96%) + Ternary : 4163 (Ratio: 0.36%) + Conflict : 1160125 (Average Length: 930.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 1160125 (Average: 6.41 Max: 810 Sum: 7432623) + Executed : 1160087 (Average: 6.41 Max: 810 Sum: 7432082 Ratio: 99.99%) + Bounded : 38 (Average: 14.24 Max: 62 Sum: 541 Ratio: 0.01%) + +Rules : 55133 (Original: 53913) +Atoms : 43853 +Bodies : 10280 (Original: 9059) + Count : 232 (Original: 476) +Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) +Tight : Yes +Variables : 373951 (Eliminated: 1464 Frozen: 372487) +Constraints : 2787751 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) + +Memory Peak : 695MB +Max. Length : 85 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 43.55s +Memory: 662MB (+0MB) +UNKNOWN +Iteration Time: 43.59s + +Iteration 24 +Queue: [(7,35,1,True), (8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True), (22,110,0,True)] +Grounded Until: 85 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 25 +Time : 879.751s (Solving: 863.89s 1st Model: 0.00s Unsat: 19.29s) +CPU Time : 880.044s + +Choices : 8128841 (Domain: 7921375) +Conflicts : 1220760 (Analyzed: 1220756) +Restarts : 2053 (Average: 594.62 Last: 2225) +Model-Level : 147.0 +Problems : 25 (Average Length: 46.60 Splits: 0) +Lemmas : 1220756 (Deleted: 1147275) + Binary : 22983 (Ratio: 1.88%) + Ternary : 4224 (Ratio: 0.35%) + Conflict : 1220756 (Average Length: 941.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 1220756 (Average: 6.29 Max: 810 Sum: 7678134) + Executed : 1220718 (Average: 6.29 Max: 810 Sum: 7677593 Ratio: 99.99%) + Bounded : 38 (Average: 14.24 Max: 62 Sum: 541 Ratio: 0.01%) + +Rules : 55133 (Original: 53913) +Atoms : 43853 +Bodies : 10280 (Original: 9059) + Count : 232 (Original: 476) +Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) +Tight : Yes +Variables : 373951 (Eliminated: 1464 Frozen: 372487) +Constraints : 2787751 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) + +Memory Peak : 695MB +Max. Length : 85 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 51.96s +Memory: 662MB (+0MB) +UNKNOWN +Iteration Time: 52.03s + +Iteration 25 +Queue: [(8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True), (22,110,0,True)] +Grounded Until: 85 +Unblocking actions... +Solving... +*** Info : (planner): INTERRUPTED by signal! +UNKNOWN + +INTERRUPTED : 1 + +Models : 0+ +Calls : 26 +Time : 895.001s (Solving: 879.05s 1st Model: 0.00s Unsat: 19.29s) +CPU Time : 895.284s + +Choices : 8289380 (Domain: 8081914) +Conflicts : 1245722 (Analyzed: 1245718) +Restarts : 2111 (Average: 590.11 Last: 2225) +Model-Level : 147.0 +Problems : 26 (Average Length: 48.15 Splits: 0) +Lemmas : 1245718 (Deleted: 1177076) + Binary : 23249 (Ratio: 1.87%) + Ternary : 4273 (Ratio: 0.34%) + Conflict : 1245718 (Average Length: 936.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 1245718 (Average: 6.28 Max: 810 Sum: 7825992) + Executed : 1245680 (Average: 6.28 Max: 810 Sum: 7825451 Ratio: 99.99%) + Bounded : 38 (Average: 14.24 Max: 62 Sum: 541 Ratio: 0.01%) + +Rules : 55133 (Original: 53913) +Atoms : 43853 +Bodies : 10280 (Original: 9059) + Count : 232 (Original: 476) +Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) +Tight : Yes +Variables : 373951 (Eliminated: 1464 Frozen: 372487) +Constraints : 2787751 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) + +Memory Peak : 695MB +Max. Length : 85 steps +Models : 1 + +