diff --git a/gc-ta1-tt1/ipc-2011_elevator-sequential-satisficing_8.env b/gc-ta1-tt1/ipc-2011_elevator-sequential-satisficing_8.env new file mode 100644 index 000000000..7cc45ad43 --- /dev/null +++ b/gc-ta1-tt1/ipc-2011_elevator-sequential-satisficing_8.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/elevator-sequential-satisficing/domain.pddl +- /home/pluehne/Documents/ASP/pddl-instances/ipc-2011/domains/elevator-sequential-satisficing/instances/instance-8.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: elevator-sequential-satisficing + instance: 8 + 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_elevator-sequential-satisficing_8.err b/gc-ta1-tt1/ipc-2011_elevator-sequential-satisficing_8.err new file mode 100644 index 000000000..d9338b8d1 --- /dev/null +++ b/gc-ta1-tt1/ipc-2011_elevator-sequential-satisficing_8.err @@ -0,0 +1,23 @@ +# 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': 'elevator-sequential-satisficing', 'instance': 8} +# 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/elevator-sequential-satisficing/domain.pddl', '/home/pluehne/Documents/ASP/pddl-instances/ipc-2011/domains/elevator-sequential-satisficing/instances/instance-8.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 +/home/pluehne/Documents/ASP/plasp-javier/encodings/strips/strips-incremental.lp:66:15-28: info: atom does not occur in any rule head: + mutexGroup(G) + +/home/pluehne/Documents/ASP/plasp-javier/encodings/strips/strips-incremental.lp:66:30-45: info: atom does not occur in any rule head: + contains(G,X,V) + +/home/pluehne/Documents/ASP/plasp-javier/encodings/strips/strips-incremental.lp:67:15-28: info: atom does not occur in any rule head: + mutexGroup(G) + +/home/pluehne/Documents/ASP/plasp-javier/encodings/strips/strips-incremental.lp:74:41-56: info: atom does not occur in any rule head: + contains(G,X,V) + +/home/pluehne/Documents/ASP/plasp-javier/encodings/strips/strips-incremental.lp:84:41-56: info: atom does not occur in any rule head: + contains(G,X,V) + +TIMEOUT CPU 900.03 MEM 1728372 MAXMEM 1777496 STALE 1 MAXMEM_RSS 1682260 + + diff --git a/gc-ta1-tt1/ipc-2011_elevator-sequential-satisficing_8.out b/gc-ta1-tt1/ipc-2011_elevator-sequential-satisficing_8.out new file mode 100644 index 000000000..147e230b2 --- /dev/null +++ b/gc-ta1-tt1/ipc-2011_elevator-sequential-satisficing_8.out @@ -0,0 +1,1445 @@ +INFO Running translator. +INFO translator input: ['/home/pluehne/Documents/ASP/pddl-instances/ipc-2011/domains/elevator-sequential-satisficing/domain.pddl', '/home/pluehne/Documents/ASP/pddl-instances/ipc-2011/domains/elevator-sequential-satisficing/instances/instance-8.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/elevator-sequential-satisficing/domain.pddl /home/pluehne/Documents/ASP/pddl-instances/ipc-2011/domains/elevator-sequential-satisficing/instances/instance-8.pddl +Parsing... +Parsing: [0.080s CPU, 0.071s wall-clock] +Normalizing task... [0.000s CPU, 0.003s wall-clock] +Instantiating... +Generating Datalog program... [0.020s CPU, 0.018s wall-clock] +Normalizing Datalog program... +Normalizing Datalog program: [0.020s CPU, 0.027s wall-clock] +Preparing model... [0.050s CPU, 0.053s wall-clock] +Generated 46 rules. +Computing model... [1.650s CPU, 1.653s wall-clock] +14616 relevant atoms +6960 auxiliary atoms +21576 final queue length +46203 total queue pushes +Completing instantiation... [4.780s CPU, 4.771s wall-clock] +Instantiating: [6.540s CPU, 6.542s wall-clock] +Computing fact groups... +Finding invariants... +12 initial candidates +Finding invariants: [0.080s CPU, 0.082s wall-clock] +Checking invariant weight... [0.010s CPU, 0.004s wall-clock] +Instantiating groups... [0.060s CPU, 0.064s wall-clock] +Collecting mutex groups... [0.010s CPU, 0.007s wall-clock] +Choosing groups... +0 uncovered facts +Choosing groups: [0.020s CPU, 0.020s wall-clock] +Building translation key... [0.010s CPU, 0.012s wall-clock] +Computing fact groups: [0.240s CPU, 0.241s wall-clock] +Building STRIPS to SAS dictionary... [0.010s CPU, 0.006s wall-clock] +Building dictionary for full mutex groups... [0.000s CPU, 0.008s wall-clock] +Building mutex information... +Building mutex information: [0.010s CPU, 0.006s wall-clock] +Translating task... +Processing axioms... +Simplifying axioms... [0.000s CPU, 0.000s wall-clock] +Processing axioms: [0.220s CPU, 0.216s wall-clock] +Translating task: [4.170s CPU, 4.163s wall-clock] +0 effect conditions simplified +0 implied preconditions added +Detecting unreachable propositions... +0 operators removed +0 axioms removed +43 propositions removed +Detecting unreachable propositions: [2.110s CPU, 2.103s wall-clock] +Reordering and filtering variables... +43 of 43 variables necessary. +0 of 43 mutex groups necessary. +12972 of 12972 operators necessary. +0 of 0 axiom rules necessary. +Reordering and filtering variables: [0.610s CPU, 0.613s wall-clock] +Translator variables: 43 +Translator derived variables: 0 +Translator facts: 1060 +Translator goal facts: 33 +Translator mutex groups: 0 +Translator total mutex groups size: 0 +Translator operators: 12972 +Translator axioms: 0 +Translator task size: 78068 +Translator peak memory: 86988 KB +Writing output... [1.370s CPU, 1.475s wall-clock] +Done! [15.310s CPU, 15.407s wall-clock] +planner.py version 0.0.1 + +Time: 3.25s +Memory: 265MB + +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 : 3.737s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s) +CPU Time : 3.272s + +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 : 235886 +Atoms : 235886 +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 : 401MB +Max. Length : 0 steps +Models : 0 + +[endof: stats after solve call] +Solving Time: 0.02s +Memory: 337MB (+72MB) +UNSAT +Iteration Time: 0.02s + +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: 337MB +Grounding... [('step', [1]), ('step', [2]), ('step', [3]), ('step', [4]), ('step', [5]), ('check', [5])] +Grounding Time: 1.06s +Memory: 337MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0 +Calls : 2 +Time : 5.605s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s) +CPU Time : 5.140s + +Choices : 0 +Conflicts : 0 (Analyzed: 0) +Restarts : 0 +Problems : 2 (Average Length: 4.50 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 : 235886 +Atoms : 235886 +Bodies : 1 (Original: 0) +Tight : Yes +Variables : 61661 (Eliminated: 0 Frozen: 4221) +Constraints : 107675 (Binary: 96.8% Ternary: 1.5% Other: 1.7%) + +Memory Peak : 401MB +Max. Length : 0 steps +Models : 0 + +[endof: stats after solve call] +Solving Time: 0.19s +Memory: 350MB (+13MB) +UNSAT +Iteration Time: 1.87s + +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: 363.0MB +Grounding... [('step', [6]), ('step', [7]), ('step', [8]), ('step', [9]), ('step', [10]), ('check', [10])] +Grounding Time: 1.22s +Memory: 360MB (+10MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 3 +Time : 10.293s (Solving: 2.82s 1st Model: 0.00s Unsat: 0.00s) +CPU Time : 9.832s + +Choices : 87257 (Domain: 87257) +Conflicts : 10326 (Analyzed: 10326) +Restarts : 100 (Average: 103.26 Last: 103) +Problems : 3 (Average Length: 7.00 Splits: 0) +Lemmas : 10326 (Deleted: 6063) + Binary : 247 (Ratio: 2.39%) + Ternary : 121 (Ratio: 1.17%) + Conflict : 10326 (Average Length: 441.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 10326 (Average: 7.91 Max: 398 Sum: 81642) + Executed : 10325 (Average: 7.91 Max: 398 Sum: 81641 Ratio: 100.00%) + Bounded : 1 (Average: 1.00 Max: 1 Sum: 1 Ratio: 0.00%) + +Rules : 235886 +Atoms : 235886 +Bodies : 1 (Original: 0) +Tight : Yes +Variables : 134789 (Eliminated: 0 Frozen: 9342) +Constraints : 666499 (Binary: 97.9% Ternary: 1.0% Other: 1.1%) + +Memory Peak : 401MB +Max. Length : 5 steps +Models : 0 + +[endof: stats after solve call] +Solving Time: 2.89s +Memory: 399MB (+39MB) +UNKNOWN +Iteration Time: 4.70s + +Iteration 4 +Queue: [(3,15,0,True), (4,20,0,True), (5,25,0,True), (6,30,0,True)] +Grounded Until: 10 +Expected Memory: 448.0MB +Grounding... [('step', [11]), ('step', [12]), ('step', [13]), ('step', [14]), ('step', [15]), ('check', [15])] +Grounding Time: 1.08s +Memory: 419MB (+20MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 4 +Time : 16.571s (Solving: 7.35s 1st Model: 0.00s Unsat: 0.00s) +CPU Time : 16.116s + +Choices : 245213 (Domain: 245213) +Conflicts : 20914 (Analyzed: 20914) +Restarts : 200 (Average: 104.57 Last: 103) +Problems : 4 (Average Length: 9.50 Splits: 0) +Lemmas : 20914 (Deleted: 15675) + Binary : 384 (Ratio: 1.84%) + Ternary : 223 (Ratio: 1.07%) + Conflict : 20914 (Average Length: 534.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 20914 (Average: 10.37 Max: 592 Sum: 216806) + Executed : 20909 (Average: 10.37 Max: 592 Sum: 216801 Ratio: 100.00%) + Bounded : 5 (Average: 1.00 Max: 1 Sum: 5 Ratio: 0.00%) + +Rules : 235886 +Atoms : 235886 +Bodies : 1 (Original: 0) +Tight : Yes +Variables : 210475 (Eliminated: 0 Frozen: 14567) +Constraints : 1255414 (Binary: 98.0% Ternary: 1.0% Other: 1.1%) + +Memory Peak : 468MB +Max. Length : 10 steps +Models : 0 + +[endof: stats after solve call] +Solving Time: 4.60s +Memory: 468MB (+49MB) +UNKNOWN +Iteration Time: 6.29s + +Iteration 5 +Queue: [(4,20,0,True), (5,25,0,True), (6,30,0,True)] +Grounded Until: 15 +Expected Memory: 537.0MB +Grounding... [('step', [16]), ('step', [17]), ('step', [18]), ('step', [19]), ('step', [20]), ('check', [20])] +Grounding Time: 1.10s +Memory: 491MB (+23MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 5 +Time : 25.394s (Solving: 14.37s 1st Model: 0.00s Unsat: 0.00s) +CPU Time : 24.944s + +Choices : 592270 (Domain: 592270) +Conflicts : 32290 (Analyzed: 32290) +Restarts : 300 (Average: 107.63 Last: 103) +Problems : 5 (Average Length: 12.00 Splits: 0) +Lemmas : 32290 (Deleted: 26257) + Binary : 482 (Ratio: 1.49%) + Ternary : 328 (Ratio: 1.02%) + Conflict : 32290 (Average Length: 563.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 32290 (Average: 15.53 Max: 1990 Sum: 501341) + Executed : 32278 (Average: 15.53 Max: 1990 Sum: 501329 Ratio: 100.00%) + Bounded : 12 (Average: 1.00 Max: 1 Sum: 12 Ratio: 0.00%) + +Rules : 235886 +Atoms : 235886 +Bodies : 1 (Original: 0) +Tight : Yes +Variables : 286161 (Eliminated: 0 Frozen: 19792) +Constraints : 1844329 (Binary: 98.0% Ternary: 0.9% Other: 1.0%) + +Memory Peak : 540MB +Max. Length : 15 steps +Models : 0 + +[endof: stats after solve call] +Solving Time: 7.11s +Memory: 516MB (+25MB) +UNKNOWN +Iteration Time: 8.84s + +Iteration 6 +Queue: [(5,25,0,True), (6,30,0,True)] +Grounded Until: 20 +Expected Memory: 585.0MB +Grounding... [('step', [21]), ('step', [22]), ('step', [23]), ('step', [24]), ('step', [25]), ('check', [25])] +Grounding Time: 1.15s +Memory: 552MB (+36MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 1+ +Calls : 6 +Time : 38.156s (Solving: 25.23s 1st Model: 10.83s Unsat: 0.00s) +CPU Time : 37.712s + +Choices : 1170975 (Domain: 1170939) +Conflicts : 42440 (Analyzed: 42440) +Restarts : 392 (Average: 108.27 Last: 103) +Model-Level : 2556.0 +Problems : 6 (Average Length: 14.50 Splits: 0) +Lemmas : 42440 (Deleted: 33910) + Binary : 593 (Ratio: 1.40%) + Ternary : 401 (Ratio: 0.94%) + Conflict : 42440 (Average Length: 612.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 42440 (Average: 23.30 Max: 2539 Sum: 988953) + Executed : 42416 (Average: 23.30 Max: 2539 Sum: 988929 Ratio: 100.00%) + Bounded : 24 (Average: 1.00 Max: 1 Sum: 24 Ratio: 0.00%) + +Rules : 235886 +Atoms : 235886 +Bodies : 1 (Original: 0) +Tight : Yes +Variables : 361847 (Eliminated: 0 Frozen: 25017) +Constraints : 2433244 (Binary: 98.1% Ternary: 0.9% Other: 1.0%) + +Memory Peak : 609MB +Max. Length : 20 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 10.97s +Memory: 607MB (+55MB) +SAT +Testing... +NOT SERIALIZABLE +Testing Time: 5.39s +Memory: 733MB (+126MB) +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 7 +Time : 81.864s (Solving: 65.77s 1st Model: 10.83s Unsat: 0.00s) +CPU Time : 81.436s + +Choices : 3093068 (Domain: 3093032) +Conflicts : 52384 (Analyzed: 52384) +Restarts : 492 (Average: 106.47 Last: 120) +Model-Level : 2556.0 +Problems : 7 (Average Length: 16.29 Splits: 0) +Lemmas : 52384 (Deleted: 42816) + Binary : 675 (Ratio: 1.29%) + Ternary : 491 (Ratio: 0.94%) + Conflict : 52384 (Average Length: 652.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 52384 (Average: 54.19 Max: 2907 Sum: 2838701) + Executed : 52338 (Average: 54.18 Max: 2907 Sum: 2838083 Ratio: 99.98%) + Bounded : 46 (Average: 13.43 Max: 27 Sum: 618 Ratio: 0.02%) + +Rules : 1053757 (Original: 1053711) +Atoms : 263807 +Bodies : 531222 (Original: 531175) + Count : 1005 (Original: 1013) +Equivalences : 269260 (Atom=Atom: 36 Body=Body: 0 Other: 269224) +Tight : Yes +Variables : 363963 (Eliminated: 0 Frozen: 294147) +Constraints : 3226526 (Binary: 98.5% Ternary: 0.7% Other: 0.8%) + +Memory Peak : 733MB +Max. Length : 20 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 41.14s +Memory: 689MB (+-44MB) +UNKNOWN +Iteration Time: 59.31s + +Iteration 7 +Queue: [(6,30,0,True)] +Grounded Until: 25 +Expected Memory: 780.0MB +Grounding... [('step', [26]), ('step', [27]), ('step', [28]), ('step', [29]), ('step', [30]), ('check', [30])] +Grounding Time: 2.22s +Memory: 739MB (+50MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 8 +Time : 98.640s (Solving: 79.43s 1st Model: 10.83s Unsat: 0.00s) +CPU Time : 98.220s + +Choices : 3576018 (Domain: 3575982) +Conflicts : 61498 (Analyzed: 61498) +Restarts : 592 (Average: 103.88 Last: 120) +Model-Level : 2556.0 +Problems : 8 (Average Length: 18.25 Splits: 0) +Lemmas : 61498 (Deleted: 52468) + Binary : 829 (Ratio: 1.35%) + Ternary : 530 (Ratio: 0.86%) + Conflict : 61498 (Average Length: 818.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 61498 (Average: 52.23 Max: 2907 Sum: 3212060) + Executed : 61374 (Average: 52.18 Max: 2907 Sum: 3208946 Ratio: 99.90%) + Bounded : 124 (Average: 25.11 Max: 32 Sum: 3114 Ratio: 0.10%) + +Rules : 1053757 (Original: 1053711) +Atoms : 263807 +Bodies : 531222 (Original: 531175) + Count : 1005 (Original: 1013) +Equivalences : 269260 (Atom=Atom: 36 Body=Body: 0 Other: 269224) +Tight : Yes +Variables : 440079 (Eliminated: 0 Frozen: 364447) +Constraints : 4003977 (Binary: 98.5% Ternary: 0.7% Other: 0.8%) + +Memory Peak : 814MB +Max. Length : 25 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 13.78s +Memory: 814MB (+75MB) +UNKNOWN +Iteration Time: 16.79s + +Iteration 8 +Queue: [(2,10,1,True), (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)] +Grounded Until: 30 +Blocking actions... +Solving... +[start: stats after solve call] + +Models : 0 +Calls : 9 +Time : 105.528s (Solving: 86.19s 1st Model: 10.83s Unsat: 6.75s) +CPU Time : 105.112s + +Choices : 3797973 (Domain: 3797937) +Conflicts : 69553 (Analyzed: 69552) +Restarts : 676 (Average: 102.89 Last: 120) +Model-Level : 2556.0 +Problems : 9 (Average Length: 19.78 Splits: 0) +Lemmas : 69552 (Deleted: 58923) + Binary : 994 (Ratio: 1.43%) + Ternary : 705 (Ratio: 1.01%) + Conflict : 69552 (Average Length: 754.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 69552 (Average: 49.35 Max: 2907 Sum: 3432364) + Executed : 69357 (Average: 49.27 Max: 2907 Sum: 3427133 Ratio: 99.85%) + Bounded : 195 (Average: 26.83 Max: 32 Sum: 5231 Ratio: 0.15%) + +Rules : 1053757 (Original: 1053711) +Atoms : 263807 +Bodies : 531222 (Original: 531175) + Count : 1005 (Original: 1013) +Equivalences : 269260 (Atom=Atom: 36 Body=Body: 0 Other: 269224) +Tight : Yes +Variables : 440079 (Eliminated: 0 Frozen: 364447) +Constraints : 3951492 (Binary: 98.5% Ternary: 0.7% Other: 0.8%) + +Memory Peak : 814MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.83s +Memory: 814MB (+0MB) +UNSAT +Iteration Time: 6.89s + +Iteration 9 +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)] +Grounded Until: 30 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 10 +Time : 122.837s (Solving: 103.39s 1st Model: 10.83s Unsat: 6.75s) +CPU Time : 122.432s + +Choices : 4311252 (Domain: 4311216) +Conflicts : 79696 (Analyzed: 79695) +Restarts : 776 (Average: 102.70 Last: 170) +Model-Level : 2556.0 +Problems : 10 (Average Length: 21.00 Splits: 0) +Lemmas : 79695 (Deleted: 67031) + Binary : 1106 (Ratio: 1.39%) + Ternary : 820 (Ratio: 1.03%) + Conflict : 79695 (Average Length: 707.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 79695 (Average: 49.38 Max: 2907 Sum: 3935461) + Executed : 79460 (Average: 49.30 Max: 2907 Sum: 3928950 Ratio: 99.83%) + Bounded : 235 (Average: 27.71 Max: 32 Sum: 6511 Ratio: 0.17%) + +Rules : 1053757 (Original: 1053711) +Atoms : 263807 +Bodies : 531222 (Original: 531175) + Count : 1005 (Original: 1013) +Equivalences : 269260 (Atom=Atom: 36 Body=Body: 0 Other: 269224) +Tight : Yes +Variables : 440079 (Eliminated: 0 Frozen: 364447) +Constraints : 3934565 (Binary: 98.5% Ternary: 0.7% Other: 0.8%) + +Memory Peak : 814MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 17.28s +Memory: 814MB (+0MB) +UNKNOWN +Iteration Time: 17.32s + +Iteration 10 +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)] +Grounded Until: 30 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 11 +Time : 148.524s (Solving: 128.95s 1st Model: 10.83s Unsat: 6.75s) +CPU Time : 148.128s + +Choices : 5132459 (Domain: 5132423) +Conflicts : 90667 (Analyzed: 90666) +Restarts : 876 (Average: 103.50 Last: 170) +Model-Level : 2556.0 +Problems : 11 (Average Length: 22.00 Splits: 0) +Lemmas : 90666 (Deleted: 75818) + Binary : 1186 (Ratio: 1.31%) + Ternary : 921 (Ratio: 1.02%) + Conflict : 90666 (Average Length: 731.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 90666 (Average: 52.06 Max: 2907 Sum: 4720078) + Executed : 90419 (Average: 51.98 Max: 2907 Sum: 4713183 Ratio: 99.85%) + Bounded : 247 (Average: 27.91 Max: 32 Sum: 6895 Ratio: 0.15%) + +Rules : 1053757 (Original: 1053711) +Atoms : 263807 +Bodies : 531222 (Original: 531175) + Count : 1005 (Original: 1013) +Equivalences : 269260 (Atom=Atom: 36 Body=Body: 0 Other: 269224) +Tight : Yes +Variables : 440079 (Eliminated: 0 Frozen: 364447) +Constraints : 3916842 (Binary: 98.5% Ternary: 0.7% Other: 0.8%) + +Memory Peak : 814MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 25.64s +Memory: 814MB (+0MB) +UNKNOWN +Iteration Time: 25.70s + +Iteration 11 +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)] +Grounded Until: 30 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 12 +Time : 178.423s (Solving: 158.72s 1st Model: 10.83s Unsat: 6.75s) +CPU Time : 178.040s + +Choices : 6391806 (Domain: 6391770) +Conflicts : 100683 (Analyzed: 100682) +Restarts : 976 (Average: 103.16 Last: 170) +Model-Level : 2556.0 +Problems : 12 (Average Length: 22.83 Splits: 0) +Lemmas : 100682 (Deleted: 86447) + Binary : 1245 (Ratio: 1.24%) + Ternary : 992 (Ratio: 0.99%) + Conflict : 100682 (Average Length: 752.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 100682 (Average: 58.62 Max: 2907 Sum: 5902110) + Executed : 100422 (Average: 58.55 Max: 2907 Sum: 5894799 Ratio: 99.88%) + Bounded : 260 (Average: 28.12 Max: 32 Sum: 7311 Ratio: 0.12%) + +Rules : 1053757 (Original: 1053711) +Atoms : 263807 +Bodies : 531222 (Original: 531175) + Count : 1005 (Original: 1013) +Equivalences : 269260 (Atom=Atom: 36 Body=Body: 0 Other: 269224) +Tight : Yes +Variables : 440079 (Eliminated: 0 Frozen: 364447) +Constraints : 3915564 (Binary: 98.5% Ternary: 0.7% Other: 0.8%) + +Memory Peak : 814MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 29.86s +Memory: 814MB (+0MB) +UNKNOWN +Iteration Time: 29.91s + +Iteration 12 +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)] +Grounded Until: 30 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 13 +Time : 221.900s (Solving: 202.09s 1st Model: 10.83s Unsat: 6.75s) +CPU Time : 221.536s + +Choices : 7541638 (Domain: 7541602) +Conflicts : 110564 (Analyzed: 110563) +Restarts : 1076 (Average: 102.75 Last: 170) +Model-Level : 2556.0 +Problems : 13 (Average Length: 23.54 Splits: 0) +Lemmas : 110563 (Deleted: 95505) + Binary : 1339 (Ratio: 1.21%) + Ternary : 1058 (Ratio: 0.96%) + Conflict : 110563 (Average Length: 787.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 110563 (Average: 63.42 Max: 5071 Sum: 7011410) + Executed : 110299 (Average: 63.35 Max: 5071 Sum: 7003971 Ratio: 99.89%) + Bounded : 264 (Average: 28.18 Max: 32 Sum: 7439 Ratio: 0.11%) + +Rules : 1053757 (Original: 1053711) +Atoms : 263807 +Bodies : 531222 (Original: 531175) + Count : 1005 (Original: 1013) +Equivalences : 269260 (Atom=Atom: 36 Body=Body: 0 Other: 269224) +Tight : Yes +Variables : 440079 (Eliminated: 0 Frozen: 364447) +Constraints : 3915130 (Binary: 98.5% Ternary: 0.7% Other: 0.8%) + +Memory Peak : 942MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 43.46s +Memory: 878MB (+64MB) +UNKNOWN +Iteration Time: 43.50s + +Iteration 13 +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)] +Grounded Until: 30 +Expected Memory: 1003.0MB +Grounding... [('step', [31]), ('step', [32]), ('step', [33]), ('step', [34]), ('step', [35]), ('check', [35])] +Grounding Time: 1.91s +Memory: 878MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 14 +Time : 255.212s (Solving: 232.53s 1st Model: 10.83s Unsat: 6.75s) +CPU Time : 254.860s + +Choices : 8295022 (Domain: 8294986) +Conflicts : 120707 (Analyzed: 120706) +Restarts : 1176 (Average: 102.64 Last: 170) +Model-Level : 2556.0 +Problems : 14 (Average Length: 24.50 Splits: 0) +Lemmas : 120706 (Deleted: 106370) + Binary : 1374 (Ratio: 1.14%) + Ternary : 1095 (Ratio: 0.91%) + Conflict : 120706 (Average Length: 899.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 120706 (Average: 63.85 Max: 5071 Sum: 7706744) + Executed : 120413 (Average: 63.78 Max: 5071 Sum: 7698232 Ratio: 99.89%) + Bounded : 293 (Average: 29.05 Max: 37 Sum: 8512 Ratio: 0.11%) + +Rules : 1053757 (Original: 1053711) +Atoms : 263807 +Bodies : 531222 (Original: 531175) + Count : 1005 (Original: 1013) +Equivalences : 269260 (Atom=Atom: 36 Body=Body: 0 Other: 269224) +Tight : Yes +Variables : 516195 (Eliminated: 0 Frozen: 434747) +Constraints : 4696135 (Binary: 98.5% Ternary: 0.7% Other: 0.8%) + +Memory Peak : 952MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 30.58s +Memory: 945MB (+67MB) +UNKNOWN +Iteration Time: 33.34s + +Iteration 14 +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)] +Grounded Until: 35 +Expected Memory: 1070.0MB +Grounding... [('step', [36]), ('step', [37]), ('step', [38]), ('step', [39]), ('step', [40]), ('check', [40])] +Grounding Time: 1.94s +Memory: 955MB (+10MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 15 +Time : 283.097s (Solving: 257.45s 1st Model: 10.83s Unsat: 6.75s) +CPU Time : 282.756s + +Choices : 9147251 (Domain: 9147215) +Conflicts : 130961 (Analyzed: 130960) +Restarts : 1276 (Average: 102.63 Last: 170) +Model-Level : 2556.0 +Problems : 15 (Average Length: 25.67 Splits: 0) +Lemmas : 130960 (Deleted: 114360) + Binary : 1396 (Ratio: 1.07%) + Ternary : 1117 (Ratio: 0.85%) + Conflict : 130960 (Average Length: 965.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 130960 (Average: 64.60 Max: 5071 Sum: 8459482) + Executed : 130651 (Average: 64.53 Max: 5071 Sum: 8450298 Ratio: 99.89%) + Bounded : 309 (Average: 29.72 Max: 42 Sum: 9184 Ratio: 0.11%) + +Rules : 1053757 (Original: 1053711) +Atoms : 263807 +Bodies : 531222 (Original: 531175) + Count : 1005 (Original: 1013) +Equivalences : 269260 (Atom=Atom: 36 Body=Body: 0 Other: 269224) +Tight : Yes +Variables : 592311 (Eliminated: 0 Frozen: 505047) +Constraints : 5469571 (Binary: 98.5% Ternary: 0.7% Other: 0.8%) + +Memory Peak : 1057MB +Max. Length : 35 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 25.08s +Memory: 1001MB (+46MB) +UNKNOWN +Iteration Time: 27.91s + +Iteration 15 +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)] +Grounded Until: 40 +Expected Memory: 1126.0MB +Grounding... [('step', [41]), ('step', [42]), ('step', [43]), ('step', [44]), ('step', [45]), ('check', [45])] +Grounding Time: 2.00s +Memory: 1039MB (+38MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 16 +Time : 330.460s (Solving: 301.77s 1st Model: 10.83s Unsat: 6.75s) +CPU Time : 330.140s + +Choices : 10064112 (Domain: 10064076) +Conflicts : 140836 (Analyzed: 140835) +Restarts : 1376 (Average: 102.35 Last: 170) +Model-Level : 2556.0 +Problems : 16 (Average Length: 27.00 Splits: 0) +Lemmas : 140835 (Deleted: 125302) + Binary : 1410 (Ratio: 1.00%) + Ternary : 1142 (Ratio: 0.81%) + Conflict : 140835 (Average Length: 1020.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 140835 (Average: 66.03 Max: 5071 Sum: 9299247) + Executed : 140526 (Average: 65.96 Max: 5071 Sum: 9290063 Ratio: 99.90%) + Bounded : 309 (Average: 29.72 Max: 42 Sum: 9184 Ratio: 0.10%) + +Rules : 1053757 (Original: 1053711) +Atoms : 263807 +Bodies : 531222 (Original: 531175) + Count : 1005 (Original: 1013) +Equivalences : 269260 (Atom=Atom: 36 Body=Body: 0 Other: 269224) +Tight : Yes +Variables : 668427 (Eliminated: 0 Frozen: 575347) +Constraints : 6247655 (Binary: 98.5% Ternary: 0.7% Other: 0.8%) + +Memory Peak : 1144MB +Max. Length : 40 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 44.49s +Memory: 1089MB (+50MB) +UNKNOWN +Iteration Time: 47.39s + +Iteration 16 +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)] +Grounded Until: 45 +Expected Memory: 1214.0MB +Grounding... [('step', [46]), ('step', [47]), ('step', [48]), ('step', [49]), ('step', [50]), ('check', [50])] +Grounding Time: 1.97s +Memory: 1106MB (+17MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 17 +Time : 364.437s (Solving: 332.66s 1st Model: 10.83s Unsat: 6.75s) +CPU Time : 364.132s + +Choices : 10837279 (Domain: 10837243) +Conflicts : 150161 (Analyzed: 150160) +Restarts : 1476 (Average: 101.73 Last: 170) +Model-Level : 2556.0 +Problems : 17 (Average Length: 28.47 Splits: 0) +Lemmas : 150160 (Deleted: 135673) + Binary : 1429 (Ratio: 0.95%) + Ternary : 1154 (Ratio: 0.77%) + Conflict : 150160 (Average Length: 1099.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 150160 (Average: 66.44 Max: 5071 Sum: 9977237) + Executed : 149846 (Average: 66.38 Max: 5071 Sum: 9967793 Ratio: 99.91%) + Bounded : 314 (Average: 30.08 Max: 52 Sum: 9444 Ratio: 0.09%) + +Rules : 1053757 (Original: 1053711) +Atoms : 263807 +Bodies : 531222 (Original: 531175) + Count : 1005 (Original: 1013) +Equivalences : 269260 (Atom=Atom: 36 Body=Body: 0 Other: 269224) +Tight : Yes +Variables : 744543 (Eliminated: 0 Frozen: 645647) +Constraints : 7028795 (Binary: 98.5% Ternary: 0.7% Other: 0.8%) + +Memory Peak : 1220MB +Max. Length : 45 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 31.07s +Memory: 1183MB (+77MB) +UNKNOWN +Iteration Time: 34.00s + +Iteration 17 +Queue: [(11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True)] +Grounded Until: 50 +Expected Memory: 1308.0MB +Grounding... [('step', [51]), ('step', [52]), ('step', [53]), ('step', [54]), ('step', [55]), ('check', [55])] +Grounding Time: 2.00s +Memory: 1203MB (+20MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 18 +Time : 419.458s (Solving: 384.56s 1st Model: 10.83s Unsat: 6.75s) +CPU Time : 419.176s + +Choices : 12031258 (Domain: 12031222) +Conflicts : 160232 (Analyzed: 160231) +Restarts : 1576 (Average: 101.67 Last: 170) +Model-Level : 2556.0 +Problems : 18 (Average Length: 30.06 Splits: 0) +Lemmas : 160231 (Deleted: 143538) + Binary : 1466 (Ratio: 0.91%) + Ternary : 1190 (Ratio: 0.74%) + Conflict : 160231 (Average Length: 1138.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 160231 (Average: 69.21 Max: 5071 Sum: 11090301) + Executed : 159912 (Average: 69.15 Max: 5071 Sum: 11080572 Ratio: 99.91%) + Bounded : 319 (Average: 30.50 Max: 57 Sum: 9729 Ratio: 0.09%) + +Rules : 1053757 (Original: 1053711) +Atoms : 263807 +Bodies : 531222 (Original: 531175) + Count : 1005 (Original: 1013) +Equivalences : 269260 (Atom=Atom: 36 Body=Body: 0 Other: 269224) +Tight : Yes +Variables : 820659 (Eliminated: 0 Frozen: 715947) +Constraints : 7809723 (Binary: 98.5% Ternary: 0.7% Other: 0.8%) + +Memory Peak : 1327MB +Max. Length : 50 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 52.10s +Memory: 1244MB (+41MB) +UNKNOWN +Iteration Time: 55.05s + +Iteration 18 +Queue: [(12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True)] +Grounded Until: 55 +Expected Memory: 1369.0MB +Grounding... [('step', [56]), ('step', [57]), ('step', [58]), ('step', [59]), ('step', [60]), ('check', [60])] +Grounding Time: 2.65s +Memory: 1322MB (+78MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 19 +Time : 467.972s (Solving: 429.25s 1st Model: 10.83s Unsat: 6.75s) +CPU Time : 467.712s + +Choices : 13335550 (Domain: 13335514) +Conflicts : 170442 (Analyzed: 170441) +Restarts : 1676 (Average: 101.70 Last: 170) +Model-Level : 2556.0 +Problems : 19 (Average Length: 31.74 Splits: 0) +Lemmas : 170441 (Deleted: 152211) + Binary : 1483 (Ratio: 0.87%) + Ternary : 1205 (Ratio: 0.71%) + Conflict : 170441 (Average Length: 1175.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 170441 (Average: 71.74 Max: 5071 Sum: 12227141) + Executed : 170117 (Average: 71.68 Max: 5071 Sum: 12217102 Ratio: 99.92%) + Bounded : 324 (Average: 30.98 Max: 62 Sum: 10039 Ratio: 0.08%) + +Rules : 1053757 (Original: 1053711) +Atoms : 263807 +Bodies : 531222 (Original: 531175) + Count : 1005 (Original: 1013) +Equivalences : 269260 (Atom=Atom: 36 Body=Body: 0 Other: 269224) +Tight : Yes +Variables : 896775 (Eliminated: 0 Frozen: 786247) +Constraints : 8590578 (Binary: 98.5% Ternary: 0.7% Other: 0.8%) + +Memory Peak : 1471MB +Max. Length : 55 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 44.89s +Memory: 1371MB (+49MB) +UNKNOWN +Iteration Time: 48.54s + +Iteration 19 +Queue: [(13,65,0,True), (14,70,0,True), (15,75,0,True)] +Grounded Until: 60 +Expected Memory: 1498.0MB +Grounding... [('step', [61]), ('step', [62]), ('step', [63]), ('step', [64]), ('step', [65]), ('check', [65])] +Grounding Time: 1.93s +Memory: 1402MB (+31MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 20 +Time : 525.357s (Solving: 483.47s 1st Model: 10.83s Unsat: 6.75s) +CPU Time : 525.120s + +Choices : 14842556 (Domain: 14842520) +Conflicts : 180796 (Analyzed: 180795) +Restarts : 1776 (Average: 101.80 Last: 170) +Model-Level : 2556.0 +Problems : 20 (Average Length: 33.50 Splits: 0) +Lemmas : 180795 (Deleted: 162491) + Binary : 1511 (Ratio: 0.84%) + Ternary : 1225 (Ratio: 0.68%) + Conflict : 180795 (Average Length: 1241.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 180795 (Average: 75.19 Max: 5071 Sum: 13593234) + Executed : 180465 (Average: 75.13 Max: 5071 Sum: 13582793 Ratio: 99.92%) + Bounded : 330 (Average: 31.64 Max: 67 Sum: 10441 Ratio: 0.08%) + +Rules : 1053757 (Original: 1053711) +Atoms : 263807 +Bodies : 531222 (Original: 531175) + Count : 1005 (Original: 1013) +Equivalences : 269260 (Atom=Atom: 36 Body=Body: 0 Other: 269224) +Tight : Yes +Variables : 972891 (Eliminated: 0 Frozen: 856547) +Constraints : 9371646 (Binary: 98.5% Ternary: 0.7% Other: 0.8%) + +Memory Peak : 1544MB +Max. Length : 60 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 54.44s +Memory: 1443MB (+41MB) +UNKNOWN +Iteration Time: 57.42s + +Iteration 20 +Queue: [(14,70,0,True), (15,75,0,True)] +Grounded Until: 65 +Expected Memory: 1570.0MB +Grounding... [('step', [66]), ('step', [67]), ('step', [68]), ('step', [69]), ('step', [70]), ('check', [70])] +Grounding Time: 1.92s +Memory: 1468MB (+25MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 21 +Time : 571.418s (Solving: 526.33s 1st Model: 10.83s Unsat: 6.75s) +CPU Time : 571.200s + +Choices : 16032472 (Domain: 16032436) +Conflicts : 190440 (Analyzed: 190439) +Restarts : 1876 (Average: 101.51 Last: 170) +Model-Level : 2556.0 +Problems : 21 (Average Length: 35.33 Splits: 0) +Lemmas : 190439 (Deleted: 172971) + Binary : 1532 (Ratio: 0.80%) + Ternary : 1240 (Ratio: 0.65%) + Conflict : 190439 (Average Length: 1322.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 190439 (Average: 76.67 Max: 5071 Sum: 14601042) + Executed : 190109 (Average: 76.62 Max: 5071 Sum: 14590601 Ratio: 99.93%) + Bounded : 330 (Average: 31.64 Max: 67 Sum: 10441 Ratio: 0.07%) + +Rules : 1053757 (Original: 1053711) +Atoms : 263807 +Bodies : 531222 (Original: 531175) + Count : 1005 (Original: 1013) +Equivalences : 269260 (Atom=Atom: 36 Body=Body: 0 Other: 269224) +Tight : Yes +Variables : 1049007 (Eliminated: 0 Frozen: 926847) +Constraints : 10152279 (Binary: 98.5% Ternary: 0.7% Other: 0.8%) + +Memory Peak : 1631MB +Max. Length : 65 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 43.10s +Memory: 1531MB (+63MB) +UNKNOWN +Iteration Time: 46.09s + +Iteration 21 +Queue: [(15,75,0,True)] +Grounded Until: 70 +Expected Memory: 1658.0MB +Grounding... [('step', [71]), ('step', [72]), ('step', [73]), ('step', [74]), ('step', [75]), ('check', [75])] +Grounding Time: 1.93s +Memory: 1536MB (+5MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 22 +Time : 675.621s (Solving: 627.25s 1st Model: 10.83s Unsat: 6.75s) +CPU Time : 675.444s + +Choices : 17932130 (Domain: 17932094) +Conflicts : 200799 (Analyzed: 200798) +Restarts : 1976 (Average: 101.62 Last: 170) +Model-Level : 2556.0 +Problems : 22 (Average Length: 37.23 Splits: 0) +Lemmas : 200798 (Deleted: 182387) + Binary : 1541 (Ratio: 0.77%) + Ternary : 1254 (Ratio: 0.62%) + Conflict : 200798 (Average Length: 1355.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 200798 (Average: 81.66 Max: 5071 Sum: 16397963) + Executed : 200466 (Average: 81.61 Max: 5071 Sum: 16387368 Ratio: 99.94%) + Bounded : 332 (Average: 31.91 Max: 77 Sum: 10595 Ratio: 0.06%) + +Rules : 1053757 (Original: 1053711) +Atoms : 263807 +Bodies : 531222 (Original: 531175) + Count : 1005 (Original: 1013) +Equivalences : 269260 (Atom=Atom: 36 Body=Body: 0 Other: 269224) +Tight : Yes +Variables : 1125123 (Eliminated: 0 Frozen: 997147) +Constraints : 10933419 (Binary: 98.5% Ternary: 0.7% Other: 0.8%) + +Memory Peak : 1698MB +Max. Length : 70 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 101.19s +Memory: 1639MB (+103MB) +UNKNOWN +Iteration Time: 104.25s + +Iteration 22 +Queue: [(3,15,2,True), (4,20,2,True), (5,25,2,True), (6,30,2,True), (7,35,1,True), (8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,0,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True)] +Grounded Until: 75 +Blocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 23 +Time : 687.310s (Solving: 638.66s 1st Model: 10.83s Unsat: 6.75s) +CPU Time : 687.140s + +Choices : 17975585 (Domain: 17975549) +Conflicts : 210000 (Analyzed: 209999) +Restarts : 2076 (Average: 101.16 Last: 170) +Model-Level : 2556.0 +Problems : 23 (Average Length: 38.96 Splits: 0) +Lemmas : 209999 (Deleted: 192770) + Binary : 1573 (Ratio: 0.75%) + Ternary : 1290 (Ratio: 0.61%) + Conflict : 209999 (Average Length: 1363.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 209999 (Average: 78.25 Max: 5071 Sum: 16431732) + Executed : 209666 (Average: 78.20 Max: 5071 Sum: 16421060 Ratio: 99.94%) + Bounded : 333 (Average: 32.05 Max: 77 Sum: 10672 Ratio: 0.06%) + +Rules : 1053757 (Original: 1053711) +Atoms : 263807 +Bodies : 531222 (Original: 531175) + Count : 1005 (Original: 1013) +Equivalences : 269260 (Atom=Atom: 36 Body=Body: 0 Other: 269224) +Tight : Yes +Variables : 1125123 (Eliminated: 0 Frozen: 997147) +Constraints : 10933395 (Binary: 98.5% Ternary: 0.7% Other: 0.8%) + +Memory Peak : 1698MB +Max. Length : 75 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 11.60s +Memory: 1650MB (+11MB) +UNKNOWN +Iteration Time: 11.70s + +Iteration 23 +Queue: [(4,20,2,True), (5,25,2,True), (6,30,2,True), (7,35,1,True), (8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,0,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True)] +Grounded Until: 75 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 24 +Time : 707.066s (Solving: 658.13s 1st Model: 10.83s Unsat: 6.75s) +CPU Time : 706.904s + +Choices : 18183796 (Domain: 18183760) +Conflicts : 220591 (Analyzed: 220590) +Restarts : 2176 (Average: 101.37 Last: 170) +Model-Level : 2556.0 +Problems : 24 (Average Length: 40.54 Splits: 0) +Lemmas : 220590 (Deleted: 201593) + Binary : 1611 (Ratio: 0.73%) + Ternary : 1330 (Ratio: 0.60%) + Conflict : 220590 (Average Length: 1423.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 220590 (Average: 75.32 Max: 5071 Sum: 16614543) + Executed : 220256 (Average: 75.27 Max: 5071 Sum: 16603794 Ratio: 99.94%) + Bounded : 334 (Average: 32.18 Max: 77 Sum: 10749 Ratio: 0.06%) + +Rules : 1053757 (Original: 1053711) +Atoms : 263807 +Bodies : 531222 (Original: 531175) + Count : 1005 (Original: 1013) +Equivalences : 269260 (Atom=Atom: 36 Body=Body: 0 Other: 269224) +Tight : Yes +Variables : 1125123 (Eliminated: 0 Frozen: 997147) +Constraints : 10933383 (Binary: 98.5% Ternary: 0.7% Other: 0.8%) + +Memory Peak : 1698MB +Max. Length : 75 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 19.66s +Memory: 1650MB (+0MB) +UNKNOWN +Iteration Time: 19.77s + +Iteration 24 +Queue: [(5,25,2,True), (6,30,2,True), (7,35,1,True), (8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,0,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True)] +Grounded Until: 75 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 25 +Time : 734.565s (Solving: 685.31s 1st Model: 10.83s Unsat: 6.75s) +CPU Time : 734.416s + +Choices : 18936641 (Domain: 18936605) +Conflicts : 231055 (Analyzed: 231054) +Restarts : 2276 (Average: 101.52 Last: 170) +Model-Level : 2556.0 +Problems : 25 (Average Length: 42.00 Splits: 0) +Lemmas : 231054 (Deleted: 209391) + Binary : 1664 (Ratio: 0.72%) + Ternary : 1378 (Ratio: 0.60%) + Conflict : 231054 (Average Length: 1402.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 231054 (Average: 74.93 Max: 5071 Sum: 17313587) + Executed : 230713 (Average: 74.88 Max: 5071 Sum: 17302299 Ratio: 99.93%) + Bounded : 341 (Average: 33.10 Max: 77 Sum: 11288 Ratio: 0.07%) + +Rules : 1053757 (Original: 1053711) +Atoms : 263807 +Bodies : 531222 (Original: 531175) + Count : 1005 (Original: 1013) +Equivalences : 269260 (Atom=Atom: 36 Body=Body: 0 Other: 269224) +Tight : Yes +Variables : 1125123 (Eliminated: 0 Frozen: 997147) +Constraints : 10933371 (Binary: 98.5% Ternary: 0.7% Other: 0.8%) + +Memory Peak : 1698MB +Max. Length : 75 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 27.38s +Memory: 1650MB (+0MB) +UNKNOWN +Iteration Time: 27.51s + +Iteration 25 +Queue: [(6,30,2,True), (7,35,1,True), (8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,0,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True)] +Grounded Until: 75 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 26 +Time : 773.802s (Solving: 724.25s 1st Model: 10.83s Unsat: 6.75s) +CPU Time : 773.668s + +Choices : 19923804 (Domain: 19923768) +Conflicts : 241680 (Analyzed: 241679) +Restarts : 2376 (Average: 101.72 Last: 170) +Model-Level : 2556.0 +Problems : 26 (Average Length: 43.35 Splits: 0) +Lemmas : 241679 (Deleted: 219076) + Binary : 1785 (Ratio: 0.74%) + Ternary : 1441 (Ratio: 0.60%) + Conflict : 241679 (Average Length: 1392.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 241679 (Average: 75.49 Max: 5071 Sum: 18243708) + Executed : 241326 (Average: 75.44 Max: 5071 Sum: 18231496 Ratio: 99.93%) + Bounded : 353 (Average: 34.59 Max: 77 Sum: 12212 Ratio: 0.07%) + +Rules : 1053757 (Original: 1053711) +Atoms : 263807 +Bodies : 531222 (Original: 531175) + Count : 1005 (Original: 1013) +Equivalences : 269260 (Atom=Atom: 36 Body=Body: 0 Other: 269224) +Tight : Yes +Variables : 1125123 (Eliminated: 0 Frozen: 997147) +Constraints : 10933289 (Binary: 98.5% Ternary: 0.7% Other: 0.8%) + +Memory Peak : 1698MB +Max. Length : 75 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 39.14s +Memory: 1650MB (+0MB) +UNKNOWN +Iteration Time: 39.26s + +Iteration 26 +Queue: [(7,35,1,True), (8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,0,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True)] +Grounded Until: 75 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 27 +Time : 810.279s (Solving: 760.41s 1st Model: 10.83s Unsat: 6.75s) +CPU Time : 810.164s + +Choices : 20816028 (Domain: 20815992) +Conflicts : 251696 (Analyzed: 251695) +Restarts : 2476 (Average: 101.65 Last: 170) +Model-Level : 2556.0 +Problems : 27 (Average Length: 44.59 Splits: 0) +Lemmas : 251695 (Deleted: 228996) + Binary : 1832 (Ratio: 0.73%) + Ternary : 1472 (Ratio: 0.58%) + Conflict : 251695 (Average Length: 1408.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 251695 (Average: 75.75 Max: 5071 Sum: 19066434) + Executed : 251341 (Average: 75.70 Max: 5071 Sum: 19054145 Ratio: 99.94%) + Bounded : 354 (Average: 34.71 Max: 77 Sum: 12289 Ratio: 0.06%) + +Rules : 1053757 (Original: 1053711) +Atoms : 263807 +Bodies : 531222 (Original: 531175) + Count : 1005 (Original: 1013) +Equivalences : 269260 (Atom=Atom: 36 Body=Body: 0 Other: 269224) +Tight : Yes +Variables : 1125123 (Eliminated: 0 Frozen: 997147) +Constraints : 10932334 (Binary: 98.5% Ternary: 0.7% Other: 0.8%) + +Memory Peak : 1698MB +Max. Length : 75 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 36.36s +Memory: 1650MB (+0MB) +UNKNOWN +Iteration Time: 36.50s + +Iteration 27 +Queue: [(8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,0,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True)] +Grounded Until: 75 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 28 +Time : 868.732s (Solving: 818.56s 1st Model: 10.83s Unsat: 6.75s) +CPU Time : 868.644s + +Choices : 21903744 (Domain: 21903708) +Conflicts : 261870 (Analyzed: 261869) +Restarts : 2576 (Average: 101.66 Last: 170) +Model-Level : 2556.0 +Problems : 28 (Average Length: 45.75 Splits: 0) +Lemmas : 261869 (Deleted: 238219) + Binary : 1883 (Ratio: 0.72%) + Ternary : 1494 (Ratio: 0.57%) + Conflict : 261869 (Average Length: 1409.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 261869 (Average: 76.70 Max: 5071 Sum: 20085513) + Executed : 261512 (Average: 76.65 Max: 5071 Sum: 20072993 Ratio: 99.94%) + Bounded : 357 (Average: 35.07 Max: 77 Sum: 12520 Ratio: 0.06%) + +Rules : 1053757 (Original: 1053711) +Atoms : 263807 +Bodies : 531222 (Original: 531175) + Count : 1005 (Original: 1013) +Equivalences : 269260 (Atom=Atom: 36 Body=Body: 0 Other: 269224) +Tight : Yes +Variables : 1125123 (Eliminated: 0 Frozen: 997147) +Constraints : 10932284 (Binary: 98.5% Ternary: 0.7% Other: 0.8%) + +Memory Peak : 1698MB +Max. Length : 75 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 58.36s +Memory: 1650MB (+0MB) +UNKNOWN +Iteration Time: 58.48s + +Iteration 28 +Queue: [(9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,0,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True)] +Grounded Until: 75 +Unblocking actions... +Solving... +*** Info : (planner): INTERRUPTED by signal! +UNKNOWN + +INTERRUPTED : 1 + +Models : 0+ +Calls : 29 +Time : 879.617s (Solving: 829.17s 1st Model: 10.83s Unsat: 6.75s) +CPU Time : 879.516s + +Choices : 22144188 (Domain: 22144152) +Conflicts : 263533 (Analyzed: 263532) +Restarts : 2590 (Average: 101.75 Last: 170) +Model-Level : 2556.0 +Problems : 29 (Average Length: 46.83 Splits: 0) +Lemmas : 263532 (Deleted: 238219) + Binary : 1902 (Ratio: 0.72%) + Ternary : 1504 (Ratio: 0.57%) + Conflict : 263532 (Average Length: 1404.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 263532 (Average: 77.10 Max: 5071 Sum: 20317886) + Executed : 263174 (Average: 77.05 Max: 5071 Sum: 20305289 Ratio: 99.94%) + Bounded : 358 (Average: 35.19 Max: 77 Sum: 12597 Ratio: 0.06%) + +Rules : 1053757 (Original: 1053711) +Atoms : 263807 +Bodies : 531222 (Original: 531175) + Count : 1005 (Original: 1013) +Equivalences : 269260 (Atom=Atom: 36 Body=Body: 0 Other: 269224) +Tight : Yes +Variables : 1125123 (Eliminated: 0 Frozen: 997147) +Constraints : 10932250 (Binary: 98.5% Ternary: 0.7% Other: 0.8%) + +Memory Peak : 1698MB +Max. Length : 75 steps +Models : 1 + +