forall(s1maxZ0 : (exists(s1min : forall(olds1 : forall(e1 : forall(e2 : forall(e3 : forall(o1 : forall(o2 : forall(delta1 : forall(delta2 : forall(s1 : ((e1min<=e1max and (e2min<=e2max and (e3min<=e3max and (s1min<=s1max and (e2min>((0) / (1))))))) and ((not (((e1<=e1max and (e1>=e1min and (e2<=e2max and (e2>=e2min and (e3<=e3max and (e3>=e3min and (olds1<=s1max and (olds1>=s1min)))))))) and ((delta1=(e1+(- olds1)) and (((delta1(- e2) and (o2=o1)) or ((not (delta2>(- e2)) and (o2=(o1+(- e2)))))))) and ((s1=o2 or (s1=e3))))))) or ((s1<=s1max and (s1>=s1min)))))))))))))))) and ((not (exists(s1min : forall(olds1 : forall(e1 : forall(e2 : forall(e3 : forall(o1 : forall(o2 : forall(delta1 : forall(delta2 : forall(s1 : ((e1min<=e1max and (e2min<=e2max and (e3min<=e3max and (s1min<=s1maxZ0 and (e2min>((0) / (1))))))) and ((not (((e1<=e1max and (e1>=e1min and (e2<=e2max and (e2>=e2min and (e3<=e3max and (e3>=e3min and (olds1<=s1maxZ0 and (olds1>=s1min)))))))) and ((delta1=(e1+(- olds1)) and (((delta1(- e2) and (o2=o1)) or ((not (delta2>(- e2)) and (o2=(o1+(- e2)))))))) and ((s1=o2 or (s1=e3))))))) or ((s1<=s1maxZ0 and (s1>=s1min))))))))))))))))) or (s1max<=s1maxZ0))))) and e1max=4 and e3max=3 and e1min=-4 and e3min=-3 and e2min=1 and e2max = 2