Optimize quantifiers and for in Z3py

Question

so I'm lloking for a way to simplify the following code in Z3py because every time I want to check this assertion (on my own computer or on http://rise4fun.com/z3py/ ) it just timed out so I think there could be fastest ways to do.

Task = Datatype('Task')
Task.declare("cons",("num", IntSort()),("order",IntSort()),("arrival",IntSort()))
Task = Task.create()
order = Task.order
num = Task.num
x = Int('x')
y = Int('y')
s = Solver()
tasks = (Task.cons(0,0,0),\
     Task.cons(0,1,0),\
     Task.cons(0,2,0),\
     Task.cons(0,3,0),\
     Task.cons(1,0,1),\
     Task.cons(1,1,1),\
     Task.cons(1,2,1),\
     Task.cons(2,0,3),\
     Task.cons(2,1,3),\
     Task.cons(2,2,3),\
     Task.cons(2,3,3),\
     Task.cons(2,4,3),\
     Task.cons(3,0,1),\
     Task.cons(3,1,1))
p1 = Function('p1',IntSort(),Task)
p2 = Function('p2',IntSort(),Task)
order = And([Exists([x,y],Or(And(p1(x)==t1,p1(y)==t2,If(num(t1)==num(t2),Implies(x<y,order(t1)<order(t2)),True)),\
                         And(p1(x)==t1,p2(y)==t2,If(num(t1)==num(t2),Implies(x<y,order(t1)<order(t2)),True)),\
                         And(p2(x)==t1,p1(y)==t2,If(num(t1)==num(t2),Implies(x<y,order(t1)<order(t2)),True)),\
                         And(p2(x)==t1,p2(y)==t2,If(num(t1)==num(t2),Implies(x<y,order(t1)<order(t2)),True))))\
             for t1 in tasks for t2 in tasks])
s.add(order)

As you can seen it is really a big formula but I didn't found a way to make it smaller... The objective is to make sure that every parts of a task are in order even if they are processed by different processors (p1 or p2)

Thanks a lot in advance if you can help me (even just a hint that could help me to change that formula would be great)

edit : I just tested that constraint alone and it works,it give strange results but still works, but I still need it to work with others constraints so if you can help me to optimize it you're welcome.

Answer 1

The question seems essentially answered in the comments section.