From 6dd8c952fe79a02c4cc322814d5ff17bd73178bb Mon Sep 17 00:00:00 2001 From: potassco-bot Date: Fri, 2 Feb 2018 09:19:20 +0100 Subject: [PATCH] Add benchmark result [gc-ta1-tt1 | ipc-2011 | barman-sequential-satisficing | 5] --- ...c-2011_barman-sequential-satisficing_5.env | 54 + ...c-2011_barman-sequential-satisficing_5.err | 8 + ...c-2011_barman-sequential-satisficing_5.out | 5951 +++++++++++++++++ 3 files changed, 6013 insertions(+) create mode 100644 gc-ta1-tt1/ipc-2011_barman-sequential-satisficing_5.env create mode 100644 gc-ta1-tt1/ipc-2011_barman-sequential-satisficing_5.err create mode 100644 gc-ta1-tt1/ipc-2011_barman-sequential-satisficing_5.out diff --git a/gc-ta1-tt1/ipc-2011_barman-sequential-satisficing_5.env b/gc-ta1-tt1/ipc-2011_barman-sequential-satisficing_5.env new file mode 100644 index 000000000..5e58b9a02 --- /dev/null +++ b/gc-ta1-tt1/ipc-2011_barman-sequential-satisficing_5.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-5.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: 5 + 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_5.err b/gc-ta1-tt1/ipc-2011_barman-sequential-satisficing_5.err new file mode 100644 index 000000000..5a1fc081e --- /dev/null +++ b/gc-ta1-tt1/ipc-2011_barman-sequential-satisficing_5.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': 5} +# 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-5.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.05 MEM 756372 MAXMEM 761208 STALE 1 MAXMEM_RSS 639140 + + diff --git a/gc-ta1-tt1/ipc-2011_barman-sequential-satisficing_5.out b/gc-ta1-tt1/ipc-2011_barman-sequential-satisficing_5.out new file mode 100644 index 000000000..20a4b862e --- /dev/null +++ b/gc-ta1-tt1/ipc-2011_barman-sequential-satisficing_5.out @@ -0,0 +1,5951 @@ +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-5.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-5.pddl +Parsing... +Parsing: [0.030s CPU, 0.031s wall-clock] +Normalizing task... [0.000s CPU, 0.002s wall-clock] +Instantiating... +Generating Datalog program... [0.010s CPU, 0.008s wall-clock] +Normalizing Datalog program... +Normalizing Datalog program: [0.030s CPU, 0.041s wall-clock] +Preparing model... [0.030s CPU, 0.022s wall-clock] +Generated 115 rules. +Computing model... [0.370s CPU, 0.373s wall-clock] +2300 relevant atoms +2393 auxiliary atoms +4693 final queue length +8087 total queue pushes +Completing instantiation... [0.690s CPU, 0.690s wall-clock] +Instantiating: [1.130s CPU, 1.139s wall-clock] +Computing fact groups... +Finding invariants... +24 initial candidates +Finding invariants: [0.130s CPU, 0.131s 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.010s CPU, 0.001s wall-clock] +Building translation key... [0.010s CPU, 0.009s wall-clock] +Computing fact groups: [0.170s CPU, 0.167s wall-clock] +Building STRIPS to SAS dictionary... [0.000s CPU, 0.002s wall-clock] +Building dictionary for full mutex groups... [0.000s CPU, 0.002s wall-clock] +Building mutex information... +Building mutex information: [0.010s CPU, 0.003s wall-clock] +Translating task... +Processing axioms... +Simplifying axioms... [0.000s CPU, 0.000s wall-clock] +Processing axioms: [0.030s CPU, 0.039s wall-clock] +Translating task: [0.730s CPU, 0.730s 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.357s 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.321s wall-clock] +Done! [2.990s CPU, 3.026s wall-clock] +planner.py version 0.0.1 + +Time: 0.61s +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.713s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s) +CPU Time : 0.616s + +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.00s + +Iteration 2 +Queue: [(1,5,0,True), (2,10,0,True), (3,15,0,True), (4,20,0,True), (5,25,0,True), (6,30,0,True)] +Grounded Until: 0 +Expected Memory: 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.005s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s) +CPU Time : 0.908s + +Choices : 367 (Domain: 28) +Conflicts : 8 (Analyzed: 8) +Restarts : 0 +Model-Level : 115.0 +Problems : 2 (Average Length: 4.50 Splits: 0) +Lemmas : 8 (Deleted: 0) + Binary : 6 (Ratio: 75.00%) + Ternary : 0 (Ratio: 0.00%) + Conflict : 8 (Average Length: 10.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 8 (Average: 32.62 Max: 84 Sum: 261) + Executed : 6 (Average: 32.38 Max: 84 Sum: 259 Ratio: 99.23%) + Bounded : 2 (Average: 1.00 Max: 1 Sum: 2 Ratio: 0.77%) + +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.102s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s) +CPU Time : 1.004s + +Choices : 368 (Domain: 28) +Conflicts : 10 (Analyzed: 9) +Restarts : 0 +Model-Level : 115.0 +Problems : 3 (Average Length: 5.33 Splits: 0) +Lemmas : 9 (Deleted: 0) + Binary : 7 (Ratio: 77.78%) + Ternary : 0 (Ratio: 0.00%) + Conflict : 9 (Average Length: 9.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 9 (Average: 29.22 Max: 84 Sum: 263) + Executed : 6 (Average: 28.89 Max: 84 Sum: 260 Ratio: 98.86%) + Bounded : 3 (Average: 1.00 Max: 1 Sum: 3 Ratio: 1.14%) + +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.227s (Solving: 0.64s 1st Model: 0.00s Unsat: 0.64s) +CPU Time : 2.128s + +Choices : 20428 (Domain: 19268) +Conflicts : 2400 (Analyzed: 2398) +Restarts : 30 (Average: 79.93 Last: 10) +Model-Level : 115.0 +Problems : 4 (Average Length: 7.00 Splits: 0) +Lemmas : 2398 (Deleted: 589) + Binary : 334 (Ratio: 13.93%) + Ternary : 293 (Ratio: 12.22%) + Conflict : 2398 (Average Length: 30.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 2398 (Average: 8.56 Max: 84 Sum: 20522) + Executed : 2365 (Average: 8.42 Max: 84 Sum: 20181 Ratio: 98.34%) + Bounded : 33 (Average: 10.33 Max: 12 Sum: 341 Ratio: 1.66%) + +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.66s +Memory: 197MB (+9MB) +UNSAT +Iteration Time: 1.13s + +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.38s +Memory: 203MB (+6MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0 +Calls : 5 +Time : 5.613s (Solving: 3.47s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 5.516s + +Choices : 83668 (Domain: 80839) +Conflicts : 9035 (Analyzed: 9032) +Restarts : 102 (Average: 88.55 Last: 20) +Model-Level : 115.0 +Problems : 5 (Average Length: 9.00 Splits: 0) +Lemmas : 9032 (Deleted: 4942) + Binary : 1008 (Ratio: 11.16%) + Ternary : 545 (Ratio: 6.03%) + Conflict : 9032 (Average Length: 125.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 9032 (Average: 9.18 Max: 95 Sum: 82898) + Executed : 8982 (Average: 9.11 Max: 95 Sum: 82286 Ratio: 99.26%) + Bounded : 50 (Average: 12.24 Max: 17 Sum: 612 Ratio: 0.74%) + +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 : 425655 (Binary: 91.7% Ternary: 6.4% Other: 2.0%) + +Memory Peak : 227MB +Max. Length : 10 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 2.86s +Memory: 216MB (+13MB) +UNSAT +Iteration Time: 3.40s + +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.40s +Memory: 223MB (+7MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 6 +Time : 11.145s (Solving: 8.41s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 11.048s + +Choices : 194835 (Domain: 179881) +Conflicts : 18138 (Analyzed: 18135) +Restarts : 202 (Average: 89.78 Last: 101) +Model-Level : 115.0 +Problems : 6 (Average Length: 11.17 Splits: 0) +Lemmas : 18135 (Deleted: 12424) + Binary : 1624 (Ratio: 8.96%) + Ternary : 778 (Ratio: 4.29%) + Conflict : 18135 (Average Length: 297.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 18135 (Average: 10.37 Max: 302 Sum: 188090) + Executed : 18076 (Average: 10.33 Max: 302 Sum: 187289 Ratio: 99.57%) + Bounded : 59 (Average: 13.58 Max: 22 Sum: 801 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 : 93752 (Eliminated: 0 Frozen: 28822) +Constraints : 621350 (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.97s +Memory: 239MB (+16MB) +UNKNOWN +Iteration Time: 5.54s + +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.37s +Memory: 244MB (+5MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 7 +Time : 17.906s (Solving: 14.59s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 17.812s + +Choices : 327156 (Domain: 302805) +Conflicts : 26901 (Analyzed: 26898) +Restarts : 302 (Average: 89.07 Last: 101) +Model-Level : 115.0 +Problems : 7 (Average Length: 13.43 Splits: 0) +Lemmas : 26898 (Deleted: 18459) + Binary : 2330 (Ratio: 8.66%) + Ternary : 962 (Ratio: 3.58%) + Conflict : 26898 (Average Length: 278.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 26898 (Average: 11.69 Max: 357 Sum: 314445) + Executed : 26829 (Average: 11.65 Max: 357 Sum: 313374 Ratio: 99.66%) + Bounded : 69 (Average: 15.52 Max: 27 Sum: 1071 Ratio: 0.34%) + +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 : 815724 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) + +Memory Peak : 263MB +Max. Length : 20 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.22s +Memory: 253MB (+9MB) +UNKNOWN +Iteration Time: 6.77s + +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.45s +Memory: 267MB (+14MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 8 +Time : 25.353s (Solving: 21.36s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 25.264s + +Choices : 455849 (Domain: 424072) +Conflicts : 36045 (Analyzed: 36042) +Restarts : 402 (Average: 89.66 Last: 101) +Model-Level : 115.0 +Problems : 8 (Average Length: 15.75 Splits: 0) +Lemmas : 36042 (Deleted: 26452) + Binary : 2666 (Ratio: 7.40%) + Ternary : 1049 (Ratio: 2.91%) + Conflict : 36042 (Average Length: 306.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 36042 (Average: 12.05 Max: 357 Sum: 434442) + Executed : 35970 (Average: 12.02 Max: 357 Sum: 433275 Ratio: 99.73%) + Bounded : 72 (Average: 16.21 Max: 32 Sum: 1167 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 : 1012058 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) + +Memory Peak : 291MB +Max. Length : 25 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.81s +Memory: 291MB (+24MB) +UNKNOWN +Iteration Time: 7.46s + +Iteration 8 +Queue: [(4,20,1,True), (5,25,1,True), (6,30,1,True), (7,35,0,True), (8,40,0,True), (9,45,0,True), (10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True), (17,85,0,True)] +Grounded Until: 30 +Blocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 9 +Time : 29.288s (Solving: 25.26s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 29.204s + +Choices : 495709 (Domain: 462324) +Conflicts : 43610 (Analyzed: 43607) +Restarts : 502 (Average: 86.87 Last: 101) +Model-Level : 115.0 +Problems : 9 (Average Length: 17.56 Splits: 0) +Lemmas : 43607 (Deleted: 34188) + Binary : 2830 (Ratio: 6.49%) + Ternary : 1098 (Ratio: 2.52%) + Conflict : 43607 (Average Length: 347.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 43607 (Average: 10.73 Max: 357 Sum: 467733) + Executed : 43535 (Average: 10.70 Max: 357 Sum: 466566 Ratio: 99.75%) + Bounded : 72 (Average: 16.21 Max: 32 Sum: 1167 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 : 1012016 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) + +Memory Peak : 291MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 3.93s +Memory: 291MB (+0MB) +UNKNOWN +Iteration Time: 3.94s + +Iteration 9 +Queue: [(5,25,1,True), (6,30,1,True), (7,35,0,True), (8,40,0,True), (9,45,0,True), (10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True), (17,85,0,True)] +Grounded Until: 30 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 10 +Time : 34.868s (Solving: 30.80s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 34.784s + +Choices : 585465 (Domain: 547882) +Conflicts : 52309 (Analyzed: 52306) +Restarts : 602 (Average: 86.89 Last: 101) +Model-Level : 115.0 +Problems : 10 (Average Length: 19.00 Splits: 0) +Lemmas : 52306 (Deleted: 41407) + Binary : 3164 (Ratio: 6.05%) + Ternary : 1154 (Ratio: 2.21%) + Conflict : 52306 (Average Length: 342.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 52306 (Average: 10.49 Max: 357 Sum: 548691) + Executed : 52232 (Average: 10.47 Max: 357 Sum: 547465 Ratio: 99.78%) + Bounded : 74 (Average: 16.57 Max: 32 Sum: 1226 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 : 1012016 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) + +Memory Peak : 291MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 5.57s +Memory: 291MB (+0MB) +UNKNOWN +Iteration Time: 5.59s + +Iteration 10 +Queue: [(6,30,1,True), (7,35,0,True), (8,40,0,True), (9,45,0,True), (10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True), (17,85,0,True)] +Grounded Until: 30 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 11 +Time : 40.323s (Solving: 36.23s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 40.240s + +Choices : 678499 (Domain: 638387) +Conflicts : 61022 (Analyzed: 61019) +Restarts : 702 (Average: 86.92 Last: 101) +Model-Level : 115.0 +Problems : 11 (Average Length: 20.18 Splits: 0) +Lemmas : 61019 (Deleted: 49566) + Binary : 3372 (Ratio: 5.53%) + Ternary : 1184 (Ratio: 1.94%) + Conflict : 61019 (Average Length: 343.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 61019 (Average: 10.37 Max: 357 Sum: 632788) + Executed : 60943 (Average: 10.35 Max: 357 Sum: 631498 Ratio: 99.80%) + Bounded : 76 (Average: 16.97 Max: 32 Sum: 1290 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 : 146544 (Eliminated: 0 Frozen: 45902) +Constraints : 1012003 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) + +Memory Peak : 291MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 5.45s +Memory: 291MB (+0MB) +UNKNOWN +Iteration Time: 5.46s + +Iteration 11 +Queue: [(7,35,0,True), (8,40,0,True), (9,45,0,True), (10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True), (17,85,0,True)] +Grounded Until: 30 +Expected Memory: 329.0MB +Grounding... [('step', [31]), ('step', [32]), ('step', [33]), ('step', [34]), ('step', [35]), ('check', [35])] +Grounding Time: 0.40s +Memory: 291MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 12 +Time : 45.860s (Solving: 41.12s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 45.780s + +Choices : 779563 (Domain: 736842) +Conflicts : 69781 (Analyzed: 69778) +Restarts : 802 (Average: 87.00 Last: 101) +Model-Level : 115.0 +Problems : 12 (Average Length: 21.58 Splits: 0) +Lemmas : 69778 (Deleted: 57819) + Binary : 3502 (Ratio: 5.02%) + Ternary : 1233 (Ratio: 1.77%) + Conflict : 69778 (Average Length: 342.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 69778 (Average: 10.38 Max: 357 Sum: 724277) + Executed : 69699 (Average: 10.36 Max: 357 Sum: 722876 Ratio: 99.81%) + Bounded : 79 (Average: 17.73 Max: 37 Sum: 1401 Ratio: 0.19%) + +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 : 1210969 (Binary: 91.5% Ternary: 6.6% Other: 1.9%) + +Memory Peak : 316MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 4.94s +Memory: 301MB (+10MB) +UNKNOWN +Iteration Time: 5.55s + +Iteration 12 +Queue: [(8,40,0,True), (9,45,0,True), (10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True), (17,85,0,True)] +Grounded Until: 35 +Expected Memory: 339.0MB +Grounding... [('step', [36]), ('step', [37]), ('step', [38]), ('step', [39]), ('step', [40]), ('check', [40])] +Grounding Time: 0.39s +Memory: 307MB (+6MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 13 +Time : 51.131s (Solving: 45.74s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 51.052s + +Choices : 867707 (Domain: 823138) +Conflicts : 78104 (Analyzed: 78101) +Restarts : 902 (Average: 86.59 Last: 107) +Model-Level : 115.0 +Problems : 13 (Average Length: 23.15 Splits: 0) +Lemmas : 78101 (Deleted: 64093) + Binary : 3639 (Ratio: 4.66%) + Ternary : 1263 (Ratio: 1.62%) + Conflict : 78101 (Average Length: 339.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 78101 (Average: 10.28 Max: 357 Sum: 802547) + Executed : 78022 (Average: 10.26 Max: 357 Sum: 801146 Ratio: 99.83%) + Bounded : 79 (Average: 17.73 Max: 37 Sum: 1401 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 : 1411993 (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: 4.67s +Memory: 320MB (+13MB) +UNKNOWN +Iteration Time: 5.28s + +Iteration 13 +Queue: [(9,45,0,True), (10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True), (17,85,0,True)] +Grounded Until: 40 +Expected Memory: 358.0MB +Grounding... [('step', [41]), ('step', [42]), ('step', [43]), ('step', [44]), ('step', [45]), ('check', [45])] +Grounding Time: 0.40s +Memory: 326MB (+6MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 14 +Time : 56.198s (Solving: 50.12s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 56.112s + +Choices : 979870 (Domain: 934167) +Conflicts : 86377 (Analyzed: 86374) +Restarts : 1002 (Average: 86.20 Last: 110) +Model-Level : 115.0 +Problems : 14 (Average Length: 24.86 Splits: 0) +Lemmas : 86374 (Deleted: 71864) + Binary : 3834 (Ratio: 4.44%) + Ternary : 1306 (Ratio: 1.51%) + Conflict : 86374 (Average Length: 327.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 86374 (Average: 10.49 Max: 423 Sum: 906136) + Executed : 86293 (Average: 10.47 Max: 423 Sum: 904651 Ratio: 99.84%) + Bounded : 81 (Average: 18.33 Max: 42 Sum: 1485 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 : 225732 (Eliminated: 0 Frozen: 71522) +Constraints : 1613063 (Binary: 91.5% Ternary: 6.6% Other: 1.9%) + +Memory Peak : 359MB +Max. Length : 40 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 4.43s +Memory: 354MB (+28MB) +UNKNOWN +Iteration Time: 5.07s + +Iteration 14 +Queue: [(10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True), (17,85,0,True)] +Grounded Until: 45 +Expected Memory: 392.0MB +Grounding... [('step', [46]), ('step', [47]), ('step', [48]), ('step', [49]), ('step', [50]), ('check', [50])] +Grounding Time: 0.37s +Memory: 354MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 15 +Time : 61.629s (Solving: 54.90s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 61.544s + +Choices : 1103188 (Domain: 1055956) +Conflicts : 94165 (Analyzed: 94162) +Restarts : 1102 (Average: 85.45 Last: 110) +Model-Level : 115.0 +Problems : 15 (Average Length: 26.67 Splits: 0) +Lemmas : 94162 (Deleted: 79983) + Binary : 3911 (Ratio: 4.15%) + Ternary : 1326 (Ratio: 1.41%) + Conflict : 94162 (Average Length: 331.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 94162 (Average: 10.79 Max: 423 Sum: 1016477) + Executed : 94081 (Average: 10.78 Max: 423 Sum: 1014992 Ratio: 99.85%) + Bounded : 81 (Average: 18.33 Max: 42 Sum: 1485 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 : 252128 (Eliminated: 0 Frozen: 80062) +Constraints : 1814133 (Binary: 91.5% Ternary: 6.6% Other: 1.9%) + +Memory Peak : 387MB +Max. Length : 45 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 4.83s +Memory: 362MB (+8MB) +UNKNOWN +Iteration Time: 5.44s + +Iteration 15 +Queue: [(11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True), (17,85,0,True)] +Grounded Until: 50 +Expected Memory: 400.0MB +Grounding... [('step', [51]), ('step', [52]), ('step', [53]), ('step', [54]), ('step', [55]), ('check', [55])] +Grounding Time: 0.38s +Memory: 367MB (+5MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 16 +Time : 67.229s (Solving: 59.82s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 67.148s + +Choices : 1220676 (Domain: 1172081) +Conflicts : 102486 (Analyzed: 102483) +Restarts : 1202 (Average: 85.26 Last: 110) +Model-Level : 115.0 +Problems : 16 (Average Length: 28.56 Splits: 0) +Lemmas : 102483 (Deleted: 87348) + Binary : 4006 (Ratio: 3.91%) + Ternary : 1342 (Ratio: 1.31%) + Conflict : 102483 (Average Length: 327.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 102483 (Average: 10.95 Max: 533 Sum: 1122544) + Executed : 102399 (Average: 10.94 Max: 533 Sum: 1120893 Ratio: 99.85%) + Bounded : 84 (Average: 19.65 Max: 57 Sum: 1651 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 : 2015203 (Binary: 91.5% Ternary: 6.6% Other: 1.9%) + +Memory Peak : 410MB +Max. Length : 50 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 4.99s +Memory: 382MB (+15MB) +UNKNOWN +Iteration Time: 5.61s + +Iteration 16 +Queue: [(12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True), (17,85,0,True)] +Grounded Until: 55 +Expected Memory: 420.0MB +Grounding... [('step', [56]), ('step', [57]), ('step', [58]), ('step', [59]), ('step', [60]), ('check', [60])] +Grounding Time: 0.39s +Memory: 383MB (+1MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 17 +Time : 72.326s (Solving: 64.21s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 72.248s + +Choices : 1366534 (Domain: 1315690) +Conflicts : 110475 (Analyzed: 110472) +Restarts : 1302 (Average: 84.85 Last: 110) +Model-Level : 115.0 +Problems : 17 (Average Length: 30.53 Splits: 0) +Lemmas : 110472 (Deleted: 95163) + Binary : 4123 (Ratio: 3.73%) + Ternary : 1359 (Ratio: 1.23%) + Conflict : 110472 (Average Length: 325.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 110472 (Average: 11.37 Max: 533 Sum: 1256134) + Executed : 110386 (Average: 11.35 Max: 533 Sum: 1254364 Ratio: 99.86%) + Bounded : 86 (Average: 20.58 Max: 62 Sum: 1770 Ratio: 0.14%) + +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 : 2216234 (Binary: 91.5% Ternary: 6.6% Other: 1.9%) + +Memory Peak : 429MB +Max. Length : 55 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 4.45s +Memory: 400MB (+17MB) +UNKNOWN +Iteration Time: 5.11s + +Iteration 17 +Queue: [(13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True), (17,85,0,True)] +Grounded Until: 60 +Expected Memory: 438.0MB +Grounding... [('step', [61]), ('step', [62]), ('step', [63]), ('step', [64]), ('step', [65]), ('check', [65])] +Grounding Time: 0.39s +Memory: 404MB (+4MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 18 +Time : 78.486s (Solving: 69.64s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 78.412s + +Choices : 1582259 (Domain: 1528281) +Conflicts : 119385 (Analyzed: 119382) +Restarts : 1402 (Average: 85.15 Last: 110) +Model-Level : 115.0 +Problems : 18 (Average Length: 32.56 Splits: 0) +Lemmas : 119382 (Deleted: 104860) + Binary : 4250 (Ratio: 3.56%) + Ternary : 1388 (Ratio: 1.16%) + Conflict : 119382 (Average Length: 332.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 119382 (Average: 12.19 Max: 533 Sum: 1455416) + Executed : 119296 (Average: 12.18 Max: 533 Sum: 1453646 Ratio: 99.88%) + Bounded : 86 (Average: 20.58 Max: 62 Sum: 1770 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 : 2413082 (Binary: 91.5% Ternary: 6.6% Other: 1.9%) + +Memory Peak : 450MB +Max. Length : 60 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 5.51s +Memory: 448MB (+44MB) +UNKNOWN +Iteration Time: 6.17s + +Iteration 18 +Queue: [(14,70,0,True), (15,75,0,True), (16,80,0,True), (17,85,0,True)] +Grounded Until: 65 +Expected Memory: 496.0MB +Grounding... [('step', [66]), ('step', [67]), ('step', [68]), ('step', [69]), ('step', [70]), ('check', [70])] +Grounding Time: 0.53s +Memory: 460MB (+12MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 19 +Time : 85.932s (Solving: 76.22s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 85.860s + +Choices : 1785835 (Domain: 1729631) +Conflicts : 127765 (Analyzed: 127762) +Restarts : 1502 (Average: 85.06 Last: 110) +Model-Level : 115.0 +Problems : 19 (Average Length: 34.63 Splits: 0) +Lemmas : 127762 (Deleted: 111723) + Binary : 4439 (Ratio: 3.47%) + Ternary : 1427 (Ratio: 1.12%) + Conflict : 127762 (Average Length: 356.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 127762 (Average: 12.82 Max: 641 Sum: 1638063) + Executed : 127673 (Average: 12.81 Max: 641 Sum: 1636080 Ratio: 99.88%) + Bounded : 89 (Average: 22.28 Max: 72 Sum: 1983 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 : 357712 (Eliminated: 0 Frozen: 114222) +Constraints : 2614152 (Binary: 91.5% Ternary: 6.6% Other: 1.9%) + +Memory Peak : 504MB +Max. Length : 65 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.65s +Memory: 463MB (+3MB) +UNKNOWN +Iteration Time: 7.46s + +Iteration 19 +Queue: [(15,75,0,True), (16,80,0,True), (17,85,0,True)] +Grounded Until: 70 +Expected Memory: 511.0MB +Grounding... [('step', [71]), ('step', [72]), ('step', [73]), ('step', [74]), ('step', [75]), ('check', [75])] +Grounding Time: 0.37s +Memory: 463MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 20 +Time : 93.510s (Solving: 83.07s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 93.440s + +Choices : 2058865 (Domain: 1999152) +Conflicts : 136710 (Analyzed: 136707) +Restarts : 1602 (Average: 85.34 Last: 110) +Model-Level : 115.0 +Problems : 20 (Average Length: 36.75 Splits: 0) +Lemmas : 136707 (Deleted: 121778) + Binary : 4652 (Ratio: 3.40%) + Ternary : 1445 (Ratio: 1.06%) + Conflict : 136707 (Average Length: 377.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 136707 (Average: 13.82 Max: 671 Sum: 1889318) + Executed : 136616 (Average: 13.80 Max: 671 Sum: 1887181 Ratio: 99.89%) + Bounded : 91 (Average: 23.48 Max: 77 Sum: 2137 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 : 384108 (Eliminated: 0 Frozen: 122762) +Constraints : 2815194 (Binary: 91.5% Ternary: 6.6% Other: 1.9%) + +Memory Peak : 515MB +Max. Length : 70 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.93s +Memory: 476MB (+13MB) +UNKNOWN +Iteration Time: 7.59s + +Iteration 20 +Queue: [(16,80,0,True), (17,85,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.39s +Memory: 479MB (+3MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 21 +Time : 101.077s (Solving: 89.87s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 101.008s + +Choices : 2377079 (Domain: 2314344) +Conflicts : 145552 (Analyzed: 145549) +Restarts : 1702 (Average: 85.52 Last: 110) +Model-Level : 115.0 +Problems : 21 (Average Length: 38.90 Splits: 0) +Lemmas : 145549 (Deleted: 129958) + Binary : 4745 (Ratio: 3.26%) + Ternary : 1465 (Ratio: 1.01%) + Conflict : 145549 (Average Length: 382.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 145549 (Average: 15.03 Max: 671 Sum: 2186977) + Executed : 145456 (Average: 15.01 Max: 671 Sum: 2184676 Ratio: 99.89%) + Bounded : 93 (Average: 24.74 Max: 82 Sum: 2301 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 : 410504 (Eliminated: 0 Frozen: 131302) +Constraints : 3016224 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 537MB +Max. Length : 75 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.88s +Memory: 498MB (+19MB) +UNKNOWN +Iteration Time: 7.58s + +Iteration 21 +Queue: [(17,85,0,True)] +Grounded Until: 80 +Expected Memory: 546.0MB +Grounding... [('step', [81]), ('step', [82]), ('step', [83]), ('step', [84]), ('step', [85]), ('check', [85])] +Grounding Time: 0.38s +Memory: 498MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 22 +Time : 106.918s (Solving: 94.94s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 106.852s + +Choices : 2626934 (Domain: 2561282) +Conflicts : 153897 (Analyzed: 153894) +Restarts : 1802 (Average: 85.40 Last: 110) +Model-Level : 115.0 +Problems : 22 (Average Length: 41.09 Splits: 0) +Lemmas : 153894 (Deleted: 136518) + Binary : 4815 (Ratio: 3.13%) + Ternary : 1475 (Ratio: 0.96%) + Conflict : 153894 (Average Length: 382.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 153894 (Average: 15.71 Max: 671 Sum: 2418322) + Executed : 153801 (Average: 15.70 Max: 671 Sum: 2416021 Ratio: 99.90%) + Bounded : 93 (Average: 24.74 Max: 82 Sum: 2301 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 : 436900 (Eliminated: 0 Frozen: 139842) +Constraints : 3217244 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 558MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 5.17s +Memory: 516MB (+18MB) +UNKNOWN +Iteration Time: 5.86s + +Iteration 22 +Queue: [(4,20,2,True), (5,25,2,True), (6,30,2,True), (7,35,1,True), (8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 85 +Blocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 23 +Time : 112.628s (Solving: 100.53s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 112.556s + +Choices : 2666289 (Domain: 2600637) +Conflicts : 161814 (Analyzed: 161811) +Restarts : 1902 (Average: 85.07 Last: 110) +Model-Level : 115.0 +Problems : 23 (Average Length: 43.09 Splits: 0) +Lemmas : 161811 (Deleted: 145241) + Binary : 4883 (Ratio: 3.02%) + Ternary : 1486 (Ratio: 0.92%) + Conflict : 161811 (Average Length: 393.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 161811 (Average: 15.14 Max: 671 Sum: 2450229) + Executed : 161716 (Average: 15.13 Max: 671 Sum: 2447754 Ratio: 99.90%) + Bounded : 95 (Average: 26.05 Max: 87 Sum: 2475 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 : 436900 (Eliminated: 0 Frozen: 139842) +Constraints : 3217244 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 558MB +Max. Length : 85 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 5.66s +Memory: 517MB (+1MB) +UNKNOWN +Iteration Time: 5.71s + +Iteration 23 +Queue: [(5,25,2,True), (6,30,2,True), (7,35,1,True), (8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 85 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 24 +Time : 117.957s (Solving: 105.77s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 117.888s + +Choices : 2734738 (Domain: 2666366) +Conflicts : 171421 (Analyzed: 171418) +Restarts : 2002 (Average: 85.62 Last: 110) +Model-Level : 115.0 +Problems : 24 (Average Length: 44.92 Splits: 0) +Lemmas : 171418 (Deleted: 154283) + Binary : 4986 (Ratio: 2.91%) + Ternary : 1509 (Ratio: 0.88%) + Conflict : 171418 (Average Length: 394.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 171418 (Average: 14.63 Max: 671 Sum: 2507902) + Executed : 171323 (Average: 14.62 Max: 671 Sum: 2505427 Ratio: 99.90%) + Bounded : 95 (Average: 26.05 Max: 87 Sum: 2475 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 : 436900 (Eliminated: 0 Frozen: 139842) +Constraints : 3214748 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 558MB +Max. Length : 85 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 5.30s +Memory: 517MB (+0MB) +UNKNOWN +Iteration Time: 5.33s + +Iteration 24 +Queue: [(6,30,2,True), (7,35,1,True), (8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 85 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 25 +Time : 123.006s (Solving: 110.73s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 122.940s + +Choices : 2815441 (Domain: 2743992) +Conflicts : 180219 (Analyzed: 180216) +Restarts : 2102 (Average: 85.74 Last: 110) +Model-Level : 115.0 +Problems : 25 (Average Length: 46.60 Splits: 0) +Lemmas : 180216 (Deleted: 163467) + Binary : 5101 (Ratio: 2.83%) + Ternary : 1532 (Ratio: 0.85%) + Conflict : 180216 (Average Length: 400.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 180216 (Average: 14.29 Max: 671 Sum: 2575753) + Executed : 180121 (Average: 14.28 Max: 671 Sum: 2573278 Ratio: 99.90%) + Bounded : 95 (Average: 26.05 Max: 87 Sum: 2475 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 : 436900 (Eliminated: 0 Frozen: 139842) +Constraints : 3214748 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 558MB +Max. Length : 85 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 5.02s +Memory: 517MB (+0MB) +UNKNOWN +Iteration Time: 5.05s + +Iteration 25 +Queue: [(7,35,1,True), (8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 85 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 26 +Time : 127.926s (Solving: 115.54s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 127.864s + +Choices : 2911485 (Domain: 2837581) +Conflicts : 188654 (Analyzed: 188651) +Restarts : 2202 (Average: 85.67 Last: 115) +Model-Level : 115.0 +Problems : 26 (Average Length: 48.15 Splits: 0) +Lemmas : 188651 (Deleted: 170310) + Binary : 5219 (Ratio: 2.77%) + Ternary : 1536 (Ratio: 0.81%) + Conflict : 188651 (Average Length: 407.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 188651 (Average: 14.09 Max: 671 Sum: 2658216) + Executed : 188555 (Average: 14.08 Max: 671 Sum: 2655654 Ratio: 99.90%) + Bounded : 96 (Average: 26.69 Max: 87 Sum: 2562 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 : 436900 (Eliminated: 0 Frozen: 139842) +Constraints : 3214748 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 558MB +Max. Length : 85 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 4.88s +Memory: 517MB (+0MB) +UNKNOWN +Iteration Time: 4.92s + +Iteration 26 +Queue: [(8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 85 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 27 +Time : 135.092s (Solving: 122.60s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 135.036s + +Choices : 3062444 (Domain: 2980038) +Conflicts : 197708 (Analyzed: 197705) +Restarts : 2302 (Average: 85.88 Last: 115) +Model-Level : 115.0 +Problems : 27 (Average Length: 49.59 Splits: 0) +Lemmas : 197705 (Deleted: 179876) + Binary : 5554 (Ratio: 2.81%) + Ternary : 1614 (Ratio: 0.82%) + Conflict : 197705 (Average Length: 427.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 197705 (Average: 14.10 Max: 671 Sum: 2788038) + Executed : 197609 (Average: 14.09 Max: 671 Sum: 2785476 Ratio: 99.91%) + Bounded : 96 (Average: 26.69 Max: 87 Sum: 2562 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 : 436900 (Eliminated: 0 Frozen: 139842) +Constraints : 3214722 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 558MB +Max. Length : 85 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.13s +Memory: 517MB (+0MB) +UNKNOWN +Iteration Time: 7.17s + +Iteration 27 +Queue: [(9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 85 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 28 +Time : 140.467s (Solving: 127.87s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 140.408s + +Choices : 3192312 (Domain: 3107985) +Conflicts : 206567 (Analyzed: 206564) +Restarts : 2402 (Average: 86.00 Last: 158) +Model-Level : 115.0 +Problems : 28 (Average Length: 50.93 Splits: 0) +Lemmas : 206564 (Deleted: 188498) + Binary : 5755 (Ratio: 2.79%) + Ternary : 1656 (Ratio: 0.80%) + Conflict : 206564 (Average Length: 433.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 206564 (Average: 14.05 Max: 671 Sum: 2901654) + Executed : 206468 (Average: 14.03 Max: 671 Sum: 2899092 Ratio: 99.91%) + Bounded : 96 (Average: 26.69 Max: 87 Sum: 2562 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 : 436900 (Eliminated: 0 Frozen: 139842) +Constraints : 3214722 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 558MB +Max. Length : 85 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 5.33s +Memory: 517MB (+0MB) +UNKNOWN +Iteration Time: 5.37s + +Iteration 28 +Queue: [(10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 85 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 29 +Time : 146.792s (Solving: 134.08s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 146.736s + +Choices : 3370471 (Domain: 3279277) +Conflicts : 215484 (Analyzed: 215481) +Restarts : 2502 (Average: 86.12 Last: 170) +Model-Level : 115.0 +Problems : 29 (Average Length: 52.17 Splits: 0) +Lemmas : 215481 (Deleted: 196820) + Binary : 6004 (Ratio: 2.79%) + Ternary : 1741 (Ratio: 0.81%) + Conflict : 215481 (Average Length: 441.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 215481 (Average: 14.20 Max: 671 Sum: 3059677) + Executed : 215385 (Average: 14.19 Max: 671 Sum: 3057115 Ratio: 99.92%) + Bounded : 96 (Average: 26.69 Max: 87 Sum: 2562 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 : 436900 (Eliminated: 0 Frozen: 139842) +Constraints : 3214722 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 558MB +Max. Length : 85 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.29s +Memory: 517MB (+0MB) +UNKNOWN +Iteration Time: 6.33s + +Iteration 29 +Queue: [(11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 85 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 30 +Time : 152.466s (Solving: 139.67s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 152.412s + +Choices : 3523031 (Domain: 3430715) +Conflicts : 224460 (Analyzed: 224457) +Restarts : 2602 (Average: 86.26 Last: 170) +Model-Level : 115.0 +Problems : 30 (Average Length: 53.33 Splits: 0) +Lemmas : 224457 (Deleted: 205177) + Binary : 6136 (Ratio: 2.73%) + Ternary : 1758 (Ratio: 0.78%) + Conflict : 224457 (Average Length: 442.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 224457 (Average: 14.24 Max: 671 Sum: 3195230) + Executed : 224361 (Average: 14.22 Max: 671 Sum: 3192668 Ratio: 99.92%) + Bounded : 96 (Average: 26.69 Max: 87 Sum: 2562 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 : 436900 (Eliminated: 0 Frozen: 139842) +Constraints : 3214722 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 558MB +Max. Length : 85 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 5.65s +Memory: 517MB (+0MB) +UNKNOWN +Iteration Time: 5.68s + +Iteration 30 +Queue: [(12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 85 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 31 +Time : 159.614s (Solving: 146.73s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 159.564s + +Choices : 3763227 (Domain: 3660922) +Conflicts : 233518 (Analyzed: 233515) +Restarts : 2702 (Average: 86.42 Last: 170) +Model-Level : 115.0 +Problems : 31 (Average Length: 54.42 Splits: 0) +Lemmas : 233515 (Deleted: 213793) + Binary : 6399 (Ratio: 2.74%) + Ternary : 1833 (Ratio: 0.78%) + Conflict : 233515 (Average Length: 451.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 233515 (Average: 14.60 Max: 671 Sum: 3408356) + Executed : 233419 (Average: 14.58 Max: 671 Sum: 3405794 Ratio: 99.92%) + Bounded : 96 (Average: 26.69 Max: 87 Sum: 2562 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 : 436900 (Eliminated: 0 Frozen: 139842) +Constraints : 3214722 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 558MB +Max. Length : 85 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.12s +Memory: 517MB (+0MB) +UNKNOWN +Iteration Time: 7.15s + +Iteration 31 +Queue: [(13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 85 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 32 +Time : 165.808s (Solving: 152.82s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 165.764s + +Choices : 3968183 (Domain: 3865263) +Conflicts : 242078 (Analyzed: 242075) +Restarts : 2802 (Average: 86.39 Last: 170) +Model-Level : 115.0 +Problems : 32 (Average Length: 55.44 Splits: 0) +Lemmas : 242075 (Deleted: 220761) + Binary : 6554 (Ratio: 2.71%) + Ternary : 1852 (Ratio: 0.77%) + Conflict : 242075 (Average Length: 453.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 242075 (Average: 14.85 Max: 671 Sum: 3593818) + Executed : 241979 (Average: 14.84 Max: 671 Sum: 3591256 Ratio: 99.93%) + Bounded : 96 (Average: 26.69 Max: 87 Sum: 2562 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 : 436900 (Eliminated: 0 Frozen: 139842) +Constraints : 3214722 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 558MB +Max. Length : 85 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.16s +Memory: 517MB (+0MB) +UNKNOWN +Iteration Time: 6.20s + +Iteration 32 +Queue: [(14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 85 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 33 +Time : 172.520s (Solving: 159.43s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 172.480s + +Choices : 4167486 (Domain: 4063718) +Conflicts : 250408 (Analyzed: 250405) +Restarts : 2902 (Average: 86.29 Last: 170) +Model-Level : 115.0 +Problems : 33 (Average Length: 56.39 Splits: 0) +Lemmas : 250405 (Deleted: 228428) + Binary : 6708 (Ratio: 2.68%) + Ternary : 1869 (Ratio: 0.75%) + Conflict : 250405 (Average Length: 456.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 250405 (Average: 15.07 Max: 671 Sum: 3774797) + Executed : 250309 (Average: 15.06 Max: 671 Sum: 3772235 Ratio: 99.93%) + Bounded : 96 (Average: 26.69 Max: 87 Sum: 2562 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 : 436900 (Eliminated: 0 Frozen: 139842) +Constraints : 3214722 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 558MB +Max. Length : 85 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.68s +Memory: 517MB (+0MB) +UNKNOWN +Iteration Time: 6.72s + +Iteration 33 +Queue: [(15,75,1,True), (16,80,1,True), (17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 85 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 34 +Time : 180.578s (Solving: 167.39s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 180.544s + +Choices : 4486419 (Domain: 4380037) +Conflicts : 259607 (Analyzed: 259604) +Restarts : 3002 (Average: 86.48 Last: 170) +Model-Level : 115.0 +Problems : 34 (Average Length: 57.29 Splits: 0) +Lemmas : 259604 (Deleted: 238658) + Binary : 6852 (Ratio: 2.64%) + Ternary : 1890 (Ratio: 0.73%) + Conflict : 259604 (Average Length: 464.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 259604 (Average: 15.67 Max: 671 Sum: 4067138) + Executed : 259508 (Average: 15.66 Max: 671 Sum: 4064576 Ratio: 99.94%) + Bounded : 96 (Average: 26.69 Max: 87 Sum: 2562 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 : 3214722 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 558MB +Max. Length : 85 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.02s +Memory: 517MB (+0MB) +UNKNOWN +Iteration Time: 8.06s + +Iteration 34 +Queue: [(16,80,1,True), (17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 85 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 35 +Time : 189.102s (Solving: 175.83s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 189.072s + +Choices : 4720405 (Domain: 4608522) +Conflicts : 268308 (Analyzed: 268305) +Restarts : 3102 (Average: 86.49 Last: 170) +Model-Level : 115.0 +Problems : 35 (Average Length: 58.14 Splits: 0) +Lemmas : 268305 (Deleted: 247041) + Binary : 7140 (Ratio: 2.66%) + Ternary : 1925 (Ratio: 0.72%) + Conflict : 268305 (Average Length: 488.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 268305 (Average: 15.92 Max: 671 Sum: 4271683) + Executed : 268209 (Average: 15.91 Max: 671 Sum: 4269121 Ratio: 99.94%) + Bounded : 96 (Average: 26.69 Max: 87 Sum: 2562 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 : 3214722 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 558MB +Max. Length : 85 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.50s +Memory: 517MB (+0MB) +UNKNOWN +Iteration Time: 8.53s + +Iteration 35 +Queue: [(17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 85 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 36 +Time : 197.636s (Solving: 184.27s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 197.608s + +Choices : 4994690 (Domain: 4881787) +Conflicts : 277279 (Analyzed: 277276) +Restarts : 3202 (Average: 86.59 Last: 170) +Model-Level : 115.0 +Problems : 36 (Average Length: 58.94 Splits: 0) +Lemmas : 277276 (Deleted: 255140) + Binary : 7259 (Ratio: 2.62%) + Ternary : 1953 (Ratio: 0.70%) + Conflict : 277276 (Average Length: 492.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 277276 (Average: 16.31 Max: 671 Sum: 4521069) + Executed : 277180 (Average: 16.30 Max: 671 Sum: 4518507 Ratio: 99.94%) + Bounded : 96 (Average: 26.69 Max: 87 Sum: 2562 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 : 3214722 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 558MB +Max. Length : 85 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.51s +Memory: 517MB (+0MB) +UNKNOWN +Iteration Time: 8.54s + +Iteration 36 +Queue: [(18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 85 +Expected Memory: 565.0MB +Grounding... [('step', [86]), ('step', [87]), ('step', [88]), ('step', [89]), ('step', [90]), ('check', [90])] +Grounding Time: 0.37s +Memory: 517MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 37 +Time : 208.934s (Solving: 194.79s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 208.908s + +Choices : 5343023 (Domain: 5228839) +Conflicts : 287148 (Analyzed: 287145) +Restarts : 3302 (Average: 86.96 Last: 170) +Model-Level : 115.0 +Problems : 37 (Average Length: 59.84 Splits: 0) +Lemmas : 287145 (Deleted: 263928) + Binary : 7392 (Ratio: 2.57%) + Ternary : 1987 (Ratio: 0.69%) + Conflict : 287145 (Average Length: 506.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 287145 (Average: 16.85 Max: 671 Sum: 4839070) + Executed : 287049 (Average: 16.84 Max: 671 Sum: 4836508 Ratio: 99.95%) + Bounded : 96 (Average: 26.69 Max: 87 Sum: 2562 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 : 463296 (Eliminated: 0 Frozen: 148382) +Constraints : 3415792 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 580MB +Max. Length : 85 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 10.62s +Memory: 534MB (+17MB) +UNKNOWN +Iteration Time: 11.31s + +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.39s +Memory: 534MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 38 +Time : 218.549s (Solving: 203.58s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 218.528s + +Choices : 5669012 (Domain: 5553843) +Conflicts : 296063 (Analyzed: 296060) +Restarts : 3402 (Average: 87.03 Last: 170) +Model-Level : 115.0 +Problems : 38 (Average Length: 60.82 Splits: 0) +Lemmas : 296060 (Deleted: 273205) + Binary : 7498 (Ratio: 2.53%) + Ternary : 2002 (Ratio: 0.68%) + Conflict : 296060 (Average Length: 512.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 296060 (Average: 17.35 Max: 671 Sum: 5136959) + Executed : 295964 (Average: 17.34 Max: 671 Sum: 5134397 Ratio: 99.95%) + Bounded : 96 (Average: 26.69 Max: 87 Sum: 2562 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 : 489692 (Eliminated: 0 Frozen: 156922) +Constraints : 3616862 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 600MB +Max. Length : 90 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.89s +Memory: 590MB (+56MB) +UNKNOWN +Iteration Time: 9.63s + +Iteration 38 +Queue: [(20,100,0,True), (21,105,0,True)] +Grounded Until: 95 +Expected Memory: 646.0MB +Grounding... [('step', [96]), ('step', [97]), ('step', [98]), ('step', [99]), ('step', [100]), ('check', [100])] +Grounding Time: 0.39s +Memory: 590MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 39 +Time : 229.487s (Solving: 213.68s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 229.468s + +Choices : 6023692 (Domain: 5903315) +Conflicts : 304951 (Analyzed: 304948) +Restarts : 3502 (Average: 87.08 Last: 170) +Model-Level : 115.0 +Problems : 39 (Average Length: 61.87 Splits: 0) +Lemmas : 304948 (Deleted: 281699) + Binary : 7742 (Ratio: 2.54%) + Ternary : 2044 (Ratio: 0.67%) + Conflict : 304948 (Average Length: 532.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 304948 (Average: 17.88 Max: 804 Sum: 5451933) + Executed : 304852 (Average: 17.87 Max: 804 Sum: 5449371 Ratio: 99.95%) + Bounded : 96 (Average: 26.69 Max: 87 Sum: 2562 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 : 3817932 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 653MB +Max. Length : 95 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 10.21s +Memory: 593MB (+3MB) +UNKNOWN +Iteration Time: 10.95s + +Iteration 39 +Queue: [(21,105,0,True)] +Grounded Until: 100 +Expected Memory: 649.0MB +Grounding... [('step', [101]), ('step', [102]), ('step', [103]), ('step', [104]), ('step', [105]), ('check', [105])] +Grounding Time: 0.39s +Memory: 593MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 40 +Time : 240.042s (Solving: 223.38s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 240.024s + +Choices : 6379244 (Domain: 6257912) +Conflicts : 314000 (Analyzed: 313997) +Restarts : 3602 (Average: 87.17 Last: 170) +Model-Level : 115.0 +Problems : 40 (Average Length: 63.00 Splits: 0) +Lemmas : 313997 (Deleted: 290078) + Binary : 7969 (Ratio: 2.54%) + Ternary : 2063 (Ratio: 0.66%) + Conflict : 313997 (Average Length: 537.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 313997 (Average: 18.40 Max: 804 Sum: 5776888) + Executed : 313901 (Average: 18.39 Max: 804 Sum: 5774326 Ratio: 99.96%) + Bounded : 96 (Average: 26.69 Max: 87 Sum: 2562 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 : 4019002 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 664MB +Max. Length : 100 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.80s +Memory: 601MB (+8MB) +UNKNOWN +Iteration Time: 10.56s + +Iteration 40 +Queue: [(4,20,3,True), (5,25,3,True), (6,30,3,True), (7,35,2,True), (8,40,2,True), (9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,2,False), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Blocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 41 +Time : 243.410s (Solving: 226.62s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 243.396s + +Choices : 6430841 (Domain: 6309509) +Conflicts : 321968 (Analyzed: 321965) +Restarts : 3702 (Average: 86.97 Last: 170) +Model-Level : 115.0 +Problems : 41 (Average Length: 64.07 Splits: 0) +Lemmas : 321965 (Deleted: 296652) + Binary : 8159 (Ratio: 2.53%) + Ternary : 2097 (Ratio: 0.65%) + Conflict : 321965 (Average Length: 532.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 321965 (Average: 18.09 Max: 804 Sum: 5822997) + Executed : 321869 (Average: 18.08 Max: 804 Sum: 5820435 Ratio: 99.96%) + Bounded : 96 (Average: 26.69 Max: 87 Sum: 2562 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 : 4019002 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 664MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 3.32s +Memory: 607MB (+6MB) +UNKNOWN +Iteration Time: 3.37s + +Iteration 41 +Queue: [(5,25,3,True), (6,30,3,True), (7,35,2,True), (8,40,2,True), (9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,2,False), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 42 +Time : 251.218s (Solving: 234.30s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 251.208s + +Choices : 6495553 (Domain: 6374179) +Conflicts : 331081 (Analyzed: 331078) +Restarts : 3802 (Average: 87.08 Last: 170) +Model-Level : 115.0 +Problems : 42 (Average Length: 65.10 Splits: 0) +Lemmas : 331078 (Deleted: 306175) + Binary : 8297 (Ratio: 2.51%) + Ternary : 2135 (Ratio: 0.64%) + Conflict : 331078 (Average Length: 542.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 331078 (Average: 17.75 Max: 804 Sum: 5876081) + Executed : 330981 (Average: 17.74 Max: 804 Sum: 5873416 Ratio: 99.95%) + Bounded : 97 (Average: 27.47 Max: 103 Sum: 2665 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 : 4019002 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 664MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.77s +Memory: 607MB (+0MB) +UNKNOWN +Iteration Time: 7.81s + +Iteration 42 +Queue: [(6,30,3,True), (7,35,2,True), (8,40,2,True), (9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,2,False), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 43 +Time : 259.001s (Solving: 241.96s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 258.996s + +Choices : 6594146 (Domain: 6472016) +Conflicts : 340237 (Analyzed: 340234) +Restarts : 3902 (Average: 87.19 Last: 170) +Model-Level : 115.0 +Problems : 43 (Average Length: 66.07 Splits: 0) +Lemmas : 340234 (Deleted: 315492) + Binary : 8513 (Ratio: 2.50%) + Ternary : 2196 (Ratio: 0.65%) + Conflict : 340234 (Average Length: 558.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 340234 (Average: 17.50 Max: 804 Sum: 5954361) + Executed : 340137 (Average: 17.49 Max: 804 Sum: 5951696 Ratio: 99.96%) + Bounded : 97 (Average: 27.47 Max: 103 Sum: 2665 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 : 4019002 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 664MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.74s +Memory: 607MB (+0MB) +UNKNOWN +Iteration Time: 7.79s + +Iteration 43 +Queue: [(7,35,2,True), (8,40,2,True), (9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,2,False), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 44 +Time : 266.714s (Solving: 249.54s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 266.712s + +Choices : 6710814 (Domain: 6584758) +Conflicts : 349303 (Analyzed: 349300) +Restarts : 4002 (Average: 87.28 Last: 170) +Model-Level : 115.0 +Problems : 44 (Average Length: 67.00 Splits: 0) +Lemmas : 349300 (Deleted: 323636) + Binary : 8739 (Ratio: 2.50%) + Ternary : 2291 (Ratio: 0.66%) + Conflict : 349300 (Average Length: 564.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 349300 (Average: 17.32 Max: 804 Sum: 6050827) + Executed : 349203 (Average: 17.32 Max: 804 Sum: 6048162 Ratio: 99.96%) + Bounded : 97 (Average: 27.47 Max: 103 Sum: 2665 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 : 4019002 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 664MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.67s +Memory: 607MB (+0MB) +UNKNOWN +Iteration Time: 7.72s + +Iteration 44 +Queue: [(8,40,2,True), (9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,2,False), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 45 +Time : 274.357s (Solving: 257.07s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 274.356s + +Choices : 6830088 (Domain: 6703845) +Conflicts : 358717 (Analyzed: 358714) +Restarts : 4102 (Average: 87.45 Last: 170) +Model-Level : 115.0 +Problems : 45 (Average Length: 67.89 Splits: 0) +Lemmas : 358714 (Deleted: 332178) + Binary : 8867 (Ratio: 2.47%) + Ternary : 2311 (Ratio: 0.64%) + Conflict : 358714 (Average Length: 566.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 358714 (Average: 17.15 Max: 804 Sum: 6150549) + Executed : 358617 (Average: 17.14 Max: 804 Sum: 6147884 Ratio: 99.96%) + Bounded : 97 (Average: 27.47 Max: 103 Sum: 2665 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 : 4019002 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 664MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.61s +Memory: 607MB (+0MB) +UNKNOWN +Iteration Time: 7.65s + +Iteration 45 +Queue: [(9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,2,False), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 46 +Time : 281.607s (Solving: 264.20s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 281.612s + +Choices : 6925774 (Domain: 6799473) +Conflicts : 368019 (Analyzed: 368016) +Restarts : 4202 (Average: 87.58 Last: 170) +Model-Level : 115.0 +Problems : 46 (Average Length: 68.74 Splits: 0) +Lemmas : 368016 (Deleted: 341260) + Binary : 8922 (Ratio: 2.42%) + Ternary : 2321 (Ratio: 0.63%) + Conflict : 368016 (Average Length: 570.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 368016 (Average: 16.92 Max: 804 Sum: 6226794) + Executed : 367919 (Average: 16.91 Max: 804 Sum: 6224129 Ratio: 99.96%) + Bounded : 97 (Average: 27.47 Max: 103 Sum: 2665 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 : 4019002 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 664MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.21s +Memory: 607MB (+0MB) +UNKNOWN +Iteration Time: 7.26s + +Iteration 46 +Queue: [(10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,2,False), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 47 +Time : 289.739s (Solving: 272.19s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 289.748s + +Choices : 7038639 (Domain: 6911918) +Conflicts : 377264 (Analyzed: 377261) +Restarts : 4302 (Average: 87.69 Last: 170) +Model-Level : 115.0 +Problems : 47 (Average Length: 69.55 Splits: 0) +Lemmas : 377261 (Deleted: 350265) + Binary : 8987 (Ratio: 2.38%) + Ternary : 2340 (Ratio: 0.62%) + Conflict : 377261 (Average Length: 574.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 377261 (Average: 16.75 Max: 804 Sum: 6318417) + Executed : 377164 (Average: 16.74 Max: 804 Sum: 6315752 Ratio: 99.96%) + Bounded : 97 (Average: 27.47 Max: 103 Sum: 2665 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 : 4019002 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 664MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.08s +Memory: 607MB (+0MB) +UNKNOWN +Iteration Time: 8.14s + +Iteration 47 +Queue: [(11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,2,False), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 48 +Time : 297.757s (Solving: 280.06s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 297.768s + +Choices : 7160939 (Domain: 7033822) +Conflicts : 386539 (Analyzed: 386536) +Restarts : 4402 (Average: 87.81 Last: 170) +Model-Level : 115.0 +Problems : 48 (Average Length: 70.33 Splits: 0) +Lemmas : 386536 (Deleted: 359257) + Binary : 9080 (Ratio: 2.35%) + Ternary : 2363 (Ratio: 0.61%) + Conflict : 386536 (Average Length: 580.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 386536 (Average: 16.60 Max: 804 Sum: 6417714) + Executed : 386439 (Average: 16.60 Max: 804 Sum: 6415049 Ratio: 99.96%) + Bounded : 97 (Average: 27.47 Max: 103 Sum: 2665 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 : 4019002 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 664MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.97s +Memory: 607MB (+0MB) +UNKNOWN +Iteration Time: 8.02s + +Iteration 48 +Queue: [(12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,2,False), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 49 +Time : 305.694s (Solving: 287.89s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 305.708s + +Choices : 7303106 (Domain: 7175841) +Conflicts : 395708 (Analyzed: 395705) +Restarts : 4502 (Average: 87.90 Last: 170) +Model-Level : 115.0 +Problems : 49 (Average Length: 71.08 Splits: 0) +Lemmas : 395705 (Deleted: 368259) + Binary : 9116 (Ratio: 2.30%) + Ternary : 2370 (Ratio: 0.60%) + Conflict : 395705 (Average Length: 583.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 395705 (Average: 16.52 Max: 804 Sum: 6537132) + Executed : 395608 (Average: 16.51 Max: 804 Sum: 6534467 Ratio: 99.96%) + Bounded : 97 (Average: 27.47 Max: 103 Sum: 2665 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 : 4019002 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 664MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.90s +Memory: 607MB (+0MB) +UNKNOWN +Iteration Time: 7.94s + +Iteration 49 +Queue: [(13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,2,False), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 50 +Time : 313.828s (Solving: 295.89s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 313.844s + +Choices : 7504335 (Domain: 7375013) +Conflicts : 404707 (Analyzed: 404704) +Restarts : 4602 (Average: 87.94 Last: 170) +Model-Level : 115.0 +Problems : 50 (Average Length: 71.80 Splits: 0) +Lemmas : 404704 (Deleted: 377119) + Binary : 9336 (Ratio: 2.31%) + Ternary : 2454 (Ratio: 0.61%) + Conflict : 404704 (Average Length: 585.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 404704 (Average: 16.58 Max: 804 Sum: 6709035) + Executed : 404607 (Average: 16.57 Max: 804 Sum: 6706370 Ratio: 99.96%) + Bounded : 97 (Average: 27.47 Max: 103 Sum: 2665 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 : 4019002 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 664MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.09s +Memory: 607MB (+0MB) +UNKNOWN +Iteration Time: 8.14s + +Iteration 50 +Queue: [(18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 51 +Time : 322.691s (Solving: 304.63s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 322.700s + +Choices : 7621989 (Domain: 7492407) +Conflicts : 413223 (Analyzed: 413220) +Restarts : 4702 (Average: 87.88 Last: 170) +Model-Level : 115.0 +Problems : 51 (Average Length: 72.49 Splits: 0) +Lemmas : 413220 (Deleted: 384332) + Binary : 9393 (Ratio: 2.27%) + Ternary : 2460 (Ratio: 0.60%) + Conflict : 413220 (Average Length: 597.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 413220 (Average: 16.45 Max: 804 Sum: 6795908) + Executed : 413123 (Average: 16.44 Max: 804 Sum: 6793243 Ratio: 99.96%) + Bounded : 97 (Average: 27.47 Max: 103 Sum: 2665 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 : 4019002 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 664MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.81s +Memory: 607MB (+0MB) +UNKNOWN +Iteration Time: 8.86s + +Iteration 51 +Queue: [(19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 52 +Time : 331.604s (Solving: 313.40s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 331.616s + +Choices : 7799647 (Domain: 7669964) +Conflicts : 422499 (Analyzed: 422496) +Restarts : 4802 (Average: 87.98 Last: 170) +Model-Level : 115.0 +Problems : 52 (Average Length: 73.15 Splits: 0) +Lemmas : 422496 (Deleted: 394032) + Binary : 9435 (Ratio: 2.23%) + Ternary : 2470 (Ratio: 0.58%) + Conflict : 422496 (Average Length: 599.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 422496 (Average: 16.43 Max: 804 Sum: 6943636) + Executed : 422399 (Average: 16.43 Max: 804 Sum: 6940971 Ratio: 99.96%) + Bounded : 97 (Average: 27.47 Max: 103 Sum: 2665 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 : 4019002 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 664MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.86s +Memory: 607MB (+0MB) +UNKNOWN +Iteration Time: 8.92s + +Iteration 52 +Queue: [(20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 53 +Time : 341.232s (Solving: 322.92s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 341.248s + +Choices : 7985443 (Domain: 7854970) +Conflicts : 431998 (Analyzed: 431995) +Restarts : 4902 (Average: 88.13 Last: 170) +Model-Level : 115.0 +Problems : 53 (Average Length: 73.79 Splits: 0) +Lemmas : 431995 (Deleted: 403120) + Binary : 9499 (Ratio: 2.20%) + Ternary : 2479 (Ratio: 0.57%) + Conflict : 431995 (Average Length: 604.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 431995 (Average: 16.42 Max: 804 Sum: 7094388) + Executed : 431898 (Average: 16.42 Max: 804 Sum: 7091723 Ratio: 99.96%) + Bounded : 97 (Average: 27.47 Max: 103 Sum: 2665 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 : 4019002 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 664MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.59s +Memory: 607MB (+0MB) +UNKNOWN +Iteration Time: 9.64s + +Iteration 53 +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 : 54 +Time : 350.764s (Solving: 332.33s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 350.784s + +Choices : 8163807 (Domain: 8032808) +Conflicts : 441246 (Analyzed: 441243) +Restarts : 5002 (Average: 88.21 Last: 170) +Model-Level : 115.0 +Problems : 54 (Average Length: 74.41 Splits: 0) +Lemmas : 441243 (Deleted: 412313) + Binary : 9593 (Ratio: 2.17%) + Ternary : 2505 (Ratio: 0.57%) + Conflict : 441243 (Average Length: 606.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 441243 (Average: 16.41 Max: 804 Sum: 7239497) + Executed : 441146 (Average: 16.40 Max: 804 Sum: 7236832 Ratio: 99.96%) + Bounded : 97 (Average: 27.47 Max: 103 Sum: 2665 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 : 4019002 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 664MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.49s +Memory: 607MB (+0MB) +UNKNOWN +Iteration Time: 9.54s + +Iteration 54 +Queue: [(22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Expected Memory: 663.0MB +Grounding... [('step', [106]), ('step', [107]), ('step', [108]), ('step', [109]), ('step', [110]), ('check', [110])] +Grounding Time: 0.38s +Memory: 607MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 55 +Time : 360.243s (Solving: 340.96s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 360.268s + +Choices : 8299406 (Domain: 8168390) +Conflicts : 450657 (Analyzed: 450654) +Restarts : 5102 (Average: 88.33 Last: 170) +Model-Level : 115.0 +Problems : 55 (Average Length: 75.09 Splits: 0) +Lemmas : 450654 (Deleted: 421286) + Binary : 9645 (Ratio: 2.14%) + Ternary : 2509 (Ratio: 0.56%) + Conflict : 450654 (Average Length: 609.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 450654 (Average: 16.30 Max: 804 Sum: 7343702) + Executed : 450557 (Average: 16.29 Max: 804 Sum: 7341037 Ratio: 99.96%) + Bounded : 97 (Average: 27.47 Max: 103 Sum: 2665 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 : 4220072 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 680MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.74s +Memory: 621MB (+14MB) +UNKNOWN +Iteration Time: 9.49s + +Iteration 55 +Queue: [(23,115,0,True)] +Grounded Until: 110 +Expected Memory: 677.0MB +Grounding... [('step', [111]), ('step', [112]), ('step', [113]), ('step', [114]), ('step', [115]), ('check', [115])] +Grounding Time: 0.38s +Memory: 621MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 56 +Time : 371.728s (Solving: 351.59s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 371.760s + +Choices : 8452358 (Domain: 8321303) +Conflicts : 460582 (Analyzed: 460579) +Restarts : 5202 (Average: 88.54 Last: 170) +Model-Level : 115.0 +Problems : 56 (Average Length: 75.84 Splits: 0) +Lemmas : 460579 (Deleted: 430544) + Binary : 9673 (Ratio: 2.10%) + Ternary : 2521 (Ratio: 0.55%) + Conflict : 460579 (Average Length: 613.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 460579 (Average: 16.20 Max: 804 Sum: 7460145) + Executed : 460482 (Average: 16.19 Max: 804 Sum: 7457480 Ratio: 99.96%) + Bounded : 97 (Average: 27.47 Max: 103 Sum: 2665 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 : 4421142 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 706MB +Max. Length : 110 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 10.74s +Memory: 637MB (+16MB) +UNKNOWN +Iteration Time: 11.50s + +Iteration 56 +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 : 57 +Time : 374.767s (Solving: 354.48s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 374.796s + +Choices : 8496233 (Domain: 8365178) +Conflicts : 468049 (Analyzed: 468046) +Restarts : 5302 (Average: 88.28 Last: 170) +Model-Level : 115.0 +Problems : 57 (Average Length: 76.56 Splits: 0) +Lemmas : 468046 (Deleted: 438008) + Binary : 9722 (Ratio: 2.08%) + Ternary : 2533 (Ratio: 0.54%) + Conflict : 468046 (Average Length: 607.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 468046 (Average: 16.02 Max: 804 Sum: 7496619) + Executed : 467948 (Average: 16.01 Max: 804 Sum: 7493837 Ratio: 99.96%) + Bounded : 98 (Average: 28.39 Max: 117 Sum: 2782 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 : 4421142 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 706MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 2.99s +Memory: 637MB (+0MB) +UNKNOWN +Iteration Time: 3.04s + +Iteration 57 +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 : 58 +Time : 383.726s (Solving: 363.31s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 383.760s + +Choices : 8542421 (Domain: 8411366) +Conflicts : 476684 (Analyzed: 476681) +Restarts : 5402 (Average: 88.24 Last: 170) +Model-Level : 115.0 +Problems : 58 (Average Length: 77.26 Splits: 0) +Lemmas : 476681 (Deleted: 447362) + Binary : 9760 (Ratio: 2.05%) + Ternary : 2544 (Ratio: 0.53%) + Conflict : 476681 (Average Length: 617.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 476681 (Average: 15.80 Max: 804 Sum: 7529934) + Executed : 476583 (Average: 15.79 Max: 804 Sum: 7527152 Ratio: 99.96%) + Bounded : 98 (Average: 28.39 Max: 117 Sum: 2782 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 : 4421128 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 706MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.92s +Memory: 637MB (+0MB) +UNKNOWN +Iteration Time: 8.97s + +Iteration 58 +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 : 59 +Time : 391.228s (Solving: 370.68s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 391.264s + +Choices : 8618700 (Domain: 8487645) +Conflicts : 485737 (Analyzed: 485734) +Restarts : 5502 (Average: 88.28 Last: 170) +Model-Level : 115.0 +Problems : 59 (Average Length: 77.93 Splits: 0) +Lemmas : 485734 (Deleted: 455742) + Binary : 9883 (Ratio: 2.03%) + Ternary : 2566 (Ratio: 0.53%) + Conflict : 485734 (Average Length: 621.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 485734 (Average: 15.62 Max: 804 Sum: 7587479) + Executed : 485636 (Average: 15.61 Max: 804 Sum: 7584697 Ratio: 99.96%) + Bounded : 98 (Average: 28.39 Max: 117 Sum: 2782 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 : 4421128 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 706MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.46s +Memory: 637MB (+0MB) +UNKNOWN +Iteration Time: 7.51s + +Iteration 59 +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 : 60 +Time : 398.492s (Solving: 377.82s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 398.532s + +Choices : 8689250 (Domain: 8557293) +Conflicts : 494574 (Analyzed: 494571) +Restarts : 5602 (Average: 88.28 Last: 170) +Model-Level : 115.0 +Problems : 60 (Average Length: 78.58 Splits: 0) +Lemmas : 494571 (Deleted: 464538) + Binary : 9965 (Ratio: 2.01%) + Ternary : 2573 (Ratio: 0.52%) + Conflict : 494571 (Average Length: 625.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 494571 (Average: 15.44 Max: 804 Sum: 7637879) + Executed : 494473 (Average: 15.44 Max: 804 Sum: 7635097 Ratio: 99.96%) + Bounded : 98 (Average: 28.39 Max: 117 Sum: 2782 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 : 4421128 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 706MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.23s +Memory: 637MB (+0MB) +UNKNOWN +Iteration Time: 7.27s + +Iteration 60 +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 : 61 +Time : 405.756s (Solving: 384.97s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 405.800s + +Choices : 8797588 (Domain: 8660669) +Conflicts : 503822 (Analyzed: 503819) +Restarts : 5702 (Average: 88.36 Last: 170) +Model-Level : 115.0 +Problems : 61 (Average Length: 79.21 Splits: 0) +Lemmas : 503819 (Deleted: 472749) + Binary : 10220 (Ratio: 2.03%) + Ternary : 2595 (Ratio: 0.52%) + Conflict : 503819 (Average Length: 627.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 503819 (Average: 15.32 Max: 804 Sum: 7718391) + Executed : 503721 (Average: 15.31 Max: 804 Sum: 7715609 Ratio: 99.96%) + Bounded : 98 (Average: 28.39 Max: 117 Sum: 2782 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 : 4421128 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 706MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.23s +Memory: 637MB (+0MB) +UNKNOWN +Iteration Time: 7.27s + +Iteration 61 +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 : 62 +Time : 413.314s (Solving: 392.40s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 413.360s + +Choices : 8880447 (Domain: 8743518) +Conflicts : 512942 (Analyzed: 512939) +Restarts : 5802 (Average: 88.41 Last: 170) +Model-Level : 115.0 +Problems : 62 (Average Length: 79.82 Splits: 0) +Lemmas : 512939 (Deleted: 481710) + Binary : 10279 (Ratio: 2.00%) + Ternary : 2607 (Ratio: 0.51%) + Conflict : 512939 (Average Length: 632.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 512939 (Average: 15.17 Max: 804 Sum: 7780418) + Executed : 512841 (Average: 15.16 Max: 804 Sum: 7777636 Ratio: 99.96%) + Bounded : 98 (Average: 28.39 Max: 117 Sum: 2782 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 : 4421128 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 706MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.52s +Memory: 637MB (+0MB) +UNKNOWN +Iteration Time: 7.56s + +Iteration 62 +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 : 63 +Time : 420.951s (Solving: 399.89s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 421.000s + +Choices : 8967467 (Domain: 8830526) +Conflicts : 522172 (Analyzed: 522169) +Restarts : 5902 (Average: 88.47 Last: 170) +Model-Level : 115.0 +Problems : 63 (Average Length: 80.41 Splits: 0) +Lemmas : 522169 (Deleted: 490655) + Binary : 10305 (Ratio: 1.97%) + Ternary : 2609 (Ratio: 0.50%) + Conflict : 522169 (Average Length: 632.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 522169 (Average: 15.03 Max: 804 Sum: 7846405) + Executed : 522071 (Average: 15.02 Max: 804 Sum: 7843623 Ratio: 99.96%) + Bounded : 98 (Average: 28.39 Max: 117 Sum: 2782 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 : 4421128 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 706MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.58s +Memory: 637MB (+0MB) +UNKNOWN +Iteration Time: 7.64s + +Iteration 63 +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 : 64 +Time : 429.223s (Solving: 408.02s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 429.276s + +Choices : 9059058 (Domain: 8922095) +Conflicts : 531500 (Analyzed: 531497) +Restarts : 6002 (Average: 88.55 Last: 170) +Model-Level : 115.0 +Problems : 64 (Average Length: 80.98 Splits: 0) +Lemmas : 531497 (Deleted: 499685) + Binary : 10323 (Ratio: 1.94%) + Ternary : 2611 (Ratio: 0.49%) + Conflict : 531497 (Average Length: 634.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 531497 (Average: 14.89 Max: 804 Sum: 7913250) + Executed : 531399 (Average: 14.88 Max: 804 Sum: 7910468 Ratio: 99.96%) + Bounded : 98 (Average: 28.39 Max: 117 Sum: 2782 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 : 4421128 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 706MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.22s +Memory: 637MB (+0MB) +UNKNOWN +Iteration Time: 8.28s + +Iteration 64 +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 : 65 +Time : 437.536s (Solving: 416.21s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 437.592s + +Choices : 9153270 (Domain: 9016300) +Conflicts : 540952 (Analyzed: 540949) +Restarts : 6102 (Average: 88.65 Last: 172) +Model-Level : 115.0 +Problems : 65 (Average Length: 81.54 Splits: 0) +Lemmas : 540949 (Deleted: 508794) + Binary : 10347 (Ratio: 1.91%) + Ternary : 2614 (Ratio: 0.48%) + Conflict : 540949 (Average Length: 636.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 540949 (Average: 14.75 Max: 804 Sum: 7981558) + Executed : 540851 (Average: 14.75 Max: 804 Sum: 7978776 Ratio: 99.97%) + Bounded : 98 (Average: 28.39 Max: 117 Sum: 2782 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 : 4421128 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 706MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.27s +Memory: 637MB (+0MB) +UNKNOWN +Iteration Time: 8.32s + +Iteration 65 +Queue: [(22,110,1,True), (23,115,1,True)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 66 +Time : 447.483s (Solving: 426.01s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 447.540s + +Choices : 9264003 (Domain: 9126961) +Conflicts : 550781 (Analyzed: 550778) +Restarts : 6202 (Average: 88.81 Last: 172) +Model-Level : 115.0 +Problems : 66 (Average Length: 82.08 Splits: 0) +Lemmas : 550778 (Deleted: 518071) + Binary : 10367 (Ratio: 1.88%) + Ternary : 2621 (Ratio: 0.48%) + Conflict : 550778 (Average Length: 640.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 550778 (Average: 14.63 Max: 804 Sum: 8058202) + Executed : 550680 (Average: 14.63 Max: 804 Sum: 8055420 Ratio: 99.97%) + Bounded : 98 (Average: 28.39 Max: 117 Sum: 2782 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 : 4421128 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 706MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.90s +Memory: 637MB (+0MB) +UNKNOWN +Iteration Time: 9.95s + +Iteration 66 +Queue: [(23,115,1,True)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 67 +Time : 456.370s (Solving: 434.76s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 456.432s + +Choices : 9380536 (Domain: 9243485) +Conflicts : 560063 (Analyzed: 560060) +Restarts : 6302 (Average: 88.87 Last: 172) +Model-Level : 115.0 +Problems : 67 (Average Length: 82.60 Splits: 0) +Lemmas : 560060 (Deleted: 527755) + Binary : 10416 (Ratio: 1.86%) + Ternary : 2622 (Ratio: 0.47%) + Conflict : 560060 (Average Length: 642.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 560060 (Average: 14.54 Max: 804 Sum: 8141773) + Executed : 559962 (Average: 14.53 Max: 804 Sum: 8138991 Ratio: 99.97%) + Bounded : 98 (Average: 28.39 Max: 117 Sum: 2782 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 : 4421128 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 706MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.84s +Memory: 637MB (+0MB) +UNKNOWN +Iteration Time: 8.89s + +Iteration 67 +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 : 68 +Time : 459.552s (Solving: 437.79s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 459.616s + +Choices : 9434154 (Domain: 9297103) +Conflicts : 567639 (Analyzed: 567636) +Restarts : 6402 (Average: 88.67 Last: 172) +Model-Level : 115.0 +Problems : 68 (Average Length: 83.10 Splits: 0) +Lemmas : 567636 (Deleted: 534523) + Binary : 10500 (Ratio: 1.85%) + Ternary : 2643 (Ratio: 0.47%) + Conflict : 567636 (Average Length: 637.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 567636 (Average: 14.43 Max: 804 Sum: 8190438) + Executed : 567535 (Average: 14.42 Max: 804 Sum: 8187305 Ratio: 99.96%) + Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 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 : 4421128 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 706MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 3.13s +Memory: 637MB (+0MB) +UNKNOWN +Iteration Time: 3.19s + +Iteration 68 +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 : 69 +Time : 470.051s (Solving: 448.16s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 470.116s + +Choices : 9482131 (Domain: 9345080) +Conflicts : 576664 (Analyzed: 576661) +Restarts : 6502 (Average: 88.69 Last: 172) +Model-Level : 115.0 +Problems : 69 (Average Length: 83.59 Splits: 0) +Lemmas : 576661 (Deleted: 543859) + Binary : 10552 (Ratio: 1.83%) + Ternary : 2651 (Ratio: 0.46%) + Conflict : 576661 (Average Length: 650.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 576661 (Average: 14.26 Max: 804 Sum: 8224004) + Executed : 576560 (Average: 14.26 Max: 804 Sum: 8220871 Ratio: 99.96%) + Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 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 : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 765MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 10.45s +Memory: 701MB (+64MB) +UNKNOWN +Iteration Time: 10.51s + +Iteration 69 +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 : 70 +Time : 476.594s (Solving: 454.55s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 476.660s + +Choices : 9557144 (Domain: 9420093) +Conflicts : 585502 (Analyzed: 585499) +Restarts : 6602 (Average: 88.69 Last: 172) +Model-Level : 115.0 +Problems : 70 (Average Length: 84.07 Splits: 0) +Lemmas : 585499 (Deleted: 552610) + Binary : 10648 (Ratio: 1.82%) + Ternary : 2662 (Ratio: 0.45%) + Conflict : 585499 (Average Length: 653.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 585499 (Average: 14.14 Max: 804 Sum: 8280709) + Executed : 585398 (Average: 14.14 Max: 804 Sum: 8277576 Ratio: 99.96%) + Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 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 : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 765MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.49s +Memory: 701MB (+0MB) +UNKNOWN +Iteration Time: 6.55s + +Iteration 70 +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 : 71 +Time : 484.082s (Solving: 461.92s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 484.152s + +Choices : 9635294 (Domain: 9497946) +Conflicts : 595789 (Analyzed: 595786) +Restarts : 6702 (Average: 88.90 Last: 172) +Model-Level : 115.0 +Problems : 71 (Average Length: 84.54 Splits: 0) +Lemmas : 595786 (Deleted: 561289) + Binary : 10713 (Ratio: 1.80%) + Ternary : 2669 (Ratio: 0.45%) + Conflict : 595786 (Average Length: 653.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 595786 (Average: 14.00 Max: 804 Sum: 8340737) + Executed : 595685 (Average: 13.99 Max: 804 Sum: 8337604 Ratio: 99.96%) + Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 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 : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 765MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.45s +Memory: 701MB (+0MB) +UNKNOWN +Iteration Time: 7.49s + +Iteration 71 +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 : 72 +Time : 491.756s (Solving: 469.45s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 491.828s + +Choices : 9707894 (Domain: 9570482) +Conflicts : 605018 (Analyzed: 605015) +Restarts : 6802 (Average: 88.95 Last: 172) +Model-Level : 115.0 +Problems : 72 (Average Length: 84.99 Splits: 0) +Lemmas : 605015 (Deleted: 571311) + Binary : 10761 (Ratio: 1.78%) + Ternary : 2675 (Ratio: 0.44%) + Conflict : 605015 (Average Length: 657.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 605015 (Average: 13.87 Max: 804 Sum: 8391385) + Executed : 604914 (Average: 13.86 Max: 804 Sum: 8388252 Ratio: 99.96%) + Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 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 : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 765MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.63s +Memory: 701MB (+0MB) +UNKNOWN +Iteration Time: 7.68s + +Iteration 72 +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 : 73 +Time : 499.479s (Solving: 477.02s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 499.552s + +Choices : 9782772 (Domain: 9645348) +Conflicts : 615176 (Analyzed: 615173) +Restarts : 6902 (Average: 89.13 Last: 172) +Model-Level : 115.0 +Problems : 73 (Average Length: 85.42 Splits: 0) +Lemmas : 615173 (Deleted: 580367) + Binary : 10788 (Ratio: 1.75%) + Ternary : 2675 (Ratio: 0.43%) + Conflict : 615173 (Average Length: 657.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 615173 (Average: 13.73 Max: 804 Sum: 8445699) + Executed : 615072 (Average: 13.72 Max: 804 Sum: 8442566 Ratio: 99.96%) + Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 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 : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 765MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.67s +Memory: 701MB (+0MB) +UNKNOWN +Iteration Time: 7.73s + +Iteration 73 +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 : 74 +Time : 507.094s (Solving: 484.51s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 507.168s + +Choices : 9855687 (Domain: 9718221) +Conflicts : 624144 (Analyzed: 624141) +Restarts : 7002 (Average: 89.14 Last: 172) +Model-Level : 115.0 +Problems : 74 (Average Length: 85.85 Splits: 0) +Lemmas : 624141 (Deleted: 590302) + Binary : 10814 (Ratio: 1.73%) + Ternary : 2685 (Ratio: 0.43%) + Conflict : 624141 (Average Length: 660.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 624141 (Average: 13.61 Max: 804 Sum: 8495389) + Executed : 624040 (Average: 13.61 Max: 804 Sum: 8492256 Ratio: 99.96%) + Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 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 : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 765MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.58s +Memory: 701MB (+0MB) +UNKNOWN +Iteration Time: 7.62s + +Iteration 74 +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 : 75 +Time : 514.984s (Solving: 492.28s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 515.060s + +Choices : 9923181 (Domain: 9785715) +Conflicts : 633437 (Analyzed: 633434) +Restarts : 7102 (Average: 89.19 Last: 172) +Model-Level : 115.0 +Problems : 75 (Average Length: 86.27 Splits: 0) +Lemmas : 633434 (Deleted: 599117) + Binary : 10832 (Ratio: 1.71%) + Ternary : 2689 (Ratio: 0.42%) + Conflict : 633434 (Average Length: 663.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 633434 (Average: 13.48 Max: 804 Sum: 8537864) + Executed : 633333 (Average: 13.47 Max: 804 Sum: 8534731 Ratio: 99.96%) + Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 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 : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 765MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.85s +Memory: 701MB (+0MB) +UNKNOWN +Iteration Time: 7.90s + +Iteration 75 +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 : 76 +Time : 523.361s (Solving: 500.52s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 523.440s + +Choices : 10023275 (Domain: 9885660) +Conflicts : 643207 (Analyzed: 643204) +Restarts : 7202 (Average: 89.31 Last: 172) +Model-Level : 115.0 +Problems : 76 (Average Length: 86.67 Splits: 0) +Lemmas : 643204 (Deleted: 608177) + Binary : 10876 (Ratio: 1.69%) + Ternary : 2695 (Ratio: 0.42%) + Conflict : 643204 (Average Length: 665.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 643204 (Average: 13.38 Max: 804 Sum: 8609242) + Executed : 643103 (Average: 13.38 Max: 804 Sum: 8606109 Ratio: 99.96%) + Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 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 : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 765MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.33s +Memory: 701MB (+0MB) +UNKNOWN +Iteration Time: 8.38s + +Iteration 76 +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 : 77 +Time : 531.762s (Solving: 508.78s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 531.844s + +Choices : 10107051 (Domain: 9969435) +Conflicts : 652228 (Analyzed: 652225) +Restarts : 7302 (Average: 89.32 Last: 172) +Model-Level : 115.0 +Problems : 77 (Average Length: 87.06 Splits: 0) +Lemmas : 652225 (Deleted: 617783) + Binary : 10887 (Ratio: 1.67%) + Ternary : 2699 (Ratio: 0.41%) + Conflict : 652225 (Average Length: 669.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 652225 (Average: 13.29 Max: 804 Sum: 8665447) + Executed : 652124 (Average: 13.28 Max: 804 Sum: 8662314 Ratio: 99.96%) + Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 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 : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 765MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.35s +Memory: 701MB (+0MB) +UNKNOWN +Iteration Time: 8.41s + +Iteration 77 +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 : 78 +Time : 534.891s (Solving: 511.78s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 534.972s + +Choices : 10158302 (Domain: 10020686) +Conflicts : 659798 (Analyzed: 659795) +Restarts : 7402 (Average: 89.14 Last: 172) +Model-Level : 115.0 +Problems : 78 (Average Length: 87.45 Splits: 0) +Lemmas : 659795 (Deleted: 624374) + Binary : 10965 (Ratio: 1.66%) + Ternary : 2706 (Ratio: 0.41%) + Conflict : 659795 (Average Length: 663.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 659795 (Average: 13.19 Max: 804 Sum: 8702473) + Executed : 659694 (Average: 13.18 Max: 804 Sum: 8699340 Ratio: 99.96%) + Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 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 : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 765MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 3.08s +Memory: 701MB (+0MB) +UNKNOWN +Iteration Time: 3.13s + +Iteration 78 +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 : 79 +Time : 544.334s (Solving: 521.10s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 544.420s + +Choices : 10197256 (Domain: 10059640) +Conflicts : 667894 (Analyzed: 667891) +Restarts : 7502 (Average: 89.03 Last: 172) +Model-Level : 115.0 +Problems : 79 (Average Length: 87.82 Splits: 0) +Lemmas : 667891 (Deleted: 631853) + Binary : 10983 (Ratio: 1.64%) + Ternary : 2717 (Ratio: 0.41%) + Conflict : 667891 (Average Length: 675.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 667891 (Average: 13.07 Max: 804 Sum: 8731224) + Executed : 667790 (Average: 13.07 Max: 804 Sum: 8728091 Ratio: 99.96%) + Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 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 : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 765MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.41s +Memory: 701MB (+0MB) +UNKNOWN +Iteration Time: 9.45s + +Iteration 79 +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 : 80 +Time : 552.480s (Solving: 529.09s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 552.568s + +Choices : 10271487 (Domain: 10133871) +Conflicts : 676239 (Analyzed: 676236) +Restarts : 7602 (Average: 88.96 Last: 172) +Model-Level : 115.0 +Problems : 80 (Average Length: 88.19 Splits: 0) +Lemmas : 676236 (Deleted: 639948) + Binary : 11038 (Ratio: 1.63%) + Ternary : 2728 (Ratio: 0.40%) + Conflict : 676236 (Average Length: 679.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 676236 (Average: 13.00 Max: 804 Sum: 8788265) + Executed : 676135 (Average: 12.99 Max: 804 Sum: 8785132 Ratio: 99.96%) + Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 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 : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 765MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.08s +Memory: 701MB (+0MB) +UNKNOWN +Iteration Time: 8.15s + +Iteration 80 +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 : 81 +Time : 559.310s (Solving: 535.80s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 559.400s + +Choices : 10337609 (Domain: 10199947) +Conflicts : 685769 (Analyzed: 685766) +Restarts : 7702 (Average: 89.04 Last: 172) +Model-Level : 115.0 +Problems : 81 (Average Length: 88.54 Splits: 0) +Lemmas : 685766 (Deleted: 649978) + Binary : 11077 (Ratio: 1.62%) + Ternary : 2735 (Ratio: 0.40%) + Conflict : 685766 (Average Length: 679.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 685766 (Average: 12.89 Max: 804 Sum: 8837229) + Executed : 685665 (Average: 12.88 Max: 804 Sum: 8834096 Ratio: 99.96%) + Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 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 : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 765MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.79s +Memory: 701MB (+0MB) +UNKNOWN +Iteration Time: 6.84s + +Iteration 81 +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 : 82 +Time : 566.491s (Solving: 542.86s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 566.584s + +Choices : 10402205 (Domain: 10264543) +Conflicts : 694775 (Analyzed: 694772) +Restarts : 7802 (Average: 89.05 Last: 172) +Model-Level : 115.0 +Problems : 82 (Average Length: 88.89 Splits: 0) +Lemmas : 694772 (Deleted: 659325) + Binary : 11104 (Ratio: 1.60%) + Ternary : 2740 (Ratio: 0.39%) + Conflict : 694772 (Average Length: 682.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 694772 (Average: 12.78 Max: 804 Sum: 8882600) + Executed : 694671 (Average: 12.78 Max: 804 Sum: 8879467 Ratio: 99.96%) + Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 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 : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 765MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.14s +Memory: 701MB (+0MB) +UNKNOWN +Iteration Time: 7.19s + +Iteration 82 +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 : 83 +Time : 573.665s (Solving: 549.90s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 573.760s + +Choices : 10471274 (Domain: 10333596) +Conflicts : 703729 (Analyzed: 703726) +Restarts : 7902 (Average: 89.06 Last: 172) +Model-Level : 115.0 +Problems : 83 (Average Length: 89.23 Splits: 0) +Lemmas : 703726 (Deleted: 668164) + Binary : 11147 (Ratio: 1.58%) + Ternary : 2742 (Ratio: 0.39%) + Conflict : 703726 (Average Length: 685.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 703726 (Average: 12.69 Max: 804 Sum: 8929593) + Executed : 703625 (Average: 12.68 Max: 804 Sum: 8926460 Ratio: 99.96%) + Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 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 : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 765MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.13s +Memory: 701MB (+0MB) +UNKNOWN +Iteration Time: 7.18s + +Iteration 83 +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 : 84 +Time : 581.706s (Solving: 557.82s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 581.804s + +Choices : 10551647 (Domain: 10413967) +Conflicts : 713098 (Analyzed: 713095) +Restarts : 8002 (Average: 89.11 Last: 172) +Model-Level : 115.0 +Problems : 84 (Average Length: 89.56 Splits: 0) +Lemmas : 713095 (Deleted: 676932) + Binary : 11170 (Ratio: 1.57%) + Ternary : 2753 (Ratio: 0.39%) + Conflict : 713095 (Average Length: 687.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 713095 (Average: 12.60 Max: 804 Sum: 8986082) + Executed : 712994 (Average: 12.60 Max: 804 Sum: 8982949 Ratio: 99.97%) + Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 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 : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 765MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.00s +Memory: 701MB (+0MB) +UNKNOWN +Iteration Time: 8.05s + +Iteration 84 +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 : 85 +Time : 590.176s (Solving: 566.16s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 590.276s + +Choices : 10649622 (Domain: 10511921) +Conflicts : 722224 (Analyzed: 722221) +Restarts : 8102 (Average: 89.14 Last: 172) +Model-Level : 115.0 +Problems : 85 (Average Length: 89.88 Splits: 0) +Lemmas : 722221 (Deleted: 686115) + Binary : 11200 (Ratio: 1.55%) + Ternary : 2758 (Ratio: 0.38%) + Conflict : 722221 (Average Length: 688.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 722221 (Average: 12.54 Max: 804 Sum: 9055371) + Executed : 722120 (Average: 12.53 Max: 804 Sum: 9052238 Ratio: 99.97%) + Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 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 : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 765MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.43s +Memory: 701MB (+0MB) +UNKNOWN +Iteration Time: 8.48s + +Iteration 85 +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 : 86 +Time : 593.536s (Solving: 569.38s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 593.636s + +Choices : 10709382 (Domain: 10571681) +Conflicts : 730159 (Analyzed: 730156) +Restarts : 8202 (Average: 89.02 Last: 172) +Model-Level : 115.0 +Problems : 86 (Average Length: 90.20 Splits: 0) +Lemmas : 730156 (Deleted: 692780) + Binary : 11262 (Ratio: 1.54%) + Ternary : 2768 (Ratio: 0.38%) + Conflict : 730156 (Average Length: 683.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 730156 (Average: 12.47 Max: 804 Sum: 9106231) + Executed : 730055 (Average: 12.47 Max: 804 Sum: 9103098 Ratio: 99.97%) + Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 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 : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 765MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 3.31s +Memory: 701MB (+0MB) +UNKNOWN +Iteration Time: 3.37s + +Iteration 86 +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 : 87 +Time : 602.390s (Solving: 578.09s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 602.496s + +Choices : 10752690 (Domain: 10614989) +Conflicts : 738328 (Analyzed: 738325) +Restarts : 8302 (Average: 88.93 Last: 172) +Model-Level : 115.0 +Problems : 87 (Average Length: 90.51 Splits: 0) +Lemmas : 738325 (Deleted: 700549) + Binary : 11278 (Ratio: 1.53%) + Ternary : 2776 (Ratio: 0.38%) + Conflict : 738325 (Average Length: 688.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 738325 (Average: 12.38 Max: 804 Sum: 9139428) + Executed : 738224 (Average: 12.37 Max: 804 Sum: 9136295 Ratio: 99.97%) + Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 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 : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 765MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.81s +Memory: 701MB (+0MB) +UNKNOWN +Iteration Time: 8.86s + +Iteration 87 +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 : 88 +Time : 608.995s (Solving: 584.56s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 609.108s + +Choices : 10813516 (Domain: 10675815) +Conflicts : 746953 (Analyzed: 746950) +Restarts : 8402 (Average: 88.90 Last: 172) +Model-Level : 115.0 +Problems : 88 (Average Length: 90.81 Splits: 0) +Lemmas : 746950 (Deleted: 710805) + Binary : 11291 (Ratio: 1.51%) + Ternary : 2780 (Ratio: 0.37%) + Conflict : 746950 (Average Length: 689.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 746950 (Average: 12.29 Max: 804 Sum: 9180716) + Executed : 746849 (Average: 12.29 Max: 804 Sum: 9177583 Ratio: 99.97%) + Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 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 : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 765MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.56s +Memory: 701MB (+0MB) +UNKNOWN +Iteration Time: 6.61s + +Iteration 88 +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 : 89 +Time : 615.995s (Solving: 591.44s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 616.112s + +Choices : 10890578 (Domain: 10752791) +Conflicts : 755509 (Analyzed: 755506) +Restarts : 8502 (Average: 88.86 Last: 172) +Model-Level : 115.0 +Problems : 89 (Average Length: 91.10 Splits: 0) +Lemmas : 755506 (Deleted: 717125) + Binary : 11326 (Ratio: 1.50%) + Ternary : 2804 (Ratio: 0.37%) + Conflict : 755506 (Average Length: 691.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 755506 (Average: 12.22 Max: 804 Sum: 9234773) + Executed : 755405 (Average: 12.22 Max: 804 Sum: 9231640 Ratio: 99.97%) + Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 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 : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 765MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.96s +Memory: 701MB (+0MB) +UNKNOWN +Iteration Time: 7.01s + +Iteration 89 +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 : 90 +Time : 623.170s (Solving: 598.47s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 623.292s + +Choices : 10962157 (Domain: 10824370) +Conflicts : 764947 (Analyzed: 764944) +Restarts : 8602 (Average: 88.93 Last: 172) +Model-Level : 115.0 +Problems : 90 (Average Length: 91.39 Splits: 0) +Lemmas : 764944 (Deleted: 727704) + Binary : 11341 (Ratio: 1.48%) + Ternary : 2805 (Ratio: 0.37%) + Conflict : 764944 (Average Length: 692.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 764944 (Average: 12.14 Max: 804 Sum: 9284631) + Executed : 764843 (Average: 12.13 Max: 804 Sum: 9281498 Ratio: 99.97%) + Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 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 : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 765MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.12s +Memory: 701MB (+0MB) +UNKNOWN +Iteration Time: 7.18s + +Iteration 90 +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 : 91 +Time : 632.132s (Solving: 607.28s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 632.256s + +Choices : 11167284 (Domain: 11026963) +Conflicts : 774502 (Analyzed: 774499) +Restarts : 8702 (Average: 89.00 Last: 172) +Model-Level : 115.0 +Problems : 91 (Average Length: 91.67 Splits: 0) +Lemmas : 774499 (Deleted: 736613) + Binary : 11533 (Ratio: 1.49%) + Ternary : 2817 (Ratio: 0.36%) + Conflict : 774499 (Average Length: 693.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 774499 (Average: 12.21 Max: 804 Sum: 9454212) + Executed : 774398 (Average: 12.20 Max: 804 Sum: 9451079 Ratio: 99.97%) + Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 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 : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 765MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.91s +Memory: 701MB (+0MB) +UNKNOWN +Iteration Time: 8.97s + +Iteration 91 +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 : 92 +Time : 640.000s (Solving: 614.98s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 640.128s + +Choices : 11248145 (Domain: 11107823) +Conflicts : 783668 (Analyzed: 783665) +Restarts : 8802 (Average: 89.03 Last: 184) +Model-Level : 115.0 +Problems : 92 (Average Length: 91.95 Splits: 0) +Lemmas : 783665 (Deleted: 746031) + Binary : 11547 (Ratio: 1.47%) + Ternary : 2818 (Ratio: 0.36%) + Conflict : 783665 (Average Length: 693.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 783665 (Average: 12.13 Max: 804 Sum: 9509243) + Executed : 783564 (Average: 12.13 Max: 804 Sum: 9506110 Ratio: 99.97%) + Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 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 : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 765MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.81s +Memory: 701MB (+0MB) +UNKNOWN +Iteration Time: 7.88s + +Iteration 92 +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 : 93 +Time : 649.676s (Solving: 624.50s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 649.804s + +Choices : 11356158 (Domain: 11215833) +Conflicts : 793553 (Analyzed: 793550) +Restarts : 8902 (Average: 89.14 Last: 184) +Model-Level : 115.0 +Problems : 93 (Average Length: 92.22 Splits: 0) +Lemmas : 793550 (Deleted: 755022) + Binary : 11594 (Ratio: 1.46%) + Ternary : 2832 (Ratio: 0.36%) + Conflict : 793550 (Average Length: 693.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 793550 (Average: 12.08 Max: 804 Sum: 9587789) + Executed : 793449 (Average: 12.08 Max: 804 Sum: 9584656 Ratio: 99.97%) + Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 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 : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 765MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.62s +Memory: 701MB (+0MB) +UNKNOWN +Iteration Time: 9.68s + +Iteration 93 +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 : 94 +Time : 652.896s (Solving: 627.60s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 653.028s + +Choices : 11405512 (Domain: 11265187) +Conflicts : 801159 (Analyzed: 801156) +Restarts : 9002 (Average: 89.00 Last: 184) +Model-Level : 115.0 +Problems : 94 (Average Length: 92.48 Splits: 0) +Lemmas : 801156 (Deleted: 762483) + Binary : 11661 (Ratio: 1.46%) + Ternary : 2841 (Ratio: 0.35%) + Conflict : 801156 (Average Length: 689.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 801156 (Average: 12.02 Max: 804 Sum: 9630252) + Executed : 801055 (Average: 12.02 Max: 804 Sum: 9627119 Ratio: 99.97%) + Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 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 : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 765MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 3.18s +Memory: 701MB (+0MB) +UNKNOWN +Iteration Time: 3.22s + +Iteration 94 +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 : 95 +Time : 663.475s (Solving: 638.06s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 663.612s + +Choices : 11460353 (Domain: 11320028) +Conflicts : 810194 (Analyzed: 810191) +Restarts : 9102 (Average: 89.01 Last: 184) +Model-Level : 115.0 +Problems : 95 (Average Length: 92.74 Splits: 0) +Lemmas : 810191 (Deleted: 772040) + Binary : 11690 (Ratio: 1.44%) + Ternary : 2856 (Ratio: 0.35%) + Conflict : 810191 (Average Length: 698.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 810191 (Average: 11.94 Max: 804 Sum: 9673989) + Executed : 810090 (Average: 11.94 Max: 804 Sum: 9670856 Ratio: 99.97%) + Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 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 : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 765MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 10.54s +Memory: 701MB (+0MB) +UNKNOWN +Iteration Time: 10.59s + +Iteration 95 +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 : 96 +Time : 671.564s (Solving: 645.99s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 671.704s + +Choices : 11542933 (Domain: 11402608) +Conflicts : 818906 (Analyzed: 818903) +Restarts : 9202 (Average: 88.99 Last: 184) +Model-Level : 115.0 +Problems : 96 (Average Length: 92.99 Splits: 0) +Lemmas : 818903 (Deleted: 780806) + Binary : 11741 (Ratio: 1.43%) + Ternary : 2872 (Ratio: 0.35%) + Conflict : 818903 (Average Length: 701.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 818903 (Average: 11.89 Max: 804 Sum: 9739410) + Executed : 818802 (Average: 11.89 Max: 804 Sum: 9736277 Ratio: 99.97%) + Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 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 : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 765MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.03s +Memory: 701MB (+0MB) +UNKNOWN +Iteration Time: 8.09s + +Iteration 96 +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 : 97 +Time : 678.129s (Solving: 652.42s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 678.268s + +Choices : 11604353 (Domain: 11464028) +Conflicts : 828070 (Analyzed: 828067) +Restarts : 9302 (Average: 89.02 Last: 184) +Model-Level : 115.0 +Problems : 97 (Average Length: 93.24 Splits: 0) +Lemmas : 828067 (Deleted: 789353) + Binary : 11764 (Ratio: 1.42%) + Ternary : 2873 (Ratio: 0.35%) + Conflict : 828067 (Average Length: 701.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 828067 (Average: 11.81 Max: 804 Sum: 9781652) + Executed : 827966 (Average: 11.81 Max: 804 Sum: 9778519 Ratio: 99.97%) + Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 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 : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 765MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.52s +Memory: 701MB (+0MB) +UNKNOWN +Iteration Time: 6.57s + +Iteration 97 +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 : 98 +Time : 685.727s (Solving: 659.89s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 685.868s + +Choices : 11670203 (Domain: 11529878) +Conflicts : 837340 (Analyzed: 837337) +Restarts : 9402 (Average: 89.06 Last: 184) +Model-Level : 115.0 +Problems : 98 (Average Length: 93.48 Splits: 0) +Lemmas : 837337 (Deleted: 798391) + Binary : 11790 (Ratio: 1.41%) + Ternary : 2878 (Ratio: 0.34%) + Conflict : 837337 (Average Length: 705.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 837337 (Average: 11.74 Max: 804 Sum: 9826639) + Executed : 837236 (Average: 11.73 Max: 804 Sum: 9823506 Ratio: 99.97%) + Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 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 : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 765MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.56s +Memory: 701MB (+0MB) +UNKNOWN +Iteration Time: 7.60s + +Iteration 98 +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 : 99 +Time : 693.616s (Solving: 667.62s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 693.764s + +Choices : 11743501 (Domain: 11603168) +Conflicts : 846866 (Analyzed: 846863) +Restarts : 9502 (Average: 89.12 Last: 184) +Model-Level : 115.0 +Problems : 99 (Average Length: 93.72 Splits: 0) +Lemmas : 846863 (Deleted: 807535) + Binary : 11813 (Ratio: 1.39%) + Ternary : 2879 (Ratio: 0.34%) + Conflict : 846863 (Average Length: 706.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 846863 (Average: 11.67 Max: 804 Sum: 9878846) + Executed : 846762 (Average: 11.66 Max: 804 Sum: 9875713 Ratio: 99.97%) + Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 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 : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 765MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.83s +Memory: 701MB (+0MB) +UNKNOWN +Iteration Time: 7.90s + +Iteration 99 +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 : 100 +Time : 702.056s (Solving: 675.93s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 702.208s + +Choices : 11827741 (Domain: 11687407) +Conflicts : 856967 (Analyzed: 856964) +Restarts : 9602 (Average: 89.25 Last: 184) +Model-Level : 115.0 +Problems : 100 (Average Length: 93.95 Splits: 0) +Lemmas : 856964 (Deleted: 816890) + Binary : 11828 (Ratio: 1.38%) + Ternary : 2882 (Ratio: 0.34%) + Conflict : 856964 (Average Length: 708.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 856964 (Average: 11.60 Max: 804 Sum: 9940425) + Executed : 856863 (Average: 11.60 Max: 804 Sum: 9937292 Ratio: 99.97%) + Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 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 : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 765MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.40s +Memory: 701MB (+0MB) +UNKNOWN +Iteration Time: 8.45s + +Iteration 100 +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 : 101 +Time : 710.878s (Solving: 684.61s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 711.032s + +Choices : 11924133 (Domain: 11783530) +Conflicts : 866234 (Analyzed: 866231) +Restarts : 9702 (Average: 89.28 Last: 184) +Model-Level : 115.0 +Problems : 101 (Average Length: 94.18 Splits: 0) +Lemmas : 866231 (Deleted: 826877) + Binary : 11848 (Ratio: 1.37%) + Ternary : 2889 (Ratio: 0.33%) + Conflict : 866231 (Average Length: 709.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 866231 (Average: 11.56 Max: 804 Sum: 10009326) + Executed : 866130 (Average: 11.55 Max: 804 Sum: 10006193 Ratio: 99.97%) + Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 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 : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 765MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.77s +Memory: 701MB (+0MB) +UNKNOWN +Iteration Time: 8.83s + +Iteration 101 +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 : 102 +Time : 720.063s (Solving: 693.67s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 720.220s + +Choices : 12024984 (Domain: 11884377) +Conflicts : 876018 (Analyzed: 876015) +Restarts : 9802 (Average: 89.37 Last: 184) +Model-Level : 115.0 +Problems : 102 (Average Length: 94.40 Splits: 0) +Lemmas : 876015 (Deleted: 836030) + Binary : 11857 (Ratio: 1.35%) + Ternary : 2892 (Ratio: 0.33%) + Conflict : 876015 (Average Length: 709.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 876015 (Average: 11.51 Max: 804 Sum: 10081329) + Executed : 875914 (Average: 11.50 Max: 804 Sum: 10078196 Ratio: 99.97%) + Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 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 : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 765MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.15s +Memory: 701MB (+0MB) +UNKNOWN +Iteration Time: 9.19s + +Iteration 102 +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 : 103 +Time : 729.881s (Solving: 703.35s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 730.040s + +Choices : 12380022 (Domain: 12236675) +Conflicts : 884930 (Analyzed: 884927) +Restarts : 9902 (Average: 89.37 Last: 184) +Model-Level : 115.0 +Problems : 103 (Average Length: 94.62 Splits: 0) +Lemmas : 884927 (Deleted: 845293) + Binary : 12077 (Ratio: 1.36%) + Ternary : 2911 (Ratio: 0.33%) + Conflict : 884927 (Average Length: 713.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 884927 (Average: 11.74 Max: 804 Sum: 10387706) + Executed : 884826 (Average: 11.73 Max: 804 Sum: 10384573 Ratio: 99.97%) + Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 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 : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 765MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.77s +Memory: 701MB (+0MB) +UNKNOWN +Iteration Time: 9.82s + +Iteration 103 +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 : 104 +Time : 732.460s (Solving: 705.81s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 732.620s + +Choices : 12414794 (Domain: 12271447) +Conflicts : 892338 (Analyzed: 892335) +Restarts : 10002 (Average: 89.22 Last: 184) +Model-Level : 115.0 +Problems : 104 (Average Length: 94.84 Splits: 0) +Lemmas : 892335 (Deleted: 851570) + Binary : 12115 (Ratio: 1.36%) + Ternary : 2915 (Ratio: 0.33%) + Conflict : 892335 (Average Length: 708.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 892335 (Average: 11.67 Max: 804 Sum: 10413513) + Executed : 892234 (Average: 11.67 Max: 804 Sum: 10410380 Ratio: 99.97%) + Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 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 : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 765MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 2.54s +Memory: 701MB (+0MB) +UNKNOWN +Iteration Time: 2.58s + +Iteration 104 +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 : 105 +Time : 742.371s (Solving: 715.57s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 742.536s + +Choices : 12485724 (Domain: 12342377) +Conflicts : 901675 (Analyzed: 901672) +Restarts : 10102 (Average: 89.26 Last: 184) +Model-Level : 115.0 +Problems : 105 (Average Length: 95.05 Splits: 0) +Lemmas : 901672 (Deleted: 861412) + Binary : 12151 (Ratio: 1.35%) + Ternary : 2921 (Ratio: 0.32%) + Conflict : 901672 (Average Length: 717.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 901672 (Average: 11.61 Max: 804 Sum: 10470229) + Executed : 901571 (Average: 11.61 Max: 804 Sum: 10467096 Ratio: 99.97%) + Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 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 : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 765MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.86s +Memory: 701MB (+0MB) +UNKNOWN +Iteration Time: 9.92s + +Iteration 105 +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 : 106 +Time : 751.446s (Solving: 724.50s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 751.616s + +Choices : 12572967 (Domain: 12429620) +Conflicts : 910932 (Analyzed: 910929) +Restarts : 10202 (Average: 89.29 Last: 184) +Model-Level : 115.0 +Problems : 106 (Average Length: 95.25 Splits: 0) +Lemmas : 910929 (Deleted: 871578) + Binary : 12217 (Ratio: 1.34%) + Ternary : 2928 (Ratio: 0.32%) + Conflict : 910929 (Average Length: 724.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 910929 (Average: 11.57 Max: 804 Sum: 10538307) + Executed : 910828 (Average: 11.57 Max: 804 Sum: 10535174 Ratio: 99.97%) + Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 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 : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 765MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.03s +Memory: 701MB (+0MB) +UNKNOWN +Iteration Time: 9.08s + +Iteration 106 +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 : 107 +Time : 758.286s (Solving: 731.21s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 758.460s + +Choices : 12635599 (Domain: 12492247) +Conflicts : 920355 (Analyzed: 920352) +Restarts : 10302 (Average: 89.34 Last: 184) +Model-Level : 115.0 +Problems : 107 (Average Length: 95.46 Splits: 0) +Lemmas : 920352 (Deleted: 879581) + Binary : 12233 (Ratio: 1.33%) + Ternary : 2928 (Ratio: 0.32%) + Conflict : 920352 (Average Length: 724.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 920352 (Average: 11.50 Max: 804 Sum: 10581898) + Executed : 920251 (Average: 11.49 Max: 804 Sum: 10578765 Ratio: 99.97%) + Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 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 : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 765MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.79s +Memory: 701MB (+0MB) +UNKNOWN +Iteration Time: 6.85s + +Iteration 107 +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 : 108 +Time : 765.679s (Solving: 738.45s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 765.856s + +Choices : 12704465 (Domain: 12561104) +Conflicts : 929262 (Analyzed: 929259) +Restarts : 10402 (Average: 89.33 Last: 184) +Model-Level : 115.0 +Problems : 108 (Average Length: 95.66 Splits: 0) +Lemmas : 929259 (Deleted: 888870) + Binary : 12254 (Ratio: 1.32%) + Ternary : 2936 (Ratio: 0.32%) + Conflict : 929259 (Average Length: 726.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 929259 (Average: 11.44 Max: 804 Sum: 10629083) + Executed : 929158 (Average: 11.43 Max: 804 Sum: 10625950 Ratio: 99.97%) + Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 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 : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 765MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.34s +Memory: 701MB (+0MB) +UNKNOWN +Iteration Time: 7.40s + +Iteration 108 +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 : 109 +Time : 773.496s (Solving: 746.11s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 773.676s + +Choices : 12791375 (Domain: 12647820) +Conflicts : 938134 (Analyzed: 938131) +Restarts : 10502 (Average: 89.33 Last: 184) +Model-Level : 115.0 +Problems : 109 (Average Length: 95.85 Splits: 0) +Lemmas : 938131 (Deleted: 897595) + Binary : 12348 (Ratio: 1.32%) + Ternary : 2947 (Ratio: 0.31%) + Conflict : 938131 (Average Length: 726.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 938131 (Average: 11.40 Max: 804 Sum: 10692359) + Executed : 938030 (Average: 11.39 Max: 804 Sum: 10689226 Ratio: 99.97%) + Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 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 : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 765MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.76s +Memory: 701MB (+0MB) +UNKNOWN +Iteration Time: 7.82s + +Iteration 109 +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 : 110 +Time : 781.078s (Solving: 753.54s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 781.260s + +Choices : 12865902 (Domain: 12722324) +Conflicts : 947574 (Analyzed: 947571) +Restarts : 10602 (Average: 89.38 Last: 184) +Model-Level : 115.0 +Problems : 110 (Average Length: 96.05 Splits: 0) +Lemmas : 947571 (Deleted: 906268) + Binary : 12356 (Ratio: 1.30%) + Ternary : 2949 (Ratio: 0.31%) + Conflict : 947571 (Average Length: 727.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 947571 (Average: 11.34 Max: 804 Sum: 10742954) + Executed : 947470 (Average: 11.33 Max: 804 Sum: 10739821 Ratio: 99.97%) + Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 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 : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 765MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.53s +Memory: 701MB (+0MB) +UNKNOWN +Iteration Time: 7.59s + +Iteration 110 +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 : 111 +Time : 788.621s (Solving: 760.96s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 788.804s + +Choices : 12943246 (Domain: 12799668) +Conflicts : 956305 (Analyzed: 956302) +Restarts : 10702 (Average: 89.36 Last: 184) +Model-Level : 115.0 +Problems : 111 (Average Length: 96.23 Splits: 0) +Lemmas : 956302 (Deleted: 915504) + Binary : 12373 (Ratio: 1.29%) + Ternary : 2955 (Ratio: 0.31%) + Conflict : 956302 (Average Length: 729.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 956302 (Average: 11.28 Max: 804 Sum: 10789739) + Executed : 956201 (Average: 11.28 Max: 804 Sum: 10786606 Ratio: 99.97%) + Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 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 : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 765MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.51s +Memory: 701MB (+0MB) +UNKNOWN +Iteration Time: 7.55s + +Iteration 111 +Queue: [(22,110,2,True), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 112 +Time : 798.694s (Solving: 770.88s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 798.880s + +Choices : 13040307 (Domain: 12896729) +Conflicts : 966555 (Analyzed: 966552) +Restarts : 10802 (Average: 89.48 Last: 184) +Model-Level : 115.0 +Problems : 112 (Average Length: 96.42 Splits: 0) +Lemmas : 966552 (Deleted: 924115) + Binary : 12395 (Ratio: 1.28%) + Ternary : 2957 (Ratio: 0.31%) + Conflict : 966552 (Average Length: 731.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 966552 (Average: 11.23 Max: 804 Sum: 10854853) + Executed : 966451 (Average: 11.23 Max: 804 Sum: 10851720 Ratio: 99.97%) + Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 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 : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 765MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 10.02s +Memory: 701MB (+0MB) +UNKNOWN +Iteration Time: 10.08s + +Iteration 112 +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 : 113 +Time : 802.753s (Solving: 774.81s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 802.940s + +Choices : 13111674 (Domain: 12968096) +Conflicts : 974599 (Analyzed: 974596) +Restarts : 10902 (Average: 89.40 Last: 184) +Model-Level : 115.0 +Problems : 113 (Average Length: 96.60 Splits: 0) +Lemmas : 974596 (Deleted: 931881) + Binary : 12454 (Ratio: 1.28%) + Ternary : 2975 (Ratio: 0.31%) + Conflict : 974596 (Average Length: 728.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 974596 (Average: 11.21 Max: 804 Sum: 10920351) + Executed : 974495 (Average: 11.20 Max: 804 Sum: 10917218 Ratio: 99.97%) + Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 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 : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 765MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 4.02s +Memory: 701MB (+0MB) +UNKNOWN +Iteration Time: 4.06s + +Iteration 113 +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 : 114 +Time : 812.869s (Solving: 784.81s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 813.064s + +Choices : 13185537 (Domain: 13041959) +Conflicts : 983518 (Analyzed: 983515) +Restarts : 11002 (Average: 89.39 Last: 184) +Model-Level : 115.0 +Problems : 114 (Average Length: 96.78 Splits: 0) +Lemmas : 983515 (Deleted: 941911) + Binary : 12505 (Ratio: 1.27%) + Ternary : 2986 (Ratio: 0.30%) + Conflict : 983515 (Average Length: 737.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 983515 (Average: 11.16 Max: 804 Sum: 10979427) + Executed : 983414 (Average: 11.16 Max: 804 Sum: 10976294 Ratio: 99.97%) + Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 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 : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 765MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 10.08s +Memory: 701MB (+0MB) +UNKNOWN +Iteration Time: 10.12s + +Iteration 114 +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 : 115 +Time : 820.835s (Solving: 792.64s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 821.036s + +Choices : 13255710 (Domain: 13112132) +Conflicts : 992455 (Analyzed: 992452) +Restarts : 11102 (Average: 89.39 Last: 184) +Model-Level : 115.0 +Problems : 115 (Average Length: 96.96 Splits: 0) +Lemmas : 992452 (Deleted: 950714) + Binary : 12552 (Ratio: 1.26%) + Ternary : 3001 (Ratio: 0.30%) + Conflict : 992452 (Average Length: 740.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 992452 (Average: 11.12 Max: 804 Sum: 11032012) + Executed : 992351 (Average: 11.11 Max: 804 Sum: 11028879 Ratio: 99.97%) + Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 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 : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 765MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.92s +Memory: 701MB (+0MB) +UNKNOWN +Iteration Time: 7.97s + +Iteration 115 +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 : 116 +Time : 827.584s (Solving: 799.26s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 827.788s + +Choices : 13320597 (Domain: 13177016) +Conflicts : 1001486 (Analyzed: 1001483) +Restarts : 11202 (Average: 89.40 Last: 184) +Model-Level : 115.0 +Problems : 116 (Average Length: 97.13 Splits: 0) +Lemmas : 1001483 (Deleted: 959507) + Binary : 12570 (Ratio: 1.26%) + Ternary : 3008 (Ratio: 0.30%) + Conflict : 1001483 (Average Length: 740.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 1001483 (Average: 11.06 Max: 804 Sum: 11079040) + Executed : 1001382 (Average: 11.06 Max: 804 Sum: 11075907 Ratio: 99.97%) + Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 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 : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 765MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.71s +Memory: 701MB (+0MB) +UNKNOWN +Iteration Time: 6.75s + +Iteration 116 +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... +[start: stats after solve call] + +Models : 0+ +Calls : 117 +Time : 836.118s (Solving: 807.67s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 836.324s + +Choices : 13400827 (Domain: 13257219) +Conflicts : 1011715 (Analyzed: 1011712) +Restarts : 11302 (Average: 89.52 Last: 184) +Model-Level : 115.0 +Problems : 117 (Average Length: 97.30 Splits: 0) +Lemmas : 1011712 (Deleted: 968327) + Binary : 12615 (Ratio: 1.25%) + Ternary : 3012 (Ratio: 0.30%) + Conflict : 1011712 (Average Length: 742.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 1011712 (Average: 11.01 Max: 804 Sum: 11136699) + Executed : 1011611 (Average: 11.00 Max: 804 Sum: 11133566 Ratio: 99.97%) + Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 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 : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 765MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.49s +Memory: 701MB (+0MB) +UNKNOWN +Iteration Time: 8.54s + +Iteration 117 +Queue: [(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 : 118 +Time : 843.607s (Solving: 815.01s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 843.812s + +Choices : 13473329 (Domain: 13329698) +Conflicts : 1020876 (Analyzed: 1020873) +Restarts : 11402 (Average: 89.53 Last: 184) +Model-Level : 115.0 +Problems : 118 (Average Length: 97.47 Splits: 0) +Lemmas : 1020873 (Deleted: 978408) + Binary : 12634 (Ratio: 1.24%) + Ternary : 3018 (Ratio: 0.30%) + Conflict : 1020873 (Average Length: 744.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 1020873 (Average: 10.96 Max: 804 Sum: 11186313) + Executed : 1020772 (Average: 10.95 Max: 804 Sum: 11183180 Ratio: 99.97%) + Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 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 : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 765MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.44s +Memory: 701MB (+0MB) +UNKNOWN +Iteration Time: 7.49s + +Iteration 118 +Queue: [(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 : 119 +Time : 851.708s (Solving: 822.96s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 851.916s + +Choices : 13557863 (Domain: 13414212) +Conflicts : 1030146 (Analyzed: 1030143) +Restarts : 11502 (Average: 89.56 Last: 184) +Model-Level : 115.0 +Problems : 119 (Average Length: 97.63 Splits: 0) +Lemmas : 1030143 (Deleted: 987414) + Binary : 12652 (Ratio: 1.23%) + Ternary : 3032 (Ratio: 0.29%) + Conflict : 1030143 (Average Length: 745.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 1030143 (Average: 10.92 Max: 804 Sum: 11244412) + Executed : 1030042 (Average: 10.91 Max: 804 Sum: 11241279 Ratio: 99.97%) + Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 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 : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 765MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.05s +Memory: 701MB (+0MB) +UNKNOWN +Iteration Time: 8.11s + +Iteration 119 +Queue: [(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 : 120 +Time : 860.236s (Solving: 831.34s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 860.448s + +Choices : 13712973 (Domain: 13568567) +Conflicts : 1039314 (Analyzed: 1039311) +Restarts : 11602 (Average: 89.58 Last: 184) +Model-Level : 115.0 +Problems : 120 (Average Length: 97.79 Splits: 0) +Lemmas : 1039311 (Deleted: 996426) + Binary : 12746 (Ratio: 1.23%) + Ternary : 3043 (Ratio: 0.29%) + Conflict : 1039311 (Average Length: 746.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 1039311 (Average: 10.94 Max: 804 Sum: 11366683) + Executed : 1039210 (Average: 10.93 Max: 804 Sum: 11363550 Ratio: 99.97%) + Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 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 : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 765MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.47s +Memory: 701MB (+0MB) +UNKNOWN +Iteration Time: 8.53s + +Iteration 120 +Queue: [(4,20,11,True), (5,25,11,True), (6,30,10,True), (7,35,9,True), (8,40,8,True), (9,45,7,True), (10,50,7,False), (11,55,6,True), (12,60,6,False), (13,65,5,True), (14,70,5,False), (15,75,4,True), (16,80,4,False), (17,85,4,False), (18,90,4,False), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,2,True)] +Grounded Until: 115 +Blocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 121 +Time : 862.239s (Solving: 833.19s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 862.452s + +Choices : 13745614 (Domain: 13601208) +Conflicts : 1046538 (Analyzed: 1046535) +Restarts : 11702 (Average: 89.43 Last: 184) +Model-Level : 115.0 +Problems : 121 (Average Length: 97.95 Splits: 0) +Lemmas : 1046535 (Deleted: 1002872) + Binary : 12779 (Ratio: 1.22%) + Ternary : 3048 (Ratio: 0.29%) + Conflict : 1046535 (Average Length: 741.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 1046535 (Average: 10.88 Max: 804 Sum: 11389452) + Executed : 1046434 (Average: 10.88 Max: 804 Sum: 11386319 Ratio: 99.97%) + Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 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 : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 765MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 1.95s +Memory: 701MB (+0MB) +UNKNOWN +Iteration Time: 2.01s + +Iteration 121 +Queue: [(5,25,11,True), (6,30,10,True), (7,35,9,True), (8,40,8,True), (9,45,7,True), (10,50,7,False), (11,55,6,True), (12,60,6,False), (13,65,5,True), (14,70,5,False), (15,75,4,True), (16,80,4,False), (17,85,4,False), (18,90,4,False), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,2,True)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 122 +Time : 870.750s (Solving: 841.55s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 870.968s + +Choices : 13808870 (Domain: 13664464) +Conflicts : 1054704 (Analyzed: 1054701) +Restarts : 11802 (Average: 89.37 Last: 184) +Model-Level : 115.0 +Problems : 122 (Average Length: 98.11 Splits: 0) +Lemmas : 1054701 (Deleted: 1010599) + Binary : 12848 (Ratio: 1.22%) + Ternary : 3058 (Ratio: 0.29%) + Conflict : 1054701 (Average Length: 751.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 1054701 (Average: 10.84 Max: 804 Sum: 11436954) + Executed : 1054600 (Average: 10.84 Max: 804 Sum: 11433821 Ratio: 99.97%) + Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 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 : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 765MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.46s +Memory: 701MB (+0MB) +UNKNOWN +Iteration Time: 8.52s + +Iteration 122 +Queue: [(6,30,10,True), (7,35,9,True), (8,40,8,True), (9,45,7,True), (10,50,7,False), (11,55,6,True), (12,60,6,False), (13,65,5,True), (14,70,5,False), (15,75,4,True), (16,80,4,False), (17,85,4,False), (18,90,4,False), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,2,True)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 123 +Time : 879.378s (Solving: 850.03s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 879.600s + +Choices : 13884685 (Domain: 13740279) +Conflicts : 1063387 (Analyzed: 1063384) +Restarts : 11902 (Average: 89.34 Last: 184) +Model-Level : 115.0 +Problems : 123 (Average Length: 98.26 Splits: 0) +Lemmas : 1063384 (Deleted: 1020841) + Binary : 12891 (Ratio: 1.21%) + Ternary : 3083 (Ratio: 0.29%) + Conflict : 1063384 (Average Length: 757.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 1063384 (Average: 10.81 Max: 804 Sum: 11494856) + Executed : 1063283 (Average: 10.81 Max: 804 Sum: 11491723 Ratio: 99.97%) + Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 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 : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 765MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.57s +Memory: 701MB (+0MB) +UNKNOWN +Iteration Time: 8.63s + +Iteration 123 +Queue: [(7,35,9,True), (8,40,8,True), (9,45,7,True), (10,50,7,False), (11,55,6,True), (12,60,6,False), (13,65,5,True), (14,70,5,False), (15,75,4,True), (16,80,4,False), (17,85,4,False), (18,90,4,False), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,2,True)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 124 +Time : 885.866s (Solving: 856.36s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 886.092s + +Choices : 13950526 (Domain: 13806057) +Conflicts : 1072375 (Analyzed: 1072372) +Restarts : 12002 (Average: 89.35 Last: 184) +Model-Level : 115.0 +Problems : 124 (Average Length: 98.41 Splits: 0) +Lemmas : 1072372 (Deleted: 1029078) + Binary : 12910 (Ratio: 1.20%) + Ternary : 3093 (Ratio: 0.29%) + Conflict : 1072372 (Average Length: 757.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 1072372 (Average: 10.76 Max: 804 Sum: 11541621) + Executed : 1072271 (Average: 10.76 Max: 804 Sum: 11538488 Ratio: 99.97%) + Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 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 : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 765MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.43s +Memory: 701MB (+0MB) +UNKNOWN +Iteration Time: 6.49s + +Iteration 124 +Queue: [(8,40,8,True), (9,45,7,True), (10,50,7,False), (11,55,6,True), (12,60,6,False), (13,65,5,True), (14,70,5,False), (15,75,4,True), (16,80,4,False), (17,85,4,False), (18,90,4,False), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,2,True)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 125 +Time : 894.113s (Solving: 864.48s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 894.344s + +Choices : 14023841 (Domain: 13879370) +Conflicts : 1081352 (Analyzed: 1081349) +Restarts : 12102 (Average: 89.35 Last: 184) +Model-Level : 115.0 +Problems : 125 (Average Length: 98.56 Splits: 0) +Lemmas : 1081349 (Deleted: 1037874) + Binary : 12991 (Ratio: 1.20%) + Ternary : 3108 (Ratio: 0.29%) + Conflict : 1081349 (Average Length: 760.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 1081349 (Average: 10.72 Max: 804 Sum: 11595129) + Executed : 1081248 (Average: 10.72 Max: 804 Sum: 11591996 Ratio: 99.97%) + Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 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 : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 765MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.21s +Memory: 701MB (+0MB) +UNKNOWN +Iteration Time: 8.25s + +Iteration 125 +Queue: [(9,45,7,True), (10,50,7,False), (11,55,6,True), (12,60,6,False), (13,65,5,True), (14,70,5,False), (15,75,4,True), (16,80,4,False), (17,85,4,False), (18,90,4,False), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,2,True)] +Grounded Until: 115 +Unblocking actions... +Solving... +*** Info : (planner): INTERRUPTED by signal! +UNKNOWN + +INTERRUPTED : 1 + +Models : 0+ +Calls : 126 +Time : 894.335s (Solving: 864.58s 1st Model: 0.00s Unsat: 3.47s) +CPU Time : 894.544s + +Choices : 14024340 (Domain: 13879869) +Conflicts : 1081471 (Analyzed: 1081468) +Restarts : 12103 (Average: 89.36 Last: 184) +Model-Level : 115.0 +Problems : 126 (Average Length: 98.71 Splits: 0) +Lemmas : 1081468 (Deleted: 1037874) + Binary : 12991 (Ratio: 1.20%) + Ternary : 3108 (Ratio: 0.29%) + Conflict : 1081468 (Average Length: 760.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 1081468 (Average: 10.72 Max: 804 Sum: 11595494) + Executed : 1081367 (Average: 10.72 Max: 804 Sum: 11592361 Ratio: 99.97%) + Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 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 : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 765MB +Max. Length : 115 steps +Models : 1 + +