--------------------Configuration: adrtl - j2sdk1.5.0 <Default> - <Default>--------------------
{L0}:[-1]:f(x) +0 < [-1]:g1(x) AND 
{L1}:[-1]:g2(x) -30 < [-1]:f(x) AND 
{L2}:[-1]:g1(y) +15 < [-1]:g2(y) AND 
{L3}:[-1]:f(T) +45 < [-1]:h1(U) AND 
{L4}:[-1]:h2(U) -59 < [-1]:f(T) AND 
{L5}:[-1]:h1(U) +1 < [-1]:g2(T) OR {L6}:[-1]:g2(T) +46 < [-1]:h2(U)

determinant:3.0
new determinant:3.0
nRows = 11
nCols = 11
 1  0  0  0  0  0  0  0  0  0  0 
 0  1  0  0  0  0  0  0  0  0  0 
 0  0  1  0  0  0  0  0  0  0  0 
 0  0  0  1  0  0  0  0  0  0  0 
 0  0  0  0  1  0  0  0  0  0  0 
-1  0 -1  0 -1  0 -1  0  0  0  0 
 0 -1  0 -1  0 -1  0  0  0  0  0 
 0  0  0 -1 -1 -1 -1  0  0  0  0 
 0  0  0  0  0  0  0  1  0  0  0 
 0  0  0  0  0  0  0  0  1  0  0 
 0  0  0  0  0  1  1  0  0  1  1 

{L0}:[0]:f(x) +0 < [1]:g1(x) AND 
{L1}:[2]:g2(x) -30 < [0]:f(x) AND 
{L2}:[3]:g1(y) +15 < [4]:g2(y) AND 
{L3}:[5]:f(T) +45 < [6]:h1(U) AND 
{L4}:[7]:h2(U) -59 < [5]:f(T) AND 
NOT {L0}:[0]:f(x) +0 < [1]:g1(x) OR NOT {L2}:[3]:g1(y) +15 < [4]:g2(y) OR NOT {L6}:[8]:g2(T) +46 < [7]:h2(U) OR NOT {L4}:[7]:h2(U) -59 < [5]:f(T) AND 
NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L5}:[6]:h1(U) +1 < [8]:g2(T) OR NOT {L1}:[2]:g2(x) -30 < [0]:f(x) AND 
NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L5}:[6]:h1(U) +1 < [8]:g2(T) OR NOT {L6}:[8]:g2(T) +46 < [7]:h2(U) OR NOT {L4}:[7]:h2(U) -59 < [5]:f(T) AND 
{L7}:[-1]:n2(z1) -10 < [-1]:n1(z1) AND 
{L8}:[-1]:n4(z2) -10 < [-1]:n3(z2) AND 
{L5}:[-1]:h1(U) +1 < [-1]:g2(T) OR {L6}:[-1]:g2(T) +46 < [-1]:h2(U) OR {L9}:[-1]:h1(U) -4 < [-1]:n2(V1) OR {L10}:[-1]:h1(U) -4 < [-1]:n4(V2)

Constraints graph for formula:
{L0}:[0]:f(x) +0 < [1]:g1(x) AND 
{L1}:[2]:g2(x) -30 < [0]:f(x) AND 
{L2}:[3]:g1(y) +15 < [4]:g2(y) AND 
{L3}:[5]:f(T) +45 < [6]:h1(U) AND 
{L4}:[7]:h2(U) -59 < [5]:f(T) AND 
NOT {L0}:[0]:f(x) +0 < [1]:g1(x) OR NOT {L2}:[3]:g1(y) +15 < [4]:g2(y) OR NOT {L6}:[8]:g2(T) +46 < [7]:h2(U) OR NOT {L4}:[7]:h2(U) -59 < [5]:f(T) AND 
NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L5}:[6]:h1(U) +1 < [8]:g2(T) OR NOT {L1}:[2]:g2(x) -30 < [0]:f(x) AND 
NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L5}:[6]:h1(U) +1 < [8]:g2(T) OR NOT {L6}:[8]:g2(T) +46 < [7]:h2(U) OR NOT {L4}:[7]:h2(U) -59 < [5]:f(T) AND 
{L7}:[9]:n2(z1) -10 < [10]:n1(z1) AND 
{L8}:[11]:n4(z2) -10 < [12]:n3(z2) AND 
{L5}:[6]:h1(U) +1 < [8]:g2(T) OR {L6}:[8]:g2(T) +46 < [7]:h2(U) OR {L9}:[6]:h1(U) -4 < [13]:n2(V1) OR {L10}:[6]:h1(U) -4 < [14]:n4(V2)

nVertexes = 15
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]:n2(V1), [14]:n4(V2)
Adjacency matrix:
nRows = 15
nCols = 15
0 C 0 0 0 S 0 0 0 0 0 0 0 0 0 
0 0 0 S 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 S 0 0 C 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 
S 0 0 0 0 0 C 0 0 0 0 0 0 0 0 
0 0 0 0 0 0 0 0 C 0 0 0 0 C C 
0 0 0 0 0 C 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 C 0 0 S 0 
0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 
0 0 0 0 0 0 0 0 0 0 0 0 C 0 S 
0 0 0 0 0 0 0 0 0 0 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 S 0 0 0 


No exit edge nodes:
[10]:n1(z1)
[12]:n3(z2)
No entry edge nodes:
new clauses,increments:
Leaving from node:[10]:n1(z1)
0 : (NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L9}:[6]:h1(U) -4 < [13]:n2(V1) OR NOT {L7}:[9]:n2(z1) -10 < [10]:n1(z1) OR NOT {L11}:[-1]:n1(V1) +29 < [-1]:h2(U) OR NOT {L4}:[7]:h2(U) -59 < [5]:f(T);-2.0) 
1 : (NOT {L9}:[6]:h1(U) -4 < [13]:n2(V1) OR NOT {L7}:[9]:n2(z1) -10 < [10]:n1(z1) OR NOT {L11}:[-1]:n1(V1) +15 < [-1]:h1(U);-2.0) 
2 : (NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L9}:[6]:h1(U) -4 < [13]:n2(V1) OR NOT {L7}:[9]:n2(z1) -10 < [10]:n1(z1) OR NOT {L11}:[-1]:n1(V1) +0 < [-1]:g2(T) OR NOT {L1}:[2]:g2(x) -30 < [0]:f(x);-2.0) 
3 : (NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L9}:[6]:h1(U) -4 < [13]:n2(V1) OR NOT {L7}:[9]:n2(z1) -10 < [10]:n1(z1) OR NOT {L11}:[-1]:n1(V1) +0 < [-1]:g2(T) OR NOT {L1}:[2]:g2(x) -30 < [0]:f(x);-2.0) 
4 : (NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L9}:[6]:h1(U) -4 < [13]:n2(V1) OR NOT {L7}:[9]:n2(z1) -10 < [10]:n1(z1) OR NOT {L11}:[-1]:n1(V1) +0 < [-1]:g2(T) OR NOT {L1}:[2]:g2(x) -30 < [0]:f(x);-2.0) 
5 : (NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L9}:[6]:h1(U) -4 < [13]:n2(V1) OR NOT {L7}:[9]:n2(z1) -10 < [10]:n1(z1) OR NOT {L11}:[-1]:n1(V1) -15 < [-1]:g1(T) OR NOT {L2}:[3]:g1(y) +15 < [4]:g2(y) OR NOT {L1}:[2]:g2(x) -30 < [0]:f(x);-2.0) 
6 : (NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L9}:[6]:h1(U) -4 < [13]:n2(V1) OR NOT {L7}:[9]:n2(z1) -10 < [10]:n1(z1) OR NOT {L11}:[-1]:n1(V1) -15 < [-1]:g1(T) OR NOT {L2}:[3]:g1(y) +15 < [4]:g2(y) OR NOT {L1}:[2]:g2(x) -30 < [0]:f(x);-2.0) 
7 : (NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L9}:[6]:h1(U) -4 < [13]:n2(V1) OR NOT {L7}:[9]:n2(z1) -10 < [10]:n1(z1) OR NOT {L11}:[-1]:n1(V1) -30 < [-1]:f(T);-2.0) 
8 : (NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L9}:[6]:h1(U) -4 < [13]:n2(V1) OR NOT {L7}:[9]:n2(z1) -10 < [10]:n1(z1) OR NOT {L11}:[-1]:n1(V1) -30 < [-1]:f(T);-2.0) 
9 : (NOT {L0}:[0]:f(x) +0 < [1]:g1(x) OR NOT {L2}:[3]:g1(y) +15 < [4]:g2(y) OR NOT {L6}:[8]:g2(T) +46 < [7]:h2(U) OR NOT {L4}:[7]:h2(U) -59 < [5]:f(T) OR NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L9}:[6]:h1(U) -4 < [13]:n2(V1) OR NOT {L7}:[9]:n2(z1) -10 < [10]:n1(z1) OR NOT {L11}:[-1]:n1(V1) -2 < [-1]:g2(T) OR NOT {L1}:[2]:g2(x) -30 < [0]:f(x);0.0) 
10 : (NOT {L6}:[8]:g2(T) +46 < [7]:h2(U) OR NOT {L4}:[7]:h2(U) -59 < [5]:f(T) OR NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L9}:[6]:h1(U) -4 < [13]:n2(V1) OR NOT {L7}:[9]:n2(z1) -10 < [10]:n1(z1) OR NOT {L11}:[-1]:n1(V1) -17 < [-1]:g2(T);0.0) 
11 : (NOT {L6}:[8]:g2(T) +46 < [7]:h2(U) OR NOT {L4}:[7]:h2(U) -59 < [5]:f(T) OR NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L9}:[6]:h1(U) -4 < [13]:n2(V1) OR NOT {L7}:[9]:n2(z1) -10 < [10]:n1(z1) OR NOT {L11}:[-1]:n1(V1) -17 < [-1]:g2(T);0.0) 
12 : (NOT {L6}:[8]:g2(T) +46 < [7]:h2(U) OR NOT {L4}:[7]:h2(U) -59 < [5]:f(T) OR NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L9}:[6]:h1(U) -4 < [13]:n2(V1) OR NOT {L7}:[9]:n2(z1) -10 < [10]:n1(z1) OR NOT {L11}:[-1]:n1(V1) -17 < [-1]:g2(T);0.0) 
13 : (NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L9}:[6]:h1(U) -4 < [13]:n2(V1) OR NOT {L7}:[9]:n2(z1) -10 < [10]:n1(z1) OR NOT {L11}:[-1]:n1(V1) -17 < [-1]:g2(T) OR NOT {L6}:[8]:g2(T) +46 < [7]:h2(U) OR NOT {L4}:[7]:h2(U) -59 < [5]:f(T);0.0) 
14 : (NOT {L2}:[3]:g1(y) +15 < [4]:g2(y) OR NOT {L6}:[8]:g2(T) +46 < [7]:h2(U) OR NOT {L4}:[7]:h2(U) -59 < [5]:f(T) OR NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L9}:[6]:h1(U) -4 < [13]:n2(V1) OR NOT {L7}:[9]:n2(z1) -10 < [10]:n1(z1) OR NOT {L11}:[-1]:n1(V1) -32 < [-1]:g1(T);0.0) 
15 : (NOT {L6}:[8]:g2(T) +46 < [7]:h2(U) OR NOT {L4}:[7]:h2(U) -59 < [5]:f(T) OR NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L9}:[6]:h1(U) -4 < [13]:n2(V1) OR NOT {L7}:[9]:n2(z1) -10 < [10]:n1(z1) OR NOT {L11}:[-1]:n1(V1) -32 < [-1]:g1(T) OR NOT {L2}:[3]:g1(y) +15 < [4]:g2(y);0.0) 
16 : (NOT {L2}:[3]:g1(y) +15 < [4]:g2(y) OR NOT {L6}:[8]:g2(T) +46 < [7]:h2(U) OR NOT {L4}:[7]:h2(U) -59 < [5]:f(T) OR NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L9}:[6]:h1(U) -4 < [13]:n2(V1) OR NOT {L7}:[9]:n2(z1) -10 < [10]:n1(z1) OR NOT {L11}:[-1]:n1(V1) -32 < [-1]:g1(T);0.0) 
17 : (NOT {L0}:[0]:f(x) +0 < [1]:g1(x) OR NOT {L2}:[3]:g1(y) +15 < [4]:g2(y) OR NOT {L6}:[8]:g2(T) +46 < [7]:h2(U) OR NOT {L4}:[7]:h2(U) -59 < [5]:f(T) OR NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L9}:[6]:h1(U) -4 < [13]:n2(V1) OR NOT {L7}:[9]:n2(z1) -10 < [10]:n1(z1) OR NOT {L11}:[-1]:n1(V1) -32 < [-1]:f(T);0.0) 
-1: Do not wish to modify this node
Pick one:
5
det in addfromclauseincrementlist:1.0
new determinant:1.0
0 : (NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L9}:[6]:h1(U) -4 < [13]:n2(V1) OR NOT {L7}:[9]:n2(z1) -10 < [10]:n1(z1) OR NOT {L11}:[-1]:n1(V1) +29 < [-1]:h2(U) OR NOT {L4}:[7]:h2(U) -59 < [5]:f(T);0.0) 
1 : (NOT {L9}:[6]:h1(U) -4 < [13]:n2(V1) OR NOT {L7}:[9]:n2(z1) -10 < [10]:n1(z1) OR NOT {L11}:[-1]:n1(V1) +15 < [-1]:h1(U);0.0) 
2 : (NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L9}:[6]:h1(U) -4 < [13]:n2(V1) OR NOT {L7}:[9]:n2(z1) -10 < [10]:n1(z1) OR NOT {L11}:[-1]:n1(V1) +0 < [-1]:g2(T) OR NOT {L1}:[2]:g2(x) -30 < [0]:f(x);0.0) 
3 : (NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L9}:[6]:h1(U) -4 < [13]:n2(V1) OR NOT {L7}:[9]:n2(z1) -10 < [10]:n1(z1) OR NOT {L11}:[-1]:n1(V1) +0 < [-1]:g2(T) OR NOT {L1}:[2]:g2(x) -30 < [0]:f(x);0.0) 
4 : (NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L9}:[6]:h1(U) -4 < [13]:n2(V1) OR NOT {L7}:[9]:n2(z1) -10 < [10]:n1(z1) OR NOT {L11}:[-1]:n1(V1) +0 < [-1]:g2(T) OR NOT {L1}:[2]:g2(x) -30 < [0]:f(x);0.0) 
5 : (NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L9}:[6]:h1(U) -4 < [13]:n2(V1) OR NOT {L7}:[9]:n2(z1) -10 < [10]:n1(z1) OR NOT {L11}:[-1]:n1(V1) -15 < [-1]:g1(T) OR NOT {L2}:[3]:g1(y) +15 < [4]:g2(y) OR NOT {L1}:[2]:g2(x) -30 < [0]:f(x);0.0) 
6 : (NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L9}:[6]:h1(U) -4 < [13]:n2(V1) OR NOT {L7}:[9]:n2(z1) -10 < [10]:n1(z1) OR NOT {L11}:[-1]:n1(V1) -30 < [-1]:f(T);0.0) 
7 : (NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L9}:[6]:h1(U) -4 < [13]:n2(V1) OR NOT {L7}:[9]:n2(z1) -10 < [10]:n1(z1) OR NOT {L11}:[-1]:n1(V1) -30 < [-1]:f(T);0.0) 
8 : (NOT {L0}:[0]:f(x) +0 < [1]:g1(x) OR NOT {L2}:[3]:g1(y) +15 < [4]:g2(y) OR NOT {L6}:[8]:g2(T) +46 < [7]:h2(U) OR NOT {L4}:[7]:h2(U) -59 < [5]:f(T) OR NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L9}:[6]:h1(U) -4 < [13]:n2(V1) OR NOT {L7}:[9]:n2(z1) -10 < [10]:n1(z1) OR NOT {L11}:[-1]:n1(V1) -2 < [-1]:g2(T) OR NOT {L1}:[2]:g2(x) -30 < [0]:f(x);0.0) 
9 : (NOT {L6}:[8]:g2(T) +46 < [7]:h2(U) OR NOT {L4}:[7]:h2(U) -59 < [5]:f(T) OR NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L9}:[6]:h1(U) -4 < [13]:n2(V1) OR NOT {L7}:[9]:n2(z1) -10 < [10]:n1(z1) OR NOT {L11}:[-1]:n1(V1) -17 < [-1]:g2(T);0.0) 
10 : (NOT {L6}:[8]:g2(T) +46 < [7]:h2(U) OR NOT {L4}:[7]:h2(U) -59 < [5]:f(T) OR NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L9}:[6]:h1(U) -4 < [13]:n2(V1) OR NOT {L7}:[9]:n2(z1) -10 < [10]:n1(z1) OR NOT {L11}:[-1]:n1(V1) -17 < [-1]:g2(T);0.0) 
11 : (NOT {L6}:[8]:g2(T) +46 < [7]:h2(U) OR NOT {L4}:[7]:h2(U) -59 < [5]:f(T) OR NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L9}:[6]:h1(U) -4 < [13]:n2(V1) OR NOT {L7}:[9]:n2(z1) -10 < [10]:n1(z1) OR NOT {L11}:[-1]:n1(V1) -17 < [-1]:g2(T);0.0) 
12 : (NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L9}:[6]:h1(U) -4 < [13]:n2(V1) OR NOT {L7}:[9]:n2(z1) -10 < [10]:n1(z1) OR NOT {L11}:[-1]:n1(V1) -17 < [-1]:g2(T) OR NOT {L6}:[8]:g2(T) +46 < [7]:h2(U) OR NOT {L4}:[7]:h2(U) -59 < [5]:f(T);0.0) 
13 : (NOT {L2}:[3]:g1(y) +15 < [4]:g2(y) OR NOT {L6}:[8]:g2(T) +46 < [7]:h2(U) OR NOT {L4}:[7]:h2(U) -59 < [5]:f(T) OR NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L9}:[6]:h1(U) -4 < [13]:n2(V1) OR NOT {L7}:[9]:n2(z1) -10 < [10]:n1(z1) OR NOT {L11}:[-1]:n1(V1) -32 < [-1]:g1(T);0.0) 
14 : (NOT {L6}:[8]:g2(T) +46 < [7]:h2(U) OR NOT {L4}:[7]:h2(U) -59 < [5]:f(T) OR NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L9}:[6]:h1(U) -4 < [13]:n2(V1) OR NOT {L7}:[9]:n2(z1) -10 < [10]:n1(z1) OR NOT {L11}:[-1]:n1(V1) -32 < [-1]:g1(T) OR NOT {L2}:[3]:g1(y) +15 < [4]:g2(y);0.0) 
15 : (NOT {L2}:[3]:g1(y) +15 < [4]:g2(y) OR NOT {L6}:[8]:g2(T) +46 < [7]:h2(U) OR NOT {L4}:[7]:h2(U) -59 < [5]:f(T) OR NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L9}:[6]:h1(U) -4 < [13]:n2(V1) OR NOT {L7}:[9]:n2(z1) -10 < [10]:n1(z1) OR NOT {L11}:[-1]:n1(V1) -32 < [-1]:g1(T);0.0) 
16 : (NOT {L0}:[0]:f(x) +0 < [1]:g1(x) OR NOT {L2}:[3]:g1(y) +15 < [4]:g2(y) OR NOT {L6}:[8]:g2(T) +46 < [7]:h2(U) OR NOT {L4}:[7]:h2(U) -59 < [5]:f(T) OR NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L9}:[6]:h1(U) -4 < [13]:n2(V1) OR NOT {L7}:[9]:n2(z1) -10 < [10]:n1(z1) OR NOT {L11}:[-1]:n1(V1) -32 < [-1]:f(T);0.0) 
-1: Do not wish to modify this node
Pick one:
-1
Leaving from node:[12]:n3(z2)
0 : (NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L10}:[6]:h1(U) -4 < [14]:n4(V2) OR NOT {L8}:[11]:n4(z2) -10 < [12]:n3(z2) OR NOT {L13}:[-1]:n3(V2) +0 < [-1]:n1(V1) OR NOT {L11}:[15]:n1(V1) -15 < [16]:g1(T) OR NOT {L2}:[3]:g1(y) +15 < [4]:g2(y) OR NOT {L1}:[2]:g2(x) -30 < [0]:f(x);-1.0) 
1 : (NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L10}:[6]:h1(U) -4 < [14]:n4(V2) OR NOT {L8}:[11]:n4(z2) -10 < [12]:n3(z2) OR NOT {L13}:[-1]:n3(V2) +0 < [-1]:n1(V1) OR NOT {L11}:[15]:n1(V1) -15 < [16]:g1(T) OR NOT {L2}:[3]:g1(y) +15 < [4]:g2(y) OR NOT {L1}:[2]:g2(x) -30 < [0]:f(x);-1.0) 
2 : (NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L10}:[6]:h1(U) -4 < [14]:n4(V2) OR NOT {L8}:[11]:n4(z2) -10 < [12]:n3(z2) OR NOT {L13}:[-1]:n3(V2) +10 < [-1]:n2(V1) OR NOT {L7}:[9]:n2(z1) -10 < [10]:n1(z1) OR NOT {L11}:[15]:n1(V1) -15 < [16]:g1(T) OR NOT {L2}:[3]:g1(y) +15 < [4]:g2(y) OR NOT {L1}:[2]:g2(x) -30 < [0]:f(x);-1.0) 
3 : (NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L10}:[6]:h1(U) -4 < [14]:n4(V2) OR NOT {L8}:[11]:n4(z2) -10 < [12]:n3(z2) OR NOT {L13}:[-1]:n3(V2) +10 < [-1]:n2(V1) OR NOT {L7}:[9]:n2(z1) -10 < [10]:n1(z1) OR NOT {L11}:[15]:n1(V1) -15 < [16]:g1(T) OR NOT {L2}:[3]:g1(y) +15 < [4]:g2(y) OR NOT {L1}:[2]:g2(x) -30 < [0]:f(x);-1.0) 
4 : (NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L10}:[6]:h1(U) -4 < [14]:n4(V2) OR NOT {L8}:[11]:n4(z2) -10 < [12]:n3(z2) OR NOT {L13}:[-1]:n3(V2) +29 < [-1]:h2(U) OR NOT {L4}:[7]:h2(U) -59 < [5]:f(T);-1.0) 
5 : (NOT {L10}:[6]:h1(U) -4 < [14]:n4(V2) OR NOT {L8}:[11]:n4(z2) -10 < [12]:n3(z2) OR NOT {L13}:[-1]:n3(V2) +15 < [-1]:h1(U);-1.0) 
6 : (NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L10}:[6]:h1(U) -4 < [14]:n4(V2) OR NOT {L8}:[11]:n4(z2) -10 < [12]:n3(z2) OR NOT {L13}:[-1]:n3(V2) +0 < [-1]:g2(T) OR NOT {L1}:[2]:g2(x) -30 < [0]:f(x);-1.0) 
7 : (NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L10}:[6]:h1(U) -4 < [14]:n4(V2) OR NOT {L8}:[11]:n4(z2) -10 < [12]:n3(z2) OR NOT {L13}:[-1]:n3(V2) +0 < [-1]:g2(T) OR NOT {L1}:[2]:g2(x) -30 < [0]:f(x);-1.0) 
8 : (NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L10}:[6]:h1(U) -4 < [14]:n4(V2) OR NOT {L8}:[11]:n4(z2) -10 < [12]:n3(z2) OR NOT {L13}:[-1]:n3(V2) +0 < [-1]:g2(T) OR NOT {L1}:[2]:g2(x) -30 < [0]:f(x);-1.0) 
9 : (NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L10}:[6]:h1(U) -4 < [14]:n4(V2) OR NOT {L8}:[11]:n4(z2) -10 < [12]:n3(z2) OR NOT {L13}:[-1]:n3(V2) -15 < [-1]:g1(T) OR NOT {L2}:[3]:g1(y) +15 < [4]:g2(y) OR NOT {L1}:[2]:g2(x) -30 < [0]:f(x);-1.0) 
10 : (NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L10}:[6]:h1(U) -4 < [14]:n4(V2) OR NOT {L8}:[11]:n4(z2) -10 < [12]:n3(z2) OR NOT {L13}:[-1]:n3(V2) -15 < [-1]:g1(T) OR NOT {L2}:[3]:g1(y) +15 < [4]:g2(y) OR NOT {L1}:[2]:g2(x) -30 < [0]:f(x);-1.0) 
11 : (NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L10}:[6]:h1(U) -4 < [14]:n4(V2) OR NOT {L8}:[11]:n4(z2) -10 < [12]:n3(z2) OR NOT {L13}:[-1]:n3(V2) -30 < [-1]:f(T);-1.0) 
12 : (NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L10}:[6]:h1(U) -4 < [14]:n4(V2) OR NOT {L8}:[11]:n4(z2) -10 < [12]:n3(z2) OR NOT {L13}:[-1]:n3(V2) -30 < [-1]:f(T);-1.0) 
13 : (NOT {L2}:[3]:g1(y) +15 < [4]:g2(y) OR NOT {L6}:[8]:g2(T) +46 < [7]:h2(U) OR NOT {L4}:[7]:h2(U) -59 < [5]:f(T) OR NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L10}:[6]:h1(U) -4 < [14]:n4(V2) OR NOT {L8}:[11]:n4(z2) -10 < [12]:n3(z2) OR NOT {L13}:[-1]:n3(V2) -17 < [-1]:n1(V1) OR NOT {L11}:[15]:n1(V1) -15 < [16]:g1(T);0.0) 
14 : (NOT {L2}:[3]:g1(y) +15 < [4]:g2(y) OR NOT {L6}:[8]:g2(T) +46 < [7]:h2(U) OR NOT {L4}:[7]:h2(U) -59 < [5]:f(T) OR NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L10}:[6]:h1(U) -4 < [14]:n4(V2) OR NOT {L8}:[11]:n4(z2) -10 < [12]:n3(z2) OR NOT {L13}:[-1]:n3(V2) -17 < [-1]:n1(V1) OR NOT {L11}:[15]:n1(V1) -15 < [16]:g1(T);0.0) 
15 : (NOT {L6}:[8]:g2(T) +46 < [7]:h2(U) OR NOT {L4}:[7]:h2(U) -59 < [5]:f(T) OR NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L10}:[6]:h1(U) -4 < [14]:n4(V2) OR NOT {L8}:[11]:n4(z2) -10 < [12]:n3(z2) OR NOT {L13}:[-1]:n3(V2) -17 < [-1]:n1(V1) OR NOT {L11}:[15]:n1(V1) -15 < [16]:g1(T) OR NOT {L2}:[3]:g1(y) +15 < [4]:g2(y);0.0) 
16 : (NOT {L6}:[8]:g2(T) +46 < [7]:h2(U) OR NOT {L4}:[7]:h2(U) -59 < [5]:f(T) OR NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L10}:[6]:h1(U) -4 < [14]:n4(V2) OR NOT {L8}:[11]:n4(z2) -10 < [12]:n3(z2) OR NOT {L13}:[-1]:n3(V2) -17 < [-1]:n1(V1) OR NOT {L11}:[15]:n1(V1) -15 < [16]:g1(T) OR NOT {L2}:[3]:g1(y) +15 < [4]:g2(y);0.0) 
17 : (NOT {L2}:[3]:g1(y) +15 < [4]:g2(y) OR NOT {L6}:[8]:g2(T) +46 < [7]:h2(U) OR NOT {L4}:[7]:h2(U) -59 < [5]:f(T) OR NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L10}:[6]:h1(U) -4 < [14]:n4(V2) OR NOT {L8}:[11]:n4(z2) -10 < [12]:n3(z2) OR NOT {L13}:[-1]:n3(V2) -17 < [-1]:n1(V1) OR NOT {L11}:[15]:n1(V1) -15 < [16]:g1(T);0.0) 
18 : (NOT {L2}:[3]:g1(y) +15 < [4]:g2(y) OR NOT {L6}:[8]:g2(T) +46 < [7]:h2(U) OR NOT {L4}:[7]:h2(U) -59 < [5]:f(T) OR NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L10}:[6]:h1(U) -4 < [14]:n4(V2) OR NOT {L8}:[11]:n4(z2) -10 < [12]:n3(z2) OR NOT {L13}:[-1]:n3(V2) -17 < [-1]:n1(V1) OR NOT {L11}:[15]:n1(V1) -15 < [16]:g1(T);0.0) 
19 : (NOT {L2}:[3]:g1(y) +15 < [4]:g2(y) OR NOT {L6}:[8]:g2(T) +46 < [7]:h2(U) OR NOT {L4}:[7]:h2(U) -59 < [5]:f(T) OR NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L10}:[6]:h1(U) -4 < [14]:n4(V2) OR NOT {L8}:[11]:n4(z2) -10 < [12]:n3(z2) OR NOT {L13}:[-1]:n3(V2) -7 < [-1]:n2(V1) OR NOT {L7}:[9]:n2(z1) -10 < [10]:n1(z1) OR NOT {L11}:[15]:n1(V1) -15 < [16]:g1(T);0.0) 
20 : (NOT {L2}:[3]:g1(y) +15 < [4]:g2(y) OR NOT {L6}:[8]:g2(T) +46 < [7]:h2(U) OR NOT {L4}:[7]:h2(U) -59 < [5]:f(T) OR NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L10}:[6]:h1(U) -4 < [14]:n4(V2) OR NOT {L8}:[11]:n4(z2) -10 < [12]:n3(z2) OR NOT {L13}:[-1]:n3(V2) -7 < [-1]:n2(V1) OR NOT {L7}:[9]:n2(z1) -10 < [10]:n1(z1) OR NOT {L11}:[15]:n1(V1) -15 < [16]:g1(T);0.0) 
21 : (NOT {L6}:[8]:g2(T) +46 < [7]:h2(U) OR NOT {L4}:[7]:h2(U) -59 < [5]:f(T) OR NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L10}:[6]:h1(U) -4 < [14]:n4(V2) OR NOT {L8}:[11]:n4(z2) -10 < [12]:n3(z2) OR NOT {L13}:[-1]:n3(V2) -7 < [-1]:n2(V1) OR NOT {L7}:[9]:n2(z1) -10 < [10]:n1(z1) OR NOT {L11}:[15]:n1(V1) -15 < [16]:g1(T) OR NOT {L2}:[3]:g1(y) +15 < [4]:g2(y);0.0) 
22 : (NOT {L6}:[8]:g2(T) +46 < [7]:h2(U) OR NOT {L4}:[7]:h2(U) -59 < [5]:f(T) OR NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L10}:[6]:h1(U) -4 < [14]:n4(V2) OR NOT {L8}:[11]:n4(z2) -10 < [12]:n3(z2) OR NOT {L13}:[-1]:n3(V2) -7 < [-1]:n2(V1) OR NOT {L7}:[9]:n2(z1) -10 < [10]:n1(z1) OR NOT {L11}:[15]:n1(V1) -15 < [16]:g1(T) OR NOT {L2}:[3]:g1(y) +15 < [4]:g2(y);0.0) 
23 : (NOT {L2}:[3]:g1(y) +15 < [4]:g2(y) OR NOT {L6}:[8]:g2(T) +46 < [7]:h2(U) OR NOT {L4}:[7]:h2(U) -59 < [5]:f(T) OR NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L10}:[6]:h1(U) -4 < [14]:n4(V2) OR NOT {L8}:[11]:n4(z2) -10 < [12]:n3(z2) OR NOT {L13}:[-1]:n3(V2) -7 < [-1]:n2(V1) OR NOT {L7}:[9]:n2(z1) -10 < [10]:n1(z1) OR NOT {L11}:[15]:n1(V1) -15 < [16]:g1(T);0.0) 
24 : (NOT {L2}:[3]:g1(y) +15 < [4]:g2(y) OR NOT {L6}:[8]:g2(T) +46 < [7]:h2(U) OR NOT {L4}:[7]:h2(U) -59 < [5]:f(T) OR NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L10}:[6]:h1(U) -4 < [14]:n4(V2) OR NOT {L8}:[11]:n4(z2) -10 < [12]:n3(z2) OR NOT {L13}:[-1]:n3(V2) -7 < [-1]:n2(V1) OR NOT {L7}:[9]:n2(z1) -10 < [10]:n1(z1) OR NOT {L11}:[15]:n1(V1) -15 < [16]:g1(T);0.0) 
25 : (NOT {L0}:[0]:f(x) +0 < [1]:g1(x) OR NOT {L2}:[3]:g1(y) +15 < [4]:g2(y) OR NOT {L6}:[8]:g2(T) +46 < [7]:h2(U) OR NOT {L4}:[7]:h2(U) -59 < [5]:f(T) OR NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L10}:[6]:h1(U) -4 < [14]:n4(V2) OR NOT {L8}:[11]:n4(z2) -10 < [12]:n3(z2) OR NOT {L13}:[-1]:n3(V2) -2 < [-1]:g2(T) OR NOT {L1}:[2]:g2(x) -30 < [0]:f(x);0.0) 
26 : (NOT {L6}:[8]:g2(T) +46 < [7]:h2(U) OR NOT {L4}:[7]:h2(U) -59 < [5]:f(T) OR NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L10}:[6]:h1(U) -4 < [14]:n4(V2) OR NOT {L8}:[11]:n4(z2) -10 < [12]:n3(z2) OR NOT {L13}:[-1]:n3(V2) -17 < [-1]:g2(T);0.0) 
27 : (NOT {L6}:[8]:g2(T) +46 < [7]:h2(U) OR NOT {L4}:[7]:h2(U) -59 < [5]:f(T) OR NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L10}:[6]:h1(U) -4 < [14]:n4(V2) OR NOT {L8}:[11]:n4(z2) -10 < [12]:n3(z2) OR NOT {L13}:[-1]:n3(V2) -17 < [-1]:g2(T);0.0) 
28 : (NOT {L6}:[8]:g2(T) +46 < [7]:h2(U) OR NOT {L4}:[7]:h2(U) -59 < [5]:f(T) OR NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L10}:[6]:h1(U) -4 < [14]:n4(V2) OR NOT {L8}:[11]:n4(z2) -10 < [12]:n3(z2) OR NOT {L13}:[-1]:n3(V2) -17 < [-1]:g2(T);0.0) 
29 : (NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L10}:[6]:h1(U) -4 < [14]:n4(V2) OR NOT {L8}:[11]:n4(z2) -10 < [12]:n3(z2) OR NOT {L13}:[-1]:n3(V2) -17 < [-1]:g2(T) OR NOT {L6}:[8]:g2(T) +46 < [7]:h2(U) OR NOT {L4}:[7]:h2(U) -59 < [5]:f(T);0.0) 
30 : (NOT {L2}:[3]:g1(y) +15 < [4]:g2(y) OR NOT {L6}:[8]:g2(T) +46 < [7]:h2(U) OR NOT {L4}:[7]:h2(U) -59 < [5]:f(T) OR NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L10}:[6]:h1(U) -4 < [14]:n4(V2) OR NOT {L8}:[11]:n4(z2) -10 < [12]:n3(z2) OR NOT {L13}:[-1]:n3(V2) -32 < [-1]:g1(T);0.0) 
31 : (NOT {L2}:[3]:g1(y) +15 < [4]:g2(y) OR NOT {L6}:[8]:g2(T) +46 < [7]:h2(U) OR NOT {L4}:[7]:h2(U) -59 < [5]:f(T) OR NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L10}:[6]:h1(U) -4 < [14]:n4(V2) OR NOT {L8}:[11]:n4(z2) -10 < [12]:n3(z2) OR NOT {L13}:[-1]:n3(V2) -32 < [-1]:g1(T);0.0) 
32 : (NOT {L6}:[8]:g2(T) +46 < [7]:h2(U) OR NOT {L4}:[7]:h2(U) -59 < [5]:f(T) OR NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L10}:[6]:h1(U) -4 < [14]:n4(V2) OR NOT {L8}:[11]:n4(z2) -10 < [12]:n3(z2) OR NOT {L13}:[-1]:n3(V2) -32 < [-1]:g1(T) OR NOT {L2}:[3]:g1(y) +15 < [4]:g2(y);0.0) 
33 : (NOT {L6}:[8]:g2(T) +46 < [7]:h2(U) OR NOT {L4}:[7]:h2(U) -59 < [5]:f(T) OR NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L10}:[6]:h1(U) -4 < [14]:n4(V2) OR NOT {L8}:[11]:n4(z2) -10 < [12]:n3(z2) OR NOT {L13}:[-1]:n3(V2) -32 < [-1]:g1(T) OR NOT {L2}:[3]:g1(y) +15 < [4]:g2(y);0.0) 
34 : (NOT {L2}:[3]:g1(y) +15 < [4]:g2(y) OR NOT {L6}:[8]:g2(T) +46 < [7]:h2(U) OR NOT {L4}:[7]:h2(U) -59 < [5]:f(T) OR NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L10}:[6]:h1(U) -4 < [14]:n4(V2) OR NOT {L8}:[11]:n4(z2) -10 < [12]:n3(z2) OR NOT {L13}:[-1]:n3(V2) -32 < [-1]:g1(T);0.0) 
35 : (NOT {L2}:[3]:g1(y) +15 < [4]:g2(y) OR NOT {L6}:[8]:g2(T) +46 < [7]:h2(U) OR NOT {L4}:[7]:h2(U) -59 < [5]:f(T) OR NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L10}:[6]:h1(U) -4 < [14]:n4(V2) OR NOT {L8}:[11]:n4(z2) -10 < [12]:n3(z2) OR NOT {L13}:[-1]:n3(V2) -32 < [-1]:g1(T);0.0) 
36 : (NOT {L0}:[0]:f(x) +0 < [1]:g1(x) OR NOT {L2}:[3]:g1(y) +15 < [4]:g2(y) OR NOT {L6}:[8]:g2(T) +46 < [7]:h2(U) OR NOT {L4}:[7]:h2(U) -59 < [5]:f(T) OR NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L10}:[6]:h1(U) -4 < [14]:n4(V2) OR NOT {L8}:[11]:n4(z2) -10 < [12]:n3(z2) OR NOT {L13}:[-1]:n3(V2) -32 < [-1]:f(T);0.0) 
-1: Do not wish to modify this node
Pick one:
9
det in addfromclauseincrementlist:0.0
new determinant:0.0
Wish to continue (0/1) ?
0
Do you wish to continue with no entry edges? (0/1)
0
new determinant:0.0
Do you wish to continue with negative cycles? (0/1)
0
Formula:
{L0}:[0]:f(x) +0 < [1]:g1(x) AND 
{L1}:[2]:g2(x) -30 < [0]:f(x) AND 
{L2}:[3]:g1(y) +15 < [4]:g2(y) AND 
{L3}:[5]:f(T) +45 < [6]:h1(U) AND 
{L4}:[7]:h2(U) -59 < [5]:f(T) AND 
NOT {L0}:[0]:f(x) +0 < [1]:g1(x) OR NOT {L2}:[3]:g1(y) +15 < [4]:g2(y) OR NOT {L6}:[8]:g2(T) +46 < [7]:h2(U) OR NOT {L4}:[7]:h2(U) -59 < [5]:f(T) AND 
NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L5}:[6]:h1(U) +1 < [8]:g2(T) OR NOT {L1}:[2]:g2(x) -30 < [0]:f(x) AND 
NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L5}:[6]:h1(U) +1 < [8]:g2(T) OR NOT {L6}:[8]:g2(T) +46 < [7]:h2(U) OR NOT {L4}:[7]:h2(U) -59 < [5]:f(T) AND 
{L7}:[9]:n2(z1) -10 < [10]:n1(z1) AND 
{L8}:[11]:n4(z2) -10 < [12]:n3(z2) AND 
{L5}:[6]:h1(U) +1 < [8]:g2(T) OR {L6}:[8]:g2(T) +46 < [7]:h2(U) OR {L9}:[6]:h1(U) -4 < [13]:n2(V1) OR {L10}:[6]:h1(U) -4 < [14]:n4(V2) AND 
NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L9}:[6]:h1(U) -4 < [13]:n2(V1) OR NOT {L7}:[9]:n2(z1) -10 < [10]:n1(z1) OR NOT {L11}:[15]:n1(V1) -15 < [16]:g1(T) OR NOT {L2}:[3]:g1(y) +15 < [4]:g2(y) OR NOT {L1}:[2]:g2(x) -30 < [0]:f(x) AND 
{L11}:[15]:n1(V1) -15 < [16]:g1(T) AND 
NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L10}:[6]:h1(U) -4 < [14]:n4(V2) OR NOT {L8}:[11]:n4(z2) -10 < [12]:n3(z2) OR NOT {L12}:[17]:n3(V2) -15 < [16]:g1(T) OR NOT {L2}:[3]:g1(y) +15 < [4]:g2(y) OR NOT {L1}:[2]:g2(x) -30 < [0]:f(x) AND 
{L12}:[17]:n3(V2) -15 < [16]:g1(T)

Determinant:0.0
Is this the formula you wanted? (0/1)
1
Final formula:
{L0}:[0]:f(x) +0 < [1]:g1(x) AND 
{L1}:[2]:g2(x) -30 < [0]:f(x) AND 
{L2}:[3]:g1(y) +15 < [4]:g2(y) AND 
{L3}:[5]:f(T) +45 < [6]:h1(U) AND 
{L4}:[7]:h2(U) -59 < [5]:f(T) AND 
NOT {L0}:[0]:f(x) +0 < [1]:g1(x) OR NOT {L2}:[3]:g1(y) +15 < [4]:g2(y) OR NOT {L6}:[8]:g2(T) +46 < [7]:h2(U) OR NOT {L4}:[7]:h2(U) -59 < [5]:f(T) AND 
NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L5}:[6]:h1(U) +1 < [8]:g2(T) OR NOT {L1}:[2]:g2(x) -30 < [0]:f(x) AND 
NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L5}:[6]:h1(U) +1 < [8]:g2(T) OR NOT {L6}:[8]:g2(T) +46 < [7]:h2(U) OR NOT {L4}:[7]:h2(U) -59 < [5]:f(T) AND 
{L7}:[9]:n2(z1) -10 < [10]:n1(z1) AND 
{L8}:[11]:n4(z2) -10 < [12]:n3(z2) AND 
{L5}:[6]:h1(U) +1 < [8]:g2(T) OR {L6}:[8]:g2(T) +46 < [7]:h2(U) OR {L9}:[6]:h1(U) -4 < [13]:n2(V1) OR {L10}:[6]:h1(U) -4 < [14]:n4(V2) AND 
NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L9}:[6]:h1(U) -4 < [13]:n2(V1) OR NOT {L7}:[9]:n2(z1) -10 < [10]:n1(z1) OR NOT {L11}:[15]:n1(V1) -15 < [16]:g1(T) OR NOT {L2}:[3]:g1(y) +15 < [4]:g2(y) OR NOT {L1}:[2]:g2(x) -30 < [0]:f(x) AND 
{L11}:[15]:n1(V1) -15 < [16]:g1(T) AND 
NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L10}:[6]:h1(U) -4 < [14]:n4(V2) OR NOT {L8}:[11]:n4(z2) -10 < [12]:n3(z2) OR NOT {L12}:[17]:n3(V2) -15 < [16]:g1(T) OR NOT {L2}:[3]:g1(y) +15 < [4]:g2(y) OR NOT {L1}:[2]:g2(x) -30 < [0]:f(x) AND 
{L12}:[17]:n3(V2) -15 < [16]:g1(T)

Determinant:0.0

Process completed.