INFO Running translator. INFO translator input: ['/home/pluehne/Documents/ASP/pddl-instances/ipc-2011/domains/barman-sequential-satisficing/domain.pddl', '/home/pluehne/Documents/ASP/pddl-instances/ipc-2011/domains/barman-sequential-satisficing/instances/instance-15.pddl'] INFO translator arguments: [] INFO translator time limit: None INFO translator memory limit: None INFO callstring: /home/pluehne/.usr/bin/python /home/wv/bin/linux/64/fast-downward-10997/builds/release64/bin/translate/translate.py /home/pluehne/Documents/ASP/pddl-instances/ipc-2011/domains/barman-sequential-satisficing/domain.pddl /home/pluehne/Documents/ASP/pddl-instances/ipc-2011/domains/barman-sequential-satisficing/instances/instance-15.pddl Parsing... Parsing: [0.030s CPU, 0.031s wall-clock] Normalizing task... [0.000s CPU, 0.002s wall-clock] Instantiating... Generating Datalog program... [0.010s CPU, 0.008s wall-clock] Normalizing Datalog program... Normalizing Datalog program: [0.040s CPU, 0.041s wall-clock] Preparing model... [0.030s CPU, 0.024s wall-clock] Generated 115 rules. Computing model... [0.500s CPU, 0.504s wall-clock] 3094 relevant atoms 3221 auxiliary atoms 6315 final queue length 10878 total queue pushes Completing instantiation... [0.960s CPU, 0.962s wall-clock] Instantiating: [1.550s CPU, 1.547s wall-clock] Computing fact groups... Finding invariants... 24 initial candidates Finding invariants: [0.110s CPU, 0.112s wall-clock] Checking invariant weight... [0.000s CPU, 0.001s wall-clock] Instantiating groups... [0.010s CPU, 0.009s wall-clock] Collecting mutex groups... [0.010s CPU, 0.001s wall-clock] Choosing groups... 328 uncovered facts Choosing groups: [0.000s CPU, 0.002s wall-clock] Building translation key... [0.010s CPU, 0.012s wall-clock] Computing fact groups: [0.160s CPU, 0.163s wall-clock] Building STRIPS to SAS dictionary... [0.010s CPU, 0.003s wall-clock] Building dictionary for full mutex groups... [0.000s CPU, 0.003s 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.051s wall-clock] Translating task: [1.000s CPU, 0.996s wall-clock] 3672 effect conditions simplified 0 implied preconditions added Detecting unreachable propositions... 0 operators removed 0 axioms removed 3 propositions removed Detecting unreachable propositions: [0.490s CPU, 0.490s wall-clock] Reordering and filtering variables... 331 of 331 variables necessary. 15 of 18 mutex groups necessary. 2194 of 2194 operators necessary. 0 of 0 axiom rules necessary. Reordering and filtering variables: [0.400s CPU, 0.401s wall-clock] Translator variables: 331 Translator derived variables: 0 Translator facts: 691 Translator goal facts: 13 Translator mutex groups: 15 Translator total mutex groups size: 45 Translator operators: 2194 Translator axioms: 0 Translator task size: 21018 Translator peak memory: 48332 KB Writing output... [0.400s CPU, 0.441s wall-clock] Done! [4.080s CPU, 4.121s wall-clock] planner.py version 0.0.1 Time: 0.85s Memory: 107MB Iteration 1 Queue: [(0,0,0,True), (1,5,0,True), (2,10,0,True), (3,15,0,True), (4,20,0,True), (5,25,0,True), (6,30,0,True)] Grounded Until: 0 Solving... [start: stats after solve call] Models : 0 Calls : 1 Time : 0.985s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s) CPU Time : 0.852s Choices : 0 Conflicts : 0 (Analyzed: 0) Restarts : 0 Problems : 1 (Average Length: 2.00 Splits: 0) Lemmas : 0 (Deleted: 0) Binary : 0 (Ratio: 0.00%) Ternary : 0 (Ratio: 0.00%) Conflict : 0 (Average Length: 0.0 Ratio: 0.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 0 (Average: 0.00 Max: 0 Sum: 0) Executed : 0 (Average: 0.00 Max: 0 Sum: 0 Ratio: 0.00%) Bounded : 0 (Average: 0.00 Max: 0 Sum: 0 Ratio: 100.00%) Rules : 60629 Atoms : 60629 Bodies : 1 (Original: 0) Tight : Yes Variables : 0 (Eliminated: 0 Frozen: 0) Constraints : 0 (Binary: 0.0% Ternary: 0.0% Other: 0.0%) Memory Peak : 243MB Max. Length : 0 steps Models : 0 [endof: stats after solve call] Solving Time: 0.01s Memory: 179MB (+72MB) UNSAT Iteration Time: 0.01s Iteration 2 Queue: [(1,5,0,True), (2,10,0,True), (3,15,0,True), (4,20,0,True), (5,25,0,True), (6,30,0,True)] Grounded Until: 0 Expected Memory: 179MB Grounding... [('step', [1]), ('step', [2]), ('step', [3]), ('step', [4]), ('step', [5]), ('check', [5])] Grounding Time: 0.26s Memory: 179MB (+0MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0 Calls : 2 Time : 1.393s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s) CPU Time : 1.260s Choices : 328 (Domain: 271) Conflicts : 52 (Analyzed: 51) Restarts : 0 Problems : 2 (Average Length: 4.50 Splits: 0) Lemmas : 51 (Deleted: 0) Binary : 20 (Ratio: 39.22%) Ternary : 2 (Ratio: 3.92%) Conflict : 51 (Average Length: 5.1 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 51 (Average: 6.47 Max: 37 Sum: 330) Executed : 49 (Average: 6.43 Max: 37 Sum: 328 Ratio: 99.39%) Bounded : 2 (Average: 1.00 Max: 1 Sum: 2 Ratio: 0.61%) Rules : 60629 Atoms : 60629 Bodies : 1 (Original: 0) Tight : Yes Variables : 16256 (Eliminated: 0 Frozen: 160) Constraints : 53667 (Binary: 95.3% Ternary: 3.3% Other: 1.4%) Memory Peak : 243MB Max. Length : 0 steps Models : 0 [endof: stats after solve call] Solving Time: 0.02s Memory: 183MB (+4MB) UNSAT Iteration Time: 0.41s Iteration 3 Queue: [(2,10,0,True), (3,15,0,True), (4,20,0,True), (5,25,0,True), (6,30,0,True)] Grounded Until: 5 Expected Memory: 187.0MB Grounding... [('step', [6]), ('step', [7]), ('step', [8]), ('step', [9]), ('step', [10]), ('check', [10])] Grounding Time: 0.31s Memory: 190MB (+7MB) Unblocking actions... Solving... [start: stats after solve call] Models : 1+ Calls : 3 Time : 1.924s (Solving: 0.08s 1st Model: 0.07s Unsat: 0.00s) CPU Time : 1.788s Choices : 2349 (Domain: 2154) Conflicts : 334 (Analyzed: 333) Restarts : 2 (Average: 166.50 Last: 62) Model-Level : 251.0 Problems : 3 (Average Length: 7.00 Splits: 0) Lemmas : 333 (Deleted: 0) Binary : 70 (Ratio: 21.02%) Ternary : 10 (Ratio: 3.00%) Conflict : 333 (Average Length: 182.2 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 333 (Average: 6.20 Max: 132 Sum: 2065) Executed : 331 (Average: 6.20 Max: 132 Sum: 2063 Ratio: 99.90%) Bounded : 2 (Average: 1.00 Max: 1 Sum: 2 Ratio: 0.10%) Rules : 60629 Atoms : 60629 Bodies : 1 (Original: 0) Tight : Yes Variables : 35632 (Eliminated: 0 Frozen: 320) Constraints : 211962 (Binary: 95.6% Ternary: 3.2% Other: 1.2%) Memory Peak : 243MB Max. Length : 5 steps Models : 1 [endof: stats after solve call] Solving Time: 0.09s Memory: 198MB (+8MB) SAT Testing... NOT SERIALIZABLE Testing Time: 1.08s Memory: 232MB (+34MB) Solving... [start: stats after solve call] Models : 0 Calls : 4 Time : 2.542s (Solving: 0.36s 1st Model: 0.07s Unsat: 0.29s) CPU Time : 2.408s Choices : 9441 (Domain: 7693) Conflicts : 972 (Analyzed: 970) Restarts : 10 (Average: 97.00 Last: 62) Model-Level : 251.0 Problems : 4 (Average Length: 8.25 Splits: 0) Lemmas : 970 (Deleted: 0) Binary : 215 (Ratio: 22.16%) Ternary : 73 (Ratio: 7.53%) Conflict : 970 (Average Length: 87.8 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 970 (Average: 9.43 Max: 132 Sum: 9151) Executed : 963 (Average: 9.39 Max: 132 Sum: 9111 Ratio: 99.56%) Bounded : 7 (Average: 5.71 Max: 12 Sum: 40 Ratio: 0.44%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 56254 (Eliminated: 0 Frozen: 15821) Constraints : 347145 (Binary: 91.4% Ternary: 7.0% Other: 1.7%) Memory Peak : 243MB Max. Length : 5 steps Models : 1 [endof: stats after solve call] Solving Time: 0.37s Memory: 232MB (+0MB) UNSAT Iteration Time: 1.99s Iteration 4 Queue: [(3,15,0,True), (4,20,0,True), (5,25,0,True), (6,30,0,True)] Grounded Until: 10 Expected Memory: 247.0MB Grounding... [('step', [11]), ('step', [12]), ('step', [13]), ('step', [14]), ('step', [15]), ('check', [15])] Grounding Time: 0.50s Memory: 234MB (+2MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 5 Time : 7.321s (Solving: 4.40s 1st Model: 0.07s Unsat: 0.29s) CPU Time : 7.188s Choices : 103274 (Domain: 83893) Conflicts : 10049 (Analyzed: 10047) Restarts : 110 (Average: 91.34 Last: 82) Model-Level : 251.0 Problems : 5 (Average Length: 10.00 Splits: 0) Lemmas : 10047 (Deleted: 5861) Binary : 934 (Ratio: 9.30%) Ternary : 431 (Ratio: 4.29%) Conflict : 10047 (Average Length: 173.3 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 10047 (Average: 9.91 Max: 328 Sum: 99516) Executed : 10030 (Average: 9.88 Max: 328 Sum: 99309 Ratio: 99.79%) Bounded : 17 (Average: 12.18 Max: 17 Sum: 207 Ratio: 0.21%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 93745 (Eliminated: 0 Frozen: 27481) Constraints : 624347 (Binary: 91.3% Ternary: 7.0% Other: 1.7%) Memory Peak : 257MB Max. Length : 10 steps Models : 1 [endof: stats after solve call] Solving Time: 4.07s Memory: 257MB (+23MB) UNKNOWN Iteration Time: 4.79s Iteration 5 Queue: [(4,20,0,True), (5,25,0,True), (6,30,0,True)] Grounded Until: 15 Expected Memory: 282.0MB Grounding... [('step', [16]), ('step', [17]), ('step', [18]), ('step', [19]), ('step', [20]), ('check', [20])] Grounding Time: 0.51s Memory: 260MB (+3MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 6 Time : 13.330s (Solving: 9.64s 1st Model: 0.07s Unsat: 0.29s) CPU Time : 13.196s Choices : 195626 (Domain: 161158) Conflicts : 18931 (Analyzed: 18929) Restarts : 210 (Average: 90.14 Last: 147) Model-Level : 251.0 Problems : 6 (Average Length: 12.00 Splits: 0) Lemmas : 18929 (Deleted: 13925) Binary : 1451 (Ratio: 7.67%) Ternary : 525 (Ratio: 2.77%) Conflict : 18929 (Average Length: 627.6 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 18929 (Average: 9.70 Max: 328 Sum: 183697) Executed : 18912 (Average: 9.69 Max: 328 Sum: 183490 Ratio: 99.89%) Bounded : 17 (Average: 12.18 Max: 17 Sum: 207 Ratio: 0.11%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 131236 (Eliminated: 0 Frozen: 39141) Constraints : 896242 (Binary: 91.3% Ternary: 6.9% Other: 1.8%) Memory Peak : 280MB Max. Length : 15 steps Models : 1 [endof: stats after solve call] Solving Time: 5.27s Memory: 276MB (+16MB) UNKNOWN Iteration Time: 6.02s Iteration 6 Queue: [(5,25,0,True), (6,30,0,True)] Grounded Until: 20 Expected Memory: 301.0MB Grounding... [('step', [21]), ('step', [22]), ('step', [23]), ('step', [24]), ('step', [25]), ('check', [25])] Grounding Time: 0.68s Memory: 297MB (+21MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 7 Time : 20.219s (Solving: 15.46s 1st Model: 0.07s Unsat: 0.29s) CPU Time : 20.088s Choices : 312221 (Domain: 262527) Conflicts : 27833 (Analyzed: 27831) Restarts : 310 (Average: 89.78 Last: 147) Model-Level : 251.0 Problems : 7 (Average Length: 14.14 Splits: 0) Lemmas : 27831 (Deleted: 22272) Binary : 1738 (Ratio: 6.24%) Ternary : 551 (Ratio: 1.98%) Conflict : 27831 (Average Length: 876.2 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 27831 (Average: 10.39 Max: 328 Sum: 289195) Executed : 27814 (Average: 10.38 Max: 328 Sum: 288988 Ratio: 99.93%) Bounded : 17 (Average: 12.18 Max: 17 Sum: 207 Ratio: 0.07%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 168727 (Eliminated: 0 Frozen: 50801) Constraints : 1178702 (Binary: 91.3% Ternary: 7.0% Other: 1.8%) Memory Peak : 321MB Max. Length : 20 steps Models : 1 [endof: stats after solve call] Solving Time: 5.89s Memory: 309MB (+12MB) UNKNOWN Iteration Time: 6.90s Iteration 7 Queue: [(6,30,0,True)] Grounded Until: 25 Expected Memory: 342.0MB Grounding... [('step', [26]), ('step', [27]), ('step', [28]), ('step', [29]), ('step', [30]), ('check', [30])] Grounding Time: 0.55s Memory: 320MB (+11MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 8 Time : 27.651s (Solving: 22.03s 1st Model: 0.07s Unsat: 0.29s) CPU Time : 27.524s Choices : 479799 (Domain: 417037) Conflicts : 37022 (Analyzed: 37020) Restarts : 410 (Average: 90.29 Last: 147) Model-Level : 251.0 Problems : 8 (Average Length: 16.38 Splits: 0) Lemmas : 37020 (Deleted: 30710) Binary : 2027 (Ratio: 5.48%) Ternary : 575 (Ratio: 1.55%) Conflict : 37020 (Average Length: 983.7 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 37020 (Average: 12.01 Max: 328 Sum: 444719) Executed : 37003 (Average: 12.01 Max: 328 Sum: 444512 Ratio: 99.95%) Bounded : 17 (Average: 12.18 Max: 17 Sum: 207 Ratio: 0.05%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 206218 (Eliminated: 0 Frozen: 62461) Constraints : 1461162 (Binary: 91.3% Ternary: 7.0% Other: 1.8%) Memory Peak : 351MB Max. Length : 25 steps Models : 1 [endof: stats after solve call] Solving Time: 6.62s Memory: 351MB (+31MB) UNKNOWN Iteration Time: 7.44s Iteration 8 Queue: [(3,15,1,True), (4,20,1,True), (5,25,1,True), (6,30,1,True), (7,35,0,True), (8,40,0,True), (9,45,0,True), (10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True)] Grounded Until: 30 Blocking actions... Solving... [start: stats after solve call] Models : 0 Calls : 9 Time : 33.602s (Solving: 27.92s 1st Model: 0.07s Unsat: 6.19s) CPU Time : 33.476s Choices : 572044 (Domain: 497302) Conflicts : 45447 (Analyzed: 45444) Restarts : 507 (Average: 89.63 Last: 147) Model-Level : 251.0 Problems : 9 (Average Length: 18.11 Splits: 0) Lemmas : 45444 (Deleted: 36473) Binary : 2700 (Ratio: 5.94%) Ternary : 694 (Ratio: 1.53%) Conflict : 45444 (Average Length: 832.4 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 45444 (Average: 11.77 Max: 328 Sum: 534686) Executed : 45406 (Average: 11.75 Max: 328 Sum: 533812 Ratio: 99.84%) Bounded : 38 (Average: 23.00 Max: 32 Sum: 874 Ratio: 0.16%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 206218 (Eliminated: 0 Frozen: 62461) Constraints : 1461162 (Binary: 91.3% Ternary: 7.0% Other: 1.8%) Memory Peak : 351MB Max. Length : 30 steps Models : 1 [endof: stats after solve call] Solving Time: 5.94s Memory: 351MB (+0MB) UNSAT Iteration Time: 5.96s Iteration 9 Queue: [(4,20,1,True), (5,25,1,True), (6,30,1,True), (7,35,0,True), (8,40,0,True), (9,45,0,True), (10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True)] Grounded Until: 30 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 10 Time : 40.287s (Solving: 34.56s 1st Model: 0.07s Unsat: 6.19s) CPU Time : 40.164s Choices : 683784 (Domain: 598350) Conflicts : 54404 (Analyzed: 54401) Restarts : 607 (Average: 89.62 Last: 147) Model-Level : 251.0 Problems : 10 (Average Length: 19.50 Splits: 0) Lemmas : 54401 (Deleted: 44132) Binary : 3401 (Ratio: 6.25%) Ternary : 902 (Ratio: 1.66%) Conflict : 54401 (Average Length: 721.3 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 54401 (Average: 11.81 Max: 328 Sum: 642270) Executed : 54339 (Average: 11.78 Max: 328 Sum: 640633 Ratio: 99.75%) Bounded : 62 (Average: 26.40 Max: 32 Sum: 1637 Ratio: 0.25%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 206218 (Eliminated: 0 Frozen: 62461) Constraints : 1421811 (Binary: 91.3% Ternary: 6.9% Other: 1.8%) Memory Peak : 351MB Max. Length : 30 steps Models : 1 [endof: stats after solve call] Solving Time: 6.67s Memory: 351MB (+0MB) UNKNOWN Iteration Time: 6.69s Iteration 10 Queue: [(5,25,1,True), (6,30,1,True), (7,35,0,True), (8,40,0,True), (9,45,0,True), (10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True)] Grounded Until: 30 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 11 Time : 46.293s (Solving: 40.52s 1st Model: 0.07s Unsat: 6.19s) CPU Time : 46.176s Choices : 781906 (Domain: 687551) Conflicts : 62886 (Analyzed: 62883) Restarts : 707 (Average: 88.94 Last: 147) Model-Level : 251.0 Problems : 11 (Average Length: 20.64 Splits: 0) Lemmas : 62883 (Deleted: 50567) Binary : 3689 (Ratio: 5.87%) Ternary : 961 (Ratio: 1.53%) Conflict : 62883 (Average Length: 655.6 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 62883 (Average: 11.65 Max: 328 Sum: 732627) Executed : 62808 (Average: 11.62 Max: 328 Sum: 730579 Ratio: 99.72%) Bounded : 75 (Average: 27.31 Max: 32 Sum: 2048 Ratio: 0.28%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 206218 (Eliminated: 0 Frozen: 62461) Constraints : 1395626 (Binary: 91.3% Ternary: 6.9% Other: 1.8%) Memory Peak : 351MB Max. Length : 30 steps Models : 1 [endof: stats after solve call] Solving Time: 5.99s Memory: 351MB (+0MB) UNKNOWN Iteration Time: 6.01s Iteration 11 Queue: [(6,30,1,True), (7,35,0,True), (8,40,0,True), (9,45,0,True), (10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True)] Grounded Until: 30 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 12 Time : 52.276s (Solving: 46.46s 1st Model: 0.07s Unsat: 6.19s) CPU Time : 52.160s Choices : 909194 (Domain: 808893) Conflicts : 71442 (Analyzed: 71439) Restarts : 807 (Average: 88.52 Last: 147) Model-Level : 251.0 Problems : 12 (Average Length: 21.58 Splits: 0) Lemmas : 71439 (Deleted: 58311) Binary : 4029 (Ratio: 5.64%) Ternary : 1035 (Ratio: 1.45%) Conflict : 71439 (Average Length: 611.0 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 71439 (Average: 11.91 Max: 335 Sum: 850558) Executed : 71357 (Average: 11.87 Max: 335 Sum: 848286 Ratio: 99.73%) Bounded : 82 (Average: 27.71 Max: 32 Sum: 2272 Ratio: 0.27%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 206218 (Eliminated: 0 Frozen: 62461) Constraints : 1395295 (Binary: 91.3% Ternary: 6.9% Other: 1.8%) Memory Peak : 351MB Max. Length : 30 steps Models : 1 [endof: stats after solve call] Solving Time: 5.97s Memory: 351MB (+0MB) UNKNOWN Iteration Time: 5.99s Iteration 12 Queue: [(7,35,0,True), (8,40,0,True), (9,45,0,True), (10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True)] Grounded Until: 30 Expected Memory: 393.0MB Grounding... [('step', [31]), ('step', [32]), ('step', [33]), ('step', [34]), ('step', [35]), ('check', [35])] Grounding Time: 0.56s Memory: 351MB (+0MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 13 Time : 60.308s (Solving: 53.58s 1st Model: 0.07s Unsat: 6.19s) CPU Time : 60.196s Choices : 1157175 (Domain: 1048177) Conflicts : 80479 (Analyzed: 80476) Restarts : 907 (Average: 88.73 Last: 156) Model-Level : 251.0 Problems : 13 (Average Length: 22.77 Splits: 0) Lemmas : 80476 (Deleted: 69453) Binary : 4441 (Ratio: 5.52%) Ternary : 1051 (Ratio: 1.31%) Conflict : 80476 (Average Length: 617.5 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 80476 (Average: 13.49 Max: 335 Sum: 1085595) Executed : 80394 (Average: 13.46 Max: 335 Sum: 1083323 Ratio: 99.79%) Bounded : 82 (Average: 27.71 Max: 32 Sum: 2272 Ratio: 0.21%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 243709 (Eliminated: 0 Frozen: 74121) Constraints : 1672459 (Binary: 91.3% Ternary: 6.9% Other: 1.8%) Memory Peak : 387MB Max. Length : 30 steps Models : 1 [endof: stats after solve call] Solving Time: 7.19s Memory: 365MB (+14MB) UNKNOWN Iteration Time: 8.05s Iteration 13 Queue: [(8,40,0,True), (9,45,0,True), (10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True)] Grounded Until: 35 Expected Memory: 407.0MB Grounding... [('step', [36]), ('step', [37]), ('step', [38]), ('step', [39]), ('step', [40]), ('check', [40])] Grounding Time: 0.55s Memory: 373MB (+8MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 14 Time : 67.826s (Solving: 60.19s 1st Model: 0.07s Unsat: 6.19s) CPU Time : 67.716s Choices : 1371177 (Domain: 1254940) Conflicts : 89370 (Analyzed: 89367) Restarts : 1007 (Average: 88.75 Last: 156) Model-Level : 251.0 Problems : 14 (Average Length: 24.14 Splits: 0) Lemmas : 89367 (Deleted: 78148) Binary : 4597 (Ratio: 5.14%) Ternary : 1053 (Ratio: 1.18%) Conflict : 89367 (Average Length: 640.8 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 89367 (Average: 14.37 Max: 335 Sum: 1283888) Executed : 89285 (Average: 14.34 Max: 335 Sum: 1281616 Ratio: 99.82%) Bounded : 82 (Average: 27.71 Max: 32 Sum: 2272 Ratio: 0.18%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 281200 (Eliminated: 0 Frozen: 85781) Constraints : 1954919 (Binary: 91.3% Ternary: 6.9% Other: 1.8%) Memory Peak : 412MB Max. Length : 35 steps Models : 1 [endof: stats after solve call] Solving Time: 6.68s Memory: 388MB (+15MB) UNKNOWN Iteration Time: 7.53s Iteration 14 Queue: [(9,45,0,True), (10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True)] Grounded Until: 40 Expected Memory: 430.0MB Grounding... [('step', [41]), ('step', [42]), ('step', [43]), ('step', [44]), ('step', [45]), ('check', [45])] Grounding Time: 0.54s Memory: 398MB (+10MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 15 Time : 75.260s (Solving: 66.71s 1st Model: 0.07s Unsat: 6.19s) CPU Time : 75.152s Choices : 1571613 (Domain: 1449993) Conflicts : 97515 (Analyzed: 97512) Restarts : 1107 (Average: 88.09 Last: 156) Model-Level : 251.0 Problems : 15 (Average Length: 25.67 Splits: 0) Lemmas : 97512 (Deleted: 84548) Binary : 4675 (Ratio: 4.79%) Ternary : 1057 (Ratio: 1.08%) Conflict : 97512 (Average Length: 667.9 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 97512 (Average: 15.04 Max: 396 Sum: 1466301) Executed : 97430 (Average: 15.01 Max: 396 Sum: 1464029 Ratio: 99.85%) Bounded : 82 (Average: 27.71 Max: 32 Sum: 2272 Ratio: 0.15%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 318691 (Eliminated: 0 Frozen: 97441) Constraints : 2237379 (Binary: 91.3% Ternary: 6.9% Other: 1.8%) Memory Peak : 444MB Max. Length : 40 steps Models : 1 [endof: stats after solve call] Solving Time: 6.60s Memory: 443MB (+45MB) UNKNOWN Iteration Time: 7.45s Iteration 15 Queue: [(10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True)] Grounded Until: 45 Expected Memory: 498.0MB Grounding... [('step', [46]), ('step', [47]), ('step', [48]), ('step', [49]), ('step', [50]), ('check', [50])] Grounding Time: 0.69s Memory: 455MB (+12MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 16 Time : 83.220s (Solving: 73.58s 1st Model: 0.07s Unsat: 6.19s) CPU Time : 83.116s Choices : 1827366 (Domain: 1699900) Conflicts : 106260 (Analyzed: 106257) Restarts : 1207 (Average: 88.03 Last: 156) Model-Level : 251.0 Problems : 16 (Average Length: 27.31 Splits: 0) Lemmas : 106257 (Deleted: 94747) Binary : 4743 (Ratio: 4.46%) Ternary : 1058 (Ratio: 1.00%) Conflict : 106257 (Average Length: 695.3 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 106257 (Average: 16.03 Max: 415 Sum: 1703438) Executed : 106175 (Average: 16.01 Max: 415 Sum: 1701166 Ratio: 99.87%) Bounded : 82 (Average: 27.71 Max: 32 Sum: 2272 Ratio: 0.13%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 356182 (Eliminated: 0 Frozen: 109101) Constraints : 2519839 (Binary: 91.3% Ternary: 6.9% Other: 1.8%) Memory Peak : 503MB Max. Length : 45 steps Models : 1 [endof: stats after solve call] Solving Time: 6.95s Memory: 466MB (+11MB) UNKNOWN Iteration Time: 7.98s Iteration 16 Queue: [(11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True)] Grounded Until: 50 Expected Memory: 521.0MB Grounding... [('step', [51]), ('step', [52]), ('step', [53]), ('step', [54]), ('step', [55]), ('check', [55])] Grounding Time: 0.52s Memory: 470MB (+4MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 17 Time : 91.545s (Solving: 80.96s 1st Model: 0.07s Unsat: 6.19s) CPU Time : 91.448s Choices : 2131193 (Domain: 1996576) Conflicts : 114823 (Analyzed: 114820) Restarts : 1307 (Average: 87.85 Last: 156) Model-Level : 251.0 Problems : 17 (Average Length: 29.06 Splits: 0) Lemmas : 114820 (Deleted: 100990) Binary : 4792 (Ratio: 4.17%) Ternary : 1059 (Ratio: 0.92%) Conflict : 114820 (Average Length: 713.8 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 114820 (Average: 17.30 Max: 490 Sum: 1986954) Executed : 114738 (Average: 17.29 Max: 490 Sum: 1984682 Ratio: 99.89%) Bounded : 82 (Average: 27.71 Max: 32 Sum: 2272 Ratio: 0.11%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 393673 (Eliminated: 0 Frozen: 120761) Constraints : 2802299 (Binary: 91.3% Ternary: 6.9% Other: 1.8%) Memory Peak : 527MB Max. Length : 50 steps Models : 1 [endof: stats after solve call] Solving Time: 7.47s Memory: 489MB (+19MB) UNKNOWN Iteration Time: 8.34s Iteration 17 Queue: [(12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True)] Grounded Until: 55 Expected Memory: 544.0MB Grounding... [('step', [56]), ('step', [57]), ('step', [58]), ('step', [59]), ('step', [60]), ('check', [60])] Grounding Time: 0.51s Memory: 494MB (+5MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 18 Time : 99.920s (Solving: 88.38s 1st Model: 0.07s Unsat: 6.19s) CPU Time : 99.828s Choices : 2424475 (Domain: 2284371) Conflicts : 123053 (Analyzed: 123050) Restarts : 1407 (Average: 87.46 Last: 156) Model-Level : 251.0 Problems : 18 (Average Length: 30.89 Splits: 0) Lemmas : 123050 (Deleted: 109356) Binary : 4830 (Ratio: 3.93%) Ternary : 1060 (Ratio: 0.86%) Conflict : 123050 (Average Length: 740.6 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 123050 (Average: 18.35 Max: 543 Sum: 2257534) Executed : 122968 (Average: 18.33 Max: 543 Sum: 2255262 Ratio: 99.90%) Bounded : 82 (Average: 27.71 Max: 32 Sum: 2272 Ratio: 0.10%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 431164 (Eliminated: 0 Frozen: 132421) Constraints : 3084759 (Binary: 91.2% Ternary: 6.9% Other: 1.8%) Memory Peak : 557MB Max. Length : 55 steps Models : 1 [endof: stats after solve call] Solving Time: 7.51s Memory: 552MB (+58MB) UNKNOWN Iteration Time: 8.39s Iteration 18 Queue: [(13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True)] Grounded Until: 60 Expected Memory: 615.0MB Grounding... [('step', [61]), ('step', [62]), ('step', [63]), ('step', [64]), ('step', [65]), ('check', [65])] Grounding Time: 0.54s Memory: 552MB (+0MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 19 Time : 108.976s (Solving: 96.44s 1st Model: 0.07s Unsat: 6.19s) CPU Time : 108.888s Choices : 2742954 (Domain: 2597685) Conflicts : 131174 (Analyzed: 131171) Restarts : 1507 (Average: 87.04 Last: 156) Model-Level : 251.0 Problems : 19 (Average Length: 32.79 Splits: 0) Lemmas : 131171 (Deleted: 117422) Binary : 4855 (Ratio: 3.70%) Ternary : 1062 (Ratio: 0.81%) Conflict : 131171 (Average Length: 764.4 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 131171 (Average: 19.46 Max: 581 Sum: 2552228) Executed : 131089 (Average: 19.44 Max: 581 Sum: 2549956 Ratio: 99.91%) Bounded : 82 (Average: 27.71 Max: 32 Sum: 2272 Ratio: 0.09%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 468655 (Eliminated: 0 Frozen: 144081) Constraints : 3367219 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 609MB Max. Length : 60 steps Models : 1 [endof: stats after solve call] Solving Time: 8.16s Memory: 557MB (+5MB) UNKNOWN Iteration Time: 9.07s Iteration 19 Queue: [(14,70,0,True), (15,75,0,True), (16,80,0,True)] Grounded Until: 65 Expected Memory: 620.0MB Grounding... [('step', [66]), ('step', [67]), ('step', [68]), ('step', [69]), ('step', [70]), ('check', [70])] Grounding Time: 0.54s Memory: 562MB (+5MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 20 Time : 118.280s (Solving: 104.72s 1st Model: 0.07s Unsat: 6.19s) CPU Time : 118.196s Choices : 3075555 (Domain: 2925291) Conflicts : 139318 (Analyzed: 139315) Restarts : 1607 (Average: 86.69 Last: 156) Model-Level : 251.0 Problems : 20 (Average Length: 34.75 Splits: 0) Lemmas : 139315 (Deleted: 125364) Binary : 4891 (Ratio: 3.51%) Ternary : 1064 (Ratio: 0.76%) Conflict : 139315 (Average Length: 786.6 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 139315 (Average: 20.53 Max: 627 Sum: 2860030) Executed : 139233 (Average: 20.51 Max: 627 Sum: 2857758 Ratio: 99.92%) Bounded : 82 (Average: 27.71 Max: 32 Sum: 2272 Ratio: 0.08%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 506146 (Eliminated: 0 Frozen: 155741) Constraints : 3649679 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 633MB Max. Length : 65 steps Models : 1 [endof: stats after solve call] Solving Time: 8.39s Memory: 583MB (+21MB) UNKNOWN Iteration Time: 9.32s Iteration 20 Queue: [(15,75,0,True), (16,80,0,True)] Grounded Until: 70 Expected Memory: 646.0MB Grounding... [('step', [71]), ('step', [72]), ('step', [73]), ('step', [74]), ('step', [75]), ('check', [75])] Grounding Time: 0.52s Memory: 584MB (+1MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 21 Time : 127.830s (Solving: 113.25s 1st Model: 0.07s Unsat: 6.19s) CPU Time : 127.752s Choices : 3463794 (Domain: 3308410) Conflicts : 147563 (Analyzed: 147560) Restarts : 1707 (Average: 86.44 Last: 156) Model-Level : 251.0 Problems : 21 (Average Length: 36.76 Splits: 0) Lemmas : 147560 (Deleted: 133359) Binary : 4921 (Ratio: 3.33%) Ternary : 1064 (Ratio: 0.72%) Conflict : 147560 (Average Length: 801.6 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 147560 (Average: 21.84 Max: 682 Sum: 3222187) Executed : 147478 (Average: 21.82 Max: 682 Sum: 3219915 Ratio: 99.93%) Bounded : 82 (Average: 27.71 Max: 32 Sum: 2272 Ratio: 0.07%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 543637 (Eliminated: 0 Frozen: 167401) Constraints : 3932139 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 666MB Max. Length : 70 steps Models : 1 [endof: stats after solve call] Solving Time: 8.64s Memory: 609MB (+25MB) UNKNOWN Iteration Time: 9.57s Iteration 21 Queue: [(16,80,0,True)] Grounded Until: 75 Expected Memory: 672.0MB Grounding... [('step', [76]), ('step', [77]), ('step', [78]), ('step', [79]), ('step', [80]), ('check', [80])] Grounding Time: 0.53s Memory: 609MB (+0MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 22 Time : 137.655s (Solving: 122.02s 1st Model: 0.07s Unsat: 6.19s) CPU Time : 137.584s Choices : 3861148 (Domain: 3700237) Conflicts : 155896 (Analyzed: 155893) Restarts : 1807 (Average: 86.27 Last: 156) Model-Level : 251.0 Problems : 22 (Average Length: 38.82 Splits: 0) Lemmas : 155893 (Deleted: 141480) Binary : 4942 (Ratio: 3.17%) Ternary : 1065 (Ratio: 0.68%) Conflict : 155893 (Average Length: 818.8 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 155893 (Average: 23.04 Max: 732 Sum: 3592289) Executed : 155811 (Average: 23.03 Max: 732 Sum: 3590017 Ratio: 99.94%) Bounded : 82 (Average: 27.71 Max: 32 Sum: 2272 Ratio: 0.06%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 581128 (Eliminated: 0 Frozen: 179061) Constraints : 4214599 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 694MB Max. Length : 75 steps Models : 1 [endof: stats after solve call] Solving Time: 8.89s Memory: 633MB (+24MB) UNKNOWN Iteration Time: 9.84s Iteration 22 Queue: [(4,20,2,True), (5,25,2,True), (6,30,2,True), (7,35,1,True), (8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] Grounded Until: 80 Blocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 23 Time : 143.128s (Solving: 127.37s 1st Model: 0.07s Unsat: 6.19s) CPU Time : 143.056s Choices : 3944840 (Domain: 3778004) Conflicts : 164803 (Analyzed: 164800) Restarts : 1907 (Average: 86.42 Last: 156) Model-Level : 251.0 Problems : 23 (Average Length: 40.70 Splits: 0) Lemmas : 164800 (Deleted: 149207) Binary : 5344 (Ratio: 3.24%) Ternary : 1201 (Ratio: 0.73%) Conflict : 164800 (Average Length: 790.8 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 164800 (Average: 22.26 Max: 732 Sum: 3667764) Executed : 164713 (Average: 22.24 Max: 732 Sum: 3665082 Ratio: 99.93%) Bounded : 87 (Average: 30.83 Max: 82 Sum: 2682 Ratio: 0.07%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 581128 (Eliminated: 0 Frozen: 179061) Constraints : 4214599 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 694MB Max. Length : 80 steps Models : 1 [endof: stats after solve call] Solving Time: 5.43s Memory: 633MB (+0MB) UNKNOWN Iteration Time: 5.48s Iteration 23 Queue: [(5,25,2,True), (6,30,2,True), (7,35,1,True), (8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] Grounded Until: 80 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 24 Time : 151.500s (Solving: 135.62s 1st Model: 0.07s Unsat: 6.19s) CPU Time : 151.432s Choices : 4073315 (Domain: 3899978) Conflicts : 174025 (Analyzed: 174022) Restarts : 2007 (Average: 86.71 Last: 156) Model-Level : 251.0 Problems : 24 (Average Length: 42.42 Splits: 0) Lemmas : 174022 (Deleted: 157070) Binary : 5843 (Ratio: 3.36%) Ternary : 1372 (Ratio: 0.79%) Conflict : 174022 (Average Length: 762.6 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 174022 (Average: 21.76 Max: 732 Sum: 3786698) Executed : 173930 (Average: 21.74 Max: 732 Sum: 3783606 Ratio: 99.92%) Bounded : 92 (Average: 33.61 Max: 82 Sum: 3092 Ratio: 0.08%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 581128 (Eliminated: 0 Frozen: 179061) Constraints : 4214529 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 694MB Max. Length : 80 steps Models : 1 [endof: stats after solve call] Solving Time: 8.33s Memory: 633MB (+0MB) UNKNOWN Iteration Time: 8.38s Iteration 24 Queue: [(6,30,2,True), (7,35,1,True), (8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] Grounded Until: 80 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 25 Time : 160.748s (Solving: 144.71s 1st Model: 0.07s Unsat: 6.19s) CPU Time : 160.684s Choices : 4206834 (Domain: 4026174) Conflicts : 183158 (Analyzed: 183155) Restarts : 2107 (Average: 86.93 Last: 156) Model-Level : 251.0 Problems : 25 (Average Length: 44.00 Splits: 0) Lemmas : 183155 (Deleted: 165457) Binary : 6112 (Ratio: 3.34%) Ternary : 1447 (Ratio: 0.79%) Conflict : 183155 (Average Length: 742.5 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 183155 (Average: 21.34 Max: 732 Sum: 3909028) Executed : 183061 (Average: 21.32 Max: 732 Sum: 3905772 Ratio: 99.92%) Bounded : 94 (Average: 34.64 Max: 82 Sum: 3256 Ratio: 0.08%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 581128 (Eliminated: 0 Frozen: 179061) Constraints : 4214460 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 694MB Max. Length : 80 steps Models : 1 [endof: stats after solve call] Solving Time: 9.20s Memory: 633MB (+0MB) UNKNOWN Iteration Time: 9.26s Iteration 25 Queue: [(7,35,1,True), (8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] Grounded Until: 80 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 26 Time : 169.942s (Solving: 153.78s 1st Model: 0.07s Unsat: 6.19s) CPU Time : 169.884s Choices : 4339020 (Domain: 4152862) Conflicts : 192009 (Analyzed: 192006) Restarts : 2207 (Average: 87.00 Last: 156) Model-Level : 251.0 Problems : 26 (Average Length: 45.46 Splits: 0) Lemmas : 192006 (Deleted: 174050) Binary : 6269 (Ratio: 3.27%) Ternary : 1477 (Ratio: 0.77%) Conflict : 192006 (Average Length: 724.4 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 192006 (Average: 20.98 Max: 732 Sum: 4028203) Executed : 191909 (Average: 20.96 Max: 732 Sum: 4024701 Ratio: 99.91%) Bounded : 97 (Average: 36.10 Max: 82 Sum: 3502 Ratio: 0.09%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 581128 (Eliminated: 0 Frozen: 179061) Constraints : 4214421 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 694MB Max. Length : 80 steps Models : 1 [endof: stats after solve call] Solving Time: 9.15s Memory: 633MB (+0MB) UNKNOWN Iteration Time: 9.20s Iteration 26 Queue: [(8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] Grounded Until: 80 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 27 Time : 178.563s (Solving: 162.28s 1st Model: 0.07s Unsat: 6.19s) CPU Time : 178.508s Choices : 4483150 (Domain: 4294988) Conflicts : 200250 (Analyzed: 200247) Restarts : 2307 (Average: 86.80 Last: 156) Model-Level : 251.0 Problems : 27 (Average Length: 46.81 Splits: 0) Lemmas : 200247 (Deleted: 180348) Binary : 6424 (Ratio: 3.21%) Ternary : 1518 (Ratio: 0.76%) Conflict : 200247 (Average Length: 706.7 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 200247 (Average: 20.79 Max: 732 Sum: 4162747) Executed : 200150 (Average: 20.77 Max: 732 Sum: 4159245 Ratio: 99.92%) Bounded : 97 (Average: 36.10 Max: 82 Sum: 3502 Ratio: 0.08%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 581128 (Eliminated: 0 Frozen: 179061) Constraints : 4214383 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 694MB Max. Length : 80 steps Models : 1 [endof: stats after solve call] Solving Time: 8.58s Memory: 633MB (+0MB) UNKNOWN Iteration Time: 8.63s Iteration 27 Queue: [(9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] Grounded Until: 80 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 28 Time : 188.806s (Solving: 172.39s 1st Model: 0.07s Unsat: 6.19s) CPU Time : 188.756s Choices : 4710857 (Domain: 4518979) Conflicts : 209443 (Analyzed: 209440) Restarts : 2407 (Average: 87.01 Last: 156) Model-Level : 251.0 Problems : 28 (Average Length: 48.07 Splits: 0) Lemmas : 209440 (Deleted: 190144) Binary : 6772 (Ratio: 3.23%) Ternary : 1671 (Ratio: 0.80%) Conflict : 209440 (Average Length: 690.3 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 209440 (Average: 20.90 Max: 732 Sum: 4377404) Executed : 209340 (Average: 20.88 Max: 732 Sum: 4373661 Ratio: 99.91%) Bounded : 100 (Average: 37.43 Max: 82 Sum: 3743 Ratio: 0.09%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 581128 (Eliminated: 0 Frozen: 179061) Constraints : 4214383 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 694MB Max. Length : 80 steps Models : 1 [endof: stats after solve call] Solving Time: 10.20s Memory: 633MB (+0MB) UNKNOWN Iteration Time: 10.25s Iteration 28 Queue: [(10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] Grounded Until: 80 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 29 Time : 198.772s (Solving: 182.24s 1st Model: 0.07s Unsat: 6.19s) CPU Time : 198.724s Choices : 4942110 (Domain: 4746373) Conflicts : 218428 (Analyzed: 218425) Restarts : 2507 (Average: 87.13 Last: 156) Model-Level : 251.0 Problems : 29 (Average Length: 49.24 Splits: 0) Lemmas : 218425 (Deleted: 198382) Binary : 7052 (Ratio: 3.23%) Ternary : 1758 (Ratio: 0.80%) Conflict : 218425 (Average Length: 672.1 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 218425 (Average: 21.04 Max: 732 Sum: 4594966) Executed : 218324 (Average: 21.02 Max: 732 Sum: 4591141 Ratio: 99.92%) Bounded : 101 (Average: 37.87 Max: 82 Sum: 3825 Ratio: 0.08%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 581128 (Eliminated: 0 Frozen: 179061) Constraints : 4214355 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 694MB Max. Length : 80 steps Models : 1 [endof: stats after solve call] Solving Time: 9.93s Memory: 633MB (+0MB) UNKNOWN Iteration Time: 9.97s Iteration 29 Queue: [(11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] Grounded Until: 80 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 30 Time : 213.776s (Solving: 197.13s 1st Model: 0.07s Unsat: 6.19s) CPU Time : 213.736s Choices : 5543602 (Domain: 5335717) Conflicts : 228019 (Analyzed: 228016) Restarts : 2607 (Average: 87.46 Last: 156) Model-Level : 251.0 Problems : 30 (Average Length: 50.33 Splits: 0) Lemmas : 228016 (Deleted: 206371) Binary : 7863 (Ratio: 3.45%) Ternary : 1962 (Ratio: 0.86%) Conflict : 228016 (Average Length: 655.3 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 228016 (Average: 22.71 Max: 732 Sum: 5177436) Executed : 227915 (Average: 22.69 Max: 732 Sum: 5173611 Ratio: 99.93%) Bounded : 101 (Average: 37.87 Max: 82 Sum: 3825 Ratio: 0.07%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 581128 (Eliminated: 0 Frozen: 179061) Constraints : 4214341 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 694MB Max. Length : 80 steps Models : 1 [endof: stats after solve call] Solving Time: 14.97s Memory: 633MB (+0MB) UNKNOWN Iteration Time: 15.01s Iteration 30 Queue: [(12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] Grounded Until: 80 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 31 Time : 230.104s (Solving: 213.33s 1st Model: 0.07s Unsat: 6.19s) CPU Time : 230.072s Choices : 5912692 (Domain: 5701705) Conflicts : 237089 (Analyzed: 237086) Restarts : 2707 (Average: 87.58 Last: 156) Model-Level : 251.0 Problems : 31 (Average Length: 51.35 Splits: 0) Lemmas : 237086 (Deleted: 214344) Binary : 8345 (Ratio: 3.52%) Ternary : 2067 (Ratio: 0.87%) Conflict : 237086 (Average Length: 642.2 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 237086 (Average: 23.32 Max: 732 Sum: 5529510) Executed : 236985 (Average: 23.31 Max: 732 Sum: 5525685 Ratio: 99.93%) Bounded : 101 (Average: 37.87 Max: 82 Sum: 3825 Ratio: 0.07%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 581128 (Eliminated: 0 Frozen: 179061) Constraints : 4214341 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 694MB Max. Length : 80 steps Models : 1 [endof: stats after solve call] Solving Time: 16.29s Memory: 633MB (+0MB) UNKNOWN Iteration Time: 16.34s Iteration 31 Queue: [(13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] Grounded Until: 80 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 32 Time : 247.661s (Solving: 230.77s 1st Model: 0.07s Unsat: 6.19s) CPU Time : 247.640s Choices : 6355466 (Domain: 6140328) Conflicts : 246112 (Analyzed: 246109) Restarts : 2807 (Average: 87.68 Last: 156) Model-Level : 251.0 Problems : 32 (Average Length: 52.31 Splits: 0) Lemmas : 246109 (Deleted: 222644) Binary : 8751 (Ratio: 3.56%) Ternary : 2149 (Ratio: 0.87%) Conflict : 246109 (Average Length: 631.7 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 246109 (Average: 24.18 Max: 732 Sum: 5951293) Executed : 246008 (Average: 24.17 Max: 732 Sum: 5947468 Ratio: 99.94%) Bounded : 101 (Average: 37.87 Max: 82 Sum: 3825 Ratio: 0.06%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 581128 (Eliminated: 0 Frozen: 179061) Constraints : 4214341 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 694MB Max. Length : 80 steps Models : 1 [endof: stats after solve call] Solving Time: 17.53s Memory: 633MB (+0MB) UNKNOWN Iteration Time: 17.57s Iteration 32 Queue: [(14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] Grounded Until: 80 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 33 Time : 262.904s (Solving: 245.88s 1st Model: 0.07s Unsat: 6.19s) CPU Time : 262.888s Choices : 6768299 (Domain: 6550555) Conflicts : 254644 (Analyzed: 254641) Restarts : 2907 (Average: 87.60 Last: 156) Model-Level : 251.0 Problems : 33 (Average Length: 53.21 Splits: 0) Lemmas : 254641 (Deleted: 228922) Binary : 9085 (Ratio: 3.57%) Ternary : 2205 (Ratio: 0.87%) Conflict : 254641 (Average Length: 621.5 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 254641 (Average: 24.91 Max: 781 Sum: 6342905) Executed : 254540 (Average: 24.89 Max: 781 Sum: 6339080 Ratio: 99.94%) Bounded : 101 (Average: 37.87 Max: 82 Sum: 3825 Ratio: 0.06%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 581128 (Eliminated: 0 Frozen: 179061) Constraints : 4214341 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 694MB Max. Length : 80 steps Models : 1 [endof: stats after solve call] Solving Time: 15.20s Memory: 633MB (+0MB) UNKNOWN Iteration Time: 15.25s Iteration 33 Queue: [(15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] Grounded Until: 80 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 34 Time : 277.295s (Solving: 260.16s 1st Model: 0.07s Unsat: 6.19s) CPU Time : 277.284s Choices : 7147633 (Domain: 6925074) Conflicts : 263491 (Analyzed: 263488) Restarts : 3007 (Average: 87.62 Last: 156) Model-Level : 251.0 Problems : 34 (Average Length: 54.06 Splits: 0) Lemmas : 263488 (Deleted: 238764) Binary : 9400 (Ratio: 3.57%) Ternary : 2238 (Ratio: 0.85%) Conflict : 263488 (Average Length: 640.5 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 263488 (Average: 25.39 Max: 781 Sum: 6690109) Executed : 263387 (Average: 25.38 Max: 781 Sum: 6686284 Ratio: 99.94%) Bounded : 101 (Average: 37.87 Max: 82 Sum: 3825 Ratio: 0.06%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 581128 (Eliminated: 0 Frozen: 179061) Constraints : 4214341 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 761MB Max. Length : 80 steps Models : 1 [endof: stats after solve call] Solving Time: 14.36s Memory: 697MB (+64MB) UNKNOWN Iteration Time: 14.40s Iteration 34 Queue: [(16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] Grounded Until: 80 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 35 Time : 288.086s (Solving: 270.81s 1st Model: 0.07s Unsat: 6.19s) CPU Time : 288.076s Choices : 7331654 (Domain: 7108520) Conflicts : 271441 (Analyzed: 271438) Restarts : 3107 (Average: 87.36 Last: 156) Model-Level : 251.0 Problems : 35 (Average Length: 54.86 Splits: 0) Lemmas : 271438 (Deleted: 245100) Binary : 9510 (Ratio: 3.50%) Ternary : 2261 (Ratio: 0.83%) Conflict : 271438 (Average Length: 628.6 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 271438 (Average: 25.28 Max: 781 Sum: 6860706) Executed : 271336 (Average: 25.26 Max: 781 Sum: 6856799 Ratio: 99.94%) Bounded : 102 (Average: 38.30 Max: 82 Sum: 3907 Ratio: 0.06%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 581128 (Eliminated: 0 Frozen: 179061) Constraints : 4214341 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 761MB Max. Length : 80 steps Models : 1 [endof: stats after solve call] Solving Time: 10.74s Memory: 697MB (+0MB) UNKNOWN Iteration Time: 10.80s Iteration 35 Queue: [(17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] Grounded Until: 80 Expected Memory: 760.0MB Grounding... [('step', [81]), ('step', [82]), ('step', [83]), ('step', [84]), ('step', [85]), ('check', [85])] Grounding Time: 0.54s Memory: 697MB (+0MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 36 Time : 304.557s (Solving: 286.20s 1st Model: 0.07s Unsat: 6.19s) CPU Time : 304.556s Choices : 7852212 (Domain: 7625348) Conflicts : 281214 (Analyzed: 281211) Restarts : 3207 (Average: 87.69 Last: 156) Model-Level : 251.0 Problems : 36 (Average Length: 55.75 Splits: 0) Lemmas : 281211 (Deleted: 255259) Binary : 9793 (Ratio: 3.48%) Ternary : 2331 (Ratio: 0.83%) Conflict : 281211 (Average Length: 630.2 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 281211 (Average: 26.14 Max: 859 Sum: 7351427) Executed : 281109 (Average: 26.13 Max: 859 Sum: 7347520 Ratio: 99.95%) Bounded : 102 (Average: 38.30 Max: 82 Sum: 3907 Ratio: 0.05%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 618619 (Eliminated: 0 Frozen: 190721) Constraints : 4496787 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 784MB Max. Length : 80 steps Models : 1 [endof: stats after solve call] Solving Time: 15.52s Memory: 719MB (+22MB) UNKNOWN Iteration Time: 16.49s Iteration 36 Queue: [(18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] Grounded Until: 85 Expected Memory: 782.0MB Grounding... [('step', [86]), ('step', [87]), ('step', [88]), ('step', [89]), ('step', [90]), ('check', [90])] Grounding Time: 0.55s Memory: 719MB (+0MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 37 Time : 319.373s (Solving: 299.88s 1st Model: 0.07s Unsat: 6.19s) CPU Time : 319.376s Choices : 8188396 (Domain: 7959985) Conflicts : 289503 (Analyzed: 289500) Restarts : 3307 (Average: 87.54 Last: 156) Model-Level : 251.0 Problems : 37 (Average Length: 56.73 Splits: 0) Lemmas : 289500 (Deleted: 263146) Binary : 9950 (Ratio: 3.44%) Ternary : 2354 (Ratio: 0.81%) Conflict : 289500 (Average Length: 641.6 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 289500 (Average: 26.44 Max: 886 Sum: 7653554) Executed : 289398 (Average: 26.42 Max: 886 Sum: 7649647 Ratio: 99.95%) Bounded : 102 (Average: 38.30 Max: 82 Sum: 3907 Ratio: 0.05%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 656110 (Eliminated: 0 Frozen: 202381) Constraints : 4779247 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 811MB Max. Length : 85 steps Models : 1 [endof: stats after solve call] Solving Time: 13.81s Memory: 799MB (+80MB) UNKNOWN Iteration Time: 14.83s Iteration 37 Queue: [(19,95,0,True), (20,100,0,True), (21,105,0,True)] Grounded Until: 90 Expected Memory: 879.0MB Grounding... [('step', [91]), ('step', [92]), ('step', [93]), ('step', [94]), ('step', [95]), ('check', [95])] Grounding Time: 0.57s Memory: 799MB (+0MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 38 Time : 333.411s (Solving: 312.75s 1st Model: 0.07s Unsat: 6.19s) CPU Time : 333.420s Choices : 8440963 (Domain: 8211293) Conflicts : 297935 (Analyzed: 297932) Restarts : 3407 (Average: 87.45 Last: 156) Model-Level : 251.0 Problems : 38 (Average Length: 57.79 Splits: 0) Lemmas : 297932 (Deleted: 271843) Binary : 10074 (Ratio: 3.38%) Ternary : 2387 (Ratio: 0.80%) Conflict : 297932 (Average Length: 655.5 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 297932 (Average: 26.42 Max: 1023 Sum: 7872147) Executed : 297830 (Average: 26.41 Max: 1023 Sum: 7868240 Ratio: 99.95%) Bounded : 102 (Average: 38.30 Max: 82 Sum: 3907 Ratio: 0.05%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 693601 (Eliminated: 0 Frozen: 214041) Constraints : 5061707 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 884MB Max. Length : 90 steps Models : 1 [endof: stats after solve call] Solving Time: 13.01s Memory: 803MB (+4MB) UNKNOWN Iteration Time: 14.05s Iteration 38 Queue: [(20,100,0,True), (21,105,0,True)] Grounded Until: 95 Expected Memory: 883.0MB Grounding... [('step', [96]), ('step', [97]), ('step', [98]), ('step', [99]), ('step', [100]), ('check', [100])] Grounding Time: 0.89s Memory: 854MB (+51MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 39 Time : 347.630s (Solving: 325.49s 1st Model: 0.07s Unsat: 6.19s) CPU Time : 347.644s Choices : 8659704 (Domain: 8429461) Conflicts : 306292 (Analyzed: 306289) Restarts : 3507 (Average: 87.34 Last: 156) Model-Level : 251.0 Problems : 39 (Average Length: 58.92 Splits: 0) Lemmas : 306289 (Deleted: 280030) Binary : 10188 (Ratio: 3.33%) Ternary : 2407 (Ratio: 0.79%) Conflict : 306289 (Average Length: 666.3 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 306289 (Average: 26.30 Max: 1023 Sum: 8055366) Executed : 306187 (Average: 26.29 Max: 1023 Sum: 8051459 Ratio: 99.95%) Bounded : 102 (Average: 38.30 Max: 82 Sum: 3907 Ratio: 0.05%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 731092 (Eliminated: 0 Frozen: 225701) Constraints : 5344167 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 943MB Max. Length : 95 steps Models : 1 [endof: stats after solve call] Solving Time: 12.87s Memory: 858MB (+4MB) UNKNOWN Iteration Time: 14.24s Iteration 39 Queue: [(21,105,0,True)] Grounded Until: 100 Expected Memory: 938.0MB Grounding... [('step', [101]), ('step', [102]), ('step', [103]), ('step', [104]), ('step', [105]), ('check', [105])] Grounding Time: 0.52s Memory: 858MB (+0MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 40 Time : 359.992s (Solving: 336.71s 1st Model: 0.07s Unsat: 6.19s) CPU Time : 360.012s Choices : 8821634 (Domain: 8591315) Conflicts : 314575 (Analyzed: 314572) Restarts : 3607 (Average: 87.21 Last: 156) Model-Level : 251.0 Problems : 40 (Average Length: 60.12 Splits: 0) Lemmas : 314572 (Deleted: 288205) Binary : 10258 (Ratio: 3.26%) Ternary : 2414 (Ratio: 0.77%) Conflict : 314572 (Average Length: 681.2 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 314572 (Average: 26.01 Max: 1023 Sum: 8181575) Executed : 314470 (Average: 26.00 Max: 1023 Sum: 8177668 Ratio: 99.95%) Bounded : 102 (Average: 38.30 Max: 82 Sum: 3907 Ratio: 0.05%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 768583 (Eliminated: 0 Frozen: 237361) Constraints : 5626627 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 953MB Max. Length : 100 steps Models : 1 [endof: stats after solve call] Solving Time: 11.37s Memory: 868MB (+10MB) UNKNOWN Iteration Time: 12.38s Iteration 40 Queue: [(4,20,3,True), (5,25,3,True), (6,30,3,True), (7,35,2,True), (8,40,2,True), (9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] Grounded Until: 105 Blocking actions... Solving... [start: stats after solve call] Models : 0 Calls : 41 Time : 365.716s (Solving: 342.26s 1st Model: 0.07s Unsat: 11.73s) CPU Time : 365.740s Choices : 8873173 (Domain: 8642854) Conflicts : 319882 (Analyzed: 319878) Restarts : 3672 (Average: 87.11 Last: 156) Model-Level : 251.0 Problems : 41 (Average Length: 61.27 Splits: 0) Lemmas : 319878 (Deleted: 293629) Binary : 10410 (Ratio: 3.25%) Ternary : 2446 (Ratio: 0.76%) Conflict : 319878 (Average Length: 675.2 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 319878 (Average: 25.73 Max: 1023 Sum: 8232011) Executed : 319768 (Average: 25.72 Max: 1023 Sum: 8227990 Ratio: 99.95%) Bounded : 110 (Average: 36.55 Max: 107 Sum: 4021 Ratio: 0.05%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 768583 (Eliminated: 0 Frozen: 237361) Constraints : 5626627 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 953MB Max. Length : 105 steps Models : 1 [endof: stats after solve call] Solving Time: 5.66s Memory: 872MB (+4MB) UNSAT Iteration Time: 5.73s Iteration 41 Queue: [(5,25,3,True), (6,30,3,True), (7,35,2,True), (8,40,2,True), (9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] Grounded Until: 105 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 42 Time : 370.558s (Solving: 346.95s 1st Model: 0.07s Unsat: 11.73s) CPU Time : 370.580s Choices : 8920227 (Domain: 8689908) Conflicts : 327253 (Analyzed: 327249) Restarts : 3772 (Average: 86.76 Last: 156) Model-Level : 251.0 Problems : 42 (Average Length: 62.36 Splits: 0) Lemmas : 327249 (Deleted: 298682) Binary : 10504 (Ratio: 3.21%) Ternary : 2480 (Ratio: 0.76%) Conflict : 327249 (Average Length: 667.0 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 327249 (Average: 25.28 Max: 1023 Sum: 8272642) Executed : 327137 (Average: 25.27 Max: 1023 Sum: 8268407 Ratio: 99.95%) Bounded : 112 (Average: 37.81 Max: 107 Sum: 4235 Ratio: 0.05%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 768583 (Eliminated: 0 Frozen: 237361) Constraints : 5626613 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 953MB Max. Length : 105 steps Models : 1 [endof: stats after solve call] Solving Time: 4.80s Memory: 872MB (+0MB) UNKNOWN Iteration Time: 4.85s Iteration 42 Queue: [(6,30,3,True), (7,35,2,True), (8,40,2,True), (9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] Grounded Until: 105 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 43 Time : 376.030s (Solving: 352.27s 1st Model: 0.07s Unsat: 11.73s) CPU Time : 376.056s Choices : 8957184 (Domain: 8726865) Conflicts : 335518 (Analyzed: 335514) Restarts : 3872 (Average: 86.65 Last: 156) Model-Level : 251.0 Problems : 43 (Average Length: 63.40 Splits: 0) Lemmas : 335514 (Deleted: 305695) Binary : 10555 (Ratio: 3.15%) Ternary : 2501 (Ratio: 0.75%) Conflict : 335514 (Average Length: 657.7 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 335514 (Average: 24.75 Max: 1023 Sum: 8302817) Executed : 335399 (Average: 24.73 Max: 1023 Sum: 8298267 Ratio: 99.95%) Bounded : 115 (Average: 39.57 Max: 107 Sum: 4550 Ratio: 0.05%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 768583 (Eliminated: 0 Frozen: 237361) Constraints : 5626573 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 953MB Max. Length : 105 steps Models : 1 [endof: stats after solve call] Solving Time: 5.42s Memory: 872MB (+0MB) UNKNOWN Iteration Time: 5.48s Iteration 43 Queue: [(7,35,2,True), (8,40,2,True), (9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] Grounded Until: 105 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 44 Time : 382.072s (Solving: 358.13s 1st Model: 0.07s Unsat: 11.73s) CPU Time : 382.100s Choices : 9012585 (Domain: 8781888) Conflicts : 343292 (Analyzed: 343288) Restarts : 3972 (Average: 86.43 Last: 156) Model-Level : 251.0 Problems : 44 (Average Length: 64.39 Splits: 0) Lemmas : 343288 (Deleted: 313547) Binary : 10635 (Ratio: 3.10%) Ternary : 2523 (Ratio: 0.73%) Conflict : 343288 (Average Length: 649.1 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 343288 (Average: 24.33 Max: 1023 Sum: 8350864) Executed : 343171 (Average: 24.31 Max: 1023 Sum: 8346105 Ratio: 99.94%) Bounded : 117 (Average: 40.68 Max: 107 Sum: 4759 Ratio: 0.06%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 768583 (Eliminated: 0 Frozen: 237361) Constraints : 5626545 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 953MB Max. Length : 105 steps Models : 1 [endof: stats after solve call] Solving Time: 5.98s Memory: 872MB (+0MB) UNKNOWN Iteration Time: 6.05s Iteration 44 Queue: [(8,40,2,True), (9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] Grounded Until: 105 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 45 Time : 389.462s (Solving: 365.37s 1st Model: 0.07s Unsat: 11.73s) CPU Time : 389.492s Choices : 9099779 (Domain: 8867922) Conflicts : 351879 (Analyzed: 351875) Restarts : 4072 (Average: 86.41 Last: 156) Model-Level : 251.0 Problems : 45 (Average Length: 65.33 Splits: 0) Lemmas : 351875 (Deleted: 320980) Binary : 10718 (Ratio: 3.05%) Ternary : 2524 (Ratio: 0.72%) Conflict : 351875 (Average Length: 639.2 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 351875 (Average: 23.95 Max: 1023 Sum: 8427989) Executed : 351758 (Average: 23.94 Max: 1023 Sum: 8423230 Ratio: 99.94%) Bounded : 117 (Average: 40.68 Max: 107 Sum: 4759 Ratio: 0.06%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 768583 (Eliminated: 0 Frozen: 237361) Constraints : 5626532 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 953MB Max. Length : 105 steps Models : 1 [endof: stats after solve call] Solving Time: 7.34s Memory: 872MB (+0MB) UNKNOWN Iteration Time: 7.39s Iteration 45 Queue: [(9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] Grounded Until: 105 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 46 Time : 397.083s (Solving: 372.84s 1st Model: 0.07s Unsat: 11.73s) CPU Time : 397.116s Choices : 9175045 (Domain: 8942781) Conflicts : 359970 (Analyzed: 359966) Restarts : 4172 (Average: 86.28 Last: 156) Model-Level : 251.0 Problems : 46 (Average Length: 66.24 Splits: 0) Lemmas : 359966 (Deleted: 329350) Binary : 10809 (Ratio: 3.00%) Ternary : 2532 (Ratio: 0.70%) Conflict : 359966 (Average Length: 630.9 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 359966 (Average: 23.59 Max: 1023 Sum: 8491221) Executed : 359848 (Average: 23.58 Max: 1023 Sum: 8486355 Ratio: 99.94%) Bounded : 118 (Average: 41.24 Max: 107 Sum: 4866 Ratio: 0.06%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 768583 (Eliminated: 0 Frozen: 237361) Constraints : 5626532 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 953MB Max. Length : 105 steps Models : 1 [endof: stats after solve call] Solving Time: 7.58s Memory: 872MB (+0MB) UNKNOWN Iteration Time: 7.63s Iteration 46 Queue: [(10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] Grounded Until: 105 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 47 Time : 404.461s (Solving: 380.07s 1st Model: 0.07s Unsat: 11.73s) CPU Time : 404.496s Choices : 9267150 (Domain: 9034455) Conflicts : 368151 (Analyzed: 368147) Restarts : 4272 (Average: 86.18 Last: 156) Model-Level : 251.0 Problems : 47 (Average Length: 67.11 Splits: 0) Lemmas : 368147 (Deleted: 337169) Binary : 10863 (Ratio: 2.95%) Ternary : 2547 (Ratio: 0.69%) Conflict : 368147 (Average Length: 622.4 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 368147 (Average: 23.29 Max: 1023 Sum: 8572935) Executed : 368029 (Average: 23.27 Max: 1023 Sum: 8568069 Ratio: 99.94%) Bounded : 118 (Average: 41.24 Max: 107 Sum: 4866 Ratio: 0.06%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 768583 (Eliminated: 0 Frozen: 237361) Constraints : 5626519 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 953MB Max. Length : 105 steps Models : 1 [endof: stats after solve call] Solving Time: 7.33s Memory: 872MB (+0MB) UNKNOWN Iteration Time: 7.38s Iteration 47 Queue: [(11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] Grounded Until: 105 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 48 Time : 412.856s (Solving: 388.31s 1st Model: 0.07s Unsat: 11.73s) CPU Time : 412.892s Choices : 9404999 (Domain: 9171074) Conflicts : 376181 (Analyzed: 376177) Restarts : 4372 (Average: 86.04 Last: 156) Model-Level : 251.0 Problems : 48 (Average Length: 67.94 Splits: 0) Lemmas : 376177 (Deleted: 344901) Binary : 10984 (Ratio: 2.92%) Ternary : 2581 (Ratio: 0.69%) Conflict : 376177 (Average Length: 613.9 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 376177 (Average: 23.12 Max: 1023 Sum: 8698808) Executed : 376058 (Average: 23.11 Max: 1023 Sum: 8693835 Ratio: 99.94%) Bounded : 119 (Average: 41.79 Max: 107 Sum: 4973 Ratio: 0.06%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 768583 (Eliminated: 0 Frozen: 237361) Constraints : 5626519 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 953MB Max. Length : 105 steps Models : 1 [endof: stats after solve call] Solving Time: 8.35s Memory: 872MB (+0MB) UNKNOWN Iteration Time: 8.40s Iteration 48 Queue: [(12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] Grounded Until: 105 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 49 Time : 420.928s (Solving: 396.23s 1st Model: 0.07s Unsat: 11.73s) CPU Time : 420.968s Choices : 9505662 (Domain: 9271445) Conflicts : 384278 (Analyzed: 384274) Restarts : 4472 (Average: 85.93 Last: 156) Model-Level : 251.0 Problems : 49 (Average Length: 68.73 Splits: 0) Lemmas : 384274 (Deleted: 352566) Binary : 11089 (Ratio: 2.89%) Ternary : 2603 (Ratio: 0.68%) Conflict : 384274 (Average Length: 606.0 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 384274 (Average: 22.87 Max: 1023 Sum: 8788887) Executed : 384154 (Average: 22.86 Max: 1023 Sum: 8783810 Ratio: 99.94%) Bounded : 120 (Average: 42.31 Max: 107 Sum: 5077 Ratio: 0.06%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 768583 (Eliminated: 0 Frozen: 237361) Constraints : 5624066 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 953MB Max. Length : 105 steps Models : 1 [endof: stats after solve call] Solving Time: 8.02s Memory: 872MB (+0MB) UNKNOWN Iteration Time: 8.08s Iteration 49 Queue: [(13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] Grounded Until: 105 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 50 Time : 427.806s (Solving: 402.93s 1st Model: 0.07s Unsat: 11.73s) CPU Time : 427.848s Choices : 9625963 (Domain: 9391270) Conflicts : 392459 (Analyzed: 392455) Restarts : 4572 (Average: 85.84 Last: 156) Model-Level : 251.0 Problems : 50 (Average Length: 69.50 Splits: 0) Lemmas : 392455 (Deleted: 360317) Binary : 11167 (Ratio: 2.85%) Ternary : 2619 (Ratio: 0.67%) Conflict : 392455 (Average Length: 598.2 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 392455 (Average: 22.67 Max: 1023 Sum: 8896777) Executed : 392334 (Average: 22.66 Max: 1023 Sum: 8891593 Ratio: 99.94%) Bounded : 121 (Average: 42.84 Max: 107 Sum: 5184 Ratio: 0.06%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 768583 (Eliminated: 0 Frozen: 237361) Constraints : 5624066 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 953MB Max. Length : 105 steps Models : 1 [endof: stats after solve call] Solving Time: 6.82s Memory: 872MB (+0MB) UNKNOWN Iteration Time: 6.88s Iteration 50 Queue: [(17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] Grounded Until: 105 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 51 Time : 435.846s (Solving: 410.82s 1st Model: 0.07s Unsat: 11.73s) CPU Time : 435.892s Choices : 9779433 (Domain: 9544044) Conflicts : 400194 (Analyzed: 400190) Restarts : 4672 (Average: 85.66 Last: 156) Model-Level : 251.0 Problems : 51 (Average Length: 70.24 Splits: 0) Lemmas : 400190 (Deleted: 368168) Binary : 11259 (Ratio: 2.81%) Ternary : 2634 (Ratio: 0.66%) Conflict : 400190 (Average Length: 591.6 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 400190 (Average: 22.58 Max: 1023 Sum: 9035408) Executed : 400069 (Average: 22.56 Max: 1023 Sum: 9030224 Ratio: 99.94%) Bounded : 121 (Average: 42.84 Max: 107 Sum: 5184 Ratio: 0.06%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 768583 (Eliminated: 0 Frozen: 237361) Constraints : 5624052 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 953MB Max. Length : 105 steps Models : 1 [endof: stats after solve call] Solving Time: 7.99s Memory: 872MB (+0MB) UNKNOWN Iteration Time: 8.05s Iteration 51 Queue: [(18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] Grounded Until: 105 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 52 Time : 446.075s (Solving: 420.90s 1st Model: 0.07s Unsat: 11.73s) CPU Time : 446.116s Choices : 9905268 (Domain: 9669814) Conflicts : 408173 (Analyzed: 408169) Restarts : 4772 (Average: 85.53 Last: 156) Model-Level : 251.0 Problems : 52 (Average Length: 70.94 Splits: 0) Lemmas : 408169 (Deleted: 375638) Binary : 11366 (Ratio: 2.78%) Ternary : 2653 (Ratio: 0.65%) Conflict : 408169 (Average Length: 585.7 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 408169 (Average: 22.40 Max: 1023 Sum: 9142549) Executed : 408048 (Average: 22.39 Max: 1023 Sum: 9137365 Ratio: 99.94%) Bounded : 121 (Average: 42.84 Max: 107 Sum: 5184 Ratio: 0.06%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 768583 (Eliminated: 0 Frozen: 237361) Constraints : 5624052 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 953MB Max. Length : 105 steps Models : 1 [endof: stats after solve call] Solving Time: 10.17s Memory: 872MB (+0MB) UNKNOWN Iteration Time: 10.22s Iteration 52 Queue: [(19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] Grounded Until: 105 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 53 Time : 455.758s (Solving: 430.39s 1st Model: 0.07s Unsat: 11.73s) CPU Time : 455.804s Choices : 10158880 (Domain: 9921926) Conflicts : 416559 (Analyzed: 416555) Restarts : 4872 (Average: 85.50 Last: 156) Model-Level : 251.0 Problems : 53 (Average Length: 71.62 Splits: 0) Lemmas : 416555 (Deleted: 383356) Binary : 11464 (Ratio: 2.75%) Ternary : 2698 (Ratio: 0.65%) Conflict : 416555 (Average Length: 579.5 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 416555 (Average: 22.51 Max: 1023 Sum: 9377370) Executed : 416434 (Average: 22.50 Max: 1023 Sum: 9372186 Ratio: 99.94%) Bounded : 121 (Average: 42.84 Max: 107 Sum: 5184 Ratio: 0.06%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 768583 (Eliminated: 0 Frozen: 237361) Constraints : 5624052 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 953MB Max. Length : 105 steps Models : 1 [endof: stats after solve call] Solving Time: 9.61s Memory: 872MB (+0MB) UNKNOWN Iteration Time: 9.69s Iteration 53 Queue: [(20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] Grounded Until: 105 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 54 Time : 463.893s (Solving: 438.34s 1st Model: 0.07s Unsat: 11.73s) CPU Time : 463.940s Choices : 10300002 (Domain: 10061882) Conflicts : 424673 (Analyzed: 424669) Restarts : 4972 (Average: 85.41 Last: 156) Model-Level : 251.0 Problems : 54 (Average Length: 72.28 Splits: 0) Lemmas : 424669 (Deleted: 391322) Binary : 11509 (Ratio: 2.71%) Ternary : 2711 (Ratio: 0.64%) Conflict : 424669 (Average Length: 573.8 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 424669 (Average: 22.38 Max: 1023 Sum: 9502950) Executed : 424546 (Average: 22.36 Max: 1023 Sum: 9497557 Ratio: 99.94%) Bounded : 123 (Average: 43.85 Max: 107 Sum: 5393 Ratio: 0.06%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 768583 (Eliminated: 0 Frozen: 237361) Constraints : 5624052 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 953MB Max. Length : 105 steps Models : 1 [endof: stats after solve call] Solving Time: 8.07s Memory: 872MB (+0MB) UNKNOWN Iteration Time: 8.14s Iteration 54 Queue: [(21,105,1,True), (22,110,0,True), (23,115,0,True)] Grounded Until: 105 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 55 Time : 470.272s (Solving: 444.57s 1st Model: 0.07s Unsat: 11.73s) CPU Time : 470.320s Choices : 10426836 (Domain: 10188457) Conflicts : 432581 (Analyzed: 432577) Restarts : 5072 (Average: 85.29 Last: 156) Model-Level : 251.0 Problems : 55 (Average Length: 72.91 Splits: 0) Lemmas : 432577 (Deleted: 399214) Binary : 11536 (Ratio: 2.67%) Ternary : 2722 (Ratio: 0.63%) Conflict : 432577 (Average Length: 568.3 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 432577 (Average: 22.23 Max: 1023 Sum: 9614354) Executed : 432453 (Average: 22.21 Max: 1023 Sum: 9608857 Ratio: 99.94%) Bounded : 124 (Average: 44.33 Max: 107 Sum: 5497 Ratio: 0.06%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 768583 (Eliminated: 0 Frozen: 237361) Constraints : 5624038 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 953MB Max. Length : 105 steps Models : 1 [endof: stats after solve call] Solving Time: 6.33s Memory: 872MB (+0MB) UNKNOWN Iteration Time: 6.38s Iteration 55 Queue: [(22,110,0,True), (23,115,0,True)] Grounded Until: 105 Expected Memory: 952.0MB Grounding... [('step', [106]), ('step', [107]), ('step', [108]), ('step', [109]), ('step', [110]), ('check', [110])] Grounding Time: 0.53s Memory: 874MB (+2MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 56 Time : 484.717s (Solving: 457.82s 1st Model: 0.07s Unsat: 11.73s) CPU Time : 484.772s Choices : 10668740 (Domain: 10429909) Conflicts : 441287 (Analyzed: 441283) Restarts : 5172 (Average: 85.32 Last: 156) Model-Level : 251.0 Problems : 56 (Average Length: 73.61 Splits: 0) Lemmas : 441283 (Deleted: 409052) Binary : 11634 (Ratio: 2.64%) Ternary : 2724 (Ratio: 0.62%) Conflict : 441283 (Average Length: 572.4 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 441283 (Average: 22.25 Max: 1075 Sum: 9820081) Executed : 441159 (Average: 22.24 Max: 1075 Sum: 9814584 Ratio: 99.94%) Bounded : 124 (Average: 44.33 Max: 107 Sum: 5497 Ratio: 0.06%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 806074 (Eliminated: 0 Frozen: 249021) Constraints : 5906498 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 987MB Max. Length : 105 steps Models : 1 [endof: stats after solve call] Solving Time: 13.41s Memory: 902MB (+28MB) UNKNOWN Iteration Time: 14.46s Iteration 56 Queue: [(23,115,0,True)] Grounded Until: 110 Expected Memory: 982.0MB Grounding... [('step', [111]), ('step', [112]), ('step', [113]), ('step', [114]), ('step', [115]), ('check', [115])] Grounding Time: 0.53s Memory: 902MB (+0MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 57 Time : 495.871s (Solving: 467.77s 1st Model: 0.07s Unsat: 11.73s) CPU Time : 495.916s Choices : 10772507 (Domain: 10533671) Conflicts : 449452 (Analyzed: 449448) Restarts : 5272 (Average: 85.25 Last: 156) Model-Level : 251.0 Problems : 57 (Average Length: 74.37 Splits: 0) Lemmas : 449448 (Deleted: 416419) Binary : 11660 (Ratio: 2.59%) Ternary : 2727 (Ratio: 0.61%) Conflict : 449448 (Average Length: 582.2 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 449448 (Average: 21.99 Max: 1075 Sum: 9884708) Executed : 449324 (Average: 21.98 Max: 1075 Sum: 9879211 Ratio: 99.94%) Bounded : 124 (Average: 44.33 Max: 107 Sum: 5497 Ratio: 0.06%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 843565 (Eliminated: 0 Frozen: 260681) Constraints : 6188958 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1016MB Max. Length : 110 steps Models : 1 [endof: stats after solve call] Solving Time: 10.08s Memory: 917MB (+15MB) UNKNOWN Iteration Time: 11.16s Iteration 57 Queue: [(5,25,4,True), (6,30,4,True), (7,35,3,True), (8,40,3,True), (9,45,3,True), (10,50,3,True), (11,55,3,True), (12,60,3,False), (13,65,3,False), (14,70,2,True), (15,75,2,True), (16,80,2,True), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,1,True), (23,115,1,True), (24,120,0,True)] Grounded Until: 115 Blocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 58 Time : 499.255s (Solving: 470.95s 1st Model: 0.07s Unsat: 11.73s) CPU Time : 499.300s Choices : 10812374 (Domain: 10573538) Conflicts : 456821 (Analyzed: 456817) Restarts : 5372 (Average: 85.04 Last: 156) Model-Level : 251.0 Problems : 58 (Average Length: 75.10 Splits: 0) Lemmas : 456817 (Deleted: 423390) Binary : 11706 (Ratio: 2.56%) Ternary : 2735 (Ratio: 0.60%) Conflict : 456817 (Average Length: 576.6 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 456817 (Average: 21.71 Max: 1075 Sum: 9919018) Executed : 456692 (Average: 21.70 Max: 1075 Sum: 9913409 Ratio: 99.94%) Bounded : 125 (Average: 44.87 Max: 112 Sum: 5609 Ratio: 0.06%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 843565 (Eliminated: 0 Frozen: 260681) Constraints : 6188958 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1016MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 3.31s Memory: 927MB (+10MB) UNKNOWN Iteration Time: 3.39s Iteration 58 Queue: [(6,30,4,True), (7,35,3,True), (8,40,3,True), (9,45,3,True), (10,50,3,True), (11,55,3,True), (12,60,3,False), (13,65,3,False), (14,70,2,True), (15,75,2,True), (16,80,2,True), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,1,True), (23,115,1,True), (24,120,0,True)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 59 Time : 503.796s (Solving: 475.31s 1st Model: 0.07s Unsat: 11.73s) CPU Time : 503.844s Choices : 10858072 (Domain: 10619236) Conflicts : 464736 (Analyzed: 464732) Restarts : 5472 (Average: 84.93 Last: 156) Model-Level : 251.0 Problems : 59 (Average Length: 75.81 Splits: 0) Lemmas : 464732 (Deleted: 430527) Binary : 11723 (Ratio: 2.52%) Ternary : 2749 (Ratio: 0.59%) Conflict : 464732 (Average Length: 571.9 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 464732 (Average: 21.43 Max: 1075 Sum: 9957893) Executed : 464605 (Average: 21.41 Max: 1075 Sum: 9952058 Ratio: 99.94%) Bounded : 127 (Average: 45.94 Max: 114 Sum: 5835 Ratio: 0.06%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 843565 (Eliminated: 0 Frozen: 260681) Constraints : 6188958 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1016MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 4.48s Memory: 927MB (+0MB) UNKNOWN Iteration Time: 4.55s Iteration 59 Queue: [(7,35,3,True), (8,40,3,True), (9,45,3,True), (10,50,3,True), (11,55,3,True), (12,60,3,False), (13,65,3,False), (14,70,2,True), (15,75,2,True), (16,80,2,True), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,1,True), (23,115,1,True), (24,120,0,True)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 60 Time : 509.698s (Solving: 481.03s 1st Model: 0.07s Unsat: 11.73s) CPU Time : 509.748s Choices : 10938343 (Domain: 10698726) Conflicts : 473005 (Analyzed: 473001) Restarts : 5572 (Average: 84.89 Last: 156) Model-Level : 251.0 Problems : 60 (Average Length: 76.50 Splits: 0) Lemmas : 473001 (Deleted: 438128) Binary : 11839 (Ratio: 2.50%) Ternary : 2762 (Ratio: 0.58%) Conflict : 473001 (Average Length: 566.6 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 473001 (Average: 21.20 Max: 1075 Sum: 10029310) Executed : 472874 (Average: 21.19 Max: 1075 Sum: 10023475 Ratio: 99.94%) Bounded : 127 (Average: 45.94 Max: 114 Sum: 5835 Ratio: 0.06%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 843565 (Eliminated: 0 Frozen: 260681) Constraints : 6188958 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1016MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 5.83s Memory: 927MB (+0MB) UNKNOWN Iteration Time: 5.91s Iteration 60 Queue: [(8,40,3,True), (9,45,3,True), (10,50,3,True), (11,55,3,True), (12,60,3,False), (13,65,3,False), (14,70,2,True), (15,75,2,True), (16,80,2,True), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,1,True), (23,115,1,True), (24,120,0,True)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 61 Time : 517.744s (Solving: 488.91s 1st Model: 0.07s Unsat: 11.73s) CPU Time : 517.800s Choices : 11034827 (Domain: 10794716) Conflicts : 481513 (Analyzed: 481509) Restarts : 5672 (Average: 84.89 Last: 156) Model-Level : 251.0 Problems : 61 (Average Length: 77.16 Splits: 0) Lemmas : 481509 (Deleted: 446167) Binary : 11939 (Ratio: 2.48%) Ternary : 2780 (Ratio: 0.58%) Conflict : 481509 (Average Length: 561.6 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 481509 (Average: 21.01 Max: 1075 Sum: 10115598) Executed : 481382 (Average: 21.00 Max: 1075 Sum: 10109763 Ratio: 99.94%) Bounded : 127 (Average: 45.94 Max: 114 Sum: 5835 Ratio: 0.06%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 843565 (Eliminated: 0 Frozen: 260681) Constraints : 6188958 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1016MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 7.99s Memory: 927MB (+0MB) UNKNOWN Iteration Time: 8.05s Iteration 61 Queue: [(9,45,3,True), (10,50,3,True), (11,55,3,True), (12,60,3,False), (13,65,3,False), (14,70,2,True), (15,75,2,True), (16,80,2,True), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,1,True), (23,115,1,True), (24,120,0,True)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 62 Time : 521.594s (Solving: 492.59s 1st Model: 0.07s Unsat: 11.73s) CPU Time : 521.652s Choices : 11082265 (Domain: 10842139) Conflicts : 488820 (Analyzed: 488816) Restarts : 5772 (Average: 84.69 Last: 156) Model-Level : 251.0 Problems : 62 (Average Length: 77.81 Splits: 0) Lemmas : 488816 (Deleted: 454353) Binary : 11995 (Ratio: 2.45%) Ternary : 2789 (Ratio: 0.57%) Conflict : 488816 (Average Length: 556.3 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 488816 (Average: 20.77 Max: 1075 Sum: 10152675) Executed : 488689 (Average: 20.76 Max: 1075 Sum: 10146840 Ratio: 99.94%) Bounded : 127 (Average: 45.94 Max: 114 Sum: 5835 Ratio: 0.06%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 843565 (Eliminated: 0 Frozen: 260681) Constraints : 6188958 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1016MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 3.80s Memory: 927MB (+0MB) UNKNOWN Iteration Time: 3.85s Iteration 62 Queue: [(10,50,3,True), (11,55,3,True), (12,60,3,False), (13,65,3,False), (14,70,2,True), (15,75,2,True), (16,80,2,True), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,1,True), (23,115,1,True), (24,120,0,True)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 63 Time : 530.749s (Solving: 501.56s 1st Model: 0.07s Unsat: 11.73s) CPU Time : 530.812s Choices : 11222325 (Domain: 10981354) Conflicts : 497837 (Analyzed: 497833) Restarts : 5872 (Average: 84.78 Last: 156) Model-Level : 251.0 Problems : 63 (Average Length: 78.43 Splits: 0) Lemmas : 497833 (Deleted: 463546) Binary : 12171 (Ratio: 2.44%) Ternary : 2808 (Ratio: 0.56%) Conflict : 497833 (Average Length: 552.5 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 497833 (Average: 20.65 Max: 1075 Sum: 10278415) Executed : 497706 (Average: 20.63 Max: 1075 Sum: 10272580 Ratio: 99.94%) Bounded : 127 (Average: 45.94 Max: 114 Sum: 5835 Ratio: 0.06%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 843565 (Eliminated: 0 Frozen: 260681) Constraints : 6188958 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1016MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 9.09s Memory: 927MB (+0MB) UNKNOWN Iteration Time: 9.16s Iteration 63 Queue: [(11,55,3,True), (12,60,3,False), (13,65,3,False), (14,70,2,True), (15,75,2,True), (16,80,2,True), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,1,True), (23,115,1,True), (24,120,0,True)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 64 Time : 537.295s (Solving: 507.89s 1st Model: 0.07s Unsat: 11.73s) CPU Time : 537.360s Choices : 11306159 (Domain: 11064750) Conflicts : 506280 (Analyzed: 506276) Restarts : 5972 (Average: 84.77 Last: 156) Model-Level : 251.0 Problems : 64 (Average Length: 79.03 Splits: 0) Lemmas : 506276 (Deleted: 470056) Binary : 12234 (Ratio: 2.42%) Ternary : 2820 (Ratio: 0.56%) Conflict : 506276 (Average Length: 548.6 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 506276 (Average: 20.44 Max: 1075 Sum: 10350693) Executed : 506148 (Average: 20.43 Max: 1075 Sum: 10344741 Ratio: 99.94%) Bounded : 128 (Average: 46.50 Max: 117 Sum: 5952 Ratio: 0.06%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 843565 (Eliminated: 0 Frozen: 260681) Constraints : 6188958 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1016MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 6.47s Memory: 927MB (+0MB) UNKNOWN Iteration Time: 6.55s Iteration 64 Queue: [(14,70,2,True), (15,75,2,True), (16,80,2,True), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,1,True), (23,115,1,True), (24,120,0,True)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 65 Time : 544.810s (Solving: 515.24s 1st Model: 0.07s Unsat: 11.73s) CPU Time : 544.880s Choices : 11455247 (Domain: 11212748) Conflicts : 514387 (Analyzed: 514383) Restarts : 6072 (Average: 84.71 Last: 156) Model-Level : 251.0 Problems : 65 (Average Length: 79.62 Splits: 0) Lemmas : 514383 (Deleted: 478195) Binary : 12351 (Ratio: 2.40%) Ternary : 2841 (Ratio: 0.55%) Conflict : 514383 (Average Length: 545.4 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 514383 (Average: 20.38 Max: 1075 Sum: 10484475) Executed : 514255 (Average: 20.37 Max: 1075 Sum: 10478523 Ratio: 99.94%) Bounded : 128 (Average: 46.50 Max: 117 Sum: 5952 Ratio: 0.06%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 843565 (Eliminated: 0 Frozen: 260681) Constraints : 6188944 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1016MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 7.46s Memory: 927MB (+0MB) UNKNOWN Iteration Time: 7.52s Iteration 65 Queue: [(15,75,2,True), (16,80,2,True), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,1,True), (23,115,1,True), (24,120,0,True)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 66 Time : 550.994s (Solving: 521.22s 1st Model: 0.07s Unsat: 11.73s) CPU Time : 551.056s Choices : 11541864 (Domain: 11299167) Conflicts : 522560 (Analyzed: 522556) Restarts : 6172 (Average: 84.67 Last: 156) Model-Level : 251.0 Problems : 66 (Average Length: 80.18 Splits: 0) Lemmas : 522556 (Deleted: 485968) Binary : 12433 (Ratio: 2.38%) Ternary : 2858 (Ratio: 0.55%) Conflict : 522556 (Average Length: 542.1 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 522556 (Average: 20.20 Max: 1075 Sum: 10556947) Executed : 522428 (Average: 20.19 Max: 1075 Sum: 10550995 Ratio: 99.94%) Bounded : 128 (Average: 46.50 Max: 117 Sum: 5952 Ratio: 0.06%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 843565 (Eliminated: 0 Frozen: 260681) Constraints : 6188944 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1016MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 6.10s Memory: 927MB (+0MB) UNKNOWN Iteration Time: 6.18s Iteration 66 Queue: [(16,80,2,True), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,1,True), (23,115,1,True), (24,120,0,True)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 67 Time : 559.177s (Solving: 529.20s 1st Model: 0.07s Unsat: 11.73s) CPU Time : 559.244s Choices : 11708081 (Domain: 11465007) Conflicts : 530676 (Analyzed: 530672) Restarts : 6272 (Average: 84.61 Last: 156) Model-Level : 251.0 Problems : 67 (Average Length: 80.73 Splits: 0) Lemmas : 530672 (Deleted: 493893) Binary : 12530 (Ratio: 2.36%) Ternary : 2875 (Ratio: 0.54%) Conflict : 530672 (Average Length: 538.8 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 530672 (Average: 20.17 Max: 1075 Sum: 10705980) Executed : 530544 (Average: 20.16 Max: 1075 Sum: 10700028 Ratio: 99.94%) Bounded : 128 (Average: 46.50 Max: 117 Sum: 5952 Ratio: 0.06%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 843565 (Eliminated: 0 Frozen: 260681) Constraints : 6188944 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1016MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 8.11s Memory: 927MB (+0MB) UNKNOWN Iteration Time: 8.19s Iteration 67 Queue: [(22,110,1,True), (23,115,1,True), (24,120,0,True)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 68 Time : 568.017s (Solving: 537.87s 1st Model: 0.07s Unsat: 11.73s) CPU Time : 568.088s Choices : 11908051 (Domain: 11664762) Conflicts : 539322 (Analyzed: 539318) Restarts : 6372 (Average: 84.64 Last: 156) Model-Level : 251.0 Problems : 68 (Average Length: 81.26 Splits: 0) Lemmas : 539318 (Deleted: 503888) Binary : 12638 (Ratio: 2.34%) Ternary : 2884 (Ratio: 0.53%) Conflict : 539318 (Average Length: 534.7 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 539318 (Average: 20.19 Max: 1075 Sum: 10886391) Executed : 539189 (Average: 20.17 Max: 1075 Sum: 10880327 Ratio: 99.94%) Bounded : 129 (Average: 47.01 Max: 117 Sum: 6064 Ratio: 0.06%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 843565 (Eliminated: 0 Frozen: 260681) Constraints : 6188944 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1016MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 8.79s Memory: 927MB (+0MB) UNKNOWN Iteration Time: 8.85s Iteration 68 Queue: [(23,115,1,True), (24,120,0,True)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 69 Time : 574.518s (Solving: 544.16s 1st Model: 0.07s Unsat: 11.73s) CPU Time : 574.592s Choices : 12047760 (Domain: 11804381) Conflicts : 548179 (Analyzed: 548175) Restarts : 6472 (Average: 84.70 Last: 156) Model-Level : 251.0 Problems : 69 (Average Length: 81.78 Splits: 0) Lemmas : 548175 (Deleted: 512269) Binary : 12742 (Ratio: 2.32%) Ternary : 2894 (Ratio: 0.53%) Conflict : 548175 (Average Length: 531.5 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 548175 (Average: 20.08 Max: 1075 Sum: 11006343) Executed : 548046 (Average: 20.07 Max: 1075 Sum: 11000279 Ratio: 99.94%) Bounded : 129 (Average: 47.01 Max: 117 Sum: 6064 Ratio: 0.06%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 843565 (Eliminated: 0 Frozen: 260681) Constraints : 6188944 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1016MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 6.42s Memory: 927MB (+0MB) UNKNOWN Iteration Time: 6.51s Iteration 69 Queue: [(24,120,0,True)] Grounded Until: 115 Expected Memory: 1007.0MB Grounding... [('step', [116]), ('step', [117]), ('step', [118]), ('step', [119]), ('step', [120]), ('check', [120])] Grounding Time: 0.55s Memory: 927MB (+0MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 70 Time : 587.844s (Solving: 556.24s 1st Model: 0.07s Unsat: 11.73s) CPU Time : 587.924s Choices : 12230896 (Domain: 11987474) Conflicts : 557651 (Analyzed: 557647) Restarts : 6572 (Average: 84.85 Last: 156) Model-Level : 251.0 Problems : 70 (Average Length: 82.36 Splits: 0) Lemmas : 557647 (Deleted: 520972) Binary : 12795 (Ratio: 2.29%) Ternary : 2897 (Ratio: 0.52%) Conflict : 557647 (Average Length: 535.3 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 557647 (Average: 19.99 Max: 1251 Sum: 11149909) Executed : 557518 (Average: 19.98 Max: 1251 Sum: 11143845 Ratio: 99.95%) Bounded : 129 (Average: 47.01 Max: 117 Sum: 6064 Ratio: 0.05%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 881056 (Eliminated: 0 Frozen: 272341) Constraints : 6471404 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1048MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 12.23s Memory: 945MB (+18MB) UNKNOWN Iteration Time: 13.34s Iteration 70 Queue: [(5,25,5,True), (6,30,5,True), (7,35,4,True), (8,40,4,True), (9,45,4,True), (10,50,4,True), (11,55,4,False), (12,60,3,True), (13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,3,False), (17,85,2,True), (18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False), (24,120,1,True)] Grounded Until: 120 Blocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 71 Time : 592.054s (Solving: 560.24s 1st Model: 0.07s Unsat: 11.73s) CPU Time : 592.136s Choices : 12274419 (Domain: 12030997) Conflicts : 565316 (Analyzed: 565312) Restarts : 6672 (Average: 84.73 Last: 156) Model-Level : 251.0 Problems : 71 (Average Length: 82.92 Splits: 0) Lemmas : 565312 (Deleted: 528048) Binary : 12842 (Ratio: 2.27%) Ternary : 2901 (Ratio: 0.51%) Conflict : 565312 (Average Length: 531.7 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 565312 (Average: 19.79 Max: 1251 Sum: 11187560) Executed : 565182 (Average: 19.78 Max: 1251 Sum: 11181379 Ratio: 99.94%) Bounded : 130 (Average: 47.55 Max: 117 Sum: 6181 Ratio: 0.06%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 881056 (Eliminated: 0 Frozen: 272341) Constraints : 6471404 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1048MB Max. Length : 120 steps Models : 1 [endof: stats after solve call] Solving Time: 4.13s Memory: 951MB (+6MB) UNKNOWN Iteration Time: 4.22s Iteration 71 Queue: [(6,30,5,True), (7,35,4,True), (8,40,4,True), (9,45,4,True), (10,50,4,True), (11,55,4,False), (12,60,3,True), (13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,3,False), (17,85,2,True), (18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False), (24,120,1,True)] Grounded Until: 120 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 72 Time : 599.780s (Solving: 567.79s 1st Model: 0.07s Unsat: 11.73s) CPU Time : 599.864s Choices : 12331284 (Domain: 12087862) Conflicts : 573401 (Analyzed: 573397) Restarts : 6772 (Average: 84.67 Last: 156) Model-Level : 251.0 Problems : 72 (Average Length: 83.46 Splits: 0) Lemmas : 573397 (Deleted: 535492) Binary : 12961 (Ratio: 2.26%) Ternary : 2915 (Ratio: 0.51%) Conflict : 573397 (Average Length: 543.2 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 573397 (Average: 19.58 Max: 1251 Sum: 11228500) Executed : 573265 (Average: 19.57 Max: 1251 Sum: 11222075 Ratio: 99.94%) Bounded : 132 (Average: 48.67 Max: 122 Sum: 6425 Ratio: 0.06%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 881056 (Eliminated: 0 Frozen: 272341) Constraints : 6471404 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1048MB Max. Length : 120 steps Models : 1 [endof: stats after solve call] Solving Time: 7.67s Memory: 951MB (+0MB) UNKNOWN Iteration Time: 7.73s Iteration 72 Queue: [(7,35,4,True), (8,40,4,True), (9,45,4,True), (10,50,4,True), (11,55,4,False), (12,60,3,True), (13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,3,False), (17,85,2,True), (18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False), (24,120,1,True)] Grounded Until: 120 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 73 Time : 604.310s (Solving: 572.14s 1st Model: 0.07s Unsat: 11.73s) CPU Time : 604.396s Choices : 12388157 (Domain: 12143984) Conflicts : 581175 (Analyzed: 581171) Restarts : 6872 (Average: 84.57 Last: 156) Model-Level : 251.0 Problems : 73 (Average Length: 83.99 Splits: 0) Lemmas : 581171 (Deleted: 543337) Binary : 13009 (Ratio: 2.24%) Ternary : 2922 (Ratio: 0.50%) Conflict : 581171 (Average Length: 539.8 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 581171 (Average: 19.40 Max: 1251 Sum: 11275940) Executed : 581039 (Average: 19.39 Max: 1251 Sum: 11269515 Ratio: 99.94%) Bounded : 132 (Average: 48.67 Max: 122 Sum: 6425 Ratio: 0.06%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 881056 (Eliminated: 0 Frozen: 272341) Constraints : 6468928 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1048MB Max. Length : 120 steps Models : 1 [endof: stats after solve call] Solving Time: 4.47s Memory: 951MB (+0MB) UNKNOWN Iteration Time: 4.54s Iteration 73 Queue: [(8,40,4,True), (9,45,4,True), (10,50,4,True), (11,55,4,False), (12,60,3,True), (13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,3,False), (17,85,2,True), (18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False), (24,120,1,True)] Grounded Until: 120 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 74 Time : 609.227s (Solving: 576.85s 1st Model: 0.07s Unsat: 11.73s) CPU Time : 609.316s Choices : 12450398 (Domain: 12206165) Conflicts : 589246 (Analyzed: 589242) Restarts : 6972 (Average: 84.52 Last: 156) Model-Level : 251.0 Problems : 74 (Average Length: 84.50 Splits: 0) Lemmas : 589242 (Deleted: 550901) Binary : 13068 (Ratio: 2.22%) Ternary : 2941 (Ratio: 0.50%) Conflict : 589242 (Average Length: 536.6 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 589242 (Average: 19.23 Max: 1251 Sum: 11328485) Executed : 589110 (Average: 19.21 Max: 1251 Sum: 11322060 Ratio: 99.94%) Bounded : 132 (Average: 48.67 Max: 122 Sum: 6425 Ratio: 0.06%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 881056 (Eliminated: 0 Frozen: 272341) Constraints : 6468928 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1048MB Max. Length : 120 steps Models : 1 [endof: stats after solve call] Solving Time: 4.84s Memory: 951MB (+0MB) UNKNOWN Iteration Time: 4.92s Iteration 74 Queue: [(9,45,4,True), (10,50,4,True), (11,55,4,False), (12,60,3,True), (13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,3,False), (17,85,2,True), (18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False), (24,120,1,True)] Grounded Until: 120 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 75 Time : 615.467s (Solving: 582.91s 1st Model: 0.07s Unsat: 11.73s) CPU Time : 615.560s Choices : 12534348 (Domain: 12289844) Conflicts : 597354 (Analyzed: 597350) Restarts : 7072 (Average: 84.47 Last: 156) Model-Level : 251.0 Problems : 75 (Average Length: 85.00 Splits: 0) Lemmas : 597350 (Deleted: 558717) Binary : 13138 (Ratio: 2.20%) Ternary : 2943 (Ratio: 0.49%) Conflict : 597350 (Average Length: 534.0 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 597350 (Average: 19.09 Max: 1251 Sum: 11400868) Executed : 597217 (Average: 19.07 Max: 1251 Sum: 11394321 Ratio: 99.94%) Bounded : 133 (Average: 49.23 Max: 122 Sum: 6547 Ratio: 0.06%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 881056 (Eliminated: 0 Frozen: 272341) Constraints : 6468928 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1048MB Max. Length : 120 steps Models : 1 [endof: stats after solve call] Solving Time: 6.18s Memory: 951MB (+0MB) UNKNOWN Iteration Time: 6.25s Iteration 75 Queue: [(10,50,4,True), (11,55,4,False), (12,60,3,True), (13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,3,False), (17,85,2,True), (18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False), (24,120,1,True)] Grounded Until: 120 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 76 Time : 621.430s (Solving: 588.68s 1st Model: 0.07s Unsat: 11.73s) CPU Time : 621.524s Choices : 12606874 (Domain: 12362239) Conflicts : 605822 (Analyzed: 605818) Restarts : 7172 (Average: 84.47 Last: 156) Model-Level : 251.0 Problems : 76 (Average Length: 85.49 Splits: 0) Lemmas : 605818 (Deleted: 566586) Binary : 13230 (Ratio: 2.18%) Ternary : 2953 (Ratio: 0.49%) Conflict : 605818 (Average Length: 530.6 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 605818 (Average: 18.92 Max: 1251 Sum: 11462312) Executed : 605684 (Average: 18.91 Max: 1251 Sum: 11455643 Ratio: 99.94%) Bounded : 134 (Average: 49.77 Max: 122 Sum: 6669 Ratio: 0.06%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 881056 (Eliminated: 0 Frozen: 272341) Constraints : 6468915 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1048MB Max. Length : 120 steps Models : 1 [endof: stats after solve call] Solving Time: 5.90s Memory: 951MB (+0MB) UNKNOWN Iteration Time: 5.97s Iteration 76 Queue: [(12,60,3,True), (13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,3,False), (17,85,2,True), (18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False), (24,120,1,True)] Grounded Until: 120 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 77 Time : 631.348s (Solving: 598.39s 1st Model: 0.07s Unsat: 11.73s) CPU Time : 631.444s Choices : 12745085 (Domain: 12500208) Conflicts : 615251 (Analyzed: 615247) Restarts : 7272 (Average: 84.60 Last: 156) Model-Level : 251.0 Problems : 77 (Average Length: 85.96 Splits: 0) Lemmas : 615247 (Deleted: 576945) Binary : 13385 (Ratio: 2.18%) Ternary : 2968 (Ratio: 0.48%) Conflict : 615247 (Average Length: 529.3 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 615247 (Average: 18.83 Max: 1251 Sum: 11584576) Executed : 615113 (Average: 18.82 Max: 1251 Sum: 11577907 Ratio: 99.94%) Bounded : 134 (Average: 49.77 Max: 122 Sum: 6669 Ratio: 0.06%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 881056 (Eliminated: 0 Frozen: 272341) Constraints : 6468901 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1048MB Max. Length : 120 steps Models : 1 [endof: stats after solve call] Solving Time: 9.85s Memory: 951MB (+0MB) UNKNOWN Iteration Time: 9.93s Iteration 77 Queue: [(13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,3,False), (17,85,2,True), (18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False), (24,120,1,True)] Grounded Until: 120 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 78 Time : 637.526s (Solving: 604.40s 1st Model: 0.07s Unsat: 11.73s) CPU Time : 637.616s Choices : 12840301 (Domain: 12595227) Conflicts : 623777 (Analyzed: 623773) Restarts : 7372 (Average: 84.61 Last: 156) Model-Level : 251.0 Problems : 78 (Average Length: 86.42 Splits: 0) Lemmas : 623773 (Deleted: 583858) Binary : 13468 (Ratio: 2.16%) Ternary : 2973 (Ratio: 0.48%) Conflict : 623773 (Average Length: 527.0 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 623773 (Average: 18.70 Max: 1251 Sum: 11665137) Executed : 623639 (Average: 18.69 Max: 1251 Sum: 11658468 Ratio: 99.94%) Bounded : 134 (Average: 49.77 Max: 122 Sum: 6669 Ratio: 0.06%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 881056 (Eliminated: 0 Frozen: 272341) Constraints : 6468901 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1048MB Max. Length : 120 steps Models : 1 [endof: stats after solve call] Solving Time: 6.11s Memory: 951MB (+0MB) UNKNOWN Iteration Time: 6.17s Iteration 78 Queue: [(17,85,2,True), (18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False), (24,120,1,True)] Grounded Until: 120 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 79 Time : 644.934s (Solving: 611.63s 1st Model: 0.07s Unsat: 11.73s) CPU Time : 645.024s Choices : 12990926 (Domain: 12745618) Conflicts : 632710 (Analyzed: 632706) Restarts : 7472 (Average: 84.68 Last: 156) Model-Level : 251.0 Problems : 79 (Average Length: 86.87 Splits: 0) Lemmas : 632706 (Deleted: 594227) Binary : 13570 (Ratio: 2.14%) Ternary : 2988 (Ratio: 0.47%) Conflict : 632706 (Average Length: 525.4 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 632706 (Average: 18.65 Max: 1251 Sum: 11798054) Executed : 632571 (Average: 18.64 Max: 1251 Sum: 11791263 Ratio: 99.94%) Bounded : 135 (Average: 50.30 Max: 122 Sum: 6791 Ratio: 0.06%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 881056 (Eliminated: 0 Frozen: 272341) Constraints : 6468901 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1048MB Max. Length : 120 steps Models : 1 [endof: stats after solve call] Solving Time: 7.35s Memory: 951MB (+0MB) UNKNOWN Iteration Time: 7.41s Iteration 79 Queue: [(18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False), (24,120,1,True)] Grounded Until: 120 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 80 Time : 651.915s (Solving: 618.41s 1st Model: 0.07s Unsat: 11.73s) CPU Time : 652.008s Choices : 13064093 (Domain: 12818779) Conflicts : 640944 (Analyzed: 640940) Restarts : 7572 (Average: 84.65 Last: 156) Model-Level : 251.0 Problems : 80 (Average Length: 87.31 Splits: 0) Lemmas : 640940 (Deleted: 600744) Binary : 13612 (Ratio: 2.12%) Ternary : 2991 (Ratio: 0.47%) Conflict : 640940 (Average Length: 522.7 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 640940 (Average: 18.50 Max: 1251 Sum: 11856447) Executed : 640804 (Average: 18.49 Max: 1251 Sum: 11849534 Ratio: 99.94%) Bounded : 136 (Average: 50.83 Max: 122 Sum: 6913 Ratio: 0.06%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 881056 (Eliminated: 0 Frozen: 272341) Constraints : 6468887 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1048MB Max. Length : 120 steps Models : 1 [endof: stats after solve call] Solving Time: 6.91s Memory: 951MB (+0MB) UNKNOWN Iteration Time: 6.99s Iteration 80 Queue: [(24,120,1,True)] Grounded Until: 120 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 81 Time : 662.305s (Solving: 628.62s 1st Model: 0.07s Unsat: 11.73s) CPU Time : 662.400s Choices : 13283271 (Domain: 13037641) Conflicts : 649889 (Analyzed: 649885) Restarts : 7672 (Average: 84.71 Last: 156) Model-Level : 251.0 Problems : 81 (Average Length: 87.74 Splits: 0) Lemmas : 649885 (Deleted: 610894) Binary : 13715 (Ratio: 2.11%) Ternary : 3007 (Ratio: 0.46%) Conflict : 649885 (Average Length: 521.8 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 649885 (Average: 18.55 Max: 1251 Sum: 12052144) Executed : 649749 (Average: 18.53 Max: 1251 Sum: 12045231 Ratio: 99.94%) Bounded : 136 (Average: 50.83 Max: 122 Sum: 6913 Ratio: 0.06%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 881056 (Eliminated: 0 Frozen: 272341) Constraints : 6468873 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1048MB Max. Length : 120 steps Models : 1 [endof: stats after solve call] Solving Time: 10.33s Memory: 951MB (+0MB) UNKNOWN Iteration Time: 10.40s Iteration 81 Queue: [(5,25,6,True), (6,30,6,True), (7,35,5,True), (8,40,5,True), (9,45,5,True), (10,50,5,False), (11,55,4,True), (12,60,4,False), (13,65,4,False), (14,70,3,True), (15,75,3,False), (16,80,3,False), (17,85,3,False), (18,90,3,False), (19,95,2,True), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False), (24,120,2,False)] Grounded Until: 120 Blocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 82 Time : 672.185s (Solving: 638.32s 1st Model: 0.07s Unsat: 11.73s) CPU Time : 672.284s Choices : 13337257 (Domain: 13091627) Conflicts : 658070 (Analyzed: 658066) Restarts : 7772 (Average: 84.67 Last: 156) Model-Level : 251.0 Problems : 82 (Average Length: 88.16 Splits: 0) Lemmas : 658066 (Deleted: 617231) Binary : 13785 (Ratio: 2.09%) Ternary : 3023 (Ratio: 0.46%) Conflict : 658066 (Average Length: 527.6 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 658066 (Average: 18.38 Max: 1251 Sum: 12092844) Executed : 657930 (Average: 18.37 Max: 1251 Sum: 12085931 Ratio: 99.94%) Bounded : 136 (Average: 50.83 Max: 122 Sum: 6913 Ratio: 0.06%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 881056 (Eliminated: 0 Frozen: 272341) Constraints : 6468873 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1048MB Max. Length : 120 steps Models : 1 [endof: stats after solve call] Solving Time: 9.82s Memory: 951MB (+0MB) UNKNOWN Iteration Time: 9.89s Iteration 82 Queue: [(6,30,6,True), (7,35,5,True), (8,40,5,True), (9,45,5,True), (10,50,5,False), (11,55,4,True), (12,60,4,False), (13,65,4,False), (14,70,3,True), (15,75,3,False), (16,80,3,False), (17,85,3,False), (18,90,3,False), (19,95,2,True), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False), (24,120,2,False)] Grounded Until: 120 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 83 Time : 675.796s (Solving: 641.71s 1st Model: 0.07s Unsat: 11.73s) CPU Time : 675.896s Choices : 13377378 (Domain: 13131748) Conflicts : 665295 (Analyzed: 665291) Restarts : 7872 (Average: 84.51 Last: 156) Model-Level : 251.0 Problems : 83 (Average Length: 88.57 Splits: 0) Lemmas : 665291 (Deleted: 625249) Binary : 13809 (Ratio: 2.08%) Ternary : 3024 (Ratio: 0.45%) Conflict : 665291 (Average Length: 524.0 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 665291 (Average: 18.23 Max: 1251 Sum: 12125089) Executed : 665155 (Average: 18.21 Max: 1251 Sum: 12118176 Ratio: 99.94%) Bounded : 136 (Average: 50.83 Max: 122 Sum: 6913 Ratio: 0.06%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 881056 (Eliminated: 0 Frozen: 272341) Constraints : 6468873 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1048MB Max. Length : 120 steps Models : 1 [endof: stats after solve call] Solving Time: 3.53s Memory: 951MB (+0MB) UNKNOWN Iteration Time: 3.62s Iteration 83 Queue: [(7,35,5,True), (8,40,5,True), (9,45,5,True), (10,50,5,False), (11,55,4,True), (12,60,4,False), (13,65,4,False), (14,70,3,True), (15,75,3,False), (16,80,3,False), (17,85,3,False), (18,90,3,False), (19,95,2,True), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False), (24,120,2,False)] Grounded Until: 120 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 84 Time : 679.353s (Solving: 645.09s 1st Model: 0.07s Unsat: 11.73s) CPU Time : 679.456s Choices : 13425656 (Domain: 13179993) Conflicts : 672988 (Analyzed: 672984) Restarts : 7972 (Average: 84.42 Last: 156) Model-Level : 251.0 Problems : 84 (Average Length: 88.96 Splits: 0) Lemmas : 672984 (Deleted: 632372) Binary : 13826 (Ratio: 2.05%) Ternary : 3026 (Ratio: 0.45%) Conflict : 672984 (Average Length: 520.9 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 672984 (Average: 18.08 Max: 1251 Sum: 12165299) Executed : 672848 (Average: 18.07 Max: 1251 Sum: 12158386 Ratio: 99.94%) Bounded : 136 (Average: 50.83 Max: 122 Sum: 6913 Ratio: 0.06%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 881056 (Eliminated: 0 Frozen: 272341) Constraints : 6468873 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1048MB Max. Length : 120 steps Models : 1 [endof: stats after solve call] Solving Time: 3.50s Memory: 951MB (+0MB) UNKNOWN Iteration Time: 3.56s Iteration 84 Queue: [(8,40,5,True), (9,45,5,True), (10,50,5,False), (11,55,4,True), (12,60,4,False), (13,65,4,False), (14,70,3,True), (15,75,3,False), (16,80,3,False), (17,85,3,False), (18,90,3,False), (19,95,2,True), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False), (24,120,2,False)] Grounded Until: 120 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 85 Time : 686.314s (Solving: 651.85s 1st Model: 0.07s Unsat: 11.73s) CPU Time : 686.412s Choices : 13499104 (Domain: 13252923) Conflicts : 681243 (Analyzed: 681239) Restarts : 8072 (Average: 84.40 Last: 156) Model-Level : 251.0 Problems : 85 (Average Length: 89.35 Splits: 0) Lemmas : 681239 (Deleted: 639894) Binary : 13918 (Ratio: 2.04%) Ternary : 3036 (Ratio: 0.45%) Conflict : 681239 (Average Length: 519.0 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 681239 (Average: 17.95 Max: 1251 Sum: 12227614) Executed : 681103 (Average: 17.94 Max: 1251 Sum: 12220701 Ratio: 99.94%) Bounded : 136 (Average: 50.83 Max: 122 Sum: 6913 Ratio: 0.06%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 881056 (Eliminated: 0 Frozen: 272341) Constraints : 6468873 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1048MB Max. Length : 120 steps Models : 1 [endof: stats after solve call] Solving Time: 6.88s Memory: 951MB (+0MB) UNKNOWN Iteration Time: 6.96s Iteration 85 Queue: [(9,45,5,True), (10,50,5,False), (11,55,4,True), (12,60,4,False), (13,65,4,False), (14,70,3,True), (15,75,3,False), (16,80,3,False), (17,85,3,False), (18,90,3,False), (19,95,2,True), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False), (24,120,2,False)] Grounded Until: 120 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 86 Time : 693.390s (Solving: 658.75s 1st Model: 0.07s Unsat: 11.73s) CPU Time : 693.480s Choices : 13598005 (Domain: 13351528) Conflicts : 689711 (Analyzed: 689707) Restarts : 8172 (Average: 84.40 Last: 156) Model-Level : 251.0 Problems : 86 (Average Length: 89.73 Splits: 0) Lemmas : 689707 (Deleted: 647946) Binary : 13991 (Ratio: 2.03%) Ternary : 3050 (Ratio: 0.44%) Conflict : 689707 (Average Length: 517.7 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 689707 (Average: 17.85 Max: 1251 Sum: 12312506) Executed : 689571 (Average: 17.84 Max: 1251 Sum: 12305593 Ratio: 99.94%) Bounded : 136 (Average: 50.83 Max: 122 Sum: 6913 Ratio: 0.06%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 881056 (Eliminated: 0 Frozen: 272341) Constraints : 6468873 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1048MB Max. Length : 120 steps Models : 1 [endof: stats after solve call] Solving Time: 7.00s Memory: 951MB (+0MB) UNKNOWN Iteration Time: 7.07s Iteration 86 Queue: [(11,55,4,True), (12,60,4,False), (13,65,4,False), (14,70,3,True), (15,75,3,False), (16,80,3,False), (17,85,3,False), (18,90,3,False), (19,95,2,True), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False), (24,120,2,False)] Grounded Until: 120 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 87 Time : 702.439s (Solving: 667.62s 1st Model: 0.07s Unsat: 11.73s) CPU Time : 702.532s Choices : 13725705 (Domain: 13478968) Conflicts : 698962 (Analyzed: 698958) Restarts : 8272 (Average: 84.50 Last: 156) Model-Level : 251.0 Problems : 87 (Average Length: 90.10 Splits: 0) Lemmas : 698958 (Deleted: 658186) Binary : 14086 (Ratio: 2.02%) Ternary : 3069 (Ratio: 0.44%) Conflict : 698958 (Average Length: 517.1 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 698958 (Average: 17.78 Max: 1251 Sum: 12424271) Executed : 698822 (Average: 17.77 Max: 1251 Sum: 12417358 Ratio: 99.94%) Bounded : 136 (Average: 50.83 Max: 122 Sum: 6913 Ratio: 0.06%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 881056 (Eliminated: 0 Frozen: 272341) Constraints : 6468873 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1048MB Max. Length : 120 steps Models : 1 [endof: stats after solve call] Solving Time: 9.00s Memory: 951MB (+0MB) UNKNOWN Iteration Time: 9.06s Iteration 87 Queue: [(14,70,3,True), (15,75,3,False), (16,80,3,False), (17,85,3,False), (18,90,3,False), (19,95,2,True), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False), (24,120,2,False)] Grounded Until: 120 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 88 Time : 711.949s (Solving: 676.95s 1st Model: 0.07s Unsat: 11.73s) CPU Time : 712.044s Choices : 13886763 (Domain: 13639450) Conflicts : 707595 (Analyzed: 707591) Restarts : 8372 (Average: 84.52 Last: 156) Model-Level : 251.0 Problems : 88 (Average Length: 90.47 Splits: 0) Lemmas : 707591 (Deleted: 667058) Binary : 14222 (Ratio: 2.01%) Ternary : 3077 (Ratio: 0.43%) Conflict : 707591 (Average Length: 516.4 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 707591 (Average: 17.76 Max: 1251 Sum: 12567182) Executed : 707455 (Average: 17.75 Max: 1251 Sum: 12560269 Ratio: 99.94%) Bounded : 136 (Average: 50.83 Max: 122 Sum: 6913 Ratio: 0.06%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 881056 (Eliminated: 0 Frozen: 272341) Constraints : 6468873 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1048MB Max. Length : 120 steps Models : 1 [endof: stats after solve call] Solving Time: 9.45s Memory: 951MB (+0MB) UNKNOWN Iteration Time: 9.52s Iteration 88 Queue: [(19,95,2,True), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False), (24,120,2,False)] Grounded Until: 120 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 89 Time : 721.091s (Solving: 685.92s 1st Model: 0.07s Unsat: 11.73s) CPU Time : 721.192s Choices : 14059637 (Domain: 13812265) Conflicts : 716080 (Analyzed: 716076) Restarts : 8472 (Average: 84.52 Last: 156) Model-Level : 251.0 Problems : 89 (Average Length: 90.82 Splits: 0) Lemmas : 716076 (Deleted: 673327) Binary : 14329 (Ratio: 2.00%) Ternary : 3090 (Ratio: 0.43%) Conflict : 716076 (Average Length: 515.8 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 716076 (Average: 17.76 Max: 1251 Sum: 12720490) Executed : 715940 (Average: 17.75 Max: 1251 Sum: 12713577 Ratio: 99.95%) Bounded : 136 (Average: 50.83 Max: 122 Sum: 6913 Ratio: 0.05%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 881056 (Eliminated: 0 Frozen: 272341) Constraints : 6468873 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1048MB Max. Length : 120 steps Models : 1 [endof: stats after solve call] Solving Time: 9.09s Memory: 951MB (+0MB) UNKNOWN Iteration Time: 9.15s Iteration 89 Queue: [(5,25,7,True), (6,30,7,True), (7,35,6,True), (8,40,6,True), (9,45,6,False), (10,50,5,True), (11,55,5,False), (12,60,4,True), (13,65,4,False), (14,70,4,False), (15,75,3,True), (16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,False), (22,110,2,False), (23,115,2,False), (24,120,2,False)] Grounded Until: 120 Blocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 90 Time : 732.579s (Solving: 697.20s 1st Model: 0.07s Unsat: 11.73s) CPU Time : 732.684s Choices : 14100867 (Domain: 13853495) Conflicts : 724077 (Analyzed: 724073) Restarts : 8572 (Average: 84.47 Last: 156) Model-Level : 251.0 Problems : 90 (Average Length: 91.17 Splits: 0) Lemmas : 724073 (Deleted: 681409) Binary : 14360 (Ratio: 1.98%) Ternary : 3100 (Ratio: 0.43%) Conflict : 724073 (Average Length: 525.9 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 724073 (Average: 17.60 Max: 1251 Sum: 12747146) Executed : 723937 (Average: 17.60 Max: 1251 Sum: 12740233 Ratio: 99.95%) Bounded : 136 (Average: 50.83 Max: 122 Sum: 6913 Ratio: 0.05%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 881056 (Eliminated: 0 Frozen: 272341) Constraints : 6468873 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1048MB Max. Length : 120 steps Models : 1 [endof: stats after solve call] Solving Time: 11.42s Memory: 951MB (+0MB) UNKNOWN Iteration Time: 11.50s Iteration 90 Queue: [(6,30,7,True), (7,35,6,True), (8,40,6,True), (9,45,6,False), (10,50,5,True), (11,55,5,False), (12,60,4,True), (13,65,4,False), (14,70,4,False), (15,75,3,True), (16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,False), (22,110,2,False), (23,115,2,False), (24,120,2,False)] Grounded Until: 120 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 91 Time : 743.153s (Solving: 707.60s 1st Model: 0.07s Unsat: 11.73s) CPU Time : 743.264s Choices : 14181205 (Domain: 13933833) Conflicts : 732907 (Analyzed: 732903) Restarts : 8672 (Average: 84.51 Last: 156) Model-Level : 251.0 Problems : 91 (Average Length: 91.51 Splits: 0) Lemmas : 732903 (Deleted: 691313) Binary : 14488 (Ratio: 1.98%) Ternary : 3115 (Ratio: 0.43%) Conflict : 732903 (Average Length: 534.0 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 732903 (Average: 17.48 Max: 1251 Sum: 12810514) Executed : 732767 (Average: 17.47 Max: 1251 Sum: 12803601 Ratio: 99.95%) Bounded : 136 (Average: 50.83 Max: 122 Sum: 6913 Ratio: 0.05%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 881056 (Eliminated: 0 Frozen: 272341) Constraints : 6468873 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1048MB Max. Length : 120 steps Models : 1 [endof: stats after solve call] Solving Time: 10.51s Memory: 951MB (+0MB) UNKNOWN Iteration Time: 10.58s Iteration 91 Queue: [(7,35,6,True), (8,40,6,True), (9,45,6,False), (10,50,5,True), (11,55,5,False), (12,60,4,True), (13,65,4,False), (14,70,4,False), (15,75,3,True), (16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,False), (22,110,2,False), (23,115,2,False), (24,120,2,False)] Grounded Until: 120 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 92 Time : 751.909s (Solving: 716.15s 1st Model: 0.07s Unsat: 11.73s) CPU Time : 752.024s Choices : 14274384 (Domain: 14025315) Conflicts : 741979 (Analyzed: 741975) Restarts : 8772 (Average: 84.58 Last: 156) Model-Level : 251.0 Problems : 92 (Average Length: 91.84 Splits: 0) Lemmas : 741975 (Deleted: 699712) Binary : 14683 (Ratio: 1.98%) Ternary : 3138 (Ratio: 0.42%) Conflict : 741975 (Average Length: 536.0 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 741975 (Average: 17.36 Max: 1251 Sum: 12884042) Executed : 741839 (Average: 17.36 Max: 1251 Sum: 12877129 Ratio: 99.95%) Bounded : 136 (Average: 50.83 Max: 122 Sum: 6913 Ratio: 0.05%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 881056 (Eliminated: 0 Frozen: 272341) Constraints : 6468873 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1048MB Max. Length : 120 steps Models : 1 [endof: stats after solve call] Solving Time: 8.68s Memory: 951MB (+0MB) UNKNOWN Iteration Time: 8.76s Iteration 92 Queue: [(8,40,6,True), (9,45,6,False), (10,50,5,True), (11,55,5,False), (12,60,4,True), (13,65,4,False), (14,70,4,False), (15,75,3,True), (16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,False), (22,110,2,False), (23,115,2,False), (24,120,2,False)] Grounded Until: 120 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 93 Time : 760.968s (Solving: 725.03s 1st Model: 0.07s Unsat: 11.73s) CPU Time : 761.084s Choices : 14345501 (Domain: 14096386) Conflicts : 749879 (Analyzed: 749875) Restarts : 8872 (Average: 84.52 Last: 156) Model-Level : 251.0 Problems : 93 (Average Length: 92.16 Splits: 0) Lemmas : 749875 (Deleted: 706140) Binary : 14752 (Ratio: 1.97%) Ternary : 3145 (Ratio: 0.42%) Conflict : 749875 (Average Length: 540.6 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 749875 (Average: 17.26 Max: 1251 Sum: 12939485) Executed : 749739 (Average: 17.25 Max: 1251 Sum: 12932572 Ratio: 99.95%) Bounded : 136 (Average: 50.83 Max: 122 Sum: 6913 Ratio: 0.05%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 881056 (Eliminated: 0 Frozen: 272341) Constraints : 6468873 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1048MB Max. Length : 120 steps Models : 1 [endof: stats after solve call] Solving Time: 9.00s Memory: 951MB (+0MB) UNKNOWN Iteration Time: 9.07s Iteration 93 Queue: [(10,50,5,True), (11,55,5,False), (12,60,4,True), (13,65,4,False), (14,70,4,False), (15,75,3,True), (16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,False), (22,110,2,False), (23,115,2,False), (24,120,2,False)] Grounded Until: 120 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 94 Time : 765.766s (Solving: 729.65s 1st Model: 0.07s Unsat: 11.73s) CPU Time : 765.880s Choices : 14413522 (Domain: 14164389) Conflicts : 758025 (Analyzed: 758021) Restarts : 8972 (Average: 84.49 Last: 156) Model-Level : 251.0 Problems : 94 (Average Length: 92.48 Splits: 0) Lemmas : 758021 (Deleted: 713728) Binary : 14787 (Ratio: 1.95%) Ternary : 3160 (Ratio: 0.42%) Conflict : 758021 (Average Length: 537.6 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 758021 (Average: 17.15 Max: 1251 Sum: 12997739) Executed : 757882 (Average: 17.14 Max: 1251 Sum: 12990466 Ratio: 99.94%) Bounded : 139 (Average: 52.32 Max: 122 Sum: 7273 Ratio: 0.06%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 881056 (Eliminated: 0 Frozen: 272341) Constraints : 6468873 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1048MB Max. Length : 120 steps Models : 1 [endof: stats after solve call] Solving Time: 4.73s Memory: 951MB (+0MB) UNKNOWN Iteration Time: 4.80s Iteration 94 Queue: [(12,60,4,True), (13,65,4,False), (14,70,4,False), (15,75,3,True), (16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,False), (22,110,2,False), (23,115,2,False), (24,120,2,False)] Grounded Until: 120 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 95 Time : 771.423s (Solving: 735.10s 1st Model: 0.07s Unsat: 11.73s) CPU Time : 771.532s Choices : 14498861 (Domain: 14249452) Conflicts : 766363 (Analyzed: 766359) Restarts : 9072 (Average: 84.48 Last: 156) Model-Level : 251.0 Problems : 95 (Average Length: 92.79 Splits: 0) Lemmas : 766359 (Deleted: 721649) Binary : 14850 (Ratio: 1.94%) Ternary : 3190 (Ratio: 0.42%) Conflict : 766359 (Average Length: 535.3 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 766359 (Average: 17.05 Max: 1251 Sum: 13070078) Executed : 766220 (Average: 17.05 Max: 1251 Sum: 13062805 Ratio: 99.94%) Bounded : 139 (Average: 52.32 Max: 122 Sum: 7273 Ratio: 0.06%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 881056 (Eliminated: 0 Frozen: 272341) Constraints : 6468859 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1048MB Max. Length : 120 steps Models : 1 [endof: stats after solve call] Solving Time: 5.57s Memory: 951MB (+0MB) UNKNOWN Iteration Time: 5.65s Iteration 95 Queue: [(15,75,3,True), (16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,False), (22,110,2,False), (23,115,2,False), (24,120,2,False)] Grounded Until: 120 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 96 Time : 780.173s (Solving: 743.65s 1st Model: 0.07s Unsat: 11.73s) CPU Time : 780.272s Choices : 14675328 (Domain: 14425529) Conflicts : 775282 (Analyzed: 775278) Restarts : 9172 (Average: 84.53 Last: 156) Model-Level : 251.0 Problems : 96 (Average Length: 93.09 Splits: 0) Lemmas : 775278 (Deleted: 731774) Binary : 14940 (Ratio: 1.93%) Ternary : 3241 (Ratio: 0.42%) Conflict : 775278 (Average Length: 533.6 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 775278 (Average: 17.06 Max: 1251 Sum: 13226041) Executed : 775138 (Average: 17.05 Max: 1251 Sum: 13218646 Ratio: 99.94%) Bounded : 140 (Average: 52.82 Max: 122 Sum: 7395 Ratio: 0.06%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 881056 (Eliminated: 0 Frozen: 272341) Constraints : 6468859 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1048MB Max. Length : 120 steps Models : 1 [endof: stats after solve call] Solving Time: 8.67s Memory: 951MB (+0MB) UNKNOWN Iteration Time: 8.74s Iteration 96 Queue: [(16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,False), (22,110,2,False), (23,115,2,False), (24,120,2,False)] Grounded Until: 120 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 97 Time : 787.232s (Solving: 750.51s 1st Model: 0.07s Unsat: 11.73s) CPU Time : 787.332s Choices : 14784362 (Domain: 14534491) Conflicts : 784058 (Analyzed: 784054) Restarts : 9272 (Average: 84.56 Last: 175) Model-Level : 251.0 Problems : 97 (Average Length: 93.39 Splits: 0) Lemmas : 784054 (Deleted: 740441) Binary : 14984 (Ratio: 1.91%) Ternary : 3242 (Ratio: 0.41%) Conflict : 784054 (Average Length: 532.6 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 784054 (Average: 16.99 Max: 1251 Sum: 13317516) Executed : 783913 (Average: 16.98 Max: 1251 Sum: 13310001 Ratio: 99.94%) Bounded : 141 (Average: 53.30 Max: 122 Sum: 7515 Ratio: 0.06%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 881056 (Eliminated: 0 Frozen: 272341) Constraints : 6468845 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1048MB Max. Length : 120 steps Models : 1 [endof: stats after solve call] Solving Time: 6.99s Memory: 951MB (+0MB) UNKNOWN Iteration Time: 7.06s Iteration 97 Queue: [(20,100,2,True), (21,105,2,False), (22,110,2,False), (23,115,2,False), (24,120,2,False)] Grounded Until: 120 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 98 Time : 796.625s (Solving: 759.73s 1st Model: 0.07s Unsat: 11.73s) CPU Time : 796.728s Choices : 14965365 (Domain: 14715389) Conflicts : 792908 (Analyzed: 792904) Restarts : 9372 (Average: 84.60 Last: 175) Model-Level : 251.0 Problems : 98 (Average Length: 93.68 Splits: 0) Lemmas : 792904 (Deleted: 749033) Binary : 15063 (Ratio: 1.90%) Ternary : 3255 (Ratio: 0.41%) Conflict : 792904 (Average Length: 532.4 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 792904 (Average: 16.99 Max: 1251 Sum: 13475352) Executed : 792763 (Average: 16.99 Max: 1251 Sum: 13467837 Ratio: 99.94%) Bounded : 141 (Average: 53.30 Max: 122 Sum: 7515 Ratio: 0.06%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 881056 (Eliminated: 0 Frozen: 272341) Constraints : 6468845 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1048MB Max. Length : 120 steps Models : 1 [endof: stats after solve call] Solving Time: 9.34s Memory: 951MB (+0MB) UNKNOWN Iteration Time: 9.40s Iteration 98 Queue: [(5,25,8,True), (6,30,8,True), (7,35,7,True), (8,40,7,True), (9,45,6,True), (10,50,6,False), (11,55,5,True), (12,60,5,False), (13,65,4,True), (14,70,4,False), (15,75,4,False), (16,80,4,False), (17,85,3,True), (18,90,3,False), (19,95,3,False), (20,100,3,False), (21,105,2,True), (22,110,2,True), (23,115,2,False), (24,120,2,False)] Grounded Until: 120 Blocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 99 Time : 808.948s (Solving: 771.88s 1st Model: 0.07s Unsat: 11.73s) CPU Time : 809.056s Choices : 15007662 (Domain: 14757686) Conflicts : 801451 (Analyzed: 801447) Restarts : 9472 (Average: 84.61 Last: 175) Model-Level : 251.0 Problems : 99 (Average Length: 93.97 Splits: 0) Lemmas : 801447 (Deleted: 755408) Binary : 15082 (Ratio: 1.88%) Ternary : 3261 (Ratio: 0.41%) Conflict : 801447 (Average Length: 541.8 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 801447 (Average: 16.85 Max: 1251 Sum: 13502815) Executed : 801306 (Average: 16.84 Max: 1251 Sum: 13495300 Ratio: 99.94%) Bounded : 141 (Average: 53.30 Max: 122 Sum: 7515 Ratio: 0.06%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 881056 (Eliminated: 0 Frozen: 272341) Constraints : 6468845 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1048MB Max. Length : 120 steps Models : 1 [endof: stats after solve call] Solving Time: 12.27s Memory: 951MB (+0MB) UNKNOWN Iteration Time: 12.33s Iteration 99 Queue: [(6,30,8,True), (7,35,7,True), (8,40,7,True), (9,45,6,True), (10,50,6,False), (11,55,5,True), (12,60,5,False), (13,65,4,True), (14,70,4,False), (15,75,4,False), (16,80,4,False), (17,85,3,True), (18,90,3,False), (19,95,3,False), (20,100,3,False), (21,105,2,True), (22,110,2,True), (23,115,2,False), (24,120,2,False)] Grounded Until: 120 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 100 Time : 814.343s (Solving: 777.09s 1st Model: 0.07s Unsat: 11.73s) CPU Time : 814.452s Choices : 15064033 (Domain: 14814057) Conflicts : 809315 (Analyzed: 809311) Restarts : 9572 (Average: 84.55 Last: 175) Model-Level : 251.0 Problems : 100 (Average Length: 94.25 Splits: 0) Lemmas : 809311 (Deleted: 763810) Binary : 15137 (Ratio: 1.87%) Ternary : 3265 (Ratio: 0.40%) Conflict : 809311 (Average Length: 543.1 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 809311 (Average: 16.74 Max: 1251 Sum: 13544713) Executed : 809170 (Average: 16.73 Max: 1251 Sum: 13537198 Ratio: 99.94%) Bounded : 141 (Average: 53.30 Max: 122 Sum: 7515 Ratio: 0.06%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 881056 (Eliminated: 0 Frozen: 272341) Constraints : 6468845 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1048MB Max. Length : 120 steps Models : 1 [endof: stats after solve call] Solving Time: 5.33s Memory: 951MB (+0MB) UNKNOWN Iteration Time: 5.40s Iteration 100 Queue: [(7,35,7,True), (8,40,7,True), (9,45,6,True), (10,50,6,False), (11,55,5,True), (12,60,5,False), (13,65,4,True), (14,70,4,False), (15,75,4,False), (16,80,4,False), (17,85,3,True), (18,90,3,False), (19,95,3,False), (20,100,3,False), (21,105,2,True), (22,110,2,True), (23,115,2,False), (24,120,2,False)] Grounded Until: 120 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 101 Time : 820.053s (Solving: 782.59s 1st Model: 0.07s Unsat: 11.73s) CPU Time : 820.164s Choices : 15122775 (Domain: 14872505) Conflicts : 817152 (Analyzed: 817148) Restarts : 9672 (Average: 84.49 Last: 175) Model-Level : 251.0 Problems : 101 (Average Length: 94.52 Splits: 0) Lemmas : 817148 (Deleted: 771503) Binary : 15204 (Ratio: 1.86%) Ternary : 3276 (Ratio: 0.40%) Conflict : 817148 (Average Length: 543.6 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 817148 (Average: 16.63 Max: 1251 Sum: 13589349) Executed : 817007 (Average: 16.62 Max: 1251 Sum: 13581834 Ratio: 99.94%) Bounded : 141 (Average: 53.30 Max: 122 Sum: 7515 Ratio: 0.06%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 881056 (Eliminated: 0 Frozen: 272341) Constraints : 6468845 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1048MB Max. Length : 120 steps Models : 1 [endof: stats after solve call] Solving Time: 5.63s Memory: 951MB (+0MB) UNKNOWN Iteration Time: 5.71s Iteration 101 Queue: [(8,40,7,True), (9,45,6,True), (10,50,6,False), (11,55,5,True), (12,60,5,False), (13,65,4,True), (14,70,4,False), (15,75,4,False), (16,80,4,False), (17,85,3,True), (18,90,3,False), (19,95,3,False), (20,100,3,False), (21,105,2,True), (22,110,2,True), (23,115,2,False), (24,120,2,False)] Grounded Until: 120 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 102 Time : 825.353s (Solving: 787.70s 1st Model: 0.07s Unsat: 11.73s) CPU Time : 825.464s Choices : 15190386 (Domain: 14939890) Conflicts : 825719 (Analyzed: 825715) Restarts : 9772 (Average: 84.50 Last: 175) Model-Level : 251.0 Problems : 102 (Average Length: 94.79 Splits: 0) Lemmas : 825715 (Deleted: 779081) Binary : 15222 (Ratio: 1.84%) Ternary : 3277 (Ratio: 0.40%) Conflict : 825715 (Average Length: 541.5 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 825715 (Average: 16.53 Max: 1251 Sum: 13646282) Executed : 825574 (Average: 16.52 Max: 1251 Sum: 13638767 Ratio: 99.94%) Bounded : 141 (Average: 53.30 Max: 122 Sum: 7515 Ratio: 0.06%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 881056 (Eliminated: 0 Frozen: 272341) Constraints : 6468845 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1048MB Max. Length : 120 steps Models : 1 [endof: stats after solve call] Solving Time: 5.23s Memory: 951MB (+0MB) UNKNOWN Iteration Time: 5.31s Iteration 102 Queue: [(9,45,6,True), (10,50,6,False), (11,55,5,True), (12,60,5,False), (13,65,4,True), (14,70,4,False), (15,75,4,False), (16,80,4,False), (17,85,3,True), (18,90,3,False), (19,95,3,False), (20,100,3,False), (21,105,2,True), (22,110,2,True), (23,115,2,False), (24,120,2,False)] Grounded Until: 120 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 103 Time : 832.837s (Solving: 795.00s 1st Model: 0.07s Unsat: 11.73s) CPU Time : 832.952s Choices : 15274880 (Domain: 15023207) Conflicts : 834297 (Analyzed: 834293) Restarts : 9872 (Average: 84.51 Last: 175) Model-Level : 251.0 Problems : 103 (Average Length: 95.06 Splits: 0) Lemmas : 834293 (Deleted: 787437) Binary : 15292 (Ratio: 1.83%) Ternary : 3293 (Ratio: 0.39%) Conflict : 834293 (Average Length: 540.5 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 834293 (Average: 16.44 Max: 1251 Sum: 13716372) Executed : 834152 (Average: 16.43 Max: 1251 Sum: 13708857 Ratio: 99.95%) Bounded : 141 (Average: 53.30 Max: 122 Sum: 7515 Ratio: 0.05%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 881056 (Eliminated: 0 Frozen: 272341) Constraints : 6468845 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1048MB Max. Length : 120 steps Models : 1 [endof: stats after solve call] Solving Time: 7.43s Memory: 951MB (+0MB) UNKNOWN Iteration Time: 7.49s Iteration 103 Queue: [(11,55,5,True), (12,60,5,False), (13,65,4,True), (14,70,4,False), (15,75,4,False), (16,80,4,False), (17,85,3,True), (18,90,3,False), (19,95,3,False), (20,100,3,False), (21,105,2,True), (22,110,2,True), (23,115,2,False), (24,120,2,False)] Grounded Until: 120 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 104 Time : 840.410s (Solving: 802.36s 1st Model: 0.07s Unsat: 11.73s) CPU Time : 840.528s Choices : 15372997 (Domain: 15121000) Conflicts : 843061 (Analyzed: 843057) Restarts : 9972 (Average: 84.54 Last: 175) Model-Level : 251.0 Problems : 104 (Average Length: 95.32 Splits: 0) Lemmas : 843057 (Deleted: 797996) Binary : 15355 (Ratio: 1.82%) Ternary : 3305 (Ratio: 0.39%) Conflict : 843057 (Average Length: 539.8 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 843057 (Average: 16.37 Max: 1251 Sum: 13798070) Executed : 842916 (Average: 16.36 Max: 1251 Sum: 13790555 Ratio: 99.95%) Bounded : 141 (Average: 53.30 Max: 122 Sum: 7515 Ratio: 0.05%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 881056 (Eliminated: 0 Frozen: 272341) Constraints : 6468845 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1048MB Max. Length : 120 steps Models : 1 [endof: stats after solve call] Solving Time: 7.49s Memory: 951MB (+0MB) UNKNOWN Iteration Time: 7.58s Iteration 104 Queue: [(13,65,4,True), (14,70,4,False), (15,75,4,False), (16,80,4,False), (17,85,3,True), (18,90,3,False), (19,95,3,False), (20,100,3,False), (21,105,2,True), (22,110,2,True), (23,115,2,False), (24,120,2,False)] Grounded Until: 120 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 105 Time : 848.750s (Solving: 810.52s 1st Model: 0.07s Unsat: 11.73s) CPU Time : 848.872s Choices : 15494748 (Domain: 15242114) Conflicts : 852032 (Analyzed: 852028) Restarts : 10072 (Average: 84.59 Last: 175) Model-Level : 251.0 Problems : 105 (Average Length: 95.57 Splits: 0) Lemmas : 852028 (Deleted: 806503) Binary : 15417 (Ratio: 1.81%) Ternary : 3320 (Ratio: 0.39%) Conflict : 852028 (Average Length: 540.3 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 852028 (Average: 16.31 Max: 1251 Sum: 13899546) Executed : 851887 (Average: 16.30 Max: 1251 Sum: 13892031 Ratio: 99.95%) Bounded : 141 (Average: 53.30 Max: 122 Sum: 7515 Ratio: 0.05%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 881056 (Eliminated: 0 Frozen: 272341) Constraints : 6468845 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1048MB Max. Length : 120 steps Models : 1 [endof: stats after solve call] Solving Time: 8.28s Memory: 951MB (+0MB) UNKNOWN Iteration Time: 8.35s Iteration 105 Queue: [(17,85,3,True), (18,90,3,False), (19,95,3,False), (20,100,3,False), (21,105,2,True), (22,110,2,True), (23,115,2,False), (24,120,2,False)] Grounded Until: 120 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 106 Time : 858.788s (Solving: 820.38s 1st Model: 0.07s Unsat: 11.73s) CPU Time : 858.916s Choices : 15654408 (Domain: 15401376) Conflicts : 861696 (Analyzed: 861692) Restarts : 10172 (Average: 84.71 Last: 175) Model-Level : 251.0 Problems : 106 (Average Length: 95.82 Splits: 0) Lemmas : 861692 (Deleted: 815289) Binary : 15459 (Ratio: 1.79%) Ternary : 3334 (Ratio: 0.39%) Conflict : 861692 (Average Length: 541.0 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 861692 (Average: 16.29 Max: 1251 Sum: 14037007) Executed : 861551 (Average: 16.28 Max: 1251 Sum: 14029492 Ratio: 99.95%) Bounded : 141 (Average: 53.30 Max: 122 Sum: 7515 Ratio: 0.05%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 881056 (Eliminated: 0 Frozen: 272341) Constraints : 6468845 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1048MB Max. Length : 120 steps Models : 1 [endof: stats after solve call] Solving Time: 9.98s Memory: 951MB (+0MB) UNKNOWN Iteration Time: 10.04s Iteration 106 Queue: [(21,105,2,True), (22,110,2,True), (23,115,2,False), (24,120,2,False)] Grounded Until: 120 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 107 Time : 865.664s (Solving: 827.09s 1st Model: 0.07s Unsat: 11.73s) CPU Time : 865.796s Choices : 15772191 (Domain: 15518880) Conflicts : 870232 (Analyzed: 870228) Restarts : 10272 (Average: 84.72 Last: 175) Model-Level : 251.0 Problems : 107 (Average Length: 96.07 Splits: 0) Lemmas : 870228 (Deleted: 822590) Binary : 15473 (Ratio: 1.78%) Ternary : 3353 (Ratio: 0.39%) Conflict : 870228 (Average Length: 539.6 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 870228 (Average: 16.24 Max: 1251 Sum: 14135261) Executed : 870087 (Average: 16.23 Max: 1251 Sum: 14127746 Ratio: 99.95%) Bounded : 141 (Average: 53.30 Max: 122 Sum: 7515 Ratio: 0.05%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 881056 (Eliminated: 0 Frozen: 272341) Constraints : 6468845 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1048MB Max. Length : 120 steps Models : 1 [endof: stats after solve call] Solving Time: 6.82s Memory: 951MB (+0MB) UNKNOWN Iteration Time: 6.88s Iteration 107 Queue: [(22,110,2,True), (23,115,2,False), (24,120,2,False)] Grounded Until: 120 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 108 Time : 874.352s (Solving: 835.60s 1st Model: 0.07s Unsat: 11.73s) CPU Time : 874.484s Choices : 15910592 (Domain: 15657216) Conflicts : 878853 (Analyzed: 878849) Restarts : 10372 (Average: 84.73 Last: 175) Model-Level : 251.0 Problems : 108 (Average Length: 96.31 Splits: 0) Lemmas : 878849 (Deleted: 833073) Binary : 15500 (Ratio: 1.76%) Ternary : 3364 (Ratio: 0.38%) Conflict : 878849 (Average Length: 540.5 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 878849 (Average: 16.21 Max: 1251 Sum: 14248228) Executed : 878708 (Average: 16.20 Max: 1251 Sum: 14240713 Ratio: 99.95%) Bounded : 141 (Average: 53.30 Max: 122 Sum: 7515 Ratio: 0.05%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 881056 (Eliminated: 0 Frozen: 272341) Constraints : 6468845 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1048MB Max. Length : 120 steps Models : 1 [endof: stats after solve call] Solving Time: 8.63s Memory: 951MB (+0MB) UNKNOWN Iteration Time: 8.70s Iteration 108 Queue: [(5,25,9,True), (6,30,9,True), (7,35,8,True), (8,40,8,False), (9,45,7,True), (10,50,6,True), (11,55,6,False), (12,60,5,True), (13,65,5,False), (14,70,4,True), (15,75,4,False), (16,80,4,False), (17,85,4,False), (18,90,3,True), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,2,True), (24,120,2,False)] Grounded Until: 120 Blocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 109 Time : 881.451s (Solving: 842.51s 1st Model: 0.07s Unsat: 11.73s) CPU Time : 881.584s Choices : 15955076 (Domain: 15701700) Conflicts : 886877 (Analyzed: 886873) Restarts : 10472 (Average: 84.69 Last: 175) Model-Level : 251.0 Problems : 109 (Average Length: 96.54 Splits: 0) Lemmas : 886873 (Deleted: 839363) Binary : 15547 (Ratio: 1.75%) Ternary : 3369 (Ratio: 0.38%) Conflict : 886873 (Average Length: 541.3 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 886873 (Average: 16.10 Max: 1251 Sum: 14282515) Executed : 886732 (Average: 16.10 Max: 1251 Sum: 14275000 Ratio: 99.95%) Bounded : 141 (Average: 53.30 Max: 122 Sum: 7515 Ratio: 0.05%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 881056 (Eliminated: 0 Frozen: 272341) Constraints : 6468845 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1048MB Max. Length : 120 steps Models : 1 [endof: stats after solve call] Solving Time: 7.03s Memory: 951MB (+0MB) UNKNOWN Iteration Time: 7.11s Iteration 109 Queue: [(6,30,9,True), (7,35,8,True), (8,40,8,False), (9,45,7,True), (10,50,6,True), (11,55,6,False), (12,60,5,True), (13,65,5,False), (14,70,4,True), (15,75,4,False), (16,80,4,False), (17,85,4,False), (18,90,3,True), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,2,True), (24,120,2,False)] Grounded Until: 120 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 110 Time : 887.574s (Solving: 848.41s 1st Model: 0.07s Unsat: 11.73s) CPU Time : 887.712s Choices : 16017591 (Domain: 15764215) Conflicts : 895202 (Analyzed: 895198) Restarts : 10572 (Average: 84.68 Last: 175) Model-Level : 251.0 Problems : 110 (Average Length: 96.77 Splits: 0) Lemmas : 895198 (Deleted: 847259) Binary : 15578 (Ratio: 1.74%) Ternary : 3386 (Ratio: 0.38%) Conflict : 895198 (Average Length: 541.0 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 895198 (Average: 16.01 Max: 1251 Sum: 14331417) Executed : 895057 (Average: 16.00 Max: 1251 Sum: 14323902 Ratio: 99.95%) Bounded : 141 (Average: 53.30 Max: 122 Sum: 7515 Ratio: 0.05%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 881056 (Eliminated: 0 Frozen: 272341) Constraints : 6468845 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1048MB Max. Length : 120 steps Models : 1 [endof: stats after solve call] Solving Time: 6.04s Memory: 951MB (+0MB) UNKNOWN Iteration Time: 6.13s Iteration 110 Queue: [(7,35,8,True), (8,40,8,False), (9,45,7,True), (10,50,6,True), (11,55,6,False), (12,60,5,True), (13,65,5,False), (14,70,4,True), (15,75,4,False), (16,80,4,False), (17,85,4,False), (18,90,3,True), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,2,True), (24,120,2,False)] Grounded Until: 120 Unblocking actions... Solving... *** Info : (planner): INTERRUPTED by signal! UNKNOWN INTERRUPTED : 1 Models : 0+ Calls : 111 Time : 893.084s (Solving: 853.74s 1st Model: 0.07s Unsat: 11.73s) CPU Time : 893.204s Choices : 16072168 (Domain: 15818777) Conflicts : 902178 (Analyzed: 902174) Restarts : 10652 (Average: 84.70 Last: 175) Model-Level : 251.0 Problems : 111 (Average Length: 97.00 Splits: 0) Lemmas : 902174 (Deleted: 855390) Binary : 15640 (Ratio: 1.73%) Ternary : 3406 (Ratio: 0.38%) Conflict : 902174 (Average Length: 541.5 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 902174 (Average: 15.93 Max: 1251 Sum: 14373564) Executed : 902033 (Average: 15.92 Max: 1251 Sum: 14366049 Ratio: 99.95%) Bounded : 141 (Average: 53.30 Max: 122 Sum: 7515 Ratio: 0.05%) Rules : 150286 (Original: 135821) Atoms : 72368 Bodies : 65513 (Original: 51047) Count : 841 (Original: 2348) Equivalences : 15742 (Atom=Atom: 82 Body=Body: 0 Other: 15660) Tight : Yes Variables : 881056 (Eliminated: 0 Frozen: 272341) Constraints : 6468845 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1048MB Max. Length : 120 steps Models : 1