Z3 is the only system that is able to refute REL051+1.p?

Question

The problem in relational algebra REL051+1.p reads

  File     : REL051+1 : TPTP v6.1.0. Released v4.0.0.
% Domain   : Relation Algebra
% Problem  : Dense linear ordering

Using TPTP syntax with fof the corresponding code is

fof(f01,axiom,(
    ! [A] : o(A,A) )).

fof(f02,axiom,(
    ! [A,B] :
      ( ( A != B
        & o(A,B) )
     => ~ o(B,A) ) )).

fof(f03,axiom,(
    ! [A,B,C] :
      ( ( o(A,B)
        & o(B,C) )
     => o(A,C) ) )).

fof(f04,axiom,(
    ! [A,B] :
      ( ( A != B
        & o(A,B) )
     => ( o(A,f(A,B))
        & o(f(A,B),B) ) ) )).

fof(f05,axiom,(
    ! [A,B] :
      ( f(A,B) != A
      & f(A,B) != B ) )).

fof(f06,axiom,(
    ! [A,B] :
      ( o(A,B)
      | o(B,A) ) )).

As you can see in TPTP all ATPs are unable to prove such problem.

This theorem was refuted with Z3 using the following SMT-LIB

(declare-sort S)
(declare-fun o (S S) Bool)
(declare-fun f (S S) S)
(assert (forall ((A S)) (o A A) ))
(assert (forall ((A S) (B S)) (implies (and (distinct A B) (o A B)) 
                                       (not (o B A)))   ) )
(assert (forall ((A S) (B S) (C S)) (implies (and (o A B) (o B C)) 
                                             (o A C))   ) )
(assert (forall ((A S) (B S)) (implies (and (distinct A B) (o A B)) 
                                       (and (o A (f A B)) (o (f A B) B)))   ) )
(declare-fun B () S)
(assert (forall ((A S)) (and (distinct (f A B) A) 
                                   (distinct (f A B) B))    ) )

(assert (not (forall ((A S)) (or (o A B) (o B A)) ) ))

(check-sat)
(get-model)

and the corresponding output is

    sat
    (model
      ;; universe for S:
      ;;   S!val!0 S!val!3 S!val!1 S!val!2
      ;; -----------
      ;; definitions for universe elements:
      (declare-fun S!val!0 () S)
      (declare-fun S!val!3 () S)
      (declare-fun S!val!1 () S)
      (declare-fun S!val!2 () S)
      ;; cardinality constraint:
      (forall ((x S)) (or (= x S!val!0) (= x S!val!3) (= x S!val!1) (= x S!val!2)))
      ;; -----------
      (define-fun B () S
        S!val!1)
      (define-fun A!0 () S
        S!val!0)
      (define-fun f!47 ((x!1 S) (x!2 S)) S
        (ite (and (= x!1 S!val!2) (= x!2 S!val!1)) S!val!3
          S!val!2))
      (define-fun k!46 ((x!1 S)) S
        (ite (= x!1 S!val!2) S!val!2
        (ite (= x!1 S!val!0) S!val!0
        (ite (= x!1 S!val!3) S!val!3
          S!val!1))))
      (define-fun f ((x!1 S) (x!2 S)) S
        (f!47 (k!46 x!1) (k!46 x!2)))
      (define-fun o!48 ((x!1 S) (x!2 S)) Bool
        (ite (and (= x!1 S!val!1) (= x!2 S!val!1)) true
        (ite (and (= x!1 S!val!0) (= x!2 S!val!0)) true
        (ite (and (= x!1 S!val!2) (= x!2 S!val!2)) true
        (ite (and (= x!1 S!val!3) (= x!2 S!val!3)) true
          false)))))
      (define-fun o ((x!1 S) (x!2 S)) Bool
        (o!48 (k!46 x!1) (k!46 x!2)))
)

Please run this example online here

My question is: This refutation with Z3 is correct?