railroadtest/railroadadd1possible bounds: {L0}:[-1]:n2(x) +0[-20,20] < [-1]:f(x) AND {L1}:[-1]:f(x) +0[-20,20] < [-1]:n2(x) AND {L2}:[-1]:n2(x) +0[-20,20] < [-1]:g1(x) AND {L3}:[-1]:g1(x) +0[-20,20] < [-1]:n2(x) AND {L4}:[-1]:n2(x) +0[-20,20] < [-1]:g2(x) AND {L5}:[-1]:g2(x) +0[-20,20] < [-1]:n2(x) AND {L6}:[-1]:n2(x) +0[-20,20] < [-1]:h1(x) AND {L7}:[-1]:h1(x) +0[-20,20] < [-1]:n2(x) AND {L8}:[-1]:n2(x) +0[-20,20] < [-1]:h2(x) AND {L9}:[-1]:h2(x) +0[-20,20] < [-1]:n2(x) AND {L10}:[-1]:n2(x) +0[-20,20] < [-1]:n1(x) AND {L11}:[-1]:n1(x) +0[-20,20] < [-1]:n2(x) AND {L12}:[-1]:n2(x) +0[-20,20] < [-1]:n4(x) AND {L13}:[-1]:n4(x) +0[-20,20] < [-1]:n2(x) AND {L14}:[-1]:n2(x) +0[-20,20] < [-1]:n3(x) AND {L15}:[-1]:n3(x) +0[-20,20] < [-1]:n2(x) AND {L16}:[-1]:n1(x) +0[-20,20] < [-1]:f(x) AND {L17}:[-1]:f(x) +0[-20,20] < [-1]:n1(x) AND {L18}:[-1]:n1(x) +0[-20,20] < [-1]:g1(x) AND {L19}:[-1]:g1(x) +0[-20,20] < [-1]:n1(x) AND {L20}:[-1]:n1(x) +0[-20,20] < [-1]:g2(x) AND {L21}:[-1]:g2(x) +0[-20,20] < [-1]:n1(x) AND {L22}:[-1]:n1(x) +0[-20,20] < [-1]:h1(x) AND {L23}:[-1]:h1(x) +0[-20,20] < [-1]:n1(x) AND {L24}:[-1]:n1(x) +0[-20,20] < [-1]:h2(x) AND {L25}:[-1]:h2(x) +0[-20,20] < [-1]:n1(x) AND {L11}:[-1]:n1(x) +0[-20,20] < [-1]:n2(x) AND {L10}:[-1]:n2(x) +0[-20,20] < [-1]:n1(x) AND {L26}:[-1]:n1(x) +0[-20,20] < [-1]:n4(x) AND {L27}:[-1]:n4(x) +0[-20,20] < [-1]:n1(x) AND {L28}:[-1]:n1(x) +0[-20,20] < [-1]:n3(x) AND {L29}:[-1]:n3(x) +0[-20,20] < [-1]:n1(x) AND {L30}:[-1]:n4(x) +0[-20,20] < [-1]:f(x) AND {L31}:[-1]:f(x) +0[-20,20] < [-1]:n4(x) AND {L32}:[-1]:n4(x) +0[-20,20] < [-1]:g1(x) AND {L33}:[-1]:g1(x) +0[-20,20] < [-1]:n4(x) AND {L34}:[-1]:n4(x) +0[-20,20] < [-1]:g2(x) AND {L35}:[-1]:g2(x) +0[-20,20] < [-1]:n4(x) AND {L36}:[-1]:n4(x) +0[-20,20] < [-1]:h1(x) AND {L37}:[-1]:h1(x) +0[-20,20] < [-1]:n4(x) AND {L38}:[-1]:n4(x) +0[-20,20] < [-1]:h2(x) AND {L39}:[-1]:h2(x) +0[-20,20] < [-1]:n4(x) AND {L13}:[-1]:n4(x) +0[-20,20] < [-1]:n2(x) AND {L12}:[-1]:n2(x) +0[-20,20] < [-1]:n4(x) AND {L27}:[-1]:n4(x) +0[-20,20] < [-1]:n1(x) AND {L26}:[-1]:n1(x) +0[-20,20] < [-1]:n4(x) AND {L40}:[-1]:n4(x) +0[-20,20] < [-1]:n3(x) AND {L41}:[-1]:n3(x) +0[-20,20] < [-1]:n4(x) AND {L42}:[-1]:n3(x) +0[-20,20] < [-1]:f(x) AND {L43}:[-1]:f(x) +0[-20,20] < [-1]:n3(x) AND {L44}:[-1]:n3(x) +0[-20,20] < [-1]:g1(x) AND {L45}:[-1]:g1(x) +0[-20,20] < [-1]:n3(x) AND {L46}:[-1]:n3(x) +0[-20,20] < [-1]:g2(x) AND {L47}:[-1]:g2(x) +0[-20,20] < [-1]:n3(x) AND {L48}:[-1]:n3(x) +0[-20,20] < [-1]:h1(x) AND {L49}:[-1]:h1(x) +0[-20,20] < [-1]:n3(x) AND {L50}:[-1]:n3(x) +0[-20,20] < [-1]:h2(x) AND {L51}:[-1]:h2(x) +0[-20,20] < [-1]:n3(x) AND {L15}:[-1]:n3(x) +0[-20,20] < [-1]:n2(x) AND {L14}:[-1]:n2(x) +0[-20,20] < [-1]:n3(x) AND {L29}:[-1]:n3(x) +0[-20,20] < [-1]:n1(x) AND {L28}:[-1]:n1(x) +0[-20,20] < [-1]:n3(x) AND {L41}:[-1]:n3(x) +0[-20,20] < [-1]:n4(x) AND {L40}:[-1]:n4(x) +0[-20,20] < [-1]:n3(x) AND {L52}:[-1]:g1(x) +0[-20,20] < [-1]:f(x) AND {L53}:[-1]:f(x) +0[-20,20] < [-1]:g1(x) AND {L54}:[-1]:g1(x) +0[-20,20] < [-1]:g2(x) AND {L55}:[-1]:g2(x) +0[-20,20] < [-1]:g1(x) AND {L56}:[-1]:g1(x) +0[-20,20] < [-1]:h1(x) AND {L57}:[-1]:h1(x) +0[-20,20] < [-1]:g1(x) AND {L58}:[-1]:g1(x) +0[-20,20] < [-1]:h2(x) AND {L59}:[-1]:h2(x) +0[-20,20] < [-1]:g1(x) AND {L3}:[-1]:g1(x) +0[-20,20] < [-1]:n2(x) AND {L2}:[-1]:n2(x) +0[-20,20] < [-1]:g1(x) AND {L19}:[-1]:g1(x) +0[-20,20] < [-1]:n1(x) AND {L18}:[-1]:n1(x) +0[-20,20] < [-1]:g1(x) AND {L33}:[-1]:g1(x) +0[-20,20] < [-1]:n4(x) AND {L32}:[-1]:n4(x) +0[-20,20] < [-1]:g1(x) AND {L45}:[-1]:g1(x) +0[-20,20] < [-1]:n3(x) AND {L44}:[-1]:n3(x) +0[-20,20] < [-1]:g1(x) AND {L60}:[-1]:h1(x) +0[-20,20] < [-1]:f(x) AND {L61}:[-1]:f(x) +0[-20,20] < [-1]:h1(x) AND {L57}:[-1]:h1(x) +0[-20,20] < [-1]:g1(x) AND {L56}:[-1]:g1(x) +0[-20,20] < [-1]:h1(x) AND {L62}:[-1]:h1(x) +0[-20,20] < [-1]:g2(x) AND {L63}:[-1]:g2(x) +0[-20,20] < [-1]:h1(x) AND {L64}:[-1]:h1(x) +0[-20,20] < [-1]:h2(x) AND {L65}:[-1]:h2(x) +0[-20,20] < [-1]:h1(x) AND {L7}:[-1]:h1(x) +0[-20,20] < [-1]:n2(x) AND {L6}:[-1]:n2(x) +0[-20,20] < [-1]:h1(x) AND {L23}:[-1]:h1(x) +0[-20,20] < [-1]:n1(x) AND {L22}:[-1]:n1(x) +0[-20,20] < [-1]:h1(x) AND {L37}:[-1]:h1(x) +0[-20,20] < [-1]:n4(x) AND {L36}:[-1]:n4(x) +0[-20,20] < [-1]:h1(x) AND {L49}:[-1]:h1(x) +0[-20,20] < [-1]:n3(x) AND {L48}:[-1]:n3(x) +0[-20,20] < [-1]:h1(x) AND {L66}:[-1]:g2(x) +0[-20,20] < [-1]:f(x) AND {L67}:[-1]:f(x) +0[-20,20] < [-1]:g2(x) AND {L55}:[-1]:g2(x) +0[-20,20] < [-1]:g1(x) AND {L54}:[-1]:g1(x) +0[-20,20] < [-1]:g2(x) AND {L63}:[-1]:g2(x) +0[-20,20] < [-1]:h1(x) AND {L62}:[-1]:h1(x) +0[-20,20] < [-1]:g2(x) AND {L68}:[-1]:g2(x) +0[-20,20] < [-1]:h2(x) AND {L69}:[-1]:h2(x) +0[-20,20] < [-1]:g2(x) AND {L5}:[-1]:g2(x) +0[-20,20] < [-1]:n2(x) AND {L4}:[-1]:n2(x) +0[-20,20] < [-1]:g2(x) AND {L21}:[-1]:g2(x) +0[-20,20] < [-1]:n1(x) AND {L20}:[-1]:n1(x) +0[-20,20] < [-1]:g2(x) AND {L35}:[-1]:g2(x) +0[-20,20] < [-1]:n4(x) AND {L34}:[-1]:n4(x) +0[-20,20] < [-1]:g2(x) AND {L47}:[-1]:g2(x) +0[-20,20] < [-1]:n3(x) AND {L46}:[-1]:n3(x) +0[-20,20] < [-1]:g2(x) AND {L70}:[-1]:h2(x) +0[-20,20] < [-1]:f(x) AND {L71}:[-1]:f(x) +0[-20,20] < [-1]:h2(x) AND {L59}:[-1]:h2(x) +0[-20,20] < [-1]:g1(x) AND {L58}:[-1]:g1(x) +0[-20,20] < [-1]:h2(x) AND {L69}:[-1]:h2(x) +0[-20,20] < [-1]:g2(x) AND {L68}:[-1]:g2(x) +0[-20,20] < [-1]:h2(x) AND {L65}:[-1]:h2(x) +0[-20,20] < [-1]:h1(x) AND {L64}:[-1]:h1(x) +0[-20,20] < [-1]:h2(x) AND {L9}:[-1]:h2(x) +0[-20,20] < [-1]:n2(x) AND {L8}:[-1]:n2(x) +0[-20,20] < [-1]:h2(x) AND {L25}:[-1]:h2(x) +0[-20,20] < [-1]:n1(x) AND {L24}:[-1]:n1(x) +0[-20,20] < [-1]:h2(x) AND {L39}:[-1]:h2(x) +0[-20,20] < [-1]:n4(x) AND {L38}:[-1]:n4(x) +0[-20,20] < [-1]:h2(x) AND {L51}:[-1]:h2(x) +0[-20,20] < [-1]:n3(x) AND {L50}:[-1]:n3(x) +0[-20,20] < [-1]:h2(x) Constraints graph for formula: {L0}:[0]:n2(x) +0[-20,20] < [1]:f(x) AND {L1}:[1]:f(x) +0[-20,20] < [0]:n2(x) AND {L2}:[0]:n2(x) +0[-20,20] < [2]:g1(x) AND {L3}:[2]:g1(x) +0[-20,20] < [0]:n2(x) AND {L4}:[0]:n2(x) +0[-20,20] < [3]:g2(x) AND {L5}:[3]:g2(x) +0[-20,20] < [0]:n2(x) AND {L6}:[0]:n2(x) +0[-20,20] < [4]:h1(x) AND {L7}:[4]:h1(x) +0[-20,20] < [0]:n2(x) AND {L8}:[0]:n2(x) +0[-20,20] < [5]:h2(x) AND {L9}:[5]:h2(x) +0[-20,20] < [0]:n2(x) AND {L10}:[0]:n2(x) +0[-20,20] < [6]:n1(x) AND {L11}:[6]:n1(x) +0[-20,20] < [0]:n2(x) AND {L12}:[0]:n2(x) +0[-20,20] < [7]:n4(x) AND {L13}:[7]:n4(x) +0[-20,20] < [0]:n2(x) AND {L14}:[0]:n2(x) +0[-20,20] < [8]:n3(x) AND {L15}:[8]:n3(x) +0[-20,20] < [0]:n2(x) AND {L16}:[6]:n1(x) +0[-20,20] < [1]:f(x) AND {L17}:[1]:f(x) +0[-20,20] < [6]:n1(x) AND {L18}:[6]:n1(x) +0[-20,20] < [2]:g1(x) AND {L19}:[2]:g1(x) +0[-20,20] < [6]:n1(x) AND {L20}:[6]:n1(x) +0[-20,20] < [3]:g2(x) AND {L21}:[3]:g2(x) +0[-20,20] < [6]:n1(x) AND {L22}:[6]:n1(x) +0[-20,20] < [4]:h1(x) AND {L23}:[4]:h1(x) +0[-20,20] < [6]:n1(x) AND {L24}:[6]:n1(x) +0[-20,20] < [5]:h2(x) AND {L25}:[5]:h2(x) +0[-20,20] < [6]:n1(x) AND {L11}:[6]:n1(x) +0[-20,20] < [0]:n2(x) AND {L10}:[0]:n2(x) +0[-20,20] < [6]:n1(x) AND {L26}:[6]:n1(x) +0[-20,20] < [7]:n4(x) AND {L27}:[7]:n4(x) +0[-20,20] < [6]:n1(x) AND {L28}:[6]:n1(x) +0[-20,20] < [8]:n3(x) AND {L29}:[8]:n3(x) +0[-20,20] < [6]:n1(x) AND {L30}:[7]:n4(x) +0[-20,20] < [1]:f(x) AND {L31}:[1]:f(x) +0[-20,20] < [7]:n4(x) AND {L32}:[7]:n4(x) +0[-20,20] < [2]:g1(x) AND {L33}:[2]:g1(x) +0[-20,20] < [7]:n4(x) AND {L34}:[7]:n4(x) +0[-20,20] < [3]:g2(x) AND {L35}:[3]:g2(x) +0[-20,20] < [7]:n4(x) AND {L36}:[7]:n4(x) +0[-20,20] < [4]:h1(x) AND {L37}:[4]:h1(x) +0[-20,20] < [7]:n4(x) AND {L38}:[7]:n4(x) +0[-20,20] < [5]:h2(x) AND {L39}:[5]:h2(x) +0[-20,20] < [7]:n4(x) AND {L13}:[7]:n4(x) +0[-20,20] < [0]:n2(x) AND {L12}:[0]:n2(x) +0[-20,20] < [7]:n4(x) AND {L27}:[7]:n4(x) +0[-20,20] < [6]:n1(x) AND {L26}:[6]:n1(x) +0[-20,20] < [7]:n4(x) AND {L40}:[7]:n4(x) +0[-20,20] < [8]:n3(x) AND {L41}:[8]:n3(x) +0[-20,20] < [7]:n4(x) AND {L42}:[8]:n3(x) +0[-20,20] < [1]:f(x) AND {L43}:[1]:f(x) +0[-20,20] < [8]:n3(x) AND {L44}:[8]:n3(x) +0[-20,20] < [2]:g1(x) AND {L45}:[2]:g1(x) +0[-20,20] < [8]:n3(x) AND {L46}:[8]:n3(x) +0[-20,20] < [3]:g2(x) AND {L47}:[3]:g2(x) +0[-20,20] < [8]:n3(x) AND {L48}:[8]:n3(x) +0[-20,20] < [4]:h1(x) AND {L49}:[4]:h1(x) +0[-20,20] < [8]:n3(x) AND {L50}:[8]:n3(x) +0[-20,20] < [5]:h2(x) AND {L51}:[5]:h2(x) +0[-20,20] < [8]:n3(x) AND {L15}:[8]:n3(x) +0[-20,20] < [0]:n2(x) AND {L14}:[0]:n2(x) +0[-20,20] < [8]:n3(x) AND {L29}:[8]:n3(x) +0[-20,20] < [6]:n1(x) AND {L28}:[6]:n1(x) +0[-20,20] < [8]:n3(x) AND {L41}:[8]:n3(x) +0[-20,20] < [7]:n4(x) AND {L40}:[7]:n4(x) +0[-20,20] < [8]:n3(x) AND {L52}:[2]:g1(x) +0[-20,20] < [1]:f(x) AND {L53}:[1]:f(x) +0[-20,20] < [2]:g1(x) AND {L54}:[2]:g1(x) +0[-20,20] < [3]:g2(x) AND {L55}:[3]:g2(x) +0[-20,20] < [2]:g1(x) AND {L56}:[2]:g1(x) +0[-20,20] < [4]:h1(x) AND {L57}:[4]:h1(x) +0[-20,20] < [2]:g1(x) AND {L58}:[2]:g1(x) +0[-20,20] < [5]:h2(x) AND {L59}:[5]:h2(x) +0[-20,20] < [2]:g1(x) AND {L3}:[2]:g1(x) +0[-20,20] < [0]:n2(x) AND {L2}:[0]:n2(x) +0[-20,20] < [2]:g1(x) AND {L19}:[2]:g1(x) +0[-20,20] < [6]:n1(x) AND {L18}:[6]:n1(x) +0[-20,20] < [2]:g1(x) AND {L33}:[2]:g1(x) +0[-20,20] < [7]:n4(x) AND {L32}:[7]:n4(x) +0[-20,20] < [2]:g1(x) AND {L45}:[2]:g1(x) +0[-20,20] < [8]:n3(x) AND {L44}:[8]:n3(x) +0[-20,20] < [2]:g1(x) AND {L60}:[4]:h1(x) +0[-20,20] < [1]:f(x) AND {L61}:[1]:f(x) +0[-20,20] < [4]:h1(x) AND {L57}:[4]:h1(x) +0[-20,20] < [2]:g1(x) AND {L56}:[2]:g1(x) +0[-20,20] < [4]:h1(x) AND {L62}:[4]:h1(x) +0[-20,20] < [3]:g2(x) AND {L63}:[3]:g2(x) +0[-20,20] < [4]:h1(x) AND {L64}:[4]:h1(x) +0[-20,20] < [5]:h2(x) AND {L65}:[5]:h2(x) +0[-20,20] < [4]:h1(x) AND {L7}:[4]:h1(x) +0[-20,20] < [0]:n2(x) AND {L6}:[0]:n2(x) +0[-20,20] < [4]:h1(x) AND {L23}:[4]:h1(x) +0[-20,20] < [6]:n1(x) AND {L22}:[6]:n1(x) +0[-20,20] < [4]:h1(x) AND {L37}:[4]:h1(x) +0[-20,20] < [7]:n4(x) AND {L36}:[7]:n4(x) +0[-20,20] < [4]:h1(x) AND {L49}:[4]:h1(x) +0[-20,20] < [8]:n3(x) AND {L48}:[8]:n3(x) +0[-20,20] < [4]:h1(x) AND {L66}:[3]:g2(x) +0[-20,20] < [1]:f(x) AND {L67}:[1]:f(x) +0[-20,20] < [3]:g2(x) AND {L55}:[3]:g2(x) +0[-20,20] < [2]:g1(x) AND {L54}:[2]:g1(x) +0[-20,20] < [3]:g2(x) AND {L63}:[3]:g2(x) +0[-20,20] < [4]:h1(x) AND {L62}:[4]:h1(x) +0[-20,20] < [3]:g2(x) AND {L68}:[3]:g2(x) +0[-20,20] < [5]:h2(x) AND {L69}:[5]:h2(x) +0[-20,20] < [3]:g2(x) AND {L5}:[3]:g2(x) +0[-20,20] < [0]:n2(x) AND {L4}:[0]:n2(x) +0[-20,20] < [3]:g2(x) AND {L21}:[3]:g2(x) +0[-20,20] < [6]:n1(x) AND {L20}:[6]:n1(x) +0[-20,20] < [3]:g2(x) AND {L35}:[3]:g2(x) +0[-20,20] < [7]:n4(x) AND {L34}:[7]:n4(x) +0[-20,20] < [3]:g2(x) AND {L47}:[3]:g2(x) +0[-20,20] < [8]:n3(x) AND {L46}:[8]:n3(x) +0[-20,20] < [3]:g2(x) AND {L70}:[5]:h2(x) +0[-20,20] < [1]:f(x) AND {L71}:[1]:f(x) +0[-20,20] < [5]:h2(x) AND {L59}:[5]:h2(x) +0[-20,20] < [2]:g1(x) AND {L58}:[2]:g1(x) +0[-20,20] < [5]:h2(x) AND {L69}:[5]:h2(x) +0[-20,20] < [3]:g2(x) AND {L68}:[3]:g2(x) +0[-20,20] < [5]:h2(x) AND {L65}:[5]:h2(x) +0[-20,20] < [4]:h1(x) AND {L64}:[4]:h1(x) +0[-20,20] < [5]:h2(x) AND {L9}:[5]:h2(x) +0[-20,20] < [0]:n2(x) AND {L8}:[0]:n2(x) +0[-20,20] < [5]:h2(x) AND {L25}:[5]:h2(x) +0[-20,20] < [6]:n1(x) AND {L24}:[6]:n1(x) +0[-20,20] < [5]:h2(x) AND {L39}:[5]:h2(x) +0[-20,20] < [7]:n4(x) AND {L38}:[7]:n4(x) +0[-20,20] < [5]:h2(x) AND {L51}:[5]:h2(x) +0[-20,20] < [8]:n3(x) AND {L50}:[8]:n3(x) +0[-20,20] < [5]:h2(x) nVertexes = 9 List of nodes: [0]:n2(x), [1]:f(x), [2]:g1(x), [3]:g2(x), [4]:h1(x), [5]:h2(x), [6]:n1(x), [7]:n4(x), [8]:n3(x) Adjacency matrix: nRows = 9 nCols = 9 0 C C C C C C C C C 0 C C C C C C C C C 0 C C C C C C C C C 0 C C C C C C C C C 0 C C C C C C C C C 0 C C C C C C C C C 0 C C C C C C C C C 0 C C C C C C C C C 0 {L0}:[-1]:f(x) -10[-10,10] < [-1]:g1(x) AND {L1}:[-1]:g2(x) -30[-40,-20] < [-1]:f(x) AND {L2}:[-1]:g1(y) +15[5,25] < [-1]:g2(y) AND {L3}:[-1]:f(T) +45[35,55] < [-1]:h1(U) AND {L4}:[-1]:h2(U) -59[-69,49] < [-1]:f(T) AND {L5}:[-1]:h1(U) +1[-9,11] < [-1]:g2(T) OR {L6}:[-1]:g2(T) +46[36,56] < [-1]:h2(U) determinant:3.0 new formula: {L0}:[0]:f(x) -10[-10,10] < [1]:g1(x) AND {L1}:[2]:g2(x) -30[-40,-20] < [0]:f(x) AND {L2}:[3]:g1(y) +15[5,25] < [4]:g2(y) AND {L3}:[5]:f(T) +45[35,55] < [6]:h1(U) AND {L4}:[7]:h2(U) -59[-69,49] < [5]:f(T) AND {L5}:[6]:h1(U) +1[-9,11] < [8]:g2(T) OR {L6}:[8]:g2(T) +46[36,56] < [7]:h2(U) AND NOT {L3}:[5]:f(T) +45[35,55] < [6]:h1(U) OR NOT {L5}:[6]:h1(U) +1[-9,11] < [8]:g2(T) OR NOT {L1}:[2]:g2(x) -30[-40,-20] < [0]:f(x) AND NOT {L3}:[5]:f(T) +45[35,55] < [6]:h1(U) OR NOT {L5}:[6]:h1(U) +1[-9,11] < [8]:g2(T) OR NOT {L6}:[8]:g2(T) +46[36,56] < [7]:h2(U) OR NOT {L4}:[7]:h2(U) -59[-69,49] < [5]:f(T) new determinant:1.0 new determinant:7.0 nRows = 11 nCols = 12 1 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 0 -1 0 -1 0 -1 0 0 0 0 0 0 0 0 0 -1 -1 -1 -1 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 1 1 0 0 0 1 1 {L0}:[0]:f(x) -10[-10,10] < [1]:g1(x) AND {L1}:[2]:g2(x) -30[-40,-20] < [0]:f(x) AND {L2}:[3]:g1(y) +15[5,25] < [4]:g2(y) AND {L3}:[5]:f(T) +45[35,55] < [6]:h1(U) AND {L4}:[7]:h2(U) -59[-69,49] < [5]:f(T) AND NOT {L3}:[5]:f(T) +45[35,55] < [6]:h1(U) OR NOT {L5}:[6]:h1(U) +1[-9,11] < [8]:g2(T) OR NOT {L1}:[2]:g2(x) -30[-40,-20] < [0]:f(x) AND NOT {L3}:[5]:f(T) +45[35,55] < [6]:h1(U) OR NOT {L5}:[6]:h1(U) +1[-9,11] < [8]:g2(T) OR NOT {L6}:[8]:g2(T) +46[36,56] < [7]:h2(U) OR NOT {L4}:[7]:h2(U) -59[-69,49] < [5]:f(T) AND {L7}:[-1]:n2(z1) -10[-20,0] < [-1]:n1(z1) AND {L8}:[-1]:n4(z2) -10[-20,0] < [-1]:n3(z2) AND {L9}:[-1]:n1(V1) -15[-25,0] < [-1]:g1(y) AND {L5}:[-1]:h1(U) +1[-9,11] < [-1]:g2(T) OR {L6}:[-1]:g2(T) +46[36,56] < [-1]:h2(U) OR {L10}:[-1]:h1(U) -4[-14,6] < [-1]:n2(V1) OR {L11}:[-1]:h1(U) -4[-14,6] < [-1]:n4(V2) Constraints graph for formula: {L0}:[0]:f(x) -10[-10,10] < [1]:g1(x) AND {L1}:[2]:g2(x) -30[-40,-20] < [0]:f(x) AND {L2}:[3]:g1(y) +15[5,25] < [4]:g2(y) AND {L3}:[5]:f(T) +45[35,55] < [6]:h1(U) AND {L4}:[7]:h2(U) -59[-69,49] < [5]:f(T) AND NOT {L3}:[5]:f(T) +45[35,55] < [6]:h1(U) OR NOT {L5}:[6]:h1(U) +1[-9,11] < [8]:g2(T) OR NOT {L1}:[2]:g2(x) -30[-40,-20] < [0]:f(x) AND NOT {L3}:[5]:f(T) +45[35,55] < [6]:h1(U) OR NOT {L5}:[6]:h1(U) +1[-9,11] < [8]:g2(T) OR NOT {L6}:[8]:g2(T) +46[36,56] < [7]:h2(U) OR NOT {L4}:[7]:h2(U) -59[-69,49] < [5]:f(T) AND {L7}:[9]:n2(z1) -10[-20,0] < [10]:n1(z1) AND {L8}:[11]:n4(z2) -10[-20,0] < [12]:n3(z2) AND {L9}:[13]:n1(V1) -15[-25,0] < [3]:g1(y) AND {L5}:[6]:h1(U) +1[-9,11] < [8]:g2(T) OR {L6}:[8]:g2(T) +46[36,56] < [7]:h2(U) OR {L10}:[6]:h1(U) -4[-14,6] < [14]:n2(V1) OR {L11}:[6]:h1(U) -4[-14,6] < [15]:n4(V2) nVertexes = 16 List of nodes: [0]:f(x), [1]:g1(x), [2]:g2(x), [3]:g1(y), [4]:g2(y), [5]:f(T), [6]:h1(U), [7]:h2(U), [8]:g2(T), [9]:n2(z1), [10]:n1(z1), [11]:n4(z2), [12]:n3(z2), [13]:n1(V1), [14]:n2(V1), [15]:n4(V2) Adjacency matrix: nRows = 16 nCols = 16 0 C 0 0 0 S 0 0 0 0 0 0 0 0 0 0 0 0 0 S 0 0 0 0 0 0 0 0 0 0 0 0 C 0 0 0 S 0 0 0 S 0 0 0 0 0 0 0 0 S 0 0 C 0 0 0 0 0 0 0 0 0 0 0 0 0 S 0 0 0 0 0 S 0 0 0 0 0 0 0 S 0 0 0 0 0 C 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 C 0 0 0 0 0 C C 0 0 0 0 0 C 0 0 0 0 0 0 0 0 0 0 0 0 S 0 S 0 0 C 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 C 0 0 0 S 0 0 0 0 0 0 0 0 0 0 0 0 0 0 S 0 0 0 0 0 0 0 0 0 0 0 0 0 0 C 0 0 S 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 C 0 0 0 0 0 0 S 0 0 0 0 0 0 0 0 0 0 0 0 0 0 S 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 S 0 0 0 0 No exit edge nodes: [12]:n3(z2) No entry edge nodes: new clauses,increments: Leaving from node:[12]:n3(z2) [0]:f(x) [1]:g1(x) [2]:g2(x) [3]:g1(y) [4]:g2(y) [5]:f(T) [6]:h1(U) [7]:h2(U) [8]:g2(T) [9]:n2(z1) [10]:n1(z1) [11]:n4(z2) [12]:n3(z2) [13]:n1(V1) [14]:n2(V1) [15]:n4(V2) 0 : (NOT {L3}:[5]:f(T) +45[35,55] < [6]:h1(U) OR NOT {L11}:[6]:h1(U) -4[-14,6] < [15]:n4(V2) OR NOT {L8}:[11]:n4(z2) -10[-20,0] < [12]:n3(z2) OR NOT {L13}:[-1]:n3(V2) +0[-20,20] < [-1]:n1(V1) OR NOT {L9}:[13]:n1(V1) -15[-25,0] < [3]:g1(y) OR NOT {L2}:[3]:g1(y) +15[5,25] < [4]:g2(y) OR NOT {L1}:[2]:g2(x) -30[-40,-20] < [0]:f(x);-2.0) 1 : (NOT {L3}:[5]:f(T) +45[35,55] < [6]:h1(U) OR NOT {L11}:[6]:h1(U) -4[-14,6] < [15]:n4(V2) OR NOT {L8}:[11]:n4(z2) -10[-20,0] < [12]:n3(z2) OR NOT {L13}:[-1]:n3(V2) +10[-20,20] < [-1]:n2(V1) OR NOT {L7}:[9]:n2(z1) -10[-20,0] < [10]:n1(z1) OR NOT {L9}:[13]:n1(V1) -15[-25,0] < [3]:g1(y) OR NOT {L2}:[3]:g1(y) +15[5,25] < [4]:g2(y) OR NOT {L1}:[2]:g2(x) -30[-40,-20] < [0]:f(x);-2.0) 2 : (NOT {L11}:[6]:h1(U) -4[-14,6] < [15]:n4(V2) OR NOT {L8}:[11]:n4(z2) -10[-20,0] < [12]:n3(z2) OR NOT {L13}:[-1]:n3(V2) +15[-20,20] < [-1]:h1(U);-2.0) 3 : (NOT {L3}:[5]:f(T) +45[35,55] < [6]:h1(U) OR NOT {L11}:[6]:h1(U) -4[-14,6] < [15]:n4(V2) OR NOT {L8}:[11]:n4(z2) -10[-20,0] < [12]:n3(z2) OR NOT {L13}:[-1]:n3(V2) +0[-20,20] < [-1]:g2(T) OR NOT {L1}:[2]:g2(x) -30[-40,-20] < [0]:f(x);-2.0) 4 : (NOT {L3}:[5]:f(T) +45[35,55] < [6]:h1(U) OR NOT {L11}:[6]:h1(U) -4[-14,6] < [15]:n4(V2) OR NOT {L8}:[11]:n4(z2) -10[-20,0] < [12]:n3(z2) OR NOT {L13}:[-1]:n3(V2) -15[-20,20] < [-1]:g1(T) OR NOT {L2}:[3]:g1(y) +15[5,25] < [4]:g2(y) OR NOT {L1}:[2]:g2(x) -30[-40,-20] < [0]:f(x);-2.0) 5 : (NOT {L6}:[8]:g2(T) +46[36,56] < [7]:h2(U) OR NOT {L4}:[7]:h2(U) -59[-69,49] < [5]:f(T) OR NOT {L3}:[5]:f(T) +45[35,55] < [6]:h1(U) OR NOT {L11}:[6]:h1(U) -4[-14,6] < [15]:n4(V2) OR NOT {L8}:[11]:n4(z2) -10[-20,0] < [12]:n3(z2) OR NOT {L13}:[-1]:n3(V2) -17[-20,20] < [-1]:n1(V1) OR NOT {L9}:[13]:n1(V1) -15[-25,0] < [3]:g1(y) OR NOT {L2}:[3]:g1(y) +15[5,25] < [4]:g2(y);-1.0) 6 : (NOT {L2}:[3]:g1(y) +15[5,25] < [4]:g2(y) OR NOT {L6}:[8]:g2(T) +46[36,56] < [7]:h2(U) OR NOT {L4}:[7]:h2(U) -59[-69,49] < [5]:f(T) OR NOT {L3}:[5]:f(T) +45[35,55] < [6]:h1(U) OR NOT {L11}:[6]:h1(U) -4[-14,6] < [15]:n4(V2) OR NOT {L8}:[11]:n4(z2) -10[-20,0] < [12]:n3(z2) OR NOT {L13}:[-1]:n3(V2) -17[-20,20] < [-1]:n1(V1) OR NOT {L9}:[13]:n1(V1) -15[-25,0] < [3]:g1(y);-1.0) 7 : (NOT {L6}:[8]:g2(T) +46[36,56] < [7]:h2(U) OR NOT {L4}:[7]:h2(U) -59[-69,49] < [5]:f(T) OR NOT {L3}:[5]:f(T) +45[35,55] < [6]:h1(U) OR NOT {L11}:[6]:h1(U) -4[-14,6] < [15]:n4(V2) OR NOT {L8}:[11]:n4(z2) -10[-20,0] < [12]:n3(z2) OR NOT {L13}:[-1]:n3(V2) -7[-20,20] < [-1]:n2(V1) OR NOT {L7}:[9]:n2(z1) -10[-20,0] < [10]:n1(z1) OR NOT {L9}:[13]:n1(V1) -15[-25,0] < [3]:g1(y) OR NOT {L2}:[3]:g1(y) +15[5,25] < [4]:g2(y);-1.0) 8 : (NOT {L2}:[3]:g1(y) +15[5,25] < [4]:g2(y) OR NOT {L6}:[8]:g2(T) +46[36,56] < [7]:h2(U) OR NOT {L4}:[7]:h2(U) -59[-69,49] < [5]:f(T) OR NOT {L3}:[5]:f(T) +45[35,55] < [6]:h1(U) OR NOT {L11}:[6]:h1(U) -4[-14,6] < [15]:n4(V2) OR NOT {L8}:[11]:n4(z2) -10[-20,0] < [12]:n3(z2) OR NOT {L13}:[-1]:n3(V2) -7[-20,20] < [-1]:n2(V1) OR NOT {L7}:[9]:n2(z1) -10[-20,0] < [10]:n1(z1) OR NOT {L9}:[13]:n1(V1) -15[-25,0] < [3]:g1(y);-1.0) 9 : (NOT {L0}:[0]:f(x) -10[-10,10] < [1]:g1(x) OR NOT {L2}:[3]:g1(y) +15[5,25] < [4]:g2(y) OR NOT {L6}:[8]:g2(T) +46[36,56] < [7]:h2(U) OR NOT {L4}:[7]:h2(U) -59[-69,49] < [5]:f(T) OR NOT {L3}:[5]:f(T) +45[35,55] < [6]:h1(U) OR NOT {L11}:[6]:h1(U) -4[-14,6] < [15]:n4(V2) OR NOT {L8}:[11]:n4(z2) -10[-20,0] < [12]:n3(z2) OR NOT {L13}:[-1]:n3(V2) +8[-20,20] < [-1]:g2(T) OR NOT {L1}:[2]:g2(x) -30[-40,-20] < [0]:f(x);-1.0) 10 : (NOT {L6}:[8]:g2(T) +46[36,56] < [7]:h2(U) OR NOT {L4}:[7]:h2(U) -59[-69,49] < [5]:f(T) OR NOT {L3}:[5]:f(T) +45[35,55] < [6]:h1(U) OR NOT {L11}:[6]:h1(U) -4[-14,6] < [15]:n4(V2) OR NOT {L8}:[11]:n4(z2) -10[-20,0] < [12]:n3(z2) OR NOT {L13}:[-1]:n3(V2) -17[-20,20] < [-1]:g2(T);-1.0) 11 : (NOT {L3}:[5]:f(T) +45[35,55] < [6]:h1(U) OR NOT {L11}:[6]:h1(U) -4[-14,6] < [15]:n4(V2) OR NOT {L8}:[11]:n4(z2) -10[-20,0] < [12]:n3(z2) OR NOT {L13}:[-1]:n3(V2) -17[-20,20] < [-1]:g2(T) OR NOT {L6}:[8]:g2(T) +46[36,56] < [7]:h2(U) OR NOT {L4}:[7]:h2(U) -59[-69,49] < [5]:f(T);-1.0) Pick one: adding clause: NOT {L3}:[5]:f(T) +45[35,55] < [6]:h1(U) OR NOT {L11}:[6]:h1(U) -4[-14,6] < [15]:n4(V2) OR NOT {L8}:[11]:n4(z2) -10[-20,0] < [12]:n3(z2) OR NOT {L13}:[-1]:n3(V2) +0[-20,20] < [-1]:n1(V1) OR NOT {L9}:[13]:n1(V1) -15[-25,0] < [3]:g1(y) OR NOT {L2}:[3]:g1(y) +15[5,25] < [4]:g2(y) OR NOT {L1}:[2]:g2(x) -30[-40,-20] < [0]:f(x) det in addfromclauseincrementlist:1.0 new determinant:1.0 new determinant:1.0 We have found the following negative cycles. Pick one to modify: 0: [[0]:f(x) -10[-10,10] < [1]:g1(x), [1]:g1(x)--[3]:g1(y), [3]:g1(y) +15[5,25] < [4]:g2(y), [4]:g2(y)--[2]:g2(x), [2]:g2(x) -30[-40,-20] < [0]:f(x)] 1: [[0]:f(x) -10[-10,10] < [1]:g1(x), [1]:g1(x)--[3]:g1(y), [3]:g1(y) +15[5,25] < [4]:g2(y), [4]:g2(y)--[8]:g2(T), [8]:g2(T) +46[36,56] < [7]:h2(U), [7]:h2(U) -59[-69,49] < [5]:f(T), [5]:f(T)--[0]:f(x)] You have chosen to modify the clause: 0: NOT {L0}:[0]:f(x) -10[-10,10] < [1]:g1(x) OR 1: NOT {L2}:[3]:g1(y) +15[5,25] < [4]:g2(y) OR 2: NOT {L1}:[2]:g2(x) -30[-40,-20] < [0]:f(x) The weight of which literal do you wish to modify? You chose to modify literal:NOT {L0}:[0]:f(x) -10[-10,10] < [1]:g1(x) Determinant:0.0 Formula: {L0}:[0]:f(x) +10[-10,10] < [1]:g1(x) AND {L1}:[2]:g2(x) -30[-40,-20] < [0]:f(x) AND {L2}:[3]:g1(y) +21[5,25] < [4]:g2(y) AND {L3}:[5]:f(T) +45[35,55] < [6]:h1(U) AND {L4}:[7]:h2(U) -59[-69,49] < [5]:f(T) AND NOT {L3}:[5]:f(T) +45[35,55] < [6]:h1(U) OR NOT {L5}:[6]:h1(U) +1[-9,11] < [8]:g2(T) OR NOT {L1}:[2]:g2(x) -30[-40,-20] < [0]:f(x) AND NOT {L3}:[5]:f(T) +45[35,55] < [6]:h1(U) OR NOT {L5}:[6]:h1(U) +1[-9,11] < [8]:g2(T) OR NOT {L6}:[8]:g2(T) +46[36,56] < [7]:h2(U) OR NOT {L4}:[7]:h2(U) -59[-69,49] < [5]:f(T) AND {L7}:[9]:n2(z1) -10[-20,0] < [10]:n1(z1) AND {L8}:[11]:n4(z2) -10[-20,0] < [12]:n3(z2) AND {L9}:[13]:n1(V1) -15[-25,0] < [3]:g1(y) AND {L5}:[6]:h1(U) +1[-9,11] < [8]:g2(T) OR {L6}:[8]:g2(T) +46[36,56] < [7]:h2(U) OR {L10}:[6]:h1(U) -4[-14,6] < [14]:n2(V1) OR {L11}:[6]:h1(U) -4[-14,6] < [15]:n4(V2) AND NOT {L3}:[5]:f(T) +45[35,55] < [6]:h1(U) OR NOT {L10}:[6]:h1(U) -4[-14,6] < [14]:n2(V1) OR NOT {L7}:[9]:n2(z1) -10[-20,0] < [10]:n1(z1) OR NOT {L9}:[13]:n1(V1) -15[-25,0] < [3]:g1(y) OR NOT {L2}:[3]:g1(y) +21[5,25] < [4]:g2(y) OR NOT {L1}:[2]:g2(x) -30[-40,-20] < [0]:f(x) AND NOT {L6}:[8]:g2(T) +46[36,56] < [7]:h2(U) OR NOT {L4}:[7]:h2(U) -59[-69,49] < [5]:f(T) OR NOT {L3}:[5]:f(T) +45[35,55] < [6]:h1(U) OR NOT {L10}:[6]:h1(U) -4[-14,6] < [14]:n2(V1) OR NOT {L7}:[9]:n2(z1) -10[-20,0] < [10]:n1(z1) OR NOT {L9}:[13]:n1(V1) -15[-25,0] < [3]:g1(y) OR NOT {L2}:[3]:g1(y) +21[5,25] < [4]:g2(y) AND NOT {L3}:[5]:f(T) +45[35,55] < [6]:h1(U) OR NOT {L11}:[6]:h1(U) -4[-14,6] < [15]:n4(V2) OR NOT {L8}:[11]:n4(z2) -10[-20,0] < [12]:n3(z2) OR NOT {L12}:[16]:n3(V2) +0[-20,20] < [13]:n1(V1) OR NOT {L9}:[13]:n1(V1) -15[-25,0] < [3]:g1(y) OR NOT {L2}:[3]:g1(y) +21[5,25] < [4]:g2(y) OR NOT {L1}:[2]:g2(x) -30[-40,-20] < [0]:f(x) AND {L12}:[16]:n3(V2) +0[-20,20] < [13]:n1(V1) AND NOT {L0}:[0]:f(x) +10[-10,10] < [1]:g1(x) OR NOT {L2}:[3]:g1(y) +21[5,25] < [4]:g2(y) OR NOT {L1}:[2]:g2(x) -30[-40,-20] < [0]:f(x) Determinant:0.0 Final formula: {L0}:[0]:f(x) +10[-10,10] < [1]:g1(x) AND {L1}:[2]:g2(x) -30[-40,-20] < [0]:f(x) AND {L2}:[3]:g1(y) +21[5,25] < [4]:g2(y) AND {L3}:[5]:f(T) +45[35,55] < [6]:h1(U) AND {L4}:[7]:h2(U) -59[-69,49] < [5]:f(T) AND NOT {L3}:[5]:f(T) +45[35,55] < [6]:h1(U) OR NOT {L5}:[6]:h1(U) +1[-9,11] < [8]:g2(T) OR NOT {L1}:[2]:g2(x) -30[-40,-20] < [0]:f(x) AND NOT {L3}:[5]:f(T) +45[35,55] < [6]:h1(U) OR NOT {L5}:[6]:h1(U) +1[-9,11] < [8]:g2(T) OR NOT {L6}:[8]:g2(T) +46[36,56] < [7]:h2(U) OR NOT {L4}:[7]:h2(U) -59[-69,49] < [5]:f(T) AND {L7}:[9]:n2(z1) -10[-20,0] < [10]:n1(z1) AND {L8}:[11]:n4(z2) -10[-20,0] < [12]:n3(z2) AND {L9}:[13]:n1(V1) -15[-25,0] < [3]:g1(y) AND {L5}:[6]:h1(U) +1[-9,11] < [8]:g2(T) OR {L6}:[8]:g2(T) +46[36,56] < [7]:h2(U) OR {L10}:[6]:h1(U) -4[-14,6] < [14]:n2(V1) OR {L11}:[6]:h1(U) -4[-14,6] < [15]:n4(V2) AND NOT {L3}:[5]:f(T) +45[35,55] < [6]:h1(U) OR NOT {L10}:[6]:h1(U) -4[-14,6] < [14]:n2(V1) OR NOT {L7}:[9]:n2(z1) -10[-20,0] < [10]:n1(z1) OR NOT {L9}:[13]:n1(V1) -15[-25,0] < [3]:g1(y) OR NOT {L2}:[3]:g1(y) +21[5,25] < [4]:g2(y) OR NOT {L1}:[2]:g2(x) -30[-40,-20] < [0]:f(x) AND NOT {L6}:[8]:g2(T) +46[36,56] < [7]:h2(U) OR NOT {L4}:[7]:h2(U) -59[-69,49] < [5]:f(T) OR NOT {L3}:[5]:f(T) +45[35,55] < [6]:h1(U) OR NOT {L10}:[6]:h1(U) -4[-14,6] < [14]:n2(V1) OR NOT {L7}:[9]:n2(z1) -10[-20,0] < [10]:n1(z1) OR NOT {L9}:[13]:n1(V1) -15[-25,0] < [3]:g1(y) OR NOT {L2}:[3]:g1(y) +21[5,25] < [4]:g2(y) AND NOT {L3}:[5]:f(T) +45[35,55] < [6]:h1(U) OR NOT {L11}:[6]:h1(U) -4[-14,6] < [15]:n4(V2) OR NOT {L8}:[11]:n4(z2) -10[-20,0] < [12]:n3(z2) OR NOT {L12}:[16]:n3(V2) +0[-20,20] < [13]:n1(V1) OR NOT {L9}:[13]:n1(V1) -15[-25,0] < [3]:g1(y) OR NOT {L2}:[3]:g1(y) +21[5,25] < [4]:g2(y) OR NOT {L1}:[2]:g2(x) -30[-40,-20] < [0]:f(x) AND {L12}:[16]:n3(V2) +0[-20,20] < [13]:n1(V1) AND NOT {L0}:[0]:f(x) +10[-10,10] < [1]:g1(x) OR NOT {L2}:[3]:g1(y) +21[5,25] < [4]:g2(y) OR NOT {L1}:[2]:g2(x) -30[-40,-20] < [0]:f(x) Determinant:0.0