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-17.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-17.pddl Parsing... Parsing: [0.040s CPU, 0.036s wall-clock] Normalizing task... [0.000s CPU, 0.003s wall-clock] Instantiating... Generating Datalog program... [0.010s CPU, 0.010s wall-clock] Normalizing Datalog program... Normalizing Datalog program: [0.040s CPU, 0.045s wall-clock] Preparing model... [0.030s CPU, 0.026s wall-clock] Generated 115 rules. Computing model... [0.530s CPU, 0.536s wall-clock] 3296 relevant atoms 3425 auxiliary atoms 6721 final queue length 11595 total queue pushes Completing instantiation... [1.030s CPU, 1.028s wall-clock] Instantiating: [1.650s CPU, 1.652s wall-clock] Computing fact groups... Finding invariants... 24 initial candidates Finding invariants: [0.140s CPU, 0.142s wall-clock] Checking invariant weight... [0.000s CPU, 0.001s wall-clock] Instantiating groups... [0.010s CPU, 0.010s wall-clock] Collecting mutex groups... [0.000s CPU, 0.001s wall-clock] Choosing groups... 350 uncovered facts Choosing groups: [0.000s CPU, 0.002s wall-clock] Building translation key... [0.010s CPU, 0.013s wall-clock] Computing fact groups: [0.190s CPU, 0.195s wall-clock] Building STRIPS to SAS dictionary... [0.010s CPU, 0.006s wall-clock] Building dictionary for full mutex groups... [0.000s CPU, 0.003s wall-clock] Building mutex information... Building mutex information: [0.010s CPU, 0.004s wall-clock] Translating task... Processing axioms... Simplifying axioms... [0.000s CPU, 0.000s wall-clock] Processing axioms: [0.050s CPU, 0.057s wall-clock] Translating task: [1.060s CPU, 1.067s wall-clock] 3920 effect conditions simplified 0 implied preconditions added Detecting unreachable propositions... 0 operators removed 0 axioms removed 3 propositions removed Detecting unreachable propositions: [0.590s CPU, 0.587s wall-clock] Reordering and filtering variables... 353 of 353 variables necessary. 16 of 19 mutex groups necessary. 2344 of 2344 operators necessary. 0 of 0 axiom rules necessary. Reordering and filtering variables: [0.380s CPU, 0.378s wall-clock] Translator variables: 353 Translator derived variables: 0 Translator facts: 737 Translator goal facts: 14 Translator mutex groups: 16 Translator total mutex groups size: 48 Translator operators: 2344 Translator axioms: 0 Translator task size: 22454 Translator peak memory: 49100 KB Writing output... [0.380s CPU, 0.411s wall-clock] Done! [4.350s CPU, 4.383s wall-clock] planner.py version 0.0.1 Time: 0.91s Memory: 111MB 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 : 1.068s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s) CPU Time : 0.908s 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 : 64767 Atoms : 64767 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 : 247MB Max. Length : 0 steps Models : 0 [endof: stats after solve call] Solving Time: 0.01s Memory: 183MB (+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: 183MB Grounding... [('step', [1]), ('step', [2]), ('step', [3]), ('step', [4]), ('step', [5]), ('check', [5])] Grounding Time: 0.27s Memory: 183MB (+0MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0 Calls : 2 Time : 1.501s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s) CPU Time : 1.340s Choices : 171 (Domain: 108) Conflicts : 40 (Analyzed: 39) Restarts : 0 Problems : 2 (Average Length: 4.50 Splits: 0) Lemmas : 39 (Deleted: 0) Binary : 11 (Ratio: 28.21%) Ternary : 4 (Ratio: 10.26%) Conflict : 39 (Average Length: 4.8 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 39 (Average: 4.41 Max: 28 Sum: 172) Executed : 38 (Average: 4.38 Max: 28 Sum: 171 Ratio: 99.42%) Bounded : 1 (Average: 1.00 Max: 1 Sum: 1 Ratio: 0.58%) Rules : 64767 Atoms : 64767 Bodies : 1 (Original: 0) Tight : Yes Variables : 17354 (Eliminated: 0 Frozen: 170) Constraints : 57355 (Binary: 95.3% Ternary: 3.3% Other: 1.4%) Memory Peak : 247MB Max. Length : 0 steps Models : 0 [endof: stats after solve call] Solving Time: 0.02s Memory: 187MB (+4MB) UNSAT Iteration Time: 0.44s 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: 191.0MB Grounding... [('step', [6]), ('step', [7]), ('step', [8]), ('step', [9]), ('step', [10]), ('check', [10])] Grounding Time: 0.34s Memory: 195MB (+8MB) Unblocking actions... Solving... [start: stats after solve call] Models : 1+ Calls : 3 Time : 2.018s (Solving: 0.02s 1st Model: 0.01s Unsat: 0.00s) CPU Time : 1.856s Choices : 1028 (Domain: 926) Conflicts : 96 (Analyzed: 95) Restarts : 0 Model-Level : 254.0 Problems : 3 (Average Length: 7.00 Splits: 0) Lemmas : 95 (Deleted: 0) Binary : 38 (Ratio: 40.00%) Ternary : 6 (Ratio: 6.32%) Conflict : 95 (Average Length: 59.9 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 95 (Average: 8.28 Max: 144 Sum: 787) Executed : 94 (Average: 8.27 Max: 144 Sum: 786 Ratio: 99.87%) Bounded : 1 (Average: 1.00 Max: 1 Sum: 1 Ratio: 0.13%) Rules : 64767 Atoms : 64767 Bodies : 1 (Original: 0) Tight : Yes Variables : 38040 (Eliminated: 0 Frozen: 340) Constraints : 226475 (Binary: 95.6% Ternary: 3.2% Other: 1.2%) Memory Peak : 247MB Max. Length : 5 steps Models : 1 [endof: stats after solve call] Solving Time: 0.04s Memory: 205MB (+10MB) SAT Testing... NOT SERIALIZABLE Testing Time: 1.16s Memory: 241MB (+36MB) Solving... [start: stats after solve call] Models : 0 Calls : 4 Time : 3.305s (Solving: 0.95s 1st Model: 0.01s Unsat: 0.93s) CPU Time : 3.140s Choices : 30026 (Domain: 23080) Conflicts : 3147 (Analyzed: 3145) Restarts : 33 (Average: 95.30 Last: 56) Model-Level : 254.0 Problems : 4 (Average Length: 8.25 Splits: 0) Lemmas : 3145 (Deleted: 858) Binary : 260 (Ratio: 8.27%) Ternary : 82 (Ratio: 2.61%) Conflict : 3145 (Average Length: 103.7 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 3145 (Average: 9.32 Max: 196 Sum: 29297) Executed : 3134 (Average: 9.28 Max: 196 Sum: 29198 Ratio: 99.66%) Bounded : 11 (Average: 9.00 Max: 12 Sum: 99 Ratio: 0.34%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 60107 (Eliminated: 0 Frozen: 16894) Constraints : 371085 (Binary: 91.4% Ternary: 7.0% Other: 1.6%) Memory Peak : 247MB Max. Length : 5 steps Models : 1 [endof: stats after solve call] Solving Time: 1.02s Memory: 240MB (+-1MB) UNSAT Iteration Time: 2.70s Iteration 4 Queue: [(3,15,0,True), (4,20,0,True), (5,25,0,True), (6,30,0,True)] Grounded Until: 10 Expected Memory: 258.0MB Grounding... [('step', [11]), ('step', [12]), ('step', [13]), ('step', [14]), ('step', [15]), ('check', [15])] Grounding Time: 0.52s Memory: 241MB (+1MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 5 Time : 8.640s (Solving: 5.52s 1st Model: 0.01s Unsat: 0.93s) CPU Time : 8.480s Choices : 120633 (Domain: 94496) Conflicts : 11866 (Analyzed: 11864) Restarts : 133 (Average: 89.20 Last: 113) Model-Level : 254.0 Problems : 5 (Average Length: 10.00 Splits: 0) Lemmas : 11864 (Deleted: 8150) Binary : 939 (Ratio: 7.91%) Ternary : 300 (Ratio: 2.53%) Conflict : 11864 (Average Length: 192.7 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 11864 (Average: 9.80 Max: 199 Sum: 116208) Executed : 11841 (Average: 9.77 Max: 199 Sum: 115915 Ratio: 99.75%) Bounded : 23 (Average: 12.74 Max: 17 Sum: 293 Ratio: 0.25%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 100183 (Eliminated: 0 Frozen: 29344) Constraints : 661845 (Binary: 91.3% Ternary: 6.9% Other: 1.7%) Memory Peak : 266MB Max. Length : 10 steps Models : 1 [endof: stats after solve call] Solving Time: 4.60s Memory: 266MB (+25MB) UNKNOWN Iteration Time: 5.35s Iteration 5 Queue: [(4,20,0,True), (5,25,0,True), (6,30,0,True)] Grounded Until: 15 Expected Memory: 292.0MB Grounding... [('step', [16]), ('step', [17]), ('step', [18]), ('step', [19]), ('step', [20]), ('check', [20])] Grounding Time: 0.62s Memory: 279MB (+13MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 6 Time : 15.324s (Solving: 11.29s 1st Model: 0.01s Unsat: 0.93s) CPU Time : 15.168s Choices : 228016 (Domain: 186850) Conflicts : 20689 (Analyzed: 20687) Restarts : 233 (Average: 88.79 Last: 113) Model-Level : 254.0 Problems : 6 (Average Length: 12.00 Splits: 0) Lemmas : 20687 (Deleted: 15856) Binary : 1617 (Ratio: 7.82%) Ternary : 415 (Ratio: 2.01%) Conflict : 20687 (Average Length: 495.6 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 20687 (Average: 10.52 Max: 199 Sum: 217670) Executed : 20664 (Average: 10.51 Max: 199 Sum: 217377 Ratio: 99.87%) Bounded : 23 (Average: 12.74 Max: 17 Sum: 293 Ratio: 0.13%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 140259 (Eliminated: 0 Frozen: 41794) Constraints : 958119 (Binary: 91.3% Ternary: 6.9% Other: 1.7%) Memory Peak : 297MB Max. Length : 15 steps Models : 1 [endof: stats after solve call] Solving Time: 5.83s Memory: 293MB (+14MB) UNKNOWN Iteration Time: 6.70s Iteration 6 Queue: [(5,25,0,True), (6,30,0,True)] Grounded Until: 20 Expected Memory: 320.0MB Grounding... [('step', [21]), ('step', [22]), ('step', [23]), ('step', [24]), ('step', [25]), ('check', [25])] Grounding Time: 0.59s Memory: 307MB (+14MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 7 Time : 23.100s (Solving: 18.16s 1st Model: 0.01s Unsat: 0.93s) CPU Time : 22.948s Choices : 340659 (Domain: 289099) Conflicts : 29741 (Analyzed: 29739) Restarts : 333 (Average: 89.31 Last: 113) Model-Level : 254.0 Problems : 7 (Average Length: 14.14 Splits: 0) Lemmas : 29739 (Deleted: 24092) Binary : 1976 (Ratio: 6.64%) Ternary : 449 (Ratio: 1.51%) Conflict : 29739 (Average Length: 822.1 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 29739 (Average: 10.82 Max: 248 Sum: 321843) Executed : 29716 (Average: 10.81 Max: 248 Sum: 321550 Ratio: 99.91%) Bounded : 23 (Average: 12.74 Max: 17 Sum: 293 Ratio: 0.09%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 180335 (Eliminated: 0 Frozen: 54244) Constraints : 1260099 (Binary: 91.3% Ternary: 7.0% Other: 1.8%) Memory Peak : 334MB Max. Length : 20 steps Models : 1 [endof: stats after solve call] Solving Time: 6.92s Memory: 321MB (+14MB) UNKNOWN Iteration Time: 7.79s Iteration 7 Queue: [(6,30,0,True)] Grounded Until: 25 Expected Memory: 349.0MB Grounding... [('step', [26]), ('step', [27]), ('step', [28]), ('step', [29]), ('step', [30]), ('check', [30])] Grounding Time: 0.56s Memory: 333MB (+12MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 8 Time : 30.707s (Solving: 24.87s 1st Model: 0.01s Unsat: 0.93s) CPU Time : 30.556s Choices : 460469 (Domain: 402838) Conflicts : 37831 (Analyzed: 37829) Restarts : 433 (Average: 87.36 Last: 113) Model-Level : 254.0 Problems : 8 (Average Length: 16.38 Splits: 0) Lemmas : 37829 (Deleted: 30595) Binary : 2189 (Ratio: 5.79%) Ternary : 466 (Ratio: 1.23%) Conflict : 37829 (Average Length: 1056.9 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 37829 (Average: 11.38 Max: 262 Sum: 430377) Executed : 37806 (Average: 11.37 Max: 262 Sum: 430084 Ratio: 99.93%) Bounded : 23 (Average: 12.74 Max: 17 Sum: 293 Ratio: 0.07%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 220411 (Eliminated: 0 Frozen: 66694) Constraints : 1562079 (Binary: 91.3% Ternary: 7.0% Other: 1.8%) Memory Peak : 367MB Max. Length : 25 steps Models : 1 [endof: stats after solve call] Solving Time: 6.77s Memory: 367MB (+34MB) UNKNOWN Iteration Time: 7.62s 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 : 36.604s (Solving: 30.70s 1st Model: 0.01s Unsat: 0.93s) CPU Time : 36.456s Choices : 545520 (Domain: 482044) Conflicts : 46602 (Analyzed: 46600) Restarts : 533 (Average: 87.43 Last: 113) Model-Level : 254.0 Problems : 9 (Average Length: 18.11 Splits: 0) Lemmas : 46600 (Deleted: 40009) Binary : 2669 (Ratio: 5.73%) Ternary : 563 (Ratio: 1.21%) Conflict : 46600 (Average Length: 916.7 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 46600 (Average: 10.93 Max: 269 Sum: 509528) Executed : 46563 (Average: 10.92 Max: 269 Sum: 508787 Ratio: 99.85%) Bounded : 37 (Average: 20.03 Max: 32 Sum: 741 Ratio: 0.15%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 220411 (Eliminated: 0 Frozen: 66694) Constraints : 1562079 (Binary: 91.3% Ternary: 7.0% Other: 1.8%) Memory Peak : 367MB Max. Length : 30 steps Models : 1 [endof: stats after solve call] Solving Time: 5.88s Memory: 367MB (+0MB) UNKNOWN Iteration Time: 5.90s 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 : 42.786s (Solving: 36.83s 1st Model: 0.01s Unsat: 0.93s) CPU Time : 42.640s Choices : 685916 (Domain: 614218) Conflicts : 55643 (Analyzed: 55641) Restarts : 633 (Average: 87.90 Last: 113) Model-Level : 254.0 Problems : 10 (Average Length: 19.50 Splits: 0) Lemmas : 55641 (Deleted: 47014) Binary : 3310 (Ratio: 5.95%) Ternary : 679 (Ratio: 1.22%) Conflict : 55641 (Average Length: 796.5 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 55641 (Average: 11.59 Max: 282 Sum: 644675) Executed : 55592 (Average: 11.57 Max: 282 Sum: 643550 Ratio: 99.83%) Bounded : 49 (Average: 22.96 Max: 32 Sum: 1125 Ratio: 0.17%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 220411 (Eliminated: 0 Frozen: 66694) Constraints : 1539434 (Binary: 91.3% Ternary: 6.9% Other: 1.8%) Memory Peak : 367MB Max. Length : 30 steps Models : 1 [endof: stats after solve call] Solving Time: 6.17s Memory: 367MB (+0MB) UNKNOWN Iteration Time: 6.19s 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 : 48.750s (Solving: 42.75s 1st Model: 0.01s Unsat: 0.93s) CPU Time : 48.604s Choices : 829159 (Domain: 750755) Conflicts : 64375 (Analyzed: 64373) Restarts : 733 (Average: 87.82 Last: 116) Model-Level : 254.0 Problems : 11 (Average Length: 20.64 Splits: 0) Lemmas : 64373 (Deleted: 54670) Binary : 3548 (Ratio: 5.51%) Ternary : 777 (Ratio: 1.21%) Conflict : 64373 (Average Length: 715.2 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 64373 (Average: 12.15 Max: 307 Sum: 782285) Executed : 64313 (Average: 12.13 Max: 307 Sum: 780838 Ratio: 99.82%) Bounded : 60 (Average: 24.12 Max: 32 Sum: 1447 Ratio: 0.18%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 220411 (Eliminated: 0 Frozen: 66694) Constraints : 1517106 (Binary: 91.3% Ternary: 6.9% Other: 1.8%) Memory Peak : 367MB Max. Length : 30 steps Models : 1 [endof: stats after solve call] Solving Time: 5.95s Memory: 367MB (+0MB) UNKNOWN Iteration Time: 5.97s 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 : 54.222s (Solving: 48.16s 1st Model: 0.01s Unsat: 0.93s) CPU Time : 54.076s Choices : 990974 (Domain: 903422) Conflicts : 73229 (Analyzed: 73227) Restarts : 833 (Average: 87.91 Last: 150) Model-Level : 254.0 Problems : 12 (Average Length: 21.58 Splits: 0) Lemmas : 73227 (Deleted: 62428) Binary : 3764 (Ratio: 5.14%) Ternary : 847 (Ratio: 1.16%) Conflict : 73227 (Average Length: 648.5 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 73227 (Average: 12.77 Max: 404 Sum: 934765) Executed : 73160 (Average: 12.74 Max: 404 Sum: 933099 Ratio: 99.82%) Bounded : 67 (Average: 24.87 Max: 32 Sum: 1666 Ratio: 0.18%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 220411 (Eliminated: 0 Frozen: 66694) Constraints : 1506186 (Binary: 91.3% Ternary: 6.9% Other: 1.8%) Memory Peak : 367MB Max. Length : 30 steps Models : 1 [endof: stats after solve call] Solving Time: 5.45s Memory: 367MB (+0MB) UNKNOWN Iteration Time: 5.48s 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: 413.0MB Grounding... [('step', [31]), ('step', [32]), ('step', [33]), ('step', [34]), ('step', [35]), ('check', [35])] Grounding Time: 0.59s Memory: 367MB (+0MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 13 Time : 61.201s (Solving: 54.18s 1st Model: 0.01s Unsat: 0.93s) CPU Time : 61.060s Choices : 1215033 (Domain: 1122075) Conflicts : 82083 (Analyzed: 82081) Restarts : 933 (Average: 87.98 Last: 150) Model-Level : 254.0 Problems : 13 (Average Length: 22.77 Splits: 0) Lemmas : 82081 (Deleted: 72810) Binary : 4020 (Ratio: 4.90%) Ternary : 860 (Ratio: 1.05%) Conflict : 82081 (Average Length: 661.1 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 82081 (Average: 13.97 Max: 404 Sum: 1146403) Executed : 82014 (Average: 13.95 Max: 404 Sum: 1144737 Ratio: 99.85%) Bounded : 67 (Average: 24.87 Max: 32 Sum: 1666 Ratio: 0.15%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 260487 (Eliminated: 0 Frozen: 79144) Constraints : 1804964 (Binary: 91.3% Ternary: 6.9% Other: 1.8%) Memory Peak : 403MB Max. Length : 30 steps Models : 1 [endof: stats after solve call] Solving Time: 6.09s Memory: 380MB (+13MB) UNKNOWN Iteration Time: 6.99s 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: 426.0MB Grounding... [('step', [36]), ('step', [37]), ('step', [38]), ('step', [39]), ('step', [40]), ('check', [40])] Grounding Time: 0.57s Memory: 392MB (+12MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 14 Time : 68.153s (Solving: 60.19s 1st Model: 0.01s Unsat: 0.93s) CPU Time : 68.016s Choices : 1422851 (Domain: 1322434) Conflicts : 90673 (Analyzed: 90671) Restarts : 1033 (Average: 87.77 Last: 150) Model-Level : 254.0 Problems : 14 (Average Length: 24.14 Splits: 0) Lemmas : 90671 (Deleted: 79068) Binary : 4254 (Ratio: 4.69%) Ternary : 864 (Ratio: 0.95%) Conflict : 90671 (Average Length: 677.5 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 90671 (Average: 14.74 Max: 440 Sum: 1336710) Executed : 90604 (Average: 14.72 Max: 440 Sum: 1335044 Ratio: 99.88%) Bounded : 67 (Average: 24.87 Max: 32 Sum: 1666 Ratio: 0.12%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 300563 (Eliminated: 0 Frozen: 91594) Constraints : 2106944 (Binary: 91.3% Ternary: 6.9% Other: 1.8%) Memory Peak : 435MB Max. Length : 35 steps Models : 1 [endof: stats after solve call] Solving Time: 6.08s Memory: 406MB (+14MB) UNKNOWN Iteration Time: 6.97s 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: 452.0MB Grounding... [('step', [41]), ('step', [42]), ('step', [43]), ('step', [44]), ('step', [45]), ('check', [45])] Grounding Time: 0.75s Memory: 430MB (+24MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 15 Time : 75.878s (Solving: 66.74s 1st Model: 0.01s Unsat: 0.93s) CPU Time : 75.744s Choices : 1592918 (Domain: 1489489) Conflicts : 99212 (Analyzed: 99210) Restarts : 1133 (Average: 87.56 Last: 150) Model-Level : 254.0 Problems : 15 (Average Length: 25.67 Splits: 0) Lemmas : 99210 (Deleted: 87296) Binary : 4358 (Ratio: 4.39%) Ternary : 869 (Ratio: 0.88%) Conflict : 99210 (Average Length: 724.6 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 99210 (Average: 14.98 Max: 440 Sum: 1486626) Executed : 99143 (Average: 14.97 Max: 440 Sum: 1484960 Ratio: 99.89%) Bounded : 67 (Average: 24.87 Max: 32 Sum: 1666 Ratio: 0.11%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 340639 (Eliminated: 0 Frozen: 104044) Constraints : 2408924 (Binary: 91.3% Ternary: 7.0% Other: 1.8%) Memory Peak : 480MB Max. Length : 40 steps Models : 1 [endof: stats after solve call] Solving Time: 6.64s Memory: 478MB (+48MB) UNKNOWN Iteration Time: 7.74s 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: 550.0MB Grounding... [('step', [46]), ('step', [47]), ('step', [48]), ('step', [49]), ('step', [50]), ('check', [50])] Grounding Time: 0.56s Memory: 478MB (+0MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 16 Time : 83.761s (Solving: 73.63s 1st Model: 0.01s Unsat: 0.93s) CPU Time : 83.632s Choices : 1779320 (Domain: 1670641) Conflicts : 107288 (Analyzed: 107286) Restarts : 1233 (Average: 87.01 Last: 150) Model-Level : 254.0 Problems : 16 (Average Length: 27.31 Splits: 0) Lemmas : 107286 (Deleted: 95633) Binary : 4449 (Ratio: 4.15%) Ternary : 876 (Ratio: 0.82%) Conflict : 107286 (Average Length: 756.4 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 107286 (Average: 15.37 Max: 482 Sum: 1649238) Executed : 107219 (Average: 15.36 Max: 482 Sum: 1647572 Ratio: 99.90%) Bounded : 67 (Average: 24.87 Max: 32 Sum: 1666 Ratio: 0.10%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 380715 (Eliminated: 0 Frozen: 116494) Constraints : 2710904 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 525MB Max. Length : 45 steps Models : 1 [endof: stats after solve call] Solving Time: 6.97s Memory: 488MB (+10MB) UNKNOWN Iteration Time: 7.90s 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: 560.0MB Grounding... [('step', [51]), ('step', [52]), ('step', [53]), ('step', [54]), ('step', [55]), ('check', [55])] Grounding Time: 0.55s Memory: 492MB (+4MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 17 Time : 91.812s (Solving: 80.69s 1st Model: 0.01s Unsat: 0.93s) CPU Time : 91.684s Choices : 2037604 (Domain: 1924173) Conflicts : 115480 (Analyzed: 115478) Restarts : 1333 (Average: 86.63 Last: 150) Model-Level : 254.0 Problems : 17 (Average Length: 29.06 Splits: 0) Lemmas : 115478 (Deleted: 103546) Binary : 4612 (Ratio: 3.99%) Ternary : 877 (Ratio: 0.76%) Conflict : 115478 (Average Length: 784.5 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 115478 (Average: 16.32 Max: 537 Sum: 1884467) Executed : 115411 (Average: 16.30 Max: 537 Sum: 1882801 Ratio: 99.91%) Bounded : 67 (Average: 24.87 Max: 32 Sum: 1666 Ratio: 0.09%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 420791 (Eliminated: 0 Frozen: 128944) Constraints : 3012884 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 551MB Max. Length : 50 steps Models : 1 [endof: stats after solve call] Solving Time: 7.15s Memory: 512MB (+20MB) UNKNOWN Iteration Time: 8.06s 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: 584.0MB Grounding... [('step', [56]), ('step', [57]), ('step', [58]), ('step', [59]), ('step', [60]), ('check', [60])] Grounding Time: 0.56s Memory: 517MB (+5MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 18 Time : 100.293s (Solving: 88.13s 1st Model: 0.01s Unsat: 0.93s) CPU Time : 100.168s Choices : 2275221 (Domain: 2158172) Conflicts : 123546 (Analyzed: 123544) Restarts : 1433 (Average: 86.21 Last: 150) Model-Level : 254.0 Problems : 18 (Average Length: 30.89 Splits: 0) Lemmas : 123544 (Deleted: 111469) Binary : 4654 (Ratio: 3.77%) Ternary : 878 (Ratio: 0.71%) Conflict : 123544 (Average Length: 800.3 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 123544 (Average: 16.97 Max: 606 Sum: 2096708) Executed : 123477 (Average: 16.96 Max: 606 Sum: 2095042 Ratio: 99.92%) Bounded : 67 (Average: 24.87 Max: 32 Sum: 1666 Ratio: 0.08%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 460867 (Eliminated: 0 Frozen: 141394) Constraints : 3314864 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 589MB Max. Length : 55 steps Models : 1 [endof: stats after solve call] Solving Time: 7.54s Memory: 589MB (+72MB) UNKNOWN Iteration Time: 8.50s Iteration 18 Queue: [(13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True)] Grounded Until: 60 Expected Memory: 666.0MB Grounding... [('step', [61]), ('step', [62]), ('step', [63]), ('step', [64]), ('step', [65]), ('check', [65])] Grounding Time: 0.56s Memory: 589MB (+0MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 19 Time : 108.491s (Solving: 95.28s 1st Model: 0.01s Unsat: 0.93s) CPU Time : 108.368s Choices : 2547612 (Domain: 2426157) Conflicts : 131557 (Analyzed: 131555) Restarts : 1533 (Average: 85.82 Last: 150) Model-Level : 254.0 Problems : 19 (Average Length: 32.79 Splits: 0) Lemmas : 131555 (Deleted: 119386) Binary : 4699 (Ratio: 3.57%) Ternary : 879 (Ratio: 0.67%) Conflict : 131555 (Average Length: 813.5 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 131555 (Average: 17.80 Max: 638 Sum: 2341876) Executed : 131488 (Average: 17.79 Max: 638 Sum: 2340210 Ratio: 99.93%) Bounded : 67 (Average: 24.87 Max: 32 Sum: 1666 Ratio: 0.07%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 500943 (Eliminated: 0 Frozen: 153844) Constraints : 3616844 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 650MB Max. Length : 60 steps Models : 1 [endof: stats after solve call] Solving Time: 7.26s Memory: 594MB (+5MB) UNKNOWN Iteration Time: 8.21s Iteration 19 Queue: [(14,70,0,True), (15,75,0,True), (16,80,0,True)] Grounded Until: 65 Expected Memory: 671.0MB Grounding... [('step', [66]), ('step', [67]), ('step', [68]), ('step', [69]), ('step', [70]), ('check', [70])] Grounding Time: 0.56s Memory: 594MB (+0MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 20 Time : 117.209s (Solving: 102.92s 1st Model: 0.01s Unsat: 0.93s) CPU Time : 117.092s Choices : 2844978 (Domain: 2719694) Conflicts : 139082 (Analyzed: 139080) Restarts : 1633 (Average: 85.17 Last: 150) Model-Level : 254.0 Problems : 20 (Average Length: 34.75 Splits: 0) Lemmas : 139080 (Deleted: 127229) Binary : 4733 (Ratio: 3.40%) Ternary : 880 (Ratio: 0.63%) Conflict : 139080 (Average Length: 829.1 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 139080 (Average: 18.78 Max: 708 Sum: 2612039) Executed : 139013 (Average: 18.77 Max: 708 Sum: 2610373 Ratio: 99.94%) Bounded : 67 (Average: 24.87 Max: 32 Sum: 1666 Ratio: 0.06%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 541019 (Eliminated: 0 Frozen: 166294) Constraints : 3918824 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 664MB Max. Length : 65 steps Models : 1 [endof: stats after solve call] Solving Time: 7.75s Memory: 610MB (+16MB) UNKNOWN Iteration Time: 8.73s Iteration 20 Queue: [(15,75,0,True), (16,80,0,True)] Grounded Until: 70 Expected Memory: 687.0MB Grounding... [('step', [71]), ('step', [72]), ('step', [73]), ('step', [74]), ('step', [75]), ('check', [75])] Grounding Time: 0.56s Memory: 615MB (+5MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 21 Time : 126.455s (Solving: 111.07s 1st Model: 0.01s Unsat: 0.93s) CPU Time : 126.344s Choices : 3156384 (Domain: 3026249) Conflicts : 146866 (Analyzed: 146864) Restarts : 1733 (Average: 84.75 Last: 150) Model-Level : 254.0 Problems : 21 (Average Length: 36.76 Splits: 0) Lemmas : 146864 (Deleted: 134594) Binary : 4775 (Ratio: 3.25%) Ternary : 881 (Ratio: 0.60%) Conflict : 146864 (Average Length: 841.9 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 146864 (Average: 19.71 Max: 746 Sum: 2894403) Executed : 146797 (Average: 19.70 Max: 746 Sum: 2892737 Ratio: 99.94%) Bounded : 67 (Average: 24.87 Max: 32 Sum: 1666 Ratio: 0.06%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 581095 (Eliminated: 0 Frozen: 178744) Constraints : 4220804 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 698MB Max. Length : 70 steps Models : 1 [endof: stats after solve call] Solving Time: 8.27s Memory: 642MB (+27MB) UNKNOWN Iteration Time: 9.26s Iteration 21 Queue: [(16,80,0,True)] Grounded Until: 75 Expected Memory: 719.0MB Grounding... [('step', [76]), ('step', [77]), ('step', [78]), ('step', [79]), ('step', [80]), ('check', [80])] Grounding Time: 0.58s Memory: 642MB (+0MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 22 Time : 136.032s (Solving: 119.51s 1st Model: 0.01s Unsat: 0.93s) CPU Time : 135.924s Choices : 3453062 (Domain: 3319382) Conflicts : 155063 (Analyzed: 155061) Restarts : 1833 (Average: 84.59 Last: 150) Model-Level : 254.0 Problems : 22 (Average Length: 38.82 Splits: 0) Lemmas : 155061 (Deleted: 142241) Binary : 4804 (Ratio: 3.10%) Ternary : 882 (Ratio: 0.57%) Conflict : 155061 (Average Length: 857.4 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 155061 (Average: 20.36 Max: 818 Sum: 3157695) Executed : 154994 (Average: 20.35 Max: 818 Sum: 3156029 Ratio: 99.95%) Bounded : 67 (Average: 24.87 Max: 32 Sum: 1666 Ratio: 0.05%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 621171 (Eliminated: 0 Frozen: 191194) Constraints : 4522784 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 726MB Max. Length : 75 steps Models : 1 [endof: stats after solve call] Solving Time: 8.56s Memory: 667MB (+25MB) UNKNOWN Iteration Time: 9.59s Iteration 22 Queue: [(3,15,2,True), (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)] Grounded Until: 80 Blocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 23 Time : 141.721s (Solving: 125.05s 1st Model: 0.01s Unsat: 0.93s) CPU Time : 141.616s Choices : 3517322 (Domain: 3372595) Conflicts : 163853 (Analyzed: 163851) Restarts : 1933 (Average: 84.77 Last: 150) Model-Level : 254.0 Problems : 23 (Average Length: 40.70 Splits: 0) Lemmas : 163851 (Deleted: 149929) Binary : 5047 (Ratio: 3.08%) Ternary : 960 (Ratio: 0.59%) Conflict : 163851 (Average Length: 824.2 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 163851 (Average: 19.64 Max: 818 Sum: 3217490) Executed : 163779 (Average: 19.63 Max: 818 Sum: 3215576 Ratio: 99.94%) Bounded : 72 (Average: 26.58 Max: 82 Sum: 1914 Ratio: 0.06%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 621171 (Eliminated: 0 Frozen: 191194) Constraints : 4522784 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 726MB Max. Length : 80 steps Models : 1 [endof: stats after solve call] Solving Time: 5.64s Memory: 667MB (+0MB) UNKNOWN Iteration Time: 5.70s Iteration 23 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)] Grounded Until: 80 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 24 Time : 147.911s (Solving: 131.12s 1st Model: 0.01s Unsat: 0.93s) CPU Time : 147.808s Choices : 3616155 (Domain: 3462337) Conflicts : 172662 (Analyzed: 172660) Restarts : 2033 (Average: 84.93 Last: 150) Model-Level : 254.0 Problems : 24 (Average Length: 42.42 Splits: 0) Lemmas : 172660 (Deleted: 158068) Binary : 5318 (Ratio: 3.08%) Ternary : 1065 (Ratio: 0.62%) Conflict : 172660 (Average Length: 794.3 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 172660 (Average: 19.17 Max: 818 Sum: 3309760) Executed : 172585 (Average: 19.16 Max: 818 Sum: 3307600 Ratio: 99.93%) Bounded : 75 (Average: 28.80 Max: 82 Sum: 2160 Ratio: 0.07%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 621171 (Eliminated: 0 Frozen: 191194) Constraints : 4522579 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 726MB Max. Length : 80 steps Models : 1 [endof: stats after solve call] Solving Time: 6.15s Memory: 667MB (+0MB) UNKNOWN Iteration Time: 6.20s Iteration 24 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)] Grounded Until: 80 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 25 Time : 156.601s (Solving: 139.68s 1st Model: 0.01s Unsat: 0.93s) CPU Time : 156.500s Choices : 3731283 (Domain: 3573611) Conflicts : 181844 (Analyzed: 181842) Restarts : 2133 (Average: 85.25 Last: 150) Model-Level : 254.0 Problems : 25 (Average Length: 44.00 Splits: 0) Lemmas : 181842 (Deleted: 165509) Binary : 5874 (Ratio: 3.23%) Ternary : 1244 (Ratio: 0.68%) Conflict : 181842 (Average Length: 766.6 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 181842 (Average: 18.79 Max: 818 Sum: 3416660) Executed : 181763 (Average: 18.78 Max: 818 Sum: 3414172 Ratio: 99.93%) Bounded : 79 (Average: 31.49 Max: 82 Sum: 2488 Ratio: 0.07%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 621171 (Eliminated: 0 Frozen: 191194) Constraints : 4522538 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 726MB Max. Length : 80 steps Models : 1 [endof: stats after solve call] Solving Time: 8.65s Memory: 667MB (+0MB) UNKNOWN Iteration Time: 8.70s Iteration 25 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)] Grounded Until: 80 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 26 Time : 164.981s (Solving: 147.94s 1st Model: 0.01s Unsat: 0.93s) CPU Time : 164.884s Choices : 3853462 (Domain: 3689639) Conflicts : 190803 (Analyzed: 190801) Restarts : 2233 (Average: 85.45 Last: 150) Model-Level : 254.0 Problems : 26 (Average Length: 45.46 Splits: 0) Lemmas : 190801 (Deleted: 174103) Binary : 6040 (Ratio: 3.17%) Ternary : 1303 (Ratio: 0.68%) Conflict : 190801 (Average Length: 746.5 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 190801 (Average: 18.48 Max: 818 Sum: 3526386) Executed : 190721 (Average: 18.47 Max: 818 Sum: 3523816 Ratio: 99.93%) Bounded : 80 (Average: 32.12 Max: 82 Sum: 2570 Ratio: 0.07%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 621171 (Eliminated: 0 Frozen: 191194) Constraints : 4519680 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 726MB Max. Length : 80 steps Models : 1 [endof: stats after solve call] Solving Time: 8.34s Memory: 667MB (+0MB) UNKNOWN Iteration Time: 8.39s Iteration 26 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)] Grounded Until: 80 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 27 Time : 174.129s (Solving: 156.97s 1st Model: 0.01s Unsat: 0.93s) CPU Time : 174.036s Choices : 4026215 (Domain: 3854302) Conflicts : 200213 (Analyzed: 200211) Restarts : 2333 (Average: 85.82 Last: 150) Model-Level : 254.0 Problems : 27 (Average Length: 46.81 Splits: 0) Lemmas : 200211 (Deleted: 182615) Binary : 6189 (Ratio: 3.09%) Ternary : 1328 (Ratio: 0.66%) Conflict : 200211 (Average Length: 727.9 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 200211 (Average: 18.41 Max: 818 Sum: 3685588) Executed : 200131 (Average: 18.40 Max: 818 Sum: 3683018 Ratio: 99.93%) Bounded : 80 (Average: 32.12 Max: 82 Sum: 2570 Ratio: 0.07%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 621171 (Eliminated: 0 Frozen: 191194) Constraints : 4519667 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 726MB Max. Length : 80 steps Models : 1 [endof: stats after solve call] Solving Time: 9.11s Memory: 667MB (+0MB) UNKNOWN Iteration Time: 9.15s Iteration 27 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)] Grounded Until: 80 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 28 Time : 183.475s (Solving: 166.18s 1st Model: 0.01s Unsat: 0.93s) CPU Time : 183.388s Choices : 4188503 (Domain: 4013177) Conflicts : 209061 (Analyzed: 209059) Restarts : 2433 (Average: 85.93 Last: 150) Model-Level : 254.0 Problems : 28 (Average Length: 48.07 Splits: 0) Lemmas : 209059 (Deleted: 191460) Binary : 6421 (Ratio: 3.07%) Ternary : 1402 (Ratio: 0.67%) Conflict : 209059 (Average Length: 711.0 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 209059 (Average: 18.34 Max: 818 Sum: 3834561) Executed : 208977 (Average: 18.33 Max: 818 Sum: 3831827 Ratio: 99.93%) Bounded : 82 (Average: 33.34 Max: 82 Sum: 2734 Ratio: 0.07%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 621171 (Eliminated: 0 Frozen: 191194) Constraints : 4519667 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 726MB Max. Length : 80 steps Models : 1 [endof: stats after solve call] Solving Time: 9.30s Memory: 667MB (+0MB) UNKNOWN Iteration Time: 9.35s Iteration 28 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)] Grounded Until: 80 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 29 Time : 194.149s (Solving: 176.69s 1st Model: 0.01s Unsat: 0.93s) CPU Time : 194.068s Choices : 4388056 (Domain: 4208740) Conflicts : 217872 (Analyzed: 217870) Restarts : 2533 (Average: 86.01 Last: 150) Model-Level : 254.0 Problems : 29 (Average Length: 49.24 Splits: 0) Lemmas : 217870 (Deleted: 199733) Binary : 6576 (Ratio: 3.02%) Ternary : 1444 (Ratio: 0.66%) Conflict : 217870 (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 : 217870 (Average: 18.44 Max: 818 Sum: 4017279) Executed : 217787 (Average: 18.43 Max: 818 Sum: 4014463 Ratio: 99.93%) Bounded : 83 (Average: 33.93 Max: 82 Sum: 2816 Ratio: 0.07%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 621171 (Eliminated: 0 Frozen: 191194) Constraints : 4519639 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 726MB Max. Length : 80 steps Models : 1 [endof: stats after solve call] Solving Time: 10.62s Memory: 667MB (+0MB) UNKNOWN Iteration Time: 10.68s Iteration 29 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)] Grounded Until: 80 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 30 Time : 205.573s (Solving: 187.96s 1st Model: 0.01s Unsat: 0.93s) CPU Time : 205.496s Choices : 4605515 (Domain: 4423171) Conflicts : 226831 (Analyzed: 226829) Restarts : 2633 (Average: 86.15 Last: 150) Model-Level : 254.0 Problems : 30 (Average Length: 50.33 Splits: 0) Lemmas : 226829 (Deleted: 208173) Binary : 6714 (Ratio: 2.96%) Ternary : 1482 (Ratio: 0.65%) Conflict : 226829 (Average Length: 679.7 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 226829 (Average: 18.60 Max: 818 Sum: 4219156) Executed : 226744 (Average: 18.59 Max: 818 Sum: 4216176 Ratio: 99.93%) Bounded : 85 (Average: 35.06 Max: 82 Sum: 2980 Ratio: 0.07%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 621171 (Eliminated: 0 Frozen: 191194) Constraints : 4519625 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 726MB Max. Length : 80 steps Models : 1 [endof: stats after solve call] Solving Time: 11.37s Memory: 667MB (+0MB) UNKNOWN Iteration Time: 11.43s Iteration 30 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)] Grounded Until: 80 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 31 Time : 215.341s (Solving: 197.60s 1st Model: 0.01s Unsat: 0.93s) CPU Time : 215.268s Choices : 4793152 (Domain: 4608690) Conflicts : 235198 (Analyzed: 235196) Restarts : 2733 (Average: 86.06 Last: 150) Model-Level : 254.0 Problems : 31 (Average Length: 51.35 Splits: 0) Lemmas : 235196 (Deleted: 214549) Binary : 6844 (Ratio: 2.91%) Ternary : 1505 (Ratio: 0.64%) Conflict : 235196 (Average Length: 665.9 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 235196 (Average: 18.66 Max: 818 Sum: 4389743) Executed : 235110 (Average: 18.65 Max: 818 Sum: 4386681 Ratio: 99.93%) Bounded : 86 (Average: 35.60 Max: 82 Sum: 3062 Ratio: 0.07%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 621171 (Eliminated: 0 Frozen: 191194) Constraints : 4519599 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 726MB Max. Length : 80 steps Models : 1 [endof: stats after solve call] Solving Time: 9.73s Memory: 667MB (+0MB) UNKNOWN Iteration Time: 9.78s Iteration 31 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)] Grounded Until: 80 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 32 Time : 225.223s (Solving: 207.34s 1st Model: 0.01s Unsat: 0.93s) CPU Time : 225.152s Choices : 5007257 (Domain: 4821249) Conflicts : 243968 (Analyzed: 243966) Restarts : 2833 (Average: 86.12 Last: 175) Model-Level : 254.0 Problems : 32 (Average Length: 52.31 Splits: 0) Lemmas : 243966 (Deleted: 224708) Binary : 6950 (Ratio: 2.85%) Ternary : 1543 (Ratio: 0.63%) Conflict : 243966 (Average Length: 652.4 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 243966 (Average: 18.81 Max: 818 Sum: 4589957) Executed : 243877 (Average: 18.80 Max: 818 Sum: 4586649 Ratio: 99.93%) Bounded : 89 (Average: 37.17 Max: 82 Sum: 3308 Ratio: 0.07%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 621171 (Eliminated: 0 Frozen: 191194) Constraints : 4519585 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 726MB Max. Length : 80 steps Models : 1 [endof: stats after solve call] Solving Time: 9.84s Memory: 667MB (+0MB) UNKNOWN Iteration Time: 9.89s Iteration 32 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)] Grounded Until: 80 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 33 Time : 234.701s (Solving: 216.68s 1st Model: 0.01s Unsat: 0.93s) CPU Time : 234.636s Choices : 5196384 (Domain: 5009297) Conflicts : 252514 (Analyzed: 252512) Restarts : 2933 (Average: 86.09 Last: 175) Model-Level : 254.0 Problems : 33 (Average Length: 53.21 Splits: 0) Lemmas : 252512 (Deleted: 230991) Binary : 7049 (Ratio: 2.79%) Ternary : 1572 (Ratio: 0.62%) Conflict : 252512 (Average Length: 640.0 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 252512 (Average: 18.87 Max: 818 Sum: 4764711) Executed : 252423 (Average: 18.86 Max: 818 Sum: 4761403 Ratio: 99.93%) Bounded : 89 (Average: 37.17 Max: 82 Sum: 3308 Ratio: 0.07%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 621171 (Eliminated: 0 Frozen: 191194) Constraints : 4519544 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 726MB Max. Length : 80 steps Models : 1 [endof: stats after solve call] Solving Time: 9.43s Memory: 667MB (+0MB) UNKNOWN Iteration Time: 9.48s Iteration 33 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)] Grounded Until: 80 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 34 Time : 242.672s (Solving: 224.52s 1st Model: 0.01s Unsat: 0.93s) CPU Time : 242.612s Choices : 5291696 (Domain: 5104282) Conflicts : 260780 (Analyzed: 260778) Restarts : 3033 (Average: 85.98 Last: 175) Model-Level : 254.0 Problems : 34 (Average Length: 54.06 Splits: 0) Lemmas : 260778 (Deleted: 240360) Binary : 7147 (Ratio: 2.74%) Ternary : 1588 (Ratio: 0.61%) Conflict : 260778 (Average Length: 631.0 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 260778 (Average: 18.59 Max: 818 Sum: 4846892) Executed : 260689 (Average: 18.57 Max: 818 Sum: 4843584 Ratio: 99.93%) Bounded : 89 (Average: 37.17 Max: 82 Sum: 3308 Ratio: 0.07%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 621171 (Eliminated: 0 Frozen: 191194) Constraints : 4519544 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 726MB Max. Length : 80 steps Models : 1 [endof: stats after solve call] Solving Time: 7.93s Memory: 667MB (+0MB) UNKNOWN Iteration Time: 7.98s Iteration 34 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)] Grounded Until: 80 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 35 Time : 254.873s (Solving: 236.60s 1st Model: 0.01s Unsat: 0.93s) CPU Time : 254.820s Choices : 5670287 (Domain: 5479652) Conflicts : 269812 (Analyzed: 269810) Restarts : 3133 (Average: 86.12 Last: 175) Model-Level : 254.0 Problems : 35 (Average Length: 54.86 Splits: 0) Lemmas : 269810 (Deleted: 249341) Binary : 7352 (Ratio: 2.72%) Ternary : 1664 (Ratio: 0.62%) Conflict : 269810 (Average Length: 618.6 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 269810 (Average: 19.28 Max: 966 Sum: 5203281) Executed : 269720 (Average: 19.27 Max: 966 Sum: 5199891 Ratio: 99.93%) Bounded : 90 (Average: 37.67 Max: 82 Sum: 3390 Ratio: 0.07%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 621171 (Eliminated: 0 Frozen: 191194) Constraints : 4519544 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 726MB Max. Length : 80 steps Models : 1 [endof: stats after solve call] Solving Time: 12.17s Memory: 667MB (+0MB) UNKNOWN Iteration Time: 12.21s Iteration 35 Queue: [(16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True)] Grounded Until: 80 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 36 Time : 267.508s (Solving: 249.11s 1st Model: 0.01s Unsat: 0.93s) CPU Time : 267.464s Choices : 6035181 (Domain: 5841662) Conflicts : 278819 (Analyzed: 278817) Restarts : 3233 (Average: 86.24 Last: 175) Model-Level : 254.0 Problems : 36 (Average Length: 55.61 Splits: 0) Lemmas : 278817 (Deleted: 257774) Binary : 7522 (Ratio: 2.70%) Ternary : 1720 (Ratio: 0.62%) Conflict : 278817 (Average Length: 607.5 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 278817 (Average: 19.89 Max: 1061 Sum: 5545315) Executed : 278724 (Average: 19.88 Max: 1061 Sum: 5541679 Ratio: 99.93%) Bounded : 93 (Average: 39.10 Max: 82 Sum: 3636 Ratio: 0.07%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 621171 (Eliminated: 0 Frozen: 191194) Constraints : 4519530 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 726MB Max. Length : 80 steps Models : 1 [endof: stats after solve call] Solving Time: 12.60s Memory: 667MB (+0MB) UNKNOWN Iteration Time: 12.64s Iteration 36 Queue: [(17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True)] Grounded Until: 80 Expected Memory: 744.0MB Grounding... [('step', [81]), ('step', [82]), ('step', [83]), ('step', [84]), ('step', [85]), ('check', [85])] Grounding Time: 0.59s Memory: 667MB (+0MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 37 Time : 278.843s (Solving: 259.27s 1st Model: 0.01s Unsat: 0.93s) CPU Time : 278.800s Choices : 6492250 (Domain: 6295822) Conflicts : 287420 (Analyzed: 287418) Restarts : 3333 (Average: 86.23 Last: 175) Model-Level : 254.0 Problems : 37 (Average Length: 56.46 Splits: 0) Lemmas : 287418 (Deleted: 266380) Binary : 7719 (Ratio: 2.69%) Ternary : 1739 (Ratio: 0.61%) Conflict : 287418 (Average Length: 614.6 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 287418 (Average: 20.79 Max: 1061 Sum: 5974881) Executed : 287325 (Average: 20.78 Max: 1061 Sum: 5971245 Ratio: 99.94%) Bounded : 93 (Average: 39.10 Max: 82 Sum: 3636 Ratio: 0.06%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 661247 (Eliminated: 0 Frozen: 203644) Constraints : 4821468 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 753MB Max. Length : 80 steps Models : 1 [endof: stats after solve call] Solving Time: 10.28s Memory: 689MB (+22MB) UNKNOWN Iteration Time: 11.35s Iteration 37 Queue: [(18,90,0,True), (19,95,0,True), (20,100,0,True)] Grounded Until: 85 Expected Memory: 766.0MB Grounding... [('step', [86]), ('step', [87]), ('step', [88]), ('step', [89]), ('step', [90]), ('check', [90])] Grounding Time: 0.59s Memory: 689MB (+0MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 38 Time : 289.370s (Solving: 268.58s 1st Model: 0.01s Unsat: 0.93s) CPU Time : 289.328s Choices : 6925880 (Domain: 6725902) Conflicts : 296604 (Analyzed: 296602) Restarts : 3433 (Average: 86.40 Last: 175) Model-Level : 254.0 Problems : 38 (Average Length: 57.39 Splits: 0) Lemmas : 296602 (Deleted: 277010) Binary : 7792 (Ratio: 2.63%) Ternary : 1746 (Ratio: 0.59%) Conflict : 296602 (Average Length: 624.1 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 296602 (Average: 21.49 Max: 1061 Sum: 6375261) Executed : 296509 (Average: 21.48 Max: 1061 Sum: 6371625 Ratio: 99.94%) Bounded : 93 (Average: 39.10 Max: 82 Sum: 3636 Ratio: 0.06%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 701323 (Eliminated: 0 Frozen: 216094) Constraints : 5123448 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 791MB Max. Length : 85 steps Models : 1 [endof: stats after solve call] Solving Time: 9.45s Memory: 791MB (+102MB) UNKNOWN Iteration Time: 10.54s Iteration 38 Queue: [(19,95,0,True), (20,100,0,True)] Grounded Until: 90 Expected Memory: 893.0MB Grounding... [('step', [91]), ('step', [92]), ('step', [93]), ('step', [94]), ('step', [95]), ('check', [95])] Grounding Time: 0.92s Memory: 791MB (+0MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 39 Time : 299.836s (Solving: 277.50s 1st Model: 0.01s Unsat: 0.93s) CPU Time : 299.796s Choices : 7279684 (Domain: 7077152) Conflicts : 304419 (Analyzed: 304417) Restarts : 3533 (Average: 86.16 Last: 175) Model-Level : 254.0 Problems : 39 (Average Length: 58.41 Splits: 0) Lemmas : 304417 (Deleted: 283811) Binary : 7827 (Ratio: 2.57%) Ternary : 1750 (Ratio: 0.57%) Conflict : 304417 (Average Length: 639.6 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 304417 (Average: 21.99 Max: 1061 Sum: 6693104) Executed : 304324 (Average: 21.97 Max: 1061 Sum: 6689468 Ratio: 99.95%) Bounded : 93 (Average: 39.10 Max: 82 Sum: 3636 Ratio: 0.05%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 741399 (Eliminated: 0 Frozen: 228544) Constraints : 5425428 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 882MB Max. Length : 90 steps Models : 1 [endof: stats after solve call] Solving Time: 9.06s Memory: 797MB (+6MB) UNKNOWN Iteration Time: 10.48s Iteration 39 Queue: [(20,100,0,True)] Grounded Until: 95 Expected Memory: 899.0MB Grounding... [('step', [96]), ('step', [97]), ('step', [98]), ('step', [99]), ('step', [100]), ('check', [100])] Grounding Time: 0.56s Memory: 797MB (+0MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 40 Time : 310.789s (Solving: 287.23s 1st Model: 0.01s Unsat: 0.93s) CPU Time : 310.752s Choices : 7694764 (Domain: 7489396) Conflicts : 312176 (Analyzed: 312174) Restarts : 3633 (Average: 85.93 Last: 175) Model-Level : 254.0 Problems : 40 (Average Length: 59.50 Splits: 0) Lemmas : 312174 (Deleted: 291534) Binary : 7854 (Ratio: 2.52%) Ternary : 1754 (Ratio: 0.56%) Conflict : 312174 (Average Length: 652.1 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 312174 (Average: 22.65 Max: 1061 Sum: 7071021) Executed : 312081 (Average: 22.64 Max: 1061 Sum: 7067385 Ratio: 99.95%) Bounded : 93 (Average: 39.10 Max: 82 Sum: 3636 Ratio: 0.05%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 781475 (Eliminated: 0 Frozen: 240994) Constraints : 5727408 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 898MB Max. Length : 95 steps Models : 1 [endof: stats after solve call] Solving Time: 9.88s Memory: 821MB (+24MB) UNKNOWN Iteration Time: 10.97s Iteration 40 Queue: [(3,15,3,True), (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,False), (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,0,True), (22,110,0,True)] Grounded Until: 100 Blocking actions... Solving... [start: stats after solve call] Models : 0 Calls : 41 Time : 311.274s (Solving: 287.56s 1st Model: 0.01s Unsat: 1.26s) CPU Time : 311.240s Choices : 7695314 (Domain: 7489946) Conflicts : 312400 (Analyzed: 312397) Restarts : 3636 (Average: 85.92 Last: 175) Model-Level : 254.0 Problems : 41 (Average Length: 60.54 Splits: 0) Lemmas : 312397 (Deleted: 291534) Binary : 7861 (Ratio: 2.52%) Ternary : 1759 (Ratio: 0.56%) Conflict : 312397 (Average Length: 651.7 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 312397 (Average: 22.64 Max: 1061 Sum: 7071567) Executed : 312302 (Average: 22.62 Max: 1061 Sum: 7067929 Ratio: 99.95%) Bounded : 95 (Average: 38.29 Max: 82 Sum: 3638 Ratio: 0.05%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 781475 (Eliminated: 0 Frozen: 240994) Constraints : 5727408 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 898MB Max. Length : 100 steps Models : 1 [endof: stats after solve call] Solving Time: 0.43s Memory: 821MB (+0MB) UNSAT Iteration Time: 0.49s Iteration 41 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,False), (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,0,True), (22,110,0,True)] Grounded Until: 100 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 42 Time : 321.291s (Solving: 297.42s 1st Model: 0.01s Unsat: 1.26s) CPU Time : 321.264s Choices : 7778212 (Domain: 7572844) Conflicts : 320938 (Analyzed: 320935) Restarts : 3736 (Average: 85.90 Last: 175) Model-Level : 254.0 Problems : 42 (Average Length: 61.52 Splits: 0) Lemmas : 320935 (Deleted: 297578) Binary : 7962 (Ratio: 2.48%) Ternary : 1787 (Ratio: 0.56%) Conflict : 320935 (Average Length: 648.5 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 320935 (Average: 22.27 Max: 1061 Sum: 7148340) Executed : 320836 (Average: 22.26 Max: 1061 Sum: 7144602 Ratio: 99.95%) Bounded : 99 (Average: 37.76 Max: 97 Sum: 3738 Ratio: 0.05%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 781475 (Eliminated: 0 Frozen: 240994) Constraints : 5727408 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 898MB Max. Length : 100 steps Models : 1 [endof: stats after solve call] Solving Time: 9.97s Memory: 821MB (+0MB) UNKNOWN Iteration Time: 10.02s Iteration 42 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,False), (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,0,True), (22,110,0,True)] Grounded Until: 100 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 43 Time : 328.910s (Solving: 304.88s 1st Model: 0.01s Unsat: 1.26s) CPU Time : 328.888s Choices : 7842415 (Domain: 7635242) Conflicts : 328957 (Analyzed: 328954) Restarts : 3836 (Average: 85.75 Last: 175) Model-Level : 254.0 Problems : 43 (Average Length: 62.47 Splits: 0) Lemmas : 328954 (Deleted: 305068) Binary : 8032 (Ratio: 2.44%) Ternary : 1809 (Ratio: 0.55%) Conflict : 328954 (Average Length: 639.0 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 328954 (Average: 21.90 Max: 1061 Sum: 7203294) Executed : 328854 (Average: 21.89 Max: 1061 Sum: 7199454 Ratio: 99.95%) Bounded : 100 (Average: 38.40 Max: 102 Sum: 3840 Ratio: 0.05%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 781475 (Eliminated: 0 Frozen: 240994) Constraints : 5727408 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 898MB Max. Length : 100 steps Models : 1 [endof: stats after solve call] Solving Time: 7.56s Memory: 821MB (+0MB) UNKNOWN Iteration Time: 7.62s Iteration 43 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,False), (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,0,True), (22,110,0,True)] Grounded Until: 100 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 44 Time : 337.176s (Solving: 312.99s 1st Model: 0.01s Unsat: 1.26s) CPU Time : 337.156s Choices : 7925575 (Domain: 7717227) Conflicts : 337204 (Analyzed: 337201) Restarts : 3936 (Average: 85.67 Last: 175) Model-Level : 254.0 Problems : 44 (Average Length: 63.36 Splits: 0) Lemmas : 337201 (Deleted: 312789) Binary : 8114 (Ratio: 2.41%) Ternary : 1839 (Ratio: 0.55%) Conflict : 337201 (Average Length: 630.1 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 337201 (Average: 21.58 Max: 1061 Sum: 7276712) Executed : 337099 (Average: 21.57 Max: 1061 Sum: 7272668 Ratio: 99.94%) Bounded : 102 (Average: 39.65 Max: 102 Sum: 4044 Ratio: 0.06%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 781475 (Eliminated: 0 Frozen: 240994) Constraints : 5727394 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 898MB Max. Length : 100 steps Models : 1 [endof: stats after solve call] Solving Time: 8.22s Memory: 821MB (+0MB) UNKNOWN Iteration Time: 8.27s Iteration 44 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,False), (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,0,True), (22,110,0,True)] Grounded Until: 100 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 45 Time : 345.060s (Solving: 320.70s 1st Model: 0.01s Unsat: 1.26s) CPU Time : 345.044s Choices : 7997611 (Domain: 7788740) Conflicts : 345433 (Analyzed: 345430) Restarts : 4036 (Average: 85.59 Last: 175) Model-Level : 254.0 Problems : 45 (Average Length: 64.22 Splits: 0) Lemmas : 345430 (Deleted: 320700) Binary : 8161 (Ratio: 2.36%) Ternary : 1850 (Ratio: 0.54%) Conflict : 345430 (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 : 345430 (Average: 21.25 Max: 1061 Sum: 7339477) Executed : 345328 (Average: 21.24 Max: 1061 Sum: 7335433 Ratio: 99.94%) Bounded : 102 (Average: 39.65 Max: 102 Sum: 4044 Ratio: 0.06%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 781475 (Eliminated: 0 Frozen: 240994) Constraints : 5727367 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 898MB Max. Length : 100 steps Models : 1 [endof: stats after solve call] Solving Time: 7.82s Memory: 821MB (+0MB) UNKNOWN Iteration Time: 7.89s Iteration 45 Queue: [(8,40,2,True), (9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,False), (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,0,True), (22,110,0,True)] Grounded Until: 100 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 46 Time : 353.439s (Solving: 328.91s 1st Model: 0.01s Unsat: 1.26s) CPU Time : 353.428s Choices : 8100519 (Domain: 7890476) Conflicts : 353550 (Analyzed: 353547) Restarts : 4136 (Average: 85.48 Last: 175) Model-Level : 254.0 Problems : 46 (Average Length: 65.04 Splits: 0) Lemmas : 353547 (Deleted: 328589) Binary : 8283 (Ratio: 2.34%) Ternary : 1884 (Ratio: 0.53%) Conflict : 353547 (Average Length: 613.4 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 353547 (Average: 21.02 Max: 1061 Sum: 7432066) Executed : 353444 (Average: 21.01 Max: 1061 Sum: 7427925 Ratio: 99.94%) Bounded : 103 (Average: 40.20 Max: 102 Sum: 4141 Ratio: 0.06%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 781475 (Eliminated: 0 Frozen: 240994) Constraints : 5727367 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 898MB Max. Length : 100 steps Models : 1 [endof: stats after solve call] Solving Time: 8.32s Memory: 821MB (+0MB) UNKNOWN Iteration Time: 8.39s Iteration 46 Queue: [(9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,False), (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,0,True), (22,110,0,True)] Grounded Until: 100 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 47 Time : 361.667s (Solving: 336.99s 1st Model: 0.01s Unsat: 1.26s) CPU Time : 361.660s Choices : 8216292 (Domain: 8005467) Conflicts : 361715 (Analyzed: 361712) Restarts : 4236 (Average: 85.39 Last: 175) Model-Level : 254.0 Problems : 47 (Average Length: 65.83 Splits: 0) Lemmas : 361712 (Deleted: 336327) Binary : 8344 (Ratio: 2.31%) Ternary : 1906 (Ratio: 0.53%) Conflict : 361712 (Average Length: 605.3 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 361712 (Average: 20.84 Max: 1061 Sum: 7538558) Executed : 361606 (Average: 20.83 Max: 1061 Sum: 7534116 Ratio: 99.94%) Bounded : 106 (Average: 41.91 Max: 102 Sum: 4442 Ratio: 0.06%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 781475 (Eliminated: 0 Frozen: 240994) Constraints : 5727367 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 898MB Max. Length : 100 steps Models : 1 [endof: stats after solve call] Solving Time: 8.18s Memory: 821MB (+0MB) UNKNOWN Iteration Time: 8.24s Iteration 47 Queue: [(10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,False), (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,0,True), (22,110,0,True)] Grounded Until: 100 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 48 Time : 369.596s (Solving: 344.74s 1st Model: 0.01s Unsat: 1.26s) CPU Time : 369.592s Choices : 8309386 (Domain: 8098255) Conflicts : 369874 (Analyzed: 369871) Restarts : 4336 (Average: 85.30 Last: 175) Model-Level : 254.0 Problems : 48 (Average Length: 66.58 Splits: 0) Lemmas : 369871 (Deleted: 344182) Binary : 8389 (Ratio: 2.27%) Ternary : 1916 (Ratio: 0.52%) Conflict : 369871 (Average Length: 597.5 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 369871 (Average: 20.61 Max: 1061 Sum: 7622602) Executed : 369762 (Average: 20.60 Max: 1061 Sum: 7617869 Ratio: 99.94%) Bounded : 109 (Average: 43.42 Max: 102 Sum: 4733 Ratio: 0.06%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 781475 (Eliminated: 0 Frozen: 240994) Constraints : 5724726 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 898MB Max. Length : 100 steps Models : 1 [endof: stats after solve call] Solving Time: 7.87s Memory: 821MB (+0MB) UNKNOWN Iteration Time: 7.93s Iteration 48 Queue: [(11,55,2,True), (12,60,2,True), (13,65,2,False), (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,0,True), (22,110,0,True)] Grounded Until: 100 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 49 Time : 376.690s (Solving: 351.69s 1st Model: 0.01s Unsat: 1.26s) CPU Time : 376.688s Choices : 8387060 (Domain: 8175628) Conflicts : 377753 (Analyzed: 377750) Restarts : 4436 (Average: 85.16 Last: 175) Model-Level : 254.0 Problems : 49 (Average Length: 67.31 Splits: 0) Lemmas : 377750 (Deleted: 352030) Binary : 8450 (Ratio: 2.24%) Ternary : 1933 (Ratio: 0.51%) Conflict : 377750 (Average Length: 590.7 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 377750 (Average: 20.36 Max: 1061 Sum: 7690130) Executed : 377637 (Average: 20.34 Max: 1061 Sum: 7684998 Ratio: 99.93%) Bounded : 113 (Average: 45.42 Max: 102 Sum: 5132 Ratio: 0.07%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 781475 (Eliminated: 0 Frozen: 240994) Constraints : 5724726 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 898MB Max. Length : 100 steps Models : 1 [endof: stats after solve call] Solving Time: 7.05s Memory: 821MB (+0MB) UNKNOWN Iteration Time: 7.10s Iteration 49 Queue: [(12,60,2,True), (13,65,2,False), (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,0,True), (22,110,0,True)] Grounded Until: 100 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 50 Time : 386.491s (Solving: 361.29s 1st Model: 0.01s Unsat: 1.26s) CPU Time : 386.496s Choices : 8718905 (Domain: 8505205) Conflicts : 386599 (Analyzed: 386596) Restarts : 4536 (Average: 85.23 Last: 175) Model-Level : 254.0 Problems : 50 (Average Length: 68.00 Splits: 0) Lemmas : 386596 (Deleted: 361308) Binary : 8919 (Ratio: 2.31%) Ternary : 2114 (Ratio: 0.55%) Conflict : 386596 (Average Length: 582.6 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 386596 (Average: 20.71 Max: 1061 Sum: 8007308) Executed : 386482 (Average: 20.70 Max: 1061 Sum: 8002079 Ratio: 99.93%) Bounded : 114 (Average: 45.87 Max: 102 Sum: 5229 Ratio: 0.07%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 781475 (Eliminated: 0 Frozen: 240994) Constraints : 5724686 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 898MB Max. Length : 100 steps Models : 1 [endof: stats after solve call] Solving Time: 9.73s Memory: 821MB (+0MB) UNKNOWN Iteration Time: 9.81s Iteration 50 Queue: [(17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,0,True), (22,110,0,True)] Grounded Until: 100 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 51 Time : 394.728s (Solving: 369.36s 1st Model: 0.01s Unsat: 1.26s) CPU Time : 394.736s Choices : 9024213 (Domain: 8808303) Conflicts : 394396 (Analyzed: 394393) Restarts : 4636 (Average: 85.07 Last: 175) Model-Level : 254.0 Problems : 51 (Average Length: 68.67 Splits: 0) Lemmas : 394393 (Deleted: 367228) Binary : 9101 (Ratio: 2.31%) Ternary : 2169 (Ratio: 0.55%) Conflict : 394393 (Average Length: 576.0 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 394393 (Average: 21.04 Max: 1061 Sum: 8296840) Executed : 394279 (Average: 21.02 Max: 1061 Sum: 8291611 Ratio: 99.94%) Bounded : 114 (Average: 45.87 Max: 102 Sum: 5229 Ratio: 0.06%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 781475 (Eliminated: 0 Frozen: 240994) Constraints : 5724686 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 898MB Max. Length : 100 steps Models : 1 [endof: stats after solve call] Solving Time: 8.18s Memory: 821MB (+0MB) UNKNOWN Iteration Time: 8.24s Iteration 51 Queue: [(18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,0,True), (22,110,0,True)] Grounded Until: 100 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 52 Time : 404.262s (Solving: 378.74s 1st Model: 0.01s Unsat: 1.26s) CPU Time : 404.276s Choices : 9292134 (Domain: 9074978) Conflicts : 402431 (Analyzed: 402428) Restarts : 4736 (Average: 84.97 Last: 175) Model-Level : 254.0 Problems : 52 (Average Length: 69.31 Splits: 0) Lemmas : 402428 (Deleted: 374683) Binary : 9231 (Ratio: 2.29%) Ternary : 2198 (Ratio: 0.55%) Conflict : 402428 (Average Length: 569.9 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 402428 (Average: 21.24 Max: 1075 Sum: 8547240) Executed : 402314 (Average: 21.23 Max: 1075 Sum: 8542011 Ratio: 99.94%) Bounded : 114 (Average: 45.87 Max: 102 Sum: 5229 Ratio: 0.06%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 781475 (Eliminated: 0 Frozen: 240994) Constraints : 5724686 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 898MB Max. Length : 100 steps Models : 1 [endof: stats after solve call] Solving Time: 9.49s Memory: 821MB (+0MB) UNKNOWN Iteration Time: 9.54s Iteration 52 Queue: [(19,95,1,True), (20,100,1,True), (21,105,0,True), (22,110,0,True)] Grounded Until: 100 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 53 Time : 413.940s (Solving: 388.26s 1st Model: 0.01s Unsat: 1.26s) CPU Time : 413.960s Choices : 9562327 (Domain: 9344325) Conflicts : 410458 (Analyzed: 410455) Restarts : 4836 (Average: 84.87 Last: 175) Model-Level : 254.0 Problems : 53 (Average Length: 69.92 Splits: 0) Lemmas : 410455 (Deleted: 382351) Binary : 9301 (Ratio: 2.27%) Ternary : 2222 (Ratio: 0.54%) Conflict : 410455 (Average Length: 564.2 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 410455 (Average: 21.43 Max: 1126 Sum: 8797640) Executed : 410341 (Average: 21.42 Max: 1126 Sum: 8792411 Ratio: 99.94%) Bounded : 114 (Average: 45.87 Max: 102 Sum: 5229 Ratio: 0.06%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 781475 (Eliminated: 0 Frozen: 240994) Constraints : 5724686 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 898MB Max. Length : 100 steps Models : 1 [endof: stats after solve call] Solving Time: 9.63s Memory: 821MB (+0MB) UNKNOWN Iteration Time: 9.68s Iteration 53 Queue: [(20,100,1,True), (21,105,0,True), (22,110,0,True)] Grounded Until: 100 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 54 Time : 429.082s (Solving: 403.25s 1st Model: 0.01s Unsat: 1.26s) CPU Time : 429.108s Choices : 10126990 (Domain: 9906927) Conflicts : 419268 (Analyzed: 419265) Restarts : 4936 (Average: 84.94 Last: 175) Model-Level : 254.0 Problems : 54 (Average Length: 70.52 Splits: 0) Lemmas : 419265 (Deleted: 391947) Binary : 9605 (Ratio: 2.29%) Ternary : 2334 (Ratio: 0.56%) Conflict : 419265 (Average Length: 558.8 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 419265 (Average: 22.28 Max: 1130 Sum: 9340952) Executed : 419150 (Average: 22.27 Max: 1130 Sum: 9335621 Ratio: 99.94%) Bounded : 115 (Average: 46.36 Max: 102 Sum: 5331 Ratio: 0.06%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 781475 (Eliminated: 0 Frozen: 240994) Constraints : 5724686 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 898MB Max. Length : 100 steps Models : 1 [endof: stats after solve call] Solving Time: 15.10s Memory: 821MB (+0MB) UNKNOWN Iteration Time: 15.15s Iteration 54 Queue: [(21,105,0,True), (22,110,0,True)] Grounded Until: 100 Expected Memory: 923.0MB Grounding... [('step', [101]), ('step', [102]), ('step', [103]), ('step', [104]), ('step', [105]), ('check', [105])] Grounding Time: 0.57s Memory: 822MB (+1MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 55 Time : 443.624s (Solving: 416.54s 1st Model: 0.01s Unsat: 1.26s) CPU Time : 443.656s Choices : 10679603 (Domain: 10455698) Conflicts : 428070 (Analyzed: 428067) Restarts : 5036 (Average: 85.00 Last: 175) Model-Level : 254.0 Problems : 55 (Average Length: 71.18 Splits: 0) Lemmas : 428067 (Deleted: 400883) Binary : 9734 (Ratio: 2.27%) Ternary : 2367 (Ratio: 0.55%) Conflict : 428067 (Average Length: 563.5 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 428067 (Average: 23.03 Max: 1146 Sum: 9857106) Executed : 427952 (Average: 23.01 Max: 1146 Sum: 9851775 Ratio: 99.95%) Bounded : 115 (Average: 46.36 Max: 102 Sum: 5331 Ratio: 0.05%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 821551 (Eliminated: 0 Frozen: 253444) Constraints : 6026640 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 938MB Max. Length : 100 steps Models : 1 [endof: stats after solve call] Solving Time: 13.45s Memory: 848MB (+26MB) UNKNOWN Iteration Time: 14.56s Iteration 55 Queue: [(22,110,0,True)] Grounded Until: 105 Expected Memory: 950.0MB Grounding... [('step', [106]), ('step', [107]), ('step', [108]), ('step', [109]), ('step', [110]), ('check', [110])] Grounding Time: 0.56s Memory: 848MB (+0MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 56 Time : 455.316s (Solving: 426.99s 1st Model: 0.01s Unsat: 1.26s) CPU Time : 455.352s Choices : 11009832 (Domain: 10784491) Conflicts : 435988 (Analyzed: 435985) Restarts : 5136 (Average: 84.89 Last: 175) Model-Level : 254.0 Problems : 56 (Average Length: 71.91 Splits: 0) Lemmas : 435985 (Deleted: 408670) Binary : 9768 (Ratio: 2.24%) Ternary : 2371 (Ratio: 0.54%) Conflict : 435985 (Average Length: 571.6 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 435985 (Average: 23.28 Max: 1146 Sum: 10147993) Executed : 435870 (Average: 23.26 Max: 1146 Sum: 10142662 Ratio: 99.95%) Bounded : 115 (Average: 46.36 Max: 102 Sum: 5331 Ratio: 0.05%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 861627 (Eliminated: 0 Frozen: 265894) Constraints : 6328620 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 971MB Max. Length : 105 steps Models : 1 [endof: stats after solve call] Solving Time: 10.61s Memory: 881MB (+33MB) UNKNOWN Iteration Time: 11.71s Iteration 56 Queue: [(4,20,4,True), (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,False), (12,60,3,False), (13,65,2,True), (14,70,2,True), (15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,1,True), (22,110,1,True), (23,115,0,True)] Grounded Until: 110 Blocking actions... Solving... [start: stats after solve call] Models : 0 Calls : 57 Time : 466.556s (Solving: 438.01s 1st Model: 0.01s Unsat: 12.29s) CPU Time : 466.600s Choices : 11089562 (Domain: 10864221) Conflicts : 442558 (Analyzed: 442554) Restarts : 5210 (Average: 84.94 Last: 175) Model-Level : 254.0 Problems : 57 (Average Length: 72.61 Splits: 0) Lemmas : 442554 (Deleted: 414658) Binary : 9922 (Ratio: 2.24%) Ternary : 2388 (Ratio: 0.54%) Conflict : 442554 (Average Length: 568.1 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 442554 (Average: 23.11 Max: 1146 Sum: 10226036) Executed : 442431 (Average: 23.09 Max: 1146 Sum: 10220591 Ratio: 99.95%) Bounded : 123 (Average: 44.27 Max: 107 Sum: 5445 Ratio: 0.05%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 861627 (Eliminated: 0 Frozen: 265894) Constraints : 6328620 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 971MB Max. Length : 110 steps Models : 1 [endof: stats after solve call] Solving Time: 11.16s Memory: 884MB (+3MB) UNSAT Iteration Time: 11.25s 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,False), (12,60,3,False), (13,65,2,True), (14,70,2,True), (15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,1,True), (22,110,1,True), (23,115,0,True)] Grounded Until: 110 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 58 Time : 472.195s (Solving: 443.47s 1st Model: 0.01s Unsat: 12.29s) CPU Time : 472.240s Choices : 11140666 (Domain: 10915316) Conflicts : 450162 (Analyzed: 450158) Restarts : 5310 (Average: 84.78 Last: 175) Model-Level : 254.0 Problems : 58 (Average Length: 73.29 Splits: 0) Lemmas : 450158 (Deleted: 420439) Binary : 9993 (Ratio: 2.22%) Ternary : 2417 (Ratio: 0.54%) Conflict : 450158 (Average Length: 563.2 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 450158 (Average: 22.81 Max: 1146 Sum: 10269499) Executed : 450035 (Average: 22.80 Max: 1146 Sum: 10264054 Ratio: 99.95%) Bounded : 123 (Average: 44.27 Max: 107 Sum: 5445 Ratio: 0.05%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 861627 (Eliminated: 0 Frozen: 265894) Constraints : 6328620 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 971MB Max. Length : 110 steps Models : 1 [endof: stats after solve call] Solving Time: 5.58s Memory: 884MB (+0MB) UNKNOWN Iteration Time: 5.65s 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,False), (12,60,3,False), (13,65,2,True), (14,70,2,True), (15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,1,True), (22,110,1,True), (23,115,0,True)] Grounded Until: 110 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 59 Time : 477.975s (Solving: 449.05s 1st Model: 0.01s Unsat: 12.29s) CPU Time : 478.020s Choices : 11195924 (Domain: 10970510) Conflicts : 457999 (Analyzed: 457995) Restarts : 5410 (Average: 84.66 Last: 175) Model-Level : 254.0 Problems : 59 (Average Length: 73.95 Splits: 0) Lemmas : 457995 (Deleted: 427638) Binary : 10078 (Ratio: 2.20%) Ternary : 2438 (Ratio: 0.53%) Conflict : 457995 (Average Length: 558.2 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 457995 (Average: 22.53 Max: 1146 Sum: 10317774) Executed : 457870 (Average: 22.52 Max: 1146 Sum: 10312110 Ratio: 99.95%) Bounded : 125 (Average: 45.31 Max: 112 Sum: 5664 Ratio: 0.05%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 861627 (Eliminated: 0 Frozen: 265894) Constraints : 6328620 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 971MB Max. Length : 110 steps Models : 1 [endof: stats after solve call] Solving Time: 5.71s Memory: 884MB (+0MB) UNKNOWN Iteration Time: 5.79s Iteration 59 Queue: [(7,35,3,True), (8,40,3,True), (9,45,3,True), (10,50,3,True), (11,55,3,False), (12,60,3,False), (13,65,2,True), (14,70,2,True), (15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,1,True), (22,110,1,True), (23,115,0,True)] Grounded Until: 110 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 60 Time : 485.713s (Solving: 456.59s 1st Model: 0.01s Unsat: 12.29s) CPU Time : 485.764s Choices : 11299372 (Domain: 11072098) Conflicts : 466473 (Analyzed: 466469) Restarts : 5510 (Average: 84.66 Last: 175) Model-Level : 254.0 Problems : 60 (Average Length: 74.58 Splits: 0) Lemmas : 466469 (Deleted: 435134) Binary : 10300 (Ratio: 2.21%) Ternary : 2544 (Ratio: 0.55%) Conflict : 466469 (Average Length: 552.8 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 466469 (Average: 22.32 Max: 1146 Sum: 10410869) Executed : 466342 (Average: 22.31 Max: 1146 Sum: 10404986 Ratio: 99.94%) Bounded : 127 (Average: 46.32 Max: 112 Sum: 5883 Ratio: 0.06%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 861627 (Eliminated: 0 Frozen: 265894) Constraints : 6328606 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 971MB Max. Length : 110 steps Models : 1 [endof: stats after solve call] Solving Time: 7.67s Memory: 884MB (+0MB) UNKNOWN Iteration Time: 7.74s Iteration 60 Queue: [(8,40,3,True), (9,45,3,True), (10,50,3,True), (11,55,3,False), (12,60,3,False), (13,65,2,True), (14,70,2,True), (15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,1,True), (22,110,1,True), (23,115,0,True)] Grounded Until: 110 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 61 Time : 493.456s (Solving: 464.11s 1st Model: 0.01s Unsat: 12.29s) CPU Time : 493.508s Choices : 11420205 (Domain: 11191068) Conflicts : 475017 (Analyzed: 475013) Restarts : 5610 (Average: 84.67 Last: 175) Model-Level : 254.0 Problems : 61 (Average Length: 75.20 Splits: 0) Lemmas : 475013 (Deleted: 443064) Binary : 10587 (Ratio: 2.23%) Ternary : 2626 (Ratio: 0.55%) Conflict : 475013 (Average Length: 547.9 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 475013 (Average: 22.15 Max: 1146 Sum: 10520141) Executed : 474886 (Average: 22.13 Max: 1146 Sum: 10514258 Ratio: 99.94%) Bounded : 127 (Average: 46.32 Max: 112 Sum: 5883 Ratio: 0.06%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 861627 (Eliminated: 0 Frozen: 265894) Constraints : 6328580 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 971MB Max. Length : 110 steps Models : 1 [endof: stats after solve call] Solving Time: 7.66s Memory: 884MB (+0MB) UNKNOWN Iteration Time: 7.75s Iteration 61 Queue: [(9,45,3,True), (10,50,3,True), (11,55,3,False), (12,60,3,False), (13,65,2,True), (14,70,2,True), (15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,1,True), (22,110,1,True), (23,115,0,True)] Grounded Until: 110 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 62 Time : 500.880s (Solving: 471.35s 1st Model: 0.01s Unsat: 12.29s) CPU Time : 500.936s Choices : 11544660 (Domain: 11313881) Conflicts : 482966 (Analyzed: 482962) Restarts : 5710 (Average: 84.58 Last: 175) Model-Level : 254.0 Problems : 62 (Average Length: 75.79 Splits: 0) Lemmas : 482962 (Deleted: 451002) Binary : 10724 (Ratio: 2.22%) Ternary : 2664 (Ratio: 0.55%) Conflict : 482962 (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 : 482962 (Average: 22.02 Max: 1146 Sum: 10632575) Executed : 482835 (Average: 22.00 Max: 1146 Sum: 10626692 Ratio: 99.94%) Bounded : 127 (Average: 46.32 Max: 112 Sum: 5883 Ratio: 0.06%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 861627 (Eliminated: 0 Frozen: 265894) Constraints : 6328580 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 971MB Max. Length : 110 steps Models : 1 [endof: stats after solve call] Solving Time: 7.36s Memory: 884MB (+0MB) UNKNOWN Iteration Time: 7.43s Iteration 62 Queue: [(10,50,3,True), (11,55,3,False), (12,60,3,False), (13,65,2,True), (14,70,2,True), (15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,1,True), (22,110,1,True), (23,115,0,True)] Grounded Until: 110 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 63 Time : 510.227s (Solving: 480.52s 1st Model: 0.01s Unsat: 12.29s) CPU Time : 510.288s Choices : 11752698 (Domain: 11519372) Conflicts : 491386 (Analyzed: 491382) Restarts : 5810 (Average: 84.58 Last: 175) Model-Level : 254.0 Problems : 63 (Average Length: 76.37 Splits: 0) Lemmas : 491382 (Deleted: 458343) Binary : 11120 (Ratio: 2.26%) Ternary : 2838 (Ratio: 0.58%) Conflict : 491382 (Average Length: 538.2 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 491382 (Average: 22.03 Max: 1146 Sum: 10825014) Executed : 491254 (Average: 22.02 Max: 1146 Sum: 10819019 Ratio: 99.94%) Bounded : 128 (Average: 46.84 Max: 112 Sum: 5995 Ratio: 0.06%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 861627 (Eliminated: 0 Frozen: 265894) Constraints : 6328580 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 971MB Max. Length : 110 steps Models : 1 [endof: stats after solve call] Solving Time: 9.29s Memory: 884MB (+0MB) UNKNOWN Iteration Time: 9.35s Iteration 63 Queue: [(13,65,2,True), (14,70,2,True), (15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,1,True), (22,110,1,True), (23,115,0,True)] Grounded Until: 110 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 64 Time : 517.566s (Solving: 487.69s 1st Model: 0.01s Unsat: 12.29s) CPU Time : 517.632s Choices : 11913679 (Domain: 11679834) Conflicts : 499648 (Analyzed: 499644) Restarts : 5910 (Average: 84.54 Last: 175) Model-Level : 254.0 Problems : 64 (Average Length: 76.92 Splits: 0) Lemmas : 499644 (Deleted: 465893) Binary : 11349 (Ratio: 2.27%) Ternary : 2891 (Ratio: 0.58%) Conflict : 499644 (Average Length: 533.3 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 499644 (Average: 21.96 Max: 1146 Sum: 10971841) Executed : 499515 (Average: 21.95 Max: 1146 Sum: 10965739 Ratio: 99.94%) Bounded : 129 (Average: 47.30 Max: 112 Sum: 6102 Ratio: 0.06%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 861627 (Eliminated: 0 Frozen: 265894) Constraints : 6328554 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 971MB Max. Length : 110 steps Models : 1 [endof: stats after solve call] Solving Time: 7.29s Memory: 884MB (+0MB) UNKNOWN Iteration Time: 7.34s Iteration 64 Queue: [(14,70,2,True), (15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,1,True), (22,110,1,True), (23,115,0,True)] Grounded Until: 110 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 65 Time : 526.309s (Solving: 496.25s 1st Model: 0.01s Unsat: 12.29s) CPU Time : 526.376s Choices : 12115412 (Domain: 11880075) Conflicts : 507889 (Analyzed: 507885) Restarts : 6010 (Average: 84.51 Last: 175) Model-Level : 254.0 Problems : 65 (Average Length: 77.46 Splits: 0) Lemmas : 507885 (Deleted: 473600) Binary : 11555 (Ratio: 2.28%) Ternary : 2941 (Ratio: 0.58%) Conflict : 507885 (Average Length: 529.4 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 507885 (Average: 21.97 Max: 1146 Sum: 11157853) Executed : 507756 (Average: 21.96 Max: 1146 Sum: 11151751 Ratio: 99.95%) Bounded : 129 (Average: 47.30 Max: 112 Sum: 6102 Ratio: 0.05%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 861627 (Eliminated: 0 Frozen: 265894) Constraints : 6328554 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 971MB Max. Length : 110 steps Models : 1 [endof: stats after solve call] Solving Time: 8.68s Memory: 884MB (+0MB) UNKNOWN Iteration Time: 8.75s Iteration 65 Queue: [(15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,1,True), (22,110,1,True), (23,115,0,True)] Grounded Until: 110 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 66 Time : 531.173s (Solving: 500.94s 1st Model: 0.01s Unsat: 12.29s) CPU Time : 531.240s Choices : 12257399 (Domain: 12021648) Conflicts : 515266 (Analyzed: 515262) Restarts : 6110 (Average: 84.33 Last: 175) Model-Level : 254.0 Problems : 66 (Average Length: 77.98 Splits: 0) Lemmas : 515262 (Deleted: 481624) Binary : 11680 (Ratio: 2.27%) Ternary : 2981 (Ratio: 0.58%) Conflict : 515262 (Average Length: 524.5 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 515262 (Average: 21.90 Max: 1146 Sum: 11283889) Executed : 515133 (Average: 21.89 Max: 1146 Sum: 11277787 Ratio: 99.95%) Bounded : 129 (Average: 47.30 Max: 112 Sum: 6102 Ratio: 0.05%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 861627 (Eliminated: 0 Frozen: 265894) Constraints : 6328554 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 971MB Max. Length : 110 steps Models : 1 [endof: stats after solve call] Solving Time: 4.81s Memory: 884MB (+0MB) UNKNOWN Iteration Time: 4.87s Iteration 66 Queue: [(21,105,1,True), (22,110,1,True), (23,115,0,True)] Grounded Until: 110 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 67 Time : 541.644s (Solving: 511.24s 1st Model: 0.01s Unsat: 12.29s) CPU Time : 541.716s Choices : 12611331 (Domain: 12374369) Conflicts : 523435 (Analyzed: 523431) Restarts : 6210 (Average: 84.29 Last: 175) Model-Level : 254.0 Problems : 67 (Average Length: 78.49 Splits: 0) Lemmas : 523431 (Deleted: 488321) Binary : 12008 (Ratio: 2.29%) Ternary : 3047 (Ratio: 0.58%) Conflict : 523431 (Average Length: 520.2 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 523431 (Average: 22.19 Max: 1227 Sum: 11616138) Executed : 523301 (Average: 22.18 Max: 1227 Sum: 11609924 Ratio: 99.95%) Bounded : 130 (Average: 47.80 Max: 112 Sum: 6214 Ratio: 0.05%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 861627 (Eliminated: 0 Frozen: 265894) Constraints : 6328554 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 971MB Max. Length : 110 steps Models : 1 [endof: stats after solve call] Solving Time: 10.42s Memory: 884MB (+0MB) UNKNOWN Iteration Time: 10.48s Iteration 67 Queue: [(22,110,1,True), (23,115,0,True)] Grounded Until: 110 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 68 Time : 553.874s (Solving: 523.30s 1st Model: 0.01s Unsat: 12.29s) CPU Time : 553.952s Choices : 12992440 (Domain: 12754027) Conflicts : 531758 (Analyzed: 531754) Restarts : 6310 (Average: 84.27 Last: 175) Model-Level : 254.0 Problems : 68 (Average Length: 78.99 Splits: 0) Lemmas : 531754 (Deleted: 495804) Binary : 12298 (Ratio: 2.31%) Ternary : 3145 (Ratio: 0.59%) Conflict : 531754 (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 : 531754 (Average: 22.52 Max: 1313 Sum: 11973008) Executed : 531624 (Average: 22.50 Max: 1313 Sum: 11966794 Ratio: 99.95%) Bounded : 130 (Average: 47.80 Max: 112 Sum: 6214 Ratio: 0.05%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 861627 (Eliminated: 0 Frozen: 265894) Constraints : 6328540 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 971MB Max. Length : 110 steps Models : 1 [endof: stats after solve call] Solving Time: 12.18s Memory: 884MB (+0MB) UNKNOWN Iteration Time: 12.24s Iteration 68 Queue: [(23,115,0,True)] Grounded Until: 110 Expected Memory: 986.0MB Grounding... [('step', [111]), ('step', [112]), ('step', [113]), ('step', [114]), ('step', [115]), ('check', [115])] Grounding Time: 0.59s Memory: 884MB (+0MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 69 Time : 570.212s (Solving: 538.31s 1st Model: 0.01s Unsat: 12.29s) CPU Time : 570.296s Choices : 13409834 (Domain: 13170777) Conflicts : 541304 (Analyzed: 541300) Restarts : 6410 (Average: 84.45 Last: 175) Model-Level : 254.0 Problems : 69 (Average Length: 79.54 Splits: 0) Lemmas : 541300 (Deleted: 505809) Binary : 12573 (Ratio: 2.32%) Ternary : 3215 (Ratio: 0.59%) Conflict : 541300 (Average Length: 521.5 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 541300 (Average: 22.82 Max: 1313 Sum: 12349815) Executed : 541170 (Average: 22.80 Max: 1313 Sum: 12343601 Ratio: 99.95%) Bounded : 130 (Average: 47.80 Max: 112 Sum: 6214 Ratio: 0.05%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 901703 (Eliminated: 0 Frozen: 278344) Constraints : 6630520 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1037MB Max. Length : 110 steps Models : 1 [endof: stats after solve call] Solving Time: 15.18s Memory: 973MB (+89MB) UNKNOWN Iteration Time: 16.36s Iteration 69 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,3,True), (12,60,3,True), (13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,2,True), (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,1,True), (24,120,0,True)] Grounded Until: 115 Blocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 70 Time : 574.954s (Solving: 542.86s 1st Model: 0.01s Unsat: 12.29s) CPU Time : 575.040s Choices : 13446171 (Domain: 13207114) Conflicts : 548635 (Analyzed: 548631) Restarts : 6510 (Average: 84.28 Last: 175) Model-Level : 254.0 Problems : 70 (Average Length: 80.07 Splits: 0) Lemmas : 548631 (Deleted: 512656) Binary : 12660 (Ratio: 2.31%) Ternary : 3219 (Ratio: 0.59%) Conflict : 548631 (Average Length: 518.3 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 548631 (Average: 22.56 Max: 1313 Sum: 12377314) Executed : 548501 (Average: 22.55 Max: 1313 Sum: 12371100 Ratio: 99.95%) Bounded : 130 (Average: 47.80 Max: 112 Sum: 6214 Ratio: 0.05%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 901703 (Eliminated: 0 Frozen: 278344) Constraints : 6630520 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1037MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 4.67s Memory: 973MB (+0MB) UNKNOWN Iteration Time: 4.75s Iteration 70 Queue: [(6,30,5,True), (7,35,4,True), (8,40,4,True), (9,45,4,True), (10,50,4,True), (11,55,3,True), (12,60,3,True), (13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,2,True), (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,1,True), (24,120,0,True)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 71 Time : 579.391s (Solving: 547.09s 1st Model: 0.01s Unsat: 12.29s) CPU Time : 579.480s Choices : 13491098 (Domain: 13252041) Conflicts : 556034 (Analyzed: 556030) Restarts : 6610 (Average: 84.12 Last: 175) Model-Level : 254.0 Problems : 71 (Average Length: 80.59 Splits: 0) Lemmas : 556030 (Deleted: 519769) Binary : 12694 (Ratio: 2.28%) Ternary : 3227 (Ratio: 0.58%) Conflict : 556030 (Average Length: 514.6 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 556030 (Average: 22.32 Max: 1313 Sum: 12413263) Executed : 555900 (Average: 22.31 Max: 1313 Sum: 12407049 Ratio: 99.95%) Bounded : 130 (Average: 47.80 Max: 112 Sum: 6214 Ratio: 0.05%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 901703 (Eliminated: 0 Frozen: 278344) Constraints : 6630520 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1037MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 4.37s Memory: 973MB (+0MB) UNKNOWN Iteration Time: 4.44s Iteration 71 Queue: [(7,35,4,True), (8,40,4,True), (9,45,4,True), (10,50,4,True), (11,55,3,True), (12,60,3,True), (13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,2,True), (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,1,True), (24,120,0,True)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 72 Time : 585.615s (Solving: 553.14s 1st Model: 0.01s Unsat: 12.29s) CPU Time : 585.708s Choices : 13531946 (Domain: 13292889) Conflicts : 563864 (Analyzed: 563860) Restarts : 6710 (Average: 84.03 Last: 175) Model-Level : 254.0 Problems : 72 (Average Length: 81.10 Splits: 0) Lemmas : 563860 (Deleted: 526767) Binary : 12787 (Ratio: 2.27%) Ternary : 3256 (Ratio: 0.58%) Conflict : 563860 (Average Length: 511.2 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 563860 (Average: 22.08 Max: 1313 Sum: 12447450) Executed : 563729 (Average: 22.06 Max: 1313 Sum: 12441124 Ratio: 99.95%) Bounded : 131 (Average: 48.29 Max: 112 Sum: 6326 Ratio: 0.05%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 901703 (Eliminated: 0 Frozen: 278344) Constraints : 6630520 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1037MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 6.17s Memory: 973MB (+0MB) UNKNOWN Iteration Time: 6.23s Iteration 72 Queue: [(8,40,4,True), (9,45,4,True), (10,50,4,True), (11,55,3,True), (12,60,3,True), (13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,2,True), (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,1,True), (24,120,0,True)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 73 Time : 592.702s (Solving: 560.05s 1st Model: 0.01s Unsat: 12.29s) CPU Time : 592.796s Choices : 13614649 (Domain: 13374499) Conflicts : 571828 (Analyzed: 571824) Restarts : 6810 (Average: 83.97 Last: 175) Model-Level : 254.0 Problems : 73 (Average Length: 81.59 Splits: 0) Lemmas : 571824 (Deleted: 534296) Binary : 12927 (Ratio: 2.26%) Ternary : 3312 (Ratio: 0.58%) Conflict : 571824 (Average Length: 507.7 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 571824 (Average: 21.89 Max: 1313 Sum: 12518622) Executed : 571693 (Average: 21.88 Max: 1313 Sum: 12512296 Ratio: 99.95%) Bounded : 131 (Average: 48.29 Max: 112 Sum: 6326 Ratio: 0.05%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 901703 (Eliminated: 0 Frozen: 278344) Constraints : 6630520 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1037MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 7.03s Memory: 973MB (+0MB) UNKNOWN Iteration Time: 7.09s Iteration 73 Queue: [(9,45,4,True), (10,50,4,True), (11,55,3,True), (12,60,3,True), (13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,2,True), (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,1,True), (24,120,0,True)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 74 Time : 602.183s (Solving: 569.35s 1st Model: 0.01s Unsat: 12.29s) CPU Time : 602.280s Choices : 13776933 (Domain: 13533403) Conflicts : 580467 (Analyzed: 580463) Restarts : 6910 (Average: 84.00 Last: 175) Model-Level : 254.0 Problems : 74 (Average Length: 82.07 Splits: 0) Lemmas : 580463 (Deleted: 543005) Binary : 13444 (Ratio: 2.32%) Ternary : 3517 (Ratio: 0.61%) Conflict : 580463 (Average Length: 503.7 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 580463 (Average: 21.82 Max: 1313 Sum: 12662988) Executed : 580332 (Average: 21.80 Max: 1313 Sum: 12656662 Ratio: 99.95%) Bounded : 131 (Average: 48.29 Max: 112 Sum: 6326 Ratio: 0.05%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 901703 (Eliminated: 0 Frozen: 278344) Constraints : 6630520 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1037MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 9.43s Memory: 973MB (+0MB) UNKNOWN Iteration Time: 9.49s Iteration 74 Queue: [(10,50,4,True), (11,55,3,True), (12,60,3,True), (13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,2,True), (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,1,True), (24,120,0,True)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 75 Time : 612.329s (Solving: 579.32s 1st Model: 0.01s Unsat: 12.29s) CPU Time : 612.428s Choices : 13937524 (Domain: 13692561) Conflicts : 589145 (Analyzed: 589141) Restarts : 7010 (Average: 84.04 Last: 175) Model-Level : 254.0 Problems : 75 (Average Length: 82.53 Splits: 0) Lemmas : 589141 (Deleted: 550894) Binary : 13829 (Ratio: 2.35%) Ternary : 3671 (Ratio: 0.62%) Conflict : 589141 (Average Length: 500.4 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 589141 (Average: 21.74 Max: 1313 Sum: 12805704) Executed : 589010 (Average: 21.73 Max: 1313 Sum: 12799378 Ratio: 99.95%) Bounded : 131 (Average: 48.29 Max: 112 Sum: 6326 Ratio: 0.05%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 901703 (Eliminated: 0 Frozen: 278344) Constraints : 6630520 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1037MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 10.09s Memory: 973MB (+0MB) UNKNOWN Iteration Time: 10.15s Iteration 75 Queue: [(11,55,3,True), (12,60,3,True), (13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,2,True), (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,1,True), (24,120,0,True)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 76 Time : 615.550s (Solving: 582.35s 1st Model: 0.01s Unsat: 12.29s) CPU Time : 615.648s Choices : 13983157 (Domain: 13737812) Conflicts : 596233 (Analyzed: 596229) Restarts : 7110 (Average: 83.86 Last: 175) Model-Level : 254.0 Problems : 76 (Average Length: 82.99 Splits: 0) Lemmas : 596229 (Deleted: 557136) Binary : 13869 (Ratio: 2.33%) Ternary : 3677 (Ratio: 0.62%) Conflict : 596229 (Average Length: 497.1 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 596229 (Average: 21.53 Max: 1313 Sum: 12839165) Executed : 596098 (Average: 21.52 Max: 1313 Sum: 12832839 Ratio: 99.95%) Bounded : 131 (Average: 48.29 Max: 112 Sum: 6326 Ratio: 0.05%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 901703 (Eliminated: 0 Frozen: 278344) Constraints : 6630520 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1037MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 3.16s Memory: 973MB (+0MB) UNKNOWN Iteration Time: 3.23s Iteration 76 Queue: [(12,60,3,True), (13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,2,True), (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,1,True), (24,120,0,True)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 77 Time : 624.307s (Solving: 590.89s 1st Model: 0.01s Unsat: 12.29s) CPU Time : 624.408s Choices : 14099868 (Domain: 13854097) Conflicts : 604263 (Analyzed: 604259) Restarts : 7210 (Average: 83.81 Last: 175) Model-Level : 254.0 Problems : 77 (Average Length: 83.43 Splits: 0) Lemmas : 604259 (Deleted: 563960) Binary : 14006 (Ratio: 2.32%) Ternary : 3718 (Ratio: 0.62%) Conflict : 604259 (Average Length: 493.7 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 604259 (Average: 21.42 Max: 1313 Sum: 12941884) Executed : 604128 (Average: 21.41 Max: 1313 Sum: 12935558 Ratio: 99.95%) Bounded : 131 (Average: 48.29 Max: 112 Sum: 6326 Ratio: 0.05%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 901703 (Eliminated: 0 Frozen: 278344) Constraints : 6630520 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1037MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 8.68s Memory: 973MB (+0MB) UNKNOWN Iteration Time: 8.76s Iteration 77 Queue: [(13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,2,True), (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,1,True), (24,120,0,True)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 78 Time : 632.869s (Solving: 599.27s 1st Model: 0.01s Unsat: 12.29s) CPU Time : 632.976s Choices : 14246362 (Domain: 13999342) Conflicts : 612492 (Analyzed: 612488) Restarts : 7310 (Average: 83.79 Last: 175) Model-Level : 254.0 Problems : 78 (Average Length: 83.86 Splits: 0) Lemmas : 612488 (Deleted: 571449) Binary : 14232 (Ratio: 2.32%) Ternary : 3802 (Ratio: 0.62%) Conflict : 612488 (Average Length: 491.0 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 612488 (Average: 21.34 Max: 1313 Sum: 13071729) Executed : 612357 (Average: 21.33 Max: 1313 Sum: 13065403 Ratio: 99.95%) Bounded : 131 (Average: 48.29 Max: 112 Sum: 6326 Ratio: 0.05%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 901703 (Eliminated: 0 Frozen: 278344) Constraints : 6630520 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1037MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 8.50s Memory: 973MB (+0MB) UNKNOWN Iteration Time: 8.57s Iteration 78 Queue: [(16,80,2,True), (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,1,True), (24,120,0,True)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 79 Time : 646.626s (Solving: 612.84s 1st Model: 0.01s Unsat: 12.29s) CPU Time : 646.740s Choices : 14610259 (Domain: 14361153) Conflicts : 621443 (Analyzed: 621439) Restarts : 7410 (Average: 83.86 Last: 175) Model-Level : 254.0 Problems : 79 (Average Length: 84.28 Splits: 0) Lemmas : 621439 (Deleted: 580923) Binary : 14666 (Ratio: 2.36%) Ternary : 3901 (Ratio: 0.63%) Conflict : 621439 (Average Length: 488.2 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 621439 (Average: 21.58 Max: 1313 Sum: 13412106) Executed : 621307 (Average: 21.57 Max: 1313 Sum: 13405668 Ratio: 99.95%) Bounded : 132 (Average: 48.77 Max: 112 Sum: 6438 Ratio: 0.05%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 901703 (Eliminated: 0 Frozen: 278344) Constraints : 6630520 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1037MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 13.70s Memory: 973MB (+0MB) UNKNOWN Iteration Time: 13.76s Iteration 79 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,1,True), (24,120,0,True)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 80 Time : 658.985s (Solving: 625.02s 1st Model: 0.01s Unsat: 12.29s) CPU Time : 659.104s Choices : 14911412 (Domain: 14660787) Conflicts : 630232 (Analyzed: 630228) Restarts : 7510 (Average: 83.92 Last: 175) Model-Level : 254.0 Problems : 80 (Average Length: 84.69 Splits: 0) Lemmas : 630228 (Deleted: 589240) Binary : 14941 (Ratio: 2.37%) Ternary : 3964 (Ratio: 0.63%) Conflict : 630228 (Average Length: 486.1 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 630228 (Average: 21.73 Max: 1313 Sum: 13691843) Executed : 630096 (Average: 21.72 Max: 1313 Sum: 13685405 Ratio: 99.95%) Bounded : 132 (Average: 48.77 Max: 112 Sum: 6438 Ratio: 0.05%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 901703 (Eliminated: 0 Frozen: 278344) Constraints : 6630520 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1037MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 12.31s Memory: 973MB (+0MB) UNKNOWN Iteration Time: 12.37s Iteration 80 Queue: [(18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,1,True), (24,120,0,True)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 81 Time : 670.846s (Solving: 636.71s 1st Model: 0.01s Unsat: 12.29s) CPU Time : 670.972s Choices : 15197297 (Domain: 14945608) Conflicts : 638728 (Analyzed: 638724) Restarts : 7610 (Average: 83.93 Last: 175) Model-Level : 254.0 Problems : 81 (Average Length: 85.09 Splits: 0) Lemmas : 638724 (Deleted: 595481) Binary : 15128 (Ratio: 2.37%) Ternary : 4007 (Ratio: 0.63%) Conflict : 638724 (Average Length: 483.2 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 638724 (Average: 21.85 Max: 1313 Sum: 13955446) Executed : 638592 (Average: 21.84 Max: 1313 Sum: 13949008 Ratio: 99.95%) Bounded : 132 (Average: 48.77 Max: 112 Sum: 6438 Ratio: 0.05%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 901703 (Eliminated: 0 Frozen: 278344) Constraints : 6630520 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1037MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 11.81s Memory: 973MB (+0MB) UNKNOWN Iteration Time: 11.87s Iteration 81 Queue: [(23,115,1,True), (24,120,0,True)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 82 Time : 683.609s (Solving: 649.27s 1st Model: 0.01s Unsat: 12.29s) CPU Time : 683.740s Choices : 15538119 (Domain: 15285849) Conflicts : 646852 (Analyzed: 646848) Restarts : 7710 (Average: 83.90 Last: 175) Model-Level : 254.0 Problems : 82 (Average Length: 85.48 Splits: 0) Lemmas : 646848 (Deleted: 603429) Binary : 15323 (Ratio: 2.37%) Ternary : 4043 (Ratio: 0.63%) Conflict : 646848 (Average Length: 481.1 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 646848 (Average: 22.06 Max: 1313 Sum: 14271484) Executed : 646716 (Average: 22.05 Max: 1313 Sum: 14265046 Ratio: 99.95%) Bounded : 132 (Average: 48.77 Max: 112 Sum: 6438 Ratio: 0.05%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 901703 (Eliminated: 0 Frozen: 278344) Constraints : 6630520 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1037MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 12.69s Memory: 973MB (+0MB) UNKNOWN Iteration Time: 12.77s Iteration 82 Queue: [(24,120,0,True)] Grounded Until: 115 Expected Memory: 1075.0MB Grounding... [('step', [116]), ('step', [117]), ('step', [118]), ('step', [119]), ('step', [120]), ('check', [120])] Grounding Time: 0.57s Memory: 973MB (+0MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 83 Time : 698.253s (Solving: 662.61s 1st Model: 0.01s Unsat: 12.29s) CPU Time : 698.392s Choices : 15771287 (Domain: 15518801) Conflicts : 655429 (Analyzed: 655425) Restarts : 7810 (Average: 83.92 Last: 175) Model-Level : 254.0 Problems : 83 (Average Length: 85.92 Splits: 0) Lemmas : 655425 (Deleted: 611775) Binary : 15369 (Ratio: 2.34%) Ternary : 4053 (Ratio: 0.62%) Conflict : 655425 (Average Length: 488.0 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 655425 (Average: 22.07 Max: 1313 Sum: 14463238) Executed : 655293 (Average: 22.06 Max: 1313 Sum: 14456800 Ratio: 99.96%) Bounded : 132 (Average: 48.77 Max: 112 Sum: 6438 Ratio: 0.04%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 941779 (Eliminated: 0 Frozen: 290794) Constraints : 6932500 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1096MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 13.51s Memory: 995MB (+22MB) UNKNOWN Iteration Time: 14.66s Iteration 83 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,1,True)] Grounded Until: 120 Blocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 84 Time : 703.781s (Solving: 667.94s 1st Model: 0.01s Unsat: 12.29s) CPU Time : 703.924s Choices : 15805574 (Domain: 15553088) Conflicts : 663000 (Analyzed: 662996) Restarts : 7910 (Average: 83.82 Last: 175) Model-Level : 254.0 Problems : 84 (Average Length: 86.35 Splits: 0) Lemmas : 662996 (Deleted: 619824) Binary : 15385 (Ratio: 2.32%) Ternary : 4058 (Ratio: 0.61%) Conflict : 662996 (Average Length: 486.1 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 662996 (Average: 21.86 Max: 1313 Sum: 14489901) Executed : 662864 (Average: 21.85 Max: 1313 Sum: 14483463 Ratio: 99.96%) Bounded : 132 (Average: 48.77 Max: 112 Sum: 6438 Ratio: 0.04%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 941779 (Eliminated: 0 Frozen: 290794) Constraints : 6932500 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1096MB Max. Length : 120 steps Models : 1 [endof: stats after solve call] Solving Time: 5.46s Memory: 995MB (+0MB) UNKNOWN Iteration Time: 5.53s Iteration 84 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,1,True)] Grounded Until: 120 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 85 Time : 710.958s (Solving: 674.94s 1st Model: 0.01s Unsat: 12.29s) CPU Time : 711.108s Choices : 15868523 (Domain: 15616037) Conflicts : 671189 (Analyzed: 671185) Restarts : 8010 (Average: 83.79 Last: 175) Model-Level : 254.0 Problems : 85 (Average Length: 86.76 Splits: 0) Lemmas : 671185 (Deleted: 627106) Binary : 15416 (Ratio: 2.30%) Ternary : 4081 (Ratio: 0.61%) Conflict : 671185 (Average Length: 484.3 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 671185 (Average: 21.67 Max: 1313 Sum: 14542116) Executed : 671052 (Average: 21.66 Max: 1313 Sum: 14535556 Ratio: 99.95%) Bounded : 133 (Average: 49.32 Max: 122 Sum: 6560 Ratio: 0.05%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 941779 (Eliminated: 0 Frozen: 290794) Constraints : 6932500 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1096MB Max. Length : 120 steps Models : 1 [endof: stats after solve call] Solving Time: 7.12s Memory: 995MB (+0MB) UNKNOWN Iteration Time: 7.19s Iteration 85 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,1,True)] Grounded Until: 120 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 86 Time : 720.193s (Solving: 683.94s 1st Model: 0.01s Unsat: 12.29s) CPU Time : 720.348s Choices : 15998224 (Domain: 15745738) Conflicts : 679540 (Analyzed: 679536) Restarts : 8110 (Average: 83.79 Last: 175) Model-Level : 254.0 Problems : 86 (Average Length: 87.17 Splits: 0) Lemmas : 679536 (Deleted: 634806) Binary : 15514 (Ratio: 2.28%) Ternary : 4107 (Ratio: 0.60%) Conflict : 679536 (Average Length: 482.4 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 679536 (Average: 21.57 Max: 1313 Sum: 14659332) Executed : 679403 (Average: 21.56 Max: 1313 Sum: 14652772 Ratio: 99.96%) Bounded : 133 (Average: 49.32 Max: 122 Sum: 6560 Ratio: 0.04%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 941779 (Eliminated: 0 Frozen: 290794) Constraints : 6932486 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1096MB Max. Length : 120 steps Models : 1 [endof: stats after solve call] Solving Time: 9.15s Memory: 995MB (+0MB) UNKNOWN Iteration Time: 9.24s Iteration 86 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,1,True)] Grounded Until: 120 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 87 Time : 727.501s (Solving: 691.05s 1st Model: 0.01s Unsat: 12.29s) CPU Time : 727.660s Choices : 16054400 (Domain: 15801914) Conflicts : 687311 (Analyzed: 687307) Restarts : 8210 (Average: 83.72 Last: 175) Model-Level : 254.0 Problems : 87 (Average Length: 87.57 Splits: 0) Lemmas : 687307 (Deleted: 642710) Binary : 15594 (Ratio: 2.27%) Ternary : 4132 (Ratio: 0.60%) Conflict : 687307 (Average Length: 480.8 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 687307 (Average: 21.40 Max: 1313 Sum: 14706257) Executed : 687171 (Average: 21.39 Max: 1313 Sum: 14699336 Ratio: 99.95%) Bounded : 136 (Average: 50.89 Max: 122 Sum: 6921 Ratio: 0.05%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 941779 (Eliminated: 0 Frozen: 290794) Constraints : 6932486 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1096MB Max. Length : 120 steps Models : 1 [endof: stats after solve call] Solving Time: 7.24s Memory: 995MB (+0MB) UNKNOWN Iteration Time: 7.31s Iteration 87 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,1,True)] Grounded Until: 120 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 88 Time : 734.932s (Solving: 698.28s 1st Model: 0.01s Unsat: 12.29s) CPU Time : 735.096s Choices : 16165621 (Domain: 15911533) Conflicts : 695340 (Analyzed: 695336) Restarts : 8310 (Average: 83.67 Last: 175) Model-Level : 254.0 Problems : 88 (Average Length: 87.97 Splits: 0) Lemmas : 695336 (Deleted: 650072) Binary : 15737 (Ratio: 2.26%) Ternary : 4154 (Ratio: 0.60%) Conflict : 695336 (Average Length: 478.6 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 695336 (Average: 21.29 Max: 1313 Sum: 14803973) Executed : 695200 (Average: 21.28 Max: 1313 Sum: 14797052 Ratio: 99.95%) Bounded : 136 (Average: 50.89 Max: 122 Sum: 6921 Ratio: 0.05%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 941779 (Eliminated: 0 Frozen: 290794) Constraints : 6932449 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1096MB Max. Length : 120 steps Models : 1 [endof: stats after solve call] Solving Time: 7.37s Memory: 995MB (+0MB) UNKNOWN Iteration Time: 7.44s Iteration 88 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,1,True)] Grounded Until: 120 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 89 Time : 747.379s (Solving: 710.54s 1st Model: 0.01s Unsat: 12.29s) CPU Time : 747.548s Choices : 16364648 (Domain: 16109060) Conflicts : 703984 (Analyzed: 703980) Restarts : 8410 (Average: 83.71 Last: 175) Model-Level : 254.0 Problems : 89 (Average Length: 88.35 Splits: 0) Lemmas : 703980 (Deleted: 659522) Binary : 16043 (Ratio: 2.28%) Ternary : 4195 (Ratio: 0.60%) Conflict : 703980 (Average Length: 476.7 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 703980 (Average: 21.29 Max: 1313 Sum: 14984301) Executed : 703844 (Average: 21.28 Max: 1313 Sum: 14977380 Ratio: 99.95%) Bounded : 136 (Average: 50.89 Max: 122 Sum: 6921 Ratio: 0.05%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 941779 (Eliminated: 0 Frozen: 290794) Constraints : 6932449 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1096MB Max. Length : 120 steps Models : 1 [endof: stats after solve call] Solving Time: 12.39s Memory: 995MB (+0MB) UNKNOWN Iteration Time: 12.45s Iteration 89 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,1,True)] Grounded Until: 120 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 90 Time : 758.875s (Solving: 721.84s 1st Model: 0.01s Unsat: 12.29s) CPU Time : 759.048s Choices : 16580047 (Domain: 16322792) Conflicts : 712296 (Analyzed: 712292) Restarts : 8510 (Average: 83.70 Last: 175) Model-Level : 254.0 Problems : 90 (Average Length: 88.72 Splits: 0) Lemmas : 712292 (Deleted: 665591) Binary : 16346 (Ratio: 2.29%) Ternary : 4260 (Ratio: 0.60%) Conflict : 712292 (Average Length: 474.8 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 712292 (Average: 21.31 Max: 1313 Sum: 15177233) Executed : 712156 (Average: 21.30 Max: 1313 Sum: 15170312 Ratio: 99.95%) Bounded : 136 (Average: 50.89 Max: 122 Sum: 6921 Ratio: 0.05%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 941779 (Eliminated: 0 Frozen: 290794) Constraints : 6932449 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1096MB Max. Length : 120 steps Models : 1 [endof: stats after solve call] Solving Time: 11.43s Memory: 995MB (+0MB) UNKNOWN Iteration Time: 11.50s Iteration 90 Queue: [(19,95,2,True), (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 : 91 Time : 773.112s (Solving: 735.88s 1st Model: 0.01s Unsat: 12.29s) CPU Time : 773.292s Choices : 16853495 (Domain: 16595624) Conflicts : 720916 (Analyzed: 720912) Restarts : 8610 (Average: 83.73 Last: 175) Model-Level : 254.0 Problems : 91 (Average Length: 89.09 Splits: 0) Lemmas : 720912 (Deleted: 675097) Binary : 16661 (Ratio: 2.31%) Ternary : 4309 (Ratio: 0.60%) Conflict : 720912 (Average Length: 473.4 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 720912 (Average: 21.40 Max: 1313 Sum: 15425534) Executed : 720775 (Average: 21.39 Max: 1313 Sum: 15418491 Ratio: 99.95%) Bounded : 137 (Average: 51.41 Max: 122 Sum: 7043 Ratio: 0.05%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 941779 (Eliminated: 0 Frozen: 290794) Constraints : 6932449 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1096MB Max. Length : 120 steps Models : 1 [endof: stats after solve call] Solving Time: 14.17s Memory: 995MB (+0MB) UNKNOWN Iteration Time: 14.25s Iteration 91 Queue: [(24,120,1,True)] Grounded Until: 120 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 92 Time : 788.163s (Solving: 750.74s 1st Model: 0.01s Unsat: 12.29s) CPU Time : 788.348s Choices : 17177392 (Domain: 16919325) Conflicts : 729150 (Analyzed: 729146) Restarts : 8710 (Average: 83.71 Last: 175) Model-Level : 254.0 Problems : 92 (Average Length: 89.45 Splits: 0) Lemmas : 729146 (Deleted: 681441) Binary : 16992 (Ratio: 2.33%) Ternary : 4349 (Ratio: 0.60%) Conflict : 729146 (Average Length: 472.6 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 729146 (Average: 21.56 Max: 1456 Sum: 15718597) Executed : 729009 (Average: 21.55 Max: 1456 Sum: 15711554 Ratio: 99.96%) Bounded : 137 (Average: 51.41 Max: 122 Sum: 7043 Ratio: 0.04%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 941779 (Eliminated: 0 Frozen: 290794) Constraints : 6932435 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1096MB Max. Length : 120 steps Models : 1 [endof: stats after solve call] Solving Time: 15.00s Memory: 995MB (+0MB) UNKNOWN Iteration Time: 15.06s Iteration 92 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 : 93 Time : 792.979s (Solving: 755.37s 1st Model: 0.01s Unsat: 12.29s) CPU Time : 793.168s Choices : 17213665 (Domain: 16955598) Conflicts : 736679 (Analyzed: 736675) Restarts : 8810 (Average: 83.62 Last: 175) Model-Level : 254.0 Problems : 93 (Average Length: 89.80 Splits: 0) Lemmas : 736675 (Deleted: 689255) Binary : 17005 (Ratio: 2.31%) Ternary : 4352 (Ratio: 0.59%) Conflict : 736675 (Average Length: 471.1 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 736675 (Average: 21.38 Max: 1456 Sum: 15746780) Executed : 736538 (Average: 21.37 Max: 1456 Sum: 15739737 Ratio: 99.96%) Bounded : 137 (Average: 51.41 Max: 122 Sum: 7043 Ratio: 0.04%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 941779 (Eliminated: 0 Frozen: 290794) Constraints : 6932435 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1096MB Max. Length : 120 steps Models : 1 [endof: stats after solve call] Solving Time: 4.75s Memory: 995MB (+0MB) UNKNOWN Iteration Time: 4.82s Iteration 93 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 : 94 Time : 802.882s (Solving: 765.08s 1st Model: 0.01s Unsat: 12.29s) CPU Time : 803.072s Choices : 17285111 (Domain: 17027044) Conflicts : 745231 (Analyzed: 745227) Restarts : 8910 (Average: 83.64 Last: 175) Model-Level : 254.0 Problems : 94 (Average Length: 90.14 Splits: 0) Lemmas : 745227 (Deleted: 696548) Binary : 17143 (Ratio: 2.30%) Ternary : 4371 (Ratio: 0.59%) Conflict : 745227 (Average Length: 474.2 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 745227 (Average: 21.21 Max: 1456 Sum: 15803740) Executed : 745089 (Average: 21.20 Max: 1456 Sum: 15796575 Ratio: 99.95%) Bounded : 138 (Average: 51.92 Max: 122 Sum: 7165 Ratio: 0.05%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 941779 (Eliminated: 0 Frozen: 290794) Constraints : 6932435 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1096MB Max. Length : 120 steps Models : 1 [endof: stats after solve call] Solving Time: 9.85s Memory: 995MB (+0MB) UNKNOWN Iteration Time: 9.91s Iteration 94 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 : 95 Time : 808.597s (Solving: 770.57s 1st Model: 0.01s Unsat: 12.29s) CPU Time : 808.792s Choices : 17325774 (Domain: 17067707) Conflicts : 753155 (Analyzed: 753151) Restarts : 9010 (Average: 83.59 Last: 175) Model-Level : 254.0 Problems : 95 (Average Length: 90.47 Splits: 0) Lemmas : 753151 (Deleted: 704737) Binary : 17170 (Ratio: 2.28%) Ternary : 4377 (Ratio: 0.58%) Conflict : 753151 (Average Length: 472.4 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 753151 (Average: 21.03 Max: 1456 Sum: 15836845) Executed : 753009 (Average: 21.02 Max: 1456 Sum: 15829197 Ratio: 99.95%) Bounded : 142 (Average: 53.86 Max: 122 Sum: 7648 Ratio: 0.05%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 941779 (Eliminated: 0 Frozen: 290794) Constraints : 6932421 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1096MB Max. Length : 120 steps Models : 1 [endof: stats after solve call] Solving Time: 5.63s Memory: 995MB (+0MB) UNKNOWN Iteration Time: 5.72s Iteration 95 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 : 96 Time : 814.108s (Solving: 775.88s 1st Model: 0.01s Unsat: 12.29s) CPU Time : 814.304s Choices : 17392914 (Domain: 17134799) Conflicts : 760999 (Analyzed: 760995) Restarts : 9110 (Average: 83.53 Last: 175) Model-Level : 254.0 Problems : 96 (Average Length: 90.80 Splits: 0) Lemmas : 760995 (Deleted: 712312) Binary : 17224 (Ratio: 2.26%) Ternary : 4386 (Ratio: 0.58%) Conflict : 760995 (Average Length: 470.6 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 760995 (Average: 20.89 Max: 1456 Sum: 15893771) Executed : 760853 (Average: 20.88 Max: 1456 Sum: 15886123 Ratio: 99.95%) Bounded : 142 (Average: 53.86 Max: 122 Sum: 7648 Ratio: 0.05%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 941779 (Eliminated: 0 Frozen: 290794) Constraints : 6932379 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1096MB Max. Length : 120 steps Models : 1 [endof: stats after solve call] Solving Time: 5.44s Memory: 995MB (+0MB) UNKNOWN Iteration Time: 5.52s Iteration 96 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 : 97 Time : 825.024s (Solving: 786.61s 1st Model: 0.01s Unsat: 12.29s) CPU Time : 825.224s Choices : 17539391 (Domain: 17280896) Conflicts : 769512 (Analyzed: 769508) Restarts : 9210 (Average: 83.55 Last: 175) Model-Level : 254.0 Problems : 97 (Average Length: 91.12 Splits: 0) Lemmas : 769508 (Deleted: 719799) Binary : 17400 (Ratio: 2.26%) Ternary : 4417 (Ratio: 0.57%) Conflict : 769508 (Average Length: 469.3 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 769508 (Average: 20.82 Max: 1456 Sum: 16023834) Executed : 769366 (Average: 20.81 Max: 1456 Sum: 16016186 Ratio: 99.95%) Bounded : 142 (Average: 53.86 Max: 122 Sum: 7648 Ratio: 0.05%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 941779 (Eliminated: 0 Frozen: 290794) Constraints : 6932379 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1096MB Max. Length : 120 steps Models : 1 [endof: stats after solve call] Solving Time: 10.85s Memory: 995MB (+0MB) UNKNOWN Iteration Time: 10.92s Iteration 97 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 : 98 Time : 836.489s (Solving: 797.87s 1st Model: 0.01s Unsat: 12.29s) CPU Time : 836.692s Choices : 17691327 (Domain: 17431589) Conflicts : 778275 (Analyzed: 778271) Restarts : 9310 (Average: 83.60 Last: 191) Model-Level : 254.0 Problems : 98 (Average Length: 91.44 Splits: 0) Lemmas : 778271 (Deleted: 729623) Binary : 17589 (Ratio: 2.26%) Ternary : 4447 (Ratio: 0.57%) Conflict : 778271 (Average Length: 469.4 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 778271 (Average: 20.76 Max: 1456 Sum: 16157004) Executed : 778128 (Average: 20.75 Max: 1456 Sum: 16149234 Ratio: 99.95%) Bounded : 143 (Average: 54.34 Max: 122 Sum: 7770 Ratio: 0.05%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 941779 (Eliminated: 0 Frozen: 290794) Constraints : 6932379 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1096MB Max. Length : 120 steps Models : 1 [endof: stats after solve call] Solving Time: 11.40s Memory: 995MB (+0MB) UNKNOWN Iteration Time: 11.47s Iteration 98 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 : 99 Time : 845.821s (Solving: 807.01s 1st Model: 0.01s Unsat: 12.29s) CPU Time : 846.028s Choices : 17782307 (Domain: 17522479) Conflicts : 786276 (Analyzed: 786272) Restarts : 9410 (Average: 83.56 Last: 191) Model-Level : 254.0 Problems : 99 (Average Length: 91.75 Splits: 0) Lemmas : 786272 (Deleted: 736243) Binary : 17666 (Ratio: 2.25%) Ternary : 4462 (Ratio: 0.57%) Conflict : 786272 (Average Length: 469.3 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 786272 (Average: 20.64 Max: 1456 Sum: 16231550) Executed : 786129 (Average: 20.63 Max: 1456 Sum: 16223780 Ratio: 99.95%) Bounded : 143 (Average: 54.34 Max: 122 Sum: 7770 Ratio: 0.05%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 941779 (Eliminated: 0 Frozen: 290794) Constraints : 6932366 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1096MB Max. Length : 120 steps Models : 1 [endof: stats after solve call] Solving Time: 9.27s Memory: 995MB (+0MB) UNKNOWN Iteration Time: 9.34s Iteration 99 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 : 100 Time : 856.441s (Solving: 817.44s 1st Model: 0.01s Unsat: 12.29s) CPU Time : 856.652s Choices : 17955240 (Domain: 17695244) Conflicts : 794744 (Analyzed: 794740) Restarts : 9510 (Average: 83.57 Last: 191) Model-Level : 254.0 Problems : 100 (Average Length: 92.05 Splits: 0) Lemmas : 794740 (Deleted: 744000) Binary : 17814 (Ratio: 2.24%) Ternary : 4493 (Ratio: 0.57%) Conflict : 794740 (Average Length: 469.5 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 794740 (Average: 20.62 Max: 1456 Sum: 16385032) Executed : 794597 (Average: 20.61 Max: 1456 Sum: 16377262 Ratio: 99.95%) Bounded : 143 (Average: 54.34 Max: 122 Sum: 7770 Ratio: 0.05%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 941779 (Eliminated: 0 Frozen: 290794) Constraints : 6932366 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1096MB Max. Length : 120 steps Models : 1 [endof: stats after solve call] Solving Time: 10.56s Memory: 995MB (+0MB) UNKNOWN Iteration Time: 10.63s Iteration 100 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 : 101 Time : 865.659s (Solving: 826.47s 1st Model: 0.01s Unsat: 12.29s) CPU Time : 865.876s Choices : 18127019 (Domain: 17866821) Conflicts : 803129 (Analyzed: 803125) Restarts : 9610 (Average: 83.57 Last: 191) Model-Level : 254.0 Problems : 101 (Average Length: 92.35 Splits: 0) Lemmas : 803125 (Deleted: 751967) Binary : 17915 (Ratio: 2.23%) Ternary : 4518 (Ratio: 0.56%) Conflict : 803125 (Average Length: 469.2 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 803125 (Average: 20.59 Max: 1456 Sum: 16535251) Executed : 802982 (Average: 20.58 Max: 1456 Sum: 16527481 Ratio: 99.95%) Bounded : 143 (Average: 54.34 Max: 122 Sum: 7770 Ratio: 0.05%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 941779 (Eliminated: 0 Frozen: 290794) Constraints : 6932366 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1096MB Max. Length : 120 steps Models : 1 [endof: stats after solve call] Solving Time: 9.16s Memory: 995MB (+0MB) UNKNOWN Iteration Time: 9.22s Iteration 101 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 : 102 Time : 871.761s (Solving: 832.37s 1st Model: 0.01s Unsat: 12.29s) CPU Time : 871.980s Choices : 18163656 (Domain: 17903458) Conflicts : 810860 (Analyzed: 810856) Restarts : 9710 (Average: 83.51 Last: 191) Model-Level : 254.0 Problems : 102 (Average Length: 92.64 Splits: 0) Lemmas : 810856 (Deleted: 760191) Binary : 17945 (Ratio: 2.21%) Ternary : 4524 (Ratio: 0.56%) Conflict : 810856 (Average Length: 468.5 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 810856 (Average: 20.43 Max: 1456 Sum: 16563240) Executed : 810713 (Average: 20.42 Max: 1456 Sum: 16555470 Ratio: 99.95%) Bounded : 143 (Average: 54.34 Max: 122 Sum: 7770 Ratio: 0.05%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 941779 (Eliminated: 0 Frozen: 290794) Constraints : 6932366 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1096MB Max. Length : 120 steps Models : 1 [endof: stats after solve call] Solving Time: 6.03s Memory: 995MB (+0MB) UNKNOWN Iteration Time: 6.11s Iteration 102 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 : 103 Time : 887.554s (Solving: 847.97s 1st Model: 0.01s Unsat: 12.29s) CPU Time : 887.776s Choices : 18241294 (Domain: 17981096) Conflicts : 819330 (Analyzed: 819326) Restarts : 9810 (Average: 83.52 Last: 191) Model-Level : 254.0 Problems : 103 (Average Length: 92.92 Splits: 0) Lemmas : 819326 (Deleted: 767691) Binary : 17983 (Ratio: 2.19%) Ternary : 4533 (Ratio: 0.55%) Conflict : 819326 (Average Length: 481.0 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 819326 (Average: 20.29 Max: 1456 Sum: 16625112) Executed : 819183 (Average: 20.28 Max: 1456 Sum: 16617342 Ratio: 99.95%) Bounded : 143 (Average: 54.34 Max: 122 Sum: 7770 Ratio: 0.05%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 941779 (Eliminated: 0 Frozen: 290794) Constraints : 6932366 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1096MB Max. Length : 120 steps Models : 1 [endof: stats after solve call] Solving Time: 15.74s Memory: 995MB (+0MB) UNKNOWN Iteration Time: 15.80s Iteration 103 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... *** Info : (planner): INTERRUPTED by signal! UNKNOWN INTERRUPTED : 1 Models : 0+ Calls : 104 Time : 892.536s (Solving: 852.76s 1st Model: 0.01s Unsat: 12.29s) CPU Time : 892.740s Choices : 18282206 (Domain: 18022008) Conflicts : 825524 (Analyzed: 825520) Restarts : 9894 (Average: 83.44 Last: 191) Model-Level : 254.0 Problems : 104 (Average Length: 93.20 Splits: 0) Lemmas : 825520 (Deleted: 772098) Binary : 17989 (Ratio: 2.18%) Ternary : 4538 (Ratio: 0.55%) Conflict : 825520 (Average Length: 480.0 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 825520 (Average: 20.18 Max: 1456 Sum: 16658548) Executed : 825377 (Average: 20.17 Max: 1456 Sum: 16650778 Ratio: 99.95%) Bounded : 143 (Average: 54.34 Max: 122 Sum: 7770 Ratio: 0.05%) Rules : 160595 (Original: 145100) Atoms : 77287 Bodies : 70054 (Original: 54558) Count : 890 (Original: 2504) Equivalences : 16810 (Atom=Atom: 87 Body=Body: 0 Other: 16723) Tight : Yes Variables : 941779 (Eliminated: 0 Frozen: 290794) Constraints : 6932366 (Binary: 91.2% Ternary: 7.0% Other: 1.8%) Memory Peak : 1096MB Max. Length : 120 steps Models : 1