diff --git a/gc-ta1-tt1/ipc-2011_barman-sequential-satisficing_10.env b/gc-ta1-tt1/ipc-2011_barman-sequential-satisficing_10.env new file mode 100644 index 000000000..a467ff8b9 --- /dev/null +++ b/gc-ta1-tt1/ipc-2011_barman-sequential-satisficing_10.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-10.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: 10 + 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_10.err b/gc-ta1-tt1/ipc-2011_barman-sequential-satisficing_10.err new file mode 100644 index 000000000..6dca9465c --- /dev/null +++ b/gc-ta1-tt1/ipc-2011_barman-sequential-satisficing_10.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': 10} +# 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-10.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.04 MEM 915784 MAXMEM 1004492 STALE 0 MAXMEM_RSS 867224 + + diff --git a/gc-ta1-tt1/ipc-2011_barman-sequential-satisficing_10.out b/gc-ta1-tt1/ipc-2011_barman-sequential-satisficing_10.out new file mode 100644 index 000000000..2d18656c0 --- /dev/null +++ b/gc-ta1-tt1/ipc-2011_barman-sequential-satisficing_10.out @@ -0,0 +1,5445 @@ +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-10.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-10.pddl +Parsing... +Parsing: [0.030s CPU, 0.035s wall-clock] +Normalizing task... [0.000s CPU, 0.003s wall-clock] +Instantiating... +Generating Datalog program... [0.010s CPU, 0.009s wall-clock] +Normalizing Datalog program... +Normalizing Datalog program: [0.040s CPU, 0.044s wall-clock] +Preparing model... [0.030s CPU, 0.025s wall-clock] +Generated 115 rules. +Computing model... [0.450s CPU, 0.450s wall-clock] +2784 relevant atoms +2893 auxiliary atoms +5677 final queue length +9793 total queue pushes +Completing instantiation... [0.870s CPU, 0.867s wall-clock] +Instantiating: [1.400s CPU, 1.401s wall-clock] +Computing fact groups... +Finding invariants... +24 initial candidates +Finding invariants: [0.130s CPU, 0.131s wall-clock] +Checking invariant weight... [0.010s CPU, 0.001s wall-clock] +Instantiating groups... [0.000s CPU, 0.008s wall-clock] +Collecting mutex groups... [0.000s CPU, 0.001s wall-clock] +Choosing groups... +292 uncovered facts +Choosing groups: [0.010s CPU, 0.002s wall-clock] +Building translation key... [0.010s CPU, 0.011s wall-clock] +Computing fact groups: [0.180s CPU, 0.176s wall-clock] +Building STRIPS to SAS dictionary... [0.000s CPU, 0.003s wall-clock] +Building dictionary for full mutex groups... [0.010s CPU, 0.006s wall-clock] +Building mutex information... +Building mutex information: [0.000s CPU, 0.003s wall-clock] +Translating task... +Processing axioms... +Simplifying axioms... [0.000s CPU, 0.000s wall-clock] +Processing axioms: [0.050s CPU, 0.047s wall-clock] +Translating task: [0.890s CPU, 0.890s wall-clock] +3276 effect conditions simplified +0 implied preconditions added +Detecting unreachable propositions... +0 operators removed +0 axioms removed +3 propositions removed +Detecting unreachable propositions: [0.440s CPU, 0.437s wall-clock] +Reordering and filtering variables... +295 of 295 variables necessary. +14 of 17 mutex groups necessary. +1958 of 1958 operators necessary. +0 of 0 axiom rules necessary. +Reordering and filtering variables: [0.300s CPU, 0.304s wall-clock] +Translator variables: 295 +Translator derived variables: 0 +Translator facts: 617 +Translator goal facts: 12 +Translator mutex groups: 14 +Translator total mutex groups size: 42 +Translator operators: 1958 +Translator axioms: 0 +Translator task size: 18764 +Translator peak memory: 47052 KB +Writing output... [0.310s CPU, 0.342s wall-clock] +Done! [3.600s CPU, 3.635s wall-clock] +planner.py version 0.0.1 + +Time: 0.76s +Memory: 101MB + +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.910s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s) +CPU Time : 0.764s + +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 : 54149 +Atoms : 54149 +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 : 237MB +Max. Length : 0 steps +Models : 0 + +[endof: stats after solve call] +Solving Time: 0.01s +Memory: 173MB (+72MB) +UNSAT +Iteration Time: 0.01s + +Iteration 2 +Queue: [(1,5,0,True), (2,10,0,True), (3,15,0,True), (4,20,0,True), (5,25,0,True), (6,30,0,True)] +Grounded Until: 0 +Expected Memory: 173MB +Grounding... [('step', [1]), ('step', [2]), ('step', [3]), ('step', [4]), ('step', [5]), ('check', [5])] +Grounding Time: 0.23s +Memory: 173MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 1+ +Calls : 2 +Time : 1.263s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s) +CPU Time : 1.116s + +Choices : 158 (Domain: 32) +Conflicts : 4 (Analyzed: 4) +Restarts : 0 +Model-Level : 148.0 +Problems : 2 (Average Length: 4.50 Splits: 0) +Lemmas : 4 (Deleted: 0) + Binary : 2 (Ratio: 50.00%) + Ternary : 0 (Ratio: 0.00%) + Conflict : 4 (Average Length: 15.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 4 (Average: 4.50 Max: 14 Sum: 18) + Executed : 3 (Average: 4.25 Max: 14 Sum: 17 Ratio: 94.44%) + Bounded : 1 (Average: 1.00 Max: 1 Sum: 1 Ratio: 5.56%) + +Rules : 54149 +Atoms : 54149 +Bodies : 1 (Original: 0) +Tight : Yes +Variables : 14506 (Eliminated: 0 Frozen: 150) +Constraints : 48947 (Binary: 95.2% Ternary: 3.3% Other: 1.4%) + +Memory Peak : 237MB +Max. Length : 0 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 0.02s +Memory: 176MB (+3MB) +SAT +Testing... +NOT SERIALIZABLE +Testing Time: 0.76s +Memory: 203MB (+27MB) +Solving... +[start: stats after solve call] + +Models : 0 +Calls : 3 +Time : 1.387s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s) +CPU Time : 1.244s + +Choices : 176 (Domain: 33) +Conflicts : 13 (Analyzed: 12) +Restarts : 0 +Model-Level : 148.0 +Problems : 3 (Average Length: 5.33 Splits: 0) +Lemmas : 12 (Deleted: 0) + Binary : 4 (Ratio: 33.33%) + Ternary : 4 (Ratio: 33.33%) + Conflict : 12 (Average Length: 7.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 12 (Average: 3.17 Max: 14 Sum: 38) + Executed : 9 (Average: 2.92 Max: 14 Sum: 35 Ratio: 92.11%) + Bounded : 3 (Average: 1.00 Max: 1 Sum: 3 Ratio: 7.89%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 17794 (Eliminated: 0 Frozen: 3815) +Constraints : 73341 (Binary: 92.3% Ternary: 5.4% Other: 2.2%) + +Memory Peak : 237MB +Max. Length : 0 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 0.02s +Memory: 203MB (+0MB) +UNSAT +Iteration Time: 1.14s + +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: 206.0MB +Grounding... [('step', [6]), ('step', [7]), ('step', [8]), ('step', [9]), ('step', [10]), ('check', [10])] +Grounding Time: 0.46s +Memory: 203MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0 +Calls : 4 +Time : 2.723s (Solving: 0.69s 1st Model: 0.00s Unsat: 0.69s) +CPU Time : 2.580s + +Choices : 14860 (Domain: 14099) +Conflicts : 2048 (Analyzed: 2046) +Restarts : 22 (Average: 93.00 Last: 11) +Model-Level : 148.0 +Problems : 4 (Average Length: 7.00 Splits: 0) +Lemmas : 2046 (Deleted: 625) + Binary : 226 (Ratio: 11.05%) + Ternary : 305 (Ratio: 14.91%) + Conflict : 2046 (Average Length: 21.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 2046 (Average: 7.27 Max: 66 Sum: 14884) + Executed : 2016 (Average: 7.13 Max: 66 Sum: 14590 Ratio: 98.02%) + Bounded : 30 (Average: 9.80 Max: 12 Sum: 294 Ratio: 1.98%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 50740 (Eliminated: 0 Frozen: 14250) +Constraints : 322926 (Binary: 91.5% Ternary: 6.6% Other: 1.9%) + +Memory Peak : 237MB +Max. Length : 5 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 0.71s +Memory: 213MB (+10MB) +UNSAT +Iteration Time: 1.34s + +Iteration 4 +Queue: [(3,15,0,True), (4,20,0,True), (5,25,0,True), (6,30,0,True)] +Grounded Until: 10 +Expected Memory: 223.0MB +Grounding... [('step', [11]), ('step', [12]), ('step', [13]), ('step', [14]), ('step', [15]), ('check', [15])] +Grounding Time: 0.43s +Memory: 223MB (+10MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 5 +Time : 7.300s (Solving: 4.63s 1st Model: 0.00s Unsat: 0.69s) +CPU Time : 7.160s + +Choices : 78060 (Domain: 68959) +Conflicts : 10619 (Analyzed: 10617) +Restarts : 122 (Average: 87.02 Last: 78) +Model-Level : 148.0 +Problems : 5 (Average Length: 9.00 Splits: 0) +Lemmas : 10617 (Deleted: 4869) + Binary : 643 (Ratio: 6.06%) + Ternary : 500 (Ratio: 4.71%) + Conflict : 10617 (Average Length: 235.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 10617 (Average: 7.08 Max: 149 Sum: 75198) + Executed : 10576 (Average: 7.04 Max: 149 Sum: 74721 Ratio: 99.37%) + Bounded : 41 (Average: 11.63 Max: 17 Sum: 477 Ratio: 0.63%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 83686 (Eliminated: 0 Frozen: 24685) +Constraints : 554156 (Binary: 91.5% Ternary: 6.6% Other: 1.9%) + +Memory Peak : 239MB +Max. Length : 10 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 3.97s +Memory: 239MB (+16MB) +UNKNOWN +Iteration Time: 4.59s + +Iteration 5 +Queue: [(4,20,0,True), (5,25,0,True), (6,30,0,True)] +Grounded Until: 15 +Expected Memory: 265.0MB +Grounding... [('step', [16]), ('step', [17]), ('step', [18]), ('step', [19]), ('step', [20]), ('check', [20])] +Grounding Time: 0.48s +Memory: 247MB (+8MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 6 +Time : 12.209s (Solving: 8.81s 1st Model: 0.00s Unsat: 0.69s) +CPU Time : 12.072s + +Choices : 170091 (Domain: 148240) +Conflicts : 19840 (Analyzed: 19838) +Restarts : 222 (Average: 89.36 Last: 104) +Model-Level : 148.0 +Problems : 6 (Average Length: 11.17 Splits: 0) +Lemmas : 19838 (Deleted: 14254) + Binary : 1032 (Ratio: 5.20%) + Ternary : 614 (Ratio: 3.10%) + Conflict : 19838 (Average Length: 256.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 19838 (Average: 8.14 Max: 277 Sum: 161445) + Executed : 19776 (Average: 8.09 Max: 277 Sum: 160511 Ratio: 99.42%) + Bounded : 62 (Average: 15.06 Max: 22 Sum: 934 Ratio: 0.58%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 116632 (Eliminated: 0 Frozen: 35120) +Constraints : 795856 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 265MB +Max. Length : 15 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 4.23s +Memory: 265MB (+18MB) +UNKNOWN +Iteration Time: 4.92s + +Iteration 6 +Queue: [(5,25,0,True), (6,30,0,True)] +Grounded Until: 20 +Expected Memory: 291.0MB +Grounding... [('step', [21]), ('step', [22]), ('step', [23]), ('step', [24]), ('step', [25]), ('check', [25])] +Grounding Time: 0.54s +Memory: 278MB (+13MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 7 +Time : 18.329s (Solving: 14.13s 1st Model: 0.00s Unsat: 0.69s) +CPU Time : 18.196s + +Choices : 311716 (Domain: 276263) +Conflicts : 28786 (Analyzed: 28784) +Restarts : 322 (Average: 89.39 Last: 104) +Model-Level : 148.0 +Problems : 7 (Average Length: 13.43 Splits: 0) +Lemmas : 28784 (Deleted: 21060) + Binary : 1876 (Ratio: 6.52%) + Ternary : 957 (Ratio: 3.32%) + Conflict : 28784 (Average Length: 297.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 28784 (Average: 10.18 Max: 376 Sum: 292956) + Executed : 28710 (Average: 10.13 Max: 376 Sum: 291700 Ratio: 99.57%) + Bounded : 74 (Average: 16.97 Max: 27 Sum: 1256 Ratio: 0.43%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 149578 (Eliminated: 0 Frozen: 45555) +Constraints : 1034643 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 301MB +Max. Length : 20 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 5.37s +Memory: 289MB (+11MB) +UNKNOWN +Iteration Time: 6.14s + +Iteration 7 +Queue: [(6,30,0,True)] +Grounded Until: 25 +Expected Memory: 315.0MB +Grounding... [('step', [26]), ('step', [27]), ('step', [28]), ('step', [29]), ('step', [30]), ('check', [30])] +Grounding Time: 0.65s +Memory: 300MB (+11MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 8 +Time : 27.454s (Solving: 22.22s 1st Model: 0.00s Unsat: 0.69s) +CPU Time : 27.324s + +Choices : 435256 (Domain: 387472) +Conflicts : 38279 (Analyzed: 38277) +Restarts : 422 (Average: 90.70 Last: 111) +Model-Level : 148.0 +Problems : 8 (Average Length: 15.75 Splits: 0) +Lemmas : 38277 (Deleted: 28680) + Binary : 2260 (Ratio: 5.90%) + Ternary : 1145 (Ratio: 2.99%) + Conflict : 38277 (Average Length: 322.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 38277 (Average: 10.64 Max: 509 Sum: 407200) + Executed : 38198 (Average: 10.60 Max: 509 Sum: 405785 Ratio: 99.65%) + Bounded : 79 (Average: 17.91 Max: 32 Sum: 1415 Ratio: 0.35%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 182524 (Eliminated: 0 Frozen: 55990) +Constraints : 1263687 (Binary: 91.4% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 326MB +Max. Length : 25 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.16s +Memory: 324MB (+24MB) +UNKNOWN +Iteration Time: 9.14s + +Iteration 8 +Queue: [(3,15,1,True), (4,20,1,True), (5,25,1,True), (6,30,1,True), (7,35,0,True), (8,40,0,True), (9,45,0,True), (10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True)] +Grounded Until: 30 +Blocking actions... +Solving... +[start: stats after solve call] + +Models : 0 +Calls : 9 +Time : 29.090s (Solving: 23.82s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 28.960s + +Choices : 444161 (Domain: 394803) +Conflicts : 40170 (Analyzed: 40167) +Restarts : 443 (Average: 90.67 Last: 111) +Model-Level : 148.0 +Problems : 9 (Average Length: 17.56 Splits: 0) +Lemmas : 40167 (Deleted: 28680) + Binary : 2339 (Ratio: 5.82%) + Ternary : 1176 (Ratio: 2.93%) + Conflict : 40167 (Average Length: 317.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 40167 (Average: 10.35 Max: 509 Sum: 415921) + Executed : 40087 (Average: 10.32 Max: 509 Sum: 414505 Ratio: 99.66%) + Bounded : 80 (Average: 17.70 Max: 32 Sum: 1416 Ratio: 0.34%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 182524 (Eliminated: 0 Frozen: 55990) +Constraints : 1263631 (Binary: 91.4% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 326MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 1.62s +Memory: 324MB (+0MB) +UNSAT +Iteration Time: 1.64s + +Iteration 9 +Queue: [(4,20,1,True), (5,25,1,True), (6,30,1,True), (7,35,0,True), (8,40,0,True), (9,45,0,True), (10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True)] +Grounded Until: 30 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 10 +Time : 36.964s (Solving: 31.64s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 36.836s + +Choices : 493744 (Domain: 435637) +Conflicts : 48914 (Analyzed: 48911) +Restarts : 543 (Average: 90.08 Last: 111) +Model-Level : 148.0 +Problems : 10 (Average Length: 19.00 Splits: 0) +Lemmas : 48911 (Deleted: 38023) + Binary : 2522 (Ratio: 5.16%) + Ternary : 1328 (Ratio: 2.72%) + Conflict : 48911 (Average Length: 422.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 48911 (Average: 9.43 Max: 509 Sum: 461331) + Executed : 48830 (Average: 9.40 Max: 509 Sum: 459883 Ratio: 99.69%) + Bounded : 81 (Average: 17.88 Max: 32 Sum: 1448 Ratio: 0.31%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 182524 (Eliminated: 0 Frozen: 55990) +Constraints : 1263631 (Binary: 91.4% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 326MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.86s +Memory: 324MB (+0MB) +UNKNOWN +Iteration Time: 7.88s + +Iteration 10 +Queue: [(5,25,1,True), (6,30,1,True), (7,35,0,True), (8,40,0,True), (9,45,0,True), (10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True)] +Grounded Until: 30 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 11 +Time : 43.964s (Solving: 38.60s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 43.836s + +Choices : 572132 (Domain: 505239) +Conflicts : 57534 (Analyzed: 57531) +Restarts : 643 (Average: 89.47 Last: 111) +Model-Level : 148.0 +Problems : 11 (Average Length: 20.18 Splits: 0) +Lemmas : 57531 (Deleted: 45329) + Binary : 2890 (Ratio: 5.02%) + Ternary : 1461 (Ratio: 2.54%) + Conflict : 57531 (Average Length: 436.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 57531 (Average: 9.27 Max: 509 Sum: 533081) + Executed : 57445 (Average: 9.24 Max: 509 Sum: 531473 Ratio: 99.70%) + Bounded : 86 (Average: 18.70 Max: 32 Sum: 1608 Ratio: 0.30%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 182524 (Eliminated: 0 Frozen: 55990) +Constraints : 1263617 (Binary: 91.4% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 326MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.99s +Memory: 324MB (+0MB) +UNKNOWN +Iteration Time: 7.00s + +Iteration 11 +Queue: [(6,30,1,True), (7,35,0,True), (8,40,0,True), (9,45,0,True), (10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True)] +Grounded Until: 30 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 12 +Time : 49.704s (Solving: 44.30s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 49.580s + +Choices : 651504 (Domain: 575594) +Conflicts : 65352 (Analyzed: 65349) +Restarts : 743 (Average: 87.95 Last: 111) +Model-Level : 148.0 +Problems : 12 (Average Length: 21.17 Splits: 0) +Lemmas : 65349 (Deleted: 51225) + Binary : 3148 (Ratio: 4.82%) + Ternary : 1555 (Ratio: 2.38%) + Conflict : 65349 (Average Length: 437.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 65349 (Average: 9.22 Max: 509 Sum: 602562) + Executed : 65260 (Average: 9.19 Max: 509 Sum: 600858 Ratio: 99.72%) + Bounded : 89 (Average: 19.15 Max: 32 Sum: 1704 Ratio: 0.28%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 182524 (Eliminated: 0 Frozen: 55990) +Constraints : 1263547 (Binary: 91.4% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 326MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 5.73s +Memory: 324MB (+0MB) +UNKNOWN +Iteration Time: 5.75s + +Iteration 12 +Queue: [(7,35,0,True), (8,40,0,True), (9,45,0,True), (10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True)] +Grounded Until: 30 +Expected Memory: 359.0MB +Grounding... [('step', [31]), ('step', [32]), ('step', [33]), ('step', [34]), ('step', [35]), ('check', [35])] +Grounding Time: 0.48s +Memory: 327MB (+3MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 13 +Time : 56.267s (Solving: 50.08s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 56.144s + +Choices : 735656 (Domain: 654916) +Conflicts : 73377 (Analyzed: 73374) +Restarts : 843 (Average: 87.04 Last: 111) +Model-Level : 148.0 +Problems : 13 (Average Length: 22.38 Splits: 0) +Lemmas : 73374 (Deleted: 57875) + Binary : 3467 (Ratio: 4.73%) + Ternary : 1760 (Ratio: 2.40%) + Conflict : 73374 (Average Length: 448.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 73374 (Average: 9.21 Max: 509 Sum: 676140) + Executed : 73283 (Average: 9.19 Max: 509 Sum: 674362 Ratio: 99.74%) + Bounded : 91 (Average: 19.54 Max: 37 Sum: 1778 Ratio: 0.26%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 215470 (Eliminated: 0 Frozen: 66425) +Constraints : 1513090 (Binary: 91.4% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 360MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 5.84s +Memory: 341MB (+14MB) +UNKNOWN +Iteration Time: 6.58s + +Iteration 13 +Queue: [(8,40,0,True), (9,45,0,True), (10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True)] +Grounded Until: 35 +Expected Memory: 376.0MB +Grounding... [('step', [36]), ('step', [37]), ('step', [38]), ('step', [39]), ('step', [40]), ('check', [40])] +Grounding Time: 0.48s +Memory: 348MB (+7MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 14 +Time : 63.027s (Solving: 56.03s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 62.908s + +Choices : 789742 (Domain: 708818) +Conflicts : 81495 (Analyzed: 81492) +Restarts : 943 (Average: 86.42 Last: 111) +Model-Level : 148.0 +Problems : 14 (Average Length: 23.79 Splits: 0) +Lemmas : 81492 (Deleted: 65195) + Binary : 3580 (Ratio: 4.39%) + Ternary : 1786 (Ratio: 2.19%) + Conflict : 81492 (Average Length: 432.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 81492 (Average: 8.87 Max: 517 Sum: 722840) + Executed : 81401 (Average: 8.85 Max: 517 Sum: 721062 Ratio: 99.75%) + Bounded : 91 (Average: 19.54 Max: 37 Sum: 1778 Ratio: 0.25%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 248416 (Eliminated: 0 Frozen: 76860) +Constraints : 1762647 (Binary: 91.4% Ternary: 6.8% Other: 1.9%) + +Memory Peak : 383MB +Max. Length : 35 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.03s +Memory: 362MB (+14MB) +UNKNOWN +Iteration Time: 6.77s + +Iteration 14 +Queue: [(9,45,0,True), (10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True)] +Grounded Until: 40 +Expected Memory: 397.0MB +Grounding... [('step', [41]), ('step', [42]), ('step', [43]), ('step', [44]), ('step', [45]), ('check', [45])] +Grounding Time: 0.47s +Memory: 370MB (+8MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 15 +Time : 71.119s (Solving: 63.32s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 71.000s + +Choices : 948263 (Domain: 862777) +Conflicts : 89765 (Analyzed: 89762) +Restarts : 1043 (Average: 86.06 Last: 111) +Model-Level : 148.0 +Problems : 15 (Average Length: 25.33 Splits: 0) +Lemmas : 89762 (Deleted: 72415) + Binary : 3941 (Ratio: 4.39%) + Ternary : 1936 (Ratio: 2.16%) + Conflict : 89762 (Average Length: 411.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 89762 (Average: 9.65 Max: 774 Sum: 865953) + Executed : 89669 (Average: 9.63 Max: 774 Sum: 864081 Ratio: 99.78%) + Bounded : 93 (Average: 20.13 Max: 47 Sum: 1872 Ratio: 0.22%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 281362 (Eliminated: 0 Frozen: 87295) +Constraints : 2012232 (Binary: 91.4% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 411MB +Max. Length : 40 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.35s +Memory: 404MB (+34MB) +UNKNOWN +Iteration Time: 8.11s + +Iteration 15 +Queue: [(10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True)] +Grounded Until: 45 +Expected Memory: 446.0MB +Grounding... [('step', [46]), ('step', [47]), ('step', [48]), ('step', [49]), ('step', [50]), ('check', [50])] +Grounding Time: 0.49s +Memory: 404MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 16 +Time : 78.561s (Solving: 69.91s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 78.448s + +Choices : 1055346 (Domain: 961782) +Conflicts : 97974 (Analyzed: 97971) +Restarts : 1143 (Average: 85.71 Last: 111) +Model-Level : 148.0 +Problems : 16 (Average Length: 27.00 Splits: 0) +Lemmas : 97971 (Deleted: 79839) + Binary : 4086 (Ratio: 4.17%) + Ternary : 1991 (Ratio: 2.03%) + Conflict : 97971 (Average Length: 403.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 97971 (Average: 9.74 Max: 774 Sum: 954678) + Executed : 97878 (Average: 9.73 Max: 774 Sum: 952806 Ratio: 99.80%) + Bounded : 93 (Average: 20.13 Max: 47 Sum: 1872 Ratio: 0.20%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 314308 (Eliminated: 0 Frozen: 97730) +Constraints : 2261777 (Binary: 91.4% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 448MB +Max. Length : 45 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.67s +Memory: 418MB (+14MB) +UNKNOWN +Iteration Time: 7.45s + +Iteration 16 +Queue: [(11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True)] +Grounded Until: 50 +Expected Memory: 460.0MB +Grounding... [('step', [51]), ('step', [52]), ('step', [53]), ('step', [54]), ('step', [55]), ('check', [55])] +Grounding Time: 0.62s +Memory: 435MB (+17MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 17 +Time : 87.749s (Solving: 78.10s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 87.640s + +Choices : 1191783 (Domain: 1094372) +Conflicts : 106343 (Analyzed: 106340) +Restarts : 1243 (Average: 85.55 Last: 111) +Model-Level : 148.0 +Problems : 17 (Average Length: 28.76 Splits: 0) +Lemmas : 106340 (Deleted: 87384) + Binary : 4313 (Ratio: 4.06%) + Ternary : 2093 (Ratio: 1.97%) + Conflict : 106340 (Average Length: 400.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 106340 (Average: 10.09 Max: 774 Sum: 1072670) + Executed : 106247 (Average: 10.07 Max: 774 Sum: 1070798 Ratio: 99.83%) + Bounded : 93 (Average: 20.13 Max: 47 Sum: 1872 Ratio: 0.17%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 347254 (Eliminated: 0 Frozen: 108165) +Constraints : 2511362 (Binary: 91.4% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 485MB +Max. Length : 50 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.28s +Memory: 452MB (+17MB) +UNKNOWN +Iteration Time: 9.20s + +Iteration 17 +Queue: [(12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True)] +Grounded Until: 55 +Expected Memory: 494.0MB +Grounding... [('step', [56]), ('step', [57]), ('step', [58]), ('step', [59]), ('step', [60]), ('check', [60])] +Grounding Time: 0.45s +Memory: 456MB (+4MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 18 +Time : 95.959s (Solving: 85.47s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 95.852s + +Choices : 1323325 (Domain: 1222605) +Conflicts : 114010 (Analyzed: 114007) +Restarts : 1343 (Average: 84.89 Last: 111) +Model-Level : 148.0 +Problems : 18 (Average Length: 30.61 Splits: 0) +Lemmas : 114007 (Deleted: 95286) + Binary : 4470 (Ratio: 3.92%) + Ternary : 2135 (Ratio: 1.87%) + Conflict : 114007 (Average Length: 394.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 114007 (Average: 10.39 Max: 774 Sum: 1184382) + Executed : 113913 (Average: 10.37 Max: 774 Sum: 1182448 Ratio: 99.84%) + Bounded : 94 (Average: 20.57 Max: 62 Sum: 1934 Ratio: 0.16%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 380200 (Eliminated: 0 Frozen: 118600) +Constraints : 2760947 (Binary: 91.4% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 510MB +Max. Length : 55 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.45s +Memory: 471MB (+15MB) +UNKNOWN +Iteration Time: 8.22s + +Iteration 18 +Queue: [(13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True)] +Grounded Until: 60 +Expected Memory: 513.0MB +Grounding... [('step', [61]), ('step', [62]), ('step', [63]), ('step', [64]), ('step', [65]), ('check', [65])] +Grounding Time: 0.45s +Memory: 479MB (+8MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 19 +Time : 104.064s (Solving: 92.71s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 103.960s + +Choices : 1427277 (Domain: 1324028) +Conflicts : 121551 (Analyzed: 121548) +Restarts : 1443 (Average: 84.23 Last: 159) +Model-Level : 148.0 +Problems : 19 (Average Length: 32.53 Splits: 0) +Lemmas : 121548 (Deleted: 102495) + Binary : 4555 (Ratio: 3.75%) + Ternary : 2169 (Ratio: 1.78%) + Conflict : 121548 (Average Length: 387.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 121548 (Average: 10.46 Max: 774 Sum: 1270979) + Executed : 121451 (Average: 10.44 Max: 774 Sum: 1268844 Ratio: 99.83%) + Bounded : 97 (Average: 22.01 Max: 67 Sum: 2135 Ratio: 0.17%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 413146 (Eliminated: 0 Frozen: 129035) +Constraints : 3010506 (Binary: 91.4% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 537MB +Max. Length : 60 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.33s +Memory: 528MB (+49MB) +UNKNOWN +Iteration Time: 8.12s + +Iteration 19 +Queue: [(14,70,0,True), (15,75,0,True), (16,80,0,True)] +Grounded Until: 65 +Expected Memory: 585.0MB +Grounding... [('step', [66]), ('step', [67]), ('step', [68]), ('step', [69]), ('step', [70]), ('check', [70])] +Grounding Time: 0.45s +Memory: 528MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 20 +Time : 111.037s (Solving: 98.81s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 110.936s + +Choices : 1500972 (Domain: 1396939) +Conflicts : 128890 (Analyzed: 128887) +Restarts : 1543 (Average: 83.53 Last: 159) +Model-Level : 148.0 +Problems : 20 (Average Length: 34.50 Splits: 0) +Lemmas : 128887 (Deleted: 109718) + Binary : 4607 (Ratio: 3.57%) + Ternary : 2193 (Ratio: 1.70%) + Conflict : 128887 (Average Length: 380.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 128887 (Average: 10.32 Max: 774 Sum: 1329866) + Executed : 128789 (Average: 10.30 Max: 774 Sum: 1327659 Ratio: 99.83%) + Bounded : 98 (Average: 22.52 Max: 72 Sum: 2207 Ratio: 0.17%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 446092 (Eliminated: 0 Frozen: 139470) +Constraints : 3260041 (Binary: 91.4% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 582MB +Max. Length : 65 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.19s +Memory: 532MB (+4MB) +UNKNOWN +Iteration Time: 6.99s + +Iteration 20 +Queue: [(15,75,0,True), (16,80,0,True)] +Grounded Until: 70 +Expected Memory: 589.0MB +Grounding... [('step', [71]), ('step', [72]), ('step', [73]), ('step', [74]), ('step', [75]), ('check', [75])] +Grounding Time: 0.47s +Memory: 535MB (+3MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 21 +Time : 118.947s (Solving: 105.80s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 118.848s + +Choices : 1589971 (Domain: 1483795) +Conflicts : 136496 (Analyzed: 136493) +Restarts : 1643 (Average: 83.08 Last: 159) +Model-Level : 148.0 +Problems : 21 (Average Length: 36.52 Splits: 0) +Lemmas : 136493 (Deleted: 116783) + Binary : 4692 (Ratio: 3.44%) + Ternary : 2209 (Ratio: 1.62%) + Conflict : 136493 (Average Length: 376.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 136493 (Average: 10.26 Max: 775 Sum: 1401023) + Executed : 136395 (Average: 10.25 Max: 775 Sum: 1398816 Ratio: 99.84%) + Bounded : 98 (Average: 22.52 Max: 72 Sum: 2207 Ratio: 0.16%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 479038 (Eliminated: 0 Frozen: 149905) +Constraints : 3509601 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 607MB +Max. Length : 70 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.09s +Memory: 558MB (+23MB) +UNKNOWN +Iteration Time: 7.92s + +Iteration 21 +Queue: [(16,80,0,True)] +Grounded Until: 75 +Expected Memory: 615.0MB +Grounding... [('step', [76]), ('step', [77]), ('step', [78]), ('step', [79]), ('step', [80]), ('check', [80])] +Grounding Time: 0.47s +Memory: 558MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 22 +Time : 129.516s (Solving: 115.44s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 129.420s + +Choices : 1780958 (Domain: 1670882) +Conflicts : 144738 (Analyzed: 144735) +Restarts : 1743 (Average: 83.04 Last: 159) +Model-Level : 148.0 +Problems : 22 (Average Length: 38.59 Splits: 0) +Lemmas : 144735 (Deleted: 123899) + Binary : 4911 (Ratio: 3.39%) + Ternary : 2305 (Ratio: 1.59%) + Conflict : 144735 (Average Length: 384.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 144735 (Average: 10.80 Max: 775 Sum: 1562709) + Executed : 144637 (Average: 10.78 Max: 775 Sum: 1560502 Ratio: 99.86%) + Bounded : 98 (Average: 22.52 Max: 72 Sum: 2207 Ratio: 0.14%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 511984 (Eliminated: 0 Frozen: 160340) +Constraints : 3759186 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 630MB +Max. Length : 75 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.74s +Memory: 581MB (+23MB) +UNKNOWN +Iteration Time: 10.58s + +Iteration 22 +Queue: [(4,20,2,True), (5,25,2,True), (6,30,2,True), (7,35,1,True), (8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 80 +Blocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 23 +Time : 133.071s (Solving: 118.89s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 132.976s + +Choices : 1807843 (Domain: 1697767) +Conflicts : 151929 (Analyzed: 151926) +Restarts : 1843 (Average: 82.43 Last: 159) +Model-Level : 148.0 +Problems : 23 (Average Length: 40.48 Splits: 0) +Lemmas : 151926 (Deleted: 131781) + Binary : 4944 (Ratio: 3.25%) + Ternary : 2325 (Ratio: 1.53%) + Conflict : 151926 (Average Length: 378.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 151926 (Average: 10.42 Max: 775 Sum: 1583713) + Executed : 151828 (Average: 10.41 Max: 775 Sum: 1581506 Ratio: 99.86%) + Bounded : 98 (Average: 22.52 Max: 72 Sum: 2207 Ratio: 0.14%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 511984 (Eliminated: 0 Frozen: 160340) +Constraints : 3759186 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 630MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 3.52s +Memory: 583MB (+2MB) +UNKNOWN +Iteration Time: 3.56s + +Iteration 23 +Queue: [(5,25,2,True), (6,30,2,True), (7,35,1,True), (8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 80 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 24 +Time : 138.723s (Solving: 124.40s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 138.628s + +Choices : 1851780 (Domain: 1741704) +Conflicts : 159791 (Analyzed: 159788) +Restarts : 1943 (Average: 82.24 Last: 159) +Model-Level : 148.0 +Problems : 24 (Average Length: 42.21 Splits: 0) +Lemmas : 159788 (Deleted: 138644) + Binary : 5011 (Ratio: 3.14%) + Ternary : 2350 (Ratio: 1.47%) + Conflict : 159788 (Average Length: 375.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 159788 (Average: 10.15 Max: 775 Sum: 1621953) + Executed : 159690 (Average: 10.14 Max: 775 Sum: 1619746 Ratio: 99.86%) + Bounded : 98 (Average: 22.52 Max: 72 Sum: 2207 Ratio: 0.14%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 511984 (Eliminated: 0 Frozen: 160340) +Constraints : 3759186 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 630MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 5.60s +Memory: 583MB (+0MB) +UNKNOWN +Iteration Time: 5.66s + +Iteration 24 +Queue: [(6,30,2,True), (7,35,1,True), (8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 80 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 25 +Time : 143.338s (Solving: 128.88s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 143.244s + +Choices : 1889488 (Domain: 1778476) +Conflicts : 167541 (Analyzed: 167538) +Restarts : 2043 (Average: 82.01 Last: 159) +Model-Level : 148.0 +Problems : 25 (Average Length: 43.80 Splits: 0) +Lemmas : 167538 (Deleted: 145932) + Binary : 5058 (Ratio: 3.02%) + Ternary : 2366 (Ratio: 1.41%) + Conflict : 167538 (Average Length: 369.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 167538 (Average: 9.87 Max: 775 Sum: 1653157) + Executed : 167439 (Average: 9.85 Max: 775 Sum: 1650868 Ratio: 99.86%) + Bounded : 99 (Average: 23.12 Max: 82 Sum: 2289 Ratio: 0.14%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 511984 (Eliminated: 0 Frozen: 160340) +Constraints : 3759186 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 630MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 4.57s +Memory: 583MB (+0MB) +UNKNOWN +Iteration Time: 4.62s + +Iteration 25 +Queue: [(7,35,1,True), (8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 80 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 26 +Time : 149.287s (Solving: 134.73s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 149.196s + +Choices : 1938816 (Domain: 1827394) +Conflicts : 175116 (Analyzed: 175113) +Restarts : 2143 (Average: 81.71 Last: 159) +Model-Level : 148.0 +Problems : 26 (Average Length: 45.27 Splits: 0) +Lemmas : 175113 (Deleted: 153237) + Binary : 5168 (Ratio: 2.95%) + Ternary : 2380 (Ratio: 1.36%) + Conflict : 175113 (Average Length: 365.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 175113 (Average: 9.68 Max: 775 Sum: 1694488) + Executed : 175013 (Average: 9.66 Max: 775 Sum: 1692117 Ratio: 99.86%) + Bounded : 100 (Average: 23.71 Max: 82 Sum: 2371 Ratio: 0.14%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 511984 (Eliminated: 0 Frozen: 160340) +Constraints : 3759172 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 630MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 5.92s +Memory: 583MB (+0MB) +UNKNOWN +Iteration Time: 5.95s + +Iteration 26 +Queue: [(8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 80 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 27 +Time : 156.184s (Solving: 141.52s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 156.096s + +Choices : 2013412 (Domain: 1898919) +Conflicts : 183283 (Analyzed: 183280) +Restarts : 2243 (Average: 81.71 Last: 159) +Model-Level : 148.0 +Problems : 27 (Average Length: 46.63 Splits: 0) +Lemmas : 183280 (Deleted: 160499) + Binary : 5220 (Ratio: 2.85%) + Ternary : 2401 (Ratio: 1.31%) + Conflict : 183280 (Average Length: 363.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 183280 (Average: 9.57 Max: 775 Sum: 1754389) + Executed : 183180 (Average: 9.56 Max: 775 Sum: 1752018 Ratio: 99.86%) + Bounded : 100 (Average: 23.71 Max: 82 Sum: 2371 Ratio: 0.14%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 511984 (Eliminated: 0 Frozen: 160340) +Constraints : 3759158 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 630MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.86s +Memory: 583MB (+0MB) +UNKNOWN +Iteration Time: 6.90s + +Iteration 27 +Queue: [(9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 80 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 28 +Time : 163.639s (Solving: 148.86s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 163.552s + +Choices : 2088124 (Domain: 1971219) +Conflicts : 191612 (Analyzed: 191609) +Restarts : 2343 (Average: 81.78 Last: 159) +Model-Level : 148.0 +Problems : 28 (Average Length: 47.89 Splits: 0) +Lemmas : 191609 (Deleted: 168451) + Binary : 5293 (Ratio: 2.76%) + Ternary : 2438 (Ratio: 1.27%) + Conflict : 191609 (Average Length: 360.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 191609 (Average: 9.49 Max: 814 Sum: 1818021) + Executed : 191506 (Average: 9.47 Max: 814 Sum: 1815404 Ratio: 99.86%) + Bounded : 103 (Average: 25.41 Max: 82 Sum: 2617 Ratio: 0.14%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 511984 (Eliminated: 0 Frozen: 160340) +Constraints : 3759158 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 630MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.42s +Memory: 583MB (+0MB) +UNKNOWN +Iteration Time: 7.46s + +Iteration 28 +Queue: [(10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 80 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 29 +Time : 170.568s (Solving: 155.66s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 170.484s + +Choices : 2167260 (Domain: 2046633) +Conflicts : 199585 (Analyzed: 199582) +Restarts : 2443 (Average: 81.70 Last: 159) +Model-Level : 148.0 +Problems : 29 (Average Length: 49.07 Splits: 0) +Lemmas : 199582 (Deleted: 176144) + Binary : 5407 (Ratio: 2.71%) + Ternary : 2505 (Ratio: 1.26%) + Conflict : 199582 (Average Length: 360.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 199582 (Average: 9.42 Max: 814 Sum: 1880690) + Executed : 199479 (Average: 9.41 Max: 814 Sum: 1878073 Ratio: 99.86%) + Bounded : 103 (Average: 25.41 Max: 82 Sum: 2617 Ratio: 0.14%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 511984 (Eliminated: 0 Frozen: 160340) +Constraints : 3759105 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 630MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.88s +Memory: 583MB (+0MB) +UNKNOWN +Iteration Time: 6.93s + +Iteration 29 +Queue: [(11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 80 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 30 +Time : 178.816s (Solving: 163.80s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 178.736s + +Choices : 2283872 (Domain: 2158631) +Conflicts : 207741 (Analyzed: 207738) +Restarts : 2543 (Average: 81.69 Last: 159) +Model-Level : 148.0 +Problems : 30 (Average Length: 50.17 Splits: 0) +Lemmas : 207738 (Deleted: 183732) + Binary : 5513 (Ratio: 2.65%) + Ternary : 2537 (Ratio: 1.22%) + Conflict : 207738 (Average Length: 364.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 207738 (Average: 9.51 Max: 814 Sum: 1976605) + Executed : 207635 (Average: 9.50 Max: 814 Sum: 1973988 Ratio: 99.87%) + Bounded : 103 (Average: 25.41 Max: 82 Sum: 2617 Ratio: 0.13%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 511984 (Eliminated: 0 Frozen: 160340) +Constraints : 3759105 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 630MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.22s +Memory: 583MB (+0MB) +UNKNOWN +Iteration Time: 8.25s + +Iteration 30 +Queue: [(12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 80 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 31 +Time : 186.116s (Solving: 171.00s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 186.040s + +Choices : 2368951 (Domain: 2241125) +Conflicts : 215177 (Analyzed: 215174) +Restarts : 2643 (Average: 81.41 Last: 159) +Model-Level : 148.0 +Problems : 31 (Average Length: 51.19 Splits: 0) +Lemmas : 215174 (Deleted: 191445) + Binary : 5592 (Ratio: 2.60%) + Ternary : 2553 (Ratio: 1.19%) + Conflict : 215174 (Average Length: 364.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 215174 (Average: 9.51 Max: 814 Sum: 2045576) + Executed : 215071 (Average: 9.49 Max: 814 Sum: 2042959 Ratio: 99.87%) + Bounded : 103 (Average: 25.41 Max: 82 Sum: 2617 Ratio: 0.13%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 511984 (Eliminated: 0 Frozen: 160340) +Constraints : 3759105 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 630MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.27s +Memory: 583MB (+0MB) +UNKNOWN +Iteration Time: 7.31s + +Iteration 31 +Queue: [(13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 80 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 32 +Time : 193.432s (Solving: 178.21s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 193.360s + +Choices : 2470796 (Domain: 2340598) +Conflicts : 222452 (Analyzed: 222449) +Restarts : 2743 (Average: 81.10 Last: 159) +Model-Level : 148.0 +Problems : 32 (Average Length: 52.16 Splits: 0) +Lemmas : 222449 (Deleted: 198753) + Binary : 5655 (Ratio: 2.54%) + Ternary : 2592 (Ratio: 1.17%) + Conflict : 222449 (Average Length: 363.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 222449 (Average: 9.58 Max: 814 Sum: 2131554) + Executed : 222346 (Average: 9.57 Max: 814 Sum: 2128937 Ratio: 99.88%) + Bounded : 103 (Average: 25.41 Max: 82 Sum: 2617 Ratio: 0.12%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 511984 (Eliminated: 0 Frozen: 160340) +Constraints : 3759105 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 630MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.28s +Memory: 583MB (+0MB) +UNKNOWN +Iteration Time: 7.32s + +Iteration 32 +Queue: [(14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 80 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 33 +Time : 202.132s (Solving: 186.78s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 202.064s + +Choices : 2587643 (Domain: 2454056) +Conflicts : 230202 (Analyzed: 230199) +Restarts : 2843 (Average: 80.97 Last: 159) +Model-Level : 148.0 +Problems : 33 (Average Length: 53.06 Splits: 0) +Lemmas : 230199 (Deleted: 205662) + Binary : 5740 (Ratio: 2.49%) + Ternary : 2607 (Ratio: 1.13%) + Conflict : 230199 (Average Length: 364.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 230199 (Average: 9.69 Max: 814 Sum: 2230931) + Executed : 230095 (Average: 9.68 Max: 814 Sum: 2228232 Ratio: 99.88%) + Bounded : 104 (Average: 25.95 Max: 82 Sum: 2699 Ratio: 0.12%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 511984 (Eliminated: 0 Frozen: 160340) +Constraints : 3759105 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 630MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.65s +Memory: 583MB (+0MB) +UNKNOWN +Iteration Time: 8.71s + +Iteration 33 +Queue: [(15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 80 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 34 +Time : 210.489s (Solving: 195.01s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 210.424s + +Choices : 2716130 (Domain: 2580743) +Conflicts : 238017 (Analyzed: 238014) +Restarts : 2943 (Average: 80.87 Last: 159) +Model-Level : 148.0 +Problems : 34 (Average Length: 53.91 Splits: 0) +Lemmas : 238014 (Deleted: 213024) + Binary : 5810 (Ratio: 2.44%) + Ternary : 2645 (Ratio: 1.11%) + Conflict : 238014 (Average Length: 362.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 238014 (Average: 9.84 Max: 814 Sum: 2343046) + Executed : 237909 (Average: 9.83 Max: 814 Sum: 2340265 Ratio: 99.88%) + Bounded : 105 (Average: 26.49 Max: 82 Sum: 2781 Ratio: 0.12%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 511984 (Eliminated: 0 Frozen: 160340) +Constraints : 3759091 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 630MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.31s +Memory: 583MB (+0MB) +UNKNOWN +Iteration Time: 8.36s + +Iteration 34 +Queue: [(16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 80 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 35 +Time : 219.175s (Solving: 203.57s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 219.112s + +Choices : 2850433 (Domain: 2712692) +Conflicts : 245867 (Analyzed: 245864) +Restarts : 3043 (Average: 80.80 Last: 159) +Model-Level : 148.0 +Problems : 35 (Average Length: 54.71 Splits: 0) +Lemmas : 245864 (Deleted: 220430) + Binary : 5881 (Ratio: 2.39%) + Ternary : 2685 (Ratio: 1.09%) + Conflict : 245864 (Average Length: 361.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 245864 (Average: 10.00 Max: 814 Sum: 2459789) + Executed : 245759 (Average: 9.99 Max: 814 Sum: 2457008 Ratio: 99.89%) + Bounded : 105 (Average: 26.49 Max: 82 Sum: 2781 Ratio: 0.11%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 511984 (Eliminated: 0 Frozen: 160340) +Constraints : 3759073 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 630MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.65s +Memory: 583MB (+0MB) +UNKNOWN +Iteration Time: 8.69s + +Iteration 35 +Queue: [(17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 80 +Expected Memory: 640.0MB +Grounding... [('step', [81]), ('step', [82]), ('step', [83]), ('step', [84]), ('step', [85]), ('check', [85])] +Grounding Time: 0.47s +Memory: 583MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 36 +Time : 228.559s (Solving: 211.99s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 228.496s + +Choices : 2998710 (Domain: 2859367) +Conflicts : 253634 (Analyzed: 253631) +Restarts : 3143 (Average: 80.70 Last: 159) +Model-Level : 148.0 +Problems : 36 (Average Length: 55.61 Splits: 0) +Lemmas : 253631 (Deleted: 228078) + Binary : 5971 (Ratio: 2.35%) + Ternary : 2732 (Ratio: 1.08%) + Conflict : 253631 (Average Length: 359.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 253631 (Average: 10.21 Max: 882 Sum: 2590441) + Executed : 253526 (Average: 10.20 Max: 882 Sum: 2587660 Ratio: 99.89%) + Bounded : 105 (Average: 26.49 Max: 82 Sum: 2781 Ratio: 0.11%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 544930 (Eliminated: 0 Frozen: 170775) +Constraints : 4008658 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 659MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.53s +Memory: 601MB (+18MB) +UNKNOWN +Iteration Time: 9.40s + +Iteration 36 +Queue: [(18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 85 +Expected Memory: 658.0MB +Grounding... [('step', [86]), ('step', [87]), ('step', [88]), ('step', [89]), ('step', [90]), ('check', [90])] +Grounding Time: 0.48s +Memory: 601MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 37 +Time : 238.252s (Solving: 220.69s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 238.192s + +Choices : 3170212 (Domain: 3028736) +Conflicts : 261445 (Analyzed: 261442) +Restarts : 3243 (Average: 80.62 Last: 159) +Model-Level : 148.0 +Problems : 37 (Average Length: 56.59 Splits: 0) +Lemmas : 261442 (Deleted: 235399) + Binary : 6129 (Ratio: 2.34%) + Ternary : 2798 (Ratio: 1.07%) + Conflict : 261442 (Average Length: 355.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 261442 (Average: 10.50 Max: 882 Sum: 2745941) + Executed : 261336 (Average: 10.49 Max: 882 Sum: 2743068 Ratio: 99.90%) + Bounded : 106 (Average: 27.10 Max: 92 Sum: 2873 Ratio: 0.10%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 577876 (Eliminated: 0 Frozen: 181210) +Constraints : 4258243 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 682MB +Max. Length : 85 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.82s +Memory: 621MB (+20MB) +UNKNOWN +Iteration Time: 9.70s + +Iteration 37 +Queue: [(19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 90 +Expected Memory: 678.0MB +Grounding... [('step', [91]), ('step', [92]), ('step', [93]), ('step', [94]), ('step', [95]), ('check', [95])] +Grounding Time: 0.48s +Memory: 622MB (+1MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 38 +Time : 249.715s (Solving: 231.14s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 249.660s + +Choices : 3474637 (Domain: 3329889) +Conflicts : 269142 (Analyzed: 269139) +Restarts : 3343 (Average: 80.51 Last: 159) +Model-Level : 148.0 +Problems : 38 (Average Length: 57.66 Splits: 0) +Lemmas : 269139 (Deleted: 242452) + Binary : 6477 (Ratio: 2.41%) + Ternary : 2896 (Ratio: 1.08%) + Conflict : 269139 (Average Length: 353.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 269139 (Average: 11.26 Max: 944 Sum: 3029192) + Executed : 269033 (Average: 11.24 Max: 944 Sum: 3026319 Ratio: 99.91%) + Bounded : 106 (Average: 27.10 Max: 92 Sum: 2873 Ratio: 0.09%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 610822 (Eliminated: 0 Frozen: 191645) +Constraints : 4507814 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 709MB +Max. Length : 90 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 10.56s +Memory: 693MB (+71MB) +UNKNOWN +Iteration Time: 11.48s + +Iteration 38 +Queue: [(20,100,0,True), (21,105,0,True)] +Grounded Until: 95 +Expected Memory: 765.0MB +Grounding... [('step', [96]), ('step', [97]), ('step', [98]), ('step', [99]), ('step', [100]), ('check', [100])] +Grounding Time: 0.48s +Memory: 693MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 39 +Time : 262.040s (Solving: 242.45s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 261.992s + +Choices : 3858341 (Domain: 3711317) +Conflicts : 277514 (Analyzed: 277511) +Restarts : 3443 (Average: 80.60 Last: 159) +Model-Level : 148.0 +Problems : 39 (Average Length: 58.79 Splits: 0) +Lemmas : 277511 (Deleted: 249318) + Binary : 6875 (Ratio: 2.48%) + Ternary : 3036 (Ratio: 1.09%) + Conflict : 277511 (Average Length: 353.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 277511 (Average: 12.21 Max: 1035 Sum: 3388836) + Executed : 277404 (Average: 12.20 Max: 1035 Sum: 3385861 Ratio: 99.91%) + Bounded : 107 (Average: 27.80 Max: 102 Sum: 2975 Ratio: 0.09%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 643768 (Eliminated: 0 Frozen: 202080) +Constraints : 4757399 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 772MB +Max. Length : 95 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 11.44s +Memory: 697MB (+4MB) +UNKNOWN +Iteration Time: 12.34s + +Iteration 39 +Queue: [(21,105,0,True)] +Grounded Until: 100 +Expected Memory: 769.0MB +Grounding... [('step', [101]), ('step', [102]), ('step', [103]), ('step', [104]), ('step', [105]), ('check', [105])] +Grounding Time: 0.51s +Memory: 697MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 40 +Time : 281.093s (Solving: 260.42s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 281.052s + +Choices : 4362555 (Domain: 4214068) +Conflicts : 286424 (Analyzed: 286421) +Restarts : 3543 (Average: 80.84 Last: 159) +Model-Level : 148.0 +Problems : 40 (Average Length: 60.00 Splits: 0) +Lemmas : 286421 (Deleted: 258618) + Binary : 7425 (Ratio: 2.59%) + Ternary : 3146 (Ratio: 1.10%) + Conflict : 286421 (Average Length: 367.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 286421 (Average: 13.47 Max: 1058 Sum: 3857690) + Executed : 286314 (Average: 13.46 Max: 1058 Sum: 3854715 Ratio: 99.92%) + Bounded : 107 (Average: 27.80 Max: 102 Sum: 2975 Ratio: 0.08%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 676714 (Eliminated: 0 Frozen: 212515) +Constraints : 5006970 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 780MB +Max. Length : 100 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 18.11s +Memory: 706MB (+9MB) +UNKNOWN +Iteration Time: 19.07s + +Iteration 40 +Queue: [(4,20,3,True), (5,25,3,True), (6,30,3,True), (7,35,2,True), (8,40,2,True), (9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Blocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 41 +Time : 286.687s (Solving: 265.86s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 286.648s + +Choices : 4412771 (Domain: 4264266) +Conflicts : 294294 (Analyzed: 294291) +Restarts : 3643 (Average: 80.78 Last: 159) +Model-Level : 148.0 +Problems : 41 (Average Length: 61.15 Splits: 0) +Lemmas : 294291 (Deleted: 264978) + Binary : 7473 (Ratio: 2.54%) + Ternary : 3171 (Ratio: 1.08%) + Conflict : 294291 (Average Length: 369.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 294291 (Average: 13.26 Max: 1058 Sum: 3901585) + Executed : 294183 (Average: 13.25 Max: 1058 Sum: 3898503 Ratio: 99.92%) + Bounded : 108 (Average: 28.54 Max: 107 Sum: 3082 Ratio: 0.08%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 676714 (Eliminated: 0 Frozen: 212515) +Constraints : 5006970 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 834MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 5.54s +Memory: 770MB (+64MB) +UNKNOWN +Iteration Time: 5.60s + +Iteration 41 +Queue: [(5,25,3,True), (6,30,3,True), (7,35,2,True), (8,40,2,True), (9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 42 +Time : 294.358s (Solving: 273.38s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 294.324s + +Choices : 4470707 (Domain: 4322198) +Conflicts : 302299 (Analyzed: 302296) +Restarts : 3743 (Average: 80.76 Last: 159) +Model-Level : 148.0 +Problems : 42 (Average Length: 62.24 Splits: 0) +Lemmas : 302296 (Deleted: 272551) + Binary : 7521 (Ratio: 2.49%) + Ternary : 3183 (Ratio: 1.05%) + Conflict : 302296 (Average Length: 371.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 302296 (Average: 13.08 Max: 1058 Sum: 3952952) + Executed : 302188 (Average: 13.07 Max: 1058 Sum: 3949870 Ratio: 99.92%) + Bounded : 108 (Average: 28.54 Max: 107 Sum: 3082 Ratio: 0.08%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 676714 (Eliminated: 0 Frozen: 212515) +Constraints : 5006958 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 834MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.62s +Memory: 770MB (+0MB) +UNKNOWN +Iteration Time: 7.68s + +Iteration 42 +Queue: [(6,30,3,True), (7,35,2,True), (8,40,2,True), (9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 43 +Time : 301.150s (Solving: 280.03s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 301.120s + +Choices : 4520875 (Domain: 4372366) +Conflicts : 310145 (Analyzed: 310142) +Restarts : 3843 (Average: 80.70 Last: 159) +Model-Level : 148.0 +Problems : 43 (Average Length: 63.28 Splits: 0) +Lemmas : 310142 (Deleted: 280197) + Binary : 7589 (Ratio: 2.45%) + Ternary : 3192 (Ratio: 1.03%) + Conflict : 310142 (Average Length: 372.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 310142 (Average: 12.88 Max: 1058 Sum: 3994814) + Executed : 310034 (Average: 12.87 Max: 1058 Sum: 3991732 Ratio: 99.92%) + Bounded : 108 (Average: 28.54 Max: 107 Sum: 3082 Ratio: 0.08%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 676714 (Eliminated: 0 Frozen: 212515) +Constraints : 5006958 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 834MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.74s +Memory: 770MB (+0MB) +UNKNOWN +Iteration Time: 6.80s + +Iteration 43 +Queue: [(7,35,2,True), (8,40,2,True), (9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 44 +Time : 309.503s (Solving: 288.22s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 309.476s + +Choices : 4598441 (Domain: 4449093) +Conflicts : 318441 (Analyzed: 318438) +Restarts : 3943 (Average: 80.76 Last: 159) +Model-Level : 148.0 +Problems : 44 (Average Length: 64.27 Splits: 0) +Lemmas : 318438 (Deleted: 287749) + Binary : 7772 (Ratio: 2.44%) + Ternary : 3226 (Ratio: 1.01%) + Conflict : 318438 (Average Length: 377.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 318438 (Average: 12.75 Max: 1058 Sum: 4059205) + Executed : 318330 (Average: 12.74 Max: 1058 Sum: 4056123 Ratio: 99.92%) + Bounded : 108 (Average: 28.54 Max: 107 Sum: 3082 Ratio: 0.08%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 676714 (Eliminated: 0 Frozen: 212515) +Constraints : 5006958 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 834MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.30s +Memory: 770MB (+0MB) +UNKNOWN +Iteration Time: 8.36s + +Iteration 44 +Queue: [(8,40,2,True), (9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 45 +Time : 319.446s (Solving: 298.02s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 319.424s + +Choices : 4732995 (Domain: 4582672) +Conflicts : 326695 (Analyzed: 326692) +Restarts : 4043 (Average: 80.80 Last: 159) +Model-Level : 148.0 +Problems : 45 (Average Length: 65.22 Splits: 0) +Lemmas : 326692 (Deleted: 295501) + Binary : 8041 (Ratio: 2.46%) + Ternary : 3252 (Ratio: 1.00%) + Conflict : 326692 (Average Length: 388.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 326692 (Average: 12.78 Max: 1058 Sum: 4176320) + Executed : 326583 (Average: 12.77 Max: 1058 Sum: 4173131 Ratio: 99.92%) + Bounded : 109 (Average: 29.26 Max: 107 Sum: 3189 Ratio: 0.08%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 676714 (Eliminated: 0 Frozen: 212515) +Constraints : 5006958 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 834MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.90s +Memory: 770MB (+0MB) +UNKNOWN +Iteration Time: 9.95s + +Iteration 45 +Queue: [(9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 46 +Time : 331.242s (Solving: 309.66s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 331.224s + +Choices : 4883441 (Domain: 4732585) +Conflicts : 335451 (Analyzed: 335448) +Restarts : 4143 (Average: 80.97 Last: 159) +Model-Level : 148.0 +Problems : 46 (Average Length: 66.13 Splits: 0) +Lemmas : 335448 (Deleted: 305236) + Binary : 8337 (Ratio: 2.49%) + Ternary : 3302 (Ratio: 0.98%) + Conflict : 335448 (Average Length: 400.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 335448 (Average: 12.84 Max: 1058 Sum: 4307898) + Executed : 335339 (Average: 12.83 Max: 1058 Sum: 4304709 Ratio: 99.93%) + Bounded : 109 (Average: 29.26 Max: 107 Sum: 3189 Ratio: 0.07%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 676714 (Eliminated: 0 Frozen: 212515) +Constraints : 5006944 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 834MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 11.74s +Memory: 770MB (+0MB) +UNKNOWN +Iteration Time: 11.80s + +Iteration 46 +Queue: [(10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 47 +Time : 339.375s (Solving: 317.65s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 339.364s + +Choices : 4979210 (Domain: 4828005) +Conflicts : 343943 (Analyzed: 343940) +Restarts : 4243 (Average: 81.06 Last: 199) +Model-Level : 148.0 +Problems : 47 (Average Length: 67.00 Splits: 0) +Lemmas : 343940 (Deleted: 311472) + Binary : 8484 (Ratio: 2.47%) + Ternary : 3342 (Ratio: 0.97%) + Conflict : 343940 (Average Length: 407.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 343940 (Average: 12.76 Max: 1058 Sum: 4388239) + Executed : 343831 (Average: 12.75 Max: 1058 Sum: 4385050 Ratio: 99.93%) + Bounded : 109 (Average: 29.26 Max: 107 Sum: 3189 Ratio: 0.07%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 676714 (Eliminated: 0 Frozen: 212515) +Constraints : 5006944 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 834MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.08s +Memory: 770MB (+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,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 48 +Time : 353.249s (Solving: 331.35s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 353.244s + +Choices : 5215039 (Domain: 5061950) +Conflicts : 352840 (Analyzed: 352837) +Restarts : 4343 (Average: 81.24 Last: 199) +Model-Level : 148.0 +Problems : 48 (Average Length: 67.83 Splits: 0) +Lemmas : 352837 (Deleted: 321529) + Binary : 8912 (Ratio: 2.53%) + Ternary : 3411 (Ratio: 0.97%) + Conflict : 352837 (Average Length: 420.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 352837 (Average: 13.04 Max: 1058 Sum: 4600970) + Executed : 352728 (Average: 13.03 Max: 1058 Sum: 4597781 Ratio: 99.93%) + Bounded : 109 (Average: 29.26 Max: 107 Sum: 3189 Ratio: 0.07%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 676714 (Eliminated: 0 Frozen: 212515) +Constraints : 5006944 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 834MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 13.81s +Memory: 770MB (+0MB) +UNKNOWN +Iteration Time: 13.88s + +Iteration 48 +Queue: [(12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 49 +Time : 361.821s (Solving: 339.78s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 361.820s + +Choices : 5339492 (Domain: 5185899) +Conflicts : 360999 (Analyzed: 360996) +Restarts : 4443 (Average: 81.25 Last: 199) +Model-Level : 148.0 +Problems : 49 (Average Length: 68.63 Splits: 0) +Lemmas : 360996 (Deleted: 327811) + Binary : 9061 (Ratio: 2.51%) + Ternary : 3440 (Ratio: 0.95%) + Conflict : 360996 (Average Length: 425.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 360996 (Average: 13.04 Max: 1058 Sum: 4706779) + Executed : 360887 (Average: 13.03 Max: 1058 Sum: 4703590 Ratio: 99.93%) + Bounded : 109 (Average: 29.26 Max: 107 Sum: 3189 Ratio: 0.07%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 676714 (Eliminated: 0 Frozen: 212515) +Constraints : 5006944 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 834MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.53s +Memory: 770MB (+0MB) +UNKNOWN +Iteration Time: 8.58s + +Iteration 49 +Queue: [(13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 50 +Time : 371.561s (Solving: 349.36s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 371.564s + +Choices : 5442711 (Domain: 5288677) +Conflicts : 369661 (Analyzed: 369658) +Restarts : 4543 (Average: 81.37 Last: 199) +Model-Level : 148.0 +Problems : 50 (Average Length: 69.40 Splits: 0) +Lemmas : 369658 (Deleted: 337659) + Binary : 9134 (Ratio: 2.47%) + Ternary : 3472 (Ratio: 0.94%) + Conflict : 369658 (Average Length: 429.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 369658 (Average: 12.97 Max: 1058 Sum: 4794376) + Executed : 369549 (Average: 12.96 Max: 1058 Sum: 4791187 Ratio: 99.93%) + Bounded : 109 (Average: 29.26 Max: 107 Sum: 3189 Ratio: 0.07%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 676714 (Eliminated: 0 Frozen: 212515) +Constraints : 5006944 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 834MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.68s +Memory: 770MB (+0MB) +UNKNOWN +Iteration Time: 9.75s + +Iteration 50 +Queue: [(17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 51 +Time : 379.915s (Solving: 357.54s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 379.920s + +Choices : 5511291 (Domain: 5357243) +Conflicts : 377449 (Analyzed: 377446) +Restarts : 4643 (Average: 81.29 Last: 199) +Model-Level : 148.0 +Problems : 51 (Average Length: 70.14 Splits: 0) +Lemmas : 377446 (Deleted: 343925) + Binary : 9154 (Ratio: 2.43%) + Ternary : 3477 (Ratio: 0.92%) + Conflict : 377446 (Average Length: 431.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 377446 (Average: 12.84 Max: 1058 Sum: 4845498) + Executed : 377337 (Average: 12.83 Max: 1058 Sum: 4842309 Ratio: 99.93%) + Bounded : 109 (Average: 29.26 Max: 107 Sum: 3189 Ratio: 0.07%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 676714 (Eliminated: 0 Frozen: 212515) +Constraints : 5006944 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 834MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.29s +Memory: 770MB (+0MB) +UNKNOWN +Iteration Time: 8.36s + +Iteration 51 +Queue: [(18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 52 +Time : 387.856s (Solving: 365.33s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 387.864s + +Choices : 5608591 (Domain: 5453833) +Conflicts : 385686 (Analyzed: 385683) +Restarts : 4743 (Average: 81.32 Last: 199) +Model-Level : 148.0 +Problems : 52 (Average Length: 70.85 Splits: 0) +Lemmas : 385683 (Deleted: 351500) + Binary : 9255 (Ratio: 2.40%) + Ternary : 3490 (Ratio: 0.90%) + Conflict : 385683 (Average Length: 434.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 385683 (Average: 12.76 Max: 1058 Sum: 4923227) + Executed : 385574 (Average: 12.76 Max: 1058 Sum: 4920038 Ratio: 99.94%) + Bounded : 109 (Average: 29.26 Max: 107 Sum: 3189 Ratio: 0.06%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 676714 (Eliminated: 0 Frozen: 212515) +Constraints : 5006944 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 834MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.89s +Memory: 770MB (+0MB) +UNKNOWN +Iteration Time: 7.95s + +Iteration 52 +Queue: [(19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 53 +Time : 395.982s (Solving: 373.32s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 395.996s + +Choices : 5710949 (Domain: 5555752) +Conflicts : 393815 (Analyzed: 393812) +Restarts : 4843 (Average: 81.32 Last: 199) +Model-Level : 148.0 +Problems : 53 (Average Length: 71.53 Splits: 0) +Lemmas : 393812 (Deleted: 359513) + Binary : 9388 (Ratio: 2.38%) + Ternary : 3493 (Ratio: 0.89%) + Conflict : 393812 (Average Length: 439.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 393812 (Average: 12.71 Max: 1058 Sum: 5005431) + Executed : 393703 (Average: 12.70 Max: 1058 Sum: 5002242 Ratio: 99.94%) + Bounded : 109 (Average: 29.26 Max: 107 Sum: 3189 Ratio: 0.06%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 676714 (Eliminated: 0 Frozen: 212515) +Constraints : 5006944 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 834MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.08s +Memory: 770MB (+0MB) +UNKNOWN +Iteration Time: 8.13s + +Iteration 53 +Queue: [(20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 54 +Time : 404.039s (Solving: 381.24s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 404.056s + +Choices : 5776284 (Domain: 5621085) +Conflicts : 401720 (Analyzed: 401717) +Restarts : 4943 (Average: 81.27 Last: 199) +Model-Level : 148.0 +Problems : 54 (Average Length: 72.19 Splits: 0) +Lemmas : 401717 (Deleted: 367390) + Binary : 9431 (Ratio: 2.35%) + Ternary : 3503 (Ratio: 0.87%) + Conflict : 401717 (Average Length: 441.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 401717 (Average: 12.58 Max: 1058 Sum: 5053258) + Executed : 401607 (Average: 12.57 Max: 1058 Sum: 5049962 Ratio: 99.93%) + Bounded : 110 (Average: 29.96 Max: 107 Sum: 3296 Ratio: 0.07%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 676714 (Eliminated: 0 Frozen: 212515) +Constraints : 5006944 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 834MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.01s +Memory: 770MB (+0MB) +UNKNOWN +Iteration Time: 8.06s + +Iteration 54 +Queue: [(21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 55 +Time : 411.421s (Solving: 388.49s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 411.440s + +Choices : 5860546 (Domain: 5705341) +Conflicts : 409665 (Analyzed: 409662) +Restarts : 5043 (Average: 81.23 Last: 199) +Model-Level : 148.0 +Problems : 55 (Average Length: 72.82 Splits: 0) +Lemmas : 409662 (Deleted: 375188) + Binary : 9463 (Ratio: 2.31%) + Ternary : 3508 (Ratio: 0.86%) + Conflict : 409662 (Average Length: 443.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 409662 (Average: 12.49 Max: 1058 Sum: 5117575) + Executed : 409551 (Average: 12.48 Max: 1058 Sum: 5114172 Ratio: 99.93%) + Bounded : 111 (Average: 30.66 Max: 107 Sum: 3403 Ratio: 0.07%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 676714 (Eliminated: 0 Frozen: 212515) +Constraints : 5006930 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 834MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.34s +Memory: 770MB (+0MB) +UNKNOWN +Iteration Time: 7.39s + +Iteration 55 +Queue: [(22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Expected Memory: 842.0MB +Grounding... [('step', [106]), ('step', [107]), ('step', [108]), ('step', [109]), ('step', [110]), ('check', [110])] +Grounding Time: 0.49s +Memory: 770MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 56 +Time : 423.459s (Solving: 399.46s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 423.480s + +Choices : 6095255 (Domain: 5938570) +Conflicts : 417514 (Analyzed: 417511) +Restarts : 5143 (Average: 81.18 Last: 199) +Model-Level : 148.0 +Problems : 56 (Average Length: 73.52 Splits: 0) +Lemmas : 417511 (Deleted: 382970) + Binary : 9683 (Ratio: 2.32%) + Ternary : 3582 (Ratio: 0.86%) + Conflict : 417511 (Average Length: 453.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 417511 (Average: 12.74 Max: 1058 Sum: 5319045) + Executed : 417400 (Average: 12.73 Max: 1058 Sum: 5315642 Ratio: 99.94%) + Bounded : 111 (Average: 30.66 Max: 107 Sum: 3403 Ratio: 0.06%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 709660 (Eliminated: 0 Frozen: 222950) +Constraints : 5256489 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 876MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 11.10s +Memory: 802MB (+32MB) +UNKNOWN +Iteration Time: 12.05s + +Iteration 56 +Queue: [(23,115,0,True)] +Grounded Until: 110 +Expected Memory: 874.0MB +Grounding... [('step', [111]), ('step', [112]), ('step', [113]), ('step', [114]), ('step', [115]), ('check', [115])] +Grounding Time: 0.80s +Memory: 853MB (+51MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 57 +Time : 433.449s (Solving: 408.05s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 433.472s + +Choices : 6169695 (Domain: 6013009) +Conflicts : 425778 (Analyzed: 425775) +Restarts : 5243 (Average: 81.21 Last: 199) +Model-Level : 148.0 +Problems : 57 (Average Length: 74.28 Splits: 0) +Lemmas : 425775 (Deleted: 390387) + Binary : 9704 (Ratio: 2.28%) + Ternary : 3584 (Ratio: 0.84%) + Conflict : 425775 (Average Length: 453.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 425775 (Average: 12.62 Max: 1058 Sum: 5372357) + Executed : 425664 (Average: 12.61 Max: 1058 Sum: 5368954 Ratio: 99.94%) + Bounded : 111 (Average: 30.66 Max: 107 Sum: 3403 Ratio: 0.06%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 742606 (Eliminated: 0 Frozen: 233385) +Constraints : 5506074 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 943MB +Max. Length : 110 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.73s +Memory: 857MB (+4MB) +UNKNOWN +Iteration Time: 10.00s + +Iteration 57 +Queue: [(4,20,4,True), (5,25,4,True), (6,30,4,True), (7,35,3,True), (8,40,3,True), (9,45,3,True), (10,50,3,True), (11,55,3,False), (12,60,3,False), (13,65,3,False), (14,70,2,True), (15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,1,True), (23,115,1,True)] +Grounded Until: 115 +Blocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 58 +Time : 438.137s (Solving: 412.59s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 438.164s + +Choices : 6202218 (Domain: 6045532) +Conflicts : 433386 (Analyzed: 433383) +Restarts : 5343 (Average: 81.11 Last: 199) +Model-Level : 148.0 +Problems : 58 (Average Length: 75.02 Splits: 0) +Lemmas : 433383 (Deleted: 398473) + Binary : 9732 (Ratio: 2.25%) + Ternary : 3589 (Ratio: 0.83%) + Conflict : 433383 (Average Length: 451.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 433383 (Average: 12.46 Max: 1058 Sum: 5399873) + Executed : 433271 (Average: 12.45 Max: 1058 Sum: 5396353 Ratio: 99.93%) + Bounded : 112 (Average: 31.43 Max: 117 Sum: 3520 Ratio: 0.07%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 742606 (Eliminated: 0 Frozen: 233385) +Constraints : 5506074 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 943MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 4.64s +Memory: 857MB (+0MB) +UNKNOWN +Iteration Time: 4.69s + +Iteration 58 +Queue: [(5,25,4,True), (6,30,4,True), (7,35,3,True), (8,40,3,True), (9,45,3,True), (10,50,3,True), (11,55,3,False), (12,60,3,False), (13,65,3,False), (14,70,2,True), (15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,1,True), (23,115,1,True)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 59 +Time : 444.999s (Solving: 419.29s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 445.028s + +Choices : 6240550 (Domain: 6083864) +Conflicts : 441543 (Analyzed: 441540) +Restarts : 5443 (Average: 81.12 Last: 199) +Model-Level : 148.0 +Problems : 59 (Average Length: 75.73 Splits: 0) +Lemmas : 441540 (Deleted: 405905) + Binary : 9761 (Ratio: 2.21%) + Ternary : 3592 (Ratio: 0.81%) + Conflict : 441540 (Average Length: 450.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 441540 (Average: 12.30 Max: 1058 Sum: 5431406) + Executed : 441428 (Average: 12.29 Max: 1058 Sum: 5427886 Ratio: 99.94%) + Bounded : 112 (Average: 31.43 Max: 117 Sum: 3520 Ratio: 0.06%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 742606 (Eliminated: 0 Frozen: 233385) +Constraints : 5506061 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 943MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.81s +Memory: 857MB (+0MB) +UNKNOWN +Iteration Time: 6.87s + +Iteration 59 +Queue: [(6,30,4,True), (7,35,3,True), (8,40,3,True), (9,45,3,True), (10,50,3,True), (11,55,3,False), (12,60,3,False), (13,65,3,False), (14,70,2,True), (15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,1,True), (23,115,1,True)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 60 +Time : 451.503s (Solving: 425.65s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 451.536s + +Choices : 6302523 (Domain: 6145837) +Conflicts : 449969 (Analyzed: 449966) +Restarts : 5543 (Average: 81.18 Last: 199) +Model-Level : 148.0 +Problems : 60 (Average Length: 76.42 Splits: 0) +Lemmas : 449966 (Deleted: 413770) + Binary : 9826 (Ratio: 2.18%) + Ternary : 3606 (Ratio: 0.80%) + Conflict : 449966 (Average Length: 453.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 449966 (Average: 12.18 Max: 1058 Sum: 5482244) + Executed : 449854 (Average: 12.18 Max: 1058 Sum: 5478724 Ratio: 99.94%) + Bounded : 112 (Average: 31.43 Max: 117 Sum: 3520 Ratio: 0.06%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 742606 (Eliminated: 0 Frozen: 233385) +Constraints : 5506061 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 943MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.46s +Memory: 857MB (+0MB) +UNKNOWN +Iteration Time: 6.51s + +Iteration 60 +Queue: [(7,35,3,True), (8,40,3,True), (9,45,3,True), (10,50,3,True), (11,55,3,False), (12,60,3,False), (13,65,3,False), (14,70,2,True), (15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,1,True), (23,115,1,True)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 61 +Time : 459.521s (Solving: 433.50s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 459.560s + +Choices : 6368446 (Domain: 6211751) +Conflicts : 458324 (Analyzed: 458321) +Restarts : 5643 (Average: 81.22 Last: 199) +Model-Level : 148.0 +Problems : 61 (Average Length: 77.08 Splits: 0) +Lemmas : 458321 (Deleted: 421968) + Binary : 9920 (Ratio: 2.16%) + Ternary : 3614 (Ratio: 0.79%) + Conflict : 458321 (Average Length: 468.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 458321 (Average: 12.06 Max: 1058 Sum: 5528485) + Executed : 458209 (Average: 12.05 Max: 1058 Sum: 5524965 Ratio: 99.94%) + Bounded : 112 (Average: 31.43 Max: 117 Sum: 3520 Ratio: 0.06%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 742606 (Eliminated: 0 Frozen: 233385) +Constraints : 5506061 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 943MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.96s +Memory: 857MB (+0MB) +UNKNOWN +Iteration Time: 8.02s + +Iteration 61 +Queue: [(8,40,3,True), (9,45,3,True), (10,50,3,True), (11,55,3,False), (12,60,3,False), (13,65,3,False), (14,70,2,True), (15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,1,True), (23,115,1,True)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 62 +Time : 467.796s (Solving: 441.63s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 467.840s + +Choices : 6423923 (Domain: 6267183) +Conflicts : 466042 (Analyzed: 466039) +Restarts : 5743 (Average: 81.15 Last: 199) +Model-Level : 148.0 +Problems : 62 (Average Length: 77.73 Splits: 0) +Lemmas : 466039 (Deleted: 430119) + Binary : 9967 (Ratio: 2.14%) + Ternary : 3621 (Ratio: 0.78%) + Conflict : 466039 (Average Length: 486.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 466039 (Average: 11.93 Max: 1058 Sum: 5560681) + Executed : 465927 (Average: 11.92 Max: 1058 Sum: 5557161 Ratio: 99.94%) + Bounded : 112 (Average: 31.43 Max: 117 Sum: 3520 Ratio: 0.06%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 742606 (Eliminated: 0 Frozen: 233385) +Constraints : 5506061 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 943MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.23s +Memory: 857MB (+0MB) +UNKNOWN +Iteration Time: 8.28s + +Iteration 62 +Queue: [(9,45,3,True), (10,50,3,True), (11,55,3,False), (12,60,3,False), (13,65,3,False), (14,70,2,True), (15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,1,True), (23,115,1,True)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 63 +Time : 473.874s (Solving: 447.55s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 473.920s + +Choices : 6483121 (Domain: 6325618) +Conflicts : 473770 (Analyzed: 473767) +Restarts : 5843 (Average: 81.08 Last: 199) +Model-Level : 148.0 +Problems : 63 (Average Length: 78.35 Splits: 0) +Lemmas : 473767 (Deleted: 437651) + Binary : 10000 (Ratio: 2.11%) + Ternary : 3626 (Ratio: 0.77%) + Conflict : 473767 (Average Length: 486.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 473767 (Average: 11.83 Max: 1058 Sum: 5606098) + Executed : 473655 (Average: 11.83 Max: 1058 Sum: 5602578 Ratio: 99.94%) + Bounded : 112 (Average: 31.43 Max: 117 Sum: 3520 Ratio: 0.06%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 742606 (Eliminated: 0 Frozen: 233385) +Constraints : 5506061 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 943MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.03s +Memory: 857MB (+0MB) +UNKNOWN +Iteration Time: 6.08s + +Iteration 63 +Queue: [(10,50,3,True), (11,55,3,False), (12,60,3,False), (13,65,3,False), (14,70,2,True), (15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,1,True), (23,115,1,True)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 64 +Time : 481.677s (Solving: 455.16s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 481.724s + +Choices : 6569867 (Domain: 6412264) +Conflicts : 482429 (Analyzed: 482426) +Restarts : 5943 (Average: 81.18 Last: 199) +Model-Level : 148.0 +Problems : 64 (Average Length: 78.95 Splits: 0) +Lemmas : 482426 (Deleted: 447280) + Binary : 10091 (Ratio: 2.09%) + Ternary : 3643 (Ratio: 0.76%) + Conflict : 482426 (Average Length: 493.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 482426 (Average: 11.76 Max: 1058 Sum: 5673538) + Executed : 482314 (Average: 11.75 Max: 1058 Sum: 5670018 Ratio: 99.94%) + Bounded : 112 (Average: 31.43 Max: 117 Sum: 3520 Ratio: 0.06%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 742606 (Eliminated: 0 Frozen: 233385) +Constraints : 5506061 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 943MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.73s +Memory: 857MB (+0MB) +UNKNOWN +Iteration Time: 7.81s + +Iteration 64 +Queue: [(14,70,2,True), (15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,1,True), (23,115,1,True)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 65 +Time : 490.031s (Solving: 463.35s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 490.080s + +Choices : 6660411 (Domain: 6502426) +Conflicts : 490907 (Analyzed: 490904) +Restarts : 6043 (Average: 81.24 Last: 199) +Model-Level : 148.0 +Problems : 65 (Average Length: 79.54 Splits: 0) +Lemmas : 490904 (Deleted: 453451) + Binary : 10187 (Ratio: 2.08%) + Ternary : 3671 (Ratio: 0.75%) + Conflict : 490904 (Average Length: 499.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 490904 (Average: 11.69 Max: 1058 Sum: 5741051) + Executed : 490792 (Average: 11.69 Max: 1058 Sum: 5737531 Ratio: 99.94%) + Bounded : 112 (Average: 31.43 Max: 117 Sum: 3520 Ratio: 0.06%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 742606 (Eliminated: 0 Frozen: 233385) +Constraints : 5506061 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 943MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.30s +Memory: 857MB (+0MB) +UNKNOWN +Iteration Time: 8.36s + +Iteration 65 +Queue: [(15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,1,True), (23,115,1,True)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 66 +Time : 498.612s (Solving: 471.77s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 498.656s + +Choices : 6750029 (Domain: 6590608) +Conflicts : 499206 (Analyzed: 499203) +Restarts : 6143 (Average: 81.26 Last: 199) +Model-Level : 148.0 +Problems : 66 (Average Length: 80.11 Splits: 0) +Lemmas : 499203 (Deleted: 461699) + Binary : 10243 (Ratio: 2.05%) + Ternary : 3694 (Ratio: 0.74%) + Conflict : 499203 (Average Length: 498.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 499203 (Average: 11.64 Max: 1058 Sum: 5812823) + Executed : 499090 (Average: 11.64 Max: 1058 Sum: 5809186 Ratio: 99.94%) + Bounded : 113 (Average: 32.19 Max: 117 Sum: 3637 Ratio: 0.06%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 742606 (Eliminated: 0 Frozen: 233385) +Constraints : 5506061 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 943MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.52s +Memory: 857MB (+0MB) +UNKNOWN +Iteration Time: 8.58s + +Iteration 66 +Queue: [(22,110,1,True), (23,115,1,True)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 67 +Time : 508.112s (Solving: 481.12s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 508.160s + +Choices : 6838515 (Domain: 6679092) +Conflicts : 507401 (Analyzed: 507398) +Restarts : 6243 (Average: 81.27 Last: 199) +Model-Level : 148.0 +Problems : 67 (Average Length: 80.66 Splits: 0) +Lemmas : 507398 (Deleted: 469898) + Binary : 10285 (Ratio: 2.03%) + Ternary : 3703 (Ratio: 0.73%) + Conflict : 507398 (Average Length: 502.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 507398 (Average: 11.57 Max: 1058 Sum: 5872503) + Executed : 507285 (Average: 11.57 Max: 1058 Sum: 5868866 Ratio: 99.94%) + Bounded : 113 (Average: 32.19 Max: 117 Sum: 3637 Ratio: 0.06%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 742606 (Eliminated: 0 Frozen: 233385) +Constraints : 5506047 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 943MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.45s +Memory: 857MB (+0MB) +UNKNOWN +Iteration Time: 9.51s + +Iteration 67 +Queue: [(23,115,1,True)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 68 +Time : 516.589s (Solving: 489.41s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 516.640s + +Choices : 6927122 (Domain: 6767680) +Conflicts : 515786 (Analyzed: 515783) +Restarts : 6343 (Average: 81.32 Last: 199) +Model-Level : 148.0 +Problems : 68 (Average Length: 81.19 Splits: 0) +Lemmas : 515783 (Deleted: 477840) + Binary : 10306 (Ratio: 2.00%) + Ternary : 3717 (Ratio: 0.72%) + Conflict : 515783 (Average Length: 503.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 515783 (Average: 11.51 Max: 1058 Sum: 5938286) + Executed : 515670 (Average: 11.51 Max: 1058 Sum: 5934649 Ratio: 99.94%) + Bounded : 113 (Average: 32.19 Max: 117 Sum: 3637 Ratio: 0.06%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 742606 (Eliminated: 0 Frozen: 233385) +Constraints : 5506047 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 943MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.41s +Memory: 857MB (+0MB) +UNKNOWN +Iteration Time: 8.48s + +Iteration 68 +Queue: [(4,20,5,True), (5,25,5,True), (6,30,5,True), (7,35,4,True), (8,40,4,True), (9,45,4,True), (10,50,4,False), (11,55,3,True), (12,60,3,True), (13,65,3,False), (14,70,3,False), (15,75,3,False), (16,80,2,True), (17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Blocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 69 +Time : 521.638s (Solving: 494.29s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 521.688s + +Choices : 6972117 (Domain: 6812675) +Conflicts : 523446 (Analyzed: 523443) +Restarts : 6443 (Average: 81.24 Last: 199) +Model-Level : 148.0 +Problems : 69 (Average Length: 81.71 Splits: 0) +Lemmas : 523443 (Deleted: 486016) + Binary : 10394 (Ratio: 1.99%) + Ternary : 3727 (Ratio: 0.71%) + Conflict : 523443 (Average Length: 501.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 523443 (Average: 11.42 Max: 1058 Sum: 5977673) + Executed : 523330 (Average: 11.41 Max: 1058 Sum: 5974036 Ratio: 99.94%) + Bounded : 113 (Average: 32.19 Max: 117 Sum: 3637 Ratio: 0.06%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 742606 (Eliminated: 0 Frozen: 233385) +Constraints : 5506047 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 943MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 4.99s +Memory: 857MB (+0MB) +UNKNOWN +Iteration Time: 5.05s + +Iteration 69 +Queue: [(5,25,5,True), (6,30,5,True), (7,35,4,True), (8,40,4,True), (9,45,4,True), (10,50,4,False), (11,55,3,True), (12,60,3,True), (13,65,3,False), (14,70,3,False), (15,75,3,False), (16,80,2,True), (17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 70 +Time : 532.270s (Solving: 504.74s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 532.324s + +Choices : 7024016 (Domain: 6864574) +Conflicts : 532564 (Analyzed: 532561) +Restarts : 6543 (Average: 81.39 Last: 199) +Model-Level : 148.0 +Problems : 70 (Average Length: 82.21 Splits: 0) +Lemmas : 532561 (Deleted: 495546) + Binary : 10420 (Ratio: 1.96%) + Ternary : 3730 (Ratio: 0.70%) + Conflict : 532561 (Average Length: 510.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 532561 (Average: 11.30 Max: 1058 Sum: 6017997) + Executed : 532448 (Average: 11.29 Max: 1058 Sum: 6014360 Ratio: 99.94%) + Bounded : 113 (Average: 32.19 Max: 117 Sum: 3637 Ratio: 0.06%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 742606 (Eliminated: 0 Frozen: 233385) +Constraints : 5506047 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 943MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 10.57s +Memory: 857MB (+0MB) +UNKNOWN +Iteration Time: 10.64s + +Iteration 70 +Queue: [(6,30,5,True), (7,35,4,True), (8,40,4,True), (9,45,4,True), (10,50,4,False), (11,55,3,True), (12,60,3,True), (13,65,3,False), (14,70,3,False), (15,75,3,False), (16,80,2,True), (17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 71 +Time : 539.480s (Solving: 511.78s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 539.536s + +Choices : 7075739 (Domain: 6916297) +Conflicts : 541125 (Analyzed: 541122) +Restarts : 6643 (Average: 81.46 Last: 199) +Model-Level : 148.0 +Problems : 71 (Average Length: 82.70 Splits: 0) +Lemmas : 541122 (Deleted: 502319) + Binary : 10467 (Ratio: 1.93%) + Ternary : 3744 (Ratio: 0.69%) + Conflict : 541122 (Average Length: 509.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 541122 (Average: 11.20 Max: 1058 Sum: 6058554) + Executed : 541009 (Average: 11.19 Max: 1058 Sum: 6054917 Ratio: 99.94%) + Bounded : 113 (Average: 32.19 Max: 117 Sum: 3637 Ratio: 0.06%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 742606 (Eliminated: 0 Frozen: 233385) +Constraints : 5506047 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 943MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.15s +Memory: 857MB (+0MB) +UNKNOWN +Iteration Time: 7.22s + +Iteration 71 +Queue: [(7,35,4,True), (8,40,4,True), (9,45,4,True), (10,50,4,False), (11,55,3,True), (12,60,3,True), (13,65,3,False), (14,70,3,False), (15,75,3,False), (16,80,2,True), (17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 72 +Time : 546.729s (Solving: 518.88s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 546.788s + +Choices : 7141225 (Domain: 6981783) +Conflicts : 549648 (Analyzed: 549645) +Restarts : 6743 (Average: 81.51 Last: 199) +Model-Level : 148.0 +Problems : 72 (Average Length: 83.18 Splits: 0) +Lemmas : 549645 (Deleted: 510685) + Binary : 10534 (Ratio: 1.92%) + Ternary : 3757 (Ratio: 0.68%) + Conflict : 549645 (Average Length: 516.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 549645 (Average: 11.11 Max: 1058 Sum: 6104837) + Executed : 549532 (Average: 11.10 Max: 1058 Sum: 6101200 Ratio: 99.94%) + Bounded : 113 (Average: 32.19 Max: 117 Sum: 3637 Ratio: 0.06%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 742606 (Eliminated: 0 Frozen: 233385) +Constraints : 5506047 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 943MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.20s +Memory: 857MB (+0MB) +UNKNOWN +Iteration Time: 7.25s + +Iteration 72 +Queue: [(8,40,4,True), (9,45,4,True), (10,50,4,False), (11,55,3,True), (12,60,3,True), (13,65,3,False), (14,70,3,False), (15,75,3,False), (16,80,2,True), (17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 73 +Time : 555.168s (Solving: 527.13s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 555.232s + +Choices : 7224004 (Domain: 7063798) +Conflicts : 557776 (Analyzed: 557773) +Restarts : 6843 (Average: 81.51 Last: 199) +Model-Level : 148.0 +Problems : 73 (Average Length: 83.64 Splits: 0) +Lemmas : 557773 (Deleted: 518948) + Binary : 10660 (Ratio: 1.91%) + Ternary : 3779 (Ratio: 0.68%) + Conflict : 557773 (Average Length: 526.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 557773 (Average: 11.05 Max: 1058 Sum: 6165088) + Executed : 557660 (Average: 11.05 Max: 1058 Sum: 6161451 Ratio: 99.94%) + Bounded : 113 (Average: 32.19 Max: 117 Sum: 3637 Ratio: 0.06%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 742606 (Eliminated: 0 Frozen: 233385) +Constraints : 5506047 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 943MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.37s +Memory: 857MB (+0MB) +UNKNOWN +Iteration Time: 8.44s + +Iteration 73 +Queue: [(9,45,4,True), (10,50,4,False), (11,55,3,True), (12,60,3,True), (13,65,3,False), (14,70,3,False), (15,75,3,False), (16,80,2,True), (17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 74 +Time : 561.209s (Solving: 533.00s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 561.280s + +Choices : 7285602 (Domain: 7125365) +Conflicts : 565760 (Analyzed: 565757) +Restarts : 6943 (Average: 81.49 Last: 199) +Model-Level : 148.0 +Problems : 74 (Average Length: 84.09 Splits: 0) +Lemmas : 565757 (Deleted: 526870) + Binary : 10682 (Ratio: 1.89%) + Ternary : 3786 (Ratio: 0.67%) + Conflict : 565757 (Average Length: 530.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 565757 (Average: 10.98 Max: 1058 Sum: 6211042) + Executed : 565644 (Average: 10.97 Max: 1058 Sum: 6207405 Ratio: 99.94%) + Bounded : 113 (Average: 32.19 Max: 117 Sum: 3637 Ratio: 0.06%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 742606 (Eliminated: 0 Frozen: 233385) +Constraints : 5506047 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 943MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 5.98s +Memory: 857MB (+0MB) +UNKNOWN +Iteration Time: 6.05s + +Iteration 74 +Queue: [(11,55,3,True), (12,60,3,True), (13,65,3,False), (14,70,3,False), (15,75,3,False), (16,80,2,True), (17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 75 +Time : 567.239s (Solving: 538.86s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 567.312s + +Choices : 7351056 (Domain: 7190796) +Conflicts : 573593 (Analyzed: 573590) +Restarts : 7043 (Average: 81.44 Last: 199) +Model-Level : 148.0 +Problems : 75 (Average Length: 84.53 Splits: 0) +Lemmas : 573590 (Deleted: 534658) + Binary : 10689 (Ratio: 1.86%) + Ternary : 3793 (Ratio: 0.66%) + Conflict : 573590 (Average Length: 532.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 573590 (Average: 10.92 Max: 1058 Sum: 6261502) + Executed : 573477 (Average: 10.91 Max: 1058 Sum: 6257865 Ratio: 99.94%) + Bounded : 113 (Average: 32.19 Max: 117 Sum: 3637 Ratio: 0.06%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 742606 (Eliminated: 0 Frozen: 233385) +Constraints : 5506047 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 943MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 5.97s +Memory: 857MB (+0MB) +UNKNOWN +Iteration Time: 6.03s + +Iteration 75 +Queue: [(12,60,3,True), (13,65,3,False), (14,70,3,False), (15,75,3,False), (16,80,2,True), (17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 76 +Time : 573.962s (Solving: 545.41s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 574.036s + +Choices : 7423032 (Domain: 7262757) +Conflicts : 582261 (Analyzed: 582258) +Restarts : 7143 (Average: 81.51 Last: 199) +Model-Level : 148.0 +Problems : 76 (Average Length: 84.96 Splits: 0) +Lemmas : 582258 (Deleted: 544502) + Binary : 10722 (Ratio: 1.84%) + Ternary : 3805 (Ratio: 0.65%) + Conflict : 582258 (Average Length: 536.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 582258 (Average: 10.85 Max: 1058 Sum: 6315671) + Executed : 582145 (Average: 10.84 Max: 1058 Sum: 6312034 Ratio: 99.94%) + Bounded : 113 (Average: 32.19 Max: 117 Sum: 3637 Ratio: 0.06%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 742606 (Eliminated: 0 Frozen: 233385) +Constraints : 5506047 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 943MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.66s +Memory: 857MB (+0MB) +UNKNOWN +Iteration Time: 6.73s + +Iteration 76 +Queue: [(16,80,2,True), (17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 77 +Time : 583.396s (Solving: 554.68s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 583.472s + +Choices : 7546732 (Domain: 7386230) +Conflicts : 590685 (Analyzed: 590682) +Restarts : 7243 (Average: 81.55 Last: 199) +Model-Level : 148.0 +Problems : 77 (Average Length: 85.38 Splits: 0) +Lemmas : 590682 (Deleted: 550812) + Binary : 10855 (Ratio: 1.84%) + Ternary : 3822 (Ratio: 0.65%) + Conflict : 590682 (Average Length: 544.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 590682 (Average: 10.86 Max: 1058 Sum: 6412052) + Executed : 590569 (Average: 10.85 Max: 1058 Sum: 6408415 Ratio: 99.94%) + Bounded : 113 (Average: 32.19 Max: 117 Sum: 3637 Ratio: 0.06%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 742606 (Eliminated: 0 Frozen: 233385) +Constraints : 5506047 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 943MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.38s +Memory: 857MB (+0MB) +UNKNOWN +Iteration Time: 9.44s + +Iteration 77 +Queue: [(17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 78 +Time : 592.007s (Solving: 563.14s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 592.084s + +Choices : 7639224 (Domain: 7478679) +Conflicts : 599022 (Analyzed: 599019) +Restarts : 7343 (Average: 81.58 Last: 199) +Model-Level : 148.0 +Problems : 78 (Average Length: 85.78 Splits: 0) +Lemmas : 599019 (Deleted: 558937) + Binary : 10897 (Ratio: 1.82%) + Ternary : 3833 (Ratio: 0.64%) + Conflict : 599019 (Average Length: 545.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 599019 (Average: 10.82 Max: 1058 Sum: 6483134) + Executed : 598906 (Average: 10.82 Max: 1058 Sum: 6479497 Ratio: 99.94%) + Bounded : 113 (Average: 32.19 Max: 117 Sum: 3637 Ratio: 0.06%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 742606 (Eliminated: 0 Frozen: 233385) +Constraints : 5506047 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 943MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.56s +Memory: 857MB (+0MB) +UNKNOWN +Iteration Time: 8.62s + +Iteration 78 +Queue: [(4,20,6,True), (5,25,6,True), (6,30,6,True), (7,35,5,True), (8,40,5,True), (9,45,5,False), (10,50,4,True), (11,55,4,False), (12,60,4,False), (13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,3,False), (17,85,3,False), (18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Blocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 79 +Time : 598.408s (Solving: 569.37s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 598.488s + +Choices : 7701168 (Domain: 7540622) +Conflicts : 606830 (Analyzed: 606827) +Restarts : 7443 (Average: 81.53 Last: 199) +Model-Level : 148.0 +Problems : 79 (Average Length: 86.18 Splits: 0) +Lemmas : 606827 (Deleted: 567084) + Binary : 10970 (Ratio: 1.81%) + Ternary : 3849 (Ratio: 0.63%) + Conflict : 606827 (Average Length: 545.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 606827 (Average: 10.77 Max: 1058 Sum: 6536396) + Executed : 606714 (Average: 10.77 Max: 1058 Sum: 6532759 Ratio: 99.94%) + Bounded : 113 (Average: 32.19 Max: 117 Sum: 3637 Ratio: 0.06%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 742606 (Eliminated: 0 Frozen: 233385) +Constraints : 5506047 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 943MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.34s +Memory: 857MB (+0MB) +UNKNOWN +Iteration Time: 6.41s + +Iteration 79 +Queue: [(5,25,6,True), (6,30,6,True), (7,35,5,True), (8,40,5,True), (9,45,5,False), (10,50,4,True), (11,55,4,False), (12,60,4,False), (13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,3,False), (17,85,3,False), (18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 80 +Time : 607.848s (Solving: 578.65s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 607.932s + +Choices : 7750646 (Domain: 7590100) +Conflicts : 615547 (Analyzed: 615544) +Restarts : 7543 (Average: 81.60 Last: 199) +Model-Level : 148.0 +Problems : 80 (Average Length: 86.56 Splits: 0) +Lemmas : 615544 (Deleted: 576756) + Binary : 11003 (Ratio: 1.79%) + Ternary : 3854 (Ratio: 0.63%) + Conflict : 615544 (Average Length: 550.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 615544 (Average: 10.68 Max: 1058 Sum: 6575957) + Executed : 615431 (Average: 10.68 Max: 1058 Sum: 6572320 Ratio: 99.94%) + Bounded : 113 (Average: 32.19 Max: 117 Sum: 3637 Ratio: 0.06%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 742606 (Eliminated: 0 Frozen: 233385) +Constraints : 5506047 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 943MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.39s +Memory: 857MB (+0MB) +UNKNOWN +Iteration Time: 9.45s + +Iteration 80 +Queue: [(6,30,6,True), (7,35,5,True), (8,40,5,True), (9,45,5,False), (10,50,4,True), (11,55,4,False), (12,60,4,False), (13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,3,False), (17,85,3,False), (18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 81 +Time : 614.123s (Solving: 584.78s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 614.208s + +Choices : 7804164 (Domain: 7643618) +Conflicts : 623754 (Analyzed: 623751) +Restarts : 7643 (Average: 81.61 Last: 199) +Model-Level : 148.0 +Problems : 81 (Average Length: 86.94 Splits: 0) +Lemmas : 623751 (Deleted: 583195) + Binary : 11019 (Ratio: 1.77%) + Ternary : 3862 (Ratio: 0.62%) + Conflict : 623751 (Average Length: 549.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 623751 (Average: 10.61 Max: 1058 Sum: 6616578) + Executed : 623638 (Average: 10.60 Max: 1058 Sum: 6612941 Ratio: 99.95%) + Bounded : 113 (Average: 32.19 Max: 117 Sum: 3637 Ratio: 0.05%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 742606 (Eliminated: 0 Frozen: 233385) +Constraints : 5506047 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 943MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.23s +Memory: 857MB (+0MB) +UNKNOWN +Iteration Time: 6.28s + +Iteration 81 +Queue: [(7,35,5,True), (8,40,5,True), (9,45,5,False), (10,50,4,True), (11,55,4,False), (12,60,4,False), (13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,3,False), (17,85,3,False), (18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 82 +Time : 622.288s (Solving: 592.78s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 622.380s + +Choices : 7869664 (Domain: 7708891) +Conflicts : 632230 (Analyzed: 632227) +Restarts : 7743 (Average: 81.65 Last: 199) +Model-Level : 148.0 +Problems : 82 (Average Length: 87.30 Splits: 0) +Lemmas : 632227 (Deleted: 591220) + Binary : 11073 (Ratio: 1.75%) + Ternary : 3869 (Ratio: 0.61%) + Conflict : 632227 (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 : 632227 (Average: 10.54 Max: 1058 Sum: 6661979) + Executed : 632114 (Average: 10.53 Max: 1058 Sum: 6658342 Ratio: 99.95%) + Bounded : 113 (Average: 32.19 Max: 117 Sum: 3637 Ratio: 0.05%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 742606 (Eliminated: 0 Frozen: 233385) +Constraints : 5506047 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 943MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.11s +Memory: 857MB (+0MB) +UNKNOWN +Iteration Time: 8.17s + +Iteration 82 +Queue: [(8,40,5,True), (9,45,5,False), (10,50,4,True), (11,55,4,False), (12,60,4,False), (13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,3,False), (17,85,3,False), (18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 83 +Time : 628.508s (Solving: 598.84s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 628.604s + +Choices : 7924346 (Domain: 7763559) +Conflicts : 640076 (Analyzed: 640073) +Restarts : 7843 (Average: 81.61 Last: 199) +Model-Level : 148.0 +Problems : 83 (Average Length: 87.66 Splits: 0) +Lemmas : 640073 (Deleted: 599476) + Binary : 11104 (Ratio: 1.73%) + Ternary : 3891 (Ratio: 0.61%) + Conflict : 640073 (Average Length: 557.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 640073 (Average: 10.48 Max: 1058 Sum: 6705046) + Executed : 639960 (Average: 10.47 Max: 1058 Sum: 6701409 Ratio: 99.95%) + Bounded : 113 (Average: 32.19 Max: 117 Sum: 3637 Ratio: 0.05%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 742606 (Eliminated: 0 Frozen: 233385) +Constraints : 5506047 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 943MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.16s +Memory: 857MB (+0MB) +UNKNOWN +Iteration Time: 6.23s + +Iteration 83 +Queue: [(10,50,4,True), (11,55,4,False), (12,60,4,False), (13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,3,False), (17,85,3,False), (18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 84 +Time : 637.078s (Solving: 607.25s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 637.176s + +Choices : 8001331 (Domain: 7840540) +Conflicts : 648455 (Analyzed: 648452) +Restarts : 7943 (Average: 81.64 Last: 199) +Model-Level : 148.0 +Problems : 84 (Average Length: 88.01 Splits: 0) +Lemmas : 648452 (Deleted: 607111) + Binary : 11153 (Ratio: 1.72%) + Ternary : 3897 (Ratio: 0.60%) + Conflict : 648452 (Average Length: 565.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 648452 (Average: 10.42 Max: 1058 Sum: 6759738) + Executed : 648339 (Average: 10.42 Max: 1058 Sum: 6756101 Ratio: 99.95%) + Bounded : 113 (Average: 32.19 Max: 117 Sum: 3637 Ratio: 0.05%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 742606 (Eliminated: 0 Frozen: 233385) +Constraints : 5506047 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 943MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.52s +Memory: 857MB (+0MB) +UNKNOWN +Iteration Time: 8.58s + +Iteration 84 +Queue: [(13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,3,False), (17,85,3,False), (18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 85 +Time : 645.136s (Solving: 615.13s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 645.236s + +Choices : 8064931 (Domain: 7904133) +Conflicts : 656449 (Analyzed: 656446) +Restarts : 8043 (Average: 81.62 Last: 199) +Model-Level : 148.0 +Problems : 85 (Average Length: 88.35 Splits: 0) +Lemmas : 656446 (Deleted: 615346) + Binary : 11172 (Ratio: 1.70%) + Ternary : 3900 (Ratio: 0.59%) + Conflict : 656446 (Average Length: 565.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 656446 (Average: 10.37 Max: 1058 Sum: 6807063) + Executed : 656333 (Average: 10.36 Max: 1058 Sum: 6803426 Ratio: 99.95%) + Bounded : 113 (Average: 32.19 Max: 117 Sum: 3637 Ratio: 0.05%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 742606 (Eliminated: 0 Frozen: 233385) +Constraints : 5506047 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 943MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.99s +Memory: 857MB (+0MB) +UNKNOWN +Iteration Time: 8.06s + +Iteration 85 +Queue: [(18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 86 +Time : 655.553s (Solving: 625.38s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 655.656s + +Choices : 8162962 (Domain: 8002144) +Conflicts : 664960 (Analyzed: 664957) +Restarts : 8143 (Average: 81.66 Last: 199) +Model-Level : 148.0 +Problems : 86 (Average Length: 88.69 Splits: 0) +Lemmas : 664957 (Deleted: 623180) + Binary : 11209 (Ratio: 1.69%) + Ternary : 3904 (Ratio: 0.59%) + Conflict : 664957 (Average Length: 574.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 664957 (Average: 10.34 Max: 1058 Sum: 6874599) + Executed : 664844 (Average: 10.33 Max: 1058 Sum: 6870962 Ratio: 99.95%) + Bounded : 113 (Average: 32.19 Max: 117 Sum: 3637 Ratio: 0.05%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 742606 (Eliminated: 0 Frozen: 233385) +Constraints : 5506047 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 943MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 10.36s +Memory: 857MB (+0MB) +UNKNOWN +Iteration Time: 10.42s + +Iteration 86 +Queue: [(4,20,7,True), (5,25,7,True), (6,30,7,False), (7,35,6,True), (8,40,6,False), (9,45,5,True), (10,50,5,False), (11,55,4,True), (12,60,4,False), (13,65,4,False), (14,70,3,True), (15,75,3,True), (16,80,3,False), (17,85,3,False), (18,90,3,False), (19,95,2,True), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Blocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 87 +Time : 660.441s (Solving: 630.07s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 660.544s + +Choices : 8213787 (Domain: 8052969) +Conflicts : 672654 (Analyzed: 672651) +Restarts : 8243 (Average: 81.60 Last: 199) +Model-Level : 148.0 +Problems : 87 (Average Length: 89.01 Splits: 0) +Lemmas : 672651 (Deleted: 631493) + Binary : 11263 (Ratio: 1.67%) + Ternary : 3911 (Ratio: 0.58%) + Conflict : 672651 (Average Length: 575.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 672651 (Average: 10.28 Max: 1058 Sum: 6917793) + Executed : 672537 (Average: 10.28 Max: 1058 Sum: 6914039 Ratio: 99.95%) + Bounded : 114 (Average: 32.93 Max: 117 Sum: 3754 Ratio: 0.05%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 742606 (Eliminated: 0 Frozen: 233385) +Constraints : 5506047 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 943MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 4.81s +Memory: 857MB (+0MB) +UNKNOWN +Iteration Time: 4.89s + +Iteration 87 +Queue: [(5,25,7,True), (6,30,7,False), (7,35,6,True), (8,40,6,False), (9,45,5,True), (10,50,5,False), (11,55,4,True), (12,60,4,False), (13,65,4,False), (14,70,3,True), (15,75,3,True), (16,80,3,False), (17,85,3,False), (18,90,3,False), (19,95,2,True), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 88 +Time : 670.337s (Solving: 639.78s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 670.444s + +Choices : 8255021 (Domain: 8094203) +Conflicts : 681563 (Analyzed: 681560) +Restarts : 8343 (Average: 81.69 Last: 199) +Model-Level : 148.0 +Problems : 88 (Average Length: 89.33 Splits: 0) +Lemmas : 681560 (Deleted: 641187) + Binary : 11282 (Ratio: 1.66%) + Ternary : 3915 (Ratio: 0.57%) + Conflict : 681560 (Average Length: 582.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 681560 (Average: 10.20 Max: 1058 Sum: 6948663) + Executed : 681446 (Average: 10.19 Max: 1058 Sum: 6944909 Ratio: 99.95%) + Bounded : 114 (Average: 32.93 Max: 117 Sum: 3754 Ratio: 0.05%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 742606 (Eliminated: 0 Frozen: 233385) +Constraints : 5506021 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 943MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.83s +Memory: 857MB (+0MB) +UNKNOWN +Iteration Time: 9.90s + +Iteration 88 +Queue: [(7,35,6,True), (8,40,6,False), (9,45,5,True), (10,50,5,False), (11,55,4,True), (12,60,4,False), (13,65,4,False), (14,70,3,True), (15,75,3,True), (16,80,3,False), (17,85,3,False), (18,90,3,False), (19,95,2,True), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 89 +Time : 677.573s (Solving: 646.85s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 677.684s + +Choices : 8313740 (Domain: 8152922) +Conflicts : 689779 (Analyzed: 689776) +Restarts : 8443 (Average: 81.70 Last: 199) +Model-Level : 148.0 +Problems : 89 (Average Length: 89.64 Splits: 0) +Lemmas : 689776 (Deleted: 647830) + Binary : 11326 (Ratio: 1.64%) + Ternary : 3920 (Ratio: 0.57%) + Conflict : 689776 (Average Length: 586.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 689776 (Average: 10.13 Max: 1058 Sum: 6988292) + Executed : 689662 (Average: 10.13 Max: 1058 Sum: 6984538 Ratio: 99.95%) + Bounded : 114 (Average: 32.93 Max: 117 Sum: 3754 Ratio: 0.05%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 742606 (Eliminated: 0 Frozen: 233385) +Constraints : 5506021 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 943MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.18s +Memory: 857MB (+0MB) +UNKNOWN +Iteration Time: 7.24s + +Iteration 89 +Queue: [(9,45,5,True), (10,50,5,False), (11,55,4,True), (12,60,4,False), (13,65,4,False), (14,70,3,True), (15,75,3,True), (16,80,3,False), (17,85,3,False), (18,90,3,False), (19,95,2,True), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 90 +Time : 684.716s (Solving: 653.83s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 684.832s + +Choices : 8377164 (Domain: 8216341) +Conflicts : 698142 (Analyzed: 698139) +Restarts : 8543 (Average: 81.72 Last: 199) +Model-Level : 148.0 +Problems : 90 (Average Length: 89.94 Splits: 0) +Lemmas : 698139 (Deleted: 655884) + Binary : 11352 (Ratio: 1.63%) + Ternary : 3924 (Ratio: 0.56%) + Conflict : 698139 (Average Length: 587.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 698139 (Average: 10.08 Max: 1058 Sum: 7038067) + Executed : 698025 (Average: 10.08 Max: 1058 Sum: 7034313 Ratio: 99.95%) + Bounded : 114 (Average: 32.93 Max: 117 Sum: 3754 Ratio: 0.05%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 742606 (Eliminated: 0 Frozen: 233385) +Constraints : 5506021 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 943MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.09s +Memory: 857MB (+0MB) +UNKNOWN +Iteration Time: 7.15s + +Iteration 90 +Queue: [(11,55,4,True), (12,60,4,False), (13,65,4,False), (14,70,3,True), (15,75,3,True), (16,80,3,False), (17,85,3,False), (18,90,3,False), (19,95,2,True), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 91 +Time : 692.954s (Solving: 661.89s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 693.076s + +Choices : 8443070 (Domain: 8282247) +Conflicts : 706403 (Analyzed: 706400) +Restarts : 8643 (Average: 81.73 Last: 199) +Model-Level : 148.0 +Problems : 91 (Average Length: 90.24 Splits: 0) +Lemmas : 706400 (Deleted: 664086) + Binary : 11374 (Ratio: 1.61%) + Ternary : 3926 (Ratio: 0.56%) + Conflict : 706400 (Average Length: 586.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 706400 (Average: 10.03 Max: 1058 Sum: 7088156) + Executed : 706286 (Average: 10.03 Max: 1058 Sum: 7084402 Ratio: 99.95%) + Bounded : 114 (Average: 32.93 Max: 117 Sum: 3754 Ratio: 0.05%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 742606 (Eliminated: 0 Frozen: 233385) +Constraints : 5506021 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 943MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.18s +Memory: 857MB (+0MB) +UNKNOWN +Iteration Time: 8.24s + +Iteration 91 +Queue: [(14,70,3,True), (15,75,3,True), (16,80,3,False), (17,85,3,False), (18,90,3,False), (19,95,2,True), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 92 +Time : 701.785s (Solving: 670.54s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 701.908s + +Choices : 8518957 (Domain: 8358110) +Conflicts : 714658 (Analyzed: 714655) +Restarts : 8743 (Average: 81.74 Last: 199) +Model-Level : 148.0 +Problems : 92 (Average Length: 90.53 Splits: 0) +Lemmas : 714655 (Deleted: 672195) + Binary : 11403 (Ratio: 1.60%) + Ternary : 3935 (Ratio: 0.55%) + Conflict : 714655 (Average Length: 588.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 714655 (Average: 10.00 Max: 1058 Sum: 7144264) + Executed : 714541 (Average: 9.99 Max: 1058 Sum: 7140510 Ratio: 99.95%) + Bounded : 114 (Average: 32.93 Max: 117 Sum: 3754 Ratio: 0.05%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 742606 (Eliminated: 0 Frozen: 233385) +Constraints : 5506021 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 943MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.76s +Memory: 857MB (+0MB) +UNKNOWN +Iteration Time: 8.84s + +Iteration 92 +Queue: [(15,75,3,True), (16,80,3,False), (17,85,3,False), (18,90,3,False), (19,95,2,True), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 93 +Time : 709.638s (Solving: 678.20s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 709.764s + +Choices : 8603940 (Domain: 8443037) +Conflicts : 722921 (Analyzed: 722918) +Restarts : 8843 (Average: 81.75 Last: 199) +Model-Level : 148.0 +Problems : 93 (Average Length: 90.82 Splits: 0) +Lemmas : 722918 (Deleted: 680248) + Binary : 11430 (Ratio: 1.58%) + Ternary : 3940 (Ratio: 0.55%) + Conflict : 722918 (Average Length: 589.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 722918 (Average: 9.97 Max: 1058 Sum: 7209996) + Executed : 722804 (Average: 9.97 Max: 1058 Sum: 7206242 Ratio: 99.95%) + Bounded : 114 (Average: 32.93 Max: 117 Sum: 3754 Ratio: 0.05%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 742606 (Eliminated: 0 Frozen: 233385) +Constraints : 5506021 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 943MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.78s +Memory: 857MB (+0MB) +UNKNOWN +Iteration Time: 7.86s + +Iteration 93 +Queue: [(19,95,2,True), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 94 +Time : 718.195s (Solving: 686.58s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 718.324s + +Choices : 8706565 (Domain: 8545601) +Conflicts : 731785 (Analyzed: 731782) +Restarts : 8943 (Average: 81.83 Last: 199) +Model-Level : 148.0 +Problems : 94 (Average Length: 91.10 Splits: 0) +Lemmas : 731782 (Deleted: 690497) + Binary : 11482 (Ratio: 1.57%) + Ternary : 3948 (Ratio: 0.54%) + Conflict : 731782 (Average Length: 594.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 731782 (Average: 9.95 Max: 1058 Sum: 7282683) + Executed : 731668 (Average: 9.95 Max: 1058 Sum: 7278929 Ratio: 99.95%) + Bounded : 114 (Average: 32.93 Max: 117 Sum: 3754 Ratio: 0.05%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 742606 (Eliminated: 0 Frozen: 233385) +Constraints : 5506021 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 943MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.49s +Memory: 857MB (+0MB) +UNKNOWN +Iteration Time: 8.56s + +Iteration 94 +Queue: [(4,20,8,True), (5,25,8,True), (6,30,7,True), (7,35,7,True), (8,40,6,True), (9,45,6,False), (10,50,5,True), (11,55,5,False), (12,60,4,True), (13,65,4,False), (14,70,4,False), (15,75,4,False), (16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,True), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Blocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 95 +Time : 722.369s (Solving: 690.59s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 722.500s + +Choices : 8755018 (Domain: 8594054) +Conflicts : 739296 (Analyzed: 739293) +Restarts : 9043 (Average: 81.75 Last: 199) +Model-Level : 148.0 +Problems : 95 (Average Length: 91.37 Splits: 0) +Lemmas : 739293 (Deleted: 696877) + Binary : 11550 (Ratio: 1.56%) + Ternary : 3961 (Ratio: 0.54%) + Conflict : 739293 (Average Length: 592.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 739293 (Average: 9.91 Max: 1058 Sum: 7325039) + Executed : 739179 (Average: 9.90 Max: 1058 Sum: 7321285 Ratio: 99.95%) + Bounded : 114 (Average: 32.93 Max: 117 Sum: 3754 Ratio: 0.05%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 742606 (Eliminated: 0 Frozen: 233385) +Constraints : 5506021 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 943MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 4.12s +Memory: 857MB (+0MB) +UNKNOWN +Iteration Time: 4.18s + +Iteration 95 +Queue: [(5,25,8,True), (6,30,7,True), (7,35,7,True), (8,40,6,True), (9,45,6,False), (10,50,5,True), (11,55,5,False), (12,60,4,True), (13,65,4,False), (14,70,4,False), (15,75,4,False), (16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,True), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 96 +Time : 731.443s (Solving: 699.49s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 731.576s + +Choices : 8810270 (Domain: 8649306) +Conflicts : 748234 (Analyzed: 748231) +Restarts : 9143 (Average: 81.84 Last: 199) +Model-Level : 148.0 +Problems : 96 (Average Length: 91.64 Splits: 0) +Lemmas : 748231 (Deleted: 706419) + Binary : 11585 (Ratio: 1.55%) + Ternary : 3966 (Ratio: 0.53%) + Conflict : 748231 (Average Length: 596.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 748231 (Average: 9.85 Max: 1058 Sum: 7369842) + Executed : 748117 (Average: 9.84 Max: 1058 Sum: 7366088 Ratio: 99.95%) + Bounded : 114 (Average: 32.93 Max: 117 Sum: 3754 Ratio: 0.05%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 742606 (Eliminated: 0 Frozen: 233385) +Constraints : 5506021 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 943MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.01s +Memory: 857MB (+0MB) +UNKNOWN +Iteration Time: 9.08s + +Iteration 96 +Queue: [(6,30,7,True), (7,35,7,True), (8,40,6,True), (9,45,6,False), (10,50,5,True), (11,55,5,False), (12,60,4,True), (13,65,4,False), (14,70,4,False), (15,75,4,False), (16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,True), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 97 +Time : 740.986s (Solving: 708.88s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 741.124s + +Choices : 8902891 (Domain: 8741927) +Conflicts : 756805 (Analyzed: 756802) +Restarts : 9243 (Average: 81.88 Last: 199) +Model-Level : 148.0 +Problems : 97 (Average Length: 91.90 Splits: 0) +Lemmas : 756802 (Deleted: 713026) + Binary : 11633 (Ratio: 1.54%) + Ternary : 3976 (Ratio: 0.53%) + Conflict : 756802 (Average Length: 601.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 756802 (Average: 9.83 Max: 1058 Sum: 7440639) + Executed : 756688 (Average: 9.83 Max: 1058 Sum: 7436885 Ratio: 99.95%) + Bounded : 114 (Average: 32.93 Max: 117 Sum: 3754 Ratio: 0.05%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 742606 (Eliminated: 0 Frozen: 233385) +Constraints : 5506021 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 943MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.50s +Memory: 857MB (+0MB) +UNKNOWN +Iteration Time: 9.55s + +Iteration 97 +Queue: [(7,35,7,True), (8,40,6,True), (9,45,6,False), (10,50,5,True), (11,55,5,False), (12,60,4,True), (13,65,4,False), (14,70,4,False), (15,75,4,False), (16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,True), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 98 +Time : 748.422s (Solving: 716.16s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 748.564s + +Choices : 8972295 (Domain: 8811308) +Conflicts : 765418 (Analyzed: 765415) +Restarts : 9343 (Average: 81.92 Last: 199) +Model-Level : 148.0 +Problems : 98 (Average Length: 92.15 Splits: 0) +Lemmas : 765415 (Deleted: 723528) + Binary : 11685 (Ratio: 1.53%) + Ternary : 3993 (Ratio: 0.52%) + Conflict : 765415 (Average Length: 606.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 765415 (Average: 9.79 Max: 1058 Sum: 7490848) + Executed : 765301 (Average: 9.78 Max: 1058 Sum: 7487094 Ratio: 99.95%) + Bounded : 114 (Average: 32.93 Max: 117 Sum: 3754 Ratio: 0.05%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 742606 (Eliminated: 0 Frozen: 233385) +Constraints : 5506021 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 943MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.39s +Memory: 857MB (+0MB) +UNKNOWN +Iteration Time: 7.44s + +Iteration 98 +Queue: [(8,40,6,True), (9,45,6,False), (10,50,5,True), (11,55,5,False), (12,60,4,True), (13,65,4,False), (14,70,4,False), (15,75,4,False), (16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,True), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 99 +Time : 756.504s (Solving: 724.09s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 756.652s + +Choices : 9048323 (Domain: 8887241) +Conflicts : 773738 (Analyzed: 773735) +Restarts : 9443 (Average: 81.94 Last: 199) +Model-Level : 148.0 +Problems : 99 (Average Length: 92.40 Splits: 0) +Lemmas : 773735 (Deleted: 729839) + Binary : 11754 (Ratio: 1.52%) + Ternary : 4004 (Ratio: 0.52%) + Conflict : 773735 (Average Length: 614.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 773735 (Average: 9.75 Max: 1058 Sum: 7545457) + Executed : 773621 (Average: 9.75 Max: 1058 Sum: 7541703 Ratio: 99.95%) + Bounded : 114 (Average: 32.93 Max: 117 Sum: 3754 Ratio: 0.05%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 742606 (Eliminated: 0 Frozen: 233385) +Constraints : 5506021 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 943MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.03s +Memory: 857MB (+0MB) +UNKNOWN +Iteration Time: 8.09s + +Iteration 99 +Queue: [(10,50,5,True), (11,55,5,False), (12,60,4,True), (13,65,4,False), (14,70,4,False), (15,75,4,False), (16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,True), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 100 +Time : 765.667s (Solving: 733.10s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 765.820s + +Choices : 9130864 (Domain: 8969757) +Conflicts : 782471 (Analyzed: 782468) +Restarts : 9543 (Average: 81.99 Last: 199) +Model-Level : 148.0 +Problems : 100 (Average Length: 92.65 Splits: 0) +Lemmas : 782468 (Deleted: 740075) + Binary : 11778 (Ratio: 1.51%) + Ternary : 4008 (Ratio: 0.51%) + Conflict : 782468 (Average Length: 622.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 782468 (Average: 9.72 Max: 1058 Sum: 7603314) + Executed : 782354 (Average: 9.71 Max: 1058 Sum: 7599560 Ratio: 99.95%) + Bounded : 114 (Average: 32.93 Max: 117 Sum: 3754 Ratio: 0.05%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 742606 (Eliminated: 0 Frozen: 233385) +Constraints : 5506021 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 943MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.11s +Memory: 857MB (+0MB) +UNKNOWN +Iteration Time: 9.17s + +Iteration 100 +Queue: [(12,60,4,True), (13,65,4,False), (14,70,4,False), (15,75,4,False), (16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,True), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 101 +Time : 774.653s (Solving: 741.92s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 774.808s + +Choices : 9191976 (Domain: 9030867) +Conflicts : 791222 (Analyzed: 791219) +Restarts : 9643 (Average: 82.05 Last: 199) +Model-Level : 148.0 +Problems : 101 (Average Length: 92.89 Splits: 0) +Lemmas : 791219 (Deleted: 748661) + Binary : 11784 (Ratio: 1.49%) + Ternary : 4009 (Ratio: 0.51%) + Conflict : 791219 (Average Length: 622.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 791219 (Average: 9.67 Max: 1058 Sum: 7649071) + Executed : 791105 (Average: 9.66 Max: 1058 Sum: 7645317 Ratio: 99.95%) + Bounded : 114 (Average: 32.93 Max: 117 Sum: 3754 Ratio: 0.05%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 742606 (Eliminated: 0 Frozen: 233385) +Constraints : 5506021 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 943MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.92s +Memory: 857MB (+0MB) +UNKNOWN +Iteration Time: 8.99s + +Iteration 101 +Queue: [(16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,True), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 102 +Time : 782.524s (Solving: 749.62s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 782.684s + +Choices : 9267875 (Domain: 9106764) +Conflicts : 799718 (Analyzed: 799715) +Restarts : 9743 (Average: 82.08 Last: 199) +Model-Level : 148.0 +Problems : 102 (Average Length: 93.13 Splits: 0) +Lemmas : 799715 (Deleted: 755133) + Binary : 11797 (Ratio: 1.48%) + Ternary : 4017 (Ratio: 0.50%) + Conflict : 799715 (Average Length: 622.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 799715 (Average: 9.64 Max: 1058 Sum: 7706284) + Executed : 799601 (Average: 9.63 Max: 1058 Sum: 7702530 Ratio: 99.95%) + Bounded : 114 (Average: 32.93 Max: 117 Sum: 3754 Ratio: 0.05%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 742606 (Eliminated: 0 Frozen: 233385) +Constraints : 5506021 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 943MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.81s +Memory: 857MB (+0MB) +UNKNOWN +Iteration Time: 7.88s + +Iteration 102 +Queue: [(20,100,2,True), (21,105,2,True), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 103 +Time : 790.891s (Solving: 757.83s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 791.056s + +Choices : 9353756 (Domain: 9192645) +Conflicts : 808956 (Analyzed: 808953) +Restarts : 9843 (Average: 82.19 Last: 199) +Model-Level : 148.0 +Problems : 103 (Average Length: 93.36 Splits: 0) +Lemmas : 808953 (Deleted: 765640) + Binary : 11814 (Ratio: 1.46%) + Ternary : 4023 (Ratio: 0.50%) + Conflict : 808953 (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 : 808953 (Average: 9.60 Max: 1058 Sum: 7765927) + Executed : 808838 (Average: 9.60 Max: 1058 Sum: 7762056 Ratio: 99.95%) + Bounded : 115 (Average: 33.66 Max: 117 Sum: 3871 Ratio: 0.05%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 742606 (Eliminated: 0 Frozen: 233385) +Constraints : 5506021 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 943MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.31s +Memory: 857MB (+0MB) +UNKNOWN +Iteration Time: 8.37s + +Iteration 103 +Queue: [(21,105,2,True), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 104 +Time : 799.335s (Solving: 766.11s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 799.504s + +Choices : 9435298 (Domain: 9274181) +Conflicts : 816954 (Analyzed: 816951) +Restarts : 9943 (Average: 82.16 Last: 199) +Model-Level : 148.0 +Problems : 104 (Average Length: 93.59 Splits: 0) +Lemmas : 816951 (Deleted: 772601) + Binary : 11822 (Ratio: 1.45%) + Ternary : 4029 (Ratio: 0.49%) + Conflict : 816951 (Average Length: 624.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 816951 (Average: 9.58 Max: 1058 Sum: 7826602) + Executed : 816836 (Average: 9.58 Max: 1058 Sum: 7822731 Ratio: 99.95%) + Bounded : 115 (Average: 33.66 Max: 117 Sum: 3871 Ratio: 0.05%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 742606 (Eliminated: 0 Frozen: 233385) +Constraints : 5506007 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 943MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.39s +Memory: 857MB (+0MB) +UNKNOWN +Iteration Time: 8.45s + +Iteration 104 +Queue: [(4,20,9,True), (5,25,9,True), (6,30,8,True), (7,35,8,False), (8,40,7,True), (9,45,6,True), (10,50,6,False), (11,55,5,True), (12,60,5,False), (13,65,4,True), (14,70,4,False), (15,75,4,False), (16,80,4,False), (17,85,3,True), (18,90,3,False), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,2,True), (23,115,2,False)] +Grounded Until: 115 +Blocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 105 +Time : 805.119s (Solving: 771.74s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 805.292s + +Choices : 9483454 (Domain: 9322337) +Conflicts : 825009 (Analyzed: 825006) +Restarts : 10043 (Average: 82.15 Last: 199) +Model-Level : 148.0 +Problems : 105 (Average Length: 93.81 Splits: 0) +Lemmas : 825006 (Deleted: 780339) + Binary : 11871 (Ratio: 1.44%) + Ternary : 4039 (Ratio: 0.49%) + Conflict : 825006 (Average Length: 624.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 825006 (Average: 9.54 Max: 1058 Sum: 7868631) + Executed : 824891 (Average: 9.53 Max: 1058 Sum: 7864760 Ratio: 99.95%) + Bounded : 115 (Average: 33.66 Max: 117 Sum: 3871 Ratio: 0.05%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 742606 (Eliminated: 0 Frozen: 233385) +Constraints : 5506007 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 943MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 5.73s +Memory: 857MB (+0MB) +UNKNOWN +Iteration Time: 5.79s + +Iteration 105 +Queue: [(5,25,9,True), (6,30,8,True), (7,35,8,False), (8,40,7,True), (9,45,6,True), (10,50,6,False), (11,55,5,True), (12,60,5,False), (13,65,4,True), (14,70,4,False), (15,75,4,False), (16,80,4,False), (17,85,3,True), (18,90,3,False), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,2,True), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 106 +Time : 816.483s (Solving: 782.95s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 816.660s + +Choices : 9536234 (Domain: 9375117) +Conflicts : 834315 (Analyzed: 834312) +Restarts : 10143 (Average: 82.25 Last: 199) +Model-Level : 148.0 +Problems : 106 (Average Length: 94.03 Splits: 0) +Lemmas : 834312 (Deleted: 790395) + Binary : 11883 (Ratio: 1.42%) + Ternary : 4044 (Ratio: 0.48%) + Conflict : 834312 (Average Length: 632.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 834312 (Average: 9.48 Max: 1058 Sum: 7909082) + Executed : 834197 (Average: 9.48 Max: 1058 Sum: 7905211 Ratio: 99.95%) + Bounded : 115 (Average: 33.66 Max: 117 Sum: 3871 Ratio: 0.05%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 742606 (Eliminated: 0 Frozen: 233385) +Constraints : 5506007 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 943MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 11.32s +Memory: 857MB (+0MB) +UNKNOWN +Iteration Time: 11.37s + +Iteration 106 +Queue: [(6,30,8,True), (7,35,8,False), (8,40,7,True), (9,45,6,True), (10,50,6,False), (11,55,5,True), (12,60,5,False), (13,65,4,True), (14,70,4,False), (15,75,4,False), (16,80,4,False), (17,85,3,True), (18,90,3,False), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,2,True), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 107 +Time : 821.661s (Solving: 787.96s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 821.840s + +Choices : 9580412 (Domain: 9419295) +Conflicts : 841863 (Analyzed: 841860) +Restarts : 10243 (Average: 82.19 Last: 199) +Model-Level : 148.0 +Problems : 107 (Average Length: 94.24 Splits: 0) +Lemmas : 841860 (Deleted: 797354) + Binary : 11902 (Ratio: 1.41%) + Ternary : 4048 (Ratio: 0.48%) + Conflict : 841860 (Average Length: 631.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 841860 (Average: 9.43 Max: 1058 Sum: 7941299) + Executed : 841745 (Average: 9.43 Max: 1058 Sum: 7937428 Ratio: 99.95%) + Bounded : 115 (Average: 33.66 Max: 117 Sum: 3871 Ratio: 0.05%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 742606 (Eliminated: 0 Frozen: 233385) +Constraints : 5506007 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 943MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 5.12s +Memory: 857MB (+0MB) +UNKNOWN +Iteration Time: 5.18s + +Iteration 107 +Queue: [(8,40,7,True), (9,45,6,True), (10,50,6,False), (11,55,5,True), (12,60,5,False), (13,65,4,True), (14,70,4,False), (15,75,4,False), (16,80,4,False), (17,85,3,True), (18,90,3,False), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,2,True), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 108 +Time : 828.554s (Solving: 794.68s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 828.736s + +Choices : 9656002 (Domain: 9494786) +Conflicts : 850202 (Analyzed: 850199) +Restarts : 10343 (Average: 82.20 Last: 199) +Model-Level : 148.0 +Problems : 108 (Average Length: 94.45 Splits: 0) +Lemmas : 850199 (Deleted: 804818) + Binary : 11959 (Ratio: 1.41%) + Ternary : 4063 (Ratio: 0.48%) + Conflict : 850199 (Average Length: 633.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 850199 (Average: 9.41 Max: 1058 Sum: 7998333) + Executed : 850084 (Average: 9.40 Max: 1058 Sum: 7994462 Ratio: 99.95%) + Bounded : 115 (Average: 33.66 Max: 117 Sum: 3871 Ratio: 0.05%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 742606 (Eliminated: 0 Frozen: 233385) +Constraints : 5506007 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 943MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.83s +Memory: 857MB (+0MB) +UNKNOWN +Iteration Time: 6.90s + +Iteration 108 +Queue: [(9,45,6,True), (10,50,6,False), (11,55,5,True), (12,60,5,False), (13,65,4,True), (14,70,4,False), (15,75,4,False), (16,80,4,False), (17,85,3,True), (18,90,3,False), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,2,True), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 109 +Time : 835.431s (Solving: 801.39s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 835.616s + +Choices : 9727918 (Domain: 9566701) +Conflicts : 858819 (Analyzed: 858816) +Restarts : 10443 (Average: 82.24 Last: 199) +Model-Level : 148.0 +Problems : 109 (Average Length: 94.66 Splits: 0) +Lemmas : 858816 (Deleted: 815156) + Binary : 11975 (Ratio: 1.39%) + Ternary : 4064 (Ratio: 0.47%) + Conflict : 858816 (Average Length: 636.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 858816 (Average: 9.37 Max: 1058 Sum: 8050938) + Executed : 858701 (Average: 9.37 Max: 1058 Sum: 8047067 Ratio: 99.95%) + Bounded : 115 (Average: 33.66 Max: 117 Sum: 3871 Ratio: 0.05%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 742606 (Eliminated: 0 Frozen: 233385) +Constraints : 5506007 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 943MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.82s +Memory: 857MB (+0MB) +UNKNOWN +Iteration Time: 6.88s + +Iteration 109 +Queue: [(11,55,5,True), (12,60,5,False), (13,65,4,True), (14,70,4,False), (15,75,4,False), (16,80,4,False), (17,85,3,True), (18,90,3,False), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,2,True), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 110 +Time : 842.347s (Solving: 808.12s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 842.532s + +Choices : 9797223 (Domain: 9636001) +Conflicts : 867543 (Analyzed: 867540) +Restarts : 10543 (Average: 82.29 Last: 199) +Model-Level : 148.0 +Problems : 110 (Average Length: 94.86 Splits: 0) +Lemmas : 867540 (Deleted: 823646) + Binary : 11991 (Ratio: 1.38%) + Ternary : 4066 (Ratio: 0.47%) + Conflict : 867540 (Average Length: 638.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 867540 (Average: 9.34 Max: 1058 Sum: 8102047) + Executed : 867425 (Average: 9.33 Max: 1058 Sum: 8098176 Ratio: 99.95%) + Bounded : 115 (Average: 33.66 Max: 117 Sum: 3871 Ratio: 0.05%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 742606 (Eliminated: 0 Frozen: 233385) +Constraints : 5506007 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 943MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.85s +Memory: 857MB (+0MB) +UNKNOWN +Iteration Time: 6.92s + +Iteration 110 +Queue: [(13,65,4,True), (14,70,4,False), (15,75,4,False), (16,80,4,False), (17,85,3,True), (18,90,3,False), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,2,True), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 111 +Time : 853.659s (Solving: 819.28s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 853.848s + +Choices : 9949967 (Domain: 9785794) +Conflicts : 876581 (Analyzed: 876578) +Restarts : 10643 (Average: 82.36 Last: 199) +Model-Level : 148.0 +Problems : 111 (Average Length: 95.06 Splits: 0) +Lemmas : 876578 (Deleted: 832232) + Binary : 12158 (Ratio: 1.39%) + Ternary : 4113 (Ratio: 0.47%) + Conflict : 876578 (Average Length: 645.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 876578 (Average: 9.38 Max: 1058 Sum: 8225712) + Executed : 876463 (Average: 9.38 Max: 1058 Sum: 8221841 Ratio: 99.95%) + Bounded : 115 (Average: 33.66 Max: 117 Sum: 3871 Ratio: 0.05%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 742606 (Eliminated: 0 Frozen: 233385) +Constraints : 5506007 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 943MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 11.27s +Memory: 857MB (+0MB) +UNKNOWN +Iteration Time: 11.32s + +Iteration 111 +Queue: [(17,85,3,True), (18,90,3,False), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,2,True), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 112 +Time : 863.426s (Solving: 828.89s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 863.620s + +Choices : 10042502 (Domain: 9878317) +Conflicts : 885738 (Analyzed: 885735) +Restarts : 10743 (Average: 82.45 Last: 199) +Model-Level : 148.0 +Problems : 112 (Average Length: 95.26 Splits: 0) +Lemmas : 885735 (Deleted: 840911) + Binary : 12184 (Ratio: 1.38%) + Ternary : 4119 (Ratio: 0.47%) + Conflict : 885735 (Average Length: 650.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 885735 (Average: 9.36 Max: 1058 Sum: 8289402) + Executed : 885620 (Average: 9.35 Max: 1058 Sum: 8285531 Ratio: 99.95%) + Bounded : 115 (Average: 33.66 Max: 117 Sum: 3871 Ratio: 0.05%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 742606 (Eliminated: 0 Frozen: 233385) +Constraints : 5506007 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 943MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.71s +Memory: 857MB (+0MB) +UNKNOWN +Iteration Time: 9.77s + +Iteration 112 +Queue: [(22,110,2,True), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 113 +Time : 879.556s (Solving: 844.86s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 879.756s + +Choices : 10485047 (Domain: 10316374) +Conflicts : 894880 (Analyzed: 894877) +Restarts : 10843 (Average: 82.53 Last: 199) +Model-Level : 148.0 +Problems : 113 (Average Length: 95.45 Splits: 0) +Lemmas : 894877 (Deleted: 848790) + Binary : 12604 (Ratio: 1.41%) + Ternary : 4199 (Ratio: 0.47%) + Conflict : 894877 (Average Length: 654.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 894877 (Average: 9.70 Max: 1105 Sum: 8684412) + Executed : 894762 (Average: 9.70 Max: 1105 Sum: 8680541 Ratio: 99.96%) + Bounded : 115 (Average: 33.66 Max: 117 Sum: 3871 Ratio: 0.04%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 742606 (Eliminated: 0 Frozen: 233385) +Constraints : 5506007 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 943MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 16.08s +Memory: 857MB (+0MB) +UNKNOWN +Iteration Time: 16.14s + +Iteration 113 +Queue: [(4,20,10,True), (5,25,10,True), (6,30,9,True), (7,35,8,True), (8,40,8,False), (9,45,7,False), (10,50,6,True), (11,55,6,False), (12,60,5,True), (13,65,5,False), (14,70,4,True), (15,75,4,False), (16,80,4,False), (17,85,4,False), (18,90,3,True), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,2,False)] +Grounded Until: 115 +Blocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 114 +Time : 883.591s (Solving: 848.74s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 883.792s + +Choices : 10528161 (Domain: 10359488) +Conflicts : 902448 (Analyzed: 902445) +Restarts : 10943 (Average: 82.47 Last: 199) +Model-Level : 148.0 +Problems : 114 (Average Length: 95.64 Splits: 0) +Lemmas : 902445 (Deleted: 855730) + Binary : 12665 (Ratio: 1.40%) + Ternary : 4206 (Ratio: 0.47%) + Conflict : 902445 (Average Length: 654.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 902445 (Average: 9.66 Max: 1105 Sum: 8721053) + Executed : 902330 (Average: 9.66 Max: 1105 Sum: 8717182 Ratio: 99.96%) + Bounded : 115 (Average: 33.66 Max: 117 Sum: 3871 Ratio: 0.04%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 742606 (Eliminated: 0 Frozen: 233385) +Constraints : 5506007 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 943MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 3.98s +Memory: 857MB (+0MB) +UNKNOWN +Iteration Time: 4.04s + +Iteration 114 +Queue: [(5,25,10,True), (6,30,9,True), (7,35,8,True), (8,40,8,False), (9,45,7,False), (10,50,6,True), (11,55,6,False), (12,60,5,True), (13,65,5,False), (14,70,4,True), (15,75,4,False), (16,80,4,False), (17,85,4,False), (18,90,3,True), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +*** Info : (planner): INTERRUPTED by signal! +UNKNOWN + +INTERRUPTED : 1 + +Models : 0+ +Calls : 115 +Time : 893.530s (Solving: 858.51s 1st Model: 0.00s Unsat: 2.29s) +CPU Time : 893.716s + +Choices : 10567602 (Domain: 10398929) +Conflicts : 909948 (Analyzed: 909945) +Restarts : 11022 (Average: 82.56 Last: 199) +Model-Level : 148.0 +Problems : 115 (Average Length: 95.83 Splits: 0) +Lemmas : 909945 (Deleted: 863605) + Binary : 12691 (Ratio: 1.39%) + Ternary : 4208 (Ratio: 0.46%) + Conflict : 909945 (Average Length: 661.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 909945 (Average: 9.61 Max: 1105 Sum: 8748557) + Executed : 909830 (Average: 9.61 Max: 1105 Sum: 8744686 Ratio: 99.96%) + Bounded : 115 (Average: 33.66 Max: 117 Sum: 3871 Ratio: 0.04%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 742606 (Eliminated: 0 Frozen: 233385) +Constraints : 5506007 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 943MB +Max. Length : 115 steps +Models : 1 + +