diff --git a/gc-ta1-tt1/ipc-2011_barman-sequential-satisficing_17.env b/gc-ta1-tt1/ipc-2011_barman-sequential-satisficing_17.env new file mode 100644 index 000000000..75e057ff6 --- /dev/null +++ b/gc-ta1-tt1/ipc-2011_barman-sequential-satisficing_17.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-17.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: 17 + 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_17.err b/gc-ta1-tt1/ipc-2011_barman-sequential-satisficing_17.err new file mode 100644 index 000000000..e854be20b --- /dev/null +++ b/gc-ta1-tt1/ipc-2011_barman-sequential-satisficing_17.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': 17} +# 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-17.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.07 MEM 1057924 MAXMEM 1160448 STALE 0 MAXMEM_RSS 982708 + + diff --git a/gc-ta1-tt1/ipc-2011_barman-sequential-satisficing_17.out b/gc-ta1-tt1/ipc-2011_barman-sequential-satisficing_17.out new file mode 100644 index 000000000..e1f2890c2 --- /dev/null +++ b/gc-ta1-tt1/ipc-2011_barman-sequential-satisficing_17.out @@ -0,0 +1,4940 @@ +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-17.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-17.pddl +Parsing... +Parsing: [0.040s CPU, 0.036s wall-clock] +Normalizing task... [0.000s CPU, 0.003s wall-clock] +Instantiating... +Generating Datalog program... [0.010s CPU, 0.010s wall-clock] +Normalizing Datalog program... +Normalizing Datalog program: [0.040s CPU, 0.045s wall-clock] +Preparing model... [0.030s CPU, 0.026s wall-clock] +Generated 115 rules. +Computing model... [0.530s CPU, 0.536s wall-clock] +3296 relevant atoms +3425 auxiliary atoms +6721 final queue length +11595 total queue pushes +Completing instantiation... [1.030s CPU, 1.028s wall-clock] +Instantiating: [1.650s CPU, 1.652s wall-clock] +Computing fact groups... +Finding invariants... +24 initial candidates +Finding invariants: [0.140s CPU, 0.142s wall-clock] +Checking invariant weight... [0.000s CPU, 0.001s wall-clock] +Instantiating groups... [0.010s CPU, 0.010s wall-clock] +Collecting mutex groups... [0.000s CPU, 0.001s wall-clock] +Choosing groups... +350 uncovered facts +Choosing groups: [0.000s CPU, 0.002s wall-clock] +Building translation key... [0.010s CPU, 0.013s wall-clock] +Computing fact groups: [0.190s CPU, 0.195s wall-clock] +Building STRIPS to SAS dictionary... [0.010s CPU, 0.006s wall-clock] +Building dictionary for full mutex groups... [0.000s CPU, 0.003s wall-clock] +Building mutex information... +Building mutex information: [0.010s CPU, 0.004s wall-clock] +Translating task... +Processing axioms... +Simplifying axioms... [0.000s CPU, 0.000s wall-clock] +Processing axioms: [0.050s CPU, 0.057s wall-clock] +Translating task: [1.060s CPU, 1.067s wall-clock] +3920 effect conditions simplified +0 implied preconditions added +Detecting unreachable propositions... +0 operators removed +0 axioms removed +3 propositions removed +Detecting unreachable propositions: [0.590s CPU, 0.587s wall-clock] +Reordering and filtering variables... +353 of 353 variables necessary. +16 of 19 mutex groups necessary. +2344 of 2344 operators necessary. +0 of 0 axiom rules necessary. +Reordering and filtering variables: [0.380s CPU, 0.378s wall-clock] +Translator variables: 353 +Translator derived variables: 0 +Translator facts: 737 +Translator goal facts: 14 +Translator mutex groups: 16 +Translator total mutex groups size: 48 +Translator operators: 2344 +Translator axioms: 0 +Translator task size: 22454 +Translator peak memory: 49100 KB +Writing output... [0.380s CPU, 0.411s wall-clock] +Done! [4.350s CPU, 4.383s wall-clock] +planner.py version 0.0.1 + +Time: 0.91s +Memory: 111MB + +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 : 1.068s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s) +CPU Time : 0.908s + +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 : 64767 +Atoms : 64767 +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 : 247MB +Max. Length : 0 steps +Models : 0 + +[endof: stats after solve call] +Solving Time: 0.01s +Memory: 183MB (+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: 183MB +Grounding... [('step', [1]), ('step', [2]), ('step', [3]), ('step', [4]), ('step', [5]), ('check', [5])] +Grounding Time: 0.27s +Memory: 183MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0 +Calls : 2 +Time : 1.501s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s) +CPU Time : 1.340s + +Choices : 171 (Domain: 108) +Conflicts : 40 (Analyzed: 39) +Restarts : 0 +Problems : 2 (Average Length: 4.50 Splits: 0) +Lemmas : 39 (Deleted: 0) + Binary : 11 (Ratio: 28.21%) + Ternary : 4 (Ratio: 10.26%) + Conflict : 39 (Average Length: 4.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 39 (Average: 4.41 Max: 28 Sum: 172) + Executed : 38 (Average: 4.38 Max: 28 Sum: 171 Ratio: 99.42%) + Bounded : 1 (Average: 1.00 Max: 1 Sum: 1 Ratio: 0.58%) + +Rules : 64767 +Atoms : 64767 +Bodies : 1 (Original: 0) +Tight : Yes +Variables : 17354 (Eliminated: 0 Frozen: 170) +Constraints : 57355 (Binary: 95.3% Ternary: 3.3% Other: 1.4%) + +Memory Peak : 247MB +Max. Length : 0 steps +Models : 0 + +[endof: stats after solve call] +Solving Time: 0.02s +Memory: 187MB (+4MB) +UNSAT +Iteration Time: 0.44s + +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: 191.0MB +Grounding... [('step', [6]), ('step', [7]), ('step', [8]), ('step', [9]), ('step', [10]), ('check', [10])] +Grounding Time: 0.34s +Memory: 195MB (+8MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 1+ +Calls : 3 +Time : 2.018s (Solving: 0.02s 1st Model: 0.01s Unsat: 0.00s) +CPU Time : 1.856s + +Choices : 1028 (Domain: 926) +Conflicts : 96 (Analyzed: 95) +Restarts : 0 +Model-Level : 254.0 +Problems : 3 (Average Length: 7.00 Splits: 0) +Lemmas : 95 (Deleted: 0) + Binary : 38 (Ratio: 40.00%) + Ternary : 6 (Ratio: 6.32%) + Conflict : 95 (Average Length: 59.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 95 (Average: 8.28 Max: 144 Sum: 787) + Executed : 94 (Average: 8.27 Max: 144 Sum: 786 Ratio: 99.87%) + Bounded : 1 (Average: 1.00 Max: 1 Sum: 1 Ratio: 0.13%) + +Rules : 64767 +Atoms : 64767 +Bodies : 1 (Original: 0) +Tight : Yes +Variables : 38040 (Eliminated: 0 Frozen: 340) +Constraints : 226475 (Binary: 95.6% Ternary: 3.2% Other: 1.2%) + +Memory Peak : 247MB +Max. Length : 5 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 0.04s +Memory: 205MB (+10MB) +SAT +Testing... +NOT SERIALIZABLE +Testing Time: 1.16s +Memory: 241MB (+36MB) +Solving... +[start: stats after solve call] + +Models : 0 +Calls : 4 +Time : 3.305s (Solving: 0.95s 1st Model: 0.01s Unsat: 0.93s) +CPU Time : 3.140s + +Choices : 30026 (Domain: 23080) +Conflicts : 3147 (Analyzed: 3145) +Restarts : 33 (Average: 95.30 Last: 56) +Model-Level : 254.0 +Problems : 4 (Average Length: 8.25 Splits: 0) +Lemmas : 3145 (Deleted: 858) + Binary : 260 (Ratio: 8.27%) + Ternary : 82 (Ratio: 2.61%) + Conflict : 3145 (Average Length: 103.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 3145 (Average: 9.32 Max: 196 Sum: 29297) + Executed : 3134 (Average: 9.28 Max: 196 Sum: 29198 Ratio: 99.66%) + Bounded : 11 (Average: 9.00 Max: 12 Sum: 99 Ratio: 0.34%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 60107 (Eliminated: 0 Frozen: 16894) +Constraints : 371085 (Binary: 91.4% Ternary: 7.0% Other: 1.6%) + +Memory Peak : 247MB +Max. Length : 5 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 1.02s +Memory: 240MB (+-1MB) +UNSAT +Iteration Time: 2.70s + +Iteration 4 +Queue: [(3,15,0,True), (4,20,0,True), (5,25,0,True), (6,30,0,True)] +Grounded Until: 10 +Expected Memory: 258.0MB +Grounding... [('step', [11]), ('step', [12]), ('step', [13]), ('step', [14]), ('step', [15]), ('check', [15])] +Grounding Time: 0.52s +Memory: 241MB (+1MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 5 +Time : 8.640s (Solving: 5.52s 1st Model: 0.01s Unsat: 0.93s) +CPU Time : 8.480s + +Choices : 120633 (Domain: 94496) +Conflicts : 11866 (Analyzed: 11864) +Restarts : 133 (Average: 89.20 Last: 113) +Model-Level : 254.0 +Problems : 5 (Average Length: 10.00 Splits: 0) +Lemmas : 11864 (Deleted: 8150) + Binary : 939 (Ratio: 7.91%) + Ternary : 300 (Ratio: 2.53%) + Conflict : 11864 (Average Length: 192.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 11864 (Average: 9.80 Max: 199 Sum: 116208) + Executed : 11841 (Average: 9.77 Max: 199 Sum: 115915 Ratio: 99.75%) + Bounded : 23 (Average: 12.74 Max: 17 Sum: 293 Ratio: 0.25%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 100183 (Eliminated: 0 Frozen: 29344) +Constraints : 661845 (Binary: 91.3% Ternary: 6.9% Other: 1.7%) + +Memory Peak : 266MB +Max. Length : 10 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 4.60s +Memory: 266MB (+25MB) +UNKNOWN +Iteration Time: 5.35s + +Iteration 5 +Queue: [(4,20,0,True), (5,25,0,True), (6,30,0,True)] +Grounded Until: 15 +Expected Memory: 292.0MB +Grounding... [('step', [16]), ('step', [17]), ('step', [18]), ('step', [19]), ('step', [20]), ('check', [20])] +Grounding Time: 0.62s +Memory: 279MB (+13MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 6 +Time : 15.324s (Solving: 11.29s 1st Model: 0.01s Unsat: 0.93s) +CPU Time : 15.168s + +Choices : 228016 (Domain: 186850) +Conflicts : 20689 (Analyzed: 20687) +Restarts : 233 (Average: 88.79 Last: 113) +Model-Level : 254.0 +Problems : 6 (Average Length: 12.00 Splits: 0) +Lemmas : 20687 (Deleted: 15856) + Binary : 1617 (Ratio: 7.82%) + Ternary : 415 (Ratio: 2.01%) + Conflict : 20687 (Average Length: 495.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 20687 (Average: 10.52 Max: 199 Sum: 217670) + Executed : 20664 (Average: 10.51 Max: 199 Sum: 217377 Ratio: 99.87%) + Bounded : 23 (Average: 12.74 Max: 17 Sum: 293 Ratio: 0.13%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 140259 (Eliminated: 0 Frozen: 41794) +Constraints : 958119 (Binary: 91.3% Ternary: 6.9% Other: 1.7%) + +Memory Peak : 297MB +Max. Length : 15 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 5.83s +Memory: 293MB (+14MB) +UNKNOWN +Iteration Time: 6.70s + +Iteration 6 +Queue: [(5,25,0,True), (6,30,0,True)] +Grounded Until: 20 +Expected Memory: 320.0MB +Grounding... [('step', [21]), ('step', [22]), ('step', [23]), ('step', [24]), ('step', [25]), ('check', [25])] +Grounding Time: 0.59s +Memory: 307MB (+14MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 7 +Time : 23.100s (Solving: 18.16s 1st Model: 0.01s Unsat: 0.93s) +CPU Time : 22.948s + +Choices : 340659 (Domain: 289099) +Conflicts : 29741 (Analyzed: 29739) +Restarts : 333 (Average: 89.31 Last: 113) +Model-Level : 254.0 +Problems : 7 (Average Length: 14.14 Splits: 0) +Lemmas : 29739 (Deleted: 24092) + Binary : 1976 (Ratio: 6.64%) + Ternary : 449 (Ratio: 1.51%) + Conflict : 29739 (Average Length: 822.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 29739 (Average: 10.82 Max: 248 Sum: 321843) + Executed : 29716 (Average: 10.81 Max: 248 Sum: 321550 Ratio: 99.91%) + Bounded : 23 (Average: 12.74 Max: 17 Sum: 293 Ratio: 0.09%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 180335 (Eliminated: 0 Frozen: 54244) +Constraints : 1260099 (Binary: 91.3% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 334MB +Max. Length : 20 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.92s +Memory: 321MB (+14MB) +UNKNOWN +Iteration Time: 7.79s + +Iteration 7 +Queue: [(6,30,0,True)] +Grounded Until: 25 +Expected Memory: 349.0MB +Grounding... [('step', [26]), ('step', [27]), ('step', [28]), ('step', [29]), ('step', [30]), ('check', [30])] +Grounding Time: 0.56s +Memory: 333MB (+12MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 8 +Time : 30.707s (Solving: 24.87s 1st Model: 0.01s Unsat: 0.93s) +CPU Time : 30.556s + +Choices : 460469 (Domain: 402838) +Conflicts : 37831 (Analyzed: 37829) +Restarts : 433 (Average: 87.36 Last: 113) +Model-Level : 254.0 +Problems : 8 (Average Length: 16.38 Splits: 0) +Lemmas : 37829 (Deleted: 30595) + Binary : 2189 (Ratio: 5.79%) + Ternary : 466 (Ratio: 1.23%) + Conflict : 37829 (Average Length: 1056.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 37829 (Average: 11.38 Max: 262 Sum: 430377) + Executed : 37806 (Average: 11.37 Max: 262 Sum: 430084 Ratio: 99.93%) + Bounded : 23 (Average: 12.74 Max: 17 Sum: 293 Ratio: 0.07%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 220411 (Eliminated: 0 Frozen: 66694) +Constraints : 1562079 (Binary: 91.3% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 367MB +Max. Length : 25 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.77s +Memory: 367MB (+34MB) +UNKNOWN +Iteration Time: 7.62s + +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 : 36.604s (Solving: 30.70s 1st Model: 0.01s Unsat: 0.93s) +CPU Time : 36.456s + +Choices : 545520 (Domain: 482044) +Conflicts : 46602 (Analyzed: 46600) +Restarts : 533 (Average: 87.43 Last: 113) +Model-Level : 254.0 +Problems : 9 (Average Length: 18.11 Splits: 0) +Lemmas : 46600 (Deleted: 40009) + Binary : 2669 (Ratio: 5.73%) + Ternary : 563 (Ratio: 1.21%) + Conflict : 46600 (Average Length: 916.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 46600 (Average: 10.93 Max: 269 Sum: 509528) + Executed : 46563 (Average: 10.92 Max: 269 Sum: 508787 Ratio: 99.85%) + Bounded : 37 (Average: 20.03 Max: 32 Sum: 741 Ratio: 0.15%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 220411 (Eliminated: 0 Frozen: 66694) +Constraints : 1562079 (Binary: 91.3% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 367MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 5.88s +Memory: 367MB (+0MB) +UNKNOWN +Iteration Time: 5.90s + +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 : 42.786s (Solving: 36.83s 1st Model: 0.01s Unsat: 0.93s) +CPU Time : 42.640s + +Choices : 685916 (Domain: 614218) +Conflicts : 55643 (Analyzed: 55641) +Restarts : 633 (Average: 87.90 Last: 113) +Model-Level : 254.0 +Problems : 10 (Average Length: 19.50 Splits: 0) +Lemmas : 55641 (Deleted: 47014) + Binary : 3310 (Ratio: 5.95%) + Ternary : 679 (Ratio: 1.22%) + Conflict : 55641 (Average Length: 796.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 55641 (Average: 11.59 Max: 282 Sum: 644675) + Executed : 55592 (Average: 11.57 Max: 282 Sum: 643550 Ratio: 99.83%) + Bounded : 49 (Average: 22.96 Max: 32 Sum: 1125 Ratio: 0.17%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 220411 (Eliminated: 0 Frozen: 66694) +Constraints : 1539434 (Binary: 91.3% Ternary: 6.9% Other: 1.8%) + +Memory Peak : 367MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.17s +Memory: 367MB (+0MB) +UNKNOWN +Iteration Time: 6.19s + +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 : 48.750s (Solving: 42.75s 1st Model: 0.01s Unsat: 0.93s) +CPU Time : 48.604s + +Choices : 829159 (Domain: 750755) +Conflicts : 64375 (Analyzed: 64373) +Restarts : 733 (Average: 87.82 Last: 116) +Model-Level : 254.0 +Problems : 11 (Average Length: 20.64 Splits: 0) +Lemmas : 64373 (Deleted: 54670) + Binary : 3548 (Ratio: 5.51%) + Ternary : 777 (Ratio: 1.21%) + Conflict : 64373 (Average Length: 715.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 64373 (Average: 12.15 Max: 307 Sum: 782285) + Executed : 64313 (Average: 12.13 Max: 307 Sum: 780838 Ratio: 99.82%) + Bounded : 60 (Average: 24.12 Max: 32 Sum: 1447 Ratio: 0.18%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 220411 (Eliminated: 0 Frozen: 66694) +Constraints : 1517106 (Binary: 91.3% Ternary: 6.9% Other: 1.8%) + +Memory Peak : 367MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 5.95s +Memory: 367MB (+0MB) +UNKNOWN +Iteration Time: 5.97s + +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 : 54.222s (Solving: 48.16s 1st Model: 0.01s Unsat: 0.93s) +CPU Time : 54.076s + +Choices : 990974 (Domain: 903422) +Conflicts : 73229 (Analyzed: 73227) +Restarts : 833 (Average: 87.91 Last: 150) +Model-Level : 254.0 +Problems : 12 (Average Length: 21.58 Splits: 0) +Lemmas : 73227 (Deleted: 62428) + Binary : 3764 (Ratio: 5.14%) + Ternary : 847 (Ratio: 1.16%) + Conflict : 73227 (Average Length: 648.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 73227 (Average: 12.77 Max: 404 Sum: 934765) + Executed : 73160 (Average: 12.74 Max: 404 Sum: 933099 Ratio: 99.82%) + Bounded : 67 (Average: 24.87 Max: 32 Sum: 1666 Ratio: 0.18%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 220411 (Eliminated: 0 Frozen: 66694) +Constraints : 1506186 (Binary: 91.3% Ternary: 6.9% Other: 1.8%) + +Memory Peak : 367MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 5.45s +Memory: 367MB (+0MB) +UNKNOWN +Iteration Time: 5.48s + +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: 413.0MB +Grounding... [('step', [31]), ('step', [32]), ('step', [33]), ('step', [34]), ('step', [35]), ('check', [35])] +Grounding Time: 0.59s +Memory: 367MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 13 +Time : 61.201s (Solving: 54.18s 1st Model: 0.01s Unsat: 0.93s) +CPU Time : 61.060s + +Choices : 1215033 (Domain: 1122075) +Conflicts : 82083 (Analyzed: 82081) +Restarts : 933 (Average: 87.98 Last: 150) +Model-Level : 254.0 +Problems : 13 (Average Length: 22.77 Splits: 0) +Lemmas : 82081 (Deleted: 72810) + Binary : 4020 (Ratio: 4.90%) + Ternary : 860 (Ratio: 1.05%) + Conflict : 82081 (Average Length: 661.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 82081 (Average: 13.97 Max: 404 Sum: 1146403) + Executed : 82014 (Average: 13.95 Max: 404 Sum: 1144737 Ratio: 99.85%) + Bounded : 67 (Average: 24.87 Max: 32 Sum: 1666 Ratio: 0.15%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 260487 (Eliminated: 0 Frozen: 79144) +Constraints : 1804964 (Binary: 91.3% Ternary: 6.9% Other: 1.8%) + +Memory Peak : 403MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.09s +Memory: 380MB (+13MB) +UNKNOWN +Iteration Time: 6.99s + +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: 426.0MB +Grounding... [('step', [36]), ('step', [37]), ('step', [38]), ('step', [39]), ('step', [40]), ('check', [40])] +Grounding Time: 0.57s +Memory: 392MB (+12MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 14 +Time : 68.153s (Solving: 60.19s 1st Model: 0.01s Unsat: 0.93s) +CPU Time : 68.016s + +Choices : 1422851 (Domain: 1322434) +Conflicts : 90673 (Analyzed: 90671) +Restarts : 1033 (Average: 87.77 Last: 150) +Model-Level : 254.0 +Problems : 14 (Average Length: 24.14 Splits: 0) +Lemmas : 90671 (Deleted: 79068) + Binary : 4254 (Ratio: 4.69%) + Ternary : 864 (Ratio: 0.95%) + Conflict : 90671 (Average Length: 677.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 90671 (Average: 14.74 Max: 440 Sum: 1336710) + Executed : 90604 (Average: 14.72 Max: 440 Sum: 1335044 Ratio: 99.88%) + Bounded : 67 (Average: 24.87 Max: 32 Sum: 1666 Ratio: 0.12%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 300563 (Eliminated: 0 Frozen: 91594) +Constraints : 2106944 (Binary: 91.3% Ternary: 6.9% Other: 1.8%) + +Memory Peak : 435MB +Max. Length : 35 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.08s +Memory: 406MB (+14MB) +UNKNOWN +Iteration Time: 6.97s + +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: 452.0MB +Grounding... [('step', [41]), ('step', [42]), ('step', [43]), ('step', [44]), ('step', [45]), ('check', [45])] +Grounding Time: 0.75s +Memory: 430MB (+24MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 15 +Time : 75.878s (Solving: 66.74s 1st Model: 0.01s Unsat: 0.93s) +CPU Time : 75.744s + +Choices : 1592918 (Domain: 1489489) +Conflicts : 99212 (Analyzed: 99210) +Restarts : 1133 (Average: 87.56 Last: 150) +Model-Level : 254.0 +Problems : 15 (Average Length: 25.67 Splits: 0) +Lemmas : 99210 (Deleted: 87296) + Binary : 4358 (Ratio: 4.39%) + Ternary : 869 (Ratio: 0.88%) + Conflict : 99210 (Average Length: 724.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 99210 (Average: 14.98 Max: 440 Sum: 1486626) + Executed : 99143 (Average: 14.97 Max: 440 Sum: 1484960 Ratio: 99.89%) + Bounded : 67 (Average: 24.87 Max: 32 Sum: 1666 Ratio: 0.11%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 340639 (Eliminated: 0 Frozen: 104044) +Constraints : 2408924 (Binary: 91.3% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 480MB +Max. Length : 40 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.64s +Memory: 478MB (+48MB) +UNKNOWN +Iteration Time: 7.74s + +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: 550.0MB +Grounding... [('step', [46]), ('step', [47]), ('step', [48]), ('step', [49]), ('step', [50]), ('check', [50])] +Grounding Time: 0.56s +Memory: 478MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 16 +Time : 83.761s (Solving: 73.63s 1st Model: 0.01s Unsat: 0.93s) +CPU Time : 83.632s + +Choices : 1779320 (Domain: 1670641) +Conflicts : 107288 (Analyzed: 107286) +Restarts : 1233 (Average: 87.01 Last: 150) +Model-Level : 254.0 +Problems : 16 (Average Length: 27.31 Splits: 0) +Lemmas : 107286 (Deleted: 95633) + Binary : 4449 (Ratio: 4.15%) + Ternary : 876 (Ratio: 0.82%) + Conflict : 107286 (Average Length: 756.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 107286 (Average: 15.37 Max: 482 Sum: 1649238) + Executed : 107219 (Average: 15.36 Max: 482 Sum: 1647572 Ratio: 99.90%) + Bounded : 67 (Average: 24.87 Max: 32 Sum: 1666 Ratio: 0.10%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 380715 (Eliminated: 0 Frozen: 116494) +Constraints : 2710904 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 525MB +Max. Length : 45 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.97s +Memory: 488MB (+10MB) +UNKNOWN +Iteration Time: 7.90s + +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: 560.0MB +Grounding... [('step', [51]), ('step', [52]), ('step', [53]), ('step', [54]), ('step', [55]), ('check', [55])] +Grounding Time: 0.55s +Memory: 492MB (+4MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 17 +Time : 91.812s (Solving: 80.69s 1st Model: 0.01s Unsat: 0.93s) +CPU Time : 91.684s + +Choices : 2037604 (Domain: 1924173) +Conflicts : 115480 (Analyzed: 115478) +Restarts : 1333 (Average: 86.63 Last: 150) +Model-Level : 254.0 +Problems : 17 (Average Length: 29.06 Splits: 0) +Lemmas : 115478 (Deleted: 103546) + Binary : 4612 (Ratio: 3.99%) + Ternary : 877 (Ratio: 0.76%) + Conflict : 115478 (Average Length: 784.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 115478 (Average: 16.32 Max: 537 Sum: 1884467) + Executed : 115411 (Average: 16.30 Max: 537 Sum: 1882801 Ratio: 99.91%) + Bounded : 67 (Average: 24.87 Max: 32 Sum: 1666 Ratio: 0.09%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 420791 (Eliminated: 0 Frozen: 128944) +Constraints : 3012884 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 551MB +Max. Length : 50 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.15s +Memory: 512MB (+20MB) +UNKNOWN +Iteration Time: 8.06s + +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: 584.0MB +Grounding... [('step', [56]), ('step', [57]), ('step', [58]), ('step', [59]), ('step', [60]), ('check', [60])] +Grounding Time: 0.56s +Memory: 517MB (+5MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 18 +Time : 100.293s (Solving: 88.13s 1st Model: 0.01s Unsat: 0.93s) +CPU Time : 100.168s + +Choices : 2275221 (Domain: 2158172) +Conflicts : 123546 (Analyzed: 123544) +Restarts : 1433 (Average: 86.21 Last: 150) +Model-Level : 254.0 +Problems : 18 (Average Length: 30.89 Splits: 0) +Lemmas : 123544 (Deleted: 111469) + Binary : 4654 (Ratio: 3.77%) + Ternary : 878 (Ratio: 0.71%) + Conflict : 123544 (Average Length: 800.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 123544 (Average: 16.97 Max: 606 Sum: 2096708) + Executed : 123477 (Average: 16.96 Max: 606 Sum: 2095042 Ratio: 99.92%) + Bounded : 67 (Average: 24.87 Max: 32 Sum: 1666 Ratio: 0.08%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 460867 (Eliminated: 0 Frozen: 141394) +Constraints : 3314864 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 589MB +Max. Length : 55 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.54s +Memory: 589MB (+72MB) +UNKNOWN +Iteration Time: 8.50s + +Iteration 18 +Queue: [(13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True)] +Grounded Until: 60 +Expected Memory: 666.0MB +Grounding... [('step', [61]), ('step', [62]), ('step', [63]), ('step', [64]), ('step', [65]), ('check', [65])] +Grounding Time: 0.56s +Memory: 589MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 19 +Time : 108.491s (Solving: 95.28s 1st Model: 0.01s Unsat: 0.93s) +CPU Time : 108.368s + +Choices : 2547612 (Domain: 2426157) +Conflicts : 131557 (Analyzed: 131555) +Restarts : 1533 (Average: 85.82 Last: 150) +Model-Level : 254.0 +Problems : 19 (Average Length: 32.79 Splits: 0) +Lemmas : 131555 (Deleted: 119386) + Binary : 4699 (Ratio: 3.57%) + Ternary : 879 (Ratio: 0.67%) + Conflict : 131555 (Average Length: 813.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 131555 (Average: 17.80 Max: 638 Sum: 2341876) + Executed : 131488 (Average: 17.79 Max: 638 Sum: 2340210 Ratio: 99.93%) + Bounded : 67 (Average: 24.87 Max: 32 Sum: 1666 Ratio: 0.07%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 500943 (Eliminated: 0 Frozen: 153844) +Constraints : 3616844 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 650MB +Max. Length : 60 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.26s +Memory: 594MB (+5MB) +UNKNOWN +Iteration Time: 8.21s + +Iteration 19 +Queue: [(14,70,0,True), (15,75,0,True), (16,80,0,True)] +Grounded Until: 65 +Expected Memory: 671.0MB +Grounding... [('step', [66]), ('step', [67]), ('step', [68]), ('step', [69]), ('step', [70]), ('check', [70])] +Grounding Time: 0.56s +Memory: 594MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 20 +Time : 117.209s (Solving: 102.92s 1st Model: 0.01s Unsat: 0.93s) +CPU Time : 117.092s + +Choices : 2844978 (Domain: 2719694) +Conflicts : 139082 (Analyzed: 139080) +Restarts : 1633 (Average: 85.17 Last: 150) +Model-Level : 254.0 +Problems : 20 (Average Length: 34.75 Splits: 0) +Lemmas : 139080 (Deleted: 127229) + Binary : 4733 (Ratio: 3.40%) + Ternary : 880 (Ratio: 0.63%) + Conflict : 139080 (Average Length: 829.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 139080 (Average: 18.78 Max: 708 Sum: 2612039) + Executed : 139013 (Average: 18.77 Max: 708 Sum: 2610373 Ratio: 99.94%) + Bounded : 67 (Average: 24.87 Max: 32 Sum: 1666 Ratio: 0.06%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 541019 (Eliminated: 0 Frozen: 166294) +Constraints : 3918824 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 664MB +Max. Length : 65 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.75s +Memory: 610MB (+16MB) +UNKNOWN +Iteration Time: 8.73s + +Iteration 20 +Queue: [(15,75,0,True), (16,80,0,True)] +Grounded Until: 70 +Expected Memory: 687.0MB +Grounding... [('step', [71]), ('step', [72]), ('step', [73]), ('step', [74]), ('step', [75]), ('check', [75])] +Grounding Time: 0.56s +Memory: 615MB (+5MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 21 +Time : 126.455s (Solving: 111.07s 1st Model: 0.01s Unsat: 0.93s) +CPU Time : 126.344s + +Choices : 3156384 (Domain: 3026249) +Conflicts : 146866 (Analyzed: 146864) +Restarts : 1733 (Average: 84.75 Last: 150) +Model-Level : 254.0 +Problems : 21 (Average Length: 36.76 Splits: 0) +Lemmas : 146864 (Deleted: 134594) + Binary : 4775 (Ratio: 3.25%) + Ternary : 881 (Ratio: 0.60%) + Conflict : 146864 (Average Length: 841.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 146864 (Average: 19.71 Max: 746 Sum: 2894403) + Executed : 146797 (Average: 19.70 Max: 746 Sum: 2892737 Ratio: 99.94%) + Bounded : 67 (Average: 24.87 Max: 32 Sum: 1666 Ratio: 0.06%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 581095 (Eliminated: 0 Frozen: 178744) +Constraints : 4220804 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 698MB +Max. Length : 70 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.27s +Memory: 642MB (+27MB) +UNKNOWN +Iteration Time: 9.26s + +Iteration 21 +Queue: [(16,80,0,True)] +Grounded Until: 75 +Expected Memory: 719.0MB +Grounding... [('step', [76]), ('step', [77]), ('step', [78]), ('step', [79]), ('step', [80]), ('check', [80])] +Grounding Time: 0.58s +Memory: 642MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 22 +Time : 136.032s (Solving: 119.51s 1st Model: 0.01s Unsat: 0.93s) +CPU Time : 135.924s + +Choices : 3453062 (Domain: 3319382) +Conflicts : 155063 (Analyzed: 155061) +Restarts : 1833 (Average: 84.59 Last: 150) +Model-Level : 254.0 +Problems : 22 (Average Length: 38.82 Splits: 0) +Lemmas : 155061 (Deleted: 142241) + Binary : 4804 (Ratio: 3.10%) + Ternary : 882 (Ratio: 0.57%) + Conflict : 155061 (Average Length: 857.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 155061 (Average: 20.36 Max: 818 Sum: 3157695) + Executed : 154994 (Average: 20.35 Max: 818 Sum: 3156029 Ratio: 99.95%) + Bounded : 67 (Average: 24.87 Max: 32 Sum: 1666 Ratio: 0.05%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 621171 (Eliminated: 0 Frozen: 191194) +Constraints : 4522784 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 726MB +Max. Length : 75 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.56s +Memory: 667MB (+25MB) +UNKNOWN +Iteration Time: 9.59s + +Iteration 22 +Queue: [(3,15,2,True), (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)] +Grounded Until: 80 +Blocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 23 +Time : 141.721s (Solving: 125.05s 1st Model: 0.01s Unsat: 0.93s) +CPU Time : 141.616s + +Choices : 3517322 (Domain: 3372595) +Conflicts : 163853 (Analyzed: 163851) +Restarts : 1933 (Average: 84.77 Last: 150) +Model-Level : 254.0 +Problems : 23 (Average Length: 40.70 Splits: 0) +Lemmas : 163851 (Deleted: 149929) + Binary : 5047 (Ratio: 3.08%) + Ternary : 960 (Ratio: 0.59%) + Conflict : 163851 (Average Length: 824.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 163851 (Average: 19.64 Max: 818 Sum: 3217490) + Executed : 163779 (Average: 19.63 Max: 818 Sum: 3215576 Ratio: 99.94%) + Bounded : 72 (Average: 26.58 Max: 82 Sum: 1914 Ratio: 0.06%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 621171 (Eliminated: 0 Frozen: 191194) +Constraints : 4522784 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 726MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 5.64s +Memory: 667MB (+0MB) +UNKNOWN +Iteration Time: 5.70s + +Iteration 23 +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)] +Grounded Until: 80 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 24 +Time : 147.911s (Solving: 131.12s 1st Model: 0.01s Unsat: 0.93s) +CPU Time : 147.808s + +Choices : 3616155 (Domain: 3462337) +Conflicts : 172662 (Analyzed: 172660) +Restarts : 2033 (Average: 84.93 Last: 150) +Model-Level : 254.0 +Problems : 24 (Average Length: 42.42 Splits: 0) +Lemmas : 172660 (Deleted: 158068) + Binary : 5318 (Ratio: 3.08%) + Ternary : 1065 (Ratio: 0.62%) + Conflict : 172660 (Average Length: 794.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 172660 (Average: 19.17 Max: 818 Sum: 3309760) + Executed : 172585 (Average: 19.16 Max: 818 Sum: 3307600 Ratio: 99.93%) + Bounded : 75 (Average: 28.80 Max: 82 Sum: 2160 Ratio: 0.07%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 621171 (Eliminated: 0 Frozen: 191194) +Constraints : 4522579 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 726MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.15s +Memory: 667MB (+0MB) +UNKNOWN +Iteration Time: 6.20s + +Iteration 24 +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)] +Grounded Until: 80 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 25 +Time : 156.601s (Solving: 139.68s 1st Model: 0.01s Unsat: 0.93s) +CPU Time : 156.500s + +Choices : 3731283 (Domain: 3573611) +Conflicts : 181844 (Analyzed: 181842) +Restarts : 2133 (Average: 85.25 Last: 150) +Model-Level : 254.0 +Problems : 25 (Average Length: 44.00 Splits: 0) +Lemmas : 181842 (Deleted: 165509) + Binary : 5874 (Ratio: 3.23%) + Ternary : 1244 (Ratio: 0.68%) + Conflict : 181842 (Average Length: 766.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 181842 (Average: 18.79 Max: 818 Sum: 3416660) + Executed : 181763 (Average: 18.78 Max: 818 Sum: 3414172 Ratio: 99.93%) + Bounded : 79 (Average: 31.49 Max: 82 Sum: 2488 Ratio: 0.07%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 621171 (Eliminated: 0 Frozen: 191194) +Constraints : 4522538 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 726MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.65s +Memory: 667MB (+0MB) +UNKNOWN +Iteration Time: 8.70s + +Iteration 25 +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)] +Grounded Until: 80 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 26 +Time : 164.981s (Solving: 147.94s 1st Model: 0.01s Unsat: 0.93s) +CPU Time : 164.884s + +Choices : 3853462 (Domain: 3689639) +Conflicts : 190803 (Analyzed: 190801) +Restarts : 2233 (Average: 85.45 Last: 150) +Model-Level : 254.0 +Problems : 26 (Average Length: 45.46 Splits: 0) +Lemmas : 190801 (Deleted: 174103) + Binary : 6040 (Ratio: 3.17%) + Ternary : 1303 (Ratio: 0.68%) + Conflict : 190801 (Average Length: 746.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 190801 (Average: 18.48 Max: 818 Sum: 3526386) + Executed : 190721 (Average: 18.47 Max: 818 Sum: 3523816 Ratio: 99.93%) + Bounded : 80 (Average: 32.12 Max: 82 Sum: 2570 Ratio: 0.07%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 621171 (Eliminated: 0 Frozen: 191194) +Constraints : 4519680 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 726MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.34s +Memory: 667MB (+0MB) +UNKNOWN +Iteration Time: 8.39s + +Iteration 26 +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)] +Grounded Until: 80 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 27 +Time : 174.129s (Solving: 156.97s 1st Model: 0.01s Unsat: 0.93s) +CPU Time : 174.036s + +Choices : 4026215 (Domain: 3854302) +Conflicts : 200213 (Analyzed: 200211) +Restarts : 2333 (Average: 85.82 Last: 150) +Model-Level : 254.0 +Problems : 27 (Average Length: 46.81 Splits: 0) +Lemmas : 200211 (Deleted: 182615) + Binary : 6189 (Ratio: 3.09%) + Ternary : 1328 (Ratio: 0.66%) + Conflict : 200211 (Average Length: 727.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 200211 (Average: 18.41 Max: 818 Sum: 3685588) + Executed : 200131 (Average: 18.40 Max: 818 Sum: 3683018 Ratio: 99.93%) + Bounded : 80 (Average: 32.12 Max: 82 Sum: 2570 Ratio: 0.07%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 621171 (Eliminated: 0 Frozen: 191194) +Constraints : 4519667 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 726MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.11s +Memory: 667MB (+0MB) +UNKNOWN +Iteration Time: 9.15s + +Iteration 27 +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)] +Grounded Until: 80 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 28 +Time : 183.475s (Solving: 166.18s 1st Model: 0.01s Unsat: 0.93s) +CPU Time : 183.388s + +Choices : 4188503 (Domain: 4013177) +Conflicts : 209061 (Analyzed: 209059) +Restarts : 2433 (Average: 85.93 Last: 150) +Model-Level : 254.0 +Problems : 28 (Average Length: 48.07 Splits: 0) +Lemmas : 209059 (Deleted: 191460) + Binary : 6421 (Ratio: 3.07%) + Ternary : 1402 (Ratio: 0.67%) + Conflict : 209059 (Average Length: 711.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 209059 (Average: 18.34 Max: 818 Sum: 3834561) + Executed : 208977 (Average: 18.33 Max: 818 Sum: 3831827 Ratio: 99.93%) + Bounded : 82 (Average: 33.34 Max: 82 Sum: 2734 Ratio: 0.07%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 621171 (Eliminated: 0 Frozen: 191194) +Constraints : 4519667 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 726MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.30s +Memory: 667MB (+0MB) +UNKNOWN +Iteration Time: 9.35s + +Iteration 28 +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)] +Grounded Until: 80 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 29 +Time : 194.149s (Solving: 176.69s 1st Model: 0.01s Unsat: 0.93s) +CPU Time : 194.068s + +Choices : 4388056 (Domain: 4208740) +Conflicts : 217872 (Analyzed: 217870) +Restarts : 2533 (Average: 86.01 Last: 150) +Model-Level : 254.0 +Problems : 29 (Average Length: 49.24 Splits: 0) +Lemmas : 217870 (Deleted: 199733) + Binary : 6576 (Ratio: 3.02%) + Ternary : 1444 (Ratio: 0.66%) + Conflict : 217870 (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 : 217870 (Average: 18.44 Max: 818 Sum: 4017279) + Executed : 217787 (Average: 18.43 Max: 818 Sum: 4014463 Ratio: 99.93%) + Bounded : 83 (Average: 33.93 Max: 82 Sum: 2816 Ratio: 0.07%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 621171 (Eliminated: 0 Frozen: 191194) +Constraints : 4519639 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 726MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 10.62s +Memory: 667MB (+0MB) +UNKNOWN +Iteration Time: 10.68s + +Iteration 29 +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)] +Grounded Until: 80 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 30 +Time : 205.573s (Solving: 187.96s 1st Model: 0.01s Unsat: 0.93s) +CPU Time : 205.496s + +Choices : 4605515 (Domain: 4423171) +Conflicts : 226831 (Analyzed: 226829) +Restarts : 2633 (Average: 86.15 Last: 150) +Model-Level : 254.0 +Problems : 30 (Average Length: 50.33 Splits: 0) +Lemmas : 226829 (Deleted: 208173) + Binary : 6714 (Ratio: 2.96%) + Ternary : 1482 (Ratio: 0.65%) + Conflict : 226829 (Average Length: 679.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 226829 (Average: 18.60 Max: 818 Sum: 4219156) + Executed : 226744 (Average: 18.59 Max: 818 Sum: 4216176 Ratio: 99.93%) + Bounded : 85 (Average: 35.06 Max: 82 Sum: 2980 Ratio: 0.07%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 621171 (Eliminated: 0 Frozen: 191194) +Constraints : 4519625 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 726MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 11.37s +Memory: 667MB (+0MB) +UNKNOWN +Iteration Time: 11.43s + +Iteration 30 +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)] +Grounded Until: 80 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 31 +Time : 215.341s (Solving: 197.60s 1st Model: 0.01s Unsat: 0.93s) +CPU Time : 215.268s + +Choices : 4793152 (Domain: 4608690) +Conflicts : 235198 (Analyzed: 235196) +Restarts : 2733 (Average: 86.06 Last: 150) +Model-Level : 254.0 +Problems : 31 (Average Length: 51.35 Splits: 0) +Lemmas : 235196 (Deleted: 214549) + Binary : 6844 (Ratio: 2.91%) + Ternary : 1505 (Ratio: 0.64%) + Conflict : 235196 (Average Length: 665.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 235196 (Average: 18.66 Max: 818 Sum: 4389743) + Executed : 235110 (Average: 18.65 Max: 818 Sum: 4386681 Ratio: 99.93%) + Bounded : 86 (Average: 35.60 Max: 82 Sum: 3062 Ratio: 0.07%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 621171 (Eliminated: 0 Frozen: 191194) +Constraints : 4519599 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 726MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.73s +Memory: 667MB (+0MB) +UNKNOWN +Iteration Time: 9.78s + +Iteration 31 +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)] +Grounded Until: 80 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 32 +Time : 225.223s (Solving: 207.34s 1st Model: 0.01s Unsat: 0.93s) +CPU Time : 225.152s + +Choices : 5007257 (Domain: 4821249) +Conflicts : 243968 (Analyzed: 243966) +Restarts : 2833 (Average: 86.12 Last: 175) +Model-Level : 254.0 +Problems : 32 (Average Length: 52.31 Splits: 0) +Lemmas : 243966 (Deleted: 224708) + Binary : 6950 (Ratio: 2.85%) + Ternary : 1543 (Ratio: 0.63%) + Conflict : 243966 (Average Length: 652.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 243966 (Average: 18.81 Max: 818 Sum: 4589957) + Executed : 243877 (Average: 18.80 Max: 818 Sum: 4586649 Ratio: 99.93%) + Bounded : 89 (Average: 37.17 Max: 82 Sum: 3308 Ratio: 0.07%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 621171 (Eliminated: 0 Frozen: 191194) +Constraints : 4519585 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 726MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.84s +Memory: 667MB (+0MB) +UNKNOWN +Iteration Time: 9.89s + +Iteration 32 +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)] +Grounded Until: 80 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 33 +Time : 234.701s (Solving: 216.68s 1st Model: 0.01s Unsat: 0.93s) +CPU Time : 234.636s + +Choices : 5196384 (Domain: 5009297) +Conflicts : 252514 (Analyzed: 252512) +Restarts : 2933 (Average: 86.09 Last: 175) +Model-Level : 254.0 +Problems : 33 (Average Length: 53.21 Splits: 0) +Lemmas : 252512 (Deleted: 230991) + Binary : 7049 (Ratio: 2.79%) + Ternary : 1572 (Ratio: 0.62%) + Conflict : 252512 (Average Length: 640.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 252512 (Average: 18.87 Max: 818 Sum: 4764711) + Executed : 252423 (Average: 18.86 Max: 818 Sum: 4761403 Ratio: 99.93%) + Bounded : 89 (Average: 37.17 Max: 82 Sum: 3308 Ratio: 0.07%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 621171 (Eliminated: 0 Frozen: 191194) +Constraints : 4519544 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 726MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.43s +Memory: 667MB (+0MB) +UNKNOWN +Iteration Time: 9.48s + +Iteration 33 +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)] +Grounded Until: 80 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 34 +Time : 242.672s (Solving: 224.52s 1st Model: 0.01s Unsat: 0.93s) +CPU Time : 242.612s + +Choices : 5291696 (Domain: 5104282) +Conflicts : 260780 (Analyzed: 260778) +Restarts : 3033 (Average: 85.98 Last: 175) +Model-Level : 254.0 +Problems : 34 (Average Length: 54.06 Splits: 0) +Lemmas : 260778 (Deleted: 240360) + Binary : 7147 (Ratio: 2.74%) + Ternary : 1588 (Ratio: 0.61%) + Conflict : 260778 (Average Length: 631.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 260778 (Average: 18.59 Max: 818 Sum: 4846892) + Executed : 260689 (Average: 18.57 Max: 818 Sum: 4843584 Ratio: 99.93%) + Bounded : 89 (Average: 37.17 Max: 82 Sum: 3308 Ratio: 0.07%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 621171 (Eliminated: 0 Frozen: 191194) +Constraints : 4519544 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 726MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.93s +Memory: 667MB (+0MB) +UNKNOWN +Iteration Time: 7.98s + +Iteration 34 +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)] +Grounded Until: 80 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 35 +Time : 254.873s (Solving: 236.60s 1st Model: 0.01s Unsat: 0.93s) +CPU Time : 254.820s + +Choices : 5670287 (Domain: 5479652) +Conflicts : 269812 (Analyzed: 269810) +Restarts : 3133 (Average: 86.12 Last: 175) +Model-Level : 254.0 +Problems : 35 (Average Length: 54.86 Splits: 0) +Lemmas : 269810 (Deleted: 249341) + Binary : 7352 (Ratio: 2.72%) + Ternary : 1664 (Ratio: 0.62%) + Conflict : 269810 (Average Length: 618.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 269810 (Average: 19.28 Max: 966 Sum: 5203281) + Executed : 269720 (Average: 19.27 Max: 966 Sum: 5199891 Ratio: 99.93%) + Bounded : 90 (Average: 37.67 Max: 82 Sum: 3390 Ratio: 0.07%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 621171 (Eliminated: 0 Frozen: 191194) +Constraints : 4519544 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 726MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 12.17s +Memory: 667MB (+0MB) +UNKNOWN +Iteration Time: 12.21s + +Iteration 35 +Queue: [(16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True)] +Grounded Until: 80 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 36 +Time : 267.508s (Solving: 249.11s 1st Model: 0.01s Unsat: 0.93s) +CPU Time : 267.464s + +Choices : 6035181 (Domain: 5841662) +Conflicts : 278819 (Analyzed: 278817) +Restarts : 3233 (Average: 86.24 Last: 175) +Model-Level : 254.0 +Problems : 36 (Average Length: 55.61 Splits: 0) +Lemmas : 278817 (Deleted: 257774) + Binary : 7522 (Ratio: 2.70%) + Ternary : 1720 (Ratio: 0.62%) + Conflict : 278817 (Average Length: 607.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 278817 (Average: 19.89 Max: 1061 Sum: 5545315) + Executed : 278724 (Average: 19.88 Max: 1061 Sum: 5541679 Ratio: 99.93%) + Bounded : 93 (Average: 39.10 Max: 82 Sum: 3636 Ratio: 0.07%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 621171 (Eliminated: 0 Frozen: 191194) +Constraints : 4519530 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 726MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 12.60s +Memory: 667MB (+0MB) +UNKNOWN +Iteration Time: 12.64s + +Iteration 36 +Queue: [(17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True)] +Grounded Until: 80 +Expected Memory: 744.0MB +Grounding... [('step', [81]), ('step', [82]), ('step', [83]), ('step', [84]), ('step', [85]), ('check', [85])] +Grounding Time: 0.59s +Memory: 667MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 37 +Time : 278.843s (Solving: 259.27s 1st Model: 0.01s Unsat: 0.93s) +CPU Time : 278.800s + +Choices : 6492250 (Domain: 6295822) +Conflicts : 287420 (Analyzed: 287418) +Restarts : 3333 (Average: 86.23 Last: 175) +Model-Level : 254.0 +Problems : 37 (Average Length: 56.46 Splits: 0) +Lemmas : 287418 (Deleted: 266380) + Binary : 7719 (Ratio: 2.69%) + Ternary : 1739 (Ratio: 0.61%) + Conflict : 287418 (Average Length: 614.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 287418 (Average: 20.79 Max: 1061 Sum: 5974881) + Executed : 287325 (Average: 20.78 Max: 1061 Sum: 5971245 Ratio: 99.94%) + Bounded : 93 (Average: 39.10 Max: 82 Sum: 3636 Ratio: 0.06%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 661247 (Eliminated: 0 Frozen: 203644) +Constraints : 4821468 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 753MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 10.28s +Memory: 689MB (+22MB) +UNKNOWN +Iteration Time: 11.35s + +Iteration 37 +Queue: [(18,90,0,True), (19,95,0,True), (20,100,0,True)] +Grounded Until: 85 +Expected Memory: 766.0MB +Grounding... [('step', [86]), ('step', [87]), ('step', [88]), ('step', [89]), ('step', [90]), ('check', [90])] +Grounding Time: 0.59s +Memory: 689MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 38 +Time : 289.370s (Solving: 268.58s 1st Model: 0.01s Unsat: 0.93s) +CPU Time : 289.328s + +Choices : 6925880 (Domain: 6725902) +Conflicts : 296604 (Analyzed: 296602) +Restarts : 3433 (Average: 86.40 Last: 175) +Model-Level : 254.0 +Problems : 38 (Average Length: 57.39 Splits: 0) +Lemmas : 296602 (Deleted: 277010) + Binary : 7792 (Ratio: 2.63%) + Ternary : 1746 (Ratio: 0.59%) + Conflict : 296602 (Average Length: 624.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 296602 (Average: 21.49 Max: 1061 Sum: 6375261) + Executed : 296509 (Average: 21.48 Max: 1061 Sum: 6371625 Ratio: 99.94%) + Bounded : 93 (Average: 39.10 Max: 82 Sum: 3636 Ratio: 0.06%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 701323 (Eliminated: 0 Frozen: 216094) +Constraints : 5123448 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 791MB +Max. Length : 85 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.45s +Memory: 791MB (+102MB) +UNKNOWN +Iteration Time: 10.54s + +Iteration 38 +Queue: [(19,95,0,True), (20,100,0,True)] +Grounded Until: 90 +Expected Memory: 893.0MB +Grounding... [('step', [91]), ('step', [92]), ('step', [93]), ('step', [94]), ('step', [95]), ('check', [95])] +Grounding Time: 0.92s +Memory: 791MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 39 +Time : 299.836s (Solving: 277.50s 1st Model: 0.01s Unsat: 0.93s) +CPU Time : 299.796s + +Choices : 7279684 (Domain: 7077152) +Conflicts : 304419 (Analyzed: 304417) +Restarts : 3533 (Average: 86.16 Last: 175) +Model-Level : 254.0 +Problems : 39 (Average Length: 58.41 Splits: 0) +Lemmas : 304417 (Deleted: 283811) + Binary : 7827 (Ratio: 2.57%) + Ternary : 1750 (Ratio: 0.57%) + Conflict : 304417 (Average Length: 639.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 304417 (Average: 21.99 Max: 1061 Sum: 6693104) + Executed : 304324 (Average: 21.97 Max: 1061 Sum: 6689468 Ratio: 99.95%) + Bounded : 93 (Average: 39.10 Max: 82 Sum: 3636 Ratio: 0.05%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 741399 (Eliminated: 0 Frozen: 228544) +Constraints : 5425428 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 882MB +Max. Length : 90 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.06s +Memory: 797MB (+6MB) +UNKNOWN +Iteration Time: 10.48s + +Iteration 39 +Queue: [(20,100,0,True)] +Grounded Until: 95 +Expected Memory: 899.0MB +Grounding... [('step', [96]), ('step', [97]), ('step', [98]), ('step', [99]), ('step', [100]), ('check', [100])] +Grounding Time: 0.56s +Memory: 797MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 40 +Time : 310.789s (Solving: 287.23s 1st Model: 0.01s Unsat: 0.93s) +CPU Time : 310.752s + +Choices : 7694764 (Domain: 7489396) +Conflicts : 312176 (Analyzed: 312174) +Restarts : 3633 (Average: 85.93 Last: 175) +Model-Level : 254.0 +Problems : 40 (Average Length: 59.50 Splits: 0) +Lemmas : 312174 (Deleted: 291534) + Binary : 7854 (Ratio: 2.52%) + Ternary : 1754 (Ratio: 0.56%) + Conflict : 312174 (Average Length: 652.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 312174 (Average: 22.65 Max: 1061 Sum: 7071021) + Executed : 312081 (Average: 22.64 Max: 1061 Sum: 7067385 Ratio: 99.95%) + Bounded : 93 (Average: 39.10 Max: 82 Sum: 3636 Ratio: 0.05%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 781475 (Eliminated: 0 Frozen: 240994) +Constraints : 5727408 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 898MB +Max. Length : 95 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.88s +Memory: 821MB (+24MB) +UNKNOWN +Iteration Time: 10.97s + +Iteration 40 +Queue: [(3,15,3,True), (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,False), (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,0,True), (22,110,0,True)] +Grounded Until: 100 +Blocking actions... +Solving... +[start: stats after solve call] + +Models : 0 +Calls : 41 +Time : 311.274s (Solving: 287.56s 1st Model: 0.01s Unsat: 1.26s) +CPU Time : 311.240s + +Choices : 7695314 (Domain: 7489946) +Conflicts : 312400 (Analyzed: 312397) +Restarts : 3636 (Average: 85.92 Last: 175) +Model-Level : 254.0 +Problems : 41 (Average Length: 60.54 Splits: 0) +Lemmas : 312397 (Deleted: 291534) + Binary : 7861 (Ratio: 2.52%) + Ternary : 1759 (Ratio: 0.56%) + Conflict : 312397 (Average Length: 651.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 312397 (Average: 22.64 Max: 1061 Sum: 7071567) + Executed : 312302 (Average: 22.62 Max: 1061 Sum: 7067929 Ratio: 99.95%) + Bounded : 95 (Average: 38.29 Max: 82 Sum: 3638 Ratio: 0.05%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 781475 (Eliminated: 0 Frozen: 240994) +Constraints : 5727408 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 898MB +Max. Length : 100 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 0.43s +Memory: 821MB (+0MB) +UNSAT +Iteration Time: 0.49s + +Iteration 41 +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,False), (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,0,True), (22,110,0,True)] +Grounded Until: 100 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 42 +Time : 321.291s (Solving: 297.42s 1st Model: 0.01s Unsat: 1.26s) +CPU Time : 321.264s + +Choices : 7778212 (Domain: 7572844) +Conflicts : 320938 (Analyzed: 320935) +Restarts : 3736 (Average: 85.90 Last: 175) +Model-Level : 254.0 +Problems : 42 (Average Length: 61.52 Splits: 0) +Lemmas : 320935 (Deleted: 297578) + Binary : 7962 (Ratio: 2.48%) + Ternary : 1787 (Ratio: 0.56%) + Conflict : 320935 (Average Length: 648.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 320935 (Average: 22.27 Max: 1061 Sum: 7148340) + Executed : 320836 (Average: 22.26 Max: 1061 Sum: 7144602 Ratio: 99.95%) + Bounded : 99 (Average: 37.76 Max: 97 Sum: 3738 Ratio: 0.05%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 781475 (Eliminated: 0 Frozen: 240994) +Constraints : 5727408 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 898MB +Max. Length : 100 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.97s +Memory: 821MB (+0MB) +UNKNOWN +Iteration Time: 10.02s + +Iteration 42 +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,False), (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,0,True), (22,110,0,True)] +Grounded Until: 100 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 43 +Time : 328.910s (Solving: 304.88s 1st Model: 0.01s Unsat: 1.26s) +CPU Time : 328.888s + +Choices : 7842415 (Domain: 7635242) +Conflicts : 328957 (Analyzed: 328954) +Restarts : 3836 (Average: 85.75 Last: 175) +Model-Level : 254.0 +Problems : 43 (Average Length: 62.47 Splits: 0) +Lemmas : 328954 (Deleted: 305068) + Binary : 8032 (Ratio: 2.44%) + Ternary : 1809 (Ratio: 0.55%) + Conflict : 328954 (Average Length: 639.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 328954 (Average: 21.90 Max: 1061 Sum: 7203294) + Executed : 328854 (Average: 21.89 Max: 1061 Sum: 7199454 Ratio: 99.95%) + Bounded : 100 (Average: 38.40 Max: 102 Sum: 3840 Ratio: 0.05%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 781475 (Eliminated: 0 Frozen: 240994) +Constraints : 5727408 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 898MB +Max. Length : 100 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.56s +Memory: 821MB (+0MB) +UNKNOWN +Iteration Time: 7.62s + +Iteration 43 +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,False), (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,0,True), (22,110,0,True)] +Grounded Until: 100 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 44 +Time : 337.176s (Solving: 312.99s 1st Model: 0.01s Unsat: 1.26s) +CPU Time : 337.156s + +Choices : 7925575 (Domain: 7717227) +Conflicts : 337204 (Analyzed: 337201) +Restarts : 3936 (Average: 85.67 Last: 175) +Model-Level : 254.0 +Problems : 44 (Average Length: 63.36 Splits: 0) +Lemmas : 337201 (Deleted: 312789) + Binary : 8114 (Ratio: 2.41%) + Ternary : 1839 (Ratio: 0.55%) + Conflict : 337201 (Average Length: 630.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 337201 (Average: 21.58 Max: 1061 Sum: 7276712) + Executed : 337099 (Average: 21.57 Max: 1061 Sum: 7272668 Ratio: 99.94%) + Bounded : 102 (Average: 39.65 Max: 102 Sum: 4044 Ratio: 0.06%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 781475 (Eliminated: 0 Frozen: 240994) +Constraints : 5727394 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 898MB +Max. Length : 100 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.22s +Memory: 821MB (+0MB) +UNKNOWN +Iteration Time: 8.27s + +Iteration 44 +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,False), (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,0,True), (22,110,0,True)] +Grounded Until: 100 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 45 +Time : 345.060s (Solving: 320.70s 1st Model: 0.01s Unsat: 1.26s) +CPU Time : 345.044s + +Choices : 7997611 (Domain: 7788740) +Conflicts : 345433 (Analyzed: 345430) +Restarts : 4036 (Average: 85.59 Last: 175) +Model-Level : 254.0 +Problems : 45 (Average Length: 64.22 Splits: 0) +Lemmas : 345430 (Deleted: 320700) + Binary : 8161 (Ratio: 2.36%) + Ternary : 1850 (Ratio: 0.54%) + Conflict : 345430 (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 : 345430 (Average: 21.25 Max: 1061 Sum: 7339477) + Executed : 345328 (Average: 21.24 Max: 1061 Sum: 7335433 Ratio: 99.94%) + Bounded : 102 (Average: 39.65 Max: 102 Sum: 4044 Ratio: 0.06%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 781475 (Eliminated: 0 Frozen: 240994) +Constraints : 5727367 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 898MB +Max. Length : 100 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.82s +Memory: 821MB (+0MB) +UNKNOWN +Iteration Time: 7.89s + +Iteration 45 +Queue: [(8,40,2,True), (9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,False), (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,0,True), (22,110,0,True)] +Grounded Until: 100 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 46 +Time : 353.439s (Solving: 328.91s 1st Model: 0.01s Unsat: 1.26s) +CPU Time : 353.428s + +Choices : 8100519 (Domain: 7890476) +Conflicts : 353550 (Analyzed: 353547) +Restarts : 4136 (Average: 85.48 Last: 175) +Model-Level : 254.0 +Problems : 46 (Average Length: 65.04 Splits: 0) +Lemmas : 353547 (Deleted: 328589) + Binary : 8283 (Ratio: 2.34%) + Ternary : 1884 (Ratio: 0.53%) + Conflict : 353547 (Average Length: 613.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 353547 (Average: 21.02 Max: 1061 Sum: 7432066) + Executed : 353444 (Average: 21.01 Max: 1061 Sum: 7427925 Ratio: 99.94%) + Bounded : 103 (Average: 40.20 Max: 102 Sum: 4141 Ratio: 0.06%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 781475 (Eliminated: 0 Frozen: 240994) +Constraints : 5727367 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 898MB +Max. Length : 100 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.32s +Memory: 821MB (+0MB) +UNKNOWN +Iteration Time: 8.39s + +Iteration 46 +Queue: [(9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,False), (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,0,True), (22,110,0,True)] +Grounded Until: 100 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 47 +Time : 361.667s (Solving: 336.99s 1st Model: 0.01s Unsat: 1.26s) +CPU Time : 361.660s + +Choices : 8216292 (Domain: 8005467) +Conflicts : 361715 (Analyzed: 361712) +Restarts : 4236 (Average: 85.39 Last: 175) +Model-Level : 254.0 +Problems : 47 (Average Length: 65.83 Splits: 0) +Lemmas : 361712 (Deleted: 336327) + Binary : 8344 (Ratio: 2.31%) + Ternary : 1906 (Ratio: 0.53%) + Conflict : 361712 (Average Length: 605.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 361712 (Average: 20.84 Max: 1061 Sum: 7538558) + Executed : 361606 (Average: 20.83 Max: 1061 Sum: 7534116 Ratio: 99.94%) + Bounded : 106 (Average: 41.91 Max: 102 Sum: 4442 Ratio: 0.06%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 781475 (Eliminated: 0 Frozen: 240994) +Constraints : 5727367 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 898MB +Max. Length : 100 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.18s +Memory: 821MB (+0MB) +UNKNOWN +Iteration Time: 8.24s + +Iteration 47 +Queue: [(10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,False), (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,0,True), (22,110,0,True)] +Grounded Until: 100 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 48 +Time : 369.596s (Solving: 344.74s 1st Model: 0.01s Unsat: 1.26s) +CPU Time : 369.592s + +Choices : 8309386 (Domain: 8098255) +Conflicts : 369874 (Analyzed: 369871) +Restarts : 4336 (Average: 85.30 Last: 175) +Model-Level : 254.0 +Problems : 48 (Average Length: 66.58 Splits: 0) +Lemmas : 369871 (Deleted: 344182) + Binary : 8389 (Ratio: 2.27%) + Ternary : 1916 (Ratio: 0.52%) + Conflict : 369871 (Average Length: 597.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 369871 (Average: 20.61 Max: 1061 Sum: 7622602) + Executed : 369762 (Average: 20.60 Max: 1061 Sum: 7617869 Ratio: 99.94%) + Bounded : 109 (Average: 43.42 Max: 102 Sum: 4733 Ratio: 0.06%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 781475 (Eliminated: 0 Frozen: 240994) +Constraints : 5724726 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 898MB +Max. Length : 100 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.87s +Memory: 821MB (+0MB) +UNKNOWN +Iteration Time: 7.93s + +Iteration 48 +Queue: [(11,55,2,True), (12,60,2,True), (13,65,2,False), (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,0,True), (22,110,0,True)] +Grounded Until: 100 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 49 +Time : 376.690s (Solving: 351.69s 1st Model: 0.01s Unsat: 1.26s) +CPU Time : 376.688s + +Choices : 8387060 (Domain: 8175628) +Conflicts : 377753 (Analyzed: 377750) +Restarts : 4436 (Average: 85.16 Last: 175) +Model-Level : 254.0 +Problems : 49 (Average Length: 67.31 Splits: 0) +Lemmas : 377750 (Deleted: 352030) + Binary : 8450 (Ratio: 2.24%) + Ternary : 1933 (Ratio: 0.51%) + Conflict : 377750 (Average Length: 590.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 377750 (Average: 20.36 Max: 1061 Sum: 7690130) + Executed : 377637 (Average: 20.34 Max: 1061 Sum: 7684998 Ratio: 99.93%) + Bounded : 113 (Average: 45.42 Max: 102 Sum: 5132 Ratio: 0.07%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 781475 (Eliminated: 0 Frozen: 240994) +Constraints : 5724726 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 898MB +Max. Length : 100 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.05s +Memory: 821MB (+0MB) +UNKNOWN +Iteration Time: 7.10s + +Iteration 49 +Queue: [(12,60,2,True), (13,65,2,False), (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,0,True), (22,110,0,True)] +Grounded Until: 100 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 50 +Time : 386.491s (Solving: 361.29s 1st Model: 0.01s Unsat: 1.26s) +CPU Time : 386.496s + +Choices : 8718905 (Domain: 8505205) +Conflicts : 386599 (Analyzed: 386596) +Restarts : 4536 (Average: 85.23 Last: 175) +Model-Level : 254.0 +Problems : 50 (Average Length: 68.00 Splits: 0) +Lemmas : 386596 (Deleted: 361308) + Binary : 8919 (Ratio: 2.31%) + Ternary : 2114 (Ratio: 0.55%) + Conflict : 386596 (Average Length: 582.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 386596 (Average: 20.71 Max: 1061 Sum: 8007308) + Executed : 386482 (Average: 20.70 Max: 1061 Sum: 8002079 Ratio: 99.93%) + Bounded : 114 (Average: 45.87 Max: 102 Sum: 5229 Ratio: 0.07%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 781475 (Eliminated: 0 Frozen: 240994) +Constraints : 5724686 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 898MB +Max. Length : 100 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.73s +Memory: 821MB (+0MB) +UNKNOWN +Iteration Time: 9.81s + +Iteration 50 +Queue: [(17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,0,True), (22,110,0,True)] +Grounded Until: 100 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 51 +Time : 394.728s (Solving: 369.36s 1st Model: 0.01s Unsat: 1.26s) +CPU Time : 394.736s + +Choices : 9024213 (Domain: 8808303) +Conflicts : 394396 (Analyzed: 394393) +Restarts : 4636 (Average: 85.07 Last: 175) +Model-Level : 254.0 +Problems : 51 (Average Length: 68.67 Splits: 0) +Lemmas : 394393 (Deleted: 367228) + Binary : 9101 (Ratio: 2.31%) + Ternary : 2169 (Ratio: 0.55%) + Conflict : 394393 (Average Length: 576.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 394393 (Average: 21.04 Max: 1061 Sum: 8296840) + Executed : 394279 (Average: 21.02 Max: 1061 Sum: 8291611 Ratio: 99.94%) + Bounded : 114 (Average: 45.87 Max: 102 Sum: 5229 Ratio: 0.06%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 781475 (Eliminated: 0 Frozen: 240994) +Constraints : 5724686 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 898MB +Max. Length : 100 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.18s +Memory: 821MB (+0MB) +UNKNOWN +Iteration Time: 8.24s + +Iteration 51 +Queue: [(18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,0,True), (22,110,0,True)] +Grounded Until: 100 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 52 +Time : 404.262s (Solving: 378.74s 1st Model: 0.01s Unsat: 1.26s) +CPU Time : 404.276s + +Choices : 9292134 (Domain: 9074978) +Conflicts : 402431 (Analyzed: 402428) +Restarts : 4736 (Average: 84.97 Last: 175) +Model-Level : 254.0 +Problems : 52 (Average Length: 69.31 Splits: 0) +Lemmas : 402428 (Deleted: 374683) + Binary : 9231 (Ratio: 2.29%) + Ternary : 2198 (Ratio: 0.55%) + Conflict : 402428 (Average Length: 569.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 402428 (Average: 21.24 Max: 1075 Sum: 8547240) + Executed : 402314 (Average: 21.23 Max: 1075 Sum: 8542011 Ratio: 99.94%) + Bounded : 114 (Average: 45.87 Max: 102 Sum: 5229 Ratio: 0.06%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 781475 (Eliminated: 0 Frozen: 240994) +Constraints : 5724686 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 898MB +Max. Length : 100 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.49s +Memory: 821MB (+0MB) +UNKNOWN +Iteration Time: 9.54s + +Iteration 52 +Queue: [(19,95,1,True), (20,100,1,True), (21,105,0,True), (22,110,0,True)] +Grounded Until: 100 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 53 +Time : 413.940s (Solving: 388.26s 1st Model: 0.01s Unsat: 1.26s) +CPU Time : 413.960s + +Choices : 9562327 (Domain: 9344325) +Conflicts : 410458 (Analyzed: 410455) +Restarts : 4836 (Average: 84.87 Last: 175) +Model-Level : 254.0 +Problems : 53 (Average Length: 69.92 Splits: 0) +Lemmas : 410455 (Deleted: 382351) + Binary : 9301 (Ratio: 2.27%) + Ternary : 2222 (Ratio: 0.54%) + Conflict : 410455 (Average Length: 564.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 410455 (Average: 21.43 Max: 1126 Sum: 8797640) + Executed : 410341 (Average: 21.42 Max: 1126 Sum: 8792411 Ratio: 99.94%) + Bounded : 114 (Average: 45.87 Max: 102 Sum: 5229 Ratio: 0.06%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 781475 (Eliminated: 0 Frozen: 240994) +Constraints : 5724686 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 898MB +Max. Length : 100 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.63s +Memory: 821MB (+0MB) +UNKNOWN +Iteration Time: 9.68s + +Iteration 53 +Queue: [(20,100,1,True), (21,105,0,True), (22,110,0,True)] +Grounded Until: 100 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 54 +Time : 429.082s (Solving: 403.25s 1st Model: 0.01s Unsat: 1.26s) +CPU Time : 429.108s + +Choices : 10126990 (Domain: 9906927) +Conflicts : 419268 (Analyzed: 419265) +Restarts : 4936 (Average: 84.94 Last: 175) +Model-Level : 254.0 +Problems : 54 (Average Length: 70.52 Splits: 0) +Lemmas : 419265 (Deleted: 391947) + Binary : 9605 (Ratio: 2.29%) + Ternary : 2334 (Ratio: 0.56%) + Conflict : 419265 (Average Length: 558.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 419265 (Average: 22.28 Max: 1130 Sum: 9340952) + Executed : 419150 (Average: 22.27 Max: 1130 Sum: 9335621 Ratio: 99.94%) + Bounded : 115 (Average: 46.36 Max: 102 Sum: 5331 Ratio: 0.06%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 781475 (Eliminated: 0 Frozen: 240994) +Constraints : 5724686 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 898MB +Max. Length : 100 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 15.10s +Memory: 821MB (+0MB) +UNKNOWN +Iteration Time: 15.15s + +Iteration 54 +Queue: [(21,105,0,True), (22,110,0,True)] +Grounded Until: 100 +Expected Memory: 923.0MB +Grounding... [('step', [101]), ('step', [102]), ('step', [103]), ('step', [104]), ('step', [105]), ('check', [105])] +Grounding Time: 0.57s +Memory: 822MB (+1MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 55 +Time : 443.624s (Solving: 416.54s 1st Model: 0.01s Unsat: 1.26s) +CPU Time : 443.656s + +Choices : 10679603 (Domain: 10455698) +Conflicts : 428070 (Analyzed: 428067) +Restarts : 5036 (Average: 85.00 Last: 175) +Model-Level : 254.0 +Problems : 55 (Average Length: 71.18 Splits: 0) +Lemmas : 428067 (Deleted: 400883) + Binary : 9734 (Ratio: 2.27%) + Ternary : 2367 (Ratio: 0.55%) + Conflict : 428067 (Average Length: 563.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 428067 (Average: 23.03 Max: 1146 Sum: 9857106) + Executed : 427952 (Average: 23.01 Max: 1146 Sum: 9851775 Ratio: 99.95%) + Bounded : 115 (Average: 46.36 Max: 102 Sum: 5331 Ratio: 0.05%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 821551 (Eliminated: 0 Frozen: 253444) +Constraints : 6026640 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 938MB +Max. Length : 100 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 13.45s +Memory: 848MB (+26MB) +UNKNOWN +Iteration Time: 14.56s + +Iteration 55 +Queue: [(22,110,0,True)] +Grounded Until: 105 +Expected Memory: 950.0MB +Grounding... [('step', [106]), ('step', [107]), ('step', [108]), ('step', [109]), ('step', [110]), ('check', [110])] +Grounding Time: 0.56s +Memory: 848MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 56 +Time : 455.316s (Solving: 426.99s 1st Model: 0.01s Unsat: 1.26s) +CPU Time : 455.352s + +Choices : 11009832 (Domain: 10784491) +Conflicts : 435988 (Analyzed: 435985) +Restarts : 5136 (Average: 84.89 Last: 175) +Model-Level : 254.0 +Problems : 56 (Average Length: 71.91 Splits: 0) +Lemmas : 435985 (Deleted: 408670) + Binary : 9768 (Ratio: 2.24%) + Ternary : 2371 (Ratio: 0.54%) + Conflict : 435985 (Average Length: 571.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 435985 (Average: 23.28 Max: 1146 Sum: 10147993) + Executed : 435870 (Average: 23.26 Max: 1146 Sum: 10142662 Ratio: 99.95%) + Bounded : 115 (Average: 46.36 Max: 102 Sum: 5331 Ratio: 0.05%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 861627 (Eliminated: 0 Frozen: 265894) +Constraints : 6328620 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 971MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 10.61s +Memory: 881MB (+33MB) +UNKNOWN +Iteration Time: 11.71s + +Iteration 56 +Queue: [(4,20,4,True), (5,25,4,True), (6,30,4,True), (7,35,3,True), (8,40,3,True), (9,45,3,True), (10,50,3,True), (11,55,3,False), (12,60,3,False), (13,65,2,True), (14,70,2,True), (15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,1,True), (22,110,1,True), (23,115,0,True)] +Grounded Until: 110 +Blocking actions... +Solving... +[start: stats after solve call] + +Models : 0 +Calls : 57 +Time : 466.556s (Solving: 438.01s 1st Model: 0.01s Unsat: 12.29s) +CPU Time : 466.600s + +Choices : 11089562 (Domain: 10864221) +Conflicts : 442558 (Analyzed: 442554) +Restarts : 5210 (Average: 84.94 Last: 175) +Model-Level : 254.0 +Problems : 57 (Average Length: 72.61 Splits: 0) +Lemmas : 442554 (Deleted: 414658) + Binary : 9922 (Ratio: 2.24%) + Ternary : 2388 (Ratio: 0.54%) + Conflict : 442554 (Average Length: 568.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 442554 (Average: 23.11 Max: 1146 Sum: 10226036) + Executed : 442431 (Average: 23.09 Max: 1146 Sum: 10220591 Ratio: 99.95%) + Bounded : 123 (Average: 44.27 Max: 107 Sum: 5445 Ratio: 0.05%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 861627 (Eliminated: 0 Frozen: 265894) +Constraints : 6328620 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 971MB +Max. Length : 110 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 11.16s +Memory: 884MB (+3MB) +UNSAT +Iteration Time: 11.25s + +Iteration 57 +Queue: [(5,25,4,True), (6,30,4,True), (7,35,3,True), (8,40,3,True), (9,45,3,True), (10,50,3,True), (11,55,3,False), (12,60,3,False), (13,65,2,True), (14,70,2,True), (15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,1,True), (22,110,1,True), (23,115,0,True)] +Grounded Until: 110 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 58 +Time : 472.195s (Solving: 443.47s 1st Model: 0.01s Unsat: 12.29s) +CPU Time : 472.240s + +Choices : 11140666 (Domain: 10915316) +Conflicts : 450162 (Analyzed: 450158) +Restarts : 5310 (Average: 84.78 Last: 175) +Model-Level : 254.0 +Problems : 58 (Average Length: 73.29 Splits: 0) +Lemmas : 450158 (Deleted: 420439) + Binary : 9993 (Ratio: 2.22%) + Ternary : 2417 (Ratio: 0.54%) + Conflict : 450158 (Average Length: 563.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 450158 (Average: 22.81 Max: 1146 Sum: 10269499) + Executed : 450035 (Average: 22.80 Max: 1146 Sum: 10264054 Ratio: 99.95%) + Bounded : 123 (Average: 44.27 Max: 107 Sum: 5445 Ratio: 0.05%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 861627 (Eliminated: 0 Frozen: 265894) +Constraints : 6328620 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 971MB +Max. Length : 110 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 5.58s +Memory: 884MB (+0MB) +UNKNOWN +Iteration Time: 5.65s + +Iteration 58 +Queue: [(6,30,4,True), (7,35,3,True), (8,40,3,True), (9,45,3,True), (10,50,3,True), (11,55,3,False), (12,60,3,False), (13,65,2,True), (14,70,2,True), (15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,1,True), (22,110,1,True), (23,115,0,True)] +Grounded Until: 110 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 59 +Time : 477.975s (Solving: 449.05s 1st Model: 0.01s Unsat: 12.29s) +CPU Time : 478.020s + +Choices : 11195924 (Domain: 10970510) +Conflicts : 457999 (Analyzed: 457995) +Restarts : 5410 (Average: 84.66 Last: 175) +Model-Level : 254.0 +Problems : 59 (Average Length: 73.95 Splits: 0) +Lemmas : 457995 (Deleted: 427638) + Binary : 10078 (Ratio: 2.20%) + Ternary : 2438 (Ratio: 0.53%) + Conflict : 457995 (Average Length: 558.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 457995 (Average: 22.53 Max: 1146 Sum: 10317774) + Executed : 457870 (Average: 22.52 Max: 1146 Sum: 10312110 Ratio: 99.95%) + Bounded : 125 (Average: 45.31 Max: 112 Sum: 5664 Ratio: 0.05%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 861627 (Eliminated: 0 Frozen: 265894) +Constraints : 6328620 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 971MB +Max. Length : 110 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 5.71s +Memory: 884MB (+0MB) +UNKNOWN +Iteration Time: 5.79s + +Iteration 59 +Queue: [(7,35,3,True), (8,40,3,True), (9,45,3,True), (10,50,3,True), (11,55,3,False), (12,60,3,False), (13,65,2,True), (14,70,2,True), (15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,1,True), (22,110,1,True), (23,115,0,True)] +Grounded Until: 110 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 60 +Time : 485.713s (Solving: 456.59s 1st Model: 0.01s Unsat: 12.29s) +CPU Time : 485.764s + +Choices : 11299372 (Domain: 11072098) +Conflicts : 466473 (Analyzed: 466469) +Restarts : 5510 (Average: 84.66 Last: 175) +Model-Level : 254.0 +Problems : 60 (Average Length: 74.58 Splits: 0) +Lemmas : 466469 (Deleted: 435134) + Binary : 10300 (Ratio: 2.21%) + Ternary : 2544 (Ratio: 0.55%) + Conflict : 466469 (Average Length: 552.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 466469 (Average: 22.32 Max: 1146 Sum: 10410869) + Executed : 466342 (Average: 22.31 Max: 1146 Sum: 10404986 Ratio: 99.94%) + Bounded : 127 (Average: 46.32 Max: 112 Sum: 5883 Ratio: 0.06%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 861627 (Eliminated: 0 Frozen: 265894) +Constraints : 6328606 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 971MB +Max. Length : 110 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.67s +Memory: 884MB (+0MB) +UNKNOWN +Iteration Time: 7.74s + +Iteration 60 +Queue: [(8,40,3,True), (9,45,3,True), (10,50,3,True), (11,55,3,False), (12,60,3,False), (13,65,2,True), (14,70,2,True), (15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,1,True), (22,110,1,True), (23,115,0,True)] +Grounded Until: 110 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 61 +Time : 493.456s (Solving: 464.11s 1st Model: 0.01s Unsat: 12.29s) +CPU Time : 493.508s + +Choices : 11420205 (Domain: 11191068) +Conflicts : 475017 (Analyzed: 475013) +Restarts : 5610 (Average: 84.67 Last: 175) +Model-Level : 254.0 +Problems : 61 (Average Length: 75.20 Splits: 0) +Lemmas : 475013 (Deleted: 443064) + Binary : 10587 (Ratio: 2.23%) + Ternary : 2626 (Ratio: 0.55%) + Conflict : 475013 (Average Length: 547.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 475013 (Average: 22.15 Max: 1146 Sum: 10520141) + Executed : 474886 (Average: 22.13 Max: 1146 Sum: 10514258 Ratio: 99.94%) + Bounded : 127 (Average: 46.32 Max: 112 Sum: 5883 Ratio: 0.06%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 861627 (Eliminated: 0 Frozen: 265894) +Constraints : 6328580 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 971MB +Max. Length : 110 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.66s +Memory: 884MB (+0MB) +UNKNOWN +Iteration Time: 7.75s + +Iteration 61 +Queue: [(9,45,3,True), (10,50,3,True), (11,55,3,False), (12,60,3,False), (13,65,2,True), (14,70,2,True), (15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,1,True), (22,110,1,True), (23,115,0,True)] +Grounded Until: 110 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 62 +Time : 500.880s (Solving: 471.35s 1st Model: 0.01s Unsat: 12.29s) +CPU Time : 500.936s + +Choices : 11544660 (Domain: 11313881) +Conflicts : 482966 (Analyzed: 482962) +Restarts : 5710 (Average: 84.58 Last: 175) +Model-Level : 254.0 +Problems : 62 (Average Length: 75.79 Splits: 0) +Lemmas : 482962 (Deleted: 451002) + Binary : 10724 (Ratio: 2.22%) + Ternary : 2664 (Ratio: 0.55%) + Conflict : 482962 (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 : 482962 (Average: 22.02 Max: 1146 Sum: 10632575) + Executed : 482835 (Average: 22.00 Max: 1146 Sum: 10626692 Ratio: 99.94%) + Bounded : 127 (Average: 46.32 Max: 112 Sum: 5883 Ratio: 0.06%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 861627 (Eliminated: 0 Frozen: 265894) +Constraints : 6328580 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 971MB +Max. Length : 110 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.36s +Memory: 884MB (+0MB) +UNKNOWN +Iteration Time: 7.43s + +Iteration 62 +Queue: [(10,50,3,True), (11,55,3,False), (12,60,3,False), (13,65,2,True), (14,70,2,True), (15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,1,True), (22,110,1,True), (23,115,0,True)] +Grounded Until: 110 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 63 +Time : 510.227s (Solving: 480.52s 1st Model: 0.01s Unsat: 12.29s) +CPU Time : 510.288s + +Choices : 11752698 (Domain: 11519372) +Conflicts : 491386 (Analyzed: 491382) +Restarts : 5810 (Average: 84.58 Last: 175) +Model-Level : 254.0 +Problems : 63 (Average Length: 76.37 Splits: 0) +Lemmas : 491382 (Deleted: 458343) + Binary : 11120 (Ratio: 2.26%) + Ternary : 2838 (Ratio: 0.58%) + Conflict : 491382 (Average Length: 538.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 491382 (Average: 22.03 Max: 1146 Sum: 10825014) + Executed : 491254 (Average: 22.02 Max: 1146 Sum: 10819019 Ratio: 99.94%) + Bounded : 128 (Average: 46.84 Max: 112 Sum: 5995 Ratio: 0.06%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 861627 (Eliminated: 0 Frozen: 265894) +Constraints : 6328580 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 971MB +Max. Length : 110 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.29s +Memory: 884MB (+0MB) +UNKNOWN +Iteration Time: 9.35s + +Iteration 63 +Queue: [(13,65,2,True), (14,70,2,True), (15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,1,True), (22,110,1,True), (23,115,0,True)] +Grounded Until: 110 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 64 +Time : 517.566s (Solving: 487.69s 1st Model: 0.01s Unsat: 12.29s) +CPU Time : 517.632s + +Choices : 11913679 (Domain: 11679834) +Conflicts : 499648 (Analyzed: 499644) +Restarts : 5910 (Average: 84.54 Last: 175) +Model-Level : 254.0 +Problems : 64 (Average Length: 76.92 Splits: 0) +Lemmas : 499644 (Deleted: 465893) + Binary : 11349 (Ratio: 2.27%) + Ternary : 2891 (Ratio: 0.58%) + Conflict : 499644 (Average Length: 533.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 499644 (Average: 21.96 Max: 1146 Sum: 10971841) + Executed : 499515 (Average: 21.95 Max: 1146 Sum: 10965739 Ratio: 99.94%) + Bounded : 129 (Average: 47.30 Max: 112 Sum: 6102 Ratio: 0.06%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 861627 (Eliminated: 0 Frozen: 265894) +Constraints : 6328554 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 971MB +Max. Length : 110 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.29s +Memory: 884MB (+0MB) +UNKNOWN +Iteration Time: 7.34s + +Iteration 64 +Queue: [(14,70,2,True), (15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,1,True), (22,110,1,True), (23,115,0,True)] +Grounded Until: 110 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 65 +Time : 526.309s (Solving: 496.25s 1st Model: 0.01s Unsat: 12.29s) +CPU Time : 526.376s + +Choices : 12115412 (Domain: 11880075) +Conflicts : 507889 (Analyzed: 507885) +Restarts : 6010 (Average: 84.51 Last: 175) +Model-Level : 254.0 +Problems : 65 (Average Length: 77.46 Splits: 0) +Lemmas : 507885 (Deleted: 473600) + Binary : 11555 (Ratio: 2.28%) + Ternary : 2941 (Ratio: 0.58%) + Conflict : 507885 (Average Length: 529.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 507885 (Average: 21.97 Max: 1146 Sum: 11157853) + Executed : 507756 (Average: 21.96 Max: 1146 Sum: 11151751 Ratio: 99.95%) + Bounded : 129 (Average: 47.30 Max: 112 Sum: 6102 Ratio: 0.05%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 861627 (Eliminated: 0 Frozen: 265894) +Constraints : 6328554 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 971MB +Max. Length : 110 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.68s +Memory: 884MB (+0MB) +UNKNOWN +Iteration Time: 8.75s + +Iteration 65 +Queue: [(15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,1,True), (22,110,1,True), (23,115,0,True)] +Grounded Until: 110 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 66 +Time : 531.173s (Solving: 500.94s 1st Model: 0.01s Unsat: 12.29s) +CPU Time : 531.240s + +Choices : 12257399 (Domain: 12021648) +Conflicts : 515266 (Analyzed: 515262) +Restarts : 6110 (Average: 84.33 Last: 175) +Model-Level : 254.0 +Problems : 66 (Average Length: 77.98 Splits: 0) +Lemmas : 515262 (Deleted: 481624) + Binary : 11680 (Ratio: 2.27%) + Ternary : 2981 (Ratio: 0.58%) + Conflict : 515262 (Average Length: 524.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 515262 (Average: 21.90 Max: 1146 Sum: 11283889) + Executed : 515133 (Average: 21.89 Max: 1146 Sum: 11277787 Ratio: 99.95%) + Bounded : 129 (Average: 47.30 Max: 112 Sum: 6102 Ratio: 0.05%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 861627 (Eliminated: 0 Frozen: 265894) +Constraints : 6328554 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 971MB +Max. Length : 110 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 4.81s +Memory: 884MB (+0MB) +UNKNOWN +Iteration Time: 4.87s + +Iteration 66 +Queue: [(21,105,1,True), (22,110,1,True), (23,115,0,True)] +Grounded Until: 110 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 67 +Time : 541.644s (Solving: 511.24s 1st Model: 0.01s Unsat: 12.29s) +CPU Time : 541.716s + +Choices : 12611331 (Domain: 12374369) +Conflicts : 523435 (Analyzed: 523431) +Restarts : 6210 (Average: 84.29 Last: 175) +Model-Level : 254.0 +Problems : 67 (Average Length: 78.49 Splits: 0) +Lemmas : 523431 (Deleted: 488321) + Binary : 12008 (Ratio: 2.29%) + Ternary : 3047 (Ratio: 0.58%) + Conflict : 523431 (Average Length: 520.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 523431 (Average: 22.19 Max: 1227 Sum: 11616138) + Executed : 523301 (Average: 22.18 Max: 1227 Sum: 11609924 Ratio: 99.95%) + Bounded : 130 (Average: 47.80 Max: 112 Sum: 6214 Ratio: 0.05%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 861627 (Eliminated: 0 Frozen: 265894) +Constraints : 6328554 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 971MB +Max. Length : 110 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 10.42s +Memory: 884MB (+0MB) +UNKNOWN +Iteration Time: 10.48s + +Iteration 67 +Queue: [(22,110,1,True), (23,115,0,True)] +Grounded Until: 110 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 68 +Time : 553.874s (Solving: 523.30s 1st Model: 0.01s Unsat: 12.29s) +CPU Time : 553.952s + +Choices : 12992440 (Domain: 12754027) +Conflicts : 531758 (Analyzed: 531754) +Restarts : 6310 (Average: 84.27 Last: 175) +Model-Level : 254.0 +Problems : 68 (Average Length: 78.99 Splits: 0) +Lemmas : 531754 (Deleted: 495804) + Binary : 12298 (Ratio: 2.31%) + Ternary : 3145 (Ratio: 0.59%) + Conflict : 531754 (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 : 531754 (Average: 22.52 Max: 1313 Sum: 11973008) + Executed : 531624 (Average: 22.50 Max: 1313 Sum: 11966794 Ratio: 99.95%) + Bounded : 130 (Average: 47.80 Max: 112 Sum: 6214 Ratio: 0.05%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 861627 (Eliminated: 0 Frozen: 265894) +Constraints : 6328540 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 971MB +Max. Length : 110 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 12.18s +Memory: 884MB (+0MB) +UNKNOWN +Iteration Time: 12.24s + +Iteration 68 +Queue: [(23,115,0,True)] +Grounded Until: 110 +Expected Memory: 986.0MB +Grounding... [('step', [111]), ('step', [112]), ('step', [113]), ('step', [114]), ('step', [115]), ('check', [115])] +Grounding Time: 0.59s +Memory: 884MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 69 +Time : 570.212s (Solving: 538.31s 1st Model: 0.01s Unsat: 12.29s) +CPU Time : 570.296s + +Choices : 13409834 (Domain: 13170777) +Conflicts : 541304 (Analyzed: 541300) +Restarts : 6410 (Average: 84.45 Last: 175) +Model-Level : 254.0 +Problems : 69 (Average Length: 79.54 Splits: 0) +Lemmas : 541300 (Deleted: 505809) + Binary : 12573 (Ratio: 2.32%) + Ternary : 3215 (Ratio: 0.59%) + Conflict : 541300 (Average Length: 521.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 541300 (Average: 22.82 Max: 1313 Sum: 12349815) + Executed : 541170 (Average: 22.80 Max: 1313 Sum: 12343601 Ratio: 99.95%) + Bounded : 130 (Average: 47.80 Max: 112 Sum: 6214 Ratio: 0.05%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 901703 (Eliminated: 0 Frozen: 278344) +Constraints : 6630520 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1037MB +Max. Length : 110 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 15.18s +Memory: 973MB (+89MB) +UNKNOWN +Iteration Time: 16.36s + +Iteration 69 +Queue: [(5,25,5,True), (6,30,5,True), (7,35,4,True), (8,40,4,True), (9,45,4,True), (10,50,4,True), (11,55,3,True), (12,60,3,True), (13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,2,True), (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,1,True), (24,120,0,True)] +Grounded Until: 115 +Blocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 70 +Time : 574.954s (Solving: 542.86s 1st Model: 0.01s Unsat: 12.29s) +CPU Time : 575.040s + +Choices : 13446171 (Domain: 13207114) +Conflicts : 548635 (Analyzed: 548631) +Restarts : 6510 (Average: 84.28 Last: 175) +Model-Level : 254.0 +Problems : 70 (Average Length: 80.07 Splits: 0) +Lemmas : 548631 (Deleted: 512656) + Binary : 12660 (Ratio: 2.31%) + Ternary : 3219 (Ratio: 0.59%) + Conflict : 548631 (Average Length: 518.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 548631 (Average: 22.56 Max: 1313 Sum: 12377314) + Executed : 548501 (Average: 22.55 Max: 1313 Sum: 12371100 Ratio: 99.95%) + Bounded : 130 (Average: 47.80 Max: 112 Sum: 6214 Ratio: 0.05%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 901703 (Eliminated: 0 Frozen: 278344) +Constraints : 6630520 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1037MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 4.67s +Memory: 973MB (+0MB) +UNKNOWN +Iteration Time: 4.75s + +Iteration 70 +Queue: [(6,30,5,True), (7,35,4,True), (8,40,4,True), (9,45,4,True), (10,50,4,True), (11,55,3,True), (12,60,3,True), (13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,2,True), (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,1,True), (24,120,0,True)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 71 +Time : 579.391s (Solving: 547.09s 1st Model: 0.01s Unsat: 12.29s) +CPU Time : 579.480s + +Choices : 13491098 (Domain: 13252041) +Conflicts : 556034 (Analyzed: 556030) +Restarts : 6610 (Average: 84.12 Last: 175) +Model-Level : 254.0 +Problems : 71 (Average Length: 80.59 Splits: 0) +Lemmas : 556030 (Deleted: 519769) + Binary : 12694 (Ratio: 2.28%) + Ternary : 3227 (Ratio: 0.58%) + Conflict : 556030 (Average Length: 514.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 556030 (Average: 22.32 Max: 1313 Sum: 12413263) + Executed : 555900 (Average: 22.31 Max: 1313 Sum: 12407049 Ratio: 99.95%) + Bounded : 130 (Average: 47.80 Max: 112 Sum: 6214 Ratio: 0.05%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 901703 (Eliminated: 0 Frozen: 278344) +Constraints : 6630520 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1037MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 4.37s +Memory: 973MB (+0MB) +UNKNOWN +Iteration Time: 4.44s + +Iteration 71 +Queue: [(7,35,4,True), (8,40,4,True), (9,45,4,True), (10,50,4,True), (11,55,3,True), (12,60,3,True), (13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,2,True), (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,1,True), (24,120,0,True)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 72 +Time : 585.615s (Solving: 553.14s 1st Model: 0.01s Unsat: 12.29s) +CPU Time : 585.708s + +Choices : 13531946 (Domain: 13292889) +Conflicts : 563864 (Analyzed: 563860) +Restarts : 6710 (Average: 84.03 Last: 175) +Model-Level : 254.0 +Problems : 72 (Average Length: 81.10 Splits: 0) +Lemmas : 563860 (Deleted: 526767) + Binary : 12787 (Ratio: 2.27%) + Ternary : 3256 (Ratio: 0.58%) + Conflict : 563860 (Average Length: 511.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 563860 (Average: 22.08 Max: 1313 Sum: 12447450) + Executed : 563729 (Average: 22.06 Max: 1313 Sum: 12441124 Ratio: 99.95%) + Bounded : 131 (Average: 48.29 Max: 112 Sum: 6326 Ratio: 0.05%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 901703 (Eliminated: 0 Frozen: 278344) +Constraints : 6630520 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1037MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.17s +Memory: 973MB (+0MB) +UNKNOWN +Iteration Time: 6.23s + +Iteration 72 +Queue: [(8,40,4,True), (9,45,4,True), (10,50,4,True), (11,55,3,True), (12,60,3,True), (13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,2,True), (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,1,True), (24,120,0,True)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 73 +Time : 592.702s (Solving: 560.05s 1st Model: 0.01s Unsat: 12.29s) +CPU Time : 592.796s + +Choices : 13614649 (Domain: 13374499) +Conflicts : 571828 (Analyzed: 571824) +Restarts : 6810 (Average: 83.97 Last: 175) +Model-Level : 254.0 +Problems : 73 (Average Length: 81.59 Splits: 0) +Lemmas : 571824 (Deleted: 534296) + Binary : 12927 (Ratio: 2.26%) + Ternary : 3312 (Ratio: 0.58%) + Conflict : 571824 (Average Length: 507.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 571824 (Average: 21.89 Max: 1313 Sum: 12518622) + Executed : 571693 (Average: 21.88 Max: 1313 Sum: 12512296 Ratio: 99.95%) + Bounded : 131 (Average: 48.29 Max: 112 Sum: 6326 Ratio: 0.05%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 901703 (Eliminated: 0 Frozen: 278344) +Constraints : 6630520 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1037MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.03s +Memory: 973MB (+0MB) +UNKNOWN +Iteration Time: 7.09s + +Iteration 73 +Queue: [(9,45,4,True), (10,50,4,True), (11,55,3,True), (12,60,3,True), (13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,2,True), (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,1,True), (24,120,0,True)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 74 +Time : 602.183s (Solving: 569.35s 1st Model: 0.01s Unsat: 12.29s) +CPU Time : 602.280s + +Choices : 13776933 (Domain: 13533403) +Conflicts : 580467 (Analyzed: 580463) +Restarts : 6910 (Average: 84.00 Last: 175) +Model-Level : 254.0 +Problems : 74 (Average Length: 82.07 Splits: 0) +Lemmas : 580463 (Deleted: 543005) + Binary : 13444 (Ratio: 2.32%) + Ternary : 3517 (Ratio: 0.61%) + Conflict : 580463 (Average Length: 503.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 580463 (Average: 21.82 Max: 1313 Sum: 12662988) + Executed : 580332 (Average: 21.80 Max: 1313 Sum: 12656662 Ratio: 99.95%) + Bounded : 131 (Average: 48.29 Max: 112 Sum: 6326 Ratio: 0.05%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 901703 (Eliminated: 0 Frozen: 278344) +Constraints : 6630520 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1037MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.43s +Memory: 973MB (+0MB) +UNKNOWN +Iteration Time: 9.49s + +Iteration 74 +Queue: [(10,50,4,True), (11,55,3,True), (12,60,3,True), (13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,2,True), (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,1,True), (24,120,0,True)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 75 +Time : 612.329s (Solving: 579.32s 1st Model: 0.01s Unsat: 12.29s) +CPU Time : 612.428s + +Choices : 13937524 (Domain: 13692561) +Conflicts : 589145 (Analyzed: 589141) +Restarts : 7010 (Average: 84.04 Last: 175) +Model-Level : 254.0 +Problems : 75 (Average Length: 82.53 Splits: 0) +Lemmas : 589141 (Deleted: 550894) + Binary : 13829 (Ratio: 2.35%) + Ternary : 3671 (Ratio: 0.62%) + Conflict : 589141 (Average Length: 500.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 589141 (Average: 21.74 Max: 1313 Sum: 12805704) + Executed : 589010 (Average: 21.73 Max: 1313 Sum: 12799378 Ratio: 99.95%) + Bounded : 131 (Average: 48.29 Max: 112 Sum: 6326 Ratio: 0.05%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 901703 (Eliminated: 0 Frozen: 278344) +Constraints : 6630520 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1037MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 10.09s +Memory: 973MB (+0MB) +UNKNOWN +Iteration Time: 10.15s + +Iteration 75 +Queue: [(11,55,3,True), (12,60,3,True), (13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,2,True), (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,1,True), (24,120,0,True)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 76 +Time : 615.550s (Solving: 582.35s 1st Model: 0.01s Unsat: 12.29s) +CPU Time : 615.648s + +Choices : 13983157 (Domain: 13737812) +Conflicts : 596233 (Analyzed: 596229) +Restarts : 7110 (Average: 83.86 Last: 175) +Model-Level : 254.0 +Problems : 76 (Average Length: 82.99 Splits: 0) +Lemmas : 596229 (Deleted: 557136) + Binary : 13869 (Ratio: 2.33%) + Ternary : 3677 (Ratio: 0.62%) + Conflict : 596229 (Average Length: 497.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 596229 (Average: 21.53 Max: 1313 Sum: 12839165) + Executed : 596098 (Average: 21.52 Max: 1313 Sum: 12832839 Ratio: 99.95%) + Bounded : 131 (Average: 48.29 Max: 112 Sum: 6326 Ratio: 0.05%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 901703 (Eliminated: 0 Frozen: 278344) +Constraints : 6630520 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1037MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 3.16s +Memory: 973MB (+0MB) +UNKNOWN +Iteration Time: 3.23s + +Iteration 76 +Queue: [(12,60,3,True), (13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,2,True), (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,1,True), (24,120,0,True)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 77 +Time : 624.307s (Solving: 590.89s 1st Model: 0.01s Unsat: 12.29s) +CPU Time : 624.408s + +Choices : 14099868 (Domain: 13854097) +Conflicts : 604263 (Analyzed: 604259) +Restarts : 7210 (Average: 83.81 Last: 175) +Model-Level : 254.0 +Problems : 77 (Average Length: 83.43 Splits: 0) +Lemmas : 604259 (Deleted: 563960) + Binary : 14006 (Ratio: 2.32%) + Ternary : 3718 (Ratio: 0.62%) + Conflict : 604259 (Average Length: 493.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 604259 (Average: 21.42 Max: 1313 Sum: 12941884) + Executed : 604128 (Average: 21.41 Max: 1313 Sum: 12935558 Ratio: 99.95%) + Bounded : 131 (Average: 48.29 Max: 112 Sum: 6326 Ratio: 0.05%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 901703 (Eliminated: 0 Frozen: 278344) +Constraints : 6630520 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1037MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.68s +Memory: 973MB (+0MB) +UNKNOWN +Iteration Time: 8.76s + +Iteration 77 +Queue: [(13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,2,True), (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,1,True), (24,120,0,True)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 78 +Time : 632.869s (Solving: 599.27s 1st Model: 0.01s Unsat: 12.29s) +CPU Time : 632.976s + +Choices : 14246362 (Domain: 13999342) +Conflicts : 612492 (Analyzed: 612488) +Restarts : 7310 (Average: 83.79 Last: 175) +Model-Level : 254.0 +Problems : 78 (Average Length: 83.86 Splits: 0) +Lemmas : 612488 (Deleted: 571449) + Binary : 14232 (Ratio: 2.32%) + Ternary : 3802 (Ratio: 0.62%) + Conflict : 612488 (Average Length: 491.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 612488 (Average: 21.34 Max: 1313 Sum: 13071729) + Executed : 612357 (Average: 21.33 Max: 1313 Sum: 13065403 Ratio: 99.95%) + Bounded : 131 (Average: 48.29 Max: 112 Sum: 6326 Ratio: 0.05%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 901703 (Eliminated: 0 Frozen: 278344) +Constraints : 6630520 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1037MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.50s +Memory: 973MB (+0MB) +UNKNOWN +Iteration Time: 8.57s + +Iteration 78 +Queue: [(16,80,2,True), (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,1,True), (24,120,0,True)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 79 +Time : 646.626s (Solving: 612.84s 1st Model: 0.01s Unsat: 12.29s) +CPU Time : 646.740s + +Choices : 14610259 (Domain: 14361153) +Conflicts : 621443 (Analyzed: 621439) +Restarts : 7410 (Average: 83.86 Last: 175) +Model-Level : 254.0 +Problems : 79 (Average Length: 84.28 Splits: 0) +Lemmas : 621439 (Deleted: 580923) + Binary : 14666 (Ratio: 2.36%) + Ternary : 3901 (Ratio: 0.63%) + Conflict : 621439 (Average Length: 488.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 621439 (Average: 21.58 Max: 1313 Sum: 13412106) + Executed : 621307 (Average: 21.57 Max: 1313 Sum: 13405668 Ratio: 99.95%) + Bounded : 132 (Average: 48.77 Max: 112 Sum: 6438 Ratio: 0.05%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 901703 (Eliminated: 0 Frozen: 278344) +Constraints : 6630520 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1037MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 13.70s +Memory: 973MB (+0MB) +UNKNOWN +Iteration Time: 13.76s + +Iteration 79 +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,1,True), (24,120,0,True)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 80 +Time : 658.985s (Solving: 625.02s 1st Model: 0.01s Unsat: 12.29s) +CPU Time : 659.104s + +Choices : 14911412 (Domain: 14660787) +Conflicts : 630232 (Analyzed: 630228) +Restarts : 7510 (Average: 83.92 Last: 175) +Model-Level : 254.0 +Problems : 80 (Average Length: 84.69 Splits: 0) +Lemmas : 630228 (Deleted: 589240) + Binary : 14941 (Ratio: 2.37%) + Ternary : 3964 (Ratio: 0.63%) + Conflict : 630228 (Average Length: 486.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 630228 (Average: 21.73 Max: 1313 Sum: 13691843) + Executed : 630096 (Average: 21.72 Max: 1313 Sum: 13685405 Ratio: 99.95%) + Bounded : 132 (Average: 48.77 Max: 112 Sum: 6438 Ratio: 0.05%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 901703 (Eliminated: 0 Frozen: 278344) +Constraints : 6630520 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1037MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 12.31s +Memory: 973MB (+0MB) +UNKNOWN +Iteration Time: 12.37s + +Iteration 80 +Queue: [(18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,1,True), (24,120,0,True)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 81 +Time : 670.846s (Solving: 636.71s 1st Model: 0.01s Unsat: 12.29s) +CPU Time : 670.972s + +Choices : 15197297 (Domain: 14945608) +Conflicts : 638728 (Analyzed: 638724) +Restarts : 7610 (Average: 83.93 Last: 175) +Model-Level : 254.0 +Problems : 81 (Average Length: 85.09 Splits: 0) +Lemmas : 638724 (Deleted: 595481) + Binary : 15128 (Ratio: 2.37%) + Ternary : 4007 (Ratio: 0.63%) + Conflict : 638724 (Average Length: 483.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 638724 (Average: 21.85 Max: 1313 Sum: 13955446) + Executed : 638592 (Average: 21.84 Max: 1313 Sum: 13949008 Ratio: 99.95%) + Bounded : 132 (Average: 48.77 Max: 112 Sum: 6438 Ratio: 0.05%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 901703 (Eliminated: 0 Frozen: 278344) +Constraints : 6630520 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1037MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 11.81s +Memory: 973MB (+0MB) +UNKNOWN +Iteration Time: 11.87s + +Iteration 81 +Queue: [(23,115,1,True), (24,120,0,True)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 82 +Time : 683.609s (Solving: 649.27s 1st Model: 0.01s Unsat: 12.29s) +CPU Time : 683.740s + +Choices : 15538119 (Domain: 15285849) +Conflicts : 646852 (Analyzed: 646848) +Restarts : 7710 (Average: 83.90 Last: 175) +Model-Level : 254.0 +Problems : 82 (Average Length: 85.48 Splits: 0) +Lemmas : 646848 (Deleted: 603429) + Binary : 15323 (Ratio: 2.37%) + Ternary : 4043 (Ratio: 0.63%) + Conflict : 646848 (Average Length: 481.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 646848 (Average: 22.06 Max: 1313 Sum: 14271484) + Executed : 646716 (Average: 22.05 Max: 1313 Sum: 14265046 Ratio: 99.95%) + Bounded : 132 (Average: 48.77 Max: 112 Sum: 6438 Ratio: 0.05%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 901703 (Eliminated: 0 Frozen: 278344) +Constraints : 6630520 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1037MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 12.69s +Memory: 973MB (+0MB) +UNKNOWN +Iteration Time: 12.77s + +Iteration 82 +Queue: [(24,120,0,True)] +Grounded Until: 115 +Expected Memory: 1075.0MB +Grounding... [('step', [116]), ('step', [117]), ('step', [118]), ('step', [119]), ('step', [120]), ('check', [120])] +Grounding Time: 0.57s +Memory: 973MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 83 +Time : 698.253s (Solving: 662.61s 1st Model: 0.01s Unsat: 12.29s) +CPU Time : 698.392s + +Choices : 15771287 (Domain: 15518801) +Conflicts : 655429 (Analyzed: 655425) +Restarts : 7810 (Average: 83.92 Last: 175) +Model-Level : 254.0 +Problems : 83 (Average Length: 85.92 Splits: 0) +Lemmas : 655425 (Deleted: 611775) + Binary : 15369 (Ratio: 2.34%) + Ternary : 4053 (Ratio: 0.62%) + Conflict : 655425 (Average Length: 488.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 655425 (Average: 22.07 Max: 1313 Sum: 14463238) + Executed : 655293 (Average: 22.06 Max: 1313 Sum: 14456800 Ratio: 99.96%) + Bounded : 132 (Average: 48.77 Max: 112 Sum: 6438 Ratio: 0.04%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 941779 (Eliminated: 0 Frozen: 290794) +Constraints : 6932500 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1096MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 13.51s +Memory: 995MB (+22MB) +UNKNOWN +Iteration Time: 14.66s + +Iteration 83 +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,1,True)] +Grounded Until: 120 +Blocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 84 +Time : 703.781s (Solving: 667.94s 1st Model: 0.01s Unsat: 12.29s) +CPU Time : 703.924s + +Choices : 15805574 (Domain: 15553088) +Conflicts : 663000 (Analyzed: 662996) +Restarts : 7910 (Average: 83.82 Last: 175) +Model-Level : 254.0 +Problems : 84 (Average Length: 86.35 Splits: 0) +Lemmas : 662996 (Deleted: 619824) + Binary : 15385 (Ratio: 2.32%) + Ternary : 4058 (Ratio: 0.61%) + Conflict : 662996 (Average Length: 486.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 662996 (Average: 21.86 Max: 1313 Sum: 14489901) + Executed : 662864 (Average: 21.85 Max: 1313 Sum: 14483463 Ratio: 99.96%) + Bounded : 132 (Average: 48.77 Max: 112 Sum: 6438 Ratio: 0.04%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 941779 (Eliminated: 0 Frozen: 290794) +Constraints : 6932500 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1096MB +Max. Length : 120 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 5.46s +Memory: 995MB (+0MB) +UNKNOWN +Iteration Time: 5.53s + +Iteration 84 +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,1,True)] +Grounded Until: 120 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 85 +Time : 710.958s (Solving: 674.94s 1st Model: 0.01s Unsat: 12.29s) +CPU Time : 711.108s + +Choices : 15868523 (Domain: 15616037) +Conflicts : 671189 (Analyzed: 671185) +Restarts : 8010 (Average: 83.79 Last: 175) +Model-Level : 254.0 +Problems : 85 (Average Length: 86.76 Splits: 0) +Lemmas : 671185 (Deleted: 627106) + Binary : 15416 (Ratio: 2.30%) + Ternary : 4081 (Ratio: 0.61%) + Conflict : 671185 (Average Length: 484.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 671185 (Average: 21.67 Max: 1313 Sum: 14542116) + Executed : 671052 (Average: 21.66 Max: 1313 Sum: 14535556 Ratio: 99.95%) + Bounded : 133 (Average: 49.32 Max: 122 Sum: 6560 Ratio: 0.05%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 941779 (Eliminated: 0 Frozen: 290794) +Constraints : 6932500 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1096MB +Max. Length : 120 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.12s +Memory: 995MB (+0MB) +UNKNOWN +Iteration Time: 7.19s + +Iteration 85 +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,1,True)] +Grounded Until: 120 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 86 +Time : 720.193s (Solving: 683.94s 1st Model: 0.01s Unsat: 12.29s) +CPU Time : 720.348s + +Choices : 15998224 (Domain: 15745738) +Conflicts : 679540 (Analyzed: 679536) +Restarts : 8110 (Average: 83.79 Last: 175) +Model-Level : 254.0 +Problems : 86 (Average Length: 87.17 Splits: 0) +Lemmas : 679536 (Deleted: 634806) + Binary : 15514 (Ratio: 2.28%) + Ternary : 4107 (Ratio: 0.60%) + Conflict : 679536 (Average Length: 482.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 679536 (Average: 21.57 Max: 1313 Sum: 14659332) + Executed : 679403 (Average: 21.56 Max: 1313 Sum: 14652772 Ratio: 99.96%) + Bounded : 133 (Average: 49.32 Max: 122 Sum: 6560 Ratio: 0.04%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 941779 (Eliminated: 0 Frozen: 290794) +Constraints : 6932486 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1096MB +Max. Length : 120 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.15s +Memory: 995MB (+0MB) +UNKNOWN +Iteration Time: 9.24s + +Iteration 86 +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,1,True)] +Grounded Until: 120 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 87 +Time : 727.501s (Solving: 691.05s 1st Model: 0.01s Unsat: 12.29s) +CPU Time : 727.660s + +Choices : 16054400 (Domain: 15801914) +Conflicts : 687311 (Analyzed: 687307) +Restarts : 8210 (Average: 83.72 Last: 175) +Model-Level : 254.0 +Problems : 87 (Average Length: 87.57 Splits: 0) +Lemmas : 687307 (Deleted: 642710) + Binary : 15594 (Ratio: 2.27%) + Ternary : 4132 (Ratio: 0.60%) + Conflict : 687307 (Average Length: 480.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 687307 (Average: 21.40 Max: 1313 Sum: 14706257) + Executed : 687171 (Average: 21.39 Max: 1313 Sum: 14699336 Ratio: 99.95%) + Bounded : 136 (Average: 50.89 Max: 122 Sum: 6921 Ratio: 0.05%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 941779 (Eliminated: 0 Frozen: 290794) +Constraints : 6932486 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1096MB +Max. Length : 120 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.24s +Memory: 995MB (+0MB) +UNKNOWN +Iteration Time: 7.31s + +Iteration 87 +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,1,True)] +Grounded Until: 120 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 88 +Time : 734.932s (Solving: 698.28s 1st Model: 0.01s Unsat: 12.29s) +CPU Time : 735.096s + +Choices : 16165621 (Domain: 15911533) +Conflicts : 695340 (Analyzed: 695336) +Restarts : 8310 (Average: 83.67 Last: 175) +Model-Level : 254.0 +Problems : 88 (Average Length: 87.97 Splits: 0) +Lemmas : 695336 (Deleted: 650072) + Binary : 15737 (Ratio: 2.26%) + Ternary : 4154 (Ratio: 0.60%) + Conflict : 695336 (Average Length: 478.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 695336 (Average: 21.29 Max: 1313 Sum: 14803973) + Executed : 695200 (Average: 21.28 Max: 1313 Sum: 14797052 Ratio: 99.95%) + Bounded : 136 (Average: 50.89 Max: 122 Sum: 6921 Ratio: 0.05%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 941779 (Eliminated: 0 Frozen: 290794) +Constraints : 6932449 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1096MB +Max. Length : 120 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.37s +Memory: 995MB (+0MB) +UNKNOWN +Iteration Time: 7.44s + +Iteration 88 +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,1,True)] +Grounded Until: 120 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 89 +Time : 747.379s (Solving: 710.54s 1st Model: 0.01s Unsat: 12.29s) +CPU Time : 747.548s + +Choices : 16364648 (Domain: 16109060) +Conflicts : 703984 (Analyzed: 703980) +Restarts : 8410 (Average: 83.71 Last: 175) +Model-Level : 254.0 +Problems : 89 (Average Length: 88.35 Splits: 0) +Lemmas : 703980 (Deleted: 659522) + Binary : 16043 (Ratio: 2.28%) + Ternary : 4195 (Ratio: 0.60%) + Conflict : 703980 (Average Length: 476.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 703980 (Average: 21.29 Max: 1313 Sum: 14984301) + Executed : 703844 (Average: 21.28 Max: 1313 Sum: 14977380 Ratio: 99.95%) + Bounded : 136 (Average: 50.89 Max: 122 Sum: 6921 Ratio: 0.05%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 941779 (Eliminated: 0 Frozen: 290794) +Constraints : 6932449 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1096MB +Max. Length : 120 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 12.39s +Memory: 995MB (+0MB) +UNKNOWN +Iteration Time: 12.45s + +Iteration 89 +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,1,True)] +Grounded Until: 120 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 90 +Time : 758.875s (Solving: 721.84s 1st Model: 0.01s Unsat: 12.29s) +CPU Time : 759.048s + +Choices : 16580047 (Domain: 16322792) +Conflicts : 712296 (Analyzed: 712292) +Restarts : 8510 (Average: 83.70 Last: 175) +Model-Level : 254.0 +Problems : 90 (Average Length: 88.72 Splits: 0) +Lemmas : 712292 (Deleted: 665591) + Binary : 16346 (Ratio: 2.29%) + Ternary : 4260 (Ratio: 0.60%) + Conflict : 712292 (Average Length: 474.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 712292 (Average: 21.31 Max: 1313 Sum: 15177233) + Executed : 712156 (Average: 21.30 Max: 1313 Sum: 15170312 Ratio: 99.95%) + Bounded : 136 (Average: 50.89 Max: 122 Sum: 6921 Ratio: 0.05%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 941779 (Eliminated: 0 Frozen: 290794) +Constraints : 6932449 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1096MB +Max. Length : 120 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 11.43s +Memory: 995MB (+0MB) +UNKNOWN +Iteration Time: 11.50s + +Iteration 90 +Queue: [(19,95,2,True), (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 : 91 +Time : 773.112s (Solving: 735.88s 1st Model: 0.01s Unsat: 12.29s) +CPU Time : 773.292s + +Choices : 16853495 (Domain: 16595624) +Conflicts : 720916 (Analyzed: 720912) +Restarts : 8610 (Average: 83.73 Last: 175) +Model-Level : 254.0 +Problems : 91 (Average Length: 89.09 Splits: 0) +Lemmas : 720912 (Deleted: 675097) + Binary : 16661 (Ratio: 2.31%) + Ternary : 4309 (Ratio: 0.60%) + Conflict : 720912 (Average Length: 473.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 720912 (Average: 21.40 Max: 1313 Sum: 15425534) + Executed : 720775 (Average: 21.39 Max: 1313 Sum: 15418491 Ratio: 99.95%) + Bounded : 137 (Average: 51.41 Max: 122 Sum: 7043 Ratio: 0.05%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 941779 (Eliminated: 0 Frozen: 290794) +Constraints : 6932449 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1096MB +Max. Length : 120 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 14.17s +Memory: 995MB (+0MB) +UNKNOWN +Iteration Time: 14.25s + +Iteration 91 +Queue: [(24,120,1,True)] +Grounded Until: 120 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 92 +Time : 788.163s (Solving: 750.74s 1st Model: 0.01s Unsat: 12.29s) +CPU Time : 788.348s + +Choices : 17177392 (Domain: 16919325) +Conflicts : 729150 (Analyzed: 729146) +Restarts : 8710 (Average: 83.71 Last: 175) +Model-Level : 254.0 +Problems : 92 (Average Length: 89.45 Splits: 0) +Lemmas : 729146 (Deleted: 681441) + Binary : 16992 (Ratio: 2.33%) + Ternary : 4349 (Ratio: 0.60%) + Conflict : 729146 (Average Length: 472.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 729146 (Average: 21.56 Max: 1456 Sum: 15718597) + Executed : 729009 (Average: 21.55 Max: 1456 Sum: 15711554 Ratio: 99.96%) + Bounded : 137 (Average: 51.41 Max: 122 Sum: 7043 Ratio: 0.04%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 941779 (Eliminated: 0 Frozen: 290794) +Constraints : 6932435 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1096MB +Max. Length : 120 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 15.00s +Memory: 995MB (+0MB) +UNKNOWN +Iteration Time: 15.06s + +Iteration 92 +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 : 93 +Time : 792.979s (Solving: 755.37s 1st Model: 0.01s Unsat: 12.29s) +CPU Time : 793.168s + +Choices : 17213665 (Domain: 16955598) +Conflicts : 736679 (Analyzed: 736675) +Restarts : 8810 (Average: 83.62 Last: 175) +Model-Level : 254.0 +Problems : 93 (Average Length: 89.80 Splits: 0) +Lemmas : 736675 (Deleted: 689255) + Binary : 17005 (Ratio: 2.31%) + Ternary : 4352 (Ratio: 0.59%) + Conflict : 736675 (Average Length: 471.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 736675 (Average: 21.38 Max: 1456 Sum: 15746780) + Executed : 736538 (Average: 21.37 Max: 1456 Sum: 15739737 Ratio: 99.96%) + Bounded : 137 (Average: 51.41 Max: 122 Sum: 7043 Ratio: 0.04%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 941779 (Eliminated: 0 Frozen: 290794) +Constraints : 6932435 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1096MB +Max. Length : 120 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 4.75s +Memory: 995MB (+0MB) +UNKNOWN +Iteration Time: 4.82s + +Iteration 93 +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 : 94 +Time : 802.882s (Solving: 765.08s 1st Model: 0.01s Unsat: 12.29s) +CPU Time : 803.072s + +Choices : 17285111 (Domain: 17027044) +Conflicts : 745231 (Analyzed: 745227) +Restarts : 8910 (Average: 83.64 Last: 175) +Model-Level : 254.0 +Problems : 94 (Average Length: 90.14 Splits: 0) +Lemmas : 745227 (Deleted: 696548) + Binary : 17143 (Ratio: 2.30%) + Ternary : 4371 (Ratio: 0.59%) + Conflict : 745227 (Average Length: 474.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 745227 (Average: 21.21 Max: 1456 Sum: 15803740) + Executed : 745089 (Average: 21.20 Max: 1456 Sum: 15796575 Ratio: 99.95%) + Bounded : 138 (Average: 51.92 Max: 122 Sum: 7165 Ratio: 0.05%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 941779 (Eliminated: 0 Frozen: 290794) +Constraints : 6932435 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1096MB +Max. Length : 120 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.85s +Memory: 995MB (+0MB) +UNKNOWN +Iteration Time: 9.91s + +Iteration 94 +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 : 95 +Time : 808.597s (Solving: 770.57s 1st Model: 0.01s Unsat: 12.29s) +CPU Time : 808.792s + +Choices : 17325774 (Domain: 17067707) +Conflicts : 753155 (Analyzed: 753151) +Restarts : 9010 (Average: 83.59 Last: 175) +Model-Level : 254.0 +Problems : 95 (Average Length: 90.47 Splits: 0) +Lemmas : 753151 (Deleted: 704737) + Binary : 17170 (Ratio: 2.28%) + Ternary : 4377 (Ratio: 0.58%) + Conflict : 753151 (Average Length: 472.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 753151 (Average: 21.03 Max: 1456 Sum: 15836845) + Executed : 753009 (Average: 21.02 Max: 1456 Sum: 15829197 Ratio: 99.95%) + Bounded : 142 (Average: 53.86 Max: 122 Sum: 7648 Ratio: 0.05%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 941779 (Eliminated: 0 Frozen: 290794) +Constraints : 6932421 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1096MB +Max. Length : 120 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 5.63s +Memory: 995MB (+0MB) +UNKNOWN +Iteration Time: 5.72s + +Iteration 95 +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 : 96 +Time : 814.108s (Solving: 775.88s 1st Model: 0.01s Unsat: 12.29s) +CPU Time : 814.304s + +Choices : 17392914 (Domain: 17134799) +Conflicts : 760999 (Analyzed: 760995) +Restarts : 9110 (Average: 83.53 Last: 175) +Model-Level : 254.0 +Problems : 96 (Average Length: 90.80 Splits: 0) +Lemmas : 760995 (Deleted: 712312) + Binary : 17224 (Ratio: 2.26%) + Ternary : 4386 (Ratio: 0.58%) + Conflict : 760995 (Average Length: 470.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 760995 (Average: 20.89 Max: 1456 Sum: 15893771) + Executed : 760853 (Average: 20.88 Max: 1456 Sum: 15886123 Ratio: 99.95%) + Bounded : 142 (Average: 53.86 Max: 122 Sum: 7648 Ratio: 0.05%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 941779 (Eliminated: 0 Frozen: 290794) +Constraints : 6932379 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1096MB +Max. Length : 120 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 5.44s +Memory: 995MB (+0MB) +UNKNOWN +Iteration Time: 5.52s + +Iteration 96 +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 : 97 +Time : 825.024s (Solving: 786.61s 1st Model: 0.01s Unsat: 12.29s) +CPU Time : 825.224s + +Choices : 17539391 (Domain: 17280896) +Conflicts : 769512 (Analyzed: 769508) +Restarts : 9210 (Average: 83.55 Last: 175) +Model-Level : 254.0 +Problems : 97 (Average Length: 91.12 Splits: 0) +Lemmas : 769508 (Deleted: 719799) + Binary : 17400 (Ratio: 2.26%) + Ternary : 4417 (Ratio: 0.57%) + Conflict : 769508 (Average Length: 469.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 769508 (Average: 20.82 Max: 1456 Sum: 16023834) + Executed : 769366 (Average: 20.81 Max: 1456 Sum: 16016186 Ratio: 99.95%) + Bounded : 142 (Average: 53.86 Max: 122 Sum: 7648 Ratio: 0.05%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 941779 (Eliminated: 0 Frozen: 290794) +Constraints : 6932379 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1096MB +Max. Length : 120 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 10.85s +Memory: 995MB (+0MB) +UNKNOWN +Iteration Time: 10.92s + +Iteration 97 +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 : 98 +Time : 836.489s (Solving: 797.87s 1st Model: 0.01s Unsat: 12.29s) +CPU Time : 836.692s + +Choices : 17691327 (Domain: 17431589) +Conflicts : 778275 (Analyzed: 778271) +Restarts : 9310 (Average: 83.60 Last: 191) +Model-Level : 254.0 +Problems : 98 (Average Length: 91.44 Splits: 0) +Lemmas : 778271 (Deleted: 729623) + Binary : 17589 (Ratio: 2.26%) + Ternary : 4447 (Ratio: 0.57%) + Conflict : 778271 (Average Length: 469.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 778271 (Average: 20.76 Max: 1456 Sum: 16157004) + Executed : 778128 (Average: 20.75 Max: 1456 Sum: 16149234 Ratio: 99.95%) + Bounded : 143 (Average: 54.34 Max: 122 Sum: 7770 Ratio: 0.05%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 941779 (Eliminated: 0 Frozen: 290794) +Constraints : 6932379 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1096MB +Max. Length : 120 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 11.40s +Memory: 995MB (+0MB) +UNKNOWN +Iteration Time: 11.47s + +Iteration 98 +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 : 99 +Time : 845.821s (Solving: 807.01s 1st Model: 0.01s Unsat: 12.29s) +CPU Time : 846.028s + +Choices : 17782307 (Domain: 17522479) +Conflicts : 786276 (Analyzed: 786272) +Restarts : 9410 (Average: 83.56 Last: 191) +Model-Level : 254.0 +Problems : 99 (Average Length: 91.75 Splits: 0) +Lemmas : 786272 (Deleted: 736243) + Binary : 17666 (Ratio: 2.25%) + Ternary : 4462 (Ratio: 0.57%) + Conflict : 786272 (Average Length: 469.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 786272 (Average: 20.64 Max: 1456 Sum: 16231550) + Executed : 786129 (Average: 20.63 Max: 1456 Sum: 16223780 Ratio: 99.95%) + Bounded : 143 (Average: 54.34 Max: 122 Sum: 7770 Ratio: 0.05%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 941779 (Eliminated: 0 Frozen: 290794) +Constraints : 6932366 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1096MB +Max. Length : 120 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.27s +Memory: 995MB (+0MB) +UNKNOWN +Iteration Time: 9.34s + +Iteration 99 +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 : 100 +Time : 856.441s (Solving: 817.44s 1st Model: 0.01s Unsat: 12.29s) +CPU Time : 856.652s + +Choices : 17955240 (Domain: 17695244) +Conflicts : 794744 (Analyzed: 794740) +Restarts : 9510 (Average: 83.57 Last: 191) +Model-Level : 254.0 +Problems : 100 (Average Length: 92.05 Splits: 0) +Lemmas : 794740 (Deleted: 744000) + Binary : 17814 (Ratio: 2.24%) + Ternary : 4493 (Ratio: 0.57%) + Conflict : 794740 (Average Length: 469.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 794740 (Average: 20.62 Max: 1456 Sum: 16385032) + Executed : 794597 (Average: 20.61 Max: 1456 Sum: 16377262 Ratio: 99.95%) + Bounded : 143 (Average: 54.34 Max: 122 Sum: 7770 Ratio: 0.05%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 941779 (Eliminated: 0 Frozen: 290794) +Constraints : 6932366 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1096MB +Max. Length : 120 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 10.56s +Memory: 995MB (+0MB) +UNKNOWN +Iteration Time: 10.63s + +Iteration 100 +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 : 101 +Time : 865.659s (Solving: 826.47s 1st Model: 0.01s Unsat: 12.29s) +CPU Time : 865.876s + +Choices : 18127019 (Domain: 17866821) +Conflicts : 803129 (Analyzed: 803125) +Restarts : 9610 (Average: 83.57 Last: 191) +Model-Level : 254.0 +Problems : 101 (Average Length: 92.35 Splits: 0) +Lemmas : 803125 (Deleted: 751967) + Binary : 17915 (Ratio: 2.23%) + Ternary : 4518 (Ratio: 0.56%) + Conflict : 803125 (Average Length: 469.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 803125 (Average: 20.59 Max: 1456 Sum: 16535251) + Executed : 802982 (Average: 20.58 Max: 1456 Sum: 16527481 Ratio: 99.95%) + Bounded : 143 (Average: 54.34 Max: 122 Sum: 7770 Ratio: 0.05%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 941779 (Eliminated: 0 Frozen: 290794) +Constraints : 6932366 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1096MB +Max. Length : 120 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.16s +Memory: 995MB (+0MB) +UNKNOWN +Iteration Time: 9.22s + +Iteration 101 +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 : 102 +Time : 871.761s (Solving: 832.37s 1st Model: 0.01s Unsat: 12.29s) +CPU Time : 871.980s + +Choices : 18163656 (Domain: 17903458) +Conflicts : 810860 (Analyzed: 810856) +Restarts : 9710 (Average: 83.51 Last: 191) +Model-Level : 254.0 +Problems : 102 (Average Length: 92.64 Splits: 0) +Lemmas : 810856 (Deleted: 760191) + Binary : 17945 (Ratio: 2.21%) + Ternary : 4524 (Ratio: 0.56%) + Conflict : 810856 (Average Length: 468.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 810856 (Average: 20.43 Max: 1456 Sum: 16563240) + Executed : 810713 (Average: 20.42 Max: 1456 Sum: 16555470 Ratio: 99.95%) + Bounded : 143 (Average: 54.34 Max: 122 Sum: 7770 Ratio: 0.05%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 941779 (Eliminated: 0 Frozen: 290794) +Constraints : 6932366 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1096MB +Max. Length : 120 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.03s +Memory: 995MB (+0MB) +UNKNOWN +Iteration Time: 6.11s + +Iteration 102 +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 : 103 +Time : 887.554s (Solving: 847.97s 1st Model: 0.01s Unsat: 12.29s) +CPU Time : 887.776s + +Choices : 18241294 (Domain: 17981096) +Conflicts : 819330 (Analyzed: 819326) +Restarts : 9810 (Average: 83.52 Last: 191) +Model-Level : 254.0 +Problems : 103 (Average Length: 92.92 Splits: 0) +Lemmas : 819326 (Deleted: 767691) + Binary : 17983 (Ratio: 2.19%) + Ternary : 4533 (Ratio: 0.55%) + Conflict : 819326 (Average Length: 481.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 819326 (Average: 20.29 Max: 1456 Sum: 16625112) + Executed : 819183 (Average: 20.28 Max: 1456 Sum: 16617342 Ratio: 99.95%) + Bounded : 143 (Average: 54.34 Max: 122 Sum: 7770 Ratio: 0.05%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 941779 (Eliminated: 0 Frozen: 290794) +Constraints : 6932366 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1096MB +Max. Length : 120 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 15.74s +Memory: 995MB (+0MB) +UNKNOWN +Iteration Time: 15.80s + +Iteration 103 +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... +*** Info : (planner): INTERRUPTED by signal! +UNKNOWN + +INTERRUPTED : 1 + +Models : 0+ +Calls : 104 +Time : 892.536s (Solving: 852.76s 1st Model: 0.01s Unsat: 12.29s) +CPU Time : 892.740s + +Choices : 18282206 (Domain: 18022008) +Conflicts : 825524 (Analyzed: 825520) +Restarts : 9894 (Average: 83.44 Last: 191) +Model-Level : 254.0 +Problems : 104 (Average Length: 93.20 Splits: 0) +Lemmas : 825520 (Deleted: 772098) + Binary : 17989 (Ratio: 2.18%) + Ternary : 4538 (Ratio: 0.55%) + Conflict : 825520 (Average Length: 480.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 825520 (Average: 20.18 Max: 1456 Sum: 16658548) + Executed : 825377 (Average: 20.17 Max: 1456 Sum: 16650778 Ratio: 99.95%) + Bounded : 143 (Average: 54.34 Max: 122 Sum: 7770 Ratio: 0.05%) + +Rules : 160595 (Original: 145100) +Atoms : 77287 +Bodies : 70054 (Original: 54558) + Count : 890 (Original: 2504) +Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) +Tight : Yes +Variables : 941779 (Eliminated: 0 Frozen: 290794) +Constraints : 6932366 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1096MB +Max. Length : 120 steps +Models : 1 + +