use(int).


/*

at(8) <-  (at(9) and all(E,processed9(E))).


% a7: AXIOM processed9(e) IFF (flow(e) >= 0 OR (flow(e) <= cap(e)))

processed9(E) == (flow(E) >= 0 or cap(E)>= flow(E)).



% THEOREM (at_9 AND (FORALL e: flow(e) >= 0)) IMPLIES at_8

~((at(9) and all(E,flow(E) >=0)) => at(8)).



%:-option(iterative_saturation(on)).




*/


~(((at(8) ==  (at(9) or  all(E,processed9(E)))) and (all(E,processed9(E) == (flow(E) >= 0 or cap(E)>= flow(E)))))=>(at_8 =>(at_9 and all(E,(flow(E)>=0 and cap(E)>=flow(E)))))) .