%------------------------------------------------------------------------------ % File : ZenonModulo---0.5.0 % Problem : LCL668+1.020 : TPTP v9.3.1. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : run_zenon_modulo %d %s % Computer : n003.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:22 PM UTC 2026 % Result : Unknown 33.95s 34.28s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : LCL668+1.020 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.02 % Command : run_zenon_modulo %d %s % 0.09/0.34 % Computer : n003.cluster.edu % 0.09/0.34 % Model : x86_64 x86_64 % 0.09/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.34 % Memory : 8046.5625MB % 0.09/0.34 % OS : Linux 6.8.0-71-generic % 0.09/0.34 % CPULimit : 300 % 0.09/0.34 % WCLimit : 300 % 0.09/0.34 % DateTime : Sat Sep 5 15:54:36 UTC 2026 % 0.09/0.34 % CPUTime : % 33.95/34.26 Zenon error: exhausted search space without finding a proof % 33.95/34.26 (* Current branch: % 33.95/34.26 (r1 zenon_Vjb zenon_Vkb) % 33.95/34.26 (-. (p56 zenon_Vfte)) % 33.95/34.26 (zenon_Veef != zenon_Vbcf) % 33.95/34.26 (r1 zenon_Vqta zenon_Vfxa) % 33.95/34.26 (-. (p38 zenon_Vudg)) % 33.95/34.26 (-. (p42 zenon_Vgxf)) % 33.95/34.26 (-. (p54 zenon_Vyze)) % 33.95/34.26 (-. (p101 zenon_Vil)) % 33.95/34.26 (zenon_Vsyb != zenon_Vkvb) % 33.95/34.26 (-. (p54 zenon_Vsxe)) % 33.95/34.26 (r1 zenon_Vhb zenon_Vib) % 33.95/34.26 (r1 zenon_Voa zenon_Vpa) % 33.95/34.26 (r1 zenon_Vzaa zenon_Vtea) % 33.95/34.26 (p43 zenon_Vmvf) % 33.95/34.26 (p58 zenon_Vxqe) % 33.95/34.26 (-. (p84 zenon_Vbsb)) % 33.95/34.26 (r1 zenon_Vljh zenon_Vmjh) % 33.95/34.26 (zenon_Vtje != zenon_Vuje) % 33.95/34.26 (r1 zenon_Vjfg zenon_Vvgg) % 33.95/34.26 (zenon_Vxaa != zenon_Vyaa) % 33.95/34.26 (zenon_Vfmd != zenon_Vkjd) % 33.95/34.26 (-. (p26 zenon_Vosg)) % 33.95/34.26 (zenon_Vtug != zenon_Vuug) % 33.95/34.26 (zenon_Vmia != zenon_Vsea) % 33.95/34.26 (p94 zenon_Vfma) % 33.95/34.26 (zenon_Vet != zenon_Vft) % 33.95/34.26 (r1 zenon_Vfb zenon_Vgb) % 33.95/34.26 (-. (p63 zenon_Vgce)) % 33.95/34.26 (-. (p64 zenon_Vhce)) % 33.95/34.26 (zenon_Vhfg != zenon_Vtdg) % 33.95/34.26 (r1 zenon_Vka zenon_Vla) % 33.95/34.26 (r1 zenon_Vlc zenon_Vmc) % 33.95/34.26 (zenon_Vblg != zenon_Vrjg) % 33.95/34.26 (zenon_Vtdg != zenon_Vudg) % 33.95/34.26 (-. (p62 zenon_Vuee)) % 33.95/34.26 (p55 zenon_Vsxe) % 33.95/34.26 (-. (p61 zenon_Vuje)) % 33.95/34.26 (p1 zenon_Vhh) % 33.95/34.26 (r1 zenon_Vta zenon_Vua) % 33.95/34.26 (zenon_Vxrf != zenon_Vyrf) % 33.95/34.26 (r1 zenon_Vna zenon_Voa) % 33.95/34.26 (-. (p55 zenon_Vmve)) % 33.95/34.26 (p45 zenon_Vxrf) % 33.95/34.26 (r1 zenon_Vip zenon_Vft) % 33.95/34.26 (-. (p100 zenon_Vhp)) % 33.95/34.26 (zenon_Vxrf != zenon_Vbqf) % 33.95/34.26 (p5 zenon_Vfih) % 33.95/34.26 (r1 zenon_Vyjh zenon_Vzjh) % 33.95/34.26 (zenon_Vzbc != zenon_Vacc) % 33.95/34.26 (r1 zenon_Vtoc zenon_Vurc) % 33.95/34.26 (-. (p82 zenon_Vsyb)) % 33.95/34.26 (r1 zenon_Vuxe zenon_Vyze) % 33.95/34.26 (p99 zenon_Vet) % 33.95/34.26 (-. (p66 zenon_Vkud)) % 33.95/34.26 (r1 zenon_Vikh zenon_Vjkh) % 33.95/34.26 (-. (p29 zenon_Vzog)) % 33.95/34.26 (-. (p71 zenon_Vogd)) % 33.95/34.26 (-. (p40 zenon_Vpag)) % 33.95/34.26 (-. (p51 zenon_Veef)) % 33.95/34.26 (-. (p85 zenon_Vrob)) % 33.95/34.26 (-. (p73 zenon_Vtad)) % 33.95/34.26 (-. (p91 zenon_Vota)) % 33.95/34.26 (p15 zenon_Vkdh) % 33.95/34.26 (-. (p60 zenon_Vtje)) % 33.95/34.26 (-. (p50 zenon_Vggf)) % 33.95/34.26 (r1 zenon_Vqsg zenon_Vstg) % 33.95/34.26 (zenon_Vuhb != zenon_Vheb) % 33.95/34.26 (zenon_Vbx != zenon_Vet) % 33.95/34.26 (r1 zenon_Vub zenon_Vvb) % 33.95/34.26 (r1 zenon_Vmb zenon_Vnb) % 33.95/34.26 (-. (p16 zenon_Vzbh)) % 33.95/34.26 (p9 zenon_Vtgh) % 33.95/34.26 (p46 zenon_Vbqf) % 33.95/34.26 (-. (p8 zenon_Vtgh)) % 33.95/34.26 (-. (p32 zenon_Vblg)) % 33.95/34.26 (zenon_Vbqf != zenon_Vcqf) % 33.95/34.26 (-. (p30 zenon_Vsng)) % 33.95/34.26 (r1 zenon_Vijh zenon_Vjjh) % 33.95/34.26 (r1 zenon_Vtjg zenon_Vclg) % 33.95/34.26 (zenon_Vrtg != zenon_Vosg) % 33.95/34.26 (p57 zenon_Vfte) % 33.95/34.26 (zenon_Vheb != zenon_Vieb) % 33.95/34.26 (r1 zenon_Vfkh zenon_Vgkh) % 33.95/34.26 (r1 zenon_Vpc zenon_Vqc) % 33.95/34.26 (zenon_Vhh != zenon_Vumh) % 33.95/34.26 (zenon_Vsrd != zenon_Vzod) % 33.95/34.26 (r1 zenon_Vtlh zenon_Vulh) % 33.95/34.26 (r1 zenon_Vqag zenon_Vfcg) % 33.95/34.26 (r1 zenon_Vbkh zenon_Vckh) % 33.95/34.26 (-. (p38 zenon_Vecg)) % 33.95/34.26 (-. (p68 zenon_Vtrd)) % 33.95/34.26 (-. (p41 zenon_Vyyf)) % 33.95/34.26 (-. (p96 zenon_Vxaa)) % 33.95/34.26 (r1 Tau_0 Tau_2) % 33.95/34.26 (r1 zenon_Vtb zenon_Vub) % 33.95/34.26 (zenon_Vbx != zenon_Vcx) % 33.95/34.26 (-. (p88 zenon_Vvhb)) % 33.95/34.26 (r1 zenon_Vvxg zenon_Vsyg) % 33.95/34.26 (zenon_Vet != zenon_Vgp) % 33.95/34.26 (r1 zenon_Vykh zenon_Vzkh) % 33.95/34.26 (-. (p71 zenon_Vljd)) % 33.95/34.26 (r1 zenon_Vzhh zenon_Vgih) % 33.95/34.26 (zenon_Vkvb != zenon_Vlvb) % 33.95/34.26 (zenon_Vfqg != zenon_Vgqg) % 33.95/34.26 (r1 zenon_Vzze zenon_Vccf) % 33.95/34.26 (p91 zenon_Vexa) % 33.95/34.26 (-. (p60 zenon_Vfme)) % 33.95/34.26 (zenon_Vhhe != zenon_Vuee) % 33.95/34.26 (p19 zenon_Vkah) % 33.95/34.26 (r1 zenon_Vhfc zenon_Vlic) % 33.95/34.26 (-. (p28 zenon_Vfqg)) % 33.95/34.26 (r1 zenon_Vqoe zenon_Vyqe) % 33.95/34.26 (r1 zenon_Vylh zenon_Vzlh) % 33.95/34.26 (r1 zenon_Vnc zenon_Voc) % 33.95/34.26 (-. (p102 zenon_Vih)) % 33.95/34.26 (r1 zenon_Vurd zenon_Vlud) % 33.95/34.26 (-. (p80 zenon_Vffc)) % 33.95/34.26 (r1 zenon_Vdxd zenon_Vszd) % 33.95/34.26 (-. (p50 zenon_Viif)) % 33.95/34.26 (r1 zenon_Vua zenon_Vva) % 33.95/34.26 (-. (p96 zenon_Vtea)) % 33.95/34.26 (p18 zenon_Vfbh) % 33.95/34.26 (zenon_Vbxd != zenon_Vcxd) % 33.95/34.26 (-. (p35 zenon_Vugg)) % 33.95/34.26 (r1 zenon_Vdqf zenon_Vyrf) % 33.95/34.26 (p29 zenon_Vfqg) % 33.95/34.26 (r1 zenon_Vjjh zenon_Vkjh) % 33.95/34.26 (-. (p23 zenon_Vuvg)) % 33.95/34.26 (r1 zenon_Voih zenon_Vtih) % 33.95/34.26 (-. (p33 zenon_Vclg)) % 33.95/34.26 (-. (p46 zenon_Veof)) % 33.95/34.26 (p27 zenon_Vosg) % 33.95/34.26 (r1 zenon_Vutf zenon_Vnvf) % 33.95/34.26 (p86 zenon_Vrob) % 33.95/34.26 (zenon_Vxhh != zenon_Vyhh) % 33.95/34.26 (r1 zenon_Vvb zenon_Vwb) % 33.95/34.26 (r1 zenon_Vejh zenon_Vfjh) % 33.95/34.26 (-. (p85 zenon_Vcsb)) % 33.95/34.26 (-. (p67 zenon_Vsrd)) % 33.95/34.26 (r1 zenon_Vtmh zenon_Vumh) % 33.95/34.26 (-. (p98 zenon_Vcx)) % 33.95/34.26 (r1 zenon_Vwwg zenon_Vuxg) % 33.95/34.26 (r1 zenon_Vcb zenon_Vdb) % 33.95/34.26 (r1 zenon_Vdcf zenon_Vfef) % 33.95/34.26 (zenon_Vsea != zenon_Vxaa) % 33.95/34.26 (-. (p48 zenon_Vhkf)) % 33.95/34.26 (p83 zenon_Vsyb) % 33.95/34.26 (r1 zenon_Vpmh zenon_Vqmh) % 33.95/34.26 (-. (p76 zenon_Vtrc)) % 33.95/34.26 (zenon_Vsch != zenon_Vzbh) % 33.95/34.26 (zenon_Vxhh != zenon_Vohh) % 33.95/34.26 (r1 zenon_Vza zenon_Vab) % 33.95/34.26 (zenon_Vsng != zenon_Vkmg) % 33.95/34.26 (-. (p5 zenon_Vgih)) % 33.95/34.26 (r1 zenon_Vvkh zenon_Vwkh) % 33.95/34.26 (r1 zenon_Vwxc zenon_Vuad) % 33.95/34.26 (zenon_Vgfh != zenon_Vreh) % 33.95/34.26 (zenon_Vfih != zenon_Vxhh) % 33.95/34.26 (r1 zenon_Vwkh zenon_Vxkh) % 33.95/34.26 (p79 zenon_Volc) % 33.95/34.26 (r1 zenon_Vojh zenon_Vpjh) % 33.95/34.26 (zenon_Vxze != zenon_Vsxe) % 33.95/34.26 (p92 zenon_Vota) % 33.95/34.26 (r1 zenon_Veb zenon_Vfb) % 33.95/34.26 (r1 zenon_Vhkh zenon_Vikh) % 33.95/34.26 (zenon_Vxqe != zenon_Vooe) % 33.95/34.26 (-. (p75 zenon_Vvxc)) % 33.95/34.26 (r1 zenon_Vkc zenon_Vlc) % 33.95/34.26 (-. (p24 zenon_Vtug)) % 33.95/34.26 (r1 zenon_Vwgg zenon_Vhig) % 33.95/34.26 (-. (p27 zenon_Vkrg)) % 33.95/34.26 (zenon_Vrzd != zenon_Vszd) % 33.95/34.26 (r1 zenon_Vea zenon_Vfa) % 33.95/34.26 (r1 zenon_Ved zenon_Vfd) % 33.95/34.26 (p82 zenon_Vzbc) % 33.95/34.26 (-. (p16 zenon_Vtch)) % 33.95/34.26 (zenon_Vfxf != zenon_Vgxf) % 33.95/34.26 (r1 zenon_Vvje zenon_Vfme) % 33.95/34.26 (zenon_Vhhe != zenon_Vihe) % 33.95/34.26 (r1 zenon_Vrjh zenon_Vsjh) % 33.95/34.26 (zenon_Vmvf != zenon_Vnvf) % 33.95/34.26 (r1 zenon_Vfd zenon_Vgd) % 33.95/34.26 (r1 zenon_Vslh zenon_Vtlh) % 33.95/34.26 (r1 zenon_Vgc zenon_Vhc) % 33.95/34.26 (-. (p25 zenon_Vrtg)) % 33.95/34.26 (p96 zenon_Vsea) % 33.95/34.26 (p49 zenon_Vhkf) % 33.95/34.26 (p32 zenon_Vkmg) % 33.95/34.26 (-. (p83 zenon_Vkvb)) % 33.95/34.26 (r1 zenon_Vkjh zenon_Vljh) % 33.95/34.26 (r1 zenon_Vulh zenon_Vvlh) % 33.95/34.26 (zenon_Vufh != zenon_Vgfh) % 33.95/34.26 (r1 zenon_Vdjh zenon_Vejh) % 33.95/34.26 (p74 zenon_Vtad) % 33.95/34.26 (r1 zenon_Vokh zenon_Vpkh) % 33.95/34.26 (r1 zenon_Vz zenon_Vaa) % 33.95/34.26 (-. (p77 zenon_Vurc)) % 33.95/34.26 (r1 zenon_Vclh zenon_Vdlh) % 33.95/34.26 (zenon_Vkud != zenon_Vsrd) % 33.95/34.26 (r1 zenon_Vjkf zenon_Vhmf) % 33.95/34.26 (-. (p22 zenon_Vuwg)) % 33.95/34.26 (r1 zenon_Vvjh zenon_Vwjh) % 33.95/34.26 (p7 zenon_Vohh) % 33.95/34.26 (r1 Tau_0 Tau_1) % 33.95/34.26 (zenon_Vozg != zenon_Vpzg) % 33.95/34.26 (zenon_Vrdd != zenon_Vtad) % 33.95/34.26 (r1 zenon_Vsmh zenon_Vtmh) % 33.95/34.26 (r1 zenon_Vfa zenon_Vga) % 33.95/34.26 (r1 zenon_Vpjh zenon_Vqjh) % 33.95/34.26 (r1 zenon_Vpb zenon_Vqb) % 33.95/34.26 (r1 zenon_Vdc zenon_Vec) % 33.95/34.26 (r1 zenon_Vomh zenon_Vpmh) % 33.95/34.26 (p16 zenon_Vsch) % 33.95/34.26 (zenon_Vmve != zenon_Vnve) % 33.95/34.26 (r1 zenon_Vib zenon_Vjb) % 33.95/34.26 (r1 zenon_Vvgh zenon_Vfhh) % 33.95/34.26 (-. (p20 zenon_Vpzg)) % 33.95/34.26 (r1 zenon_Vcc zenon_Vdc) % 33.95/34.26 (r1 zenon_Vzih zenon_Vajh) % 33.95/34.26 (r1 zenon_Vqkh zenon_Vrkh) % 33.95/34.26 (zenon_Vrob != zenon_Vglb) % 33.95/34.26 (-. (p62 zenon_Vihe)) % 33.95/34.26 (r1 zenon_Vqlh zenon_Vrlh) % 33.95/34.26 (r1 zenon_Vnb zenon_Vob) % 33.95/34.26 (zenon_Vsrd != zenon_Vtrd) % 33.95/34.26 (r1 zenon_Vakh zenon_Vbkh) % 33.95/34.26 (p35 zenon_Vgig) % 33.95/34.26 (zenon_Vid != zenon_Vsih) % 33.95/34.26 (r1 zenon_Vwlh zenon_Vxlh) % 33.95/34.26 (-. (p86 zenon_Vsob)) % 33.95/34.26 (p63 zenon_Vuee) % 33.95/34.26 (zenon_Vhl != zenon_Vil) % 33.95/34.26 (r1 zenon_Vxjh zenon_Vyjh) % 33.95/34.26 (r1 zenon_Volh zenon_Vplh) % 33.95/34.26 (r1 zenon_Vad zenon_Vbd) % 33.95/34.26 (r1 zenon_Vigf zenon_Viif) % 33.95/34.26 (-. (p37 zenon_Vifg)) % 33.95/34.26 (-. (p42 zenon_Vmvf)) % 33.95/34.26 (zenon_Vtrc != zenon_Vroc) % 33.95/34.26 (zenon_Vfxf != zenon_Vmvf) % 33.95/34.26 (r1 zenon_Vdeh zenon_Vseh) % 33.95/34.26 (r1 zenon_Vhjh zenon_Vijh) % 33.95/34.26 (-. (p26 zenon_Vstg)) % 33.95/34.26 (-. (p10 zenon_Vigh)) % 33.95/34.26 (r1 zenon_Vmlh zenon_Vnlh) % 33.95/34.26 (r1 zenon_X4 zenon_Vih) % 33.95/34.26 (zenon_Vzog != zenon_Vsng) % 33.95/34.26 (r1 zenon_Vmmg zenon_Vtng) % 33.95/34.26 (zenon_Vbxd != zenon_Vkud) % 33.95/34.26 (r1 zenon_Vung zenon_Vapg) % 33.95/34.26 (zenon_Vfih != zenon_Vgih) % 33.95/34.26 (r1 zenon_Vw zenon_Vx) % 33.95/34.26 (zenon_Vuxc != zenon_Vuuc) % 33.95/34.26 (r1 zenon_Vkmh zenon_Vlmh) % 33.95/34.26 (r1 zenon_Vxc zenon_Vyc) % 33.95/34.26 (-. (p78 zenon_Vsoc)) % 33.95/34.26 (p17 zenon_Vzbh) % 33.95/34.26 (r1 zenon_Velh zenon_Vflh) % 33.95/34.26 (zenon_Vkah != zenon_Vozg) % 33.95/34.26 (-. (p97 zenon_Vbx)) % 33.95/34.26 (r1 zenon_Vgcg zenon_Vudg) % 33.95/34.26 (r1 zenon_Vsb zenon_Vtb) % 33.95/34.26 (zenon_Vzbh != zenon_Vach) % 33.95/34.26 (-. (p14 zenon_Vceh)) % 33.95/34.26 (r1 zenon_Vra zenon_Vsa) % 33.95/34.26 (zenon_Vryg != zenon_Vsyg) % 33.95/34.26 (-. (p81 zenon_Vgfc)) % 33.95/34.26 (-. (p5 zenon_Vxhh)) % 33.95/34.26 (zenon_Vohh != zenon_Vehh) % 33.95/34.26 (zenon_Vkic != zenon_Vffc) % 33.95/34.26 (-. (p34 zenon_Vsjg)) % 33.95/34.26 (r1 zenon_Vtyg zenon_Vpzg) % 33.95/34.26 (-. (p48 zenon_Vhmf)) % 33.95/34.26 (r1 zenon_Vgb zenon_Vhb) % 33.95/34.26 (-. (p101 zenon_Vhh)) % 33.95/34.26 (-. (p83 zenon_Vtyb)) % 33.95/34.26 (-. (p93 zenon_Vypa)) % 33.95/34.26 (zenon_Vfbh != zenon_Vgbh) % 33.95/34.26 (r1 zenon_Vn zenon_Vo) % 33.95/34.26 (r1 zenon_Vxa zenon_Vya) % 33.95/34.26 (r1 zenon_Vlmh zenon_Vmmh) % 33.95/34.26 (r1 zenon_Vwee zenon_Vihe) % 33.95/34.26 (r1 zenon_Vrb zenon_Vsb) % 33.95/34.26 (zenon_Vgig != zenon_Vhig) % 33.95/34.26 (zenon_Vbsb != zenon_Vrob) % 33.95/34.26 (-. (p79 zenon_Vplc)) % 33.95/34.26 (r1 zenon_Vyih zenon_Vzih) % 33.95/34.26 (-. (p63 zenon_Vvee)) % 33.95/34.26 (zenon_Vggf != zenon_Veef) % 33.95/34.26 (zenon_Vbeh != zenon_Vkdh) % 33.95/34.26 (r1 zenon_Vmrg zenon_Vpsg) % 33.95/34.26 (r1 zenon_Vac zenon_Vbc) % 33.95/34.26 (zenon_Vuwg != zenon_Vvwg) % 33.95/34.26 (r1 zenon_Voc zenon_Vpc) % 33.95/34.26 (-. (p24 zenon_Vvvg)) % 33.95/34.26 (zenon_Vtxg != zenon_Vuwg) % 33.95/34.26 (-. (p9 zenon_Vugh)) % 33.95/34.26 (r1 zenon_Vxb zenon_Vyb) % 33.95/34.26 (r1 zenon_Vsc zenon_Vtc) % 33.95/34.26 (zenon_Vuwg != zenon_Vuvg) % 33.95/34.26 (zenon_Vkvb != zenon_Vbsb) % 33.95/34.26 (p37 zenon_Vhfg) % 33.95/34.26 (r1 zenon_Vzb zenon_Vac) % 33.95/34.26 (zenon_Vogd != zenon_Vpgd) % 33.95/34.26 (zenon_Vbeh != zenon_Vceh) % 33.95/34.26 (-. (p2 zenon_Vsih)) % 33.95/34.26 (-. (p89 zenon_Vieb)) % 33.95/34.26 (r1 zenon_Vvlh zenon_Vwlh) % 33.95/34.26 (r1 zenon_Viig zenon_Vsjg) % 33.95/34.26 (zenon_Vzbh != zenon_Vfbh) % 33.95/34.26 (r1 zenon_Vvrc zenon_Vvuc) % 33.95/34.26 (zenon_Vhkf != zenon_Vhif) % 33.95/34.26 (r1 zenon_Vaa zenon_Vba) % 33.95/34.26 (zenon_Vtrc != zenon_Vurc) % 33.95/34.26 (zenon_Vota != zenon_Vxpa) % 33.95/34.26 (r1 zenon_Vdlg zenon_Vlmg) % 33.95/34.26 (-. (p86 zenon_Vglb)) % 33.95/34.26 (-. (p11 zenon_Vvfh)) % 33.95/34.26 (zenon_Vgce != zenon_Vrzd) % 33.95/34.26 (p10 zenon_Vhgh) % 33.95/34.26 (r1 zenon_Vjmh zenon_Vkmh) % 33.95/34.26 (r1 zenon_Vekh zenon_Vfkh) % 33.95/34.26 (-. (p91 zenon_Vfxa)) % 33.95/34.26 (p21 zenon_Vryg) % 33.95/34.26 (zenon_Vmia != zenon_Vnia) % 33.95/34.26 (r1 zenon_Vgjh zenon_Vhjh) % 33.95/34.26 (p68 zenon_Vsrd) % 33.95/34.26 (r1 zenon_Vjh zenon_Vil) % 33.95/34.26 (p71 zenon_Vkjd) % 33.95/34.26 (zenon_Vheb != zenon_Vtab) % 33.95/34.26 (p4 zenon_Vmih) % 33.95/34.26 (r1 zenon_Vmjh zenon_Vnjh) % 33.95/34.26 (zenon_Vtje != zenon_Vhhe) % 33.95/34.26 (-. (p49 zenon_Vikf)) % 33.95/34.26 (r1 zenon_Vjc zenon_Vkc) % 33.95/34.26 (r1 zenon_Vfmh zenon_Vgmh) % 33.95/34.26 (r1 zenon_Vbpg zenon_Vgqg) % 33.95/34.26 (r1 zenon_Vic zenon_Vjc) % 33.95/34.26 (r1 zenon_Vrc zenon_Vsc) % 33.95/34.26 (-. (p97 zenon_Vyaa)) % 33.95/34.26 (-. (p103 Tau_2)) % 33.95/34.26 (-. (p12 zenon_Vhfh)) % 33.95/34.26 (p81 zenon_Vffc) % 33.95/34.26 (p62 zenon_Vhhe) % 33.95/34.26 (r1 zenon_Vrlh zenon_Vslh) % 33.95/34.26 (r1 zenon_Vmmh zenon_Vnmh) % 33.95/34.26 (p50 zenon_Vhif) % 33.95/34.26 (r1 zenon_Vkkh zenon_Vlkh) % 33.95/34.26 (-. (p65 zenon_Vbxd)) % 33.95/34.26 (r1 zenon_Vwb zenon_Vxb) % 33.95/34.26 (-. (p87 zenon_Vuhb)) % 33.95/34.26 (p95 zenon_Vmia) % 33.95/34.26 (p2 zenon_Vxih) % 33.95/34.26 (-. (p59 zenon_Vpoe)) % 33.95/34.26 (-. (p18 zenon_Vkah)) % 33.95/34.26 (zenon_Vzod != zenon_Vapd) % 33.95/34.26 (p90 zenon_Vtab) % 33.95/34.26 (r1 zenon_Vbch zenon_Vtch) % 33.95/34.26 (zenon_Vgce != zenon_Vhce) % 33.95/34.26 (-. (p92 zenon_Vpta)) % 33.95/34.26 (zenon_Vroc != zenon_Vsoc) % 33.95/34.26 (zenon_Vstf != zenon_Vttf) % 33.95/34.26 (-. (p17 zenon_Vach)) % 33.95/34.26 (-. (p56 zenon_Vnve)) % 33.95/34.26 (zenon_Vsih != zenon_Vtih) % 33.95/34.26 (p59 zenon_Vooe) % 33.95/34.26 (-. (p43 zenon_Vnvf)) % 33.95/34.26 (-. (p87 zenon_Vhlb)) % 33.95/34.26 (r1 zenon_Vwuc zenon_Vvxc) % 33.95/34.26 (-. (p46 zenon_Vcqf)) % 33.95/34.26 (r1 zenon_Vv zenon_Vw) % 33.95/34.26 (r1 zenon_Vtc zenon_Vuc) % 33.95/34.26 (zenon_Vtad != zenon_Vuxc) % 33.95/34.26 (p73 zenon_Vrdd) % 33.95/34.26 (-. (p55 zenon_Vtxe)) % 33.95/34.26 (zenon_Vrzd != zenon_Vbxd) % 33.95/34.26 (r1 zenon_Vnkh zenon_Vokh) % 33.95/34.26 (zenon_Vohh != zenon_Vphh) % 33.95/34.26 (-. (p28 zenon_Vlrg)) % 33.95/34.26 (p85 zenon_Vbsb) % 33.95/34.26 (r1 zenon_Vvug zenon_Vvvg) % 33.95/34.26 (r1 zenon_Vamh zenon_Vbmh) % 33.95/34.26 (-. (p84 zenon_Vlvb)) % 33.95/34.26 (r1 zenon_Vxlh zenon_Vylh) % 33.95/34.26 (-. (p39 zenon_Voag)) % 33.95/34.26 (-. (p7 zenon_Vphh)) % 33.95/34.26 (r1 zenon_Vcmh zenon_Vdmh) % 33.95/34.26 (r1 zenon_Vwjh zenon_Vxjh) % 33.95/34.26 (r1 zenon_Vhc zenon_Vic) % 33.95/34.26 (r1 zenon_Vqlc zenon_Vsoc) % 33.95/34.26 (r1 zenon_Vgof zenon_Vcqf) % 33.95/34.26 (r1 zenon_Vma zenon_Vna) % 33.95/34.26 (zenon_Vrdd != zenon_Vsdd) % 33.95/34.26 (-. (p9 zenon_Vhgh)) % 33.95/34.26 (-. (p32 zenon_Vlmg)) % 33.95/34.26 (r1 zenon_Vplh zenon_Vqlh) % 33.95/34.26 (-. (p58 zenon_Vyqe)) % 33.95/34.26 (r1 zenon_Vhbh zenon_Vach) % 33.95/34.26 (-. (p41 zenon_Vfxf)) % 33.95/34.26 (r1 zenon_Vqzg zenon_Vlah) % 33.95/34.26 (zenon_Voag != zenon_Vxyf) % 33.95/34.26 (-. (p19 zenon_Vozg)) % 33.95/34.26 (zenon_Vzog != zenon_Vapg) % 33.95/34.26 (r1 zenon_Vlkh zenon_Vmkh) % 33.95/34.26 (zenon_Vfte != zenon_Vxqe) % 33.95/34.26 (r1 zenon_Vzqe zenon_Vgte) % 33.95/34.26 (zenon_Vfqg != zenon_Vzog) % 33.95/34.26 (zenon_Vkjd != zenon_Vljd) % 33.95/34.26 (zenon_Vecg != zenon_Vfcg) % 33.95/34.26 (r1 zenon_Vbjh zenon_Vcjh) % 33.95/34.26 (zenon_Vgp != zenon_Vhl) % 33.95/34.26 (r1 zenon_Vice zenon_Vvee) % 33.95/34.26 (-. (p25 zenon_Vuug)) % 33.95/34.26 (r1 zenon_Vdd zenon_Ved) % 33.95/34.26 (p28 zenon_Vkrg) % 33.95/34.26 (-. (p45 zenon_Vbqf)) % 33.95/34.26 (p70 zenon_Vfmd) % 33.95/34.26 (r1 zenon_Valh zenon_Vblh) % 33.95/34.26 (zenon_Vtxg != zenon_Vuxg) % 33.95/34.26 (zenon_Veef != zenon_Vfef) % 33.95/34.26 (-. (p13 zenon_Vseh)) % 33.95/34.26 (r1 zenon_Vbc zenon_Vcc) % 33.95/34.26 (-. (p70 zenon_Vkjd)) % 33.95/34.26 (-. (p33 zenon_Vrjg)) % 33.95/34.26 (zenon_Vufh != zenon_Vvfh) % 33.95/34.26 (r1 zenon_Vrkh zenon_Vskh) % 33.95/34.26 (zenon_Vgp != zenon_Vhp) % 33.95/34.26 (p80 zenon_Vkic) % 33.95/34.26 (-. (p100 zenon_Vhl)) % 33.95/34.26 (-. (p31 zenon_Vkmg)) % 33.95/34.26 (p44 zenon_Vstf) % 33.95/34.26 (r1 zenon_Vha zenon_Via) % 33.95/34.26 (r1 zenon_Vq zenon_Vr) % 33.95/34.26 (p25 zenon_Vtug) % 33.95/34.26 (p52 zenon_Veef) % 33.95/34.26 (r1 zenon_Vimh zenon_Vjmh) % 33.95/34.26 (r1 zenon_Vx zenon_Vy) % 33.95/34.26 (r1 zenon_Vhqg zenon_Vlrg) % 33.95/34.26 (zenon_Vxyf != zenon_Vfxf) % 33.95/34.26 (r1 Tau_3 zenon_Vyih) % 33.95/34.26 (zenon_Vuxc != zenon_Vvxc) % 33.95/34.26 (zenon_Vosg != zenon_Vpsg) % 33.95/34.26 (zenon_Vugg != zenon_Vhfg) % 33.95/34.26 (r1 zenon_Vjl zenon_Vhp) % 33.95/34.26 (r1 zenon_Vbb zenon_Vcb) % 33.95/34.26 (-. (p4 zenon_Vfih)) % 33.95/34.26 (r1 zenon_Vdx zenon_Vyaa) % 33.95/34.26 (zenon_Vehh != zenon_Vtgh) % 33.95/34.26 (zenon_Vkdh != zenon_Vsch) % 33.95/34.26 (r1 Tau_0 Tau_3) % 33.95/34.26 (r1 zenon_Vzpa zenon_Vpta) % 33.95/34.26 (-. (p53 zenon_Vxze)) % 33.95/34.26 (r1 zenon_Vec zenon_Vfc) % 33.95/34.26 (-. (p82 zenon_Vacc)) % 33.95/34.26 (zenon_Vuhb != zenon_Vvhb) % 33.95/34.26 (-. (p36 zenon_Vvgg)) % 33.95/34.26 (r1 zenon_Vcd zenon_Vdd) % 33.95/34.26 (-. (p44 zenon_Vxrf)) % 33.95/34.26 (p48 zenon_Vgmf) % 33.95/34.26 (r1 zenon_Vzrf zenon_Vttf) % 33.95/34.26 (-. (p1 zenon_Vxih)) % 33.95/34.26 (r1 Tau_1 zenon_Vm) % 33.95/34.26 (r1 zenon_Vflh zenon_Vglh) % 33.95/34.26 (-. (p52 zenon_Vfef)) % 33.95/34.26 (-. (p57 zenon_Vxqe)) % 33.95/34.26 (zenon_Volc != zenon_Vplc) % 33.95/34.26 (r1 zenon_Vwfh zenon_Vigh) % 33.95/34.26 (zenon_Vooe != zenon_Veme) % 33.95/34.26 (p26 zenon_Vrtg) % 33.95/34.26 (-. (p47 zenon_Vfof)) % 33.95/34.26 (p14 zenon_Vbeh) % 33.95/34.26 (r1 zenon_Vfjh zenon_Vgjh) % 33.95/34.26 (-. (p47 zenon_Vgmf)) % 33.95/34.26 (-. (p74 zenon_Vuad)) % 33.95/34.26 (zenon_Vmih != zenon_Vfih) % 33.95/34.26 (r1 zenon_Vsjh zenon_Vtjh) % 33.95/34.26 (zenon_Vkjd != zenon_Vogd) % 33.95/34.26 (r1 zenon_Vvc zenon_Vwc) % 33.95/34.26 (r1 zenon_Vglh zenon_Vhlh) % 33.95/34.26 (-. (p73 zenon_Vsdd)) % 33.95/34.26 (r1 zenon_Vs zenon_Vt) % 33.95/34.26 (zenon_Vffc != zenon_Vgfc) % 33.95/34.26 (zenon_Vhgh != zenon_Vigh) % 33.95/34.26 (zenon_Vecg != zenon_Voag) % 33.95/34.26 (-. (p81 zenon_Vzbc)) % 33.95/34.26 (p40 zenon_Voag) % 33.95/34.26 (r1 zenon_Vjif zenon_Vikf) % 33.95/34.26 (-. (p44 zenon_Vttf)) % 33.95/34.26 (-. (p12 zenon_Vreh)) % 33.95/34.26 (-. (p18 zenon_Vgbh)) % 33.95/34.26 (zenon_Vtug != zenon_Vrtg) % 33.95/34.26 (r1 zenon_Vm zenon_Vn) % 33.95/34.26 (r1 zenon_Vove zenon_Vtxe) % 33.95/34.26 (r1 zenon_Vzkh zenon_Valh) % 33.95/34.26 (-. (p70 zenon_Vgmd)) % 33.95/34.26 (-. (p17 zenon_Vfbh)) % 33.95/34.26 (-. (p65 zenon_Vszd)) % 33.95/34.26 (zenon_Vxpa != zenon_Vfma) % 33.95/34.26 (p36 zenon_Vugg) % 33.95/34.26 (r1 zenon_Vwhb zenon_Vhlb) % 33.95/34.26 (zenon_Voag != zenon_Vpag) % 33.95/34.26 (r1 zenon_Vbd zenon_Vcd) % 33.95/34.26 (zenon_Vkrg != zenon_Vlrg) % 33.95/34.26 (r1 zenon_Vwc zenon_Vxc) % 33.95/34.26 (zenon_Vkud != zenon_Vlud) % 33.95/34.26 (r1 zenon_Vskh zenon_Vtkh) % 33.95/34.26 (r1 zenon_Vt zenon_Vu) % 33.95/34.26 (p24 zenon_Vuvg) % 33.95/34.26 (-. (p76 zenon_Vvuc)) % 33.95/34.26 (zenon_Vota != zenon_Vpta) % 33.95/34.26 (zenon_Vgig != zenon_Vugg) % 33.95/34.26 (r1 zenon_Vtjh zenon_Vujh) % 33.95/34.26 (zenon_Vuvg != zenon_Vtug) % 33.95/34.26 (-. (p36 zenon_Vhfg)) % 33.95/34.26 (zenon_Vmve != zenon_Vfte) % 33.95/34.26 (-. (p4 zenon_Vnih)) % 33.95/34.26 (-. (p1 zenon_Vumh)) % 33.95/34.26 (r1 zenon_Vovf zenon_Vgxf) % 33.95/34.26 (r1 zenon_Vteh zenon_Vhfh) % 33.95/34.26 (p30 zenon_Vzog) % 33.95/34.26 (r1 zenon_Vpa zenon_Vqa) % 33.95/34.26 (r1 zenon_Vla zenon_Vma) % 33.95/34.26 (zenon_Vhif != zenon_Viif) % 33.95/34.26 (zenon_Vgfh != zenon_Vhfh) % 33.95/34.26 (zenon_Vxaa != zenon_Vbx) % 33.95/34.26 (p13 zenon_Vreh) % 33.95/34.26 (zenon_Vfte != zenon_Vgte) % 33.95/34.26 (r1 zenon_Vqmh zenon_Vrmh) % 33.95/34.26 (r1 zenon_Vab zenon_Vbb) % 33.95/34.26 (r1 zenon_Vimf zenon_Vfof) % 33.95/34.26 (-. (p49 zenon_Vhif)) % 33.95/34.26 (r1 zenon_Vwvg zenon_Vvwg) % 33.95/34.26 (-. (p77 zenon_Vroc)) % 33.95/34.26 (r1 zenon_Vgef zenon_Vhgf) % 33.95/34.26 (p34 zenon_Vrjg) % 33.95/34.26 (-. (p40 zenon_Vxyf)) % 33.95/34.26 (r1 zenon_Vob zenon_Vpb) % 33.95/34.26 (zenon_Vtad != zenon_Vuad) % 33.95/34.26 (-. (p39 zenon_Vfcg)) % 33.95/34.26 (-. (p51 zenon_Vhgf)) % 33.95/34.26 (zenon_Vxih != zenon_Vsih) % 33.95/34.26 (p2 zenon_Vid) % 33.95/34.26 (zenon_Vbcf != zenon_Vxze) % 33.95/34.26 (zenon_Veof != zenon_Vgmf) % 33.95/34.26 (zenon_Vreh != zenon_Vbeh) % 33.95/34.26 (r1 zenon_Vgd zenon_Vhd) % 33.95/34.26 (p93 zenon_Vxpa) % 33.95/34.26 (p97 zenon_Vxaa) % 33.95/34.26 (-. (p98 zenon_Vet)) % 33.95/34.26 (r1 zenon_Vuch zenon_Vldh) % 33.95/34.26 (r1 zenon_Vqhh zenon_Vyhh) % 33.95/34.26 (-. (p72 zenon_Vpgd)) % 33.95/34.26 (p41 zenon_Vxyf) % 33.95/34.26 (r1 zenon_Vjkh zenon_Vkkh) % 33.95/34.26 (-. (p90 zenon_Vexa)) % 33.95/34.26 (zenon_Veme != zenon_Vfme) % 33.95/34.26 (p20 zenon_Vozg) % 33.95/34.26 (zenon_Veme != zenon_Vtje) % 33.95/34.26 (zenon_Vmvf != zenon_Vstf) % 33.95/34.26 (r1 zenon_Vhih zenon_Vnih) % 33.95/34.26 (p75 zenon_Vuxc) % 33.95/34.26 (r1 zenon_Vvad zenon_Vsdd) % 33.95/34.26 (r1 zenon_Vca zenon_Vda) % 33.95/34.26 (-. (p53 zenon_Vccf)) % 33.95/34.26 (r1 zenon_Vgxa zenon_Vuab) % 33.95/34.26 (zenon_Vgmf != zenon_Vhmf) % 33.95/34.26 (r1 zenon_Vghh zenon_Vphh) % 33.95/34.26 (-. (p8 zenon_Vfhh)) % 33.95/34.26 (-. (p29 zenon_Vgqg)) % 33.95/34.26 (-. (p52 zenon_Vbcf)) % 33.95/34.26 (r1 zenon_Voia zenon_Vgma) % 33.95/34.26 (-. (p69 zenon_Vapd)) % 33.95/34.26 (p72 zenon_Vogd) % 33.95/34.26 (r1 zenon_Vhlh zenon_Vilh) % 33.95/34.26 (r1 zenon_Vdsb zenon_Vlvb) % 33.95/34.26 (r1 zenon_Vcjh zenon_Vdjh) % 33.95/34.26 (r1 zenon_Vjhe zenon_Vuje) % 33.95/34.26 (r1 zenon_Vhma zenon_Vypa) % 33.95/34.26 (r1 zenon_Via zenon_Vja) % 33.95/34.26 (r1 zenon_Vmkh zenon_Vnkh) % 33.95/34.26 (r1 zenon_Vvab zenon_Vieb) % 33.95/34.26 (zenon_Vmih != zenon_Vnih) % 33.95/34.26 (zenon_Vffc != zenon_Vzbc) % 33.95/34.26 (r1 zenon_Vgmh zenon_Vhmh) % 33.95/34.26 (p39 zenon_Vecg) % 33.95/34.26 (zenon_Vgmf != zenon_Vhkf) % 33.95/34.26 (-. (p67 zenon_Vlud)) % 33.95/34.26 (r1 zenon_Vukh zenon_Vvkh) % 33.95/34.26 (zenon_Vhl != zenon_Vhh) % 33.95/34.26 (r1 zenon_Vtkh zenon_Vukh) % 33.95/34.26 (r1 zenon_Vxkh zenon_Vykh) % 33.95/34.26 (p77 zenon_Vtrc) % 33.95/34.26 (zenon_Vhgh != zenon_Vufh) % 33.95/34.26 (r1 zenon_Vda zenon_Vea) % 33.95/34.26 (r1 zenon_Vbmh zenon_Vcmh) % 33.95/34.26 (-. (p72 zenon_Vrdd)) % 33.95/34.26 (r1 zenon_Vmdh zenon_Vceh) % 33.95/34.26 (p64 zenon_Vgce) % 33.95/34.26 (r1 zenon_Vya zenon_Vza) % 33.95/34.26 (r1 zenon_Vlb zenon_Vmb) % 33.95/34.26 (r1 zenon_Vga zenon_Vha) % 33.95/34.26 (zenon_Vzbc != zenon_Vsyb) % 33.95/34.26 (r1 zenon_Vifh zenon_Vvfh) % 33.95/34.26 (zenon_Vkrg != zenon_Vfqg) % 33.95/34.26 (zenon_Vkmg != zenon_Vlmg) % 33.95/34.26 (r1 zenon_Vqa zenon_Vra) % 33.95/34.26 (zenon_Vsea != zenon_Vtea) % 33.95/34.26 (zenon_Vroc != zenon_Volc) % 33.95/34.26 (-. (p90 zenon_Vuab)) % 33.95/34.26 (zenon_Vsih != zenon_Vmih) % 33.95/34.26 (zenon_Vhfg != zenon_Vifg) % 33.95/34.26 (r1 zenon_Vtdd zenon_Vpgd) % 33.95/34.26 (-. (p34 zenon_Vgig)) % 33.95/34.26 (-. (p3 zenon_Vtih)) % 33.95/34.26 (r1 zenon_Vpkh zenon_Vqkh) % 33.95/34.26 (r1 zenon_Vgt zenon_Vcx) % 33.95/34.26 (r1 zenon_Vyb zenon_Vzb) % 33.95/34.26 (r1 zenon_Vhte zenon_Vnve) % 33.95/34.26 (zenon_Vsxe != zenon_Vmve) % 33.95/34.26 (r1 zenon_Vhmh zenon_Vimh) % 33.95/34.26 (r1 zenon_Vqgd zenon_Vljd) % 33.95/34.26 (zenon_Vglb != zenon_Vuhb) % 33.95/34.26 (p89 zenon_Vheb) % 33.95/34.26 (p98 zenon_Vbx) % 33.95/34.26 (r1 zenon_Vblh zenon_Vclh) % 33.95/34.26 (r1 zenon_Vajh zenon_Vbjh) % 33.95/34.26 (r1 zenon_Vjlh zenon_Vklh) % 33.95/34.26 (r1 zenon_Vzyf zenon_Vpag) % 33.95/34.26 (-. (p31 zenon_Vtng)) % 33.95/34.26 (zenon_Vogd != zenon_Vrdd) % 33.95/34.26 (r1 zenon_Vilb zenon_Vsob) % 33.95/34.26 (-. (p89 zenon_Vtab)) % 33.95/34.26 (zenon_Vozg != zenon_Vryg) % 33.95/34.26 (zenon_Vbsb != zenon_Vcsb) % 33.95/34.26 (-. (p92 zenon_Vxpa)) % 33.95/34.26 (zenon_Vuuc != zenon_Vtrc) % 33.95/34.26 (zenon_Vggf != zenon_Vhgf) % 33.95/34.26 (r1 zenon_Vhd zenon_Vid) % 33.95/34.26 (zenon_Vtgh != zenon_Vugh) % 33.95/34.26 (p53 zenon_Vbcf) % 33.95/34.26 (p8 zenon_Vehh) % 33.95/34.26 (zenon_Vuuc != zenon_Vvuc) % 33.95/34.26 (zenon_Vfma != zenon_Vgma) % 33.95/34.26 (r1 zenon_Vnlh zenon_Volh) % 33.95/34.26 (-. (p45 zenon_Vyrf)) % 33.95/34.26 (r1 zenon_Vbpd zenon_Vtrd) % 33.95/34.26 (zenon_Vreh != zenon_Vseh) % 33.95/34.26 (-. (p94 zenon_Vmia)) % 33.95/34.26 (zenon_Vxpa != zenon_Vypa) % 33.95/34.26 (r1 zenon_Vyc zenon_Vzc) % 33.95/34.26 (r1 zenon_Vkb zenon_Vlb) % 33.95/34.26 (-. (p75 zenon_Vuuc)) % 33.95/34.26 (zenon_Vkic != zenon_Vlic) % 33.95/34.26 (r1 zenon_Vnjh zenon_Vojh) % 33.95/34.26 (zenon_Volc != zenon_Vkic) % 33.95/34.26 (-. (p13 zenon_Vbeh)) % 33.95/34.26 (r1 zenon_Vilh zenon_Vjlh) % 33.95/34.26 (r1 zenon_Vjgh zenon_Vugh) % 33.95/34.26 (r1 zenon_Vwa zenon_Vxa) % 33.95/34.26 (p22 zenon_Vtxg) % 33.95/34.26 (-. (p20 zenon_Vryg)) % 33.95/34.26 (p67 zenon_Vkud) % 33.95/34.26 (zenon_Vblg != zenon_Vclg) % 33.95/34.26 (-. (p30 zenon_Vapg)) % 33.95/34.26 (p60 zenon_Veme) % 33.95/34.26 (-. (p21 zenon_Vtxg)) % 33.95/34.26 (-. (p99 zenon_Vgp)) % 33.95/34.26 (zenon_Vtab != zenon_Vexa) % 33.95/34.26 (-. (p57 zenon_Vgte)) % 33.95/34.26 (zenon_Vhkf != zenon_Vikf) % 33.95/34.26 (zenon_Vfmd != zenon_Vgmd) % 33.95/34.26 (-. (p7 zenon_Vehh)) % 33.95/34.26 (zenon_Vglb != zenon_Vhlb) % 33.95/34.26 (zenon_Vehh != zenon_Vfhh) % 33.95/34.26 (r1 zenon_Vsa zenon_Vta) % 33.95/34.26 (r1 zenon_Vhmd zenon_Vapd) % 33.95/34.28 (r1 zenon_Vr zenon_Vs) % 33.95/34.28 (-. (p19 zenon_Vlah)) % 33.95/34.28 (zenon_Vuee != zenon_Vgce) % 33.95/34.28 (r1 zenon_Vbcc zenon_Vgfc) % 33.95/34.28 (zenon_Vryg != zenon_Vtxg) % 33.95/34.28 (p11 zenon_Vufh) % 33.95/34.28 (p12 zenon_Vgfh) % 33.95/34.28 (p66 zenon_Vbxd) % 33.95/34.28 (zenon_Vfma != zenon_Vmia) % 33.95/34.28 (p31 zenon_Vsng) % 33.95/34.28 (zenon_Vexa != zenon_Vota) % 33.95/34.28 (r1 zenon_Vnmh zenon_Vomh) % 33.95/34.28 (p65 zenon_Vrzd) % 33.95/34.28 (-. (p64 zenon_Vrzd)) % 33.95/34.28 (-. (p15 zenon_Vldh)) % 33.95/34.28 (p84 zenon_Vkvb) % 33.95/34.28 (zenon_Vxze != zenon_Vyze) % 33.95/34.28 (zenon_Vxyf != zenon_Vyyf) % 33.95/34.28 (p88 zenon_Vuhb) % 33.95/34.28 (r1 zenon_Vemh zenon_Vfmh) % 33.95/34.28 (r1 zenon_Vvdg zenon_Vifg) % 33.95/34.28 (-. (p61 zenon_Vhhe)) % 33.95/34.28 (zenon_Vtdg != zenon_Vecg) % 33.95/34.28 (r1 zenon_Vuc zenon_Vvc) % 33.95/34.28 (zenon_Vuee != zenon_Vvee) % 33.95/34.28 (zenon_Vsyb != zenon_Vtyb) % 33.95/34.28 (-. (p11 zenon_Vgfh)) % 33.95/34.28 (-. (p74 zenon_Vuxc)) % 33.95/34.28 (-. (p93 zenon_Vfma)) % 33.95/34.28 (r1 zenon_Vzlh zenon_Vamh) % 33.95/34.28 (zenon_Vrob != zenon_Vsob) % 33.95/34.28 (r1 zenon_Vgme zenon_Vpoe) % 33.95/34.28 (-. (p23 zenon_Vvwg)) % 33.95/34.28 (r1 zenon_Vja zenon_Vka) % 33.95/34.28 (zenon_Vsxe != zenon_Vtxe) % 33.95/34.28 (-. (p59 zenon_Veme)) % 33.95/34.28 (r1 zenon_Vhxf zenon_Vyyf) % 33.95/34.28 (-. (p79 zenon_Vkic)) % 33.95/34.28 (-. (p3 zenon_Vmih)) % 33.95/34.28 (r1 zenon_Vrmh zenon_Vsmh) % 33.95/34.28 (-. (p14 zenon_Vkdh)) % 33.95/34.28 (p47 zenon_Veof) % 33.95/34.28 (r1 zenon_Vmvb zenon_Vtyb) % 33.95/34.28 (-. (p15 zenon_Vsch)) % 33.95/34.28 (zenon_Vhif != zenon_Vggf) % 33.95/34.28 (r1 zenon_Vckh zenon_Vdkh) % 33.95/34.28 (-. (p58 zenon_Vooe)) % 33.95/34.28 (-. (p22 zenon_Vuxg)) % 33.95/34.28 (r1 zenon_Vu zenon_Vv) % 33.95/34.28 (zenon_Vrjg != zenon_Vgig) % 33.95/34.28 (r1 zenon_Vjeb zenon_Vvhb) % 33.95/34.28 (-. (p27 zenon_Vpsg)) % 33.95/34.28 (zenon_Vtgh != zenon_Vhgh) % 33.95/34.28 (r1 zenon_Vklh zenon_Vllh) % 33.95/34.28 (zenon_Vkah != zenon_Vlah) % 33.95/34.28 (-. (p78 zenon_Volc)) % 33.95/34.28 (r1 zenon_Vqb zenon_Vrb) % 33.95/34.28 (-. (p6 zenon_Vohh)) % 33.95/34.28 (zenon_Vkdh != zenon_Vldh) % 33.95/34.28 (r1 zenon_Vmic zenon_Vplc) % 33.95/34.28 (zenon_Vexa != zenon_Vfxa) % 33.95/34.28 (zenon_Vhh != zenon_Vxih) % 33.95/34.28 (r1 zenon_Vujh zenon_Vvjh) % 33.95/34.28 (r1 zenon_Vo zenon_Vp) % 33.95/34.28 (zenon_Vooe != zenon_Vpoe) % 33.95/34.28 (p38 zenon_Vtdg) % 33.95/34.28 (-. (p66 zenon_Vcxd)) % 33.95/34.28 (r1 zenon_Vqc zenon_Vrc) % 33.95/34.28 (p56 zenon_Vmve) % 33.95/34.28 (p51 zenon_Vggf) % 33.95/34.28 (zenon_Vxqe != zenon_Vyqe) % 33.95/34.28 (p61 zenon_Vtje) % 33.95/34.28 (r1 zenon_Vzc zenon_Vad) % 33.95/34.28 (p3 zenon_Vsih) % 33.95/34.28 (-. (p10 zenon_Vufh)) % 33.95/34.28 (zenon_Vugg != zenon_Vvgg) % 33.95/34.28 (zenon_Vbcf != zenon_Vccf) % 33.95/34.28 (r1 zenon_Vp zenon_Vq) % 33.95/34.28 (zenon_Vfbh != zenon_Vkah) % 33.95/34.28 (r1 zenon_Vuyb zenon_Vacc) % 33.95/34.28 (p6 zenon_Vxhh) % 33.95/34.28 (zenon_Vsng != zenon_Vtng) % 33.95/34.28 (zenon_Vrtg != zenon_Vstg) % 33.95/34.28 (-. (p68 zenon_Vzod)) % 33.95/34.28 (r1 zenon_Vva zenon_Vwa) % 33.95/34.28 (-. (p6 zenon_Vyhh)) % 33.95/34.28 (r1 zenon_Vqjh zenon_Vrjh) % 33.95/34.28 (zenon_Vkmg != zenon_Vblg) % 33.95/34.28 (-. (p69 zenon_Vfmd)) % 33.95/34.28 (r1 zenon_Vdb zenon_Veb) % 33.95/34.28 (p76 zenon_Vuuc) % 33.95/34.28 (zenon_Vrjg != zenon_Vsjg) % 33.95/34.28 (zenon_Vsch != zenon_Vtch) % 33.95/34.28 (r1 zenon_Vmc zenon_Vnc) % 33.95/34.28 (p78 zenon_Vroc) % 33.95/34.28 (r1 zenon_Vgkh zenon_Vhkh) % 33.95/34.28 (-. (p80 zenon_Vlic)) % 33.95/34.28 (p42 zenon_Vfxf) % 33.95/34.28 (zenon_Vtab != zenon_Vuab) % 33.95/34.28 (r1 zenon_Vy zenon_Vz) % 33.95/34.28 (-. (p95 zenon_Vnia)) % 33.95/34.28 (zenon_Vzod != zenon_Vfmd) % 33.95/34.28 (r1 zenon_Vmjd zenon_Vgmd) % 33.95/34.28 (-. (p21 zenon_Vsyg)) % 33.95/34.28 (r1 zenon_Vdmh zenon_Vemh) % 33.95/34.28 (r1 zenon_Vba zenon_Vca) % 33.95/34.28 (r1 zenon_Vdkh zenon_Vekh) % 33.95/34.28 (-. (p99 zenon_Vft)) % 33.95/34.28 (p100 zenon_Vgp) % 33.95/34.28 (zenon_Vosg != zenon_Vkrg) % 33.95/34.28 (p23 zenon_Vuwg) % 33.95/34.28 (r1 zenon_Vmah zenon_Vgbh) % 33.95/34.28 (-. (p35 zenon_Vhig)) % 33.95/34.28 (zenon_Veof != zenon_Vfof) % 33.95/34.28 (zenon_Vbqf != zenon_Veof) % 33.95/34.28 (p101 zenon_Vhl) % 33.95/34.28 (-. (p43 zenon_Vstf)) % 33.95/34.28 (r1 zenon_Vdlh zenon_Velh) % 33.95/34.28 (r1 zenon_Vttg zenon_Vuug) % 33.95/34.28 (zenon_Vuvg != zenon_Vvvg) % 33.95/34.28 (r1 zenon_Vfc zenon_Vgc) % 33.95/34.28 (p69 zenon_Vzod) % 33.95/34.28 (p54 zenon_Vxze) % 33.95/34.28 (-. (p88 zenon_Vheb)) % 33.95/34.28 (p87 zenon_Vglb) % 33.95/34.28 (-. (p37 zenon_Vtdg)) % 33.95/34.28 (-. (p94 zenon_Vgma)) % 33.95/34.28 (r1 zenon_Vzjh zenon_Vakh) % 33.95/34.28 (p33 zenon_Vblg) % 33.95/34.28 (r1 zenon_Vllh zenon_Vmlh) % 33.95/34.28 (r1 zenon_Vtob zenon_Vcsb) % 33.95/34.28 (r1 zenon_Vtzd zenon_Vhce) % 33.95/34.28 (r1 zenon_Vuea zenon_Vnia) % 33.95/34.28 (r1 zenon_Vmud zenon_Vcxd) % 33.95/34.28 (zenon_Vstf != zenon_Vxrf) % 33.95/34.28 (-. (p95 zenon_Vsea)) % 33.95/34.28 *) % 33.95/34.28 (* NO-PROOF *) % 33.95/34.28 % SZS status GaveUp % 33.95/34.28 Number of rewrites on terms: 0 % 33.95/34.28 Number of rewrites on props: 0 % 33.95/34.28 nodes searched: 12536 % 33.95/34.28 max branch formulas: 13145 % 33.95/34.28 proof nodes created: 0 % 33.95/34.28 formulas created: 64736 % 33.95/34.28 %------------------------------------------------------------------------------