From 3a496782ffc5847e3352de9262d207e4f06106b7 Mon Sep 17 00:00:00 2001 From: potassco-bot Date: Fri, 2 Feb 2018 16:25:09 +0100 Subject: [PATCH] Add benchmark result [gc-ta1-tt1 | ipc-2011 | barman-sequential-satisficing | 20] --- ...-2011_barman-sequential-satisficing_20.env | 54 + ...-2011_barman-sequential-satisficing_20.err | 8 + ...-2011_barman-sequential-satisficing_20.out | 4801 +++++++++++++++++ 3 files changed, 4863 insertions(+) create mode 100644 gc-ta1-tt1/ipc-2011_barman-sequential-satisficing_20.env create mode 100644 gc-ta1-tt1/ipc-2011_barman-sequential-satisficing_20.err create mode 100644 gc-ta1-tt1/ipc-2011_barman-sequential-satisficing_20.out diff --git a/gc-ta1-tt1/ipc-2011_barman-sequential-satisficing_20.env b/gc-ta1-tt1/ipc-2011_barman-sequential-satisficing_20.env new file mode 100644 index 000000000..d4284aa16 --- /dev/null +++ b/gc-ta1-tt1/ipc-2011_barman-sequential-satisficing_20.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-20.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: 20 + 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_20.err b/gc-ta1-tt1/ipc-2011_barman-sequential-satisficing_20.err new file mode 100644 index 000000000..f7313a2c7 --- /dev/null +++ b/gc-ta1-tt1/ipc-2011_barman-sequential-satisficing_20.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': 20} +# 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-20.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.02 MEM 1037316 MAXMEM 1135032 STALE 0 MAXMEM_RSS 976280 + + diff --git a/gc-ta1-tt1/ipc-2011_barman-sequential-satisficing_20.out b/gc-ta1-tt1/ipc-2011_barman-sequential-satisficing_20.out new file mode 100644 index 000000000..39c7bc3e7 --- /dev/null +++ b/gc-ta1-tt1/ipc-2011_barman-sequential-satisficing_20.out @@ -0,0 +1,4801 @@ +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-20.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-20.pddl +Parsing... +Parsing: [0.040s CPU, 0.043s wall-clock] +Normalizing task... [0.000s CPU, 0.003s wall-clock] +Instantiating... +Generating Datalog program... [0.010s CPU, 0.012s wall-clock] +Normalizing Datalog program... +Normalizing Datalog program: [0.050s CPU, 0.053s wall-clock] +Preparing model... [0.030s CPU, 0.030s wall-clock] +Generated 115 rules. +Computing model... [0.540s CPU, 0.544s wall-clock] +3296 relevant atoms +3425 auxiliary atoms +6721 final queue length +11595 total queue pushes +Completing instantiation... [1.030s CPU, 1.030s wall-clock] +Instantiating: [1.680s CPU, 1.676s 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.014s wall-clock] +Computing fact groups: [0.190s CPU, 0.197s 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.056s wall-clock] +Translating task: [1.060s CPU, 1.070s 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.591s 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.379s 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.370s CPU, 0.407s wall-clock] +Done! [4.380s CPU, 4.422s wall-clock] +planner.py version 0.0.1 + +Time: 0.92s +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.109s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s) +CPU Time : 0.924s + +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.28s +Memory: 183MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 1+ +Calls : 2 +Time : 1.543s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s) +CPU Time : 1.360s + +Choices : 195 (Domain: 36) +Conflicts : 4 (Analyzed: 4) +Restarts : 0 +Model-Level : 183.0 +Problems : 2 (Average Length: 4.50 Splits: 0) +Lemmas : 4 (Deleted: 0) + Binary : 2 (Ratio: 50.00%) + Ternary : 0 (Ratio: 0.00%) + Conflict : 4 (Average Length: 16.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 4 (Average: 5.00 Max: 16 Sum: 20) + Executed : 3 (Average: 4.75 Max: 16 Sum: 19 Ratio: 95.00%) + Bounded : 1 (Average: 1.00 Max: 1 Sum: 1 Ratio: 5.00%) + +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 : 1 + +[endof: stats after solve call] +Solving Time: 0.02s +Memory: 187MB (+4MB) +SAT +Testing... +NOT SERIALIZABLE +Testing Time: 1.00s +Memory: 218MB (+31MB) +Solving... +[start: stats after solve call] + +Models : 0 +Calls : 3 +Time : 1.696s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s) +CPU Time : 1.516s + +Choices : 212 (Domain: 37) +Conflicts : 13 (Analyzed: 12) +Restarts : 0 +Model-Level : 183.0 +Problems : 3 (Average Length: 5.33 Splits: 0) +Lemmas : 12 (Deleted: 0) + Binary : 4 (Ratio: 33.33%) + Ternary : 4 (Ratio: 33.33%) + Conflict : 12 (Average Length: 7.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 12 (Average: 3.25 Max: 16 Sum: 39) + Executed : 9 (Average: 3.00 Max: 16 Sum: 36 Ratio: 92.31%) + Bounded : 3 (Average: 1.00 Max: 1 Sum: 3 Ratio: 7.69%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 21236 (Eliminated: 0 Frozen: 4444) +Constraints : 86170 (Binary: 92.4% Ternary: 5.4% Other: 2.2%) + +Memory Peak : 247MB +Max. Length : 0 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 0.02s +Memory: 218MB (+0MB) +UNSAT +Iteration Time: 1.46s + +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: 222.0MB +Grounding... [('step', [6]), ('step', [7]), ('step', [8]), ('step', [9]), ('step', [10]), ('check', [10])] +Grounding Time: 0.55s +Memory: 218MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0 +Calls : 4 +Time : 3.582s (Solving: 1.11s 1st Model: 0.00s Unsat: 1.11s) +CPU Time : 3.408s + +Choices : 36338 (Domain: 29490) +Conflicts : 3123 (Analyzed: 3121) +Restarts : 36 (Average: 86.69 Last: 26) +Model-Level : 183.0 +Problems : 4 (Average Length: 7.00 Splits: 0) +Lemmas : 3121 (Deleted: 570) + Binary : 325 (Ratio: 10.41%) + Ternary : 504 (Ratio: 16.15%) + Conflict : 3121 (Average Length: 42.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 3121 (Average: 11.58 Max: 265 Sum: 36155) + Executed : 3080 (Average: 11.44 Max: 265 Sum: 35707 Ratio: 98.76%) + Bounded : 41 (Average: 10.93 Max: 12 Sum: 448 Ratio: 1.24%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 61312 (Eliminated: 0 Frozen: 16894) +Constraints : 388150 (Binary: 91.5% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 247MB +Max. Length : 5 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 1.14s +Memory: 230MB (+12MB) +UNSAT +Iteration Time: 1.89s + +Iteration 4 +Queue: [(3,15,0,True), (4,20,0,True), (5,25,0,True), (6,30,0,True)] +Grounded Until: 10 +Expected Memory: 242.0MB +Grounding... [('step', [11]), ('step', [12]), ('step', [13]), ('step', [14]), ('step', [15]), ('check', [15])] +Grounding Time: 0.53s +Memory: 242MB (+12MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 5 +Time : 8.918s (Solving: 5.65s 1st Model: 0.00s Unsat: 1.11s) +CPU Time : 8.748s + +Choices : 115133 (Domain: 89050) +Conflicts : 12082 (Analyzed: 12080) +Restarts : 136 (Average: 88.82 Last: 101) +Model-Level : 183.0 +Problems : 5 (Average Length: 9.00 Splits: 0) +Lemmas : 12080 (Deleted: 7160) + Binary : 775 (Ratio: 6.42%) + Ternary : 845 (Ratio: 7.00%) + Conflict : 12080 (Average Length: 130.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 12080 (Average: 9.19 Max: 265 Sum: 110997) + Executed : 12022 (Average: 9.13 Max: 265 Sum: 110262 Ratio: 99.34%) + Bounded : 58 (Average: 12.67 Max: 17 Sum: 735 Ratio: 0.66%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 101388 (Eliminated: 0 Frozen: 29344) +Constraints : 645808 (Binary: 91.4% Ternary: 6.7% Other: 1.9%) + +Memory Peak : 262MB +Max. Length : 10 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 4.58s +Memory: 262MB (+20MB) +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: 294.0MB +Grounding... [('step', [16]), ('step', [17]), ('step', [18]), ('step', [19]), ('step', [20]), ('check', [20])] +Grounding Time: 0.64s +Memory: 276MB (+14MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 6 +Time : 14.138s (Solving: 9.94s 1st Model: 0.00s Unsat: 1.11s) +CPU Time : 13.968s + +Choices : 157868 (Domain: 131138) +Conflicts : 19485 (Analyzed: 19483) +Restarts : 236 (Average: 82.56 Last: 101) +Model-Level : 183.0 +Problems : 6 (Average Length: 11.17 Splits: 0) +Lemmas : 19483 (Deleted: 13053) + Binary : 1076 (Ratio: 5.52%) + Ternary : 912 (Ratio: 4.68%) + Conflict : 19483 (Average Length: 181.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 19483 (Average: 7.64 Max: 265 Sum: 148779) + Executed : 19423 (Average: 7.60 Max: 265 Sum: 148003 Ratio: 99.48%) + Bounded : 60 (Average: 12.93 Max: 22 Sum: 776 Ratio: 0.52%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 141464 (Eliminated: 0 Frozen: 41794) +Constraints : 941310 (Binary: 91.3% Ternary: 6.8% Other: 1.9%) + +Memory Peak : 302MB +Max. Length : 15 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 4.33s +Memory: 302MB (+26MB) +UNKNOWN +Iteration Time: 5.23s + +Iteration 6 +Queue: [(5,25,0,True), (6,30,0,True)] +Grounded Until: 20 +Expected Memory: 342.0MB +Grounding... [('step', [21]), ('step', [22]), ('step', [23]), ('step', [24]), ('step', [25]), ('check', [25])] +Grounding Time: 0.54s +Memory: 308MB (+6MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 7 +Time : 20.394s (Solving: 15.35s 1st Model: 0.00s Unsat: 1.11s) +CPU Time : 20.224s + +Choices : 331212 (Domain: 285212) +Conflicts : 28062 (Analyzed: 28060) +Restarts : 336 (Average: 83.51 Last: 131) +Model-Level : 183.0 +Problems : 7 (Average Length: 13.43 Splits: 0) +Lemmas : 28060 (Deleted: 18557) + Binary : 1903 (Ratio: 6.78%) + Ternary : 1288 (Ratio: 4.59%) + Conflict : 28060 (Average Length: 175.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 28060 (Average: 11.25 Max: 782 Sum: 315796) + Executed : 27986 (Average: 11.21 Max: 782 Sum: 314642 Ratio: 99.63%) + Bounded : 74 (Average: 15.59 Max: 27 Sum: 1154 Ratio: 0.37%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 181540 (Eliminated: 0 Frozen: 54244) +Constraints : 1240231 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 336MB +Max. Length : 20 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 5.47s +Memory: 322MB (+14MB) +UNKNOWN +Iteration Time: 6.27s + +Iteration 7 +Queue: [(6,30,0,True)] +Grounded Until: 25 +Expected Memory: 362.0MB +Grounding... [('step', [26]), ('step', [27]), ('step', [28]), ('step', [29]), ('step', [30]), ('check', [30])] +Grounding Time: 0.58s +Memory: 334MB (+12MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 8 +Time : 27.275s (Solving: 21.30s 1st Model: 0.00s Unsat: 1.11s) +CPU Time : 27.108s + +Choices : 464738 (Domain: 402252) +Conflicts : 36744 (Analyzed: 36742) +Restarts : 436 (Average: 84.27 Last: 131) +Model-Level : 183.0 +Problems : 8 (Average Length: 15.75 Splits: 0) +Lemmas : 36742 (Deleted: 27143) + Binary : 2231 (Ratio: 6.07%) + Ternary : 1421 (Ratio: 3.87%) + Conflict : 36742 (Average Length: 201.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 36742 (Average: 11.94 Max: 782 Sum: 438868) + Executed : 36653 (Average: 11.90 Max: 782 Sum: 437244 Ratio: 99.63%) + Bounded : 89 (Average: 18.25 Max: 32 Sum: 1624 Ratio: 0.37%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 221616 (Eliminated: 0 Frozen: 66694) +Constraints : 1520780 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 368MB +Max. Length : 25 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.02s +Memory: 368MB (+34MB) +UNKNOWN +Iteration Time: 6.89s + +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 : 28.615s (Solving: 22.59s 1st Model: 0.00s Unsat: 2.40s) +CPU Time : 28.448s + +Choices : 467550 (Domain: 405060) +Conflicts : 37906 (Analyzed: 37903) +Restarts : 450 (Average: 84.23 Last: 131) +Model-Level : 183.0 +Problems : 9 (Average Length: 17.56 Splits: 0) +Lemmas : 37903 (Deleted: 27143) + Binary : 2261 (Ratio: 5.97%) + Ternary : 1439 (Ratio: 3.80%) + Conflict : 37903 (Average Length: 202.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 37903 (Average: 11.65 Max: 782 Sum: 441640) + Executed : 37813 (Average: 11.61 Max: 782 Sum: 440015 Ratio: 99.63%) + Bounded : 90 (Average: 18.06 Max: 32 Sum: 1625 Ratio: 0.37%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 221616 (Eliminated: 0 Frozen: 66694) +Constraints : 1503174 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 368MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 1.32s +Memory: 368MB (+0MB) +UNSAT +Iteration Time: 1.34s + +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 : 34.297s (Solving: 28.21s 1st Model: 0.00s Unsat: 2.40s) +CPU Time : 34.132s + +Choices : 529904 (Domain: 452412) +Conflicts : 46631 (Analyzed: 46628) +Restarts : 550 (Average: 84.78 Last: 131) +Model-Level : 183.0 +Problems : 10 (Average Length: 19.00 Splits: 0) +Lemmas : 46628 (Deleted: 36484) + Binary : 2472 (Ratio: 5.30%) + Ternary : 1508 (Ratio: 3.23%) + Conflict : 46628 (Average Length: 244.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 46628 (Average: 10.67 Max: 782 Sum: 497348) + Executed : 46537 (Average: 10.63 Max: 782 Sum: 495696 Ratio: 99.67%) + Bounded : 91 (Average: 18.15 Max: 32 Sum: 1652 Ratio: 0.33%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 221616 (Eliminated: 0 Frozen: 66694) +Constraints : 1503174 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 368MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 5.66s +Memory: 368MB (+0MB) +UNKNOWN +Iteration Time: 5.69s + +Iteration 10 +Queue: [(5,25,1,True), (6,30,1,True), (7,35,0,True), (8,40,0,True), (9,45,0,True), (10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True)] +Grounded Until: 30 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 11 +Time : 41.774s (Solving: 35.64s 1st Model: 0.00s Unsat: 2.40s) +CPU Time : 41.612s + +Choices : 633897 (Domain: 541048) +Conflicts : 55908 (Analyzed: 55905) +Restarts : 650 (Average: 86.01 Last: 131) +Model-Level : 183.0 +Problems : 11 (Average Length: 20.18 Splits: 0) +Lemmas : 55905 (Deleted: 42997) + Binary : 3035 (Ratio: 5.43%) + Ternary : 1728 (Ratio: 3.09%) + Conflict : 55905 (Average Length: 289.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 55905 (Average: 10.58 Max: 782 Sum: 591368) + Executed : 55806 (Average: 10.54 Max: 782 Sum: 589465 Ratio: 99.68%) + Bounded : 99 (Average: 19.22 Max: 32 Sum: 1903 Ratio: 0.32%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 221616 (Eliminated: 0 Frozen: 66694) +Constraints : 1503174 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 368MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.46s +Memory: 368MB (+0MB) +UNKNOWN +Iteration Time: 7.48s + +Iteration 11 +Queue: [(6,30,1,True), (7,35,0,True), (8,40,0,True), (9,45,0,True), (10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True)] +Grounded Until: 30 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 12 +Time : 49.815s (Solving: 43.63s 1st Model: 0.00s Unsat: 2.40s) +CPU Time : 49.656s + +Choices : 743498 (Domain: 635142) +Conflicts : 65194 (Analyzed: 65191) +Restarts : 750 (Average: 86.92 Last: 131) +Model-Level : 183.0 +Problems : 12 (Average Length: 21.17 Splits: 0) +Lemmas : 65191 (Deleted: 51200) + Binary : 3305 (Ratio: 5.07%) + Ternary : 1857 (Ratio: 2.85%) + Conflict : 65191 (Average Length: 330.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 65191 (Average: 10.52 Max: 782 Sum: 685498) + Executed : 65090 (Average: 10.49 Max: 782 Sum: 683531 Ratio: 99.71%) + Bounded : 101 (Average: 19.48 Max: 32 Sum: 1967 Ratio: 0.29%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 221616 (Eliminated: 0 Frozen: 66694) +Constraints : 1497569 (Binary: 91.3% Ternary: 6.8% Other: 1.9%) + +Memory Peak : 368MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.03s +Memory: 368MB (+0MB) +UNKNOWN +Iteration Time: 8.05s + +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: 414.0MB +Grounding... [('step', [31]), ('step', [32]), ('step', [33]), ('step', [34]), ('step', [35]), ('check', [35])] +Grounding Time: 0.56s +Memory: 368MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 13 +Time : 59.310s (Solving: 52.21s 1st Model: 0.00s Unsat: 2.40s) +CPU Time : 59.156s + +Choices : 881351 (Domain: 756871) +Conflicts : 74031 (Analyzed: 74028) +Restarts : 850 (Average: 87.09 Last: 157) +Model-Level : 183.0 +Problems : 13 (Average Length: 22.38 Splits: 0) +Lemmas : 74028 (Deleted: 59920) + Binary : 3488 (Ratio: 4.71%) + Ternary : 1914 (Ratio: 2.59%) + Conflict : 74028 (Average Length: 407.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 74028 (Average: 10.85 Max: 782 Sum: 803239) + Executed : 73919 (Average: 10.82 Max: 782 Sum: 800976 Ratio: 99.72%) + Bounded : 109 (Average: 20.76 Max: 37 Sum: 2263 Ratio: 0.28%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 261692 (Eliminated: 0 Frozen: 79144) +Constraints : 1799341 (Binary: 91.3% Ternary: 6.9% Other: 1.8%) + +Memory Peak : 405MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.65s +Memory: 381MB (+13MB) +UNKNOWN +Iteration Time: 9.51s + +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: 427.0MB +Grounding... [('step', [36]), ('step', [37]), ('step', [38]), ('step', [39]), ('step', [40]), ('check', [40])] +Grounding Time: 0.57s +Memory: 392MB (+11MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 14 +Time : 68.733s (Solving: 60.68s 1st Model: 0.00s Unsat: 2.40s) +CPU Time : 68.584s + +Choices : 1039739 (Domain: 899452) +Conflicts : 82621 (Analyzed: 82618) +Restarts : 950 (Average: 86.97 Last: 157) +Model-Level : 183.0 +Problems : 14 (Average Length: 23.79 Splits: 0) +Lemmas : 82618 (Deleted: 66758) + Binary : 3639 (Ratio: 4.40%) + Ternary : 1978 (Ratio: 2.39%) + Conflict : 82618 (Average Length: 425.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 82618 (Average: 11.38 Max: 782 Sum: 940232) + Executed : 82507 (Average: 11.35 Max: 782 Sum: 937886 Ratio: 99.75%) + Bounded : 111 (Average: 21.14 Max: 42 Sum: 2346 Ratio: 0.25%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 301768 (Eliminated: 0 Frozen: 91594) +Constraints : 2101210 (Binary: 91.3% Ternary: 6.9% Other: 1.8%) + +Memory Peak : 436MB +Max. Length : 35 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.55s +Memory: 407MB (+15MB) +UNKNOWN +Iteration Time: 9.44s + +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: 453.0MB +Grounding... [('step', [41]), ('step', [42]), ('step', [43]), ('step', [44]), ('step', [45]), ('check', [45])] +Grounding Time: 0.72s +Memory: 431MB (+24MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 15 +Time : 79.407s (Solving: 70.22s 1st Model: 0.00s Unsat: 2.40s) +CPU Time : 79.264s + +Choices : 1223417 (Domain: 1070592) +Conflicts : 91188 (Analyzed: 91185) +Restarts : 1050 (Average: 86.84 Last: 157) +Model-Level : 183.0 +Problems : 15 (Average Length: 25.33 Splits: 0) +Lemmas : 91185 (Deleted: 74522) + Binary : 3852 (Ratio: 4.22%) + Ternary : 2045 (Ratio: 2.24%) + Conflict : 91185 (Average Length: 444.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 91185 (Average: 12.09 Max: 794 Sum: 1102182) + Executed : 91068 (Average: 12.06 Max: 794 Sum: 1099554 Ratio: 99.76%) + Bounded : 117 (Average: 22.46 Max: 47 Sum: 2628 Ratio: 0.24%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 341844 (Eliminated: 0 Frozen: 104044) +Constraints : 2403164 (Binary: 91.3% Ternary: 6.9% Other: 1.8%) + +Memory Peak : 482MB +Max. Length : 40 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.63s +Memory: 481MB (+50MB) +UNKNOWN +Iteration Time: 10.69s + +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: 555.0MB +Grounding... [('step', [46]), ('step', [47]), ('step', [48]), ('step', [49]), ('step', [50]), ('check', [50])] +Grounding Time: 0.60s +Memory: 481MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 16 +Time : 90.472s (Solving: 80.24s 1st Model: 0.00s Unsat: 2.40s) +CPU Time : 90.336s + +Choices : 1429024 (Domain: 1264883) +Conflicts : 100027 (Analyzed: 100024) +Restarts : 1150 (Average: 86.98 Last: 157) +Model-Level : 183.0 +Problems : 16 (Average Length: 27.00 Splits: 0) +Lemmas : 100024 (Deleted: 84018) + Binary : 3987 (Ratio: 3.99%) + Ternary : 2087 (Ratio: 2.09%) + Conflict : 100024 (Average Length: 472.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 100024 (Average: 12.81 Max: 794 Sum: 1281367) + Executed : 99905 (Average: 12.78 Max: 794 Sum: 1278640 Ratio: 99.79%) + Bounded : 119 (Average: 22.92 Max: 52 Sum: 2727 Ratio: 0.21%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 381920 (Eliminated: 0 Frozen: 116494) +Constraints : 2702017 (Binary: 91.3% Ternary: 6.9% Other: 1.8%) + +Memory Peak : 527MB +Max. Length : 45 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 10.12s +Memory: 490MB (+9MB) +UNKNOWN +Iteration Time: 11.08s + +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: 564.0MB +Grounding... [('step', [51]), ('step', [52]), ('step', [53]), ('step', [54]), ('step', [55]), ('check', [55])] +Grounding Time: 0.57s +Memory: 493MB (+3MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 17 +Time : 100.209s (Solving: 88.95s 1st Model: 0.00s Unsat: 2.40s) +CPU Time : 100.076s + +Choices : 1577246 (Domain: 1405775) +Conflicts : 108978 (Analyzed: 108975) +Restarts : 1250 (Average: 87.18 Last: 157) +Model-Level : 183.0 +Problems : 17 (Average Length: 28.76 Splits: 0) +Lemmas : 108975 (Deleted: 93155) + Binary : 4109 (Ratio: 3.77%) + Ternary : 2118 (Ratio: 1.94%) + Conflict : 108975 (Average Length: 513.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 108975 (Average: 12.71 Max: 794 Sum: 1384883) + Executed : 108856 (Average: 12.68 Max: 794 Sum: 1382156 Ratio: 99.80%) + Bounded : 119 (Average: 22.92 Max: 52 Sum: 2727 Ratio: 0.20%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 421996 (Eliminated: 0 Frozen: 128944) +Constraints : 3003983 (Binary: 91.3% Ternary: 6.9% Other: 1.8%) + +Memory Peak : 552MB +Max. Length : 50 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.80s +Memory: 513MB (+20MB) +UNKNOWN +Iteration Time: 9.75s + +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: 587.0MB +Grounding... [('step', [56]), ('step', [57]), ('step', [58]), ('step', [59]), ('step', [60]), ('check', [60])] +Grounding Time: 0.56s +Memory: 518MB (+5MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 18 +Time : 110.217s (Solving: 97.92s 1st Model: 0.00s Unsat: 2.40s) +CPU Time : 110.088s + +Choices : 1776257 (Domain: 1595430) +Conflicts : 117090 (Analyzed: 117087) +Restarts : 1350 (Average: 86.73 Last: 157) +Model-Level : 183.0 +Problems : 18 (Average Length: 30.61 Splits: 0) +Lemmas : 117087 (Deleted: 99028) + Binary : 4216 (Ratio: 3.60%) + Ternary : 2159 (Ratio: 1.84%) + Conflict : 117087 (Average Length: 523.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 117087 (Average: 13.30 Max: 910 Sum: 1557696) + Executed : 116968 (Average: 13.28 Max: 910 Sum: 1554969 Ratio: 99.82%) + Bounded : 119 (Average: 22.92 Max: 52 Sum: 2727 Ratio: 0.18%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 462072 (Eliminated: 0 Frozen: 141394) +Constraints : 3305963 (Binary: 91.2% Ternary: 6.9% Other: 1.8%) + +Memory Peak : 586MB +Max. Length : 55 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.07s +Memory: 542MB (+24MB) +UNKNOWN +Iteration Time: 10.02s + +Iteration 18 +Queue: [(13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True)] +Grounded Until: 60 +Expected Memory: 616.0MB +Grounding... [('step', [61]), ('step', [62]), ('step', [63]), ('step', [64]), ('step', [65]), ('check', [65])] +Grounding Time: 0.56s +Memory: 549MB (+7MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 19 +Time : 120.307s (Solving: 106.94s 1st Model: 0.00s Unsat: 2.40s) +CPU Time : 120.184s + +Choices : 1952515 (Domain: 1767971) +Conflicts : 125373 (Analyzed: 125370) +Restarts : 1450 (Average: 86.46 Last: 157) +Model-Level : 183.0 +Problems : 19 (Average Length: 32.53 Splits: 0) +Lemmas : 125370 (Deleted: 107415) + Binary : 4297 (Ratio: 3.43%) + Ternary : 2186 (Ratio: 1.74%) + Conflict : 125370 (Average Length: 544.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 125370 (Average: 13.53 Max: 910 Sum: 1696732) + Executed : 125248 (Average: 13.51 Max: 910 Sum: 1693804 Ratio: 99.83%) + Bounded : 122 (Average: 24.00 Max: 67 Sum: 2928 Ratio: 0.17%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 502148 (Eliminated: 0 Frozen: 153844) +Constraints : 3607943 (Binary: 91.2% Ternary: 6.9% Other: 1.8%) + +Memory Peak : 618MB +Max. Length : 60 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.13s +Memory: 610MB (+61MB) +UNKNOWN +Iteration Time: 10.11s + +Iteration 19 +Queue: [(14,70,0,True), (15,75,0,True), (16,80,0,True)] +Grounded Until: 65 +Expected Memory: 684.0MB +Grounding... [('step', [66]), ('step', [67]), ('step', [68]), ('step', [69]), ('step', [70]), ('check', [70])] +Grounding Time: 0.56s +Memory: 610MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 20 +Time : 130.946s (Solving: 116.50s 1st Model: 0.00s Unsat: 2.40s) +CPU Time : 130.828s + +Choices : 2197548 (Domain: 2008753) +Conflicts : 133633 (Analyzed: 133630) +Restarts : 1550 (Average: 86.21 Last: 157) +Model-Level : 183.0 +Problems : 20 (Average Length: 34.50 Splits: 0) +Lemmas : 133630 (Deleted: 114772) + Binary : 4403 (Ratio: 3.29%) + Ternary : 2221 (Ratio: 1.66%) + Conflict : 133630 (Average Length: 539.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 133630 (Average: 14.40 Max: 910 Sum: 1924414) + Executed : 133505 (Average: 14.38 Max: 910 Sum: 1921270 Ratio: 99.84%) + Bounded : 125 (Average: 25.15 Max: 72 Sum: 3144 Ratio: 0.16%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 542224 (Eliminated: 0 Frozen: 166294) +Constraints : 3909881 (Binary: 91.2% Ternary: 6.9% Other: 1.8%) + +Memory Peak : 676MB +Max. Length : 65 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.67s +Memory: 615MB (+5MB) +UNKNOWN +Iteration Time: 10.66s + +Iteration 20 +Queue: [(15,75,0,True), (16,80,0,True)] +Grounded Until: 70 +Expected Memory: 689.0MB +Grounding... [('step', [71]), ('step', [72]), ('step', [73]), ('step', [74]), ('step', [75]), ('check', [75])] +Grounding Time: 0.57s +Memory: 616MB (+1MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 21 +Time : 143.234s (Solving: 127.68s 1st Model: 0.00s Unsat: 2.40s) +CPU Time : 143.120s + +Choices : 2401935 (Domain: 2211433) +Conflicts : 141844 (Analyzed: 141841) +Restarts : 1650 (Average: 85.96 Last: 157) +Model-Level : 183.0 +Problems : 21 (Average Length: 36.52 Splits: 0) +Lemmas : 141841 (Deleted: 122531) + Binary : 4527 (Ratio: 3.19%) + Ternary : 2257 (Ratio: 1.59%) + Conflict : 141841 (Average Length: 531.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 141841 (Average: 14.90 Max: 910 Sum: 2113516) + Executed : 141713 (Average: 14.88 Max: 910 Sum: 2110141 Ratio: 99.84%) + Bounded : 128 (Average: 26.37 Max: 77 Sum: 3375 Ratio: 0.16%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 582300 (Eliminated: 0 Frozen: 178744) +Constraints : 4211821 (Binary: 91.2% Ternary: 6.9% Other: 1.8%) + +Memory Peak : 698MB +Max. Length : 70 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 11.29s +Memory: 643MB (+27MB) +UNKNOWN +Iteration Time: 12.30s + +Iteration 21 +Queue: [(16,80,0,True)] +Grounded Until: 75 +Expected Memory: 717.0MB +Grounding... [('step', [76]), ('step', [77]), ('step', [78]), ('step', [79]), ('step', [80]), ('check', [80])] +Grounding Time: 0.57s +Memory: 643MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 22 +Time : 153.637s (Solving: 136.96s 1st Model: 0.00s Unsat: 2.40s) +CPU Time : 153.528s + +Choices : 2605196 (Domain: 2410332) +Conflicts : 150017 (Analyzed: 150014) +Restarts : 1750 (Average: 85.72 Last: 157) +Model-Level : 183.0 +Problems : 22 (Average Length: 38.59 Splits: 0) +Lemmas : 150014 (Deleted: 130452) + Binary : 4621 (Ratio: 3.08%) + Ternary : 2282 (Ratio: 1.52%) + Conflict : 150014 (Average Length: 525.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 150014 (Average: 15.26 Max: 1010 Sum: 2289293) + Executed : 149883 (Average: 15.24 Max: 1010 Sum: 2285672 Ratio: 99.84%) + Bounded : 131 (Average: 27.64 Max: 82 Sum: 3621 Ratio: 0.16%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 622376 (Eliminated: 0 Frozen: 191194) +Constraints : 4513760 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 727MB +Max. Length : 75 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.41s +Memory: 668MB (+25MB) +UNKNOWN +Iteration Time: 10.42s + +Iteration 22 +Queue: [(4,20,2,True), (5,25,2,True), (6,30,2,True), (7,35,1,True), (8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 80 +Blocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 23 +Time : 162.246s (Solving: 145.43s 1st Model: 0.00s Unsat: 2.40s) +CPU Time : 162.144s + +Choices : 2670865 (Domain: 2470369) +Conflicts : 158594 (Analyzed: 158591) +Restarts : 1850 (Average: 85.72 Last: 157) +Model-Level : 183.0 +Problems : 23 (Average Length: 40.48 Splits: 0) +Lemmas : 158591 (Deleted: 138588) + Binary : 4772 (Ratio: 3.01%) + Ternary : 2342 (Ratio: 1.48%) + Conflict : 158591 (Average Length: 525.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 158591 (Average: 14.81 Max: 1010 Sum: 2348653) + Executed : 158458 (Average: 14.79 Max: 1010 Sum: 2344949 Ratio: 99.84%) + Bounded : 133 (Average: 27.85 Max: 82 Sum: 3704 Ratio: 0.16%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 622376 (Eliminated: 0 Frozen: 191194) +Constraints : 4513718 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 727MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.56s +Memory: 668MB (+0MB) +UNKNOWN +Iteration Time: 8.62s + +Iteration 23 +Queue: [(5,25,2,True), (6,30,2,True), (7,35,1,True), (8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 80 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 24 +Time : 169.973s (Solving: 153.03s 1st Model: 0.00s Unsat: 2.40s) +CPU Time : 169.876s + +Choices : 2743021 (Domain: 2537527) +Conflicts : 167336 (Analyzed: 167333) +Restarts : 1950 (Average: 85.81 Last: 157) +Model-Level : 183.0 +Problems : 24 (Average Length: 42.21 Splits: 0) +Lemmas : 167333 (Deleted: 148243) + Binary : 4901 (Ratio: 2.93%) + Ternary : 2416 (Ratio: 1.44%) + Conflict : 167333 (Average Length: 533.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 167333 (Average: 14.39 Max: 1010 Sum: 2407912) + Executed : 167200 (Average: 14.37 Max: 1010 Sum: 2404208 Ratio: 99.85%) + Bounded : 133 (Average: 27.85 Max: 82 Sum: 3704 Ratio: 0.15%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 622376 (Eliminated: 0 Frozen: 191194) +Constraints : 4513705 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 727MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.69s +Memory: 668MB (+0MB) +UNKNOWN +Iteration Time: 7.73s + +Iteration 24 +Queue: [(6,30,2,True), (7,35,1,True), (8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 80 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 25 +Time : 176.838s (Solving: 159.75s 1st Model: 0.00s Unsat: 2.40s) +CPU Time : 176.748s + +Choices : 2793194 (Domain: 2586360) +Conflicts : 175654 (Analyzed: 175651) +Restarts : 2050 (Average: 85.68 Last: 157) +Model-Level : 183.0 +Problems : 25 (Average Length: 43.80 Splits: 0) +Lemmas : 175651 (Deleted: 154469) + Binary : 4994 (Ratio: 2.84%) + Ternary : 2449 (Ratio: 1.39%) + Conflict : 175651 (Average Length: 523.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 175651 (Average: 13.95 Max: 1010 Sum: 2449845) + Executed : 175518 (Average: 13.93 Max: 1010 Sum: 2446141 Ratio: 99.85%) + Bounded : 133 (Average: 27.85 Max: 82 Sum: 3704 Ratio: 0.15%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 622376 (Eliminated: 0 Frozen: 191194) +Constraints : 4513705 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 727MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.82s +Memory: 668MB (+0MB) +UNKNOWN +Iteration Time: 6.87s + +Iteration 25 +Queue: [(7,35,1,True), (8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 80 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 26 +Time : 184.556s (Solving: 167.33s 1st Model: 0.00s Unsat: 2.40s) +CPU Time : 184.468s + +Choices : 2881735 (Domain: 2673125) +Conflicts : 183975 (Analyzed: 183972) +Restarts : 2150 (Average: 85.57 Last: 157) +Model-Level : 183.0 +Problems : 26 (Average Length: 45.27 Splits: 0) +Lemmas : 183972 (Deleted: 162565) + Binary : 5040 (Ratio: 2.74%) + Ternary : 2464 (Ratio: 1.34%) + Conflict : 183972 (Average Length: 518.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 183972 (Average: 13.72 Max: 1010 Sum: 2524861) + Executed : 183837 (Average: 13.70 Max: 1010 Sum: 2520998 Ratio: 99.85%) + Bounded : 135 (Average: 28.61 Max: 82 Sum: 3863 Ratio: 0.15%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 622376 (Eliminated: 0 Frozen: 191194) +Constraints : 4513705 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 727MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.67s +Memory: 668MB (+0MB) +UNKNOWN +Iteration Time: 7.72s + +Iteration 26 +Queue: [(8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 80 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 27 +Time : 192.272s (Solving: 174.90s 1st Model: 0.00s Unsat: 2.40s) +CPU Time : 192.188s + +Choices : 2993870 (Domain: 2779772) +Conflicts : 192077 (Analyzed: 192074) +Restarts : 2250 (Average: 85.37 Last: 157) +Model-Level : 183.0 +Problems : 27 (Average Length: 46.63 Splits: 0) +Lemmas : 192074 (Deleted: 170725) + Binary : 5110 (Ratio: 2.66%) + Ternary : 2477 (Ratio: 1.29%) + Conflict : 192074 (Average Length: 519.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 192074 (Average: 13.64 Max: 1010 Sum: 2620085) + Executed : 191939 (Average: 13.62 Max: 1010 Sum: 2616222 Ratio: 99.85%) + Bounded : 135 (Average: 28.61 Max: 82 Sum: 3863 Ratio: 0.15%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 622376 (Eliminated: 0 Frozen: 191194) +Constraints : 4513691 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 727MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.66s +Memory: 668MB (+0MB) +UNKNOWN +Iteration Time: 7.72s + +Iteration 27 +Queue: [(9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 80 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 28 +Time : 204.351s (Solving: 186.86s 1st Model: 0.00s Unsat: 2.40s) +CPU Time : 204.272s + +Choices : 3317666 (Domain: 3078914) +Conflicts : 201174 (Analyzed: 201171) +Restarts : 2350 (Average: 85.60 Last: 157) +Model-Level : 183.0 +Problems : 28 (Average Length: 47.89 Splits: 0) +Lemmas : 201171 (Deleted: 180087) + Binary : 5501 (Ratio: 2.73%) + Ternary : 2562 (Ratio: 1.27%) + Conflict : 201171 (Average Length: 536.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 201171 (Average: 14.49 Max: 1010 Sum: 2915539) + Executed : 201036 (Average: 14.47 Max: 1010 Sum: 2911676 Ratio: 99.87%) + Bounded : 135 (Average: 28.61 Max: 82 Sum: 3863 Ratio: 0.13%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 622376 (Eliminated: 0 Frozen: 191194) +Constraints : 4513691 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 727MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 12.04s +Memory: 668MB (+0MB) +UNKNOWN +Iteration Time: 12.09s + +Iteration 28 +Queue: [(10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 80 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 29 +Time : 211.665s (Solving: 194.04s 1st Model: 0.00s Unsat: 2.40s) +CPU Time : 211.588s + +Choices : 3439190 (Domain: 3199143) +Conflicts : 208925 (Analyzed: 208922) +Restarts : 2450 (Average: 85.27 Last: 157) +Model-Level : 183.0 +Problems : 29 (Average Length: 49.07 Splits: 0) +Lemmas : 208922 (Deleted: 186770) + Binary : 5579 (Ratio: 2.67%) + Ternary : 2572 (Ratio: 1.23%) + Conflict : 208922 (Average Length: 528.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 208922 (Average: 14.47 Max: 1010 Sum: 3023317) + Executed : 208787 (Average: 14.45 Max: 1010 Sum: 3019454 Ratio: 99.87%) + Bounded : 135 (Average: 28.61 Max: 82 Sum: 3863 Ratio: 0.13%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 622376 (Eliminated: 0 Frozen: 191194) +Constraints : 4513691 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 727MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.27s +Memory: 668MB (+0MB) +UNKNOWN +Iteration Time: 7.32s + +Iteration 29 +Queue: [(11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 80 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 30 +Time : 217.857s (Solving: 200.09s 1st Model: 0.00s Unsat: 2.40s) +CPU Time : 217.784s + +Choices : 3520051 (Domain: 3279560) +Conflicts : 216107 (Analyzed: 216104) +Restarts : 2550 (Average: 84.75 Last: 157) +Model-Level : 183.0 +Problems : 30 (Average Length: 50.17 Splits: 0) +Lemmas : 216104 (Deleted: 194246) + Binary : 5641 (Ratio: 2.61%) + Ternary : 2593 (Ratio: 1.20%) + Conflict : 216104 (Average Length: 523.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 216104 (Average: 14.31 Max: 1010 Sum: 3091425) + Executed : 215969 (Average: 14.29 Max: 1010 Sum: 3087562 Ratio: 99.88%) + Bounded : 135 (Average: 28.61 Max: 82 Sum: 3863 Ratio: 0.12%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 622376 (Eliminated: 0 Frozen: 191194) +Constraints : 4513691 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 727MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.14s +Memory: 668MB (+0MB) +UNKNOWN +Iteration Time: 6.20s + +Iteration 30 +Queue: [(12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 80 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 31 +Time : 224.621s (Solving: 206.70s 1st Model: 0.00s Unsat: 2.40s) +CPU Time : 224.548s + +Choices : 3585219 (Domain: 3344599) +Conflicts : 224007 (Analyzed: 224004) +Restarts : 2650 (Average: 84.53 Last: 157) +Model-Level : 183.0 +Problems : 31 (Average Length: 51.19 Splits: 0) +Lemmas : 224004 (Deleted: 201238) + Binary : 5663 (Ratio: 2.53%) + Ternary : 2601 (Ratio: 1.16%) + Conflict : 224004 (Average Length: 515.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 224004 (Average: 14.05 Max: 1010 Sum: 3146534) + Executed : 223868 (Average: 14.03 Max: 1010 Sum: 3142594 Ratio: 99.87%) + Bounded : 136 (Average: 28.97 Max: 82 Sum: 3940 Ratio: 0.13%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 622376 (Eliminated: 0 Frozen: 191194) +Constraints : 4513691 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 727MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.71s +Memory: 668MB (+0MB) +UNKNOWN +Iteration Time: 6.77s + +Iteration 31 +Queue: [(13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 80 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 32 +Time : 233.395s (Solving: 215.32s 1st Model: 0.00s Unsat: 2.40s) +CPU Time : 233.328s + +Choices : 3731353 (Domain: 3489030) +Conflicts : 232313 (Analyzed: 232310) +Restarts : 2750 (Average: 84.48 Last: 157) +Model-Level : 183.0 +Problems : 32 (Average Length: 52.16 Splits: 0) +Lemmas : 232310 (Deleted: 208952) + Binary : 5741 (Ratio: 2.47%) + Ternary : 2619 (Ratio: 1.13%) + Conflict : 232310 (Average Length: 509.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 232310 (Average: 14.11 Max: 1010 Sum: 3277720) + Executed : 232173 (Average: 14.09 Max: 1010 Sum: 3273698 Ratio: 99.88%) + Bounded : 137 (Average: 29.36 Max: 82 Sum: 4022 Ratio: 0.12%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 622376 (Eliminated: 0 Frozen: 191194) +Constraints : 4513691 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 727MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.72s +Memory: 668MB (+0MB) +UNKNOWN +Iteration Time: 8.78s + +Iteration 32 +Queue: [(14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 80 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 33 +Time : 243.720s (Solving: 225.52s 1st Model: 0.00s Unsat: 2.40s) +CPU Time : 243.660s + +Choices : 3939332 (Domain: 3695182) +Conflicts : 240640 (Analyzed: 240637) +Restarts : 2850 (Average: 84.43 Last: 157) +Model-Level : 183.0 +Problems : 33 (Average Length: 53.06 Splits: 0) +Lemmas : 240637 (Deleted: 216962) + Binary : 5848 (Ratio: 2.43%) + Ternary : 2635 (Ratio: 1.10%) + Conflict : 240637 (Average Length: 505.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 240637 (Average: 14.41 Max: 1010 Sum: 3468650) + Executed : 240499 (Average: 14.40 Max: 1010 Sum: 3464546 Ratio: 99.88%) + Bounded : 138 (Average: 29.74 Max: 82 Sum: 4104 Ratio: 0.12%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 622376 (Eliminated: 0 Frozen: 191194) +Constraints : 4513693 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 727MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 10.29s +Memory: 668MB (+0MB) +UNKNOWN +Iteration Time: 10.33s + +Iteration 33 +Queue: [(15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 80 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 34 +Time : 252.404s (Solving: 234.05s 1st Model: 0.00s Unsat: 2.40s) +CPU Time : 252.348s + +Choices : 4104662 (Domain: 3859160) +Conflicts : 248722 (Analyzed: 248719) +Restarts : 2950 (Average: 84.31 Last: 157) +Model-Level : 183.0 +Problems : 34 (Average Length: 53.91 Splits: 0) +Lemmas : 248719 (Deleted: 224964) + Binary : 5921 (Ratio: 2.38%) + Ternary : 2653 (Ratio: 1.07%) + Conflict : 248719 (Average Length: 500.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 248719 (Average: 14.54 Max: 1044 Sum: 3617011) + Executed : 248579 (Average: 14.53 Max: 1044 Sum: 3612747 Ratio: 99.88%) + Bounded : 140 (Average: 30.46 Max: 82 Sum: 4264 Ratio: 0.12%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 622376 (Eliminated: 0 Frozen: 191194) +Constraints : 4513679 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 727MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.63s +Memory: 668MB (+0MB) +UNKNOWN +Iteration Time: 8.69s + +Iteration 34 +Queue: [(16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 80 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 35 +Time : 260.213s (Solving: 241.73s 1st Model: 0.00s Unsat: 2.40s) +CPU Time : 260.160s + +Choices : 4269250 (Domain: 4022750) +Conflicts : 256518 (Analyzed: 256515) +Restarts : 3050 (Average: 84.10 Last: 157) +Model-Level : 183.0 +Problems : 35 (Average Length: 54.71 Splits: 0) +Lemmas : 256515 (Deleted: 232812) + Binary : 5995 (Ratio: 2.34%) + Ternary : 2672 (Ratio: 1.04%) + Conflict : 256515 (Average Length: 496.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 256515 (Average: 14.68 Max: 1044 Sum: 3765684) + Executed : 256374 (Average: 14.66 Max: 1044 Sum: 3761338 Ratio: 99.88%) + Bounded : 141 (Average: 30.82 Max: 82 Sum: 4346 Ratio: 0.12%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 622376 (Eliminated: 0 Frozen: 191194) +Constraints : 4513665 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 727MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.77s +Memory: 668MB (+0MB) +UNKNOWN +Iteration Time: 7.82s + +Iteration 35 +Queue: [(17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 80 +Expected Memory: 742.0MB +Grounding... [('step', [81]), ('step', [82]), ('step', [83]), ('step', [84]), ('step', [85]), ('check', [85])] +Grounding Time: 0.60s +Memory: 668MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 36 +Time : 267.786s (Solving: 248.11s 1st Model: 0.00s Unsat: 2.40s) +CPU Time : 267.736s + +Choices : 4348686 (Domain: 4101788) +Conflicts : 264283 (Analyzed: 264280) +Restarts : 3150 (Average: 83.90 Last: 157) +Model-Level : 183.0 +Problems : 36 (Average Length: 55.61 Splits: 0) +Lemmas : 264280 (Deleted: 240259) + Binary : 6036 (Ratio: 2.28%) + Ternary : 2685 (Ratio: 1.02%) + Conflict : 264280 (Average Length: 490.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 264280 (Average: 14.49 Max: 1044 Sum: 3830386) + Executed : 264137 (Average: 14.48 Max: 1044 Sum: 3825871 Ratio: 99.88%) + Bounded : 143 (Average: 31.57 Max: 87 Sum: 4515 Ratio: 0.12%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 662452 (Eliminated: 0 Frozen: 203644) +Constraints : 4815631 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 755MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.51s +Memory: 691MB (+23MB) +UNKNOWN +Iteration Time: 7.59s + +Iteration 36 +Queue: [(18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 85 +Expected Memory: 765.0MB +Grounding... [('step', [86]), ('step', [87]), ('step', [88]), ('step', [89]), ('step', [90]), ('check', [90])] +Grounding Time: 0.59s +Memory: 691MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 37 +Time : 280.324s (Solving: 259.44s 1st Model: 0.00s Unsat: 2.40s) +CPU Time : 280.280s + +Choices : 4806070 (Domain: 4550562) +Conflicts : 272656 (Analyzed: 272653) +Restarts : 3250 (Average: 83.89 Last: 157) +Model-Level : 183.0 +Problems : 37 (Average Length: 56.59 Splits: 0) +Lemmas : 272653 (Deleted: 247693) + Binary : 6270 (Ratio: 2.30%) + Ternary : 2729 (Ratio: 1.00%) + Conflict : 272653 (Average Length: 500.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 272653 (Average: 15.62 Max: 1044 Sum: 4257604) + Executed : 272510 (Average: 15.60 Max: 1044 Sum: 4253089 Ratio: 99.89%) + Bounded : 143 (Average: 31.57 Max: 87 Sum: 4515 Ratio: 0.11%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 702528 (Eliminated: 0 Frozen: 216094) +Constraints : 5114549 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 790MB +Max. Length : 85 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 11.47s +Memory: 763MB (+72MB) +UNKNOWN +Iteration Time: 12.56s + +Iteration 37 +Queue: [(19,95,0,True), (20,100,0,True), (21,105,0,True)] +Grounded Until: 90 +Expected Memory: 837.0MB +Grounding... [('step', [91]), ('step', [92]), ('step', [93]), ('step', [94]), ('step', [95]), ('check', [95])] +Grounding Time: 0.95s +Memory: 813MB (+50MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 38 +Time : 296.936s (Solving: 274.46s 1st Model: 0.00s Unsat: 2.40s) +CPU Time : 296.896s + +Choices : 5382955 (Domain: 5117111) +Conflicts : 281712 (Analyzed: 281709) +Restarts : 3350 (Average: 84.09 Last: 157) +Model-Level : 183.0 +Problems : 38 (Average Length: 57.66 Splits: 0) +Lemmas : 281709 (Deleted: 257600) + Binary : 6538 (Ratio: 2.32%) + Ternary : 2790 (Ratio: 0.99%) + Conflict : 281709 (Average Length: 525.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 281709 (Average: 17.02 Max: 1044 Sum: 4793424) + Executed : 281566 (Average: 17.00 Max: 1044 Sum: 4788909 Ratio: 99.91%) + Bounded : 143 (Average: 31.57 Max: 87 Sum: 4515 Ratio: 0.09%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 742604 (Eliminated: 0 Frozen: 228544) +Constraints : 5416529 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 946MB +Max. Length : 90 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 15.16s +Memory: 882MB (+69MB) +UNKNOWN +Iteration Time: 16.63s + +Iteration 38 +Queue: [(20,100,0,True), (21,105,0,True)] +Grounded Until: 95 +Expected Memory: 1001.0MB +Grounding... [('step', [96]), ('step', [97]), ('step', [98]), ('step', [99]), ('step', [100]), ('check', [100])] +Grounding Time: 0.56s +Memory: 882MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 39 +Time : 305.801s (Solving: 282.12s 1st Model: 0.00s Unsat: 2.40s) +CPU Time : 305.764s + +Choices : 5562451 (Domain: 5295760) +Conflicts : 289712 (Analyzed: 289709) +Restarts : 3450 (Average: 83.97 Last: 157) +Model-Level : 183.0 +Problems : 39 (Average Length: 58.79 Splits: 0) +Lemmas : 289709 (Deleted: 264065) + Binary : 6653 (Ratio: 2.30%) + Ternary : 2806 (Ratio: 0.97%) + Conflict : 289709 (Average Length: 519.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 289709 (Average: 17.11 Max: 1273 Sum: 4955544) + Executed : 289565 (Average: 17.09 Max: 1273 Sum: 4950927 Ratio: 99.91%) + Bounded : 144 (Average: 32.06 Max: 102 Sum: 4617 Ratio: 0.09%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 782680 (Eliminated: 0 Frozen: 240994) +Constraints : 5718509 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 977MB +Max. Length : 95 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.81s +Memory: 888MB (+6MB) +UNKNOWN +Iteration Time: 8.88s + +Iteration 39 +Queue: [(21,105,0,True)] +Grounded Until: 100 +Expected Memory: 1007.0MB +Grounding... [('step', [101]), ('step', [102]), ('step', [103]), ('step', [104]), ('step', [105]), ('check', [105])] +Grounding Time: 0.55s +Memory: 889MB (+1MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 40 +Time : 314.321s (Solving: 289.43s 1st Model: 0.00s Unsat: 2.40s) +CPU Time : 314.288s + +Choices : 5768001 (Domain: 5500320) +Conflicts : 297542 (Analyzed: 297539) +Restarts : 3550 (Average: 83.81 Last: 157) +Model-Level : 183.0 +Problems : 40 (Average Length: 60.00 Splits: 0) +Lemmas : 297539 (Deleted: 271686) + Binary : 6728 (Ratio: 2.26%) + Ternary : 2824 (Ratio: 0.95%) + Conflict : 297539 (Average Length: 515.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 297539 (Average: 17.28 Max: 1374 Sum: 5142263) + Executed : 297394 (Average: 17.27 Max: 1374 Sum: 5137542 Ratio: 99.91%) + Bounded : 145 (Average: 32.56 Max: 104 Sum: 4721 Ratio: 0.09%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 822756 (Eliminated: 0 Frozen: 253444) +Constraints : 6020476 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1005MB +Max. Length : 100 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.46s +Memory: 914MB (+25MB) +UNKNOWN +Iteration Time: 8.54s + +Iteration 40 +Queue: [(4,20,3,True), (5,25,3,True), (6,30,3,True), (7,35,2,True), (8,40,2,True), (9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Blocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 41 +Time : 321.643s (Solving: 296.58s 1st Model: 0.00s Unsat: 2.40s) +CPU Time : 321.616s + +Choices : 5826604 (Domain: 5558923) +Conflicts : 305230 (Analyzed: 305227) +Restarts : 3650 (Average: 83.62 Last: 157) +Model-Level : 183.0 +Problems : 41 (Average Length: 61.15 Splits: 0) +Lemmas : 305227 (Deleted: 279254) + Binary : 6823 (Ratio: 2.24%) + Ternary : 2826 (Ratio: 0.93%) + Conflict : 305227 (Average Length: 512.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 305227 (Average: 17.02 Max: 1374 Sum: 5195791) + Executed : 305082 (Average: 17.01 Max: 1374 Sum: 5191070 Ratio: 99.91%) + Bounded : 145 (Average: 32.56 Max: 104 Sum: 4721 Ratio: 0.09%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 822756 (Eliminated: 0 Frozen: 253444) +Constraints : 6020476 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1005MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.27s +Memory: 914MB (+0MB) +UNKNOWN +Iteration Time: 7.33s + +Iteration 41 +Queue: [(5,25,3,True), (6,30,3,True), (7,35,2,True), (8,40,2,True), (9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 42 +Time : 330.430s (Solving: 305.20s 1st Model: 0.00s Unsat: 2.40s) +CPU Time : 330.408s + +Choices : 5896868 (Domain: 5623680) +Conflicts : 313655 (Analyzed: 313652) +Restarts : 3750 (Average: 83.64 Last: 157) +Model-Level : 183.0 +Problems : 42 (Average Length: 62.24 Splits: 0) +Lemmas : 313652 (Deleted: 286601) + Binary : 6949 (Ratio: 2.22%) + Ternary : 2855 (Ratio: 0.91%) + Conflict : 313652 (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 : 313652 (Average: 16.75 Max: 1374 Sum: 5252391) + Executed : 313507 (Average: 16.73 Max: 1374 Sum: 5247670 Ratio: 99.91%) + Bounded : 145 (Average: 32.56 Max: 104 Sum: 4721 Ratio: 0.09%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 822756 (Eliminated: 0 Frozen: 253444) +Constraints : 6020476 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1005MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.73s +Memory: 914MB (+0MB) +UNKNOWN +Iteration Time: 8.79s + +Iteration 42 +Queue: [(6,30,3,True), (7,35,2,True), (8,40,2,True), (9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 43 +Time : 335.159s (Solving: 309.74s 1st Model: 0.00s Unsat: 2.40s) +CPU Time : 335.140s + +Choices : 5947391 (Domain: 5673356) +Conflicts : 321491 (Analyzed: 321488) +Restarts : 3850 (Average: 83.50 Last: 157) +Model-Level : 183.0 +Problems : 43 (Average Length: 63.28 Splits: 0) +Lemmas : 321488 (Deleted: 294702) + Binary : 6992 (Ratio: 2.17%) + Ternary : 2866 (Ratio: 0.89%) + Conflict : 321488 (Average Length: 514.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 321488 (Average: 16.47 Max: 1374 Sum: 5294129) + Executed : 321343 (Average: 16.45 Max: 1374 Sum: 5289408 Ratio: 99.91%) + Bounded : 145 (Average: 32.56 Max: 104 Sum: 4721 Ratio: 0.09%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 822756 (Eliminated: 0 Frozen: 253444) +Constraints : 6020476 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1005MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 4.66s +Memory: 914MB (+0MB) +UNKNOWN +Iteration Time: 4.74s + +Iteration 43 +Queue: [(7,35,2,True), (8,40,2,True), (9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 44 +Time : 342.312s (Solving: 316.69s 1st Model: 0.00s Unsat: 2.40s) +CPU Time : 342.296s + +Choices : 6036512 (Domain: 5760556) +Conflicts : 329836 (Analyzed: 329833) +Restarts : 3950 (Average: 83.50 Last: 185) +Model-Level : 183.0 +Problems : 44 (Average Length: 64.27 Splits: 0) +Lemmas : 329833 (Deleted: 302258) + Binary : 7076 (Ratio: 2.15%) + Ternary : 2884 (Ratio: 0.87%) + Conflict : 329833 (Average Length: 510.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 329833 (Average: 16.29 Max: 1374 Sum: 5372439) + Executed : 329685 (Average: 16.27 Max: 1374 Sum: 5367404 Ratio: 99.91%) + Bounded : 148 (Average: 34.02 Max: 107 Sum: 5035 Ratio: 0.09%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 822756 (Eliminated: 0 Frozen: 253444) +Constraints : 6020476 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1005MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.08s +Memory: 914MB (+0MB) +UNKNOWN +Iteration Time: 7.16s + +Iteration 44 +Queue: [(8,40,2,True), (9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 45 +Time : 350.390s (Solving: 324.61s 1st Model: 0.00s Unsat: 2.40s) +CPU Time : 350.380s + +Choices : 6168437 (Domain: 5888804) +Conflicts : 338780 (Analyzed: 338777) +Restarts : 4050 (Average: 83.65 Last: 185) +Model-Level : 183.0 +Problems : 45 (Average Length: 65.22 Splits: 0) +Lemmas : 338777 (Deleted: 312440) + Binary : 7165 (Ratio: 2.11%) + Ternary : 2895 (Ratio: 0.85%) + Conflict : 338777 (Average Length: 510.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 338777 (Average: 16.20 Max: 1374 Sum: 5488988) + Executed : 338629 (Average: 16.19 Max: 1374 Sum: 5483953 Ratio: 99.91%) + Bounded : 148 (Average: 34.02 Max: 107 Sum: 5035 Ratio: 0.09%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 822756 (Eliminated: 0 Frozen: 253444) +Constraints : 6020462 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1005MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.03s +Memory: 914MB (+0MB) +UNKNOWN +Iteration Time: 8.09s + +Iteration 45 +Queue: [(9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 46 +Time : 357.056s (Solving: 331.11s 1st Model: 0.00s Unsat: 2.40s) +CPU Time : 357.048s + +Choices : 6280639 (Domain: 5999286) +Conflicts : 346955 (Analyzed: 346952) +Restarts : 4150 (Average: 83.60 Last: 185) +Model-Level : 183.0 +Problems : 46 (Average Length: 66.13 Splits: 0) +Lemmas : 346952 (Deleted: 318946) + Binary : 7213 (Ratio: 2.08%) + Ternary : 2904 (Ratio: 0.84%) + Conflict : 346952 (Average Length: 509.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 346952 (Average: 16.10 Max: 1374 Sum: 5586987) + Executed : 346804 (Average: 16.09 Max: 1374 Sum: 5581952 Ratio: 99.91%) + Bounded : 148 (Average: 34.02 Max: 107 Sum: 5035 Ratio: 0.09%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 822756 (Eliminated: 0 Frozen: 253444) +Constraints : 6020462 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1005MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.61s +Memory: 914MB (+0MB) +UNKNOWN +Iteration Time: 6.67s + +Iteration 46 +Queue: [(10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 47 +Time : 364.389s (Solving: 338.29s 1st Model: 0.00s Unsat: 2.40s) +CPU Time : 364.384s + +Choices : 6439253 (Domain: 6155618) +Conflicts : 355230 (Analyzed: 355227) +Restarts : 4250 (Average: 83.58 Last: 185) +Model-Level : 183.0 +Problems : 47 (Average Length: 67.00 Splits: 0) +Lemmas : 355227 (Deleted: 326815) + Binary : 7410 (Ratio: 2.09%) + Ternary : 3010 (Ratio: 0.85%) + Conflict : 355227 (Average Length: 506.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 355227 (Average: 16.13 Max: 1374 Sum: 5731234) + Executed : 355078 (Average: 16.12 Max: 1374 Sum: 5726095 Ratio: 99.91%) + Bounded : 149 (Average: 34.49 Max: 107 Sum: 5139 Ratio: 0.09%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 822756 (Eliminated: 0 Frozen: 253444) +Constraints : 6020462 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1005MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.28s +Memory: 914MB (+0MB) +UNKNOWN +Iteration Time: 7.34s + +Iteration 47 +Queue: [(11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 48 +Time : 372.105s (Solving: 345.82s 1st Model: 0.00s Unsat: 2.40s) +CPU Time : 372.104s + +Choices : 6631973 (Domain: 6346310) +Conflicts : 363365 (Analyzed: 363362) +Restarts : 4350 (Average: 83.53 Last: 185) +Model-Level : 183.0 +Problems : 48 (Average Length: 67.83 Splits: 0) +Lemmas : 363362 (Deleted: 334432) + Binary : 7577 (Ratio: 2.09%) + Ternary : 3087 (Ratio: 0.85%) + Conflict : 363362 (Average Length: 504.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 363362 (Average: 16.26 Max: 1374 Sum: 5907978) + Executed : 363212 (Average: 16.24 Max: 1374 Sum: 5902732 Ratio: 99.91%) + Bounded : 150 (Average: 34.97 Max: 107 Sum: 5246 Ratio: 0.09%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 822756 (Eliminated: 0 Frozen: 253444) +Constraints : 6020462 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1005MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.65s +Memory: 914MB (+0MB) +UNKNOWN +Iteration Time: 7.72s + +Iteration 48 +Queue: [(12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 49 +Time : 379.766s (Solving: 353.29s 1st Model: 0.00s Unsat: 2.40s) +CPU Time : 379.768s + +Choices : 6831592 (Domain: 6541482) +Conflicts : 371683 (Analyzed: 371680) +Restarts : 4450 (Average: 83.52 Last: 185) +Model-Level : 183.0 +Problems : 49 (Average Length: 68.63 Splits: 0) +Lemmas : 371680 (Deleted: 342205) + Binary : 7672 (Ratio: 2.06%) + Ternary : 3104 (Ratio: 0.84%) + Conflict : 371680 (Average Length: 503.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 371680 (Average: 16.37 Max: 1374 Sum: 6084055) + Executed : 371530 (Average: 16.35 Max: 1374 Sum: 6078809 Ratio: 99.91%) + Bounded : 150 (Average: 34.97 Max: 107 Sum: 5246 Ratio: 0.09%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 822756 (Eliminated: 0 Frozen: 253444) +Constraints : 6020448 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1005MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.59s +Memory: 914MB (+0MB) +UNKNOWN +Iteration Time: 7.67s + +Iteration 49 +Queue: [(13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 50 +Time : 389.333s (Solving: 362.66s 1st Model: 0.00s Unsat: 2.40s) +CPU Time : 389.340s + +Choices : 7114481 (Domain: 6821255) +Conflicts : 380450 (Analyzed: 380447) +Restarts : 4550 (Average: 83.61 Last: 185) +Model-Level : 183.0 +Problems : 50 (Average Length: 69.40 Splits: 0) +Lemmas : 380447 (Deleted: 352305) + Binary : 7803 (Ratio: 2.05%) + Ternary : 3142 (Ratio: 0.83%) + Conflict : 380447 (Average Length: 502.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 380447 (Average: 16.68 Max: 1374 Sum: 6346973) + Executed : 380297 (Average: 16.67 Max: 1374 Sum: 6341727 Ratio: 99.92%) + Bounded : 150 (Average: 34.97 Max: 107 Sum: 5246 Ratio: 0.08%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 822756 (Eliminated: 0 Frozen: 253444) +Constraints : 6020448 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1005MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.49s +Memory: 914MB (+0MB) +UNKNOWN +Iteration Time: 9.57s + +Iteration 50 +Queue: [(17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 51 +Time : 399.271s (Solving: 372.43s 1st Model: 0.00s Unsat: 2.40s) +CPU Time : 399.276s + +Choices : 7405815 (Domain: 7110612) +Conflicts : 388712 (Analyzed: 388709) +Restarts : 4650 (Average: 83.59 Last: 185) +Model-Level : 183.0 +Problems : 51 (Average Length: 70.14 Splits: 0) +Lemmas : 388709 (Deleted: 358623) + Binary : 7858 (Ratio: 2.02%) + Ternary : 3160 (Ratio: 0.81%) + Conflict : 388709 (Average Length: 504.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 388709 (Average: 17.02 Max: 1374 Sum: 6614005) + Executed : 388559 (Average: 17.00 Max: 1374 Sum: 6608759 Ratio: 99.92%) + Bounded : 150 (Average: 34.97 Max: 107 Sum: 5246 Ratio: 0.08%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 822756 (Eliminated: 0 Frozen: 253444) +Constraints : 6020448 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1005MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.88s +Memory: 914MB (+0MB) +UNKNOWN +Iteration Time: 9.94s + +Iteration 51 +Queue: [(18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 52 +Time : 412.928s (Solving: 385.89s 1st Model: 0.00s Unsat: 2.40s) +CPU Time : 412.936s + +Choices : 7920513 (Domain: 7620183) +Conflicts : 397908 (Analyzed: 397905) +Restarts : 4750 (Average: 83.77 Last: 185) +Model-Level : 183.0 +Problems : 52 (Average Length: 70.85 Splits: 0) +Lemmas : 397905 (Deleted: 368777) + Binary : 8035 (Ratio: 2.02%) + Ternary : 3185 (Ratio: 0.80%) + Conflict : 397905 (Average Length: 510.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 397905 (Average: 17.84 Max: 1374 Sum: 7097953) + Executed : 397755 (Average: 17.83 Max: 1374 Sum: 7092707 Ratio: 99.93%) + Bounded : 150 (Average: 34.97 Max: 107 Sum: 5246 Ratio: 0.07%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 822756 (Eliminated: 0 Frozen: 253444) +Constraints : 6020448 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1005MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 13.58s +Memory: 914MB (+0MB) +UNKNOWN +Iteration Time: 13.67s + +Iteration 52 +Queue: [(19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 53 +Time : 420.742s (Solving: 393.51s 1st Model: 0.00s Unsat: 2.40s) +CPU Time : 420.752s + +Choices : 8140639 (Domain: 7838774) +Conflicts : 405543 (Analyzed: 405540) +Restarts : 4850 (Average: 83.62 Last: 185) +Model-Level : 183.0 +Problems : 53 (Average Length: 71.53 Splits: 0) +Lemmas : 405540 (Deleted: 375482) + Binary : 8079 (Ratio: 1.99%) + Ternary : 3192 (Ratio: 0.79%) + Conflict : 405540 (Average Length: 509.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 405540 (Average: 18.00 Max: 1374 Sum: 7298202) + Executed : 405390 (Average: 17.98 Max: 1374 Sum: 7292956 Ratio: 99.93%) + Bounded : 150 (Average: 34.97 Max: 107 Sum: 5246 Ratio: 0.07%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 822756 (Eliminated: 0 Frozen: 253444) +Constraints : 6020448 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1005MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.74s +Memory: 914MB (+0MB) +UNKNOWN +Iteration Time: 7.82s + +Iteration 53 +Queue: [(20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 54 +Time : 428.666s (Solving: 401.27s 1st Model: 0.00s Unsat: 2.40s) +CPU Time : 428.676s + +Choices : 8438795 (Domain: 8135512) +Conflicts : 413601 (Analyzed: 413598) +Restarts : 4950 (Average: 83.56 Last: 185) +Model-Level : 183.0 +Problems : 54 (Average Length: 72.19 Splits: 0) +Lemmas : 413598 (Deleted: 382895) + Binary : 8130 (Ratio: 1.97%) + Ternary : 3219 (Ratio: 0.78%) + Conflict : 413598 (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 : 413598 (Average: 18.30 Max: 1374 Sum: 7570763) + Executed : 413448 (Average: 18.29 Max: 1374 Sum: 7565517 Ratio: 99.93%) + Bounded : 150 (Average: 34.97 Max: 107 Sum: 5246 Ratio: 0.07%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 822756 (Eliminated: 0 Frozen: 253444) +Constraints : 6020448 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1005MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.87s +Memory: 914MB (+0MB) +UNKNOWN +Iteration Time: 7.93s + +Iteration 54 +Queue: [(21,105,1,True), (22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 55 +Time : 440.515s (Solving: 412.95s 1st Model: 0.00s Unsat: 2.40s) +CPU Time : 440.516s + +Choices : 9046151 (Domain: 8739101) +Conflicts : 422005 (Analyzed: 422002) +Restarts : 5050 (Average: 83.56 Last: 185) +Model-Level : 183.0 +Problems : 55 (Average Length: 72.82 Splits: 0) +Lemmas : 422002 (Deleted: 390171) + Binary : 8341 (Ratio: 1.98%) + Ternary : 3405 (Ratio: 0.81%) + Conflict : 422002 (Average Length: 505.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 422002 (Average: 19.31 Max: 1374 Sum: 8148974) + Executed : 421852 (Average: 19.30 Max: 1374 Sum: 8143728 Ratio: 99.94%) + Bounded : 150 (Average: 34.97 Max: 107 Sum: 5246 Ratio: 0.06%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 822756 (Eliminated: 0 Frozen: 253444) +Constraints : 6020448 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1005MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 11.77s +Memory: 914MB (+0MB) +UNKNOWN +Iteration Time: 11.84s + +Iteration 55 +Queue: [(22,110,0,True), (23,115,0,True)] +Grounded Until: 105 +Expected Memory: 1033.0MB +Grounding... [('step', [106]), ('step', [107]), ('step', [108]), ('step', [109]), ('step', [110]), ('check', [110])] +Grounding Time: 0.56s +Memory: 914MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 56 +Time : 453.155s (Solving: 424.33s 1st Model: 0.00s Unsat: 2.40s) +CPU Time : 453.164s + +Choices : 9387514 (Domain: 9078824) +Conflicts : 430106 (Analyzed: 430103) +Restarts : 5150 (Average: 83.52 Last: 185) +Model-Level : 183.0 +Problems : 56 (Average Length: 73.52 Splits: 0) +Lemmas : 430103 (Deleted: 397920) + Binary : 8438 (Ratio: 1.96%) + Ternary : 3434 (Ratio: 0.80%) + Conflict : 430103 (Average Length: 503.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 430103 (Average: 19.67 Max: 1374 Sum: 8461648) + Executed : 429953 (Average: 19.66 Max: 1374 Sum: 8456402 Ratio: 99.94%) + Bounded : 150 (Average: 34.97 Max: 107 Sum: 5246 Ratio: 0.06%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 862832 (Eliminated: 0 Frozen: 265894) +Constraints : 6322428 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1037MB +Max. Length : 105 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 11.54s +Memory: 946MB (+32MB) +UNKNOWN +Iteration Time: 12.66s + +Iteration 56 +Queue: [(23,115,0,True)] +Grounded Until: 110 +Expected Memory: 1065.0MB +Grounding... [('step', [111]), ('step', [112]), ('step', [113]), ('step', [114]), ('step', [115]), ('check', [115])] +Grounding Time: 0.56s +Memory: 946MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 57 +Time : 477.954s (Solving: 447.85s 1st Model: 0.00s Unsat: 2.40s) +CPU Time : 477.940s + +Choices : 10831659 (Domain: 10511735) +Conflicts : 440818 (Analyzed: 440815) +Restarts : 5250 (Average: 83.96 Last: 185) +Model-Level : 183.0 +Problems : 57 (Average Length: 74.28 Splits: 0) +Lemmas : 440815 (Deleted: 406854) + Binary : 9271 (Ratio: 2.10%) + Ternary : 3822 (Ratio: 0.87%) + Conflict : 440815 (Average Length: 505.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 440815 (Average: 22.35 Max: 1455 Sum: 9854382) + Executed : 440665 (Average: 22.34 Max: 1455 Sum: 9849136 Ratio: 99.95%) + Bounded : 150 (Average: 34.97 Max: 107 Sum: 5246 Ratio: 0.05%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 902908 (Eliminated: 0 Frozen: 278344) +Constraints : 6624408 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1071MB +Max. Length : 110 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 23.66s +Memory: 975MB (+29MB) +UNKNOWN +Iteration Time: 24.79s + +Iteration 57 +Queue: [(4,20,4,True), (5,25,4,True), (6,30,4,True), (7,35,3,True), (8,40,3,True), (9,45,3,True), (10,50,3,True), (11,55,3,False), (12,60,3,False), (13,65,3,False), (14,70,2,True), (15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,1,True), (23,115,1,True)] +Grounded Until: 115 +Blocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 58 +Time : 484.554s (Solving: 454.27s 1st Model: 0.00s Unsat: 2.40s) +CPU Time : 484.544s + +Choices : 10879063 (Domain: 10559139) +Conflicts : 448316 (Analyzed: 448313) +Restarts : 5350 (Average: 83.80 Last: 185) +Model-Level : 183.0 +Problems : 58 (Average Length: 75.02 Splits: 0) +Lemmas : 448313 (Deleted: 413945) + Binary : 9333 (Ratio: 2.08%) + Ternary : 3831 (Ratio: 0.85%) + Conflict : 448313 (Average Length: 501.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 448313 (Average: 22.07 Max: 1455 Sum: 9895935) + Executed : 448161 (Average: 22.06 Max: 1455 Sum: 9890455 Ratio: 99.94%) + Bounded : 152 (Average: 36.05 Max: 117 Sum: 5480 Ratio: 0.06%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 902908 (Eliminated: 0 Frozen: 278344) +Constraints : 6624408 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1071MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.54s +Memory: 975MB (+0MB) +UNKNOWN +Iteration Time: 6.61s + +Iteration 58 +Queue: [(5,25,4,True), (6,30,4,True), (7,35,3,True), (8,40,3,True), (9,45,3,True), (10,50,3,True), (11,55,3,False), (12,60,3,False), (13,65,3,False), (14,70,2,True), (15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,1,True), (23,115,1,True)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 59 +Time : 490.556s (Solving: 460.05s 1st Model: 0.00s Unsat: 2.40s) +CPU Time : 490.548s + +Choices : 10924947 (Domain: 10605023) +Conflicts : 456079 (Analyzed: 456076) +Restarts : 5450 (Average: 83.68 Last: 185) +Model-Level : 183.0 +Problems : 59 (Average Length: 75.73 Splits: 0) +Lemmas : 456076 (Deleted: 421159) + Binary : 9367 (Ratio: 2.05%) + Ternary : 3833 (Ratio: 0.84%) + Conflict : 456076 (Average Length: 501.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 456076 (Average: 21.78 Max: 1455 Sum: 9932435) + Executed : 455924 (Average: 21.77 Max: 1455 Sum: 9926955 Ratio: 99.94%) + Bounded : 152 (Average: 36.05 Max: 117 Sum: 5480 Ratio: 0.06%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 902908 (Eliminated: 0 Frozen: 278344) +Constraints : 6624381 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1071MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 5.92s +Memory: 975MB (+0MB) +UNKNOWN +Iteration Time: 6.01s + +Iteration 59 +Queue: [(6,30,4,True), (7,35,3,True), (8,40,3,True), (9,45,3,True), (10,50,3,True), (11,55,3,False), (12,60,3,False), (13,65,3,False), (14,70,2,True), (15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,1,True), (23,115,1,True)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 60 +Time : 496.094s (Solving: 465.39s 1st Model: 0.00s Unsat: 2.40s) +CPU Time : 496.088s + +Choices : 10986705 (Domain: 10665581) +Conflicts : 463289 (Analyzed: 463286) +Restarts : 5550 (Average: 83.47 Last: 185) +Model-Level : 183.0 +Problems : 60 (Average Length: 76.42 Splits: 0) +Lemmas : 463286 (Deleted: 428631) + Binary : 9475 (Ratio: 2.05%) + Ternary : 3846 (Ratio: 0.83%) + Conflict : 463286 (Average Length: 499.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 463286 (Average: 21.55 Max: 1455 Sum: 9982573) + Executed : 463134 (Average: 21.54 Max: 1455 Sum: 9977093 Ratio: 99.95%) + Bounded : 152 (Average: 36.05 Max: 117 Sum: 5480 Ratio: 0.05%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 902908 (Eliminated: 0 Frozen: 278344) +Constraints : 6624381 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1071MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 5.47s +Memory: 975MB (+0MB) +UNKNOWN +Iteration Time: 5.54s + +Iteration 60 +Queue: [(7,35,3,True), (8,40,3,True), (9,45,3,True), (10,50,3,True), (11,55,3,False), (12,60,3,False), (13,65,3,False), (14,70,2,True), (15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,1,True), (23,115,1,True)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 61 +Time : 501.089s (Solving: 470.18s 1st Model: 0.00s Unsat: 2.40s) +CPU Time : 501.084s + +Choices : 11030102 (Domain: 10708956) +Conflicts : 470556 (Analyzed: 470553) +Restarts : 5650 (Average: 83.28 Last: 185) +Model-Level : 183.0 +Problems : 61 (Average Length: 77.08 Splits: 0) +Lemmas : 470553 (Deleted: 435488) + Binary : 9548 (Ratio: 2.03%) + Ternary : 3868 (Ratio: 0.82%) + Conflict : 470553 (Average Length: 497.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 470553 (Average: 21.29 Max: 1455 Sum: 10017916) + Executed : 470400 (Average: 21.28 Max: 1455 Sum: 10012323 Ratio: 99.94%) + Bounded : 153 (Average: 36.56 Max: 117 Sum: 5593 Ratio: 0.06%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 902908 (Eliminated: 0 Frozen: 278344) +Constraints : 6624381 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1071MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 4.92s +Memory: 975MB (+0MB) +UNKNOWN +Iteration Time: 5.00s + +Iteration 61 +Queue: [(8,40,3,True), (9,45,3,True), (10,50,3,True), (11,55,3,False), (12,60,3,False), (13,65,3,False), (14,70,2,True), (15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,1,True), (23,115,1,True)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 62 +Time : 514.305s (Solving: 483.22s 1st Model: 0.00s Unsat: 2.40s) +CPU Time : 514.304s + +Choices : 11142025 (Domain: 10817712) +Conflicts : 479227 (Analyzed: 479224) +Restarts : 5750 (Average: 83.34 Last: 185) +Model-Level : 183.0 +Problems : 62 (Average Length: 77.73 Splits: 0) +Lemmas : 479224 (Deleted: 444388) + Binary : 9753 (Ratio: 2.04%) + Ternary : 3905 (Ratio: 0.81%) + Conflict : 479224 (Average Length: 509.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 479224 (Average: 21.08 Max: 1455 Sum: 10102920) + Executed : 479071 (Average: 21.07 Max: 1455 Sum: 10097327 Ratio: 99.94%) + Bounded : 153 (Average: 36.56 Max: 117 Sum: 5593 Ratio: 0.06%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 902908 (Eliminated: 0 Frozen: 278344) +Constraints : 6624381 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1071MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 13.16s +Memory: 975MB (+0MB) +UNKNOWN +Iteration Time: 13.22s + +Iteration 62 +Queue: [(9,45,3,True), (10,50,3,True), (11,55,3,False), (12,60,3,False), (13,65,3,False), (14,70,2,True), (15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,1,True), (23,115,1,True)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 63 +Time : 521.554s (Solving: 490.28s 1st Model: 0.00s Unsat: 2.40s) +CPU Time : 521.548s + +Choices : 11217424 (Domain: 10892754) +Conflicts : 486729 (Analyzed: 486726) +Restarts : 5850 (Average: 83.20 Last: 185) +Model-Level : 183.0 +Problems : 63 (Average Length: 78.35 Splits: 0) +Lemmas : 486726 (Deleted: 450665) + Binary : 9882 (Ratio: 2.03%) + Ternary : 3947 (Ratio: 0.81%) + Conflict : 486726 (Average Length: 506.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 486726 (Average: 20.89 Max: 1455 Sum: 10166930) + Executed : 486569 (Average: 20.88 Max: 1455 Sum: 10160874 Ratio: 99.94%) + Bounded : 157 (Average: 38.57 Max: 117 Sum: 6056 Ratio: 0.06%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 902908 (Eliminated: 0 Frozen: 278344) +Constraints : 6624381 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1071MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.18s +Memory: 975MB (+0MB) +UNKNOWN +Iteration Time: 7.25s + +Iteration 63 +Queue: [(10,50,3,True), (11,55,3,False), (12,60,3,False), (13,65,3,False), (14,70,2,True), (15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,1,True), (23,115,1,True)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 64 +Time : 532.779s (Solving: 501.29s 1st Model: 0.00s Unsat: 2.40s) +CPU Time : 532.780s + +Choices : 11414476 (Domain: 11087229) +Conflicts : 495018 (Analyzed: 495015) +Restarts : 5950 (Average: 83.20 Last: 185) +Model-Level : 183.0 +Problems : 64 (Average Length: 78.95 Splits: 0) +Lemmas : 495015 (Deleted: 457334) + Binary : 10090 (Ratio: 2.04%) + Ternary : 4014 (Ratio: 0.81%) + Conflict : 495015 (Average Length: 511.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 495015 (Average: 20.89 Max: 1455 Sum: 10341849) + Executed : 494858 (Average: 20.88 Max: 1455 Sum: 10335793 Ratio: 99.94%) + Bounded : 157 (Average: 38.57 Max: 117 Sum: 6056 Ratio: 0.06%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 902908 (Eliminated: 0 Frozen: 278344) +Constraints : 6624341 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1071MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 11.14s +Memory: 975MB (+0MB) +UNKNOWN +Iteration Time: 11.23s + +Iteration 64 +Queue: [(14,70,2,True), (15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,1,True), (23,115,1,True)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 65 +Time : 544.248s (Solving: 512.57s 1st Model: 0.00s Unsat: 2.40s) +CPU Time : 544.256s + +Choices : 11668016 (Domain: 11339143) +Conflicts : 503596 (Analyzed: 503593) +Restarts : 6050 (Average: 83.24 Last: 185) +Model-Level : 183.0 +Problems : 65 (Average Length: 79.54 Splits: 0) +Lemmas : 503593 (Deleted: 465102) + Binary : 10213 (Ratio: 2.03%) + Ternary : 4053 (Ratio: 0.80%) + Conflict : 503593 (Average Length: 512.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 503593 (Average: 20.99 Max: 1455 Sum: 10572702) + Executed : 503436 (Average: 20.98 Max: 1455 Sum: 10566646 Ratio: 99.94%) + Bounded : 157 (Average: 38.57 Max: 117 Sum: 6056 Ratio: 0.06%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 902908 (Eliminated: 0 Frozen: 278344) +Constraints : 6624341 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1071MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 11.41s +Memory: 975MB (+0MB) +UNKNOWN +Iteration Time: 11.48s + +Iteration 65 +Queue: [(15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,1,True), (23,115,1,True)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 66 +Time : 555.128s (Solving: 523.24s 1st Model: 0.00s Unsat: 2.40s) +CPU Time : 555.144s + +Choices : 11937161 (Domain: 11606955) +Conflicts : 512151 (Analyzed: 512148) +Restarts : 6150 (Average: 83.28 Last: 185) +Model-Level : 183.0 +Problems : 66 (Average Length: 80.11 Splits: 0) +Lemmas : 512148 (Deleted: 473103) + Binary : 10319 (Ratio: 2.01%) + Ternary : 4077 (Ratio: 0.80%) + Conflict : 512148 (Average Length: 514.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 512148 (Average: 21.12 Max: 1455 Sum: 10816985) + Executed : 511991 (Average: 21.11 Max: 1455 Sum: 10810929 Ratio: 99.94%) + Bounded : 157 (Average: 38.57 Max: 117 Sum: 6056 Ratio: 0.06%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 902908 (Eliminated: 0 Frozen: 278344) +Constraints : 6624341 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1071MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 10.80s +Memory: 975MB (+0MB) +UNKNOWN +Iteration Time: 10.89s + +Iteration 66 +Queue: [(22,110,1,True), (23,115,1,True)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 67 +Time : 565.666s (Solving: 533.58s 1st Model: 0.00s Unsat: 2.40s) +CPU Time : 565.688s + +Choices : 12317914 (Domain: 11986494) +Conflicts : 520221 (Analyzed: 520218) +Restarts : 6250 (Average: 83.23 Last: 185) +Model-Level : 183.0 +Problems : 67 (Average Length: 80.66 Splits: 0) +Lemmas : 520218 (Deleted: 481326) + Binary : 10396 (Ratio: 2.00%) + Ternary : 4130 (Ratio: 0.79%) + Conflict : 520218 (Average Length: 517.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 520218 (Average: 21.47 Max: 1455 Sum: 11168194) + Executed : 520061 (Average: 21.46 Max: 1455 Sum: 11162138 Ratio: 99.95%) + Bounded : 157 (Average: 38.57 Max: 117 Sum: 6056 Ratio: 0.05%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 902908 (Eliminated: 0 Frozen: 278344) +Constraints : 6624341 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1071MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 10.47s +Memory: 975MB (+0MB) +UNKNOWN +Iteration Time: 10.55s + +Iteration 67 +Queue: [(23,115,1,True)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 68 +Time : 582.335s (Solving: 550.02s 1st Model: 0.00s Unsat: 2.40s) +CPU Time : 582.364s + +Choices : 13088569 (Domain: 12752469) +Conflicts : 528948 (Analyzed: 528945) +Restarts : 6350 (Average: 83.30 Last: 185) +Model-Level : 183.0 +Problems : 68 (Average Length: 81.19 Splits: 0) +Lemmas : 528945 (Deleted: 490920) + Binary : 10750 (Ratio: 2.03%) + Ternary : 4323 (Ratio: 0.82%) + Conflict : 528945 (Average Length: 519.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 528945 (Average: 22.49 Max: 1562 Sum: 11896548) + Executed : 528788 (Average: 22.48 Max: 1562 Sum: 11890492 Ratio: 99.95%) + Bounded : 157 (Average: 38.57 Max: 117 Sum: 6056 Ratio: 0.05%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 902908 (Eliminated: 0 Frozen: 278344) +Constraints : 6624341 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1071MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 16.59s +Memory: 975MB (+0MB) +UNKNOWN +Iteration Time: 16.68s + +Iteration 68 +Queue: [(4,20,5,True), (5,25,5,True), (6,30,5,True), (7,35,4,True), (8,40,4,True), (9,45,4,True), (10,50,4,False), (11,55,3,True), (12,60,3,True), (13,65,3,False), (14,70,3,False), (15,75,3,False), (16,80,2,True), (17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Blocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 69 +Time : 588.065s (Solving: 555.53s 1st Model: 0.00s Unsat: 2.40s) +CPU Time : 588.088s + +Choices : 13146278 (Domain: 12810178) +Conflicts : 536554 (Analyzed: 536551) +Restarts : 6450 (Average: 83.19 Last: 185) +Model-Level : 183.0 +Problems : 69 (Average Length: 81.71 Splits: 0) +Lemmas : 536551 (Deleted: 496486) + Binary : 10836 (Ratio: 2.02%) + Ternary : 4334 (Ratio: 0.81%) + Conflict : 536551 (Average Length: 518.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 536551 (Average: 22.27 Max: 1562 Sum: 11946514) + Executed : 536393 (Average: 22.25 Max: 1562 Sum: 11940342 Ratio: 99.95%) + Bounded : 158 (Average: 39.06 Max: 117 Sum: 6172 Ratio: 0.05%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 902908 (Eliminated: 0 Frozen: 278344) +Constraints : 6624341 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1071MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 5.64s +Memory: 975MB (+0MB) +UNKNOWN +Iteration Time: 5.73s + +Iteration 69 +Queue: [(5,25,5,True), (6,30,5,True), (7,35,4,True), (8,40,4,True), (9,45,4,True), (10,50,4,False), (11,55,3,True), (12,60,3,True), (13,65,3,False), (14,70,3,False), (15,75,3,False), (16,80,2,True), (17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 70 +Time : 592.454s (Solving: 559.74s 1st Model: 0.00s Unsat: 2.40s) +CPU Time : 592.476s + +Choices : 13186477 (Domain: 12850377) +Conflicts : 544160 (Analyzed: 544157) +Restarts : 6550 (Average: 83.08 Last: 185) +Model-Level : 183.0 +Problems : 70 (Average Length: 82.21 Splits: 0) +Lemmas : 544157 (Deleted: 503845) + Binary : 10858 (Ratio: 2.00%) + Ternary : 4336 (Ratio: 0.80%) + Conflict : 544157 (Average Length: 517.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 544157 (Average: 22.01 Max: 1562 Sum: 11978079) + Executed : 543999 (Average: 22.00 Max: 1562 Sum: 11971907 Ratio: 99.95%) + Bounded : 158 (Average: 39.06 Max: 117 Sum: 6172 Ratio: 0.05%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 902908 (Eliminated: 0 Frozen: 278344) +Constraints : 6624341 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1071MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 4.33s +Memory: 975MB (+0MB) +UNKNOWN +Iteration Time: 4.39s + +Iteration 70 +Queue: [(6,30,5,True), (7,35,4,True), (8,40,4,True), (9,45,4,True), (10,50,4,False), (11,55,3,True), (12,60,3,True), (13,65,3,False), (14,70,3,False), (15,75,3,False), (16,80,2,True), (17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 71 +Time : 600.560s (Solving: 567.65s 1st Model: 0.00s Unsat: 2.40s) +CPU Time : 600.584s + +Choices : 13260918 (Domain: 12920098) +Conflicts : 552886 (Analyzed: 552883) +Restarts : 6650 (Average: 83.14 Last: 185) +Model-Level : 183.0 +Problems : 71 (Average Length: 82.70 Splits: 0) +Lemmas : 552883 (Deleted: 513368) + Binary : 10965 (Ratio: 1.98%) + Ternary : 4358 (Ratio: 0.79%) + Conflict : 552883 (Average Length: 520.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 552883 (Average: 21.77 Max: 1562 Sum: 12034743) + Executed : 552725 (Average: 21.76 Max: 1562 Sum: 12028571 Ratio: 99.95%) + Bounded : 158 (Average: 39.06 Max: 117 Sum: 6172 Ratio: 0.05%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 902908 (Eliminated: 0 Frozen: 278344) +Constraints : 6624341 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1071MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.04s +Memory: 975MB (+0MB) +UNKNOWN +Iteration Time: 8.11s + +Iteration 71 +Queue: [(7,35,4,True), (8,40,4,True), (9,45,4,True), (10,50,4,False), (11,55,3,True), (12,60,3,True), (13,65,3,False), (14,70,3,False), (15,75,3,False), (16,80,2,True), (17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 72 +Time : 605.272s (Solving: 572.15s 1st Model: 0.00s Unsat: 2.40s) +CPU Time : 605.296s + +Choices : 13317430 (Domain: 12975523) +Conflicts : 560480 (Analyzed: 560477) +Restarts : 6750 (Average: 83.03 Last: 185) +Model-Level : 183.0 +Problems : 72 (Average Length: 83.18 Splits: 0) +Lemmas : 560477 (Deleted: 519465) + Binary : 11030 (Ratio: 1.97%) + Ternary : 4396 (Ratio: 0.78%) + Conflict : 560477 (Average Length: 517.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 560477 (Average: 21.55 Max: 1562 Sum: 12080644) + Executed : 560319 (Average: 21.54 Max: 1562 Sum: 12074472 Ratio: 99.95%) + Bounded : 158 (Average: 39.06 Max: 117 Sum: 6172 Ratio: 0.05%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 902908 (Eliminated: 0 Frozen: 278344) +Constraints : 6624341 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1071MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 4.63s +Memory: 975MB (+0MB) +UNKNOWN +Iteration Time: 4.72s + +Iteration 72 +Queue: [(8,40,4,True), (9,45,4,True), (10,50,4,False), (11,55,3,True), (12,60,3,True), (13,65,3,False), (14,70,3,False), (15,75,3,False), (16,80,2,True), (17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 73 +Time : 612.491s (Solving: 579.19s 1st Model: 0.00s Unsat: 2.40s) +CPU Time : 612.516s + +Choices : 13399866 (Domain: 13057114) +Conflicts : 568275 (Analyzed: 568272) +Restarts : 6850 (Average: 82.96 Last: 185) +Model-Level : 183.0 +Problems : 73 (Average Length: 83.64 Splits: 0) +Lemmas : 568272 (Deleted: 526626) + Binary : 11227 (Ratio: 1.98%) + Ternary : 4486 (Ratio: 0.79%) + Conflict : 568272 (Average Length: 517.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 568272 (Average: 21.38 Max: 1562 Sum: 12150356) + Executed : 568113 (Average: 21.37 Max: 1562 Sum: 12144071 Ratio: 99.95%) + Bounded : 159 (Average: 39.53 Max: 117 Sum: 6285 Ratio: 0.05%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 902908 (Eliminated: 0 Frozen: 278344) +Constraints : 6624341 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1071MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.16s +Memory: 975MB (+0MB) +UNKNOWN +Iteration Time: 7.23s + +Iteration 73 +Queue: [(9,45,4,True), (10,50,4,False), (11,55,3,True), (12,60,3,True), (13,65,3,False), (14,70,3,False), (15,75,3,False), (16,80,2,True), (17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 74 +Time : 624.730s (Solving: 591.24s 1st Model: 0.00s Unsat: 2.40s) +CPU Time : 624.756s + +Choices : 13550436 (Domain: 13206308) +Conflicts : 576763 (Analyzed: 576760) +Restarts : 6950 (Average: 82.99 Last: 185) +Model-Level : 183.0 +Problems : 74 (Average Length: 84.09 Splits: 0) +Lemmas : 576760 (Deleted: 533795) + Binary : 11402 (Ratio: 1.98%) + Ternary : 4562 (Ratio: 0.79%) + Conflict : 576760 (Average Length: 523.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 576760 (Average: 21.29 Max: 1562 Sum: 12278204) + Executed : 576601 (Average: 21.28 Max: 1562 Sum: 12271919 Ratio: 99.95%) + Bounded : 159 (Average: 39.53 Max: 117 Sum: 6285 Ratio: 0.05%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 902908 (Eliminated: 0 Frozen: 278344) +Constraints : 6624341 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1071MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 12.17s +Memory: 975MB (+0MB) +UNKNOWN +Iteration Time: 12.24s + +Iteration 74 +Queue: [(11,55,3,True), (12,60,3,True), (13,65,3,False), (14,70,3,False), (15,75,3,False), (16,80,2,True), (17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 75 +Time : 639.378s (Solving: 605.69s 1st Model: 0.00s Unsat: 2.40s) +CPU Time : 639.408s + +Choices : 13754428 (Domain: 13408461) +Conflicts : 585767 (Analyzed: 585764) +Restarts : 7050 (Average: 83.09 Last: 185) +Model-Level : 183.0 +Problems : 75 (Average Length: 84.53 Splits: 0) +Lemmas : 585764 (Deleted: 543773) + Binary : 11646 (Ratio: 1.99%) + Ternary : 4656 (Ratio: 0.79%) + Conflict : 585764 (Average Length: 531.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 585764 (Average: 21.26 Max: 1562 Sum: 12452649) + Executed : 585605 (Average: 21.25 Max: 1562 Sum: 12446364 Ratio: 99.95%) + Bounded : 159 (Average: 39.53 Max: 117 Sum: 6285 Ratio: 0.05%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 902908 (Eliminated: 0 Frozen: 278344) +Constraints : 6624341 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1071MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 14.58s +Memory: 975MB (+0MB) +UNKNOWN +Iteration Time: 14.66s + +Iteration 75 +Queue: [(12,60,3,True), (13,65,3,False), (14,70,3,False), (15,75,3,False), (16,80,2,True), (17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 76 +Time : 653.162s (Solving: 619.29s 1st Model: 0.00s Unsat: 2.40s) +CPU Time : 653.196s + +Choices : 13957281 (Domain: 13609805) +Conflicts : 594135 (Analyzed: 594132) +Restarts : 7150 (Average: 83.10 Last: 185) +Model-Level : 183.0 +Problems : 76 (Average Length: 84.96 Splits: 0) +Lemmas : 594132 (Deleted: 550302) + Binary : 11820 (Ratio: 1.99%) + Ternary : 4704 (Ratio: 0.79%) + Conflict : 594132 (Average Length: 541.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 594132 (Average: 21.25 Max: 1562 Sum: 12625961) + Executed : 593973 (Average: 21.24 Max: 1562 Sum: 12619676 Ratio: 99.95%) + Bounded : 159 (Average: 39.53 Max: 117 Sum: 6285 Ratio: 0.05%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 902908 (Eliminated: 0 Frozen: 278344) +Constraints : 6624341 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1071MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 13.73s +Memory: 975MB (+0MB) +UNKNOWN +Iteration Time: 13.79s + +Iteration 76 +Queue: [(16,80,2,True), (17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 77 +Time : 667.620s (Solving: 633.54s 1st Model: 0.00s Unsat: 2.40s) +CPU Time : 667.660s + +Choices : 14229081 (Domain: 13878957) +Conflicts : 602414 (Analyzed: 602411) +Restarts : 7250 (Average: 83.09 Last: 185) +Model-Level : 183.0 +Problems : 77 (Average Length: 85.38 Splits: 0) +Lemmas : 602411 (Deleted: 558174) + Binary : 12049 (Ratio: 2.00%) + Ternary : 4758 (Ratio: 0.79%) + Conflict : 602411 (Average Length: 551.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 602411 (Average: 21.36 Max: 1562 Sum: 12866776) + Executed : 602252 (Average: 21.35 Max: 1562 Sum: 12860491 Ratio: 99.95%) + Bounded : 159 (Average: 39.53 Max: 117 Sum: 6285 Ratio: 0.05%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 902908 (Eliminated: 0 Frozen: 278344) +Constraints : 6624341 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1071MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 14.38s +Memory: 975MB (+0MB) +UNKNOWN +Iteration Time: 14.47s + +Iteration 77 +Queue: [(17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 78 +Time : 688.445s (Solving: 654.18s 1st Model: 0.00s Unsat: 2.40s) +CPU Time : 688.492s + +Choices : 14711711 (Domain: 14353351) +Conflicts : 611580 (Analyzed: 611577) +Restarts : 7350 (Average: 83.21 Last: 185) +Model-Level : 183.0 +Problems : 78 (Average Length: 85.78 Splits: 0) +Lemmas : 611577 (Deleted: 567670) + Binary : 12557 (Ratio: 2.05%) + Ternary : 4895 (Ratio: 0.80%) + Conflict : 611577 (Average Length: 564.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 611577 (Average: 21.74 Max: 1562 Sum: 13295201) + Executed : 611418 (Average: 21.73 Max: 1562 Sum: 13288916 Ratio: 99.95%) + Bounded : 159 (Average: 39.53 Max: 117 Sum: 6285 Ratio: 0.05%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 902908 (Eliminated: 0 Frozen: 278344) +Constraints : 6624341 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1071MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 20.77s +Memory: 975MB (+0MB) +UNKNOWN +Iteration Time: 20.84s + +Iteration 78 +Queue: [(4,20,6,True), (5,25,6,True), (6,30,6,True), (7,35,5,True), (8,40,5,True), (9,45,5,False), (10,50,4,True), (11,55,4,False), (12,60,4,False), (13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,3,False), (17,85,3,False), (18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Blocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 79 +Time : 694.262s (Solving: 659.80s 1st Model: 0.00s Unsat: 2.40s) +CPU Time : 694.312s + +Choices : 14768725 (Domain: 14410365) +Conflicts : 620106 (Analyzed: 620103) +Restarts : 7450 (Average: 83.24 Last: 185) +Model-Level : 183.0 +Problems : 79 (Average Length: 86.18 Splits: 0) +Lemmas : 620103 (Deleted: 574044) + Binary : 12611 (Ratio: 2.03%) + Ternary : 4906 (Ratio: 0.79%) + Conflict : 620103 (Average Length: 561.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 620103 (Average: 21.52 Max: 1562 Sum: 13342839) + Executed : 619944 (Average: 21.51 Max: 1562 Sum: 13336554 Ratio: 99.95%) + Bounded : 159 (Average: 39.53 Max: 117 Sum: 6285 Ratio: 0.05%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 902908 (Eliminated: 0 Frozen: 278344) +Constraints : 6624341 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1071MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 5.75s +Memory: 975MB (+0MB) +UNKNOWN +Iteration Time: 5.82s + +Iteration 79 +Queue: [(5,25,6,True), (6,30,6,True), (7,35,5,True), (8,40,5,True), (9,45,5,False), (10,50,4,True), (11,55,4,False), (12,60,4,False), (13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,3,False), (17,85,3,False), (18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 80 +Time : 697.964s (Solving: 663.32s 1st Model: 0.00s Unsat: 2.40s) +CPU Time : 698.016s + +Choices : 14803436 (Domain: 14445076) +Conflicts : 627340 (Analyzed: 627337) +Restarts : 7550 (Average: 83.09 Last: 185) +Model-Level : 183.0 +Problems : 80 (Average Length: 86.56 Splits: 0) +Lemmas : 627337 (Deleted: 582303) + Binary : 12618 (Ratio: 2.01%) + Ternary : 4907 (Ratio: 0.78%) + Conflict : 627337 (Average Length: 561.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 627337 (Average: 21.31 Max: 1562 Sum: 13368084) + Executed : 627177 (Average: 21.30 Max: 1562 Sum: 13361682 Ratio: 99.95%) + Bounded : 160 (Average: 40.01 Max: 117 Sum: 6402 Ratio: 0.05%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 902908 (Eliminated: 0 Frozen: 278344) +Constraints : 6624341 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1071MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 3.64s +Memory: 975MB (+0MB) +UNKNOWN +Iteration Time: 3.71s + +Iteration 80 +Queue: [(6,30,6,True), (7,35,5,True), (8,40,5,True), (9,45,5,False), (10,50,4,True), (11,55,4,False), (12,60,4,False), (13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,3,False), (17,85,3,False), (18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 81 +Time : 705.316s (Solving: 670.46s 1st Model: 0.00s Unsat: 2.40s) +CPU Time : 705.372s + +Choices : 14876037 (Domain: 14517677) +Conflicts : 635476 (Analyzed: 635473) +Restarts : 7650 (Average: 83.07 Last: 185) +Model-Level : 183.0 +Problems : 81 (Average Length: 86.94 Splits: 0) +Lemmas : 635473 (Deleted: 589436) + Binary : 12660 (Ratio: 1.99%) + Ternary : 4927 (Ratio: 0.78%) + Conflict : 635473 (Average Length: 561.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 635473 (Average: 21.13 Max: 1562 Sum: 13427038) + Executed : 635312 (Average: 21.12 Max: 1562 Sum: 13420519 Ratio: 99.95%) + Bounded : 161 (Average: 40.49 Max: 117 Sum: 6519 Ratio: 0.05%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 902908 (Eliminated: 0 Frozen: 278344) +Constraints : 6624315 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1071MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.27s +Memory: 975MB (+0MB) +UNKNOWN +Iteration Time: 7.36s + +Iteration 81 +Queue: [(7,35,5,True), (8,40,5,True), (9,45,5,False), (10,50,4,True), (11,55,4,False), (12,60,4,False), (13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,3,False), (17,85,3,False), (18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 82 +Time : 714.196s (Solving: 679.16s 1st Model: 0.00s Unsat: 2.40s) +CPU Time : 714.240s + +Choices : 14964621 (Domain: 14606225) +Conflicts : 644276 (Analyzed: 644273) +Restarts : 7750 (Average: 83.13 Last: 185) +Model-Level : 183.0 +Problems : 82 (Average Length: 87.30 Splits: 0) +Lemmas : 644273 (Deleted: 598824) + Binary : 12774 (Ratio: 1.98%) + Ternary : 4948 (Ratio: 0.77%) + Conflict : 644273 (Average Length: 560.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 644273 (Average: 20.95 Max: 1562 Sum: 13499468) + Executed : 644112 (Average: 20.94 Max: 1562 Sum: 13492949 Ratio: 99.95%) + Bounded : 161 (Average: 40.49 Max: 117 Sum: 6519 Ratio: 0.05%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 902908 (Eliminated: 0 Frozen: 278344) +Constraints : 6624301 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1071MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.80s +Memory: 975MB (+0MB) +UNKNOWN +Iteration Time: 8.87s + +Iteration 82 +Queue: [(8,40,5,True), (9,45,5,False), (10,50,4,True), (11,55,4,False), (12,60,4,False), (13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,3,False), (17,85,3,False), (18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 83 +Time : 721.282s (Solving: 686.07s 1st Model: 0.00s Unsat: 2.40s) +CPU Time : 721.328s + +Choices : 15037395 (Domain: 14677670) +Conflicts : 652050 (Analyzed: 652047) +Restarts : 7850 (Average: 83.06 Last: 185) +Model-Level : 183.0 +Problems : 83 (Average Length: 87.66 Splits: 0) +Lemmas : 652047 (Deleted: 605184) + Binary : 12879 (Ratio: 1.98%) + Ternary : 4985 (Ratio: 0.76%) + Conflict : 652047 (Average Length: 564.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 652047 (Average: 20.79 Max: 1562 Sum: 13555664) + Executed : 651885 (Average: 20.78 Max: 1562 Sum: 13549032 Ratio: 99.95%) + Bounded : 162 (Average: 40.94 Max: 117 Sum: 6632 Ratio: 0.05%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 902908 (Eliminated: 0 Frozen: 278344) +Constraints : 6624301 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1071MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.03s +Memory: 975MB (+0MB) +UNKNOWN +Iteration Time: 7.09s + +Iteration 83 +Queue: [(10,50,4,True), (11,55,4,False), (12,60,4,False), (13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,3,False), (17,85,3,False), (18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 84 +Time : 735.705s (Solving: 700.30s 1st Model: 0.00s Unsat: 2.40s) +CPU Time : 735.756s + +Choices : 15211825 (Domain: 14851226) +Conflicts : 660424 (Analyzed: 660421) +Restarts : 7950 (Average: 83.07 Last: 185) +Model-Level : 183.0 +Problems : 84 (Average Length: 88.01 Splits: 0) +Lemmas : 660421 (Deleted: 612860) + Binary : 13052 (Ratio: 1.98%) + Ternary : 5021 (Ratio: 0.76%) + Conflict : 660421 (Average Length: 574.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 660421 (Average: 20.75 Max: 1562 Sum: 13701359) + Executed : 660259 (Average: 20.74 Max: 1562 Sum: 13694727 Ratio: 99.95%) + Bounded : 162 (Average: 40.94 Max: 117 Sum: 6632 Ratio: 0.05%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 902908 (Eliminated: 0 Frozen: 278344) +Constraints : 6624301 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1071MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 14.36s +Memory: 975MB (+0MB) +UNKNOWN +Iteration Time: 14.43s + +Iteration 84 +Queue: [(13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,3,False), (17,85,3,False), (18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 85 +Time : 749.084s (Solving: 713.49s 1st Model: 0.00s Unsat: 2.40s) +CPU Time : 749.124s + +Choices : 15373876 (Domain: 15012894) +Conflicts : 668679 (Analyzed: 668676) +Restarts : 8050 (Average: 83.07 Last: 185) +Model-Level : 183.0 +Problems : 85 (Average Length: 88.35 Splits: 0) +Lemmas : 668676 (Deleted: 620912) + Binary : 13146 (Ratio: 1.97%) + Ternary : 5041 (Ratio: 0.75%) + Conflict : 668676 (Average Length: 586.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 668676 (Average: 20.69 Max: 1562 Sum: 13833507) + Executed : 668514 (Average: 20.68 Max: 1562 Sum: 13826875 Ratio: 99.95%) + Bounded : 162 (Average: 40.94 Max: 117 Sum: 6632 Ratio: 0.05%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 902908 (Eliminated: 0 Frozen: 278344) +Constraints : 6624301 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1071MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 13.30s +Memory: 975MB (+0MB) +UNKNOWN +Iteration Time: 13.37s + +Iteration 85 +Queue: [(18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 86 +Time : 763.386s (Solving: 727.61s 1st Model: 0.00s Unsat: 2.40s) +CPU Time : 763.432s + +Choices : 15536270 (Domain: 15175157) +Conflicts : 677036 (Analyzed: 677033) +Restarts : 8150 (Average: 83.07 Last: 185) +Model-Level : 183.0 +Problems : 86 (Average Length: 88.69 Splits: 0) +Lemmas : 677033 (Deleted: 628936) + Binary : 13199 (Ratio: 1.95%) + Ternary : 5046 (Ratio: 0.75%) + Conflict : 677033 (Average Length: 605.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 677033 (Average: 20.62 Max: 1562 Sum: 13957955) + Executed : 676871 (Average: 20.61 Max: 1562 Sum: 13951323 Ratio: 99.95%) + Bounded : 162 (Average: 40.94 Max: 117 Sum: 6632 Ratio: 0.05%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 902908 (Eliminated: 0 Frozen: 278344) +Constraints : 6624301 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1071MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 14.24s +Memory: 975MB (+0MB) +UNKNOWN +Iteration Time: 14.31s + +Iteration 86 +Queue: [(4,20,7,True), (5,25,7,True), (6,30,7,False), (7,35,6,True), (8,40,6,False), (9,45,5,True), (10,50,5,False), (11,55,4,True), (12,60,4,False), (13,65,4,False), (14,70,3,True), (15,75,3,True), (16,80,3,False), (17,85,3,False), (18,90,3,False), (19,95,2,True), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Blocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 87 +Time : 769.775s (Solving: 733.81s 1st Model: 0.00s Unsat: 2.40s) +CPU Time : 769.828s + +Choices : 15591549 (Domain: 15230434) +Conflicts : 684391 (Analyzed: 684388) +Restarts : 8250 (Average: 82.96 Last: 185) +Model-Level : 183.0 +Problems : 87 (Average Length: 89.01 Splits: 0) +Lemmas : 684388 (Deleted: 637148) + Binary : 13249 (Ratio: 1.94%) + Ternary : 5048 (Ratio: 0.74%) + Conflict : 684388 (Average Length: 601.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 684388 (Average: 20.44 Max: 1562 Sum: 13987653) + Executed : 684226 (Average: 20.43 Max: 1562 Sum: 13981021 Ratio: 99.95%) + Bounded : 162 (Average: 40.94 Max: 117 Sum: 6632 Ratio: 0.05%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 902908 (Eliminated: 0 Frozen: 278344) +Constraints : 6624301 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1071MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.32s +Memory: 975MB (+0MB) +UNKNOWN +Iteration Time: 6.40s + +Iteration 87 +Queue: [(5,25,7,True), (6,30,7,False), (7,35,6,True), (8,40,6,False), (9,45,5,True), (10,50,5,False), (11,55,4,True), (12,60,4,False), (13,65,4,False), (14,70,3,True), (15,75,3,True), (16,80,3,False), (17,85,3,False), (18,90,3,False), (19,95,2,True), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 88 +Time : 773.674s (Solving: 737.53s 1st Model: 0.00s Unsat: 2.40s) +CPU Time : 773.728s + +Choices : 15625291 (Domain: 15264176) +Conflicts : 691658 (Analyzed: 691655) +Restarts : 8350 (Average: 82.83 Last: 185) +Model-Level : 183.0 +Problems : 88 (Average Length: 89.33 Splits: 0) +Lemmas : 691655 (Deleted: 644095) + Binary : 13256 (Ratio: 1.92%) + Ternary : 5049 (Ratio: 0.73%) + Conflict : 691655 (Average Length: 599.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 691655 (Average: 20.26 Max: 1562 Sum: 14012397) + Executed : 691493 (Average: 20.25 Max: 1562 Sum: 14005765 Ratio: 99.95%) + Bounded : 162 (Average: 40.94 Max: 117 Sum: 6632 Ratio: 0.05%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 902908 (Eliminated: 0 Frozen: 278344) +Constraints : 6624301 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1071MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 3.84s +Memory: 975MB (+0MB) +UNKNOWN +Iteration Time: 3.90s + +Iteration 88 +Queue: [(7,35,6,True), (8,40,6,False), (9,45,5,True), (10,50,5,False), (11,55,4,True), (12,60,4,False), (13,65,4,False), (14,70,3,True), (15,75,3,True), (16,80,3,False), (17,85,3,False), (18,90,3,False), (19,95,2,True), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 89 +Time : 783.702s (Solving: 747.38s 1st Model: 0.00s Unsat: 2.40s) +CPU Time : 783.760s + +Choices : 15701115 (Domain: 15340000) +Conflicts : 700133 (Analyzed: 700130) +Restarts : 8450 (Average: 82.86 Last: 185) +Model-Level : 183.0 +Problems : 89 (Average Length: 89.64 Splits: 0) +Lemmas : 700130 (Deleted: 651507) + Binary : 13411 (Ratio: 1.92%) + Ternary : 5069 (Ratio: 0.72%) + Conflict : 700130 (Average Length: 605.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 700130 (Average: 20.10 Max: 1562 Sum: 14069643) + Executed : 699968 (Average: 20.09 Max: 1562 Sum: 14063011 Ratio: 99.95%) + Bounded : 162 (Average: 40.94 Max: 117 Sum: 6632 Ratio: 0.05%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 902908 (Eliminated: 0 Frozen: 278344) +Constraints : 6624301 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1071MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.97s +Memory: 975MB (+0MB) +UNKNOWN +Iteration Time: 10.03s + +Iteration 89 +Queue: [(9,45,5,True), (10,50,5,False), (11,55,4,True), (12,60,4,False), (13,65,4,False), (14,70,3,True), (15,75,3,True), (16,80,3,False), (17,85,3,False), (18,90,3,False), (19,95,2,True), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 90 +Time : 798.822s (Solving: 762.31s 1st Model: 0.00s Unsat: 2.40s) +CPU Time : 798.888s + +Choices : 15834625 (Domain: 15472834) +Conflicts : 708742 (Analyzed: 708739) +Restarts : 8550 (Average: 82.89 Last: 185) +Model-Level : 183.0 +Problems : 90 (Average Length: 89.94 Splits: 0) +Lemmas : 708739 (Deleted: 659396) + Binary : 13646 (Ratio: 1.93%) + Ternary : 5096 (Ratio: 0.72%) + Conflict : 708739 (Average Length: 620.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 708739 (Average: 20.00 Max: 1562 Sum: 14174053) + Executed : 708577 (Average: 19.99 Max: 1562 Sum: 14167421 Ratio: 99.95%) + Bounded : 162 (Average: 40.94 Max: 117 Sum: 6632 Ratio: 0.05%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 902908 (Eliminated: 0 Frozen: 278344) +Constraints : 6624301 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1071MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 15.06s +Memory: 975MB (+0MB) +UNKNOWN +Iteration Time: 15.13s + +Iteration 90 +Queue: [(11,55,4,True), (12,60,4,False), (13,65,4,False), (14,70,3,True), (15,75,3,True), (16,80,3,False), (17,85,3,False), (18,90,3,False), (19,95,2,True), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 91 +Time : 810.135s (Solving: 773.44s 1st Model: 0.00s Unsat: 2.40s) +CPU Time : 810.204s + +Choices : 16005985 (Domain: 15642429) +Conflicts : 717486 (Analyzed: 717483) +Restarts : 8650 (Average: 82.95 Last: 185) +Model-Level : 183.0 +Problems : 91 (Average Length: 90.24 Splits: 0) +Lemmas : 717483 (Deleted: 669731) + Binary : 13747 (Ratio: 1.92%) + Ternary : 5143 (Ratio: 0.72%) + Conflict : 717483 (Average Length: 620.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 717483 (Average: 19.96 Max: 1562 Sum: 14324454) + Executed : 717321 (Average: 19.96 Max: 1562 Sum: 14317822 Ratio: 99.95%) + Bounded : 162 (Average: 40.94 Max: 117 Sum: 6632 Ratio: 0.05%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 902908 (Eliminated: 0 Frozen: 278344) +Constraints : 6624301 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1071MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 11.25s +Memory: 975MB (+0MB) +UNKNOWN +Iteration Time: 11.32s + +Iteration 91 +Queue: [(14,70,3,True), (15,75,3,True), (16,80,3,False), (17,85,3,False), (18,90,3,False), (19,95,2,True), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 92 +Time : 819.691s (Solving: 782.77s 1st Model: 0.00s Unsat: 2.40s) +CPU Time : 819.764s + +Choices : 16161851 (Domain: 15797917) +Conflicts : 725743 (Analyzed: 725740) +Restarts : 8750 (Average: 82.94 Last: 185) +Model-Level : 183.0 +Problems : 92 (Average Length: 90.53 Splits: 0) +Lemmas : 725740 (Deleted: 676141) + Binary : 13781 (Ratio: 1.90%) + Ternary : 5172 (Ratio: 0.71%) + Conflict : 725740 (Average Length: 621.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 725740 (Average: 19.92 Max: 1562 Sum: 14457524) + Executed : 725578 (Average: 19.91 Max: 1562 Sum: 14450892 Ratio: 99.95%) + Bounded : 162 (Average: 40.94 Max: 117 Sum: 6632 Ratio: 0.05%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 902908 (Eliminated: 0 Frozen: 278344) +Constraints : 6624301 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1071MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.47s +Memory: 975MB (+0MB) +UNKNOWN +Iteration Time: 9.56s + +Iteration 92 +Queue: [(15,75,3,True), (16,80,3,False), (17,85,3,False), (18,90,3,False), (19,95,2,True), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 93 +Time : 826.658s (Solving: 789.53s 1st Model: 0.00s Unsat: 2.40s) +CPU Time : 826.736s + +Choices : 16291240 (Domain: 15926314) +Conflicts : 733422 (Analyzed: 733419) +Restarts : 8850 (Average: 82.87 Last: 185) +Model-Level : 183.0 +Problems : 93 (Average Length: 90.82 Splits: 0) +Lemmas : 733419 (Deleted: 684072) + Binary : 13809 (Ratio: 1.88%) + Ternary : 5182 (Ratio: 0.71%) + Conflict : 733419 (Average Length: 619.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 733419 (Average: 19.86 Max: 1562 Sum: 14566457) + Executed : 733257 (Average: 19.85 Max: 1562 Sum: 14559825 Ratio: 99.95%) + Bounded : 162 (Average: 40.94 Max: 117 Sum: 6632 Ratio: 0.05%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 902908 (Eliminated: 0 Frozen: 278344) +Constraints : 6624301 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1071MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.89s +Memory: 975MB (+0MB) +UNKNOWN +Iteration Time: 6.97s + +Iteration 93 +Queue: [(19,95,2,True), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 94 +Time : 835.736s (Solving: 798.43s 1st Model: 0.00s Unsat: 2.40s) +CPU Time : 835.808s + +Choices : 16464509 (Domain: 16099110) +Conflicts : 741679 (Analyzed: 741676) +Restarts : 8950 (Average: 82.87 Last: 185) +Model-Level : 183.0 +Problems : 94 (Average Length: 91.10 Splits: 0) +Lemmas : 741676 (Deleted: 691616) + Binary : 13833 (Ratio: 1.87%) + Ternary : 5187 (Ratio: 0.70%) + Conflict : 741676 (Average Length: 620.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 741676 (Average: 19.84 Max: 1562 Sum: 14715303) + Executed : 741513 (Average: 19.83 Max: 1562 Sum: 14708554 Ratio: 99.95%) + Bounded : 163 (Average: 41.40 Max: 117 Sum: 6749 Ratio: 0.05%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 902908 (Eliminated: 0 Frozen: 278344) +Constraints : 6624301 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1071MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 9.01s +Memory: 975MB (+0MB) +UNKNOWN +Iteration Time: 9.07s + +Iteration 94 +Queue: [(4,20,8,True), (5,25,8,True), (6,30,7,True), (7,35,7,True), (8,40,6,True), (9,45,6,False), (10,50,5,True), (11,55,5,False), (12,60,4,True), (13,65,4,False), (14,70,4,False), (15,75,4,False), (16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,True), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Blocking actions... +Solving... +[start: stats after solve call] + +Models : 0 +Calls : 95 +Time : 843.746s (Solving: 806.25s 1st Model: 0.00s Unsat: 10.22s) +CPU Time : 843.820s + +Choices : 16496702 (Domain: 16131303) +Conflicts : 746118 (Analyzed: 746114) +Restarts : 9002 (Average: 82.88 Last: 185) +Model-Level : 183.0 +Problems : 95 (Average Length: 91.37 Splits: 0) +Lemmas : 746114 (Deleted: 696156) + Binary : 13909 (Ratio: 1.86%) + Ternary : 5196 (Ratio: 0.70%) + Conflict : 746114 (Average Length: 618.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 746114 (Average: 19.76 Max: 1562 Sum: 14746605) + Executed : 745949 (Average: 19.76 Max: 1562 Sum: 14739854 Ratio: 99.95%) + Bounded : 165 (Average: 40.92 Max: 117 Sum: 6751 Ratio: 0.05%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 902908 (Eliminated: 0 Frozen: 278344) +Constraints : 6624275 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1071MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 7.94s +Memory: 975MB (+0MB) +UNSAT +Iteration Time: 8.02s + +Iteration 95 +Queue: [(5,25,8,True), (6,30,7,True), (7,35,7,True), (8,40,6,True), (9,45,6,False), (10,50,5,True), (11,55,5,False), (12,60,4,True), (13,65,4,False), (14,70,4,False), (15,75,4,False), (16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,True), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 96 +Time : 846.967s (Solving: 809.29s 1st Model: 0.00s Unsat: 10.22s) +CPU Time : 847.044s + +Choices : 16532716 (Domain: 16167317) +Conflicts : 753267 (Analyzed: 753263) +Restarts : 9102 (Average: 82.76 Last: 185) +Model-Level : 183.0 +Problems : 96 (Average Length: 91.64 Splits: 0) +Lemmas : 753263 (Deleted: 703244) + Binary : 13916 (Ratio: 1.85%) + Ternary : 5197 (Ratio: 0.69%) + Conflict : 753263 (Average Length: 615.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 753263 (Average: 19.61 Max: 1562 Sum: 14773887) + Executed : 753098 (Average: 19.60 Max: 1562 Sum: 14767136 Ratio: 99.95%) + Bounded : 165 (Average: 40.92 Max: 117 Sum: 6751 Ratio: 0.05%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 902908 (Eliminated: 0 Frozen: 278344) +Constraints : 6624275 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1071MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 3.16s +Memory: 975MB (+0MB) +UNKNOWN +Iteration Time: 3.23s + +Iteration 96 +Queue: [(6,30,7,True), (7,35,7,True), (8,40,6,True), (9,45,6,False), (10,50,5,True), (11,55,5,False), (12,60,4,True), (13,65,4,False), (14,70,4,False), (15,75,4,False), (16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,True), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 97 +Time : 860.534s (Solving: 822.67s 1st Model: 0.00s Unsat: 10.22s) +CPU Time : 860.616s + +Choices : 16617579 (Domain: 16252173) +Conflicts : 761752 (Analyzed: 761748) +Restarts : 9202 (Average: 82.78 Last: 185) +Model-Level : 183.0 +Problems : 97 (Average Length: 91.90 Splits: 0) +Lemmas : 761748 (Deleted: 710889) + Binary : 13978 (Ratio: 1.83%) + Ternary : 5219 (Ratio: 0.69%) + Conflict : 761748 (Average Length: 623.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 761748 (Average: 19.48 Max: 1562 Sum: 14839853) + Executed : 761583 (Average: 19.47 Max: 1562 Sum: 14833102 Ratio: 99.95%) + Bounded : 165 (Average: 40.92 Max: 117 Sum: 6751 Ratio: 0.05%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 902908 (Eliminated: 0 Frozen: 278344) +Constraints : 6624275 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1071MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 13.50s +Memory: 975MB (+0MB) +UNKNOWN +Iteration Time: 13.57s + +Iteration 97 +Queue: [(7,35,7,True), (8,40,6,True), (9,45,6,False), (10,50,5,True), (11,55,5,False), (12,60,4,True), (13,65,4,False), (14,70,4,False), (15,75,4,False), (16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,True), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 98 +Time : 866.128s (Solving: 828.05s 1st Model: 0.00s Unsat: 10.22s) +CPU Time : 866.212s + +Choices : 16671064 (Domain: 16305658) +Conflicts : 769396 (Analyzed: 769392) +Restarts : 9302 (Average: 82.71 Last: 185) +Model-Level : 183.0 +Problems : 98 (Average Length: 92.15 Splits: 0) +Lemmas : 769392 (Deleted: 719004) + Binary : 13992 (Ratio: 1.82%) + Ternary : 5225 (Ratio: 0.68%) + Conflict : 769392 (Average Length: 621.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 769392 (Average: 19.34 Max: 1562 Sum: 14878825) + Executed : 769227 (Average: 19.33 Max: 1562 Sum: 14872074 Ratio: 99.95%) + Bounded : 165 (Average: 40.92 Max: 117 Sum: 6751 Ratio: 0.05%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 902908 (Eliminated: 0 Frozen: 278344) +Constraints : 6624275 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1071MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 5.51s +Memory: 975MB (+0MB) +UNKNOWN +Iteration Time: 5.60s + +Iteration 98 +Queue: [(8,40,6,True), (9,45,6,False), (10,50,5,True), (11,55,5,False), (12,60,4,True), (13,65,4,False), (14,70,4,False), (15,75,4,False), (16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,True), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 99 +Time : 874.300s (Solving: 836.02s 1st Model: 0.00s Unsat: 10.22s) +CPU Time : 874.388s + +Choices : 16771158 (Domain: 16405189) +Conflicts : 777657 (Analyzed: 777653) +Restarts : 9402 (Average: 82.71 Last: 185) +Model-Level : 183.0 +Problems : 99 (Average Length: 92.40 Splits: 0) +Lemmas : 777653 (Deleted: 726455) + Binary : 14083 (Ratio: 1.81%) + Ternary : 5235 (Ratio: 0.67%) + Conflict : 777653 (Average Length: 621.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 777653 (Average: 19.23 Max: 1562 Sum: 14957932) + Executed : 777488 (Average: 19.23 Max: 1562 Sum: 14951181 Ratio: 99.95%) + Bounded : 165 (Average: 40.92 Max: 117 Sum: 6751 Ratio: 0.05%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 902908 (Eliminated: 0 Frozen: 278344) +Constraints : 6624275 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1071MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 8.10s +Memory: 975MB (+0MB) +UNKNOWN +Iteration Time: 8.18s + +Iteration 99 +Queue: [(10,50,5,True), (11,55,5,False), (12,60,4,True), (13,65,4,False), (14,70,4,False), (15,75,4,False), (16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,True), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 100 +Time : 888.923s (Solving: 850.46s 1st Model: 0.00s Unsat: 10.22s) +CPU Time : 889.016s + +Choices : 16945498 (Domain: 16578149) +Conflicts : 786145 (Analyzed: 786141) +Restarts : 9502 (Average: 82.73 Last: 185) +Model-Level : 183.0 +Problems : 100 (Average Length: 92.65 Splits: 0) +Lemmas : 786141 (Deleted: 734313) + Binary : 14299 (Ratio: 1.82%) + Ternary : 5281 (Ratio: 0.67%) + Conflict : 786141 (Average Length: 624.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 786141 (Average: 19.21 Max: 1562 Sum: 15101934) + Executed : 785976 (Average: 19.20 Max: 1562 Sum: 15095183 Ratio: 99.96%) + Bounded : 165 (Average: 40.92 Max: 117 Sum: 6751 Ratio: 0.04%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 902908 (Eliminated: 0 Frozen: 278344) +Constraints : 6624275 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1071MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 14.56s +Memory: 975MB (+0MB) +UNKNOWN +Iteration Time: 14.63s + +Iteration 100 +Queue: [(12,60,4,True), (13,65,4,False), (14,70,4,False), (15,75,4,False), (16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,True), (22,110,2,False), (23,115,2,False)] +Grounded Until: 115 +Unblocking actions... +Solving... +*** Info : (planner): INTERRUPTED by signal! +UNKNOWN + +INTERRUPTED : 1 + +Models : 0+ +Calls : 101 +Time : 892.583s (Solving: 853.91s 1st Model: 0.00s Unsat: 10.22s) +CPU Time : 892.652s + +Choices : 16998304 (Domain: 16630745) +Conflicts : 788629 (Analyzed: 788625) +Restarts : 9529 (Average: 82.76 Last: 185) +Model-Level : 183.0 +Problems : 101 (Average Length: 92.89 Splits: 0) +Lemmas : 788625 (Deleted: 738218) + Binary : 14320 (Ratio: 1.82%) + Ternary : 5287 (Ratio: 0.67%) + Conflict : 788625 (Average Length: 624.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 788625 (Average: 19.21 Max: 1562 Sum: 15147547) + Executed : 788460 (Average: 19.20 Max: 1562 Sum: 15140796 Ratio: 99.96%) + Bounded : 165 (Average: 40.92 Max: 117 Sum: 6751 Ratio: 0.04%) + +Rules : 91724 (Original: 89679) +Atoms : 73746 +Bodies : 16519 (Original: 14473) + Count : 330 (Original: 739) +Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443) +Tight : Yes +Variables : 902908 (Eliminated: 0 Frozen: 278344) +Constraints : 6624275 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) + +Memory Peak : 1071MB +Max. Length : 115 steps +Models : 1 + +