Experiments with multipliers.

3 files changed, 612 insertions, 175 deletions

diff --git a/src/base/wlc/wlcGraft.c b/src/base/wlc/wlcGraft.c
index 8ac825fc..f7e59cf9 100644
--- a/src/base/wlc/wlcGraft.c
+++ b/src/base/wlc/wlcGraft.c
@@ -285,6 +285,155 @@ Wlc_Ntk_t * Wlc_NtkGraftMulti( Wlc_Ntk_t * p, int fVerbose )
     return pNew;
 }
 
+
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Generate simulation vectors.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sbc_Mult( word a, word b, word r[2] )
+{
+    word pL  = (a & 0xFFFFFFFF) * (b & 0xFFFFFFFF);
+    word pM1 = (a & 0xFFFFFFFF) * (b >> 32);
+    word pM2 = (a >> 32) * (b & 0xFFFFFFFF);
+    word pH  = (a >> 32) * (b >> 32);
+    word Car = (pM1 & 0xFFFFFFFF) + (pM2 & 0xFFFFFFFF) + (pL >> 32);
+    r[0] = pL;
+    r[1] = pH + (pM1 >> 32) + (pM2 >> 32) + (Car >> 32);
+}
+void Sbc_SimMult( word A[64], word B[64], word R[64][2] )
+{
+    word a, b, r[2]; int i, k;
+    for ( i = 0; i < 64; i++ )
+        A[i] = B[i] = R[0][i] = R[1][i] = 0;
+    Gia_ManRandom(1);
+    for ( i = 0; i < 64; i++ )
+    {
+        a = Gia_ManRandom(0);
+        b = Gia_ManRandom(0);        
+        Sbc_Mult( a, b, r );
+        for ( k = 0; k < 64; k++ )
+        {
+            if ( (a >> k) & 1 )     A[k] |= (1 << i);
+            if ( (b >> k) & 1 )     B[k] |= (1 << i);
+            if ( (r[0] >> k) & 1 )  R[0][k] |= (1 << i);
+            if ( (r[1] >> k) & 1 )  R[1][k] |= (1 << i);
+        }
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Sbc_ManDetectMult( Gia_Man_t * p, Vec_Int_t * vIns )
+{
+    int nWords = 1;
+    Vec_Int_t * vNodes = Vec_IntStart( Vec_IntSize(vIns) );
+    Gia_Obj_t * pObj; int i, Entry, nIns = Vec_IntSize(vIns)/2;
+    word A[64], B[64], R[64][2], * pInfoObj;
+
+    // alloc simulation info
+    Vec_Mem_t * vTtMem = Vec_MemAlloc( nWords, 10 );
+    Vec_MemHashAlloc( vTtMem, 10000 );
+    Vec_WrdFreeP( &p->vSims );
+    p->vSims = Vec_WrdStart( Gia_ManObjNum(p) * nWords );
+    p->nSimWords = nWords;
+
+    // prepare simulation manager
+    pInfoObj = Wlc_ObjSim( p, 0 );
+    Vec_MemHashInsert( vTtMem, pInfoObj );
+    Gia_ObjSetTravIdCurrentId( p, 0 );
+    Gia_ManForEachCi( p, pObj, i )
+        Gia_ObjSetTravIdCurrent( p, pObj );
+    // set internal nodes
+    assert( Vec_IntSize(vIns) % 2 );
+    Sbc_SimMult( A, B, R );
+    Gia_ManIncrementTravId( p );
+    Gia_ManForEachObjVec( vIns, p, pObj, i )
+    {
+        Gia_ObjSetTravIdCurrent( p, pObj );
+        pInfoObj = Wlc_ObjSim( p, Gia_ObjId(p, pObj) );
+        *pInfoObj = i < nIns ? A[i] : B[nIns-i];
+    }
+    // perform simulation
+    Gia_ManForEachObj1( p, pObj, i )
+    {
+        if ( Gia_ObjIsTravIdCurrent(p, pObj) )
+            continue;
+        if ( Gia_ObjIsAnd(pObj) )
+            Wlc_ObjSimAnd( p, i );
+        else if ( Gia_ObjIsCo(pObj) )
+            Wlc_ObjSimCo( p, i );
+        else assert( 0 );
+
+        // mark each first node
+        pInfoObj = Wlc_ObjSim( p, i );
+        Entry = *Vec_MemHashLookup( vTtMem, pInfoObj );
+        if ( Entry > 0 )
+        {
+            if ( Vec_IntEntry(vNodes, Entry) == 0 ) // new
+                Vec_IntWriteEntry( vNodes, Entry, Abc_Var2Lit(i, 0) );
+            continue;
+        }
+        Abc_TtNot( pInfoObj, nWords );
+        Entry = *Vec_MemHashLookup( vTtMem, pInfoObj );
+        Abc_TtNot( pInfoObj, nWords );
+        if ( Entry > 0 )
+        {
+            if ( Vec_IntEntry(vNodes, Entry) == 0 ) // new
+                Vec_IntWriteEntry( vNodes, Entry, Abc_Var2Lit(i, 1) );
+            continue;
+        }
+    }
+    // cleanup
+    Vec_MemHashFree( vTtMem );
+    Vec_MemFreeP( &vTtMem );
+    Vec_WrdFreeP( &p->vSims );
+    p->nSimWords = 0;
+    return vNodes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sbc_ManDetectMultTest( Gia_Man_t * p )
+{
+    extern Vec_Int_t * Sdb_StoComputeCutsDetect( Gia_Man_t * pGia );
+
+    Vec_Int_t * vIns = Sdb_StoComputeCutsDetect( p );
+    Vec_Int_t * vNodes = Sbc_ManDetectMult( p, vIns );
+
+    Vec_IntPrint( vNodes );
+
+    Vec_IntFree( vNodes );
+    Vec_IntFree( vIns );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/proof/acec/acec2Mult.c b/src/proof/acec/acec2Mult.c
index 62fd1279..d54ed007 100644
--- a/src/proof/acec/acec2Mult.c
+++ b/src/proof/acec/acec2Mult.c
@@ -24,7 +24,128 @@
 
 ABC_NAMESPACE_IMPL_START
 
-static unsigned s_FuncTruths[1920] = {
+
+static int s_nFuncTruths4a = 192; // 0xACC0 -- F(a=0)  <== useful
+static unsigned s_FuncTruths4a[192] = {
+0xACC0, 0xCAA0, 0xB8C0, 0xE288, 0xE488, 0xD8A0, 0xBC80, 0xE828, 0xE848, 0xDA80, 0xE680, 0xE860,
+0x5CC0, 0x3AA0, 0x74C0, 0x2E88, 0x4E88, 0x72A0, 0x7C40, 0x28E8, 0x48E8, 0x7A20, 0x6E08, 0x60E8,
+0xA330, 0xC550, 0x8B0C, 0xD144, 0xB122, 0x8D0A, 0x80BC, 0xD414, 0xB212, 0x80DA, 0x80E6, 0x8E06,
+0x5330, 0x3550, 0x470C, 0x1D44, 0x1B22, 0x270A, 0x407C, 0x14D4, 0x12B2, 0x207A, 0x086E, 0x068E,
+0xCA0C, 0xAC0A, 0xE230, 0xB822, 0xD844, 0xE450, 0xC0AC, 0xA0CA, 0xE320, 0xB282, 0xD484, 0xE540,
+0xCB08, 0x8E82, 0xC0B8, 0x88E2, 0xD940, 0xD490, 0x8E84, 0xAD08, 0xB290, 0xB920, 0x88E4, 0xA0D8,
+0xC50C, 0xA30A, 0xD130, 0x8B22, 0x8D44, 0xB150, 0xC05C, 0xA03A, 0xD310, 0x82B2, 0x84D4, 0xB510,
+0xC704, 0x828E, 0xC074, 0x882E, 0x9D04, 0x90D4, 0x848E, 0xA702, 0x90B2, 0x9B02, 0x884E, 0xA072,
+0xC5FC, 0xA3FA, 0xD1FC, 0x8BEE, 0x8DEE, 0xB1FA, 0xCF5C, 0xAF3A, 0xDF1C, 0x8EBE, 0x8EDE, 0xBF1A,
+0xF734, 0xB2BE, 0xF374, 0xBB2E, 0xBF26, 0xB2F6, 0xD4DE, 0xF752, 0xD4F6, 0xDF46, 0xDD4E, 0xF572,
+0xCAFC, 0xACFA, 0xE2FC, 0xB8EE, 0xD8EE, 0xE4FA, 0xCFAC, 0xAFCA, 0xEF2C, 0xBE8E, 0xDE8E, 0xEF4A,
+0xFB38, 0xBEB2, 0xF3B8, 0xBBE2, 0xFB62, 0xF6B2, 0xDED4, 0xFD58, 0xF6D4, 0xFD64, 0xDDE4, 0xF5D8,
+0x0CCA, 0x0AAC, 0x30E2, 0x22B8, 0x44D8, 0x50E4, 0x3E02, 0x2B28, 0x4D48, 0x5E04, 0x7610, 0x7160,
+0xF33A, 0xF55C, 0xCF2E, 0xDD74, 0xBB72, 0xAF4E, 0xC2FE, 0xD7D4, 0xB7B2, 0xA4FE, 0x98FE, 0x9F8E,
+0x033A, 0x055C, 0x032E, 0x1174, 0x1172, 0x054E, 0x023E, 0x1714, 0x1712, 0x045E, 0x1076, 0x1706,
+0xFCCA, 0xFAAC, 0xFCE2, 0xEEB8, 0xEED8, 0xFAE4, 0xFEC2, 0xEBE8, 0xEDE8, 0xFEA4, 0xFE98, 0xF9E8
+};
+
+
+/*
+static int s_nFuncTruths4 = 192; // 0xF335 -- F(a=1)
+static unsigned s_FuncTruths4[192] = {
+0x0CCA, 0x0AAC, 0x30E2, 0x22B8, 0x44D8, 0x50E4, 0x3E02, 0x2B28, 0x4D48, 0x5E04, 0x7610, 0x7160,
+0xF33A, 0xF55C, 0xCF2E, 0xDD74, 0xBB72, 0xAF4E, 0xC2FE, 0xD7D4, 0xB7B2, 0xA4FE, 0x98FE, 0x9F8E,
+0x033A, 0x055C, 0x032E, 0x1174, 0x1172, 0x054E, 0x023E, 0x1714, 0x1712, 0x045E, 0x1076, 0x1706,
+0xFCCA, 0xFAAC, 0xFCE2, 0xEEB8, 0xEED8, 0xFAE4, 0xFEC2, 0xEBE8, 0xEDE8, 0xFEA4, 0xFE98, 0xF9E8,
+0xC0AC, 0xA0CA, 0xC0B8, 0x88E2, 0x88E4, 0xA0D8, 0xCA0C, 0xAC0A, 0xCB08, 0x8E82, 0x8E84, 0xAD08,
+0xE320, 0xB282, 0xE230, 0xB822, 0xB920, 0xB290, 0xD484, 0xE540, 0xD490, 0xD940, 0xD844, 0xE450,
+0xC05C, 0xA03A, 0xC074, 0x882E, 0x884E, 0xA072, 0xC50C, 0xA30A, 0xC704, 0x828E, 0x848E, 0xA702,
+0xD310, 0x82B2, 0xD130, 0x8B22, 0x9B02, 0x90B2, 0x84D4, 0xB510, 0x90D4, 0x9D04, 0x8D44, 0xB150,
+0xCF5C, 0xAF3A, 0xF374, 0xBB2E, 0xDD4E, 0xF572, 0xC5FC, 0xA3FA, 0xF734, 0xB2BE, 0xD4DE, 0xF752,
+0xDF1C, 0x8EBE, 0xD1FC, 0x8BEE, 0xDF46, 0xD4F6, 0x8EDE, 0xBF1A, 0xB2F6, 0xBF26, 0x8DEE, 0xB1FA,
+0xCFAC, 0xAFCA, 0xF3B8, 0xBBE2, 0xDDE4, 0xF5D8, 0xCAFC, 0xACFA, 0xFB38, 0xBEB2, 0xDED4, 0xFD58,
+0xEF2C, 0xBE8E, 0xE2FC, 0xB8EE, 0xFD64, 0xF6D4, 0xDE8E, 0xEF4A, 0xF6B2, 0xFB62, 0xD8EE, 0xE4FA,
+0xACC0, 0xCAA0, 0xB8C0, 0xE288, 0xE488, 0xD8A0, 0xBC80, 0xE828, 0xE848, 0xDA80, 0xE680, 0xE860,
+0x5CC0, 0x3AA0, 0x74C0, 0x2E88, 0x4E88, 0x72A0, 0x7C40, 0x28E8, 0x48E8, 0x7A20, 0x6E08, 0x60E8,
+0xA330, 0xC550, 0x8B0C, 0xD144, 0xB122, 0x8D0A, 0x80BC, 0xD414, 0xB212, 0x80DA, 0x80E6, 0x8E06,
+0x5330, 0x3550, 0x470C, 0x1D44, 0x1B22, 0x270A, 0x407C, 0x14D4, 0x12B2, 0x207A, 0x086E, 0x068E
+};
+*/
+
+static int s_nFuncTruths4b = 48; // 0xF3C0 -- F(a=b)  <== useful
+static unsigned s_FuncTruths4b[48] = {
+0xF3C0, 0xF5A0, 0xCFC0, 0xDD88, 0xBB88, 0xAFA0, 0xFC30, 0xFA50, 0xCCF0, 0xD8D8, 0xB8B8, 0xAAF0,
+0xF0CC, 0xE4E4, 0xFC0C, 0xEE44, 0xAACC, 0xACAC, 0xE2E2, 0xF0AA, 0xCACA, 0xCCAA, 0xEE22, 0xFA0A,
+0x3F0C, 0x5F0A, 0x3F30, 0x7722, 0x7744, 0x5F50, 0x30FC, 0x50FA, 0x33F0, 0x7272, 0x7474, 0x55F0,
+0x0FCC, 0x4E4E, 0x0CFC, 0x44EE, 0x55CC, 0x5C5C, 0x2E2E, 0x0FAA, 0x3A3A, 0x33AA, 0x22EE, 0x0AFA
+};
+
+/*
+static int s_nFuncTruths4 = 12; // 0x35AC -- F(a!=b)
+static unsigned s_FuncTruths4[12] = {
+0x35AC, 0x53CA, 0x1DB8, 0x47E2, 0x27E4, 0x1BD8, 0x3A5C, 0x5C3A, 0x4E72, 0x2E74, 0x724E, 0x742E
+};
+*/
+
+static int s_nFuncTruths4 = 384; // 0x35C0 -- F(b=0, c=0)  <== useful
+static unsigned s_FuncTruths4[384] = {
+0x35C0, 0x53A0, 0x1DC0, 0x4788, 0x2788, 0x1BA0, 0x3C50, 0x5A30, 0x1CD0, 0x4878, 0x2878, 0x1AB0,
+0x34C4, 0x606C, 0x3C44, 0x660C, 0x268C, 0x286C, 0x606A, 0x52A2, 0x486A, 0x468A, 0x660A, 0x5A22,
+0x3AC0, 0x5CA0, 0x2EC0, 0x7488, 0x7288, 0x4EA0, 0x3CA0, 0x5AC0, 0x2CE0, 0x7848, 0x7828, 0x4AE0,
+0x38C8, 0x6C60, 0x3C88, 0x66C0, 0x62C8, 0x6C28, 0x6A60, 0x58A8, 0x6A48, 0x64A8, 0x66A0, 0x5A88,
+0xC530, 0xA350, 0xD10C, 0x8B44, 0x8D22, 0xB10A, 0xC350, 0xA530, 0xD01C, 0x84B4, 0x82D2, 0xB01A,
+0xC434, 0x909C, 0xC344, 0x990C, 0x8C26, 0x82C6, 0x909A, 0xA252, 0x84A6, 0x8A46, 0x990A, 0xA522,
+0xCA30, 0xAC50, 0xE20C, 0xB844, 0xD822, 0xE40A, 0xC3A0, 0xA5C0, 0xE02C, 0xB484, 0xD282, 0xE04A,
+0xC838, 0x9C90, 0xC388, 0x99C0, 0xC862, 0xC682, 0x9A90, 0xA858, 0xA684, 0xA864, 0x99A0, 0xA588,
+0x530C, 0x350A, 0x4730, 0x1D22, 0x1B44, 0x2750, 0x503C, 0x305A, 0x4370, 0x12D2, 0x14B4, 0x2570,
+0x434C, 0x06C6, 0x443C, 0x0C66, 0x194C, 0x149C, 0x06A6, 0x252A, 0x129A, 0x192A, 0x0A66, 0x225A,
+0xA30C, 0xC50A, 0x8B30, 0xD122, 0xB144, 0x8D50, 0xA03C, 0xC05A, 0x83B0, 0xD212, 0xB414, 0x85D0,
+0x838C, 0xC606, 0x883C, 0xC066, 0x91C4, 0x9C14, 0xA606, 0x858A, 0x9A12, 0x91A2, 0xA066, 0x885A,
+0xA3FC, 0xC5FA, 0x8BFC, 0xD1EE, 0xB1EE, 0x8DFA, 0xAF3C, 0xCF5A, 0x8FBC, 0xDE1E, 0xBE1E, 0x8FDA,
+0xB3BC, 0xF636, 0xBB3C, 0xF366, 0xB3E6, 0xBE36, 0xF656, 0xD5DA, 0xDE56, 0xD5E6, 0xF566, 0xDD5A,
+0x53FC, 0x35FA, 0x47FC, 0x1DEE, 0x1BEE, 0x27FA, 0x5F3C, 0x3F5A, 0x4F7C, 0x1EDE, 0x1EBE, 0x2F7A,
+0x737C, 0x36F6, 0x773C, 0x3F66, 0x3B6E, 0x36BE, 0x56F6, 0x757A, 0x56DE, 0x5D6E, 0x5F66, 0x775A,
+0x3FCA, 0x5FAC, 0x3FE2, 0x77B8, 0x77D8, 0x5FE4, 0x3CFA, 0x5AFC, 0x3EF2, 0x7B78, 0x7D78, 0x5EF4,
+0x3ECE, 0x6F6C, 0x3CEE, 0x66FC, 0x76DC, 0x7D6C, 0x6F6A, 0x5EAE, 0x7B6A, 0x76BA, 0x66FA, 0x5AEE,
+0xC03A, 0xA05C, 0xC02E, 0x8874, 0x8872, 0xA04E, 0xC30A, 0xA50C, 0xC20E, 0x8784, 0x8782, 0xA40E,
+0xC232, 0x9390, 0xC322, 0x9930, 0x9832, 0x9382, 0x9590, 0xA454, 0x9584, 0x9854, 0x9950, 0xA544,
+0xCF3A, 0xAF5C, 0xF32E, 0xBB74, 0xDD72, 0xF54E, 0xC3FA, 0xA5FC, 0xF23E, 0xB7B4, 0xD7D2, 0xF45E,
+0xCE3E, 0x9F9C, 0xC3EE, 0x99FC, 0xDC76, 0xD7C6, 0x9F9A, 0xAE5E, 0xB7A6, 0xBA76, 0x99FA, 0xA5EE,
+0x30CA, 0x50AC, 0x0CE2, 0x44B8, 0x22D8, 0x0AE4, 0x3C0A, 0x5A0C, 0x0EC2, 0x4B48, 0x2D28, 0x0EA4,
+0x32C2, 0x6360, 0x3C22, 0x6630, 0x3298, 0x3928, 0x6560, 0x54A4, 0x5948, 0x5498, 0x6650, 0x5A44,
+0xF3AC, 0xF5CA, 0xCFB8, 0xDDE2, 0xBBE4, 0xAFD8, 0xFA3C, 0xFC5A, 0xCBF8, 0xDED2, 0xBEB4, 0xADF8,
+0xE3EC, 0xF6C6, 0xEE3C, 0xFC66, 0xB9EC, 0xBE9C, 0xF6A6, 0xE5EA, 0xDE9A, 0xD9EA, 0xFA66, 0xEE5A,
+0xF35C, 0xF53A, 0xCF74, 0xDD2E, 0xBB4E, 0xAF72, 0xF53C, 0xF35A, 0xC7F4, 0xD2DE, 0xB4BE, 0xA7F2,
+0xD3DC, 0xC6F6, 0xDD3C, 0xCF66, 0x9BCE, 0x9CBE, 0xA6F6, 0xB5BA, 0x9ADE, 0x9DAE, 0xAF66, 0xBB5A,
+0x035C, 0x053A, 0x0374, 0x112E, 0x114E, 0x0572, 0x053C, 0x035A, 0x0734, 0x121E, 0x141E, 0x0752,
+0x131C, 0x0636, 0x113C, 0x0366, 0x1346, 0x1436, 0x0656, 0x151A, 0x1256, 0x1526, 0x0566, 0x115A,
+0x03AC, 0x05CA, 0x03B8, 0x11E2, 0x11E4, 0x05D8, 0x0A3C, 0x0C5A, 0x0B38, 0x1E12, 0x1E14, 0x0D58,
+0x232C, 0x3606, 0x223C, 0x3066, 0x3164, 0x3614, 0x5606, 0x454A, 0x5612, 0x5162, 0x5066, 0x445A
+};
+
+/*
+static int s_nFuncTruths4 = 96; // 0xFD80 -- F(d=0)
+static unsigned s_FuncTruths4[96] = {
+0xFD80, 0xFB80, 0xEF80, 0xF8D0, 0xF8B0, 0xE8F0, 0xECC4, 0xE8CC, 0xEC8C, 0xE8AA, 0xEAA2, 0xEA8A,
+0xFE40, 0xFE20, 0xFE08, 0xF4E0, 0xF2E0, 0xF0E8, 0xDCC8, 0xCCE8, 0xCEC8, 0xAAE8, 0xBAA8, 0xAEA8,
+0xF720, 0xF740, 0xDF08, 0xDF40, 0xBF20, 0xBF08, 0xF270, 0xF470, 0xD0F8, 0xD4F0, 0xB2F0, 0xB0F8,
+0xC4EC, 0xD4CC, 0xCE4C, 0xDC4C, 0x8CEC, 0x8ECC, 0xB2AA, 0xA2EA, 0x8EAA, 0x8AEA, 0xBA2A, 0xAE2A,
+0xFB10, 0xFD10, 0xEF04, 0xFD04, 0xFB02, 0xEF02, 0xF1B0, 0xF1D0, 0xE0F4, 0xF0D4, 0xF0B2, 0xE0F2,
+0xC8DC, 0xCCD4, 0xCD8C, 0xCDC4, 0xC8CE, 0xCC8E, 0xAAB2, 0xA8BA, 0xAA8E, 0xA8AE, 0xABA2, 0xAB8A,
+0x7F02, 0x7F04, 0x7F10, 0x70F2, 0x70F4, 0x71F0, 0x4CCE, 0x4DCC, 0x4CDC, 0x2BAA, 0x2AAE, 0x2ABA,
+0x40FE, 0x20FE, 0x08FE, 0x4F0E, 0x2F0E, 0x0F8E, 0x7332, 0x33B2, 0x3B32, 0x55D4, 0x7554, 0x5D54,
+};
+*/
+
+/*
+static int s_nFuncTruths4 = 48; // 0xD728 -- F(e=0)
+static unsigned s_FuncTruths4[48] = {
+0xD728, 0xB748, 0x9F60, 0xD278, 0xB478, 0x96F0, 0xC66C, 0x96CC, 0x9C6C, 0x96AA, 0xA66A, 0x9A6A,
+0xEB14, 0xED12, 0xF906, 0xE1B4, 0xE1D2, 0xF096, 0xC99C, 0xCC96, 0xC9C6, 0xAA96, 0xA99A, 0xA9A6,
+0x7D82, 0x7B84, 0x6F90, 0x78D2, 0x78B4, 0x69F0, 0x6CC6, 0x69CC, 0x6C9C, 0x69AA, 0x6AA6, 0x6A9A,
+0x41BE, 0x21DE, 0x09F6, 0x4B1E, 0x2D1E, 0x0F96, 0x6336, 0x3396, 0x3936, 0x5596, 0x6556, 0x5956
+};
+*/
+
+
+static int s_nFuncTruths5 = 960; // 0xF335ACC0
+static unsigned s_FuncTruths5[960] = {
 0xF335ACC0, 0xF553CAA0, 0xCF1DB8C0, 0xDD47E288, 0xBB27E488, 0xAF1BD8A0, 0xC1FDBC80, 0xD4D7E828,
 0xB2B7E848, 0xA1FBDA80, 0x89EFE680, 0x8E9FE860, 0xF3AC35C0, 0xF5CA53A0, 0xCFB81DC0, 0xDDE24788,
 0xBBE42788, 0xAFD81BA0, 0xC1BCFD80, 0xD4E8D728, 0xB2E8B748, 0xA1DAFB80, 0x89E6EF80, 0x8EE89F60,
@@ -32,29 +153,14 @@ static unsigned s_FuncTruths[1920] = {
 0xBEB42878, 0xADF81AB0, 0x8EE896F0, 0x8E96E8F0, 0xE334ECC4, 0xF660C66C, 0xEE3C3C44, 0xFC66660C,
 0xB926EC8C, 0xBE289C6C, 0xE3EC34C4, 0xF6C6606C, 0xB296E8CC, 0xB2E896CC, 0xB9EC268C, 0xBE9C286C,
 0xF660A66A, 0xE552EAA2, 0xDE489A6A, 0xD946EA8A, 0xFA66660A, 0xEE5A5A22, 0xD4E896AA, 0xD496E8AA,
-0xF6A6606A, 0xE5EA52A2, 0xD9EA468A, 0xDE9A486A, 0x0CCA533F, 0x0AAC355F, 0x30E2473F, 0x22B81D77,
-0x44D81B77, 0x50E4275F, 0x3E02437F, 0x2B2817D7, 0x4D4817B7, 0x5E04257F, 0x7610197F, 0x7160179F,
-0x0C53CA3F, 0x0A35AC5F, 0x3047E23F, 0x221DB877, 0x441BD877, 0x5027E45F, 0x3E43027F, 0x2B1728D7,
-0x4D1748B7, 0x5E25047F, 0x7619107F, 0x7117609F, 0x05C3C3AF, 0x03A5A5CF, 0x34E3072F, 0x21B72D87,
-0x41D74B87, 0x52E5074F, 0x3407E32F, 0x212DB787, 0x414BD787, 0x5207E54F, 0x7117690F, 0x7169170F,
-0x1CCB133B, 0x099F3993, 0x11C3C3BB, 0x039999F3, 0x46D91373, 0x41D76393, 0x1C13CB3B, 0x09399F93,
-0x4D691733, 0x4D176933, 0x4613D973, 0x4163D793, 0x099F5995, 0x1AAD155D, 0x21B76595, 0x26B91575,
-0x059999F5, 0x11A5A5DD, 0x2B176955, 0x2B691755, 0x09599F95, 0x1A15AD5D, 0x2615B975, 0x2165B795,
-0xF33A5CC0, 0xF55C3AA0, 0xCF2E74C0, 0xDD742E88, 0xBB724E88, 0xAF4E72A0, 0xC2FE7C40, 0xD7D428E8,
-0xB7B248E8, 0xA4FE7A20, 0x98FE6E08, 0x9F8E60E8, 0xF35C3AC0, 0xF53A5CA0, 0xCF742EC0, 0xDD2E7488,
-0xBB4E7288, 0xAF724EA0, 0xC27CFE40, 0xD728D4E8, 0xB748B2E8, 0xA47AFE20, 0x986EFE08, 0x9F608EE8,
-0xF53C3CA0, 0xF35A5AC0, 0xC72CF4E0, 0xD278DE48, 0xB478BE28, 0xA74AF2E0, 0xC7F42CE0, 0xD2DE7848,
-0xB4BE7828, 0xA7F24AE0, 0x96F08EE8, 0x968EF0E8, 0xD338DCC8, 0xC66CF660, 0xDD3C3C88, 0xCF6666C0,
-0x9B62CEC8, 0x9C6CBE28, 0xD3DC38C8, 0xC6F66C60, 0x96B2CCE8, 0x96CCB2E8, 0x9BCE62C8, 0x9CBE6C28,
-0xA66AF660, 0xB558BAA8, 0x9A6ADE48, 0x9D64AEA8, 0xAF6666A0, 0xBB5A5A88, 0x96AAD4E8, 0x96D4AAE8,
-0xA6F66A60, 0xB5BA58A8, 0x9DAE64A8, 0x9ADE6A48, 0x0CC5A33F, 0x0AA3C55F, 0x30D18B3F, 0x228BD177,
-0x448DB177, 0x50B18D5F, 0x3D0183BF, 0x282BD717, 0x484DB717, 0x5B0185DF, 0x670191F7, 0x60719F17,
-0x0CA3C53F, 0x0AC5A35F, 0x308BD13F, 0x22D18B77, 0x44B18D77, 0x508DB15F, 0x3D8301BF, 0x28D72B17,
-0x48B74D17, 0x5B8501DF, 0x679101F7, 0x609F7117, 0x0AC3C35F, 0x0CA5A53F, 0x38D30B1F, 0x2D8721B7,
-0x4B8741D7, 0x58B50D1F, 0x380BD31F, 0x2D2187B7, 0x4B4187D7, 0x580DB51F, 0x690F7117, 0x69710F17,
-0x2CC72337, 0x3993099F, 0x22C3C377, 0x3099993F, 0x649D3137, 0x639341D7, 0x2C23C737, 0x3909939F,
-0x694D3317, 0x69334D17, 0x64319D37, 0x634193D7, 0x5995099F, 0x4AA74557, 0x659521B7, 0x629B5157,
-0x5099995F, 0x44A5A577, 0x69552B17, 0x692B5517, 0x5909959F, 0x4A45A757, 0x62519B57, 0x652195B7,
+0xF6A6606A, 0xE5EA52A2, 0xD9EA468A, 0xDE9A486A, 0xF33A5CC0, 0xF55C3AA0, 0xCF2E74C0, 0xDD742E88,
+0xBB724E88, 0xAF4E72A0, 0xC2FE7C40, 0xD7D428E8, 0xB7B248E8, 0xA4FE7A20, 0x98FE6E08, 0x9F8E60E8,
+0xF35C3AC0, 0xF53A5CA0, 0xCF742EC0, 0xDD2E7488, 0xBB4E7288, 0xAF724EA0, 0xC27CFE40, 0xD728D4E8,
+0xB748B2E8, 0xA47AFE20, 0x986EFE08, 0x9F608EE8, 0xF53C3CA0, 0xF35A5AC0, 0xC72CF4E0, 0xD278DE48,
+0xB478BE28, 0xA74AF2E0, 0xC7F42CE0, 0xD2DE7848, 0xB4BE7828, 0xA7F24AE0, 0x96F08EE8, 0x968EF0E8,
+0xD338DCC8, 0xC66CF660, 0xDD3C3C88, 0xCF6666C0, 0x9B62CEC8, 0x9C6CBE28, 0xD3DC38C8, 0xC6F66C60,
+0x96B2CCE8, 0x96CCB2E8, 0x9BCE62C8, 0x9CBE6C28, 0xA66AF660, 0xB558BAA8, 0x9A6ADE48, 0x9D64AEA8,
+0xAF6666A0, 0xBB5A5A88, 0x96AAD4E8, 0x96D4AAE8, 0xA6F66A60, 0xB5BA58A8, 0x9DAE64A8, 0x9ADE6A48,
 0xFCC5A330, 0xFAA3C550, 0xFCD18B0C, 0xEE8BD144, 0xEE8DB122, 0xFAB18D0A, 0xFDC180BC, 0xE8EBD414,
 0xE8EDB212, 0xFBA180DA, 0xEF8980E6, 0xE8F98E06, 0xFCA3C530, 0xFAC5A350, 0xFC8BD10C, 0xEED18B44,
 0xEEB18D22, 0xFA8DB10A, 0xFD80C1BC, 0xE8D4EB14, 0xE8B2ED12, 0xFB80A1DA, 0xEF8089E6, 0xE88EF906,
@@ -62,29 +168,14 @@ static unsigned s_FuncTruths[1920] = {
 0xEBE182D2, 0xF8ADB01A, 0xE88EF096, 0xE8F08E96, 0xECC4E334, 0xF990C99C, 0xEEC3C344, 0xFC99990C,
 0xEC8CB926, 0xEB82C9C6, 0xECE3C434, 0xF9C9909C, 0xE8CCB296, 0xE8B2CC96, 0xECB98C26, 0xEBC982C6,
 0xF990A99A, 0xEAA2E552, 0xED84A9A6, 0xEA8AD946, 0xFA99990A, 0xEEA5A522, 0xE8D4AA96, 0xE8AAD496,
-0xF9A9909A, 0xEAE5A252, 0xEAD98A46, 0xEDA984A6, 0x033A5CCF, 0x055C3AAF, 0x032E74F3, 0x11742EBB,
-0x11724EDD, 0x054E72F5, 0x023E7F43, 0x17142BEB, 0x17124DED, 0x045E7F25, 0x10767F19, 0x170671F9,
-0x035C3ACF, 0x053A5CAF, 0x03742EF3, 0x112E74BB, 0x114E72DD, 0x05724EF5, 0x027F3E43, 0x172B14EB,
-0x174D12ED, 0x047F5E25, 0x107F7619, 0x177106F9, 0x053C3CAF, 0x035A5ACF, 0x072F34E3, 0x127B1E4B,
-0x147D1E2D, 0x074F52E5, 0x07342FE3, 0x121E7B4B, 0x141E7D2D, 0x07524FE5, 0x17710F69, 0x170F7169,
-0x133B1CCB, 0x066F3663, 0x113C3CBB, 0x036666F3, 0x137346D9, 0x147D3639, 0x131C3BCB, 0x06366F63,
-0x17334D69, 0x174D3369, 0x134673D9, 0x14367D39, 0x066F5665, 0x155D1AAD, 0x127B5659, 0x157526B9,
-0x056666F5, 0x115A5ADD, 0x172B5569, 0x17552B69, 0x06566F65, 0x151A5DAD, 0x152675B9, 0x12567B59,
-0xFCCA5330, 0xFAAC3550, 0xFCE2470C, 0xEEB81D44, 0xEED81B22, 0xFAE4270A, 0xFEC2407C, 0xEBE814D4,
-0xEDE812B2, 0xFEA4207A, 0xFE98086E, 0xF9E8068E, 0xFC53CA30, 0xFA35AC50, 0xFC47E20C, 0xEE1DB844,
-0xEE1BD822, 0xFA27E40A, 0xFE40C27C, 0xEB14E8D4, 0xED12E8B2, 0xFE20A47A, 0xFE08986E, 0xF906E88E,
-0xF5C3C3A0, 0xF3A5A5C0, 0xF4E0C72C, 0xE1B4ED84, 0xE1D2EB82, 0xF2E0A74A, 0xF4C7E02C, 0xE1EDB484,
-0xE1EBD282, 0xF2A7E04A, 0xF096E88E, 0xF0E8968E, 0xDCC8D338, 0xC99CF990, 0xDDC3C388, 0xCF9999C0,
-0xCEC89B62, 0xC9C6EB82, 0xDCD3C838, 0xC9F99C90, 0xCCE896B2, 0xCC96E8B2, 0xCE9BC862, 0xC9EBC682,
-0xA99AF990, 0xBAA8B558, 0xA9A6ED84, 0xAEA89D64, 0xAF9999A0, 0xBBA5A588, 0xAA96E8D4, 0xAAE896D4,
-0xA9F99A90, 0xBAB5A858, 0xAE9DA864, 0xA9EDA684, 0x0335ACCF, 0x0553CAAF, 0x031DB8F3, 0x1147E2BB,
-0x1127E4DD, 0x051BD8F5, 0x013DBF83, 0x1417EB2B, 0x1217ED4D, 0x015BDF85, 0x0167F791, 0x0617F971,
-0x03AC35CF, 0x05CA53AF, 0x03B81DF3, 0x11E247BB, 0x11E427DD, 0x05D81BF5, 0x01BF3D83, 0x14EB172B,
-0x12ED174D, 0x01DF5B85, 0x01F76791, 0x06F91771, 0x0A3C3C5F, 0x0C5A5A3F, 0x0B1F38D3, 0x1E4B127B,
-0x1E2D147D, 0x0D1F58B5, 0x0B381FD3, 0x1E124B7B, 0x1E142D7D, 0x0D581FB5, 0x0F691771, 0x0F176971,
-0x23372CC7, 0x3663066F, 0x223C3C77, 0x3066663F, 0x3137649D, 0x3639147D, 0x232C37C7, 0x3606636F,
-0x3317694D, 0x3369174D, 0x3164379D, 0x3614397D, 0x5665066F, 0x45574AA7, 0x5659127B, 0x5157629B,
-0x5066665F, 0x445A5A77, 0x5569172B, 0x5517692B, 0x5606656F, 0x454A57A7, 0x5162579B, 0x5612597B,
+0xF9A9909A, 0xEAE5A252, 0xEAD98A46, 0xEDA984A6, 0xFCCA5330, 0xFAAC3550, 0xFCE2470C, 0xEEB81D44,
+0xEED81B22, 0xFAE4270A, 0xFEC2407C, 0xEBE814D4, 0xEDE812B2, 0xFEA4207A, 0xFE98086E, 0xF9E8068E,
+0xFC53CA30, 0xFA35AC50, 0xFC47E20C, 0xEE1DB844, 0xEE1BD822, 0xFA27E40A, 0xFE40C27C, 0xEB14E8D4,
+0xED12E8B2, 0xFE20A47A, 0xFE08986E, 0xF906E88E, 0xF5C3C3A0, 0xF3A5A5C0, 0xF4E0C72C, 0xE1B4ED84,
+0xE1D2EB82, 0xF2E0A74A, 0xF4C7E02C, 0xE1EDB484, 0xE1EBD282, 0xF2A7E04A, 0xF096E88E, 0xF0E8968E,
+0xDCC8D338, 0xC99CF990, 0xDDC3C388, 0xCF9999C0, 0xCEC89B62, 0xC9C6EB82, 0xDCD3C838, 0xC9F99C90,
+0xCCE896B2, 0xCC96E8B2, 0xCE9BC862, 0xC9EBC682, 0xA99AF990, 0xBAA8B558, 0xA9A6ED84, 0xAEA89D64,
+0xAF9999A0, 0xBBA5A588, 0xAA96E8D4, 0xAAE896D4, 0xA9F99A90, 0xBAB5A858, 0xAE9DA864, 0xA9EDA684,
 0x3F53CA0C, 0x5F35AC0A, 0x3F47E230, 0x771DB822, 0x771BD844, 0x5F27E450, 0x35F3C0AC, 0x53F5A0CA,
 0x34F7E320, 0x717DB282, 0x717BD484, 0x52F7E540, 0x1CDFCB08, 0x4D7D8E82, 0x1DCFC0B8, 0x47DD88E2,
 0x46DFD940, 0x4D6FD490, 0x2B7B8E84, 0x1ABFAD08, 0x2B6FB290, 0x26BFB920, 0x27BB88E4, 0x1BAFA0D8,
@@ -100,21 +191,6 @@ static unsigned s_FuncTruths[1920] = {
 0x6F066AA6, 0x5E25AE2A, 0x7B126A9A, 0x7619BA2A, 0x660AFA66, 0x5A22EE5A, 0x60F66AA6, 0x52E5A2EA,
 0x71B269AA, 0x7169B2AA, 0x606AF6A6, 0x52A2E5EA, 0x4D8E69AA, 0x4D698EAA, 0x48DE6A9A, 0x46D98AEA,
 0x468AD9EA, 0x486ADE9A, 0x6F6A06A6, 0x5EAE252A, 0x7B6A129A, 0x76BA192A, 0x66FA0A66, 0x5AEE225A,
-0xC0AC35F3, 0xA0CA53F5, 0xC0B81DCF, 0x88E247DD, 0x88E427BB, 0xA0D81BAF, 0xCA0C3F53, 0xAC0A5F35,
-0xCB081CDF, 0x8E824D7D, 0x8E842B7B, 0xAD081ABF, 0xE32034F7, 0xB282717D, 0xE2303F47, 0xB822771D,
-0xB92026BF, 0xB2902B6F, 0xD484717B, 0xE54052F7, 0xD4904D6F, 0xD94046DF, 0xD844771B, 0xE4505F27,
-0xC035ACF3, 0xA053CAF5, 0xC01DB8CF, 0x8847E2DD, 0x8827E4BB, 0xA01BD8AF, 0xCA3F0C53, 0xAC5F0A35,
-0xCB1C08DF, 0x8E4D827D, 0x8E2B847B, 0xAD1A08BF, 0xE33420F7, 0xB271827D, 0xE23F3047, 0xB877221D,
-0xB92620BF, 0xB22B906F, 0xD471847B, 0xE55240F7, 0xD44D906F, 0xD94640DF, 0xD877441B, 0xE45F5027,
-0xC3AF05C3, 0xA5CF03A5, 0xC1BC0D8F, 0x84ED872D, 0x82EB874B, 0xA1DA0B8F, 0xC305AFC3, 0xA503CFA5,
-0xC10DBC8F, 0x8487ED2D, 0x8287EB4B, 0xA10BDA8F, 0xE32F3407, 0xB787212D, 0xE3342F07, 0xB721872D,
-0xB22B960F, 0xB2962B0F, 0xD787414B, 0xE54F5207, 0xD4964D0F, 0xD44D960F, 0xD741874B, 0xE5524F07,
-0xC1BC31B3, 0x90F99339, 0xC3BB11C3, 0x99F30399, 0x89E623B3, 0x82EB9363, 0xCB1C3B13, 0x9F099339,
-0xCB3B1C13, 0x9F930939, 0x8E962B33, 0x8E2B9633, 0xC131BCB3, 0x9093F939, 0xC311BBC3, 0x9903F399,
-0x8923E6B3, 0x8293EB63, 0xD4967133, 0xD4719633, 0xD7934163, 0xD9734613, 0xD9467313, 0xD7419363,
-0x90F99559, 0xA1DA51D5, 0x84ED9565, 0x89E645D5, 0x99F50599, 0xA5DD11A5, 0x9F099559, 0xAD1A5D15,
-0x8E4D9655, 0x8E964D55, 0x9F950959, 0xAD5D1A15, 0xB2719655, 0xB2967155, 0xB7219565, 0xB9267515,
-0xB9752615, 0xB7952165, 0x9095F959, 0xA151DAD5, 0x8495ED65, 0x8945E6D5, 0x9905F599, 0xA511DDA5,
 0x3FA3C50C, 0x5FC5A30A, 0x3F8BD130, 0x77D18B22, 0x77B18D44, 0x5F8DB150, 0x3AF3C05C, 0x5CF5A03A,
 0x38FBD310, 0x7D7182B2, 0x7B7184D4, 0x58FDB510, 0x2CEFC704, 0x7D4D828E, 0x2ECFC074, 0x74DD882E,
 0x64FD9D04, 0x6F4D90D4, 0x7B2B848E, 0x4AEFA702, 0x6F2B90B2, 0x62FB9B02, 0x72BB884E, 0x4EAFA072,
@@ -130,36 +206,6 @@ static unsigned s_FuncTruths[1920] = {
 0x6AA66F06, 0x5B85AB8A, 0x6A9A7B12, 0x6791ABA2, 0x66A0AF66, 0x5A88BB5A, 0x6AA660F6, 0x58B5A8BA,
 0x69AA71B2, 0x6971AAB2, 0x6A60A6F6, 0x58A8B5BA, 0x69AA4D8E, 0x694DAA8E, 0x6A9A48DE, 0x649DA8AE,
 0x64A89DAE, 0x6A489ADE, 0x6A6FA606, 0x5BAB858A, 0x6A7B9A12, 0x67AB91A2, 0x66AFA066, 0x5ABB885A,
-0xC05C3AF3, 0xA03A5CF5, 0xC0742ECF, 0x882E74DD, 0x884E72BB, 0xA0724EAF, 0xC50C3FA3, 0xA30A5FC5,
-0xC7042CEF, 0x828E7D4D, 0x848E7B2B, 0xA7024AEF, 0xD31038FB, 0x82B27D71, 0xD1303F8B, 0x8B2277D1,
-0x9B0262FB, 0x90B26F2B, 0x84D47B71, 0xB51058FD, 0x90D46F4D, 0x9D0464FD, 0x8D4477B1, 0xB1505F8D,
-0xC03A5CF3, 0xA05C3AF5, 0xC02E74CF, 0x88742EDD, 0x88724EBB, 0xA04E72AF, 0xC53F0CA3, 0xA35F0AC5,
-0xC72C04EF, 0x827D8E4D, 0x847B8E2B, 0xA74A02EF, 0xD33810FB, 0x827DB271, 0xD13F308B, 0x8B7722D1,
-0x9B6202FB, 0x906FB22B, 0x847BD471, 0xB55810FD, 0x906FD44D, 0x9D6404FD, 0x8D7744B1, 0xB15F508D,
-0xC35F0AC3, 0xA53F0CA5, 0xC27C0E4F, 0x872D84ED, 0x874B82EB, 0xA47A0E2F, 0xC30A5FC3, 0xA50C3FA5,
-0xC20E7C4F, 0x87842DED, 0x87824BEB, 0xA40E7A2F, 0xD31F380B, 0x87B72D21, 0xD3381F0B, 0x872DB721,
-0x960FB22B, 0x96B20F2B, 0x87D74B41, 0xB51F580D, 0x96D40F4D, 0x960FD44D, 0x874BD741, 0xB5581F0D,
-0xC27C3273, 0x933990F9, 0xC37722C3, 0x993F3099, 0x986E323B, 0x936382EB, 0xC72C3723, 0x93399F09,
-0xC7372C23, 0x939F3909, 0x968E332B, 0x96338E2B, 0xC2327C73, 0x939039F9, 0xC32277C3, 0x99303F99,
-0x98326E3B, 0x938263EB, 0x96D43371, 0x9633D471, 0x93D76341, 0x9D376431, 0x9D643731, 0x9363D741,
-0x955990F9, 0xA47A5475, 0x956584ED, 0x986E545D, 0x995F5099, 0xA57744A5, 0x95599F09, 0xA74A5745,
-0x96558E4D, 0x968E554D, 0x959F5909, 0xA7574A45, 0x9655B271, 0x96B25571, 0x9565B721, 0x9B625751,
-0x9B576251, 0x95B76521, 0x959059F9, 0xA4547A75, 0x958465ED, 0x98546E5D, 0x99505F99, 0xA54477A5,
-0xCF5C3A03, 0xAF3A5C05, 0xF3742E03, 0xBB2E7411, 0xDD4E7211, 0xF5724E05, 0xC5FC30A3, 0xA3FA50C5,
-0xF73420E3, 0xB2BE7141, 0xD4DE7121, 0xF75240E5, 0xDF1C08CB, 0x8EBE4D41, 0xD1FC0C8B, 0x8BEE44D1,
-0xDF4640D9, 0xD4F64D09, 0x8EDE2B21, 0xBF1A08AD, 0xB2F62B09, 0xBF2620B9, 0x8DEE22B1, 0xB1FA0A8D,
-0xCF3A5C03, 0xAF5C3A05, 0xF32E7403, 0xBB742E11, 0xDD724E11, 0xF54E7205, 0xC530FCA3, 0xA350FAC5,
-0xF72034E3, 0xB271BE41, 0xD471DE21, 0xF74052E5, 0xDF081CCB, 0x8E4DBE41, 0xD10CFC8B, 0x8B44EED1,
-0xDF4046D9, 0xD44DF609, 0x8E2BDE21, 0xBF081AAD, 0xB22BF609, 0xBF2026B9, 0x8D22EEB1, 0xB10AFA8D,
-0xC350FAC3, 0xA530FCA5, 0xF2703E43, 0xB721B4E1, 0xD741D2E1, 0xF4705E25, 0xC3FA50C3, 0xA5FC30A5,
-0xF23E7043, 0xB7B421E1, 0xD7D241E1, 0xF45E7025, 0xD01CF8CB, 0x84B4EDE1, 0xD0F81CCB, 0x84EDB4E1,
-0xD44DF069, 0xD4F04D69, 0x82D2EBE1, 0xB01AF8AD, 0xB2F02B69, 0xB22BF069, 0x82EBD2E1, 0xB0F81AAD,
-0xCE4C3E43, 0x9F099CC9, 0xC344EEC3, 0x990CFC99, 0xDC4C7619, 0xD741C6C9, 0xC4EC34E3, 0x90F99CC9,
-0xC434ECE3, 0x909CF9C9, 0xD4CC7169, 0xD471CC69, 0xCE3E4C43, 0x9F9C09C9, 0xC3EE44C3, 0x99FC0C99,
-0xDC764C19, 0xD7C641C9, 0x8ECC2B69, 0x8E2BCC69, 0x82C6EBC9, 0x8C26ECB9, 0x8CEC26B9, 0x82EBC6C9,
-0x9F099AA9, 0xAE2A5E25, 0xB721A6A9, 0xBA2A7619, 0x990AFA99, 0xA522EEA5, 0x90F99AA9, 0xA2EA52E5,
-0xB271AA69, 0xB2AA7169, 0x909AF9A9, 0xA252EAE5, 0x8E4DAA69, 0x8EAA4D69, 0x84EDA6A9, 0x8AEA46D9,
-0x8A46EAD9, 0x84A6EDA9, 0x9F9A09A9, 0xAE5E2A25, 0xB7A621A9, 0xBA762A19, 0x99FA0A99, 0xA5EE22A5,
 0x30A3C5FC, 0x50C5A3FA, 0x0C8BD1FC, 0x44D18BEE, 0x22B18DEE, 0x0A8DB1FA, 0x3A03CF5C, 0x5C05AF3A,
 0x08CBDF1C, 0x4D418EBE, 0x2B218EDE, 0x08ADBF1A, 0x20E3F734, 0x7141B2BE, 0x2E03F374, 0x7411BB2E,
 0x20B9BF26, 0x2B09B2F6, 0x7121D4DE, 0x40E5F752, 0x4D09D4F6, 0x40D9DF46, 0x7211DD4E, 0x4E05F572,
@@ -175,21 +221,6 @@ static unsigned s_FuncTruths[1920] = {
 0x60F66556, 0x51D5A1DA, 0x48DE5956, 0x45D589E6, 0x66F50566, 0x5ADD115A, 0x6F066556, 0x5D15AD1A,
 0x4D8E5596, 0x4D558E96, 0x6F650656, 0x5DAD151A, 0x71B25596, 0x7155B296, 0x7B125956, 0x7515B926,
 0x75B91526, 0x7B591256, 0x6065F656, 0x51A1D5DA, 0x4859DE56, 0x4589D5E6, 0x6605F566, 0x5A11DD5A,
-0xCFAC3503, 0xAFCA5305, 0xF3B81D03, 0xBBE24711, 0xDDE42711, 0xF5D81B05, 0xCAFC3053, 0xACFA5035,
-0xFB3810D3, 0xBEB24171, 0xDED42171, 0xFD5810B5, 0xEF2C04C7, 0xBE8E414D, 0xE2FC0C47, 0xB8EE441D,
-0xFD64049D, 0xF6D4094D, 0xDE8E212B, 0xEF4A02A7, 0xF6B2092B, 0xFB62029B, 0xD8EE221B, 0xE4FA0A27,
-0xCF35AC03, 0xAF53CA05, 0xF31DB803, 0xBB47E211, 0xDD27E411, 0xF51BD805, 0xCA30FC53, 0xAC50FA35,
-0xFB1038D3, 0xBE41B271, 0xDE21D471, 0xFD1058B5, 0xEF042CC7, 0xBE418E4D, 0xE20CFC47, 0xB844EE1D,
-0xFD04649D, 0xF609D44D, 0xDE218E2B, 0xEF024AA7, 0xF609B22B, 0xFB02629B, 0xD822EE1B, 0xE40AFA27,
-0xC3A0F5C3, 0xA5C0F3A5, 0xF1B03D83, 0xB4E1B721, 0xD2E1D741, 0xF1D05B85, 0xC3F5A0C3, 0xA5F3C0A5,
-0xF13DB083, 0xB4B7E121, 0xD2D7E141, 0xF15BD085, 0xE02CF4C7, 0xB484E1ED, 0xE0F42CC7, 0xB4E184ED,
-0xF069D44D, 0xF0D4694D, 0xD282E1EB, 0xE04AF2A7, 0xF0B2692B, 0xF069B22B, 0xD2E182EB, 0xE0F24AA7,
-0xCD8C3D83, 0x9CC99F09, 0xC388DDC3, 0x99C0CF99, 0xCDC46791, 0xC6C9D741, 0xC8DC38D3, 0x9CC990F9,
-0xC838DCD3, 0x9C90C9F9, 0xCCD46971, 0xCC69D471, 0xCD3D8C83, 0x9C9FC909, 0xC3DD88C3, 0x99CFC099,
-0xCD67C491, 0xC6D7C941, 0xCC8E692B, 0xCC698E2B, 0xC682C9EB, 0xC862CE9B, 0xC8CE629B, 0xC6C982EB,
-0x9AA99F09, 0xAB8A5B85, 0xA6A9B721, 0xABA26791, 0x99A0AF99, 0xA588BBA5, 0x9AA990F9, 0xA8BA58B5,
-0xAA69B271, 0xAAB26971, 0x9A90A9F9, 0xA858BAB5, 0xAA698E4D, 0xAA8E694D, 0xA6A984ED, 0xA8AE649D,
-0xA864AE9D, 0xA684A9ED, 0x9A9FA909, 0xAB5B8A85, 0xA6B7A921, 0xAB67A291, 0x99AFA099, 0xA5BB88A5,
 0x3053CAFC, 0x5035ACFA, 0x0C47E2FC, 0x441DB8EE, 0x221BD8EE, 0x0A27E4FA, 0x3503CFAC, 0x5305AFCA,
 0x04C7EF2C, 0x414DBE8E, 0x212BDE8E, 0x02A7EF4A, 0x10D3FB38, 0x4171BEB2, 0x1D03F3B8, 0x4711BBE2,
 0x029BFB62, 0x092BF6B2, 0x2171DED4, 0x10B5FD58, 0x094DF6D4, 0x049DFD64, 0x2711DDE4, 0x1B05F5D8,
@@ -212,22 +243,7 @@ static unsigned s_FuncTruths[1920] = {
 0x14B47D78, 0x25705EF4, 0x177196F0, 0x179671F0, 0x433E4CCE, 0x066FC66C, 0x443C3CEE, 0x0C6666FC,
 0x19764CDC, 0x147D9C6C, 0x434C3ECE, 0x06C66F6C, 0x17964DCC, 0x174D96CC, 0x194C76DC, 0x149C7D6C,
 0x066FA66A, 0x255E2AAE, 0x127B9A6A, 0x19762ABA, 0x0A6666FA, 0x225A5AEE, 0x172B96AA, 0x17962BAA,
-0x06A66F6A, 0x252A5EAE, 0x192A76BA, 0x129A7B6A, 0xACC0F335, 0xCAA0F553, 0xB8C0CF1D, 0xE288DD47,
-0xE488BB27, 0xD8A0AF1B, 0xBC80C1FD, 0xE828D4D7, 0xE848B2B7, 0xDA80A1FB, 0xE68089EF, 0xE8608E9F,
-0xACF3C035, 0xCAF5A053, 0xB8CFC01D, 0xE2DD8847, 0xE4BB8827, 0xD8AFA01B, 0xBCC180FD, 0xE8D428D7,
-0xE8B248B7, 0xDAA180FB, 0xE68980EF, 0xE88E609F, 0xAFC3C305, 0xCFA5A503, 0xBCC18F0D, 0xED842D87,
-0xEB824B87, 0xDAA18F0B, 0xBC8FC10D, 0xED2D8487, 0xEB4B8287, 0xDA8FA10B, 0xE88E690F, 0xE8698E0F,
-0xBCC1B331, 0xF9903993, 0xBBC3C311, 0xF3999903, 0xE689B323, 0xEB826393, 0xBCB3C131, 0xF9399093,
-0xE869B233, 0xE8B26933, 0xE6B38923, 0xEB638293, 0xF9905995, 0xDAA1D551, 0xED846595, 0xE689D545,
-0xF5999905, 0xDDA5A511, 0xE8D46955, 0xE869D455, 0xF9599095, 0xDAD5A151, 0xE6D58945, 0xED658495,
-0xA33F0CC5, 0xC55F0AA3, 0x8B3F30D1, 0xD177228B, 0xB177448D, 0x8D5F50B1, 0x83BF3D01, 0xD717282B,
-0xB717484D, 0x85DF5B01, 0x91F76701, 0x9F176071, 0xA30C3FC5, 0xC50A5FA3, 0x8B303FD1, 0xD122778B,
-0xB144778D, 0x8D505FB1, 0x833DBF01, 0xD728172B, 0xB748174D, 0x855BDF01, 0x9167F701, 0x9F601771,
-0xA03C3CF5, 0xC05A5AF3, 0x833DB0F1, 0xD278127B, 0xB478147D, 0x855BD0F1, 0x83B03DF1, 0xD212787B,
-0xB414787D, 0x85D05BF1, 0x96F01771, 0x9617F071, 0x833D8CCD, 0xC66C066F, 0x883C3CDD, 0xC06666CF,
-0x9167C4CD, 0x9C6C147D, 0x838C3DCD, 0xC6066C6F, 0x9617CC4D, 0x96CC174D, 0x91C467CD, 0x9C146C7D,
-0xA66A066F, 0x855B8AAB, 0x9A6A127B, 0x9167A2AB, 0xA06666AF, 0x885A5ABB, 0x96AA172B, 0x9617AA2B,
-0xA6066A6F, 0x858A5BAB, 0x91A267AB, 0x9A126A7B, 0x5CC0F33A, 0x3AA0F55C, 0x74C0CF2E, 0x2E88DD74,
+0x06A66F6A, 0x252A5EAE, 0x192A76BA, 0x129A7B6A, 0x5CC0F33A, 0x3AA0F55C, 0x74C0CF2E, 0x2E88DD74,
 0x4E88BB72, 0x72A0AF4E, 0x7C40C2FE, 0x28E8D7D4, 0x48E8B7B2, 0x7A20A4FE, 0x6E0898FE, 0x60E89F8E,
 0x5CF3C03A, 0x3AF5A05C, 0x74CFC02E, 0x2EDD8874, 0x4EBB8872, 0x72AFA04E, 0x7CC240FE, 0x28D7E8D4,
 0x48B7E8B2, 0x7AA420FE, 0x6E9808FE, 0x609FE88E, 0x5FC3C30A, 0x3FA5A50C, 0x7CC24F0E, 0x2D87ED84,
@@ -242,22 +258,7 @@ static unsigned s_FuncTruths[1920] = {
 0x41E1D7D2, 0x7025F45E, 0x7117F096, 0x71F01796, 0x4CCE433E, 0x099FC99C, 0x44C3C3EE, 0x0C9999FC,
 0x4CDC1976, 0x41D7C9C6, 0x4C43CE3E, 0x09C99F9C, 0x4DCC1796, 0x4D17CC96, 0x4C19DC76, 0x41C9D7C6,
 0x099FA99A, 0x2AAE255E, 0x21B7A9A6, 0x2ABA1976, 0x0A9999FA, 0x22A5A5EE, 0x2B17AA96, 0x2BAA1796,
-0x09A99F9A, 0x2A25AE5E, 0x2A19BA76, 0x21A9B7A6, 0xA330FCC5, 0xC550FAA3, 0x8B0CFCD1, 0xD144EE8B,
-0xB122EE8D, 0x8D0AFAB1, 0x80BCFDC1, 0xD414E8EB, 0xB212E8ED, 0x80DAFBA1, 0x80E6EF89, 0x8E06E8F9,
-0xA3FC30C5, 0xC5FA50A3, 0x8BFC0CD1, 0xD1EE448B, 0xB1EE228D, 0x8DFA0AB1, 0x80FDBCC1, 0xD4E814EB,
-0xB2E812ED, 0x80FBDAA1, 0x80EFE689, 0x8EE806F9, 0xAF3C3C05, 0xCF5A5A03, 0x8F0DBCC1, 0xDE481E4B,
-0xBE281E2D, 0x8F0BDAA1, 0x8FBC0DC1, 0xDE1E484B, 0xBE1E282D, 0x8FDA0BA1, 0x8EE80F69, 0x8E0FE869,
-0xB331BCC1, 0xF6603663, 0xBB3C3C11, 0xF3666603, 0xB323E689, 0xBE283639, 0xB3BC31C1, 0xF6366063,
-0xB233E869, 0xB2E83369, 0xB3E62389, 0xBE362839, 0xF6605665, 0xD551DAA1, 0xDE485659, 0xD545E689,
-0xF5666605, 0xDD5A5A11, 0xD4E85569, 0xD455E869, 0xF6566065, 0xD5DA51A1, 0xD5E64589, 0xDE564859,
-0xACCF0335, 0xCAAF0553, 0xB8F3031D, 0xE2BB1147, 0xE4DD1127, 0xD8F5051B, 0xBF83013D, 0xEB2B1417,
-0xED4D1217, 0xDF85015B, 0xF7910167, 0xF9710617, 0xAC03CF35, 0xCA05AF53, 0xB803F31D, 0xE211BB47,
-0xE411DD27, 0xD805F51B, 0xBF01833D, 0xEB142B17, 0xED124D17, 0xDF01855B, 0xF7019167, 0xF9067117,
-0xA0C3C3F5, 0xC0A5A5F3, 0xB0F1833D, 0xE1B421B7, 0xE1D241D7, 0xD0F1855B, 0xB083F13D, 0xE121B4B7,
-0xE141D2D7, 0xD085F15B, 0xF0967117, 0xF0719617, 0x8CCD833D, 0xC99C099F, 0x88C3C3DD, 0xC09999CF,
-0xC4CD9167, 0xC9C641D7, 0x8C83CD3D, 0xC9099C9F, 0xCC4D9617, 0xCC964D17, 0xC491CD67, 0xC941C6D7,
-0xA99A099F, 0x8AAB855B, 0xA9A621B7, 0xA2AB9167, 0xA09999AF, 0x88A5A5BB, 0xAA962B17, 0xAA2B9617,
-0xA9099A9F, 0x8A85AB5B, 0xA291AB67, 0xA921A6B7, 0x5330FCCA, 0x3550FAAC, 0x470CFCE2, 0x1D44EEB8,
+0x09A99F9A, 0x2A25AE5E, 0x2A19BA76, 0x21A9B7A6, 0x5330FCCA, 0x3550FAAC, 0x470CFCE2, 0x1D44EEB8,
 0x1B22EED8, 0x270AFAE4, 0x407CFEC2, 0x14D4EBE8, 0x12B2EDE8, 0x207AFEA4, 0x086EFE98, 0x068EF9E8,
 0x53FC30CA, 0x35FA50AC, 0x47FC0CE2, 0x1DEE44B8, 0x1BEE22D8, 0x27FA0AE4, 0x40FE7CC2, 0x14EBD4E8,
 0x12EDB2E8, 0x20FE7AA4, 0x08FE6E98, 0x06F98EE8, 0x5F3C3C0A, 0x3F5A5A0C, 0x4F0E7CC2, 0x1E4BDE48,
@@ -295,6 +296,7 @@ struct Sdb_Sto_t_
     int             nCutSize;
     int             nCutNum;
     int             fCutMin;
+    int             fTruthMin;
     int             fVerbose;
     Gia_Man_t *     pGia;                      // user's AIG manager (will be modified by adding nodes)
     Vec_Int_t *     vRefs;                     // refs for each node
@@ -591,7 +593,8 @@ static inline int Sdb_CutComputeTruth6( Sdb_Sto_t * p, Sdb_Cut_t * pCut0, Sdb_Cu
     t1 = Abc_Tt6Expand( t1, pCut1->pLeaves, pCut1->nLeaves, pCutR->pLeaves, pCutR->nLeaves );
     t =  fIsXor ? t0 ^ t1 : t0 & t1;
     if ( (fCompl = (int)(t & 1)) ) t = ~t;
-    pCutR->nLeaves = Abc_Tt6MinBase( &t, pCutR->pLeaves, pCutR->nLeaves );
+    if ( p->fTruthMin )
+        pCutR->nLeaves = Abc_Tt6MinBase( &t, pCutR->pLeaves, pCutR->nLeaves );
     assert( (int)(t & 1) == 0 );
     truthId        = Vec_MemHashInsert(p->vTtMem, &t);
     pCutR->iFunc   = Abc_Var2Lit( truthId, fCompl );
@@ -617,7 +620,8 @@ static inline int Sdb_CutComputeTruth( Sdb_Sto_t * p, Sdb_Cut_t * pCut0, Sdb_Cut
         Abc_TtXor( uTruth, uTruth0, uTruth1, nWords, (fCompl = (int)((uTruth0[0] ^ uTruth1[0]) & 1)) );
     else
         Abc_TtAnd( uTruth, uTruth0, uTruth1, nWords, (fCompl = (int)((uTruth0[0] & uTruth1[0]) & 1)) );
-    pCutR->nLeaves = Abc_TtMinBase( uTruth, pCutR->pLeaves, pCutR->nLeaves, nCutSize );
+    if ( p->fTruthMin )
+        pCutR->nLeaves = Abc_TtMinBase( uTruth, pCutR->pLeaves, pCutR->nLeaves, nCutSize );
     assert( (uTruth[0] & 1) == 0 );
 //Kit_DsdPrintFromTruth( uTruth, pCutR->nLeaves ), printf("\n" ), printf("\n" );
     truthId        = Vec_MemHashInsert(p->vTtMem, uTruth);
@@ -774,6 +778,167 @@ void Sdb_StoMergeCuts( Sdb_Sto_t * p, int iObj )
         Sdb_CutAddUnit( p, iObj );
 }
 
+
+
+/**Function*************************************************************
+
+  Synopsis    [Cut comparison.]
+
+  Description [Find out if there is a cut in vCuts such that pCut 
+  has only one extra input. If so, return this input.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Sdb_StoDiffExactlyOne( Vec_Wec_t * vCuts, int Limit, int * pCut )
+{
+    Vec_Int_t * vCut;  
+    int i, k, iNew;
+    // check if it is fully contained in any one
+    Vec_WecForEachLevel( vCuts, vCut, i )
+    {
+        for ( k = 1; k <= pCut[0]; k++ )
+            if ( Vec_IntFind(vCut, pCut[k]) == -1 )
+                break;
+        if ( k == pCut[0] + 1 )
+            return -1;
+    }
+    // check if there is one different
+    Vec_WecForEachLevel( vCuts, vCut, i )
+    {
+        if ( i == Limit )
+            break;
+        for ( iNew = -1, k = 1; k <= pCut[0]; k++ )
+        {
+            if ( Vec_IntFind(vCut, pCut[k]) >= 0 )
+                continue;
+            if ( iNew == -1 )
+                iNew = pCut[k];
+            else 
+                break;
+        }
+        if ( k == pCut[0] + 1 && iNew != -1 )
+            return iNew;
+    }
+    return -1;
+}
+int Sdb_StoDiffExactlyOne3( Vec_Wec_t * vCuts, int Limit, int * pCut, int * pCount )
+{
+    Vec_Int_t * vCut;  
+    int i, iNewAll = -1, Count = 0;
+    Vec_WecForEachLevel( vCuts, vCut, i )
+    {
+        int k, iNew = -1;
+        if ( i == Limit )
+            break;
+        for ( k = 1; k <= pCut[0]; k++ )
+        {
+            if ( Vec_IntFind(vCut, pCut[k]) >= 0 )
+                continue;
+            if ( iNew == -1 )
+                iNew = pCut[k];
+            else 
+                break;
+        }
+        if ( k == pCut[0] + 1 && iNew != -1 )
+        {
+            if ( iNewAll == -1 )
+                iNewAll = iNew;
+            if ( iNewAll == iNew )
+                Count++;
+        }
+    }
+    *pCount = Count;
+    return iNewAll;
+}
+Vec_Int_t * Sdb_StoFindAll( Vec_Wec_t * vCuts )
+{
+    int i, k, Entry, iNew = -1;
+    Vec_Int_t * vCut, * vAll = Vec_IntAlloc( 100 );  
+    Vec_WecForEachLevel( vCuts, vCut, i )
+        Vec_IntForEachEntry( vCut, Entry, k )
+            Vec_IntPushUnique( vAll, Entry );
+    return vAll;
+}
+int Sdb_StoDiffExactlyOne2( Vec_Int_t * vAll, int * pCut )
+{
+    int k, iNew = -1;
+    for ( k = 1; k <= pCut[0]; k++ )
+    {
+        if ( Vec_IntFind(vAll, pCut[k]) >= 0 )
+            continue;
+        if ( iNew == -1 )
+            iNew = pCut[k];
+        else 
+            break;
+    }
+    if ( k == pCut[0] + 1 && iNew != -1 )
+        return iNew;
+    return -1;
+}
+Vec_Int_t * Sdb_StoFindInputs( Vec_Wec_t * vCuts, int Front )
+{
+    int fVerbose = 1;
+    Vec_Int_t * vCut, * vCounts;
+    Vec_Int_t * vRes = Vec_IntAlloc( 100 );
+    Vec_Int_t * vResA = Vec_IntAlloc( 100 );
+    Vec_Int_t * vResB = Vec_IntAlloc( 100 );
+    int i, k, Entry, Max = 0, Min, MinValue;
+    // find MAX value
+    Vec_WecForEachLevel( vCuts, vCut, i )
+        Vec_IntForEachEntry( vCut, Entry, k )
+            Max = Abc_MaxInt( Max, Entry );
+    // count how many times each value appears
+    vCounts = Vec_IntStart( Max + 1 );
+    Vec_WecForEachLevel( vCuts, vCut, i )
+        Vec_IntForEachEntry( vCut, Entry, k )
+            Vec_IntAddToEntry( vCounts, Entry, 1 );
+    Vec_IntWriteEntry( vCounts, 0, 0 );
+    // print out
+    if ( fVerbose )
+    Vec_IntForEachEntry( vCounts, Entry, k )
+        if ( Entry )
+            printf( "%5d %5d\n", k, Entry );
+    // collect first part
+    MinValue = ABC_INFINITY;
+    Vec_IntForEachEntry( vCounts, Entry, k )
+        if ( Entry )
+            MinValue = Abc_MinInt( MinValue, Entry );
+    Min = Vec_IntFind( vCounts, MinValue );
+    Vec_IntPush( vResA, Min );
+    Vec_IntWriteEntry( vCounts, Min, 0 );
+    Vec_IntForEachEntry( vCounts, Entry, k )
+        if ( Entry == MinValue || Entry == 2*MinValue )
+        {
+            Vec_IntPush( vResA, k );
+            Vec_IntWriteEntry( vCounts, k, 0 );
+        }
+    // collect second parts
+    MinValue = Vec_IntEntry( vCounts, Front );
+    Min = Front;
+    Vec_IntPush( vResB, Min );
+    Vec_IntWriteEntry( vCounts, Min, 0 );
+    Vec_IntForEachEntry( vCounts, Entry, k )
+        if ( Entry == MinValue || Entry == 2*MinValue )
+        {
+            Vec_IntPush( vResB, k );
+            Vec_IntWriteEntry( vCounts, k, 0 );
+        }
+    Vec_IntFree( vCounts );
+    Vec_IntPrint( vResA );
+    Vec_IntPrint( vResB );
+    // here we need to order the inputs
+
+    // append
+    Vec_IntAppend( vRes, vResA );
+    Vec_IntAppend( vRes, vResB );
+    Vec_IntFree( vResA );
+    Vec_IntFree( vResB );
+    return vRes;
+}
+
 /**Function*************************************************************
 
   Synopsis    [Iterate through the cuts.]
@@ -785,41 +950,152 @@ void Sdb_StoMergeCuts( Sdb_Sto_t * p, int iObj )
   SeeAlso     []
 
 ***********************************************************************/
-int Sdb_StoIterCutsOne( Sdb_Sto_t * p, int iObj )
+int Sdb_StoIterCutsOne( Sdb_Sto_t * p, int iObj, int CutSize, int ** ppCut )
 {
-    int fVerbose = 1;
+    int fVerbose = 0;
     Vec_Int_t * vThis = Vec_WecEntry( p->vCuts, iObj );
     int i, k, * pCut, * pList = Vec_IntArray( vThis );
     word * pTruth;
     Sdb_ForEachCut( pList, pCut, i )
     {
-        if ( pCut[0] != 5 )
+        if ( pCut[0] != CutSize )
             continue;
-        pTruth = Vec_MemReadEntry(p->vTtMem, Abc_Lit2Var(pCut[pCut[0]+1]));
-        for ( k = 0; k < 1920; k++ )
-            if ( s_FuncTruths[k] == (unsigned)*pTruth )
-                break;
-        if ( k < 1920 )
+        if ( pCut[0] == 5 )
         {
-            if ( fVerbose )
+            pTruth = Vec_MemReadEntry(p->vTtMem, Abc_Lit2Var(pCut[pCut[0]+1]));
+            for ( k = 0; k < s_nFuncTruths5; k++ )
+                if ( s_FuncTruths5[k] == (unsigned)*pTruth )
+                    break;
+            if ( k < s_nFuncTruths5 )
             {
-                printf( "Object %d has 5-input cut:  ", iObj );
-                for ( k = 1; k <= pCut[0]; k++ )
-                    printf( "%d ", pCut[k] );
-                printf( "\n" );
+                if ( fVerbose )
+                {
+                    printf( "Object %d has %d-input cut:  ", iObj, pCut[0] );
+                    for ( k = 1; k <= pCut[0]; k++ )
+                        printf( "%d ", pCut[k] );
+                    printf( "\n" );
+                }
+                *ppCut = pCut;
+                return 1; // five-input
+            }
+        }
+        if ( pCut[0] == 4 )
+        {
+            pTruth = Vec_MemReadEntry(p->vTtMem, Abc_Lit2Var(pCut[pCut[0]+1]));
+            for ( k = 0; k < s_nFuncTruths4; k++ )
+                if ( s_FuncTruths4[k] == (0xFFFF & (unsigned)*pTruth) )
+                    break;
+            if ( k < s_nFuncTruths4 )
+            {
+                if ( fVerbose )
+                {
+                    printf( "Object %d has %d-input cut:  ", iObj, pCut[0] );
+                    for ( k = 1; k <= pCut[0]; k++ )
+                        printf( "%d ", pCut[k] );
+                    printf( "\n" );
+                }
+                *ppCut = pCut;
+                return 2; // front
+            }
+        }
+        if ( pCut[0] == 4 )
+        {
+            pTruth = Vec_MemReadEntry(p->vTtMem, Abc_Lit2Var(pCut[pCut[0]+1]));
+            for ( k = 0; k < s_nFuncTruths4a; k++ )
+                if ( s_FuncTruths4a[k] == (0xFFFF & (unsigned)*pTruth) )
+                    break;
+            if ( k < s_nFuncTruths4a )
+            {
+                if ( fVerbose )
+                {
+                    printf( "Object %d has %d-input cut:  ", iObj, pCut[0] );
+                    for ( k = 1; k <= pCut[0]; k++ )
+                        printf( "%d ", pCut[k] );
+                    printf( "\n" );
+                }
+                *ppCut = pCut;
+                return 3; // back unsigned
+            }
+        }
+        if ( pCut[0] == 4 )
+        {
+            pTruth = Vec_MemReadEntry(p->vTtMem, Abc_Lit2Var(pCut[pCut[0]+1]));
+            for ( k = 0; k < s_nFuncTruths4b; k++ )
+                if ( s_FuncTruths4b[k] == (0xFFFF & (unsigned)*pTruth) )
+                    break;
+            if ( k < s_nFuncTruths4b )
+            {
+                if ( fVerbose )
+                {
+                    printf( "Object %d has %d-input cut:  ", iObj, pCut[0] );
+                    for ( k = 1; k <= pCut[0]; k++ )
+                        printf( "%d ", pCut[k] );
+                    printf( "\n" );
+                }
+                *ppCut = pCut;
+                return 4; // back signed
             }
-            return 1;
         }
     }
     return 0;
 }
-void Sdb_StoIterCuts( Sdb_Sto_t * p )
+Vec_Int_t * Sdb_StoIterCuts( Sdb_Sto_t * p )
 {
+    Vec_Wec_t * v5Cuts = Vec_WecAlloc( 100 );
+    Vec_Int_t * v5Cut, * vAll, * vRes;
     Gia_Obj_t * pObj;   
-    int iObj, Count = 0;
+    int k, iObj, * pCut, Limit, iNew, iNewFront = -1, iNewBack = -1, iSigned = 0;
+    Gia_ManForEachAnd( p->pGia, pObj, iObj )
+    {
+        int RetValue = Sdb_StoIterCutsOne( p, iObj, 5, &pCut );
+        if ( RetValue == 0 )
+            continue;
+        assert( RetValue == 1 );
+        assert( pCut[0] == 5 );
+        v5Cut = Vec_WecPushLevel( v5Cuts );
+        for ( k = 1; k <= pCut[0]; k++ )
+            Vec_IntPush( v5Cut, pCut[k] );
+    }
+    Limit = Vec_WecSize( v5Cuts );
+    printf( "Detected %d  5-cuts.\n", Vec_WecSize(v5Cuts) );
+    vAll = Sdb_StoFindAll( v5Cuts );
     Gia_ManForEachAnd( p->pGia, pObj, iObj )
-        Count += Sdb_StoIterCutsOne( p, iObj );
-    printf( "Detected %d cuts.\n", Count );
+    {
+        int RetValue = Sdb_StoIterCutsOne( p, iObj, 4, &pCut );
+        if ( RetValue == 0 )
+            continue;
+        assert( RetValue >= 2 && RetValue <= 4 );
+        assert( pCut[0] == 4 );
+        // find cut, which differs in exactly one input
+        iNew = Sdb_StoDiffExactlyOne( v5Cuts, Limit, pCut );
+        if ( iNew == -1 )
+            continue;
+        if ( RetValue == 2 )
+            iNewFront = iNew;
+        else 
+            iNewBack = iNew;
+        if ( RetValue == 4 )
+            iSigned = 1;
+        // save in the second cut
+        v5Cut = Vec_WecPushLevel( v5Cuts );
+        Vec_IntPush( v5Cut, 0 );
+        for ( k = 1; k <= pCut[0]; k++ )
+            Vec_IntPush( v5Cut, pCut[k] );
+    }
+    Vec_IntFree( vAll );
+    Vec_WecPrint( v5Cuts, 0 );
+
+    if ( iNewFront )
+        printf( "Front  = %d\n", iNewFront );
+    if ( iNewBack )
+        printf( "Back   = %d\n", iNewBack );
+    if ( iSigned )
+        printf( "Sign   = %d\n", iSigned );
+
+    vRes = Sdb_StoFindInputs( v5Cuts, iNewFront );
+
+    Vec_WecFree( v5Cuts );
+    return vRes;
 }
 
 /**Function*************************************************************
@@ -833,22 +1109,23 @@ void Sdb_StoIterCuts( Sdb_Sto_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Sdb_Sto_t * Sdb_StoAlloc( Gia_Man_t * pGia, int nCutSize, int nCutNum, int fCutMin, int fVerbose )
+Sdb_Sto_t * Sdb_StoAlloc( Gia_Man_t * pGia, int nCutSize, int nCutNum, int fCutMin, int fTruthMin, int fVerbose )
 {
     Sdb_Sto_t * p;
     assert( nCutSize < SDB_CUT_NO_LEAF );
     assert( nCutSize > 1 && nCutSize <= SDB_MAX_CUTSIZE );
     assert( nCutNum > 1 && nCutNum < SDB_MAX_CUTNUM );
     p = ABC_CALLOC( Sdb_Sto_t, 1 );
-    p->clkStart = Abc_Clock();
-    p->nCutSize = nCutSize;
-    p->nCutNum  = nCutNum;
-    p->fCutMin  = fCutMin;
-    p->fVerbose = fVerbose;
-    p->pGia     = pGia;
-    p->vRefs    = Vec_IntAlloc( Gia_ManObjNum(pGia) );
-    p->vCuts    = Vec_WecStart( Gia_ManObjNum(pGia) );
-    p->vTtMem   = fCutMin ? Vec_MemAllocForTT( nCutSize, 0 ) : NULL;
+    p->clkStart  = Abc_Clock();
+    p->nCutSize  = nCutSize;
+    p->nCutNum   = nCutNum;
+    p->fCutMin   = fCutMin;
+    p->fTruthMin = fTruthMin;
+    p->fVerbose  = fVerbose;
+    p->pGia      = pGia;
+    p->vRefs     = Vec_IntAlloc( Gia_ManObjNum(pGia) );
+    p->vCuts     = Vec_WecStart( Gia_ManObjNum(pGia) );
+    p->vTtMem    = fCutMin ? Vec_MemAllocForTT( nCutSize, 0 ) : NULL;
     return p;
 }
 void Sdb_StoFree( Sdb_Sto_t * p )
@@ -886,9 +1163,10 @@ void Sdb_StoRefObj( Sdb_Sto_t * p, int iObj )
     else if ( Gia_ObjIsCo(pObj) )
         Vec_IntAddToEntry( p->vRefs, Gia_ObjFaninId0(pObj, iObj), 1 );
 }
-void Sdb_StoComputeCutsTest( Gia_Man_t * pGia )
+Vec_Int_t * Sdb_StoComputeCutsDetect( Gia_Man_t * pGia )
 {
-    Sdb_Sto_t * p = Sdb_StoAlloc( pGia, 6, 20, 1, 1 );
+    Vec_Int_t * vRes = NULL;
+    Sdb_Sto_t * p = Sdb_StoAlloc( pGia, 5, 20, 1, 0, 1 );
     Gia_Obj_t * pObj;   
     int i, iObj;
     // prepare references
@@ -912,11 +1190,15 @@ void Sdb_StoComputeCutsTest( Gia_Man_t * pGia )
         printf( "Over = %4d  ",             p->nCutsOver );
         Abc_PrintTime( 0, "Time", Abc_Clock() - p->clkStart );
     }
-    Sdb_StoIterCuts( p );
+    vRes = Sdb_StoIterCuts( p );
     Sdb_StoFree( p );
+    return vRes;
+}
+void Sdb_StoComputeCutsTest( Gia_Man_t * pGia )
+{
+    Vec_Int_t * vRes = Sdb_StoComputeCutsDetect( pGia );
+    Vec_IntFree( vRes );
 }
-
-
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/proof/acec/acecMult.c b/src/proof/acec/acecMult.c
index c63fdde2..66ee2fb7 100644
--- a/src/proof/acec/acecMult.c
+++ b/src/proof/acec/acecMult.c
@@ -189,6 +189,7 @@ unsigned Extra_TruthCanonNPN2( unsigned uTruth, int nVars, Vec_Int_t * vRes )
         for ( k = 0; k < nPerms; k++ )
         {
             uPerm = Extra_TruthPermute( uPhase, pPerms[k], nVars, 0 );
+            if ( !(uPerm & 1) )
             Vec_IntPushUnique( vRes, uPerm );
             if ( uTruthMin > uPerm )
                 uTruthMin = uPerm;
@@ -197,6 +198,7 @@ unsigned Extra_TruthCanonNPN2( unsigned uTruth, int nVars, Vec_Int_t * vRes )
         for ( k = 0; k < nPerms; k++ )
         {
             uPerm = Extra_TruthPermute( uPhase, pPerms[k], nVars, 0 );
+            if ( !(uPerm & 1) )
             Vec_IntPushUnique( vRes, uPerm );
             if ( uTruthMin > uPerm )
                 uTruthMin = uPerm;
@@ -233,8 +235,12 @@ void Acec_MultFuncTest4()
     Vec_Int_t * vRes = Vec_IntAlloc( 1000 );
     int i, Entry;
 
-    unsigned Truth = 0x35C0;
+    unsigned Truth = 0xF3C0;
+//    unsigned Truth = 0xF335;
+//    unsigned Truth = 0xFD80;
     //unsigned Truth = 0xD728;
+    //unsigned Truth = 0x35C0;
+    //unsigned Truth = 0xACC0;
     unsigned Canon = Extra_TruthCanonNPN2( Truth, 4, vRes );
 
     Extra_PrintHex( stdout, (unsigned*)&Truth, 4 );  printf( "\n" );