use(dto).
/*(q and (0=<f(X) or f(X)=<g(X)))=>z.
z and (V=0)=>r.
q and (exists(X,(f(X)<0 or g(X)<f(X))) or exists(V,~(excess(V)=0))).
0=<g(X).
~r.*/

/*q<-r  and excess(V)=0.

r.

u<-q.

~u.*/

exists(Sete,exists(Setv,models(Sete,Setv,badflow))).

models(Sete,Setv,badflow)=>exists(E,member(E,Sete) and (f(E)<0 or c(E)<f(E))).

models(Sete,Setv,badflow)=>exists(V,member(V,Setv) and ~(excess(V)=0)).


0=<c(E).

q(Sete,Setv)<-all(E,member(E,Sete)=>(0=<f(E) or f(E)=<c(E))).

r<-q(Sete,Setv) and all(V,member(V,Setv)=>excess(V)=0).

 
~r. 


%%all(V,0=<excess(V)).

/*all(X,exists(Y,Y=0)).*/