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-11.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-11.pddl Parsing... Parsing: [0.040s CPU, 0.045s wall-clock] Normalizing task... [0.000s CPU, 0.003s wall-clock] Instantiating... Generating Datalog program... [0.010s CPU, 0.012s wall-clock] Normalizing Datalog program... Normalizing Datalog program: [0.060s CPU, 0.054s wall-clock] Preparing model... [0.030s CPU, 0.029s wall-clock] Generated 115 rules. Computing model... [0.450s CPU, 0.456s wall-clock] 2784 relevant atoms 2893 auxiliary atoms 5677 final queue length 9793 total queue pushes Completing instantiation... [0.880s CPU, 0.871s wall-clock] Instantiating: [1.430s CPU, 1.428s wall-clock] Computing fact groups... Finding invariants... 24 initial candidates Finding invariants: [0.120s CPU, 0.113s wall-clock] Checking invariant weight... [0.000s CPU, 0.001s wall-clock] Instantiating groups... [0.000s CPU, 0.008s wall-clock] Collecting mutex groups... [0.000s CPU, 0.001s wall-clock] Choosing groups... 292 uncovered facts Choosing groups: [0.010s CPU, 0.002s wall-clock] Building translation key... [0.010s CPU, 0.011s wall-clock] Computing fact groups: [0.160s CPU, 0.157s wall-clock] Building STRIPS to SAS dictionary... [0.000s CPU, 0.002s wall-clock] Building dictionary for full mutex groups... [0.010s CPU, 0.005s wall-clock] Building mutex information... Building mutex information: [0.000s CPU, 0.003s wall-clock] Translating task... Processing axioms... Simplifying axioms... [0.000s CPU, 0.000s wall-clock] Processing axioms: [0.050s CPU, 0.050s wall-clock] Translating task: [0.890s CPU, 0.899s wall-clock] 3276 effect conditions simplified 0 implied preconditions added Detecting unreachable propositions... 0 operators removed 0 axioms removed 3 propositions removed Detecting unreachable propositions: [0.450s CPU, 0.436s wall-clock] Reordering and filtering variables... 295 of 295 variables necessary. 14 of 17 mutex groups necessary. 1958 of 1958 operators necessary. 0 of 0 axiom rules necessary. Reordering and filtering variables: [0.300s CPU, 0.304s wall-clock] Translator variables: 295 Translator derived variables: 0 Translator facts: 617 Translator goal facts: 12 Translator mutex groups: 14 Translator total mutex groups size: 42 Translator operators: 1958 Translator axioms: 0 Translator task size: 18764 Translator peak memory: 47052 KB Writing output... [0.330s CPU, 0.365s wall-clock] Done! [3.650s CPU, 3.686s wall-clock] planner.py version 0.0.1 Time: 0.76s Memory: 101MB Iteration 1 Queue: [(0,0,0,True), (1,5,0,True), (2,10,0,True), (3,15,0,True), (4,20,0,True), (5,25,0,True), (6,30,0,True)] Grounded Until: 0 Solving... [start: stats after solve call] Models : 0 Calls : 1 Time : 0.905s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s) CPU Time : 0.764s 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 : 54149 Atoms : 54149 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 : 237MB Max. Length : 0 steps Models : 0 [endof: stats after solve call] Solving Time: 0.01s Memory: 173MB (+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: 173MB Grounding... [('step', [1]), ('step', [2]), ('step', [3]), ('step', [4]), ('step', [5]), ('check', [5])] Grounding Time: 0.23s Memory: 173MB (+0MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0 Calls : 2 Time : 1.259s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s) CPU Time : 1.120s Choices : 103 (Domain: 92) Conflicts : 33 (Analyzed: 32) Restarts : 0 Problems : 2 (Average Length: 4.50 Splits: 0) Lemmas : 32 (Deleted: 0) Binary : 8 (Ratio: 25.00%) Ternary : 2 (Ratio: 6.25%) Conflict : 32 (Average Length: 7.2 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 32 (Average: 3.28 Max: 24 Sum: 105) Executed : 30 (Average: 3.22 Max: 24 Sum: 103 Ratio: 98.10%) Bounded : 2 (Average: 1.00 Max: 1 Sum: 2 Ratio: 1.90%) Rules : 54149 Atoms : 54149 Bodies : 1 (Original: 0) Tight : Yes Variables : 14506 (Eliminated: 0 Frozen: 150) Constraints : 48947 (Binary: 95.2% Ternary: 3.3% Other: 1.4%) Memory Peak : 237MB Max. Length : 0 steps Models : 0 [endof: stats after solve call] Solving Time: 0.02s Memory: 176MB (+3MB) UNSAT Iteration Time: 0.36s 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: 179.0MB Grounding... [('step', [6]), ('step', [7]), ('step', [8]), ('step', [9]), ('step', [10]), ('check', [10])] Grounding Time: 0.28s Memory: 183MB (+7MB) Unblocking actions... Solving... [start: stats after solve call] Models : 1+ Calls : 3 Time : 1.686s (Solving: 0.02s 1st Model: 0.02s Unsat: 0.00s) CPU Time : 1.548s Choices : 2635 (Domain: 2541) Conflicts : 143 (Analyzed: 142) Restarts : 1 (Average: 142.00 Last: 40) Model-Level : 299.0 Problems : 3 (Average Length: 7.00 Splits: 0) Lemmas : 142 (Deleted: 0) Binary : 39 (Ratio: 27.46%) Ternary : 20 (Ratio: 14.08%) Conflict : 142 (Average Length: 17.1 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 142 (Average: 16.46 Max: 111 Sum: 2337) Executed : 140 (Average: 16.44 Max: 111 Sum: 2335 Ratio: 99.91%) Bounded : 2 (Average: 1.00 Max: 1 Sum: 2 Ratio: 0.09%) Rules : 54149 Atoms : 54149 Bodies : 1 (Original: 0) Tight : Yes Variables : 31792 (Eliminated: 0 Frozen: 300) Constraints : 190267 (Binary: 95.6% Ternary: 3.2% Other: 1.2%) Memory Peak : 237MB Max. Length : 5 steps Models : 1 [endof: stats after solve call] Solving Time: 0.04s Memory: 190MB (+7MB) SAT Testing... NOT SERIALIZABLE Testing Time: 0.89s Memory: 221MB (+31MB) Solving... [start: stats after solve call] Models : 0 Calls : 4 Time : 3.157s (Solving: 1.20s 1st Model: 0.02s Unsat: 1.19s) CPU Time : 3.016s Choices : 26662 (Domain: 21394) Conflicts : 3367 (Analyzed: 3365) Restarts : 38 (Average: 88.55 Last: 40) Model-Level : 299.0 Problems : 4 (Average Length: 8.25 Splits: 0) Lemmas : 3365 (Deleted: 818) Binary : 485 (Ratio: 14.41%) Ternary : 254 (Ratio: 7.55%) Conflict : 3365 (Average Length: 67.2 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 3365 (Average: 7.70 Max: 165 Sum: 25896) Executed : 3348 (Average: 7.65 Max: 165 Sum: 25736 Ratio: 99.38%) Bounded : 17 (Average: 9.41 Max: 12 Sum: 160 Ratio: 0.62%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 49760 (Eliminated: 0 Frozen: 14250) Constraints : 309236 (Binary: 91.5% Ternary: 6.8% Other: 1.7%) Memory Peak : 237MB Max. Length : 5 steps Models : 1 [endof: stats after solve call] Solving Time: 1.25s Memory: 221MB (+0MB) UNSAT Iteration Time: 2.58s Iteration 4 Queue: [(3,15,0,True), (4,20,0,True), (5,25,0,True), (6,30,0,True)] Grounded Until: 10 Expected Memory: 235.0MB Grounding... [('step', [11]), ('step', [12]), ('step', [13]), ('step', [14]), ('step', [15]), ('check', [15])] Grounding Time: 0.44s Memory: 221MB (+0MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 5 Time : 8.055s (Solving: 5.45s 1st Model: 0.02s Unsat: 1.19s) CPU Time : 7.916s Choices : 90003 (Domain: 64271) Conflicts : 12580 (Analyzed: 12578) Restarts : 138 (Average: 91.14 Last: 111) Model-Level : 299.0 Problems : 5 (Average Length: 10.00 Splits: 0) Lemmas : 12578 (Deleted: 7802) Binary : 943 (Ratio: 7.50%) Ternary : 390 (Ratio: 3.10%) Conflict : 12578 (Average Length: 373.8 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 12578 (Average: 6.82 Max: 200 Sum: 85750) Executed : 12559 (Average: 6.80 Max: 200 Sum: 85556 Ratio: 99.77%) Bounded : 19 (Average: 10.21 Max: 17 Sum: 194 Ratio: 0.23%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 82706 (Eliminated: 0 Frozen: 24685) Constraints : 541641 (Binary: 91.5% Ternary: 6.8% Other: 1.8%) Memory Peak : 243MB Max. Length : 10 steps Models : 1 [endof: stats after solve call] Solving Time: 4.28s Memory: 243MB (+22MB) UNKNOWN Iteration Time: 4.91s Iteration 5 Queue: [(4,20,0,True), (5,25,0,True), (6,30,0,True)] Grounded Until: 15 Expected Memory: 265.0MB Grounding... [('step', [16]), ('step', [17]), ('step', [18]), ('step', [19]), ('step', [20]), ('check', [20])] Grounding Time: 0.49s Memory: 246MB (+3MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 6 Time : 13.500s (Solving: 10.18s 1st Model: 0.02s Unsat: 1.19s) CPU Time : 13.364s Choices : 191030 (Domain: 149283) Conflicts : 21635 (Analyzed: 21633) Restarts : 238 (Average: 90.89 Last: 111) Model-Level : 299.0 Problems : 6 (Average Length: 12.00 Splits: 0) Lemmas : 21633 (Deleted: 16153) Binary : 1465 (Ratio: 6.77%) Ternary : 574 (Ratio: 2.65%) Conflict : 21633 (Average Length: 522.2 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 21633 (Average: 8.26 Max: 412 Sum: 178677) Executed : 21614 (Average: 8.25 Max: 412 Sum: 178483 Ratio: 99.89%) Bounded : 19 (Average: 10.21 Max: 17 Sum: 194 Ratio: 0.11%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 115652 (Eliminated: 0 Frozen: 35120) Constraints : 791175 (Binary: 91.4% Ternary: 6.8% Other: 1.8%) Memory Peak : 263MB Max. Length : 15 steps Models : 1 [endof: stats after solve call] Solving Time: 4.76s Memory: 260MB (+14MB) UNKNOWN Iteration Time: 5.46s Iteration 6 Queue: [(5,25,0,True), (6,30,0,True)] Grounded Until: 20 Expected Memory: 282.0MB Grounding... [('step', [21]), ('step', [22]), ('step', [23]), ('step', [24]), ('step', [25]), ('check', [25])] Grounding Time: 0.58s Memory: 276MB (+16MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 7 Time : 19.981s (Solving: 15.82s 1st Model: 0.02s Unsat: 1.19s) CPU Time : 19.848s Choices : 316908 (Domain: 263664) Conflicts : 30373 (Analyzed: 30371) Restarts : 338 (Average: 89.86 Last: 111) Model-Level : 299.0 Problems : 7 (Average Length: 14.14 Splits: 0) Lemmas : 30371 (Deleted: 24159) Binary : 2093 (Ratio: 6.89%) Ternary : 758 (Ratio: 2.50%) Conflict : 30371 (Average Length: 555.9 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 30371 (Average: 9.66 Max: 412 Sum: 293253) Executed : 30352 (Average: 9.65 Max: 412 Sum: 293059 Ratio: 99.93%) Bounded : 19 (Average: 10.21 Max: 17 Sum: 194 Ratio: 0.07%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 148598 (Eliminated: 0 Frozen: 45555) Constraints : 1040760 (Binary: 91.4% Ternary: 6.8% Other: 1.8%) Memory Peak : 299MB Max. Length : 20 steps Models : 1 [endof: stats after solve call] Solving Time: 5.70s Memory: 287MB (+11MB) UNKNOWN Iteration Time: 6.49s Iteration 7 Queue: [(6,30,0,True)] Grounded Until: 25 Expected Memory: 314.0MB Grounding... [('step', [26]), ('step', [27]), ('step', [28]), ('step', [29]), ('step', [30]), ('check', [30])] Grounding Time: 0.48s Memory: 299MB (+12MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 8 Time : 27.706s (Solving: 22.79s 1st Model: 0.02s Unsat: 1.19s) CPU Time : 27.576s Choices : 453124 (Domain: 387459) Conflicts : 39030 (Analyzed: 39028) Restarts : 438 (Average: 89.11 Last: 111) Model-Level : 299.0 Problems : 8 (Average Length: 16.38 Splits: 0) Lemmas : 39028 (Deleted: 32222) Binary : 2443 (Ratio: 6.26%) Ternary : 820 (Ratio: 2.10%) Conflict : 39028 (Average Length: 628.8 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 39028 (Average: 10.63 Max: 412 Sum: 414827) Executed : 39009 (Average: 10.62 Max: 412 Sum: 414633 Ratio: 99.95%) Bounded : 19 (Average: 10.21 Max: 17 Sum: 194 Ratio: 0.05%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 181544 (Eliminated: 0 Frozen: 55990) Constraints : 1290345 (Binary: 91.4% Ternary: 6.8% Other: 1.8%) Memory Peak : 326MB Max. Length : 25 steps Models : 1 [endof: stats after solve call] Solving Time: 7.02s Memory: 323MB (+24MB) UNKNOWN Iteration Time: 7.74s 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 : 31.484s (Solving: 26.53s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 31.356s Choices : 499735 (Domain: 425015) Conflicts : 45758 (Analyzed: 45755) Restarts : 508 (Average: 90.07 Last: 111) Model-Level : 299.0 Problems : 9 (Average Length: 18.11 Splits: 0) Lemmas : 45755 (Deleted: 37915) Binary : 2831 (Ratio: 6.19%) Ternary : 925 (Ratio: 2.02%) Conflict : 45755 (Average Length: 562.4 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 45755 (Average: 10.06 Max: 412 Sum: 460107) Executed : 45724 (Average: 10.05 Max: 412 Sum: 459627 Ratio: 99.90%) Bounded : 31 (Average: 15.48 Max: 32 Sum: 480 Ratio: 0.10%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 181544 (Eliminated: 0 Frozen: 55990) Constraints : 1290345 (Binary: 91.4% Ternary: 6.8% Other: 1.8%) Memory Peak : 326MB Max. Length : 30 steps Models : 1 [endof: stats after solve call] Solving Time: 3.77s Memory: 323MB (+0MB) UNSAT Iteration Time: 3.78s 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 : 38.291s (Solving: 33.29s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 38.168s Choices : 641393 (Domain: 555999) Conflicts : 54969 (Analyzed: 54966) Restarts : 608 (Average: 90.40 Last: 111) Model-Level : 299.0 Problems : 10 (Average Length: 19.50 Splits: 0) Lemmas : 54966 (Deleted: 45709) Binary : 3383 (Ratio: 6.15%) Ternary : 978 (Ratio: 1.78%) Conflict : 54966 (Average Length: 526.7 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 54966 (Average: 10.84 Max: 412 Sum: 595605) Executed : 54924 (Average: 10.82 Max: 412 Sum: 594773 Ratio: 99.86%) Bounded : 42 (Average: 19.81 Max: 32 Sum: 832 Ratio: 0.14%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 181544 (Eliminated: 0 Frozen: 55990) Constraints : 1263349 (Binary: 91.4% Ternary: 6.8% Other: 1.8%) Memory Peak : 326MB Max. Length : 30 steps Models : 1 [endof: stats after solve call] Solving Time: 6.79s Memory: 323MB (+0MB) UNKNOWN Iteration Time: 6.81s 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 : 45.722s (Solving: 40.67s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 45.600s Choices : 793665 (Domain: 705937) Conflicts : 63487 (Analyzed: 63484) Restarts : 708 (Average: 89.67 Last: 111) Model-Level : 299.0 Problems : 11 (Average Length: 20.64 Splits: 0) Lemmas : 63484 (Deleted: 51412) Binary : 3872 (Ratio: 6.10%) Ternary : 1051 (Ratio: 1.66%) Conflict : 63484 (Average Length: 488.5 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 63484 (Average: 11.69 Max: 412 Sum: 741815) Executed : 63434 (Average: 11.67 Max: 412 Sum: 740727 Ratio: 99.85%) Bounded : 50 (Average: 21.76 Max: 32 Sum: 1088 Ratio: 0.15%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 181544 (Eliminated: 0 Frozen: 55990) Constraints : 1251059 (Binary: 91.4% Ternary: 6.8% Other: 1.8%) Memory Peak : 326MB Max. Length : 30 steps Models : 1 [endof: stats after solve call] Solving Time: 7.42s Memory: 323MB (+0MB) UNKNOWN Iteration Time: 7.44s 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 : 50.970s (Solving: 45.86s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 50.852s Choices : 858767 (Domain: 770332) Conflicts : 71467 (Analyzed: 71464) Restarts : 808 (Average: 88.45 Last: 111) Model-Level : 299.0 Problems : 12 (Average Length: 21.58 Splits: 0) Lemmas : 71464 (Deleted: 58779) Binary : 4065 (Ratio: 5.69%) Ternary : 1073 (Ratio: 1.50%) Conflict : 71464 (Average Length: 460.6 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 71464 (Average: 11.18 Max: 412 Sum: 798771) Executed : 71413 (Average: 11.16 Max: 412 Sum: 797651 Ratio: 99.86%) Bounded : 51 (Average: 21.96 Max: 32 Sum: 1120 Ratio: 0.14%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 181544 (Eliminated: 0 Frozen: 55990) Constraints : 1245773 (Binary: 91.4% Ternary: 6.7% Other: 1.8%) Memory Peak : 326MB Max. Length : 30 steps Models : 1 [endof: stats after solve call] Solving Time: 5.23s Memory: 323MB (+0MB) UNKNOWN Iteration Time: 5.25s 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: 359.0MB Grounding... [('step', [31]), ('step', [32]), ('step', [33]), ('step', [34]), ('step', [35]), ('check', [35])] Grounding Time: 0.49s Memory: 326MB (+3MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 13 Time : 58.290s (Solving: 52.38s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 58.176s Choices : 988499 (Domain: 897063) Conflicts : 79630 (Analyzed: 79627) Restarts : 908 (Average: 87.69 Last: 111) Model-Level : 299.0 Problems : 13 (Average Length: 22.77 Splits: 0) Lemmas : 79627 (Deleted: 66600) Binary : 4223 (Ratio: 5.30%) Ternary : 1084 (Ratio: 1.36%) Conflict : 79627 (Average Length: 447.0 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 79627 (Average: 11.52 Max: 412 Sum: 917478) Executed : 79576 (Average: 11.51 Max: 412 Sum: 916358 Ratio: 99.88%) Bounded : 51 (Average: 21.96 Max: 32 Sum: 1120 Ratio: 0.12%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 214490 (Eliminated: 0 Frozen: 66425) Constraints : 1495345 (Binary: 91.4% Ternary: 6.8% Other: 1.8%) Memory Peak : 358MB Max. Length : 30 steps Models : 1 [endof: stats after solve call] Solving Time: 6.59s Memory: 340MB (+14MB) UNKNOWN Iteration Time: 7.34s 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: 376.0MB Grounding... [('step', [36]), ('step', [37]), ('step', [38]), ('step', [39]), ('step', [40]), ('check', [40])] Grounding Time: 0.49s Memory: 347MB (+7MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 14 Time : 65.233s (Solving: 58.52s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 65.120s Choices : 1122235 (Domain: 1028087) Conflicts : 87885 (Analyzed: 87882) Restarts : 1008 (Average: 87.18 Last: 111) Model-Level : 299.0 Problems : 14 (Average Length: 24.14 Splits: 0) Lemmas : 87882 (Deleted: 74857) Binary : 4306 (Ratio: 4.90%) Ternary : 1092 (Ratio: 1.24%) Conflict : 87882 (Average Length: 436.4 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 87882 (Average: 11.82 Max: 412 Sum: 1038781) Executed : 87831 (Average: 11.81 Max: 412 Sum: 1037661 Ratio: 99.89%) Bounded : 51 (Average: 21.96 Max: 32 Sum: 1120 Ratio: 0.11%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 247436 (Eliminated: 0 Frozen: 76860) Constraints : 1744930 (Binary: 91.4% Ternary: 6.8% Other: 1.8%) Memory Peak : 382MB Max. Length : 35 steps Models : 1 [endof: stats after solve call] Solving Time: 6.20s Memory: 361MB (+14MB) UNKNOWN Iteration Time: 6.96s 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: 397.0MB Grounding... [('step', [41]), ('step', [42]), ('step', [43]), ('step', [44]), ('step', [45]), ('check', [45])] Grounding Time: 0.47s Memory: 369MB (+8MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 15 Time : 71.083s (Solving: 63.56s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 70.976s Choices : 1210678 (Domain: 1115623) Conflicts : 94980 (Analyzed: 94977) Restarts : 1108 (Average: 85.72 Last: 111) Model-Level : 299.0 Problems : 15 (Average Length: 25.67 Splits: 0) Lemmas : 94977 (Deleted: 82749) Binary : 4381 (Ratio: 4.61%) Ternary : 1098 (Ratio: 1.16%) Conflict : 94977 (Average Length: 427.9 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 94977 (Average: 11.72 Max: 412 Sum: 1113162) Executed : 94926 (Average: 11.71 Max: 412 Sum: 1112042 Ratio: 99.90%) Bounded : 51 (Average: 21.96 Max: 32 Sum: 1120 Ratio: 0.10%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 280382 (Eliminated: 0 Frozen: 87295) Constraints : 1994515 (Binary: 91.4% Ternary: 6.8% Other: 1.8%) Memory Peak : 410MB Max. Length : 40 steps Models : 1 [endof: stats after solve call] Solving Time: 5.11s Memory: 403MB (+34MB) UNKNOWN Iteration Time: 5.86s 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: 445.0MB Grounding... [('step', [46]), ('step', [47]), ('step', [48]), ('step', [49]), ('step', [50]), ('check', [50])] Grounding Time: 0.47s Memory: 403MB (+0MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 16 Time : 78.402s (Solving: 70.07s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 78.300s Choices : 1343512 (Domain: 1247711) Conflicts : 102906 (Analyzed: 102903) Restarts : 1208 (Average: 85.18 Last: 111) Model-Level : 299.0 Problems : 16 (Average Length: 27.31 Splits: 0) Lemmas : 102903 (Deleted: 90043) Binary : 4509 (Ratio: 4.38%) Ternary : 1119 (Ratio: 1.09%) Conflict : 102903 (Average Length: 425.6 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 102903 (Average: 11.96 Max: 503 Sum: 1230752) Executed : 102852 (Average: 11.95 Max: 503 Sum: 1229632 Ratio: 99.91%) Bounded : 51 (Average: 21.96 Max: 32 Sum: 1120 Ratio: 0.09%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 313328 (Eliminated: 0 Frozen: 97730) Constraints : 2244100 (Binary: 91.4% Ternary: 6.8% Other: 1.8%) Memory Peak : 447MB Max. Length : 45 steps Models : 1 [endof: stats after solve call] Solving Time: 6.58s Memory: 418MB (+15MB) UNKNOWN Iteration Time: 7.33s 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: 460.0MB Grounding... [('step', [51]), ('step', [52]), ('step', [53]), ('step', [54]), ('step', [55]), ('check', [55])] Grounding Time: 0.62s Memory: 434MB (+16MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 17 Time : 85.891s (Solving: 76.57s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 85.792s Choices : 1447331 (Domain: 1351297) Conflicts : 110932 (Analyzed: 110929) Restarts : 1308 (Average: 84.81 Last: 111) Model-Level : 299.0 Problems : 17 (Average Length: 29.06 Splits: 0) Lemmas : 110929 (Deleted: 97722) Binary : 4647 (Ratio: 4.19%) Ternary : 1125 (Ratio: 1.01%) Conflict : 110929 (Average Length: 428.1 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 110929 (Average: 11.88 Max: 540 Sum: 1318012) Executed : 110878 (Average: 11.87 Max: 540 Sum: 1316892 Ratio: 99.92%) Bounded : 51 (Average: 21.96 Max: 32 Sum: 1120 Ratio: 0.08%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 346274 (Eliminated: 0 Frozen: 108165) Constraints : 2493685 (Binary: 91.4% Ternary: 6.8% Other: 1.8%) Memory Peak : 484MB Max. Length : 50 steps Models : 1 [endof: stats after solve call] Solving Time: 6.58s Memory: 452MB (+18MB) UNKNOWN Iteration Time: 7.50s 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: 494.0MB Grounding... [('step', [56]), ('step', [57]), ('step', [58]), ('step', [59]), ('step', [60]), ('check', [60])] Grounding Time: 0.48s Memory: 455MB (+3MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 18 Time : 92.912s (Solving: 82.71s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 92.816s Choices : 1541379 (Domain: 1445047) Conflicts : 118811 (Analyzed: 118808) Restarts : 1408 (Average: 84.38 Last: 111) Model-Level : 299.0 Problems : 18 (Average Length: 30.89 Splits: 0) Lemmas : 118808 (Deleted: 105778) Binary : 4724 (Ratio: 3.98%) Ternary : 1129 (Ratio: 0.95%) Conflict : 118808 (Average Length: 427.9 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 118808 (Average: 11.74 Max: 540 Sum: 1394344) Executed : 118757 (Average: 11.73 Max: 540 Sum: 1393224 Ratio: 99.92%) Bounded : 51 (Average: 21.96 Max: 32 Sum: 1120 Ratio: 0.08%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 379220 (Eliminated: 0 Frozen: 118600) Constraints : 2743270 (Binary: 91.4% Ternary: 6.8% Other: 1.8%) Memory Peak : 509MB Max. Length : 55 steps Models : 1 [endof: stats after solve call] Solving Time: 6.22s Memory: 507MB (+52MB) UNKNOWN Iteration Time: 7.03s Iteration 18 Queue: [(13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True)] Grounded Until: 60 Expected Memory: 562.0MB Grounding... [('step', [61]), ('step', [62]), ('step', [63]), ('step', [64]), ('step', [65]), ('check', [65])] Grounding Time: 0.45s Memory: 507MB (+0MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 19 Time : 99.610s (Solving: 88.56s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 99.516s Choices : 1643044 (Domain: 1546068) Conflicts : 126434 (Analyzed: 126431) Restarts : 1508 (Average: 83.84 Last: 111) Model-Level : 299.0 Problems : 19 (Average Length: 32.79 Splits: 0) Lemmas : 126431 (Deleted: 113466) Binary : 4765 (Ratio: 3.77%) Ternary : 1133 (Ratio: 0.90%) Conflict : 126431 (Average Length: 425.2 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 126431 (Average: 11.69 Max: 630 Sum: 1477755) Executed : 126380 (Average: 11.68 Max: 630 Sum: 1476635 Ratio: 99.92%) Bounded : 51 (Average: 21.96 Max: 32 Sum: 1120 Ratio: 0.08%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 412166 (Eliminated: 0 Frozen: 129035) Constraints : 2992855 (Binary: 91.4% Ternary: 6.8% Other: 1.8%) Memory Peak : 557MB Max. Length : 60 steps Models : 1 [endof: stats after solve call] Solving Time: 5.94s Memory: 511MB (+4MB) UNKNOWN Iteration Time: 6.71s Iteration 19 Queue: [(14,70,0,True), (15,75,0,True), (16,80,0,True)] Grounded Until: 65 Expected Memory: 566.0MB Grounding... [('step', [66]), ('step', [67]), ('step', [68]), ('step', [69]), ('step', [70]), ('check', [70])] Grounding Time: 0.49s Memory: 514MB (+3MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 20 Time : 106.661s (Solving: 94.69s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 106.572s Choices : 1738328 (Domain: 1641164) Conflicts : 134075 (Analyzed: 134072) Restarts : 1608 (Average: 83.38 Last: 111) Model-Level : 299.0 Problems : 20 (Average Length: 34.75 Splits: 0) Lemmas : 134072 (Deleted: 120602) Binary : 4818 (Ratio: 3.59%) Ternary : 1134 (Ratio: 0.85%) Conflict : 134072 (Average Length: 420.5 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 134072 (Average: 11.59 Max: 716 Sum: 1553757) Executed : 134021 (Average: 11.58 Max: 716 Sum: 1552637 Ratio: 99.93%) Bounded : 51 (Average: 21.96 Max: 32 Sum: 1120 Ratio: 0.07%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 445112 (Eliminated: 0 Frozen: 139470) Constraints : 3242440 (Binary: 91.4% Ternary: 6.8% Other: 1.8%) Memory Peak : 576MB Max. Length : 65 steps Models : 1 [endof: stats after solve call] Solving Time: 6.22s Memory: 531MB (+17MB) UNKNOWN Iteration Time: 7.07s Iteration 20 Queue: [(15,75,0,True), (16,80,0,True)] Grounded Until: 70 Expected Memory: 586.0MB Grounding... [('step', [71]), ('step', [72]), ('step', [73]), ('step', [74]), ('step', [75]), ('check', [75])] Grounding Time: 0.48s Memory: 534MB (+3MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 21 Time : 114.640s (Solving: 101.73s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 114.556s Choices : 1834449 (Domain: 1737177) Conflicts : 141760 (Analyzed: 141757) Restarts : 1708 (Average: 83.00 Last: 158) Model-Level : 299.0 Problems : 21 (Average Length: 36.76 Splits: 0) Lemmas : 141757 (Deleted: 128097) Binary : 4891 (Ratio: 3.45%) Ternary : 1138 (Ratio: 0.80%) Conflict : 141757 (Average Length: 418.7 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 141757 (Average: 11.49 Max: 730 Sum: 1629314) Executed : 141706 (Average: 11.49 Max: 730 Sum: 1628194 Ratio: 99.93%) Bounded : 51 (Average: 21.96 Max: 32 Sum: 1120 Ratio: 0.07%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 478058 (Eliminated: 0 Frozen: 149905) Constraints : 3492025 (Binary: 91.4% Ternary: 6.8% Other: 1.8%) Memory Peak : 605MB Max. Length : 70 steps Models : 1 [endof: stats after solve call] Solving Time: 7.14s Memory: 558MB (+24MB) UNKNOWN Iteration Time: 8.00s Iteration 21 Queue: [(16,80,0,True)] Grounded Until: 75 Expected Memory: 613.0MB Grounding... [('step', [76]), ('step', [77]), ('step', [78]), ('step', [79]), ('step', [80]), ('check', [80])] Grounding Time: 0.49s Memory: 558MB (+0MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 22 Time : 121.855s (Solving: 107.98s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 121.776s Choices : 1920409 (Domain: 1823055) Conflicts : 149127 (Analyzed: 149124) Restarts : 1808 (Average: 82.48 Last: 158) Model-Level : 299.0 Problems : 22 (Average Length: 38.82 Splits: 0) Lemmas : 149124 (Deleted: 135578) Binary : 4922 (Ratio: 3.30%) Ternary : 1138 (Ratio: 0.76%) Conflict : 149124 (Average Length: 415.2 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 149124 (Average: 11.36 Max: 730 Sum: 1694162) Executed : 149073 (Average: 11.35 Max: 730 Sum: 1693042 Ratio: 99.93%) Bounded : 51 (Average: 21.96 Max: 32 Sum: 1120 Ratio: 0.07%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 511004 (Eliminated: 0 Frozen: 160340) Constraints : 3741610 (Binary: 91.4% Ternary: 6.8% Other: 1.8%) Memory Peak : 629MB Max. Length : 75 steps Models : 1 [endof: stats after solve call] Solving Time: 6.35s Memory: 582MB (+24MB) UNKNOWN Iteration Time: 7.23s Iteration 22 Queue: [(4,20,2,True), (5,25,2,True), (6,30,2,True), (7,35,1,True), (8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] Grounded Until: 80 Blocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 23 Time : 129.021s (Solving: 115.03s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 128.944s Choices : 2000487 (Domain: 1903129) Conflicts : 157808 (Analyzed: 157805) Restarts : 1908 (Average: 82.71 Last: 158) Model-Level : 299.0 Problems : 23 (Average Length: 40.70 Splits: 0) Lemmas : 157805 (Deleted: 143334) Binary : 5127 (Ratio: 3.25%) Ternary : 1180 (Ratio: 0.75%) Conflict : 157805 (Average Length: 407.9 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 157805 (Average: 11.21 Max: 730 Sum: 1768975) Executed : 157746 (Average: 11.20 Max: 730 Sum: 1767442 Ratio: 99.91%) Bounded : 59 (Average: 25.98 Max: 82 Sum: 1533 Ratio: 0.09%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 511004 (Eliminated: 0 Frozen: 160340) Constraints : 3741610 (Binary: 91.4% Ternary: 6.8% Other: 1.8%) Memory Peak : 629MB Max. Length : 80 steps Models : 1 [endof: stats after solve call] Solving Time: 7.13s Memory: 582MB (+0MB) UNKNOWN Iteration Time: 7.17s Iteration 23 Queue: [(5,25,2,True), (6,30,2,True), (7,35,1,True), (8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] Grounded Until: 80 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 24 Time : 133.518s (Solving: 119.42s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 133.440s Choices : 2054484 (Domain: 1956786) Conflicts : 165232 (Analyzed: 165229) Restarts : 2008 (Average: 82.29 Last: 158) Model-Level : 299.0 Problems : 24 (Average Length: 42.42 Splits: 0) Lemmas : 165229 (Deleted: 149362) Binary : 5228 (Ratio: 3.16%) Ternary : 1199 (Ratio: 0.73%) Conflict : 165229 (Average Length: 398.1 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 165229 (Average: 10.98 Max: 730 Sum: 1814946) Executed : 165170 (Average: 10.98 Max: 730 Sum: 1813413 Ratio: 99.92%) Bounded : 59 (Average: 25.98 Max: 82 Sum: 1533 Ratio: 0.08%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 511004 (Eliminated: 0 Frozen: 160340) Constraints : 3732105 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 629MB Max. Length : 80 steps Models : 1 [endof: stats after solve call] Solving Time: 4.46s Memory: 582MB (+0MB) UNKNOWN Iteration Time: 4.50s Iteration 24 Queue: [(6,30,2,True), (7,35,1,True), (8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] Grounded Until: 80 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 25 Time : 137.111s (Solving: 122.89s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 137.036s Choices : 2099194 (Domain: 2001330) Conflicts : 172644 (Analyzed: 172641) Restarts : 2108 (Average: 81.90 Last: 158) Model-Level : 299.0 Problems : 25 (Average Length: 44.00 Splits: 0) Lemmas : 172641 (Deleted: 156682) Binary : 5260 (Ratio: 3.05%) Ternary : 1225 (Ratio: 0.71%) Conflict : 172641 (Average Length: 392.2 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 172641 (Average: 10.73 Max: 730 Sum: 1852382) Executed : 172581 (Average: 10.72 Max: 730 Sum: 1850767 Ratio: 99.91%) Bounded : 60 (Average: 26.92 Max: 82 Sum: 1615 Ratio: 0.09%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 511004 (Eliminated: 0 Frozen: 160340) Constraints : 3732105 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 629MB Max. Length : 80 steps Models : 1 [endof: stats after solve call] Solving Time: 3.55s Memory: 582MB (+0MB) UNKNOWN Iteration Time: 3.60s Iteration 25 Queue: [(7,35,1,True), (8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] Grounded Until: 80 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 26 Time : 140.394s (Solving: 126.07s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 140.320s Choices : 2132610 (Domain: 2034728) Conflicts : 180026 (Analyzed: 180023) Restarts : 2208 (Average: 81.53 Last: 158) Model-Level : 299.0 Problems : 26 (Average Length: 45.46 Splits: 0) Lemmas : 180023 (Deleted: 163987) Binary : 5297 (Ratio: 2.94%) Ternary : 1237 (Ratio: 0.69%) Conflict : 180023 (Average Length: 386.5 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 180023 (Average: 10.44 Max: 730 Sum: 1878660) Executed : 179961 (Average: 10.43 Max: 730 Sum: 1876884 Ratio: 99.91%) Bounded : 62 (Average: 28.65 Max: 82 Sum: 1776 Ratio: 0.09%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 511004 (Eliminated: 0 Frozen: 160340) Constraints : 3731927 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 629MB Max. Length : 80 steps Models : 1 [endof: stats after solve call] Solving Time: 3.25s Memory: 582MB (+0MB) UNKNOWN Iteration Time: 3.29s Iteration 26 Queue: [(8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] Grounded Until: 80 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 27 Time : 144.510s (Solving: 130.07s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 144.440s Choices : 2201502 (Domain: 2103220) Conflicts : 187527 (Analyzed: 187524) Restarts : 2308 (Average: 81.25 Last: 158) Model-Level : 299.0 Problems : 27 (Average Length: 46.81 Splits: 0) Lemmas : 187524 (Deleted: 170855) Binary : 5365 (Ratio: 2.86%) Ternary : 1245 (Ratio: 0.66%) Conflict : 187524 (Average Length: 379.8 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 187524 (Average: 10.34 Max: 730 Sum: 1939007) Executed : 187461 (Average: 10.33 Max: 730 Sum: 1937149 Ratio: 99.90%) Bounded : 63 (Average: 29.49 Max: 82 Sum: 1858 Ratio: 0.10%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 511004 (Eliminated: 0 Frozen: 160340) Constraints : 3731913 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 629MB Max. Length : 80 steps Models : 1 [endof: stats after solve call] Solving Time: 4.07s Memory: 582MB (+0MB) UNKNOWN Iteration Time: 4.12s Iteration 27 Queue: [(9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] Grounded Until: 80 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 28 Time : 148.998s (Solving: 134.45s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 148.932s Choices : 2241566 (Domain: 2143209) Conflicts : 194817 (Analyzed: 194814) Restarts : 2408 (Average: 80.90 Last: 158) Model-Level : 299.0 Problems : 28 (Average Length: 48.07 Splits: 0) Lemmas : 194814 (Deleted: 178038) Binary : 5397 (Ratio: 2.77%) Ternary : 1259 (Ratio: 0.65%) Conflict : 194814 (Average Length: 377.4 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 194814 (Average: 10.11 Max: 730 Sum: 1969991) Executed : 194751 (Average: 10.10 Max: 730 Sum: 1968133 Ratio: 99.91%) Bounded : 63 (Average: 29.49 Max: 82 Sum: 1858 Ratio: 0.09%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 511004 (Eliminated: 0 Frozen: 160340) Constraints : 3731734 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 629MB Max. Length : 80 steps Models : 1 [endof: stats after solve call] Solving Time: 4.45s Memory: 582MB (+0MB) UNKNOWN Iteration Time: 4.49s Iteration 28 Queue: [(10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] Grounded Until: 80 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 29 Time : 154.009s (Solving: 139.34s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 153.944s Choices : 2351586 (Domain: 2252740) Conflicts : 202518 (Analyzed: 202515) Restarts : 2508 (Average: 80.75 Last: 158) Model-Level : 299.0 Problems : 29 (Average Length: 49.24 Splits: 0) Lemmas : 202515 (Deleted: 185098) Binary : 5437 (Ratio: 2.68%) Ternary : 1283 (Ratio: 0.63%) Conflict : 202515 (Average Length: 370.9 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 202515 (Average: 10.22 Max: 730 Sum: 2069638) Executed : 202450 (Average: 10.21 Max: 730 Sum: 2067620 Ratio: 99.90%) Bounded : 65 (Average: 31.05 Max: 82 Sum: 2018 Ratio: 0.10%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 511004 (Eliminated: 0 Frozen: 160340) Constraints : 3731734 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 629MB Max. Length : 80 steps Models : 1 [endof: stats after solve call] Solving Time: 4.97s Memory: 582MB (+0MB) UNKNOWN Iteration Time: 5.02s Iteration 29 Queue: [(11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] Grounded Until: 80 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 30 Time : 159.251s (Solving: 144.47s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 159.188s Choices : 2471333 (Domain: 2370532) Conflicts : 210074 (Analyzed: 210071) Restarts : 2608 (Average: 80.55 Last: 158) Model-Level : 299.0 Problems : 30 (Average Length: 50.33 Splits: 0) Lemmas : 210071 (Deleted: 192549) Binary : 5504 (Ratio: 2.62%) Ternary : 1305 (Ratio: 0.62%) Conflict : 210071 (Average Length: 366.4 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 210071 (Average: 10.37 Max: 730 Sum: 2178423) Executed : 210005 (Average: 10.36 Max: 730 Sum: 2176323 Ratio: 99.90%) Bounded : 66 (Average: 31.82 Max: 82 Sum: 2100 Ratio: 0.10%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 511004 (Eliminated: 0 Frozen: 160340) Constraints : 3731557 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 629MB Max. Length : 80 steps Models : 1 [endof: stats after solve call] Solving Time: 5.20s Memory: 582MB (+0MB) UNKNOWN Iteration Time: 5.25s Iteration 30 Queue: [(12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] Grounded Until: 80 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 31 Time : 164.673s (Solving: 149.77s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 164.612s Choices : 2559094 (Domain: 2457354) Conflicts : 217768 (Analyzed: 217765) Restarts : 2708 (Average: 80.42 Last: 158) Model-Level : 299.0 Problems : 31 (Average Length: 51.35 Splits: 0) Lemmas : 217765 (Deleted: 199892) Binary : 5554 (Ratio: 2.55%) Ternary : 1316 (Ratio: 0.60%) Conflict : 217765 (Average Length: 362.4 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 217765 (Average: 10.36 Max: 730 Sum: 2256015) Executed : 217699 (Average: 10.35 Max: 730 Sum: 2253915 Ratio: 99.91%) Bounded : 66 (Average: 31.82 Max: 82 Sum: 2100 Ratio: 0.09%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 511004 (Eliminated: 0 Frozen: 160340) Constraints : 3731531 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 629MB Max. Length : 80 steps Models : 1 [endof: stats after solve call] Solving Time: 5.38s Memory: 582MB (+0MB) UNKNOWN Iteration Time: 5.43s Iteration 31 Queue: [(13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] Grounded Until: 80 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 32 Time : 170.162s (Solving: 155.16s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 170.104s Choices : 2740269 (Domain: 2637656) Conflicts : 225465 (Analyzed: 225462) Restarts : 2808 (Average: 80.29 Last: 158) Model-Level : 299.0 Problems : 32 (Average Length: 52.31 Splits: 0) Lemmas : 225462 (Deleted: 207333) Binary : 5743 (Ratio: 2.55%) Ternary : 1427 (Ratio: 0.63%) Conflict : 225462 (Average Length: 358.1 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 225462 (Average: 10.75 Max: 730 Sum: 2424631) Executed : 225395 (Average: 10.74 Max: 730 Sum: 2422452 Ratio: 99.91%) Bounded : 67 (Average: 32.52 Max: 82 Sum: 2179 Ratio: 0.09%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 511004 (Eliminated: 0 Frozen: 160340) Constraints : 3731531 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 629MB Max. Length : 80 steps Models : 1 [endof: stats after solve call] Solving Time: 5.46s Memory: 582MB (+0MB) UNKNOWN Iteration Time: 5.49s Iteration 32 Queue: [(14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] Grounded Until: 80 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 33 Time : 176.494s (Solving: 161.39s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 176.440s Choices : 2918817 (Domain: 2815119) Conflicts : 233066 (Analyzed: 233063) Restarts : 2908 (Average: 80.15 Last: 158) Model-Level : 299.0 Problems : 33 (Average Length: 53.21 Splits: 0) Lemmas : 233063 (Deleted: 214453) Binary : 5845 (Ratio: 2.51%) Ternary : 1442 (Ratio: 0.62%) Conflict : 233063 (Average Length: 354.9 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 233063 (Average: 11.11 Max: 772 Sum: 2589823) Executed : 232996 (Average: 11.10 Max: 772 Sum: 2587644 Ratio: 99.92%) Bounded : 67 (Average: 32.52 Max: 82 Sum: 2179 Ratio: 0.08%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 511004 (Eliminated: 0 Frozen: 160340) Constraints : 3731531 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 629MB Max. Length : 80 steps Models : 1 [endof: stats after solve call] Solving Time: 6.30s Memory: 582MB (+0MB) UNKNOWN Iteration Time: 6.34s Iteration 33 Queue: [(15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] Grounded Until: 80 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 34 Time : 182.364s (Solving: 167.13s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 182.312s Choices : 3099661 (Domain: 2994801) Conflicts : 240982 (Analyzed: 240979) Restarts : 3008 (Average: 80.11 Last: 158) Model-Level : 299.0 Problems : 34 (Average Length: 54.06 Splits: 0) Lemmas : 240979 (Deleted: 221722) Binary : 5940 (Ratio: 2.46%) Ternary : 1481 (Ratio: 0.61%) Conflict : 240979 (Average Length: 351.2 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 240979 (Average: 11.44 Max: 772 Sum: 2756933) Executed : 240912 (Average: 11.43 Max: 772 Sum: 2754754 Ratio: 99.92%) Bounded : 67 (Average: 32.52 Max: 82 Sum: 2179 Ratio: 0.08%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 511004 (Eliminated: 0 Frozen: 160340) Constraints : 3731531 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 629MB Max. Length : 80 steps Models : 1 [endof: stats after solve call] Solving Time: 5.82s Memory: 582MB (+0MB) UNKNOWN Iteration Time: 5.88s Iteration 34 Queue: [(16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] Grounded Until: 80 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 35 Time : 189.349s (Solving: 174.00s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 189.300s Choices : 3331242 (Domain: 3225380) Conflicts : 248706 (Analyzed: 248703) Restarts : 3108 (Average: 80.02 Last: 158) Model-Level : 299.0 Problems : 35 (Average Length: 54.86 Splits: 0) Lemmas : 248703 (Deleted: 229344) Binary : 6026 (Ratio: 2.42%) Ternary : 1508 (Ratio: 0.61%) Conflict : 248703 (Average Length: 348.8 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 248703 (Average: 11.95 Max: 776 Sum: 2973195) Executed : 248636 (Average: 11.95 Max: 776 Sum: 2971016 Ratio: 99.93%) Bounded : 67 (Average: 32.52 Max: 82 Sum: 2179 Ratio: 0.07%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 511004 (Eliminated: 0 Frozen: 160340) Constraints : 3731531 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 629MB Max. Length : 80 steps Models : 1 [endof: stats after solve call] Solving Time: 6.95s Memory: 582MB (+0MB) UNKNOWN Iteration Time: 6.99s Iteration 35 Queue: [(17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] Grounded Until: 80 Expected Memory: 637.0MB Grounding... [('step', [81]), ('step', [82]), ('step', [83]), ('step', [84]), ('step', [85]), ('check', [85])] Grounding Time: 0.48s Memory: 582MB (+0MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 36 Time : 197.758s (Solving: 181.45s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 197.712s Choices : 3464379 (Domain: 3358328) Conflicts : 256874 (Analyzed: 256871) Restarts : 3208 (Average: 80.07 Last: 158) Model-Level : 299.0 Problems : 36 (Average Length: 55.75 Splits: 0) Lemmas : 256871 (Deleted: 237249) Binary : 6102 (Ratio: 2.38%) Ternary : 1513 (Ratio: 0.59%) Conflict : 256871 (Average Length: 347.3 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 256871 (Average: 12.01 Max: 776 Sum: 3085155) Executed : 256804 (Average: 12.00 Max: 776 Sum: 3082976 Ratio: 99.93%) Bounded : 67 (Average: 32.52 Max: 82 Sum: 2179 Ratio: 0.07%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 543950 (Eliminated: 0 Frozen: 170775) Constraints : 3981116 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 658MB Max. Length : 80 steps Models : 1 [endof: stats after solve call] Solving Time: 7.55s Memory: 602MB (+20MB) UNKNOWN Iteration Time: 8.42s Iteration 36 Queue: [(18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)] Grounded Until: 85 Expected Memory: 657.0MB Grounding... [('step', [86]), ('step', [87]), ('step', [88]), ('step', [89]), ('step', [90]), ('check', [90])] Grounding Time: 0.47s Memory: 602MB (+0MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 37 Time : 204.336s (Solving: 187.06s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 204.292s Choices : 3547140 (Domain: 3441028) Conflicts : 264789 (Analyzed: 264786) Restarts : 3308 (Average: 80.04 Last: 158) Model-Level : 299.0 Problems : 37 (Average Length: 56.73 Splits: 0) Lemmas : 264786 (Deleted: 245107) Binary : 6119 (Ratio: 2.31%) Ternary : 1515 (Ratio: 0.57%) Conflict : 264786 (Average Length: 345.1 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 264786 (Average: 11.88 Max: 776 Sum: 3145674) Executed : 264719 (Average: 11.87 Max: 776 Sum: 3143495 Ratio: 99.93%) Bounded : 67 (Average: 32.52 Max: 82 Sum: 2179 Ratio: 0.07%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 576896 (Eliminated: 0 Frozen: 181210) Constraints : 4230701 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 681MB Max. Length : 85 steps Models : 1 [endof: stats after solve call] Solving Time: 5.72s Memory: 673MB (+71MB) UNKNOWN Iteration Time: 6.59s Iteration 37 Queue: [(19,95,0,True), (20,100,0,True), (21,105,0,True)] Grounded Until: 90 Expected Memory: 744.0MB Grounding... [('step', [91]), ('step', [92]), ('step', [93]), ('step', [94]), ('step', [95]), ('check', [95])] Grounding Time: 0.47s Memory: 673MB (+0MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 38 Time : 210.808s (Solving: 192.55s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 210.764s Choices : 3604769 (Domain: 3498653) Conflicts : 272146 (Analyzed: 272143) Restarts : 3408 (Average: 79.85 Last: 158) Model-Level : 299.0 Problems : 38 (Average Length: 57.79 Splits: 0) Lemmas : 272143 (Deleted: 252725) Binary : 6141 (Ratio: 2.26%) Ternary : 1517 (Ratio: 0.56%) Conflict : 272143 (Average Length: 342.7 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 272143 (Average: 11.69 Max: 782 Sum: 3180102) Executed : 272076 (Average: 11.68 Max: 782 Sum: 3177923 Ratio: 99.93%) Bounded : 67 (Average: 32.52 Max: 82 Sum: 2179 Ratio: 0.07%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 609842 (Eliminated: 0 Frozen: 191645) Constraints : 4480286 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 747MB Max. Length : 90 steps Models : 1 [endof: stats after solve call] Solving Time: 5.61s Memory: 677MB (+4MB) UNKNOWN Iteration Time: 6.48s Iteration 38 Queue: [(20,100,0,True), (21,105,0,True)] Grounded Until: 95 Expected Memory: 748.0MB Grounding... [('step', [96]), ('step', [97]), ('step', [98]), ('step', [99]), ('step', [100]), ('check', [100])] Grounding Time: 0.51s Memory: 677MB (+0MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 39 Time : 217.985s (Solving: 198.68s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 217.944s Choices : 3687345 (Domain: 3581184) Conflicts : 279172 (Analyzed: 279169) Restarts : 3508 (Average: 79.58 Last: 158) Model-Level : 299.0 Problems : 39 (Average Length: 58.92 Splits: 0) Lemmas : 279169 (Deleted: 259926) Binary : 6171 (Ratio: 2.21%) Ternary : 1520 (Ratio: 0.54%) Conflict : 279169 (Average Length: 341.7 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 279169 (Average: 11.60 Max: 965 Sum: 3237045) Executed : 279102 (Average: 11.59 Max: 965 Sum: 3234866 Ratio: 99.93%) Bounded : 67 (Average: 32.52 Max: 82 Sum: 2179 Ratio: 0.07%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 642788 (Eliminated: 0 Frozen: 202080) Constraints : 4729871 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 756MB Max. Length : 95 steps Models : 1 [endof: stats after solve call] Solving Time: 6.25s Memory: 685MB (+8MB) UNKNOWN Iteration Time: 7.19s Iteration 39 Queue: [(21,105,0,True)] Grounded Until: 100 Expected Memory: 756.0MB Grounding... [('step', [101]), ('step', [102]), ('step', [103]), ('step', [104]), ('step', [105]), ('check', [105])] Grounding Time: 0.49s Memory: 685MB (+0MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 40 Time : 225.782s (Solving: 205.43s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 225.744s Choices : 3793124 (Domain: 3686889) Conflicts : 286744 (Analyzed: 286741) Restarts : 3608 (Average: 79.47 Last: 158) Model-Level : 299.0 Problems : 40 (Average Length: 60.12 Splits: 0) Lemmas : 286741 (Deleted: 266870) Binary : 6213 (Ratio: 2.17%) Ternary : 1529 (Ratio: 0.53%) Conflict : 286741 (Average Length: 341.0 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 286741 (Average: 11.56 Max: 997 Sum: 3315278) Executed : 286674 (Average: 11.55 Max: 997 Sum: 3313099 Ratio: 99.93%) Bounded : 67 (Average: 32.52 Max: 82 Sum: 2179 Ratio: 0.07%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 675734 (Eliminated: 0 Frozen: 212515) Constraints : 4979456 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 777MB Max. Length : 100 steps Models : 1 [endof: stats after solve call] Solving Time: 6.88s Memory: 705MB (+20MB) UNKNOWN Iteration Time: 7.81s Iteration 40 Queue: [(4,20,3,True), (5,25,3,True), (6,30,3,True), (7,35,2,True), (8,40,2,True), (9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] Grounded Until: 105 Blocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 41 Time : 229.765s (Solving: 209.26s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 229.732s Choices : 3864963 (Domain: 3758728) Conflicts : 294555 (Analyzed: 294552) Restarts : 3708 (Average: 79.44 Last: 158) Model-Level : 299.0 Problems : 41 (Average Length: 61.27 Splits: 0) Lemmas : 294552 (Deleted: 274125) Binary : 6303 (Ratio: 2.14%) Ternary : 1549 (Ratio: 0.53%) Conflict : 294552 (Average Length: 340.2 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 294552 (Average: 11.47 Max: 997 Sum: 3377467) Executed : 294482 (Average: 11.46 Max: 997 Sum: 3374967 Ratio: 99.93%) Bounded : 70 (Average: 35.71 Max: 107 Sum: 2500 Ratio: 0.07%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 675734 (Eliminated: 0 Frozen: 212515) Constraints : 4979456 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 777MB Max. Length : 105 steps Models : 1 [endof: stats after solve call] Solving Time: 3.93s Memory: 705MB (+0MB) UNKNOWN Iteration Time: 3.99s Iteration 41 Queue: [(5,25,3,True), (6,30,3,True), (7,35,2,True), (8,40,2,True), (9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] Grounded Until: 105 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 42 Time : 233.535s (Solving: 212.89s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 233.504s Choices : 3906002 (Domain: 3798679) Conflicts : 301944 (Analyzed: 301941) Restarts : 3808 (Average: 79.29 Last: 158) Model-Level : 299.0 Problems : 42 (Average Length: 62.36 Splits: 0) Lemmas : 301941 (Deleted: 281613) Binary : 6378 (Ratio: 2.11%) Ternary : 1591 (Ratio: 0.53%) Conflict : 301941 (Average Length: 338.1 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 301941 (Average: 11.30 Max: 997 Sum: 3411185) Executed : 301871 (Average: 11.29 Max: 997 Sum: 3408685 Ratio: 99.93%) Bounded : 70 (Average: 35.71 Max: 107 Sum: 2500 Ratio: 0.07%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 675734 (Eliminated: 0 Frozen: 212515) Constraints : 4974893 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 777MB Max. Length : 105 steps Models : 1 [endof: stats after solve call] Solving Time: 3.72s Memory: 705MB (+0MB) UNKNOWN Iteration Time: 3.77s Iteration 42 Queue: [(6,30,3,True), (7,35,2,True), (8,40,2,True), (9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] Grounded Until: 105 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 43 Time : 238.436s (Solving: 217.65s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 238.408s Choices : 3973476 (Domain: 3865477) Conflicts : 309721 (Analyzed: 309718) Restarts : 3908 (Average: 79.25 Last: 158) Model-Level : 299.0 Problems : 43 (Average Length: 63.40 Splits: 0) Lemmas : 309718 (Deleted: 288692) Binary : 6435 (Ratio: 2.08%) Ternary : 1608 (Ratio: 0.52%) Conflict : 309718 (Average Length: 336.0 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 309718 (Average: 11.21 Max: 997 Sum: 3470886) Executed : 309648 (Average: 11.20 Max: 997 Sum: 3468386 Ratio: 99.93%) Bounded : 70 (Average: 35.71 Max: 107 Sum: 2500 Ratio: 0.07%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 675734 (Eliminated: 0 Frozen: 212515) Constraints : 4974893 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 777MB Max. Length : 105 steps Models : 1 [endof: stats after solve call] Solving Time: 4.85s Memory: 705MB (+0MB) UNKNOWN Iteration Time: 4.91s Iteration 43 Queue: [(7,35,2,True), (8,40,2,True), (9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] Grounded Until: 105 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 44 Time : 243.947s (Solving: 223.00s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 243.920s Choices : 4060467 (Domain: 3951298) Conflicts : 317479 (Analyzed: 317476) Restarts : 4008 (Average: 79.21 Last: 158) Model-Level : 299.0 Problems : 44 (Average Length: 64.39 Splits: 0) Lemmas : 317476 (Deleted: 296184) Binary : 6541 (Ratio: 2.06%) Ternary : 1648 (Ratio: 0.52%) Conflict : 317476 (Average Length: 334.9 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 317476 (Average: 11.18 Max: 997 Sum: 3547917) Executed : 317404 (Average: 11.17 Max: 997 Sum: 3545203 Ratio: 99.92%) Bounded : 72 (Average: 37.69 Max: 107 Sum: 2714 Ratio: 0.08%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 675734 (Eliminated: 0 Frozen: 212515) Constraints : 4974893 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 777MB Max. Length : 105 steps Models : 1 [endof: stats after solve call] Solving Time: 5.45s Memory: 705MB (+0MB) UNKNOWN Iteration Time: 5.52s Iteration 44 Queue: [(8,40,2,True), (9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] Grounded Until: 105 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 45 Time : 248.826s (Solving: 227.74s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 248.800s Choices : 4138235 (Domain: 4027983) Conflicts : 324942 (Analyzed: 324939) Restarts : 4108 (Average: 79.10 Last: 158) Model-Level : 299.0 Problems : 45 (Average Length: 65.33 Splits: 0) Lemmas : 324939 (Deleted: 303720) Binary : 6631 (Ratio: 2.04%) Ternary : 1683 (Ratio: 0.52%) Conflict : 324939 (Average Length: 334.2 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 324939 (Average: 11.13 Max: 997 Sum: 3616550) Executed : 324865 (Average: 11.12 Max: 997 Sum: 3613626 Ratio: 99.92%) Bounded : 74 (Average: 39.51 Max: 107 Sum: 2924 Ratio: 0.08%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 675734 (Eliminated: 0 Frozen: 212515) Constraints : 4974854 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 777MB Max. Length : 105 steps Models : 1 [endof: stats after solve call] Solving Time: 4.84s Memory: 705MB (+0MB) UNKNOWN Iteration Time: 4.89s Iteration 45 Queue: [(9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] Grounded Until: 105 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 46 Time : 253.883s (Solving: 232.66s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 253.860s Choices : 4217754 (Domain: 4106990) Conflicts : 332583 (Analyzed: 332580) Restarts : 4208 (Average: 79.04 Last: 158) Model-Level : 299.0 Problems : 46 (Average Length: 66.24 Splits: 0) Lemmas : 332580 (Deleted: 310779) Binary : 6749 (Ratio: 2.03%) Ternary : 1717 (Ratio: 0.52%) Conflict : 332580 (Average Length: 332.2 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 332580 (Average: 11.09 Max: 997 Sum: 3687327) Executed : 332502 (Average: 11.08 Max: 997 Sum: 3683982 Ratio: 99.91%) Bounded : 78 (Average: 42.88 Max: 107 Sum: 3345 Ratio: 0.09%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 675734 (Eliminated: 0 Frozen: 212515) Constraints : 4974855 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 777MB Max. Length : 105 steps Models : 1 [endof: stats after solve call] Solving Time: 5.01s Memory: 705MB (+0MB) UNKNOWN Iteration Time: 5.06s Iteration 46 Queue: [(10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] Grounded Until: 105 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 47 Time : 261.905s (Solving: 240.50s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 261.884s Choices : 4434104 (Domain: 4320327) Conflicts : 341537 (Analyzed: 341534) Restarts : 4308 (Average: 79.28 Last: 163) Model-Level : 299.0 Problems : 47 (Average Length: 67.11 Splits: 0) Lemmas : 341534 (Deleted: 319941) Binary : 7044 (Ratio: 2.06%) Ternary : 1792 (Ratio: 0.52%) Conflict : 341534 (Average Length: 334.4 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 341534 (Average: 11.39 Max: 997 Sum: 3890199) Executed : 341456 (Average: 11.38 Max: 997 Sum: 3886854 Ratio: 99.91%) Bounded : 78 (Average: 42.88 Max: 107 Sum: 3345 Ratio: 0.09%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 675734 (Eliminated: 0 Frozen: 212515) Constraints : 4970306 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 777MB Max. Length : 105 steps Models : 1 [endof: stats after solve call] Solving Time: 7.96s Memory: 705MB (+0MB) UNKNOWN Iteration Time: 8.03s Iteration 47 Queue: [(11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] Grounded Until: 105 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 48 Time : 268.292s (Solving: 246.72s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 268.276s Choices : 4591248 (Domain: 4476533) Conflicts : 349611 (Analyzed: 349608) Restarts : 4408 (Average: 79.31 Last: 163) Model-Level : 299.0 Problems : 48 (Average Length: 67.94 Splits: 0) Lemmas : 349608 (Deleted: 326205) Binary : 7207 (Ratio: 2.06%) Ternary : 1879 (Ratio: 0.54%) Conflict : 349608 (Average Length: 333.6 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 349608 (Average: 11.54 Max: 997 Sum: 4034111) Executed : 349530 (Average: 11.53 Max: 997 Sum: 4030766 Ratio: 99.92%) Bounded : 78 (Average: 42.88 Max: 107 Sum: 3345 Ratio: 0.08%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 675734 (Eliminated: 0 Frozen: 212515) Constraints : 4970306 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 777MB Max. Length : 105 steps Models : 1 [endof: stats after solve call] Solving Time: 6.32s Memory: 705MB (+0MB) UNKNOWN Iteration Time: 6.39s Iteration 48 Queue: [(12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] Grounded Until: 105 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 49 Time : 275.550s (Solving: 253.84s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 275.536s Choices : 4781836 (Domain: 4665516) Conflicts : 357702 (Analyzed: 357699) Restarts : 4508 (Average: 79.35 Last: 163) Model-Level : 299.0 Problems : 49 (Average Length: 68.73 Splits: 0) Lemmas : 357699 (Deleted: 333767) Binary : 7371 (Ratio: 2.06%) Ternary : 1905 (Ratio: 0.53%) Conflict : 357699 (Average Length: 332.8 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 357699 (Average: 11.77 Max: 997 Sum: 4209909) Executed : 357621 (Average: 11.76 Max: 997 Sum: 4206564 Ratio: 99.92%) Bounded : 78 (Average: 42.88 Max: 107 Sum: 3345 Ratio: 0.08%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 675734 (Eliminated: 0 Frozen: 212515) Constraints : 4970306 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 777MB Max. Length : 105 steps Models : 1 [endof: stats after solve call] Solving Time: 7.21s Memory: 705MB (+0MB) UNKNOWN Iteration Time: 7.26s Iteration 49 Queue: [(13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] Grounded Until: 105 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 50 Time : 285.802s (Solving: 263.95s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 285.792s Choices : 5180054 (Domain: 5058221) Conflicts : 366497 (Analyzed: 366494) Restarts : 4608 (Average: 79.53 Last: 163) Model-Level : 299.0 Problems : 50 (Average Length: 69.50 Splits: 0) Lemmas : 366494 (Deleted: 343213) Binary : 7791 (Ratio: 2.13%) Ternary : 1981 (Ratio: 0.54%) Conflict : 366494 (Average Length: 339.5 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 366494 (Average: 12.51 Max: 997 Sum: 4584678) Executed : 366416 (Average: 12.50 Max: 997 Sum: 4581333 Ratio: 99.93%) Bounded : 78 (Average: 42.88 Max: 107 Sum: 3345 Ratio: 0.07%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 675734 (Eliminated: 0 Frozen: 212515) Constraints : 4970306 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 777MB Max. Length : 105 steps Models : 1 [endof: stats after solve call] Solving Time: 10.21s Memory: 705MB (+0MB) UNKNOWN Iteration Time: 10.26s Iteration 50 Queue: [(17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] Grounded Until: 105 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 51 Time : 290.277s (Solving: 268.27s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 290.268s Choices : 5280218 (Domain: 5158210) Conflicts : 374425 (Analyzed: 374422) Restarts : 4708 (Average: 79.53 Last: 163) Model-Level : 299.0 Problems : 51 (Average Length: 70.24 Splits: 0) Lemmas : 374422 (Deleted: 349598) Binary : 7837 (Ratio: 2.09%) Ternary : 1998 (Ratio: 0.53%) Conflict : 374422 (Average Length: 337.6 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 374422 (Average: 12.48 Max: 997 Sum: 4671202) Executed : 374343 (Average: 12.47 Max: 997 Sum: 4667750 Ratio: 99.93%) Bounded : 79 (Average: 43.70 Max: 107 Sum: 3452 Ratio: 0.07%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 675734 (Eliminated: 0 Frozen: 212515) Constraints : 4970306 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 777MB Max. Length : 105 steps Models : 1 [endof: stats after solve call] Solving Time: 4.42s Memory: 705MB (+0MB) UNKNOWN Iteration Time: 4.48s Iteration 51 Queue: [(18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] Grounded Until: 105 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 52 Time : 299.585s (Solving: 277.44s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 299.580s Choices : 5597359 (Domain: 5474121) Conflicts : 382995 (Analyzed: 382992) Restarts : 4808 (Average: 79.66 Last: 163) Model-Level : 299.0 Problems : 52 (Average Length: 70.94 Splits: 0) Lemmas : 382992 (Deleted: 357216) Binary : 8017 (Ratio: 2.09%) Ternary : 2015 (Ratio: 0.53%) Conflict : 382992 (Average Length: 338.9 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 382992 (Average: 12.97 Max: 997 Sum: 4968017) Executed : 382913 (Average: 12.96 Max: 997 Sum: 4964565 Ratio: 99.93%) Bounded : 79 (Average: 43.70 Max: 107 Sum: 3452 Ratio: 0.07%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 675734 (Eliminated: 0 Frozen: 212515) Constraints : 4970293 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 777MB Max. Length : 105 steps Models : 1 [endof: stats after solve call] Solving Time: 9.27s Memory: 705MB (+0MB) UNKNOWN Iteration Time: 9.32s Iteration 52 Queue: [(19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] Grounded Until: 105 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 53 Time : 306.542s (Solving: 284.23s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 306.540s Choices : 5813368 (Domain: 5689156) Conflicts : 390853 (Analyzed: 390850) Restarts : 4908 (Average: 79.64 Last: 163) Model-Level : 299.0 Problems : 53 (Average Length: 71.62 Splits: 0) Lemmas : 390850 (Deleted: 365385) Binary : 8112 (Ratio: 2.08%) Ternary : 2030 (Ratio: 0.52%) Conflict : 390850 (Average Length: 338.8 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 390850 (Average: 13.22 Max: 997 Sum: 5165905) Executed : 390771 (Average: 13.21 Max: 997 Sum: 5162453 Ratio: 99.93%) Bounded : 79 (Average: 43.70 Max: 107 Sum: 3452 Ratio: 0.07%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 675734 (Eliminated: 0 Frozen: 212515) Constraints : 4970293 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 777MB Max. Length : 105 steps Models : 1 [endof: stats after solve call] Solving Time: 6.90s Memory: 705MB (+0MB) UNKNOWN Iteration Time: 6.96s Iteration 53 Queue: [(20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)] Grounded Until: 105 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 54 Time : 313.579s (Solving: 291.12s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 313.580s Choices : 5884929 (Domain: 5760570) Conflicts : 398225 (Analyzed: 398222) Restarts : 5008 (Average: 79.52 Last: 163) Model-Level : 299.0 Problems : 54 (Average Length: 72.28 Splits: 0) Lemmas : 398222 (Deleted: 372975) Binary : 8156 (Ratio: 2.05%) Ternary : 2044 (Ratio: 0.51%) Conflict : 398222 (Average Length: 337.5 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 398222 (Average: 13.11 Max: 997 Sum: 5221598) Executed : 398143 (Average: 13.10 Max: 997 Sum: 5218146 Ratio: 99.93%) Bounded : 79 (Average: 43.70 Max: 107 Sum: 3452 Ratio: 0.07%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 675734 (Eliminated: 0 Frozen: 212515) Constraints : 4970293 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 777MB Max. Length : 105 steps Models : 1 [endof: stats after solve call] Solving Time: 6.99s Memory: 705MB (+0MB) UNKNOWN Iteration Time: 7.04s Iteration 54 Queue: [(21,105,1,True), (22,110,0,True), (23,115,0,True)] Grounded Until: 105 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 55 Time : 320.227s (Solving: 297.59s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 320.232s Choices : 6144011 (Domain: 6019156) Conflicts : 405777 (Analyzed: 405774) Restarts : 5108 (Average: 79.44 Last: 163) Model-Level : 299.0 Problems : 55 (Average Length: 72.91 Splits: 0) Lemmas : 405774 (Deleted: 379957) Binary : 8376 (Ratio: 2.06%) Ternary : 2126 (Ratio: 0.52%) Conflict : 405774 (Average Length: 336.0 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 405774 (Average: 13.46 Max: 997 Sum: 5463042) Executed : 405694 (Average: 13.45 Max: 997 Sum: 5459483 Ratio: 99.93%) Bounded : 80 (Average: 44.49 Max: 107 Sum: 3559 Ratio: 0.07%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 675734 (Eliminated: 0 Frozen: 212515) Constraints : 4970293 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 777MB Max. Length : 105 steps Models : 1 [endof: stats after solve call] Solving Time: 6.59s Memory: 705MB (+0MB) UNKNOWN Iteration Time: 6.65s Iteration 55 Queue: [(22,110,0,True), (23,115,0,True)] Grounded Until: 105 Expected Memory: 776.0MB Grounding... [('step', [106]), ('step', [107]), ('step', [108]), ('step', [109]), ('step', [110]), ('check', [110])] Grounding Time: 0.50s Memory: 705MB (+0MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 56 Time : 327.846s (Solving: 304.14s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 327.852s Choices : 6209025 (Domain: 6084169) Conflicts : 413665 (Analyzed: 413662) Restarts : 5208 (Average: 79.43 Last: 163) Model-Level : 299.0 Problems : 56 (Average Length: 73.61 Splits: 0) Lemmas : 413662 (Deleted: 387283) Binary : 8421 (Ratio: 2.04%) Ternary : 2131 (Ratio: 0.52%) Conflict : 413662 (Average Length: 335.9 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 413662 (Average: 13.30 Max: 997 Sum: 5502221) Executed : 413582 (Average: 13.29 Max: 997 Sum: 5498662 Ratio: 99.94%) Bounded : 80 (Average: 44.49 Max: 107 Sum: 3559 Ratio: 0.06%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 708680 (Eliminated: 0 Frozen: 222950) Constraints : 5219852 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 810MB Max. Length : 105 steps Models : 1 [endof: stats after solve call] Solving Time: 6.67s Memory: 738MB (+33MB) UNKNOWN Iteration Time: 7.63s Iteration 56 Queue: [(23,115,0,True)] Grounded Until: 110 Expected Memory: 809.0MB Grounding... [('step', [111]), ('step', [112]), ('step', [113]), ('step', [114]), ('step', [115]), ('check', [115])] Grounding Time: 0.81s Memory: 788MB (+50MB) Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 57 Time : 334.902s (Solving: 309.80s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 334.908s Choices : 6276007 (Domain: 6151149) Conflicts : 421332 (Analyzed: 421329) Restarts : 5308 (Average: 79.38 Last: 163) Model-Level : 299.0 Problems : 57 (Average Length: 74.37 Splits: 0) Lemmas : 421329 (Deleted: 394979) Binary : 8494 (Ratio: 2.02%) Ternary : 2137 (Ratio: 0.51%) Conflict : 421329 (Average Length: 335.3 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 421329 (Average: 13.16 Max: 997 Sum: 5542601) Executed : 421249 (Average: 13.15 Max: 997 Sum: 5539042 Ratio: 99.94%) Bounded : 80 (Average: 44.49 Max: 107 Sum: 3559 Ratio: 0.06%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 741626 (Eliminated: 0 Frozen: 233385) Constraints : 5469437 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 878MB Max. Length : 110 steps Models : 1 [endof: stats after solve call] Solving Time: 5.80s Memory: 792MB (+4MB) UNKNOWN Iteration Time: 7.07s Iteration 57 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,3,False), (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,2,False), (22,110,1,True), (23,115,1,True)] Grounded Until: 115 Blocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 58 Time : 338.541s (Solving: 313.29s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 338.548s Choices : 6328447 (Domain: 6203589) Conflicts : 429022 (Analyzed: 429019) Restarts : 5408 (Average: 79.33 Last: 163) Model-Level : 299.0 Problems : 58 (Average Length: 75.10 Splits: 0) Lemmas : 429019 (Deleted: 402498) Binary : 8544 (Ratio: 1.99%) Ternary : 2143 (Ratio: 0.50%) Conflict : 429019 (Average Length: 333.3 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 429019 (Average: 13.01 Max: 997 Sum: 5583601) Executed : 428939 (Average: 13.01 Max: 997 Sum: 5580042 Ratio: 99.94%) Bounded : 80 (Average: 44.49 Max: 107 Sum: 3559 Ratio: 0.06%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 741626 (Eliminated: 0 Frozen: 233385) Constraints : 5469437 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 878MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 3.59s Memory: 792MB (+0MB) UNKNOWN Iteration Time: 3.64s Iteration 58 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,3,False), (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,2,False), (22,110,1,True), (23,115,1,True)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 59 Time : 342.675s (Solving: 317.26s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 342.684s Choices : 6369183 (Domain: 6244325) Conflicts : 436671 (Analyzed: 436668) Restarts : 5508 (Average: 79.28 Last: 163) Model-Level : 299.0 Problems : 59 (Average Length: 75.81 Splits: 0) Lemmas : 436668 (Deleted: 409924) Binary : 8642 (Ratio: 1.98%) Ternary : 2162 (Ratio: 0.50%) Conflict : 436668 (Average Length: 331.7 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 436668 (Average: 12.87 Max: 997 Sum: 5618311) Executed : 436587 (Average: 12.86 Max: 997 Sum: 5614638 Ratio: 99.93%) Bounded : 81 (Average: 45.35 Max: 114 Sum: 3673 Ratio: 0.07%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 741626 (Eliminated: 0 Frozen: 233385) Constraints : 5469437 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 878MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 4.08s Memory: 792MB (+0MB) UNKNOWN Iteration Time: 4.14s Iteration 59 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,3,False), (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,2,False), (22,110,1,True), (23,115,1,True)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 60 Time : 351.516s (Solving: 325.93s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 351.528s Choices : 6433571 (Domain: 6308178) Conflicts : 444846 (Analyzed: 444843) Restarts : 5608 (Average: 79.32 Last: 163) Model-Level : 299.0 Problems : 60 (Average Length: 76.50 Splits: 0) Lemmas : 444843 (Deleted: 417187) Binary : 8883 (Ratio: 2.00%) Ternary : 2174 (Ratio: 0.49%) Conflict : 444843 (Average Length: 361.6 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 444843 (Average: 12.72 Max: 997 Sum: 5658610) Executed : 444762 (Average: 12.71 Max: 997 Sum: 5654937 Ratio: 99.94%) Bounded : 81 (Average: 45.35 Max: 114 Sum: 3673 Ratio: 0.06%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 741626 (Eliminated: 0 Frozen: 233385) Constraints : 5469437 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 920MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 8.78s Memory: 856MB (+64MB) UNKNOWN Iteration Time: 8.85s Iteration 60 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,3,False), (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,2,False), (22,110,1,True), (23,115,1,True)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 61 Time : 358.105s (Solving: 332.37s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 358.120s Choices : 6517918 (Domain: 6391398) Conflicts : 453308 (Analyzed: 453305) Restarts : 5708 (Average: 79.42 Last: 163) Model-Level : 299.0 Problems : 61 (Average Length: 77.16 Splits: 0) Lemmas : 453305 (Deleted: 424854) Binary : 9026 (Ratio: 1.99%) Ternary : 2210 (Ratio: 0.49%) Conflict : 453305 (Average Length: 361.6 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 453305 (Average: 12.64 Max: 997 Sum: 5731117) Executed : 453224 (Average: 12.63 Max: 997 Sum: 5727444 Ratio: 99.94%) Bounded : 81 (Average: 45.35 Max: 114 Sum: 3673 Ratio: 0.06%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 741626 (Eliminated: 0 Frozen: 233385) Constraints : 5469437 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 920MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 6.54s Memory: 856MB (+0MB) UNKNOWN Iteration Time: 6.59s Iteration 61 Queue: [(8,40,3,True), (9,45,3,True), (10,50,3,True), (11,55,3,False), (12,60,3,False), (13,65,3,False), (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,2,False), (22,110,1,True), (23,115,1,True)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 62 Time : 363.890s (Solving: 338.00s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 363.908s Choices : 6600319 (Domain: 6472834) Conflicts : 461100 (Analyzed: 461097) Restarts : 5808 (Average: 79.39 Last: 163) Model-Level : 299.0 Problems : 62 (Average Length: 77.81 Splits: 0) Lemmas : 461097 (Deleted: 432984) Binary : 9160 (Ratio: 1.99%) Ternary : 2238 (Ratio: 0.49%) Conflict : 461097 (Average Length: 362.0 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 461097 (Average: 12.58 Max: 997 Sum: 5801968) Executed : 461015 (Average: 12.57 Max: 997 Sum: 5798178 Ratio: 99.93%) Bounded : 82 (Average: 46.22 Max: 117 Sum: 3790 Ratio: 0.07%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 741626 (Eliminated: 0 Frozen: 233385) Constraints : 5469437 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 920MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 5.74s Memory: 856MB (+0MB) UNKNOWN Iteration Time: 5.79s Iteration 62 Queue: [(9,45,3,True), (10,50,3,True), (11,55,3,False), (12,60,3,False), (13,65,3,False), (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,2,False), (22,110,1,True), (23,115,1,True)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 63 Time : 372.012s (Solving: 345.95s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 372.032s Choices : 6723313 (Domain: 6593706) Conflicts : 469845 (Analyzed: 469842) Restarts : 5908 (Average: 79.53 Last: 163) Model-Level : 299.0 Problems : 63 (Average Length: 78.43 Splits: 0) Lemmas : 469842 (Deleted: 442434) Binary : 9297 (Ratio: 1.98%) Ternary : 2275 (Ratio: 0.48%) Conflict : 469842 (Average Length: 363.8 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 469842 (Average: 12.58 Max: 997 Sum: 5910302) Executed : 469760 (Average: 12.57 Max: 997 Sum: 5906512 Ratio: 99.94%) Bounded : 82 (Average: 46.22 Max: 117 Sum: 3790 Ratio: 0.06%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 741626 (Eliminated: 0 Frozen: 233385) Constraints : 5469411 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 920MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 8.06s Memory: 856MB (+0MB) UNKNOWN Iteration Time: 8.13s Iteration 63 Queue: [(10,50,3,True), (11,55,3,False), (12,60,3,False), (13,65,3,False), (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,2,False), (22,110,1,True), (23,115,1,True)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 64 Time : 378.419s (Solving: 352.18s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 378.440s Choices : 6817284 (Domain: 6686907) Conflicts : 478064 (Analyzed: 478061) Restarts : 6008 (Average: 79.57 Last: 163) Model-Level : 299.0 Problems : 64 (Average Length: 79.03 Splits: 0) Lemmas : 478061 (Deleted: 448784) Binary : 9373 (Ratio: 1.96%) Ternary : 2305 (Ratio: 0.48%) Conflict : 478061 (Average Length: 363.0 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 478061 (Average: 12.54 Max: 997 Sum: 5992960) Executed : 477978 (Average: 12.53 Max: 997 Sum: 5989055 Ratio: 99.93%) Bounded : 83 (Average: 47.05 Max: 117 Sum: 3905 Ratio: 0.07%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 741626 (Eliminated: 0 Frozen: 233385) Constraints : 5469411 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 920MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 6.35s Memory: 856MB (+0MB) UNKNOWN Iteration Time: 6.41s 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,2,False), (22,110,1,True), (23,115,1,True)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 65 Time : 385.396s (Solving: 359.01s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 385.424s Choices : 6988181 (Domain: 6856733) Conflicts : 486717 (Analyzed: 486714) Restarts : 6108 (Average: 79.68 Last: 163) Model-Level : 299.0 Problems : 65 (Average Length: 79.62 Splits: 0) Lemmas : 486714 (Deleted: 458721) Binary : 9563 (Ratio: 1.96%) Ternary : 2340 (Ratio: 0.48%) Conflict : 486714 (Average Length: 363.0 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 486714 (Average: 12.63 Max: 997 Sum: 6148623) Executed : 486631 (Average: 12.62 Max: 997 Sum: 6144718 Ratio: 99.94%) Bounded : 83 (Average: 47.05 Max: 117 Sum: 3905 Ratio: 0.06%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 741626 (Eliminated: 0 Frozen: 233385) Constraints : 5469411 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 920MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 6.93s Memory: 856MB (+0MB) UNKNOWN Iteration Time: 6.98s 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,2,False), (22,110,1,True), (23,115,1,True)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 66 Time : 392.217s (Solving: 365.66s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 392.248s Choices : 7164957 (Domain: 7032561) Conflicts : 494718 (Analyzed: 494715) Restarts : 6208 (Average: 79.69 Last: 163) Model-Level : 299.0 Problems : 66 (Average Length: 80.18 Splits: 0) Lemmas : 494715 (Deleted: 464891) Binary : 9691 (Ratio: 1.96%) Ternary : 2360 (Ratio: 0.48%) Conflict : 494715 (Average Length: 362.9 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 494715 (Average: 12.75 Max: 997 Sum: 6309346) Executed : 494631 (Average: 12.75 Max: 997 Sum: 6305327 Ratio: 99.94%) Bounded : 84 (Average: 47.85 Max: 117 Sum: 4019 Ratio: 0.06%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 741626 (Eliminated: 0 Frozen: 233385) Constraints : 5469411 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 920MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 6.76s Memory: 856MB (+0MB) UNKNOWN Iteration Time: 6.83s Iteration 66 Queue: [(22,110,1,True), (23,115,1,True)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 67 Time : 402.579s (Solving: 375.83s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 402.616s Choices : 7578162 (Domain: 7444499) Conflicts : 503490 (Analyzed: 503487) Restarts : 6308 (Average: 79.82 Last: 163) Model-Level : 299.0 Problems : 67 (Average Length: 80.73 Splits: 0) Lemmas : 503487 (Deleted: 474677) Binary : 9833 (Ratio: 1.95%) Ternary : 2388 (Ratio: 0.47%) Conflict : 503487 (Average Length: 364.4 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 503487 (Average: 13.30 Max: 1049 Sum: 6698011) Executed : 503403 (Average: 13.30 Max: 1049 Sum: 6693992 Ratio: 99.94%) Bounded : 84 (Average: 47.85 Max: 117 Sum: 4019 Ratio: 0.06%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 741626 (Eliminated: 0 Frozen: 233385) Constraints : 5469411 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 920MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 10.29s Memory: 856MB (+0MB) UNKNOWN Iteration Time: 10.37s Iteration 67 Queue: [(23,115,1,True)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 68 Time : 411.842s (Solving: 384.92s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 411.884s Choices : 7908681 (Domain: 7773549) Conflicts : 512509 (Analyzed: 512506) Restarts : 6408 (Average: 79.98 Last: 163) Model-Level : 299.0 Problems : 68 (Average Length: 81.26 Splits: 0) Lemmas : 512506 (Deleted: 483059) Binary : 9974 (Ratio: 1.95%) Ternary : 2405 (Ratio: 0.47%) Conflict : 512506 (Average Length: 366.2 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 512506 (Average: 13.66 Max: 1061 Sum: 7002779) Executed : 512422 (Average: 13.66 Max: 1061 Sum: 6998760 Ratio: 99.94%) Bounded : 84 (Average: 47.85 Max: 117 Sum: 4019 Ratio: 0.06%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 741626 (Eliminated: 0 Frozen: 233385) Constraints : 5469411 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 920MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 9.20s Memory: 856MB (+0MB) UNKNOWN Iteration Time: 9.27s Iteration 68 Queue: [(4,20,5,True), (5,25,5,True), (6,30,5,True), (7,35,4,True), (8,40,4,True), (9,45,4,True), (10,50,4,False), (11,55,3,True), (12,60,3,True), (13,65,3,False), (14,70,3,False), (15,75,3,False), (16,80,2,True), (17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] Grounded Until: 115 Blocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 69 Time : 415.386s (Solving: 388.31s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 415.428s Choices : 7951180 (Domain: 7816048) Conflicts : 519956 (Analyzed: 519953) Restarts : 6508 (Average: 79.89 Last: 163) Model-Level : 299.0 Problems : 69 (Average Length: 81.78 Splits: 0) Lemmas : 519953 (Deleted: 489708) Binary : 9991 (Ratio: 1.92%) Ternary : 2408 (Ratio: 0.46%) Conflict : 519953 (Average Length: 365.8 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 519953 (Average: 13.53 Max: 1061 Sum: 7034105) Executed : 519868 (Average: 13.52 Max: 1061 Sum: 7030085 Ratio: 99.94%) Bounded : 85 (Average: 47.29 Max: 117 Sum: 4020 Ratio: 0.06%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 741626 (Eliminated: 0 Frozen: 233385) Constraints : 5469411 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 920MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 3.49s Memory: 856MB (+0MB) UNKNOWN Iteration Time: 3.55s 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,False), (11,55,3,True), (12,60,3,True), (13,65,3,False), (14,70,3,False), (15,75,3,False), (16,80,2,True), (17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 70 Time : 421.018s (Solving: 393.76s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 421.064s Choices : 7992848 (Domain: 7857716) Conflicts : 527899 (Analyzed: 527896) Restarts : 6608 (Average: 79.89 Last: 163) Model-Level : 299.0 Problems : 70 (Average Length: 82.29 Splits: 0) Lemmas : 527896 (Deleted: 496985) Binary : 10010 (Ratio: 1.90%) Ternary : 2423 (Ratio: 0.46%) Conflict : 527896 (Average Length: 366.7 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 527896 (Average: 13.39 Max: 1061 Sum: 7066902) Executed : 527811 (Average: 13.38 Max: 1061 Sum: 7062882 Ratio: 99.94%) Bounded : 85 (Average: 47.29 Max: 117 Sum: 4020 Ratio: 0.06%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 741626 (Eliminated: 0 Frozen: 233385) Constraints : 5469411 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 920MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 5.56s Memory: 856MB (+0MB) UNKNOWN Iteration Time: 5.64s Iteration 70 Queue: [(6,30,5,True), (7,35,4,True), (8,40,4,True), (9,45,4,True), (10,50,4,False), (11,55,3,True), (12,60,3,True), (13,65,3,False), (14,70,3,False), (15,75,3,False), (16,80,2,True), (17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 71 Time : 429.231s (Solving: 401.82s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 429.280s Choices : 8056715 (Domain: 7920866) Conflicts : 535774 (Analyzed: 535771) Restarts : 6708 (Average: 79.87 Last: 163) Model-Level : 299.0 Problems : 71 (Average Length: 82.77 Splits: 0) Lemmas : 535771 (Deleted: 504725) Binary : 10159 (Ratio: 1.90%) Ternary : 2448 (Ratio: 0.46%) Conflict : 535771 (Average Length: 379.0 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 535771 (Average: 13.28 Max: 1061 Sum: 7112400) Executed : 535686 (Average: 13.27 Max: 1061 Sum: 7108380 Ratio: 99.94%) Bounded : 85 (Average: 47.29 Max: 117 Sum: 4020 Ratio: 0.06%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 741626 (Eliminated: 0 Frozen: 233385) Constraints : 5469411 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 920MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 8.17s Memory: 856MB (+0MB) UNKNOWN Iteration Time: 8.22s Iteration 71 Queue: [(7,35,4,True), (8,40,4,True), (9,45,4,True), (10,50,4,False), (11,55,3,True), (12,60,3,True), (13,65,3,False), (14,70,3,False), (15,75,3,False), (16,80,2,True), (17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 72 Time : 434.347s (Solving: 406.76s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 434.400s Choices : 8114514 (Domain: 7978471) Conflicts : 544053 (Analyzed: 544050) Restarts : 6808 (Average: 79.91 Last: 163) Model-Level : 299.0 Problems : 72 (Average Length: 83.25 Splits: 0) Lemmas : 544050 (Deleted: 512264) Binary : 10225 (Ratio: 1.88%) Ternary : 2475 (Ratio: 0.45%) Conflict : 544050 (Average Length: 378.1 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 544050 (Average: 13.16 Max: 1061 Sum: 7161375) Executed : 543965 (Average: 13.16 Max: 1061 Sum: 7157355 Ratio: 99.94%) Bounded : 85 (Average: 47.29 Max: 117 Sum: 4020 Ratio: 0.06%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 741626 (Eliminated: 0 Frozen: 233385) Constraints : 5469411 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 920MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 5.05s Memory: 856MB (+0MB) UNKNOWN Iteration Time: 5.12s Iteration 72 Queue: [(8,40,4,True), (9,45,4,True), (10,50,4,False), (11,55,3,True), (12,60,3,True), (13,65,3,False), (14,70,3,False), (15,75,3,False), (16,80,2,True), (17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 73 Time : 442.708s (Solving: 414.97s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 442.764s Choices : 8232020 (Domain: 8094712) Conflicts : 553427 (Analyzed: 553424) Restarts : 6908 (Average: 80.11 Last: 163) Model-Level : 299.0 Problems : 73 (Average Length: 83.71 Splits: 0) Lemmas : 553424 (Deleted: 522427) Binary : 10338 (Ratio: 1.87%) Ternary : 2490 (Ratio: 0.45%) Conflict : 553424 (Average Length: 380.6 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 553424 (Average: 13.13 Max: 1061 Sum: 7265288) Executed : 553339 (Average: 13.12 Max: 1061 Sum: 7261268 Ratio: 99.94%) Bounded : 85 (Average: 47.29 Max: 117 Sum: 4020 Ratio: 0.06%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 741626 (Eliminated: 0 Frozen: 233385) Constraints : 5469411 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 920MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 8.31s Memory: 856MB (+0MB) UNKNOWN Iteration Time: 8.37s Iteration 73 Queue: [(9,45,4,True), (10,50,4,False), (11,55,3,True), (12,60,3,True), (13,65,3,False), (14,70,3,False), (15,75,3,False), (16,80,2,True), (17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 74 Time : 450.963s (Solving: 423.07s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 451.024s Choices : 8354090 (Domain: 8215719) Conflicts : 562473 (Analyzed: 562470) Restarts : 7008 (Average: 80.26 Last: 163) Model-Level : 299.0 Problems : 74 (Average Length: 84.16 Splits: 0) Lemmas : 562470 (Deleted: 531405) Binary : 10430 (Ratio: 1.85%) Ternary : 2514 (Ratio: 0.45%) Conflict : 562470 (Average Length: 384.7 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 562470 (Average: 13.10 Max: 1061 Sum: 7370995) Executed : 562385 (Average: 13.10 Max: 1061 Sum: 7366975 Ratio: 99.95%) Bounded : 85 (Average: 47.29 Max: 117 Sum: 4020 Ratio: 0.05%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 741626 (Eliminated: 0 Frozen: 233385) Constraints : 5469411 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 920MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 8.20s Memory: 856MB (+0MB) UNKNOWN Iteration Time: 8.26s Iteration 74 Queue: [(11,55,3,True), (12,60,3,True), (13,65,3,False), (14,70,3,False), (15,75,3,False), (16,80,2,True), (17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 75 Time : 457.000s (Solving: 428.93s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 457.064s Choices : 8446708 (Domain: 8307906) Conflicts : 570682 (Analyzed: 570679) Restarts : 7108 (Average: 80.29 Last: 163) Model-Level : 299.0 Problems : 75 (Average Length: 84.60 Splits: 0) Lemmas : 570679 (Deleted: 538109) Binary : 10479 (Ratio: 1.84%) Ternary : 2539 (Ratio: 0.44%) Conflict : 570679 (Average Length: 384.9 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 570679 (Average: 13.05 Max: 1061 Sum: 7450057) Executed : 570593 (Average: 13.05 Max: 1061 Sum: 7445920 Ratio: 99.94%) Bounded : 86 (Average: 48.10 Max: 117 Sum: 4137 Ratio: 0.06%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 741626 (Eliminated: 0 Frozen: 233385) Constraints : 5469411 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 920MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 5.97s Memory: 856MB (+0MB) UNKNOWN Iteration Time: 6.04s Iteration 75 Queue: [(12,60,3,True), (13,65,3,False), (14,70,3,False), (15,75,3,False), (16,80,2,True), (17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 76 Time : 465.712s (Solving: 437.48s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 465.780s Choices : 8603533 (Domain: 8463694) Conflicts : 579356 (Analyzed: 579353) Restarts : 7208 (Average: 80.38 Last: 163) Model-Level : 299.0 Problems : 76 (Average Length: 85.03 Splits: 0) Lemmas : 579353 (Deleted: 548109) Binary : 10671 (Ratio: 1.84%) Ternary : 2578 (Ratio: 0.44%) Conflict : 579353 (Average Length: 392.3 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 579353 (Average: 13.09 Max: 1061 Sum: 7586145) Executed : 579267 (Average: 13.09 Max: 1061 Sum: 7582008 Ratio: 99.95%) Bounded : 86 (Average: 48.10 Max: 117 Sum: 4137 Ratio: 0.05%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 741626 (Eliminated: 0 Frozen: 233385) Constraints : 5469397 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 920MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 8.66s Memory: 856MB (+0MB) UNKNOWN Iteration Time: 8.72s Iteration 76 Queue: [(16,80,2,True), (17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 77 Time : 472.718s (Solving: 444.32s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 472.788s Choices : 8748240 (Domain: 8607993) Conflicts : 587505 (Analyzed: 587502) Restarts : 7308 (Average: 80.39 Last: 163) Model-Level : 299.0 Problems : 77 (Average Length: 85.44 Splits: 0) Lemmas : 587502 (Deleted: 554308) Binary : 10735 (Ratio: 1.83%) Ternary : 2587 (Ratio: 0.44%) Conflict : 587502 (Average Length: 391.3 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 587502 (Average: 13.13 Max: 1061 Sum: 7716222) Executed : 587416 (Average: 13.13 Max: 1061 Sum: 7712085 Ratio: 99.95%) Bounded : 86 (Average: 48.10 Max: 117 Sum: 4137 Ratio: 0.05%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 741626 (Eliminated: 0 Frozen: 233385) Constraints : 5469397 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 920MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 6.95s Memory: 856MB (+0MB) UNKNOWN Iteration Time: 7.01s Iteration 77 Queue: [(17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 78 Time : 481.367s (Solving: 452.82s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 481.440s Choices : 8959153 (Domain: 8818423) Conflicts : 595693 (Analyzed: 595690) Restarts : 7408 (Average: 80.41 Last: 163) Model-Level : 299.0 Problems : 78 (Average Length: 85.85 Splits: 0) Lemmas : 595690 (Deleted: 562132) Binary : 10885 (Ratio: 1.83%) Ternary : 2616 (Ratio: 0.44%) Conflict : 595690 (Average Length: 394.2 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 595690 (Average: 13.27 Max: 1061 Sum: 7906025) Executed : 595603 (Average: 13.26 Max: 1061 Sum: 7901773 Ratio: 99.95%) Bounded : 87 (Average: 48.87 Max: 117 Sum: 4252 Ratio: 0.05%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 741626 (Eliminated: 0 Frozen: 233385) Constraints : 5469397 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 920MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 8.60s Memory: 856MB (+0MB) UNKNOWN Iteration Time: 8.66s Iteration 78 Queue: [(4,20,6,True), (5,25,6,True), (6,30,6,True), (7,35,5,True), (8,40,5,True), (9,45,5,False), (10,50,4,True), (11,55,4,False), (12,60,4,False), (13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,3,False), (17,85,3,False), (18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] Grounded Until: 115 Blocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 79 Time : 484.540s (Solving: 455.83s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 484.612s Choices : 9014989 (Domain: 8874259) Conflicts : 603499 (Analyzed: 603496) Restarts : 7508 (Average: 80.38 Last: 163) Model-Level : 299.0 Problems : 79 (Average Length: 86.24 Splits: 0) Lemmas : 603496 (Deleted: 570074) Binary : 10931 (Ratio: 1.81%) Ternary : 2628 (Ratio: 0.44%) Conflict : 603496 (Average Length: 392.8 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 603496 (Average: 13.18 Max: 1061 Sum: 7952379) Executed : 603409 (Average: 13.17 Max: 1061 Sum: 7948127 Ratio: 99.95%) Bounded : 87 (Average: 48.87 Max: 117 Sum: 4252 Ratio: 0.05%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 741626 (Eliminated: 0 Frozen: 233385) Constraints : 5469397 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 920MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 3.12s Memory: 856MB (+0MB) UNKNOWN Iteration Time: 3.18s Iteration 79 Queue: [(5,25,6,True), (6,30,6,True), (7,35,5,True), (8,40,5,True), (9,45,5,False), (10,50,4,True), (11,55,4,False), (12,60,4,False), (13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,3,False), (17,85,3,False), (18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 80 Time : 490.266s (Solving: 461.41s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 490.340s Choices : 9060734 (Domain: 8920004) Conflicts : 611543 (Analyzed: 611540) Restarts : 7608 (Average: 80.38 Last: 163) Model-Level : 299.0 Problems : 80 (Average Length: 86.62 Splits: 0) Lemmas : 611540 (Deleted: 577691) Binary : 10950 (Ratio: 1.79%) Ternary : 2636 (Ratio: 0.43%) Conflict : 611540 (Average Length: 393.3 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 611540 (Average: 13.06 Max: 1061 Sum: 7989493) Executed : 611453 (Average: 13.06 Max: 1061 Sum: 7985241 Ratio: 99.95%) Bounded : 87 (Average: 48.87 Max: 117 Sum: 4252 Ratio: 0.05%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 741626 (Eliminated: 0 Frozen: 233385) Constraints : 5469397 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 920MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 5.68s Memory: 856MB (+0MB) UNKNOWN Iteration Time: 5.73s Iteration 80 Queue: [(6,30,6,True), (7,35,5,True), (8,40,5,True), (9,45,5,False), (10,50,4,True), (11,55,4,False), (12,60,4,False), (13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,3,False), (17,85,3,False), (18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 81 Time : 497.922s (Solving: 468.90s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 498.000s Choices : 9132881 (Domain: 8991803) Conflicts : 619920 (Analyzed: 619917) Restarts : 7708 (Average: 80.43 Last: 163) Model-Level : 299.0 Problems : 81 (Average Length: 87.00 Splits: 0) Lemmas : 619917 (Deleted: 585408) Binary : 11071 (Ratio: 1.79%) Ternary : 2661 (Ratio: 0.43%) Conflict : 619917 (Average Length: 401.0 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 619917 (Average: 12.97 Max: 1061 Sum: 8041738) Executed : 619830 (Average: 12.97 Max: 1061 Sum: 8037486 Ratio: 99.95%) Bounded : 87 (Average: 48.87 Max: 117 Sum: 4252 Ratio: 0.05%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 741626 (Eliminated: 0 Frozen: 233385) Constraints : 5469397 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 920MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 7.60s Memory: 856MB (+0MB) UNKNOWN Iteration Time: 7.66s Iteration 81 Queue: [(7,35,5,True), (8,40,5,True), (9,45,5,False), (10,50,4,True), (11,55,4,False), (12,60,4,False), (13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,3,False), (17,85,3,False), (18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 82 Time : 504.559s (Solving: 475.34s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 504.640s Choices : 9216235 (Domain: 9074579) Conflicts : 628811 (Analyzed: 628808) Restarts : 7808 (Average: 80.53 Last: 163) Model-Level : 299.0 Problems : 82 (Average Length: 87.37 Splits: 0) Lemmas : 628808 (Deleted: 595666) Binary : 11185 (Ratio: 1.78%) Ternary : 2678 (Ratio: 0.43%) Conflict : 628808 (Average Length: 401.7 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 628808 (Average: 12.90 Max: 1061 Sum: 8112256) Executed : 628721 (Average: 12.89 Max: 1061 Sum: 8108004 Ratio: 99.95%) Bounded : 87 (Average: 48.87 Max: 117 Sum: 4252 Ratio: 0.05%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 741626 (Eliminated: 0 Frozen: 233385) Constraints : 5469397 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 920MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 6.56s Memory: 856MB (+0MB) UNKNOWN Iteration Time: 6.64s Iteration 82 Queue: [(8,40,5,True), (9,45,5,False), (10,50,4,True), (11,55,4,False), (12,60,4,False), (13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,3,False), (17,85,3,False), (18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 83 Time : 511.966s (Solving: 482.59s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 512.052s Choices : 9311376 (Domain: 9168059) Conflicts : 637517 (Analyzed: 637514) Restarts : 7908 (Average: 80.62 Last: 163) Model-Level : 299.0 Problems : 83 (Average Length: 87.72 Splits: 0) Lemmas : 637514 (Deleted: 604069) Binary : 11415 (Ratio: 1.79%) Ternary : 2752 (Ratio: 0.43%) Conflict : 637514 (Average Length: 405.3 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 637514 (Average: 12.84 Max: 1061 Sum: 8188632) Executed : 637427 (Average: 12.84 Max: 1061 Sum: 8184380 Ratio: 99.95%) Bounded : 87 (Average: 48.87 Max: 117 Sum: 4252 Ratio: 0.05%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 741626 (Eliminated: 0 Frozen: 233385) Constraints : 5469397 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 920MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 7.35s Memory: 856MB (+0MB) UNKNOWN Iteration Time: 7.41s Iteration 83 Queue: [(10,50,4,True), (11,55,4,False), (12,60,4,False), (13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,3,False), (17,85,3,False), (18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 84 Time : 518.429s (Solving: 488.90s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 518.520s Choices : 9416164 (Domain: 9272448) Conflicts : 645741 (Analyzed: 645738) Restarts : 8008 (Average: 80.64 Last: 169) Model-Level : 299.0 Problems : 84 (Average Length: 88.07 Splits: 0) Lemmas : 645738 (Deleted: 610213) Binary : 11506 (Ratio: 1.78%) Ternary : 2803 (Ratio: 0.43%) Conflict : 645738 (Average Length: 405.4 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 645738 (Average: 12.82 Max: 1061 Sum: 8280530) Executed : 645651 (Average: 12.82 Max: 1061 Sum: 8276278 Ratio: 99.95%) Bounded : 87 (Average: 48.87 Max: 117 Sum: 4252 Ratio: 0.05%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 741626 (Eliminated: 0 Frozen: 233385) Constraints : 5469397 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 920MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 6.42s Memory: 856MB (+0MB) UNKNOWN Iteration Time: 6.47s Iteration 84 Queue: [(13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,3,False), (17,85,3,False), (18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 85 Time : 525.176s (Solving: 495.49s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 525.272s Choices : 9531679 (Domain: 9387663) Conflicts : 653642 (Analyzed: 653639) Restarts : 8108 (Average: 80.62 Last: 169) Model-Level : 299.0 Problems : 85 (Average Length: 88.41 Splits: 0) Lemmas : 653639 (Deleted: 618229) Binary : 11549 (Ratio: 1.77%) Ternary : 2816 (Ratio: 0.43%) Conflict : 653639 (Average Length: 408.0 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 653639 (Average: 12.82 Max: 1061 Sum: 8377378) Executed : 653551 (Average: 12.81 Max: 1061 Sum: 8373009 Ratio: 99.95%) Bounded : 88 (Average: 49.65 Max: 117 Sum: 4369 Ratio: 0.05%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 741626 (Eliminated: 0 Frozen: 233385) Constraints : 5469397 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 920MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 6.70s Memory: 856MB (+0MB) UNKNOWN Iteration Time: 6.75s Iteration 85 Queue: [(18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 86 Time : 535.133s (Solving: 505.30s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 535.236s Choices : 9815379 (Domain: 9670578) Conflicts : 662724 (Analyzed: 662721) Restarts : 8208 (Average: 80.74 Last: 169) Model-Level : 299.0 Problems : 86 (Average Length: 88.74 Splits: 0) Lemmas : 662721 (Deleted: 627991) Binary : 11775 (Ratio: 1.78%) Ternary : 2887 (Ratio: 0.44%) Conflict : 662721 (Average Length: 412.2 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 662721 (Average: 13.02 Max: 1061 Sum: 8631888) Executed : 662633 (Average: 13.02 Max: 1061 Sum: 8627519 Ratio: 99.95%) Bounded : 88 (Average: 49.65 Max: 117 Sum: 4369 Ratio: 0.05%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 741626 (Eliminated: 0 Frozen: 233385) Constraints : 5469383 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 920MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 9.91s Memory: 856MB (+0MB) UNKNOWN Iteration Time: 9.96s Iteration 86 Queue: [(4,20,7,True), (5,25,7,True), (6,30,7,False), (7,35,6,True), (8,40,6,False), (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,True), (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)] Grounded Until: 115 Blocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 87 Time : 538.456s (Solving: 508.46s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 538.560s Choices : 9869261 (Domain: 9724460) Conflicts : 670197 (Analyzed: 670194) Restarts : 8308 (Average: 80.67 Last: 169) Model-Level : 299.0 Problems : 87 (Average Length: 89.07 Splits: 0) Lemmas : 670194 (Deleted: 634677) Binary : 11814 (Ratio: 1.76%) Ternary : 2903 (Ratio: 0.43%) Conflict : 670194 (Average Length: 409.8 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 670194 (Average: 12.94 Max: 1061 Sum: 8670872) Executed : 670106 (Average: 12.93 Max: 1061 Sum: 8666503 Ratio: 99.95%) Bounded : 88 (Average: 49.65 Max: 117 Sum: 4369 Ratio: 0.05%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 741626 (Eliminated: 0 Frozen: 233385) Constraints : 5469383 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 920MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 3.26s Memory: 856MB (+0MB) UNKNOWN Iteration Time: 3.33s Iteration 87 Queue: [(5,25,7,True), (6,30,7,False), (7,35,6,True), (8,40,6,False), (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,True), (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)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 88 Time : 544.130s (Solving: 513.98s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 544.236s Choices : 9909142 (Domain: 9764341) Conflicts : 678276 (Analyzed: 678273) Restarts : 8408 (Average: 80.67 Last: 169) Model-Level : 299.0 Problems : 88 (Average Length: 89.39 Splits: 0) Lemmas : 678273 (Deleted: 641987) Binary : 11825 (Ratio: 1.74%) Ternary : 2903 (Ratio: 0.43%) Conflict : 678273 (Average Length: 410.1 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 678273 (Average: 12.83 Max: 1061 Sum: 8702363) Executed : 678185 (Average: 12.82 Max: 1061 Sum: 8697994 Ratio: 99.95%) Bounded : 88 (Average: 49.65 Max: 117 Sum: 4369 Ratio: 0.05%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 741626 (Eliminated: 0 Frozen: 233385) Constraints : 5469383 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 920MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 5.62s Memory: 856MB (+0MB) UNKNOWN Iteration Time: 5.68s Iteration 88 Queue: [(7,35,6,True), (8,40,6,False), (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,True), (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)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 89 Time : 550.688s (Solving: 520.38s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 550.796s Choices : 9973712 (Domain: 9828423) Conflicts : 686216 (Analyzed: 686213) Restarts : 8508 (Average: 80.66 Last: 169) Model-Level : 299.0 Problems : 89 (Average Length: 89.70 Splits: 0) Lemmas : 686213 (Deleted: 649875) Binary : 11917 (Ratio: 1.74%) Ternary : 2937 (Ratio: 0.43%) Conflict : 686213 (Average Length: 413.8 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 686213 (Average: 12.75 Max: 1061 Sum: 8751069) Executed : 686125 (Average: 12.75 Max: 1061 Sum: 8746700 Ratio: 99.95%) Bounded : 88 (Average: 49.65 Max: 117 Sum: 4369 Ratio: 0.05%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 741626 (Eliminated: 0 Frozen: 233385) Constraints : 5469383 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 920MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 6.51s Memory: 856MB (+0MB) UNKNOWN Iteration Time: 6.56s Iteration 89 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,True), (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)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 90 Time : 557.375s (Solving: 526.91s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 557.484s Choices : 10064390 (Domain: 9918062) Conflicts : 694954 (Analyzed: 694951) Restarts : 8608 (Average: 80.73 Last: 169) Model-Level : 299.0 Problems : 90 (Average Length: 90.00 Splits: 0) Lemmas : 694951 (Deleted: 659617) Binary : 12018 (Ratio: 1.73%) Ternary : 2971 (Ratio: 0.43%) Conflict : 694951 (Average Length: 414.0 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 694951 (Average: 12.70 Max: 1061 Sum: 8827610) Executed : 694863 (Average: 12.70 Max: 1061 Sum: 8823241 Ratio: 99.95%) Bounded : 88 (Average: 49.65 Max: 117 Sum: 4369 Ratio: 0.05%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 741626 (Eliminated: 0 Frozen: 233385) Constraints : 5469383 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 920MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 6.63s Memory: 856MB (+0MB) UNKNOWN Iteration Time: 6.69s Iteration 90 Queue: [(11,55,4,True), (12,60,4,False), (13,65,4,False), (14,70,3,True), (15,75,3,True), (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)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 91 Time : 563.827s (Solving: 533.21s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 563.940s Choices : 10165054 (Domain: 10018521) Conflicts : 703186 (Analyzed: 703183) Restarts : 8708 (Average: 80.75 Last: 169) Model-Level : 299.0 Problems : 91 (Average Length: 90.30 Splits: 0) Lemmas : 703183 (Deleted: 665943) Binary : 12102 (Ratio: 1.72%) Ternary : 3006 (Ratio: 0.43%) Conflict : 703183 (Average Length: 414.4 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 703183 (Average: 12.68 Max: 1061 Sum: 8913228) Executed : 703094 (Average: 12.67 Max: 1061 Sum: 8908742 Ratio: 99.95%) Bounded : 89 (Average: 50.40 Max: 117 Sum: 4486 Ratio: 0.05%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 741626 (Eliminated: 0 Frozen: 233385) Constraints : 5469383 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 920MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 6.40s Memory: 856MB (+0MB) UNKNOWN Iteration Time: 6.46s Iteration 91 Queue: [(14,70,3,True), (15,75,3,True), (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)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 92 Time : 571.781s (Solving: 541.01s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 571.896s Choices : 10307140 (Domain: 10160217) Conflicts : 711465 (Analyzed: 711462) Restarts : 8808 (Average: 80.77 Last: 169) Model-Level : 299.0 Problems : 92 (Average Length: 90.59 Splits: 0) Lemmas : 711462 (Deleted: 673901) Binary : 12192 (Ratio: 1.71%) Ternary : 3017 (Ratio: 0.42%) Conflict : 711462 (Average Length: 417.2 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 711462 (Average: 12.70 Max: 1061 Sum: 9034933) Executed : 711373 (Average: 12.69 Max: 1061 Sum: 9030447 Ratio: 99.95%) Bounded : 89 (Average: 50.40 Max: 117 Sum: 4486 Ratio: 0.05%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 741626 (Eliminated: 0 Frozen: 233385) Constraints : 5469369 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 920MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 7.91s Memory: 856MB (+0MB) UNKNOWN Iteration Time: 7.96s Iteration 92 Queue: [(15,75,3,True), (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)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 93 Time : 578.560s (Solving: 547.62s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 578.680s Choices : 10451910 (Domain: 10304558) Conflicts : 719756 (Analyzed: 719753) Restarts : 8908 (Average: 80.80 Last: 169) Model-Level : 299.0 Problems : 93 (Average Length: 90.87 Splits: 0) Lemmas : 719753 (Deleted: 681847) Binary : 12273 (Ratio: 1.71%) Ternary : 3040 (Ratio: 0.42%) Conflict : 719753 (Average Length: 417.2 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 719753 (Average: 12.73 Max: 1061 Sum: 9162253) Executed : 719664 (Average: 12.72 Max: 1061 Sum: 9157767 Ratio: 99.95%) Bounded : 89 (Average: 50.40 Max: 117 Sum: 4486 Ratio: 0.05%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 741626 (Eliminated: 0 Frozen: 233385) Constraints : 5469369 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 920MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 6.72s Memory: 856MB (+0MB) UNKNOWN Iteration Time: 6.78s Iteration 93 Queue: [(19,95,2,True), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 94 Time : 586.993s (Solving: 555.91s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 587.116s Choices : 10669146 (Domain: 10520582) Conflicts : 728368 (Analyzed: 728365) Restarts : 9008 (Average: 80.86 Last: 169) Model-Level : 299.0 Problems : 94 (Average Length: 91.15 Splits: 0) Lemmas : 728365 (Deleted: 692085) Binary : 12359 (Ratio: 1.70%) Ternary : 3058 (Ratio: 0.42%) Conflict : 728365 (Average Length: 419.4 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 728365 (Average: 12.84 Max: 1061 Sum: 9353812) Executed : 728275 (Average: 12.84 Max: 1061 Sum: 9349209 Ratio: 99.95%) Bounded : 90 (Average: 51.14 Max: 117 Sum: 4603 Ratio: 0.05%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 741626 (Eliminated: 0 Frozen: 233385) Constraints : 5469369 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 920MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 8.39s Memory: 856MB (+0MB) UNKNOWN Iteration Time: 8.44s Iteration 94 Queue: [(4,20,8,True), (5,25,8,True), (6,30,7,True), (7,35,7,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,4,False), (16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,True), (22,110,2,False), (23,115,2,False)] Grounded Until: 115 Blocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 95 Time : 590.827s (Solving: 559.57s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 590.952s Choices : 10719133 (Domain: 10570569) Conflicts : 736179 (Analyzed: 736176) Restarts : 9108 (Average: 80.83 Last: 169) Model-Level : 299.0 Problems : 95 (Average Length: 91.42 Splits: 0) Lemmas : 736176 (Deleted: 698316) Binary : 12416 (Ratio: 1.69%) Ternary : 3067 (Ratio: 0.42%) Conflict : 736176 (Average Length: 418.0 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 736176 (Average: 12.76 Max: 1061 Sum: 9391263) Executed : 736086 (Average: 12.75 Max: 1061 Sum: 9386660 Ratio: 99.95%) Bounded : 90 (Average: 51.14 Max: 117 Sum: 4603 Ratio: 0.05%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 741626 (Eliminated: 0 Frozen: 233385) Constraints : 5469343 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 920MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 3.77s Memory: 856MB (+0MB) UNKNOWN Iteration Time: 3.84s Iteration 95 Queue: [(5,25,8,True), (6,30,7,True), (7,35,7,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,4,False), (16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,True), (22,110,2,False), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 96 Time : 597.207s (Solving: 565.80s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 597.332s Choices : 10761171 (Domain: 10612607) Conflicts : 744423 (Analyzed: 744420) Restarts : 9208 (Average: 80.84 Last: 169) Model-Level : 299.0 Problems : 96 (Average Length: 91.69 Splits: 0) Lemmas : 744420 (Deleted: 706083) Binary : 12427 (Ratio: 1.67%) Ternary : 3069 (Ratio: 0.41%) Conflict : 744420 (Average Length: 418.6 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 744420 (Average: 12.66 Max: 1061 Sum: 9424807) Executed : 744330 (Average: 12.65 Max: 1061 Sum: 9420204 Ratio: 99.95%) Bounded : 90 (Average: 51.14 Max: 117 Sum: 4603 Ratio: 0.05%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 741626 (Eliminated: 0 Frozen: 233385) Constraints : 5469343 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 920MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 6.33s Memory: 856MB (+0MB) UNKNOWN Iteration Time: 6.39s Iteration 96 Queue: [(6,30,7,True), (7,35,7,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,4,False), (16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,True), (22,110,2,False), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 97 Time : 604.308s (Solving: 572.71s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 604.436s Choices : 10846900 (Domain: 10698336) Conflicts : 753056 (Analyzed: 753053) Restarts : 9308 (Average: 80.90 Last: 169) Model-Level : 299.0 Problems : 97 (Average Length: 91.95 Splits: 0) Lemmas : 753053 (Deleted: 716055) Binary : 12479 (Ratio: 1.66%) Ternary : 3085 (Ratio: 0.41%) Conflict : 753053 (Average Length: 419.5 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 753053 (Average: 12.61 Max: 1061 Sum: 9495254) Executed : 752963 (Average: 12.60 Max: 1061 Sum: 9490651 Ratio: 99.95%) Bounded : 90 (Average: 51.14 Max: 117 Sum: 4603 Ratio: 0.05%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 741626 (Eliminated: 0 Frozen: 233385) Constraints : 5469343 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 920MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 7.03s Memory: 856MB (+0MB) UNKNOWN Iteration Time: 7.11s Iteration 97 Queue: [(7,35,7,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,4,False), (16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,True), (22,110,2,False), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 98 Time : 612.590s (Solving: 580.84s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 612.720s Choices : 10917846 (Domain: 10768490) Conflicts : 761606 (Analyzed: 761603) Restarts : 9408 (Average: 80.95 Last: 169) Model-Level : 299.0 Problems : 98 (Average Length: 92.20 Splits: 0) Lemmas : 761603 (Deleted: 722273) Binary : 12548 (Ratio: 1.65%) Ternary : 3100 (Ratio: 0.41%) Conflict : 761603 (Average Length: 428.4 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 761603 (Average: 12.53 Max: 1061 Sum: 9542493) Executed : 761513 (Average: 12.52 Max: 1061 Sum: 9537890 Ratio: 99.95%) Bounded : 90 (Average: 51.14 Max: 117 Sum: 4603 Ratio: 0.05%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 741626 (Eliminated: 0 Frozen: 233385) Constraints : 5469343 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 920MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 8.24s Memory: 856MB (+0MB) UNKNOWN Iteration Time: 8.29s Iteration 98 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,4,False), (16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,True), (22,110,2,False), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 99 Time : 619.283s (Solving: 587.36s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 619.416s Choices : 10992883 (Domain: 10843211) Conflicts : 770418 (Analyzed: 770415) Restarts : 9508 (Average: 81.03 Last: 169) Model-Level : 299.0 Problems : 99 (Average Length: 92.45 Splits: 0) Lemmas : 770415 (Deleted: 732789) Binary : 12586 (Ratio: 1.63%) Ternary : 3115 (Ratio: 0.40%) Conflict : 770415 (Average Length: 428.9 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 770415 (Average: 12.47 Max: 1061 Sum: 9604608) Executed : 770325 (Average: 12.46 Max: 1061 Sum: 9600005 Ratio: 99.95%) Bounded : 90 (Average: 51.14 Max: 117 Sum: 4603 Ratio: 0.05%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 741626 (Eliminated: 0 Frozen: 233385) Constraints : 5469343 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 920MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 6.62s Memory: 856MB (+0MB) UNKNOWN Iteration Time: 6.70s Iteration 99 Queue: [(10,50,5,True), (11,55,5,False), (12,60,4,True), (13,65,4,False), (14,70,4,False), (15,75,4,False), (16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,True), (22,110,2,False), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 100 Time : 625.136s (Solving: 593.04s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 625.268s Choices : 11075816 (Domain: 10925768) Conflicts : 778929 (Analyzed: 778926) Restarts : 9608 (Average: 81.07 Last: 169) Model-Level : 299.0 Problems : 100 (Average Length: 92.70 Splits: 0) Lemmas : 778926 (Deleted: 739184) Binary : 12630 (Ratio: 1.62%) Ternary : 3137 (Ratio: 0.40%) Conflict : 778926 (Average Length: 428.9 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 778926 (Average: 12.42 Max: 1061 Sum: 9674484) Executed : 778836 (Average: 12.41 Max: 1061 Sum: 9669881 Ratio: 99.95%) Bounded : 90 (Average: 51.14 Max: 117 Sum: 4603 Ratio: 0.05%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 741626 (Eliminated: 0 Frozen: 233385) Constraints : 5469343 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 920MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 5.79s Memory: 856MB (+0MB) UNKNOWN Iteration Time: 5.86s Iteration 100 Queue: [(12,60,4,True), (13,65,4,False), (14,70,4,False), (15,75,4,False), (16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,True), (22,110,2,False), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 101 Time : 635.449s (Solving: 603.19s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 635.584s Choices : 11278892 (Domain: 11124370) Conflicts : 787871 (Analyzed: 787868) Restarts : 9708 (Average: 81.16 Last: 169) Model-Level : 299.0 Problems : 101 (Average Length: 92.94 Splits: 0) Lemmas : 787868 (Deleted: 749595) Binary : 12956 (Ratio: 1.64%) Ternary : 3220 (Ratio: 0.41%) Conflict : 787868 (Average Length: 435.2 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 787868 (Average: 12.50 Max: 1061 Sum: 9847663) Executed : 787778 (Average: 12.49 Max: 1061 Sum: 9843060 Ratio: 99.95%) Bounded : 90 (Average: 51.14 Max: 117 Sum: 4603 Ratio: 0.05%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 741626 (Eliminated: 0 Frozen: 233385) Constraints : 5469343 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 920MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 10.26s Memory: 856MB (+0MB) UNKNOWN Iteration Time: 10.32s Iteration 101 Queue: [(16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,True), (22,110,2,False), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 102 Time : 643.232s (Solving: 610.79s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 643.368s Choices : 11446915 (Domain: 11291991) Conflicts : 796674 (Analyzed: 796671) Restarts : 9808 (Average: 81.23 Last: 169) Model-Level : 299.0 Problems : 102 (Average Length: 93.18 Splits: 0) Lemmas : 796671 (Deleted: 757906) Binary : 13018 (Ratio: 1.63%) Ternary : 3229 (Ratio: 0.41%) Conflict : 796671 (Average Length: 435.3 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 796671 (Average: 12.55 Max: 1061 Sum: 9996813) Executed : 796581 (Average: 12.54 Max: 1061 Sum: 9992210 Ratio: 99.95%) Bounded : 90 (Average: 51.14 Max: 117 Sum: 4603 Ratio: 0.05%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 741626 (Eliminated: 0 Frozen: 233385) Constraints : 5469343 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 920MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 7.71s Memory: 856MB (+0MB) UNKNOWN Iteration Time: 7.79s Iteration 102 Queue: [(20,100,2,True), (21,105,2,True), (22,110,2,False), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 103 Time : 655.794s (Solving: 623.18s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 655.936s Choices : 11927068 (Domain: 11767815) Conflicts : 805110 (Analyzed: 805107) Restarts : 9908 (Average: 81.26 Last: 169) Model-Level : 299.0 Problems : 103 (Average Length: 93.41 Splits: 0) Lemmas : 805107 (Deleted: 764374) Binary : 13429 (Ratio: 1.67%) Ternary : 3354 (Ratio: 0.42%) Conflict : 805107 (Average Length: 441.3 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 805107 (Average: 12.96 Max: 1061 Sum: 10433349) Executed : 805017 (Average: 12.95 Max: 1061 Sum: 10428746 Ratio: 99.96%) Bounded : 90 (Average: 51.14 Max: 117 Sum: 4603 Ratio: 0.04%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 741626 (Eliminated: 0 Frozen: 233385) Constraints : 5469343 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 920MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 12.50s Memory: 856MB (+0MB) UNKNOWN Iteration Time: 12.57s Iteration 103 Queue: [(21,105,2,True), (22,110,2,False), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 104 Time : 663.386s (Solving: 630.62s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 663.532s Choices : 12126946 (Domain: 11967136) Conflicts : 813364 (Analyzed: 813361) Restarts : 10008 (Average: 81.27 Last: 169) Model-Level : 299.0 Problems : 104 (Average Length: 93.63 Splits: 0) Lemmas : 813361 (Deleted: 771975) Binary : 13508 (Ratio: 1.66%) Ternary : 3361 (Ratio: 0.41%) Conflict : 813361 (Average Length: 441.9 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 813361 (Average: 13.04 Max: 1061 Sum: 10608630) Executed : 813271 (Average: 13.04 Max: 1061 Sum: 10604027 Ratio: 99.96%) Bounded : 90 (Average: 51.14 Max: 117 Sum: 4603 Ratio: 0.04%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 741626 (Eliminated: 0 Frozen: 233385) Constraints : 5469343 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 920MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 7.55s Memory: 856MB (+0MB) UNKNOWN Iteration Time: 7.60s Iteration 104 Queue: [(4,20,9,True), (5,25,9,True), (6,30,8,True), (7,35,8,False), (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,3,False), (22,110,2,True), (23,115,2,False)] Grounded Until: 115 Blocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 105 Time : 669.873s (Solving: 636.92s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 670.020s Choices : 12200964 (Domain: 12041154) Conflicts : 821570 (Analyzed: 821567) Restarts : 10108 (Average: 81.28 Last: 169) Model-Level : 299.0 Problems : 105 (Average Length: 93.86 Splits: 0) Lemmas : 821567 (Deleted: 779996) Binary : 13617 (Ratio: 1.66%) Ternary : 3381 (Ratio: 0.41%) Conflict : 821567 (Average Length: 441.0 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 821567 (Average: 13.00 Max: 1061 Sum: 10676525) Executed : 821475 (Average: 12.99 Max: 1061 Sum: 10671692 Ratio: 99.95%) Bounded : 92 (Average: 52.53 Max: 117 Sum: 4833 Ratio: 0.05%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 741626 (Eliminated: 0 Frozen: 233385) Constraints : 5469343 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 920MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 6.42s Memory: 856MB (+0MB) UNKNOWN Iteration Time: 6.49s Iteration 105 Queue: [(5,25,9,True), (6,30,8,True), (7,35,8,False), (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,3,False), (22,110,2,True), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 106 Time : 679.169s (Solving: 646.06s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 679.320s Choices : 12239787 (Domain: 12079977) Conflicts : 829613 (Analyzed: 829610) Restarts : 10208 (Average: 81.27 Last: 169) Model-Level : 299.0 Problems : 106 (Average Length: 94.08 Splits: 0) Lemmas : 829610 (Deleted: 787860) Binary : 13624 (Ratio: 1.64%) Ternary : 3387 (Ratio: 0.41%) Conflict : 829610 (Average Length: 442.8 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 829610 (Average: 12.90 Max: 1061 Sum: 10702818) Executed : 829518 (Average: 12.90 Max: 1061 Sum: 10697985 Ratio: 99.95%) Bounded : 92 (Average: 52.53 Max: 117 Sum: 4833 Ratio: 0.05%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 741626 (Eliminated: 0 Frozen: 233385) Constraints : 5462480 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 920MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 9.24s Memory: 856MB (+0MB) UNKNOWN Iteration Time: 9.30s Iteration 106 Queue: [(6,30,8,True), (7,35,8,False), (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,3,False), (22,110,2,True), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 107 Time : 685.930s (Solving: 652.64s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 686.084s Choices : 12297411 (Domain: 12137601) Conflicts : 837739 (Analyzed: 837736) Restarts : 10308 (Average: 81.27 Last: 169) Model-Level : 299.0 Problems : 107 (Average Length: 94.29 Splits: 0) Lemmas : 837736 (Deleted: 795831) Binary : 13666 (Ratio: 1.63%) Ternary : 3390 (Ratio: 0.40%) Conflict : 837736 (Average Length: 446.5 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 837736 (Average: 12.83 Max: 1061 Sum: 10744549) Executed : 837644 (Average: 12.82 Max: 1061 Sum: 10739716 Ratio: 99.96%) Bounded : 92 (Average: 52.53 Max: 117 Sum: 4833 Ratio: 0.04%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 741626 (Eliminated: 0 Frozen: 233385) Constraints : 5462480 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 920MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 6.70s Memory: 856MB (+0MB) UNKNOWN Iteration Time: 6.77s Iteration 107 Queue: [(8,40,7,True), (9,45,6,True), (10,50,6,False), (11,55,5,True), (12,60,5,False), (13,65,4,True), (14,70,4,False), (15,75,4,False), (16,80,4,False), (17,85,3,True), (18,90,3,False), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,2,True), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 108 Time : 693.255s (Solving: 659.82s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 693.412s Choices : 12377741 (Domain: 12217618) Conflicts : 847060 (Analyzed: 847057) Restarts : 10408 (Average: 81.39 Last: 169) Model-Level : 299.0 Problems : 108 (Average Length: 94.50 Splits: 0) Lemmas : 847057 (Deleted: 805805) Binary : 13757 (Ratio: 1.62%) Ternary : 3401 (Ratio: 0.40%) Conflict : 847057 (Average Length: 447.7 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 847057 (Average: 12.76 Max: 1061 Sum: 10810649) Executed : 846965 (Average: 12.76 Max: 1061 Sum: 10805816 Ratio: 99.96%) Bounded : 92 (Average: 52.53 Max: 117 Sum: 4833 Ratio: 0.04%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 741626 (Eliminated: 0 Frozen: 233385) Constraints : 5462480 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 920MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 7.28s Memory: 856MB (+0MB) UNKNOWN Iteration Time: 7.33s Iteration 108 Queue: [(9,45,6,True), (10,50,6,False), (11,55,5,True), (12,60,5,False), (13,65,4,True), (14,70,4,False), (15,75,4,False), (16,80,4,False), (17,85,3,True), (18,90,3,False), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,2,True), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 109 Time : 701.133s (Solving: 667.53s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 701.292s Choices : 12468686 (Domain: 12308336) Conflicts : 855766 (Analyzed: 855763) Restarts : 10508 (Average: 81.44 Last: 169) Model-Level : 299.0 Problems : 109 (Average Length: 94.71 Splits: 0) Lemmas : 855763 (Deleted: 814886) Binary : 13829 (Ratio: 1.62%) Ternary : 3411 (Ratio: 0.40%) Conflict : 855763 (Average Length: 451.0 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 855763 (Average: 12.72 Max: 1061 Sum: 10884467) Executed : 855671 (Average: 12.71 Max: 1061 Sum: 10879634 Ratio: 99.96%) Bounded : 92 (Average: 52.53 Max: 117 Sum: 4833 Ratio: 0.04%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 741626 (Eliminated: 0 Frozen: 233385) Constraints : 5462480 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 920MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 7.82s Memory: 856MB (+0MB) UNKNOWN Iteration Time: 7.88s Iteration 109 Queue: [(11,55,5,True), (12,60,5,False), (13,65,4,True), (14,70,4,False), (15,75,4,False), (16,80,4,False), (17,85,3,True), (18,90,3,False), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,2,True), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 110 Time : 708.864s (Solving: 675.10s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 709.024s Choices : 12568169 (Domain: 12407103) Conflicts : 864309 (Analyzed: 864306) Restarts : 10608 (Average: 81.48 Last: 169) Model-Level : 299.0 Problems : 110 (Average Length: 94.91 Splits: 0) Lemmas : 864306 (Deleted: 821169) Binary : 13901 (Ratio: 1.61%) Ternary : 3423 (Ratio: 0.40%) Conflict : 864306 (Average Length: 452.1 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 864306 (Average: 12.69 Max: 1061 Sum: 10967871) Executed : 864214 (Average: 12.68 Max: 1061 Sum: 10963038 Ratio: 99.96%) Bounded : 92 (Average: 52.53 Max: 117 Sum: 4833 Ratio: 0.04%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 741626 (Eliminated: 0 Frozen: 233385) Constraints : 5462480 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 920MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 7.68s Memory: 856MB (+0MB) UNKNOWN Iteration Time: 7.74s Iteration 110 Queue: [(13,65,4,True), (14,70,4,False), (15,75,4,False), (16,80,4,False), (17,85,3,True), (18,90,3,False), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,2,True), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 111 Time : 717.597s (Solving: 683.67s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 717.760s Choices : 12693116 (Domain: 12531725) Conflicts : 872929 (Analyzed: 872926) Restarts : 10708 (Average: 81.52 Last: 169) Model-Level : 299.0 Problems : 111 (Average Length: 95.11 Splits: 0) Lemmas : 872926 (Deleted: 831650) Binary : 13953 (Ratio: 1.60%) Ternary : 3433 (Ratio: 0.39%) Conflict : 872926 (Average Length: 454.8 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 872926 (Average: 12.68 Max: 1061 Sum: 11070839) Executed : 872834 (Average: 12.68 Max: 1061 Sum: 11066006 Ratio: 99.96%) Bounded : 92 (Average: 52.53 Max: 117 Sum: 4833 Ratio: 0.04%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 741626 (Eliminated: 0 Frozen: 233385) Constraints : 5462480 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 920MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 8.68s Memory: 856MB (+0MB) UNKNOWN Iteration Time: 8.74s Iteration 111 Queue: [(17,85,3,True), (18,90,3,False), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,2,True), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 112 Time : 725.515s (Solving: 691.41s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 725.684s Choices : 12825912 (Domain: 12664357) Conflicts : 881416 (Analyzed: 881413) Restarts : 10808 (Average: 81.55 Last: 169) Model-Level : 299.0 Problems : 112 (Average Length: 95.30 Splits: 0) Lemmas : 881413 (Deleted: 837899) Binary : 14006 (Ratio: 1.59%) Ternary : 3440 (Ratio: 0.39%) Conflict : 881413 (Average Length: 456.7 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 881413 (Average: 12.69 Max: 1061 Sum: 11180771) Executed : 881321 (Average: 12.68 Max: 1061 Sum: 11175938 Ratio: 99.96%) Bounded : 92 (Average: 52.53 Max: 117 Sum: 4833 Ratio: 0.04%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 741626 (Eliminated: 0 Frozen: 233385) Constraints : 5462480 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 920MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 7.85s Memory: 856MB (+0MB) UNKNOWN Iteration Time: 7.92s Iteration 112 Queue: [(22,110,2,True), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 113 Time : 736.552s (Solving: 702.27s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 736.724s Choices : 12956813 (Domain: 12795130) Conflicts : 890174 (Analyzed: 890171) Restarts : 10908 (Average: 81.61 Last: 169) Model-Level : 299.0 Problems : 113 (Average Length: 95.50 Splits: 0) Lemmas : 890171 (Deleted: 848284) Binary : 14097 (Ratio: 1.58%) Ternary : 3444 (Ratio: 0.39%) Conflict : 890171 (Average Length: 463.6 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 890171 (Average: 12.67 Max: 1061 Sum: 11275058) Executed : 890079 (Average: 12.66 Max: 1061 Sum: 11270225 Ratio: 99.96%) Bounded : 92 (Average: 52.53 Max: 117 Sum: 4833 Ratio: 0.04%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 741626 (Eliminated: 0 Frozen: 233385) Constraints : 5462480 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 920MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 10.97s Memory: 856MB (+0MB) UNKNOWN Iteration Time: 11.04s Iteration 113 Queue: [(4,20,10,True), (5,25,10,True), (6,30,9,True), (7,35,8,True), (8,40,8,False), (9,45,7,False), (10,50,6,True), (11,55,6,False), (12,60,5,True), (13,65,5,False), (14,70,4,True), (15,75,4,False), (16,80,4,False), (17,85,4,False), (18,90,3,True), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,2,False)] Grounded Until: 115 Blocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 114 Time : 740.030s (Solving: 705.57s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 740.204s Choices : 13010236 (Domain: 12848553) Conflicts : 897697 (Analyzed: 897694) Restarts : 11008 (Average: 81.55 Last: 169) Model-Level : 299.0 Problems : 114 (Average Length: 95.68 Splits: 0) Lemmas : 897694 (Deleted: 854718) Binary : 14124 (Ratio: 1.57%) Ternary : 3456 (Ratio: 0.38%) Conflict : 897694 (Average Length: 461.6 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 897694 (Average: 12.61 Max: 1061 Sum: 11316285) Executed : 897601 (Average: 12.60 Max: 1061 Sum: 11311451 Ratio: 99.96%) Bounded : 93 (Average: 51.98 Max: 117 Sum: 4834 Ratio: 0.04%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 741626 (Eliminated: 0 Frozen: 233385) Constraints : 5462480 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 920MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 3.41s Memory: 856MB (+0MB) UNKNOWN Iteration Time: 3.48s Iteration 114 Queue: [(5,25,10,True), (6,30,9,True), (7,35,8,True), (8,40,8,False), (9,45,7,False), (10,50,6,True), (11,55,6,False), (12,60,5,True), (13,65,5,False), (14,70,4,True), (15,75,4,False), (16,80,4,False), (17,85,4,False), (18,90,3,True), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 115 Time : 751.188s (Solving: 716.56s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 751.364s Choices : 13053391 (Domain: 12891708) Conflicts : 906488 (Analyzed: 906485) Restarts : 11108 (Average: 81.61 Last: 169) Model-Level : 299.0 Problems : 115 (Average Length: 95.87 Splits: 0) Lemmas : 906485 (Deleted: 864205) Binary : 14148 (Ratio: 1.56%) Ternary : 3461 (Ratio: 0.38%) Conflict : 906485 (Average Length: 467.5 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 906485 (Average: 12.52 Max: 1061 Sum: 11345874) Executed : 906392 (Average: 12.51 Max: 1061 Sum: 11341040 Ratio: 99.96%) Bounded : 93 (Average: 51.98 Max: 117 Sum: 4834 Ratio: 0.04%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 741626 (Eliminated: 0 Frozen: 233385) Constraints : 5462480 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 920MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 11.10s Memory: 856MB (+0MB) UNKNOWN Iteration Time: 11.17s Iteration 115 Queue: [(6,30,9,True), (7,35,8,True), (8,40,8,False), (9,45,7,False), (10,50,6,True), (11,55,6,False), (12,60,5,True), (13,65,5,False), (14,70,4,True), (15,75,4,False), (16,80,4,False), (17,85,4,False), (18,90,3,True), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 116 Time : 755.705s (Solving: 720.91s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 755.884s Choices : 13105358 (Domain: 12943675) Conflicts : 914109 (Analyzed: 914106) Restarts : 11208 (Average: 81.56 Last: 169) Model-Level : 299.0 Problems : 116 (Average Length: 96.05 Splits: 0) Lemmas : 914106 (Deleted: 870755) Binary : 14163 (Ratio: 1.55%) Ternary : 3464 (Ratio: 0.38%) Conflict : 914106 (Average Length: 466.8 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 914106 (Average: 12.46 Max: 1061 Sum: 11386988) Executed : 914013 (Average: 12.45 Max: 1061 Sum: 11382154 Ratio: 99.96%) Bounded : 93 (Average: 51.98 Max: 117 Sum: 4834 Ratio: 0.04%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 741626 (Eliminated: 0 Frozen: 233385) Constraints : 5462480 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 920MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 4.45s Memory: 856MB (+0MB) UNKNOWN Iteration Time: 4.52s Iteration 116 Queue: [(7,35,8,True), (8,40,8,False), (9,45,7,False), (10,50,6,True), (11,55,6,False), (12,60,5,True), (13,65,5,False), (14,70,4,True), (15,75,4,False), (16,80,4,False), (17,85,4,False), (18,90,3,True), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 117 Time : 762.322s (Solving: 727.37s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 762.504s Choices : 13161842 (Domain: 12999997) Conflicts : 922082 (Analyzed: 922079) Restarts : 11308 (Average: 81.54 Last: 169) Model-Level : 299.0 Problems : 117 (Average Length: 96.23 Splits: 0) Lemmas : 922079 (Deleted: 878097) Binary : 14229 (Ratio: 1.54%) Ternary : 3472 (Ratio: 0.38%) Conflict : 922079 (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 : 922079 (Average: 12.39 Max: 1061 Sum: 11427032) Executed : 921986 (Average: 12.39 Max: 1061 Sum: 11422198 Ratio: 99.96%) Bounded : 93 (Average: 51.98 Max: 117 Sum: 4834 Ratio: 0.04%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 741626 (Eliminated: 0 Frozen: 233385) Constraints : 5462480 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 920MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 6.56s Memory: 856MB (+0MB) UNKNOWN Iteration Time: 6.62s Iteration 117 Queue: [(10,50,6,True), (11,55,6,False), (12,60,5,True), (13,65,5,False), (14,70,4,True), (15,75,4,False), (16,80,4,False), (17,85,4,False), (18,90,3,True), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 118 Time : 769.085s (Solving: 733.98s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 769.272s Choices : 13243475 (Domain: 13081523) Conflicts : 930370 (Analyzed: 930367) Restarts : 11408 (Average: 81.55 Last: 169) Model-Level : 299.0 Problems : 118 (Average Length: 96.41 Splits: 0) Lemmas : 930367 (Deleted: 885907) Binary : 14312 (Ratio: 1.54%) Ternary : 3501 (Ratio: 0.38%) Conflict : 930367 (Average Length: 471.0 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 930367 (Average: 12.35 Max: 1061 Sum: 11490268) Executed : 930273 (Average: 12.34 Max: 1061 Sum: 11485317 Ratio: 99.96%) Bounded : 94 (Average: 52.67 Max: 117 Sum: 4951 Ratio: 0.04%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 741626 (Eliminated: 0 Frozen: 233385) Constraints : 5462480 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 920MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 6.71s Memory: 856MB (+0MB) UNKNOWN Iteration Time: 6.77s Iteration 118 Queue: [(12,60,5,True), (13,65,5,False), (14,70,4,True), (15,75,4,False), (16,80,4,False), (17,85,4,False), (18,90,3,True), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 119 Time : 777.500s (Solving: 742.24s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 777.692s Choices : 13344523 (Domain: 13182467) Conflicts : 939164 (Analyzed: 939161) Restarts : 11508 (Average: 81.61 Last: 169) Model-Level : 299.0 Problems : 119 (Average Length: 96.58 Splits: 0) Lemmas : 939161 (Deleted: 896028) Binary : 14378 (Ratio: 1.53%) Ternary : 3508 (Ratio: 0.37%) Conflict : 939161 (Average Length: 473.2 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 939161 (Average: 12.32 Max: 1061 Sum: 11571830) Executed : 939067 (Average: 12.32 Max: 1061 Sum: 11566879 Ratio: 99.96%) Bounded : 94 (Average: 52.67 Max: 117 Sum: 4951 Ratio: 0.04%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 741626 (Eliminated: 0 Frozen: 233385) Constraints : 5462466 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 920MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 8.37s Memory: 856MB (+0MB) UNKNOWN Iteration Time: 8.42s Iteration 119 Queue: [(14,70,4,True), (15,75,4,False), (16,80,4,False), (17,85,4,False), (18,90,3,True), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 120 Time : 787.054s (Solving: 751.63s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 787.248s Choices : 13459672 (Domain: 13297261) Conflicts : 948294 (Analyzed: 948291) Restarts : 11608 (Average: 81.69 Last: 169) Model-Level : 299.0 Problems : 120 (Average Length: 96.75 Splits: 0) Lemmas : 948291 (Deleted: 904586) Binary : 14439 (Ratio: 1.52%) Ternary : 3527 (Ratio: 0.37%) Conflict : 948291 (Average Length: 478.4 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 948291 (Average: 12.30 Max: 1061 Sum: 11659992) Executed : 948197 (Average: 12.29 Max: 1061 Sum: 11655041 Ratio: 99.96%) Bounded : 94 (Average: 52.67 Max: 117 Sum: 4951 Ratio: 0.04%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 741626 (Eliminated: 0 Frozen: 233385) Constraints : 5462466 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 920MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 9.50s Memory: 856MB (+0MB) UNKNOWN Iteration Time: 9.56s Iteration 120 Queue: [(18,90,3,True), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,2,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 121 Time : 794.644s (Solving: 759.05s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 794.840s Choices : 13575870 (Domain: 13413079) Conflicts : 957019 (Analyzed: 957016) Restarts : 11708 (Average: 81.74 Last: 169) Model-Level : 299.0 Problems : 121 (Average Length: 96.92 Splits: 0) Lemmas : 957016 (Deleted: 913519) Binary : 14498 (Ratio: 1.51%) Ternary : 3536 (Ratio: 0.37%) Conflict : 957016 (Average Length: 479.7 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 957016 (Average: 12.28 Max: 1061 Sum: 11752843) Executed : 956922 (Average: 12.28 Max: 1061 Sum: 11747892 Ratio: 99.96%) Bounded : 94 (Average: 52.67 Max: 117 Sum: 4951 Ratio: 0.04%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 741626 (Eliminated: 0 Frozen: 233385) Constraints : 5462466 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 920MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 7.53s Memory: 856MB (+0MB) UNKNOWN Iteration Time: 7.60s Iteration 121 Queue: [(4,20,11,True), (5,25,11,True), (6,30,10,True), (7,35,9,True), (8,40,8,True), (9,45,7,True), (10,50,7,False), (11,55,6,True), (12,60,6,False), (13,65,5,True), (14,70,5,False), (15,75,4,True), (16,80,4,False), (17,85,4,False), (18,90,4,False), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,2,True)] Grounded Until: 115 Blocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 122 Time : 798.706s (Solving: 762.96s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 798.904s Choices : 13628206 (Domain: 13465415) Conflicts : 964871 (Analyzed: 964868) Restarts : 11808 (Average: 81.71 Last: 169) Model-Level : 299.0 Problems : 122 (Average Length: 97.08 Splits: 0) Lemmas : 964868 (Deleted: 919787) Binary : 14575 (Ratio: 1.51%) Ternary : 3553 (Ratio: 0.37%) Conflict : 964868 (Average Length: 478.5 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 964868 (Average: 12.23 Max: 1061 Sum: 11796719) Executed : 964773 (Average: 12.22 Max: 1061 Sum: 11791651 Ratio: 99.96%) Bounded : 95 (Average: 53.35 Max: 117 Sum: 5068 Ratio: 0.04%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 741626 (Eliminated: 0 Frozen: 233385) Constraints : 5462466 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 920MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 4.01s Memory: 856MB (+0MB) UNKNOWN Iteration Time: 4.07s Iteration 122 Queue: [(5,25,11,True), (6,30,10,True), (7,35,9,True), (8,40,8,True), (9,45,7,True), (10,50,7,False), (11,55,6,True), (12,60,6,False), (13,65,5,True), (14,70,5,False), (15,75,4,True), (16,80,4,False), (17,85,4,False), (18,90,4,False), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,2,True)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 123 Time : 807.509s (Solving: 771.62s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 807.712s Choices : 13669507 (Domain: 13506716) Conflicts : 973012 (Analyzed: 973009) Restarts : 11908 (Average: 81.71 Last: 169) Model-Level : 299.0 Problems : 123 (Average Length: 97.24 Splits: 0) Lemmas : 973009 (Deleted: 927470) Binary : 14602 (Ratio: 1.50%) Ternary : 3563 (Ratio: 0.37%) Conflict : 973009 (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 : 973009 (Average: 12.15 Max: 1061 Sum: 11826715) Executed : 972914 (Average: 12.15 Max: 1061 Sum: 11821647 Ratio: 99.96%) Bounded : 95 (Average: 53.35 Max: 117 Sum: 5068 Ratio: 0.04%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 741626 (Eliminated: 0 Frozen: 233385) Constraints : 5462452 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 920MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 8.76s Memory: 856MB (+0MB) UNKNOWN Iteration Time: 8.81s Iteration 123 Queue: [(6,30,10,True), (7,35,9,True), (8,40,8,True), (9,45,7,True), (10,50,7,False), (11,55,6,True), (12,60,6,False), (13,65,5,True), (14,70,5,False), (15,75,4,True), (16,80,4,False), (17,85,4,False), (18,90,4,False), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,2,True)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 124 Time : 814.163s (Solving: 778.12s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 814.368s Choices : 13726764 (Domain: 13563973) Conflicts : 981143 (Analyzed: 981140) Restarts : 12008 (Average: 81.71 Last: 169) Model-Level : 299.0 Problems : 124 (Average Length: 97.40 Splits: 0) Lemmas : 981140 (Deleted: 935543) Binary : 14623 (Ratio: 1.49%) Ternary : 3568 (Ratio: 0.36%) Conflict : 981140 (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 : 981140 (Average: 12.10 Max: 1061 Sum: 11871045) Executed : 981045 (Average: 12.09 Max: 1061 Sum: 11865977 Ratio: 99.96%) Bounded : 95 (Average: 53.35 Max: 117 Sum: 5068 Ratio: 0.04%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 741626 (Eliminated: 0 Frozen: 233385) Constraints : 5462452 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 920MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 6.61s Memory: 856MB (+0MB) UNKNOWN Iteration Time: 6.66s Iteration 124 Queue: [(7,35,9,True), (8,40,8,True), (9,45,7,True), (10,50,7,False), (11,55,6,True), (12,60,6,False), (13,65,5,True), (14,70,5,False), (15,75,4,True), (16,80,4,False), (17,85,4,False), (18,90,4,False), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,2,True)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 125 Time : 821.407s (Solving: 785.21s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 821.616s Choices : 13788603 (Domain: 13625812) Conflicts : 989195 (Analyzed: 989192) Restarts : 12108 (Average: 81.70 Last: 169) Model-Level : 299.0 Problems : 125 (Average Length: 97.56 Splits: 0) Lemmas : 989192 (Deleted: 943494) Binary : 14665 (Ratio: 1.48%) Ternary : 3573 (Ratio: 0.36%) Conflict : 989192 (Average Length: 487.7 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 989192 (Average: 12.04 Max: 1061 Sum: 11909468) Executed : 989097 (Average: 12.03 Max: 1061 Sum: 11904400 Ratio: 99.96%) Bounded : 95 (Average: 53.35 Max: 117 Sum: 5068 Ratio: 0.04%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 741626 (Eliminated: 0 Frozen: 233385) Constraints : 5462452 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 920MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 7.19s Memory: 856MB (+0MB) UNKNOWN Iteration Time: 7.25s Iteration 125 Queue: [(8,40,8,True), (9,45,7,True), (10,50,7,False), (11,55,6,True), (12,60,6,False), (13,65,5,True), (14,70,5,False), (15,75,4,True), (16,80,4,False), (17,85,4,False), (18,90,4,False), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,2,True)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 126 Time : 828.451s (Solving: 792.08s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 828.664s Choices : 13850700 (Domain: 13687759) Conflicts : 997553 (Analyzed: 997550) Restarts : 12208 (Average: 81.71 Last: 169) Model-Level : 299.0 Problems : 126 (Average Length: 97.71 Splits: 0) Lemmas : 997550 (Deleted: 951427) Binary : 14689 (Ratio: 1.47%) Ternary : 3582 (Ratio: 0.36%) Conflict : 997550 (Average Length: 488.5 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 997550 (Average: 11.99 Max: 1061 Sum: 11958412) Executed : 997455 (Average: 11.98 Max: 1061 Sum: 11953344 Ratio: 99.96%) Bounded : 95 (Average: 53.35 Max: 117 Sum: 5068 Ratio: 0.04%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 741626 (Eliminated: 0 Frozen: 233385) Constraints : 5462452 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 920MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 6.98s Memory: 856MB (+0MB) UNKNOWN Iteration Time: 7.05s Iteration 126 Queue: [(9,45,7,True), (10,50,7,False), (11,55,6,True), (12,60,6,False), (13,65,5,True), (14,70,5,False), (15,75,4,True), (16,80,4,False), (17,85,4,False), (18,90,4,False), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,2,True)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 127 Time : 835.091s (Solving: 798.56s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 835.308s Choices : 13927748 (Domain: 13763790) Conflicts : 1005938 (Analyzed: 1005935) Restarts : 12308 (Average: 81.73 Last: 169) Model-Level : 299.0 Problems : 127 (Average Length: 97.87 Splits: 0) Lemmas : 1005935 (Deleted: 959593) Binary : 14760 (Ratio: 1.47%) Ternary : 3589 (Ratio: 0.36%) Conflict : 1005935 (Average Length: 489.2 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 1005935 (Average: 11.95 Max: 1061 Sum: 12020237) Executed : 1005840 (Average: 11.94 Max: 1061 Sum: 12015169 Ratio: 99.96%) Bounded : 95 (Average: 53.35 Max: 117 Sum: 5068 Ratio: 0.04%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 741626 (Eliminated: 0 Frozen: 233385) Constraints : 5462452 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 920MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 6.58s Memory: 856MB (+0MB) UNKNOWN Iteration Time: 6.64s Iteration 127 Queue: [(11,55,6,True), (12,60,6,False), (13,65,5,True), (14,70,5,False), (15,75,4,True), (16,80,4,False), (17,85,4,False), (18,90,4,False), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,2,True)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 128 Time : 843.647s (Solving: 806.95s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 843.868s Choices : 14039814 (Domain: 13875502) Conflicts : 1014933 (Analyzed: 1014930) Restarts : 12408 (Average: 81.80 Last: 169) Model-Level : 299.0 Problems : 128 (Average Length: 98.02 Splits: 0) Lemmas : 1014930 (Deleted: 970003) Binary : 14826 (Ratio: 1.46%) Ternary : 3597 (Ratio: 0.35%) Conflict : 1014930 (Average Length: 490.6 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 1014930 (Average: 11.94 Max: 1061 Sum: 12113836) Executed : 1014835 (Average: 11.93 Max: 1061 Sum: 12108768 Ratio: 99.96%) Bounded : 95 (Average: 53.35 Max: 117 Sum: 5068 Ratio: 0.04%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 741626 (Eliminated: 0 Frozen: 233385) Constraints : 5462452 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 920MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 8.50s Memory: 856MB (+0MB) UNKNOWN Iteration Time: 8.56s Iteration 128 Queue: [(13,65,5,True), (14,70,5,False), (15,75,4,True), (16,80,4,False), (17,85,4,False), (18,90,4,False), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,2,True)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 129 Time : 853.188s (Solving: 816.32s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 853.416s Choices : 14167725 (Domain: 14003145) Conflicts : 1024225 (Analyzed: 1024222) Restarts : 12508 (Average: 81.89 Last: 169) Model-Level : 299.0 Problems : 129 (Average Length: 98.16 Splits: 0) Lemmas : 1024222 (Deleted: 978793) Binary : 14885 (Ratio: 1.45%) Ternary : 3609 (Ratio: 0.35%) Conflict : 1024222 (Average Length: 495.8 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 1024222 (Average: 11.93 Max: 1061 Sum: 12216212) Executed : 1024127 (Average: 11.92 Max: 1061 Sum: 12211144 Ratio: 99.96%) Bounded : 95 (Average: 53.35 Max: 117 Sum: 5068 Ratio: 0.04%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 741626 (Eliminated: 0 Frozen: 233385) Constraints : 5462452 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 920MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 9.48s Memory: 856MB (+0MB) UNKNOWN Iteration Time: 9.55s Iteration 129 Queue: [(15,75,4,True), (16,80,4,False), (17,85,4,False), (18,90,4,False), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,2,True)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 130 Time : 862.769s (Solving: 825.75s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 863.004s Choices : 14346547 (Domain: 14180728) Conflicts : 1033511 (Analyzed: 1033508) Restarts : 12608 (Average: 81.97 Last: 169) Model-Level : 299.0 Problems : 130 (Average Length: 98.31 Splits: 0) Lemmas : 1033508 (Deleted: 987859) Binary : 14982 (Ratio: 1.45%) Ternary : 3630 (Ratio: 0.35%) Conflict : 1033508 (Average Length: 497.9 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 1033508 (Average: 11.97 Max: 1061 Sum: 12371917) Executed : 1033413 (Average: 11.97 Max: 1061 Sum: 12366849 Ratio: 99.96%) Bounded : 95 (Average: 53.35 Max: 117 Sum: 5068 Ratio: 0.04%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 741626 (Eliminated: 0 Frozen: 233385) Constraints : 5462452 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 920MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 9.53s Memory: 856MB (+0MB) UNKNOWN Iteration Time: 9.59s Iteration 130 Queue: [(23,115,2,True)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 131 Time : 872.700s (Solving: 835.51s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 872.940s Choices : 14565525 (Domain: 14399515) Conflicts : 1042583 (Analyzed: 1042580) Restarts : 12708 (Average: 82.04 Last: 169) Model-Level : 299.0 Problems : 131 (Average Length: 98.45 Splits: 0) Lemmas : 1042580 (Deleted: 996900) Binary : 15077 (Ratio: 1.45%) Ternary : 3646 (Ratio: 0.35%) Conflict : 1042580 (Average Length: 499.9 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 1042580 (Average: 12.05 Max: 1061 Sum: 12561225) Executed : 1042485 (Average: 12.04 Max: 1061 Sum: 12556157 Ratio: 99.96%) Bounded : 95 (Average: 53.35 Max: 117 Sum: 5068 Ratio: 0.04%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 741626 (Eliminated: 0 Frozen: 233385) Constraints : 5462452 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 920MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 9.87s Memory: 856MB (+0MB) UNKNOWN Iteration Time: 9.94s Iteration 131 Queue: [(4,20,12,True), (5,25,12,True), (6,30,11,True), (7,35,10,False), (8,40,9,True), (9,45,8,True), (10,50,7,True), (11,55,7,False), (12,60,6,True), (13,65,6,False), (14,70,5,True), (15,75,5,False), (16,80,4,True), (17,85,4,False), (18,90,4,False), (19,95,3,True), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,3,False)] Grounded Until: 115 Blocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 132 Time : 881.245s (Solving: 843.91s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 881.488s Choices : 14611650 (Domain: 14445640) Conflicts : 1050465 (Analyzed: 1050462) Restarts : 12808 (Average: 82.02 Last: 169) Model-Level : 299.0 Problems : 132 (Average Length: 98.59 Splits: 0) Lemmas : 1050462 (Deleted: 1003620) Binary : 15178 (Ratio: 1.44%) Ternary : 3658 (Ratio: 0.35%) Conflict : 1050462 (Average Length: 501.6 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 1050462 (Average: 12.00 Max: 1061 Sum: 12602598) Executed : 1050366 (Average: 11.99 Max: 1061 Sum: 12597413 Ratio: 99.96%) Bounded : 96 (Average: 54.01 Max: 117 Sum: 5185 Ratio: 0.04%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 741626 (Eliminated: 0 Frozen: 233385) Constraints : 5462452 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 920MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 8.50s Memory: 856MB (+0MB) UNKNOWN Iteration Time: 8.55s Iteration 132 Queue: [(5,25,12,True), (6,30,11,True), (7,35,10,False), (8,40,9,True), (9,45,8,True), (10,50,7,True), (11,55,7,False), (12,60,6,True), (13,65,6,False), (14,70,5,True), (15,75,5,False), (16,80,4,True), (17,85,4,False), (18,90,4,False), (19,95,3,True), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,3,False)] Grounded Until: 115 Unblocking actions... Solving... [start: stats after solve call] Models : 0+ Calls : 133 Time : 892.472s (Solving: 854.98s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 892.720s Choices : 14664028 (Domain: 14498018) Conflicts : 1058988 (Analyzed: 1058985) Restarts : 12908 (Average: 82.04 Last: 169) Model-Level : 299.0 Problems : 133 (Average Length: 98.73 Splits: 0) Lemmas : 1058985 (Deleted: 1011440) Binary : 15221 (Ratio: 1.44%) Ternary : 3664 (Ratio: 0.35%) Conflict : 1058985 (Average Length: 506.1 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 1058985 (Average: 11.94 Max: 1061 Sum: 12641519) Executed : 1058889 (Average: 11.93 Max: 1061 Sum: 12636334 Ratio: 99.96%) Bounded : 96 (Average: 54.01 Max: 117 Sum: 5185 Ratio: 0.04%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 741626 (Eliminated: 0 Frozen: 233385) Constraints : 5462438 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 920MB Max. Length : 115 steps Models : 1 [endof: stats after solve call] Solving Time: 11.18s Memory: 856MB (+0MB) UNKNOWN Iteration Time: 11.23s Iteration 133 Queue: [(6,30,11,True), (7,35,10,False), (8,40,9,True), (9,45,8,True), (10,50,7,True), (11,55,7,False), (12,60,6,True), (13,65,6,False), (14,70,5,True), (15,75,5,False), (16,80,4,True), (17,85,4,False), (18,90,4,False), (19,95,3,True), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,3,False)] Grounded Until: 115 Unblocking actions... Solving... *** Info : (planner): INTERRUPTED by signal! UNKNOWN INTERRUPTED : 1 Models : 0+ Calls : 134 Time : 893.438s (Solving: 855.78s 1st Model: 0.02s Unsat: 4.93s) CPU Time : 893.664s Choices : 14669987 (Domain: 14503977) Conflicts : 1060275 (Analyzed: 1060272) Restarts : 12925 (Average: 82.03 Last: 169) Model-Level : 299.0 Problems : 134 (Average Length: 98.87 Splits: 0) Lemmas : 1060272 (Deleted: 1011440) Binary : 15221 (Ratio: 1.44%) Ternary : 3666 (Ratio: 0.35%) Conflict : 1060272 (Average Length: 505.8 Ratio: 100.00%) Loop : 0 (Average Length: 0.0 Ratio: 0.00%) Other : 0 (Average Length: 0.0 Ratio: 0.00%) Backjumps : 1060272 (Average: 11.93 Max: 1061 Sum: 12646208) Executed : 1060176 (Average: 11.92 Max: 1061 Sum: 12641023 Ratio: 99.96%) Bounded : 96 (Average: 54.01 Max: 117 Sum: 5185 Ratio: 0.04%) Rules : 133871 (Original: 121411) Atoms : 64609 Bodies : 58138 (Original: 45677) Count : 786 (Original: 2108) Equivalences : 14175 (Atom=Atom: 77 Body=Body: 0 Other: 14098) Tight : Yes Variables : 741626 (Eliminated: 0 Frozen: 233385) Constraints : 5462438 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) Memory Peak : 920MB Max. Length : 115 steps Models : 1