From a69a29636e6b46ae3343758fcdb5016be2657460 Mon Sep 17 00:00:00 2001 From: potassco-bot Date: Sun, 18 Feb 2018 19:03:58 +0100 Subject: [PATCH] Add benchmark result [gc-ta1-tt1-single-shot | ipc-2011 | barman-sequential-satisficing | 7] --- ...c-2011_barman-sequential-satisficing_7.env | 60 + ...c-2011_barman-sequential-satisficing_7.err | 8 + ...c-2011_barman-sequential-satisficing_7.out | 1963 +++++++++++++++++ 3 files changed, 2031 insertions(+) create mode 100644 gc-ta1-tt1-single-shot/ipc-2011_barman-sequential-satisficing_7.env create mode 100644 gc-ta1-tt1-single-shot/ipc-2011_barman-sequential-satisficing_7.err create mode 100644 gc-ta1-tt1-single-shot/ipc-2011_barman-sequential-satisficing_7.out diff --git a/gc-ta1-tt1-single-shot/ipc-2011_barman-sequential-satisficing_7.env b/gc-ta1-tt1-single-shot/ipc-2011_barman-sequential-satisficing_7.env new file mode 100644 index 000000000..8f8f2c846 --- /dev/null +++ b/gc-ta1-tt1-single-shot/ipc-2011_barman-sequential-satisficing_7.env @@ -0,0 +1,60 @@ +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-7.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 +- -i 0 +- -F 115 +- -T 115 +configuration: + fixedHorizon: true + id: gc-ta1-tt1-single-shot + 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 + - -i 0 +exitCode: 0 +instance: + domain: barman-sequential-satisficing + instance: 7 + ipc: ipc-2011 + planLength: 115 +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-single-shot/ipc-2011_barman-sequential-satisficing_7.err b/gc-ta1-tt1-single-shot/ipc-2011_barman-sequential-satisficing_7.err new file mode 100644 index 000000000..51e97d6fb --- /dev/null +++ b/gc-ta1-tt1-single-shot/ipc-2011_barman-sequential-satisficing_7.err @@ -0,0 +1,8 @@ +# configuration: {'id': 'gc-ta1-tt1-single-shot', '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', '-i 0'], 'instanceSets': ['rintanen-aij-2012-interesting'], 'fixedHorizon': True} +# instance: {'ipc': 'ipc-2011', 'domain': 'barman-sequential-satisficing', 'instance': 7, 'planLength': 115} +# 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-7.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', '-i 0', '-F 115', '-T 115'] +# working directory: /home/pluehne/Documents/ASP/plasp-javier/encodings/planner +# exit code: 0 +TIMEOUT CPU 900.11 MEM 1000140 MAXMEM 1000140 STALE 0 MAXMEM_RSS 873232 + + diff --git a/gc-ta1-tt1-single-shot/ipc-2011_barman-sequential-satisficing_7.out b/gc-ta1-tt1-single-shot/ipc-2011_barman-sequential-satisficing_7.out new file mode 100644 index 000000000..ed59c210b --- /dev/null +++ b/gc-ta1-tt1-single-shot/ipc-2011_barman-sequential-satisficing_7.out @@ -0,0 +1,1963 @@ +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-7.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-7.pddl +Parsing... +Parsing: [0.040s CPU, 0.041s wall-clock] +Normalizing task... [0.000s CPU, 0.003s wall-clock] +Instantiating... +Generating Datalog program... [0.010s CPU, 0.010s wall-clock] +Normalizing Datalog program... +Normalizing Datalog program: [0.050s CPU, 0.052s wall-clock] +Preparing model... [0.030s CPU, 0.026s wall-clock] +Generated 115 rules. +Computing model... [0.370s CPU, 0.374s wall-clock] +2300 relevant atoms +2393 auxiliary atoms +4693 final queue length +8087 total queue pushes +Completing instantiation... [0.690s CPU, 0.687s wall-clock] +Instantiating: [1.150s CPU, 1.155s wall-clock] +Computing fact groups... +Finding invariants... +24 initial candidates +Finding invariants: [0.120s CPU, 0.117s wall-clock] +Checking invariant weight... [0.000s CPU, 0.001s wall-clock] +Instantiating groups... [0.010s CPU, 0.007s wall-clock] +Collecting mutex groups... [0.000s CPU, 0.001s wall-clock] +Choosing groups... +238 uncovered facts +Choosing groups: [0.000s CPU, 0.001s wall-clock] +Building translation key... [0.000s CPU, 0.009s wall-clock] +Computing fact groups: [0.150s CPU, 0.152s wall-clock] +Building STRIPS to SAS dictionary... [0.000s CPU, 0.002s wall-clock] +Building dictionary for full mutex groups... [0.010s CPU, 0.002s wall-clock] +Building mutex information... +Building mutex information: [0.000s CPU, 0.003s wall-clock] +Translating task... +Processing axioms... +Simplifying axioms... [0.000s CPU, 0.000s wall-clock] +Processing axioms: [0.040s CPU, 0.040s wall-clock] +Translating task: [0.730s CPU, 0.725s wall-clock] +2672 effect conditions simplified +0 implied preconditions added +Detecting unreachable propositions... +0 operators removed +0 axioms removed +3 propositions removed +Detecting unreachable propositions: [0.350s CPU, 0.356s wall-clock] +Reordering and filtering variables... +241 of 241 variables necessary. +12 of 15 mutex groups necessary. +1596 of 1596 operators necessary. +0 of 0 axiom rules necessary. +Reordering and filtering variables: [0.250s CPU, 0.241s wall-clock] +Translator variables: 241 +Translator derived variables: 0 +Translator facts: 505 +Translator goal facts: 10 +Translator mutex groups: 12 +Translator total mutex groups size: 36 +Translator operators: 1596 +Translator axioms: 0 +Translator task size: 15302 +Translator peak memory: 45260 KB +Writing output... [0.260s CPU, 0.277s wall-clock] +Done! [2.960s CPU, 2.986s wall-clock] +planner.py version 0.0.1 + +Time: 0.61s +Memory: 91MB + +Iteration 1 +Queue: [(0,115,0,True)] +Grounded Until: 0 +Expected Memory: 91MB +Grounding... [('step', [1]), ('step', [2]), ('step', [3]), ('step', [4]), ('step', [5]), ('step', [6]), ('step', [7]), ('step', [8]), ('step', [9]), ('step', [10]), ('step', [11]), ('step', [12]), ('step', [13]), ('step', [14]), ('step', [15]), ('step', [16]), ('step', [17]), ('step', [18]), ('step', [19]), ('step', [20]), ('step', [21]), ('step', [22]), ('step', [23]), ('step', [24]), ('step', [25]), ('step', [26]), ('step', [27]), ('step', [28]), ('step', [29]), ('step', [30]), ('step', [31]), ('step', [32]), ('step', [33]), ('step', [34]), ('step', [35]), ('step', [36]), ('step', [37]), ('step', [38]), ('step', [39]), ('step', [40]), ('step', [41]), ('step', [42]), ('step', [43]), ('step', [44]), ('step', [45]), ('step', [46]), ('step', [47]), ('step', [48]), ('step', [49]), ('step', [50]), ('step', [51]), ('step', [52]), ('step', [53]), ('step', [54]), ('step', [55]), ('step', [56]), ('step', [57]), ('step', [58]), ('step', [59]), ('step', [60]), ('step', [61]), ('step', [62]), ('step', [63]), ('step', [64]), ('step', [65]), ('step', [66]), ('step', [67]), ('step', [68]), ('step', [69]), ('step', [70]), ('step', [71]), ('step', [72]), ('step', [73]), ('step', [74]), ('step', [75]), ('step', [76]), ('step', [77]), ('step', [78]), ('step', [79]), ('step', [80]), ('step', [81]), ('step', [82]), ('step', [83]), ('step', [84]), ('step', [85]), ('step', [86]), ('step', [87]), ('step', [88]), ('step', [89]), ('step', [90]), ('step', [91]), ('step', [92]), ('step', [93]), ('step', [94]), ('step', [95]), ('step', [96]), ('step', [97]), ('step', [98]), ('step', [99]), ('step', [100]), ('step', [101]), ('step', [102]), ('step', [103]), ('step', [104]), ('step', [105]), ('step', [106]), ('step', [107]), ('step', [108]), ('step', [109]), ('step', [110]), ('step', [111]), ('step', [112]), ('step', [113]), ('step', [114]), ('step', [115]), ('check', [115])] +Grounding Time: 5.31s +Memory: 572MB (+481MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 1+ +Calls : 1 +Time : 9.213s (Solving: 0.13s 1st Model: 0.11s Unsat: 0.00s) +CPU Time : 9.112s + +Choices : 21092 (Domain: 20732) +Conflicts : 67 (Analyzed: 67) +Restarts : 0 +Model-Level : 4372.0 +Problems : 1 (Average Length: 117.00 Splits: 0) +Lemmas : 67 (Deleted: 0) + Binary : 15 (Ratio: 22.39%) + Ternary : 0 (Ratio: 0.00%) + Conflict : 67 (Average Length: 47.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 67 (Average: 251.30 Max: 1731 Sum: 16837) + Executed : 67 (Average: 251.30 Max: 1731 Sum: 16837 Ratio: 100.00%) + Bounded : 0 (Average: 0.00 Max: 0 Sum: 0 Ratio: 0.00%) + +Rules : 0 +Atoms : 0 +Bodies : 0 +Tight : Yes +Variables : 322038 (Eliminated: 0 Frozen: 2990) +Constraints : 2575755 (Binary: 95.7% Ternary: 3.2% Other: 1.1%) + +Memory Peak : 816MB +Max. Length : 0 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 0.35s +Memory: 752MB (+180MB) +SAT +Testing... +NOT SERIALIZABLE +Testing Time: 2.79s +Memory: 765MB (+13MB) +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 2 +Time : 35.326s (Solving: 23.14s 1st Model: 0.11s Unsat: 0.00s) +CPU Time : 35.236s + +Choices : 2048966 (Domain: 2018629) +Conflicts : 24887 (Analyzed: 24887) +Restarts : 100 (Average: 248.87 Last: 191) +Model-Level : 4372.0 +Problems : 2 (Average Length: 117.00 Splits: 0) +Lemmas : 24887 (Deleted: 19122) + Binary : 1894 (Ratio: 7.61%) + Ternary : 557 (Ratio: 2.24%) + Conflict : 24887 (Average Length: 326.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 24887 (Average: 81.42 Max: 1731 Sum: 2026194) + Executed : 24853 (Average: 81.26 Max: 1731 Sum: 2022241 Ratio: 99.80%) + Bounded : 34 (Average: 116.26 Max: 117 Sum: 3953 Ratio: 0.20%) + +Rules : 1028283 (Original: 843628) +Atoms : 59257 +Bodies : 791604 (Original: 606949) + Count : 9712 (Original: 27041) +Equivalences : 188391 (Atom=Atom: 172 Body=Body: 0 Other: 188219) +Tight : Yes +Variables : 578090 (Eliminated: 0 Frozen: 191082) +Constraints : 4249774 (Binary: 91.4% Ternary: 7.1% Other: 1.5%) + +Memory Peak : 892MB +Max. Length : 0 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 24.00s +Memory: 872MB (+107MB) +UNKNOWN +Iteration Time: 35.34s + +Iteration 2 +Queue: [(0,115,1,True)] +Grounded Until: 115 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 3 +Time : 60.556s (Solving: 48.23s 1st Model: 0.11s Unsat: 0.00s) +CPU Time : 60.476s + +Choices : 3872517 (Domain: 3816021) +Conflicts : 51173 (Analyzed: 51173) +Restarts : 200 (Average: 255.87 Last: 325) +Model-Level : 4372.0 +Problems : 3 (Average Length: 117.00 Splits: 0) +Lemmas : 51173 (Deleted: 40835) + Binary : 3546 (Ratio: 6.93%) + Ternary : 967 (Ratio: 1.89%) + Conflict : 51173 (Average Length: 306.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 51173 (Average: 74.73 Max: 1786 Sum: 3824095) + Executed : 51131 (Average: 74.63 Max: 1786 Sum: 3819223 Ratio: 99.87%) + Bounded : 42 (Average: 116.00 Max: 117 Sum: 4872 Ratio: 0.13%) + +Rules : 1028283 (Original: 843628) +Atoms : 59257 +Bodies : 791604 (Original: 606949) + Count : 9712 (Original: 27041) +Equivalences : 188391 (Atom=Atom: 172 Body=Body: 0 Other: 188219) +Tight : Yes +Variables : 578090 (Eliminated: 0 Frozen: 191082) +Constraints : 4207579 (Binary: 91.4% Ternary: 7.1% Other: 1.6%) + +Memory Peak : 892MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 25.24s +Memory: 875MB (+3MB) +UNKNOWN +Iteration Time: 25.24s + +Iteration 3 +Queue: [(0,115,2,True)] +Grounded Until: 115 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 4 +Time : 78.821s (Solving: 66.40s 1st Model: 0.11s Unsat: 0.00s) +CPU Time : 78.748s + +Choices : 4511056 (Domain: 4451872) +Conflicts : 76087 (Analyzed: 76087) +Restarts : 300 (Average: 253.62 Last: 325) +Model-Level : 4372.0 +Problems : 4 (Average Length: 117.00 Splits: 0) +Lemmas : 76087 (Deleted: 63602) + Binary : 4163 (Ratio: 5.47%) + Ternary : 1077 (Ratio: 1.42%) + Conflict : 76087 (Average Length: 295.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 76087 (Average: 58.46 Max: 1786 Sum: 4448159) + Executed : 76039 (Average: 58.39 Max: 1786 Sum: 4442600 Ratio: 99.88%) + Bounded : 48 (Average: 115.81 Max: 117 Sum: 5559 Ratio: 0.12%) + +Rules : 1028283 (Original: 843628) +Atoms : 59257 +Bodies : 791604 (Original: 606949) + Count : 9712 (Original: 27041) +Equivalences : 188391 (Atom=Atom: 172 Body=Body: 0 Other: 188219) +Tight : Yes +Variables : 578090 (Eliminated: 0 Frozen: 191082) +Constraints : 4207523 (Binary: 91.4% Ternary: 7.1% Other: 1.6%) + +Memory Peak : 892MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 18.28s +Memory: 875MB (+0MB) +UNKNOWN +Iteration Time: 18.28s + +Iteration 4 +Queue: [(0,115,3,True)] +Grounded Until: 115 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 5 +Time : 100.912s (Solving: 88.38s 1st Model: 0.11s Unsat: 0.00s) +CPU Time : 100.848s + +Choices : 5900171 (Domain: 5832014) +Conflicts : 102155 (Analyzed: 102155) +Restarts : 400 (Average: 255.39 Last: 325) +Model-Level : 4372.0 +Problems : 5 (Average Length: 117.00 Splits: 0) +Lemmas : 102155 (Deleted: 86695) + Binary : 5112 (Ratio: 5.00%) + Ternary : 1234 (Ratio: 1.21%) + Conflict : 102155 (Average Length: 349.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 102155 (Average: 56.91 Max: 1786 Sum: 5814040) + Executed : 102102 (Average: 56.85 Max: 1786 Sum: 5807905 Ratio: 99.89%) + Bounded : 53 (Average: 115.75 Max: 117 Sum: 6135 Ratio: 0.11%) + +Rules : 1028283 (Original: 843628) +Atoms : 59257 +Bodies : 791604 (Original: 606949) + Count : 9712 (Original: 27041) +Equivalences : 188391 (Atom=Atom: 172 Body=Body: 0 Other: 188219) +Tight : Yes +Variables : 578090 (Eliminated: 0 Frozen: 191082) +Constraints : 4201702 (Binary: 91.4% Ternary: 7.1% Other: 1.6%) + +Memory Peak : 892MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 22.10s +Memory: 875MB (+0MB) +UNKNOWN +Iteration Time: 22.10s + +Iteration 5 +Queue: [(0,115,4,True)] +Grounded Until: 115 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 6 +Time : 121.772s (Solving: 109.12s 1st Model: 0.11s Unsat: 0.00s) +CPU Time : 121.716s + +Choices : 7050553 (Domain: 6975388) +Conflicts : 128140 (Analyzed: 128140) +Restarts : 500 (Average: 256.28 Last: 325) +Model-Level : 4372.0 +Problems : 6 (Average Length: 117.00 Splits: 0) +Lemmas : 128140 (Deleted: 113807) + Binary : 5766 (Ratio: 4.50%) + Ternary : 1295 (Ratio: 1.01%) + Conflict : 128140 (Average Length: 452.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 128140 (Average: 54.16 Max: 1786 Sum: 6940222) + Executed : 128085 (Average: 54.11 Max: 1786 Sum: 6933860 Ratio: 99.91%) + Bounded : 55 (Average: 115.67 Max: 117 Sum: 6362 Ratio: 0.09%) + +Rules : 1028283 (Original: 843628) +Atoms : 59257 +Bodies : 791604 (Original: 606949) + Count : 9712 (Original: 27041) +Equivalences : 188391 (Atom=Atom: 172 Body=Body: 0 Other: 188219) +Tight : Yes +Variables : 578090 (Eliminated: 0 Frozen: 191082) +Constraints : 4201661 (Binary: 91.4% Ternary: 7.1% Other: 1.6%) + +Memory Peak : 892MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 20.87s +Memory: 875MB (+0MB) +UNKNOWN +Iteration Time: 20.87s + +Iteration 6 +Queue: [(0,115,5,True)] +Grounded Until: 115 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 7 +Time : 145.498s (Solving: 132.72s 1st Model: 0.11s Unsat: 0.00s) +CPU Time : 145.452s + +Choices : 8489902 (Domain: 8406773) +Conflicts : 154622 (Analyzed: 154622) +Restarts : 600 (Average: 257.70 Last: 325) +Model-Level : 4372.0 +Problems : 7 (Average Length: 117.00 Splits: 0) +Lemmas : 154622 (Deleted: 135874) + Binary : 6316 (Ratio: 4.08%) + Ternary : 1344 (Ratio: 0.87%) + Conflict : 154622 (Average Length: 520.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 154622 (Average: 54.02 Max: 1786 Sum: 8353059) + Executed : 154565 (Average: 53.98 Max: 1786 Sum: 8346468 Ratio: 99.92%) + Bounded : 57 (Average: 115.63 Max: 117 Sum: 6591 Ratio: 0.08%) + +Rules : 1028283 (Original: 843628) +Atoms : 59257 +Bodies : 791604 (Original: 606949) + Count : 9712 (Original: 27041) +Equivalences : 188391 (Atom=Atom: 172 Body=Body: 0 Other: 188219) +Tight : Yes +Variables : 578090 (Eliminated: 0 Frozen: 191082) +Constraints : 4201661 (Binary: 91.4% Ternary: 7.1% Other: 1.6%) + +Memory Peak : 892MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 23.74s +Memory: 875MB (+0MB) +UNKNOWN +Iteration Time: 23.74s + +Iteration 7 +Queue: [(0,115,6,True)] +Grounded Until: 115 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 8 +Time : 166.501s (Solving: 153.61s 1st Model: 0.11s Unsat: 0.00s) +CPU Time : 166.464s + +Choices : 9706875 (Domain: 9618258) +Conflicts : 180223 (Analyzed: 180223) +Restarts : 700 (Average: 257.46 Last: 325) +Model-Level : 4372.0 +Problems : 8 (Average Length: 117.00 Splits: 0) +Lemmas : 180223 (Deleted: 161738) + Binary : 6797 (Ratio: 3.77%) + Ternary : 1400 (Ratio: 0.78%) + Conflict : 180223 (Average Length: 558.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 180223 (Average: 52.96 Max: 1786 Sum: 9545229) + Executed : 180165 (Average: 52.93 Max: 1786 Sum: 9538522 Ratio: 99.93%) + Bounded : 58 (Average: 115.64 Max: 117 Sum: 6707 Ratio: 0.07%) + +Rules : 1028283 (Original: 843628) +Atoms : 59257 +Bodies : 791604 (Original: 606949) + Count : 9712 (Original: 27041) +Equivalences : 188391 (Atom=Atom: 172 Body=Body: 0 Other: 188219) +Tight : Yes +Variables : 578090 (Eliminated: 0 Frozen: 191082) +Constraints : 4201647 (Binary: 91.4% Ternary: 7.1% Other: 1.6%) + +Memory Peak : 892MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 21.01s +Memory: 875MB (+0MB) +UNKNOWN +Iteration Time: 21.01s + +Iteration 8 +Queue: [(0,115,7,True)] +Grounded Until: 115 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 9 +Time : 187.845s (Solving: 174.84s 1st Model: 0.11s Unsat: 0.00s) +CPU Time : 187.816s + +Choices : 10959778 (Domain: 10864511) +Conflicts : 206844 (Analyzed: 206844) +Restarts : 800 (Average: 258.56 Last: 325) +Model-Level : 4372.0 +Problems : 9 (Average Length: 117.00 Splits: 0) +Lemmas : 206844 (Deleted: 186023) + Binary : 7209 (Ratio: 3.49%) + Ternary : 1470 (Ratio: 0.71%) + Conflict : 206844 (Average Length: 591.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 206844 (Average: 52.07 Max: 1786 Sum: 10770502) + Executed : 206786 (Average: 52.04 Max: 1786 Sum: 10763795 Ratio: 99.94%) + Bounded : 58 (Average: 115.64 Max: 117 Sum: 6707 Ratio: 0.06%) + +Rules : 1028283 (Original: 843628) +Atoms : 59257 +Bodies : 791604 (Original: 606949) + Count : 9712 (Original: 27041) +Equivalences : 188391 (Atom=Atom: 172 Body=Body: 0 Other: 188219) +Tight : Yes +Variables : 578090 (Eliminated: 0 Frozen: 191082) +Constraints : 4201647 (Binary: 91.4% Ternary: 7.1% Other: 1.6%) + +Memory Peak : 892MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 21.36s +Memory: 875MB (+0MB) +UNKNOWN +Iteration Time: 21.36s + +Iteration 9 +Queue: [(0,115,8,True)] +Grounded Until: 115 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 10 +Time : 212.388s (Solving: 199.26s 1st Model: 0.11s Unsat: 0.00s) +CPU Time : 212.368s + +Choices : 12421955 (Domain: 12315304) +Conflicts : 234047 (Analyzed: 234047) +Restarts : 900 (Average: 260.05 Last: 325) +Model-Level : 4372.0 +Problems : 10 (Average Length: 117.00 Splits: 0) +Lemmas : 234047 (Deleted: 210236) + Binary : 8240 (Ratio: 3.52%) + Ternary : 1663 (Ratio: 0.71%) + Conflict : 234047 (Average Length: 635.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 234047 (Average: 52.12 Max: 1786 Sum: 12199350) + Executed : 233989 (Average: 52.09 Max: 1786 Sum: 12192643 Ratio: 99.95%) + Bounded : 58 (Average: 115.64 Max: 117 Sum: 6707 Ratio: 0.05%) + +Rules : 1028283 (Original: 843628) +Atoms : 59257 +Bodies : 791604 (Original: 606949) + Count : 9712 (Original: 27041) +Equivalences : 188391 (Atom=Atom: 172 Body=Body: 0 Other: 188219) +Tight : Yes +Variables : 578090 (Eliminated: 0 Frozen: 191082) +Constraints : 4201647 (Binary: 91.4% Ternary: 7.1% Other: 1.6%) + +Memory Peak : 892MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 24.56s +Memory: 875MB (+0MB) +UNKNOWN +Iteration Time: 24.56s + +Iteration 10 +Queue: [(0,115,9,True)] +Grounded Until: 115 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 11 +Time : 235.434s (Solving: 222.18s 1st Model: 0.11s Unsat: 0.00s) +CPU Time : 235.424s + +Choices : 13783875 (Domain: 13670603) +Conflicts : 260263 (Analyzed: 260263) +Restarts : 1000 (Average: 260.26 Last: 325) +Model-Level : 4372.0 +Problems : 11 (Average Length: 117.00 Splits: 0) +Lemmas : 260263 (Deleted: 235996) + Binary : 8858 (Ratio: 3.40%) + Ternary : 1738 (Ratio: 0.67%) + Conflict : 260263 (Average Length: 643.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 260263 (Average: 51.99 Max: 1786 Sum: 13530807) + Executed : 260205 (Average: 51.96 Max: 1786 Sum: 13524100 Ratio: 99.95%) + Bounded : 58 (Average: 115.64 Max: 117 Sum: 6707 Ratio: 0.05%) + +Rules : 1028283 (Original: 843628) +Atoms : 59257 +Bodies : 791604 (Original: 606949) + Count : 9712 (Original: 27041) +Equivalences : 188391 (Atom=Atom: 172 Body=Body: 0 Other: 188219) +Tight : Yes +Variables : 578090 (Eliminated: 0 Frozen: 191082) +Constraints : 4201647 (Binary: 91.4% Ternary: 7.1% Other: 1.6%) + +Memory Peak : 892MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 23.06s +Memory: 875MB (+0MB) +UNKNOWN +Iteration Time: 23.06s + +Iteration 11 +Queue: [(0,115,10,True)] +Grounded Until: 115 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 12 +Time : 259.698s (Solving: 246.34s 1st Model: 0.11s Unsat: 0.00s) +CPU Time : 259.696s + +Choices : 14913066 (Domain: 14795788) +Conflicts : 285329 (Analyzed: 285329) +Restarts : 1100 (Average: 259.39 Last: 325) +Model-Level : 4372.0 +Problems : 12 (Average Length: 117.00 Splits: 0) +Lemmas : 285329 (Deleted: 260059) + Binary : 9956 (Ratio: 3.49%) + Ternary : 1947 (Ratio: 0.68%) + Conflict : 285329 (Average Length: 677.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 285329 (Average: 51.26 Max: 1786 Sum: 14625644) + Executed : 285271 (Average: 51.24 Max: 1786 Sum: 14618937 Ratio: 99.95%) + Bounded : 58 (Average: 115.64 Max: 117 Sum: 6707 Ratio: 0.05%) + +Rules : 1028283 (Original: 843628) +Atoms : 59257 +Bodies : 791604 (Original: 606949) + Count : 9712 (Original: 27041) +Equivalences : 188391 (Atom=Atom: 172 Body=Body: 0 Other: 188219) +Tight : Yes +Variables : 578090 (Eliminated: 0 Frozen: 191082) +Constraints : 4201647 (Binary: 91.4% Ternary: 7.1% Other: 1.6%) + +Memory Peak : 1003MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 24.28s +Memory: 939MB (+64MB) +UNKNOWN +Iteration Time: 24.28s + +Iteration 12 +Queue: [(0,115,11,True)] +Grounded Until: 115 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 13 +Time : 285.601s (Solving: 272.15s 1st Model: 0.11s Unsat: 0.00s) +CPU Time : 285.612s + +Choices : 15585244 (Domain: 15467219) +Conflicts : 314350 (Analyzed: 314350) +Restarts : 1200 (Average: 261.96 Last: 325) +Model-Level : 4372.0 +Problems : 13 (Average Length: 117.00 Splits: 0) +Lemmas : 314350 (Deleted: 286524) + Binary : 10677 (Ratio: 3.40%) + Ternary : 2113 (Ratio: 0.67%) + Conflict : 314350 (Average Length: 704.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 314350 (Average: 48.56 Max: 1786 Sum: 15264949) + Executed : 314292 (Average: 48.54 Max: 1786 Sum: 15258242 Ratio: 99.96%) + Bounded : 58 (Average: 115.64 Max: 117 Sum: 6707 Ratio: 0.04%) + +Rules : 1028283 (Original: 843628) +Atoms : 59257 +Bodies : 791604 (Original: 606949) + Count : 9712 (Original: 27041) +Equivalences : 188391 (Atom=Atom: 172 Body=Body: 0 Other: 188219) +Tight : Yes +Variables : 578090 (Eliminated: 0 Frozen: 191082) +Constraints : 4201647 (Binary: 91.4% Ternary: 7.1% Other: 1.6%) + +Memory Peak : 1003MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 25.92s +Memory: 939MB (+0MB) +UNKNOWN +Iteration Time: 25.92s + +Iteration 13 +Queue: [(0,115,12,True)] +Grounded Until: 115 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 14 +Time : 310.394s (Solving: 296.82s 1st Model: 0.11s Unsat: 0.00s) +CPU Time : 310.416s + +Choices : 16324755 (Domain: 16205525) +Conflicts : 343275 (Analyzed: 343275) +Restarts : 1300 (Average: 264.06 Last: 325) +Model-Level : 4372.0 +Problems : 14 (Average Length: 117.00 Splits: 0) +Lemmas : 343275 (Deleted: 313472) + Binary : 11623 (Ratio: 3.39%) + Ternary : 2287 (Ratio: 0.67%) + Conflict : 343275 (Average Length: 731.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 343275 (Average: 46.50 Max: 1786 Sum: 15963772) + Executed : 343217 (Average: 46.48 Max: 1786 Sum: 15957065 Ratio: 99.96%) + Bounded : 58 (Average: 115.64 Max: 117 Sum: 6707 Ratio: 0.04%) + +Rules : 1028283 (Original: 843628) +Atoms : 59257 +Bodies : 791604 (Original: 606949) + Count : 9712 (Original: 27041) +Equivalences : 188391 (Atom=Atom: 172 Body=Body: 0 Other: 188219) +Tight : Yes +Variables : 578090 (Eliminated: 0 Frozen: 191082) +Constraints : 4201647 (Binary: 91.4% Ternary: 7.1% Other: 1.6%) + +Memory Peak : 1003MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 24.81s +Memory: 939MB (+0MB) +UNKNOWN +Iteration Time: 24.81s + +Iteration 14 +Queue: [(0,115,13,True)] +Grounded Until: 115 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 15 +Time : 333.377s (Solving: 319.68s 1st Model: 0.11s Unsat: 0.00s) +CPU Time : 333.408s + +Choices : 16838907 (Domain: 16718886) +Conflicts : 370547 (Analyzed: 370547) +Restarts : 1400 (Average: 264.68 Last: 325) +Model-Level : 4372.0 +Problems : 15 (Average Length: 117.00 Splits: 0) +Lemmas : 370547 (Deleted: 338590) + Binary : 12054 (Ratio: 3.25%) + Ternary : 2361 (Ratio: 0.64%) + Conflict : 370547 (Average Length: 743.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 370547 (Average: 44.38 Max: 1786 Sum: 16443188) + Executed : 370489 (Average: 44.36 Max: 1786 Sum: 16436481 Ratio: 99.96%) + Bounded : 58 (Average: 115.64 Max: 117 Sum: 6707 Ratio: 0.04%) + +Rules : 1028283 (Original: 843628) +Atoms : 59257 +Bodies : 791604 (Original: 606949) + Count : 9712 (Original: 27041) +Equivalences : 188391 (Atom=Atom: 172 Body=Body: 0 Other: 188219) +Tight : Yes +Variables : 578090 (Eliminated: 0 Frozen: 191082) +Constraints : 4201647 (Binary: 91.4% Ternary: 7.1% Other: 1.6%) + +Memory Peak : 1003MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 23.00s +Memory: 939MB (+0MB) +UNKNOWN +Iteration Time: 23.00s + +Iteration 15 +Queue: [(0,115,14,True)] +Grounded Until: 115 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 16 +Time : 357.105s (Solving: 343.27s 1st Model: 0.11s Unsat: 0.00s) +CPU Time : 357.148s + +Choices : 17484833 (Domain: 17362930) +Conflicts : 400960 (Analyzed: 400960) +Restarts : 1500 (Average: 267.31 Last: 325) +Model-Level : 4372.0 +Problems : 16 (Average Length: 117.00 Splits: 0) +Lemmas : 400960 (Deleted: 367039) + Binary : 12857 (Ratio: 3.21%) + Ternary : 2521 (Ratio: 0.63%) + Conflict : 400960 (Average Length: 766.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 400960 (Average: 42.50 Max: 1786 Sum: 17042678) + Executed : 400902 (Average: 42.49 Max: 1786 Sum: 17035971 Ratio: 99.96%) + Bounded : 58 (Average: 115.64 Max: 117 Sum: 6707 Ratio: 0.04%) + +Rules : 1028283 (Original: 843628) +Atoms : 59257 +Bodies : 791604 (Original: 606949) + Count : 9712 (Original: 27041) +Equivalences : 188391 (Atom=Atom: 172 Body=Body: 0 Other: 188219) +Tight : Yes +Variables : 578090 (Eliminated: 0 Frozen: 191082) +Constraints : 4201647 (Binary: 91.4% Ternary: 7.1% Other: 1.6%) + +Memory Peak : 1003MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 23.74s +Memory: 939MB (+0MB) +UNKNOWN +Iteration Time: 23.74s + +Iteration 16 +Queue: [(0,115,15,True)] +Grounded Until: 115 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 17 +Time : 379.318s (Solving: 365.38s 1st Model: 0.11s Unsat: 0.00s) +CPU Time : 379.368s + +Choices : 17981886 (Domain: 17859175) +Conflicts : 428497 (Analyzed: 428497) +Restarts : 1600 (Average: 267.81 Last: 325) +Model-Level : 4372.0 +Problems : 17 (Average Length: 117.00 Splits: 0) +Lemmas : 428497 (Deleted: 393449) + Binary : 13283 (Ratio: 3.10%) + Ternary : 2579 (Ratio: 0.60%) + Conflict : 428497 (Average Length: 773.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 428497 (Average: 40.85 Max: 1786 Sum: 17502949) + Executed : 428439 (Average: 40.83 Max: 1786 Sum: 17496242 Ratio: 99.96%) + Bounded : 58 (Average: 115.64 Max: 117 Sum: 6707 Ratio: 0.04%) + +Rules : 1028283 (Original: 843628) +Atoms : 59257 +Bodies : 791604 (Original: 606949) + Count : 9712 (Original: 27041) +Equivalences : 188391 (Atom=Atom: 172 Body=Body: 0 Other: 188219) +Tight : Yes +Variables : 578090 (Eliminated: 0 Frozen: 191082) +Constraints : 4201647 (Binary: 91.4% Ternary: 7.1% Other: 1.6%) + +Memory Peak : 1003MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 22.22s +Memory: 939MB (+0MB) +UNKNOWN +Iteration Time: 22.23s + +Iteration 17 +Queue: [(0,115,16,True)] +Grounded Until: 115 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 18 +Time : 402.993s (Solving: 388.95s 1st Model: 0.11s Unsat: 0.00s) +CPU Time : 403.052s + +Choices : 18639848 (Domain: 18515837) +Conflicts : 457858 (Analyzed: 457858) +Restarts : 1700 (Average: 269.33 Last: 325) +Model-Level : 4372.0 +Problems : 18 (Average Length: 117.00 Splits: 0) +Lemmas : 457858 (Deleted: 422353) + Binary : 13992 (Ratio: 3.06%) + Ternary : 2713 (Ratio: 0.59%) + Conflict : 457858 (Average Length: 799.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 457858 (Average: 39.57 Max: 1786 Sum: 18116027) + Executed : 457800 (Average: 39.55 Max: 1786 Sum: 18109320 Ratio: 99.96%) + Bounded : 58 (Average: 115.64 Max: 117 Sum: 6707 Ratio: 0.04%) + +Rules : 1028283 (Original: 843628) +Atoms : 59257 +Bodies : 791604 (Original: 606949) + Count : 9712 (Original: 27041) +Equivalences : 188391 (Atom=Atom: 172 Body=Body: 0 Other: 188219) +Tight : Yes +Variables : 578090 (Eliminated: 0 Frozen: 191082) +Constraints : 4201647 (Binary: 91.4% Ternary: 7.1% Other: 1.6%) + +Memory Peak : 1003MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 23.69s +Memory: 939MB (+0MB) +UNKNOWN +Iteration Time: 23.69s + +Iteration 18 +Queue: [(0,115,17,True)] +Grounded Until: 115 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 19 +Time : 423.787s (Solving: 409.63s 1st Model: 0.11s Unsat: 0.00s) +CPU Time : 423.856s + +Choices : 19101847 (Domain: 18977218) +Conflicts : 482691 (Analyzed: 482691) +Restarts : 1800 (Average: 268.16 Last: 325) +Model-Level : 4372.0 +Problems : 19 (Average Length: 117.00 Splits: 0) +Lemmas : 482691 (Deleted: 447512) + Binary : 14510 (Ratio: 3.01%) + Ternary : 2801 (Ratio: 0.58%) + Conflict : 482691 (Average Length: 821.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 482691 (Average: 38.39 Max: 1786 Sum: 18532192) + Executed : 482633 (Average: 38.38 Max: 1786 Sum: 18525485 Ratio: 99.96%) + Bounded : 58 (Average: 115.64 Max: 117 Sum: 6707 Ratio: 0.04%) + +Rules : 1028283 (Original: 843628) +Atoms : 59257 +Bodies : 791604 (Original: 606949) + Count : 9712 (Original: 27041) +Equivalences : 188391 (Atom=Atom: 172 Body=Body: 0 Other: 188219) +Tight : Yes +Variables : 578090 (Eliminated: 0 Frozen: 191082) +Constraints : 4201647 (Binary: 91.4% Ternary: 7.1% Other: 1.6%) + +Memory Peak : 1003MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 20.81s +Memory: 939MB (+0MB) +UNKNOWN +Iteration Time: 20.81s + +Iteration 19 +Queue: [(0,115,18,True)] +Grounded Until: 115 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 20 +Time : 446.358s (Solving: 432.06s 1st Model: 0.11s Unsat: 0.00s) +CPU Time : 446.436s + +Choices : 19727025 (Domain: 19601443) +Conflicts : 511410 (Analyzed: 511410) +Restarts : 1900 (Average: 269.16 Last: 325) +Model-Level : 4372.0 +Problems : 20 (Average Length: 117.00 Splits: 0) +Lemmas : 511410 (Deleted: 473835) + Binary : 15075 (Ratio: 2.95%) + Ternary : 2971 (Ratio: 0.58%) + Conflict : 511410 (Average Length: 833.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 511410 (Average: 37.37 Max: 1786 Sum: 19110808) + Executed : 511352 (Average: 37.36 Max: 1786 Sum: 19104101 Ratio: 99.96%) + Bounded : 58 (Average: 115.64 Max: 117 Sum: 6707 Ratio: 0.04%) + +Rules : 1028283 (Original: 843628) +Atoms : 59257 +Bodies : 791604 (Original: 606949) + Count : 9712 (Original: 27041) +Equivalences : 188391 (Atom=Atom: 172 Body=Body: 0 Other: 188219) +Tight : Yes +Variables : 578090 (Eliminated: 0 Frozen: 191082) +Constraints : 4201647 (Binary: 91.4% Ternary: 7.1% Other: 1.6%) + +Memory Peak : 1003MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 22.58s +Memory: 939MB (+0MB) +UNKNOWN +Iteration Time: 22.58s + +Iteration 20 +Queue: [(0,115,19,True)] +Grounded Until: 115 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 21 +Time : 466.661s (Solving: 452.27s 1st Model: 0.11s Unsat: 0.00s) +CPU Time : 466.748s + +Choices : 20253628 (Domain: 20127111) +Conflicts : 537402 (Analyzed: 537402) +Restarts : 2000 (Average: 268.70 Last: 325) +Model-Level : 4372.0 +Problems : 21 (Average Length: 117.00 Splits: 0) +Lemmas : 537402 (Deleted: 498510) + Binary : 15567 (Ratio: 2.90%) + Ternary : 3104 (Ratio: 0.58%) + Conflict : 537402 (Average Length: 845.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 537402 (Average: 36.45 Max: 1786 Sum: 19587778) + Executed : 537344 (Average: 36.44 Max: 1786 Sum: 19581071 Ratio: 99.97%) + Bounded : 58 (Average: 115.64 Max: 117 Sum: 6707 Ratio: 0.03%) + +Rules : 1028283 (Original: 843628) +Atoms : 59257 +Bodies : 791604 (Original: 606949) + Count : 9712 (Original: 27041) +Equivalences : 188391 (Atom=Atom: 172 Body=Body: 0 Other: 188219) +Tight : Yes +Variables : 578090 (Eliminated: 0 Frozen: 191082) +Constraints : 4201647 (Binary: 91.4% Ternary: 7.1% Other: 1.6%) + +Memory Peak : 1003MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 20.31s +Memory: 939MB (+0MB) +UNKNOWN +Iteration Time: 20.31s + +Iteration 21 +Queue: [(0,115,20,True)] +Grounded Until: 115 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 22 +Time : 488.409s (Solving: 473.91s 1st Model: 0.11s Unsat: 0.00s) +CPU Time : 488.508s + +Choices : 20680606 (Domain: 20553451) +Conflicts : 564339 (Analyzed: 564339) +Restarts : 2100 (Average: 268.73 Last: 325) +Model-Level : 4372.0 +Problems : 22 (Average Length: 117.00 Splits: 0) +Lemmas : 564339 (Deleted: 523616) + Binary : 15907 (Ratio: 2.82%) + Ternary : 3187 (Ratio: 0.56%) + Conflict : 564339 (Average Length: 860.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 564339 (Average: 35.38 Max: 1786 Sum: 19966992) + Executed : 564281 (Average: 35.37 Max: 1786 Sum: 19960285 Ratio: 99.97%) + Bounded : 58 (Average: 115.64 Max: 117 Sum: 6707 Ratio: 0.03%) + +Rules : 1028283 (Original: 843628) +Atoms : 59257 +Bodies : 791604 (Original: 606949) + Count : 9712 (Original: 27041) +Equivalences : 188391 (Atom=Atom: 172 Body=Body: 0 Other: 188219) +Tight : Yes +Variables : 578090 (Eliminated: 0 Frozen: 191082) +Constraints : 4201647 (Binary: 91.4% Ternary: 7.1% Other: 1.6%) + +Memory Peak : 1003MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 21.76s +Memory: 939MB (+0MB) +UNKNOWN +Iteration Time: 21.76s + +Iteration 22 +Queue: [(0,115,21,True)] +Grounded Until: 115 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 23 +Time : 509.601s (Solving: 494.96s 1st Model: 0.11s Unsat: 0.00s) +CPU Time : 509.708s + +Choices : 21157210 (Domain: 21028550) +Conflicts : 590789 (Analyzed: 590789) +Restarts : 2200 (Average: 268.54 Last: 325) +Model-Level : 4372.0 +Problems : 23 (Average Length: 117.00 Splits: 0) +Lemmas : 590789 (Deleted: 549647) + Binary : 16276 (Ratio: 2.75%) + Ternary : 3277 (Ratio: 0.55%) + Conflict : 590789 (Average Length: 876.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 590789 (Average: 34.53 Max: 1786 Sum: 20397175) + Executed : 590731 (Average: 34.51 Max: 1786 Sum: 20390468 Ratio: 99.97%) + Bounded : 58 (Average: 115.64 Max: 117 Sum: 6707 Ratio: 0.03%) + +Rules : 1028283 (Original: 843628) +Atoms : 59257 +Bodies : 791604 (Original: 606949) + Count : 9712 (Original: 27041) +Equivalences : 188391 (Atom=Atom: 172 Body=Body: 0 Other: 188219) +Tight : Yes +Variables : 578090 (Eliminated: 0 Frozen: 191082) +Constraints : 4201647 (Binary: 91.4% Ternary: 7.1% Other: 1.6%) + +Memory Peak : 1003MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 21.20s +Memory: 939MB (+0MB) +UNKNOWN +Iteration Time: 21.20s + +Iteration 23 +Queue: [(0,115,22,True)] +Grounded Until: 115 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 24 +Time : 530.103s (Solving: 515.37s 1st Model: 0.11s Unsat: 0.00s) +CPU Time : 530.216s + +Choices : 21566865 (Domain: 21437541) +Conflicts : 619802 (Analyzed: 619802) +Restarts : 2300 (Average: 269.48 Last: 325) +Model-Level : 4372.0 +Problems : 24 (Average Length: 117.00 Splits: 0) +Lemmas : 619802 (Deleted: 578266) + Binary : 16575 (Ratio: 2.67%) + Ternary : 3362 (Ratio: 0.54%) + Conflict : 619802 (Average Length: 891.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 619802 (Average: 33.51 Max: 1786 Sum: 20768694) + Executed : 619744 (Average: 33.50 Max: 1786 Sum: 20761987 Ratio: 99.97%) + Bounded : 58 (Average: 115.64 Max: 117 Sum: 6707 Ratio: 0.03%) + +Rules : 1028283 (Original: 843628) +Atoms : 59257 +Bodies : 791604 (Original: 606949) + Count : 9712 (Original: 27041) +Equivalences : 188391 (Atom=Atom: 172 Body=Body: 0 Other: 188219) +Tight : Yes +Variables : 578090 (Eliminated: 0 Frozen: 191082) +Constraints : 4201647 (Binary: 91.4% Ternary: 7.1% Other: 1.6%) + +Memory Peak : 1003MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 20.51s +Memory: 939MB (+0MB) +UNKNOWN +Iteration Time: 20.51s + +Iteration 24 +Queue: [(0,115,23,True)] +Grounded Until: 115 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 25 +Time : 550.333s (Solving: 535.48s 1st Model: 0.11s Unsat: 0.00s) +CPU Time : 550.456s + +Choices : 21982303 (Domain: 21851647) +Conflicts : 646020 (Analyzed: 646020) +Restarts : 2400 (Average: 269.18 Last: 325) +Model-Level : 4372.0 +Problems : 25 (Average Length: 117.00 Splits: 0) +Lemmas : 646020 (Deleted: 603231) + Binary : 16982 (Ratio: 2.63%) + Ternary : 3418 (Ratio: 0.53%) + Conflict : 646020 (Average Length: 900.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 646020 (Average: 32.72 Max: 1786 Sum: 21137360) + Executed : 645962 (Average: 32.71 Max: 1786 Sum: 21130653 Ratio: 99.97%) + Bounded : 58 (Average: 115.64 Max: 117 Sum: 6707 Ratio: 0.03%) + +Rules : 1028283 (Original: 843628) +Atoms : 59257 +Bodies : 791604 (Original: 606949) + Count : 9712 (Original: 27041) +Equivalences : 188391 (Atom=Atom: 172 Body=Body: 0 Other: 188219) +Tight : Yes +Variables : 578090 (Eliminated: 0 Frozen: 191082) +Constraints : 4201647 (Binary: 91.4% Ternary: 7.1% Other: 1.6%) + +Memory Peak : 1003MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 20.24s +Memory: 939MB (+0MB) +UNKNOWN +Iteration Time: 20.24s + +Iteration 25 +Queue: [(0,115,24,True)] +Grounded Until: 115 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 26 +Time : 569.096s (Solving: 554.14s 1st Model: 0.11s Unsat: 0.00s) +CPU Time : 569.228s + +Choices : 22425207 (Domain: 22294014) +Conflicts : 670462 (Analyzed: 670462) +Restarts : 2500 (Average: 268.18 Last: 325) +Model-Level : 4372.0 +Problems : 26 (Average Length: 117.00 Splits: 0) +Lemmas : 670462 (Deleted: 625776) + Binary : 17232 (Ratio: 2.57%) + Ternary : 3491 (Ratio: 0.52%) + Conflict : 670462 (Average Length: 900.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 670462 (Average: 32.11 Max: 1786 Sum: 21531352) + Executed : 670404 (Average: 32.10 Max: 1786 Sum: 21524645 Ratio: 99.97%) + Bounded : 58 (Average: 115.64 Max: 117 Sum: 6707 Ratio: 0.03%) + +Rules : 1028283 (Original: 843628) +Atoms : 59257 +Bodies : 791604 (Original: 606949) + Count : 9712 (Original: 27041) +Equivalences : 188391 (Atom=Atom: 172 Body=Body: 0 Other: 188219) +Tight : Yes +Variables : 578090 (Eliminated: 0 Frozen: 191082) +Constraints : 4201647 (Binary: 91.4% Ternary: 7.1% Other: 1.6%) + +Memory Peak : 1003MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 18.77s +Memory: 939MB (+0MB) +UNKNOWN +Iteration Time: 18.77s + +Iteration 26 +Queue: [(0,115,25,True)] +Grounded Until: 115 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 27 +Time : 587.844s (Solving: 572.77s 1st Model: 0.11s Unsat: 0.00s) +CPU Time : 587.984s + +Choices : 22777286 (Domain: 22645410) +Conflicts : 695275 (Analyzed: 695275) +Restarts : 2600 (Average: 267.41 Last: 325) +Model-Level : 4372.0 +Problems : 27 (Average Length: 117.00 Splits: 0) +Lemmas : 695275 (Deleted: 652305) + Binary : 17448 (Ratio: 2.51%) + Ternary : 3540 (Ratio: 0.51%) + Conflict : 695275 (Average Length: 903.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 695275 (Average: 31.41 Max: 1786 Sum: 21841035) + Executed : 695217 (Average: 31.40 Max: 1786 Sum: 21834328 Ratio: 99.97%) + Bounded : 58 (Average: 115.64 Max: 117 Sum: 6707 Ratio: 0.03%) + +Rules : 1028283 (Original: 843628) +Atoms : 59257 +Bodies : 791604 (Original: 606949) + Count : 9712 (Original: 27041) +Equivalences : 188391 (Atom=Atom: 172 Body=Body: 0 Other: 188219) +Tight : Yes +Variables : 578090 (Eliminated: 0 Frozen: 191082) +Constraints : 4201647 (Binary: 91.4% Ternary: 7.1% Other: 1.6%) + +Memory Peak : 1003MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 18.76s +Memory: 939MB (+0MB) +UNKNOWN +Iteration Time: 18.76s + +Iteration 27 +Queue: [(0,115,26,True)] +Grounded Until: 115 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 28 +Time : 610.776s (Solving: 595.57s 1st Model: 0.11s Unsat: 0.00s) +CPU Time : 610.928s + +Choices : 23214111 (Domain: 23081639) +Conflicts : 726046 (Analyzed: 726046) +Restarts : 2700 (Average: 268.91 Last: 325) +Model-Level : 4372.0 +Problems : 28 (Average Length: 117.00 Splits: 0) +Lemmas : 726046 (Deleted: 682038) + Binary : 17753 (Ratio: 2.45%) + Ternary : 3653 (Ratio: 0.50%) + Conflict : 726046 (Average Length: 906.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 726046 (Average: 30.63 Max: 1786 Sum: 22239299) + Executed : 725988 (Average: 30.62 Max: 1786 Sum: 22232592 Ratio: 99.97%) + Bounded : 58 (Average: 115.64 Max: 117 Sum: 6707 Ratio: 0.03%) + +Rules : 1028283 (Original: 843628) +Atoms : 59257 +Bodies : 791604 (Original: 606949) + Count : 9712 (Original: 27041) +Equivalences : 188391 (Atom=Atom: 172 Body=Body: 0 Other: 188219) +Tight : Yes +Variables : 578090 (Eliminated: 0 Frozen: 191082) +Constraints : 4201647 (Binary: 91.4% Ternary: 7.1% Other: 1.6%) + +Memory Peak : 1003MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 22.94s +Memory: 939MB (+0MB) +UNKNOWN +Iteration Time: 22.95s + +Iteration 28 +Queue: [(0,115,27,True)] +Grounded Until: 115 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 29 +Time : 632.385s (Solving: 617.03s 1st Model: 0.11s Unsat: 0.00s) +CPU Time : 632.548s + +Choices : 23667160 (Domain: 23533806) +Conflicts : 753519 (Analyzed: 753519) +Restarts : 2800 (Average: 269.11 Last: 325) +Model-Level : 4372.0 +Problems : 29 (Average Length: 117.00 Splits: 0) +Lemmas : 753519 (Deleted: 706206) + Binary : 18045 (Ratio: 2.39%) + Ternary : 3715 (Ratio: 0.49%) + Conflict : 753519 (Average Length: 910.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 753519 (Average: 30.06 Max: 1786 Sum: 22648817) + Executed : 753461 (Average: 30.05 Max: 1786 Sum: 22642110 Ratio: 99.97%) + Bounded : 58 (Average: 115.64 Max: 117 Sum: 6707 Ratio: 0.03%) + +Rules : 1028283 (Original: 843628) +Atoms : 59257 +Bodies : 791604 (Original: 606949) + Count : 9712 (Original: 27041) +Equivalences : 188391 (Atom=Atom: 172 Body=Body: 0 Other: 188219) +Tight : Yes +Variables : 578090 (Eliminated: 0 Frozen: 191082) +Constraints : 4201647 (Binary: 91.4% Ternary: 7.1% Other: 1.6%) + +Memory Peak : 1003MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 21.62s +Memory: 939MB (+0MB) +UNKNOWN +Iteration Time: 21.62s + +Iteration 29 +Queue: [(0,115,28,True)] +Grounded Until: 115 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 30 +Time : 652.470s (Solving: 637.01s 1st Model: 0.11s Unsat: 0.00s) +CPU Time : 652.644s + +Choices : 24122919 (Domain: 23988579) +Conflicts : 779721 (Analyzed: 779721) +Restarts : 2900 (Average: 268.87 Last: 325) +Model-Level : 4372.0 +Problems : 30 (Average Length: 117.00 Splits: 0) +Lemmas : 779721 (Deleted: 732791) + Binary : 18282 (Ratio: 2.34%) + Ternary : 3769 (Ratio: 0.48%) + Conflict : 779721 (Average Length: 906.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 779721 (Average: 29.57 Max: 1786 Sum: 23054411) + Executed : 779663 (Average: 29.56 Max: 1786 Sum: 23047704 Ratio: 99.97%) + Bounded : 58 (Average: 115.64 Max: 117 Sum: 6707 Ratio: 0.03%) + +Rules : 1028283 (Original: 843628) +Atoms : 59257 +Bodies : 791604 (Original: 606949) + Count : 9712 (Original: 27041) +Equivalences : 188391 (Atom=Atom: 172 Body=Body: 0 Other: 188219) +Tight : Yes +Variables : 578090 (Eliminated: 0 Frozen: 191082) +Constraints : 4201647 (Binary: 91.4% Ternary: 7.1% Other: 1.6%) + +Memory Peak : 1003MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 20.10s +Memory: 939MB (+0MB) +UNKNOWN +Iteration Time: 20.10s + +Iteration 30 +Queue: [(0,115,29,True)] +Grounded Until: 115 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 31 +Time : 676.046s (Solving: 660.47s 1st Model: 0.11s Unsat: 0.00s) +CPU Time : 676.228s + +Choices : 24597842 (Domain: 24462468) +Conflicts : 811224 (Analyzed: 811224) +Restarts : 3000 (Average: 270.41 Last: 326) +Model-Level : 4372.0 +Problems : 31 (Average Length: 117.00 Splits: 0) +Lemmas : 811224 (Deleted: 764109) + Binary : 18542 (Ratio: 2.29%) + Ternary : 3826 (Ratio: 0.47%) + Conflict : 811224 (Average Length: 907.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 811224 (Average: 28.95 Max: 1786 Sum: 23488210) + Executed : 811166 (Average: 28.95 Max: 1786 Sum: 23481503 Ratio: 99.97%) + Bounded : 58 (Average: 115.64 Max: 117 Sum: 6707 Ratio: 0.03%) + +Rules : 1028283 (Original: 843628) +Atoms : 59257 +Bodies : 791604 (Original: 606949) + Count : 9712 (Original: 27041) +Equivalences : 188391 (Atom=Atom: 172 Body=Body: 0 Other: 188219) +Tight : Yes +Variables : 578090 (Eliminated: 0 Frozen: 191082) +Constraints : 4201647 (Binary: 91.4% Ternary: 7.1% Other: 1.6%) + +Memory Peak : 1003MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 23.59s +Memory: 939MB (+0MB) +UNKNOWN +Iteration Time: 23.59s + +Iteration 31 +Queue: [(0,115,30,True)] +Grounded Until: 115 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 32 +Time : 697.320s (Solving: 681.63s 1st Model: 0.11s Unsat: 0.00s) +CPU Time : 697.512s + +Choices : 24938437 (Domain: 24802939) +Conflicts : 839742 (Analyzed: 839742) +Restarts : 3100 (Average: 270.88 Last: 326) +Model-Level : 4372.0 +Problems : 32 (Average Length: 117.00 Splits: 0) +Lemmas : 839742 (Deleted: 791748) + Binary : 18814 (Ratio: 2.24%) + Ternary : 3884 (Ratio: 0.46%) + Conflict : 839742 (Average Length: 911.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 839742 (Average: 28.33 Max: 1786 Sum: 23790263) + Executed : 839684 (Average: 28.32 Max: 1786 Sum: 23783556 Ratio: 99.97%) + Bounded : 58 (Average: 115.64 Max: 117 Sum: 6707 Ratio: 0.03%) + +Rules : 1028283 (Original: 843628) +Atoms : 59257 +Bodies : 791604 (Original: 606949) + Count : 9712 (Original: 27041) +Equivalences : 188391 (Atom=Atom: 172 Body=Body: 0 Other: 188219) +Tight : Yes +Variables : 578090 (Eliminated: 0 Frozen: 191082) +Constraints : 4201647 (Binary: 91.4% Ternary: 7.1% Other: 1.6%) + +Memory Peak : 1003MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 21.28s +Memory: 939MB (+0MB) +UNKNOWN +Iteration Time: 21.28s + +Iteration 32 +Queue: [(0,115,31,True)] +Grounded Until: 115 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 33 +Time : 718.490s (Solving: 702.69s 1st Model: 0.11s Unsat: 0.00s) +CPU Time : 718.692s + +Choices : 25366137 (Domain: 25230264) +Conflicts : 868660 (Analyzed: 868660) +Restarts : 3200 (Average: 271.46 Last: 326) +Model-Level : 4372.0 +Problems : 33 (Average Length: 117.00 Splits: 0) +Lemmas : 868660 (Deleted: 819464) + Binary : 19051 (Ratio: 2.19%) + Ternary : 3928 (Ratio: 0.45%) + Conflict : 868660 (Average Length: 911.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 868660 (Average: 27.83 Max: 1786 Sum: 24175966) + Executed : 868602 (Average: 27.82 Max: 1786 Sum: 24169259 Ratio: 99.97%) + Bounded : 58 (Average: 115.64 Max: 117 Sum: 6707 Ratio: 0.03%) + +Rules : 1028283 (Original: 843628) +Atoms : 59257 +Bodies : 791604 (Original: 606949) + Count : 9712 (Original: 27041) +Equivalences : 188391 (Atom=Atom: 172 Body=Body: 0 Other: 188219) +Tight : Yes +Variables : 578090 (Eliminated: 0 Frozen: 191082) +Constraints : 4201647 (Binary: 91.4% Ternary: 7.1% Other: 1.6%) + +Memory Peak : 1003MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 21.18s +Memory: 939MB (+0MB) +UNKNOWN +Iteration Time: 21.18s + +Iteration 33 +Queue: [(0,115,32,True)] +Grounded Until: 115 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 34 +Time : 740.215s (Solving: 724.31s 1st Model: 0.11s Unsat: 0.00s) +CPU Time : 740.424s + +Choices : 25730893 (Domain: 25594878) +Conflicts : 897958 (Analyzed: 897958) +Restarts : 3300 (Average: 272.11 Last: 326) +Model-Level : 4372.0 +Problems : 34 (Average Length: 117.00 Splits: 0) +Lemmas : 897958 (Deleted: 847731) + Binary : 19266 (Ratio: 2.15%) + Ternary : 3993 (Ratio: 0.44%) + Conflict : 897958 (Average Length: 913.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 897958 (Average: 27.28 Max: 1786 Sum: 24499836) + Executed : 897900 (Average: 27.28 Max: 1786 Sum: 24493129 Ratio: 99.97%) + Bounded : 58 (Average: 115.64 Max: 117 Sum: 6707 Ratio: 0.03%) + +Rules : 1028283 (Original: 843628) +Atoms : 59257 +Bodies : 791604 (Original: 606949) + Count : 9712 (Original: 27041) +Equivalences : 188391 (Atom=Atom: 172 Body=Body: 0 Other: 188219) +Tight : Yes +Variables : 578090 (Eliminated: 0 Frozen: 191082) +Constraints : 4201647 (Binary: 91.4% Ternary: 7.1% Other: 1.6%) + +Memory Peak : 1003MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 21.74s +Memory: 939MB (+0MB) +UNKNOWN +Iteration Time: 21.74s + +Iteration 34 +Queue: [(0,115,33,True)] +Grounded Until: 115 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 35 +Time : 761.098s (Solving: 745.08s 1st Model: 0.11s Unsat: 0.00s) +CPU Time : 761.316s + +Choices : 26170326 (Domain: 26033413) +Conflicts : 926147 (Analyzed: 926147) +Restarts : 3400 (Average: 272.40 Last: 326) +Model-Level : 4372.0 +Problems : 35 (Average Length: 117.00 Splits: 0) +Lemmas : 926147 (Deleted: 876371) + Binary : 19483 (Ratio: 2.10%) + Ternary : 4055 (Ratio: 0.44%) + Conflict : 926147 (Average Length: 916.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 926147 (Average: 26.88 Max: 1786 Sum: 24896913) + Executed : 926089 (Average: 26.88 Max: 1786 Sum: 24890206 Ratio: 99.97%) + Bounded : 58 (Average: 115.64 Max: 117 Sum: 6707 Ratio: 0.03%) + +Rules : 1028283 (Original: 843628) +Atoms : 59257 +Bodies : 791604 (Original: 606949) + Count : 9712 (Original: 27041) +Equivalences : 188391 (Atom=Atom: 172 Body=Body: 0 Other: 188219) +Tight : Yes +Variables : 578090 (Eliminated: 0 Frozen: 191082) +Constraints : 4201647 (Binary: 91.4% Ternary: 7.1% Other: 1.6%) + +Memory Peak : 1003MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 20.89s +Memory: 939MB (+0MB) +UNKNOWN +Iteration Time: 20.89s + +Iteration 35 +Queue: [(0,115,34,True)] +Grounded Until: 115 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 36 +Time : 781.678s (Solving: 765.56s 1st Model: 0.11s Unsat: 0.00s) +CPU Time : 781.904s + +Choices : 26554069 (Domain: 26416150) +Conflicts : 951483 (Analyzed: 951483) +Restarts : 3500 (Average: 271.85 Last: 326) +Model-Level : 4372.0 +Problems : 36 (Average Length: 117.00 Splits: 0) +Lemmas : 951483 (Deleted: 900418) + Binary : 19900 (Ratio: 2.09%) + Ternary : 4159 (Ratio: 0.44%) + Conflict : 951483 (Average Length: 912.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 951483 (Average: 26.53 Max: 1786 Sum: 25243389) + Executed : 951425 (Average: 26.52 Max: 1786 Sum: 25236682 Ratio: 99.97%) + Bounded : 58 (Average: 115.64 Max: 117 Sum: 6707 Ratio: 0.03%) + +Rules : 1028283 (Original: 843628) +Atoms : 59257 +Bodies : 791604 (Original: 606949) + Count : 9712 (Original: 27041) +Equivalences : 188391 (Atom=Atom: 172 Body=Body: 0 Other: 188219) +Tight : Yes +Variables : 578090 (Eliminated: 0 Frozen: 191082) +Constraints : 4201647 (Binary: 91.4% Ternary: 7.1% Other: 1.6%) + +Memory Peak : 1003MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 20.59s +Memory: 939MB (+0MB) +UNKNOWN +Iteration Time: 20.59s + +Iteration 36 +Queue: [(0,115,35,True)] +Grounded Until: 115 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 37 +Time : 801.127s (Solving: 784.90s 1st Model: 0.11s Unsat: 0.00s) +CPU Time : 801.364s + +Choices : 26892139 (Domain: 26753297) +Conflicts : 979217 (Analyzed: 979217) +Restarts : 3600 (Average: 272.00 Last: 326) +Model-Level : 4372.0 +Problems : 37 (Average Length: 117.00 Splits: 0) +Lemmas : 979217 (Deleted: 928036) + Binary : 20098 (Ratio: 2.05%) + Ternary : 4198 (Ratio: 0.43%) + Conflict : 979217 (Average Length: 912.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 979217 (Average: 26.09 Max: 1786 Sum: 25546029) + Executed : 979159 (Average: 26.08 Max: 1786 Sum: 25539322 Ratio: 99.97%) + Bounded : 58 (Average: 115.64 Max: 117 Sum: 6707 Ratio: 0.03%) + +Rules : 1028283 (Original: 843628) +Atoms : 59257 +Bodies : 791604 (Original: 606949) + Count : 9712 (Original: 27041) +Equivalences : 188391 (Atom=Atom: 172 Body=Body: 0 Other: 188219) +Tight : Yes +Variables : 578090 (Eliminated: 0 Frozen: 191082) +Constraints : 4201647 (Binary: 91.4% Ternary: 7.1% Other: 1.6%) + +Memory Peak : 1003MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 19.46s +Memory: 939MB (+0MB) +UNKNOWN +Iteration Time: 19.46s + +Iteration 37 +Queue: [(0,115,36,True)] +Grounded Until: 115 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 38 +Time : 818.601s (Solving: 802.27s 1st Model: 0.11s Unsat: 0.00s) +CPU Time : 818.848s + +Choices : 27181636 (Domain: 27042680) +Conflicts : 1007186 (Analyzed: 1007186) +Restarts : 3700 (Average: 272.21 Last: 326) +Model-Level : 4372.0 +Problems : 38 (Average Length: 117.00 Splits: 0) +Lemmas : 1007186 (Deleted: 955194) + Binary : 20322 (Ratio: 2.02%) + Ternary : 4254 (Ratio: 0.42%) + Conflict : 1007186 (Average Length: 909.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 1007186 (Average: 25.61 Max: 1786 Sum: 25796334) + Executed : 1007128 (Average: 25.61 Max: 1786 Sum: 25789627 Ratio: 99.97%) + Bounded : 58 (Average: 115.64 Max: 117 Sum: 6707 Ratio: 0.03%) + +Rules : 1028283 (Original: 843628) +Atoms : 59257 +Bodies : 791604 (Original: 606949) + Count : 9712 (Original: 27041) +Equivalences : 188391 (Atom=Atom: 172 Body=Body: 0 Other: 188219) +Tight : Yes +Variables : 578090 (Eliminated: 0 Frozen: 191082) +Constraints : 4201647 (Binary: 91.4% Ternary: 7.1% Other: 1.6%) + +Memory Peak : 1003MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 17.48s +Memory: 939MB (+0MB) +UNKNOWN +Iteration Time: 17.48s + +Iteration 38 +Queue: [(0,115,37,True)] +Grounded Until: 115 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 39 +Time : 838.181s (Solving: 821.75s 1st Model: 0.11s Unsat: 0.00s) +CPU Time : 838.436s + +Choices : 27479457 (Domain: 27340496) +Conflicts : 1034205 (Analyzed: 1034205) +Restarts : 3800 (Average: 272.16 Last: 326) +Model-Level : 4372.0 +Problems : 39 (Average Length: 117.00 Splits: 0) +Lemmas : 1034205 (Deleted: 979655) + Binary : 20519 (Ratio: 1.98%) + Ternary : 4287 (Ratio: 0.41%) + Conflict : 1034205 (Average Length: 909.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 1034205 (Average: 25.20 Max: 1786 Sum: 26058309) + Executed : 1034147 (Average: 25.19 Max: 1786 Sum: 26051602 Ratio: 99.97%) + Bounded : 58 (Average: 115.64 Max: 117 Sum: 6707 Ratio: 0.03%) + +Rules : 1028283 (Original: 843628) +Atoms : 59257 +Bodies : 791604 (Original: 606949) + Count : 9712 (Original: 27041) +Equivalences : 188391 (Atom=Atom: 172 Body=Body: 0 Other: 188219) +Tight : Yes +Variables : 578090 (Eliminated: 0 Frozen: 191082) +Constraints : 4201647 (Binary: 91.4% Ternary: 7.1% Other: 1.6%) + +Memory Peak : 1003MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 19.59s +Memory: 939MB (+0MB) +UNKNOWN +Iteration Time: 19.59s + +Iteration 39 +Queue: [(0,115,38,True)] +Grounded Until: 115 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 40 +Time : 860.478s (Solving: 843.93s 1st Model: 0.11s Unsat: 0.00s) +CPU Time : 860.744s + +Choices : 27848665 (Domain: 27709206) +Conflicts : 1065225 (Analyzed: 1065225) +Restarts : 3900 (Average: 273.13 Last: 326) +Model-Level : 4372.0 +Problems : 40 (Average Length: 117.00 Splits: 0) +Lemmas : 1065225 (Deleted: 1012000) + Binary : 20669 (Ratio: 1.94%) + Ternary : 4323 (Ratio: 0.41%) + Conflict : 1065225 (Average Length: 908.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 1065225 (Average: 24.77 Max: 1786 Sum: 26390596) + Executed : 1065167 (Average: 24.77 Max: 1786 Sum: 26383889 Ratio: 99.97%) + Bounded : 58 (Average: 115.64 Max: 117 Sum: 6707 Ratio: 0.03%) + +Rules : 1028283 (Original: 843628) +Atoms : 59257 +Bodies : 791604 (Original: 606949) + Count : 9712 (Original: 27041) +Equivalences : 188391 (Atom=Atom: 172 Body=Body: 0 Other: 188219) +Tight : Yes +Variables : 578090 (Eliminated: 0 Frozen: 191082) +Constraints : 4201647 (Binary: 91.4% Ternary: 7.1% Other: 1.6%) + +Memory Peak : 1003MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 22.31s +Memory: 939MB (+0MB) +UNKNOWN +Iteration Time: 22.31s + +Iteration 40 +Queue: [(0,115,39,True)] +Grounded Until: 115 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 41 +Time : 882.690s (Solving: 866.04s 1st Model: 0.11s Unsat: 0.00s) +CPU Time : 882.964s + +Choices : 28246722 (Domain: 28106873) +Conflicts : 1094300 (Analyzed: 1094300) +Restarts : 4000 (Average: 273.57 Last: 326) +Model-Level : 4372.0 +Problems : 41 (Average Length: 117.00 Splits: 0) +Lemmas : 1094300 (Deleted: 1039235) + Binary : 20793 (Ratio: 1.90%) + Ternary : 4351 (Ratio: 0.40%) + Conflict : 1094300 (Average Length: 905.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 1094300 (Average: 24.45 Max: 1786 Sum: 26750286) + Executed : 1094242 (Average: 24.44 Max: 1786 Sum: 26743579 Ratio: 99.97%) + Bounded : 58 (Average: 115.64 Max: 117 Sum: 6707 Ratio: 0.03%) + +Rules : 1028283 (Original: 843628) +Atoms : 59257 +Bodies : 791604 (Original: 606949) + Count : 9712 (Original: 27041) +Equivalences : 188391 (Atom=Atom: 172 Body=Body: 0 Other: 188219) +Tight : Yes +Variables : 578090 (Eliminated: 0 Frozen: 191082) +Constraints : 4201647 (Binary: 91.4% Ternary: 7.1% Other: 1.6%) + +Memory Peak : 1003MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 22.22s +Memory: 939MB (+0MB) +UNKNOWN +Iteration Time: 22.22s + +Iteration 41 +Queue: [(0,115,40,True)] +Grounded Until: 115 +Solving... +*** Info : (planner): INTERRUPTED by signal! +UNKNOWN + +INTERRUPTED : 1 + +Models : 0+ +Calls : 42 +Time : 894.406s (Solving: 877.62s 1st Model: 0.11s Unsat: 0.00s) +CPU Time : 894.664s + +Choices : 28389015 (Domain: 28249163) +Conflicts : 1107975 (Analyzed: 1107975) +Restarts : 4057 (Average: 273.10 Last: 326) +Model-Level : 4372.0 +Problems : 42 (Average Length: 117.00 Splits: 0) +Lemmas : 1107975 (Deleted: 1054557) + Binary : 20823 (Ratio: 1.88%) + Ternary : 4364 (Ratio: 0.39%) + Conflict : 1107975 (Average Length: 906.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 1107975 (Average: 24.25 Max: 1786 Sum: 26871982) + Executed : 1107917 (Average: 24.25 Max: 1786 Sum: 26865275 Ratio: 99.98%) + Bounded : 58 (Average: 115.64 Max: 117 Sum: 6707 Ratio: 0.02%) + +Rules : 1028283 (Original: 843628) +Atoms : 59257 +Bodies : 791604 (Original: 606949) + Count : 9712 (Original: 27041) +Equivalences : 188391 (Atom=Atom: 172 Body=Body: 0 Other: 188219) +Tight : Yes +Variables : 578090 (Eliminated: 0 Frozen: 191082) +Constraints : 4201647 (Binary: 91.4% Ternary: 7.1% Other: 1.6%) + +Memory Peak : 1003MB +Max. Length : 115 steps +Models : 1 + +