↑ Up

ZenonModulo---0.5.0.UNK-Non.f

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

% Computer : n009.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:16 PM UTC 2026

% Result   : Unknown 0.43s 0.77s
% Output   : None 
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : LCL652+1.015 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03  % Command  : run_zenon_modulo %d %s
% 0.10/0.36  % Computer : n009.cluster.edu
% 0.10/0.36  % Model    : x86_64 x86_64
% 0.10/0.36  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36  % Memory   : 8046.5625MB
% 0.10/0.36  % OS       : Linux 6.8.0-71-generic
% 0.10/0.36  % CPULimit : 300
% 0.10/0.36  % WCLimit  : 300
% 0.10/0.36  % DateTime : Sat Sep  5 00:03:06 UTC 2026
% 0.10/0.36  % CPUTime  : 
% 0.43/0.76  Zenon error: exhausted search space without finding a proof
% 0.43/0.76  (* Current branch:
% 0.43/0.76  (zenon_Vxg != zenon_Vgj)
% 0.43/0.76  (zenon_Vsl != zenon_Vfb)
% 0.43/0.76  (zenon_Vuk != zenon_Voe)
% 0.43/0.76  (zenon_Vol != zenon_Vra)
% 0.43/0.76  (zenon_Vyk != zenon_Vwe)
% 0.43/0.76  (zenon_Vaj != zenon_Vcd)
% 0.43/0.76  (zenon_Vtg != zenon_Vcg)
% 0.43/0.76  (zenon_Vek != zenon_Voc)
% 0.43/0.76  (zenon_Vch != zenon_Vjd)
% 0.43/0.76  (zenon_Vwj != zenon_Vcd)
% 0.43/0.76  (zenon_Vsj != zenon_Vw)
% 0.43/0.76  (zenon_Vcl != zenon_Vgg)
% 0.43/0.76  (zenon_Vkj != zenon_Vrg)
% 0.43/0.76  (zenon_Vvl != zenon_Voc)
% 0.43/0.76  (zenon_Vgl != zenon_Vjd)
% 0.43/0.76  (zenon_Vbi != zenon_Vac)
% 0.43/0.76  (zenon_Vsj != zenon_Vhi)
% 0.43/0.76  (zenon_Vgl != zenon_Vqf)
% 0.43/0.76  (zenon_Vcl != zenon_Vdh)
% 0.43/0.76  (-. (p1 zenon_Vug))
% 0.43/0.76  (zenon_Vbi != zenon_Voe)
% 0.43/0.76  (zenon_Vqi != zenon_Vwe)
% 0.43/0.76  (zenon_Vak != zenon_Vkg)
% 0.43/0.76  (zenon_Vik != zenon_Vgj)
% 0.43/0.76  (zenon_Vli != zenon_Vbj)
% 0.43/0.76  (zenon_Vgi != zenon_Vra)
% 0.43/0.76  (r1 zenon_Vzf zenon_Vcg)
% 0.43/0.76  (zenon_Vvi != zenon_Vsh)
% 0.43/0.76  (zenon_Vcl != zenon_Vci)
% 0.43/0.76  (zenon_Vuk != zenon_Vih)
% 0.43/0.76  (zenon_Vmh != zenon_Vci)
% 0.43/0.76  (zenon_Vuk != zenon_Vqf)
% 0.43/0.76  (zenon_Vyk != zenon_Vnh)
% 0.43/0.76  (zenon_Vmh != zenon_Vbj)
% 0.43/0.76  (zenon_Vqk != zenon_Vfb)
% 0.43/0.76  (zenon_Vrh != zenon_Vyf)
% 0.43/0.76  (zenon_Vkj != zenon_Vwe)
% 0.43/0.76  (zenon_Vvl != zenon_Vcg)
% 0.43/0.76  (zenon_Vcl != zenon_Vka)
% 0.43/0.76  (zenon_Vik != zenon_Vrg)
% 0.43/0.76  (zenon_Vfj != zenon_Vxh)
% 0.43/0.76  (zenon_Vcl != zenon_Vog)
% 0.43/0.76  (zenon_Vmk != zenon_Vac)
% 0.43/0.76  (zenon_Vmk != zenon_Vri)
% 0.43/0.76  (-. (p1 zenon_Vka))
% 0.43/0.76  (zenon_Vik != zenon_Vcd)
% 0.43/0.76  (zenon_Vuk != zenon_Vac)
% 0.43/0.76  (zenon_Vmh != zenon_Vmi)
% 0.43/0.76  (zenon_Vwj != zenon_Vda)
% 0.43/0.76  (zenon_Vek != zenon_Vq)
% 0.43/0.76  (zenon_Vgl != zenon_Vdh)
% 0.43/0.76  (zenon_Vxg != zenon_Voe)
% 0.43/0.76  (zenon_Vgi != zenon_Vih)
% 0.43/0.76  (zenon_Vhh != zenon_Vra)
% 0.43/0.76  (zenon_Vli != zenon_Vyf)
% 0.43/0.76  (zenon_Vhh != zenon_Vcd)
% 0.43/0.76  (zenon_Vek != zenon_Vmi)
% 0.43/0.76  (zenon_Vkl != zenon_Vci)
% 0.43/0.76  (zenon_Vli != zenon_Vhc)
% 0.43/0.76  (zenon_Vhh != zenon_Vkg)
% 0.43/0.76  (zenon_Vsj != zenon_Vmf)
% 0.43/0.76  (zenon_Vmk != zenon_Vdh)
% 0.43/0.76  (zenon_Vmh != zenon_Vq)
% 0.43/0.76  (zenon_Vsj != zenon_Vdh)
% 0.43/0.76  (zenon_Vtg != zenon_Vse)
% 0.43/0.76  (zenon_Vgl != zenon_Vif)
% 0.43/0.76  (zenon_Vmk != zenon_Vug)
% 0.43/0.76  (zenon_Vol != zenon_Vwi)
% 0.43/0.76  (zenon_Vrh != zenon_Vse)
% 0.43/0.76  (zenon_Vol != zenon_Vsh)
% 0.43/0.76  (zenon_Vtg != zenon_Vw)
% 0.43/0.76  (zenon_Vfj != zenon_Vw)
% 0.43/0.76  (zenon_Vmk != zenon_Vvc)
% 0.43/0.76  (zenon_Vaj != zenon_Vq)
% 0.43/0.76  (zenon_Vwh != zenon_Vaf)
% 0.43/0.76  (zenon_Vmk != zenon_Vyg)
% 0.43/0.76  (zenon_Vwh != zenon_Vhi)
% 0.43/0.76  (zenon_Vqk != zenon_Vyf)
% 0.43/0.76  (zenon_Vqk != zenon_Vda)
% 0.43/0.76  (zenon_Vsj != zenon_Vse)
% 0.43/0.76  (zenon_Vcl != zenon_Vyg)
% 0.43/0.76  (zenon_Vfj != zenon_Vda)
% 0.43/0.76  (zenon_Vch != zenon_Vif)
% 0.43/0.76  (zenon_Vaj != zenon_Vif)
% 0.43/0.76  (zenon_Vvl != zenon_Vyg)
% 0.43/0.76  (zenon_Vhh != zenon_Vq)
% 0.43/0.76  (zenon_Vli != zenon_Vq)
% 0.43/0.76  (zenon_Vmh != zenon_Vhc)
% 0.43/0.76  (zenon_Vli != zenon_Voe)
% 0.43/0.76  (r1 zenon_Vxe zenon_Vaf)
% 0.43/0.76  (zenon_Vol != zenon_Vvc)
% 0.43/0.76  (zenon_Vol != zenon_Vyg)
% 0.43/0.76  (p1 zenon_Vxg)
% 0.43/0.76  (zenon_Vsl != zenon_Vw)
% 0.43/0.76  (-. (p1 zenon_Vtb))
% 0.43/0.76  (zenon_Vqi != zenon_Vgj)
% 0.43/0.76  (zenon_Vcl != zenon_Vtb)
% 0.43/0.76  (zenon_Vqi != zenon_Vfb)
% 0.43/0.76  (zenon_Vkl != zenon_Vmb)
% 0.43/0.76  (zenon_Vqi != zenon_Vci)
% 0.43/0.76  (p1 zenon_Vfj)
% 0.43/0.76  (zenon_Vgl != zenon_Vcd)
% 0.43/0.76  (zenon_Vgi != zenon_Vrg)
% 0.43/0.76  (zenon_Vbi != zenon_Vri)
% 0.43/0.76  (r1 zenon_Voi zenon_Vri)
% 0.43/0.76  (zenon_Vch != zenon_Vgg)
% 0.43/0.76  (zenon_Vkl != zenon_Vqf)
% 0.43/0.76  (zenon_Vek != zenon_Vkg)
% 0.43/0.76  (zenon_Vaj != zenon_Vda)
% 0.43/0.76  (zenon_Vli != zenon_Vka)
% 0.43/0.76  (zenon_Vvi != zenon_Vhc)
% 0.43/0.76  (zenon_Vqi != zenon_Vvc)
% 0.43/0.76  (zenon_Vvi != zenon_Vxh)
% 0.43/0.76  (zenon_Vbi != zenon_Vhi)
% 0.43/0.76  (zenon_Vch != zenon_Vxh)
% 0.43/0.76  (zenon_Vol != zenon_Vya)
% 0.43/0.76  (zenon_Vqk != zenon_Vjd)
% 0.43/0.76  (zenon_Vvi != zenon_Vmi)
% 0.43/0.76  (p1 zenon_Vch)
% 0.43/0.76  (zenon_Vgi != zenon_Vmi)
% 0.43/0.76  (r1 zenon_Vab zenon_Veb)
% 0.43/0.76  (-. (p1 zenon_Vdh))
% 0.43/0.76  (zenon_Vch != zenon_Vfb)
% 0.43/0.76  (zenon_Vbi != zenon_Vuf)
% 0.43/0.76  (zenon_Vli != zenon_Vri)
% 0.43/0.76  (zenon_Vqk != zenon_Vka)
% 0.43/0.76  (zenon_Vyk != zenon_Vrg)
% 0.43/0.76  (zenon_Vtg != zenon_Vmf)
% 0.43/0.76  (zenon_Vqi != zenon_Vyf)
% 0.43/0.76  (zenon_Vli != zenon_Vgg)
% 0.43/0.76  (zenon_Vtg != zenon_Vhi)
% 0.43/0.76  (zenon_Vgi != zenon_Vse)
% 0.43/0.76  (-. (p1 zenon_Vaf))
% 0.43/0.76  (zenon_Vik != zenon_Vsh)
% 0.43/0.76  (zenon_Vli != zenon_Vmi)
% 0.43/0.76  (zenon_Vwj != zenon_Vih)
% 0.43/0.76  (zenon_Vkl != zenon_Vnh)
% 0.43/0.76  (-. (p1 zenon_Vsh))
% 0.43/0.76  (zenon_Vgi != zenon_Vhi)
% 0.43/0.76  (zenon_Vcl != zenon_Vug)
% 0.43/0.76  (zenon_Vqk != zenon_Vmb)
% 0.43/0.76  (r1 zenon_Vxi zenon_Vcj)
% 0.43/0.76  (zenon_Vgl != zenon_Vvc)
% 0.43/0.76  (r1 zenon_Voi zenon_Vpi)
% 0.43/0.76  (zenon_Vxg != zenon_Vlj)
% 0.43/0.76  (zenon_Vik != zenon_Vcg)
% 0.43/0.76  (zenon_Vek != zenon_Vac)
% 0.43/0.76  (zenon_Vrh != zenon_Voe)
% 0.43/0.76  (zenon_Vvl != zenon_Vbj)
% 0.43/0.76  (r1 zenon_Vtj zenon_Vwj)
% 0.43/0.76  (zenon_Vxg != zenon_Vhi)
% 0.43/0.76  (zenon_Vxg != zenon_Vwi)
% 0.43/0.76  (zenon_Vxg != zenon_Vgg)
% 0.43/0.76  (r1 zenon_Vll zenon_Vol)
% 0.43/0.76  (r1 zenon_Vji zenon_Vki)
% 0.43/0.76  (zenon_Vmk != zenon_Vsh)
% 0.43/0.76  (zenon_Vgi != zenon_Vda)
% 0.43/0.76  (p1 zenon_Vmh)
% 0.43/0.76  (zenon_Vaj != zenon_Vgj)
% 0.43/0.76  (zenon_Vtg != zenon_Vdh)
% 0.43/0.76  (zenon_Vsj != zenon_Vih)
% 0.43/0.76  (zenon_Vfe != zenon_Vtd)
% 0.43/0.76  (zenon_Vuk != zenon_Vaf)
% 0.43/0.76  (zenon_Vvi != zenon_Voe)
% 0.43/0.76  (zenon_Vhh != zenon_Vhc)
% 0.43/0.76  (zenon_Vwh != zenon_Vog)
% 0.43/0.76  (zenon_Vli != zenon_Vcd)
% 0.43/0.76  (zenon_Vsj != zenon_Vog)
% 0.43/0.76  (p1 zenon_Vaj)
% 0.43/0.76  (r1 zenon_Vxj zenon_Vak)
% 0.43/0.76  (zenon_Vqk != zenon_Vrg)
% 0.43/0.76  (zenon_Vqk != zenon_Vkg)
% 0.43/0.76  (zenon_Vcl != zenon_Vih)
% 0.43/0.76  (zenon_Vqi != zenon_Vcd)
% 0.43/0.76  (zenon_Vli != zenon_Vug)
% 0.43/0.76  (zenon_Vwj != zenon_Vlj)
% 0.43/0.76  (-. (p1 zenon_Vya))
% 0.43/0.76  (zenon_Vyk != zenon_Vgj)
% 0.43/0.76  (zenon_Vch != zenon_Vbj)
% 0.43/0.76  (zenon_Vak != zenon_Vih)
% 0.43/0.76  (zenon_Vvi != zenon_Vnh)
% 0.43/0.76  (zenon_Vcl != zenon_Vwi)
% 0.43/0.76  (zenon_Vkj != zenon_Vya)
% 0.43/0.76  (r1 zenon_Ved zenon_Vid)
% 0.43/0.76  (zenon_Vch != zenon_Vwi)
% 0.43/0.76  (zenon_Vwh != zenon_Vug)
% 0.43/0.76  (zenon_Vtg != zenon_Vif)
% 0.43/0.76  (zenon_Vrh != zenon_Vih)
% 0.43/0.76  (zenon_Vqi != zenon_Vlj)
% 0.43/0.76  (zenon_Vxg != zenon_Vqf)
% 0.43/0.76  (zenon_Vxg != zenon_Vtb)
% 0.43/0.76  (zenon_Vmk != zenon_Vnh)
% 0.43/0.76  (zenon_Vkl != zenon_Vyf)
% 0.43/0.76  (zenon_Vmk != zenon_Vgg)
% 0.43/0.76  (r1 zenon_Vyh zenon_Vzh)
% 0.43/0.76  (zenon_Vsl != zenon_Vya)
% 0.43/0.76  (r1 zenon_Vni zenon_Voi)
% 0.43/0.76  (-. (p1 zenon_Vbj))
% 0.43/0.76  (zenon_Vxg != zenon_Vhc)
% 0.43/0.76  (zenon_Vgl != zenon_Vtb)
% 0.43/0.76  (zenon_Vuk != zenon_Vgj)
% 0.43/0.76  (zenon_Vcl != zenon_Vda)
% 0.43/0.76  (zenon_Vwj != zenon_Vif)
% 0.43/0.76  (zenon_Vak != zenon_Vcd)
% 0.43/0.76  (zenon_Vfj != zenon_Vug)
% 0.43/0.76  (zenon_Vkl != zenon_Vcg)
% 0.43/0.76  (zenon_Vsl != zenon_Vhc)
% 0.43/0.76  (zenon_Vaj != zenon_Vih)
% 0.43/0.76  (zenon_Vqk != zenon_Vhi)
% 0.43/0.76  (p1 zenon_Vvl)
% 0.43/0.76  (zenon_Vrh != zenon_Vq)
% 0.43/0.76  (r1 zenon_Vte zenon_Vwe)
% 0.43/0.76  (zenon_Vol != zenon_Vka)
% 0.43/0.76  (zenon_Vkl != zenon_Vxh)
% 0.43/0.76  (zenon_Vli != zenon_Vkg)
% 0.43/0.76  (zenon_Vvi != zenon_Vgj)
% 0.43/0.76  (zenon_Vkl != zenon_Vcd)
% 0.43/0.76  (zenon_Vwh != zenon_Vqf)
% 0.43/0.76  (zenon_Vqi != zenon_Vbj)
% 0.43/0.76  (zenon_Vyk != zenon_Vhi)
% 0.43/0.76  (-. (p1 zenon_Vcd))
% 0.43/0.76  (zenon_Vbi != zenon_Vgg)
% 0.43/0.76  (zenon_Vvl != zenon_Vfb)
% 0.43/0.76  (zenon_Vsl != zenon_Vnh)
% 0.43/0.76  (zenon_Vsl != zenon_Vmf)
% 0.43/0.76  (zenon_Vyk != zenon_Vjd)
% 0.43/0.76  (zenon_Vkj != zenon_Vqf)
% 0.43/0.76  (zenon_Vmh != zenon_Voc)
% 0.43/0.76  (zenon_Vyk != zenon_Vyf)
% 0.43/0.76  (zenon_Vmh != zenon_Vdh)
% 0.43/0.76  (zenon_Vhh != zenon_Vhi)
% 0.43/0.76  (zenon_Vxg != zenon_Vw)
% 0.43/0.76  (zenon_Vol != zenon_Vmf)
% 0.43/0.76  (zenon_Vcl != zenon_Vqf)
% 0.43/0.76  (r1 zenon_Vii zenon_Vni)
% 0.43/0.76  (zenon_Vqi != zenon_Voe)
% 0.43/0.76  (zenon_Vyk != zenon_Vug)
% 0.43/0.76  (p1 zenon_Vwh)
% 0.43/0.76  (zenon_Vwj != zenon_Vka)
% 0.43/0.76  (zenon_Vgi != zenon_Vlj)
% 0.43/0.76  (zenon_Vik != zenon_Vug)
% 0.43/0.76  (zenon_Vek != zenon_Vhc)
% 0.43/0.76  (zenon_Vrh != zenon_Vya)
% 0.43/0.76  (zenon_Vrh != zenon_Vsh)
% 0.43/0.76  (zenon_Vqi != zenon_Vmb)
% 0.43/0.76  (zenon_Vgi != zenon_Vya)
% 0.43/0.76  (zenon_Vsl != zenon_Vef)
% 0.43/0.76  (zenon_Vcl != zenon_Vkg)
% 0.43/0.76  (zenon_Vqk != zenon_Vbj)
% 0.43/0.76  (zenon_Vxg != zenon_Vih)
% 0.43/0.76  (r1 zenon_Vdj zenon_Vgj)
% 0.43/0.76  (zenon_Vgi != zenon_Vri)
% 0.43/0.76  (zenon_Vtg != zenon_Vwi)
% 0.43/0.76  (zenon_Vfj != zenon_Voe)
% 0.43/0.76  (p1 zenon_Vgl)
% 0.43/0.76  (zenon_Vwh != zenon_Vih)
% 0.43/0.76  (zenon_Vkl != zenon_Vjd)
% 0.43/0.76  (zenon_Vtg != zenon_Vgg)
% 0.43/0.76  (zenon_Vvl != zenon_Vaf)
% 0.43/0.76  (zenon_Vol != zenon_Voe)
% 0.43/0.76  (zenon_Vik != zenon_Vif)
% 0.43/0.76  (zenon_Vgi != zenon_Vmf)
% 0.43/0.76  (zenon_Vkl != zenon_Vuf)
% 0.43/0.76  (zenon_Vgi != zenon_Vog)
% 0.43/0.76  (zenon_Vvi != zenon_Vih)
% 0.43/0.76  (zenon_Vgl != zenon_Vlj)
% 0.43/0.76  (zenon_Vkl != zenon_Vac)
% 0.43/0.76  (zenon_Vcl != zenon_Vef)
% 0.43/0.76  (zenon_Vvl != zenon_Vnh)
% 0.43/0.76  (zenon_Vqi != zenon_Vsh)
% 0.43/0.76  (zenon_Vhh != zenon_Vtb)
% 0.43/0.76  (-. (p1 zenon_Vda))
% 0.43/0.76  (zenon_Vtg != zenon_Vjd)
% 0.43/0.76  (r1 zenon_Vmd zenon_Vnd)
% 0.43/0.76  (zenon_Vcl != zenon_Vwe)
% 0.43/0.76  (zenon_Vrh != zenon_Vwe)
% 0.43/0.76  (zenon_Vkl != zenon_Vmi)
% 0.43/0.76  (zenon_Vek != zenon_Vse)
% 0.43/0.76  (zenon_Vkl != zenon_Vw)
% 0.43/0.76  (zenon_Vmk != zenon_Vka)
% 0.43/0.76  (zenon_Vwh != zenon_Vmf)
% 0.43/0.76  (zenon_Vgl != zenon_Vya)
% 0.43/0.76  (zenon_Vkl != zenon_Voc)
% 0.43/0.76  (zenon_Vsl != zenon_Vci)
% 0.43/0.76  (zenon_Vsl != zenon_Vsh)
% 0.43/0.76  (zenon_Vak != zenon_Vac)
% 0.43/0.76  (zenon_Vuk != zenon_Vhc)
% 0.43/0.76  (r1 zenon_X4 zenon_Vp)
% 0.43/0.76  (zenon_Vmh != zenon_Vug)
% 0.43/0.76  (zenon_Vwj != zenon_Vef)
% 0.43/0.76  (zenon_Vsl != zenon_Vrg)
% 0.43/0.76  (zenon_Vsj != zenon_Vcd)
% 0.43/0.76  (zenon_Vsj != zenon_Vka)
% 0.43/0.76  (zenon_Vtg != zenon_Vog)
% 0.43/0.76  (zenon_Vyk != zenon_Vsh)
% 0.43/0.76  (zenon_Vik != zenon_Vfb)
% 0.43/0.76  (zenon_Vch != zenon_Vuf)
% 0.43/0.76  (zenon_Vkj != zenon_Vif)
% 0.43/0.76  (zenon_Vvi != zenon_Vse)
% 0.43/0.76  (r1 zenon_Vah zenon_Vbh)
% 0.43/0.76  (zenon_Vik != zenon_Vjd)
% 0.43/0.76  (zenon_Vqi != zenon_Vdh)
% 0.43/0.76  (r1 zenon_Vsi zenon_Vti)
% 0.43/0.76  (zenon_Vcl != zenon_Vri)
% 0.43/0.76  (zenon_Vhh != zenon_Vri)
% 0.43/0.76  (zenon_Vak != zenon_Vtb)
% 0.43/0.76  (zenon_Vaj != zenon_Vhc)
% 0.43/0.76  (zenon_Vli != zenon_Vxh)
% 0.43/0.76  (zenon_Vsj != zenon_Vmb)
% 0.43/0.76  (zenon_Vkl != zenon_Vtb)
% 0.43/0.76  (zenon_Vyk != zenon_Vbj)
% 0.43/0.76  (zenon_Vqi != zenon_Vjd)
% 0.43/0.76  (zenon_Vxg != zenon_Vrg)
% 0.43/0.76  (zenon_Vhh != zenon_Vfb)
% 0.43/0.76  (zenon_Vmk != zenon_Vef)
% 0.43/0.76  (zenon_Vxg != zenon_Vdh)
% 0.43/0.76  (zenon_Vwj != zenon_Vtb)
% 0.43/0.76  (zenon_Vrh != zenon_Voc)
% 0.43/0.76  (zenon_Vmk != zenon_Voe)
% 0.43/0.76  (zenon_Vqk != zenon_Vyg)
% 0.43/0.76  (zenon_Vmh != zenon_Vcd)
% 0.43/0.76  (zenon_Vol != zenon_Vgj)
% 0.43/0.76  (zenon_Vaj != zenon_Vaf)
% 0.43/0.76  (zenon_Vuk != zenon_Vmb)
% 0.43/0.76  (zenon_Vqi != zenon_Vih)
% 0.43/0.76  (zenon_Vuk != zenon_Voc)
% 0.43/0.76  (r1 zenon_Vzg zenon_Veh)
% 0.43/0.76  (zenon_Vsj != zenon_Vug)
% 0.43/0.76  (zenon_Vwj != zenon_Vdh)
% 0.43/0.76  (zenon_Vqk != zenon_Vsh)
% 0.43/0.76  (zenon_Vcl != zenon_Vaf)
% 0.43/0.76  (zenon_Vuk != zenon_Vra)
% 0.43/0.76  (-. (p1 zenon_Vwi))
% 0.43/0.76  (zenon_Vmh != zenon_Voe)
% 0.43/0.76  (zenon_Vqi != zenon_Vqf)
% 0.43/0.76  (zenon_Vuk != zenon_Vsh)
% 0.43/0.76  (zenon_Vwj != zenon_Vse)
% 0.43/0.76  (r1 zenon_Vpe zenon_Vse)
% 0.43/0.76  (zenon_Vgi != zenon_Voe)
% 0.43/0.76  (zenon_Vvl != zenon_Vse)
% 0.43/0.76  (zenon_Vtg != zenon_Vmi)
% 0.43/0.76  (zenon_Vbi != zenon_Vug)
% 0.43/0.76  (zenon_Vqk != zenon_Voc)
% 0.43/0.76  (zenon_Vcl != zenon_Vyf)
% 0.43/0.76  (zenon_Vsj != zenon_Vgg)
% 0.43/0.76  (zenon_Vvi != zenon_Vci)
% 0.43/0.76  (zenon_Vgi != zenon_Vyf)
% 0.43/0.76  (zenon_Vgl != zenon_Vef)
% 0.43/0.76  (zenon_Vsl != zenon_Vbj)
% 0.43/0.76  (r1 zenon_Vma zenon_Vqa)
% 0.43/0.76  (zenon_Vqk != zenon_Vse)
% 0.43/0.76  (zenon_Vwh != zenon_Vya)
% 0.43/0.76  (zenon_Vmk != zenon_Vhi)
% 0.43/0.76  (p1 zenon_Vhh)
% 0.43/0.76  (zenon_Vek != zenon_Vwi)
% 0.43/0.76  (zenon_Vqi != zenon_Vyg)
% 0.43/0.76  (-. (p1 zenon_Vkg))
% 0.43/0.76  (zenon_Vak != zenon_Vqf)
% 0.43/0.76  (zenon_Vli != zenon_Vac)
% 0.43/0.76  (zenon_Vvl != zenon_Vmi)
% 0.43/0.76  (zenon_Vmk != zenon_Vse)
% 0.43/0.76  (r1 zenon_Vij zenon_Vjj)
% 0.43/0.76  (zenon_Vik != zenon_Vyg)
% 0.43/0.76  (r1 zenon_Vjh zenon_Vkh)
% 0.43/0.76  (zenon_Vgi != zenon_Vvc)
% 0.43/0.76  (zenon_Vuk != zenon_Vci)
% 0.43/0.76  (zenon_Vgl != zenon_Vci)
% 0.43/0.76  (zenon_Vaj != zenon_Vuf)
% 0.43/0.76  (zenon_Vmh != zenon_Vuf)
% 0.43/0.76  (zenon_Vfj != zenon_Vmb)
% 0.43/0.76  (-. (p1 zenon_Vq))
% 0.43/0.76  (p1 zenon_Vek)
% 0.43/0.76  (zenon_Vch != zenon_Vsh)
% 0.43/0.76  (zenon_Vek != zenon_Vfb)
% 0.43/0.76  (zenon_Vxg != zenon_Vsh)
% 0.43/0.76  (zenon_Vgi != zenon_Vw)
% 0.43/0.76  (zenon_Vgl != zenon_Voe)
% 0.43/0.76  (zenon_Vol != zenon_Vih)
% 0.43/0.76  (zenon_Vmk != zenon_Vkg)
% 0.43/0.76  (zenon_Vwh != zenon_Vrg)
% 0.43/0.76  (zenon_Vik != zenon_Vbj)
% 0.43/0.76  (zenon_Vli != zenon_Vgj)
% 0.43/0.76  (r1 zenon_Veh zenon_Vjh)
% 0.43/0.76  (zenon_Vcl != zenon_Vlj)
% 0.43/0.76  (zenon_Vaj != zenon_Vrg)
% 0.43/0.76  (zenon_Vrh != zenon_Vnh)
% 0.43/0.76  (r1 zenon_Vcj zenon_Vdj)
% 0.43/0.76  (zenon_Vmk != zenon_Vw)
% 0.43/0.76  (p1 zenon_Vgi)
% 0.43/0.76  (zenon_Vwj != zenon_Vxh)
% 0.43/0.76  (zenon_Vch != zenon_Voe)
% 0.43/0.76  (zenon_Vik != zenon_Vda)
% 0.43/0.76  (zenon_Vvl != zenon_Vhc)
% 0.43/0.76  (zenon_Vgi != zenon_Vbj)
% 0.43/0.76  (zenon_Vvl != zenon_Vdh)
% 0.43/0.76  (zenon_Vbi != zenon_Vxh)
% 0.43/0.76  (zenon_Vch != zenon_Vq)
% 0.43/0.76  (zenon_Vak != zenon_Vyf)
% 0.43/0.76  (-. (p1 zenon_Vmi))
% 0.43/0.76  (r1 zenon_Vbk zenon_Vek)
% 0.43/0.76  (zenon_Vkj != zenon_Vnh)
% 0.43/0.76  (zenon_Vch != zenon_Vmi)
% 0.43/0.76  (-. (p1 zenon_Vgg))
% 0.43/0.76  (zenon_Vhh != zenon_Vci)
% 0.43/0.76  (r1 zenon_Vkd zenon_Vyd)
% 0.43/0.76  (zenon_Vli != zenon_Vdh)
% 0.43/0.76  (zenon_Vvl != zenon_Vif)
% 0.43/0.76  (r1 zenon_Vhg zenon_Vkg)
% 0.43/0.76  (zenon_Vhh != zenon_Vjd)
% 0.43/0.76  (zenon_Vli != zenon_Vsh)
% 0.43/0.76  (zenon_Vgl != zenon_Vwe)
% 0.43/0.76  (zenon_Vmk != zenon_Vmi)
% 0.43/0.76  (zenon_Vmh != zenon_Vra)
% 0.43/0.76  (zenon_Vmh != zenon_Vif)
% 0.43/0.76  (zenon_Vwh != zenon_Vif)
% 0.43/0.76  (r1 zenon_Vfh zenon_Vih)
% 0.43/0.76  (zenon_Vol != zenon_Vhi)
% 0.43/0.76  (zenon_Vek != zenon_Vif)
% 0.43/0.76  (zenon_Vvi != zenon_Vra)
% 0.43/0.76  (zenon_Vik != zenon_Vaf)
% 0.43/0.76  (zenon_Vuk != zenon_Vyf)
% 0.43/0.76  (zenon_Vaj != zenon_Vsh)
% 0.43/0.76  (zenon_Vrh != zenon_Vdh)
% 0.43/0.76  (zenon_Vyk != zenon_Vda)
% 0.43/0.76  (zenon_Vgi != zenon_Voc)
% 0.43/0.76  (zenon_Vsj != zenon_Vmi)
% 0.43/0.76  (zenon_Vqk != zenon_Voe)
% 0.43/0.76  (zenon_Vch != zenon_Vih)
% 0.43/0.76  (zenon_Vyk != zenon_Vlj)
% 0.43/0.76  (zenon_Vsj != zenon_Vtb)
% 0.43/0.76  (zenon_Vrh != zenon_Vif)
% 0.43/0.76  (r1 zenon_Vjk zenon_Vmk)
% 0.43/0.76  (zenon_Vsl != zenon_Voe)
% 0.43/0.76  (zenon_Vsl != zenon_Vcd)
% 0.43/0.76  (zenon_Vik != zenon_Vhi)
% 0.43/0.76  (zenon_Vli != zenon_Vnh)
% 0.43/0.76  (zenon_Vyk != zenon_Vri)
% 0.43/0.76  (zenon_Vgl != zenon_Vyg)
% 0.43/0.76  (zenon_Vmk != zenon_Vtb)
% 0.43/0.76  (zenon_Vli != zenon_Vvc)
% 0.43/0.76  (zenon_Vtg != zenon_Vlj)
% 0.43/0.76  (zenon_Vsl != zenon_Vtb)
% 0.43/0.76  (zenon_Vrh != zenon_Vac)
% 0.43/0.76  (zenon_Vak != zenon_Vcg)
% 0.43/0.76  (zenon_Vmk != zenon_Vcd)
% 0.43/0.76  (zenon_Vvi != zenon_Vcd)
% 0.43/0.76  (p1 zenon_Vol)
% 0.43/0.76  (r1 zenon_Vyi zenon_Vbj)
% 0.43/0.76  (zenon_Vcl != zenon_Vmi)
% 0.43/0.76  (zenon_Vbi != zenon_Vef)
% 0.43/0.76  (zenon_Vgl != zenon_Vq)
% 0.43/0.76  (r1 zenon_Vob zenon_Vsb)
% 0.43/0.76  (zenon_Vik != zenon_Vlj)
% 0.43/0.76  (zenon_Vvi != zenon_Vjd)
% 0.43/0.76  (zenon_Vgi != zenon_Vtb)
% 0.43/0.76  (zenon_Vch != zenon_Vda)
% 0.43/0.76  (zenon_Vfj != zenon_Vwi)
% 0.43/0.76  (zenon_Vvi != zenon_Vtb)
% 0.43/0.76  (zenon_Vwj != zenon_Vug)
% 0.43/0.76  (zenon_Vkj != zenon_Vef)
% 0.43/0.76  (zenon_Vkl != zenon_Vaf)
% 0.43/0.76  (zenon_Vsl != zenon_Vxh)
% 0.43/0.76  (zenon_Vak != zenon_Vhc)
% 0.43/0.76  (zenon_Vkj != zenon_Voe)
% 0.43/0.76  (zenon_Vik != zenon_Vka)
% 0.43/0.76  (zenon_Vqi != zenon_Vka)
% 0.43/0.76  (r1 zenon_Vkd zenon_Vje)
% 0.43/0.76  (zenon_Vsj != zenon_Vjd)
% 0.43/0.76  (zenon_Vkj != zenon_Vaf)
% 0.43/0.76  (zenon_Vkj != zenon_Vsh)
% 0.43/0.76  (zenon_Vek != zenon_Vgg)
% 0.43/0.76  (zenon_Vyk != zenon_Vvc)
% 0.43/0.76  (-. (p1 zenon_Vxh))
% 0.43/0.76  (zenon_Vli != zenon_Voc)
% 0.43/0.76  (zenon_Vhh != zenon_Vw)
% 0.43/0.76  (-. (p1 zenon_Vfb))
% 0.43/0.76  (zenon_Vik != zenon_Vmi)
% 0.43/0.76  (zenon_Vvl != zenon_Vvc)
% 0.43/0.76  (zenon_Vak != zenon_Vfb)
% 0.43/0.76  (zenon_Vak != zenon_Vsh)
% 0.43/0.76  (zenon_Vvl != zenon_Vjd)
% 0.43/0.76  (zenon_Vek != zenon_Vyf)
% 0.43/0.76  (zenon_Vwj != zenon_Vrg)
% 0.43/0.76  (zenon_Vrh != zenon_Vgj)
% 0.43/0.76  (zenon_Vch != zenon_Vnh)
% 0.43/0.76  (zenon_Vwh != zenon_Vef)
% 0.43/0.76  (r1 zenon_Vqc zenon_Vuc)
% 0.43/0.76  (zenon_Vsl != zenon_Vih)
% 0.43/0.76  (p1 zenon_Vli)
% 0.43/0.76  (zenon_Vuk != zenon_Vnh)
% 0.43/0.76  (zenon_Vqi != zenon_Vra)
% 0.43/0.76  (zenon_Vmh != zenon_Vvc)
% 0.43/0.76  (zenon_Vwj != zenon_Vqf)
% 0.43/0.76  (zenon_Vwj != zenon_Vmi)
% 0.43/0.76  (zenon_Vxg != zenon_Vka)
% 0.43/0.76  (r1 zenon_Vdi zenon_Vei)
% 0.43/0.76  (zenon_Vuk != zenon_Vwe)
% 0.43/0.76  (zenon_Vkj != zenon_Vvc)
% 0.43/0.76  (zenon_Vtg != zenon_Vmb)
% 0.43/0.76  (zenon_Vch != zenon_Vef)
% 0.43/0.76  (zenon_Vak != zenon_Vmf)
% 0.43/0.76  (zenon_Vtg != zenon_Vri)
% 0.43/0.76  (r1 zenon_Vzh zenon_Vci)
% 0.43/0.76  (zenon_Vaj != zenon_Vug)
% 0.43/0.76  (zenon_Vak != zenon_Vug)
% 0.43/0.76  (zenon_Vol != zenon_Vw)
% 0.43/0.76  (zenon_Vqi != zenon_Vnh)
% 0.43/0.76  (zenon_Vsj != zenon_Vaf)
% 0.43/0.76  (zenon_Vuk != zenon_Vdh)
% 0.43/0.76  (zenon_Vmk != zenon_Vqf)
% 0.43/0.76  (zenon_Vcl != zenon_Vfb)
% 0.43/0.76  (zenon_Vqk != zenon_Vmf)
% 0.43/0.76  (zenon_Vsl != zenon_Vkg)
% 0.43/0.76  (zenon_Vch != zenon_Vri)
% 0.43/0.76  (zenon_Vek != zenon_Vmf)
% 0.43/0.76  (zenon_Vli != zenon_Vmb)
% 0.43/0.76  (zenon_Vol != zenon_Vgg)
% 0.43/0.76  (zenon_Vhh != zenon_Vgj)
% 0.43/0.76  (zenon_Vxg != zenon_Vog)
% 0.43/0.76  (zenon_Vuk != zenon_Vgg)
% 0.43/0.76  (zenon_Vrh != zenon_Vxh)
% 0.43/0.76  (r1 zenon_Vyi zenon_Vzi)
% 0.43/0.76  (zenon_Vkl != zenon_Vhi)
% 0.43/0.76  (zenon_Vyk != zenon_Vq)
% 0.43/0.76  (zenon_Vak != zenon_Vq)
% 0.43/0.76  (zenon_Vvi != zenon_Vmf)
% 0.43/0.76  (zenon_Vvi != zenon_Vya)
% 0.43/0.76  (zenon_Vak != zenon_Vwe)
% 0.43/0.76  (zenon_Vvi != zenon_Vaf)
% 0.43/0.76  (zenon_Vik != zenon_Vri)
% 0.43/0.76  (zenon_Vvi != zenon_Vq)
% 0.43/0.76  (zenon_Vxg != zenon_Vcd)
% 0.43/0.76  (zenon_Vfj != zenon_Vwe)
% 0.43/0.76  (zenon_Vli != zenon_Vhi)
% 0.43/0.76  (zenon_Vyk != zenon_Voe)
% 0.43/0.76  (zenon_Vsl != zenon_Vug)
% 0.43/0.76  (zenon_Vol != zenon_Vhc)
% 0.43/0.76  (zenon_Vrh != zenon_Vvc)
% 0.43/0.76  (zenon_Vmh != zenon_Vse)
% 0.43/0.76  (zenon_Vqi != zenon_Vmf)
% 0.43/0.76  (zenon_Vrh != zenon_Vri)
% 0.43/0.76  (zenon_Vhh != zenon_Vnh)
% 0.43/0.76  (r1 zenon_X6 zenon_Vrg)
% 0.43/0.76  (r1 zenon_Voh zenon_Vth)
% 0.43/0.76  (zenon_Vrh != zenon_Vmf)
% 0.43/0.76  (zenon_Vgi != zenon_Vq)
% 0.43/0.76  (zenon_Vsj != zenon_Vyf)
% 0.43/0.76  (zenon_Vwj != zenon_Vmf)
% 0.43/0.76  (zenon_Vaj != zenon_Vse)
% 0.43/0.76  (zenon_Vkl != zenon_Vfb)
% 0.43/0.76  (zenon_Vhh != zenon_Vyg)
% 0.43/0.76  (zenon_Vmk != zenon_Vfb)
% 0.43/0.76  (zenon_Vol != zenon_Vaf)
% 0.43/0.76  (zenon_Vwj != zenon_Vbj)
% 0.43/0.76  (zenon_Vqi != zenon_Vef)
% 0.43/0.76  (zenon_Vbi != zenon_Vsh)
% 0.43/0.76  (zenon_Vyk != zenon_Vcd)
% 0.43/0.76  (r1 zenon_Vkh zenon_Vlh)
% 0.43/0.76  (zenon_Vqk != zenon_Vra)
% 0.43/0.76  (zenon_Vsl != zenon_Vwi)
% 0.43/0.76  (zenon_Vuk != zenon_Vlj)
% 0.43/0.76  (zenon_Vol != zenon_Vcg)
% 0.43/0.76  (zenon_Vak != zenon_Vxh)
% 0.43/0.76  (zenon_Vqk != zenon_Vaf)
% 0.43/0.76  (zenon_Vol != zenon_Vog)
% 0.43/0.76  (zenon_Vkl != zenon_Vrg)
% 0.43/0.76  (r1 zenon_Vld zenon_Vmd)
% 0.43/0.76  (-. (p1 zenon_Vif))
% 0.43/0.76  (zenon_Vkj != zenon_Vra)
% 0.43/0.76  (zenon_Vsj != zenon_Vci)
% 0.43/0.76  (r1 zenon_Vph zenon_Vsh)
% 0.43/0.76  (zenon_Vaj != zenon_Voe)
% 0.43/0.76  (-. (p1 zenon_Vgj))
% 0.43/0.76  (zenon_Vol != zenon_Vri)
% 0.43/0.76  (-. (p1 zenon_Voc))
% 0.43/0.76  (zenon_Vvi != zenon_Vvc)
% 0.43/0.76  (zenon_Vgl != zenon_Vda)
% 0.43/0.76  (zenon_Vuk != zenon_Vuf)
% 0.43/0.76  (r1 zenon_Vdi zenon_Vii)
% 0.43/0.76  (zenon_Vik != zenon_Vtb)
% 0.43/0.76  (zenon_Vaj != zenon_Vri)
% 0.43/0.76  (zenon_Vcl != zenon_Voe)
% 0.43/0.76  (zenon_Vsl != zenon_Vra)
% 0.43/0.76  (zenon_Vik != zenon_Vxh)
% 0.43/0.76  (zenon_Vcl != zenon_Vjd)
% 0.43/0.76  (zenon_Vkl != zenon_Vef)
% 0.43/0.76  (zenon_Vmk != zenon_Vxh)
% 0.43/0.76  (zenon_Vqk != zenon_Vmi)
% 0.43/0.76  (zenon_Vvl != zenon_Vrg)
% 0.43/0.76  (zenon_Vrh != zenon_Vfb)
% 0.43/0.76  (r1 zenon_Vhj zenon_Vmj)
% 0.43/0.76  (zenon_Vak != zenon_Vw)
% 0.43/0.76  (zenon_Vfj != zenon_Vgj)
% 0.43/0.76  (zenon_Vxg != zenon_Vfb)
% 0.43/0.76  (zenon_Vhh != zenon_Vaf)
% 0.43/0.76  (zenon_Vgl != zenon_Vnh)
% 0.43/0.76  (zenon_Vgi != zenon_Vmb)
% 0.43/0.76  (zenon_Vik != zenon_Vwi)
% 0.43/0.76  (zenon_Vvl != zenon_Vmf)
% 0.43/0.76  (zenon_Vhh != zenon_Vcg)
% 0.43/0.76  (zenon_Vik != zenon_Vef)
% 0.43/0.76  (zenon_Vwj != zenon_Vgg)
% 0.43/0.76  (r1 zenon_Vdg zenon_Vgg)
% 0.43/0.76  (zenon_Vvi != zenon_Vlj)
% 0.43/0.76  (zenon_Vxg != zenon_Vvc)
% 0.43/0.76  (-. (p1 zenon_Vw))
% 0.43/0.76  (zenon_Vsj != zenon_Vvc)
% 0.43/0.76  (r1 zenon_Vvb zenon_Vzb)
% 0.43/0.76  (zenon_Vek != zenon_Vri)
% 0.43/0.76  (zenon_Vfj != zenon_Vfb)
% 0.43/0.76  (zenon_Vgi != zenon_Vgg)
% 0.43/0.76  (zenon_Vhh != zenon_Vwi)
% 0.43/0.76  (zenon_Vaj != zenon_Vjd)
% 0.43/0.76  (r1 zenon_Vcc zenon_Vgc)
% 0.43/0.76  (zenon_Vvl != zenon_Vih)
% 0.43/0.76  (zenon_Vhh != zenon_Vlj)
% 0.43/0.76  (zenon_Vuk != zenon_Vka)
% 0.43/0.76  (zenon_Vol != zenon_Vyf)
% 0.43/0.76  (zenon_Vyk != zenon_Vgg)
% 0.43/0.76  (zenon_Vtg != zenon_Vkg)
% 0.43/0.76  (zenon_Vgi != zenon_Vwe)
% 0.43/0.76  (zenon_Vmh != zenon_Vgj)
% 0.43/0.76  (zenon_Vtg != zenon_Vci)
% 0.43/0.76  (zenon_Vch != zenon_Vcd)
% 0.43/0.76  (zenon_Vbi != zenon_Vse)
% 0.43/0.76  (zenon_Vwh != zenon_Vmi)
% 0.43/0.76  (zenon_Vgl != zenon_Vgj)
% 0.43/0.76  (zenon_Vmh != zenon_Vhi)
% 0.43/0.76  (zenon_Vaj != zenon_Vnh)
% 0.43/0.76  (r1 zenon_Vii zenon_Vji)
% 0.43/0.76  (zenon_Vwh != zenon_Voe)
% 0.43/0.76  (r1 zenon_Vyh zenon_Vdi)
% 0.43/0.76  (zenon_Vvl != zenon_Voe)
% 0.43/0.76  (zenon_Vol != zenon_Vxh)
% 0.43/0.76  (zenon_Vvl != zenon_Vac)
% 0.43/0.76  (zenon_Vek != zenon_Vlj)
% 0.43/0.76  (zenon_Vli != zenon_Vjd)
% 0.43/0.76  (zenon_Vsj != zenon_Vya)
% 0.43/0.76  (zenon_Vfj != zenon_Vmf)
% 0.43/0.76  (zenon_Vvl != zenon_Vef)
% 0.43/0.76  (zenon_Vgl != zenon_Vuf)
% 0.43/0.76  (zenon_Vmk != zenon_Vlj)
% 0.43/0.76  (-. (p1 zenon_Vri))
% 0.43/0.76  (p1 zenon_Vvi)
% 0.43/0.76  (zenon_Vvi != zenon_Vog)
% 0.43/0.76  (r1 zenon_Vpj zenon_Vsj)
% 0.43/0.76  (r1 zenon_Vff zenon_Vif)
% 0.43/0.76  (zenon_Vsl != zenon_Vse)
% 0.43/0.76  (zenon_Vkl != zenon_Vog)
% 0.43/0.76  (zenon_Vmh != zenon_Vmb)
% 0.43/0.76  (zenon_Vrh != zenon_Vjd)
% 0.43/0.76  (zenon_Vkl != zenon_Vdh)
% 0.43/0.76  (zenon_Vrh != zenon_Vug)
% 0.43/0.76  (zenon_Vik != zenon_Vmf)
% 0.43/0.76  (zenon_Vsj != zenon_Vkg)
% 0.43/0.76  (r1 zenon_Vti zenon_Vui)
% 0.43/0.76  (zenon_Vmh != zenon_Vda)
% 0.43/0.76  (zenon_Vgi != zenon_Vac)
% 0.43/0.76  (zenon_Vgl != zenon_Vsh)
% 0.43/0.76  (zenon_Vkl != zenon_Vbj)
% 0.43/0.76  (zenon_Vqk != zenon_Vq)
% 0.43/0.76  (zenon_Vcl != zenon_Vw)
% 0.43/0.76  (zenon_Vli != zenon_Vda)
% 0.43/0.76  (zenon_Vvl != zenon_Vmb)
% 0.43/0.76  (zenon_Vwh != zenon_Vfb)
% 0.43/0.76  (zenon_Vsl != zenon_Vlj)
% 0.43/0.76  (zenon_Vmk != zenon_Vjd)
% 0.43/0.76  (zenon_Vek != zenon_Vgj)
% 0.43/0.76  (zenon_Vtg != zenon_Vfb)
% 0.43/0.76  (zenon_Vrh != zenon_Vaf)
% 0.43/0.76  (zenon_Vak != zenon_Vwi)
% 0.43/0.76  (zenon_Vek != zenon_Vyg)
% 0.43/0.76  (zenon_Vqk != zenon_Vwi)
% 0.43/0.76  (-. (p1 zenon_Vyf))
% 0.43/0.76  (r1 Tau_0 Tau_1)
% 0.43/0.76  (zenon_Vol != zenon_Vnh)
% 0.43/0.76  (zenon_Vsl != zenon_Vgj)
% 0.43/0.76  (zenon_Vch != zenon_Vra)
% 0.43/0.76  (zenon_Vvi != zenon_Vwi)
% 0.43/0.76  (zenon_Vcl != zenon_Vq)
% 0.43/0.76  (zenon_Vyk != zenon_Vmb)
% 0.43/0.76  (zenon_Vuk != zenon_Vcg)
% 0.43/0.76  (zenon_Vvi != zenon_Vac)
% 0.43/0.76  (zenon_Vvi != zenon_Vka)
% 0.43/0.76  (zenon_Vkj != zenon_Vse)
% 0.43/0.76  (zenon_Vaj != zenon_Vmf)
% 0.43/0.76  (zenon_Vik != zenon_Vya)
% 0.43/0.76  (zenon_Vyk != zenon_Voc)
% 0.43/0.76  (r1 zenon_Vkh zenon_Vnh)
% 0.43/0.76  (zenon_Vwj != zenon_Vuf)
% 0.43/0.76  (zenon_Vol != zenon_Vif)
% 0.43/0.76  (zenon_Vwh != zenon_Vsh)
% 0.43/0.76  (zenon_Vhh != zenon_Vog)
% 0.43/0.76  (zenon_Vuk != zenon_Vfb)
% 0.43/0.76  (zenon_Vrh != zenon_Vrg)
% 0.43/0.76  (r1 zenon_Vvg zenon_Vyg)
% 0.43/0.76  (r1 zenon_Vfh zenon_Vgh)
% 0.43/0.76  (zenon_Vfj != zenon_Vhc)
% 0.43/0.76  (zenon_Vmh != zenon_Vaf)
% 0.43/0.76  (zenon_Vsl != zenon_Vvc)
% 0.43/0.76  (r1 zenon_Vvg zenon_Vwg)
% 0.43/0.76  (zenon_Vvi != zenon_Vef)
% 0.43/0.76  (zenon_Vkj != zenon_Vmi)
% 0.43/0.76  (-. (p4 zenon_X3))
% 0.43/0.76  (zenon_Vsj != zenon_Vif)
% 0.43/0.76  (zenon_Vvl != zenon_Vug)
% 0.43/0.76  (zenon_Vwj != zenon_Vog)
% 0.43/0.76  (zenon_Vfe != zenon_Vzd)
% 0.43/0.76  (zenon_Vvl != zenon_Vq)
% 0.43/0.76  (zenon_Vmk != zenon_Vrg)
% 0.43/0.76  (zenon_Vvi != zenon_Vfb)
% 0.43/0.76  (zenon_Vvl != zenon_Vtb)
% 0.43/0.76  (zenon_Vwh != zenon_Vtb)
% 0.43/0.76  (zenon_Vwh != zenon_Vci)
% 0.43/0.76  (zenon_Vol != zenon_Vcd)
% 0.43/0.76  (zenon_Vhh != zenon_Vwe)
% 0.43/0.76  (zenon_Vvi != zenon_Vrg)
% 0.43/0.76  (zenon_Vvl != zenon_Vog)
% 0.43/0.76  (zenon_Vch != zenon_Vvc)
% 0.43/0.76  (zenon_Vak != zenon_Vaf)
% 0.43/0.76  (zenon_Vkj != zenon_Vkg)
% 0.43/0.76  (zenon_Vwj != zenon_Vwe)
% 0.43/0.76  (zenon_Vsj != zenon_Vyg)
% 0.43/0.76  (zenon_Vyk != zenon_Vmf)
% 0.43/0.76  (r1 zenon_Vrd zenon_Vsd)
% 0.43/0.76  (zenon_Vfj != zenon_Vih)
% 0.43/0.76  (zenon_Vkj != zenon_Vka)
% 0.43/0.76  (zenon_Vvl != zenon_Vkg)
% 0.43/0.76  (r1 zenon_Vdj zenon_Vej)
% 0.43/0.76  (zenon_Vvl != zenon_Vgj)
% 0.43/0.76  (zenon_Vqk != zenon_Vuf)
% 0.43/0.76  (-. (p1 zenon_Vlj))
% 0.43/0.76  (zenon_Vcl != zenon_Vmf)
% 0.43/0.76  (r1 Tau_0 Tau_2)
% 0.43/0.76  (zenon_Vqi != zenon_Vwi)
% 0.43/0.76  (zenon_Vak != zenon_Vse)
% 0.43/0.76  (-. (p1 zenon_Vef))
% 0.43/0.76  (zenon_Vwj != zenon_Voc)
% 0.43/0.76  (r1 zenon_X7 zenon_Vvl)
% 0.43/0.76  (zenon_Vol != zenon_Vlj)
% 0.43/0.76  (zenon_Vkj != zenon_Vac)
% 0.43/0.76  (zenon_Vuk != zenon_Vyg)
% 0.43/0.76  (zenon_Vgl != zenon_Vac)
% 0.43/0.76  (zenon_Vrh != zenon_Vmi)
% 0.43/0.76  (zenon_Vek != zenon_Vbj)
% 0.43/0.76  (zenon_Vli != zenon_Vih)
% 0.43/0.76  (r1 zenon_Vhl zenon_Vkl)
% 0.43/0.76  (zenon_Vcl != zenon_Vhi)
% 0.43/0.76  (zenon_Vbi != zenon_Vhc)
% 0.43/0.76  (zenon_Vyk != zenon_Vif)
% 0.43/0.76  (zenon_Vch != zenon_Vmb)
% 0.43/0.76  (zenon_Vol != zenon_Voc)
% 0.43/0.76  (zenon_Vqk != zenon_Vqf)
% 0.43/0.76  (zenon_Vkj != zenon_Vri)
% 0.43/0.76  (zenon_Vek != zenon_Vug)
% 0.43/0.76  (zenon_Vbi != zenon_Vq)
% 0.43/0.76  (zenon_Vyk != zenon_Vfb)
% 0.43/0.76  (zenon_Vmh != zenon_Vyg)
% 0.43/0.76  (zenon_Vik != zenon_Vq)
% 0.43/0.76  (r1 Tau_2 zenon_Vvg)
% 0.43/0.76  (r1 Tau_2 zenon_Vzg)
% 0.43/0.76  (zenon_Vqi != zenon_Vug)
% 0.43/0.76  (zenon_Vol != zenon_Vq)
% 0.43/0.76  (zenon_Vaj != zenon_Vbj)
% 0.43/0.76  (zenon_Vch != zenon_Vka)
% 0.43/0.76  (zenon_Vmh != zenon_Vrg)
% 0.43/0.76  (zenon_Vkj != zenon_Vog)
% 0.43/0.76  (zenon_Vkl != zenon_Vgg)
% 0.43/0.76  (zenon_Vli != zenon_Vci)
% 0.43/0.76  (zenon_Vhh != zenon_Voe)
% 0.43/0.76  (zenon_Vtg != zenon_Vhc)
% 0.43/0.76  (zenon_Vak != zenon_Vog)
% 0.43/0.76  (zenon_Vch != zenon_Vqf)
% 0.43/0.76  (zenon_Vaj != zenon_Vcg)
% 0.43/0.76  (zenon_Vvi != zenon_Vbj)
% 0.43/0.76  (zenon_Vwj != zenon_Vhc)
% 0.43/0.76  (zenon_Vwj != zenon_Vci)
% 0.43/0.76  (zenon_Vqi != zenon_Vw)
% 0.43/0.76  (zenon_Vxg != zenon_Vjd)
% 0.43/0.76  (zenon_Vsj != zenon_Vwi)
% 0.43/0.76  (zenon_Vwj != zenon_Vcg)
% 0.43/0.76  (zenon_Vrh != zenon_Vci)
% 0.43/0.76  (zenon_Vyk != zenon_Vog)
% 0.43/0.76  (zenon_Vch != zenon_Vog)
% 0.43/0.76  (zenon_Vak != zenon_Vrg)
% 0.43/0.76  (zenon_Vfj != zenon_Vya)
% 0.43/0.76  (zenon_Vwj != zenon_Vkg)
% 0.43/0.76  (zenon_Vol != zenon_Vda)
% 0.43/0.76  (zenon_Vwh != zenon_Vda)
% 0.43/0.76  (zenon_Vbi != zenon_Vif)
% 0.43/0.76  (zenon_Vtg != zenon_Vka)
% 0.43/0.76  (zenon_Vwh != zenon_Vra)
% 0.43/0.76  (zenon_Vxg != zenon_Vra)
% 0.43/0.76  (zenon_Vbi != zenon_Vog)
% 0.43/0.76  (zenon_Vli != zenon_Vrg)
% 0.43/0.76  (zenon_Vqk != zenon_Vwe)
% 0.43/0.76  (zenon_Vmk != zenon_Vuf)
% 0.43/0.76  (-. (p3 zenon_Vnd))
% 0.43/0.76  (zenon_Vli != zenon_Vmf)
% 0.43/0.76  (zenon_Vkl != zenon_Vyg)
% 0.43/0.76  (zenon_Vxg != zenon_Vaf)
% 0.43/0.76  (p1 zenon_Vtg)
% 0.43/0.76  (zenon_Vli != zenon_Vyg)
% 0.43/0.76  (zenon_Vrh != zenon_Vw)
% 0.43/0.76  (zenon_Vyk != zenon_Vka)
% 0.43/0.76  (zenon_Vfj != zenon_Vgg)
% 0.43/0.76  (zenon_Vol != zenon_Vtb)
% 0.43/0.76  (zenon_Vtg != zenon_Voe)
% 0.43/0.76  (zenon_Vqi != zenon_Vrg)
% 0.43/0.76  (r1 zenon_Vth zenon_Vyh)
% 0.43/0.76  (zenon_Vfj != zenon_Vjd)
% 0.43/0.76  (zenon_Vek != zenon_Vw)
% 0.43/0.76  (zenon_Vli != zenon_Vtb)
% 0.43/0.76  (zenon_Vfj != zenon_Vdh)
% 0.43/0.76  (zenon_Vch != zenon_Vcg)
% 0.43/0.76  (zenon_Vgl != zenon_Vaf)
% 0.43/0.76  (zenon_Vek != zenon_Voe)
% 0.43/0.76  (zenon_Vch != zenon_Vtb)
% 0.43/0.76  (zenon_Vxg != zenon_Vya)
% 0.43/0.76  (zenon_Vhh != zenon_Vka)
% 0.43/0.76  (zenon_Vek != zenon_Vjd)
% 0.43/0.76  (zenon_Vak != zenon_Vef)
% 0.43/0.76  (zenon_Vgi != zenon_Vqf)
% 0.43/0.76  (zenon_Vol != zenon_Vac)
% 0.43/0.76  (zenon_Vli != zenon_Vlj)
% 0.43/0.76  (zenon_Vwh != zenon_Vri)
% 0.43/0.76  (zenon_Vmk != zenon_Vwe)
% 0.43/0.76  (zenon_Vgl != zenon_Vkg)
% 0.43/0.76  (r1 Tau_1 zenon_Vsg)
% 0.43/0.76  (zenon_Vol != zenon_Vci)
% 0.43/0.76  (zenon_Vwh != zenon_Vq)
% 0.43/0.76  (zenon_Vsj != zenon_Vq)
% 0.43/0.76  (zenon_Vgl != zenon_Vug)
% 0.43/0.76  (zenon_Vqi != zenon_Vgg)
% 0.43/0.76  (-. (p1 zenon_Vyg))
% 0.43/0.76  (zenon_Vkl != zenon_Vra)
% 0.43/0.76  (zenon_Vek != zenon_Vcg)
% 0.43/0.76  (zenon_Vaj != zenon_Vxh)
% 0.43/0.76  (zenon_Vak != zenon_Vci)
% 0.43/0.76  (zenon_Vgl != zenon_Vyf)
% 0.43/0.76  (r1 zenon_Voh zenon_Vph)
% 0.43/0.76  (r1 zenon_Vth zenon_Vuh)
% 0.43/0.76  (r1 zenon_Vph zenon_Vqh)
% 0.43/0.76  (zenon_Vsj != zenon_Vgj)
% 0.43/0.76  (zenon_Vak != zenon_Vjd)
% 0.43/0.76  (zenon_Vfj != zenon_Vkg)
% 0.43/0.76  (zenon_Vek != zenon_Vrg)
% 0.43/0.76  (zenon_Vxg != zenon_Vuf)
% 0.43/0.76  (zenon_Vkj != zenon_Vwi)
% 0.43/0.76  (zenon_Vmh != zenon_Vya)
% 0.43/0.76  (zenon_Vqk != zenon_Vxh)
% 0.43/0.76  (-. (p1 zenon_Vnh))
% 0.43/0.76  (zenon_Vsj != zenon_Vbj)
% 0.43/0.76  (zenon_Vhh != zenon_Vmi)
% 0.43/0.76  (zenon_Vbi != zenon_Vrg)
% 0.43/0.76  (zenon_Vek != zenon_Vih)
% 0.43/0.76  (zenon_Vkj != zenon_Vih)
% 0.43/0.76  (zenon_Vqi != zenon_Vmi)
% 0.43/0.76  (zenon_Vbi != zenon_Vyg)
% 0.43/0.76  (zenon_Vxg != zenon_Vyg)
% 0.43/0.76  (zenon_Vaj != zenon_Vfb)
% 0.43/0.76  (zenon_Vxg != zenon_Vif)
% 0.43/0.76  (zenon_Vek != zenon_Vhi)
% 0.43/0.76  (zenon_Vfj != zenon_Vcg)
% 0.43/0.76  (zenon_Vmd != zenon_Vzd)
% 0.43/0.76  (zenon_Vuk != zenon_Vxh)
% 0.43/0.76  (r1 zenon_Vy zenon_Vca)
% 0.43/0.76  (zenon_Vvi != zenon_Vyf)
% 0.43/0.76  (zenon_Vak != zenon_Vgg)
% 0.43/0.76  (zenon_Vsl != zenon_Vyf)
% 0.43/0.76  (zenon_Vgi != zenon_Vkg)
% 0.43/0.76  (zenon_Vol != zenon_Vug)
% 0.43/0.76  (zenon_Vfj != zenon_Vef)
% 0.43/0.76  (zenon_Vmk != zenon_Vq)
% 0.43/0.76  (zenon_Vqk != zenon_Vya)
% 0.43/0.76  (zenon_Vak != zenon_Vvc)
% 0.43/0.76  (zenon_Vrh != zenon_Vog)
% 0.43/0.76  (zenon_Vvl != zenon_Vra)
% 0.43/0.76  (zenon_Vvl != zenon_Vxh)
% 0.43/0.76  (zenon_Vmk != zenon_Vda)
% 0.43/0.76  (zenon_Vbi != zenon_Vkg)
% 0.43/0.76  (zenon_Vgi != zenon_Vci)
% 0.43/0.76  (zenon_Vyk != zenon_Vaf)
% 0.43/0.76  (zenon_Vaj != zenon_Vkg)
% 0.43/0.76  (zenon_Vol != zenon_Vef)
% 0.43/0.76  (zenon_Vxg != zenon_Vug)
% 0.43/0.76  (zenon_Vuk != zenon_Vhi)
% 0.43/0.76  (zenon_Vsl != zenon_Vgg)
% 0.43/0.76  (zenon_Vch != zenon_Vyg)
% 0.43/0.76  (zenon_Vqi != zenon_Vxh)
% 0.43/0.76  (zenon_Vuk != zenon_Vri)
% 0.43/0.76  (zenon_Vuk != zenon_Vog)
% 0.43/0.76  (zenon_Vuk != zenon_Vya)
% 0.43/0.76  (zenon_Vgi != zenon_Vhc)
% 0.43/0.76  (zenon_Vch != zenon_Vse)
% 0.43/0.76  (zenon_Vyk != zenon_Vuf)
% 0.43/0.76  (zenon_Vik != zenon_Vmb)
% 0.43/0.76  (zenon_Vkj != zenon_Vq)
% 0.43/0.76  (zenon_Vli != zenon_Vra)
% 0.43/0.76  (zenon_Vik != zenon_Vyf)
% 0.43/0.76  (zenon_Vbi != zenon_Vaf)
% 0.43/0.76  (zenon_Vvl != zenon_Vka)
% 0.43/0.76  (zenon_Vkj != zenon_Vxh)
% 0.43/0.76  (zenon_Vyk != zenon_Vhc)
% 0.43/0.76  (zenon_Vxg != zenon_Vda)
% 0.43/0.76  (zenon_Vgl != zenon_Vbj)
% 0.43/0.76  (zenon_Vfj != zenon_Vvc)
% 0.43/0.76  (zenon_Vvi != zenon_Vif)
% 0.43/0.76  (zenon_Vxg != zenon_Vci)
% 0.43/0.76  (zenon_Vfj != zenon_Vbj)
% 0.43/0.76  (zenon_Vqi != zenon_Vcg)
% 0.43/0.76  (zenon_Vol != zenon_Vkg)
% 0.43/0.76  (zenon_Vvi != zenon_Voc)
% 0.43/0.76  (zenon_Vgi != zenon_Vyg)
% 0.43/0.76  (zenon_Vxg != zenon_Vbj)
% 0.43/0.76  (zenon_Vik != zenon_Vvc)
% 0.43/0.76  (-. (p1 zenon_Vjd))
% 0.43/0.76  (zenon_Vgl != zenon_Vwi)
% 0.43/0.76  (zenon_Vik != zenon_Voc)
% 0.43/0.76  (zenon_Vsj != zenon_Voc)
% 0.43/0.76  (zenon_Vkj != zenon_Vcd)
% 0.43/0.76  (zenon_Vyk != zenon_Vra)
% 0.43/0.76  (zenon_Vch != zenon_Vaf)
% 0.43/0.76  (zenon_Vmk != zenon_Vwi)
% 0.43/0.76  (zenon_Vol != zenon_Vmb)
% 0.43/0.76  (zenon_Vwh != zenon_Vw)
% 0.43/0.76  (zenon_Vvi != zenon_Vgg)
% 0.43/0.76  (zenon_Vaj != zenon_Vka)
% 0.43/0.76  (zenon_Vyk != zenon_Vtb)
% 0.43/0.76  (zenon_Vuk != zenon_Vjd)
% 0.43/0.76  (p1 zenon_Vrh)
% 0.43/0.76  (zenon_Vmh != zenon_Vwe)
% 0.43/0.76  (zenon_Vmh != zenon_Vkg)
% 0.43/0.76  (zenon_Vfj != zenon_Vhi)
% 0.43/0.76  (zenon_Vqk != zenon_Vtb)
% 0.43/0.76  (zenon_Vaj != zenon_Vmb)
% 0.43/0.76  (zenon_Vcl != zenon_Vra)
% 0.43/0.76  (zenon_Vsj != zenon_Vac)
% 0.43/0.76  (zenon_Vkj != zenon_Vmf)
% 0.43/0.76  (zenon_Vcl != zenon_Vxh)
% 0.43/0.76  (zenon_Vkl != zenon_Vgj)
% 0.43/0.76  (zenon_Vrh != zenon_Vef)
% 0.43/0.76  (r1 zenon_Vhb zenon_Vlb)
% 0.43/0.76  (zenon_Vak != zenon_Vbj)
% 0.43/0.76  (zenon_Vch != zenon_Vci)
% 0.43/0.76  (r1 zenon_Vle zenon_Voe)
% 0.43/0.76  (zenon_Vkj != zenon_Vhc)
% 0.43/0.76  (zenon_Vvl != zenon_Vlj)
% 0.43/0.76  (-. (p2 zenon_Voj))
% 0.43/0.76  (zenon_Vtg != zenon_Vgj)
% 0.43/0.76  (zenon_Vbi != zenon_Vmi)
% 0.43/0.76  (r1 zenon_Vzg zenon_Vah)
% 0.43/0.76  (zenon_Vmk != zenon_Vih)
% 0.43/0.76  (zenon_Vwj != zenon_Vsh)
% 0.43/0.76  (zenon_Vmh != zenon_Vxh)
% 0.43/0.76  (zenon_Vtg != zenon_Vac)
% 0.43/0.76  (zenon_Vvl != zenon_Vri)
% 0.43/0.76  (zenon_Vqk != zenon_Vnh)
% 0.43/0.76  (zenon_Vmh != zenon_Vjd)
% 0.43/0.76  (zenon_Vgi != zenon_Vsh)
% 0.43/0.76  (zenon_Vek != zenon_Vwe)
% 0.43/0.76  (zenon_Vvl != zenon_Vya)
% 0.43/0.76  (zenon_Vsj != zenon_Vri)
% 0.43/0.76  (zenon_Vgl != zenon_Vog)
% 0.43/0.76  (r1 zenon_Vnf zenon_Vqf)
% 0.43/0.76  (zenon_Vak != zenon_Vhi)
% 0.43/0.76  (zenon_Vwj != zenon_Vfb)
% 0.43/0.76  (r1 zenon_Vpl zenon_Vsl)
% 0.43/0.76  (zenon_Vcl != zenon_Vif)
% 0.43/0.76  (r1 zenon_Vxi zenon_Vyi)
% 0.43/0.76  (zenon_Vsl != zenon_Vcg)
% 0.43/0.76  (zenon_Vmk != zenon_Vgj)
% 0.43/0.76  (zenon_Vyk != zenon_Vdh)
% 0.43/0.76  (zenon_Vhh != zenon_Vbj)
% 0.43/0.76  (zenon_Vaj != zenon_Vqf)
% 0.43/0.76  (zenon_Vfj != zenon_Vmi)
% 0.43/0.76  (zenon_Vik != zenon_Vci)
% 0.43/0.76  (zenon_Vcl != zenon_Vnh)
% 0.43/0.76  (zenon_Vwh != zenon_Vxh)
% 0.43/0.76  (zenon_Vkj != zenon_Vbj)
% 0.43/0.76  (zenon_Vsj != zenon_Vcg)
% 0.43/0.76  (zenon_Vqi != zenon_Vri)
% 0.43/0.76  (zenon_Vek != zenon_Vdh)
% 0.43/0.76  (p1 zenon_Vcl)
% 0.43/0.76  (zenon_Vgl != zenon_Vri)
% 0.43/0.76  (zenon_Vkj != zenon_Vuf)
% 0.43/0.76  (-. (p3 zenon_Vge))
% 0.43/0.76  (zenon_Vmh != zenon_Vtb)
% 0.43/0.76  (zenon_Vcl != zenon_Vuf)
% 0.43/0.76  (zenon_Vqk != zenon_Vgg)
% 0.43/0.76  (zenon_Vuk != zenon_Vbj)
% 0.43/0.76  (zenon_Vch != zenon_Vdh)
% 0.43/0.76  (zenon_Vsj != zenon_Vfb)
% 0.43/0.76  (zenon_Vuk != zenon_Vvc)
% 0.43/0.76  (zenon_Vch != zenon_Vrg)
% 0.43/0.76  (-. (p1 zenon_Vvc))
% 0.43/0.76  (zenon_Vkj != zenon_Vgg)
% 0.43/0.76  (r1 zenon_Vjf zenon_Vmf)
% 0.43/0.76  (zenon_Vbi != zenon_Vda)
% 0.43/0.76  (zenon_Vsl != zenon_Vuf)
% 0.43/0.76  (zenon_Vch != zenon_Vw)
% 0.43/0.76  (zenon_Vqk != zenon_Vef)
% 0.43/0.76  (r1 zenon_Vr zenon_Vv)
% 0.43/0.76  (-. (p1 zenon_Vcg))
% 0.43/0.76  (zenon_Vkl != zenon_Vse)
% 0.43/0.76  (-. (p1 zenon_Vac))
% 0.43/0.76  (zenon_Vqi != zenon_Vhi)
% 0.43/0.76  (zenon_Vbi != zenon_Vci)
% 0.43/0.76  (zenon_Vqi != zenon_Vse)
% 0.43/0.76  (zenon_Vfj != zenon_Vse)
% 0.43/0.76  (zenon_Vtg != zenon_Vnh)
% 0.43/0.76  (zenon_Vek != zenon_Vef)
% 0.43/0.76  (zenon_Vgl != zenon_Vih)
% 0.43/0.76  (zenon_Vvl != zenon_Vhi)
% 0.43/0.76  (zenon_Vkj != zenon_Vmb)
% 0.43/0.76  (zenon_Vch != zenon_Vwe)
% 0.43/0.76  (zenon_Vmk != zenon_Vaf)
% 0.43/0.76  (r1 zenon_Vrk zenon_Vuk)
% 0.43/0.76  (zenon_Vxg != zenon_Vwe)
% 0.43/0.76  (zenon_Vbi != zenon_Vmb)
% 0.43/0.76  (zenon_Vrh != zenon_Vka)
% 0.43/0.76  (zenon_Vkj != zenon_Vda)
% 0.43/0.76  (zenon_Vfj != zenon_Vtb)
% 0.43/0.76  (zenon_Vkj != zenon_Vw)
% 0.43/0.76  (zenon_Vol != zenon_Vwe)
% 0.43/0.76  (-. (p1 zenon_Vuf))
% 0.43/0.76  (zenon_Vfj != zenon_Vsh)
% 0.43/0.76  (-. (p1 zenon_Vhc))
% 0.43/0.76  (zenon_Vsl != zenon_Vhi)
% 0.43/0.76  (zenon_Vqk != zenon_Vac)
% 0.43/0.76  (zenon_Vxg != zenon_Vnh)
% 0.43/0.76  (zenon_Vli != zenon_Vse)
% 0.43/0.76  (zenon_Vfj != zenon_Vqf)
% 0.43/0.76  (zenon_Vfj != zenon_Vlj)
% 0.43/0.76  (zenon_Vgl != zenon_Vhc)
% 0.43/0.76  (zenon_Vch != zenon_Vkg)
% 0.43/0.76  (zenon_Vxg != zenon_Vri)
% 0.43/0.76  (zenon_Vwh != zenon_Vbj)
% 0.43/0.76  (zenon_Vkl != zenon_Vq)
% 0.43/0.76  (zenon_Vsj != zenon_Vqf)
% 0.43/0.76  (zenon_Vaj != zenon_Vhi)
% 0.43/0.76  (zenon_Vmh != zenon_Vka)
% 0.43/0.76  (zenon_Vqk != zenon_Vhc)
% 0.43/0.76  (zenon_Vak != zenon_Vmi)
% 0.43/0.76  (zenon_Vmh != zenon_Vri)
% 0.43/0.76  (-. (p2 zenon_Vzd))
% 0.43/0.76  (zenon_Vch != zenon_Vhi)
% 0.43/0.76  (zenon_Vxg != zenon_Vse)
% 0.43/0.76  (zenon_Vwj != zenon_Vgj)
% 0.43/0.76  (zenon_Vrh != zenon_Vhc)
% 0.43/0.76  (zenon_Vwh != zenon_Vac)
% 0.43/0.76  (zenon_Vrh != zenon_Vkg)
% 0.43/0.76  (zenon_Vak != zenon_Vif)
% 0.43/0.76  (-. (p1 zenon_Vqf))
% 0.43/0.76  (zenon_Vmh != zenon_Vqf)
% 0.43/0.76  (r1 zenon_Vae zenon_Vde)
% 0.43/0.76  (zenon_Vvl != zenon_Vuf)
% 0.43/0.76  (zenon_Vaj != zenon_Vdh)
% 0.43/0.76  (zenon_Vaj != zenon_Vci)
% 0.43/0.76  (zenon_Vmh != zenon_Vgg)
% 0.43/0.76  (zenon_Vaj != zenon_Vgg)
% 0.43/0.76  (zenon_Vsl != zenon_Vmb)
% 0.43/0.76  (r1 zenon_Vcj zenon_Vhj)
% 0.43/0.76  (zenon_Vhh != zenon_Voc)
% 0.43/0.76  (zenon_Vol != zenon_Vmi)
% 0.43/0.76  (zenon_Vik != zenon_Vuf)
% 0.43/0.76  (zenon_Vkl != zenon_Vkg)
% 0.43/0.76  (zenon_Vfj != zenon_Vog)
% 0.43/0.76  (zenon_Vwj != zenon_Vri)
% 0.43/0.76  (zenon_Vwj != zenon_Vnh)
% 0.43/0.76  (zenon_Vek != zenon_Vmb)
% 0.43/0.76  (zenon_Vhh != zenon_Vif)
% 0.43/0.76  (-. (p1 zenon_Vse))
% 0.43/0.76  (zenon_Vcl != zenon_Voc)
% 0.43/0.76  (zenon_Vak != zenon_Vnh)
% 0.43/0.76  (zenon_Vmk != zenon_Vmb)
% 0.43/0.76  (zenon_Vfj != zenon_Vac)
% 0.43/0.76  (zenon_Vrh != zenon_Vda)
% 0.43/0.76  (zenon_Vqk != zenon_Vif)
% 0.43/0.76  (zenon_Vvi != zenon_Vmb)
% 0.43/0.76  (zenon_Vqk != zenon_Vcg)
% 0.43/0.76  (zenon_Vbi != zenon_Vnh)
% 0.43/0.76  (zenon_Vaj != zenon_Vog)
% 0.43/0.76  (zenon_Vli != zenon_Vef)
% 0.43/0.76  (zenon_Vwj != zenon_Vra)
% 0.43/0.76  (zenon_Vtg != zenon_Vih)
% 0.43/0.76  (zenon_Vqi != zenon_Vif)
% 0.43/0.76  (zenon_Vwh != zenon_Vyf)
% 0.43/0.76  (r1 zenon_Vfa zenon_Vja)
% 0.43/0.76  (zenon_Vgl != zenon_Vxh)
% 0.43/0.76  (zenon_Vtg != zenon_Vef)
% 0.43/0.76  (zenon_Vyk != zenon_Vxh)
% 0.43/0.76  (zenon_Vwj != zenon_Vwi)
% 0.43/0.76  (zenon_Vhh != zenon_Vug)
% 0.43/0.76  (zenon_Vek != zenon_Vaf)
% 0.43/0.76  (zenon_Vik != zenon_Vog)
% 0.43/0.76  (zenon_Vik != zenon_Vse)
% 0.43/0.76  (zenon_Vwh != zenon_Vdh)
% 0.43/0.76  (zenon_Vmk != zenon_Vyf)
% 0.43/0.76  (p1 zenon_Vmk)
% 0.43/0.76  (zenon_Vaj != zenon_Vvc)
% 0.43/0.76  (zenon_Vkl != zenon_Vka)
% 0.43/0.76  (zenon_Vrh != zenon_Vtb)
% 0.43/0.76  (zenon_Vbi != zenon_Vya)
% 0.43/0.76  (zenon_Vch != zenon_Voc)
% 0.43/0.76  (zenon_Vli != zenon_Vwe)
% 0.43/0.76  (r1 zenon_Vee zenon_Vfe)
% 0.43/0.76  (zenon_Vsl != zenon_Vq)
% 0.43/0.76  (zenon_Vhh != zenon_Vmf)
% 0.43/0.76  (zenon_Vsl != zenon_Vac)
% 0.43/0.76  (zenon_Vkl != zenon_Vri)
% 0.43/0.76  (zenon_Vfe != zenon_Voj)
% 0.43/0.76  (zenon_Vsl != zenon_Vog)
% 0.43/0.76  (r1 zenon_Vxc zenon_Vbd)
% 0.43/0.76  (zenon_Vsl != zenon_Vif)
% 0.43/0.76  (zenon_Vak != zenon_Vmb)
% 0.43/0.76  (zenon_Vqi != zenon_Vaf)
% 0.43/0.76  (p1 zenon_Vsl)
% 0.43/0.76  (zenon_Vfj != zenon_Vif)
% 0.43/0.76  (r1 zenon_Veh zenon_Vfh)
% 0.43/0.76  (zenon_Vsl != zenon_Vyg)
% 0.43/0.76  (zenon_Vvi != zenon_Vcg)
% 0.43/0.76  (zenon_Vcl != zenon_Vbj)
% 0.43/0.76  (zenon_Vtg != zenon_Vsh)
% 0.43/0.76  (zenon_Vli != zenon_Vcg)
% 0.43/0.76  (zenon_Vkj != zenon_Vdh)
% 0.43/0.76  (zenon_Vhh != zenon_Vxh)
% 0.43/0.76  (zenon_Vwh != zenon_Voc)
% 0.43/0.76  (zenon_Vrh != zenon_Vuf)
% 0.43/0.76  (zenon_Vxg != zenon_Voc)
% 0.43/0.76  (zenon_Vwh != zenon_Vse)
% 0.43/0.76  (zenon_Vmk != zenon_Vci)
% 0.43/0.76  (zenon_Vkl != zenon_Vmf)
% 0.43/0.76  (zenon_Vmh != zenon_Vmf)
% 0.43/0.76  (p1 zenon_Vqk)
% 0.43/0.76  (zenon_Vkl != zenon_Vsh)
% 0.43/0.76  (zenon_Vkl != zenon_Vlj)
% 0.43/0.76  (zenon_Vfj != zenon_Vq)
% 0.43/0.76  (zenon_Vgl != zenon_Vra)
% 0.43/0.76  (zenon_Vbi != zenon_Vka)
% 0.43/0.76  (zenon_Vyk != zenon_Vkg)
% 0.43/0.76  (zenon_Vmh != zenon_Vnh)
% 0.43/0.76  (p1 zenon_Vik)
% 0.43/0.76  (zenon_Vwh != zenon_Vjd)
% 0.43/0.76  (zenon_Vmh != zenon_Vyf)
% 0.43/0.76  (zenon_Vsj != zenon_Vsh)
% 0.43/0.76  (zenon_Vyk != zenon_Vac)
% 0.43/0.76  (zenon_Vmh != zenon_Vcg)
% 0.43/0.76  (zenon_Vik != zenon_Vnh)
% 0.43/0.76  (zenon_Vcl != zenon_Vvc)
% 0.43/0.76  (r1 zenon_Vnj zenon_Voj)
% 0.43/0.76  (zenon_Vak != zenon_Vgj)
% 0.43/0.76  (r1 zenon_Vfk zenon_Vik)
% 0.43/0.76  (zenon_Vrh != zenon_Vwi)
% 0.43/0.76  (zenon_Vtg != zenon_Voc)
% 0.43/0.76  (zenon_Vkl != zenon_Vih)
% 0.43/0.76  (zenon_Vhh != zenon_Vvc)
% 0.43/0.76  (zenon_Vtg != zenon_Vaf)
% 0.43/0.76  (zenon_Vyk != zenon_Vef)
% 0.43/0.76  (zenon_Vmk != zenon_Vif)
% 0.43/0.76  (zenon_Vak != zenon_Vuf)
% 0.43/0.76  (zenon_Vcl != zenon_Vya)
% 0.43/0.76  (zenon_Vmk != zenon_Vog)
% 0.43/0.76  (zenon_Vtg != zenon_Vtb)
% 0.43/0.76  (zenon_Vwj != zenon_Vyg)
% 0.43/0.76  (zenon_Vch != zenon_Vlj)
% 0.43/0.76  (r1 zenon_Vrf zenon_Vuf)
% 0.43/0.76  (zenon_Vkj != zenon_Vug)
% 0.43/0.76  (zenon_Vli != zenon_Vqf)
% 0.43/0.76  (zenon_Vaj != zenon_Vmi)
% 0.43/0.76  (zenon_Vhh != zenon_Vsh)
% 0.43/0.76  (zenon_Vyk != zenon_Vci)
% 0.43/0.76  (zenon_Vgi != zenon_Vef)
% 0.43/0.76  (zenon_Vqk != zenon_Vri)
% 0.43/0.76  (zenon_Vgl != zenon_Vw)
% 0.43/0.76  (zenon_Vkj != zenon_Vlj)
% 0.43/0.76  (zenon_Vwh != zenon_Vka)
% 0.43/0.76  (zenon_Vgi != zenon_Vif)
% 0.43/0.76  (zenon_Vuk != zenon_Vse)
% 0.43/0.76  (zenon_Vqi != zenon_Vac)
% 0.43/0.76  (zenon_Vtg != zenon_Vcd)
% 0.43/0.76  (zenon_Vhh != zenon_Vrg)
% 0.43/0.76  (zenon_Vli != zenon_Vya)
% 0.43/0.76  (zenon_Vfj != zenon_Vnh)
% 0.43/0.76  (r1 zenon_Vei zenon_Vhi)
% 0.43/0.76  (zenon_Vvi != zenon_Vda)
% 0.43/0.76  (zenon_Vrh != zenon_Vlj)
% 0.43/0.76  (zenon_Vsj != zenon_Vuf)
% 0.43/0.76  (zenon_Vik != zenon_Vgg)
% 0.43/0.76  (p1 zenon_Vak)
% 0.43/0.76  (-. (p1 zenon_Vmf))
% 0.43/0.76  (zenon_Vwj != zenon_Vhi)
% 0.43/0.76  (zenon_Vwh != zenon_Vgj)
% 0.43/0.76  (-. (p1 zenon_Vrg))
% 0.43/0.76  (zenon_Vvl != zenon_Vwi)
% 0.43/0.76  (zenon_Vfj != zenon_Vcd)
% 0.43/0.76  (p2 zenon_Vmd)
% 0.43/0.76  (zenon_Vkj != zenon_Vcg)
% 0.43/0.76  (p1 zenon_Vkj)
% 0.43/0.76  (zenon_Vyk != zenon_Vse)
% 0.43/0.76  (zenon_Vhh != zenon_Vyf)
% 0.43/0.76  (zenon_Vsl != zenon_Vwe)
% 0.43/0.76  (zenon_Vrh != zenon_Vqf)
% 0.43/0.76  (zenon_Vfj != zenon_Vaf)
% 0.43/0.76  (r1 zenon_Vzh zenon_Vai)
% 0.43/0.76  (zenon_Vhh != zenon_Vse)
% 0.43/0.76  (zenon_Vcl != zenon_Vse)
% 0.43/0.76  (zenon_Vqk != zenon_Vw)
% 0.43/0.76  (zenon_Vwh != zenon_Vcg)
% 0.43/0.76  (zenon_Vak != zenon_Vda)
% 0.43/0.76  (zenon_Vmk != zenon_Vra)
% 0.43/0.76  (zenon_Vvi != zenon_Vqf)
% 0.43/0.76  (zenon_Vfj != zenon_Vuf)
% 0.43/0.76  (zenon_Vuk != zenon_Vq)
% 0.43/0.76  (zenon_Vmh != zenon_Vih)
% 0.43/0.76  (zenon_Vqi != zenon_Vya)
% 0.43/0.76  (zenon_Vxg != zenon_Vac)
% 0.43/0.76  (zenon_Vrh != zenon_Vcg)
% 0.43/0.76  (zenon_Vgl != zenon_Vfb)
% 0.43/0.76  (zenon_Vbi != zenon_Vyf)
% 0.43/0.76  (zenon_Vgl != zenon_Vmf)
% 0.43/0.76  (zenon_Vqi != zenon_Vq)
% 0.43/0.76  (zenon_Vwj != zenon_Vac)
% 0.43/0.76  (zenon_Vaj != zenon_Vwe)
% 0.43/0.76  (zenon_Vqi != zenon_Vtb)
% 0.43/0.76  (r1 zenon_Vhj zenon_Vij)
% 0.43/0.76  (zenon_Vbi != zenon_Vvc)
% 0.43/0.76  (zenon_Vli != zenon_Vif)
% 0.43/0.76  (zenon_Vkj != zenon_Vgj)
% 0.43/0.76  (zenon_Vhh != zenon_Vda)
% 0.43/0.76  (zenon_Vuk != zenon_Vmi)
% 0.43/0.76  (zenon_Vcl != zenon_Vsh)
% 0.43/0.76  (zenon_Vol != zenon_Vbj)
% 0.43/0.76  (zenon_Vsl != zenon_Vka)
% 0.43/0.76  (zenon_Vsl != zenon_Vmi)
% 0.43/0.76  (zenon_Vtg != zenon_Vuf)
% 0.43/0.76  (zenon_Vsj != zenon_Vlj)
% 0.43/0.76  (zenon_Vwh != zenon_Vhc)
% 0.43/0.76  (-. (p2 zenon_Vke))
% 0.43/0.76  (zenon_Vuk != zenon_Vmf)
% 0.43/0.76  (zenon_Vgl != zenon_Vrg)
% 0.43/0.76  (zenon_Vtg != zenon_Vq)
% 0.43/0.76  (zenon_Vmh != zenon_Vfb)
% 0.43/0.76  (zenon_Vmh != zenon_Vlj)
% 0.43/0.76  (zenon_Vcl != zenon_Vhc)
% 0.43/0.76  (zenon_Vik != zenon_Vwe)
% 0.43/0.76  (zenon_Vqk != zenon_Vlj)
% 0.43/0.76  (zenon_Vol != zenon_Vse)
% 0.43/0.76  (zenon_Vwh != zenon_Vmb)
% 0.43/0.76  (zenon_Vwj != zenon_Vmb)
% 0.43/0.76  (r1 zenon_Vdl zenon_Vgl)
% 0.43/0.76  (-. (p1 zenon_Vih))
% 0.43/0.76  (zenon_Vtg != zenon_Vra)
% 0.43/0.76  (zenon_Vmh != zenon_Vac)
% 0.43/0.76  (-. (p1 zenon_Voe))
% 0.43/0.76  (zenon_Vqi != zenon_Voc)
% 0.43/0.76  (zenon_Vsl != zenon_Vaf)
% 0.43/0.76  (zenon_Vrh != zenon_Vmb)
% 0.43/0.76  (zenon_Vak != zenon_Voe)
% 0.43/0.76  (zenon_Vmh != zenon_Vef)
% 0.43/0.76  (r1 zenon_Vfe zenon_Vge)
% 0.43/0.76  (zenon_Vwh != zenon_Vgg)
% 0.43/0.76  (p1 zenon_Vbi)
% 0.43/0.76  (zenon_Vyk != zenon_Vyg)
% 0.43/0.76  (zenon_Vbi != zenon_Voc)
% 0.43/0.76  (p1 zenon_Vsj)
% 0.43/0.76  (zenon_Vek != zenon_Vxh)
% 0.43/0.76  (zenon_Vuk != zenon_Vug)
% 0.43/0.76  (zenon_Vak != zenon_Vri)
% 0.43/0.76  (zenon_Vbi != zenon_Vgj)
% 0.43/0.76  (-. (p1 zenon_Vwe))
% 0.43/0.76  (zenon_Vvi != zenon_Vkg)
% 0.43/0.76  (zenon_Vgi != zenon_Vgj)
% 0.43/0.76  (zenon_Vgi != zenon_Vfb)
% 0.43/0.76  (zenon_Vxg != zenon_Vkg)
% 0.43/0.76  (zenon_Vfj != zenon_Vyf)
% 0.43/0.76  (zenon_Vmk != zenon_Vhc)
% 0.43/0.76  (zenon_Vik != zenon_Vqf)
% 0.43/0.76  (zenon_Vkj != zenon_Vjd)
% 0.43/0.76  (zenon_Vfj != zenon_Vyg)
% 0.43/0.76  (zenon_Vvi != zenon_Vuf)
% 0.43/0.76  (zenon_Vvl != zenon_Vcd)
% 0.43/0.76  (zenon_Vaj != zenon_Vlj)
% 0.43/0.76  (zenon_Vli != zenon_Vw)
% 0.43/0.76  (zenon_Vgi != zenon_Vcd)
% 0.43/0.76  (r1 zenon_Vzk zenon_Vcl)
% 0.43/0.76  (-. (p1 zenon_Vog))
% 0.43/0.76  (zenon_Vak != zenon_Vra)
% 0.43/0.76  (zenon_Vvl != zenon_Vyf)
% 0.43/0.76  (zenon_Vek != zenon_Vsh)
% 0.43/0.76  (zenon_Vch != zenon_Vyf)
% 0.43/0.76  (zenon_Vqk != zenon_Vog)
% 0.43/0.76  (zenon_Vkj != zenon_Vtb)
% 0.43/0.76  (zenon_Vuk != zenon_Vkg)
% 0.43/0.76  (zenon_Vvi != zenon_Vri)
% 0.43/0.76  (zenon_Vfj != zenon_Vrg)
% 0.43/0.76  (zenon_Vuk != zenon_Vrg)
% 0.43/0.76  (zenon_Vch != zenon_Vmf)
% 0.43/0.76  (zenon_Vwh != zenon_Vuf)
% 0.43/0.76  (zenon_Vek != zenon_Vog)
% 0.43/0.76  (zenon_Vak != zenon_Voc)
% 0.43/0.76  (zenon_Vmh != zenon_Vwi)
% 0.43/0.76  (zenon_Vgi != zenon_Vjd)
% 0.43/0.76  (zenon_Vwj != zenon_Voe)
% 0.43/0.76  (zenon_Vfj != zenon_Vri)
% 0.43/0.76  (zenon_Vkj != zenon_Voc)
% 0.43/0.76  (zenon_Vgi != zenon_Vuf)
% 0.43/0.76  (zenon_Vuk != zenon_Vtb)
% 0.43/0.76  (zenon_Vch != zenon_Vgj)
% 0.43/0.76  (-. (p1 zenon_Vmb))
% 0.43/0.76  (p1 zenon_Vqi)
% 0.43/0.76  (zenon_Vmk != zenon_Vcg)
% 0.43/0.76  (zenon_Vli != zenon_Vuf)
% 0.43/0.76  (zenon_Vik != zenon_Vra)
% 0.43/0.76  (zenon_Vvi != zenon_Vhi)
% 0.43/0.76  (zenon_Vli != zenon_Vaf)
% 0.43/0.76  (p1 zenon_Vwj)
% 0.43/0.76  (zenon_Vkl != zenon_Vwe)
% 0.43/0.76  (zenon_Vwj != zenon_Vjd)
% 0.43/0.76  (zenon_Vli != zenon_Vwi)
% 0.43/0.76  (zenon_Vsj != zenon_Vnh)
% 0.43/0.76  (r1 zenon_Vah zenon_Vdh)
% 0.43/0.76  (zenon_Vwh != zenon_Vwe)
% 0.43/0.76  (r1 zenon_Vuh zenon_Vxh)
% 0.43/0.76  (zenon_Vwj != zenon_Vya)
% 0.43/0.76  (zenon_Vcl != zenon_Vac)
% 0.43/0.76  (zenon_Vwh != zenon_Vnh)
% 0.43/0.76  (zenon_Vek != zenon_Vda)
% 0.43/0.76  (zenon_Vch != zenon_Vhc)
% 0.43/0.76  (zenon_Vqi != zenon_Vog)
% 0.43/0.76  (zenon_Vtg != zenon_Vrg)
% 0.43/0.76  (zenon_Vcl != zenon_Vcg)
% 0.43/0.77  (p1 zenon_Vkl)
% 0.43/0.77  (zenon_Vwj != zenon_Vw)
% 0.43/0.77  (zenon_Vyk != zenon_Vqf)
% 0.43/0.77  (zenon_Vhh != zenon_Vdh)
% 0.43/0.77  (zenon_Vgi != zenon_Vcg)
% 0.43/0.77  (zenon_Vmh != zenon_Vog)
% 0.43/0.77  (zenon_Vqi != zenon_Vkg)
% 0.43/0.77  (zenon_Vtg != zenon_Vug)
% 0.43/0.77  (zenon_Vcl != zenon_Vmb)
% 0.43/0.77  (zenon_Vvl != zenon_Vgg)
% 0.43/0.77  (r1 zenon_Vij zenon_Vlj)
% 0.43/0.77  (zenon_Vbi != zenon_Vwe)
% 0.43/0.77  (zenon_Vgl != zenon_Vmb)
% 0.43/0.77  (zenon_Vkl != zenon_Vda)
% 0.43/0.77  (zenon_Vmk != zenon_Voc)
% 0.43/0.77  (zenon_Vtg != zenon_Vwe)
% 0.43/0.77  (zenon_Vek != zenon_Vci)
% 0.43/0.77  (zenon_Vik != zenon_Vkg)
% 0.43/0.77  (zenon_Vyk != zenon_Vih)
% 0.43/0.77  (zenon_Vuk != zenon_Vcd)
% 0.43/0.77  (zenon_Vuk != zenon_Vif)
% 0.43/0.77  (-. (p1 zenon_Vra))
% 0.43/0.77  (zenon_Vaj != zenon_Vyg)
% 0.43/0.77  (zenon_Vaj != zenon_Voc)
% 0.43/0.77  (zenon_Vtg != zenon_Vxh)
% 0.43/0.77  (zenon_Vol != zenon_Vrg)
% 0.43/0.77  (zenon_Vch != zenon_Vac)
% 0.43/0.77  (zenon_Vaj != zenon_Vef)
% 0.43/0.77  (-. (p2 zenon_Vtd))
% 0.43/0.77  (zenon_Vuk != zenon_Vda)
% 0.43/0.77  (zenon_Vsl != zenon_Vjd)
% 0.43/0.77  (zenon_Vik != zenon_Voe)
% 0.43/0.77  (zenon_Vxg != zenon_Vmf)
% 0.43/0.77  (zenon_Vxg != zenon_Vxh)
% 0.43/0.77  (zenon_Vhh != zenon_Vac)
% 0.43/0.77  (zenon_Vgl != zenon_Vse)
% 0.43/0.77  (zenon_Vbi != zenon_Vwi)
% 0.43/0.77  (zenon_Vkl != zenon_Vya)
% 0.43/0.77  (zenon_Vwj != zenon_Vq)
% 0.43/0.77  (zenon_Vsj != zenon_Vef)
% 0.43/0.77  (zenon_Vrh != zenon_Vgg)
% 0.43/0.77  (zenon_Vgi != zenon_Vxh)
% 0.43/0.77  (zenon_Vyk != zenon_Vw)
% 0.43/0.77  (zenon_Vsj != zenon_Vda)
% 0.43/0.77  (zenon_Vtg != zenon_Vyg)
% 0.43/0.77  (zenon_Vek != zenon_Vcd)
% 0.43/0.77  (zenon_Vmk != zenon_Vbj)
% 0.43/0.77  (zenon_Vhh != zenon_Vya)
% 0.43/0.77  (zenon_Vgi != zenon_Vwi)
% 0.43/0.77  (zenon_Vsj != zenon_Vxh)
% 0.43/0.77  (zenon_Vsl != zenon_Voc)
% 0.43/0.77  (zenon_Vtg != zenon_Vyf)
% 0.43/0.77  (zenon_Vyk != zenon_Vya)
% 0.43/0.77  (zenon_Vrh != zenon_Vyg)
% 0.43/0.77  (zenon_Vbi != zenon_Vcd)
% 0.43/0.77  (zenon_Vli != zenon_Vog)
% 0.43/0.77  (zenon_Vgi != zenon_Vaf)
% 0.43/0.77  (zenon_Vwj != zenon_Vyf)
% 0.43/0.77  (zenon_Vak != zenon_Vya)
% 0.43/0.77  (zenon_Vgl != zenon_Vgg)
% 0.43/0.77  (zenon_Vbi != zenon_Vdh)
% 0.43/0.77  (r1 zenon_Vji zenon_Vmi)
% 0.43/0.77  (zenon_Vxg != zenon_Vef)
% 0.43/0.77  (zenon_Vgl != zenon_Vka)
% 0.43/0.77  (zenon_Vtg != zenon_Vda)
% 0.43/0.77  (zenon_Vsl != zenon_Vri)
% 0.43/0.77  (zenon_Vwj != zenon_Vvc)
% 0.43/0.77  (zenon_Vhh != zenon_Vuf)
% 0.43/0.77  (zenon_Vgl != zenon_Vhi)
% 0.43/0.77  (zenon_Vch != zenon_Vug)
% 0.43/0.77  (zenon_Vik != zenon_Vac)
% 0.43/0.77  (zenon_Vkj != zenon_Vfb)
% 0.43/0.77  (zenon_Vqi != zenon_Vuf)
% 0.43/0.77  (zenon_Vgl != zenon_Vcg)
% 0.43/0.77  (zenon_Vvl != zenon_Vsh)
% 0.43/0.77  (zenon_Vvl != zenon_Vda)
% 0.43/0.77  (zenon_Vwh != zenon_Vcd)
% 0.43/0.77  (r1 zenon_Vuh zenon_Vvh)
% 0.43/0.77  (zenon_Vhh != zenon_Vih)
% 0.43/0.77  (zenon_Vvl != zenon_Vci)
% 0.43/0.77  (zenon_Vwh != zenon_Vlj)
% 0.43/0.77  (zenon_Vfe != zenon_Vke)
% 0.43/0.77  (zenon_Vwh != zenon_Vwi)
% 0.43/0.77  (zenon_Vxg != zenon_Vmb)
% 0.43/0.77  (-. (p1 zenon_Vhi))
% 0.43/0.77  (zenon_Vuk != zenon_Vef)
% 0.43/0.77  (zenon_Vrh != zenon_Vra)
% 0.43/0.77  (zenon_Vtg != zenon_Vqf)
% 0.43/0.77  (zenon_Vkj != zenon_Vci)
% 0.43/0.77  (zenon_Vik != zenon_Vdh)
% 0.43/0.77  (zenon_Vsj != zenon_Vwe)
% 0.43/0.77  (r1 zenon_Vvk zenon_Vyk)
% 0.43/0.77  (zenon_Vqi != zenon_Vhc)
% 0.43/0.77  (zenon_Vwh != zenon_Vyg)
% 0.43/0.77  (zenon_Vqk != zenon_Vcd)
% 0.43/0.77  (zenon_Vkj != zenon_Vhi)
% 0.43/0.77  (zenon_Vak != zenon_Vlj)
% 0.43/0.77  (zenon_Vgl != zenon_Voc)
% 0.43/0.77  (zenon_Vyk != zenon_Vmi)
% 0.43/0.77  (zenon_Vhh != zenon_Vef)
% 0.43/0.77  (zenon_Vsl != zenon_Vdh)
% 0.43/0.77  (zenon_Vol != zenon_Vuf)
% 0.43/0.77  (zenon_Vkj != zenon_Vyg)
% 0.43/0.77  (zenon_Vqk != zenon_Vvc)
% 0.43/0.77  (r1 zenon_Vbf zenon_Vef)
% 0.43/0.77  (zenon_Vbi != zenon_Vtb)
% 0.43/0.77  (zenon_Vkj != zenon_Vyf)
% 0.43/0.77  (r1 zenon_Vni zenon_Vsi)
% 0.43/0.77  (zenon_Vek != zenon_Vra)
% 0.43/0.77  (zenon_Vvl != zenon_Vw)
% 0.43/0.77  (zenon_Vbi != zenon_Vbj)
% 0.43/0.77  (zenon_Vaj != zenon_Vw)
% 0.43/0.77  (zenon_Vfj != zenon_Vci)
% 0.43/0.77  (zenon_Vkl != zenon_Vhc)
% 0.43/0.77  (zenon_Vkl != zenon_Voe)
% 0.43/0.77  (zenon_Vwh != zenon_Vvc)
% 0.43/0.77  (zenon_Vek != zenon_Vtb)
% 0.43/0.77  (zenon_Vcl != zenon_Vgj)
% 0.43/0.77  (zenon_Vbi != zenon_Vqf)
% 0.43/0.77  (zenon_Vqk != zenon_Vdh)
% 0.43/0.77  (zenon_Vfj != zenon_Vra)
% 0.43/0.77  (zenon_Vyk != zenon_Vwi)
% 0.43/0.77  (zenon_Vsj != zenon_Vhc)
% 0.43/0.77  (zenon_Vli != zenon_Vfb)
% 0.43/0.77  (zenon_Vvi != zenon_Vyg)
% 0.43/0.77  (r1 zenon_Vsi zenon_Vxi)
% 0.43/0.77  (zenon_Vxg != zenon_Vmi)
% 0.43/0.77  (zenon_Vaj != zenon_Vya)
% 0.43/0.77  (r1 Tau_1 zenon_Vug)
% 0.43/0.77  (zenon_Vqk != zenon_Vih)
% 0.43/0.77  (zenon_Vtg != zenon_Vya)
% 0.43/0.77  (zenon_Vbi != zenon_Vih)
% 0.43/0.77  (zenon_Vvi != zenon_Vug)
% 0.43/0.77  (zenon_Vrh != zenon_Vcd)
% 0.43/0.77  (zenon_Vfj != zenon_Voc)
% 0.43/0.77  (zenon_Vwj != zenon_Vaf)
% 0.43/0.77  (zenon_Vol != zenon_Vdh)
% 0.43/0.77  (zenon_Vqk != zenon_Vug)
% 0.43/0.77  (zenon_Vik != zenon_Vw)
% 0.43/0.77  (zenon_Vbi != zenon_Vfb)
% 0.43/0.77  (zenon_Vcl != zenon_Vrg)
% 0.43/0.77  (zenon_Vak != zenon_Vyg)
% 0.43/0.77  (zenon_Vaj != zenon_Vwi)
% 0.43/0.77  (zenon_Vrh != zenon_Vbj)
% 0.43/0.77  (zenon_Vak != zenon_Vka)
% 0.43/0.77  (zenon_Vaj != zenon_Vra)
% 0.43/0.77  (zenon_Vkl != zenon_Vwi)
% 0.43/0.77  (zenon_Vmd != zenon_Vtd)
% 0.43/0.77  (zenon_Vuk != zenon_Vw)
% 0.43/0.77  (zenon_Vkl != zenon_Vug)
% 0.43/0.77  (zenon_Vch != zenon_Vya)
% 0.43/0.77  (zenon_Vmk != zenon_Vmf)
% 0.43/0.77  (zenon_Vek != zenon_Vka)
% 0.43/0.77  (zenon_Vek != zenon_Vvc)
% 0.43/0.77  (zenon_Vkl != zenon_Vif)
% 0.43/0.77  (zenon_Vbi != zenon_Vlj)
% 0.43/0.77  (r1 zenon_Vei zenon_Vfi)
% 0.43/0.77  (zenon_Vqk != zenon_Vgj)
% 0.43/0.77  (zenon_Vmk != zenon_Vya)
% 0.43/0.77  (zenon_Vaj != zenon_Vyf)
% 0.43/0.77  (r1 zenon_Vnk zenon_Vqk)
% 0.43/0.77  (zenon_Vbi != zenon_Vcg)
% 0.43/0.77  (zenon_Vwh != zenon_Vkg)
% 0.43/0.77  (zenon_Vek != zenon_Vqf)
% 0.43/0.77  (zenon_Vhh != zenon_Vgg)
% 0.43/0.77  (zenon_Vtg != zenon_Vbj)
% 0.43/0.77  (zenon_Vek != zenon_Vnh)
% 0.43/0.77  (zenon_Vgi != zenon_Vug)
% 0.43/0.77  (zenon_Vhh != zenon_Vqf)
% 0.43/0.77  (zenon_Vxg != zenon_Vyf)
% 0.43/0.77  (r1 zenon_Vlg zenon_Vog)
% 0.43/0.77  (zenon_Vhh != zenon_Vmb)
% 0.43/0.77  (p1 zenon_Vyk)
% 0.43/0.77  (zenon_Vek != zenon_Vya)
% 0.43/0.77  (zenon_Vol != zenon_Vjd)
% 0.43/0.77  (zenon_Vgi != zenon_Vka)
% 0.43/0.77  (zenon_Vqi != zenon_Vda)
% 0.43/0.77  (zenon_Vaj != zenon_Vtb)
% 0.43/0.77  (zenon_Vrh != zenon_Vhi)
% 0.43/0.77  (zenon_Vvi != zenon_Vw)
% 0.43/0.77  (zenon_Vbi != zenon_Vw)
% 0.43/0.77  (zenon_Vbi != zenon_Vjd)
% 0.43/0.77  (zenon_Vmh != zenon_Vsh)
% 0.43/0.77  (zenon_Vtg != zenon_Vvc)
% 0.43/0.77  (zenon_Vmd != zenon_Vke)
% 0.43/0.77  (zenon_Vek != zenon_Vuf)
% 0.43/0.77  (zenon_Vvi != zenon_Vdh)
% 0.43/0.77  (zenon_Vol != zenon_Vqf)
% 0.43/0.77  (zenon_Vxg != zenon_Vcg)
% 0.43/0.77  (zenon_Vaj != zenon_Vac)
% 0.43/0.77  (zenon_Vxg != zenon_Vq)
% 0.43/0.77  (zenon_Vik != zenon_Vhc)
% 0.43/0.77  (zenon_Vsl != zenon_Vqf)
% 0.43/0.77  (zenon_Vgi != zenon_Vnh)
% 0.43/0.77  (p2 zenon_Vfe)
% 0.43/0.77  (zenon_Vvl != zenon_Vqf)
% 0.43/0.77  (zenon_Vgi != zenon_Vdh)
% 0.43/0.77  (zenon_Vvl != zenon_Vwe)
% 0.43/0.77  (r1 zenon_Vvf zenon_Vyf)
% 0.43/0.77  (zenon_Vuk != zenon_Vwi)
% 0.43/0.77  (zenon_Vgl != zenon_Vmi)
% 0.43/0.77  (zenon_Vmd != zenon_Voj)
% 0.43/0.77  (r1 zenon_Vti zenon_Vwi)
% 0.43/0.77  (p1 zenon_Vuk)
% 0.43/0.77  (zenon_Vkl != zenon_Vvc)
% 0.43/0.77  (zenon_Vbi != zenon_Vmf)
% 0.43/0.77  (zenon_Vsl != zenon_Vda)
% 0.43/0.77  (zenon_Vbi != zenon_Vra)
% 0.43/0.77  (zenon_Vak != zenon_Vdh)
% 0.43/0.77  (zenon_Vik != zenon_Vih)
% 0.43/0.77  (zenon_Vcl != zenon_Vcd)
% 0.43/0.77  (-. (p1 zenon_Vci))
% 0.43/0.77  (zenon_Vsj != zenon_Voe)
% 0.43/0.77  (zenon_Vyk != zenon_Vcg)
% 0.43/0.77  (r1 zenon_Vta zenon_Vxa)
% 0.43/0.77  (zenon_Vsj != zenon_Vra)
% 0.43/0.77  (zenon_Vfj != zenon_Vka)
% 0.43/0.77  (zenon_Vol != zenon_Vfb)
% 0.43/0.77  (zenon_Vqk != zenon_Vci)
% 0.43/0.77  (zenon_Vmh != zenon_Vw)
% 0.43/0.77  (zenon_Vsj != zenon_Vrg)
% 0.43/0.77  (r1 zenon_Vjh zenon_Voh)
% 0.43/0.77  (zenon_Vvi != zenon_Vwe)
% 0.43/0.77  (r1 zenon_Vjc zenon_Vnc)
% 0.43/0.77  *)
% 0.43/0.77  (* NO-PROOF *)
% 0.43/0.77  % SZS status GaveUp
% 0.43/0.77  Number of rewrites on terms: 0
% 0.43/0.77  Number of rewrites on props: 0
% 0.43/0.77  nodes searched: 1940
% 0.43/0.77  max branch formulas: 2137
% 0.43/0.77  proof nodes created: 0
% 0.43/0.77  formulas created: 10687
% 0.43/0.77  
%------------------------------------------------------------------------------