$ anthem verify --equivalence external primes.1.lp primes.2.lp primes.ug primes.po
> Proving forward_outline_0_0...
Axioms:
    forall V1 (composite(V1) <-> exists I1$i J1$i (V1 = I1$i * J1$i and (I1$i > 1 and J1$i > 1)))
    forall V1 (composite_p(V1) <-> exists I1$i J1$i (V1 = I1$i * J1$i and (2 <= I1$i and I1$i <= n$i and (2 <= J1$i and J1$i <= n$i))))
    forall V1 (prime(V1) <-> exists K$i (2 <= K$i and K$i <= n$i and V1 = K$i and not composite(V1)))

Conjectures:
    forall M$i N$i (M$i >= 1 and N$i >= 1 -> M$i * N$i >= M$i)

> Proving forward_outline_0_0 ended with a SZS status
Status: Theorem (249 ms)

> Proving forward_problem_0...
Axioms:
    forall V1 (composite(V1) <-> exists I1$i J1$i (V1 = I1$i * J1$i and (I1$i > 1 and J1$i > 1)))
    forall V1 (composite_p(V1) <-> exists I1$i J1$i (V1 = I1$i * J1$i and (2 <= I1$i and I1$i <= n$i and (2 <= J1$i and J1$i <= n$i))))
    forall V1 (prime(V1) <-> exists K$i (2 <= K$i and K$i <= n$i and V1 = K$i and not composite(V1)))
    forall M$i N$i (M$i >= 1 and N$i >= 1 -> M$i * N$i >= M$i)

Conjectures:
    forall V1 (prime(V1) -> exists K$i (2 <= K$i and K$i <= n$i and V1 = K$i and not composite_p(V1)))

> Proving forward_problem_0 ended with a SZS status
Status: Theorem (52 ms)

> Proving forward_problem_1...
Axioms:
    forall V1 (composite(V1) <-> exists I1$i J1$i (V1 = I1$i * J1$i and (I1$i > 1 and J1$i > 1)))
    forall V1 (composite_p(V1) <-> exists I1$i J1$i (V1 = I1$i * J1$i and (2 <= I1$i and I1$i <= n$i and (2 <= J1$i and J1$i <= n$i))))
    forall V1 (prime(V1) <-> exists K$i (2 <= K$i and K$i <= n$i and V1 = K$i and not composite(V1)))
    forall M$i N$i (M$i >= 1 and N$i >= 1 -> M$i * N$i >= M$i)
    forall V1 (prime(V1) -> exists K$i (2 <= K$i and K$i <= n$i and V1 = K$i and not composite_p(V1)))

Conjectures:
    forall V1 (prime(V1) <- exists K$i (2 <= K$i and K$i <= n$i and V1 = K$i and not composite_p(V1)))

> Proving forward_problem_1 ended with a SZS status
Status: Theorem (1588 ms)

> Proving backward_outline_0_0...
Axioms:
    forall V1 (composite(V1) <-> exists I1$i J1$i (V1 = I1$i * J1$i and (I1$i > 1 and J1$i > 1)))
    forall V1 (composite_p(V1) <-> exists I1$i J1$i (V1 = I1$i * J1$i and (2 <= I1$i and I1$i <= n$i and (2 <= J1$i and J1$i <= n$i))))
    forall V1 (prime(V1) <-> exists K$i (2 <= K$i and K$i <= n$i and V1 = K$i and not composite_p(V1)))

Conjectures:
    forall M$i N$i (M$i >= 1 and N$i >= 1 -> M$i * N$i >= M$i)

> Proving backward_outline_0_0 ended with a SZS status
Status: Theorem (259 ms)

> Proving backward_problem_0...
Axioms:
    forall V1 (composite(V1) <-> exists I1$i J1$i (V1 = I1$i * J1$i and (I1$i > 1 and J1$i > 1)))
    forall V1 (composite_p(V1) <-> exists I1$i J1$i (V1 = I1$i * J1$i and (2 <= I1$i and I1$i <= n$i and (2 <= J1$i and J1$i <= n$i))))
    forall V1 (prime(V1) <-> exists K$i (2 <= K$i and K$i <= n$i and V1 = K$i and not composite_p(V1)))
    forall M$i N$i (M$i >= 1 and N$i >= 1 -> M$i * N$i >= M$i)

Conjectures:
    forall V1 (prime(V1) -> exists K$i (2 <= K$i and K$i <= n$i and V1 = K$i and not composite(V1)))

> Proving backward_problem_0 ended with a SZS status
Status: Theorem (773 ms)

> Proving backward_problem_1...
Axioms:
    forall V1 (composite(V1) <-> exists I1$i J1$i (V1 = I1$i * J1$i and (I1$i > 1 and J1$i > 1)))
    forall V1 (composite_p(V1) <-> exists I1$i J1$i (V1 = I1$i * J1$i and (2 <= I1$i and I1$i <= n$i and (2 <= J1$i and J1$i <= n$i))))
    forall V1 (prime(V1) <-> exists K$i (2 <= K$i and K$i <= n$i and V1 = K$i and not composite_p(V1)))
    forall M$i N$i (M$i >= 1 and N$i >= 1 -> M$i * N$i >= M$i)
    forall V1 (prime(V1) -> exists K$i (2 <= K$i and K$i <= n$i and V1 = K$i and not composite(V1)))

Conjectures:
    forall V1 (prime(V1) <- exists K$i (2 <= K$i and K$i <= n$i and V1 = K$i and not composite(V1)))

> Proving backward_problem_1 ended with a SZS status
Status: Theorem (1579 ms)

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