%------------------------------------------------------------------------------ % File : ZenonModulo---0.5.0 % Problem : LCL671+1.010 : TPTP v9.3.1. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : run_zenon_modulo %d %s % Computer : n019.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Mon Sep 7 01:34:23 PM UTC 2026 % Result : Unknown 0.16s 0.70s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LCL671+1.010 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.03 % Command : run_zenon_modulo %d %s % 0.08/0.35 % Computer : n019.cluster.edu % 0.08/0.35 % Model : x86_64 x86_64 % 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.35 % Memory : 8046.5625MB % 0.08/0.35 % OS : Linux 6.8.0-71-generic % 0.08/0.35 % CPULimit : 300 % 0.08/0.35 % WCLimit : 300 % 0.08/0.35 % DateTime : Fri Sep 4 13:43:38 UTC 2026 % 0.08/0.35 % CPUTime : % 0.38/0.70 Zenon error: exhausted search space without finding a proof % 0.38/0.70 (* Current branch: % 0.38/0.70 (r1 zenon_Vgb zenon_Vjb) % 0.38/0.70 (zenon_Vzf != zenon_Vgf) % 0.38/0.70 (zenon_Vfi != zenon_Vtd) % 0.38/0.70 (zenon_Vfi != zenon_Vbd) % 0.38/0.70 (zenon_Veg != zenon_Vwe) % 0.38/0.70 (zenon_Vaf != zenon_Vnb) % 0.38/0.70 (zenon_Vzf != zenon_Vug) % 0.38/0.70 (zenon_Vzf != zenon_Vzg) % 0.38/0.70 (zenon_Vri != zenon_Vqf) % 0.38/0.70 (zenon_Vxj != zenon_Vxc) % 0.38/0.70 (zenon_Vph != zenon_Vlf) % 0.38/0.70 (zenon_Vkf != zenon_Vag) % 0.38/0.70 (zenon_Vlj != zenon_Vxd) % 0.38/0.70 (r1 zenon_Vyd zenon_Vzd) % 0.38/0.70 (zenon_Vth != zenon_Vvf) % 0.38/0.70 (zenon_Vxj != zenon_Vqd) % 0.38/0.70 (zenon_Vzi != zenon_Vre) % 0.38/0.70 (zenon_Vsd != zenon_Vce) % 0.38/0.70 (zenon_Vri != zenon_Vpc) % 0.38/0.70 (zenon_Vqe != zenon_Vqd) % 0.38/0.70 (zenon_Vdh != zenon_Vlf) % 0.38/0.70 (zenon_Vpf != zenon_Vce) % 0.38/0.70 (zenon_Vpj != zenon_Vjb) % 0.38/0.70 (zenon_Vbk != zenon_Vvb) % 0.38/0.70 (zenon_Veg != zenon_Vzb) % 0.38/0.70 (zenon_Vxj != zenon_Vvf) % 0.38/0.70 (zenon_Vbk != zenon_Vlf) % 0.38/0.70 (zenon_Vbe != zenon_Vnd) % 0.38/0.70 (zenon_Vkf != zenon_Vrb) % 0.38/0.70 (zenon_Vwd != zenon_Vqd) % 0.38/0.70 (zenon_Vxh != zenon_Vlc) % 0.38/0.70 (zenon_Vph != zenon_Vbd) % 0.38/0.70 (r1 zenon_Vrf zenon_Vsf) % 0.38/0.70 (zenon_Veg != zenon_Vxd) % 0.38/0.70 (zenon_Vhj != zenon_Vgf) % 0.38/0.70 (zenon_Vek != zenon_Vvb) % 0.38/0.70 (zenon_Vbi != zenon_Vbd) % 0.38/0.70 (-. (p1 zenon_Vug)) % 0.38/0.70 (zenon_Vpf != zenon_Vxc) % 0.38/0.70 (zenon_Vtg != zenon_Vbd) % 0.38/0.70 (zenon_Vog != zenon_Vnd) % 0.38/0.70 (zenon_Vdh != zenon_Vgf) % 0.38/0.70 (zenon_Veg != zenon_Vfd) % 0.38/0.70 (zenon_Vaf != zenon_Vvb) % 0.38/0.70 (zenon_Vth != zenon_Vfd) % 0.38/0.70 (zenon_Vlh != zenon_Vrb) % 0.38/0.70 (zenon_Vlh != zenon_Vvf) % 0.38/0.70 (zenon_Vdj != zenon_Vjd) % 0.38/0.70 (zenon_Vve != zenon_Vgf) % 0.38/0.70 (zenon_Vqe != zenon_Vkg) % 0.38/0.70 (p1 zenon_Vdj) % 0.38/0.70 (zenon_Vaf != zenon_Vxd) % 0.38/0.70 (zenon_Vle != zenon_Vre) % 0.38/0.70 (zenon_Veg != zenon_Vce) % 0.38/0.70 (zenon_Vaf != zenon_Vqd) % 0.38/0.70 (zenon_Vpj != zenon_Vjd) % 0.38/0.70 (zenon_Vhj != zenon_Vjd) % 0.38/0.70 (zenon_Vjg != zenon_Vlc) % 0.38/0.70 (zenon_Vjg != zenon_Vnb) % 0.38/0.70 (zenon_Vfi != zenon_Vhc) % 0.38/0.70 (zenon_Vff != zenon_Vkg) % 0.38/0.70 (zenon_Vji != zenon_Vme) % 0.38/0.70 (zenon_Vri != zenon_Vpg) % 0.38/0.70 (zenon_Vhj != zenon_Vrb) % 0.38/0.70 (zenon_Vth != zenon_Vrb) % 0.38/0.70 (zenon_Vxj != zenon_Vnb) % 0.38/0.70 (zenon_Vlh != zenon_Vbf) % 0.38/0.70 (zenon_Vqe != zenon_Vre) % 0.38/0.70 (zenon_Vri != zenon_Vfb) % 0.38/0.70 (zenon_Vzf != zenon_Vfg) % 0.38/0.70 (zenon_Vaf != zenon_Vpg) % 0.38/0.70 (zenon_Vve != zenon_Vhc) % 0.38/0.70 (zenon_Vsd != zenon_Vtd) % 0.38/0.70 (zenon_Vyg != zenon_Vgf) % 0.38/0.70 (zenon_Vff != zenon_Vug) % 0.38/0.70 (zenon_Vle != zenon_Vxc) % 0.38/0.70 (zenon_Vpj != zenon_Vzg) % 0.38/0.70 (zenon_Vbk != zenon_Vqf) % 0.38/0.70 (zenon_Vlh != zenon_Vjb) % 0.38/0.70 (zenon_Vtg != zenon_Vnd) % 0.38/0.70 (zenon_Vpf != zenon_Vlc) % 0.38/0.70 (zenon_Vuf != zenon_Vfg) % 0.38/0.70 (zenon_Vxj != zenon_Vpg) % 0.38/0.70 (zenon_Vek != zenon_Vre) % 0.38/0.70 (zenon_Vdh != zenon_Vkg) % 0.38/0.70 (zenon_Vfi != zenon_Vre) % 0.38/0.70 (zenon_Vqe != zenon_Vnb) % 0.38/0.70 (zenon_Vff != zenon_Vbd) % 0.38/0.70 (zenon_Vbk != zenon_Vgf) % 0.38/0.70 (zenon_Vsd != zenon_Vxc) % 0.38/0.70 (zenon_Vdh != zenon_Vlc) % 0.38/0.70 (zenon_Vbe != zenon_Vlf) % 0.38/0.70 (zenon_Vxj != zenon_Vdc) % 0.38/0.70 (r1 zenon_Vic zenon_Vlc) % 0.38/0.70 (zenon_Vtg != zenon_Vbf) % 0.38/0.70 (zenon_Vzf != zenon_Vqf) % 0.38/0.70 (zenon_Vzi != zenon_Vlf) % 0.38/0.70 (zenon_Vlh != zenon_Vzb) % 0.38/0.70 (zenon_Vni != zenon_Vjd) % 0.38/0.70 (zenon_Vji != zenon_Veh) % 0.38/0.70 (zenon_Vdh != zenon_Vnd) % 0.38/0.70 (zenon_Vtj != zenon_Vnb) % 0.38/0.70 (zenon_Vxh != zenon_Vdc) % 0.38/0.70 (zenon_Vzf != zenon_Vjb) % 0.38/0.70 (zenon_Vbe != zenon_Vfb) % 0.38/0.70 (zenon_Vdj != zenon_Vhc) % 0.38/0.70 (zenon_Vth != zenon_Vbf) % 0.38/0.70 (zenon_Vog != zenon_Vwe) % 0.38/0.70 (zenon_Vog != zenon_Vnb) % 0.38/0.70 (zenon_Vhj != zenon_Vbd) % 0.38/0.70 (zenon_Vaf != zenon_Vnd) % 0.38/0.70 (zenon_Vlh != zenon_Vlc) % 0.38/0.70 (zenon_Vdj != zenon_Vqd) % 0.38/0.70 (zenon_Vni != zenon_Vbb) % 0.38/0.70 (r1 zenon_Vwf zenon_Vbg) % 0.38/0.70 (zenon_Vji != zenon_Vhe) % 0.38/0.70 (zenon_Vge != zenon_Vme) % 0.38/0.70 (zenon_Vbi != zenon_Vqd) % 0.38/0.70 (zenon_Vve != zenon_Vlf) % 0.38/0.70 (zenon_Vwd != zenon_Vbb) % 0.38/0.70 (zenon_Vog != zenon_Vvf) % 0.38/0.70 (r1 zenon_Vec zenon_Vhc) % 0.38/0.70 (zenon_Vxj != zenon_Vvb) % 0.38/0.70 (zenon_Vdj != zenon_Vvb) % 0.38/0.70 (zenon_Vek != zenon_Vgf) % 0.38/0.70 (zenon_Vfi != zenon_Vlf) % 0.38/0.70 (r1 zenon_Vse zenon_Vxe) % 0.38/0.70 (zenon_Veg != zenon_Vpg) % 0.38/0.70 (zenon_Vvi != zenon_Vgf) % 0.38/0.70 (zenon_Vpj != zenon_Vtd) % 0.38/0.70 (zenon_Vwd != zenon_Vbd) % 0.38/0.70 (zenon_Vji != zenon_Vlc) % 0.38/0.70 (zenon_Vpf != zenon_Vbb) % 0.38/0.70 (zenon_Vlh != zenon_Vpg) % 0.38/0.70 (zenon_Vek != zenon_Vxc) % 0.38/0.70 (zenon_Vzi != zenon_Vjd) % 0.38/0.70 (zenon_Vbk != zenon_Vqd) % 0.38/0.70 (r1 zenon_Vkd zenon_Vnd) % 0.38/0.70 (r1 zenon_Voi zenon_Vri) % 0.38/0.70 (zenon_Vog != zenon_Vre) % 0.38/0.70 (zenon_Vek != zenon_Vkg) % 0.38/0.70 (zenon_Vvi != zenon_Vme) % 0.38/0.70 (zenon_Vjg != zenon_Vqf) % 0.38/0.70 (zenon_Vri != zenon_Vtc) % 0.38/0.70 (zenon_Vvi != zenon_Vhc) % 0.38/0.70 (zenon_Vbi != zenon_Vbb) % 0.38/0.70 (zenon_Vle != zenon_Vme) % 0.38/0.70 (r1 zenon_Vse zenon_Vte) % 0.38/0.70 (zenon_Vfi != zenon_Vxc) % 0.38/0.70 (zenon_Vdh != zenon_Vjd) % 0.38/0.70 (zenon_Vji != zenon_Vvf) % 0.38/0.70 (zenon_Vpf != zenon_Vme) % 0.38/0.70 (zenon_Vlj != zenon_Vgf) % 0.38/0.70 (p1 zenon_Vpj) % 0.38/0.70 (zenon_Vfi != zenon_Vce) % 0.38/0.70 (zenon_Vxh != zenon_Vug) % 0.38/0.70 (zenon_Vri != zenon_Vtd) % 0.38/0.70 (zenon_Vkf != zenon_Vvf) % 0.38/0.70 (zenon_Vdj != zenon_Vbf) % 0.38/0.70 (r1 zenon_Vxe zenon_Vye) % 0.38/0.70 (zenon_Vbe != zenon_Vpc) % 0.38/0.70 (zenon_Vwd != zenon_Vvb) % 0.38/0.70 (zenon_Vek != zenon_Vxd) % 0.38/0.70 (r1 zenon_Vbg zenon_Vcg) % 0.38/0.70 (zenon_Veg != zenon_Vjd) % 0.38/0.70 (zenon_Vkf != zenon_Vqd) % 0.38/0.70 (zenon_Vxj != zenon_Veh) % 0.38/0.70 (zenon_Vth != zenon_Vjd) % 0.38/0.70 (zenon_Vjg != zenon_Vfb) % 0.38/0.70 (zenon_Vji != zenon_Vqd) % 0.38/0.70 (zenon_Vlj != zenon_Vzg) % 0.38/0.70 (zenon_Vsd != zenon_Vkg) % 0.38/0.70 (zenon_Vyg != zenon_Vhe) % 0.38/0.70 (zenon_Vhj != zenon_Veh) % 0.38/0.70 (zenon_Vji != zenon_Vvb) % 0.38/0.70 (zenon_Vge != zenon_Vrb) % 0.38/0.70 (zenon_Vhj != zenon_Vhc) % 0.38/0.70 (zenon_Vwd != zenon_Vpc) % 0.38/0.70 (zenon_Vri != zenon_Vzb) % 0.38/0.70 (zenon_Vve != zenon_Vfb) % 0.38/0.70 (zenon_Vtj != zenon_Vhc) % 0.38/0.70 (zenon_Vpj != zenon_Vhc) % 0.38/0.70 (-. (p2 zenon_Vja)) % 0.38/0.70 (zenon_Vni != zenon_Vug) % 0.38/0.70 (zenon_Vhj != zenon_Vhe) % 0.38/0.70 (r1 zenon_Voe zenon_Vpe) % 0.38/0.70 (zenon_Vff != zenon_Vlf) % 0.38/0.70 (zenon_Vqe != zenon_Vfb) % 0.38/0.70 (zenon_Vri != zenon_Vzg) % 0.38/0.70 (zenon_Vaf != zenon_Vqf) % 0.38/0.70 (zenon_Vek != zenon_Vvf) % 0.38/0.70 (zenon_Vsd != zenon_Vfd) % 0.38/0.70 (zenon_Vge != zenon_Vfg) % 0.38/0.70 (zenon_Vwd != zenon_Vme) % 0.38/0.70 (zenon_Vkf != zenon_Vzg) % 0.38/0.70 (zenon_Vtj != zenon_Vvb) % 0.38/0.70 (zenon_Vyg != zenon_Vqd) % 0.38/0.70 (p1 zenon_Vri) % 0.38/0.70 (zenon_Vle != zenon_Vbb) % 0.38/0.70 (r1 zenon_Vwf zenon_Vxf) % 0.38/0.70 (zenon_Vpj != zenon_Vnd) % 0.38/0.70 (zenon_Vni != zenon_Vlf) % 0.38/0.70 (zenon_Vbe != zenon_Vlc) % 0.38/0.70 (zenon_Vlj != zenon_Vxc) % 0.38/0.70 (zenon_Vfi != zenon_Vvb) % 0.38/0.70 (zenon_Vjg != zenon_Vqd) % 0.38/0.70 (zenon_Veg != zenon_Veh) % 0.38/0.70 (zenon_Vyg != zenon_Vtd) % 0.38/0.70 (zenon_Vsd != zenon_Vvf) % 0.38/0.70 (zenon_Vge != zenon_Vug) % 0.38/0.70 (zenon_Vxh != zenon_Vpc) % 0.38/0.70 (zenon_Vle != zenon_Vhe) % 0.38/0.70 (zenon_Vdj != zenon_Vzg) % 0.38/0.70 (zenon_Vph != zenon_Vtc) % 0.38/0.70 (zenon_Vjg != zenon_Vhc) % 0.38/0.70 (zenon_Vpf != zenon_Vkg) % 0.38/0.70 (zenon_Vqe != zenon_Vag) % 0.38/0.70 (zenon_Vtg != zenon_Vce) % 0.38/0.70 (zenon_Vzi != zenon_Vxc) % 0.38/0.70 (zenon_Vtg != zenon_Vqd) % 0.38/0.70 (zenon_Vzi != zenon_Vag) % 0.38/0.70 (zenon_Vhj != zenon_Vqf) % 0.38/0.70 (zenon_Vfi != zenon_Vfb) % 0.38/0.70 (r1 zenon_Vih zenon_Vlh) % 0.38/0.70 (zenon_Vbe != zenon_Vvf) % 0.38/0.70 (zenon_Vzf != zenon_Vfb) % 0.38/0.70 (r1 zenon_Vcg zenon_Vfg) % 0.38/0.70 (zenon_Vuf != zenon_Veh) % 0.38/0.70 (r1 zenon_Vdf zenon_Vgf) % 0.38/0.70 (r1 zenon_Vrg zenon_Vsg) % 0.38/0.70 (zenon_Vpf != zenon_Vfg) % 0.38/0.70 (zenon_Vph != zenon_Vnd) % 0.38/0.70 (zenon_Veg != zenon_Vhe) % 0.38/0.70 (zenon_Vaf != zenon_Vlc) % 0.38/0.70 (zenon_Vbi != zenon_Vxd) % 0.38/0.70 (r1 zenon_Vte zenon_Vwe) % 0.38/0.70 (zenon_Vqe != zenon_Vhc) % 0.38/0.70 (zenon_Vtg != zenon_Vpc) % 0.38/0.70 (zenon_Vqe != zenon_Vxc) % 0.38/0.70 (zenon_Vve != zenon_Vlc) % 0.38/0.70 (zenon_Vfi != zenon_Vvf) % 0.38/0.70 (zenon_Vek != zenon_Vrb) % 0.38/0.70 (r1 zenon_Vcf zenon_Vhf) % 0.38/0.70 (zenon_Vth != zenon_Vag) % 0.38/0.70 (p1 zenon_Vlh) % 0.16/0.70 (zenon_Vph != zenon_Vvf) % 0.16/0.70 (zenon_Vdh != zenon_Vjb) % 0.16/0.70 (zenon_Vzi != zenon_Vzg) % 0.16/0.70 (zenon_Vzi != zenon_Vtd) % 0.16/0.70 (r1 zenon_Vda zenon_Vsa) % 0.16/0.70 (zenon_Vve != zenon_Vwe) % 0.16/0.70 (zenon_Vni != zenon_Vvf) % 0.16/0.70 (p1 zenon_Vff) % 0.16/0.70 (zenon_Vfi != zenon_Vrb) % 0.16/0.70 (zenon_Vkf != zenon_Vbd) % 0.16/0.70 (zenon_Vfi != zenon_Vpc) % 0.16/0.70 (zenon_Veg != zenon_Vbf) % 0.16/0.70 (zenon_Vkf != zenon_Vnb) % 0.16/0.70 (zenon_Vph != zenon_Vre) % 0.16/0.70 (zenon_Vve != zenon_Vzg) % 0.16/0.70 (zenon_Vlj != zenon_Vvf) % 0.16/0.70 (zenon_Vbk != zenon_Vhe) % 0.16/0.70 (zenon_Vuf != zenon_Vfd) % 0.16/0.70 (zenon_Vek != zenon_Vhc) % 0.16/0.70 (zenon_Vji != zenon_Vkg) % 0.16/0.70 (zenon_Vzi != zenon_Vwe) % 0.16/0.70 (zenon_Vff != zenon_Vqd) % 0.16/0.70 (zenon_Vfi != zenon_Vbb) % 0.16/0.70 (zenon_Vkf != zenon_Vjd) % 0.16/0.70 (zenon_Vph != zenon_Vwe) % 0.16/0.70 (zenon_Vwd != zenon_Vjb) % 0.16/0.70 (zenon_Vpf != zenon_Vqd) % 0.16/0.70 (zenon_Vxh != zenon_Vhc) % 0.16/0.70 (zenon_Vff != zenon_Vnd) % 0.16/0.70 (zenon_Vtg != zenon_Vjd) % 0.16/0.70 (zenon_Vuf != zenon_Vtd) % 0.16/0.70 (zenon_Vpj != zenon_Vkg) % 0.16/0.70 (r1 zenon_Vde zenon_Vee) % 0.16/0.70 (zenon_Vbi != zenon_Vre) % 0.16/0.70 (zenon_Vle != zenon_Vtc) % 0.16/0.70 (-. (p1 zenon_Vhe)) % 0.16/0.70 (zenon_Vlj != zenon_Vag) % 0.16/0.70 (p1 zenon_Vxj) % 0.16/0.70 (zenon_Vog != zenon_Vgf) % 0.16/0.70 (zenon_Vjg != zenon_Vag) % 0.16/0.70 (zenon_Vhj != zenon_Vxd) % 0.16/0.70 (zenon_Vxj != zenon_Vbf) % 0.16/0.70 (zenon_Vzi != zenon_Vgf) % 0.16/0.70 (zenon_Vbk != zenon_Vpg) % 0.16/0.70 (zenon_Vjg != zenon_Vlf) % 0.16/0.70 (-. (p1 zenon_Vbf)) % 0.16/0.70 (zenon_Vle != zenon_Veh) % 0.16/0.70 (zenon_Vkf != zenon_Vre) % 0.16/0.70 (zenon_Vve != zenon_Vdc) % 0.16/0.70 (zenon_Vhj != zenon_Vpc) % 0.16/0.70 (zenon_Vdh != zenon_Vbb) % 0.16/0.70 (zenon_Vxj != zenon_Vce) % 0.16/0.70 (zenon_Vwd != zenon_Vug) % 0.16/0.70 (r1 zenon_Vqg zenon_Vvg) % 0.16/0.70 (zenon_Vyg != zenon_Vce) % 0.16/0.70 (zenon_Vwd != zenon_Vzg) % 0.16/0.70 (zenon_Vjg != zenon_Vjd) % 0.16/0.70 (zenon_Vff != zenon_Vzg) % 0.16/0.70 (zenon_Vbe != zenon_Vre) % 0.16/0.70 (zenon_Vlh != zenon_Vbd) % 0.16/0.70 (r1 zenon_Vah zenon_Vbh) % 0.16/0.70 (zenon_Vri != zenon_Vhc) % 0.16/0.70 (zenon_Vdj != zenon_Vre) % 0.16/0.70 (zenon_Vqe != zenon_Vhe) % 0.16/0.70 (zenon_Vtj != zenon_Vbb) % 0.16/0.70 (zenon_Vog != zenon_Veh) % 0.16/0.70 (zenon_Vxh != zenon_Vwe) % 0.16/0.70 (zenon_Vth != zenon_Vtc) % 0.16/0.70 (zenon_Vhj != zenon_Vjb) % 0.16/0.70 (zenon_Vbe != zenon_Vce) % 0.16/0.70 (zenon_Vkf != zenon_Vfb) % 0.16/0.70 (zenon_Vpj != zenon_Vlc) % 0.16/0.70 (zenon_Vbe != zenon_Vrb) % 0.16/0.70 (zenon_Vbi != zenon_Vpc) % 0.16/0.70 (zenon_Vek != zenon_Vce) % 0.16/0.70 (zenon_Vxj != zenon_Vbd) % 0.16/0.70 (zenon_Vyg != zenon_Vjd) % 0.16/0.70 (zenon_Vfi != zenon_Vlc) % 0.16/0.70 (zenon_Vkf != zenon_Vtd) % 0.16/0.70 (-. (p1 zenon_Veh)) % 0.16/0.70 (zenon_Vkf != zenon_Vgf) % 0.16/0.70 (zenon_Vzi != zenon_Vvb) % 0.16/0.70 (zenon_Vvi != zenon_Veh) % 0.16/0.70 (zenon_Vaf != zenon_Vgf) % 0.16/0.70 (zenon_Vbi != zenon_Vzb) % 0.16/0.70 (r1 zenon_Vha zenon_Via) % 0.16/0.70 (zenon_Vth != zenon_Vpc) % 0.16/0.70 (zenon_Vve != zenon_Vqf) % 0.16/0.70 (zenon_Vpf != zenon_Vug) % 0.16/0.70 (zenon_Vji != zenon_Vpg) % 0.16/0.70 (zenon_Vtj != zenon_Vme) % 0.16/0.70 (zenon_Vff != zenon_Vxd) % 0.16/0.70 (zenon_Vkf != zenon_Vfd) % 0.16/0.70 (-. (p1 zenon_Vre)) % 0.16/0.70 (zenon_Vge != zenon_Vpg) % 0.16/0.70 (zenon_Vni != zenon_Vjb) % 0.16/0.70 (zenon_Vlj != zenon_Veh) % 0.16/0.70 (zenon_Vbi != zenon_Vug) % 0.16/0.70 (zenon_Vfi != zenon_Vme) % 0.16/0.70 (zenon_Vve != zenon_Vre) % 0.16/0.70 (zenon_Vji != zenon_Vxc) % 0.16/0.70 (zenon_Vth != zenon_Vce) % 0.16/0.70 (p1 zenon_Vwd) % 0.16/0.70 (zenon_Vqe != zenon_Vqf) % 0.16/0.70 (zenon_Vqe != zenon_Vxa) % 0.16/0.70 (zenon_Vhj != zenon_Vvb) % 0.16/0.70 (zenon_Vff != zenon_Vtc) % 0.16/0.70 (r1 zenon_Vne zenon_Vse) % 0.16/0.70 (zenon_Vbe != zenon_Vpg) % 0.16/0.70 (zenon_Vbk != zenon_Vce) % 0.16/0.70 (zenon_Veg != zenon_Vvb) % 0.16/0.70 (zenon_Vyg != zenon_Vtc) % 0.16/0.70 (zenon_Vog != zenon_Vfd) % 0.16/0.70 (r1 zenon_Voe zenon_Vre) % 0.16/0.70 (zenon_Vpj != zenon_Vfd) % 0.16/0.70 (zenon_Vff != zenon_Vpc) % 0.16/0.70 (r1 zenon_Vmf zenon_Vnf) % 0.16/0.70 (-. (p1 zenon_Vkg)) % 0.16/0.70 (zenon_Vji != zenon_Vrb) % 0.16/0.70 (zenon_Vji != zenon_Vre) % 0.16/0.70 (zenon_Vbk != zenon_Vlc) % 0.16/0.70 (zenon_Vni != zenon_Vrb) % 0.16/0.70 (zenon_Vjg != zenon_Vfd) % 0.16/0.70 (zenon_Vzi != zenon_Vrb) % 0.16/0.70 (zenon_Vaf != zenon_Vkg) % 0.16/0.70 (zenon_Vyg != zenon_Vre) % 0.16/0.70 (zenon_Vkf != zenon_Vfg) % 0.16/0.70 (zenon_Vog != zenon_Vag) % 0.16/0.70 (zenon_Vve != zenon_Vqd) % 0.16/0.70 (zenon_Vfi != zenon_Vwe) % 0.16/0.70 (zenon_Vri != zenon_Vlc) % 0.16/0.70 (p1 zenon_Vek) % 0.16/0.70 (zenon_Vqe != zenon_Vpc) % 0.16/0.70 (zenon_Veg != zenon_Vdc) % 0.16/0.70 (zenon_Vek != zenon_Vfb) % 0.16/0.70 (zenon_Vtg != zenon_Vag) % 0.16/0.70 (zenon_Vaf != zenon_Vjb) % 0.16/0.70 (r1 zenon_Vhf zenon_Vif) % 0.16/0.70 (r1 zenon_Vye zenon_Vbf) % 0.16/0.70 (zenon_Vbk != zenon_Vkg) % 0.16/0.70 (zenon_Vuf != zenon_Vqd) % 0.16/0.70 (zenon_Vpf != zenon_Vhe) % 0.16/0.70 (zenon_Vdj != zenon_Vhe) % 0.16/0.70 (zenon_Vtj != zenon_Vdc) % 0.16/0.70 (zenon_Vjg != zenon_Vzg) % 0.16/0.70 (zenon_Vbe != zenon_Vwe) % 0.16/0.70 (zenon_Vyg != zenon_Vlf) % 0.16/0.70 (zenon_Vge != zenon_Vlf) % 0.16/0.70 (zenon_Vaf != zenon_Vpc) % 0.16/0.70 (zenon_Veg != zenon_Vpc) % 0.16/0.70 (zenon_Vsd != zenon_Vqd) % 0.16/0.70 (zenon_Vbe != zenon_Vgf) % 0.16/0.70 (zenon_Vqe != zenon_Vfg) % 0.16/0.70 (zenon_Vri != zenon_Vnd) % 0.16/0.70 (p1 zenon_Veg) % 0.16/0.70 (zenon_Vzi != zenon_Vbf) % 0.16/0.70 (zenon_Vtj != zenon_Vlf) % 0.16/0.70 (zenon_Vqe != zenon_Vzg) % 0.16/0.70 (zenon_Vkf != zenon_Vwe) % 0.16/0.70 (-. (p1 zenon_Vxa)) % 0.16/0.70 (zenon_Vuf != zenon_Vxa) % 0.16/0.70 (zenon_Vve != zenon_Vfg) % 0.16/0.70 (zenon_Veg != zenon_Vgf) % 0.16/0.70 (zenon_Vhj != zenon_Vfb) % 0.16/0.70 (zenon_Vtg != zenon_Vtd) % 0.16/0.70 (r1 zenon_Vah zenon_Vfh) % 0.16/0.70 (zenon_Vzf != zenon_Vme) % 0.16/0.70 (r1 zenon_Vhg zenon_Vkg) % 0.16/0.70 (zenon_Vth != zenon_Vzb) % 0.16/0.70 (r1 zenon_Vda zenon_Voa) % 0.16/0.70 (zenon_Vbi != zenon_Vnd) % 0.16/0.70 (zenon_Vxh != zenon_Vqf) % 0.16/0.70 (p1 zenon_Vbe) % 0.16/0.70 (zenon_Vqe != zenon_Vvf) % 0.16/0.70 (zenon_Vog != zenon_Vlf) % 0.16/0.70 (zenon_Vth != zenon_Vzg) % 0.16/0.70 (zenon_Vtj != zenon_Vzb) % 0.16/0.70 (r1 zenon_Vgg zenon_Vhg) % 0.16/0.70 (zenon_Vog != zenon_Vdc) % 0.16/0.70 (zenon_Vdj != zenon_Vnb) % 0.16/0.70 (zenon_Vph != zenon_Vbb) % 0.16/0.70 (zenon_Vkf != zenon_Vhc) % 0.16/0.70 (zenon_Vri != zenon_Vjd) % 0.16/0.70 (zenon_Veg != zenon_Vag) % 0.16/0.70 (zenon_Vpf != zenon_Vqf) % 0.16/0.70 (zenon_Vve != zenon_Vhe) % 0.16/0.70 (zenon_Vge != zenon_Vbb) % 0.16/0.70 (zenon_Vhj != zenon_Vre) % 0.16/0.70 (zenon_Vkf != zenon_Vxa) % 0.16/0.70 (zenon_Vuf != zenon_Vbf) % 0.16/0.70 (zenon_Vog != zenon_Vxa) % 0.16/0.70 (zenon_Vek != zenon_Vbf) % 0.16/0.70 (zenon_Vaf != zenon_Veh) % 0.16/0.70 (zenon_Vge != zenon_Vvb) % 0.16/0.70 (zenon_Vuf != zenon_Vwe) % 0.16/0.70 (zenon_Vve != zenon_Vzb) % 0.16/0.70 (zenon_Vdj != zenon_Vbb) % 0.16/0.70 (-. (p1 zenon_Vgf)) % 0.16/0.70 (zenon_Vpj != zenon_Vhe) % 0.16/0.70 (zenon_Vph != zenon_Vlc) % 0.16/0.70 (zenon_Vfi != zenon_Vkg) % 0.16/0.70 (zenon_Vpf != zenon_Vvf) % 0.16/0.70 (zenon_Vri != zenon_Vxa) % 0.16/0.70 (zenon_Vog != zenon_Vrb) % 0.16/0.70 (zenon_Vlh != zenon_Vfd) % 0.16/0.70 (zenon_Vsd != zenon_Vnb) % 0.16/0.70 (zenon_Vkf != zenon_Vxd) % 0.16/0.70 (zenon_Vlj != zenon_Vme) % 0.16/0.70 (zenon_Vle != zenon_Vqf) % 0.16/0.70 (zenon_Vtg != zenon_Vvf) % 0.16/0.70 (r1 zenon_X5 zenon_Vqd) % 0.16/0.70 (zenon_Vdh != zenon_Vbf) % 0.16/0.70 (zenon_Vzf != zenon_Vbf) % 0.16/0.70 (zenon_Vaf != zenon_Vlf) % 0.16/0.70 (zenon_Vvi != zenon_Vjd) % 0.16/0.70 (-. (p1 zenon_Vpc)) % 0.16/0.70 (zenon_Vth != zenon_Vhe) % 0.16/0.70 (zenon_Vpj != zenon_Vpg) % 0.16/0.70 (zenon_Vlj != zenon_Vlc) % 0.16/0.70 (zenon_Vpj != zenon_Vbd) % 0.16/0.70 (zenon_Vlh != zenon_Vlf) % 0.16/0.70 (zenon_Vtg != zenon_Vfd) % 0.16/0.70 (-. (p1 zenon_Vvb)) % 0.16/0.70 (zenon_Vfi != zenon_Vdc) % 0.16/0.70 (zenon_Vvi != zenon_Vxd) % 0.16/0.70 (zenon_Vtj != zenon_Vrb) % 0.16/0.70 (zenon_Vpf != zenon_Vdc) % 0.16/0.70 (zenon_Vek != zenon_Vjb) % 0.16/0.70 (-. (p1 zenon_Vlc)) % 0.16/0.70 (zenon_Vsd != zenon_Vzb) % 0.16/0.70 (zenon_Vri != zenon_Vrb) % 0.16/0.70 (-. (p1 zenon_Vce)) % 0.16/0.70 (zenon_Vsd != zenon_Vvb) % 0.16/0.70 (zenon_Vuf != zenon_Vlf) % 0.16/0.70 (zenon_Vhj != zenon_Vbf) % 0.16/0.70 (r1 zenon_Vzd zenon_Vce) % 0.16/0.70 (zenon_Vdj != zenon_Vpg) % 0.16/0.70 (zenon_Vaf != zenon_Vzb) % 0.16/0.70 (r1 Tau_1 zenon_Vrd) % 0.16/0.70 (zenon_Vpj != zenon_Veh) % 0.16/0.70 (zenon_Vbe != zenon_Vxd) % 0.16/0.70 (zenon_Vxj != zenon_Vrb) % 0.16/0.70 (r1 zenon_Vmj zenon_Vpj) % 0.16/0.70 (zenon_Vlh != zenon_Vug) % 0.16/0.70 (zenon_Vni != zenon_Vfg) % 0.16/0.70 (zenon_Vsd != zenon_Vbb) % 0.16/0.70 (zenon_Vbi != zenon_Vtc) % 0.16/0.70 (r1 zenon_Vkb zenon_Vnb) % 0.16/0.70 (zenon_Vtg != zenon_Vxc) % 0.16/0.70 (zenon_Vbk != zenon_Vzg) % 0.16/0.70 (zenon_Vle != zenon_Vbd) % 0.16/0.70 (zenon_Vni != zenon_Vtd) % 0.16/0.70 (r1 zenon_Vvg zenon_Vah) % 0.16/0.70 (zenon_Vth != zenon_Vme) % 0.16/0.70 (zenon_Vxj != zenon_Vzg) % 0.16/0.70 (zenon_Vff != zenon_Vwe) % 0.16/0.70 (zenon_Vaf != zenon_Vfb) % 0.16/0.70 (-. (p1 zenon_Vfb)) % 0.16/0.70 (zenon_Vqe != zenon_Vbd) % 0.16/0.70 (zenon_Veg != zenon_Vjb) % 0.16/0.70 (zenon_Vxh != zenon_Vqd) % 0.16/0.70 (r1 zenon_Vee zenon_Vhe) % 0.16/0.70 (-. (p1 zenon_Vme)) % 0.16/0.70 (zenon_Vqe != zenon_Vzb) % 0.16/0.70 (zenon_Vzf != zenon_Vbb) % 0.16/0.70 (zenon_Vdj != zenon_Vtc) % 0.16/0.70 (r1 zenon_Vzd zenon_Vae) % 0.16/0.70 (r1 zenon_Vxf zenon_Vyf) % 0.16/0.70 (zenon_Vyg != zenon_Vzg) % 0.16/0.70 (zenon_Vbe != zenon_Vbf) % 0.16/0.70 (zenon_Vsd != zenon_Vbf) % 0.16/0.70 (zenon_Vbi != zenon_Vdc) % 0.16/0.70 (zenon_Vuf != zenon_Vvb) % 0.16/0.70 (zenon_Vzi != zenon_Vkg) % 0.16/0.70 (zenon_Vwd != zenon_Vzb) % 0.16/0.70 (zenon_Vxj != zenon_Vhc) % 0.16/0.70 (zenon_Vdj != zenon_Vfb) % 0.16/0.70 (zenon_Vdh != zenon_Vzg) % 0.16/0.70 (zenon_Vuf != zenon_Vkg) % 0.16/0.70 (zenon_Vdh != zenon_Vvf) % 0.16/0.70 (zenon_Veg != zenon_Vtd) % 0.16/0.70 (zenon_Vtg != zenon_Vtc) % 0.16/0.70 (zenon_Vni != zenon_Vhc) % 0.16/0.70 (zenon_Vtg != zenon_Vvb) % 0.16/0.70 (r1 zenon_Vqc zenon_Vtc) % 0.16/0.70 (zenon_Vri != zenon_Vbf) % 0.16/0.70 (zenon_Vjg != zenon_Vbd) % 0.16/0.70 (zenon_Vth != zenon_Vug) % 0.16/0.70 (r1 zenon_Vsi zenon_Vvi) % 0.16/0.70 (zenon_Vxh != zenon_Vgf) % 0.16/0.70 (zenon_Veg != zenon_Vkg) % 0.16/0.70 (zenon_Vxh != zenon_Vrb) % 0.16/0.70 (zenon_Vff != zenon_Vdc) % 0.16/0.70 (zenon_Vpf != zenon_Vrb) % 0.16/0.70 (zenon_Vxh != zenon_Vtc) % 0.16/0.70 (zenon_Vdj != zenon_Vjb) % 0.16/0.70 (zenon_Vog != zenon_Vxd) % 0.16/0.70 (zenon_Vtg != zenon_Vzg) % 0.16/0.70 (zenon_Vvi != zenon_Vxc) % 0.16/0.70 (zenon_Vle != zenon_Vag) % 0.16/0.70 (zenon_Vhj != zenon_Vfd) % 0.16/0.70 (-. (p1 zenon_Vfg)) % 0.16/0.70 (zenon_Vpf != zenon_Vwe) % 0.16/0.70 (zenon_Vwd != zenon_Vfg) % 0.16/0.70 (zenon_Vvi != zenon_Vce) % 0.16/0.70 (zenon_Vzf != zenon_Vtd) % 0.16/0.70 (zenon_Vwd != zenon_Vfb) % 0.16/0.70 (zenon_Vlj != zenon_Vqd) % 0.16/0.70 (zenon_Vve != zenon_Vvf) % 0.16/0.70 (zenon_Vth != zenon_Vfg) % 0.16/0.70 (zenon_Vji != zenon_Vtc) % 0.16/0.70 (zenon_Vvi != zenon_Vnb) % 0.16/0.70 (zenon_Vzf != zenon_Vnb) % 0.16/0.70 (zenon_Veg != zenon_Vfg) % 0.16/0.70 (zenon_Vkf != zenon_Vce) % 0.16/0.70 (zenon_Vhj != zenon_Vpg) % 0.16/0.70 (zenon_Vqe != zenon_Vug) % 0.16/0.70 (zenon_Vbk != zenon_Vrb) % 0.16/0.70 (zenon_Vfi != zenon_Veh) % 0.16/0.70 (zenon_Vlj != zenon_Vbd) % 0.16/0.70 (zenon_Vri != zenon_Vlf) % 0.16/0.70 (zenon_Vbk != zenon_Vme) % 0.16/0.70 (zenon_Vkf != zenon_Vjb) % 0.16/0.70 (zenon_Vfi != zenon_Vqd) % 0.16/0.70 (zenon_Vff != zenon_Vtd) % 0.16/0.70 (r1 zenon_Vgg zenon_Vlg) % 0.16/0.70 (zenon_Vdj != zenon_Vnd) % 0.16/0.70 (zenon_Vpf != zenon_Vbd) % 0.16/0.70 (zenon_Vkf != zenon_Vvb) % 0.16/0.70 (zenon_Vpj != zenon_Vpc) % 0.16/0.70 (zenon_Vzi != zenon_Vhc) % 0.16/0.70 (zenon_Vyg != zenon_Vzb) % 0.16/0.70 (zenon_Vbe != zenon_Vjb) % 0.16/0.70 (zenon_Vvi != zenon_Vtc) % 0.16/0.70 (zenon_Vaf != zenon_Vdc) % 0.16/0.70 (zenon_Vxh != zenon_Vhe) % 0.16/0.70 (r1 zenon_Vbh zenon_Vch) % 0.16/0.70 (-. (p1 zenon_Vtc)) % 0.16/0.70 (zenon_Vni != zenon_Vag) % 0.16/0.70 (p1 zenon_Vqe) % 0.16/0.70 (zenon_Vxj != zenon_Vlc) % 0.16/0.70 (r1 Tau_0 Tau_2) % 0.16/0.70 (zenon_Vjg != zenon_Vkg) % 0.16/0.70 (zenon_Vtj != zenon_Vxc) % 0.16/0.70 (zenon_Vaf != zenon_Vwe) % 0.16/0.70 (zenon_Vjg != zenon_Vxa) % 0.16/0.70 (zenon_Vzi != zenon_Vpg) % 0.16/0.70 (zenon_Vle != zenon_Vce) % 0.16/0.70 (-. (p2 zenon_Vta)) % 0.16/0.70 (zenon_Vji != zenon_Vwe) % 0.16/0.70 (zenon_Vlh != zenon_Vjd) % 0.16/0.70 (zenon_Vph != zenon_Vtd) % 0.16/0.70 (zenon_Vxj != zenon_Vlf) % 0.16/0.70 (r1 zenon_Vnf zenon_Vof) % 0.16/0.70 (r1 zenon_Vwg zenon_Vzg) % 0.16/0.70 (zenon_Vxj != zenon_Vqf) % 0.16/0.70 (zenon_Vfi != zenon_Vhe) % 0.16/0.70 (zenon_Vog != zenon_Vzb) % 0.16/0.70 (zenon_Veg != zenon_Vme) % 0.16/0.70 (zenon_Vfi != zenon_Vfg) % 0.16/0.70 (zenon_Vaf != zenon_Vfg) % 0.16/0.70 (zenon_Vbe != zenon_Vtd) % 0.16/0.70 (zenon_Vjg != zenon_Vjb) % 0.16/0.70 (zenon_Vsd != zenon_Vag) % 0.16/0.70 (zenon_Vwd != zenon_Vvf) % 0.16/0.70 (zenon_Vsd != zenon_Vjb) % 0.16/0.70 (zenon_Vog != zenon_Vbf) % 0.16/0.70 (zenon_Vdh != zenon_Vfd) % 0.16/0.70 (zenon_Vzf != zenon_Vxa) % 0.16/0.70 (zenon_Vsd != zenon_Vnd) % 0.16/0.70 (zenon_Vph != zenon_Vxd) % 0.16/0.70 (r1 Tau_1 zenon_Vtd) % 0.16/0.70 (r1 zenon_Vrf zenon_Vwf) % 0.16/0.70 (zenon_Vvi != zenon_Vbd) % 0.16/0.70 (zenon_Vek != zenon_Vzg) % 0.16/0.70 (zenon_Vlj != zenon_Vfd) % 0.16/0.70 (zenon_Vqe != zenon_Vxd) % 0.16/0.70 (zenon_Vzi != zenon_Vxa) % 0.16/0.70 (zenon_Vxh != zenon_Vxa) % 0.16/0.70 (zenon_Vkf != zenon_Vqf) % 0.16/0.70 (zenon_Vve != zenon_Vkg) % 0.16/0.70 (zenon_Vve != zenon_Vbb) % 0.16/0.70 (zenon_Vzi != zenon_Vjb) % 0.16/0.70 (zenon_Vri != zenon_Vjb) % 0.16/0.70 (zenon_Vph != zenon_Vgf) % 0.16/0.70 (zenon_Vjg != zenon_Vug) % 0.16/0.70 (zenon_Vyg != zenon_Vbd) % 0.16/0.70 (zenon_Vhj != zenon_Vkg) % 0.16/0.70 (zenon_Vwd != zenon_Veh) % 0.16/0.70 (zenon_Vfi != zenon_Vfd) % 0.16/0.70 (zenon_Vth != zenon_Vlc) % 0.16/0.70 (zenon_Vge != zenon_Vhe) % 0.16/0.70 (zenon_Vzf != zenon_Vce) % 0.16/0.70 (zenon_Vdh != zenon_Veh) % 0.16/0.70 (zenon_Vzi != zenon_Vbb) % 0.16/0.70 (p1 zenon_Vyg) % 0.16/0.70 (zenon_Vhj != zenon_Vnd) % 0.16/0.70 (zenon_Vyg != zenon_Vjb) % 0.16/0.70 (zenon_Vek != zenon_Vnb) % 0.16/0.70 (zenon_Vdh != zenon_Vbd) % 0.16/0.70 (zenon_Vyg != zenon_Vvf) % 0.16/0.70 (zenon_Vth != zenon_Vxd) % 0.16/0.70 (zenon_Vbk != zenon_Vag) % 0.16/0.70 (zenon_Vtg != zenon_Vkg) % 0.16/0.70 (zenon_Vwd != zenon_Vhc) % 0.16/0.70 (zenon_Vlh != zenon_Vgf) % 0.16/0.70 (zenon_Vri != zenon_Vag) % 0.16/0.70 (zenon_Vge != zenon_Vxd) % 0.16/0.70 (zenon_Vwd != zenon_Vkg) % 0.16/0.70 (zenon_Vle != zenon_Vrb) % 0.16/0.70 (p1 zenon_Vji) % 0.16/0.70 (zenon_Vxj != zenon_Vjd) % 0.16/0.70 (zenon_Vpf != zenon_Vnb) % 0.16/0.70 (zenon_Vek != zenon_Vqd) % 0.16/0.70 (zenon_Vaf != zenon_Vre) % 0.16/0.70 (zenon_Vyg != zenon_Vfd) % 0.16/0.70 (zenon_Vri != zenon_Vnb) % 0.16/0.70 (zenon_Vbi != zenon_Vfd) % 0.16/0.70 (-. (p1 zenon_Vjb)) % 0.16/0.70 (zenon_Vve != zenon_Vfd) % 0.16/0.70 (zenon_Vdj != zenon_Vbd) % 0.16/0.70 (p1 zenon_Vdh) % 0.16/0.70 (zenon_Vbi != zenon_Vzg) % 0.16/0.70 (zenon_Vth != zenon_Vgf) % 0.16/0.70 (zenon_Vpf != zenon_Vxd) % 0.16/0.70 (zenon_Vdh != zenon_Vfg) % 0.16/0.70 (zenon_Vfi != zenon_Vzg) % 0.16/0.70 (p1 zenon_Vvi) % 0.16/0.70 (r1 zenon_Vcf zenon_Vdf) % 0.16/0.70 (zenon_Vzi != zenon_Vfd) % 0.16/0.70 (zenon_Vzi != zenon_Vzb) % 0.16/0.70 (zenon_Vdh != zenon_Vzb) % 0.16/0.70 (zenon_Vpf != zenon_Vjd) % 0.16/0.70 (zenon_Vve != zenon_Vbd) % 0.16/0.70 (zenon_Vqe != zenon_Vgf) % 0.16/0.70 (zenon_Vdh != zenon_Vtc) % 0.16/0.70 (zenon_Vri != zenon_Vvf) % 0.16/0.70 (zenon_Vdj != zenon_Vgf) % 0.16/0.70 (zenon_Vuf != zenon_Vjd) % 0.16/0.70 (zenon_Vyg != zenon_Vug) % 0.16/0.70 (zenon_Vph != zenon_Vhc) % 0.16/0.70 (zenon_Vkf != zenon_Vxc) % 0.16/0.70 (zenon_Vji != zenon_Vdc) % 0.16/0.70 (zenon_Vpf != zenon_Vlf) % 0.16/0.70 (zenon_Veg != zenon_Vhc) % 0.16/0.70 (zenon_Vek != zenon_Vme) % 0.16/0.70 (zenon_Veg != zenon_Vbd) % 0.16/0.70 (zenon_Vog != zenon_Vvb) % 0.16/0.70 (zenon_Vfi != zenon_Vnb) % 0.16/0.70 (zenon_Vhj != zenon_Vug) % 0.16/0.70 (zenon_Vaf != zenon_Vce) % 0.16/0.70 (zenon_Vtj != zenon_Vxd) % 0.16/0.70 (zenon_Vtj != zenon_Veh) % 0.16/0.70 (-. (p1 zenon_Vlf)) % 0.16/0.70 (zenon_Vdh != zenon_Vre) % 0.16/0.70 (zenon_Vbk != zenon_Vhc) % 0.16/0.70 (p1 zenon_Vkf) % 0.16/0.70 (zenon_Vuf != zenon_Vnb) % 0.16/0.70 (zenon_Vtg != zenon_Vfb) % 0.16/0.70 (zenon_Vlh != zenon_Vme) % 0.16/0.70 (zenon_Vtj != zenon_Vjb) % 0.16/0.70 (r1 zenon_Vmh zenon_Vph) % 0.16/0.70 (zenon_Vdj != zenon_Vxd) % 0.16/0.70 (zenon_Vaf != zenon_Vxa) % 0.16/0.70 (zenon_Vxj != zenon_Vug) % 0.16/0.70 (zenon_Vek != zenon_Vtc) % 0.16/0.70 (zenon_Veg != zenon_Vxc) % 0.16/0.70 (zenon_Vvi != zenon_Vvf) % 0.16/0.70 (zenon_Vhj != zenon_Vwe) % 0.16/0.70 (zenon_Vtg != zenon_Vzb) % 0.16/0.70 (zenon_Vkf != zenon_Vzb) % 0.16/0.70 (zenon_Vph != zenon_Vfb) % 0.16/0.70 (zenon_Vxh != zenon_Vbb) % 0.16/0.70 (zenon_Vbe != zenon_Vbb) % 0.16/0.70 (zenon_Vtg != zenon_Vre) % 0.16/0.70 (p1 zenon_Vve) % 0.16/0.70 (zenon_Vni != zenon_Vpg) % 0.16/0.70 (zenon_Vzi != zenon_Vvf) % 0.16/0.70 (zenon_Vsd != zenon_Vpc) % 0.16/0.70 (zenon_Vaf != zenon_Vug) % 0.16/0.70 (zenon_Vlj != zenon_Vtd) % 0.16/0.70 (zenon_Vlj != zenon_Vbb) % 0.16/0.70 (zenon_Vvi != zenon_Vxa) % 0.16/0.70 (zenon_Vfi != zenon_Vxa) % 0.16/0.70 (zenon_Vyg != zenon_Vfb) % 0.16/0.70 (zenon_Vkf != zenon_Veh) % 0.16/0.70 (zenon_Vji != zenon_Vug) % 0.16/0.70 (zenon_Vbi != zenon_Vlf) % 0.16/0.70 (zenon_Vwd != zenon_Vag) % 0.16/0.70 (zenon_Veg != zenon_Vqf) % 0.16/0.70 (zenon_Vge != zenon_Vxa) % 0.16/0.70 (zenon_Vni != zenon_Vqd) % 0.16/0.70 (zenon_Vog != zenon_Vce) % 0.16/0.70 (zenon_Vzf != zenon_Vre) % 0.16/0.70 (zenon_Vxj != zenon_Vkg) % 0.16/0.70 (zenon_Vle != zenon_Vjb) % 0.16/0.70 (zenon_Vyg != zenon_Vag) % 0.16/0.70 (zenon_Vfi != zenon_Vjd) % 0.16/0.70 (zenon_Veg != zenon_Vug) % 0.16/0.70 (r1 zenon_Vvg zenon_Vwg) % 0.16/0.70 (zenon_Vaf != zenon_Vtc) % 0.16/0.70 (zenon_Vjg != zenon_Vpc) % 0.16/0.70 (zenon_Vuf != zenon_Vdc) % 0.16/0.70 (r1 zenon_Vya zenon_Vbb) % 0.16/0.70 (zenon_Vji != zenon_Vfb) % 0.16/0.70 (zenon_Vhj != zenon_Vvf) % 0.16/0.70 (zenon_Vpf != zenon_Vpg) % 0.16/0.70 (zenon_Vpj != zenon_Vag) % 0.16/0.70 (-. (p1 zenon_Vbb)) % 0.16/0.70 (zenon_Vth != zenon_Vbd) % 0.16/0.70 (zenon_Vbk != zenon_Vxc) % 0.16/0.70 (zenon_Vxh != zenon_Vjb) % 0.16/0.70 (zenon_Vdh != zenon_Vwe) % 0.16/0.70 (zenon_Vvi != zenon_Vfb) % 0.16/0.70 (zenon_Vph != zenon_Vvb) % 0.16/0.70 (zenon_Vge != zenon_Vvf) % 0.16/0.70 (r1 zenon_Vie zenon_Vje) % 0.16/0.70 (zenon_Vri != zenon_Vre) % 0.16/0.70 (zenon_Vdj != zenon_Vfg) % 0.16/0.70 (zenon_Vwd != zenon_Vlc) % 0.16/0.70 (p1 zenon_Vth) % 0.16/0.70 (zenon_Vvi != zenon_Vjb) % 0.16/0.70 (zenon_Vjg != zenon_Vrb) % 0.16/0.70 (p1 zenon_Vpf) % 0.16/0.70 (zenon_Vve != zenon_Vxa) % 0.16/0.70 (zenon_Vlj != zenon_Vrb) % 0.16/0.70 (zenon_Vxj != zenon_Vtc) % 0.16/0.70 (zenon_Vni != zenon_Vnb) % 0.16/0.70 (-. (p1 zenon_Vnb)) % 0.16/0.70 (zenon_Vwd != zenon_Vpg) % 0.16/0.70 (zenon_Vzi != zenon_Vug) % 0.16/0.70 (zenon_Vuf != zenon_Vlc) % 0.16/0.70 (zenon_Vyg != zenon_Vwe) % 0.16/0.70 (zenon_Vwd != zenon_Vnb) % 0.16/0.70 (zenon_Vtj != zenon_Vpc) % 0.16/0.70 (zenon_Vbk != zenon_Vfb) % 0.16/0.70 (zenon_Vuf != zenon_Vhc) % 0.16/0.70 (zenon_Vsd != zenon_Vxa) % 0.16/0.70 (zenon_Vxh != zenon_Vxc) % 0.16/0.70 (zenon_Vff != zenon_Vlc) % 0.16/0.70 (zenon_Vpf != zenon_Vfb) % 0.16/0.70 (zenon_Vfi != zenon_Vbf) % 0.16/0.70 (zenon_Vzi != zenon_Vlc) % 0.16/0.70 (zenon_Vth != zenon_Vhc) % 0.16/0.70 (zenon_Vth != zenon_Vkg) % 0.16/0.70 (zenon_Vff != zenon_Vhc) % 0.16/0.70 (zenon_Vdj != zenon_Vzb) % 0.16/0.70 (zenon_Vge != zenon_Vqd) % 0.16/0.70 (zenon_Vuf != zenon_Vbd) % 0.16/0.70 (zenon_Vle != zenon_Vfb) % 0.16/0.70 (zenon_Vbi != zenon_Vhc) % 0.16/0.70 (zenon_Vek != zenon_Vfg) % 0.16/0.70 (zenon_Vsd != zenon_Vhe) % 0.16/0.70 (zenon_Vff != zenon_Vbf) % 0.16/0.70 (zenon_Vhj != zenon_Vtc) % 0.16/0.70 (zenon_Vji != zenon_Vgf) % 0.16/0.70 (zenon_Vni != zenon_Vxa) % 0.16/0.70 (zenon_Vwd != zenon_Vxc) % 0.16/0.70 (zenon_Vbi != zenon_Vxc) % 0.16/0.70 (zenon_Vek != zenon_Vug) % 0.16/0.70 (zenon_Vog != zenon_Vhe) % 0.16/0.70 (zenon_Vni != zenon_Vkg) % 0.16/0.70 (zenon_Vbk != zenon_Vwe) % 0.16/0.70 (zenon_Vni != zenon_Vtc) % 0.16/0.70 (zenon_Vge != zenon_Vzb) % 0.16/0.70 (zenon_Vle != zenon_Vnb) % 0.16/0.70 (zenon_Vle != zenon_Vqd) % 0.16/0.70 (zenon_Vxj != zenon_Vwe) % 0.16/0.70 (zenon_Vjg != zenon_Vce) % 0.16/0.70 (zenon_Vxh != zenon_Vzg) % 0.16/0.70 (zenon_Vsd != zenon_Vhc) % 0.16/0.70 (zenon_Vtg != zenon_Vme) % 0.16/0.70 (zenon_Vog != zenon_Vkg) % 0.16/0.70 (zenon_Vxj != zenon_Vre) % 0.16/0.70 (-. (p1 zenon_Vpg)) % 0.16/0.70 (r1 zenon_Vhg zenon_Vig) % 0.16/0.70 (zenon_Vdj != zenon_Vce) % 0.16/0.70 (-. (p1 zenon_Vzg)) % 0.16/0.70 (zenon_Vtg != zenon_Vhc) % 0.16/0.70 (zenon_Vwd != zenon_Vlf) % 0.16/0.70 (zenon_Vqe != zenon_Vtd) % 0.16/0.70 (zenon_Vbe != zenon_Vag) % 0.16/0.70 (zenon_Vph != zenon_Vqd) % 0.16/0.70 (zenon_Vbk != zenon_Vxd) % 0.16/0.70 (zenon_Vvi != zenon_Vnd) % 0.16/0.70 (zenon_Vji != zenon_Vqf) % 0.16/0.70 (zenon_Vhj != zenon_Vzb) % 0.16/0.70 (zenon_Vpj != zenon_Vrb) % 0.16/0.70 (zenon_Vlj != zenon_Vnb) % 0.16/0.70 (p1 zenon_Vni) % 0.16/0.70 (zenon_Vpj != zenon_Vgf) % 0.16/0.70 (zenon_Vhj != zenon_Vag) % 0.16/0.70 (zenon_Vlj != zenon_Vfb) % 0.16/0.70 (zenon_Vzi != zenon_Vfg) % 0.16/0.70 (zenon_Vbk != zenon_Vfg) % 0.16/0.70 (zenon_Vtj != zenon_Vbd) % 0.16/0.70 (zenon_Vaf != zenon_Vme) % 0.16/0.70 (zenon_Vfi != zenon_Vgf) % 0.16/0.70 (zenon_Vkf != zenon_Vnd) % 0.16/0.70 (zenon_Vlh != zenon_Vzg) % 0.16/0.70 (zenon_Vpj != zenon_Vvf) % 0.16/0.70 (zenon_Vek != zenon_Veh) % 0.16/0.70 (zenon_Vph != zenon_Vbf) % 0.16/0.70 (zenon_Vph != zenon_Vkg) % 0.16/0.70 (zenon_Vzf != zenon_Vrb) % 0.16/0.70 (r1 zenon_Vje zenon_Vme) % 0.16/0.70 (zenon_Vle != zenon_Vwe) % 0.16/0.70 (p1 zenon_Vsd) % 0.16/0.70 (zenon_Vaf != zenon_Vbf) % 0.16/0.70 (zenon_Vwd != zenon_Vjd) % 0.16/0.70 (zenon_Vff != zenon_Vjd) % 0.16/0.70 (zenon_Vbk != zenon_Vzb) % 0.16/0.70 (p1 zenon_Vtg) % 0.16/0.70 (zenon_Vge != zenon_Vzg) % 0.16/0.70 (zenon_Vvi != zenon_Vag) % 0.16/0.70 (zenon_Vwd != zenon_Vdc) % 0.16/0.70 (zenon_Vkf != zenon_Vtc) % 0.16/0.70 (zenon_Vqe != zenon_Vlc) % 0.16/0.70 (zenon_Vff != zenon_Vxa) % 0.16/0.70 (zenon_Vve != zenon_Vbf) % 0.16/0.70 (zenon_Vtg != zenon_Vhe) % 0.16/0.70 (zenon_Vzf != zenon_Vwe) % 0.16/0.70 (zenon_Vkf != zenon_Vpc) % 0.16/0.70 (zenon_Vlh != zenon_Vqd) % 0.16/0.70 (zenon_Vff != zenon_Vme) % 0.16/0.70 (zenon_Vek != zenon_Vjd) % 0.16/0.70 (zenon_Vxh != zenon_Vkg) % 0.16/0.70 (zenon_Veg != zenon_Vbb) % 0.16/0.70 (zenon_Vpf != zenon_Vxa) % 0.16/0.70 (zenon_Vkf != zenon_Vlc) % 0.16/0.70 (zenon_Vle != zenon_Vzb) % 0.16/0.70 (zenon_Vbk != zenon_Vxa) % 0.16/0.70 (zenon_Vvi != zenon_Vqd) % 0.16/0.70 (zenon_Vog != zenon_Vbd) % 0.16/0.70 (zenon_Vzi != zenon_Vtc) % 0.16/0.70 (zenon_Vbk != zenon_Vvf) % 0.16/0.70 (zenon_Vff != zenon_Vzb) % 0.16/0.70 (p1 zenon_Vzi) % 0.16/0.70 (zenon_Vge != zenon_Vgf) % 0.16/0.70 (zenon_Vuf != zenon_Vrb) % 0.16/0.70 (zenon_Vsd != zenon_Vfb) % 0.16/0.70 (r1 zenon_Vyh zenon_Vbi) % 0.16/0.70 (zenon_Vwd != zenon_Vhe) % 0.16/0.70 (zenon_Vkf != zenon_Vlf) % 0.16/0.70 (zenon_Vff != zenon_Vpg) % 0.16/0.70 (zenon_Vpj != zenon_Vre) % 0.16/0.70 (zenon_Vog != zenon_Vjd) % 0.16/0.70 (-. (p1 zenon_Vxd)) % 0.16/0.70 (zenon_Vtg != zenon_Vfg) % 0.16/0.70 (zenon_Vbe != zenon_Vug) % 0.16/0.70 (zenon_Vpj != zenon_Vfb) % 0.16/0.70 (zenon_Vuf != zenon_Vvf) % 0.16/0.70 (r1 zenon_Vwb zenon_Vzb) % 0.16/0.70 (zenon_Vsd != zenon_Vrb) % 0.16/0.70 (zenon_Vth != zenon_Vfb) % 0.16/0.70 (zenon_Vbi != zenon_Vvf) % 0.16/0.70 (zenon_Vni != zenon_Vfb) % 0.16/0.70 (p1 zenon_Vuf) % 0.16/0.70 (zenon_Vlj != zenon_Vpg) % 0.16/0.70 (zenon_Vri != zenon_Vhe) % 0.16/0.70 (zenon_Vle != zenon_Vlf) % 0.16/0.70 (zenon_Vog != zenon_Vxc) % 0.16/0.70 (zenon_Vkf != zenon_Vbb) % 0.16/0.70 (zenon_Vtj != zenon_Vtd) % 0.16/0.70 (zenon_Vxh != zenon_Veh) % 0.16/0.70 (zenon_Vbk != zenon_Vjd) % 0.16/0.70 (r1 zenon_Vxf zenon_Vag) % 0.16/0.70 (zenon_Vpf != zenon_Veh) % 0.16/0.70 (zenon_Vtj != zenon_Vce) % 0.16/0.70 (zenon_Vlh != zenon_Vqf) % 0.16/0.70 (r1 zenon_Vde zenon_Vie) % 0.16/0.70 (zenon_Vni != zenon_Vfd) % 0.16/0.70 (zenon_Vbi != zenon_Vkg) % 0.16/0.70 (zenon_Vuf != zenon_Vnd) % 0.16/0.70 (zenon_Vzf != zenon_Vag) % 0.16/0.70 (zenon_Vpj != zenon_Vzb) % 0.16/0.70 (zenon_Vwd != zenon_Vqf) % 0.16/0.70 (zenon_Vvi != zenon_Vvb) % 0.16/0.70 (zenon_Vbi != zenon_Vjb) % 0.16/0.70 (zenon_Vge != zenon_Vhc) % 0.16/0.70 (zenon_Vxj != zenon_Vjb) % 0.16/0.70 (zenon_Vzf != zenon_Veh) % 0.16/0.70 (zenon_Vyg != zenon_Vxc) % 0.16/0.70 (-. (p1 zenon_Vvf)) % 0.16/0.70 (r1 zenon_Vua zenon_Vxa) % 0.16/0.70 (zenon_Vhj != zenon_Vxc) % 0.16/0.70 (zenon_Vwd != zenon_Vtc) % 0.16/0.70 (zenon_Vtj != zenon_Vhe) % 0.16/0.70 (zenon_Vqe != zenon_Vce) % 0.16/0.70 (zenon_Vni != zenon_Vvb) % 0.16/0.70 (zenon_Vuf != zenon_Vzg) % 0.16/0.70 (p1 zenon_Vle) % 0.16/0.70 (zenon_Vxh != zenon_Vbd) % 0.16/0.70 (zenon_Vji != zenon_Vjb) % 0.16/0.70 (zenon_Vjg != zenon_Vfg) % 0.16/0.70 (zenon_Vpj != zenon_Vxd) % 0.16/0.70 (zenon_Vlj != zenon_Vxa) % 0.16/0.70 (zenon_Vtj != zenon_Vug) % 0.16/0.70 (zenon_Vdj != zenon_Vrb) % 0.16/0.70 (zenon_Vji != zenon_Vbb) % 0.16/0.70 (zenon_Vbi != zenon_Vgf) % 0.16/0.70 (zenon_Vsd != zenon_Vgf) % 0.16/0.70 (-. (p1 zenon_Vzb)) % 0.16/0.70 (r1 zenon_Vci zenon_Vfi) % 0.16/0.70 (-. (p1 zenon_Vxc)) % 0.16/0.70 (zenon_Vdh != zenon_Vqf) % 0.16/0.70 (zenon_Vuf != zenon_Vpc) % 0.16/0.70 (zenon_Vxj != zenon_Vxa) % 0.16/0.70 (zenon_Vyg != zenon_Vlc) % 0.16/0.70 (zenon_Vzf != zenon_Vdc) % 0.16/0.70 (zenon_Vyg != zenon_Vnd) % 0.16/0.70 (zenon_Vpf != zenon_Vag) % 0.16/0.70 (zenon_Vdj != zenon_Vdc) % 0.16/0.70 (zenon_Vve != zenon_Vug) % 0.16/0.70 (zenon_Vph != zenon_Vpg) % 0.16/0.70 (zenon_Vdj != zenon_Vqf) % 0.16/0.70 (-. (p1 zenon_Vjd)) % 0.16/0.70 (zenon_Vve != zenon_Vjb) % 0.16/0.70 (zenon_Vaf != zenon_Vhc) % 0.16/0.70 (zenon_Vph != zenon_Vag) % 0.16/0.70 (zenon_Vsd != zenon_Vdc) % 0.16/0.70 (r1 zenon_Vsb zenon_Vvb) % 0.16/0.70 (zenon_Vri != zenon_Vce) % 0.16/0.70 (zenon_Vog != zenon_Vhc) % 0.16/0.70 (zenon_Vvi != zenon_Vzg) % 0.16/0.70 (zenon_Vbk != zenon_Veh) % 0.16/0.70 (zenon_Vyg != zenon_Vvb) % 0.16/0.70 (zenon_Vji != zenon_Vxd) % 0.16/0.70 (zenon_Vpj != zenon_Vce) % 0.16/0.70 (zenon_Vpf != zenon_Vvb) % 0.16/0.70 (zenon_Vek != zenon_Vhe) % 0.16/0.70 (zenon_Vsd != zenon_Vwe) % 0.16/0.70 (zenon_Vdh != zenon_Vpg) % 0.16/0.70 (zenon_Vri != zenon_Veh) % 0.16/0.70 (p1 zenon_Vhj) % 0.16/0.70 (zenon_Vdh != zenon_Vrb) % 0.16/0.70 (r1 Tau_2 zenon_Vud) % 0.16/0.70 (r1 Tau_2 zenon_Vyd) % 0.16/0.70 (zenon_Vvi != zenon_Vfd) % 0.16/0.70 (zenon_Vzf != zenon_Vpg) % 0.16/0.70 (zenon_Vbk != zenon_Vtc) % 0.16/0.70 (zenon_Vji != zenon_Vxa) % 0.16/0.70 (zenon_Vth != zenon_Vqf) % 0.16/0.70 (zenon_Vph != zenon_Vjb) % 0.16/0.70 (zenon_Vzi != zenon_Vxd) % 0.16/0.70 (zenon_Vxh != zenon_Vag) % 0.16/0.70 (zenon_Vlj != zenon_Vdc) % 0.16/0.70 (r1 zenon_Vte zenon_Vue) % 0.16/0.70 (zenon_Vdh != zenon_Vxd) % 0.16/0.70 (zenon_Vlj != zenon_Vlf) % 0.16/0.70 (zenon_Vuf != zenon_Vug) % 0.16/0.70 (zenon_Vph != zenon_Vdc) % 0.16/0.70 (zenon_Vge != zenon_Vfd) % 0.16/0.70 (zenon_Vyg != zenon_Vpg) % 0.16/0.70 (zenon_Vdh != zenon_Vug) % 0.16/0.70 (zenon_Vpf != zenon_Vpc) % 0.16/0.70 (p1 zenon_Vaf) % 0.16/0.70 (zenon_Vve != zenon_Vce) % 0.16/0.70 (zenon_Vek != zenon_Vwe) % 0.16/0.70 (zenon_Vni != zenon_Vbf) % 0.16/0.70 (-. (p2 zenon_Vpa)) % 0.16/0.70 (r1 zenon_Vnf zenon_Vqf) % 0.16/0.70 (zenon_Vog != zenon_Vug) % 0.16/0.70 (zenon_Vpj != zenon_Vxc) % 0.16/0.70 (p1 zenon_Vtj) % 0.16/0.70 (zenon_Vbe != zenon_Vqd) % 0.16/0.70 (zenon_Vek != zenon_Vlf) % 0.16/0.70 (zenon_Vxh != zenon_Vce) % 0.16/0.70 (zenon_Vxj != zenon_Vnd) % 0.16/0.70 (zenon_Vpj != zenon_Vbf) % 0.16/0.70 (zenon_Vth != zenon_Vqd) % 0.16/0.70 (zenon_Vtj != zenon_Vjd) % 0.16/0.70 (r1 Tau_0 Tau_1) % 0.16/0.70 (zenon_Vri != zenon_Vkg) % 0.16/0.70 (zenon_Vlj != zenon_Vbf) % 0.16/0.70 (zenon_Vzf != zenon_Vfd) % 0.16/0.70 (zenon_Vtj != zenon_Vgf) % 0.16/0.70 (zenon_Vog != zenon_Vtd) % 0.16/0.70 (zenon_Vpf != zenon_Vzb) % 0.16/0.70 (zenon_Vzi != zenon_Vqf) % 0.16/0.70 (zenon_Vle != zenon_Vfd) % 0.16/0.70 (zenon_Vsd != zenon_Vtc) % 0.16/0.70 (zenon_Vth != zenon_Vnb) % 0.16/0.70 (zenon_Vvi != zenon_Vbb) % 0.16/0.70 (zenon_Veg != zenon_Vlc) % 0.16/0.70 (zenon_Vyg != zenon_Vrb) % 0.16/0.70 (zenon_Vsd != zenon_Vug) % 0.16/0.70 (zenon_Vxh != zenon_Vnd) % 0.16/0.70 (zenon_Vuf != zenon_Vce) % 0.16/0.70 (r1 zenon_Vsf zenon_Vtf) % 0.16/0.70 (zenon_Vpf != zenon_Vtd) % 0.16/0.70 (zenon_Vog != zenon_Vqd) % 0.16/0.70 (zenon_Vff != zenon_Vre) % 0.16/0.70 (zenon_Vve != zenon_Veh) % 0.16/0.70 (zenon_Vge != zenon_Vtc) % 0.16/0.70 (zenon_Veg != zenon_Vlf) % 0.16/0.70 (zenon_Vle != zenon_Vbf) % 0.16/0.70 (-. (p4 zenon_X3)) % 0.16/0.70 (zenon_Vkf != zenon_Vpg) % 0.16/0.70 (zenon_Vxj != zenon_Vpc) % 0.16/0.70 (zenon_Vqe != zenon_Vbb) % 0.16/0.70 (zenon_Vni != zenon_Vre) % 0.16/0.70 (zenon_Vyg != zenon_Vxa) % 0.16/0.70 (zenon_Vfi != zenon_Vnd) % 0.16/0.70 (r1 zenon_Vqg zenon_Vrg) % 0.16/0.70 (zenon_Vve != zenon_Vvb) % 0.16/0.70 (zenon_Vaf != zenon_Vbd) % 0.16/0.70 (zenon_Vve != zenon_Vtc) % 0.16/0.70 (zenon_Vzi != zenon_Vfb) % 0.16/0.70 (zenon_Vdj != zenon_Vug) % 0.16/0.70 (zenon_Vdj != zenon_Vvf) % 0.16/0.70 (zenon_Vff != zenon_Vjb) % 0.16/0.70 (zenon_Vpf != zenon_Vhc) % 0.16/0.70 (zenon_Vlh != zenon_Vxa) % 0.16/0.70 (zenon_Vbk != zenon_Vfd) % 0.16/0.70 (zenon_Vxj != zenon_Vgf) % 0.16/0.70 (zenon_Vdh != zenon_Vxc) % 0.16/0.70 (zenon_Vve != zenon_Vxd) % 0.16/0.70 (zenon_Vsd != zenon_Vbd) % 0.16/0.70 (zenon_Vxh != zenon_Vnb) % 0.16/0.70 (zenon_Vvi != zenon_Vzb) % 0.16/0.70 (zenon_Vff != zenon_Vvf) % 0.16/0.70 (zenon_Vni != zenon_Vdc) % 0.16/0.70 (r1 zenon_Vrg zenon_Vug) % 0.16/0.70 (zenon_Vyg != zenon_Veh) % 0.16/0.70 (-. (p1 zenon_Vhc)) % 0.16/0.70 (zenon_Vge != zenon_Vxc) % 0.16/0.70 (r1 zenon_Vif zenon_Vlf) % 0.16/0.70 (zenon_Vdj != zenon_Vtd) % 0.16/0.70 (zenon_Vth != zenon_Vdc) % 0.16/0.70 (zenon_Vaf != zenon_Vfd) % 0.16/0.70 (zenon_Vvi != zenon_Vrb) % 0.16/0.70 (zenon_Vpj != zenon_Vlf) % 0.16/0.70 (zenon_Vzi != zenon_Vme) % 0.16/0.70 (zenon_Vph != zenon_Vfg) % 0.16/0.70 (p1 zenon_Vjg) % 0.16/0.70 (zenon_Vuf != zenon_Vqf) % 0.16/0.70 (zenon_Vge != zenon_Vag) % 0.16/0.70 (zenon_Vtj != zenon_Vfd) % 0.16/0.70 (zenon_Vpj != zenon_Vqd) % 0.16/0.70 (zenon_Vdj != zenon_Vpc) % 0.16/0.70 (r1 zenon_Vqj zenon_Vtj) % 0.16/0.70 (zenon_Vhj != zenon_Vlf) % 0.16/0.70 (zenon_Vog != zenon_Vtc) % 0.16/0.70 (zenon_Vle != zenon_Vtd) % 0.16/0.70 (p1 zenon_Vlj) % 0.16/0.70 (-. (p1 zenon_Vqf)) % 0.16/0.70 (zenon_Vtj != zenon_Vag) % 0.16/0.70 (zenon_Vji != zenon_Vjd) % 0.16/0.70 (zenon_Vxh != zenon_Vfd) % 0.16/0.70 (zenon_Vlj != zenon_Vtc) % 0.16/0.70 (zenon_Vbi != zenon_Vxa) % 0.16/0.70 (zenon_Vni != zenon_Vme) % 0.16/0.70 (zenon_Vbe != zenon_Vhe) % 0.16/0.70 (zenon_Vuf != zenon_Vxd) % 0.16/0.70 (zenon_Vaf != zenon_Vag) % 0.16/0.70 (zenon_Vzf != zenon_Vlc) % 0.16/0.70 (zenon_Vve != zenon_Vrb) % 0.16/0.70 (zenon_Vbe != zenon_Vme) % 0.16/0.70 (zenon_Vbi != zenon_Vme) % 0.16/0.70 (zenon_Vbe != zenon_Vvb) % 0.16/0.70 (zenon_Vjg != zenon_Vtd) % 0.16/0.70 (zenon_Vhj != zenon_Vqd) % 0.16/0.70 (zenon_Vhj != zenon_Vbb) % 0.16/0.70 (zenon_Vjg != zenon_Veh) % 0.16/0.70 (-. (p1 zenon_Vnd)) % 0.16/0.70 (zenon_Vfi != zenon_Vag) % 0.16/0.70 (zenon_Vlh != zenon_Vnb) % 0.16/0.70 (zenon_Vxj != zenon_Vxd) % 0.16/0.70 (zenon_Vek != zenon_Vdc) % 0.16/0.70 (zenon_Vth != zenon_Vwe) % 0.16/0.70 (zenon_Vph != zenon_Veh) % 0.16/0.70 (zenon_Vxh != zenon_Vzb) % 0.16/0.70 (zenon_Vbi != zenon_Vnb) % 0.16/0.70 (zenon_Vjg != zenon_Vxd) % 0.16/0.70 (zenon_Vsd != zenon_Vme) % 0.16/0.70 (zenon_Vni != zenon_Vbd) % 0.16/0.70 (zenon_Vdh != zenon_Vnb) % 0.16/0.70 (zenon_Vjg != zenon_Vxc) % 0.16/0.70 (zenon_Vtj != zenon_Vpg) % 0.16/0.70 (zenon_Vji != zenon_Vzb) % 0.16/0.70 (zenon_Vfi != zenon_Vug) % 0.16/0.70 (zenon_Vbe != zenon_Vjd) % 0.16/0.70 (zenon_Vdh != zenon_Vqd) % 0.16/0.70 (zenon_Vhj != zenon_Vfg) % 0.16/0.70 (-. (p1 zenon_Vfd)) % 0.16/0.70 (zenon_Vdh != zenon_Vhc) % 0.16/0.70 (zenon_Vji != zenon_Vnb) % 0.16/0.70 (zenon_Vge != zenon_Veh) % 0.16/0.70 (r1 zenon_Vee zenon_Vfe) % 0.16/0.70 (zenon_Vhj != zenon_Vnb) % 0.16/0.70 (-. (p1 zenon_Vdc)) % 0.16/0.70 (zenon_Vle != zenon_Vjd) % 0.16/0.70 (zenon_Vle != zenon_Vlc) % 0.16/0.70 (zenon_Vlh != zenon_Vre) % 0.16/0.70 (zenon_Vlj != zenon_Vfg) % 0.16/0.70 (zenon_Vlh != zenon_Vdc) % 0.16/0.70 (zenon_Vtj != zenon_Vfb) % 0.16/0.70 (zenon_Vxh != zenon_Vfg) % 0.16/0.70 (zenon_Vvi != zenon_Vpg) % 0.16/0.70 (zenon_Vjg != zenon_Vwe) % 0.16/0.70 (zenon_Vdj != zenon_Vlc) % 0.16/0.70 (zenon_Vlh != zenon_Vfg) % 0.16/0.70 (zenon_Vzf != zenon_Vbd) % 0.16/0.70 (zenon_Vni != zenon_Veh) % 0.16/0.70 (zenon_Vsd != zenon_Vzg) % 0.16/0.70 (zenon_Vsd != zenon_Vxd) % 0.16/0.70 (zenon_Vzf != zenon_Vjd) % 0.16/0.70 (zenon_Veg != zenon_Vfb) % 0.16/0.70 (zenon_Vyg != zenon_Vqf) % 0.16/0.70 (zenon_Vge != zenon_Vce) % 0.16/0.70 (zenon_Veg != zenon_Vqd) % 0.16/0.70 (zenon_Vyg != zenon_Vnb) % 0.16/0.70 (r1 zenon_Vud zenon_Vvd) % 0.16/0.70 (zenon_Vve != zenon_Vnb) % 0.16/0.70 (zenon_Vle != zenon_Vdc) % 0.16/0.70 (r1 zenon_Vaj zenon_Vdj) % 0.16/0.70 (zenon_Vzi != zenon_Vnb) % 0.16/0.70 (zenon_Vph != zenon_Vug) % 0.16/0.70 (zenon_Vvi != zenon_Vhe) % 0.16/0.70 (zenon_Vge != zenon_Vqf) % 0.16/0.70 (zenon_Vph != zenon_Vme) % 0.16/0.70 (zenon_Vsd != zenon_Vqf) % 0.16/0.70 (zenon_Vtj != zenon_Vbf) % 0.16/0.70 (zenon_Vtg != zenon_Vbb) % 0.16/0.70 (zenon_Vth != zenon_Vnd) % 0.16/0.70 (zenon_Vqe != zenon_Vjb) % 0.16/0.70 (zenon_Vlh != zenon_Vtd) % 0.16/0.70 (zenon_Vbe != zenon_Vxa) % 0.16/0.70 (zenon_Vge != zenon_Vwe) % 0.16/0.70 (zenon_Vlj != zenon_Vjd) % 0.16/0.70 (zenon_Vvi != zenon_Vlc) % 0.16/0.70 (zenon_Vqe != zenon_Vrb) % 0.16/0.70 (zenon_Veg != zenon_Vnb) % 0.16/0.70 (zenon_Vpj != zenon_Vug) % 0.16/0.70 (zenon_Vjg != zenon_Vpg) % 0.16/0.70 (zenon_Vbk != zenon_Vtd) % 0.16/0.70 (zenon_Vle != zenon_Vpg) % 0.16/0.70 (zenon_Vog != zenon_Vme) % 0.16/0.70 (zenon_Vvi != zenon_Vpc) % 0.16/0.70 (zenon_Vff != zenon_Vag) % 0.16/0.70 (zenon_Vog != zenon_Vbb) % 0.16/0.70 (zenon_Vek != zenon_Vpg) % 0.16/0.70 (zenon_Vdj != zenon_Veh) % 0.16/0.70 (zenon_Vdj != zenon_Vag) % 0.16/0.70 (zenon_Vqe != zenon_Vdc) % 0.16/0.70 (zenon_Vri != zenon_Vfd) % 0.16/0.70 (zenon_Vsd != zenon_Veh) % 0.16/0.70 (zenon_Vlj != zenon_Vqf) % 0.16/0.70 (zenon_Vbe != zenon_Vfd) % 0.16/0.70 (zenon_Vlh != zenon_Vwe) % 0.16/0.70 (r1 zenon_Vgh zenon_Vhh) % 0.16/0.70 (zenon_Vxj != zenon_Vbb) % 0.16/0.70 (zenon_Vji != zenon_Vfd) % 0.16/0.70 (zenon_Vlh != zenon_Vtc) % 0.16/0.70 (zenon_Vph != zenon_Vjd) % 0.16/0.70 (zenon_Vzi != zenon_Vce) % 0.16/0.70 (zenon_Vtg != zenon_Vxa) % 0.16/0.70 (-. (p1 zenon_Vtd)) % 0.16/0.70 (zenon_Veg != zenon_Vnd) % 0.16/0.70 (zenon_Vlh != zenon_Vag) % 0.16/0.70 (zenon_Vtj != zenon_Vqd) % 0.16/0.70 (zenon_Vbi != zenon_Vpg) % 0.16/0.70 (zenon_Vzi != zenon_Veh) % 0.16/0.70 (r1 zenon_Vcb zenon_Vfb) % 0.16/0.70 (zenon_Vtj != zenon_Vnd) % 0.16/0.70 (zenon_Vbi != zenon_Veh) % 0.16/0.70 (zenon_Vtj != zenon_Vqf) % 0.16/0.70 (zenon_Vyg != zenon_Vdc) % 0.16/0.70 (zenon_Vpf != zenon_Vfd) % 0.16/0.70 (zenon_Vji != zenon_Vag) % 0.16/0.70 (zenon_Vyg != zenon_Vbb) % 0.16/0.70 (p1 zenon_Vph) % 0.16/0.70 (zenon_Vjg != zenon_Vvf) % 0.16/0.70 (zenon_Vge != zenon_Vjd) % 0.16/0.70 (zenon_Vri != zenon_Vwe) % 0.16/0.70 (zenon_Vve != zenon_Vme) % 0.16/0.70 (zenon_Vek != zenon_Vbd) % 0.16/0.70 (zenon_Vji != zenon_Vlf) % 0.16/0.70 (zenon_Vlj != zenon_Vre) % 0.16/0.70 (zenon_Vle != zenon_Vnd) % 0.16/0.70 (zenon_Vyg != zenon_Vkg) % 0.16/0.70 (zenon_Vxh != zenon_Vlf) % 0.16/0.70 (zenon_Vqe != zenon_Vtc) % 0.16/0.70 (zenon_Vfi != zenon_Vjb) % 0.16/0.70 (zenon_Vbi != zenon_Vhe) % 0.16/0.70 (zenon_Vdj != zenon_Vlf) % 0.16/0.70 (zenon_Vzi != zenon_Vbd) % 0.16/0.70 (r1 zenon_Vlg zenon_Vqg) % 0.16/0.70 (zenon_Vbi != zenon_Vag) % 0.16/0.70 (zenon_Vxj != zenon_Vfb) % 0.16/0.70 (zenon_Vge != zenon_Vnb) % 0.16/0.70 (zenon_Vzi != zenon_Vdc) % 0.16/0.70 (zenon_Vxj != zenon_Vme) % 0.16/0.70 (r1 zenon_Vdf zenon_Vef) % 0.16/0.70 (zenon_Vbk != zenon_Vnd) % 0.16/0.70 (zenon_Vlh != zenon_Vxc) % 0.16/0.70 (zenon_Vri != zenon_Vvb) % 0.16/0.70 (r1 zenon_Vne zenon_Voe) % 0.16/0.70 (zenon_Vlj != zenon_Vnd) % 0.16/0.70 (zenon_Vdh != zenon_Vfb) % 0.16/0.70 (zenon_Vxh != zenon_Vvf) % 0.16/0.70 (zenon_Vbe != zenon_Vfg) % 0.16/0.70 (zenon_Vbi != zenon_Vtd) % 0.16/0.70 (zenon_Vji != zenon_Vpc) % 0.16/0.70 (zenon_Vph != zenon_Vpc) % 0.16/0.70 (zenon_Vxj != zenon_Vhe) % 0.16/0.70 (zenon_Vvi != zenon_Vqf) % 0.16/0.70 (zenon_Vzf != zenon_Vpc) % 0.16/0.70 (zenon_Vvi != zenon_Vfg) % 0.16/0.70 (r1 zenon_Vxe zenon_Vcf) % 0.16/0.70 (zenon_Vbe != zenon_Vzg) % 0.16/0.70 (zenon_Vth != zenon_Veh) % 0.16/0.70 (zenon_Vve != zenon_Vag) % 0.16/0.70 (zenon_Vth != zenon_Vre) % 0.16/0.70 (zenon_Vbk != zenon_Vjb) % 0.16/0.70 (zenon_Vji != zenon_Vhc) % 0.16/0.70 (zenon_Vwd != zenon_Vrb) % 0.16/0.70 (zenon_Vpf != zenon_Vgf) % 0.16/0.70 (zenon_Vtg != zenon_Vlc) % 0.16/0.70 (zenon_Vwd != zenon_Vgf) % 0.16/0.70 (zenon_Vzf != zenon_Vxc) % 0.16/0.70 (zenon_Vzf != zenon_Vxd) % 0.16/0.70 (zenon_Vpf != zenon_Vtc) % 0.16/0.70 (zenon_Vtj != zenon_Vtc) % 0.16/0.70 (zenon_Vek != zenon_Vzb) % 0.16/0.70 (zenon_Vdh != zenon_Vag) % 0.16/0.70 (zenon_Vog != zenon_Vfg) % 0.16/0.70 (zenon_Vbk != zenon_Vug) % 0.16/0.70 (zenon_Veg != zenon_Vzg) % 0.16/0.70 (zenon_Vqe != zenon_Vnd) % 0.16/0.70 (zenon_Vaf != zenon_Vvf) % 0.16/0.70 (zenon_Vwd != zenon_Vfd) % 0.16/0.70 (zenon_Vbk != zenon_Vbd) % 0.16/0.70 (zenon_Vfi != zenon_Vzb) % 0.16/0.70 (zenon_Vek != zenon_Vpc) % 0.16/0.70 (zenon_Vpj != zenon_Vfg) % 0.16/0.70 (zenon_Vge != zenon_Vbf) % 0.16/0.70 (zenon_Vwd != zenon_Vce) % 0.16/0.70 (zenon_Vkf != zenon_Vhe) % 0.16/0.70 (zenon_Vpj != zenon_Vvb) % 0.16/0.70 (zenon_Vri != zenon_Vdc) % 0.16/0.70 (zenon_Vhj != zenon_Vxa) % 0.16/0.70 (zenon_Vqe != zenon_Vwe) % 0.16/0.70 (zenon_Vbe != zenon_Vdc) % 0.16/0.70 (zenon_Vtj != zenon_Vfg) % 0.16/0.70 (zenon_Vni != zenon_Vxd) % 0.16/0.70 (zenon_Vhj != zenon_Vme) % 0.16/0.70 (p1 zenon_Vbi) % 0.16/0.70 (zenon_Vlj != zenon_Vjb) % 0.16/0.70 (zenon_Vji != zenon_Vbf) % 0.16/0.70 (zenon_Vpj != zenon_Vme) % 0.16/0.70 (zenon_Vqe != zenon_Vvb) % 0.16/0.70 (zenon_Vvi != zenon_Vlf) % 0.16/0.70 (zenon_Vbe != zenon_Vqf) % 0.16/0.70 (r1 zenon_Vej zenon_Vhj) % 0.16/0.70 (-. (p1 zenon_Vwe)) % 0.16/0.70 (zenon_Vvi != zenon_Vkg) % 0.16/0.70 (zenon_Vuf != zenon_Vme) % 0.16/0.70 (zenon_Vve != zenon_Vnd) % 0.16/0.70 (zenon_Vpj != zenon_Vxa) % 0.16/0.70 (zenon_Vxh != zenon_Vxd) % 0.16/0.70 (zenon_Vlj != zenon_Vkg) % 0.16/0.70 (zenon_Vbk != zenon_Vpc) % 0.16/0.70 (zenon_Vhj != zenon_Vzg) % 0.16/0.70 (zenon_Vxj != zenon_Vzb) % 0.16/0.70 (zenon_Vdj != zenon_Vme) % 0.16/0.70 (zenon_Vsd != zenon_Vre) % 0.16/0.70 (zenon_Vge != zenon_Vpc) % 0.16/0.70 (zenon_Vbe != zenon_Vkg) % 0.16/0.70 (zenon_Vaf != zenon_Vxc) % 0.16/0.70 (zenon_Vpf != zenon_Vbf) % 0.16/0.70 (zenon_Vtg != zenon_Vdc) % 0.16/0.70 (zenon_Vff != zenon_Vfg) % 0.16/0.70 (r1 zenon_Vyj zenon_Vbk) % 0.16/0.70 (zenon_Vdj != zenon_Vxc) % 0.16/0.70 (zenon_Vtg != zenon_Vnb) % 0.16/0.70 (zenon_Vdj != zenon_Vwe) % 0.16/0.70 (zenon_Vxj != zenon_Vag) % 0.16/0.70 (zenon_Vsd != zenon_Vpg) % 0.16/0.70 (zenon_Vji != zenon_Vfg) % 0.16/0.70 (zenon_Vve != zenon_Vtd) % 0.16/0.70 (zenon_Vzi != zenon_Vqd) % 0.16/0.70 (zenon_Vbe != zenon_Vnb) % 0.16/0.70 (zenon_Vxh != zenon_Vbf) % 0.16/0.70 (zenon_Vbi != zenon_Vvb) % 0.16/0.70 (zenon_Vji != zenon_Vzg) % 0.16/0.70 (zenon_Vaf != zenon_Vbb) % 0.16/0.70 (zenon_Vwd != zenon_Vxd) % 0.16/0.70 (zenon_Vzf != zenon_Vzb) % 0.16/0.70 (zenon_Vle != zenon_Vxa) % 0.16/0.70 (r1 zenon_Vif zenon_Vjf) % 0.16/0.70 (zenon_Vve != zenon_Vjd) % 0.16/0.70 (zenon_Vvi != zenon_Vdc) % 0.16/0.70 (r1 zenon_Vwi zenon_Vzi) % 0.16/0.70 (zenon_Vuf != zenon_Vag) % 0.16/0.70 (zenon_Vfi != zenon_Vxd) % 0.16/0.70 (r1 zenon_Vmc zenon_Vpc) % 0.16/0.70 (zenon_Vlh != zenon_Veh) % 0.16/0.70 (zenon_Vri != zenon_Vug) % 0.16/0.70 (zenon_Vpj != zenon_Vdc) % 0.16/0.70 (zenon_Vog != zenon_Vzg) % 0.16/0.70 (r1 zenon_Vsf zenon_Vvf) % 0.16/0.70 (zenon_Vtg != zenon_Vgf) % 0.16/0.70 (zenon_Vph != zenon_Vqf) % 0.16/0.70 (zenon_Vfi != zenon_Vqf) % 0.16/0.70 (zenon_Vth != zenon_Vpg) % 0.16/0.70 (zenon_Vtj != zenon_Vkg) % 0.16/0.70 (zenon_Vlh != zenon_Vxd) % 0.16/0.70 (p1 zenon_Vge) % 0.16/0.70 (zenon_Vjg != zenon_Vme) % 0.16/0.70 (zenon_Vri != zenon_Vxd) % 0.16/0.70 (zenon_Vdh != zenon_Vtd) % 0.16/0.70 (p1 zenon_Vbk) % 0.16/0.70 (zenon_Vzf != zenon_Vhe) % 0.16/0.70 (zenon_Vqe != zenon_Vjd) % 0.16/0.70 (r1 zenon_Vcd zenon_Vfd) % 0.16/0.70 (zenon_Vaf != zenon_Vjd) % 0.16/0.70 (r1 zenon_Vuh zenon_Vxh) % 0.16/0.70 (r1 zenon_Vye zenon_Vze) % 0.16/0.70 (zenon_Vzf != zenon_Vvf) % 0.16/0.70 (zenon_Vwd != zenon_Vre) % 0.16/0.70 (r1 zenon_Vie zenon_Vne) % 0.16/0.70 (zenon_Vle != zenon_Vvf) % 0.16/0.70 (zenon_Vvi != zenon_Vtd) % 0.16/0.70 (r1 zenon_Vje zenon_Vke) % 0.16/0.70 (zenon_Vth != zenon_Vvb) % 0.16/0.70 (zenon_Vuf != zenon_Vgf) % 0.16/0.70 (r1 zenon_Vud zenon_Vxd) % 0.16/0.70 (zenon_Vni != zenon_Vqf) % 0.16/0.70 (zenon_Vkf != zenon_Vdc) % 0.16/0.70 (zenon_Veg != zenon_Vre) % 0.16/0.70 (p1 zenon_Vxh) % 0.16/0.70 (zenon_Vyg != zenon_Vpc) % 0.16/0.70 (zenon_Vtg != zenon_Vug) % 0.16/0.70 (zenon_Vlh != zenon_Vce) % 0.16/0.70 (zenon_Vff != zenon_Vce) % 0.16/0.70 (r1 zenon_Vij zenon_Vlj) % 0.16/0.70 (zenon_Vle != zenon_Vkg) % 0.16/0.70 (r1 zenon_Vuj zenon_Vxj) % 0.16/0.70 (zenon_Vbi != zenon_Vwe) % 0.16/0.70 (zenon_Vtg != zenon_Vwe) % 0.16/0.70 (zenon_Vbe != zenon_Vhc) % 0.16/0.70 (zenon_Vlh != zenon_Vkg) % 0.16/0.70 (zenon_Vth != zenon_Vlf) % 0.16/0.70 (zenon_Vff != zenon_Vfb) % 0.16/0.70 (zenon_Vdj != zenon_Vxa) % 0.16/0.70 (zenon_Vni != zenon_Vce) % 0.16/0.70 (zenon_Vff != zenon_Vqf) % 0.16/0.70 (zenon_Vle != zenon_Vhc) % 0.16/0.70 (zenon_Vff != zenon_Veh) % 0.16/0.70 (zenon_Vjg != zenon_Vdc) % 0.16/0.70 (zenon_Vxh != zenon_Vre) % 0.16/0.70 (zenon_Vqe != zenon_Vme) % 0.16/0.70 (-. (p2 zenon_Vhh)) % 0.16/0.70 (zenon_Vzi != zenon_Vhe) % 0.16/0.70 (zenon_Vzf != zenon_Vhc) % 0.16/0.70 (zenon_Vzf != zenon_Vqd) % 0.16/0.70 (zenon_Vog != zenon_Vqf) % 0.16/0.70 (zenon_Vbe != zenon_Vxc) % 0.16/0.70 (zenon_Vqe != zenon_Veh) % 0.16/0.70 (zenon_Vkf != zenon_Vbf) % 0.16/0.70 (zenon_Vtg != zenon_Veh) % 0.16/0.70 (zenon_Vtj != zenon_Vlc) % 0.16/0.70 (p1 zenon_Vzf) % 0.16/0.70 (r1 zenon_Vob zenon_Vrb) % 0.16/0.70 (zenon_Vtj != zenon_Vwe) % 0.16/0.70 (zenon_Vsd != zenon_Vlf) % 0.16/0.70 (zenon_Vdh != zenon_Vce) % 0.16/0.70 (zenon_Vni != zenon_Vxc) % 0.16/0.70 (zenon_Vjg != zenon_Vzb) % 0.16/0.70 (zenon_Vpj != zenon_Vnb) % 0.16/0.70 (r1 zenon_Vki zenon_Vni) % 0.16/0.70 (zenon_Vph != zenon_Vhe) % 0.16/0.70 (zenon_Vjg != zenon_Vgf) % 0.16/0.70 (zenon_Vvi != zenon_Vbf) % 0.16/0.70 (zenon_Vlj != zenon_Vce) % 0.16/0.70 (zenon_Vog != zenon_Vjb) % 0.16/0.70 (-. (p1 zenon_Vag)) % 0.16/0.70 (zenon_Vqe != zenon_Vfd) % 0.16/0.70 (zenon_Vbi != zenon_Vrb) % 0.16/0.70 (zenon_Vph != zenon_Vrb) % 0.16/0.70 (zenon_Vaf != zenon_Vrb) % 0.16/0.70 (zenon_Vbi != zenon_Vfg) % 0.16/0.70 (r1 zenon_Vgi zenon_Vji) % 0.16/0.70 (zenon_Vuf != zenon_Vre) % 0.16/0.70 (zenon_Vge != zenon_Vfb) % 0.16/0.70 (zenon_Vvi != zenon_Vre) % 0.16/0.70 (zenon_Vbe != zenon_Veh) % 0.16/0.70 (zenon_Vxh != zenon_Vjd) % 0.16/0.70 (zenon_Vdh != zenon_Vxa) % 0.16/0.70 (-. (p1 zenon_Vrb)) % 0.16/0.70 (zenon_Vth != zenon_Vbb) % 0.16/0.70 (zenon_Vji != zenon_Vbd) % 0.16/0.70 (r1 zenon_Vac zenon_Vdc) % 0.16/0.70 (zenon_Vtj != zenon_Vzg) % 0.16/0.70 (zenon_Vpf != zenon_Vjb) % 0.16/0.70 (r1 zenon_Vmf zenon_Vrf) % 0.16/0.70 (zenon_Vph != zenon_Vzg) % 0.16/0.70 (zenon_Vph != zenon_Vnb) % 0.16/0.70 (zenon_Veg != zenon_Vxa) % 0.16/0.70 (zenon_Vni != zenon_Vzb) % 0.16/0.70 (zenon_Vff != zenon_Vnb) % 0.16/0.70 (zenon_Vqe != zenon_Vlf) % 0.16/0.70 (zenon_Vle != zenon_Vgf) % 0.16/0.70 (zenon_Vni != zenon_Vnd) % 0.16/0.70 (zenon_Vtg != zenon_Vlf) % 0.16/0.70 (zenon_Vtj != zenon_Vre) % 0.16/0.70 (zenon_Vbe != zenon_Vbd) % 0.16/0.70 (zenon_Vlh != zenon_Vfb) % 0.16/0.70 (zenon_Vbk != zenon_Vdc) % 0.16/0.70 (zenon_Vqe != zenon_Vbf) % 0.16/0.70 (zenon_Vff != zenon_Vhe) % 0.16/0.70 (zenon_Vle != zenon_Vxd) % 0.16/0.70 (zenon_Vyg != zenon_Vhc) % 0.16/0.70 (zenon_Vkf != zenon_Vkg) % 0.16/0.70 (zenon_Vbk != zenon_Vbb) % 0.16/0.70 (r1 zenon_Vqh zenon_Vth) % 0.16/0.70 (zenon_Vth != zenon_Vxa) % 0.16/0.70 (zenon_Vhj != zenon_Vdc) % 0.16/0.70 (zenon_Vxh != zenon_Vme) % 0.16/0.70 (zenon_Vtg != zenon_Vqf) % 0.16/0.70 (zenon_Vxh != zenon_Vvb) % 0.16/0.70 (zenon_Vog != zenon_Vfb) % 0.16/0.70 (zenon_Veg != zenon_Vvf) % 0.16/0.70 (zenon_Vuf != zenon_Vfb) % 0.16/0.70 (zenon_Vth != zenon_Vjb) % 0.16/0.70 (zenon_Vni != zenon_Vpc) % 0.16/0.70 (zenon_Vge != zenon_Vdc) % 0.16/0.70 (zenon_Vxh != zenon_Vpg) % 0.16/0.70 (zenon_Vlj != zenon_Vhc) % 0.16/0.70 (zenon_Vve != zenon_Vpc) % 0.16/0.70 (zenon_Vlh != zenon_Vbb) % 0.16/0.70 (zenon_Vge != zenon_Vre) % 0.16/0.70 (zenon_Vlj != zenon_Vpc) % 0.16/0.70 (zenon_Vsd != zenon_Vlc) % 0.16/0.70 (zenon_Vve != zenon_Vpg) % 0.16/0.70 (r1 zenon_Vhf zenon_Vmf) % 0.16/0.70 (zenon_Vpf != zenon_Vre) % 0.16/0.70 (zenon_Vff != zenon_Vbb) % 0.16/0.70 (zenon_Vtj != zenon_Vxa) % 0.16/0.70 (zenon_Vuf != zenon_Vxc) % 0.16/0.70 (zenon_Vle != zenon_Vug) % 0.16/0.70 (zenon_Vge != zenon_Vlc) % 0.16/0.70 (zenon_Vwd != zenon_Vnd) % 0.16/0.70 (zenon_Vtg != zenon_Vjb) % 0.16/0.70 (zenon_Vji != zenon_Vtd) % 0.16/0.70 (zenon_Vjg != zenon_Vre) % 0.16/0.70 (zenon_Vwd != zenon_Vbf) % 0.16/0.70 (r1 zenon_Vbg zenon_Vgg) % 0.16/0.70 (zenon_Vyg != zenon_Vme) % 0.16/0.70 (r1 zenon_Vmg zenon_Vpg) % 0.16/0.70 (zenon_Vwd != zenon_Vxa) % 0.16/0.70 (zenon_Vdh != zenon_Vhe) % 0.16/0.70 (zenon_Vbi != zenon_Vqf) % 0.16/0.70 (zenon_Vph != zenon_Vzb) % 0.16/0.70 (zenon_Vri != zenon_Vxc) % 0.16/0.70 (zenon_Vph != zenon_Vxc) % 0.16/0.70 (zenon_Vbe != zenon_Vtc) % 0.16/0.70 (zenon_Vzi != zenon_Vpc) % 0.16/0.70 (zenon_Vwd != zenon_Vtd) % 0.16/0.70 (r1 zenon_Vyc zenon_Vbd) % 0.16/0.70 (zenon_Vlh != zenon_Vvb) % 0.16/0.70 (zenon_Vpj != zenon_Vbb) % 0.16/0.70 (zenon_Vri != zenon_Vgf) % 0.16/0.70 (r1 zenon_Vcg zenon_Vdg) % 0.16/0.70 (zenon_Vbi != zenon_Vce) % 0.16/0.70 (zenon_Vuf != zenon_Vhe) % 0.16/0.70 (zenon_Vsd != zenon_Vfg) % 0.16/0.70 (zenon_Vzi != zenon_Vnd) % 0.16/0.70 (zenon_Vth != zenon_Vxc) % 0.16/0.70 (zenon_Vff != zenon_Vvb) % 0.16/0.70 (zenon_Vek != zenon_Vbb) % 0.16/0.70 (r1 zenon_Vlg zenon_Vmg) % 0.16/0.70 (zenon_Vuf != zenon_Vtc) % 0.16/0.70 (zenon_Vlj != zenon_Vzb) % 0.16/0.70 (zenon_Vjg != zenon_Vbb) % 0.16/0.70 (zenon_Vlj != zenon_Vwe) % 0.16/0.70 (zenon_Vle != zenon_Vpc) % 0.16/0.70 (zenon_Vuf != zenon_Vbb) % 0.16/0.70 (zenon_Vek != zenon_Vag) % 0.16/0.70 (r1 zenon_Vwg zenon_Vxg) % 0.16/0.70 (zenon_Vdh != zenon_Vdc) % 0.16/0.70 (zenon_Vve != zenon_Vxc) % 0.16/0.70 (zenon_Vbk != zenon_Vnb) % 0.16/0.70 (zenon_Vog != zenon_Vpc) % 0.16/0.70 (zenon_Vle != zenon_Vvb) % 0.16/0.70 (zenon_Vvi != zenon_Vug) % 0.16/0.70 (zenon_Vdj != zenon_Vkg) % 0.16/0.70 (zenon_Vtg != zenon_Vxd) % 0.16/0.70 (zenon_Vtj != zenon_Vvf) % 0.16/0.70 (zenon_Vzf != zenon_Vlf) % 0.16/0.70 (zenon_Vri != zenon_Vme) % 0.16/0.70 (r1 zenon_Vyd zenon_Vde) % 0.16/0.70 (zenon_Vog != zenon_Vpg) % 0.16/0.70 (zenon_Vji != zenon_Vnd) % 0.16/0.70 (zenon_Vog != zenon_Vlc) % 0.16/0.70 (zenon_Vtg != zenon_Vrb) % 0.16/0.70 (zenon_Vek != zenon_Vxa) % 0.16/0.70 (zenon_Vbi != zenon_Vfb) % 0.16/0.70 (zenon_Vlj != zenon_Vug) % 0.16/0.70 (zenon_Vzf != zenon_Vvb) % 0.16/0.70 (zenon_Vri != zenon_Vbb) % 0.16/0.70 (r1 zenon_Vmg zenon_Vng) % 0.16/0.70 (zenon_Vuf != zenon_Vjb) % 0.16/0.70 (zenon_Vhj != zenon_Vtd) % 0.16/0.70 (zenon_Vfi != zenon_Vpg) % 0.16/0.70 (zenon_Vni != zenon_Vlc) % 0.16/0.70 (r1 zenon_Vbh zenon_Veh) % 0.16/0.70 (zenon_Vbk != zenon_Vre) % 0.16/0.70 (zenon_Vge != zenon_Vbd) % 0.16/0.70 (zenon_Vji != zenon_Vce) % 0.16/0.70 (zenon_Vhj != zenon_Vlc) % 0.16/0.70 (zenon_Vaf != zenon_Vzg) % 0.16/0.70 (zenon_Vri != zenon_Vfg) % 0.16/0.70 (p1 zenon_Vfi) % 0.16/0.70 (zenon_Vkf != zenon_Vme) % 0.16/0.70 (zenon_Vth != zenon_Vtd) % 0.16/0.70 (zenon_Vxj != zenon_Vtd) % 0.16/0.70 (zenon_Vkf != zenon_Vug) % 0.16/0.70 (zenon_Vek != zenon_Vqf) % 0.16/0.70 (zenon_Vlh != zenon_Vhe) % 0.16/0.70 (zenon_Vjg != zenon_Vbf) % 0.16/0.70 (zenon_Vzf != zenon_Vtc) % 0.16/0.70 (zenon_Vxh != zenon_Vfb) % 0.16/0.70 (zenon_Vek != zenon_Vtd) % 0.16/0.70 (zenon_Vlh != zenon_Vnd) % 0.16/0.70 (zenon_Vdh != zenon_Vpc) % 0.16/0.70 (zenon_Vlh != zenon_Vpc) % 0.16/0.70 (zenon_Vtg != zenon_Vpg) % 0.16/0.70 (zenon_Vuf != zenon_Vzb) % 0.16/0.70 (zenon_Vyg != zenon_Vbf) % 0.16/0.70 (zenon_Vaf != zenon_Vhe) % 0.16/0.70 (zenon_Vpj != zenon_Vwe) % 0.16/0.70 (zenon_Vwd != zenon_Vwe) % 0.16/0.70 (zenon_Vlh != zenon_Vhc) % 0.16/0.70 (zenon_Vjg != zenon_Vhe) % 0.16/0.70 (zenon_Vge != zenon_Vkg) % 0.16/0.70 (r1 zenon_X6 zenon_Vek) % 0.16/0.70 (zenon_Vbe != zenon_Vzb) % 0.16/0.70 (zenon_Vff != zenon_Vxc) % 0.16/0.70 (r1 zenon_Vgd zenon_Vjd) % 0.16/0.70 (zenon_Vle != zenon_Vzg) % 0.16/0.70 (zenon_Vpf != zenon_Vzg) % 0.16/0.70 (zenon_Vdj != zenon_Vfd) % 0.16/0.70 (zenon_Vjg != zenon_Vtc) % 0.16/0.70 (zenon_Veg != zenon_Vrb) % 0.16/0.70 (zenon_Vek != zenon_Vnd) % 0.16/0.70 (zenon_Vbi != zenon_Vbf) % 0.16/0.70 (zenon_Vdh != zenon_Vvb) % 0.16/0.70 (zenon_Vbi != zenon_Vjd) % 0.16/0.70 (zenon_Vjg != zenon_Vnd) % 0.16/0.70 (r1 zenon_Vuc zenon_Vxc) % 0.16/0.70 (zenon_Vzf != zenon_Vkg) % 0.16/0.70 (zenon_Vek != zenon_Vlc) % 0.16/0.70 (zenon_Vdh != zenon_Vme) % 0.16/0.70 (zenon_Vfi != zenon_Vtc) % 0.16/0.70 (zenon_Vni != zenon_Vgf) % 0.16/0.70 (zenon_Vpf != zenon_Vnd) % 0.16/0.70 (zenon_Vri != zenon_Vbd) % 0.16/0.70 (zenon_Vff != zenon_Vfd) % 0.16/0.70 (zenon_Vxh != zenon_Vtd) % 0.16/0.70 (zenon_Vri != zenon_Vqd) % 0.16/0.70 (zenon_Vff != zenon_Vgf) % 0.16/0.70 (zenon_Vlj != zenon_Vhe) % 0.16/0.70 (p1 zenon_Vog) % 0.16/0.70 (zenon_Vxj != zenon_Vfd) % 0.16/0.70 (zenon_Vni != zenon_Vzg) % 0.16/0.70 (zenon_Vqe != zenon_Vpg) % 0.16/0.70 (zenon_Vsd != zenon_Vjd) % 0.16/0.70 (zenon_Vff != zenon_Vrb) % 0.16/0.70 (zenon_Vxj != zenon_Vfg) % 0.16/0.70 (zenon_Vph != zenon_Vce) % 0.16/0.70 (zenon_Vhj != zenon_Vce) % 0.16/0.70 (zenon_Vbi != zenon_Vlc) % 0.16/0.70 (zenon_Vpj != zenon_Vqf) % 0.16/0.70 (zenon_Vph != zenon_Vfd) % 0.16/0.70 (zenon_Vaf != zenon_Vtd) % 0.16/0.70 (zenon_Vph != zenon_Vxa) % 0.16/0.70 (zenon_Vyg != zenon_Vfg) % 0.16/0.70 (zenon_Vni != zenon_Vhe) % 0.16/0.70 (zenon_Vbk != zenon_Vbf) % 0.16/0.70 (zenon_Vjg != zenon_Vvb) % 0.16/0.70 (zenon_Vyg != zenon_Vxd) % 0.16/0.70 (zenon_Vle != zenon_Vfg) % 0.16/0.70 (zenon_Vge != zenon_Vjb) % 0.16/0.70 (zenon_Vuf != zenon_Vpg) % 0.16/0.70 (zenon_Vpj != zenon_Vtc) % 0.16/0.70 (zenon_Veg != zenon_Vtc) % 0.16/0.70 (zenon_Vzf != zenon_Vnd) % 0.16/0.70 (zenon_Vni != zenon_Vwe) % 0.16/0.70 (-. (p1 zenon_Vbd)) % 0.16/0.70 (zenon_Vge != zenon_Vnd) % 0.16/0.70 (-. (p1 zenon_Vqd)) % 0.16/0.70 (zenon_Vvi != zenon_Vwe) % 0.16/0.70 (zenon_Vge != zenon_Vtd) % 0.16/0.70 (zenon_Vlj != zenon_Vvb) % 0.16/0.70 (zenon_Vek != zenon_Vfd) % 0.16/0.70 *) % 0.16/0.70 (* NO-PROOF *) % 0.16/0.70 % SZS status GaveUp % 0.16/0.70 Number of rewrites on terms: 0 % 0.16/0.70 Number of rewrites on props: 0 % 0.16/0.70 nodes searched: 2030 % 0.16/0.70 max branch formulas: 2228 % 0.16/0.70 proof nodes created: 0 % 0.16/0.70 formulas created: 10804 % 0.16/0.70 %------------------------------------------------------------------------------