↑ Up

ZenonModulo---0.5.0.UNK-Non.f

View TPTP
Problem Process solution in
SystemOnTSTP Download .tgz 
%------------------------------------------------------------------------------
% File     : ZenonModulo---0.5.0
% Problem  : LCL685+1.010 : TPTP v9.3.1. Released v4.0.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : run_zenon_modulo %d %s

% Computer : n029.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 9.88s 10.18s
% Output   : None 
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : LCL685+1.010 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03  % Command  : run_zenon_modulo %d %s
% 0.07/0.34  % Computer : n029.cluster.edu
% 0.07/0.34  % Model    : x86_64 x86_64
% 0.07/0.34  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.34  % Memory   : 8046.5625MB
% 0.07/0.34  % OS       : Linux 6.8.0-71-generic
% 0.07/0.34  % CPULimit : 300
% 0.07/0.34  % WCLimit  : 300
% 0.07/0.34  % DateTime : Sat Sep  5 20:03:40 UTC 2026
% 0.07/0.34  % CPUTime  : 
% 9.88/10.17  Zenon error: exhausted search space without finding a proof
% 9.88/10.17  (* Current branch:
% 9.88/10.17  (-. (p102 zenon_Vmja))
% 9.88/10.17  (-. (p103 zenon_Vwga))
% 9.88/10.17  (r1 zenon_Vmw zenon_Vow)
% 9.88/10.17  (-. (p602 zenon_Vwha))
% 9.88/10.17  (-. (p109 zenon_Vij))
% 9.88/10.17  (-. (p708 zenon_Vrk))
% 9.88/10.17  (-. (p704 zenon_Vkba))
% 9.88/10.17  (-. (p207 zenon_Vyr))
% 9.88/10.17  (-. (p306 zenon_Vtv))
% 9.88/10.17  (-. (p401 zenon_Vuka))
% 9.88/10.17  (-. (p509 zenon_Vig))
% 9.88/10.17  (-. (p104 zenon_Vqda))
% 9.88/10.17  (-. (p303 zenon_Vrfa))
% 9.88/10.17  (r1 zenon_Vsn zenon_Vun)
% 9.88/10.17  (-. (p203 zenon_Vmga))
% 9.88/10.17  (-. (p207 zenon_Vgs))
% 9.88/10.17  (-. (p110 zenon_Vie))
% 9.88/10.17  (-. (p103 zenon_Veha))
% 9.88/10.17  (-. (p401 zenon_Vtka))
% 9.88/10.17  (r1 zenon_Vir zenon_Vkr)
% 9.88/10.17  (r1 zenon_Vhu zenon_Viu)
% 9.88/10.17  (-. (p406 zenon_Vsu))
% 9.88/10.17  (-. (p409 zenon_Vfh))
% 9.88/10.17  (r1 zenon_Vtz zenon_Vuz)
% 9.88/10.17  (-. (p301 zenon_Vzka))
% 9.88/10.17  (-. (p308 zenon_Vxm))
% 9.88/10.17  (-. (p304 zenon_Vlca))
% 9.88/10.17  (r1 zenon_Vjl zenon_Vkl)
% 9.88/10.17  (-. (p108 zenon_Vlo))
% 9.88/10.17  (r1 zenon_Vlu zenon_Vmu)
% 9.88/10.17  (-. (p504 zenon_Vvba))
% 9.88/10.17  (-. (p1010 zenon_Vm))
% 9.88/10.17  (-. (p404 zenon_Veca))
% 9.88/10.17  (r1 zenon_Vvs zenon_Vws)
% 9.88/10.17  (-. (p102 zenon_Vuja))
% 9.88/10.17  (r1 zenon_Vcr zenon_Vdr)
% 9.88/10.17  (-. (p701 zenon_Veka))
% 9.88/10.17  (-. (p106 zenon_Vuw))
% 9.88/10.17  (r1 zenon_Vgh zenon_Vih)
% 9.88/10.17  (-. (p104 zenon_Vaea))
% 9.88/10.17  (-. (p305 zenon_Vzy))
% 9.88/10.17  (-. (p104 zenon_Vuda))
% 9.88/10.17  (r1 zenon_Vxfa zenon_Vyfa)
% 9.88/10.17  (-. (p501 zenon_Vkka))
% 9.88/10.17  (-. (p910 zenon_Vq))
% 9.88/10.17  (r1 zenon_Viz zenon_Vjz)
% 9.88/10.17  (-. (p610 zenon_Vja))
% 9.88/10.17  (-. (p305 zenon_Vxy))
% 9.88/10.17  (r1 zenon_Viy zenon_Vjy)
% 9.88/10.17  (-. (p502 zenon_Vzha))
% 9.88/10.17  (r1 zenon_Vgn zenon_Vhn)
% 9.88/10.17  (r1 zenon_Vde zenon_Vfe)
% 9.88/10.17  (-. (p407 zenon_Vxq))
% 9.88/10.17  (r1 zenon_Vfa zenon_Vha)
% 9.88/10.17  (r1 zenon_Vwi zenon_Vyi)
% 9.88/10.17  (-. (p104 zenon_Veea))
% 9.88/10.17  (r1 zenon_Vyn zenon_Vao)
% 9.88/10.17  (p1101 Tau_0)
% 9.88/10.17  (-. (p401 zenon_Vska))
% 9.88/10.17  (r1 zenon_Vzr zenon_Vas)
% 9.88/10.17  (-. (p106 zenon_Vdx))
% 9.88/10.17  (-. (p606 zenon_Vxt))
% 9.88/10.17  (r1 zenon_Vye zenon_Vaf)
% 9.88/10.17  (-. (p304 zenon_Vpca))
% 9.88/10.17  (r1 zenon_Vvu zenon_Vwu)
% 9.88/10.17  (-. (p109 zenon_Vwj))
% 9.88/10.17  (-. (p106 zenon_Vqw))
% 9.88/10.17  (-. (p303 zenon_Vufa))
% 9.88/10.17  (r1 zenon_Vhja zenon_Vija)
% 9.88/10.17  (-. (p210 zenon_Vjd))
% 9.88/10.17  (-. (p609 zenon_Veg))
% 9.88/10.17  (r1 zenon_Vlp zenon_Vmp)
% 9.88/10.17  (-. (p906 zenon_Vot))
% 9.88/10.17  (-. (p301 zenon_Vala))
% 9.88/10.17  (-. (p505 zenon_Vhy))
% 9.88/10.17  (r1 zenon_Vuk zenon_Vvk)
% 9.88/10.17  (-. (p309 zenon_Vgi))
% 9.88/10.17  (r1 zenon_Vjh zenon_Vlh)
% 9.88/10.17  (-. (p301 zenon_Vela))
% 9.88/10.17  (-. (p305 zenon_Vbz))
% 9.88/10.17  (r1 zenon_Vem zenon_Vgm)
% 9.88/10.17  (r1 zenon_Vnd zenon_Vpd)
% 9.88/10.17  (r1 zenon_Vgc zenon_Vhc)
% 9.88/10.17  (-. (p110 zenon_Vxe))
% 9.88/10.17  (-. (p406 zenon_Vyu))
% 9.88/10.17  (-. (p309 zenon_Vai))
% 9.88/10.17  (Tau_0 != zenon_Vvja)
% 9.88/10.17  (Tau_0 != zenon_Vwja)
% 9.88/10.17  (Tau_0 != zenon_Vxja)
% 9.88/10.17  (Tau_0 != zenon_Vyja)
% 9.88/10.17  (Tau_0 != zenon_Vzja)
% 9.88/10.17  (Tau_0 != zenon_Vaka)
% 9.88/10.17  (Tau_0 != zenon_Vbka)
% 9.88/10.17  (Tau_0 != zenon_Vcka)
% 9.88/10.17  (Tau_0 != zenon_Vdka)
% 9.88/10.17  (Tau_0 != zenon_Veka)
% 9.88/10.17  (Tau_0 != zenon_Vfka)
% 9.88/10.17  (Tau_0 != zenon_Vgka)
% 9.88/10.17  (Tau_0 != zenon_Vhka)
% 9.88/10.17  (Tau_0 != zenon_Vika)
% 9.88/10.17  (Tau_0 != zenon_Vjka)
% 9.88/10.17  (Tau_0 != zenon_Vkka)
% 9.88/10.17  (Tau_0 != zenon_Vlka)
% 9.88/10.17  (Tau_0 != zenon_Vmka)
% 9.88/10.17  (Tau_0 != zenon_Vnka)
% 9.88/10.17  (Tau_0 != zenon_Voka)
% 9.88/10.17  (Tau_0 != zenon_Vpka)
% 9.88/10.17  (Tau_0 != zenon_Vqka)
% 9.88/10.17  (Tau_0 != zenon_Vrka)
% 9.88/10.17  (Tau_0 != zenon_Vska)
% 9.88/10.17  (Tau_0 != zenon_Vtka)
% 9.88/10.17  (Tau_0 != zenon_Vuka)
% 9.88/10.17  (Tau_0 != zenon_Vvka)
% 9.88/10.17  (Tau_0 != zenon_Vwka)
% 9.88/10.17  (Tau_0 != zenon_Vxka)
% 9.88/10.17  (Tau_0 != zenon_Vyka)
% 9.88/10.17  (Tau_0 != zenon_Vzka)
% 9.88/10.17  (Tau_0 != zenon_Vala)
% 9.88/10.17  (Tau_0 != zenon_Vbla)
% 9.88/10.17  (Tau_0 != zenon_Vcla)
% 9.88/10.17  (Tau_0 != zenon_Vdla)
% 9.88/10.17  (Tau_0 != zenon_Vela)
% 9.88/10.17  (Tau_0 != zenon_Vfla)
% 9.88/10.17  (Tau_0 != zenon_Vgla)
% 9.88/10.17  (Tau_0 != zenon_Vhla)
% 9.88/10.17  (Tau_0 != zenon_Vila)
% 9.88/10.17  (Tau_0 != zenon_Vjla)
% 9.88/10.17  (Tau_0 != zenon_Vkla)
% 9.88/10.17  (Tau_0 != zenon_Vlla)
% 9.88/10.17  (Tau_0 != zenon_Vmla)
% 9.88/10.17  (Tau_0 != zenon_Vnla)
% 9.88/10.17  (Tau_0 != zenon_Vola)
% 9.88/10.17  (Tau_0 != zenon_Vpla)
% 9.88/10.17  (Tau_0 != zenon_Vqla)
% 9.88/10.17  (Tau_0 != zenon_Vrla)
% 9.88/10.17  (Tau_0 != zenon_Vsla)
% 9.88/10.17  (Tau_0 != zenon_Vtla)
% 9.88/10.17  (Tau_0 != zenon_Vula)
% 9.88/10.17  (Tau_0 != zenon_Vvla)
% 9.88/10.17  (Tau_0 != zenon_Vwla)
% 9.88/10.17  (Tau_0 != zenon_Vxla)
% 9.88/10.17  (-. (p310 zenon_Vhc))
% 9.88/10.17  (-. (p202 zenon_Vaja))
% 9.88/10.17  (r1 zenon_Vqh zenon_Vrh)
% 9.88/10.17  (-. (p209 zenon_Vii))
% 9.88/10.17  (-. (p208 zenon_Vrn))
% 9.88/10.17  (-. (p807 zenon_Vgp))
% 9.88/10.17  (-. (p207 zenon_Vms))
% 9.88/10.17  (r1 zenon_Vei zenon_Vgi)
% 9.88/10.17  (r1 zenon_Vji zenon_Vki)
% 9.88/10.17  (r1 zenon_Vef zenon_Vff)
% 9.88/10.17  (r1 zenon_Vwy zenon_Vxy)
% 9.88/10.17  (-. (p206 zenon_Vzv))
% 9.88/10.17  (-. (p201 zenon_Vfla))
% 9.88/10.17  (-. (p810 zenon_Vx))
% 9.88/10.17  (r1 zenon_Vvb zenon_Vxb)
% 9.88/10.17  (-. (p309 zenon_Vdi))
% 9.88/10.17  (r1 zenon_Vvp zenon_Vwp)
% 9.88/10.17  (-. (p202 zenon_Vxia))
% 9.88/10.17  (r1 zenon_Vbc zenon_Vdc)
% 9.88/10.17  (-. (p105 zenon_Vaba))
% 9.88/10.17  (-. (p507 zenon_Vhq))
% 9.88/10.17  (-. (p203 zenon_Vega))
% 9.88/10.17  (r1 zenon_Vzda zenon_Vaea)
% 9.88/10.17  (r1 zenon_Vbo zenon_Vco)
% 9.88/10.17  (-. (p607 zenon_Vsp))
% 9.88/10.17  (-. (p606 zenon_Vyt))
% 9.88/10.17  (-. (p210 zenon_Vdd))
% 9.88/10.17  (-. (p710 zenon_Vea))
% 9.88/10.17  (r1 zenon_Vsy zenon_Vty)
% 9.88/10.17  (-. (p701 zenon_Vdka))
% 9.88/10.17  (-. (p304 zenon_Vnca))
% 9.88/10.17  (r1 zenon_Vkq zenon_Vlq)
% 9.88/10.17  (r1 zenon_Vrv zenon_Vtv)
% 9.88/10.17  (r1 zenon_Vica zenon_Vjca)
% 9.88/10.17  (-. (p510 zenon_Veb))
% 9.88/10.17  (r1 zenon_Vdea zenon_Veea)
% 9.88/10.17  (-. (p909 zenon_Vdf))
% 9.88/10.17  (-. (p404 zenon_Vzba))
% 9.88/10.17  (r1 zenon_Vvz zenon_Vwz)
% 9.88/10.17  (-. (p302 zenon_Vkia))
% 9.88/10.17  (-. (p110 zenon_Voe))
% 9.88/10.17  (-. (p209 zenon_Vpi))
% 9.88/10.17  (r1 zenon_Vtl zenon_Vul)
% 9.88/10.17  (-. (p806 zenon_Vpt))
% 9.88/10.17  (-. (p802 zenon_Vlha))
% 9.88/10.17  (r1 zenon_Vvaa zenon_Vxaa)
% 9.88/10.17  (p501 Tau_0)
% 9.88/10.17  (r1 zenon_Vfu zenon_Vgu)
% 9.88/10.17  (-. (p709 zenon_Vpf))
% 9.88/10.17  (r1 zenon_Vgda zenon_Vhda)
% 9.88/10.17  (r1 zenon_Vug zenon_Vvg)
% 9.88/10.17  (-. (p105 zenon_Vqaa))
% 9.88/10.17  (p901 Tau_0)
% 9.88/10.17  (r1 zenon_Vgf zenon_Vhf)
% 9.88/10.17  (-. (p203 zenon_Vwfa))
% 9.88/10.17  (-. (p410 zenon_Vob))
% 9.88/10.17  (-. (p510 zenon_Vhb))
% 9.88/10.17  (r1 zenon_Vjj zenon_Vkj)
% 9.88/10.17  (-. (p710 zenon_Vba))
% 9.88/10.17  (-. (p603 zenon_Vyea))
% 9.88/10.17  (r1 zenon_Vpp zenon_Vqp)
% 9.88/10.17  (-. (p403 zenon_Vmfa))
% 9.88/10.17  (r1 zenon_Vsh zenon_Vuh)
% 9.88/10.17  (-. (p404 zenon_Vbca))
% 9.88/10.17  (-. (p206 zenon_Vfw))
% 9.88/10.17  (-. (p304 zenon_Vvca))
% 9.88/10.17  (r1 zenon_Vmq zenon_Vnq)
% 9.88/10.17  (r1 zenon_Vuy zenon_Vvy)
% 9.88/10.17  (r1 zenon_Vzz zenon_Vaaa)
% 9.88/10.17  (-. (p204 zenon_Vfda))
% 9.88/10.17  (-. (p207 zenon_Vur))
% 9.88/10.17  (r1 zenon_Vsm zenon_Vum)
% 9.88/10.17  (-. (p703 zenon_Vrea))
% 9.88/10.17  (r1 zenon_Vvn zenon_Vxn)
% 9.88/10.17  (-. (p706 zenon_Vtt))
% 9.88/10.17  (-. (p307 zenon_Vdr))
% 9.88/10.17  (-. (p507 zenon_Vcq))
% 9.88/10.17  (r1 zenon_Vkda zenon_Vlda)
% 9.88/10.17  (-. (p303 zenon_Vofa))
% 9.88/10.17  (-. (p308 zenon_Vum))
% 9.88/10.17  (-. (p310 zenon_Vwc))
% 9.88/10.17  (-. (p210 zenon_Vvd))
% 9.88/10.17  (r1 zenon_Vka zenon_Vla)
% 9.88/10.17  (-. (p910 zenon_Vo))
% 9.88/10.17  (r1 zenon_Vex zenon_Vgx)
% 9.88/10.17  (r1 zenon_Ved zenon_Vgd)
% 9.88/10.17  (-. (p107 zenon_Vft))
% 9.88/10.17  (-. (p206 zenon_Vow))
% 9.88/10.17  (-. (p402 zenon_Viia))
% 9.88/10.17  (-. (p104 zenon_Vcea))
% 9.88/10.17  (-. (p403 zenon_Vifa))
% 9.88/10.17  (r1 zenon_Vtp zenon_Vup)
% 9.88/10.17  (r1 zenon_Vgr zenon_Vhr)
% 9.88/10.17  (r1 zenon_Vfg zenon_Vgg)
% 9.88/10.17  (-. (p205 zenon_Vdaa))
% 9.88/10.17  (-. (p101 zenon_Vrla))
% 9.88/10.17  (r1 zenon_Vmf zenon_Vnf)
% 9.88/10.17  (r1 zenon_Vwca zenon_Vxca)
% 9.88/10.17  (r1 zenon_Vmv zenon_Vnv)
% 9.88/10.17  (-. (p602 zenon_Vsha))
% 9.88/10.17  (-. (p201 zenon_Vjla))
% 9.88/10.17  (-. (p208 zenon_Vao))
% 9.88/10.17  (p301 Tau_0)
% 9.88/10.17  (r1 zenon_Vpga zenon_Vqga)
% 9.88/10.17  (-. (p102 zenon_Vcja))
% 9.88/10.17  (-. (p301 zenon_Vcla))
% 9.88/10.17  (-. (p405 zenon_Vvy))
% 9.88/10.17  (r1 zenon_Vns zenon_Vos)
% 9.88/10.17  (-. (p501 zenon_Vmka))
% 9.88/10.17  (-. (p106 zenon_Vww))
% 9.88/10.17  (-. (p304 zenon_Vjca))
% 9.88/10.17  (-. (p209 zenon_Vyi))
% 9.88/10.17  (r1 zenon_Vdo zenon_Veo)
% 9.88/10.17  (r1 zenon_Vok zenon_Vpk)
% 9.88/10.17  (r1 zenon_Vlj zenon_Vnj)
% 9.88/10.17  (r1 zenon_Vtd zenon_Vvd)
% 9.88/10.17  (-. (p409 zenon_Vch))
% 9.88/10.17  (-. (p406 zenon_Vou))
% 9.88/10.17  (-. (p207 zenon_Vds))
% 9.88/10.17  (-. (p205 zenon_Vgaa))
% 9.88/10.17  (-. (p102 zenon_Vsja))
% 9.88/10.17  (-. (p708 zenon_Vtk))
% 9.88/10.17  (r1 zenon_Vtw zenon_Vuw)
% 9.88/10.17  (-. (p104 zenon_Vsda))
% 9.88/10.17  (-. (p906 zenon_Vnt))
% 9.88/10.17  (r1 zenon_Vsb zenon_Vub)
% 9.88/10.17  (-. (p1007 zenon_Vbp))
% 9.88/10.17  (r1 zenon_Vcl zenon_Vel)
% 9.88/10.17  (-. (p708 zenon_Vnk))
% 9.88/10.17  (r1 zenon_Vqi zenon_Vsi)
% 9.88/10.17  (r1 zenon_Vju zenon_Vku)
% 9.88/10.17  (-. (p603 zenon_Vxea))
% 9.88/10.17  (-. (p501 zenon_Vlka))
% 9.88/10.17  (-. (p306 zenon_Vfv))
% 9.88/10.17  (-. (p202 zenon_Vuia))
% 9.88/10.17  (-. (p205 zenon_Vwz))
% 9.88/10.17  (-. (p902 zenon_Vjha))
% 9.88/10.17  (-. (p605 zenon_Vay))
% 9.88/10.17  (r1 zenon_Vfj zenon_Vgj)
% 9.88/10.17  (-. (p107 zenon_Vit))
% 9.88/10.17  (r1 zenon_Vraa zenon_Vsaa)
% 9.88/10.17  (-. (p501 zenon_Vpka))
% 9.88/10.17  (r1 zenon_Vpe zenon_Vre)
% 9.88/10.17  (p401 Tau_0)
% 9.88/10.17  (-. (p608 zenon_Vzk))
% 9.88/10.17  (r1 zenon_Vca zenon_Vea)
% 9.88/10.17  (r1 zenon_Vge zenon_Vie)
% 9.88/10.17  (-. (p203 zenon_Vaga))
% 9.88/10.17  (-. (p601 zenon_Vjka))
% 9.88/10.17  (r1 zenon_Vkd zenon_Vmd)
% 9.88/10.17  (r1 zenon_Vbi zenon_Vdi)
% 9.88/10.17  (-. (p209 zenon_Vsi))
% 9.88/10.17  (r1 zenon_Vkv zenon_Vlv)
% 9.88/10.17  (-. (p506 zenon_Viu))
% 9.88/10.17  (r1 zenon_Vev zenon_Vfv)
% 9.88/10.17  (-. (p308 zenon_Vrm))
% 9.88/10.17  (-. (p203 zenon_Vcga))
% 9.88/10.17  (r1 zenon_Vec zenon_Vfc)
% 9.88/10.17  (r1 zenon_Vmn zenon_Von)
% 9.88/10.17  (r1 zenon_Vvfa zenon_Vwfa)
% 9.88/10.17  (-. (p604 zenon_Vqba))
% 9.88/10.17  (-. (p607 zenon_Vmp))
% 9.88/10.17  (-. (p508 zenon_Vgl))
% 9.88/10.17  (-. (p105 zenon_Vsaa))
% 9.88/10.17  (p101 Tau_0)
% 9.88/10.17  (r1 zenon_Vlc zenon_Vnc)
% 9.88/10.17  (r1 zenon_Vvr zenon_Vwr)
% 9.88/10.18  (r1 zenon_Vvq zenon_Vxq)
% 9.88/10.18  (-. (p703 zenon_Vuea))
% 9.88/10.18  (r1 zenon_Vcd zenon_Vdd)
% 9.88/10.18  (r1 zenon_Vso zenon_Vuo)
% 9.88/10.18  (-. (p309 zenon_Vrh))
% 9.88/10.18  (-. (p103 zenon_Vyga))
% 9.88/10.18  (-. (p107 zenon_Vss))
% 9.88/10.18  (-. (p503 zenon_Vbfa))
% 9.88/10.18  (r1 zenon_Vse zenon_Vue)
% 9.88/10.18  (r1 zenon_Viv zenon_Vjv)
% 9.88/10.18  (-. (p701 zenon_Vbka))
% 9.88/10.18  (r1 zenon_Vzd zenon_Vae)
% 9.88/10.18  (r1 zenon_Vxf zenon_Vyf)
% 9.88/10.18  (r1 zenon_Vnja zenon_Voja)
% 9.88/10.18  (-. (p608 zenon_Vbl))
% 9.88/10.18  (r1 zenon_Vhi zenon_Vii)
% 9.88/10.18  (-. (p403 zenon_Vgfa))
% 9.88/10.18  (r1 zenon_Vkca zenon_Vlca)
% 9.88/10.18  (-. (p103 zenon_Voga))
% 9.88/10.18  (-. (p210 zenon_Vyd))
% 9.88/10.18  (r1 zenon_Vdk zenon_Vfk)
% 9.88/10.18  (-. (p608 zenon_Vxk))
% 9.88/10.18  (-. (p701 zenon_Vcka))
% 9.88/10.18  (r1 zenon_Vnb zenon_Vob)
% 9.88/10.18  (-. (p602 zenon_Vuha))
% 9.88/10.18  (-. (p204 zenon_Voda))
% 9.88/10.18  (r1 zenon_Vni zenon_Vpi)
% 9.88/10.18  (p701 Tau_0)
% 9.88/10.18  (-. (p503 zenon_Vafa))
% 9.88/10.18  (-. (p509 zenon_Vqg))
% 9.88/10.18  (-. (p208 zenon_Vun))
% 9.88/10.18  (-. (p605 zenon_Vxx))
% 9.88/10.18  (r1 zenon_Vsa zenon_Vua)
% 9.88/10.18  (-. (p507 zenon_Vwp))
% 9.88/10.18  (-. (p204 zenon_Vzca))
% 9.88/10.18  (-. (p405 zenon_Vjy))
% 9.88/10.18  (-. (p309 zenon_Vxh))
% 9.88/10.18  (-. (p210 zenon_Vgd))
% 9.88/10.18  (-. (p109 zenon_Vkj))
% 9.88/10.18  (-. (p206 zenon_Vlw))
% 9.88/10.18  (-. (p204 zenon_Vxca))
% 9.88/10.18  (-. (p505 zenon_Vgy))
% 9.88/10.18  (-. (p702 zenon_Vqha))
% 9.88/10.18  (-. (p307 zenon_Vbr))
% 9.88/10.18  (-. (p107 zenon_Vlt))
% 9.88/10.18  (-. (p605 zenon_Vzx))
% 9.88/10.18  (r1 zenon_Vcb zenon_Veb)
% 9.88/10.18  (r1 zenon_Vvf zenon_Vwf)
% 9.88/10.18  (r1 zenon_Vr zenon_Vs)
% 9.88/10.18  (-. (p308 zenon_Vdn))
% 9.88/10.18  (-. (p506 zenon_Vmu))
% 9.88/10.18  (-. (p508 zenon_Vkl))
% 9.88/10.18  (-. (p103 zenon_Vqga))
% 9.88/10.18  (-. (p404 zenon_Vaca))
% 9.88/10.18  (-. (p508 zenon_Vpl))
% 9.88/10.18  (r1 zenon_Vsq zenon_Vuq)
% 9.88/10.18  (r1 zenon_Vlg zenon_Vng)
% 9.88/10.18  (-. (p308 zenon_Vlm))
% 9.88/10.18  (-. (p107 zenon_Vws))
% 9.88/10.18  (-. (p105 zenon_Vdba))
% 9.88/10.18  (-. (p409 zenon_Vvg))
% 9.88/10.18  (-. (p310 zenon_Vnc))
% 9.88/10.18  (r1 zenon_Vin zenon_Vjn)
% 9.88/10.18  (r1 zenon_Vtu zenon_Vuu)
% 9.88/10.18  (r1 zenon_Vpaa zenon_Vqaa)
% 9.88/10.18  (r1 zenon_Vdt zenon_Vft)
% 9.88/10.18  (r1 zenon_Vhaa zenon_Viaa)
% 9.88/10.18  (-. (p408 zenon_Vyl))
% 9.88/10.18  (r1 zenon_Vfea zenon_Vhea)
% 9.88/10.18  (-. (p509 zenon_Vkg))
% 9.88/10.18  (-. (p310 zenon_Vfc))
% 9.88/10.18  (-. (p503 zenon_Vffa))
% 9.88/10.18  (-. (p108 zenon_Vro))
% 9.88/10.18  (-. (p109 zenon_Vqj))
% 9.88/10.18  (-. (p303 zenon_Vsfa))
% 9.88/10.18  (r1 zenon_Vbn zenon_Vdn)
% 9.88/10.18  (-. (p202 zenon_Vzia))
% 9.88/10.18  (-. (p106 zenon_Vax))
% 9.88/10.18  (-. (p107 zenon_Vus))
% 9.88/10.18  (r1 zenon_Vbu zenon_Vcu)
% 9.88/10.18  (r1 zenon_Vlr zenon_Vnr)
% 9.88/10.18  (r1 zenon_Vxda zenon_Vyda)
% 9.88/10.18  (r1 zenon_Vxw zenon_Vyw)
% 9.88/10.18  (-. (p106 zenon_Vmx))
% 9.88/10.18  (-. (p801 zenon_Vyja))
% 9.88/10.18  (r1 zenon_Vxp zenon_Vyp)
% 9.88/10.18  (r1 zenon_Vbe zenon_Vce)
% 9.88/10.18  (r1 zenon_Vad zenon_Vbd)
% 9.88/10.18  (-. (p105 zenon_Vuaa))
% 9.88/10.18  (r1 zenon_Vsk zenon_Vtk)
% 9.88/10.18  (-. (p907 zenon_Vcp))
% 9.88/10.18  (r1 zenon_Vida zenon_Vjda)
% 9.88/10.18  (-. (p204 zenon_Vjda))
% 9.88/10.18  (-. (p306 zenon_Vqv))
% 9.88/10.18  (-. (p904 zenon_Vgba))
% 9.88/10.18  (r1 zenon_Vzga zenon_Vaha)
% 9.88/10.18  (-. (p705 zenon_Vtx))
% 9.88/10.18  (r1 zenon_Vtga zenon_Vuga)
% 9.88/10.18  (-. (p704 zenon_Vlba))
% 9.88/10.18  (r1 zenon_Vak zenon_Vck)
% 9.88/10.18  (r1 zenon_Vnu zenon_Vou)
% 9.88/10.18  (r1 zenon_Vjga zenon_Vkga)
% 9.88/10.18  (r1 zenon_Vrc zenon_Vtc)
% 9.88/10.18  (-. (p303 zenon_Vpfa))
% 9.88/10.18  (-. (p305 zenon_Vmz))
% 9.88/10.18  (-. (p209 zenon_Vvi))
% 9.88/10.18  (-. (p505 zenon_Vey))
% 9.88/10.18  (-. (p109 zenon_Vzj))
% 9.88/10.18  (-. (p609 zenon_Vuf))
% 9.88/10.18  (-. (p307 zenon_Vqr))
% 9.88/10.18  (-. (p208 zenon_Vhn))
% 9.88/10.18  (-. (p709 zenon_Vnf))
% 9.88/10.18  (r1 zenon_Vxj zenon_Vzj)
% 9.88/10.18  (r1 zenon_Vhs zenon_Vjs)
% 9.88/10.18  (-. (p405 zenon_Vpy))
% 9.88/10.18  (-. (p208 zenon_Vfn))
% 9.88/10.18  (-. (p507 zenon_Vaq))
% 9.88/10.18  (-. (p110 zenon_Vue))
% 9.88/10.18  (-. (p308 zenon_Vnm))
% 9.88/10.18  (-. (p302 zenon_Vlia))
% 9.88/10.18  (-. (p207 zenon_Vwr))
% 9.88/10.18  (r1 zenon_Vmca zenon_Vnca)
% 9.88/10.18  (r1 zenon_Vyk zenon_Vzk)
% 9.88/10.18  (-. (p206 zenon_Vbw))
% 9.88/10.18  (-. (p709 zenon_Vlf))
% 9.88/10.18  (-. (p709 zenon_Vsf))
% 9.88/10.18  (-. (p504 zenon_Vwba))
% 9.88/10.18  (-. (p405 zenon_Vty))
% 9.88/10.18  (-. (p102 zenon_Vqja))
% 9.88/10.18  (p1001 Tau_0)
% 9.88/10.18  (-. (p609 zenon_Vbg))
% 9.88/10.18  (r1 zenon_Vbx zenon_Vdx)
% 9.88/10.18  (-. (p304 zenon_Vrca))
% 9.88/10.18  (r1 zenon_Vxs zenon_Vzs)
% 9.88/10.18  (r1 zenon_Vrda zenon_Vsda)
% 9.88/10.18  (r1 zenon_Vgt zenon_Vit)
% 9.88/10.18  (r1 zenon_Vvh zenon_Vxh)
% 9.88/10.18  (-. (p207 zenon_Vsr))
% 9.88/10.18  (-. (p807 zenon_Vep))
% 9.88/10.18  (-. (p104 zenon_Vwda))
% 9.88/10.18  (r1 zenon_Vcda zenon_Vdda)
% 9.88/10.18  (r1 zenon_Vlga zenon_Vmga)
% 9.88/10.18  (r1 zenon_Vkn zenon_Vln)
% 9.88/10.18  (-. (p207 zenon_Vjs))
% 9.88/10.18  (-. (p201 zenon_Vmla))
% 9.88/10.18  (r1 zenon_Vov zenon_Vqv)
% 9.88/10.18  (-. (p208 zenon_Vln))
% 9.88/10.18  (r1 zenon_Vaw zenon_Vbw)
% 9.88/10.18  (r1 zenon_Vqca zenon_Vrca)
% 9.88/10.18  (-. (p109 zenon_Vfk))
% 9.88/10.18  (-. (p306 zenon_Vjv))
% 9.88/10.18  (-. (p507 zenon_Vyp))
% 9.88/10.18  (-. (p509 zenon_Vtg))
% 9.88/10.18  (-. (p804 zenon_Viba))
% 9.88/10.18  (-. (p106 zenon_Vsw))
% 9.88/10.18  (-. (p508 zenon_Vsl))
% 9.88/10.18  (-. (p804 zenon_Vhba))
% 9.88/10.18  (-. (p602 zenon_Vtha))
% 9.88/10.18  (-. (p304 zenon_Vhca))
% 9.88/10.18  (-. (p202 zenon_Vvia))
% 9.88/10.18  (-. (p408 zenon_Vdm))
% 9.88/10.18  (-. (p606 zenon_Vau))
% 9.88/10.18  (-. (p307 zenon_Vfr))
% 9.88/10.18  (-. (p805 zenon_Vsx))
% 9.88/10.18  (-. (p309 zenon_Vph))
% 9.88/10.18  (r1 zenon_Vve zenon_Vxe)
% 9.88/10.18  (-. (p706 zenon_Vst))
% 9.88/10.18  (-. (p102 zenon_Vija))
% 9.88/10.18  (-. (p109 zenon_Vck))
% 9.88/10.18  (-. (p102 zenon_Veja))
% 9.88/10.18  (-. (p605 zenon_Vby))
% 9.88/10.18  (r1 zenon_Vbq zenon_Vcq)
% 9.88/10.18  (-. (p406 zenon_Vwu))
% 9.88/10.18  (r1 zenon_Vhg zenon_Vig)
% 9.88/10.18  (r1 zenon_Vrs zenon_Vss)
% 9.88/10.18  (-. (p408 zenon_Vwl))
% 9.88/10.18  (-. (p206 zenon_Viw))
% 9.88/10.18  (r1 zenon_Vrj zenon_Vtj)
% 9.88/10.18  (r1 zenon_Voq zenon_Vpq)
% 9.88/10.18  (r1 zenon_Vqk zenon_Vrk)
% 9.88/10.18  (r1 zenon_Vti zenon_Vvi)
% 9.88/10.18  (-. (p502 zenon_Vaia))
% 9.88/10.18  (r1 zenon_Vhm zenon_Vjm)
% 9.88/10.18  (r1 zenon_Vfja zenon_Vgja)
% 9.88/10.18  (-. (p310 zenon_Vqc))
% 9.88/10.18  (-. (p904 zenon_Vfba))
% 9.88/10.18  (-. (p307 zenon_Vzq))
% 9.88/10.18  (-. (p602 zenon_Vvha))
% 9.88/10.18  (-. (p206 zenon_Vvv))
% 9.88/10.18  (-. (p705 zenon_Vwx))
% 9.88/10.18  (r1 zenon_Vbja zenon_Vcja)
% 9.88/10.18  (-. (p605 zenon_Vyx))
% 9.88/10.18  (r1 zenon_Vvda zenon_Vwda)
% 9.88/10.18  (-. (p808 zenon_Vkk))
% 9.88/10.18  (-. (p903 zenon_Vmea))
% 9.88/10.18  (-. (p407 zenon_Vuq))
% 9.88/10.18  (r1 zenon_Vdga zenon_Vega)
% 9.88/10.18  (-. (p410 zenon_Vmb))
% 9.88/10.18  (-. (p604 zenon_Vsba))
% 9.88/10.18  (-. (p409 zenon_Vih))
% 9.88/10.18  (p707 zenon_Vkp)
% 9.88/10.18  (-. (p1004 zenon_Veba))
% 9.88/10.18  (-. (p103 zenon_Vhha))
% 9.88/10.18  (-. (p204 zenon_Vbda))
% 9.88/10.18  (r1 zenon_Vfb zenon_Vhb)
% 9.88/10.18  (-. (p201 zenon_Vgla))
% 9.88/10.18  (r1 zenon_Vt zenon_Vu)
% 9.88/10.18  (-. (p106 zenon_Vgx))
% 9.88/10.18  (-. (p704 zenon_Vmba))
% 9.88/10.18  (p801 Tau_0)
% 9.88/10.18  (r1 zenon_Vzp zenon_Vaq)
% 9.88/10.18  (-. (p207 zenon_Vas))
% 9.88/10.18  (r1 zenon_Vhd zenon_Vjd)
% 9.88/10.18  (-. (p1001 zenon_Vvja))
% 9.88/10.18  (-. (p107 zenon_Vct))
% 9.88/10.18  (-. (p502 zenon_Vbia))
% 9.88/10.18  (-. (p407 zenon_Vrq))
% 9.88/10.18  (r1 zenon_Voh zenon_Vph)
% 9.88/10.18  (-. (p704 zenon_Vnba))
% 9.88/10.18  (r1 zenon_Vll zenon_Vml)
% 9.88/10.18  (-. (p808 zenon_Vlk))
% 9.88/10.18  (-. (p504 zenon_Vyba))
% 9.88/10.18  (r1 zenon_Vmo zenon_Voo)
% 9.88/10.18  (-. (p108 zenon_Vxo))
% 9.88/10.18  (r1 zenon_Vbea zenon_Vcea)
% 9.88/10.18  (r1 zenon_Vuca zenon_Vvca)
% 9.88/10.18  (-. (p208 zenon_Vxn))
% 9.88/10.18  (-. (p606 zenon_Vzt))
% 9.88/10.18  (-. (p104 zenon_Vkea))
% 9.88/10.18  (-. (p401 zenon_Vrka))
% 9.88/10.18  (-. (p508 zenon_Vml))
% 9.88/10.18  (-. (p307 zenon_Vkr))
% 9.88/10.18  (-. (p210 zenon_Vsd))
% 9.88/10.18  (r1 zenon_Vzi zenon_Vbj)
% 9.88/10.18  (r1 zenon_Vxu zenon_Vyu)
% 9.88/10.18  (-. (p401 zenon_Vqka))
% 9.88/10.18  (-. (p506 zenon_Vcu))
% 9.88/10.18  (-. (p101 zenon_Vtla))
% 9.88/10.18  (r1 zenon_Vfl zenon_Vgl)
% 9.88/10.18  (r1 zenon_Vks zenon_Vms)
% 9.88/10.18  (r1 zenon_Voc zenon_Vqc)
% 9.88/10.18  (-. (p108 zenon_Vuo))
% 9.88/10.18  (-. (p403 zenon_Vkfa))
% 9.88/10.18  (-. (p907 zenon_Vdp))
% 9.88/10.18  (-. (p401 zenon_Vwka))
% 9.88/10.18  (r1 zenon_Vyv zenon_Vzv)
% 9.88/10.18  (r1 zenon_Vn zenon_Vo)
% 9.88/10.18  (-. (p105 zenon_Voaa))
% 9.88/10.18  (-. (p902 zenon_Vkha))
% 9.88/10.18  (r1 zenon_Vxa zenon_Vya)
% 9.88/10.18  (r1 zenon_Vjja zenon_Vkja)
% 9.88/10.18  (-. (p604 zenon_Voba))
% 9.88/10.18  (r1 zenon_Vps zenon_Vqs)
% 9.88/10.18  (-. (p106 zenon_Vjx))
% 9.88/10.18  (-. (p1002 zenon_Viha))
% 9.88/10.18  (-. (p402 zenon_Vfia))
% 9.88/10.18  (-. (p309 zenon_Vnh))
% 9.88/10.18  (r1 zenon_Vtr zenon_Vur)
% 9.88/10.18  (-. (p101 zenon_Vvla))
% 9.88/10.18  (-. (p509 zenon_Vng))
% 9.88/10.18  (r1 zenon_Vkz zenon_Vmz)
% 9.88/10.18  (r1 zenon_Vme zenon_Voe)
% 9.88/10.18  (r1 zenon_Vvo zenon_Vxo)
% 9.88/10.18  (-. (p502 zenon_Vcia))
% 9.88/10.18  (r1 zenon_Vfo zenon_Vgo)
% 9.88/10.18  (-. (p203 zenon_Vgga))
% 9.88/10.18  (-. (p410 zenon_Vdc))
% 9.88/10.18  (-. (p203 zenon_Vkga))
% 9.88/10.18  (-. (p905 zenon_Vox))
% 9.88/10.18  (-. (p210 zenon_Vmd))
% 9.88/10.18  (-. (p408 zenon_Vjm))
% 9.88/10.18  (-. (p802 zenon_Vnha))
% 9.88/10.18  (-. (p601 zenon_Vgka))
% 9.88/10.18  (-. (p109 zenon_Vtj))
% 9.88/10.18  (-. (p803 zenon_Voea))
% 9.88/10.18  (-. (p202 zenon_Vwia))
% 9.88/10.18  (-. (p105 zenon_Vxaa))
% 9.88/10.18  (-. (p905 zenon_Vpx))
% 9.88/10.18  (-. (p409 zenon_Vxg))
% 9.88/10.18  (-. (p203 zenon_Vyfa))
% 9.88/10.18  (-. (p110 zenon_Vce))
% 9.88/10.18  (r1 zenon_Vbm zenon_Vdm)
% 9.88/10.18  (-. (p306 zenon_Vlv))
% 9.88/10.18  (-. (p103 zenon_Vuga))
% 9.88/10.18  (p601 Tau_0)
% 9.88/10.18  (-. (p102 zenon_Vkja))
% 9.88/10.18  (-. (p310 zenon_Vtc))
% 9.88/10.18  (r1 zenon_Vru zenon_Vsu)
% 9.88/10.18  (-. (p810 zenon_Vu))
% 9.88/10.18  (r1 zenon_Vky zenon_Vly)
% 9.88/10.18  (-. (p702 zenon_Vrha))
% 9.88/10.18  (-. (p801 zenon_Vaka))
% 9.88/10.18  (r1 zenon_Vyh zenon_Vai)
% 9.88/10.18  (r1 zenon_Vwv zenon_Vxv)
% 9.88/10.18  (-. (p809 zenon_Vff))
% 9.88/10.18  (-. (p308 zenon_Vpm))
% 9.88/10.18  (-. (p402 zenon_Vgia))
% 9.88/10.18  (-. (p606 zenon_Vwt))
% 9.88/10.18  (r1 zenon_Vrja zenon_Vsja)
% 9.88/10.18  (-. (p202 zenon_Vsia))
% 9.88/10.18  (-. (p107 zenon_Vqs))
% 9.88/10.18  (r1 zenon_Vqf zenon_Vsf)
% 9.88/10.18  (r1 zenon_Vcv zenon_Vdv)
% 9.88/10.18  (-. (p603 zenon_Vvea))
% 9.88/10.18  (-. (p310 zenon_Vzc))
% 9.88/10.18  (-. (p403 zenon_Vlfa))
% 9.88/10.18  (-. (p101 zenon_Vqla))
% 9.88/10.18  (r1 zenon_Viq zenon_Vjq)
% 9.88/10.18  (-. (p705 zenon_Vux))
% 9.88/10.18  (r1 zenon_Vhga zenon_Viga)
% 9.88/10.18  (-. (p1005 zenon_Vnx))
% 9.88/10.18  (-. (p205 zenon_Vqz))
% 9.88/10.18  (-. (p109 zenon_Vgj))
% 9.88/10.18  (-. (p705 zenon_Vvx))
% 9.88/10.18  (-. (p806 zenon_Vqt))
% 9.88/10.18  (-. (p107 zenon_Vos))
% 9.88/10.18  (-. (p706 zenon_Vut))
% 9.88/10.18  (r1 zenon_Vjw zenon_Vlw)
% 9.88/10.18  (r1 zenon_Vwd zenon_Vyd)
% 9.88/10.18  (-. (p108 zenon_Veo))
% 9.88/10.18  (-. (p307 zenon_Vnr))
% 9.88/10.18  (r1 zenon_Vmk zenon_Vnk)
% 9.88/10.18  (-. (p805 zenon_Vrx))
% 9.88/10.18  (r1 zenon_Vcz zenon_Vdz)
% 9.88/10.18  (-. (p608 zenon_Vvk))
% 9.88/10.18  (r1 zenon_Vqq zenon_Vrq)
% 9.88/10.18  (-. (p201 zenon_Vlla))
% 9.88/10.18  (-. (p703 zenon_Vsea))
% 9.88/10.18  (r1 zenon_Vdu zenon_Veu)
% 9.88/10.18  (-. (p204 zenon_Vlda))
% 9.88/10.18  (-. (p108 zenon_Vgo))
% 9.88/10.18  (-. (p301 zenon_Vdla))
% 9.88/10.18  (r1 zenon_Vli zenon_Vmi)
% 9.88/10.18  (-. (p501 zenon_Voka))
% 9.88/10.18  (r1 zenon_Vvga zenon_Vwga)
% 9.88/10.18  (r1 zenon_Vnga zenon_Voga)
% 9.88/10.18  (-. (p102 zenon_Voja))
% 9.88/10.18  (-. (p404 zenon_Vdca))
% 9.88/10.18  (-. (p610 zenon_Voa))
% 9.88/10.18  (-. (p301 zenon_Vbla))
% 9.88/10.18  (r1 zenon_Val zenon_Vbl)
% 9.88/10.18  (r1 zenon_Vdha zenon_Veha)
% 9.88/10.18  (-. (p607 zenon_Vop))
% 9.88/10.18  (-. (p805 zenon_Vqx))
% 9.88/10.18  (r1 zenon_Vp zenon_Vq)
% 9.88/10.18  (r1 zenon_Vma zenon_Voa)
% 9.88/10.18  (-. (p208 zenon_Vjn))
% 9.88/10.18  (-. (p908 zenon_Vik))
% 9.88/10.18  (-. (p208 zenon_Von))
% 9.88/10.18  (r1 zenon_Vdja zenon_Veja)
% 9.88/10.18  (-. (p610 zenon_Vra))
% 9.88/10.18  (r1 zenon_Vwk zenon_Vxk)
% 9.88/10.18  (-. (p803 zenon_Vqea))
% 9.88/10.18  (r1 zenon_Ver zenon_Vfr)
% 9.88/10.18  (r1 zenon_Vrp zenon_Vsp)
% 9.88/10.18  (-. (p510 zenon_Vya))
% 9.88/10.18  (-. (p407 zenon_Vpq))
% 9.88/10.18  (-. (p304 zenon_Vtca))
% 9.88/10.18  (r1 zenon_Vfq zenon_Vhq)
% 9.88/10.18  (-. (p809 zenon_Vjf))
% 9.88/10.18  (-. (p801 zenon_Vzja))
% 9.88/10.18  (r1 zenon_Vgz zenon_Vhz)
% 9.88/10.18  (r1 zenon_Vog zenon_Vqg)
% 9.88/10.18  (r1 zenon_Var zenon_Vbr)
% 9.88/10.18  (-. (p305 zenon_Vfz))
% 9.88/10.18  (r1 zenon_Vbba zenon_Vdba)
% 9.88/10.18  (r1 zenon_Vxr zenon_Vyr)
% 9.88/10.18  (-. (p609 zenon_Vwf))
% 9.88/10.18  (-. (p808 zenon_Vjk))
% 9.88/10.18  (-. (p608 zenon_Vel))
% 9.88/10.18  (-. (p401 zenon_Vvka))
% 9.88/10.18  (r1 zenon_Vva zenon_Vwa)
% 9.88/10.18  (r1 zenon_Vvl zenon_Vwl)
% 9.88/10.18  (r1 zenon_Vaa zenon_Vba)
% 9.88/10.18  (-. (p109 zenon_Vnj))
% 9.88/10.18  (-. (p505 zenon_Vcy))
% 9.88/10.18  (-. (p108 zenon_Voo))
% 9.88/10.18  (r1 zenon_Veda zenon_Vfda)
% 9.88/10.18  (r1 zenon_Vjo zenon_Vlo)
% 9.88/10.18  (-. (p209 zenon_Vej))
% 9.88/10.18  (r1 zenon_Vada zenon_Vbda)
% 9.88/10.18  (-. (p603 zenon_Vwea))
% 9.88/10.18  (r1 zenon_Vfga zenon_Vgga)
% 9.88/10.18  (r1 zenon_Vcj zenon_Vej)
% 9.88/10.18  (-. (p307 zenon_Vhr))
% 9.88/10.18  (-. (p209 zenon_Vmi))
% 9.88/10.18  (r1 zenon_Vmy zenon_Vny)
% 9.88/10.18  (r1 zenon_Vv zenon_Vx)
% 9.88/10.18  (-. (p205 zenon_Voz))
% 9.88/10.18  (r1 zenon_Vrz zenon_Vsz)
% 9.88/10.18  (-. (p205 zenon_Vsz))
% 9.88/10.18  (-. (p302 zenon_Vqia))
% 9.88/10.18  (-. (p410 zenon_Vac))
% 9.88/10.18  (r1 zenon_Vkf zenon_Vlf)
% 9.88/10.18  (r1 zenon_Vgv zenon_Vhv)
% 9.88/10.18  (-. (p110 zenon_Vfe))
% 9.88/10.18  (r1 zenon_Vlja zenon_Vmja)
% 9.88/10.18  (-. (p301 zenon_Vxka))
% 9.88/10.18  (r1 zenon_Vyca zenon_Vzca)
% 9.88/10.18  (r1 zenon_Voj zenon_Vqj)
% 9.88/10.18  (r1 zenon_Vof zenon_Vpf)
% 9.88/10.18  (r1 zenon_Vlaa zenon_Vmaa)
% 9.88/10.18  (r1 zenon_Vbha zenon_Vcha)
% 9.88/10.18  (-. (p909 zenon_Vcf))
% 9.88/10.18  (-. (p201 zenon_Vhla))
% 9.88/10.18  (r1 zenon_Vql zenon_Vsl)
% 9.88/10.18  (-. (p504 zenon_Vtba))
% 9.88/10.18  (-. (p408 zenon_Vam))
% 9.88/10.18  (r1 zenon_Vuc zenon_Vwc)
% 9.88/10.18  (r1 zenon_Vmm zenon_Vnm)
% 9.88/10.18  (-. (p405 zenon_Vly))
% 9.88/10.18  (-. (p601 zenon_Vfka))
% 9.88/10.18  (-. (p202 zenon_Vyia))
% 9.88/10.18  (r1 zenon_Vpw zenon_Vqw)
% 9.88/10.18  (r1 zenon_Vdh zenon_Vfh)
% 9.88/10.18  (-. (p201 zenon_Vkla))
% 9.88/10.18  (r1 zenon_Vcg zenon_Veg)
% 9.88/10.18  (-. (p506 zenon_Vgu))
% 9.88/10.18  (r1 zenon_Vzf zenon_Vbg)
% 9.88/10.18  (-. (p506 zenon_Veu))
% 9.88/10.18  (r1 zenon_Vqy zenon_Vry)
% 9.88/10.18  (-. (p202 zenon_Vtia))
% 9.88/10.18  (r1 zenon_Vxz zenon_Vyz)
% 9.88/10.18  (-. (p702 zenon_Voha))
% 9.88/10.18  (r1 zenon_Vzu zenon_Vbv)
% 9.88/10.18  (-. (p505 zenon_Vdy))
% 9.88/10.18  (r1 zenon_Vfha zenon_Vhha)
% 9.88/10.18  (-. (p303 zenon_Vnfa))
% 9.88/10.18  (r1 zenon_Ves zenon_Vgs)
% 9.88/10.18  (-. (p306 zenon_Vnv))
% 9.88/10.18  (-. (p302 zenon_Vpia))
% 9.88/10.18  (r1 zenon_Vez zenon_Vfz)
% 9.88/10.18  (-. (p407 zenon_Vnq))
% 9.88/10.18  (-. (p702 zenon_Vpha))
% 9.88/10.18  (-. (p405 zenon_Vry))
% 9.88/10.18  (r1 zenon_Vza zenon_Vbb)
% 9.88/10.18  (r1 zenon_Vew zenon_Vfw)
% 9.88/10.18  (-. (p105 zenon_Vkaa))
% 9.88/10.18  (-. (p101 zenon_Vola))
% 9.88/10.18  (p707 zenon_Vhp)
% 9.88/10.18  (-. (p410 zenon_Vub))
% 9.88/10.18  (r1 zenon_Vbga zenon_Vcga)
% 9.88/10.18  (-. (p706 zenon_Vvt))
% 9.88/10.18  (r1 zenon_Vyq zenon_Vzq)
% 9.88/10.18  (-. (p402 zenon_Vdia))
% 9.88/10.18  (r1 zenon_Vy zenon_Vz)
% 9.88/10.18  (-. (p209 zenon_Vki))
% 9.88/10.18  (r1 zenon_Vhj zenon_Vij)
% 9.88/10.18  (r1 zenon_Vho zenon_Vio)
% 9.88/10.18  (-. (p204 zenon_Vdda))
% 9.88/10.18  (-. (p703 zenon_Vtea))
% 9.88/10.18  (-. (p409 zenon_Vlh))
% 9.88/10.18  (r1 zenon_Vzw zenon_Vax)
% 9.88/10.18  (-. (p610 zenon_Vua))
% 9.88/10.18  (-. (p607 zenon_Vup))
% 9.88/10.18  (-. (p807 zenon_Vfp))
% 9.88/10.18  (-. (p108 zenon_Vap))
% 9.88/10.18  (r1 zenon_Voca zenon_Vpca)
% 9.88/10.18  (r1 zenon_Veaa zenon_Vgaa)
% 9.88/10.18  (r1 zenon_Vyo zenon_Vap)
% 9.88/10.18  (-. (p104 zenon_Vhea))
% 9.88/10.18  (-. (p309 zenon_Vuh))
% 9.88/10.18  (-. (p604 zenon_Vrba))
% 9.88/10.18  (-. (p301 zenon_Vyka))
% 9.88/10.18  (-. (p903 zenon_Vnea))
% 9.88/10.18  (r1 zenon_Vxl zenon_Vyl)
% 9.88/10.18  (-. (p410 zenon_Vrb))
% 9.88/10.18  (-. (p108 zenon_Vio))
% 9.88/10.18  (-. (p403 zenon_Vhfa))
% 9.88/10.18  (-. (p502 zenon_Vxha))
% 9.88/10.18  (-. (p404 zenon_Vfca))
% 9.88/10.18  (r1 zenon_Vrga zenon_Vsga)
% 9.88/10.18  (r1 zenon_Vkx zenon_Vmx)
% 9.88/10.18  (r1 zenon_Vkm zenon_Vlm)
% 9.88/10.18  (r1 zenon_Vqm zenon_Vrm)
% 9.88/10.18  (-. (p408 zenon_Vgm))
% 9.88/10.18  (r1 zenon_Vzl zenon_Vam)
% 9.88/10.18  (r1 zenon_Vpo zenon_Vro)
% 9.88/10.18  (-. (p810 zenon_Vs))
% 9.88/10.18  (-. (p302 zenon_Vria))
% 9.88/10.18  (-. (p604 zenon_Vpba))
% 9.88/10.18  (r1 zenon_Vic zenon_Vkc)
% 9.88/10.18  (-. (p204 zenon_Vhda))
% 9.88/10.18  (-. (p610 zenon_Vla))
% 9.88/10.18  (-. (p508 zenon_Vil))
% 9.88/10.18  (r1 zenon_Vyaa zenon_Vaba)
% 9.88/10.18  (-. (p710 zenon_Vz))
% 9.88/10.18  (r1 zenon_Vif zenon_Vjf)
% 9.88/10.18  (r1 zenon_Vym zenon_Van)
% 9.88/10.18  (r1 zenon_Vom zenon_Vpm)
% 9.88/10.18  (r1 zenon_Vat zenon_Vct)
% 9.88/10.18  (-. (p108 zenon_Vco))
% 9.88/10.18  (-. (p206 zenon_Vdw))
% 9.88/10.18  (-. (p803 zenon_Vpea))
% 9.88/10.18  (-. (p302 zenon_Voia))
% 9.88/10.18  (r1 zenon_Vqd zenon_Vsd)
% 9.88/10.18  (-. (p503 zenon_Vdfa))
% 9.88/10.18  (-. (p205 zenon_Vuz))
% 9.88/10.18  (-. (p101 zenon_Vsla))
% 9.88/10.18  (-. (p305 zenon_Vhz))
% 9.88/10.18  (r1 zenon_Vgca zenon_Vhca)
% 9.88/10.18  (-. (p201 zenon_Vila))
% 9.88/10.18  (-. (p110 zenon_Vae))
% 9.88/10.18  (-. (p609 zenon_Vyf))
% 9.88/10.18  (r1 zenon_Vyb zenon_Vac)
% 9.88/10.18  (-. (p203 zenon_Viga))
% 9.88/10.18  (-. (p110 zenon_Vle))
% 9.88/10.18  (-. (p607 zenon_Vqp))
% 9.88/10.18  (-. (p804 zenon_Vjba))
% 9.88/10.18  (r1 zenon_Via zenon_Vja)
% 9.88/10.18  (r1 zenon_Ven zenon_Vfn)
% 9.88/10.18  (-. (p710 zenon_Vha))
% 9.88/10.18  (r1 zenon_Vaz zenon_Vbz)
% 9.88/10.18  (-. (p1006 zenon_Vmt))
% 9.88/10.18  (-. (p503 zenon_Vcfa))
% 9.88/10.18  (-. (p210 zenon_Vpd))
% 9.88/10.18  (r1 zenon_Voy zenon_Vpy)
% 9.88/10.18  (-. (p403 zenon_Vjfa))
% 9.88/10.18  (p201 Tau_0)
% 9.88/10.18  (-. (p409 zenon_Vzg))
% 9.88/10.18  (-. (p506 zenon_Vku))
% 9.88/10.18  (-. (p809 zenon_Vhf))
% 9.88/10.18  (-. (p601 zenon_Vika))
% 9.88/10.18  (r1 zenon_Vxc zenon_Vzc)
% 9.88/10.18  (-. (p107 zenon_Vzs))
% 9.88/10.18  (-. (p408 zenon_Vul))
% 9.88/10.18  (r1 zenon_Vtja zenon_Vuja)
% 9.88/10.18  (-. (p406 zenon_Vuu))
% 9.88/10.18  (r1 zenon_Vbaa zenon_Vdaa)
% 9.88/10.18  (-. (p501 zenon_Vnka))
% 9.88/10.18  (r1 zenon_Vuv zenon_Vvv)
% 9.88/10.18  (-. (p406 zenon_Vbv))
% 9.88/10.18  (r1 zenon_Vcw zenon_Vdw)
% 9.88/10.18  (-. (p103 zenon_Vcha))
% 9.88/10.18  (-. (p1008 zenon_Vgk))
% 9.88/10.18  (-. (p406 zenon_Vqu))
% 9.88/10.18  (-. (p110 zenon_Vaf))
% 9.88/10.18  (-. (p404 zenon_Vcca))
% 9.88/10.18  (r1 zenon_Vpda zenon_Vqda)
% 9.88/10.18  (r1 zenon_Vsca zenon_Vtca)
% 9.88/10.18  (-. (p502 zenon_Vyha))
% 9.88/10.18  (-. (p510 zenon_Vwa))
% 9.88/10.18  (-. (p908 zenon_Vhk))
% 9.88/10.18  (-. (p310 zenon_Vkc))
% 9.88/10.18  (r1 zenon_Vyy zenon_Vzy)
% 9.88/10.18  (-. (p503 zenon_Vefa))
% 9.88/10.18  (r1 zenon_Vah zenon_Vch)
% 9.88/10.18  (r1 zenon_Vpja zenon_Vqja)
% 9.88/10.18  (r1 zenon_Vnl zenon_Vpl)
% 9.88/10.18  (-. (p806 zenon_Vrt))
% 9.88/10.18  (-. (p504 zenon_Vuba))
% 9.88/10.18  (r1 zenon_Vhx zenon_Vjx)
% 9.88/10.18  (r1 zenon_Vhl zenon_Vil)
% 9.88/10.18  (-. (p302 zenon_Vmia))
% 9.88/10.18  (-. (p407 zenon_Vjq))
% 9.88/10.18  (-. (p507 zenon_Veq))
% 9.88/10.18  (r1 zenon_Vdq zenon_Veq)
% 9.88/10.18  (-. (p305 zenon_Vdz))
% 9.88/10.18  (r1 zenon_Vmda zenon_Voda)
% 9.88/10.18  (r1 zenon_Vtda zenon_Vuda)
% 9.88/10.18  (r1 zenon_Vzfa zenon_Vaga)
% 9.88/10.18  (-. (p402 zenon_Vjia))
% 9.88/10.18  (r1 zenon_Vvw zenon_Vww)
% 9.88/10.18  (-. (p101 zenon_Vxla))
% 9.88/10.18  (-. (p101 zenon_Vpla))
% 9.88/10.18  (r1 zenon_Viea zenon_Vkea)
% 9.88/10.18  (-. (p101 zenon_Vula))
% 9.88/10.18  (-. (p306 zenon_Vhv))
% 9.88/10.18  (-. (p708 zenon_Vpk))
% 9.88/10.18  (r1 zenon_Vbs zenon_Vds)
% 9.88/10.18  (r1 zenon_Vpu zenon_Vqu)
% 9.88/10.18  (-. (p505 zenon_Vfy))
% 9.88/10.18  (r1 zenon_Vnaa zenon_Voaa)
% 9.88/10.18  (-. (p603 zenon_Vzea))
% 9.88/10.18  (p707 zenon_Vip)
% 9.88/10.18  (-. (p308 zenon_Van))
% 9.88/10.18  (r1 zenon_Vjt zenon_Vlt)
% 9.88/10.18  (-. (p102 zenon_Vgja))
% 9.88/10.18  (r1 zenon_Vpn zenon_Vrn)
% 9.88/10.18  (-. (p201 zenon_Vnla))
% 9.88/10.18  (-. (p510 zenon_Vkb))
% 9.88/10.18  (r1 zenon_Vor zenon_Vqr)
% 9.88/10.18  (-. (p410 zenon_Vxb))
% 9.88/10.18  (-. (p106 zenon_Vyw))
% 9.88/10.18  (r1 zenon_Vxga zenon_Vyga)
% 9.88/10.18  (r1 zenon_Vtaa zenon_Vuaa)
% 9.88/10.18  (r1 zenon_Vrw zenon_Vsw)
% 9.88/10.18  (-. (p205 zenon_Vaaa))
% 9.88/10.18  (-. (p405 zenon_Vny))
% 9.88/10.18  (r1 zenon_Vwg zenon_Vxg)
% 9.88/10.18  (r1 zenon_Vpa zenon_Vra)
% 9.88/10.18  (-. (p407 zenon_Vlq))
% 9.88/10.18  (r1 zenon_Vgw zenon_Viw)
% 9.88/10.18  (r1 zenon_Vib zenon_Vkb)
% 9.88/10.18  (-. (p504 zenon_Vxba))
% 9.88/10.18  (r1 zenon_Vts zenon_Vus)
% 9.88/10.18  (-. (p601 zenon_Vhka))
% 9.88/10.18  (-. (p101 zenon_Vwla))
% 9.88/10.18  (r1 zenon_Vlb zenon_Vmb)
% 9.88/10.18  (r1 zenon_Vjaa zenon_Vkaa)
% 9.88/10.18  (r1 zenon_Vnp zenon_Vop)
% 9.88/10.18  (-. (p205 zenon_Vyz))
% 9.88/10.18  (r1 zenon_Vtf zenon_Vuf)
% 9.88/10.18  (-. (p402 zenon_Vhia))
% 9.88/10.18  (-. (p210 zenon_Vbd))
% 9.88/10.18  (r1 zenon_Vmh zenon_Vnh)
% 9.88/10.18  (-. (p303 zenon_Vtfa))
% 9.88/10.18  (-. (p302 zenon_Vnia))
% 9.88/10.18  (-. (p306 zenon_Vdv))
% 9.88/10.18  (-. (p901 zenon_Vxja))
% 9.88/10.18  (r1 zenon_Vpb zenon_Vrb)
% 9.88/10.18  (r1 zenon_Vnz zenon_Voz)
% 9.88/10.18  (-. (p901 zenon_Vwja))
% 9.88/10.18  (r1 zenon_Vje zenon_Vle)
% 9.88/10.18  (-. (p510 zenon_Vbb))
% 9.88/10.18  (-. (p305 zenon_Vjz))
% 9.88/10.18  (-. (p206 zenon_Vxv))
% 9.88/10.18  (-. (p103 zenon_Vsga))
% 9.88/10.18  (-. (p1009 zenon_Vbf))
% 9.88/10.18  (-. (p209 zenon_Vbj))
% 9.88/10.18  (-. (p105 zenon_Viaa))
% 9.88/10.18  (r1 zenon_Vyg zenon_Vzg)
% 9.88/10.18  (r1 zenon_Vuj zenon_Vwj)
% 9.88/10.18  (r1 zenon_Vrg zenon_Vtg)
% 9.88/10.18  (-. (p110 zenon_Vre))
% 9.88/10.18  (-. (p104 zenon_Vyda))
% 9.88/10.18  (r1 zenon_Vjg zenon_Vkg)
% 9.88/10.18  (p707 zenon_Vjp)
% 9.88/10.18  (r1 zenon_Vrr zenon_Vsr)
% 9.88/10.18  (-. (p402 zenon_Veia))
% 9.88/10.18  (-. (p303 zenon_Vqfa))
% 9.88/10.18  (-. (p509 zenon_Vgg))
% 9.88/10.18  (-. (p1003 zenon_Vlea))
% 9.88/10.18  (-. (p103 zenon_Vaha))
% 9.88/10.18  (-. (p802 zenon_Vmha))
% 9.88/10.18  (r1 zenon_Vpz zenon_Vqz)
% 9.88/10.18  (r1 zenon_Vvm zenon_Vxm)
% 9.88/10.18  (-. (p105 zenon_Vmaa))
% 9.88/10.18  *)
% 9.88/10.18  (* NO-PROOF *)
% 9.88/10.18  % SZS status GaveUp
% 9.88/10.18  Number of rewrites on terms: 0
% 9.88/10.18  Number of rewrites on props: 0
% 9.88/10.18  nodes searched: 2163
% 9.88/10.18  max branch formulas: 3053
% 9.88/10.18  proof nodes created: 0
% 9.88/10.18  formulas created: 21549
% 9.88/10.18  
%------------------------------------------------------------------------------