A1:
intloc (3 + 1) <> intloc (5 + 1)
by SCMFSA_2:101;
A2:
not (intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))) destroys intloc (3 + 1)
by SCMFSA7B:14, SCMFSA_2:101;
A3:
not SubFrom ((intloc (2 + 1)),(intloc 0)) destroys intloc (3 + 1)
by SCMFSA7B:8, SCMFSA_2:101;
not (intloc (1 + 1)) := (intloc (2 + 1)) destroys intloc (3 + 1)
by SCMFSA7B:6, SCMFSA_2:101;
then
not (((intloc (1 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1)))) destroys intloc (3 + 1)
by A3, A2, SCMFSA8C:54, SCMFSA8C:55;
then
not ((((intloc (1 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1)))) destroys intloc (3 + 1)
by A1, SCMFSA7B:14, SCMFSA8C:54;
then
not (((((intloc (1 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1))) destroys intloc (3 + 1)
by SCMFSA7B:15, SCMFSA8C:54;
hence
not ((((((intloc (1 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1))) destroys intloc (3 + 1)
by SCMFSA7B:15, SCMFSA8C:54; verum