4941 lines
181 KiB
Plaintext
4941 lines
181 KiB
Plaintext
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
|
|
|
|
|