ZenonModulo---0.5.0.UNK-Non.f

%------------------------------------------------------------------------------
% File     : ZenonModulo---0.5.0
% Problem  : LCL685+1.015 : TPTP v9.3.1. Released v4.0.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : run_zenon_modulo %d %s

% Computer : n001.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:29 PM UTC 2026

% Result   : Unknown 257.77s 258.10s
% Output   : None 
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : LCL685+1.015 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03  % Command  : run_zenon_modulo %d %s
% 0.08/0.35  % Computer : n001.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 : Sat Sep  5 11:07:31 UTC 2026
% 0.08/0.35  % CPUTime  : 
% 257.77/258.08  Zenon error: exhausted search space without finding a proof
% 257.77/258.08  (* Current branch:
% 257.77/258.08  (-. (p805 zenon_Vuxc))
% 257.77/258.08  (-. (p1404 zenon_Vkdd))
% 257.77/258.08  (-. (p809 zenon_Vqqb))
% 257.77/258.08  (-. (p105 zenon_Vzcd))
% 257.77/258.08  (-. (p115 zenon_Vll))
% 257.77/258.08  (-. (p515 zenon_Vnf))
% 257.77/258.08  (r1 zenon_Vosa zenon_Vqsa)
% 257.77/258.08  (-. (p509 zenon_Vnsb))
% 257.77/258.08  (-. (p412 zenon_Vxpa))
% 257.77/258.08  (-. (p1412 zenon_Vwja))
% 257.77/258.08  (-. (p1410 zenon_Vgfb))
% 257.77/258.08  (r1 zenon_Vlea zenon_Vmea)
% 257.77/258.08  (-. (p303 zenon_Vxmd))
% 257.77/258.08  (r1 zenon_Vgbc zenon_Vhbc)
% 257.77/258.08  (-. (p601 zenon_Vqwd))
% 257.77/258.08  (-. (p1109 zenon_Vnpb))
% 257.77/258.08  (r1 zenon_Vqgc zenon_Vsgc)
% 257.77/258.08  (r1 zenon_Vtka zenon_Vuka)
% 257.77/258.08  (-. (p109 zenon_Vhxb))
% 257.77/258.08  (r1 zenon_Vmjd zenon_Vojd)
% 257.77/258.08  (-. (p601 zenon_Vmwd))
% 257.77/258.08  (-. (p113 zenon_Vzia))
% 257.77/258.08  (-. (p1311 zenon_Vxua))
% 257.77/258.08  (-. (p207 zenon_Vanc))
% 257.77/258.08  (-. (p413 zenon_Viea))
% 257.77/258.08  (-. (p311 zenon_Vxbb))
% 257.77/258.08  (-. (p1010 zenon_Vwfb))
% 257.77/258.08  (r1 zenon_Vow zenon_Vqw)
% 257.77/258.08  (-. (p403 zenon_Vkmd))
% 257.77/258.08  (r1 zenon_Vebb zenon_Vfbb)
% 257.77/258.08  (-. (p102 zenon_Vgud))
% 257.77/258.08  (-. (p308 zenon_Vodc))
% 257.77/258.08  (-. (p603 zenon_Vqld))
% 257.77/258.08  (-. (p813 zenon_Vmaa))
% 257.77/258.08  (r1 zenon_Vuab zenon_Vwab)
% 257.77/258.08  (-. (p314 zenon_Vru))
% 257.77/258.08  (-. (p208 zenon_Vzec))
% 257.77/258.08  (r1 zenon_Vbrb zenon_Vcrb)
% 257.77/258.08  (r1 zenon_Vrac zenon_Vsac)
% 257.77/258.08  (-. (p501 zenon_Vxwd))
% 257.77/258.08  (r1 zenon_Vzoa zenon_Vbpa)
% 257.77/258.08  (r1 zenon_Vxgb zenon_Vygb)
% 257.77/258.08  (r1 zenon_Vde zenon_Vfe)
% 257.77/258.08  (-. (p1004 zenon_Vbed))
% 257.77/258.08  (-. (p106 zenon_Vkvc))
% 257.77/258.08  (-. (p902 zenon_Vjqd))
% 257.77/258.08  (r1 zenon_Vmya zenon_Voya)
% 257.77/258.08  (-. (p703 zenon_Vhld))
% 257.77/258.08  (r1 zenon_Vdqb zenon_Veqb)
% 257.77/258.08  (r1 zenon_Veab zenon_Vfab)
% 257.77/258.08  (-. (p615 zenon_Vaf))
% 257.77/258.08  (-. (p513 zenon_Vjda))
% 257.77/258.08  (r1 zenon_Vjmc zenon_Vkmc)
% 257.77/258.08  (r1 zenon_Vjj zenon_Vlj)
% 257.77/258.08  (-. (p702 zenon_Vwqd))
% 257.77/258.08  (-. (p504 zenon_Vofd))
% 257.77/258.08  (r1 zenon_Vkxa zenon_Vlxa)
% 257.77/258.08  (r1 zenon_Vnod zenon_Vood)
% 257.77/258.08  (r1 zenon_Vzv zenon_Vbw)
% 257.77/258.08  (-. (p404 zenon_Vbgd))
% 257.77/258.08  (r1 zenon_Vjad zenon_Vkad)
% 257.77/258.08  (r1 zenon_Vhqa zenon_Vjqa)
% 257.77/258.08  (r1 zenon_Vhob zenon_Vjob)
% 257.77/258.08  (-. (p205 zenon_Vjbd))
% 257.77/258.08  (r1 zenon_Vusa zenon_Vwsa)
% 257.77/258.08  (-. (p408 zenon_Vjcc))
% 257.77/258.08  (-. (p213 zenon_Vcia))
% 257.77/258.08  (-. (p206 zenon_Vtuc))
% 257.77/258.08  (r1 zenon_Vjqb zenon_Vkqb)
% 257.77/258.08  (-. (p605 zenon_Viyc))
% 257.77/258.08  (r1 zenon_Vifa zenon_Vkfa)
% 257.77/258.08  (r1 zenon_Vlsc zenon_Vmsc)
% 257.77/258.08  (-. (p701 zenon_Vjwd))
% 257.77/258.08  (-. (p204 zenon_Vuhd))
% 257.77/258.08  (r1 zenon_Vocd zenon_Vpcd)
% 257.77/258.08  (r1 zenon_Vela zenon_Vfla)
% 257.77/258.08  (-. (p815 zenon_Vqc))
% 257.77/258.08  (-. (p209 zenon_Vzvb))
% 257.77/258.08  (-. (p408 zenon_Vncc))
% 257.77/258.08  (-. (p1107 zenon_Vhhc))
% 257.77/258.08  (-. (p1203 zenon_Vakd))
% 257.77/258.08  (r1 zenon_Vquc zenon_Vruc)
% 257.77/258.08  (-. (p413 zenon_Vvea))
% 257.77/258.08  (-. (p415 zenon_Vhg))
% 257.77/258.08  (r1 zenon_Vsya zenon_Vuya)
% 257.77/258.08  (-. (p306 zenon_Vxsc))
% 257.77/258.08  (-. (p312 zenon_Vlra))
% 257.77/258.08  (-. (p814 zenon_Vso))
% 257.77/258.08  (r1 zenon_Vbo zenon_Vco)
% 257.77/258.08  (r1 zenon_Vcn zenon_Ven)
% 257.77/258.08  (-. (p708 zenon_Vcac))
% 257.77/258.08  (-. (p1101 zenon_Vbvd))
% 257.77/258.08  (-. (p202 zenon_Vetd))
% 257.77/258.08  (-. (p807 zenon_Vyhc))
% 257.77/258.08  (-. (p814 zenon_Vap))
% 257.77/258.08  (-. (p603 zenon_Vlld))
% 257.77/258.08  (-. (p1302 zenon_Vqpd))
% 257.77/258.08  (r1 zenon_Vypa zenon_Vaqa)
% 257.77/258.08  (r1 zenon_Vbsa zenon_Vcsa)
% 257.77/258.08  (r1 zenon_Viga zenon_Vkga)
% 257.77/258.08  (r1 zenon_Vica zenon_Vjca)
% 257.77/258.08  (r1 zenon_Vtta zenon_Vvta)
% 257.77/258.08  (-. (p306 zenon_Vhtc))
% 257.77/258.08  (r1 zenon_Vuvb zenon_Vvvb)
% 257.77/258.08  (r1 zenon_Vtod zenon_Vuod)
% 257.77/258.08  (r1 zenon_Vpgb zenon_Vqgb)
% 257.77/258.08  (r1 zenon_Vvrc zenon_Vwrc)
% 257.77/258.08  (r1 zenon_Vssb zenon_Vtsb)
% 257.77/258.08  (-. (p913 zenon_Vzz))
% 257.77/258.08  (r1 zenon_Vbwa zenon_Vcwa)
% 257.77/258.08  (-. (p613 zenon_Vjca))
% 257.77/258.08  (-. (p102 zenon_Vstd))
% 257.77/258.08  (r1 zenon_Vqtc zenon_Vrtc)
% 257.77/258.08  (-. (p505 zenon_Vsyc))
% 257.77/258.08  (-. (p214 zenon_Vjv))
% 257.77/258.08  (r1 zenon_Vnnb zenon_Vonb)
% 257.77/258.08  (r1 zenon_Vngd zenon_Vogd)
% 257.77/258.08  (r1 zenon_Vlud zenon_Vmud)
% 257.77/258.08  (-. (p807 zenon_Vzhc))
% 257.77/258.08  (r1 zenon_Veuc zenon_Vfuc)
% 257.77/258.08  (-. (p1301 zenon_Vvud))
% 257.77/258.08  (-. (p407 zenon_Vvkc))
% 257.77/258.09  (-. (p507 zenon_Vmjc))
% 257.77/258.09  (-. (p904 zenon_Veed))
% 257.77/258.09  (-. (p615 zenon_Voe))
% 257.77/258.09  (r1 zenon_Vml zenon_Vol)
% 257.77/258.09  (-. (p205 zenon_Vybd))
% 257.77/258.09  (r1 zenon_Vebc zenon_Vfbc)
% 257.77/258.09  (r1 zenon_Vsh zenon_Vuh)
% 257.77/258.09  (r1 zenon_Vlsa zenon_Vnsa)
% 257.77/258.09  (-. (p901 zenon_Vnvd))
% 257.77/258.09  (-. (p715 zenon_Vbd))
% 257.77/258.09  (r1 zenon_Vvbb zenon_Vxbb)
% 257.77/258.09  (-. (p305 zenon_Vxad))
% 257.77/258.09  (r1 zenon_Vbcb zenon_Vdcb)
% 257.77/258.09  (-. (p311 zenon_Vdcb))
% 257.77/258.09  (-. (p1213 zenon_Vuy))
% 257.77/258.09  (-. (p1010 zenon_Vvfb))
% 257.77/258.09  (-. (p313 zenon_Vhga))
% 257.77/258.09  (-. (p107 zenon_Vroc))
% 257.77/258.09  (r1 zenon_Vot zenon_Vqt)
% 257.77/258.09  (-. (p502 zenon_Vprd))
% 257.77/258.09  (r1 zenon_Vwbd zenon_Vybd)
% 257.77/258.09  (-. (p304 zenon_Vsgd))
% 257.77/258.09  (r1 zenon_Vytc zenon_Vztc)
% 257.77/258.09  (r1 zenon_Vpqb zenon_Vqqb)
% 257.77/258.09  (r1 zenon_Vka zenon_Vla)
% 257.77/258.09  (-. (p110 zenon_Vdob))
% 257.77/258.09  (p101 Tau_0)
% 257.77/258.09  (-. (p310 zenon_Vrlb))
% 257.77/258.09  (-. (p109 zenon_Vfxb))
% 257.77/258.09  (r1 zenon_Vgla zenon_Vhla)
% 257.77/258.09  (r1 zenon_Vfh zenon_Vhh)
% 257.77/258.09  (-. (p706 zenon_Vlqc))
% 257.77/258.09  (-. (p514 zenon_Vms))
% 257.77/258.09  (-. (p1201 zenon_Vxud))
% 257.77/258.09  (-. (p405 zenon_Vczc))
% 257.77/258.09  (-. (p1213 zenon_Voy))
% 257.77/258.09  (r1 zenon_Vxqb zenon_Vyqb)
% 257.77/258.09  (r1 zenon_Vpjb zenon_Vrjb)
% 257.77/258.09  (r1 zenon_Vbz zenon_Vcz)
% 257.77/258.09  (-. (p601 zenon_Vrwd))
% 257.77/258.09  (-. (p415 zenon_Vyg))
% 257.77/258.09  (-. (p1007 zenon_Vqhc))
% 257.77/258.09  (-. (p301 zenon_Vcyd))
% 257.77/258.09  (-. (p904 zenon_Vied))
% 257.77/258.09  (-. (p511 zenon_Vyya))
% 257.77/258.09  (-. (p508 zenon_Vzbc))
% 257.77/258.09  (r1 zenon_Vtd zenon_Vvd)
% 257.77/258.09  (-. (p105 zenon_Vxcd))
% 257.77/258.09  (r1 zenon_Vukc zenon_Vvkc)
% 257.77/258.09  (-. (p1213 zenon_Vqy))
% 257.77/258.09  (-. (p103 zenon_Vwod))
% 257.77/258.09  (r1 zenon_Vilc zenon_Vjlc)
% 257.77/258.09  (Tau_0 != zenon_Vrud)
% 257.77/258.09  (Tau_0 != zenon_Vsud)
% 257.77/258.09  (Tau_0 != zenon_Vtud)
% 257.77/258.09  (Tau_0 != zenon_Vuud)
% 257.77/258.09  (Tau_0 != zenon_Vvud)
% 257.77/258.09  (Tau_0 != zenon_Vwud)
% 257.77/258.09  (Tau_0 != zenon_Vxud)
% 257.77/258.09  (Tau_0 != zenon_Vyud)
% 257.77/258.09  (Tau_0 != zenon_Vzud)
% 257.77/258.09  (Tau_0 != zenon_Vavd)
% 257.77/258.09  (Tau_0 != zenon_Vbvd)
% 257.77/258.09  (Tau_0 != zenon_Vcvd)
% 257.77/258.09  (Tau_0 != zenon_Vdvd)
% 257.77/258.09  (Tau_0 != zenon_Vevd)
% 257.77/258.09  (Tau_0 != zenon_Vfvd)
% 257.77/258.09  (Tau_0 != zenon_Vgvd)
% 257.77/258.09  (Tau_0 != zenon_Vhvd)
% 257.77/258.09  (Tau_0 != zenon_Vivd)
% 257.77/258.09  (Tau_0 != zenon_Vjvd)
% 257.77/258.09  (Tau_0 != zenon_Vkvd)
% 257.77/258.09  (Tau_0 != zenon_Vlvd)
% 257.77/258.09  (Tau_0 != zenon_Vmvd)
% 257.77/258.09  (Tau_0 != zenon_Vnvd)
% 257.77/258.09  (Tau_0 != zenon_Vovd)
% 257.77/258.09  (Tau_0 != zenon_Vpvd)
% 257.77/258.09  (Tau_0 != zenon_Vqvd)
% 257.77/258.09  (Tau_0 != zenon_Vrvd)
% 257.77/258.09  (Tau_0 != zenon_Vsvd)
% 257.77/258.09  (Tau_0 != zenon_Vtvd)
% 257.77/258.09  (Tau_0 != zenon_Vuvd)
% 257.77/258.09  (Tau_0 != zenon_Vvvd)
% 257.77/258.09  (Tau_0 != zenon_Vwvd)
% 257.77/258.09  (Tau_0 != zenon_Vxvd)
% 257.77/258.09  (Tau_0 != zenon_Vyvd)
% 257.77/258.09  (Tau_0 != zenon_Vzvd)
% 257.77/258.09  (Tau_0 != zenon_Vawd)
% 257.77/258.09  (Tau_0 != zenon_Vbwd)
% 257.77/258.09  (Tau_0 != zenon_Vcwd)
% 257.77/258.09  (Tau_0 != zenon_Vdwd)
% 257.77/258.09  (Tau_0 != zenon_Vewd)
% 257.77/258.09  (Tau_0 != zenon_Vfwd)
% 257.77/258.09  (Tau_0 != zenon_Vgwd)
% 257.77/258.09  (Tau_0 != zenon_Vhwd)
% 257.77/258.09  (Tau_0 != zenon_Viwd)
% 257.77/258.09  (Tau_0 != zenon_Vjwd)
% 257.77/258.09  (Tau_0 != zenon_Vkwd)
% 257.77/258.09  (Tau_0 != zenon_Vlwd)
% 257.77/258.09  (Tau_0 != zenon_Vmwd)
% 257.77/258.09  (Tau_0 != zenon_Vnwd)
% 257.77/258.09  (Tau_0 != zenon_Vowd)
% 257.77/258.09  (Tau_0 != zenon_Vpwd)
% 257.77/258.09  (Tau_0 != zenon_Vqwd)
% 257.77/258.09  (Tau_0 != zenon_Vrwd)
% 257.77/258.09  (Tau_0 != zenon_Vswd)
% 257.77/258.09  (Tau_0 != zenon_Vtwd)
% 257.77/258.09  (Tau_0 != zenon_Vuwd)
% 257.77/258.09  (Tau_0 != zenon_Vvwd)
% 257.77/258.09  (Tau_0 != zenon_Vwwd)
% 257.77/258.09  (Tau_0 != zenon_Vxwd)
% 257.77/258.09  (Tau_0 != zenon_Vywd)
% 257.77/258.09  (Tau_0 != zenon_Vzwd)
% 257.77/258.09  (Tau_0 != zenon_Vaxd)
% 257.77/258.09  (Tau_0 != zenon_Vbxd)
% 257.77/258.09  (Tau_0 != zenon_Vcxd)
% 257.77/258.09  (Tau_0 != zenon_Vdxd)
% 257.77/258.09  (Tau_0 != zenon_Vexd)
% 257.77/258.09  (Tau_0 != zenon_Vfxd)
% 257.77/258.09  (Tau_0 != zenon_Vgxd)
% 257.77/258.09  (Tau_0 != zenon_Vhxd)
% 257.77/258.09  (Tau_0 != zenon_Vixd)
% 257.77/258.09  (Tau_0 != zenon_Vjxd)
% 257.77/258.09  (Tau_0 != zenon_Vkxd)
% 257.77/258.09  (Tau_0 != zenon_Vlxd)
% 257.77/258.09  (Tau_0 != zenon_Vmxd)
% 257.77/258.09  (Tau_0 != zenon_Vnxd)
% 257.77/258.09  (Tau_0 != zenon_Voxd)
% 257.77/258.09  (Tau_0 != zenon_Vpxd)
% 257.77/258.09  (Tau_0 != zenon_Vqxd)
% 257.77/258.09  (Tau_0 != zenon_Vrxd)
% 257.77/258.09  (Tau_0 != zenon_Vsxd)
% 257.77/258.09  (Tau_0 != zenon_Vtxd)
% 257.77/258.09  (Tau_0 != zenon_Vuxd)
% 257.77/258.09  (Tau_0 != zenon_Vvxd)
% 257.77/258.09  (Tau_0 != zenon_Vwxd)
% 257.77/258.09  (Tau_0 != zenon_Vxxd)
% 257.77/258.09  (Tau_0 != zenon_Vyxd)
% 257.77/258.09  (Tau_0 != zenon_Vzxd)
% 257.77/258.09  (Tau_0 != zenon_Vayd)
% 257.77/258.09  (Tau_0 != zenon_Vbyd)
% 257.77/258.09  (Tau_0 != zenon_Vcyd)
% 257.77/258.09  (Tau_0 != zenon_Vdyd)
% 257.77/258.09  (Tau_0 != zenon_Veyd)
% 257.77/258.09  (Tau_0 != zenon_Vfyd)
% 257.77/258.09  (Tau_0 != zenon_Vgyd)
% 257.77/258.09  (Tau_0 != zenon_Vhyd)
% 257.77/258.09  (Tau_0 != zenon_Viyd)
% 257.77/258.09  (Tau_0 != zenon_Vjyd)
% 257.77/258.09  (Tau_0 != zenon_Vkyd)
% 257.77/258.09  (Tau_0 != zenon_Vlyd)
% 257.77/258.09  (Tau_0 != zenon_Vmyd)
% 257.77/258.09  (Tau_0 != zenon_Vnyd)
% 257.77/258.09  (Tau_0 != zenon_Voyd)
% 257.77/258.09  (Tau_0 != zenon_Vpyd)
% 257.77/258.09  (Tau_0 != zenon_Vqyd)
% 257.77/258.09  (Tau_0 != zenon_Vryd)
% 257.77/258.09  (Tau_0 != zenon_Vsyd)
% 257.77/258.09  (Tau_0 != zenon_Vtyd)
% 257.77/258.09  (Tau_0 != zenon_Vuyd)
% 257.77/258.09  (Tau_0 != zenon_Vvyd)
% 257.77/258.09  (Tau_0 != zenon_Vwyd)
% 257.77/258.09  (Tau_0 != zenon_Vxyd)
% 257.77/258.09  (Tau_0 != zenon_Vyyd)
% 257.77/258.09  (Tau_0 != zenon_Vzyd)
% 257.77/258.09  (Tau_0 != zenon_Vazd)
% 257.77/258.09  (Tau_0 != zenon_Vbzd)
% 257.77/258.09  (Tau_0 != zenon_Vczd)
% 257.77/258.09  (Tau_0 != zenon_Vdzd)
% 257.77/258.09  (Tau_0 != zenon_Vezd)
% 257.77/258.09  (Tau_0 != zenon_Vfzd)
% 257.77/258.09  (Tau_0 != zenon_Vgzd)
% 257.77/258.09  (-. (p308 zenon_Vidc))
% 257.77/258.09  (r1 zenon_Vgja zenon_Vija)
% 257.77/258.09  (r1 zenon_Vtm zenon_Vvm)
% 257.77/258.09  (-. (p214 zenon_Vvv))
% 257.77/258.09  (r1 zenon_Vrtd zenon_Vstd)
% 257.77/258.09  (r1 zenon_Vvtd zenon_Vwtd)
% 257.77/258.09  (r1 zenon_Vlnd zenon_Vmnd)
% 257.77/258.09  (r1 zenon_Vnob zenon_Vpob)
% 257.77/258.09  (r1 zenon_Vdsb zenon_Vfsb)
% 257.77/258.09  (r1 zenon_Vjvb zenon_Vlvb)
% 257.77/258.09  (-. (p314 zenon_Vxt))
% 257.77/258.09  (-. (p303 zenon_Vtmd))
% 257.77/258.09  (-. (p714 zenon_Vlp))
% 257.77/258.09  (r1 zenon_Vwid zenon_Vxid)
% 257.77/258.09  (r1 zenon_Vufc zenon_Vvfc)
% 257.77/258.09  (-. (p1308 zenon_Vjyb))
% 257.77/258.09  (-. (p408 zenon_Vxcc))
% 257.77/258.09  (-. (p308 zenon_Vmdc))
% 257.77/258.09  (r1 zenon_Vbrc zenon_Vcrc)
% 257.77/258.09  (r1 zenon_Vxab zenon_Vzab)
% 257.77/258.09  (-. (p306 zenon_Vjtc))
% 257.77/258.09  (-. (p308 zenon_Vedc))
% 257.77/258.09  (-. (p610 zenon_Vfib))
% 257.77/258.09  (-. (p102 zenon_Voud))
% 257.77/258.09  (r1 zenon_Vhwa zenon_Vjwa)
% 257.77/258.09  (r1 zenon_Vdvc zenon_Vevc)
% 257.77/258.09  (r1 zenon_Vswa zenon_Vtwa)
% 257.77/258.09  (r1 zenon_Vev zenon_Vfv)
% 257.77/258.09  (-. (p406 zenon_Vssc))
% 257.77/258.09  (-. (p914 zenon_Vfo))
% 257.77/258.09  (-. (p614 zenon_Vtq))
% 257.77/258.09  (r1 zenon_Vrgb zenon_Vsgb)
% 257.77/258.09  (-. (p903 zenon_Vpkd))
% 257.77/258.09  (-. (p915 zenon_Vdc))
% 257.77/258.09  (r1 zenon_Vrua zenon_Vtua)
% 257.77/258.09  (-. (p713 zenon_Vpba))
% 257.77/258.09  (-. (p904 zenon_Vked))
% 257.77/258.09  (-. (p201 zenon_Vqyd))
% 257.77/258.09  (r1 zenon_Vse zenon_Vue)
% 257.77/258.09  (r1 zenon_Viv zenon_Vjv)
% 257.77/258.09  (-. (p408 zenon_Vlcc))
% 257.77/258.09  (r1 zenon_Vnmc zenon_Vomc)
% 257.77/258.09  (r1 zenon_Vbhb zenon_Vdhb)
% 257.77/258.09  (-. (p910 zenon_Vmgb))
% 257.77/258.09  (-. (p308 zenon_Vcdc))
% 257.77/258.09  (-. (p803 zenon_Vvkd))
% 257.77/258.09  (r1 zenon_Vrod zenon_Vsod)
% 257.77/258.09  (-. (p1407 zenon_Vygc))
% 257.77/258.09  (-. (p607 zenon_Vejc))
% 257.77/258.09  (-. (p211 zenon_Vkcb))
% 257.77/258.09  (r1 zenon_Vto zenon_Vuo)
% 257.77/258.09  (-. (p411 zenon_Vzab))
% 257.77/258.09  (-. (p507 zenon_Vujc))
% 257.77/258.09  (-. (p1103 zenon_Vekd))
% 257.77/258.09  (-. (p307 zenon_Vzlc))
% 257.77/258.09  (-. (p1003 zenon_Vikd))
% 257.77/258.09  (-. (p108 zenon_Vpfc))
% 257.77/258.09  (r1 zenon_Vjm zenon_Vkm)
% 257.77/258.09  (r1 zenon_Vnva zenon_Vova)
% 257.77/258.09  (-. (p303 zenon_Vwmd))
% 257.77/258.09  (r1 zenon_Vcpa zenon_Vepa)
% 257.77/258.09  (r1 zenon_Vlcb zenon_Vmcb)
% 257.77/258.09  (r1 zenon_Vxw zenon_Vzw)
% 257.77/258.09  (-. (p404 zenon_Vigd))
% 257.77/258.09  (r1 zenon_Vkjd zenon_Vljd)
% 257.77/258.09  (-. (p407 zenon_Vzkc))
% 257.77/258.09  (-. (p511 zenon_Vjza))
% 257.77/258.09  (-. (p615 zenon_Vfe))
% 257.77/258.09  (r1 zenon_Vngc zenon_Vpgc)
% 257.77/258.09  (-. (p210 zenon_Vfmb))
% 257.77/258.09  (r1 zenon_Vxtd zenon_Vytd)
% 257.77/258.09  (-. (p204 zenon_Vaid))
% 257.77/258.09  (-. (p905 zenon_Vkxc))
% 257.77/258.09  (r1 zenon_Vnqa zenon_Voqa)
% 257.77/258.09  (-. (p411 zenon_Vqab))
% 257.77/258.09  (r1 zenon_Vmta zenon_Vnta)
% 257.77/258.09  (-. (p1307 zenon_Vzgc))
% 257.77/258.09  (-. (p308 zenon_Vydc))
% 257.77/258.09  (r1 zenon_Vbpd zenon_Vcpd)
% 257.77/258.09  (-. (p208 zenon_Vwec))
% 257.77/258.09  (r1 zenon_Vfwb zenon_Vhwb)
% 257.77/258.09  (-. (p1309 zenon_Vcpb))
% 257.77/258.09  (r1 zenon_Vmia zenon_Vnia)
% 257.77/258.09  (-. (p1312 zenon_Vzja))
% 257.77/258.09  (-. (p1108 zenon_Vsyb))
% 257.77/258.09  (-. (p801 zenon_Vyvd))
% 257.77/258.09  (-. (p1007 zenon_Vphc))
% 257.77/258.09  (-. (p1107 zenon_Vkhc))
% 257.77/258.09  (-. (p204 zenon_Vwhd))
% 257.77/258.09  (r1 zenon_Vkgc zenon_Vmgc)
% 257.77/258.09  (p1101 Tau_0)
% 257.77/258.09  (r1 zenon_Vfoc zenon_Vgoc)
% 257.77/258.09  (r1 zenon_Vnec zenon_Voec)
% 257.77/258.09  (-. (p109 zenon_Vvwb))
% 257.77/258.09  (-. (p501 zenon_Vcxd))
% 257.77/258.09  (r1 zenon_Vxub zenon_Vzub)
% 257.77/258.09  (-. (p1106 zenon_Vkpc))
% 257.77/258.09  (-. (p106 zenon_Vyvc))
% 257.77/258.09  (-. (p301 zenon_Vzxd))
% 257.77/258.09  (-. (p311 zenon_Vlbb))
% 257.77/258.09  (r1 zenon_Vsu zenon_Vuu)
% 257.77/258.09  (-. (p104 zenon_Vvid))
% 257.77/258.09  (-. (p311 zenon_Vrbb))
% 257.77/258.09  (r1 zenon_Vwla zenon_Vxla)
% 257.77/258.09  (-. (p106 zenon_Vovc))
% 257.77/258.09  (r1 zenon_Vyfc zenon_Vzfc)
% 257.77/258.09  (-. (p103 zenon_Vqod))
% 257.77/258.09  (r1 zenon_Vikc zenon_Vjkc)
% 257.77/258.09  (r1 zenon_Vrub zenon_Vsub)
% 257.77/258.09  (-. (p215 zenon_Vuj))
% 257.77/258.09  (r1 zenon_Vcbd zenon_Vdbd)
% 257.77/258.09  (-. (p611 zenon_Vcya))
% 257.77/258.09  (-. (p411 zenon_Vwab))
% 257.77/258.09  (-. (p305 zenon_Vqad))
% 257.77/258.09  (r1 zenon_Vbod zenon_Vcod)
% 257.77/258.09  (r1 zenon_Vsoc zenon_Vuoc)
% 257.77/258.09  (r1 zenon_Vlgb zenon_Vmgb)
% 257.77/258.09  (-. (p113 zenon_Vija))
% 257.77/258.09  (r1 zenon_Vsbd zenon_Vtbd)
% 257.77/258.09  (r1 zenon_Vhs zenon_Vjs)
% 257.77/258.09  (-. (p708 zenon_Vqzb))
% 257.77/258.09  (-. (p612 zenon_Vzna))
% 257.77/258.09  (-. (p514 zenon_Vrr))
% 257.77/258.09  (-. (p513 zenon_Vsda))
% 257.77/258.09  (r1 zenon_Vff zenon_Vhf)
% 257.77/258.09  (r1 zenon_Vby zenon_Vdy)
% 257.77/258.09  (-. (p203 zenon_Vind))
% 257.77/258.09  (r1 zenon_Vjid zenon_Vlid)
% 257.77/258.09  (r1 zenon_Vgia zenon_Vhia)
% 257.77/258.09  (-. (p210 zenon_Vxmb))
% 257.77/258.09  (r1 zenon_Val zenon_Vcl)
% 257.77/258.09  (-. (p1102 zenon_Vwpd))
% 257.77/258.09  (-. (p304 zenon_Vghd))
% 257.77/258.09  (r1 zenon_Vpja zenon_Vrja)
% 257.77/258.09  (-. (p406 zenon_Vksc))
% 257.77/258.09  (r1 zenon_Vgmc zenon_Vimc)
% 257.77/258.09  (-. (p407 zenon_Vflc))
% 257.77/258.09  (-. (p814 zenon_Vgp))
% 257.77/258.09  (-. (p107 zenon_Vqnc))
% 257.77/258.09  (-. (p101 zenon_Vyyd))
% 257.77/258.09  (-. (p215 zenon_Vgk))
% 257.77/258.09  (r1 zenon_Vfpa zenon_Vhpa)
% 257.77/258.09  (-. (p814 zenon_Vdp))
% 257.77/258.09  (r1 zenon_Vxuc zenon_Vzuc)
% 257.77/258.09  (-. (p109 zenon_Vjxb))
% 257.77/258.09  (r1 zenon_Vslc zenon_Vtlc)
% 257.77/258.09  (r1 zenon_Vdia zenon_Vfia)
% 257.77/258.09  (-. (p103 zenon_Vepd))
% 257.77/258.09  (r1 zenon_Vqcc zenon_Vrcc)
% 257.77/258.09  (r1 zenon_Vwp zenon_Vyp)
% 257.77/258.09  (-. (p311 zenon_Vdbb))
% 257.77/258.09  (-. (p111 zenon_Vsdb))
% 257.77/258.09  (r1 zenon_Vtjc zenon_Vujc)
% 257.77/258.09  (-. (p609 zenon_Vnrb))
% 257.77/258.09  (r1 zenon_Vnv zenon_Vpv)
% 257.77/258.09  (-. (p110 zenon_Vyob))
% 257.77/258.09  (-. (p607 zenon_Vcjc))
% 257.77/258.09  (r1 zenon_Vkn zenon_Vln)
% 257.77/258.09  (-. (p1113 zenon_Vfz))
% 257.77/258.09  (-. (p604 zenon_Vcfd))
% 257.77/258.09  (r1 zenon_Vrt zenon_Vtt)
% 257.77/258.09  (-. (p204 zenon_Vmhd))
% 257.77/258.09  (-. (p510 zenon_Vcjb))
% 257.77/258.09  (r1 zenon_Vofc zenon_Vpfc)
% 257.77/258.09  (-. (p406 zenon_Visc))
% 257.77/258.09  (-. (p210 zenon_Vlmb))
% 257.77/258.09  (-. (p701 zenon_Viwd))
% 257.77/258.09  (r1 zenon_Vrec zenon_Vsec)
% 257.77/258.09  (r1 zenon_Vhjc zenon_Vijc)
% 257.77/258.09  (r1 zenon_Vxac zenon_Vyac)
% 257.77/258.09  (-. (p902 zenon_Vlqd))
% 257.77/258.09  (r1 zenon_Vota zenon_Vpta)
% 257.77/258.09  (r1 zenon_Vvjb zenon_Vwjb)
% 257.77/258.09  (-. (p507 zenon_Vqjc))
% 257.77/258.09  (-. (p302 zenon_Vysd))
% 257.77/258.09  (-. (p1208 zenon_Vlyb))
% 257.77/258.09  (r1 zenon_Vcaa zenon_Veaa)
% 257.77/258.09  (r1 zenon_Vstc zenon_Vutc)
% 257.77/258.09  (-. (p1211 zenon_Vcva))
% 257.77/258.09  (r1 zenon_Vnda zenon_Vpda)
% 257.77/258.09  (r1 zenon_Vagc zenon_Vbgc)
% 257.77/258.09  (r1 zenon_Vbk zenon_Vdk)
% 257.77/258.09  (-. (p808 zenon_Vjzb))
% 257.77/258.09  (-. (p504 zenon_Vtfd))
% 257.77/258.09  (r1 zenon_Vjec zenon_Vkec)
% 257.77/258.09  (-. (p1310 zenon_Vhfb))
% 257.77/258.09  (r1 zenon_Vfrc zenon_Vgrc)
% 257.77/258.09  (-. (p411 zenon_Vfab))
% 257.77/258.09  (-. (p215 zenon_Vcj))
% 257.77/258.09  (r1 zenon_Vvac zenon_Vwac)
% 257.77/258.09  (-. (p508 zenon_Vtbc))
% 257.77/258.09  (-. (p515 zenon_Vcg))
% 257.77/258.09  (r1 zenon_Vrs zenon_Vss)
% 257.77/258.09  (r1 zenon_Vzba zenon_Vbca)
% 257.77/258.09  (r1 zenon_Vti zenon_Vvi)
% 257.77/258.09  (r1 zenon_Vlfa zenon_Vmfa)
% 257.77/258.09  (-. (p211 zenon_Vscb))
% 257.77/258.09  (-. (p711 zenon_Vhxa))
% 257.77/258.09  (-. (p202 zenon_Vgtd))
% 257.77/258.09  (-. (p411 zenon_Vkab))
% 257.77/258.09  (r1 zenon_Vmlb zenon_Volb)
% 257.77/258.09  (-. (p413 zenon_Vbfa))
% 257.77/258.09  (-. (p406 zenon_Vmsc))
% 257.77/258.09  (-. (p1009 zenon_Vtpb))
% 257.77/258.09  (-. (p1003 zenon_Vhkd))
% 257.77/258.09  (-. (p411 zenon_Vdab))
% 257.77/258.09  (r1 zenon_Vvnd zenon_Vwnd)
% 257.77/258.09  (-. (p514 zenon_Vgs))
% 257.77/258.09  (r1 zenon_Vjl zenon_Vll)
% 257.77/258.09  (r1 zenon_Vijd zenon_Vjjd)
% 257.77/258.09  (-. (p409 zenon_Votb))
% 257.77/258.09  (r1 zenon_Vwt zenon_Vxt)
% 257.77/258.09  (-. (p1008 zenon_Vwyb))
% 257.77/258.09  (-. (p613 zenon_Vvca))
% 257.77/258.09  (r1 zenon_Vgx zenon_Vix)
% 257.77/258.09  (-. (p509 zenon_Vysb))
% 257.77/258.09  (-. (p503 zenon_Vamd))
% 257.77/258.09  (-. (p404 zenon_Vhgd))
% 257.77/258.09  (r1 zenon_Vtub zenon_Vuub)
% 257.77/258.09  (-. (p704 zenon_Vbfd))
% 257.77/258.09  (r1 zenon_Vuwb zenon_Vvwb)
% 257.77/258.09  (r1 zenon_Vmpa zenon_Vnpa)
% 257.77/258.09  (r1 zenon_Vxn zenon_Vyn)
% 257.77/258.09  (r1 zenon_Vbf zenon_Vcf)
% 257.77/258.09  (r1 zenon_Vmo zenon_Voo)
% 257.77/258.09  (-. (p504 zenon_Vpfd))
% 257.77/258.09  (-. (p508 zenon_Vdbc))
% 257.77/258.09  (r1 zenon_Vsrb zenon_Vtrb)
% 257.77/258.09  (-. (p209 zenon_Vewb))
% 257.77/258.09  (-. (p411 zenon_Vnab))
% 257.77/258.09  (r1 zenon_Vocc zenon_Vpcc)
% 257.77/258.09  (-. (p504 zenon_Vrfd))
% 257.77/258.09  (r1 zenon_Vysc zenon_Vzsc)
% 257.77/258.09  (-. (p213 zenon_Vhha))
% 257.77/258.09  (-. (p613 zenon_Vsca))
% 257.77/258.09  (r1 zenon_Vpod zenon_Vqod)
% 257.77/258.09  (-. (p212 zenon_Vfta))
% 257.77/258.09  (p1001 Tau_0)
% 257.77/258.09  (-. (p415 zenon_Vmg))
% 257.77/258.09  (-. (p510 zenon_Vojb))
% 257.77/258.09  (r1 zenon_Vecc zenon_Vfcc)
% 257.77/258.09  (-. (p508 zenon_Vpbc))
% 257.77/258.09  (-. (p501 zenon_Vwwd))
% 257.77/258.09  (-. (p915 zenon_Vxb))
% 257.77/258.09  (r1 zenon_Vps zenon_Vqs)
% 257.77/258.09  (-. (p115 zenon_Vwk))
% 257.77/258.09  (-. (p306 zenon_Vbtc))
% 257.77/258.09  (r1 zenon_Vpj zenon_Vrj)
% 257.77/258.09  (-. (p605 zenon_Veyc))
% 257.77/258.09  (r1 zenon_Veqa zenon_Vgqa)
% 257.77/258.09  (r1 zenon_Vxha zenon_Vzha)
% 257.77/258.09  (-. (p202 zenon_Vatd))
% 257.77/258.09  (r1 zenon_Vme zenon_Voe)
% 257.77/258.09  (-. (p712 zenon_Vxma))
% 257.77/258.09  (r1 zenon_Vcbb zenon_Vdbb)
% 257.77/258.09  (-. (p307 zenon_Vnlc))
% 257.77/258.09  (r1 zenon_Vpma zenon_Vqma)
% 257.77/258.09  (-. (p808 zenon_Vkzb))
% 257.77/258.09  (r1 zenon_Vltb zenon_Vmtb)
% 257.77/258.09  (r1 zenon_Vtma zenon_Vuma)
% 257.77/258.09  (-. (p613 zenon_Vfca))
% 257.77/258.09  (-. (p1004 zenon_Vydd))
% 257.77/258.09  (r1 zenon_Vzaa zenon_Vbba)
% 257.77/258.09  (r1 zenon_Vgfc zenon_Vifc)
% 257.77/258.09  (r1 zenon_Vgnc zenon_Vinc)
% 257.77/258.09  (r1 zenon_Vwcb zenon_Vycb)
% 257.77/258.09  (r1 zenon_Voxa zenon_Vqxa)
% 257.77/258.09  (-. (p701 zenon_Vewd))
% 257.77/258.09  (-. (p303 zenon_Vumd))
% 257.77/258.09  (-. (p607 zenon_Vajc))
% 257.77/258.09  (r1 zenon_Vjeb zenon_Vleb)
% 257.77/258.09  (r1 zenon_Vdo zenon_Vfo)
% 257.77/258.09  (-. (p403 zenon_Vgmd))
% 257.77/258.09  (-. (p712 zenon_Vuma))
% 257.77/258.09  (r1 zenon_Vtgc zenon_Vvgc)
% 257.77/258.09  (-. (p1215 zenon_Vha))
% 257.77/258.09  (r1 zenon_Vnna zenon_Vona)
% 257.77/258.09  (r1 zenon_Vwcd zenon_Vxcd)
% 257.77/258.09  (-. (p1002 zenon_Vdqd))
% 257.77/258.09  (-. (p203 zenon_Vknd))
% 257.77/258.09  (r1 zenon_Vfjb zenon_Vgjb)
% 257.77/258.09  (r1 zenon_Vvy zenon_Vwy)
% 257.77/258.09  (r1 zenon_Vata zenon_Vcta)
% 257.77/258.09  (-. (p606 zenon_Vsqc))
% 257.77/258.09  (-. (p705 zenon_Vzxc))
% 257.77/258.09  (-. (p311 zenon_Vubb))
% 257.77/258.09  (-. (p715 zenon_Vmd))
% 257.77/258.09  (r1 zenon_Vemb zenon_Vfmb)
% 257.77/258.09  (-. (p601 zenon_Vpwd))
% 257.77/258.09  (-. (p207 zenon_Vmmc))
% 257.77/258.09  (-. (p212 zenon_Vesa))
% 257.77/258.09  (r1 zenon_Vwg zenon_Vyg)
% 257.77/258.09  (-. (p211 zenon_Vicb))
% 257.77/258.09  (-. (p112 zenon_Vnua))
% 257.77/258.09  (r1 zenon_Vscd zenon_Vtcd)
% 257.77/258.09  (-. (p214 zenon_Vhv))
% 257.77/258.09  (-. (p212 zenon_Vqsa))
% 257.77/258.09  (-. (p105 zenon_Vdcd))
% 257.77/258.09  (r1 zenon_Vpqa zenon_Vqqa)
% 257.77/258.09  (r1 zenon_Viua zenon_Vkua)
% 257.77/258.09  (-. (p1105 zenon_Vzwc))
% 257.77/258.09  (r1 zenon_Vdkb zenon_Vekb)
% 257.77/258.09  (-. (p1003 zenon_Vlkd))
% 257.77/258.09  (r1 zenon_Vclb zenon_Vdlb)
% 257.77/258.09  (-. (p714 zenon_Vhq))
% 257.77/258.09  (-. (p901 zenon_Vrvd))
% 257.77/258.09  (-. (p1011 zenon_Vova))
% 257.77/258.09  (-. (p412 zenon_Vppa))
% 257.77/258.09  (-. (p413 zenon_Vsea))
% 257.77/258.09  (r1 zenon_Vfjc zenon_Vgjc)
% 257.77/258.09  (-. (p409 zenon_Vgub))
% 257.77/258.09  (-. (p1007 zenon_Vlhc))
% 257.77/258.09  (-. (p111 zenon_Vydb))
% 257.77/258.09  (-. (p403 zenon_Vnmd))
% 257.77/258.09  (r1 zenon_Vkbc zenon_Vlbc)
% 257.77/258.09  (-. (p711 zenon_Vtxa))
% 257.77/258.09  (-. (p505 zenon_Vryc))
% 257.77/258.09  (-. (p1314 zenon_Vmm))
% 257.77/258.09  (-. (p1411 zenon_Vvua))
% 257.77/258.09  (-. (p106 zenon_Vivc))
% 257.77/258.09  (r1 zenon_Vzta zenon_Vbua)
% 257.77/258.09  (r1 zenon_Vdgb zenon_Vegb)
% 257.77/258.09  (-. (p504 zenon_Vwfd))
% 257.77/258.09  (r1 zenon_Vasb zenon_Vcsb)
% 257.77/258.09  (-. (p1015 zenon_Veb))
% 257.77/258.09  (-. (p612 zenon_Vina))
% 257.77/258.09  (r1 zenon_Vfw zenon_Vhw)
% 257.77/258.09  (-. (p809 zenon_Veqb))
% 257.77/258.09  (r1 zenon_Vttd zenon_Vutd)
% 257.77/258.09  (-. (p912 zenon_Vrla))
% 257.77/258.09  (-. (p604 zenon_Vifd))
% 257.77/258.09  (-. (p602 zenon_Vlrd))
% 257.77/258.09  (-. (p913 zenon_Vhaa))
% 257.77/258.09  (r1 zenon_Vhac zenon_Viac)
% 257.77/258.09  (r1 zenon_Vnea zenon_Vpea)
% 257.77/258.09  (r1 zenon_Vgr zenon_Vir)
% 257.77/258.09  (r1 zenon_Vxqa zenon_Vzqa)
% 257.77/258.09  (-. (p901 zenon_Vqvd))
% 257.77/258.09  (-. (p1010 zenon_Vxfb))
% 257.77/258.09  (-. (p208 zenon_Vcfc))
% 257.77/258.09  (-. (p801 zenon_Vtvd))
% 257.77/258.09  (-. (p815 zenon_Vnc))
% 257.77/258.09  (-. (p308 zenon_Vsdc))
% 257.77/258.09  (-. (p802 zenon_Vtqd))
% 257.77/258.09  (-. (p301 zenon_Vxxd))
% 257.77/258.09  (-. (p103 zenon_Viod))
% 257.77/258.09  (-. (p704 zenon_Vwed))
% 257.77/258.09  (-. (p602 zenon_Vjrd))
% 257.77/258.09  (r1 zenon_Vpjd zenon_Vrjd)
% 257.77/258.09  (-. (p1013 zenon_Vjz))
% 257.77/258.09  (-. (p1113 zenon_Vyy))
% 257.77/258.09  (-. (p1402 zenon_Vnpd))
% 257.77/258.09  (-. (p112 zenon_Vpta))
% 257.77/258.09  (-. (p802 zenon_Vvqd))
% 257.77/258.09  (-. (p304 zenon_Vqgd))
% 257.77/258.09  (-. (p310 zenon_Vhlb))
% 257.77/258.09  (r1 zenon_Vdya zenon_Veya)
% 257.77/258.09  (r1 zenon_Vmp zenon_Vnp)
% 257.77/258.09  (-. (p1304 zenon_Vodd))
% 257.77/258.09  (r1 zenon_Vrnc zenon_Vsnc)
% 257.77/258.09  (-. (p410 zenon_Vrkb))
% 257.77/258.09  (r1 zenon_Vula zenon_Vvla)
% 257.77/258.09  (-. (p902 zenon_Vhqd))
% 257.77/258.09  (-. (p709 zenon_Varb))
% 257.77/258.09  (-. (p415 zenon_Vhh))
% 257.77/258.09  (r1 zenon_Vbid zenon_Vcid)
% 257.77/258.09  (-. (p1204 zenon_Vrdd))
% 257.77/258.09  (-. (p204 zenon_Viid))
% 257.77/258.09  (r1 zenon_Vokc zenon_Vpkc)
% 257.77/258.09  (r1 zenon_Vxjc zenon_Vyjc)
% 257.77/258.09  (-. (p1306 zenon_Vcpc))
% 257.77/258.09  (-. (p605 zenon_Vlyc))
% 257.77/258.09  (-. (p408 zenon_Vhcc))
% 257.77/258.09  (-. (p401 zenon_Vkxd))
% 257.77/258.09  (r1 zenon_Var zenon_Vcr)
% 257.77/258.09  (-. (p806 zenon_Vaqc))
% 257.77/258.09  (r1 zenon_Vdja zenon_Vfja)
% 257.77/258.09  (-. (p408 zenon_Vrcc))
% 257.77/258.09  (-. (p913 zenon_Vxz))
% 257.77/258.09  (-. (p611 zenon_Vuya))
% 257.77/258.09  (-. (p505 zenon_Vwyc))
% 257.77/258.09  (-. (p301 zenon_Vvxd))
% 257.77/258.09  (-. (p505 zenon_Vyyc))
% 257.77/258.09  (-. (p402 zenon_Vdsd))
% 257.77/258.09  (-. (p710 zenon_Vlhb))
% 257.77/258.09  (r1 zenon_Vtic zenon_Vuic)
% 257.77/258.09  (-. (p109 zenon_Vyxb))
% 257.77/258.09  (r1 zenon_Vjba zenon_Vkba)
% 257.77/258.09  (-. (p607 zenon_Vuic))
% 257.77/258.09  (-. (p414 zenon_Vss))
% 257.77/258.09  (-. (p915 zenon_Vrb))
% 257.77/258.09  (r1 zenon_Vfkb zenon_Vgkb)
% 257.77/258.09  (-. (p707 zenon_Vjic))
% 257.77/258.09  (-. (p102 zenon_Vaud))
% 257.77/258.09  (-. (p1115 zenon_Vla))
% 257.77/258.09  (-. (p611 zenon_Viya))
% 257.77/258.09  (r1 zenon_Vxy zenon_Vyy)
% 257.77/258.09  (-. (p303 zenon_Vand))
% 257.77/258.09  (r1 zenon_Vhi zenon_Vji)
% 257.77/258.09  (r1 zenon_Vrn zenon_Vtn)
% 257.77/258.09  (-. (p605 zenon_Vgyc))
% 257.77/258.09  (r1 zenon_Vrm zenon_Vsm)
% 257.77/258.09  (-. (p1305 zenon_Vpwc))
% 257.77/258.09  (-. (p101 zenon_Vczd))
% 257.77/258.09  (r1 zenon_Vylc zenon_Vzlc)
% 257.77/258.09  (-. (p214 zenon_Vhw))
% 257.77/258.09  (r1 zenon_Vdra zenon_Vfra)
% 257.77/258.09  (-. (p603 zenon_Vold))
% 257.77/258.09  (-. (p1112 zenon_Voka))
% 257.77/258.09  (-. (p1409 zenon_Vbpb))
% 257.77/258.09  (-. (p804 zenon_Voed))
% 257.77/258.09  (-. (p314 zenon_Vxu))
% 257.77/258.09  (-. (p506 zenon_Virc))
% 257.77/258.09  (-. (p208 zenon_Vuec))
% 257.77/258.09  (r1 zenon_Vovb zenon_Vpvb)
% 257.77/258.09  (r1 zenon_Vajd zenon_Vbjd)
% 257.77/258.09  (-. (p415 zenon_Vkh))
% 257.77/258.09  (-. (p1006 zenon_Vspc))
% 257.77/258.09  (-. (p1104 zenon_Vwdd))
% 257.77/258.09  (-. (p215 zenon_Vak))
% 257.77/258.09  (-. (p815 zenon_Vwc))
% 257.77/258.09  (-. (p315 zenon_Vuh))
% 257.77/258.09  (r1 zenon_Vqhb zenon_Vrhb)
% 257.77/258.09  (r1 zenon_Vxq zenon_Vzq)
% 257.77/258.09  (r1 zenon_Vwoa zenon_Vyoa)
% 257.77/258.09  (-. (p105 zenon_Vncd))
% 257.77/258.09  (-. (p110 zenon_Vjob))
% 257.77/258.09  (-. (p105 zenon_Vfdd))
% 257.77/258.09  (r1 zenon_Vylb zenon_Vamb)
% 257.77/258.09  (r1 zenon_Vbgb zenon_Vcgb)
% 257.77/258.09  (-. (p1310 zenon_Vjfb))
% 257.77/258.09  (r1 zenon_Vkxb zenon_Vmxb)
% 257.77/258.09  (-. (p507 zenon_Vkjc))
% 257.77/258.09  (r1 zenon_Voia zenon_Vqia)
% 257.77/258.09  (r1 zenon_Vwlc zenon_Vxlc)
% 257.77/258.09  (-. (p1113 zenon_Vaz))
% 257.77/258.09  (-. (p506 zenon_Verc))
% 257.77/258.09  (-. (p309 zenon_Vsub))
% 257.77/258.09  (r1 zenon_Vyb zenon_Vac)
% 257.77/258.09  (-. (p514 zenon_Vor))
% 257.77/258.09  (-. (p401 zenon_Voxd))
% 257.77/258.09  (r1 zenon_Vvx zenon_Vxx)
% 257.77/258.09  (-. (p406 zenon_Vesc))
% 257.77/258.09  (-. (p203 zenon_Vund))
% 257.77/258.09  (r1 zenon_Vvkb zenon_Vxkb)
% 257.77/258.09  (-. (p1011 zenon_Vkva))
% 257.77/258.09  (-. (p1205 zenon_Vuwc))
% 257.77/258.09  (-. (p105 zenon_Vrcd))
% 257.77/258.09  (-. (p311 zenon_Vjbb))
% 257.77/258.09  (r1 zenon_Vexa zenon_Vfxa)
% 257.77/258.09  (r1 zenon_Vlw zenon_Vnw)
% 257.77/258.09  (-. (p1015 zenon_Vkb))
% 257.77/258.09  (r1 zenon_Vgta zenon_Vhta)
% 257.77/258.09  (-. (p211 zenon_Vycb))
% 257.77/258.09  (-. (p608 zenon_Vsac))
% 257.77/258.09  (r1 zenon_Vjgb zenon_Vkgb)
% 257.77/258.09  (-. (p309 zenon_Vmub))
% 257.77/258.09  (-. (p202 zenon_Vdtd))
% 257.77/258.09  (-. (p108 zenon_Vmgc))
% 257.77/258.09  (-. (p202 zenon_Vzsd))
% 257.77/258.09  (-. (p802 zenon_Vrqd))
% 257.77/258.09  (-. (p515 zenon_Vqf))
% 257.77/258.09  (p801 Tau_0)
% 257.77/258.09  (-. (p513 zenon_Vvda))
% 257.77/258.09  (-. (p303 zenon_Vbnd))
% 257.77/258.09  (-. (p205 zenon_Vzad))
% 257.77/258.09  (-. (p806 zenon_Vcqc))
% 257.77/258.09  (-. (p1106 zenon_Vmpc))
% 257.77/258.09  (-. (p911 zenon_Vgwa))
% 257.77/258.09  (r1 zenon_Vnub zenon_Voub)
% 257.77/258.09  (-. (p715 zenon_Vjd))
% 257.77/258.09  (r1 zenon_Vag zenon_Vcg)
% 257.77/258.09  (r1 zenon_Vmwa zenon_Vnwa)
% 257.77/258.09  (-. (p909 zenon_Vypb))
% 257.77/258.09  (-. (p307 zenon_Vllc))
% 257.77/258.09  (-. (p101 zenon_Vfzd))
% 257.77/258.09  (-. (p114 zenon_Vuw))
% 257.77/258.09  (-. (p315 zenon_Vpi))
% 257.77/258.09  (-. (p1013 zenon_Vtz))
% 257.77/258.09  (r1 zenon_Vskc zenon_Vtkc)
% 257.77/258.09  (-. (p110 zenon_Vvob))
% 257.77/258.09  (r1 zenon_Vomb zenon_Vpmb)
% 257.77/258.09  (-. (p1412 zenon_Vxja))
% 257.77/258.09  (r1 zenon_Vkcc zenon_Vlcc)
% 257.77/258.09  (r1 zenon_Veib zenon_Vfib)
% 257.77/258.09  (-. (p1009 zenon_Vrpb))
% 257.77/258.09  (-. (p314 zenon_Vuu))
% 257.77/258.09  (r1 zenon_Vddd zenon_Vfdd)
% 257.77/258.09  (-. (p1403 zenon_Vtjd))
% 257.77/258.09  (-. (p213 zenon_Veha))
% 257.77/258.09  (-. (p815 zenon_Vtc))
% 257.77/258.09  (r1 zenon_Vgjd zenon_Vhjd)
% 257.77/258.09  (-. (p410 zenon_Vokb))
% 257.77/258.09  (-. (p1009 zenon_Vqpb))
% 257.77/258.09  (r1 zenon_Vjod zenon_Vkod)
% 257.77/258.09  (-. (p114 zenon_Vlx))
% 257.77/258.09  (r1 zenon_Vkk zenon_Vmk)
% 257.77/258.09  (-. (p607 zenon_Vqic))
% 257.77/258.09  (-. (p1201 zenon_Vavd))
% 257.77/258.09  (r1 zenon_Vhm zenon_Vim)
% 257.77/258.09  (r1 zenon_Von zenon_Vqn)
% 257.77/258.09  (-. (p506 zenon_Vqrc))
% 257.77/258.09  (-. (p807 zenon_Veic))
% 257.77/258.09  (-. (p202 zenon_Vitd))
% 257.77/258.09  (-. (p714 zenon_Vyp))
% 257.77/258.09  (-. (p607 zenon_Vwic))
% 257.77/258.09  (r1 zenon_Vamc zenon_Vcmc)
% 257.77/258.09  (-. (p1205 zenon_Vrwc))
% 257.77/258.09  (-. (p113 zenon_Voja))
% 257.77/258.09  (-. (p605 zenon_Vhyc))
% 257.77/258.09  (r1 zenon_Vsib zenon_Vuib)
% 257.77/258.09  (r1 zenon_Vnvc zenon_Vovc)
% 257.77/258.09  (-. (p1013 zenon_Vhz))
% 257.77/258.09  (-. (p110 zenon_Vynb))
% 257.77/258.09  (r1 zenon_Vlod zenon_Vmod)
% 257.77/258.09  (-. (p304 zenon_Vchd))
% 257.77/258.09  (-. (p803 zenon_Vbld))
% 257.77/258.09  (-. (p512 zenon_Vhoa))
% 257.77/258.09  (r1 zenon_Vpb zenon_Vrb)
% 257.77/258.09  (-. (p305 zenon_Vead))
% 257.77/258.09  (r1 zenon_Vcxa zenon_Vdxa)
% 257.77/258.09  (r1 zenon_Vxmc zenon_Vymc)
% 257.77/258.09  (-. (p415 zenon_Vnh))
% 257.77/258.09  (-. (p710 zenon_Vhhb))
% 257.77/258.09  (-. (p304 zenon_Vihd))
% 257.77/258.09  (-. (p414 zenon_Vht))
% 257.77/258.09  (r1 zenon_Vfwc zenon_Vhwc)
% 257.77/258.09  (r1 zenon_Vkp zenon_Vlp)
% 257.77/258.09  (-. (p206 zenon_Vduc))
% 257.77/258.09  (r1 zenon_Vouc zenon_Vpuc)
% 257.77/258.09  (-. (p810 zenon_Vogb))
% 257.77/258.09  (-. (p707 zenon_Vmic))
% 257.77/258.09  (-. (p1014 zenon_Vqn))
% 257.77/258.09  (-. (p405 zenon_Vozc))
% 257.77/258.09  (-. (p310 zenon_Vamb))
% 257.77/258.09  (-. (p305 zenon_Voad))
% 257.77/258.09  (r1 zenon_Vpva zenon_Vqva)
% 257.77/258.09  (-. (p215 zenon_Vxj))
% 257.77/258.09  (r1 zenon_Vlr zenon_Vmr)
% 257.77/258.09  (r1 zenon_Vmla zenon_Vola)
% 257.77/258.09  (r1 zenon_Vpzc zenon_Vqzc)
% 257.77/258.09  (-. (p211 zenon_Vndb))
% 257.77/258.09  (-. (p1206 zenon_Vhpc))
% 257.77/258.09  (r1 zenon_Vttb zenon_Vutb)
% 257.77/258.09  (-. (p1010 zenon_Vufb))
% 257.77/258.09  (r1 zenon_Vbjc zenon_Vcjc)
% 257.77/258.09  (r1 zenon_Vetc zenon_Vftc)
% 257.77/258.09  (-. (p313 zenon_Vega))
% 257.77/258.09  (r1 zenon_Vihb zenon_Vjhb)
% 257.77/258.09  (-. (p114 zenon_Vix))
% 257.77/258.09  (r1 zenon_Vaaa zenon_Vbaa)
% 257.77/258.09  (r1 zenon_Vyj zenon_Vak)
% 257.77/258.09  (-. (p303 zenon_Vdnd))
% 257.77/258.09  (r1 zenon_Vnba zenon_Vpba)
% 257.77/258.09  (-. (p206 zenon_Vruc))
% 257.77/258.09  (-. (p103 zenon_Vmod))
% 257.77/258.09  (r1 zenon_Vbnc zenon_Vcnc)
% 257.77/258.09  (-. (p1012 zenon_Vuka))
% 257.77/258.09  (-. (p1415 zenon_Vq))
% 257.77/258.09  (-. (p803 zenon_Vzkd))
% 257.77/258.09  (-. (p109 zenon_Vpxb))
% 257.77/258.09  (-. (p414 zenon_Vtt))
% 257.77/258.09  (-. (p1213 zenon_Vsy))
% 257.77/258.09  (r1 zenon_Vkkc zenon_Vlkc)
% 257.77/258.09  (-. (p1105 zenon_Vywc))
% 257.77/258.09  (-. (p402 zenon_Vesd))
% 257.77/258.09  (-. (p312 zenon_Vsqa))
% 257.77/258.09  (r1 zenon_Vhvc zenon_Vivc)
% 257.77/258.09  (-. (p108 zenon_Vpgc))
% 257.77/258.09  (-. (p107 zenon_Vuoc))
% 257.77/258.09  (-. (p514 zenon_Vxr))
% 257.77/258.09  (r1 zenon_Vyeb zenon_Vafb)
% 257.77/258.09  (-. (p1304 zenon_Vndd))
% 257.77/258.09  (r1 zenon_Viz zenon_Vjz)
% 257.77/258.09  (-. (p611 zenon_Vaya))
% 257.77/258.09  (r1 zenon_Vvl zenon_Vxl)
% 257.77/258.09  (-. (p106 zenon_Vhwc))
% 257.77/258.09  (r1 zenon_Vju zenon_Vlu)
% 257.77/258.09  (-. (p909 zenon_Vaqb))
% 257.77/258.09  (-. (p615 zenon_Vle))
% 257.77/258.09  (r1 zenon_Vzbd zenon_Vbcd)
% 257.77/258.09  (r1 zenon_Vvzb zenon_Vwzb)
% 257.77/258.09  (-. (p208 zenon_Voec))
% 257.77/258.09  (-. (p108 zenon_Vdgc))
% 257.77/258.09  (r1 zenon_Vfwa zenon_Vgwa)
% 257.77/258.09  (-. (p209 zenon_Vbwb))
% 257.77/258.09  (-. (p208 zenon_Vifc))
% 257.77/258.09  (-. (p210 zenon_Vjmb))
% 257.77/258.09  (r1 zenon_Vnk zenon_Vok)
% 257.77/258.09  (-. (p511 zenon_Vgza))
% 257.77/258.09  (-. (p210 zenon_Vgnb))
% 257.77/258.09  (-. (p1510 zenon_Vefb))
% 257.77/258.09  (-. (p613 zenon_Vhca))
% 257.77/258.09  (r1 zenon_Vxhd zenon_Vyhd)
% 257.77/258.09  (r1 zenon_Vvib zenon_Vwib)
% 257.77/258.09  (-. (p211 zenon_Vbdb))
% 257.77/258.09  (r1 zenon_Vlm zenon_Vmm)
% 257.77/258.09  (-. (p713 zenon_Vvba))
% 257.77/258.09  (-. (p509 zenon_Vbtb))
% 257.77/258.09  (-. (p1401 zenon_Vsud))
% 257.77/258.09  (r1 zenon_Vcjd zenon_Vdjd)
% 257.77/258.09  (-. (p504 zenon_Vvfd))
% 257.77/258.09  (-. (p608 zenon_Vmac))
% 257.77/258.09  (-. (p1105 zenon_Vxwc))
% 257.77/258.09  (r1 zenon_Vgc zenon_Vhc)
% 257.77/258.09  (-. (p213 zenon_Vqha))
% 257.77/258.09  (-. (p602 zenon_Vkrd))
% 257.77/258.09  (r1 zenon_Vjka zenon_Vkka)
% 257.77/258.09  (-. (p106 zenon_Vqvc))
% 257.77/258.09  (-. (p1102 zenon_Vypd))
% 257.77/258.09  (-. (p1002 zenon_Vcqd))
% 257.77/258.09  (r1 zenon_Vdod zenon_Veod)
% 257.77/258.09  (r1 zenon_Vqh zenon_Vrh)
% 257.77/258.09  (-. (p812 zenon_Vbma))
% 257.77/258.09  (-. (p1003 zenon_Vmkd))
% 257.77/258.09  (r1 zenon_Vslb zenon_Vulb)
% 257.77/258.09  (-. (p309 zenon_Vkub))
% 257.77/258.09  (-. (p1305 zenon_Vqwc))
% 257.77/258.09  (-. (p509 zenon_Vvsb))
% 257.77/258.09  (-. (p1306 zenon_Vbpc))
% 257.77/258.09  (r1 zenon_Vauc zenon_Vbuc)
% 257.77/258.09  (-. (p615 zenon_Vie))
% 257.77/258.09  (-. (p610 zenon_Vrib))
% 257.77/258.09  (-. (p502 zenon_Vsrd))
% 257.77/258.09  (r1 zenon_Vvb zenon_Vxb)
% 257.77/258.09  (-. (p813 zenon_Vsaa))
% 257.77/258.09  (-. (p513 zenon_Vyda))
% 257.77/258.09  (-. (p612 zenon_Vmna))
% 257.77/258.09  (r1 zenon_Vuwa zenon_Vvwa)
% 257.77/258.09  (-. (p614 zenon_Vnq))
% 257.77/258.09  (r1 zenon_Vpl zenon_Vrl)
% 257.77/258.09  (-. (p706 zenon_Vmqc))
% 257.77/258.09  (r1 zenon_Vrsa zenon_Vtsa)
% 257.77/258.09  (r1 zenon_Vqv zenon_Vsv)
% 257.77/258.09  (p1201 Tau_0)
% 257.77/258.09  (r1 zenon_Vlf zenon_Vnf)
% 257.77/258.09  (-. (p1410 zenon_Vffb))
% 257.77/258.09  (-. (p210 zenon_Vdnb))
% 257.77/258.09  (-. (p908 zenon_Vgzb))
% 257.77/258.09  (-. (p303 zenon_Vzmd))
% 257.77/258.09  (r1 zenon_Vbdc zenon_Vcdc)
% 257.77/258.09  (-. (p105 zenon_Vpcd))
% 257.77/258.09  (r1 zenon_Viha zenon_Vkha)
% 257.77/258.09  (r1 zenon_Vycd zenon_Vzcd)
% 257.77/258.09  (-. (p703 zenon_Vgld))
% 257.77/258.09  (-. (p107 zenon_Vwnc))
% 257.77/258.09  (r1 zenon_Vwz zenon_Vxz)
% 257.77/258.09  (r1 zenon_Vfud zenon_Vgud)
% 257.77/258.09  (-. (p408 zenon_Vadc))
% 257.77/258.09  (-. (p205 zenon_Vfbd))
% 257.77/258.09  (-. (p603 zenon_Vrld))
% 257.77/258.09  (r1 zenon_Vkz zenon_Vlz)
% 257.77/258.09  (-. (p304 zenon_Vogd))
% 257.77/258.09  (r1 zenon_Vatc zenon_Vbtc)
% 257.77/258.09  (r1 zenon_Vohb zenon_Vphb)
% 257.77/258.09  (-. (p512 zenon_Vbpa))
% 257.77/258.09  (-. (p809 zenon_Vmqb))
% 257.77/258.09  (-. (p210 zenon_Vnmb))
% 257.77/258.09  (-. (p1101 zenon_Vfvd))
% 257.77/258.09  (p1111 zenon_Vgva)
% 257.77/258.09  (-. (p110 zenon_Vgob))
% 257.77/258.09  (r1 zenon_Vdrb zenon_Verb)
% 257.77/258.09  (-. (p301 zenon_Vsxd))
% 257.77/258.09  (-. (p410 zenon_Vukb))
% 257.77/258.09  (-. (p203 zenon_Vond))
% 257.77/258.09  (-. (p609 zenon_Vzrb))
% 257.77/258.09  (r1 zenon_Vbub zenon_Vdub)
% 257.77/258.09  (-. (p305 zenon_Vaad))
% 257.77/258.09  (-. (p411 zenon_Vxza))
% 257.77/258.09  (-. (p1307 zenon_Vbhc))
% 257.77/258.09  (r1 zenon_Vmq zenon_Vnq)
% 257.77/258.09  (r1 zenon_Vrz zenon_Vtz)
% 257.77/258.09  (-. (p704 zenon_Vted))
% 257.77/258.09  (-. (p109 zenon_Vvxb))
% 257.77/258.09  (r1 zenon_Vjsc zenon_Vksc)
% 257.77/258.09  (-. (p1205 zenon_Vtwc))
% 257.77/258.09  (-. (p402 zenon_Vbsd))
% 257.77/258.09  (-. (p403 zenon_Vhmd))
% 257.77/258.09  (-. (p704 zenon_Vued))
% 257.77/258.09  (r1 zenon_Vhkb zenon_Vikb)
% 257.77/258.09  (p601 Tau_0)
% 257.77/258.09  (-. (p505 zenon_Vuyc))
% 257.77/258.09  (r1 zenon_Vjzc zenon_Vkzc)
% 257.77/258.09  (r1 zenon_Vzva zenon_Vawa)
% 257.77/258.09  (-. (p1308 zenon_Vkyb))
% 257.77/258.09  (-. (p401 zenon_Vfxd))
% 257.77/258.09  (r1 zenon_Vlwb zenon_Vnwb)
% 257.77/258.09  (r1 zenon_Vmmb zenon_Vnmb)
% 257.77/258.09  (-. (p201 zenon_Vlyd))
% 257.77/258.09  (-. (p413 zenon_Vyea))
% 257.77/258.09  (r1 zenon_Ved zenon_Vgd)
% 257.77/258.09  (-. (p409 zenon_Vutb))
% 257.77/258.09  (r1 zenon_Vzgb zenon_Vahb)
% 257.77/258.09  (r1 zenon_Vrqa zenon_Vsqa)
% 257.77/258.09  (-. (p311 zenon_Vacb))
% 257.77/258.09  (-. (p608 zenon_Vbbc))
% 257.77/258.09  (-. (p609 zenon_Vxrb))
% 257.77/258.09  (-. (p402 zenon_Vhsd))
% 257.77/258.09  (r1 zenon_Vvdb zenon_Vwdb)
% 257.77/258.09  (r1 zenon_Vznc zenon_Vaoc)
% 257.77/258.09  (r1 zenon_Vbad zenon_Vcad)
% 257.77/258.09  (-. (p104 zenon_Vljd))
% 257.77/258.09  (-. (p414 zenon_Vos))
% 257.77/258.09  (-. (p205 zenon_Vbcd))
% 257.77/258.09  (-. (p104 zenon_Vojd))
% 257.77/258.09  (r1 zenon_Vpx zenon_Vrx)
% 257.77/258.09  (-. (p112 zenon_Vhta))
% 257.77/258.09  (r1 zenon_Vng zenon_Vpg)
% 257.77/258.09  (-. (p912 zenon_Vfla))
% 257.77/258.09  (-. (p412 zenon_Vjpa))
% 257.77/258.09  (-. (p401 zenon_Vnxd))
% 257.77/258.09  (-. (p104 zenon_Vjjd))
% 257.77/258.09  (-. (p615 zenon_Vce))
% 257.77/258.09  (-. (p1405 zenon_Vmwc))
% 257.77/258.09  (r1 zenon_Vmcd zenon_Vncd)
% 257.77/258.09  (-. (p909 zenon_Vxpb))
% 257.77/258.09  (-. (p107 zenon_Vsnc))
% 257.77/258.09  (-. (p512 zenon_Vhpa))
% 257.77/258.09  (r1 zenon_Vxec zenon_Vzec)
% 257.77/258.09  (-. (p605 zenon_Vnyc))
% 257.77/258.09  (-. (p914 zenon_Vao))
% 257.77/258.09  (-. (p606 zenon_Vyqc))
% 257.77/258.09  (r1 zenon_Vlma zenon_Vmma)
% 257.77/258.09  (-. (p705 zenon_Vyxc))
% 257.77/258.09  (r1 zenon_Vnma zenon_Voma)
% 257.77/258.09  (r1 zenon_Vxzb zenon_Vyzb)
% 257.77/258.09  (r1 zenon_Vzcb zenon_Vbdb)
% 257.77/258.09  (r1 zenon_Vhnb zenon_Vjnb)
% 257.77/258.09  (-. (p107 zenon_Vloc))
% 257.77/258.09  (-. (p104 zenon_Vrid))
% 257.77/258.09  (r1 zenon_Vsb zenon_Vub)
% 257.77/258.09  (r1 zenon_Voab zenon_Vqab)
% 257.77/258.09  (-. (p708 zenon_Veac))
% 257.77/258.09  (-. (p1504 zenon_Vjdd))
% 257.77/258.09  (r1 zenon_Vgg zenon_Vhg)
% 257.77/258.09  (-. (p1114 zenon_Vxm))
% 257.77/258.09  (-. (p106 zenon_Vsvc))
% 257.77/258.09  (-. (p1110 zenon_Vqfb))
% 257.77/258.09  (-. (p1202 zenon_Vspd))
% 257.77/258.09  (-. (p1114 zenon_Vzm))
% 257.77/258.09  (r1 zenon_Vpe zenon_Vre)
% 257.77/258.09  (r1 zenon_Vge zenon_Vie)
% 257.77/258.09  (r1 zenon_Vbfb zenon_Vdfb)
% 257.77/258.09  (r1 zenon_Vtnc zenon_Vunc)
% 257.77/258.09  (-. (p111 zenon_Vdfb))
% 257.77/258.09  (-. (p705 zenon_Vvxc))
% 257.77/258.09  (-. (p806 zenon_Vfqc))
% 257.77/258.09  (-. (p708 zenon_Vgac))
% 257.77/258.09  (-. (p815 zenon_Vfc))
% 257.77/258.09  (r1 zenon_Vkd zenon_Vmd)
% 257.77/258.09  (-. (p211 zenon_Vqcb))
% 257.77/258.09  (-. (p103 zenon_Vipd))
% 257.77/258.09  (-. (p414 zenon_Vqt))
% 257.77/258.09  (r1 zenon_Vyrb zenon_Vzrb)
% 257.77/258.09  (-. (p312 zenon_Vwqa))
% 257.77/258.09  (r1 zenon_Vbmb zenon_Vdmb)
% 257.77/258.09  (r1 zenon_Veca zenon_Vfca)
% 257.77/258.09  (-. (p314 zenon_Vlu))
% 257.77/258.09  (-. (p503 zenon_Vdmd))
% 257.77/258.09  (-. (p613 zenon_Vdca))
% 257.77/258.09  (-. (p304 zenon_Vygd))
% 257.77/258.09  (-. (p502 zenon_Vvrd))
% 257.77/258.09  (-. (p915 zenon_Vob))
% 257.77/258.09  (r1 zenon_Vxsa zenon_Vzsa)
% 257.77/258.09  (-. (p510 zenon_Vrjb))
% 257.77/258.09  (-. (p1512 zenon_Vvja))
% 257.77/258.09  (-. (p602 zenon_Vhrd))
% 257.77/258.09  (-. (p313 zenon_Vtga))
% 257.77/258.09  (-. (p206 zenon_Vcvc))
% 257.77/258.09  (-. (p1012 zenon_Vyka))
% 257.77/258.09  (-. (p304 zenon_Vehd))
% 257.77/258.09  (r1 zenon_Vzod zenon_Vapd)
% 257.77/258.09  (-. (p101 zenon_Vzyd))
% 257.77/258.09  (-. (p114 zenon_Vzw))
% 257.77/258.09  (-. (p208 zenon_Vkec))
% 257.77/258.09  (-. (p204 zenon_Veid))
% 257.77/258.09  (-. (p504 zenon_Vmfd))
% 257.77/258.09  (r1 zenon_Volc zenon_Vplc)
% 257.77/258.09  (r1 zenon_Vsuc zenon_Vtuc)
% 257.77/258.09  (-. (p111 zenon_Vreb))
% 257.77/258.09  (r1 zenon_Vxjb zenon_Vyjb)
% 257.77/258.09  (-. (p1406 zenon_Vzoc))
% 257.77/258.09  (-. (p907 zenon_Vthc))
% 257.77/258.09  (r1 zenon_Vtoa zenon_Vvoa)
% 257.77/258.09  (-. (p802 zenon_Vqqd))
% 257.77/258.09  (-. (p412 zenon_Vjqa))
% 257.77/258.09  (-. (p513 zenon_Vfda))
% 257.77/258.09  (r1 zenon_Vrna zenon_Vtna)
% 257.77/258.09  (-. (p1001 zenon_Vjvd))
% 257.77/258.09  (-. (p315 zenon_Vrh))
% 257.77/258.09  (p901 Tau_0)
% 257.77/258.09  (r1 zenon_Vnb zenon_Vob)
% 257.77/258.09  (-. (p708 zenon_Vwzb))
% 257.77/258.09  (r1 zenon_Vni zenon_Vpi)
% 257.77/258.09  (-. (p112 zenon_Vtua))
% 257.77/258.09  (r1 zenon_Vkuc zenon_Vluc)
% 257.77/258.09  (-. (p1002 zenon_Vfqd))
% 257.77/258.09  (r1 zenon_Vbqa zenon_Vdqa)
% 257.77/258.09  (-. (p415 zenon_Vjg))
% 257.77/258.09  (-. (p713 zenon_Vgba))
% 257.77/258.09  (-. (p606 zenon_Vvqc))
% 257.77/258.09  (-. (p1107 zenon_Vjhc))
% 257.77/258.09  (r1 zenon_Vknb zenon_Vmnb)
% 257.77/258.09  (-. (p914 zenon_Vyn))
% 257.77/258.09  (-. (p305 zenon_Vmad))
% 257.77/258.09  (r1 zenon_Vxnd zenon_Vynd)
% 257.77/258.09  (r1 zenon_Vlh zenon_Vnh)
% 257.77/258.09  (-. (p415 zenon_Vpg))
% 257.77/258.09  (r1 zenon_Vft zenon_Vht)
% 257.77/258.09  (-. (p213 zenon_Vbha))
% 257.77/258.09  (r1 zenon_Vgmb zenon_Vhmb)
% 257.77/258.09  (-. (p809 zenon_Viqb))
% 257.77/258.09  (r1 zenon_Vnka zenon_Voka)
% 257.77/258.09  (r1 zenon_Vgbd zenon_Vhbd)
% 257.77/258.09  (r1 zenon_Vrxa zenon_Vtxa)
% 257.77/258.09  (-. (p201 zenon_Veyd))
% 257.77/258.09  (r1 zenon_Vkla zenon_Vlla)
% 257.77/258.09  (r1 zenon_Vptb zenon_Vqtb)
% 257.77/258.09  (-. (p311 zenon_Vgcb))
% 257.77/258.09  (-. (p701 zenon_Vcwd))
% 257.77/258.09  (-. (p705 zenon_Vcyc))
% 257.77/258.09  (-. (p102 zenon_Votd))
% 257.77/258.09  (r1 zenon_Vnca zenon_Vpca)
% 257.77/258.09  (-. (p403 zenon_Vomd))
% 257.77/258.09  (r1 zenon_Vpfa zenon_Vqfa)
% 257.77/258.09  (-. (p1112 zenon_Vgka))
% 257.77/258.09  (-. (p403 zenon_Vqmd))
% 257.77/258.09  (-. (p814 zenon_Vxo))
% 257.77/258.09  (r1 zenon_Vtxb zenon_Vvxb)
% 257.77/258.09  (-. (p409 zenon_Vdub))
% 257.77/258.09  (-. (p106 zenon_Vewc))
% 257.77/258.09  (-. (p215 zenon_Vmk))
% 257.77/258.09  (r1 zenon_Vgvb zenon_Vivb)
% 257.77/258.09  (p1301 Tau_0)
% 257.77/258.09  (r1 zenon_Vzvc zenon_Vbwc)
% 257.77/258.09  (-. (p211 zenon_Vocb))
% 257.77/258.09  (-. (p907 zenon_Vxhc))
% 257.77/258.09  (r1 zenon_Vvqa zenon_Vwqa)
% 257.77/258.09  (-. (p515 zenon_Vcf))
% 257.77/258.09  (r1 zenon_Vhhd zenon_Vihd)
% 257.77/258.09  (-. (p211 zenon_Vhdb))
% 257.77/258.09  (-. (p907 zenon_Vvhc))
% 257.77/258.09  (-. (p601 zenon_Vtwd))
% 257.77/258.09  (-. (p103 zenon_Vkod))
% 257.77/258.09  (r1 zenon_Vbe zenon_Vce)
% 257.77/258.09  (r1 zenon_Vad zenon_Vbd)
% 257.77/258.09  (r1 zenon_Vida zenon_Vjda)
% 257.77/258.09  (r1 zenon_Vzya zenon_Vaza)
% 257.77/258.09  (-. (p1108 zenon_Vpyb))
% 257.77/258.09  (r1 zenon_Vtzc zenon_Vuzc)
% 257.77/258.09  (r1 zenon_Vjnc zenon_Vlnc)
% 257.77/258.09  (r1 zenon_Vmeb zenon_Voeb)
% 257.77/258.09  (-. (p406 zenon_Vyrc))
% 257.77/258.09  (-. (p503 zenon_Vyld))
% 257.77/258.09  (r1 zenon_Vrc zenon_Vtc)
% 257.77/258.09  (r1 zenon_Vrk zenon_Vtk)
% 257.77/258.09  (r1 zenon_Vrvc zenon_Vsvc)
% 257.77/258.09  (-. (p115 zenon_Vxl))
% 257.77/258.09  (-. (p1411 zenon_Vwua))
% 257.77/258.09  (r1 zenon_Vcxb zenon_Vdxb)
% 257.77/258.09  (-. (p211 zenon_Vvcb))
% 257.77/258.09  (-. (p207 zenon_Vqmc))
% 257.77/258.09  (-. (p503 zenon_Vcmd))
% 257.77/258.09  (-. (p801 zenon_Vwvd))
% 257.77/258.09  (-. (p114 zenon_Vrx))
% 257.77/258.09  (-. (p307 zenon_Vhlc))
% 257.77/258.09  (-. (p715 zenon_Vyd))
% 257.77/258.09  (-. (p1115 zenon_Voa))
% 257.77/258.09  (-. (p1313 zenon_Vmy))
% 257.77/258.09  (-. (p607 zenon_Vsic))
% 257.77/258.09  (-. (p405 zenon_Vuzc))
% 257.77/258.09  (-. (p201 zenon_Vryd))
% 257.77/258.09  (-. (p807 zenon_Vdic))
% 257.77/258.09  (-. (p706 zenon_Voqc))
% 257.77/258.09  (-. (p704 zenon_Vafd))
% 257.77/258.09  (r1 zenon_Vdl zenon_Vfl)
% 257.77/258.09  (r1 zenon_Vhad zenon_Viad)
% 257.77/258.09  (r1 zenon_Vyl zenon_Vam)
% 257.77/258.09  (-. (p212 zenon_Vyra))
% 257.77/258.09  (-. (p911 zenon_Vjwa))
% 257.77/258.09  (-. (p514 zenon_Vur))
% 257.77/258.09  (-. (p1012 zenon_Vbla))
% 257.77/258.09  (-. (p110 zenon_Vonb))
% 257.77/258.09  (-. (p1006 zenon_Vppc))
% 257.77/258.09  (r1 zenon_Vafc zenon_Vcfc)
% 257.77/258.09  (-. (p901 zenon_Vovd))
% 257.77/258.09  (r1 zenon_Vyad zenon_Vzad)
% 257.77/258.09  (r1 zenon_Vqea zenon_Vsea)
% 257.77/258.09  (-. (p214 zenon_Vpv))
% 257.77/258.09  (-. (p111 zenon_Vafb))
% 257.77/258.09  (-. (p211 zenon_Vkdb))
% 257.77/258.09  (r1 zenon_Vfba zenon_Vgba)
% 257.77/258.09  (-. (p1415 zenon_Vo))
% 257.77/258.09  (r1 zenon_Vfpd zenon_Vgpd)
% 257.77/258.09  (-. (p1202 zenon_Vvpd))
% 257.77/258.09  (-. (p110 zenon_Vsob))
% 257.77/258.09  (-. (p501 zenon_Vexd))
% 257.77/258.09  (r1 zenon_Vehb zenon_Vfhb)
% 257.77/258.09  (-. (p113 zenon_Vfja))
% 257.77/258.09  (r1 zenon_Vcwb zenon_Vewb)
% 257.77/258.09  (-. (p212 zenon_Vtsa))
% 257.77/258.09  (r1 zenon_Vmsb zenon_Vnsb)
% 257.77/258.09  (-. (p209 zenon_Vnvb))
% 257.77/258.09  (r1 zenon_Voua zenon_Vqua)
% 257.77/258.09  (r1 zenon_Vkbb zenon_Vlbb)
% 257.77/258.09  (-. (p1008 zenon_Vzyb))
% 257.77/258.09  (-. (p811 zenon_Vrwa))
% 257.77/258.09  (-. (p201 zenon_Vkyd))
% 257.77/258.09  (r1 zenon_Voq zenon_Vqq)
% 257.77/258.09  (-. (p606 zenon_Vzqc))
% 257.77/258.09  (p1111 zenon_Vhva)
% 257.77/258.09  (r1 zenon_Vrfa zenon_Vsfa)
% 257.77/258.09  (-. (p210 zenon_Vpmb))
% 257.77/258.09  (-. (p413 zenon_Vkea))
% 257.77/258.09  (p701 Tau_0)
% 257.77/258.09  (-. (p405 zenon_Vwzc))
% 257.77/258.09  (-. (p313 zenon_Vyfa))
% 257.77/258.09  (r1 zenon_Vmj zenon_Voj)
% 257.77/258.09  (-. (p614 zenon_Vir))
% 257.77/258.09  (-. (p714 zenon_Vbq))
% 257.77/258.09  (r1 zenon_Vctb zenon_Vetb)
% 257.77/258.09  (-. (p107 zenon_Vync))
% 257.77/258.09  (r1 zenon_Vyma zenon_Vana)
% 257.77/258.09  (r1 zenon_Vljc zenon_Vmjc)
% 257.77/258.09  (-. (p412 zenon_Vaqa))
% 257.77/258.09  (r1 zenon_Vhgb zenon_Vigb)
% 257.77/258.09  (r1 zenon_Vaoa zenon_Vcoa)
% 257.77/258.09  (r1 zenon_Vyza zenon_Vzza)
% 257.77/258.09  (-. (p1001 zenon_Vivd))
% 257.77/258.09  (-. (p1001 zenon_Vkvd))
% 257.77/258.09  (r1 zenon_Vjra zenon_Vlra)
% 257.77/258.09  (r1 zenon_Vdjb zenon_Vejb)
% 257.77/258.09  (-. (p206 zenon_Vnuc))
% 257.77/258.09  (-. (p901 zenon_Vpvd))
% 257.77/258.09  (r1 zenon_Vwkc zenon_Vxkc)
% 257.77/258.09  (-. (p707 zenon_Vkic))
% 257.77/258.09  (-. (p402 zenon_Vfsd))
% 257.77/258.09  (-. (p613 zenon_Vyca))
% 257.77/258.09  (-. (p107 zenon_Vooc))
% 257.77/258.09  (-. (p412 zenon_Vupa))
% 257.77/258.09  (r1 zenon_Vkza zenon_Vmza)
% 257.77/258.09  (-. (p612 zenon_Vkna))
% 257.77/258.09  (-. (p1212 zenon_Vcka))
% 257.77/258.09  (r1 zenon_Vwba zenon_Vyba)
% 257.77/258.09  (-. (p111 zenon_Vueb))
% 257.77/258.09  (r1 zenon_Vzea zenon_Vbfa)
% 257.77/258.09  (-. (p1009 zenon_Vppb))
% 257.77/258.09  (-. (p215 zenon_Vrj))
% 257.77/258.09  (-. (p415 zenon_Vsg))
% 257.77/258.09  (r1 zenon_Vhec zenon_Viec)
% 257.77/258.09  (-. (p914 zenon_Vio))
% 257.77/258.09  (-. (p1309 zenon_Vepb))
% 257.77/258.09  (-. (p114 zenon_Vdy))
% 257.77/258.09  (-. (p207 zenon_Vymc))
% 257.77/258.09  (-. (p701 zenon_Vfwd))
% 257.77/258.09  (r1 zenon_Vgbb zenon_Vhbb)
% 257.77/258.09  (-. (p207 zenon_Vumc))
% 257.77/258.09  (-. (p402 zenon_Vlsd))
% 257.77/258.09  (r1 zenon_Vcw zenon_Vew)
% 257.77/258.09  (r1 zenon_Vnfa zenon_Vofa)
% 257.77/258.09  (r1 zenon_Vdoa zenon_Vfoa)
% 257.77/258.09  (-. (p703 zenon_Vdld))
% 257.77/258.09  (-. (p210 zenon_Vhmb))
% 257.77/258.09  (-. (p801 zenon_Vzvd))
% 257.77/258.09  (-. (p712 zenon_Voma))
% 257.77/258.09  (r1 zenon_Vglc zenon_Vhlc)
% 257.77/258.09  (-. (p615 zenon_Vre))
% 257.77/258.09  (r1 zenon_Vnxb zenon_Vpxb)
% 257.77/258.09  (-. (p604 zenon_Vhfd))
% 257.77/258.09  (r1 zenon_Vaab zenon_Vbab)
% 257.77/258.09  (-. (p911 zenon_Vwva))
% 257.77/258.09  (-. (p214 zenon_Vyv))
% 257.77/258.09  (r1 zenon_Vxva zenon_Vyva)
% 257.77/258.09  (-. (p913 zenon_Vbaa))
% 257.77/258.09  (r1 zenon_Vrwb zenon_Vtwb)
% 257.77/258.09  (-. (p903 zenon_Vnkd))
% 257.77/258.09  (r1 zenon_Vbzc zenon_Vczc)
% 257.77/258.09  (r1 zenon_Vecd zenon_Vfcd)
% 257.77/258.09  (r1 zenon_Voc zenon_Vqc)
% 257.77/258.09  (-. (p205 zenon_Vhbd))
% 257.77/258.09  (-. (p202 zenon_Vltd))
% 257.77/258.09  (-. (p912 zenon_Vhla))
% 257.77/258.09  (r1 zenon_Vaja zenon_Vcja)
% 257.77/258.09  (r1 zenon_Vpec zenon_Vqec)
% 257.77/258.09  (r1 zenon_Vjkb zenon_Vlkb)
% 257.77/258.09  (-. (p206 zenon_Vjuc))
% 257.77/258.09  (r1 zenon_Vn zenon_Vo)
% 257.77/258.09  (r1 zenon_Vxa zenon_Vya)
% 257.77/258.09  (-. (p710 zenon_Vnhb))
% 257.77/258.09  (-. (p1102 zenon_Vaqd))
% 257.77/258.09  (-. (p1105 zenon_Vwwc))
% 257.77/258.09  (-. (p107 zenon_Vgoc))
% 257.77/258.09  (r1 zenon_Vjgd zenon_Vkgd)
% 257.77/258.09  (-. (p605 zenon_Vfyc))
% 257.77/258.09  (-. (p405 zenon_Vszc))
% 257.77/258.09  (r1 zenon_Vsj zenon_Vuj)
% 257.77/258.09  (r1 zenon_Vuuc zenon_Vwuc)
% 257.77/258.09  (r1 zenon_Vvo zenon_Vxo)
% 257.77/258.09  (r1 zenon_Vcwc zenon_Vewc)
% 257.77/258.09  (-. (p506 zenon_Vorc))
% 257.77/258.09  (-. (p1303 zenon_Vvjd))
% 257.77/258.09  (-. (p108 zenon_Vzfc))
% 257.77/258.09  (-. (p714 zenon_Vnp))
% 257.77/258.09  (-. (p1210 zenon_Vnfb))
% 257.77/258.09  (-. (p113 zenon_Vuja))
% 257.77/258.09  (r1 zenon_Vpud zenon_Vqud)
% 257.77/258.09  (-. (p710 zenon_Vxhb))
% 257.77/258.09  (r1 zenon_Vuga zenon_Vvga)
% 257.77/258.09  (r1 zenon_Vywb zenon_Vzwb)
% 257.77/258.09  (-. (p412 zenon_Vrpa))
% 257.77/258.09  (-. (p207 zenon_Vwmc))
% 257.77/258.09  (-. (p1508 zenon_Vfyb))
% 257.77/258.09  (-. (p1215 zenon_Vea))
% 257.77/258.09  (-. (p606 zenon_Varc))
% 257.77/258.09  (-. (p501 zenon_Vywd))
% 257.77/258.09  (p501 Tau_0)
% 257.77/258.09  (r1 zenon_Vnad zenon_Voad)
% 257.77/258.09  (-. (p310 zenon_Vdmb))
% 257.77/258.09  (-. (p1001 zenon_Vgvd))
% 257.77/258.09  (-. (p814 zenon_Vuo))
% 257.77/258.09  (-. (p210 zenon_Vumb))
% 257.77/258.09  (-. (p1003 zenon_Vkkd))
% 257.77/258.09  (r1 zenon_Vch zenon_Veh)
% 257.77/258.09  (r1 zenon_Valb zenon_Vblb)
% 257.77/258.09  (-. (p603 zenon_Vnld))
% 257.77/258.09  (r1 zenon_Vwd zenon_Vyd)
% 257.77/258.09  (r1 zenon_Vpmc zenon_Vqmc)
% 257.77/258.09  (-. (p114 zenon_Vww))
% 257.77/258.09  (-. (p705 zenon_Vbyc))
% 257.77/258.09  (r1 zenon_Vpnb zenon_Vqnb)
% 257.77/258.09  (-. (p514 zenon_Vds))
% 257.77/258.09  (-. (p1306 zenon_Vdpc))
% 257.77/258.09  (r1 zenon_Vpo zenon_Vqo)
% 257.77/258.09  (-. (p807 zenon_Vaic))
% 257.77/258.09  (r1 zenon_Vwda zenon_Vyda)
% 257.77/258.09  (r1 zenon_Vlba zenon_Vmba)
% 257.77/258.09  (-. (p108 zenon_Vvgc))
% 257.77/258.09  (-. (p1404 zenon_Vldd))
% 257.77/258.09  (-. (p508 zenon_Vwbc))
% 257.77/258.09  (r1 zenon_Vshb zenon_Vuhb)
% 257.77/258.09  (-. (p408 zenon_Vucc))
% 257.77/258.09  (-. (p406 zenon_Vvsc))
% 257.77/258.09  (-. (p114 zenon_Vxx))
% 257.77/258.09  (r1 zenon_Vccd zenon_Vdcd)
% 257.77/258.09  (r1 zenon_Vvzc zenon_Vwzc)
% 257.77/258.09  (r1 zenon_Vma zenon_Voa)
% 257.77/258.09  (-. (p712 zenon_Vsma))
% 257.77/258.09  (-. (p409 zenon_Vxtb))
% 257.77/258.09  (-. (p106 zenon_Vevc))
% 257.77/258.09  (r1 zenon_Vfsc zenon_Vgsc)
% 257.77/258.09  (-. (p806 zenon_Vhqc))
% 257.77/258.09  (r1 zenon_Vtgd zenon_Vugd)
% 257.77/258.09  (-. (p306 zenon_Vrtc))
% 257.77/258.09  (r1 zenon_Vhzc zenon_Vizc)
% 257.77/258.09  (r1 zenon_Vlka zenon_Vmka)
% 257.77/258.09  (r1 zenon_Vgz zenon_Vhz)
% 257.77/258.09  (p1111 zenon_Viva)
% 257.77/258.09  (-. (p603 zenon_Vsld))
% 257.77/258.09  (r1 zenon_Vicd zenon_Vjcd)
% 257.77/258.09  (-. (p812 zenon_Vhma))
% 257.77/258.09  (-. (p407 zenon_Vhkc))
% 257.77/258.09  (r1 zenon_Vvmb zenon_Vxmb)
% 257.77/258.09  (-. (p711 zenon_Vnxa))
% 257.77/258.09  (r1 zenon_Vaa zenon_Vba)
% 257.77/258.09  (-. (p404 zenon_Vcgd))
% 257.77/258.09  (r1 zenon_Vgu zenon_Viu)
% 257.77/258.09  (r1 zenon_Vvec zenon_Vwec)
% 257.77/258.09  (-. (p205 zenon_Vnbd))
% 257.77/258.09  (r1 zenon_Vjo zenon_Vlo)
% 257.77/258.09  (-. (p204 zenon_Vcid))
% 257.77/258.09  (-. (p405 zenon_Vkzc))
% 257.77/258.09  (-. (p612 zenon_Vona))
% 257.77/258.09  (r1 zenon_Vgv zenon_Vhv)
% 257.77/258.09  (r1 zenon_Vzib zenon_Vajb)
% 257.77/258.09  (-. (p810 zenon_Vugb))
% 257.77/258.09  (r1 zenon_Vnsc zenon_Vosc)
% 257.77/258.09  (r1 zenon_Vsx zenon_Vux)
% 257.77/258.09  (-. (p307 zenon_Vfmc))
% 257.77/258.09  (-. (p515 zenon_Vef))
% 257.77/258.09  (-. (p112 zenon_Vlta))
% 257.77/258.09  (r1 zenon_Vtdb zenon_Vudb)
% 257.77/258.09  (-. (p1009 zenon_Vspb))
% 257.77/258.09  (-. (p301 zenon_Vyxd))
% 257.77/258.09  (r1 zenon_Vuc zenon_Vwc)
% 257.77/258.09  (r1 zenon_Vjvc zenon_Vkvc)
% 257.77/258.09  (r1 zenon_Vmu zenon_Vou)
% 257.77/258.09  (r1 zenon_Vdrc zenon_Verc)
% 257.77/258.09  (r1 zenon_Vtob zenon_Vvob)
% 257.77/258.09  (-. (p609 zenon_Vvrb))
% 257.77/258.09  (r1 zenon_Vzdc zenon_Vbec)
% 257.77/258.09  (-. (p111 zenon_Vudb))
% 257.77/258.09  (-. (p403 zenon_Vlmd))
% 257.77/258.09  (r1 zenon_Vvvc zenon_Vwvc)
% 257.77/258.09  (r1 zenon_Vwza zenon_Vxza)
% 257.77/258.09  (-. (p515 zenon_Vfg))
% 257.77/258.09  (-. (p906 zenon_Vtpc))
% 257.77/258.09  (-. (p1008 zenon_Vxyb))
% 257.77/258.09  (-. (p113 zenon_Vtia))
% 257.77/258.09  (-. (p1214 zenon_Vvm))
% 257.77/258.09  (r1 zenon_Vfha zenon_Vhha)
% 257.77/258.09  (-. (p313 zenon_Vmfa))
% 257.77/258.09  (-. (p708 zenon_Vszb))
% 257.77/258.09  (-. (p1408 zenon_Vgyb))
% 257.77/258.09  (-. (p812 zenon_Vzla))
% 257.77/258.09  (-. (p210 zenon_Vmnb))
% 257.77/258.09  (-. (p103 zenon_Vgpd))
% 257.77/258.09  (r1 zenon_Ves zenon_Vgs)
% 257.77/258.09  (-. (p908 zenon_Vazb))
% 257.77/258.09  (-. (p605 zenon_Vmyc))
% 257.77/258.09  (r1 zenon_Vsvb zenon_Vtvb)
% 257.77/258.09  (-. (p101 zenon_Vxyd))
% 257.77/258.09  (r1 zenon_Vbkc zenon_Vckc)
% 257.77/258.09  (-. (p401 zenon_Vpxd))
% 257.77/258.09  (-. (p610 zenon_Vuib))
% 257.77/258.09  (-. (p201 zenon_Vgyd))
% 257.77/258.09  (-. (p406 zenon_Vasc))
% 257.77/258.09  (-. (p315 zenon_Vgi))
% 257.77/258.09  (-. (p101 zenon_Vuyd))
% 257.77/258.09  (-. (p604 zenon_Vdfd))
% 257.77/258.09  (-. (p304 zenon_Vugd))
% 257.77/258.09  (-. (p103 zenon_Vuod))
% 257.77/258.09  (-. (p912 zenon_Vdla))
% 257.77/258.09  (r1 zenon_Vvka zenon_Vwka)
% 257.77/258.09  (r1 zenon_Vooa zenon_Vpoa)
% 257.77/258.09  (r1 zenon_Vyo zenon_Vap)
% 257.77/258.09  (r1 zenon_Vdkc zenon_Vfkc)
% 257.77/258.09  (-. (p915 zenon_Vmb))
% 257.77/258.09  (-. (p913 zenon_Veaa))
% 257.77/258.09  (r1 zenon_Vdu zenon_Vfu)
% 257.77/258.09  (-. (p1004 zenon_Vaed))
% 257.77/258.09  (-. (p1004 zenon_Vced))
% 257.77/258.09  (-. (p706 zenon_Vjqc))
% 257.77/258.09  (-. (p707 zenon_Vlic))
% 257.77/258.09  (-. (p515 zenon_Vzf))
% 257.77/258.09  (-. (p302 zenon_Vmsd))
% 257.77/258.09  (-. (p509 zenon_Vjsb))
% 257.77/258.09  (-. (p1012 zenon_Vqka))
% 257.77/258.09  (-. (p412 zenon_Vgqa))
% 257.77/258.09  (-. (p1108 zenon_Vqyb))
% 257.77/258.09  (r1 zenon_Vdhd zenon_Vehd)
% 257.77/258.09  (-. (p413 zenon_Vgea))
% 257.77/258.09  (-. (p113 zenon_Vrja))
% 257.77/258.09  (r1 zenon_Vkib zenon_Vlib)
% 257.77/258.09  (r1 zenon_Vtva zenon_Vuva)
% 257.77/258.09  (r1 zenon_Vmrb zenon_Vnrb)
% 257.77/258.09  (-. (p711 zenon_Vfxa))
% 257.77/258.09  (-. (p215 zenon_Vlj))
% 257.77/258.09  (r1 zenon_Vucd zenon_Vvcd)
% 257.77/258.09  (r1 zenon_Vmkc zenon_Vnkc)
% 257.77/258.09  (-. (p502 zenon_Vurd))
% 257.77/258.09  (r1 zenon_Vqd zenon_Vsd)
% 257.77/258.09  (r1 zenon_Vsbb zenon_Vubb)
% 257.77/258.09  (r1 zenon_Vjnd zenon_Vknd)
% 257.77/258.09  (r1 zenon_Vrsc zenon_Vssc)
% 257.77/258.09  (-. (p806 zenon_Vdqc))
% 257.77/258.09  (-. (p108 zenon_Vvfc))
% 257.77/258.09  (r1 zenon_Vzp zenon_Vbq)
% 257.77/258.09  (-. (p604 zenon_Vlfd))
% 257.77/258.09  (r1 zenon_Vqoa zenon_Vsoa)
% 257.77/258.09  (-. (p910 zenon_Vcgb))
% 257.77/258.09  (r1 zenon_Vgkc zenon_Vhkc)
% 257.77/258.09  (-. (p314 zenon_Vfu))
% 257.77/258.09  (-. (p806 zenon_Vgqc))
% 257.77/258.09  (-. (p1201 zenon_Vzud))
% 257.77/258.09  (-. (p111 zenon_Vxeb))
% 257.77/258.09  (p1401 Tau_0)
% 257.77/258.09  (-. (p602 zenon_Vmrd))
% 257.77/258.09  (-. (p407 zenon_Vxkc))
% 257.77/258.09  (-. (p306 zenon_Vutc))
% 257.77/258.09  (-. (p1013 zenon_Vlz))
% 257.77/258.09  (-. (p105 zenon_Vlcd))
% 257.77/258.09  (-. (p611 zenon_Vgya))
% 257.77/258.09  (-. (p311 zenon_Vfbb))
% 257.77/258.09  (-. (p910 zenon_Vggb))
% 257.77/258.09  (-. (p905 zenon_Vmxc))
% 257.77/258.09  (r1 zenon_Vxzc zenon_Vyzc)
% 257.77/258.09  (-. (p101 zenon_Vazd))
% 257.77/258.09  (r1 zenon_Vgxb zenon_Vhxb)
% 257.77/258.09  (r1 zenon_Vkia zenon_Vlia)
% 257.77/258.09  (-. (p1301 zenon_Vwud))
% 257.77/258.09  (-. (p1012 zenon_Vska))
% 257.77/258.09  (-. (p802 zenon_Vpqd))
% 257.77/258.09  (-. (p1115 zenon_Vua))
% 257.77/258.09  (r1 zenon_Vvjc zenon_Vwjc)
% 257.77/258.09  (-. (p309 zenon_Vivb))
% 257.77/258.09  (-. (p911 zenon_Vewa))
% 257.77/258.09  (-. (p610 zenon_Vbib))
% 257.77/258.09  (r1 zenon_Vbsc zenon_Vcsc)
% 257.77/258.09  (-. (p907 zenon_Vwhc))
% 257.77/258.09  (r1 zenon_Vejd zenon_Vfjd)
% 257.77/258.09  (-. (p104 zenon_Vhjd))
% 257.77/258.09  (-. (p113 zenon_Vlia))
% 257.77/258.09  (r1 zenon_Vyvb zenon_Vzvb)
% 257.77/258.09  (r1 zenon_Vvma zenon_Vxma)
% 257.77/258.09  (r1 zenon_Vdnc zenon_Vfnc)
% 257.77/258.09  (-. (p904 zenon_Vjed))
% 257.77/258.09  (-. (p912 zenon_Vjla))
% 257.77/258.09  (-. (p203 zenon_Vgnd))
% 257.77/258.09  (-. (p908 zenon_Vczb))
% 257.77/258.09  (r1 zenon_Vqob zenon_Vsob)
% 257.77/258.09  (-. (p1208 zenon_Vnyb))
% 257.77/258.09  (-. (p201 zenon_Voyd))
% 257.77/258.09  (r1 zenon_Vdjc zenon_Vejc)
% 257.77/258.09  (-. (p213 zenon_Vzha))
% 257.77/258.09  (-. (p710 zenon_Vfhb))
% 257.77/258.09  (r1 zenon_Vpjc zenon_Vqjc)
% 257.77/258.09  (-. (p210 zenon_Vanb))
% 257.77/258.09  (r1 zenon_Vxbc zenon_Vzbc)
% 257.77/258.09  (r1 zenon_Vlhd zenon_Vmhd)
% 257.77/258.09  (r1 zenon_Vrw zenon_Vsw)
% 257.77/258.09  (r1 zenon_Vcha zenon_Veha)
% 257.77/258.09  (r1 zenon_Vwfc zenon_Vxfc)
% 257.77/258.09  (r1 zenon_Vib zenon_Vkb)
% 257.77/258.09  (r1 zenon_Vax zenon_Vcx)
% 257.77/258.09  (-. (p111 zenon_Vleb))
% 257.77/258.09  (-. (p607 zenon_Vijc))
% 257.77/258.09  (-. (p110 zenon_Vaob))
% 257.77/258.09  (-. (p106 zenon_Vbwc))
% 257.77/258.09  (r1 zenon_Vof zenon_Vqf)
% 257.77/258.09  (r1 zenon_Vowa zenon_Vpwa)
% 257.77/258.09  (-. (p910 zenon_Vigb))
% 257.77/258.09  (-. (p509 zenon_Vetb))
% 257.77/258.09  (-. (p803 zenon_Vykd))
% 257.77/258.09  (-. (p308 zenon_Vgdc))
% 257.77/258.09  (-. (p301 zenon_Vbyd))
% 257.77/258.09  (-. (p1109 zenon_Vjpb))
% 257.77/258.09  (-. (p515 zenon_Vhf))
% 257.77/258.09  (-. (p404 zenon_Vfgd))
% 257.77/258.09  (r1 zenon_Vjhd zenon_Vkhd)
% 257.77/258.09  (-. (p104 zenon_Vxid))
% 257.77/258.09  (-. (p914 zenon_Vco))
% 257.77/258.09  (-. (p307 zenon_Vcmc))
% 257.77/258.09  (-. (p1101 zenon_Vdvd))
% 257.77/258.09  (r1 zenon_Vkob zenon_Vmob)
% 257.77/258.09  (r1 zenon_Vilb zenon_Vjlb)
% 257.77/258.09  (-. (p404 zenon_Vdgd))
% 257.77/258.09  (-. (p811 zenon_Vnwa))
% 257.77/258.09  (r1 zenon_Vfrb zenon_Vgrb)
% 257.77/258.09  (-. (p707 zenon_Viic))
% 257.77/258.09  (-. (p603 zenon_Vtld))
% 257.77/258.09  (r1 zenon_Vwsc zenon_Vxsc)
% 257.77/258.09  (r1 zenon_Vhrc zenon_Virc)
% 257.77/258.09  (r1 zenon_Vrqb zenon_Vsqb)
% 257.77/258.09  (-. (p608 zenon_Viac))
% 257.77/258.09  (-. (p801 zenon_Vvvd))
% 257.77/258.09  (-. (p104 zenon_Vnid))
% 257.77/258.09  (r1 zenon_Vrka zenon_Vska)
% 257.77/258.09  (-. (p409 zenon_Vaub))
% 257.77/258.09  (-. (p512 zenon_Vvoa))
% 257.77/258.09  (r1 zenon_Vgo zenon_Vio)
% 257.77/258.09  (-. (p214 zenon_Vnw))
% 257.77/258.09  (r1 zenon_Vpla zenon_Vrla)
% 257.77/258.09  (-. (p1114 zenon_Ven))
% 257.77/258.09  (r1 zenon_Vxia zenon_Vzia)
% 257.77/258.09  (-. (p310 zenon_Vllb))
% 257.77/258.09  (r1 zenon_Vhba zenon_Viba)
% 257.77/258.09  (-. (p203 zenon_Vqnd))
% 257.77/258.09  (r1 zenon_Vnr zenon_Vor)
% 257.77/258.09  (r1 zenon_Vntb zenon_Votb)
% 257.77/258.09  (-. (p804 zenon_Vped))
% 257.77/258.09  (r1 zenon_Vhp zenon_Vjp)
% 257.77/258.09  (-. (p501 zenon_Vzwd))
% 257.77/258.09  (-. (p107 zenon_Vaoc))
% 257.77/258.09  (r1 zenon_Vzgd zenon_Vahd)
% 257.77/258.09  (r1 zenon_Vsbc zenon_Vtbc)
% 257.77/258.09  (-. (p1011 zenon_Vuva))
% 257.77/258.09  (-. (p308 zenon_Vqdc))
% 257.77/258.09  (-. (p110 zenon_Vsnb))
% 257.77/258.09  (-. (p711 zenon_Vjxa))
% 257.77/258.09  (r1 zenon_Vorb zenon_Vprb)
% 257.77/258.09  (r1 zenon_Vthd zenon_Vuhd)
% 257.77/258.09  (-. (p102 zenon_Viud))
% 257.77/258.09  (r1 zenon_Vgdd zenon_Vidd)
% 257.77/258.09  (-. (p414 zenon_Vvs))
% 257.77/258.09  (-. (p813 zenon_Voaa))
% 257.77/258.09  (r1 zenon_Vcba zenon_Veba)
% 257.77/258.09  (-. (p113 zenon_Vwia))
% 257.77/258.09  (-. (p1311 zenon_Vyua))
% 257.77/258.09  (r1 zenon_Vksb zenon_Vlsb)
% 257.77/258.09  (r1 zenon_Vric zenon_Vsic)
% 257.77/258.09  (-. (p1109 zenon_Vmpb))
% 257.77/258.09  (r1 zenon_Vpna zenon_Vqna)
% 257.77/258.09  (-. (p407 zenon_Vlkc))
% 257.77/258.09  (-. (p1313 zenon_Vly))
% 257.77/258.09  (r1 zenon_Vzxb zenon_Vbyb)
% 257.77/258.09  (r1 zenon_Vrha zenon_Vtha)
% 257.77/258.09  (r1 zenon_Vpgd zenon_Vqgd)
% 257.77/258.09  (-. (p707 zenon_Vnic))
% 257.77/258.09  (r1 zenon_Vpic zenon_Vqic)
% 257.77/258.09  (-. (p1010 zenon_Vyfb))
% 257.77/258.09  (-. (p1013 zenon_Vnz))
% 257.77/258.09  (-. (p702 zenon_Vbrd))
% 257.77/258.09  (-. (p115 zenon_Vol))
% 257.77/258.09  (r1 zenon_Vwwa zenon_Vywa)
% 257.77/258.09  (-. (p106 zenon_Vmvc))
% 257.77/258.09  (-. (p809 zenon_Voqb))
% 257.77/258.09  (-. (p202 zenon_Vhtd))
% 257.77/258.09  (-. (p104 zenon_Vzid))
% 257.77/258.09  (r1 zenon_Vipa zenon_Vjpa)
% 257.77/258.09  (r1 zenon_Vzg zenon_Vbh)
% 257.77/258.09  (-. (p213 zenon_Vwha))
% 257.77/258.09  (-. (p206 zenon_Vluc))
% 257.77/258.09  (-. (p303 zenon_Vvmd))
% 257.77/258.09  (r1 zenon_Vzjb zenon_Vakb)
% 257.77/258.09  (r1 zenon_Vegc zenon_Vggc)
% 257.77/258.09  (r1 zenon_Vgoa zenon_Vhoa)
% 257.77/258.09  (-. (p612 zenon_Vcoa))
% 257.77/258.09  (-. (p909 zenon_Vwpb))
% 257.77/258.09  (-. (p605 zenon_Vjyc))
% 257.77/258.09  (p1111 zenon_Vfva)
% 257.77/258.09  (-. (p813 zenon_Vbba))
% 257.77/258.09  (-. (p512 zenon_Vyoa))
% 257.77/258.09  (r1 zenon_Vfa zenon_Vha)
% 257.77/258.09  (-. (p512 zenon_Vepa))
% 257.77/258.09  (-. (p913 zenon_Vkaa))
% 257.77/258.09  (-. (p111 zenon_Vfeb))
% 257.77/258.09  (r1 zenon_Vjcb zenon_Vkcb)
% 257.77/258.09  (-. (p1015 zenon_Vwa))
% 257.77/258.09  (-. (p305 zenon_Vuad))
% 257.77/258.09  (-. (p1007 zenon_Vohc))
% 257.77/258.09  (-. (p908 zenon_Vdzb))
% 257.77/258.09  (-. (p410 zenon_Vekb))
% 257.77/258.09  (r1 zenon_Vye zenon_Vaf)
% 257.77/258.09  (-. (p110 zenon_Vunb))
% 257.77/258.09  (r1 zenon_Vobc zenon_Vpbc)
% 257.77/258.09  (-. (p108 zenon_Vtfc))
% 257.77/258.09  (-. (p413 zenon_Vhfa))
% 257.77/258.09  (-. (p1007 zenon_Vmhc))
% 257.77/258.09  (-. (p609 zenon_Vfsb))
% 257.77/258.09  (r1 zenon_Vlzc zenon_Vmzc)
% 257.77/258.09  (r1 zenon_Vvnb zenon_Vwnb)
% 257.77/258.09  (r1 zenon_Vxrc zenon_Vyrc)
% 257.77/258.09  (-. (p702 zenon_Vard))
% 257.77/258.09  (-. (p712 zenon_Vdna))
% 257.77/258.09  (r1 zenon_Vnd zenon_Vpd)
% 257.77/258.09  (r1 zenon_Vzi zenon_Vaj)
% 257.77/258.09  (-. (p513 zenon_Veea))
% 257.77/258.09  (-. (p602 zenon_Vord))
% 257.77/258.09  (-. (p1215 zenon_Vz))
% 257.77/258.09  (-. (p114 zenon_Vox))
% 257.77/258.09  (r1 zenon_Vzwa zenon_Vbxa)
% 257.77/258.09  (-. (p808 zenon_Vlzb))
% 257.77/258.09  (-. (p614 zenon_Vjq))
% 257.77/258.09  (-. (p604 zenon_Vkfd))
% 257.77/258.09  (-. (p212 zenon_Vcta))
% 257.77/258.09  (-. (p503 zenon_Vbmd))
% 257.77/258.09  (-. (p301 zenon_Vtxd))
% 257.77/258.09  (r1 zenon_Vkda zenon_Vmda)
% 257.77/258.09  (-. (p114 zenon_Vgy))
% 257.77/258.09  (r1 zenon_Vtmc zenon_Vumc)
% 257.77/258.09  (-. (p505 zenon_Vpyc))
% 257.77/258.09  (r1 zenon_Vkg zenon_Vmg)
% 257.77/258.09  (-. (p905 zenon_Vhxc))
% 257.77/258.09  (-. (p413 zenon_Vpea))
% 257.77/258.09  (-. (p808 zenon_Vhzb))
% 257.77/258.09  (-. (p805 zenon_Vrxc))
% 257.77/258.09  (-. (p1103 zenon_Vdkd))
% 257.77/258.09  (-. (p302 zenon_Vpsd))
% 257.77/258.09  (-. (p206 zenon_Vztc))
% 257.77/258.09  (-. (p805 zenon_Voxc))
% 257.77/258.09  (-. (p715 zenon_Vdd))
% 257.77/258.09  (r1 zenon_Vbc zenon_Vdc)
% 257.77/258.09  (r1 zenon_Vdad zenon_Vead)
% 257.77/258.09  (r1 zenon_Vhna zenon_Vina)
% 257.77/258.09  (-. (p101 zenon_Vdzd))
% 257.77/258.09  (r1 zenon_Vwob zenon_Vyob)
% 257.77/258.09  (-. (p911 zenon_Vawa))
% 257.77/258.09  (p1111 zenon_Veva)
% 257.77/258.09  (-. (p103 zenon_Vcpd))
% 257.77/258.09  (r1 zenon_Vzyc zenon_Vazc)
% 257.77/258.09  (-. (p1110 zenon_Vpfb))
% 257.77/258.09  (r1 zenon_Vitc zenon_Vjtc)
% 257.77/258.09  (-. (p1008 zenon_Vvyb))
% 257.77/258.09  (-. (p208 zenon_Vgec))
% 257.77/258.09  (-. (p207 zenon_Vonc))
% 257.77/258.09  (r1 zenon_Vtg zenon_Vvg)
% 257.77/258.09  (r1 zenon_Vcma zenon_Vema)
% 257.77/258.09  (-. (p204 zenon_Vshd))
% 257.77/258.09  (-. (p412 zenon_Vmqa))
% 257.77/258.09  (-. (p714 zenon_Vsp))
% 257.77/258.09  (-. (p1103 zenon_Vckd))
% 257.77/258.09  (r1 zenon_Vkq zenon_Vlq)
% 257.77/258.09  (r1 zenon_Vctc zenon_Vdtc)
% 257.77/258.09  (r1 zenon_Veub zenon_Vgub)
% 257.77/258.09  (-. (p109 zenon_Vxwb))
% 257.77/258.09  (r1 zenon_Vdfc zenon_Vffc)
% 257.77/258.09  (-. (p911 zenon_Vcwa))
% 257.77/258.09  (-. (p110 zenon_Vmob))
% 257.77/258.09  (-. (p106 zenon_Vgvc))
% 257.77/258.09  (-. (p308 zenon_Vkdc))
% 257.77/258.09  (-. (p107 zenon_Vcoc))
% 257.77/258.09  (r1 zenon_Vdvb zenon_Vfvb)
% 257.77/258.09  (-. (p508 zenon_Vjbc))
% 257.77/258.09  (-. (p1311 zenon_Vzua))
% 257.77/258.09  (-. (p512 zenon_Vjoa))
% 257.77/258.09  (r1 zenon_Vixa zenon_Vjxa)
% 257.77/258.09  (r1 zenon_Vjdc zenon_Vkdc)
% 257.77/258.09  (r1 zenon_Vcab zenon_Vdab)
% 257.77/258.09  (r1 zenon_Vgab zenon_Vhab)
% 257.77/258.09  (r1 zenon_Vqfc zenon_Vrfc)
% 257.77/258.09  (r1 zenon_Vjoc zenon_Vloc)
% 257.77/258.09  (-. (p1015 zenon_Vya))
% 257.77/258.09  (-. (p507 zenon_Vckc))
% 257.77/258.09  (-. (p1212 zenon_Veka))
% 257.77/258.09  (-. (p1509 zenon_Vzob))
% 257.77/258.09  (-. (p414 zenon_Vys))
% 257.77/258.09  (-. (p311 zenon_Vbbb))
% 257.77/258.09  (-. (p1313 zenon_Vky))
% 257.77/258.09  (r1 zenon_Vmbb zenon_Vobb)
% 257.77/258.09  (-. (p610 zenon_Vdib))
% 257.77/258.09  (-. (p302 zenon_Vssd))
% 257.77/258.09  (-. (p706 zenon_Vpqc))
% 257.77/258.09  (-. (p1209 zenon_Vfpb))
% 257.77/258.09  (-. (p708 zenon_Vaac))
% 257.77/258.09  (r1 zenon_Vebd zenon_Vfbd)
% 257.77/258.09  (-. (p710 zenon_Vrhb))
% 257.77/258.09  (r1 zenon_Vqba zenon_Vsba)
% 257.77/258.09  (r1 zenon_Vgra zenon_Vira)
% 257.77/258.09  (-. (p1211 zenon_Vava))
% 257.77/258.09  (-. (p206 zenon_Vhuc))
% 257.77/258.09  (r1 zenon_Vyt zenon_Vzt)
% 257.77/258.09  (-. (p105 zenon_Vfcd))
% 257.77/258.09  (-. (p404 zenon_Vyfd))
% 257.77/258.09  (r1 zenon_Vym zenon_Vzm)
% 257.77/258.09  (-. (p1005 zenon_Vexc))
% 257.77/258.09  (-. (p312 zenon_Vura))
% 257.77/258.09  (r1 zenon_Viab zenon_Vkab)
% 257.77/258.09  (-. (p301 zenon_Vwxd))
% 257.77/258.09  (r1 zenon_Vjub zenon_Vkub)
% 257.77/258.09  (r1 zenon_Vimb zenon_Vjmb)
% 257.77/258.09  (-. (p101 zenon_Vvyd))
% 257.77/258.09  (-. (p805 zenon_Vtxc))
% 257.77/258.09  (-. (p202 zenon_Vktd))
% 257.77/258.09  (-. (p309 zenon_Vzub))
% 257.77/258.09  (r1 zenon_Vgsb zenon_Vhsb)
% 257.77/258.09  (-. (p804 zenon_Vqed))
% 257.77/258.09  (r1 zenon_Vnud zenon_Voud)
% 257.77/258.09  (r1 zenon_Vqg zenon_Vsg)
% 257.77/258.09  (-. (p414 zenon_Vqs))
% 257.77/258.09  (r1 zenon_Vtza zenon_Vvza)
% 257.77/258.09  (-. (p1011 zenon_Vmva))
% 257.77/258.09  (r1 zenon_Vymb zenon_Vanb)
% 257.77/258.09  (r1 zenon_Vcca zenon_Vdca)
% 257.77/258.09  (r1 zenon_Vhud zenon_Viud)
% 257.77/258.09  (-. (p612 zenon_Vqna))
% 257.77/258.09  (-. (p1514 zenon_Vem))
% 257.77/258.09  (-. (p906 zenon_Vwpc))
% 257.77/258.09  (r1 zenon_Vey zenon_Vgy)
% 257.77/258.09  (r1 zenon_Vpad zenon_Vqad)
% 257.77/258.09  (-. (p1302 zenon_Vppd))
% 257.77/258.09  (-. (p207 zenon_Vfnc))
% 257.77/258.09  (-. (p608 zenon_Voac))
% 257.77/258.09  (r1 zenon_Vqlc zenon_Vrlc)
% 257.77/258.09  (-. (p312 zenon_Vira))
% 257.77/258.09  (r1 zenon_Vlua zenon_Vnua)
% 257.77/258.09  (-. (p804 zenon_Vsed))
% 257.77/258.09  (r1 zenon_Vusb zenon_Vvsb)
% 257.77/258.09  (-. (p113 zenon_Vjia))
% 257.77/258.09  (r1 zenon_Vtvc zenon_Vuvc)
% 257.77/258.09  (-. (p1105 zenon_Vvwc))
% 257.77/258.09  (r1 zenon_Vtzb zenon_Vuzb)
% 257.77/258.09  (-. (p314 zenon_Vcu))
% 257.77/258.09  (r1 zenon_Vvj zenon_Vxj)
% 257.77/258.09  (-. (p409 zenon_Vqtb))
% 257.77/258.09  (r1 zenon_Vlmc zenon_Vmmc)
% 257.77/258.09  (r1 zenon_Vwdc zenon_Vydc)
% 257.77/258.09  (r1 zenon_Vqi zenon_Vsi)
% 257.77/258.09  (r1 zenon_Vzxa zenon_Vaya)
% 257.77/258.09  (-. (p903 zenon_Vrkd))
% 257.77/258.09  (-. (p706 zenon_Vkqc))
% 257.77/258.09  (-. (p1001 zenon_Vhvd))
% 257.77/258.09  (r1 zenon_Vraa zenon_Vsaa)
% 257.77/258.09  (-. (p811 zenon_Vtwa))
% 257.77/258.09  (r1 zenon_Vecb zenon_Vgcb)
% 257.77/258.09  (-. (p904 zenon_Vfed))
% 257.77/258.09  (r1 zenon_Vqsb zenon_Vrsb)
% 257.77/258.09  (r1 zenon_Vvra zenon_Vwra)
% 257.77/258.09  (-. (p107 zenon_Vxoc))
% 257.77/258.09  (r1 zenon_Vbac zenon_Vcac)
% 257.77/258.09  (r1 zenon_Vbi zenon_Vdi)
% 257.77/258.09  (-. (p311 zenon_Vhbb))
% 257.77/258.09  (r1 zenon_Vmxa zenon_Vnxa)
% 257.77/258.09  (-. (p712 zenon_Vqma))
% 257.77/258.09  (r1 zenon_Vhsc zenon_Visc)
% 257.77/258.09  (-. (p502 zenon_Vwrd))
% 257.77/258.09  (r1 zenon_Vec zenon_Vfc)
% 257.77/258.09  (-. (p505 zenon_Voyc))
% 257.77/258.09  (-. (p115 zenon_Vil))
% 257.77/258.09  (-. (p512 zenon_Vpoa))
% 257.77/258.09  (-. (p1204 zenon_Vqdd))
% 257.77/258.09  (r1 zenon_Vsr zenon_Vur)
% 257.77/258.09  (r1 zenon_Vmx zenon_Vox)
% 257.77/258.09  (-. (p313 zenon_Vbga))
% 257.77/258.09  (r1 zenon_Vcla zenon_Vdla)
% 257.77/258.09  (-. (p1007 zenon_Vnhc))
% 257.77/258.09  (-. (p103 zenon_Vyod))
% 257.77/258.09  (r1 zenon_Vkta zenon_Vlta)
% 257.77/258.09  (-. (p604 zenon_Vjfd))
% 257.77/258.09  (r1 zenon_Vgib zenon_Vhib)
% 257.77/258.09  (-. (p310 zenon_Vzkb))
% 257.77/258.09  (r1 zenon_Vcd zenon_Vdd)
% 257.77/258.09  (-. (p201 zenon_Vpyd))
% 257.77/258.09  (-. (p512 zenon_Vsoa))
% 257.77/258.09  (r1 zenon_Vxf zenon_Vzf)
% 257.77/258.09  (-. (p912 zenon_Vola))
% 257.77/258.09  (r1 zenon_Vulc zenon_Vvlc)
% 257.77/258.09  (r1 zenon_Vvcc zenon_Vxcc)
% 257.77/258.09  (-. (p614 zenon_Vzq))
% 257.77/258.09  (r1 zenon_Vpka zenon_Vqka)
% 257.77/258.09  (r1 zenon_Vtp zenon_Vvp)
% 257.77/258.09  (r1 zenon_Vodb zenon_Vqdb)
% 257.77/258.09  (r1 zenon_Vct zenon_Vet)
% 257.77/258.09  (r1 zenon_Vqta zenon_Vsta)
% 257.77/258.09  (-. (p506 zenon_Vurc))
% 257.77/258.09  (r1 zenon_Vzsb zenon_Vbtb)
% 257.77/258.09  (r1 zenon_Vktc zenon_Vltc)
% 257.77/258.09  (r1 zenon_Vyz zenon_Vzz)
% 257.77/258.09  (-. (p1206 zenon_Vepc))
% 257.77/258.09  (-. (p804 zenon_Vmed))
% 257.77/258.09  (-. (p1212 zenon_Vdka))
% 257.77/258.09  (-. (p608 zenon_Vyac))
% 257.77/258.09  (r1 zenon_Vro zenon_Vso)
% 257.77/258.09  (-. (p511 zenon_Vsza))
% 257.77/258.09  (-. (p406 zenon_Vqsc))
% 257.77/258.09  (r1 zenon_Vyga zenon_Vzga)
% 257.77/258.09  (-. (p1207 zenon_Vdhc))
% 257.77/258.09  (-. (p1315 zenon_Vu))
% 257.77/258.09  (r1 zenon_Vmjb zenon_Vojb)
% 257.77/258.09  (r1 zenon_Vmn zenon_Vnn)
% 257.77/258.09  (r1 zenon_Vqbc zenon_Vrbc)
% 257.77/258.09  (-. (p201 zenon_Vjyd))
% 257.77/258.09  (-. (p311 zenon_Vobb))
% 257.77/258.09  (r1 zenon_Vara zenon_Vcra)
% 257.77/258.09  (-. (p510 zenon_Vgjb))
% 257.77/258.09  (r1 zenon_Vqwa zenon_Vrwa)
% 257.77/258.09  (-. (p310 zenon_Vulb))
% 257.77/258.09  (r1 zenon_Vin zenon_Vjn)
% 257.77/258.09  (r1 zenon_Vhid zenon_Viid)
% 257.77/258.09  (r1 zenon_Vama zenon_Vbma)
% 257.77/258.09  (r1 zenon_Vngb zenon_Vogb)
% 257.77/258.09  (r1 zenon_Vwxb zenon_Vyxb)
% 257.77/258.09  (r1 zenon_Vkmb zenon_Vlmb)
% 257.77/258.09  (-. (p102 zenon_Vwtd))
% 257.77/258.09  (r1 zenon_Vut zenon_Vvt)
% 257.77/258.09  (-. (p1014 zenon_Vwn))
% 257.77/258.09  (-. (p602 zenon_Vnrd))
% 257.77/258.09  (-. (p314 zenon_Vdv))
% 257.77/258.09  (-. (p401 zenon_Vhxd))
% 257.77/258.09  (-. (p1015 zenon_Vbb))
% 257.77/258.09  (-. (p802 zenon_Vuqd))
% 257.77/258.09  (-. (p510 zenon_Vijb))
% 257.77/258.09  (-. (p102 zenon_Vkud))
% 257.77/258.09  (r1 zenon_Vvoc zenon_Vxoc)
% 257.77/258.09  (-. (p1303 zenon_Vwjd))
% 257.77/258.09  (r1 zenon_Vdzc zenon_Vezc)
% 257.77/258.09  (-. (p507 zenon_Vwjc))
% 257.77/258.09  (r1 zenon_Vkcd zenon_Vlcd)
% 257.77/258.09  (-. (p708 zenon_Vyzb))
% 257.77/258.09  (r1 zenon_Vpnd zenon_Vqnd)
% 257.77/258.09  (r1 zenon_Vlub zenon_Vmub)
% 257.77/258.09  (-. (p203 zenon_Vynd))
% 257.77/258.09  (r1 zenon_Vtea zenon_Vvea)
% 257.77/258.09  (-. (p1506 zenon_Vyoc))
% 257.77/258.09  (-. (p315 zenon_Vvi))
% 257.77/258.09  (r1 zenon_Vzfb zenon_Vagb)
% 257.77/258.09  (-. (p1312 zenon_Vaka))
% 257.77/258.09  (r1 zenon_Vpya zenon_Vrya)
% 257.77/258.09  (-. (p906 zenon_Vzpc))
% 257.77/258.09  (-. (p102 zenon_Vytd))
% 257.77/258.09  (-. (p101 zenon_Vezd))
% 257.77/258.09  (-. (p910 zenon_Vkgb))
% 257.77/258.09  (-. (p710 zenon_Vuhb))
% 257.77/258.09  (-. (p510 zenon_Vujb))
% 257.77/258.09  (r1 zenon_Vubd zenon_Vvbd)
% 257.77/258.09  (-. (p1004 zenon_Vded))
% 257.77/258.09  (-. (p301 zenon_Vuxd))
% 257.77/258.09  (r1 zenon_Vbp zenon_Vdp)
% 257.77/258.09  (-. (p213 zenon_Vvga))
% 257.77/258.09  (r1 zenon_Vdj zenon_Vfj)
% 257.77/258.09  (r1 zenon_Vdx zenon_Vfx)
% 257.77/258.09  (-. (p204 zenon_Vkhd))
% 257.77/258.09  (-. (p709 zenon_Vwqb))
% 257.77/258.09  (-. (p514 zenon_Vas))
% 257.77/258.09  (r1 zenon_Vuia zenon_Vwia)
% 257.77/258.09  (-. (p109 zenon_Vdxb))
% 257.77/258.09  (-. (p509 zenon_Vhsb))
% 257.77/258.09  (r1 zenon_Vnhd zenon_Vohd)
% 257.77/258.09  (-. (p211 zenon_Vedb))
% 257.77/258.09  (r1 zenon_Vjtb zenon_Vktb)
% 257.77/258.09  (-. (p906 zenon_Vupc))
% 257.77/258.09  (-. (p215 zenon_Voj))
% 257.77/258.09  (r1 zenon_Vbhd zenon_Vchd)
% 257.77/258.09  (-. (p1201 zenon_Vyud))
% 257.77/258.09  (-. (p405 zenon_Vgzc))
% 257.77/258.09  (-. (p105 zenon_Vvcd))
% 257.77/258.09  (-. (p307 zenon_Vvlc))
% 257.77/258.09  (-. (p1002 zenon_Vbqd))
% 257.77/258.09  (r1 zenon_Vseb zenon_Vueb)
% 257.77/258.09  (-. (p709 zenon_Vyqb))
% 257.77/258.09  (-. (p502 zenon_Vzrd))
% 257.77/258.09  (r1 zenon_Vavb zenon_Vcvb)
% 257.77/258.09  (r1 zenon_Vgj zenon_Vij)
% 257.77/258.09  (-. (p415 zenon_Veh))
% 257.77/258.09  (r1 zenon_Vwwb zenon_Vxwb)
% 257.77/258.09  (r1 zenon_Vvh zenon_Vxh)
% 257.77/258.09  (r1 zenon_Vjja zenon_Vlja)
% 257.77/258.09  (-. (p307 zenon_Vjlc))
% 257.77/258.09  (-. (p813 zenon_Veba))
% 257.77/258.09  (-. (p601 zenon_Vlwd))
% 257.77/258.09  (r1 zenon_Vlrc zenon_Vmrc)
% 257.77/258.09  (-. (p410 zenon_Vwjb))
% 257.77/258.09  (-. (p705 zenon_Vwxc))
% 257.77/258.09  (-. (p814 zenon_Vqo))
% 257.77/258.09  (-. (p206 zenon_Vwuc))
% 257.77/258.09  (-. (p810 zenon_Vygb))
% 257.77/258.09  (-. (p601 zenon_Vswd))
% 257.77/258.09  (-. (p401 zenon_Vmxd))
% 257.77/258.09  (r1 zenon_Vima zenon_Vkma)
% 257.77/258.09  (-. (p409 zenon_Vgtb))
% 257.77/258.09  (r1 zenon_Vqkc zenon_Vrkc)
% 257.77/258.09  (-. (p406 zenon_Vcsc))
% 257.77/258.09  (-. (p215 zenon_Vfj))
% 257.77/258.09  (r1 zenon_Vosb zenon_Vpsb)
% 257.77/258.09  (-. (p208 zenon_Viec))
% 257.77/258.09  (-. (p114 zenon_Vcx))
% 257.77/258.09  (r1 zenon_Vwaa zenon_Vyaa)
% 257.77/258.09  (r1 zenon_Vqpa zenon_Vrpa)
% 257.77/258.09  (r1 zenon_Vnjc zenon_Vojc)
% 257.77/258.09  (r1 zenon_Vopa zenon_Vppa)
% 257.77/258.09  (r1 zenon_Vbza zenon_Vcza)
% 257.77/258.09  (-. (p715 zenon_Vvd))
% 257.77/258.09  (r1 zenon_Vtnb zenon_Vunb)
% 257.77/258.09  (-. (p204 zenon_Vlid))
% 257.77/258.09  (r1 zenon_Vvu zenon_Vxu)
% 257.77/258.09  (r1 zenon_Vtad zenon_Vuad)
% 257.77/258.09  (-. (p604 zenon_Vefd))
% 257.77/258.09  (-. (p414 zenon_Vkt))
% 257.77/258.09  (-. (p111 zenon_Vieb))
% 257.77/258.09  (-. (p106 zenon_Vuvc))
% 257.77/258.09  (-. (p912 zenon_Vlla))
% 257.77/258.09  (-. (p503 zenon_Vvld))
% 257.77/258.09  (r1 zenon_Vybb zenon_Vacb)
% 257.77/258.09  (-. (p1012 zenon_Vwka))
% 257.77/258.09  (r1 zenon_Vif zenon_Vkf)
% 257.77/258.09  (-. (p402 zenon_Vksd))
% 257.77/258.09  (-. (p105 zenon_Vidd))
% 257.77/258.09  (-. (p414 zenon_Vet))
% 257.77/258.09  (-. (p1014 zenon_Vnn))
% 257.77/258.09  (-. (p1104 zenon_Vxdd))
% 257.77/258.09  (-. (p1103 zenon_Vgkd))
% 257.77/258.09  (r1 zenon_Van zenon_Vbn)
% 257.77/258.09  (r1 zenon_Vuq zenon_Vwq)
% 257.77/258.09  (-. (p203 zenon_Vcod))
% 257.77/258.09  (r1 zenon_Vfka zenon_Vgka)
% 257.77/258.09  (r1 zenon_Vxdb zenon_Vydb)
% 257.77/258.09  (r1 zenon_Vwrb zenon_Vxrb)
% 257.77/258.09  (-. (p1103 zenon_Vfkd))
% 257.77/258.09  (r1 zenon_Vftb zenon_Vgtb)
% 257.77/258.09  (-. (p214 zenon_Vmv))
% 257.77/258.09  (-. (p112 zenon_Vvta))
% 257.77/258.09  (-. (p202 zenon_Vbtd))
% 257.77/258.09  (r1 zenon_Vrad zenon_Vsad)
% 257.77/258.09  (-. (p810 zenon_Vwgb))
% 257.77/258.09  (r1 zenon_Vrzc zenon_Vszc)
% 257.77/258.09  (r1 zenon_Vt zenon_Vu)
% 257.77/258.09  (-. (p610 zenon_Vjib))
% 257.77/258.09  (r1 zenon_Vdsa zenon_Vesa)
% 257.77/258.09  (-. (p715 zenon_Vgd))
% 257.77/258.09  (r1 zenon_Vhd zenon_Vjd)
% 257.77/258.09  (-. (p908 zenon_Vezb))
% 257.77/258.09  (r1 zenon_Vdwa zenon_Vewa)
% 257.77/258.09  (-. (p309 zenon_Viub))
% 257.77/258.09  (-. (p312 zenon_Vora))
% 257.77/258.09  (p1601 Tau_0)
% 257.77/258.09  (r1 zenon_Vncb zenon_Vocb)
% 257.77/258.09  (r1 zenon_Vcuc zenon_Vduc)
% 257.77/258.09  (-. (p1215 zenon_Vba))
% 257.77/258.09  (r1 zenon_Vvad zenon_Vxad)
% 257.77/258.09  (-. (p706 zenon_Viqc))
% 257.77/258.09  (-. (p905 zenon_Vjxc))
% 257.77/258.09  (-. (p713 zenon_Vbca))
% 257.77/258.09  (-. (p209 zenon_Vpvb))
% 257.77/258.09  (r1 zenon_Viwb zenon_Vkwb)
% 257.77/258.09  (r1 zenon_Vaib zenon_Vbib)
% 257.77/258.09  (-. (p1309 zenon_Vdpb))
% 257.77/258.09  (-. (p407 zenon_Vclc))
% 257.77/258.09  (-. (p215 zenon_Vdk))
% 257.77/258.09  (r1 zenon_Vrq zenon_Vtq)
% 257.77/258.09  (r1 zenon_Vhtb zenon_Vitb)
% 257.77/258.09  (r1 zenon_Vzdb zenon_Vaeb)
% 257.77/258.09  (r1 zenon_Vws zenon_Vys)
% 257.77/258.09  (r1 zenon_Vxib zenon_Vyib)
% 257.77/258.09  (-. (p608 zenon_Vuac))
% 257.77/258.09  (-. (p506 zenon_Vwrc))
% 257.77/258.09  (-. (p306 zenon_Vptc))
% 257.77/258.09  (-. (p403 zenon_Vpmd))
% 257.77/258.09  (-. (p405 zenon_Vezc))
% 257.77/258.09  (-. (p109 zenon_Vzwb))
% 257.77/258.09  (r1 zenon_Vwsb zenon_Vysb)
% 257.77/258.09  (-. (p909 zenon_Vvpb))
% 257.77/258.09  (r1 zenon_Vcbc zenon_Vdbc)
% 257.77/258.09  (-. (p412 zenon_Vdqa))
% 257.77/258.09  (-. (p1407 zenon_Vxgc))
% 257.77/258.09  (-. (p402 zenon_Vjsd))
% 257.77/258.09  (-. (p405 zenon_Vqzc))
% 257.77/258.09  (r1 zenon_Vgcc zenon_Vhcc)
% 257.77/258.09  (-. (p1310 zenon_Vifb))
% 257.77/258.09  (r1 zenon_Vnnd zenon_Vond)
% 257.77/258.09  (r1 zenon_Vlva zenon_Vmva)
% 257.77/258.09  (-. (p1015 zenon_Vhb))
% 257.77/258.09  (-. (p213 zenon_Vnha))
% 257.77/258.09  (-. (p303 zenon_Vcnd))
% 257.77/258.09  (-. (p109 zenon_Vsxb))
% 257.77/258.09  (r1 zenon_Vts zenon_Vvs)
% 257.77/258.09  (r1 zenon_Vwfa zenon_Vyfa)
% 257.77/258.09  (-. (p812 zenon_Vtla))
% 257.77/258.09  (r1 zenon_Vsfc zenon_Vtfc)
% 257.77/258.09  (-. (p102 zenon_Vcud))
% 257.77/258.09  (-. (p614 zenon_Vwq))
% 257.77/258.09  (r1 zenon_Vrf zenon_Vtf)
% 257.77/258.09  (r1 zenon_Vavc zenon_Vcvc)
% 257.77/258.09  (-. (p212 zenon_Vksa))
% 257.77/258.09  (r1 zenon_Vyh zenon_Vai)
% 257.77/258.09  (r1 zenon_Vtba zenon_Vvba)
% 257.77/258.09  (-. (p103 zenon_Vapd))
% 257.77/258.09  (r1 zenon_Vycc zenon_Vadc)
% 257.77/258.09  (r1 zenon_Vena zenon_Vgna)
% 257.77/258.09  (-. (p403 zenon_Vmmd))
% 257.77/258.09  (-. (p1110 zenon_Vofb))
% 257.77/258.09  (r1 zenon_Vqcd zenon_Vrcd)
% 257.77/258.09  (-. (p406 zenon_Vosc))
% 257.77/258.09  (-. (p904 zenon_Vhed))
% 257.77/258.09  (-. (p310 zenon_Vflb))
% 257.77/258.09  (-. (p1203 zenon_Vyjd))
% 257.77/258.09  (r1 zenon_Viq zenon_Vjq)
% 257.77/258.09  (r1 zenon_Vqid zenon_Vrid)
% 257.77/258.09  (-. (p105 zenon_Vtcd))
% 257.77/258.09  (r1 zenon_Vtcb zenon_Vvcb)
% 257.77/258.09  (-. (p315 zenon_Vyi))
% 257.77/258.09  (-. (p410 zenon_Vyjb))
% 257.77/258.09  (-. (p906 zenon_Vypc))
% 257.77/258.09  (-. (p111 zenon_Vwdb))
% 257.77/258.09  (r1 zenon_Vbj zenon_Vcj)
% 257.77/258.09  (-. (p1209 zenon_Vgpb))
% 257.77/258.09  (r1 zenon_Vykb zenon_Vzkb)
% 257.77/258.09  (r1 zenon_Vzjc zenon_Vakc)
% 257.77/258.09  (-. (p611 zenon_Vrya))
% 257.77/258.09  (-. (p1001 zenon_Vlvd))
% 257.77/258.09  (-. (p108 zenon_Vrfc))
% 257.77/258.09  (-. (p305 zenon_Viad))
% 257.77/258.09  (-. (p609 zenon_Vtrb))
% 257.77/258.09  (-. (p107 zenon_Vunc))
% 257.77/258.09  (-. (p606 zenon_Vxqc))
% 257.77/258.09  (-. (p404 zenon_Vggd))
% 257.77/258.09  (-. (p404 zenon_Vxfd))
% 257.77/258.09  (r1 zenon_Vty zenon_Vuy)
% 257.77/258.09  (r1 zenon_Vcua zenon_Veua)
% 257.77/258.09  (r1 zenon_Vzqb zenon_Varb)
% 257.77/258.09  (-. (p903 zenon_Vtkd))
% 257.77/258.09  (-. (p405 zenon_Vizc))
% 257.77/258.09  (-. (p903 zenon_Vqkd))
% 257.77/258.09  (r1 zenon_Vjjc zenon_Vkjc)
% 257.77/258.09  (r1 zenon_Vffa zenon_Vhfa)
% 257.77/258.09  (-. (p615 zenon_Vae))
% 257.77/258.09  (-. (p203 zenon_Vmnd))
% 257.77/258.09  (-. (p109 zenon_Vbxb))
% 257.77/258.09  (-. (p808 zenon_Vmzb))
% 257.77/258.09  (-. (p511 zenon_Vvza))
% 257.77/258.09  (r1 zenon_Vnac zenon_Voac)
% 257.77/258.09  (-. (p902 zenon_Vnqd))
% 257.77/258.09  (r1 zenon_Vfga zenon_Vhga)
% 257.77/258.09  (-. (p802 zenon_Voqd))
% 257.77/258.09  (-. (p515 zenon_Vkf))
% 257.77/258.09  (r1 zenon_Vgl zenon_Vil)
% 257.77/258.09  (r1 zenon_Vxic zenon_Vyic)
% 257.77/258.09  (r1 zenon_Vpoc zenon_Vroc)
% 257.77/258.09  (r1 zenon_Vmja zenon_Voja)
% 257.77/258.09  (-. (p305 zenon_Vyzc))
% 257.77/258.09  (-. (p601 zenon_Vnwd))
% 257.77/258.09  (-. (p1002 zenon_Vgqd))
% 257.77/258.09  (-. (p302 zenon_Vtsd))
% 257.77/258.09  (r1 zenon_Vhea zenon_Viea)
% 257.77/258.09  (-. (p503 zenon_Vzld))
% 257.77/258.09  (-. (p907 zenon_Vuhc))
% 257.77/258.09  (r1 zenon_Vbv zenon_Vdv)
% 257.77/258.09  (-. (p308 zenon_Vvdc))
% 257.77/258.09  (-. (p507 zenon_Vsjc))
% 257.77/258.09  (r1 zenon_Vjpd zenon_Vlpd)
% 257.77/258.09  (r1 zenon_Vpub zenon_Vqub)
% 257.77/258.09  (-. (p206 zenon_Vfuc))
% 257.77/258.09  (r1 zenon_Vpm zenon_Vqm)
% 257.77/258.09  (r1 zenon_Vfdb zenon_Vhdb)
% 257.77/258.09  (-. (p701 zenon_Vgwd))
% 257.77/258.09  (r1 zenon_Vlgd zenon_Vmgd)
% 257.77/258.09  (-. (p1102 zenon_Vxpd))
% 257.77/258.09  (-. (p401 zenon_Vjxd))
% 257.77/258.09  (r1 zenon_Veda zenon_Vfda)
% 257.77/258.09  (-. (p205 zenon_Vpbd))
% 257.77/258.09  (-. (p1212 zenon_Vbka))
% 257.77/258.09  (-. (p115 zenon_Vam))
% 257.77/258.09  (r1 zenon_Vzic zenon_Vajc)
% 257.77/258.09  (r1 zenon_Vhka zenon_Vika)
% 257.77/258.09  (-. (p902 zenon_Vmqd))
% 257.77/258.09  (r1 zenon_Vfn zenon_Vhn)
% 257.77/258.09  (r1 zenon_Vhgc zenon_Vjgc)
% 257.77/258.09  (-. (p702 zenon_Vcrd))
% 257.77/258.09  (-. (p207 zenon_Vcnc))
% 257.77/258.09  (-. (p609 zenon_Vcsb))
% 257.77/258.09  (-. (p709 zenon_Vjrb))
% 257.77/258.09  (-. (p1011 zenon_Vsva))
% 257.77/258.09  (r1 zenon_Visa zenon_Vksa)
% 257.77/258.09  (r1 zenon_Vrmc zenon_Vsmc)
% 257.77/258.09  (-. (p805 zenon_Vpxc))
% 257.77/258.09  (r1 zenon_Vki zenon_Vmi)
% 257.77/258.09  (r1 zenon_Vqca zenon_Vsca)
% 257.77/258.09  (r1 zenon_Vvhb zenon_Vxhb)
% 257.77/258.09  (r1 zenon_Vlaa zenon_Vmaa)
% 257.77/258.09  (-. (p1014 zenon_Vjn))
% 257.77/258.09  (r1 zenon_Vpnc zenon_Vqnc)
% 257.77/258.09  (r1 zenon_Vvtb zenon_Vxtb)
% 257.77/258.09  (-. (p1312 zenon_Vyja))
% 257.77/258.10  (-. (p607 zenon_Vyic))
% 257.77/258.10  (-. (p1106 zenon_Vipc))
% 257.77/258.10  (-. (p208 zenon_Vmec))
% 257.77/258.10  (r1 zenon_Vit zenon_Vkt)
% 257.77/258.10  (-. (p702 zenon_Vxqd))
% 257.77/258.10  (r1 zenon_Vykc zenon_Vzkc)
% 257.77/258.10  (-. (p111 zenon_Vceb))
% 257.77/258.10  (r1 zenon_Vkrb zenon_Vlrb)
% 257.77/258.10  (-. (p1501 zenon_Vrud))
% 257.77/258.10  (r1 zenon_Vrnd zenon_Vsnd)
% 257.77/258.10  (r1 zenon_Vuna zenon_Vwna)
% 257.77/258.10  (-. (p403 zenon_Vimd))
% 257.77/258.10  (-. (p414 zenon_Vbt))
% 257.77/258.10  (-. (p1405 zenon_Vnwc))
% 257.77/258.10  (-. (p1207 zenon_Vehc))
% 257.77/258.10  (-. (p902 zenon_Viqd))
% 257.77/258.10  (r1 zenon_Vdf zenon_Vef)
% 257.77/258.10  (-. (p611 zenon_Vyxa))
% 257.77/258.10  (-. (p601 zenon_Vowd))
% 257.77/258.10  (r1 zenon_Vmtc zenon_Vntc)
% 257.77/258.10  (-. (p305 zenon_Vgad))
% 257.77/258.10  (-. (p1114 zenon_Vhn))
% 257.77/258.10  (-. (p302 zenon_Vxsd))
% 257.77/258.10  (r1 zenon_Vza zenon_Vbb)
% 257.77/258.10  (-. (p313 zenon_Vnga))
% 257.77/258.10  (-. (p215 zenon_Vij))
% 257.77/258.10  (-. (p606 zenon_Vtqc))
% 257.77/258.10  (r1 zenon_Vxnb zenon_Vynb)
% 257.77/258.10  (r1 zenon_Vbeb zenon_Vceb)
% 257.77/258.10  (r1 zenon_Vfaa zenon_Vhaa)
% 257.77/258.10  (-. (p307 zenon_Vrlc))
% 257.77/258.10  (-. (p801 zenon_Vawd))
% 257.77/258.10  (-. (p1112 zenon_Vmka))
% 257.77/258.10  (r1 zenon_Vgtc zenon_Vhtc)
% 257.77/258.10  (-. (p510 zenon_Vljb))
% 257.77/258.10  (-. (p713 zenon_Vsba))
% 257.77/258.10  (-. (p712 zenon_Vgna))
% 257.77/258.10  (-. (p112 zenon_Vqua))
% 257.77/258.10  (-. (p1104 zenon_Vtdd))
% 257.77/258.10  (r1 zenon_Vvva zenon_Vwva)
% 257.77/258.10  (-. (p1314 zenon_Vim))
% 257.77/258.10  (-. (p606 zenon_Vuqc))
% 257.77/258.10  (-. (p1106 zenon_Vlpc))
% 257.77/258.10  (-. (p1010 zenon_Vtfb))
% 257.77/258.10  (r1 zenon_Vkwa zenon_Vlwa)
% 257.77/258.10  (-. (p908 zenon_Vfzb))
% 257.77/258.10  (-. (p515 zenon_Vtf))
% 257.77/258.10  (r1 zenon_Vsla zenon_Vtla)
% 257.77/258.10  (r1 zenon_Vsl zenon_Vul)
% 257.77/258.10  (r1 zenon_Vfqb zenon_Vgqb)
% 257.77/258.10  (r1 zenon_Vrtb zenon_Vstb)
% 257.77/258.10  (-. (p1209 zenon_Vhpb))
% 257.77/258.10  (-. (p402 zenon_Vgsd))
% 257.77/258.10  (-. (p502 zenon_Vqrd))
% 257.77/258.10  (-. (p314 zenon_Vzt))
% 257.77/258.10  (-. (p613 zenon_Vpca))
% 257.77/258.10  (r1 zenon_Vvod zenon_Vwod)
% 257.77/258.10  (-. (p108 zenon_Vbgc))
% 257.77/258.10  (r1 zenon_Vfma zenon_Vhma)
% 257.77/258.10  (-. (p314 zenon_Vou))
% 257.77/258.10  (r1 zenon_Vgca zenon_Vhca)
% 257.77/258.10  (-. (p104 zenon_Vbjd))
% 257.77/258.10  (r1 zenon_Vdz zenon_Vfz)
% 257.77/258.10  (r1 zenon_Vklb zenon_Vllb)
% 257.77/258.10  (-. (p1108 zenon_Vtyb))
% 257.77/258.10  (-. (p206 zenon_Vpuc))
% 257.77/258.10  (-. (p1005 zenon_Vaxc))
% 257.77/258.10  (-. (p504 zenon_Vufd))
% 257.77/258.10  (r1 zenon_Viaa zenon_Vkaa)
% 257.77/258.10  (r1 zenon_Via zenon_Vja)
% 257.77/258.10  (-. (p410 zenon_Vlkb))
% 257.77/258.10  (r1 zenon_Vkqa zenon_Vmqa)
% 257.77/258.10  (-. (p711 zenon_Vlxa))
% 257.77/258.10  (-. (p508 zenon_Vhbc))
% 257.77/258.10  (r1 zenon_Vmra zenon_Vora)
% 257.77/258.10  (-. (p705 zenon_Vdyc))
% 257.77/258.10  (-. (p713 zenon_Vmba))
% 257.77/258.10  (-. (p502 zenon_Vtrd))
% 257.77/258.10  (r1 zenon_Vjva zenon_Vkva)
% 257.77/258.10  (-. (p614 zenon_Vqq))
% 257.77/258.10  (-. (p709 zenon_Vcrb))
% 257.77/258.10  (-. (p708 zenon_Vuzb))
% 257.77/258.10  (-. (p105 zenon_Vhcd))
% 257.77/258.10  (-. (p514 zenon_Vmr))
% 257.77/258.10  (r1 zenon_Vfzc zenon_Vgzc)
% 257.77/258.10  (-. (p207 zenon_Vsmc))
% 257.77/258.10  (-. (p1513 zenon_Vhy))
% 257.77/258.10  (-. (p906 zenon_Vxpc))
% 257.77/258.10  (-. (p411 zenon_Vhab))
% 257.77/258.10  (-. (p1507 zenon_Vwgc))
% 257.77/258.10  (r1 zenon_Vfod zenon_Vgod)
% 257.77/258.10  (r1 zenon_Vtaa zenon_Vvaa)
% 257.77/258.10  (-. (p408 zenon_Vfcc))
% 257.77/258.10  (-. (p112 zenon_Vbua))
% 257.77/258.10  (-. (p106 zenon_Vwvc))
% 257.77/258.10  (-. (p613 zenon_Vbda))
% 257.77/258.10  (r1 zenon_Vmoc zenon_Vooc)
% 257.77/258.10  (r1 zenon_Vzka zenon_Vbla)
% 257.77/258.10  (-. (p210 zenon_Vrmb))
% 257.77/258.10  (-. (p714 zenon_Vpp))
% 257.77/258.10  (-. (p410 zenon_Vckb))
% 257.77/258.10  (-. (p105 zenon_Vcdd))
% 257.77/258.10  (r1 zenon_Vubc zenon_Vwbc)
% 257.77/258.10  (-. (p302 zenon_Vnsd))
% 257.77/258.10  (-. (p215 zenon_Vaj))
% 257.77/258.10  (r1 zenon_Vjx zenon_Vlx)
% 257.77/258.10  (-. (p714 zenon_Vvp))
% 257.77/258.10  (r1 zenon_Vzac zenon_Vbbc)
% 257.77/258.10  (-. (p608 zenon_Vkac))
% 257.77/258.10  (r1 zenon_Vpu zenon_Vru)
% 257.77/258.10  (-. (p706 zenon_Vqqc))
% 257.77/258.10  (-. (p1014 zenon_Vtn))
% 257.77/258.10  (-. (p302 zenon_Vrsd))
% 257.77/258.10  (-. (p407 zenon_Vjkc))
% 257.77/258.10  (-. (p1413 zenon_Vjy))
% 257.77/258.10  (-. (p110 zenon_Vpob))
% 257.77/258.10  (-. (p507 zenon_Vakc))
% 257.77/258.10  (-. (p905 zenon_Vlxc))
% 257.77/258.10  (-. (p112 zenon_Vkua))
% 257.77/258.10  (-. (p412 zenon_Vnpa))
% 257.77/258.10  (r1 zenon_Vsra zenon_Vura)
% 257.77/258.10  (-. (p715 zenon_Vpd))
% 257.77/258.10  (-. (p1214 zenon_Vqm))
% 257.77/258.10  (-. (p302 zenon_Vosd))
% 257.77/258.10  (r1 zenon_Vhoc zenon_Vioc)
% 257.77/258.10  (r1 zenon_Vsid zenon_Vtid)
% 257.77/258.10  (-. (p907 zenon_Vrhc))
% 257.77/258.10  (r1 zenon_Vmbd zenon_Vnbd)
% 257.77/258.10  (-. (p214 zenon_Vfv))
% 257.77/258.10  (-. (p114 zenon_Vay))
% 257.77/258.10  (r1 zenon_Vop zenon_Vpp)
% 257.77/258.10  (-. (p209 zenon_Vrvb))
% 257.77/258.10  (r1 zenon_Vskb zenon_Vukb)
% 257.77/258.10  (r1 zenon_Vpa zenon_Vra)
% 257.77/258.10  (-. (p609 zenon_Vprb))
% 257.77/258.10  (-. (p112 zenon_Vnta))
% 257.77/258.10  (r1 zenon_Vlga zenon_Vnga)
% 257.77/258.10  (r1 zenon_Vacc zenon_Vbcc)
% 257.77/258.10  (r1 zenon_Vqbd zenon_Vrbd)
% 257.77/258.10  (r1 zenon_Vlb zenon_Vmb)
% 257.77/258.10  (r1 zenon_Vfza zenon_Vgza)
% 257.77/258.10  (-. (p101 zenon_Vgzd))
% 257.77/258.10  (-. (p1110 zenon_Vsfb))
% 257.77/258.10  (r1 zenon_Vpk zenon_Vqk)
% 257.77/258.10  (-. (p711 zenon_Vqxa))
% 257.77/258.10  (r1 zenon_Vfvc zenon_Vgvc)
% 257.77/258.10  (-. (p105 zenon_Vjcd))
% 257.77/258.10  (r1 zenon_Vvmc zenon_Vwmc)
% 257.77/258.10  (-. (p102 zenon_Vutd))
% 257.77/258.10  (r1 zenon_Vztd zenon_Vaud)
% 257.77/258.10  (-. (p815 zenon_Vzc))
% 257.77/258.10  (-. (p404 zenon_Vegd))
% 257.77/258.10  (-. (p508 zenon_Vfbc))
% 257.77/258.10  (-. (p701 zenon_Vdwd))
% 257.77/258.10  (r1 zenon_Vqmb zenon_Vrmb)
% 257.77/258.10  (r1 zenon_Vrzb zenon_Vszb)
% 257.77/258.10  (-. (p307 zenon_Vxlc))
% 257.77/258.10  (r1 zenon_Vfsa zenon_Vhsa)
% 257.77/258.10  (-. (p610 zenon_Vhib))
% 257.77/258.10  (-. (p1302 zenon_Vrpd))
% 257.77/258.10  (-. (p910 zenon_Vagb))
% 257.77/258.10  (-. (p811 zenon_Vbxa))
% 257.77/258.10  (-. (p407 zenon_Vtkc))
% 257.77/258.10  (r1 zenon_Vpvc zenon_Vqvc)
% 257.77/258.10  (-. (p107 zenon_Vioc))
% 257.77/258.10  (-. (p609 zenon_Vrrb))
% 257.77/258.10  (r1 zenon_Vcec zenon_Veec)
% 257.77/258.10  (-. (p801 zenon_Vuvd))
% 257.77/258.10  (r1 zenon_Vpeb zenon_Vreb)
% 257.77/258.10  (-. (p506 zenon_Vsrc))
% 257.77/258.10  (-. (p812 zenon_Vvla))
% 257.77/258.10  (r1 zenon_Vldc zenon_Vmdc)
% 257.77/258.10  (-. (p208 zenon_Vqec))
% 257.77/258.10  (-. (p702 zenon_Vdrd))
% 257.77/258.10  (-. (p312 zenon_Vfra))
% 257.77/258.10  (-. (p313 zenon_Vvfa))
% 257.77/258.10  (-. (p604 zenon_Vgfd))
% 257.77/258.10  (-. (p214 zenon_Vkw))
% 257.77/258.10  (-. (p207 zenon_Vomc))
% 257.77/258.10  (-. (p1005 zenon_Vbxc))
% 257.77/258.10  (r1 zenon_Vun zenon_Vwn)
% 257.77/258.10  (-. (p104 zenon_Vfjd))
% 257.77/258.10  (-. (p202 zenon_Vmtd))
% 257.77/258.10  (-. (p1207 zenon_Vchc))
% 257.77/258.10  (-. (p909 zenon_Vzpb))
% 257.77/258.10  (-. (p302 zenon_Vwsd))
% 257.77/258.10  (-. (p1413 zenon_Viy))
% 257.77/258.10  (-. (p1011 zenon_Vqva))
% 257.77/258.10  (-. (p811 zenon_Vpwa))
% 257.77/258.10  (-. (p1205 zenon_Vswc))
% 257.77/258.10  (-. (p407 zenon_Vnkc))
% 257.77/258.10  (-. (p114 zenon_Vsw))
% 257.77/258.10  (-. (p805 zenon_Vnxc))
% 257.77/258.10  (r1 zenon_Vmkb zenon_Vokb)
% 257.77/258.10  (-. (p703 zenon_Vild))
% 257.77/258.10  (r1 zenon_Vhod zenon_Viod)
% 257.77/258.10  (-. (p506 zenon_Vgrc))
% 257.77/258.10  (r1 zenon_Vnm zenon_Vom)
% 257.77/258.10  (-. (p512 zenon_Vnoa))
% 257.77/258.10  (r1 zenon_Vkpa zenon_Vlpa)
% 257.77/258.10  (r1 zenon_Vmfc zenon_Vnfc)
% 257.77/258.10  (r1 zenon_Vjr zenon_Vkr)
% 257.77/258.10  (r1 zenon_Vgxa zenon_Vhxa)
% 257.77/258.10  (-. (p901 zenon_Vsvd))
% 257.77/258.10  (r1 zenon_Vvic zenon_Vwic)
% 257.77/258.10  (-. (p1305 zenon_Vowc))
% 257.77/258.10  (r1 zenon_Vsmb zenon_Vumb)
% 257.77/258.10  (r1 zenon_Vqrb zenon_Vrrb)
% 257.77/258.10  (r1 zenon_Vhnd zenon_Vind)
% 257.77/258.10  (r1 zenon_Vjfc zenon_Vlfc)
% 257.77/258.10  (r1 zenon_Vdeb zenon_Vfeb)
% 257.77/258.10  (-. (p506 zenon_Vkrc))
% 257.77/258.10  (r1 zenon_Vrjc zenon_Vsjc)
% 257.77/258.10  (r1 zenon_Vqvb zenon_Vrvb)
% 257.77/258.10  (-. (p508 zenon_Vrbc))
% 257.77/258.10  (r1 zenon_Vwvb zenon_Vxvb)
% 257.77/258.10  (-. (p307 zenon_Vtlc))
% 257.77/258.10  (r1 zenon_Vwv zenon_Vyv)
% 257.77/258.10  (-. (p113 zenon_Vlja))
% 257.77/258.10  (r1 zenon_Vndc zenon_Vodc)
% 257.77/258.10  (p201 Tau_0)
% 257.77/258.10  (-. (p1314 zenon_Vkm))
% 257.77/258.10  (r1 zenon_Vddc zenon_Vedc)
% 257.77/258.10  (-. (p510 zenon_Vejb))
% 257.77/258.10  (-. (p108 zenon_Vxfc))
% 257.77/258.10  (-. (p401 zenon_Vixd))
% 257.77/258.10  (-. (p302 zenon_Vusd))
% 257.77/258.10  (-. (p315 zenon_Vji))
% 257.77/258.10  (-. (p1206 zenon_Vfpc))
% 257.77/258.10  (r1 zenon_Vveb zenon_Vxeb)
% 257.77/258.10  (r1 zenon_Vyid zenon_Vzid)
% 257.77/258.10  (r1 zenon_Vwi zenon_Vyi)
% 257.77/258.10  (r1 zenon_Vfad zenon_Vgad)
% 257.77/258.10  (r1 zenon_Vmvb zenon_Vnvb)
% 257.77/258.10  (-. (p313 zenon_Vofa))
% 257.77/258.10  (-. (p112 zenon_Vjta))
% 257.77/258.10  (r1 zenon_Vnqb zenon_Voqb)
% 257.77/258.10  (r1 zenon_Vzn zenon_Vao)
% 257.77/258.10  (-. (p306 zenon_Vftc))
% 257.77/258.10  (-. (p502 zenon_Vrrd))
% 257.77/258.10  (r1 zenon_Vhk zenon_Vjk)
% 257.77/258.10  (r1 zenon_Vrcb zenon_Vscb)
% 257.77/258.10  (-. (p811 zenon_Vywa))
% 257.77/258.10  (-. (p111 zenon_Voeb))
% 257.77/258.10  (r1 zenon_Vurb zenon_Vvrb)
% 257.77/258.10  (-. (p307 zenon_Vimc))
% 257.77/258.10  (-. (p905 zenon_Vgxc))
% 257.77/258.10  (-. (p205 zenon_Vdbd))
% 257.77/258.10  (r1 zenon_Vwca zenon_Vyca)
% 257.77/258.10  (-. (p803 zenon_Vxkd))
% 257.77/258.10  (r1 zenon_Vtsc zenon_Vvsc)
% 257.77/258.10  (-. (p1006 zenon_Vopc))
% 257.77/258.10  (-. (p313 zenon_Vkga))
% 257.77/258.10  (-. (p511 zenon_Vwya))
% 257.77/258.10  (-. (p610 zenon_Vlib))
% 257.77/258.10  (-. (p112 zenon_Vhua))
% 257.77/258.10  (-. (p513 zenon_Vmda))
% 257.77/258.10  (r1 zenon_Vxnc zenon_Vync)
% 257.77/258.10  (r1 zenon_Vexb zenon_Vfxb)
% 257.77/258.10  (r1 zenon_Vdmc zenon_Vfmc)
% 257.77/258.10  (-. (p601 zenon_Vkwd))
% 257.77/258.10  (r1 zenon_Vei zenon_Vgi)
% 257.77/258.10  (-. (p410 zenon_Vgkb))
% 257.77/258.10  (-. (p801 zenon_Vxvd))
% 257.77/258.10  (-. (p410 zenon_Vxkb))
% 257.77/258.10  (-. (p1214 zenon_Vsm))
% 257.77/258.10  (r1 zenon_Vmib zenon_Voib)
% 257.77/258.10  (-. (p1002 zenon_Veqd))
% 257.77/258.10  (-. (p702 zenon_Vyqd))
% 257.77/258.10  (r1 zenon_Vcib zenon_Vdib)
% 257.77/258.10  (r1 zenon_Vioa zenon_Vjoa)
% 257.77/258.10  (-. (p804 zenon_Vled))
% 257.77/258.10  (r1 zenon_Vzca zenon_Vbda)
% 257.77/258.10  (r1 zenon_Vlad zenon_Vmad)
% 257.77/258.10  (-. (p914 zenon_Vlo))
% 257.77/258.10  (-. (p811 zenon_Vlwa))
% 257.77/258.10  (r1 zenon_Vpcb zenon_Vqcb)
% 257.77/258.10  (r1 zenon_Vwea zenon_Vyea)
% 257.77/258.10  (r1 zenon_Vmlc zenon_Vnlc)
% 257.77/258.10  (-. (p1515 zenon_Vm))
% 257.77/258.10  (r1 zenon_Vvqb zenon_Vwqb)
% 257.77/258.10  (-. (p215 zenon_Vjk))
% 257.77/258.10  (-. (p408 zenon_Vbcc))
% 257.77/258.10  (r1 zenon_Vcga zenon_Vega)
% 257.77/258.10  (r1 zenon_Vcea zenon_Veea)
% 257.77/258.10  (-. (p106 zenon_Vkwc))
% 257.77/258.10  (r1 zenon_Vzzb zenon_Vaac)
% 257.77/258.10  (-. (p212 zenon_Vwra))
% 257.77/258.10  (-. (p1503 zenon_Vsjd))
% 257.77/258.10  (-. (p402 zenon_Visd))
% 257.77/258.10  (-. (p1102 zenon_Vzpd))
% 257.77/258.10  (-. (p410 zenon_Vakb))
% 257.77/258.10  (r1 zenon_Vmuc zenon_Vnuc)
% 257.77/258.10  (-. (p603 zenon_Vmld))
% 257.77/258.10  (-. (p701 zenon_Vbwd))
% 257.77/258.10  (-. (p108 zenon_Vggc))
% 257.77/258.10  (r1 zenon_Vidb zenon_Vkdb)
% 257.77/258.10  (r1 zenon_Vgcd zenon_Vhcd)
% 257.77/258.10  (r1 zenon_Vgda zenon_Vhda)
% 257.77/258.10  (-. (p1112 zenon_Vkka))
% 257.77/258.10  (r1 zenon_Vdza zenon_Veza)
% 257.77/258.10  (r1 zenon_Vzy zenon_Vaz)
% 257.77/258.10  (-. (p1107 zenon_Vghc))
% 257.77/258.10  (-. (p203 zenon_Vaod))
% 257.77/258.10  (r1 zenon_Vspa zenon_Vupa)
% 257.77/258.10  (-. (p304 zenon_Vahd))
% 257.77/258.10  (r1 zenon_Vfnd zenon_Vgnd)
% 257.77/258.10  (-. (p115 zenon_Vok))
% 257.77/258.10  (-. (p308 zenon_Vbec))
% 257.77/258.10  (r1 zenon_Vcyb zenon_Veyb)
% 257.77/258.10  (-. (p109 zenon_Veyb))
% 257.77/258.10  (-. (p315 zenon_Vai))
% 257.77/258.10  (-. (p807 zenon_Vcic))
% 257.77/258.10  (-. (p303 zenon_Vymd))
% 257.77/258.10  (r1 zenon_Vrhd zenon_Vshd)
% 257.77/258.10  (-. (p808 zenon_Vnzb))
% 257.77/258.10  (r1 zenon_Vdg zenon_Vfg)
% 257.77/258.10  (r1 zenon_Vry zenon_Vsy)
% 257.77/258.10  (r1 zenon_Vlvc zenon_Vmvc)
% 257.77/258.10  (-. (p112 zenon_Vsta))
% 257.77/258.10  (-. (p413 zenon_Vmea))
% 257.77/258.10  (-. (p1009 zenon_Vopb))
% 257.77/258.10  (-. (p108 zenon_Vjgc))
% 257.77/258.10  (-. (p703 zenon_Vkld))
% 257.77/258.10  (r1 zenon_Vdpd zenon_Vepd)
% 257.77/258.10  (-. (p114 zenon_Vfx))
% 257.77/258.10  (-. (p514 zenon_Vjs))
% 257.77/258.10  (-. (p809 zenon_Vgqb))
% 257.77/258.10  (-. (p212 zenon_Vwsa))
% 257.77/258.10  (-. (p804 zenon_Vred))
% 257.77/258.10  (-. (p1301 zenon_Vuud))
% 257.77/258.10  (r1 zenon_Vvgd zenon_Vwgd)
% 257.77/258.10  (r1 zenon_Vibd zenon_Vjbd)
% 257.77/258.10  (r1 zenon_Vbud zenon_Vcud)
% 257.77/258.10  (r1 zenon_Viib zenon_Vjib)
% 257.77/258.10  (-. (p202 zenon_Vftd))
% 257.77/258.10  (-. (p505 zenon_Vvyc))
% 257.77/258.10  (-. (p709 zenon_Verb))
% 257.77/258.10  (-. (p112 zenon_Veua))
% 257.77/258.10  (r1 zenon_Vnrc zenon_Vorc)
% 257.77/258.10  (r1 zenon_Vfua zenon_Vhua)
% 257.77/258.10  (-. (p1202 zenon_Vtpd))
% 257.77/258.10  (-. (p415 zenon_Vbh))
% 257.77/258.10  (-. (p407 zenon_Vrkc))
% 257.77/258.10  (r1 zenon_Vns zenon_Vos)
% 257.77/258.10  (-. (p309 zenon_Vuub))
% 257.77/258.10  (r1 zenon_Vtdc zenon_Vvdc)
% 257.77/258.10  (-. (p413 zenon_Vkfa))
% 257.77/258.10  (-. (p810 zenon_Vqgb))
% 257.77/258.10  (r1 zenon_Valc zenon_Vclc)
% 257.77/258.10  (r1 zenon_Vrrc zenon_Vsrc)
% 257.77/258.10  (-. (p603 zenon_Vpld))
% 257.77/258.10  (-. (p414 zenon_Vnt))
% 257.77/258.10  (-. (p511 zenon_Veza))
% 257.77/258.10  (-. (p402 zenon_Vasd))
% 257.77/258.10  (-. (p810 zenon_Vsgb))
% 257.77/258.10  (-. (p113 zenon_Vcja))
% 257.77/258.10  (-. (p807 zenon_Vfic))
% 257.77/258.10  (r1 zenon_Vpdc zenon_Vqdc)
% 257.77/258.10  (r1 zenon_Vtw zenon_Vuw)
% 257.77/258.10  (-. (p909 zenon_Vupb))
% 257.77/258.10  (r1 zenon_Vixb zenon_Vjxb)
% 257.77/258.10  (-. (p108 zenon_Vnfc))
% 257.77/258.10  (-. (p509 zenon_Vtsb))
% 257.77/258.10  (r1 zenon_Vklc zenon_Vllc)
% 257.77/258.10  (r1 zenon_Vig zenon_Vjg)
% 257.77/258.10  (r1 zenon_Vnzc zenon_Vozc)
% 257.77/258.10  (-. (p602 zenon_Vgrd))
% 257.77/258.10  (-. (p310 zenon_Volb))
% 257.77/258.10  (-. (p102 zenon_Vmud))
% 257.77/258.10  (-. (p1207 zenon_Vfhc))
% 257.77/258.10  (r1 zenon_Vria zenon_Vtia)
% 257.77/258.10  (r1 zenon_Vbjb zenon_Vcjb)
% 257.77/258.10  (r1 zenon_Vccc zenon_Vdcc)
% 257.77/258.10  (r1 zenon_Vprc zenon_Vqrc)
% 257.77/258.10  (-. (p713 zenon_Viba))
% 257.77/258.10  (r1 zenon_Vbnb zenon_Vdnb)
% 257.77/258.10  (r1 zenon_Vca zenon_Vea)
% 257.77/258.10  (-. (p108 zenon_Vsgc))
% 257.77/258.10  (r1 zenon_Viia zenon_Vjia)
% 257.77/258.10  (-. (p513 zenon_Vpda))
% 257.77/258.10  (-. (p1006 zenon_Vrpc))
% 257.77/258.10  (-. (p705 zenon_Vayc))
% 257.77/258.10  (r1 zenon_Vrgd zenon_Vsgd)
% 257.77/258.10  (p301 Tau_0)
% 257.77/258.10  (r1 zenon_Vqza zenon_Vsza)
% 257.77/258.10  (-. (p310 zenon_Vxlb))
% 257.77/258.10  (-. (p109 zenon_Vmxb))
% 257.77/258.10  (-. (p501 zenon_Vdxd))
% 257.77/258.10  (r1 zenon_Vvya zenon_Vwya)
% 257.77/258.10  (r1 zenon_Vfea zenon_Vgea)
% 257.77/258.10  (r1 zenon_Vadd zenon_Vcdd)
% 257.77/258.10  (r1 zenon_Vuz zenon_Vvz)
% 257.77/258.10  (r1 zenon_Vzfa zenon_Vbga)
% 257.77/258.10  (-. (p611 zenon_Voya))
% 257.77/258.10  (-. (p707 zenon_Vgic))
% 257.77/258.10  (-. (p1114 zenon_Vbn))
% 257.77/258.10  (r1 zenon_Vytb zenon_Vaub)
% 257.77/258.10  (-. (p404 zenon_Vagd))
% 257.77/258.10  (r1 zenon_Vuf zenon_Vwf)
% 257.77/258.10  (r1 zenon_Vlc zenon_Vnc)
% 257.77/258.10  (-. (p404 zenon_Vzfd))
% 257.77/258.10  (r1 zenon_Vznb zenon_Vaob)
% 257.77/258.10  (r1 zenon_Vabb zenon_Vbbb)
% 257.77/258.10  (-. (p510 zenon_Vajb))
% 257.77/258.10  (r1 zenon_Vvub zenon_Vwub)
% 257.77/258.10  (-. (p212 zenon_Vasa))
% 257.77/258.10  (r1 zenon_Vnza zenon_Vpza)
% 257.77/258.10  (-. (p1315 zenon_Vx))
% 257.77/258.10  (r1 zenon_Vzd zenon_Vae)
% 257.77/258.10  (-. (p301 zenon_Vdyd))
% 257.77/258.10  (-. (p505 zenon_Vtyc))
% 257.77/258.10  (-. (p411 zenon_Vtab))
% 257.77/258.10  (r1 zenon_Vdsc zenon_Vesc)
% 257.77/258.10  (r1 zenon_Vwga zenon_Vxga)
% 257.77/258.10  (-. (p1006 zenon_Vqpc))
% 257.77/258.10  (r1 zenon_Vrdb zenon_Vsdb)
% 257.77/258.10  (-. (p509 zenon_Vpsb))
% 257.77/258.10  (r1 zenon_Vaxb zenon_Vbxb)
% 257.77/258.10  (-. (p607 zenon_Vgjc))
% 257.77/258.10  (r1 zenon_Vhrb zenon_Vjrb)
% 257.77/258.10  (r1 zenon_Vfhd zenon_Vghd)
% 257.77/258.10  (r1 zenon_Vobd zenon_Vpbd)
% 257.77/258.10  (-. (p1304 zenon_Vmdd))
% 257.77/258.10  (-. (p1511 zenon_Vuua))
% 257.77/258.10  (r1 zenon_Vsa zenon_Vua)
% 257.77/258.10  (r1 zenon_Vdr zenon_Vfr)
% 257.77/258.10  (-. (p511 zenon_Vcza))
% 257.77/258.10  (-. (p309 zenon_Vlvb))
% 257.77/258.10  (r1 zenon_Viwc zenon_Vkwc)
% 257.77/258.10  (-. (p903 zenon_Vskd))
% 257.77/258.10  (r1 zenon_Vdta zenon_Vfta)
% 257.77/258.10  (-. (p609 zenon_Vlrb))
% 257.77/258.10  (r1 zenon_Vcb zenon_Veb)
% 257.77/258.10  (r1 zenon_Vpkb zenon_Vrkb)
% 257.77/258.10  (-. (p301 zenon_Vrxd))
% 257.77/258.10  (r1 zenon_Vr zenon_Vs)
% 257.77/258.10  (r1 zenon_Vrab zenon_Vtab)
% 257.77/258.10  (-. (p613 zenon_Vmca))
% 257.77/258.10  (-. (p203 zenon_Veod))
% 257.77/258.10  (r1 zenon_Voha zenon_Vqha)
% 257.77/258.10  (-. (p509 zenon_Vlsb))
% 257.77/258.10  (-. (p306 zenon_Vdtc))
% 257.77/258.10  (-. (p315 zenon_Vph))
% 257.77/258.10  (-. (p205 zenon_Vbbd))
% 257.77/258.10  (r1 zenon_Vlha zenon_Vnha)
% 257.77/258.10  (-. (p101 zenon_Vbzd))
% 257.77/258.10  (-. (p1401 zenon_Vtud))
% 257.77/258.10  (r1 zenon_Vau zenon_Vcu)
% 257.77/258.10  (-. (p309 zenon_Vwub))
% 257.77/258.10  (r1 zenon_Vntd zenon_Votd)
% 257.77/258.10  (r1 zenon_Vjjb zenon_Vljb)
% 257.77/258.10  (-. (p101 zenon_Vtyd))
% 257.77/258.10  (r1 zenon_Vpaa zenon_Vqaa)
% 257.77/258.10  (r1 zenon_Vtv zenon_Vvv)
% 257.77/258.10  (-. (p813 zenon_Vqaa))
% 257.77/258.10  (-. (p707 zenon_Vhic))
% 257.77/258.10  (r1 zenon_Vxvc zenon_Vyvc)
% 257.77/258.10  (-. (p510 zenon_Vwib))
% 257.77/258.10  (-. (p802 zenon_Vsqd))
% 257.77/258.10  (-. (p309 zenon_Vcvb))
% 257.77/258.10  (-. (p202 zenon_Vctd))
% 257.77/258.10  (r1 zenon_Vaia zenon_Vcia)
% 257.77/258.10  (-. (p815 zenon_Vhc))
% 257.77/258.10  (-. (p606 zenon_Vrqc))
% 257.77/258.10  (-. (p502 zenon_Vxrd))
% 257.77/258.10  (-. (p814 zenon_Vjp))
% 257.77/258.10  (-. (p611 zenon_Veya))
% 257.77/258.10  (-. (p604 zenon_Vffd))
% 257.77/258.10  (r1 zenon_Vzmc zenon_Vanc)
% 257.77/258.10  (-. (p1204 zenon_Vsdd))
% 257.77/258.10  (r1 zenon_Velb zenon_Vflb)
% 257.77/258.10  (-. (p110 zenon_Vwnb))
% 257.77/258.10  (-. (p712 zenon_Vmma))
% 257.77/258.10  (r1 zenon_Vpac zenon_Vqac)
% 257.77/258.10  (r1 zenon_Visb zenon_Vjsb)
% 257.77/258.10  (-. (p503 zenon_Vfmd))
% 257.77/258.10  (-. (p812 zenon_Vkma))
% 257.77/258.10  (-. (p1014 zenon_Vln))
% 257.77/258.10  (-. (p812 zenon_Vxla))
% 257.77/258.10  (-. (p409 zenon_Vitb))
% 257.77/258.10  (r1 zenon_Vowb zenon_Vqwb)
% 257.77/258.10  (-. (p610 zenon_Voib))
% 257.77/258.10  (r1 zenon_Vhdc zenon_Vidc)
% 257.77/258.10  (-. (p112 zenon_Vyta))
% 257.77/258.10  (-. (p205 zenon_Vlbd))
% 257.77/258.10  (r1 zenon_Vmcc zenon_Vncc)
% 257.77/258.10  (-. (p709 zenon_Vgrb))
% 257.77/258.10  (r1 zenon_Voz zenon_Vqz)
% 257.77/258.10  (r1 zenon_Vtca zenon_Vvca)
% 257.77/258.10  (r1 zenon_Vpra zenon_Vrra)
% 257.77/258.10  (-. (p1210 zenon_Vmfb))
% 257.77/258.10  (r1 zenon_Vuha zenon_Vwha)
% 257.77/258.10  (-. (p302 zenon_Vqsd))
% 257.77/258.10  (-. (p214 zenon_Vqw))
% 257.77/258.10  (-. (p702 zenon_Verd))
% 257.77/258.10  (-. (p515 zenon_Vwf))
% 257.77/258.10  (r1 zenon_Vfac zenon_Vgac)
% 257.77/258.10  (r1 zenon_Vkoa zenon_Vloa)
% 257.77/258.10  (r1 zenon_Vboc zenon_Vcoc)
% 257.77/258.10  (-. (p201 zenon_Vfyd))
% 257.77/258.10  (-. (p114 zenon_Vux))
% 257.77/258.10  (-. (p402 zenon_Vcsd))
% 257.77/258.10  (r1 zenon_Vjna zenon_Vkna)
% 257.77/258.10  (r1 zenon_Vvr zenon_Vxr)
% 257.77/258.10  (r1 zenon_Vih zenon_Vkh)
% 257.77/258.10  (-. (p408 zenon_Vpcc))
% 257.77/258.10  (-. (p709 zenon_Vuqb))
% 257.77/258.10  (-. (p312 zenon_Vuqa))
% 257.77/258.10  (r1 zenon_Vcdb zenon_Vedb)
% 257.77/258.10  (-. (p209 zenon_Vkwb))
% 257.77/258.10  (-. (p113 zenon_Vqia))
% 257.77/258.10  (-. (p405 zenon_Vmzc))
% 257.77/258.10  (-. (p305 zenon_Vcad))
% 257.77/258.10  (r1 zenon_Vbqb zenon_Vcqb)
% 257.77/258.10  (r1 zenon_Vkca zenon_Vmca)
% 257.77/258.10  (r1 zenon_Vila zenon_Vjla)
% 257.77/258.10  (-. (p401 zenon_Vlxd))
% 257.77/258.10  (-. (p907 zenon_Vshc))
% 257.77/258.10  (r1 zenon_Vvhd zenon_Vwhd)
% 257.77/258.10  (r1 zenon_Vxya zenon_Vyya)
% 257.77/258.10  (r1 zenon_Vcda zenon_Vdda)
% 257.77/258.10  (-. (p1107 zenon_Vihc))
% 257.77/258.10  (-. (p1101 zenon_Vevd))
% 257.77/258.10  (-. (p209 zenon_Vhwb))
% 257.77/258.10  (r1 zenon_Vxka zenon_Vyka)
% 257.77/258.10  (-. (p902 zenon_Vkqd))
% 257.77/258.10  (-. (p608 zenon_Vqac))
% 257.77/258.10  (r1 zenon_Vaha zenon_Vbha)
% 257.77/258.10  (r1 zenon_Vpzb zenon_Vqzb)
% 257.77/258.10  (-. (p910 zenon_Vegb))
% 257.77/258.10  (p1501 Tau_0)
% 257.77/258.10  (-. (p808 zenon_Vozb))
% 257.77/258.10  (-. (p1112 zenon_Vika))
% 257.77/258.10  (r1 zenon_Vyu zenon_Vav)
% 257.77/258.10  (-. (p103 zenon_Vsod))
% 257.77/258.10  (r1 zenon_Vlac zenon_Vmac)
% 257.77/258.10  (-. (p704 zenon_Vxed))
% 257.77/258.10  (-. (p702 zenon_Vzqd))
% 257.77/258.10  (r1 zenon_Vve zenon_Vxe)
% 257.77/258.10  (r1 zenon_Vfya zenon_Vgya)
% 257.77/258.10  (-. (p1004 zenon_Vzdd))
% 257.77/258.10  (r1 zenon_Viw zenon_Vkw)
% 257.77/258.10  (-. (p408 zenon_Vdcc))
% 257.77/258.10  (r1 zenon_Vdid zenon_Veid)
% 257.77/258.10  (-. (p807 zenon_Vbic))
% 257.77/258.10  (-. (p303 zenon_Vend))
% 257.77/258.10  (r1 zenon_Vpbb zenon_Vrbb)
% 257.77/258.10  (-. (p201 zenon_Vhyd))
% 257.77/258.10  (r1 zenon_Vldb zenon_Vndb)
% 257.77/258.10  (-. (p308 zenon_Veec))
% 257.77/258.10  (r1 zenon_Vvnc zenon_Vwnc)
% 257.77/258.10  (-. (p315 zenon_Vxh))
% 257.77/258.10  (-. (p606 zenon_Vwqc))
% 257.77/258.10  (-. (p1402 zenon_Vopd))
% 257.77/258.10  (-. (p212 zenon_Vzsa))
% 257.77/258.10  (-. (p810 zenon_Vahb))
% 257.77/258.10  (-. (p209 zenon_Vqwb))
% 257.77/258.10  (-. (p204 zenon_Vyhd))
% 257.77/258.10  (-. (p703 zenon_Vfld))
% 257.77/258.10  (-. (p205 zenon_Vvbd))
% 257.77/258.10  (r1 zenon_Vtfa zenon_Vvfa)
% 257.77/258.10  (-. (p1502 zenon_Vmpd))
% 257.77/258.10  (-. (p507 zenon_Vyjc))
% 257.77/258.10  (-. (p304 zenon_Vkgd))
% 257.77/258.10  (-. (p313 zenon_Vqfa))
% 257.77/258.10  (r1 zenon_Vfb zenon_Vhb)
% 257.77/258.10  (r1 zenon_Vfdc zenon_Vgdc)
% 257.77/258.10  (r1 zenon_Vbna zenon_Vdna)
% 257.77/258.10  (-. (p1208 zenon_Vmyb))
% 257.77/258.10  (r1 zenon_Vzda zenon_Vbea)
% 257.77/258.10  (-. (p115 zenon_Vcl))
% 257.77/258.10  (-. (p602 zenon_Vird))
% 257.77/258.10  (-. (p815 zenon_Vkc))
% 257.77/258.10  (-. (p510 zenon_Vyib))
% 257.77/258.10  (r1 zenon_Vmid zenon_Vnid)
% 257.77/258.10  (-. (p1003 zenon_Vjkd))
% 257.77/258.10  (r1 zenon_Vrga zenon_Vtga)
% 257.77/258.10  (-. (p505 zenon_Vxyc))
% 257.77/258.10  (r1 zenon_Vyr zenon_Vas)
% 257.77/258.10  (-. (p1109 zenon_Vlpb))
% 257.77/258.10  (r1 zenon_Veob zenon_Vgob)
% 257.77/258.10  (-. (p506 zenon_Vcrc))
% 257.77/258.10  (r1 zenon_Vznd zenon_Vaod)
% 257.77/258.10  (r1 zenon_Vlt zenon_Vnt)
% 257.77/258.10  (-. (p512 zenon_Vloa))
% 257.77/258.10  (r1 zenon_Viuc zenon_Vjuc)
% 257.77/258.10  (r1 zenon_Voh zenon_Vph)
% 257.77/258.10  (-. (p901 zenon_Vmvd))
% 257.77/258.10  (-. (p209 zenon_Vnwb))
% 257.77/258.10  (-. (p206 zenon_Vbuc))
% 257.77/258.10  (-. (p202 zenon_Vjtd))
% 257.77/258.10  (-. (p709 zenon_Vsqb))
% 257.77/258.10  (-. (p214 zenon_Vbw))
% 257.77/258.10  (-. (p706 zenon_Vnqc))
% 257.77/258.10  (-. (p906 zenon_Vvpc))
% 257.77/258.10  (r1 zenon_Voga zenon_Vqga)
% 257.77/258.10  (-. (p204 zenon_Vgid))
% 257.77/258.10  (-. (p809 zenon_Vkqb))
% 257.77/258.10  (-. (p908 zenon_Vbzb))
% 257.77/258.10  (-. (p306 zenon_Vntc))
% 257.77/258.10  (-. (p1414 zenon_Vfm))
% 257.77/258.10  (-. (p614 zenon_Vcr))
% 257.77/258.10  (-. (p502 zenon_Vyrd))
% 257.77/258.10  (-. (p309 zenon_Vqub))
% 257.77/258.10  (-. (p511 zenon_Vmza))
% 257.77/258.10  (-. (p109 zenon_Vbyb))
% 257.77/258.10  (-. (p1005 zenon_Vcxc))
% 257.77/258.10  (r1 zenon_Vks zenon_Vms)
% 257.77/258.10  (-. (p1108 zenon_Vryb))
% 257.77/258.10  (-. (p501 zenon_Vuwd))
% 257.77/258.10  (-. (p501 zenon_Vvwd))
% 257.77/258.10  (r1 zenon_Vawb zenon_Vbwb)
% 257.77/258.10  (r1 zenon_Vcq zenon_Veq)
% 257.77/258.10  (r1 zenon_Vny zenon_Voy)
% 257.77/258.10  (-. (p615 zenon_Vxe))
% 257.77/258.10  (-. (p1202 zenon_Vupd))
% 257.77/258.10  (-. (p204 zenon_Vqhd))
% 257.77/258.10  (-. (p314 zenon_Vav))
% 257.77/258.10  (r1 zenon_Vmhb zenon_Vnhb)
% 257.77/258.10  (r1 zenon_Vtec zenon_Vuec)
% 257.77/258.10  (r1 zenon_Vmoa zenon_Vnoa)
% 257.77/258.10  (r1 zenon_Vvlb zenon_Vxlb)
% 257.77/258.10  (-. (p1005 zenon_Vdxc))
% 257.77/258.10  (-. (p504 zenon_Vnfd))
% 257.77/258.10  (r1 zenon_Vdud zenon_Veud)
% 257.77/258.10  (-. (p703 zenon_Vcld))
% 257.77/258.10  (r1 zenon_Vicc zenon_Vjcc)
% 257.77/258.10  (-. (p811 zenon_Vvwa))
% 257.77/258.10  (-. (p210 zenon_Vjnb))
% 257.77/258.10  (-. (p1414 zenon_Vgm))
% 257.77/258.10  (-. (p409 zenon_Vstb))
% 257.77/258.10  (-. (p803 zenon_Vukd))
% 257.77/258.10  (-. (p209 zenon_Vvvb))
% 257.77/258.10  (-. (p508 zenon_Vnbc))
% 257.77/258.10  (r1 zenon_Vyx zenon_Vay)
% 257.77/258.10  (-. (p806 zenon_Vbqc))
% 257.77/258.10  (-. (p115 zenon_Vul))
% 257.77/258.10  (r1 zenon_Vjya zenon_Vlya)
% 257.77/258.10  (-. (p615 zenon_Vue))
% 257.77/258.10  (-. (p306 zenon_Vltc))
% 257.77/258.10  (r1 zenon_Vbm zenon_Vdm)
% 257.77/258.10  (r1 zenon_Vrdc zenon_Vsdc)
% 257.77/258.10  (-. (p701 zenon_Vhwd))
% 257.77/258.10  (r1 zenon_Vdoc zenon_Veoc)
% 257.77/258.10  (-. (p913 zenon_Vvz))
% 257.77/258.10  (-. (p704 zenon_Vved))
% 257.77/258.10  (-. (p306 zenon_Vzsc))
% 257.77/258.10  (r1 zenon_Vqp zenon_Vsp)
% 257.77/258.10  (-. (p1214 zenon_Vom))
% 257.77/258.10  (-. (p201 zenon_Vmyd))
% 257.77/258.10  (r1 zenon_Vzs zenon_Vbt)
% 257.77/258.10  (-. (p1406 zenon_Vapc))
% 257.77/258.10  (-. (p1113 zenon_Vwy))
% 257.77/258.10  (r1 zenon_Vbkb zenon_Vckb)
% 257.77/258.10  (-. (p1006 zenon_Vnpc))
% 257.77/258.10  (r1 zenon_Vlab zenon_Vnab)
% 257.77/258.10  (r1 zenon_Vrma zenon_Vsma)
% 257.77/258.10  (-. (p310 zenon_Vjlb))
% 257.77/258.10  (-. (p409 zenon_Vmtb))
% 257.77/258.10  (r1 zenon_Vita zenon_Vjta)
% 257.77/258.10  (-. (p1408 zenon_Vhyb))
% 257.77/258.10  (r1 zenon_Vtnd zenon_Vund)
% 257.77/258.10  (-. (p1210 zenon_Vlfb))
% 257.77/258.10  (-. (p1211 zenon_Vdva))
% 257.77/258.10  (-. (p309 zenon_Voub))
% 257.77/258.10  (-. (p213 zenon_Vkha))
% 257.77/258.10  (-. (p703 zenon_Vjld))
% 257.77/258.10  (-. (p1203 zenon_Vbkd))
% 257.77/258.10  (-. (p302 zenon_Vvsd))
% 257.77/258.10  (-. (p713 zenon_Vyba))
% 257.77/258.10  (r1 zenon_Vkhb zenon_Vlhb)
% 257.77/258.10  (r1 zenon_Vwm zenon_Vxm)
% 257.77/258.10  (r1 zenon_Vhjb zenon_Vijb)
% 257.77/258.10  (r1 zenon_Vpr zenon_Vrr)
% 257.77/258.10  (-. (p315 zenon_Vmi))
% 257.77/258.10  (-. (p507 zenon_Vfkc))
% 257.77/258.10  (r1 zenon_Vtac zenon_Vuac)
% 257.77/258.10  (-. (p303 zenon_Vsmd))
% 257.77/258.10  (-. (p312 zenon_Vcra))
% 257.77/258.10  (-. (p205 zenon_Vrbd))
% 257.77/258.10  (-. (p204 zenon_Vohd))
% 257.77/258.10  (r1 zenon_Vibb zenon_Vjbb)
% 257.77/258.10  (r1 zenon_Vzzc zenon_Vaad)
% 257.77/258.10  (-. (p1307 zenon_Vahc))
% 257.77/258.10  (-. (p207 zenon_Vlnc))
% 257.77/258.10  (-. (p209 zenon_Vtwb))
% 257.77/258.10  (r1 zenon_Vp zenon_Vq)
% 257.77/258.10  (-. (p104 zenon_Vdjd))
% 257.77/258.10  (-. (p506 zenon_Vmrc))
% 257.77/258.10  (-. (p612 zenon_Vwna))
% 257.77/258.10  (r1 zenon_Vxra zenon_Vyra)
% 257.77/258.10  (-. (p806 zenon_Veqc))
% 257.77/258.10  (-. (p313 zenon_Vqga))
% 257.77/258.10  (r1 zenon_Vphd zenon_Vqhd)
% 257.77/258.10  (-. (p104 zenon_Vtid))
% 257.77/258.10  (-. (p104 zenon_Vrjd))
% 257.77/258.10  (r1 zenon_Vtrc zenon_Vurc)
% 257.77/258.10  (r1 zenon_Vuid zenon_Vvid)
% 257.77/258.10  (-. (p304 zenon_Vmgd))
% 257.77/258.10  (r1 zenon_Vgeb zenon_Vieb)
% 257.77/258.10  (-. (p503 zenon_Vxld))
% 257.77/258.10  (r1 zenon_Vxxa zenon_Vyxa)
% 257.77/258.10  (r1 zenon_Vfq zenon_Vhq)
% 257.77/258.10  (-. (p306 zenon_Vxtc))
% 257.77/258.10  (-. (p203 zenon_Vwnd))
% 257.77/258.10  (-. (p1403 zenon_Vujd))
% 257.77/258.10  (-. (p313 zenon_Vsfa))
% 257.77/258.10  (r1 zenon_Vxgd zenon_Vygd)
% 257.77/258.10  (r1 zenon_Vfec zenon_Vgec)
% 257.77/258.10  (r1 zenon_Vva zenon_Vwa)
% 257.77/258.10  (-. (p1008 zenon_Vuyb))
% 257.77/258.10  (-. (p1101 zenon_Vcvd))
% 257.77/258.10  (-. (p803 zenon_Vwkd))
% 257.77/258.10  (-. (p612 zenon_Vfoa))
% 257.77/258.10  (-. (p406 zenon_Vgsc))
% 257.77/258.10  (r1 zenon_Vjac zenon_Vkac)
% 257.77/258.10  (-. (p401 zenon_Vgxd))
% 257.77/258.10  (-. (p314 zenon_Viu))
% 257.77/258.10  (-. (p305 zenon_Vsad))
% 257.77/258.10  (r1 zenon_Vhcb zenon_Vicb)
% 257.77/258.10  (-. (p312 zenon_Voqa))
% 257.77/258.10  (-. (p401 zenon_Vqxd))
% 257.77/258.10  (r1 zenon_Vv zenon_Vx)
% 257.77/258.10  (-. (p312 zenon_Vzqa))
% 257.77/258.10  (-. (p407 zenon_Vpkc))
% 257.77/258.10  (r1 zenon_Vzhd zenon_Vaid)
% 257.77/258.10  (-. (p305 zenon_Vkad))
% 257.77/258.10  (r1 zenon_Vscc zenon_Vucc)
% 257.77/258.10  (-. (p1109 zenon_Vkpb))
% 257.77/258.10  (-. (p805 zenon_Vsxc))
% 257.77/258.10  (r1 zenon_Vqxb zenon_Vsxb)
% 257.77/258.10  (-. (p315 zenon_Vsi))
% 257.77/258.10  (-. (p710 zenon_Vphb))
% 257.77/258.10  (-. (p213 zenon_Vfia))
% 257.77/258.10  (r1 zenon_Vxna zenon_Vzna)
% 257.77/258.10  (-. (p403 zenon_Vrmd))
% 257.77/258.10  (-. (p813 zenon_Vvaa))
% 257.77/258.10  (r1 zenon_Vvpa zenon_Vxpa)
% 257.77/258.10  (-. (p410 zenon_Vikb))
% 257.77/258.10  (-. (p111 zenon_Vaeb))
% 257.77/258.10  (r1 zenon_Vvgb zenon_Vwgb)
% 257.77/258.10  (r1 zenon_Vkbd zenon_Vlbd)
% 257.77/258.10  (-. (p1008 zenon_Vyyb))
% 257.77/258.10  (-. (p605 zenon_Vkyc))
% 257.77/258.10  (-. (p310 zenon_Vblb))
% 257.77/258.10  (r1 zenon_Vjud zenon_Vkud)
% 257.77/258.10  (r1 zenon_Vtqa zenon_Vuqa)
% 257.77/258.10  (-. (p115 zenon_Vrl))
% 257.77/258.10  (-. (p103 zenon_Vlpd))
% 257.77/258.10  (-. (p501 zenon_Vaxd))
% 257.77/258.10  (-. (p914 zenon_Voo))
% 257.77/258.10  (-. (p911 zenon_Vyva))
% 257.77/258.10  (-. (p115 zenon_Vqk))
% 257.77/258.10  (r1 zenon_Vptd zenon_Vqtd)
% 257.77/258.10  (-. (p713 zenon_Vkba))
% 257.77/258.10  (r1 zenon_Vpy zenon_Vqy)
% 257.77/258.10  (-. (p1013 zenon_Vqz))
% 257.77/258.10  (r1 zenon_Vxod zenon_Vyod)
% 257.77/258.10  (r1 zenon_Vkv zenon_Vmv)
% 257.77/258.10  (r1 zenon_Vtqb zenon_Vuqb)
% 257.77/258.10  (-. (p413 zenon_Vefa))
% 257.77/258.10  (-. (p208 zenon_Vlfc))
% 257.77/258.10  (-. (p711 zenon_Vdxa))
% 257.77/258.10  (-. (p1203 zenon_Vzjd))
% 257.77/258.10  (-. (p1210 zenon_Vkfb))
% 257.77/258.10  (-. (p614 zenon_Vlq))
% 257.77/258.10  (p401 Tau_0)
% 257.77/258.10  (r1 zenon_Vqda zenon_Vsda)
% 257.77/258.10  (-. (p211 zenon_Vmcb))
% 257.77/258.10  (-. (p213 zenon_Vzga))
% 257.77/258.10  (r1 zenon_Vlec zenon_Vmec)
% 257.77/258.10  (-. (p508 zenon_Vlbc))
% 257.77/258.10  (r1 zenon_Vy zenon_Vz)
% 257.77/258.10  (r1 zenon_Vek zenon_Vgk)
% 257.77/258.10  (r1 zenon_Vrva zenon_Vsva)
% 257.77/258.10  (r1 zenon_Vlqb zenon_Vmqb)
% 257.77/258.10  (-. (p513 zenon_Vhda))
% 257.77/258.10  (-. (p1110 zenon_Vrfb))
% 257.77/258.10  (-. (p104 zenon_Vpid))
% 257.77/258.10  (-. (p504 zenon_Vsfd))
% 257.77/258.10  (r1 zenon_Vyhb zenon_Vzhb)
% 257.77/258.10  (-. (p101 zenon_Vwyd))
% 257.77/258.10  (-. (p503 zenon_Vwld))
% 257.77/258.10  (-. (p201 zenon_Vnyd))
% 257.77/258.10  (-. (p403 zenon_Vjmd))
% 257.77/258.10  (-. (p511 zenon_Vpza))
% 257.77/258.10  (-. (p903 zenon_Vokd))
% 257.77/258.10  (r1 zenon_Vvtc zenon_Vxtc)
% 257.77/258.10  (-. (p813 zenon_Vyaa))
% 257.77/258.10  (-. (p1104 zenon_Vudd))
% 257.77/258.10  (r1 zenon_Vtda zenon_Vvda)
% 257.77/258.10  (-. (p808 zenon_Vizb))
% 257.77/258.10  (r1 zenon_Vguc zenon_Vhuc)
% 257.77/258.10  (r1 zenon_Vuk zenon_Vwk)
% 257.77/258.10  (r1 zenon_Vcgc zenon_Vdgc)
% 257.77/258.10  (-. (p614 zenon_Vfr))
% 257.77/258.10  (-. (p1206 zenon_Vgpc))
% 257.77/258.10  (-. (p115 zenon_Vdm))
% 257.77/258.10  (r1 zenon_Vuxa zenon_Vwxa)
% 257.77/258.10  (-. (p1005 zenon_Vfxc))
% 257.77/258.10  (r1 zenon_Vjea zenon_Vkea)
% 257.77/258.10  (-. (p312 zenon_Vqqa))
% 257.77/258.10  (r1 zenon_Vic zenon_Vkc)
% 257.77/258.10  (-. (p710 zenon_Vjhb))
% 257.77/258.10  (-. (p1115 zenon_Vra))
% 257.77/258.10  (-. (p611 zenon_Vlya))
% 257.77/258.10  (-. (p203 zenon_Vgod))
% 257.77/258.10  (r1 zenon_Vsja zenon_Vuja)
% 257.77/258.10  (r1 zenon_Vghb zenon_Vhhb)
% 257.77/258.10  (-. (p102 zenon_Vqtd))
% 257.77/258.10  (-. (p1106 zenon_Vjpc))
% 257.77/258.10  (r1 zenon_Vep zenon_Vgp)
% 257.77/258.10  (-. (p804 zenon_Vned))
% 257.77/258.10  (-. (p1204 zenon_Vpdd))
% 257.77/258.10  (r1 zenon_Vfid zenon_Vgid)
% 257.77/258.10  (-. (p209 zenon_Vtvb))
% 257.77/258.10  (-. (p209 zenon_Vxvb))
% 257.77/258.10  (-. (p101 zenon_Vsyd))
% 257.77/258.10  (r1 zenon_Vrnb zenon_Vsnb)
% 257.77/258.10  (-. (p511 zenon_Vaza))
% 257.77/258.10  (-. (p904 zenon_Vged))
% 257.77/258.10  (r1 zenon_Votc zenon_Vptc)
% 257.77/258.10  (-. (p704 zenon_Vyed))
% 257.77/258.10  (r1 zenon_Vxk zenon_Vzk)
% 257.77/258.10  (r1 zenon_Vhya zenon_Viya)
% 257.77/258.10  (r1 zenon_Venb zenon_Vgnb)
% 257.77/258.10  (r1 zenon_Vhpd zenon_Vipd)
% 257.77/258.10  (-. (p315 zenon_Vdi))
% 257.77/258.10  (r1 zenon_Vhqb zenon_Viqb)
% 257.77/258.10  (r1 zenon_Vdlc zenon_Vflc)
% 257.77/258.10  (r1 zenon_Vdac zenon_Veac)
% 257.77/258.10  (r1 zenon_Vibc zenon_Vjbc)
% 257.77/258.10  (-. (p915 zenon_Vub))
% 257.77/258.10  (-. (p1505 zenon_Vlwc))
% 257.77/258.10  (r1 zenon_Vtgb zenon_Vugb)
% 257.77/258.10  (-. (p1308 zenon_Viyb))
% 257.77/258.10  (r1 zenon_Vxc zenon_Vzc)
% 257.77/258.10  (-. (p1115 zenon_Vja))
% 257.77/258.10  (-. (p603 zenon_Vuld))
% 257.77/258.10  (-. (p503 zenon_Vemd))
% 257.77/258.10  (-. (p103 zenon_Vood))
% 257.77/258.10  (-. (p208 zenon_Vsec))
% 257.77/258.10  (-. (p107 zenon_Veoc))
% 257.77/258.10  (-. (p115 zenon_Vzk))
% 257.77/258.10  (-. (p214 zenon_Vew))
% 257.77/258.10  (-. (p113 zenon_Vhia))
% 257.77/258.10  (-. (p206 zenon_Vzuc))
% 257.77/258.10  (r1 zenon_Vwta zenon_Vyta)
% 257.77/258.10  (-. (p803 zenon_Vald))
% 257.77/258.10  (-. (p102 zenon_Vqud))
% 257.77/258.10  (-. (p514 zenon_Vkr))
% 257.77/258.10  (-. (p102 zenon_Veud))
% 257.77/258.10  (r1 zenon_Vplb zenon_Vrlb)
% 257.77/258.10  (-. (p1209 zenon_Vipb))
% 257.77/258.10  (-. (p715 zenon_Vsd))
% 257.77/258.10  (-. (p115 zenon_Vfl))
% 257.77/258.10  (-. (p312 zenon_Vrra))
% 257.77/258.10  (r1 zenon_Vpib zenon_Vrib)
% 257.77/258.10  (r1 zenon_Vmz zenon_Vnz)
% 257.77/258.10  (-. (p412 zenon_Vlpa))
% 257.77/258.10  (-. (p201 zenon_Viyd))
% 257.77/258.10  (r1 zenon_Vmbc zenon_Vnbc)
% 257.77/258.10  (-. (p812 zenon_Vema))
% 257.77/258.10  (-. (p309 zenon_Vfvb))
% 257.77/258.10  (r1 zenon_Vvw zenon_Vww)
% 257.77/258.10  (r1 zenon_Vhza zenon_Vjza)
% 257.77/258.10  (-. (p411 zenon_Vzza))
% 257.77/258.10  (-. (p1303 zenon_Vxjd))
% 257.77/258.10  (r1 zenon_Vfgb zenon_Vggb)
% 257.77/258.10  (r1 zenon_Vbs zenon_Vds)
% 257.77/258.10  (-. (p214 zenon_Vsv))
% 257.77/258.10  (r1 zenon_Vnaa zenon_Voaa)
% 257.77/258.10  (-. (p915 zenon_Vac))
% 257.77/258.10  (r1 zenon_Vyla zenon_Vzla)
% 257.77/258.10  (-. (p208 zenon_Vffc))
% 257.77/258.10  (-. (p301 zenon_Vayd))
% 257.77/258.10  (-. (p905 zenon_Vixc))
% 257.77/258.10  (r1 zenon_Vpsc zenon_Vqsc)
% 257.77/258.10  (-. (p1315 zenon_Vs))
% 257.77/258.10  (r1 zenon_Void zenon_Vpid)
% 257.77/258.10  (-. (p608 zenon_Vwac))
% 257.77/258.10  (-. (p1211 zenon_Vbva))
% 257.77/258.10  (-. (p415 zenon_Vvg))
% 257.77/258.10  (-. (p712 zenon_Vana))
% 257.77/258.10  (-. (p213 zenon_Vtha))
% 257.77/258.10  (-. (p207 zenon_Vinc))
% 257.77/258.10  (-. (p704 zenon_Vzed))
% 257.77/258.10  (-. (p505 zenon_Vqyc))
% 257.77/258.10  (r1 zenon_Vhub zenon_Viub)
% 257.77/258.10  (-. (p805 zenon_Vqxc))
% 257.77/258.10  (-. (p810 zenon_Vdhb))
% 257.77/258.10  (-. (p513 zenon_Vbea))
% 257.77/258.10  (-. (p411 zenon_Vbab))
% 257.77/258.10  (-. (p304 zenon_Vwgd))
% 257.77/258.10  (-. (p513 zenon_Vdda))
% 257.77/258.10  (r1 zenon_Vbya zenon_Vcya)
% 257.77/258.10  (r1 zenon_Vmnc zenon_Vonc)
% 257.77/258.10  (-. (p203 zenon_Vsnd))
% 257.77/258.10  (-. (p711 zenon_Vwxa))
% 257.77/258.10  (-. (p703 zenon_Veld))
% 257.77/258.10  (-. (p1104 zenon_Vvdd))
% 257.77/258.10  (-. (p307 zenon_Vplc))
% 257.77/258.10  (-. (p1113 zenon_Vcz))
% 257.77/258.10  (-. (p213 zenon_Vxga))
% 257.77/258.10  (-. (p1409 zenon_Vapb))
% 257.77/258.10  (-. (p211 zenon_Vqdb))
% 257.77/258.10  (-. (p501 zenon_Vbxd))
% 257.77/258.10  (-. (p705 zenon_Vxxc))
% 257.77/258.10  (-. (p405 zenon_Vazc))
% 257.77/258.10  (r1 zenon_Vjrc zenon_Vkrc)
% 257.77/258.10  (r1 zenon_Vje zenon_Vle)
% 257.77/258.10  (r1 zenon_Vglb zenon_Vhlb)
% 257.77/258.10  (-. (p207 zenon_Vkmc))
% 257.77/258.10  (-. (p610 zenon_Vzhb))
% 257.77/258.10  (r1 zenon_Vabd zenon_Vbbd)
% 257.77/258.10  (-. (p110 zenon_Vqnb))
% 257.77/258.10  (-. (p809 zenon_Vcqb))
% 257.77/258.10  (-. (p1208 zenon_Voyb))
% 257.77/258.10  (-. (p504 zenon_Vqfd))
% 257.77/258.10  (-. (p212 zenon_Vnsa))
% 257.77/258.10  (-. (p509 zenon_Vrsb))
% 257.77/258.10  (-. (p409 zenon_Vktb))
% 257.77/258.10  (r1 zenon_Vcfa zenon_Vefa)
% 257.77/258.10  (r1 zenon_Vbob zenon_Vdob)
% 257.77/258.10  (-. (p205 zenon_Vtbd))
% 257.77/258.10  (-. (p602 zenon_Vfrd))
% 257.77/258.10  (-. (p707 zenon_Voic))
% 257.77/258.10  (-. (p612 zenon_Vtna))
% 257.77/258.10  (r1 zenon_Vlna zenon_Vmna)
% 257.77/258.10  (-. (p212 zenon_Vcsa))
% 257.77/258.10  (-. (p310 zenon_Vdlb))
% 257.77/258.10  (r1 zenon_Vzra zenon_Vasa)
% 257.77/258.10  (r1 zenon_Vsjb zenon_Vujb)
% 257.77/258.10  (-. (p314 zenon_Vvt))
% 257.77/258.10  (-. (p113 zenon_Vnia))
% 257.77/258.10  (-. (p714 zenon_Veq))
% 257.77/258.10  (-. (p507 zenon_Vojc))
% 257.77/258.10  (-. (p115 zenon_Vtk))
% 257.77/258.10  (-. (p212 zenon_Vhsa))
% 257.77/258.10  (r1 zenon_Vzrc zenon_Vasc)
% 257.77/258.10  *)
% 257.77/258.10  (* NO-PROOF *)
% 257.77/258.10  % SZS status GaveUp
% 257.77/258.10  Number of rewrites on terms: 0
% 257.77/258.10  Number of rewrites on props: 0
% 257.77/258.10  nodes searched: 7103
% 257.77/258.10  max branch formulas: 10038
% 257.77/258.10  proof nodes created: 0
% 257.77/258.10  formulas created: 69469
% 257.77/258.10  
%------------------------------------------------------------------------------