↑ Up

ZenonModulo---0.5.0.UNK-Non.f

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

% Computer : n007.cluster.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory   : 8046.5625MB
% OS       : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit  : 300s
% DateTime : Mon Sep  7 01:34:23 PM UTC 2026

% Result   : Unknown 0.32s 0.61s
% Output   : None 
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : LCL670+1.015 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03  % Command  : run_zenon_modulo %d %s
% 0.07/0.34  % Computer : n007.cluster.edu
% 0.07/0.34  % Model    : x86_64 x86_64
% 0.07/0.34  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.34  % Memory   : 8046.5625MB
% 0.07/0.34  % OS       : Linux 6.8.0-71-generic
% 0.07/0.34  % CPULimit : 300
% 0.07/0.34  % WCLimit  : 300
% 0.07/0.34  % DateTime : Fri Sep  4 18:03:54 UTC 2026
% 0.07/0.34  % CPUTime  : 
% 0.32/0.61  Zenon error: exhausted search space without finding a proof
% 0.32/0.61  (* Current branch:
% 0.32/0.61  (zenon_Vwh != zenon_Vrd)
% 0.32/0.61  (r1 zenon_Vtd zenon_Vwd)
% 0.32/0.61  (zenon_Vug != zenon_Vhd)
% 0.32/0.61  (zenon_Vgd != zenon_Vgc)
% 0.32/0.61  (zenon_Vof != zenon_Vcc)
% 0.32/0.61  (zenon_Vke != zenon_Vmb)
% 0.32/0.61  (zenon_Vqd != zenon_Vsc)
% 0.32/0.61  (zenon_Vfe != zenon_Veb)
% 0.32/0.61  (r1 zenon_Vjg zenon_Vmg)
% 0.32/0.61  (zenon_Veg != zenon_Vbe)
% 0.32/0.61  (zenon_Vug != zenon_Vmd)
% 0.32/0.61  (p1 zenon_Vgh)
% 0.32/0.61  (zenon_Vkh != zenon_Vqe)
% 0.32/0.61  (r1 zenon_Vyd zenon_Vzd)
% 0.32/0.61  (zenon_Vld != zenon_Voc)
% 0.32/0.61  (zenon_Vgh != zenon_Vwa)
% 0.32/0.61  (zenon_Vug != zenon_Voc)
% 0.32/0.61  (p1 zenon_Vpe)
% 0.32/0.61  (zenon_Vxc != zenon_Vff)
% 0.32/0.61  (zenon_Vbd != zenon_Vsa)
% 0.32/0.61  (zenon_Vmg != zenon_Vpf)
% 0.32/0.61  (zenon_Vqd != zenon_Vkc)
% 0.32/0.61  (zenon_Vof != zenon_Vsa)
% 0.32/0.61  (r1 zenon_Vrf zenon_Vsf)
% 0.32/0.61  (zenon_Vef != zenon_Vcc)
% 0.32/0.61  (-. (p1 zenon_Vyc))
% 0.32/0.61  (zenon_Vue != zenon_Vyb)
% 0.32/0.61  (zenon_Vvd != zenon_Vqe)
% 0.32/0.61  (zenon_Vyg != zenon_Vqb)
% 0.32/0.61  (zenon_Vig != zenon_Vqe)
% 0.32/0.61  (zenon_Vfe != zenon_Vsa)
% 0.32/0.61  (zenon_Voh != zenon_Vle)
% 0.32/0.61  (zenon_Vwh != zenon_Vib)
% 0.32/0.61  (p1 zenon_Vkh)
% 0.32/0.61  (zenon_Vyg != zenon_Vff)
% 0.32/0.61  (zenon_Vmg != zenon_Vqb)
% 0.32/0.61  (zenon_Vke != zenon_Veb)
% 0.32/0.61  (zenon_Vpe != zenon_Vkf)
% 0.32/0.61  (zenon_Vyg != zenon_Vpf)
% 0.32/0.61  (zenon_Vch != zenon_Vhd)
% 0.32/0.61  (zenon_Vgd != zenon_Vsc)
% 0.32/0.61  (zenon_Vqd != zenon_Vqb)
% 0.32/0.61  (zenon_Vxc != zenon_Voc)
% 0.32/0.61  (zenon_Vig != zenon_Vvc)
% 0.32/0.61  (zenon_Vjf != zenon_Vle)
% 0.32/0.61  (zenon_Veg != zenon_Vqb)
% 0.32/0.61  (zenon_Vwf != zenon_Vib)
% 0.32/0.61  (zenon_Vug != zenon_Vqb)
% 0.32/0.61  (zenon_Vvd != zenon_Vmb)
% 0.32/0.61  (zenon_Vqd != zenon_Vrd)
% 0.32/0.61  (p1 zenon_Vue)
% 0.32/0.61  (zenon_Vig != zenon_Vkf)
% 0.32/0.61  (zenon_Vvd != zenon_Vff)
% 0.32/0.61  (zenon_Vwf != zenon_Vaf)
% 0.32/0.61  (zenon_Vgd != zenon_Vmd)
% 0.32/0.61  (zenon_Vwf != zenon_Vqe)
% 0.32/0.61  (zenon_Vig != zenon_Vwd)
% 0.32/0.61  (zenon_Vch != zenon_Vwa)
% 0.32/0.61  (zenon_Voh != zenon_Vge)
% 0.32/0.61  (zenon_Vjf != zenon_Vve)
% 0.32/0.61  (r1 zenon_Vid zenon_Vjd)
% 0.32/0.61  (p1 zenon_Vze)
% 0.32/0.61  (zenon_Vmg != zenon_Vcc)
% 0.32/0.61  (zenon_Vze != zenon_Vff)
% 0.32/0.61  (zenon_Vkh != zenon_Vvc)
% 0.32/0.61  (r1 zenon_Vzc zenon_Vcd)
% 0.32/0.61  (zenon_Vwf != zenon_Vmb)
% 0.32/0.61  (r1 zenon_Vz zenon_Vna)
% 0.32/0.61  (zenon_Vwf != zenon_Veb)
% 0.32/0.61  (-. (p4 zenon_X3))
% 0.32/0.61  (r1 zenon_Ved zenon_Vfd)
% 0.32/0.61  (zenon_Vig != zenon_Vyc)
% 0.32/0.61  (zenon_Voh != zenon_Vub)
% 0.32/0.61  (zenon_Vvd != zenon_Vkf)
% 0.32/0.61  (zenon_Vqg != zenon_Vib)
% 0.32/0.61  (-. (p1 zenon_Vmd))
% 0.32/0.61  (zenon_Vwf != zenon_Vbe)
% 0.32/0.61  (zenon_Vpe != zenon_Vbe)
% 0.32/0.61  (zenon_Vgh != zenon_Vab)
% 0.32/0.61  (-. (p1 zenon_Vkc))
% 0.32/0.61  (zenon_Vyg != zenon_Vhd)
% 0.32/0.61  (zenon_Vfe != zenon_Vpf)
% 0.32/0.61  (zenon_Vae != zenon_Vgc)
% 0.32/0.61  (r1 zenon_Vsd zenon_Vxd)
% 0.32/0.61  (zenon_Vyg != zenon_Vve)
% 0.32/0.61  (zenon_Vue != zenon_Vsc)
% 0.32/0.61  (zenon_Vig != zenon_Vyb)
% 0.32/0.61  (zenon_Vue != zenon_Vab)
% 0.32/0.61  (r1 zenon_Vie zenon_Vle)
% 0.32/0.61  (zenon_Vvd != zenon_Vyb)
% 0.32/0.61  (zenon_Vwh != zenon_Vqe)
% 0.32/0.61  (zenon_Vfe != zenon_Vqb)
% 0.32/0.61  (zenon_Vgh != zenon_Vmb)
% 0.32/0.61  (zenon_Vke != zenon_Vaf)
% 0.32/0.61  (zenon_Vke != zenon_Vvc)
% 0.32/0.61  (zenon_Vxc != zenon_Vcc)
% 0.32/0.61  (zenon_Vch != zenon_Vwd)
% 0.32/0.61  (zenon_Vag != zenon_Voc)
% 0.32/0.61  (zenon_Vld != zenon_Vpf)
% 0.32/0.61  (zenon_Vwf != zenon_Vve)
% 0.32/0.61  (r1 zenon_Vme zenon_Vre)
% 0.32/0.61  (zenon_Vwh != zenon_Vle)
% 0.32/0.61  (zenon_Vgd != zenon_Veb)
% 0.32/0.61  (zenon_Vjf != zenon_Vkf)
% 0.32/0.61  (zenon_Vef != zenon_Vgc)
% 0.32/0.61  (zenon_Vbd != zenon_Vwa)
% 0.32/0.61  (r1 zenon_Vbf zenon_Vcf)
% 0.32/0.61  (zenon_Vef != zenon_Vwa)
% 0.32/0.61  (r1 zenon_Vid zenon_Vnd)
% 0.32/0.61  (zenon_Vue != zenon_Vhd)
% 0.32/0.61  (-. (p1 zenon_Vyb))
% 0.32/0.61  (zenon_Vpe != zenon_Vpf)
% 0.32/0.61  (zenon_Vvd != zenon_Vle)
% 0.32/0.61  (zenon_Vkh != zenon_Vqb)
% 0.32/0.61  (r1 Tau_0 Tau_1)
% 0.32/0.61  (r1 zenon_Vtf zenon_Vwf)
% 0.32/0.61  (zenon_Vmg != zenon_Vge)
% 0.32/0.61  (p1 zenon_Vld)
% 0.32/0.61  (zenon_Vag != zenon_Vcc)
% 0.32/0.61  (zenon_Vue != zenon_Vbe)
% 0.32/0.61  (zenon_Vch != zenon_Vmd)
% 0.32/0.61  (zenon_Vue != zenon_Vle)
% 0.32/0.61  (zenon_Vpe != zenon_Vle)
% 0.32/0.61  (zenon_Vwh != zenon_Vaf)
% 0.32/0.61  (zenon_Vfe != zenon_Vle)
% 0.32/0.61  (r1 zenon_Vxa zenon_Vab)
% 0.32/0.61  (zenon_Vyg != zenon_Vkc)
% 0.32/0.61  (zenon_Vvd != zenon_Vgc)
% 0.32/0.61  (zenon_Vsh != zenon_Vge)
% 0.32/0.61  (zenon_Veg != zenon_Vrd)
% 0.32/0.61  (zenon_Vpe != zenon_Vaf)
% 0.32/0.61  (zenon_Vze != zenon_Vmb)
% 0.32/0.61  (zenon_Vig != zenon_Vbe)
% 0.32/0.61  (zenon_Vue != zenon_Vaf)
% 0.32/0.61  (r1 zenon_Vxf zenon_Vag)
% 0.32/0.61  (zenon_Vue != zenon_Vve)
% 0.32/0.61  (r1 zenon_Vre zenon_Vwe)
% 0.32/0.61  (zenon_Vug != zenon_Vbe)
% 0.32/0.61  (zenon_Vkh != zenon_Vve)
% 0.32/0.61  (zenon_Vyg != zenon_Vcc)
% 0.32/0.61  (zenon_Vae != zenon_Vsa)
% 0.32/0.61  (zenon_Vze != zenon_Vcc)
% 0.32/0.61  (zenon_Vef != zenon_Vab)
% 0.32/0.61  (zenon_Vjf != zenon_Vaf)
% 0.32/0.61  (zenon_Vkh != zenon_Vgc)
% 0.32/0.61  (r1 zenon_Vlh zenon_Voh)
% 0.32/0.61  (zenon_Vof != zenon_Vwa)
% 0.32/0.61  (zenon_Vfe != zenon_Vvc)
% 0.32/0.61  (zenon_Vwf != zenon_Vvc)
% 0.32/0.61  (r1 zenon_Vfg zenon_Vig)
% 0.32/0.61  (zenon_Vig != zenon_Vle)
% 0.32/0.61  (zenon_Vug != zenon_Vff)
% 0.32/0.61  (zenon_Vwh != zenon_Vkf)
% 0.32/0.61  (zenon_Vef != zenon_Vvc)
% 0.32/0.61  (r1 zenon_Vxe zenon_Vaf)
% 0.32/0.61  (zenon_Vug != zenon_Vle)
% 0.32/0.61  (zenon_Vgd != zenon_Vaf)
% 0.32/0.61  (zenon_Vbd != zenon_Vve)
% 0.32/0.61  (zenon_Vch != zenon_Veb)
% 0.32/0.61  (zenon_Vbd != zenon_Vmd)
% 0.32/0.61  (zenon_Vke != zenon_Vkf)
% 0.32/0.61  (zenon_Vxc != zenon_Vyb)
% 0.32/0.61  (zenon_Vqd != zenon_Vmb)
% 0.32/0.61  (zenon_Voh != zenon_Vaf)
% 0.32/0.61  (zenon_Vag != zenon_Veb)
% 0.32/0.61  (zenon_Vvd != zenon_Vcd)
% 0.32/0.61  (zenon_Vbd != zenon_Vab)
% 0.32/0.61  (zenon_Vsh != zenon_Vcd)
% 0.32/0.61  (zenon_Veg != zenon_Vmb)
% 0.32/0.61  (zenon_Vqd != zenon_Vff)
% 0.32/0.61  (zenon_Vbd != zenon_Vub)
% 0.32/0.61  (zenon_Vgd != zenon_Vbe)
% 0.32/0.61  (zenon_Vfe != zenon_Vib)
% 0.32/0.61  (zenon_Vgh != zenon_Vaf)
% 0.32/0.61  (zenon_Veg != zenon_Vwd)
% 0.32/0.61  (zenon_Vfe != zenon_Vbe)
% 0.32/0.61  (zenon_Vbd != zenon_Vsc)
% 0.32/0.61  (zenon_Vgd != zenon_Vcc)
% 0.32/0.61  (zenon_Vwf != zenon_Vub)
% 0.32/0.61  (zenon_Vbd != zenon_Vib)
% 0.32/0.61  (zenon_Vzh != zenon_Vbe)
% 0.32/0.61  (r1 zenon_Vse zenon_Vte)
% 0.32/0.61  (r1 zenon_Vlf zenon_Vmf)
% 0.32/0.61  (zenon_Vwf != zenon_Vcd)
% 0.32/0.61  (zenon_Vld != zenon_Vwd)
% 0.32/0.61  (zenon_Vgd != zenon_Vcd)
% 0.32/0.61  (zenon_Vqg != zenon_Vsc)
% 0.32/0.61  (zenon_Vsh != zenon_Veb)
% 0.32/0.61  (zenon_Voh != zenon_Vve)
% 0.32/0.61  (zenon_Vbd != zenon_Vkc)
% 0.32/0.61  (zenon_Vze != zenon_Vle)
% 0.32/0.61  (zenon_Vvd != zenon_Vbe)
% 0.32/0.61  (zenon_Vyg != zenon_Vgc)
% 0.32/0.61  (zenon_Veg != zenon_Vab)
% 0.32/0.61  (zenon_Vae != zenon_Vkf)
% 0.32/0.61  (zenon_Vig != zenon_Vwa)
% 0.32/0.61  (p1 zenon_Vch)
% 0.32/0.61  (zenon_Veg != zenon_Vmd)
% 0.32/0.61  (p1 zenon_Vqd)
% 0.32/0.61  (zenon_Vze != zenon_Vrd)
% 0.32/0.61  (r1 zenon_Vxe zenon_Vye)
% 0.32/0.61  (p1 zenon_Vke)
% 0.32/0.61  (p1 zenon_Vae)
% 0.32/0.61  (zenon_Vqg != zenon_Vbe)
% 0.32/0.61  (zenon_Vqg != zenon_Vqb)
% 0.32/0.61  (zenon_Vqd != zenon_Vwa)
% 0.32/0.61  (zenon_Vwh != zenon_Vmd)
% 0.32/0.61  (zenon_Vch != zenon_Vaf)
% 0.32/0.61  (zenon_Vxc != zenon_Vle)
% 0.32/0.61  (zenon_Vyg != zenon_Vwa)
% 0.32/0.61  (zenon_Vqg != zenon_Vyb)
% 0.32/0.61  (zenon_Vag != zenon_Vyc)
% 0.32/0.61  (zenon_Vqd != zenon_Vcd)
% 0.32/0.61  (zenon_Vkh != zenon_Vaf)
% 0.32/0.61  (zenon_Vjf != zenon_Vsc)
% 0.32/0.61  (p1 zenon_Vzh)
% 0.32/0.61  (zenon_Vze != zenon_Vkf)
% 0.32/0.61  (zenon_Vqg != zenon_Vab)
% 0.32/0.61  (zenon_Vfe != zenon_Vyc)
% 0.32/0.61  (-. (p1 zenon_Vaf))
% 0.32/0.61  (zenon_Vgd != zenon_Vqb)
% 0.32/0.61  (zenon_Vgh != zenon_Vrd)
% 0.32/0.61  (zenon_Vvd != zenon_Vsa)
% 0.32/0.61  (-. (p1 zenon_Vab))
% 0.32/0.61  (zenon_Vue != zenon_Vge)
% 0.32/0.61  (zenon_Vug != zenon_Veb)
% 0.32/0.61  (zenon_Vsh != zenon_Vqe)
% 0.32/0.61  (zenon_Vvd != zenon_Vrd)
% 0.32/0.61  (zenon_Vwf != zenon_Vge)
% 0.32/0.61  (zenon_Voh != zenon_Vmb)
% 0.32/0.61  (zenon_Vke != zenon_Voc)
% 0.32/0.61  (zenon_Vag != zenon_Vyb)
% 0.32/0.61  (zenon_Vof != zenon_Vhd)
% 0.32/0.61  (zenon_Vzh != zenon_Vkc)
% 0.32/0.61  (zenon_Vig != zenon_Vge)
% 0.32/0.61  (zenon_Vch != zenon_Vpf)
% 0.32/0.61  (zenon_Vqg != zenon_Vyc)
% 0.32/0.61  (zenon_Vef != zenon_Vcd)
% 0.32/0.61  (zenon_Vig != zenon_Vgc)
% 0.32/0.61  (zenon_Vld != zenon_Vff)
% 0.32/0.61  (zenon_Vmg != zenon_Vsc)
% 0.32/0.61  (zenon_Vue != zenon_Veb)
% 0.32/0.61  (zenon_Vof != zenon_Vbe)
% 0.32/0.61  (zenon_Vpe != zenon_Vgc)
% 0.32/0.61  (zenon_Vgh != zenon_Vqe)
% 0.32/0.61  (zenon_Vke != zenon_Vgc)
% 0.32/0.61  (zenon_Vgh != zenon_Vve)
% 0.32/0.61  (zenon_Vzh != zenon_Vve)
% 0.32/0.61  (zenon_Vvd != zenon_Vsc)
% 0.32/0.61  (zenon_Vag != zenon_Vqb)
% 0.32/0.61  (zenon_Vkh != zenon_Vyb)
% 0.32/0.61  (zenon_Vfe != zenon_Vqe)
% 0.32/0.61  (p1 zenon_Vvd)
% 0.32/0.61  (zenon_Vsh != zenon_Vkc)
% 0.32/0.61  (p1 zenon_Vxc)
% 0.32/0.61  (zenon_Vsh != zenon_Vub)
% 0.32/0.61  (zenon_Vqg != zenon_Vve)
% 0.32/0.61  (zenon_Voh != zenon_Vff)
% 0.32/0.61  (zenon_Veg != zenon_Veb)
% 0.32/0.61  (zenon_Vmg != zenon_Vwd)
% 0.32/0.61  (zenon_Vsh != zenon_Vyc)
% 0.32/0.61  (zenon_Vld != zenon_Vqb)
% 0.32/0.61  (zenon_Vxc != zenon_Vgc)
% 0.32/0.61  (zenon_Vze != zenon_Vqe)
% 0.32/0.61  (zenon_Vld != zenon_Vbe)
% 0.32/0.61  (zenon_Vyg != zenon_Vsa)
% 0.32/0.61  (zenon_Vzh != zenon_Vqe)
% 0.32/0.61  (zenon_Vef != zenon_Vkf)
% 0.32/0.61  (zenon_Vvd != zenon_Vwd)
% 0.32/0.61  (r1 zenon_Vcf zenon_Vff)
% 0.32/0.61  (zenon_Voh != zenon_Vcd)
% 0.32/0.61  (zenon_Vag != zenon_Vab)
% 0.32/0.61  (zenon_Vsh != zenon_Vpf)
% 0.32/0.61  (zenon_Vbd != zenon_Vmb)
% 0.32/0.61  (zenon_Voh != zenon_Vab)
% 0.32/0.61  (zenon_Voh != zenon_Vhd)
% 0.32/0.61  (zenon_Vch != zenon_Vyc)
% 0.32/0.61  (zenon_Vmg != zenon_Vyb)
% 0.32/0.61  (zenon_Vpe != zenon_Vmb)
% 0.32/0.61  (r1 zenon_Vjb zenon_Vmb)
% 0.32/0.61  (p1 zenon_Vsh)
% 0.32/0.61  (zenon_Vsh != zenon_Vab)
% 0.32/0.61  (zenon_Vch != zenon_Vkc)
% 0.32/0.61  (zenon_Voh != zenon_Veb)
% 0.32/0.61  (zenon_Vpe != zenon_Veb)
% 0.32/0.61  (zenon_Vqg != zenon_Vhd)
% 0.32/0.61  (r1 zenon_Vdd zenon_Ved)
% 0.32/0.61  (zenon_Vke != zenon_Vcc)
% 0.32/0.61  (zenon_Vqd != zenon_Vcc)
% 0.32/0.61  (zenon_Vgh != zenon_Vpf)
% 0.32/0.61  (zenon_Vxc != zenon_Vib)
% 0.32/0.61  (zenon_Vsh != zenon_Vff)
% 0.32/0.61  (zenon_Vmg != zenon_Vaf)
% 0.32/0.61  (zenon_Voh != zenon_Vmd)
% 0.32/0.61  (r1 zenon_Vod zenon_Vrd)
% 0.32/0.61  (-. (p1 zenon_Vsc))
% 0.32/0.61  (zenon_Vke != zenon_Vkc)
% 0.32/0.61  (zenon_Vae != zenon_Vib)
% 0.32/0.61  (zenon_Vof != zenon_Veb)
% 0.32/0.61  (zenon_Vag != zenon_Vmd)
% 0.32/0.61  (zenon_Vag != zenon_Vvc)
% 0.32/0.61  (zenon_Vef != zenon_Vrd)
% 0.32/0.61  (zenon_Vvd != zenon_Vve)
% 0.32/0.61  (zenon_Vmg != zenon_Vbe)
% 0.32/0.61  (zenon_Vug != zenon_Vpf)
% 0.32/0.61  (zenon_Vkh != zenon_Vwd)
% 0.32/0.61  (zenon_Vgd != zenon_Vyc)
% 0.32/0.61  (zenon_Vch != zenon_Vib)
% 0.32/0.61  (-. (p1 zenon_Vle))
% 0.32/0.61  (r1 zenon_Vng zenon_Vqg)
% 0.32/0.61  (zenon_Vae != zenon_Vge)
% 0.32/0.61  (zenon_Vmg != zenon_Vsa)
% 0.32/0.61  (zenon_Vig != zenon_Vcc)
% 0.32/0.61  (-. (p1 zenon_Vvc))
% 0.32/0.61  (zenon_Vgh != zenon_Vmd)
% 0.32/0.61  (zenon_Vfe != zenon_Vgc)
% 0.32/0.61  (zenon_Vld != zenon_Vub)
% 0.32/0.61  (zenon_Vze != zenon_Vsa)
% 0.32/0.61  (zenon_Vug != zenon_Vkc)
% 0.32/0.61  (zenon_Vjf != zenon_Vkc)
% 0.32/0.61  (zenon_Vae != zenon_Vbe)
% 0.32/0.61  (zenon_Vwh != zenon_Vcc)
% 0.32/0.61  (zenon_Vof != zenon_Vgc)
% 0.32/0.61  (-. (p1 zenon_Vkf))
% 0.32/0.61  (zenon_Vpe != zenon_Vqe)
% 0.32/0.61  (zenon_Vke != zenon_Vle)
% 0.32/0.61  (zenon_Vwh != zenon_Vyb)
% 0.32/0.61  (r1 zenon_Vzc zenon_Vad)
% 0.32/0.61  (zenon_Veg != zenon_Vwa)
% 0.32/0.61  (zenon_Vqd != zenon_Vgc)
% 0.32/0.61  (zenon_Vae != zenon_Veb)
% 0.32/0.61  (zenon_Vke != zenon_Vsa)
% 0.32/0.61  (zenon_Vef != zenon_Vhd)
% 0.32/0.61  (zenon_Vkh != zenon_Vkf)
% 0.32/0.61  (-. (p1 zenon_Vcd))
% 0.32/0.61  (zenon_Vze != zenon_Vve)
% 0.32/0.61  (r1 zenon_Vzg zenon_Vch)
% 0.32/0.61  (zenon_Vug != zenon_Vge)
% 0.32/0.61  (zenon_Vvd != zenon_Vyc)
% 0.32/0.61  (zenon_Vbd != zenon_Vle)
% 0.32/0.61  (zenon_Vch != zenon_Vab)
% 0.32/0.61  (zenon_Vgh != zenon_Vyb)
% 0.32/0.61  (zenon_Vpe != zenon_Vwd)
% 0.32/0.61  (zenon_Vbd != zenon_Vcd)
% 0.32/0.61  (zenon_Voh != zenon_Vrd)
% 0.32/0.61  (zenon_Vqd != zenon_Veb)
% 0.32/0.61  (zenon_Vof != zenon_Vpf)
% 0.32/0.61  (zenon_Vfe != zenon_Vkf)
% 0.32/0.61  (zenon_Vch != zenon_Vkf)
% 0.32/0.61  (zenon_Vgd != zenon_Vmb)
% 0.32/0.61  (p1 zenon_Vwh)
% 0.32/0.61  (zenon_Vch != zenon_Vff)
% 0.32/0.61  (zenon_Vyg != zenon_Vab)
% 0.32/0.61  (zenon_Vsh != zenon_Vib)
% 0.32/0.61  (r1 zenon_Vrg zenon_Vug)
% 0.32/0.61  (zenon_Vpe != zenon_Vkc)
% 0.32/0.61  (zenon_Vwh != zenon_Vgc)
% 0.32/0.61  (zenon_Vvd != zenon_Veb)
% 0.32/0.61  (zenon_Vke != zenon_Vyc)
% 0.32/0.61  (zenon_Vsh != zenon_Vle)
% 0.32/0.61  (zenon_Voh != zenon_Vyc)
% 0.32/0.61  (zenon_Vzh != zenon_Vab)
% 0.32/0.61  (zenon_Vze != zenon_Vwa)
% 0.32/0.61  (zenon_Vld != zenon_Vaf)
% 0.32/0.61  (p2 zenon_Vba)
% 0.32/0.61  (zenon_Vof != zenon_Vwd)
% 0.32/0.61  (zenon_Vag != zenon_Vub)
% 0.32/0.61  (zenon_Vqd != zenon_Vib)
% 0.32/0.61  (zenon_Vug != zenon_Vqe)
% 0.32/0.61  (zenon_Vag != zenon_Vpf)
% 0.32/0.61  (zenon_Vgh != zenon_Vcd)
% 0.32/0.61  (zenon_Vqd != zenon_Vaf)
% 0.32/0.61  (zenon_Vze != zenon_Vub)
% 0.32/0.61  (zenon_Vef != zenon_Vpf)
% 0.32/0.61  (zenon_Veg != zenon_Vge)
% 0.32/0.61  (zenon_Vef != zenon_Vsc)
% 0.32/0.61  (zenon_Vvd != zenon_Vcc)
% 0.32/0.61  (zenon_Vug != zenon_Vvc)
% 0.32/0.61  (zenon_Vug != zenon_Vcc)
% 0.32/0.61  (zenon_Vmg != zenon_Vab)
% 0.32/0.61  (zenon_Vqd != zenon_Vkf)
% 0.32/0.61  (zenon_Vig != zenon_Vkc)
% 0.32/0.61  (zenon_Veg != zenon_Vyc)
% 0.32/0.61  (zenon_Vue != zenon_Vmb)
% 0.32/0.61  (r1 zenon_Vhe zenon_Vme)
% 0.32/0.61  (r1 zenon_Vrb zenon_Vub)
% 0.32/0.61  (zenon_Vae != zenon_Vab)
% 0.32/0.61  (p1 zenon_Vig)
% 0.32/0.61  (zenon_Vwf != zenon_Vff)
% 0.32/0.61  (zenon_Vig != zenon_Vmb)
% 0.32/0.61  (zenon_Vqd != zenon_Vle)
% 0.32/0.61  (zenon_Vbd != zenon_Vyb)
% 0.32/0.61  (r1 zenon_Vgf zenon_Vhf)
% 0.32/0.61  (zenon_Vbd != zenon_Vqe)
% 0.32/0.61  (zenon_Vzh != zenon_Vyc)
% 0.32/0.61  (zenon_Vld != zenon_Vsc)
% 0.32/0.61  (zenon_Vue != zenon_Vpf)
% 0.32/0.61  (zenon_Vqg != zenon_Vrd)
% 0.32/0.61  (zenon_Vxc != zenon_Vsc)
% 0.32/0.61  (zenon_Vof != zenon_Vkc)
% 0.32/0.61  (zenon_Vqg != zenon_Vle)
% 0.32/0.61  (r1 zenon_Vde zenon_Vee)
% 0.32/0.61  (zenon_Vae != zenon_Vyc)
% 0.32/0.61  (zenon_Vze != zenon_Vaf)
% 0.32/0.61  (zenon_Vvd != zenon_Vab)
% 0.32/0.61  (zenon_Vke != zenon_Vbe)
% 0.32/0.61  (zenon_Vke != zenon_Vcd)
% 0.32/0.61  (zenon_Vae != zenon_Vkc)
% 0.32/0.61  (-. (p1 zenon_Vrd))
% 0.32/0.61  (zenon_Vke != zenon_Vhd)
% 0.32/0.61  (zenon_Vae != zenon_Vcc)
% 0.32/0.61  (r1 zenon_Vre zenon_Vse)
% 0.32/0.61  (zenon_Vwf != zenon_Vyc)
% 0.32/0.61  (zenon_Veg != zenon_Vsa)
% 0.32/0.61  (zenon_Vke != zenon_Vqe)
% 0.32/0.61  (zenon_Vae != zenon_Vvc)
% 0.32/0.61  (zenon_Vzh != zenon_Vpf)
% 0.32/0.61  (r1 zenon_X6 zenon_Vzh)
% 0.32/0.61  (zenon_Vkh != zenon_Vpf)
% 0.32/0.61  (zenon_Veg != zenon_Vcc)
% 0.32/0.61  (zenon_Vxc != zenon_Vve)
% 0.32/0.61  (zenon_Vof != zenon_Vsc)
% 0.32/0.61  (r1 zenon_Vnd zenon_Vod)
% 0.32/0.61  (zenon_Vug != zenon_Vkf)
% 0.32/0.61  (zenon_Vxc != zenon_Vub)
% 0.32/0.61  (zenon_Vwf != zenon_Vkf)
% 0.32/0.61  (zenon_Vch != zenon_Vle)
% 0.32/0.61  (zenon_Vof != zenon_Vaf)
% 0.32/0.61  (zenon_Vag != zenon_Vaf)
% 0.32/0.61  (-. (p1 zenon_Vib))
% 0.32/0.61  (zenon_Vch != zenon_Vgc)
% 0.32/0.61  (zenon_Vef != zenon_Vyc)
% 0.32/0.61  (zenon_Vof != zenon_Vab)
% 0.32/0.61  (zenon_Vfe != zenon_Vhd)
% 0.32/0.61  (zenon_Vld != zenon_Vrd)
% 0.32/0.61  (r1 zenon_Vfb zenon_Vib)
% 0.32/0.61  (zenon_Vke != zenon_Vwa)
% 0.32/0.61  (zenon_Vsh != zenon_Vrd)
% 0.32/0.61  (zenon_Vkh != zenon_Vub)
% 0.32/0.61  (r1 zenon_Ved zenon_Vhd)
% 0.32/0.61  (zenon_Vyg != zenon_Vyb)
% 0.32/0.61  (zenon_Vkh != zenon_Vab)
% 0.32/0.61  (zenon_Vef != zenon_Vqe)
% 0.32/0.61  (zenon_Vpe != zenon_Vsa)
% 0.32/0.61  (zenon_Vwf != zenon_Vsa)
% 0.32/0.61  (zenon_Vjf != zenon_Vvc)
% 0.32/0.61  (zenon_Vze != zenon_Vab)
% 0.32/0.61  (zenon_Vig != zenon_Vmd)
% 0.32/0.61  (zenon_Vue != zenon_Vqb)
% 0.32/0.61  (zenon_Vvd != zenon_Vkc)
% 0.32/0.61  (zenon_Vue != zenon_Vmd)
% 0.32/0.61  (zenon_Vkh != zenon_Vmd)
% 0.32/0.61  (zenon_Vch != zenon_Vcc)
% 0.32/0.61  (zenon_Vke != zenon_Vqb)
% 0.32/0.61  (zenon_Vxc != zenon_Vmb)
% 0.32/0.61  (zenon_Vqg != zenon_Vcd)
% 0.32/0.61  (zenon_Vyg != zenon_Voc)
% 0.32/0.61  (zenon_Vug != zenon_Vyc)
% 0.32/0.61  (zenon_Vbd != zenon_Veb)
% 0.32/0.61  (zenon_Vld != zenon_Vab)
% 0.32/0.61  (zenon_Vzh != zenon_Vhd)
% 0.32/0.61  (zenon_Vch != zenon_Voc)
% 0.32/0.61  (zenon_Vmg != zenon_Vgc)
% 0.32/0.61  (zenon_Voh != zenon_Vcc)
% 0.32/0.61  (r1 zenon_Vaa zenon_Vba)
% 0.32/0.61  (zenon_Vag != zenon_Vbe)
% 0.32/0.61  (zenon_Vgd != zenon_Vqe)
% 0.32/0.61  (zenon_Vbd != zenon_Vwd)
% 0.32/0.61  (zenon_Vxc != zenon_Vqe)
% 0.32/0.61  (zenon_Vzh != zenon_Vsa)
% 0.32/0.61  (zenon_Vjf != zenon_Veb)
% 0.32/0.61  (zenon_Vwh != zenon_Vwa)
% 0.32/0.61  (zenon_Vig != zenon_Vub)
% 0.32/0.61  (zenon_Vwf != zenon_Vwd)
% 0.32/0.61  (zenon_Vgd != zenon_Vkc)
% 0.32/0.61  (zenon_Vld != zenon_Vkf)
% 0.32/0.61  (zenon_Vwf != zenon_Vrd)
% 0.32/0.61  (zenon_Vqg != zenon_Vqe)
% 0.32/0.61  (zenon_Vae != zenon_Vhd)
% 0.32/0.61  (r1 zenon_Vbf zenon_Vgf)
% 0.32/0.61  (zenon_Vze != zenon_Vib)
% 0.32/0.61  (zenon_Vag != zenon_Vwa)
% 0.32/0.61  (zenon_Vwf != zenon_Vgc)
% 0.32/0.61  (r1 zenon_Vbg zenon_Veg)
% 0.32/0.61  (zenon_Vke != zenon_Vge)
% 0.32/0.61  (zenon_Vbd != zenon_Vkf)
% 0.32/0.61  (r1 zenon_Vmf zenon_Vpf)
% 0.32/0.61  (zenon_Vch != zenon_Vsa)
% 0.32/0.61  (zenon_Vug != zenon_Vve)
% 0.32/0.61  (zenon_Vsh != zenon_Vmd)
% 0.32/0.61  (zenon_Vkh != zenon_Vcc)
% 0.32/0.61  (zenon_Vwh != zenon_Vsa)
% 0.32/0.61  (zenon_Vqg != zenon_Vff)
% 0.32/0.61  (zenon_Vwh != zenon_Vqb)
% 0.32/0.61  (zenon_Vwf != zenon_Vle)
% 0.32/0.61  (zenon_Vae != zenon_Vle)
% 0.32/0.61  (zenon_Vch != zenon_Vyb)
% 0.32/0.61  (r1 zenon_Vce zenon_Vhe)
% 0.32/0.61  (r1 zenon_Vmf zenon_Vnf)
% 0.32/0.61  (zenon_Veg != zenon_Vhd)
% 0.32/0.61  (zenon_Vsh != zenon_Vwa)
% 0.32/0.61  (zenon_Vld != zenon_Vhd)
% 0.32/0.61  (zenon_Vef != zenon_Vkc)
% 0.32/0.61  (zenon_Vjf != zenon_Vgc)
% 0.32/0.61  (zenon_Vgd != zenon_Vve)
% 0.32/0.61  (r1 zenon_Vtd zenon_Vud)
% 0.32/0.61  (zenon_Vwh != zenon_Voc)
% 0.32/0.61  (zenon_Vef != zenon_Vsa)
% 0.32/0.61  (zenon_Vag != zenon_Vib)
% 0.32/0.61  (zenon_Vjf != zenon_Vpf)
% 0.32/0.61  (p1 zenon_Vbd)
% 0.32/0.61  (zenon_Vae != zenon_Vmd)
% 0.32/0.61  (zenon_Vsh != zenon_Vqb)
% 0.32/0.61  (zenon_Vze != zenon_Vvc)
% 0.32/0.61  (zenon_Vvd != zenon_Vhd)
% 0.32/0.61  (zenon_Vxc != zenon_Vqb)
% 0.32/0.61  (zenon_Vwf != zenon_Vab)
% 0.32/0.61  (zenon_Vch != zenon_Vrd)
% 0.32/0.61  (zenon_Vxc != zenon_Vge)
% 0.32/0.61  (zenon_Vig != zenon_Vsc)
% 0.32/0.61  (zenon_Vmg != zenon_Veb)
% 0.32/0.61  (r1 zenon_Vhf zenon_Vif)
% 0.32/0.61  (zenon_Vkh != zenon_Vbe)
% 0.32/0.61  (zenon_Vld != zenon_Vyc)
% 0.32/0.61  (zenon_Vfe != zenon_Vaf)
% 0.32/0.61  (zenon_Vpe != zenon_Vcc)
% 0.32/0.61  (zenon_Vue != zenon_Vcd)
% 0.32/0.61  (zenon_Vld != zenon_Vge)
% 0.32/0.61  (zenon_Vvd != zenon_Voc)
% 0.32/0.61  (zenon_Veg != zenon_Vgc)
% 0.32/0.61  (zenon_Vue != zenon_Vrd)
% 0.32/0.61  (zenon_Vxc != zenon_Vpf)
% 0.32/0.61  (zenon_Vpe != zenon_Vqb)
% 0.32/0.61  (zenon_Vpe != zenon_Voc)
% 0.32/0.61  (zenon_Vzh != zenon_Vub)
% 0.32/0.61  (r1 zenon_Vme zenon_Vne)
% 0.32/0.61  (zenon_Voh != zenon_Vqe)
% 0.32/0.61  (zenon_Voh != zenon_Vkc)
% 0.32/0.61  (zenon_Vgd != zenon_Vab)
% 0.32/0.61  (p1 zenon_Veg)
% 0.32/0.61  (zenon_Vze != zenon_Vsc)
% 0.32/0.61  (zenon_Vgd != zenon_Vub)
% 0.32/0.61  (zenon_Vqg != zenon_Veb)
% 0.32/0.61  (zenon_Vpe != zenon_Vmd)
% 0.32/0.61  (zenon_Vkh != zenon_Vge)
% 0.32/0.61  (r1 zenon_Vhf zenon_Vkf)
% 0.32/0.61  (zenon_Vpe != zenon_Vrd)
% 0.32/0.61  (zenon_Vyg != zenon_Vwd)
% 0.32/0.61  (zenon_Vke != zenon_Vsc)
% 0.32/0.61  (zenon_Vbd != zenon_Vhd)
% 0.32/0.61  (zenon_Vfe != zenon_Voc)
% 0.32/0.61  (zenon_Vzh != zenon_Vle)
% 0.32/0.61  (zenon_Voh != zenon_Vqb)
% 0.32/0.61  (zenon_Vld != zenon_Vvc)
% 0.32/0.61  (zenon_Vof != zenon_Vyc)
% 0.32/0.61  (zenon_Vig != zenon_Vve)
% 0.32/0.61  (zenon_Vze != zenon_Vgc)
% 0.32/0.61  (zenon_Vwf != zenon_Voc)
% 0.32/0.61  (zenon_Vfe != zenon_Vyb)
% 0.32/0.61  (zenon_Vof != zenon_Vle)
% 0.32/0.61  (zenon_Vze != zenon_Vhd)
% 0.32/0.61  (r1 zenon_Vse zenon_Vve)
% 0.32/0.61  (zenon_Vch != zenon_Vge)
% 0.32/0.61  (zenon_Vzh != zenon_Vsc)
% 0.32/0.61  (-. (p1 zenon_Vhd))
% 0.32/0.61  (zenon_Vug != zenon_Vab)
% 0.32/0.61  (p1 zenon_Voh)
% 0.32/0.61  (zenon_Vbd != zenon_Vqb)
% 0.32/0.61  (zenon_Vkh != zenon_Voc)
% 0.32/0.61  (zenon_Vxc != zenon_Vrd)
% 0.32/0.61  (zenon_Vug != zenon_Vwd)
% 0.32/0.61  (zenon_Vef != zenon_Vqb)
% 0.32/0.61  (zenon_Vbd != zenon_Vcc)
% 0.32/0.61  (zenon_Vwf != zenon_Vwa)
% 0.32/0.61  (p1 zenon_Vwf)
% 0.32/0.61  (zenon_Vyg != zenon_Vub)
% 0.32/0.61  (p1 zenon_Vag)
% 0.32/0.61  (zenon_Vxc != zenon_Veb)
% 0.32/0.61  (zenon_Vjf != zenon_Vff)
% 0.32/0.61  (zenon_Vbd != zenon_Vrd)
% 0.32/0.61  (zenon_Veg != zenon_Vve)
% 0.32/0.61  (zenon_Vef != zenon_Veb)
% 0.32/0.61  (-. (p1 zenon_Vve))
% 0.32/0.61  (zenon_Vbd != zenon_Vge)
% 0.32/0.61  (zenon_Vzh != zenon_Vcc)
% 0.32/0.61  (zenon_Vqg != zenon_Vsa)
% 0.32/0.61  (p1 zenon_Vug)
% 0.32/0.61  (zenon_Vmg != zenon_Vff)
% 0.32/0.61  (zenon_Vld != zenon_Vve)
% 0.32/0.61  (zenon_Vyg != zenon_Vle)
% 0.32/0.61  (zenon_Vgd != zenon_Vsa)
% 0.32/0.61  (zenon_Vwh != zenon_Vge)
% 0.32/0.61  (zenon_Vmg != zenon_Vwa)
% 0.32/0.61  (zenon_Vxc != zenon_Vsa)
% 0.32/0.61  (zenon_Vag != zenon_Vsc)
% 0.32/0.61  (zenon_Veg != zenon_Voc)
% 0.32/0.61  (zenon_Vof != zenon_Vmb)
% 0.32/0.61  (zenon_Vjf != zenon_Vib)
% 0.32/0.61  (r1 Tau_1 zenon_Vyc)
% 0.32/0.61  (zenon_Vxc != zenon_Vaf)
% 0.32/0.61  (r1 zenon_Vne zenon_Voe)
% 0.32/0.61  (zenon_Vvd != zenon_Vub)
% 0.32/0.61  (zenon_Vmg != zenon_Vmb)
% 0.32/0.61  (zenon_Vue != zenon_Vqe)
% 0.32/0.61  (zenon_Vkh != zenon_Vff)
% 0.32/0.61  (zenon_Vof != zenon_Vib)
% 0.32/0.61  (zenon_Vgd != zenon_Vwa)
% 0.32/0.61  (zenon_Vld != zenon_Vwa)
% 0.32/0.61  (zenon_Vkh != zenon_Vrd)
% 0.32/0.61  (zenon_Vze != zenon_Vqb)
% 0.32/0.61  (zenon_Veg != zenon_Vaf)
% 0.32/0.61  (r1 zenon_Vlc zenon_Voc)
% 0.32/0.61  (zenon_Vbd != zenon_Vyc)
% 0.32/0.61  (zenon_Vmg != zenon_Vrd)
% 0.32/0.61  (zenon_Vyg != zenon_Veb)
% 0.32/0.61  (zenon_Vzh != zenon_Vff)
% 0.32/0.61  (-. (p1 zenon_Vqe))
% 0.32/0.61  (zenon_Vjf != zenon_Vab)
% 0.32/0.61  (zenon_Vld != zenon_Vmb)
% 0.32/0.61  (zenon_Vqg != zenon_Vpf)
% 0.32/0.61  (zenon_Vkh != zenon_Vmb)
% 0.32/0.61  (zenon_Voh != zenon_Vvc)
% 0.32/0.61  (zenon_Vvd != zenon_Vge)
% 0.32/0.61  (zenon_Vxc != zenon_Vmd)
% 0.32/0.61  (zenon_Vwf != zenon_Vcc)
% 0.32/0.61  (zenon_Vyg != zenon_Vyc)
% 0.32/0.61  (zenon_Vqg != zenon_Vwa)
% 0.32/0.61  (zenon_Vgd != zenon_Vvc)
% 0.32/0.61  (zenon_Vvd != zenon_Vpf)
% 0.32/0.61  (r1 zenon_X5 zenon_Vvc)
% 0.32/0.61  (zenon_Vag != zenon_Vwd)
% 0.32/0.61  (zenon_Vwh != zenon_Vab)
% 0.32/0.61  (zenon_Vsh != zenon_Vsa)
% 0.32/0.61  (zenon_Vgh != zenon_Vsa)
% 0.32/0.61  (r1 zenon_Vpa zenon_Vsa)
% 0.32/0.61  (zenon_Vof != zenon_Vcd)
% 0.32/0.61  (zenon_Vae != zenon_Vqe)
% 0.32/0.61  (zenon_Voh != zenon_Vyb)
% 0.32/0.61  (r1 zenon_Vbb zenon_Veb)
% 0.32/0.61  (zenon_Vjf != zenon_Vrd)
% 0.32/0.61  (zenon_Vwf != zenon_Vsc)
% 0.32/0.61  (zenon_Vsh != zenon_Vbe)
% 0.32/0.61  (r1 zenon_Vth zenon_Vwh)
% 0.32/0.61  (zenon_Vae != zenon_Vub)
% 0.32/0.61  (zenon_Vbd != zenon_Vgc)
% 0.32/0.61  (zenon_Vgh != zenon_Vwd)
% 0.32/0.61  (zenon_Vfe != zenon_Vsc)
% 0.32/0.61  (r1 Tau_0 Tau_2)
% 0.32/0.61  (-. (p1 zenon_Vwd))
% 0.32/0.61  (zenon_Vjf != zenon_Vyc)
% 0.32/0.61  (zenon_Vld != zenon_Vcc)
% 0.32/0.61  (zenon_Vag != zenon_Vrd)
% 0.32/0.61  (zenon_Vqg != zenon_Vcc)
% 0.32/0.61  (zenon_Vwh != zenon_Vmb)
% 0.32/0.61  (zenon_Vze != zenon_Vyc)
% 0.32/0.61  (zenon_Vch != zenon_Vve)
% 0.32/0.61  (zenon_Vld != zenon_Vyb)
% 0.32/0.61  (zenon_Vug != zenon_Vib)
% 0.32/0.61  (zenon_Vpe != zenon_Vff)
% 0.32/0.61  (zenon_Vyg != zenon_Vqe)
% 0.32/0.61  (zenon_Vgh != zenon_Vib)
% 0.32/0.61  (zenon_Vqg != zenon_Vkf)
% 0.32/0.61  (r1 zenon_Vxd zenon_Vyd)
% 0.32/0.61  (p1 zenon_Vgd)
% 0.32/0.61  (zenon_Vld != zenon_Vsa)
% 0.32/0.61  (zenon_Vjf != zenon_Vmd)
% 0.32/0.61  (zenon_Vsh != zenon_Vvc)
% 0.32/0.61  (r1 zenon_Vba zenon_Vca)
% 0.32/0.61  (zenon_Vig != zenon_Vff)
% 0.32/0.61  (p1 zenon_Vjf)
% 0.32/0.61  (zenon_Vig != zenon_Veb)
% 0.32/0.61  (zenon_Vyg != zenon_Vsc)
% 0.32/0.61  (zenon_Vae != zenon_Voc)
% 0.32/0.61  (zenon_Veg != zenon_Vib)
% 0.32/0.61  (zenon_Vae != zenon_Vqb)
% 0.32/0.61  (zenon_Vug != zenon_Vcd)
% 0.32/0.61  (zenon_Vmg != zenon_Vyc)
% 0.32/0.61  (zenon_Vjf != zenon_Vhd)
% 0.32/0.61  (zenon_Vof != zenon_Vub)
% 0.32/0.61  (zenon_Vsh != zenon_Vaf)
% 0.32/0.61  (zenon_Vag != zenon_Vle)
% 0.32/0.61  (zenon_Vzh != zenon_Vge)
% 0.32/0.61  (r1 zenon_Vhh zenon_Vkh)
% 0.32/0.61  (zenon_Vig != zenon_Vib)
% 0.32/0.61  (zenon_Vgh != zenon_Vkc)
% 0.32/0.61  (zenon_Vld != zenon_Vmd)
% 0.32/0.61  (zenon_Vgd != zenon_Vff)
% 0.32/0.61  (r1 zenon_Vwe zenon_Vxe)
% 0.32/0.61  (zenon_Vef != zenon_Vib)
% 0.32/0.61  (zenon_Vpe != zenon_Vwa)
% 0.32/0.61  (zenon_Vze != zenon_Voc)
% 0.32/0.61  (zenon_Vyg != zenon_Vmb)
% 0.32/0.61  (r1 zenon_Vdd zenon_Vid)
% 0.32/0.61  (-. (p2 zenon_Via))
% 0.32/0.61  (zenon_Vpe != zenon_Vcd)
% 0.32/0.61  (zenon_Vbd != zenon_Vpf)
% 0.32/0.61  (zenon_Vef != zenon_Vaf)
% 0.32/0.61  (zenon_Vze != zenon_Vmd)
% 0.32/0.61  (zenon_Vkh != zenon_Vcd)
% 0.32/0.61  (zenon_Vxc != zenon_Vcd)
% 0.32/0.61  (zenon_Vzh != zenon_Vyb)
% 0.32/0.61  (zenon_Veg != zenon_Vkc)
% 0.32/0.61  (r1 zenon_Vce zenon_Vde)
% 0.32/0.61  (zenon_Vsh != zenon_Vve)
% 0.32/0.61  (zenon_Vfe != zenon_Vff)
% 0.32/0.61  (zenon_Vqd != zenon_Vyb)
% 0.32/0.61  (r1 zenon_Vwe zenon_Vbf)
% 0.32/0.61  (zenon_Vqd != zenon_Vve)
% 0.32/0.61  (zenon_Vke != zenon_Vff)
% 0.32/0.61  (zenon_Vjf != zenon_Vsa)
% 0.32/0.61  (zenon_Vfe != zenon_Vge)
% 0.32/0.61  (zenon_Vof != zenon_Vqe)
% 0.32/0.61  (zenon_Vqd != zenon_Vub)
% 0.32/0.61  (zenon_Vue != zenon_Vvc)
% 0.32/0.61  (zenon_Vxc != zenon_Vwd)
% 0.32/0.61  (zenon_Vag != zenon_Vqe)
% 0.32/0.61  (zenon_Vfe != zenon_Vab)
% 0.32/0.61  (zenon_Vbd != zenon_Voc)
% 0.32/0.61  (zenon_Vkh != zenon_Vsc)
% 0.32/0.61  (zenon_Vef != zenon_Vub)
% 0.32/0.61  (zenon_Vwf != zenon_Vqb)
% 0.32/0.61  (p1 zenon_Vof)
% 0.32/0.61  (zenon_Vue != zenon_Vff)
% 0.32/0.61  (zenon_Vqg != zenon_Vvc)
% 0.32/0.61  (-. (p1 zenon_Vmb))
% 0.32/0.61  (zenon_Vwh != zenon_Vff)
% 0.32/0.61  (zenon_Veg != zenon_Vcd)
% 0.32/0.61  (zenon_Vug != zenon_Vub)
% 0.32/0.61  (zenon_Vqd != zenon_Vvc)
% 0.32/0.61  (zenon_Vld != zenon_Vqe)
% 0.32/0.61  (zenon_Vfe != zenon_Vrd)
% 0.32/0.61  (zenon_Vjf != zenon_Vcc)
% 0.32/0.61  (zenon_Vwf != zenon_Vpf)
% 0.32/0.61  (zenon_Vvd != zenon_Vib)
% 0.32/0.61  (zenon_Vag != zenon_Vsa)
% 0.32/0.61  (zenon_Vqd != zenon_Vmd)
% 0.32/0.61  (zenon_Vke != zenon_Vpf)
% 0.32/0.61  (zenon_Vgh != zenon_Vkf)
% 0.32/0.61  (zenon_Voh != zenon_Voc)
% 0.32/0.61  (zenon_Vgd != zenon_Vib)
% 0.32/0.61  (zenon_Vmg != zenon_Vhd)
% 0.32/0.61  (zenon_Vig != zenon_Voc)
% 0.32/0.61  (zenon_Vug != zenon_Vgc)
% 0.32/0.61  (-. (p1 zenon_Vge))
% 0.32/0.61  (zenon_Vxc != zenon_Vhd)
% 0.32/0.61  (zenon_Vsh != zenon_Voc)
% 0.32/0.61  (zenon_Vae != zenon_Vyb)
% 0.32/0.61  (zenon_Voh != zenon_Vkf)
% 0.32/0.61  (zenon_Vpe != zenon_Vge)
% 0.32/0.61  (zenon_Vqd != zenon_Vyc)
% 0.32/0.61  (zenon_Vwf != zenon_Vmd)
% 0.32/0.61  (zenon_Vfe != zenon_Vcd)
% 0.32/0.61  (zenon_Vmg != zenon_Vmd)
% 0.32/0.61  (zenon_Vbd != zenon_Vbe)
% 0.32/0.61  (zenon_Vke != zenon_Vyb)
% 0.32/0.61  (zenon_Vae != zenon_Vff)
% 0.32/0.61  (zenon_Vld != zenon_Vcd)
% 0.32/0.61  (zenon_Vxc != zenon_Vkc)
% 0.32/0.61  (zenon_Vug != zenon_Vwa)
% 0.32/0.61  (r1 zenon_Vvb zenon_Vyb)
% 0.32/0.61  (zenon_Vze != zenon_Vcd)
% 0.32/0.61  (zenon_Vsh != zenon_Vmb)
% 0.32/0.61  (zenon_Vmg != zenon_Vib)
% 0.32/0.61  (zenon_Vsh != zenon_Vwd)
% 0.32/0.61  (zenon_Vae != zenon_Vrd)
% 0.32/0.61  (zenon_Vwh != zenon_Vyc)
% 0.32/0.61  (zenon_Vgh != zenon_Vge)
% 0.32/0.61  (zenon_Vjf != zenon_Vwa)
% 0.32/0.61  (zenon_Vof != zenon_Vve)
% 0.32/0.61  (zenon_Vpe != zenon_Vve)
% 0.32/0.61  (zenon_Vwf != zenon_Vyb)
% 0.32/0.61  (zenon_Vmg != zenon_Vvc)
% 0.32/0.61  (zenon_Voh != zenon_Vpf)
% 0.32/0.61  (r1 zenon_Vnb zenon_Vqb)
% 0.32/0.61  (zenon_Vld != zenon_Veb)
% 0.32/0.61  (zenon_Vzh != zenon_Vcd)
% 0.32/0.61  (zenon_Vef != zenon_Vmb)
% 0.32/0.61  (r1 zenon_Vph zenon_Vsh)
% 0.32/0.61  (r1 zenon_Vzb zenon_Vcc)
% 0.32/0.61  (zenon_Vqg != zenon_Vmd)
% 0.32/0.61  (zenon_Vpe != zenon_Vyc)
% 0.32/0.61  (zenon_Vgd != zenon_Vyb)
% 0.32/0.61  (zenon_Vjf != zenon_Vwd)
% 0.32/0.61  (zenon_Vae != zenon_Vmb)
% 0.32/0.61  (zenon_Vzh != zenon_Vaf)
% 0.32/0.61  (r1 zenon_Vta zenon_Vwa)
% 0.32/0.61  (zenon_Vke != zenon_Vwd)
% 0.32/0.61  (zenon_Vyg != zenon_Vmd)
% 0.32/0.61  (zenon_Vqd != zenon_Vwd)
% 0.32/0.61  (zenon_Vgd != zenon_Vwd)
% 0.32/0.61  (-. (p1 zenon_Voc))
% 0.32/0.61  (zenon_Vmg != zenon_Vve)
% 0.32/0.61  (r1 zenon_Vde zenon_Vge)
% 0.32/0.61  (zenon_Vef != zenon_Vbe)
% 0.32/0.61  (zenon_Veg != zenon_Vqe)
% 0.32/0.61  (zenon_Veg != zenon_Vsc)
% 0.32/0.61  (zenon_Vae != zenon_Vcd)
% 0.32/0.61  (zenon_Vef != zenon_Vle)
% 0.32/0.61  (zenon_Vfe != zenon_Vmd)
% 0.32/0.61  (zenon_Vzh != zenon_Vmd)
% 0.32/0.61  (zenon_Vig != zenon_Vrd)
% 0.32/0.61  (zenon_Vjf != zenon_Vqb)
% 0.32/0.61  (zenon_Vzh != zenon_Vrd)
% 0.32/0.61  (zenon_Vgd != zenon_Vhd)
% 0.32/0.61  (zenon_Vwf != zenon_Vkc)
% 0.32/0.61  (-. (p2 zenon_Vsf))
% 0.32/0.61  (zenon_Vsh != zenon_Vgc)
% 0.32/0.61  (zenon_Vig != zenon_Vaf)
% 0.32/0.61  (zenon_Vjf != zenon_Vqe)
% 0.32/0.61  (zenon_Vsh != zenon_Vcc)
% 0.32/0.61  (r1 zenon_Vyd zenon_Vbe)
% 0.32/0.61  (zenon_Vzh != zenon_Vqb)
% 0.32/0.61  (-. (p1 zenon_Vff))
% 0.32/0.61  (zenon_Veg != zenon_Vle)
% 0.32/0.61  (zenon_Vze != zenon_Vpf)
% 0.32/0.61  (zenon_Vkh != zenon_Vwa)
% 0.32/0.61  (zenon_Vef != zenon_Vmd)
% 0.32/0.61  (-. (p1 zenon_Veb))
% 0.32/0.61  (-. (p1 zenon_Vbe))
% 0.32/0.61  (zenon_Vxc != zenon_Vkf)
% 0.32/0.61  (zenon_Vue != zenon_Vcc)
% 0.32/0.61  (zenon_Vpe != zenon_Vsc)
% 0.32/0.61  (zenon_Vue != zenon_Vwa)
% 0.32/0.61  (zenon_Vpe != zenon_Vab)
% 0.32/0.61  (zenon_Vqg != zenon_Voc)
% 0.32/0.61  (zenon_Vzh != zenon_Vkf)
% 0.32/0.61  (-. (p1 zenon_Vpf))
% 0.32/0.61  (zenon_Vwf != zenon_Vhd)
% 0.32/0.61  (zenon_Vae != zenon_Vve)
% 0.32/0.61  (zenon_Vmg != zenon_Vcd)
% 0.32/0.61  (zenon_Vke != zenon_Vve)
% 0.32/0.61  (zenon_Vke != zenon_Vmd)
% 0.32/0.61  (zenon_Vqg != zenon_Vmb)
% 0.32/0.61  (r1 zenon_Vne zenon_Vqe)
% 0.32/0.61  (zenon_Vyg != zenon_Vrd)
% 0.32/0.61  (zenon_Voh != zenon_Vib)
% 0.32/0.61  (-. (p2 zenon_Voa))
% 0.32/0.61  (zenon_Vof != zenon_Vmd)
% 0.32/0.61  (zenon_Vzh != zenon_Vmb)
% 0.32/0.61  (r1 Tau_2 zenon_Vzc)
% 0.32/0.61  (r1 Tau_2 zenon_Vdd)
% 0.32/0.61  (zenon_Vef != zenon_Vge)
% 0.32/0.61  (zenon_Vwh != zenon_Vwd)
% 0.32/0.61  (zenon_Vfe != zenon_Vmb)
% 0.32/0.61  (zenon_Vzh != zenon_Vib)
% 0.32/0.61  (zenon_Vba != zenon_Via)
% 0.32/0.61  (p1 zenon_Vqg)
% 0.32/0.61  (zenon_Vkh != zenon_Vhd)
% 0.32/0.61  (zenon_Vwh != zenon_Veb)
% 0.32/0.61  (zenon_Vfe != zenon_Vwa)
% 0.32/0.61  (zenon_Vgh != zenon_Vqb)
% 0.32/0.61  (zenon_Vba != zenon_Voa)
% 0.32/0.61  (p1 zenon_Vyg)
% 0.32/0.61  (zenon_Vae != zenon_Vwd)
% 0.32/0.61  (p1 zenon_Vfe)
% 0.32/0.61  (zenon_Vig != zenon_Vsa)
% 0.32/0.61  (r1 zenon_Vdc zenon_Vgc)
% 0.32/0.61  (zenon_Vgh != zenon_Vsc)
% 0.32/0.61  (zenon_Vch != zenon_Vqe)
% 0.32/0.61  (zenon_Vue != zenon_Vyc)
% 0.32/0.61  (zenon_Vzh != zenon_Vvc)
% 0.32/0.61  (zenon_Vug != zenon_Vrd)
% 0.32/0.61  (zenon_Vue != zenon_Voc)
% 0.32/0.61  (zenon_Vke != zenon_Vrd)
% 0.32/0.61  (zenon_Vpe != zenon_Vvc)
% 0.32/0.61  (zenon_Vwh != zenon_Vsc)
% 0.32/0.61  (r1 zenon_Vhe zenon_Vie)
% 0.32/0.61  (zenon_Vch != zenon_Vcd)
% 0.32/0.61  (zenon_Vzh != zenon_Vgc)
% 0.32/0.61  (r1 zenon_Vpc zenon_Vsc)
% 0.32/0.61  (zenon_Vig != zenon_Vpf)
% 0.32/0.61  (zenon_Vxc != zenon_Vwa)
% 0.32/0.61  (zenon_Vpe != zenon_Vhd)
% 0.32/0.61  (zenon_Vkh != zenon_Vyc)
% 0.32/0.61  (zenon_Vqg != zenon_Vge)
% 0.32/0.61  (zenon_Vbd != zenon_Vff)
% 0.32/0.61  (zenon_Vvd != zenon_Vqb)
% 0.32/0.61  (zenon_Vqg != zenon_Vkc)
% 0.32/0.61  (zenon_Vef != zenon_Voc)
% 0.32/0.61  (zenon_Vkh != zenon_Vsa)
% 0.32/0.61  (zenon_Vvd != zenon_Vaf)
% 0.32/0.61  (zenon_Vef != zenon_Vff)
% 0.32/0.61  (zenon_Vzh != zenon_Veb)
% 0.32/0.61  (r1 zenon_Vcf zenon_Vdf)
% 0.32/0.61  (zenon_Vwh != zenon_Vcd)
% 0.32/0.61  (zenon_Vag != zenon_Vkc)
% 0.32/0.61  (zenon_Vag != zenon_Vff)
% 0.32/0.61  (zenon_Vig != zenon_Vhd)
% 0.32/0.61  (zenon_Vfe != zenon_Vub)
% 0.32/0.61  (zenon_Vfe != zenon_Vve)
% 0.32/0.61  (zenon_Vze != zenon_Vkc)
% 0.32/0.61  (zenon_Vug != zenon_Vmb)
% 0.32/0.61  (zenon_Vag != zenon_Vge)
% 0.32/0.61  (zenon_Vue != zenon_Vwd)
% 0.32/0.61  (zenon_Vyg != zenon_Vkf)
% 0.32/0.61  (zenon_Vue != zenon_Vub)
% 0.32/0.61  (zenon_Vug != zenon_Vsa)
% 0.32/0.61  (zenon_Vxc != zenon_Vbe)
% 0.32/0.61  (zenon_Vue != zenon_Vkf)
% 0.32/0.61  (zenon_Vze != zenon_Veb)
% 0.32/0.61  (zenon_Vyg != zenon_Vvc)
% 0.32/0.61  (-. (p1 zenon_Vsa))
% 0.32/0.61  (zenon_Vag != zenon_Vve)
% 0.32/0.61  (zenon_Vwh != zenon_Vve)
% 0.32/0.61  (p1 zenon_Vmg)
% 0.32/0.61  (zenon_Vgd != zenon_Voc)
% 0.32/0.61  (zenon_Vof != zenon_Vyb)
% 0.32/0.61  (zenon_Vgh != zenon_Vgc)
% 0.32/0.61  (zenon_Vig != zenon_Vqb)
% 0.32/0.61  (zenon_Voh != zenon_Vbe)
% 0.32/0.61  (zenon_Vgh != zenon_Vub)
% 0.32/0.61  (zenon_Vof != zenon_Vge)
% 0.32/0.61  (zenon_Vqd != zenon_Vbe)
% 0.32/0.61  (-. (p1 zenon_Vqb))
% 0.32/0.61  (-. (p1 zenon_Vub))
% 0.32/0.61  (zenon_Vch != zenon_Vqb)
% 0.32/0.61  (zenon_Vue != zenon_Vgc)
% 0.32/0.61  (zenon_Vch != zenon_Vub)
% 0.32/0.61  (zenon_Vqd != zenon_Vsa)
% 0.32/0.61  (zenon_Vyg != zenon_Vcd)
% 0.32/0.61  (zenon_Vqd != zenon_Vqe)
% 0.32/0.61  (r1 zenon_Vhc zenon_Vkc)
% 0.32/0.61  (zenon_Vqd != zenon_Vab)
% 0.32/0.61  (zenon_Vjf != zenon_Voc)
% 0.32/0.61  (zenon_Vug != zenon_Vyb)
% 0.32/0.61  (zenon_Vqg != zenon_Vub)
% 0.32/0.61  (zenon_Vae != zenon_Vwa)
% 0.32/0.61  (zenon_Vzh != zenon_Vwd)
% 0.32/0.61  (zenon_Vag != zenon_Vgc)
% 0.32/0.61  (zenon_Vue != zenon_Vsa)
% 0.32/0.61  (zenon_Vwh != zenon_Vvc)
% 0.32/0.61  (zenon_Vgh != zenon_Vbe)
% 0.32/0.61  (zenon_Vsh != zenon_Vkf)
% 0.32/0.61  (zenon_Vjf != zenon_Vbe)
% 0.32/0.61  (zenon_Vef != zenon_Vwd)
% 0.32/0.61  (zenon_Vyg != zenon_Vbe)
% 0.32/0.61  (zenon_Vqg != zenon_Vwd)
% 0.32/0.61  (zenon_Vzh != zenon_Voc)
% 0.32/0.61  (zenon_Vgh != zenon_Vcc)
% 0.32/0.61  (zenon_Vmg != zenon_Vqe)
% 0.32/0.61  (zenon_Vmg != zenon_Vub)
% 0.32/0.61  (r1 zenon_Vgf zenon_Vlf)
% 0.32/0.61  (zenon_Vwh != zenon_Vkc)
% 0.32/0.61  (zenon_Vld != zenon_Vkc)
% 0.32/0.61  (zenon_Veg != zenon_Vyb)
% 0.32/0.61  (zenon_Vgh != zenon_Vvc)
% 0.32/0.61  (zenon_Vef != zenon_Vve)
% 0.32/0.61  (zenon_Veg != zenon_Vff)
% 0.32/0.61  (zenon_Veg != zenon_Vub)
% 0.32/0.61  (r1 zenon_Vvg zenon_Vyg)
% 0.32/0.61  (zenon_Vch != zenon_Vbe)
% 0.32/0.61  (zenon_Vue != zenon_Vkc)
% 0.32/0.61  (zenon_Vgd != zenon_Vrd)
% 0.32/0.61  (zenon_Vgd != zenon_Vge)
% 0.32/0.61  (zenon_Voh != zenon_Vwa)
% 0.32/0.61  (r1 zenon_Vsd zenon_Vtd)
% 0.32/0.61  (zenon_Vmg != zenon_Voc)
% 0.32/0.61  (zenon_Vke != zenon_Vab)
% 0.32/0.61  (zenon_Vof != zenon_Vrd)
% 0.32/0.61  (zenon_Vyg != zenon_Vaf)
% 0.32/0.61  (zenon_Vqd != zenon_Vge)
% 0.32/0.61  (zenon_Vpe != zenon_Vib)
% 0.32/0.61  (zenon_Vba != zenon_Vsf)
% 0.32/0.61  (zenon_Vgh != zenon_Vle)
% 0.32/0.61  (r1 zenon_Vjd zenon_Vmd)
% 0.32/0.61  (zenon_Voh != zenon_Vgc)
% 0.32/0.61  (zenon_Vvd != zenon_Vwa)
% 0.32/0.61  (r1 zenon_Vjd zenon_Vkd)
% 0.32/0.61  (zenon_Vke != zenon_Vib)
% 0.32/0.61  (-. (p1 zenon_Vgc))
% 0.32/0.61  (zenon_Vyg != zenon_Vge)
% 0.32/0.61  (r1 zenon_Vod zenon_Vpd)
% 0.32/0.61  (zenon_Veg != zenon_Vvc)
% 0.32/0.61  (zenon_Vbd != zenon_Vaf)
% 0.32/0.61  (zenon_Vjf != zenon_Vmb)
% 0.32/0.61  (zenon_Vkh != zenon_Vkc)
% 0.32/0.61  (r1 zenon_Vga zenon_Vha)
% 0.32/0.61  (zenon_Vsh != zenon_Vsc)
% 0.32/0.61  (zenon_Vof != zenon_Voc)
% 0.32/0.61  (zenon_Vyg != zenon_Vib)
% 0.32/0.61  (zenon_Vke != zenon_Vub)
% 0.32/0.61  (r1 zenon_Vie zenon_Vje)
% 0.32/0.61  (zenon_Vgd != zenon_Vle)
% 0.32/0.61  (zenon_Vef != zenon_Vyb)
% 0.32/0.61  (zenon_Vze != zenon_Vge)
% 0.32/0.61  (zenon_Vmg != zenon_Vkc)
% 0.32/0.61  (zenon_Vch != zenon_Vvc)
% 0.32/0.61  (zenon_Vjf != zenon_Vyb)
% 0.32/0.61  (zenon_Vof != zenon_Vff)
% 0.32/0.61  (zenon_Vof != zenon_Vkf)
% 0.32/0.61  (zenon_Vsh != zenon_Vyb)
% 0.32/0.61  (r1 zenon_Vdh zenon_Vgh)
% 0.32/0.61  (zenon_Vof != zenon_Vvc)
% 0.32/0.61  (zenon_Vpe != zenon_Vub)
% 0.32/0.61  (zenon_Voh != zenon_Vsa)
% 0.32/0.61  (zenon_Vgd != zenon_Vpf)
% 0.32/0.61  (zenon_Vgh != zenon_Vff)
% 0.32/0.61  (zenon_Voh != zenon_Vsc)
% 0.32/0.61  (zenon_Vof != zenon_Vqb)
% 0.32/0.61  (zenon_Vxc != zenon_Vyc)
% 0.32/0.61  (p1 zenon_Vef)
% 0.32/0.61  (zenon_Vvd != zenon_Vmd)
% 0.32/0.61  (zenon_Vqd != zenon_Vpf)
% 0.32/0.61  (zenon_Vld != zenon_Vib)
% 0.32/0.61  (zenon_Vjf != zenon_Vge)
% 0.32/0.61  (zenon_Vqg != zenon_Vaf)
% 0.32/0.61  (zenon_Vch != zenon_Vsc)
% 0.32/0.61  (zenon_Vae != zenon_Vaf)
% 0.32/0.61  (zenon_Vgh != zenon_Veb)
% 0.32/0.61  (zenon_Vze != zenon_Vwd)
% 0.32/0.61  (r1 zenon_Vnd zenon_Vsd)
% 0.32/0.61  (zenon_Vgd != zenon_Vkf)
% 0.32/0.61  (zenon_Vue != zenon_Vib)
% 0.32/0.61  (zenon_Vgh != zenon_Vyc)
% 0.32/0.61  (zenon_Vwh != zenon_Vub)
% 0.32/0.61  (-. (p1 zenon_Vcc))
% 0.32/0.61  (zenon_Vae != zenon_Vpf)
% 0.32/0.61  (zenon_Vjf != zenon_Vub)
% 0.32/0.61  (zenon_Vgh != zenon_Voc)
% 0.32/0.61  (zenon_Vze != zenon_Vyb)
% 0.32/0.61  (-. (p3 zenon_Vca))
% 0.32/0.61  (zenon_Vag != zenon_Vmb)
% 0.32/0.61  (zenon_Vag != zenon_Vkf)
% 0.32/0.61  (zenon_Vpe != zenon_Vyb)
% 0.32/0.61  (zenon_Vwh != zenon_Vhd)
% 0.32/0.61  (zenon_Vsh != zenon_Vhd)
% 0.32/0.61  (zenon_Vze != zenon_Vbe)
% 0.32/0.61  (zenon_Vxc != zenon_Vab)
% 0.32/0.61  (r1 zenon_Vlf zenon_Vqf)
% 0.32/0.61  (zenon_Vkh != zenon_Vib)
% 0.32/0.61  (zenon_Vch != zenon_Vmb)
% 0.32/0.61  (zenon_Vzh != zenon_Vwa)
% 0.32/0.61  (zenon_Vug != zenon_Vsc)
% 0.32/0.61  (zenon_Vag != zenon_Vhd)
% 0.32/0.61  (r1 zenon_Vxd zenon_Vce)
% 0.32/0.61  (zenon_Vvd != zenon_Vvc)
% 0.32/0.61  (zenon_Vug != zenon_Vaf)
% 0.32/0.61  (zenon_Vfe != zenon_Vkc)
% 0.32/0.61  (zenon_Vqd != zenon_Vhd)
% 0.32/0.61  (zenon_Vgh != zenon_Vhd)
% 0.32/0.61  (zenon_Vwh != zenon_Vpf)
% 0.32/0.61  (zenon_Vae != zenon_Vsc)
% 0.32/0.61  (zenon_Veg != zenon_Vpf)
% 0.32/0.61  (zenon_Vig != zenon_Vcd)
% 0.32/0.61  (zenon_Vkh != zenon_Vle)
% 0.32/0.61  (zenon_Vld != zenon_Vle)
% 0.32/0.61  (-. (p1 zenon_Vwa))
% 0.32/0.61  (zenon_Vwh != zenon_Vbe)
% 0.32/0.61  (zenon_Vqd != zenon_Voc)
% 0.32/0.61  (zenon_Vfe != zenon_Vcc)
% 0.32/0.61  (r1 Tau_1 zenon_Vwc)
% 0.32/0.61  (zenon_Vbd != zenon_Vvc)
% 0.32/0.61  (zenon_Vjf != zenon_Vcd)
% 0.32/0.61  (zenon_Vmg != zenon_Vle)
% 0.32/0.61  (zenon_Vfe != zenon_Vwd)
% 0.32/0.61  (zenon_Vag != zenon_Vcd)
% 0.32/0.61  (zenon_Vig != zenon_Vab)
% 0.32/0.61  (zenon_Vxc != zenon_Vvc)
% 0.32/0.61  (zenon_Vld != zenon_Vgc)
% 0.32/0.61  (zenon_Voh != zenon_Vwd)
% 0.32/0.61  (zenon_Vqg != zenon_Vgc)
% 0.32/0.61  (zenon_Veg != zenon_Vkf)
% 0.32/0.61  (zenon_Vmg != zenon_Vkf)
% 0.32/0.61  (zenon_Vkh != zenon_Veb)
% 0.32/0.61  *)
% 0.32/0.61  (* NO-PROOF *)
% 0.32/0.61  % SZS status GaveUp
% 0.32/0.61  Number of rewrites on terms: 0
% 0.32/0.61  Number of rewrites on props: 0
% 0.32/0.61  nodes searched: 1373
% 0.32/0.61  max branch formulas: 1533
% 0.32/0.61  proof nodes created: 0
% 0.32/0.61  formulas created: 7456
% 0.32/0.61  
%------------------------------------------------------------------------------