diff --git a/gc-ta1-tt1-jumpy/ipc-2011_barman-sequential-satisficing_2.env b/gc-ta1-tt1-jumpy/ipc-2011_barman-sequential-satisficing_2.env new file mode 100644 index 000000000..e94ed7d34 --- /dev/null +++ b/gc-ta1-tt1-jumpy/ipc-2011_barman-sequential-satisficing_2.env @@ -0,0 +1,59 @@ +command: +- timeout +- -m=9216000 +- -t=900 +- python3 +- /home/pluehne/Documents/ASP/plasp-javier/encodings/planner/runplanner.py +- --domain=/home/pluehne/Documents/ASP/pddl-instances/ipc-2011/domains/barman-sequential-satisficing/domain.pddl +- /home/pluehne/Documents/ASP/pddl-instances/ipc-2011/domains/barman-sequential-satisficing/instances/instance-2.pddl +- --stats +- --stats-iter +- --verbose +- --print-call +- -m 8192 +- --translate +- -B 0.9 +- --parallel=0 +- --shallow +- --use-heuristic +- --test-until-not-sat +- --test=0 +- --test-add=1 +- --test-times=1 +- --configuration=jumpy +- -i 0 +configuration: + id: gc-ta1-tt1-jumpy + instanceSets: + - rintanen-aij-2012-interesting + options: + - --stats + - --stats-iter + - --verbose + - --print-call + - -m 8192 + - --translate + - -B 0.9 + - --parallel=0 + - --shallow + - --use-heuristic + - --test-until-not-sat + - --test=0 + - --test-add=1 + - --test-times=1 + - --configuration=jumpy + - -i 0 +exitCode: 0 +instance: + domain: barman-sequential-satisficing + instance: 2 + ipc: ipc-2011 + planLength: 105 +versions: + clingo: 5.2.2 + fastDownward: 10997:847cdf0069cab0c8841a9958e783d1a7340fe2e9 (2017-11-02 15:10 +0100) + planner: f090434475c02dbccc3811039498f2a63a357ddc (2018-02-01 18:15:39 +0100) + plasp: 3.1.1 + python: 3.6.3 +workingDirectory: /home/pluehne/Documents/ASP/plasp-javier/encodings/planner + diff --git a/gc-ta1-tt1-jumpy/ipc-2011_barman-sequential-satisficing_2.err b/gc-ta1-tt1-jumpy/ipc-2011_barman-sequential-satisficing_2.err new file mode 100644 index 000000000..d4a5626dd --- /dev/null +++ b/gc-ta1-tt1-jumpy/ipc-2011_barman-sequential-satisficing_2.err @@ -0,0 +1,8 @@ +# configuration: {'id': 'gc-ta1-tt1-jumpy', 'options': ['--stats', '--stats-iter', '--verbose', '--print-call', '-m 8192', '--translate', '-B 0.9', '--parallel=0', '--shallow', '--use-heuristic', '--test-until-not-sat', '--test=0', '--test-add=1', '--test-times=1', '--configuration=jumpy', '-i 0'], 'instanceSets': ['rintanen-aij-2012-interesting']} +# instance: {'ipc': 'ipc-2011', 'domain': 'barman-sequential-satisficing', 'instance': 2, 'planLength': 105} +# 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-2.pddl', '--stats', '--stats-iter', '--verbose', '--print-call', '-m 8192', '--translate', '-B 0.9', '--parallel=0', '--shallow', '--use-heuristic', '--test-until-not-sat', '--test=0', '--test-add=1', '--test-times=1', '--configuration=jumpy', '-i 0'] +# working directory: /home/pluehne/Documents/ASP/plasp-javier/encodings/planner +# exit code: 0 +TIMEOUT CPU 900.12 MEM 734680 MAXMEM 734680 STALE 1 MAXMEM_RSS 632752 + + diff --git a/gc-ta1-tt1-jumpy/ipc-2011_barman-sequential-satisficing_2.out b/gc-ta1-tt1-jumpy/ipc-2011_barman-sequential-satisficing_2.out new file mode 100644 index 000000000..d5ef94f0d --- /dev/null +++ b/gc-ta1-tt1-jumpy/ipc-2011_barman-sequential-satisficing_2.out @@ -0,0 +1,2447 @@ +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-2.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-2.pddl +Parsing... +Parsing: [0.040s CPU, 0.037s wall-clock] +Normalizing task... [0.000s CPU, 0.003s wall-clock] +Instantiating... +Generating Datalog program... [0.010s CPU, 0.009s wall-clock] +Normalizing Datalog program... +Normalizing Datalog program: [0.050s CPU, 0.049s wall-clock] +Preparing model... [0.020s CPU, 0.025s wall-clock] +Generated 115 rules. +Computing model... [0.330s CPU, 0.330s wall-clock] +2025 relevant atoms +2105 auxiliary atoms +4130 final queue length +7122 total queue pushes +Completing instantiation... [0.600s CPU, 0.598s wall-clock] +Instantiating: [1.010s CPU, 1.018s wall-clock] +Computing fact groups... +Finding invariants... +24 initial candidates +Finding invariants: [0.100s CPU, 0.097s wall-clock] +Checking invariant weight... [0.000s CPU, 0.001s wall-clock] +Instantiating groups... [0.010s CPU, 0.006s wall-clock] +Collecting mutex groups... [0.000s CPU, 0.000s wall-clock] +Choosing groups... +207 uncovered facts +Choosing groups: [0.000s CPU, 0.001s wall-clock] +Building translation key... [0.010s CPU, 0.008s wall-clock] +Computing fact groups: [0.130s CPU, 0.130s wall-clock] +Building STRIPS to SAS dictionary... [0.000s CPU, 0.002s wall-clock] +Building dictionary for full mutex groups... [0.000s CPU, 0.002s wall-clock] +Building mutex information... +Building mutex information: [0.000s CPU, 0.002s wall-clock] +Translating task... +Processing axioms... +Simplifying axioms... [0.000s CPU, 0.000s wall-clock] +Processing axioms: [0.040s CPU, 0.033s wall-clock] +Translating task: [0.660s CPU, 0.657s wall-clock] +2326 effect conditions simplified +0 implied preconditions added +Detecting unreachable propositions... +0 operators removed +0 axioms removed +3 propositions removed +Detecting unreachable propositions: [0.310s CPU, 0.308s wall-clock] +Reordering and filtering variables... +210 of 210 variables necessary. +11 of 14 mutex groups necessary. +1390 of 1390 operators necessary. +0 of 0 axiom rules necessary. +Reordering and filtering variables: [0.210s CPU, 0.207s wall-clock] +Translator variables: 210 +Translator derived variables: 0 +Translator facts: 441 +Translator goal facts: 9 +Translator mutex groups: 11 +Translator total mutex groups size: 33 +Translator operators: 1390 +Translator axioms: 0 +Translator task size: 13333 +Translator peak memory: 43980 KB +Writing output... [0.260s CPU, 0.271s wall-clock] +Done! [2.640s CPU, 2.663s wall-clock] +planner.py version 0.0.1 + +Time: 0.57s +Memory: 86MB + +Iteration 1 +Queue: [(0,0,0,True), (1,5,0,True), (2,10,0,True), (3,15,0,True), (4,20,0,True), (5,25,0,True), (6,30,0,True)] +Grounded Until: 0 +Solving... +[start: stats after solve call] + +Models : 0 +Calls : 1 +Time : 0.658s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s) +CPU Time : 0.568s + +Choices : 0 +Conflicts : 0 (Analyzed: 0) +Restarts : 0 +Problems : 1 (Average Length: 2.00 Splits: 0) +Lemmas : 0 (Deleted: 0) + Binary : 0 (Ratio: 0.00%) + Ternary : 0 (Ratio: 0.00%) + Conflict : 0 (Average Length: 0.0 Ratio: 0.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 0 (Average: 0.00 Max: 0 Sum: 0) + Executed : 0 (Average: 0.00 Max: 0 Sum: 0 Ratio: 0.00%) + Bounded : 0 (Average: 0.00 Max: 0 Sum: 0 Ratio: 100.00%) + +Rules : 38518 +Atoms : 38518 +Bodies : 1 (Original: 0) +Tight : Yes +Variables : 0 (Eliminated: 0 Frozen: 0) +Constraints : 0 (Binary: 0.0% Ternary: 0.0% Other: 0.0%) + +Memory Peak : 222MB +Max. Length : 0 steps +Models : 0 + +[endof: stats after solve call] +Solving Time: 0.00s +Memory: 158MB (+72MB) +UNSAT +Iteration Time: 0.00s + +Iteration 2 +Queue: [(1,5,0,True), (2,10,0,True), (3,15,0,True), (4,20,0,True), (5,25,0,True), (6,30,0,True)] +Grounded Until: 0 +Expected Memory: 158MB +Grounding... [('step', [1]), ('step', [2]), ('step', [3]), ('step', [4]), ('step', [5]), ('check', [5])] +Grounding Time: 0.15s +Memory: 158MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 1+ +Calls : 2 +Time : 0.982s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s) +CPU Time : 0.892s + +Choices : 152 (Domain: 73) +Conflicts : 2 (Analyzed: 2) +Restarts : 0 +Model-Level : 147.0 +Problems : 2 (Average Length: 4.50 Splits: 0) +Lemmas : 2 (Deleted: 0) + Binary : 0 (Ratio: 0.00%) + Ternary : 0 (Ratio: 0.00%) + Conflict : 2 (Average Length: 23.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 2 (Average: 6.00 Max: 11 Sum: 12) + Executed : 2 (Average: 6.00 Max: 11 Sum: 12 Ratio: 100.00%) + Bounded : 0 (Average: 0.00 Max: 0 Sum: 0 Ratio: 0.00%) + +Rules : 38518 +Atoms : 38518 +Bodies : 1 (Original: 0) +Tight : Yes +Variables : 10322 (Eliminated: 0 Frozen: 10322) +Constraints : 36431 (Binary: 95.0% Ternary: 3.5% Other: 1.5%) + +Memory Peak : 222MB +Max. Length : 0 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 0.10s +Memory: 160MB (+2MB) +SAT +Testing... +NOT SERIALIZABLE +Testing Time: 0.58s +Memory: 178MB (+18MB) +Solving... +[start: stats after solve call] + +Models : 0 +Calls : 3 +Time : 1.081s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s) +CPU Time : 0.992s + +Choices : 161 (Domain: 78) +Conflicts : 9 (Analyzed: 8) +Restarts : 0 +Model-Level : 147.0 +Problems : 3 (Average Length: 5.33 Splits: 0) +Lemmas : 8 (Deleted: 0) + Binary : 1 (Ratio: 12.50%) + Ternary : 2 (Ratio: 25.00%) + Conflict : 8 (Average Length: 8.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 8 (Average: 2.75 Max: 11 Sum: 22) + Executed : 7 (Average: 2.62 Max: 11 Sum: 21 Ratio: 95.45%) + Bounded : 1 (Average: 1.00 Max: 1 Sum: 1 Ratio: 4.55%) + +Rules : 55133 (Original: 53913) +Atoms : 43853 +Bodies : 10280 (Original: 9059) + Count : 232 (Original: 476) +Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) +Tight : Yes +Variables : 12735 (Eliminated: 1464 Frozen: 11271) +Constraints : 50631 (Binary: 90.2% Ternary: 5.9% Other: 3.9%) + +Memory Peak : 222MB +Max. Length : 0 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 0.02s +Memory: 178MB (+0MB) +UNSAT +Iteration Time: 0.93s + +Iteration 3 +Queue: [(2,10,0,True), (3,15,0,True), (4,20,0,True), (5,25,0,True), (6,30,0,True)] +Grounded Until: 5 +Expected Memory: 180.0MB +Grounding... [('step', [6]), ('step', [7]), ('step', [8]), ('step', [9]), ('step', [10]), ('check', [10])] +Grounding Time: 0.29s +Memory: 178MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0 +Calls : 4 +Time : 2.170s (Solving: 0.38s 1st Model: 0.00s Unsat: 0.38s) +CPU Time : 2.080s + +Choices : 12799 (Domain: 10798) +Conflicts : 1643 (Analyzed: 1641) +Restarts : 10 (Average: 164.10 Last: 20) +Model-Level : 147.0 +Problems : 4 (Average Length: 7.00 Splits: 0) +Lemmas : 1641 (Deleted: 0) + Binary : 185 (Ratio: 11.27%) + Ternary : 187 (Ratio: 11.40%) + Conflict : 1641 (Average Length: 27.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 1641 (Average: 7.73 Max: 79 Sum: 12687) + Executed : 1623 (Average: 7.62 Max: 79 Sum: 12504 Ratio: 98.56%) + Bounded : 18 (Average: 10.17 Max: 12 Sum: 183 Ratio: 1.44%) + +Rules : 55133 (Original: 53913) +Atoms : 43853 +Bodies : 10280 (Original: 9059) + Count : 232 (Original: 476) +Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) +Tight : Yes +Variables : 35311 (Eliminated: 1464 Frozen: 26317) +Constraints : 223676 (Binary: 91.3% Ternary: 6.4% Other: 2.3%) + +Memory Peak : 222MB +Max. Length : 5 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 0.70s +Memory: 189MB (+11MB) +UNSAT +Iteration Time: 1.10s + +Iteration 4 +Queue: [(3,15,0,True), (4,20,0,True), (5,25,0,True), (6,30,0,True)] +Grounded Until: 10 +Expected Memory: 200.0MB +Grounding... [('step', [11]), ('step', [12]), ('step', [13]), ('step', [14]), ('step', [15]), ('check', [15])] +Grounding Time: 0.38s +Memory: 195MB (+6MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0 +Calls : 5 +Time : 6.807s (Solving: 4.20s 1st Model: 0.00s Unsat: 4.20s) +CPU Time : 6.720s + +Choices : 95323 (Domain: 72132) +Conflicts : 13704 (Analyzed: 13701) +Restarts : 61 (Average: 224.61 Last: 168) +Model-Level : 147.0 +Problems : 5 (Average Length: 9.00 Splits: 0) +Lemmas : 13701 (Deleted: 7320) + Binary : 884 (Ratio: 6.45%) + Ternary : 495 (Ratio: 3.61%) + Conflict : 13701 (Average Length: 196.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 13701 (Average: 6.83 Max: 380 Sum: 93639) + Executed : 13664 (Average: 6.80 Max: 380 Sum: 93177 Ratio: 99.51%) + Bounded : 37 (Average: 12.49 Max: 17 Sum: 462 Ratio: 0.49%) + +Rules : 55133 (Original: 53913) +Atoms : 43853 +Bodies : 10280 (Original: 9059) + Count : 232 (Original: 476) +Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) +Tight : Yes +Variables : 57887 (Eliminated: 1464 Frozen: 48893) +Constraints : 381121 (Binary: 91.6% Ternary: 6.3% Other: 2.1%) + +Memory Peak : 222MB +Max. Length : 10 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 4.14s +Memory: 209MB (+14MB) +UNSAT +Iteration Time: 4.65s + +Iteration 5 +Queue: [(4,20,0,True), (5,25,0,True), (6,30,0,True)] +Grounded Until: 15 +Expected Memory: 229.0MB +Grounding... [('step', [16]), ('step', [17]), ('step', [18]), ('step', [19]), ('step', [20]), ('check', [20])] +Grounding Time: 0.30s +Memory: 212MB (+3MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 6 +Time : 21.097s (Solving: 17.72s 1st Model: 0.00s Unsat: 4.20s) +CPU Time : 21.012s + +Choices : 318692 (Domain: 274484) +Conflicts : 41885 (Analyzed: 41882) +Restarts : 161 (Average: 260.14 Last: 200) +Model-Level : 147.0 +Problems : 6 (Average Length: 11.17 Splits: 0) +Lemmas : 41882 (Deleted: 27757) + Binary : 2114 (Ratio: 5.05%) + Ternary : 772 (Ratio: 1.84%) + Conflict : 41882 (Average Length: 420.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 41882 (Average: 7.36 Max: 431 Sum: 308320) + Executed : 41843 (Average: 7.35 Max: 431 Sum: 307814 Ratio: 99.84%) + Bounded : 39 (Average: 12.97 Max: 22 Sum: 506 Ratio: 0.16%) + +Rules : 55133 (Original: 53913) +Atoms : 43853 +Bodies : 10280 (Original: 9059) + Count : 232 (Original: 476) +Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) +Tight : Yes +Variables : 80463 (Eliminated: 1464 Frozen: 71469) +Constraints : 538293 (Binary: 91.6% Ternary: 6.4% Other: 2.1%) + +Memory Peak : 227MB +Max. Length : 15 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 13.86s +Memory: 227MB (+15MB) +UNKNOWN +Iteration Time: 14.30s + +Iteration 6 +Queue: [(5,25,0,True), (6,30,0,True)] +Grounded Until: 20 +Expected Memory: 247.0MB +Grounding... [('step', [21]), ('step', [22]), ('step', [23]), ('step', [24]), ('step', [25]), ('check', [25])] +Grounding Time: 0.31s +Memory: 230MB (+3MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 7 +Time : 38.488s (Solving: 34.32s 1st Model: 0.00s Unsat: 4.20s) +CPU Time : 38.412s + +Choices : 544925 (Domain: 486198) +Conflicts : 70044 (Analyzed: 70041) +Restarts : 261 (Average: 268.36 Last: 203) +Model-Level : 147.0 +Problems : 7 (Average Length: 13.43 Splits: 0) +Lemmas : 70041 (Deleted: 53675) + Binary : 3314 (Ratio: 4.73%) + Ternary : 972 (Ratio: 1.39%) + Conflict : 70041 (Average Length: 595.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 70041 (Average: 7.41 Max: 431 Sum: 518924) + Executed : 70002 (Average: 7.40 Max: 431 Sum: 518418 Ratio: 99.90%) + Bounded : 39 (Average: 12.97 Max: 22 Sum: 506 Ratio: 0.10%) + +Rules : 55133 (Original: 53913) +Atoms : 43853 +Bodies : 10280 (Original: 9059) + Count : 232 (Original: 476) +Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) +Tight : Yes +Variables : 103039 (Eliminated: 1464 Frozen: 94045) +Constraints : 711310 (Binary: 91.6% Ternary: 6.4% Other: 2.0%) + +Memory Peak : 246MB +Max. Length : 20 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 16.94s +Memory: 242MB (+12MB) +UNKNOWN +Iteration Time: 17.40s + +Iteration 7 +Queue: [(6,30,0,True)] +Grounded Until: 25 +Expected Memory: 262.0MB +Grounding... [('step', [26]), ('step', [27]), ('step', [28]), ('step', [29]), ('step', [30]), ('check', [30])] +Grounding Time: 0.36s +Memory: 244MB (+2MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 8 +Time : 58.835s (Solving: 53.79s 1st Model: 0.00s Unsat: 4.20s) +CPU Time : 58.768s + +Choices : 795479 (Domain: 727093) +Conflicts : 98170 (Analyzed: 98167) +Restarts : 361 (Average: 271.93 Last: 203) +Model-Level : 147.0 +Problems : 8 (Average Length: 15.75 Splits: 0) +Lemmas : 98167 (Deleted: 80033) + Binary : 4642 (Ratio: 4.73%) + Ternary : 1200 (Ratio: 1.22%) + Conflict : 98167 (Average Length: 701.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 98167 (Average: 7.65 Max: 431 Sum: 751388) + Executed : 98127 (Average: 7.65 Max: 431 Sum: 750850 Ratio: 99.93%) + Bounded : 40 (Average: 13.45 Max: 32 Sum: 538 Ratio: 0.07%) + +Rules : 55133 (Original: 53913) +Atoms : 43853 +Bodies : 10280 (Original: 9059) + Count : 232 (Original: 476) +Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) +Tight : Yes +Variables : 125615 (Eliminated: 1464 Frozen: 116621) +Constraints : 884355 (Binary: 91.6% Ternary: 6.4% Other: 2.0%) + +Memory Peak : 390MB +Max. Length : 25 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 19.83s +Memory: 326MB (+82MB) +UNKNOWN +Iteration Time: 20.36s + +Iteration 8 +Queue: [(4,20,1,True), (5,25,1,True), (6,30,1,True), (7,35,0,True), (8,40,0,True), (9,45,0,True), (10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True), (17,85,0,True)] +Grounded Until: 30 +Blocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 9 +Time : 73.429s (Solving: 68.35s 1st Model: 0.00s Unsat: 4.20s) +CPU Time : 73.368s + +Choices : 908988 (Domain: 840602) +Conflicts : 126350 (Analyzed: 126347) +Restarts : 461 (Average: 274.07 Last: 203) +Model-Level : 147.0 +Problems : 9 (Average Length: 17.56 Splits: 0) +Lemmas : 126347 (Deleted: 107054) + Binary : 5110 (Ratio: 4.04%) + Ternary : 1272 (Ratio: 1.01%) + Conflict : 126347 (Average Length: 680.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 126347 (Average: 6.80 Max: 431 Sum: 859482) + Executed : 126306 (Average: 6.80 Max: 431 Sum: 858912 Ratio: 99.93%) + Bounded : 41 (Average: 13.90 Max: 32 Sum: 570 Ratio: 0.07%) + +Rules : 55133 (Original: 53913) +Atoms : 43853 +Bodies : 10280 (Original: 9059) + Count : 232 (Original: 476) +Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) +Tight : Yes +Variables : 125615 (Eliminated: 1464 Frozen: 124151) +Constraints : 884341 (Binary: 91.6% Ternary: 6.4% Other: 2.0%) + +Memory Peak : 390MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 14.58s +Memory: 326MB (+0MB) +UNKNOWN +Iteration Time: 14.60s + +Iteration 9 +Queue: [(5,25,1,True), (6,30,1,True), (7,35,0,True), (8,40,0,True), (9,45,0,True), (10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True), (17,85,0,True)] +Grounded Until: 30 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 10 +Time : 98.747s (Solving: 93.63s 1st Model: 0.00s Unsat: 4.20s) +CPU Time : 98.696s + +Choices : 1039074 (Domain: 970650) +Conflicts : 154469 (Analyzed: 154466) +Restarts : 561 (Average: 275.34 Last: 204) +Model-Level : 147.0 +Problems : 10 (Average Length: 19.00 Splits: 0) +Lemmas : 154466 (Deleted: 134626) + Binary : 5352 (Ratio: 3.46%) + Ternary : 1336 (Ratio: 0.86%) + Conflict : 154466 (Average Length: 791.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 154466 (Average: 6.32 Max: 431 Sum: 976481) + Executed : 154424 (Average: 6.32 Max: 431 Sum: 975879 Ratio: 99.94%) + Bounded : 42 (Average: 14.33 Max: 32 Sum: 602 Ratio: 0.06%) + +Rules : 55133 (Original: 53913) +Atoms : 43853 +Bodies : 10280 (Original: 9059) + Count : 232 (Original: 476) +Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) +Tight : Yes +Variables : 125615 (Eliminated: 1464 Frozen: 124151) +Constraints : 884328 (Binary: 91.6% Ternary: 6.4% Other: 2.0%) + +Memory Peak : 390MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 25.32s +Memory: 326MB (+0MB) +UNKNOWN +Iteration Time: 25.33s + +Iteration 10 +Queue: [(6,30,1,True), (7,35,0,True), (8,40,0,True), (9,45,0,True), (10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True), (17,85,0,True)] +Grounded Until: 30 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 11 +Time : 121.765s (Solving: 116.61s 1st Model: 0.00s Unsat: 4.20s) +CPU Time : 121.724s + +Choices : 1259852 (Domain: 1190405) +Conflicts : 182648 (Analyzed: 182645) +Restarts : 661 (Average: 276.32 Last: 204) +Model-Level : 147.0 +Problems : 11 (Average Length: 20.18 Splits: 0) +Lemmas : 182645 (Deleted: 161750) + Binary : 5826 (Ratio: 3.19%) + Ternary : 1427 (Ratio: 0.78%) + Conflict : 182645 (Average Length: 840.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 182645 (Average: 6.46 Max: 431 Sum: 1180686) + Executed : 182602 (Average: 6.46 Max: 431 Sum: 1180052 Ratio: 99.95%) + Bounded : 43 (Average: 14.74 Max: 32 Sum: 634 Ratio: 0.05%) + +Rules : 55133 (Original: 53913) +Atoms : 43853 +Bodies : 10280 (Original: 9059) + Count : 232 (Original: 476) +Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) +Tight : Yes +Variables : 125615 (Eliminated: 1464 Frozen: 124151) +Constraints : 884314 (Binary: 91.6% Ternary: 6.4% Other: 2.0%) + +Memory Peak : 390MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 23.01s +Memory: 326MB (+0MB) +UNKNOWN +Iteration Time: 23.03s + +Iteration 11 +Queue: [(7,35,0,True), (8,40,0,True), (9,45,0,True), (10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True), (17,85,0,True)] +Grounded Until: 30 +Expected Memory: 410.0MB +Grounding... [('step', [31]), ('step', [32]), ('step', [33]), ('step', [34]), ('step', [35]), ('check', [35])] +Grounding Time: 0.32s +Memory: 327MB (+1MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 12 +Time : 140.038s (Solving: 134.04s 1st Model: 0.00s Unsat: 4.20s) +CPU Time : 140.004s + +Choices : 1469681 (Domain: 1393123) +Conflicts : 210833 (Analyzed: 210830) +Restarts : 761 (Average: 277.04 Last: 204) +Model-Level : 147.0 +Problems : 12 (Average Length: 21.58 Splits: 0) +Lemmas : 210830 (Deleted: 188096) + Binary : 6845 (Ratio: 3.25%) + Ternary : 1557 (Ratio: 0.74%) + Conflict : 210830 (Average Length: 847.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 210830 (Average: 6.49 Max: 431 Sum: 1369029) + Executed : 210786 (Average: 6.49 Max: 431 Sum: 1368358 Ratio: 99.95%) + Bounded : 44 (Average: 15.25 Max: 37 Sum: 671 Ratio: 0.05%) + +Rules : 55133 (Original: 53913) +Atoms : 43853 +Bodies : 10280 (Original: 9059) + Count : 232 (Original: 476) +Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) +Tight : Yes +Variables : 148191 (Eliminated: 1464 Frozen: 139197) +Constraints : 1057342 (Binary: 91.6% Ternary: 6.5% Other: 2.0%) + +Memory Peak : 390MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 17.78s +Memory: 341MB (+14MB) +UNKNOWN +Iteration Time: 18.29s + +Iteration 12 +Queue: [(8,40,0,True), (9,45,0,True), (10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True), (17,85,0,True)] +Grounded Until: 35 +Expected Memory: 425.0MB +Grounding... [('step', [36]), ('step', [37]), ('step', [38]), ('step', [39]), ('step', [40]), ('check', [40])] +Grounding Time: 0.42s +Memory: 348MB (+7MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 13 +Time : 158.318s (Solving: 151.36s 1st Model: 0.00s Unsat: 4.20s) +CPU Time : 158.292s + +Choices : 1722991 (Domain: 1639840) +Conflicts : 239049 (Analyzed: 239046) +Restarts : 861 (Average: 277.64 Last: 204) +Model-Level : 147.0 +Problems : 13 (Average Length: 23.15 Splits: 0) +Lemmas : 239046 (Deleted: 215086) + Binary : 7595 (Ratio: 3.18%) + Ternary : 1618 (Ratio: 0.68%) + Conflict : 239046 (Average Length: 840.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 239046 (Average: 6.70 Max: 431 Sum: 1600769) + Executed : 239002 (Average: 6.69 Max: 431 Sum: 1600098 Ratio: 99.96%) + Bounded : 44 (Average: 15.25 Max: 37 Sum: 671 Ratio: 0.04%) + +Rules : 55133 (Original: 53913) +Atoms : 43853 +Bodies : 10280 (Original: 9059) + Count : 232 (Original: 476) +Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) +Tight : Yes +Variables : 170767 (Eliminated: 1464 Frozen: 161773) +Constraints : 1230373 (Binary: 91.6% Ternary: 6.5% Other: 2.0%) + +Memory Peak : 390MB +Max. Length : 35 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 17.68s +Memory: 362MB (+14MB) +UNKNOWN +Iteration Time: 18.29s + +Iteration 13 +Queue: [(9,45,0,True), (10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True), (17,85,0,True)] +Grounded Until: 40 +Expected Memory: 446.0MB +Grounding... [('step', [41]), ('step', [42]), ('step', [43]), ('step', [44]), ('step', [45]), ('check', [45])] +Grounding Time: 0.31s +Memory: 366MB (+4MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 14 +Time : 175.477s (Solving: 167.66s 1st Model: 0.00s Unsat: 4.20s) +CPU Time : 175.456s + +Choices : 1976070 (Domain: 1888390) +Conflicts : 267225 (Analyzed: 267222) +Restarts : 961 (Average: 278.07 Last: 204) +Model-Level : 147.0 +Problems : 14 (Average Length: 24.86 Splits: 0) +Lemmas : 267222 (Deleted: 241788) + Binary : 8210 (Ratio: 3.07%) + Ternary : 1715 (Ratio: 0.64%) + Conflict : 267222 (Average Length: 830.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 267222 (Average: 6.86 Max: 431 Sum: 1833630) + Executed : 267178 (Average: 6.86 Max: 431 Sum: 1832959 Ratio: 99.96%) + Bounded : 44 (Average: 15.25 Max: 37 Sum: 671 Ratio: 0.04%) + +Rules : 55133 (Original: 53913) +Atoms : 43853 +Bodies : 10280 (Original: 9059) + Count : 232 (Original: 476) +Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) +Tight : Yes +Variables : 193343 (Eliminated: 1464 Frozen: 184349) +Constraints : 1403418 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) + +Memory Peak : 391MB +Max. Length : 40 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 16.67s +Memory: 389MB (+23MB) +UNKNOWN +Iteration Time: 17.18s + +Iteration 14 +Queue: [(10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True), (17,85,0,True)] +Grounded Until: 45 +Expected Memory: 473.0MB +Grounding... [('step', [46]), ('step', [47]), ('step', [48]), ('step', [49]), ('step', [50]), ('check', [50])] +Grounding Time: 0.32s +Memory: 389MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 15 +Time : 193.509s (Solving: 184.81s 1st Model: 0.00s Unsat: 4.20s) +CPU Time : 193.496s + +Choices : 2212664 (Domain: 2122911) +Conflicts : 295414 (Analyzed: 295411) +Restarts : 1061 (Average: 278.43 Last: 204) +Model-Level : 147.0 +Problems : 15 (Average Length: 26.67 Splits: 0) +Lemmas : 295411 (Deleted: 268828) + Binary : 8624 (Ratio: 2.92%) + Ternary : 1761 (Ratio: 0.60%) + Conflict : 295411 (Average Length: 827.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 295411 (Average: 6.94 Max: 431 Sum: 2050016) + Executed : 295365 (Average: 6.94 Max: 431 Sum: 2049241 Ratio: 99.96%) + Bounded : 46 (Average: 16.85 Max: 52 Sum: 775 Ratio: 0.04%) + +Rules : 55133 (Original: 53913) +Atoms : 43853 +Bodies : 10280 (Original: 9059) + Count : 232 (Original: 476) +Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) +Tight : Yes +Variables : 215919 (Eliminated: 1464 Frozen: 206925) +Constraints : 1576463 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) + +Memory Peak : 419MB +Max. Length : 45 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 17.51s +Memory: 403MB (+14MB) +UNKNOWN +Iteration Time: 18.05s + +Iteration 15 +Queue: [(11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True), (17,85,0,True)] +Grounded Until: 50 +Expected Memory: 487.0MB +Grounding... [('step', [51]), ('step', [52]), ('step', [53]), ('step', [54]), ('step', [55]), ('check', [55])] +Grounding Time: 0.32s +Memory: 403MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 16 +Time : 212.232s (Solving: 202.65s 1st Model: 0.00s Unsat: 4.20s) +CPU Time : 212.228s + +Choices : 2583279 (Domain: 2479786) +Conflicts : 323565 (Analyzed: 323562) +Restarts : 1161 (Average: 278.69 Last: 204) +Model-Level : 147.0 +Problems : 16 (Average Length: 28.56 Splits: 0) +Lemmas : 323562 (Deleted: 295387) + Binary : 9565 (Ratio: 2.96%) + Ternary : 1916 (Ratio: 0.59%) + Conflict : 323562 (Average Length: 836.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 323562 (Average: 7.38 Max: 431 Sum: 2387890) + Executed : 323516 (Average: 7.38 Max: 431 Sum: 2387115 Ratio: 99.97%) + Bounded : 46 (Average: 16.85 Max: 52 Sum: 775 Ratio: 0.03%) + +Rules : 55133 (Original: 53913) +Atoms : 43853 +Bodies : 10280 (Original: 9059) + Count : 232 (Original: 476) +Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) +Tight : Yes +Variables : 238495 (Eliminated: 1464 Frozen: 229501) +Constraints : 1749480 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) + +Memory Peak : 437MB +Max. Length : 50 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 18.21s +Memory: 417MB (+14MB) +UNKNOWN +Iteration Time: 18.74s + +Iteration 16 +Queue: [(12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True), (17,85,0,True)] +Grounded Until: 55 +Expected Memory: 501.0MB +Grounding... [('step', [56]), ('step', [57]), ('step', [58]), ('step', [59]), ('step', [60]), ('check', [60])] +Grounding Time: 0.36s +Memory: 417MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 17 +Time : 231.016s (Solving: 220.49s 1st Model: 0.00s Unsat: 4.20s) +CPU Time : 231.020s + +Choices : 2835214 (Domain: 2730967) +Conflicts : 351769 (Analyzed: 351766) +Restarts : 1261 (Average: 278.96 Last: 204) +Model-Level : 147.0 +Problems : 17 (Average Length: 30.53 Splits: 0) +Lemmas : 351766 (Deleted: 322486) + Binary : 9951 (Ratio: 2.83%) + Ternary : 1978 (Ratio: 0.56%) + Conflict : 351766 (Average Length: 825.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 351766 (Average: 7.44 Max: 431 Sum: 2618009) + Executed : 351719 (Average: 7.44 Max: 431 Sum: 2617172 Ratio: 99.97%) + Bounded : 47 (Average: 17.81 Max: 62 Sum: 837 Ratio: 0.03%) + +Rules : 55133 (Original: 53913) +Atoms : 43853 +Bodies : 10280 (Original: 9059) + Count : 232 (Original: 476) +Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) +Tight : Yes +Variables : 261071 (Eliminated: 1464 Frozen: 252077) +Constraints : 1922525 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) + +Memory Peak : 454MB +Max. Length : 55 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 18.21s +Memory: 432MB (+15MB) +UNKNOWN +Iteration Time: 18.80s + +Iteration 17 +Queue: [(13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True), (17,85,0,True)] +Grounded Until: 60 +Expected Memory: 516.0MB +Grounding... [('step', [61]), ('step', [62]), ('step', [63]), ('step', [64]), ('step', [65]), ('check', [65])] +Grounding Time: 0.35s +Memory: 432MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 18 +Time : 251.557s (Solving: 240.07s 1st Model: 0.00s Unsat: 4.20s) +CPU Time : 251.568s + +Choices : 3279607 (Domain: 3169584) +Conflicts : 379925 (Analyzed: 379922) +Restarts : 1361 (Average: 279.15 Last: 204) +Model-Level : 147.0 +Problems : 18 (Average Length: 32.56 Splits: 0) +Lemmas : 379922 (Deleted: 348956) + Binary : 11063 (Ratio: 2.91%) + Ternary : 2142 (Ratio: 0.56%) + Conflict : 379922 (Average Length: 826.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 379922 (Average: 7.96 Max: 431 Sum: 3025976) + Executed : 379875 (Average: 7.96 Max: 431 Sum: 3025139 Ratio: 99.97%) + Bounded : 47 (Average: 17.81 Max: 62 Sum: 837 Ratio: 0.03%) + +Rules : 55133 (Original: 53913) +Atoms : 43853 +Bodies : 10280 (Original: 9059) + Count : 232 (Original: 476) +Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) +Tight : Yes +Variables : 283647 (Eliminated: 1464 Frozen: 274653) +Constraints : 2095556 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) + +Memory Peak : 471MB +Max. Length : 60 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 19.96s +Memory: 465MB (+33MB) +UNKNOWN +Iteration Time: 20.56s + +Iteration 18 +Queue: [(14,70,0,True), (15,75,0,True), (16,80,0,True), (17,85,0,True)] +Grounded Until: 65 +Expected Memory: 549.0MB +Grounding... [('step', [66]), ('step', [67]), ('step', [68]), ('step', [69]), ('step', [70]), ('check', [70])] +Grounding Time: 0.33s +Memory: 465MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 19 +Time : 273.683s (Solving: 261.27s 1st Model: 0.00s Unsat: 4.20s) +CPU Time : 273.704s + +Choices : 3620280 (Domain: 3509710) +Conflicts : 408106 (Analyzed: 408103) +Restarts : 1461 (Average: 279.33 Last: 204) +Model-Level : 147.0 +Problems : 19 (Average Length: 34.63 Splits: 0) +Lemmas : 408103 (Deleted: 375917) + Binary : 11570 (Ratio: 2.84%) + Ternary : 2226 (Ratio: 0.55%) + Conflict : 408103 (Average Length: 829.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 408103 (Average: 8.18 Max: 431 Sum: 3337540) + Executed : 408056 (Average: 8.18 Max: 431 Sum: 3336703 Ratio: 99.97%) + Bounded : 47 (Average: 17.81 Max: 62 Sum: 837 Ratio: 0.03%) + +Rules : 55133 (Original: 53913) +Atoms : 43853 +Bodies : 10280 (Original: 9059) + Count : 232 (Original: 476) +Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) +Tight : Yes +Variables : 306223 (Eliminated: 1464 Frozen: 297229) +Constraints : 2268601 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) + +Memory Peak : 503MB +Max. Length : 65 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 21.57s +Memory: 477MB (+12MB) +UNKNOWN +Iteration Time: 22.14s + +Iteration 19 +Queue: [(15,75,0,True), (16,80,0,True), (17,85,0,True)] +Grounded Until: 70 +Expected Memory: 561.0MB +Grounding... [('step', [71]), ('step', [72]), ('step', [73]), ('step', [74]), ('step', [75]), ('check', [75])] +Grounding Time: 0.34s +Memory: 477MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 20 +Time : 294.476s (Solving: 281.11s 1st Model: 0.00s Unsat: 4.20s) +CPU Time : 294.504s + +Choices : 4030873 (Domain: 3916810) +Conflicts : 436313 (Analyzed: 436310) +Restarts : 1561 (Average: 279.51 Last: 204) +Model-Level : 147.0 +Problems : 20 (Average Length: 36.75 Splits: 0) +Lemmas : 436310 (Deleted: 401371) + Binary : 12272 (Ratio: 2.81%) + Ternary : 2334 (Ratio: 0.53%) + Conflict : 436310 (Average Length: 833.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 436310 (Average: 8.51 Max: 431 Sum: 3714399) + Executed : 436263 (Average: 8.51 Max: 431 Sum: 3713562 Ratio: 99.98%) + Bounded : 47 (Average: 17.81 Max: 62 Sum: 837 Ratio: 0.02%) + +Rules : 55133 (Original: 53913) +Atoms : 43853 +Bodies : 10280 (Original: 9059) + Count : 232 (Original: 476) +Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) +Tight : Yes +Variables : 328799 (Eliminated: 1464 Frozen: 319805) +Constraints : 2441646 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) + +Memory Peak : 518MB +Max. Length : 70 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 20.23s +Memory: 492MB (+15MB) +UNKNOWN +Iteration Time: 20.81s + +Iteration 20 +Queue: [(16,80,0,True), (17,85,0,True)] +Grounded Until: 75 +Expected Memory: 576.0MB +Grounding... [('step', [76]), ('step', [77]), ('step', [78]), ('step', [79]), ('step', [80]), ('check', [80])] +Grounding Time: 0.48s +Memory: 507MB (+15MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 21 +Time : 316.121s (Solving: 301.64s 1st Model: 0.00s Unsat: 4.20s) +CPU Time : 316.156s + +Choices : 4363980 (Domain: 4249676) +Conflicts : 464504 (Analyzed: 464501) +Restarts : 1661 (Average: 279.65 Last: 204) +Model-Level : 147.0 +Problems : 21 (Average Length: 38.90 Splits: 0) +Lemmas : 464501 (Deleted: 429631) + Binary : 12709 (Ratio: 2.74%) + Ternary : 2409 (Ratio: 0.52%) + Conflict : 464501 (Average Length: 830.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 464501 (Average: 8.65 Max: 431 Sum: 4016299) + Executed : 464453 (Average: 8.64 Max: 431 Sum: 4015380 Ratio: 99.98%) + Bounded : 48 (Average: 19.15 Max: 82 Sum: 919 Ratio: 0.02%) + +Rules : 55133 (Original: 53913) +Atoms : 43853 +Bodies : 10280 (Original: 9059) + Count : 232 (Original: 476) +Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) +Tight : Yes +Variables : 351375 (Eliminated: 1464 Frozen: 342381) +Constraints : 2614691 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) + +Memory Peak : 554MB +Max. Length : 75 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 20.92s +Memory: 521MB (+14MB) +UNKNOWN +Iteration Time: 21.66s + +Iteration 21 +Queue: [(17,85,0,True)] +Grounded Until: 80 +Expected Memory: 605.0MB +Grounding... [('step', [81]), ('step', [82]), ('step', [83]), ('step', [84]), ('step', [85]), ('check', [85])] +Grounding Time: 0.32s +Memory: 521MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 22 +Time : 339.079s (Solving: 323.63s 1st Model: 0.00s Unsat: 4.20s) +CPU Time : 339.124s + +Choices : 4698272 (Domain: 4583605) +Conflicts : 492648 (Analyzed: 492645) +Restarts : 1761 (Average: 279.75 Last: 204) +Model-Level : 147.0 +Problems : 22 (Average Length: 41.09 Splits: 0) +Lemmas : 492645 (Deleted: 456973) + Binary : 13120 (Ratio: 2.66%) + Ternary : 2458 (Ratio: 0.50%) + Conflict : 492645 (Average Length: 839.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 492645 (Average: 8.75 Max: 431 Sum: 4309179) + Executed : 492597 (Average: 8.75 Max: 431 Sum: 4308260 Ratio: 99.98%) + Bounded : 48 (Average: 19.15 Max: 82 Sum: 919 Ratio: 0.02%) + +Rules : 55133 (Original: 53913) +Atoms : 43853 +Bodies : 10280 (Original: 9059) + Count : 232 (Original: 476) +Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) +Tight : Yes +Variables : 373951 (Eliminated: 1464 Frozen: 364957) +Constraints : 2787722 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) + +Memory Peak : 570MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 22.39s +Memory: 535MB (+14MB) +UNKNOWN +Iteration Time: 22.97s + +Iteration 22 +Queue: [(4,20,2,True), (5,25,2,True), (6,30,2,True), (7,35,1,True), (8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 85 +Blocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 23 +Time : 350.517s (Solving: 334.98s 1st Model: 0.00s Unsat: 4.20s) +CPU Time : 350.568s + +Choices : 4813255 (Domain: 4698588) +Conflicts : 520838 (Analyzed: 520835) +Restarts : 1861 (Average: 279.87 Last: 204) +Model-Level : 147.0 +Problems : 23 (Average Length: 43.09 Splits: 0) +Lemmas : 520835 (Deleted: 484258) + Binary : 13398 (Ratio: 2.57%) + Ternary : 2506 (Ratio: 0.48%) + Conflict : 520835 (Average Length: 826.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 520835 (Average: 8.48 Max: 431 Sum: 4417398) + Executed : 520786 (Average: 8.48 Max: 431 Sum: 4416392 Ratio: 99.98%) + Bounded : 49 (Average: 20.53 Max: 87 Sum: 1006 Ratio: 0.02%) + +Rules : 55133 (Original: 53913) +Atoms : 43853 +Bodies : 10280 (Original: 9059) + Count : 232 (Original: 476) +Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) +Tight : Yes +Variables : 373951 (Eliminated: 1464 Frozen: 372487) +Constraints : 2787722 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) + +Memory Peak : 570MB +Max. Length : 85 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 11.41s +Memory: 537MB (+2MB) +UNKNOWN +Iteration Time: 11.45s + +Iteration 23 +Queue: [(5,25,2,True), (6,30,2,True), (7,35,1,True), (8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 85 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 24 +Time : 376.151s (Solving: 360.52s 1st Model: 0.00s Unsat: 4.20s) +CPU Time : 376.216s + +Choices : 4911678 (Domain: 4797011) +Conflicts : 548996 (Analyzed: 548993) +Restarts : 1961 (Average: 279.96 Last: 204) +Model-Level : 147.0 +Problems : 24 (Average Length: 44.92 Splits: 0) +Lemmas : 548993 (Deleted: 511889) + Binary : 13480 (Ratio: 2.46%) + Ternary : 2531 (Ratio: 0.46%) + Conflict : 548993 (Average Length: 846.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 548993 (Average: 8.21 Max: 431 Sum: 4506436) + Executed : 548943 (Average: 8.21 Max: 431 Sum: 4505343 Ratio: 99.98%) + Bounded : 50 (Average: 21.86 Max: 87 Sum: 1093 Ratio: 0.02%) + +Rules : 55133 (Original: 53913) +Atoms : 43853 +Bodies : 10280 (Original: 9059) + Count : 232 (Original: 476) +Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) +Tight : Yes +Variables : 373951 (Eliminated: 1464 Frozen: 372487) +Constraints : 2787708 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) + +Memory Peak : 570MB +Max. Length : 85 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 25.61s +Memory: 537MB (+0MB) +UNKNOWN +Iteration Time: 25.65s + +Iteration 24 +Queue: [(6,30,2,True), (7,35,1,True), (8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 85 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 25 +Time : 395.354s (Solving: 379.63s 1st Model: 0.00s Unsat: 4.20s) +CPU Time : 395.428s + +Choices : 5101516 (Domain: 4986849) +Conflicts : 577235 (Analyzed: 577232) +Restarts : 2061 (Average: 280.07 Last: 204) +Model-Level : 147.0 +Problems : 25 (Average Length: 46.60 Splits: 0) +Lemmas : 577232 (Deleted: 539550) + Binary : 13703 (Ratio: 2.37%) + Ternary : 2558 (Ratio: 0.44%) + Conflict : 577232 (Average Length: 861.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 577232 (Average: 8.11 Max: 431 Sum: 4678791) + Executed : 577182 (Average: 8.10 Max: 431 Sum: 4677698 Ratio: 99.98%) + Bounded : 50 (Average: 21.86 Max: 87 Sum: 1093 Ratio: 0.02%) + +Rules : 55133 (Original: 53913) +Atoms : 43853 +Bodies : 10280 (Original: 9059) + Count : 232 (Original: 476) +Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) +Tight : Yes +Variables : 373951 (Eliminated: 1464 Frozen: 372487) +Constraints : 2787694 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) + +Memory Peak : 570MB +Max. Length : 85 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 19.18s +Memory: 537MB (+0MB) +UNKNOWN +Iteration Time: 19.22s + +Iteration 25 +Queue: [(7,35,1,True), (8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 85 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 26 +Time : 413.248s (Solving: 397.41s 1st Model: 0.00s Unsat: 4.20s) +CPU Time : 413.328s + +Choices : 5288141 (Domain: 5173473) +Conflicts : 605398 (Analyzed: 605395) +Restarts : 2161 (Average: 280.15 Last: 204) +Model-Level : 147.0 +Problems : 26 (Average Length: 48.15 Splits: 0) +Lemmas : 605395 (Deleted: 566903) + Binary : 13934 (Ratio: 2.30%) + Ternary : 2601 (Ratio: 0.43%) + Conflict : 605395 (Average Length: 864.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 605395 (Average: 8.01 Max: 431 Sum: 4847208) + Executed : 605345 (Average: 8.00 Max: 431 Sum: 4846115 Ratio: 99.98%) + Bounded : 50 (Average: 21.86 Max: 87 Sum: 1093 Ratio: 0.02%) + +Rules : 55133 (Original: 53913) +Atoms : 43853 +Bodies : 10280 (Original: 9059) + Count : 232 (Original: 476) +Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) +Tight : Yes +Variables : 373951 (Eliminated: 1464 Frozen: 372487) +Constraints : 2787694 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) + +Memory Peak : 570MB +Max. Length : 85 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 17.85s +Memory: 537MB (+0MB) +UNKNOWN +Iteration Time: 17.90s + +Iteration 26 +Queue: [(8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 85 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 27 +Time : 434.403s (Solving: 418.46s 1st Model: 0.00s Unsat: 4.20s) +CPU Time : 434.492s + +Choices : 5485373 (Domain: 5370691) +Conflicts : 633582 (Analyzed: 633579) +Restarts : 2261 (Average: 280.22 Last: 204) +Model-Level : 147.0 +Problems : 27 (Average Length: 49.59 Splits: 0) +Lemmas : 633579 (Deleted: 594155) + Binary : 14225 (Ratio: 2.25%) + Ternary : 2658 (Ratio: 0.42%) + Conflict : 633579 (Average Length: 875.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 633579 (Average: 7.93 Max: 431 Sum: 5022002) + Executed : 633529 (Average: 7.92 Max: 431 Sum: 5020909 Ratio: 99.98%) + Bounded : 50 (Average: 21.86 Max: 87 Sum: 1093 Ratio: 0.02%) + +Rules : 55133 (Original: 53913) +Atoms : 43853 +Bodies : 10280 (Original: 9059) + Count : 232 (Original: 476) +Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) +Tight : Yes +Variables : 373951 (Eliminated: 1464 Frozen: 372487) +Constraints : 2787694 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) + +Memory Peak : 570MB +Max. Length : 85 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 21.12s +Memory: 537MB (+0MB) +UNKNOWN +Iteration Time: 21.17s + +Iteration 27 +Queue: [(9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 85 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 28 +Time : 451.839s (Solving: 435.81s 1st Model: 0.00s Unsat: 4.20s) +CPU Time : 451.932s + +Choices : 5700364 (Domain: 5584170) +Conflicts : 661765 (Analyzed: 661762) +Restarts : 2361 (Average: 280.29 Last: 204) +Model-Level : 147.0 +Problems : 28 (Average Length: 50.93 Splits: 0) +Lemmas : 661762 (Deleted: 621439) + Binary : 14657 (Ratio: 2.21%) + Ternary : 2708 (Ratio: 0.41%) + Conflict : 661762 (Average Length: 872.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 661762 (Average: 7.88 Max: 431 Sum: 5212706) + Executed : 661712 (Average: 7.88 Max: 431 Sum: 5211613 Ratio: 99.98%) + Bounded : 50 (Average: 21.86 Max: 87 Sum: 1093 Ratio: 0.02%) + +Rules : 55133 (Original: 53913) +Atoms : 43853 +Bodies : 10280 (Original: 9059) + Count : 232 (Original: 476) +Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) +Tight : Yes +Variables : 373951 (Eliminated: 1464 Frozen: 372487) +Constraints : 2787694 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) + +Memory Peak : 570MB +Max. Length : 85 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 17.41s +Memory: 537MB (+0MB) +UNKNOWN +Iteration Time: 17.45s + +Iteration 28 +Queue: [(10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 85 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 29 +Time : 468.754s (Solving: 452.63s 1st Model: 0.00s Unsat: 4.20s) +CPU Time : 468.856s + +Choices : 5892645 (Domain: 5776369) +Conflicts : 689962 (Analyzed: 689959) +Restarts : 2461 (Average: 280.36 Last: 204) +Model-Level : 147.0 +Problems : 29 (Average Length: 52.17 Splits: 0) +Lemmas : 689959 (Deleted: 647517) + Binary : 14908 (Ratio: 2.16%) + Ternary : 2759 (Ratio: 0.40%) + Conflict : 689959 (Average Length: 871.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 689959 (Average: 7.80 Max: 431 Sum: 5382814) + Executed : 689909 (Average: 7.80 Max: 431 Sum: 5381721 Ratio: 99.98%) + Bounded : 50 (Average: 21.86 Max: 87 Sum: 1093 Ratio: 0.02%) + +Rules : 55133 (Original: 53913) +Atoms : 43853 +Bodies : 10280 (Original: 9059) + Count : 232 (Original: 476) +Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) +Tight : Yes +Variables : 373951 (Eliminated: 1464 Frozen: 372487) +Constraints : 2787694 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) + +Memory Peak : 570MB +Max. Length : 85 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 16.89s +Memory: 537MB (+0MB) +UNKNOWN +Iteration Time: 16.93s + +Iteration 29 +Queue: [(11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 85 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 30 +Time : 489.515s (Solving: 473.27s 1st Model: 0.00s Unsat: 4.20s) +CPU Time : 489.628s + +Choices : 6121052 (Domain: 6004694) +Conflicts : 718096 (Analyzed: 718093) +Restarts : 2561 (Average: 280.40 Last: 204) +Model-Level : 147.0 +Problems : 30 (Average Length: 53.33 Splits: 0) +Lemmas : 718093 (Deleted: 676101) + Binary : 15186 (Ratio: 2.11%) + Ternary : 2806 (Ratio: 0.39%) + Conflict : 718093 (Average Length: 878.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 718093 (Average: 7.78 Max: 431 Sum: 5583729) + Executed : 718043 (Average: 7.77 Max: 431 Sum: 5582636 Ratio: 99.98%) + Bounded : 50 (Average: 21.86 Max: 87 Sum: 1093 Ratio: 0.02%) + +Rules : 55133 (Original: 53913) +Atoms : 43853 +Bodies : 10280 (Original: 9059) + Count : 232 (Original: 476) +Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) +Tight : Yes +Variables : 373951 (Eliminated: 1464 Frozen: 372487) +Constraints : 2787694 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) + +Memory Peak : 570MB +Max. Length : 85 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 20.72s +Memory: 537MB (+0MB) +UNKNOWN +Iteration Time: 20.77s + +Iteration 30 +Queue: [(12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 85 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 31 +Time : 508.521s (Solving: 492.15s 1st Model: 0.00s Unsat: 4.20s) +CPU Time : 508.640s + +Choices : 6340515 (Domain: 6223979) +Conflicts : 746262 (Analyzed: 746259) +Restarts : 2661 (Average: 280.44 Last: 204) +Model-Level : 147.0 +Problems : 31 (Average Length: 54.42 Splits: 0) +Lemmas : 746259 (Deleted: 703489) + Binary : 15397 (Ratio: 2.06%) + Ternary : 2842 (Ratio: 0.38%) + Conflict : 746259 (Average Length: 881.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 746259 (Average: 7.74 Max: 431 Sum: 5774391) + Executed : 746208 (Average: 7.74 Max: 431 Sum: 5773211 Ratio: 99.98%) + Bounded : 51 (Average: 23.14 Max: 87 Sum: 1180 Ratio: 0.02%) + +Rules : 55133 (Original: 53913) +Atoms : 43853 +Bodies : 10280 (Original: 9059) + Count : 232 (Original: 476) +Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) +Tight : Yes +Variables : 373951 (Eliminated: 1464 Frozen: 372487) +Constraints : 2787694 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) + +Memory Peak : 570MB +Max. Length : 85 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 18.96s +Memory: 537MB (+0MB) +UNKNOWN +Iteration Time: 19.02s + +Iteration 31 +Queue: [(13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 85 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 32 +Time : 527.510s (Solving: 511.05s 1st Model: 0.00s Unsat: 4.20s) +CPU Time : 527.636s + +Choices : 6600559 (Domain: 6482924) +Conflicts : 774478 (Analyzed: 774475) +Restarts : 2761 (Average: 280.51 Last: 204) +Model-Level : 147.0 +Problems : 32 (Average Length: 55.44 Splits: 0) +Lemmas : 774475 (Deleted: 730698) + Binary : 15878 (Ratio: 2.05%) + Ternary : 2908 (Ratio: 0.38%) + Conflict : 774475 (Average Length: 883.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 774475 (Average: 7.75 Max: 431 Sum: 6000830) + Executed : 774424 (Average: 7.75 Max: 431 Sum: 5999650 Ratio: 99.98%) + Bounded : 51 (Average: 23.14 Max: 87 Sum: 1180 Ratio: 0.02%) + +Rules : 55133 (Original: 53913) +Atoms : 43853 +Bodies : 10280 (Original: 9059) + Count : 232 (Original: 476) +Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) +Tight : Yes +Variables : 373951 (Eliminated: 1464 Frozen: 372487) +Constraints : 2787687 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) + +Memory Peak : 570MB +Max. Length : 85 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 18.96s +Memory: 537MB (+0MB) +UNKNOWN +Iteration Time: 19.00s + +Iteration 32 +Queue: [(14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 85 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 33 +Time : 547.765s (Solving: 531.21s 1st Model: 0.00s Unsat: 4.20s) +CPU Time : 547.900s + +Choices : 6914199 (Domain: 6794643) +Conflicts : 802630 (Analyzed: 802627) +Restarts : 2861 (Average: 280.54 Last: 204) +Model-Level : 147.0 +Problems : 33 (Average Length: 56.39 Splits: 0) +Lemmas : 802627 (Deleted: 757893) + Binary : 16327 (Ratio: 2.03%) + Ternary : 2968 (Ratio: 0.37%) + Conflict : 802627 (Average Length: 885.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 802627 (Average: 7.82 Max: 431 Sum: 6279139) + Executed : 802576 (Average: 7.82 Max: 431 Sum: 6277959 Ratio: 99.98%) + Bounded : 51 (Average: 23.14 Max: 87 Sum: 1180 Ratio: 0.02%) + +Rules : 55133 (Original: 53913) +Atoms : 43853 +Bodies : 10280 (Original: 9059) + Count : 232 (Original: 476) +Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) +Tight : Yes +Variables : 373951 (Eliminated: 1464 Frozen: 372487) +Constraints : 2787687 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) + +Memory Peak : 570MB +Max. Length : 85 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 20.22s +Memory: 537MB (+0MB) +UNKNOWN +Iteration Time: 20.27s + +Iteration 33 +Queue: [(15,75,1,True), (16,80,1,True), (17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 85 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 34 +Time : 568.390s (Solving: 551.74s 1st Model: 0.00s Unsat: 4.20s) +CPU Time : 568.536s + +Choices : 7151395 (Domain: 7031757) +Conflicts : 830822 (Analyzed: 830819) +Restarts : 2961 (Average: 280.59 Last: 204) +Model-Level : 147.0 +Problems : 34 (Average Length: 57.29 Splits: 0) +Lemmas : 830819 (Deleted: 785308) + Binary : 16566 (Ratio: 1.99%) + Ternary : 3004 (Ratio: 0.36%) + Conflict : 830819 (Average Length: 889.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 830819 (Average: 7.81 Max: 431 Sum: 6485634) + Executed : 830768 (Average: 7.80 Max: 431 Sum: 6484454 Ratio: 99.98%) + Bounded : 51 (Average: 23.14 Max: 87 Sum: 1180 Ratio: 0.02%) + +Rules : 55133 (Original: 53913) +Atoms : 43853 +Bodies : 10280 (Original: 9059) + Count : 232 (Original: 476) +Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) +Tight : Yes +Variables : 373951 (Eliminated: 1464 Frozen: 372487) +Constraints : 2787687 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) + +Memory Peak : 570MB +Max. Length : 85 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 20.60s +Memory: 537MB (+0MB) +UNKNOWN +Iteration Time: 20.64s + +Iteration 34 +Queue: [(16,80,1,True), (17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 85 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 35 +Time : 589.267s (Solving: 572.51s 1st Model: 0.00s Unsat: 4.20s) +CPU Time : 589.420s + +Choices : 7441227 (Domain: 7316328) +Conflicts : 858998 (Analyzed: 858995) +Restarts : 3061 (Average: 280.63 Last: 204) +Model-Level : 147.0 +Problems : 35 (Average Length: 58.14 Splits: 0) +Lemmas : 858995 (Deleted: 812298) + Binary : 17110 (Ratio: 1.99%) + Ternary : 3091 (Ratio: 0.36%) + Conflict : 858995 (Average Length: 892.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 858995 (Average: 7.85 Max: 431 Sum: 6741586) + Executed : 858944 (Average: 7.85 Max: 431 Sum: 6740406 Ratio: 99.98%) + Bounded : 51 (Average: 23.14 Max: 87 Sum: 1180 Ratio: 0.02%) + +Rules : 55133 (Original: 53913) +Atoms : 43853 +Bodies : 10280 (Original: 9059) + Count : 232 (Original: 476) +Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) +Tight : Yes +Variables : 373951 (Eliminated: 1464 Frozen: 372487) +Constraints : 2787687 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) + +Memory Peak : 570MB +Max. Length : 85 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 20.85s +Memory: 537MB (+0MB) +UNKNOWN +Iteration Time: 20.89s + +Iteration 35 +Queue: [(17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 85 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 36 +Time : 611.139s (Solving: 594.28s 1st Model: 0.00s Unsat: 4.20s) +CPU Time : 611.300s + +Choices : 7717670 (Domain: 7592616) +Conflicts : 887211 (Analyzed: 887208) +Restarts : 3161 (Average: 280.67 Last: 204) +Model-Level : 147.0 +Problems : 36 (Average Length: 58.94 Splits: 0) +Lemmas : 887208 (Deleted: 839899) + Binary : 17380 (Ratio: 1.96%) + Ternary : 3137 (Ratio: 0.35%) + Conflict : 887208 (Average Length: 893.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 887208 (Average: 7.87 Max: 493 Sum: 6983010) + Executed : 887157 (Average: 7.87 Max: 493 Sum: 6981830 Ratio: 99.98%) + Bounded : 51 (Average: 23.14 Max: 87 Sum: 1180 Ratio: 0.02%) + +Rules : 55133 (Original: 53913) +Atoms : 43853 +Bodies : 10280 (Original: 9059) + Count : 232 (Original: 476) +Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) +Tight : Yes +Variables : 373951 (Eliminated: 1464 Frozen: 372487) +Constraints : 2787687 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) + +Memory Peak : 570MB +Max. Length : 85 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 21.84s +Memory: 537MB (+0MB) +UNKNOWN +Iteration Time: 21.88s + +Iteration 36 +Queue: [(18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 85 +Expected Memory: 621.0MB +Grounding... [('step', [86]), ('step', [87]), ('step', [88]), ('step', [89]), ('step', [90]), ('check', [90])] +Grounding Time: 0.32s +Memory: 537MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 37 +Time : 632.985s (Solving: 615.15s 1st Model: 0.00s Unsat: 4.20s) +CPU Time : 633.156s + +Choices : 7997616 (Domain: 7872364) +Conflicts : 915441 (Analyzed: 915438) +Restarts : 3261 (Average: 280.72 Last: 204) +Model-Level : 147.0 +Problems : 37 (Average Length: 59.84 Splits: 0) +Lemmas : 915438 (Deleted: 867282) + Binary : 17707 (Ratio: 1.93%) + Ternary : 3182 (Ratio: 0.35%) + Conflict : 915438 (Average Length: 893.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 915438 (Average: 7.89 Max: 493 Sum: 7226121) + Executed : 915387 (Average: 7.89 Max: 493 Sum: 7224941 Ratio: 99.98%) + Bounded : 51 (Average: 23.14 Max: 87 Sum: 1180 Ratio: 0.02%) + +Rules : 55133 (Original: 53913) +Atoms : 43853 +Bodies : 10280 (Original: 9059) + Count : 232 (Original: 476) +Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) +Tight : Yes +Variables : 396527 (Eliminated: 1464 Frozen: 387533) +Constraints : 2960732 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) + +Memory Peak : 587MB +Max. Length : 85 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 21.26s +Memory: 549MB (+12MB) +UNKNOWN +Iteration Time: 21.86s + +Iteration 37 +Queue: [(19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 90 +Expected Memory: 633.0MB +Grounding... [('step', [91]), ('step', [92]), ('step', [93]), ('step', [94]), ('step', [95]), ('check', [95])] +Grounding Time: 0.32s +Memory: 549MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 38 +Time : 654.789s (Solving: 635.95s 1st Model: 0.00s Unsat: 4.20s) +CPU Time : 654.972s + +Choices : 8272236 (Domain: 8146669) +Conflicts : 943641 (Analyzed: 943638) +Restarts : 3361 (Average: 280.76 Last: 204) +Model-Level : 147.0 +Problems : 38 (Average Length: 60.82 Splits: 0) +Lemmas : 943638 (Deleted: 894728) + Binary : 17930 (Ratio: 1.90%) + Ternary : 3210 (Ratio: 0.34%) + Conflict : 943638 (Average Length: 889.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 943638 (Average: 7.92 Max: 493 Sum: 7469400) + Executed : 943587 (Average: 7.91 Max: 493 Sum: 7468220 Ratio: 99.98%) + Bounded : 51 (Average: 23.14 Max: 87 Sum: 1180 Ratio: 0.02%) + +Rules : 55133 (Original: 53913) +Atoms : 43853 +Bodies : 10280 (Original: 9059) + Count : 232 (Original: 476) +Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) +Tight : Yes +Variables : 419103 (Eliminated: 1464 Frozen: 410109) +Constraints : 3133777 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) + +Memory Peak : 607MB +Max. Length : 90 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 21.20s +Memory: 596MB (+47MB) +UNKNOWN +Iteration Time: 21.82s + +Iteration 38 +Queue: [(20,100,0,True), (21,105,0,True)] +Grounded Until: 95 +Expected Memory: 680.0MB +Grounding... [('step', [96]), ('step', [97]), ('step', [98]), ('step', [99]), ('step', [100]), ('check', [100])] +Grounding Time: 0.33s +Memory: 596MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 39 +Time : 678.370s (Solving: 658.52s 1st Model: 0.00s Unsat: 4.20s) +CPU Time : 678.564s + +Choices : 8579392 (Domain: 8453731) +Conflicts : 971840 (Analyzed: 971837) +Restarts : 3461 (Average: 280.80 Last: 204) +Model-Level : 147.0 +Problems : 39 (Average Length: 61.87 Splits: 0) +Lemmas : 971837 (Deleted: 922125) + Binary : 18257 (Ratio: 1.88%) + Ternary : 3262 (Ratio: 0.34%) + Conflict : 971837 (Average Length: 888.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 971837 (Average: 7.96 Max: 493 Sum: 7736535) + Executed : 971786 (Average: 7.96 Max: 493 Sum: 7735355 Ratio: 99.98%) + Bounded : 51 (Average: 23.14 Max: 87 Sum: 1180 Ratio: 0.02%) + +Rules : 55133 (Original: 53913) +Atoms : 43853 +Bodies : 10280 (Original: 9059) + Count : 232 (Original: 476) +Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) +Tight : Yes +Variables : 441679 (Eliminated: 1464 Frozen: 432685) +Constraints : 3306822 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) + +Memory Peak : 650MB +Max. Length : 95 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 22.97s +Memory: 612MB (+16MB) +UNKNOWN +Iteration Time: 23.60s + +Iteration 39 +Queue: [(21,105,0,True)] +Grounded Until: 100 +Expected Memory: 696.0MB +Grounding... [('step', [101]), ('step', [102]), ('step', [103]), ('step', [104]), ('step', [105]), ('check', [105])] +Grounding Time: 0.32s +Memory: 612MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 40 +Time : 700.801s (Solving: 679.93s 1st Model: 0.00s Unsat: 4.20s) +CPU Time : 701.004s + +Choices : 8853119 (Domain: 8727423) +Conflicts : 1000007 (Analyzed: 1000004) +Restarts : 3561 (Average: 280.82 Last: 204) +Model-Level : 147.0 +Problems : 40 (Average Length: 63.00 Splits: 0) +Lemmas : 1000004 (Deleted: 946111) + Binary : 18417 (Ratio: 1.84%) + Ternary : 3291 (Ratio: 0.33%) + Conflict : 1000004 (Average Length: 887.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 1000004 (Average: 7.97 Max: 493 Sum: 7973347) + Executed : 999953 (Average: 7.97 Max: 493 Sum: 7972167 Ratio: 99.99%) + Bounded : 51 (Average: 23.14 Max: 87 Sum: 1180 Ratio: 0.01%) + +Rules : 55133 (Original: 53913) +Atoms : 43853 +Bodies : 10280 (Original: 9059) + Count : 232 (Original: 476) +Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) +Tight : Yes +Variables : 464255 (Eliminated: 1464 Frozen: 455261) +Constraints : 3479867 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) + +Memory Peak : 669MB +Max. Length : 100 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 21.82s +Memory: 616MB (+4MB) +UNKNOWN +Iteration Time: 22.45s + +Iteration 40 +Queue: [(4,20,3,True), (5,25,3,True), (6,30,3,True), (7,35,2,True), (8,40,2,True), (9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,2,False), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Blocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 41 +Time : 713.054s (Solving: 692.05s 1st Model: 0.00s Unsat: 4.20s) +CPU Time : 713.264s + +Choices : 9003898 (Domain: 8878202) +Conflicts : 1028184 (Analyzed: 1028181) +Restarts : 3661 (Average: 280.85 Last: 204) +Model-Level : 147.0 +Problems : 41 (Average Length: 64.07 Splits: 0) +Lemmas : 1028181 (Deleted: 977173) + Binary : 18547 (Ratio: 1.80%) + Ternary : 3325 (Ratio: 0.32%) + Conflict : 1028181 (Average Length: 876.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 1028181 (Average: 7.89 Max: 493 Sum: 8117468) + Executed : 1028130 (Average: 7.89 Max: 493 Sum: 8116288 Ratio: 99.99%) + Bounded : 51 (Average: 23.14 Max: 87 Sum: 1180 Ratio: 0.01%) + +Rules : 55133 (Original: 53913) +Atoms : 43853 +Bodies : 10280 (Original: 9059) + Count : 232 (Original: 476) +Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) +Tight : Yes +Variables : 464255 (Eliminated: 1464 Frozen: 462791) +Constraints : 3479867 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) + +Memory Peak : 669MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 12.20s +Memory: 616MB (+0MB) +UNKNOWN +Iteration Time: 12.26s + +Iteration 41 +Queue: [(5,25,3,True), (6,30,3,True), (7,35,2,True), (8,40,2,True), (9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,2,False), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 42 +Time : 738.564s (Solving: 717.46s 1st Model: 0.00s Unsat: 4.20s) +CPU Time : 738.784s + +Choices : 9105606 (Domain: 8979910) +Conflicts : 1056370 (Analyzed: 1056367) +Restarts : 3761 (Average: 280.87 Last: 204) +Model-Level : 147.0 +Problems : 42 (Average Length: 65.10 Splits: 0) +Lemmas : 1056367 (Deleted: 1004871) + Binary : 18597 (Ratio: 1.76%) + Ternary : 3363 (Ratio: 0.32%) + Conflict : 1056367 (Average Length: 876.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 1056367 (Average: 7.77 Max: 493 Sum: 8209915) + Executed : 1056316 (Average: 7.77 Max: 493 Sum: 8208735 Ratio: 99.99%) + Bounded : 51 (Average: 23.14 Max: 87 Sum: 1180 Ratio: 0.01%) + +Rules : 55133 (Original: 53913) +Atoms : 43853 +Bodies : 10280 (Original: 9059) + Count : 232 (Original: 476) +Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) +Tight : Yes +Variables : 464255 (Eliminated: 1464 Frozen: 462791) +Constraints : 3479867 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) + +Memory Peak : 669MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 25.48s +Memory: 616MB (+0MB) +UNKNOWN +Iteration Time: 25.52s + +Iteration 42 +Queue: [(6,30,3,True), (7,35,2,True), (8,40,2,True), (9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,2,False), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 43 +Time : 764.452s (Solving: 743.24s 1st Model: 0.00s Unsat: 4.20s) +CPU Time : 764.680s + +Choices : 9282110 (Domain: 9156414) +Conflicts : 1084555 (Analyzed: 1084552) +Restarts : 3861 (Average: 280.90 Last: 204) +Model-Level : 147.0 +Problems : 43 (Average Length: 66.07 Splits: 0) +Lemmas : 1084552 (Deleted: 1032580) + Binary : 18721 (Ratio: 1.73%) + Ternary : 3384 (Ratio: 0.31%) + Conflict : 1084552 (Average Length: 891.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 1084552 (Average: 7.72 Max: 493 Sum: 8370316) + Executed : 1084501 (Average: 7.72 Max: 493 Sum: 8369136 Ratio: 99.99%) + Bounded : 51 (Average: 23.14 Max: 87 Sum: 1180 Ratio: 0.01%) + +Rules : 55133 (Original: 53913) +Atoms : 43853 +Bodies : 10280 (Original: 9059) + Count : 232 (Original: 476) +Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) +Tight : Yes +Variables : 464255 (Eliminated: 1464 Frozen: 462791) +Constraints : 3479867 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) + +Memory Peak : 744MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 25.86s +Memory: 680MB (+64MB) +UNKNOWN +Iteration Time: 25.90s + +Iteration 43 +Queue: [(7,35,2,True), (8,40,2,True), (9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,2,False), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 44 +Time : 784.115s (Solving: 762.79s 1st Model: 0.00s Unsat: 4.20s) +CPU Time : 784.352s + +Choices : 9451213 (Domain: 9325517) +Conflicts : 1112727 (Analyzed: 1112724) +Restarts : 3961 (Average: 280.92 Last: 204) +Model-Level : 147.0 +Problems : 44 (Average Length: 67.00 Splits: 0) +Lemmas : 1112724 (Deleted: 1060159) + Binary : 18869 (Ratio: 1.70%) + Ternary : 3425 (Ratio: 0.31%) + Conflict : 1112724 (Average Length: 894.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 1112724 (Average: 7.66 Max: 493 Sum: 8519634) + Executed : 1112673 (Average: 7.66 Max: 493 Sum: 8518454 Ratio: 99.99%) + Bounded : 51 (Average: 23.14 Max: 87 Sum: 1180 Ratio: 0.01%) + +Rules : 55133 (Original: 53913) +Atoms : 43853 +Bodies : 10280 (Original: 9059) + Count : 232 (Original: 476) +Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) +Tight : Yes +Variables : 464255 (Eliminated: 1464 Frozen: 462791) +Constraints : 3479867 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) + +Memory Peak : 744MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 19.63s +Memory: 680MB (+0MB) +UNKNOWN +Iteration Time: 19.67s + +Iteration 44 +Queue: [(8,40,2,True), (9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,2,False), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 45 +Time : 803.797s (Solving: 782.37s 1st Model: 0.00s Unsat: 4.20s) +CPU Time : 804.040s + +Choices : 9629811 (Domain: 9504115) +Conflicts : 1140953 (Analyzed: 1140950) +Restarts : 4061 (Average: 280.95 Last: 204) +Model-Level : 147.0 +Problems : 45 (Average Length: 67.89 Splits: 0) +Lemmas : 1140950 (Deleted: 1087827) + Binary : 19015 (Ratio: 1.67%) + Ternary : 3450 (Ratio: 0.30%) + Conflict : 1140950 (Average Length: 897.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 1140950 (Average: 7.60 Max: 493 Sum: 8675794) + Executed : 1140899 (Average: 7.60 Max: 493 Sum: 8674614 Ratio: 99.99%) + Bounded : 51 (Average: 23.14 Max: 87 Sum: 1180 Ratio: 0.01%) + +Rules : 55133 (Original: 53913) +Atoms : 43853 +Bodies : 10280 (Original: 9059) + Count : 232 (Original: 476) +Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) +Tight : Yes +Variables : 464255 (Eliminated: 1464 Frozen: 462791) +Constraints : 3479867 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) + +Memory Peak : 744MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 19.65s +Memory: 680MB (+0MB) +UNKNOWN +Iteration Time: 19.69s + +Iteration 45 +Queue: [(9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,2,False), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 46 +Time : 825.313s (Solving: 803.76s 1st Model: 0.00s Unsat: 4.20s) +CPU Time : 825.564s + +Choices : 9823417 (Domain: 9697580) +Conflicts : 1169150 (Analyzed: 1169147) +Restarts : 4161 (Average: 280.98 Last: 204) +Model-Level : 147.0 +Problems : 46 (Average Length: 68.74 Splits: 0) +Lemmas : 1169147 (Deleted: 1115335) + Binary : 19295 (Ratio: 1.65%) + Ternary : 3485 (Ratio: 0.30%) + Conflict : 1169147 (Average Length: 904.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 1169147 (Average: 7.56 Max: 493 Sum: 8842595) + Executed : 1169096 (Average: 7.56 Max: 493 Sum: 8841415 Ratio: 99.99%) + Bounded : 51 (Average: 23.14 Max: 87 Sum: 1180 Ratio: 0.01%) + +Rules : 55133 (Original: 53913) +Atoms : 43853 +Bodies : 10280 (Original: 9059) + Count : 232 (Original: 476) +Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) +Tight : Yes +Variables : 464255 (Eliminated: 1464 Frozen: 462791) +Constraints : 3479867 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) + +Memory Peak : 744MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 21.47s +Memory: 680MB (+0MB) +UNKNOWN +Iteration Time: 21.53s + +Iteration 46 +Queue: [(10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,2,False), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 47 +Time : 844.567s (Solving: 822.91s 1st Model: 0.00s Unsat: 4.20s) +CPU Time : 844.828s + +Choices : 10033085 (Domain: 9907237) +Conflicts : 1197341 (Analyzed: 1197338) +Restarts : 4261 (Average: 281.00 Last: 204) +Model-Level : 147.0 +Problems : 47 (Average Length: 69.55 Splits: 0) +Lemmas : 1197338 (Deleted: 1142902) + Binary : 19440 (Ratio: 1.62%) + Ternary : 3518 (Ratio: 0.29%) + Conflict : 1197338 (Average Length: 903.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 1197338 (Average: 7.54 Max: 493 Sum: 9026213) + Executed : 1197287 (Average: 7.54 Max: 493 Sum: 9025033 Ratio: 99.99%) + Bounded : 51 (Average: 23.14 Max: 87 Sum: 1180 Ratio: 0.01%) + +Rules : 55133 (Original: 53913) +Atoms : 43853 +Bodies : 10280 (Original: 9059) + Count : 232 (Original: 476) +Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) +Tight : Yes +Variables : 464255 (Eliminated: 1464 Frozen: 462791) +Constraints : 3479867 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) + +Memory Peak : 744MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 19.22s +Memory: 680MB (+0MB) +UNKNOWN +Iteration Time: 19.26s + +Iteration 47 +Queue: [(11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,2,False), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 48 +Time : 863.330s (Solving: 841.57s 1st Model: 0.00s Unsat: 4.20s) +CPU Time : 863.600s + +Choices : 10251284 (Domain: 10125432) +Conflicts : 1225502 (Analyzed: 1225499) +Restarts : 4361 (Average: 281.01 Last: 204) +Model-Level : 147.0 +Problems : 48 (Average Length: 70.33 Splits: 0) +Lemmas : 1225499 (Deleted: 1170396) + Binary : 19701 (Ratio: 1.61%) + Ternary : 3549 (Ratio: 0.29%) + Conflict : 1225499 (Average Length: 904.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 1225499 (Average: 7.52 Max: 493 Sum: 9214105) + Executed : 1225448 (Average: 7.52 Max: 493 Sum: 9212925 Ratio: 99.99%) + Bounded : 51 (Average: 23.14 Max: 87 Sum: 1180 Ratio: 0.01%) + +Rules : 55133 (Original: 53913) +Atoms : 43853 +Bodies : 10280 (Original: 9059) + Count : 232 (Original: 476) +Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) +Tight : Yes +Variables : 464255 (Eliminated: 1464 Frozen: 462791) +Constraints : 3479867 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) + +Memory Peak : 744MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 18.73s +Memory: 680MB (+0MB) +UNKNOWN +Iteration Time: 18.77s + +Iteration 48 +Queue: [(12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,2,False), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 49 +Time : 881.523s (Solving: 859.66s 1st Model: 0.00s Unsat: 4.20s) +CPU Time : 881.800s + +Choices : 10489316 (Domain: 10363047) +Conflicts : 1253686 (Analyzed: 1253683) +Restarts : 4461 (Average: 281.03 Last: 204) +Model-Level : 147.0 +Problems : 49 (Average Length: 71.08 Splits: 0) +Lemmas : 1253683 (Deleted: 1197683) + Binary : 19958 (Ratio: 1.59%) + Ternary : 3584 (Ratio: 0.29%) + Conflict : 1253683 (Average Length: 903.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 1253683 (Average: 7.51 Max: 493 Sum: 9421101) + Executed : 1253631 (Average: 7.51 Max: 493 Sum: 9419814 Ratio: 99.99%) + Bounded : 52 (Average: 24.75 Max: 107 Sum: 1287 Ratio: 0.01%) + +Rules : 55133 (Original: 53913) +Atoms : 43853 +Bodies : 10280 (Original: 9059) + Count : 232 (Original: 476) +Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) +Tight : Yes +Variables : 464255 (Eliminated: 1464 Frozen: 462791) +Constraints : 3479867 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) + +Memory Peak : 744MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 18.16s +Memory: 680MB (+0MB) +UNKNOWN +Iteration Time: 18.20s + +Iteration 49 +Queue: [(13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,2,False), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +*** Info : (planner): INTERRUPTED by signal! +UNKNOWN + +INTERRUPTED : 1 + +Models : 0+ +Calls : 50 +Time : 900.347s (Solving: 878.37s 1st Model: 0.00s Unsat: 4.20s) +CPU Time : 900.616s + +Choices : 10729648 (Domain: 10602630) +Conflicts : 1281834 (Analyzed: 1281831) +Restarts : 4561 (Average: 281.04 Last: 204) +Model-Level : 147.0 +Problems : 50 (Average Length: 71.80 Splits: 0) +Lemmas : 1281831 (Deleted: 1225188) + Binary : 20176 (Ratio: 1.57%) + Ternary : 3624 (Ratio: 0.28%) + Conflict : 1281831 (Average Length: 903.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 1281831 (Average: 7.51 Max: 493 Sum: 9629023) + Executed : 1281779 (Average: 7.51 Max: 493 Sum: 9627736 Ratio: 99.99%) + Bounded : 52 (Average: 24.75 Max: 107 Sum: 1287 Ratio: 0.01%) + +Rules : 55133 (Original: 53913) +Atoms : 43853 +Bodies : 10280 (Original: 9059) + Count : 232 (Original: 476) +Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872) +Tight : Yes +Variables : 464255 (Eliminated: 1464 Frozen: 462791) +Constraints : 3479853 (Binary: 91.6% Ternary: 6.5% Other: 1.9%) + +Memory Peak : 744MB +Max. Length : 105 steps +Models : 1 + +