$𝖟𝕷𝖔𝖌𝖎𝖈/𝕾𝖒𝖚𝖑𝖑𝖞𝖆𝖓/𝕾𝖆𝖙𝖆𝖓-𝕮𝖆𝖓𝖙𝖔𝖗-𝖆𝖓𝖉-𝕴𝖓𝖋𝖎𝖓𝖎𝖙𝖞/𝖎-𝖘𝖆𝖙𝖆𝖓.𝖘𝖆𝖕𝖕𝖍𝖎𝖗𝖊 
    0---------------------------------|·Satan,·Cantor·&·Infinity·I·|---------------------------------
    1--|·problem·on·Page·3:·a→Arthur·b→Bernard·c→Charles                                            
    2--|·Arthur·confirms·Bernard·and·Charles·are·both·knights                                       
    3a(bc)¬a¬(bc)                                                                              
    4--|·Arthur·denies·Bernard·is·a·knight                                                          
    5a¬b¬ab                                                                                      
    6                                                                                               
    7proof:·a(bc)¬a(¬b¬c)·a¬b¬ab··¬ab¬c                                                  
    8A··A····································[eqsp]·--|·Equivalent·Sapphire·Normal·Forms         
    9(AX)(¬AY)··XY·······················[r]                                                 
   10AB··A··································[cind]·--|·Conjunctive·Independence                 
   11P(PQ)··Q······························[mp]···--|·Modus·Ponens                             
   12·P¬P···································[lem]··--|·The·Law·of·Excluded·Middle               
   13A(XY)··AXAY························[ado]··--|·And·Distribution·over·Or                 
   14BZW··(BZ)(BW)······················[oda]··--|·Or·Distribution·over·And                 
   15¬AB··AB·······························[imp]··--|·Implication                              
   16AB··¬AB·······························[imp2]·--|·Implication                              
   17AB··¬B¬A······························[cp]···--|·Contrapositive                           
   18(XA)(XB)··XAB······················[cc]···--|·Composition·of·Conjunction               
   19XAB··XA······························[dcc]··--|·Decomposition·of·Conjunction             
   20·¬(A¬A)································[con]··--|·Consistency                              
   21A··¬¬A··································[dneg]·--|·Double·Negation                          
   22                                                                                               
   23a(bc)¬a(¬b¬c)·······················[0] - assumption                                    
   24a¬b¬ab································[1] - assumption                                    
   25                                                                                               
   26(a¬b¬a)(a¬bb)··oda·1···············[2] - BZW ≡ (BZ)(BW) Ba¬b W¬a Zb         
   27(a(bc)¬a)(a(bc)(¬b¬c))··oda·0···[3] - BZW ≡ (BZ)(BW) Babc W¬b¬c Z¬a    
   28a¬b¬a··cind·2·························[4] - AB  A A¬aa¬b Bba¬b                  
   29a¬a··lem                                   -  P¬P Pa                                  
   30(¬aa)(¬a¬b)··oda·4···················[6] - BZW ≡ (BZ)(BW) B¬a W¬b Za           
   31a¬a··lem                                   -  P¬P Pa                                  
   32¬a¬b··cind·6···························[8] - AB  A A¬a¬b Ba¬a                      
   33a¬b··imp·8·····························[9] - ¬AB ≡ AB Aa B¬b                         
   34a(bc)¬a··cind·3······················[10] - AB  A A¬aabc B¬b¬cabc           
   35a¬a··lem                                    -  P¬P Pa                                 
   36aa(bc)··imp·10·······················[12] - ¬AB ≡ AB Aa Babc                     
   37abc··dcc·12···························[13] - XAB  XA Xa Abc Ba                  
   38ab··dcc·13·····························[14] - XAB  XA Xa Ab Bc                    
   39ab¬b··cc·9·14·························[15] - (XA)(XB) ≡ XAB Xa A¬b Bb           
   40¬(b¬b)¬a··cp·15·······················[16] - AB ≡ ¬B¬A Bb¬b Aa                     
   41¬(b¬b)··con····························[17] -  ¬(A¬A) Ab                              
   42¬a··mp·17·16····························[18] - P(PQ)  Q Q¬a P¬(b¬b)                 
   43a¬a··lem                                    -  P¬P Pa                                 
   44a¬bb··cind·2··························[20] - AB  A Aba¬b B¬aa¬b                 
   45a¬a··lem                                    -  P¬P Pa                                 
   46(ba)(b¬b)··oda·20····················[22] - BZW ≡ (BZ)(BW) Bb W¬b Za           
   47ba··cind·22····························[23] - AB  A Aab Bb¬b                       
   48a¬a··lem                                    -  P¬P Pa                                 
   49¬ab··imp2··23··························[25] - AB ≡ ¬AB Aa Bb                         
   50b··mp·18·25·····························[26] - P(PQ)  Q Qb P¬a                       
   51a¬a··lem                                    -  P¬P Pa                                 
   52a(bc)(¬b¬c)··cind·3·················[28] - AB  A A¬b¬cabc B¬aabc           
   53a¬a··lem                                    -  P¬P Pa                                 
   54((¬b¬c)a)((¬b¬c)(bc))··oda·28·····[30] - BZW ≡ (BZ)(BW) B¬b¬c Wbc Za      
   55(¬b¬c)a··cind·30······················[31] - AB  A Aa¬b¬c B¬b¬cbc              
   56a¬a··lem                                    -  P¬P Pa                                 
   57¬a(¬b¬c)··imp2·31·····················[33] - AB ≡ ¬AB Aa B¬b¬c                     
   58¬b¬c··mp·18·33·························[34] - P(PQ)  Q Q¬b¬c P¬a                   
   59b¬c··imp·34····························[35] - ¬AB ≡ AB Ab B¬c                        
   60¬c··mp·26·35····························[36] - P(PQ)  Q Q¬c Pb                       
   61¬ab¬c··eqsp·18·26·36                       - A ≡ A Ab¬a¬c