diff --git a/gc-ta1-tt1-jumpy/ipc-2011_barman-sequential-satisficing_3.env b/gc-ta1-tt1-jumpy/ipc-2011_barman-sequential-satisficing_3.env new file mode 100644 index 000000000..0cc96dad8 --- /dev/null +++ b/gc-ta1-tt1-jumpy/ipc-2011_barman-sequential-satisficing_3.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-3.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=jumpy +- -i 0 +configuration: + id: gc-ta1-tt1-jumpy + 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=jumpy + - -i 0 +exitCode: 0 +instance: + domain: barman-sequential-satisficing + instance: 3 + ipc: ipc-2011 + planLength: 100 +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-jumpy/ipc-2011_barman-sequential-satisficing_3.err b/gc-ta1-tt1-jumpy/ipc-2011_barman-sequential-satisficing_3.err new file mode 100644 index 000000000..a28080fb4 --- /dev/null +++ b/gc-ta1-tt1-jumpy/ipc-2011_barman-sequential-satisficing_3.err @@ -0,0 +1,8 @@ +# configuration: {'id': 'gc-ta1-tt1-jumpy', '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=jumpy', '-i 0'], 'instanceSets': ['rintanen-aij-2012-interesting']} +# instance: {'ipc': 'ipc-2011', 'domain': 'barman-sequential-satisficing', 'instance': 3, 'planLength': 100} +# 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-3.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=jumpy', '-i 0'] +# working directory: /home/pluehne/Documents/ASP/plasp-javier/encodings/planner +# exit code: 0 +TIMEOUT CPU 900.09 MEM 747880 MAXMEM 747880 STALE 1 MAXMEM_RSS 625500 + + diff --git a/gc-ta1-tt1-jumpy/ipc-2011_barman-sequential-satisficing_3.out b/gc-ta1-tt1-jumpy/ipc-2011_barman-sequential-satisficing_3.out new file mode 100644 index 000000000..c1c32dae6 --- /dev/null +++ b/gc-ta1-tt1-jumpy/ipc-2011_barman-sequential-satisficing_3.out @@ -0,0 +1,2628 @@ +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-3.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-3.pddl +Parsing... +Parsing: [0.040s CPU, 0.039s wall-clock] +Normalizing task... [0.000s CPU, 0.003s wall-clock] +Instantiating... +Generating Datalog program... [0.010s CPU, 0.010s wall-clock] +Normalizing Datalog program... +Normalizing Datalog program: [0.050s CPU, 0.050s wall-clock] +Preparing model... [0.030s CPU, 0.025s wall-clock] +Generated 115 rules. +Computing model... [0.320s CPU, 0.327s wall-clock] +2025 relevant atoms +2105 auxiliary atoms +4130 final queue length +7122 total queue pushes +Completing instantiation... [0.600s CPU, 0.600s wall-clock] +Instantiating: [1.010s CPU, 1.016s wall-clock] +Computing fact groups... +Finding invariants... +24 initial candidates +Finding invariants: [0.100s CPU, 0.090s wall-clock] +Checking invariant weight... [0.000s CPU, 0.001s wall-clock] +Instantiating groups... [0.000s 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.130s CPU, 0.121s 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.000s CPU, 0.002s wall-clock] +Translating task... +Processing axioms... +Simplifying axioms... [0.000s CPU, 0.000s wall-clock] +Processing axioms: [0.040s CPU, 0.033s wall-clock] +Translating task: [0.660s CPU, 0.658s 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.311s 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.240s CPU, 0.255s wall-clock] +Done! [2.620s CPU, 2.641s 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.653s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s) +CPU Time : 0.568s + +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 : 0 +Calls : 2 +Time : 0.981s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s) +CPU Time : 0.896s + +Choices : 87 (Domain: 79) +Conflicts : 41 (Analyzed: 40) +Restarts : 0 +Problems : 2 (Average Length: 4.50 Splits: 0) +Lemmas : 40 (Deleted: 0) + Binary : 5 (Ratio: 12.50%) + Ternary : 0 (Ratio: 0.00%) + Conflict : 40 (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 : 40 (Average: 2.20 Max: 11 Sum: 88) + Executed : 39 (Average: 2.17 Max: 11 Sum: 87 Ratio: 98.86%) + Bounded : 1 (Average: 1.00 Max: 1 Sum: 1 Ratio: 1.14%) + +Rules : 38518 +Atoms : 38518 +Bodies : 1 (Original: 0) +Tight : Yes +Variables : 10318 (Eliminated: 0 Frozen: 10318) +Constraints : 36429 (Binary: 95.1% Ternary: 3.5% Other: 1.5%) + +Memory Peak : 222MB +Max. Length : 0 steps +Models : 0 + +[endof: stats after solve call] +Solving Time: 0.10s +Memory: 160MB (+2MB) +UNSAT +Iteration Time: 0.33s + +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: 162.0MB +Grounding... [('step', [6]), ('step', [7]), ('step', [8]), ('step', [9]), ('step', [10]), ('check', [10])] +Grounding Time: 0.18s +Memory: 164MB (+4MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 1+ +Calls : 3 +Time : 1.409s (Solving: 0.01s 1st Model: 0.00s Unsat: 0.00s) +CPU Time : 1.324s + +Choices : 554 (Domain: 518) +Conflicts : 55 (Analyzed: 54) +Restarts : 0 +Model-Level : 212.0 +Problems : 3 (Average Length: 7.00 Splits: 0) +Lemmas : 54 (Deleted: 0) + Binary : 10 (Ratio: 18.52%) + Ternary : 2 (Ratio: 3.70%) + Conflict : 54 (Average Length: 12.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 54 (Average: 6.57 Max: 65 Sum: 355) + Executed : 53 (Average: 6.56 Max: 65 Sum: 354 Ratio: 99.72%) + Bounded : 1 (Average: 1.00 Max: 1 Sum: 1 Ratio: 0.28%) + +Rules : 38518 +Atoms : 38518 +Bodies : 1 (Original: 0) +Tight : Yes +Variables : 22604 (Eliminated: 0 Frozen: 22604) +Constraints : 136839 (Binary: 95.5% Ternary: 3.2% Other: 1.2%) + +Memory Peak : 222MB +Max. Length : 5 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 0.17s +Memory: 171MB (+7MB) +SAT +Testing... +NOT SERIALIZABLE +Testing Time: 0.65s +Memory: 191MB (+20MB) +Solving... +[start: stats after solve call] + +Models : 0 +Calls : 4 +Time : 1.943s (Solving: 0.27s 1st Model: 0.00s Unsat: 0.26s) +CPU Time : 1.856s + +Choices : 8046 (Domain: 7436) +Conflicts : 961 (Analyzed: 959) +Restarts : 6 (Average: 159.83 Last: 98) +Model-Level : 212.0 +Problems : 4 (Average Length: 8.25 Splits: 0) +Lemmas : 959 (Deleted: 0) + Binary : 286 (Ratio: 29.82%) + Ternary : 161 (Ratio: 16.79%) + Conflict : 959 (Average Length: 34.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 959 (Average: 8.24 Max: 89 Sum: 7898) + Executed : 945 (Average: 8.14 Max: 89 Sum: 7807 Ratio: 98.85%) + Bounded : 14 (Average: 6.50 Max: 12 Sum: 91 Ratio: 1.15%) + +Rules : 94613 (Original: 86518) +Atoms : 45936 +Bodies : 40692 (Original: 32596) + Count : 619 (Original: 1518) +Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) +Tight : Yes +Variables : 34632 (Eliminated: 8994 Frozen: 25638) +Constraints : 194982 (Binary: 88.9% Ternary: 7.3% Other: 3.8%) + +Memory Peak : 222MB +Max. Length : 5 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 0.39s +Memory: 188MB (+-3MB) +UNSAT +Iteration Time: 1.47s + +Iteration 4 +Queue: [(3,15,0,True), (4,20,0,True), (5,25,0,True), (6,30,0,True)] +Grounded Until: 10 +Expected Memory: 199.0MB +Grounding... [('step', [11]), ('step', [12]), ('step', [13]), ('step', [14]), ('step', [15]), ('check', [15])] +Grounding Time: 0.34s +Memory: 195MB (+7MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0 +Calls : 5 +Time : 9.858s (Solving: 7.40s 1st Model: 0.00s Unsat: 7.40s) +CPU Time : 9.776s + +Choices : 178625 (Domain: 143317) +Conflicts : 25090 (Analyzed: 25087) +Restarts : 94 (Average: 266.88 Last: 98) +Model-Level : 212.0 +Problems : 5 (Average Length: 10.00 Splits: 0) +Lemmas : 25087 (Deleted: 16452) + Binary : 1522 (Ratio: 6.07%) + Ternary : 479 (Ratio: 1.91%) + Conflict : 25087 (Average Length: 288.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 25087 (Average: 6.95 Max: 401 Sum: 174374) + Executed : 25056 (Average: 6.94 Max: 401 Sum: 174016 Ratio: 99.79%) + Bounded : 31 (Average: 11.55 Max: 17 Sum: 358 Ratio: 0.21%) + +Rules : 94613 (Original: 86518) +Atoms : 45936 +Bodies : 40692 (Original: 32596) + Count : 619 (Original: 1518) +Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) +Tight : Yes +Variables : 57193 (Eliminated: 8994 Frozen: 40669) +Constraints : 363350 (Binary: 90.3% Ternary: 6.9% Other: 2.9%) + +Memory Peak : 222MB +Max. Length : 10 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.46s +Memory: 206MB (+11MB) +UNSAT +Iteration Time: 7.93s + +Iteration 5 +Queue: [(4,20,0,True), (5,25,0,True), (6,30,0,True)] +Grounded Until: 15 +Expected Memory: 224.0MB +Grounding... [('step', [16]), ('step', [17]), ('step', [18]), ('step', [19]), ('step', [20]), ('check', [20])] +Grounding Time: 0.35s +Memory: 213MB (+7MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 6 +Time : 24.515s (Solving: 21.24s 1st Model: 0.00s Unsat: 7.40s) +CPU Time : 24.440s + +Choices : 450104 (Domain: 398284) +Conflicts : 53216 (Analyzed: 53213) +Restarts : 194 (Average: 274.29 Last: 201) +Model-Level : 212.0 +Problems : 6 (Average Length: 12.00 Splits: 0) +Lemmas : 53213 (Deleted: 38381) + Binary : 2964 (Ratio: 5.57%) + Ternary : 766 (Ratio: 1.44%) + Conflict : 53213 (Average Length: 476.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 53213 (Average: 8.17 Max: 401 Sum: 435006) + Executed : 53170 (Average: 8.16 Max: 401 Sum: 434408 Ratio: 99.86%) + Bounded : 43 (Average: 13.91 Max: 22 Sum: 598 Ratio: 0.14%) + +Rules : 94613 (Original: 86518) +Atoms : 45936 +Bodies : 40692 (Original: 32596) + Count : 619 (Original: 1518) +Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) +Tight : Yes +Variables : 79754 (Eliminated: 8994 Frozen: 63230) +Constraints : 517735 (Binary: 90.8% Ternary: 6.7% Other: 2.5%) + +Memory Peak : 225MB +Max. Length : 15 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 14.18s +Memory: 225MB (+12MB) +UNKNOWN +Iteration Time: 14.67s + +Iteration 6 +Queue: [(5,25,0,True), (6,30,0,True)] +Grounded Until: 20 +Expected Memory: 244.0MB +Grounding... [('step', [21]), ('step', [22]), ('step', [23]), ('step', [24]), ('step', [25]), ('check', [25])] +Grounding Time: 0.36s +Memory: 227MB (+2MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 7 +Time : 41.662s (Solving: 37.54s 1st Model: 0.00s Unsat: 7.40s) +CPU Time : 41.596s + +Choices : 644218 (Domain: 583497) +Conflicts : 81366 (Analyzed: 81363) +Restarts : 294 (Average: 276.74 Last: 202) +Model-Level : 212.0 +Problems : 7 (Average Length: 14.14 Splits: 0) +Lemmas : 81363 (Deleted: 64324) + Binary : 4084 (Ratio: 5.02%) + Ternary : 955 (Ratio: 1.17%) + Conflict : 81363 (Average Length: 724.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 81363 (Average: 7.56 Max: 401 Sum: 614802) + Executed : 81318 (Average: 7.55 Max: 401 Sum: 614150 Ratio: 99.89%) + Bounded : 45 (Average: 14.49 Max: 27 Sum: 652 Ratio: 0.11%) + +Rules : 94613 (Original: 86518) +Atoms : 45936 +Bodies : 40692 (Original: 32596) + Count : 619 (Original: 1518) +Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) +Tight : Yes +Variables : 102315 (Eliminated: 8994 Frozen: 85791) +Constraints : 684819 (Binary: 91.1% Ternary: 6.6% Other: 2.3%) + +Memory Peak : 371MB +Max. Length : 20 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 16.64s +Memory: 307MB (+80MB) +UNKNOWN +Iteration Time: 17.16s + +Iteration 7 +Queue: [(6,30,0,True)] +Grounded Until: 25 +Expected Memory: 389.0MB +Grounding... [('step', [26]), ('step', [27]), ('step', [28]), ('step', [29]), ('step', [30]), ('check', [30])] +Grounding Time: 0.31s +Memory: 309MB (+2MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 8 +Time : 59.418s (Solving: 54.48s 1st Model: 0.00s Unsat: 7.40s) +CPU Time : 59.364s + +Choices : 877843 (Domain: 807962) +Conflicts : 109490 (Analyzed: 109487) +Restarts : 394 (Average: 277.89 Last: 202) +Model-Level : 212.0 +Problems : 8 (Average Length: 16.38 Splits: 0) +Lemmas : 109487 (Deleted: 90819) + Binary : 5308 (Ratio: 4.85%) + Ternary : 1262 (Ratio: 1.15%) + Conflict : 109487 (Average Length: 786.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 109487 (Average: 7.61 Max: 401 Sum: 833224) + Executed : 109442 (Average: 7.60 Max: 401 Sum: 832572 Ratio: 99.92%) + Bounded : 45 (Average: 14.49 Max: 27 Sum: 652 Ratio: 0.08%) + +Rules : 94613 (Original: 86518) +Atoms : 45936 +Bodies : 40692 (Original: 32596) + Count : 619 (Original: 1518) +Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) +Tight : Yes +Variables : 124876 (Eliminated: 8994 Frozen: 108352) +Constraints : 851268 (Binary: 91.2% Ternary: 6.6% Other: 2.2%) + +Memory Peak : 371MB +Max. Length : 25 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 17.29s +Memory: 322MB (+13MB) +UNKNOWN +Iteration Time: 17.77s + +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 : 68.575s (Solving: 63.60s 1st Model: 0.00s Unsat: 7.40s) +CPU Time : 68.524s + +Choices : 967961 (Domain: 898080) +Conflicts : 137673 (Analyzed: 137670) +Restarts : 494 (Average: 278.68 Last: 202) +Model-Level : 212.0 +Problems : 9 (Average Length: 18.11 Splits: 0) +Lemmas : 137670 (Deleted: 117901) + Binary : 5569 (Ratio: 4.05%) + Ternary : 1305 (Ratio: 0.95%) + Conflict : 137670 (Average Length: 706.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 137670 (Average: 6.66 Max: 401 Sum: 917259) + Executed : 137622 (Average: 6.66 Max: 401 Sum: 916516 Ratio: 99.92%) + Bounded : 48 (Average: 15.48 Max: 32 Sum: 743 Ratio: 0.08%) + +Rules : 94613 (Original: 86518) +Atoms : 45936 +Bodies : 40692 (Original: 32596) + Count : 619 (Original: 1518) +Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) +Tight : Yes +Variables : 124876 (Eliminated: 8994 Frozen: 115882) +Constraints : 851268 (Binary: 91.2% Ternary: 6.6% Other: 2.2%) + +Memory Peak : 371MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.15s +Memory: 322MB (+0MB) +UNKNOWN +Iteration Time: 9.16s + +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 : 93.661s (Solving: 88.65s 1st Model: 0.00s Unsat: 7.40s) +CPU Time : 93.620s + +Choices : 1092316 (Domain: 1022396) +Conflicts : 165767 (Analyzed: 165764) +Restarts : 594 (Average: 279.06 Last: 202) +Model-Level : 212.0 +Problems : 10 (Average Length: 19.50 Splits: 0) +Lemmas : 165764 (Deleted: 145297) + Binary : 5831 (Ratio: 3.52%) + Ternary : 1370 (Ratio: 0.83%) + Conflict : 165764 (Average Length: 807.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 165764 (Average: 6.21 Max: 401 Sum: 1028957) + Executed : 165715 (Average: 6.20 Max: 401 Sum: 1028182 Ratio: 99.92%) + Bounded : 49 (Average: 15.82 Max: 32 Sum: 775 Ratio: 0.08%) + +Rules : 94613 (Original: 86518) +Atoms : 45936 +Bodies : 40692 (Original: 32596) + Count : 619 (Original: 1518) +Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) +Tight : Yes +Variables : 124876 (Eliminated: 8994 Frozen: 115882) +Constraints : 851240 (Binary: 91.2% Ternary: 6.6% Other: 2.2%) + +Memory Peak : 371MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 25.09s +Memory: 322MB (+0MB) +UNKNOWN +Iteration Time: 25.10s + +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 : 114.674s (Solving: 109.62s 1st Model: 0.00s Unsat: 7.40s) +CPU Time : 114.644s + +Choices : 1339062 (Domain: 1266460) +Conflicts : 193889 (Analyzed: 193886) +Restarts : 694 (Average: 279.37 Last: 202) +Model-Level : 212.0 +Problems : 11 (Average Length: 20.64 Splits: 0) +Lemmas : 193886 (Deleted: 172108) + Binary : 6429 (Ratio: 3.32%) + Ternary : 1486 (Ratio: 0.77%) + Conflict : 193886 (Average Length: 813.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 193886 (Average: 6.49 Max: 401 Sum: 1259166) + Executed : 193837 (Average: 6.49 Max: 401 Sum: 1258391 Ratio: 99.94%) + Bounded : 49 (Average: 15.82 Max: 32 Sum: 775 Ratio: 0.06%) + +Rules : 94613 (Original: 86518) +Atoms : 45936 +Bodies : 40692 (Original: 32596) + Count : 619 (Original: 1518) +Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) +Tight : Yes +Variables : 124876 (Eliminated: 8994 Frozen: 115882) +Constraints : 849719 (Binary: 91.2% Ternary: 6.6% Other: 2.2%) + +Memory Peak : 371MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 21.00s +Memory: 322MB (+0MB) +UNKNOWN +Iteration Time: 21.03s + +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: 404.0MB +Grounding... [('step', [31]), ('step', [32]), ('step', [33]), ('step', [34]), ('step', [35]), ('check', [35])] +Grounding Time: 0.32s +Memory: 324MB (+2MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 12 +Time : 129.744s (Solving: 123.86s 1st Model: 0.00s Unsat: 7.40s) +CPU Time : 129.720s + +Choices : 1533857 (Domain: 1454042) +Conflicts : 222078 (Analyzed: 222075) +Restarts : 794 (Average: 279.69 Last: 202) +Model-Level : 212.0 +Problems : 12 (Average Length: 22.00 Splits: 0) +Lemmas : 222075 (Deleted: 198986) + Binary : 7350 (Ratio: 3.31%) + Ternary : 1575 (Ratio: 0.71%) + Conflict : 222075 (Average Length: 769.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 222075 (Average: 6.49 Max: 401 Sum: 1440214) + Executed : 222025 (Average: 6.48 Max: 401 Sum: 1439402 Ratio: 99.94%) + Bounded : 50 (Average: 16.24 Max: 37 Sum: 812 Ratio: 0.06%) + +Rules : 94613 (Original: 86518) +Atoms : 45936 +Bodies : 40692 (Original: 32596) + Count : 619 (Original: 1518) +Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) +Tight : Yes +Variables : 147437 (Eliminated: 8994 Frozen: 130913) +Constraints : 1022744 (Binary: 91.3% Ternary: 6.6% Other: 2.2%) + +Memory Peak : 371MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 14.59s +Memory: 344MB (+20MB) +UNKNOWN +Iteration Time: 15.09s + +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: 426.0MB +Grounding... [('step', [36]), ('step', [37]), ('step', [38]), ('step', [39]), ('step', [40]), ('check', [40])] +Grounding Time: 0.42s +Memory: 357MB (+13MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 13 +Time : 145.922s (Solving: 139.08s 1st Model: 0.00s Unsat: 7.40s) +CPU Time : 145.904s + +Choices : 1767987 (Domain: 1676424) +Conflicts : 250245 (Analyzed: 250242) +Restarts : 894 (Average: 279.91 Last: 206) +Model-Level : 212.0 +Problems : 13 (Average Length: 23.54 Splits: 0) +Lemmas : 250242 (Deleted: 225054) + Binary : 8412 (Ratio: 3.36%) + Ternary : 1719 (Ratio: 0.69%) + Conflict : 250242 (Average Length: 767.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 250242 (Average: 6.60 Max: 401 Sum: 1652594) + Executed : 250191 (Average: 6.60 Max: 401 Sum: 1651740 Ratio: 99.95%) + Bounded : 51 (Average: 16.75 Max: 42 Sum: 854 Ratio: 0.05%) + +Rules : 94613 (Original: 86518) +Atoms : 45936 +Bodies : 40692 (Original: 32596) + Count : 619 (Original: 1518) +Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) +Tight : Yes +Variables : 169998 (Eliminated: 8994 Frozen: 153474) +Constraints : 1195759 (Binary: 91.3% Ternary: 6.6% Other: 2.1%) + +Memory Peak : 377MB +Max. Length : 35 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 15.59s +Memory: 366MB (+9MB) +UNKNOWN +Iteration Time: 16.20s + +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: 448.0MB +Grounding... [('step', [41]), ('step', [42]), ('step', [43]), ('step', [44]), ('step', [45]), ('check', [45])] +Grounding Time: 0.31s +Memory: 367MB (+1MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 14 +Time : 162.860s (Solving: 155.16s 1st Model: 0.00s Unsat: 7.40s) +CPU Time : 162.848s + +Choices : 2012899 (Domain: 1917846) +Conflicts : 278412 (Analyzed: 278409) +Restarts : 994 (Average: 280.09 Last: 206) +Model-Level : 212.0 +Problems : 14 (Average Length: 25.21 Splits: 0) +Lemmas : 278409 (Deleted: 251719) + Binary : 9241 (Ratio: 3.32%) + Ternary : 1798 (Ratio: 0.65%) + Conflict : 278409 (Average Length: 767.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 278409 (Average: 6.73 Max: 401 Sum: 1873261) + Executed : 278358 (Average: 6.73 Max: 401 Sum: 1872407 Ratio: 99.95%) + Bounded : 51 (Average: 16.75 Max: 42 Sum: 854 Ratio: 0.05%) + +Rules : 94613 (Original: 86518) +Atoms : 45936 +Bodies : 40692 (Original: 32596) + Count : 619 (Original: 1518) +Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) +Tight : Yes +Variables : 192559 (Eliminated: 8994 Frozen: 176035) +Constraints : 1368767 (Binary: 91.3% Ternary: 6.6% Other: 2.1%) + +Memory Peak : 393MB +Max. Length : 40 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 16.44s +Memory: 381MB (+14MB) +UNKNOWN +Iteration Time: 16.95s + +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: 463.0MB +Grounding... [('step', [46]), ('step', [47]), ('step', [48]), ('step', [49]), ('step', [50]), ('check', [50])] +Grounding Time: 0.31s +Memory: 381MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 15 +Time : 178.759s (Solving: 170.19s 1st Model: 0.00s Unsat: 7.40s) +CPU Time : 178.752s + +Choices : 2307695 (Domain: 2197417) +Conflicts : 306536 (Analyzed: 306533) +Restarts : 1094 (Average: 280.19 Last: 208) +Model-Level : 212.0 +Problems : 15 (Average Length: 27.00 Splits: 0) +Lemmas : 306533 (Deleted: 278324) + Binary : 10317 (Ratio: 3.37%) + Ternary : 1985 (Ratio: 0.65%) + Conflict : 306533 (Average Length: 750.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 306533 (Average: 6.98 Max: 401 Sum: 2139960) + Executed : 306482 (Average: 6.98 Max: 401 Sum: 2139106 Ratio: 99.96%) + Bounded : 51 (Average: 16.75 Max: 42 Sum: 854 Ratio: 0.04%) + +Rules : 94613 (Original: 86518) +Atoms : 45936 +Bodies : 40692 (Original: 32596) + Count : 619 (Original: 1518) +Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) +Tight : Yes +Variables : 215120 (Eliminated: 8994 Frozen: 198596) +Constraints : 1541792 (Binary: 91.4% Ternary: 6.6% Other: 2.1%) + +Memory Peak : 412MB +Max. Length : 45 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 15.40s +Memory: 410MB (+29MB) +UNKNOWN +Iteration Time: 15.91s + +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: 492.0MB +Grounding... [('step', [51]), ('step', [52]), ('step', [53]), ('step', [54]), ('step', [55]), ('check', [55])] +Grounding Time: 0.31s +Memory: 410MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 16 +Time : 196.304s (Solving: 186.86s 1st Model: 0.00s Unsat: 7.40s) +CPU Time : 196.304s + +Choices : 2586997 (Domain: 2474559) +Conflicts : 334700 (Analyzed: 334697) +Restarts : 1194 (Average: 280.32 Last: 208) +Model-Level : 212.0 +Problems : 16 (Average Length: 28.88 Splits: 0) +Lemmas : 334697 (Deleted: 304977) + Binary : 11080 (Ratio: 3.31%) + Ternary : 2047 (Ratio: 0.61%) + Conflict : 334697 (Average Length: 761.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 334697 (Average: 7.14 Max: 401 Sum: 2391390) + Executed : 334646 (Average: 7.14 Max: 401 Sum: 2390536 Ratio: 99.96%) + Bounded : 51 (Average: 16.75 Max: 42 Sum: 854 Ratio: 0.04%) + +Rules : 94613 (Original: 86518) +Atoms : 45936 +Bodies : 40692 (Original: 32596) + Count : 619 (Original: 1518) +Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) +Tight : Yes +Variables : 237681 (Eliminated: 8994 Frozen: 221157) +Constraints : 1714817 (Binary: 91.4% Ternary: 6.6% Other: 2.0%) + +Memory Peak : 439MB +Max. Length : 50 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 17.03s +Memory: 420MB (+10MB) +UNKNOWN +Iteration Time: 17.56s + +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: 502.0MB +Grounding... [('step', [56]), ('step', [57]), ('step', [58]), ('step', [59]), ('step', [60]), ('check', [60])] +Grounding Time: 0.34s +Memory: 420MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 17 +Time : 212.017s (Solving: 201.64s 1st Model: 0.00s Unsat: 7.40s) +CPU Time : 212.024s + +Choices : 2773336 (Domain: 2660889) +Conflicts : 362908 (Analyzed: 362905) +Restarts : 1294 (Average: 280.45 Last: 208) +Model-Level : 212.0 +Problems : 17 (Average Length: 30.82 Splits: 0) +Lemmas : 362905 (Deleted: 332355) + Binary : 11510 (Ratio: 3.17%) + Ternary : 2097 (Ratio: 0.58%) + Conflict : 362905 (Average Length: 755.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 362905 (Average: 7.05 Max: 401 Sum: 2556974) + Executed : 362854 (Average: 7.04 Max: 401 Sum: 2556120 Ratio: 99.97%) + Bounded : 51 (Average: 16.75 Max: 42 Sum: 854 Ratio: 0.03%) + +Rules : 94613 (Original: 86518) +Atoms : 45936 +Bodies : 40692 (Original: 32596) + Count : 619 (Original: 1518) +Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) +Tight : Yes +Variables : 260242 (Eliminated: 8994 Frozen: 243718) +Constraints : 1887842 (Binary: 91.4% Ternary: 6.6% Other: 2.0%) + +Memory Peak : 455MB +Max. Length : 55 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 15.15s +Memory: 434MB (+14MB) +UNKNOWN +Iteration Time: 15.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: 516.0MB +Grounding... [('step', [61]), ('step', [62]), ('step', [63]), ('step', [64]), ('step', [65]), ('check', [65])] +Grounding Time: 0.32s +Memory: 434MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 18 +Time : 231.824s (Solving: 220.52s 1st Model: 0.00s Unsat: 7.40s) +CPU Time : 231.840s + +Choices : 3047628 (Domain: 2934473) +Conflicts : 391041 (Analyzed: 391038) +Restarts : 1394 (Average: 280.52 Last: 208) +Model-Level : 212.0 +Problems : 18 (Average Length: 32.83 Splits: 0) +Lemmas : 391038 (Deleted: 359574) + Binary : 11990 (Ratio: 3.07%) + Ternary : 2151 (Ratio: 0.55%) + Conflict : 391038 (Average Length: 753.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 391038 (Average: 7.17 Max: 401 Sum: 2805345) + Executed : 390987 (Average: 7.17 Max: 401 Sum: 2804491 Ratio: 99.97%) + Bounded : 51 (Average: 16.75 Max: 42 Sum: 854 Ratio: 0.03%) + +Rules : 94613 (Original: 86518) +Atoms : 45936 +Bodies : 40692 (Original: 32596) + Count : 619 (Original: 1518) +Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) +Tight : Yes +Variables : 282803 (Eliminated: 8994 Frozen: 266279) +Constraints : 2060867 (Binary: 91.4% Ternary: 6.6% Other: 2.0%) + +Memory Peak : 473MB +Max. Length : 60 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 19.27s +Memory: 452MB (+18MB) +UNKNOWN +Iteration Time: 19.82s + +Iteration 18 +Queue: [(14,70,0,True), (15,75,0,True), (16,80,0,True), (17,85,0,True)] +Grounded Until: 65 +Expected Memory: 534.0MB +Grounding... [('step', [66]), ('step', [67]), ('step', [68]), ('step', [69]), ('step', [70]), ('check', [70])] +Grounding Time: 0.33s +Memory: 452MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 19 +Time : 249.390s (Solving: 237.13s 1st Model: 0.00s Unsat: 7.40s) +CPU Time : 249.416s + +Choices : 3272129 (Domain: 3158615) +Conflicts : 419210 (Analyzed: 419207) +Restarts : 1494 (Average: 280.59 Last: 208) +Model-Level : 212.0 +Problems : 19 (Average Length: 34.89 Splits: 0) +Lemmas : 419207 (Deleted: 385854) + Binary : 12459 (Ratio: 2.97%) + Ternary : 2197 (Ratio: 0.52%) + Conflict : 419207 (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 : 419207 (Average: 7.16 Max: 401 Sum: 3002607) + Executed : 419156 (Average: 7.16 Max: 401 Sum: 3001753 Ratio: 99.97%) + Bounded : 51 (Average: 16.75 Max: 42 Sum: 854 Ratio: 0.03%) + +Rules : 94613 (Original: 86518) +Atoms : 45936 +Bodies : 40692 (Original: 32596) + Count : 619 (Original: 1518) +Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) +Tight : Yes +Variables : 305364 (Eliminated: 8994 Frozen: 288840) +Constraints : 2233892 (Binary: 91.4% Ternary: 6.6% Other: 2.0%) + +Memory Peak : 491MB +Max. Length : 65 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 17.00s +Memory: 490MB (+38MB) +UNKNOWN +Iteration Time: 17.58s + +Iteration 19 +Queue: [(15,75,0,True), (16,80,0,True), (17,85,0,True)] +Grounded Until: 70 +Expected Memory: 572.0MB +Grounding... [('step', [71]), ('step', [72]), ('step', [73]), ('step', [74]), ('step', [75]), ('check', [75])] +Grounding Time: 0.34s +Memory: 490MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 20 +Time : 270.819s (Solving: 257.60s 1st Model: 0.00s Unsat: 7.40s) +CPU Time : 270.856s + +Choices : 3640853 (Domain: 3525454) +Conflicts : 447391 (Analyzed: 447388) +Restarts : 1594 (Average: 280.67 Last: 208) +Model-Level : 212.0 +Problems : 20 (Average Length: 37.00 Splits: 0) +Lemmas : 447388 (Deleted: 413840) + Binary : 13149 (Ratio: 2.94%) + Ternary : 2305 (Ratio: 0.52%) + Conflict : 447388 (Average Length: 767.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 447388 (Average: 7.46 Max: 411 Sum: 3339733) + Executed : 447337 (Average: 7.46 Max: 411 Sum: 3338879 Ratio: 99.97%) + Bounded : 51 (Average: 16.75 Max: 42 Sum: 854 Ratio: 0.03%) + +Rules : 94613 (Original: 86518) +Atoms : 45936 +Bodies : 40692 (Original: 32596) + Count : 619 (Original: 1518) +Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) +Tight : Yes +Variables : 327925 (Eliminated: 8994 Frozen: 311401) +Constraints : 2406917 (Binary: 91.4% Ternary: 6.6% Other: 2.0%) + +Memory Peak : 530MB +Max. Length : 70 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 20.86s +Memory: 503MB (+13MB) +UNKNOWN +Iteration Time: 21.45s + +Iteration 20 +Queue: [(16,80,0,True), (17,85,0,True)] +Grounded Until: 75 +Expected Memory: 585.0MB +Grounding... [('step', [76]), ('step', [77]), ('step', [78]), ('step', [79]), ('step', [80]), ('check', [80])] +Grounding Time: 0.48s +Memory: 518MB (+15MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 21 +Time : 289.759s (Solving: 275.43s 1st Model: 0.00s Unsat: 7.40s) +CPU Time : 289.804s + +Choices : 3919967 (Domain: 3804120) +Conflicts : 475574 (Analyzed: 475571) +Restarts : 1694 (Average: 280.74 Last: 208) +Model-Level : 212.0 +Problems : 21 (Average Length: 39.14 Splits: 0) +Lemmas : 475571 (Deleted: 441027) + Binary : 13579 (Ratio: 2.86%) + Ternary : 2347 (Ratio: 0.49%) + Conflict : 475571 (Average Length: 769.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 475571 (Average: 7.53 Max: 411 Sum: 3583315) + Executed : 475520 (Average: 7.53 Max: 411 Sum: 3582461 Ratio: 99.98%) + Bounded : 51 (Average: 16.75 Max: 42 Sum: 854 Ratio: 0.02%) + +Rules : 94613 (Original: 86518) +Atoms : 45936 +Bodies : 40692 (Original: 32596) + Count : 619 (Original: 1518) +Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) +Tight : Yes +Variables : 350486 (Eliminated: 8994 Frozen: 333962) +Constraints : 2579942 (Binary: 91.5% Ternary: 6.6% Other: 2.0%) + +Memory Peak : 561MB +Max. Length : 75 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 18.22s +Memory: 521MB (+3MB) +UNKNOWN +Iteration Time: 18.96s + +Iteration 21 +Queue: [(17,85,0,True)] +Grounded Until: 80 +Expected Memory: 603.0MB +Grounding... [('step', [81]), ('step', [82]), ('step', [83]), ('step', [84]), ('step', [85]), ('check', [85])] +Grounding Time: 0.35s +Memory: 521MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 22 +Time : 308.599s (Solving: 293.27s 1st Model: 0.00s Unsat: 7.40s) +CPU Time : 308.652s + +Choices : 4144295 (Domain: 4028411) +Conflicts : 503747 (Analyzed: 503744) +Restarts : 1794 (Average: 280.79 Last: 208) +Model-Level : 212.0 +Problems : 22 (Average Length: 41.32 Splits: 0) +Lemmas : 503744 (Deleted: 468601) + Binary : 13902 (Ratio: 2.76%) + Ternary : 2400 (Ratio: 0.48%) + Conflict : 503744 (Average Length: 769.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 503744 (Average: 7.50 Max: 422 Sum: 3776949) + Executed : 503693 (Average: 7.50 Max: 422 Sum: 3776095 Ratio: 99.98%) + Bounded : 51 (Average: 16.75 Max: 42 Sum: 854 Ratio: 0.02%) + +Rules : 94613 (Original: 86518) +Atoms : 45936 +Bodies : 40692 (Original: 32596) + Count : 619 (Original: 1518) +Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) +Tight : Yes +Variables : 373047 (Eliminated: 8994 Frozen: 356523) +Constraints : 2752967 (Binary: 91.5% Ternary: 6.6% Other: 2.0%) + +Memory Peak : 570MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 18.23s +Memory: 538MB (+17MB) +UNKNOWN +Iteration Time: 18.86s + +Iteration 22 +Queue: [(4,20,2,True), (5,25,2,True), (6,30,2,True), (7,35,1,True), (8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 85 +Blocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 23 +Time : 318.795s (Solving: 303.36s 1st Model: 0.00s Unsat: 7.40s) +CPU Time : 318.852s + +Choices : 4279001 (Domain: 4163117) +Conflicts : 531936 (Analyzed: 531933) +Restarts : 1894 (Average: 280.85 Last: 208) +Model-Level : 212.0 +Problems : 23 (Average Length: 43.30 Splits: 0) +Lemmas : 531933 (Deleted: 495516) + Binary : 14207 (Ratio: 2.67%) + Ternary : 2487 (Ratio: 0.47%) + Conflict : 531933 (Average Length: 746.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 531933 (Average: 7.34 Max: 422 Sum: 3904971) + Executed : 531877 (Average: 7.34 Max: 422 Sum: 3903854 Ratio: 99.97%) + Bounded : 56 (Average: 19.95 Max: 87 Sum: 1117 Ratio: 0.03%) + +Rules : 94613 (Original: 86518) +Atoms : 45936 +Bodies : 40692 (Original: 32596) + Count : 619 (Original: 1518) +Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) +Tight : Yes +Variables : 373047 (Eliminated: 8994 Frozen: 364053) +Constraints : 2752967 (Binary: 91.5% Ternary: 6.6% Other: 2.0%) + +Memory Peak : 570MB +Max. Length : 85 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 10.16s +Memory: 539MB (+1MB) +UNKNOWN +Iteration Time: 10.20s + +Iteration 23 +Queue: [(5,25,2,True), (6,30,2,True), (7,35,1,True), (8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 85 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 24 +Time : 341.990s (Solving: 326.47s 1st Model: 0.00s Unsat: 7.40s) +CPU Time : 342.056s + +Choices : 4445936 (Domain: 4330052) +Conflicts : 560051 (Analyzed: 560048) +Restarts : 1994 (Average: 280.87 Last: 208) +Model-Level : 212.0 +Problems : 24 (Average Length: 45.12 Splits: 0) +Lemmas : 560048 (Deleted: 523095) + Binary : 14316 (Ratio: 2.56%) + Ternary : 2508 (Ratio: 0.45%) + Conflict : 560048 (Average Length: 770.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 560048 (Average: 7.25 Max: 422 Sum: 4058898) + Executed : 559992 (Average: 7.25 Max: 422 Sum: 4057781 Ratio: 99.97%) + Bounded : 56 (Average: 19.95 Max: 87 Sum: 1117 Ratio: 0.03%) + +Rules : 94613 (Original: 86518) +Atoms : 45936 +Bodies : 40692 (Original: 32596) + Count : 619 (Original: 1518) +Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) +Tight : Yes +Variables : 373047 (Eliminated: 8994 Frozen: 364053) +Constraints : 2752926 (Binary: 91.5% Ternary: 6.6% Other: 2.0%) + +Memory Peak : 570MB +Max. Length : 85 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 23.17s +Memory: 539MB (+0MB) +UNKNOWN +Iteration Time: 23.21s + +Iteration 24 +Queue: [(6,30,2,True), (7,35,1,True), (8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 85 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 25 +Time : 363.254s (Solving: 347.64s 1st Model: 0.00s Unsat: 7.40s) +CPU Time : 363.328s + +Choices : 4644807 (Domain: 4528923) +Conflicts : 588257 (Analyzed: 588254) +Restarts : 2094 (Average: 280.92 Last: 208) +Model-Level : 212.0 +Problems : 25 (Average Length: 46.80 Splits: 0) +Lemmas : 588254 (Deleted: 550824) + Binary : 14516 (Ratio: 2.47%) + Ternary : 2528 (Ratio: 0.43%) + Conflict : 588254 (Average Length: 784.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 588254 (Average: 7.21 Max: 422 Sum: 4239616) + Executed : 588198 (Average: 7.21 Max: 422 Sum: 4238499 Ratio: 99.97%) + Bounded : 56 (Average: 19.95 Max: 87 Sum: 1117 Ratio: 0.03%) + +Rules : 94613 (Original: 86518) +Atoms : 45936 +Bodies : 40692 (Original: 32596) + Count : 619 (Original: 1518) +Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) +Tight : Yes +Variables : 373047 (Eliminated: 8994 Frozen: 364053) +Constraints : 2752926 (Binary: 91.5% Ternary: 6.6% Other: 2.0%) + +Memory Peak : 570MB +Max. Length : 85 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 21.24s +Memory: 539MB (+0MB) +UNKNOWN +Iteration Time: 21.27s + +Iteration 25 +Queue: [(7,35,1,True), (8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 85 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 26 +Time : 382.171s (Solving: 366.47s 1st Model: 0.00s Unsat: 7.40s) +CPU Time : 382.252s + +Choices : 4830241 (Domain: 4714316) +Conflicts : 616452 (Analyzed: 616449) +Restarts : 2194 (Average: 280.97 Last: 208) +Model-Level : 212.0 +Problems : 26 (Average Length: 48.35 Splits: 0) +Lemmas : 616449 (Deleted: 578167) + Binary : 14789 (Ratio: 2.40%) + Ternary : 2561 (Ratio: 0.42%) + Conflict : 616449 (Average Length: 796.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 616449 (Average: 7.14 Max: 422 Sum: 4404496) + Executed : 616393 (Average: 7.14 Max: 422 Sum: 4403379 Ratio: 99.97%) + Bounded : 56 (Average: 19.95 Max: 87 Sum: 1117 Ratio: 0.03%) + +Rules : 94613 (Original: 86518) +Atoms : 45936 +Bodies : 40692 (Original: 32596) + Count : 619 (Original: 1518) +Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) +Tight : Yes +Variables : 373047 (Eliminated: 8994 Frozen: 364053) +Constraints : 2752926 (Binary: 91.5% Ternary: 6.6% Other: 2.0%) + +Memory Peak : 570MB +Max. Length : 85 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 18.89s +Memory: 539MB (+0MB) +UNKNOWN +Iteration Time: 18.93s + +Iteration 26 +Queue: [(8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 85 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 27 +Time : 401.087s (Solving: 385.29s 1st Model: 0.00s Unsat: 7.40s) +CPU Time : 401.176s + +Choices : 5047045 (Domain: 4930963) +Conflicts : 644660 (Analyzed: 644657) +Restarts : 2294 (Average: 281.02 Last: 208) +Model-Level : 212.0 +Problems : 27 (Average Length: 49.78 Splits: 0) +Lemmas : 644657 (Deleted: 605343) + Binary : 15109 (Ratio: 2.34%) + Ternary : 2628 (Ratio: 0.41%) + Conflict : 644657 (Average Length: 801.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 644657 (Average: 7.13 Max: 422 Sum: 4599188) + Executed : 644601 (Average: 7.13 Max: 422 Sum: 4598071 Ratio: 99.98%) + Bounded : 56 (Average: 19.95 Max: 87 Sum: 1117 Ratio: 0.02%) + +Rules : 94613 (Original: 86518) +Atoms : 45936 +Bodies : 40692 (Original: 32596) + Count : 619 (Original: 1518) +Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) +Tight : Yes +Variables : 373047 (Eliminated: 8994 Frozen: 364053) +Constraints : 2752926 (Binary: 91.5% Ternary: 6.6% Other: 2.0%) + +Memory Peak : 570MB +Max. Length : 85 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 18.88s +Memory: 539MB (+0MB) +UNKNOWN +Iteration Time: 18.93s + +Iteration 27 +Queue: [(9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 85 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 28 +Time : 418.204s (Solving: 402.31s 1st Model: 0.00s Unsat: 7.40s) +CPU Time : 418.300s + +Choices : 5239786 (Domain: 5123692) +Conflicts : 672866 (Analyzed: 672863) +Restarts : 2394 (Average: 281.06 Last: 208) +Model-Level : 212.0 +Problems : 28 (Average Length: 51.11 Splits: 0) +Lemmas : 672863 (Deleted: 629204) + Binary : 15390 (Ratio: 2.29%) + Ternary : 2662 (Ratio: 0.40%) + Conflict : 672863 (Average Length: 807.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 672863 (Average: 7.09 Max: 422 Sum: 4768425) + Executed : 672806 (Average: 7.08 Max: 422 Sum: 4767221 Ratio: 99.97%) + Bounded : 57 (Average: 21.12 Max: 87 Sum: 1204 Ratio: 0.03%) + +Rules : 94613 (Original: 86518) +Atoms : 45936 +Bodies : 40692 (Original: 32596) + Count : 619 (Original: 1518) +Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) +Tight : Yes +Variables : 373047 (Eliminated: 8994 Frozen: 364053) +Constraints : 2752926 (Binary: 91.5% Ternary: 6.6% Other: 2.0%) + +Memory Peak : 570MB +Max. Length : 85 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 17.09s +Memory: 539MB (+0MB) +UNKNOWN +Iteration Time: 17.13s + +Iteration 28 +Queue: [(10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 85 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 29 +Time : 436.448s (Solving: 420.46s 1st Model: 0.00s Unsat: 7.40s) +CPU Time : 436.556s + +Choices : 5467858 (Domain: 5351680) +Conflicts : 701060 (Analyzed: 701057) +Restarts : 2494 (Average: 281.10 Last: 208) +Model-Level : 212.0 +Problems : 29 (Average Length: 52.34 Splits: 0) +Lemmas : 701057 (Deleted: 660279) + Binary : 15680 (Ratio: 2.24%) + Ternary : 2715 (Ratio: 0.39%) + Conflict : 701057 (Average Length: 812.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 701057 (Average: 7.09 Max: 422 Sum: 4970877) + Executed : 701000 (Average: 7.09 Max: 422 Sum: 4969673 Ratio: 99.98%) + Bounded : 57 (Average: 21.12 Max: 87 Sum: 1204 Ratio: 0.02%) + +Rules : 94613 (Original: 86518) +Atoms : 45936 +Bodies : 40692 (Original: 32596) + Count : 619 (Original: 1518) +Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) +Tight : Yes +Variables : 373047 (Eliminated: 8994 Frozen: 364053) +Constraints : 2752943 (Binary: 91.5% Ternary: 6.6% Other: 2.0%) + +Memory Peak : 570MB +Max. Length : 85 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 18.21s +Memory: 539MB (+0MB) +UNKNOWN +Iteration Time: 18.25s + +Iteration 29 +Queue: [(11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 85 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 30 +Time : 454.565s (Solving: 438.46s 1st Model: 0.00s Unsat: 7.40s) +CPU Time : 454.680s + +Choices : 5730727 (Domain: 5611371) +Conflicts : 729232 (Analyzed: 729229) +Restarts : 2594 (Average: 281.12 Last: 208) +Model-Level : 212.0 +Problems : 30 (Average Length: 53.50 Splits: 0) +Lemmas : 729229 (Deleted: 687180) + Binary : 16233 (Ratio: 2.23%) + Ternary : 2797 (Ratio: 0.38%) + Conflict : 729229 (Average Length: 817.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 729229 (Average: 7.13 Max: 422 Sum: 5202937) + Executed : 729172 (Average: 7.13 Max: 422 Sum: 5201733 Ratio: 99.98%) + Bounded : 57 (Average: 21.12 Max: 87 Sum: 1204 Ratio: 0.02%) + +Rules : 94613 (Original: 86518) +Atoms : 45936 +Bodies : 40692 (Original: 32596) + Count : 619 (Original: 1518) +Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) +Tight : Yes +Variables : 373047 (Eliminated: 8994 Frozen: 364053) +Constraints : 2752943 (Binary: 91.5% Ternary: 6.6% Other: 2.0%) + +Memory Peak : 570MB +Max. Length : 85 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 18.08s +Memory: 539MB (+0MB) +UNKNOWN +Iteration Time: 18.13s + +Iteration 30 +Queue: [(12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 85 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 31 +Time : 473.320s (Solving: 457.13s 1st Model: 0.00s Unsat: 7.40s) +CPU Time : 473.444s + +Choices : 5981872 (Domain: 5862089) +Conflicts : 757399 (Analyzed: 757396) +Restarts : 2694 (Average: 281.14 Last: 208) +Model-Level : 212.0 +Problems : 31 (Average Length: 54.58 Splits: 0) +Lemmas : 757396 (Deleted: 714426) + Binary : 16612 (Ratio: 2.19%) + Ternary : 2876 (Ratio: 0.38%) + Conflict : 757396 (Average Length: 824.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 757396 (Average: 7.16 Max: 422 Sum: 5421783) + Executed : 757339 (Average: 7.16 Max: 422 Sum: 5420579 Ratio: 99.98%) + Bounded : 57 (Average: 21.12 Max: 87 Sum: 1204 Ratio: 0.02%) + +Rules : 94613 (Original: 86518) +Atoms : 45936 +Bodies : 40692 (Original: 32596) + Count : 619 (Original: 1518) +Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) +Tight : Yes +Variables : 373047 (Eliminated: 8994 Frozen: 364053) +Constraints : 2752943 (Binary: 91.5% Ternary: 6.6% Other: 2.0%) + +Memory Peak : 570MB +Max. Length : 85 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 18.73s +Memory: 539MB (+0MB) +UNKNOWN +Iteration Time: 18.77s + +Iteration 31 +Queue: [(13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 85 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 32 +Time : 492.304s (Solving: 476.02s 1st Model: 0.00s Unsat: 7.40s) +CPU Time : 492.436s + +Choices : 6228255 (Domain: 6106842) +Conflicts : 785595 (Analyzed: 785592) +Restarts : 2794 (Average: 281.17 Last: 208) +Model-Level : 212.0 +Problems : 32 (Average Length: 55.59 Splits: 0) +Lemmas : 785592 (Deleted: 741922) + Binary : 16886 (Ratio: 2.15%) + Ternary : 2920 (Ratio: 0.37%) + Conflict : 785592 (Average Length: 824.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 785592 (Average: 7.18 Max: 422 Sum: 5638165) + Executed : 785535 (Average: 7.18 Max: 422 Sum: 5636961 Ratio: 99.98%) + Bounded : 57 (Average: 21.12 Max: 87 Sum: 1204 Ratio: 0.02%) + +Rules : 94613 (Original: 86518) +Atoms : 45936 +Bodies : 40692 (Original: 32596) + Count : 619 (Original: 1518) +Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) +Tight : Yes +Variables : 373047 (Eliminated: 8994 Frozen: 364053) +Constraints : 2752943 (Binary: 91.5% Ternary: 6.6% Other: 2.0%) + +Memory Peak : 570MB +Max. Length : 85 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 18.96s +Memory: 539MB (+0MB) +UNKNOWN +Iteration Time: 18.99s + +Iteration 32 +Queue: [(14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 85 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 33 +Time : 510.250s (Solving: 493.88s 1st Model: 0.00s Unsat: 7.40s) +CPU Time : 510.388s + +Choices : 6411718 (Domain: 6290301) +Conflicts : 813772 (Analyzed: 813769) +Restarts : 2894 (Average: 281.19 Last: 208) +Model-Level : 212.0 +Problems : 33 (Average Length: 56.55 Splits: 0) +Lemmas : 813769 (Deleted: 769442) + Binary : 17087 (Ratio: 2.10%) + Ternary : 2949 (Ratio: 0.36%) + Conflict : 813769 (Average Length: 824.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 813769 (Average: 7.12 Max: 422 Sum: 5794406) + Executed : 813712 (Average: 7.12 Max: 422 Sum: 5793202 Ratio: 99.98%) + Bounded : 57 (Average: 21.12 Max: 87 Sum: 1204 Ratio: 0.02%) + +Rules : 94613 (Original: 86518) +Atoms : 45936 +Bodies : 40692 (Original: 32596) + Count : 619 (Original: 1518) +Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) +Tight : Yes +Variables : 373047 (Eliminated: 8994 Frozen: 364053) +Constraints : 2752943 (Binary: 91.5% Ternary: 6.6% Other: 2.0%) + +Memory Peak : 570MB +Max. Length : 85 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 17.92s +Memory: 539MB (+0MB) +UNKNOWN +Iteration Time: 17.96s + +Iteration 33 +Queue: [(15,75,1,True), (16,80,1,True), (17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 85 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 34 +Time : 528.226s (Solving: 511.78s 1st Model: 0.00s Unsat: 7.40s) +CPU Time : 528.372s + +Choices : 6782170 (Domain: 6651138) +Conflicts : 841921 (Analyzed: 841918) +Restarts : 2994 (Average: 281.20 Last: 208) +Model-Level : 212.0 +Problems : 34 (Average Length: 57.44 Splits: 0) +Lemmas : 841918 (Deleted: 796005) + Binary : 17873 (Ratio: 2.12%) + Ternary : 3072 (Ratio: 0.36%) + Conflict : 841918 (Average Length: 818.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 841918 (Average: 7.28 Max: 422 Sum: 6127115) + Executed : 841861 (Average: 7.28 Max: 422 Sum: 6125911 Ratio: 99.98%) + Bounded : 57 (Average: 21.12 Max: 87 Sum: 1204 Ratio: 0.02%) + +Rules : 94613 (Original: 86518) +Atoms : 45936 +Bodies : 40692 (Original: 32596) + Count : 619 (Original: 1518) +Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) +Tight : Yes +Variables : 373047 (Eliminated: 8994 Frozen: 364053) +Constraints : 2752943 (Binary: 91.5% Ternary: 6.6% Other: 2.0%) + +Memory Peak : 570MB +Max. Length : 85 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 17.96s +Memory: 539MB (+0MB) +UNKNOWN +Iteration Time: 17.99s + +Iteration 34 +Queue: [(16,80,1,True), (17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 85 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 35 +Time : 548.030s (Solving: 531.50s 1st Model: 0.00s Unsat: 7.40s) +CPU Time : 548.184s + +Choices : 7064505 (Domain: 6933096) +Conflicts : 870060 (Analyzed: 870057) +Restarts : 3094 (Average: 281.21 Last: 208) +Model-Level : 212.0 +Problems : 35 (Average Length: 58.29 Splits: 0) +Lemmas : 870057 (Deleted: 823431) + Binary : 18171 (Ratio: 2.09%) + Ternary : 3117 (Ratio: 0.36%) + Conflict : 870057 (Average Length: 820.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 870057 (Average: 7.32 Max: 422 Sum: 6371425) + Executed : 870000 (Average: 7.32 Max: 422 Sum: 6370221 Ratio: 99.98%) + Bounded : 57 (Average: 21.12 Max: 87 Sum: 1204 Ratio: 0.02%) + +Rules : 94613 (Original: 86518) +Atoms : 45936 +Bodies : 40692 (Original: 32596) + Count : 619 (Original: 1518) +Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) +Tight : Yes +Variables : 373047 (Eliminated: 8994 Frozen: 364053) +Constraints : 2752943 (Binary: 91.5% Ternary: 6.6% Other: 2.0%) + +Memory Peak : 570MB +Max. Length : 85 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 19.78s +Memory: 539MB (+0MB) +UNKNOWN +Iteration Time: 19.81s + +Iteration 35 +Queue: [(17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 85 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 36 +Time : 566.296s (Solving: 549.68s 1st Model: 0.00s Unsat: 7.40s) +CPU Time : 566.460s + +Choices : 7461431 (Domain: 7325234) +Conflicts : 898209 (Analyzed: 898206) +Restarts : 3194 (Average: 281.22 Last: 208) +Model-Level : 212.0 +Problems : 36 (Average Length: 59.08 Splits: 0) +Lemmas : 898206 (Deleted: 850370) + Binary : 18778 (Ratio: 2.09%) + Ternary : 3193 (Ratio: 0.36%) + Conflict : 898206 (Average Length: 822.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 898206 (Average: 7.49 Max: 422 Sum: 6724056) + Executed : 898149 (Average: 7.48 Max: 422 Sum: 6722852 Ratio: 99.98%) + Bounded : 57 (Average: 21.12 Max: 87 Sum: 1204 Ratio: 0.02%) + +Rules : 94613 (Original: 86518) +Atoms : 45936 +Bodies : 40692 (Original: 32596) + Count : 619 (Original: 1518) +Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) +Tight : Yes +Variables : 373047 (Eliminated: 8994 Frozen: 364053) +Constraints : 2752943 (Binary: 91.5% Ternary: 6.6% Other: 2.0%) + +Memory Peak : 570MB +Max. Length : 85 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 18.24s +Memory: 539MB (+0MB) +UNKNOWN +Iteration Time: 18.28s + +Iteration 36 +Queue: [(18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 85 +Expected Memory: 621.0MB +Grounding... [('step', [86]), ('step', [87]), ('step', [88]), ('step', [89]), ('step', [90]), ('check', [90])] +Grounding Time: 0.32s +Memory: 539MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 37 +Time : 582.807s (Solving: 565.20s 1st Model: 0.00s Unsat: 7.40s) +CPU Time : 582.980s + +Choices : 7643277 (Domain: 7507080) +Conflicts : 926448 (Analyzed: 926445) +Restarts : 3294 (Average: 281.25 Last: 208) +Model-Level : 212.0 +Problems : 37 (Average Length: 59.97 Splits: 0) +Lemmas : 926445 (Deleted: 874406) + Binary : 18949 (Ratio: 2.05%) + Ternary : 3224 (Ratio: 0.35%) + Conflict : 926445 (Average Length: 811.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 926445 (Average: 7.42 Max: 422 Sum: 6878725) + Executed : 926388 (Average: 7.42 Max: 422 Sum: 6877521 Ratio: 99.98%) + Bounded : 57 (Average: 21.12 Max: 87 Sum: 1204 Ratio: 0.02%) + +Rules : 94613 (Original: 86518) +Atoms : 45936 +Bodies : 40692 (Original: 32596) + Count : 619 (Original: 1518) +Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) +Tight : Yes +Variables : 395608 (Eliminated: 8994 Frozen: 379084) +Constraints : 2925968 (Binary: 91.5% Ternary: 6.6% Other: 2.0%) + +Memory Peak : 589MB +Max. Length : 85 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 15.92s +Memory: 551MB (+12MB) +UNKNOWN +Iteration Time: 16.53s + +Iteration 37 +Queue: [(19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 90 +Expected Memory: 633.0MB +Grounding... [('step', [91]), ('step', [92]), ('step', [93]), ('step', [94]), ('step', [95]), ('check', [95])] +Grounding Time: 0.31s +Memory: 551MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 38 +Time : 604.129s (Solving: 585.54s 1st Model: 0.00s Unsat: 7.40s) +CPU Time : 604.308s + +Choices : 7887991 (Domain: 7751790) +Conflicts : 954605 (Analyzed: 954602) +Restarts : 3394 (Average: 281.26 Last: 208) +Model-Level : 212.0 +Problems : 38 (Average Length: 60.95 Splits: 0) +Lemmas : 954602 (Deleted: 905607) + Binary : 19248 (Ratio: 2.02%) + Ternary : 3267 (Ratio: 0.34%) + Conflict : 954602 (Average Length: 818.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 954602 (Average: 7.42 Max: 426 Sum: 7083953) + Executed : 954545 (Average: 7.42 Max: 426 Sum: 7082749 Ratio: 99.98%) + Bounded : 57 (Average: 21.12 Max: 87 Sum: 1204 Ratio: 0.02%) + +Rules : 94613 (Original: 86518) +Atoms : 45936 +Bodies : 40692 (Original: 32596) + Count : 619 (Original: 1518) +Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) +Tight : Yes +Variables : 418169 (Eliminated: 8994 Frozen: 401645) +Constraints : 3098993 (Binary: 91.5% Ternary: 6.6% Other: 2.0%) + +Memory Peak : 609MB +Max. Length : 90 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 20.74s +Memory: 573MB (+22MB) +UNKNOWN +Iteration Time: 21.34s + +Iteration 38 +Queue: [(20,100,0,True), (21,105,0,True)] +Grounded Until: 95 +Expected Memory: 655.0MB +Grounding... [('step', [96]), ('step', [97]), ('step', [98]), ('step', [99]), ('step', [100]), ('check', [100])] +Grounding Time: 0.34s +Memory: 573MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 39 +Time : 622.153s (Solving: 602.52s 1st Model: 0.00s Unsat: 7.40s) +CPU Time : 622.340s + +Choices : 8085108 (Domain: 7948889) +Conflicts : 982843 (Analyzed: 982840) +Restarts : 3494 (Average: 281.29 Last: 208) +Model-Level : 212.0 +Problems : 39 (Average Length: 62.00 Splits: 0) +Lemmas : 982840 (Deleted: 933407) + Binary : 19431 (Ratio: 1.98%) + Ternary : 3289 (Ratio: 0.33%) + Conflict : 982840 (Average Length: 809.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 982840 (Average: 7.37 Max: 426 Sum: 7248294) + Executed : 982782 (Average: 7.37 Max: 426 Sum: 7246988 Ratio: 99.98%) + Bounded : 58 (Average: 22.52 Max: 102 Sum: 1306 Ratio: 0.02%) + +Rules : 94613 (Original: 86518) +Atoms : 45936 +Bodies : 40692 (Original: 32596) + Count : 619 (Original: 1518) +Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) +Tight : Yes +Variables : 440730 (Eliminated: 8994 Frozen: 424206) +Constraints : 3272018 (Binary: 91.5% Ternary: 6.6% Other: 2.0%) + +Memory Peak : 627MB +Max. Length : 95 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 17.39s +Memory: 626MB (+53MB) +UNKNOWN +Iteration Time: 18.04s + +Iteration 39 +Queue: [(21,105,0,True)] +Grounded Until: 100 +Expected Memory: 708.0MB +Grounding... [('step', [101]), ('step', [102]), ('step', [103]), ('step', [104]), ('step', [105]), ('check', [105])] +Grounding Time: 0.35s +Memory: 626MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 40 +Time : 640.838s (Solving: 620.15s 1st Model: 0.00s Unsat: 7.40s) +CPU Time : 641.032s + +Choices : 8299964 (Domain: 8163588) +Conflicts : 1011054 (Analyzed: 1011051) +Restarts : 3594 (Average: 281.32 Last: 208) +Model-Level : 212.0 +Problems : 40 (Average Length: 63.12 Splits: 0) +Lemmas : 1011051 (Deleted: 960990) + Binary : 19575 (Ratio: 1.94%) + Ternary : 3324 (Ratio: 0.33%) + Conflict : 1011051 (Average Length: 803.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 1011051 (Average: 7.35 Max: 426 Sum: 7430291) + Executed : 1010993 (Average: 7.35 Max: 426 Sum: 7428985 Ratio: 99.98%) + Bounded : 58 (Average: 22.52 Max: 102 Sum: 1306 Ratio: 0.02%) + +Rules : 94613 (Original: 86518) +Atoms : 45936 +Bodies : 40692 (Original: 32596) + Count : 619 (Original: 1518) +Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) +Tight : Yes +Variables : 463291 (Eliminated: 8994 Frozen: 446767) +Constraints : 3445029 (Binary: 91.5% Ternary: 6.6% Other: 2.0%) + +Memory Peak : 682MB +Max. Length : 100 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 18.04s +Memory: 629MB (+3MB) +UNKNOWN +Iteration Time: 18.70s + +Iteration 40 +Queue: [(4,20,3,True), (5,25,3,True), (6,30,3,True), (7,35,2,True), (8,40,2,True), (9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,2,False), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Blocking actions... +Solving... +[start: stats after solve call] + +Models : 0 +Calls : 41 +Time : 650.250s (Solving: 629.43s 1st Model: 0.00s Unsat: 16.67s) +CPU Time : 650.448s + +Choices : 8456222 (Domain: 8319846) +Conflicts : 1039175 (Analyzed: 1039171) +Restarts : 3693 (Average: 281.39 Last: 208) +Model-Level : 212.0 +Problems : 41 (Average Length: 64.20 Splits: 0) +Lemmas : 1039171 (Deleted: 988171) + Binary : 19785 (Ratio: 1.90%) + Ternary : 3407 (Ratio: 0.33%) + Conflict : 1039171 (Average Length: 789.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 1039171 (Average: 7.29 Max: 426 Sum: 7580351) + Executed : 1039111 (Average: 7.29 Max: 426 Sum: 7578937 Ratio: 99.98%) + Bounded : 60 (Average: 23.57 Max: 107 Sum: 1414 Ratio: 0.02%) + +Rules : 94613 (Original: 86518) +Atoms : 45936 +Bodies : 40692 (Original: 32596) + Count : 619 (Original: 1518) +Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) +Tight : Yes +Variables : 463291 (Eliminated: 8994 Frozen: 454297) +Constraints : 3445029 (Binary: 91.5% Ternary: 6.6% Other: 2.0%) + +Memory Peak : 682MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.36s +Memory: 629MB (+0MB) +UNSAT +Iteration Time: 9.42s + +Iteration 41 +Queue: [(5,25,3,True), (6,30,3,True), (7,35,2,True), (8,40,2,True), (9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,2,False), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 42 +Time : 675.013s (Solving: 654.09s 1st Model: 0.00s Unsat: 16.67s) +CPU Time : 675.224s + +Choices : 8601062 (Domain: 8464686) +Conflicts : 1067320 (Analyzed: 1067316) +Restarts : 3793 (Average: 281.39 Last: 208) +Model-Level : 212.0 +Problems : 42 (Average Length: 65.21 Splits: 0) +Lemmas : 1067316 (Deleted: 1015695) + Binary : 19938 (Ratio: 1.87%) + Ternary : 3428 (Ratio: 0.32%) + Conflict : 1067316 (Average Length: 793.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 1067316 (Average: 7.23 Max: 426 Sum: 7714494) + Executed : 1067255 (Average: 7.23 Max: 426 Sum: 7712973 Ratio: 99.98%) + Bounded : 61 (Average: 24.93 Max: 107 Sum: 1521 Ratio: 0.02%) + +Rules : 94613 (Original: 86518) +Atoms : 45936 +Bodies : 40692 (Original: 32596) + Count : 619 (Original: 1518) +Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) +Tight : Yes +Variables : 463291 (Eliminated: 8994 Frozen: 454297) +Constraints : 3445015 (Binary: 91.5% Ternary: 6.6% Other: 2.0%) + +Memory Peak : 682MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 24.74s +Memory: 629MB (+0MB) +UNKNOWN +Iteration Time: 24.78s + +Iteration 42 +Queue: [(6,30,3,True), (7,35,2,True), (8,40,2,True), (9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,2,False), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 43 +Time : 700.352s (Solving: 679.31s 1st Model: 0.00s Unsat: 16.67s) +CPU Time : 700.576s + +Choices : 8769209 (Domain: 8632833) +Conflicts : 1095491 (Analyzed: 1095487) +Restarts : 3893 (Average: 281.40 Last: 208) +Model-Level : 212.0 +Problems : 43 (Average Length: 66.19 Splits: 0) +Lemmas : 1095487 (Deleted: 1043519) + Binary : 20111 (Ratio: 1.84%) + Ternary : 3439 (Ratio: 0.31%) + Conflict : 1095487 (Average Length: 818.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 1095487 (Average: 7.18 Max: 426 Sum: 7864412) + Executed : 1095426 (Average: 7.18 Max: 426 Sum: 7862891 Ratio: 99.98%) + Bounded : 61 (Average: 24.93 Max: 107 Sum: 1521 Ratio: 0.02%) + +Rules : 94613 (Original: 86518) +Atoms : 45936 +Bodies : 40692 (Original: 32596) + Count : 619 (Original: 1518) +Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) +Tight : Yes +Variables : 463291 (Eliminated: 8994 Frozen: 454297) +Constraints : 3445001 (Binary: 91.5% Ternary: 6.6% Other: 2.0%) + +Memory Peak : 693MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 25.30s +Memory: 693MB (+64MB) +UNKNOWN +Iteration Time: 25.35s + +Iteration 43 +Queue: [(7,35,2,True), (8,40,2,True), (9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,2,False), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 44 +Time : 718.784s (Solving: 697.64s 1st Model: 0.00s Unsat: 16.67s) +CPU Time : 719.016s + +Choices : 8947892 (Domain: 8811516) +Conflicts : 1123688 (Analyzed: 1123684) +Restarts : 3993 (Average: 281.41 Last: 208) +Model-Level : 212.0 +Problems : 44 (Average Length: 67.11 Splits: 0) +Lemmas : 1123684 (Deleted: 1071211) + Binary : 20240 (Ratio: 1.80%) + Ternary : 3456 (Ratio: 0.31%) + Conflict : 1123684 (Average Length: 820.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 1123684 (Average: 7.14 Max: 426 Sum: 8021804) + Executed : 1123623 (Average: 7.14 Max: 426 Sum: 8020283 Ratio: 99.98%) + Bounded : 61 (Average: 24.93 Max: 107 Sum: 1521 Ratio: 0.02%) + +Rules : 94613 (Original: 86518) +Atoms : 45936 +Bodies : 40692 (Original: 32596) + Count : 619 (Original: 1518) +Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) +Tight : Yes +Variables : 463291 (Eliminated: 8994 Frozen: 454297) +Constraints : 3445001 (Binary: 91.5% Ternary: 6.6% Other: 2.0%) + +Memory Peak : 693MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 18.40s +Memory: 693MB (+0MB) +UNKNOWN +Iteration Time: 18.44s + +Iteration 44 +Queue: [(8,40,2,True), (9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,2,False), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 45 +Time : 736.806s (Solving: 715.53s 1st Model: 0.00s Unsat: 16.67s) +CPU Time : 737.048s + +Choices : 9151203 (Domain: 9014827) +Conflicts : 1151869 (Analyzed: 1151865) +Restarts : 4093 (Average: 281.42 Last: 208) +Model-Level : 212.0 +Problems : 45 (Average Length: 68.00 Splits: 0) +Lemmas : 1151865 (Deleted: 1098669) + Binary : 20406 (Ratio: 1.77%) + Ternary : 3501 (Ratio: 0.30%) + Conflict : 1151865 (Average Length: 819.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 1151865 (Average: 7.12 Max: 426 Sum: 8200967) + Executed : 1151804 (Average: 7.12 Max: 426 Sum: 8199446 Ratio: 99.98%) + Bounded : 61 (Average: 24.93 Max: 107 Sum: 1521 Ratio: 0.02%) + +Rules : 94613 (Original: 86518) +Atoms : 45936 +Bodies : 40692 (Original: 32596) + Count : 619 (Original: 1518) +Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) +Tight : Yes +Variables : 463291 (Eliminated: 8994 Frozen: 454297) +Constraints : 3445001 (Binary: 91.5% Ternary: 6.6% Other: 2.0%) + +Memory Peak : 693MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 17.98s +Memory: 693MB (+0MB) +UNKNOWN +Iteration Time: 18.03s + +Iteration 45 +Queue: [(9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,2,False), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 46 +Time : 754.954s (Solving: 733.57s 1st Model: 0.00s Unsat: 16.67s) +CPU Time : 755.204s + +Choices : 9352554 (Domain: 9215956) +Conflicts : 1180060 (Analyzed: 1180056) +Restarts : 4193 (Average: 281.43 Last: 208) +Model-Level : 212.0 +Problems : 46 (Average Length: 68.85 Splits: 0) +Lemmas : 1180056 (Deleted: 1126024) + Binary : 20672 (Ratio: 1.75%) + Ternary : 3546 (Ratio: 0.30%) + Conflict : 1180056 (Average Length: 820.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 1180056 (Average: 7.10 Max: 426 Sum: 8376547) + Executed : 1179995 (Average: 7.10 Max: 426 Sum: 8375026 Ratio: 99.98%) + Bounded : 61 (Average: 24.93 Max: 107 Sum: 1521 Ratio: 0.02%) + +Rules : 94613 (Original: 86518) +Atoms : 45936 +Bodies : 40692 (Original: 32596) + Count : 619 (Original: 1518) +Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) +Tight : Yes +Variables : 463291 (Eliminated: 8994 Frozen: 454297) +Constraints : 3445001 (Binary: 91.5% Ternary: 6.6% Other: 2.0%) + +Memory Peak : 693MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 18.12s +Memory: 693MB (+0MB) +UNKNOWN +Iteration Time: 18.16s + +Iteration 46 +Queue: [(10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,2,False), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 47 +Time : 772.790s (Solving: 751.28s 1st Model: 0.00s Unsat: 16.67s) +CPU Time : 773.048s + +Choices : 9572653 (Domain: 9435574) +Conflicts : 1208245 (Analyzed: 1208241) +Restarts : 4293 (Average: 281.44 Last: 208) +Model-Level : 212.0 +Problems : 47 (Average Length: 69.66 Splits: 0) +Lemmas : 1208241 (Deleted: 1153476) + Binary : 20930 (Ratio: 1.73%) + Ternary : 3599 (Ratio: 0.30%) + Conflict : 1208241 (Average Length: 823.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 1208241 (Average: 7.09 Max: 426 Sum: 8566212) + Executed : 1208180 (Average: 7.09 Max: 426 Sum: 8564691 Ratio: 99.98%) + Bounded : 61 (Average: 24.93 Max: 107 Sum: 1521 Ratio: 0.02%) + +Rules : 94613 (Original: 86518) +Atoms : 45936 +Bodies : 40692 (Original: 32596) + Count : 619 (Original: 1518) +Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) +Tight : Yes +Variables : 463291 (Eliminated: 8994 Frozen: 454297) +Constraints : 3445001 (Binary: 91.5% Ternary: 6.6% Other: 2.0%) + +Memory Peak : 693MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 17.79s +Memory: 693MB (+0MB) +UNKNOWN +Iteration Time: 17.85s + +Iteration 47 +Queue: [(11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,2,False), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 48 +Time : 790.010s (Solving: 768.37s 1st Model: 0.00s Unsat: 16.67s) +CPU Time : 790.276s + +Choices : 9786609 (Domain: 9649467) +Conflicts : 1236454 (Analyzed: 1236450) +Restarts : 4393 (Average: 281.46 Last: 208) +Model-Level : 212.0 +Problems : 48 (Average Length: 70.44 Splits: 0) +Lemmas : 1236450 (Deleted: 1181052) + Binary : 21219 (Ratio: 1.72%) + Ternary : 3640 (Ratio: 0.29%) + Conflict : 1236450 (Average Length: 824.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 1236450 (Average: 7.08 Max: 426 Sum: 8748483) + Executed : 1236389 (Average: 7.07 Max: 426 Sum: 8746962 Ratio: 99.98%) + Bounded : 61 (Average: 24.93 Max: 107 Sum: 1521 Ratio: 0.02%) + +Rules : 94613 (Original: 86518) +Atoms : 45936 +Bodies : 40692 (Original: 32596) + Count : 619 (Original: 1518) +Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) +Tight : Yes +Variables : 463291 (Eliminated: 8994 Frozen: 454297) +Constraints : 3445001 (Binary: 91.5% Ternary: 6.6% Other: 2.0%) + +Memory Peak : 693MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 17.18s +Memory: 693MB (+0MB) +UNKNOWN +Iteration Time: 17.23s + +Iteration 48 +Queue: [(12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,2,False), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 49 +Time : 806.202s (Solving: 784.44s 1st Model: 0.00s Unsat: 16.67s) +CPU Time : 806.472s + +Choices : 10026136 (Domain: 9888329) +Conflicts : 1264633 (Analyzed: 1264629) +Restarts : 4493 (Average: 281.47 Last: 208) +Model-Level : 212.0 +Problems : 49 (Average Length: 71.18 Splits: 0) +Lemmas : 1264629 (Deleted: 1208327) + Binary : 21668 (Ratio: 1.71%) + Ternary : 3674 (Ratio: 0.29%) + Conflict : 1264629 (Average Length: 824.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 1264629 (Average: 7.08 Max: 426 Sum: 8948813) + Executed : 1264568 (Average: 7.08 Max: 426 Sum: 8947292 Ratio: 99.98%) + Bounded : 61 (Average: 24.93 Max: 107 Sum: 1521 Ratio: 0.02%) + +Rules : 94613 (Original: 86518) +Atoms : 45936 +Bodies : 40692 (Original: 32596) + Count : 619 (Original: 1518) +Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) +Tight : Yes +Variables : 463291 (Eliminated: 8994 Frozen: 454297) +Constraints : 3445001 (Binary: 91.5% Ternary: 6.6% Other: 2.0%) + +Memory Peak : 693MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 16.15s +Memory: 693MB (+0MB) +UNKNOWN +Iteration Time: 16.20s + +Iteration 49 +Queue: [(13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,2,False), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 50 +Time : 823.151s (Solving: 801.27s 1st Model: 0.00s Unsat: 16.67s) +CPU Time : 823.428s + +Choices : 10216776 (Domain: 10078969) +Conflicts : 1292793 (Analyzed: 1292789) +Restarts : 4593 (Average: 281.47 Last: 208) +Model-Level : 212.0 +Problems : 50 (Average Length: 71.90 Splits: 0) +Lemmas : 1292789 (Deleted: 1235993) + Binary : 21766 (Ratio: 1.68%) + Ternary : 3686 (Ratio: 0.29%) + Conflict : 1292789 (Average Length: 824.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 1292789 (Average: 7.05 Max: 426 Sum: 9110026) + Executed : 1292728 (Average: 7.05 Max: 426 Sum: 9108505 Ratio: 99.98%) + Bounded : 61 (Average: 24.93 Max: 107 Sum: 1521 Ratio: 0.02%) + +Rules : 94613 (Original: 86518) +Atoms : 45936 +Bodies : 40692 (Original: 32596) + Count : 619 (Original: 1518) +Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) +Tight : Yes +Variables : 463291 (Eliminated: 8994 Frozen: 454297) +Constraints : 3445001 (Binary: 91.5% Ternary: 6.6% Other: 2.0%) + +Memory Peak : 693MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 16.91s +Memory: 693MB (+0MB) +UNKNOWN +Iteration Time: 16.96s + +Iteration 50 +Queue: [(18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 51 +Time : 843.238s (Solving: 821.23s 1st Model: 0.00s Unsat: 16.67s) +CPU Time : 843.524s + +Choices : 10496385 (Domain: 10358552) +Conflicts : 1320996 (Analyzed: 1320992) +Restarts : 4693 (Average: 281.48 Last: 208) +Model-Level : 212.0 +Problems : 51 (Average Length: 72.59 Splits: 0) +Lemmas : 1320992 (Deleted: 1263506) + Binary : 22044 (Ratio: 1.67%) + Ternary : 3737 (Ratio: 0.28%) + Conflict : 1320992 (Average Length: 826.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 1320992 (Average: 7.08 Max: 426 Sum: 9351586) + Executed : 1320931 (Average: 7.08 Max: 426 Sum: 9350065 Ratio: 99.98%) + Bounded : 61 (Average: 24.93 Max: 107 Sum: 1521 Ratio: 0.02%) + +Rules : 94613 (Original: 86518) +Atoms : 45936 +Bodies : 40692 (Original: 32596) + Count : 619 (Original: 1518) +Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) +Tight : Yes +Variables : 463291 (Eliminated: 8994 Frozen: 454297) +Constraints : 3445001 (Binary: 91.5% Ternary: 6.6% Other: 2.0%) + +Memory Peak : 693MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 20.05s +Memory: 693MB (+0MB) +UNKNOWN +Iteration Time: 20.10s + +Iteration 51 +Queue: [(19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 52 +Time : 862.265s (Solving: 840.15s 1st Model: 0.00s Unsat: 16.67s) +CPU Time : 862.560s + +Choices : 10764696 (Domain: 10626340) +Conflicts : 1349196 (Analyzed: 1349192) +Restarts : 4793 (Average: 281.49 Last: 208) +Model-Level : 212.0 +Problems : 52 (Average Length: 73.25 Splits: 0) +Lemmas : 1349192 (Deleted: 1291046) + Binary : 22249 (Ratio: 1.65%) + Ternary : 3767 (Ratio: 0.28%) + Conflict : 1349192 (Average Length: 828.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 1349192 (Average: 7.10 Max: 426 Sum: 9578947) + Executed : 1349131 (Average: 7.10 Max: 426 Sum: 9577426 Ratio: 99.98%) + Bounded : 61 (Average: 24.93 Max: 107 Sum: 1521 Ratio: 0.02%) + +Rules : 94613 (Original: 86518) +Atoms : 45936 +Bodies : 40692 (Original: 32596) + Count : 619 (Original: 1518) +Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) +Tight : Yes +Variables : 463291 (Eliminated: 8994 Frozen: 454297) +Constraints : 3445001 (Binary: 91.5% Ternary: 6.6% Other: 2.0%) + +Memory Peak : 693MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 19.00s +Memory: 693MB (+0MB) +UNKNOWN +Iteration Time: 19.04s + +Iteration 52 +Queue: [(20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 53 +Time : 883.700s (Solving: 861.48s 1st Model: 0.00s Unsat: 16.67s) +CPU Time : 884.004s + +Choices : 11013874 (Domain: 10875518) +Conflicts : 1377434 (Analyzed: 1377430) +Restarts : 4893 (Average: 281.51 Last: 208) +Model-Level : 212.0 +Problems : 53 (Average Length: 73.89 Splits: 0) +Lemmas : 1377430 (Deleted: 1318807) + Binary : 22405 (Ratio: 1.63%) + Ternary : 3804 (Ratio: 0.28%) + Conflict : 1377430 (Average Length: 834.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 1377430 (Average: 7.10 Max: 426 Sum: 9783579) + Executed : 1377369 (Average: 7.10 Max: 426 Sum: 9782058 Ratio: 99.98%) + Bounded : 61 (Average: 24.93 Max: 107 Sum: 1521 Ratio: 0.02%) + +Rules : 94613 (Original: 86518) +Atoms : 45936 +Bodies : 40692 (Original: 32596) + Count : 619 (Original: 1518) +Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) +Tight : Yes +Variables : 463291 (Eliminated: 8994 Frozen: 454297) +Constraints : 3445001 (Binary: 91.5% Ternary: 6.6% Other: 2.0%) + +Memory Peak : 693MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 21.41s +Memory: 693MB (+0MB) +UNKNOWN +Iteration Time: 21.45s + +Iteration 53 +Queue: [(21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +*** Info : (planner): INTERRUPTED by signal! +UNKNOWN + +INTERRUPTED : 1 + +Models : 0+ +Calls : 54 +Time : 894.855s (Solving: 872.53s 1st Model: 0.00s Unsat: 16.67s) +CPU Time : 895.144s + +Choices : 11145256 (Domain: 11006899) +Conflicts : 1391952 (Analyzed: 1391948) +Restarts : 4954 (Average: 280.97 Last: 208) +Model-Level : 212.0 +Problems : 54 (Average Length: 74.50 Splits: 0) +Lemmas : 1391948 (Deleted: 1335497) + Binary : 22457 (Ratio: 1.61%) + Ternary : 3815 (Ratio: 0.27%) + Conflict : 1391948 (Average Length: 833.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 1391948 (Average: 7.11 Max: 426 Sum: 9892370) + Executed : 1391887 (Average: 7.11 Max: 426 Sum: 9890849 Ratio: 99.98%) + Bounded : 61 (Average: 24.93 Max: 107 Sum: 1521 Ratio: 0.02%) + +Rules : 94613 (Original: 86518) +Atoms : 45936 +Bodies : 40692 (Original: 32596) + Count : 619 (Original: 1518) +Equivalences : 10271 (Atom=Atom: 62 Body=Body: 0 Other: 10209) +Tight : Yes +Variables : 463291 (Eliminated: 8994 Frozen: 454297) +Constraints : 3445001 (Binary: 91.5% Ternary: 6.6% Other: 2.0%) + +Memory Peak : 693MB +Max. Length : 105 steps +Models : 1 + +