4802 lines
176 KiB
Plaintext
4802 lines
176 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-20.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-20.pddl
|
|
Parsing...
|
|
Parsing: [0.040s CPU, 0.043s wall-clock]
|
|
Normalizing task... [0.000s CPU, 0.003s wall-clock]
|
|
Instantiating...
|
|
Generating Datalog program... [0.010s CPU, 0.012s wall-clock]
|
|
Normalizing Datalog program...
|
|
Normalizing Datalog program: [0.050s CPU, 0.053s wall-clock]
|
|
Preparing model... [0.030s CPU, 0.030s wall-clock]
|
|
Generated 115 rules.
|
|
Computing model... [0.540s CPU, 0.544s wall-clock]
|
|
3296 relevant atoms
|
|
3425 auxiliary atoms
|
|
6721 final queue length
|
|
11595 total queue pushes
|
|
Completing instantiation... [1.030s CPU, 1.030s wall-clock]
|
|
Instantiating: [1.680s CPU, 1.676s 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.014s wall-clock]
|
|
Computing fact groups: [0.190s CPU, 0.197s 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.056s wall-clock]
|
|
Translating task: [1.060s CPU, 1.070s 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.591s 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.379s 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.370s CPU, 0.407s wall-clock]
|
|
Done! [4.380s CPU, 4.422s wall-clock]
|
|
planner.py version 0.0.1
|
|
|
|
Time: 0.92s
|
|
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.109s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
|
|
CPU Time : 0.924s
|
|
|
|
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.28s
|
|
Memory: 183MB (+0MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 1+
|
|
Calls : 2
|
|
Time : 1.543s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
|
|
CPU Time : 1.360s
|
|
|
|
Choices : 195 (Domain: 36)
|
|
Conflicts : 4 (Analyzed: 4)
|
|
Restarts : 0
|
|
Model-Level : 183.0
|
|
Problems : 2 (Average Length: 4.50 Splits: 0)
|
|
Lemmas : 4 (Deleted: 0)
|
|
Binary : 2 (Ratio: 50.00%)
|
|
Ternary : 0 (Ratio: 0.00%)
|
|
Conflict : 4 (Average Length: 16.2 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 4 (Average: 5.00 Max: 16 Sum: 20)
|
|
Executed : 3 (Average: 4.75 Max: 16 Sum: 19 Ratio: 95.00%)
|
|
Bounded : 1 (Average: 1.00 Max: 1 Sum: 1 Ratio: 5.00%)
|
|
|
|
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 : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 0.02s
|
|
Memory: 187MB (+4MB)
|
|
SAT
|
|
Testing...
|
|
NOT SERIALIZABLE
|
|
Testing Time: 1.00s
|
|
Memory: 218MB (+31MB)
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0
|
|
Calls : 3
|
|
Time : 1.696s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
|
|
CPU Time : 1.516s
|
|
|
|
Choices : 212 (Domain: 37)
|
|
Conflicts : 13 (Analyzed: 12)
|
|
Restarts : 0
|
|
Model-Level : 183.0
|
|
Problems : 3 (Average Length: 5.33 Splits: 0)
|
|
Lemmas : 12 (Deleted: 0)
|
|
Binary : 4 (Ratio: 33.33%)
|
|
Ternary : 4 (Ratio: 33.33%)
|
|
Conflict : 12 (Average Length: 7.5 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 12 (Average: 3.25 Max: 16 Sum: 39)
|
|
Executed : 9 (Average: 3.00 Max: 16 Sum: 36 Ratio: 92.31%)
|
|
Bounded : 3 (Average: 1.00 Max: 1 Sum: 3 Ratio: 7.69%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 21236 (Eliminated: 0 Frozen: 4444)
|
|
Constraints : 86170 (Binary: 92.4% Ternary: 5.4% Other: 2.2%)
|
|
|
|
Memory Peak : 247MB
|
|
Max. Length : 0 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 0.02s
|
|
Memory: 218MB (+0MB)
|
|
UNSAT
|
|
Iteration Time: 1.46s
|
|
|
|
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: 222.0MB
|
|
Grounding... [('step', [6]), ('step', [7]), ('step', [8]), ('step', [9]), ('step', [10]), ('check', [10])]
|
|
Grounding Time: 0.55s
|
|
Memory: 218MB (+0MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0
|
|
Calls : 4
|
|
Time : 3.582s (Solving: 1.11s 1st Model: 0.00s Unsat: 1.11s)
|
|
CPU Time : 3.408s
|
|
|
|
Choices : 36338 (Domain: 29490)
|
|
Conflicts : 3123 (Analyzed: 3121)
|
|
Restarts : 36 (Average: 86.69 Last: 26)
|
|
Model-Level : 183.0
|
|
Problems : 4 (Average Length: 7.00 Splits: 0)
|
|
Lemmas : 3121 (Deleted: 570)
|
|
Binary : 325 (Ratio: 10.41%)
|
|
Ternary : 504 (Ratio: 16.15%)
|
|
Conflict : 3121 (Average Length: 42.3 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 3121 (Average: 11.58 Max: 265 Sum: 36155)
|
|
Executed : 3080 (Average: 11.44 Max: 265 Sum: 35707 Ratio: 98.76%)
|
|
Bounded : 41 (Average: 10.93 Max: 12 Sum: 448 Ratio: 1.24%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 61312 (Eliminated: 0 Frozen: 16894)
|
|
Constraints : 388150 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
|
|
|
|
Memory Peak : 247MB
|
|
Max. Length : 5 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 1.14s
|
|
Memory: 230MB (+12MB)
|
|
UNSAT
|
|
Iteration Time: 1.89s
|
|
|
|
Iteration 4
|
|
Queue: [(3,15,0,True), (4,20,0,True), (5,25,0,True), (6,30,0,True)]
|
|
Grounded Until: 10
|
|
Expected Memory: 242.0MB
|
|
Grounding... [('step', [11]), ('step', [12]), ('step', [13]), ('step', [14]), ('step', [15]), ('check', [15])]
|
|
Grounding Time: 0.53s
|
|
Memory: 242MB (+12MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 5
|
|
Time : 8.918s (Solving: 5.65s 1st Model: 0.00s Unsat: 1.11s)
|
|
CPU Time : 8.748s
|
|
|
|
Choices : 115133 (Domain: 89050)
|
|
Conflicts : 12082 (Analyzed: 12080)
|
|
Restarts : 136 (Average: 88.82 Last: 101)
|
|
Model-Level : 183.0
|
|
Problems : 5 (Average Length: 9.00 Splits: 0)
|
|
Lemmas : 12080 (Deleted: 7160)
|
|
Binary : 775 (Ratio: 6.42%)
|
|
Ternary : 845 (Ratio: 7.00%)
|
|
Conflict : 12080 (Average Length: 130.4 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 12080 (Average: 9.19 Max: 265 Sum: 110997)
|
|
Executed : 12022 (Average: 9.13 Max: 265 Sum: 110262 Ratio: 99.34%)
|
|
Bounded : 58 (Average: 12.67 Max: 17 Sum: 735 Ratio: 0.66%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 101388 (Eliminated: 0 Frozen: 29344)
|
|
Constraints : 645808 (Binary: 91.4% Ternary: 6.7% Other: 1.9%)
|
|
|
|
Memory Peak : 262MB
|
|
Max. Length : 10 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 4.58s
|
|
Memory: 262MB (+20MB)
|
|
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: 294.0MB
|
|
Grounding... [('step', [16]), ('step', [17]), ('step', [18]), ('step', [19]), ('step', [20]), ('check', [20])]
|
|
Grounding Time: 0.64s
|
|
Memory: 276MB (+14MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 6
|
|
Time : 14.138s (Solving: 9.94s 1st Model: 0.00s Unsat: 1.11s)
|
|
CPU Time : 13.968s
|
|
|
|
Choices : 157868 (Domain: 131138)
|
|
Conflicts : 19485 (Analyzed: 19483)
|
|
Restarts : 236 (Average: 82.56 Last: 101)
|
|
Model-Level : 183.0
|
|
Problems : 6 (Average Length: 11.17 Splits: 0)
|
|
Lemmas : 19483 (Deleted: 13053)
|
|
Binary : 1076 (Ratio: 5.52%)
|
|
Ternary : 912 (Ratio: 4.68%)
|
|
Conflict : 19483 (Average Length: 181.6 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 19483 (Average: 7.64 Max: 265 Sum: 148779)
|
|
Executed : 19423 (Average: 7.60 Max: 265 Sum: 148003 Ratio: 99.48%)
|
|
Bounded : 60 (Average: 12.93 Max: 22 Sum: 776 Ratio: 0.52%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 141464 (Eliminated: 0 Frozen: 41794)
|
|
Constraints : 941310 (Binary: 91.3% Ternary: 6.8% Other: 1.9%)
|
|
|
|
Memory Peak : 302MB
|
|
Max. Length : 15 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 4.33s
|
|
Memory: 302MB (+26MB)
|
|
UNKNOWN
|
|
Iteration Time: 5.23s
|
|
|
|
Iteration 6
|
|
Queue: [(5,25,0,True), (6,30,0,True)]
|
|
Grounded Until: 20
|
|
Expected Memory: 342.0MB
|
|
Grounding... [('step', [21]), ('step', [22]), ('step', [23]), ('step', [24]), ('step', [25]), ('check', [25])]
|
|
Grounding Time: 0.54s
|
|
Memory: 308MB (+6MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 7
|
|
Time : 20.394s (Solving: 15.35s 1st Model: 0.00s Unsat: 1.11s)
|
|
CPU Time : 20.224s
|
|
|
|
Choices : 331212 (Domain: 285212)
|
|
Conflicts : 28062 (Analyzed: 28060)
|
|
Restarts : 336 (Average: 83.51 Last: 131)
|
|
Model-Level : 183.0
|
|
Problems : 7 (Average Length: 13.43 Splits: 0)
|
|
Lemmas : 28060 (Deleted: 18557)
|
|
Binary : 1903 (Ratio: 6.78%)
|
|
Ternary : 1288 (Ratio: 4.59%)
|
|
Conflict : 28060 (Average Length: 175.7 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 28060 (Average: 11.25 Max: 782 Sum: 315796)
|
|
Executed : 27986 (Average: 11.21 Max: 782 Sum: 314642 Ratio: 99.63%)
|
|
Bounded : 74 (Average: 15.59 Max: 27 Sum: 1154 Ratio: 0.37%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 181540 (Eliminated: 0 Frozen: 54244)
|
|
Constraints : 1240231 (Binary: 91.3% Ternary: 6.8% Other: 1.8%)
|
|
|
|
Memory Peak : 336MB
|
|
Max. Length : 20 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 5.47s
|
|
Memory: 322MB (+14MB)
|
|
UNKNOWN
|
|
Iteration Time: 6.27s
|
|
|
|
Iteration 7
|
|
Queue: [(6,30,0,True)]
|
|
Grounded Until: 25
|
|
Expected Memory: 362.0MB
|
|
Grounding... [('step', [26]), ('step', [27]), ('step', [28]), ('step', [29]), ('step', [30]), ('check', [30])]
|
|
Grounding Time: 0.58s
|
|
Memory: 334MB (+12MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 8
|
|
Time : 27.275s (Solving: 21.30s 1st Model: 0.00s Unsat: 1.11s)
|
|
CPU Time : 27.108s
|
|
|
|
Choices : 464738 (Domain: 402252)
|
|
Conflicts : 36744 (Analyzed: 36742)
|
|
Restarts : 436 (Average: 84.27 Last: 131)
|
|
Model-Level : 183.0
|
|
Problems : 8 (Average Length: 15.75 Splits: 0)
|
|
Lemmas : 36742 (Deleted: 27143)
|
|
Binary : 2231 (Ratio: 6.07%)
|
|
Ternary : 1421 (Ratio: 3.87%)
|
|
Conflict : 36742 (Average Length: 201.4 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 36742 (Average: 11.94 Max: 782 Sum: 438868)
|
|
Executed : 36653 (Average: 11.90 Max: 782 Sum: 437244 Ratio: 99.63%)
|
|
Bounded : 89 (Average: 18.25 Max: 32 Sum: 1624 Ratio: 0.37%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 221616 (Eliminated: 0 Frozen: 66694)
|
|
Constraints : 1520780 (Binary: 91.3% Ternary: 6.8% Other: 1.8%)
|
|
|
|
Memory Peak : 368MB
|
|
Max. Length : 25 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 6.02s
|
|
Memory: 368MB (+34MB)
|
|
UNKNOWN
|
|
Iteration Time: 6.89s
|
|
|
|
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 : 28.615s (Solving: 22.59s 1st Model: 0.00s Unsat: 2.40s)
|
|
CPU Time : 28.448s
|
|
|
|
Choices : 467550 (Domain: 405060)
|
|
Conflicts : 37906 (Analyzed: 37903)
|
|
Restarts : 450 (Average: 84.23 Last: 131)
|
|
Model-Level : 183.0
|
|
Problems : 9 (Average Length: 17.56 Splits: 0)
|
|
Lemmas : 37903 (Deleted: 27143)
|
|
Binary : 2261 (Ratio: 5.97%)
|
|
Ternary : 1439 (Ratio: 3.80%)
|
|
Conflict : 37903 (Average Length: 202.3 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 37903 (Average: 11.65 Max: 782 Sum: 441640)
|
|
Executed : 37813 (Average: 11.61 Max: 782 Sum: 440015 Ratio: 99.63%)
|
|
Bounded : 90 (Average: 18.06 Max: 32 Sum: 1625 Ratio: 0.37%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 221616 (Eliminated: 0 Frozen: 66694)
|
|
Constraints : 1503174 (Binary: 91.3% Ternary: 6.8% Other: 1.8%)
|
|
|
|
Memory Peak : 368MB
|
|
Max. Length : 30 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 1.32s
|
|
Memory: 368MB (+0MB)
|
|
UNSAT
|
|
Iteration Time: 1.34s
|
|
|
|
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 : 34.297s (Solving: 28.21s 1st Model: 0.00s Unsat: 2.40s)
|
|
CPU Time : 34.132s
|
|
|
|
Choices : 529904 (Domain: 452412)
|
|
Conflicts : 46631 (Analyzed: 46628)
|
|
Restarts : 550 (Average: 84.78 Last: 131)
|
|
Model-Level : 183.0
|
|
Problems : 10 (Average Length: 19.00 Splits: 0)
|
|
Lemmas : 46628 (Deleted: 36484)
|
|
Binary : 2472 (Ratio: 5.30%)
|
|
Ternary : 1508 (Ratio: 3.23%)
|
|
Conflict : 46628 (Average Length: 244.7 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 46628 (Average: 10.67 Max: 782 Sum: 497348)
|
|
Executed : 46537 (Average: 10.63 Max: 782 Sum: 495696 Ratio: 99.67%)
|
|
Bounded : 91 (Average: 18.15 Max: 32 Sum: 1652 Ratio: 0.33%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 221616 (Eliminated: 0 Frozen: 66694)
|
|
Constraints : 1503174 (Binary: 91.3% Ternary: 6.8% Other: 1.8%)
|
|
|
|
Memory Peak : 368MB
|
|
Max. Length : 30 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 5.66s
|
|
Memory: 368MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 5.69s
|
|
|
|
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 : 41.774s (Solving: 35.64s 1st Model: 0.00s Unsat: 2.40s)
|
|
CPU Time : 41.612s
|
|
|
|
Choices : 633897 (Domain: 541048)
|
|
Conflicts : 55908 (Analyzed: 55905)
|
|
Restarts : 650 (Average: 86.01 Last: 131)
|
|
Model-Level : 183.0
|
|
Problems : 11 (Average Length: 20.18 Splits: 0)
|
|
Lemmas : 55905 (Deleted: 42997)
|
|
Binary : 3035 (Ratio: 5.43%)
|
|
Ternary : 1728 (Ratio: 3.09%)
|
|
Conflict : 55905 (Average Length: 289.2 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 55905 (Average: 10.58 Max: 782 Sum: 591368)
|
|
Executed : 55806 (Average: 10.54 Max: 782 Sum: 589465 Ratio: 99.68%)
|
|
Bounded : 99 (Average: 19.22 Max: 32 Sum: 1903 Ratio: 0.32%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 221616 (Eliminated: 0 Frozen: 66694)
|
|
Constraints : 1503174 (Binary: 91.3% Ternary: 6.8% Other: 1.8%)
|
|
|
|
Memory Peak : 368MB
|
|
Max. Length : 30 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 7.46s
|
|
Memory: 368MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 7.48s
|
|
|
|
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 : 49.815s (Solving: 43.63s 1st Model: 0.00s Unsat: 2.40s)
|
|
CPU Time : 49.656s
|
|
|
|
Choices : 743498 (Domain: 635142)
|
|
Conflicts : 65194 (Analyzed: 65191)
|
|
Restarts : 750 (Average: 86.92 Last: 131)
|
|
Model-Level : 183.0
|
|
Problems : 12 (Average Length: 21.17 Splits: 0)
|
|
Lemmas : 65191 (Deleted: 51200)
|
|
Binary : 3305 (Ratio: 5.07%)
|
|
Ternary : 1857 (Ratio: 2.85%)
|
|
Conflict : 65191 (Average Length: 330.5 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 65191 (Average: 10.52 Max: 782 Sum: 685498)
|
|
Executed : 65090 (Average: 10.49 Max: 782 Sum: 683531 Ratio: 99.71%)
|
|
Bounded : 101 (Average: 19.48 Max: 32 Sum: 1967 Ratio: 0.29%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 221616 (Eliminated: 0 Frozen: 66694)
|
|
Constraints : 1497569 (Binary: 91.3% Ternary: 6.8% Other: 1.9%)
|
|
|
|
Memory Peak : 368MB
|
|
Max. Length : 30 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 8.03s
|
|
Memory: 368MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 8.05s
|
|
|
|
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: 414.0MB
|
|
Grounding... [('step', [31]), ('step', [32]), ('step', [33]), ('step', [34]), ('step', [35]), ('check', [35])]
|
|
Grounding Time: 0.56s
|
|
Memory: 368MB (+0MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 13
|
|
Time : 59.310s (Solving: 52.21s 1st Model: 0.00s Unsat: 2.40s)
|
|
CPU Time : 59.156s
|
|
|
|
Choices : 881351 (Domain: 756871)
|
|
Conflicts : 74031 (Analyzed: 74028)
|
|
Restarts : 850 (Average: 87.09 Last: 157)
|
|
Model-Level : 183.0
|
|
Problems : 13 (Average Length: 22.38 Splits: 0)
|
|
Lemmas : 74028 (Deleted: 59920)
|
|
Binary : 3488 (Ratio: 4.71%)
|
|
Ternary : 1914 (Ratio: 2.59%)
|
|
Conflict : 74028 (Average Length: 407.7 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 74028 (Average: 10.85 Max: 782 Sum: 803239)
|
|
Executed : 73919 (Average: 10.82 Max: 782 Sum: 800976 Ratio: 99.72%)
|
|
Bounded : 109 (Average: 20.76 Max: 37 Sum: 2263 Ratio: 0.28%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 261692 (Eliminated: 0 Frozen: 79144)
|
|
Constraints : 1799341 (Binary: 91.3% Ternary: 6.9% Other: 1.8%)
|
|
|
|
Memory Peak : 405MB
|
|
Max. Length : 30 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 8.65s
|
|
Memory: 381MB (+13MB)
|
|
UNKNOWN
|
|
Iteration Time: 9.51s
|
|
|
|
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: 427.0MB
|
|
Grounding... [('step', [36]), ('step', [37]), ('step', [38]), ('step', [39]), ('step', [40]), ('check', [40])]
|
|
Grounding Time: 0.57s
|
|
Memory: 392MB (+11MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 14
|
|
Time : 68.733s (Solving: 60.68s 1st Model: 0.00s Unsat: 2.40s)
|
|
CPU Time : 68.584s
|
|
|
|
Choices : 1039739 (Domain: 899452)
|
|
Conflicts : 82621 (Analyzed: 82618)
|
|
Restarts : 950 (Average: 86.97 Last: 157)
|
|
Model-Level : 183.0
|
|
Problems : 14 (Average Length: 23.79 Splits: 0)
|
|
Lemmas : 82618 (Deleted: 66758)
|
|
Binary : 3639 (Ratio: 4.40%)
|
|
Ternary : 1978 (Ratio: 2.39%)
|
|
Conflict : 82618 (Average Length: 425.5 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 82618 (Average: 11.38 Max: 782 Sum: 940232)
|
|
Executed : 82507 (Average: 11.35 Max: 782 Sum: 937886 Ratio: 99.75%)
|
|
Bounded : 111 (Average: 21.14 Max: 42 Sum: 2346 Ratio: 0.25%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 301768 (Eliminated: 0 Frozen: 91594)
|
|
Constraints : 2101210 (Binary: 91.3% Ternary: 6.9% Other: 1.8%)
|
|
|
|
Memory Peak : 436MB
|
|
Max. Length : 35 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 8.55s
|
|
Memory: 407MB (+15MB)
|
|
UNKNOWN
|
|
Iteration Time: 9.44s
|
|
|
|
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: 453.0MB
|
|
Grounding... [('step', [41]), ('step', [42]), ('step', [43]), ('step', [44]), ('step', [45]), ('check', [45])]
|
|
Grounding Time: 0.72s
|
|
Memory: 431MB (+24MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 15
|
|
Time : 79.407s (Solving: 70.22s 1st Model: 0.00s Unsat: 2.40s)
|
|
CPU Time : 79.264s
|
|
|
|
Choices : 1223417 (Domain: 1070592)
|
|
Conflicts : 91188 (Analyzed: 91185)
|
|
Restarts : 1050 (Average: 86.84 Last: 157)
|
|
Model-Level : 183.0
|
|
Problems : 15 (Average Length: 25.33 Splits: 0)
|
|
Lemmas : 91185 (Deleted: 74522)
|
|
Binary : 3852 (Ratio: 4.22%)
|
|
Ternary : 2045 (Ratio: 2.24%)
|
|
Conflict : 91185 (Average Length: 444.0 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 91185 (Average: 12.09 Max: 794 Sum: 1102182)
|
|
Executed : 91068 (Average: 12.06 Max: 794 Sum: 1099554 Ratio: 99.76%)
|
|
Bounded : 117 (Average: 22.46 Max: 47 Sum: 2628 Ratio: 0.24%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 341844 (Eliminated: 0 Frozen: 104044)
|
|
Constraints : 2403164 (Binary: 91.3% Ternary: 6.9% Other: 1.8%)
|
|
|
|
Memory Peak : 482MB
|
|
Max. Length : 40 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 9.63s
|
|
Memory: 481MB (+50MB)
|
|
UNKNOWN
|
|
Iteration Time: 10.69s
|
|
|
|
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: 555.0MB
|
|
Grounding... [('step', [46]), ('step', [47]), ('step', [48]), ('step', [49]), ('step', [50]), ('check', [50])]
|
|
Grounding Time: 0.60s
|
|
Memory: 481MB (+0MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 16
|
|
Time : 90.472s (Solving: 80.24s 1st Model: 0.00s Unsat: 2.40s)
|
|
CPU Time : 90.336s
|
|
|
|
Choices : 1429024 (Domain: 1264883)
|
|
Conflicts : 100027 (Analyzed: 100024)
|
|
Restarts : 1150 (Average: 86.98 Last: 157)
|
|
Model-Level : 183.0
|
|
Problems : 16 (Average Length: 27.00 Splits: 0)
|
|
Lemmas : 100024 (Deleted: 84018)
|
|
Binary : 3987 (Ratio: 3.99%)
|
|
Ternary : 2087 (Ratio: 2.09%)
|
|
Conflict : 100024 (Average Length: 472.5 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 100024 (Average: 12.81 Max: 794 Sum: 1281367)
|
|
Executed : 99905 (Average: 12.78 Max: 794 Sum: 1278640 Ratio: 99.79%)
|
|
Bounded : 119 (Average: 22.92 Max: 52 Sum: 2727 Ratio: 0.21%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 381920 (Eliminated: 0 Frozen: 116494)
|
|
Constraints : 2702017 (Binary: 91.3% Ternary: 6.9% Other: 1.8%)
|
|
|
|
Memory Peak : 527MB
|
|
Max. Length : 45 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 10.12s
|
|
Memory: 490MB (+9MB)
|
|
UNKNOWN
|
|
Iteration Time: 11.08s
|
|
|
|
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: 564.0MB
|
|
Grounding... [('step', [51]), ('step', [52]), ('step', [53]), ('step', [54]), ('step', [55]), ('check', [55])]
|
|
Grounding Time: 0.57s
|
|
Memory: 493MB (+3MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 17
|
|
Time : 100.209s (Solving: 88.95s 1st Model: 0.00s Unsat: 2.40s)
|
|
CPU Time : 100.076s
|
|
|
|
Choices : 1577246 (Domain: 1405775)
|
|
Conflicts : 108978 (Analyzed: 108975)
|
|
Restarts : 1250 (Average: 87.18 Last: 157)
|
|
Model-Level : 183.0
|
|
Problems : 17 (Average Length: 28.76 Splits: 0)
|
|
Lemmas : 108975 (Deleted: 93155)
|
|
Binary : 4109 (Ratio: 3.77%)
|
|
Ternary : 2118 (Ratio: 1.94%)
|
|
Conflict : 108975 (Average Length: 513.6 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 108975 (Average: 12.71 Max: 794 Sum: 1384883)
|
|
Executed : 108856 (Average: 12.68 Max: 794 Sum: 1382156 Ratio: 99.80%)
|
|
Bounded : 119 (Average: 22.92 Max: 52 Sum: 2727 Ratio: 0.20%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 421996 (Eliminated: 0 Frozen: 128944)
|
|
Constraints : 3003983 (Binary: 91.3% Ternary: 6.9% Other: 1.8%)
|
|
|
|
Memory Peak : 552MB
|
|
Max. Length : 50 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 8.80s
|
|
Memory: 513MB (+20MB)
|
|
UNKNOWN
|
|
Iteration Time: 9.75s
|
|
|
|
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: 587.0MB
|
|
Grounding... [('step', [56]), ('step', [57]), ('step', [58]), ('step', [59]), ('step', [60]), ('check', [60])]
|
|
Grounding Time: 0.56s
|
|
Memory: 518MB (+5MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 18
|
|
Time : 110.217s (Solving: 97.92s 1st Model: 0.00s Unsat: 2.40s)
|
|
CPU Time : 110.088s
|
|
|
|
Choices : 1776257 (Domain: 1595430)
|
|
Conflicts : 117090 (Analyzed: 117087)
|
|
Restarts : 1350 (Average: 86.73 Last: 157)
|
|
Model-Level : 183.0
|
|
Problems : 18 (Average Length: 30.61 Splits: 0)
|
|
Lemmas : 117087 (Deleted: 99028)
|
|
Binary : 4216 (Ratio: 3.60%)
|
|
Ternary : 2159 (Ratio: 1.84%)
|
|
Conflict : 117087 (Average Length: 523.8 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 117087 (Average: 13.30 Max: 910 Sum: 1557696)
|
|
Executed : 116968 (Average: 13.28 Max: 910 Sum: 1554969 Ratio: 99.82%)
|
|
Bounded : 119 (Average: 22.92 Max: 52 Sum: 2727 Ratio: 0.18%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 462072 (Eliminated: 0 Frozen: 141394)
|
|
Constraints : 3305963 (Binary: 91.2% Ternary: 6.9% Other: 1.8%)
|
|
|
|
Memory Peak : 586MB
|
|
Max. Length : 55 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 9.07s
|
|
Memory: 542MB (+24MB)
|
|
UNKNOWN
|
|
Iteration Time: 10.02s
|
|
|
|
Iteration 18
|
|
Queue: [(13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True)]
|
|
Grounded Until: 60
|
|
Expected Memory: 616.0MB
|
|
Grounding... [('step', [61]), ('step', [62]), ('step', [63]), ('step', [64]), ('step', [65]), ('check', [65])]
|
|
Grounding Time: 0.56s
|
|
Memory: 549MB (+7MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 19
|
|
Time : 120.307s (Solving: 106.94s 1st Model: 0.00s Unsat: 2.40s)
|
|
CPU Time : 120.184s
|
|
|
|
Choices : 1952515 (Domain: 1767971)
|
|
Conflicts : 125373 (Analyzed: 125370)
|
|
Restarts : 1450 (Average: 86.46 Last: 157)
|
|
Model-Level : 183.0
|
|
Problems : 19 (Average Length: 32.53 Splits: 0)
|
|
Lemmas : 125370 (Deleted: 107415)
|
|
Binary : 4297 (Ratio: 3.43%)
|
|
Ternary : 2186 (Ratio: 1.74%)
|
|
Conflict : 125370 (Average Length: 544.3 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 125370 (Average: 13.53 Max: 910 Sum: 1696732)
|
|
Executed : 125248 (Average: 13.51 Max: 910 Sum: 1693804 Ratio: 99.83%)
|
|
Bounded : 122 (Average: 24.00 Max: 67 Sum: 2928 Ratio: 0.17%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 502148 (Eliminated: 0 Frozen: 153844)
|
|
Constraints : 3607943 (Binary: 91.2% Ternary: 6.9% Other: 1.8%)
|
|
|
|
Memory Peak : 618MB
|
|
Max. Length : 60 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 9.13s
|
|
Memory: 610MB (+61MB)
|
|
UNKNOWN
|
|
Iteration Time: 10.11s
|
|
|
|
Iteration 19
|
|
Queue: [(14,70,0,True), (15,75,0,True), (16,80,0,True)]
|
|
Grounded Until: 65
|
|
Expected Memory: 684.0MB
|
|
Grounding... [('step', [66]), ('step', [67]), ('step', [68]), ('step', [69]), ('step', [70]), ('check', [70])]
|
|
Grounding Time: 0.56s
|
|
Memory: 610MB (+0MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 20
|
|
Time : 130.946s (Solving: 116.50s 1st Model: 0.00s Unsat: 2.40s)
|
|
CPU Time : 130.828s
|
|
|
|
Choices : 2197548 (Domain: 2008753)
|
|
Conflicts : 133633 (Analyzed: 133630)
|
|
Restarts : 1550 (Average: 86.21 Last: 157)
|
|
Model-Level : 183.0
|
|
Problems : 20 (Average Length: 34.50 Splits: 0)
|
|
Lemmas : 133630 (Deleted: 114772)
|
|
Binary : 4403 (Ratio: 3.29%)
|
|
Ternary : 2221 (Ratio: 1.66%)
|
|
Conflict : 133630 (Average Length: 539.3 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 133630 (Average: 14.40 Max: 910 Sum: 1924414)
|
|
Executed : 133505 (Average: 14.38 Max: 910 Sum: 1921270 Ratio: 99.84%)
|
|
Bounded : 125 (Average: 25.15 Max: 72 Sum: 3144 Ratio: 0.16%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 542224 (Eliminated: 0 Frozen: 166294)
|
|
Constraints : 3909881 (Binary: 91.2% Ternary: 6.9% Other: 1.8%)
|
|
|
|
Memory Peak : 676MB
|
|
Max. Length : 65 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 9.67s
|
|
Memory: 615MB (+5MB)
|
|
UNKNOWN
|
|
Iteration Time: 10.66s
|
|
|
|
Iteration 20
|
|
Queue: [(15,75,0,True), (16,80,0,True)]
|
|
Grounded Until: 70
|
|
Expected Memory: 689.0MB
|
|
Grounding... [('step', [71]), ('step', [72]), ('step', [73]), ('step', [74]), ('step', [75]), ('check', [75])]
|
|
Grounding Time: 0.57s
|
|
Memory: 616MB (+1MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 21
|
|
Time : 143.234s (Solving: 127.68s 1st Model: 0.00s Unsat: 2.40s)
|
|
CPU Time : 143.120s
|
|
|
|
Choices : 2401935 (Domain: 2211433)
|
|
Conflicts : 141844 (Analyzed: 141841)
|
|
Restarts : 1650 (Average: 85.96 Last: 157)
|
|
Model-Level : 183.0
|
|
Problems : 21 (Average Length: 36.52 Splits: 0)
|
|
Lemmas : 141841 (Deleted: 122531)
|
|
Binary : 4527 (Ratio: 3.19%)
|
|
Ternary : 2257 (Ratio: 1.59%)
|
|
Conflict : 141841 (Average Length: 531.4 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 141841 (Average: 14.90 Max: 910 Sum: 2113516)
|
|
Executed : 141713 (Average: 14.88 Max: 910 Sum: 2110141 Ratio: 99.84%)
|
|
Bounded : 128 (Average: 26.37 Max: 77 Sum: 3375 Ratio: 0.16%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 582300 (Eliminated: 0 Frozen: 178744)
|
|
Constraints : 4211821 (Binary: 91.2% Ternary: 6.9% Other: 1.8%)
|
|
|
|
Memory Peak : 698MB
|
|
Max. Length : 70 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 11.29s
|
|
Memory: 643MB (+27MB)
|
|
UNKNOWN
|
|
Iteration Time: 12.30s
|
|
|
|
Iteration 21
|
|
Queue: [(16,80,0,True)]
|
|
Grounded Until: 75
|
|
Expected Memory: 717.0MB
|
|
Grounding... [('step', [76]), ('step', [77]), ('step', [78]), ('step', [79]), ('step', [80]), ('check', [80])]
|
|
Grounding Time: 0.57s
|
|
Memory: 643MB (+0MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 22
|
|
Time : 153.637s (Solving: 136.96s 1st Model: 0.00s Unsat: 2.40s)
|
|
CPU Time : 153.528s
|
|
|
|
Choices : 2605196 (Domain: 2410332)
|
|
Conflicts : 150017 (Analyzed: 150014)
|
|
Restarts : 1750 (Average: 85.72 Last: 157)
|
|
Model-Level : 183.0
|
|
Problems : 22 (Average Length: 38.59 Splits: 0)
|
|
Lemmas : 150014 (Deleted: 130452)
|
|
Binary : 4621 (Ratio: 3.08%)
|
|
Ternary : 2282 (Ratio: 1.52%)
|
|
Conflict : 150014 (Average Length: 525.3 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 150014 (Average: 15.26 Max: 1010 Sum: 2289293)
|
|
Executed : 149883 (Average: 15.24 Max: 1010 Sum: 2285672 Ratio: 99.84%)
|
|
Bounded : 131 (Average: 27.64 Max: 82 Sum: 3621 Ratio: 0.16%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 622376 (Eliminated: 0 Frozen: 191194)
|
|
Constraints : 4513760 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
|
|
|
|
Memory Peak : 727MB
|
|
Max. Length : 75 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 9.41s
|
|
Memory: 668MB (+25MB)
|
|
UNKNOWN
|
|
Iteration Time: 10.42s
|
|
|
|
Iteration 22
|
|
Queue: [(4,20,2,True), (5,25,2,True), (6,30,2,True), (7,35,1,True), (8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
|
|
Grounded Until: 80
|
|
Blocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 23
|
|
Time : 162.246s (Solving: 145.43s 1st Model: 0.00s Unsat: 2.40s)
|
|
CPU Time : 162.144s
|
|
|
|
Choices : 2670865 (Domain: 2470369)
|
|
Conflicts : 158594 (Analyzed: 158591)
|
|
Restarts : 1850 (Average: 85.72 Last: 157)
|
|
Model-Level : 183.0
|
|
Problems : 23 (Average Length: 40.48 Splits: 0)
|
|
Lemmas : 158591 (Deleted: 138588)
|
|
Binary : 4772 (Ratio: 3.01%)
|
|
Ternary : 2342 (Ratio: 1.48%)
|
|
Conflict : 158591 (Average Length: 525.0 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 158591 (Average: 14.81 Max: 1010 Sum: 2348653)
|
|
Executed : 158458 (Average: 14.79 Max: 1010 Sum: 2344949 Ratio: 99.84%)
|
|
Bounded : 133 (Average: 27.85 Max: 82 Sum: 3704 Ratio: 0.16%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 622376 (Eliminated: 0 Frozen: 191194)
|
|
Constraints : 4513718 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
|
|
|
|
Memory Peak : 727MB
|
|
Max. Length : 80 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 8.56s
|
|
Memory: 668MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 8.62s
|
|
|
|
Iteration 23
|
|
Queue: [(5,25,2,True), (6,30,2,True), (7,35,1,True), (8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
|
|
Grounded Until: 80
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 24
|
|
Time : 169.973s (Solving: 153.03s 1st Model: 0.00s Unsat: 2.40s)
|
|
CPU Time : 169.876s
|
|
|
|
Choices : 2743021 (Domain: 2537527)
|
|
Conflicts : 167336 (Analyzed: 167333)
|
|
Restarts : 1950 (Average: 85.81 Last: 157)
|
|
Model-Level : 183.0
|
|
Problems : 24 (Average Length: 42.21 Splits: 0)
|
|
Lemmas : 167333 (Deleted: 148243)
|
|
Binary : 4901 (Ratio: 2.93%)
|
|
Ternary : 2416 (Ratio: 1.44%)
|
|
Conflict : 167333 (Average Length: 533.0 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 167333 (Average: 14.39 Max: 1010 Sum: 2407912)
|
|
Executed : 167200 (Average: 14.37 Max: 1010 Sum: 2404208 Ratio: 99.85%)
|
|
Bounded : 133 (Average: 27.85 Max: 82 Sum: 3704 Ratio: 0.15%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 622376 (Eliminated: 0 Frozen: 191194)
|
|
Constraints : 4513705 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
|
|
|
|
Memory Peak : 727MB
|
|
Max. Length : 80 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 7.69s
|
|
Memory: 668MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 7.73s
|
|
|
|
Iteration 24
|
|
Queue: [(6,30,2,True), (7,35,1,True), (8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
|
|
Grounded Until: 80
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 25
|
|
Time : 176.838s (Solving: 159.75s 1st Model: 0.00s Unsat: 2.40s)
|
|
CPU Time : 176.748s
|
|
|
|
Choices : 2793194 (Domain: 2586360)
|
|
Conflicts : 175654 (Analyzed: 175651)
|
|
Restarts : 2050 (Average: 85.68 Last: 157)
|
|
Model-Level : 183.0
|
|
Problems : 25 (Average Length: 43.80 Splits: 0)
|
|
Lemmas : 175651 (Deleted: 154469)
|
|
Binary : 4994 (Ratio: 2.84%)
|
|
Ternary : 2449 (Ratio: 1.39%)
|
|
Conflict : 175651 (Average Length: 523.4 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 175651 (Average: 13.95 Max: 1010 Sum: 2449845)
|
|
Executed : 175518 (Average: 13.93 Max: 1010 Sum: 2446141 Ratio: 99.85%)
|
|
Bounded : 133 (Average: 27.85 Max: 82 Sum: 3704 Ratio: 0.15%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 622376 (Eliminated: 0 Frozen: 191194)
|
|
Constraints : 4513705 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
|
|
|
|
Memory Peak : 727MB
|
|
Max. Length : 80 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 6.82s
|
|
Memory: 668MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 6.87s
|
|
|
|
Iteration 25
|
|
Queue: [(7,35,1,True), (8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
|
|
Grounded Until: 80
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 26
|
|
Time : 184.556s (Solving: 167.33s 1st Model: 0.00s Unsat: 2.40s)
|
|
CPU Time : 184.468s
|
|
|
|
Choices : 2881735 (Domain: 2673125)
|
|
Conflicts : 183975 (Analyzed: 183972)
|
|
Restarts : 2150 (Average: 85.57 Last: 157)
|
|
Model-Level : 183.0
|
|
Problems : 26 (Average Length: 45.27 Splits: 0)
|
|
Lemmas : 183972 (Deleted: 162565)
|
|
Binary : 5040 (Ratio: 2.74%)
|
|
Ternary : 2464 (Ratio: 1.34%)
|
|
Conflict : 183972 (Average Length: 518.7 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 183972 (Average: 13.72 Max: 1010 Sum: 2524861)
|
|
Executed : 183837 (Average: 13.70 Max: 1010 Sum: 2520998 Ratio: 99.85%)
|
|
Bounded : 135 (Average: 28.61 Max: 82 Sum: 3863 Ratio: 0.15%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 622376 (Eliminated: 0 Frozen: 191194)
|
|
Constraints : 4513705 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
|
|
|
|
Memory Peak : 727MB
|
|
Max. Length : 80 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 7.67s
|
|
Memory: 668MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 7.72s
|
|
|
|
Iteration 26
|
|
Queue: [(8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
|
|
Grounded Until: 80
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 27
|
|
Time : 192.272s (Solving: 174.90s 1st Model: 0.00s Unsat: 2.40s)
|
|
CPU Time : 192.188s
|
|
|
|
Choices : 2993870 (Domain: 2779772)
|
|
Conflicts : 192077 (Analyzed: 192074)
|
|
Restarts : 2250 (Average: 85.37 Last: 157)
|
|
Model-Level : 183.0
|
|
Problems : 27 (Average Length: 46.63 Splits: 0)
|
|
Lemmas : 192074 (Deleted: 170725)
|
|
Binary : 5110 (Ratio: 2.66%)
|
|
Ternary : 2477 (Ratio: 1.29%)
|
|
Conflict : 192074 (Average Length: 519.7 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 192074 (Average: 13.64 Max: 1010 Sum: 2620085)
|
|
Executed : 191939 (Average: 13.62 Max: 1010 Sum: 2616222 Ratio: 99.85%)
|
|
Bounded : 135 (Average: 28.61 Max: 82 Sum: 3863 Ratio: 0.15%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 622376 (Eliminated: 0 Frozen: 191194)
|
|
Constraints : 4513691 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
|
|
|
|
Memory Peak : 727MB
|
|
Max. Length : 80 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 7.66s
|
|
Memory: 668MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 7.72s
|
|
|
|
Iteration 27
|
|
Queue: [(9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
|
|
Grounded Until: 80
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 28
|
|
Time : 204.351s (Solving: 186.86s 1st Model: 0.00s Unsat: 2.40s)
|
|
CPU Time : 204.272s
|
|
|
|
Choices : 3317666 (Domain: 3078914)
|
|
Conflicts : 201174 (Analyzed: 201171)
|
|
Restarts : 2350 (Average: 85.60 Last: 157)
|
|
Model-Level : 183.0
|
|
Problems : 28 (Average Length: 47.89 Splits: 0)
|
|
Lemmas : 201171 (Deleted: 180087)
|
|
Binary : 5501 (Ratio: 2.73%)
|
|
Ternary : 2562 (Ratio: 1.27%)
|
|
Conflict : 201171 (Average Length: 536.3 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 201171 (Average: 14.49 Max: 1010 Sum: 2915539)
|
|
Executed : 201036 (Average: 14.47 Max: 1010 Sum: 2911676 Ratio: 99.87%)
|
|
Bounded : 135 (Average: 28.61 Max: 82 Sum: 3863 Ratio: 0.13%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 622376 (Eliminated: 0 Frozen: 191194)
|
|
Constraints : 4513691 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
|
|
|
|
Memory Peak : 727MB
|
|
Max. Length : 80 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 12.04s
|
|
Memory: 668MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 12.09s
|
|
|
|
Iteration 28
|
|
Queue: [(10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
|
|
Grounded Until: 80
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 29
|
|
Time : 211.665s (Solving: 194.04s 1st Model: 0.00s Unsat: 2.40s)
|
|
CPU Time : 211.588s
|
|
|
|
Choices : 3439190 (Domain: 3199143)
|
|
Conflicts : 208925 (Analyzed: 208922)
|
|
Restarts : 2450 (Average: 85.27 Last: 157)
|
|
Model-Level : 183.0
|
|
Problems : 29 (Average Length: 49.07 Splits: 0)
|
|
Lemmas : 208922 (Deleted: 186770)
|
|
Binary : 5579 (Ratio: 2.67%)
|
|
Ternary : 2572 (Ratio: 1.23%)
|
|
Conflict : 208922 (Average Length: 528.9 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 208922 (Average: 14.47 Max: 1010 Sum: 3023317)
|
|
Executed : 208787 (Average: 14.45 Max: 1010 Sum: 3019454 Ratio: 99.87%)
|
|
Bounded : 135 (Average: 28.61 Max: 82 Sum: 3863 Ratio: 0.13%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 622376 (Eliminated: 0 Frozen: 191194)
|
|
Constraints : 4513691 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
|
|
|
|
Memory Peak : 727MB
|
|
Max. Length : 80 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 7.27s
|
|
Memory: 668MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 7.32s
|
|
|
|
Iteration 29
|
|
Queue: [(11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
|
|
Grounded Until: 80
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 30
|
|
Time : 217.857s (Solving: 200.09s 1st Model: 0.00s Unsat: 2.40s)
|
|
CPU Time : 217.784s
|
|
|
|
Choices : 3520051 (Domain: 3279560)
|
|
Conflicts : 216107 (Analyzed: 216104)
|
|
Restarts : 2550 (Average: 84.75 Last: 157)
|
|
Model-Level : 183.0
|
|
Problems : 30 (Average Length: 50.17 Splits: 0)
|
|
Lemmas : 216104 (Deleted: 194246)
|
|
Binary : 5641 (Ratio: 2.61%)
|
|
Ternary : 2593 (Ratio: 1.20%)
|
|
Conflict : 216104 (Average Length: 523.9 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 216104 (Average: 14.31 Max: 1010 Sum: 3091425)
|
|
Executed : 215969 (Average: 14.29 Max: 1010 Sum: 3087562 Ratio: 99.88%)
|
|
Bounded : 135 (Average: 28.61 Max: 82 Sum: 3863 Ratio: 0.12%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 622376 (Eliminated: 0 Frozen: 191194)
|
|
Constraints : 4513691 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
|
|
|
|
Memory Peak : 727MB
|
|
Max. Length : 80 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 6.14s
|
|
Memory: 668MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 6.20s
|
|
|
|
Iteration 30
|
|
Queue: [(12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
|
|
Grounded Until: 80
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 31
|
|
Time : 224.621s (Solving: 206.70s 1st Model: 0.00s Unsat: 2.40s)
|
|
CPU Time : 224.548s
|
|
|
|
Choices : 3585219 (Domain: 3344599)
|
|
Conflicts : 224007 (Analyzed: 224004)
|
|
Restarts : 2650 (Average: 84.53 Last: 157)
|
|
Model-Level : 183.0
|
|
Problems : 31 (Average Length: 51.19 Splits: 0)
|
|
Lemmas : 224004 (Deleted: 201238)
|
|
Binary : 5663 (Ratio: 2.53%)
|
|
Ternary : 2601 (Ratio: 1.16%)
|
|
Conflict : 224004 (Average Length: 515.5 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 224004 (Average: 14.05 Max: 1010 Sum: 3146534)
|
|
Executed : 223868 (Average: 14.03 Max: 1010 Sum: 3142594 Ratio: 99.87%)
|
|
Bounded : 136 (Average: 28.97 Max: 82 Sum: 3940 Ratio: 0.13%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 622376 (Eliminated: 0 Frozen: 191194)
|
|
Constraints : 4513691 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
|
|
|
|
Memory Peak : 727MB
|
|
Max. Length : 80 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 6.71s
|
|
Memory: 668MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 6.77s
|
|
|
|
Iteration 31
|
|
Queue: [(13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
|
|
Grounded Until: 80
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 32
|
|
Time : 233.395s (Solving: 215.32s 1st Model: 0.00s Unsat: 2.40s)
|
|
CPU Time : 233.328s
|
|
|
|
Choices : 3731353 (Domain: 3489030)
|
|
Conflicts : 232313 (Analyzed: 232310)
|
|
Restarts : 2750 (Average: 84.48 Last: 157)
|
|
Model-Level : 183.0
|
|
Problems : 32 (Average Length: 52.16 Splits: 0)
|
|
Lemmas : 232310 (Deleted: 208952)
|
|
Binary : 5741 (Ratio: 2.47%)
|
|
Ternary : 2619 (Ratio: 1.13%)
|
|
Conflict : 232310 (Average Length: 509.9 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 232310 (Average: 14.11 Max: 1010 Sum: 3277720)
|
|
Executed : 232173 (Average: 14.09 Max: 1010 Sum: 3273698 Ratio: 99.88%)
|
|
Bounded : 137 (Average: 29.36 Max: 82 Sum: 4022 Ratio: 0.12%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 622376 (Eliminated: 0 Frozen: 191194)
|
|
Constraints : 4513691 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
|
|
|
|
Memory Peak : 727MB
|
|
Max. Length : 80 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 8.72s
|
|
Memory: 668MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 8.78s
|
|
|
|
Iteration 32
|
|
Queue: [(14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
|
|
Grounded Until: 80
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 33
|
|
Time : 243.720s (Solving: 225.52s 1st Model: 0.00s Unsat: 2.40s)
|
|
CPU Time : 243.660s
|
|
|
|
Choices : 3939332 (Domain: 3695182)
|
|
Conflicts : 240640 (Analyzed: 240637)
|
|
Restarts : 2850 (Average: 84.43 Last: 157)
|
|
Model-Level : 183.0
|
|
Problems : 33 (Average Length: 53.06 Splits: 0)
|
|
Lemmas : 240637 (Deleted: 216962)
|
|
Binary : 5848 (Ratio: 2.43%)
|
|
Ternary : 2635 (Ratio: 1.10%)
|
|
Conflict : 240637 (Average Length: 505.6 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 240637 (Average: 14.41 Max: 1010 Sum: 3468650)
|
|
Executed : 240499 (Average: 14.40 Max: 1010 Sum: 3464546 Ratio: 99.88%)
|
|
Bounded : 138 (Average: 29.74 Max: 82 Sum: 4104 Ratio: 0.12%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 622376 (Eliminated: 0 Frozen: 191194)
|
|
Constraints : 4513693 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
|
|
|
|
Memory Peak : 727MB
|
|
Max. Length : 80 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 10.29s
|
|
Memory: 668MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 10.33s
|
|
|
|
Iteration 33
|
|
Queue: [(15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
|
|
Grounded Until: 80
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 34
|
|
Time : 252.404s (Solving: 234.05s 1st Model: 0.00s Unsat: 2.40s)
|
|
CPU Time : 252.348s
|
|
|
|
Choices : 4104662 (Domain: 3859160)
|
|
Conflicts : 248722 (Analyzed: 248719)
|
|
Restarts : 2950 (Average: 84.31 Last: 157)
|
|
Model-Level : 183.0
|
|
Problems : 34 (Average Length: 53.91 Splits: 0)
|
|
Lemmas : 248719 (Deleted: 224964)
|
|
Binary : 5921 (Ratio: 2.38%)
|
|
Ternary : 2653 (Ratio: 1.07%)
|
|
Conflict : 248719 (Average Length: 500.1 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 248719 (Average: 14.54 Max: 1044 Sum: 3617011)
|
|
Executed : 248579 (Average: 14.53 Max: 1044 Sum: 3612747 Ratio: 99.88%)
|
|
Bounded : 140 (Average: 30.46 Max: 82 Sum: 4264 Ratio: 0.12%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 622376 (Eliminated: 0 Frozen: 191194)
|
|
Constraints : 4513679 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
|
|
|
|
Memory Peak : 727MB
|
|
Max. Length : 80 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 8.63s
|
|
Memory: 668MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 8.69s
|
|
|
|
Iteration 34
|
|
Queue: [(16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
|
|
Grounded Until: 80
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 35
|
|
Time : 260.213s (Solving: 241.73s 1st Model: 0.00s Unsat: 2.40s)
|
|
CPU Time : 260.160s
|
|
|
|
Choices : 4269250 (Domain: 4022750)
|
|
Conflicts : 256518 (Analyzed: 256515)
|
|
Restarts : 3050 (Average: 84.10 Last: 157)
|
|
Model-Level : 183.0
|
|
Problems : 35 (Average Length: 54.71 Splits: 0)
|
|
Lemmas : 256515 (Deleted: 232812)
|
|
Binary : 5995 (Ratio: 2.34%)
|
|
Ternary : 2672 (Ratio: 1.04%)
|
|
Conflict : 256515 (Average Length: 496.1 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 256515 (Average: 14.68 Max: 1044 Sum: 3765684)
|
|
Executed : 256374 (Average: 14.66 Max: 1044 Sum: 3761338 Ratio: 99.88%)
|
|
Bounded : 141 (Average: 30.82 Max: 82 Sum: 4346 Ratio: 0.12%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 622376 (Eliminated: 0 Frozen: 191194)
|
|
Constraints : 4513665 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
|
|
|
|
Memory Peak : 727MB
|
|
Max. Length : 80 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 7.77s
|
|
Memory: 668MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 7.82s
|
|
|
|
Iteration 35
|
|
Queue: [(17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
|
|
Grounded Until: 80
|
|
Expected Memory: 742.0MB
|
|
Grounding... [('step', [81]), ('step', [82]), ('step', [83]), ('step', [84]), ('step', [85]), ('check', [85])]
|
|
Grounding Time: 0.60s
|
|
Memory: 668MB (+0MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 36
|
|
Time : 267.786s (Solving: 248.11s 1st Model: 0.00s Unsat: 2.40s)
|
|
CPU Time : 267.736s
|
|
|
|
Choices : 4348686 (Domain: 4101788)
|
|
Conflicts : 264283 (Analyzed: 264280)
|
|
Restarts : 3150 (Average: 83.90 Last: 157)
|
|
Model-Level : 183.0
|
|
Problems : 36 (Average Length: 55.61 Splits: 0)
|
|
Lemmas : 264280 (Deleted: 240259)
|
|
Binary : 6036 (Ratio: 2.28%)
|
|
Ternary : 2685 (Ratio: 1.02%)
|
|
Conflict : 264280 (Average Length: 490.5 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 264280 (Average: 14.49 Max: 1044 Sum: 3830386)
|
|
Executed : 264137 (Average: 14.48 Max: 1044 Sum: 3825871 Ratio: 99.88%)
|
|
Bounded : 143 (Average: 31.57 Max: 87 Sum: 4515 Ratio: 0.12%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 662452 (Eliminated: 0 Frozen: 203644)
|
|
Constraints : 4815631 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
|
|
|
|
Memory Peak : 755MB
|
|
Max. Length : 80 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 6.51s
|
|
Memory: 691MB (+23MB)
|
|
UNKNOWN
|
|
Iteration Time: 7.59s
|
|
|
|
Iteration 36
|
|
Queue: [(18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
|
|
Grounded Until: 85
|
|
Expected Memory: 765.0MB
|
|
Grounding... [('step', [86]), ('step', [87]), ('step', [88]), ('step', [89]), ('step', [90]), ('check', [90])]
|
|
Grounding Time: 0.59s
|
|
Memory: 691MB (+0MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 37
|
|
Time : 280.324s (Solving: 259.44s 1st Model: 0.00s Unsat: 2.40s)
|
|
CPU Time : 280.280s
|
|
|
|
Choices : 4806070 (Domain: 4550562)
|
|
Conflicts : 272656 (Analyzed: 272653)
|
|
Restarts : 3250 (Average: 83.89 Last: 157)
|
|
Model-Level : 183.0
|
|
Problems : 37 (Average Length: 56.59 Splits: 0)
|
|
Lemmas : 272653 (Deleted: 247693)
|
|
Binary : 6270 (Ratio: 2.30%)
|
|
Ternary : 2729 (Ratio: 1.00%)
|
|
Conflict : 272653 (Average Length: 500.5 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 272653 (Average: 15.62 Max: 1044 Sum: 4257604)
|
|
Executed : 272510 (Average: 15.60 Max: 1044 Sum: 4253089 Ratio: 99.89%)
|
|
Bounded : 143 (Average: 31.57 Max: 87 Sum: 4515 Ratio: 0.11%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 702528 (Eliminated: 0 Frozen: 216094)
|
|
Constraints : 5114549 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
|
|
|
|
Memory Peak : 790MB
|
|
Max. Length : 85 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 11.47s
|
|
Memory: 763MB (+72MB)
|
|
UNKNOWN
|
|
Iteration Time: 12.56s
|
|
|
|
Iteration 37
|
|
Queue: [(19,95,0,True), (20,100,0,True), (21,105,0,True)]
|
|
Grounded Until: 90
|
|
Expected Memory: 837.0MB
|
|
Grounding... [('step', [91]), ('step', [92]), ('step', [93]), ('step', [94]), ('step', [95]), ('check', [95])]
|
|
Grounding Time: 0.95s
|
|
Memory: 813MB (+50MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 38
|
|
Time : 296.936s (Solving: 274.46s 1st Model: 0.00s Unsat: 2.40s)
|
|
CPU Time : 296.896s
|
|
|
|
Choices : 5382955 (Domain: 5117111)
|
|
Conflicts : 281712 (Analyzed: 281709)
|
|
Restarts : 3350 (Average: 84.09 Last: 157)
|
|
Model-Level : 183.0
|
|
Problems : 38 (Average Length: 57.66 Splits: 0)
|
|
Lemmas : 281709 (Deleted: 257600)
|
|
Binary : 6538 (Ratio: 2.32%)
|
|
Ternary : 2790 (Ratio: 0.99%)
|
|
Conflict : 281709 (Average Length: 525.8 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 281709 (Average: 17.02 Max: 1044 Sum: 4793424)
|
|
Executed : 281566 (Average: 17.00 Max: 1044 Sum: 4788909 Ratio: 99.91%)
|
|
Bounded : 143 (Average: 31.57 Max: 87 Sum: 4515 Ratio: 0.09%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 742604 (Eliminated: 0 Frozen: 228544)
|
|
Constraints : 5416529 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
|
|
|
|
Memory Peak : 946MB
|
|
Max. Length : 90 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 15.16s
|
|
Memory: 882MB (+69MB)
|
|
UNKNOWN
|
|
Iteration Time: 16.63s
|
|
|
|
Iteration 38
|
|
Queue: [(20,100,0,True), (21,105,0,True)]
|
|
Grounded Until: 95
|
|
Expected Memory: 1001.0MB
|
|
Grounding... [('step', [96]), ('step', [97]), ('step', [98]), ('step', [99]), ('step', [100]), ('check', [100])]
|
|
Grounding Time: 0.56s
|
|
Memory: 882MB (+0MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 39
|
|
Time : 305.801s (Solving: 282.12s 1st Model: 0.00s Unsat: 2.40s)
|
|
CPU Time : 305.764s
|
|
|
|
Choices : 5562451 (Domain: 5295760)
|
|
Conflicts : 289712 (Analyzed: 289709)
|
|
Restarts : 3450 (Average: 83.97 Last: 157)
|
|
Model-Level : 183.0
|
|
Problems : 39 (Average Length: 58.79 Splits: 0)
|
|
Lemmas : 289709 (Deleted: 264065)
|
|
Binary : 6653 (Ratio: 2.30%)
|
|
Ternary : 2806 (Ratio: 0.97%)
|
|
Conflict : 289709 (Average Length: 519.8 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 289709 (Average: 17.11 Max: 1273 Sum: 4955544)
|
|
Executed : 289565 (Average: 17.09 Max: 1273 Sum: 4950927 Ratio: 99.91%)
|
|
Bounded : 144 (Average: 32.06 Max: 102 Sum: 4617 Ratio: 0.09%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 782680 (Eliminated: 0 Frozen: 240994)
|
|
Constraints : 5718509 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
|
|
|
|
Memory Peak : 977MB
|
|
Max. Length : 95 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 7.81s
|
|
Memory: 888MB (+6MB)
|
|
UNKNOWN
|
|
Iteration Time: 8.88s
|
|
|
|
Iteration 39
|
|
Queue: [(21,105,0,True)]
|
|
Grounded Until: 100
|
|
Expected Memory: 1007.0MB
|
|
Grounding... [('step', [101]), ('step', [102]), ('step', [103]), ('step', [104]), ('step', [105]), ('check', [105])]
|
|
Grounding Time: 0.55s
|
|
Memory: 889MB (+1MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 40
|
|
Time : 314.321s (Solving: 289.43s 1st Model: 0.00s Unsat: 2.40s)
|
|
CPU Time : 314.288s
|
|
|
|
Choices : 5768001 (Domain: 5500320)
|
|
Conflicts : 297542 (Analyzed: 297539)
|
|
Restarts : 3550 (Average: 83.81 Last: 157)
|
|
Model-Level : 183.0
|
|
Problems : 40 (Average Length: 60.00 Splits: 0)
|
|
Lemmas : 297539 (Deleted: 271686)
|
|
Binary : 6728 (Ratio: 2.26%)
|
|
Ternary : 2824 (Ratio: 0.95%)
|
|
Conflict : 297539 (Average Length: 515.1 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 297539 (Average: 17.28 Max: 1374 Sum: 5142263)
|
|
Executed : 297394 (Average: 17.27 Max: 1374 Sum: 5137542 Ratio: 99.91%)
|
|
Bounded : 145 (Average: 32.56 Max: 104 Sum: 4721 Ratio: 0.09%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 822756 (Eliminated: 0 Frozen: 253444)
|
|
Constraints : 6020476 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
|
|
|
|
Memory Peak : 1005MB
|
|
Max. Length : 100 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 7.46s
|
|
Memory: 914MB (+25MB)
|
|
UNKNOWN
|
|
Iteration Time: 8.54s
|
|
|
|
Iteration 40
|
|
Queue: [(4,20,3,True), (5,25,3,True), (6,30,3,True), (7,35,2,True), (8,40,2,True), (9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)]
|
|
Grounded Until: 105
|
|
Blocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 41
|
|
Time : 321.643s (Solving: 296.58s 1st Model: 0.00s Unsat: 2.40s)
|
|
CPU Time : 321.616s
|
|
|
|
Choices : 5826604 (Domain: 5558923)
|
|
Conflicts : 305230 (Analyzed: 305227)
|
|
Restarts : 3650 (Average: 83.62 Last: 157)
|
|
Model-Level : 183.0
|
|
Problems : 41 (Average Length: 61.15 Splits: 0)
|
|
Lemmas : 305227 (Deleted: 279254)
|
|
Binary : 6823 (Ratio: 2.24%)
|
|
Ternary : 2826 (Ratio: 0.93%)
|
|
Conflict : 305227 (Average Length: 512.0 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 305227 (Average: 17.02 Max: 1374 Sum: 5195791)
|
|
Executed : 305082 (Average: 17.01 Max: 1374 Sum: 5191070 Ratio: 99.91%)
|
|
Bounded : 145 (Average: 32.56 Max: 104 Sum: 4721 Ratio: 0.09%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 822756 (Eliminated: 0 Frozen: 253444)
|
|
Constraints : 6020476 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
|
|
|
|
Memory Peak : 1005MB
|
|
Max. Length : 105 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 7.27s
|
|
Memory: 914MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 7.33s
|
|
|
|
Iteration 41
|
|
Queue: [(5,25,3,True), (6,30,3,True), (7,35,2,True), (8,40,2,True), (9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)]
|
|
Grounded Until: 105
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 42
|
|
Time : 330.430s (Solving: 305.20s 1st Model: 0.00s Unsat: 2.40s)
|
|
CPU Time : 330.408s
|
|
|
|
Choices : 5896868 (Domain: 5623680)
|
|
Conflicts : 313655 (Analyzed: 313652)
|
|
Restarts : 3750 (Average: 83.64 Last: 157)
|
|
Model-Level : 183.0
|
|
Problems : 42 (Average Length: 62.24 Splits: 0)
|
|
Lemmas : 313652 (Deleted: 286601)
|
|
Binary : 6949 (Ratio: 2.22%)
|
|
Ternary : 2855 (Ratio: 0.91%)
|
|
Conflict : 313652 (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 : 313652 (Average: 16.75 Max: 1374 Sum: 5252391)
|
|
Executed : 313507 (Average: 16.73 Max: 1374 Sum: 5247670 Ratio: 99.91%)
|
|
Bounded : 145 (Average: 32.56 Max: 104 Sum: 4721 Ratio: 0.09%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 822756 (Eliminated: 0 Frozen: 253444)
|
|
Constraints : 6020476 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
|
|
|
|
Memory Peak : 1005MB
|
|
Max. Length : 105 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 8.73s
|
|
Memory: 914MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 8.79s
|
|
|
|
Iteration 42
|
|
Queue: [(6,30,3,True), (7,35,2,True), (8,40,2,True), (9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)]
|
|
Grounded Until: 105
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 43
|
|
Time : 335.159s (Solving: 309.74s 1st Model: 0.00s Unsat: 2.40s)
|
|
CPU Time : 335.140s
|
|
|
|
Choices : 5947391 (Domain: 5673356)
|
|
Conflicts : 321491 (Analyzed: 321488)
|
|
Restarts : 3850 (Average: 83.50 Last: 157)
|
|
Model-Level : 183.0
|
|
Problems : 43 (Average Length: 63.28 Splits: 0)
|
|
Lemmas : 321488 (Deleted: 294702)
|
|
Binary : 6992 (Ratio: 2.17%)
|
|
Ternary : 2866 (Ratio: 0.89%)
|
|
Conflict : 321488 (Average Length: 514.4 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 321488 (Average: 16.47 Max: 1374 Sum: 5294129)
|
|
Executed : 321343 (Average: 16.45 Max: 1374 Sum: 5289408 Ratio: 99.91%)
|
|
Bounded : 145 (Average: 32.56 Max: 104 Sum: 4721 Ratio: 0.09%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 822756 (Eliminated: 0 Frozen: 253444)
|
|
Constraints : 6020476 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
|
|
|
|
Memory Peak : 1005MB
|
|
Max. Length : 105 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 4.66s
|
|
Memory: 914MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 4.74s
|
|
|
|
Iteration 43
|
|
Queue: [(7,35,2,True), (8,40,2,True), (9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)]
|
|
Grounded Until: 105
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 44
|
|
Time : 342.312s (Solving: 316.69s 1st Model: 0.00s Unsat: 2.40s)
|
|
CPU Time : 342.296s
|
|
|
|
Choices : 6036512 (Domain: 5760556)
|
|
Conflicts : 329836 (Analyzed: 329833)
|
|
Restarts : 3950 (Average: 83.50 Last: 185)
|
|
Model-Level : 183.0
|
|
Problems : 44 (Average Length: 64.27 Splits: 0)
|
|
Lemmas : 329833 (Deleted: 302258)
|
|
Binary : 7076 (Ratio: 2.15%)
|
|
Ternary : 2884 (Ratio: 0.87%)
|
|
Conflict : 329833 (Average Length: 510.4 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 329833 (Average: 16.29 Max: 1374 Sum: 5372439)
|
|
Executed : 329685 (Average: 16.27 Max: 1374 Sum: 5367404 Ratio: 99.91%)
|
|
Bounded : 148 (Average: 34.02 Max: 107 Sum: 5035 Ratio: 0.09%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 822756 (Eliminated: 0 Frozen: 253444)
|
|
Constraints : 6020476 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
|
|
|
|
Memory Peak : 1005MB
|
|
Max. Length : 105 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 7.08s
|
|
Memory: 914MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 7.16s
|
|
|
|
Iteration 44
|
|
Queue: [(8,40,2,True), (9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)]
|
|
Grounded Until: 105
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 45
|
|
Time : 350.390s (Solving: 324.61s 1st Model: 0.00s Unsat: 2.40s)
|
|
CPU Time : 350.380s
|
|
|
|
Choices : 6168437 (Domain: 5888804)
|
|
Conflicts : 338780 (Analyzed: 338777)
|
|
Restarts : 4050 (Average: 83.65 Last: 185)
|
|
Model-Level : 183.0
|
|
Problems : 45 (Average Length: 65.22 Splits: 0)
|
|
Lemmas : 338777 (Deleted: 312440)
|
|
Binary : 7165 (Ratio: 2.11%)
|
|
Ternary : 2895 (Ratio: 0.85%)
|
|
Conflict : 338777 (Average Length: 510.5 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 338777 (Average: 16.20 Max: 1374 Sum: 5488988)
|
|
Executed : 338629 (Average: 16.19 Max: 1374 Sum: 5483953 Ratio: 99.91%)
|
|
Bounded : 148 (Average: 34.02 Max: 107 Sum: 5035 Ratio: 0.09%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 822756 (Eliminated: 0 Frozen: 253444)
|
|
Constraints : 6020462 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
|
|
|
|
Memory Peak : 1005MB
|
|
Max. Length : 105 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 8.03s
|
|
Memory: 914MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 8.09s
|
|
|
|
Iteration 45
|
|
Queue: [(9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)]
|
|
Grounded Until: 105
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 46
|
|
Time : 357.056s (Solving: 331.11s 1st Model: 0.00s Unsat: 2.40s)
|
|
CPU Time : 357.048s
|
|
|
|
Choices : 6280639 (Domain: 5999286)
|
|
Conflicts : 346955 (Analyzed: 346952)
|
|
Restarts : 4150 (Average: 83.60 Last: 185)
|
|
Model-Level : 183.0
|
|
Problems : 46 (Average Length: 66.13 Splits: 0)
|
|
Lemmas : 346952 (Deleted: 318946)
|
|
Binary : 7213 (Ratio: 2.08%)
|
|
Ternary : 2904 (Ratio: 0.84%)
|
|
Conflict : 346952 (Average Length: 509.3 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 346952 (Average: 16.10 Max: 1374 Sum: 5586987)
|
|
Executed : 346804 (Average: 16.09 Max: 1374 Sum: 5581952 Ratio: 99.91%)
|
|
Bounded : 148 (Average: 34.02 Max: 107 Sum: 5035 Ratio: 0.09%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 822756 (Eliminated: 0 Frozen: 253444)
|
|
Constraints : 6020462 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
|
|
|
|
Memory Peak : 1005MB
|
|
Max. Length : 105 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 6.61s
|
|
Memory: 914MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 6.67s
|
|
|
|
Iteration 46
|
|
Queue: [(10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)]
|
|
Grounded Until: 105
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 47
|
|
Time : 364.389s (Solving: 338.29s 1st Model: 0.00s Unsat: 2.40s)
|
|
CPU Time : 364.384s
|
|
|
|
Choices : 6439253 (Domain: 6155618)
|
|
Conflicts : 355230 (Analyzed: 355227)
|
|
Restarts : 4250 (Average: 83.58 Last: 185)
|
|
Model-Level : 183.0
|
|
Problems : 47 (Average Length: 67.00 Splits: 0)
|
|
Lemmas : 355227 (Deleted: 326815)
|
|
Binary : 7410 (Ratio: 2.09%)
|
|
Ternary : 3010 (Ratio: 0.85%)
|
|
Conflict : 355227 (Average Length: 506.1 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 355227 (Average: 16.13 Max: 1374 Sum: 5731234)
|
|
Executed : 355078 (Average: 16.12 Max: 1374 Sum: 5726095 Ratio: 99.91%)
|
|
Bounded : 149 (Average: 34.49 Max: 107 Sum: 5139 Ratio: 0.09%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 822756 (Eliminated: 0 Frozen: 253444)
|
|
Constraints : 6020462 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
|
|
|
|
Memory Peak : 1005MB
|
|
Max. Length : 105 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 7.28s
|
|
Memory: 914MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 7.34s
|
|
|
|
Iteration 47
|
|
Queue: [(11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)]
|
|
Grounded Until: 105
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 48
|
|
Time : 372.105s (Solving: 345.82s 1st Model: 0.00s Unsat: 2.40s)
|
|
CPU Time : 372.104s
|
|
|
|
Choices : 6631973 (Domain: 6346310)
|
|
Conflicts : 363365 (Analyzed: 363362)
|
|
Restarts : 4350 (Average: 83.53 Last: 185)
|
|
Model-Level : 183.0
|
|
Problems : 48 (Average Length: 67.83 Splits: 0)
|
|
Lemmas : 363362 (Deleted: 334432)
|
|
Binary : 7577 (Ratio: 2.09%)
|
|
Ternary : 3087 (Ratio: 0.85%)
|
|
Conflict : 363362 (Average Length: 504.6 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 363362 (Average: 16.26 Max: 1374 Sum: 5907978)
|
|
Executed : 363212 (Average: 16.24 Max: 1374 Sum: 5902732 Ratio: 99.91%)
|
|
Bounded : 150 (Average: 34.97 Max: 107 Sum: 5246 Ratio: 0.09%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 822756 (Eliminated: 0 Frozen: 253444)
|
|
Constraints : 6020462 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
|
|
|
|
Memory Peak : 1005MB
|
|
Max. Length : 105 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 7.65s
|
|
Memory: 914MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 7.72s
|
|
|
|
Iteration 48
|
|
Queue: [(12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)]
|
|
Grounded Until: 105
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 49
|
|
Time : 379.766s (Solving: 353.29s 1st Model: 0.00s Unsat: 2.40s)
|
|
CPU Time : 379.768s
|
|
|
|
Choices : 6831592 (Domain: 6541482)
|
|
Conflicts : 371683 (Analyzed: 371680)
|
|
Restarts : 4450 (Average: 83.52 Last: 185)
|
|
Model-Level : 183.0
|
|
Problems : 49 (Average Length: 68.63 Splits: 0)
|
|
Lemmas : 371680 (Deleted: 342205)
|
|
Binary : 7672 (Ratio: 2.06%)
|
|
Ternary : 3104 (Ratio: 0.84%)
|
|
Conflict : 371680 (Average Length: 503.5 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 371680 (Average: 16.37 Max: 1374 Sum: 6084055)
|
|
Executed : 371530 (Average: 16.35 Max: 1374 Sum: 6078809 Ratio: 99.91%)
|
|
Bounded : 150 (Average: 34.97 Max: 107 Sum: 5246 Ratio: 0.09%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 822756 (Eliminated: 0 Frozen: 253444)
|
|
Constraints : 6020448 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
|
|
|
|
Memory Peak : 1005MB
|
|
Max. Length : 105 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 7.59s
|
|
Memory: 914MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 7.67s
|
|
|
|
Iteration 49
|
|
Queue: [(13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)]
|
|
Grounded Until: 105
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 50
|
|
Time : 389.333s (Solving: 362.66s 1st Model: 0.00s Unsat: 2.40s)
|
|
CPU Time : 389.340s
|
|
|
|
Choices : 7114481 (Domain: 6821255)
|
|
Conflicts : 380450 (Analyzed: 380447)
|
|
Restarts : 4550 (Average: 83.61 Last: 185)
|
|
Model-Level : 183.0
|
|
Problems : 50 (Average Length: 69.40 Splits: 0)
|
|
Lemmas : 380447 (Deleted: 352305)
|
|
Binary : 7803 (Ratio: 2.05%)
|
|
Ternary : 3142 (Ratio: 0.83%)
|
|
Conflict : 380447 (Average Length: 502.3 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 380447 (Average: 16.68 Max: 1374 Sum: 6346973)
|
|
Executed : 380297 (Average: 16.67 Max: 1374 Sum: 6341727 Ratio: 99.92%)
|
|
Bounded : 150 (Average: 34.97 Max: 107 Sum: 5246 Ratio: 0.08%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 822756 (Eliminated: 0 Frozen: 253444)
|
|
Constraints : 6020448 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
|
|
|
|
Memory Peak : 1005MB
|
|
Max. Length : 105 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 9.49s
|
|
Memory: 914MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 9.57s
|
|
|
|
Iteration 50
|
|
Queue: [(17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)]
|
|
Grounded Until: 105
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 51
|
|
Time : 399.271s (Solving: 372.43s 1st Model: 0.00s Unsat: 2.40s)
|
|
CPU Time : 399.276s
|
|
|
|
Choices : 7405815 (Domain: 7110612)
|
|
Conflicts : 388712 (Analyzed: 388709)
|
|
Restarts : 4650 (Average: 83.59 Last: 185)
|
|
Model-Level : 183.0
|
|
Problems : 51 (Average Length: 70.14 Splits: 0)
|
|
Lemmas : 388709 (Deleted: 358623)
|
|
Binary : 7858 (Ratio: 2.02%)
|
|
Ternary : 3160 (Ratio: 0.81%)
|
|
Conflict : 388709 (Average Length: 504.2 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 388709 (Average: 17.02 Max: 1374 Sum: 6614005)
|
|
Executed : 388559 (Average: 17.00 Max: 1374 Sum: 6608759 Ratio: 99.92%)
|
|
Bounded : 150 (Average: 34.97 Max: 107 Sum: 5246 Ratio: 0.08%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 822756 (Eliminated: 0 Frozen: 253444)
|
|
Constraints : 6020448 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
|
|
|
|
Memory Peak : 1005MB
|
|
Max. Length : 105 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 9.88s
|
|
Memory: 914MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 9.94s
|
|
|
|
Iteration 51
|
|
Queue: [(18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)]
|
|
Grounded Until: 105
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 52
|
|
Time : 412.928s (Solving: 385.89s 1st Model: 0.00s Unsat: 2.40s)
|
|
CPU Time : 412.936s
|
|
|
|
Choices : 7920513 (Domain: 7620183)
|
|
Conflicts : 397908 (Analyzed: 397905)
|
|
Restarts : 4750 (Average: 83.77 Last: 185)
|
|
Model-Level : 183.0
|
|
Problems : 52 (Average Length: 70.85 Splits: 0)
|
|
Lemmas : 397905 (Deleted: 368777)
|
|
Binary : 8035 (Ratio: 2.02%)
|
|
Ternary : 3185 (Ratio: 0.80%)
|
|
Conflict : 397905 (Average Length: 510.3 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 397905 (Average: 17.84 Max: 1374 Sum: 7097953)
|
|
Executed : 397755 (Average: 17.83 Max: 1374 Sum: 7092707 Ratio: 99.93%)
|
|
Bounded : 150 (Average: 34.97 Max: 107 Sum: 5246 Ratio: 0.07%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 822756 (Eliminated: 0 Frozen: 253444)
|
|
Constraints : 6020448 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
|
|
|
|
Memory Peak : 1005MB
|
|
Max. Length : 105 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 13.58s
|
|
Memory: 914MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 13.67s
|
|
|
|
Iteration 52
|
|
Queue: [(19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)]
|
|
Grounded Until: 105
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 53
|
|
Time : 420.742s (Solving: 393.51s 1st Model: 0.00s Unsat: 2.40s)
|
|
CPU Time : 420.752s
|
|
|
|
Choices : 8140639 (Domain: 7838774)
|
|
Conflicts : 405543 (Analyzed: 405540)
|
|
Restarts : 4850 (Average: 83.62 Last: 185)
|
|
Model-Level : 183.0
|
|
Problems : 53 (Average Length: 71.53 Splits: 0)
|
|
Lemmas : 405540 (Deleted: 375482)
|
|
Binary : 8079 (Ratio: 1.99%)
|
|
Ternary : 3192 (Ratio: 0.79%)
|
|
Conflict : 405540 (Average Length: 509.0 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 405540 (Average: 18.00 Max: 1374 Sum: 7298202)
|
|
Executed : 405390 (Average: 17.98 Max: 1374 Sum: 7292956 Ratio: 99.93%)
|
|
Bounded : 150 (Average: 34.97 Max: 107 Sum: 5246 Ratio: 0.07%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 822756 (Eliminated: 0 Frozen: 253444)
|
|
Constraints : 6020448 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
|
|
|
|
Memory Peak : 1005MB
|
|
Max. Length : 105 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 7.74s
|
|
Memory: 914MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 7.82s
|
|
|
|
Iteration 53
|
|
Queue: [(20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)]
|
|
Grounded Until: 105
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 54
|
|
Time : 428.666s (Solving: 401.27s 1st Model: 0.00s Unsat: 2.40s)
|
|
CPU Time : 428.676s
|
|
|
|
Choices : 8438795 (Domain: 8135512)
|
|
Conflicts : 413601 (Analyzed: 413598)
|
|
Restarts : 4950 (Average: 83.56 Last: 185)
|
|
Model-Level : 183.0
|
|
Problems : 54 (Average Length: 72.19 Splits: 0)
|
|
Lemmas : 413598 (Deleted: 382895)
|
|
Binary : 8130 (Ratio: 1.97%)
|
|
Ternary : 3219 (Ratio: 0.78%)
|
|
Conflict : 413598 (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 : 413598 (Average: 18.30 Max: 1374 Sum: 7570763)
|
|
Executed : 413448 (Average: 18.29 Max: 1374 Sum: 7565517 Ratio: 99.93%)
|
|
Bounded : 150 (Average: 34.97 Max: 107 Sum: 5246 Ratio: 0.07%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 822756 (Eliminated: 0 Frozen: 253444)
|
|
Constraints : 6020448 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
|
|
|
|
Memory Peak : 1005MB
|
|
Max. Length : 105 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 7.87s
|
|
Memory: 914MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 7.93s
|
|
|
|
Iteration 54
|
|
Queue: [(21,105,1,True), (22,110,0,True), (23,115,0,True)]
|
|
Grounded Until: 105
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 55
|
|
Time : 440.515s (Solving: 412.95s 1st Model: 0.00s Unsat: 2.40s)
|
|
CPU Time : 440.516s
|
|
|
|
Choices : 9046151 (Domain: 8739101)
|
|
Conflicts : 422005 (Analyzed: 422002)
|
|
Restarts : 5050 (Average: 83.56 Last: 185)
|
|
Model-Level : 183.0
|
|
Problems : 55 (Average Length: 72.82 Splits: 0)
|
|
Lemmas : 422002 (Deleted: 390171)
|
|
Binary : 8341 (Ratio: 1.98%)
|
|
Ternary : 3405 (Ratio: 0.81%)
|
|
Conflict : 422002 (Average Length: 505.8 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 422002 (Average: 19.31 Max: 1374 Sum: 8148974)
|
|
Executed : 421852 (Average: 19.30 Max: 1374 Sum: 8143728 Ratio: 99.94%)
|
|
Bounded : 150 (Average: 34.97 Max: 107 Sum: 5246 Ratio: 0.06%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 822756 (Eliminated: 0 Frozen: 253444)
|
|
Constraints : 6020448 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
|
|
|
|
Memory Peak : 1005MB
|
|
Max. Length : 105 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 11.77s
|
|
Memory: 914MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 11.84s
|
|
|
|
Iteration 55
|
|
Queue: [(22,110,0,True), (23,115,0,True)]
|
|
Grounded Until: 105
|
|
Expected Memory: 1033.0MB
|
|
Grounding... [('step', [106]), ('step', [107]), ('step', [108]), ('step', [109]), ('step', [110]), ('check', [110])]
|
|
Grounding Time: 0.56s
|
|
Memory: 914MB (+0MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 56
|
|
Time : 453.155s (Solving: 424.33s 1st Model: 0.00s Unsat: 2.40s)
|
|
CPU Time : 453.164s
|
|
|
|
Choices : 9387514 (Domain: 9078824)
|
|
Conflicts : 430106 (Analyzed: 430103)
|
|
Restarts : 5150 (Average: 83.52 Last: 185)
|
|
Model-Level : 183.0
|
|
Problems : 56 (Average Length: 73.52 Splits: 0)
|
|
Lemmas : 430103 (Deleted: 397920)
|
|
Binary : 8438 (Ratio: 1.96%)
|
|
Ternary : 3434 (Ratio: 0.80%)
|
|
Conflict : 430103 (Average Length: 503.6 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 430103 (Average: 19.67 Max: 1374 Sum: 8461648)
|
|
Executed : 429953 (Average: 19.66 Max: 1374 Sum: 8456402 Ratio: 99.94%)
|
|
Bounded : 150 (Average: 34.97 Max: 107 Sum: 5246 Ratio: 0.06%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 862832 (Eliminated: 0 Frozen: 265894)
|
|
Constraints : 6322428 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
|
|
|
|
Memory Peak : 1037MB
|
|
Max. Length : 105 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 11.54s
|
|
Memory: 946MB (+32MB)
|
|
UNKNOWN
|
|
Iteration Time: 12.66s
|
|
|
|
Iteration 56
|
|
Queue: [(23,115,0,True)]
|
|
Grounded Until: 110
|
|
Expected Memory: 1065.0MB
|
|
Grounding... [('step', [111]), ('step', [112]), ('step', [113]), ('step', [114]), ('step', [115]), ('check', [115])]
|
|
Grounding Time: 0.56s
|
|
Memory: 946MB (+0MB)
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 57
|
|
Time : 477.954s (Solving: 447.85s 1st Model: 0.00s Unsat: 2.40s)
|
|
CPU Time : 477.940s
|
|
|
|
Choices : 10831659 (Domain: 10511735)
|
|
Conflicts : 440818 (Analyzed: 440815)
|
|
Restarts : 5250 (Average: 83.96 Last: 185)
|
|
Model-Level : 183.0
|
|
Problems : 57 (Average Length: 74.28 Splits: 0)
|
|
Lemmas : 440815 (Deleted: 406854)
|
|
Binary : 9271 (Ratio: 2.10%)
|
|
Ternary : 3822 (Ratio: 0.87%)
|
|
Conflict : 440815 (Average Length: 505.3 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 440815 (Average: 22.35 Max: 1455 Sum: 9854382)
|
|
Executed : 440665 (Average: 22.34 Max: 1455 Sum: 9849136 Ratio: 99.95%)
|
|
Bounded : 150 (Average: 34.97 Max: 107 Sum: 5246 Ratio: 0.05%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 902908 (Eliminated: 0 Frozen: 278344)
|
|
Constraints : 6624408 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
|
|
|
|
Memory Peak : 1071MB
|
|
Max. Length : 110 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 23.66s
|
|
Memory: 975MB (+29MB)
|
|
UNKNOWN
|
|
Iteration Time: 24.79s
|
|
|
|
Iteration 57
|
|
Queue: [(4,20,4,True), (5,25,4,True), (6,30,4,True), (7,35,3,True), (8,40,3,True), (9,45,3,True), (10,50,3,True), (11,55,3,False), (12,60,3,False), (13,65,3,False), (14,70,2,True), (15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,1,True), (23,115,1,True)]
|
|
Grounded Until: 115
|
|
Blocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 58
|
|
Time : 484.554s (Solving: 454.27s 1st Model: 0.00s Unsat: 2.40s)
|
|
CPU Time : 484.544s
|
|
|
|
Choices : 10879063 (Domain: 10559139)
|
|
Conflicts : 448316 (Analyzed: 448313)
|
|
Restarts : 5350 (Average: 83.80 Last: 185)
|
|
Model-Level : 183.0
|
|
Problems : 58 (Average Length: 75.02 Splits: 0)
|
|
Lemmas : 448313 (Deleted: 413945)
|
|
Binary : 9333 (Ratio: 2.08%)
|
|
Ternary : 3831 (Ratio: 0.85%)
|
|
Conflict : 448313 (Average Length: 501.9 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 448313 (Average: 22.07 Max: 1455 Sum: 9895935)
|
|
Executed : 448161 (Average: 22.06 Max: 1455 Sum: 9890455 Ratio: 99.94%)
|
|
Bounded : 152 (Average: 36.05 Max: 117 Sum: 5480 Ratio: 0.06%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 902908 (Eliminated: 0 Frozen: 278344)
|
|
Constraints : 6624408 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
|
|
|
|
Memory Peak : 1071MB
|
|
Max. Length : 115 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 6.54s
|
|
Memory: 975MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 6.61s
|
|
|
|
Iteration 58
|
|
Queue: [(5,25,4,True), (6,30,4,True), (7,35,3,True), (8,40,3,True), (9,45,3,True), (10,50,3,True), (11,55,3,False), (12,60,3,False), (13,65,3,False), (14,70,2,True), (15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,1,True), (23,115,1,True)]
|
|
Grounded Until: 115
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 59
|
|
Time : 490.556s (Solving: 460.05s 1st Model: 0.00s Unsat: 2.40s)
|
|
CPU Time : 490.548s
|
|
|
|
Choices : 10924947 (Domain: 10605023)
|
|
Conflicts : 456079 (Analyzed: 456076)
|
|
Restarts : 5450 (Average: 83.68 Last: 185)
|
|
Model-Level : 183.0
|
|
Problems : 59 (Average Length: 75.73 Splits: 0)
|
|
Lemmas : 456076 (Deleted: 421159)
|
|
Binary : 9367 (Ratio: 2.05%)
|
|
Ternary : 3833 (Ratio: 0.84%)
|
|
Conflict : 456076 (Average Length: 501.1 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 456076 (Average: 21.78 Max: 1455 Sum: 9932435)
|
|
Executed : 455924 (Average: 21.77 Max: 1455 Sum: 9926955 Ratio: 99.94%)
|
|
Bounded : 152 (Average: 36.05 Max: 117 Sum: 5480 Ratio: 0.06%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 902908 (Eliminated: 0 Frozen: 278344)
|
|
Constraints : 6624381 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
|
|
|
|
Memory Peak : 1071MB
|
|
Max. Length : 115 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 5.92s
|
|
Memory: 975MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 6.01s
|
|
|
|
Iteration 59
|
|
Queue: [(6,30,4,True), (7,35,3,True), (8,40,3,True), (9,45,3,True), (10,50,3,True), (11,55,3,False), (12,60,3,False), (13,65,3,False), (14,70,2,True), (15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,1,True), (23,115,1,True)]
|
|
Grounded Until: 115
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 60
|
|
Time : 496.094s (Solving: 465.39s 1st Model: 0.00s Unsat: 2.40s)
|
|
CPU Time : 496.088s
|
|
|
|
Choices : 10986705 (Domain: 10665581)
|
|
Conflicts : 463289 (Analyzed: 463286)
|
|
Restarts : 5550 (Average: 83.47 Last: 185)
|
|
Model-Level : 183.0
|
|
Problems : 60 (Average Length: 76.42 Splits: 0)
|
|
Lemmas : 463286 (Deleted: 428631)
|
|
Binary : 9475 (Ratio: 2.05%)
|
|
Ternary : 3846 (Ratio: 0.83%)
|
|
Conflict : 463286 (Average Length: 499.3 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 463286 (Average: 21.55 Max: 1455 Sum: 9982573)
|
|
Executed : 463134 (Average: 21.54 Max: 1455 Sum: 9977093 Ratio: 99.95%)
|
|
Bounded : 152 (Average: 36.05 Max: 117 Sum: 5480 Ratio: 0.05%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 902908 (Eliminated: 0 Frozen: 278344)
|
|
Constraints : 6624381 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
|
|
|
|
Memory Peak : 1071MB
|
|
Max. Length : 115 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 5.47s
|
|
Memory: 975MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 5.54s
|
|
|
|
Iteration 60
|
|
Queue: [(7,35,3,True), (8,40,3,True), (9,45,3,True), (10,50,3,True), (11,55,3,False), (12,60,3,False), (13,65,3,False), (14,70,2,True), (15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,1,True), (23,115,1,True)]
|
|
Grounded Until: 115
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 61
|
|
Time : 501.089s (Solving: 470.18s 1st Model: 0.00s Unsat: 2.40s)
|
|
CPU Time : 501.084s
|
|
|
|
Choices : 11030102 (Domain: 10708956)
|
|
Conflicts : 470556 (Analyzed: 470553)
|
|
Restarts : 5650 (Average: 83.28 Last: 185)
|
|
Model-Level : 183.0
|
|
Problems : 61 (Average Length: 77.08 Splits: 0)
|
|
Lemmas : 470553 (Deleted: 435488)
|
|
Binary : 9548 (Ratio: 2.03%)
|
|
Ternary : 3868 (Ratio: 0.82%)
|
|
Conflict : 470553 (Average Length: 497.0 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 470553 (Average: 21.29 Max: 1455 Sum: 10017916)
|
|
Executed : 470400 (Average: 21.28 Max: 1455 Sum: 10012323 Ratio: 99.94%)
|
|
Bounded : 153 (Average: 36.56 Max: 117 Sum: 5593 Ratio: 0.06%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 902908 (Eliminated: 0 Frozen: 278344)
|
|
Constraints : 6624381 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
|
|
|
|
Memory Peak : 1071MB
|
|
Max. Length : 115 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 4.92s
|
|
Memory: 975MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 5.00s
|
|
|
|
Iteration 61
|
|
Queue: [(8,40,3,True), (9,45,3,True), (10,50,3,True), (11,55,3,False), (12,60,3,False), (13,65,3,False), (14,70,2,True), (15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,1,True), (23,115,1,True)]
|
|
Grounded Until: 115
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 62
|
|
Time : 514.305s (Solving: 483.22s 1st Model: 0.00s Unsat: 2.40s)
|
|
CPU Time : 514.304s
|
|
|
|
Choices : 11142025 (Domain: 10817712)
|
|
Conflicts : 479227 (Analyzed: 479224)
|
|
Restarts : 5750 (Average: 83.34 Last: 185)
|
|
Model-Level : 183.0
|
|
Problems : 62 (Average Length: 77.73 Splits: 0)
|
|
Lemmas : 479224 (Deleted: 444388)
|
|
Binary : 9753 (Ratio: 2.04%)
|
|
Ternary : 3905 (Ratio: 0.81%)
|
|
Conflict : 479224 (Average Length: 509.2 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 479224 (Average: 21.08 Max: 1455 Sum: 10102920)
|
|
Executed : 479071 (Average: 21.07 Max: 1455 Sum: 10097327 Ratio: 99.94%)
|
|
Bounded : 153 (Average: 36.56 Max: 117 Sum: 5593 Ratio: 0.06%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 902908 (Eliminated: 0 Frozen: 278344)
|
|
Constraints : 6624381 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
|
|
|
|
Memory Peak : 1071MB
|
|
Max. Length : 115 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 13.16s
|
|
Memory: 975MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 13.22s
|
|
|
|
Iteration 62
|
|
Queue: [(9,45,3,True), (10,50,3,True), (11,55,3,False), (12,60,3,False), (13,65,3,False), (14,70,2,True), (15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,1,True), (23,115,1,True)]
|
|
Grounded Until: 115
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 63
|
|
Time : 521.554s (Solving: 490.28s 1st Model: 0.00s Unsat: 2.40s)
|
|
CPU Time : 521.548s
|
|
|
|
Choices : 11217424 (Domain: 10892754)
|
|
Conflicts : 486729 (Analyzed: 486726)
|
|
Restarts : 5850 (Average: 83.20 Last: 185)
|
|
Model-Level : 183.0
|
|
Problems : 63 (Average Length: 78.35 Splits: 0)
|
|
Lemmas : 486726 (Deleted: 450665)
|
|
Binary : 9882 (Ratio: 2.03%)
|
|
Ternary : 3947 (Ratio: 0.81%)
|
|
Conflict : 486726 (Average Length: 506.9 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 486726 (Average: 20.89 Max: 1455 Sum: 10166930)
|
|
Executed : 486569 (Average: 20.88 Max: 1455 Sum: 10160874 Ratio: 99.94%)
|
|
Bounded : 157 (Average: 38.57 Max: 117 Sum: 6056 Ratio: 0.06%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 902908 (Eliminated: 0 Frozen: 278344)
|
|
Constraints : 6624381 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
|
|
|
|
Memory Peak : 1071MB
|
|
Max. Length : 115 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 7.18s
|
|
Memory: 975MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 7.25s
|
|
|
|
Iteration 63
|
|
Queue: [(10,50,3,True), (11,55,3,False), (12,60,3,False), (13,65,3,False), (14,70,2,True), (15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,1,True), (23,115,1,True)]
|
|
Grounded Until: 115
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 64
|
|
Time : 532.779s (Solving: 501.29s 1st Model: 0.00s Unsat: 2.40s)
|
|
CPU Time : 532.780s
|
|
|
|
Choices : 11414476 (Domain: 11087229)
|
|
Conflicts : 495018 (Analyzed: 495015)
|
|
Restarts : 5950 (Average: 83.20 Last: 185)
|
|
Model-Level : 183.0
|
|
Problems : 64 (Average Length: 78.95 Splits: 0)
|
|
Lemmas : 495015 (Deleted: 457334)
|
|
Binary : 10090 (Ratio: 2.04%)
|
|
Ternary : 4014 (Ratio: 0.81%)
|
|
Conflict : 495015 (Average Length: 511.1 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 495015 (Average: 20.89 Max: 1455 Sum: 10341849)
|
|
Executed : 494858 (Average: 20.88 Max: 1455 Sum: 10335793 Ratio: 99.94%)
|
|
Bounded : 157 (Average: 38.57 Max: 117 Sum: 6056 Ratio: 0.06%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 902908 (Eliminated: 0 Frozen: 278344)
|
|
Constraints : 6624341 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
|
|
|
|
Memory Peak : 1071MB
|
|
Max. Length : 115 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 11.14s
|
|
Memory: 975MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 11.23s
|
|
|
|
Iteration 64
|
|
Queue: [(14,70,2,True), (15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,1,True), (23,115,1,True)]
|
|
Grounded Until: 115
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 65
|
|
Time : 544.248s (Solving: 512.57s 1st Model: 0.00s Unsat: 2.40s)
|
|
CPU Time : 544.256s
|
|
|
|
Choices : 11668016 (Domain: 11339143)
|
|
Conflicts : 503596 (Analyzed: 503593)
|
|
Restarts : 6050 (Average: 83.24 Last: 185)
|
|
Model-Level : 183.0
|
|
Problems : 65 (Average Length: 79.54 Splits: 0)
|
|
Lemmas : 503593 (Deleted: 465102)
|
|
Binary : 10213 (Ratio: 2.03%)
|
|
Ternary : 4053 (Ratio: 0.80%)
|
|
Conflict : 503593 (Average Length: 512.5 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 503593 (Average: 20.99 Max: 1455 Sum: 10572702)
|
|
Executed : 503436 (Average: 20.98 Max: 1455 Sum: 10566646 Ratio: 99.94%)
|
|
Bounded : 157 (Average: 38.57 Max: 117 Sum: 6056 Ratio: 0.06%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 902908 (Eliminated: 0 Frozen: 278344)
|
|
Constraints : 6624341 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
|
|
|
|
Memory Peak : 1071MB
|
|
Max. Length : 115 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 11.41s
|
|
Memory: 975MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 11.48s
|
|
|
|
Iteration 65
|
|
Queue: [(15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,1,True), (23,115,1,True)]
|
|
Grounded Until: 115
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 66
|
|
Time : 555.128s (Solving: 523.24s 1st Model: 0.00s Unsat: 2.40s)
|
|
CPU Time : 555.144s
|
|
|
|
Choices : 11937161 (Domain: 11606955)
|
|
Conflicts : 512151 (Analyzed: 512148)
|
|
Restarts : 6150 (Average: 83.28 Last: 185)
|
|
Model-Level : 183.0
|
|
Problems : 66 (Average Length: 80.11 Splits: 0)
|
|
Lemmas : 512148 (Deleted: 473103)
|
|
Binary : 10319 (Ratio: 2.01%)
|
|
Ternary : 4077 (Ratio: 0.80%)
|
|
Conflict : 512148 (Average Length: 514.2 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 512148 (Average: 21.12 Max: 1455 Sum: 10816985)
|
|
Executed : 511991 (Average: 21.11 Max: 1455 Sum: 10810929 Ratio: 99.94%)
|
|
Bounded : 157 (Average: 38.57 Max: 117 Sum: 6056 Ratio: 0.06%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 902908 (Eliminated: 0 Frozen: 278344)
|
|
Constraints : 6624341 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
|
|
|
|
Memory Peak : 1071MB
|
|
Max. Length : 115 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 10.80s
|
|
Memory: 975MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 10.89s
|
|
|
|
Iteration 66
|
|
Queue: [(22,110,1,True), (23,115,1,True)]
|
|
Grounded Until: 115
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 67
|
|
Time : 565.666s (Solving: 533.58s 1st Model: 0.00s Unsat: 2.40s)
|
|
CPU Time : 565.688s
|
|
|
|
Choices : 12317914 (Domain: 11986494)
|
|
Conflicts : 520221 (Analyzed: 520218)
|
|
Restarts : 6250 (Average: 83.23 Last: 185)
|
|
Model-Level : 183.0
|
|
Problems : 67 (Average Length: 80.66 Splits: 0)
|
|
Lemmas : 520218 (Deleted: 481326)
|
|
Binary : 10396 (Ratio: 2.00%)
|
|
Ternary : 4130 (Ratio: 0.79%)
|
|
Conflict : 520218 (Average Length: 517.9 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 520218 (Average: 21.47 Max: 1455 Sum: 11168194)
|
|
Executed : 520061 (Average: 21.46 Max: 1455 Sum: 11162138 Ratio: 99.95%)
|
|
Bounded : 157 (Average: 38.57 Max: 117 Sum: 6056 Ratio: 0.05%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 902908 (Eliminated: 0 Frozen: 278344)
|
|
Constraints : 6624341 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
|
|
|
|
Memory Peak : 1071MB
|
|
Max. Length : 115 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 10.47s
|
|
Memory: 975MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 10.55s
|
|
|
|
Iteration 67
|
|
Queue: [(23,115,1,True)]
|
|
Grounded Until: 115
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 68
|
|
Time : 582.335s (Solving: 550.02s 1st Model: 0.00s Unsat: 2.40s)
|
|
CPU Time : 582.364s
|
|
|
|
Choices : 13088569 (Domain: 12752469)
|
|
Conflicts : 528948 (Analyzed: 528945)
|
|
Restarts : 6350 (Average: 83.30 Last: 185)
|
|
Model-Level : 183.0
|
|
Problems : 68 (Average Length: 81.19 Splits: 0)
|
|
Lemmas : 528945 (Deleted: 490920)
|
|
Binary : 10750 (Ratio: 2.03%)
|
|
Ternary : 4323 (Ratio: 0.82%)
|
|
Conflict : 528945 (Average Length: 519.5 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 528945 (Average: 22.49 Max: 1562 Sum: 11896548)
|
|
Executed : 528788 (Average: 22.48 Max: 1562 Sum: 11890492 Ratio: 99.95%)
|
|
Bounded : 157 (Average: 38.57 Max: 117 Sum: 6056 Ratio: 0.05%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 902908 (Eliminated: 0 Frozen: 278344)
|
|
Constraints : 6624341 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
|
|
|
|
Memory Peak : 1071MB
|
|
Max. Length : 115 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 16.59s
|
|
Memory: 975MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 16.68s
|
|
|
|
Iteration 68
|
|
Queue: [(4,20,5,True), (5,25,5,True), (6,30,5,True), (7,35,4,True), (8,40,4,True), (9,45,4,True), (10,50,4,False), (11,55,3,True), (12,60,3,True), (13,65,3,False), (14,70,3,False), (15,75,3,False), (16,80,2,True), (17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
|
|
Grounded Until: 115
|
|
Blocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 69
|
|
Time : 588.065s (Solving: 555.53s 1st Model: 0.00s Unsat: 2.40s)
|
|
CPU Time : 588.088s
|
|
|
|
Choices : 13146278 (Domain: 12810178)
|
|
Conflicts : 536554 (Analyzed: 536551)
|
|
Restarts : 6450 (Average: 83.19 Last: 185)
|
|
Model-Level : 183.0
|
|
Problems : 69 (Average Length: 81.71 Splits: 0)
|
|
Lemmas : 536551 (Deleted: 496486)
|
|
Binary : 10836 (Ratio: 2.02%)
|
|
Ternary : 4334 (Ratio: 0.81%)
|
|
Conflict : 536551 (Average Length: 518.2 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 536551 (Average: 22.27 Max: 1562 Sum: 11946514)
|
|
Executed : 536393 (Average: 22.25 Max: 1562 Sum: 11940342 Ratio: 99.95%)
|
|
Bounded : 158 (Average: 39.06 Max: 117 Sum: 6172 Ratio: 0.05%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 902908 (Eliminated: 0 Frozen: 278344)
|
|
Constraints : 6624341 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
|
|
|
|
Memory Peak : 1071MB
|
|
Max. Length : 115 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 5.64s
|
|
Memory: 975MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 5.73s
|
|
|
|
Iteration 69
|
|
Queue: [(5,25,5,True), (6,30,5,True), (7,35,4,True), (8,40,4,True), (9,45,4,True), (10,50,4,False), (11,55,3,True), (12,60,3,True), (13,65,3,False), (14,70,3,False), (15,75,3,False), (16,80,2,True), (17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
|
|
Grounded Until: 115
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 70
|
|
Time : 592.454s (Solving: 559.74s 1st Model: 0.00s Unsat: 2.40s)
|
|
CPU Time : 592.476s
|
|
|
|
Choices : 13186477 (Domain: 12850377)
|
|
Conflicts : 544160 (Analyzed: 544157)
|
|
Restarts : 6550 (Average: 83.08 Last: 185)
|
|
Model-Level : 183.0
|
|
Problems : 70 (Average Length: 82.21 Splits: 0)
|
|
Lemmas : 544157 (Deleted: 503845)
|
|
Binary : 10858 (Ratio: 2.00%)
|
|
Ternary : 4336 (Ratio: 0.80%)
|
|
Conflict : 544157 (Average Length: 517.4 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 544157 (Average: 22.01 Max: 1562 Sum: 11978079)
|
|
Executed : 543999 (Average: 22.00 Max: 1562 Sum: 11971907 Ratio: 99.95%)
|
|
Bounded : 158 (Average: 39.06 Max: 117 Sum: 6172 Ratio: 0.05%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 902908 (Eliminated: 0 Frozen: 278344)
|
|
Constraints : 6624341 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
|
|
|
|
Memory Peak : 1071MB
|
|
Max. Length : 115 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 4.33s
|
|
Memory: 975MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 4.39s
|
|
|
|
Iteration 70
|
|
Queue: [(6,30,5,True), (7,35,4,True), (8,40,4,True), (9,45,4,True), (10,50,4,False), (11,55,3,True), (12,60,3,True), (13,65,3,False), (14,70,3,False), (15,75,3,False), (16,80,2,True), (17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
|
|
Grounded Until: 115
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 71
|
|
Time : 600.560s (Solving: 567.65s 1st Model: 0.00s Unsat: 2.40s)
|
|
CPU Time : 600.584s
|
|
|
|
Choices : 13260918 (Domain: 12920098)
|
|
Conflicts : 552886 (Analyzed: 552883)
|
|
Restarts : 6650 (Average: 83.14 Last: 185)
|
|
Model-Level : 183.0
|
|
Problems : 71 (Average Length: 82.70 Splits: 0)
|
|
Lemmas : 552883 (Deleted: 513368)
|
|
Binary : 10965 (Ratio: 1.98%)
|
|
Ternary : 4358 (Ratio: 0.79%)
|
|
Conflict : 552883 (Average Length: 520.9 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 552883 (Average: 21.77 Max: 1562 Sum: 12034743)
|
|
Executed : 552725 (Average: 21.76 Max: 1562 Sum: 12028571 Ratio: 99.95%)
|
|
Bounded : 158 (Average: 39.06 Max: 117 Sum: 6172 Ratio: 0.05%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 902908 (Eliminated: 0 Frozen: 278344)
|
|
Constraints : 6624341 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
|
|
|
|
Memory Peak : 1071MB
|
|
Max. Length : 115 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 8.04s
|
|
Memory: 975MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 8.11s
|
|
|
|
Iteration 71
|
|
Queue: [(7,35,4,True), (8,40,4,True), (9,45,4,True), (10,50,4,False), (11,55,3,True), (12,60,3,True), (13,65,3,False), (14,70,3,False), (15,75,3,False), (16,80,2,True), (17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
|
|
Grounded Until: 115
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 72
|
|
Time : 605.272s (Solving: 572.15s 1st Model: 0.00s Unsat: 2.40s)
|
|
CPU Time : 605.296s
|
|
|
|
Choices : 13317430 (Domain: 12975523)
|
|
Conflicts : 560480 (Analyzed: 560477)
|
|
Restarts : 6750 (Average: 83.03 Last: 185)
|
|
Model-Level : 183.0
|
|
Problems : 72 (Average Length: 83.18 Splits: 0)
|
|
Lemmas : 560477 (Deleted: 519465)
|
|
Binary : 11030 (Ratio: 1.97%)
|
|
Ternary : 4396 (Ratio: 0.78%)
|
|
Conflict : 560477 (Average Length: 517.7 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 560477 (Average: 21.55 Max: 1562 Sum: 12080644)
|
|
Executed : 560319 (Average: 21.54 Max: 1562 Sum: 12074472 Ratio: 99.95%)
|
|
Bounded : 158 (Average: 39.06 Max: 117 Sum: 6172 Ratio: 0.05%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 902908 (Eliminated: 0 Frozen: 278344)
|
|
Constraints : 6624341 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
|
|
|
|
Memory Peak : 1071MB
|
|
Max. Length : 115 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 4.63s
|
|
Memory: 975MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 4.72s
|
|
|
|
Iteration 72
|
|
Queue: [(8,40,4,True), (9,45,4,True), (10,50,4,False), (11,55,3,True), (12,60,3,True), (13,65,3,False), (14,70,3,False), (15,75,3,False), (16,80,2,True), (17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
|
|
Grounded Until: 115
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 73
|
|
Time : 612.491s (Solving: 579.19s 1st Model: 0.00s Unsat: 2.40s)
|
|
CPU Time : 612.516s
|
|
|
|
Choices : 13399866 (Domain: 13057114)
|
|
Conflicts : 568275 (Analyzed: 568272)
|
|
Restarts : 6850 (Average: 82.96 Last: 185)
|
|
Model-Level : 183.0
|
|
Problems : 73 (Average Length: 83.64 Splits: 0)
|
|
Lemmas : 568272 (Deleted: 526626)
|
|
Binary : 11227 (Ratio: 1.98%)
|
|
Ternary : 4486 (Ratio: 0.79%)
|
|
Conflict : 568272 (Average Length: 517.5 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 568272 (Average: 21.38 Max: 1562 Sum: 12150356)
|
|
Executed : 568113 (Average: 21.37 Max: 1562 Sum: 12144071 Ratio: 99.95%)
|
|
Bounded : 159 (Average: 39.53 Max: 117 Sum: 6285 Ratio: 0.05%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 902908 (Eliminated: 0 Frozen: 278344)
|
|
Constraints : 6624341 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
|
|
|
|
Memory Peak : 1071MB
|
|
Max. Length : 115 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 7.16s
|
|
Memory: 975MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 7.23s
|
|
|
|
Iteration 73
|
|
Queue: [(9,45,4,True), (10,50,4,False), (11,55,3,True), (12,60,3,True), (13,65,3,False), (14,70,3,False), (15,75,3,False), (16,80,2,True), (17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
|
|
Grounded Until: 115
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 74
|
|
Time : 624.730s (Solving: 591.24s 1st Model: 0.00s Unsat: 2.40s)
|
|
CPU Time : 624.756s
|
|
|
|
Choices : 13550436 (Domain: 13206308)
|
|
Conflicts : 576763 (Analyzed: 576760)
|
|
Restarts : 6950 (Average: 82.99 Last: 185)
|
|
Model-Level : 183.0
|
|
Problems : 74 (Average Length: 84.09 Splits: 0)
|
|
Lemmas : 576760 (Deleted: 533795)
|
|
Binary : 11402 (Ratio: 1.98%)
|
|
Ternary : 4562 (Ratio: 0.79%)
|
|
Conflict : 576760 (Average Length: 523.7 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 576760 (Average: 21.29 Max: 1562 Sum: 12278204)
|
|
Executed : 576601 (Average: 21.28 Max: 1562 Sum: 12271919 Ratio: 99.95%)
|
|
Bounded : 159 (Average: 39.53 Max: 117 Sum: 6285 Ratio: 0.05%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 902908 (Eliminated: 0 Frozen: 278344)
|
|
Constraints : 6624341 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
|
|
|
|
Memory Peak : 1071MB
|
|
Max. Length : 115 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 12.17s
|
|
Memory: 975MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 12.24s
|
|
|
|
Iteration 74
|
|
Queue: [(11,55,3,True), (12,60,3,True), (13,65,3,False), (14,70,3,False), (15,75,3,False), (16,80,2,True), (17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
|
|
Grounded Until: 115
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 75
|
|
Time : 639.378s (Solving: 605.69s 1st Model: 0.00s Unsat: 2.40s)
|
|
CPU Time : 639.408s
|
|
|
|
Choices : 13754428 (Domain: 13408461)
|
|
Conflicts : 585767 (Analyzed: 585764)
|
|
Restarts : 7050 (Average: 83.09 Last: 185)
|
|
Model-Level : 183.0
|
|
Problems : 75 (Average Length: 84.53 Splits: 0)
|
|
Lemmas : 585764 (Deleted: 543773)
|
|
Binary : 11646 (Ratio: 1.99%)
|
|
Ternary : 4656 (Ratio: 0.79%)
|
|
Conflict : 585764 (Average Length: 531.8 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 585764 (Average: 21.26 Max: 1562 Sum: 12452649)
|
|
Executed : 585605 (Average: 21.25 Max: 1562 Sum: 12446364 Ratio: 99.95%)
|
|
Bounded : 159 (Average: 39.53 Max: 117 Sum: 6285 Ratio: 0.05%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 902908 (Eliminated: 0 Frozen: 278344)
|
|
Constraints : 6624341 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
|
|
|
|
Memory Peak : 1071MB
|
|
Max. Length : 115 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 14.58s
|
|
Memory: 975MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 14.66s
|
|
|
|
Iteration 75
|
|
Queue: [(12,60,3,True), (13,65,3,False), (14,70,3,False), (15,75,3,False), (16,80,2,True), (17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
|
|
Grounded Until: 115
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 76
|
|
Time : 653.162s (Solving: 619.29s 1st Model: 0.00s Unsat: 2.40s)
|
|
CPU Time : 653.196s
|
|
|
|
Choices : 13957281 (Domain: 13609805)
|
|
Conflicts : 594135 (Analyzed: 594132)
|
|
Restarts : 7150 (Average: 83.10 Last: 185)
|
|
Model-Level : 183.0
|
|
Problems : 76 (Average Length: 84.96 Splits: 0)
|
|
Lemmas : 594132 (Deleted: 550302)
|
|
Binary : 11820 (Ratio: 1.99%)
|
|
Ternary : 4704 (Ratio: 0.79%)
|
|
Conflict : 594132 (Average Length: 541.1 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 594132 (Average: 21.25 Max: 1562 Sum: 12625961)
|
|
Executed : 593973 (Average: 21.24 Max: 1562 Sum: 12619676 Ratio: 99.95%)
|
|
Bounded : 159 (Average: 39.53 Max: 117 Sum: 6285 Ratio: 0.05%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 902908 (Eliminated: 0 Frozen: 278344)
|
|
Constraints : 6624341 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
|
|
|
|
Memory Peak : 1071MB
|
|
Max. Length : 115 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 13.73s
|
|
Memory: 975MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 13.79s
|
|
|
|
Iteration 76
|
|
Queue: [(16,80,2,True), (17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
|
|
Grounded Until: 115
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 77
|
|
Time : 667.620s (Solving: 633.54s 1st Model: 0.00s Unsat: 2.40s)
|
|
CPU Time : 667.660s
|
|
|
|
Choices : 14229081 (Domain: 13878957)
|
|
Conflicts : 602414 (Analyzed: 602411)
|
|
Restarts : 7250 (Average: 83.09 Last: 185)
|
|
Model-Level : 183.0
|
|
Problems : 77 (Average Length: 85.38 Splits: 0)
|
|
Lemmas : 602411 (Deleted: 558174)
|
|
Binary : 12049 (Ratio: 2.00%)
|
|
Ternary : 4758 (Ratio: 0.79%)
|
|
Conflict : 602411 (Average Length: 551.5 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 602411 (Average: 21.36 Max: 1562 Sum: 12866776)
|
|
Executed : 602252 (Average: 21.35 Max: 1562 Sum: 12860491 Ratio: 99.95%)
|
|
Bounded : 159 (Average: 39.53 Max: 117 Sum: 6285 Ratio: 0.05%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 902908 (Eliminated: 0 Frozen: 278344)
|
|
Constraints : 6624341 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
|
|
|
|
Memory Peak : 1071MB
|
|
Max. Length : 115 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 14.38s
|
|
Memory: 975MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 14.47s
|
|
|
|
Iteration 77
|
|
Queue: [(17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
|
|
Grounded Until: 115
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 78
|
|
Time : 688.445s (Solving: 654.18s 1st Model: 0.00s Unsat: 2.40s)
|
|
CPU Time : 688.492s
|
|
|
|
Choices : 14711711 (Domain: 14353351)
|
|
Conflicts : 611580 (Analyzed: 611577)
|
|
Restarts : 7350 (Average: 83.21 Last: 185)
|
|
Model-Level : 183.0
|
|
Problems : 78 (Average Length: 85.78 Splits: 0)
|
|
Lemmas : 611577 (Deleted: 567670)
|
|
Binary : 12557 (Ratio: 2.05%)
|
|
Ternary : 4895 (Ratio: 0.80%)
|
|
Conflict : 611577 (Average Length: 564.1 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 611577 (Average: 21.74 Max: 1562 Sum: 13295201)
|
|
Executed : 611418 (Average: 21.73 Max: 1562 Sum: 13288916 Ratio: 99.95%)
|
|
Bounded : 159 (Average: 39.53 Max: 117 Sum: 6285 Ratio: 0.05%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 902908 (Eliminated: 0 Frozen: 278344)
|
|
Constraints : 6624341 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
|
|
|
|
Memory Peak : 1071MB
|
|
Max. Length : 115 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 20.77s
|
|
Memory: 975MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 20.84s
|
|
|
|
Iteration 78
|
|
Queue: [(4,20,6,True), (5,25,6,True), (6,30,6,True), (7,35,5,True), (8,40,5,True), (9,45,5,False), (10,50,4,True), (11,55,4,False), (12,60,4,False), (13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,3,False), (17,85,3,False), (18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
|
|
Grounded Until: 115
|
|
Blocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 79
|
|
Time : 694.262s (Solving: 659.80s 1st Model: 0.00s Unsat: 2.40s)
|
|
CPU Time : 694.312s
|
|
|
|
Choices : 14768725 (Domain: 14410365)
|
|
Conflicts : 620106 (Analyzed: 620103)
|
|
Restarts : 7450 (Average: 83.24 Last: 185)
|
|
Model-Level : 183.0
|
|
Problems : 79 (Average Length: 86.18 Splits: 0)
|
|
Lemmas : 620103 (Deleted: 574044)
|
|
Binary : 12611 (Ratio: 2.03%)
|
|
Ternary : 4906 (Ratio: 0.79%)
|
|
Conflict : 620103 (Average Length: 561.7 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 620103 (Average: 21.52 Max: 1562 Sum: 13342839)
|
|
Executed : 619944 (Average: 21.51 Max: 1562 Sum: 13336554 Ratio: 99.95%)
|
|
Bounded : 159 (Average: 39.53 Max: 117 Sum: 6285 Ratio: 0.05%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 902908 (Eliminated: 0 Frozen: 278344)
|
|
Constraints : 6624341 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
|
|
|
|
Memory Peak : 1071MB
|
|
Max. Length : 115 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 5.75s
|
|
Memory: 975MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 5.82s
|
|
|
|
Iteration 79
|
|
Queue: [(5,25,6,True), (6,30,6,True), (7,35,5,True), (8,40,5,True), (9,45,5,False), (10,50,4,True), (11,55,4,False), (12,60,4,False), (13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,3,False), (17,85,3,False), (18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
|
|
Grounded Until: 115
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 80
|
|
Time : 697.964s (Solving: 663.32s 1st Model: 0.00s Unsat: 2.40s)
|
|
CPU Time : 698.016s
|
|
|
|
Choices : 14803436 (Domain: 14445076)
|
|
Conflicts : 627340 (Analyzed: 627337)
|
|
Restarts : 7550 (Average: 83.09 Last: 185)
|
|
Model-Level : 183.0
|
|
Problems : 80 (Average Length: 86.56 Splits: 0)
|
|
Lemmas : 627337 (Deleted: 582303)
|
|
Binary : 12618 (Ratio: 2.01%)
|
|
Ternary : 4907 (Ratio: 0.78%)
|
|
Conflict : 627337 (Average Length: 561.4 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 627337 (Average: 21.31 Max: 1562 Sum: 13368084)
|
|
Executed : 627177 (Average: 21.30 Max: 1562 Sum: 13361682 Ratio: 99.95%)
|
|
Bounded : 160 (Average: 40.01 Max: 117 Sum: 6402 Ratio: 0.05%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 902908 (Eliminated: 0 Frozen: 278344)
|
|
Constraints : 6624341 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
|
|
|
|
Memory Peak : 1071MB
|
|
Max. Length : 115 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 3.64s
|
|
Memory: 975MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 3.71s
|
|
|
|
Iteration 80
|
|
Queue: [(6,30,6,True), (7,35,5,True), (8,40,5,True), (9,45,5,False), (10,50,4,True), (11,55,4,False), (12,60,4,False), (13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,3,False), (17,85,3,False), (18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
|
|
Grounded Until: 115
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 81
|
|
Time : 705.316s (Solving: 670.46s 1st Model: 0.00s Unsat: 2.40s)
|
|
CPU Time : 705.372s
|
|
|
|
Choices : 14876037 (Domain: 14517677)
|
|
Conflicts : 635476 (Analyzed: 635473)
|
|
Restarts : 7650 (Average: 83.07 Last: 185)
|
|
Model-Level : 183.0
|
|
Problems : 81 (Average Length: 86.94 Splits: 0)
|
|
Lemmas : 635473 (Deleted: 589436)
|
|
Binary : 12660 (Ratio: 1.99%)
|
|
Ternary : 4927 (Ratio: 0.78%)
|
|
Conflict : 635473 (Average Length: 561.9 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 635473 (Average: 21.13 Max: 1562 Sum: 13427038)
|
|
Executed : 635312 (Average: 21.12 Max: 1562 Sum: 13420519 Ratio: 99.95%)
|
|
Bounded : 161 (Average: 40.49 Max: 117 Sum: 6519 Ratio: 0.05%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 902908 (Eliminated: 0 Frozen: 278344)
|
|
Constraints : 6624315 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
|
|
|
|
Memory Peak : 1071MB
|
|
Max. Length : 115 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 7.27s
|
|
Memory: 975MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 7.36s
|
|
|
|
Iteration 81
|
|
Queue: [(7,35,5,True), (8,40,5,True), (9,45,5,False), (10,50,4,True), (11,55,4,False), (12,60,4,False), (13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,3,False), (17,85,3,False), (18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
|
|
Grounded Until: 115
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 82
|
|
Time : 714.196s (Solving: 679.16s 1st Model: 0.00s Unsat: 2.40s)
|
|
CPU Time : 714.240s
|
|
|
|
Choices : 14964621 (Domain: 14606225)
|
|
Conflicts : 644276 (Analyzed: 644273)
|
|
Restarts : 7750 (Average: 83.13 Last: 185)
|
|
Model-Level : 183.0
|
|
Problems : 82 (Average Length: 87.30 Splits: 0)
|
|
Lemmas : 644273 (Deleted: 598824)
|
|
Binary : 12774 (Ratio: 1.98%)
|
|
Ternary : 4948 (Ratio: 0.77%)
|
|
Conflict : 644273 (Average Length: 560.8 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 644273 (Average: 20.95 Max: 1562 Sum: 13499468)
|
|
Executed : 644112 (Average: 20.94 Max: 1562 Sum: 13492949 Ratio: 99.95%)
|
|
Bounded : 161 (Average: 40.49 Max: 117 Sum: 6519 Ratio: 0.05%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 902908 (Eliminated: 0 Frozen: 278344)
|
|
Constraints : 6624301 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
|
|
|
|
Memory Peak : 1071MB
|
|
Max. Length : 115 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 8.80s
|
|
Memory: 975MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 8.87s
|
|
|
|
Iteration 82
|
|
Queue: [(8,40,5,True), (9,45,5,False), (10,50,4,True), (11,55,4,False), (12,60,4,False), (13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,3,False), (17,85,3,False), (18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
|
|
Grounded Until: 115
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 83
|
|
Time : 721.282s (Solving: 686.07s 1st Model: 0.00s Unsat: 2.40s)
|
|
CPU Time : 721.328s
|
|
|
|
Choices : 15037395 (Domain: 14677670)
|
|
Conflicts : 652050 (Analyzed: 652047)
|
|
Restarts : 7850 (Average: 83.06 Last: 185)
|
|
Model-Level : 183.0
|
|
Problems : 83 (Average Length: 87.66 Splits: 0)
|
|
Lemmas : 652047 (Deleted: 605184)
|
|
Binary : 12879 (Ratio: 1.98%)
|
|
Ternary : 4985 (Ratio: 0.76%)
|
|
Conflict : 652047 (Average Length: 564.4 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 652047 (Average: 20.79 Max: 1562 Sum: 13555664)
|
|
Executed : 651885 (Average: 20.78 Max: 1562 Sum: 13549032 Ratio: 99.95%)
|
|
Bounded : 162 (Average: 40.94 Max: 117 Sum: 6632 Ratio: 0.05%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 902908 (Eliminated: 0 Frozen: 278344)
|
|
Constraints : 6624301 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
|
|
|
|
Memory Peak : 1071MB
|
|
Max. Length : 115 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 7.03s
|
|
Memory: 975MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 7.09s
|
|
|
|
Iteration 83
|
|
Queue: [(10,50,4,True), (11,55,4,False), (12,60,4,False), (13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,3,False), (17,85,3,False), (18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
|
|
Grounded Until: 115
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 84
|
|
Time : 735.705s (Solving: 700.30s 1st Model: 0.00s Unsat: 2.40s)
|
|
CPU Time : 735.756s
|
|
|
|
Choices : 15211825 (Domain: 14851226)
|
|
Conflicts : 660424 (Analyzed: 660421)
|
|
Restarts : 7950 (Average: 83.07 Last: 185)
|
|
Model-Level : 183.0
|
|
Problems : 84 (Average Length: 88.01 Splits: 0)
|
|
Lemmas : 660421 (Deleted: 612860)
|
|
Binary : 13052 (Ratio: 1.98%)
|
|
Ternary : 5021 (Ratio: 0.76%)
|
|
Conflict : 660421 (Average Length: 574.6 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 660421 (Average: 20.75 Max: 1562 Sum: 13701359)
|
|
Executed : 660259 (Average: 20.74 Max: 1562 Sum: 13694727 Ratio: 99.95%)
|
|
Bounded : 162 (Average: 40.94 Max: 117 Sum: 6632 Ratio: 0.05%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 902908 (Eliminated: 0 Frozen: 278344)
|
|
Constraints : 6624301 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
|
|
|
|
Memory Peak : 1071MB
|
|
Max. Length : 115 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 14.36s
|
|
Memory: 975MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 14.43s
|
|
|
|
Iteration 84
|
|
Queue: [(13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,3,False), (17,85,3,False), (18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
|
|
Grounded Until: 115
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 85
|
|
Time : 749.084s (Solving: 713.49s 1st Model: 0.00s Unsat: 2.40s)
|
|
CPU Time : 749.124s
|
|
|
|
Choices : 15373876 (Domain: 15012894)
|
|
Conflicts : 668679 (Analyzed: 668676)
|
|
Restarts : 8050 (Average: 83.07 Last: 185)
|
|
Model-Level : 183.0
|
|
Problems : 85 (Average Length: 88.35 Splits: 0)
|
|
Lemmas : 668676 (Deleted: 620912)
|
|
Binary : 13146 (Ratio: 1.97%)
|
|
Ternary : 5041 (Ratio: 0.75%)
|
|
Conflict : 668676 (Average Length: 586.8 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 668676 (Average: 20.69 Max: 1562 Sum: 13833507)
|
|
Executed : 668514 (Average: 20.68 Max: 1562 Sum: 13826875 Ratio: 99.95%)
|
|
Bounded : 162 (Average: 40.94 Max: 117 Sum: 6632 Ratio: 0.05%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 902908 (Eliminated: 0 Frozen: 278344)
|
|
Constraints : 6624301 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
|
|
|
|
Memory Peak : 1071MB
|
|
Max. Length : 115 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 13.30s
|
|
Memory: 975MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 13.37s
|
|
|
|
Iteration 85
|
|
Queue: [(18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
|
|
Grounded Until: 115
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 86
|
|
Time : 763.386s (Solving: 727.61s 1st Model: 0.00s Unsat: 2.40s)
|
|
CPU Time : 763.432s
|
|
|
|
Choices : 15536270 (Domain: 15175157)
|
|
Conflicts : 677036 (Analyzed: 677033)
|
|
Restarts : 8150 (Average: 83.07 Last: 185)
|
|
Model-Level : 183.0
|
|
Problems : 86 (Average Length: 88.69 Splits: 0)
|
|
Lemmas : 677033 (Deleted: 628936)
|
|
Binary : 13199 (Ratio: 1.95%)
|
|
Ternary : 5046 (Ratio: 0.75%)
|
|
Conflict : 677033 (Average Length: 605.8 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 677033 (Average: 20.62 Max: 1562 Sum: 13957955)
|
|
Executed : 676871 (Average: 20.61 Max: 1562 Sum: 13951323 Ratio: 99.95%)
|
|
Bounded : 162 (Average: 40.94 Max: 117 Sum: 6632 Ratio: 0.05%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 902908 (Eliminated: 0 Frozen: 278344)
|
|
Constraints : 6624301 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
|
|
|
|
Memory Peak : 1071MB
|
|
Max. Length : 115 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 14.24s
|
|
Memory: 975MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 14.31s
|
|
|
|
Iteration 86
|
|
Queue: [(4,20,7,True), (5,25,7,True), (6,30,7,False), (7,35,6,True), (8,40,6,False), (9,45,5,True), (10,50,5,False), (11,55,4,True), (12,60,4,False), (13,65,4,False), (14,70,3,True), (15,75,3,True), (16,80,3,False), (17,85,3,False), (18,90,3,False), (19,95,2,True), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
|
|
Grounded Until: 115
|
|
Blocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 87
|
|
Time : 769.775s (Solving: 733.81s 1st Model: 0.00s Unsat: 2.40s)
|
|
CPU Time : 769.828s
|
|
|
|
Choices : 15591549 (Domain: 15230434)
|
|
Conflicts : 684391 (Analyzed: 684388)
|
|
Restarts : 8250 (Average: 82.96 Last: 185)
|
|
Model-Level : 183.0
|
|
Problems : 87 (Average Length: 89.01 Splits: 0)
|
|
Lemmas : 684388 (Deleted: 637148)
|
|
Binary : 13249 (Ratio: 1.94%)
|
|
Ternary : 5048 (Ratio: 0.74%)
|
|
Conflict : 684388 (Average Length: 601.7 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 684388 (Average: 20.44 Max: 1562 Sum: 13987653)
|
|
Executed : 684226 (Average: 20.43 Max: 1562 Sum: 13981021 Ratio: 99.95%)
|
|
Bounded : 162 (Average: 40.94 Max: 117 Sum: 6632 Ratio: 0.05%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 902908 (Eliminated: 0 Frozen: 278344)
|
|
Constraints : 6624301 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
|
|
|
|
Memory Peak : 1071MB
|
|
Max. Length : 115 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 6.32s
|
|
Memory: 975MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 6.40s
|
|
|
|
Iteration 87
|
|
Queue: [(5,25,7,True), (6,30,7,False), (7,35,6,True), (8,40,6,False), (9,45,5,True), (10,50,5,False), (11,55,4,True), (12,60,4,False), (13,65,4,False), (14,70,3,True), (15,75,3,True), (16,80,3,False), (17,85,3,False), (18,90,3,False), (19,95,2,True), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
|
|
Grounded Until: 115
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 88
|
|
Time : 773.674s (Solving: 737.53s 1st Model: 0.00s Unsat: 2.40s)
|
|
CPU Time : 773.728s
|
|
|
|
Choices : 15625291 (Domain: 15264176)
|
|
Conflicts : 691658 (Analyzed: 691655)
|
|
Restarts : 8350 (Average: 82.83 Last: 185)
|
|
Model-Level : 183.0
|
|
Problems : 88 (Average Length: 89.33 Splits: 0)
|
|
Lemmas : 691655 (Deleted: 644095)
|
|
Binary : 13256 (Ratio: 1.92%)
|
|
Ternary : 5049 (Ratio: 0.73%)
|
|
Conflict : 691655 (Average Length: 599.6 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 691655 (Average: 20.26 Max: 1562 Sum: 14012397)
|
|
Executed : 691493 (Average: 20.25 Max: 1562 Sum: 14005765 Ratio: 99.95%)
|
|
Bounded : 162 (Average: 40.94 Max: 117 Sum: 6632 Ratio: 0.05%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 902908 (Eliminated: 0 Frozen: 278344)
|
|
Constraints : 6624301 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
|
|
|
|
Memory Peak : 1071MB
|
|
Max. Length : 115 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 3.84s
|
|
Memory: 975MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 3.90s
|
|
|
|
Iteration 88
|
|
Queue: [(7,35,6,True), (8,40,6,False), (9,45,5,True), (10,50,5,False), (11,55,4,True), (12,60,4,False), (13,65,4,False), (14,70,3,True), (15,75,3,True), (16,80,3,False), (17,85,3,False), (18,90,3,False), (19,95,2,True), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
|
|
Grounded Until: 115
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 89
|
|
Time : 783.702s (Solving: 747.38s 1st Model: 0.00s Unsat: 2.40s)
|
|
CPU Time : 783.760s
|
|
|
|
Choices : 15701115 (Domain: 15340000)
|
|
Conflicts : 700133 (Analyzed: 700130)
|
|
Restarts : 8450 (Average: 82.86 Last: 185)
|
|
Model-Level : 183.0
|
|
Problems : 89 (Average Length: 89.64 Splits: 0)
|
|
Lemmas : 700130 (Deleted: 651507)
|
|
Binary : 13411 (Ratio: 1.92%)
|
|
Ternary : 5069 (Ratio: 0.72%)
|
|
Conflict : 700130 (Average Length: 605.5 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 700130 (Average: 20.10 Max: 1562 Sum: 14069643)
|
|
Executed : 699968 (Average: 20.09 Max: 1562 Sum: 14063011 Ratio: 99.95%)
|
|
Bounded : 162 (Average: 40.94 Max: 117 Sum: 6632 Ratio: 0.05%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 902908 (Eliminated: 0 Frozen: 278344)
|
|
Constraints : 6624301 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
|
|
|
|
Memory Peak : 1071MB
|
|
Max. Length : 115 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 9.97s
|
|
Memory: 975MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 10.03s
|
|
|
|
Iteration 89
|
|
Queue: [(9,45,5,True), (10,50,5,False), (11,55,4,True), (12,60,4,False), (13,65,4,False), (14,70,3,True), (15,75,3,True), (16,80,3,False), (17,85,3,False), (18,90,3,False), (19,95,2,True), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
|
|
Grounded Until: 115
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 90
|
|
Time : 798.822s (Solving: 762.31s 1st Model: 0.00s Unsat: 2.40s)
|
|
CPU Time : 798.888s
|
|
|
|
Choices : 15834625 (Domain: 15472834)
|
|
Conflicts : 708742 (Analyzed: 708739)
|
|
Restarts : 8550 (Average: 82.89 Last: 185)
|
|
Model-Level : 183.0
|
|
Problems : 90 (Average Length: 89.94 Splits: 0)
|
|
Lemmas : 708739 (Deleted: 659396)
|
|
Binary : 13646 (Ratio: 1.93%)
|
|
Ternary : 5096 (Ratio: 0.72%)
|
|
Conflict : 708739 (Average Length: 620.5 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 708739 (Average: 20.00 Max: 1562 Sum: 14174053)
|
|
Executed : 708577 (Average: 19.99 Max: 1562 Sum: 14167421 Ratio: 99.95%)
|
|
Bounded : 162 (Average: 40.94 Max: 117 Sum: 6632 Ratio: 0.05%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 902908 (Eliminated: 0 Frozen: 278344)
|
|
Constraints : 6624301 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
|
|
|
|
Memory Peak : 1071MB
|
|
Max. Length : 115 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 15.06s
|
|
Memory: 975MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 15.13s
|
|
|
|
Iteration 90
|
|
Queue: [(11,55,4,True), (12,60,4,False), (13,65,4,False), (14,70,3,True), (15,75,3,True), (16,80,3,False), (17,85,3,False), (18,90,3,False), (19,95,2,True), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
|
|
Grounded Until: 115
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 91
|
|
Time : 810.135s (Solving: 773.44s 1st Model: 0.00s Unsat: 2.40s)
|
|
CPU Time : 810.204s
|
|
|
|
Choices : 16005985 (Domain: 15642429)
|
|
Conflicts : 717486 (Analyzed: 717483)
|
|
Restarts : 8650 (Average: 82.95 Last: 185)
|
|
Model-Level : 183.0
|
|
Problems : 91 (Average Length: 90.24 Splits: 0)
|
|
Lemmas : 717483 (Deleted: 669731)
|
|
Binary : 13747 (Ratio: 1.92%)
|
|
Ternary : 5143 (Ratio: 0.72%)
|
|
Conflict : 717483 (Average Length: 620.5 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 717483 (Average: 19.96 Max: 1562 Sum: 14324454)
|
|
Executed : 717321 (Average: 19.96 Max: 1562 Sum: 14317822 Ratio: 99.95%)
|
|
Bounded : 162 (Average: 40.94 Max: 117 Sum: 6632 Ratio: 0.05%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 902908 (Eliminated: 0 Frozen: 278344)
|
|
Constraints : 6624301 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
|
|
|
|
Memory Peak : 1071MB
|
|
Max. Length : 115 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 11.25s
|
|
Memory: 975MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 11.32s
|
|
|
|
Iteration 91
|
|
Queue: [(14,70,3,True), (15,75,3,True), (16,80,3,False), (17,85,3,False), (18,90,3,False), (19,95,2,True), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
|
|
Grounded Until: 115
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 92
|
|
Time : 819.691s (Solving: 782.77s 1st Model: 0.00s Unsat: 2.40s)
|
|
CPU Time : 819.764s
|
|
|
|
Choices : 16161851 (Domain: 15797917)
|
|
Conflicts : 725743 (Analyzed: 725740)
|
|
Restarts : 8750 (Average: 82.94 Last: 185)
|
|
Model-Level : 183.0
|
|
Problems : 92 (Average Length: 90.53 Splits: 0)
|
|
Lemmas : 725740 (Deleted: 676141)
|
|
Binary : 13781 (Ratio: 1.90%)
|
|
Ternary : 5172 (Ratio: 0.71%)
|
|
Conflict : 725740 (Average Length: 621.0 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 725740 (Average: 19.92 Max: 1562 Sum: 14457524)
|
|
Executed : 725578 (Average: 19.91 Max: 1562 Sum: 14450892 Ratio: 99.95%)
|
|
Bounded : 162 (Average: 40.94 Max: 117 Sum: 6632 Ratio: 0.05%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 902908 (Eliminated: 0 Frozen: 278344)
|
|
Constraints : 6624301 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
|
|
|
|
Memory Peak : 1071MB
|
|
Max. Length : 115 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 9.47s
|
|
Memory: 975MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 9.56s
|
|
|
|
Iteration 92
|
|
Queue: [(15,75,3,True), (16,80,3,False), (17,85,3,False), (18,90,3,False), (19,95,2,True), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
|
|
Grounded Until: 115
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 93
|
|
Time : 826.658s (Solving: 789.53s 1st Model: 0.00s Unsat: 2.40s)
|
|
CPU Time : 826.736s
|
|
|
|
Choices : 16291240 (Domain: 15926314)
|
|
Conflicts : 733422 (Analyzed: 733419)
|
|
Restarts : 8850 (Average: 82.87 Last: 185)
|
|
Model-Level : 183.0
|
|
Problems : 93 (Average Length: 90.82 Splits: 0)
|
|
Lemmas : 733419 (Deleted: 684072)
|
|
Binary : 13809 (Ratio: 1.88%)
|
|
Ternary : 5182 (Ratio: 0.71%)
|
|
Conflict : 733419 (Average Length: 619.9 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 733419 (Average: 19.86 Max: 1562 Sum: 14566457)
|
|
Executed : 733257 (Average: 19.85 Max: 1562 Sum: 14559825 Ratio: 99.95%)
|
|
Bounded : 162 (Average: 40.94 Max: 117 Sum: 6632 Ratio: 0.05%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 902908 (Eliminated: 0 Frozen: 278344)
|
|
Constraints : 6624301 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
|
|
|
|
Memory Peak : 1071MB
|
|
Max. Length : 115 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 6.89s
|
|
Memory: 975MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 6.97s
|
|
|
|
Iteration 93
|
|
Queue: [(19,95,2,True), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
|
|
Grounded Until: 115
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 94
|
|
Time : 835.736s (Solving: 798.43s 1st Model: 0.00s Unsat: 2.40s)
|
|
CPU Time : 835.808s
|
|
|
|
Choices : 16464509 (Domain: 16099110)
|
|
Conflicts : 741679 (Analyzed: 741676)
|
|
Restarts : 8950 (Average: 82.87 Last: 185)
|
|
Model-Level : 183.0
|
|
Problems : 94 (Average Length: 91.10 Splits: 0)
|
|
Lemmas : 741676 (Deleted: 691616)
|
|
Binary : 13833 (Ratio: 1.87%)
|
|
Ternary : 5187 (Ratio: 0.70%)
|
|
Conflict : 741676 (Average Length: 620.4 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 741676 (Average: 19.84 Max: 1562 Sum: 14715303)
|
|
Executed : 741513 (Average: 19.83 Max: 1562 Sum: 14708554 Ratio: 99.95%)
|
|
Bounded : 163 (Average: 41.40 Max: 117 Sum: 6749 Ratio: 0.05%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 902908 (Eliminated: 0 Frozen: 278344)
|
|
Constraints : 6624301 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
|
|
|
|
Memory Peak : 1071MB
|
|
Max. Length : 115 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 9.01s
|
|
Memory: 975MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 9.07s
|
|
|
|
Iteration 94
|
|
Queue: [(4,20,8,True), (5,25,8,True), (6,30,7,True), (7,35,7,True), (8,40,6,True), (9,45,6,False), (10,50,5,True), (11,55,5,False), (12,60,4,True), (13,65,4,False), (14,70,4,False), (15,75,4,False), (16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,True), (22,110,2,False), (23,115,2,False)]
|
|
Grounded Until: 115
|
|
Blocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0
|
|
Calls : 95
|
|
Time : 843.746s (Solving: 806.25s 1st Model: 0.00s Unsat: 10.22s)
|
|
CPU Time : 843.820s
|
|
|
|
Choices : 16496702 (Domain: 16131303)
|
|
Conflicts : 746118 (Analyzed: 746114)
|
|
Restarts : 9002 (Average: 82.88 Last: 185)
|
|
Model-Level : 183.0
|
|
Problems : 95 (Average Length: 91.37 Splits: 0)
|
|
Lemmas : 746114 (Deleted: 696156)
|
|
Binary : 13909 (Ratio: 1.86%)
|
|
Ternary : 5196 (Ratio: 0.70%)
|
|
Conflict : 746114 (Average Length: 618.5 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 746114 (Average: 19.76 Max: 1562 Sum: 14746605)
|
|
Executed : 745949 (Average: 19.76 Max: 1562 Sum: 14739854 Ratio: 99.95%)
|
|
Bounded : 165 (Average: 40.92 Max: 117 Sum: 6751 Ratio: 0.05%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 902908 (Eliminated: 0 Frozen: 278344)
|
|
Constraints : 6624275 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
|
|
|
|
Memory Peak : 1071MB
|
|
Max. Length : 115 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 7.94s
|
|
Memory: 975MB (+0MB)
|
|
UNSAT
|
|
Iteration Time: 8.02s
|
|
|
|
Iteration 95
|
|
Queue: [(5,25,8,True), (6,30,7,True), (7,35,7,True), (8,40,6,True), (9,45,6,False), (10,50,5,True), (11,55,5,False), (12,60,4,True), (13,65,4,False), (14,70,4,False), (15,75,4,False), (16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,True), (22,110,2,False), (23,115,2,False)]
|
|
Grounded Until: 115
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 96
|
|
Time : 846.967s (Solving: 809.29s 1st Model: 0.00s Unsat: 10.22s)
|
|
CPU Time : 847.044s
|
|
|
|
Choices : 16532716 (Domain: 16167317)
|
|
Conflicts : 753267 (Analyzed: 753263)
|
|
Restarts : 9102 (Average: 82.76 Last: 185)
|
|
Model-Level : 183.0
|
|
Problems : 96 (Average Length: 91.64 Splits: 0)
|
|
Lemmas : 753263 (Deleted: 703244)
|
|
Binary : 13916 (Ratio: 1.85%)
|
|
Ternary : 5197 (Ratio: 0.69%)
|
|
Conflict : 753263 (Average Length: 615.9 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 753263 (Average: 19.61 Max: 1562 Sum: 14773887)
|
|
Executed : 753098 (Average: 19.60 Max: 1562 Sum: 14767136 Ratio: 99.95%)
|
|
Bounded : 165 (Average: 40.92 Max: 117 Sum: 6751 Ratio: 0.05%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 902908 (Eliminated: 0 Frozen: 278344)
|
|
Constraints : 6624275 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
|
|
|
|
Memory Peak : 1071MB
|
|
Max. Length : 115 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 3.16s
|
|
Memory: 975MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 3.23s
|
|
|
|
Iteration 96
|
|
Queue: [(6,30,7,True), (7,35,7,True), (8,40,6,True), (9,45,6,False), (10,50,5,True), (11,55,5,False), (12,60,4,True), (13,65,4,False), (14,70,4,False), (15,75,4,False), (16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,True), (22,110,2,False), (23,115,2,False)]
|
|
Grounded Until: 115
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 97
|
|
Time : 860.534s (Solving: 822.67s 1st Model: 0.00s Unsat: 10.22s)
|
|
CPU Time : 860.616s
|
|
|
|
Choices : 16617579 (Domain: 16252173)
|
|
Conflicts : 761752 (Analyzed: 761748)
|
|
Restarts : 9202 (Average: 82.78 Last: 185)
|
|
Model-Level : 183.0
|
|
Problems : 97 (Average Length: 91.90 Splits: 0)
|
|
Lemmas : 761748 (Deleted: 710889)
|
|
Binary : 13978 (Ratio: 1.83%)
|
|
Ternary : 5219 (Ratio: 0.69%)
|
|
Conflict : 761748 (Average Length: 623.0 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 761748 (Average: 19.48 Max: 1562 Sum: 14839853)
|
|
Executed : 761583 (Average: 19.47 Max: 1562 Sum: 14833102 Ratio: 99.95%)
|
|
Bounded : 165 (Average: 40.92 Max: 117 Sum: 6751 Ratio: 0.05%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 902908 (Eliminated: 0 Frozen: 278344)
|
|
Constraints : 6624275 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
|
|
|
|
Memory Peak : 1071MB
|
|
Max. Length : 115 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 13.50s
|
|
Memory: 975MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 13.57s
|
|
|
|
Iteration 97
|
|
Queue: [(7,35,7,True), (8,40,6,True), (9,45,6,False), (10,50,5,True), (11,55,5,False), (12,60,4,True), (13,65,4,False), (14,70,4,False), (15,75,4,False), (16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,True), (22,110,2,False), (23,115,2,False)]
|
|
Grounded Until: 115
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 98
|
|
Time : 866.128s (Solving: 828.05s 1st Model: 0.00s Unsat: 10.22s)
|
|
CPU Time : 866.212s
|
|
|
|
Choices : 16671064 (Domain: 16305658)
|
|
Conflicts : 769396 (Analyzed: 769392)
|
|
Restarts : 9302 (Average: 82.71 Last: 185)
|
|
Model-Level : 183.0
|
|
Problems : 98 (Average Length: 92.15 Splits: 0)
|
|
Lemmas : 769392 (Deleted: 719004)
|
|
Binary : 13992 (Ratio: 1.82%)
|
|
Ternary : 5225 (Ratio: 0.68%)
|
|
Conflict : 769392 (Average Length: 621.7 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 769392 (Average: 19.34 Max: 1562 Sum: 14878825)
|
|
Executed : 769227 (Average: 19.33 Max: 1562 Sum: 14872074 Ratio: 99.95%)
|
|
Bounded : 165 (Average: 40.92 Max: 117 Sum: 6751 Ratio: 0.05%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 902908 (Eliminated: 0 Frozen: 278344)
|
|
Constraints : 6624275 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
|
|
|
|
Memory Peak : 1071MB
|
|
Max. Length : 115 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 5.51s
|
|
Memory: 975MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 5.60s
|
|
|
|
Iteration 98
|
|
Queue: [(8,40,6,True), (9,45,6,False), (10,50,5,True), (11,55,5,False), (12,60,4,True), (13,65,4,False), (14,70,4,False), (15,75,4,False), (16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,True), (22,110,2,False), (23,115,2,False)]
|
|
Grounded Until: 115
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 99
|
|
Time : 874.300s (Solving: 836.02s 1st Model: 0.00s Unsat: 10.22s)
|
|
CPU Time : 874.388s
|
|
|
|
Choices : 16771158 (Domain: 16405189)
|
|
Conflicts : 777657 (Analyzed: 777653)
|
|
Restarts : 9402 (Average: 82.71 Last: 185)
|
|
Model-Level : 183.0
|
|
Problems : 99 (Average Length: 92.40 Splits: 0)
|
|
Lemmas : 777653 (Deleted: 726455)
|
|
Binary : 14083 (Ratio: 1.81%)
|
|
Ternary : 5235 (Ratio: 0.67%)
|
|
Conflict : 777653 (Average Length: 621.4 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 777653 (Average: 19.23 Max: 1562 Sum: 14957932)
|
|
Executed : 777488 (Average: 19.23 Max: 1562 Sum: 14951181 Ratio: 99.95%)
|
|
Bounded : 165 (Average: 40.92 Max: 117 Sum: 6751 Ratio: 0.05%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 902908 (Eliminated: 0 Frozen: 278344)
|
|
Constraints : 6624275 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
|
|
|
|
Memory Peak : 1071MB
|
|
Max. Length : 115 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 8.10s
|
|
Memory: 975MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 8.18s
|
|
|
|
Iteration 99
|
|
Queue: [(10,50,5,True), (11,55,5,False), (12,60,4,True), (13,65,4,False), (14,70,4,False), (15,75,4,False), (16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,True), (22,110,2,False), (23,115,2,False)]
|
|
Grounded Until: 115
|
|
Unblocking actions...
|
|
Solving...
|
|
[start: stats after solve call]
|
|
|
|
Models : 0+
|
|
Calls : 100
|
|
Time : 888.923s (Solving: 850.46s 1st Model: 0.00s Unsat: 10.22s)
|
|
CPU Time : 889.016s
|
|
|
|
Choices : 16945498 (Domain: 16578149)
|
|
Conflicts : 786145 (Analyzed: 786141)
|
|
Restarts : 9502 (Average: 82.73 Last: 185)
|
|
Model-Level : 183.0
|
|
Problems : 100 (Average Length: 92.65 Splits: 0)
|
|
Lemmas : 786141 (Deleted: 734313)
|
|
Binary : 14299 (Ratio: 1.82%)
|
|
Ternary : 5281 (Ratio: 0.67%)
|
|
Conflict : 786141 (Average Length: 624.0 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 786141 (Average: 19.21 Max: 1562 Sum: 15101934)
|
|
Executed : 785976 (Average: 19.20 Max: 1562 Sum: 15095183 Ratio: 99.96%)
|
|
Bounded : 165 (Average: 40.92 Max: 117 Sum: 6751 Ratio: 0.04%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 902908 (Eliminated: 0 Frozen: 278344)
|
|
Constraints : 6624275 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
|
|
|
|
Memory Peak : 1071MB
|
|
Max. Length : 115 steps
|
|
Models : 1
|
|
|
|
[endof: stats after solve call]
|
|
Solving Time: 14.56s
|
|
Memory: 975MB (+0MB)
|
|
UNKNOWN
|
|
Iteration Time: 14.63s
|
|
|
|
Iteration 100
|
|
Queue: [(12,60,4,True), (13,65,4,False), (14,70,4,False), (15,75,4,False), (16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,True), (22,110,2,False), (23,115,2,False)]
|
|
Grounded Until: 115
|
|
Unblocking actions...
|
|
Solving...
|
|
*** Info : (planner): INTERRUPTED by signal!
|
|
UNKNOWN
|
|
|
|
INTERRUPTED : 1
|
|
|
|
Models : 0+
|
|
Calls : 101
|
|
Time : 892.583s (Solving: 853.91s 1st Model: 0.00s Unsat: 10.22s)
|
|
CPU Time : 892.652s
|
|
|
|
Choices : 16998304 (Domain: 16630745)
|
|
Conflicts : 788629 (Analyzed: 788625)
|
|
Restarts : 9529 (Average: 82.76 Last: 185)
|
|
Model-Level : 183.0
|
|
Problems : 101 (Average Length: 92.89 Splits: 0)
|
|
Lemmas : 788625 (Deleted: 738218)
|
|
Binary : 14320 (Ratio: 1.82%)
|
|
Ternary : 5287 (Ratio: 0.67%)
|
|
Conflict : 788625 (Average Length: 624.7 Ratio: 100.00%)
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
|
Backjumps : 788625 (Average: 19.21 Max: 1562 Sum: 15147547)
|
|
Executed : 788460 (Average: 19.20 Max: 1562 Sum: 15140796 Ratio: 99.96%)
|
|
Bounded : 165 (Average: 40.92 Max: 117 Sum: 6751 Ratio: 0.04%)
|
|
|
|
Rules : 91724 (Original: 89679)
|
|
Atoms : 73746
|
|
Bodies : 16519 (Original: 14473)
|
|
Count : 330 (Original: 739)
|
|
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
|
|
Tight : Yes
|
|
Variables : 902908 (Eliminated: 0 Frozen: 278344)
|
|
Constraints : 6624275 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
|
|
|
|
Memory Peak : 1071MB
|
|
Max. Length : 115 steps
|
|
Models : 1
|
|
|
|
|