Algorithm Walter Randelshofer 2014
N3F2 N3R2 · NU2 N3D2 · N3R2 N3F2 · NU2 N3D2
NF2 NR2 M2U2 NR2 NF2 M2U2
L2 MF2 L2 · N3U' ND · L2 MF2 L2 · N3U ND' (24 btm)
Algorithm Walter Randelshofer 2014
N3F2 VR2 NF2 M2U2 NF2 NR2 V4U2 N3R2 N3F2 · NU2 N3D2
MR' (ND N3U' · MR · ND2 N3U2 · MR' · ND N3U') MR (21 btm)
Algorithm Walter Randelshofer 2014
N3R2 VF2 TR2 MF2 R2 · N3U' ND · R2 MF2 R2 · N3U M2U2 ND' · NR2 NF2 V4U2 N3F2 N3R2 · NU2 N3D2 (20 btm)
Algorithm Per Kristen Fredlund 2014
MR2 MF2 (WR' M2U' WR M2U2 WR' M2U' WR)
(M3R' V4U' M3R V4U2 M3R' V4U' M3R) MF2 MR2 (18 btm)