diff --git a/Experimentation/Investigations/Cryptography/AdvancedEncryptionStandard/plans/Representations/Inv_8.hpp b/Experimentation/Investigations/Cryptography/AdvancedEncryptionStandard/plans/Representations/Inv_8.hpp
index 230951cab7..106aeb3ed1 100644
--- a/Experimentation/Investigations/Cryptography/AdvancedEncryptionStandard/plans/Representations/Inv_8.hpp
+++ b/Experimentation/Investigations/Cryptography/AdvancedEncryptionStandard/plans/Representations/Inv_8.hpp
@@ -1,5 +1,5 @@
 // Matthew Gwynne, 12.1.2011 (Swansea)
-/* Copyright 2011 Oliver Kullmann
+/* Copyright 2011, 2012 Oliver Kullmann
 This file is part of the OKlibrary. OKlibrary is free software; you can redistribute
 it and/or modify it under the terms of the GNU General Public License as published by
 the Free Software Foundation and included in this library; either version 3 of the
@@ -148,6 +148,9 @@ R> subset(E, min == 359)
 
   \todo r_1-bases : mincl_r1 <= 4200
   <ul>
+   <li> The 1-bases below need to be checked to ensure they are actually
+   1-bases; see "Computing r_1-bases for a set of prime implicates" in
+   Satisfiability/Reductions/Bases/plans/UcpBase.hpp. </li>
    <li> Current minimum clause-count of an r_1-base: 4200. </li>
    <li> Iterating through the random seeds, while sorting inputs in
    ascending order of clause-length into RUcpGen, and descending into
diff --git a/Experimentation/Investigations/Cryptography/AdvancedEncryptionStandard/plans/Representations/Mul_11_8.hpp b/Experimentation/Investigations/Cryptography/AdvancedEncryptionStandard/plans/Representations/Mul_11_8.hpp
index b6ab1c990e..94de2a6f6b 100644
--- a/Experimentation/Investigations/Cryptography/AdvancedEncryptionStandard/plans/Representations/Mul_11_8.hpp
+++ b/Experimentation/Investigations/Cryptography/AdvancedEncryptionStandard/plans/Representations/Mul_11_8.hpp
@@ -1,5 +1,5 @@
 // Matthew Gwynne, 7.1.2011 (Swansea)
-/* Copyright 2011 Oliver Kullmann
+/* Copyright 2011, 2012 Oliver Kullmann
 This file is part of the OKlibrary. OKlibrary is free software; you can redistribute
 it and/or modify it under the terms of the GNU General Public License as published by
 the Free Software Foundation and included in this library; either version 3 of the
@@ -53,6 +53,9 @@ c's = 1, n = 16, c = 15008, tc = 0, ntc = 15008, tl = 119824, l = 119824, finish
 
   \todo r_1-bases : mincl_r1 <= 1376
   <ul>
+   <li> The 1-bases below need to be checked to ensure they are actually
+   1-bases; see "Computing r_1-bases for a set of prime implicates" in
+   Satisfiability/Reductions/Bases/plans/UcpBase.hpp. </li>
    <li> Computing an r_1-base:
    \verbatim
 shell> QuineMcCluskey-n16-O3-DNDEBUG AES_byte_field_mul_full_11.cnf > AES_byte_field_mul_pi_11.cnf
diff --git a/Experimentation/Investigations/Cryptography/AdvancedEncryptionStandard/plans/Representations/Mul_13_8.hpp b/Experimentation/Investigations/Cryptography/AdvancedEncryptionStandard/plans/Representations/Mul_13_8.hpp
index 4f72206f2c..e52834815d 100644
--- a/Experimentation/Investigations/Cryptography/AdvancedEncryptionStandard/plans/Representations/Mul_13_8.hpp
+++ b/Experimentation/Investigations/Cryptography/AdvancedEncryptionStandard/plans/Representations/Mul_13_8.hpp
@@ -1,5 +1,5 @@
 // Matthew Gwynne, 7.1.2011 (Swansea)
-/* Copyright 2011 Oliver Kullmann
+/* Copyright 2011, 2012 Oliver Kullmann
 This file is part of the OKlibrary. OKlibrary is free software; you can redistribute
 it and/or modify it under the terms of the GNU General Public License as published by
 the Free Software Foundation and included in this library; either version 3 of the
@@ -53,6 +53,9 @@ c's = 1, n = 16, c = 15312, tc = 0, ntc = 15312, tl = 122816, l = 122816, finish
 
   \todo r_1-bases : mincl_r1 <= 1040
   <ul>
+   <li> The 1-bases below need to be checked to ensure they are actually
+   1-bases; see "Computing r_1-bases for a set of prime implicates" in
+   Satisfiability/Reductions/Bases/plans/UcpBase.hpp. </li>
    <li> Computing an r_1-base:
    \verbatim
 shell> QuineMcCluskey-n16-O3-DNDEBUG AES_byte_field_mul_full_13.cnf > AES_byte_field_mul_pi_13.cnf
diff --git a/Experimentation/Investigations/Cryptography/AdvancedEncryptionStandard/plans/Representations/Mul_14_8.hpp b/Experimentation/Investigations/Cryptography/AdvancedEncryptionStandard/plans/Representations/Mul_14_8.hpp
index 40f1b213e7..499c67eb75 100644
--- a/Experimentation/Investigations/Cryptography/AdvancedEncryptionStandard/plans/Representations/Mul_14_8.hpp
+++ b/Experimentation/Investigations/Cryptography/AdvancedEncryptionStandard/plans/Representations/Mul_14_8.hpp
@@ -1,5 +1,5 @@
 // Matthew Gwynne, 7.1.2011 (Swansea)
-/* Copyright 2011 Oliver Kullmann
+/* Copyright 2011, 2012 Oliver Kullmann
 This file is part of the OKlibrary. OKlibrary is free software; you can redistribute
 it and/or modify it under the terms of the GNU General Public License as published by
 the Free Software Foundation and included in this library; either version 3 of the
@@ -55,6 +55,9 @@ c's = 1, n = 16, c = 14300, tc = 0, ntc = 14300, tl = 114252, l = 114252, finish
 
   \todo r_1-bases : mincl_r1 <= 1052
   <ul>
+   <li> The 1-bases below need to be checked to ensure they are actually
+   1-bases; see "Computing r_1-bases for a set of prime implicates" in
+   Satisfiability/Reductions/Bases/plans/UcpBase.hpp. </li>
    <li> Computing an r_1-base:
    \verbatim
 shell> QuineMcCluskey-n16-O3-DNDEBUG AES_byte_field_mul_full_14.cnf > AES_byte_field_mul_pi_14.cnf
diff --git a/Experimentation/Investigations/Cryptography/AdvancedEncryptionStandard/plans/Representations/Mul_2_8.hpp b/Experimentation/Investigations/Cryptography/AdvancedEncryptionStandard/plans/Representations/Mul_2_8.hpp
index 2cf36dae1e..7561e53a3f 100644
--- a/Experimentation/Investigations/Cryptography/AdvancedEncryptionStandard/plans/Representations/Mul_2_8.hpp
+++ b/Experimentation/Investigations/Cryptography/AdvancedEncryptionStandard/plans/Representations/Mul_2_8.hpp
@@ -1,5 +1,5 @@
 // Matthew Gwynne, 7.1.2011 (Swansea)
-/* Copyright 2011 Oliver Kullmann
+/* Copyright 2011, 2012 Oliver Kullmann
 This file is part of the OKlibrary. OKlibrary is free software; you can redistribute
 it and/or modify it under the terms of the GNU General Public License as published by
 the Free Software Foundation and included in this library; either version 3 of the
@@ -89,6 +89,9 @@ maxima> Mul2_min_F_hd_l : setify(create_list(hardness_wpi_cs(setify(Mul2_min_F_l
 
   \todo r_1-bases : mincl_r1 <= 22
   <ul>
+   <li> The 1-bases below need to be checked to ensure they are actually
+   1-bases; see "Computing r_1-bases for a set of prime implicates" in
+   Satisfiability/Reductions/Bases/plans/UcpBase.hpp. </li>
    <li> Current minimum clause-count of an r_1-base: 22. </li>
    <li> For the mincl_rinf representations, see "Minimising using hypergraph
    transversal tools". </li>
diff --git a/Experimentation/Investigations/Cryptography/AdvancedEncryptionStandard/plans/Representations/Mul_3_8.hpp b/Experimentation/Investigations/Cryptography/AdvancedEncryptionStandard/plans/Representations/Mul_3_8.hpp
index d5d906996d..259a52c573 100644
--- a/Experimentation/Investigations/Cryptography/AdvancedEncryptionStandard/plans/Representations/Mul_3_8.hpp
+++ b/Experimentation/Investigations/Cryptography/AdvancedEncryptionStandard/plans/Representations/Mul_3_8.hpp
@@ -1,5 +1,5 @@
 // Matthew Gwynne, 7.1.2011 (Swansea)
-/* Copyright 2011 Oliver Kullmann
+/* Copyright 2011, 2012 Oliver Kullmann
 This file is part of the OKlibrary. OKlibrary is free software; you can redistribute
 it and/or modify it under the terms of the GNU General Public License as published by
 the Free Software Foundation and included in this library; either version 3 of the
@@ -103,6 +103,9 @@ maxima> hardness_wpi_cs(setify(ev_hm(ss_field_cnfs,[8,3])[2]),Mul3_F_primes[2]);
 
   \todo r_1-bases : mincl_r1 <= 80
   <ul>
+   <li> The 1-bases below need to be checked to ensure they are actually
+   1-bases; see "Computing r_1-bases for a set of prime implicates" in
+   Satisfiability/Reductions/Bases/plans/UcpBase.hpp. </li>
    <li> Computing three r_1-bases:
    \verbatim
 > seed=1; RandomShuffleDimacs-O3-DNDEBUG ${seed} < AES_byte_field_mul_pi_3.cnf | RUcpBase-O3-DNDEBUG | tee AES_byte_field_mul_bases_${seed}.cnf | ExtendedDimacsFullStatistics-O3-DNDEBUG
diff --git a/Experimentation/Investigations/Cryptography/AdvancedEncryptionStandard/plans/Representations/Mul_9_8.hpp b/Experimentation/Investigations/Cryptography/AdvancedEncryptionStandard/plans/Representations/Mul_9_8.hpp
index 3303eb8d62..bb672fb736 100644
--- a/Experimentation/Investigations/Cryptography/AdvancedEncryptionStandard/plans/Representations/Mul_9_8.hpp
+++ b/Experimentation/Investigations/Cryptography/AdvancedEncryptionStandard/plans/Representations/Mul_9_8.hpp
@@ -1,5 +1,5 @@
 // Matthew Gwynne, 7.1.2011 (Swansea)
-/* Copyright 2011 Oliver Kullmann
+/* Copyright 2011, 2012 Oliver Kullmann
 This file is part of the OKlibrary. OKlibrary is free software; you can redistribute
 it and/or modify it under the terms of the GNU General Public License as published by
 the Free Software Foundation and included in this library; either version 3 of the
@@ -54,6 +54,9 @@ c's = 1, n = 16, c = 7840, tc = 0, ntc = 7840, tl = 60352, l = 60352, finished =
 
   \todo r_1-bases : mincl_r1 <= 272
   <ul>
+   <li> The 1-bases below need to be checked to ensure they are actually
+   1-bases; see "Computing r_1-bases for a set of prime implicates" in
+   Satisfiability/Reductions/Bases/plans/UcpBase.hpp. </li>
    <li> Computing an r_1-base:
    \verbatim
 shell> QuineMcCluskey-n16-O3-DNDEBUG AES_byte_field_mul_full_9.cnf > AES_byte_field_mul_pi_9.cnf
diff --git a/Experimentation/Investigations/Cryptography/AdvancedEncryptionStandard/plans/Representations/RoundColumn_2_4.hpp b/Experimentation/Investigations/Cryptography/AdvancedEncryptionStandard/plans/Representations/RoundColumn_2_4.hpp
index 7eaff2aa4f..61f5a87026 100644
--- a/Experimentation/Investigations/Cryptography/AdvancedEncryptionStandard/plans/Representations/RoundColumn_2_4.hpp
+++ b/Experimentation/Investigations/Cryptography/AdvancedEncryptionStandard/plans/Representations/RoundColumn_2_4.hpp
@@ -151,6 +151,9 @@ maxima> output_fcs("16-bit AES Round",bf2relation_fullcnf_fcs(lambda([V],ss_roun
 
   \todo r_1-bases : mincl_r1 <= 2712
   <ul>
+   <li> The 1-bases below need to be checked to ensure they are actually
+   1-bases; see "Computing r_1-bases for a set of prime implicates" in
+   Satisfiability/Reductions/Bases/plans/UcpBase.hpp. </li>
    <li> We can compute r_1-base statistics by:
    \verbatim
 shell> RandomRUcpBases round_column_16_full.cnf
diff --git a/Experimentation/Investigations/Cryptography/AdvancedEncryptionStandard/plans/Representations/Sbox_8.hpp b/Experimentation/Investigations/Cryptography/AdvancedEncryptionStandard/plans/Representations/Sbox_8.hpp
index 7b8439853f..9b1e7d3d48 100644
--- a/Experimentation/Investigations/Cryptography/AdvancedEncryptionStandard/plans/Representations/Sbox_8.hpp
+++ b/Experimentation/Investigations/Cryptography/AdvancedEncryptionStandard/plans/Representations/Sbox_8.hpp
@@ -302,9 +302,40 @@ Error: Impossible to solve the PI chart (too many possible combinations).
   </ul>
 
 
-  \todo r_1-bases : mincl_r1 <= 4398
+  \todo r_1-bases : mincl_r1 <= ????
   <ul>
-   <li> Current minimum clause-count of an r_1-base: 4398. </li>
+   <li> The 1-bases below need to be checked to ensure they are actually
+   1-bases; see "Computing r_1-bases for a set of prime implicates" in
+   Satisfiability/Reductions/Bases/plans/UcpBase.hpp. </li>
+   <li> The current "best 1-base" with 4398 clauses is not a 1-base!
+   \verbatim
+maxima> output_rijnsbox_fullcnf_stdname();
+shell> QuineMcCluskey-n16-O3-DNDEBUG AES_Sbox_full.cnf > AES_Sbox_PI.cnf
+shell> cat AES_Sbox_PI.cnf | RandomShuffleDimacs-O3-DNDEBUG 103 | SortByClauseLength-O3-DNDEBUG > AES_Sbox_PI_randsort_103.cnf
+shell> RUcpGen-O3-DNDEBUG AES_Sbox_PI_randsort_103.cnf > AES_Sbox_gen_103.cnf
+shell> cat AES_Sbox_gen_103.cnf | RandomShuffleDimacs-O3-DNDEBUG 1 | SortByClauseLengthDescending-O3-DNDEBUG | RUcpBase-O3-DNDEBUG > AES_Sbox_base_gs103_bs1.cnf
+maxima> Sbox_1base : read_fcl_f("AES_Sbox_base_gs103_bs1.cnf")$
+maxima> Sbox_PI : read_fcl_f("AES_Sbox_PI.cnf")$
+maxima> hardness_wpi_cs(setify(Sbox_1base[2]),setify(Sbox_PI[2]));
+2
+   \endverbatim
+   However, far more prime implicates follow by UCP for the "current 1-base"
+   than for the current best minimum representation, which may help to
+   explain any differences in the performance of SAT solvers:
+   \verbatim
+ksoft_primes_cs(F,F_PI,k) :=
+   subset(map(comp_sl,F_PI),
+           lambda([C], is(hardness_wpi_cs(apply_pa_cs(C, F),{{}}) <= k)))$
+Sbox_1base_1soft_primes : ksoft_primes_cs(setify(Sbox_1base[2]),setify(Sbox_PI[2]),1)$
+print(length(Sbox_1base_1soft_primes), "/", length(Sbox_PI[2]));
+132025 / 136253
+
+Sbox_min_1soft_primes : ksoft_primes_cs(setify(ev_hm(ss_sbox_cnfs,8)[2]),setify(Sbox_PI[2]),1)$
+print(length(Sbox_min_1soft_primes),"/", length(Sbox_PI[2]));
+3474 / 136253
+   \endverbatim
+   </li>
+   <li> Current minimum clause-count of an r_1-base: ???. </li>
    <li> Starting with a generating set, created from scratch:
    \verbatim
 > RUcpGen-O3-DNDEBUG AES_PK.cnf > AES_gen.cnf