2448 lines
88 KiB
Plaintext
2448 lines
88 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-2.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-2.pddl
|
|
Parsing...
|
|
Parsing: [0.040s CPU, 0.037s wall-clock]
|
|
Normalizing task... [0.000s CPU, 0.003s wall-clock]
|
|
Instantiating...
|
|
Generating Datalog program... [0.010s CPU, 0.009s wall-clock]
|
|
Normalizing Datalog program...
|
|
Normalizing Datalog program: [0.050s CPU, 0.049s wall-clock]
|
|
Preparing model... [0.020s CPU, 0.025s wall-clock]
|
|
Generated 115 rules.
|
|
Computing model... [0.330s CPU, 0.330s wall-clock]
|
|
2025 relevant atoms
|
|
2105 auxiliary atoms
|
|
4130 final queue length
|
|
7122 total queue pushes
|
|
Completing instantiation... [0.600s CPU, 0.598s wall-clock]
|
|
Instantiating: [1.010s CPU, 1.018s wall-clock]
|
|
Computing fact groups...
|
|
Finding invariants...
|
|
24 initial candidates
|
|
Finding invariants: [0.100s CPU, 0.097s wall-clock]
|
|
Checking invariant weight... [0.000s CPU, 0.001s wall-clock]
|
|
Instantiating groups... [0.010s CPU, 0.006s wall-clock]
|
|
Collecting mutex groups... [0.000s CPU, 0.000s wall-clock]
|
|
Choosing groups...
|
|
207 uncovered facts
|
|
Choosing groups: [0.000s CPU, 0.001s wall-clock]
|
|
Building translation key... [0.010s CPU, 0.008s wall-clock]
|
|
Computing fact groups: [0.130s CPU, 0.130s wall-clock]
|
|
Building STRIPS to SAS dictionary... [0.000s CPU, 0.002s wall-clock]
|
|
Building dictionary for full mutex groups... [0.000s CPU, 0.002s wall-clock]
|
|
Building mutex information...
|
|
Building mutex information: [0.000s CPU, 0.002s wall-clock]
|
|
Translating task...
|
|
Processing axioms...
|
|
Simplifying axioms... [0.000s CPU, 0.000s wall-clock]
|
|
Processing axioms: [0.040s CPU, 0.033s wall-clock]
|
|
Translating task: [0.660s CPU, 0.657s wall-clock]
|
|
2326 effect conditions simplified
|
|
0 implied preconditions added
|
|
Detecting unreachable propositions...
|
|
0 operators removed
|
|
0 axioms removed
|
|
3 propositions removed
|
|
Detecting unreachable propositions: [0.310s CPU, 0.308s wall-clock]
|
|
Reordering and filtering variables...
|
|
210 of 210 variables necessary.
|
|
11 of 14 mutex groups necessary.
|
|
1390 of 1390 operators necessary.
|
|
0 of 0 axiom rules necessary.
|
|
Reordering and filtering variables: [0.210s CPU, 0.207s wall-clock]
|
|
Translator variables: 210
|
|
Translator derived variables: 0
|
|
Translator facts: 441
|
|
Translator goal facts: 9
|
|
Translator mutex groups: 11
|
|
Translator total mutex groups size: 33
|
|
Translator operators: 1390
|
|
Translator axioms: 0
|
|
Translator task size: 13333
|
|
Translator peak memory: 43980 KB
|
|
Writing output... [0.260s CPU, 0.271s wall-clock]
|
|
Done! [2.640s CPU, 2.663s wall-clock]
|
|
planner.py version 0.0.1
|
|
|
|
Time: 0.57s
|
|
Memory: 86MB
|
|
|
|
Iteration 1
|
|
Queue: [(0,0,0,True), (1,5,0,True), (2,10,0,True), (3,15,0,True), (4,20,0,True), (5,25,0,True), (6,30,0,True)]
|
|
Grounded Until: 0
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0
|
|
Calls : 1
|
|
Time : 0.658s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
|
|
CPU Time : 0.568s
|
|
|
|
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 : 38518
|
|
Atoms : 38518
|
|
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 : 222MB
|
|
Max. Length : 0 steps
|
|
Models : 0
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 0.00s
|
|
Memory: 158MB (+72MB)
|
|
UNSAT
|
|
Iteration Time: 0.00s
|
|
|
|
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: 158MB
|
|
Grounding... [('step', [1]), ('step', [2]), ('step', [3]), ('step', [4]), ('step', [5]), ('check', [5])]
|
|
Grounding Time: 0.15s
|
|
Memory: 158MB (+0MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 1+
|
|
Calls : 2
|
|
Time : 0.982s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
|
|
CPU Time : 0.892s
|
|
|
|
Choices : 152 (Domain: 73)
|
|
Conflicts : 2 (Analyzed: 2)
|
|
Restarts : 0
|
|
Model-Level : 147.0
|
|
Problems : 2 (Average Length: 4.50 Splits: 0)
|
|
Lemmas : 2 (Deleted: 0)
|
|
Binary : 0 (Ratio: 0.00%)
|
|
Ternary : 0 (Ratio: 0.00%)
|
|
Conflict : 2 (Average Length: 23.0 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 2 (Average: 6.00 Max: 11 Sum: 12)
|
|
Executed : 2 (Average: 6.00 Max: 11 Sum: 12 Ratio: 100.00%)
|
|
Bounded : 0 (Average: 0.00 Max: 0 Sum: 0 Ratio: 0.00%)
|
|
|
|
Rules : 38518
|
|
Atoms : 38518
|
|
Bodies : 1 (Original: 0)
|
|
Tight : Yes
|
|
Variables : 10322 (Eliminated: 0 Frozen: 10322)
|
|
Constraints : 36431 (Binary: 95.0% Ternary: 3.5% Other: 1.5%)
|
|
|
|
Memory Peak : 222MB
|
|
Max. Length : 0 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 0.10s
|
|
Memory: 160MB (+2MB)
|
|
SAT
|
|
Testing...
|
|
NOT SERIALIZABLE
|
|
Testing Time: 0.58s
|
|
Memory: 178MB (+18MB)
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0
|
|
Calls : 3
|
|
Time : 1.081s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
|
|
CPU Time : 0.992s
|
|
|
|
Choices : 161 (Domain: 78)
|
|
Conflicts : 9 (Analyzed: 8)
|
|
Restarts : 0
|
|
Model-Level : 147.0
|
|
Problems : 3 (Average Length: 5.33 Splits: 0)
|
|
Lemmas : 8 (Deleted: 0)
|
|
Binary : 1 (Ratio: 12.50%)
|
|
Ternary : 2 (Ratio: 25.00%)
|
|
Conflict : 8 (Average Length: 8.4 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 8 (Average: 2.75 Max: 11 Sum: 22)
|
|
Executed : 7 (Average: 2.62 Max: 11 Sum: 21 Ratio: 95.45%)
|
|
Bounded : 1 (Average: 1.00 Max: 1 Sum: 1 Ratio: 4.55%)
|
|
|
|
Rules : 55133 (Original: 53913)
|
|
Atoms : 43853
|
|
Bodies : 10280 (Original: 9059)
|
|
Count : 232 (Original: 476)
|
|
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
|
|
Tight : Yes
|
|
Variables : 12735 (Eliminated: 1464 Frozen: 11271)
|
|
Constraints : 50631 (Binary: 90.2% Ternary: 5.9% Other: 3.9%)
|
|
|
|
Memory Peak : 222MB
|
|
Max. Length : 0 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 0.02s
|
|
Memory: 178MB (+0MB)
|
|
UNSAT
|
|
Iteration Time: 0.93s
|
|
|
|
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: 180.0MB
|
|
Grounding... [('step', [6]), ('step', [7]), ('step', [8]), ('step', [9]), ('step', [10]), ('check', [10])]
|
|
Grounding Time: 0.29s
|
|
Memory: 178MB (+0MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0
|
|
Calls : 4
|
|
Time : 2.170s (Solving: 0.38s 1st Model: 0.00s Unsat: 0.38s)
|
|
CPU Time : 2.080s
|
|
|
|
Choices : 12799 (Domain: 10798)
|
|
Conflicts : 1643 (Analyzed: 1641)
|
|
Restarts : 10 (Average: 164.10 Last: 20)
|
|
Model-Level : 147.0
|
|
Problems : 4 (Average Length: 7.00 Splits: 0)
|
|
Lemmas : 1641 (Deleted: 0)
|
|
Binary : 185 (Ratio: 11.27%)
|
|
Ternary : 187 (Ratio: 11.40%)
|
|
Conflict : 1641 (Average Length: 27.6 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 1641 (Average: 7.73 Max: 79 Sum: 12687)
|
|
Executed : 1623 (Average: 7.62 Max: 79 Sum: 12504 Ratio: 98.56%)
|
|
Bounded : 18 (Average: 10.17 Max: 12 Sum: 183 Ratio: 1.44%)
|
|
|
|
Rules : 55133 (Original: 53913)
|
|
Atoms : 43853
|
|
Bodies : 10280 (Original: 9059)
|
|
Count : 232 (Original: 476)
|
|
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
|
|
Tight : Yes
|
|
Variables : 35311 (Eliminated: 1464 Frozen: 26317)
|
|
Constraints : 223676 (Binary: 91.3% Ternary: 6.4% Other: 2.3%)
|
|
|
|
Memory Peak : 222MB
|
|
Max. Length : 5 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 0.70s
|
|
Memory: 189MB (+11MB)
|
|
UNSAT
|
|
Iteration Time: 1.10s
|
|
|
|
Iteration 4
|
|
Queue: [(3,15,0,True), (4,20,0,True), (5,25,0,True), (6,30,0,True)]
|
|
Grounded Until: 10
|
|
Expected Memory: 200.0MB
|
|
Grounding... [('step', [11]), ('step', [12]), ('step', [13]), ('step', [14]), ('step', [15]), ('check', [15])]
|
|
Grounding Time: 0.38s
|
|
Memory: 195MB (+6MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0
|
|
Calls : 5
|
|
Time : 6.807s (Solving: 4.20s 1st Model: 0.00s Unsat: 4.20s)
|
|
CPU Time : 6.720s
|
|
|
|
Choices : 95323 (Domain: 72132)
|
|
Conflicts : 13704 (Analyzed: 13701)
|
|
Restarts : 61 (Average: 224.61 Last: 168)
|
|
Model-Level : 147.0
|
|
Problems : 5 (Average Length: 9.00 Splits: 0)
|
|
Lemmas : 13701 (Deleted: 7320)
|
|
Binary : 884 (Ratio: 6.45%)
|
|
Ternary : 495 (Ratio: 3.61%)
|
|
Conflict : 13701 (Average Length: 196.3 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 13701 (Average: 6.83 Max: 380 Sum: 93639)
|
|
Executed : 13664 (Average: 6.80 Max: 380 Sum: 93177 Ratio: 99.51%)
|
|
Bounded : 37 (Average: 12.49 Max: 17 Sum: 462 Ratio: 0.49%)
|
|
|
|
Rules : 55133 (Original: 53913)
|
|
Atoms : 43853
|
|
Bodies : 10280 (Original: 9059)
|
|
Count : 232 (Original: 476)
|
|
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
|
|
Tight : Yes
|
|
Variables : 57887 (Eliminated: 1464 Frozen: 48893)
|
|
Constraints : 381121 (Binary: 91.6% Ternary: 6.3% Other: 2.1%)
|
|
|
|
Memory Peak : 222MB
|
|
Max. Length : 10 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 4.14s
|
|
Memory: 209MB (+14MB)
|
|
UNSAT
|
|
Iteration Time: 4.65s
|
|
|
|
Iteration 5
|
|
Queue: [(4,20,0,True), (5,25,0,True), (6,30,0,True)]
|
|
Grounded Until: 15
|
|
Expected Memory: 229.0MB
|
|
Grounding... [('step', [16]), ('step', [17]), ('step', [18]), ('step', [19]), ('step', [20]), ('check', [20])]
|
|
Grounding Time: 0.30s
|
|
Memory: 212MB (+3MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 6
|
|
Time : 21.097s (Solving: 17.72s 1st Model: 0.00s Unsat: 4.20s)
|
|
CPU Time : 21.012s
|
|
|
|
Choices : 318692 (Domain: 274484)
|
|
Conflicts : 41885 (Analyzed: 41882)
|
|
Restarts : 161 (Average: 260.14 Last: 200)
|
|
Model-Level : 147.0
|
|
Problems : 6 (Average Length: 11.17 Splits: 0)
|
|
Lemmas : 41882 (Deleted: 27757)
|
|
Binary : 2114 (Ratio: 5.05%)
|
|
Ternary : 772 (Ratio: 1.84%)
|
|
Conflict : 41882 (Average Length: 420.1 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 41882 (Average: 7.36 Max: 431 Sum: 308320)
|
|
Executed : 41843 (Average: 7.35 Max: 431 Sum: 307814 Ratio: 99.84%)
|
|
Bounded : 39 (Average: 12.97 Max: 22 Sum: 506 Ratio: 0.16%)
|
|
|
|
Rules : 55133 (Original: 53913)
|
|
Atoms : 43853
|
|
Bodies : 10280 (Original: 9059)
|
|
Count : 232 (Original: 476)
|
|
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
|
|
Tight : Yes
|
|
Variables : 80463 (Eliminated: 1464 Frozen: 71469)
|
|
Constraints : 538293 (Binary: 91.6% Ternary: 6.4% Other: 2.1%)
|
|
|
|
Memory Peak : 227MB
|
|
Max. Length : 15 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 13.86s
|
|
Memory: 227MB (+15MB)
|
|
UNKNOWN
|
|
Iteration Time: 14.30s
|
|
|
|
Iteration 6
|
|
Queue: [(5,25,0,True), (6,30,0,True)]
|
|
Grounded Until: 20
|
|
Expected Memory: 247.0MB
|
|
Grounding... [('step', [21]), ('step', [22]), ('step', [23]), ('step', [24]), ('step', [25]), ('check', [25])]
|
|
Grounding Time: 0.31s
|
|
Memory: 230MB (+3MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 7
|
|
Time : 38.488s (Solving: 34.32s 1st Model: 0.00s Unsat: 4.20s)
|
|
CPU Time : 38.412s
|
|
|
|
Choices : 544925 (Domain: 486198)
|
|
Conflicts : 70044 (Analyzed: 70041)
|
|
Restarts : 261 (Average: 268.36 Last: 203)
|
|
Model-Level : 147.0
|
|
Problems : 7 (Average Length: 13.43 Splits: 0)
|
|
Lemmas : 70041 (Deleted: 53675)
|
|
Binary : 3314 (Ratio: 4.73%)
|
|
Ternary : 972 (Ratio: 1.39%)
|
|
Conflict : 70041 (Average Length: 595.2 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 70041 (Average: 7.41 Max: 431 Sum: 518924)
|
|
Executed : 70002 (Average: 7.40 Max: 431 Sum: 518418 Ratio: 99.90%)
|
|
Bounded : 39 (Average: 12.97 Max: 22 Sum: 506 Ratio: 0.10%)
|
|
|
|
Rules : 55133 (Original: 53913)
|
|
Atoms : 43853
|
|
Bodies : 10280 (Original: 9059)
|
|
Count : 232 (Original: 476)
|
|
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
|
|
Tight : Yes
|
|
Variables : 103039 (Eliminated: 1464 Frozen: 94045)
|
|
Constraints : 711310 (Binary: 91.6% Ternary: 6.4% Other: 2.0%)
|
|
|
|
Memory Peak : 246MB
|
|
Max. Length : 20 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 16.94s
|
|
Memory: 242MB (+12MB)
|
|
UNKNOWN
|
|
Iteration Time: 17.40s
|
|
|
|
Iteration 7
|
|
Queue: [(6,30,0,True)]
|
|
Grounded Until: 25
|
|
Expected Memory: 262.0MB
|
|
Grounding... [('step', [26]), ('step', [27]), ('step', [28]), ('step', [29]), ('step', [30]), ('check', [30])]
|
|
Grounding Time: 0.36s
|
|
Memory: 244MB (+2MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 8
|
|
Time : 58.835s (Solving: 53.79s 1st Model: 0.00s Unsat: 4.20s)
|
|
CPU Time : 58.768s
|
|
|
|
Choices : 795479 (Domain: 727093)
|
|
Conflicts : 98170 (Analyzed: 98167)
|
|
Restarts : 361 (Average: 271.93 Last: 203)
|
|
Model-Level : 147.0
|
|
Problems : 8 (Average Length: 15.75 Splits: 0)
|
|
Lemmas : 98167 (Deleted: 80033)
|
|
Binary : 4642 (Ratio: 4.73%)
|
|
Ternary : 1200 (Ratio: 1.22%)
|
|
Conflict : 98167 (Average Length: 701.2 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 98167 (Average: 7.65 Max: 431 Sum: 751388)
|
|
Executed : 98127 (Average: 7.65 Max: 431 Sum: 750850 Ratio: 99.93%)
|
|
Bounded : 40 (Average: 13.45 Max: 32 Sum: 538 Ratio: 0.07%)
|
|
|
|
Rules : 55133 (Original: 53913)
|
|
Atoms : 43853
|
|
Bodies : 10280 (Original: 9059)
|
|
Count : 232 (Original: 476)
|
|
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
|
|
Tight : Yes
|
|
Variables : 125615 (Eliminated: 1464 Frozen: 116621)
|
|
Constraints : 884355 (Binary: 91.6% Ternary: 6.4% Other: 2.0%)
|
|
|
|
Memory Peak : 390MB
|
|
Max. Length : 25 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 19.83s
|
|
Memory: 326MB (+82MB)
|
|
UNKNOWN
|
|
Iteration Time: 20.36s
|
|
|
|
Iteration 8
|
|
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), (17,85,0,True)]
|
|
Grounded Until: 30
|
|
Blocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 9
|
|
Time : 73.429s (Solving: 68.35s 1st Model: 0.00s Unsat: 4.20s)
|
|
CPU Time : 73.368s
|
|
|
|
Choices : 908988 (Domain: 840602)
|
|
Conflicts : 126350 (Analyzed: 126347)
|
|
Restarts : 461 (Average: 274.07 Last: 203)
|
|
Model-Level : 147.0
|
|
Problems : 9 (Average Length: 17.56 Splits: 0)
|
|
Lemmas : 126347 (Deleted: 107054)
|
|
Binary : 5110 (Ratio: 4.04%)
|
|
Ternary : 1272 (Ratio: 1.01%)
|
|
Conflict : 126347 (Average Length: 680.7 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 126347 (Average: 6.80 Max: 431 Sum: 859482)
|
|
Executed : 126306 (Average: 6.80 Max: 431 Sum: 858912 Ratio: 99.93%)
|
|
Bounded : 41 (Average: 13.90 Max: 32 Sum: 570 Ratio: 0.07%)
|
|
|
|
Rules : 55133 (Original: 53913)
|
|
Atoms : 43853
|
|
Bodies : 10280 (Original: 9059)
|
|
Count : 232 (Original: 476)
|
|
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
|
|
Tight : Yes
|
|
Variables : 125615 (Eliminated: 1464 Frozen: 124151)
|
|
Constraints : 884341 (Binary: 91.6% Ternary: 6.4% Other: 2.0%)
|
|
|
|
Memory Peak : 390MB
|
|
Max. Length : 30 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 14.58s
|
|
Memory: 326MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 14.60s
|
|
|
|
Iteration 9
|
|
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), (17,85,0,True)]
|
|
Grounded Until: 30
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 10
|
|
Time : 98.747s (Solving: 93.63s 1st Model: 0.00s Unsat: 4.20s)
|
|
CPU Time : 98.696s
|
|
|
|
Choices : 1039074 (Domain: 970650)
|
|
Conflicts : 154469 (Analyzed: 154466)
|
|
Restarts : 561 (Average: 275.34 Last: 204)
|
|
Model-Level : 147.0
|
|
Problems : 10 (Average Length: 19.00 Splits: 0)
|
|
Lemmas : 154466 (Deleted: 134626)
|
|
Binary : 5352 (Ratio: 3.46%)
|
|
Ternary : 1336 (Ratio: 0.86%)
|
|
Conflict : 154466 (Average Length: 791.7 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 154466 (Average: 6.32 Max: 431 Sum: 976481)
|
|
Executed : 154424 (Average: 6.32 Max: 431 Sum: 975879 Ratio: 99.94%)
|
|
Bounded : 42 (Average: 14.33 Max: 32 Sum: 602 Ratio: 0.06%)
|
|
|
|
Rules : 55133 (Original: 53913)
|
|
Atoms : 43853
|
|
Bodies : 10280 (Original: 9059)
|
|
Count : 232 (Original: 476)
|
|
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
|
|
Tight : Yes
|
|
Variables : 125615 (Eliminated: 1464 Frozen: 124151)
|
|
Constraints : 884328 (Binary: 91.6% Ternary: 6.4% Other: 2.0%)
|
|
|
|
Memory Peak : 390MB
|
|
Max. Length : 30 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 25.32s
|
|
Memory: 326MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 25.33s
|
|
|
|
Iteration 10
|
|
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), (17,85,0,True)]
|
|
Grounded Until: 30
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 11
|
|
Time : 121.765s (Solving: 116.61s 1st Model: 0.00s Unsat: 4.20s)
|
|
CPU Time : 121.724s
|
|
|
|
Choices : 1259852 (Domain: 1190405)
|
|
Conflicts : 182648 (Analyzed: 182645)
|
|
Restarts : 661 (Average: 276.32 Last: 204)
|
|
Model-Level : 147.0
|
|
Problems : 11 (Average Length: 20.18 Splits: 0)
|
|
Lemmas : 182645 (Deleted: 161750)
|
|
Binary : 5826 (Ratio: 3.19%)
|
|
Ternary : 1427 (Ratio: 0.78%)
|
|
Conflict : 182645 (Average Length: 840.8 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 182645 (Average: 6.46 Max: 431 Sum: 1180686)
|
|
Executed : 182602 (Average: 6.46 Max: 431 Sum: 1180052 Ratio: 99.95%)
|
|
Bounded : 43 (Average: 14.74 Max: 32 Sum: 634 Ratio: 0.05%)
|
|
|
|
Rules : 55133 (Original: 53913)
|
|
Atoms : 43853
|
|
Bodies : 10280 (Original: 9059)
|
|
Count : 232 (Original: 476)
|
|
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
|
|
Tight : Yes
|
|
Variables : 125615 (Eliminated: 1464 Frozen: 124151)
|
|
Constraints : 884314 (Binary: 91.6% Ternary: 6.4% Other: 2.0%)
|
|
|
|
Memory Peak : 390MB
|
|
Max. Length : 30 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 23.01s
|
|
Memory: 326MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 23.03s
|
|
|
|
Iteration 11
|
|
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), (17,85,0,True)]
|
|
Grounded Until: 30
|
|
Expected Memory: 410.0MB
|
|
Grounding... [('step', [31]), ('step', [32]), ('step', [33]), ('step', [34]), ('step', [35]), ('check', [35])]
|
|
Grounding Time: 0.32s
|
|
Memory: 327MB (+1MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 12
|
|
Time : 140.038s (Solving: 134.04s 1st Model: 0.00s Unsat: 4.20s)
|
|
CPU Time : 140.004s
|
|
|
|
Choices : 1469681 (Domain: 1393123)
|
|
Conflicts : 210833 (Analyzed: 210830)
|
|
Restarts : 761 (Average: 277.04 Last: 204)
|
|
Model-Level : 147.0
|
|
Problems : 12 (Average Length: 21.58 Splits: 0)
|
|
Lemmas : 210830 (Deleted: 188096)
|
|
Binary : 6845 (Ratio: 3.25%)
|
|
Ternary : 1557 (Ratio: 0.74%)
|
|
Conflict : 210830 (Average Length: 847.9 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 210830 (Average: 6.49 Max: 431 Sum: 1369029)
|
|
Executed : 210786 (Average: 6.49 Max: 431 Sum: 1368358 Ratio: 99.95%)
|
|
Bounded : 44 (Average: 15.25 Max: 37 Sum: 671 Ratio: 0.05%)
|
|
|
|
Rules : 55133 (Original: 53913)
|
|
Atoms : 43853
|
|
Bodies : 10280 (Original: 9059)
|
|
Count : 232 (Original: 476)
|
|
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
|
|
Tight : Yes
|
|
Variables : 148191 (Eliminated: 1464 Frozen: 139197)
|
|
Constraints : 1057342 (Binary: 91.6% Ternary: 6.5% Other: 2.0%)
|
|
|
|
Memory Peak : 390MB
|
|
Max. Length : 30 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 17.78s
|
|
Memory: 341MB (+14MB)
|
|
UNKNOWN
|
|
Iteration Time: 18.29s
|
|
|
|
Iteration 12
|
|
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), (17,85,0,True)]
|
|
Grounded Until: 35
|
|
Expected Memory: 425.0MB
|
|
Grounding... [('step', [36]), ('step', [37]), ('step', [38]), ('step', [39]), ('step', [40]), ('check', [40])]
|
|
Grounding Time: 0.42s
|
|
Memory: 348MB (+7MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 13
|
|
Time : 158.318s (Solving: 151.36s 1st Model: 0.00s Unsat: 4.20s)
|
|
CPU Time : 158.292s
|
|
|
|
Choices : 1722991 (Domain: 1639840)
|
|
Conflicts : 239049 (Analyzed: 239046)
|
|
Restarts : 861 (Average: 277.64 Last: 204)
|
|
Model-Level : 147.0
|
|
Problems : 13 (Average Length: 23.15 Splits: 0)
|
|
Lemmas : 239046 (Deleted: 215086)
|
|
Binary : 7595 (Ratio: 3.18%)
|
|
Ternary : 1618 (Ratio: 0.68%)
|
|
Conflict : 239046 (Average Length: 840.7 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 239046 (Average: 6.70 Max: 431 Sum: 1600769)
|
|
Executed : 239002 (Average: 6.69 Max: 431 Sum: 1600098 Ratio: 99.96%)
|
|
Bounded : 44 (Average: 15.25 Max: 37 Sum: 671 Ratio: 0.04%)
|
|
|
|
Rules : 55133 (Original: 53913)
|
|
Atoms : 43853
|
|
Bodies : 10280 (Original: 9059)
|
|
Count : 232 (Original: 476)
|
|
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
|
|
Tight : Yes
|
|
Variables : 170767 (Eliminated: 1464 Frozen: 161773)
|
|
Constraints : 1230373 (Binary: 91.6% Ternary: 6.5% Other: 2.0%)
|
|
|
|
Memory Peak : 390MB
|
|
Max. Length : 35 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 17.68s
|
|
Memory: 362MB (+14MB)
|
|
UNKNOWN
|
|
Iteration Time: 18.29s
|
|
|
|
Iteration 13
|
|
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), (17,85,0,True)]
|
|
Grounded Until: 40
|
|
Expected Memory: 446.0MB
|
|
Grounding... [('step', [41]), ('step', [42]), ('step', [43]), ('step', [44]), ('step', [45]), ('check', [45])]
|
|
Grounding Time: 0.31s
|
|
Memory: 366MB (+4MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 14
|
|
Time : 175.477s (Solving: 167.66s 1st Model: 0.00s Unsat: 4.20s)
|
|
CPU Time : 175.456s
|
|
|
|
Choices : 1976070 (Domain: 1888390)
|
|
Conflicts : 267225 (Analyzed: 267222)
|
|
Restarts : 961 (Average: 278.07 Last: 204)
|
|
Model-Level : 147.0
|
|
Problems : 14 (Average Length: 24.86 Splits: 0)
|
|
Lemmas : 267222 (Deleted: 241788)
|
|
Binary : 8210 (Ratio: 3.07%)
|
|
Ternary : 1715 (Ratio: 0.64%)
|
|
Conflict : 267222 (Average Length: 830.5 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 267222 (Average: 6.86 Max: 431 Sum: 1833630)
|
|
Executed : 267178 (Average: 6.86 Max: 431 Sum: 1832959 Ratio: 99.96%)
|
|
Bounded : 44 (Average: 15.25 Max: 37 Sum: 671 Ratio: 0.04%)
|
|
|
|
Rules : 55133 (Original: 53913)
|
|
Atoms : 43853
|
|
Bodies : 10280 (Original: 9059)
|
|
Count : 232 (Original: 476)
|
|
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
|
|
Tight : Yes
|
|
Variables : 193343 (Eliminated: 1464 Frozen: 184349)
|
|
Constraints : 1403418 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
|
|
|
|
Memory Peak : 391MB
|
|
Max. Length : 40 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 16.67s
|
|
Memory: 389MB (+23MB)
|
|
UNKNOWN
|
|
Iteration Time: 17.18s
|
|
|
|
Iteration 14
|
|
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), (17,85,0,True)]
|
|
Grounded Until: 45
|
|
Expected Memory: 473.0MB
|
|
Grounding... [('step', [46]), ('step', [47]), ('step', [48]), ('step', [49]), ('step', [50]), ('check', [50])]
|
|
Grounding Time: 0.32s
|
|
Memory: 389MB (+0MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 15
|
|
Time : 193.509s (Solving: 184.81s 1st Model: 0.00s Unsat: 4.20s)
|
|
CPU Time : 193.496s
|
|
|
|
Choices : 2212664 (Domain: 2122911)
|
|
Conflicts : 295414 (Analyzed: 295411)
|
|
Restarts : 1061 (Average: 278.43 Last: 204)
|
|
Model-Level : 147.0
|
|
Problems : 15 (Average Length: 26.67 Splits: 0)
|
|
Lemmas : 295411 (Deleted: 268828)
|
|
Binary : 8624 (Ratio: 2.92%)
|
|
Ternary : 1761 (Ratio: 0.60%)
|
|
Conflict : 295411 (Average Length: 827.8 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 295411 (Average: 6.94 Max: 431 Sum: 2050016)
|
|
Executed : 295365 (Average: 6.94 Max: 431 Sum: 2049241 Ratio: 99.96%)
|
|
Bounded : 46 (Average: 16.85 Max: 52 Sum: 775 Ratio: 0.04%)
|
|
|
|
Rules : 55133 (Original: 53913)
|
|
Atoms : 43853
|
|
Bodies : 10280 (Original: 9059)
|
|
Count : 232 (Original: 476)
|
|
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
|
|
Tight : Yes
|
|
Variables : 215919 (Eliminated: 1464 Frozen: 206925)
|
|
Constraints : 1576463 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
|
|
|
|
Memory Peak : 419MB
|
|
Max. Length : 45 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 17.51s
|
|
Memory: 403MB (+14MB)
|
|
UNKNOWN
|
|
Iteration Time: 18.05s
|
|
|
|
Iteration 15
|
|
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), (17,85,0,True)]
|
|
Grounded Until: 50
|
|
Expected Memory: 487.0MB
|
|
Grounding... [('step', [51]), ('step', [52]), ('step', [53]), ('step', [54]), ('step', [55]), ('check', [55])]
|
|
Grounding Time: 0.32s
|
|
Memory: 403MB (+0MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 16
|
|
Time : 212.232s (Solving: 202.65s 1st Model: 0.00s Unsat: 4.20s)
|
|
CPU Time : 212.228s
|
|
|
|
Choices : 2583279 (Domain: 2479786)
|
|
Conflicts : 323565 (Analyzed: 323562)
|
|
Restarts : 1161 (Average: 278.69 Last: 204)
|
|
Model-Level : 147.0
|
|
Problems : 16 (Average Length: 28.56 Splits: 0)
|
|
Lemmas : 323562 (Deleted: 295387)
|
|
Binary : 9565 (Ratio: 2.96%)
|
|
Ternary : 1916 (Ratio: 0.59%)
|
|
Conflict : 323562 (Average Length: 836.5 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 323562 (Average: 7.38 Max: 431 Sum: 2387890)
|
|
Executed : 323516 (Average: 7.38 Max: 431 Sum: 2387115 Ratio: 99.97%)
|
|
Bounded : 46 (Average: 16.85 Max: 52 Sum: 775 Ratio: 0.03%)
|
|
|
|
Rules : 55133 (Original: 53913)
|
|
Atoms : 43853
|
|
Bodies : 10280 (Original: 9059)
|
|
Count : 232 (Original: 476)
|
|
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
|
|
Tight : Yes
|
|
Variables : 238495 (Eliminated: 1464 Frozen: 229501)
|
|
Constraints : 1749480 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
|
|
|
|
Memory Peak : 437MB
|
|
Max. Length : 50 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 18.21s
|
|
Memory: 417MB (+14MB)
|
|
UNKNOWN
|
|
Iteration Time: 18.74s
|
|
|
|
Iteration 16
|
|
Queue: [(12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True), (17,85,0,True)]
|
|
Grounded Until: 55
|
|
Expected Memory: 501.0MB
|
|
Grounding... [('step', [56]), ('step', [57]), ('step', [58]), ('step', [59]), ('step', [60]), ('check', [60])]
|
|
Grounding Time: 0.36s
|
|
Memory: 417MB (+0MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 17
|
|
Time : 231.016s (Solving: 220.49s 1st Model: 0.00s Unsat: 4.20s)
|
|
CPU Time : 231.020s
|
|
|
|
Choices : 2835214 (Domain: 2730967)
|
|
Conflicts : 351769 (Analyzed: 351766)
|
|
Restarts : 1261 (Average: 278.96 Last: 204)
|
|
Model-Level : 147.0
|
|
Problems : 17 (Average Length: 30.53 Splits: 0)
|
|
Lemmas : 351766 (Deleted: 322486)
|
|
Binary : 9951 (Ratio: 2.83%)
|
|
Ternary : 1978 (Ratio: 0.56%)
|
|
Conflict : 351766 (Average Length: 825.1 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 351766 (Average: 7.44 Max: 431 Sum: 2618009)
|
|
Executed : 351719 (Average: 7.44 Max: 431 Sum: 2617172 Ratio: 99.97%)
|
|
Bounded : 47 (Average: 17.81 Max: 62 Sum: 837 Ratio: 0.03%)
|
|
|
|
Rules : 55133 (Original: 53913)
|
|
Atoms : 43853
|
|
Bodies : 10280 (Original: 9059)
|
|
Count : 232 (Original: 476)
|
|
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
|
|
Tight : Yes
|
|
Variables : 261071 (Eliminated: 1464 Frozen: 252077)
|
|
Constraints : 1922525 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
|
|
|
|
Memory Peak : 454MB
|
|
Max. Length : 55 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 18.21s
|
|
Memory: 432MB (+15MB)
|
|
UNKNOWN
|
|
Iteration Time: 18.80s
|
|
|
|
Iteration 17
|
|
Queue: [(13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True), (17,85,0,True)]
|
|
Grounded Until: 60
|
|
Expected Memory: 516.0MB
|
|
Grounding... [('step', [61]), ('step', [62]), ('step', [63]), ('step', [64]), ('step', [65]), ('check', [65])]
|
|
Grounding Time: 0.35s
|
|
Memory: 432MB (+0MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 18
|
|
Time : 251.557s (Solving: 240.07s 1st Model: 0.00s Unsat: 4.20s)
|
|
CPU Time : 251.568s
|
|
|
|
Choices : 3279607 (Domain: 3169584)
|
|
Conflicts : 379925 (Analyzed: 379922)
|
|
Restarts : 1361 (Average: 279.15 Last: 204)
|
|
Model-Level : 147.0
|
|
Problems : 18 (Average Length: 32.56 Splits: 0)
|
|
Lemmas : 379922 (Deleted: 348956)
|
|
Binary : 11063 (Ratio: 2.91%)
|
|
Ternary : 2142 (Ratio: 0.56%)
|
|
Conflict : 379922 (Average Length: 826.5 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 379922 (Average: 7.96 Max: 431 Sum: 3025976)
|
|
Executed : 379875 (Average: 7.96 Max: 431 Sum: 3025139 Ratio: 99.97%)
|
|
Bounded : 47 (Average: 17.81 Max: 62 Sum: 837 Ratio: 0.03%)
|
|
|
|
Rules : 55133 (Original: 53913)
|
|
Atoms : 43853
|
|
Bodies : 10280 (Original: 9059)
|
|
Count : 232 (Original: 476)
|
|
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
|
|
Tight : Yes
|
|
Variables : 283647 (Eliminated: 1464 Frozen: 274653)
|
|
Constraints : 2095556 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
|
|
|
|
Memory Peak : 471MB
|
|
Max. Length : 60 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 19.96s
|
|
Memory: 465MB (+33MB)
|
|
UNKNOWN
|
|
Iteration Time: 20.56s
|
|
|
|
Iteration 18
|
|
Queue: [(14,70,0,True), (15,75,0,True), (16,80,0,True), (17,85,0,True)]
|
|
Grounded Until: 65
|
|
Expected Memory: 549.0MB
|
|
Grounding... [('step', [66]), ('step', [67]), ('step', [68]), ('step', [69]), ('step', [70]), ('check', [70])]
|
|
Grounding Time: 0.33s
|
|
Memory: 465MB (+0MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 19
|
|
Time : 273.683s (Solving: 261.27s 1st Model: 0.00s Unsat: 4.20s)
|
|
CPU Time : 273.704s
|
|
|
|
Choices : 3620280 (Domain: 3509710)
|
|
Conflicts : 408106 (Analyzed: 408103)
|
|
Restarts : 1461 (Average: 279.33 Last: 204)
|
|
Model-Level : 147.0
|
|
Problems : 19 (Average Length: 34.63 Splits: 0)
|
|
Lemmas : 408103 (Deleted: 375917)
|
|
Binary : 11570 (Ratio: 2.84%)
|
|
Ternary : 2226 (Ratio: 0.55%)
|
|
Conflict : 408103 (Average Length: 829.8 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 408103 (Average: 8.18 Max: 431 Sum: 3337540)
|
|
Executed : 408056 (Average: 8.18 Max: 431 Sum: 3336703 Ratio: 99.97%)
|
|
Bounded : 47 (Average: 17.81 Max: 62 Sum: 837 Ratio: 0.03%)
|
|
|
|
Rules : 55133 (Original: 53913)
|
|
Atoms : 43853
|
|
Bodies : 10280 (Original: 9059)
|
|
Count : 232 (Original: 476)
|
|
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
|
|
Tight : Yes
|
|
Variables : 306223 (Eliminated: 1464 Frozen: 297229)
|
|
Constraints : 2268601 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
|
|
|
|
Memory Peak : 503MB
|
|
Max. Length : 65 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 21.57s
|
|
Memory: 477MB (+12MB)
|
|
UNKNOWN
|
|
Iteration Time: 22.14s
|
|
|
|
Iteration 19
|
|
Queue: [(15,75,0,True), (16,80,0,True), (17,85,0,True)]
|
|
Grounded Until: 70
|
|
Expected Memory: 561.0MB
|
|
Grounding... [('step', [71]), ('step', [72]), ('step', [73]), ('step', [74]), ('step', [75]), ('check', [75])]
|
|
Grounding Time: 0.34s
|
|
Memory: 477MB (+0MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 20
|
|
Time : 294.476s (Solving: 281.11s 1st Model: 0.00s Unsat: 4.20s)
|
|
CPU Time : 294.504s
|
|
|
|
Choices : 4030873 (Domain: 3916810)
|
|
Conflicts : 436313 (Analyzed: 436310)
|
|
Restarts : 1561 (Average: 279.51 Last: 204)
|
|
Model-Level : 147.0
|
|
Problems : 20 (Average Length: 36.75 Splits: 0)
|
|
Lemmas : 436310 (Deleted: 401371)
|
|
Binary : 12272 (Ratio: 2.81%)
|
|
Ternary : 2334 (Ratio: 0.53%)
|
|
Conflict : 436310 (Average Length: 833.3 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 436310 (Average: 8.51 Max: 431 Sum: 3714399)
|
|
Executed : 436263 (Average: 8.51 Max: 431 Sum: 3713562 Ratio: 99.98%)
|
|
Bounded : 47 (Average: 17.81 Max: 62 Sum: 837 Ratio: 0.02%)
|
|
|
|
Rules : 55133 (Original: 53913)
|
|
Atoms : 43853
|
|
Bodies : 10280 (Original: 9059)
|
|
Count : 232 (Original: 476)
|
|
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
|
|
Tight : Yes
|
|
Variables : 328799 (Eliminated: 1464 Frozen: 319805)
|
|
Constraints : 2441646 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
|
|
|
|
Memory Peak : 518MB
|
|
Max. Length : 70 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 20.23s
|
|
Memory: 492MB (+15MB)
|
|
UNKNOWN
|
|
Iteration Time: 20.81s
|
|
|
|
Iteration 20
|
|
Queue: [(16,80,0,True), (17,85,0,True)]
|
|
Grounded Until: 75
|
|
Expected Memory: 576.0MB
|
|
Grounding... [('step', [76]), ('step', [77]), ('step', [78]), ('step', [79]), ('step', [80]), ('check', [80])]
|
|
Grounding Time: 0.48s
|
|
Memory: 507MB (+15MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 21
|
|
Time : 316.121s (Solving: 301.64s 1st Model: 0.00s Unsat: 4.20s)
|
|
CPU Time : 316.156s
|
|
|
|
Choices : 4363980 (Domain: 4249676)
|
|
Conflicts : 464504 (Analyzed: 464501)
|
|
Restarts : 1661 (Average: 279.65 Last: 204)
|
|
Model-Level : 147.0
|
|
Problems : 21 (Average Length: 38.90 Splits: 0)
|
|
Lemmas : 464501 (Deleted: 429631)
|
|
Binary : 12709 (Ratio: 2.74%)
|
|
Ternary : 2409 (Ratio: 0.52%)
|
|
Conflict : 464501 (Average Length: 830.6 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 464501 (Average: 8.65 Max: 431 Sum: 4016299)
|
|
Executed : 464453 (Average: 8.64 Max: 431 Sum: 4015380 Ratio: 99.98%)
|
|
Bounded : 48 (Average: 19.15 Max: 82 Sum: 919 Ratio: 0.02%)
|
|
|
|
Rules : 55133 (Original: 53913)
|
|
Atoms : 43853
|
|
Bodies : 10280 (Original: 9059)
|
|
Count : 232 (Original: 476)
|
|
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
|
|
Tight : Yes
|
|
Variables : 351375 (Eliminated: 1464 Frozen: 342381)
|
|
Constraints : 2614691 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
|
|
|
|
Memory Peak : 554MB
|
|
Max. Length : 75 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 20.92s
|
|
Memory: 521MB (+14MB)
|
|
UNKNOWN
|
|
Iteration Time: 21.66s
|
|
|
|
Iteration 21
|
|
Queue: [(17,85,0,True)]
|
|
Grounded Until: 80
|
|
Expected Memory: 605.0MB
|
|
Grounding... [('step', [81]), ('step', [82]), ('step', [83]), ('step', [84]), ('step', [85]), ('check', [85])]
|
|
Grounding Time: 0.32s
|
|
Memory: 521MB (+0MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 22
|
|
Time : 339.079s (Solving: 323.63s 1st Model: 0.00s Unsat: 4.20s)
|
|
CPU Time : 339.124s
|
|
|
|
Choices : 4698272 (Domain: 4583605)
|
|
Conflicts : 492648 (Analyzed: 492645)
|
|
Restarts : 1761 (Average: 279.75 Last: 204)
|
|
Model-Level : 147.0
|
|
Problems : 22 (Average Length: 41.09 Splits: 0)
|
|
Lemmas : 492645 (Deleted: 456973)
|
|
Binary : 13120 (Ratio: 2.66%)
|
|
Ternary : 2458 (Ratio: 0.50%)
|
|
Conflict : 492645 (Average Length: 839.4 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 492645 (Average: 8.75 Max: 431 Sum: 4309179)
|
|
Executed : 492597 (Average: 8.75 Max: 431 Sum: 4308260 Ratio: 99.98%)
|
|
Bounded : 48 (Average: 19.15 Max: 82 Sum: 919 Ratio: 0.02%)
|
|
|
|
Rules : 55133 (Original: 53913)
|
|
Atoms : 43853
|
|
Bodies : 10280 (Original: 9059)
|
|
Count : 232 (Original: 476)
|
|
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
|
|
Tight : Yes
|
|
Variables : 373951 (Eliminated: 1464 Frozen: 364957)
|
|
Constraints : 2787722 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
|
|
|
|
Memory Peak : 570MB
|
|
Max. Length : 80 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 22.39s
|
|
Memory: 535MB (+14MB)
|
|
UNKNOWN
|
|
Iteration Time: 22.97s
|
|
|
|
Iteration 22
|
|
Queue: [(4,20,2,True), (5,25,2,True), (6,30,2,True), (7,35,1,True), (8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
|
|
Grounded Until: 85
|
|
Blocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 23
|
|
Time : 350.517s (Solving: 334.98s 1st Model: 0.00s Unsat: 4.20s)
|
|
CPU Time : 350.568s
|
|
|
|
Choices : 4813255 (Domain: 4698588)
|
|
Conflicts : 520838 (Analyzed: 520835)
|
|
Restarts : 1861 (Average: 279.87 Last: 204)
|
|
Model-Level : 147.0
|
|
Problems : 23 (Average Length: 43.09 Splits: 0)
|
|
Lemmas : 520835 (Deleted: 484258)
|
|
Binary : 13398 (Ratio: 2.57%)
|
|
Ternary : 2506 (Ratio: 0.48%)
|
|
Conflict : 520835 (Average Length: 826.3 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 520835 (Average: 8.48 Max: 431 Sum: 4417398)
|
|
Executed : 520786 (Average: 8.48 Max: 431 Sum: 4416392 Ratio: 99.98%)
|
|
Bounded : 49 (Average: 20.53 Max: 87 Sum: 1006 Ratio: 0.02%)
|
|
|
|
Rules : 55133 (Original: 53913)
|
|
Atoms : 43853
|
|
Bodies : 10280 (Original: 9059)
|
|
Count : 232 (Original: 476)
|
|
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
|
|
Tight : Yes
|
|
Variables : 373951 (Eliminated: 1464 Frozen: 372487)
|
|
Constraints : 2787722 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
|
|
|
|
Memory Peak : 570MB
|
|
Max. Length : 85 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 11.41s
|
|
Memory: 537MB (+2MB)
|
|
UNKNOWN
|
|
Iteration Time: 11.45s
|
|
|
|
Iteration 23
|
|
Queue: [(5,25,2,True), (6,30,2,True), (7,35,1,True), (8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
|
|
Grounded Until: 85
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 24
|
|
Time : 376.151s (Solving: 360.52s 1st Model: 0.00s Unsat: 4.20s)
|
|
CPU Time : 376.216s
|
|
|
|
Choices : 4911678 (Domain: 4797011)
|
|
Conflicts : 548996 (Analyzed: 548993)
|
|
Restarts : 1961 (Average: 279.96 Last: 204)
|
|
Model-Level : 147.0
|
|
Problems : 24 (Average Length: 44.92 Splits: 0)
|
|
Lemmas : 548993 (Deleted: 511889)
|
|
Binary : 13480 (Ratio: 2.46%)
|
|
Ternary : 2531 (Ratio: 0.46%)
|
|
Conflict : 548993 (Average Length: 846.1 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 548993 (Average: 8.21 Max: 431 Sum: 4506436)
|
|
Executed : 548943 (Average: 8.21 Max: 431 Sum: 4505343 Ratio: 99.98%)
|
|
Bounded : 50 (Average: 21.86 Max: 87 Sum: 1093 Ratio: 0.02%)
|
|
|
|
Rules : 55133 (Original: 53913)
|
|
Atoms : 43853
|
|
Bodies : 10280 (Original: 9059)
|
|
Count : 232 (Original: 476)
|
|
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
|
|
Tight : Yes
|
|
Variables : 373951 (Eliminated: 1464 Frozen: 372487)
|
|
Constraints : 2787708 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
|
|
|
|
Memory Peak : 570MB
|
|
Max. Length : 85 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 25.61s
|
|
Memory: 537MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 25.65s
|
|
|
|
Iteration 24
|
|
Queue: [(6,30,2,True), (7,35,1,True), (8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
|
|
Grounded Until: 85
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 25
|
|
Time : 395.354s (Solving: 379.63s 1st Model: 0.00s Unsat: 4.20s)
|
|
CPU Time : 395.428s
|
|
|
|
Choices : 5101516 (Domain: 4986849)
|
|
Conflicts : 577235 (Analyzed: 577232)
|
|
Restarts : 2061 (Average: 280.07 Last: 204)
|
|
Model-Level : 147.0
|
|
Problems : 25 (Average Length: 46.60 Splits: 0)
|
|
Lemmas : 577232 (Deleted: 539550)
|
|
Binary : 13703 (Ratio: 2.37%)
|
|
Ternary : 2558 (Ratio: 0.44%)
|
|
Conflict : 577232 (Average Length: 861.7 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 577232 (Average: 8.11 Max: 431 Sum: 4678791)
|
|
Executed : 577182 (Average: 8.10 Max: 431 Sum: 4677698 Ratio: 99.98%)
|
|
Bounded : 50 (Average: 21.86 Max: 87 Sum: 1093 Ratio: 0.02%)
|
|
|
|
Rules : 55133 (Original: 53913)
|
|
Atoms : 43853
|
|
Bodies : 10280 (Original: 9059)
|
|
Count : 232 (Original: 476)
|
|
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
|
|
Tight : Yes
|
|
Variables : 373951 (Eliminated: 1464 Frozen: 372487)
|
|
Constraints : 2787694 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
|
|
|
|
Memory Peak : 570MB
|
|
Max. Length : 85 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 19.18s
|
|
Memory: 537MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 19.22s
|
|
|
|
Iteration 25
|
|
Queue: [(7,35,1,True), (8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
|
|
Grounded Until: 85
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 26
|
|
Time : 413.248s (Solving: 397.41s 1st Model: 0.00s Unsat: 4.20s)
|
|
CPU Time : 413.328s
|
|
|
|
Choices : 5288141 (Domain: 5173473)
|
|
Conflicts : 605398 (Analyzed: 605395)
|
|
Restarts : 2161 (Average: 280.15 Last: 204)
|
|
Model-Level : 147.0
|
|
Problems : 26 (Average Length: 48.15 Splits: 0)
|
|
Lemmas : 605395 (Deleted: 566903)
|
|
Binary : 13934 (Ratio: 2.30%)
|
|
Ternary : 2601 (Ratio: 0.43%)
|
|
Conflict : 605395 (Average Length: 864.4 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 605395 (Average: 8.01 Max: 431 Sum: 4847208)
|
|
Executed : 605345 (Average: 8.00 Max: 431 Sum: 4846115 Ratio: 99.98%)
|
|
Bounded : 50 (Average: 21.86 Max: 87 Sum: 1093 Ratio: 0.02%)
|
|
|
|
Rules : 55133 (Original: 53913)
|
|
Atoms : 43853
|
|
Bodies : 10280 (Original: 9059)
|
|
Count : 232 (Original: 476)
|
|
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
|
|
Tight : Yes
|
|
Variables : 373951 (Eliminated: 1464 Frozen: 372487)
|
|
Constraints : 2787694 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
|
|
|
|
Memory Peak : 570MB
|
|
Max. Length : 85 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 17.85s
|
|
Memory: 537MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 17.90s
|
|
|
|
Iteration 26
|
|
Queue: [(8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
|
|
Grounded Until: 85
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 27
|
|
Time : 434.403s (Solving: 418.46s 1st Model: 0.00s Unsat: 4.20s)
|
|
CPU Time : 434.492s
|
|
|
|
Choices : 5485373 (Domain: 5370691)
|
|
Conflicts : 633582 (Analyzed: 633579)
|
|
Restarts : 2261 (Average: 280.22 Last: 204)
|
|
Model-Level : 147.0
|
|
Problems : 27 (Average Length: 49.59 Splits: 0)
|
|
Lemmas : 633579 (Deleted: 594155)
|
|
Binary : 14225 (Ratio: 2.25%)
|
|
Ternary : 2658 (Ratio: 0.42%)
|
|
Conflict : 633579 (Average Length: 875.0 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 633579 (Average: 7.93 Max: 431 Sum: 5022002)
|
|
Executed : 633529 (Average: 7.92 Max: 431 Sum: 5020909 Ratio: 99.98%)
|
|
Bounded : 50 (Average: 21.86 Max: 87 Sum: 1093 Ratio: 0.02%)
|
|
|
|
Rules : 55133 (Original: 53913)
|
|
Atoms : 43853
|
|
Bodies : 10280 (Original: 9059)
|
|
Count : 232 (Original: 476)
|
|
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
|
|
Tight : Yes
|
|
Variables : 373951 (Eliminated: 1464 Frozen: 372487)
|
|
Constraints : 2787694 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
|
|
|
|
Memory Peak : 570MB
|
|
Max. Length : 85 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 21.12s
|
|
Memory: 537MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 21.17s
|
|
|
|
Iteration 27
|
|
Queue: [(9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
|
|
Grounded Until: 85
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 28
|
|
Time : 451.839s (Solving: 435.81s 1st Model: 0.00s Unsat: 4.20s)
|
|
CPU Time : 451.932s
|
|
|
|
Choices : 5700364 (Domain: 5584170)
|
|
Conflicts : 661765 (Analyzed: 661762)
|
|
Restarts : 2361 (Average: 280.29 Last: 204)
|
|
Model-Level : 147.0
|
|
Problems : 28 (Average Length: 50.93 Splits: 0)
|
|
Lemmas : 661762 (Deleted: 621439)
|
|
Binary : 14657 (Ratio: 2.21%)
|
|
Ternary : 2708 (Ratio: 0.41%)
|
|
Conflict : 661762 (Average Length: 872.9 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 661762 (Average: 7.88 Max: 431 Sum: 5212706)
|
|
Executed : 661712 (Average: 7.88 Max: 431 Sum: 5211613 Ratio: 99.98%)
|
|
Bounded : 50 (Average: 21.86 Max: 87 Sum: 1093 Ratio: 0.02%)
|
|
|
|
Rules : 55133 (Original: 53913)
|
|
Atoms : 43853
|
|
Bodies : 10280 (Original: 9059)
|
|
Count : 232 (Original: 476)
|
|
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
|
|
Tight : Yes
|
|
Variables : 373951 (Eliminated: 1464 Frozen: 372487)
|
|
Constraints : 2787694 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
|
|
|
|
Memory Peak : 570MB
|
|
Max. Length : 85 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 17.41s
|
|
Memory: 537MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 17.45s
|
|
|
|
Iteration 28
|
|
Queue: [(10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
|
|
Grounded Until: 85
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 29
|
|
Time : 468.754s (Solving: 452.63s 1st Model: 0.00s Unsat: 4.20s)
|
|
CPU Time : 468.856s
|
|
|
|
Choices : 5892645 (Domain: 5776369)
|
|
Conflicts : 689962 (Analyzed: 689959)
|
|
Restarts : 2461 (Average: 280.36 Last: 204)
|
|
Model-Level : 147.0
|
|
Problems : 29 (Average Length: 52.17 Splits: 0)
|
|
Lemmas : 689959 (Deleted: 647517)
|
|
Binary : 14908 (Ratio: 2.16%)
|
|
Ternary : 2759 (Ratio: 0.40%)
|
|
Conflict : 689959 (Average Length: 871.6 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 689959 (Average: 7.80 Max: 431 Sum: 5382814)
|
|
Executed : 689909 (Average: 7.80 Max: 431 Sum: 5381721 Ratio: 99.98%)
|
|
Bounded : 50 (Average: 21.86 Max: 87 Sum: 1093 Ratio: 0.02%)
|
|
|
|
Rules : 55133 (Original: 53913)
|
|
Atoms : 43853
|
|
Bodies : 10280 (Original: 9059)
|
|
Count : 232 (Original: 476)
|
|
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
|
|
Tight : Yes
|
|
Variables : 373951 (Eliminated: 1464 Frozen: 372487)
|
|
Constraints : 2787694 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
|
|
|
|
Memory Peak : 570MB
|
|
Max. Length : 85 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 16.89s
|
|
Memory: 537MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 16.93s
|
|
|
|
Iteration 29
|
|
Queue: [(11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
|
|
Grounded Until: 85
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 30
|
|
Time : 489.515s (Solving: 473.27s 1st Model: 0.00s Unsat: 4.20s)
|
|
CPU Time : 489.628s
|
|
|
|
Choices : 6121052 (Domain: 6004694)
|
|
Conflicts : 718096 (Analyzed: 718093)
|
|
Restarts : 2561 (Average: 280.40 Last: 204)
|
|
Model-Level : 147.0
|
|
Problems : 30 (Average Length: 53.33 Splits: 0)
|
|
Lemmas : 718093 (Deleted: 676101)
|
|
Binary : 15186 (Ratio: 2.11%)
|
|
Ternary : 2806 (Ratio: 0.39%)
|
|
Conflict : 718093 (Average Length: 878.1 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 718093 (Average: 7.78 Max: 431 Sum: 5583729)
|
|
Executed : 718043 (Average: 7.77 Max: 431 Sum: 5582636 Ratio: 99.98%)
|
|
Bounded : 50 (Average: 21.86 Max: 87 Sum: 1093 Ratio: 0.02%)
|
|
|
|
Rules : 55133 (Original: 53913)
|
|
Atoms : 43853
|
|
Bodies : 10280 (Original: 9059)
|
|
Count : 232 (Original: 476)
|
|
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
|
|
Tight : Yes
|
|
Variables : 373951 (Eliminated: 1464 Frozen: 372487)
|
|
Constraints : 2787694 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
|
|
|
|
Memory Peak : 570MB
|
|
Max. Length : 85 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 20.72s
|
|
Memory: 537MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 20.77s
|
|
|
|
Iteration 30
|
|
Queue: [(12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
|
|
Grounded Until: 85
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 31
|
|
Time : 508.521s (Solving: 492.15s 1st Model: 0.00s Unsat: 4.20s)
|
|
CPU Time : 508.640s
|
|
|
|
Choices : 6340515 (Domain: 6223979)
|
|
Conflicts : 746262 (Analyzed: 746259)
|
|
Restarts : 2661 (Average: 280.44 Last: 204)
|
|
Model-Level : 147.0
|
|
Problems : 31 (Average Length: 54.42 Splits: 0)
|
|
Lemmas : 746259 (Deleted: 703489)
|
|
Binary : 15397 (Ratio: 2.06%)
|
|
Ternary : 2842 (Ratio: 0.38%)
|
|
Conflict : 746259 (Average Length: 881.2 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 746259 (Average: 7.74 Max: 431 Sum: 5774391)
|
|
Executed : 746208 (Average: 7.74 Max: 431 Sum: 5773211 Ratio: 99.98%)
|
|
Bounded : 51 (Average: 23.14 Max: 87 Sum: 1180 Ratio: 0.02%)
|
|
|
|
Rules : 55133 (Original: 53913)
|
|
Atoms : 43853
|
|
Bodies : 10280 (Original: 9059)
|
|
Count : 232 (Original: 476)
|
|
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
|
|
Tight : Yes
|
|
Variables : 373951 (Eliminated: 1464 Frozen: 372487)
|
|
Constraints : 2787694 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
|
|
|
|
Memory Peak : 570MB
|
|
Max. Length : 85 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 18.96s
|
|
Memory: 537MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 19.02s
|
|
|
|
Iteration 31
|
|
Queue: [(13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
|
|
Grounded Until: 85
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 32
|
|
Time : 527.510s (Solving: 511.05s 1st Model: 0.00s Unsat: 4.20s)
|
|
CPU Time : 527.636s
|
|
|
|
Choices : 6600559 (Domain: 6482924)
|
|
Conflicts : 774478 (Analyzed: 774475)
|
|
Restarts : 2761 (Average: 280.51 Last: 204)
|
|
Model-Level : 147.0
|
|
Problems : 32 (Average Length: 55.44 Splits: 0)
|
|
Lemmas : 774475 (Deleted: 730698)
|
|
Binary : 15878 (Ratio: 2.05%)
|
|
Ternary : 2908 (Ratio: 0.38%)
|
|
Conflict : 774475 (Average Length: 883.2 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 774475 (Average: 7.75 Max: 431 Sum: 6000830)
|
|
Executed : 774424 (Average: 7.75 Max: 431 Sum: 5999650 Ratio: 99.98%)
|
|
Bounded : 51 (Average: 23.14 Max: 87 Sum: 1180 Ratio: 0.02%)
|
|
|
|
Rules : 55133 (Original: 53913)
|
|
Atoms : 43853
|
|
Bodies : 10280 (Original: 9059)
|
|
Count : 232 (Original: 476)
|
|
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
|
|
Tight : Yes
|
|
Variables : 373951 (Eliminated: 1464 Frozen: 372487)
|
|
Constraints : 2787687 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
|
|
|
|
Memory Peak : 570MB
|
|
Max. Length : 85 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 18.96s
|
|
Memory: 537MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 19.00s
|
|
|
|
Iteration 32
|
|
Queue: [(14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
|
|
Grounded Until: 85
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 33
|
|
Time : 547.765s (Solving: 531.21s 1st Model: 0.00s Unsat: 4.20s)
|
|
CPU Time : 547.900s
|
|
|
|
Choices : 6914199 (Domain: 6794643)
|
|
Conflicts : 802630 (Analyzed: 802627)
|
|
Restarts : 2861 (Average: 280.54 Last: 204)
|
|
Model-Level : 147.0
|
|
Problems : 33 (Average Length: 56.39 Splits: 0)
|
|
Lemmas : 802627 (Deleted: 757893)
|
|
Binary : 16327 (Ratio: 2.03%)
|
|
Ternary : 2968 (Ratio: 0.37%)
|
|
Conflict : 802627 (Average Length: 885.7 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 802627 (Average: 7.82 Max: 431 Sum: 6279139)
|
|
Executed : 802576 (Average: 7.82 Max: 431 Sum: 6277959 Ratio: 99.98%)
|
|
Bounded : 51 (Average: 23.14 Max: 87 Sum: 1180 Ratio: 0.02%)
|
|
|
|
Rules : 55133 (Original: 53913)
|
|
Atoms : 43853
|
|
Bodies : 10280 (Original: 9059)
|
|
Count : 232 (Original: 476)
|
|
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
|
|
Tight : Yes
|
|
Variables : 373951 (Eliminated: 1464 Frozen: 372487)
|
|
Constraints : 2787687 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
|
|
|
|
Memory Peak : 570MB
|
|
Max. Length : 85 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 20.22s
|
|
Memory: 537MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 20.27s
|
|
|
|
Iteration 33
|
|
Queue: [(15,75,1,True), (16,80,1,True), (17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
|
|
Grounded Until: 85
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 34
|
|
Time : 568.390s (Solving: 551.74s 1st Model: 0.00s Unsat: 4.20s)
|
|
CPU Time : 568.536s
|
|
|
|
Choices : 7151395 (Domain: 7031757)
|
|
Conflicts : 830822 (Analyzed: 830819)
|
|
Restarts : 2961 (Average: 280.59 Last: 204)
|
|
Model-Level : 147.0
|
|
Problems : 34 (Average Length: 57.29 Splits: 0)
|
|
Lemmas : 830819 (Deleted: 785308)
|
|
Binary : 16566 (Ratio: 1.99%)
|
|
Ternary : 3004 (Ratio: 0.36%)
|
|
Conflict : 830819 (Average Length: 889.3 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 830819 (Average: 7.81 Max: 431 Sum: 6485634)
|
|
Executed : 830768 (Average: 7.80 Max: 431 Sum: 6484454 Ratio: 99.98%)
|
|
Bounded : 51 (Average: 23.14 Max: 87 Sum: 1180 Ratio: 0.02%)
|
|
|
|
Rules : 55133 (Original: 53913)
|
|
Atoms : 43853
|
|
Bodies : 10280 (Original: 9059)
|
|
Count : 232 (Original: 476)
|
|
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
|
|
Tight : Yes
|
|
Variables : 373951 (Eliminated: 1464 Frozen: 372487)
|
|
Constraints : 2787687 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
|
|
|
|
Memory Peak : 570MB
|
|
Max. Length : 85 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 20.60s
|
|
Memory: 537MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 20.64s
|
|
|
|
Iteration 34
|
|
Queue: [(16,80,1,True), (17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
|
|
Grounded Until: 85
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 35
|
|
Time : 589.267s (Solving: 572.51s 1st Model: 0.00s Unsat: 4.20s)
|
|
CPU Time : 589.420s
|
|
|
|
Choices : 7441227 (Domain: 7316328)
|
|
Conflicts : 858998 (Analyzed: 858995)
|
|
Restarts : 3061 (Average: 280.63 Last: 204)
|
|
Model-Level : 147.0
|
|
Problems : 35 (Average Length: 58.14 Splits: 0)
|
|
Lemmas : 858995 (Deleted: 812298)
|
|
Binary : 17110 (Ratio: 1.99%)
|
|
Ternary : 3091 (Ratio: 0.36%)
|
|
Conflict : 858995 (Average Length: 892.4 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 858995 (Average: 7.85 Max: 431 Sum: 6741586)
|
|
Executed : 858944 (Average: 7.85 Max: 431 Sum: 6740406 Ratio: 99.98%)
|
|
Bounded : 51 (Average: 23.14 Max: 87 Sum: 1180 Ratio: 0.02%)
|
|
|
|
Rules : 55133 (Original: 53913)
|
|
Atoms : 43853
|
|
Bodies : 10280 (Original: 9059)
|
|
Count : 232 (Original: 476)
|
|
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
|
|
Tight : Yes
|
|
Variables : 373951 (Eliminated: 1464 Frozen: 372487)
|
|
Constraints : 2787687 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
|
|
|
|
Memory Peak : 570MB
|
|
Max. Length : 85 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 20.85s
|
|
Memory: 537MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 20.89s
|
|
|
|
Iteration 35
|
|
Queue: [(17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
|
|
Grounded Until: 85
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 36
|
|
Time : 611.139s (Solving: 594.28s 1st Model: 0.00s Unsat: 4.20s)
|
|
CPU Time : 611.300s
|
|
|
|
Choices : 7717670 (Domain: 7592616)
|
|
Conflicts : 887211 (Analyzed: 887208)
|
|
Restarts : 3161 (Average: 280.67 Last: 204)
|
|
Model-Level : 147.0
|
|
Problems : 36 (Average Length: 58.94 Splits: 0)
|
|
Lemmas : 887208 (Deleted: 839899)
|
|
Binary : 17380 (Ratio: 1.96%)
|
|
Ternary : 3137 (Ratio: 0.35%)
|
|
Conflict : 887208 (Average Length: 893.9 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 887208 (Average: 7.87 Max: 493 Sum: 6983010)
|
|
Executed : 887157 (Average: 7.87 Max: 493 Sum: 6981830 Ratio: 99.98%)
|
|
Bounded : 51 (Average: 23.14 Max: 87 Sum: 1180 Ratio: 0.02%)
|
|
|
|
Rules : 55133 (Original: 53913)
|
|
Atoms : 43853
|
|
Bodies : 10280 (Original: 9059)
|
|
Count : 232 (Original: 476)
|
|
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
|
|
Tight : Yes
|
|
Variables : 373951 (Eliminated: 1464 Frozen: 372487)
|
|
Constraints : 2787687 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
|
|
|
|
Memory Peak : 570MB
|
|
Max. Length : 85 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 21.84s
|
|
Memory: 537MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 21.88s
|
|
|
|
Iteration 36
|
|
Queue: [(18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
|
|
Grounded Until: 85
|
|
Expected Memory: 621.0MB
|
|
Grounding... [('step', [86]), ('step', [87]), ('step', [88]), ('step', [89]), ('step', [90]), ('check', [90])]
|
|
Grounding Time: 0.32s
|
|
Memory: 537MB (+0MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 37
|
|
Time : 632.985s (Solving: 615.15s 1st Model: 0.00s Unsat: 4.20s)
|
|
CPU Time : 633.156s
|
|
|
|
Choices : 7997616 (Domain: 7872364)
|
|
Conflicts : 915441 (Analyzed: 915438)
|
|
Restarts : 3261 (Average: 280.72 Last: 204)
|
|
Model-Level : 147.0
|
|
Problems : 37 (Average Length: 59.84 Splits: 0)
|
|
Lemmas : 915438 (Deleted: 867282)
|
|
Binary : 17707 (Ratio: 1.93%)
|
|
Ternary : 3182 (Ratio: 0.35%)
|
|
Conflict : 915438 (Average Length: 893.9 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 915438 (Average: 7.89 Max: 493 Sum: 7226121)
|
|
Executed : 915387 (Average: 7.89 Max: 493 Sum: 7224941 Ratio: 99.98%)
|
|
Bounded : 51 (Average: 23.14 Max: 87 Sum: 1180 Ratio: 0.02%)
|
|
|
|
Rules : 55133 (Original: 53913)
|
|
Atoms : 43853
|
|
Bodies : 10280 (Original: 9059)
|
|
Count : 232 (Original: 476)
|
|
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
|
|
Tight : Yes
|
|
Variables : 396527 (Eliminated: 1464 Frozen: 387533)
|
|
Constraints : 2960732 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
|
|
|
|
Memory Peak : 587MB
|
|
Max. Length : 85 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 21.26s
|
|
Memory: 549MB (+12MB)
|
|
UNKNOWN
|
|
Iteration Time: 21.86s
|
|
|
|
Iteration 37
|
|
Queue: [(19,95,0,True), (20,100,0,True), (21,105,0,True)]
|
|
Grounded Until: 90
|
|
Expected Memory: 633.0MB
|
|
Grounding... [('step', [91]), ('step', [92]), ('step', [93]), ('step', [94]), ('step', [95]), ('check', [95])]
|
|
Grounding Time: 0.32s
|
|
Memory: 549MB (+0MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 38
|
|
Time : 654.789s (Solving: 635.95s 1st Model: 0.00s Unsat: 4.20s)
|
|
CPU Time : 654.972s
|
|
|
|
Choices : 8272236 (Domain: 8146669)
|
|
Conflicts : 943641 (Analyzed: 943638)
|
|
Restarts : 3361 (Average: 280.76 Last: 204)
|
|
Model-Level : 147.0
|
|
Problems : 38 (Average Length: 60.82 Splits: 0)
|
|
Lemmas : 943638 (Deleted: 894728)
|
|
Binary : 17930 (Ratio: 1.90%)
|
|
Ternary : 3210 (Ratio: 0.34%)
|
|
Conflict : 943638 (Average Length: 889.7 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 943638 (Average: 7.92 Max: 493 Sum: 7469400)
|
|
Executed : 943587 (Average: 7.91 Max: 493 Sum: 7468220 Ratio: 99.98%)
|
|
Bounded : 51 (Average: 23.14 Max: 87 Sum: 1180 Ratio: 0.02%)
|
|
|
|
Rules : 55133 (Original: 53913)
|
|
Atoms : 43853
|
|
Bodies : 10280 (Original: 9059)
|
|
Count : 232 (Original: 476)
|
|
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
|
|
Tight : Yes
|
|
Variables : 419103 (Eliminated: 1464 Frozen: 410109)
|
|
Constraints : 3133777 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
|
|
|
|
Memory Peak : 607MB
|
|
Max. Length : 90 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 21.20s
|
|
Memory: 596MB (+47MB)
|
|
UNKNOWN
|
|
Iteration Time: 21.82s
|
|
|
|
Iteration 38
|
|
Queue: [(20,100,0,True), (21,105,0,True)]
|
|
Grounded Until: 95
|
|
Expected Memory: 680.0MB
|
|
Grounding... [('step', [96]), ('step', [97]), ('step', [98]), ('step', [99]), ('step', [100]), ('check', [100])]
|
|
Grounding Time: 0.33s
|
|
Memory: 596MB (+0MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 39
|
|
Time : 678.370s (Solving: 658.52s 1st Model: 0.00s Unsat: 4.20s)
|
|
CPU Time : 678.564s
|
|
|
|
Choices : 8579392 (Domain: 8453731)
|
|
Conflicts : 971840 (Analyzed: 971837)
|
|
Restarts : 3461 (Average: 280.80 Last: 204)
|
|
Model-Level : 147.0
|
|
Problems : 39 (Average Length: 61.87 Splits: 0)
|
|
Lemmas : 971837 (Deleted: 922125)
|
|
Binary : 18257 (Ratio: 1.88%)
|
|
Ternary : 3262 (Ratio: 0.34%)
|
|
Conflict : 971837 (Average Length: 888.9 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 971837 (Average: 7.96 Max: 493 Sum: 7736535)
|
|
Executed : 971786 (Average: 7.96 Max: 493 Sum: 7735355 Ratio: 99.98%)
|
|
Bounded : 51 (Average: 23.14 Max: 87 Sum: 1180 Ratio: 0.02%)
|
|
|
|
Rules : 55133 (Original: 53913)
|
|
Atoms : 43853
|
|
Bodies : 10280 (Original: 9059)
|
|
Count : 232 (Original: 476)
|
|
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
|
|
Tight : Yes
|
|
Variables : 441679 (Eliminated: 1464 Frozen: 432685)
|
|
Constraints : 3306822 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
|
|
|
|
Memory Peak : 650MB
|
|
Max. Length : 95 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 22.97s
|
|
Memory: 612MB (+16MB)
|
|
UNKNOWN
|
|
Iteration Time: 23.60s
|
|
|
|
Iteration 39
|
|
Queue: [(21,105,0,True)]
|
|
Grounded Until: 100
|
|
Expected Memory: 696.0MB
|
|
Grounding... [('step', [101]), ('step', [102]), ('step', [103]), ('step', [104]), ('step', [105]), ('check', [105])]
|
|
Grounding Time: 0.32s
|
|
Memory: 612MB (+0MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 40
|
|
Time : 700.801s (Solving: 679.93s 1st Model: 0.00s Unsat: 4.20s)
|
|
CPU Time : 701.004s
|
|
|
|
Choices : 8853119 (Domain: 8727423)
|
|
Conflicts : 1000007 (Analyzed: 1000004)
|
|
Restarts : 3561 (Average: 280.82 Last: 204)
|
|
Model-Level : 147.0
|
|
Problems : 40 (Average Length: 63.00 Splits: 0)
|
|
Lemmas : 1000004 (Deleted: 946111)
|
|
Binary : 18417 (Ratio: 1.84%)
|
|
Ternary : 3291 (Ratio: 0.33%)
|
|
Conflict : 1000004 (Average Length: 887.8 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 1000004 (Average: 7.97 Max: 493 Sum: 7973347)
|
|
Executed : 999953 (Average: 7.97 Max: 493 Sum: 7972167 Ratio: 99.99%)
|
|
Bounded : 51 (Average: 23.14 Max: 87 Sum: 1180 Ratio: 0.01%)
|
|
|
|
Rules : 55133 (Original: 53913)
|
|
Atoms : 43853
|
|
Bodies : 10280 (Original: 9059)
|
|
Count : 232 (Original: 476)
|
|
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
|
|
Tight : Yes
|
|
Variables : 464255 (Eliminated: 1464 Frozen: 455261)
|
|
Constraints : 3479867 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
|
|
|
|
Memory Peak : 669MB
|
|
Max. Length : 100 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 21.82s
|
|
Memory: 616MB (+4MB)
|
|
UNKNOWN
|
|
Iteration Time: 22.45s
|
|
|
|
Iteration 40
|
|
Queue: [(4,20,3,True), (5,25,3,True), (6,30,3,True), (7,35,2,True), (8,40,2,True), (9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,2,False), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)]
|
|
Grounded Until: 105
|
|
Blocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 41
|
|
Time : 713.054s (Solving: 692.05s 1st Model: 0.00s Unsat: 4.20s)
|
|
CPU Time : 713.264s
|
|
|
|
Choices : 9003898 (Domain: 8878202)
|
|
Conflicts : 1028184 (Analyzed: 1028181)
|
|
Restarts : 3661 (Average: 280.85 Last: 204)
|
|
Model-Level : 147.0
|
|
Problems : 41 (Average Length: 64.07 Splits: 0)
|
|
Lemmas : 1028181 (Deleted: 977173)
|
|
Binary : 18547 (Ratio: 1.80%)
|
|
Ternary : 3325 (Ratio: 0.32%)
|
|
Conflict : 1028181 (Average Length: 876.5 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 1028181 (Average: 7.89 Max: 493 Sum: 8117468)
|
|
Executed : 1028130 (Average: 7.89 Max: 493 Sum: 8116288 Ratio: 99.99%)
|
|
Bounded : 51 (Average: 23.14 Max: 87 Sum: 1180 Ratio: 0.01%)
|
|
|
|
Rules : 55133 (Original: 53913)
|
|
Atoms : 43853
|
|
Bodies : 10280 (Original: 9059)
|
|
Count : 232 (Original: 476)
|
|
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
|
|
Tight : Yes
|
|
Variables : 464255 (Eliminated: 1464 Frozen: 462791)
|
|
Constraints : 3479867 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
|
|
|
|
Memory Peak : 669MB
|
|
Max. Length : 105 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 12.20s
|
|
Memory: 616MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 12.26s
|
|
|
|
Iteration 41
|
|
Queue: [(5,25,3,True), (6,30,3,True), (7,35,2,True), (8,40,2,True), (9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,2,False), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)]
|
|
Grounded Until: 105
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 42
|
|
Time : 738.564s (Solving: 717.46s 1st Model: 0.00s Unsat: 4.20s)
|
|
CPU Time : 738.784s
|
|
|
|
Choices : 9105606 (Domain: 8979910)
|
|
Conflicts : 1056370 (Analyzed: 1056367)
|
|
Restarts : 3761 (Average: 280.87 Last: 204)
|
|
Model-Level : 147.0
|
|
Problems : 42 (Average Length: 65.10 Splits: 0)
|
|
Lemmas : 1056367 (Deleted: 1004871)
|
|
Binary : 18597 (Ratio: 1.76%)
|
|
Ternary : 3363 (Ratio: 0.32%)
|
|
Conflict : 1056367 (Average Length: 876.7 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 1056367 (Average: 7.77 Max: 493 Sum: 8209915)
|
|
Executed : 1056316 (Average: 7.77 Max: 493 Sum: 8208735 Ratio: 99.99%)
|
|
Bounded : 51 (Average: 23.14 Max: 87 Sum: 1180 Ratio: 0.01%)
|
|
|
|
Rules : 55133 (Original: 53913)
|
|
Atoms : 43853
|
|
Bodies : 10280 (Original: 9059)
|
|
Count : 232 (Original: 476)
|
|
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
|
|
Tight : Yes
|
|
Variables : 464255 (Eliminated: 1464 Frozen: 462791)
|
|
Constraints : 3479867 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
|
|
|
|
Memory Peak : 669MB
|
|
Max. Length : 105 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 25.48s
|
|
Memory: 616MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 25.52s
|
|
|
|
Iteration 42
|
|
Queue: [(6,30,3,True), (7,35,2,True), (8,40,2,True), (9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,2,False), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)]
|
|
Grounded Until: 105
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 43
|
|
Time : 764.452s (Solving: 743.24s 1st Model: 0.00s Unsat: 4.20s)
|
|
CPU Time : 764.680s
|
|
|
|
Choices : 9282110 (Domain: 9156414)
|
|
Conflicts : 1084555 (Analyzed: 1084552)
|
|
Restarts : 3861 (Average: 280.90 Last: 204)
|
|
Model-Level : 147.0
|
|
Problems : 43 (Average Length: 66.07 Splits: 0)
|
|
Lemmas : 1084552 (Deleted: 1032580)
|
|
Binary : 18721 (Ratio: 1.73%)
|
|
Ternary : 3384 (Ratio: 0.31%)
|
|
Conflict : 1084552 (Average Length: 891.5 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 1084552 (Average: 7.72 Max: 493 Sum: 8370316)
|
|
Executed : 1084501 (Average: 7.72 Max: 493 Sum: 8369136 Ratio: 99.99%)
|
|
Bounded : 51 (Average: 23.14 Max: 87 Sum: 1180 Ratio: 0.01%)
|
|
|
|
Rules : 55133 (Original: 53913)
|
|
Atoms : 43853
|
|
Bodies : 10280 (Original: 9059)
|
|
Count : 232 (Original: 476)
|
|
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
|
|
Tight : Yes
|
|
Variables : 464255 (Eliminated: 1464 Frozen: 462791)
|
|
Constraints : 3479867 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
|
|
|
|
Memory Peak : 744MB
|
|
Max. Length : 105 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 25.86s
|
|
Memory: 680MB (+64MB)
|
|
UNKNOWN
|
|
Iteration Time: 25.90s
|
|
|
|
Iteration 43
|
|
Queue: [(7,35,2,True), (8,40,2,True), (9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,2,False), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)]
|
|
Grounded Until: 105
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 44
|
|
Time : 784.115s (Solving: 762.79s 1st Model: 0.00s Unsat: 4.20s)
|
|
CPU Time : 784.352s
|
|
|
|
Choices : 9451213 (Domain: 9325517)
|
|
Conflicts : 1112727 (Analyzed: 1112724)
|
|
Restarts : 3961 (Average: 280.92 Last: 204)
|
|
Model-Level : 147.0
|
|
Problems : 44 (Average Length: 67.00 Splits: 0)
|
|
Lemmas : 1112724 (Deleted: 1060159)
|
|
Binary : 18869 (Ratio: 1.70%)
|
|
Ternary : 3425 (Ratio: 0.31%)
|
|
Conflict : 1112724 (Average Length: 894.9 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 1112724 (Average: 7.66 Max: 493 Sum: 8519634)
|
|
Executed : 1112673 (Average: 7.66 Max: 493 Sum: 8518454 Ratio: 99.99%)
|
|
Bounded : 51 (Average: 23.14 Max: 87 Sum: 1180 Ratio: 0.01%)
|
|
|
|
Rules : 55133 (Original: 53913)
|
|
Atoms : 43853
|
|
Bodies : 10280 (Original: 9059)
|
|
Count : 232 (Original: 476)
|
|
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
|
|
Tight : Yes
|
|
Variables : 464255 (Eliminated: 1464 Frozen: 462791)
|
|
Constraints : 3479867 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
|
|
|
|
Memory Peak : 744MB
|
|
Max. Length : 105 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 19.63s
|
|
Memory: 680MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 19.67s
|
|
|
|
Iteration 44
|
|
Queue: [(8,40,2,True), (9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,2,False), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)]
|
|
Grounded Until: 105
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 45
|
|
Time : 803.797s (Solving: 782.37s 1st Model: 0.00s Unsat: 4.20s)
|
|
CPU Time : 804.040s
|
|
|
|
Choices : 9629811 (Domain: 9504115)
|
|
Conflicts : 1140953 (Analyzed: 1140950)
|
|
Restarts : 4061 (Average: 280.95 Last: 204)
|
|
Model-Level : 147.0
|
|
Problems : 45 (Average Length: 67.89 Splits: 0)
|
|
Lemmas : 1140950 (Deleted: 1087827)
|
|
Binary : 19015 (Ratio: 1.67%)
|
|
Ternary : 3450 (Ratio: 0.30%)
|
|
Conflict : 1140950 (Average Length: 897.3 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 1140950 (Average: 7.60 Max: 493 Sum: 8675794)
|
|
Executed : 1140899 (Average: 7.60 Max: 493 Sum: 8674614 Ratio: 99.99%)
|
|
Bounded : 51 (Average: 23.14 Max: 87 Sum: 1180 Ratio: 0.01%)
|
|
|
|
Rules : 55133 (Original: 53913)
|
|
Atoms : 43853
|
|
Bodies : 10280 (Original: 9059)
|
|
Count : 232 (Original: 476)
|
|
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
|
|
Tight : Yes
|
|
Variables : 464255 (Eliminated: 1464 Frozen: 462791)
|
|
Constraints : 3479867 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
|
|
|
|
Memory Peak : 744MB
|
|
Max. Length : 105 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 19.65s
|
|
Memory: 680MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 19.69s
|
|
|
|
Iteration 45
|
|
Queue: [(9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,2,False), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)]
|
|
Grounded Until: 105
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 46
|
|
Time : 825.313s (Solving: 803.76s 1st Model: 0.00s Unsat: 4.20s)
|
|
CPU Time : 825.564s
|
|
|
|
Choices : 9823417 (Domain: 9697580)
|
|
Conflicts : 1169150 (Analyzed: 1169147)
|
|
Restarts : 4161 (Average: 280.98 Last: 204)
|
|
Model-Level : 147.0
|
|
Problems : 46 (Average Length: 68.74 Splits: 0)
|
|
Lemmas : 1169147 (Deleted: 1115335)
|
|
Binary : 19295 (Ratio: 1.65%)
|
|
Ternary : 3485 (Ratio: 0.30%)
|
|
Conflict : 1169147 (Average Length: 904.0 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 1169147 (Average: 7.56 Max: 493 Sum: 8842595)
|
|
Executed : 1169096 (Average: 7.56 Max: 493 Sum: 8841415 Ratio: 99.99%)
|
|
Bounded : 51 (Average: 23.14 Max: 87 Sum: 1180 Ratio: 0.01%)
|
|
|
|
Rules : 55133 (Original: 53913)
|
|
Atoms : 43853
|
|
Bodies : 10280 (Original: 9059)
|
|
Count : 232 (Original: 476)
|
|
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
|
|
Tight : Yes
|
|
Variables : 464255 (Eliminated: 1464 Frozen: 462791)
|
|
Constraints : 3479867 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
|
|
|
|
Memory Peak : 744MB
|
|
Max. Length : 105 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 21.47s
|
|
Memory: 680MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 21.53s
|
|
|
|
Iteration 46
|
|
Queue: [(10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,2,False), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)]
|
|
Grounded Until: 105
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 47
|
|
Time : 844.567s (Solving: 822.91s 1st Model: 0.00s Unsat: 4.20s)
|
|
CPU Time : 844.828s
|
|
|
|
Choices : 10033085 (Domain: 9907237)
|
|
Conflicts : 1197341 (Analyzed: 1197338)
|
|
Restarts : 4261 (Average: 281.00 Last: 204)
|
|
Model-Level : 147.0
|
|
Problems : 47 (Average Length: 69.55 Splits: 0)
|
|
Lemmas : 1197338 (Deleted: 1142902)
|
|
Binary : 19440 (Ratio: 1.62%)
|
|
Ternary : 3518 (Ratio: 0.29%)
|
|
Conflict : 1197338 (Average Length: 903.7 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 1197338 (Average: 7.54 Max: 493 Sum: 9026213)
|
|
Executed : 1197287 (Average: 7.54 Max: 493 Sum: 9025033 Ratio: 99.99%)
|
|
Bounded : 51 (Average: 23.14 Max: 87 Sum: 1180 Ratio: 0.01%)
|
|
|
|
Rules : 55133 (Original: 53913)
|
|
Atoms : 43853
|
|
Bodies : 10280 (Original: 9059)
|
|
Count : 232 (Original: 476)
|
|
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
|
|
Tight : Yes
|
|
Variables : 464255 (Eliminated: 1464 Frozen: 462791)
|
|
Constraints : 3479867 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
|
|
|
|
Memory Peak : 744MB
|
|
Max. Length : 105 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 19.22s
|
|
Memory: 680MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 19.26s
|
|
|
|
Iteration 47
|
|
Queue: [(11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,2,False), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)]
|
|
Grounded Until: 105
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 48
|
|
Time : 863.330s (Solving: 841.57s 1st Model: 0.00s Unsat: 4.20s)
|
|
CPU Time : 863.600s
|
|
|
|
Choices : 10251284 (Domain: 10125432)
|
|
Conflicts : 1225502 (Analyzed: 1225499)
|
|
Restarts : 4361 (Average: 281.01 Last: 204)
|
|
Model-Level : 147.0
|
|
Problems : 48 (Average Length: 70.33 Splits: 0)
|
|
Lemmas : 1225499 (Deleted: 1170396)
|
|
Binary : 19701 (Ratio: 1.61%)
|
|
Ternary : 3549 (Ratio: 0.29%)
|
|
Conflict : 1225499 (Average Length: 904.6 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 1225499 (Average: 7.52 Max: 493 Sum: 9214105)
|
|
Executed : 1225448 (Average: 7.52 Max: 493 Sum: 9212925 Ratio: 99.99%)
|
|
Bounded : 51 (Average: 23.14 Max: 87 Sum: 1180 Ratio: 0.01%)
|
|
|
|
Rules : 55133 (Original: 53913)
|
|
Atoms : 43853
|
|
Bodies : 10280 (Original: 9059)
|
|
Count : 232 (Original: 476)
|
|
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
|
|
Tight : Yes
|
|
Variables : 464255 (Eliminated: 1464 Frozen: 462791)
|
|
Constraints : 3479867 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
|
|
|
|
Memory Peak : 744MB
|
|
Max. Length : 105 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 18.73s
|
|
Memory: 680MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 18.77s
|
|
|
|
Iteration 48
|
|
Queue: [(12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,2,False), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)]
|
|
Grounded Until: 105
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 49
|
|
Time : 881.523s (Solving: 859.66s 1st Model: 0.00s Unsat: 4.20s)
|
|
CPU Time : 881.800s
|
|
|
|
Choices : 10489316 (Domain: 10363047)
|
|
Conflicts : 1253686 (Analyzed: 1253683)
|
|
Restarts : 4461 (Average: 281.03 Last: 204)
|
|
Model-Level : 147.0
|
|
Problems : 49 (Average Length: 71.08 Splits: 0)
|
|
Lemmas : 1253683 (Deleted: 1197683)
|
|
Binary : 19958 (Ratio: 1.59%)
|
|
Ternary : 3584 (Ratio: 0.29%)
|
|
Conflict : 1253683 (Average Length: 903.4 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 1253683 (Average: 7.51 Max: 493 Sum: 9421101)
|
|
Executed : 1253631 (Average: 7.51 Max: 493 Sum: 9419814 Ratio: 99.99%)
|
|
Bounded : 52 (Average: 24.75 Max: 107 Sum: 1287 Ratio: 0.01%)
|
|
|
|
Rules : 55133 (Original: 53913)
|
|
Atoms : 43853
|
|
Bodies : 10280 (Original: 9059)
|
|
Count : 232 (Original: 476)
|
|
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
|
|
Tight : Yes
|
|
Variables : 464255 (Eliminated: 1464 Frozen: 462791)
|
|
Constraints : 3479867 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
|
|
|
|
Memory Peak : 744MB
|
|
Max. Length : 105 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 18.16s
|
|
Memory: 680MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 18.20s
|
|
|
|
Iteration 49
|
|
Queue: [(13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,2,False), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)]
|
|
Grounded Until: 105
|
|
Unblocking actions...
|
|
Solving...
|
|
*** Info : (planner): INTERRUPTED by signal!
|
|
UNKNOWN
|
|
|
|
INTERRUPTED : 1
|
|
|
|
Models : 0+
|
|
Calls : 50
|
|
Time : 900.347s (Solving: 878.37s 1st Model: 0.00s Unsat: 4.20s)
|
|
CPU Time : 900.616s
|
|
|
|
Choices : 10729648 (Domain: 10602630)
|
|
Conflicts : 1281834 (Analyzed: 1281831)
|
|
Restarts : 4561 (Average: 281.04 Last: 204)
|
|
Model-Level : 147.0
|
|
Problems : 50 (Average Length: 71.80 Splits: 0)
|
|
Lemmas : 1281831 (Deleted: 1225188)
|
|
Binary : 20176 (Ratio: 1.57%)
|
|
Ternary : 3624 (Ratio: 0.28%)
|
|
Conflict : 1281831 (Average Length: 903.4 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 1281831 (Average: 7.51 Max: 493 Sum: 9629023)
|
|
Executed : 1281779 (Average: 7.51 Max: 493 Sum: 9627736 Ratio: 99.99%)
|
|
Bounded : 52 (Average: 24.75 Max: 107 Sum: 1287 Ratio: 0.01%)
|
|
|
|
Rules : 55133 (Original: 53913)
|
|
Atoms : 43853
|
|
Bodies : 10280 (Original: 9059)
|
|
Count : 232 (Original: 476)
|
|
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
|
|
Tight : Yes
|
|
Variables : 464255 (Eliminated: 1464 Frozen: 462791)
|
|
Constraints : 3479853 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
|
|
|
|
Memory Peak : 744MB
|
|
Max. Length : 105 steps
|
|
Models : 1
|
|
|
|
|