THE INPUT FORMULA
The specification is:
{L0}:[-1]:f(x) +0 < [-1]:g1(x)
{L1}:[-1]:g2(x) -30 < [-1]:f(x)
{L2}:[-1]:g1(y) +15 < [-1]:g2(y)
The safety assertion is:
{L3}:[-1]:f(T) +45 < [-1]:h1(U)
{L4}:[-1]:h2(U) -59 < [-1]:f(T)
{L5}:[-1]:h1(U) +1 < [-1]:g2(T) OR {L6}:[-1]:g2(T) +46 < [-1]:h2(U)

THE UNOPTIMIZED FORMULA
The specification is:
{L0}:[0]:f(x) +0 < [1]:g1(x)
{L1}:[2]:g2(x) -30 < [0]:f(x)
{L2}:[3]:g1(y) +15 < [4]:g2(y)
The safety assertion is:
{L3}:[5]:f(T) +45 < [6]:h1(U)
{L4}:[7]:h2(U) -59 < [5]:f(T)
{L5}:[6]:h1(U) +1 < [8]:g2(T) OR {L6}:[8]:g2(T) +46 < [7]:h2(U)
The set of positive cycles:
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)
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)
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)

The determinant of the unoptimized formula:0.0 (so the real-time specification implies the safety assertion)

THE OPTIMIZED FORMULA
The specification is:
{L0}:[0]:f(x) -1 < [1]:g1(x)
{L1}:[2]:g2(x) -47 < [0]:f(x)
{L2}:[3]:g1(y) +15 < [4]:g2(y)
The safety assertion is:
{L3}:[5]:f(T) +45 < [6]:h1(U)
{L4}:[7]:h2(U) -59 < [5]:f(T)
{L5}:[6]:h1(U) +1 < [8]:g2(T) OR {L6}:[8]:g2(T) +46 < [7]:h2(U)
The set of positive cycles:
NOT {L0}:[0]:f(x) -1 < [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)
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) -47 < [0]:f(x)
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)

The determinant of the optimized formula: 0.0 (so the real-time specification implies the safety assertion)