↑ 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.010 : TPTP v9.3.1. Released v4.0.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : run_zenon_modulo %d %s

% Computer : n019.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.30s 0.62s
% Output   : None 
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02  % Problem  : LCL652+1.010 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.02  % Command  : run_zenon_modulo %d %s
% 0.08/0.35  % Computer : n019.cluster.edu
% 0.08/0.35  % Model    : x86_64 x86_64
% 0.08/0.35  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35  % Memory   : 8046.5625MB
% 0.08/0.35  % OS       : Linux 6.8.0-71-generic
% 0.08/0.35  % CPULimit : 300
% 0.08/0.35  % WCLimit  : 300
% 0.08/0.35  % DateTime : Fri Sep  4 19:53:38 UTC 2026
% 0.08/0.35  % CPUTime  : 
% 0.30/0.62  Zenon error: exhausted search space without finding a proof
% 0.30/0.62  (* Current branch:
% 0.30/0.62  (zenon_Vwh != zenon_Vrd)
% 0.30/0.62  (zenon_Vqe != zenon_Vya)
% 0.30/0.62  (zenon_Vgh != zenon_Vde)
% 0.30/0.62  (zenon_Vef != zenon_Vfb)
% 0.30/0.62  (zenon_Vug != zenon_Vhe)
% 0.30/0.62  (zenon_Vtf != zenon_Vka)
% 0.30/0.62  (p1 zenon_Vgh)
% 0.30/0.62  (zenon_Vig != zenon_Vda)
% 0.30/0.62  (zenon_Vze != zenon_Voe)
% 0.30/0.62  (zenon_Vof != zenon_Vhe)
% 0.30/0.62  (zenon_Vwh != zenon_Vda)
% 0.30/0.62  (zenon_Vtf != zenon_Vrd)
% 0.30/0.62  (zenon_Vgh != zenon_Vvd)
% 0.30/0.62  (zenon_Vch != zenon_Vjd)
% 0.30/0.62  (zenon_Vwh != zenon_Vra)
% 0.30/0.62  (zenon_Vtf != zenon_Vhe)
% 0.30/0.62  (r1 zenon_Vwc zenon_Vxc)
% 0.30/0.62  (zenon_Vug != zenon_Vfd)
% 0.30/0.62  (zenon_Vue != zenon_Vde)
% 0.30/0.62  (r1 zenon_Vrf zenon_Vsf)
% 0.30/0.62  (zenon_Voh != zenon_Vjg)
% 0.30/0.62  (zenon_Vig != zenon_Vra)
% 0.30/0.62  (zenon_Vch != zenon_Veg)
% 0.30/0.62  (zenon_Voh != zenon_Vfb)
% 0.30/0.62  (zenon_Vqg != zenon_Vvd)
% 0.30/0.62  (zenon_Vue != zenon_Vnd)
% 0.30/0.62  (zenon_Vch != zenon_Vhe)
% 0.30/0.62  (zenon_Vef != zenon_Vzf)
% 0.30/0.62  (zenon_Vze != zenon_Vfb)
% 0.30/0.62  (zenon_Vkh != zenon_Vjd)
% 0.30/0.62  (zenon_Voh != zenon_Vle)
% 0.30/0.62  (p1 zenon_Vkh)
% 0.30/0.62  (zenon_Vyg != zenon_Vjg)
% 0.30/0.62  (zenon_Vyg != zenon_Vff)
% 0.30/0.62  (zenon_Vyg != zenon_Vpf)
% 0.30/0.62  (zenon_Vyg != zenon_Vw)
% 0.30/0.62  (zenon_Vjf != zenon_Vle)
% 0.30/0.62  (zenon_Voh != zenon_Vw)
% 0.30/0.62  (zenon_Vef != zenon_Vjd)
% 0.30/0.62  (zenon_Vze != zenon_Vvd)
% 0.30/0.62  (p1 zenon_Vue)
% 0.30/0.62  (zenon_Vzh != zenon_Vq)
% 0.30/0.62  (zenon_Vig != zenon_Vkf)
% 0.30/0.62  (zenon_Vch != zenon_Vtb)
% 0.30/0.62  (zenon_Vyf != zenon_Vde)
% 0.30/0.62  (zenon_Vsh != zenon_Vde)
% 0.30/0.62  (zenon_Vjf != zenon_Vve)
% 0.30/0.62  (zenon_Vyf != zenon_Vvd)
% 0.30/0.62  (p1 zenon_Vze)
% 0.30/0.62  (zenon_Vze != zenon_Vff)
% 0.30/0.62  (-. (p1 zenon_Vka))
% 0.30/0.62  (zenon_Vqg != zenon_Vw)
% 0.30/0.62  (r1 zenon_X6 zenon_Voe)
% 0.30/0.62  (zenon_Vyf != zenon_Vkf)
% 0.30/0.62  (zenon_Vwh != zenon_Vq)
% 0.30/0.62  (zenon_Vqe != zenon_Vre)
% 0.30/0.62  (zenon_Vze != zenon_Vq)
% 0.30/0.62  (zenon_Voh != zenon_Vre)
% 0.30/0.62  (zenon_Vef != zenon_Vfd)
% 0.30/0.62  (zenon_Vof != zenon_Vjd)
% 0.30/0.62  (zenon_Vyg != zenon_Vve)
% 0.30/0.62  (r1 zenon_Vie zenon_Vle)
% 0.30/0.62  (r1 zenon_Vvf zenon_Vag)
% 0.30/0.62  (zenon_Vue != zenon_Vfb)
% 0.30/0.62  (zenon_Vgh != zenon_Vmb)
% 0.30/0.62  (zenon_Vyg != zenon_Vac)
% 0.30/0.62  (zenon_Vjf != zenon_Vvd)
% 0.30/0.62  (zenon_Vug != zenon_Vre)
% 0.30/0.62  (zenon_Vwh != zenon_Vle)
% 0.30/0.62  (zenon_Vjf != zenon_Vkf)
% 0.30/0.62  (r1 zenon_Vbf zenon_Vcf)
% 0.30/0.62  (zenon_Vug != zenon_Vzf)
% 0.30/0.62  (zenon_Vtf != zenon_Vjg)
% 0.30/0.62  (zenon_Vue != zenon_Vq)
% 0.30/0.62  (zenon_Vue != zenon_Vle)
% 0.30/0.62  (zenon_Vwh != zenon_Vaf)
% 0.30/0.62  (zenon_Vue != zenon_Veg)
% 0.30/0.62  (zenon_Vze != zenon_Vjd)
% 0.30/0.62  (zenon_Vig != zenon_Vac)
% 0.30/0.62  (zenon_Vug != zenon_Vzd)
% 0.30/0.62  (r1 zenon_Vy zenon_Vca)
% 0.30/0.62  (zenon_Vze != zenon_Vmb)
% 0.30/0.62  (zenon_Vue != zenon_Vaf)
% 0.30/0.62  (zenon_Vue != zenon_Vve)
% 0.30/0.62  (r1 zenon_Vqf zenon_Vvf)
% 0.30/0.62  (zenon_Vkh != zenon_Vve)
% 0.30/0.62  (zenon_Vtf != zenon_Vq)
% 0.30/0.62  (zenon_Vzh != zenon_Vre)
% 0.30/0.62  (zenon_Vkh != zenon_Vjg)
% 0.30/0.62  (zenon_Vjf != zenon_Vaf)
% 0.30/0.62  (zenon_Vjf != zenon_Vda)
% 0.30/0.62  (r1 zenon_Vlh zenon_Voh)
% 0.30/0.62  (zenon_Vqg != zenon_Vjg)
% 0.30/0.62  (zenon_Vkh != zenon_Vre)
% 0.30/0.62  (zenon_Vig != zenon_Vle)
% 0.30/0.62  (r1 zenon_X7 zenon_Vzh)
% 0.30/0.62  (zenon_Vug != zenon_Vff)
% 0.30/0.62  (zenon_Vwh != zenon_Vkf)
% 0.30/0.62  (r1 zenon_Vxe zenon_Vaf)
% 0.30/0.62  (zenon_Vch != zenon_Vjg)
% 0.30/0.62  (zenon_Vug != zenon_Vle)
% 0.30/0.62  (-. (p1 zenon_Vtb))
% 0.30/0.62  (-. (p1 zenon_Vvd))
% 0.30/0.62  (zenon_Voh != zenon_Vaf)
% 0.30/0.62  (zenon_Vof != zenon_Vw)
% 0.30/0.62  (zenon_Vyf != zenon_Vfd)
% 0.30/0.62  (zenon_Vig != zenon_Vzf)
% 0.30/0.62  (zenon_Vkh != zenon_Vnd)
% 0.30/0.62  (zenon_Vsh != zenon_Vzd)
% 0.30/0.62  (zenon_Vqe != zenon_Vff)
% 0.30/0.62  (zenon_Vwc != zenon_Vqc)
% 0.30/0.62  (zenon_Vof != zenon_Vac)
% 0.30/0.62  (r1 zenon_Vkd zenon_Vnd)
% 0.30/0.62  (zenon_Vgh != zenon_Vaf)
% 0.30/0.62  (zenon_Vkh != zenon_Vuf)
% 0.30/0.62  (r1 zenon_Vse zenon_Vte)
% 0.30/0.62  (r1 zenon_Vlf zenon_Vmf)
% 0.30/0.62  (zenon_Vef != zenon_Vuf)
% 0.30/0.62  (zenon_Vgh != zenon_Vw)
% 0.30/0.62  (zenon_Vyf != zenon_Vya)
% 0.30/0.62  (zenon_Vig != zenon_Vzd)
% 0.30/0.62  (zenon_Vzh != zenon_Vac)
% 0.30/0.62  (zenon_Voh != zenon_Vve)
% 0.30/0.62  (zenon_Vyf != zenon_Vle)
% 0.30/0.62  (zenon_Vze != zenon_Vle)
% 0.30/0.62  (zenon_Vdc != zenon_Vqc)
% 0.30/0.62  (zenon_Vyg != zenon_Vnd)
% 0.30/0.62  (zenon_Vtf != zenon_Vaf)
% 0.30/0.62  (p1 zenon_Vch)
% 0.30/0.62  (zenon_Vqg != zenon_Vq)
% 0.30/0.62  (r1 zenon_Vab zenon_Veb)
% 0.30/0.62  (-. (p1 zenon_Vjd))
% 0.30/0.62  (zenon_Vze != zenon_Vrd)
% 0.30/0.62  (r1 zenon_Vbc zenon_Vpc)
% 0.30/0.62  (r1 zenon_Vxe zenon_Vye)
% 0.30/0.62  (zenon_Vch != zenon_Vfb)
% 0.30/0.62  (r1 zenon_Vbg zenon_Vcg)
% 0.30/0.62  (zenon_Vch != zenon_Vaf)
% 0.30/0.62  (zenon_Vwh != zenon_Vw)
% 0.30/0.62  (zenon_Vof != zenon_Vya)
% 0.30/0.62  (zenon_Vdg != zenon_Vfd)
% 0.30/0.62  (zenon_Vkh != zenon_Vaf)
% 0.30/0.62  (p1 zenon_Vzh)
% 0.30/0.62  (zenon_Vze != zenon_Vkf)
% 0.30/0.62  (zenon_Vgh != zenon_Vda)
% 0.30/0.62  (zenon_Vqg != zenon_Vtb)
% 0.30/0.62  (zenon_Vyg != zenon_Vhe)
% 0.30/0.62  (zenon_Vue != zenon_Voe)
% 0.30/0.62  (-. (p1 zenon_Vaf))
% 0.30/0.62  (zenon_Vsh != zenon_Vka)
% 0.30/0.62  (zenon_Vgh != zenon_Vrd)
% 0.30/0.62  (zenon_Vug != zenon_Vda)
% 0.30/0.62  (zenon_Vgh != zenon_Veg)
% 0.30/0.62  (zenon_Voh != zenon_Vmb)
% 0.30/0.62  (zenon_Vof != zenon_Vuf)
% 0.30/0.62  (zenon_Vue != zenon_Vre)
% 0.30/0.62  (r1 zenon_X4 zenon_Vp)
% 0.30/0.62  (zenon_Vqe != zenon_Vfb)
% 0.30/0.62  (zenon_Vch != zenon_Vpf)
% 0.30/0.62  (zenon_Vug != zenon_Vuf)
% 0.30/0.62  (zenon_Vjf != zenon_Vw)
% 0.30/0.62  (zenon_Vzh != zenon_Vw)
% 0.30/0.62  (zenon_Vzh != zenon_Vuf)
% 0.30/0.62  (zenon_Vze != zenon_Vac)
% 0.30/0.62  (r1 zenon_Vhb zenon_Vlb)
% 0.30/0.62  (zenon_Vue != zenon_Vya)
% 0.30/0.62  (zenon_Vdg != zenon_Vaf)
% 0.30/0.62  (zenon_Vsh != zenon_Vjd)
% 0.30/0.62  (zenon_Vwc != zenon_Vkc)
% 0.30/0.62  (r1 Tau_1 zenon_Vre)
% 0.30/0.62  (zenon_Vig != zenon_Vvd)
% 0.30/0.62  (zenon_Vgh != zenon_Vve)
% 0.30/0.62  (zenon_Vzh != zenon_Vve)
% 0.30/0.62  (zenon_Vch != zenon_Vre)
% 0.30/0.62  (zenon_Vqg != zenon_Vve)
% 0.30/0.62  (zenon_Vqe != zenon_Vda)
% 0.30/0.62  (zenon_Vyg != zenon_Vya)
% 0.30/0.62  (zenon_Voh != zenon_Vff)
% 0.30/0.62  (zenon_Vjf != zenon_Vjd)
% 0.30/0.62  (r1 zenon_Vwf zenon_Vxf)
% 0.30/0.62  (zenon_Vgh != zenon_Vzf)
% 0.30/0.62  (zenon_Voh != zenon_Vjd)
% 0.30/0.62  (zenon_Vqg != zenon_Vre)
% 0.30/0.62  (zenon_Vef != zenon_Vkf)
% 0.30/0.62  (r1 zenon_Vcf zenon_Vff)
% 0.30/0.62  (zenon_Vzh != zenon_Vda)
% 0.30/0.62  (zenon_Vjf != zenon_Vzd)
% 0.30/0.62  (zenon_Vsh != zenon_Vpf)
% 0.30/0.62  (zenon_Vjf != zenon_Vde)
% 0.30/0.62  (-. (p1 zenon_Vya))
% 0.30/0.62  (p1 zenon_Vsh)
% 0.30/0.62  (zenon_Vof != zenon_Vzf)
% 0.30/0.62  (p1 zenon_Vyf)
% 0.30/0.62  (zenon_Vdg != zenon_Vhe)
% 0.30/0.62  (zenon_Vue != zenon_Vac)
% 0.30/0.62  (zenon_Vdg != zenon_Vde)
% 0.30/0.62  (zenon_Vig != zenon_Vq)
% 0.30/0.62  (zenon_Vgh != zenon_Vpf)
% 0.30/0.62  (zenon_Vtf != zenon_Vmb)
% 0.30/0.62  (zenon_Vsh != zenon_Vff)
% 0.30/0.62  (r1 zenon_Vod zenon_Vrd)
% 0.30/0.62  (zenon_Vzh != zenon_Vjd)
% 0.30/0.62  (zenon_Vdg != zenon_Vfb)
% 0.30/0.62  (zenon_Vef != zenon_Vrd)
% 0.30/0.62  (zenon_Vug != zenon_Vac)
% 0.30/0.62  (zenon_Vug != zenon_Vpf)
% 0.30/0.62  (-. (p1 zenon_Vle))
% 0.30/0.62  (zenon_Vyg != zenon_Vvd)
% 0.30/0.62  (r1 zenon_Vng zenon_Vqg)
% 0.30/0.62  (zenon_Vdc != zenon_Vkc)
% 0.30/0.62  (zenon_Vyf != zenon_Veg)
% 0.30/0.62  (zenon_Voh != zenon_Vzf)
% 0.30/0.62  (zenon_Vkh != zenon_Vw)
% 0.30/0.62  (zenon_Vch != zenon_Vw)
% 0.30/0.62  (r1 zenon_Vr zenon_Vv)
% 0.30/0.62  (zenon_Vze != zenon_Vjg)
% 0.30/0.62  (zenon_Voh != zenon_Vhe)
% 0.30/0.62  (-. (p1 zenon_Vac))
% 0.30/0.62  (zenon_Vof != zenon_Vzd)
% 0.30/0.62  (zenon_Vyf != zenon_Vw)
% 0.30/0.62  (zenon_Vue != zenon_Vtb)
% 0.30/0.62  (-. (p1 zenon_Vkf))
% 0.30/0.62  (zenon_Vzh != zenon_Vzd)
% 0.30/0.62  (zenon_Vig != zenon_Vde)
% 0.30/0.62  (zenon_Vkh != zenon_Vkf)
% 0.30/0.62  (zenon_Vyf != zenon_Vda)
% 0.30/0.62  (zenon_Vze != zenon_Vve)
% 0.30/0.62  (r1 zenon_Vzg zenon_Vch)
% 0.30/0.62  (zenon_Vue != zenon_Vra)
% 0.30/0.62  (r1 Tau_2 zenon_Vse)
% 0.30/0.62  (r1 Tau_2 zenon_Vwe)
% 0.30/0.62  (zenon_Vtf != zenon_Vnd)
% 0.30/0.62  (zenon_Voh != zenon_Vrd)
% 0.30/0.62  (zenon_Vch != zenon_Vkf)
% 0.30/0.62  (zenon_Vof != zenon_Vpf)
% 0.30/0.62  (p1 zenon_Vwh)
% 0.30/0.62  (zenon_Vch != zenon_Vff)
% 0.30/0.62  (zenon_Vkh != zenon_Veg)
% 0.30/0.62  (zenon_Vdc != zenon_Vbd)
% 0.30/0.62  (-. (p1 zenon_Vuf))
% 0.30/0.62  (r1 zenon_Vrg zenon_Vug)
% 0.30/0.62  (zenon_Vqe != zenon_Vmb)
% 0.30/0.62  (zenon_Vof != zenon_Vjg)
% 0.30/0.62  (zenon_Vqg != zenon_Vfb)
% 0.30/0.62  (zenon_Vsh != zenon_Vle)
% 0.30/0.62  (zenon_Vsh != zenon_Vq)
% 0.30/0.62  (zenon_Vof != zenon_Vnd)
% 0.30/0.62  (zenon_Vyf != zenon_Vre)
% 0.30/0.62  (-. (p2 zenon_Vmg))
% 0.30/0.62  (zenon_Vef != zenon_Vpf)
% 0.30/0.62  (zenon_Vsh != zenon_Vre)
% 0.30/0.62  (zenon_Vug != zenon_Vra)
% 0.30/0.62  (zenon_Vtf != zenon_Vw)
% 0.30/0.62  (zenon_Vug != zenon_Vya)
% 0.30/0.62  (zenon_Vue != zenon_Vmb)
% 0.30/0.62  (p1 zenon_Vig)
% 0.30/0.62  (zenon_Vig != zenon_Vmb)
% 0.30/0.62  (zenon_Vqe != zenon_Vle)
% 0.30/0.62  (r1 zenon_Vgf zenon_Vhf)
% 0.30/0.62  (zenon_Vef != zenon_Vw)
% 0.30/0.62  (-. (p1 zenon_Vda))
% 0.30/0.62  (zenon_Vue != zenon_Vpf)
% 0.30/0.62  (zenon_Vwh != zenon_Vac)
% 0.30/0.62  (zenon_Vqg != zenon_Vrd)
% 0.30/0.62  (zenon_Vze != zenon_Veg)
% 0.30/0.62  (zenon_Vqg != zenon_Vle)
% 0.30/0.62  (-. (p2 zenon_Vbd))
% 0.30/0.62  (-. (p1 zenon_Vhe))
% 0.30/0.62  (zenon_Vjf != zenon_Vra)
% 0.30/0.62  (r1 zenon_Vae zenon_Vde)
% 0.30/0.62  (zenon_Vze != zenon_Vaf)
% 0.30/0.62  (zenon_Vef != zenon_Vzd)
% 0.30/0.62  (-. (p1 zenon_Vrd))
% 0.30/0.62  (zenon_Vue != zenon_Vzd)
% 0.30/0.62  (zenon_Vjf != zenon_Vjg)
% 0.30/0.62  (zenon_Vyf != zenon_Vve)
% 0.30/0.62  (zenon_Vef != zenon_Vka)
% 0.30/0.62  (-. (p1 zenon_Veg))
% 0.30/0.62  (zenon_Vqe != zenon_Vrd)
% 0.30/0.62  (zenon_Vqg != zenon_Vhe)
% 0.30/0.62  (zenon_Vzh != zenon_Vpf)
% 0.30/0.62  (zenon_Vkh != zenon_Vpf)
% 0.30/0.62  (zenon_Vtf != zenon_Vjd)
% 0.30/0.62  (zenon_Vug != zenon_Vkf)
% 0.30/0.62  (zenon_Vtf != zenon_Vuf)
% 0.30/0.62  (zenon_Vch != zenon_Vle)
% 0.30/0.62  (zenon_Vch != zenon_Vuf)
% 0.30/0.62  (zenon_Vsh != zenon_Vw)
% 0.30/0.62  (zenon_Vof != zenon_Vaf)
% 0.30/0.62  (zenon_Vdg != zenon_Vq)
% 0.30/0.62  (-. (p1 zenon_Vnd))
% 0.30/0.62  (zenon_Vug != zenon_Vq)
% 0.30/0.62  (zenon_Vqg != zenon_Voe)
% 0.30/0.62  (zenon_Vsh != zenon_Vya)
% 0.30/0.62  (zenon_Vqe != zenon_Vhe)
% 0.30/0.62  (r1 zenon_Vfa zenon_Vja)
% 0.30/0.62  (zenon_Vsh != zenon_Vrd)
% 0.30/0.62  (zenon_Vch != zenon_Vde)
% 0.30/0.62  (r1 zenon_Vfg zenon_Vkg)
% 0.30/0.62  (zenon_Vkh != zenon_Vka)
% 0.30/0.62  (zenon_Vqe != zenon_Vzf)
% 0.30/0.62  (zenon_Vjf != zenon_Vka)
% 0.30/0.62  (zenon_Vdg != zenon_Voe)
% 0.30/0.62  (zenon_Vch != zenon_Vzd)
% 0.30/0.62  (zenon_Vyg != zenon_Vjd)
% 0.30/0.62  (zenon_Vef != zenon_Vre)
% 0.30/0.62  (zenon_Vsh != zenon_Vhe)
% 0.30/0.62  (-. (p1 zenon_Vfd))
% 0.30/0.62  (zenon_Voh != zenon_Vvd)
% 0.30/0.62  (zenon_Vkh != zenon_Vq)
% 0.30/0.62  (r1 zenon_Vbf zenon_Vgf)
% 0.30/0.62  (zenon_Vug != zenon_Vjd)
% 0.30/0.62  (zenon_Vef != zenon_Vtb)
% 0.30/0.62  (zenon_Vig != zenon_Vfd)
% 0.30/0.62  (zenon_Vze != zenon_Vda)
% 0.30/0.62  (-. (p1 zenon_Vre))
% 0.30/0.62  (r1 zenon_Vbg zenon_Veg)
% 0.30/0.62  (r1 zenon_Vag zenon_Vfg)
% 0.30/0.62  (zenon_Vug != zenon_Vw)
% 0.30/0.62  (r1 zenon_Vmf zenon_Vpf)
% 0.30/0.62  (zenon_Vof != zenon_Vfd)
% 0.30/0.62  (zenon_Vug != zenon_Vve)
% 0.30/0.62  (zenon_Vze != zenon_Vka)
% 0.30/0.62  (r1 zenon_Vfg zenon_Vgg)
% 0.30/0.62  (r1 zenon_Vma zenon_Vqa)
% 0.30/0.62  (zenon_Vwh != zenon_Vjg)
% 0.30/0.62  (zenon_Vze != zenon_Vya)
% 0.30/0.62  (zenon_Vwh != zenon_Vya)
% 0.30/0.62  (zenon_Vqg != zenon_Vff)
% 0.30/0.62  (zenon_Vgh != zenon_Vka)
% 0.30/0.62  (zenon_Vyf != zenon_Voe)
% 0.30/0.62  (zenon_Vwc != zenon_Vbd)
% 0.30/0.62  (zenon_Vdg != zenon_Vzd)
% 0.30/0.62  (zenon_Vsh != zenon_Vzf)
% 0.30/0.62  (zenon_Vyg != zenon_Vka)
% 0.30/0.62  (r1 zenon_Vmf zenon_Vnf)
% 0.30/0.62  (zenon_Vyf != zenon_Vpf)
% 0.30/0.62  (zenon_Vyf != zenon_Vnd)
% 0.30/0.62  (zenon_Vtf != zenon_Vzd)
% 0.30/0.62  (zenon_Vwh != zenon_Vvd)
% 0.30/0.62  (zenon_Vyg != zenon_Vra)
% 0.30/0.62  (zenon_Vjf != zenon_Vpf)
% 0.30/0.62  (zenon_Vyg != zenon_Vre)
% 0.30/0.62  (zenon_Vqg != zenon_Vya)
% 0.30/0.62  (zenon_Vdg != zenon_Vtb)
% 0.30/0.62  (-. (p1 zenon_Vq))
% 0.30/0.62  (zenon_Vyf != zenon_Vtb)
% 0.30/0.62  (zenon_Vyg != zenon_Vde)
% 0.30/0.62  (zenon_Vqg != zenon_Vfd)
% 0.30/0.62  (zenon_Vkh != zenon_Vhe)
% 0.30/0.62  (zenon_Vqe != zenon_Vw)
% 0.30/0.62  (zenon_Vch != zenon_Vrd)
% 0.30/0.62  (-. (p1 zenon_Vzd))
% 0.30/0.62  (zenon_Vwh != zenon_Vjd)
% 0.30/0.62  (r1 zenon_Vhf zenon_Vif)
% 0.30/0.62  (zenon_Vqg != zenon_Vra)
% 0.30/0.62  (zenon_Vdg != zenon_Vda)
% 0.30/0.62  (zenon_Vwh != zenon_Vde)
% 0.30/0.62  (zenon_Vdg != zenon_Vmb)
% 0.30/0.62  (zenon_Vzh != zenon_Vjg)
% 0.30/0.62  (zenon_Vue != zenon_Vka)
% 0.30/0.62  (zenon_Vue != zenon_Vrd)
% 0.30/0.62  (zenon_Vch != zenon_Voe)
% 0.30/0.62  (zenon_Vtf != zenon_Vda)
% 0.30/0.62  (zenon_Vqe != zenon_Vkf)
% 0.30/0.62  (zenon_Vue != zenon_Vjd)
% 0.30/0.62  (zenon_Vqg != zenon_Vuf)
% 0.30/0.62  (zenon_Vyg != zenon_Voe)
% 0.30/0.62  (zenon_Vyf != zenon_Vaf)
% 0.30/0.62  (zenon_Vig != zenon_Vfb)
% 0.30/0.62  (zenon_Vug != zenon_Vde)
% 0.30/0.62  (zenon_Vgh != zenon_Vq)
% 0.30/0.62  (zenon_Vch != zenon_Vq)
% 0.30/0.62  (r1 zenon_Vhf zenon_Vkf)
% 0.30/0.62  (zenon_Vze != zenon_Vde)
% 0.30/0.62  (zenon_Vzh != zenon_Vle)
% 0.30/0.62  (zenon_Vig != zenon_Vve)
% 0.30/0.62  (zenon_Vze != zenon_Vzd)
% 0.30/0.62  (r1 Tau_1 zenon_Vpe)
% 0.30/0.62  (r1 zenon_Vrf zenon_Vuf)
% 0.30/0.62  (zenon_Vkh != zenon_Voe)
% 0.30/0.62  (zenon_Vof != zenon_Vle)
% 0.30/0.62  (r1 zenon_Vse zenon_Vve)
% 0.30/0.62  (zenon_Vkh != zenon_Vac)
% 0.30/0.62  (zenon_Vof != zenon_Vre)
% 0.30/0.62  (p1 zenon_Voh)
% 0.30/0.62  (zenon_Vug != zenon_Vnd)
% 0.30/0.62  (zenon_Vwh != zenon_Vka)
% 0.30/0.62  (r1 zenon_Vgg zenon_Vhg)
% 0.30/0.62  (zenon_Vtf != zenon_Vzf)
% 0.30/0.62  (zenon_Voh != zenon_Vra)
% 0.30/0.62  (zenon_Vdg != zenon_Vvd)
% 0.30/0.62  (zenon_Vug != zenon_Veg)
% 0.30/0.62  (zenon_Vsh != zenon_Vra)
% 0.30/0.62  (zenon_Vgh != zenon_Vfb)
% 0.30/0.62  (r1 zenon_Vwd zenon_Vzd)
% 0.30/0.62  (zenon_Vjf != zenon_Vff)
% 0.30/0.62  (zenon_Vof != zenon_Vka)
% 0.30/0.62  (zenon_Vqe != zenon_Vve)
% 0.30/0.62  (zenon_Vig != zenon_Vw)
% 0.30/0.62  (-. (p1 zenon_Vve))
% 0.30/0.62  (zenon_Vze != zenon_Vfd)
% 0.30/0.62  (r1 zenon_Vdc zenon_Vec)
% 0.30/0.62  (p1 zenon_Vug)
% 0.30/0.62  (zenon_Vyg != zenon_Vle)
% 0.30/0.62  (zenon_Vyf != zenon_Vka)
% 0.30/0.62  (zenon_Vof != zenon_Vmb)
% 0.30/0.62  (zenon_Vch != zenon_Vvd)
% 0.30/0.62  (r1 zenon_Vob zenon_Vsb)
% 0.30/0.62  (zenon_Vkh != zenon_Vff)
% 0.30/0.62  (zenon_Vdg != zenon_Vac)
% 0.30/0.62  (zenon_Vtf != zenon_Vtb)
% 0.30/0.62  (zenon_Vkh != zenon_Vrd)
% 0.30/0.62  (zenon_Vyg != zenon_Vzd)
% 0.30/0.62  (zenon_Vkh != zenon_Vzf)
% 0.30/0.62  (zenon_Vch != zenon_Vda)
% 0.30/0.62  (zenon_Vyg != zenon_Vtb)
% 0.30/0.62  (zenon_Vzh != zenon_Vff)
% 0.30/0.62  (zenon_Vqg != zenon_Vpf)
% 0.30/0.62  (zenon_Vig != zenon_Vuf)
% 0.30/0.62  (zenon_Vkh != zenon_Vmb)
% 0.30/0.62  (-. (p1 zenon_Vzf))
% 0.30/0.62  (zenon_Vef != zenon_Voe)
% 0.30/0.62  (r1 Tau_0 Tau_1)
% 0.30/0.62  (zenon_Vdg != zenon_Vkf)
% 0.30/0.62  (zenon_Vof != zenon_Voe)
% 0.30/0.62  (zenon_Vtf != zenon_Vya)
% 0.30/0.62  (zenon_Vgh != zenon_Voe)
% 0.30/0.62  (zenon_Vjf != zenon_Vrd)
% 0.30/0.62  (zenon_Vqe != zenon_Vra)
% 0.30/0.62  (zenon_Vef != zenon_Vac)
% 0.30/0.62  (r1 zenon_Vcc zenon_Vdc)
% 0.30/0.62  (zenon_Vue != zenon_Vjg)
% 0.30/0.62  (zenon_Vtf != zenon_Vkf)
% 0.30/0.62  (zenon_Vyf != zenon_Vjd)
% 0.30/0.62  (zenon_Vdg != zenon_Vle)
% 0.30/0.62  (r1 zenon_Vth zenon_Vwh)
% 0.30/0.62  (zenon_Vyf != zenon_Vac)
% 0.30/0.62  (zenon_Vjf != zenon_Vnd)
% 0.30/0.62  (zenon_Vdg != zenon_Vrd)
% 0.30/0.62  (zenon_Vqe != zenon_Vka)
% 0.30/0.62  (zenon_Vdg != zenon_Veg)
% 0.30/0.62  (zenon_Vtf != zenon_Vpf)
% 0.30/0.62  (zenon_Voh != zenon_Vuf)
% 0.30/0.62  (zenon_Vue != zenon_Vw)
% 0.30/0.62  (-. (p1 zenon_Vfb))
% 0.30/0.62  (zenon_Vqe != zenon_Vnd)
% 0.30/0.62  (zenon_Vwh != zenon_Vmb)
% 0.30/0.62  (zenon_Vch != zenon_Vve)
% 0.30/0.62  (zenon_Vze != zenon_Vre)
% 0.30/0.62  (zenon_Voh != zenon_Vya)
% 0.30/0.62  (r1 zenon_Vee zenon_Vhe)
% 0.30/0.62  (zenon_Vwh != zenon_Vfd)
% 0.30/0.62  (-. (p1 zenon_Voe))
% 0.30/0.62  (zenon_Vqg != zenon_Vkf)
% 0.30/0.62  (zenon_Vze != zenon_Vw)
% 0.30/0.62  (zenon_Vze != zenon_Vhe)
% 0.30/0.62  (zenon_Vug != zenon_Vtb)
% 0.30/0.62  (zenon_Vue != zenon_Vfd)
% 0.30/0.62  (zenon_Vzh != zenon_Vhe)
% 0.30/0.62  (-. (p2 zenon_Vkc))
% 0.30/0.62  (zenon_Vig != zenon_Vff)
% 0.30/0.62  (zenon_Vqe != zenon_Vq)
% 0.30/0.62  (zenon_Vyf != zenon_Vhe)
% 0.30/0.62  (p1 zenon_Vjf)
% 0.30/0.62  (zenon_Vig != zenon_Vjg)
% 0.30/0.62  (zenon_Vwc != zenon_Vmg)
% 0.30/0.62  (zenon_Vzh != zenon_Vka)
% 0.30/0.62  (zenon_Vdg != zenon_Vka)
% 0.30/0.62  (zenon_Vch != zenon_Vnd)
% 0.30/0.62  (zenon_Vjf != zenon_Vya)
% 0.30/0.62  (zenon_Vyf != zenon_Vuf)
% 0.30/0.62  (r1 zenon_Vic zenon_Vjc)
% 0.30/0.62  (zenon_Vsh != zenon_Vaf)
% 0.30/0.62  (zenon_Vjf != zenon_Vhe)
% 0.30/0.62  (r1 zenon_Vhh zenon_Vkh)
% 0.30/0.62  (zenon_Vwh != zenon_Vzf)
% 0.30/0.62  (zenon_Vkh != zenon_Vvd)
% 0.30/0.62  (zenon_Vig != zenon_Vtb)
% 0.30/0.62  (zenon_Vsh != zenon_Vnd)
% 0.30/0.62  (r1 zenon_Vwe zenon_Vxe)
% 0.30/0.62  (r1 zenon_Vwf zenon_Vzf)
% 0.30/0.62  (zenon_Vef != zenon_Vnd)
% 0.30/0.62  (zenon_Vyg != zenon_Vmb)
% 0.30/0.62  (zenon_Vkh != zenon_Vfd)
% 0.30/0.62  (zenon_Vug != zenon_Voe)
% 0.30/0.62  (zenon_Vqg != zenon_Veg)
% 0.30/0.62  (zenon_Vef != zenon_Vaf)
% 0.30/0.62  (zenon_Vqe != zenon_Veg)
% 0.30/0.62  (zenon_Vsh != zenon_Vve)
% 0.30/0.62  (zenon_Vwh != zenon_Vuf)
% 0.30/0.62  (zenon_Vjf != zenon_Vuf)
% 0.30/0.62  (r1 zenon_Vwe zenon_Vbf)
% 0.30/0.62  (zenon_Vqg != zenon_Vjd)
% 0.30/0.62  (zenon_Vof != zenon_Vq)
% 0.30/0.62  (zenon_Vsh != zenon_Vda)
% 0.30/0.62  (zenon_Vzh != zenon_Voe)
% 0.30/0.62  (zenon_Vdc != zenon_Vmg)
% 0.30/0.62  (zenon_Vjf != zenon_Veg)
% 0.30/0.62  (p1 zenon_Vof)
% 0.30/0.62  (zenon_Vue != zenon_Vff)
% 0.30/0.62  (-. (p1 zenon_Vmb))
% 0.30/0.62  (zenon_Vug != zenon_Vjg)
% 0.30/0.62  (zenon_Vwh != zenon_Vff)
% 0.30/0.62  (zenon_Vef != zenon_Vjg)
% 0.30/0.62  (zenon_Vqe != zenon_Vtb)
% 0.30/0.62  (zenon_Vze != zenon_Vtb)
% 0.30/0.62  (zenon_Vig != zenon_Vnd)
% 0.30/0.62  (p2 zenon_Vdc)
% 0.30/0.62  (zenon_Vqe != zenon_Vaf)
% 0.30/0.62  (zenon_Vgh != zenon_Vkf)
% 0.30/0.62  (zenon_Vqe != zenon_Vde)
% 0.30/0.62  (zenon_Voh != zenon_Vkf)
% 0.30/0.62  (zenon_Vdg != zenon_Vw)
% 0.30/0.62  (zenon_Vug != zenon_Vka)
% 0.30/0.62  (zenon_Vqe != zenon_Vjd)
% 0.30/0.62  (zenon_Vqg != zenon_Vnd)
% 0.30/0.62  (zenon_Vue != zenon_Vvd)
% 0.30/0.62  (r1 zenon_Vcd zenon_Vfd)
% 0.30/0.62  (zenon_Vgh != zenon_Vre)
% 0.30/0.62  (zenon_Vsh != zenon_Vmb)
% 0.30/0.62  (zenon_Vdg != zenon_Vnd)
% 0.30/0.62  (zenon_Vtf != zenon_Vvd)
% 0.30/0.62  (zenon_Vig != zenon_Vka)
% 0.30/0.62  (zenon_Vdg != zenon_Vff)
% 0.30/0.62  (r1 zenon_Vvf zenon_Vwf)
% 0.30/0.62  (-. (p4 zenon_X3))
% 0.30/0.62  (zenon_Vqe != zenon_Vjg)
% 0.30/0.62  (zenon_Vtf != zenon_Vff)
% 0.30/0.62  (p1 zenon_Vqe)
% 0.30/0.62  (zenon_Vtf != zenon_Vfd)
% 0.30/0.62  (zenon_Vof != zenon_Vve)
% 0.30/0.62  (zenon_Vkh != zenon_Vde)
% 0.30/0.62  (zenon_Vof != zenon_Veg)
% 0.30/0.62  (zenon_Voh != zenon_Vpf)
% 0.30/0.62  (zenon_Vig != zenon_Vjd)
% 0.30/0.62  (zenon_Vue != zenon_Vzf)
% 0.30/0.62  (zenon_Vgh != zenon_Vfd)
% 0.30/0.62  (zenon_Vkh != zenon_Vfb)
% 0.30/0.62  (zenon_Vef != zenon_Vmb)
% 0.30/0.62  (r1 zenon_Vph zenon_Vsh)
% 0.30/0.62  (-. (p3 zenon_Vec))
% 0.30/0.62  (zenon_Vzh != zenon_Vaf)
% 0.30/0.62  (p2 zenon_Vwc)
% 0.30/0.62  (zenon_Vef != zenon_Vda)
% 0.30/0.62  (zenon_Vgh != zenon_Vtb)
% 0.30/0.62  (zenon_Vsh != zenon_Vfb)
% 0.30/0.62  (zenon_Vyg != zenon_Vda)
% 0.30/0.62  (zenon_Vjf != zenon_Vq)
% 0.30/0.62  (zenon_Voh != zenon_Veg)
% 0.30/0.62  (zenon_Voh != zenon_Vq)
% 0.30/0.62  (zenon_Vef != zenon_Vle)
% 0.30/0.62  (zenon_Vig != zenon_Vrd)
% 0.30/0.62  (zenon_Vzh != zenon_Vrd)
% 0.30/0.62  (zenon_Vof != zenon_Vtb)
% 0.30/0.62  (zenon_Vig != zenon_Vhe)
% 0.30/0.62  (zenon_Voh != zenon_Voe)
% 0.30/0.62  (zenon_Vig != zenon_Vaf)
% 0.30/0.62  (zenon_Vzh != zenon_Vzf)
% 0.30/0.62  (-. (p1 zenon_Vra))
% 0.30/0.62  (-. (p1 zenon_Vff))
% 0.30/0.62  (zenon_Vze != zenon_Vpf)
% 0.30/0.62  (-. (p3 zenon_Vxc))
% 0.30/0.62  (zenon_Vgh != zenon_Vuf)
% 0.30/0.62  (zenon_Vjf != zenon_Vfd)
% 0.30/0.62  (zenon_Vef != zenon_Vhe)
% 0.30/0.62  (zenon_Vch != zenon_Vac)
% 0.30/0.62  (zenon_Vsh != zenon_Vfd)
% 0.30/0.62  (zenon_Vjf != zenon_Vzf)
% 0.30/0.62  (zenon_Vkh != zenon_Vya)
% 0.30/0.62  (zenon_Vzh != zenon_Vkf)
% 0.30/0.62  (-. (p1 zenon_Vpf))
% 0.30/0.62  (zenon_Vsh != zenon_Vtb)
% 0.30/0.62  (zenon_Vsh != zenon_Voe)
% 0.30/0.62  (zenon_Vdg != zenon_Vzf)
% 0.30/0.62  (zenon_Vjf != zenon_Vac)
% 0.30/0.62  (zenon_Vqg != zenon_Vde)
% 0.30/0.62  (zenon_Vtf != zenon_Vve)
% 0.30/0.62  (zenon_Vqg != zenon_Vmb)
% 0.30/0.62  (zenon_Vof != zenon_Vda)
% 0.30/0.62  (zenon_Vyg != zenon_Vrd)
% 0.30/0.62  (zenon_Vzh != zenon_Vmb)
% 0.30/0.62  (r1 zenon_Vvc zenon_Vwc)
% 0.30/0.62  (-. (p1 zenon_Vw))
% 0.30/0.62  (r1 zenon_Vbc zenon_Vad)
% 0.30/0.62  (zenon_Vyf != zenon_Vzf)
% 0.30/0.62  (zenon_Vsh != zenon_Vvd)
% 0.30/0.62  (zenon_Vef != zenon_Vvd)
% 0.30/0.62  (zenon_Vqg != zenon_Vda)
% 0.30/0.62  (r1 zenon_Vvb zenon_Vzb)
% 0.30/0.62  (zenon_Vqe != zenon_Vzd)
% 0.30/0.62  (p1 zenon_Vqg)
% 0.30/0.62  (zenon_Vof != zenon_Vfb)
% 0.30/0.62  (zenon_Vqe != zenon_Vfd)
% 0.30/0.62  (p1 zenon_Vyg)
% 0.30/0.62  (zenon_Vdg != zenon_Vre)
% 0.30/0.62  (zenon_Vyf != zenon_Vmb)
% 0.30/0.62  (zenon_Voh != zenon_Vtb)
% 0.30/0.62  (r1 zenon_Vrc zenon_Vuc)
% 0.30/0.62  (zenon_Vdg != zenon_Vpf)
% 0.30/0.62  (zenon_Vkh != zenon_Vzd)
% 0.30/0.62  (zenon_Vef != zenon_Vq)
% 0.30/0.62  (zenon_Vug != zenon_Vrd)
% 0.30/0.62  (zenon_Vwh != zenon_Vhe)
% 0.30/0.62  (zenon_Vdg != zenon_Vjd)
% 0.30/0.62  (zenon_Vwh != zenon_Veg)
% 0.30/0.62  (zenon_Vzh != zenon_Vtb)
% 0.30/0.62  (zenon_Vig != zenon_Vpf)
% 0.30/0.62  (zenon_Voh != zenon_Vzd)
% 0.30/0.62  (zenon_Vzh != zenon_Vde)
% 0.30/0.62  (zenon_Vef != zenon_Vra)
% 0.30/0.62  (zenon_Vyg != zenon_Vfd)
% 0.30/0.62  (zenon_Vgh != zenon_Vjg)
% 0.30/0.62  (zenon_Vch != zenon_Vfd)
% 0.30/0.62  (zenon_Vwh != zenon_Voe)
% 0.30/0.62  (zenon_Vdg != zenon_Vra)
% 0.30/0.62  (zenon_Vgh != zenon_Vhe)
% 0.30/0.62  (zenon_Vch != zenon_Vzf)
% 0.30/0.62  (zenon_Vze != zenon_Vzf)
% 0.30/0.62  (zenon_Vef != zenon_Vff)
% 0.30/0.62  (zenon_Voh != zenon_Vde)
% 0.30/0.62  (r1 zenon_Vcf zenon_Vdf)
% 0.30/0.62  (zenon_Vef != zenon_Vde)
% 0.30/0.62  (zenon_Vug != zenon_Vmb)
% 0.30/0.62  (zenon_Vyg != zenon_Vkf)
% 0.30/0.62  (zenon_Vyg != zenon_Vzf)
% 0.30/0.62  (zenon_Vue != zenon_Vkf)
% 0.30/0.62  (zenon_Vjf != zenon_Vre)
% 0.30/0.62  (zenon_Vqe != zenon_Vac)
% 0.30/0.62  (zenon_Vdg != zenon_Vya)
% 0.30/0.62  (zenon_Vwh != zenon_Vve)
% 0.30/0.62  (zenon_Voh != zenon_Vda)
% 0.30/0.62  (zenon_Vyg != zenon_Veg)
% 0.30/0.62  (zenon_Vzh != zenon_Vfb)
% 0.30/0.62  (zenon_Vof != zenon_Vde)
% 0.30/0.62  (zenon_Vkh != zenon_Vda)
% 0.30/0.62  (zenon_Vgh != zenon_Vzd)
% 0.30/0.62  (zenon_Vsh != zenon_Vuf)
% 0.30/0.62  (r1 zenon_Vgg zenon_Vjg)
% 0.30/0.62  (zenon_Vgh != zenon_Vac)
% 0.30/0.62  (zenon_Vgh != zenon_Vnd)
% 0.30/0.62  (zenon_Vug != zenon_Vvd)
% 0.30/0.62  (zenon_Vyf != zenon_Vq)
% 0.30/0.62  (zenon_Vgh != zenon_Vya)
% 0.30/0.62  (zenon_Vwh != zenon_Vfb)
% 0.30/0.62  (zenon_Vof != zenon_Vra)
% 0.30/0.62  (zenon_Vtf != zenon_Vle)
% 0.30/0.62  (zenon_Vtf != zenon_Veg)
% 0.30/0.62  (zenon_Vyf != zenon_Vff)
% 0.30/0.62  (zenon_Vjf != zenon_Vtb)
% 0.30/0.62  (p1 zenon_Vtf)
% 0.30/0.62  (zenon_Vze != zenon_Vra)
% 0.30/0.62  (zenon_Vch != zenon_Vra)
% 0.30/0.62  (zenon_Vgh != zenon_Vjd)
% 0.30/0.62  (r1 zenon_Vqf zenon_Vrf)
% 0.30/0.62  (zenon_Vzh != zenon_Vnd)
% 0.30/0.62  (zenon_Vyg != zenon_Vq)
% 0.30/0.62  (zenon_Vgh != zenon_Vra)
% 0.30/0.62  (zenon_Vig != zenon_Vre)
% 0.30/0.62  (zenon_Vsh != zenon_Vkf)
% 0.30/0.62  (zenon_Vtf != zenon_Vac)
% 0.30/0.62  (zenon_Vyg != zenon_Vfb)
% 0.30/0.62  (zenon_Vtf != zenon_Vra)
% 0.30/0.62  (r1 zenon_Vgf zenon_Vlf)
% 0.30/0.62  (r1 zenon_Vlg zenon_Vmg)
% 0.30/0.62  (zenon_Vef != zenon_Vve)
% 0.30/0.62  (r1 Tau_0 Tau_2)
% 0.30/0.62  (r1 zenon_Vvg zenon_Vyg)
% 0.30/0.62  (zenon_Voh != zenon_Vnd)
% 0.30/0.62  (-. (p1 zenon_Vjg))
% 0.30/0.62  (zenon_Vyg != zenon_Vaf)
% 0.30/0.62  (zenon_Vef != zenon_Vya)
% 0.30/0.62  (zenon_Vof != zenon_Vrd)
% 0.30/0.62  (zenon_Vgh != zenon_Vle)
% 0.30/0.62  (zenon_Vzh != zenon_Vfd)
% 0.30/0.62  (zenon_Vyf != zenon_Vrd)
% 0.30/0.62  (zenon_Vkh != zenon_Vra)
% 0.30/0.62  (p1 zenon_Vdg)
% 0.30/0.62  (zenon_Vsh != zenon_Veg)
% 0.30/0.62  (zenon_Vyf != zenon_Vra)
% 0.30/0.62  (zenon_Vch != zenon_Vya)
% 0.30/0.62  (zenon_Vjf != zenon_Vmb)
% 0.30/0.62  (zenon_Vyf != zenon_Vjg)
% 0.30/0.62  (zenon_Vwh != zenon_Vtb)
% 0.30/0.62  (zenon_Vsh != zenon_Vac)
% 0.30/0.62  (zenon_Vzh != zenon_Vra)
% 0.30/0.62  (zenon_Voh != zenon_Vac)
% 0.30/0.62  (zenon_Vzh != zenon_Vya)
% 0.30/0.62  (zenon_Vzh != zenon_Veg)
% 0.30/0.62  (zenon_Vof != zenon_Vff)
% 0.30/0.62  (zenon_Vtf != zenon_Vde)
% 0.30/0.62  (zenon_Vsh != zenon_Vjg)
% 0.30/0.62  (zenon_Vof != zenon_Vkf)
% 0.30/0.62  (r1 zenon_Vdh zenon_Vgh)
% 0.30/0.62  (zenon_Vqe != zenon_Vpf)
% 0.30/0.62  (zenon_Vze != zenon_Vnd)
% 0.30/0.62  (zenon_Vue != zenon_Vuf)
% 0.30/0.62  (r1 zenon_Vag zenon_Vbg)
% 0.30/0.62  (zenon_Vgh != zenon_Vff)
% 0.30/0.62  (-. (p1 zenon_Vde))
% 0.30/0.62  (p1 zenon_Vef)
% 0.30/0.62  (zenon_Vdg != zenon_Vjg)
% 0.30/0.62  (zenon_Vef != zenon_Veg)
% 0.30/0.62  (zenon_Vtf != zenon_Vfb)
% 0.30/0.62  (zenon_Vqg != zenon_Vaf)
% 0.30/0.62  (zenon_Vtf != zenon_Vre)
% 0.30/0.62  (zenon_Voh != zenon_Vfd)
% 0.30/0.62  (zenon_Vyf != zenon_Vzd)
% 0.30/0.62  (r1 zenon_Vgd zenon_Vjd)
% 0.30/0.62  (zenon_Vqg != zenon_Vka)
% 0.30/0.62  (zenon_Vqe != zenon_Voe)
% 0.30/0.62  (zenon_Vig != zenon_Voe)
% 0.30/0.62  (zenon_Vof != zenon_Vvd)
% 0.30/0.62  (r1 zenon_Vsd zenon_Vvd)
% 0.30/0.62  (zenon_Vqg != zenon_Vzf)
% 0.30/0.62  (r1 zenon_Vlf zenon_Vqf)
% 0.30/0.62  (zenon_Vjf != zenon_Voe)
% 0.30/0.62  (zenon_Vch != zenon_Vmb)
% 0.30/0.62  (zenon_Vqg != zenon_Vzd)
% 0.30/0.62  (-. (p2 zenon_Vqc))
% 0.30/0.62  (zenon_Vyf != zenon_Vfb)
% 0.30/0.62  (zenon_Vdg != zenon_Vuf)
% 0.30/0.62  (zenon_Vwh != zenon_Vre)
% 0.30/0.62  (zenon_Vyg != zenon_Vuf)
% 0.30/0.62  (zenon_Vug != zenon_Vaf)
% 0.30/0.62  (zenon_Vch != zenon_Vka)
% 0.30/0.62  (zenon_Voh != zenon_Vka)
% 0.30/0.62  (zenon_Vtf != zenon_Voe)
% 0.30/0.62  (zenon_Vzh != zenon_Vvd)
% 0.30/0.62  (zenon_Vwh != zenon_Vpf)
% 0.30/0.62  (zenon_Vjf != zenon_Vfb)
% 0.30/0.62  (zenon_Vig != zenon_Vya)
% 0.30/0.62  (zenon_Vwh != zenon_Vnd)
% 0.30/0.62  (zenon_Vdg != zenon_Vve)
% 0.30/0.62  (zenon_Vkh != zenon_Vle)
% 0.30/0.62  (zenon_Vig != zenon_Veg)
% 0.30/0.62  (zenon_Vqe != zenon_Vuf)
% 0.30/0.62  (zenon_Vkh != zenon_Vtb)
% 0.30/0.62  (r1 zenon_Vta zenon_Vxa)
% 0.30/0.62  (zenon_Vqg != zenon_Vac)
% 0.30/0.62  (zenon_Vue != zenon_Vda)
% 0.30/0.62  (zenon_Vue != zenon_Vhe)
% 0.30/0.62  (zenon_Vze != zenon_Vuf)
% 0.30/0.62  (zenon_Vug != zenon_Vfb)
% 0.30/0.62  (zenon_Vqe != zenon_Vvd)
% 0.30/0.62  (zenon_Vwh != zenon_Vzd)
% 0.30/0.62  *)
% 0.30/0.62  (* NO-PROOF *)
% 0.30/0.62  % SZS status GaveUp
% 0.30/0.62  Number of rewrites on terms: 0
% 0.30/0.62  Number of rewrites on props: 0
% 0.30/0.62  nodes searched: 1015
% 0.30/0.62  max branch formulas: 1152
% 0.30/0.62  proof nodes created: 0
% 0.30/0.62  formulas created: 5875
% 0.30/0.62  
%------------------------------------------------------------------------------