↑ Up

ZenonModulo---0.5.0.UNK-Non.f

View TPTP
Problem Process solution in
SystemOnTSTP Download .tgz 
%------------------------------------------------------------------------------
% File     : ZenonModulo---0.5.0
% Problem  : SWX152_1 : TPTP v9.3.0. Released v9.3.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : run_zenon_modulo %d %s

% Computer : n017.cluster.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory   : 8042.1875MB
% OS       : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit  : 300s
% DateTime : Tue May  5 07:08:32 PM UTC 2026

% Result   : Unknown 1.02s 1.27s
% Output   : None 
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11  % Problem  : SWX152_1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.11  % Command  : run_zenon_modulo %d %s
% 0.13/0.32  % Computer : n017.cluster.edu
% 0.13/0.32  % Model    : x86_64 x86_64
% 0.13/0.32  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.32  % Memory   : 8042.1875MB
% 0.13/0.32  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.13/0.32  % CPULimit : 300
% 0.13/0.32  % WCLimit  : 300
% 0.13/0.32  % DateTime : Tue May  5 08:53:42 EDT 2026
% 0.13/0.32  % CPUTime  : 
% 1.02/1.26  Zenon error: exhausted search space without finding a proof
% 1.02/1.26  (* Current branch:
% 1.02/1.26  ((tau00 zenon_X10) != zenon_X4)
% 1.02/1.26  (zenon_Vpi >= (1))
% 1.02/1.26  ((d2 zenon_X4) != zenon_X1)
% 1.02/1.26  ((g1 zenon_X0) != (g2 (taur22 (g1 (d1 zenon_X10)) (d2 zenon_X10))))
% 1.02/1.26  (zenon_Vwh >= (1))
% 1.02/1.26  ((1) != (g2 (taur2b2 (g1 (d1 zenon_X10)) (d2 zenon_X10))))
% 1.02/1.26  (zenon_Vre = (zenon_X1 - (d2 (tau10 zenon_X10))))
% 1.02/1.26  ((tau01 zenon_X2) >= (1))
% 1.02/1.26  ((lambdai3 (tau01 zenon_X8)) >= (lambdai3 zenon_X8))
% 1.02/1.26  (zenon_Vmd >= (1))
% 1.02/1.26  ((0) < (g2 zenon_X1))
% 1.02/1.26  ((tau11 zenon_X2) > (g2 (taur22 (g1 (d1 zenon_X10)) (d2 zenon_X10))))
% 1.02/1.26  (((d2 (tau00 zenon_X10)) - (d2 (tau01 zenon_X10))) >= (1))
% 1.02/1.26  (((tau10 zenon_X10) - (tau11 zenon_X10)) >= (1))
% 1.02/1.26  ((tau01 zenon_X2) > (g2 (d2 (tau01 zenon_X10))))
% 1.02/1.26  (zenon_Vec <= (0))
% 1.02/1.26  ((tau11 zenon_X2) > (g2 (d2 (tau00 zenon_X10))))
% 1.02/1.26  ((g1 zenon_X0) > (g2 (taur22 (g1 (d1 zenon_X10)) (d2 zenon_X10))))
% 1.02/1.26  (((tau00 zenon_X10) - (tau11 zenon_X10)) >= (1))
% 1.02/1.26  ((tau10 zenon_X2) != (g2 (d2 (tau11 zenon_X10))))
% 1.02/1.26  ((g2 (d2 zenon_X4)) != (1))
% 1.02/1.26  ((g2 zenon_X1) > (g2 (taur2b2 (g1 (d1 zenon_X10)) (d2 zenon_X10))))
% 1.02/1.26  ((tau10 zenon_X2) > (g2 (d2 (tau01 zenon_X10))))
% 1.02/1.26  (zenon_Vsh <= (-1))
% 1.02/1.26  (zenon_Vtb >= (0))
% 1.02/1.26  (((tau11 zenon_X2) - (g2 (d2 (tau10 zenon_X10)))) >= (1))
% 1.02/1.26  (((d2 (tau01 zenon_X10)) - (taur2b2 (g1 (d1 zenon_X10)) (d2 zenon_X10))) <= (-1))
% 1.02/1.26  (r2 (tau11 zenon_X2))
% 1.02/1.26  ((tau11 zenon_X2) != (tau01 zenon_X2))
% 1.02/1.26  (zenon_Vtc = ((d2 (tau11 zenon_X10)) - (d2 (tau01 zenon_X10))))
% 1.02/1.26  ((d2 (tau01 zenon_X10)) > zenon_X1)
% 1.02/1.26  (zenon_X1 != (taur22 (g1 (d1 zenon_X10)) (d2 zenon_X10)))
% 1.02/1.26  ((d2 (tau10 zenon_X10)) > (taur22 (g1 (d1 zenon_X10)) (d2 zenon_X10)))
% 1.02/1.26  (((d2 zenon_X4) - zenon_X1) >= (1))
% 1.02/1.26  ((tau11 zenon_X2) > (g2 (d2 (tau11 zenon_X10))))
% 1.02/1.26  (((d1 (tau01 zenon_X9)) - (d1 (tau00 zenon_X9))) <= (0))
% 1.02/1.26  (zenon_Vtd <= (-1))
% 1.02/1.26  (lambdab1 (tau11 zenon_X3))
% 1.02/1.26  (zenon_Vue >= (1))
% 1.02/1.26  (r1 (tau11 zenon_X2))
% 1.02/1.26  ((tau10 zenon_X10) > (tau01 zenon_X10))
% 1.02/1.26  ((d2 (tau10 zenon_X10)) != (d2 (tau11 zenon_X10)))
% 1.02/1.26  ((d2 (tau00 zenon_X10)) > (d2 (tau01 zenon_X10)))
% 1.02/1.26  (zenon_Vqe = (zenon_X1 - (taur2b2 (g1 (d1 zenon_X10)) (d2 zenon_X10))))
% 1.02/1.26  ((tau11 zenon_X2) > (tau01 zenon_X2))
% 1.02/1.26  ((g1 zenon_X0) <= (1))
% 1.02/1.26  ((lambdai3 (tau11 zenon_X8)) >= (lambdai3 zenon_X8))
% 1.02/1.26  (((taur2b2 (g1 (d1 zenon_X10)) (d2 zenon_X10)) - (d2 (tau00 zenon_X10))) >= (0))
% 1.02/1.26  (zenon_Vmh = ((tau10 zenon_X2) - (tau00 zenon_X2)))
% 1.02/1.26  (zenon_Vuh = ((tau11 zenon_X2) - (tau01 zenon_X2)))
% 1.02/1.26  (zenon_Vjc >= (0))
% 1.02/1.26  (zenon_Vp = ((lambdai1 (tau00 zenon_X3)) - (lambdai1 zenon_X3)))
% 1.02/1.26  ((tau11 zenon_X2) != (g2 (taur2b2 (g1 (d1 zenon_X10)) (d2 zenon_X10))))
% 1.02/1.26  (-. (r1 (0)))
% 1.02/1.26  ((d2 (tau10 zenon_X10)) = (d2 (tau00 zenon_X10)))
% 1.02/1.26  (zenon_Vzc = ((d2 (tau10 zenon_X10)) - (d2 (tau00 zenon_X10))))
% 1.02/1.26  (zenon_Vxb >= (0))
% 1.02/1.26  (zenon_Vp >= (0))
% 1.02/1.26  (zenon_Vdc = ((taur11 (g2 (d2 zenon_X9)) (d1 zenon_X9)) - (d1 (tau11 zenon_X9))))
% 1.02/1.26  (((tau10 zenon_X2) - (g2 (taur2b2 (g1 (d1 zenon_X10)) (d2 zenon_X10)))) >= (1))
% 1.02/1.26  (((tau10 zenon_X2) - (g2 (d2 (tau00 zenon_X10)))) >= (1))
% 1.02/1.26  ((g2 (d2 (tau01 zenon_X10))) < (1))
% 1.02/1.26  ((d2 zenon_X4) < (taur2b2 (g1 (d1 zenon_X10)) (d2 zenon_X10)))
% 1.02/1.26  (zenon_Voh >= (1))
% 1.02/1.26  (zenon_Vsh = ((g2 (d2 (tau00 zenon_X10))) - (g2 zenon_X1)))
% 1.02/1.26  (zenon_Vcc = ((lambdai3 (tau00 zenon_X8)) - (lambdai3 zenon_X8)))
% 1.02/1.26  (zenon_Vkc = ((taur1b1 (g2 (d2 zenon_X9)) (d1 zenon_X9)) - (d1 (tau01 zenon_X9))))
% 1.02/1.26  (((taur22 (g1 (d1 zenon_X10)) (d2 zenon_X10)) - (d2 (tau01 zenon_X10))) <= (0))
% 1.02/1.26  ((tau01 zenon_X2) > (g2 (d2 (tau00 zenon_X10))))
% 1.02/1.26  ((tau10 zenon_X2) != (g2 (d2 (tau01 zenon_X10))))
% 1.02/1.26  ((tau11 zenon_X2) != (tau10 zenon_X2))
% 1.02/1.26  ((g2 (d2 zenon_X4)) != (g2 zenon_X1))
% 1.02/1.26  (((g2 (d2 (tau00 zenon_X10))) - (g1 zenon_X0)) <= (-1))
% 1.02/1.26  ((tau10 zenon_X2) > (g2 (d2 (tau11 zenon_X10))))
% 1.02/1.26  ((g2 zenon_X1) != (g2 (taur2b2 (g1 (d1 zenon_X10)) (d2 zenon_X10))))
% 1.02/1.26  (((tau00 zenon_X10) - (tau01 zenon_X10)) >= (1))
% 1.02/1.26  (((g2 (d2 (tau00 zenon_X10))) - (g2 zenon_X1)) <= (-1))
% 1.02/1.26  ((lambdai1 (tau10 zenon_X3)) >= (lambdai1 zenon_X3))
% 1.02/1.26  (zenon_Vo = ((lambdai1 (tau01 zenon_X3)) - (lambdai1 zenon_X3)))
% 1.02/1.26  ((tau01 zenon_X2) != (g2 (taur2b2 (g1 (d1 zenon_X10)) (d2 zenon_X10))))
% 1.02/1.26  (zenon_Vyh = ((g1 zenon_X0) - (g2 (taur22 (g1 (d1 zenon_X10)) (d2 zenon_X10)))))
% 1.02/1.26  (zenon_Vlc >= (0))
% 1.02/1.26  (lambdab1 (tau00 zenon_X3))
% 1.02/1.26  ((d2 (tau10 zenon_X10)) != (d2 zenon_X4))
% 1.02/1.26  ((tau01 zenon_X2) != (g2 (d2 (tau01 zenon_X10))))
% 1.02/1.26  (zenon_Vdi = ((tau01 zenon_X2) - (g2 (d2 (tau11 zenon_X10)))))
% 1.02/1.26  ((lambdai2 (tau00 zenon_X7)) >= (lambdai2 zenon_X7))
% 1.02/1.26  (lambdab3 (tau00 zenon_X6))
% 1.02/1.26  (zenon_Vpc >= (0))
% 1.02/1.26  (zenon_Vue = ((tau10 zenon_X10) - (tau11 zenon_X10)))
% 1.02/1.26  (zenon_Vei >= (1))
% 1.02/1.26  (zenon_Vwh = ((g1 zenon_X0) - (g2 (taur2b2 (g1 (d1 zenon_X10)) (d2 zenon_X10)))))
% 1.02/1.26  (zenon_Vvb >= (0))
% 1.02/1.26  (((tau11 zenon_X2) - (g2 (d2 (tau11 zenon_X10)))) >= (1))
% 1.02/1.26  (zenon_Vgd = ((d2 (tau01 zenon_X10)) - zenon_X1))
% 1.02/1.26  (zenon_Vdh <= (-1))
% 1.02/1.26  ((tau11 zenon_X2) != (g2 (d2 (tau11 zenon_X10))))
% 1.02/1.26  (zenon_Voi = ((tau11 zenon_X2) - (g2 (taur22 (g1 (d1 zenon_X10)) (d2 zenon_X10)))))
% 1.02/1.26  ((tau10 zenon_X2) > (tau00 zenon_X2))
% 1.02/1.26  (zenon_Vti >= (1))
% 1.02/1.26  (zenon_Vwe >= (1))
% 1.02/1.26  ((g2 (d2 (tau00 zenon_X10))) < (1))
% 1.02/1.26  (zenon_Vpd = ((tau00 zenon_X10) - zenon_X4))
% 1.02/1.26  ((d2 zenon_X4) != (taur22 (g1 (d1 zenon_X10)) (d2 zenon_X10)))
% 1.02/1.26  (zenon_Vrc >= (0))
% 1.02/1.26  (((tau10 zenon_X10) - zenon_X4) >= (1))
% 1.02/1.26  ((tau10 zenon_X2) > (g2 (d2 (tau00 zenon_X10))))
% 1.02/1.26  (zenon_Vkd >= (1))
% 1.02/1.26  ((g2 (d2 (tau00 zenon_X10))) != (g1 zenon_X0))
% 1.02/1.26  ((g2 (d2 (tau00 zenon_X10))) >= (0))
% 1.02/1.27  (zenon_Vwc <= (0))
% 1.02/1.27  (zenon_Vld = ((tau01 zenon_X10) - zenon_X4))
% 1.02/1.27  (zenon_Vhh <= (-1))
% 1.02/1.27  (((g2 (d2 (tau01 zenon_X10))) - (g1 zenon_X0)) <= (-1))
% 1.02/1.27  (zenon_Vai = ((tau01 zenon_X2) - (g2 (taur22 (g1 (d1 zenon_X10)) (d2 zenon_X10)))))
% 1.02/1.27  ((taur11 (g2 (d2 zenon_X9)) (d1 zenon_X9)) = (d1 (tau10 zenon_X9)))
% 1.02/1.27  ((tau10 zenon_X2) != (g2 (taur2b2 (g1 (d1 zenon_X10)) (d2 zenon_X10))))
% 1.02/1.27  (zenon_Vrd = (zenon_X1 - (taur22 (g1 (d1 zenon_X10)) (d2 zenon_X10))))
% 1.02/1.27  (zenon_Vsi >= (1))
% 1.02/1.27  ((g1 zenon_X0) = (1))
% 1.02/1.27  (zenon_Vcd <= (-1))
% 1.02/1.27  (zenon_Vph = ((tau11 zenon_X2) - (tau00 zenon_X2)))
% 1.02/1.27  (((taur22 (g1 (d1 zenon_X10)) (d2 zenon_X10)) - (d2 (tau11 zenon_X10))) >= (0))
% 1.02/1.27  (((taur2b2 (g1 (d1 zenon_X10)) (d2 zenon_X10)) - (d2 (tau00 zenon_X10))) <= (0))
% 1.02/1.27  (zenon_Vve = ((d2 (tau00 zenon_X10)) - (d2 (tau11 zenon_X10))))
% 1.02/1.27  ((g2 (d2 (tau01 zenon_X10))) = (0))
% 1.02/1.27  (zenon_Vac = ((lambdai3 (tau10 zenon_X8)) - (lambdai3 zenon_X8)))
% 1.02/1.27  ((g2 (taur22 (g1 (d1 zenon_X10)) (d2 zenon_X10))) >= (0))
% 1.02/1.27  (zenon_X1 != (d2 (tau10 zenon_X10)))
% 1.02/1.27  (zenon_Vzh = ((taur2b2 (g1 (d1 zenon_X10)) (d2 zenon_X10)) - (taur22 (g1 (d1 zenon_X10)) (d2 zenon_X10))))
% 1.02/1.27  ((lambdai2 (tau00 zenon_X5)) >= (lambdai1 zenon_X5))
% 1.02/1.27  ((g2 (d2 (tau11 zenon_X10))) < (g2 zenon_X1))
% 1.02/1.27  ((d2 (tau10 zenon_X10)) > (d2 (tau01 zenon_X10)))
% 1.02/1.27  (((tau11 zenon_X2) - (tau10 zenon_X2)) >= (1))
% 1.02/1.27  ((tau10 zenon_X2) != (tau00 zenon_X2))
% 1.02/1.27  ((tau10 zenon_X2) > (g2 (d2 zenon_X4)))
% 1.02/1.27  (zenon_Vii >= (1))
% 1.02/1.27  ((d1 (tau01 zenon_X9)) = (d1 (tau00 zenon_X9)))
% 1.02/1.27  ((g2 (d2 (tau00 zenon_X10))) != (g2 zenon_X1))
% 1.02/1.27  (((d2 (tau01 zenon_X10)) - (d2 zenon_X4)) >= (1))
% 1.02/1.27  ((g2 (taur22 (g1 (d1 zenon_X10)) (d2 zenon_X10))) <= (0))
% 1.02/1.27  ((- (g2 (taur22 (g1 (d1 zenon_X10)) (d2 zenon_X10)))) >= (0))
% 1.02/1.27  ((d2 (tau00 zenon_X10)) != (d2 zenon_X4))
% 1.02/1.27  (zenon_Vgh = ((d2 (tau00 zenon_X10)) - (taur22 (g1 (d1 zenon_X10)) (d2 zenon_X10))))
% 1.02/1.27  (zenon_Vwc = ((taur2b2 (g1 (d1 zenon_X10)) (d2 zenon_X10)) - (d2 (tau10 zenon_X10))))
% 1.02/1.27  ((tau11 zenon_X2) != (tau00 zenon_X2))
% 1.02/1.27  ((tau10 zenon_X10) > (tau11 zenon_X10))
% 1.02/1.27  (zenon_Vgc <= (0))
% 1.02/1.27  (((d2 zenon_X4) - (taur2b2 (g1 (d1 zenon_X10)) (d2 zenon_X10))) <= (-1))
% 1.02/1.27  (zenon_Vbi = ((tau01 zenon_X2) - (g2 (taur2b2 (g1 (d1 zenon_X10)) (d2 zenon_X10)))))
% 1.02/1.27  ((0) != (g1 zenon_X0))
% 1.02/1.27  ((lambdai2 (tau11 zenon_X5)) >= (lambdai1 zenon_X5))
% 1.02/1.27  ((d2 (tau10 zenon_X10)) != (d2 (tau01 zenon_X10)))
% 1.02/1.27  ((tau11 zenon_X2) > (g2 (d2 zenon_X4)))
% 1.02/1.27  (((d2 (tau00 zenon_X10)) - (taur22 (g1 (d1 zenon_X10)) (d2 zenon_X10))) >= (1))
% 1.02/1.27  (zenon_Vub >= (0))
% 1.02/1.27  ((tau00 zenon_X10) != (tau11 zenon_X10))
% 1.02/1.27  (zenon_Vxh = ((g2 zenon_X1) - (g2 (taur22 (g1 (d1 zenon_X10)) (d2 zenon_X10)))))
% 1.02/1.27  ((g2 (d2 (tau01 zenon_X10))) < (g1 zenon_X0))
% 1.02/1.27  ((tau01 zenon_X2) > (g2 (d2 zenon_X4)))
% 1.02/1.27  (zenon_Vli = ((tau10 zenon_X2) - (g2 (d2 (tau00 zenon_X10)))))
% 1.02/1.27  (((tau10 zenon_X2) - (g2 (d2 zenon_X4))) >= (1))
% 1.02/1.27  ((1) > (g2 (taur2b2 (g1 (d1 zenon_X10)) (d2 zenon_X10))))
% 1.02/1.27  (zenon_Vqh = ((g2 (d2 (tau10 zenon_X10))) - (g2 zenon_X1)))
% 1.02/1.27  (((tau00 zenon_X10) - zenon_X4) >= (1))
% 1.02/1.27  (((d1 (tau01 zenon_X9)) - (d1 (tau00 zenon_X9))) >= (0))
% 1.02/1.27  ((lambdai2 (tau01 zenon_X5)) >= (lambdai1 zenon_X5))
% 1.02/1.27  (zenon_Vbc >= (0))
% 1.02/1.27  (zenon_Vye <= (-1))
% 1.02/1.27  (zenon_Vxc = ((taur2b2 (g1 (d1 zenon_X10)) (d2 zenon_X10)) - (d2 (tau00 zenon_X10))))
% 1.02/1.27  (zenon_Vfd <= (-1))
% 1.02/1.27  (zenon_Vvd = ((tau10 zenon_X10) - (tau01 zenon_X10)))
% 1.02/1.27  (((taur2b2 (g1 (d1 zenon_X10)) (d2 zenon_X10)) - (d2 (tau10 zenon_X10))) <= (0))
% 1.02/1.27  (((tau01 zenon_X2) - (g2 (taur2b2 (g1 (d1 zenon_X10)) (d2 zenon_X10)))) >= (1))
% 1.02/1.27  (zenon_Vji >= (1))
% 1.02/1.27  (zenon_Vsi = ((tau11 zenon_X2) - (g2 (d2 (tau00 zenon_X10)))))
% 1.02/1.27  (zenon_Vrh <= (-1))
% 1.02/1.27  (zenon_Vui = ((tau11 zenon_X2) - (g2 (d2 zenon_X4))))
% 1.02/1.27  (zenon_Vvc >= (0))
% 1.02/1.27  (((d2 (tau01 zenon_X10)) - zenon_X1) >= (1))
% 1.02/1.27  (zenon_Vii = ((tau10 zenon_X2) - (g2 (taur2b2 (g1 (d1 zenon_X10)) (d2 zenon_X10)))))
% 1.02/1.27  (r2 (tau01 zenon_X2))
% 1.02/1.27  (lambdab1 (tau10 zenon_X3))
% 1.02/1.27  (zenon_Vwd >= (1))
% 1.02/1.27  (((tau10 zenon_X2) - (tau00 zenon_X2)) >= (1))
% 1.02/1.27  (lambdab2 (tau10 zenon_X7))
% 1.02/1.27  ((- (g1 zenon_X0)) <= (-1))
% 1.02/1.27  ((g2 (d2 (tau10 zenon_X10))) < (g1 zenon_X0))
% 1.02/1.27  (((g2 zenon_X1) - (g2 (taur2b2 (g1 (d1 zenon_X10)) (d2 zenon_X10)))) >= (1))
% 1.02/1.27  ((tau01 zenon_X2) != (g2 (d2 (tau00 zenon_X10))))
% 1.02/1.27  (zenon_Vfi >= (1))
% 1.02/1.27  (zenon_Vud = ((d2 (tau10 zenon_X10)) - (d2 (tau01 zenon_X10))))
% 1.02/1.27  (((g1 zenon_X0) - (g2 (taur2b2 (g1 (d1 zenon_X10)) (d2 zenon_X10)))) >= (1))
% 1.02/1.27  (((g1 zenon_X0) - (g2 (taur22 (g1 (d1 zenon_X10)) (d2 zenon_X10)))) >= (1))
% 1.02/1.27  ((tau01 zenon_X2) > (g2 (taur2b2 (g1 (d1 zenon_X10)) (d2 zenon_X10))))
% 1.02/1.27  ((d2 (tau00 zenon_X10)) > zenon_X1)
% 1.02/1.27  (((taur22 (g1 (d1 zenon_X10)) (d2 zenon_X10)) - (d2 (tau11 zenon_X10))) <= (0))
% 1.02/1.27  ((g2 (d2 (tau00 zenon_X10))) <= (0))
% 1.02/1.27  ((1) > (g2 (taur22 (g1 (d1 zenon_X10)) (d2 zenon_X10))))
% 1.02/1.27  ((1) != (g2 (taur22 (g1 (d1 zenon_X10)) (d2 zenon_X10))))
% 1.02/1.27  ((tau00 zenon_X10) > (tau01 zenon_X10))
% 1.02/1.27  (zenon_Vnb >= (0))
% 1.02/1.27  (((d2 (tau11 zenon_X10)) - (d2 (tau01 zenon_X10))) <= (0))
% 1.02/1.27  (zenon_Vad <= (0))
% 1.02/1.27  ((tau10 zenon_X2) != (g2 (d2 zenon_X4)))
% 1.02/1.27  (-. (r2 (tau10 zenon_X2)))
% 1.02/1.27  ((g2 (d2 (tau11 zenon_X10))) != (g1 zenon_X0))
% 1.02/1.27  (zenon_Vqb >= (0))
% 1.02/1.27  (zenon_Voc = ((d1 (tau01 zenon_X9)) - (d1 (tau00 zenon_X9))))
% 1.02/1.27  (zenon_Vnh <= (-1))
% 1.02/1.27  ((tau10 zenon_X2) != (0))
% 1.02/1.27  ((lambdai1 (tau11 zenon_X3)) >= (lambdai1 zenon_X3))
% 1.02/1.27  ((lambdai3 (tau00 zenon_X8)) >= (lambdai3 zenon_X8))
% 1.02/1.27  ((tau10 zenon_X2) >= (1))
% 1.02/1.27  ((d2 (tau11 zenon_X10)) > (d2 zenon_X4))
% 1.02/1.27  (lambdab2 (tau10 zenon_X5))
% 1.02/1.27  ((lambdai3 (tau10 zenon_X8)) >= (lambdai3 zenon_X8))
% 1.02/1.27  ((d2 zenon_X4) < (taur22 (g1 (d1 zenon_X10)) (d2 zenon_X10)))
% 1.02/1.27  ((d2 (tau00 zenon_X10)) != (d2 (tau11 zenon_X10)))
% 1.02/1.27  (((g2 (d2 zenon_X4)) - (g1 zenon_X0)) <= (-1))
% 1.02/1.27  ((g2 (d2 (tau10 zenon_X10))) != (g2 zenon_X1))
% 1.02/1.27  (zenon_Vmh >= (1))
% 1.02/1.27  ((d2 (tau01 zenon_X10)) != (taur2b2 (g1 (d1 zenon_X10)) (d2 zenon_X10)))
% 1.02/1.27  ((tau01 zenon_X2) != (g2 (d2 (tau11 zenon_X10))))
% 1.02/1.27  (((tau01 zenon_X2) - (g2 (taur22 (g1 (d1 zenon_X10)) (d2 zenon_X10)))) >= (1))
% 1.02/1.27  ((g2 (d2 (tau10 zenon_X10))) = (0))
% 1.02/1.27  (zenon_Vni >= (1))
% 1.02/1.27  (zenon_Vjd = ((tau11 zenon_X10) - zenon_X4))
% 1.02/1.27  ((g2 (d2 zenon_X4)) < (1))
% 1.02/1.27  (((d1 (tau11 zenon_X9)) - (d1 (tau10 zenon_X9))) <= (0))
% 1.02/1.27  (((d2 (tau00 zenon_X10)) - zenon_X1) >= (1))
% 1.02/1.27  ((g2 (d2 (tau01 zenon_X10))) != (1))
% 1.02/1.27  ((g2 (d2 (tau00 zenon_X10))) = (0))
% 1.02/1.27  (zenon_Vic <= (0))
% 1.02/1.27  (zenon_Vyc = ((taur2b2 (g1 (d1 zenon_X10)) (d2 zenon_X10)) - (d2 (tau00 zenon_X10))))
% 1.02/1.27  (zenon_Vki >= (1))
% 1.02/1.27  (zenon_Vxb = ((lambdai2 (tau01 zenon_X7)) - (lambdai2 zenon_X7)))
% 1.02/1.27  (zenon_X1 != (d2 (tau11 zenon_X10)))
% 1.02/1.27  ((tau10 zenon_X10) > zenon_X4)
% 1.02/1.27  (zenon_Voh = ((tau11 zenon_X2) - (tau10 zenon_X2)))
% 1.02/1.27  (zenon_X1 != (taur2b2 (g1 (d1 zenon_X10)) (d2 zenon_X10)))
% 1.02/1.27  (zenon_Vgi = ((tau01 zenon_X2) - (g2 (d2 zenon_X4))))
% 1.02/1.27  ((g2 zenon_X1) != (g2 (taur22 (g1 (d1 zenon_X10)) (d2 zenon_X10))))
% 1.02/1.27  (((taur2b2 (g1 (d1 zenon_X10)) (d2 zenon_X10)) - (taur22 (g1 (d1 zenon_X10)) (d2 zenon_X10))) >= (1))
% 1.02/1.27  ((tau11 zenon_X2) != (g2 (d2 (tau00 zenon_X10))))
% 1.02/1.27  (zenon_Vcc >= (0))
% 1.02/1.27  (((taur11 (g2 (d2 zenon_X9)) (d1 zenon_X9)) - (d1 (tau10 zenon_X9))) <= (0))
% 1.02/1.27  (zenon_Vih = ((tau01 zenon_X2) - (tau10 zenon_X2)))
% 1.02/1.27  (((d2 (tau11 zenon_X10)) - (taur2b2 (g1 (d1 zenon_X10)) (d2 zenon_X10))) <= (-1))
% 1.02/1.27  (zenon_Vqh <= (-1))
% 1.02/1.27  (zenon_Vfd = ((g2 (d2 zenon_X4)) - (g1 zenon_X0)))
% 1.02/1.27  ((tau01 zenon_X2) != (g2 (taur22 (g1 (d1 zenon_X10)) (d2 zenon_X10))))
% 1.02/1.27  (zenon_Vwd = ((d2 (tau00 zenon_X10)) - (d2 (tau01 zenon_X10))))
% 1.02/1.27  ((tau10 zenon_X2) != (g2 (taur22 (g1 (d1 zenon_X10)) (d2 zenon_X10))))
% 1.02/1.27  (((d2 zenon_X4) - (taur22 (g1 (d1 zenon_X10)) (d2 zenon_X10))) <= (-1))
% 1.02/1.27  ((tau00 zenon_X10) > (tau11 zenon_X10))
% 1.02/1.27  (((tau01 zenon_X2) - (g2 (d2 (tau01 zenon_X10)))) >= (1))
% 1.02/1.27  (zenon_Vlh = ((g2 (d2 (tau01 zenon_X10))) - (g1 zenon_X0)))
% 1.02/1.27  (zenon_Vfc >= (0))
% 1.02/1.27  (zenon_Vuc = ((d2 (tau11 zenon_X10)) - (d2 (tau01 zenon_X10))))
% 1.02/1.27  ((g2 (d2 (tau10 zenon_X10))) <= (0))
% 1.02/1.27  (((tau01 zenon_X10) - zenon_X4) >= (1))
% 1.02/1.27  ((g2 (d2 zenon_X4)) < (g2 zenon_X1))
% 1.02/1.27  (zenon_Vhi >= (1))
% 1.02/1.27  ((d2 (tau01 zenon_X10)) != (d2 zenon_X4))
% 1.02/1.27  (((tau01 zenon_X2) - (g2 (d2 zenon_X4))) >= (1))
% 1.02/1.27  (zenon_Vhc = ((d1 (tau11 zenon_X9)) - (d1 (tau10 zenon_X9))))
% 1.02/1.27  ((zenon_X1 - (d2 (tau11 zenon_X10))) <= (-1))
% 1.02/1.27  (((g2 (d2 (tau10 zenon_X10))) - (g2 zenon_X1)) <= (-1))
% 1.02/1.27  (((tau10 zenon_X2) - (g2 (d2 (tau10 zenon_X10)))) >= (1))
% 1.02/1.27  ((taur1b1 (g2 (d2 zenon_X9)) (d1 zenon_X9)) = (d1 (tau01 zenon_X9)))
% 1.02/1.27  (zenon_Vfc = ((taur11 (g2 (d2 zenon_X9)) (d1 zenon_X9)) - (d1 (tau10 zenon_X9))))
% 1.02/1.27  (((d2 (tau10 zenon_X10)) - (taur22 (g1 (d1 zenon_X10)) (d2 zenon_X10))) >= (1))
% 1.02/1.27  ((tau01 zenon_X2) > (g2 (taur22 (g1 (d1 zenon_X10)) (d2 zenon_X10))))
% 1.02/1.27  (((tau01 zenon_X2) - (g2 (d2 (tau11 zenon_X10)))) >= (1))
% 1.02/1.27  (zenon_Vkh <= (-1))
% 1.02/1.27  (zenon_Vid >= (1))
% 1.02/1.27  (zenon_Vth = ((g2 (d2 (tau00 zenon_X10))) - (g1 zenon_X0)))
% 1.02/1.27  ((tau11 zenon_X2) >= (1))
% 1.02/1.27  (((tau11 zenon_X2) - (tau00 zenon_X2)) >= (1))
% 1.02/1.27  ((0) != (1))
% 1.02/1.27  (zenon_Vrd <= (-1))
% 1.02/1.27  (zenon_Vnd = ((tau10 zenon_X10) - zenon_X4))
% 1.02/1.27  (zenon_Vuc <= (0))
% 1.02/1.27  (((tau11 zenon_X2) - (g2 (d2 (tau00 zenon_X10)))) >= (1))
% 1.02/1.27  (zenon_Vbi >= (1))
% 1.02/1.27  (zenon_Vmi >= (1))
% 1.02/1.27  (zenon_Vfi = ((tau01 zenon_X2) - (g2 (d2 (tau01 zenon_X10)))))
% 1.02/1.27  ((taur22 (g1 (d1 zenon_X10)) (d2 zenon_X10)) = (d2 (tau11 zenon_X10)))
% 1.02/1.27  (zenon_Vqi = ((tau11 zenon_X2) - (g2 (d2 (tau10 zenon_X10)))))
% 1.02/1.27  ((lambdai3 (tau00 zenon_X6)) >= (lambdai1 zenon_X6))
% 1.02/1.27  (zenon_Vre <= (-1))
% 1.02/1.27  (zenon_Vdd = ((d2 zenon_X4) - zenon_X1))
% 1.02/1.27  (zenon_Vtd = (zenon_X1 - (d2 (tau11 zenon_X10))))
% 1.02/1.27  ((g2 (d2 (tau10 zenon_X10))) != (1))
% 1.02/1.27  (zenon_Vve >= (1))
% 1.02/1.27  (zenon_Vzb = ((lambdai3 (tau11 zenon_X8)) - (lambdai3 zenon_X8)))
% 1.02/1.27  ((tau10 zenon_X10) != (tau01 zenon_X10))
% 1.02/1.27  (zenon_X1 < (taur22 (g1 (d1 zenon_X10)) (d2 zenon_X10)))
% 1.02/1.27  (zenon_Vwe = ((tau00 zenon_X10) - (tau11 zenon_X10)))
% 1.02/1.27  (lambdab2 (tau11 zenon_X5))
% 1.02/1.27  (zenon_Vqb = ((lambdai2 (tau00 zenon_X5)) - (lambdai1 zenon_X5)))
% 1.02/1.27  ((g2 (d2 (tau10 zenon_X10))) >= (0))
% 1.02/1.27  (zenon_X1 < (taur2b2 (g1 (d1 zenon_X10)) (d2 zenon_X10)))
% 1.02/1.27  ((tau11 zenon_X2) != (g2 (d2 (tau01 zenon_X10))))
% 1.02/1.27  ((zenon_X1 - (d2 (tau10 zenon_X10))) <= (-1))
% 1.02/1.27  (zenon_Vad = ((d2 (tau10 zenon_X10)) - (d2 (tau00 zenon_X10))))
% 1.02/1.27  (zenon_Vsb = ((lambdai3 (tau10 zenon_X6)) - (lambdai1 zenon_X6)))
% 1.02/1.27  (zenon_Vac >= (0))
% 1.02/1.27  ((taur2b2 (g1 (d1 zenon_X10)) (d2 zenon_X10)) = (d2 (tau00 zenon_X10)))
% 1.02/1.27  ((taur22 (g1 (d1 zenon_X10)) (d2 zenon_X10)) = (d2 (tau01 zenon_X10)))
% 1.02/1.27  (((d2 (tau00 zenon_X10)) - (d2 zenon_X4)) >= (1))
% 1.02/1.27  ((g2 (taur2b2 (g1 (d1 zenon_X10)) (d2 zenon_X10))) >= (0))
% 1.02/1.27  ((g2 (d2 (tau01 zenon_X10))) < (g2 zenon_X1))
% 1.02/1.27  (zenon_Vgi >= (1))
% 1.02/1.27  (zenon_Vmc = ((taur1b1 (g2 (d2 zenon_X9)) (d1 zenon_X9)) - (d1 (tau00 zenon_X9))))
% 1.02/1.27  (zenon_Veh = ((d2 (tau10 zenon_X10)) - (taur22 (g1 (d1 zenon_X10)) (d2 zenon_X10))))
% 1.02/1.27  ((tau11 zenon_X2) != (0))
% 1.02/1.27  (zenon_Vai >= (1))
% 1.02/1.27  (((g2 (d2 (tau11 zenon_X10))) - (g2 zenon_X1)) <= (-1))
% 1.02/1.27  (((taur1b1 (g2 (d2 zenon_X9)) (d1 zenon_X9)) - (d1 (tau00 zenon_X9))) <= (0))
% 1.02/1.27  ((d2 (tau11 zenon_X10)) < (taur2b2 (g1 (d1 zenon_X10)) (d2 zenon_X10)))
% 1.02/1.27  (zenon_Vpc = ((taur22 (g1 (d1 zenon_X10)) (d2 zenon_X10)) - (d2 (tau11 zenon_X10))))
% 1.02/1.27  (zenon_Vod >= (1))
% 1.02/1.27  ((tau10 zenon_X2) > (0))
% 1.02/1.27  (((g2 zenon_X1) - (g2 (taur22 (g1 (d1 zenon_X10)) (d2 zenon_X10)))) >= (1))
% 1.02/1.27  ((taur1b1 (g2 (d2 zenon_X9)) (d1 zenon_X9)) = (d1 (tau00 zenon_X9)))
% 1.02/1.27  ((g2 (d2 (tau11 zenon_X10))) <= (0))
% 1.02/1.27  (zenon_Veh >= (1))
% 1.02/1.27  ((g2 (d2 (tau01 zenon_X10))) != (g2 zenon_X1))
% 1.02/1.27  ((tau10 zenon_X2) != (g2 (d2 (tau00 zenon_X10))))
% 1.02/1.27  (zenon_Vec = ((taur11 (g2 (d2 zenon_X9)) (d1 zenon_X9)) - (d1 (tau11 zenon_X9))))
% 1.02/1.27  ((lambdai1 (tau00 zenon_X3)) >= (lambdai1 zenon_X3))
% 1.02/1.27  (lambdab2 (tau00 zenon_X7))
% 1.02/1.27  (((taur11 (g2 (d2 zenon_X9)) (d1 zenon_X9)) - (d1 (tau10 zenon_X9))) >= (0))
% 1.02/1.27  (zenon_Vxh >= (1))
% 1.02/1.27  (zenon_Vyc <= (0))
% 1.02/1.27  ((lambdai2 (tau10 zenon_X5)) >= (lambdai1 zenon_X5))
% 1.02/1.27  (zenon_Vhd >= (1))
% 1.02/1.27  (((taur1b1 (g2 (d2 zenon_X9)) (d1 zenon_X9)) - (d1 (tau01 zenon_X9))) >= (0))
% 1.02/1.27  ((tau10 zenon_X2) > (g2 (d2 (tau10 zenon_X10))))
% 1.02/1.27  (zenon_Vnc >= (0))
% 1.02/1.27  ((d2 (tau00 zenon_X10)) > (taur22 (g1 (d1 zenon_X10)) (d2 zenon_X10)))
% 1.02/1.27  (zenon_Vxd >= (1))
% 1.02/1.27  ((g2 (d2 (tau10 zenon_X10))) < (1))
% 1.02/1.27  (zenon_Vkc <= (0))
% 1.02/1.27  (zenon_Vmc <= (0))
% 1.02/1.27  (((tau10 zenon_X2) - (g2 (d2 (tau11 zenon_X10)))) >= (1))
% 1.02/1.27  (zenon_Vud >= (1))
% 1.02/1.27  ((g1 zenon_X0) >= (1))
% 1.02/1.27  (zenon_Vpb = ((lambdai2 (tau01 zenon_X5)) - (lambdai1 zenon_X5)))
% 1.02/1.27  (((tau11 zenon_X2) - (g2 (taur22 (g1 (d1 zenon_X10)) (d2 zenon_X10)))) >= (1))
% 1.02/1.27  (zenon_Vnb = ((lambdai2 (tau11 zenon_X5)) - (lambdai1 zenon_X5)))
% 1.02/1.27  (zenon_Vhd = ((d2 (tau00 zenon_X10)) - zenon_X1))
% 1.02/1.27  ((g2 (d2 (tau00 zenon_X10))) != (1))
% 1.02/1.27  (r1 (tau10 zenon_X2))
% 1.02/1.27  ((tau11 zenon_X2) > (g2 (d2 (tau01 zenon_X10))))
% 1.02/1.27  (zenon_Vn >= (0))
% 1.02/1.27  ((tau00 zenon_X10) > zenon_X4)
% 1.02/1.27  (zenon_Vgc = ((taur11 (g2 (d2 zenon_X9)) (d1 zenon_X9)) - (d1 (tau10 zenon_X9))))
% 1.02/1.27  ((g2 (d2 (tau11 zenon_X10))) = (0))
% 1.02/1.27  ((tau01 zenon_X2) > (g2 (d2 (tau10 zenon_X10))))
% 1.02/1.27  (lambdab3 (tau01 zenon_X6))
% 1.02/1.27  ((taur2b2 (g1 (d1 zenon_X10)) (d2 zenon_X10)) != (taur22 (g1 (d1 zenon_X10)) (d2 zenon_X10)))
% 1.02/1.27  ((tau01 zenon_X2) != (g2 (d2 (tau10 zenon_X10))))
% 1.02/1.27  (zenon_Vo >= (0))
% 1.02/1.27  ((lambdai2 (tau11 zenon_X7)) >= (lambdai2 zenon_X7))
% 1.02/1.27  (lambdab2 (tau01 zenon_X5))
% 1.02/1.27  ((tau10 zenon_X10) != (tau11 zenon_X10))
% 1.02/1.27  (lambdab3 (tau01 zenon_X8))
% 1.02/1.27  (zenon_Vvh = ((g2 zenon_X1) - (g2 (taur2b2 (g1 (d1 zenon_X10)) (d2 zenon_X10)))))
% 1.02/1.27  (zenon_Vjh = ((g2 (d2 (tau11 zenon_X10))) - (g1 zenon_X0)))
% 1.02/1.27  (zenon_Vid = ((d2 (tau11 zenon_X10)) - (d2 zenon_X4)))
% 1.02/1.27  (zenon_Vqc <= (0))
% 1.02/1.27  ((g2 (d2 (tau01 zenon_X10))) != (g1 zenon_X0))
% 1.02/1.27  (zenon_Vgd >= (1))
% 1.02/1.27  ((tau01 zenon_X2) > (g2 (d2 (tau11 zenon_X10))))
% 1.02/1.27  (-. (r2 (0)))
% 1.02/1.27  ((g2 (d2 zenon_X4)) <= (0))
% 1.02/1.27  (((g2 (d2 (tau11 zenon_X10))) - (g1 zenon_X0)) <= (-1))
% 1.02/1.27  (zenon_Vpb >= (0))
% 1.02/1.27  ((g2 zenon_X1) <= (1))
% 1.02/1.27  ((lambdai2 (tau01 zenon_X7)) >= (lambdai2 zenon_X7))
% 1.02/1.27  (zenon_Vjd >= (1))
% 1.02/1.27  (((d2 (tau00 zenon_X10)) - (d2 (tau11 zenon_X10))) >= (1))
% 1.02/1.27  ((0) < (1))
% 1.02/1.27  (zenon_Vfh >= (1))
% 1.02/1.27  (zenon_Vsb >= (0))
% 1.02/1.27  (((tau11 zenon_X2) - (g2 (taur2b2 (g1 (d1 zenon_X10)) (d2 zenon_X10)))) >= (1))
% 1.02/1.27  ((g2 (d2 zenon_X4)) >= (0))
% 1.02/1.27  (zenon_Vri >= (1))
% 1.02/1.27  (lambdab1 (0))
% 1.02/1.27  (zenon_Vtc >= (0))
% 1.02/1.27  (zenon_Vti = ((tau11 zenon_X2) - (g2 (d2 (tau01 zenon_X10)))))
% 1.02/1.27  (((g2 (d2 zenon_X4)) - (g2 zenon_X1)) <= (-1))
% 1.02/1.27  ((zenon_X1 - (taur2b2 (g1 (d1 zenon_X10)) (d2 zenon_X10))) <= (-1))
% 1.02/1.27  ((g1 zenon_X0) != (g2 (taur2b2 (g1 (d1 zenon_X10)) (d2 zenon_X10))))
% 1.02/1.27  ((tau01 zenon_X2) > (0))
% 1.02/1.27  (zenon_Voi >= (1))
% 1.02/1.27  (zenon_Vte = ((d2 (tau10 zenon_X10)) - (d2 (tau11 zenon_X10))))
% 1.02/1.27  (-. (r2 (tau00 zenon_X2)))
% 1.02/1.27  (zenon_Vth <= (-1))
% 1.02/1.27  (zenon_Vni = ((tau10 zenon_X2) - (g2 (d2 zenon_X4))))
% 1.02/1.27  (zenon_Vob = ((lambdai2 (tau10 zenon_X5)) - (lambdai1 zenon_X5)))
% 1.02/1.27  ((tau01 zenon_X2) > (tau00 zenon_X2))
% 1.02/1.27  (zenon_Vte >= (1))
% 1.02/1.27  ((tau10 zenon_X2) != (g2 (d2 (tau10 zenon_X10))))
% 1.02/1.27  (zenon_Vhi = ((tau10 zenon_X2) - (g2 (taur22 (g1 (d1 zenon_X10)) (d2 zenon_X10)))))
% 1.02/1.27  (((d2 (tau10 zenon_X10)) - (d2 (tau01 zenon_X10))) >= (1))
% 1.02/1.27  (zenon_Vnc = ((d1 (tau01 zenon_X9)) - (d1 (tau00 zenon_X9))))
% 1.02/1.27  (((d2 (tau10 zenon_X10)) - (d2 (tau11 zenon_X10))) >= (1))
% 1.02/1.27  (zenon_Vrc = ((taur22 (g1 (d1 zenon_X10)) (d2 zenon_X10)) - (d2 (tau01 zenon_X10))))
% 1.02/1.27  ((g2 (d2 (tau01 zenon_X10))) <= (0))
% 1.02/1.27  ((tau11 zenon_X2) != (g2 (d2 zenon_X4)))
% 1.02/1.27  ((tau11 zenon_X2) != (g2 (taur22 (g1 (d1 zenon_X10)) (d2 zenon_X10))))
% 1.02/1.27  (zenon_Vod = ((d2 (tau00 zenon_X10)) - (d2 zenon_X4)))
% 1.02/1.27  (((tau01 zenon_X2) - (tau10 zenon_X2)) >= (1))
% 1.02/1.27  (((tau11 zenon_X2) - (tau01 zenon_X2)) >= (1))
% 1.02/1.27  (zenon_Vli >= (1))
% 1.02/1.27  (zenon_Vsc <= (0))
% 1.02/1.27  ((d2 (tau01 zenon_X10)) != zenon_X1)
% 1.02/1.27  (zenon_Vzb >= (0))
% 1.02/1.27  ((- (g2 zenon_X1)) <= (-1))
% 1.02/1.27  (zenon_Vlh <= (-1))
% 1.02/1.27  (lambdab3 (tau10 zenon_X6))
% 1.02/1.27  (zenon_Vvd >= (1))
% 1.02/1.27  (-. (r1 (tau01 zenon_X2)))
% 1.02/1.27  (((d2 (tau11 zenon_X10)) - (d2 (tau01 zenon_X10))) >= (0))
% 1.02/1.27  ((tau10 zenon_X10) != zenon_X4)
% 1.02/1.27  (((tau01 zenon_X2) - (g2 (d2 (tau00 zenon_X10)))) >= (1))
% 1.02/1.27  (zenon_Vci >= (1))
% 1.02/1.27  ((g2 zenon_X1) > (g2 (taur22 (g1 (d1 zenon_X10)) (d2 zenon_X10))))
% 1.02/1.27  (((tau11 zenon_X10) - zenon_X4) >= (1))
% 1.02/1.27  ((g2 zenon_X1) >= (1))
% 1.02/1.27  (((d2 (tau11 zenon_X10)) - (d2 zenon_X4)) >= (1))
% 1.02/1.27  ((lambdai3 (tau01 zenon_X6)) >= (lambdai1 zenon_X6))
% 1.02/1.27  (zenon_Vdh = ((d2 (tau01 zenon_X10)) - (taur2b2 (g1 (d1 zenon_X10)) (d2 zenon_X10))))
% 1.02/1.27  (((g2 (d2 (tau01 zenon_X10))) - (g2 zenon_X1)) <= (-1))
% 1.02/1.27  (zenon_Vm = ((lambdai1 (tau11 zenon_X3)) - (lambdai1 zenon_X3)))
% 1.02/1.27  (zenon_Vm >= (0))
% 1.02/1.27  (zenon_Vub = ((lambdai3 (tau00 zenon_X6)) - (lambdai1 zenon_X6)))
% 1.02/1.27  (zenon_Vnh = ((d2 (tau11 zenon_X10)) - (taur2b2 (g1 (d1 zenon_X10)) (d2 zenon_X10))))
% 1.02/1.27  (zenon_Vld >= (1))
% 1.02/1.27  ((lambdai3 (tau11 zenon_X6)) >= (lambdai1 zenon_X6))
% 1.02/1.27  (zenon_Vmi = ((tau10 zenon_X2) - (g2 (d2 (tau01 zenon_X10)))))
% 1.02/1.27  ((d2 (tau00 zenon_X10)) > (d2 (tau11 zenon_X10)))
% 1.02/1.27  ((tau01 zenon_X2) > (tau10 zenon_X2))
% 1.02/1.27  (zenon_X1 < (d2 (tau11 zenon_X10)))
% 1.02/1.27  (zenon_Vjc = ((taur1b1 (g2 (d2 zenon_X9)) (d1 zenon_X9)) - (d1 (tau01 zenon_X9))))
% 1.02/1.27  (zenon_Vvc = ((taur2b2 (g1 (d1 zenon_X10)) (d2 zenon_X10)) - (d2 (tau10 zenon_X10))))
% 1.02/1.27  ((g2 (d2 (tau11 zenon_X10))) < (g1 zenon_X0))
% 1.02/1.27  (zenon_Vei = ((tau01 zenon_X2) - (g2 (d2 (tau00 zenon_X10)))))
% 1.02/1.27  (((tau10 zenon_X10) - (tau01 zenon_X10)) >= (1))
% 1.02/1.27  ((tau11 zenon_X2) != (g2 (d2 (tau10 zenon_X10))))
% 1.02/1.27  ((tau01 zenon_X10) != zenon_X4)
% 1.02/1.27  ((d2 (tau10 zenon_X10)) > (d2 (tau11 zenon_X10)))
% 1.02/1.27  (zenon_Vhh = ((g2 (d2 (tau11 zenon_X10))) - (g2 zenon_X1)))
% 1.02/1.27  (zenon_Vqe <= (-1))
% 1.02/1.27  ((d2 (tau11 zenon_X10)) = (d2 (tau01 zenon_X10)))
% 1.02/1.27  (((d2 (tau10 zenon_X10)) - (d2 (tau00 zenon_X10))) >= (0))
% 1.02/1.27  ((tau11 zenon_X2) > (0))
% 1.02/1.27  ((d2 (tau01 zenon_X10)) > (d2 zenon_X4))
% 1.02/1.27  ((g2 (d2 zenon_X4)) = (0))
% 1.02/1.27  ((d1 (tau11 zenon_X9)) = (d1 (tau10 zenon_X9)))
% 1.02/1.27  (zenon_Vxc >= (0))
% 1.02/1.27  ((g2 (d2 zenon_X4)) < (g1 zenon_X0))
% 1.02/1.27  (((taur1b1 (g2 (d2 zenon_X9)) (d1 zenon_X9)) - (d1 (tau01 zenon_X9))) <= (0))
% 1.02/1.27  (zenon_Vqc = ((taur22 (g1 (d1 zenon_X10)) (d2 zenon_X10)) - (d2 (tau11 zenon_X10))))
% 1.02/1.27  (-. (r1 (tau00 zenon_X2)))
% 1.02/1.27  (lambdab3 (tau11 zenon_X8))
% 1.02/1.27  ((g2 (d2 (tau11 zenon_X10))) >= (0))
% 1.02/1.27  ((0) < (g1 zenon_X0))
% 1.02/1.27  (zenon_Vcd = ((g2 (d2 zenon_X4)) - (g2 zenon_X1)))
% 1.02/1.27  (zenon_Vri = ((tau11 zenon_X2) - (g2 (d2 (tau11 zenon_X10)))))
% 1.02/1.27  (((tau11 zenon_X2) - (g2 (d2 (tau01 zenon_X10)))) >= (1))
% 1.02/1.27  ((tau01 zenon_X2) != (tau10 zenon_X2))
% 1.02/1.27  ((taur11 (g2 (d2 zenon_X9)) (d1 zenon_X9)) = (d1 (tau11 zenon_X9)))
% 1.02/1.27  (zenon_Vyb = ((lambdai2 (tau00 zenon_X7)) - (lambdai2 zenon_X7)))
% 1.02/1.27  (zenon_Vjh <= (-1))
% 1.02/1.27  (zenon_Vpd >= (1))
% 1.02/1.27  (zenon_Vdd >= (1))
% 1.02/1.27  ((d2 (tau11 zenon_X10)) != (taur2b2 (g1 (d1 zenon_X10)) (d2 zenon_X10)))
% 1.02/1.27  (zenon_Vob >= (0))
% 1.02/1.27  (((d1 (tau11 zenon_X9)) - (d1 (tau10 zenon_X9))) >= (0))
% 1.02/1.27  (zenon_Vrb = ((lambdai3 (tau11 zenon_X6)) - (lambdai1 zenon_X6)))
% 1.02/1.27  ((g2 (d2 (tau00 zenon_X10))) < (g1 zenon_X0))
% 1.02/1.27  (((tau01 zenon_X2) - (tau00 zenon_X2)) >= (1))
% 1.02/1.27  ((g2 zenon_X1) = (1))
% 1.02/1.27  ((lambdai2 (tau10 zenon_X7)) >= (lambdai2 zenon_X7))
% 1.02/1.27  ((tau00 zenon_X10) != (tau01 zenon_X10))
% 1.02/1.27  ((- (g2 (taur2b2 (g1 (d1 zenon_X10)) (d2 zenon_X10)))) >= (0))
% 1.02/1.27  ((d2 zenon_X4) != (taur2b2 (g1 (d1 zenon_X10)) (d2 zenon_X10)))
% 1.02/1.27  ((tau11 zenon_X2) > (g2 (taur2b2 (g1 (d1 zenon_X10)) (d2 zenon_X10))))
% 1.02/1.27  ((tau11 zenon_X2) > (tau10 zenon_X2))
% 1.02/1.27  (zenon_Vki = ((tau10 zenon_X2) - (g2 (d2 (tau11 zenon_X10)))))
% 1.02/1.27  (zenon_Vse <= (-1))
% 1.02/1.27  ((d2 (tau10 zenon_X10)) > (d2 zenon_X4))
% 1.02/1.27  ((g2 (taur2b2 (g1 (d1 zenon_X10)) (d2 zenon_X10))) = (0))
% 1.02/1.27  ((d2 zenon_X4) > zenon_X1)
% 1.02/1.27  ((d2 (tau00 zenon_X10)) != (d2 (tau01 zenon_X10)))
% 1.02/1.27  (zenon_Vih >= (1))
% 1.02/1.27  ((tau11 zenon_X2) > (tau00 zenon_X2))
% 1.02/1.27  ((tau10 zenon_X2) > (g2 (taur22 (g1 (d1 zenon_X10)) (d2 zenon_X10))))
% 1.02/1.27  ((tau01 zenon_X2) != (0))
% 1.02/1.27  (zenon_Vph >= (1))
% 1.02/1.27  (zenon_Vyh >= (1))
% 1.02/1.27  (lambdab3 (tau11 zenon_X6))
% 1.02/1.27  (((tau10 zenon_X2) - (g2 (taur22 (g1 (d1 zenon_X10)) (d2 zenon_X10)))) >= (1))
% 1.02/1.27  (zenon_Vqi >= (1))
% 1.02/1.27  (((taur11 (g2 (d2 zenon_X9)) (d1 zenon_X9)) - (d1 (tau11 zenon_X9))) <= (0))
% 1.02/1.27  (zenon_Vdc >= (0))
% 1.02/1.27  ((tau11 zenon_X10) > zenon_X4)
% 1.02/1.27  (lambdab3 (tau00 zenon_X8))
% 1.02/1.27  (zenon_Vlc = ((taur1b1 (g2 (d2 zenon_X9)) (d1 zenon_X9)) - (d1 (tau00 zenon_X9))))
% 1.02/1.27  ((d2 (tau00 zenon_X10)) != (taur22 (g1 (d1 zenon_X10)) (d2 zenon_X10)))
% 1.02/1.27  ((taur2b2 (g1 (d1 zenon_X10)) (d2 zenon_X10)) > (taur22 (g1 (d1 zenon_X10)) (d2 zenon_X10)))
% 1.02/1.27  ((taur2b2 (g1 (d1 zenon_X10)) (d2 zenon_X10)) = (d2 (tau10 zenon_X10)))
% 1.02/1.27  (((d2 (tau10 zenon_X10)) - (d2 (tau00 zenon_X10))) <= (0))
% 1.02/1.27  ((d2 (tau01 zenon_X10)) < (taur2b2 (g1 (d1 zenon_X10)) (d2 zenon_X10)))
% 1.02/1.27  (zenon_Vpi = ((tau11 zenon_X2) - (g2 (taur2b2 (g1 (d1 zenon_X10)) (d2 zenon_X10)))))
% 1.02/1.27  (zenon_Vji = ((tau10 zenon_X2) - (g2 (d2 (tau10 zenon_X10)))))
% 1.02/1.27  (((tau10 zenon_X2) - (g2 (d2 (tau01 zenon_X10)))) >= (1))
% 1.02/1.27  ((tau11 zenon_X10) != zenon_X4)
% 1.02/1.27  (zenon_Vgh >= (1))
% 1.02/1.27  ((g2 (d2 (tau10 zenon_X10))) < (g2 zenon_X1))
% 1.02/1.27  ((lambdai1 (tau01 zenon_X3)) >= (lambdai1 zenon_X3))
% 1.02/1.27  (zenon_Vrh = ((g2 (d2 (tau10 zenon_X10))) - (g1 zenon_X0)))
% 1.02/1.27  (zenon_Vvh >= (1))
% 1.02/1.27  (zenon_Vn = ((lambdai1 (tau10 zenon_X3)) - (lambdai1 zenon_X3)))
% 1.02/1.27  ((tau11 zenon_X2) > (g2 (d2 (tau10 zenon_X10))))
% 1.02/1.27  ((g2 (d2 (tau11 zenon_X10))) != (1))
% 1.02/1.27  (lambdab2 (tau01 zenon_X7))
% 1.02/1.27  (zenon_Vyb >= (0))
% 1.02/1.27  ((tau01 zenon_X2) != (tau00 zenon_X2))
% 1.02/1.27  (zenon_Vwb = ((lambdai2 (tau10 zenon_X7)) - (lambdai2 zenon_X7)))
% 1.02/1.27  (zenon_Vuh >= (1))
% 1.02/1.27  ((g2 (d2 (tau10 zenon_X10))) != (g1 zenon_X0))
% 1.02/1.27  (zenon_Vhc >= (0))
% 1.02/1.27  (zenon_Vkd = ((d2 (tau01 zenon_X10)) - (d2 zenon_X4)))
% 1.02/1.27  ((g2 (d2 (tau00 zenon_X10))) < (g2 zenon_X1))
% 1.02/1.27  ((g2 (d2 zenon_X4)) != (g1 zenon_X0))
% 1.02/1.27  (((d2 (tau10 zenon_X10)) - (d2 zenon_X4)) >= (1))
% 1.02/1.27  (zenon_Vye = ((d2 zenon_X4) - (taur2b2 (g1 (d1 zenon_X10)) (d2 zenon_X10))))
% 1.02/1.27  ((tau01 zenon_X2) != (g2 (d2 zenon_X4)))
% 1.02/1.27  (zenon_Vic = ((d1 (tau11 zenon_X9)) - (d1 (tau10 zenon_X9))))
% 1.02/1.27  (lambdab1 (tau01 zenon_X3))
% 1.02/1.27  (zenon_Vfh = ((tau01 zenon_X2) - (tau00 zenon_X2)))
% 1.02/1.27  (zenon_Vvb = ((lambdai2 (tau11 zenon_X7)) - (lambdai2 zenon_X7)))
% 1.02/1.27  ((zenon_X1 - (taur22 (g1 (d1 zenon_X10)) (d2 zenon_X10))) <= (-1))
% 1.02/1.27  ((tau10 zenon_X2) > (g2 (taur2b2 (g1 (d1 zenon_X10)) (d2 zenon_X10))))
% 1.02/1.27  (zenon_Vmd = ((d2 (tau10 zenon_X10)) - (d2 zenon_X4)))
% 1.02/1.27  ((tau01 zenon_X10) > zenon_X4)
% 1.02/1.27  (lambdab3 (tau10 zenon_X8))
% 1.02/1.27  (zenon_Vnd >= (1))
% 1.02/1.27  ((g2 (d2 (tau11 zenon_X10))) < (1))
% 1.02/1.27  ((lambdai3 (tau10 zenon_X6)) >= (lambdai1 zenon_X6))
% 1.02/1.27  (zenon_Vui >= (1))
% 1.02/1.27  (zenon_Vrb >= (0))
% 1.02/1.27  ((g2 (d2 (tau01 zenon_X10))) >= (0))
% 1.02/1.27  ((g2 (d2 (tau11 zenon_X10))) != (g2 zenon_X1))
% 1.02/1.27  (((tau01 zenon_X2) - (g2 (d2 (tau10 zenon_X10)))) >= (1))
% 1.02/1.27  (zenon_Vzc >= (0))
% 1.02/1.27  (zenon_Vbc = ((lambdai3 (tau01 zenon_X8)) - (lambdai3 zenon_X8)))
% 1.02/1.27  (zenon_Vdi >= (1))
% 1.02/1.27  (((taur22 (g1 (d1 zenon_X10)) (d2 zenon_X10)) - (d2 (tau01 zenon_X10))) >= (0))
% 1.02/1.27  (((taur1b1 (g2 (d2 zenon_X9)) (d1 zenon_X9)) - (d1 (tau00 zenon_X9))) >= (0))
% 1.02/1.27  (((g2 (d2 (tau10 zenon_X10))) - (g1 zenon_X0)) <= (-1))
% 1.02/1.27  (lambdab2 (tau11 zenon_X7))
% 1.02/1.27  (zenon_Vwb >= (0))
% 1.02/1.27  ((d2 (tau10 zenon_X10)) != (taur22 (g1 (d1 zenon_X10)) (d2 zenon_X10)))
% 1.02/1.27  (zenon_Vxd = ((tau00 zenon_X10) - (tau01 zenon_X10)))
% 1.02/1.27  (zenon_Vsc = ((taur22 (g1 (d1 zenon_X10)) (d2 zenon_X10)) - (d2 (tau01 zenon_X10))))
% 1.02/1.27  ((g2 (taur2b2 (g1 (d1 zenon_X10)) (d2 zenon_X10))) <= (0))
% 1.02/1.27  (zenon_X1 < (d2 (tau10 zenon_X10)))
% 1.02/1.27  (zenon_Vse = ((d2 zenon_X4) - (taur22 (g1 (d1 zenon_X10)) (d2 zenon_X10))))
% 1.02/1.27  ((0) != (g2 zenon_X1))
% 1.02/1.27  (((tau11 zenon_X2) - (g2 (d2 zenon_X4))) >= (1))
% 1.02/1.27  (zenon_Voc <= (0))
% 1.02/1.27  ((g2 (taur22 (g1 (d1 zenon_X10)) (d2 zenon_X10))) = (0))
% 1.02/1.27  (zenon_Vkh = ((g2 (d2 (tau01 zenon_X10))) - (g2 zenon_X1)))
% 1.02/1.27  (((taur11 (g2 (d2 zenon_X9)) (d1 zenon_X9)) - (d1 (tau11 zenon_X9))) >= (0))
% 1.02/1.27  (((taur2b2 (g1 (d1 zenon_X10)) (d2 zenon_X10)) - (d2 (tau10 zenon_X10))) >= (0))
% 1.02/1.27  ((g1 zenon_X0) > (g2 (taur2b2 (g1 (d1 zenon_X10)) (d2 zenon_X10))))
% 1.02/1.27  (zenon_Vci = ((tau01 zenon_X2) - (g2 (d2 (tau10 zenon_X10)))))
% 1.02/1.27  (lambdab2 (tau00 zenon_X5))
% 1.02/1.27  ((d2 (tau00 zenon_X10)) != zenon_X1)
% 1.02/1.27  (zenon_Vzh >= (1))
% 1.02/1.27  ((d2 (tau11 zenon_X10)) != (d2 zenon_X4))
% 1.02/1.27  ((d2 (tau00 zenon_X10)) > (d2 zenon_X4))
% 1.02/1.27  (zenon_Vtb = ((lambdai3 (tau01 zenon_X6)) - (lambdai1 zenon_X6)))
% 1.02/1.27  *)
% 1.02/1.27  (* NO-PROOF *)
% 1.02/1.27  % SZS status GaveUp
% 1.02/1.27  Number of rewrites on terms: 0
% 1.02/1.27  Number of rewrites on props: 0
% 1.02/1.27  nodes searched: 1996
% 1.02/1.27  max branch formulas: 629
% 1.02/1.27  proof nodes created: 252
% 1.02/1.27  formulas created: 6130
% 1.02/1.27  
%------------------------------------------------------------------------------