diff --git a/gc-ta1-tt1-single-shot/ipc-2011_elevator-sequential-satisficing_4.env b/gc-ta1-tt1-single-shot/ipc-2011_elevator-sequential-satisficing_4.env new file mode 100644 index 000000000..27ab95020 --- /dev/null +++ b/gc-ta1-tt1-single-shot/ipc-2011_elevator-sequential-satisficing_4.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-4.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 35 +- -T 35 +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: 4 + ipc: ipc-2011 + planLength: 35 +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_4.err b/gc-ta1-tt1-single-shot/ipc-2011_elevator-sequential-satisficing_4.err new file mode 100644 index 000000000..f8ccecb04 --- /dev/null +++ b/gc-ta1-tt1-single-shot/ipc-2011_elevator-sequential-satisficing_4.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': 4, 'planLength': 35} +# 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-4.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 35', '-T 35'] +# 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.03 MEM 674008 MAXMEM 674008 STALE 0 MAXMEM_RSS 571924 + + diff --git a/gc-ta1-tt1-single-shot/ipc-2011_elevator-sequential-satisficing_4.out b/gc-ta1-tt1-single-shot/ipc-2011_elevator-sequential-satisficing_4.out new file mode 100644 index 000000000..e67cde003 --- /dev/null +++ b/gc-ta1-tt1-single-shot/ipc-2011_elevator-sequential-satisficing_4.out @@ -0,0 +1,1648 @@ +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-4.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-4.pddl +Parsing... +Parsing: [0.030s CPU, 0.041s wall-clock] +Normalizing task... [0.010s CPU, 0.002s wall-clock] +Instantiating... +Generating Datalog program... [0.010s CPU, 0.011s wall-clock] +Normalizing Datalog program... +Normalizing Datalog program: [0.020s CPU, 0.024s wall-clock] +Preparing model... [0.030s CPU, 0.030s wall-clock] +Generated 46 rules. +Computing model... [0.710s CPU, 0.712s wall-clock] +6004 relevant atoms +3524 auxiliary atoms +9528 final queue length +18930 total queue pushes +Completing instantiation... [1.770s CPU, 1.769s wall-clock] +Instantiating: [2.550s CPU, 2.555s wall-clock] +Computing fact groups... +Finding invariants... +12 initial candidates +Finding invariants: [0.040s CPU, 0.042s wall-clock] +Checking invariant weight... [0.010s CPU, 0.003s wall-clock] +Instantiating groups... [0.090s CPU, 0.096s wall-clock] +Collecting mutex groups... [0.010s CPU, 0.004s wall-clock] +Choosing groups... +0 uncovered facts +Choosing groups: [0.010s CPU, 0.011s wall-clock] +Building translation key... [0.010s CPU, 0.007s wall-clock] +Computing fact groups: [0.190s CPU, 0.189s wall-clock] +Building STRIPS to SAS dictionary... [0.000s CPU, 0.004s wall-clock] +Building dictionary for full mutex groups... [0.010s CPU, 0.003s wall-clock] +Building mutex information... +Building mutex information: [0.000s CPU, 0.004s wall-clock] +Translating task... +Processing axioms... +Simplifying axioms... [0.000s CPU, 0.000s wall-clock] +Processing axioms: [0.080s CPU, 0.081s wall-clock] +Translating task: [1.480s CPU, 1.479s wall-clock] +0 effect conditions simplified +0 implied preconditions added +Detecting unreachable propositions... +0 operators removed +0 axioms removed +34 propositions removed +Detecting unreachable propositions: [0.820s CPU, 0.822s wall-clock] +Reordering and filtering variables... +34 of 34 variables necessary. +0 of 34 mutex groups necessary. +5072 of 5072 operators necessary. +0 of 0 axiom rules necessary. +Reordering and filtering variables: [0.240s CPU, 0.238s wall-clock] +Translator variables: 34 +Translator derived variables: 0 +Translator facts: 592 +Translator goal facts: 26 +Translator mutex groups: 0 +Translator total mutex groups size: 0 +Translator operators: 5072 +Translator axioms: 0 +Translator task size: 30532 +Translator peak memory: 56012 KB +Writing output... [0.520s CPU, 0.559s wall-clock] +Done! [5.920s CPU, 5.964s wall-clock] +planner.py version 0.0.1 + +Time: 1.24s +Memory: 133MB + +Iteration 1 +Queue: [(0,35,0,True)] +Grounded Until: 0 +Expected Memory: 133MB +Grounding... [('step', [1]), ('step', [2]), ('step', [3]), ('step', [4]), ('step', [5]), ('step', [6]), ('step', [7]), ('step', [8]), ('step', [9]), ('step', [10]), ('step', [11]), ('step', [12]), ('step', [13]), ('step', [14]), ('step', [15]), ('step', [16]), ('step', [17]), ('step', [18]), ('step', [19]), ('step', [20]), ('step', [21]), ('step', [22]), ('step', [23]), ('step', [24]), ('step', [25]), ('step', [26]), ('step', [27]), ('step', [28]), ('step', [29]), ('step', [30]), ('step', [31]), ('step', [32]), ('step', [33]), ('step', [34]), ('step', [35]), ('check', [35])] +Grounding Time: 2.94s +Memory: 375MB (+242MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 1+ +Calls : 1 +Time : 6.516s (Solving: 0.21s 1st Model: 0.19s Unsat: 0.00s) +CPU Time : 6.332s + +Choices : 13442 (Domain: 13418) +Conflicts : 184 (Analyzed: 184) +Restarts : 2 (Average: 92.00 Last: 24) +Model-Level : 2483.0 +Problems : 1 (Average Length: 37.00 Splits: 0) +Lemmas : 184 (Deleted: 0) + Binary : 29 (Ratio: 15.76%) + Ternary : 31 (Ratio: 16.85%) + Conflict : 184 (Average Length: 166.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 184 (Average: 53.40 Max: 571 Sum: 9825) + Executed : 184 (Average: 53.40 Max: 571 Sum: 9825 Ratio: 100.00%) + Bounded : 0 (Average: 0.00 Max: 0 Sum: 0 Ratio: 0.00%) + +Rules : 0 +Atoms : 0 +Bodies : 0 +Tight : Yes +Variables : 214565 (Eliminated: 0 Frozen: 19194) +Constraints : 1466315 (Binary: 97.3% Ternary: 1.3% Other: 1.4%) + +Memory Peak : 588MB +Max. Length : 0 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 0.35s +Memory: 524MB (+149MB) +SAT +Testing... +NOT SERIALIZABLE +Testing Time: 2.42s +Memory: 542MB (+18MB) +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 2 +Time : 97.973s (Solving: 90.04s 1st Model: 0.19s Unsat: 0.00s) +CPU Time : 97.828s + +Choices : 7085552 (Domain: 7085528) +Conflicts : 32782 (Analyzed: 32782) +Restarts : 102 (Average: 321.39 Last: 305) +Model-Level : 2483.0 +Problems : 2 (Average Length: 37.00 Splits: 0) +Lemmas : 32782 (Deleted: 24924) + Binary : 953 (Ratio: 2.91%) + Ternary : 973 (Ratio: 2.97%) + Conflict : 32782 (Average Length: 441.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 32782 (Average: 214.59 Max: 3860 Sum: 7034755) + Executed : 32697 (Average: 214.50 Max: 3860 Sum: 7031682 Ratio: 99.96%) + Bounded : 85 (Average: 36.15 Max: 37 Sum: 3073 Ratio: 0.04%) + +Rules : 482958 (Original: 482854) +Atoms : 12443 +Bodies : 318208 (Original: 318104) + Count : 1137 (Original: 1148) +Equivalences : 162277 (Atom=Atom: 48 Body=Body: 0 Other: 162229) +Tight : Yes +Variables : 216990 (Eliminated: 0 Frozen: 181320) +Constraints : 1940687 (Binary: 97.8% Ternary: 1.0% Other: 1.2%) + +Memory Peak : 588MB +Max. Length : 0 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 90.21s +Memory: 557MB (+15MB) +UNKNOWN +Iteration Time: 97.73s + +Iteration 2 +Queue: [(0,35,1,True)] +Grounded Until: 35 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 3 +Time : 156.485s (Solving: 148.50s 1st Model: 0.19s Unsat: 0.00s) +CPU Time : 156.364s + +Choices : 12327759 (Domain: 12327735) +Conflicts : 64198 (Analyzed: 64198) +Restarts : 202 (Average: 317.81 Last: 542) +Model-Level : 2483.0 +Problems : 3 (Average Length: 37.00 Splits: 0) +Lemmas : 64198 (Deleted: 51604) + Binary : 1641 (Ratio: 2.56%) + Ternary : 1572 (Ratio: 2.45%) + Conflict : 64198 (Average Length: 634.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 64198 (Average: 189.56 Max: 4236 Sum: 12169322) + Executed : 64098 (Average: 189.50 Max: 4236 Sum: 12165766 Ratio: 99.97%) + Bounded : 100 (Average: 35.56 Max: 37 Sum: 3556 Ratio: 0.03%) + +Rules : 482958 (Original: 482854) +Atoms : 12443 +Bodies : 318208 (Original: 318104) + Count : 1137 (Original: 1148) +Equivalences : 162277 (Atom=Atom: 48 Body=Body: 0 Other: 162229) +Tight : Yes +Variables : 216990 (Eliminated: 0 Frozen: 181320) +Constraints : 1927277 (Binary: 97.8% Ternary: 1.0% Other: 1.2%) + +Memory Peak : 588MB +Max. Length : 35 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 58.54s +Memory: 557MB (+0MB) +UNKNOWN +Iteration Time: 58.54s + +Iteration 3 +Queue: [(0,35,2,True)] +Grounded Until: 35 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 4 +Time : 179.449s (Solving: 171.41s 1st Model: 0.19s Unsat: 0.00s) +CPU Time : 179.340s + +Choices : 13347525 (Domain: 13347501) +Conflicts : 90597 (Analyzed: 90597) +Restarts : 302 (Average: 299.99 Last: 542) +Model-Level : 2483.0 +Problems : 4 (Average Length: 37.00 Splits: 0) +Lemmas : 90597 (Deleted: 74374) + Binary : 2014 (Ratio: 2.22%) + Ternary : 1911 (Ratio: 2.11%) + Conflict : 90597 (Average Length: 834.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 90597 (Average: 144.16 Max: 4236 Sum: 13060353) + Executed : 90486 (Average: 144.12 Max: 4236 Sum: 13056606 Ratio: 99.97%) + Bounded : 111 (Average: 33.76 Max: 37 Sum: 3747 Ratio: 0.03%) + +Rules : 482958 (Original: 482854) +Atoms : 12443 +Bodies : 318208 (Original: 318104) + Count : 1137 (Original: 1148) +Equivalences : 162277 (Atom=Atom: 48 Body=Body: 0 Other: 162229) +Tight : Yes +Variables : 216990 (Eliminated: 0 Frozen: 181320) +Constraints : 1926043 (Binary: 97.8% Ternary: 1.0% Other: 1.2%) + +Memory Peak : 588MB +Max. Length : 35 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 22.98s +Memory: 557MB (+0MB) +UNKNOWN +Iteration Time: 22.98s + +Iteration 4 +Queue: [(0,35,3,True)] +Grounded Until: 35 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 5 +Time : 201.643s (Solving: 193.56s 1st Model: 0.19s Unsat: 0.00s) +CPU Time : 201.540s + +Choices : 14095121 (Domain: 14095097) +Conflicts : 116349 (Analyzed: 116349) +Restarts : 402 (Average: 289.43 Last: 542) +Model-Level : 2483.0 +Problems : 5 (Average Length: 37.00 Splits: 0) +Lemmas : 116349 (Deleted: 98780) + Binary : 2226 (Ratio: 1.91%) + Ternary : 2108 (Ratio: 1.81%) + Conflict : 116349 (Average Length: 975.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 116349 (Average: 117.55 Max: 4236 Sum: 13676917) + Executed : 116233 (Average: 117.52 Max: 4236 Sum: 13673129 Ratio: 99.97%) + Bounded : 116 (Average: 32.66 Max: 37 Sum: 3788 Ratio: 0.03%) + +Rules : 482958 (Original: 482854) +Atoms : 12443 +Bodies : 318208 (Original: 318104) + Count : 1137 (Original: 1148) +Equivalences : 162277 (Atom=Atom: 48 Body=Body: 0 Other: 162229) +Tight : Yes +Variables : 216990 (Eliminated: 0 Frozen: 181320) +Constraints : 1925001 (Binary: 97.8% Ternary: 1.0% Other: 1.2%) + +Memory Peak : 588MB +Max. Length : 35 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 22.20s +Memory: 557MB (+0MB) +UNKNOWN +Iteration Time: 22.20s + +Iteration 5 +Queue: [(0,35,4,True)] +Grounded Until: 35 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 6 +Time : 225.512s (Solving: 217.38s 1st Model: 0.19s Unsat: 0.00s) +CPU Time : 225.420s + +Choices : 15004909 (Domain: 15004885) +Conflicts : 144273 (Analyzed: 144273) +Restarts : 502 (Average: 287.40 Last: 542) +Model-Level : 2483.0 +Problems : 6 (Average Length: 37.00 Splits: 0) +Lemmas : 144273 (Deleted: 125657) + Binary : 2355 (Ratio: 1.63%) + Ternary : 2248 (Ratio: 1.56%) + Conflict : 144273 (Average Length: 1056.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 144273 (Average: 100.24 Max: 4236 Sum: 14462250) + Executed : 144155 (Average: 100.22 Max: 4236 Sum: 14458424 Ratio: 99.97%) + Bounded : 118 (Average: 32.42 Max: 37 Sum: 3826 Ratio: 0.03%) + +Rules : 482958 (Original: 482854) +Atoms : 12443 +Bodies : 318208 (Original: 318104) + Count : 1137 (Original: 1148) +Equivalences : 162277 (Atom=Atom: 48 Body=Body: 0 Other: 162229) +Tight : Yes +Variables : 216990 (Eliminated: 0 Frozen: 181320) +Constraints : 1924955 (Binary: 97.8% Ternary: 1.0% Other: 1.2%) + +Memory Peak : 588MB +Max. Length : 35 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 23.88s +Memory: 557MB (+0MB) +UNKNOWN +Iteration Time: 23.88s + +Iteration 6 +Queue: [(0,35,5,True)] +Grounded Until: 35 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 7 +Time : 247.414s (Solving: 239.23s 1st Model: 0.19s Unsat: 0.00s) +CPU Time : 247.332s + +Choices : 15463363 (Domain: 15463339) +Conflicts : 169703 (Analyzed: 169703) +Restarts : 602 (Average: 281.90 Last: 542) +Model-Level : 2483.0 +Problems : 7 (Average Length: 37.00 Splits: 0) +Lemmas : 169703 (Deleted: 149447) + Binary : 2451 (Ratio: 1.44%) + Ternary : 2356 (Ratio: 1.39%) + Conflict : 169703 (Average Length: 1171.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 169703 (Average: 87.17 Max: 4236 Sum: 14793569) + Executed : 169581 (Average: 87.15 Max: 4236 Sum: 14789631 Ratio: 99.97%) + Bounded : 122 (Average: 32.28 Max: 37 Sum: 3938 Ratio: 0.03%) + +Rules : 482958 (Original: 482854) +Atoms : 12443 +Bodies : 318208 (Original: 318104) + Count : 1137 (Original: 1148) +Equivalences : 162277 (Atom=Atom: 48 Body=Body: 0 Other: 162229) +Tight : Yes +Variables : 216990 (Eliminated: 0 Frozen: 181320) +Constraints : 1924943 (Binary: 97.8% Ternary: 1.0% Other: 1.2%) + +Memory Peak : 685MB +Max. Length : 35 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 21.91s +Memory: 621MB (+64MB) +UNKNOWN +Iteration Time: 21.91s + +Iteration 7 +Queue: [(0,35,6,True)] +Grounded Until: 35 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 8 +Time : 273.582s (Solving: 265.36s 1st Model: 0.19s Unsat: 0.00s) +CPU Time : 273.508s + +Choices : 16579343 (Domain: 16579319) +Conflicts : 197588 (Analyzed: 197588) +Restarts : 702 (Average: 281.46 Last: 542) +Model-Level : 2483.0 +Problems : 8 (Average Length: 37.00 Splits: 0) +Lemmas : 197588 (Deleted: 176631) + Binary : 2519 (Ratio: 1.27%) + Ternary : 2426 (Ratio: 1.23%) + Conflict : 197588 (Average Length: 1240.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 197588 (Average: 79.79 Max: 4236 Sum: 15766532) + Executed : 197462 (Average: 79.77 Max: 4236 Sum: 15762446 Ratio: 99.97%) + Bounded : 126 (Average: 32.43 Max: 37 Sum: 4086 Ratio: 0.03%) + +Rules : 482958 (Original: 482854) +Atoms : 12443 +Bodies : 318208 (Original: 318104) + Count : 1137 (Original: 1148) +Equivalences : 162277 (Atom=Atom: 48 Body=Body: 0 Other: 162229) +Tight : Yes +Variables : 216990 (Eliminated: 0 Frozen: 181320) +Constraints : 1923227 (Binary: 97.8% Ternary: 1.0% Other: 1.2%) + +Memory Peak : 685MB +Max. Length : 35 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 26.18s +Memory: 621MB (+0MB) +UNKNOWN +Iteration Time: 26.18s + +Iteration 8 +Queue: [(0,35,7,True)] +Grounded Until: 35 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 9 +Time : 295.457s (Solving: 287.16s 1st Model: 0.19s Unsat: 0.00s) +CPU Time : 295.392s + +Choices : 17203488 (Domain: 17203464) +Conflicts : 222459 (Analyzed: 222459) +Restarts : 802 (Average: 277.38 Last: 542) +Model-Level : 2483.0 +Problems : 9 (Average Length: 37.00 Splits: 0) +Lemmas : 222459 (Deleted: 200364) + Binary : 2631 (Ratio: 1.18%) + Ternary : 2536 (Ratio: 1.14%) + Conflict : 222459 (Average Length: 1278.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 222459 (Average: 73.11 Max: 4236 Sum: 16264223) + Executed : 222331 (Average: 73.09 Max: 4236 Sum: 16260135 Ratio: 99.97%) + Bounded : 128 (Average: 31.94 Max: 37 Sum: 4088 Ratio: 0.03%) + +Rules : 482958 (Original: 482854) +Atoms : 12443 +Bodies : 318208 (Original: 318104) + Count : 1137 (Original: 1148) +Equivalences : 162277 (Atom=Atom: 48 Body=Body: 0 Other: 162229) +Tight : Yes +Variables : 216990 (Eliminated: 0 Frozen: 181320) +Constraints : 1919040 (Binary: 97.8% Ternary: 1.0% Other: 1.2%) + +Memory Peak : 685MB +Max. Length : 35 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 21.89s +Memory: 621MB (+0MB) +UNKNOWN +Iteration Time: 21.89s + +Iteration 9 +Queue: [(0,35,8,True)] +Grounded Until: 35 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 10 +Time : 315.583s (Solving: 307.24s 1st Model: 0.19s Unsat: 0.00s) +CPU Time : 315.528s + +Choices : 17787177 (Domain: 17787153) +Conflicts : 246879 (Analyzed: 246879) +Restarts : 902 (Average: 273.70 Last: 542) +Model-Level : 2483.0 +Problems : 10 (Average Length: 37.00 Splits: 0) +Lemmas : 246879 (Deleted: 221392) + Binary : 2765 (Ratio: 1.12%) + Ternary : 2643 (Ratio: 1.07%) + Conflict : 246879 (Average Length: 1290.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 246879 (Average: 67.74 Max: 4236 Sum: 16722395) + Executed : 246747 (Average: 67.72 Max: 4236 Sum: 16718231 Ratio: 99.98%) + Bounded : 132 (Average: 31.55 Max: 37 Sum: 4164 Ratio: 0.02%) + +Rules : 482958 (Original: 482854) +Atoms : 12443 +Bodies : 318208 (Original: 318104) + Count : 1137 (Original: 1148) +Equivalences : 162277 (Atom=Atom: 48 Body=Body: 0 Other: 162229) +Tight : Yes +Variables : 216990 (Eliminated: 0 Frozen: 181320) +Constraints : 1919040 (Binary: 97.8% Ternary: 1.0% Other: 1.2%) + +Memory Peak : 685MB +Max. Length : 35 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 20.14s +Memory: 621MB (+0MB) +UNKNOWN +Iteration Time: 20.14s + +Iteration 10 +Queue: [(0,35,9,True)] +Grounded Until: 35 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 11 +Time : 337.287s (Solving: 328.87s 1st Model: 0.19s Unsat: 0.00s) +CPU Time : 337.244s + +Choices : 18437770 (Domain: 18437746) +Conflicts : 272239 (Analyzed: 272239) +Restarts : 1002 (Average: 271.70 Last: 542) +Model-Level : 2483.0 +Problems : 11 (Average Length: 37.00 Splits: 0) +Lemmas : 272239 (Deleted: 247627) + Binary : 2840 (Ratio: 1.04%) + Ternary : 2705 (Ratio: 0.99%) + Conflict : 272239 (Average Length: 1302.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 272239 (Average: 63.36 Max: 4236 Sum: 17248757) + Executed : 272106 (Average: 63.34 Max: 4236 Sum: 17244556 Ratio: 99.98%) + Bounded : 133 (Average: 31.59 Max: 37 Sum: 4201 Ratio: 0.02%) + +Rules : 482958 (Original: 482854) +Atoms : 12443 +Bodies : 318208 (Original: 318104) + Count : 1137 (Original: 1148) +Equivalences : 162277 (Atom=Atom: 48 Body=Body: 0 Other: 162229) +Tight : Yes +Variables : 216990 (Eliminated: 0 Frozen: 181320) +Constraints : 1918882 (Binary: 97.8% Ternary: 1.0% Other: 1.2%) + +Memory Peak : 685MB +Max. Length : 35 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 21.71s +Memory: 621MB (+0MB) +UNKNOWN +Iteration Time: 21.72s + +Iteration 11 +Queue: [(0,35,10,True)] +Grounded Until: 35 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 12 +Time : 361.588s (Solving: 353.13s 1st Model: 0.19s Unsat: 0.00s) +CPU Time : 361.556s + +Choices : 19105128 (Domain: 19105104) +Conflicts : 301753 (Analyzed: 301753) +Restarts : 1102 (Average: 273.82 Last: 542) +Model-Level : 2483.0 +Problems : 12 (Average Length: 37.00 Splits: 0) +Lemmas : 301753 (Deleted: 274821) + Binary : 2955 (Ratio: 0.98%) + Ternary : 2788 (Ratio: 0.92%) + Conflict : 301753 (Average Length: 1304.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 301753 (Average: 58.96 Max: 4236 Sum: 17792302) + Executed : 301614 (Average: 58.95 Max: 4236 Sum: 17787915 Ratio: 99.98%) + Bounded : 139 (Average: 31.56 Max: 37 Sum: 4387 Ratio: 0.02%) + +Rules : 482958 (Original: 482854) +Atoms : 12443 +Bodies : 318208 (Original: 318104) + Count : 1137 (Original: 1148) +Equivalences : 162277 (Atom=Atom: 48 Body=Body: 0 Other: 162229) +Tight : Yes +Variables : 216990 (Eliminated: 0 Frozen: 181320) +Constraints : 1918724 (Binary: 97.8% Ternary: 1.0% Other: 1.2%) + +Memory Peak : 685MB +Max. Length : 35 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 24.31s +Memory: 621MB (+0MB) +UNKNOWN +Iteration Time: 24.32s + +Iteration 12 +Queue: [(0,35,11,True)] +Grounded Until: 35 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 13 +Time : 385.133s (Solving: 376.61s 1st Model: 0.19s Unsat: 0.00s) +CPU Time : 385.112s + +Choices : 19941666 (Domain: 19941642) +Conflicts : 328035 (Analyzed: 328035) +Restarts : 1202 (Average: 272.91 Last: 542) +Model-Level : 2483.0 +Problems : 13 (Average Length: 37.00 Splits: 0) +Lemmas : 328035 (Deleted: 300181) + Binary : 3028 (Ratio: 0.92%) + Ternary : 2892 (Ratio: 0.88%) + Conflict : 328035 (Average Length: 1291.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 328035 (Average: 56.41 Max: 4236 Sum: 18504961) + Executed : 327893 (Average: 56.40 Max: 4236 Sum: 18500571 Ratio: 99.98%) + Bounded : 142 (Average: 30.92 Max: 37 Sum: 4390 Ratio: 0.02%) + +Rules : 482958 (Original: 482854) +Atoms : 12443 +Bodies : 318208 (Original: 318104) + Count : 1137 (Original: 1148) +Equivalences : 162277 (Atom=Atom: 48 Body=Body: 0 Other: 162229) +Tight : Yes +Variables : 216990 (Eliminated: 0 Frozen: 181320) +Constraints : 1915646 (Binary: 97.8% Ternary: 1.0% Other: 1.2%) + +Memory Peak : 685MB +Max. Length : 35 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 23.56s +Memory: 621MB (+0MB) +UNKNOWN +Iteration Time: 23.56s + +Iteration 13 +Queue: [(0,35,12,True)] +Grounded Until: 35 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 14 +Time : 410.612s (Solving: 402.04s 1st Model: 0.19s Unsat: 0.00s) +CPU Time : 410.600s + +Choices : 20857283 (Domain: 20857259) +Conflicts : 354236 (Analyzed: 354236) +Restarts : 1302 (Average: 272.07 Last: 542) +Model-Level : 2483.0 +Problems : 14 (Average Length: 37.00 Splits: 0) +Lemmas : 354236 (Deleted: 325452) + Binary : 3104 (Ratio: 0.88%) + Ternary : 2984 (Ratio: 0.84%) + Conflict : 354236 (Average Length: 1288.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 354236 (Average: 54.47 Max: 4236 Sum: 19296688) + Executed : 354091 (Average: 54.46 Max: 4236 Sum: 19292187 Ratio: 99.98%) + Bounded : 145 (Average: 31.04 Max: 37 Sum: 4501 Ratio: 0.02%) + +Rules : 482958 (Original: 482854) +Atoms : 12443 +Bodies : 318208 (Original: 318104) + Count : 1137 (Original: 1148) +Equivalences : 162277 (Atom=Atom: 48 Body=Body: 0 Other: 162229) +Tight : Yes +Variables : 216990 (Eliminated: 0 Frozen: 181320) +Constraints : 1915646 (Binary: 97.8% Ternary: 1.0% Other: 1.2%) + +Memory Peak : 685MB +Max. Length : 35 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 25.49s +Memory: 621MB (+0MB) +UNKNOWN +Iteration Time: 25.49s + +Iteration 14 +Queue: [(0,35,13,True)] +Grounded Until: 35 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 15 +Time : 439.750s (Solving: 431.13s 1st Model: 0.19s Unsat: 0.00s) +CPU Time : 439.748s + +Choices : 21993118 (Domain: 21993094) +Conflicts : 380240 (Analyzed: 380240) +Restarts : 1402 (Average: 271.21 Last: 542) +Model-Level : 2483.0 +Problems : 15 (Average Length: 37.00 Splits: 0) +Lemmas : 380240 (Deleted: 350641) + Binary : 3196 (Ratio: 0.84%) + Ternary : 3060 (Ratio: 0.80%) + Conflict : 380240 (Average Length: 1280.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 380240 (Average: 53.39 Max: 4236 Sum: 20299583) + Executed : 380094 (Average: 53.37 Max: 4236 Sum: 20295045 Ratio: 99.98%) + Bounded : 146 (Average: 31.08 Max: 37 Sum: 4538 Ratio: 0.02%) + +Rules : 482958 (Original: 482854) +Atoms : 12443 +Bodies : 318208 (Original: 318104) + Count : 1137 (Original: 1148) +Equivalences : 162277 (Atom=Atom: 48 Body=Body: 0 Other: 162229) +Tight : Yes +Variables : 216990 (Eliminated: 0 Frozen: 181320) +Constraints : 1914737 (Binary: 97.8% Ternary: 1.0% Other: 1.2%) + +Memory Peak : 685MB +Max. Length : 35 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 29.15s +Memory: 621MB (+0MB) +UNKNOWN +Iteration Time: 29.15s + +Iteration 15 +Queue: [(0,35,14,True)] +Grounded Until: 35 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 16 +Time : 463.404s (Solving: 454.74s 1st Model: 0.19s Unsat: 0.00s) +CPU Time : 463.412s + +Choices : 22701010 (Domain: 22700986) +Conflicts : 405744 (Analyzed: 405744) +Restarts : 1502 (Average: 270.14 Last: 542) +Model-Level : 2483.0 +Problems : 16 (Average Length: 37.00 Splits: 0) +Lemmas : 405744 (Deleted: 375967) + Binary : 3234 (Ratio: 0.80%) + Ternary : 3112 (Ratio: 0.77%) + Conflict : 405744 (Average Length: 1293.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 405744 (Average: 51.46 Max: 4236 Sum: 20878849) + Executed : 405598 (Average: 51.45 Max: 4236 Sum: 20874311 Ratio: 99.98%) + Bounded : 146 (Average: 31.08 Max: 37 Sum: 4538 Ratio: 0.02%) + +Rules : 482958 (Original: 482854) +Atoms : 12443 +Bodies : 318208 (Original: 318104) + Count : 1137 (Original: 1148) +Equivalences : 162277 (Atom=Atom: 48 Body=Body: 0 Other: 162229) +Tight : Yes +Variables : 216990 (Eliminated: 0 Frozen: 181320) +Constraints : 1914726 (Binary: 97.8% Ternary: 1.0% Other: 1.2%) + +Memory Peak : 685MB +Max. Length : 35 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 23.67s +Memory: 621MB (+0MB) +UNKNOWN +Iteration Time: 23.67s + +Iteration 16 +Queue: [(0,35,15,True)] +Grounded Until: 35 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 17 +Time : 486.608s (Solving: 477.87s 1st Model: 0.19s Unsat: 0.00s) +CPU Time : 486.628s + +Choices : 23383420 (Domain: 23383396) +Conflicts : 433319 (Analyzed: 433319) +Restarts : 1602 (Average: 270.49 Last: 542) +Model-Level : 2483.0 +Problems : 17 (Average Length: 37.00 Splits: 0) +Lemmas : 433319 (Deleted: 403428) + Binary : 3308 (Ratio: 0.76%) + Ternary : 3199 (Ratio: 0.74%) + Conflict : 433319 (Average Length: 1295.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 433319 (Average: 49.45 Max: 4236 Sum: 21429478) + Executed : 433169 (Average: 49.44 Max: 4236 Sum: 21424900 Ratio: 99.98%) + Bounded : 150 (Average: 30.52 Max: 37 Sum: 4578 Ratio: 0.02%) + +Rules : 482958 (Original: 482854) +Atoms : 12443 +Bodies : 318208 (Original: 318104) + Count : 1137 (Original: 1148) +Equivalences : 162277 (Atom=Atom: 48 Body=Body: 0 Other: 162229) +Tight : Yes +Variables : 216990 (Eliminated: 0 Frozen: 181320) +Constraints : 1914726 (Binary: 97.8% Ternary: 1.0% Other: 1.2%) + +Memory Peak : 685MB +Max. Length : 35 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 23.22s +Memory: 621MB (+0MB) +UNKNOWN +Iteration Time: 23.22s + +Iteration 17 +Queue: [(0,35,16,True)] +Grounded Until: 35 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 18 +Time : 508.668s (Solving: 499.87s 1st Model: 0.19s Unsat: 0.00s) +CPU Time : 508.700s + +Choices : 24047492 (Domain: 24047468) +Conflicts : 458956 (Analyzed: 458956) +Restarts : 1702 (Average: 269.66 Last: 542) +Model-Level : 2483.0 +Problems : 18 (Average Length: 37.00 Splits: 0) +Lemmas : 458956 (Deleted: 427121) + Binary : 3405 (Ratio: 0.74%) + Ternary : 3283 (Ratio: 0.72%) + Conflict : 458956 (Average Length: 1302.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 458956 (Average: 47.86 Max: 4236 Sum: 21965539) + Executed : 458806 (Average: 47.85 Max: 4236 Sum: 21960961 Ratio: 99.98%) + Bounded : 150 (Average: 30.52 Max: 37 Sum: 4578 Ratio: 0.02%) + +Rules : 482958 (Original: 482854) +Atoms : 12443 +Bodies : 318208 (Original: 318104) + Count : 1137 (Original: 1148) +Equivalences : 162277 (Atom=Atom: 48 Body=Body: 0 Other: 162229) +Tight : Yes +Variables : 216990 (Eliminated: 0 Frozen: 181320) +Constraints : 1914664 (Binary: 97.8% Ternary: 1.0% Other: 1.2%) + +Memory Peak : 685MB +Max. Length : 35 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 22.07s +Memory: 621MB (+0MB) +UNKNOWN +Iteration Time: 22.07s + +Iteration 18 +Queue: [(0,35,17,True)] +Grounded Until: 35 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 19 +Time : 533.888s (Solving: 525.03s 1st Model: 0.19s Unsat: 0.00s) +CPU Time : 533.932s + +Choices : 24999411 (Domain: 24999387) +Conflicts : 486351 (Analyzed: 486351) +Restarts : 1802 (Average: 269.90 Last: 542) +Model-Level : 2483.0 +Problems : 19 (Average Length: 37.00 Splits: 0) +Lemmas : 486351 (Deleted: 451484) + Binary : 3504 (Ratio: 0.72%) + Ternary : 3414 (Ratio: 0.70%) + Conflict : 486351 (Average Length: 1299.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 486351 (Average: 46.84 Max: 4236 Sum: 22778975) + Executed : 486200 (Average: 46.83 Max: 4236 Sum: 22774396 Ratio: 99.98%) + Bounded : 151 (Average: 30.32 Max: 37 Sum: 4579 Ratio: 0.02%) + +Rules : 482958 (Original: 482854) +Atoms : 12443 +Bodies : 318208 (Original: 318104) + Count : 1137 (Original: 1148) +Equivalences : 162277 (Atom=Atom: 48 Body=Body: 0 Other: 162229) +Tight : Yes +Variables : 216990 (Eliminated: 0 Frozen: 181320) +Constraints : 1914664 (Binary: 97.8% Ternary: 1.0% Other: 1.2%) + +Memory Peak : 685MB +Max. Length : 35 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 25.23s +Memory: 621MB (+0MB) +UNKNOWN +Iteration Time: 25.24s + +Iteration 19 +Queue: [(0,35,18,True)] +Grounded Until: 35 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 20 +Time : 557.377s (Solving: 548.45s 1st Model: 0.19s Unsat: 0.00s) +CPU Time : 557.428s + +Choices : 25614063 (Domain: 25614039) +Conflicts : 513723 (Analyzed: 513723) +Restarts : 1902 (Average: 270.10 Last: 542) +Model-Level : 2483.0 +Problems : 20 (Average Length: 37.00 Splits: 0) +Lemmas : 513723 (Deleted: 478126) + Binary : 3579 (Ratio: 0.70%) + Ternary : 3481 (Ratio: 0.68%) + Conflict : 513723 (Average Length: 1312.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 513723 (Average: 45.28 Max: 4236 Sum: 23259209) + Executed : 513572 (Average: 45.27 Max: 4236 Sum: 23254630 Ratio: 99.98%) + Bounded : 151 (Average: 30.32 Max: 37 Sum: 4579 Ratio: 0.02%) + +Rules : 482958 (Original: 482854) +Atoms : 12443 +Bodies : 318208 (Original: 318104) + Count : 1137 (Original: 1148) +Equivalences : 162277 (Atom=Atom: 48 Body=Body: 0 Other: 162229) +Tight : Yes +Variables : 216990 (Eliminated: 0 Frozen: 181320) +Constraints : 1914664 (Binary: 97.8% Ternary: 1.0% Other: 1.2%) + +Memory Peak : 685MB +Max. Length : 35 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 23.50s +Memory: 621MB (+0MB) +UNKNOWN +Iteration Time: 23.50s + +Iteration 20 +Queue: [(0,35,19,True)] +Grounded Until: 35 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 21 +Time : 580.249s (Solving: 571.25s 1st Model: 0.19s Unsat: 0.00s) +CPU Time : 580.312s + +Choices : 26243658 (Domain: 26243634) +Conflicts : 540323 (Analyzed: 540323) +Restarts : 2002 (Average: 269.89 Last: 542) +Model-Level : 2483.0 +Problems : 21 (Average Length: 37.00 Splits: 0) +Lemmas : 540323 (Deleted: 504816) + Binary : 3634 (Ratio: 0.67%) + Ternary : 3537 (Ratio: 0.65%) + Conflict : 540323 (Average Length: 1320.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 540323 (Average: 43.94 Max: 4236 Sum: 23743359) + Executed : 540169 (Average: 43.93 Max: 4236 Sum: 23738777 Ratio: 99.98%) + Bounded : 154 (Average: 29.75 Max: 37 Sum: 4582 Ratio: 0.02%) + +Rules : 482958 (Original: 482854) +Atoms : 12443 +Bodies : 318208 (Original: 318104) + Count : 1137 (Original: 1148) +Equivalences : 162277 (Atom=Atom: 48 Body=Body: 0 Other: 162229) +Tight : Yes +Variables : 216990 (Eliminated: 0 Frozen: 181320) +Constraints : 1914664 (Binary: 97.8% Ternary: 1.0% Other: 1.2%) + +Memory Peak : 685MB +Max. Length : 35 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 22.88s +Memory: 621MB (+0MB) +UNKNOWN +Iteration Time: 22.88s + +Iteration 21 +Queue: [(0,35,20,True)] +Grounded Until: 35 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 22 +Time : 603.063s (Solving: 594.01s 1st Model: 0.19s Unsat: 0.00s) +CPU Time : 603.136s + +Choices : 26930145 (Domain: 26930121) +Conflicts : 564784 (Analyzed: 564784) +Restarts : 2102 (Average: 268.69 Last: 542) +Model-Level : 2483.0 +Problems : 22 (Average Length: 37.00 Splits: 0) +Lemmas : 564784 (Deleted: 527985) + Binary : 3688 (Ratio: 0.65%) + Ternary : 3581 (Ratio: 0.63%) + Conflict : 564784 (Average Length: 1329.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 564784 (Average: 43.01 Max: 4236 Sum: 24291955) + Executed : 564628 (Average: 43.00 Max: 4236 Sum: 24287335 Ratio: 99.98%) + Bounded : 156 (Average: 29.62 Max: 37 Sum: 4620 Ratio: 0.02%) + +Rules : 482958 (Original: 482854) +Atoms : 12443 +Bodies : 318208 (Original: 318104) + Count : 1137 (Original: 1148) +Equivalences : 162277 (Atom=Atom: 48 Body=Body: 0 Other: 162229) +Tight : Yes +Variables : 216990 (Eliminated: 0 Frozen: 181320) +Constraints : 1914664 (Binary: 97.8% Ternary: 1.0% Other: 1.2%) + +Memory Peak : 685MB +Max. Length : 35 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 22.83s +Memory: 621MB (+0MB) +UNKNOWN +Iteration Time: 22.83s + +Iteration 22 +Queue: [(0,35,21,True)] +Grounded Until: 35 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 23 +Time : 623.418s (Solving: 614.30s 1st Model: 0.19s Unsat: 0.00s) +CPU Time : 623.500s + +Choices : 27541313 (Domain: 27541289) +Conflicts : 587825 (Analyzed: 587825) +Restarts : 2202 (Average: 266.95 Last: 542) +Model-Level : 2483.0 +Problems : 23 (Average Length: 37.00 Splits: 0) +Lemmas : 587825 (Deleted: 551879) + Binary : 3745 (Ratio: 0.64%) + Ternary : 3648 (Ratio: 0.62%) + Conflict : 587825 (Average Length: 1331.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 587825 (Average: 42.12 Max: 4236 Sum: 24760832) + Executed : 587669 (Average: 42.11 Max: 4236 Sum: 24756212 Ratio: 99.98%) + Bounded : 156 (Average: 29.62 Max: 37 Sum: 4620 Ratio: 0.02%) + +Rules : 482958 (Original: 482854) +Atoms : 12443 +Bodies : 318208 (Original: 318104) + Count : 1137 (Original: 1148) +Equivalences : 162277 (Atom=Atom: 48 Body=Body: 0 Other: 162229) +Tight : Yes +Variables : 216990 (Eliminated: 0 Frozen: 181320) +Constraints : 1914652 (Binary: 97.8% Ternary: 1.0% Other: 1.2%) + +Memory Peak : 685MB +Max. Length : 35 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 20.37s +Memory: 621MB (+0MB) +UNKNOWN +Iteration Time: 20.37s + +Iteration 23 +Queue: [(0,35,22,True)] +Grounded Until: 35 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 24 +Time : 647.559s (Solving: 638.39s 1st Model: 0.19s Unsat: 0.00s) +CPU Time : 647.648s + +Choices : 28240574 (Domain: 28240550) +Conflicts : 616674 (Analyzed: 616674) +Restarts : 2302 (Average: 267.89 Last: 542) +Model-Level : 2483.0 +Problems : 24 (Average Length: 37.00 Splits: 0) +Lemmas : 616674 (Deleted: 579373) + Binary : 3899 (Ratio: 0.63%) + Ternary : 3786 (Ratio: 0.61%) + Conflict : 616674 (Average Length: 1344.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 616674 (Average: 41.03 Max: 4236 Sum: 25300609) + Executed : 616517 (Average: 41.02 Max: 4236 Sum: 25295952 Ratio: 99.98%) + Bounded : 157 (Average: 29.66 Max: 37 Sum: 4657 Ratio: 0.02%) + +Rules : 482958 (Original: 482854) +Atoms : 12443 +Bodies : 318208 (Original: 318104) + Count : 1137 (Original: 1148) +Equivalences : 162277 (Atom=Atom: 48 Body=Body: 0 Other: 162229) +Tight : Yes +Variables : 216990 (Eliminated: 0 Frozen: 181320) +Constraints : 1914652 (Binary: 97.8% Ternary: 1.0% Other: 1.2%) + +Memory Peak : 685MB +Max. Length : 35 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 24.15s +Memory: 621MB (+0MB) +UNKNOWN +Iteration Time: 24.15s + +Iteration 24 +Queue: [(0,35,23,True)] +Grounded Until: 35 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 25 +Time : 670.268s (Solving: 661.05s 1st Model: 0.19s Unsat: 0.00s) +CPU Time : 670.368s + +Choices : 28833349 (Domain: 28833325) +Conflicts : 645067 (Analyzed: 645067) +Restarts : 2402 (Average: 268.55 Last: 542) +Model-Level : 2483.0 +Problems : 25 (Average Length: 37.00 Splits: 0) +Lemmas : 645067 (Deleted: 606247) + Binary : 3946 (Ratio: 0.61%) + Ternary : 3861 (Ratio: 0.60%) + Conflict : 645067 (Average Length: 1357.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 645067 (Average: 39.92 Max: 4236 Sum: 25751338) + Executed : 644910 (Average: 39.91 Max: 4236 Sum: 25746681 Ratio: 99.98%) + Bounded : 157 (Average: 29.66 Max: 37 Sum: 4657 Ratio: 0.02%) + +Rules : 482958 (Original: 482854) +Atoms : 12443 +Bodies : 318208 (Original: 318104) + Count : 1137 (Original: 1148) +Equivalences : 162277 (Atom=Atom: 48 Body=Body: 0 Other: 162229) +Tight : Yes +Variables : 216990 (Eliminated: 0 Frozen: 181320) +Constraints : 1914590 (Binary: 97.8% Ternary: 1.0% Other: 1.2%) + +Memory Peak : 685MB +Max. Length : 35 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 22.72s +Memory: 621MB (+0MB) +UNKNOWN +Iteration Time: 22.72s + +Iteration 25 +Queue: [(0,35,24,True)] +Grounded Until: 35 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 26 +Time : 693.620s (Solving: 684.36s 1st Model: 0.19s Unsat: 0.00s) +CPU Time : 693.732s + +Choices : 29454752 (Domain: 29454728) +Conflicts : 673092 (Analyzed: 673092) +Restarts : 2502 (Average: 269.02 Last: 542) +Model-Level : 2483.0 +Problems : 26 (Average Length: 37.00 Splits: 0) +Lemmas : 673092 (Deleted: 634682) + Binary : 4087 (Ratio: 0.61%) + Ternary : 3942 (Ratio: 0.59%) + Conflict : 673092 (Average Length: 1366.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 673092 (Average: 38.98 Max: 4236 Sum: 26234674) + Executed : 672934 (Average: 38.97 Max: 4236 Sum: 26230016 Ratio: 99.98%) + Bounded : 158 (Average: 29.48 Max: 37 Sum: 4658 Ratio: 0.02%) + +Rules : 482958 (Original: 482854) +Atoms : 12443 +Bodies : 318208 (Original: 318104) + Count : 1137 (Original: 1148) +Equivalences : 162277 (Atom=Atom: 48 Body=Body: 0 Other: 162229) +Tight : Yes +Variables : 216990 (Eliminated: 0 Frozen: 181320) +Constraints : 1914590 (Binary: 97.8% Ternary: 1.0% Other: 1.2%) + +Memory Peak : 685MB +Max. Length : 35 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 23.37s +Memory: 621MB (+0MB) +UNKNOWN +Iteration Time: 23.37s + +Iteration 26 +Queue: [(0,35,25,True)] +Grounded Until: 35 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 27 +Time : 713.201s (Solving: 703.88s 1st Model: 0.19s Unsat: 0.00s) +CPU Time : 713.320s + +Choices : 29961334 (Domain: 29961310) +Conflicts : 695547 (Analyzed: 695547) +Restarts : 2602 (Average: 267.31 Last: 542) +Model-Level : 2483.0 +Problems : 27 (Average Length: 37.00 Splits: 0) +Lemmas : 695547 (Deleted: 656540) + Binary : 4117 (Ratio: 0.59%) + Ternary : 3969 (Ratio: 0.57%) + Conflict : 695547 (Average Length: 1368.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 695547 (Average: 38.26 Max: 4236 Sum: 26609476) + Executed : 695385 (Average: 38.25 Max: 4236 Sum: 26604670 Ratio: 99.98%) + Bounded : 162 (Average: 29.67 Max: 37 Sum: 4806 Ratio: 0.02%) + +Rules : 482958 (Original: 482854) +Atoms : 12443 +Bodies : 318208 (Original: 318104) + Count : 1137 (Original: 1148) +Equivalences : 162277 (Atom=Atom: 48 Body=Body: 0 Other: 162229) +Tight : Yes +Variables : 216990 (Eliminated: 0 Frozen: 181320) +Constraints : 1914590 (Binary: 97.8% Ternary: 1.0% Other: 1.2%) + +Memory Peak : 685MB +Max. Length : 35 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 19.59s +Memory: 621MB (+0MB) +UNKNOWN +Iteration Time: 19.59s + +Iteration 27 +Queue: [(0,35,26,True)] +Grounded Until: 35 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 28 +Time : 734.751s (Solving: 725.38s 1st Model: 0.19s Unsat: 0.00s) +CPU Time : 734.876s + +Choices : 30574275 (Domain: 30574251) +Conflicts : 720438 (Analyzed: 720438) +Restarts : 2702 (Average: 266.63 Last: 542) +Model-Level : 2483.0 +Problems : 28 (Average Length: 37.00 Splits: 0) +Lemmas : 720438 (Deleted: 680956) + Binary : 4197 (Ratio: 0.58%) + Ternary : 4046 (Ratio: 0.56%) + Conflict : 720438 (Average Length: 1372.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 720438 (Average: 37.58 Max: 4236 Sum: 27077141) + Executed : 720276 (Average: 37.58 Max: 4236 Sum: 27072335 Ratio: 99.98%) + Bounded : 162 (Average: 29.67 Max: 37 Sum: 4806 Ratio: 0.02%) + +Rules : 482958 (Original: 482854) +Atoms : 12443 +Bodies : 318208 (Original: 318104) + Count : 1137 (Original: 1148) +Equivalences : 162277 (Atom=Atom: 48 Body=Body: 0 Other: 162229) +Tight : Yes +Variables : 216990 (Eliminated: 0 Frozen: 181320) +Constraints : 1912870 (Binary: 97.8% Ternary: 1.0% Other: 1.2%) + +Memory Peak : 685MB +Max. Length : 35 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 21.56s +Memory: 621MB (+0MB) +UNKNOWN +Iteration Time: 21.56s + +Iteration 28 +Queue: [(0,35,27,True)] +Grounded Until: 35 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 29 +Time : 759.120s (Solving: 749.68s 1st Model: 0.19s Unsat: 0.00s) +CPU Time : 759.256s + +Choices : 31136210 (Domain: 31136186) +Conflicts : 747330 (Analyzed: 747330) +Restarts : 2802 (Average: 266.71 Last: 542) +Model-Level : 2483.0 +Problems : 29 (Average Length: 37.00 Splits: 0) +Lemmas : 747330 (Deleted: 705050) + Binary : 4253 (Ratio: 0.57%) + Ternary : 4084 (Ratio: 0.55%) + Conflict : 747330 (Average Length: 1377.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 747330 (Average: 36.81 Max: 4236 Sum: 27505506) + Executed : 747167 (Average: 36.80 Max: 4236 Sum: 27500663 Ratio: 99.98%) + Bounded : 163 (Average: 29.71 Max: 37 Sum: 4843 Ratio: 0.02%) + +Rules : 482958 (Original: 482854) +Atoms : 12443 +Bodies : 318208 (Original: 318104) + Count : 1137 (Original: 1148) +Equivalences : 162277 (Atom=Atom: 48 Body=Body: 0 Other: 162229) +Tight : Yes +Variables : 216990 (Eliminated: 0 Frozen: 181320) +Constraints : 1912870 (Binary: 97.8% Ternary: 1.0% Other: 1.2%) + +Memory Peak : 685MB +Max. Length : 35 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 24.38s +Memory: 621MB (+0MB) +UNKNOWN +Iteration Time: 24.38s + +Iteration 29 +Queue: [(0,35,28,True)] +Grounded Until: 35 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 30 +Time : 782.043s (Solving: 772.52s 1st Model: 0.19s Unsat: 0.00s) +CPU Time : 782.188s + +Choices : 31668474 (Domain: 31668450) +Conflicts : 774284 (Analyzed: 774284) +Restarts : 2902 (Average: 266.81 Last: 542) +Model-Level : 2483.0 +Problems : 30 (Average Length: 37.00 Splits: 0) +Lemmas : 774284 (Deleted: 731410) + Binary : 4372 (Ratio: 0.56%) + Ternary : 4152 (Ratio: 0.54%) + Conflict : 774284 (Average Length: 1400.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 774284 (Average: 36.02 Max: 4236 Sum: 27886633) + Executed : 774120 (Average: 36.01 Max: 4236 Sum: 27881753 Ratio: 99.98%) + Bounded : 164 (Average: 29.76 Max: 37 Sum: 4880 Ratio: 0.02%) + +Rules : 482958 (Original: 482854) +Atoms : 12443 +Bodies : 318208 (Original: 318104) + Count : 1137 (Original: 1148) +Equivalences : 162277 (Atom=Atom: 48 Body=Body: 0 Other: 162229) +Tight : Yes +Variables : 216990 (Eliminated: 0 Frozen: 181320) +Constraints : 1912858 (Binary: 97.8% Ternary: 1.0% Other: 1.2%) + +Memory Peak : 685MB +Max. Length : 35 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 22.93s +Memory: 621MB (+0MB) +UNKNOWN +Iteration Time: 22.93s + +Iteration 30 +Queue: [(0,35,29,True)] +Grounded Until: 35 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 31 +Time : 806.414s (Solving: 796.81s 1st Model: 0.19s Unsat: 0.00s) +CPU Time : 806.568s + +Choices : 32212167 (Domain: 32212143) +Conflicts : 803689 (Analyzed: 803689) +Restarts : 3002 (Average: 267.72 Last: 542) +Model-Level : 2483.0 +Problems : 31 (Average Length: 37.00 Splits: 0) +Lemmas : 803689 (Deleted: 759611) + Binary : 4460 (Ratio: 0.55%) + Ternary : 4225 (Ratio: 0.53%) + Conflict : 803689 (Average Length: 1407.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 803689 (Average: 35.19 Max: 4236 Sum: 28282702) + Executed : 803522 (Average: 35.18 Max: 4236 Sum: 28277711 Ratio: 99.98%) + Bounded : 167 (Average: 29.89 Max: 37 Sum: 4991 Ratio: 0.02%) + +Rules : 482958 (Original: 482854) +Atoms : 12443 +Bodies : 318208 (Original: 318104) + Count : 1137 (Original: 1148) +Equivalences : 162277 (Atom=Atom: 48 Body=Body: 0 Other: 162229) +Tight : Yes +Variables : 216990 (Eliminated: 0 Frozen: 181320) +Constraints : 1912760 (Binary: 97.8% Ternary: 1.0% Other: 1.2%) + +Memory Peak : 685MB +Max. Length : 35 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 24.38s +Memory: 621MB (+0MB) +UNKNOWN +Iteration Time: 24.38s + +Iteration 31 +Queue: [(0,35,30,True)] +Grounded Until: 35 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 32 +Time : 834.197s (Solving: 824.53s 1st Model: 0.19s Unsat: 0.00s) +CPU Time : 834.360s + +Choices : 32869485 (Domain: 32869461) +Conflicts : 831984 (Analyzed: 831984) +Restarts : 3102 (Average: 268.21 Last: 542) +Model-Level : 2483.0 +Problems : 32 (Average Length: 37.00 Splits: 0) +Lemmas : 831984 (Deleted: 788502) + Binary : 4614 (Ratio: 0.55%) + Ternary : 4330 (Ratio: 0.52%) + Conflict : 831984 (Average Length: 1420.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 831984 (Average: 34.60 Max: 4236 Sum: 28785801) + Executed : 831815 (Average: 34.59 Max: 4236 Sum: 28780808 Ratio: 99.98%) + Bounded : 169 (Average: 29.54 Max: 37 Sum: 4993 Ratio: 0.02%) + +Rules : 482958 (Original: 482854) +Atoms : 12443 +Bodies : 318208 (Original: 318104) + Count : 1137 (Original: 1148) +Equivalences : 162277 (Atom=Atom: 48 Body=Body: 0 Other: 162229) +Tight : Yes +Variables : 216990 (Eliminated: 0 Frozen: 181320) +Constraints : 1912041 (Binary: 97.8% Ternary: 1.0% Other: 1.2%) + +Memory Peak : 685MB +Max. Length : 35 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 27.80s +Memory: 621MB (+0MB) +UNKNOWN +Iteration Time: 27.80s + +Iteration 32 +Queue: [(0,35,31,True)] +Grounded Until: 35 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 33 +Time : 859.343s (Solving: 849.63s 1st Model: 0.19s Unsat: 0.00s) +CPU Time : 859.516s + +Choices : 33454989 (Domain: 33454965) +Conflicts : 860485 (Analyzed: 860485) +Restarts : 3202 (Average: 268.73 Last: 542) +Model-Level : 2483.0 +Problems : 33 (Average Length: 37.00 Splits: 0) +Lemmas : 860485 (Deleted: 815642) + Binary : 4731 (Ratio: 0.55%) + Ternary : 4385 (Ratio: 0.51%) + Conflict : 860485 (Average Length: 1428.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 860485 (Average: 33.96 Max: 4236 Sum: 29221017) + Executed : 860316 (Average: 33.95 Max: 4236 Sum: 29216024 Ratio: 99.98%) + Bounded : 169 (Average: 29.54 Max: 37 Sum: 4993 Ratio: 0.02%) + +Rules : 482958 (Original: 482854) +Atoms : 12443 +Bodies : 318208 (Original: 318104) + Count : 1137 (Original: 1148) +Equivalences : 162277 (Atom=Atom: 48 Body=Body: 0 Other: 162229) +Tight : Yes +Variables : 216990 (Eliminated: 0 Frozen: 181320) +Constraints : 1912041 (Binary: 97.8% Ternary: 1.0% Other: 1.2%) + +Memory Peak : 685MB +Max. Length : 35 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 25.16s +Memory: 621MB (+0MB) +UNKNOWN +Iteration Time: 25.16s + +Iteration 33 +Queue: [(0,35,32,True)] +Grounded Until: 35 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 34 +Time : 886.061s (Solving: 876.29s 1st Model: 0.19s Unsat: 0.00s) +CPU Time : 886.244s + +Choices : 34011774 (Domain: 34011750) +Conflicts : 890019 (Analyzed: 890019) +Restarts : 3302 (Average: 269.54 Last: 542) +Model-Level : 2483.0 +Problems : 34 (Average Length: 37.00 Splits: 0) +Lemmas : 890019 (Deleted: 843327) + Binary : 4809 (Ratio: 0.54%) + Ternary : 4427 (Ratio: 0.50%) + Conflict : 890019 (Average Length: 1430.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 890019 (Average: 33.30 Max: 4236 Sum: 29634994) + Executed : 889850 (Average: 33.29 Max: 4236 Sum: 29630001 Ratio: 99.98%) + Bounded : 169 (Average: 29.54 Max: 37 Sum: 4993 Ratio: 0.02%) + +Rules : 482958 (Original: 482854) +Atoms : 12443 +Bodies : 318208 (Original: 318104) + Count : 1137 (Original: 1148) +Equivalences : 162277 (Atom=Atom: 48 Body=Body: 0 Other: 162229) +Tight : Yes +Variables : 216990 (Eliminated: 0 Frozen: 181320) +Constraints : 1912041 (Binary: 97.8% Ternary: 1.0% Other: 1.2%) + +Memory Peak : 685MB +Max. Length : 35 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 26.73s +Memory: 621MB (+0MB) +UNKNOWN +Iteration Time: 26.73s + +Iteration 34 +Queue: [(0,35,33,True)] +Grounded Until: 35 +Solving... +*** Info : (planner): INTERRUPTED by signal! +UNKNOWN + +INTERRUPTED : 1 + +Models : 0+ +Calls : 35 +Time : 912.171s (Solving: 902.35s 1st Model: 0.19s Unsat: 0.00s) +CPU Time : 912.348s + +Choices : 34615184 (Domain: 34615160) +Conflicts : 919629 (Analyzed: 919629) +Restarts : 3402 (Average: 270.32 Last: 542) +Model-Level : 2483.0 +Problems : 35 (Average Length: 37.00 Splits: 0) +Lemmas : 919629 (Deleted: 872085) + Binary : 4880 (Ratio: 0.53%) + Ternary : 4472 (Ratio: 0.49%) + Conflict : 919629 (Average Length: 1433.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 919629 (Average: 32.72 Max: 4236 Sum: 30092001) + Executed : 919460 (Average: 32.72 Max: 4236 Sum: 30087008 Ratio: 99.98%) + Bounded : 169 (Average: 29.54 Max: 37 Sum: 4993 Ratio: 0.02%) + +Rules : 482958 (Original: 482854) +Atoms : 12443 +Bodies : 318208 (Original: 318104) + Count : 1137 (Original: 1148) +Equivalences : 162277 (Atom=Atom: 48 Body=Body: 0 Other: 162229) +Tight : Yes +Variables : 216990 (Eliminated: 0 Frozen: 181320) +Constraints : 1912041 (Binary: 97.8% Ternary: 1.0% Other: 1.2%) + +Memory Peak : 685MB +Max. Length : 35 steps +Models : 1 + +