Linear extension of partial orders with Z3

Question

I'm trying to write a script that, given a partial order over a (small) set of constants, finds a total order that can be built as an extension of the given partial ordering constrains (i.e. a linear extension).

As an example, if given a,b,c,d as constants and a>b && b>d as constrains, the program should output any of these orderings (or all, if feasible - linear extensions are #P-complete):

c > a > b > d  
a > c > b > d  
a > b > c > d  
a > b > d > c  

Here is my first attempt with z3py:

from z3 import *

s = Solver()
s.set("timeout", 3000)

if len(sys.argv) > 1 and sys.argv[1] == "int":
    sort = IntSort()
else:
    sort = DeclareSort('T')
to = Function('>', sort, sort, BoolSort())

x,y,z = Consts('x y z', sort)
s.add(ForAll([x,y], Implies(And(to(x,y),to(y,x)), x==y)))       # antisymmetry
s.add(ForAll([x,y,z], Implies(And(to(x,y),to(y,z)), to(x,z))))  # transitivity
s.add(ForAll([x,y], Or(to(x,y), to(y,x))))                      # totality

a,b,c,d = Consts('a b c d', sort)
s.add(Distinct(a,b,c,d))

s.add(to(a,b))
s.add(to(b,d))
#s.add(to(d,a)) # add cycle to make it unsat

print s.check()
print s.model()  

And these are my questions:

1. why does it timeout when using the totality constrain over constants defined as IntSort?
2. Is there a way to obtain a more usable representation of the model (e.g. a<b<c<d)? (related question: link)
3. Is there a better way or a more suitable tool to solve this problem?

Thanks in advance for any help!