Check why algorithm doesn't halt for certain input

```
∀x∀y(R²xy ⊃ ~R²yx)
∴ ~∀x∀y(R²xy ⊃ R²yx)
```

```
∀x((P¹x & B¹x) ⊃ ∀y((P¹y & O¹y) ⊃ H²xy)),
P¹e
∴ ∀x((P¹x & B¹x) ⊃ H²xe)
```

```
(∀x)(S¹x ⊃ (∀y)(A¹y ⊃ (∀z)(T¹z ⊃ (S³xyz ⊃ ~F²xz))))                                                    
∴ (∀x)(∀z)((S¹x & ((∃y)(A¹y & T¹z & S³xyz))) ⊃ ~F²xz)
```

```
∀x(A ⊃ B)
```