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