From e7da53f054b3f86c94da07807be588003ccd4032 Mon Sep 17 00:00:00 2001 From: potassco-bot Date: Thu, 22 Feb 2018 00:32:44 +0100 Subject: [PATCH] Add benchmark result [gc-ta1-tt1-single-shot | ipc-2011 | elevator-sequential-satisficing | 1] --- ...2011_elevator-sequential-satisficing_1.env | 60 + ...2011_elevator-sequential-satisficing_1.err | 23 + ...2011_elevator-sequential-satisficing_1.out | 2908 +++++++++++++++++ 3 files changed, 2991 insertions(+) create mode 100644 gc-ta1-tt1-single-shot/ipc-2011_elevator-sequential-satisficing_1.env create mode 100644 gc-ta1-tt1-single-shot/ipc-2011_elevator-sequential-satisficing_1.err create mode 100644 gc-ta1-tt1-single-shot/ipc-2011_elevator-sequential-satisficing_1.out diff --git a/gc-ta1-tt1-single-shot/ipc-2011_elevator-sequential-satisficing_1.env b/gc-ta1-tt1-single-shot/ipc-2011_elevator-sequential-satisficing_1.env new file mode 100644 index 000000000..c7c56d098 --- /dev/null +++ b/gc-ta1-tt1-single-shot/ipc-2011_elevator-sequential-satisficing_1.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/elevator-sequential-satisficing/domain.pddl +- /home/pluehne/Documents/ASP/pddl-instances/ipc-2011/domains/elevator-sequential-satisficing/instances/instance-1.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 30 +- -T 30 +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: elevator-sequential-satisficing + instance: 1 + ipc: ipc-2011 + planLength: 30 +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_elevator-sequential-satisficing_1.err b/gc-ta1-tt1-single-shot/ipc-2011_elevator-sequential-satisficing_1.err new file mode 100644 index 000000000..e1db5009d --- /dev/null +++ b/gc-ta1-tt1-single-shot/ipc-2011_elevator-sequential-satisficing_1.err @@ -0,0 +1,23 @@ +# 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': 'elevator-sequential-satisficing', 'instance': 1, 'planLength': 30} +# 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/elevator-sequential-satisficing/domain.pddl', '/home/pluehne/Documents/ASP/pddl-instances/ipc-2011/domains/elevator-sequential-satisficing/instances/instance-1.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 30', '-T 30'] +# working directory: /home/pluehne/Documents/ASP/plasp-javier/encodings/planner +# exit code: 0 +/home/pluehne/Documents/ASP/plasp-javier/encodings/strips/strips-incremental.lp:66:15-28: info: atom does not occur in any rule head: + mutexGroup(G) + +/home/pluehne/Documents/ASP/plasp-javier/encodings/strips/strips-incremental.lp:66:30-45: info: atom does not occur in any rule head: + contains(G,X,V) + +/home/pluehne/Documents/ASP/plasp-javier/encodings/strips/strips-incremental.lp:67:15-28: info: atom does not occur in any rule head: + mutexGroup(G) + +/home/pluehne/Documents/ASP/plasp-javier/encodings/strips/strips-incremental.lp:74:41-56: info: atom does not occur in any rule head: + contains(G,X,V) + +/home/pluehne/Documents/ASP/plasp-javier/encodings/strips/strips-incremental.lp:84:41-56: info: atom does not occur in any rule head: + contains(G,X,V) + +TIMEOUT CPU 900.09 MEM 429952 MAXMEM 429952 STALE 1 MAXMEM_RSS 349268 + + diff --git a/gc-ta1-tt1-single-shot/ipc-2011_elevator-sequential-satisficing_1.out b/gc-ta1-tt1-single-shot/ipc-2011_elevator-sequential-satisficing_1.out new file mode 100644 index 000000000..26b9670f7 --- /dev/null +++ b/gc-ta1-tt1-single-shot/ipc-2011_elevator-sequential-satisficing_1.out @@ -0,0 +1,2908 @@ +INFO Running translator. +INFO translator input: ['/home/pluehne/Documents/ASP/pddl-instances/ipc-2011/domains/elevator-sequential-satisficing/domain.pddl', '/home/pluehne/Documents/ASP/pddl-instances/ipc-2011/domains/elevator-sequential-satisficing/instances/instance-1.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/elevator-sequential-satisficing/domain.pddl /home/pluehne/Documents/ASP/pddl-instances/ipc-2011/domains/elevator-sequential-satisficing/instances/instance-1.pddl +Parsing... +Parsing: [0.030s CPU, 0.033s wall-clock] +Normalizing task... [0.010s CPU, 0.002s wall-clock] +Instantiating... +Generating Datalog program... [0.000s CPU, 0.008s wall-clock] +Normalizing Datalog program... +Normalizing Datalog program: [0.020s CPU, 0.022s wall-clock] +Preparing model... [0.030s CPU, 0.024s wall-clock] +Generated 46 rules. +Computing model... [0.440s CPU, 0.445s wall-clock] +3460 relevant atoms +2552 auxiliary atoms +6012 final queue length +11142 total queue pushes +Completing instantiation... [1.010s CPU, 1.002s wall-clock] +Instantiating: [1.500s CPU, 1.508s wall-clock] +Computing fact groups... +Finding invariants... +12 initial candidates +Finding invariants: [0.030s CPU, 0.033s wall-clock] +Checking invariant weight... [0.010s CPU, 0.002s wall-clock] +Instantiating groups... [0.010s CPU, 0.017s wall-clock] +Collecting mutex groups... [0.000s CPU, 0.002s wall-clock] +Choosing groups... +0 uncovered facts +Choosing groups: [0.010s CPU, 0.007s wall-clock] +Building translation key... [0.000s CPU, 0.004s wall-clock] +Computing fact groups: [0.080s CPU, 0.079s wall-clock] +Building STRIPS to SAS dictionary... [0.000s CPU, 0.002s wall-clock] +Building dictionary for full mutex groups... [0.000s CPU, 0.001s wall-clock] +Building mutex information... +Building mutex information: [0.000s CPU, 0.003s wall-clock] +Translating task... +Processing axioms... +Simplifying axioms... [0.000s CPU, 0.000s wall-clock] +Processing axioms: [0.050s CPU, 0.044s wall-clock] +Translating task: [0.820s CPU, 0.812s wall-clock] +0 effect conditions simplified +0 implied preconditions added +Detecting unreachable propositions... +0 operators removed +0 axioms removed +22 propositions removed +Detecting unreachable propositions: [0.400s CPU, 0.404s wall-clock] +Reordering and filtering variables... +22 of 22 variables necessary. +0 of 22 mutex groups necessary. +2816 of 2816 operators necessary. +0 of 0 axiom rules necessary. +Reordering and filtering variables: [0.140s CPU, 0.131s wall-clock] +Translator variables: 22 +Translator derived variables: 0 +Translator facts: 340 +Translator goal facts: 14 +Translator mutex groups: 0 +Translator total mutex groups size: 0 +Translator operators: 2816 +Translator axioms: 0 +Translator task size: 16720 +Translator peak memory: 47308 KB +Writing output... [0.290s CPU, 0.307s wall-clock] +Done! [3.300s CPU, 3.319s wall-clock] +planner.py version 0.0.1 + +Time: 0.67s +Memory: 95MB + +Iteration 1 +Queue: [(0,30,0,True)] +Grounded Until: 0 +Expected Memory: 95MB +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]), ('check', [30])] +Grounding Time: 1.28s +Memory: 205MB (+110MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 1+ +Calls : 1 +Time : 2.991s (Solving: 0.07s 1st Model: 0.06s Unsat: 0.00s) +CPU Time : 2.888s + +Choices : 3949 (Domain: 3925) +Conflicts : 94 (Analyzed: 94) +Restarts : 1 (Average: 94.00 Last: 19) +Model-Level : 1229.0 +Problems : 1 (Average Length: 32.00 Splits: 0) +Lemmas : 94 (Deleted: 0) + Binary : 38 (Ratio: 40.43%) + Ternary : 20 (Ratio: 21.28%) + Conflict : 94 (Average Length: 30.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 94 (Average: 28.99 Max: 359 Sum: 2725) + Executed : 94 (Average: 28.99 Max: 359 Sum: 2725 Ratio: 100.00%) + Bounded : 0 (Average: 0.00 Max: 0 Sum: 0 Ratio: 0.00%) + +Rules : 0 +Atoms : 0 +Bodies : 0 +Tight : Yes +Variables : 102462 (Eliminated: 0 Frozen: 9069) +Constraints : 679498 (Binary: 97.1% Ternary: 1.4% Other: 1.5%) + +Memory Peak : 376MB +Max. Length : 0 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 0.14s +Memory: 312MB (+107MB) +SAT +Testing... +NOT SERIALIZABLE +Testing Time: 1.14s +Memory: 316MB (+4MB) +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 2 +Time : 28.875s (Solving: 25.29s 1st Model: 0.06s Unsat: 0.00s) +CPU Time : 28.784s + +Choices : 1668764 (Domain: 1668740) +Conflicts : 31743 (Analyzed: 31743) +Restarts : 101 (Average: 314.29 Last: 143) +Model-Level : 1229.0 +Problems : 2 (Average Length: 32.00 Splits: 0) +Lemmas : 31743 (Deleted: 25656) + Binary : 862 (Ratio: 2.72%) + Ternary : 707 (Ratio: 2.23%) + Conflict : 31743 (Average Length: 569.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 31743 (Average: 51.61 Max: 1535 Sum: 1638358) + Executed : 31678 (Average: 51.55 Max: 1535 Sum: 1636371 Ratio: 99.88%) + Bounded : 65 (Average: 30.57 Max: 32 Sum: 1987 Ratio: 0.12%) + +Rules : 222636 (Original: 222598) +Atoms : 6829 +Bodies : 147015 (Original: 146977) + Count : 629 (Original: 633) +Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207) +Tight : Yes +Variables : 103790 (Eliminated: 0 Frozen: 85188) +Constraints : 897395 (Binary: 97.7% Ternary: 1.0% Other: 1.3%) + +Memory Peak : 376MB +Max. Length : 0 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 25.40s +Memory: 318MB (+2MB) +UNKNOWN +Iteration Time: 28.76s + +Iteration 2 +Queue: [(0,30,1,True)] +Grounded Until: 30 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 3 +Time : 43.079s (Solving: 39.46s 1st Model: 0.06s Unsat: 0.00s) +CPU Time : 42.996s + +Choices : 2557018 (Domain: 2556994) +Conflicts : 61145 (Analyzed: 61145) +Restarts : 201 (Average: 304.20 Last: 230) +Model-Level : 1229.0 +Problems : 3 (Average Length: 32.00 Splits: 0) +Lemmas : 61145 (Deleted: 51706) + Binary : 1430 (Ratio: 2.34%) + Ternary : 1142 (Ratio: 1.87%) + Conflict : 61145 (Average Length: 652.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 61145 (Average: 40.30 Max: 1535 Sum: 2464203) + Executed : 61074 (Average: 40.27 Max: 1535 Sum: 2462055 Ratio: 99.91%) + Bounded : 71 (Average: 30.25 Max: 32 Sum: 2148 Ratio: 0.09%) + +Rules : 222636 (Original: 222598) +Atoms : 6829 +Bodies : 147015 (Original: 146977) + Count : 629 (Original: 633) +Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207) +Tight : Yes +Variables : 103790 (Eliminated: 0 Frozen: 85188) +Constraints : 879798 (Binary: 97.7% Ternary: 1.0% Other: 1.3%) + +Memory Peak : 376MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 14.22s +Memory: 318MB (+0MB) +UNKNOWN +Iteration Time: 14.22s + +Iteration 3 +Queue: [(0,30,2,True)] +Grounded Until: 30 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 4 +Time : 57.174s (Solving: 53.52s 1st Model: 0.06s Unsat: 0.00s) +CPU Time : 57.100s + +Choices : 3090641 (Domain: 3090617) +Conflicts : 90647 (Analyzed: 90647) +Restarts : 301 (Average: 301.15 Last: 289) +Model-Level : 1229.0 +Problems : 4 (Average Length: 32.00 Splits: 0) +Lemmas : 90647 (Deleted: 77680) + Binary : 1640 (Ratio: 1.81%) + Ternary : 1380 (Ratio: 1.52%) + Conflict : 90647 (Average Length: 838.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 90647 (Average: 32.23 Max: 1535 Sum: 2921152) + Executed : 90573 (Average: 32.20 Max: 1535 Sum: 2919001 Ratio: 99.93%) + Bounded : 74 (Average: 29.07 Max: 32 Sum: 2151 Ratio: 0.07%) + +Rules : 222636 (Original: 222598) +Atoms : 6829 +Bodies : 147015 (Original: 146977) + Count : 629 (Original: 633) +Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207) +Tight : Yes +Variables : 103790 (Eliminated: 0 Frozen: 85188) +Constraints : 877891 (Binary: 97.7% Ternary: 1.0% Other: 1.3%) + +Memory Peak : 376MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 14.11s +Memory: 318MB (+0MB) +UNKNOWN +Iteration Time: 14.11s + +Iteration 4 +Queue: [(0,30,3,True)] +Grounded Until: 30 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 5 +Time : 70.461s (Solving: 66.77s 1st Model: 0.06s Unsat: 0.00s) +CPU Time : 70.392s + +Choices : 3775179 (Domain: 3775155) +Conflicts : 117031 (Analyzed: 117031) +Restarts : 401 (Average: 291.85 Last: 289) +Model-Level : 1229.0 +Problems : 5 (Average Length: 32.00 Splits: 0) +Lemmas : 117031 (Deleted: 102014) + Binary : 1764 (Ratio: 1.51%) + Ternary : 1519 (Ratio: 1.30%) + Conflict : 117031 (Average Length: 935.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 117031 (Average: 30.04 Max: 1535 Sum: 3516182) + Executed : 116955 (Average: 30.03 Max: 1535 Sum: 3513967 Ratio: 99.94%) + Bounded : 76 (Average: 29.14 Max: 32 Sum: 2215 Ratio: 0.06%) + +Rules : 222636 (Original: 222598) +Atoms : 6829 +Bodies : 147015 (Original: 146977) + Count : 629 (Original: 633) +Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207) +Tight : Yes +Variables : 103790 (Eliminated: 0 Frozen: 85188) +Constraints : 877891 (Binary: 97.7% Ternary: 1.0% Other: 1.3%) + +Memory Peak : 376MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 13.30s +Memory: 318MB (+0MB) +UNKNOWN +Iteration Time: 13.30s + +Iteration 5 +Queue: [(0,30,4,True)] +Grounded Until: 30 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 6 +Time : 88.035s (Solving: 84.31s 1st Model: 0.06s Unsat: 0.00s) +CPU Time : 87.972s + +Choices : 4346761 (Domain: 4346737) +Conflicts : 146155 (Analyzed: 146155) +Restarts : 501 (Average: 291.73 Last: 289) +Model-Level : 1229.0 +Problems : 6 (Average Length: 32.00 Splits: 0) +Lemmas : 146155 (Deleted: 132485) + Binary : 1992 (Ratio: 1.36%) + Ternary : 1708 (Ratio: 1.17%) + Conflict : 146155 (Average Length: 1219.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 146155 (Average: 27.43 Max: 1535 Sum: 4009477) + Executed : 146071 (Average: 27.42 Max: 1535 Sum: 4007099 Ratio: 99.94%) + Bounded : 84 (Average: 28.31 Max: 32 Sum: 2378 Ratio: 0.06%) + +Rules : 222636 (Original: 222598) +Atoms : 6829 +Bodies : 147015 (Original: 146977) + Count : 629 (Original: 633) +Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207) +Tight : Yes +Variables : 103790 (Eliminated: 0 Frozen: 85188) +Constraints : 877867 (Binary: 97.7% Ternary: 1.0% Other: 1.3%) + +Memory Peak : 446MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 17.59s +Memory: 382MB (+64MB) +UNKNOWN +Iteration Time: 17.59s + +Iteration 6 +Queue: [(0,30,5,True)] +Grounded Until: 30 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 7 +Time : 104.389s (Solving: 100.62s 1st Model: 0.06s Unsat: 0.00s) +CPU Time : 104.336s + +Choices : 4884968 (Domain: 4884944) +Conflicts : 175894 (Analyzed: 175894) +Restarts : 601 (Average: 292.67 Last: 289) +Model-Level : 1229.0 +Problems : 7 (Average Length: 32.00 Splits: 0) +Lemmas : 175894 (Deleted: 159446) + Binary : 2286 (Ratio: 1.30%) + Ternary : 1954 (Ratio: 1.11%) + Conflict : 175894 (Average Length: 1310.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 175894 (Average: 25.37 Max: 1535 Sum: 4462744) + Executed : 175802 (Average: 25.36 Max: 1535 Sum: 4460296 Ratio: 99.95%) + Bounded : 92 (Average: 26.61 Max: 32 Sum: 2448 Ratio: 0.05%) + +Rules : 222636 (Original: 222598) +Atoms : 6829 +Bodies : 147015 (Original: 146977) + Count : 629 (Original: 633) +Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207) +Tight : Yes +Variables : 103790 (Eliminated: 0 Frozen: 85188) +Constraints : 877754 (Binary: 97.7% Ternary: 1.0% Other: 1.3%) + +Memory Peak : 446MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 16.36s +Memory: 382MB (+0MB) +UNKNOWN +Iteration Time: 16.36s + +Iteration 7 +Queue: [(0,30,6,True)] +Grounded Until: 30 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 8 +Time : 118.877s (Solving: 115.08s 1st Model: 0.06s Unsat: 0.00s) +CPU Time : 118.832s + +Choices : 5400238 (Domain: 5400214) +Conflicts : 204393 (Analyzed: 204393) +Restarts : 701 (Average: 291.57 Last: 289) +Model-Level : 1229.0 +Problems : 8 (Average Length: 32.00 Splits: 0) +Lemmas : 204393 (Deleted: 187326) + Binary : 2553 (Ratio: 1.25%) + Ternary : 2172 (Ratio: 1.06%) + Conflict : 204393 (Average Length: 1371.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 204393 (Average: 23.90 Max: 1535 Sum: 4885113) + Executed : 204297 (Average: 23.89 Max: 1535 Sum: 4882630 Ratio: 99.95%) + Bounded : 96 (Average: 25.86 Max: 32 Sum: 2483 Ratio: 0.05%) + +Rules : 222636 (Original: 222598) +Atoms : 6829 +Bodies : 147015 (Original: 146977) + Count : 629 (Original: 633) +Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207) +Tight : Yes +Variables : 103790 (Eliminated: 0 Frozen: 85188) +Constraints : 877018 (Binary: 97.7% Ternary: 1.0% Other: 1.3%) + +Memory Peak : 446MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 14.50s +Memory: 382MB (+0MB) +UNKNOWN +Iteration Time: 14.50s + +Iteration 8 +Queue: [(0,30,7,True)] +Grounded Until: 30 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 9 +Time : 134.154s (Solving: 130.32s 1st Model: 0.06s Unsat: 0.00s) +CPU Time : 134.116s + +Choices : 5842268 (Domain: 5842244) +Conflicts : 232860 (Analyzed: 232860) +Restarts : 801 (Average: 290.71 Last: 289) +Model-Level : 1229.0 +Problems : 9 (Average Length: 32.00 Splits: 0) +Lemmas : 232860 (Deleted: 213883) + Binary : 2715 (Ratio: 1.17%) + Ternary : 2331 (Ratio: 1.00%) + Conflict : 232860 (Average Length: 1436.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 232860 (Average: 22.49 Max: 1535 Sum: 5236417) + Executed : 232758 (Average: 22.48 Max: 1535 Sum: 5233897 Ratio: 99.95%) + Bounded : 102 (Average: 24.71 Max: 32 Sum: 2520 Ratio: 0.05%) + +Rules : 222636 (Original: 222598) +Atoms : 6829 +Bodies : 147015 (Original: 146977) + Count : 629 (Original: 633) +Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207) +Tight : Yes +Variables : 103790 (Eliminated: 0 Frozen: 85188) +Constraints : 877006 (Binary: 97.7% Ternary: 1.0% Other: 1.3%) + +Memory Peak : 446MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 15.29s +Memory: 382MB (+0MB) +UNKNOWN +Iteration Time: 15.29s + +Iteration 9 +Queue: [(0,30,8,True)] +Grounded Until: 30 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 10 +Time : 149.430s (Solving: 145.57s 1st Model: 0.06s Unsat: 0.00s) +CPU Time : 149.400s + +Choices : 6217683 (Domain: 6217659) +Conflicts : 260552 (Analyzed: 260552) +Restarts : 901 (Average: 289.18 Last: 289) +Model-Level : 1229.0 +Problems : 10 (Average Length: 32.00 Splits: 0) +Lemmas : 260552 (Deleted: 238946) + Binary : 2850 (Ratio: 1.09%) + Ternary : 2454 (Ratio: 0.94%) + Conflict : 260552 (Average Length: 1441.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 260552 (Average: 21.18 Max: 1535 Sum: 5518379) + Executed : 260449 (Average: 21.17 Max: 1535 Sum: 5515858 Ratio: 99.95%) + Bounded : 103 (Average: 24.48 Max: 32 Sum: 2521 Ratio: 0.05%) + +Rules : 222636 (Original: 222598) +Atoms : 6829 +Bodies : 147015 (Original: 146977) + Count : 629 (Original: 633) +Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207) +Tight : Yes +Variables : 103790 (Eliminated: 0 Frozen: 85188) +Constraints : 876994 (Binary: 97.7% Ternary: 1.0% Other: 1.3%) + +Memory Peak : 446MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 15.29s +Memory: 382MB (+0MB) +UNKNOWN +Iteration Time: 15.29s + +Iteration 10 +Queue: [(0,30,9,True)] +Grounded Until: 30 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 11 +Time : 162.777s (Solving: 158.89s 1st Model: 0.06s Unsat: 0.00s) +CPU Time : 162.752s + +Choices : 6580720 (Domain: 6580696) +Conflicts : 287204 (Analyzed: 287204) +Restarts : 1001 (Average: 286.92 Last: 289) +Model-Level : 1229.0 +Problems : 11 (Average Length: 32.00 Splits: 0) +Lemmas : 287204 (Deleted: 262781) + Binary : 2952 (Ratio: 1.03%) + Ternary : 2553 (Ratio: 0.89%) + Conflict : 287204 (Average Length: 1448.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 287204 (Average: 20.14 Max: 1535 Sum: 5783024) + Executed : 287099 (Average: 20.13 Max: 1535 Sum: 5780470 Ratio: 99.96%) + Bounded : 105 (Average: 24.32 Max: 32 Sum: 2554 Ratio: 0.04%) + +Rules : 222636 (Original: 222598) +Atoms : 6829 +Bodies : 147015 (Original: 146977) + Count : 629 (Original: 633) +Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207) +Tight : Yes +Variables : 103790 (Eliminated: 0 Frozen: 85188) +Constraints : 876994 (Binary: 97.7% Ternary: 1.0% Other: 1.3%) + +Memory Peak : 446MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 13.36s +Memory: 382MB (+0MB) +UNKNOWN +Iteration Time: 13.36s + +Iteration 11 +Queue: [(0,30,10,True)] +Grounded Until: 30 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 12 +Time : 176.984s (Solving: 173.07s 1st Model: 0.06s Unsat: 0.00s) +CPU Time : 176.964s + +Choices : 6920813 (Domain: 6920789) +Conflicts : 313774 (Analyzed: 313774) +Restarts : 1101 (Average: 284.99 Last: 289) +Model-Level : 1229.0 +Problems : 12 (Average Length: 32.00 Splits: 0) +Lemmas : 313774 (Deleted: 288599) + Binary : 3030 (Ratio: 0.97%) + Ternary : 2633 (Ratio: 0.84%) + Conflict : 313774 (Average Length: 1456.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 313774 (Average: 19.21 Max: 1535 Sum: 6026128) + Executed : 313667 (Average: 19.20 Max: 1535 Sum: 6023541 Ratio: 99.96%) + Bounded : 107 (Average: 24.18 Max: 32 Sum: 2587 Ratio: 0.04%) + +Rules : 222636 (Original: 222598) +Atoms : 6829 +Bodies : 147015 (Original: 146977) + Count : 629 (Original: 633) +Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207) +Tight : Yes +Variables : 103790 (Eliminated: 0 Frozen: 85188) +Constraints : 876982 (Binary: 97.7% Ternary: 1.0% Other: 1.3%) + +Memory Peak : 446MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 14.22s +Memory: 382MB (+0MB) +UNKNOWN +Iteration Time: 14.22s + +Iteration 12 +Queue: [(0,30,11,True)] +Grounded Until: 30 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 13 +Time : 191.910s (Solving: 187.97s 1st Model: 0.06s Unsat: 0.00s) +CPU Time : 191.896s + +Choices : 7234369 (Domain: 7234345) +Conflicts : 342508 (Analyzed: 342508) +Restarts : 1201 (Average: 285.19 Last: 289) +Model-Level : 1229.0 +Problems : 13 (Average Length: 32.00 Splits: 0) +Lemmas : 342508 (Deleted: 317256) + Binary : 3117 (Ratio: 0.91%) + Ternary : 2681 (Ratio: 0.78%) + Conflict : 342508 (Average Length: 1477.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 342508 (Average: 18.22 Max: 1535 Sum: 6239123) + Executed : 342401 (Average: 18.21 Max: 1535 Sum: 6236536 Ratio: 99.96%) + Bounded : 107 (Average: 24.18 Max: 32 Sum: 2587 Ratio: 0.04%) + +Rules : 222636 (Original: 222598) +Atoms : 6829 +Bodies : 147015 (Original: 146977) + Count : 629 (Original: 633) +Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207) +Tight : Yes +Variables : 103790 (Eliminated: 0 Frozen: 85188) +Constraints : 876970 (Binary: 97.7% Ternary: 1.0% Other: 1.3%) + +Memory Peak : 446MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 14.93s +Memory: 382MB (+0MB) +UNKNOWN +Iteration Time: 14.93s + +Iteration 13 +Queue: [(0,30,12,True)] +Grounded Until: 30 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 14 +Time : 206.296s (Solving: 202.32s 1st Model: 0.06s Unsat: 0.00s) +CPU Time : 206.288s + +Choices : 7569779 (Domain: 7569755) +Conflicts : 370015 (Analyzed: 370015) +Restarts : 1301 (Average: 284.41 Last: 289) +Model-Level : 1229.0 +Problems : 14 (Average Length: 32.00 Splits: 0) +Lemmas : 370015 (Deleted: 342379) + Binary : 3182 (Ratio: 0.86%) + Ternary : 2723 (Ratio: 0.74%) + Conflict : 370015 (Average Length: 1498.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 370015 (Average: 17.48 Max: 1535 Sum: 6469458) + Executed : 369908 (Average: 17.48 Max: 1535 Sum: 6466871 Ratio: 99.96%) + Bounded : 107 (Average: 24.18 Max: 32 Sum: 2587 Ratio: 0.04%) + +Rules : 222636 (Original: 222598) +Atoms : 6829 +Bodies : 147015 (Original: 146977) + Count : 629 (Original: 633) +Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207) +Tight : Yes +Variables : 103790 (Eliminated: 0 Frozen: 85188) +Constraints : 876970 (Binary: 97.7% Ternary: 1.0% Other: 1.3%) + +Memory Peak : 446MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 14.39s +Memory: 382MB (+0MB) +UNKNOWN +Iteration Time: 14.39s + +Iteration 14 +Queue: [(0,30,13,True)] +Grounded Until: 30 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 15 +Time : 219.254s (Solving: 215.23s 1st Model: 0.06s Unsat: 0.00s) +CPU Time : 219.252s + +Choices : 7902024 (Domain: 7902000) +Conflicts : 395821 (Analyzed: 395821) +Restarts : 1401 (Average: 282.53 Last: 289) +Model-Level : 1229.0 +Problems : 15 (Average Length: 32.00 Splits: 0) +Lemmas : 395821 (Deleted: 369254) + Binary : 3244 (Ratio: 0.82%) + Ternary : 2768 (Ratio: 0.70%) + Conflict : 395821 (Average Length: 1488.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 395821 (Average: 16.93 Max: 1535 Sum: 6702510) + Executed : 395712 (Average: 16.93 Max: 1535 Sum: 6699921 Ratio: 99.96%) + Bounded : 109 (Average: 23.75 Max: 32 Sum: 2589 Ratio: 0.04%) + +Rules : 222636 (Original: 222598) +Atoms : 6829 +Bodies : 147015 (Original: 146977) + Count : 629 (Original: 633) +Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207) +Tight : Yes +Variables : 103790 (Eliminated: 0 Frozen: 85188) +Constraints : 876970 (Binary: 97.7% Ternary: 1.0% Other: 1.3%) + +Memory Peak : 446MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 12.97s +Memory: 382MB (+0MB) +UNKNOWN +Iteration Time: 12.97s + +Iteration 15 +Queue: [(0,30,14,True)] +Grounded Until: 30 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 16 +Time : 232.422s (Solving: 228.36s 1st Model: 0.06s Unsat: 0.00s) +CPU Time : 232.424s + +Choices : 8195399 (Domain: 8195375) +Conflicts : 420846 (Analyzed: 420846) +Restarts : 1501 (Average: 280.38 Last: 289) +Model-Level : 1229.0 +Problems : 16 (Average Length: 32.00 Splits: 0) +Lemmas : 420846 (Deleted: 394454) + Binary : 3292 (Ratio: 0.78%) + Ternary : 2792 (Ratio: 0.66%) + Conflict : 420846 (Average Length: 1485.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 420846 (Average: 16.37 Max: 1535 Sum: 6888405) + Executed : 420737 (Average: 16.36 Max: 1535 Sum: 6885816 Ratio: 99.96%) + Bounded : 109 (Average: 23.75 Max: 32 Sum: 2589 Ratio: 0.04%) + +Rules : 222636 (Original: 222598) +Atoms : 6829 +Bodies : 147015 (Original: 146977) + Count : 629 (Original: 633) +Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207) +Tight : Yes +Variables : 103790 (Eliminated: 0 Frozen: 85188) +Constraints : 876970 (Binary: 97.7% Ternary: 1.0% Other: 1.3%) + +Memory Peak : 446MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 13.17s +Memory: 382MB (+0MB) +UNKNOWN +Iteration Time: 13.18s + +Iteration 16 +Queue: [(0,30,15,True)] +Grounded Until: 30 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 17 +Time : 246.630s (Solving: 242.55s 1st Model: 0.06s Unsat: 0.00s) +CPU Time : 246.636s + +Choices : 8500375 (Domain: 8500351) +Conflicts : 446423 (Analyzed: 446423) +Restarts : 1601 (Average: 278.84 Last: 289) +Model-Level : 1229.0 +Problems : 17 (Average Length: 32.00 Splits: 0) +Lemmas : 446423 (Deleted: 418980) + Binary : 3337 (Ratio: 0.75%) + Ternary : 2837 (Ratio: 0.64%) + Conflict : 446423 (Average Length: 1509.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 446423 (Average: 15.86 Max: 1535 Sum: 7080164) + Executed : 446313 (Average: 15.85 Max: 1535 Sum: 7077574 Ratio: 99.96%) + Bounded : 110 (Average: 23.55 Max: 32 Sum: 2590 Ratio: 0.04%) + +Rules : 222636 (Original: 222598) +Atoms : 6829 +Bodies : 147015 (Original: 146977) + Count : 629 (Original: 633) +Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207) +Tight : Yes +Variables : 103790 (Eliminated: 0 Frozen: 85188) +Constraints : 876970 (Binary: 97.7% Ternary: 1.0% Other: 1.3%) + +Memory Peak : 446MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 14.22s +Memory: 382MB (+0MB) +UNKNOWN +Iteration Time: 14.22s + +Iteration 17 +Queue: [(0,30,16,True)] +Grounded Until: 30 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 18 +Time : 259.925s (Solving: 255.81s 1st Model: 0.06s Unsat: 0.00s) +CPU Time : 259.936s + +Choices : 8829133 (Domain: 8829109) +Conflicts : 472161 (Analyzed: 472161) +Restarts : 1701 (Average: 277.58 Last: 289) +Model-Level : 1229.0 +Problems : 18 (Average Length: 32.00 Splits: 0) +Lemmas : 472161 (Deleted: 444020) + Binary : 3391 (Ratio: 0.72%) + Ternary : 2877 (Ratio: 0.61%) + Conflict : 472161 (Average Length: 1502.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 472161 (Average: 15.45 Max: 1535 Sum: 7292678) + Executed : 472050 (Average: 15.44 Max: 1535 Sum: 7290087 Ratio: 99.96%) + Bounded : 111 (Average: 23.34 Max: 32 Sum: 2591 Ratio: 0.04%) + +Rules : 222636 (Original: 222598) +Atoms : 6829 +Bodies : 147015 (Original: 146977) + Count : 629 (Original: 633) +Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207) +Tight : Yes +Variables : 103790 (Eliminated: 0 Frozen: 85188) +Constraints : 876970 (Binary: 97.7% Ternary: 1.0% Other: 1.3%) + +Memory Peak : 446MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 13.30s +Memory: 382MB (+0MB) +UNKNOWN +Iteration Time: 13.30s + +Iteration 18 +Queue: [(0,30,17,True)] +Grounded Until: 30 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 19 +Time : 273.349s (Solving: 269.21s 1st Model: 0.06s Unsat: 0.00s) +CPU Time : 273.368s + +Choices : 9152743 (Domain: 9152719) +Conflicts : 497627 (Analyzed: 497627) +Restarts : 1801 (Average: 276.31 Last: 289) +Model-Level : 1229.0 +Problems : 19 (Average Length: 32.00 Splits: 0) +Lemmas : 497627 (Deleted: 469531) + Binary : 3415 (Ratio: 0.69%) + Ternary : 2894 (Ratio: 0.58%) + Conflict : 497627 (Average Length: 1489.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 497627 (Average: 15.09 Max: 1535 Sum: 7506724) + Executed : 497515 (Average: 15.08 Max: 1535 Sum: 7504132 Ratio: 99.97%) + Bounded : 112 (Average: 23.14 Max: 32 Sum: 2592 Ratio: 0.03%) + +Rules : 222636 (Original: 222598) +Atoms : 6829 +Bodies : 147015 (Original: 146977) + Count : 629 (Original: 633) +Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207) +Tight : Yes +Variables : 103790 (Eliminated: 0 Frozen: 85188) +Constraints : 876970 (Binary: 97.7% Ternary: 1.0% Other: 1.3%) + +Memory Peak : 446MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 13.43s +Memory: 382MB (+0MB) +UNKNOWN +Iteration Time: 13.43s + +Iteration 19 +Queue: [(0,30,18,True)] +Grounded Until: 30 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 20 +Time : 286.647s (Solving: 282.48s 1st Model: 0.06s Unsat: 0.00s) +CPU Time : 286.676s + +Choices : 9477763 (Domain: 9477739) +Conflicts : 524550 (Analyzed: 524550) +Restarts : 1901 (Average: 275.93 Last: 289) +Model-Level : 1229.0 +Problems : 20 (Average Length: 32.00 Splits: 0) +Lemmas : 524550 (Deleted: 494282) + Binary : 3454 (Ratio: 0.66%) + Ternary : 2917 (Ratio: 0.56%) + Conflict : 524550 (Average Length: 1476.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 524550 (Average: 14.72 Max: 1535 Sum: 7719641) + Executed : 524437 (Average: 14.71 Max: 1535 Sum: 7717048 Ratio: 99.97%) + Bounded : 113 (Average: 22.95 Max: 32 Sum: 2593 Ratio: 0.03%) + +Rules : 222636 (Original: 222598) +Atoms : 6829 +Bodies : 147015 (Original: 146977) + Count : 629 (Original: 633) +Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207) +Tight : Yes +Variables : 103790 (Eliminated: 0 Frozen: 85188) +Constraints : 876970 (Binary: 97.7% Ternary: 1.0% Other: 1.3%) + +Memory Peak : 446MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 13.31s +Memory: 382MB (+0MB) +UNKNOWN +Iteration Time: 13.31s + +Iteration 20 +Queue: [(0,30,19,True)] +Grounded Until: 30 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 21 +Time : 301.954s (Solving: 297.74s 1st Model: 0.06s Unsat: 0.00s) +CPU Time : 301.988s + +Choices : 9819391 (Domain: 9819367) +Conflicts : 554951 (Analyzed: 554951) +Restarts : 2001 (Average: 277.34 Last: 289) +Model-Level : 1229.0 +Problems : 21 (Average Length: 32.00 Splits: 0) +Lemmas : 554951 (Deleted: 524093) + Binary : 3508 (Ratio: 0.63%) + Ternary : 2969 (Ratio: 0.54%) + Conflict : 554951 (Average Length: 1479.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 554951 (Average: 14.33 Max: 1535 Sum: 7950725) + Executed : 554836 (Average: 14.32 Max: 1535 Sum: 7948130 Ratio: 99.97%) + Bounded : 115 (Average: 22.57 Max: 32 Sum: 2595 Ratio: 0.03%) + +Rules : 222636 (Original: 222598) +Atoms : 6829 +Bodies : 147015 (Original: 146977) + Count : 629 (Original: 633) +Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207) +Tight : Yes +Variables : 103790 (Eliminated: 0 Frozen: 85188) +Constraints : 876970 (Binary: 97.7% Ternary: 1.0% Other: 1.3%) + +Memory Peak : 446MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 15.32s +Memory: 382MB (+0MB) +UNKNOWN +Iteration Time: 15.32s + +Iteration 21 +Queue: [(0,30,20,True)] +Grounded Until: 30 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 22 +Time : 315.880s (Solving: 311.64s 1st Model: 0.06s Unsat: 0.00s) +CPU Time : 315.920s + +Choices : 10139241 (Domain: 10139217) +Conflicts : 580052 (Analyzed: 580052) +Restarts : 2101 (Average: 276.08 Last: 289) +Model-Level : 1229.0 +Problems : 22 (Average Length: 32.00 Splits: 0) +Lemmas : 580052 (Deleted: 550660) + Binary : 3542 (Ratio: 0.61%) + Ternary : 2988 (Ratio: 0.52%) + Conflict : 580052 (Average Length: 1491.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 580052 (Average: 14.07 Max: 1535 Sum: 8158949) + Executed : 579937 (Average: 14.06 Max: 1535 Sum: 8156354 Ratio: 99.97%) + Bounded : 115 (Average: 22.57 Max: 32 Sum: 2595 Ratio: 0.03%) + +Rules : 222636 (Original: 222598) +Atoms : 6829 +Bodies : 147015 (Original: 146977) + Count : 629 (Original: 633) +Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207) +Tight : Yes +Variables : 103790 (Eliminated: 0 Frozen: 85188) +Constraints : 876970 (Binary: 97.7% Ternary: 1.0% Other: 1.3%) + +Memory Peak : 446MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 13.93s +Memory: 382MB (+0MB) +UNKNOWN +Iteration Time: 13.93s + +Iteration 22 +Queue: [(0,30,21,True)] +Grounded Until: 30 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 23 +Time : 329.775s (Solving: 325.51s 1st Model: 0.06s Unsat: 0.00s) +CPU Time : 329.820s + +Choices : 10447769 (Domain: 10447745) +Conflicts : 607007 (Analyzed: 607007) +Restarts : 2201 (Average: 275.79 Last: 289) +Model-Level : 1229.0 +Problems : 23 (Average Length: 32.00 Splits: 0) +Lemmas : 607007 (Deleted: 575354) + Binary : 3569 (Ratio: 0.59%) + Ternary : 3006 (Ratio: 0.50%) + Conflict : 607007 (Average Length: 1488.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 607007 (Average: 13.76 Max: 1535 Sum: 8355100) + Executed : 606892 (Average: 13.76 Max: 1535 Sum: 8352505 Ratio: 99.97%) + Bounded : 115 (Average: 22.57 Max: 32 Sum: 2595 Ratio: 0.03%) + +Rules : 222636 (Original: 222598) +Atoms : 6829 +Bodies : 147015 (Original: 146977) + Count : 629 (Original: 633) +Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207) +Tight : Yes +Variables : 103790 (Eliminated: 0 Frozen: 85188) +Constraints : 876970 (Binary: 97.7% Ternary: 1.0% Other: 1.3%) + +Memory Peak : 446MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 13.90s +Memory: 382MB (+0MB) +UNKNOWN +Iteration Time: 13.90s + +Iteration 23 +Queue: [(0,30,22,True)] +Grounded Until: 30 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 24 +Time : 344.692s (Solving: 340.39s 1st Model: 0.06s Unsat: 0.00s) +CPU Time : 344.744s + +Choices : 10768072 (Domain: 10768048) +Conflicts : 633821 (Analyzed: 633821) +Restarts : 2301 (Average: 275.45 Last: 289) +Model-Level : 1229.0 +Problems : 24 (Average Length: 32.00 Splits: 0) +Lemmas : 633821 (Deleted: 601851) + Binary : 3623 (Ratio: 0.57%) + Ternary : 3040 (Ratio: 0.48%) + Conflict : 633821 (Average Length: 1504.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 633821 (Average: 13.51 Max: 1535 Sum: 8563515) + Executed : 633705 (Average: 13.51 Max: 1535 Sum: 8560919 Ratio: 99.97%) + Bounded : 116 (Average: 22.38 Max: 32 Sum: 2596 Ratio: 0.03%) + +Rules : 222636 (Original: 222598) +Atoms : 6829 +Bodies : 147015 (Original: 146977) + Count : 629 (Original: 633) +Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207) +Tight : Yes +Variables : 103790 (Eliminated: 0 Frozen: 85188) +Constraints : 876970 (Binary: 97.7% Ternary: 1.0% Other: 1.3%) + +Memory Peak : 446MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 14.93s +Memory: 382MB (+0MB) +UNKNOWN +Iteration Time: 14.93s + +Iteration 24 +Queue: [(0,30,23,True)] +Grounded Until: 30 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 25 +Time : 360.194s (Solving: 355.85s 1st Model: 0.06s Unsat: 0.00s) +CPU Time : 360.252s + +Choices : 11105100 (Domain: 11105076) +Conflicts : 661550 (Analyzed: 661550) +Restarts : 2401 (Average: 275.53 Last: 289) +Model-Level : 1229.0 +Problems : 25 (Average Length: 32.00 Splits: 0) +Lemmas : 661550 (Deleted: 631137) + Binary : 3649 (Ratio: 0.55%) + Ternary : 3073 (Ratio: 0.46%) + Conflict : 661550 (Average Length: 1518.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 661550 (Average: 13.28 Max: 1535 Sum: 8786138) + Executed : 661434 (Average: 13.28 Max: 1535 Sum: 8783542 Ratio: 99.97%) + Bounded : 116 (Average: 22.38 Max: 32 Sum: 2596 Ratio: 0.03%) + +Rules : 222636 (Original: 222598) +Atoms : 6829 +Bodies : 147015 (Original: 146977) + Count : 629 (Original: 633) +Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207) +Tight : Yes +Variables : 103790 (Eliminated: 0 Frozen: 85188) +Constraints : 876970 (Binary: 97.7% Ternary: 1.0% Other: 1.3%) + +Memory Peak : 446MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 15.51s +Memory: 382MB (+0MB) +UNKNOWN +Iteration Time: 15.51s + +Iteration 25 +Queue: [(0,30,24,True)] +Grounded Until: 30 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 26 +Time : 375.078s (Solving: 370.70s 1st Model: 0.06s Unsat: 0.00s) +CPU Time : 375.144s + +Choices : 11447050 (Domain: 11447026) +Conflicts : 689902 (Analyzed: 689902) +Restarts : 2501 (Average: 275.85 Last: 289) +Model-Level : 1229.0 +Problems : 26 (Average Length: 32.00 Splits: 0) +Lemmas : 689902 (Deleted: 658486) + Binary : 3686 (Ratio: 0.53%) + Ternary : 3082 (Ratio: 0.45%) + Conflict : 689902 (Average Length: 1519.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 689902 (Average: 13.06 Max: 1535 Sum: 9010367) + Executed : 689783 (Average: 13.06 Max: 1535 Sum: 9007768 Ratio: 99.97%) + Bounded : 119 (Average: 21.84 Max: 32 Sum: 2599 Ratio: 0.03%) + +Rules : 222636 (Original: 222598) +Atoms : 6829 +Bodies : 147015 (Original: 146977) + Count : 629 (Original: 633) +Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207) +Tight : Yes +Variables : 103790 (Eliminated: 0 Frozen: 85188) +Constraints : 876970 (Binary: 97.7% Ternary: 1.0% Other: 1.3%) + +Memory Peak : 446MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 14.89s +Memory: 382MB (+0MB) +UNKNOWN +Iteration Time: 14.89s + +Iteration 26 +Queue: [(0,30,25,True)] +Grounded Until: 30 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 27 +Time : 391.008s (Solving: 386.60s 1st Model: 0.06s Unsat: 0.00s) +CPU Time : 391.080s + +Choices : 11768423 (Domain: 11768399) +Conflicts : 718070 (Analyzed: 718070) +Restarts : 2601 (Average: 276.07 Last: 289) +Model-Level : 1229.0 +Problems : 27 (Average Length: 32.00 Splits: 0) +Lemmas : 718070 (Deleted: 686479) + Binary : 3762 (Ratio: 0.52%) + Ternary : 3116 (Ratio: 0.43%) + Conflict : 718070 (Average Length: 1521.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 718070 (Average: 12.83 Max: 1535 Sum: 9209651) + Executed : 717951 (Average: 12.82 Max: 1535 Sum: 9207052 Ratio: 99.97%) + Bounded : 119 (Average: 21.84 Max: 32 Sum: 2599 Ratio: 0.03%) + +Rules : 222636 (Original: 222598) +Atoms : 6829 +Bodies : 147015 (Original: 146977) + Count : 629 (Original: 633) +Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207) +Tight : Yes +Variables : 103790 (Eliminated: 0 Frozen: 85188) +Constraints : 876970 (Binary: 97.7% Ternary: 1.0% Other: 1.3%) + +Memory Peak : 446MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 15.94s +Memory: 382MB (+0MB) +UNKNOWN +Iteration Time: 15.94s + +Iteration 27 +Queue: [(0,30,26,True)] +Grounded Until: 30 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 28 +Time : 405.208s (Solving: 400.78s 1st Model: 0.06s Unsat: 0.00s) +CPU Time : 405.284s + +Choices : 12074394 (Domain: 12074370) +Conflicts : 743180 (Analyzed: 743180) +Restarts : 2701 (Average: 275.15 Last: 289) +Model-Level : 1229.0 +Problems : 28 (Average Length: 32.00 Splits: 0) +Lemmas : 743180 (Deleted: 711475) + Binary : 3782 (Ratio: 0.51%) + Ternary : 3132 (Ratio: 0.42%) + Conflict : 743180 (Average Length: 1522.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 743180 (Average: 12.65 Max: 1535 Sum: 9399964) + Executed : 743061 (Average: 12.64 Max: 1535 Sum: 9397365 Ratio: 99.97%) + Bounded : 119 (Average: 21.84 Max: 32 Sum: 2599 Ratio: 0.03%) + +Rules : 222636 (Original: 222598) +Atoms : 6829 +Bodies : 147015 (Original: 146977) + Count : 629 (Original: 633) +Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207) +Tight : Yes +Variables : 103790 (Eliminated: 0 Frozen: 85188) +Constraints : 876970 (Binary: 97.7% Ternary: 1.0% Other: 1.3%) + +Memory Peak : 446MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 14.21s +Memory: 382MB (+0MB) +UNKNOWN +Iteration Time: 14.21s + +Iteration 28 +Queue: [(0,30,27,True)] +Grounded Until: 30 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 29 +Time : 420.958s (Solving: 416.51s 1st Model: 0.06s Unsat: 0.00s) +CPU Time : 421.040s + +Choices : 12372119 (Domain: 12372095) +Conflicts : 769686 (Analyzed: 769686) +Restarts : 2801 (Average: 274.79 Last: 289) +Model-Level : 1229.0 +Problems : 29 (Average Length: 32.00 Splits: 0) +Lemmas : 769686 (Deleted: 736713) + Binary : 3862 (Ratio: 0.50%) + Ternary : 3177 (Ratio: 0.41%) + Conflict : 769686 (Average Length: 1547.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 769686 (Average: 12.45 Max: 1535 Sum: 9579994) + Executed : 769566 (Average: 12.44 Max: 1535 Sum: 9577394 Ratio: 99.97%) + Bounded : 120 (Average: 21.67 Max: 32 Sum: 2600 Ratio: 0.03%) + +Rules : 222636 (Original: 222598) +Atoms : 6829 +Bodies : 147015 (Original: 146977) + Count : 629 (Original: 633) +Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207) +Tight : Yes +Variables : 103790 (Eliminated: 0 Frozen: 85188) +Constraints : 876970 (Binary: 97.7% Ternary: 1.0% Other: 1.3%) + +Memory Peak : 446MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 15.76s +Memory: 382MB (+0MB) +UNKNOWN +Iteration Time: 15.76s + +Iteration 29 +Queue: [(0,30,28,True)] +Grounded Until: 30 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 30 +Time : 436.217s (Solving: 431.73s 1st Model: 0.06s Unsat: 0.00s) +CPU Time : 436.308s + +Choices : 12745014 (Domain: 12744990) +Conflicts : 796882 (Analyzed: 796882) +Restarts : 2901 (Average: 274.69 Last: 289) +Model-Level : 1229.0 +Problems : 30 (Average Length: 32.00 Splits: 0) +Lemmas : 796882 (Deleted: 762166) + Binary : 3903 (Ratio: 0.49%) + Ternary : 3205 (Ratio: 0.40%) + Conflict : 796882 (Average Length: 1545.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 796882 (Average: 12.34 Max: 1535 Sum: 9831281) + Executed : 796762 (Average: 12.33 Max: 1535 Sum: 9828681 Ratio: 99.97%) + Bounded : 120 (Average: 21.67 Max: 32 Sum: 2600 Ratio: 0.03%) + +Rules : 222636 (Original: 222598) +Atoms : 6829 +Bodies : 147015 (Original: 146977) + Count : 629 (Original: 633) +Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207) +Tight : Yes +Variables : 103790 (Eliminated: 0 Frozen: 85188) +Constraints : 876970 (Binary: 97.7% Ternary: 1.0% Other: 1.3%) + +Memory Peak : 446MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 15.27s +Memory: 382MB (+0MB) +UNKNOWN +Iteration Time: 15.27s + +Iteration 30 +Queue: [(0,30,29,True)] +Grounded Until: 30 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 31 +Time : 449.609s (Solving: 445.08s 1st Model: 0.06s Unsat: 0.00s) +CPU Time : 449.704s + +Choices : 13072022 (Domain: 13071998) +Conflicts : 821837 (Analyzed: 821837) +Restarts : 3001 (Average: 273.85 Last: 289) +Model-Level : 1229.0 +Problems : 31 (Average Length: 32.00 Splits: 0) +Lemmas : 821837 (Deleted: 788956) + Binary : 3950 (Ratio: 0.48%) + Ternary : 3233 (Ratio: 0.39%) + Conflict : 821837 (Average Length: 1543.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 821837 (Average: 12.21 Max: 1535 Sum: 10036424) + Executed : 821717 (Average: 12.21 Max: 1535 Sum: 10033824 Ratio: 99.97%) + Bounded : 120 (Average: 21.67 Max: 32 Sum: 2600 Ratio: 0.03%) + +Rules : 222636 (Original: 222598) +Atoms : 6829 +Bodies : 147015 (Original: 146977) + Count : 629 (Original: 633) +Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207) +Tight : Yes +Variables : 103790 (Eliminated: 0 Frozen: 85188) +Constraints : 876970 (Binary: 97.7% Ternary: 1.0% Other: 1.3%) + +Memory Peak : 446MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 13.40s +Memory: 382MB (+0MB) +UNKNOWN +Iteration Time: 13.40s + +Iteration 31 +Queue: [(0,30,30,True)] +Grounded Until: 30 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 32 +Time : 464.982s (Solving: 460.42s 1st Model: 0.06s Unsat: 0.00s) +CPU Time : 465.084s + +Choices : 13384092 (Domain: 13384068) +Conflicts : 848075 (Analyzed: 848075) +Restarts : 3101 (Average: 273.48 Last: 289) +Model-Level : 1229.0 +Problems : 32 (Average Length: 32.00 Splits: 0) +Lemmas : 848075 (Deleted: 813488) + Binary : 4016 (Ratio: 0.47%) + Ternary : 3273 (Ratio: 0.39%) + Conflict : 848075 (Average Length: 1559.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 848075 (Average: 12.06 Max: 1535 Sum: 10229951) + Executed : 847954 (Average: 12.06 Max: 1535 Sum: 10227350 Ratio: 99.97%) + Bounded : 121 (Average: 21.50 Max: 32 Sum: 2601 Ratio: 0.03%) + +Rules : 222636 (Original: 222598) +Atoms : 6829 +Bodies : 147015 (Original: 146977) + Count : 629 (Original: 633) +Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207) +Tight : Yes +Variables : 103790 (Eliminated: 0 Frozen: 85188) +Constraints : 876970 (Binary: 97.7% Ternary: 1.0% Other: 1.3%) + +Memory Peak : 446MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 15.38s +Memory: 382MB (+0MB) +UNKNOWN +Iteration Time: 15.38s + +Iteration 32 +Queue: [(0,30,31,True)] +Grounded Until: 30 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 33 +Time : 480.647s (Solving: 476.06s 1st Model: 0.06s Unsat: 0.00s) +CPU Time : 480.756s + +Choices : 13708035 (Domain: 13708011) +Conflicts : 876603 (Analyzed: 876603) +Restarts : 3201 (Average: 273.85 Last: 289) +Model-Level : 1229.0 +Problems : 33 (Average Length: 32.00 Splits: 0) +Lemmas : 876603 (Deleted: 842286) + Binary : 4036 (Ratio: 0.46%) + Ternary : 3291 (Ratio: 0.38%) + Conflict : 876603 (Average Length: 1563.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 876603 (Average: 11.90 Max: 1535 Sum: 10433637) + Executed : 876480 (Average: 11.90 Max: 1535 Sum: 10431034 Ratio: 99.98%) + Bounded : 123 (Average: 21.16 Max: 32 Sum: 2603 Ratio: 0.02%) + +Rules : 222636 (Original: 222598) +Atoms : 6829 +Bodies : 147015 (Original: 146977) + Count : 629 (Original: 633) +Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207) +Tight : Yes +Variables : 103790 (Eliminated: 0 Frozen: 85188) +Constraints : 876970 (Binary: 97.7% Ternary: 1.0% Other: 1.3%) + +Memory Peak : 446MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 15.67s +Memory: 382MB (+0MB) +UNKNOWN +Iteration Time: 15.67s + +Iteration 33 +Queue: [(0,30,32,True)] +Grounded Until: 30 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 34 +Time : 494.767s (Solving: 490.15s 1st Model: 0.06s Unsat: 0.00s) +CPU Time : 494.884s + +Choices : 14036749 (Domain: 14036725) +Conflicts : 904023 (Analyzed: 904023) +Restarts : 3301 (Average: 273.86 Last: 289) +Model-Level : 1229.0 +Problems : 34 (Average Length: 32.00 Splits: 0) +Lemmas : 904023 (Deleted: 867598) + Binary : 4061 (Ratio: 0.45%) + Ternary : 3306 (Ratio: 0.37%) + Conflict : 904023 (Average Length: 1557.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 904023 (Average: 11.77 Max: 1535 Sum: 10641647) + Executed : 903899 (Average: 11.77 Max: 1535 Sum: 10639043 Ratio: 99.98%) + Bounded : 124 (Average: 21.00 Max: 32 Sum: 2604 Ratio: 0.02%) + +Rules : 222636 (Original: 222598) +Atoms : 6829 +Bodies : 147015 (Original: 146977) + Count : 629 (Original: 633) +Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207) +Tight : Yes +Variables : 103790 (Eliminated: 0 Frozen: 85188) +Constraints : 876970 (Binary: 97.7% Ternary: 1.0% Other: 1.3%) + +Memory Peak : 446MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 14.13s +Memory: 382MB (+0MB) +UNKNOWN +Iteration Time: 14.13s + +Iteration 34 +Queue: [(0,30,33,True)] +Grounded Until: 30 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 35 +Time : 509.227s (Solving: 504.56s 1st Model: 0.06s Unsat: 0.00s) +CPU Time : 509.348s + +Choices : 14361761 (Domain: 14361737) +Conflicts : 930324 (Analyzed: 930324) +Restarts : 3401 (Average: 273.54 Last: 289) +Model-Level : 1229.0 +Problems : 35 (Average Length: 32.00 Splits: 0) +Lemmas : 930324 (Deleted: 894704) + Binary : 4096 (Ratio: 0.44%) + Ternary : 3318 (Ratio: 0.36%) + Conflict : 930324 (Average Length: 1555.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 930324 (Average: 11.66 Max: 1535 Sum: 10848082) + Executed : 930199 (Average: 11.66 Max: 1535 Sum: 10845477 Ratio: 99.98%) + Bounded : 125 (Average: 20.84 Max: 32 Sum: 2605 Ratio: 0.02%) + +Rules : 222636 (Original: 222598) +Atoms : 6829 +Bodies : 147015 (Original: 146977) + Count : 629 (Original: 633) +Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207) +Tight : Yes +Variables : 103790 (Eliminated: 0 Frozen: 85188) +Constraints : 876970 (Binary: 97.7% Ternary: 1.0% Other: 1.3%) + +Memory Peak : 446MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 14.47s +Memory: 382MB (+0MB) +UNKNOWN +Iteration Time: 14.47s + +Iteration 35 +Queue: [(0,30,34,True)] +Grounded Until: 30 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 36 +Time : 523.957s (Solving: 519.26s 1st Model: 0.06s Unsat: 0.00s) +CPU Time : 524.084s + +Choices : 14665881 (Domain: 14665857) +Conflicts : 956807 (Analyzed: 956807) +Restarts : 3501 (Average: 273.30 Last: 289) +Model-Level : 1229.0 +Problems : 36 (Average Length: 32.00 Splits: 0) +Lemmas : 956807 (Deleted: 920700) + Binary : 4114 (Ratio: 0.43%) + Ternary : 3327 (Ratio: 0.35%) + Conflict : 956807 (Average Length: 1552.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 956807 (Average: 11.53 Max: 1535 Sum: 11034020) + Executed : 956680 (Average: 11.53 Max: 1535 Sum: 11031413 Ratio: 99.98%) + Bounded : 127 (Average: 20.53 Max: 32 Sum: 2607 Ratio: 0.02%) + +Rules : 222636 (Original: 222598) +Atoms : 6829 +Bodies : 147015 (Original: 146977) + Count : 629 (Original: 633) +Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207) +Tight : Yes +Variables : 103790 (Eliminated: 0 Frozen: 85188) +Constraints : 876970 (Binary: 97.7% Ternary: 1.0% Other: 1.3%) + +Memory Peak : 446MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 14.74s +Memory: 382MB (+0MB) +UNKNOWN +Iteration Time: 14.74s + +Iteration 36 +Queue: [(0,30,35,True)] +Grounded Until: 30 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 37 +Time : 537.897s (Solving: 533.17s 1st Model: 0.06s Unsat: 0.00s) +CPU Time : 538.028s + +Choices : 14979466 (Domain: 14979442) +Conflicts : 984516 (Analyzed: 984516) +Restarts : 3601 (Average: 273.40 Last: 289) +Model-Level : 1229.0 +Problems : 37 (Average Length: 32.00 Splits: 0) +Lemmas : 984516 (Deleted: 949797) + Binary : 4132 (Ratio: 0.42%) + Ternary : 3338 (Ratio: 0.34%) + Conflict : 984516 (Average Length: 1542.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 984516 (Average: 11.40 Max: 1535 Sum: 11225450) + Executed : 984388 (Average: 11.40 Max: 1535 Sum: 11222811 Ratio: 99.98%) + Bounded : 128 (Average: 20.62 Max: 32 Sum: 2639 Ratio: 0.02%) + +Rules : 222636 (Original: 222598) +Atoms : 6829 +Bodies : 147015 (Original: 146977) + Count : 629 (Original: 633) +Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207) +Tight : Yes +Variables : 103790 (Eliminated: 0 Frozen: 85188) +Constraints : 876970 (Binary: 97.7% Ternary: 1.0% Other: 1.3%) + +Memory Peak : 446MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 13.95s +Memory: 382MB (+0MB) +UNKNOWN +Iteration Time: 13.95s + +Iteration 37 +Queue: [(0,30,36,True)] +Grounded Until: 30 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 38 +Time : 553.847s (Solving: 549.09s 1st Model: 0.06s Unsat: 0.00s) +CPU Time : 553.984s + +Choices : 15291010 (Domain: 15290986) +Conflicts : 1014439 (Analyzed: 1014439) +Restarts : 3701 (Average: 274.10 Last: 289) +Model-Level : 1229.0 +Problems : 38 (Average Length: 32.00 Splits: 0) +Lemmas : 1014439 (Deleted: 977194) + Binary : 4165 (Ratio: 0.41%) + Ternary : 3351 (Ratio: 0.33%) + Conflict : 1014439 (Average Length: 1548.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 1014439 (Average: 11.26 Max: 1535 Sum: 11419058) + Executed : 1014308 (Average: 11.25 Max: 1535 Sum: 11416385 Ratio: 99.98%) + Bounded : 131 (Average: 20.40 Max: 32 Sum: 2673 Ratio: 0.02%) + +Rules : 222636 (Original: 222598) +Atoms : 6829 +Bodies : 147015 (Original: 146977) + Count : 629 (Original: 633) +Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207) +Tight : Yes +Variables : 103790 (Eliminated: 0 Frozen: 85188) +Constraints : 876958 (Binary: 97.7% Ternary: 1.0% Other: 1.3%) + +Memory Peak : 446MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 15.96s +Memory: 382MB (+0MB) +UNKNOWN +Iteration Time: 15.96s + +Iteration 38 +Queue: [(0,30,37,True)] +Grounded Until: 30 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 39 +Time : 568.027s (Solving: 563.23s 1st Model: 0.06s Unsat: 0.00s) +CPU Time : 568.168s + +Choices : 15577118 (Domain: 15577094) +Conflicts : 1040686 (Analyzed: 1040686) +Restarts : 3801 (Average: 273.79 Last: 289) +Model-Level : 1229.0 +Problems : 39 (Average Length: 32.00 Splits: 0) +Lemmas : 1040686 (Deleted: 1003935) + Binary : 4194 (Ratio: 0.40%) + Ternary : 3363 (Ratio: 0.32%) + Conflict : 1040686 (Average Length: 1548.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 1040686 (Average: 11.14 Max: 1535 Sum: 11593785) + Executed : 1040554 (Average: 11.14 Max: 1535 Sum: 11591111 Ratio: 99.98%) + Bounded : 132 (Average: 20.26 Max: 32 Sum: 2674 Ratio: 0.02%) + +Rules : 222636 (Original: 222598) +Atoms : 6829 +Bodies : 147015 (Original: 146977) + Count : 629 (Original: 633) +Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207) +Tight : Yes +Variables : 103790 (Eliminated: 0 Frozen: 85188) +Constraints : 876946 (Binary: 97.7% Ternary: 1.0% Other: 1.3%) + +Memory Peak : 446MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 14.19s +Memory: 382MB (+0MB) +UNKNOWN +Iteration Time: 14.19s + +Iteration 39 +Queue: [(0,30,38,True)] +Grounded Until: 30 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 40 +Time : 582.016s (Solving: 577.20s 1st Model: 0.06s Unsat: 0.00s) +CPU Time : 582.164s + +Choices : 15879418 (Domain: 15879394) +Conflicts : 1065048 (Analyzed: 1065048) +Restarts : 3901 (Average: 273.02 Last: 289) +Model-Level : 1229.0 +Problems : 40 (Average Length: 32.00 Splits: 0) +Lemmas : 1065048 (Deleted: 1027091) + Binary : 4223 (Ratio: 0.40%) + Ternary : 3384 (Ratio: 0.32%) + Conflict : 1065048 (Average Length: 1549.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 1065048 (Average: 11.08 Max: 1535 Sum: 11802952) + Executed : 1064916 (Average: 11.08 Max: 1535 Sum: 11800278 Ratio: 99.98%) + Bounded : 132 (Average: 20.26 Max: 32 Sum: 2674 Ratio: 0.02%) + +Rules : 222636 (Original: 222598) +Atoms : 6829 +Bodies : 147015 (Original: 146977) + Count : 629 (Original: 633) +Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207) +Tight : Yes +Variables : 103790 (Eliminated: 0 Frozen: 85188) +Constraints : 876946 (Binary: 97.7% Ternary: 1.0% Other: 1.3%) + +Memory Peak : 446MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 14.00s +Memory: 382MB (+0MB) +UNKNOWN +Iteration Time: 14.00s + +Iteration 40 +Queue: [(0,30,39,True)] +Grounded Until: 30 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 41 +Time : 596.192s (Solving: 591.34s 1st Model: 0.06s Unsat: 0.00s) +CPU Time : 596.348s + +Choices : 16207654 (Domain: 16207630) +Conflicts : 1089862 (Analyzed: 1089862) +Restarts : 4001 (Average: 272.40 Last: 289) +Model-Level : 1229.0 +Problems : 41 (Average Length: 32.00 Splits: 0) +Lemmas : 1089862 (Deleted: 1053980) + Binary : 4260 (Ratio: 0.39%) + Ternary : 3410 (Ratio: 0.31%) + Conflict : 1089862 (Average Length: 1550.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 1089862 (Average: 11.04 Max: 1535 Sum: 12033198) + Executed : 1089730 (Average: 11.04 Max: 1535 Sum: 12030524 Ratio: 99.98%) + Bounded : 132 (Average: 20.26 Max: 32 Sum: 2674 Ratio: 0.02%) + +Rules : 222636 (Original: 222598) +Atoms : 6829 +Bodies : 147015 (Original: 146977) + Count : 629 (Original: 633) +Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207) +Tight : Yes +Variables : 103790 (Eliminated: 0 Frozen: 85188) +Constraints : 876946 (Binary: 97.7% Ternary: 1.0% Other: 1.3%) + +Memory Peak : 446MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 14.18s +Memory: 382MB (+0MB) +UNKNOWN +Iteration Time: 14.18s + +Iteration 41 +Queue: [(0,30,40,True)] +Grounded Until: 30 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 42 +Time : 610.113s (Solving: 605.24s 1st Model: 0.06s Unsat: 0.00s) +CPU Time : 610.276s + +Choices : 16541036 (Domain: 16541012) +Conflicts : 1116124 (Analyzed: 1116124) +Restarts : 4101 (Average: 272.16 Last: 289) +Model-Level : 1229.0 +Problems : 42 (Average Length: 32.00 Splits: 0) +Lemmas : 1116124 (Deleted: 1078393) + Binary : 4307 (Ratio: 0.39%) + Ternary : 3445 (Ratio: 0.31%) + Conflict : 1116124 (Average Length: 1550.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 1116124 (Average: 10.99 Max: 1535 Sum: 12263768) + Executed : 1115992 (Average: 10.99 Max: 1535 Sum: 12261094 Ratio: 99.98%) + Bounded : 132 (Average: 20.26 Max: 32 Sum: 2674 Ratio: 0.02%) + +Rules : 222636 (Original: 222598) +Atoms : 6829 +Bodies : 147015 (Original: 146977) + Count : 629 (Original: 633) +Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207) +Tight : Yes +Variables : 103790 (Eliminated: 0 Frozen: 85188) +Constraints : 876946 (Binary: 97.7% Ternary: 1.0% Other: 1.3%) + +Memory Peak : 446MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 13.93s +Memory: 382MB (+0MB) +UNKNOWN +Iteration Time: 13.93s + +Iteration 42 +Queue: [(0,30,41,True)] +Grounded Until: 30 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 43 +Time : 624.032s (Solving: 619.12s 1st Model: 0.06s Unsat: 0.00s) +CPU Time : 624.200s + +Choices : 16887218 (Domain: 16887194) +Conflicts : 1142136 (Analyzed: 1142136) +Restarts : 4201 (Average: 271.87 Last: 289) +Model-Level : 1229.0 +Problems : 43 (Average Length: 32.00 Splits: 0) +Lemmas : 1142136 (Deleted: 1104338) + Binary : 4326 (Ratio: 0.38%) + Ternary : 3467 (Ratio: 0.30%) + Conflict : 1142136 (Average Length: 1546.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 1142136 (Average: 10.95 Max: 1535 Sum: 12509555) + Executed : 1142004 (Average: 10.95 Max: 1535 Sum: 12506881 Ratio: 99.98%) + Bounded : 132 (Average: 20.26 Max: 32 Sum: 2674 Ratio: 0.02%) + +Rules : 222636 (Original: 222598) +Atoms : 6829 +Bodies : 147015 (Original: 146977) + Count : 629 (Original: 633) +Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207) +Tight : Yes +Variables : 103790 (Eliminated: 0 Frozen: 85188) +Constraints : 876946 (Binary: 97.7% Ternary: 1.0% Other: 1.3%) + +Memory Peak : 446MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 13.93s +Memory: 382MB (+0MB) +UNKNOWN +Iteration Time: 13.93s + +Iteration 43 +Queue: [(0,30,42,True)] +Grounded Until: 30 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 44 +Time : 638.509s (Solving: 633.57s 1st Model: 0.06s Unsat: 0.00s) +CPU Time : 638.684s + +Choices : 17268384 (Domain: 17268360) +Conflicts : 1166754 (Analyzed: 1166754) +Restarts : 4301 (Average: 271.28 Last: 289) +Model-Level : 1229.0 +Problems : 44 (Average Length: 32.00 Splits: 0) +Lemmas : 1166754 (Deleted: 1130124) + Binary : 4345 (Ratio: 0.37%) + Ternary : 3481 (Ratio: 0.30%) + Conflict : 1166754 (Average Length: 1545.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 1166754 (Average: 10.96 Max: 1535 Sum: 12792440) + Executed : 1166621 (Average: 10.96 Max: 1535 Sum: 12789765 Ratio: 99.98%) + Bounded : 133 (Average: 20.11 Max: 32 Sum: 2675 Ratio: 0.02%) + +Rules : 222636 (Original: 222598) +Atoms : 6829 +Bodies : 147015 (Original: 146977) + Count : 629 (Original: 633) +Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207) +Tight : Yes +Variables : 103790 (Eliminated: 0 Frozen: 85188) +Constraints : 876946 (Binary: 97.7% Ternary: 1.0% Other: 1.3%) + +Memory Peak : 446MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 14.48s +Memory: 382MB (+0MB) +UNKNOWN +Iteration Time: 14.48s + +Iteration 44 +Queue: [(0,30,43,True)] +Grounded Until: 30 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 45 +Time : 654.183s (Solving: 649.20s 1st Model: 0.06s Unsat: 0.00s) +CPU Time : 654.364s + +Choices : 17574339 (Domain: 17574315) +Conflicts : 1194093 (Analyzed: 1194093) +Restarts : 4401 (Average: 271.32 Last: 289) +Model-Level : 1229.0 +Problems : 45 (Average Length: 32.00 Splits: 0) +Lemmas : 1194093 (Deleted: 1154414) + Binary : 4394 (Ratio: 0.37%) + Ternary : 3527 (Ratio: 0.30%) + Conflict : 1194093 (Average Length: 1549.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 1194093 (Average: 10.89 Max: 1535 Sum: 13002423) + Executed : 1193960 (Average: 10.89 Max: 1535 Sum: 12999748 Ratio: 99.98%) + Bounded : 133 (Average: 20.11 Max: 32 Sum: 2675 Ratio: 0.02%) + +Rules : 222636 (Original: 222598) +Atoms : 6829 +Bodies : 147015 (Original: 146977) + Count : 629 (Original: 633) +Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207) +Tight : Yes +Variables : 103790 (Eliminated: 0 Frozen: 85188) +Constraints : 876946 (Binary: 97.7% Ternary: 1.0% Other: 1.3%) + +Memory Peak : 446MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 15.68s +Memory: 382MB (+0MB) +UNKNOWN +Iteration Time: 15.68s + +Iteration 45 +Queue: [(0,30,44,True)] +Grounded Until: 30 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 46 +Time : 668.361s (Solving: 663.34s 1st Model: 0.06s Unsat: 0.00s) +CPU Time : 668.548s + +Choices : 17873188 (Domain: 17873164) +Conflicts : 1218783 (Analyzed: 1218783) +Restarts : 4501 (Average: 270.78 Last: 289) +Model-Level : 1229.0 +Problems : 46 (Average Length: 32.00 Splits: 0) +Lemmas : 1218783 (Deleted: 1181472) + Binary : 4416 (Ratio: 0.36%) + Ternary : 3555 (Ratio: 0.29%) + Conflict : 1218783 (Average Length: 1546.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 1218783 (Average: 10.84 Max: 1535 Sum: 13206694) + Executed : 1218649 (Average: 10.83 Max: 1535 Sum: 13203987 Ratio: 99.98%) + Bounded : 134 (Average: 20.20 Max: 32 Sum: 2707 Ratio: 0.02%) + +Rules : 222636 (Original: 222598) +Atoms : 6829 +Bodies : 147015 (Original: 146977) + Count : 629 (Original: 633) +Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207) +Tight : Yes +Variables : 103790 (Eliminated: 0 Frozen: 85188) +Constraints : 876946 (Binary: 97.7% Ternary: 1.0% Other: 1.3%) + +Memory Peak : 446MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 14.19s +Memory: 382MB (+0MB) +UNKNOWN +Iteration Time: 14.19s + +Iteration 46 +Queue: [(0,30,45,True)] +Grounded Until: 30 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 47 +Time : 681.735s (Solving: 676.69s 1st Model: 0.06s Unsat: 0.00s) +CPU Time : 681.928s + +Choices : 18161588 (Domain: 18161564) +Conflicts : 1243661 (Analyzed: 1243661) +Restarts : 4601 (Average: 270.30 Last: 289) +Model-Level : 1229.0 +Problems : 47 (Average Length: 32.00 Splits: 0) +Lemmas : 1243661 (Deleted: 1205793) + Binary : 4446 (Ratio: 0.36%) + Ternary : 3569 (Ratio: 0.29%) + Conflict : 1243661 (Average Length: 1542.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 1243661 (Average: 10.77 Max: 1535 Sum: 13391413) + Executed : 1243526 (Average: 10.77 Max: 1535 Sum: 13388705 Ratio: 99.98%) + Bounded : 135 (Average: 20.06 Max: 32 Sum: 2708 Ratio: 0.02%) + +Rules : 222636 (Original: 222598) +Atoms : 6829 +Bodies : 147015 (Original: 146977) + Count : 629 (Original: 633) +Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207) +Tight : Yes +Variables : 103790 (Eliminated: 0 Frozen: 85188) +Constraints : 876934 (Binary: 97.7% Ternary: 1.0% Other: 1.3%) + +Memory Peak : 446MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 13.38s +Memory: 382MB (+0MB) +UNKNOWN +Iteration Time: 13.38s + +Iteration 47 +Queue: [(0,30,46,True)] +Grounded Until: 30 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 48 +Time : 696.387s (Solving: 691.30s 1st Model: 0.06s Unsat: 0.00s) +CPU Time : 696.588s + +Choices : 18462804 (Domain: 18462780) +Conflicts : 1269171 (Analyzed: 1269171) +Restarts : 4701 (Average: 269.98 Last: 289) +Model-Level : 1229.0 +Problems : 48 (Average Length: 32.00 Splits: 0) +Lemmas : 1269171 (Deleted: 1230466) + Binary : 4478 (Ratio: 0.35%) + Ternary : 3592 (Ratio: 0.28%) + Conflict : 1269171 (Average Length: 1547.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 1269171 (Average: 10.70 Max: 1535 Sum: 13585959) + Executed : 1269035 (Average: 10.70 Max: 1535 Sum: 13583219 Ratio: 99.98%) + Bounded : 136 (Average: 20.15 Max: 32 Sum: 2740 Ratio: 0.02%) + +Rules : 222636 (Original: 222598) +Atoms : 6829 +Bodies : 147015 (Original: 146977) + Count : 629 (Original: 633) +Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207) +Tight : Yes +Variables : 103790 (Eliminated: 0 Frozen: 85188) +Constraints : 876934 (Binary: 97.7% Ternary: 1.0% Other: 1.3%) + +Memory Peak : 446MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 14.66s +Memory: 382MB (+0MB) +UNKNOWN +Iteration Time: 14.66s + +Iteration 48 +Queue: [(0,30,47,True)] +Grounded Until: 30 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 49 +Time : 710.676s (Solving: 705.56s 1st Model: 0.06s Unsat: 0.00s) +CPU Time : 710.884s + +Choices : 18757681 (Domain: 18757657) +Conflicts : 1295037 (Analyzed: 1295037) +Restarts : 4801 (Average: 269.74 Last: 289) +Model-Level : 1229.0 +Problems : 49 (Average Length: 32.00 Splits: 0) +Lemmas : 1295037 (Deleted: 1255761) + Binary : 4498 (Ratio: 0.35%) + Ternary : 3597 (Ratio: 0.28%) + Conflict : 1295037 (Average Length: 1541.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 1295037 (Average: 10.65 Max: 1535 Sum: 13785693) + Executed : 1294900 (Average: 10.64 Max: 1535 Sum: 13782952 Ratio: 99.98%) + Bounded : 137 (Average: 20.01 Max: 32 Sum: 2741 Ratio: 0.02%) + +Rules : 222636 (Original: 222598) +Atoms : 6829 +Bodies : 147015 (Original: 146977) + Count : 629 (Original: 633) +Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207) +Tight : Yes +Variables : 103790 (Eliminated: 0 Frozen: 85188) +Constraints : 876922 (Binary: 97.7% Ternary: 1.0% Other: 1.3%) + +Memory Peak : 446MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 14.30s +Memory: 382MB (+0MB) +UNKNOWN +Iteration Time: 14.30s + +Iteration 49 +Queue: [(0,30,48,True)] +Grounded Until: 30 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 50 +Time : 724.048s (Solving: 718.91s 1st Model: 0.06s Unsat: 0.00s) +CPU Time : 724.260s + +Choices : 19087757 (Domain: 19087733) +Conflicts : 1320354 (Analyzed: 1320354) +Restarts : 4901 (Average: 269.41 Last: 289) +Model-Level : 1229.0 +Problems : 50 (Average Length: 32.00 Splits: 0) +Lemmas : 1320354 (Deleted: 1281163) + Binary : 4529 (Ratio: 0.34%) + Ternary : 3621 (Ratio: 0.27%) + Conflict : 1320354 (Average Length: 1534.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 1320354 (Average: 10.61 Max: 1535 Sum: 14015035) + Executed : 1320217 (Average: 10.61 Max: 1535 Sum: 14012294 Ratio: 99.98%) + Bounded : 137 (Average: 20.01 Max: 32 Sum: 2741 Ratio: 0.02%) + +Rules : 222636 (Original: 222598) +Atoms : 6829 +Bodies : 147015 (Original: 146977) + Count : 629 (Original: 633) +Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207) +Tight : Yes +Variables : 103790 (Eliminated: 0 Frozen: 85188) +Constraints : 876922 (Binary: 97.7% Ternary: 1.0% Other: 1.3%) + +Memory Peak : 446MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 13.38s +Memory: 382MB (+0MB) +UNKNOWN +Iteration Time: 13.38s + +Iteration 50 +Queue: [(0,30,49,True)] +Grounded Until: 30 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 51 +Time : 736.820s (Solving: 731.65s 1st Model: 0.06s Unsat: 0.00s) +CPU Time : 737.036s + +Choices : 19402130 (Domain: 19402106) +Conflicts : 1343463 (Analyzed: 1343463) +Restarts : 5001 (Average: 268.64 Last: 289) +Model-Level : 1229.0 +Problems : 51 (Average Length: 32.00 Splits: 0) +Lemmas : 1343463 (Deleted: 1303436) + Binary : 4556 (Ratio: 0.34%) + Ternary : 3639 (Ratio: 0.27%) + Conflict : 1343463 (Average Length: 1531.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 1343463 (Average: 10.59 Max: 1535 Sum: 14224897) + Executed : 1343326 (Average: 10.59 Max: 1535 Sum: 14222156 Ratio: 99.98%) + Bounded : 137 (Average: 20.01 Max: 32 Sum: 2741 Ratio: 0.02%) + +Rules : 222636 (Original: 222598) +Atoms : 6829 +Bodies : 147015 (Original: 146977) + Count : 629 (Original: 633) +Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207) +Tight : Yes +Variables : 103790 (Eliminated: 0 Frozen: 85188) +Constraints : 876922 (Binary: 97.7% Ternary: 1.0% Other: 1.3%) + +Memory Peak : 446MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 12.78s +Memory: 382MB (+0MB) +UNKNOWN +Iteration Time: 12.78s + +Iteration 51 +Queue: [(0,30,50,True)] +Grounded Until: 30 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 52 +Time : 751.174s (Solving: 745.97s 1st Model: 0.06s Unsat: 0.00s) +CPU Time : 751.396s + +Choices : 19726312 (Domain: 19726288) +Conflicts : 1368998 (Analyzed: 1368998) +Restarts : 5101 (Average: 268.38 Last: 289) +Model-Level : 1229.0 +Problems : 52 (Average Length: 32.00 Splits: 0) +Lemmas : 1368998 (Deleted: 1329013) + Binary : 4579 (Ratio: 0.33%) + Ternary : 3652 (Ratio: 0.27%) + Conflict : 1368998 (Average Length: 1532.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 1368998 (Average: 10.55 Max: 1535 Sum: 14446001) + Executed : 1368861 (Average: 10.55 Max: 1535 Sum: 14443260 Ratio: 99.98%) + Bounded : 137 (Average: 20.01 Max: 32 Sum: 2741 Ratio: 0.02%) + +Rules : 222636 (Original: 222598) +Atoms : 6829 +Bodies : 147015 (Original: 146977) + Count : 629 (Original: 633) +Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207) +Tight : Yes +Variables : 103790 (Eliminated: 0 Frozen: 85188) +Constraints : 876922 (Binary: 97.7% Ternary: 1.0% Other: 1.3%) + +Memory Peak : 446MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 14.36s +Memory: 382MB (+0MB) +UNKNOWN +Iteration Time: 14.36s + +Iteration 52 +Queue: [(0,30,51,True)] +Grounded Until: 30 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 53 +Time : 765.500s (Solving: 760.25s 1st Model: 0.06s Unsat: 0.00s) +CPU Time : 765.728s + +Choices : 20091443 (Domain: 20091419) +Conflicts : 1395186 (Analyzed: 1395186) +Restarts : 5201 (Average: 268.25 Last: 289) +Model-Level : 1229.0 +Problems : 53 (Average Length: 32.00 Splits: 0) +Lemmas : 1395186 (Deleted: 1354356) + Binary : 4597 (Ratio: 0.33%) + Ternary : 3662 (Ratio: 0.26%) + Conflict : 1395186 (Average Length: 1525.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 1395186 (Average: 10.54 Max: 1535 Sum: 14710018) + Executed : 1395049 (Average: 10.54 Max: 1535 Sum: 14707277 Ratio: 99.98%) + Bounded : 137 (Average: 20.01 Max: 32 Sum: 2741 Ratio: 0.02%) + +Rules : 222636 (Original: 222598) +Atoms : 6829 +Bodies : 147015 (Original: 146977) + Count : 629 (Original: 633) +Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207) +Tight : Yes +Variables : 103790 (Eliminated: 0 Frozen: 85188) +Constraints : 876922 (Binary: 97.7% Ternary: 1.0% Other: 1.3%) + +Memory Peak : 446MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 14.33s +Memory: 382MB (+0MB) +UNKNOWN +Iteration Time: 14.33s + +Iteration 53 +Queue: [(0,30,52,True)] +Grounded Until: 30 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 54 +Time : 778.559s (Solving: 773.28s 1st Model: 0.06s Unsat: 0.00s) +CPU Time : 778.792s + +Choices : 20410556 (Domain: 20410532) +Conflicts : 1418624 (Analyzed: 1418624) +Restarts : 5301 (Average: 267.61 Last: 289) +Model-Level : 1229.0 +Problems : 54 (Average Length: 32.00 Splits: 0) +Lemmas : 1418624 (Deleted: 1377514) + Binary : 4602 (Ratio: 0.32%) + Ternary : 3663 (Ratio: 0.26%) + Conflict : 1418624 (Average Length: 1519.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 1418624 (Average: 10.52 Max: 1535 Sum: 14927946) + Executed : 1418487 (Average: 10.52 Max: 1535 Sum: 14925205 Ratio: 99.98%) + Bounded : 137 (Average: 20.01 Max: 32 Sum: 2741 Ratio: 0.02%) + +Rules : 222636 (Original: 222598) +Atoms : 6829 +Bodies : 147015 (Original: 146977) + Count : 629 (Original: 633) +Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207) +Tight : Yes +Variables : 103790 (Eliminated: 0 Frozen: 85188) +Constraints : 876922 (Binary: 97.7% Ternary: 1.0% Other: 1.3%) + +Memory Peak : 446MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 13.07s +Memory: 382MB (+0MB) +UNKNOWN +Iteration Time: 13.07s + +Iteration 54 +Queue: [(0,30,53,True)] +Grounded Until: 30 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 55 +Time : 793.323s (Solving: 788.01s 1st Model: 0.06s Unsat: 0.00s) +CPU Time : 793.564s + +Choices : 20718909 (Domain: 20718885) +Conflicts : 1444592 (Analyzed: 1444592) +Restarts : 5401 (Average: 267.47 Last: 289) +Model-Level : 1229.0 +Problems : 55 (Average Length: 32.00 Splits: 0) +Lemmas : 1444592 (Deleted: 1403553) + Binary : 4611 (Ratio: 0.32%) + Ternary : 3670 (Ratio: 0.25%) + Conflict : 1444592 (Average Length: 1515.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 1444592 (Average: 10.47 Max: 1535 Sum: 15131324) + Executed : 1444454 (Average: 10.47 Max: 1535 Sum: 15128551 Ratio: 99.98%) + Bounded : 138 (Average: 20.09 Max: 32 Sum: 2773 Ratio: 0.02%) + +Rules : 222636 (Original: 222598) +Atoms : 6829 +Bodies : 147015 (Original: 146977) + Count : 629 (Original: 633) +Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207) +Tight : Yes +Variables : 103790 (Eliminated: 0 Frozen: 85188) +Constraints : 876922 (Binary: 97.7% Ternary: 1.0% Other: 1.3%) + +Memory Peak : 446MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 14.77s +Memory: 382MB (+0MB) +UNKNOWN +Iteration Time: 14.77s + +Iteration 55 +Queue: [(0,30,54,True)] +Grounded Until: 30 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 56 +Time : 807.526s (Solving: 802.19s 1st Model: 0.06s Unsat: 0.00s) +CPU Time : 807.776s + +Choices : 21012255 (Domain: 21012231) +Conflicts : 1470925 (Analyzed: 1470925) +Restarts : 5501 (Average: 267.39 Last: 289) +Model-Level : 1229.0 +Problems : 56 (Average Length: 32.00 Splits: 0) +Lemmas : 1470925 (Deleted: 1429221) + Binary : 4658 (Ratio: 0.32%) + Ternary : 3684 (Ratio: 0.25%) + Conflict : 1470925 (Average Length: 1519.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 1470925 (Average: 10.42 Max: 1535 Sum: 15324542) + Executed : 1470787 (Average: 10.42 Max: 1535 Sum: 15321769 Ratio: 99.98%) + Bounded : 138 (Average: 20.09 Max: 32 Sum: 2773 Ratio: 0.02%) + +Rules : 222636 (Original: 222598) +Atoms : 6829 +Bodies : 147015 (Original: 146977) + Count : 629 (Original: 633) +Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207) +Tight : Yes +Variables : 103790 (Eliminated: 0 Frozen: 85188) +Constraints : 876910 (Binary: 97.7% Ternary: 1.0% Other: 1.3%) + +Memory Peak : 446MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 14.21s +Memory: 382MB (+0MB) +UNKNOWN +Iteration Time: 14.21s + +Iteration 56 +Queue: [(0,30,55,True)] +Grounded Until: 30 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 57 +Time : 821.013s (Solving: 815.64s 1st Model: 0.06s Unsat: 0.00s) +CPU Time : 821.268s + +Choices : 21318347 (Domain: 21318323) +Conflicts : 1496657 (Analyzed: 1496657) +Restarts : 5601 (Average: 267.21 Last: 289) +Model-Level : 1229.0 +Problems : 57 (Average Length: 32.00 Splits: 0) +Lemmas : 1496657 (Deleted: 1455347) + Binary : 4671 (Ratio: 0.31%) + Ternary : 3691 (Ratio: 0.25%) + Conflict : 1496657 (Average Length: 1516.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 1496657 (Average: 10.38 Max: 1535 Sum: 15529417) + Executed : 1496518 (Average: 10.37 Max: 1535 Sum: 15526643 Ratio: 99.98%) + Bounded : 139 (Average: 19.96 Max: 32 Sum: 2774 Ratio: 0.02%) + +Rules : 222636 (Original: 222598) +Atoms : 6829 +Bodies : 147015 (Original: 146977) + Count : 629 (Original: 633) +Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207) +Tight : Yes +Variables : 103790 (Eliminated: 0 Frozen: 85188) +Constraints : 876910 (Binary: 97.7% Ternary: 1.0% Other: 1.3%) + +Memory Peak : 446MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 13.50s +Memory: 382MB (+0MB) +UNKNOWN +Iteration Time: 13.50s + +Iteration 57 +Queue: [(0,30,56,True)] +Grounded Until: 30 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 58 +Time : 834.893s (Solving: 829.48s 1st Model: 0.06s Unsat: 0.00s) +CPU Time : 835.152s + +Choices : 21631508 (Domain: 21631484) +Conflicts : 1520661 (Analyzed: 1520661) +Restarts : 5701 (Average: 266.74 Last: 289) +Model-Level : 1229.0 +Problems : 58 (Average Length: 32.00 Splits: 0) +Lemmas : 1520661 (Deleted: 1478049) + Binary : 4684 (Ratio: 0.31%) + Ternary : 3706 (Ratio: 0.24%) + Conflict : 1520661 (Average Length: 1516.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 1520661 (Average: 10.35 Max: 1535 Sum: 15736535) + Executed : 1520522 (Average: 10.35 Max: 1535 Sum: 15733761 Ratio: 99.98%) + Bounded : 139 (Average: 19.96 Max: 32 Sum: 2774 Ratio: 0.02%) + +Rules : 222636 (Original: 222598) +Atoms : 6829 +Bodies : 147015 (Original: 146977) + Count : 629 (Original: 633) +Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207) +Tight : Yes +Variables : 103790 (Eliminated: 0 Frozen: 85188) +Constraints : 876910 (Binary: 97.7% Ternary: 1.0% Other: 1.3%) + +Memory Peak : 446MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 13.89s +Memory: 382MB (+0MB) +UNKNOWN +Iteration Time: 13.89s + +Iteration 58 +Queue: [(0,30,57,True)] +Grounded Until: 30 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 59 +Time : 848.393s (Solving: 842.94s 1st Model: 0.06s Unsat: 0.00s) +CPU Time : 848.656s + +Choices : 21917820 (Domain: 21917796) +Conflicts : 1543956 (Analyzed: 1543956) +Restarts : 5801 (Average: 266.15 Last: 289) +Model-Level : 1229.0 +Problems : 59 (Average Length: 32.00 Splits: 0) +Lemmas : 1543956 (Deleted: 1501839) + Binary : 4701 (Ratio: 0.30%) + Ternary : 3718 (Ratio: 0.24%) + Conflict : 1543956 (Average Length: 1515.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 1543956 (Average: 10.31 Max: 1535 Sum: 15923496) + Executed : 1543817 (Average: 10.31 Max: 1535 Sum: 15920722 Ratio: 99.98%) + Bounded : 139 (Average: 19.96 Max: 32 Sum: 2774 Ratio: 0.02%) + +Rules : 222636 (Original: 222598) +Atoms : 6829 +Bodies : 147015 (Original: 146977) + Count : 629 (Original: 633) +Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207) +Tight : Yes +Variables : 103790 (Eliminated: 0 Frozen: 85188) +Constraints : 876910 (Binary: 97.7% Ternary: 1.0% Other: 1.3%) + +Memory Peak : 446MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 13.51s +Memory: 382MB (+0MB) +UNKNOWN +Iteration Time: 13.51s + +Iteration 59 +Queue: [(0,30,58,True)] +Grounded Until: 30 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 60 +Time : 863.223s (Solving: 857.75s 1st Model: 0.06s Unsat: 0.00s) +CPU Time : 863.492s + +Choices : 22234122 (Domain: 22234098) +Conflicts : 1569941 (Analyzed: 1569941) +Restarts : 5901 (Average: 266.05 Last: 289) +Model-Level : 1229.0 +Problems : 60 (Average Length: 32.00 Splits: 0) +Lemmas : 1569941 (Deleted: 1527679) + Binary : 4724 (Ratio: 0.30%) + Ternary : 3722 (Ratio: 0.24%) + Conflict : 1569941 (Average Length: 1513.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 1569941 (Average: 10.28 Max: 1535 Sum: 16135091) + Executed : 1569802 (Average: 10.28 Max: 1535 Sum: 16132317 Ratio: 99.98%) + Bounded : 139 (Average: 19.96 Max: 32 Sum: 2774 Ratio: 0.02%) + +Rules : 222636 (Original: 222598) +Atoms : 6829 +Bodies : 147015 (Original: 146977) + Count : 629 (Original: 633) +Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207) +Tight : Yes +Variables : 103790 (Eliminated: 0 Frozen: 85188) +Constraints : 876910 (Binary: 97.7% Ternary: 1.0% Other: 1.3%) + +Memory Peak : 446MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 14.84s +Memory: 382MB (+0MB) +UNKNOWN +Iteration Time: 14.84s + +Iteration 60 +Queue: [(0,30,59,True)] +Grounded Until: 30 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 61 +Time : 876.789s (Solving: 871.29s 1st Model: 0.06s Unsat: 0.00s) +CPU Time : 877.064s + +Choices : 22525850 (Domain: 22525826) +Conflicts : 1593773 (Analyzed: 1593773) +Restarts : 6001 (Average: 265.58 Last: 289) +Model-Level : 1229.0 +Problems : 61 (Average Length: 32.00 Splits: 0) +Lemmas : 1593773 (Deleted: 1550691) + Binary : 4735 (Ratio: 0.30%) + Ternary : 3733 (Ratio: 0.23%) + Conflict : 1593773 (Average Length: 1511.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 1593773 (Average: 10.25 Max: 1535 Sum: 16330011) + Executed : 1593633 (Average: 10.24 Max: 1535 Sum: 16327236 Ratio: 99.98%) + Bounded : 140 (Average: 19.82 Max: 32 Sum: 2775 Ratio: 0.02%) + +Rules : 222636 (Original: 222598) +Atoms : 6829 +Bodies : 147015 (Original: 146977) + Count : 629 (Original: 633) +Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207) +Tight : Yes +Variables : 103790 (Eliminated: 0 Frozen: 85188) +Constraints : 876910 (Binary: 97.7% Ternary: 1.0% Other: 1.3%) + +Memory Peak : 446MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 13.57s +Memory: 382MB (+0MB) +UNKNOWN +Iteration Time: 13.58s + +Iteration 61 +Queue: [(0,30,60,True)] +Grounded Until: 30 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 62 +Time : 891.934s (Solving: 886.39s 1st Model: 0.06s Unsat: 0.00s) +CPU Time : 892.216s + +Choices : 22805746 (Domain: 22805722) +Conflicts : 1619161 (Analyzed: 1619161) +Restarts : 6101 (Average: 265.39 Last: 289) +Model-Level : 1229.0 +Problems : 62 (Average Length: 32.00 Splits: 0) +Lemmas : 1619161 (Deleted: 1577125) + Binary : 4759 (Ratio: 0.29%) + Ternary : 3741 (Ratio: 0.23%) + Conflict : 1619161 (Average Length: 1511.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 1619161 (Average: 10.19 Max: 1535 Sum: 16505965) + Executed : 1619021 (Average: 10.19 Max: 1535 Sum: 16503190 Ratio: 99.98%) + Bounded : 140 (Average: 19.82 Max: 32 Sum: 2775 Ratio: 0.02%) + +Rules : 222636 (Original: 222598) +Atoms : 6829 +Bodies : 147015 (Original: 146977) + Count : 629 (Original: 633) +Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207) +Tight : Yes +Variables : 103790 (Eliminated: 0 Frozen: 85188) +Constraints : 876910 (Binary: 97.7% Ternary: 1.0% Other: 1.3%) + +Memory Peak : 446MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 15.15s +Memory: 382MB (+0MB) +UNKNOWN +Iteration Time: 15.15s + +Iteration 62 +Queue: [(0,30,61,True)] +Grounded Until: 30 +Solving... +*** Info : (planner): INTERRUPTED by signal! +UNKNOWN + +INTERRUPTED : 1 + +Models : 0+ +Calls : 63 +Time : 894.175s (Solving: 888.60s 1st Model: 0.06s Unsat: 0.00s) +CPU Time : 894.440s + +Choices : 22863173 (Domain: 22863149) +Conflicts : 1622864 (Analyzed: 1622864) +Restarts : 6125 (Average: 264.96 Last: 289) +Model-Level : 1229.0 +Problems : 63 (Average Length: 32.00 Splits: 0) +Lemmas : 1622864 (Deleted: 1581658) + Binary : 4771 (Ratio: 0.29%) + Ternary : 3745 (Ratio: 0.23%) + Conflict : 1622864 (Average Length: 1511.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 1622864 (Average: 10.19 Max: 1535 Sum: 16537536) + Executed : 1622724 (Average: 10.19 Max: 1535 Sum: 16534761 Ratio: 99.98%) + Bounded : 140 (Average: 19.82 Max: 32 Sum: 2775 Ratio: 0.02%) + +Rules : 222636 (Original: 222598) +Atoms : 6829 +Bodies : 147015 (Original: 146977) + Count : 629 (Original: 633) +Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207) +Tight : Yes +Variables : 103790 (Eliminated: 0 Frozen: 85188) +Constraints : 876910 (Binary: 97.7% Ternary: 1.0% Other: 1.3%) + +Memory Peak : 446MB +Max. Length : 30 steps +Models : 1 + +