$ anthem verify --equivalence strong bounds.1.lp bounds.2.lp
> Proving forward_0...
Axioms:
    forall X1 (hp(X1) -> tp(X1))
    forall V1 X ((V1 = X and (X > 3 and X < 5) -> hp(V1)) and (V1 = X and (X > 3 and X < 5) -> tp(V1)))

Conjectures:
    forall V1 ((V1 = 4 -> hp(V1)) and (V1 = 4 -> tp(V1)))

> Proving forward_0 ended with a SZS status
Status: Theorem (200 ms)

> Proving backward_0...
Axioms:
    forall X1 (hp(X1) -> tp(X1))
    forall V1 ((V1 = 4 -> hp(V1)) and (V1 = 4 -> tp(V1)))

Conjectures:
    forall V1 X ((V1 = X and (X > 3 and X < 5) -> hp(V1)) and (V1 = X and (X > 3 and X < 5) -> tp(V1)))

> Proving backward_0 ended with a SZS status
Status: Theorem (3606 ms)

> Success! Anthem found a proof of the theorem. (3811 ms)
