Commit 22d56ae9 authored by BenChurcheward's avatar BenChurcheward
Browse files

Added stats file

parent 33e4400a
########## Stats for k=1 ##########
Models : 1
Optimum : yes
Optimization : 121
Calls : 1
Time : 0.581s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
CPU Time : 0.580s
Choices : 0
Conflicts : 0 (Analyzed: 0)
Restarts : 0
Model-Level : 0.0
Problems : 1 (Average Length: 0.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 : 86979
Choice : 156
Minimize : 1
Atoms : 62642
Bodies : 36978
Sum : 1
Count : 1
Equivalences : 37737 (Atom=Atom: 12682 Body=Body: 12372 Other: 12683)
Tight : Yes
Variables : 156 (Eliminated: 0 Frozen: 0)
Constraints : 0 (Binary: 0.0% Ternary: 0.0% Other: 0.0%)
########## Stats for k=2 ##########
Models : 4
Optimum : yes
Optimization : 162
Calls : 1
Time : 0.800s (Solving: 0.02s 1st Model: 0.00s Unsat: 0.01s)
CPU Time : 0.800s
Choices : 70
Conflicts : 42 (Analyzed: 41)
Restarts : 0
Model-Level : 9.2
Problems : 1 (Average Length: 0.00 Splits: 0)
Lemmas : 41 (Deleted: 0)
Binary : 17 (Ratio: 41.46%)
Ternary : 5 (Ratio: 12.20%)
Conflict : 41 (Average Length: 32.8 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 41 (Average: 1.29 Max: 12 Sum: 53)
Executed : 41 (Average: 1.29 Max: 12 Sum: 53 Ratio: 100.00%)
Bounded : 0 (Average: 0.00 Max: 0 Sum: 0 Ratio: 0.00%)
Rules : 185534 (Original: 185378)
Choice : 156
Minimize : 1
Atoms : 100750
Bodies : 134750 (Original: 134906)
Sum : 2
Count : 2 (Original: 158)
Equivalences : 99624 (Atom=Atom: 508 Body=Body: 32 Other: 99084)
Tight : Yes
Variables : 74397 (Eliminated: 0 Frozen: 510)
Constraints : 305672 (Binary: 75.8% Ternary: 24.0% Other: 0.2%)
########## Stats for k=3 ##########
Models : 10
Optimum : yes
Optimization : 157
Calls : 1
Time : 1.275s (Solving: 0.17s 1st Model: 0.02s Unsat: 0.02s)
CPU Time : 1.276s
Choices : 747
Conflicts : 71 (Analyzed: 70)
Restarts : 0
Model-Level : 82.0
Problems : 1 (Average Length: 0.00 Splits: 0)
Lemmas : 70 (Deleted: 0)
Binary : 2 (Ratio: 2.86%)
Ternary : 3 (Ratio: 4.29%)
Conflict : 70 (Average Length: 116.6 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 70 (Average: 7.11 Max: 106 Sum: 498)
Executed : 70 (Average: 7.11 Max: 106 Sum: 498 Ratio: 100.00%)
Bounded : 0 (Average: 0.00 Max: 0 Sum: 0 Ratio: 0.00%)
Rules : 295594 (Original: 294970)
Choice : 156
Minimize : 1
Atoms : 113777
Bodies : 244029 (Original: 244338)
Sum : 3
Count : 3 (Original: 315)
Equivalences : 100569 (Atom=Atom: 669 Body=Body: 35 Other: 99865)
Tight : Yes
Variables : 171736 (Eliminated: 0 Frozen: 668)
Constraints : 669450 (Binary: 74.4% Ternary: 21.9% Other: 3.7%)
########## Stats for k=4 ##########
Models : 7
Optimum : yes
Optimization : 145
Calls : 1
Time : 1.905s (Solving: 0.39s 1st Model: 0.03s Unsat: 0.17s)
CPU Time : 1.904s
Choices : 757
Conflicts : 88 (Analyzed: 87)
Restarts : 1 (Average: 87.00 Last: 8)
Model-Level : 190.3
Problems : 1 (Average Length: 0.00 Splits: 0)
Lemmas : 87 (Deleted: 0)
Binary : 3 (Ratio: 3.45%)
Ternary : 7 (Ratio: 8.05%)
Conflict : 87 (Average Length: 107.3 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 87 (Average: 4.52 Max: 102 Sum: 393)
Executed : 87 (Average: 4.52 Max: 102 Sum: 393 Ratio: 100.00%)
Bounded : 0 (Average: 0.00 Max: 0 Sum: 0 Ratio: 0.00%)
Rules : 442080 (Original: 440832)
Choice : 156
Minimize : 1
Atoms : 126804
Bodies : 389579 (Original: 389885)
Sum : 4
Count : 4 (Original: 316)
Equivalences : 125694 (Atom=Atom: 830 Body=Body: 38 Other: 124826)
Tight : Yes
Variables : 269075 (Eliminated: 0 Frozen: 826)
Constraints : 1093679 (Binary: 75.5% Ternary: 22.2% Other: 2.3%)
########## Stats for k=5 ##########
Models : 24
Optimum : yes
Optimization : 142
Calls : 1
Time : 5.556s (Solving: 3.42s 1st Model: 0.10s Unsat: 1.55s)
CPU Time : 5.556s
Choices : 4621
Conflicts : 651 (Analyzed: 650)
Restarts : 5 (Average: 130.00 Last: 112)
Model-Level : 103.1
Problems : 1 (Average Length: 0.00 Splits: 0)
Lemmas : 650 (Deleted: 0)
Binary : 42 (Ratio: 6.46%)
Ternary : 139 (Ratio: 21.38%)
Conflict : 650 (Average Length: 56.3 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 650 (Average: 4.25 Max: 119 Sum: 2763)
Executed : 650 (Average: 4.25 Max: 119 Sum: 2763 Ratio: 100.00%)
Bounded : 0 (Average: 0.00 Max: 0 Sum: 0 Ratio: 0.00%)
Rules : 624992 (Original: 622964)
Choice : 156
Minimize : 1
Atoms : 139831
Bodies : 571400 (Original: 571702)
Sum : 5
Count : 5 (Original: 317)
Equivalences : 150819 (Atom=Atom: 991 Body=Body: 41 Other: 149787)
Tight : Yes
Variables : 390594 (Eliminated: 0 Frozen: 984)
Constraints : 1626719 (Binary: 76.0% Ternary: 22.4% Other: 1.6%)
########## Stats for k=6 ##########
Models : 31
Optimum : yes
Optimization : 141
Calls : 1
Time : 11.650s (Solving: 8.89s 1st Model: 0.13s Unsat: 6.63s)
CPU Time : 11.644s
Choices : 9724
Conflicts : 921 (Analyzed: 920)
Restarts : 6 (Average: 153.33 Last: 102)
Model-Level : 345.7
Problems : 1 (Average Length: 0.00 Splits: 0)
Lemmas : 920 (Deleted: 0)
Binary : 27 (Ratio: 2.93%)
Ternary : 116 (Ratio: 12.61%)
Conflict : 920 (Average Length: 42.5 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 920 (Average: 5.68 Max: 293 Sum: 5228)
Executed : 920 (Average: 5.68 Max: 293 Sum: 5228 Ratio: 100.00%)
Bounded : 0 (Average: 0.00 Max: 0 Sum: 0 Ratio: 0.00%)
Rules : 844330 (Original: 841366)
Choice : 156
Minimize : 1
Atoms : 152858
Bodies : 789492 (Original: 789789)
Sum : 6
Count : 6 (Original: 318)
Equivalences : 175944 (Atom=Atom: 1152 Body=Body: 44 Other: 174748)
Tight : Yes
Variables : 536293 (Eliminated: 0 Frozen: 1142)
Constraints : 2268570 (Binary: 76.4% Ternary: 22.5% Other: 1.1%)
########## Stats for k=7 ##########
Models : 53
Optimum : yes
Optimization : 139
Calls : 1
Time : 14.847s (Solving: 11.30s 1st Model: 0.11s Unsat: 4.29s)
CPU Time : 14.840s
Choices : 16726
Conflicts : 855 (Analyzed: 854)
Restarts : 6 (Average: 142.33 Last: 12)
Model-Level : 269.7
Problems : 1 (Average Length: 0.00 Splits: 0)
Lemmas : 854 (Deleted: 0)
Binary : 66 (Ratio: 7.73%)
Ternary : 144 (Ratio: 16.86%)
Conflict : 854 (Average Length: 146.5 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 854 (Average: 4.34 Max: 158 Sum: 3705)
Executed : 854 (Average: 4.34 Max: 158 Sum: 3705 Ratio: 100.00%)
Bounded : 0 (Average: 0.00 Max: 0 Sum: 0 Ratio: 0.00%)
Rules : 1096974 (Original: 1096038)
Choice : 156
Minimize : 1
Atoms : 165885
Bodies : 1043990 (Original: 1044146)
Sum : 7
Count : 163 (Original: 319)
Equivalences : 201224 (Atom=Atom: 1313 Body=Body: 47 Other: 199864)
Tight : Yes
Variables : 709582 (Eliminated: 0 Frozen: 1300)
Constraints : 3029442 (Binary: 76.6% Ternary: 22.5% Other: 0.9%)
########## Stats for k=8 ##########
Models : 58
Optimum : yes
Optimization : 137
Calls : 1
Time : 72.732s (Solving: 68.18s 1st Model: 0.36s Unsat: 61.23s)
CPU Time : 72.700s
Choices : 18603
Conflicts : 3529 (Analyzed: 3528)
Restarts : 21 (Average: 168.00 Last: 72)
Model-Level : 345.7
Problems : 1 (Average Length: 0.00 Splits: 0)
Lemmas : 3528 (Deleted: 1212)
Binary : 35 (Ratio: 0.99%)
Ternary : 190 (Ratio: 5.39%)
Conflict : 3528 (Average Length: 173.9 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 3528 (Average: 3.34 Max: 710 Sum: 11781)
Executed : 3528 (Average: 3.34 Max: 710 Sum: 11781 Ratio: 100.00%)
Bounded : 0 (Average: 0.00 Max: 0 Sum: 0 Ratio: 0.00%)
Rules : 1388072 (Original: 1386980)
Choice : 156
Minimize : 1
Atoms : 178912
Bodies : 1334617 (Original: 1334773)
Sum : 8
Count : 164 (Original: 320)
Equivalences : 226349 (Atom=Atom: 1474 Body=Body: 50 Other: 224825)
Tight : Yes
Variables : 904726 (Eliminated: 0 Frozen: 1458)
Constraints : 3892163 (Binary: 76.8% Ternary: 22.5% Other: 0.7%)
########## Stats for k=9 ##########
Models : 57
Optimum : yes
Optimization : 136
Calls : 1
Time : 1163.113s (Solving: 1157.43s 1st Model: 0.21s Unsat: 1139.17s)
CPU Time : 1162.644s
Choices : 155514
Conflicts : 46407 (Analyzed: 46406)
Restarts : 172 (Average: 269.80 Last: 18)
Model-Level : 649.1
Problems : 1 (Average Length: 0.00 Splits: 0)
Lemmas : 46406 (Deleted: 38302)
Binary : 137 (Ratio: 0.30%)
Ternary : 459 (Ratio: 0.99%)
Conflict : 46406 (Average Length: 60.4 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 46406 (Average: 2.67 Max: 7524 Sum: 123821)
Executed : 46406 (Average: 2.67 Max: 7524 Sum: 123821 Ratio: 100.00%)
Bounded : 0 (Average: 0.00 Max: 0 Sum: 0 Ratio: 0.00%)
Rules : 1715440 (Original: 1714192)
Choice : 156
Minimize : 1
Atoms : 191939
Bodies : 1661514 (Original: 1661670)
Sum : 9
Count : 165 (Original: 321)
Equivalences : 251474 (Atom=Atom: 1635 Body=Body: 53 Other: 249786)
Tight : Yes
Variables : 1124205 (Eliminated: 0 Frozen: 1616)
Constraints : 4864159 (Binary: 76.9% Ternary: 22.5% Other: 0.5%)
########## Stats for k=10 ##########
Models : 20
Optimum : yes
Optimization : 136
Calls : 1
Time : 113.060s (Solving: 106.05s 1st Model: 0.32s Unsat: 80.56s)
CPU Time : 113.024s
Choices : 16878
Conflicts : 7072 (Analyzed: 7071)
Restarts : 30 (Average: 235.70 Last: 942)
Model-Level : 127.5
Problems : 1 (Average Length: 0.00 Splits: 0)
Lemmas : 7071 (Deleted: 2939)
Binary : 302 (Ratio: 4.27%)
Ternary : 634 (Ratio: 8.97%)
Conflict : 7071 (Average Length: 129.8 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 7071 (Average: 2.01 Max: 151 Sum: 14206)
Executed : 7071 (Average: 2.01 Max: 151 Sum: 14206 Ratio: 100.00%)
Bounded : 0 (Average: 0.00 Max: 0 Sum: 0 Ratio: 0.00%)
Rules : 2079078 (Original: 2077674)
Choice : 156
Minimize : 1
Atoms : 204966
Bodies : 2024681 (Original: 2024837)
Sum : 10
Count : 166 (Original: 322)
Equivalences : 276599 (Atom=Atom: 1796 Body=Body: 56 Other: 274747)
Tight : Yes
Variables : 1368019 (Eliminated: 0 Frozen: 1774)
Constraints : 5945430 (Binary: 77.0% Ternary: 22.5% Other: 0.4%)
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment