Algorithm Walter Randelshofer 2015
M3R2 VF2 MR2 N3F2 · M3R2 MR2 · V4U2 NF2 V4U2
L' M3F NL2 M3F' L M3F NL2 M3F'
MD2 MR MD2 MR'
F' MD2 F · N3U2 VD2 · F' MD2 F · N3U2 VD2
VR2 V4U2 N3R2 · NU2 N3D2 · NR2 M2U2 (38 btm, 70 ftm, 122 qtm)
Algorithm Walter Randelshofer 2015
M3R2 VF2 MR2 N3F2 · M3R2 MR2 · V4U2 NF2 V4U2
L' M3F NL2 M3F' L M3F NL2 M3F'
F' MD2 F · N3U2 VD2 · F' MD2 F V4D2 MR MD2 MR'
VR2 V4U2 N3R2 · NU2 N3D2 · NR2 M2U2 (36 btm, 66 ftm, 114 qtm)
Algorithm Walter Randelshofer 2015
M3R2 VF2 MR2 N3F2 · M3R2 MR2 · V4U2 NF2 WD2
M3F' D2 M3F ND2 M3F' D2 M3F
F' MD2 F · N3U2 VD2 · F' MD2 F V4D2 MR MD2 MR'
VR2 V4U2 N3R2 · NU2 N3D2 · NR2 M2U2 (35 btm, 64 ftm, 112 qtm)
Algorithm Per Kristen Fredlund 2015
VR2 V4U2 N3R2 · NU2 N3D2 · NR2 N3D2 MR M3D2 NF2 MR'
F2 MR NF2 MR' TF2 V4U2 M3R2 NF2 M3R2 WD2
M3F' U2 M3F ND2 M3F' U2 M3F (28 btm, 52 ftm, 88 qtm)