From 8afb42770f882c8590aea20d7f0eeb9f5cd7acfb Mon Sep 17 00:00:00 2001 From: potassco-bot Date: Fri, 2 Feb 2018 10:20:11 +0100 Subject: [PATCH] Add benchmark result [gc-ta1-tt1 | ipc-2011 | barman-sequential-satisficing | 8] --- ...c-2011_barman-sequential-satisficing_8.env | 54 + ...c-2011_barman-sequential-satisficing_8.err | 8 + ...c-2011_barman-sequential-satisficing_8.out | 5583 +++++++++++++++++ 3 files changed, 5645 insertions(+) create mode 100644 gc-ta1-tt1/ipc-2011_barman-sequential-satisficing_8.env create mode 100644 gc-ta1-tt1/ipc-2011_barman-sequential-satisficing_8.err create mode 100644 gc-ta1-tt1/ipc-2011_barman-sequential-satisficing_8.out diff --git a/gc-ta1-tt1/ipc-2011_barman-sequential-satisficing_8.env b/gc-ta1-tt1/ipc-2011_barman-sequential-satisficing_8.env new file mode 100644 index 000000000..f912d20a0 --- /dev/null +++ b/gc-ta1-tt1/ipc-2011_barman-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/barman-sequential-satisficing/domain.pddl +- /home/pluehne/Documents/ASP/pddl-instances/ipc-2011/domains/barman-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: barman-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_barman-sequential-satisficing_8.err b/gc-ta1-tt1/ipc-2011_barman-sequential-satisficing_8.err new file mode 100644 index 000000000..ad9b8dd02 --- /dev/null +++ b/gc-ta1-tt1/ipc-2011_barman-sequential-satisficing_8.err @@ -0,0 +1,8 @@ +# configuration: {'id': 'gc-ta1-tt1', 'options': ['--stats', '--stats-iter', '--verbose', '--print-call', '-m 8192', '--translate', '-B 0.9', '--parallel=0', '--shallow', '--use-heuristic', '--test-until-not-sat', '--test=0', '--test-add=1', '--test-times=1'], 'instanceSets': ['rintanen-aij-2012-interesting']} +# instance: {'ipc': 'ipc-2011', 'domain': 'barman-sequential-satisficing', 'instance': 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/barman-sequential-satisficing/domain.pddl', '/home/pluehne/Documents/ASP/pddl-instances/ipc-2011/domains/barman-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 +TIMEOUT CPU 900.06 MEM 755804 MAXMEM 826200 STALE 0 MAXMEM_RSS 648044 + + diff --git a/gc-ta1-tt1/ipc-2011_barman-sequential-satisficing_8.out b/gc-ta1-tt1/ipc-2011_barman-sequential-satisficing_8.out new file mode 100644 index 000000000..360178ecb --- /dev/null +++ b/gc-ta1-tt1/ipc-2011_barman-sequential-satisficing_8.out @@ -0,0 +1,5583 @@ +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-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/barman-sequential-satisficing/domain.pddl /home/pluehne/Documents/ASP/pddl-instances/ipc-2011/domains/barman-sequential-satisficing/instances/instance-8.pddl +Parsing... +Parsing: [0.050s CPU, 0.048s wall-clock] +Normalizing task... [0.000s CPU, 0.004s wall-clock] +Instantiating... +Generating Datalog program... [0.020s CPU, 0.012s wall-clock] +Normalizing Datalog program... +Normalizing Datalog program: [0.060s CPU, 0.076s wall-clock] +Preparing model... [0.040s CPU, 0.038s wall-clock] +Generated 115 rules. +Computing model... [0.400s CPU, 0.403s wall-clock] +2300 relevant atoms +2393 auxiliary atoms +4693 final queue length +8087 total queue pushes +Completing instantiation... [0.680s CPU, 0.687s wall-clock] +Instantiating: [1.220s CPU, 1.221s wall-clock] +Computing fact groups... +Finding invariants... +24 initial candidates +Finding invariants: [0.110s CPU, 0.115s wall-clock] +Checking invariant weight... [0.000s CPU, 0.001s wall-clock] +Instantiating groups... [0.010s CPU, 0.007s wall-clock] +Collecting mutex groups... [0.000s CPU, 0.001s wall-clock] +Choosing groups... +238 uncovered facts +Choosing groups: [0.000s CPU, 0.001s wall-clock] +Building translation key... [0.000s CPU, 0.009s wall-clock] +Computing fact groups: [0.140s CPU, 0.151s wall-clock] +Building STRIPS to SAS dictionary... [0.010s 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.003s wall-clock] +Translating task... +Processing axioms... +Simplifying axioms... [0.000s CPU, 0.000s wall-clock] +Processing axioms: [0.040s CPU, 0.038s wall-clock] +Translating task: [0.740s CPU, 0.729s wall-clock] +2672 effect conditions simplified +0 implied preconditions added +Detecting unreachable propositions... +0 operators removed +0 axioms removed +3 propositions removed +Detecting unreachable propositions: [0.360s CPU, 0.358s wall-clock] +Reordering and filtering variables... +241 of 241 variables necessary. +12 of 15 mutex groups necessary. +1596 of 1596 operators necessary. +0 of 0 axiom rules necessary. +Reordering and filtering variables: [0.240s CPU, 0.242s wall-clock] +Translator variables: 241 +Translator derived variables: 0 +Translator facts: 505 +Translator goal facts: 10 +Translator mutex groups: 12 +Translator total mutex groups size: 36 +Translator operators: 1596 +Translator axioms: 0 +Translator task size: 15302 +Translator peak memory: 45004 KB +Writing output... [0.300s CPU, 0.327s wall-clock] +Done! [3.090s CPU, 3.118s wall-clock] +planner.py version 0.0.1 + +Time: 0.62s +Memory: 91MB + +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.729s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s) +CPU Time : 0.620s + +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 : 44183 +Atoms : 44183 +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 : 227MB +Max. Length : 0 steps +Models : 0 + +[endof: stats after solve call] +Solving Time: 0.00s +Memory: 163MB (+72MB) +UNSAT +Iteration Time: 0.01s + +Iteration 2 +Queue: [(1,5,0,True), (2,10,0,True), (3,15,0,True), (4,20,0,True), (5,25,0,True), (6,30,0,True)] +Grounded Until: 0 +Expected Memory: 163MB +Grounding... [('step', [1]), ('step', [2]), ('step', [3]), ('step', [4]), ('step', [5]), ('check', [5])] +Grounding Time: 0.19s +Memory: 163MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 1+ +Calls : 2 +Time : 1.023s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s) +CPU Time : 0.912s + +Choices : 533 (Domain: 28) +Conflicts : 10 (Analyzed: 10) +Restarts : 0 +Model-Level : 115.0 +Problems : 2 (Average Length: 4.50 Splits: 0) +Lemmas : 10 (Deleted: 0) + Binary : 8 (Ratio: 80.00%) + Ternary : 0 (Ratio: 0.00%) + Conflict : 10 (Average Length: 8.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 10 (Average: 42.80 Max: 85 Sum: 428) + Executed : 7 (Average: 42.50 Max: 85 Sum: 425 Ratio: 99.30%) + Bounded : 3 (Average: 1.00 Max: 1 Sum: 3 Ratio: 0.70%) + +Rules : 44183 +Atoms : 44183 +Bodies : 1 (Original: 0) +Tight : Yes +Variables : 11842 (Eliminated: 0 Frozen: 130) +Constraints : 40811 (Binary: 95.1% Ternary: 3.4% Other: 1.4%) + +Memory Peak : 227MB +Max. Length : 0 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 0.02s +Memory: 165MB (+2MB) +SAT +Testing... +NOT SERIALIZABLE +Testing Time: 0.62s +Memory: 188MB (+23MB) +Solving... +[start: stats after solve call] + +Models : 0 +Calls : 3 +Time : 1.121s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s) +CPU Time : 1.012s + +Choices : 534 (Domain: 28) +Conflicts : 12 (Analyzed: 11) +Restarts : 0 +Model-Level : 115.0 +Problems : 3 (Average Length: 5.33 Splits: 0) +Lemmas : 11 (Deleted: 0) + Binary : 9 (Ratio: 81.82%) + Ternary : 0 (Ratio: 0.00%) + Conflict : 11 (Average Length: 7.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 11 (Average: 39.09 Max: 85 Sum: 430) + Executed : 7 (Average: 38.73 Max: 85 Sum: 426 Ratio: 99.07%) + Bounded : 4 (Average: 1.00 Max: 1 Sum: 4 Ratio: 0.93%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 14564 (Eliminated: 0 Frozen: 3202) +Constraints : 60980 (Binary: 92.3% Ternary: 5.5% Other: 2.3%) + +Memory Peak : 227MB +Max. Length : 0 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 0.01s +Memory: 188MB (+0MB) +UNSAT +Iteration Time: 0.93s + +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: 190.0MB +Grounding... [('step', [6]), ('step', [7]), ('step', [8]), ('step', [9]), ('step', [10]), ('check', [10])] +Grounding Time: 0.34s +Memory: 188MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0 +Calls : 4 +Time : 2.257s (Solving: 0.65s 1st Model: 0.00s Unsat: 0.65s) +CPU Time : 2.148s + +Choices : 18178 (Domain: 16746) +Conflicts : 2193 (Analyzed: 2191) +Restarts : 24 (Average: 91.29 Last: 10) +Model-Level : 115.0 +Problems : 4 (Average Length: 7.00 Splits: 0) +Lemmas : 2191 (Deleted: 707) + Binary : 321 (Ratio: 14.65%) + Ternary : 219 (Ratio: 10.00%) + Conflict : 2191 (Average Length: 46.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 2191 (Average: 8.34 Max: 98 Sum: 18275) + Executed : 2156 (Average: 8.17 Max: 98 Sum: 17910 Ratio: 98.00%) + Bounded : 35 (Average: 10.43 Max: 12 Sum: 365 Ratio: 2.00%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 40960 (Eliminated: 0 Frozen: 11742) +Constraints : 262050 (Binary: 91.6% Ternary: 6.4% Other: 1.9%) + +Memory Peak : 227MB +Max. Length : 5 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 0.67s +Memory: 197MB (+9MB) +UNSAT +Iteration Time: 1.14s + +Iteration 4 +Queue: [(3,15,0,True), (4,20,0,True), (5,25,0,True), (6,30,0,True)] +Grounded Until: 10 +Expected Memory: 206.0MB +Grounding... [('step', [11]), ('step', [12]), ('step', [13]), ('step', [14]), ('step', [15]), ('check', [15])] +Grounding Time: 0.39s +Memory: 204MB (+7MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 5 +Time : 5.360s (Solving: 3.19s 1st Model: 0.00s Unsat: 0.65s) +CPU Time : 5.252s + +Choices : 102837 (Domain: 99024) +Conflicts : 10268 (Analyzed: 10266) +Restarts : 124 (Average: 82.79 Last: 76) +Model-Level : 115.0 +Problems : 5 (Average Length: 9.00 Splits: 0) +Lemmas : 10266 (Deleted: 5160) + Binary : 907 (Ratio: 8.83%) + Ternary : 376 (Ratio: 3.66%) + Conflict : 10266 (Average Length: 150.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 10266 (Average: 9.81 Max: 122 Sum: 100680) + Executed : 10196 (Average: 9.72 Max: 122 Sum: 99742 Ratio: 99.07%) + Bounded : 70 (Average: 13.40 Max: 17 Sum: 938 Ratio: 0.93%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 67356 (Eliminated: 0 Frozen: 20282) +Constraints : 430122 (Binary: 91.6% Ternary: 6.4% Other: 2.0%) + +Memory Peak : 227MB +Max. Length : 10 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 2.56s +Memory: 216MB (+12MB) +UNKNOWN +Iteration Time: 3.11s + +Iteration 5 +Queue: [(4,20,0,True), (5,25,0,True), (6,30,0,True)] +Grounded Until: 15 +Expected Memory: 235.0MB +Grounding... [('step', [16]), ('step', [17]), ('step', [18]), ('step', [19]), ('step', [20]), ('check', [20])] +Grounding Time: 0.36s +Memory: 223MB (+7MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 6 +Time : 9.895s (Solving: 7.17s 1st Model: 0.00s Unsat: 0.65s) +CPU Time : 9.788s + +Choices : 206672 (Domain: 193750) +Conflicts : 19379 (Analyzed: 19377) +Restarts : 224 (Average: 86.50 Last: 83) +Model-Level : 115.0 +Problems : 6 (Average Length: 11.17 Splits: 0) +Lemmas : 19377 (Deleted: 12371) + Binary : 1729 (Ratio: 8.92%) + Ternary : 772 (Ratio: 3.98%) + Conflict : 19377 (Average Length: 185.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 19377 (Average: 10.28 Max: 242 Sum: 199184) + Executed : 19300 (Average: 10.22 Max: 242 Sum: 198104 Ratio: 99.46%) + Bounded : 77 (Average: 14.03 Max: 22 Sum: 1080 Ratio: 0.54%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 93752 (Eliminated: 0 Frozen: 28822) +Constraints : 606556 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) + +Memory Peak : 239MB +Max. Length : 15 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 4.02s +Memory: 239MB (+16MB) +UNKNOWN +Iteration Time: 4.55s + +Iteration 6 +Queue: [(5,25,0,True), (6,30,0,True)] +Grounded Until: 20 +Expected Memory: 262.0MB +Grounding... [('step', [21]), ('step', [22]), ('step', [23]), ('step', [24]), ('step', [25]), ('check', [25])] +Grounding Time: 0.42s +Memory: 244MB (+5MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 7 +Time : 15.418s (Solving: 12.06s 1st Model: 0.00s Unsat: 0.65s) +CPU Time : 15.316s + +Choices : 272499 (Domain: 252610) +Conflicts : 27782 (Analyzed: 27780) +Restarts : 324 (Average: 85.74 Last: 83) +Model-Level : 115.0 +Problems : 7 (Average Length: 13.43 Splits: 0) +Lemmas : 27780 (Deleted: 18655) + Binary : 1983 (Ratio: 7.14%) + Ternary : 897 (Ratio: 3.23%) + Conflict : 27780 (Average Length: 273.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 27780 (Average: 9.26 Max: 242 Sum: 257237) + Executed : 27702 (Average: 9.22 Max: 242 Sum: 256136 Ratio: 99.57%) + Bounded : 78 (Average: 14.12 Max: 22 Sum: 1101 Ratio: 0.43%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 120148 (Eliminated: 0 Frozen: 37362) +Constraints : 807584 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) + +Memory Peak : 262MB +Max. Length : 20 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 4.93s +Memory: 253MB (+9MB) +UNKNOWN +Iteration Time: 5.53s + +Iteration 7 +Queue: [(6,30,0,True)] +Grounded Until: 25 +Expected Memory: 276.0MB +Grounding... [('step', [26]), ('step', [27]), ('step', [28]), ('step', [29]), ('step', [30]), ('check', [30])] +Grounding Time: 0.47s +Memory: 267MB (+14MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 8 +Time : 22.306s (Solving: 18.26s 1st Model: 0.00s Unsat: 0.65s) +CPU Time : 22.204s + +Choices : 390496 (Domain: 363376) +Conflicts : 36726 (Analyzed: 36724) +Restarts : 424 (Average: 86.61 Last: 83) +Model-Level : 115.0 +Problems : 8 (Average Length: 15.75 Splits: 0) +Lemmas : 36724 (Deleted: 27296) + Binary : 2472 (Ratio: 6.73%) + Ternary : 1065 (Ratio: 2.90%) + Conflict : 36724 (Average Length: 288.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 36724 (Average: 9.91 Max: 314 Sum: 364028) + Executed : 36645 (Average: 9.88 Max: 314 Sum: 362895 Ratio: 99.69%) + Bounded : 79 (Average: 14.34 Max: 32 Sum: 1133 Ratio: 0.31%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 146544 (Eliminated: 0 Frozen: 45902) +Constraints : 1008654 (Binary: 91.5% Ternary: 6.6% Other: 1.9%) + +Memory Peak : 290MB +Max. Length : 25 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.24s +Memory: 290MB (+23MB) +UNKNOWN +Iteration Time: 6.90s + +Iteration 8 +Queue: [(3,15,1,True), (4,20,1,True), (5,25,1,True), (6,30,1,True), (7,35,0,True), (8,40,0,True), (9,45,0,True), (10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True)] +Grounded Until: 30 +Blocking actions... +Solving... +[start: stats after solve call] + +Models : 0 +Calls : 9 +Time : 22.755s (Solving: 18.68s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 22.652s + +Choices : 400612 (Domain: 370530) +Conflicts : 37677 (Analyzed: 37674) +Restarts : 436 (Average: 86.41 Last: 83) +Model-Level : 115.0 +Problems : 9 (Average Length: 17.56 Splits: 0) +Lemmas : 37674 (Deleted: 27296) + Binary : 2559 (Ratio: 6.79%) + Ternary : 1083 (Ratio: 2.87%) + Conflict : 37674 (Average Length: 284.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 37674 (Average: 9.93 Max: 314 Sum: 373999) + Executed : 37594 (Average: 9.90 Max: 314 Sum: 372865 Ratio: 99.70%) + Bounded : 80 (Average: 14.18 Max: 32 Sum: 1134 Ratio: 0.30%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 146544 (Eliminated: 0 Frozen: 45902) +Constraints : 1008640 (Binary: 91.5% Ternary: 6.6% Other: 1.9%) + +Memory Peak : 290MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 0.44s +Memory: 290MB (+0MB) +UNSAT +Iteration Time: 0.45s + +Iteration 9 +Queue: [(4,20,1,True), (5,25,1,True), (6,30,1,True), (7,35,0,True), (8,40,0,True), (9,45,0,True), (10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True)] +Grounded Until: 30 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 10 +Time : 29.515s (Solving: 25.40s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 29.412s + +Choices : 477025 (Domain: 444470) +Conflicts : 46459 (Analyzed: 46456) +Restarts : 536 (Average: 86.67 Last: 119) +Model-Level : 115.0 +Problems : 10 (Average Length: 19.00 Splits: 0) +Lemmas : 46456 (Deleted: 35604) + Binary : 2782 (Ratio: 5.99%) + Ternary : 1173 (Ratio: 2.52%) + Conflict : 46456 (Average Length: 295.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 46456 (Average: 9.64 Max: 314 Sum: 447818) + Executed : 46373 (Average: 9.61 Max: 314 Sum: 446619 Ratio: 99.73%) + Bounded : 83 (Average: 14.45 Max: 32 Sum: 1199 Ratio: 0.27%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 146544 (Eliminated: 0 Frozen: 45902) +Constraints : 1008640 (Binary: 91.5% Ternary: 6.6% Other: 1.9%) + +Memory Peak : 290MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.75s +Memory: 290MB (+0MB) +UNKNOWN +Iteration Time: 6.76s + +Iteration 10 +Queue: [(5,25,1,True), (6,30,1,True), (7,35,0,True), (8,40,0,True), (9,45,0,True), (10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True)] +Grounded Until: 30 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 11 +Time : 35.146s (Solving: 31.00s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 35.044s + +Choices : 548045 (Domain: 512216) +Conflicts : 55487 (Analyzed: 55484) +Restarts : 636 (Average: 87.24 Last: 119) +Model-Level : 115.0 +Problems : 11 (Average Length: 20.18 Splits: 0) +Lemmas : 55484 (Deleted: 43513) + Binary : 3046 (Ratio: 5.49%) + Ternary : 1327 (Ratio: 2.39%) + Conflict : 55484 (Average Length: 296.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 55484 (Average: 9.22 Max: 314 Sum: 511584) + Executed : 55399 (Average: 9.20 Max: 314 Sum: 510321 Ratio: 99.75%) + Bounded : 85 (Average: 14.86 Max: 32 Sum: 1263 Ratio: 0.25%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 146544 (Eliminated: 0 Frozen: 45902) +Constraints : 1008612 (Binary: 91.5% Ternary: 6.6% Other: 1.9%) + +Memory Peak : 290MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 5.62s +Memory: 290MB (+0MB) +UNKNOWN +Iteration Time: 5.64s + +Iteration 11 +Queue: [(6,30,1,True), (7,35,0,True), (8,40,0,True), (9,45,0,True), (10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True)] +Grounded Until: 30 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 12 +Time : 41.556s (Solving: 37.37s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 41.456s + +Choices : 627807 (Domain: 586947) +Conflicts : 64123 (Analyzed: 64120) +Restarts : 736 (Average: 87.12 Last: 119) +Model-Level : 115.0 +Problems : 12 (Average Length: 21.17 Splits: 0) +Lemmas : 64120 (Deleted: 51571) + Binary : 3341 (Ratio: 5.21%) + Ternary : 1454 (Ratio: 2.27%) + Conflict : 64120 (Average Length: 311.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 64120 (Average: 9.07 Max: 318 Sum: 581841) + Executed : 64034 (Average: 9.05 Max: 318 Sum: 580549 Ratio: 99.78%) + Bounded : 86 (Average: 15.02 Max: 32 Sum: 1292 Ratio: 0.22%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 146544 (Eliminated: 0 Frozen: 45902) +Constraints : 1008587 (Binary: 91.5% Ternary: 6.6% Other: 1.9%) + +Memory Peak : 290MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.40s +Memory: 290MB (+0MB) +UNKNOWN +Iteration Time: 6.42s + +Iteration 12 +Queue: [(7,35,0,True), (8,40,0,True), (9,45,0,True), (10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True)] +Grounded Until: 30 +Expected Memory: 327.0MB +Grounding... [('step', [31]), ('step', [32]), ('step', [33]), ('step', [34]), ('step', [35]), ('check', [35])] +Grounding Time: 0.41s +Memory: 290MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 13 +Time : 49.893s (Solving: 45.05s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 49.796s + +Choices : 735324 (Domain: 690298) +Conflicts : 72686 (Analyzed: 72683) +Restarts : 836 (Average: 86.94 Last: 119) +Model-Level : 115.0 +Problems : 13 (Average Length: 22.38 Splits: 0) +Lemmas : 72683 (Deleted: 57530) + Binary : 3696 (Ratio: 5.09%) + Ternary : 1524 (Ratio: 2.10%) + Conflict : 72683 (Average Length: 359.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 72683 (Average: 9.29 Max: 318 Sum: 675314) + Executed : 72595 (Average: 9.27 Max: 318 Sum: 673953 Ratio: 99.80%) + Bounded : 88 (Average: 15.47 Max: 35 Sum: 1361 Ratio: 0.20%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 172940 (Eliminated: 0 Frozen: 54442) +Constraints : 1209657 (Binary: 91.5% Ternary: 6.6% Other: 1.9%) + +Memory Peak : 315MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.73s +Memory: 300MB (+10MB) +UNKNOWN +Iteration Time: 8.35s + +Iteration 13 +Queue: [(8,40,0,True), (9,45,0,True), (10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True)] +Grounded Until: 35 +Expected Memory: 337.0MB +Grounding... [('step', [36]), ('step', [37]), ('step', [38]), ('step', [39]), ('step', [40]), ('check', [40])] +Grounding Time: 0.38s +Memory: 307MB (+7MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 14 +Time : 57.448s (Solving: 51.96s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 57.352s + +Choices : 860682 (Domain: 808718) +Conflicts : 81209 (Analyzed: 81206) +Restarts : 936 (Average: 86.76 Last: 119) +Model-Level : 115.0 +Problems : 14 (Average Length: 23.79 Splits: 0) +Lemmas : 81206 (Deleted: 66260) + Binary : 3965 (Ratio: 4.88%) + Ternary : 1587 (Ratio: 1.95%) + Conflict : 81206 (Average Length: 411.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 81206 (Average: 9.62 Max: 318 Sum: 781288) + Executed : 81118 (Average: 9.60 Max: 318 Sum: 779927 Ratio: 99.83%) + Bounded : 88 (Average: 15.47 Max: 35 Sum: 1361 Ratio: 0.17%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 199336 (Eliminated: 0 Frozen: 62982) +Constraints : 1410727 (Binary: 91.5% Ternary: 6.6% Other: 1.9%) + +Memory Peak : 337MB +Max. Length : 35 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.97s +Memory: 319MB (+12MB) +UNKNOWN +Iteration Time: 7.57s + +Iteration 14 +Queue: [(9,45,0,True), (10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True)] +Grounded Until: 40 +Expected Memory: 356.0MB +Grounding... [('step', [41]), ('step', [42]), ('step', [43]), ('step', [44]), ('step', [45]), ('check', [45])] +Grounding Time: 0.37s +Memory: 325MB (+6MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 15 +Time : 63.955s (Solving: 57.82s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 63.864s + +Choices : 950001 (Domain: 897227) +Conflicts : 89808 (Analyzed: 89805) +Restarts : 1036 (Average: 86.68 Last: 119) +Model-Level : 115.0 +Problems : 15 (Average Length: 25.33 Splits: 0) +Lemmas : 89805 (Deleted: 73318) + Binary : 4104 (Ratio: 4.57%) + Ternary : 1628 (Ratio: 1.81%) + Conflict : 89805 (Average Length: 400.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 89805 (Average: 9.60 Max: 343 Sum: 861799) + Executed : 89715 (Average: 9.58 Max: 343 Sum: 860347 Ratio: 99.83%) + Bounded : 90 (Average: 16.13 Max: 47 Sum: 1452 Ratio: 0.17%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 225732 (Eliminated: 0 Frozen: 71522) +Constraints : 1611797 (Binary: 91.5% Ternary: 6.6% Other: 1.9%) + +Memory Peak : 358MB +Max. Length : 40 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 5.91s +Memory: 353MB (+28MB) +UNKNOWN +Iteration Time: 6.52s + +Iteration 15 +Queue: [(10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True)] +Grounded Until: 45 +Expected Memory: 390.0MB +Grounding... [('step', [46]), ('step', [47]), ('step', [48]), ('step', [49]), ('step', [50]), ('check', [50])] +Grounding Time: 0.37s +Memory: 353MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 16 +Time : 70.860s (Solving: 64.07s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 70.772s + +Choices : 1077851 (Domain: 1023155) +Conflicts : 98364 (Analyzed: 98361) +Restarts : 1136 (Average: 86.59 Last: 119) +Model-Level : 115.0 +Problems : 16 (Average Length: 27.00 Splits: 0) +Lemmas : 98361 (Deleted: 81342) + Binary : 4366 (Ratio: 4.44%) + Ternary : 1760 (Ratio: 1.79%) + Conflict : 98361 (Average Length: 387.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 98361 (Average: 9.95 Max: 470 Sum: 978949) + Executed : 98268 (Average: 9.94 Max: 470 Sum: 977349 Ratio: 99.84%) + Bounded : 93 (Average: 17.20 Max: 51 Sum: 1600 Ratio: 0.16%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 252128 (Eliminated: 0 Frozen: 80062) +Constraints : 1812853 (Binary: 91.5% Ternary: 6.6% Other: 1.9%) + +Memory Peak : 386MB +Max. Length : 45 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.31s +Memory: 361MB (+8MB) +UNKNOWN +Iteration Time: 6.92s + +Iteration 16 +Queue: [(11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True)] +Grounded Until: 50 +Expected Memory: 398.0MB +Grounding... [('step', [51]), ('step', [52]), ('step', [53]), ('step', [54]), ('step', [55]), ('check', [55])] +Grounding Time: 0.38s +Memory: 366MB (+5MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 17 +Time : 80.249s (Solving: 72.78s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 80.164s + +Choices : 1263652 (Domain: 1206883) +Conflicts : 107513 (Analyzed: 107510) +Restarts : 1236 (Average: 86.98 Last: 119) +Model-Level : 115.0 +Problems : 17 (Average Length: 28.76 Splits: 0) +Lemmas : 107510 (Deleted: 91143) + Binary : 4636 (Ratio: 4.31%) + Ternary : 1826 (Ratio: 1.70%) + Conflict : 107510 (Average Length: 385.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 107510 (Average: 10.71 Max: 487 Sum: 1151165) + Executed : 107415 (Average: 10.69 Max: 487 Sum: 1149453 Ratio: 99.85%) + Bounded : 95 (Average: 18.02 Max: 57 Sum: 1712 Ratio: 0.15%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 278524 (Eliminated: 0 Frozen: 88602) +Constraints : 2013923 (Binary: 91.5% Ternary: 6.6% Other: 1.9%) + +Memory Peak : 409MB +Max. Length : 50 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.78s +Memory: 380MB (+14MB) +UNKNOWN +Iteration Time: 9.40s + +Iteration 17 +Queue: [(12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True)] +Grounded Until: 55 +Expected Memory: 417.0MB +Grounding... [('step', [56]), ('step', [57]), ('step', [58]), ('step', [59]), ('step', [60]), ('check', [60])] +Grounding Time: 0.38s +Memory: 382MB (+2MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 18 +Time : 90.868s (Solving: 82.71s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 90.788s + +Choices : 1494412 (Domain: 1430437) +Conflicts : 116762 (Analyzed: 116759) +Restarts : 1336 (Average: 87.39 Last: 119) +Model-Level : 115.0 +Problems : 18 (Average Length: 30.61 Splits: 0) +Lemmas : 116759 (Deleted: 99482) + Binary : 4965 (Ratio: 4.25%) + Ternary : 1908 (Ratio: 1.63%) + Conflict : 116759 (Average Length: 426.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 116759 (Average: 11.61 Max: 512 Sum: 1356002) + Executed : 116664 (Average: 11.60 Max: 512 Sum: 1354290 Ratio: 99.87%) + Bounded : 95 (Average: 18.02 Max: 57 Sum: 1712 Ratio: 0.13%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 304920 (Eliminated: 0 Frozen: 97142) +Constraints : 2214979 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 428MB +Max. Length : 55 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 10.00s +Memory: 399MB (+17MB) +UNKNOWN +Iteration Time: 10.63s + +Iteration 18 +Queue: [(13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True)] +Grounded Until: 60 +Expected Memory: 436.0MB +Grounding... [('step', [61]), ('step', [62]), ('step', [63]), ('step', [64]), ('step', [65]), ('check', [65])] +Grounding Time: 0.39s +Memory: 403MB (+4MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 19 +Time : 100.228s (Solving: 91.34s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 100.144s + +Choices : 1694612 (Domain: 1629189) +Conflicts : 125781 (Analyzed: 125778) +Restarts : 1436 (Average: 87.59 Last: 140) +Model-Level : 115.0 +Problems : 19 (Average Length: 32.53 Splits: 0) +Lemmas : 125778 (Deleted: 108197) + Binary : 5250 (Ratio: 4.17%) + Ternary : 1967 (Ratio: 1.56%) + Conflict : 125778 (Average Length: 426.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 125778 (Average: 12.24 Max: 512 Sum: 1540099) + Executed : 125682 (Average: 12.23 Max: 512 Sum: 1538322 Ratio: 99.88%) + Bounded : 96 (Average: 18.51 Max: 65 Sum: 1777 Ratio: 0.12%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 331316 (Eliminated: 0 Frozen: 105682) +Constraints : 2416049 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 449MB +Max. Length : 60 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.71s +Memory: 447MB (+44MB) +UNKNOWN +Iteration Time: 9.37s + +Iteration 19 +Queue: [(14,70,0,True), (15,75,0,True), (16,80,0,True)] +Grounded Until: 65 +Expected Memory: 495.0MB +Grounding... [('step', [66]), ('step', [67]), ('step', [68]), ('step', [69]), ('step', [70]), ('check', [70])] +Grounding Time: 0.54s +Memory: 459MB (+12MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 20 +Time : 108.962s (Solving: 99.18s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 108.880s + +Choices : 1870137 (Domain: 1803025) +Conflicts : 134463 (Analyzed: 134460) +Restarts : 1536 (Average: 87.54 Last: 140) +Model-Level : 115.0 +Problems : 20 (Average Length: 34.50 Splits: 0) +Lemmas : 134460 (Deleted: 116693) + Binary : 5414 (Ratio: 4.03%) + Ternary : 1994 (Ratio: 1.48%) + Conflict : 134460 (Average Length: 438.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 134460 (Average: 12.61 Max: 663 Sum: 1695217) + Executed : 134363 (Average: 12.59 Max: 663 Sum: 1693368 Ratio: 99.89%) + Bounded : 97 (Average: 19.06 Max: 72 Sum: 1849 Ratio: 0.11%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 357712 (Eliminated: 0 Frozen: 114222) +Constraints : 2617119 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 503MB +Max. Length : 65 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.92s +Memory: 462MB (+3MB) +UNKNOWN +Iteration Time: 8.75s + +Iteration 20 +Queue: [(15,75,0,True), (16,80,0,True)] +Grounded Until: 70 +Expected Memory: 510.0MB +Grounding... [('step', [71]), ('step', [72]), ('step', [73]), ('step', [74]), ('step', [75]), ('check', [75])] +Grounding Time: 0.38s +Memory: 462MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 21 +Time : 119.140s (Solving: 108.62s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 119.064s + +Choices : 2039124 (Domain: 1970627) +Conflicts : 143078 (Analyzed: 143075) +Restarts : 1636 (Average: 87.45 Last: 140) +Model-Level : 115.0 +Problems : 21 (Average Length: 36.52 Splits: 0) +Lemmas : 143075 (Deleted: 125341) + Binary : 5594 (Ratio: 3.91%) + Ternary : 2046 (Ratio: 1.43%) + Conflict : 143075 (Average Length: 495.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 143075 (Average: 12.84 Max: 663 Sum: 1837672) + Executed : 142978 (Average: 12.83 Max: 663 Sum: 1835823 Ratio: 99.90%) + Bounded : 97 (Average: 19.06 Max: 72 Sum: 1849 Ratio: 0.10%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 384108 (Eliminated: 0 Frozen: 122762) +Constraints : 2818175 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 517MB +Max. Length : 70 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.52s +Memory: 476MB (+14MB) +UNKNOWN +Iteration Time: 10.19s + +Iteration 21 +Queue: [(16,80,0,True)] +Grounded Until: 75 +Expected Memory: 524.0MB +Grounding... [('step', [76]), ('step', [77]), ('step', [78]), ('step', [79]), ('step', [80]), ('check', [80])] +Grounding Time: 0.41s +Memory: 478MB (+2MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 22 +Time : 126.975s (Solving: 115.66s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 126.904s + +Choices : 2185071 (Domain: 2115747) +Conflicts : 151394 (Analyzed: 151391) +Restarts : 1736 (Average: 87.21 Last: 140) +Model-Level : 115.0 +Problems : 22 (Average Length: 38.59 Splits: 0) +Lemmas : 151391 (Deleted: 131099) + Binary : 5727 (Ratio: 3.78%) + Ternary : 2073 (Ratio: 1.37%) + Conflict : 151391 (Average Length: 500.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 151391 (Average: 12.99 Max: 663 Sum: 1965948) + Executed : 151294 (Average: 12.97 Max: 663 Sum: 1964099 Ratio: 99.91%) + Bounded : 97 (Average: 19.06 Max: 72 Sum: 1849 Ratio: 0.09%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 410504 (Eliminated: 0 Frozen: 131302) +Constraints : 3019245 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 536MB +Max. Length : 75 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.13s +Memory: 497MB (+19MB) +UNKNOWN +Iteration Time: 7.85s + +Iteration 22 +Queue: [(4,20,2,True), (5,25,2,True), (6,30,2,True), (7,35,1,True), (8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 80 +Blocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 23 +Time : 133.263s (Solving: 121.85s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 133.192s + +Choices : 2261957 (Domain: 2192633) +Conflicts : 159520 (Analyzed: 159517) +Restarts : 1836 (Average: 86.88 Last: 140) +Model-Level : 115.0 +Problems : 23 (Average Length: 40.48 Splits: 0) +Lemmas : 159517 (Deleted: 138996) + Binary : 5859 (Ratio: 3.67%) + Ternary : 2097 (Ratio: 1.31%) + Conflict : 159517 (Average Length: 491.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 159517 (Average: 12.78 Max: 663 Sum: 2039122) + Executed : 159419 (Average: 12.77 Max: 663 Sum: 2037191 Ratio: 99.91%) + Bounded : 98 (Average: 19.70 Max: 82 Sum: 1931 Ratio: 0.09%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 410504 (Eliminated: 0 Frozen: 131302) +Constraints : 3019245 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 536MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.25s +Memory: 497MB (+0MB) +UNKNOWN +Iteration Time: 6.29s + +Iteration 23 +Queue: [(5,25,2,True), (6,30,2,True), (7,35,1,True), (8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 80 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 24 +Time : 138.467s (Solving: 126.97s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 138.400s + +Choices : 2314613 (Domain: 2243718) +Conflicts : 168202 (Analyzed: 168199) +Restarts : 1936 (Average: 86.88 Last: 140) +Model-Level : 115.0 +Problems : 24 (Average Length: 42.21 Splits: 0) +Lemmas : 168199 (Deleted: 148792) + Binary : 5944 (Ratio: 3.53%) + Ternary : 2136 (Ratio: 1.27%) + Conflict : 168199 (Average Length: 487.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 168199 (Average: 12.40 Max: 663 Sum: 2085351) + Executed : 168098 (Average: 12.39 Max: 663 Sum: 2083178 Ratio: 99.90%) + Bounded : 101 (Average: 21.51 Max: 82 Sum: 2173 Ratio: 0.10%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 410504 (Eliminated: 0 Frozen: 131302) +Constraints : 3019232 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 536MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 5.17s +Memory: 497MB (+0MB) +UNKNOWN +Iteration Time: 5.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,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 80 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 25 +Time : 145.493s (Solving: 133.91s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 145.432s + +Choices : 2392472 (Domain: 2320880) +Conflicts : 177307 (Analyzed: 177304) +Restarts : 2036 (Average: 87.08 Last: 140) +Model-Level : 115.0 +Problems : 25 (Average Length: 43.80 Splits: 0) +Lemmas : 177304 (Deleted: 156963) + Binary : 6100 (Ratio: 3.44%) + Ternary : 2181 (Ratio: 1.23%) + Conflict : 177304 (Average Length: 490.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 177304 (Average: 12.12 Max: 663 Sum: 2149269) + Executed : 177203 (Average: 12.11 Max: 663 Sum: 2147096 Ratio: 99.90%) + Bounded : 101 (Average: 21.51 Max: 82 Sum: 2173 Ratio: 0.10%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 410504 (Eliminated: 0 Frozen: 131302) +Constraints : 3019218 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 536MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.00s +Memory: 497MB (+0MB) +UNKNOWN +Iteration Time: 7.03s + +Iteration 25 +Queue: [(7,35,1,True), (8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 80 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 26 +Time : 154.124s (Solving: 142.45s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 154.064s + +Choices : 2488902 (Domain: 2415421) +Conflicts : 186775 (Analyzed: 186772) +Restarts : 2136 (Average: 87.44 Last: 140) +Model-Level : 115.0 +Problems : 26 (Average Length: 45.27 Splits: 0) +Lemmas : 186772 (Deleted: 165694) + Binary : 6325 (Ratio: 3.39%) + Ternary : 2240 (Ratio: 1.20%) + Conflict : 186772 (Average Length: 515.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 186772 (Average: 11.93 Max: 663 Sum: 2227888) + Executed : 186671 (Average: 11.92 Max: 663 Sum: 2225715 Ratio: 99.90%) + Bounded : 101 (Average: 21.51 Max: 82 Sum: 2173 Ratio: 0.10%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 410504 (Eliminated: 0 Frozen: 131302) +Constraints : 3019218 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 536MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.60s +Memory: 497MB (+0MB) +UNKNOWN +Iteration Time: 8.64s + +Iteration 26 +Queue: [(8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 80 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 27 +Time : 161.498s (Solving: 149.73s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 161.444s + +Choices : 2569830 (Domain: 2495784) +Conflicts : 195487 (Analyzed: 195484) +Restarts : 2236 (Average: 87.43 Last: 140) +Model-Level : 115.0 +Problems : 27 (Average Length: 46.63 Splits: 0) +Lemmas : 195484 (Deleted: 174716) + Binary : 6407 (Ratio: 3.28%) + Ternary : 2246 (Ratio: 1.15%) + Conflict : 195484 (Average Length: 531.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 195484 (Average: 11.73 Max: 663 Sum: 2292245) + Executed : 195382 (Average: 11.71 Max: 663 Sum: 2289990 Ratio: 99.90%) + Bounded : 102 (Average: 22.11 Max: 82 Sum: 2255 Ratio: 0.10%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 410504 (Eliminated: 0 Frozen: 131302) +Constraints : 3019218 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 536MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.34s +Memory: 497MB (+0MB) +UNKNOWN +Iteration Time: 7.38s + +Iteration 27 +Queue: [(9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 80 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 28 +Time : 170.232s (Solving: 158.37s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 170.180s + +Choices : 2693557 (Domain: 2618679) +Conflicts : 205205 (Analyzed: 205202) +Restarts : 2336 (Average: 87.84 Last: 140) +Model-Level : 115.0 +Problems : 28 (Average Length: 47.89 Splits: 0) +Lemmas : 205202 (Deleted: 183229) + Binary : 6494 (Ratio: 3.16%) + Ternary : 2260 (Ratio: 1.10%) + Conflict : 205202 (Average Length: 549.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 205202 (Average: 11.68 Max: 663 Sum: 2396937) + Executed : 205100 (Average: 11.67 Max: 663 Sum: 2394682 Ratio: 99.91%) + Bounded : 102 (Average: 22.11 Max: 82 Sum: 2255 Ratio: 0.09%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 410504 (Eliminated: 0 Frozen: 131302) +Constraints : 3019204 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 536MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.70s +Memory: 497MB (+0MB) +UNKNOWN +Iteration Time: 8.74s + +Iteration 28 +Queue: [(10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 80 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 29 +Time : 179.094s (Solving: 167.12s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 179.032s + +Choices : 2817211 (Domain: 2741842) +Conflicts : 214377 (Analyzed: 214374) +Restarts : 2436 (Average: 88.00 Last: 140) +Model-Level : 115.0 +Problems : 29 (Average Length: 49.07 Splits: 0) +Lemmas : 214374 (Deleted: 192959) + Binary : 6574 (Ratio: 3.07%) + Ternary : 2276 (Ratio: 1.06%) + Conflict : 214374 (Average Length: 570.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 214374 (Average: 11.66 Max: 663 Sum: 2499886) + Executed : 214272 (Average: 11.65 Max: 663 Sum: 2497631 Ratio: 99.91%) + Bounded : 102 (Average: 22.11 Max: 82 Sum: 2255 Ratio: 0.09%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 410504 (Eliminated: 0 Frozen: 131302) +Constraints : 3019204 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 536MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.81s +Memory: 497MB (+0MB) +UNKNOWN +Iteration Time: 8.85s + +Iteration 29 +Queue: [(11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 80 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 30 +Time : 188.395s (Solving: 176.32s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 188.324s + +Choices : 2942104 (Domain: 2866477) +Conflicts : 223011 (Analyzed: 223008) +Restarts : 2536 (Average: 87.94 Last: 140) +Model-Level : 115.0 +Problems : 30 (Average Length: 50.17 Splits: 0) +Lemmas : 223008 (Deleted: 201500) + Binary : 6860 (Ratio: 3.08%) + Ternary : 2304 (Ratio: 1.03%) + Conflict : 223008 (Average Length: 598.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 223008 (Average: 11.65 Max: 663 Sum: 2597541) + Executed : 222906 (Average: 11.64 Max: 663 Sum: 2595286 Ratio: 99.91%) + Bounded : 102 (Average: 22.11 Max: 82 Sum: 2255 Ratio: 0.09%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 410504 (Eliminated: 0 Frozen: 131302) +Constraints : 3019204 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 536MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.26s +Memory: 497MB (+0MB) +UNKNOWN +Iteration Time: 9.30s + +Iteration 30 +Queue: [(12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 80 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 31 +Time : 196.863s (Solving: 184.68s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 196.796s + +Choices : 3132845 (Domain: 3055017) +Conflicts : 231800 (Analyzed: 231797) +Restarts : 2636 (Average: 87.94 Last: 140) +Model-Level : 115.0 +Problems : 31 (Average Length: 51.19 Splits: 0) +Lemmas : 231797 (Deleted: 209762) + Binary : 7187 (Ratio: 3.10%) + Ternary : 2415 (Ratio: 1.04%) + Conflict : 231797 (Average Length: 607.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 231797 (Average: 11.92 Max: 663 Sum: 2761912) + Executed : 231695 (Average: 11.91 Max: 663 Sum: 2759657 Ratio: 99.92%) + Bounded : 102 (Average: 22.11 Max: 82 Sum: 2255 Ratio: 0.08%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 410504 (Eliminated: 0 Frozen: 131302) +Constraints : 3019204 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 536MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.43s +Memory: 497MB (+0MB) +UNKNOWN +Iteration Time: 8.47s + +Iteration 31 +Queue: [(13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 80 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 32 +Time : 205.785s (Solving: 193.50s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 205.720s + +Choices : 3288719 (Domain: 3210193) +Conflicts : 240496 (Analyzed: 240493) +Restarts : 2736 (Average: 87.90 Last: 140) +Model-Level : 115.0 +Problems : 32 (Average Length: 52.16 Splits: 0) +Lemmas : 240493 (Deleted: 217804) + Binary : 7303 (Ratio: 3.04%) + Ternary : 2429 (Ratio: 1.01%) + Conflict : 240493 (Average Length: 623.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 240493 (Average: 12.02 Max: 663 Sum: 2891855) + Executed : 240391 (Average: 12.02 Max: 663 Sum: 2889600 Ratio: 99.92%) + Bounded : 102 (Average: 22.11 Max: 82 Sum: 2255 Ratio: 0.08%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 410504 (Eliminated: 0 Frozen: 131302) +Constraints : 3019204 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 536MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.89s +Memory: 497MB (+0MB) +UNKNOWN +Iteration Time: 8.93s + +Iteration 32 +Queue: [(14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 80 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 33 +Time : 214.168s (Solving: 201.77s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 214.104s + +Choices : 3432539 (Domain: 3353716) +Conflicts : 249286 (Analyzed: 249283) +Restarts : 2836 (Average: 87.90 Last: 140) +Model-Level : 115.0 +Problems : 33 (Average Length: 53.06 Splits: 0) +Lemmas : 249283 (Deleted: 226279) + Binary : 7355 (Ratio: 2.95%) + Ternary : 2443 (Ratio: 0.98%) + Conflict : 249283 (Average Length: 634.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 249283 (Average: 12.08 Max: 663 Sum: 3011781) + Executed : 249181 (Average: 12.07 Max: 663 Sum: 3009526 Ratio: 99.93%) + Bounded : 102 (Average: 22.11 Max: 82 Sum: 2255 Ratio: 0.07%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 410504 (Eliminated: 0 Frozen: 131302) +Constraints : 3019204 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 536MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.35s +Memory: 497MB (+0MB) +UNKNOWN +Iteration Time: 8.39s + +Iteration 33 +Queue: [(15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 80 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 34 +Time : 222.726s (Solving: 210.23s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 222.664s + +Choices : 3592981 (Domain: 3513628) +Conflicts : 258371 (Analyzed: 258368) +Restarts : 2936 (Average: 88.00 Last: 176) +Model-Level : 115.0 +Problems : 34 (Average Length: 53.91 Splits: 0) +Lemmas : 258368 (Deleted: 234880) + Binary : 7404 (Ratio: 2.87%) + Ternary : 2455 (Ratio: 0.95%) + Conflict : 258368 (Average Length: 642.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 258368 (Average: 12.18 Max: 663 Sum: 3146171) + Executed : 258266 (Average: 12.17 Max: 663 Sum: 3143916 Ratio: 99.93%) + Bounded : 102 (Average: 22.11 Max: 82 Sum: 2255 Ratio: 0.07%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 410504 (Eliminated: 0 Frozen: 131302) +Constraints : 3019204 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 536MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.52s +Memory: 497MB (+0MB) +UNKNOWN +Iteration Time: 8.57s + +Iteration 34 +Queue: [(16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 80 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 35 +Time : 232.793s (Solving: 220.20s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 232.736s + +Choices : 3877900 (Domain: 3794531) +Conflicts : 267061 (Analyzed: 267058) +Restarts : 3036 (Average: 87.96 Last: 176) +Model-Level : 115.0 +Problems : 35 (Average Length: 54.71 Splits: 0) +Lemmas : 267058 (Deleted: 243589) + Binary : 7792 (Ratio: 2.92%) + Ternary : 2535 (Ratio: 0.95%) + Conflict : 267058 (Average Length: 654.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 267058 (Average: 12.72 Max: 663 Sum: 3396085) + Executed : 266956 (Average: 12.71 Max: 663 Sum: 3393830 Ratio: 99.93%) + Bounded : 102 (Average: 22.11 Max: 82 Sum: 2255 Ratio: 0.07%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 410504 (Eliminated: 0 Frozen: 131302) +Constraints : 3019204 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 536MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 10.04s +Memory: 497MB (+0MB) +UNKNOWN +Iteration Time: 10.07s + +Iteration 35 +Queue: [(17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 80 +Expected Memory: 545.0MB +Grounding... [('step', [81]), ('step', [82]), ('step', [83]), ('step', [84]), ('step', [85]), ('check', [85])] +Grounding Time: 0.37s +Memory: 497MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 36 +Time : 243.645s (Solving: 230.29s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 243.592s + +Choices : 4181021 (Domain: 4093925) +Conflicts : 276377 (Analyzed: 276374) +Restarts : 3136 (Average: 88.13 Last: 176) +Model-Level : 115.0 +Problems : 36 (Average Length: 55.61 Splits: 0) +Lemmas : 276374 (Deleted: 251525) + Binary : 8148 (Ratio: 2.95%) + Ternary : 2585 (Ratio: 0.94%) + Conflict : 276374 (Average Length: 661.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 276374 (Average: 13.25 Max: 663 Sum: 3662936) + Executed : 276272 (Average: 13.25 Max: 663 Sum: 3660681 Ratio: 99.94%) + Bounded : 102 (Average: 22.11 Max: 82 Sum: 2255 Ratio: 0.06%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 436900 (Eliminated: 0 Frozen: 139842) +Constraints : 3220274 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 557MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 10.18s +Memory: 514MB (+17MB) +UNKNOWN +Iteration Time: 10.86s + +Iteration 36 +Queue: [(18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 85 +Expected Memory: 562.0MB +Grounding... [('step', [86]), ('step', [87]), ('step', [88]), ('step', [89]), ('step', [90]), ('check', [90])] +Grounding Time: 0.37s +Memory: 514MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 37 +Time : 255.192s (Solving: 241.05s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 255.144s + +Choices : 4503354 (Domain: 4412880) +Conflicts : 285248 (Analyzed: 285245) +Restarts : 3236 (Average: 88.15 Last: 176) +Model-Level : 115.0 +Problems : 37 (Average Length: 56.59 Splits: 0) +Lemmas : 285245 (Deleted: 259852) + Binary : 8507 (Ratio: 2.98%) + Ternary : 2649 (Ratio: 0.93%) + Conflict : 285245 (Average Length: 668.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 285245 (Average: 13.83 Max: 663 Sum: 3944444) + Executed : 285143 (Average: 13.82 Max: 663 Sum: 3942189 Ratio: 99.94%) + Bounded : 102 (Average: 22.11 Max: 82 Sum: 2255 Ratio: 0.06%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 463296 (Eliminated: 0 Frozen: 148382) +Constraints : 3421344 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 579MB +Max. Length : 85 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 10.86s +Memory: 534MB (+20MB) +UNKNOWN +Iteration Time: 11.56s + +Iteration 37 +Queue: [(19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 90 +Expected Memory: 582.0MB +Grounding... [('step', [91]), ('step', [92]), ('step', [93]), ('step', [94]), ('step', [95]), ('check', [95])] +Grounding Time: 0.40s +Memory: 534MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 38 +Time : 264.812s (Solving: 249.84s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 264.768s + +Choices : 4628359 (Domain: 4537823) +Conflicts : 294272 (Analyzed: 294269) +Restarts : 3336 (Average: 88.21 Last: 176) +Model-Level : 115.0 +Problems : 38 (Average Length: 57.66 Splits: 0) +Lemmas : 294269 (Deleted: 268492) + Binary : 8562 (Ratio: 2.91%) + Ternary : 2662 (Ratio: 0.90%) + Conflict : 294269 (Average Length: 678.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 294269 (Average: 13.72 Max: 749 Sum: 4037502) + Executed : 294167 (Average: 13.71 Max: 749 Sum: 4035247 Ratio: 99.94%) + Bounded : 102 (Average: 22.11 Max: 82 Sum: 2255 Ratio: 0.06%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 489692 (Eliminated: 0 Frozen: 156922) +Constraints : 3622414 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 599MB +Max. Length : 90 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.88s +Memory: 589MB (+55MB) +UNKNOWN +Iteration Time: 9.63s + +Iteration 38 +Queue: [(20,100,0,True), (21,105,0,True)] +Grounded Until: 95 +Expected Memory: 644.0MB +Grounding... [('step', [96]), ('step', [97]), ('step', [98]), ('step', [99]), ('step', [100]), ('check', [100])] +Grounding Time: 0.38s +Memory: 589MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 39 +Time : 274.227s (Solving: 258.44s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 274.188s + +Choices : 4767706 (Domain: 4677146) +Conflicts : 303380 (Analyzed: 303377) +Restarts : 3436 (Average: 88.29 Last: 176) +Model-Level : 115.0 +Problems : 39 (Average Length: 58.79 Splits: 0) +Lemmas : 303377 (Deleted: 277400) + Binary : 8596 (Ratio: 2.83%) + Ternary : 2672 (Ratio: 0.88%) + Conflict : 303377 (Average Length: 684.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 303377 (Average: 13.67 Max: 749 Sum: 4148352) + Executed : 303275 (Average: 13.67 Max: 749 Sum: 4146097 Ratio: 99.95%) + Bounded : 102 (Average: 22.11 Max: 82 Sum: 2255 Ratio: 0.05%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 516088 (Eliminated: 0 Frozen: 165462) +Constraints : 3823484 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 652MB +Max. Length : 95 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.70s +Memory: 593MB (+4MB) +UNKNOWN +Iteration Time: 9.43s + +Iteration 39 +Queue: [(21,105,0,True)] +Grounded Until: 100 +Expected Memory: 648.0MB +Grounding... [('step', [101]), ('step', [102]), ('step', [103]), ('step', [104]), ('step', [105]), ('check', [105])] +Grounding Time: 0.38s +Memory: 593MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 40 +Time : 285.155s (Solving: 268.55s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 285.120s + +Choices : 4907796 (Domain: 4817210) +Conflicts : 312857 (Analyzed: 312854) +Restarts : 3536 (Average: 88.48 Last: 176) +Model-Level : 115.0 +Problems : 40 (Average Length: 60.00 Splits: 0) +Lemmas : 312854 (Deleted: 286431) + Binary : 8659 (Ratio: 2.77%) + Ternary : 2681 (Ratio: 0.86%) + Conflict : 312854 (Average Length: 698.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 312854 (Average: 13.59 Max: 749 Sum: 4252735) + Executed : 312752 (Average: 13.59 Max: 749 Sum: 4250480 Ratio: 99.95%) + Bounded : 102 (Average: 22.11 Max: 82 Sum: 2255 Ratio: 0.05%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 542484 (Eliminated: 0 Frozen: 174002) +Constraints : 4024554 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 663MB +Max. Length : 100 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 10.22s +Memory: 600MB (+7MB) +UNKNOWN +Iteration Time: 10.94s + +Iteration 40 +Queue: [(4,20,3,True), (5,25,3,True), (6,30,3,True), (7,35,2,True), (8,40,2,True), (9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Blocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 41 +Time : 287.156s (Solving: 270.41s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 287.120s + +Choices : 4942736 (Domain: 4852150) +Conflicts : 319881 (Analyzed: 319878) +Restarts : 3636 (Average: 87.98 Last: 176) +Model-Level : 115.0 +Problems : 41 (Average Length: 61.15 Splits: 0) +Lemmas : 319878 (Deleted: 293456) + Binary : 8706 (Ratio: 2.72%) + Ternary : 2685 (Ratio: 0.84%) + Conflict : 319878 (Average Length: 688.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 319878 (Average: 13.36 Max: 749 Sum: 4273452) + Executed : 319776 (Average: 13.35 Max: 749 Sum: 4271197 Ratio: 99.95%) + Bounded : 102 (Average: 22.11 Max: 82 Sum: 2255 Ratio: 0.05%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 542484 (Eliminated: 0 Frozen: 174002) +Constraints : 4024554 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 663MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 1.94s +Memory: 607MB (+7MB) +UNKNOWN +Iteration Time: 2.00s + +Iteration 41 +Queue: [(5,25,3,True), (6,30,3,True), (7,35,2,True), (8,40,2,True), (9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 42 +Time : 296.305s (Solving: 279.44s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 296.272s + +Choices : 5000061 (Domain: 4907566) +Conflicts : 329635 (Analyzed: 329632) +Restarts : 3736 (Average: 88.23 Last: 176) +Model-Level : 115.0 +Problems : 42 (Average Length: 62.24 Splits: 0) +Lemmas : 329632 (Deleted: 302437) + Binary : 8753 (Ratio: 2.66%) + Ternary : 2694 (Ratio: 0.82%) + Conflict : 329632 (Average Length: 703.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 329632 (Average: 13.09 Max: 749 Sum: 4315421) + Executed : 329530 (Average: 13.08 Max: 749 Sum: 4313166 Ratio: 99.95%) + Bounded : 102 (Average: 22.11 Max: 82 Sum: 2255 Ratio: 0.05%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 542484 (Eliminated: 0 Frozen: 174002) +Constraints : 4024554 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 663MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.11s +Memory: 607MB (+0MB) +UNKNOWN +Iteration Time: 9.16s + +Iteration 42 +Queue: [(6,30,3,True), (7,35,2,True), (8,40,2,True), (9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 43 +Time : 303.888s (Solving: 286.88s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 303.860s + +Choices : 5077192 (Domain: 4984697) +Conflicts : 338616 (Analyzed: 338613) +Restarts : 3836 (Average: 88.27 Last: 176) +Model-Level : 115.0 +Problems : 43 (Average Length: 63.28 Splits: 0) +Lemmas : 338613 (Deleted: 311887) + Binary : 8797 (Ratio: 2.60%) + Ternary : 2716 (Ratio: 0.80%) + Conflict : 338613 (Average Length: 703.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 338613 (Average: 12.92 Max: 749 Sum: 4375324) + Executed : 338511 (Average: 12.91 Max: 749 Sum: 4373069 Ratio: 99.95%) + Bounded : 102 (Average: 22.11 Max: 82 Sum: 2255 Ratio: 0.05%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 542484 (Eliminated: 0 Frozen: 174002) +Constraints : 4024554 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 663MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.53s +Memory: 607MB (+0MB) +UNKNOWN +Iteration Time: 7.59s + +Iteration 43 +Queue: [(7,35,2,True), (8,40,2,True), (9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 44 +Time : 311.106s (Solving: 293.99s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 311.084s + +Choices : 5149776 (Domain: 5057190) +Conflicts : 347519 (Analyzed: 347516) +Restarts : 3936 (Average: 88.29 Last: 176) +Model-Level : 115.0 +Problems : 44 (Average Length: 64.27 Splits: 0) +Lemmas : 347516 (Deleted: 320707) + Binary : 8884 (Ratio: 2.56%) + Ternary : 2724 (Ratio: 0.78%) + Conflict : 347516 (Average Length: 711.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 347516 (Average: 12.74 Max: 749 Sum: 4427839) + Executed : 347414 (Average: 12.73 Max: 749 Sum: 4425584 Ratio: 99.95%) + Bounded : 102 (Average: 22.11 Max: 82 Sum: 2255 Ratio: 0.05%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 542484 (Eliminated: 0 Frozen: 174002) +Constraints : 4024554 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 663MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.18s +Memory: 607MB (+0MB) +UNKNOWN +Iteration Time: 7.22s + +Iteration 44 +Queue: [(8,40,2,True), (9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 45 +Time : 318.548s (Solving: 301.32s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 318.532s + +Choices : 5232581 (Domain: 5139951) +Conflicts : 356198 (Analyzed: 356195) +Restarts : 4036 (Average: 88.25 Last: 176) +Model-Level : 115.0 +Problems : 45 (Average Length: 65.22 Splits: 0) +Lemmas : 356195 (Deleted: 329365) + Binary : 8938 (Ratio: 2.51%) + Ternary : 2729 (Ratio: 0.77%) + Conflict : 356195 (Average Length: 719.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 356195 (Average: 12.61 Max: 749 Sum: 4491214) + Executed : 356093 (Average: 12.60 Max: 749 Sum: 4488959 Ratio: 99.95%) + Bounded : 102 (Average: 22.11 Max: 82 Sum: 2255 Ratio: 0.05%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 542484 (Eliminated: 0 Frozen: 174002) +Constraints : 4024554 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 663MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.41s +Memory: 607MB (+0MB) +UNKNOWN +Iteration Time: 7.45s + +Iteration 45 +Queue: [(9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 46 +Time : 326.810s (Solving: 309.47s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 326.796s + +Choices : 5344987 (Domain: 5251586) +Conflicts : 365483 (Analyzed: 365480) +Restarts : 4136 (Average: 88.37 Last: 176) +Model-Level : 115.0 +Problems : 46 (Average Length: 66.13 Splits: 0) +Lemmas : 365480 (Deleted: 337903) + Binary : 9094 (Ratio: 2.49%) + Ternary : 2760 (Ratio: 0.76%) + Conflict : 365480 (Average Length: 720.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 365480 (Average: 12.53 Max: 749 Sum: 4580656) + Executed : 365378 (Average: 12.53 Max: 749 Sum: 4578401 Ratio: 99.95%) + Bounded : 102 (Average: 22.11 Max: 82 Sum: 2255 Ratio: 0.05%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 542484 (Eliminated: 0 Frozen: 174002) +Constraints : 4024554 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 663MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.23s +Memory: 607MB (+0MB) +UNKNOWN +Iteration Time: 8.27s + +Iteration 46 +Queue: [(10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 47 +Time : 335.970s (Solving: 318.48s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 335.960s + +Choices : 5472786 (Domain: 5377969) +Conflicts : 374294 (Analyzed: 374291) +Restarts : 4236 (Average: 88.36 Last: 176) +Model-Level : 115.0 +Problems : 47 (Average Length: 67.00 Splits: 0) +Lemmas : 374291 (Deleted: 346564) + Binary : 9426 (Ratio: 2.52%) + Ternary : 2803 (Ratio: 0.75%) + Conflict : 374291 (Average Length: 727.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 374291 (Average: 12.50 Max: 749 Sum: 4679651) + Executed : 374189 (Average: 12.50 Max: 749 Sum: 4677396 Ratio: 99.95%) + Bounded : 102 (Average: 22.11 Max: 82 Sum: 2255 Ratio: 0.05%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 542484 (Eliminated: 0 Frozen: 174002) +Constraints : 4024554 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 663MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.11s +Memory: 607MB (+0MB) +UNKNOWN +Iteration Time: 9.17s + +Iteration 47 +Queue: [(11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 48 +Time : 346.111s (Solving: 328.48s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 346.108s + +Choices : 5614538 (Domain: 5518534) +Conflicts : 383455 (Analyzed: 383452) +Restarts : 4336 (Average: 88.43 Last: 176) +Model-Level : 115.0 +Problems : 48 (Average Length: 67.83 Splits: 0) +Lemmas : 383452 (Deleted: 354974) + Binary : 9597 (Ratio: 2.50%) + Ternary : 2819 (Ratio: 0.74%) + Conflict : 383452 (Average Length: 737.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 383452 (Average: 12.50 Max: 749 Sum: 4791944) + Executed : 383350 (Average: 12.49 Max: 749 Sum: 4789689 Ratio: 99.95%) + Bounded : 102 (Average: 22.11 Max: 82 Sum: 2255 Ratio: 0.05%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 542484 (Eliminated: 0 Frozen: 174002) +Constraints : 4024554 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 735MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 10.09s +Memory: 671MB (+64MB) +UNKNOWN +Iteration Time: 10.15s + +Iteration 48 +Queue: [(12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 49 +Time : 354.056s (Solving: 336.29s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 354.056s + +Choices : 5719960 (Domain: 5623921) +Conflicts : 392643 (Analyzed: 392640) +Restarts : 4436 (Average: 88.51 Last: 176) +Model-Level : 115.0 +Problems : 49 (Average Length: 68.63 Splits: 0) +Lemmas : 392640 (Deleted: 363872) + Binary : 9629 (Ratio: 2.45%) + Ternary : 2834 (Ratio: 0.72%) + Conflict : 392640 (Average Length: 741.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 392640 (Average: 12.41 Max: 749 Sum: 4874223) + Executed : 392537 (Average: 12.41 Max: 749 Sum: 4871861 Ratio: 99.95%) + Bounded : 103 (Average: 22.93 Max: 107 Sum: 2362 Ratio: 0.05%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 542484 (Eliminated: 0 Frozen: 174002) +Constraints : 4024554 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 735MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.90s +Memory: 671MB (+0MB) +UNKNOWN +Iteration Time: 7.95s + +Iteration 49 +Queue: [(13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 50 +Time : 363.462s (Solving: 345.54s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 363.468s + +Choices : 5852039 (Domain: 5755449) +Conflicts : 401350 (Analyzed: 401347) +Restarts : 4536 (Average: 88.48 Last: 176) +Model-Level : 115.0 +Problems : 50 (Average Length: 69.40 Splits: 0) +Lemmas : 401347 (Deleted: 372889) + Binary : 9737 (Ratio: 2.43%) + Ternary : 2845 (Ratio: 0.71%) + Conflict : 401347 (Average Length: 749.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 401347 (Average: 12.40 Max: 749 Sum: 4975948) + Executed : 401244 (Average: 12.39 Max: 749 Sum: 4973586 Ratio: 99.95%) + Bounded : 103 (Average: 22.93 Max: 107 Sum: 2362 Ratio: 0.05%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 542484 (Eliminated: 0 Frozen: 174002) +Constraints : 4024540 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 735MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.35s +Memory: 671MB (+0MB) +UNKNOWN +Iteration Time: 9.41s + +Iteration 50 +Queue: [(17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 51 +Time : 371.215s (Solving: 353.18s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 371.224s + +Choices : 5942328 (Domain: 5845735) +Conflicts : 409926 (Analyzed: 409923) +Restarts : 4636 (Average: 88.42 Last: 176) +Model-Level : 115.0 +Problems : 51 (Average Length: 70.14 Splits: 0) +Lemmas : 409923 (Deleted: 379501) + Binary : 9748 (Ratio: 2.38%) + Ternary : 2848 (Ratio: 0.69%) + Conflict : 409923 (Average Length: 753.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 409923 (Average: 12.29 Max: 749 Sum: 5038609) + Executed : 409820 (Average: 12.29 Max: 749 Sum: 5036247 Ratio: 99.95%) + Bounded : 103 (Average: 22.93 Max: 107 Sum: 2362 Ratio: 0.05%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 542484 (Eliminated: 0 Frozen: 174002) +Constraints : 4024540 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 735MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.72s +Memory: 671MB (+0MB) +UNKNOWN +Iteration Time: 7.76s + +Iteration 51 +Queue: [(18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 52 +Time : 379.357s (Solving: 361.18s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 379.368s + +Choices : 6044493 (Domain: 5947886) +Conflicts : 418658 (Analyzed: 418655) +Restarts : 4736 (Average: 88.40 Last: 176) +Model-Level : 115.0 +Problems : 52 (Average Length: 70.85 Splits: 0) +Lemmas : 418655 (Deleted: 389772) + Binary : 9770 (Ratio: 2.33%) + Ternary : 2857 (Ratio: 0.68%) + Conflict : 418655 (Average Length: 758.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 418655 (Average: 12.21 Max: 749 Sum: 5113202) + Executed : 418552 (Average: 12.21 Max: 749 Sum: 5110840 Ratio: 99.95%) + Bounded : 103 (Average: 22.93 Max: 107 Sum: 2362 Ratio: 0.05%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 542484 (Eliminated: 0 Frozen: 174002) +Constraints : 4024540 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 735MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.09s +Memory: 671MB (+0MB) +UNKNOWN +Iteration Time: 8.15s + +Iteration 52 +Queue: [(19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 53 +Time : 387.801s (Solving: 369.50s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 387.816s + +Choices : 6155409 (Domain: 6058789) +Conflicts : 427478 (Analyzed: 427475) +Restarts : 4836 (Average: 88.39 Last: 176) +Model-Level : 115.0 +Problems : 53 (Average Length: 71.53 Splits: 0) +Lemmas : 427475 (Deleted: 398353) + Binary : 9818 (Ratio: 2.30%) + Ternary : 2863 (Ratio: 0.67%) + Conflict : 427475 (Average Length: 763.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 427475 (Average: 12.15 Max: 749 Sum: 5194031) + Executed : 427372 (Average: 12.14 Max: 749 Sum: 5191669 Ratio: 99.95%) + Bounded : 103 (Average: 22.93 Max: 107 Sum: 2362 Ratio: 0.05%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 542484 (Eliminated: 0 Frozen: 174002) +Constraints : 4024540 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 735MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.40s +Memory: 671MB (+0MB) +UNKNOWN +Iteration Time: 8.45s + +Iteration 53 +Queue: [(20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 54 +Time : 395.758s (Solving: 377.34s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 395.776s + +Choices : 6250965 (Domain: 6154151) +Conflicts : 435761 (Analyzed: 435758) +Restarts : 4936 (Average: 88.28 Last: 176) +Model-Level : 115.0 +Problems : 54 (Average Length: 72.19 Splits: 0) +Lemmas : 435758 (Deleted: 405426) + Binary : 9870 (Ratio: 2.27%) + Ternary : 2867 (Ratio: 0.66%) + Conflict : 435758 (Average Length: 770.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 435758 (Average: 12.06 Max: 749 Sum: 5254641) + Executed : 435655 (Average: 12.05 Max: 749 Sum: 5252279 Ratio: 99.96%) + Bounded : 103 (Average: 22.93 Max: 107 Sum: 2362 Ratio: 0.04%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 542484 (Eliminated: 0 Frozen: 174002) +Constraints : 4024540 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 735MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.92s +Memory: 671MB (+0MB) +UNKNOWN +Iteration Time: 7.96s + +Iteration 54 +Queue: [(21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 55 +Time : 404.622s (Solving: 386.09s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 404.644s + +Choices : 6361764 (Domain: 6264949) +Conflicts : 444366 (Analyzed: 444363) +Restarts : 5036 (Average: 88.24 Last: 176) +Model-Level : 115.0 +Problems : 55 (Average Length: 72.82 Splits: 0) +Lemmas : 444363 (Deleted: 413923) + Binary : 9895 (Ratio: 2.23%) + Ternary : 2873 (Ratio: 0.65%) + Conflict : 444363 (Average Length: 775.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 444363 (Average: 12.00 Max: 749 Sum: 5331624) + Executed : 444260 (Average: 11.99 Max: 749 Sum: 5329262 Ratio: 99.96%) + Bounded : 103 (Average: 22.93 Max: 107 Sum: 2362 Ratio: 0.04%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 542484 (Eliminated: 0 Frozen: 174002) +Constraints : 4024540 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 735MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.83s +Memory: 671MB (+0MB) +UNKNOWN +Iteration Time: 8.87s + +Iteration 55 +Queue: [(22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Expected Memory: 726.0MB +Grounding... [('step', [106]), ('step', [107]), ('step', [108]), ('step', [109]), ('step', [110]), ('check', [110])] +Grounding Time: 0.39s +Memory: 671MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 56 +Time : 416.570s (Solving: 397.18s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 416.600s + +Choices : 6634390 (Domain: 6536879) +Conflicts : 453641 (Analyzed: 453638) +Restarts : 5136 (Average: 88.33 Last: 176) +Model-Level : 115.0 +Problems : 56 (Average Length: 73.52 Splits: 0) +Lemmas : 453638 (Deleted: 423493) + Binary : 10024 (Ratio: 2.21%) + Ternary : 2891 (Ratio: 0.64%) + Conflict : 453638 (Average Length: 781.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 453638 (Average: 12.26 Max: 749 Sum: 5562958) + Executed : 453535 (Average: 12.26 Max: 749 Sum: 5560596 Ratio: 99.96%) + Bounded : 103 (Average: 22.93 Max: 107 Sum: 2362 Ratio: 0.04%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 568880 (Eliminated: 0 Frozen: 182542) +Constraints : 4225610 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 744MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 11.20s +Memory: 685MB (+14MB) +UNKNOWN +Iteration Time: 11.96s + +Iteration 56 +Queue: [(23,115,0,True)] +Grounded Until: 110 +Expected Memory: 740.0MB +Grounding... [('step', [111]), ('step', [112]), ('step', [113]), ('step', [114]), ('step', [115]), ('check', [115])] +Grounding Time: 0.39s +Memory: 685MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 57 +Time : 427.280s (Solving: 407.00s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 427.316s + +Choices : 6854646 (Domain: 6756623) +Conflicts : 462668 (Analyzed: 462665) +Restarts : 5236 (Average: 88.36 Last: 176) +Model-Level : 115.0 +Problems : 57 (Average Length: 74.28 Splits: 0) +Lemmas : 462665 (Deleted: 432406) + Binary : 10175 (Ratio: 2.20%) + Ternary : 2901 (Ratio: 0.63%) + Conflict : 462665 (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 : 462665 (Average: 12.40 Max: 749 Sum: 5737512) + Executed : 462562 (Average: 12.40 Max: 749 Sum: 5735150 Ratio: 99.96%) + Bounded : 103 (Average: 22.93 Max: 107 Sum: 2362 Ratio: 0.04%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 595276 (Eliminated: 0 Frozen: 191082) +Constraints : 4426680 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 769MB +Max. Length : 110 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.94s +Memory: 700MB (+15MB) +UNKNOWN +Iteration Time: 10.73s + +Iteration 57 +Queue: [(4,20,4,True), (5,25,4,True), (6,30,4,True), (7,35,3,True), (8,40,3,True), (9,45,3,True), (10,50,3,True), (11,55,3,False), (12,60,3,False), (13,65,3,False), (14,70,2,True), (15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,1,True), (23,115,1,True)] +Grounded Until: 115 +Blocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 58 +Time : 430.580s (Solving: 410.15s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 430.616s + +Choices : 6898780 (Domain: 6800757) +Conflicts : 470288 (Analyzed: 470285) +Restarts : 5336 (Average: 88.13 Last: 176) +Model-Level : 115.0 +Problems : 58 (Average Length: 75.02 Splits: 0) +Lemmas : 470285 (Deleted: 439000) + Binary : 10245 (Ratio: 2.18%) + Ternary : 2903 (Ratio: 0.62%) + Conflict : 470285 (Average Length: 776.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 470285 (Average: 12.27 Max: 749 Sum: 5772736) + Executed : 470182 (Average: 12.27 Max: 749 Sum: 5770374 Ratio: 99.96%) + Bounded : 103 (Average: 22.93 Max: 107 Sum: 2362 Ratio: 0.04%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 595276 (Eliminated: 0 Frozen: 191082) +Constraints : 4426680 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 769MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 3.25s +Memory: 700MB (+0MB) +UNKNOWN +Iteration Time: 3.30s + +Iteration 58 +Queue: [(5,25,4,True), (6,30,4,True), (7,35,3,True), (8,40,3,True), (9,45,3,True), (10,50,3,True), (11,55,3,False), (12,60,3,False), (13,65,3,False), (14,70,2,True), (15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,1,True), (23,115,1,True)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 59 +Time : 439.385s (Solving: 418.83s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 439.428s + +Choices : 6961616 (Domain: 6863593) +Conflicts : 479443 (Analyzed: 479440) +Restarts : 5436 (Average: 88.20 Last: 176) +Model-Level : 115.0 +Problems : 59 (Average Length: 75.73 Splits: 0) +Lemmas : 479440 (Deleted: 448669) + Binary : 10287 (Ratio: 2.15%) + Ternary : 2910 (Ratio: 0.61%) + Conflict : 479440 (Average Length: 783.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 479440 (Average: 12.14 Max: 749 Sum: 5821610) + Executed : 479337 (Average: 12.14 Max: 749 Sum: 5819248 Ratio: 99.96%) + Bounded : 103 (Average: 22.93 Max: 107 Sum: 2362 Ratio: 0.04%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 595276 (Eliminated: 0 Frozen: 191082) +Constraints : 4426680 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 769MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.77s +Memory: 700MB (+0MB) +UNKNOWN +Iteration Time: 8.81s + +Iteration 59 +Queue: [(6,30,4,True), (7,35,3,True), (8,40,3,True), (9,45,3,True), (10,50,3,True), (11,55,3,False), (12,60,3,False), (13,65,3,False), (14,70,2,True), (15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,1,True), (23,115,1,True)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 60 +Time : 447.565s (Solving: 426.87s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 447.612s + +Choices : 7044420 (Domain: 6946397) +Conflicts : 488143 (Analyzed: 488140) +Restarts : 5536 (Average: 88.18 Last: 176) +Model-Level : 115.0 +Problems : 60 (Average Length: 76.42 Splits: 0) +Lemmas : 488140 (Deleted: 457648) + Binary : 10337 (Ratio: 2.12%) + Ternary : 2932 (Ratio: 0.60%) + Conflict : 488140 (Average Length: 786.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 488140 (Average: 12.06 Max: 749 Sum: 5886394) + Executed : 488037 (Average: 12.05 Max: 749 Sum: 5884032 Ratio: 99.96%) + Bounded : 103 (Average: 22.93 Max: 107 Sum: 2362 Ratio: 0.04%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 595276 (Eliminated: 0 Frozen: 191082) +Constraints : 4426680 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 769MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.13s +Memory: 700MB (+0MB) +UNKNOWN +Iteration Time: 8.19s + +Iteration 60 +Queue: [(7,35,3,True), (8,40,3,True), (9,45,3,True), (10,50,3,True), (11,55,3,False), (12,60,3,False), (13,65,3,False), (14,70,2,True), (15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,1,True), (23,115,1,True)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 61 +Time : 455.097s (Solving: 434.28s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 455.148s + +Choices : 7122921 (Domain: 7024658) +Conflicts : 496782 (Analyzed: 496779) +Restarts : 5636 (Average: 88.14 Last: 176) +Model-Level : 115.0 +Problems : 61 (Average Length: 77.08 Splits: 0) +Lemmas : 496779 (Deleted: 466098) + Binary : 10405 (Ratio: 2.09%) + Ternary : 2963 (Ratio: 0.60%) + Conflict : 496779 (Average Length: 789.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 496779 (Average: 11.97 Max: 749 Sum: 5945292) + Executed : 496676 (Average: 11.96 Max: 749 Sum: 5942930 Ratio: 99.96%) + Bounded : 103 (Average: 22.93 Max: 107 Sum: 2362 Ratio: 0.04%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 595276 (Eliminated: 0 Frozen: 191082) +Constraints : 4426680 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 769MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.49s +Memory: 700MB (+0MB) +UNKNOWN +Iteration Time: 7.54s + +Iteration 61 +Queue: [(8,40,3,True), (9,45,3,True), (10,50,3,True), (11,55,3,False), (12,60,3,False), (13,65,3,False), (14,70,2,True), (15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,1,True), (23,115,1,True)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 62 +Time : 462.209s (Solving: 441.25s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 462.264s + +Choices : 7198787 (Domain: 7100519) +Conflicts : 505856 (Analyzed: 505853) +Restarts : 5736 (Average: 88.19 Last: 176) +Model-Level : 115.0 +Problems : 62 (Average Length: 77.73 Splits: 0) +Lemmas : 505853 (Deleted: 474538) + Binary : 10428 (Ratio: 2.06%) + Ternary : 2969 (Ratio: 0.59%) + Conflict : 505853 (Average Length: 791.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 505853 (Average: 11.87 Max: 749 Sum: 6001952) + Executed : 505750 (Average: 11.86 Max: 749 Sum: 5999590 Ratio: 99.96%) + Bounded : 103 (Average: 22.93 Max: 107 Sum: 2362 Ratio: 0.04%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 595276 (Eliminated: 0 Frozen: 191082) +Constraints : 4426680 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 769MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.06s +Memory: 700MB (+0MB) +UNKNOWN +Iteration Time: 7.12s + +Iteration 62 +Queue: [(9,45,3,True), (10,50,3,True), (11,55,3,False), (12,60,3,False), (13,65,3,False), (14,70,2,True), (15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,1,True), (23,115,1,True)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 63 +Time : 469.150s (Solving: 448.04s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 469.208s + +Choices : 7272724 (Domain: 7174386) +Conflicts : 514342 (Analyzed: 514339) +Restarts : 5836 (Average: 88.13 Last: 176) +Model-Level : 115.0 +Problems : 63 (Average Length: 78.35 Splits: 0) +Lemmas : 514339 (Deleted: 481691) + Binary : 10455 (Ratio: 2.03%) + Ternary : 2980 (Ratio: 0.58%) + Conflict : 514339 (Average Length: 794.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 514339 (Average: 11.77 Max: 749 Sum: 6053957) + Executed : 514236 (Average: 11.77 Max: 749 Sum: 6051595 Ratio: 99.96%) + Bounded : 103 (Average: 22.93 Max: 107 Sum: 2362 Ratio: 0.04%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 595276 (Eliminated: 0 Frozen: 191082) +Constraints : 4426680 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 769MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.89s +Memory: 700MB (+0MB) +UNKNOWN +Iteration Time: 6.95s + +Iteration 63 +Queue: [(10,50,3,True), (11,55,3,False), (12,60,3,False), (13,65,3,False), (14,70,2,True), (15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,1,True), (23,115,1,True)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 64 +Time : 477.697s (Solving: 456.43s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 477.760s + +Choices : 7362725 (Domain: 7264239) +Conflicts : 523723 (Analyzed: 523720) +Restarts : 5936 (Average: 88.23 Last: 176) +Model-Level : 115.0 +Problems : 64 (Average Length: 78.95 Splits: 0) +Lemmas : 523720 (Deleted: 491829) + Binary : 10520 (Ratio: 2.01%) + Ternary : 2985 (Ratio: 0.57%) + Conflict : 523720 (Average Length: 797.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 523720 (Average: 11.68 Max: 749 Sum: 6118029) + Executed : 523617 (Average: 11.68 Max: 749 Sum: 6115667 Ratio: 99.96%) + Bounded : 103 (Average: 22.93 Max: 107 Sum: 2362 Ratio: 0.04%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 595276 (Eliminated: 0 Frozen: 191082) +Constraints : 4426680 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 769MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.49s +Memory: 700MB (+0MB) +UNKNOWN +Iteration Time: 8.56s + +Iteration 64 +Queue: [(14,70,2,True), (15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,1,True), (23,115,1,True)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 65 +Time : 484.580s (Solving: 463.16s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 484.648s + +Choices : 7455974 (Domain: 7357475) +Conflicts : 532431 (Analyzed: 532428) +Restarts : 6036 (Average: 88.21 Last: 176) +Model-Level : 115.0 +Problems : 65 (Average Length: 79.54 Splits: 0) +Lemmas : 532428 (Deleted: 500996) + Binary : 10538 (Ratio: 1.98%) + Ternary : 2990 (Ratio: 0.56%) + Conflict : 532428 (Average Length: 796.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 532428 (Average: 11.62 Max: 749 Sum: 6188896) + Executed : 532325 (Average: 11.62 Max: 749 Sum: 6186534 Ratio: 99.96%) + Bounded : 103 (Average: 22.93 Max: 107 Sum: 2362 Ratio: 0.04%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 595276 (Eliminated: 0 Frozen: 191082) +Constraints : 4426680 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 769MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.82s +Memory: 700MB (+0MB) +UNKNOWN +Iteration Time: 6.89s + +Iteration 65 +Queue: [(15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,1,True), (23,115,1,True)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 66 +Time : 493.472s (Solving: 471.93s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 493.544s + +Choices : 7558100 (Domain: 7459590) +Conflicts : 541833 (Analyzed: 541830) +Restarts : 6136 (Average: 88.30 Last: 176) +Model-Level : 115.0 +Problems : 66 (Average Length: 80.11 Splits: 0) +Lemmas : 541830 (Deleted: 509587) + Binary : 10555 (Ratio: 1.95%) + Ternary : 2995 (Ratio: 0.55%) + Conflict : 541830 (Average Length: 800.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 541830 (Average: 11.56 Max: 749 Sum: 6263632) + Executed : 541727 (Average: 11.56 Max: 749 Sum: 6261270 Ratio: 99.96%) + Bounded : 103 (Average: 22.93 Max: 107 Sum: 2362 Ratio: 0.04%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 595276 (Eliminated: 0 Frozen: 191082) +Constraints : 4426680 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 769MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.86s +Memory: 700MB (+0MB) +UNKNOWN +Iteration Time: 8.90s + +Iteration 66 +Queue: [(22,110,1,True), (23,115,1,True)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 67 +Time : 504.803s (Solving: 483.11s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 504.880s + +Choices : 7708577 (Domain: 7609988) +Conflicts : 550913 (Analyzed: 550910) +Restarts : 6236 (Average: 88.34 Last: 176) +Model-Level : 115.0 +Problems : 67 (Average Length: 80.66 Splits: 0) +Lemmas : 550910 (Deleted: 518787) + Binary : 10620 (Ratio: 1.93%) + Ternary : 3005 (Ratio: 0.55%) + Conflict : 550910 (Average Length: 806.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 550910 (Average: 11.57 Max: 884 Sum: 6375079) + Executed : 550807 (Average: 11.57 Max: 884 Sum: 6372717 Ratio: 99.96%) + Bounded : 103 (Average: 22.93 Max: 107 Sum: 2362 Ratio: 0.04%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 595276 (Eliminated: 0 Frozen: 191082) +Constraints : 4426680 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 769MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 11.28s +Memory: 700MB (+0MB) +UNKNOWN +Iteration Time: 11.34s + +Iteration 67 +Queue: [(23,115,1,True)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 68 +Time : 515.350s (Solving: 493.53s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 515.428s + +Choices : 7822662 (Domain: 7724051) +Conflicts : 559761 (Analyzed: 559758) +Restarts : 6336 (Average: 88.35 Last: 176) +Model-Level : 115.0 +Problems : 68 (Average Length: 81.19 Splits: 0) +Lemmas : 559758 (Deleted: 527717) + Binary : 10654 (Ratio: 1.90%) + Ternary : 3010 (Ratio: 0.54%) + Conflict : 559758 (Average Length: 815.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 559758 (Average: 11.53 Max: 884 Sum: 6451365) + Executed : 559655 (Average: 11.52 Max: 884 Sum: 6449003 Ratio: 99.96%) + Bounded : 103 (Average: 22.93 Max: 107 Sum: 2362 Ratio: 0.04%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 595276 (Eliminated: 0 Frozen: 191082) +Constraints : 4426680 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 769MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 10.50s +Memory: 700MB (+0MB) +UNKNOWN +Iteration Time: 10.55s + +Iteration 68 +Queue: [(4,20,5,True), (5,25,5,True), (6,30,5,True), (7,35,4,True), (8,40,4,True), (9,45,4,True), (10,50,4,False), (11,55,3,True), (12,60,3,True), (13,65,3,False), (14,70,3,False), (15,75,3,False), (16,80,2,True), (17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Blocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 69 +Time : 517.562s (Solving: 495.60s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 517.640s + +Choices : 7856295 (Domain: 7757684) +Conflicts : 566780 (Analyzed: 566777) +Restarts : 6436 (Average: 88.06 Last: 176) +Model-Level : 115.0 +Problems : 69 (Average Length: 81.71 Splits: 0) +Lemmas : 566777 (Deleted: 534191) + Binary : 10696 (Ratio: 1.89%) + Ternary : 3011 (Ratio: 0.53%) + Conflict : 566777 (Average Length: 808.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 566777 (Average: 11.42 Max: 884 Sum: 6472036) + Executed : 566674 (Average: 11.41 Max: 884 Sum: 6469674 Ratio: 99.96%) + Bounded : 103 (Average: 22.93 Max: 107 Sum: 2362 Ratio: 0.04%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 595276 (Eliminated: 0 Frozen: 191082) +Constraints : 4426680 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 769MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 2.16s +Memory: 700MB (+0MB) +UNKNOWN +Iteration Time: 2.22s + +Iteration 69 +Queue: [(5,25,5,True), (6,30,5,True), (7,35,4,True), (8,40,4,True), (9,45,4,True), (10,50,4,False), (11,55,3,True), (12,60,3,True), (13,65,3,False), (14,70,3,False), (15,75,3,False), (16,80,2,True), (17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 70 +Time : 527.596s (Solving: 505.48s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 527.680s + +Choices : 7911967 (Domain: 7813356) +Conflicts : 576020 (Analyzed: 576017) +Restarts : 6536 (Average: 88.13 Last: 176) +Model-Level : 115.0 +Problems : 70 (Average Length: 82.21 Splits: 0) +Lemmas : 576017 (Deleted: 543296) + Binary : 10756 (Ratio: 1.87%) + Ternary : 3019 (Ratio: 0.52%) + Conflict : 576017 (Average Length: 815.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 576017 (Average: 11.31 Max: 884 Sum: 6512176) + Executed : 575914 (Average: 11.30 Max: 884 Sum: 6509814 Ratio: 99.96%) + Bounded : 103 (Average: 22.93 Max: 107 Sum: 2362 Ratio: 0.04%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 595276 (Eliminated: 0 Frozen: 191082) +Constraints : 4426680 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 769MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.98s +Memory: 700MB (+0MB) +UNKNOWN +Iteration Time: 10.04s + +Iteration 70 +Queue: [(6,30,5,True), (7,35,4,True), (8,40,4,True), (9,45,4,True), (10,50,4,False), (11,55,3,True), (12,60,3,True), (13,65,3,False), (14,70,3,False), (15,75,3,False), (16,80,2,True), (17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 71 +Time : 535.328s (Solving: 513.05s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 535.416s + +Choices : 7991315 (Domain: 7892704) +Conflicts : 584916 (Analyzed: 584913) +Restarts : 6636 (Average: 88.14 Last: 176) +Model-Level : 115.0 +Problems : 71 (Average Length: 82.70 Splits: 0) +Lemmas : 584913 (Deleted: 552337) + Binary : 10810 (Ratio: 1.85%) + Ternary : 3033 (Ratio: 0.52%) + Conflict : 584913 (Average Length: 815.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 584913 (Average: 11.24 Max: 884 Sum: 6572424) + Executed : 584810 (Average: 11.23 Max: 884 Sum: 6570062 Ratio: 99.96%) + Bounded : 103 (Average: 22.93 Max: 107 Sum: 2362 Ratio: 0.04%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 595276 (Eliminated: 0 Frozen: 191082) +Constraints : 4426680 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 769MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.67s +Memory: 700MB (+0MB) +UNKNOWN +Iteration Time: 7.74s + +Iteration 71 +Queue: [(7,35,4,True), (8,40,4,True), (9,45,4,True), (10,50,4,False), (11,55,3,True), (12,60,3,True), (13,65,3,False), (14,70,3,False), (15,75,3,False), (16,80,2,True), (17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 72 +Time : 542.157s (Solving: 519.76s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 542.248s + +Choices : 8056319 (Domain: 7957652) +Conflicts : 593180 (Analyzed: 593177) +Restarts : 6736 (Average: 88.06 Last: 176) +Model-Level : 115.0 +Problems : 72 (Average Length: 83.18 Splits: 0) +Lemmas : 593177 (Deleted: 558878) + Binary : 10849 (Ratio: 1.83%) + Ternary : 3046 (Ratio: 0.51%) + Conflict : 593177 (Average Length: 817.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 593177 (Average: 11.15 Max: 884 Sum: 6616372) + Executed : 593074 (Average: 11.15 Max: 884 Sum: 6614010 Ratio: 99.96%) + Bounded : 103 (Average: 22.93 Max: 107 Sum: 2362 Ratio: 0.04%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 595276 (Eliminated: 0 Frozen: 191082) +Constraints : 4426680 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 769MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.79s +Memory: 700MB (+0MB) +UNKNOWN +Iteration Time: 6.83s + +Iteration 72 +Queue: [(8,40,4,True), (9,45,4,True), (10,50,4,False), (11,55,3,True), (12,60,3,True), (13,65,3,False), (14,70,3,False), (15,75,3,False), (16,80,2,True), (17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 73 +Time : 549.003s (Solving: 526.47s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 549.096s + +Choices : 8121285 (Domain: 8022608) +Conflicts : 601538 (Analyzed: 601535) +Restarts : 6836 (Average: 88.00 Last: 176) +Model-Level : 115.0 +Problems : 73 (Average Length: 83.64 Splits: 0) +Lemmas : 601535 (Deleted: 567603) + Binary : 10876 (Ratio: 1.81%) + Ternary : 3048 (Ratio: 0.51%) + Conflict : 601535 (Average Length: 823.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 601535 (Average: 11.07 Max: 884 Sum: 6658061) + Executed : 601432 (Average: 11.06 Max: 884 Sum: 6655699 Ratio: 99.96%) + Bounded : 103 (Average: 22.93 Max: 107 Sum: 2362 Ratio: 0.04%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 595276 (Eliminated: 0 Frozen: 191082) +Constraints : 4426680 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 769MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.80s +Memory: 700MB (+0MB) +UNKNOWN +Iteration Time: 6.85s + +Iteration 73 +Queue: [(9,45,4,True), (10,50,4,False), (11,55,3,True), (12,60,3,True), (13,65,3,False), (14,70,3,False), (15,75,3,False), (16,80,2,True), (17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 74 +Time : 556.355s (Solving: 533.67s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 556.448s + +Choices : 8200333 (Domain: 8101633) +Conflicts : 610522 (Analyzed: 610519) +Restarts : 6936 (Average: 88.02 Last: 176) +Model-Level : 115.0 +Problems : 74 (Average Length: 84.09 Splits: 0) +Lemmas : 610519 (Deleted: 577334) + Binary : 10897 (Ratio: 1.78%) + Ternary : 3052 (Ratio: 0.50%) + Conflict : 610519 (Average Length: 824.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 610519 (Average: 11.00 Max: 884 Sum: 6717745) + Executed : 610416 (Average: 11.00 Max: 884 Sum: 6715383 Ratio: 99.96%) + Bounded : 103 (Average: 22.93 Max: 107 Sum: 2362 Ratio: 0.04%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 595276 (Eliminated: 0 Frozen: 191082) +Constraints : 4426680 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 769MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.29s +Memory: 700MB (+0MB) +UNKNOWN +Iteration Time: 7.36s + +Iteration 74 +Queue: [(11,55,3,True), (12,60,3,True), (13,65,3,False), (14,70,3,False), (15,75,3,False), (16,80,2,True), (17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 75 +Time : 563.409s (Solving: 540.61s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 563.504s + +Choices : 8268354 (Domain: 8169647) +Conflicts : 619341 (Analyzed: 619338) +Restarts : 7036 (Average: 88.02 Last: 176) +Model-Level : 115.0 +Problems : 75 (Average Length: 84.53 Splits: 0) +Lemmas : 619338 (Deleted: 586203) + Binary : 10914 (Ratio: 1.76%) + Ternary : 3054 (Ratio: 0.49%) + Conflict : 619338 (Average Length: 826.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 619338 (Average: 10.92 Max: 884 Sum: 6761958) + Executed : 619235 (Average: 10.91 Max: 884 Sum: 6759596 Ratio: 99.97%) + Bounded : 103 (Average: 22.93 Max: 107 Sum: 2362 Ratio: 0.03%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 595276 (Eliminated: 0 Frozen: 191082) +Constraints : 4426680 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 769MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.02s +Memory: 700MB (+0MB) +UNKNOWN +Iteration Time: 7.06s + +Iteration 75 +Queue: [(12,60,3,True), (13,65,3,False), (14,70,3,False), (15,75,3,False), (16,80,2,True), (17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 76 +Time : 571.635s (Solving: 548.70s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 571.732s + +Choices : 8354981 (Domain: 8256228) +Conflicts : 628143 (Analyzed: 628140) +Restarts : 7136 (Average: 88.02 Last: 176) +Model-Level : 115.0 +Problems : 76 (Average Length: 84.96 Splits: 0) +Lemmas : 628140 (Deleted: 594837) + Binary : 10970 (Ratio: 1.75%) + Ternary : 3059 (Ratio: 0.49%) + Conflict : 628140 (Average Length: 828.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 628140 (Average: 10.86 Max: 884 Sum: 6823667) + Executed : 628037 (Average: 10.86 Max: 884 Sum: 6821305 Ratio: 99.97%) + Bounded : 103 (Average: 22.93 Max: 107 Sum: 2362 Ratio: 0.03%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 595276 (Eliminated: 0 Frozen: 191082) +Constraints : 4426680 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 769MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.18s +Memory: 700MB (+0MB) +UNKNOWN +Iteration Time: 8.23s + +Iteration 76 +Queue: [(16,80,2,True), (17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 77 +Time : 580.142s (Solving: 557.06s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 580.244s + +Choices : 8455109 (Domain: 8356291) +Conflicts : 636973 (Analyzed: 636970) +Restarts : 7236 (Average: 88.03 Last: 176) +Model-Level : 115.0 +Problems : 77 (Average Length: 85.38 Splits: 0) +Lemmas : 636970 (Deleted: 603515) + Binary : 11021 (Ratio: 1.73%) + Ternary : 3065 (Ratio: 0.48%) + Conflict : 636970 (Average Length: 830.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 636970 (Average: 10.82 Max: 884 Sum: 6892840) + Executed : 636867 (Average: 10.82 Max: 884 Sum: 6890478 Ratio: 99.97%) + Bounded : 103 (Average: 22.93 Max: 107 Sum: 2362 Ratio: 0.03%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 595276 (Eliminated: 0 Frozen: 191082) +Constraints : 4426680 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 769MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.46s +Memory: 700MB (+0MB) +UNKNOWN +Iteration Time: 8.51s + +Iteration 77 +Queue: [(17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 78 +Time : 590.510s (Solving: 567.28s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 590.616s + +Choices : 8670102 (Domain: 8570341) +Conflicts : 645928 (Analyzed: 645925) +Restarts : 7336 (Average: 88.05 Last: 176) +Model-Level : 115.0 +Problems : 78 (Average Length: 85.78 Splits: 0) +Lemmas : 645925 (Deleted: 612071) + Binary : 11164 (Ratio: 1.73%) + Ternary : 3090 (Ratio: 0.48%) + Conflict : 645925 (Average Length: 834.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 645925 (Average: 10.95 Max: 884 Sum: 7070245) + Executed : 645822 (Average: 10.94 Max: 884 Sum: 7067883 Ratio: 99.97%) + Bounded : 103 (Average: 22.93 Max: 107 Sum: 2362 Ratio: 0.03%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 595276 (Eliminated: 0 Frozen: 191082) +Constraints : 4426680 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 769MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 10.32s +Memory: 700MB (+0MB) +UNKNOWN +Iteration Time: 10.38s + +Iteration 78 +Queue: [(4,20,6,True), (5,25,6,True), (6,30,6,True), (7,35,5,True), (8,40,5,True), (9,45,5,False), (10,50,4,True), (11,55,4,False), (12,60,4,False), (13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,3,False), (17,85,3,False), (18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Blocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 79 +Time : 594.386s (Solving: 571.03s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 594.492s + +Choices : 8720847 (Domain: 8621086) +Conflicts : 653996 (Analyzed: 653993) +Restarts : 7436 (Average: 87.95 Last: 176) +Model-Level : 115.0 +Problems : 79 (Average Length: 86.18 Splits: 0) +Lemmas : 653993 (Deleted: 618602) + Binary : 11206 (Ratio: 1.71%) + Ternary : 3095 (Ratio: 0.47%) + Conflict : 653993 (Average Length: 827.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 653993 (Average: 10.88 Max: 884 Sum: 7114161) + Executed : 653890 (Average: 10.87 Max: 884 Sum: 7111799 Ratio: 99.97%) + Bounded : 103 (Average: 22.93 Max: 107 Sum: 2362 Ratio: 0.03%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 595276 (Eliminated: 0 Frozen: 191082) +Constraints : 4426680 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 769MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 3.83s +Memory: 700MB (+0MB) +UNKNOWN +Iteration Time: 3.88s + +Iteration 79 +Queue: [(5,25,6,True), (6,30,6,True), (7,35,5,True), (8,40,5,True), (9,45,5,False), (10,50,4,True), (11,55,4,False), (12,60,4,False), (13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,3,False), (17,85,3,False), (18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 80 +Time : 605.387s (Solving: 581.87s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 605.500s + +Choices : 8770208 (Domain: 8670447) +Conflicts : 663385 (Analyzed: 663382) +Restarts : 7536 (Average: 88.03 Last: 176) +Model-Level : 115.0 +Problems : 80 (Average Length: 86.56 Splits: 0) +Lemmas : 663382 (Deleted: 628663) + Binary : 11237 (Ratio: 1.69%) + Ternary : 3109 (Ratio: 0.47%) + Conflict : 663382 (Average Length: 833.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 663382 (Average: 10.78 Max: 884 Sum: 7149617) + Executed : 663279 (Average: 10.77 Max: 884 Sum: 7147255 Ratio: 99.97%) + Bounded : 103 (Average: 22.93 Max: 107 Sum: 2362 Ratio: 0.03%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 595276 (Eliminated: 0 Frozen: 191082) +Constraints : 4426680 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 769MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 10.94s +Memory: 700MB (+0MB) +UNKNOWN +Iteration Time: 11.01s + +Iteration 80 +Queue: [(6,30,6,True), (7,35,5,True), (8,40,5,True), (9,45,5,False), (10,50,4,True), (11,55,4,False), (12,60,4,False), (13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,3,False), (17,85,3,False), (18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 81 +Time : 613.702s (Solving: 590.03s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 613.820s + +Choices : 8846995 (Domain: 8747234) +Conflicts : 672499 (Analyzed: 672496) +Restarts : 7636 (Average: 88.07 Last: 176) +Model-Level : 115.0 +Problems : 81 (Average Length: 86.94 Splits: 0) +Lemmas : 672496 (Deleted: 637884) + Binary : 11266 (Ratio: 1.68%) + Ternary : 3115 (Ratio: 0.46%) + Conflict : 672496 (Average Length: 836.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 672496 (Average: 10.72 Max: 884 Sum: 7207054) + Executed : 672393 (Average: 10.71 Max: 884 Sum: 7204692 Ratio: 99.97%) + Bounded : 103 (Average: 22.93 Max: 107 Sum: 2362 Ratio: 0.03%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 595276 (Eliminated: 0 Frozen: 191082) +Constraints : 4426680 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 769MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.26s +Memory: 700MB (+0MB) +UNKNOWN +Iteration Time: 8.32s + +Iteration 81 +Queue: [(7,35,5,True), (8,40,5,True), (9,45,5,False), (10,50,4,True), (11,55,4,False), (12,60,4,False), (13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,3,False), (17,85,3,False), (18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 82 +Time : 621.511s (Solving: 597.68s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 621.632s + +Choices : 8925951 (Domain: 8826184) +Conflicts : 681301 (Analyzed: 681298) +Restarts : 7736 (Average: 88.07 Last: 176) +Model-Level : 115.0 +Problems : 82 (Average Length: 87.30 Splits: 0) +Lemmas : 681298 (Deleted: 646697) + Binary : 11417 (Ratio: 1.68%) + Ternary : 3143 (Ratio: 0.46%) + Conflict : 681298 (Average Length: 836.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 681298 (Average: 10.66 Max: 884 Sum: 7265975) + Executed : 681195 (Average: 10.66 Max: 884 Sum: 7263613 Ratio: 99.97%) + Bounded : 103 (Average: 22.93 Max: 107 Sum: 2362 Ratio: 0.03%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 595276 (Eliminated: 0 Frozen: 191082) +Constraints : 4426680 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 769MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.75s +Memory: 700MB (+0MB) +UNKNOWN +Iteration Time: 7.82s + +Iteration 82 +Queue: [(8,40,5,True), (9,45,5,False), (10,50,4,True), (11,55,4,False), (12,60,4,False), (13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,3,False), (17,85,3,False), (18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 83 +Time : 628.899s (Solving: 604.93s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 629.024s + +Choices : 9002710 (Domain: 8902814) +Conflicts : 690243 (Analyzed: 690240) +Restarts : 7836 (Average: 88.09 Last: 176) +Model-Level : 115.0 +Problems : 83 (Average Length: 87.66 Splits: 0) +Lemmas : 690240 (Deleted: 655282) + Binary : 11456 (Ratio: 1.66%) + Ternary : 3149 (Ratio: 0.46%) + Conflict : 690240 (Average Length: 840.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 690240 (Average: 10.61 Max: 884 Sum: 7320411) + Executed : 690137 (Average: 10.60 Max: 884 Sum: 7318049 Ratio: 99.97%) + Bounded : 103 (Average: 22.93 Max: 107 Sum: 2362 Ratio: 0.03%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 595276 (Eliminated: 0 Frozen: 191082) +Constraints : 4426680 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 769MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.34s +Memory: 700MB (+0MB) +UNKNOWN +Iteration Time: 7.40s + +Iteration 83 +Queue: [(10,50,4,True), (11,55,4,False), (12,60,4,False), (13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,3,False), (17,85,3,False), (18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 84 +Time : 637.746s (Solving: 613.62s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 637.872s + +Choices : 9089071 (Domain: 8989028) +Conflicts : 699684 (Analyzed: 699681) +Restarts : 7936 (Average: 88.17 Last: 176) +Model-Level : 115.0 +Problems : 84 (Average Length: 88.01 Splits: 0) +Lemmas : 699681 (Deleted: 664032) + Binary : 11504 (Ratio: 1.64%) + Ternary : 3153 (Ratio: 0.45%) + Conflict : 699681 (Average Length: 844.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 699681 (Average: 10.55 Max: 884 Sum: 7382641) + Executed : 699578 (Average: 10.55 Max: 884 Sum: 7380279 Ratio: 99.97%) + Bounded : 103 (Average: 22.93 Max: 107 Sum: 2362 Ratio: 0.03%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 595276 (Eliminated: 0 Frozen: 191082) +Constraints : 4426680 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 769MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.79s +Memory: 700MB (+0MB) +UNKNOWN +Iteration Time: 8.85s + +Iteration 84 +Queue: [(13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,3,False), (17,85,3,False), (18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 85 +Time : 647.062s (Solving: 622.82s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 647.192s + +Choices : 9230228 (Domain: 9129316) +Conflicts : 708716 (Analyzed: 708713) +Restarts : 8036 (Average: 88.19 Last: 176) +Model-Level : 115.0 +Problems : 85 (Average Length: 88.35 Splits: 0) +Lemmas : 708713 (Deleted: 673175) + Binary : 11622 (Ratio: 1.64%) + Ternary : 3172 (Ratio: 0.45%) + Conflict : 708713 (Average Length: 851.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 708713 (Average: 10.57 Max: 884 Sum: 7489278) + Executed : 708610 (Average: 10.56 Max: 884 Sum: 7486916 Ratio: 99.97%) + Bounded : 103 (Average: 22.93 Max: 107 Sum: 2362 Ratio: 0.03%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 595276 (Eliminated: 0 Frozen: 191082) +Constraints : 4426680 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 769MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.28s +Memory: 700MB (+0MB) +UNKNOWN +Iteration Time: 9.32s + +Iteration 85 +Queue: [(18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 86 +Time : 655.120s (Solving: 630.72s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 655.256s + +Choices : 9308761 (Domain: 9207849) +Conflicts : 717324 (Analyzed: 717321) +Restarts : 8136 (Average: 88.17 Last: 176) +Model-Level : 115.0 +Problems : 86 (Average Length: 88.69 Splits: 0) +Lemmas : 717321 (Deleted: 679856) + Binary : 11658 (Ratio: 1.63%) + Ternary : 3174 (Ratio: 0.44%) + Conflict : 717321 (Average Length: 853.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 717321 (Average: 10.51 Max: 884 Sum: 7535673) + Executed : 717218 (Average: 10.50 Max: 884 Sum: 7533311 Ratio: 99.97%) + Bounded : 103 (Average: 22.93 Max: 107 Sum: 2362 Ratio: 0.03%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 595276 (Eliminated: 0 Frozen: 191082) +Constraints : 4426680 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 769MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.01s +Memory: 700MB (+0MB) +UNKNOWN +Iteration Time: 8.06s + +Iteration 86 +Queue: [(4,20,7,True), (5,25,7,True), (6,30,7,False), (7,35,6,True), (8,40,6,False), (9,45,5,True), (10,50,5,False), (11,55,4,True), (12,60,4,False), (13,65,4,False), (14,70,3,True), (15,75,3,True), (16,80,3,False), (17,85,3,False), (18,90,3,False), (19,95,2,True), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Blocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 87 +Time : 657.278s (Solving: 632.74s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 657.412s + +Choices : 9343687 (Domain: 9242775) +Conflicts : 724383 (Analyzed: 724380) +Restarts : 8236 (Average: 87.95 Last: 176) +Model-Level : 115.0 +Problems : 87 (Average Length: 89.01 Splits: 0) +Lemmas : 724380 (Deleted: 688362) + Binary : 11693 (Ratio: 1.61%) + Ternary : 3175 (Ratio: 0.44%) + Conflict : 724380 (Average Length: 848.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 724380 (Average: 10.43 Max: 884 Sum: 7558268) + Executed : 724276 (Average: 10.43 Max: 884 Sum: 7555789 Ratio: 99.97%) + Bounded : 104 (Average: 23.84 Max: 117 Sum: 2479 Ratio: 0.03%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 595276 (Eliminated: 0 Frozen: 191082) +Constraints : 4426680 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 769MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 2.11s +Memory: 700MB (+0MB) +UNKNOWN +Iteration Time: 2.16s + +Iteration 87 +Queue: [(5,25,7,True), (6,30,7,False), (7,35,6,True), (8,40,6,False), (9,45,5,True), (10,50,5,False), (11,55,4,True), (12,60,4,False), (13,65,4,False), (14,70,3,True), (15,75,3,True), (16,80,3,False), (17,85,3,False), (18,90,3,False), (19,95,2,True), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 88 +Time : 666.974s (Solving: 642.31s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 667.112s + +Choices : 9385555 (Domain: 9284643) +Conflicts : 732647 (Analyzed: 732644) +Restarts : 8336 (Average: 87.89 Last: 176) +Model-Level : 115.0 +Problems : 88 (Average Length: 89.33 Splits: 0) +Lemmas : 732644 (Deleted: 695318) + Binary : 11713 (Ratio: 1.60%) + Ternary : 3184 (Ratio: 0.43%) + Conflict : 732644 (Average Length: 851.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 732644 (Average: 10.36 Max: 884 Sum: 7587815) + Executed : 732540 (Average: 10.35 Max: 884 Sum: 7585336 Ratio: 99.97%) + Bounded : 104 (Average: 23.84 Max: 117 Sum: 2479 Ratio: 0.03%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 595276 (Eliminated: 0 Frozen: 191082) +Constraints : 4426666 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 769MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.66s +Memory: 700MB (+0MB) +UNKNOWN +Iteration Time: 9.70s + +Iteration 88 +Queue: [(7,35,6,True), (8,40,6,False), (9,45,5,True), (10,50,5,False), (11,55,4,True), (12,60,4,False), (13,65,4,False), (14,70,3,True), (15,75,3,True), (16,80,3,False), (17,85,3,False), (18,90,3,False), (19,95,2,True), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 89 +Time : 674.341s (Solving: 649.52s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 674.484s + +Choices : 9458598 (Domain: 9357685) +Conflicts : 741747 (Analyzed: 741744) +Restarts : 8436 (Average: 87.93 Last: 176) +Model-Level : 115.0 +Problems : 89 (Average Length: 89.64 Splits: 0) +Lemmas : 741744 (Deleted: 705625) + Binary : 11760 (Ratio: 1.59%) + Ternary : 3192 (Ratio: 0.43%) + Conflict : 741744 (Average Length: 852.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 741744 (Average: 10.30 Max: 884 Sum: 7639661) + Executed : 741640 (Average: 10.30 Max: 884 Sum: 7637182 Ratio: 99.97%) + Bounded : 104 (Average: 23.84 Max: 117 Sum: 2479 Ratio: 0.03%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 595276 (Eliminated: 0 Frozen: 191082) +Constraints : 4426666 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 769MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.31s +Memory: 700MB (+0MB) +UNKNOWN +Iteration Time: 7.37s + +Iteration 89 +Queue: [(9,45,5,True), (10,50,5,False), (11,55,4,True), (12,60,4,False), (13,65,4,False), (14,70,3,True), (15,75,3,True), (16,80,3,False), (17,85,3,False), (18,90,3,False), (19,95,2,True), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 90 +Time : 681.506s (Solving: 656.56s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 681.652s + +Choices : 9527119 (Domain: 9425857) +Conflicts : 750262 (Analyzed: 750259) +Restarts : 8536 (Average: 87.89 Last: 176) +Model-Level : 115.0 +Problems : 90 (Average Length: 89.94 Splits: 0) +Lemmas : 750259 (Deleted: 712430) + Binary : 11788 (Ratio: 1.57%) + Ternary : 3196 (Ratio: 0.43%) + Conflict : 750259 (Average Length: 854.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 750259 (Average: 10.24 Max: 884 Sum: 7684480) + Executed : 750155 (Average: 10.24 Max: 884 Sum: 7682001 Ratio: 99.97%) + Bounded : 104 (Average: 23.84 Max: 117 Sum: 2479 Ratio: 0.03%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 595276 (Eliminated: 0 Frozen: 191082) +Constraints : 4426666 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 769MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.13s +Memory: 700MB (+0MB) +UNKNOWN +Iteration Time: 7.17s + +Iteration 90 +Queue: [(11,55,4,True), (12,60,4,False), (13,65,4,False), (14,70,3,True), (15,75,3,True), (16,80,3,False), (17,85,3,False), (18,90,3,False), (19,95,2,True), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 91 +Time : 690.376s (Solving: 665.29s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 690.524s + +Choices : 9625951 (Domain: 9524562) +Conflicts : 759471 (Analyzed: 759468) +Restarts : 8636 (Average: 87.94 Last: 176) +Model-Level : 115.0 +Problems : 91 (Average Length: 90.24 Splits: 0) +Lemmas : 759468 (Deleted: 722922) + Binary : 11918 (Ratio: 1.57%) + Ternary : 3218 (Ratio: 0.42%) + Conflict : 759468 (Average Length: 855.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 759468 (Average: 10.21 Max: 884 Sum: 7756224) + Executed : 759364 (Average: 10.21 Max: 884 Sum: 7753745 Ratio: 99.97%) + Bounded : 104 (Average: 23.84 Max: 117 Sum: 2479 Ratio: 0.03%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 595276 (Eliminated: 0 Frozen: 191082) +Constraints : 4426666 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 769MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.82s +Memory: 700MB (+0MB) +UNKNOWN +Iteration Time: 8.88s + +Iteration 91 +Queue: [(14,70,3,True), (15,75,3,True), (16,80,3,False), (17,85,3,False), (18,90,3,False), (19,95,2,True), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 92 +Time : 698.394s (Solving: 673.19s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 698.548s + +Choices : 9732903 (Domain: 9630883) +Conflicts : 768019 (Analyzed: 768016) +Restarts : 8736 (Average: 87.91 Last: 176) +Model-Level : 115.0 +Problems : 92 (Average Length: 90.53 Splits: 0) +Lemmas : 768016 (Deleted: 729713) + Binary : 11950 (Ratio: 1.56%) + Ternary : 3241 (Ratio: 0.42%) + Conflict : 768016 (Average Length: 857.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 768016 (Average: 10.20 Max: 884 Sum: 7832757) + Executed : 767912 (Average: 10.20 Max: 884 Sum: 7830278 Ratio: 99.97%) + Bounded : 104 (Average: 23.84 Max: 117 Sum: 2479 Ratio: 0.03%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 595276 (Eliminated: 0 Frozen: 191082) +Constraints : 4426666 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 769MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.98s +Memory: 700MB (+0MB) +UNKNOWN +Iteration Time: 8.02s + +Iteration 92 +Queue: [(15,75,3,True), (16,80,3,False), (17,85,3,False), (18,90,3,False), (19,95,2,True), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 93 +Time : 706.583s (Solving: 681.24s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 706.740s + +Choices : 9808985 (Domain: 9706947) +Conflicts : 776680 (Analyzed: 776677) +Restarts : 8836 (Average: 87.90 Last: 176) +Model-Level : 115.0 +Problems : 93 (Average Length: 90.82 Splits: 0) +Lemmas : 776677 (Deleted: 740182) + Binary : 12067 (Ratio: 1.55%) + Ternary : 3252 (Ratio: 0.42%) + Conflict : 776677 (Average Length: 860.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 776677 (Average: 10.15 Max: 884 Sum: 7880517) + Executed : 776573 (Average: 10.14 Max: 884 Sum: 7878038 Ratio: 99.97%) + Bounded : 104 (Average: 23.84 Max: 117 Sum: 2479 Ratio: 0.03%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 595276 (Eliminated: 0 Frozen: 191082) +Constraints : 4426666 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 769MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.14s +Memory: 700MB (+0MB) +UNKNOWN +Iteration Time: 8.20s + +Iteration 93 +Queue: [(19,95,2,True), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 94 +Time : 714.608s (Solving: 689.12s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 714.768s + +Choices : 9892255 (Domain: 9790195) +Conflicts : 784975 (Analyzed: 784972) +Restarts : 8936 (Average: 87.84 Last: 176) +Model-Level : 115.0 +Problems : 94 (Average Length: 91.10 Splits: 0) +Lemmas : 784972 (Deleted: 746453) + Binary : 12112 (Ratio: 1.54%) + Ternary : 3258 (Ratio: 0.42%) + Conflict : 784972 (Average Length: 861.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 784972 (Average: 10.10 Max: 884 Sum: 7931104) + Executed : 784868 (Average: 10.10 Max: 884 Sum: 7928625 Ratio: 99.97%) + Bounded : 104 (Average: 23.84 Max: 117 Sum: 2479 Ratio: 0.03%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 595276 (Eliminated: 0 Frozen: 191082) +Constraints : 4426666 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 769MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.97s +Memory: 700MB (+0MB) +UNKNOWN +Iteration Time: 8.03s + +Iteration 94 +Queue: [(4,20,8,True), (5,25,8,True), (6,30,7,True), (7,35,7,True), (8,40,6,True), (9,45,6,False), (10,50,5,True), (11,55,5,False), (12,60,4,True), (13,65,4,False), (14,70,4,False), (15,75,4,False), (16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,True), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Blocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 95 +Time : 718.227s (Solving: 692.61s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 718.388s + +Choices : 9944180 (Domain: 9842120) +Conflicts : 793181 (Analyzed: 793178) +Restarts : 9036 (Average: 87.78 Last: 176) +Model-Level : 115.0 +Problems : 95 (Average Length: 91.37 Splits: 0) +Lemmas : 793178 (Deleted: 754533) + Binary : 12156 (Ratio: 1.53%) + Ternary : 3262 (Ratio: 0.41%) + Conflict : 793178 (Average Length: 854.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 793178 (Average: 10.06 Max: 884 Sum: 7975866) + Executed : 793074 (Average: 10.05 Max: 884 Sum: 7973387 Ratio: 99.97%) + Bounded : 104 (Average: 23.84 Max: 117 Sum: 2479 Ratio: 0.03%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 595276 (Eliminated: 0 Frozen: 191082) +Constraints : 4426666 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 769MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 3.58s +Memory: 700MB (+0MB) +UNKNOWN +Iteration Time: 3.62s + +Iteration 95 +Queue: [(5,25,8,True), (6,30,7,True), (7,35,7,True), (8,40,6,True), (9,45,6,False), (10,50,5,True), (11,55,5,False), (12,60,4,True), (13,65,4,False), (14,70,4,False), (15,75,4,False), (16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,True), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 96 +Time : 728.241s (Solving: 702.50s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 728.408s + +Choices : 9995169 (Domain: 9893109) +Conflicts : 802572 (Analyzed: 802569) +Restarts : 9136 (Average: 87.85 Last: 176) +Model-Level : 115.0 +Problems : 96 (Average Length: 91.64 Splits: 0) +Lemmas : 802569 (Deleted: 764792) + Binary : 12191 (Ratio: 1.52%) + Ternary : 3272 (Ratio: 0.41%) + Conflict : 802569 (Average Length: 860.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 802569 (Average: 9.98 Max: 884 Sum: 8012887) + Executed : 802465 (Average: 9.98 Max: 884 Sum: 8010408 Ratio: 99.97%) + Bounded : 104 (Average: 23.84 Max: 117 Sum: 2479 Ratio: 0.03%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 595276 (Eliminated: 0 Frozen: 191082) +Constraints : 4426666 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 769MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.98s +Memory: 700MB (+0MB) +UNKNOWN +Iteration Time: 10.02s + +Iteration 96 +Queue: [(6,30,7,True), (7,35,7,True), (8,40,6,True), (9,45,6,False), (10,50,5,True), (11,55,5,False), (12,60,4,True), (13,65,4,False), (14,70,4,False), (15,75,4,False), (16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,True), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 97 +Time : 736.820s (Solving: 710.96s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 736.988s + +Choices : 10067176 (Domain: 9965116) +Conflicts : 811784 (Analyzed: 811781) +Restarts : 9236 (Average: 87.89 Last: 176) +Model-Level : 115.0 +Problems : 97 (Average Length: 91.90 Splits: 0) +Lemmas : 811781 (Deleted: 774096) + Binary : 12215 (Ratio: 1.50%) + Ternary : 3279 (Ratio: 0.40%) + Conflict : 811781 (Average Length: 861.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 811781 (Average: 9.94 Max: 884 Sum: 8065751) + Executed : 811677 (Average: 9.93 Max: 884 Sum: 8063272 Ratio: 99.97%) + Bounded : 104 (Average: 23.84 Max: 117 Sum: 2479 Ratio: 0.03%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 595276 (Eliminated: 0 Frozen: 191082) +Constraints : 4426666 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 769MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.54s +Memory: 700MB (+0MB) +UNKNOWN +Iteration Time: 8.58s + +Iteration 97 +Queue: [(7,35,7,True), (8,40,6,True), (9,45,6,False), (10,50,5,True), (11,55,5,False), (12,60,4,True), (13,65,4,False), (14,70,4,False), (15,75,4,False), (16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,True), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 98 +Time : 743.488s (Solving: 717.50s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 743.660s + +Choices : 10130739 (Domain: 10028679) +Conflicts : 820945 (Analyzed: 820942) +Restarts : 9336 (Average: 87.93 Last: 176) +Model-Level : 115.0 +Problems : 98 (Average Length: 92.15 Splits: 0) +Lemmas : 820942 (Deleted: 783175) + Binary : 12220 (Ratio: 1.49%) + Ternary : 3283 (Ratio: 0.40%) + Conflict : 820942 (Average Length: 861.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 820942 (Average: 9.88 Max: 884 Sum: 8109096) + Executed : 820838 (Average: 9.87 Max: 884 Sum: 8106617 Ratio: 99.97%) + Bounded : 104 (Average: 23.84 Max: 117 Sum: 2479 Ratio: 0.03%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 595276 (Eliminated: 0 Frozen: 191082) +Constraints : 4426666 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 769MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.62s +Memory: 700MB (+0MB) +UNKNOWN +Iteration Time: 6.67s + +Iteration 98 +Queue: [(8,40,6,True), (9,45,6,False), (10,50,5,True), (11,55,5,False), (12,60,4,True), (13,65,4,False), (14,70,4,False), (15,75,4,False), (16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,True), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 99 +Time : 751.141s (Solving: 725.00s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 751.316s + +Choices : 10199943 (Domain: 10097869) +Conflicts : 830296 (Analyzed: 830293) +Restarts : 9436 (Average: 87.99 Last: 176) +Model-Level : 115.0 +Problems : 99 (Average Length: 92.40 Splits: 0) +Lemmas : 830293 (Deleted: 792217) + Binary : 12258 (Ratio: 1.48%) + Ternary : 3290 (Ratio: 0.40%) + Conflict : 830293 (Average Length: 862.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 830293 (Average: 9.83 Max: 884 Sum: 8158843) + Executed : 830189 (Average: 9.82 Max: 884 Sum: 8156364 Ratio: 99.97%) + Bounded : 104 (Average: 23.84 Max: 117 Sum: 2479 Ratio: 0.03%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 595276 (Eliminated: 0 Frozen: 191082) +Constraints : 4426666 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 769MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.60s +Memory: 700MB (+0MB) +UNKNOWN +Iteration Time: 7.66s + +Iteration 99 +Queue: [(10,50,5,True), (11,55,5,False), (12,60,4,True), (13,65,4,False), (14,70,4,False), (15,75,4,False), (16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,True), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 100 +Time : 759.312s (Solving: 733.01s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 759.492s + +Choices : 10279045 (Domain: 10176913) +Conflicts : 839359 (Analyzed: 839356) +Restarts : 9536 (Average: 88.02 Last: 176) +Model-Level : 115.0 +Problems : 100 (Average Length: 92.65 Splits: 0) +Lemmas : 839356 (Deleted: 801411) + Binary : 12285 (Ratio: 1.46%) + Ternary : 3297 (Ratio: 0.39%) + Conflict : 839356 (Average Length: 865.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 839356 (Average: 9.79 Max: 884 Sum: 8214205) + Executed : 839252 (Average: 9.78 Max: 884 Sum: 8211726 Ratio: 99.97%) + Bounded : 104 (Average: 23.84 Max: 117 Sum: 2479 Ratio: 0.03%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 595276 (Eliminated: 0 Frozen: 191082) +Constraints : 4426666 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 769MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.11s +Memory: 700MB (+0MB) +UNKNOWN +Iteration Time: 8.18s + +Iteration 100 +Queue: [(12,60,4,True), (13,65,4,False), (14,70,4,False), (15,75,4,False), (16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,True), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 101 +Time : 766.569s (Solving: 740.14s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 766.752s + +Choices : 10345247 (Domain: 10243114) +Conflicts : 847874 (Analyzed: 847871) +Restarts : 9636 (Average: 87.99 Last: 176) +Model-Level : 115.0 +Problems : 101 (Average Length: 92.89 Splits: 0) +Lemmas : 847871 (Deleted: 808255) + Binary : 12301 (Ratio: 1.45%) + Ternary : 3298 (Ratio: 0.39%) + Conflict : 847871 (Average Length: 868.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 847871 (Average: 9.74 Max: 884 Sum: 8255882) + Executed : 847767 (Average: 9.73 Max: 884 Sum: 8253403 Ratio: 99.97%) + Bounded : 104 (Average: 23.84 Max: 117 Sum: 2479 Ratio: 0.03%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 595276 (Eliminated: 0 Frozen: 191082) +Constraints : 4426666 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 769MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.22s +Memory: 700MB (+0MB) +UNKNOWN +Iteration Time: 7.26s + +Iteration 101 +Queue: [(16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,True), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 102 +Time : 774.707s (Solving: 748.11s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 774.892s + +Choices : 10433019 (Domain: 10330857) +Conflicts : 856819 (Analyzed: 856816) +Restarts : 9736 (Average: 88.00 Last: 176) +Model-Level : 115.0 +Problems : 102 (Average Length: 93.13 Splits: 0) +Lemmas : 856816 (Deleted: 818675) + Binary : 12331 (Ratio: 1.44%) + Ternary : 3303 (Ratio: 0.39%) + Conflict : 856816 (Average Length: 869.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 856816 (Average: 9.71 Max: 884 Sum: 8317349) + Executed : 856712 (Average: 9.70 Max: 884 Sum: 8314870 Ratio: 99.97%) + Bounded : 104 (Average: 23.84 Max: 117 Sum: 2479 Ratio: 0.03%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 595276 (Eliminated: 0 Frozen: 191082) +Constraints : 4426666 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 769MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.07s +Memory: 700MB (+0MB) +UNKNOWN +Iteration Time: 8.14s + +Iteration 102 +Queue: [(20,100,2,True), (21,105,2,True), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 103 +Time : 783.987s (Solving: 757.25s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 784.180s + +Choices : 10524794 (Domain: 10422606) +Conflicts : 865849 (Analyzed: 865846) +Restarts : 9836 (Average: 88.03 Last: 206) +Model-Level : 115.0 +Problems : 103 (Average Length: 93.36 Splits: 0) +Lemmas : 865846 (Deleted: 827530) + Binary : 12363 (Ratio: 1.43%) + Ternary : 3307 (Ratio: 0.38%) + Conflict : 865846 (Average Length: 872.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 865846 (Average: 9.67 Max: 884 Sum: 8371246) + Executed : 865742 (Average: 9.67 Max: 884 Sum: 8368767 Ratio: 99.97%) + Bounded : 104 (Average: 23.84 Max: 117 Sum: 2479 Ratio: 0.03%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 595276 (Eliminated: 0 Frozen: 191082) +Constraints : 4426666 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 769MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.23s +Memory: 700MB (+0MB) +UNKNOWN +Iteration Time: 9.29s + +Iteration 103 +Queue: [(21,105,2,True), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 104 +Time : 793.387s (Solving: 766.53s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 793.584s + +Choices : 10721685 (Domain: 10619059) +Conflicts : 874734 (Analyzed: 874731) +Restarts : 9936 (Average: 88.04 Last: 206) +Model-Level : 115.0 +Problems : 104 (Average Length: 93.59 Splits: 0) +Lemmas : 874731 (Deleted: 836257) + Binary : 12453 (Ratio: 1.42%) + Ternary : 3339 (Ratio: 0.38%) + Conflict : 874731 (Average Length: 873.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 874731 (Average: 9.75 Max: 884 Sum: 8525130) + Executed : 874627 (Average: 9.74 Max: 884 Sum: 8522651 Ratio: 99.97%) + Bounded : 104 (Average: 23.84 Max: 117 Sum: 2479 Ratio: 0.03%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 595276 (Eliminated: 0 Frozen: 191082) +Constraints : 4426666 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 769MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.36s +Memory: 700MB (+0MB) +UNKNOWN +Iteration Time: 9.41s + +Iteration 104 +Queue: [(4,20,9,True), (5,25,9,True), (6,30,8,True), (7,35,8,False), (8,40,7,True), (9,45,6,True), (10,50,6,False), (11,55,5,True), (12,60,5,False), (13,65,4,True), (14,70,4,False), (15,75,4,False), (16,80,4,False), (17,85,3,True), (18,90,3,False), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,2,True), (23,115,2,False)] +Grounded Until: 115 +Blocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 105 +Time : 797.029s (Solving: 770.01s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 797.228s + +Choices : 10772177 (Domain: 10669551) +Conflicts : 882663 (Analyzed: 882660) +Restarts : 10036 (Average: 87.95 Last: 206) +Model-Level : 115.0 +Problems : 105 (Average Length: 93.81 Splits: 0) +Lemmas : 882660 (Deleted: 842472) + Binary : 12567 (Ratio: 1.42%) + Ternary : 3350 (Ratio: 0.38%) + Conflict : 882660 (Average Length: 867.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 882660 (Average: 9.71 Max: 884 Sum: 8568795) + Executed : 882556 (Average: 9.71 Max: 884 Sum: 8566316 Ratio: 99.97%) + Bounded : 104 (Average: 23.84 Max: 117 Sum: 2479 Ratio: 0.03%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 595276 (Eliminated: 0 Frozen: 191082) +Constraints : 4426666 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 769MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 3.58s +Memory: 700MB (+0MB) +UNKNOWN +Iteration Time: 3.65s + +Iteration 105 +Queue: [(5,25,9,True), (6,30,8,True), (7,35,8,False), (8,40,7,True), (9,45,6,True), (10,50,6,False), (11,55,5,True), (12,60,5,False), (13,65,4,True), (14,70,4,False), (15,75,4,False), (16,80,4,False), (17,85,3,True), (18,90,3,False), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,2,True), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 106 +Time : 806.339s (Solving: 779.17s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 806.544s + +Choices : 10828753 (Domain: 10726127) +Conflicts : 891405 (Analyzed: 891402) +Restarts : 10136 (Average: 87.94 Last: 206) +Model-Level : 115.0 +Problems : 106 (Average Length: 94.03 Splits: 0) +Lemmas : 891402 (Deleted: 852586) + Binary : 12589 (Ratio: 1.41%) + Ternary : 3358 (Ratio: 0.38%) + Conflict : 891402 (Average Length: 873.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 891402 (Average: 9.66 Max: 884 Sum: 8609920) + Executed : 891298 (Average: 9.66 Max: 884 Sum: 8607441 Ratio: 99.97%) + Bounded : 104 (Average: 23.84 Max: 117 Sum: 2479 Ratio: 0.03%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 595276 (Eliminated: 0 Frozen: 191082) +Constraints : 4426666 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 769MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.26s +Memory: 700MB (+0MB) +UNKNOWN +Iteration Time: 9.32s + +Iteration 106 +Queue: [(6,30,8,True), (7,35,8,False), (8,40,7,True), (9,45,6,True), (10,50,6,False), (11,55,5,True), (12,60,5,False), (13,65,4,True), (14,70,4,False), (15,75,4,False), (16,80,4,False), (17,85,3,True), (18,90,3,False), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,2,True), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 107 +Time : 815.401s (Solving: 788.08s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 815.612s + +Choices : 10905184 (Domain: 10802558) +Conflicts : 900298 (Analyzed: 900295) +Restarts : 10236 (Average: 87.95 Last: 206) +Model-Level : 115.0 +Problems : 107 (Average Length: 94.24 Splits: 0) +Lemmas : 900295 (Deleted: 861177) + Binary : 12611 (Ratio: 1.40%) + Ternary : 3361 (Ratio: 0.37%) + Conflict : 900295 (Average Length: 874.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 900295 (Average: 9.63 Max: 884 Sum: 8668650) + Executed : 900191 (Average: 9.63 Max: 884 Sum: 8666171 Ratio: 99.97%) + Bounded : 104 (Average: 23.84 Max: 117 Sum: 2479 Ratio: 0.03%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 595276 (Eliminated: 0 Frozen: 191082) +Constraints : 4426666 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 769MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.01s +Memory: 700MB (+0MB) +UNKNOWN +Iteration Time: 9.07s + +Iteration 107 +Queue: [(8,40,7,True), (9,45,6,True), (10,50,6,False), (11,55,5,True), (12,60,5,False), (13,65,4,True), (14,70,4,False), (15,75,4,False), (16,80,4,False), (17,85,3,True), (18,90,3,False), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,2,True), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 108 +Time : 821.386s (Solving: 793.92s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 821.600s + +Choices : 10966833 (Domain: 10864159) +Conflicts : 908618 (Analyzed: 908615) +Restarts : 10336 (Average: 87.91 Last: 206) +Model-Level : 115.0 +Problems : 108 (Average Length: 94.45 Splits: 0) +Lemmas : 908615 (Deleted: 867841) + Binary : 12634 (Ratio: 1.39%) + Ternary : 3367 (Ratio: 0.37%) + Conflict : 908615 (Average Length: 873.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 908615 (Average: 9.58 Max: 884 Sum: 8708345) + Executed : 908511 (Average: 9.58 Max: 884 Sum: 8705866 Ratio: 99.97%) + Bounded : 104 (Average: 23.84 Max: 117 Sum: 2479 Ratio: 0.03%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 595276 (Eliminated: 0 Frozen: 191082) +Constraints : 4426666 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 769MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 5.93s +Memory: 700MB (+0MB) +UNKNOWN +Iteration Time: 5.99s + +Iteration 108 +Queue: [(9,45,6,True), (10,50,6,False), (11,55,5,True), (12,60,5,False), (13,65,4,True), (14,70,4,False), (15,75,4,False), (16,80,4,False), (17,85,3,True), (18,90,3,False), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,2,True), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 109 +Time : 828.599s (Solving: 801.01s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 828.816s + +Choices : 11028739 (Domain: 10926065) +Conflicts : 917230 (Analyzed: 917227) +Restarts : 10436 (Average: 87.89 Last: 206) +Model-Level : 115.0 +Problems : 109 (Average Length: 94.66 Splits: 0) +Lemmas : 917227 (Deleted: 878125) + Binary : 12641 (Ratio: 1.38%) + Ternary : 3369 (Ratio: 0.37%) + Conflict : 917227 (Average Length: 874.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 917227 (Average: 9.54 Max: 884 Sum: 8747238) + Executed : 917123 (Average: 9.53 Max: 884 Sum: 8744759 Ratio: 99.97%) + Bounded : 104 (Average: 23.84 Max: 117 Sum: 2479 Ratio: 0.03%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 595276 (Eliminated: 0 Frozen: 191082) +Constraints : 4426666 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 769MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.17s +Memory: 700MB (+0MB) +UNKNOWN +Iteration Time: 7.22s + +Iteration 109 +Queue: [(11,55,5,True), (12,60,5,False), (13,65,4,True), (14,70,4,False), (15,75,4,False), (16,80,4,False), (17,85,3,True), (18,90,3,False), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,2,True), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 110 +Time : 836.588s (Solving: 808.87s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 836.808s + +Choices : 11102178 (Domain: 10999501) +Conflicts : 926097 (Analyzed: 926094) +Restarts : 10536 (Average: 87.90 Last: 206) +Model-Level : 115.0 +Problems : 110 (Average Length: 94.86 Splits: 0) +Lemmas : 926094 (Deleted: 886691) + Binary : 12659 (Ratio: 1.37%) + Ternary : 3373 (Ratio: 0.36%) + Conflict : 926094 (Average Length: 877.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 926094 (Average: 9.50 Max: 884 Sum: 8796738) + Executed : 925990 (Average: 9.50 Max: 884 Sum: 8794259 Ratio: 99.97%) + Bounded : 104 (Average: 23.84 Max: 117 Sum: 2479 Ratio: 0.03%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 595276 (Eliminated: 0 Frozen: 191082) +Constraints : 4426666 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 769MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.95s +Memory: 700MB (+0MB) +UNKNOWN +Iteration Time: 8.00s + +Iteration 110 +Queue: [(13,65,4,True), (14,70,4,False), (15,75,4,False), (16,80,4,False), (17,85,3,True), (18,90,3,False), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,2,True), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 111 +Time : 844.625s (Solving: 816.79s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 844.848s + +Choices : 11180110 (Domain: 11077398) +Conflicts : 934786 (Analyzed: 934783) +Restarts : 10636 (Average: 87.89 Last: 206) +Model-Level : 115.0 +Problems : 111 (Average Length: 95.06 Splits: 0) +Lemmas : 934783 (Deleted: 895447) + Binary : 12689 (Ratio: 1.36%) + Ternary : 3374 (Ratio: 0.36%) + Conflict : 934783 (Average Length: 879.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 934783 (Average: 9.46 Max: 884 Sum: 8845679) + Executed : 934678 (Average: 9.46 Max: 884 Sum: 8843083 Ratio: 99.97%) + Bounded : 105 (Average: 24.72 Max: 117 Sum: 2596 Ratio: 0.03%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 595276 (Eliminated: 0 Frozen: 191082) +Constraints : 4426666 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 769MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.00s +Memory: 700MB (+0MB) +UNKNOWN +Iteration Time: 8.04s + +Iteration 111 +Queue: [(17,85,3,True), (18,90,3,False), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,2,True), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 112 +Time : 852.604s (Solving: 824.61s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 852.828s + +Choices : 11275349 (Domain: 11172631) +Conflicts : 943619 (Analyzed: 943616) +Restarts : 10736 (Average: 87.89 Last: 206) +Model-Level : 115.0 +Problems : 112 (Average Length: 95.26 Splits: 0) +Lemmas : 943616 (Deleted: 904019) + Binary : 12714 (Ratio: 1.35%) + Ternary : 3382 (Ratio: 0.36%) + Conflict : 943616 (Average Length: 878.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 943616 (Average: 9.45 Max: 884 Sum: 8913409) + Executed : 943511 (Average: 9.44 Max: 884 Sum: 8910813 Ratio: 99.97%) + Bounded : 105 (Average: 24.72 Max: 117 Sum: 2596 Ratio: 0.03%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 595276 (Eliminated: 0 Frozen: 191082) +Constraints : 4426652 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 769MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.93s +Memory: 700MB (+0MB) +UNKNOWN +Iteration Time: 7.99s + +Iteration 112 +Queue: [(22,110,2,True), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 113 +Time : 862.274s (Solving: 834.13s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 862.504s + +Choices : 11446141 (Domain: 11343062) +Conflicts : 952624 (Analyzed: 952621) +Restarts : 10836 (Average: 87.91 Last: 206) +Model-Level : 115.0 +Problems : 113 (Average Length: 95.45 Splits: 0) +Lemmas : 952621 (Deleted: 912722) + Binary : 12757 (Ratio: 1.34%) + Ternary : 3390 (Ratio: 0.36%) + Conflict : 952621 (Average Length: 878.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 952621 (Average: 9.49 Max: 884 Sum: 9043935) + Executed : 952516 (Average: 9.49 Max: 884 Sum: 9041339 Ratio: 99.97%) + Bounded : 105 (Average: 24.72 Max: 117 Sum: 2596 Ratio: 0.03%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 595276 (Eliminated: 0 Frozen: 191082) +Constraints : 4426652 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 769MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.62s +Memory: 700MB (+0MB) +UNKNOWN +Iteration Time: 9.68s + +Iteration 113 +Queue: [(4,20,10,True), (5,25,10,True), (6,30,9,True), (7,35,8,True), (8,40,8,False), (9,45,7,False), (10,50,6,True), (11,55,6,False), (12,60,5,True), (13,65,5,False), (14,70,4,True), (15,75,4,False), (16,80,4,False), (17,85,4,False), (18,90,3,True), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,2,False)] +Grounded Until: 115 +Blocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 114 +Time : 864.651s (Solving: 836.37s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 864.884s + +Choices : 11480938 (Domain: 11377859) +Conflicts : 960294 (Analyzed: 960291) +Restarts : 10936 (Average: 87.81 Last: 206) +Model-Level : 115.0 +Problems : 114 (Average Length: 95.64 Splits: 0) +Lemmas : 960291 (Deleted: 919128) + Binary : 12786 (Ratio: 1.33%) + Ternary : 3391 (Ratio: 0.35%) + Conflict : 960291 (Average Length: 873.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 960291 (Average: 9.44 Max: 884 Sum: 9067518) + Executed : 960186 (Average: 9.44 Max: 884 Sum: 9064922 Ratio: 99.97%) + Bounded : 105 (Average: 24.72 Max: 117 Sum: 2596 Ratio: 0.03%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 595276 (Eliminated: 0 Frozen: 191082) +Constraints : 4426652 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 769MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 2.33s +Memory: 700MB (+0MB) +UNKNOWN +Iteration Time: 2.38s + +Iteration 114 +Queue: [(5,25,10,True), (6,30,9,True), (7,35,8,True), (8,40,8,False), (9,45,7,False), (10,50,6,True), (11,55,6,False), (12,60,5,True), (13,65,5,False), (14,70,4,True), (15,75,4,False), (16,80,4,False), (17,85,4,False), (18,90,3,True), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 115 +Time : 875.500s (Solving: 847.07s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 875.736s + +Choices : 11521953 (Domain: 11418874) +Conflicts : 969489 (Analyzed: 969486) +Restarts : 11036 (Average: 87.85 Last: 206) +Model-Level : 115.0 +Problems : 115 (Average Length: 95.83 Splits: 0) +Lemmas : 969486 (Deleted: 929071) + Binary : 12819 (Ratio: 1.32%) + Ternary : 3400 (Ratio: 0.35%) + Conflict : 969486 (Average Length: 874.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 969486 (Average: 9.38 Max: 884 Sum: 9095602) + Executed : 969381 (Average: 9.38 Max: 884 Sum: 9093006 Ratio: 99.97%) + Bounded : 105 (Average: 24.72 Max: 117 Sum: 2596 Ratio: 0.03%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 595276 (Eliminated: 0 Frozen: 191082) +Constraints : 4426652 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 769MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 10.80s +Memory: 700MB (+0MB) +UNKNOWN +Iteration Time: 10.86s + +Iteration 115 +Queue: [(6,30,9,True), (7,35,8,True), (8,40,8,False), (9,45,7,False), (10,50,6,True), (11,55,6,False), (12,60,5,True), (13,65,5,False), (14,70,4,True), (15,75,4,False), (16,80,4,False), (17,85,4,False), (18,90,3,True), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 116 +Time : 882.918s (Solving: 854.34s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 883.156s + +Choices : 11587100 (Domain: 11484021) +Conflicts : 977730 (Analyzed: 977727) +Restarts : 11136 (Average: 87.80 Last: 206) +Model-Level : 115.0 +Problems : 116 (Average Length: 96.01 Splits: 0) +Lemmas : 977727 (Deleted: 936058) + Binary : 12859 (Ratio: 1.32%) + Ternary : 3408 (Ratio: 0.35%) + Conflict : 977727 (Average Length: 875.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 977727 (Average: 9.35 Max: 884 Sum: 9142183) + Executed : 977622 (Average: 9.35 Max: 884 Sum: 9139587 Ratio: 99.97%) + Bounded : 105 (Average: 24.72 Max: 117 Sum: 2596 Ratio: 0.03%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 595276 (Eliminated: 0 Frozen: 191082) +Constraints : 4426652 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 769MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.36s +Memory: 700MB (+0MB) +UNKNOWN +Iteration Time: 7.42s + +Iteration 116 +Queue: [(7,35,8,True), (8,40,8,False), (9,45,7,False), (10,50,6,True), (11,55,6,False), (12,60,5,True), (13,65,5,False), (14,70,4,True), (15,75,4,False), (16,80,4,False), (17,85,4,False), (18,90,3,True), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 117 +Time : 890.100s (Solving: 861.40s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 890.340s + +Choices : 11652029 (Domain: 11548949) +Conflicts : 986620 (Analyzed: 986617) +Restarts : 11236 (Average: 87.81 Last: 206) +Model-Level : 115.0 +Problems : 117 (Average Length: 96.19 Splits: 0) +Lemmas : 986617 (Deleted: 946284) + Binary : 12864 (Ratio: 1.30%) + Ternary : 3408 (Ratio: 0.35%) + Conflict : 986617 (Average Length: 876.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 986617 (Average: 9.31 Max: 884 Sum: 9186743) + Executed : 986512 (Average: 9.31 Max: 884 Sum: 9184147 Ratio: 99.97%) + Bounded : 105 (Average: 24.72 Max: 117 Sum: 2596 Ratio: 0.03%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 595276 (Eliminated: 0 Frozen: 191082) +Constraints : 4426652 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 769MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.14s +Memory: 700MB (+0MB) +UNKNOWN +Iteration Time: 7.19s + +Iteration 117 +Queue: [(10,50,6,True), (11,55,6,False), (12,60,5,True), (13,65,5,False), (14,70,4,True), (15,75,4,False), (16,80,4,False), (17,85,4,False), (18,90,3,True), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +*** Info : (planner): INTERRUPTED by signal! +UNKNOWN + +INTERRUPTED : 1 + +Models : 0+ +Calls : 118 +Time : 894.156s (Solving: 865.30s 1st Model: 0.00s Unsat: 1.07s) +CPU Time : 894.372s + +Choices : 11687134 (Domain: 11584041) +Conflicts : 990816 (Analyzed: 990813) +Restarts : 11285 (Average: 87.80 Last: 206) +Model-Level : 115.0 +Problems : 118 (Average Length: 96.36 Splits: 0) +Lemmas : 990813 (Deleted: 952033) + Binary : 12877 (Ratio: 1.30%) + Ternary : 3408 (Ratio: 0.34%) + Conflict : 990813 (Average Length: 877.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 990813 (Average: 9.30 Max: 884 Sum: 9210344) + Executed : 990708 (Average: 9.29 Max: 884 Sum: 9207748 Ratio: 99.97%) + Bounded : 105 (Average: 24.72 Max: 117 Sum: 2596 Ratio: 0.03%) + +Rules : 62994 (Original: 61599) +Atoms : 50308 +Bodies : 11595 (Original: 10199) + Count : 252 (Original: 531) +Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199) +Tight : Yes +Variables : 595276 (Eliminated: 0 Frozen: 191082) +Constraints : 4426652 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 769MB +Max. Length : 115 steps +Models : 1 + +