↑ Up

ZenonModulo---0.5.0.UNK-Non.f

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

% Computer : n018.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:30 PM UTC 2026

% Result   : Unknown 0.20s 0.53s
% Output   : None 
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : LCL688+1.010 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03  % Command  : run_zenon_modulo %d %s
% 0.09/0.35  % Computer : n018.cluster.edu
% 0.09/0.35  % Model    : x86_64 x86_64
% 0.09/0.35  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35  % Memory   : 8046.5625MB
% 0.09/0.35  % OS       : Linux 6.8.0-71-generic
% 0.09/0.35  % CPULimit : 300
% 0.09/0.35  % WCLimit  : 300
% 0.09/0.35  % DateTime : Sat Sep  5 15:11:19 UTC 2026
% 0.09/0.35  % CPUTime  : 
% 0.20/0.53  Zenon error: exhausted search space without finding a proof
% 0.20/0.53  (* Current branch:
% 0.20/0.53  (zenon_Vdg != zenon_Vxc)
% 0.20/0.53  (zenon_Vgf != zenon_Vfb)
% 0.20/0.53  (zenon_Vjh != zenon_Vid)
% 0.20/0.53  (p1 zenon_Vbf)
% 0.20/0.53  (zenon_Vbh != zenon_Vjb)
% 0.20/0.53  (zenon_Vde != zenon_Vrf)
% 0.20/0.53  (zenon_Vfh != zenon_Vec)
% 0.20/0.53  (zenon_Vme != zenon_Vrf)
% 0.20/0.53  (zenon_Vlg != zenon_Vza)
% 0.20/0.53  (zenon_Vqf != zenon_Vee)
% 0.20/0.53  (zenon_Vme != zenon_Vxe)
% 0.20/0.53  (zenon_Vxg != zenon_Vmd)
% 0.20/0.53  (p1 zenon_Vqf)
% 0.20/0.53  (zenon_Vxg != zenon_Vdc)
% 0.20/0.53  (zenon_Vre != zenon_Vqa)
% 0.20/0.53  (zenon_Vre != zenon_Vyb)
% 0.20/0.53  (zenon_Vtg != zenon_Vkb)
% 0.20/0.53  (zenon_Vhe != zenon_Vqa)
% 0.20/0.53  (zenon_Vhe != zenon_Vse)
% 0.20/0.53  (zenon_Vde != zenon_Vtb)
% 0.20/0.53  (zenon_Vre != zenon_Veb)
% 0.20/0.53  (zenon_Vdg != zenon_Vua)
% 0.20/0.53  (zenon_Vpg != zenon_Vab)
% 0.20/0.53  (zenon_Vfh != zenon_Vyc)
% 0.20/0.53  (zenon_Vbh != zenon_Vyc)
% 0.20/0.53  (-. (p1 zenon_Vyc))
% 0.20/0.53  (zenon_Vde != zenon_Vae)
% 0.20/0.53  (zenon_Vpg != zenon_Vcd)
% 0.20/0.53  (zenon_Vpg != zenon_Veb)
% 0.20/0.53  (zenon_Vme != zenon_Vsc)
% 0.20/0.53  (zenon_Vxg != zenon_Vjb)
% 0.20/0.53  (p1 zenon_Vtg)
% 0.20/0.53  (zenon_Vhg != zenon_Vza)
% 0.20/0.53  (r1 zenon_Vgh zenon_Vjh)
% 0.20/0.53  (zenon_Vhe != zenon_Vxd)
% 0.20/0.53  (zenon_Vbh != zenon_Vjc)
% 0.20/0.53  (zenon_Vxg != zenon_Vec)
% 0.20/0.53  (zenon_Vvf != zenon_Vnd)
% 0.20/0.53  (zenon_Vgf != zenon_Vee)
% 0.20/0.53  (zenon_Vbh != zenon_Vsd)
% 0.20/0.53  (zenon_Vgf != zenon_Vic)
% 0.20/0.53  (zenon_Vpg != zenon_Vdc)
% 0.20/0.53  (zenon_Vgf != zenon_Vdd)
% 0.20/0.53  (zenon_Vbh != zenon_Vdd)
% 0.20/0.53  (zenon_Vdg != zenon_Vnc)
% 0.20/0.53  (zenon_Vxg != zenon_Veb)
% 0.20/0.53  (zenon_Vqf != zenon_Vwd)
% 0.20/0.53  (zenon_Vhe != zenon_Vpa)
% 0.20/0.53  (zenon_Vwe != zenon_Vxe)
% 0.20/0.53  (r1 zenon_Veg zenon_Vhg)
% 0.20/0.53  (zenon_Vpg != zenon_Vza)
% 0.20/0.53  (zenon_Vdg != zenon_Vse)
% 0.20/0.53  (zenon_Vdg != zenon_Vie)
% 0.20/0.53  (r1 zenon_Vje zenon_Voe)
% 0.20/0.53  (zenon_Vwe != zenon_Vee)
% 0.20/0.53  (r1 zenon_Vca zenon_Vpa)
% 0.20/0.53  (zenon_Vre != zenon_Vxd)
% 0.20/0.53  (zenon_Vwe != zenon_Vrf)
% 0.20/0.53  (zenon_Vxg != zenon_Vtc)
% 0.20/0.53  (zenon_Vmh != zenon_Vjc)
% 0.20/0.53  (r1 zenon_Vea zenon_Vfa)
% 0.20/0.53  (zenon_Vwe != zenon_Vec)
% 0.20/0.53  (zenon_Vde != zenon_Vyb)
% 0.20/0.53  (zenon_Vmh != zenon_Vyb)
% 0.20/0.53  (-. (p1 zenon_Vmd))
% 0.20/0.53  (zenon_Vqf != zenon_Vse)
% 0.20/0.53  (zenon_Vme != zenon_Vmf)
% 0.20/0.53  (zenon_Vlg != zenon_Vsc)
% 0.20/0.53  (zenon_Vhg != zenon_Vdc)
% 0.20/0.53  (zenon_Vme != zenon_Vjb)
% 0.20/0.53  (zenon_Vfh != zenon_Vab)
% 0.20/0.53  (zenon_Vdg != zenon_Vsd)
% 0.20/0.53  (zenon_Vlf != zenon_Vic)
% 0.20/0.53  (r1 zenon_Vjf zenon_Vkf)
% 0.20/0.53  (zenon_Vqf != zenon_Veb)
% 0.20/0.53  (-. (p1 zenon_Vpa))
% 0.20/0.53  (zenon_Vre != zenon_Vsd)
% 0.20/0.53  (-. (p1 zenon_Vqa))
% 0.20/0.53  (zenon_Vgf != zenon_Vub)
% 0.20/0.53  (zenon_Vde != zenon_Vcd)
% 0.20/0.53  (zenon_Vbf != zenon_Vhd)
% 0.20/0.53  (zenon_Vre != zenon_Vrd)
% 0.20/0.53  (zenon_Vgf != zenon_Vmf)
% 0.20/0.53  (zenon_Vwe != zenon_Vwf)
% 0.20/0.53  (zenon_Vxg != zenon_Vne)
% 0.20/0.53  (zenon_Vme != zenon_Vmd)
% 0.20/0.53  (zenon_Vtg != zenon_Vnd)
% 0.20/0.53  (zenon_Vlg != zenon_Vub)
% 0.20/0.53  (-. (p1 zenon_Vxd))
% 0.20/0.53  (zenon_Vgf != zenon_Vrd)
% 0.20/0.53  (zenon_Vbf != zenon_Vsd)
% 0.20/0.53  (zenon_Vvf != zenon_Vec)
% 0.20/0.53  (zenon_Vpg != zenon_Vyb)
% 0.20/0.53  (r1 zenon_Vig zenon_Vlg)
% 0.20/0.53  (zenon_Vbf != zenon_Vwd)
% 0.20/0.53  (zenon_Vtg != zenon_Vwd)
% 0.20/0.53  (-. (p1 zenon_Vrf))
% 0.20/0.53  (zenon_Vtg != zenon_Vse)
% 0.20/0.53  (zenon_Vvf != zenon_Vmf)
% 0.20/0.53  (zenon_Vjh != zenon_Vhd)
% 0.20/0.53  (zenon_Vbh != zenon_Vzb)
% 0.20/0.53  (-. (p1 zenon_Vyb))
% 0.20/0.53  (zenon_Vfh != zenon_Vyb)
% 0.20/0.53  (zenon_Vbf != zenon_Vee)
% 0.20/0.53  (zenon_Vlg != zenon_Vid)
% 0.20/0.53  (zenon_Vhg != zenon_Vyb)
% 0.20/0.53  (zenon_Vmh != zenon_Vsd)
% 0.20/0.53  (r1 Tau_1 zenon_Vce)
% 0.20/0.53  (r1 zenon_Vtf zenon_Vwf)
% 0.20/0.53  (zenon_Vre != zenon_Vmf)
% 0.20/0.53  (zenon_Vgf != zenon_Vkb)
% 0.20/0.53  (zenon_Vde != zenon_Vxd)
% 0.20/0.53  (zenon_Vgf != zenon_Vtb)
% 0.20/0.53  (zenon_Vhe != zenon_Vpb)
% 0.20/0.53  (p1 zenon_Vpg)
% 0.20/0.53  (zenon_Vbf != zenon_Vzb)
% 0.20/0.53  (zenon_Vhg != zenon_Vrf)
% 0.20/0.53  (zenon_Vpg != zenon_Vpb)
% 0.20/0.53  (zenon_Vfh != zenon_Vva)
% 0.20/0.53  (zenon_Vlf != zenon_Vnd)
% 0.20/0.53  (zenon_Vjh != zenon_Vec)
% 0.20/0.53  (-. (p1 zenon_Vae))
% 0.20/0.53  (zenon_Vvf != zenon_Vrf)
% 0.20/0.53  (zenon_Vbh != zenon_Vcd)
% 0.20/0.53  (p1 zenon_Vre)
% 0.20/0.53  (zenon_Vwe != zenon_Vic)
% 0.20/0.53  (zenon_Vlf != zenon_Vec)
% 0.20/0.53  (zenon_Vbf != zenon_Vqa)
% 0.20/0.53  (zenon_Vde != zenon_Vza)
% 0.20/0.53  (zenon_Vmh != zenon_Veb)
% 0.20/0.53  (-. (p1 zenon_Vhf))
% 0.20/0.53  (zenon_Vvf != zenon_Vzb)
% 0.20/0.53  (zenon_Vwe != zenon_Vab)
% 0.20/0.53  (zenon_Vxg != zenon_Vpa)
% 0.20/0.53  (zenon_Vpg != zenon_Vse)
% 0.20/0.53  (zenon_Vme != zenon_Vdd)
% 0.20/0.53  (zenon_Vfh != zenon_Vqa)
% 0.20/0.53  (zenon_Vlg != zenon_Vxc)
% 0.20/0.53  (zenon_Vre != zenon_Vua)
% 0.20/0.53  (zenon_Vmh != zenon_Vae)
% 0.20/0.53  (zenon_Vpg != zenon_Vnc)
% 0.20/0.53  (zenon_Vhe != zenon_Vob)
% 0.20/0.53  (zenon_Vqf != zenon_Vab)
% 0.20/0.53  (zenon_Vlg != zenon_Vic)
% 0.20/0.53  (zenon_Vfh != zenon_Vmf)
% 0.20/0.53  (zenon_Vde != zenon_Voc)
% 0.20/0.53  (zenon_Vmh != zenon_Vqa)
% 0.20/0.53  (zenon_Vdg != zenon_Vmd)
% 0.20/0.53  (zenon_Vme != zenon_Vtc)
% 0.20/0.53  (zenon_Vlf != zenon_Vhf)
% 0.20/0.53  (zenon_Vjh != zenon_Vmf)
% 0.20/0.53  (zenon_Vre != zenon_Vva)
% 0.20/0.53  (p1 zenon_Vlf)
% 0.20/0.53  (p1 zenon_Vxg)
% 0.20/0.53  (zenon_Vre != zenon_Vjc)
% 0.20/0.53  (-. (p1 zenon_Vtb))
% 0.20/0.53  (zenon_Vtg != zenon_Vua)
% 0.20/0.53  (zenon_Vde != zenon_Vid)
% 0.20/0.53  (zenon_Vbf != zenon_Vse)
% 0.20/0.53  (zenon_Vde != zenon_Vpa)
% 0.20/0.53  (zenon_Vbf != zenon_Vec)
% 0.20/0.53  (zenon_Vdg != zenon_Vid)
% 0.20/0.53  (zenon_Vqf != zenon_Vhf)
% 0.20/0.53  (zenon_Vhg != zenon_Vqa)
% 0.20/0.53  (zenon_Vmh != zenon_Vec)
% 0.20/0.53  (zenon_Vde != zenon_Vjc)
% 0.20/0.53  (zenon_Vlg != zenon_Vwf)
% 0.20/0.53  (zenon_Vdg != zenon_Voc)
% 0.20/0.53  (zenon_Vbf != zenon_Vza)
% 0.20/0.53  (zenon_Vvf != zenon_Vie)
% 0.20/0.53  (zenon_Vtg != zenon_Vsd)
% 0.20/0.53  (-. (p1 zenon_Vzb))
% 0.20/0.53  (zenon_Vtg != zenon_Vec)
% 0.20/0.53  (zenon_Vjh != zenon_Vic)
% 0.20/0.53  (-. (p1 zenon_Vxc))
% 0.20/0.53  (zenon_Vbh != zenon_Vee)
% 0.20/0.53  (zenon_Vtg != zenon_Vae)
% 0.20/0.53  (zenon_Vqf != zenon_Vsc)
% 0.20/0.53  (zenon_Vfh != zenon_Vcd)
% 0.20/0.53  (zenon_Vwe != zenon_Vmd)
% 0.20/0.53  (zenon_Vbf != zenon_Vyb)
% 0.20/0.53  (zenon_Vdg != zenon_Vxe)
% 0.20/0.53  (zenon_Vmh != zenon_Vxc)
% 0.20/0.53  (zenon_Vlf != zenon_Vse)
% 0.20/0.53  (zenon_Vre != zenon_Vne)
% 0.20/0.53  (zenon_Vfh != zenon_Vjb)
% 0.20/0.53  (zenon_Vde != zenon_Vic)
% 0.20/0.53  (zenon_Vhe != zenon_Vkb)
% 0.20/0.53  (r1 Tau_0 Tau_1)
% 0.20/0.53  (zenon_Vbh != zenon_Vtb)
% 0.20/0.53  (-. (p1 zenon_Vdd))
% 0.20/0.53  (zenon_Vqf != zenon_Vqa)
% 0.20/0.53  (zenon_Vvf != zenon_Vmd)
% 0.20/0.53  (zenon_Vxg != zenon_Vdd)
% 0.20/0.53  (zenon_Vvf != zenon_Vfb)
% 0.20/0.53  (zenon_Vpg != zenon_Vfb)
% 0.20/0.53  (zenon_Vlg != zenon_Vkb)
% 0.20/0.53  (zenon_Vjh != zenon_Vab)
% 0.20/0.53  (zenon_Vdg != zenon_Vva)
% 0.20/0.53  (zenon_Vjh != zenon_Vee)
% 0.20/0.53  (zenon_Vfh != zenon_Vjc)
% 0.20/0.53  (zenon_Vmh != zenon_Vxd)
% 0.20/0.53  (zenon_Vhg != zenon_Vwd)
% 0.20/0.53  (zenon_Vpg != zenon_Vva)
% 0.20/0.53  (zenon_Vhg != zenon_Vcf)
% 0.20/0.53  (zenon_Vbh != zenon_Vxd)
% 0.20/0.53  (r1 zenon_Vqg zenon_Vtg)
% 0.20/0.53  (-. (p1 zenon_Vpb))
% 0.20/0.53  (zenon_Vtg != zenon_Vmf)
% 0.20/0.53  (zenon_Vmh != zenon_Vzb)
% 0.20/0.53  (zenon_Vbf != zenon_Vnd)
% 0.20/0.53  (zenon_Vxg != zenon_Vva)
% 0.20/0.53  (zenon_Vmh != zenon_Vub)
% 0.20/0.53  (zenon_Vvf != zenon_Vyc)
% 0.20/0.53  (zenon_Vhe != zenon_Vub)
% 0.20/0.53  (zenon_Vhg != zenon_Vjb)
% 0.20/0.53  (-. (p1 zenon_Vne))
% 0.20/0.53  (zenon_Vbf != zenon_Vtb)
% 0.20/0.53  (zenon_Vtg != zenon_Vva)
% 0.20/0.53  (-. (p1 zenon_Vab))
% 0.20/0.53  (zenon_Vjh != zenon_Vyb)
% 0.20/0.53  (zenon_Vvf != zenon_Vic)
% 0.20/0.53  (zenon_Vhg != zenon_Vab)
% 0.20/0.53  (zenon_Vxg != zenon_Vae)
% 0.20/0.53  (zenon_Vbh != zenon_Vic)
% 0.20/0.53  (zenon_Vlg != zenon_Vae)
% 0.20/0.53  (zenon_Vhe != zenon_Vmd)
% 0.20/0.53  (r1 zenon_Voe zenon_Vpe)
% 0.20/0.53  (zenon_Vmh != zenon_Vmd)
% 0.20/0.53  (zenon_Vdg != zenon_Vhf)
% 0.20/0.53  (zenon_Vmh != zenon_Vne)
% 0.20/0.53  (-. (p1 zenon_Vcf))
% 0.20/0.53  (zenon_Vjh != zenon_Vrd)
% 0.20/0.53  (zenon_Vfh != zenon_Vpb)
% 0.20/0.53  (zenon_Vre != zenon_Vse)
% 0.20/0.53  (zenon_Vre != zenon_Vpb)
% 0.20/0.53  (zenon_Vbf != zenon_Vsc)
% 0.20/0.53  (zenon_Vlf != zenon_Vtc)
% 0.20/0.53  (r1 zenon_Vef zenon_Vff)
% 0.20/0.53  (zenon_Vqf != zenon_Vsd)
% 0.20/0.53  (r1 zenon_Vke zenon_Vne)
% 0.20/0.53  (zenon_Vjh != zenon_Vkb)
% 0.20/0.53  (zenon_Vfh != zenon_Vne)
% 0.20/0.53  (zenon_Vqf != zenon_Vfb)
% 0.20/0.53  (r1 zenon_Vte zenon_Vue)
% 0.20/0.53  (p1 zenon_Vmh)
% 0.20/0.53  (zenon_Vlg != zenon_Vfb)
% 0.20/0.53  (zenon_Vre != zenon_Vyc)
% 0.20/0.53  (zenon_Vtg != zenon_Vyc)
% 0.20/0.53  (zenon_Vhe != zenon_Vsc)
% 0.20/0.53  (zenon_Vdg != zenon_Vmf)
% 0.20/0.53  (zenon_Vjh != zenon_Vwf)
% 0.20/0.53  (zenon_Vjh != zenon_Vrf)
% 0.20/0.53  (zenon_Vbf != zenon_Voc)
% 0.20/0.53  (zenon_Vde != zenon_Vpb)
% 0.20/0.53  (zenon_Vxg != zenon_Vnd)
% 0.20/0.53  (zenon_Vre != zenon_Vsc)
% 0.20/0.53  (zenon_Vmh != zenon_Vua)
% 0.20/0.53  (zenon_Vmh != zenon_Vhd)
% 0.20/0.53  (zenon_Vwe != zenon_Vcf)
% 0.20/0.53  (zenon_Vpg != zenon_Vua)
% 0.20/0.53  (zenon_Vbh != zenon_Vcf)
% 0.20/0.53  (zenon_Vwe != zenon_Vxc)
% 0.20/0.53  (zenon_Vme != zenon_Vie)
% 0.20/0.53  (r1 zenon_Vo zenon_Vhd)
% 0.20/0.53  (zenon_Vjh != zenon_Vpa)
% 0.20/0.53  (zenon_Vjh != zenon_Vse)
% 0.20/0.53  (zenon_Vqf != zenon_Vxd)
% 0.20/0.53  (zenon_Vhe != zenon_Vab)
% 0.20/0.53  (zenon_Vme != zenon_Vsd)
% 0.20/0.53  (zenon_Vtg != zenon_Vpb)
% 0.20/0.53  (zenon_Vwe != zenon_Vdc)
% 0.20/0.53  (zenon_Vdg != zenon_Vxd)
% 0.20/0.53  (zenon_Vbf != zenon_Vmd)
% 0.20/0.53  (r1 Tau_1 zenon_Vee)
% 0.20/0.53  (zenon_Vxg != zenon_Vsd)
% 0.20/0.53  (zenon_Vqf != zenon_Vzb)
% 0.20/0.53  (r1 zenon_Vug zenon_Vxg)
% 0.20/0.53  (zenon_Vpg != zenon_Vqa)
% 0.20/0.53  (zenon_Vbf != zenon_Vhf)
% 0.20/0.53  (zenon_Vdg != zenon_Vzb)
% 0.20/0.53  (zenon_Vhg != zenon_Vmf)
% 0.20/0.53  (zenon_Vme != zenon_Vse)
% 0.20/0.53  (zenon_Vvf != zenon_Vne)
% 0.20/0.53  (zenon_Vfh != zenon_Vid)
% 0.20/0.53  (zenon_Vme != zenon_Vyc)
% 0.20/0.53  (zenon_Vvf != zenon_Vub)
% 0.20/0.53  (zenon_Vgf != zenon_Vab)
% 0.20/0.53  (zenon_Vme != zenon_Vid)
% 0.20/0.53  (zenon_Vqf != zenon_Vua)
% 0.20/0.53  (zenon_Vdg != zenon_Vhd)
% 0.20/0.53  (zenon_Vwe != zenon_Vyb)
% 0.20/0.53  (zenon_Vvf != zenon_Vva)
% 0.20/0.53  (zenon_Vmh != zenon_Vwd)
% 0.20/0.53  (r1 zenon_Vn zenon_Vmd)
% 0.20/0.53  (zenon_Vpg != zenon_Vdd)
% 0.20/0.53  (zenon_Vxg != zenon_Vtb)
% 0.20/0.53  (zenon_Vxg != zenon_Vid)
% 0.20/0.53  (r1 zenon_Vw zenon_Vtb)
% 0.20/0.53  (zenon_Vjh != zenon_Vnd)
% 0.20/0.53  (zenon_Vre != zenon_Vwf)
% 0.20/0.53  (r1 Tau_0 Tau_3)
% 0.20/0.53  (-. (p1 zenon_Vsc))
% 0.20/0.53  (zenon_Vwe != zenon_Vnd)
% 0.20/0.53  (zenon_Vhg != zenon_Voc)
% 0.20/0.53  (zenon_Vhg != zenon_Vob)
% 0.20/0.53  (r1 zenon_Vsf zenon_Vtf)
% 0.20/0.53  (zenon_Vdg != zenon_Vfb)
% 0.20/0.53  (zenon_Vmh != zenon_Vtb)
% 0.20/0.53  (zenon_Vbf != zenon_Vae)
% 0.20/0.53  (zenon_Vfh != zenon_Vkb)
% 0.20/0.53  (zenon_Vwe != zenon_Vmf)
% 0.20/0.53  (zenon_Vlg != zenon_Vne)
% 0.20/0.53  (zenon_Vhe != zenon_Vhd)
% 0.20/0.53  (zenon_Vdg != zenon_Vdc)
% 0.20/0.53  (zenon_Vlg != zenon_Vnc)
% 0.20/0.53  (zenon_Vpg != zenon_Vjc)
% 0.20/0.53  (zenon_Vfh != zenon_Vob)
% 0.20/0.53  (r1 zenon_Vyf zenon_Vzf)
% 0.20/0.53  (zenon_Vbf != zenon_Vyc)
% 0.20/0.53  (r1 zenon_Vjf zenon_Vmf)
% 0.20/0.53  (zenon_Vxg != zenon_Vic)
% 0.20/0.53  (zenon_Vlg != zenon_Vob)
% 0.20/0.53  (zenon_Vbf != zenon_Vcf)
% 0.20/0.53  (zenon_Vfh != zenon_Vxe)
% 0.20/0.53  (zenon_Vre != zenon_Vtc)
% 0.20/0.53  (zenon_Vme != zenon_Vyb)
% 0.20/0.53  (zenon_Vpg != zenon_Vob)
% 0.20/0.53  (zenon_Vpg != zenon_Vxc)
% 0.20/0.53  (zenon_Vhe != zenon_Vwf)
% 0.20/0.53  (zenon_Vlf != zenon_Vzb)
% 0.20/0.53  (zenon_Vwe != zenon_Vyc)
% 0.20/0.53  (zenon_Vhe != zenon_Vtb)
% 0.20/0.53  (r1 zenon_Vte zenon_Vye)
% 0.20/0.53  (-. (p1 zenon_Vcd))
% 0.20/0.53  (zenon_Vfh != zenon_Vhf)
% 0.20/0.53  (p1 zenon_Vhe)
% 0.20/0.53  (zenon_Vlf != zenon_Vyc)
% 0.20/0.53  (zenon_Vdg != zenon_Vic)
% 0.20/0.53  (zenon_Vtg != zenon_Vsc)
% 0.20/0.53  (zenon_Vhg != zenon_Vtb)
% 0.20/0.53  (zenon_Vmh != zenon_Voc)
% 0.20/0.53  (zenon_Vde != zenon_Vob)
% 0.20/0.53  (zenon_Vwe != zenon_Vie)
% 0.20/0.53  (zenon_Vqf != zenon_Vec)
% 0.20/0.53  (r1 zenon_Vyg zenon_Vbh)
% 0.20/0.53  (zenon_Vwe != zenon_Vnc)
% 0.20/0.53  (zenon_Vpg != zenon_Vxe)
% 0.20/0.53  (zenon_Vde != zenon_Vrd)
% 0.20/0.53  (zenon_Vre != zenon_Vec)
% 0.20/0.53  (zenon_Vde != zenon_Vdc)
% 0.20/0.53  (zenon_Vde != zenon_Veb)
% 0.20/0.53  (zenon_Vhe != zenon_Vua)
% 0.20/0.53  (zenon_Vhg != zenon_Vyc)
% 0.20/0.53  (zenon_Vlf != zenon_Vie)
% 0.20/0.53  (zenon_Vhe != zenon_Vcd)
% 0.20/0.53  (zenon_Vvf != zenon_Vcd)
% 0.20/0.53  (zenon_Vxg != zenon_Vza)
% 0.20/0.53  (zenon_Vlf != zenon_Vua)
% 0.20/0.53  (zenon_Vqf != zenon_Vtc)
% 0.20/0.53  (zenon_Vtg != zenon_Vob)
% 0.20/0.53  (zenon_Vjh != zenon_Vza)
% 0.20/0.53  (p1 zenon_Vbh)
% 0.20/0.53  (p2 zenon_Vfa)
% 0.20/0.53  (zenon_Vhg != zenon_Vcd)
% 0.20/0.53  (zenon_Vfh != zenon_Vee)
% 0.20/0.53  (zenon_Vre != zenon_Vnd)
% 0.20/0.53  (zenon_Vtg != zenon_Vab)
% 0.20/0.53  (zenon_Vbh != zenon_Vdc)
% 0.20/0.53  (-. (p1 zenon_Vxe))
% 0.20/0.53  (zenon_Vme != zenon_Vxd)
% 0.20/0.53  (zenon_Vbf != zenon_Vtc)
% 0.20/0.53  (zenon_Vxg != zenon_Vse)
% 0.20/0.53  (zenon_Vfh != zenon_Vsd)
% 0.20/0.53  (zenon_Vre != zenon_Vkb)
% 0.20/0.53  (-. (p1 Tau_3))
% 0.20/0.53  (zenon_Vqf != zenon_Vdd)
% 0.20/0.53  (zenon_Vvf != zenon_Vtc)
% 0.20/0.53  (zenon_Vlg != zenon_Vxd)
% 0.20/0.53  (zenon_Vre != zenon_Vxc)
% 0.20/0.53  (zenon_Vhg != zenon_Vjc)
% 0.20/0.53  (zenon_Vwe != zenon_Veb)
% 0.20/0.53  (zenon_Vre != zenon_Vwd)
% 0.20/0.53  (zenon_Vde != zenon_Vdd)
% 0.20/0.53  (zenon_Vhe != zenon_Vcf)
% 0.20/0.53  (zenon_Vqf != zenon_Vkb)
% 0.20/0.53  (zenon_Vqf != zenon_Vpa)
% 0.20/0.53  (zenon_Vhg != zenon_Veb)
% 0.20/0.53  (p1 zenon_Vlg)
% 0.20/0.53  (zenon_Vhg != zenon_Vua)
% 0.20/0.53  (zenon_Vme != zenon_Voc)
% 0.20/0.53  (-. (p1 zenon_Vrd))
% 0.20/0.53  (zenon_Vgf != zenon_Vid)
% 0.20/0.53  (zenon_Vde != zenon_Vtc)
% 0.20/0.53  (zenon_Vbh != zenon_Vxc)
% 0.20/0.53  (zenon_Vfh != zenon_Vsc)
% 0.20/0.53  (zenon_Vme != zenon_Vxc)
% 0.20/0.53  (zenon_Vxg != zenon_Vwd)
% 0.20/0.53  (zenon_Vfh != zenon_Vmd)
% 0.20/0.53  (zenon_Vme != zenon_Vpb)
% 0.20/0.53  (zenon_Vhg != zenon_Vpa)
% 0.20/0.53  (zenon_Vbh != zenon_Vnc)
% 0.20/0.53  (zenon_Vdg != zenon_Veb)
% 0.20/0.53  (zenon_Vwe != zenon_Vpa)
% 0.20/0.53  (zenon_Vlf != zenon_Vsc)
% 0.20/0.53  (zenon_Vwe != zenon_Vjc)
% 0.20/0.53  (zenon_Vbf != zenon_Vfb)
% 0.20/0.53  (zenon_Vre != zenon_Vic)
% 0.20/0.53  (r1 zenon_Vye zenon_Vdf)
% 0.20/0.53  (-. (p1 zenon_Vse))
% 0.20/0.53  (r1 zenon_X6 zenon_Vmh)
% 0.20/0.53  (zenon_Vdg != zenon_Vrf)
% 0.20/0.53  (zenon_Vwe != zenon_Vhf)
% 0.20/0.53  (zenon_Vlg != zenon_Vhd)
% 0.20/0.53  (zenon_Vmh != zenon_Vkb)
% 0.20/0.53  (zenon_Vxg != zenon_Vcf)
% 0.20/0.53  (zenon_Vre != zenon_Vhd)
% 0.20/0.53  (zenon_Vhe != zenon_Voc)
% 0.20/0.53  (zenon_Vmh != zenon_Vcf)
% 0.20/0.53  (-. (p1 zenon_Vnd))
% 0.20/0.53  (zenon_Vtg != zenon_Vxe)
% 0.20/0.53  (zenon_Vhe != zenon_Vyc)
% 0.20/0.53  (-. (p1 zenon_Vza))
% 0.20/0.53  (zenon_Vre != zenon_Vrf)
% 0.20/0.53  (zenon_Vdg != zenon_Vab)
% 0.20/0.53  (zenon_Vde != zenon_Vua)
% 0.20/0.53  (zenon_Vhg != zenon_Vzb)
% 0.20/0.53  (r1 zenon_Vaa zenon_Vza)
% 0.20/0.53  (zenon_Vjh != zenon_Vne)
% 0.20/0.53  (zenon_Vfh != zenon_Vtc)
% 0.20/0.53  (zenon_Vde != zenon_Vmd)
% 0.20/0.53  (zenon_Vde != zenon_Vnc)
% 0.20/0.53  (zenon_Vde != zenon_Vqa)
% 0.20/0.53  (r1 zenon_Vx zenon_Vob)
% 0.20/0.53  (zenon_Vlf != zenon_Vpa)
% 0.20/0.53  (zenon_Vfh != zenon_Vxd)
% 0.20/0.53  (zenon_Vme != zenon_Vua)
% 0.20/0.53  (zenon_Vbh != zenon_Veb)
% 0.20/0.53  (zenon_Vxg != zenon_Vxd)
% 0.20/0.53  (zenon_Vlf != zenon_Vfb)
% 0.20/0.53  (zenon_Vfh != zenon_Vie)
% 0.20/0.53  (zenon_Vmh != zenon_Vpa)
% 0.20/0.53  (zenon_Vjh != zenon_Vsd)
% 0.20/0.53  (zenon_Vxg != zenon_Vjc)
% 0.20/0.53  (zenon_Vlf != zenon_Vne)
% 0.20/0.53  (zenon_Vxg != zenon_Vsc)
% 0.20/0.53  (r1 zenon_Vs zenon_Vnc)
% 0.20/0.53  (zenon_Vqf != zenon_Vxe)
% 0.20/0.53  (zenon_Vbh != zenon_Vrd)
% 0.20/0.53  (zenon_Vjh != zenon_Vfb)
% 0.20/0.53  (zenon_Vme != zenon_Vnd)
% 0.20/0.53  (zenon_Vfh != zenon_Vpa)
% 0.20/0.53  (r1 zenon_Vef zenon_Vhf)
% 0.20/0.53  (zenon_Vlf != zenon_Vxe)
% 0.20/0.53  (zenon_Vmh != zenon_Vcd)
% 0.20/0.53  (zenon_Vxg != zenon_Vxc)
% 0.20/0.53  (zenon_Vqf != zenon_Vxc)
% 0.20/0.53  (zenon_Vpg != zenon_Vie)
% 0.20/0.53  (zenon_Vbh != zenon_Vid)
% 0.20/0.53  (zenon_Vvf != zenon_Vcf)
% 0.20/0.53  (zenon_Vlg != zenon_Vsd)
% 0.20/0.53  (zenon_Vlf != zenon_Vwf)
% 0.20/0.53  (zenon_Vdg != zenon_Vpa)
% 0.20/0.53  (r1 zenon_Vka zenon_Vla)
% 0.20/0.53  (zenon_Vlg != zenon_Vcf)
% 0.20/0.53  (zenon_Vjh != zenon_Vdc)
% 0.20/0.53  (zenon_Vgf != zenon_Vjb)
% 0.20/0.53  (zenon_Vdg != zenon_Vpb)
% 0.20/0.53  (-. (p1 zenon_Vdc))
% 0.20/0.53  (zenon_Vjh != zenon_Vnc)
% 0.20/0.53  (zenon_Vbf != zenon_Vva)
% 0.20/0.53  (zenon_Vvf != zenon_Vae)
% 0.20/0.53  (zenon_Vde != zenon_Vub)
% 0.20/0.53  (zenon_Vlg != zenon_Vpa)
% 0.20/0.53  (r1 zenon_Vpe zenon_Vse)
% 0.20/0.53  (zenon_Vfh != zenon_Vdc)
% 0.20/0.53  (zenon_Vfh != zenon_Vua)
% 0.20/0.53  (r1 zenon_Vke zenon_Vle)
% 0.20/0.53  (zenon_Vme != zenon_Vqa)
% 0.20/0.53  (zenon_Vlg != zenon_Vyc)
% 0.20/0.53  (zenon_Vxg != zenon_Vhf)
% 0.20/0.53  (zenon_Vfh != zenon_Vae)
% 0.20/0.53  (zenon_Vqf != zenon_Vrd)
% 0.20/0.53  (zenon_Vxg != zenon_Vzb)
% 0.20/0.53  (zenon_Vme != zenon_Vne)
% 0.20/0.53  (zenon_Vhg != zenon_Vsc)
% 0.20/0.53  (zenon_Vre != zenon_Vcd)
% 0.20/0.53  (zenon_Vlg != zenon_Vab)
% 0.20/0.53  (zenon_Vbh != zenon_Vtc)
% 0.20/0.53  (zenon_Vvf != zenon_Vab)
% 0.20/0.53  (zenon_Vde != zenon_Vnd)
% 0.20/0.53  (zenon_Vwe != zenon_Vid)
% 0.20/0.53  (zenon_Vwe != zenon_Vpb)
% 0.20/0.53  (zenon_Vlf != zenon_Vwd)
% 0.20/0.53  (zenon_Vlf != zenon_Vob)
% 0.20/0.53  (zenon_Vbh != zenon_Vkb)
% 0.20/0.53  (zenon_Vbf != zenon_Vjb)
% 0.20/0.53  (zenon_Vbf != zenon_Vdc)
% 0.20/0.53  (zenon_Vbh != zenon_Vpb)
% 0.20/0.53  (zenon_Vjh != zenon_Vjb)
% 0.20/0.53  (zenon_Vlg != zenon_Vva)
% 0.20/0.53  (zenon_Vtg != zenon_Vpa)
% 0.20/0.53  (zenon_Vjh != zenon_Vua)
% 0.20/0.53  (r1 zenon_Vdf zenon_Vif)
% 0.20/0.53  (zenon_Vgf != zenon_Vzb)
% 0.20/0.53  (zenon_Vdg != zenon_Vyc)
% 0.20/0.53  (zenon_Vvf != zenon_Vtb)
% 0.20/0.53  (zenon_Vfh != zenon_Vfb)
% 0.20/0.53  (zenon_Vjh != zenon_Vtb)
% 0.20/0.53  (zenon_Vdg != zenon_Vkb)
% 0.20/0.53  (-. (p1 zenon_Vee))
% 0.20/0.53  (zenon_Vlg != zenon_Vzb)
% 0.20/0.53  (zenon_Vme != zenon_Vcf)
% 0.20/0.53  (zenon_Vhe != zenon_Vmf)
% 0.20/0.53  (zenon_Vbf != zenon_Vjc)
% 0.20/0.53  (zenon_Vmh != zenon_Vza)
% 0.20/0.53  (zenon_Vxg != zenon_Voc)
% 0.20/0.53  (zenon_Vmh != zenon_Vrd)
% 0.20/0.53  (zenon_Vgf != zenon_Vxe)
% 0.20/0.53  (zenon_Vpg != zenon_Vcf)
% 0.20/0.53  (zenon_Vbf != zenon_Vkb)
% 0.20/0.53  (zenon_Vmh != zenon_Vmf)
% 0.20/0.53  (zenon_Vgf != zenon_Vyb)
% 0.20/0.53  (zenon_Vwe != zenon_Vva)
% 0.20/0.53  (zenon_Vhg != zenon_Vsd)
% 0.20/0.53  (zenon_Vjh != zenon_Vmd)
% 0.20/0.53  (zenon_Vdg != zenon_Vtb)
% 0.20/0.53  (zenon_Vde != zenon_Vfb)
% 0.20/0.53  (zenon_Vbf != zenon_Vrf)
% 0.20/0.53  (zenon_Vlg != zenon_Veb)
% 0.20/0.53  (zenon_Vwe != zenon_Vzb)
% 0.20/0.53  (zenon_Vhe != zenon_Vae)
% 0.20/0.53  (zenon_Vme != zenon_Vec)
% 0.20/0.53  (-. (p1 zenon_Vec))
% 0.20/0.53  (zenon_Vlg != zenon_Vyb)
% 0.20/0.53  (zenon_Vmh != zenon_Vwf)
% 0.20/0.53  (zenon_Vlf != zenon_Vmd)
% 0.20/0.53  (r1 zenon_Vch zenon_Vfh)
% 0.20/0.53  (r1 zenon_Vof zenon_Vpf)
% 0.20/0.53  (zenon_Vgf != zenon_Vxd)
% 0.20/0.53  (zenon_Vlf != zenon_Vdc)
% 0.20/0.53  (zenon_Vxg != zenon_Vkb)
% 0.20/0.53  (zenon_Vtg != zenon_Vdd)
% 0.20/0.53  (zenon_Vgf != zenon_Vob)
% 0.20/0.53  (zenon_Vlf != zenon_Vrd)
% 0.20/0.53  (zenon_Vpg != zenon_Vmd)
% 0.20/0.53  (zenon_Vre != zenon_Vid)
% 0.20/0.53  (zenon_Vlg != zenon_Vdc)
% 0.20/0.53  (zenon_Vre != zenon_Vpa)
% 0.20/0.53  (zenon_Vdg != zenon_Vza)
% 0.20/0.53  (zenon_Vvf != zenon_Vyb)
% 0.20/0.53  (zenon_Vfh != zenon_Vdd)
% 0.20/0.53  (zenon_Vdg != zenon_Vee)
% 0.20/0.53  (zenon_Vbh != zenon_Vwd)
% 0.20/0.53  (r1 zenon_Vfe zenon_Vie)
% 0.20/0.53  (zenon_Vhg != zenon_Vse)
% 0.20/0.53  (zenon_Vqf != zenon_Vrf)
% 0.20/0.53  (zenon_Vxg != zenon_Vrf)
% 0.20/0.53  (zenon_Vtg != zenon_Vid)
% 0.20/0.53  (zenon_Vre != zenon_Vee)
% 0.20/0.53  (zenon_Vtg != zenon_Voc)
% 0.20/0.53  (zenon_Vlf != zenon_Vub)
% 0.20/0.53  (zenon_Vbh != zenon_Vqa)
% 0.20/0.53  (zenon_Vhg != zenon_Vkb)
% 0.20/0.53  (zenon_Vgf != zenon_Vcf)
% 0.20/0.53  (zenon_Vwe != zenon_Vjb)
% 0.20/0.53  (zenon_Vfa != zenon_Vma)
% 0.20/0.53  (p1 zenon_Vvf)
% 0.20/0.53  (zenon_Vtg != zenon_Vtb)
% 0.20/0.53  (-. (p1 zenon_Vob))
% 0.20/0.53  (zenon_Vme != zenon_Vjc)
% 0.20/0.53  (zenon_Vfh != zenon_Vic)
% 0.20/0.53  (zenon_Vhe != zenon_Vyb)
% 0.20/0.53  (zenon_Vmh != zenon_Vrf)
% 0.20/0.53  (zenon_Vhe != zenon_Vdd)
% 0.20/0.53  (zenon_Vhg != zenon_Vnc)
% 0.20/0.53  (zenon_Vmh != zenon_Vdd)
% 0.20/0.53  (zenon_Vlf != zenon_Vmf)
% 0.20/0.53  (zenon_Vdg != zenon_Vcf)
% 0.20/0.53  (zenon_Vjh != zenon_Vae)
% 0.20/0.53  (zenon_Vjh != zenon_Vxc)
% 0.20/0.53  (zenon_Vwe != zenon_Vob)
% 0.20/0.53  (r1 zenon_Vfa zenon_Vga)
% 0.20/0.53  (zenon_Vvf != zenon_Vxc)
% 0.20/0.53  (-. (p1 zenon_Vhd))
% 0.20/0.53  (zenon_Vwe != zenon_Vkb)
% 0.20/0.53  (zenon_Vbf != zenon_Vab)
% 0.20/0.53  (zenon_Vfh != zenon_Voc)
% 0.20/0.53  (-. (p1 zenon_Vjc))
% 0.20/0.53  (zenon_Vtg != zenon_Vnc)
% 0.20/0.53  (zenon_Vvf != zenon_Vhd)
% 0.20/0.53  (zenon_Vlf != zenon_Vpb)
% 0.20/0.53  (zenon_Vbf != zenon_Vxd)
% 0.20/0.53  (zenon_Vtg != zenon_Vcd)
% 0.20/0.53  (zenon_Vbf != zenon_Vpa)
% 0.20/0.53  (zenon_Vde != zenon_Vie)
% 0.20/0.53  (zenon_Vgf != zenon_Vyc)
% 0.20/0.53  (zenon_Vbf != zenon_Vdd)
% 0.20/0.53  (zenon_Vdg != zenon_Vub)
% 0.20/0.53  (zenon_Vjh != zenon_Vxe)
% 0.20/0.53  (zenon_Vfh != zenon_Vcf)
% 0.20/0.53  (zenon_Vme != zenon_Vcd)
% 0.20/0.53  (zenon_Vre != zenon_Vza)
% 0.20/0.53  (zenon_Vwe != zenon_Vsc)
% 0.20/0.53  (zenon_Vlg != zenon_Vmd)
% 0.20/0.53  (zenon_Vwe != zenon_Vqa)
% 0.20/0.53  (zenon_Vme != zenon_Vob)
% 0.20/0.53  (zenon_Vme != zenon_Vwf)
% 0.20/0.53  (zenon_Vbf != zenon_Vid)
% 0.20/0.53  (r1 zenon_Vag zenon_Vdg)
% 0.20/0.53  (zenon_Vde != zenon_Vne)
% 0.20/0.53  (zenon_Vgf != zenon_Vnd)
% 0.20/0.53  (zenon_Vlf != zenon_Vqa)
% 0.20/0.53  (r1 zenon_Vdf zenon_Vef)
% 0.20/0.53  (-. (p1 zenon_Vmf))
% 0.20/0.53  (zenon_Vhg != zenon_Vmd)
% 0.20/0.53  (zenon_Vhe != zenon_Vrf)
% 0.20/0.53  (zenon_Vde != zenon_Vjb)
% 0.20/0.53  (zenon_Vmh != zenon_Vsc)
% 0.20/0.53  (zenon_Vmh != zenon_Vee)
% 0.20/0.53  (zenon_Vpg != zenon_Vzb)
% 0.20/0.53  (zenon_Vhe != zenon_Vid)
% 0.20/0.53  (zenon_Vvf != zenon_Vob)
% 0.20/0.53  (zenon_Vlf != zenon_Vza)
% 0.20/0.53  (zenon_Vhe != zenon_Vee)
% 0.20/0.53  (zenon_Vhe != zenon_Vxc)
% 0.20/0.53  (zenon_Vjh != zenon_Vtc)
% 0.20/0.53  (zenon_Vbf != zenon_Veb)
% 0.20/0.53  (r1 zenon_Vsf zenon_Vxf)
% 0.20/0.53  (-. (p3 zenon_Vga))
% 0.20/0.53  (zenon_Vhe != zenon_Veb)
% 0.20/0.53  (zenon_Vde != zenon_Vwf)
% 0.20/0.53  (zenon_Vvf != zenon_Vua)
% 0.20/0.53  (r1 zenon_Vze zenon_Vaf)
% 0.20/0.53  (zenon_Vvf != zenon_Vwf)
% 0.20/0.53  (zenon_Vdg != zenon_Vtc)
% 0.20/0.53  (zenon_Vwe != zenon_Vub)
% 0.20/0.53  (zenon_Vlf != zenon_Vcf)
% 0.20/0.53  (zenon_Vbf != zenon_Vie)
% 0.20/0.53  (r1 zenon_Vq zenon_Vxc)
% 0.20/0.53  (zenon_Vhe != zenon_Vzb)
% 0.20/0.53  (zenon_Vgf != zenon_Vpb)
% 0.20/0.53  (zenon_Vfh != zenon_Vwf)
% 0.20/0.53  (zenon_Vqf != zenon_Vub)
% 0.20/0.53  (p1 zenon_Vhg)
% 0.20/0.53  (r1 zenon_X5 zenon_Vwd)
% 0.20/0.53  (zenon_Vdg != zenon_Vwd)
% 0.20/0.53  (zenon_Vgf != zenon_Vhf)
% 0.20/0.53  (zenon_Vpg != zenon_Vwf)
% 0.20/0.53  (zenon_Vgf != zenon_Vie)
% 0.20/0.53  (zenon_Vlf != zenon_Vxd)
% 0.20/0.53  (zenon_Vbh != zenon_Vua)
% 0.20/0.53  (zenon_Vpg != zenon_Vhf)
% 0.20/0.53  (zenon_Vlg != zenon_Vua)
% 0.20/0.53  (zenon_Vlf != zenon_Vee)
% 0.20/0.53  (zenon_Vjh != zenon_Vyc)
% 0.20/0.53  (zenon_Vbh != zenon_Vec)
% 0.20/0.53  (zenon_Vlf != zenon_Vhd)
% 0.20/0.53  (zenon_Vvf != zenon_Voc)
% 0.20/0.53  (zenon_Vbh != zenon_Vse)
% 0.20/0.53  (zenon_Vvf != zenon_Vqa)
% 0.20/0.53  (zenon_Vfh != zenon_Vhd)
% 0.20/0.53  (zenon_Vlg != zenon_Vhf)
% 0.20/0.53  (zenon_Vtg != zenon_Vxc)
% 0.20/0.53  (zenon_Vhe != zenon_Vic)
% 0.20/0.53  (zenon_Vdg != zenon_Vrd)
% 0.20/0.53  (zenon_Vme != zenon_Vkb)
% 0.20/0.53  (zenon_Vxg != zenon_Vyc)
% 0.20/0.53  (zenon_Vmh != zenon_Vfb)
% 0.20/0.53  (zenon_Vlg != zenon_Vee)
% 0.20/0.53  (zenon_Vme != zenon_Vee)
% 0.20/0.53  (zenon_Vde != zenon_Vxc)
% 0.20/0.53  (zenon_Vbh != zenon_Vza)
% 0.20/0.53  (-. (p1 zenon_Vwd))
% 0.20/0.53  (-. (p1 zenon_Vfb))
% 0.20/0.53  (zenon_Vmh != zenon_Vab)
% 0.20/0.53  (zenon_Vjh != zenon_Vie)
% 0.20/0.53  (zenon_Vwe != zenon_Vse)
% 0.20/0.53  (zenon_Vre != zenon_Vzb)
% 0.20/0.53  (-. (p1 zenon_Vsd))
% 0.20/0.53  (zenon_Vxg != zenon_Vrd)
% 0.20/0.53  (r1 zenon_Vfe zenon_Vge)
% 0.20/0.53  (zenon_Vvf != zenon_Vxe)
% 0.20/0.53  (zenon_Vfh != zenon_Vse)
% 0.20/0.53  (zenon_Vme != zenon_Vtb)
% 0.20/0.53  (zenon_Vgf != zenon_Vpa)
% 0.20/0.53  (zenon_Vgf != zenon_Voc)
% 0.20/0.53  (zenon_Vhg != zenon_Vnd)
% 0.20/0.53  (zenon_Vwe != zenon_Vne)
% 0.20/0.53  (zenon_Vre != zenon_Vjb)
% 0.20/0.53  (zenon_Vvf != zenon_Vse)
% 0.20/0.53  (zenon_Vgf != zenon_Vmd)
% 0.20/0.53  (zenon_Vpg != zenon_Vnd)
% 0.20/0.53  (zenon_Vgf != zenon_Vva)
% 0.20/0.53  (zenon_Vqf != zenon_Vae)
% 0.20/0.53  (zenon_Vlg != zenon_Vjc)
% 0.20/0.53  (zenon_Vjh != zenon_Vub)
% 0.20/0.53  (zenon_Vqf != zenon_Vza)
% 0.20/0.53  (zenon_Vhe != zenon_Vdc)
% 0.20/0.53  (zenon_Vhe != zenon_Vva)
% 0.20/0.53  (zenon_Vde != zenon_Vmf)
% 0.20/0.53  (zenon_Vde != zenon_Vsc)
% 0.20/0.53  (zenon_Vbf != zenon_Vne)
% 0.20/0.53  (zenon_Vme != zenon_Vae)
% 0.20/0.53  (zenon_Vtg != zenon_Vtc)
% 0.20/0.53  (zenon_Vde != zenon_Vec)
% 0.20/0.53  (zenon_Vhe != zenon_Vwd)
% 0.20/0.53  (zenon_Vlg != zenon_Voc)
% 0.20/0.53  (zenon_Vme != zenon_Vab)
% 0.20/0.53  (zenon_Vdg != zenon_Vae)
% 0.20/0.53  (p1 zenon_Vwe)
% 0.20/0.53  (zenon_Vtg != zenon_Vdc)
% 0.20/0.53  (zenon_Vbh != zenon_Vie)
% 0.20/0.53  (zenon_Vde != zenon_Vee)
% 0.20/0.53  (zenon_Vhe != zenon_Vjc)
% 0.20/0.53  (zenon_Vhe != zenon_Vnc)
% 0.20/0.53  (zenon_Vgf != zenon_Vsd)
% 0.20/0.53  (zenon_Vbf != zenon_Vcd)
% 0.20/0.53  (zenon_Vqf != zenon_Vjc)
% 0.20/0.53  (zenon_Vme != zenon_Vub)
% 0.20/0.53  (zenon_Vde != zenon_Vhd)
% 0.20/0.53  (zenon_Vqf != zenon_Vic)
% 0.20/0.53  (zenon_Vhg != zenon_Vfb)
% 0.20/0.53  (zenon_Vqf != zenon_Vie)
% 0.20/0.53  (zenon_Vfh != zenon_Vza)
% 0.20/0.53  (zenon_Vtg != zenon_Vyb)
% 0.20/0.53  (zenon_Vlf != zenon_Vsd)
% 0.20/0.53  (zenon_Vgf != zenon_Vxc)
% 0.20/0.53  (r1 zenon_Vu zenon_Vdc)
% 0.20/0.53  (zenon_Vbh != zenon_Vhf)
% 0.20/0.53  (p1 zenon_Vme)
% 0.20/0.53  (zenon_Vgf != zenon_Vec)
% 0.20/0.53  (r1 zenon_Vif zenon_Vjf)
% 0.20/0.53  (zenon_Vpg != zenon_Vtc)
% 0.20/0.53  (zenon_Vxg != zenon_Vcd)
% 0.20/0.53  (zenon_Vvf != Tau_3)
% 0.20/0.53  (zenon_Vdg != Tau_3)
% 0.20/0.53  (zenon_Vqf != Tau_3)
% 0.20/0.53  (zenon_Vhg != Tau_3)
% 0.20/0.53  (zenon_Vlf != Tau_3)
% 0.20/0.53  (zenon_Vlg != Tau_3)
% 0.20/0.53  (zenon_Vgf != Tau_3)
% 0.20/0.53  (zenon_Vpg != Tau_3)
% 0.20/0.53  (zenon_Vbf != Tau_3)
% 0.20/0.53  (zenon_Vtg != Tau_3)
% 0.20/0.53  (zenon_Vtg != zenon_Vhf)
% 0.20/0.53  (zenon_Vwe != Tau_3)
% 0.20/0.53  (zenon_Vxg != Tau_3)
% 0.20/0.53  (zenon_Vre != Tau_3)
% 0.20/0.53  (zenon_Vbh != Tau_3)
% 0.20/0.53  (zenon_Vme != Tau_3)
% 0.20/0.53  (zenon_Vfh != Tau_3)
% 0.20/0.53  (zenon_Vhe != Tau_3)
% 0.20/0.53  (zenon_Vjh != Tau_3)
% 0.20/0.53  (zenon_Vde != Tau_3)
% 0.20/0.53  (zenon_Vmh != Tau_3)
% 0.20/0.53  (zenon_Vgf != zenon_Vnc)
% 0.20/0.53  (zenon_Vqf != zenon_Vhd)
% 0.20/0.53  (zenon_Vmh != zenon_Vse)
% 0.20/0.53  (zenon_Vwe != zenon_Vwd)
% 0.20/0.53  (zenon_Vvf != zenon_Vee)
% 0.20/0.53  (zenon_Vqf != zenon_Vob)
% 0.20/0.53  (zenon_Vqf != zenon_Vyc)
% 0.20/0.53  (zenon_Vdg != zenon_Vjc)
% 0.20/0.53  (r1 zenon_Voe zenon_Vte)
% 0.20/0.53  (zenon_Vbh != zenon_Vne)
% 0.20/0.53  (zenon_Vde != zenon_Vzb)
% 0.20/0.53  (zenon_Vlg != zenon_Vnd)
% 0.20/0.53  (zenon_Vgf != zenon_Vdc)
% 0.20/0.53  (zenon_Vre != zenon_Vie)
% 0.20/0.53  (zenon_Vgf != zenon_Vsc)
% 0.20/0.53  (zenon_Vme != zenon_Vnc)
% 0.20/0.53  (zenon_Vlg != zenon_Vxe)
% 0.20/0.53  (r1 zenon_Vue zenon_Vxe)
% 0.20/0.53  (zenon_Vgf != zenon_Vwd)
% 0.20/0.53  (zenon_Vbf != zenon_Vwf)
% 0.20/0.53  (zenon_Vtg != zenon_Vmd)
% 0.20/0.53  (zenon_Vqf != zenon_Vid)
% 0.20/0.53  (zenon_Vdg != zenon_Vdd)
% 0.20/0.53  (zenon_Vde != zenon_Vse)
% 0.20/0.53  (zenon_Vhe != zenon_Vtc)
% 0.20/0.53  (r1 zenon_Vv zenon_Vyb)
% 0.20/0.53  (zenon_Vqf != zenon_Vjb)
% 0.20/0.53  (zenon_Vlg != zenon_Vse)
% 0.20/0.53  (zenon_Vmh != zenon_Vnc)
% 0.20/0.53  (zenon_Vxg != zenon_Vua)
% 0.20/0.53  (zenon_Vmh != zenon_Vpb)
% 0.20/0.53  (zenon_Vdg != zenon_Vnd)
% 0.20/0.53  (zenon_Vme != zenon_Vic)
% 0.20/0.53  (zenon_Vhg != zenon_Vee)
% 0.20/0.53  (zenon_Vde != zenon_Vsd)
% 0.20/0.53  (zenon_Vfh != zenon_Vzb)
% 0.20/0.53  (r1 zenon_Vye zenon_Vze)
% 0.20/0.53  (zenon_Vgf != zenon_Vtc)
% 0.20/0.53  (zenon_Vpg != zenon_Vub)
% 0.20/0.53  (zenon_Vfh != zenon_Vwd)
% 0.20/0.53  (zenon_Vjh != zenon_Vva)
% 0.20/0.53  (r1 zenon_Vif zenon_Vnf)
% 0.20/0.53  (-. (p1 zenon_Vtc))
% 0.20/0.53  (-. (p1 zenon_Vnc))
% 0.20/0.53  (zenon_Vhe != zenon_Vec)
% 0.20/0.53  (zenon_Vgf != zenon_Vjc)
% 0.20/0.53  (r1 zenon_Vje zenon_Vke)
% 0.20/0.53  (zenon_Vpg != zenon_Vrf)
% 0.20/0.53  (zenon_Vxg != zenon_Vnc)
% 0.20/0.53  (-. (p1 zenon_Vic))
% 0.20/0.53  (zenon_Vbh != zenon_Vpa)
% 0.20/0.53  (zenon_Vlf != zenon_Vrf)
% 0.20/0.53  (zenon_Vbh != zenon_Vae)
% 0.20/0.53  (r1 zenon_Vnf zenon_Vsf)
% 0.20/0.53  (zenon_Vbf != zenon_Vub)
% 0.20/0.53  (zenon_Vjh != zenon_Vob)
% 0.20/0.53  (zenon_Vmh != zenon_Vid)
% 0.20/0.53  (zenon_Vhg != zenon_Vhf)
% 0.20/0.53  (zenon_Vqf != zenon_Vmf)
% 0.20/0.53  (r1 zenon_Vm zenon_Vrd)
% 0.20/0.53  (zenon_Vme != zenon_Vhf)
% 0.20/0.53  (r1 zenon_Vnf zenon_Vof)
% 0.20/0.53  (-. (p1 zenon_Voc))
% 0.20/0.53  (zenon_Vtg != zenon_Vie)
% 0.20/0.53  (zenon_Vbf != zenon_Vxe)
% 0.20/0.53  (zenon_Vqf != zenon_Vnc)
% 0.20/0.53  (zenon_Vhg != zenon_Vub)
% 0.20/0.53  (zenon_Vtg != zenon_Vcf)
% 0.20/0.53  (zenon_Vlg != zenon_Vjb)
% 0.20/0.53  (zenon_Vre != zenon_Vob)
% 0.20/0.53  (zenon_Vpg != zenon_Vee)
% 0.20/0.53  (zenon_Vbh != zenon_Vub)
% 0.20/0.53  (-. (p1 zenon_Vie))
% 0.20/0.53  (zenon_Vvf != zenon_Vjb)
% 0.20/0.53  (zenon_Vxg != zenon_Vyb)
% 0.20/0.53  (r1 zenon_Vze zenon_Vcf)
% 0.20/0.53  (-. (p1 zenon_Vid))
% 0.20/0.53  (zenon_Vxg != zenon_Vqa)
% 0.20/0.53  (zenon_Vgf != zenon_Vae)
% 0.20/0.53  (zenon_Vbf != zenon_Vrd)
% 0.20/0.53  (zenon_Vbf != zenon_Vpb)
% 0.20/0.53  (zenon_Vmh != zenon_Vdc)
% 0.20/0.53  (zenon_Vjh != zenon_Voc)
% 0.20/0.53  (zenon_Vbf != zenon_Vnc)
% 0.20/0.53  (zenon_Vdg != zenon_Vwf)
% 0.20/0.53  (zenon_Vdg != zenon_Vsc)
% 0.20/0.53  (zenon_Vlf != zenon_Vnc)
% 0.20/0.53  (zenon_Vwe != zenon_Vcd)
% 0.20/0.53  (zenon_Vlf != zenon_Vdd)
% 0.20/0.53  (zenon_Vqf != zenon_Vva)
% 0.20/0.53  (zenon_Vhg != zenon_Vxe)
% 0.20/0.53  (zenon_Vjh != zenon_Vwd)
% 0.20/0.53  (zenon_Vxg != zenon_Vfb)
% 0.20/0.53  (zenon_Vhe != zenon_Vhf)
% 0.20/0.53  (zenon_Vjh != zenon_Vhf)
% 0.20/0.53  (-. (p1 zenon_Veb))
% 0.20/0.53  (zenon_Vbh != zenon_Vob)
% 0.20/0.53  (zenon_Vvf != zenon_Vhf)
% 0.20/0.53  (zenon_Vbh != zenon_Vfb)
% 0.20/0.53  (zenon_Vhe != zenon_Vnd)
% 0.20/0.53  (zenon_Vhg != zenon_Vwf)
% 0.20/0.53  (-. (p1 zenon_Vua))
% 0.20/0.53  (zenon_Vde != zenon_Vcf)
% 0.20/0.53  (zenon_Vhg != zenon_Vtc)
% 0.20/0.53  (zenon_Vxg != zenon_Vmf)
% 0.20/0.53  (zenon_Vgf != zenon_Vse)
% 0.20/0.53  (zenon_Vbf != zenon_Vob)
% 0.20/0.53  (zenon_Vmh != zenon_Vyc)
% 0.20/0.53  (zenon_Vdg != zenon_Vcd)
% 0.20/0.53  (zenon_Vqf != zenon_Vwf)
% 0.20/0.53  (zenon_Vme != zenon_Vhd)
% 0.20/0.53  (zenon_Vtg != zenon_Vjc)
% 0.20/0.53  (zenon_Vbf != zenon_Vmf)
% 0.20/0.53  (zenon_Vbh != zenon_Vyb)
% 0.20/0.53  (zenon_Vjh != zenon_Vzb)
% 0.20/0.53  (zenon_Vbh != zenon_Voc)
% 0.20/0.53  (zenon_Vbh != zenon_Vab)
% 0.20/0.53  (zenon_Vhg != zenon_Vae)
% 0.20/0.53  (zenon_Vlf != zenon_Vcd)
% 0.20/0.53  (zenon_Vmh != zenon_Vhf)
% 0.20/0.53  (zenon_Vqf != zenon_Vmd)
% 0.20/0.53  (zenon_Vjh != zenon_Veb)
% 0.20/0.53  (zenon_Vlg != zenon_Vdd)
% 0.20/0.53  (zenon_Vtg != zenon_Vrd)
% 0.20/0.53  (zenon_Vgf != zenon_Vwf)
% 0.20/0.53  (zenon_Vvf != zenon_Vxd)
% 0.20/0.53  (zenon_Vdg != zenon_Vyb)
% 0.20/0.53  (zenon_Vbh != zenon_Vwf)
% 0.20/0.53  (zenon_Vpg != zenon_Vhd)
% 0.20/0.53  (zenon_Vlg != zenon_Vrd)
% 0.20/0.53  (zenon_Vgf != zenon_Veb)
% 0.20/0.53  (zenon_Vfh != zenon_Vrf)
% 0.20/0.53  (zenon_Vre != zenon_Voc)
% 0.20/0.53  (zenon_Vlg != zenon_Vmf)
% 0.20/0.53  (zenon_Vmh != zenon_Vnd)
% 0.20/0.53  (zenon_Vlg != zenon_Vtb)
% 0.20/0.53  (zenon_Vxg != zenon_Vub)
% 0.20/0.53  (zenon_Vjh != zenon_Vqa)
% 0.20/0.53  (zenon_Vme != zenon_Vrd)
% 0.20/0.53  (zenon_Vwe != zenon_Vza)
% 0.20/0.53  (zenon_Vme != zenon_Vfb)
% 0.20/0.53  (zenon_Vde != zenon_Vxe)
% 0.20/0.53  (zenon_Vpg != zenon_Vxd)
% 0.20/0.53  (zenon_Vbf != zenon_Vua)
% 0.20/0.53  (zenon_Vbh != zenon_Vnd)
% 0.20/0.53  (zenon_Vhg != zenon_Vxc)
% 0.20/0.53  (zenon_Vbh != zenon_Vmf)
% 0.20/0.53  (zenon_Vhg != zenon_Vdd)
% 0.20/0.53  (zenon_Vlg != zenon_Vtc)
% 0.20/0.53  (zenon_Vde != zenon_Vyc)
% 0.20/0.53  (zenon_Vfh != zenon_Vub)
% 0.20/0.53  (zenon_Vdg != zenon_Vjb)
% 0.20/0.53  (zenon_Vvf != zenon_Veb)
% 0.20/0.53  (zenon_Vhe != zenon_Vxe)
% 0.20/0.53  (zenon_Vre != zenon_Vnc)
% 0.20/0.53  (zenon_Vtg != zenon_Vqa)
% 0.20/0.53  (r1 Tau_2 zenon_Vfe)
% 0.20/0.53  (r1 Tau_2 zenon_Vje)
% 0.20/0.53  (-. (p1 zenon_Vjb))
% 0.20/0.53  (zenon_Vhg != zenon_Vva)
% 0.20/0.53  (zenon_Vqf != zenon_Vcd)
% 0.20/0.53  (zenon_Vre != zenon_Vdc)
% 0.20/0.53  (zenon_Vde != zenon_Vab)
% 0.20/0.53  (zenon_Vqf != zenon_Vtb)
% 0.20/0.53  (zenon_Vmh != zenon_Vic)
% 0.20/0.53  (zenon_Vwe != zenon_Vtb)
% 0.20/0.53  (zenon_Vhg != zenon_Vne)
% 0.20/0.53  (zenon_Vxg != zenon_Vab)
% 0.20/0.53  (zenon_Vgf != zenon_Vne)
% 0.20/0.53  (zenon_Vhg != zenon_Vec)
% 0.20/0.53  (-. (p4 zenon_X4))
% 0.20/0.53  (zenon_Vxg != zenon_Vie)
% 0.20/0.53  (r1 zenon_Vz zenon_Veb)
% 0.20/0.53  (zenon_Vre != zenon_Vae)
% 0.20/0.53  (zenon_Vtg != zenon_Vic)
% 0.20/0.53  (zenon_Vtg != zenon_Vza)
% 0.20/0.53  (zenon_Vhg != zenon_Vrd)
% 0.20/0.53  (zenon_Vlf != zenon_Vjb)
% 0.20/0.53  (r1 zenon_Vba zenon_Vua)
% 0.20/0.53  (zenon_Vtg != zenon_Vne)
% 0.20/0.53  (zenon_Vpg != zenon_Vtb)
% 0.20/0.53  (zenon_Vqf != zenon_Voc)
% 0.20/0.53  (zenon_Vxg != zenon_Vxe)
% 0.20/0.53  (zenon_Vpg != zenon_Vid)
% 0.20/0.53  (zenon_Vfa != zenon_Vzf)
% 0.20/0.53  (zenon_Vpg != zenon_Vmf)
% 0.20/0.53  (zenon_Vbh != zenon_Vxe)
% 0.20/0.53  (zenon_Vqf != zenon_Vyb)
% 0.20/0.53  (zenon_Vlg != zenon_Vie)
% 0.20/0.53  (zenon_Vjh != zenon_Vcf)
% 0.20/0.53  (zenon_Vvf != zenon_Vsd)
% 0.20/0.53  (p1 zenon_Vgf)
% 0.20/0.53  (zenon_Vme != zenon_Vzb)
% 0.20/0.53  (zenon_Vlg != zenon_Vqa)
% 0.20/0.53  (zenon_Vvf != zenon_Vkb)
% 0.20/0.53  (zenon_Vtg != zenon_Vfb)
% 0.20/0.53  (r1 zenon_Vp zenon_Vcd)
% 0.20/0.53  (zenon_Vqf != zenon_Vdc)
% 0.20/0.53  (zenon_Vvf != zenon_Vjc)
% 0.20/0.53  (zenon_Vxg != zenon_Vee)
% 0.20/0.53  (zenon_Vjh != zenon_Vjc)
% 0.20/0.53  (-. (p1 zenon_Vwf))
% 0.20/0.53  (-. (p1 zenon_Vub))
% 0.20/0.53  (zenon_Vlf != zenon_Vae)
% 0.20/0.53  (zenon_Vvf != zenon_Vdd)
% 0.20/0.53  (zenon_Vde != zenon_Vwd)
% 0.20/0.53  (zenon_Vpg != zenon_Vkb)
% 0.20/0.53  (zenon_Vwe != zenon_Vsd)
% 0.20/0.53  (zenon_Vtg != zenon_Vzb)
% 0.20/0.53  (-. (p1 zenon_Vkb))
% 0.20/0.53  (zenon_Vvf != zenon_Vrd)
% 0.20/0.53  (zenon_Vbh != zenon_Vmd)
% 0.20/0.53  (zenon_Vbf != zenon_Vic)
% 0.20/0.53  (zenon_Vgf != zenon_Vqa)
% 0.20/0.53  (zenon_Vtg != zenon_Vjb)
% 0.20/0.53  (zenon_Vme != zenon_Vza)
% 0.20/0.53  (r1 Tau_0 Tau_2)
% 0.20/0.53  (zenon_Vlf != zenon_Veb)
% 0.20/0.53  (zenon_Vlg != zenon_Vwd)
% 0.20/0.53  (zenon_Vfh != zenon_Vnc)
% 0.20/0.53  (r1 zenon_Vmg zenon_Vpg)
% 0.20/0.53  (zenon_Vvf != zenon_Vza)
% 0.20/0.53  (zenon_Vfh != zenon_Vxc)
% 0.20/0.53  (zenon_Vgf != zenon_Vza)
% 0.20/0.53  (zenon_Vtg != zenon_Vee)
% 0.20/0.53  (zenon_Vjh != zenon_Vpb)
% 0.20/0.53  (zenon_Vmh != zenon_Vtc)
% 0.20/0.53  (zenon_Vbf != zenon_Vxc)
% 0.20/0.53  (r1 zenon_Vt zenon_Vic)
% 0.20/0.53  (zenon_Vlf != zenon_Vtb)
% 0.20/0.53  (zenon_Vpg != zenon_Vae)
% 0.20/0.53  (zenon_Vhe != zenon_Vjb)
% 0.20/0.53  (zenon_Vgf != zenon_Vua)
% 0.20/0.53  (zenon_Vlg != zenon_Vrf)
% 0.20/0.53  (zenon_Vhg != zenon_Vpb)
% 0.20/0.53  (zenon_Vre != zenon_Vmd)
% 0.20/0.53  (zenon_Vvf != zenon_Vid)
% 0.20/0.53  (zenon_Vdg != zenon_Vne)
% 0.20/0.53  (zenon_Vpg != zenon_Voc)
% 0.20/0.53  (zenon_Vhe != zenon_Vne)
% 0.20/0.53  (zenon_Vlf != zenon_Vid)
% 0.20/0.53  (zenon_Vfh != zenon_Veb)
% 0.20/0.53  (zenon_Vpg != zenon_Vyc)
% 0.20/0.53  (zenon_Vfh != zenon_Vrd)
% 0.20/0.53  (zenon_Vhg != zenon_Vid)
% 0.20/0.53  (zenon_Vjh != zenon_Vdd)
% 0.20/0.53  (zenon_Vpg != zenon_Vsc)
% 0.20/0.53  (zenon_Vpg != zenon_Vpa)
% 0.20/0.53  (zenon_Vjh != zenon_Vsc)
% 0.20/0.53  (zenon_Vjh != zenon_Vcd)
% 0.20/0.53  (zenon_Vtg != zenon_Vxd)
% 0.20/0.53  (zenon_Vtg != zenon_Vwf)
% 0.20/0.53  (zenon_Vbh != zenon_Vva)
% 0.20/0.53  (zenon_Vre != zenon_Vab)
% 0.20/0.53  (zenon_Vdg != zenon_Vob)
% 0.20/0.53  (zenon_Vmh != zenon_Vob)
% 0.20/0.53  (r1 zenon_Vr zenon_Vsc)
% 0.20/0.53  (zenon_Vhe != zenon_Vfb)
% 0.20/0.53  (zenon_Vxg != zenon_Vob)
% 0.20/0.53  (zenon_Vre != zenon_Vxe)
% 0.20/0.53  (p1 zenon_Vdg)
% 0.20/0.53  (zenon_Vlg != zenon_Vcd)
% 0.20/0.53  (zenon_Vtg != zenon_Vub)
% 0.20/0.53  (zenon_Vvf != zenon_Vnc)
% 0.20/0.53  (zenon_Vpg != zenon_Vjb)
% 0.20/0.53  (zenon_Vme != zenon_Vva)
% 0.20/0.53  (zenon_Vlf != zenon_Vyb)
% 0.20/0.53  (zenon_Vvf != zenon_Vdc)
% 0.20/0.53  (zenon_Vpg != zenon_Vwd)
% 0.20/0.53  (zenon_Vre != zenon_Vcf)
% 0.20/0.53  (zenon_Vhe != zenon_Vsd)
% 0.20/0.53  (r1 zenon_Vof zenon_Vrf)
% 0.20/0.53  (r1 zenon_Vtf zenon_Vuf)
% 0.20/0.53  (zenon_Vwe != zenon_Vxd)
% 0.20/0.53  (r1 zenon_Vpe zenon_Vqe)
% 0.20/0.53  (zenon_Vwe != zenon_Vae)
% 0.20/0.53  (zenon_Vre != zenon_Vfb)
% 0.20/0.53  (r1 zenon_Vy zenon_Vjb)
% 0.20/0.53  (zenon_Vpg != zenon_Vic)
% 0.20/0.53  (zenon_Vpg != zenon_Vrd)
% 0.20/0.53  (zenon_Vlg != zenon_Vpb)
% 0.20/0.53  (zenon_Vtg != zenon_Veb)
% 0.20/0.53  (zenon_Vde != zenon_Vva)
% 0.20/0.53  (zenon_Vdg != zenon_Vqa)
% 0.20/0.53  (zenon_Vvf != zenon_Vpb)
% 0.20/0.53  (zenon_Vvf != zenon_Vwd)
% 0.20/0.53  (p1 zenon_Vjh)
% 0.20/0.53  (zenon_Vlf != zenon_Vxc)
% 0.20/0.53  (zenon_Vhg != zenon_Vic)
% 0.20/0.53  (zenon_Vre != zenon_Vhf)
% 0.20/0.53  (zenon_Vtg != zenon_Vhd)
% 0.20/0.53  (zenon_Vqf != zenon_Vpb)
% 0.20/0.53  (zenon_Vwe != zenon_Vtc)
% 0.20/0.53  (zenon_Vxg != zenon_Vpb)
% 0.20/0.53  (zenon_Vme != zenon_Vpa)
% 0.20/0.53  (p1 zenon_Vde)
% 0.20/0.53  (zenon_Vwe != zenon_Voc)
% 0.20/0.53  (zenon_Vre != zenon_Vub)
% 0.20/0.53  (zenon_Vfh != zenon_Vnd)
% 0.20/0.53  (zenon_Vwe != zenon_Vua)
% 0.20/0.53  (zenon_Vlf != zenon_Vkb)
% 0.20/0.53  (zenon_Vxg != zenon_Vwf)
% 0.20/0.53  (zenon_Vgf != zenon_Vcd)
% 0.20/0.53  (zenon_Vwe != zenon_Vhd)
% 0.20/0.53  (r1 zenon_Vue zenon_Vve)
% 0.20/0.53  (zenon_Vlf != zenon_Voc)
% 0.20/0.53  (zenon_Vlf != zenon_Vjc)
% 0.20/0.53  (-. (p2 zenon_Vzf))
% 0.20/0.53  (zenon_Vhg != zenon_Vxd)
% 0.20/0.53  (zenon_Vhe != zenon_Vza)
% 0.20/0.53  (zenon_Vmh != zenon_Vie)
% 0.20/0.53  (zenon_Vqf != zenon_Vcf)
% 0.20/0.53  (zenon_Vhg != zenon_Vie)
% 0.20/0.53  (zenon_Vpg != zenon_Vsd)
% 0.20/0.53  (zenon_Vhg != zenon_Vhd)
% 0.20/0.53  (zenon_Vtg != zenon_Vrf)
% 0.20/0.53  (p1 zenon_Vfh)
% 0.20/0.53  (zenon_Vme != zenon_Vdc)
% 0.20/0.53  (zenon_Vbh != zenon_Vhd)
% 0.20/0.53  (zenon_Vgf != zenon_Vrf)
% 0.20/0.53  (zenon_Vhe != zenon_Vrd)
% 0.20/0.53  (zenon_Vme != zenon_Veb)
% 0.20/0.53  (zenon_Vqf != zenon_Vne)
% 0.20/0.53  (zenon_Vqf != zenon_Vnd)
% 0.20/0.53  (zenon_Vbh != zenon_Vsc)
% 0.20/0.53  (zenon_Vmh != zenon_Vva)
% 0.20/0.53  (zenon_Vmh != zenon_Vjb)
% 0.20/0.53  (zenon_Vwe != zenon_Vfb)
% 0.20/0.53  (zenon_Vwe != zenon_Vdd)
% 0.20/0.53  (zenon_Vhe != zenon_Vie)
% 0.20/0.53  (zenon_Vlg != zenon_Vec)
% 0.20/0.53  (zenon_Vwe != zenon_Vrd)
% 0.20/0.53  (zenon_Vme != zenon_Vwd)
% 0.20/0.53  (-. (p2 zenon_Vma))
% 0.20/0.53  (zenon_Vvf != zenon_Vsc)
% 0.20/0.53  (zenon_Vde != zenon_Vkb)
% 0.20/0.53  (zenon_Vre != zenon_Vdd)
% 0.20/0.53  (zenon_Vlf != zenon_Vva)
% 0.20/0.53  (-. (p1 zenon_Vva))
% 0.20/0.53  (zenon_Vjh != zenon_Vxd)
% 0.20/0.53  (zenon_Vbh != zenon_Vrf)
% 0.20/0.53  (zenon_Vxg != zenon_Vhd)
% 0.20/0.53  (zenon_Vdg != zenon_Vec)
% 0.20/0.53  (zenon_Vre != zenon_Vtb)
% 0.20/0.53  (zenon_Vde != zenon_Vhf)
% 0.20/0.53  (zenon_Vgf != zenon_Vhd)
% 0.20/0.53  (zenon_Vlf != zenon_Vab)
% 0.20/0.53  (zenon_Vmh != zenon_Vxe)
% 0.20/0.53  (zenon_Vpg != zenon_Vne)
% 0.20/0.53  (zenon_Vvf != zenon_Vpa)
% 0.20/0.53  (zenon_Vfh != zenon_Vtb)
% 0.20/0.53  (zenon_Vpg != zenon_Vec)
% 0.20/0.53  *)
% 0.20/0.53  (* NO-PROOF *)
% 0.20/0.53  % SZS status GaveUp
% 0.20/0.53  Number of rewrites on terms: 0
% 0.20/0.53  Number of rewrites on props: 0
% 0.20/0.53  nodes searched: 1354
% 0.20/0.53  max branch formulas: 1499
% 0.20/0.53  proof nodes created: 0
% 0.20/0.53  formulas created: 7697
% 0.20/0.53  
%------------------------------------------------------------------------------