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