diff --git a/gc-ta1-tt1/ipc-2011_barman-sequential-satisficing_15.env b/gc-ta1-tt1/ipc-2011_barman-sequential-satisficing_15.env new file mode 100644 index 000000000..d4688b296 --- /dev/null +++ b/gc-ta1-tt1/ipc-2011_barman-sequential-satisficing_15.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-15.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: 15 + 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_15.err b/gc-ta1-tt1/ipc-2011_barman-sequential-satisficing_15.err new file mode 100644 index 000000000..d37fb2cec --- /dev/null +++ b/gc-ta1-tt1/ipc-2011_barman-sequential-satisficing_15.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': 15} +# 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-15.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.10 MEM 1012168 MAXMEM 1112004 STALE 1 MAXMEM_RSS 977156 + + diff --git a/gc-ta1-tt1/ipc-2011_barman-sequential-satisficing_15.out b/gc-ta1-tt1/ipc-2011_barman-sequential-satisficing_15.out new file mode 100644 index 000000000..4ec314203 --- /dev/null +++ b/gc-ta1-tt1/ipc-2011_barman-sequential-satisficing_15.out @@ -0,0 +1,5262 @@ +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-15.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-15.pddl +Parsing... +Parsing: [0.030s CPU, 0.031s wall-clock] +Normalizing task... [0.000s CPU, 0.002s wall-clock] +Instantiating... +Generating Datalog program... [0.010s CPU, 0.008s wall-clock] +Normalizing Datalog program... +Normalizing Datalog program: [0.040s CPU, 0.041s wall-clock] +Preparing model... [0.030s CPU, 0.024s wall-clock] +Generated 115 rules. +Computing model... [0.500s CPU, 0.504s wall-clock] +3094 relevant atoms +3221 auxiliary atoms +6315 final queue length +10878 total queue pushes +Completing instantiation... [0.960s CPU, 0.962s wall-clock] +Instantiating: [1.550s CPU, 1.547s wall-clock] +Computing fact groups... +Finding invariants... +24 initial candidates +Finding invariants: [0.110s CPU, 0.112s wall-clock] +Checking invariant weight... [0.000s CPU, 0.001s wall-clock] +Instantiating groups... [0.010s CPU, 0.009s wall-clock] +Collecting mutex groups... [0.010s CPU, 0.001s wall-clock] +Choosing groups... +328 uncovered facts +Choosing groups: [0.000s CPU, 0.002s wall-clock] +Building translation key... [0.010s CPU, 0.012s wall-clock] +Computing fact groups: [0.160s CPU, 0.163s wall-clock] +Building STRIPS to SAS dictionary... [0.010s CPU, 0.003s wall-clock] +Building dictionary for full mutex groups... [0.000s CPU, 0.003s 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.051s wall-clock] +Translating task: [1.000s CPU, 0.996s wall-clock] +3672 effect conditions simplified +0 implied preconditions added +Detecting unreachable propositions... +0 operators removed +0 axioms removed +3 propositions removed +Detecting unreachable propositions: [0.490s CPU, 0.490s wall-clock] +Reordering and filtering variables... +331 of 331 variables necessary. +15 of 18 mutex groups necessary. +2194 of 2194 operators necessary. +0 of 0 axiom rules necessary. +Reordering and filtering variables: [0.400s CPU, 0.401s wall-clock] +Translator variables: 331 +Translator derived variables: 0 +Translator facts: 691 +Translator goal facts: 13 +Translator mutex groups: 15 +Translator total mutex groups size: 45 +Translator operators: 2194 +Translator axioms: 0 +Translator task size: 21018 +Translator peak memory: 48332 KB +Writing output... [0.400s CPU, 0.441s wall-clock] +Done! [4.080s CPU, 4.121s wall-clock] +planner.py version 0.0.1 + +Time: 0.85s +Memory: 107MB + +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.985s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s) +CPU Time : 0.852s + +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 : 60629 +Atoms : 60629 +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 : 243MB +Max. Length : 0 steps +Models : 0 + +[endof: stats after solve call] +Solving Time: 0.01s +Memory: 179MB (+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: 179MB +Grounding... [('step', [1]), ('step', [2]), ('step', [3]), ('step', [4]), ('step', [5]), ('check', [5])] +Grounding Time: 0.26s +Memory: 179MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0 +Calls : 2 +Time : 1.393s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s) +CPU Time : 1.260s + +Choices : 328 (Domain: 271) +Conflicts : 52 (Analyzed: 51) +Restarts : 0 +Problems : 2 (Average Length: 4.50 Splits: 0) +Lemmas : 51 (Deleted: 0) + Binary : 20 (Ratio: 39.22%) + Ternary : 2 (Ratio: 3.92%) + Conflict : 51 (Average Length: 5.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 51 (Average: 6.47 Max: 37 Sum: 330) + Executed : 49 (Average: 6.43 Max: 37 Sum: 328 Ratio: 99.39%) + Bounded : 2 (Average: 1.00 Max: 1 Sum: 2 Ratio: 0.61%) + +Rules : 60629 +Atoms : 60629 +Bodies : 1 (Original: 0) +Tight : Yes +Variables : 16256 (Eliminated: 0 Frozen: 160) +Constraints : 53667 (Binary: 95.3% Ternary: 3.3% Other: 1.4%) + +Memory Peak : 243MB +Max. Length : 0 steps +Models : 0 + +[endof: stats after solve call] +Solving Time: 0.02s +Memory: 183MB (+4MB) +UNSAT +Iteration Time: 0.41s + +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: 187.0MB +Grounding... [('step', [6]), ('step', [7]), ('step', [8]), ('step', [9]), ('step', [10]), ('check', [10])] +Grounding Time: 0.31s +Memory: 190MB (+7MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 1+ +Calls : 3 +Time : 1.924s (Solving: 0.08s 1st Model: 0.07s Unsat: 0.00s) +CPU Time : 1.788s + +Choices : 2349 (Domain: 2154) +Conflicts : 334 (Analyzed: 333) +Restarts : 2 (Average: 166.50 Last: 62) +Model-Level : 251.0 +Problems : 3 (Average Length: 7.00 Splits: 0) +Lemmas : 333 (Deleted: 0) + Binary : 70 (Ratio: 21.02%) + Ternary : 10 (Ratio: 3.00%) + Conflict : 333 (Average Length: 182.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 333 (Average: 6.20 Max: 132 Sum: 2065) + Executed : 331 (Average: 6.20 Max: 132 Sum: 2063 Ratio: 99.90%) + Bounded : 2 (Average: 1.00 Max: 1 Sum: 2 Ratio: 0.10%) + +Rules : 60629 +Atoms : 60629 +Bodies : 1 (Original: 0) +Tight : Yes +Variables : 35632 (Eliminated: 0 Frozen: 320) +Constraints : 211962 (Binary: 95.6% Ternary: 3.2% Other: 1.2%) + +Memory Peak : 243MB +Max. Length : 5 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 0.09s +Memory: 198MB (+8MB) +SAT +Testing... +NOT SERIALIZABLE +Testing Time: 1.08s +Memory: 232MB (+34MB) +Solving... +[start: stats after solve call] + +Models : 0 +Calls : 4 +Time : 2.542s (Solving: 0.36s 1st Model: 0.07s Unsat: 0.29s) +CPU Time : 2.408s + +Choices : 9441 (Domain: 7693) +Conflicts : 972 (Analyzed: 970) +Restarts : 10 (Average: 97.00 Last: 62) +Model-Level : 251.0 +Problems : 4 (Average Length: 8.25 Splits: 0) +Lemmas : 970 (Deleted: 0) + Binary : 215 (Ratio: 22.16%) + Ternary : 73 (Ratio: 7.53%) + Conflict : 970 (Average Length: 87.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 970 (Average: 9.43 Max: 132 Sum: 9151) + Executed : 963 (Average: 9.39 Max: 132 Sum: 9111 Ratio: 99.56%) + Bounded : 7 (Average: 5.71 Max: 12 Sum: 40 Ratio: 0.44%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 56254 (Eliminated: 0 Frozen: 15821) +Constraints : 347145 (Binary: 91.4% Ternary: 7.0% Other: 1.7%) + +Memory Peak : 243MB +Max. Length : 5 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 0.37s +Memory: 232MB (+0MB) +UNSAT +Iteration Time: 1.99s + +Iteration 4 +Queue: [(3,15,0,True), (4,20,0,True), (5,25,0,True), (6,30,0,True)] +Grounded Until: 10 +Expected Memory: 247.0MB +Grounding... [('step', [11]), ('step', [12]), ('step', [13]), ('step', [14]), ('step', [15]), ('check', [15])] +Grounding Time: 0.50s +Memory: 234MB (+2MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 5 +Time : 7.321s (Solving: 4.40s 1st Model: 0.07s Unsat: 0.29s) +CPU Time : 7.188s + +Choices : 103274 (Domain: 83893) +Conflicts : 10049 (Analyzed: 10047) +Restarts : 110 (Average: 91.34 Last: 82) +Model-Level : 251.0 +Problems : 5 (Average Length: 10.00 Splits: 0) +Lemmas : 10047 (Deleted: 5861) + Binary : 934 (Ratio: 9.30%) + Ternary : 431 (Ratio: 4.29%) + Conflict : 10047 (Average Length: 173.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 10047 (Average: 9.91 Max: 328 Sum: 99516) + Executed : 10030 (Average: 9.88 Max: 328 Sum: 99309 Ratio: 99.79%) + Bounded : 17 (Average: 12.18 Max: 17 Sum: 207 Ratio: 0.21%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 93745 (Eliminated: 0 Frozen: 27481) +Constraints : 624347 (Binary: 91.3% Ternary: 7.0% Other: 1.7%) + +Memory Peak : 257MB +Max. Length : 10 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 4.07s +Memory: 257MB (+23MB) +UNKNOWN +Iteration Time: 4.79s + +Iteration 5 +Queue: [(4,20,0,True), (5,25,0,True), (6,30,0,True)] +Grounded Until: 15 +Expected Memory: 282.0MB +Grounding... [('step', [16]), ('step', [17]), ('step', [18]), ('step', [19]), ('step', [20]), ('check', [20])] +Grounding Time: 0.51s +Memory: 260MB (+3MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 6 +Time : 13.330s (Solving: 9.64s 1st Model: 0.07s Unsat: 0.29s) +CPU Time : 13.196s + +Choices : 195626 (Domain: 161158) +Conflicts : 18931 (Analyzed: 18929) +Restarts : 210 (Average: 90.14 Last: 147) +Model-Level : 251.0 +Problems : 6 (Average Length: 12.00 Splits: 0) +Lemmas : 18929 (Deleted: 13925) + Binary : 1451 (Ratio: 7.67%) + Ternary : 525 (Ratio: 2.77%) + Conflict : 18929 (Average Length: 627.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 18929 (Average: 9.70 Max: 328 Sum: 183697) + Executed : 18912 (Average: 9.69 Max: 328 Sum: 183490 Ratio: 99.89%) + Bounded : 17 (Average: 12.18 Max: 17 Sum: 207 Ratio: 0.11%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 131236 (Eliminated: 0 Frozen: 39141) +Constraints : 896242 (Binary: 91.3% Ternary: 6.9% Other: 1.8%) + +Memory Peak : 280MB +Max. Length : 15 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 5.27s +Memory: 276MB (+16MB) +UNKNOWN +Iteration Time: 6.02s + +Iteration 6 +Queue: [(5,25,0,True), (6,30,0,True)] +Grounded Until: 20 +Expected Memory: 301.0MB +Grounding... [('step', [21]), ('step', [22]), ('step', [23]), ('step', [24]), ('step', [25]), ('check', [25])] +Grounding Time: 0.68s +Memory: 297MB (+21MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 7 +Time : 20.219s (Solving: 15.46s 1st Model: 0.07s Unsat: 0.29s) +CPU Time : 20.088s + +Choices : 312221 (Domain: 262527) +Conflicts : 27833 (Analyzed: 27831) +Restarts : 310 (Average: 89.78 Last: 147) +Model-Level : 251.0 +Problems : 7 (Average Length: 14.14 Splits: 0) +Lemmas : 27831 (Deleted: 22272) + Binary : 1738 (Ratio: 6.24%) + Ternary : 551 (Ratio: 1.98%) + Conflict : 27831 (Average Length: 876.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 27831 (Average: 10.39 Max: 328 Sum: 289195) + Executed : 27814 (Average: 10.38 Max: 328 Sum: 288988 Ratio: 99.93%) + Bounded : 17 (Average: 12.18 Max: 17 Sum: 207 Ratio: 0.07%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 168727 (Eliminated: 0 Frozen: 50801) +Constraints : 1178702 (Binary: 91.3% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 321MB +Max. Length : 20 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 5.89s +Memory: 309MB (+12MB) +UNKNOWN +Iteration Time: 6.90s + +Iteration 7 +Queue: [(6,30,0,True)] +Grounded Until: 25 +Expected Memory: 342.0MB +Grounding... [('step', [26]), ('step', [27]), ('step', [28]), ('step', [29]), ('step', [30]), ('check', [30])] +Grounding Time: 0.55s +Memory: 320MB (+11MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 8 +Time : 27.651s (Solving: 22.03s 1st Model: 0.07s Unsat: 0.29s) +CPU Time : 27.524s + +Choices : 479799 (Domain: 417037) +Conflicts : 37022 (Analyzed: 37020) +Restarts : 410 (Average: 90.29 Last: 147) +Model-Level : 251.0 +Problems : 8 (Average Length: 16.38 Splits: 0) +Lemmas : 37020 (Deleted: 30710) + Binary : 2027 (Ratio: 5.48%) + Ternary : 575 (Ratio: 1.55%) + Conflict : 37020 (Average Length: 983.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 37020 (Average: 12.01 Max: 328 Sum: 444719) + Executed : 37003 (Average: 12.01 Max: 328 Sum: 444512 Ratio: 99.95%) + Bounded : 17 (Average: 12.18 Max: 17 Sum: 207 Ratio: 0.05%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 206218 (Eliminated: 0 Frozen: 62461) +Constraints : 1461162 (Binary: 91.3% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 351MB +Max. Length : 25 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.62s +Memory: 351MB (+31MB) +UNKNOWN +Iteration Time: 7.44s + +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 : 33.602s (Solving: 27.92s 1st Model: 0.07s Unsat: 6.19s) +CPU Time : 33.476s + +Choices : 572044 (Domain: 497302) +Conflicts : 45447 (Analyzed: 45444) +Restarts : 507 (Average: 89.63 Last: 147) +Model-Level : 251.0 +Problems : 9 (Average Length: 18.11 Splits: 0) +Lemmas : 45444 (Deleted: 36473) + Binary : 2700 (Ratio: 5.94%) + Ternary : 694 (Ratio: 1.53%) + Conflict : 45444 (Average Length: 832.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 45444 (Average: 11.77 Max: 328 Sum: 534686) + Executed : 45406 (Average: 11.75 Max: 328 Sum: 533812 Ratio: 99.84%) + Bounded : 38 (Average: 23.00 Max: 32 Sum: 874 Ratio: 0.16%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 206218 (Eliminated: 0 Frozen: 62461) +Constraints : 1461162 (Binary: 91.3% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 351MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 5.94s +Memory: 351MB (+0MB) +UNSAT +Iteration Time: 5.96s + +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 : 40.287s (Solving: 34.56s 1st Model: 0.07s Unsat: 6.19s) +CPU Time : 40.164s + +Choices : 683784 (Domain: 598350) +Conflicts : 54404 (Analyzed: 54401) +Restarts : 607 (Average: 89.62 Last: 147) +Model-Level : 251.0 +Problems : 10 (Average Length: 19.50 Splits: 0) +Lemmas : 54401 (Deleted: 44132) + Binary : 3401 (Ratio: 6.25%) + Ternary : 902 (Ratio: 1.66%) + Conflict : 54401 (Average Length: 721.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 54401 (Average: 11.81 Max: 328 Sum: 642270) + Executed : 54339 (Average: 11.78 Max: 328 Sum: 640633 Ratio: 99.75%) + Bounded : 62 (Average: 26.40 Max: 32 Sum: 1637 Ratio: 0.25%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 206218 (Eliminated: 0 Frozen: 62461) +Constraints : 1421811 (Binary: 91.3% Ternary: 6.9% Other: 1.8%) + +Memory Peak : 351MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.67s +Memory: 351MB (+0MB) +UNKNOWN +Iteration Time: 6.69s + +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 : 46.293s (Solving: 40.52s 1st Model: 0.07s Unsat: 6.19s) +CPU Time : 46.176s + +Choices : 781906 (Domain: 687551) +Conflicts : 62886 (Analyzed: 62883) +Restarts : 707 (Average: 88.94 Last: 147) +Model-Level : 251.0 +Problems : 11 (Average Length: 20.64 Splits: 0) +Lemmas : 62883 (Deleted: 50567) + Binary : 3689 (Ratio: 5.87%) + Ternary : 961 (Ratio: 1.53%) + Conflict : 62883 (Average Length: 655.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 62883 (Average: 11.65 Max: 328 Sum: 732627) + Executed : 62808 (Average: 11.62 Max: 328 Sum: 730579 Ratio: 99.72%) + Bounded : 75 (Average: 27.31 Max: 32 Sum: 2048 Ratio: 0.28%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 206218 (Eliminated: 0 Frozen: 62461) +Constraints : 1395626 (Binary: 91.3% Ternary: 6.9% Other: 1.8%) + +Memory Peak : 351MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 5.99s +Memory: 351MB (+0MB) +UNKNOWN +Iteration Time: 6.01s + +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 : 52.276s (Solving: 46.46s 1st Model: 0.07s Unsat: 6.19s) +CPU Time : 52.160s + +Choices : 909194 (Domain: 808893) +Conflicts : 71442 (Analyzed: 71439) +Restarts : 807 (Average: 88.52 Last: 147) +Model-Level : 251.0 +Problems : 12 (Average Length: 21.58 Splits: 0) +Lemmas : 71439 (Deleted: 58311) + Binary : 4029 (Ratio: 5.64%) + Ternary : 1035 (Ratio: 1.45%) + Conflict : 71439 (Average Length: 611.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 71439 (Average: 11.91 Max: 335 Sum: 850558) + Executed : 71357 (Average: 11.87 Max: 335 Sum: 848286 Ratio: 99.73%) + Bounded : 82 (Average: 27.71 Max: 32 Sum: 2272 Ratio: 0.27%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 206218 (Eliminated: 0 Frozen: 62461) +Constraints : 1395295 (Binary: 91.3% Ternary: 6.9% Other: 1.8%) + +Memory Peak : 351MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 5.97s +Memory: 351MB (+0MB) +UNKNOWN +Iteration Time: 5.99s + +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: 393.0MB +Grounding... [('step', [31]), ('step', [32]), ('step', [33]), ('step', [34]), ('step', [35]), ('check', [35])] +Grounding Time: 0.56s +Memory: 351MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 13 +Time : 60.308s (Solving: 53.58s 1st Model: 0.07s Unsat: 6.19s) +CPU Time : 60.196s + +Choices : 1157175 (Domain: 1048177) +Conflicts : 80479 (Analyzed: 80476) +Restarts : 907 (Average: 88.73 Last: 156) +Model-Level : 251.0 +Problems : 13 (Average Length: 22.77 Splits: 0) +Lemmas : 80476 (Deleted: 69453) + Binary : 4441 (Ratio: 5.52%) + Ternary : 1051 (Ratio: 1.31%) + Conflict : 80476 (Average Length: 617.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 80476 (Average: 13.49 Max: 335 Sum: 1085595) + Executed : 80394 (Average: 13.46 Max: 335 Sum: 1083323 Ratio: 99.79%) + Bounded : 82 (Average: 27.71 Max: 32 Sum: 2272 Ratio: 0.21%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 243709 (Eliminated: 0 Frozen: 74121) +Constraints : 1672459 (Binary: 91.3% Ternary: 6.9% Other: 1.8%) + +Memory Peak : 387MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.19s +Memory: 365MB (+14MB) +UNKNOWN +Iteration Time: 8.05s + +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: 407.0MB +Grounding... [('step', [36]), ('step', [37]), ('step', [38]), ('step', [39]), ('step', [40]), ('check', [40])] +Grounding Time: 0.55s +Memory: 373MB (+8MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 14 +Time : 67.826s (Solving: 60.19s 1st Model: 0.07s Unsat: 6.19s) +CPU Time : 67.716s + +Choices : 1371177 (Domain: 1254940) +Conflicts : 89370 (Analyzed: 89367) +Restarts : 1007 (Average: 88.75 Last: 156) +Model-Level : 251.0 +Problems : 14 (Average Length: 24.14 Splits: 0) +Lemmas : 89367 (Deleted: 78148) + Binary : 4597 (Ratio: 5.14%) + Ternary : 1053 (Ratio: 1.18%) + Conflict : 89367 (Average Length: 640.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 89367 (Average: 14.37 Max: 335 Sum: 1283888) + Executed : 89285 (Average: 14.34 Max: 335 Sum: 1281616 Ratio: 99.82%) + Bounded : 82 (Average: 27.71 Max: 32 Sum: 2272 Ratio: 0.18%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 281200 (Eliminated: 0 Frozen: 85781) +Constraints : 1954919 (Binary: 91.3% Ternary: 6.9% Other: 1.8%) + +Memory Peak : 412MB +Max. Length : 35 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.68s +Memory: 388MB (+15MB) +UNKNOWN +Iteration Time: 7.53s + +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: 430.0MB +Grounding... [('step', [41]), ('step', [42]), ('step', [43]), ('step', [44]), ('step', [45]), ('check', [45])] +Grounding Time: 0.54s +Memory: 398MB (+10MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 15 +Time : 75.260s (Solving: 66.71s 1st Model: 0.07s Unsat: 6.19s) +CPU Time : 75.152s + +Choices : 1571613 (Domain: 1449993) +Conflicts : 97515 (Analyzed: 97512) +Restarts : 1107 (Average: 88.09 Last: 156) +Model-Level : 251.0 +Problems : 15 (Average Length: 25.67 Splits: 0) +Lemmas : 97512 (Deleted: 84548) + Binary : 4675 (Ratio: 4.79%) + Ternary : 1057 (Ratio: 1.08%) + Conflict : 97512 (Average Length: 667.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 97512 (Average: 15.04 Max: 396 Sum: 1466301) + Executed : 97430 (Average: 15.01 Max: 396 Sum: 1464029 Ratio: 99.85%) + Bounded : 82 (Average: 27.71 Max: 32 Sum: 2272 Ratio: 0.15%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 318691 (Eliminated: 0 Frozen: 97441) +Constraints : 2237379 (Binary: 91.3% Ternary: 6.9% Other: 1.8%) + +Memory Peak : 444MB +Max. Length : 40 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.60s +Memory: 443MB (+45MB) +UNKNOWN +Iteration Time: 7.45s + +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: 498.0MB +Grounding... [('step', [46]), ('step', [47]), ('step', [48]), ('step', [49]), ('step', [50]), ('check', [50])] +Grounding Time: 0.69s +Memory: 455MB (+12MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 16 +Time : 83.220s (Solving: 73.58s 1st Model: 0.07s Unsat: 6.19s) +CPU Time : 83.116s + +Choices : 1827366 (Domain: 1699900) +Conflicts : 106260 (Analyzed: 106257) +Restarts : 1207 (Average: 88.03 Last: 156) +Model-Level : 251.0 +Problems : 16 (Average Length: 27.31 Splits: 0) +Lemmas : 106257 (Deleted: 94747) + Binary : 4743 (Ratio: 4.46%) + Ternary : 1058 (Ratio: 1.00%) + Conflict : 106257 (Average Length: 695.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 106257 (Average: 16.03 Max: 415 Sum: 1703438) + Executed : 106175 (Average: 16.01 Max: 415 Sum: 1701166 Ratio: 99.87%) + Bounded : 82 (Average: 27.71 Max: 32 Sum: 2272 Ratio: 0.13%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 356182 (Eliminated: 0 Frozen: 109101) +Constraints : 2519839 (Binary: 91.3% Ternary: 6.9% Other: 1.8%) + +Memory Peak : 503MB +Max. Length : 45 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.95s +Memory: 466MB (+11MB) +UNKNOWN +Iteration Time: 7.98s + +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: 521.0MB +Grounding... [('step', [51]), ('step', [52]), ('step', [53]), ('step', [54]), ('step', [55]), ('check', [55])] +Grounding Time: 0.52s +Memory: 470MB (+4MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 17 +Time : 91.545s (Solving: 80.96s 1st Model: 0.07s Unsat: 6.19s) +CPU Time : 91.448s + +Choices : 2131193 (Domain: 1996576) +Conflicts : 114823 (Analyzed: 114820) +Restarts : 1307 (Average: 87.85 Last: 156) +Model-Level : 251.0 +Problems : 17 (Average Length: 29.06 Splits: 0) +Lemmas : 114820 (Deleted: 100990) + Binary : 4792 (Ratio: 4.17%) + Ternary : 1059 (Ratio: 0.92%) + Conflict : 114820 (Average Length: 713.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 114820 (Average: 17.30 Max: 490 Sum: 1986954) + Executed : 114738 (Average: 17.29 Max: 490 Sum: 1984682 Ratio: 99.89%) + Bounded : 82 (Average: 27.71 Max: 32 Sum: 2272 Ratio: 0.11%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 393673 (Eliminated: 0 Frozen: 120761) +Constraints : 2802299 (Binary: 91.3% Ternary: 6.9% Other: 1.8%) + +Memory Peak : 527MB +Max. Length : 50 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.47s +Memory: 489MB (+19MB) +UNKNOWN +Iteration Time: 8.34s + +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: 544.0MB +Grounding... [('step', [56]), ('step', [57]), ('step', [58]), ('step', [59]), ('step', [60]), ('check', [60])] +Grounding Time: 0.51s +Memory: 494MB (+5MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 18 +Time : 99.920s (Solving: 88.38s 1st Model: 0.07s Unsat: 6.19s) +CPU Time : 99.828s + +Choices : 2424475 (Domain: 2284371) +Conflicts : 123053 (Analyzed: 123050) +Restarts : 1407 (Average: 87.46 Last: 156) +Model-Level : 251.0 +Problems : 18 (Average Length: 30.89 Splits: 0) +Lemmas : 123050 (Deleted: 109356) + Binary : 4830 (Ratio: 3.93%) + Ternary : 1060 (Ratio: 0.86%) + Conflict : 123050 (Average Length: 740.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 123050 (Average: 18.35 Max: 543 Sum: 2257534) + Executed : 122968 (Average: 18.33 Max: 543 Sum: 2255262 Ratio: 99.90%) + Bounded : 82 (Average: 27.71 Max: 32 Sum: 2272 Ratio: 0.10%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 431164 (Eliminated: 0 Frozen: 132421) +Constraints : 3084759 (Binary: 91.2% Ternary: 6.9% Other: 1.8%) + +Memory Peak : 557MB +Max. Length : 55 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.51s +Memory: 552MB (+58MB) +UNKNOWN +Iteration Time: 8.39s + +Iteration 18 +Queue: [(13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True)] +Grounded Until: 60 +Expected Memory: 615.0MB +Grounding... [('step', [61]), ('step', [62]), ('step', [63]), ('step', [64]), ('step', [65]), ('check', [65])] +Grounding Time: 0.54s +Memory: 552MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 19 +Time : 108.976s (Solving: 96.44s 1st Model: 0.07s Unsat: 6.19s) +CPU Time : 108.888s + +Choices : 2742954 (Domain: 2597685) +Conflicts : 131174 (Analyzed: 131171) +Restarts : 1507 (Average: 87.04 Last: 156) +Model-Level : 251.0 +Problems : 19 (Average Length: 32.79 Splits: 0) +Lemmas : 131171 (Deleted: 117422) + Binary : 4855 (Ratio: 3.70%) + Ternary : 1062 (Ratio: 0.81%) + Conflict : 131171 (Average Length: 764.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 131171 (Average: 19.46 Max: 581 Sum: 2552228) + Executed : 131089 (Average: 19.44 Max: 581 Sum: 2549956 Ratio: 99.91%) + Bounded : 82 (Average: 27.71 Max: 32 Sum: 2272 Ratio: 0.09%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 468655 (Eliminated: 0 Frozen: 144081) +Constraints : 3367219 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 609MB +Max. Length : 60 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.16s +Memory: 557MB (+5MB) +UNKNOWN +Iteration Time: 9.07s + +Iteration 19 +Queue: [(14,70,0,True), (15,75,0,True), (16,80,0,True)] +Grounded Until: 65 +Expected Memory: 620.0MB +Grounding... [('step', [66]), ('step', [67]), ('step', [68]), ('step', [69]), ('step', [70]), ('check', [70])] +Grounding Time: 0.54s +Memory: 562MB (+5MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 20 +Time : 118.280s (Solving: 104.72s 1st Model: 0.07s Unsat: 6.19s) +CPU Time : 118.196s + +Choices : 3075555 (Domain: 2925291) +Conflicts : 139318 (Analyzed: 139315) +Restarts : 1607 (Average: 86.69 Last: 156) +Model-Level : 251.0 +Problems : 20 (Average Length: 34.75 Splits: 0) +Lemmas : 139315 (Deleted: 125364) + Binary : 4891 (Ratio: 3.51%) + Ternary : 1064 (Ratio: 0.76%) + Conflict : 139315 (Average Length: 786.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 139315 (Average: 20.53 Max: 627 Sum: 2860030) + Executed : 139233 (Average: 20.51 Max: 627 Sum: 2857758 Ratio: 99.92%) + Bounded : 82 (Average: 27.71 Max: 32 Sum: 2272 Ratio: 0.08%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 506146 (Eliminated: 0 Frozen: 155741) +Constraints : 3649679 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 633MB +Max. Length : 65 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.39s +Memory: 583MB (+21MB) +UNKNOWN +Iteration Time: 9.32s + +Iteration 20 +Queue: [(15,75,0,True), (16,80,0,True)] +Grounded Until: 70 +Expected Memory: 646.0MB +Grounding... [('step', [71]), ('step', [72]), ('step', [73]), ('step', [74]), ('step', [75]), ('check', [75])] +Grounding Time: 0.52s +Memory: 584MB (+1MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 21 +Time : 127.830s (Solving: 113.25s 1st Model: 0.07s Unsat: 6.19s) +CPU Time : 127.752s + +Choices : 3463794 (Domain: 3308410) +Conflicts : 147563 (Analyzed: 147560) +Restarts : 1707 (Average: 86.44 Last: 156) +Model-Level : 251.0 +Problems : 21 (Average Length: 36.76 Splits: 0) +Lemmas : 147560 (Deleted: 133359) + Binary : 4921 (Ratio: 3.33%) + Ternary : 1064 (Ratio: 0.72%) + Conflict : 147560 (Average Length: 801.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 147560 (Average: 21.84 Max: 682 Sum: 3222187) + Executed : 147478 (Average: 21.82 Max: 682 Sum: 3219915 Ratio: 99.93%) + Bounded : 82 (Average: 27.71 Max: 32 Sum: 2272 Ratio: 0.07%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 543637 (Eliminated: 0 Frozen: 167401) +Constraints : 3932139 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 666MB +Max. Length : 70 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.64s +Memory: 609MB (+25MB) +UNKNOWN +Iteration Time: 9.57s + +Iteration 21 +Queue: [(16,80,0,True)] +Grounded Until: 75 +Expected Memory: 672.0MB +Grounding... [('step', [76]), ('step', [77]), ('step', [78]), ('step', [79]), ('step', [80]), ('check', [80])] +Grounding Time: 0.53s +Memory: 609MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 22 +Time : 137.655s (Solving: 122.02s 1st Model: 0.07s Unsat: 6.19s) +CPU Time : 137.584s + +Choices : 3861148 (Domain: 3700237) +Conflicts : 155896 (Analyzed: 155893) +Restarts : 1807 (Average: 86.27 Last: 156) +Model-Level : 251.0 +Problems : 22 (Average Length: 38.82 Splits: 0) +Lemmas : 155893 (Deleted: 141480) + Binary : 4942 (Ratio: 3.17%) + Ternary : 1065 (Ratio: 0.68%) + Conflict : 155893 (Average Length: 818.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 155893 (Average: 23.04 Max: 732 Sum: 3592289) + Executed : 155811 (Average: 23.03 Max: 732 Sum: 3590017 Ratio: 99.94%) + Bounded : 82 (Average: 27.71 Max: 32 Sum: 2272 Ratio: 0.06%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 581128 (Eliminated: 0 Frozen: 179061) +Constraints : 4214599 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 694MB +Max. Length : 75 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.89s +Memory: 633MB (+24MB) +UNKNOWN +Iteration Time: 9.84s + +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 : 143.128s (Solving: 127.37s 1st Model: 0.07s Unsat: 6.19s) +CPU Time : 143.056s + +Choices : 3944840 (Domain: 3778004) +Conflicts : 164803 (Analyzed: 164800) +Restarts : 1907 (Average: 86.42 Last: 156) +Model-Level : 251.0 +Problems : 23 (Average Length: 40.70 Splits: 0) +Lemmas : 164800 (Deleted: 149207) + Binary : 5344 (Ratio: 3.24%) + Ternary : 1201 (Ratio: 0.73%) + Conflict : 164800 (Average Length: 790.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 164800 (Average: 22.26 Max: 732 Sum: 3667764) + Executed : 164713 (Average: 22.24 Max: 732 Sum: 3665082 Ratio: 99.93%) + Bounded : 87 (Average: 30.83 Max: 82 Sum: 2682 Ratio: 0.07%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 581128 (Eliminated: 0 Frozen: 179061) +Constraints : 4214599 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 694MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 5.43s +Memory: 633MB (+0MB) +UNKNOWN +Iteration Time: 5.48s + +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 : 151.500s (Solving: 135.62s 1st Model: 0.07s Unsat: 6.19s) +CPU Time : 151.432s + +Choices : 4073315 (Domain: 3899978) +Conflicts : 174025 (Analyzed: 174022) +Restarts : 2007 (Average: 86.71 Last: 156) +Model-Level : 251.0 +Problems : 24 (Average Length: 42.42 Splits: 0) +Lemmas : 174022 (Deleted: 157070) + Binary : 5843 (Ratio: 3.36%) + Ternary : 1372 (Ratio: 0.79%) + Conflict : 174022 (Average Length: 762.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 174022 (Average: 21.76 Max: 732 Sum: 3786698) + Executed : 173930 (Average: 21.74 Max: 732 Sum: 3783606 Ratio: 99.92%) + Bounded : 92 (Average: 33.61 Max: 82 Sum: 3092 Ratio: 0.08%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 581128 (Eliminated: 0 Frozen: 179061) +Constraints : 4214529 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 694MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.33s +Memory: 633MB (+0MB) +UNKNOWN +Iteration Time: 8.38s + +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 : 160.748s (Solving: 144.71s 1st Model: 0.07s Unsat: 6.19s) +CPU Time : 160.684s + +Choices : 4206834 (Domain: 4026174) +Conflicts : 183158 (Analyzed: 183155) +Restarts : 2107 (Average: 86.93 Last: 156) +Model-Level : 251.0 +Problems : 25 (Average Length: 44.00 Splits: 0) +Lemmas : 183155 (Deleted: 165457) + Binary : 6112 (Ratio: 3.34%) + Ternary : 1447 (Ratio: 0.79%) + Conflict : 183155 (Average Length: 742.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 183155 (Average: 21.34 Max: 732 Sum: 3909028) + Executed : 183061 (Average: 21.32 Max: 732 Sum: 3905772 Ratio: 99.92%) + Bounded : 94 (Average: 34.64 Max: 82 Sum: 3256 Ratio: 0.08%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 581128 (Eliminated: 0 Frozen: 179061) +Constraints : 4214460 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 694MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.20s +Memory: 633MB (+0MB) +UNKNOWN +Iteration Time: 9.26s + +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 : 169.942s (Solving: 153.78s 1st Model: 0.07s Unsat: 6.19s) +CPU Time : 169.884s + +Choices : 4339020 (Domain: 4152862) +Conflicts : 192009 (Analyzed: 192006) +Restarts : 2207 (Average: 87.00 Last: 156) +Model-Level : 251.0 +Problems : 26 (Average Length: 45.46 Splits: 0) +Lemmas : 192006 (Deleted: 174050) + Binary : 6269 (Ratio: 3.27%) + Ternary : 1477 (Ratio: 0.77%) + Conflict : 192006 (Average Length: 724.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 192006 (Average: 20.98 Max: 732 Sum: 4028203) + Executed : 191909 (Average: 20.96 Max: 732 Sum: 4024701 Ratio: 99.91%) + Bounded : 97 (Average: 36.10 Max: 82 Sum: 3502 Ratio: 0.09%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 581128 (Eliminated: 0 Frozen: 179061) +Constraints : 4214421 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 694MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.15s +Memory: 633MB (+0MB) +UNKNOWN +Iteration Time: 9.20s + +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 : 178.563s (Solving: 162.28s 1st Model: 0.07s Unsat: 6.19s) +CPU Time : 178.508s + +Choices : 4483150 (Domain: 4294988) +Conflicts : 200250 (Analyzed: 200247) +Restarts : 2307 (Average: 86.80 Last: 156) +Model-Level : 251.0 +Problems : 27 (Average Length: 46.81 Splits: 0) +Lemmas : 200247 (Deleted: 180348) + Binary : 6424 (Ratio: 3.21%) + Ternary : 1518 (Ratio: 0.76%) + Conflict : 200247 (Average Length: 706.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 200247 (Average: 20.79 Max: 732 Sum: 4162747) + Executed : 200150 (Average: 20.77 Max: 732 Sum: 4159245 Ratio: 99.92%) + Bounded : 97 (Average: 36.10 Max: 82 Sum: 3502 Ratio: 0.08%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 581128 (Eliminated: 0 Frozen: 179061) +Constraints : 4214383 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 694MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.58s +Memory: 633MB (+0MB) +UNKNOWN +Iteration Time: 8.63s + +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 : 188.806s (Solving: 172.39s 1st Model: 0.07s Unsat: 6.19s) +CPU Time : 188.756s + +Choices : 4710857 (Domain: 4518979) +Conflicts : 209443 (Analyzed: 209440) +Restarts : 2407 (Average: 87.01 Last: 156) +Model-Level : 251.0 +Problems : 28 (Average Length: 48.07 Splits: 0) +Lemmas : 209440 (Deleted: 190144) + Binary : 6772 (Ratio: 3.23%) + Ternary : 1671 (Ratio: 0.80%) + Conflict : 209440 (Average Length: 690.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 209440 (Average: 20.90 Max: 732 Sum: 4377404) + Executed : 209340 (Average: 20.88 Max: 732 Sum: 4373661 Ratio: 99.91%) + Bounded : 100 (Average: 37.43 Max: 82 Sum: 3743 Ratio: 0.09%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 581128 (Eliminated: 0 Frozen: 179061) +Constraints : 4214383 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 694MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 10.20s +Memory: 633MB (+0MB) +UNKNOWN +Iteration Time: 10.25s + +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 : 198.772s (Solving: 182.24s 1st Model: 0.07s Unsat: 6.19s) +CPU Time : 198.724s + +Choices : 4942110 (Domain: 4746373) +Conflicts : 218428 (Analyzed: 218425) +Restarts : 2507 (Average: 87.13 Last: 156) +Model-Level : 251.0 +Problems : 29 (Average Length: 49.24 Splits: 0) +Lemmas : 218425 (Deleted: 198382) + Binary : 7052 (Ratio: 3.23%) + Ternary : 1758 (Ratio: 0.80%) + Conflict : 218425 (Average Length: 672.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 218425 (Average: 21.04 Max: 732 Sum: 4594966) + Executed : 218324 (Average: 21.02 Max: 732 Sum: 4591141 Ratio: 99.92%) + Bounded : 101 (Average: 37.87 Max: 82 Sum: 3825 Ratio: 0.08%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 581128 (Eliminated: 0 Frozen: 179061) +Constraints : 4214355 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 694MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.93s +Memory: 633MB (+0MB) +UNKNOWN +Iteration Time: 9.97s + +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 : 213.776s (Solving: 197.13s 1st Model: 0.07s Unsat: 6.19s) +CPU Time : 213.736s + +Choices : 5543602 (Domain: 5335717) +Conflicts : 228019 (Analyzed: 228016) +Restarts : 2607 (Average: 87.46 Last: 156) +Model-Level : 251.0 +Problems : 30 (Average Length: 50.33 Splits: 0) +Lemmas : 228016 (Deleted: 206371) + Binary : 7863 (Ratio: 3.45%) + Ternary : 1962 (Ratio: 0.86%) + Conflict : 228016 (Average Length: 655.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 228016 (Average: 22.71 Max: 732 Sum: 5177436) + Executed : 227915 (Average: 22.69 Max: 732 Sum: 5173611 Ratio: 99.93%) + Bounded : 101 (Average: 37.87 Max: 82 Sum: 3825 Ratio: 0.07%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 581128 (Eliminated: 0 Frozen: 179061) +Constraints : 4214341 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 694MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 14.97s +Memory: 633MB (+0MB) +UNKNOWN +Iteration Time: 15.01s + +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 : 230.104s (Solving: 213.33s 1st Model: 0.07s Unsat: 6.19s) +CPU Time : 230.072s + +Choices : 5912692 (Domain: 5701705) +Conflicts : 237089 (Analyzed: 237086) +Restarts : 2707 (Average: 87.58 Last: 156) +Model-Level : 251.0 +Problems : 31 (Average Length: 51.35 Splits: 0) +Lemmas : 237086 (Deleted: 214344) + Binary : 8345 (Ratio: 3.52%) + Ternary : 2067 (Ratio: 0.87%) + Conflict : 237086 (Average Length: 642.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 237086 (Average: 23.32 Max: 732 Sum: 5529510) + Executed : 236985 (Average: 23.31 Max: 732 Sum: 5525685 Ratio: 99.93%) + Bounded : 101 (Average: 37.87 Max: 82 Sum: 3825 Ratio: 0.07%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 581128 (Eliminated: 0 Frozen: 179061) +Constraints : 4214341 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 694MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 16.29s +Memory: 633MB (+0MB) +UNKNOWN +Iteration Time: 16.34s + +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 : 247.661s (Solving: 230.77s 1st Model: 0.07s Unsat: 6.19s) +CPU Time : 247.640s + +Choices : 6355466 (Domain: 6140328) +Conflicts : 246112 (Analyzed: 246109) +Restarts : 2807 (Average: 87.68 Last: 156) +Model-Level : 251.0 +Problems : 32 (Average Length: 52.31 Splits: 0) +Lemmas : 246109 (Deleted: 222644) + Binary : 8751 (Ratio: 3.56%) + Ternary : 2149 (Ratio: 0.87%) + Conflict : 246109 (Average Length: 631.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 246109 (Average: 24.18 Max: 732 Sum: 5951293) + Executed : 246008 (Average: 24.17 Max: 732 Sum: 5947468 Ratio: 99.94%) + Bounded : 101 (Average: 37.87 Max: 82 Sum: 3825 Ratio: 0.06%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 581128 (Eliminated: 0 Frozen: 179061) +Constraints : 4214341 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 694MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 17.53s +Memory: 633MB (+0MB) +UNKNOWN +Iteration Time: 17.57s + +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 : 262.904s (Solving: 245.88s 1st Model: 0.07s Unsat: 6.19s) +CPU Time : 262.888s + +Choices : 6768299 (Domain: 6550555) +Conflicts : 254644 (Analyzed: 254641) +Restarts : 2907 (Average: 87.60 Last: 156) +Model-Level : 251.0 +Problems : 33 (Average Length: 53.21 Splits: 0) +Lemmas : 254641 (Deleted: 228922) + Binary : 9085 (Ratio: 3.57%) + Ternary : 2205 (Ratio: 0.87%) + Conflict : 254641 (Average Length: 621.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 254641 (Average: 24.91 Max: 781 Sum: 6342905) + Executed : 254540 (Average: 24.89 Max: 781 Sum: 6339080 Ratio: 99.94%) + Bounded : 101 (Average: 37.87 Max: 82 Sum: 3825 Ratio: 0.06%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 581128 (Eliminated: 0 Frozen: 179061) +Constraints : 4214341 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 694MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 15.20s +Memory: 633MB (+0MB) +UNKNOWN +Iteration Time: 15.25s + +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 : 277.295s (Solving: 260.16s 1st Model: 0.07s Unsat: 6.19s) +CPU Time : 277.284s + +Choices : 7147633 (Domain: 6925074) +Conflicts : 263491 (Analyzed: 263488) +Restarts : 3007 (Average: 87.62 Last: 156) +Model-Level : 251.0 +Problems : 34 (Average Length: 54.06 Splits: 0) +Lemmas : 263488 (Deleted: 238764) + Binary : 9400 (Ratio: 3.57%) + Ternary : 2238 (Ratio: 0.85%) + Conflict : 263488 (Average Length: 640.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 263488 (Average: 25.39 Max: 781 Sum: 6690109) + Executed : 263387 (Average: 25.38 Max: 781 Sum: 6686284 Ratio: 99.94%) + Bounded : 101 (Average: 37.87 Max: 82 Sum: 3825 Ratio: 0.06%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 581128 (Eliminated: 0 Frozen: 179061) +Constraints : 4214341 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 761MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 14.36s +Memory: 697MB (+64MB) +UNKNOWN +Iteration Time: 14.40s + +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 : 288.086s (Solving: 270.81s 1st Model: 0.07s Unsat: 6.19s) +CPU Time : 288.076s + +Choices : 7331654 (Domain: 7108520) +Conflicts : 271441 (Analyzed: 271438) +Restarts : 3107 (Average: 87.36 Last: 156) +Model-Level : 251.0 +Problems : 35 (Average Length: 54.86 Splits: 0) +Lemmas : 271438 (Deleted: 245100) + Binary : 9510 (Ratio: 3.50%) + Ternary : 2261 (Ratio: 0.83%) + Conflict : 271438 (Average Length: 628.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 271438 (Average: 25.28 Max: 781 Sum: 6860706) + Executed : 271336 (Average: 25.26 Max: 781 Sum: 6856799 Ratio: 99.94%) + Bounded : 102 (Average: 38.30 Max: 82 Sum: 3907 Ratio: 0.06%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 581128 (Eliminated: 0 Frozen: 179061) +Constraints : 4214341 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 761MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 10.74s +Memory: 697MB (+0MB) +UNKNOWN +Iteration Time: 10.80s + +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: 760.0MB +Grounding... [('step', [81]), ('step', [82]), ('step', [83]), ('step', [84]), ('step', [85]), ('check', [85])] +Grounding Time: 0.54s +Memory: 697MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 36 +Time : 304.557s (Solving: 286.20s 1st Model: 0.07s Unsat: 6.19s) +CPU Time : 304.556s + +Choices : 7852212 (Domain: 7625348) +Conflicts : 281214 (Analyzed: 281211) +Restarts : 3207 (Average: 87.69 Last: 156) +Model-Level : 251.0 +Problems : 36 (Average Length: 55.75 Splits: 0) +Lemmas : 281211 (Deleted: 255259) + Binary : 9793 (Ratio: 3.48%) + Ternary : 2331 (Ratio: 0.83%) + Conflict : 281211 (Average Length: 630.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 281211 (Average: 26.14 Max: 859 Sum: 7351427) + Executed : 281109 (Average: 26.13 Max: 859 Sum: 7347520 Ratio: 99.95%) + Bounded : 102 (Average: 38.30 Max: 82 Sum: 3907 Ratio: 0.05%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 618619 (Eliminated: 0 Frozen: 190721) +Constraints : 4496787 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 784MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 15.52s +Memory: 719MB (+22MB) +UNKNOWN +Iteration Time: 16.49s + +Iteration 36 +Queue: [(18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 85 +Expected Memory: 782.0MB +Grounding... [('step', [86]), ('step', [87]), ('step', [88]), ('step', [89]), ('step', [90]), ('check', [90])] +Grounding Time: 0.55s +Memory: 719MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 37 +Time : 319.373s (Solving: 299.88s 1st Model: 0.07s Unsat: 6.19s) +CPU Time : 319.376s + +Choices : 8188396 (Domain: 7959985) +Conflicts : 289503 (Analyzed: 289500) +Restarts : 3307 (Average: 87.54 Last: 156) +Model-Level : 251.0 +Problems : 37 (Average Length: 56.73 Splits: 0) +Lemmas : 289500 (Deleted: 263146) + Binary : 9950 (Ratio: 3.44%) + Ternary : 2354 (Ratio: 0.81%) + Conflict : 289500 (Average Length: 641.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 289500 (Average: 26.44 Max: 886 Sum: 7653554) + Executed : 289398 (Average: 26.42 Max: 886 Sum: 7649647 Ratio: 99.95%) + Bounded : 102 (Average: 38.30 Max: 82 Sum: 3907 Ratio: 0.05%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 656110 (Eliminated: 0 Frozen: 202381) +Constraints : 4779247 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 811MB +Max. Length : 85 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 13.81s +Memory: 799MB (+80MB) +UNKNOWN +Iteration Time: 14.83s + +Iteration 37 +Queue: [(19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 90 +Expected Memory: 879.0MB +Grounding... [('step', [91]), ('step', [92]), ('step', [93]), ('step', [94]), ('step', [95]), ('check', [95])] +Grounding Time: 0.57s +Memory: 799MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 38 +Time : 333.411s (Solving: 312.75s 1st Model: 0.07s Unsat: 6.19s) +CPU Time : 333.420s + +Choices : 8440963 (Domain: 8211293) +Conflicts : 297935 (Analyzed: 297932) +Restarts : 3407 (Average: 87.45 Last: 156) +Model-Level : 251.0 +Problems : 38 (Average Length: 57.79 Splits: 0) +Lemmas : 297932 (Deleted: 271843) + Binary : 10074 (Ratio: 3.38%) + Ternary : 2387 (Ratio: 0.80%) + Conflict : 297932 (Average Length: 655.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 297932 (Average: 26.42 Max: 1023 Sum: 7872147) + Executed : 297830 (Average: 26.41 Max: 1023 Sum: 7868240 Ratio: 99.95%) + Bounded : 102 (Average: 38.30 Max: 82 Sum: 3907 Ratio: 0.05%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 693601 (Eliminated: 0 Frozen: 214041) +Constraints : 5061707 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 884MB +Max. Length : 90 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 13.01s +Memory: 803MB (+4MB) +UNKNOWN +Iteration Time: 14.05s + +Iteration 38 +Queue: [(20,100,0,True), (21,105,0,True)] +Grounded Until: 95 +Expected Memory: 883.0MB +Grounding... [('step', [96]), ('step', [97]), ('step', [98]), ('step', [99]), ('step', [100]), ('check', [100])] +Grounding Time: 0.89s +Memory: 854MB (+51MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 39 +Time : 347.630s (Solving: 325.49s 1st Model: 0.07s Unsat: 6.19s) +CPU Time : 347.644s + +Choices : 8659704 (Domain: 8429461) +Conflicts : 306292 (Analyzed: 306289) +Restarts : 3507 (Average: 87.34 Last: 156) +Model-Level : 251.0 +Problems : 39 (Average Length: 58.92 Splits: 0) +Lemmas : 306289 (Deleted: 280030) + Binary : 10188 (Ratio: 3.33%) + Ternary : 2407 (Ratio: 0.79%) + Conflict : 306289 (Average Length: 666.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 306289 (Average: 26.30 Max: 1023 Sum: 8055366) + Executed : 306187 (Average: 26.29 Max: 1023 Sum: 8051459 Ratio: 99.95%) + Bounded : 102 (Average: 38.30 Max: 82 Sum: 3907 Ratio: 0.05%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 731092 (Eliminated: 0 Frozen: 225701) +Constraints : 5344167 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 943MB +Max. Length : 95 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 12.87s +Memory: 858MB (+4MB) +UNKNOWN +Iteration Time: 14.24s + +Iteration 39 +Queue: [(21,105,0,True)] +Grounded Until: 100 +Expected Memory: 938.0MB +Grounding... [('step', [101]), ('step', [102]), ('step', [103]), ('step', [104]), ('step', [105]), ('check', [105])] +Grounding Time: 0.52s +Memory: 858MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 40 +Time : 359.992s (Solving: 336.71s 1st Model: 0.07s Unsat: 6.19s) +CPU Time : 360.012s + +Choices : 8821634 (Domain: 8591315) +Conflicts : 314575 (Analyzed: 314572) +Restarts : 3607 (Average: 87.21 Last: 156) +Model-Level : 251.0 +Problems : 40 (Average Length: 60.12 Splits: 0) +Lemmas : 314572 (Deleted: 288205) + Binary : 10258 (Ratio: 3.26%) + Ternary : 2414 (Ratio: 0.77%) + Conflict : 314572 (Average Length: 681.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 314572 (Average: 26.01 Max: 1023 Sum: 8181575) + Executed : 314470 (Average: 26.00 Max: 1023 Sum: 8177668 Ratio: 99.95%) + Bounded : 102 (Average: 38.30 Max: 82 Sum: 3907 Ratio: 0.05%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 768583 (Eliminated: 0 Frozen: 237361) +Constraints : 5626627 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 953MB +Max. Length : 100 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 11.37s +Memory: 868MB (+10MB) +UNKNOWN +Iteration Time: 12.38s + +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 : 365.716s (Solving: 342.26s 1st Model: 0.07s Unsat: 11.73s) +CPU Time : 365.740s + +Choices : 8873173 (Domain: 8642854) +Conflicts : 319882 (Analyzed: 319878) +Restarts : 3672 (Average: 87.11 Last: 156) +Model-Level : 251.0 +Problems : 41 (Average Length: 61.27 Splits: 0) +Lemmas : 319878 (Deleted: 293629) + Binary : 10410 (Ratio: 3.25%) + Ternary : 2446 (Ratio: 0.76%) + Conflict : 319878 (Average Length: 675.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 319878 (Average: 25.73 Max: 1023 Sum: 8232011) + Executed : 319768 (Average: 25.72 Max: 1023 Sum: 8227990 Ratio: 99.95%) + Bounded : 110 (Average: 36.55 Max: 107 Sum: 4021 Ratio: 0.05%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 768583 (Eliminated: 0 Frozen: 237361) +Constraints : 5626627 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 953MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 5.66s +Memory: 872MB (+4MB) +UNSAT +Iteration Time: 5.73s + +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 : 370.558s (Solving: 346.95s 1st Model: 0.07s Unsat: 11.73s) +CPU Time : 370.580s + +Choices : 8920227 (Domain: 8689908) +Conflicts : 327253 (Analyzed: 327249) +Restarts : 3772 (Average: 86.76 Last: 156) +Model-Level : 251.0 +Problems : 42 (Average Length: 62.36 Splits: 0) +Lemmas : 327249 (Deleted: 298682) + Binary : 10504 (Ratio: 3.21%) + Ternary : 2480 (Ratio: 0.76%) + Conflict : 327249 (Average Length: 667.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 327249 (Average: 25.28 Max: 1023 Sum: 8272642) + Executed : 327137 (Average: 25.27 Max: 1023 Sum: 8268407 Ratio: 99.95%) + Bounded : 112 (Average: 37.81 Max: 107 Sum: 4235 Ratio: 0.05%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 768583 (Eliminated: 0 Frozen: 237361) +Constraints : 5626613 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 953MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 4.80s +Memory: 872MB (+0MB) +UNKNOWN +Iteration Time: 4.85s + +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 : 376.030s (Solving: 352.27s 1st Model: 0.07s Unsat: 11.73s) +CPU Time : 376.056s + +Choices : 8957184 (Domain: 8726865) +Conflicts : 335518 (Analyzed: 335514) +Restarts : 3872 (Average: 86.65 Last: 156) +Model-Level : 251.0 +Problems : 43 (Average Length: 63.40 Splits: 0) +Lemmas : 335514 (Deleted: 305695) + Binary : 10555 (Ratio: 3.15%) + Ternary : 2501 (Ratio: 0.75%) + Conflict : 335514 (Average Length: 657.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 335514 (Average: 24.75 Max: 1023 Sum: 8302817) + Executed : 335399 (Average: 24.73 Max: 1023 Sum: 8298267 Ratio: 99.95%) + Bounded : 115 (Average: 39.57 Max: 107 Sum: 4550 Ratio: 0.05%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 768583 (Eliminated: 0 Frozen: 237361) +Constraints : 5626573 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 953MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 5.42s +Memory: 872MB (+0MB) +UNKNOWN +Iteration Time: 5.48s + +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 : 382.072s (Solving: 358.13s 1st Model: 0.07s Unsat: 11.73s) +CPU Time : 382.100s + +Choices : 9012585 (Domain: 8781888) +Conflicts : 343292 (Analyzed: 343288) +Restarts : 3972 (Average: 86.43 Last: 156) +Model-Level : 251.0 +Problems : 44 (Average Length: 64.39 Splits: 0) +Lemmas : 343288 (Deleted: 313547) + Binary : 10635 (Ratio: 3.10%) + Ternary : 2523 (Ratio: 0.73%) + Conflict : 343288 (Average Length: 649.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 343288 (Average: 24.33 Max: 1023 Sum: 8350864) + Executed : 343171 (Average: 24.31 Max: 1023 Sum: 8346105 Ratio: 99.94%) + Bounded : 117 (Average: 40.68 Max: 107 Sum: 4759 Ratio: 0.06%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 768583 (Eliminated: 0 Frozen: 237361) +Constraints : 5626545 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 953MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 5.98s +Memory: 872MB (+0MB) +UNKNOWN +Iteration Time: 6.05s + +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 : 389.462s (Solving: 365.37s 1st Model: 0.07s Unsat: 11.73s) +CPU Time : 389.492s + +Choices : 9099779 (Domain: 8867922) +Conflicts : 351879 (Analyzed: 351875) +Restarts : 4072 (Average: 86.41 Last: 156) +Model-Level : 251.0 +Problems : 45 (Average Length: 65.33 Splits: 0) +Lemmas : 351875 (Deleted: 320980) + Binary : 10718 (Ratio: 3.05%) + Ternary : 2524 (Ratio: 0.72%) + Conflict : 351875 (Average Length: 639.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 351875 (Average: 23.95 Max: 1023 Sum: 8427989) + Executed : 351758 (Average: 23.94 Max: 1023 Sum: 8423230 Ratio: 99.94%) + Bounded : 117 (Average: 40.68 Max: 107 Sum: 4759 Ratio: 0.06%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 768583 (Eliminated: 0 Frozen: 237361) +Constraints : 5626532 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 953MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.34s +Memory: 872MB (+0MB) +UNKNOWN +Iteration Time: 7.39s + +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 : 397.083s (Solving: 372.84s 1st Model: 0.07s Unsat: 11.73s) +CPU Time : 397.116s + +Choices : 9175045 (Domain: 8942781) +Conflicts : 359970 (Analyzed: 359966) +Restarts : 4172 (Average: 86.28 Last: 156) +Model-Level : 251.0 +Problems : 46 (Average Length: 66.24 Splits: 0) +Lemmas : 359966 (Deleted: 329350) + Binary : 10809 (Ratio: 3.00%) + Ternary : 2532 (Ratio: 0.70%) + Conflict : 359966 (Average Length: 630.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 359966 (Average: 23.59 Max: 1023 Sum: 8491221) + Executed : 359848 (Average: 23.58 Max: 1023 Sum: 8486355 Ratio: 99.94%) + Bounded : 118 (Average: 41.24 Max: 107 Sum: 4866 Ratio: 0.06%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 768583 (Eliminated: 0 Frozen: 237361) +Constraints : 5626532 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 953MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.58s +Memory: 872MB (+0MB) +UNKNOWN +Iteration Time: 7.63s + +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 : 404.461s (Solving: 380.07s 1st Model: 0.07s Unsat: 11.73s) +CPU Time : 404.496s + +Choices : 9267150 (Domain: 9034455) +Conflicts : 368151 (Analyzed: 368147) +Restarts : 4272 (Average: 86.18 Last: 156) +Model-Level : 251.0 +Problems : 47 (Average Length: 67.11 Splits: 0) +Lemmas : 368147 (Deleted: 337169) + Binary : 10863 (Ratio: 2.95%) + Ternary : 2547 (Ratio: 0.69%) + Conflict : 368147 (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 : 368147 (Average: 23.29 Max: 1023 Sum: 8572935) + Executed : 368029 (Average: 23.27 Max: 1023 Sum: 8568069 Ratio: 99.94%) + Bounded : 118 (Average: 41.24 Max: 107 Sum: 4866 Ratio: 0.06%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 768583 (Eliminated: 0 Frozen: 237361) +Constraints : 5626519 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 953MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.33s +Memory: 872MB (+0MB) +UNKNOWN +Iteration Time: 7.38s + +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 : 412.856s (Solving: 388.31s 1st Model: 0.07s Unsat: 11.73s) +CPU Time : 412.892s + +Choices : 9404999 (Domain: 9171074) +Conflicts : 376181 (Analyzed: 376177) +Restarts : 4372 (Average: 86.04 Last: 156) +Model-Level : 251.0 +Problems : 48 (Average Length: 67.94 Splits: 0) +Lemmas : 376177 (Deleted: 344901) + Binary : 10984 (Ratio: 2.92%) + Ternary : 2581 (Ratio: 0.69%) + Conflict : 376177 (Average Length: 613.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 376177 (Average: 23.12 Max: 1023 Sum: 8698808) + Executed : 376058 (Average: 23.11 Max: 1023 Sum: 8693835 Ratio: 99.94%) + Bounded : 119 (Average: 41.79 Max: 107 Sum: 4973 Ratio: 0.06%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 768583 (Eliminated: 0 Frozen: 237361) +Constraints : 5626519 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 953MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.35s +Memory: 872MB (+0MB) +UNKNOWN +Iteration Time: 8.40s + +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 : 420.928s (Solving: 396.23s 1st Model: 0.07s Unsat: 11.73s) +CPU Time : 420.968s + +Choices : 9505662 (Domain: 9271445) +Conflicts : 384278 (Analyzed: 384274) +Restarts : 4472 (Average: 85.93 Last: 156) +Model-Level : 251.0 +Problems : 49 (Average Length: 68.73 Splits: 0) +Lemmas : 384274 (Deleted: 352566) + Binary : 11089 (Ratio: 2.89%) + Ternary : 2603 (Ratio: 0.68%) + Conflict : 384274 (Average Length: 606.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 384274 (Average: 22.87 Max: 1023 Sum: 8788887) + Executed : 384154 (Average: 22.86 Max: 1023 Sum: 8783810 Ratio: 99.94%) + Bounded : 120 (Average: 42.31 Max: 107 Sum: 5077 Ratio: 0.06%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 768583 (Eliminated: 0 Frozen: 237361) +Constraints : 5624066 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 953MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.02s +Memory: 872MB (+0MB) +UNKNOWN +Iteration Time: 8.08s + +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 : 427.806s (Solving: 402.93s 1st Model: 0.07s Unsat: 11.73s) +CPU Time : 427.848s + +Choices : 9625963 (Domain: 9391270) +Conflicts : 392459 (Analyzed: 392455) +Restarts : 4572 (Average: 85.84 Last: 156) +Model-Level : 251.0 +Problems : 50 (Average Length: 69.50 Splits: 0) +Lemmas : 392455 (Deleted: 360317) + Binary : 11167 (Ratio: 2.85%) + Ternary : 2619 (Ratio: 0.67%) + Conflict : 392455 (Average Length: 598.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 392455 (Average: 22.67 Max: 1023 Sum: 8896777) + Executed : 392334 (Average: 22.66 Max: 1023 Sum: 8891593 Ratio: 99.94%) + Bounded : 121 (Average: 42.84 Max: 107 Sum: 5184 Ratio: 0.06%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 768583 (Eliminated: 0 Frozen: 237361) +Constraints : 5624066 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 953MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.82s +Memory: 872MB (+0MB) +UNKNOWN +Iteration Time: 6.88s + +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 : 435.846s (Solving: 410.82s 1st Model: 0.07s Unsat: 11.73s) +CPU Time : 435.892s + +Choices : 9779433 (Domain: 9544044) +Conflicts : 400194 (Analyzed: 400190) +Restarts : 4672 (Average: 85.66 Last: 156) +Model-Level : 251.0 +Problems : 51 (Average Length: 70.24 Splits: 0) +Lemmas : 400190 (Deleted: 368168) + Binary : 11259 (Ratio: 2.81%) + Ternary : 2634 (Ratio: 0.66%) + Conflict : 400190 (Average Length: 591.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 400190 (Average: 22.58 Max: 1023 Sum: 9035408) + Executed : 400069 (Average: 22.56 Max: 1023 Sum: 9030224 Ratio: 99.94%) + Bounded : 121 (Average: 42.84 Max: 107 Sum: 5184 Ratio: 0.06%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 768583 (Eliminated: 0 Frozen: 237361) +Constraints : 5624052 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 953MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.99s +Memory: 872MB (+0MB) +UNKNOWN +Iteration Time: 8.05s + +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 : 446.075s (Solving: 420.90s 1st Model: 0.07s Unsat: 11.73s) +CPU Time : 446.116s + +Choices : 9905268 (Domain: 9669814) +Conflicts : 408173 (Analyzed: 408169) +Restarts : 4772 (Average: 85.53 Last: 156) +Model-Level : 251.0 +Problems : 52 (Average Length: 70.94 Splits: 0) +Lemmas : 408169 (Deleted: 375638) + Binary : 11366 (Ratio: 2.78%) + Ternary : 2653 (Ratio: 0.65%) + Conflict : 408169 (Average Length: 585.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 408169 (Average: 22.40 Max: 1023 Sum: 9142549) + Executed : 408048 (Average: 22.39 Max: 1023 Sum: 9137365 Ratio: 99.94%) + Bounded : 121 (Average: 42.84 Max: 107 Sum: 5184 Ratio: 0.06%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 768583 (Eliminated: 0 Frozen: 237361) +Constraints : 5624052 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 953MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 10.17s +Memory: 872MB (+0MB) +UNKNOWN +Iteration Time: 10.22s + +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 : 455.758s (Solving: 430.39s 1st Model: 0.07s Unsat: 11.73s) +CPU Time : 455.804s + +Choices : 10158880 (Domain: 9921926) +Conflicts : 416559 (Analyzed: 416555) +Restarts : 4872 (Average: 85.50 Last: 156) +Model-Level : 251.0 +Problems : 53 (Average Length: 71.62 Splits: 0) +Lemmas : 416555 (Deleted: 383356) + Binary : 11464 (Ratio: 2.75%) + Ternary : 2698 (Ratio: 0.65%) + Conflict : 416555 (Average Length: 579.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 416555 (Average: 22.51 Max: 1023 Sum: 9377370) + Executed : 416434 (Average: 22.50 Max: 1023 Sum: 9372186 Ratio: 99.94%) + Bounded : 121 (Average: 42.84 Max: 107 Sum: 5184 Ratio: 0.06%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 768583 (Eliminated: 0 Frozen: 237361) +Constraints : 5624052 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 953MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.61s +Memory: 872MB (+0MB) +UNKNOWN +Iteration Time: 9.69s + +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 : 463.893s (Solving: 438.34s 1st Model: 0.07s Unsat: 11.73s) +CPU Time : 463.940s + +Choices : 10300002 (Domain: 10061882) +Conflicts : 424673 (Analyzed: 424669) +Restarts : 4972 (Average: 85.41 Last: 156) +Model-Level : 251.0 +Problems : 54 (Average Length: 72.28 Splits: 0) +Lemmas : 424669 (Deleted: 391322) + Binary : 11509 (Ratio: 2.71%) + Ternary : 2711 (Ratio: 0.64%) + Conflict : 424669 (Average Length: 573.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 424669 (Average: 22.38 Max: 1023 Sum: 9502950) + Executed : 424546 (Average: 22.36 Max: 1023 Sum: 9497557 Ratio: 99.94%) + Bounded : 123 (Average: 43.85 Max: 107 Sum: 5393 Ratio: 0.06%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 768583 (Eliminated: 0 Frozen: 237361) +Constraints : 5624052 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 953MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.07s +Memory: 872MB (+0MB) +UNKNOWN +Iteration Time: 8.14s + +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 : 470.272s (Solving: 444.57s 1st Model: 0.07s Unsat: 11.73s) +CPU Time : 470.320s + +Choices : 10426836 (Domain: 10188457) +Conflicts : 432581 (Analyzed: 432577) +Restarts : 5072 (Average: 85.29 Last: 156) +Model-Level : 251.0 +Problems : 55 (Average Length: 72.91 Splits: 0) +Lemmas : 432577 (Deleted: 399214) + Binary : 11536 (Ratio: 2.67%) + Ternary : 2722 (Ratio: 0.63%) + Conflict : 432577 (Average Length: 568.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 432577 (Average: 22.23 Max: 1023 Sum: 9614354) + Executed : 432453 (Average: 22.21 Max: 1023 Sum: 9608857 Ratio: 99.94%) + Bounded : 124 (Average: 44.33 Max: 107 Sum: 5497 Ratio: 0.06%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 768583 (Eliminated: 0 Frozen: 237361) +Constraints : 5624038 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 953MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.33s +Memory: 872MB (+0MB) +UNKNOWN +Iteration Time: 6.38s + +Iteration 55 +Queue: [(22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Expected Memory: 952.0MB +Grounding... [('step', [106]), ('step', [107]), ('step', [108]), ('step', [109]), ('step', [110]), ('check', [110])] +Grounding Time: 0.53s +Memory: 874MB (+2MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 56 +Time : 484.717s (Solving: 457.82s 1st Model: 0.07s Unsat: 11.73s) +CPU Time : 484.772s + +Choices : 10668740 (Domain: 10429909) +Conflicts : 441287 (Analyzed: 441283) +Restarts : 5172 (Average: 85.32 Last: 156) +Model-Level : 251.0 +Problems : 56 (Average Length: 73.61 Splits: 0) +Lemmas : 441283 (Deleted: 409052) + Binary : 11634 (Ratio: 2.64%) + Ternary : 2724 (Ratio: 0.62%) + Conflict : 441283 (Average Length: 572.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 441283 (Average: 22.25 Max: 1075 Sum: 9820081) + Executed : 441159 (Average: 22.24 Max: 1075 Sum: 9814584 Ratio: 99.94%) + Bounded : 124 (Average: 44.33 Max: 107 Sum: 5497 Ratio: 0.06%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 806074 (Eliminated: 0 Frozen: 249021) +Constraints : 5906498 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 987MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 13.41s +Memory: 902MB (+28MB) +UNKNOWN +Iteration Time: 14.46s + +Iteration 56 +Queue: [(23,115,0,True)] +Grounded Until: 110 +Expected Memory: 982.0MB +Grounding... [('step', [111]), ('step', [112]), ('step', [113]), ('step', [114]), ('step', [115]), ('check', [115])] +Grounding Time: 0.53s +Memory: 902MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 57 +Time : 495.871s (Solving: 467.77s 1st Model: 0.07s Unsat: 11.73s) +CPU Time : 495.916s + +Choices : 10772507 (Domain: 10533671) +Conflicts : 449452 (Analyzed: 449448) +Restarts : 5272 (Average: 85.25 Last: 156) +Model-Level : 251.0 +Problems : 57 (Average Length: 74.37 Splits: 0) +Lemmas : 449448 (Deleted: 416419) + Binary : 11660 (Ratio: 2.59%) + Ternary : 2727 (Ratio: 0.61%) + Conflict : 449448 (Average Length: 582.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 449448 (Average: 21.99 Max: 1075 Sum: 9884708) + Executed : 449324 (Average: 21.98 Max: 1075 Sum: 9879211 Ratio: 99.94%) + Bounded : 124 (Average: 44.33 Max: 107 Sum: 5497 Ratio: 0.06%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 843565 (Eliminated: 0 Frozen: 260681) +Constraints : 6188958 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1016MB +Max. Length : 110 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 10.08s +Memory: 917MB (+15MB) +UNKNOWN +Iteration Time: 11.16s + +Iteration 57 +Queue: [(5,25,4,True), (6,30,4,True), (7,35,3,True), (8,40,3,True), (9,45,3,True), (10,50,3,True), (11,55,3,True), (12,60,3,False), (13,65,3,False), (14,70,2,True), (15,75,2,True), (16,80,2,True), (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), (24,120,0,True)] +Grounded Until: 115 +Blocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 58 +Time : 499.255s (Solving: 470.95s 1st Model: 0.07s Unsat: 11.73s) +CPU Time : 499.300s + +Choices : 10812374 (Domain: 10573538) +Conflicts : 456821 (Analyzed: 456817) +Restarts : 5372 (Average: 85.04 Last: 156) +Model-Level : 251.0 +Problems : 58 (Average Length: 75.10 Splits: 0) +Lemmas : 456817 (Deleted: 423390) + Binary : 11706 (Ratio: 2.56%) + Ternary : 2735 (Ratio: 0.60%) + Conflict : 456817 (Average Length: 576.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 456817 (Average: 21.71 Max: 1075 Sum: 9919018) + Executed : 456692 (Average: 21.70 Max: 1075 Sum: 9913409 Ratio: 99.94%) + Bounded : 125 (Average: 44.87 Max: 112 Sum: 5609 Ratio: 0.06%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 843565 (Eliminated: 0 Frozen: 260681) +Constraints : 6188958 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1016MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 3.31s +Memory: 927MB (+10MB) +UNKNOWN +Iteration Time: 3.39s + +Iteration 58 +Queue: [(6,30,4,True), (7,35,3,True), (8,40,3,True), (9,45,3,True), (10,50,3,True), (11,55,3,True), (12,60,3,False), (13,65,3,False), (14,70,2,True), (15,75,2,True), (16,80,2,True), (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), (24,120,0,True)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 59 +Time : 503.796s (Solving: 475.31s 1st Model: 0.07s Unsat: 11.73s) +CPU Time : 503.844s + +Choices : 10858072 (Domain: 10619236) +Conflicts : 464736 (Analyzed: 464732) +Restarts : 5472 (Average: 84.93 Last: 156) +Model-Level : 251.0 +Problems : 59 (Average Length: 75.81 Splits: 0) +Lemmas : 464732 (Deleted: 430527) + Binary : 11723 (Ratio: 2.52%) + Ternary : 2749 (Ratio: 0.59%) + Conflict : 464732 (Average Length: 571.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 464732 (Average: 21.43 Max: 1075 Sum: 9957893) + Executed : 464605 (Average: 21.41 Max: 1075 Sum: 9952058 Ratio: 99.94%) + Bounded : 127 (Average: 45.94 Max: 114 Sum: 5835 Ratio: 0.06%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 843565 (Eliminated: 0 Frozen: 260681) +Constraints : 6188958 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1016MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 4.48s +Memory: 927MB (+0MB) +UNKNOWN +Iteration Time: 4.55s + +Iteration 59 +Queue: [(7,35,3,True), (8,40,3,True), (9,45,3,True), (10,50,3,True), (11,55,3,True), (12,60,3,False), (13,65,3,False), (14,70,2,True), (15,75,2,True), (16,80,2,True), (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), (24,120,0,True)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 60 +Time : 509.698s (Solving: 481.03s 1st Model: 0.07s Unsat: 11.73s) +CPU Time : 509.748s + +Choices : 10938343 (Domain: 10698726) +Conflicts : 473005 (Analyzed: 473001) +Restarts : 5572 (Average: 84.89 Last: 156) +Model-Level : 251.0 +Problems : 60 (Average Length: 76.50 Splits: 0) +Lemmas : 473001 (Deleted: 438128) + Binary : 11839 (Ratio: 2.50%) + Ternary : 2762 (Ratio: 0.58%) + Conflict : 473001 (Average Length: 566.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 473001 (Average: 21.20 Max: 1075 Sum: 10029310) + Executed : 472874 (Average: 21.19 Max: 1075 Sum: 10023475 Ratio: 99.94%) + Bounded : 127 (Average: 45.94 Max: 114 Sum: 5835 Ratio: 0.06%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 843565 (Eliminated: 0 Frozen: 260681) +Constraints : 6188958 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1016MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 5.83s +Memory: 927MB (+0MB) +UNKNOWN +Iteration Time: 5.91s + +Iteration 60 +Queue: [(8,40,3,True), (9,45,3,True), (10,50,3,True), (11,55,3,True), (12,60,3,False), (13,65,3,False), (14,70,2,True), (15,75,2,True), (16,80,2,True), (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), (24,120,0,True)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 61 +Time : 517.744s (Solving: 488.91s 1st Model: 0.07s Unsat: 11.73s) +CPU Time : 517.800s + +Choices : 11034827 (Domain: 10794716) +Conflicts : 481513 (Analyzed: 481509) +Restarts : 5672 (Average: 84.89 Last: 156) +Model-Level : 251.0 +Problems : 61 (Average Length: 77.16 Splits: 0) +Lemmas : 481509 (Deleted: 446167) + Binary : 11939 (Ratio: 2.48%) + Ternary : 2780 (Ratio: 0.58%) + Conflict : 481509 (Average Length: 561.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 481509 (Average: 21.01 Max: 1075 Sum: 10115598) + Executed : 481382 (Average: 21.00 Max: 1075 Sum: 10109763 Ratio: 99.94%) + Bounded : 127 (Average: 45.94 Max: 114 Sum: 5835 Ratio: 0.06%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 843565 (Eliminated: 0 Frozen: 260681) +Constraints : 6188958 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1016MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.99s +Memory: 927MB (+0MB) +UNKNOWN +Iteration Time: 8.05s + +Iteration 61 +Queue: [(9,45,3,True), (10,50,3,True), (11,55,3,True), (12,60,3,False), (13,65,3,False), (14,70,2,True), (15,75,2,True), (16,80,2,True), (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), (24,120,0,True)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 62 +Time : 521.594s (Solving: 492.59s 1st Model: 0.07s Unsat: 11.73s) +CPU Time : 521.652s + +Choices : 11082265 (Domain: 10842139) +Conflicts : 488820 (Analyzed: 488816) +Restarts : 5772 (Average: 84.69 Last: 156) +Model-Level : 251.0 +Problems : 62 (Average Length: 77.81 Splits: 0) +Lemmas : 488816 (Deleted: 454353) + Binary : 11995 (Ratio: 2.45%) + Ternary : 2789 (Ratio: 0.57%) + Conflict : 488816 (Average Length: 556.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 488816 (Average: 20.77 Max: 1075 Sum: 10152675) + Executed : 488689 (Average: 20.76 Max: 1075 Sum: 10146840 Ratio: 99.94%) + Bounded : 127 (Average: 45.94 Max: 114 Sum: 5835 Ratio: 0.06%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 843565 (Eliminated: 0 Frozen: 260681) +Constraints : 6188958 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1016MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 3.80s +Memory: 927MB (+0MB) +UNKNOWN +Iteration Time: 3.85s + +Iteration 62 +Queue: [(10,50,3,True), (11,55,3,True), (12,60,3,False), (13,65,3,False), (14,70,2,True), (15,75,2,True), (16,80,2,True), (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), (24,120,0,True)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 63 +Time : 530.749s (Solving: 501.56s 1st Model: 0.07s Unsat: 11.73s) +CPU Time : 530.812s + +Choices : 11222325 (Domain: 10981354) +Conflicts : 497837 (Analyzed: 497833) +Restarts : 5872 (Average: 84.78 Last: 156) +Model-Level : 251.0 +Problems : 63 (Average Length: 78.43 Splits: 0) +Lemmas : 497833 (Deleted: 463546) + Binary : 12171 (Ratio: 2.44%) + Ternary : 2808 (Ratio: 0.56%) + Conflict : 497833 (Average Length: 552.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 497833 (Average: 20.65 Max: 1075 Sum: 10278415) + Executed : 497706 (Average: 20.63 Max: 1075 Sum: 10272580 Ratio: 99.94%) + Bounded : 127 (Average: 45.94 Max: 114 Sum: 5835 Ratio: 0.06%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 843565 (Eliminated: 0 Frozen: 260681) +Constraints : 6188958 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1016MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.09s +Memory: 927MB (+0MB) +UNKNOWN +Iteration Time: 9.16s + +Iteration 63 +Queue: [(11,55,3,True), (12,60,3,False), (13,65,3,False), (14,70,2,True), (15,75,2,True), (16,80,2,True), (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), (24,120,0,True)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 64 +Time : 537.295s (Solving: 507.89s 1st Model: 0.07s Unsat: 11.73s) +CPU Time : 537.360s + +Choices : 11306159 (Domain: 11064750) +Conflicts : 506280 (Analyzed: 506276) +Restarts : 5972 (Average: 84.77 Last: 156) +Model-Level : 251.0 +Problems : 64 (Average Length: 79.03 Splits: 0) +Lemmas : 506276 (Deleted: 470056) + Binary : 12234 (Ratio: 2.42%) + Ternary : 2820 (Ratio: 0.56%) + Conflict : 506276 (Average Length: 548.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 506276 (Average: 20.44 Max: 1075 Sum: 10350693) + Executed : 506148 (Average: 20.43 Max: 1075 Sum: 10344741 Ratio: 99.94%) + Bounded : 128 (Average: 46.50 Max: 117 Sum: 5952 Ratio: 0.06%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 843565 (Eliminated: 0 Frozen: 260681) +Constraints : 6188958 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1016MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.47s +Memory: 927MB (+0MB) +UNKNOWN +Iteration Time: 6.55s + +Iteration 64 +Queue: [(14,70,2,True), (15,75,2,True), (16,80,2,True), (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), (24,120,0,True)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 65 +Time : 544.810s (Solving: 515.24s 1st Model: 0.07s Unsat: 11.73s) +CPU Time : 544.880s + +Choices : 11455247 (Domain: 11212748) +Conflicts : 514387 (Analyzed: 514383) +Restarts : 6072 (Average: 84.71 Last: 156) +Model-Level : 251.0 +Problems : 65 (Average Length: 79.62 Splits: 0) +Lemmas : 514383 (Deleted: 478195) + Binary : 12351 (Ratio: 2.40%) + Ternary : 2841 (Ratio: 0.55%) + Conflict : 514383 (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 : 514383 (Average: 20.38 Max: 1075 Sum: 10484475) + Executed : 514255 (Average: 20.37 Max: 1075 Sum: 10478523 Ratio: 99.94%) + Bounded : 128 (Average: 46.50 Max: 117 Sum: 5952 Ratio: 0.06%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 843565 (Eliminated: 0 Frozen: 260681) +Constraints : 6188944 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1016MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.46s +Memory: 927MB (+0MB) +UNKNOWN +Iteration Time: 7.52s + +Iteration 65 +Queue: [(15,75,2,True), (16,80,2,True), (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), (24,120,0,True)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 66 +Time : 550.994s (Solving: 521.22s 1st Model: 0.07s Unsat: 11.73s) +CPU Time : 551.056s + +Choices : 11541864 (Domain: 11299167) +Conflicts : 522560 (Analyzed: 522556) +Restarts : 6172 (Average: 84.67 Last: 156) +Model-Level : 251.0 +Problems : 66 (Average Length: 80.18 Splits: 0) +Lemmas : 522556 (Deleted: 485968) + Binary : 12433 (Ratio: 2.38%) + Ternary : 2858 (Ratio: 0.55%) + Conflict : 522556 (Average Length: 542.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 522556 (Average: 20.20 Max: 1075 Sum: 10556947) + Executed : 522428 (Average: 20.19 Max: 1075 Sum: 10550995 Ratio: 99.94%) + Bounded : 128 (Average: 46.50 Max: 117 Sum: 5952 Ratio: 0.06%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 843565 (Eliminated: 0 Frozen: 260681) +Constraints : 6188944 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1016MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.10s +Memory: 927MB (+0MB) +UNKNOWN +Iteration Time: 6.18s + +Iteration 66 +Queue: [(16,80,2,True), (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), (24,120,0,True)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 67 +Time : 559.177s (Solving: 529.20s 1st Model: 0.07s Unsat: 11.73s) +CPU Time : 559.244s + +Choices : 11708081 (Domain: 11465007) +Conflicts : 530676 (Analyzed: 530672) +Restarts : 6272 (Average: 84.61 Last: 156) +Model-Level : 251.0 +Problems : 67 (Average Length: 80.73 Splits: 0) +Lemmas : 530672 (Deleted: 493893) + Binary : 12530 (Ratio: 2.36%) + Ternary : 2875 (Ratio: 0.54%) + Conflict : 530672 (Average Length: 538.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 530672 (Average: 20.17 Max: 1075 Sum: 10705980) + Executed : 530544 (Average: 20.16 Max: 1075 Sum: 10700028 Ratio: 99.94%) + Bounded : 128 (Average: 46.50 Max: 117 Sum: 5952 Ratio: 0.06%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 843565 (Eliminated: 0 Frozen: 260681) +Constraints : 6188944 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1016MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.11s +Memory: 927MB (+0MB) +UNKNOWN +Iteration Time: 8.19s + +Iteration 67 +Queue: [(22,110,1,True), (23,115,1,True), (24,120,0,True)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 68 +Time : 568.017s (Solving: 537.87s 1st Model: 0.07s Unsat: 11.73s) +CPU Time : 568.088s + +Choices : 11908051 (Domain: 11664762) +Conflicts : 539322 (Analyzed: 539318) +Restarts : 6372 (Average: 84.64 Last: 156) +Model-Level : 251.0 +Problems : 68 (Average Length: 81.26 Splits: 0) +Lemmas : 539318 (Deleted: 503888) + Binary : 12638 (Ratio: 2.34%) + Ternary : 2884 (Ratio: 0.53%) + Conflict : 539318 (Average Length: 534.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 539318 (Average: 20.19 Max: 1075 Sum: 10886391) + Executed : 539189 (Average: 20.17 Max: 1075 Sum: 10880327 Ratio: 99.94%) + Bounded : 129 (Average: 47.01 Max: 117 Sum: 6064 Ratio: 0.06%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 843565 (Eliminated: 0 Frozen: 260681) +Constraints : 6188944 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1016MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.79s +Memory: 927MB (+0MB) +UNKNOWN +Iteration Time: 8.85s + +Iteration 68 +Queue: [(23,115,1,True), (24,120,0,True)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 69 +Time : 574.518s (Solving: 544.16s 1st Model: 0.07s Unsat: 11.73s) +CPU Time : 574.592s + +Choices : 12047760 (Domain: 11804381) +Conflicts : 548179 (Analyzed: 548175) +Restarts : 6472 (Average: 84.70 Last: 156) +Model-Level : 251.0 +Problems : 69 (Average Length: 81.78 Splits: 0) +Lemmas : 548175 (Deleted: 512269) + Binary : 12742 (Ratio: 2.32%) + Ternary : 2894 (Ratio: 0.53%) + Conflict : 548175 (Average Length: 531.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 548175 (Average: 20.08 Max: 1075 Sum: 11006343) + Executed : 548046 (Average: 20.07 Max: 1075 Sum: 11000279 Ratio: 99.94%) + Bounded : 129 (Average: 47.01 Max: 117 Sum: 6064 Ratio: 0.06%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 843565 (Eliminated: 0 Frozen: 260681) +Constraints : 6188944 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1016MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.42s +Memory: 927MB (+0MB) +UNKNOWN +Iteration Time: 6.51s + +Iteration 69 +Queue: [(24,120,0,True)] +Grounded Until: 115 +Expected Memory: 1007.0MB +Grounding... [('step', [116]), ('step', [117]), ('step', [118]), ('step', [119]), ('step', [120]), ('check', [120])] +Grounding Time: 0.55s +Memory: 927MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 70 +Time : 587.844s (Solving: 556.24s 1st Model: 0.07s Unsat: 11.73s) +CPU Time : 587.924s + +Choices : 12230896 (Domain: 11987474) +Conflicts : 557651 (Analyzed: 557647) +Restarts : 6572 (Average: 84.85 Last: 156) +Model-Level : 251.0 +Problems : 70 (Average Length: 82.36 Splits: 0) +Lemmas : 557647 (Deleted: 520972) + Binary : 12795 (Ratio: 2.29%) + Ternary : 2897 (Ratio: 0.52%) + Conflict : 557647 (Average Length: 535.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 557647 (Average: 19.99 Max: 1251 Sum: 11149909) + Executed : 557518 (Average: 19.98 Max: 1251 Sum: 11143845 Ratio: 99.95%) + Bounded : 129 (Average: 47.01 Max: 117 Sum: 6064 Ratio: 0.05%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 881056 (Eliminated: 0 Frozen: 272341) +Constraints : 6471404 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1048MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 12.23s +Memory: 945MB (+18MB) +UNKNOWN +Iteration Time: 13.34s + +Iteration 70 +Queue: [(5,25,5,True), (6,30,5,True), (7,35,4,True), (8,40,4,True), (9,45,4,True), (10,50,4,True), (11,55,4,False), (12,60,3,True), (13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,3,False), (17,85,2,True), (18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False), (24,120,1,True)] +Grounded Until: 120 +Blocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 71 +Time : 592.054s (Solving: 560.24s 1st Model: 0.07s Unsat: 11.73s) +CPU Time : 592.136s + +Choices : 12274419 (Domain: 12030997) +Conflicts : 565316 (Analyzed: 565312) +Restarts : 6672 (Average: 84.73 Last: 156) +Model-Level : 251.0 +Problems : 71 (Average Length: 82.92 Splits: 0) +Lemmas : 565312 (Deleted: 528048) + Binary : 12842 (Ratio: 2.27%) + Ternary : 2901 (Ratio: 0.51%) + Conflict : 565312 (Average Length: 531.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 565312 (Average: 19.79 Max: 1251 Sum: 11187560) + Executed : 565182 (Average: 19.78 Max: 1251 Sum: 11181379 Ratio: 99.94%) + Bounded : 130 (Average: 47.55 Max: 117 Sum: 6181 Ratio: 0.06%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 881056 (Eliminated: 0 Frozen: 272341) +Constraints : 6471404 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1048MB +Max. Length : 120 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 4.13s +Memory: 951MB (+6MB) +UNKNOWN +Iteration Time: 4.22s + +Iteration 71 +Queue: [(6,30,5,True), (7,35,4,True), (8,40,4,True), (9,45,4,True), (10,50,4,True), (11,55,4,False), (12,60,3,True), (13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,3,False), (17,85,2,True), (18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False), (24,120,1,True)] +Grounded Until: 120 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 72 +Time : 599.780s (Solving: 567.79s 1st Model: 0.07s Unsat: 11.73s) +CPU Time : 599.864s + +Choices : 12331284 (Domain: 12087862) +Conflicts : 573401 (Analyzed: 573397) +Restarts : 6772 (Average: 84.67 Last: 156) +Model-Level : 251.0 +Problems : 72 (Average Length: 83.46 Splits: 0) +Lemmas : 573397 (Deleted: 535492) + Binary : 12961 (Ratio: 2.26%) + Ternary : 2915 (Ratio: 0.51%) + Conflict : 573397 (Average Length: 543.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 573397 (Average: 19.58 Max: 1251 Sum: 11228500) + Executed : 573265 (Average: 19.57 Max: 1251 Sum: 11222075 Ratio: 99.94%) + Bounded : 132 (Average: 48.67 Max: 122 Sum: 6425 Ratio: 0.06%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 881056 (Eliminated: 0 Frozen: 272341) +Constraints : 6471404 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1048MB +Max. Length : 120 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.67s +Memory: 951MB (+0MB) +UNKNOWN +Iteration Time: 7.73s + +Iteration 72 +Queue: [(7,35,4,True), (8,40,4,True), (9,45,4,True), (10,50,4,True), (11,55,4,False), (12,60,3,True), (13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,3,False), (17,85,2,True), (18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False), (24,120,1,True)] +Grounded Until: 120 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 73 +Time : 604.310s (Solving: 572.14s 1st Model: 0.07s Unsat: 11.73s) +CPU Time : 604.396s + +Choices : 12388157 (Domain: 12143984) +Conflicts : 581175 (Analyzed: 581171) +Restarts : 6872 (Average: 84.57 Last: 156) +Model-Level : 251.0 +Problems : 73 (Average Length: 83.99 Splits: 0) +Lemmas : 581171 (Deleted: 543337) + Binary : 13009 (Ratio: 2.24%) + Ternary : 2922 (Ratio: 0.50%) + Conflict : 581171 (Average Length: 539.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 581171 (Average: 19.40 Max: 1251 Sum: 11275940) + Executed : 581039 (Average: 19.39 Max: 1251 Sum: 11269515 Ratio: 99.94%) + Bounded : 132 (Average: 48.67 Max: 122 Sum: 6425 Ratio: 0.06%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 881056 (Eliminated: 0 Frozen: 272341) +Constraints : 6468928 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1048MB +Max. Length : 120 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 4.47s +Memory: 951MB (+0MB) +UNKNOWN +Iteration Time: 4.54s + +Iteration 73 +Queue: [(8,40,4,True), (9,45,4,True), (10,50,4,True), (11,55,4,False), (12,60,3,True), (13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,3,False), (17,85,2,True), (18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False), (24,120,1,True)] +Grounded Until: 120 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 74 +Time : 609.227s (Solving: 576.85s 1st Model: 0.07s Unsat: 11.73s) +CPU Time : 609.316s + +Choices : 12450398 (Domain: 12206165) +Conflicts : 589246 (Analyzed: 589242) +Restarts : 6972 (Average: 84.52 Last: 156) +Model-Level : 251.0 +Problems : 74 (Average Length: 84.50 Splits: 0) +Lemmas : 589242 (Deleted: 550901) + Binary : 13068 (Ratio: 2.22%) + Ternary : 2941 (Ratio: 0.50%) + Conflict : 589242 (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 : 589242 (Average: 19.23 Max: 1251 Sum: 11328485) + Executed : 589110 (Average: 19.21 Max: 1251 Sum: 11322060 Ratio: 99.94%) + Bounded : 132 (Average: 48.67 Max: 122 Sum: 6425 Ratio: 0.06%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 881056 (Eliminated: 0 Frozen: 272341) +Constraints : 6468928 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1048MB +Max. Length : 120 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 4.84s +Memory: 951MB (+0MB) +UNKNOWN +Iteration Time: 4.92s + +Iteration 74 +Queue: [(9,45,4,True), (10,50,4,True), (11,55,4,False), (12,60,3,True), (13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,3,False), (17,85,2,True), (18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False), (24,120,1,True)] +Grounded Until: 120 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 75 +Time : 615.467s (Solving: 582.91s 1st Model: 0.07s Unsat: 11.73s) +CPU Time : 615.560s + +Choices : 12534348 (Domain: 12289844) +Conflicts : 597354 (Analyzed: 597350) +Restarts : 7072 (Average: 84.47 Last: 156) +Model-Level : 251.0 +Problems : 75 (Average Length: 85.00 Splits: 0) +Lemmas : 597350 (Deleted: 558717) + Binary : 13138 (Ratio: 2.20%) + Ternary : 2943 (Ratio: 0.49%) + Conflict : 597350 (Average Length: 534.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 597350 (Average: 19.09 Max: 1251 Sum: 11400868) + Executed : 597217 (Average: 19.07 Max: 1251 Sum: 11394321 Ratio: 99.94%) + Bounded : 133 (Average: 49.23 Max: 122 Sum: 6547 Ratio: 0.06%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 881056 (Eliminated: 0 Frozen: 272341) +Constraints : 6468928 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1048MB +Max. Length : 120 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.18s +Memory: 951MB (+0MB) +UNKNOWN +Iteration Time: 6.25s + +Iteration 75 +Queue: [(10,50,4,True), (11,55,4,False), (12,60,3,True), (13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,3,False), (17,85,2,True), (18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False), (24,120,1,True)] +Grounded Until: 120 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 76 +Time : 621.430s (Solving: 588.68s 1st Model: 0.07s Unsat: 11.73s) +CPU Time : 621.524s + +Choices : 12606874 (Domain: 12362239) +Conflicts : 605822 (Analyzed: 605818) +Restarts : 7172 (Average: 84.47 Last: 156) +Model-Level : 251.0 +Problems : 76 (Average Length: 85.49 Splits: 0) +Lemmas : 605818 (Deleted: 566586) + Binary : 13230 (Ratio: 2.18%) + Ternary : 2953 (Ratio: 0.49%) + Conflict : 605818 (Average Length: 530.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 605818 (Average: 18.92 Max: 1251 Sum: 11462312) + Executed : 605684 (Average: 18.91 Max: 1251 Sum: 11455643 Ratio: 99.94%) + Bounded : 134 (Average: 49.77 Max: 122 Sum: 6669 Ratio: 0.06%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 881056 (Eliminated: 0 Frozen: 272341) +Constraints : 6468915 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1048MB +Max. Length : 120 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 5.90s +Memory: 951MB (+0MB) +UNKNOWN +Iteration Time: 5.97s + +Iteration 76 +Queue: [(12,60,3,True), (13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,3,False), (17,85,2,True), (18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False), (24,120,1,True)] +Grounded Until: 120 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 77 +Time : 631.348s (Solving: 598.39s 1st Model: 0.07s Unsat: 11.73s) +CPU Time : 631.444s + +Choices : 12745085 (Domain: 12500208) +Conflicts : 615251 (Analyzed: 615247) +Restarts : 7272 (Average: 84.60 Last: 156) +Model-Level : 251.0 +Problems : 77 (Average Length: 85.96 Splits: 0) +Lemmas : 615247 (Deleted: 576945) + Binary : 13385 (Ratio: 2.18%) + Ternary : 2968 (Ratio: 0.48%) + Conflict : 615247 (Average Length: 529.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 615247 (Average: 18.83 Max: 1251 Sum: 11584576) + Executed : 615113 (Average: 18.82 Max: 1251 Sum: 11577907 Ratio: 99.94%) + Bounded : 134 (Average: 49.77 Max: 122 Sum: 6669 Ratio: 0.06%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 881056 (Eliminated: 0 Frozen: 272341) +Constraints : 6468901 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1048MB +Max. Length : 120 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.85s +Memory: 951MB (+0MB) +UNKNOWN +Iteration Time: 9.93s + +Iteration 77 +Queue: [(13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,3,False), (17,85,2,True), (18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False), (24,120,1,True)] +Grounded Until: 120 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 78 +Time : 637.526s (Solving: 604.40s 1st Model: 0.07s Unsat: 11.73s) +CPU Time : 637.616s + +Choices : 12840301 (Domain: 12595227) +Conflicts : 623777 (Analyzed: 623773) +Restarts : 7372 (Average: 84.61 Last: 156) +Model-Level : 251.0 +Problems : 78 (Average Length: 86.42 Splits: 0) +Lemmas : 623773 (Deleted: 583858) + Binary : 13468 (Ratio: 2.16%) + Ternary : 2973 (Ratio: 0.48%) + Conflict : 623773 (Average Length: 527.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 623773 (Average: 18.70 Max: 1251 Sum: 11665137) + Executed : 623639 (Average: 18.69 Max: 1251 Sum: 11658468 Ratio: 99.94%) + Bounded : 134 (Average: 49.77 Max: 122 Sum: 6669 Ratio: 0.06%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 881056 (Eliminated: 0 Frozen: 272341) +Constraints : 6468901 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1048MB +Max. Length : 120 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.11s +Memory: 951MB (+0MB) +UNKNOWN +Iteration Time: 6.17s + +Iteration 78 +Queue: [(17,85,2,True), (18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False), (24,120,1,True)] +Grounded Until: 120 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 79 +Time : 644.934s (Solving: 611.63s 1st Model: 0.07s Unsat: 11.73s) +CPU Time : 645.024s + +Choices : 12990926 (Domain: 12745618) +Conflicts : 632710 (Analyzed: 632706) +Restarts : 7472 (Average: 84.68 Last: 156) +Model-Level : 251.0 +Problems : 79 (Average Length: 86.87 Splits: 0) +Lemmas : 632706 (Deleted: 594227) + Binary : 13570 (Ratio: 2.14%) + Ternary : 2988 (Ratio: 0.47%) + Conflict : 632706 (Average Length: 525.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 632706 (Average: 18.65 Max: 1251 Sum: 11798054) + Executed : 632571 (Average: 18.64 Max: 1251 Sum: 11791263 Ratio: 99.94%) + Bounded : 135 (Average: 50.30 Max: 122 Sum: 6791 Ratio: 0.06%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 881056 (Eliminated: 0 Frozen: 272341) +Constraints : 6468901 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1048MB +Max. Length : 120 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.35s +Memory: 951MB (+0MB) +UNKNOWN +Iteration Time: 7.41s + +Iteration 79 +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), (24,120,1,True)] +Grounded Until: 120 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 80 +Time : 651.915s (Solving: 618.41s 1st Model: 0.07s Unsat: 11.73s) +CPU Time : 652.008s + +Choices : 13064093 (Domain: 12818779) +Conflicts : 640944 (Analyzed: 640940) +Restarts : 7572 (Average: 84.65 Last: 156) +Model-Level : 251.0 +Problems : 80 (Average Length: 87.31 Splits: 0) +Lemmas : 640940 (Deleted: 600744) + Binary : 13612 (Ratio: 2.12%) + Ternary : 2991 (Ratio: 0.47%) + Conflict : 640940 (Average Length: 522.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 640940 (Average: 18.50 Max: 1251 Sum: 11856447) + Executed : 640804 (Average: 18.49 Max: 1251 Sum: 11849534 Ratio: 99.94%) + Bounded : 136 (Average: 50.83 Max: 122 Sum: 6913 Ratio: 0.06%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 881056 (Eliminated: 0 Frozen: 272341) +Constraints : 6468887 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1048MB +Max. Length : 120 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.91s +Memory: 951MB (+0MB) +UNKNOWN +Iteration Time: 6.99s + +Iteration 80 +Queue: [(24,120,1,True)] +Grounded Until: 120 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 81 +Time : 662.305s (Solving: 628.62s 1st Model: 0.07s Unsat: 11.73s) +CPU Time : 662.400s + +Choices : 13283271 (Domain: 13037641) +Conflicts : 649889 (Analyzed: 649885) +Restarts : 7672 (Average: 84.71 Last: 156) +Model-Level : 251.0 +Problems : 81 (Average Length: 87.74 Splits: 0) +Lemmas : 649885 (Deleted: 610894) + Binary : 13715 (Ratio: 2.11%) + Ternary : 3007 (Ratio: 0.46%) + Conflict : 649885 (Average Length: 521.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 649885 (Average: 18.55 Max: 1251 Sum: 12052144) + Executed : 649749 (Average: 18.53 Max: 1251 Sum: 12045231 Ratio: 99.94%) + Bounded : 136 (Average: 50.83 Max: 122 Sum: 6913 Ratio: 0.06%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 881056 (Eliminated: 0 Frozen: 272341) +Constraints : 6468873 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1048MB +Max. Length : 120 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 10.33s +Memory: 951MB (+0MB) +UNKNOWN +Iteration Time: 10.40s + +Iteration 81 +Queue: [(5,25,6,True), (6,30,6,True), (7,35,5,True), (8,40,5,True), (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,False), (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), (24,120,2,False)] +Grounded Until: 120 +Blocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 82 +Time : 672.185s (Solving: 638.32s 1st Model: 0.07s Unsat: 11.73s) +CPU Time : 672.284s + +Choices : 13337257 (Domain: 13091627) +Conflicts : 658070 (Analyzed: 658066) +Restarts : 7772 (Average: 84.67 Last: 156) +Model-Level : 251.0 +Problems : 82 (Average Length: 88.16 Splits: 0) +Lemmas : 658066 (Deleted: 617231) + Binary : 13785 (Ratio: 2.09%) + Ternary : 3023 (Ratio: 0.46%) + Conflict : 658066 (Average Length: 527.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 658066 (Average: 18.38 Max: 1251 Sum: 12092844) + Executed : 657930 (Average: 18.37 Max: 1251 Sum: 12085931 Ratio: 99.94%) + Bounded : 136 (Average: 50.83 Max: 122 Sum: 6913 Ratio: 0.06%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 881056 (Eliminated: 0 Frozen: 272341) +Constraints : 6468873 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1048MB +Max. Length : 120 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.82s +Memory: 951MB (+0MB) +UNKNOWN +Iteration Time: 9.89s + +Iteration 82 +Queue: [(6,30,6,True), (7,35,5,True), (8,40,5,True), (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,False), (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), (24,120,2,False)] +Grounded Until: 120 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 83 +Time : 675.796s (Solving: 641.71s 1st Model: 0.07s Unsat: 11.73s) +CPU Time : 675.896s + +Choices : 13377378 (Domain: 13131748) +Conflicts : 665295 (Analyzed: 665291) +Restarts : 7872 (Average: 84.51 Last: 156) +Model-Level : 251.0 +Problems : 83 (Average Length: 88.57 Splits: 0) +Lemmas : 665291 (Deleted: 625249) + Binary : 13809 (Ratio: 2.08%) + Ternary : 3024 (Ratio: 0.45%) + Conflict : 665291 (Average Length: 524.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 665291 (Average: 18.23 Max: 1251 Sum: 12125089) + Executed : 665155 (Average: 18.21 Max: 1251 Sum: 12118176 Ratio: 99.94%) + Bounded : 136 (Average: 50.83 Max: 122 Sum: 6913 Ratio: 0.06%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 881056 (Eliminated: 0 Frozen: 272341) +Constraints : 6468873 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1048MB +Max. Length : 120 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 3.53s +Memory: 951MB (+0MB) +UNKNOWN +Iteration Time: 3.62s + +Iteration 83 +Queue: [(7,35,5,True), (8,40,5,True), (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,False), (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), (24,120,2,False)] +Grounded Until: 120 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 84 +Time : 679.353s (Solving: 645.09s 1st Model: 0.07s Unsat: 11.73s) +CPU Time : 679.456s + +Choices : 13425656 (Domain: 13179993) +Conflicts : 672988 (Analyzed: 672984) +Restarts : 7972 (Average: 84.42 Last: 156) +Model-Level : 251.0 +Problems : 84 (Average Length: 88.96 Splits: 0) +Lemmas : 672984 (Deleted: 632372) + Binary : 13826 (Ratio: 2.05%) + Ternary : 3026 (Ratio: 0.45%) + Conflict : 672984 (Average Length: 520.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 672984 (Average: 18.08 Max: 1251 Sum: 12165299) + Executed : 672848 (Average: 18.07 Max: 1251 Sum: 12158386 Ratio: 99.94%) + Bounded : 136 (Average: 50.83 Max: 122 Sum: 6913 Ratio: 0.06%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 881056 (Eliminated: 0 Frozen: 272341) +Constraints : 6468873 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1048MB +Max. Length : 120 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 3.50s +Memory: 951MB (+0MB) +UNKNOWN +Iteration Time: 3.56s + +Iteration 84 +Queue: [(8,40,5,True), (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,False), (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), (24,120,2,False)] +Grounded Until: 120 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 85 +Time : 686.314s (Solving: 651.85s 1st Model: 0.07s Unsat: 11.73s) +CPU Time : 686.412s + +Choices : 13499104 (Domain: 13252923) +Conflicts : 681243 (Analyzed: 681239) +Restarts : 8072 (Average: 84.40 Last: 156) +Model-Level : 251.0 +Problems : 85 (Average Length: 89.35 Splits: 0) +Lemmas : 681239 (Deleted: 639894) + Binary : 13918 (Ratio: 2.04%) + Ternary : 3036 (Ratio: 0.45%) + Conflict : 681239 (Average Length: 519.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 681239 (Average: 17.95 Max: 1251 Sum: 12227614) + Executed : 681103 (Average: 17.94 Max: 1251 Sum: 12220701 Ratio: 99.94%) + Bounded : 136 (Average: 50.83 Max: 122 Sum: 6913 Ratio: 0.06%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 881056 (Eliminated: 0 Frozen: 272341) +Constraints : 6468873 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1048MB +Max. Length : 120 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.88s +Memory: 951MB (+0MB) +UNKNOWN +Iteration Time: 6.96s + +Iteration 85 +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,False), (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), (24,120,2,False)] +Grounded Until: 120 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 86 +Time : 693.390s (Solving: 658.75s 1st Model: 0.07s Unsat: 11.73s) +CPU Time : 693.480s + +Choices : 13598005 (Domain: 13351528) +Conflicts : 689711 (Analyzed: 689707) +Restarts : 8172 (Average: 84.40 Last: 156) +Model-Level : 251.0 +Problems : 86 (Average Length: 89.73 Splits: 0) +Lemmas : 689707 (Deleted: 647946) + Binary : 13991 (Ratio: 2.03%) + Ternary : 3050 (Ratio: 0.44%) + Conflict : 689707 (Average Length: 517.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 689707 (Average: 17.85 Max: 1251 Sum: 12312506) + Executed : 689571 (Average: 17.84 Max: 1251 Sum: 12305593 Ratio: 99.94%) + Bounded : 136 (Average: 50.83 Max: 122 Sum: 6913 Ratio: 0.06%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 881056 (Eliminated: 0 Frozen: 272341) +Constraints : 6468873 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1048MB +Max. Length : 120 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.00s +Memory: 951MB (+0MB) +UNKNOWN +Iteration Time: 7.07s + +Iteration 86 +Queue: [(11,55,4,True), (12,60,4,False), (13,65,4,False), (14,70,3,True), (15,75,3,False), (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), (24,120,2,False)] +Grounded Until: 120 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 87 +Time : 702.439s (Solving: 667.62s 1st Model: 0.07s Unsat: 11.73s) +CPU Time : 702.532s + +Choices : 13725705 (Domain: 13478968) +Conflicts : 698962 (Analyzed: 698958) +Restarts : 8272 (Average: 84.50 Last: 156) +Model-Level : 251.0 +Problems : 87 (Average Length: 90.10 Splits: 0) +Lemmas : 698958 (Deleted: 658186) + Binary : 14086 (Ratio: 2.02%) + Ternary : 3069 (Ratio: 0.44%) + Conflict : 698958 (Average Length: 517.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 698958 (Average: 17.78 Max: 1251 Sum: 12424271) + Executed : 698822 (Average: 17.77 Max: 1251 Sum: 12417358 Ratio: 99.94%) + Bounded : 136 (Average: 50.83 Max: 122 Sum: 6913 Ratio: 0.06%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 881056 (Eliminated: 0 Frozen: 272341) +Constraints : 6468873 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1048MB +Max. Length : 120 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.00s +Memory: 951MB (+0MB) +UNKNOWN +Iteration Time: 9.06s + +Iteration 87 +Queue: [(14,70,3,True), (15,75,3,False), (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), (24,120,2,False)] +Grounded Until: 120 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 88 +Time : 711.949s (Solving: 676.95s 1st Model: 0.07s Unsat: 11.73s) +CPU Time : 712.044s + +Choices : 13886763 (Domain: 13639450) +Conflicts : 707595 (Analyzed: 707591) +Restarts : 8372 (Average: 84.52 Last: 156) +Model-Level : 251.0 +Problems : 88 (Average Length: 90.47 Splits: 0) +Lemmas : 707591 (Deleted: 667058) + Binary : 14222 (Ratio: 2.01%) + Ternary : 3077 (Ratio: 0.43%) + Conflict : 707591 (Average Length: 516.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 707591 (Average: 17.76 Max: 1251 Sum: 12567182) + Executed : 707455 (Average: 17.75 Max: 1251 Sum: 12560269 Ratio: 99.94%) + Bounded : 136 (Average: 50.83 Max: 122 Sum: 6913 Ratio: 0.06%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 881056 (Eliminated: 0 Frozen: 272341) +Constraints : 6468873 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1048MB +Max. Length : 120 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.45s +Memory: 951MB (+0MB) +UNKNOWN +Iteration Time: 9.52s + +Iteration 88 +Queue: [(19,95,2,True), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False), (24,120,2,False)] +Grounded Until: 120 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 89 +Time : 721.091s (Solving: 685.92s 1st Model: 0.07s Unsat: 11.73s) +CPU Time : 721.192s + +Choices : 14059637 (Domain: 13812265) +Conflicts : 716080 (Analyzed: 716076) +Restarts : 8472 (Average: 84.52 Last: 156) +Model-Level : 251.0 +Problems : 89 (Average Length: 90.82 Splits: 0) +Lemmas : 716076 (Deleted: 673327) + Binary : 14329 (Ratio: 2.00%) + Ternary : 3090 (Ratio: 0.43%) + Conflict : 716076 (Average Length: 515.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 716076 (Average: 17.76 Max: 1251 Sum: 12720490) + Executed : 715940 (Average: 17.75 Max: 1251 Sum: 12713577 Ratio: 99.95%) + Bounded : 136 (Average: 50.83 Max: 122 Sum: 6913 Ratio: 0.05%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 881056 (Eliminated: 0 Frozen: 272341) +Constraints : 6468873 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1048MB +Max. Length : 120 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.09s +Memory: 951MB (+0MB) +UNKNOWN +Iteration Time: 9.15s + +Iteration 89 +Queue: [(5,25,7,True), (6,30,7,True), (7,35,6,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,3,True), (16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,False), (22,110,2,False), (23,115,2,False), (24,120,2,False)] +Grounded Until: 120 +Blocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 90 +Time : 732.579s (Solving: 697.20s 1st Model: 0.07s Unsat: 11.73s) +CPU Time : 732.684s + +Choices : 14100867 (Domain: 13853495) +Conflicts : 724077 (Analyzed: 724073) +Restarts : 8572 (Average: 84.47 Last: 156) +Model-Level : 251.0 +Problems : 90 (Average Length: 91.17 Splits: 0) +Lemmas : 724073 (Deleted: 681409) + Binary : 14360 (Ratio: 1.98%) + Ternary : 3100 (Ratio: 0.43%) + Conflict : 724073 (Average Length: 525.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 724073 (Average: 17.60 Max: 1251 Sum: 12747146) + Executed : 723937 (Average: 17.60 Max: 1251 Sum: 12740233 Ratio: 99.95%) + Bounded : 136 (Average: 50.83 Max: 122 Sum: 6913 Ratio: 0.05%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 881056 (Eliminated: 0 Frozen: 272341) +Constraints : 6468873 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1048MB +Max. Length : 120 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 11.42s +Memory: 951MB (+0MB) +UNKNOWN +Iteration Time: 11.50s + +Iteration 90 +Queue: [(6,30,7,True), (7,35,6,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,3,True), (16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,False), (22,110,2,False), (23,115,2,False), (24,120,2,False)] +Grounded Until: 120 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 91 +Time : 743.153s (Solving: 707.60s 1st Model: 0.07s Unsat: 11.73s) +CPU Time : 743.264s + +Choices : 14181205 (Domain: 13933833) +Conflicts : 732907 (Analyzed: 732903) +Restarts : 8672 (Average: 84.51 Last: 156) +Model-Level : 251.0 +Problems : 91 (Average Length: 91.51 Splits: 0) +Lemmas : 732903 (Deleted: 691313) + Binary : 14488 (Ratio: 1.98%) + Ternary : 3115 (Ratio: 0.43%) + Conflict : 732903 (Average Length: 534.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 732903 (Average: 17.48 Max: 1251 Sum: 12810514) + Executed : 732767 (Average: 17.47 Max: 1251 Sum: 12803601 Ratio: 99.95%) + Bounded : 136 (Average: 50.83 Max: 122 Sum: 6913 Ratio: 0.05%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 881056 (Eliminated: 0 Frozen: 272341) +Constraints : 6468873 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1048MB +Max. Length : 120 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 10.51s +Memory: 951MB (+0MB) +UNKNOWN +Iteration Time: 10.58s + +Iteration 91 +Queue: [(7,35,6,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,3,True), (16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,False), (22,110,2,False), (23,115,2,False), (24,120,2,False)] +Grounded Until: 120 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 92 +Time : 751.909s (Solving: 716.15s 1st Model: 0.07s Unsat: 11.73s) +CPU Time : 752.024s + +Choices : 14274384 (Domain: 14025315) +Conflicts : 741979 (Analyzed: 741975) +Restarts : 8772 (Average: 84.58 Last: 156) +Model-Level : 251.0 +Problems : 92 (Average Length: 91.84 Splits: 0) +Lemmas : 741975 (Deleted: 699712) + Binary : 14683 (Ratio: 1.98%) + Ternary : 3138 (Ratio: 0.42%) + Conflict : 741975 (Average Length: 536.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 741975 (Average: 17.36 Max: 1251 Sum: 12884042) + Executed : 741839 (Average: 17.36 Max: 1251 Sum: 12877129 Ratio: 99.95%) + Bounded : 136 (Average: 50.83 Max: 122 Sum: 6913 Ratio: 0.05%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 881056 (Eliminated: 0 Frozen: 272341) +Constraints : 6468873 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1048MB +Max. Length : 120 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.68s +Memory: 951MB (+0MB) +UNKNOWN +Iteration Time: 8.76s + +Iteration 92 +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,3,True), (16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,False), (22,110,2,False), (23,115,2,False), (24,120,2,False)] +Grounded Until: 120 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 93 +Time : 760.968s (Solving: 725.03s 1st Model: 0.07s Unsat: 11.73s) +CPU Time : 761.084s + +Choices : 14345501 (Domain: 14096386) +Conflicts : 749879 (Analyzed: 749875) +Restarts : 8872 (Average: 84.52 Last: 156) +Model-Level : 251.0 +Problems : 93 (Average Length: 92.16 Splits: 0) +Lemmas : 749875 (Deleted: 706140) + Binary : 14752 (Ratio: 1.97%) + Ternary : 3145 (Ratio: 0.42%) + Conflict : 749875 (Average Length: 540.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 749875 (Average: 17.26 Max: 1251 Sum: 12939485) + Executed : 749739 (Average: 17.25 Max: 1251 Sum: 12932572 Ratio: 99.95%) + Bounded : 136 (Average: 50.83 Max: 122 Sum: 6913 Ratio: 0.05%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 881056 (Eliminated: 0 Frozen: 272341) +Constraints : 6468873 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1048MB +Max. Length : 120 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.00s +Memory: 951MB (+0MB) +UNKNOWN +Iteration Time: 9.07s + +Iteration 93 +Queue: [(10,50,5,True), (11,55,5,False), (12,60,4,True), (13,65,4,False), (14,70,4,False), (15,75,3,True), (16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,False), (22,110,2,False), (23,115,2,False), (24,120,2,False)] +Grounded Until: 120 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 94 +Time : 765.766s (Solving: 729.65s 1st Model: 0.07s Unsat: 11.73s) +CPU Time : 765.880s + +Choices : 14413522 (Domain: 14164389) +Conflicts : 758025 (Analyzed: 758021) +Restarts : 8972 (Average: 84.49 Last: 156) +Model-Level : 251.0 +Problems : 94 (Average Length: 92.48 Splits: 0) +Lemmas : 758021 (Deleted: 713728) + Binary : 14787 (Ratio: 1.95%) + Ternary : 3160 (Ratio: 0.42%) + Conflict : 758021 (Average Length: 537.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 758021 (Average: 17.15 Max: 1251 Sum: 12997739) + Executed : 757882 (Average: 17.14 Max: 1251 Sum: 12990466 Ratio: 99.94%) + Bounded : 139 (Average: 52.32 Max: 122 Sum: 7273 Ratio: 0.06%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 881056 (Eliminated: 0 Frozen: 272341) +Constraints : 6468873 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1048MB +Max. Length : 120 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 4.73s +Memory: 951MB (+0MB) +UNKNOWN +Iteration Time: 4.80s + +Iteration 94 +Queue: [(12,60,4,True), (13,65,4,False), (14,70,4,False), (15,75,3,True), (16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,False), (22,110,2,False), (23,115,2,False), (24,120,2,False)] +Grounded Until: 120 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 95 +Time : 771.423s (Solving: 735.10s 1st Model: 0.07s Unsat: 11.73s) +CPU Time : 771.532s + +Choices : 14498861 (Domain: 14249452) +Conflicts : 766363 (Analyzed: 766359) +Restarts : 9072 (Average: 84.48 Last: 156) +Model-Level : 251.0 +Problems : 95 (Average Length: 92.79 Splits: 0) +Lemmas : 766359 (Deleted: 721649) + Binary : 14850 (Ratio: 1.94%) + Ternary : 3190 (Ratio: 0.42%) + Conflict : 766359 (Average Length: 535.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 766359 (Average: 17.05 Max: 1251 Sum: 13070078) + Executed : 766220 (Average: 17.05 Max: 1251 Sum: 13062805 Ratio: 99.94%) + Bounded : 139 (Average: 52.32 Max: 122 Sum: 7273 Ratio: 0.06%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 881056 (Eliminated: 0 Frozen: 272341) +Constraints : 6468859 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1048MB +Max. Length : 120 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 5.57s +Memory: 951MB (+0MB) +UNKNOWN +Iteration Time: 5.65s + +Iteration 95 +Queue: [(15,75,3,True), (16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,False), (22,110,2,False), (23,115,2,False), (24,120,2,False)] +Grounded Until: 120 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 96 +Time : 780.173s (Solving: 743.65s 1st Model: 0.07s Unsat: 11.73s) +CPU Time : 780.272s + +Choices : 14675328 (Domain: 14425529) +Conflicts : 775282 (Analyzed: 775278) +Restarts : 9172 (Average: 84.53 Last: 156) +Model-Level : 251.0 +Problems : 96 (Average Length: 93.09 Splits: 0) +Lemmas : 775278 (Deleted: 731774) + Binary : 14940 (Ratio: 1.93%) + Ternary : 3241 (Ratio: 0.42%) + Conflict : 775278 (Average Length: 533.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 775278 (Average: 17.06 Max: 1251 Sum: 13226041) + Executed : 775138 (Average: 17.05 Max: 1251 Sum: 13218646 Ratio: 99.94%) + Bounded : 140 (Average: 52.82 Max: 122 Sum: 7395 Ratio: 0.06%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 881056 (Eliminated: 0 Frozen: 272341) +Constraints : 6468859 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1048MB +Max. Length : 120 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.67s +Memory: 951MB (+0MB) +UNKNOWN +Iteration Time: 8.74s + +Iteration 96 +Queue: [(16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,False), (22,110,2,False), (23,115,2,False), (24,120,2,False)] +Grounded Until: 120 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 97 +Time : 787.232s (Solving: 750.51s 1st Model: 0.07s Unsat: 11.73s) +CPU Time : 787.332s + +Choices : 14784362 (Domain: 14534491) +Conflicts : 784058 (Analyzed: 784054) +Restarts : 9272 (Average: 84.56 Last: 175) +Model-Level : 251.0 +Problems : 97 (Average Length: 93.39 Splits: 0) +Lemmas : 784054 (Deleted: 740441) + Binary : 14984 (Ratio: 1.91%) + Ternary : 3242 (Ratio: 0.41%) + Conflict : 784054 (Average Length: 532.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 784054 (Average: 16.99 Max: 1251 Sum: 13317516) + Executed : 783913 (Average: 16.98 Max: 1251 Sum: 13310001 Ratio: 99.94%) + Bounded : 141 (Average: 53.30 Max: 122 Sum: 7515 Ratio: 0.06%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 881056 (Eliminated: 0 Frozen: 272341) +Constraints : 6468845 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1048MB +Max. Length : 120 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.99s +Memory: 951MB (+0MB) +UNKNOWN +Iteration Time: 7.06s + +Iteration 97 +Queue: [(20,100,2,True), (21,105,2,False), (22,110,2,False), (23,115,2,False), (24,120,2,False)] +Grounded Until: 120 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 98 +Time : 796.625s (Solving: 759.73s 1st Model: 0.07s Unsat: 11.73s) +CPU Time : 796.728s + +Choices : 14965365 (Domain: 14715389) +Conflicts : 792908 (Analyzed: 792904) +Restarts : 9372 (Average: 84.60 Last: 175) +Model-Level : 251.0 +Problems : 98 (Average Length: 93.68 Splits: 0) +Lemmas : 792904 (Deleted: 749033) + Binary : 15063 (Ratio: 1.90%) + Ternary : 3255 (Ratio: 0.41%) + Conflict : 792904 (Average Length: 532.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 792904 (Average: 16.99 Max: 1251 Sum: 13475352) + Executed : 792763 (Average: 16.99 Max: 1251 Sum: 13467837 Ratio: 99.94%) + Bounded : 141 (Average: 53.30 Max: 122 Sum: 7515 Ratio: 0.06%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 881056 (Eliminated: 0 Frozen: 272341) +Constraints : 6468845 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1048MB +Max. Length : 120 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.34s +Memory: 951MB (+0MB) +UNKNOWN +Iteration Time: 9.40s + +Iteration 98 +Queue: [(5,25,8,True), (6,30,8,True), (7,35,7,True), (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,2,True), (22,110,2,True), (23,115,2,False), (24,120,2,False)] +Grounded Until: 120 +Blocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 99 +Time : 808.948s (Solving: 771.88s 1st Model: 0.07s Unsat: 11.73s) +CPU Time : 809.056s + +Choices : 15007662 (Domain: 14757686) +Conflicts : 801451 (Analyzed: 801447) +Restarts : 9472 (Average: 84.61 Last: 175) +Model-Level : 251.0 +Problems : 99 (Average Length: 93.97 Splits: 0) +Lemmas : 801447 (Deleted: 755408) + Binary : 15082 (Ratio: 1.88%) + Ternary : 3261 (Ratio: 0.41%) + Conflict : 801447 (Average Length: 541.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 801447 (Average: 16.85 Max: 1251 Sum: 13502815) + Executed : 801306 (Average: 16.84 Max: 1251 Sum: 13495300 Ratio: 99.94%) + Bounded : 141 (Average: 53.30 Max: 122 Sum: 7515 Ratio: 0.06%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 881056 (Eliminated: 0 Frozen: 272341) +Constraints : 6468845 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1048MB +Max. Length : 120 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 12.27s +Memory: 951MB (+0MB) +UNKNOWN +Iteration Time: 12.33s + +Iteration 99 +Queue: [(6,30,8,True), (7,35,7,True), (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,2,True), (22,110,2,True), (23,115,2,False), (24,120,2,False)] +Grounded Until: 120 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 100 +Time : 814.343s (Solving: 777.09s 1st Model: 0.07s Unsat: 11.73s) +CPU Time : 814.452s + +Choices : 15064033 (Domain: 14814057) +Conflicts : 809315 (Analyzed: 809311) +Restarts : 9572 (Average: 84.55 Last: 175) +Model-Level : 251.0 +Problems : 100 (Average Length: 94.25 Splits: 0) +Lemmas : 809311 (Deleted: 763810) + Binary : 15137 (Ratio: 1.87%) + Ternary : 3265 (Ratio: 0.40%) + Conflict : 809311 (Average Length: 543.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 809311 (Average: 16.74 Max: 1251 Sum: 13544713) + Executed : 809170 (Average: 16.73 Max: 1251 Sum: 13537198 Ratio: 99.94%) + Bounded : 141 (Average: 53.30 Max: 122 Sum: 7515 Ratio: 0.06%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 881056 (Eliminated: 0 Frozen: 272341) +Constraints : 6468845 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1048MB +Max. Length : 120 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 5.33s +Memory: 951MB (+0MB) +UNKNOWN +Iteration Time: 5.40s + +Iteration 100 +Queue: [(7,35,7,True), (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,2,True), (22,110,2,True), (23,115,2,False), (24,120,2,False)] +Grounded Until: 120 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 101 +Time : 820.053s (Solving: 782.59s 1st Model: 0.07s Unsat: 11.73s) +CPU Time : 820.164s + +Choices : 15122775 (Domain: 14872505) +Conflicts : 817152 (Analyzed: 817148) +Restarts : 9672 (Average: 84.49 Last: 175) +Model-Level : 251.0 +Problems : 101 (Average Length: 94.52 Splits: 0) +Lemmas : 817148 (Deleted: 771503) + Binary : 15204 (Ratio: 1.86%) + Ternary : 3276 (Ratio: 0.40%) + Conflict : 817148 (Average Length: 543.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 817148 (Average: 16.63 Max: 1251 Sum: 13589349) + Executed : 817007 (Average: 16.62 Max: 1251 Sum: 13581834 Ratio: 99.94%) + Bounded : 141 (Average: 53.30 Max: 122 Sum: 7515 Ratio: 0.06%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 881056 (Eliminated: 0 Frozen: 272341) +Constraints : 6468845 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1048MB +Max. Length : 120 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 5.63s +Memory: 951MB (+0MB) +UNKNOWN +Iteration Time: 5.71s + +Iteration 101 +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,2,True), (22,110,2,True), (23,115,2,False), (24,120,2,False)] +Grounded Until: 120 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 102 +Time : 825.353s (Solving: 787.70s 1st Model: 0.07s Unsat: 11.73s) +CPU Time : 825.464s + +Choices : 15190386 (Domain: 14939890) +Conflicts : 825719 (Analyzed: 825715) +Restarts : 9772 (Average: 84.50 Last: 175) +Model-Level : 251.0 +Problems : 102 (Average Length: 94.79 Splits: 0) +Lemmas : 825715 (Deleted: 779081) + Binary : 15222 (Ratio: 1.84%) + Ternary : 3277 (Ratio: 0.40%) + Conflict : 825715 (Average Length: 541.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 825715 (Average: 16.53 Max: 1251 Sum: 13646282) + Executed : 825574 (Average: 16.52 Max: 1251 Sum: 13638767 Ratio: 99.94%) + Bounded : 141 (Average: 53.30 Max: 122 Sum: 7515 Ratio: 0.06%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 881056 (Eliminated: 0 Frozen: 272341) +Constraints : 6468845 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1048MB +Max. Length : 120 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 5.23s +Memory: 951MB (+0MB) +UNKNOWN +Iteration Time: 5.31s + +Iteration 102 +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,2,True), (22,110,2,True), (23,115,2,False), (24,120,2,False)] +Grounded Until: 120 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 103 +Time : 832.837s (Solving: 795.00s 1st Model: 0.07s Unsat: 11.73s) +CPU Time : 832.952s + +Choices : 15274880 (Domain: 15023207) +Conflicts : 834297 (Analyzed: 834293) +Restarts : 9872 (Average: 84.51 Last: 175) +Model-Level : 251.0 +Problems : 103 (Average Length: 95.06 Splits: 0) +Lemmas : 834293 (Deleted: 787437) + Binary : 15292 (Ratio: 1.83%) + Ternary : 3293 (Ratio: 0.39%) + Conflict : 834293 (Average Length: 540.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 834293 (Average: 16.44 Max: 1251 Sum: 13716372) + Executed : 834152 (Average: 16.43 Max: 1251 Sum: 13708857 Ratio: 99.95%) + Bounded : 141 (Average: 53.30 Max: 122 Sum: 7515 Ratio: 0.05%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 881056 (Eliminated: 0 Frozen: 272341) +Constraints : 6468845 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1048MB +Max. Length : 120 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.43s +Memory: 951MB (+0MB) +UNKNOWN +Iteration Time: 7.49s + +Iteration 103 +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,2,True), (22,110,2,True), (23,115,2,False), (24,120,2,False)] +Grounded Until: 120 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 104 +Time : 840.410s (Solving: 802.36s 1st Model: 0.07s Unsat: 11.73s) +CPU Time : 840.528s + +Choices : 15372997 (Domain: 15121000) +Conflicts : 843061 (Analyzed: 843057) +Restarts : 9972 (Average: 84.54 Last: 175) +Model-Level : 251.0 +Problems : 104 (Average Length: 95.32 Splits: 0) +Lemmas : 843057 (Deleted: 797996) + Binary : 15355 (Ratio: 1.82%) + Ternary : 3305 (Ratio: 0.39%) + Conflict : 843057 (Average Length: 539.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 843057 (Average: 16.37 Max: 1251 Sum: 13798070) + Executed : 842916 (Average: 16.36 Max: 1251 Sum: 13790555 Ratio: 99.95%) + Bounded : 141 (Average: 53.30 Max: 122 Sum: 7515 Ratio: 0.05%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 881056 (Eliminated: 0 Frozen: 272341) +Constraints : 6468845 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1048MB +Max. Length : 120 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.49s +Memory: 951MB (+0MB) +UNKNOWN +Iteration Time: 7.58s + +Iteration 104 +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,2,True), (22,110,2,True), (23,115,2,False), (24,120,2,False)] +Grounded Until: 120 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 105 +Time : 848.750s (Solving: 810.52s 1st Model: 0.07s Unsat: 11.73s) +CPU Time : 848.872s + +Choices : 15494748 (Domain: 15242114) +Conflicts : 852032 (Analyzed: 852028) +Restarts : 10072 (Average: 84.59 Last: 175) +Model-Level : 251.0 +Problems : 105 (Average Length: 95.57 Splits: 0) +Lemmas : 852028 (Deleted: 806503) + Binary : 15417 (Ratio: 1.81%) + Ternary : 3320 (Ratio: 0.39%) + Conflict : 852028 (Average Length: 540.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 852028 (Average: 16.31 Max: 1251 Sum: 13899546) + Executed : 851887 (Average: 16.30 Max: 1251 Sum: 13892031 Ratio: 99.95%) + Bounded : 141 (Average: 53.30 Max: 122 Sum: 7515 Ratio: 0.05%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 881056 (Eliminated: 0 Frozen: 272341) +Constraints : 6468845 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1048MB +Max. Length : 120 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.28s +Memory: 951MB (+0MB) +UNKNOWN +Iteration Time: 8.35s + +Iteration 105 +Queue: [(17,85,3,True), (18,90,3,False), (19,95,3,False), (20,100,3,False), (21,105,2,True), (22,110,2,True), (23,115,2,False), (24,120,2,False)] +Grounded Until: 120 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 106 +Time : 858.788s (Solving: 820.38s 1st Model: 0.07s Unsat: 11.73s) +CPU Time : 858.916s + +Choices : 15654408 (Domain: 15401376) +Conflicts : 861696 (Analyzed: 861692) +Restarts : 10172 (Average: 84.71 Last: 175) +Model-Level : 251.0 +Problems : 106 (Average Length: 95.82 Splits: 0) +Lemmas : 861692 (Deleted: 815289) + Binary : 15459 (Ratio: 1.79%) + Ternary : 3334 (Ratio: 0.39%) + Conflict : 861692 (Average Length: 541.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 861692 (Average: 16.29 Max: 1251 Sum: 14037007) + Executed : 861551 (Average: 16.28 Max: 1251 Sum: 14029492 Ratio: 99.95%) + Bounded : 141 (Average: 53.30 Max: 122 Sum: 7515 Ratio: 0.05%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 881056 (Eliminated: 0 Frozen: 272341) +Constraints : 6468845 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1048MB +Max. Length : 120 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.98s +Memory: 951MB (+0MB) +UNKNOWN +Iteration Time: 10.04s + +Iteration 106 +Queue: [(21,105,2,True), (22,110,2,True), (23,115,2,False), (24,120,2,False)] +Grounded Until: 120 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 107 +Time : 865.664s (Solving: 827.09s 1st Model: 0.07s Unsat: 11.73s) +CPU Time : 865.796s + +Choices : 15772191 (Domain: 15518880) +Conflicts : 870232 (Analyzed: 870228) +Restarts : 10272 (Average: 84.72 Last: 175) +Model-Level : 251.0 +Problems : 107 (Average Length: 96.07 Splits: 0) +Lemmas : 870228 (Deleted: 822590) + Binary : 15473 (Ratio: 1.78%) + Ternary : 3353 (Ratio: 0.39%) + Conflict : 870228 (Average Length: 539.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 870228 (Average: 16.24 Max: 1251 Sum: 14135261) + Executed : 870087 (Average: 16.23 Max: 1251 Sum: 14127746 Ratio: 99.95%) + Bounded : 141 (Average: 53.30 Max: 122 Sum: 7515 Ratio: 0.05%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 881056 (Eliminated: 0 Frozen: 272341) +Constraints : 6468845 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1048MB +Max. Length : 120 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.82s +Memory: 951MB (+0MB) +UNKNOWN +Iteration Time: 6.88s + +Iteration 107 +Queue: [(22,110,2,True), (23,115,2,False), (24,120,2,False)] +Grounded Until: 120 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 108 +Time : 874.352s (Solving: 835.60s 1st Model: 0.07s Unsat: 11.73s) +CPU Time : 874.484s + +Choices : 15910592 (Domain: 15657216) +Conflicts : 878853 (Analyzed: 878849) +Restarts : 10372 (Average: 84.73 Last: 175) +Model-Level : 251.0 +Problems : 108 (Average Length: 96.31 Splits: 0) +Lemmas : 878849 (Deleted: 833073) + Binary : 15500 (Ratio: 1.76%) + Ternary : 3364 (Ratio: 0.38%) + Conflict : 878849 (Average Length: 540.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 878849 (Average: 16.21 Max: 1251 Sum: 14248228) + Executed : 878708 (Average: 16.20 Max: 1251 Sum: 14240713 Ratio: 99.95%) + Bounded : 141 (Average: 53.30 Max: 122 Sum: 7515 Ratio: 0.05%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 881056 (Eliminated: 0 Frozen: 272341) +Constraints : 6468845 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1048MB +Max. Length : 120 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.63s +Memory: 951MB (+0MB) +UNKNOWN +Iteration Time: 8.70s + +Iteration 108 +Queue: [(5,25,9,True), (6,30,9,True), (7,35,8,True), (8,40,8,False), (9,45,7,True), (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,True), (24,120,2,False)] +Grounded Until: 120 +Blocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 109 +Time : 881.451s (Solving: 842.51s 1st Model: 0.07s Unsat: 11.73s) +CPU Time : 881.584s + +Choices : 15955076 (Domain: 15701700) +Conflicts : 886877 (Analyzed: 886873) +Restarts : 10472 (Average: 84.69 Last: 175) +Model-Level : 251.0 +Problems : 109 (Average Length: 96.54 Splits: 0) +Lemmas : 886873 (Deleted: 839363) + Binary : 15547 (Ratio: 1.75%) + Ternary : 3369 (Ratio: 0.38%) + Conflict : 886873 (Average Length: 541.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 886873 (Average: 16.10 Max: 1251 Sum: 14282515) + Executed : 886732 (Average: 16.10 Max: 1251 Sum: 14275000 Ratio: 99.95%) + Bounded : 141 (Average: 53.30 Max: 122 Sum: 7515 Ratio: 0.05%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 881056 (Eliminated: 0 Frozen: 272341) +Constraints : 6468845 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1048MB +Max. Length : 120 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.03s +Memory: 951MB (+0MB) +UNKNOWN +Iteration Time: 7.11s + +Iteration 109 +Queue: [(6,30,9,True), (7,35,8,True), (8,40,8,False), (9,45,7,True), (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,True), (24,120,2,False)] +Grounded Until: 120 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 110 +Time : 887.574s (Solving: 848.41s 1st Model: 0.07s Unsat: 11.73s) +CPU Time : 887.712s + +Choices : 16017591 (Domain: 15764215) +Conflicts : 895202 (Analyzed: 895198) +Restarts : 10572 (Average: 84.68 Last: 175) +Model-Level : 251.0 +Problems : 110 (Average Length: 96.77 Splits: 0) +Lemmas : 895198 (Deleted: 847259) + Binary : 15578 (Ratio: 1.74%) + Ternary : 3386 (Ratio: 0.38%) + Conflict : 895198 (Average Length: 541.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 895198 (Average: 16.01 Max: 1251 Sum: 14331417) + Executed : 895057 (Average: 16.00 Max: 1251 Sum: 14323902 Ratio: 99.95%) + Bounded : 141 (Average: 53.30 Max: 122 Sum: 7515 Ratio: 0.05%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 881056 (Eliminated: 0 Frozen: 272341) +Constraints : 6468845 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1048MB +Max. Length : 120 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.04s +Memory: 951MB (+0MB) +UNKNOWN +Iteration Time: 6.13s + +Iteration 110 +Queue: [(7,35,8,True), (8,40,8,False), (9,45,7,True), (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,True), (24,120,2,False)] +Grounded Until: 120 +Unblocking actions... +Solving... +*** Info : (planner): INTERRUPTED by signal! +UNKNOWN + +INTERRUPTED : 1 + +Models : 0+ +Calls : 111 +Time : 893.084s (Solving: 853.74s 1st Model: 0.07s Unsat: 11.73s) +CPU Time : 893.204s + +Choices : 16072168 (Domain: 15818777) +Conflicts : 902178 (Analyzed: 902174) +Restarts : 10652 (Average: 84.70 Last: 175) +Model-Level : 251.0 +Problems : 111 (Average Length: 97.00 Splits: 0) +Lemmas : 902174 (Deleted: 855390) + Binary : 15640 (Ratio: 1.73%) + Ternary : 3406 (Ratio: 0.38%) + Conflict : 902174 (Average Length: 541.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 902174 (Average: 15.93 Max: 1251 Sum: 14373564) + Executed : 902033 (Average: 15.92 Max: 1251 Sum: 14366049 Ratio: 99.95%) + Bounded : 141 (Average: 53.30 Max: 122 Sum: 7515 Ratio: 0.05%) + +Rules : 150286 (Original: 135821) +Atoms : 72368 +Bodies : 65513 (Original: 51047) + Count : 841 (Original: 2348) +Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) +Tight : Yes +Variables : 881056 (Eliminated: 0 Frozen: 272341) +Constraints : 6468845 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1048MB +Max. Length : 120 steps +Models : 1 + +