↑ Up

ZenonModulo---0.5.0.UNK-Non.f

View TPTP
Problem Process solution in
SystemOnTSTP Download .tgz 
%------------------------------------------------------------------------------
% File     : ZenonModulo---0.5.0
% Problem  : LCL660+1.020 : 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:20 PM UTC 2026

% Result   : Unknown 1.77s 2.11s
% Output   : None 
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02  % Problem  : LCL660+1.020 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.02  % Command  : run_zenon_modulo %d %s
% 0.09/0.35  % Computer : n019.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 : Fri Sep  4 17:03:53 UTC 2026
% 0.09/0.36  % CPUTime  : 
% 1.77/2.10  Zenon error: exhausted search space without finding a proof
% 1.77/2.10  (* Current branch:
% 1.77/2.10  (-. (p3 Tau_20))
% 1.77/2.10  (zenon_Vt != zenon_Vsf)
% 1.77/2.10  (r1 zenon_Vjb zenon_Vkb)
% 1.77/2.10  (-. (p1 zenon_Vgi))
% 1.77/2.10  (zenon_Vr != Tau_13)
% 1.77/2.10  (zenon_Vm != Tau_13)
% 1.77/2.10  (zenon_Vo != Tau_13)
% 1.77/2.10  (zenon_Vt != Tau_13)
% 1.77/2.10  (zenon_Vm != zenon_Vvi)
% 1.77/2.10  (zenon_Vt != zenon_Vle)
% 1.77/2.10  (zenon_Vm != zenon_Vkf)
% 1.77/2.10  (-. (p4 zenon_Vec))
% 1.77/2.10  (-. (p3 zenon_Vve))
% 1.77/2.10  (-. (p4 zenon_Vyi))
% 1.77/2.10  (zenon_Vo != zenon_Vdc)
% 1.77/2.10  (-. (p3 zenon_Vbg))
% 1.77/2.10  (-. (p1 zenon_Vvi))
% 1.77/2.10  (zenon_Vo != zenon_Vgi)
% 1.77/2.10  (zenon_Vo != zenon_Vle)
% 1.77/2.10  (zenon_Vo != zenon_Vfc)
% 1.77/2.10  (-. (p3 zenon_Vbd))
% 1.77/2.10  (zenon_Vt != zenon_Vqc)
% 1.77/2.10  (zenon_Vo != zenon_Vtf)
% 1.77/2.10  (zenon_Vo != zenon_Vgc)
% 1.77/2.10  (r1 zenon_Vrf zenon_Vsf)
% 1.77/2.10  (zenon_Vm != zenon_Vvj)
% 1.77/2.10  (zenon_Vo != zenon_Vmd)
% 1.77/2.10  (-. (p2 zenon_Vib))
% 1.77/2.10  (-. (p1 zenon_Vyc))
% 1.77/2.10  (-. (p3 zenon_Vgi))
% 1.77/2.10  (r1 Tau_21 zenon_Vuj)
% 1.77/2.10  (-. (p3 zenon_Vnd))
% 1.77/2.10  (zenon_Vm != zenon_Vad)
% 1.77/2.10  (zenon_Vt != zenon_Vhg)
% 1.77/2.10  (-. (p1 zenon_Vug))
% 1.77/2.10  (zenon_Vr != zenon_Vce)
% 1.77/2.10  (zenon_Vr != zenon_Vph)
% 1.77/2.10  (-. (p3 zenon_Vlb))
% 1.77/2.10  (-. (p1 zenon_Vhh))
% 1.77/2.10  (-. (p3 zenon_Vuh))
% 1.77/2.10  (-. (p2 zenon_Vle))
% 1.77/2.10  (zenon_Vo != zenon_Vuh)
% 1.77/2.10  (zenon_Vo != zenon_Vad)
% 1.77/2.10  (-. (p1 zenon_Vlb))
% 1.77/2.10  (zenon_Vm != zenon_Vce)
% 1.77/2.10  (-. (p3 Tau_12))
% 1.77/2.10  (-. (p2 zenon_Vcg))
% 1.77/2.10  (r1 zenon_Vhh zenon_Vih)
% 1.77/2.10  (zenon_Vr != zenon_Vzc)
% 1.77/2.10  (zenon_Vt != zenon_Vqg)
% 1.77/2.10  (zenon_Vt != zenon_Vtf)
% 1.77/2.10  (-. (p2 zenon_Vec))
% 1.77/2.10  (-. (p4 zenon_Vhh))
% 1.77/2.10  (r1 zenon_Vt zenon_Vu)
% 1.77/2.10  (zenon_Vr != zenon_Vmd)
% 1.77/2.10  (zenon_Vo != zenon_Vcf)
% 1.77/2.10  (zenon_Vm != zenon_Vkk)
% 1.77/2.10  (zenon_Vt != zenon_Vfc)
% 1.77/2.10  (zenon_Vt != zenon_Vu)
% 1.77/2.10  (-. (p4 Tau_20))
% 1.77/2.10  (zenon_Vm != zenon_Vpc)
% 1.77/2.10  (-. (p1 zenon_Vud))
% 1.77/2.10  (zenon_Vm != zenon_Vn)
% 1.77/2.10  (zenon_Vm != zenon_Vsd)
% 1.77/2.10  (-. (p4 zenon_Vtd))
% 1.77/2.10  (zenon_Vm != zenon_Vee)
% 1.77/2.10  (r1 Tau_14 zenon_Vhh)
% 1.77/2.10  (r1 zenon_Vic zenon_Vpc)
% 1.77/2.10  (zenon_Vo != zenon_Vud)
% 1.77/2.10  (-. (p1 zenon_Vmd))
% 1.77/2.10  (zenon_Vt != zenon_Vri)
% 1.77/2.10  (zenon_Vt != zenon_Vbd)
% 1.77/2.10  (-. (p1 zenon_Vad))
% 1.77/2.10  (-. (p4 zenon_Vpi))
% 1.77/2.10  (p1 zenon_Vt)
% 1.77/2.10  (r1 Tau_11 zenon_Vrf)
% 1.77/2.10  (r1 Tau_6 zenon_Vdc)
% 1.77/2.10  (zenon_Vr != Tau_21)
% 1.77/2.10  (zenon_Vm != Tau_21)
% 1.77/2.10  (zenon_Vo != Tau_21)
% 1.77/2.10  (zenon_Vt != zenon_Vej)
% 1.77/2.10  (zenon_Vt != Tau_21)
% 1.77/2.10  (zenon_Vo != zenon_Vxg)
% 1.77/2.10  (zenon_Vt != zenon_Vlf)
% 1.77/2.10  (r1 Tau_5 zenon_Vib)
% 1.77/2.10  (zenon_Vr != zenon_Vka)
% 1.77/2.10  (zenon_Vr != zenon_Vnd)
% 1.77/2.10  (zenon_Vr != zenon_Vdi)
% 1.77/2.10  (r1 zenon_Vph zenon_Vqh)
% 1.77/2.10  (zenon_Vr != zenon_Vrf)
% 1.77/2.10  (-. (p1 zenon_Vrf))
% 1.77/2.10  (zenon_Vo != zenon_Vwb)
% 1.77/2.10  (r1 zenon_Vbf zenon_Vcf)
% 1.77/2.10  (zenon_Vr != zenon_Vje)
% 1.77/2.10  (-. (p3 zenon_Vkb))
% 1.77/2.10  (r1 Tau_18 zenon_Vyi)
% 1.77/2.10  (-. (p3 zenon_Vlf))
% 1.77/2.10  (zenon_Vm != zenon_Vnd)
% 1.77/2.10  (zenon_Vr != zenon_Vve)
% 1.77/2.10  (zenon_Vr != zenon_Vnj)
% 1.77/2.10  (zenon_Vr != zenon_Vvg)
% 1.77/2.10  (zenon_Vm != zenon_Vef)
% 1.77/2.10  (zenon_Vt != zenon_Vqh)
% 1.77/2.10  (-. (p2 Tau_17))
% 1.77/2.10  (zenon_Vm != zenon_Vke)
% 1.77/2.10  (r1 zenon_Vch zenon_Vdh)
% 1.77/2.10  (r1 zenon_Vkg zenon_Vpg)
% 1.77/2.10  (r1 zenon_Vxh zenon_Vci)
% 1.77/2.10  (-. (p1 zenon_Vte))
% 1.77/2.10  (r1 zenon_X26 zenon_Vo)
% 1.77/2.10  (zenon_Vo != zenon_Vvi)
% 1.77/2.10  (-. (p4 Tau_16))
% 1.77/2.10  (zenon_Vr != zenon_Vaf)
% 1.77/2.10  (-. (p4 zenon_Vug))
% 1.77/2.10  (zenon_Vm != zenon_Vak)
% 1.77/2.10  (-. (p3 zenon_Vne))
% 1.77/2.10  (-. (p2 Tau_8))
% 1.77/2.10  (zenon_Vt != zenon_Vkg)
% 1.77/2.10  (zenon_Vt != zenon_Vpi)
% 1.77/2.10  (r1 Tau_0 Tau_11)
% 1.77/2.10  (zenon_Vo != zenon_Vbd)
% 1.77/2.10  (-. (p3 Tau_9))
% 1.77/2.10  (r1 Tau_0 Tau_22)
% 1.77/2.10  (-. (p4 zenon_Vch))
% 1.77/2.10  (-. (p2 zenon_Vud))
% 1.77/2.10  (zenon_Vr != zenon_Vn)
% 1.77/2.10  (zenon_Vr != zenon_Vqg)
% 1.77/2.10  (zenon_Vr != zenon_Vkk)
% 1.77/2.10  (-. (p3 zenon_Vig))
% 1.77/2.10  (zenon_Vo != zenon_Vci)
% 1.77/2.10  (-. (p1 Tau_23))
% 1.77/2.10  (-. (p1 zenon_Vvf))
% 1.77/2.10  (r1 zenon_Vef zenon_Vkf)
% 1.77/2.10  (-. (p1 zenon_Vyi))
% 1.77/2.10  (-. (p2 zenon_Vbg))
% 1.77/2.10  (zenon_Vm != zenon_Vtf)
% 1.77/2.10  (zenon_Vt != zenon_Vii)
% 1.77/2.10  (zenon_Vm != zenon_Vmf)
% 1.77/2.10  (-. (p1 zenon_Vak))
% 1.77/2.10  (-. (p3 zenon_Vcg))
% 1.77/2.10  (-. (p3 zenon_Vcf))
% 1.77/2.10  (-. (p4 zenon_Vtf))
% 1.77/2.10  (-. (p1 zenon_Vdi))
% 1.77/2.10  (-. (p2 zenon_Vch))
% 1.77/2.10  (zenon_Vm != zenon_Vdg)
% 1.77/2.10  (zenon_Vo != zenon_Vp)
% 1.77/2.10  (zenon_Vo != zenon_Vdh)
% 1.77/2.10  (zenon_Vt != zenon_Vgc)
% 1.77/2.10  (-. (p3 Tau_1))
% 1.77/2.10  (-. (p2 zenon_Vn))
% 1.77/2.10  (zenon_Vr != zenon_Vle)
% 1.77/2.10  (-. (p4 Tau_12))
% 1.77/2.10  (-. (p3 zenon_Vke))
% 1.77/2.10  (-. (p4 zenon_Vsc))
% 1.77/2.10  (-. (p2 zenon_Vbf))
% 1.77/2.10  (-. (p3 zenon_Vmi))
% 1.77/2.10  (r1 Tau_0 Tau_12)
% 1.77/2.10  (-. (p1 zenon_Vvh))
% 1.77/2.10  (-. (p3 zenon_Vce))
% 1.77/2.10  (zenon_Vo != zenon_Vkf)
% 1.77/2.10  (r1 zenon_Vlf zenon_Vmf)
% 1.77/2.10  (-. (p3 zenon_Vld))
% 1.77/2.10  (r1 zenon_Vvi zenon_Vwi)
% 1.77/2.10  (-. (p2 zenon_Vkk))
% 1.77/2.10  (-. (p3 zenon_Vte))
% 1.77/2.10  (-. (p1 zenon_Vdd))
% 1.77/2.10  (-. (p2 zenon_Vte))
% 1.77/2.10  (zenon_Vm != zenon_Vjb)
% 1.77/2.10  (-. (p1 Tau_22))
% 1.77/2.10  (-. (p3 zenon_Vej))
% 1.77/2.10  (-. (p1 zenon_Vdh))
% 1.77/2.10  (r1 zenon_Vbg zenon_Vcg)
% 1.77/2.10  (-. (p1 Tau_11))
% 1.77/2.10  (-. (p2 zenon_Vje))
% 1.77/2.10  (zenon_Vr != zenon_Vjb)
% 1.77/2.10  (r1 zenon_Vgc zenon_Vhc)
% 1.77/2.10  (-. (p3 zenon_Vaf))
% 1.77/2.10  (r1 zenon_X24 zenon_Vr)
% 1.77/2.10  (zenon_Vr != zenon_Vvi)
% 1.77/2.10  (-. (p3 zenon_Vug))
% 1.77/2.10  (-. (p3 zenon_Vmf))
% 1.77/2.10  (zenon_Vm != zenon_Vkb)
% 1.77/2.10  (-. (p1 zenon_Vaf))
% 1.77/2.10  (-. (p1 zenon_Vne))
% 1.77/2.10  (zenon_Vo != zenon_Vhg)
% 1.77/2.10  (-. (p4 zenon_Vbd))
% 1.77/2.10  (r1 Tau_9 zenon_Vje)
% 1.77/2.10  (-. (p2 zenon_Vde))
% 1.77/2.10  (zenon_Vr != zenon_Vmi)
% 1.77/2.10  (-. (p4 zenon_Vph))
% 1.77/2.10  (r1 zenon_Vo zenon_Vp)
% 1.77/2.10  (r1 zenon_Vqh zenon_Vrh)
% 1.77/2.10  (-. (p4 zenon_Vde))
% 1.77/2.10  (-. (p1 zenon_Vxb))
% 1.77/2.10  (zenon_Vr != zenon_Vrc)
% 1.77/2.10  (zenon_Vo != zenon_Vqc)
% 1.77/2.10  (-. (p1 zenon_Vcf))
% 1.77/2.10  (-. (p3 zenon_Vqh))
% 1.77/2.10  (zenon_Vr != zenon_Vlb)
% 1.77/2.10  (-. (p2 zenon_Vvg))
% 1.77/2.10  (-. (p2 zenon_Vyi))
% 1.77/2.10  (-. (p3 zenon_Vud))
% 1.77/2.10  (zenon_Vr != Tau_9)
% 1.77/2.10  (zenon_Vm != Tau_9)
% 1.77/2.10  (zenon_Vo != Tau_9)
% 1.77/2.10  (zenon_Vt != Tau_9)
% 1.77/2.10  (r1 zenon_Vte zenon_Vue)
% 1.77/2.10  (zenon_Vt != zenon_Vaj)
% 1.77/2.10  (-. (p3 zenon_Vdc))
% 1.77/2.10  (-. (p2 Tau_13))
% 1.77/2.10  (zenon_Vt != Tau_11)
% 1.77/2.10  (zenon_Vt != zenon_Vwb)
% 1.77/2.10  (-. (p2 zenon_Vad))
% 1.77/2.10  (zenon_Vm != zenon_Vkg)
% 1.77/2.10  (-. (p3 zenon_Vkd))
% 1.77/2.10  (-. (p1 zenon_Vdg))
% 1.77/2.10  (zenon_Vr != zenon_Vaj)
% 1.77/2.10  (zenon_Vt != zenon_Vfk)
% 1.77/2.10  (-. (p2 Tau_5))
% 1.77/2.10  (-. (p4 zenon_Vgi))
% 1.77/2.10  (-. (p4 zenon_Vpc))
% 1.77/2.10  (zenon_Vo != zenon_Vje)
% 1.77/2.10  (r1 zenon_Vle zenon_Vme)
% 1.77/2.10  (-. (p3 zenon_Vpc))
% 1.77/2.10  (-. (p3 zenon_Vxg))
% 1.77/2.10  (zenon_Vo != zenon_Vec)
% 1.77/2.10  (-. (p2 zenon_Vmd))
% 1.77/2.10  (r1 zenon_Vqc zenon_Vrc)
% 1.77/2.10  (-. (p3 zenon_Vhj))
% 1.77/2.10  (-. (p3 zenon_Vxb))
% 1.77/2.10  (-. (p3 zenon_Vib))
% 1.77/2.10  (-. (p2 zenon_Vkg))
% 1.77/2.10  (-. (p2 zenon_Vef))
% 1.77/2.10  (-. (p4 zenon_Vdc))
% 1.77/2.10  (zenon_Vo != zenon_Vne)
% 1.77/2.10  (-. (p1 zenon_Vsc))
% 1.77/2.10  (zenon_Vo != zenon_Vub)
% 1.77/2.10  (r1 zenon_Vsf zenon_Vtf)
% 1.77/2.10  (zenon_Vr != zenon_Vyi)
% 1.77/2.10  (zenon_Vt != zenon_Vmd)
% 1.77/2.10  (-. (p2 zenon_Vrf))
% 1.77/2.10  (-. (p2 zenon_Vih))
% 1.77/2.10  (-. (p1 zenon_Vle))
% 1.77/2.10  (-. (p3 zenon_Vpi))
% 1.77/2.10  (-. (p1 Tau_2))
% 1.77/2.10  (zenon_Vt != zenon_Vxb)
% 1.77/2.10  (zenon_Vt != zenon_Vjj)
% 1.77/2.10  (r1 zenon_Vgi zenon_Vhi)
% 1.77/2.10  (zenon_Vo != zenon_Vtd)
% 1.77/2.10  (-. (p2 zenon_Vka))
% 1.77/2.10  (-. (p2 zenon_Vaf))
% 1.77/2.10  (zenon_Vo != zenon_Vph)
% 1.77/2.10  (-. (p4 zenon_Vue))
% 1.77/2.10  (-. (p3 zenon_Vad))
% 1.77/2.10  (r1 zenon_Vqg zenon_Vrg)
% 1.77/2.10  (-. (p1 zenon_Vcg))
% 1.77/2.10  (-. (p3 zenon_Vdi))
% 1.77/2.10  (-. (p1 zenon_Vkf))
% 1.77/2.10  (-. (p2 zenon_Vii))
% 1.77/2.10  (r1 zenon_Vzc zenon_Vad)
% 1.77/2.10  (-. (p2 zenon_Vyc))
% 1.77/2.10  (-. (p2 Tau_3))
% 1.77/2.10  (-. (p2 zenon_Vvi))
% 1.77/2.10  (r1 zenon_Vxb zenon_Vyb)
% 1.77/2.10  (zenon_Vt != zenon_Vph)
% 1.77/2.10  (-. (p4 zenon_Vce))
% 1.77/2.10  (r1 zenon_Vnb zenon_Vub)
% 1.77/2.10  (r1 zenon_Vsc zenon_Vtc)
% 1.77/2.10  (r1 zenon_X28 zenon_Vjk)
% 1.77/2.10  (zenon_Vm != zenon_Vrc)
% 1.77/2.10  (zenon_Vr != zenon_Vcf)
% 1.77/2.10  (zenon_Vm != zenon_Vyi)
% 1.77/2.10  (zenon_Vm != zenon_Vcf)
% 1.77/2.10  (zenon_Vo != zenon_Vch)
% 1.77/2.10  (zenon_Vo != zenon_Vyi)
% 1.77/2.10  (-. (p4 zenon_Vle))
% 1.77/2.10  (-. (p4 zenon_Vcg))
% 1.77/2.10  (zenon_Vr != zenon_Vvj)
% 1.77/2.10  (zenon_Vt != Tau_7)
% 1.77/2.10  (zenon_Vt != zenon_Vkb)
% 1.77/2.10  (zenon_Vo != zenon_Vee)
% 1.77/2.10  (-. (p2 zenon_Vkh))
% 1.77/2.10  (zenon_Vt != zenon_Vaf)
% 1.77/2.10  (zenon_Vo != zenon_Vcg)
% 1.77/2.10  (zenon_Vo != zenon_Vaf)
% 1.77/2.10  (r1 Tau_20 zenon_Vpj)
% 1.77/2.10  (zenon_Vr != zenon_Vxg)
% 1.77/2.10  (zenon_Vo != zenon_Vve)
% 1.77/2.10  (r1 zenon_X27 zenon_Vt)
% 1.77/2.10  (r1 zenon_Vih zenon_Vjh)
% 1.77/2.10  (zenon_Vo != zenon_Vzc)
% 1.77/2.10  (r1 zenon_Vug zenon_Vvg)
% 1.77/2.10  (r1 Tau_0 Tau_18)
% 1.77/2.10  (-. (p1 zenon_Vzc))
% 1.77/2.10  (r1 zenon_Vqj zenon_Vtj)
% 1.77/2.10  (zenon_Vt != zenon_Vhj)
% 1.77/2.10  (zenon_Vt != zenon_Vjb)
% 1.77/2.10  (-. (p1 Tau_8))
% 1.77/2.10  (-. (p2 zenon_Vbd))
% 1.77/2.10  (-. (p3 zenon_Vrf))
% 1.77/2.10  (zenon_Vt != zenon_Vdd)
% 1.77/2.10  (r1 Tau_7 zenon_Vyc)
% 1.77/2.10  (r1 zenon_Vde zenon_Vee)
% 1.77/2.10  (r1 zenon_Vmd zenon_Vnd)
% 1.77/2.10  (-. (p4 zenon_Vsf))
% 1.77/2.10  (zenon_Vm != zenon_Vud)
% 1.77/2.10  (-. (p4 zenon_Vjb))
% 1.77/2.10  (-. (p1 zenon_Vvj))
% 1.77/2.10  (-. (p2 zenon_Vcb))
% 1.77/2.10  (zenon_Vr != zenon_Vdc)
% 1.77/2.10  (-. (p3 zenon_Vdh))
% 1.77/2.10  (zenon_Vt != zenon_Vcf)
% 1.77/2.10  (-. (p1 zenon_Vbf))
% 1.77/2.10  (-. (p1 zenon_Vu))
% 1.77/2.10  (zenon_Vo != zenon_Vce)
% 1.77/2.10  (-. (p3 zenon_Vih))
% 1.77/2.10  (zenon_Vm != zenon_Vub)
% 1.77/2.10  (-. (p2 Tau_12))
% 1.77/2.10  (-. (p1 Tau_13))
% 1.77/2.10  (-. (p3 Tau_21))
% 1.77/2.10  (-. (p4 Tau_8))
% 1.77/2.10  (r1 zenon_Vnd zenon_Vod)
% 1.77/2.10  (-. (p3 zenon_Vzc))
% 1.77/2.10  (-. (p2 zenon_Vug))
% 1.77/2.10  (-. (p2 zenon_Vkf))
% 1.77/2.10  (zenon_Vr != zenon_Vqj)
% 1.77/2.10  (r1 Tau_0 Tau_5)
% 1.77/2.10  (-. (p4 zenon_Vci))
% 1.77/2.10  (zenon_Vt != zenon_Vwd)
% 1.77/2.10  (zenon_Vr != Tau_17)
% 1.77/2.10  (zenon_Vm != Tau_17)
% 1.77/2.10  (zenon_Vo != Tau_17)
% 1.77/2.10  (zenon_Vt != Tau_17)
% 1.77/2.10  (-. (p2 zenon_Vld))
% 1.77/2.10  (-. (p1 zenon_Vnd))
% 1.77/2.10  (zenon_Vr != Tau_20)
% 1.77/2.10  (zenon_Vm != Tau_20)
% 1.77/2.10  (zenon_Vo != Tau_20)
% 1.77/2.10  (zenon_Vt != Tau_20)
% 1.77/2.10  (-. (p1 zenon_Vib))
% 1.77/2.10  (zenon_Vm != zenon_Vlf)
% 1.77/2.10  (zenon_Vo != zenon_Vvh)
% 1.77/2.10  (r1 Tau_16 zenon_Vgi)
% 1.77/2.10  (zenon_Vm != zenon_Vaf)
% 1.77/2.10  (zenon_Vm != zenon_Vtd)
% 1.77/2.10  (-. (p4 zenon_Vhg))
% 1.77/2.10  (-. (p4 zenon_Vqc))
% 1.77/2.10  (zenon_Vm != zenon_Vci)
% 1.77/2.10  (-. (p4 zenon_Vvi))
% 1.77/2.10  (r1 zenon_Vpg zenon_Vqg)
% 1.77/2.10  (-. (p4 zenon_Vkd))
% 1.77/2.10  (zenon_Vm != zenon_Vdi)
% 1.77/2.10  (zenon_Vt != zenon_Vlb)
% 1.77/2.10  (r1 Tau_13 zenon_Vug)
% 1.77/2.10  (r1 zenon_Vvh zenon_Vwh)
% 1.77/2.10  (zenon_Vm != zenon_Vqj)
% 1.77/2.10  (zenon_Vt != zenon_Vih)
% 1.77/2.10  (-. (p1 zenon_Vnj))
% 1.77/2.10  (r1 zenon_Vii zenon_Vmi)
% 1.77/2.10  (-. (p1 zenon_Vqh))
% 1.77/2.10  (zenon_Vr != Tau_6)
% 1.77/2.10  (zenon_Vm != Tau_6)
% 1.77/2.10  (zenon_Vt != Tau_6)
% 1.77/2.10  (zenon_Vm != zenon_Vve)
% 1.77/2.10  (r1 zenon_Vdh zenon_Veh)
% 1.77/2.10  (zenon_Vt != zenon_Vvj)
% 1.77/2.10  (-. (p2 zenon_Vdi))
% 1.77/2.10  (zenon_Vm != zenon_Vch)
% 1.77/2.10  (zenon_Vo != zenon_Vbf)
% 1.77/2.10  (zenon_Vt != zenon_Vde)
% 1.77/2.10  (-. (p4 zenon_Vrf))
% 1.77/2.10  (r1 zenon_Vej zenon_Vfj)
% 1.77/2.10  (-. (p3 Tau_13))
% 1.77/2.10  (zenon_Vr != zenon_Vig)
% 1.77/2.10  (r1 zenon_Vdg zenon_Veg)
% 1.77/2.10  (-. (p4 zenon_Vwb))
% 1.77/2.10  (zenon_Vr != zenon_Via)
% 1.77/2.10  (zenon_Vm != zenon_Vih)
% 1.77/2.10  (-. (p4 zenon_Vkf))
% 1.77/2.10  (r1 zenon_Vee zenon_Vfe)
% 1.77/2.10  (-. (p1 zenon_Vdc))
% 1.77/2.10  (r1 zenon_Vyc zenon_Vzc)
% 1.77/2.10  (zenon_Vo != zenon_Vkb)
% 1.77/2.10  (-. (p3 zenon_Vwd))
% 1.77/2.10  (zenon_Vm != zenon_Vjk)
% 1.77/2.10  (r1 Tau_0 Tau_8)
% 1.77/2.10  (r1 zenon_Vke zenon_Vle)
% 1.77/2.10  (-. (p4 zenon_Vzc))
% 1.77/2.10  (zenon_Vr != zenon_Vmf)
% 1.77/2.10  (-. (p4 zenon_Vyc))
% 1.77/2.10  (zenon_Vm != zenon_Vri)
% 1.77/2.10  (zenon_Vo != zenon_Vhh)
% 1.77/2.10  (r1 zenon_Vkb zenon_Vlb)
% 1.77/2.10  (zenon_Vr != Tau_16)
% 1.77/2.10  (zenon_Vm != Tau_16)
% 1.77/2.10  (zenon_Vo != Tau_16)
% 1.77/2.10  (zenon_Vt != Tau_16)
% 1.77/2.10  (r1 Tau_0 Tau_4)
% 1.77/2.10  (r1 zenon_Vud zenon_Vvd)
% 1.77/2.10  (-. (p2 zenon_Vcf))
% 1.77/2.10  (zenon_Vm != zenon_Vgc)
% 1.77/2.10  (-. (p4 zenon_Vgc))
% 1.77/2.10  (-. (p2 zenon_Vmf))
% 1.77/2.10  (r1 Tau_0 Tau_16)
% 1.77/2.10  (-. (p1 zenon_Vph))
% 1.77/2.10  (-. (p1 zenon_Vkg))
% 1.77/2.10  (r1 zenon_Vmf zenon_Vnf)
% 1.77/2.10  (-. (p2 zenon_Vej))
% 1.77/2.10  (zenon_Vm != zenon_Vhg)
% 1.77/2.10  (-. (p3 zenon_Vle))
% 1.77/2.10  (-. (p4 zenon_Vqg))
% 1.77/2.10  (zenon_Vt != zenon_Vci)
% 1.77/2.10  (zenon_Vr != zenon_Vde)
% 1.77/2.10  (-. (p1 zenon_Vee))
% 1.77/2.10  (r1 zenon_Vtd zenon_Vud)
% 1.77/2.10  (zenon_Vr != zenon_Vib)
% 1.77/2.10  (zenon_Vo != zenon_Vue)
% 1.77/2.10  (zenon_Vm != zenon_Vqh)
% 1.77/2.10  (r1 Tau_0 Tau_21)
% 1.77/2.10  (zenon_Vr != zenon_Vbd)
% 1.77/2.10  (zenon_Vo != zenon_Vsd)
% 1.77/2.10  (zenon_Vr != zenon_Vug)
% 1.77/2.10  (zenon_Vr != zenon_Vub)
% 1.77/2.10  (zenon_Vt != Tau_23)
% 1.77/2.10  (zenon_Vr != zenon_Vld)
% 1.77/2.10  (zenon_Vm != zenon_Vph)
% 1.77/2.10  (-. (p1 zenon_Vpi))
% 1.77/2.10  (r1 zenon_Vkf zenon_Vlf)
% 1.77/2.10  (zenon_Vr != zenon_Vsd)
% 1.77/2.10  (zenon_Vo != zenon_Vqj)
% 1.77/2.10  (zenon_Vr != zenon_Vkb)
% 1.77/2.10  (zenon_Vt != zenon_Vdc)
% 1.77/2.10  (-. (p1 zenon_Vec))
% 1.77/2.10  (-. (p4 zenon_Vad))
% 1.77/2.10  (r1 Tau_19 zenon_Vhj)
% 1.77/2.10  (-. (p1 Tau_21))
% 1.77/2.10  (-. (p4 zenon_Vqh))
% 1.77/2.10  (zenon_Vr != zenon_Vs)
% 1.77/2.10  (zenon_Vm != zenon_Vld)
% 1.77/2.10  (zenon_Vt != zenon_Vkh)
% 1.77/2.10  (zenon_Vm != zenon_Vnb)
% 1.77/2.10  (-. (p4 zenon_Vlf))
% 1.77/2.10  (p2 zenon_Vm)
% 1.77/2.10  (r1 zenon_Vak zenon_Vdk)
% 1.77/2.10  (zenon_Vt != zenon_Vce)
% 1.77/2.10  (r1 Tau_0 Tau_13)
% 1.77/2.10  (zenon_Vm != zenon_Vhh)
% 1.77/2.10  (-. (p4 zenon_Vvh))
% 1.77/2.10  (-. (p3 zenon_Vsf))
% 1.77/2.10  (zenon_Vt != zenon_Vld)
% 1.77/2.10  (-. (p3 zenon_Vje))
% 1.77/2.10  (zenon_Vr != zenon_Vdg)
% 1.77/2.10  (-. (p2 zenon_Vnj))
% 1.77/2.10  (r1 zenon_Vnj zenon_Voj)
% 1.77/2.10  (r1 zenon_Vfk zenon_Vik)
% 1.77/2.10  (zenon_Vt != zenon_Vhh)
% 1.77/2.10  (zenon_Vm != zenon_Vnj)
% 1.77/2.10  (-. (p2 zenon_Vqg))
% 1.77/2.10  (zenon_Vm != zenon_Vsf)
% 1.77/2.10  (r1 Tau_15 zenon_Vuh)
% 1.77/2.10  (zenon_Vm != zenon_Vlb)
% 1.77/2.10  (-. (p1 Tau_12))
% 1.77/2.10  (-. (p1 zenon_Vtd))
% 1.77/2.10  (-. (p2 zenon_Vue))
% 1.77/2.10  (-. (p2 Tau_20))
% 1.77/2.10  (-. (p4 zenon_Vfc))
% 1.77/2.10  (r1 Tau_8 zenon_Vsd)
% 1.77/2.10  (zenon_Vo != zenon_Vpc)
% 1.77/2.10  (-. (p1 zenon_Vmi))
% 1.77/2.10  (zenon_Vr != zenon_Vue)
% 1.77/2.10  (-. (p2 zenon_Vvh))
% 1.77/2.10  (r1 Tau_23 zenon_Vek)
% 1.77/2.10  (r1 zenon_Vvb zenon_Vwb)
% 1.77/2.10  (zenon_Vr != zenon_Vkh)
% 1.77/2.10  (zenon_Vt != zenon_Vke)
% 1.77/2.10  (-. (p1 zenon_Vld))
% 1.77/2.10  (zenon_Vr != zenon_Vbg)
% 1.77/2.10  (zenon_Vt != zenon_Vig)
% 1.77/2.10  (-. (p3 zenon_Vee))
% 1.77/2.10  (zenon_Vr != zenon_Vvb)
% 1.77/2.10  (zenon_Vm != zenon_Vsc)
% 1.77/2.10  (zenon_Vt != zenon_Vyc)
% 1.77/2.10  (r1 Tau_0 Tau_19)
% 1.77/2.10  (-. (p1 zenon_Vhj))
% 1.77/2.10  (zenon_Vm != zenon_Vpi)
% 1.77/2.10  (zenon_Vo != zenon_Vmi)
% 1.77/2.10  (-. (p3 zenon_Vph))
% 1.77/2.10  (zenon_Vt != zenon_Vak)
% 1.77/2.10  (r1 zenon_Vig zenon_Vjg)
% 1.77/2.10  (-. (p1 Tau_19))
% 1.77/2.10  (-. (p1 zenon_Vej))
% 1.77/2.10  (zenon_Vm != zenon_Vmi)
% 1.77/2.10  (r1 zenon_Vaf zenon_Vbf)
% 1.77/2.10  (-. (p4 zenon_Vih))
% 1.77/2.10  (zenon_Vt != zenon_Vvf)
% 1.77/2.10  (-. (p1 Tau_14))
% 1.77/2.10  (-. (p1 zenon_Vtf))
% 1.77/2.10  (zenon_Vt != zenon_Vte)
% 1.77/2.10  (-. (p2 zenon_Vkb))
% 1.77/2.10  (zenon_Vo != zenon_Vsc)
% 1.77/2.10  (-. (p4 zenon_Vke))
% 1.77/2.10  (-. (p1 zenon_Vve))
% 1.77/2.10  (r1 zenon_Vdc zenon_Vec)
% 1.77/2.10  (-. (p4 zenon_Vnd))
% 1.77/2.10  (zenon_Vt != zenon_Vnb)
% 1.77/2.10  (-. (p4 zenon_Vvb))
% 1.77/2.10  (zenon_Vr != zenon_Vud)
% 1.77/2.10  (zenon_Vr != Tau_10)
% 1.77/2.10  (zenon_Vm != Tau_10)
% 1.77/2.10  (zenon_Vt != Tau_10)
% 1.77/2.10  (-. (p2 zenon_Vub))
% 1.77/2.10  (r1 Tau_0 Tau_1)
% 1.77/2.10  (zenon_Vr != Tau_14)
% 1.77/2.10  (zenon_Vm != Tau_14)
% 1.77/2.10  (zenon_Vt != Tau_14)
% 1.77/2.10  (-. (p3 zenon_Vvj))
% 1.77/2.10  (-. (p3 zenon_Vp))
% 1.77/2.10  (-. (p1 zenon_Vmf))
% 1.77/2.10  (zenon_Vt != zenon_Vud)
% 1.77/2.10  (zenon_Vt != zenon_Vzc)
% 1.77/2.10  (-. (p4 zenon_Vcf))
% 1.77/2.10  (-. (p3 zenon_Vnj))
% 1.77/2.10  (zenon_Vr != Tau_5)
% 1.77/2.10  (zenon_Vm != Tau_5)
% 1.77/2.10  (zenon_Vo != Tau_5)
% 1.77/2.10  (zenon_Vt != Tau_5)
% 1.77/2.10  (-. (p1 Tau_10))
% 1.77/2.10  (-. (p1 zenon_Vke))
% 1.77/2.10  (-. (p4 zenon_Vdg))
% 1.77/2.10  (zenon_Vo != zenon_Vqg)
% 1.77/2.10  (-. (p1 zenon_Vpc))
% 1.77/2.10  (zenon_Vr != zenon_Vpi)
% 1.77/2.10  (zenon_Vm != zenon_Vqg)
% 1.77/2.10  (zenon_Vr != zenon_Vej)
% 1.77/2.10  (-. (p3 Tau_16))
% 1.77/2.10  (zenon_Vm != zenon_Vdh)
% 1.77/2.10  (-. (p1 zenon_Vvb))
% 1.77/2.10  (zenon_Vr != zenon_Vsc)
% 1.77/2.10  (zenon_Vo != zenon_Vri)
% 1.77/2.10  (-. (p2 zenon_Vve))
% 1.77/2.10  (zenon_Vt != zenon_Vve)
% 1.77/2.10  (zenon_Vr != zenon_Vgi)
% 1.77/2.10  (zenon_Vm != zenon_Vxg)
% 1.77/2.10  (zenon_Vm != zenon_Vje)
% 1.77/2.10  (zenon_Vt != zenon_Vsc)
% 1.77/2.10  (r1 zenon_Vkh zenon_Vph)
% 1.77/2.10  (-. (p1 Tau_7))
% 1.77/2.10  (-. (p2 zenon_Vkd))
% 1.77/2.10  (-. (p3 zenon_Vmd))
% 1.77/2.10  (r1 zenon_Vib zenon_Vjb)
% 1.77/2.10  (r1 zenon_Vec zenon_Vfc)
% 1.77/2.10  (r1 zenon_Vvj zenon_Vyj)
% 1.77/2.10  (-. (p1 zenon_Vce))
% 1.77/2.10  (zenon_Vt != zenon_Vbg)
% 1.77/2.10  (-. (p3 zenon_Vvi))
% 1.77/2.10  (r1 zenon_Vhj zenon_Vij)
% 1.77/2.10  (zenon_Vt != zenon_Vbf)
% 1.77/2.10  (zenon_Vr != zenon_Vak)
% 1.77/2.10  (-. (p1 Tau_5))
% 1.77/2.10  (zenon_Vr != zenon_Vef)
% 1.77/2.10  (-. (p1 zenon_Vxh))
% 1.77/2.10  (-. (p4 zenon_Vte))
% 1.77/2.10  (zenon_Vo != zenon_Vlf)
% 1.77/2.10  (zenon_Vt != zenon_Vic)
% 1.77/2.10  (-. (p2 zenon_Vke))
% 1.77/2.10  (-. (p3 zenon_Vci))
% 1.77/2.10  (r1 zenon_Vri zenon_Vvi)
% 1.77/2.10  (zenon_Vm != zenon_Via)
% 1.77/2.10  (-. (p4 zenon_Vve))
% 1.77/2.10  (-. (p4 zenon_Vbf))
% 1.77/2.10  (-. (p4 zenon_Vpg))
% 1.77/2.10  (-. (p3 zenon_Vpg))
% 1.77/2.10  (zenon_Vt != zenon_Vpc)
% 1.77/2.10  (zenon_Vm != zenon_Vue)
% 1.77/2.10  (-. (p2 zenon_Vjb))
% 1.77/2.10  (-. (p1 zenon_Vwd))
% 1.77/2.10  (-. (p2 zenon_Vqj))
% 1.77/2.10  (-. (p3 zenon_Vhg))
% 1.77/2.10  (zenon_Vr != zenon_Vjk)
% 1.77/2.10  (-. (p1 zenon_Vih))
% 1.77/2.10  (zenon_Vm != zenon_Vuh)
% 1.77/2.10  (zenon_Vt != zenon_Vuh)
% 1.77/2.10  (zenon_Vr != zenon_Vec)
% 1.77/2.10  (-. (p1 zenon_Vhg))
% 1.77/2.10  (zenon_Vo != zenon_Vig)
% 1.77/2.10  (zenon_Vt != zenon_Vrc)
% 1.77/2.10  (-. (p1 zenon_Vsd))
% 1.77/2.10  (r1 zenon_Vpi zenon_Vqi)
% 1.77/2.10  (zenon_Vt != zenon_Vcg)
% 1.77/2.10  (zenon_Vo != zenon_Vvg)
% 1.77/2.10  (zenon_Vo != zenon_Vqh)
% 1.77/2.10  (-. (p3 Tau_8))
% 1.77/2.10  (-. (p1 zenon_Vfk))
% 1.77/2.10  (r1 zenon_Vmi zenon_Vni)
% 1.77/2.10  (-. (p1 zenon_Vii))
% 1.77/2.10  (zenon_Vo != zenon_Vnd)
% 1.77/2.10  (r1 zenon_Vdi zenon_Vei)
% 1.77/2.10  (zenon_Vo != zenon_Vxb)
% 1.77/2.10  (zenon_Vo != zenon_Vii)
% 1.77/2.10  (r1 Tau_0 Tau_17)
% 1.77/2.10  (zenon_Vm != zenon_Vhj)
% 1.77/2.10  (zenon_Vr != zenon_Vch)
% 1.77/2.10  (zenon_Vt != zenon_Vne)
% 1.77/2.10  (-. (p2 Tau_21))
% 1.77/2.10  (-. (p4 zenon_Vii))
% 1.77/2.10  (zenon_Vr != zenon_Vuh)
% 1.77/2.10  (r1 zenon_Vrc zenon_Vsc)
% 1.77/2.10  (-. (p1 zenon_Vxg))
% 1.77/2.10  (-. (p1 Tau_9))
% 1.77/2.10  (zenon_Vm != zenon_Vte)
% 1.77/2.10  (-. (p3 zenon_Vqc))
% 1.77/2.10  (-. (p2 zenon_Vgc))
% 1.77/2.10  (-. (p2 zenon_Via))
% 1.77/2.10  (zenon_Vm != zenon_Vvg)
% 1.77/2.10  (zenon_Vo != zenon_Vrf)
% 1.77/2.10  (r1 zenon_Vce zenon_Vde)
% 1.77/2.10  (zenon_Vm != zenon_Vug)
% 1.77/2.10  (-. (p2 zenon_Vpc))
% 1.77/2.10  (-. (p2 zenon_Vgi))
% 1.77/2.10  (r1 zenon_Vyi zenon_Vzi)
% 1.77/2.10  (-. (p4 zenon_Vmf))
% 1.77/2.10  (zenon_Vm != zenon_Vkh)
% 1.77/2.10  (zenon_Vr != zenon_Vke)
% 1.77/2.10  (r1 Tau_0 Tau_9)
% 1.77/2.10  (zenon_Vm != zenon_Vxb)
% 1.77/2.10  (zenon_Vm != zenon_Vvh)
% 1.77/2.10  (zenon_Vo != zenon_Vrc)
% 1.77/2.10  (zenon_Vt != zenon_Vad)
% 1.77/2.10  (-. (p4 zenon_Vig))
% 1.77/2.10  (-. (p2 zenon_Vri))
% 1.77/2.10  (zenon_Vm != zenon_Vqc)
% 1.77/2.10  (zenon_Vt != zenon_Vmf)
% 1.77/2.10  (zenon_Vo != zenon_Vhj)
% 1.77/2.10  (zenon_Vt != zenon_Vvi)
% 1.77/2.10  (-. (p4 zenon_Vkb))
% 1.77/2.10  (zenon_Vm != zenon_Vfc)
% 1.77/2.10  (-. (p2 zenon_Vne))
% 1.77/2.10  (-. (p4 zenon_Vxb))
% 1.77/2.10  (-. (p2 zenon_Vvb))
% 1.77/2.10  (zenon_Vr != zenon_Vhj)
% 1.77/2.10  (zenon_Vm != zenon_Vka)
% 1.77/2.10  (-. (p1 zenon_Vvg))
% 1.77/2.10  (-. (p2 zenon_Vic))
% 1.77/2.10  (zenon_Vr != zenon_Vwd)
% 1.77/2.10  (-. (p2 zenon_Vee))
% 1.77/2.10  (zenon_Vo != zenon_Vmf)
% 1.77/2.10  (-. (p4 zenon_Vhj))
% 1.77/2.10  (-. (p2 zenon_Vce))
% 1.77/2.10  (-. (p3 zenon_Vdg))
% 1.77/2.10  (zenon_Vo != zenon_Vih)
% 1.77/2.10  (zenon_Vm != zenon_Vec)
% 1.77/2.10  (-. (p3 zenon_Vch))
% 1.77/2.10  (r1 Tau_0 Tau_20)
% 1.77/2.10  (zenon_Vt != Tau_15)
% 1.77/2.10  (r1 zenon_X25 zenon_Vm)
% 1.77/2.10  (-. (p2 zenon_Vuh))
% 1.77/2.10  (-. (p1 Tau_16))
% 1.77/2.10  (r1 zenon_Vxg zenon_Vch)
% 1.77/2.10  (zenon_Vm != zenon_Vic)
% 1.77/2.10  (-. (p1 zenon_Vue))
% 1.77/2.10  (-. (p2 zenon_Vfc))
% 1.77/2.10  (-. (p1 zenon_Vqg))
% 1.77/2.10  (zenon_Vm != zenon_Vgi)
% 1.77/2.10  (-. (p2 zenon_Vig))
% 1.77/2.10  (r1 Tau_0 Tau_2)
% 1.77/2.10  (zenon_Vr != zenon_Vii)
% 1.77/2.10  (zenon_Vr != Tau_22)
% 1.77/2.10  (zenon_Vm != Tau_22)
% 1.77/2.10  (zenon_Vm != zenon_Vdc)
% 1.77/2.10  (zenon_Vt != Tau_22)
% 1.77/2.10  (-. (p3 zenon_Vvh))
% 1.77/2.10  (r1 zenon_Vje zenon_Vke)
% 1.77/2.10  (r1 zenon_Vr zenon_Vs)
% 1.77/2.10  (zenon_Vr != zenon_Vcg)
% 1.77/2.10  (-. (p1 zenon_Vic))
% 1.77/2.10  (r1 zenon_Vwb zenon_Vxb)
% 1.77/2.10  (r1 zenon_Vkd zenon_Vld)
% 1.77/2.10  (-. (p2 zenon_Vlb))
% 1.77/2.10  (-. (p3 zenon_Vfc))
% 1.77/2.10  (r1 Tau_0 Tau_6)
% 1.77/2.10  (-. (p3 zenon_Vwb))
% 1.77/2.10  (r1 zenon_Vld zenon_Vmd)
% 1.77/2.10  (-. (p3 zenon_Vub))
% 1.77/2.10  (zenon_Vr != zenon_Vic)
% 1.77/2.10  (-. (p2 zenon_Vdc))
% 1.77/2.10  (-. (p2 zenon_Vpi))
% 1.77/2.10  (-. (p3 zenon_Vec))
% 1.77/2.10  (zenon_Vt != zenon_Vnd)
% 1.77/2.10  (-. (p2 Tau_10))
% 1.77/2.10  (zenon_Vr != zenon_Vnb)
% 1.77/2.10  (zenon_Vr != zenon_Vgc)
% 1.77/2.10  (-. (p1 zenon_Vkh))
% 1.77/2.10  (-. (p2 zenon_Vvj))
% 1.77/2.10  (zenon_Vr != zenon_Vci)
% 1.77/2.10  (-. (p4 zenon_Vvg))
% 1.77/2.10  (zenon_Vm != zenon_Vle)
% 1.77/2.10  (zenon_Vr != zenon_Vee)
% 1.77/2.10  (zenon_Vr != zenon_Vhg)
% 1.77/2.10  (zenon_Vr != zenon_Vlf)
% 1.77/2.10  (-. (p2 zenon_Vsf))
% 1.77/2.10  (-. (p3 zenon_Vrc))
% 1.77/2.10  (zenon_Vm != zenon_Vwb)
% 1.77/2.10  (-. (p2 Tau_18))
% 1.77/2.10  (-. (p2 zenon_Vsc))
% 1.77/2.10  (r1 Tau_0 Tau_7)
% 1.77/2.10  (zenon_Vm != zenon_Vrf)
% 1.77/2.10  (-. (p2 zenon_Vhh))
% 1.77/2.10  (zenon_Vm != zenon_Vde)
% 1.77/2.10  (zenon_Vr != zenon_Vtd)
% 1.77/2.10  (zenon_Vo != zenon_Vvj)
% 1.77/2.10  (zenon_Vt != zenon_Vxh)
% 1.77/2.10  (-. (p2 zenon_Vtf))
% 1.77/2.10  (-. (p2 zenon_Vdh))
% 1.77/2.10  (p2 zenon_Vr)
% 1.77/2.10  (-. (p3 zenon_Vde))
% 1.77/2.10  (zenon_Vt != zenon_Vec)
% 1.77/2.10  (-. (p2 zenon_Vtd))
% 1.77/2.10  (zenon_Vm != zenon_Vbd)
% 1.77/2.10  (-. (p3 zenon_Vue))
% 1.77/2.10  (r1 Tau_0 Tau_14)
% 1.77/2.10  (zenon_Vr != zenon_Vqh)
% 1.77/2.10  (zenon_Vo != zenon_Vde)
% 1.77/2.10  (r1 zenon_Vvf zenon_Vbg)
% 1.77/2.10  (zenon_Vr != zenon_Vqc)
% 1.77/2.10  (zenon_Vm != zenon_Vzc)
% 1.77/2.10  (-. (p2 zenon_Vnd))
% 1.77/2.10  (r1 Tau_12 zenon_Vhg)
% 1.77/2.10  (-. (p2 zenon_Vxb))
% 1.77/2.10  (-. (p3 zenon_Vjb))
% 1.77/2.10  (zenon_Vr != zenon_Vyc)
% 1.77/2.10  (r1 zenon_Vve zenon_Vwe)
% 1.77/2.10  (-. (p2 zenon_Vzc))
% 1.77/2.10  (zenon_Vr != zenon_Vpg)
% 1.77/2.10  (-. (p3 zenon_Vri))
% 1.77/2.10  (zenon_Vt != zenon_Vch)
% 1.77/2.10  (zenon_Vt != zenon_Vkf)
% 1.77/2.10  (zenon_Vo != zenon_Vsf)
% 1.77/2.10  (r1 zenon_Vfc zenon_Vgc)
% 1.77/2.10  (zenon_Vr != zenon_Vhh)
% 1.77/2.10  (zenon_Vt != zenon_Vgi)
% 1.77/2.10  (zenon_Vo != zenon_Vug)
% 1.77/2.10  (-. (p2 Tau_14))
% 1.77/2.10  (zenon_Vr != zenon_Vih)
% 1.77/2.10  (zenon_Vt != zenon_Vue)
% 1.77/2.10  (-. (p2 zenon_Vaj))
% 1.77/2.10  (-. (p1 zenon_Vje))
% 1.77/2.10  (-. (p2 zenon_Vpg))
% 1.77/2.10  (-. (p2 zenon_Vs))
% 1.77/2.10  (r1 zenon_Vad zenon_Vbd)
% 1.77/2.10  (zenon_Vr != zenon_Vtf)
% 1.77/2.10  (zenon_Vr != zenon_Vkd)
% 1.77/2.10  (zenon_Vr != zenon_Vte)
% 1.77/2.10  (zenon_Vt != zenon_Vxg)
% 1.77/2.10  (-. (p4 zenon_Vib))
% 1.77/2.10  (-. (p2 Tau_6))
% 1.77/2.10  (r1 zenon_Vub zenon_Vvb)
% 1.77/2.10  (r1 zenon_Vwd zenon_Vce)
% 1.77/2.10  (zenon_Vt != zenon_Vee)
% 1.77/2.10  (-. (p1 zenon_Vjb))
% 1.77/2.10  (-. (p1 Tau_6))
% 1.77/2.10  (-. (p2 Tau_9))
% 1.77/2.10  (zenon_Vt != zenon_Vug)
% 1.77/2.10  (-. (p2 zenon_Vjk))
% 1.77/2.10  (zenon_Vo != zenon_Vdg)
% 1.77/2.10  (zenon_Vr != zenon_Vad)
% 1.77/2.10  (-. (p1 zenon_Vri))
% 1.77/2.10  (-. (p4 zenon_Vld))
% 1.77/2.10  (r1 zenon_Vcf zenon_Vdf)
% 1.77/2.10  (-. (p2 zenon_Vak))
% 1.77/2.10  (-. (p3 zenon_Vkf))
% 1.77/2.10  (r1 zenon_Vuh zenon_Vvh)
% 1.77/2.10  (-. (p3 zenon_Vyi))
% 1.77/2.10  (zenon_Vr != zenon_Vpc)
% 1.77/2.10  (-. (p4 zenon_Vaf))
% 1.77/2.10  (zenon_Vm != zenon_Vkd)
% 1.77/2.10  (zenon_Vm != zenon_Vcg)
% 1.77/2.10  (zenon_Vm != zenon_Vvb)
% 1.77/2.10  (-. (p4 zenon_Vqj))
% 1.77/2.10  (zenon_Vr != Tau_8)
% 1.77/2.10  (zenon_Vm != Tau_8)
% 1.77/2.10  (zenon_Vo != Tau_8)
% 1.77/2.10  (zenon_Vt != Tau_8)
% 1.77/2.10  (-. (p1 zenon_Vch))
% 1.77/2.10  (-. (p1 zenon_Vfc))
% 1.77/2.10  (-. (p1 Tau_17))
% 1.77/2.10  (zenon_Vm != zenon_Vbg)
% 1.77/2.10  (r1 Tau_10 zenon_Vaf)
% 1.77/2.10  (-. (p3 zenon_Vtd))
% 1.77/2.10  (-. (p1 zenon_Vsf))
% 1.77/2.10  (-. (p3 zenon_Vqj))
% 1.77/2.10  (r1 Tau_0 Tau_3)
% 1.77/2.10  (-. (p4 zenon_Vje))
% 1.77/2.10  (zenon_Vt != Tau_19)
% 1.77/2.10  (-. (p1 zenon_Vlf))
% 1.77/2.10  (zenon_Vr != zenon_Vxb)
% 1.77/2.10  (zenon_Vt != zenon_Vdh)
% 1.77/2.10  (-. (p4 zenon_Vlb))
% 1.77/2.10  (-. (p4 zenon_Vej))
% 1.77/2.10  (-. (p3 zenon_Vkg))
% 1.77/2.10  (-. (p3 zenon_Vvb))
% 1.77/2.10  (zenon_Vo != zenon_Vpg)
% 1.77/2.10  (-. (p1 zenon_Vig))
% 1.77/2.10  (-. (p3 zenon_Vnb))
% 1.77/2.10  (zenon_Vr != zenon_Vri)
% 1.77/2.10  (zenon_Vm != zenon_Vpg)
% 1.77/2.10  (r1 Tau_22 zenon_Vzj)
% 1.77/2.10  (-. (p1 zenon_Vub))
% 1.77/2.10  (zenon_Vm != zenon_Vib)
% 1.77/2.10  (-. (p3 zenon_Vsd))
% 1.77/2.10  (-. (p3 zenon_Vyc))
% 1.77/2.10  (-. (p1 zenon_Vwb))
% 1.77/2.10  (-. (p3 Tau_5))
% 1.77/2.10  (-. (p1 zenon_Vkb))
% 1.77/2.10  (-. (p2 Tau_22))
% 1.77/2.10  (-. (p1 zenon_Vjj))
% 1.77/2.10  (r1 zenon_Vci zenon_Vdi)
% 1.77/2.10  (-. (p1 Tau_18))
% 1.77/2.10  (-. (p3 zenon_Vii))
% 1.77/2.10  (-. (p3 zenon_Vgc))
% 1.77/2.10  (-. (p4 zenon_Vdh))
% 1.77/2.10  (zenon_Vo != zenon_Vkd)
% 1.77/2.10  (r1 Tau_0 Tau_10)
% 1.77/2.10  (-. (p3 zenon_Vhh))
% 1.77/2.10  (r1 zenon_Vjj zenon_Vnj)
% 1.77/2.10  (-. (p1 zenon_Vaj))
% 1.77/2.10  (-. (p3 Tau_17))
% 1.77/2.10  (r1 zenon_Vcg zenon_Vdg)
% 1.77/2.10  (zenon_Vt != zenon_Vub)
% 1.77/2.10  (zenon_Vt != zenon_Vnj)
% 1.77/2.10  (zenon_Vo != zenon_Vld)
% 1.77/2.10  (-. (p1 zenon_Vkd))
% 1.77/2.10  (-. (p2 zenon_Vrc))
% 1.77/2.10  (-. (p3 zenon_Vsc))
% 1.77/2.10  (zenon_Vm != zenon_Vyc)
% 1.77/2.10  (zenon_Vo != zenon_Vwd)
% 1.77/2.10  (r1 zenon_Vne zenon_Vte)
% 1.77/2.10  (zenon_Vo != zenon_Vpi)
% 1.77/2.10  (zenon_Vo != zenon_Vlb)
% 1.77/2.10  (r1 zenon_Vm zenon_Vn)
% 1.77/2.10  (r1 zenon_Vsd zenon_Vtd)
% 1.77/2.10  (-. (p2 zenon_Vqh))
% 1.77/2.10  (-. (p2 zenon_Vwd))
% 1.77/2.10  (zenon_Vo != zenon_Vib)
% 1.77/2.10  (r1 zenon_Vvg zenon_Vwg)
% 1.77/2.10  (zenon_Vo != zenon_Vdi)
% 1.77/2.10  (zenon_Vo != zenon_Vkg)
% 1.77/2.10  (zenon_Vo != zenon_Vej)
% 1.77/2.10  (-. (p1 Tau_15))
% 1.77/2.10  (p3 zenon_Vo)
% 1.77/2.10  (zenon_Vo != zenon_Vbg)
% 1.77/2.10  (-. (p4 zenon_Vnj))
% 1.77/2.10  (zenon_Vt != zenon_Vkd)
% 1.77/2.10  (-. (p4 zenon_Vbg))
% 1.77/2.10  (-. (p2 zenon_Vwb))
% 1.77/2.10  (-. (p1 zenon_Vgc))
% 1.77/2.10  (zenon_Vm != zenon_Vwd)
% 1.77/2.10  (zenon_Vt != zenon_Vyi)
% 1.77/2.10  (r1 Tau_0 Tau_23)
% 1.77/2.10  (zenon_Vt != zenon_Vmi)
% 1.77/2.10  (r1 zenon_Vlb zenon_Vmb)
% 1.77/2.10  (zenon_Vr != zenon_Vfc)
% 1.77/2.10  (zenon_Vr != Tau_12)
% 1.77/2.10  (zenon_Vm != Tau_12)
% 1.77/2.10  (zenon_Vo != Tau_12)
% 1.77/2.10  (zenon_Vt != Tau_12)
% 1.77/2.10  (zenon_Vm != zenon_Vii)
% 1.77/2.10  (zenon_Vo != zenon_Vnj)
% 1.77/2.10  (-. (p2 zenon_Vph))
% 1.77/2.10  (zenon_Vm != zenon_Vbf)
% 1.77/2.10  (r1 zenon_Vaj zenon_Vej)
% 1.77/2.10  (zenon_Vr != zenon_Vvh)
% 1.77/2.10  (zenon_Vo != zenon_Vvb)
% 1.77/2.10  (zenon_Vt != zenon_Vje)
% 1.77/2.10  (-. (p4 zenon_Vsd))
% 1.77/2.10  (-. (p1 zenon_Vqj))
% 1.77/2.10  (zenon_Vt != Tau_2)
% 1.77/2.10  (zenon_Vr != zenon_Vsf)
% 1.77/2.10  (zenon_Vm != zenon_Vcb)
% 1.77/2.10  (r1 zenon_Vtf zenon_Vuf)
% 1.77/2.10  (-. (p1 zenon_Vbg))
% 1.77/2.10  (-. (p2 zenon_Vhj))
% 1.77/2.10  (-. (p2 zenon_Vxg))
% 1.77/2.10  (zenon_Vt != zenon_Vef)
% 1.77/2.10  (-. (p3 zenon_Vtf))
% 1.77/2.10  (-. (p3 zenon_Vbf))
% 1.77/2.10  (-. (p1 Tau_20))
% 1.77/2.10  (zenon_Vr != Tau_18)
% 1.77/2.10  (zenon_Vm != Tau_18)
% 1.77/2.10  (zenon_Vt != Tau_18)
% 1.77/2.10  (zenon_Vt != zenon_Vpg)
% 1.77/2.10  (-. (p2 zenon_Vhg))
% 1.77/2.10  (zenon_Vm != zenon_Vej)
% 1.77/2.10  (-. (p3 zenon_Vvg))
% 1.77/2.10  (-. (p1 zenon_Vuh))
% 1.77/2.10  (-. (p1 zenon_Vnb))
% 1.77/2.10  (-. (p1 zenon_Vde))
% 1.77/2.10  (zenon_Vr != zenon_Vbf)
% 1.77/2.10  (zenon_Vr != zenon_Vkf)
% 1.77/2.10  (zenon_Vr != zenon_Vkg)
% 1.77/2.10  (-. (p3 zenon_Vqg))
% 1.77/2.10  (zenon_Vr != zenon_Vwb)
% 1.77/2.10  (-. (p2 zenon_Vsd))
% 1.77/2.10  (-. (p2 zenon_Vci))
% 1.77/2.10  (-. (p2 Tau_16))
% 1.77/2.10  (-. (p1 zenon_Vef))
% 1.77/2.10  (zenon_Vm != zenon_Vig)
% 1.77/2.10  (zenon_Vm != zenon_Vne)
% 1.77/2.10  (zenon_Vo != zenon_Vjb)
% 1.77/2.10  (zenon_Vo != Tau_1)
% 1.77/2.10  (zenon_Vt != zenon_Vdg)
% 1.77/2.10  (-. (p2 zenon_Vmi))
% 1.77/2.10  (zenon_Vt != zenon_Vvh)
% 1.77/2.10  (r1 zenon_Vue zenon_Vve)
% 1.77/2.10  (zenon_Vt != zenon_Vsd)
% 1.77/2.10  (zenon_Vm != zenon_Vmd)
% 1.77/2.10  (-. (p4 zenon_Vmi))
% 1.77/2.10  (-. (p1 zenon_Vrc))
% 1.77/2.10  (-. (p4 zenon_Vud))
% 1.77/2.10  (zenon_Vo != zenon_Vyc)
% 1.77/2.10  (r1 Tau_17 zenon_Vpi)
% 1.77/2.10  (-. (p4 zenon_Vdi))
% 1.77/2.10  (zenon_Vt != zenon_Vib)
% 1.77/2.10  (zenon_Vr != zenon_Vcb)
% 1.77/2.10  (-. (p2 zenon_Vnb))
% 1.77/2.10  (zenon_Vr != zenon_Vdh)
% 1.77/2.10  (r1 Tau_0 Tau_15)
% 1.77/2.10  (r1 zenon_Vpc zenon_Vqc)
% 1.77/2.10  (zenon_Vr != Tau_3)
% 1.77/2.10  (zenon_Vm != Tau_3)
% 1.77/2.10  (zenon_Vt != zenon_Vqj)
% 1.77/2.10  (-. (p2 zenon_Vqc))
% 1.77/2.10  (zenon_Vr != zenon_Vne)
% 1.77/2.10  (zenon_Vt != zenon_Vvb)
% 1.77/2.10  (r1 zenon_Vdd zenon_Vkd)
% 1.77/2.10  (-. (p4 zenon_Vuh))
% 1.77/2.11  (zenon_Vo != zenon_Vke)
% 1.77/2.11  (zenon_Vo != zenon_Vte)
% 1.77/2.11  (zenon_Vt != zenon_Vdi)
% 1.77/2.11  (-. (p4 zenon_Vmd))
% 1.77/2.11  (zenon_Vr != Tau_4)
% 1.77/2.11  (zenon_Vm != Tau_4)
% 1.77/2.11  (-. (p1 zenon_Vpg))
% 1.77/2.11  (r1 zenon_Vhg zenon_Vig)
% 1.77/2.11  (zenon_Vm != zenon_Vaj)
% 1.77/2.11  (zenon_Vo != zenon_Vnb)
% 1.77/2.11  (-. (p4 zenon_Vrc))
% 1.77/2.11  (zenon_Vm != zenon_Vs)
% 1.77/2.11  (-. (p1 zenon_Vci))
% 1.77/2.11  (zenon_Vt != zenon_Vrf)
% 1.77/2.11  (-. (p4 zenon_Vee))
% 1.77/2.11  (r1 zenon_Vbd zenon_Vcd)
% 1.77/2.11  (-. (p2 Tau_4))
% 1.77/2.11  (-. (p2 zenon_Vdg))
% 1.77/2.11  (-. (p2 zenon_Vlf))
% 1.77/2.11  (-. (p4 zenon_Vkg))
% 1.77/2.11  (-. (p4 zenon_Vwd))
% 1.77/2.11  (-. (p1 zenon_Vbd))
% 1.77/2.11  (-. (p4 zenon_Vub))
% 1.77/2.11  (zenon_Vt != zenon_Vvg)
% 1.77/2.11  (-. (p1 zenon_Vqc))
% 1.77/2.11  (zenon_Vt != zenon_Vtd)
% 1.77/2.11  *)
% 1.77/2.11  (* NO-PROOF *)
% 1.77/2.11  % SZS status GaveUp
% 1.77/2.11  Number of rewrites on terms: 0
% 1.77/2.11  Number of rewrites on props: 0
% 1.77/2.11  nodes searched: 861
% 1.77/2.11  max branch formulas: 1399
% 1.77/2.11  proof nodes created: 0
% 1.77/2.11  formulas created: 8308
% 1.77/2.11  
%------------------------------------------------------------------------------