↑ Up

ZenonModulo---0.5.0.UNK-Non.f

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

% Computer : n028.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:11 PM UTC 2026

% Result   : Unknown 13.94s 14.28s
% Output   : None 
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : LCL636+1.010 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03  % Command  : run_zenon_modulo %d %s
% 0.07/0.34  % Computer : n028.cluster.edu
% 0.07/0.34  % Model    : x86_64 x86_64
% 0.07/0.34  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.34  % Memory   : 8046.5625MB
% 0.07/0.34  % OS       : Linux 6.8.0-71-generic
% 0.07/0.34  % CPULimit : 300
% 0.07/0.34  % WCLimit  : 300
% 0.07/0.35  % DateTime : Sat Sep  5 14:07:59 UTC 2026
% 0.07/0.35  % CPUTime  : 
% 13.94/14.27  Zenon error: exhausted search space without finding a proof
% 13.94/14.27  (* Current branch:
% 13.94/14.27  (zenon_Vtq != zenon_Vda)
% 13.94/14.27  (p3 zenon_Vlq)
% 13.94/14.27  (p1 zenon_Voq)
% 13.94/14.27  (p6 zenon_Viq)
% 13.94/14.27  (-. (p106 Tau_1))
% 13.94/14.27  (p2 zenon_Veq)
% 13.94/14.27  (zenon_Vdq != zenon_Vtq)
% 13.94/14.27  (r1 Tau_2 zenon_Vsq)
% 13.94/14.27  (r1 Tau_2 zenon_Vtq)
% 13.94/14.27  (p4 zenon_Veq)
% 13.94/14.27  (zenon_Vtq != zenon_Vpr)
% 13.94/14.27  (zenon_Vdq != zenon_Var)
% 13.94/14.27  (-. (p107 zenon_Vlo))
% 13.94/14.27  (zenon_Vrq != zenon_Vor)
% 13.94/14.27  (-. (p109 zenon_Vyq))
% 13.94/14.27  (zenon_Vdq != zenon_Vrr)
% 13.94/14.27  (zenon_Vfq != zenon_Vkr)
% 13.94/14.27  (-. (p104 Tau_1))
% 13.94/14.27  (zenon_Vcq != zenon_Vjr)
% 13.94/14.27  (-. (p107 zenon_Vnq))
% 13.94/14.27  (-. (p106 zenon_Vyd))
% 13.94/14.27  (p2 zenon_Voq)
% 13.94/14.27  (zenon_Vhq != zenon_Vjq)
% 13.94/14.27  (-. (p104 zenon_Vda))
% 13.94/14.27  (zenon_Viq != zenon_Vhr)
% 13.94/14.27  (p3 zenon_Viq)
% 13.94/14.27  (zenon_Vhq != zenon_Vtq)
% 13.94/14.27  (r1 zenon_Vvq zenon_Vsq)
% 13.94/14.27  (p5 zenon_Vmq)
% 13.94/14.27  (-. (p109 zenon_Vlo))
% 13.94/14.27  (zenon_Veq != zenon_Vyq)
% 13.94/14.27  (-. (p4 zenon_Vqq))
% 13.94/14.27  (zenon_Vgq != zenon_X3)
% 13.94/14.27  (zenon_Viq != zenon_Vfr)
% 13.94/14.27  (p101 zenon_Vgq)
% 13.94/14.27  (p3 zenon_Vtq)
% 13.94/14.27  (r1 zenon_Vuq zenon_Vtq)
% 13.94/14.27  (p7 zenon_Viq)
% 13.94/14.27  (zenon_Vdq != zenon_Vhr)
% 13.94/14.27  (-. (p110 zenon_X14))
% 13.94/14.27  (p5 zenon_Vkq)
% 13.94/14.27  (p4 zenon_Vdq)
% 13.94/14.27  (zenon_Vmq != zenon_Vrr)
% 13.94/14.27  (-. (p108 zenon_Viq))
% 13.94/14.27  (-. (p108 zenon_Vlo))
% 13.94/14.27  (p101 zenon_Vnq)
% 13.94/14.27  (zenon_Veq != zenon_Vpq)
% 13.94/14.27  (p3 zenon_Vhq)
% 13.94/14.27  (zenon_Vpq != zenon_Vum)
% 13.94/14.27  (zenon_Vmq != zenon_Vtq)
% 13.94/14.27  (p9 zenon_Vfq)
% 13.94/14.27  (-. (p106 zenon_X14))
% 13.94/14.27  (zenon_Vfq != zenon_Vhr)
% 13.94/14.27  (zenon_Vcq != zenon_Vxq)
% 13.94/14.27  (zenon_Vpq != zenon_X3)
% 13.94/14.27  (zenon_Vkq != zenon_Vpr)
% 13.94/14.27  (-. (p104 zenon_Vjj))
% 13.94/14.27  (zenon_Vjq != zenon_Voq)
% 13.94/14.27  (zenon_Veq != zenon_Vor)
% 13.94/14.27  (-. (p100 zenon_Vcl))
% 13.94/14.27  (p1 Tau_1)
% 13.94/14.27  (-. (p102 zenon_Vmr))
% 13.94/14.27  (zenon_Vjq != zenon_Vjr)
% 13.94/14.27  (-. (p109 zenon_Vbc))
% 13.94/14.27  (zenon_Vtq != zenon_Vuf)
% 13.94/14.27  (p3 zenon_Vdq)
% 13.94/14.27  (zenon_Vnq != zenon_Vvq)
% 13.94/14.27  (zenon_Vhq != zenon_Var)
% 13.94/14.27  (zenon_Veq != zenon_Vrq)
% 13.94/14.27  (-. (p107 zenon_Vjj))
% 13.94/14.27  (zenon_Vhq != zenon_X14)
% 13.94/14.27  (-. (p104 zenon_Vuq))
% 13.94/14.27  (p102 zenon_Vhq)
% 13.94/14.27  (p2 Tau_2)
% 13.94/14.27  (zenon_Vkq != zenon_Vjr)
% 13.94/14.27  (zenon_Vvq != zenon_X3)
% 13.94/14.27  (zenon_Vcq != zenon_Vgq)
% 13.94/14.27  (zenon_Vcq != zenon_Vwq)
% 13.94/14.27  (zenon_Vqq != zenon_Vtq)
% 13.94/14.27  (zenon_Vlq != zenon_Vgr)
% 13.94/14.27  (p101 zenon_Vuq)
% 13.94/14.27  (p106 zenon_Vkq)
% 13.94/14.27  (-. (p111 zenon_Vum))
% 13.94/14.27  (p3 zenon_Vrq)
% 13.94/14.27  (-. (p107 zenon_Vcr))
% 13.94/14.27  (Tau_2 != zenon_Vda)
% 13.94/14.27  (Tau_2 != zenon_Vbc)
% 13.94/14.27  (Tau_2 != zenon_Vyd)
% 13.94/14.27  (Tau_2 != zenon_Vuf)
% 13.94/14.27  (Tau_2 != zenon_Vph)
% 13.94/14.27  (Tau_2 != zenon_Vjj)
% 13.94/14.27  (Tau_2 != zenon_Vcl)
% 13.94/14.27  (Tau_2 != zenon_Vum)
% 13.94/14.27  (Tau_2 != zenon_Vlo)
% 13.94/14.27  (Tau_2 != zenon_Vuq)
% 13.94/14.27  (Tau_2 != zenon_Vor)
% 13.94/14.27  (Tau_2 != zenon_Vrr)
% 13.94/14.27  (Tau_2 != zenon_Vpr)
% 13.94/14.27  (r1 zenon_Veq zenon_Vcq)
% 13.94/14.27  (-. (p103 zenon_Vbc))
% 13.94/14.27  (zenon_Vnq != zenon_Vsq)
% 13.94/14.27  (-. (p104 zenon_X14))
% 13.94/14.27  (-. (p105 Tau_1))
% 13.94/14.27  (p103 zenon_Vnq)
% 13.94/14.27  (zenon_Vhq != zenon_Vlr)
% 13.94/14.27  (zenon_Veq != zenon_Vjr)
% 13.94/14.27  (p100 zenon_Vnq)
% 13.94/14.27  (zenon_Vkq != zenon_Vqq)
% 13.94/14.27  (zenon_Vuq != zenon_Vyd)
% 13.94/14.27  (r1 zenon_Vlq zenon_Viq)
% 13.94/14.27  (-. (p111 zenon_Vrq))
% 13.94/14.27  (zenon_Vsq != zenon_Vyd)
% 13.94/14.27  (zenon_Vjq != zenon_Vqq)
% 13.94/14.27  (zenon_Vcq != zenon_Vyq)
% 13.94/14.27  (-. (p108 zenon_Vda))
% 13.94/14.27  (zenon_Vjq != zenon_X14)
% 13.94/14.27  (zenon_Vrq != zenon_Vpr)
% 13.94/14.27  (-. (p109 zenon_Vsq))
% 13.94/14.27  (zenon_Voq != zenon_X14)
% 13.94/14.27  (p109 zenon_Vcq)
% 13.94/14.27  (zenon_Vfq != zenon_Vkq)
% 13.94/14.27  (zenon_Vlq != zenon_Vtq)
% 13.94/14.27  (zenon_Vlq != zenon_Vda)
% 13.94/14.27  (-. (p110 zenon_Vmq))
% 13.94/14.27  (zenon_Vuq != zenon_Vuf)
% 13.94/14.27  (-. (p101 zenon_Vyd))
% 13.94/14.27  (zenon_Viq != zenon_Vuf)
% 13.94/14.27  (-. (p102 zenon_Vuf))
% 13.94/14.27  (zenon_Vjq != zenon_Vcr)
% 13.94/14.27  (p105 zenon_Vdq)
% 13.94/14.27  (zenon_Veq != zenon_Vvq)
% 13.94/14.27  (zenon_Vvq != zenon_Vyd)
% 13.94/14.27  (zenon_Vkq != zenon_Vlo)
% 13.94/14.27  (p5 zenon_Vgq)
% 13.94/14.27  (zenon_Vlq != zenon_Vrq)
% 13.94/14.27  (zenon_Vcq != zenon_Vuf)
% 13.94/14.27  (-. (p106 zenon_Vvq))
% 13.94/14.27  (p105 zenon_Vjq)
% 13.94/14.27  (-. (p111 zenon_Vhq))
% 13.94/14.27  (zenon_Vrq != zenon_Vnr)
% 13.94/14.27  (-. (p104 zenon_Vvq))
% 13.94/14.27  (-. (p8 zenon_Viq))
% 13.94/14.27  (zenon_Vnq != zenon_Vir)
% 13.94/14.27  (zenon_Vcq != zenon_Vlr)
% 13.94/14.27  (-. (p102 zenon_Vyd))
% 13.94/14.27  (zenon_Vuq != Tau_0)
% 13.94/14.27  (zenon_Vvq != Tau_0)
% 13.94/14.27  (zenon_Vsq != Tau_0)
% 13.94/14.27  (zenon_Vtq != Tau_0)
% 13.94/14.27  (zenon_Vqq != Tau_0)
% 13.94/14.27  (zenon_Vrq != Tau_0)
% 13.94/14.27  (zenon_Voq != zenon_Vsq)
% 13.94/14.27  (zenon_Voq != Tau_0)
% 13.94/14.27  (zenon_Vpq != Tau_0)
% 13.94/14.27  (zenon_Vmq != Tau_0)
% 13.94/14.27  (zenon_Vnq != Tau_0)
% 13.94/14.27  (zenon_Vkq != Tau_0)
% 13.94/14.27  (zenon_Vlq != Tau_0)
% 13.94/14.27  (zenon_Viq != Tau_0)
% 13.94/14.27  (zenon_Vjq != Tau_0)
% 13.94/14.27  (zenon_Vgq != Tau_0)
% 13.94/14.27  (zenon_Vhq != Tau_0)
% 13.94/14.27  (zenon_Veq != Tau_0)
% 13.94/14.27  (zenon_Vfq != Tau_0)
% 13.94/14.27  (zenon_Vcq != Tau_0)
% 13.94/14.27  (zenon_Vdq != Tau_0)
% 13.94/14.27  (zenon_Vsq != zenon_Vnr)
% 13.94/14.27  (p4 zenon_Vkq)
% 13.94/14.27  (zenon_Vrq != zenon_Vrr)
% 13.94/14.27  (zenon_Voq != zenon_Vvq)
% 13.94/14.27  (zenon_Vjq != zenon_Vsq)
% 13.94/14.27  (zenon_Vdq != zenon_Vmr)
% 13.94/14.27  (-. (p110 zenon_Vjq))
% 13.94/14.27  (zenon_Vfq != zenon_Vmr)
% 13.94/14.27  (-. (p107 zenon_Vpq))
% 13.94/14.27  (zenon_Vfq != zenon_Vbr)
% 13.94/14.27  (r1 zenon_Vqq zenon_Vpq)
% 13.94/14.27  (-. (p105 zenon_Vuf))
% 13.94/14.27  (zenon_Vnq != zenon_Vyd)
% 13.94/14.27  (zenon_Vuq != zenon_Vph)
% 13.94/14.27  (zenon_Voq != zenon_Vrq)
% 13.94/14.27  (-. (p111 zenon_Vmq))
% 13.94/14.27  (-. (p107 zenon_Vlq))
% 13.94/14.27  (zenon_Vfq != zenon_Var)
% 13.94/14.27  (p1 zenon_Vhq)
% 13.94/14.27  (zenon_Vgq != zenon_Vnq)
% 13.94/14.27  (p107 zenon_Vgq)
% 13.94/14.27  (zenon_Vlq != zenon_Vjr)
% 13.94/14.27  (-. (p111 zenon_Vjj))
% 13.94/14.27  (zenon_Vlq != zenon_Vlo)
% 13.94/14.27  (zenon_Vcq != zenon_Vrq)
% 13.94/14.27  (zenon_Vrq != zenon_Vbc)
% 13.94/14.27  (zenon_Vgq != zenon_Vlo)
% 13.94/14.27  (zenon_Vpq != zenon_Vor)
% 13.94/14.27  (zenon_Vkq != zenon_Vrr)
% 13.94/14.27  (-. (p111 zenon_Vtq))
% 13.94/14.27  (zenon_Vmq != zenon_X14)
% 13.94/14.27  (-. (p107 zenon_Vrq))
% 13.94/14.27  (zenon_Viq != zenon_Vgr)
% 13.94/14.27  (zenon_Vnq != zenon_Vrr)
% 13.94/14.27  (zenon_Vmq != zenon_Vph)
% 13.94/14.27  (zenon_Vuq != zenon_Vbc)
% 13.94/14.27  (-. (p5 zenon_Voq))
% 13.94/14.27  (p100 Tau_1)
% 13.94/14.27  (zenon_Vhq != zenon_Vcl)
% 13.94/14.27  (zenon_Vfq != zenon_Vcr)
% 13.94/14.27  (p100 zenon_Vhq)
% 13.94/14.27  (zenon_Vvq != zenon_Vuq)
% 13.94/14.27  (-. (p105 zenon_Vcl))
% 13.94/14.27  (p102 zenon_Vlq)
% 13.94/14.27  (zenon_Vfq != zenon_Veq)
% 13.94/14.27  (-. (p108 zenon_Vjq))
% 13.94/14.27  (p105 zenon_Vkq)
% 13.94/14.27  (p107 zenon_Vfq)
% 13.94/14.27  (-. (p108 zenon_Vvq))
% 13.94/14.27  (p101 zenon_Vsq)
% 13.94/14.27  (zenon_Vpq != zenon_Vrr)
% 13.94/14.27  (r1 zenon_Vkq zenon_Vjq)
% 13.94/14.27  (-. (p111 zenon_Vsq))
% 13.94/14.27  (p4 zenon_Vnq)
% 13.94/14.27  (zenon_Vjq != zenon_Vlq)
% 13.94/14.27  (p100 zenon_Vuq)
% 13.94/14.27  (-. (p111 zenon_Vbc))
% 13.94/14.27  (p6 zenon_Vlq)
% 13.94/14.27  (zenon_Vhq != zenon_Vvq)
% 13.94/14.27  (-. (p2 zenon_Vuq))
% 13.94/14.27  (-. (p107 zenon_Vmq))
% 13.94/14.27  (zenon_Vvq != zenon_Vda)
% 13.94/14.27  (p5 zenon_Vfq)
% 13.94/14.27  (-. (p106 zenon_Ver))
% 13.94/14.27  (Tau_1 != zenon_X3)
% 13.94/14.27  (p105 zenon_Vhq)
% 13.94/14.27  (zenon_Vhq != zenon_Vpq)
% 13.94/14.27  (p103 zenon_Vhq)
% 13.94/14.27  (-. (p108 zenon_Vsq))
% 13.94/14.27  (r1 Tau_0 Tau_1)
% 13.94/14.27  (zenon_Vfq != zenon_Voq)
% 13.94/14.27  (p6 zenon_Vfq)
% 13.94/14.27  (zenon_Vpq != zenon_Vtq)
% 13.94/14.27  (p2 zenon_Vdq)
% 13.94/14.27  (zenon_Vgq != zenon_Vor)
% 13.94/14.27  (zenon_Voq != zenon_Vpr)
% 13.94/14.27  (-. (p107 Tau_1))
% 13.94/14.27  (zenon_Vgq != zenon_Vpr)
% 13.94/14.27  (-. (p100 zenon_Vda))
% 13.94/14.27  (zenon_Vfq != zenon_Vqq)
% 13.94/14.27  (p5 zenon_Vu)
% 13.94/14.27  (zenon_Vrq != zenon_Vkr)
% 13.94/14.27  (-. (p105 zenon_Vum))
% 13.94/14.27  (p103 zenon_Vkq)
% 13.94/14.27  (p100 zenon_Vfq)
% 13.94/14.27  (-. (p106 Tau_0))
% 13.94/14.27  (zenon_Voq != zenon_Vuq)
% 13.94/14.27  (zenon_Vjq != zenon_Vfr)
% 13.94/14.27  (zenon_Viq != zenon_Vjj)
% 13.94/14.27  (zenon_Vdq != zenon_Vcl)
% 13.94/14.27  (zenon_Vjq != zenon_Vtq)
% 13.94/14.27  (-. (p109 zenon_Vda))
% 13.94/14.27  (p6 zenon_Vgq)
% 13.94/14.27  (zenon_Viq != zenon_Vnr)
% 13.94/14.27  (zenon_Vfq != zenon_Vlr)
% 13.94/14.27  (-. (p103 zenon_X14))
% 13.94/14.27  (-. (p108 zenon_Vtq))
% 13.94/14.27  (zenon_Vrq != zenon_Vda)
% 13.94/14.27  (zenon_Vsq != zenon_Vuq)
% 13.94/14.27  (zenon_Voq != zenon_Vjr)
% 13.94/14.27  (p3 zenon_Vcq)
% 13.94/14.27  (-. (p104 Tau_0))
% 13.94/14.27  (p1 zenon_Vnq)
% 13.94/14.27  (p107 zenon_Vhq)
% 13.94/14.27  (zenon_Vjq != zenon_Vvq)
% 13.94/14.27  (zenon_Vkq != zenon_Vmr)
% 13.94/14.27  (p101 zenon_Vpq)
% 13.94/14.27  (zenon_Vsq != zenon_X14)
% 13.94/14.27  (r1 zenon_Viq zenon_Vhq)
% 13.94/14.27  (zenon_Vpq != zenon_Vir)
% 13.94/14.27  (p108 zenon_Vcq)
% 13.94/14.27  (-. (p111 zenon_Vgq))
% 13.94/14.27  (-. (p110 zenon_Veq))
% 13.94/14.27  (zenon_Vhq != zenon_Vda)
% 13.94/14.27  (zenon_Vdq != zenon_Vjj)
% 13.94/14.27  (zenon_Vqq != zenon_Vph)
% 13.94/14.27  (p102 zenon_Vpq)
% 13.94/14.27  (-. (p108 zenon_Vbc))
% 13.94/14.27  (zenon_Vqq != zenon_Vcl)
% 13.94/14.27  (zenon_Vcq != zenon_Veq)
% 13.94/14.27  (zenon_Vpq != zenon_Vuf)
% 13.94/14.27  (-. (p107 zenon_Vyd))
% 13.94/14.27  (zenon_Vtq != zenon_Vuq)
% 13.94/14.27  (-. (p109 zenon_Vrq))
% 13.94/14.27  (p106 zenon_Vdq)
% 13.94/14.27  (zenon_Voq != zenon_Vor)
% 13.94/14.27  (zenon_Vtq != zenon_Vrr)
% 13.94/14.27  (-. (p109 zenon_Vum))
% 13.94/14.27  (p100 zenon_Vsq)
% 13.94/14.27  (zenon_Vnq != zenon_Vjj)
% 13.94/14.27  (-. (p110 zenon_Vtq))
% 13.94/14.27  (zenon_Vgq != zenon_Vsq)
% 13.94/14.27  (zenon_Vfq != zenon_Vrq)
% 13.94/14.27  (p8 zenon_Veq)
% 13.94/14.27  (zenon_Vuq != zenon_Vor)
% 13.94/14.27  (p101 zenon_Vrq)
% 13.94/14.27  (zenon_Vrq != zenon_Vcl)
% 13.94/14.27  (zenon_Vlq != zenon_X14)
% 13.94/14.27  (zenon_Vjq != zenon_Vkq)
% 13.94/14.27  (-. (p106 zenon_Vuq))
% 13.94/14.27  (zenon_Vgq != zenon_Vnr)
% 13.94/14.27  (p2 zenon_Vcq)
% 13.94/14.27  (-. (p111 Tau_2))
% 13.94/14.27  (zenon_Voq != zenon_Vyd)
% 13.94/14.27  (p103 zenon_Vfq)
% 13.94/14.27  (p108 zenon_Vdq)
% 13.94/14.27  (-. (p104 zenon_Vir))
% 13.94/14.27  (r1 zenon_Vmq zenon_Vlq)
% 13.94/14.27  (-. (p102 zenon_Vph))
% 13.94/14.27  (zenon_Veq != zenon_Vuq)
% 13.94/14.27  (r1 zenon_Vhq zenon_Veq)
% 13.94/14.27  (zenon_Vpq != zenon_Vda)
% 13.94/14.27  (r1 zenon_Vsq zenon_Vqq)
% 13.94/14.27  (zenon_Vfq != zenon_Vnr)
% 13.94/14.27  (zenon_Vsq != zenon_Vrr)
% 13.94/14.27  (zenon_Viq != zenon_Vtq)
% 13.94/14.27  (p10 zenon_Vcq)
% 13.94/14.27  (zenon_Vjq != zenon_Vrr)
% 13.94/14.27  (p109 zenon_Veq)
% 13.94/14.27  (zenon_Viq != zenon_Vqq)
% 13.94/14.27  (zenon_Vrq != zenon_Vmr)
% 13.94/14.27  (-. (p107 zenon_Vph))
% 13.94/14.27  (p1 zenon_Vfq)
% 13.94/14.27  (-. (p106 zenon_Vrq))
% 13.94/14.27  (zenon_Vmq != zenon_Vqq)
% 13.94/14.27  (p102 zenon_Vfq)
% 13.94/14.27  (zenon_Veq != zenon_Vbr)
% 13.94/14.27  (-. (p105 zenon_Vda))
% 13.94/14.27  (p104 zenon_Vlq)
% 13.94/14.27  (-. (p109 zenon_Vhq))
% 13.94/14.27  (zenon_Vqq != zenon_Vpr)
% 13.94/14.27  (zenon_Vcq != zenon_Vum)
% 13.94/14.27  (-. (p111 zenon_Vdq))
% 13.94/14.27  (-. (p111 zenon_X14))
% 13.94/14.27  (zenon_Viq != zenon_Voq)
% 13.94/14.27  (p104 zenon_Veq)
% 13.94/14.27  (zenon_Vkq != zenon_Vfr)
% 13.94/14.27  (-. (p103 zenon_Vcl))
% 13.94/14.27  (zenon_Vdq != zenon_Vmq)
% 13.94/14.27  (p2 zenon_Vnq)
% 13.94/14.27  (zenon_Vfq != zenon_X14)
% 13.94/14.27  (-. (p107 Tau_0))
% 13.94/14.27  (zenon_Vlq != zenon_Vsq)
% 13.94/14.27  (zenon_Vjq != zenon_Vda)
% 13.94/14.27  (p6 zenon_Vnq)
% 13.94/14.27  (zenon_Vgq != zenon_Vbc)
% 13.94/14.27  (zenon_Vtq != zenon_Vcl)
% 13.94/14.27  (p100 zenon_Vvq)
% 13.94/14.27  (-. (p109 Tau_2))
% 13.94/14.27  (-. (p108 zenon_Vqq))
% 13.94/14.27  (zenon_Veq != zenon_Vcl)
% 13.94/14.27  (zenon_Vfq != zenon_Vuq)
% 13.94/14.27  (p2 zenon_Vmq)
% 13.94/14.27  (zenon_Vdq != zenon_Vyq)
% 13.94/14.27  (zenon_Vrq != zenon_Vuf)
% 13.94/14.27  (zenon_Vlq != zenon_Vcl)
% 13.94/14.27  (zenon_Viq != zenon_Vvq)
% 13.94/14.27  (zenon_Vkq != zenon_Vbc)
% 13.94/14.27  (zenon_Vvq != zenon_Vuf)
% 13.94/14.27  (p100 zenon_Vcq)
% 13.94/14.27  (zenon_Vpq != zenon_Vnr)
% 13.94/14.27  (-. (p107 zenon_Vkq))
% 13.94/14.27  (zenon_Vdq != zenon_Vcq)
% 13.94/14.27  (zenon_Veq != zenon_Vda)
% 13.94/14.27  (-. (p102 zenon_Vda))
% 13.94/14.27  (zenon_Vgq != zenon_Vrq)
% 13.94/14.27  (-. (p109 zenon_X14))
% 13.94/14.27  (zenon_Vpq != zenon_Vjj)
% 13.94/14.27  (zenon_Vdq != zenon_Vlq)
% 13.94/14.27  (p1 zenon_Viq)
% 13.94/14.27  (zenon_Vcq != zenon_Vkq)
% 13.94/14.27  (zenon_Vvq != zenon_Vbc)
% 13.94/14.27  (zenon_Vfq != zenon_Vph)
% 13.94/14.27  (zenon_Vmq != zenon_Vbc)
% 13.94/14.27  (zenon_Vdq != zenon_Vyd)
% 13.94/14.27  (zenon_Veq != zenon_Vcr)
% 13.94/14.27  (zenon_Vpq != zenon_Vyd)
% 13.94/14.27  (zenon_Vdq != zenon_Vjq)
% 13.94/14.27  (-. (p108 Tau_0))
% 13.94/14.27  (-. (p109 zenon_Vuq))
% 13.94/14.27  (p101 zenon_Vcq)
% 13.94/14.27  (p103 zenon_Vgq)
% 13.94/14.27  (p104 zenon_Voq)
% 13.94/14.27  (zenon_Voq != zenon_Vtq)
% 13.94/14.27  (zenon_Vmq != zenon_Vsq)
% 13.94/14.27  (zenon_Vcq != zenon_Vjj)
% 13.94/14.27  (zenon_Vuq != zenon_Vlo)
% 13.94/14.27  (zenon_Vdq != zenon_Vbc)
% 13.94/14.27  (r1 Tau_0 zenon_Vuq)
% 13.94/14.27  (r1 Tau_0 zenon_Vvq)
% 13.94/14.27  (zenon_Vlq != zenon_Voq)
% 13.94/14.27  (r1 Tau_1 zenon_Vsq)
% 13.94/14.27  (r1 Tau_1 zenon_Vtq)
% 13.94/14.27  (zenon_Vjq != zenon_Ver)
% 13.94/14.27  (zenon_Vvq != zenon_Vcl)
% 13.94/14.27  (zenon_Vcq != zenon_Vlq)
% 13.94/14.27  (zenon_Vpq != zenon_Vcl)
% 13.94/14.27  (p1 zenon_Vjq)
% 13.94/14.27  (-. (p109 zenon_Vmq))
% 13.94/14.27  (zenon_Vjq != zenon_Vum)
% 13.94/14.27  (p5 zenon_Vpq)
% 13.94/14.27  (zenon_Vhq != zenon_Voq)
% 13.94/14.27  (zenon_Vmq != zenon_Vcl)
% 13.94/14.27  (zenon_Vvq != zenon_Vlo)
% 13.94/14.27  (zenon_Voq != zenon_Vkr)
% 13.94/14.27  (-. (p111 zenon_Vnq))
% 13.94/14.27  (-. (p110 zenon_Vsq))
% 13.94/14.27  (zenon_Vkq != zenon_Vum)
% 13.94/14.27  (Tau_2 != Tau_1)
% 13.94/14.27  (zenon_Vcq != zenon_Vir)
% 13.94/14.27  (p101 zenon_Vlq)
% 13.94/14.27  (zenon_Vpq != zenon_Vkr)
% 13.94/14.27  (-. (p107 zenon_X14))
% 13.94/14.27  (zenon_Vmq != zenon_Vum)
% 13.94/14.27  (-. (p101 zenon_Vcl))
% 13.94/14.27  (p4 zenon_Voq)
% 13.94/14.27  (zenon_Vjq != zenon_Vbc)
% 13.94/14.27  (r1 zenon_Viq zenon_Vgq)
% 13.94/14.27  (zenon_Viq != zenon_Vnq)
% 13.94/14.27  (p5 zenon_Vcq)
% 13.94/14.27  (zenon_Vgq != zenon_Vfr)
% 13.94/14.27  (p103 zenon_Vmq)
% 13.94/14.27  (zenon_Vrq != zenon_Vum)
% 13.94/14.27  (p3 zenon_Vpq)
% 13.94/14.27  (zenon_Vlq != zenon_Vph)
% 13.94/14.27  (p105 zenon_Vmq)
% 13.94/14.27  (zenon_Vnq != zenon_Vuq)
% 13.94/14.27  (-. (p108 zenon_Vyd))
% 13.94/14.27  (-. (p107 zenon_Voq))
% 13.94/14.27  (zenon_Vfq != zenon_Vpr)
% 13.94/14.27  (zenon_Vlq != zenon_Vqq)
% 13.94/14.27  (zenon_Vhq != zenon_Vbc)
% 13.94/14.27  (-. (p11 zenon_Vcq))
% 13.94/14.27  (zenon_Vcq != zenon_Vnq)
% 13.94/14.27  (-. (p110 zenon_Vwq))
% 13.94/14.27  (zenon_Vkq != zenon_Vph)
% 13.94/14.27  (zenon_Vlq != zenon_Vor)
% 13.94/14.27  (p105 zenon_Vnq)
% 13.94/14.27  (r1 zenon_Vnq zenon_Vlq)
% 13.94/14.27  (zenon_Vu != zenon_Voq)
% 13.94/14.27  (-. (p101 zenon_X14))
% 13.94/14.27  (zenon_Vdq != zenon_X3)
% 13.94/14.27  (zenon_Veq != zenon_Vmq)
% 13.94/14.27  (zenon_Veq != zenon_Vir)
% 13.94/14.27  (zenon_Vgq != zenon_Vuf)
% 13.94/14.27  (-. (p103 Tau_0))
% 13.94/14.27  (zenon_Vnq != zenon_Vrq)
% 13.94/14.27  (zenon_Vsq != zenon_Vda)
% 13.94/14.27  (zenon_Vtq != zenon_Vsq)
% 13.94/14.27  (zenon_Veq != zenon_Vfr)
% 13.94/14.27  (zenon_Vsq != zenon_Vbc)
% 13.94/14.27  (r1 zenon_Vgq zenon_Vfq)
% 13.94/14.27  (zenon_Veq != zenon_Vkq)
% 13.94/14.27  (-. (p102 zenon_Vuq))
% 13.94/14.27  (zenon_Vdq != zenon_Vor)
% 13.94/14.27  (zenon_Vgq != zenon_Vvq)
% 13.94/14.27  (zenon_Vnq != zenon_Vor)
% 13.94/14.27  (zenon_Vfq != zenon_Vum)
% 13.94/14.27  (p5 zenon_Vnq)
% 13.94/14.27  (-. (p102 Tau_0))
% 13.94/14.27  (-. (p108 zenon_Vum))
% 13.94/14.27  (zenon_Voq != zenon_Vda)
% 13.94/14.27  (zenon_Veq != zenon_Vpr)
% 13.94/14.27  (zenon_Vkq != zenon_Vda)
% 13.94/14.27  (zenon_Vfq != zenon_Vzq)
% 13.94/14.27  (p9 zenon_Vcq)
% 13.94/14.27  (zenon_Vrq != zenon_Vlr)
% 13.94/14.27  (zenon_Vlq != zenon_Vpq)
% 13.94/14.27  (zenon_Vdq != zenon_Vnq)
% 13.94/14.27  (zenon_Vuq != zenon_X14)
% 13.94/14.27  (zenon_Vsq != zenon_Vmr)
% 13.94/14.27  (zenon_Vlq != zenon_Vkq)
% 13.94/14.27  (p108 zenon_Vfq)
% 13.94/14.27  (zenon_Vhq != zenon_Vmr)
% 13.94/14.27  (zenon_Vpq != zenon_Vlr)
% 13.94/14.27  (zenon_Vkq != zenon_Vjj)
% 13.94/14.27  (zenon_Vhq != zenon_Viq)
% 13.94/14.27  (-. (p104 zenon_Vum))
% 13.94/14.27  (p6 zenon_Vdq)
% 13.94/14.27  (r1 Tau_0 Tau_2)
% 13.94/14.27  (zenon_Vdq != zenon_Vfr)
% 13.94/14.27  (zenon_Voq != zenon_Vbc)
% 13.94/14.27  (zenon_Vjq != zenon_Vnr)
% 13.94/14.27  (zenon_Vfq != zenon_Vda)
% 13.94/14.27  (p5 zenon_Veq)
% 13.94/14.27  (p3 zenon_Vqq)
% 13.94/14.27  (zenon_Vqq != zenon_Vor)
% 13.94/14.27  (zenon_Vsq != zenon_Vpr)
% 13.94/14.27  (zenon_Voq != zenon_Vnr)
% 13.94/14.27  (zenon_Vgq != zenon_Vir)
% 13.94/14.27  (zenon_Vhq != zenon_Vdr)
% 13.94/14.27  (zenon_Vlq != zenon_Vbc)
% 13.94/14.27  (p11 zenon_Vdq)
% 13.94/14.27  (zenon_Viq != zenon_Vor)
% 13.94/14.27  (zenon_Vmq != zenon_Vjr)
% 13.94/14.27  (zenon_Viq != zenon_Vmq)
% 13.94/14.27  (zenon_Veq != zenon_Vnr)
% 13.94/14.27  (zenon_Vkq != zenon_Vuf)
% 13.94/14.28  (zenon_Vqq != zenon_Vum)
% 13.94/14.28  (zenon_Vnq != zenon_Vmr)
% 13.94/14.28  (p1 zenon_Vlq)
% 13.94/14.28  (zenon_Vpq != zenon_Vbc)
% 13.94/14.28  (zenon_Veq != zenon_Vlo)
% 13.94/14.28  (-. (p109 zenon_Vtq))
% 13.94/14.28  (zenon_Vcq != zenon_Vpr)
% 13.94/14.28  (-. (p111 zenon_Vlq))
% 13.94/14.28  (zenon_Vhq != zenon_Vir)
% 13.94/14.28  (p5 zenon_Vjq)
% 13.94/14.28  (p2 zenon_Vvq)
% 13.94/14.28  (zenon_Vcq != zenon_Vor)
% 13.94/14.28  (p102 zenon_Vqq)
% 13.94/14.28  (-. (p105 zenon_Vgr))
% 13.94/14.28  (p104 zenon_Viq)
% 13.94/14.28  (zenon_Vhq != zenon_Vmq)
% 13.94/14.28  (zenon_Vsq != zenon_Vjj)
% 13.94/14.28  (zenon_Vkq != zenon_Voq)
% 13.94/14.28  (p4 zenon_Vjq)
% 13.94/14.28  (-. (p100 zenon_X3))
% 13.94/14.28  (p102 zenon_Vkq)
% 13.94/14.28  (zenon_Vmq != zenon_Vnr)
% 13.94/14.28  (zenon_Vnq != zenon_Vnr)
% 13.94/14.28  (-. (p107 zenon_Vsq))
% 13.94/14.28  (-. (p106 zenon_Voq))
% 13.94/14.28  (zenon_Vlq != zenon_Vmr)
% 13.94/14.28  (zenon_Vkq != zenon_Vir)
% 13.94/14.28  (zenon_Vdq != zenon_Vvq)
% 13.94/14.28  (zenon_Veq != zenon_Vbc)
% 13.94/14.28  (p2 zenon_Vgq)
% 13.94/14.28  (-. (p104 zenon_Vsq))
% 13.94/14.28  (p108 zenon_Veq)
% 13.94/14.28  (zenon_Veq != zenon_Vlq)
% 13.94/14.28  (zenon_Vqq != zenon_Vrr)
% 13.94/14.28  (zenon_Vmq != zenon_Vor)
% 13.94/14.28  (-. (p108 zenon_Vrq))
% 13.94/14.28  (-. (p103 zenon_Vvq))
% 13.94/14.28  (-. (p107 zenon_Vcl))
% 13.94/14.28  (zenon_Vkq != zenon_Vgr)
% 13.94/14.28  (-. (p108 zenon_Vnq))
% 13.94/14.28  (zenon_Vmq != zenon_Vhr)
% 13.94/14.28  (r1 zenon_Vsq zenon_Vrq)
% 13.94/14.28  (zenon_Vhq != zenon_Vyd)
% 13.94/14.28  (-. (p107 zenon_Vum))
% 13.94/14.28  (p110 zenon_Vdq)
% 13.94/14.28  (p103 zenon_Viq)
% 13.94/14.28  (zenon_Vmq != zenon_Vkr)
% 13.94/14.28  (zenon_Vdq != zenon_Vkq)
% 13.94/14.28  (-. (p106 zenon_Vda))
% 13.94/14.28  (p106 zenon_Vfq)
% 13.94/14.28  (zenon_Vjq != zenon_Vmq)
% 13.94/14.28  (p1 zenon_Vvq)
% 13.94/14.28  (zenon_Veq != zenon_Vnq)
% 13.94/14.28  (zenon_Vqq != zenon_Vuq)
% 13.94/14.28  (p101 zenon_Vqq)
% 13.94/14.28  (r1 zenon_Vhq zenon_Vfq)
% 13.94/14.28  (zenon_Vnq != zenon_Vuf)
% 13.94/14.28  (p102 zenon_Vnq)
% 13.94/14.28  (p2 zenon_Vhq)
% 13.94/14.28  (zenon_Vtq != zenon_Vyd)
% 13.94/14.28  (r1 zenon_Vrq zenon_Vpq)
% 13.94/14.28  (zenon_Vkq != zenon_Vlr)
% 13.94/14.28  (-. (p111 zenon_Vkq))
% 13.94/14.28  (r1 zenon_Vgq zenon_Veq)
% 13.94/14.28  (zenon_Vfq != zenon_X3)
% 13.94/14.28  (zenon_Vnq != zenon_Vmq)
% 13.94/14.28  (zenon_Vgq != zenon_Vjr)
% 13.94/14.28  (zenon_Vfq != zenon_Ver)
% 13.94/14.28  (-. (p105 zenon_X14))
% 13.94/14.28  (zenon_Vmq != zenon_Vir)
% 13.94/14.28  (r1 zenon_Vfq zenon_Vcq)
% 13.94/14.28  (zenon_Veq != zenon_Vzq)
% 13.94/14.28  (-. (p108 zenon_Vlq))
% 13.94/14.28  (zenon_Vdq != zenon_Vwq)
% 13.94/14.28  (zenon_Vnq != zenon_Vbc)
% 13.94/14.28  (zenon_Vvq != zenon_Vum)
% 13.94/14.28  (zenon_Vfq != zenon_Vdr)
% 13.94/14.28  (p103 zenon_Vlq)
% 13.94/14.28  (zenon_Vgq != zenon_Vda)
% 13.94/14.28  (zenon_Vfq != zenon_Vmq)
% 13.94/14.28  (p107 zenon_Vdq)
% 13.94/14.28  (p6 zenon_Veq)
% 13.94/14.28  (zenon_Vdq != zenon_Vnr)
% 13.94/14.28  (-. (p110 zenon_Vuq))
% 13.94/14.28  (zenon_Vfq != zenon_Vir)
% 13.94/14.28  (zenon_Vfq != zenon_Vrr)
% 13.94/14.28  (zenon_Vfq != zenon_Vnq)
% 13.94/14.28  (zenon_Vdq != zenon_Vda)
% 13.94/14.28  (zenon_Veq != zenon_Vyd)
% 13.94/14.28  (zenon_Vhq != zenon_Vum)
% 13.94/14.28  (zenon_Vjq != zenon_Vrq)
% 13.94/14.28  (zenon_Vlq != zenon_Vyd)
% 13.94/14.28  (p103 zenon_Vpq)
% 13.94/14.28  (Tau_1 != zenon_Vda)
% 13.94/14.28  (Tau_1 != zenon_Vbc)
% 13.94/14.28  (Tau_1 != zenon_Vyd)
% 13.94/14.28  (Tau_1 != zenon_Vuf)
% 13.94/14.28  (Tau_1 != zenon_Vph)
% 13.94/14.28  (Tau_1 != zenon_Vjj)
% 13.94/14.28  (Tau_1 != zenon_Vcl)
% 13.94/14.28  (Tau_1 != zenon_Vum)
% 13.94/14.28  (Tau_1 != zenon_Vlo)
% 13.94/14.28  (Tau_1 != zenon_Vrr)
% 13.94/14.28  (Tau_1 != zenon_Vor)
% 13.94/14.28  (Tau_1 != zenon_Vpr)
% 13.94/14.28  (zenon_Viq != zenon_Vph)
% 13.94/14.28  (zenon_Vnq != zenon_Vda)
% 13.94/14.28  (p102 zenon_Vmq)
% 13.94/14.28  (zenon_Vdq != zenon_Vqq)
% 13.94/14.28  (zenon_Vcq != zenon_Vqq)
% 13.94/14.28  (zenon_Vsq != zenon_Vuf)
% 13.94/14.28  (zenon_Vkq != zenon_Vnq)
% 13.94/14.28  (zenon_Viq != zenon_Vlo)
% 13.94/14.28  (zenon_Vtq != zenon_Vmr)
% 13.94/14.28  (zenon_Vkq != zenon_Vrq)
% 13.94/14.28  (zenon_Vcq != zenon_Vbc)
% 13.94/14.28  (-. (p109 zenon_Vph))
% 13.94/14.28  (zenon_Vfq != zenon_Vcl)
% 13.94/14.28  (-. (p110 Tau_1))
% 13.94/14.28  (-. (p109 zenon_Vyd))
% 13.94/14.28  (p102 zenon_Vgq)
% 13.94/14.28  (-. (p103 zenon_Vyd))
% 13.94/14.28  (zenon_Vgq != zenon_Vqq)
% 13.94/14.28  (zenon_Vfq != zenon_Vfr)
% 13.94/14.28  (zenon_Vvq != zenon_X14)
% 13.94/14.28  (-. (p104 zenon_Vjr))
% 13.94/14.28  (zenon_Vdq != zenon_Vgq)
% 13.94/14.28  (-. (p101 zenon_Vlo))
% 13.94/14.28  (-. (p111 zenon_Viq))
% 13.94/14.28  (p103 zenon_Vdq)
% 13.94/14.28  (zenon_Vqq != zenon_Vlo)
% 13.94/14.28  (p3 zenon_Vfq)
% 13.94/14.28  (-. (p101 zenon_Vbc))
% 13.94/14.28  (-. (p109 zenon_Viq))
% 13.94/14.28  (zenon_Vdq != zenon_Voq)
% 13.94/14.28  (p106 zenon_Veq)
% 13.94/14.28  (-. (p103 Tau_1))
% 13.94/14.28  (r1 zenon_Vtq zenon_Vqq)
% 13.94/14.28  (zenon_Viq != zenon_Vrq)
% 13.94/14.28  (zenon_Vcq != zenon_Vhq)
% 13.94/14.28  (-. (p107 zenon_Vvq))
% 13.94/14.28  (-. (p111 zenon_Vjq))
% 13.94/14.28  (zenon_Vmq != zenon_Vuf)
% 13.94/14.28  (p100 zenon_Vkq)
% 13.94/14.28  (-. (p106 zenon_Vmq))
% 13.94/14.28  (p107 zenon_Vcq)
% 13.94/14.28  (zenon_Vnq != zenon_Vgr)
% 13.94/14.28  (-. (p111 zenon_Vpq))
% 13.94/14.28  (-. (p103 zenon_Vtq))
% 13.94/14.28  (p102 zenon_Voq)
% 13.94/14.28  (zenon_Voq != zenon_Vlr)
% 13.94/14.28  (p101 zenon_Vtq)
% 13.94/14.28  (zenon_Vdq != zenon_Ver)
% 13.94/14.28  (zenon_Vnq != zenon_Vph)
% 13.94/14.28  (zenon_Vcq != zenon_Vvq)
% 13.94/14.28  (-. (p108 zenon_Vph))
% 13.94/14.28  (zenon_Vtq != zenon_Vor)
% 13.94/14.28  (p2 zenon_Vpq)
% 13.94/14.28  (zenon_Vfq != zenon_Vgr)
% 13.94/14.28  (p4 zenon_Vfq)
% 13.94/14.28  (-. (p108 zenon_Vcl))
% 13.94/14.28  (-. (p103 zenon_Vjj))
% 13.94/14.28  (p100 zenon_Viq)
% 13.94/14.28  (p2 zenon_Vsq)
% 13.94/14.28  (p101 zenon_Vkq)
% 13.94/14.28  (zenon_Vdq != zenon_Vpr)
% 13.94/14.28  (zenon_Vvq != zenon_Vjj)
% 13.94/14.28  (zenon_Vkq != zenon_Vvq)
% 13.94/14.28  (zenon_Vfq != zenon_Vlo)
% 13.94/14.28  (zenon_Vgq != zenon_Vbr)
% 13.94/14.28  (zenon_Vtq != zenon_Vjj)
% 13.94/14.28  (zenon_Vnq != zenon_Vum)
% 13.94/14.28  (zenon_Vmq != zenon_Vgr)
% 13.94/14.28  (-. (p106 zenon_Vpq))
% 13.94/14.28  (zenon_Vhq != zenon_Vkq)
% 13.94/14.28  (p101 zenon_Vhq)
% 13.94/14.28  (zenon_Vpq != zenon_Vph)
% 13.94/14.28  (zenon_Vqq != zenon_Vnr)
% 13.94/14.28  (p1 zenon_Vdq)
% 13.94/14.28  (-. (p102 zenon_Vum))
% 13.94/14.28  (-. (p109 zenon_Vkq))
% 13.94/14.28  (zenon_Veq != zenon_Vuf)
% 13.94/14.28  (p4 zenon_Vpq)
% 13.94/14.28  (zenon_Vjq != zenon_Vir)
% 13.94/14.28  (zenon_Vcq != zenon_Vmq)
% 13.94/14.28  (-. (p110 zenon_Vyd))
% 13.94/14.28  (-. (p7 zenon_Vkq))
% 13.94/14.28  (zenon_Voq != zenon_Vcl)
% 13.94/14.28  (-. (p109 zenon_Vlq))
% 13.94/14.28  (p104 zenon_Vjq)
% 13.94/14.28  (zenon_Vrq != zenon_Vyd)
% 13.94/14.28  (-. (p100 zenon_Vph))
% 13.94/14.28  (zenon_Vcq != zenon_X14)
% 13.94/14.28  (p104 zenon_Vmq)
% 13.94/14.28  (zenon_Veq != zenon_Vrr)
% 13.94/14.28  (p1 zenon_Vsq)
% 13.94/14.28  (p3 zenon_Vnq)
% 13.94/14.28  (p100 zenon_Vqq)
% 13.94/14.28  (p4 zenon_Vhq)
% 13.94/14.28  (-. (p110 Tau_2))
% 13.94/14.28  (p101 zenon_Vfq)
% 13.94/14.28  (p7 zenon_Vfq)
% 13.94/14.28  (p100 zenon_Vrq)
% 13.94/14.28  (p103 zenon_Veq)
% 13.94/14.28  (p102 zenon_Viq)
% 13.94/14.28  (zenon_Vgq != zenon_Vcl)
% 13.94/14.28  (-. (p109 zenon_Vjq))
% 13.94/14.28  (Tau_0 != zenon_Vda)
% 13.94/14.28  (Tau_0 != zenon_Vbc)
% 13.94/14.28  (Tau_0 != zenon_Vyd)
% 13.94/14.28  (Tau_0 != zenon_Vuf)
% 13.94/14.28  (Tau_0 != zenon_Vph)
% 13.94/14.28  (Tau_0 != zenon_Vjj)
% 13.94/14.28  (Tau_0 != zenon_Vcl)
% 13.94/14.28  (Tau_0 != zenon_Vum)
% 13.94/14.28  (Tau_0 != zenon_Vlo)
% 13.94/14.28  (Tau_0 != zenon_Vrr)
% 13.94/14.28  (zenon_Vtq != zenon_Vvq)
% 13.94/14.28  (zenon_Vlq != zenon_Vlr)
% 13.94/14.28  (zenon_Vhq != zenon_Vor)
% 13.94/14.28  (p107 zenon_Viq)
% 13.94/14.28  (zenon_Vdq != zenon_Vsq)
% 13.94/14.28  (-. (p110 zenon_Vkq))
% 13.94/14.28  (p6 zenon_Vjq)
% 13.94/14.28  (zenon_Viq != zenon_X3)
% 13.94/14.28  (p103 zenon_Vjq)
% 13.94/14.28  (-. (p103 zenon_Vuq))
% 13.94/14.28  (-. (p108 zenon_Vkq))
% 13.94/14.28  (zenon_Vgq != zenon_Vlq)
% 13.94/14.28  (zenon_Vqq != zenon_Vjj)
% 13.94/14.28  (p101 Tau_2)
% 13.94/14.28  (p7 zenon_Vlq)
% 13.94/14.28  (zenon_Viq != zenon_Vkr)
% 13.94/14.28  (zenon_Vfq != zenon_Vor)
% 13.94/14.28  (-. (p110 zenon_Viq))
% 13.94/14.28  (-. (p103 zenon_Vum))
% 13.94/14.28  (r1 zenon_Vkq zenon_Viq)
% 13.94/14.28  (zenon_Vhq != zenon_Vgq)
% 13.94/14.28  (-. (p104 zenon_Vyd))
% 13.94/14.28  (-. (p100 zenon_X14))
% 13.94/14.28  (-. (p104 Tau_2))
% 13.94/14.28  (-. (p110 zenon_Vcl))
% 13.94/14.28  (zenon_Vlq != zenon_Vfr)
% 13.94/14.28  (zenon_Vnq != zenon_Vhr)
% 13.94/14.28  (-. (p106 zenon_Vsq))
% 13.94/14.28  (p104 zenon_Vfq)
% 13.94/14.28  (-. (p109 zenon_Vjj))
% 13.94/14.28  (zenon_Viq != zenon_Vbc)
% 13.94/14.28  (-. (p109 zenon_Vzq))
% 13.94/14.28  (zenon_Vkq != zenon_Vyd)
% 13.94/14.28  (zenon_Vdq != zenon_Vjr)
% 13.94/14.28  (zenon_Vpq != zenon_Vpr)
% 13.94/14.28  (zenon_Vgq != zenon_Vlr)
% 13.94/14.28  (zenon_Vmq != zenon_Vuq)
% 13.94/14.28  (zenon_Viq != zenon_Vkq)
% 13.94/14.28  (zenon_Vfq != zenon_Vyd)
% 13.94/14.28  (Tau_2 != zenon_X3)
% 13.94/14.28  (-. (p103 zenon_Vda))
% 13.94/14.28  (zenon_Vgq != zenon_Vum)
% 13.94/14.28  (p2 zenon_Vqq)
% 13.94/14.28  (r1 zenon_Vpq zenon_Vmq)
% 13.94/14.28  (-. (p110 zenon_Vnq))
% 13.94/14.28  (zenon_Vfq != zenon_Vjq)
% 13.94/14.28  (zenon_Vrq != zenon_X3)
% 13.94/14.28  (zenon_Vsq != Tau_2)
% 13.94/14.28  (zenon_Vtq != Tau_2)
% 13.94/14.28  (zenon_Vqq != Tau_2)
% 13.94/14.28  (zenon_Vrq != Tau_2)
% 13.94/14.28  (zenon_Voq != Tau_2)
% 13.94/14.28  (zenon_Vpq != Tau_2)
% 13.94/14.28  (zenon_Vmq != Tau_2)
% 13.94/14.28  (zenon_Vnq != Tau_2)
% 13.94/14.28  (zenon_Vkq != Tau_2)
% 13.94/14.28  (zenon_Vlq != Tau_2)
% 13.94/14.28  (zenon_Viq != Tau_2)
% 13.94/14.28  (zenon_Vjq != Tau_2)
% 13.94/14.28  (zenon_Vgq != Tau_2)
% 13.94/14.28  (zenon_Vhq != Tau_2)
% 13.94/14.28  (zenon_Veq != Tau_2)
% 13.94/14.28  (zenon_Vfq != Tau_2)
% 13.94/14.28  (zenon_Vcq != Tau_2)
% 13.94/14.28  (zenon_Vdq != Tau_2)
% 13.94/14.28  (-. (p109 zenon_Voq))
% 13.94/14.28  (-. (p110 zenon_Vlq))
% 13.94/14.28  (zenon_Vcq != zenon_Vsq)
% 13.94/14.28  (zenon_Vcq != zenon_Vrr)
% 13.94/14.28  (zenon_Vcq != zenon_Vfr)
% 13.94/14.28  (Tau_2 != Tau_0)
% 13.94/14.28  (-. (p106 zenon_Vqq))
% 13.94/14.28  (p2 zenon_Vjq)
% 13.94/14.28  (zenon_Viq != zenon_Vdr)
% 13.94/14.28  (-. (p103 zenon_Vsq))
% 13.94/14.28  (zenon_Viq != zenon_Vda)
% 13.94/14.28  (-. (p105 zenon_Vyd))
% 13.94/14.28  (zenon_Vhq != zenon_Vpr)
% 13.94/14.28  (zenon_Vjq != zenon_Vkr)
% 13.94/14.28  (-. (p109 zenon_Vgq))
% 13.94/14.28  (zenon_Vdq != zenon_Vxq)
% 13.94/14.28  (r1 zenon_Vlq zenon_Vjq)
% 13.94/14.28  (-. (p111 zenon_Vyd))
% 13.94/14.28  (zenon_Vdq != zenon_Vdr)
% 13.94/14.28  (-. (p103 zenon_Vkr))
% 13.94/14.28  (-. (p107 zenon_Vdr))
% 13.94/14.28  (zenon_Vgq != zenon_Voq)
% 13.94/14.28  (p8 zenon_Vjq)
% 13.94/14.28  (r1 zenon_Vnq zenon_Vkq)
% 13.94/14.28  (p7 zenon_Vgq)
% 13.94/14.28  (zenon_Viq != zenon_Vir)
% 13.94/14.28  (-. (p110 zenon_Voq))
% 13.94/14.28  (p7 zenon_Vdq)
% 13.94/14.28  (zenon_Veq != zenon_Vsq)
% 13.94/14.28  (-. (p110 zenon_Vgq))
% 13.94/14.28  (zenon_Vhq != zenon_Vqq)
% 13.94/14.28  (zenon_Viq != zenon_Vuq)
% 13.94/14.28  (zenon_Vmq != zenon_Vda)
% 13.94/14.28  (zenon_Vmq != zenon_Vpq)
% 13.94/14.28  (zenon_Vgq != zenon_Viq)
% 13.94/14.28  (p102 zenon_Vjq)
% 13.94/14.28  (zenon_Vtq != zenon_Vum)
% 13.94/14.28  (zenon_Vgq != zenon_Vjq)
% 13.94/14.28  (zenon_Vkq != zenon_Vcl)
% 13.94/14.28  (zenon_Veq != zenon_X14)
% 13.94/14.28  (-. (p102 zenon_X14))
% 13.94/14.28  (zenon_Voq != zenon_Vrr)
% 13.94/14.28  (-. (p110 zenon_Vvq))
% 13.94/14.28  (p100 zenon_Vjq)
% 13.94/14.28  (p1 zenon_Vuq)
% 13.94/14.28  (zenon_Vqq != zenon_Vda)
% 13.94/14.28  (-. (p107 zenon_Vda))
% 13.94/14.28  (p105 zenon_Veq)
% 13.94/14.28  (zenon_Vnq != zenon_Vlr)
% 13.94/14.28  (zenon_Vrq != zenon_Vsq)
% 13.94/14.28  (zenon_Vpq != zenon_X14)
% 13.94/14.28  (-. (p110 zenon_Vjj))
% 13.94/14.28  (zenon_Vkq != zenon_X14)
% 13.94/14.28  (zenon_Vgq != zenon_Var)
% 13.94/14.28  (zenon_Vcq != zenon_Ver)
% 13.94/14.28  (p8 zenon_Vgq)
% 13.94/14.28  (zenon_Vcq != zenon_Vnr)
% 13.94/14.28  (-. (p109 zenon_Vuf))
% 13.94/14.28  (zenon_Vgq != zenon_Vpq)
% 13.94/14.28  (zenon_Vhq != zenon_Vuf)
% 13.94/14.28  (zenon_Viq != zenon_Vlr)
% 13.94/14.28  (zenon_Vcq != zenon_Vcl)
% 13.94/14.28  (p1 zenon_Vmq)
% 13.94/14.28  (p7 zenon_Veq)
% 13.94/14.28  (zenon_Vcq != zenon_Vgr)
% 13.94/14.28  (zenon_Vjq != zenon_Vdr)
% 13.94/14.28  (p7 zenon_Vjq)
% 13.94/14.28  (-. (p102 zenon_Vvq))
% 13.94/14.28  (zenon_Vfq != zenon_Vvq)
% 13.94/14.28  (-. (p105 zenon_Vpq))
% 13.94/14.28  (zenon_Vlq != zenon_Vhr)
% 13.94/14.28  (-. (p101 zenon_Vuf))
% 13.94/14.28  (zenon_Vcq != zenon_Vkr)
% 13.94/14.28  (p101 zenon_Vjq)
% 13.94/14.28  (-. (p109 zenon_Vpq))
% 13.94/14.28  (zenon_Vlq != zenon_Vuf)
% 13.94/14.28  (p102 zenon_Vcq)
% 13.94/14.28  (zenon_Vvq != zenon_Vpr)
% 13.94/14.28  (zenon_Vsq != zenon_Vlo)
% 13.94/14.28  (-. (p106 zenon_Vph))
% 13.94/14.28  (r1 zenon_Vtq zenon_Vrq)
% 13.94/14.28  (p108 zenon_Vhq)
% 13.94/14.28  (zenon_Veq != zenon_Ver)
% 13.94/14.28  (p105 zenon_Viq)
% 13.94/14.28  (zenon_Vfq != zenon_Vgq)
% 13.94/14.28  (r1 zenon_Voq zenon_Vmq)
% 13.94/14.28  (-. (p111 zenon_Vfq))
% 13.94/14.28  (zenon_Vvq != zenon_Vph)
% 13.94/14.28  (zenon_Vlq != zenon_Vkr)
% 13.94/14.28  (zenon_Vjq != zenon_Vph)
% 13.94/14.28  (-. (p101 Tau_0))
% 13.94/14.28  (-. (p108 zenon_X14))
% 13.94/14.28  (-. (p110 zenon_Vda))
% 13.94/14.28  (zenon_Vgq != zenon_X14)
% 13.94/14.28  (-. (p108 Tau_1))
% 13.94/14.28  (zenon_Vdq != zenon_Viq)
% 13.94/14.28  (zenon_Voq != zenon_Vir)
% 13.94/14.28  (zenon_Vfq != zenon_Vyq)
% 13.94/14.28  (zenon_Voq != zenon_Vph)
% 13.94/14.28  (zenon_Vtq != zenon_Vph)
% 13.94/14.28  (zenon_Voq != zenon_Vmr)
% 13.94/14.28  (zenon_Vnq != zenon_X3)
% 13.94/14.28  (-. (p111 zenon_Veq))
% 13.94/14.28  (-. (p106 zenon_Vlo))
% 13.94/14.28  (zenon_Vfq != zenon_Vlq)
% 13.94/14.28  (p104 zenon_Vcq)
% 13.94/14.28  (Tau_0 != zenon_X3)
% 13.94/14.28  (zenon_Vkq != zenon_X3)
% 13.94/14.28  (p103 zenon_Vcq)
% 13.94/14.28  (-. (p111 zenon_Voq))
% 13.94/14.28  (-. (p100 zenon_Vyd))
% 13.94/14.28  (zenon_Vjq != zenon_Vcl)
% 13.94/14.28  (zenon_Vfq != zenon_Vpq)
% 13.94/14.28  (p6 zenon_Vcq)
% 13.94/14.28  (zenon_Voq != zenon_X3)
% 13.94/14.28  (-. (p104 zenon_Vbc))
% 13.94/14.28  (p5 zenon_Viq)
% 13.94/14.28  (zenon_Vqq != zenon_Vmr)
% 13.94/14.28  (zenon_Vlq != zenon_Vjj)
% 13.94/14.28  (-. (p102 zenon_Vlo))
% 13.94/14.28  (p105 zenon_Vfq)
% 13.94/14.28  (-. (p111 zenon_Vqq))
% 13.94/14.28  (r1 zenon_Veq zenon_Vdq)
% 13.94/14.28  (p3 zenon_Veq)
% 13.94/14.28  (zenon_Vhq != zenon_Vcr)
% 13.94/14.28  (zenon_Vhq != zenon_Vph)
% 13.94/14.28  (-. (p105 zenon_Vsq))
% 13.94/14.28  (zenon_Vdq != zenon_X14)
% 13.94/14.28  (zenon_Vqq != zenon_Vuf)
% 13.94/14.28  (zenon_Vqq != zenon_Vbc)
% 13.94/14.28  (zenon_Vjq != zenon_Vmr)
% 13.94/14.28  (-. (p104 zenon_Vrq))
% 13.94/14.28  (zenon_Voq != zenon_Vjj)
% 13.94/14.28  (p4 zenon_Vcq)
% 13.94/14.28  (-. (p108 zenon_Vjj))
% 13.94/14.28  (zenon_Vsq != zenon_Vcl)
% 13.94/14.28  (zenon_Vlq != zenon_Vir)
% 13.94/14.28  (zenon_Vuq != zenon_Vjj)
% 13.94/14.28  (p108 zenon_Vgq)
% 13.94/14.28  (zenon_Vqq != zenon_Vkr)
% 13.94/14.28  (zenon_Vhq != zenon_Vrr)
% 13.94/14.28  (-. (p100 zenon_Vrr))
% 13.94/14.28  (-. (p105 zenon_Vbc))
% 13.94/14.28  (p10 zenon_Vdq)
% 13.94/14.28  (-. (p109 zenon_Vcl))
% 13.94/14.28  (zenon_Viq != zenon_Vmr)
% 13.94/14.28  (-. (p105 zenon_Vjj))
% 13.94/14.28  (zenon_Vuq != zenon_Vrr)
% 13.94/14.28  (zenon_Vfq != zenon_Vjj)
% 13.94/14.28  (zenon_Vdq != zenon_Veq)
% 13.94/14.28  (p3 zenon_Voq)
% 13.94/14.28  (p8 zenon_Vdq)
% 13.94/14.28  (zenon_Veq != zenon_Vph)
% 13.94/14.28  (p4 zenon_Vgq)
% 13.94/14.28  (-. (p105 zenon_Vph))
% 13.94/14.28  (zenon_Vtq != zenon_X3)
% 13.94/14.28  (zenon_Vnq != zenon_Vpr)
% 13.94/14.28  (p1 zenon_Vpq)
% 13.94/14.28  (zenon_Veq != zenon_Vtq)
% 13.94/14.28  (p102 zenon_Vdq)
% 13.94/14.28  (zenon_Vfq != zenon_Viq)
% 13.94/14.28  (-. (p110 Tau_0))
% 13.94/14.28  (p101 zenon_Viq)
% 13.94/14.28  (zenon_Vnq != zenon_Vqq)
% 13.94/14.28  (zenon_Vdq != zenon_Vuq)
% 13.94/14.28  (-. (p110 zenon_Vhq))
% 13.94/14.28  (zenon_Vuq != zenon_Vda)
% 13.94/14.28  (-. (p6 zenon_Vmq))
% 13.94/14.28  (p100 zenon_Vdq)
% 13.94/14.28  (zenon_Veq != zenon_Var)
% 13.94/14.28  (p6 zenon_Vkq)
% 13.94/14.28  (zenon_Vpq != zenon_Vlo)
% 13.94/14.28  (zenon_Vfq != zenon_Vuf)
% 13.94/14.28  (-. (p106 zenon_Vuf))
% 13.94/14.28  (p100 zenon_Vlq)
% 13.94/14.28  (p103 zenon_Vqq)
% 13.94/14.28  (p1 zenon_Vgq)
% 13.94/14.28  (p9 zenon_Vdq)
% 13.94/14.28  (zenon_Vtq != zenon_X14)
% 13.94/14.28  (zenon_Vsq != zenon_X3)
% 13.94/14.28  (zenon_Vrq != zenon_X14)
% 13.94/14.28  (-. (p111 zenon_Vvq))
% 13.94/14.28  (zenon_Veq != zenon_Vkr)
% 13.94/14.28  (zenon_Vcq != zenon_Vyd)
% 13.94/14.28  (p106 zenon_Viq)
% 13.94/14.28  (-. (p105 zenon_Vlo))
% 13.94/14.28  (-. (p110 zenon_Vpq))
% 13.94/14.28  (-. (p111 Tau_1))
% 13.94/14.28  (-. (p107 zenon_Vbc))
% 13.94/14.28  (-. (p104 zenon_Vtq))
% 13.94/14.28  (zenon_Veq != zenon_Vqq)
% 13.94/14.28  (-. (p101 zenon_Vph))
% 13.94/14.28  (-. (p105 zenon_Voq))
% 13.94/14.28  (zenon_Vgq != zenon_Vuq)
% 13.94/14.28  (zenon_Vjq != zenon_Vlr)
% 13.94/14.28  (p5 zenon_Vdq)
% 13.94/14.28  (-. (p101 zenon_Vpr))
% 13.94/14.28  (-. (p103 zenon_Vlo))
% 13.94/14.28  (p100 zenon_Vtq)
% 13.94/14.28  (p101 zenon_Veq)
% 13.94/14.28  (zenon_Vpq != zenon_Voq)
% 13.94/14.28  (p1 zenon_Vqq)
% 13.94/14.28  (p6 zenon_Vhq)
% 13.94/14.28  (zenon_Veq != zenon_Vhr)
% 13.94/14.28  (zenon_Vdq != zenon_Vcr)
% 13.94/14.28  (-. (p102 Tau_1))
% 13.94/14.28  (p105 zenon_Vcq)
% 13.94/14.28  (-. (p105 Tau_0))
% 13.94/14.28  (zenon_Vnq != zenon_Vcl)
% 13.94/14.28  (zenon_Viq != zenon_Vpr)
% 13.94/14.28  (p110 zenon_Vcq)
% 13.94/14.28  (-. (p103 zenon_Vuf))
% 13.94/14.28  (-. (p110 zenon_Vbc))
% 13.94/14.28  (r1 zenon_Vjq zenon_Vhq)
% 13.94/14.28  (p9 zenon_Veq)
% 13.94/14.28  (zenon_Vcq != zenon_X3)
% 13.94/14.28  (-. (p106 zenon_Vum))
% 13.94/14.28  (zenon_Vmq != zenon_Vlo)
% 13.94/14.28  (-. (p108 zenon_Voq))
% 13.94/14.28  (-. (p106 zenon_Vtq))
% 13.94/14.28  (p4 zenon_Vmq)
% 13.94/14.28  (zenon_Vjq != zenon_Vpr)
% 13.94/14.28  (zenon_Vdq != zenon_Vbr)
% 13.94/14.28  (zenon_Vpq != zenon_Vuq)
% 13.94/14.28  (zenon_Vtq != zenon_Vlo)
% 13.94/14.28  (-. (p107 zenon_Vtq))
% 13.94/14.28  (p107 zenon_Veq)
% 13.94/14.28  (p100 Tau_0)
% 13.94/14.28  (p3 zenon_Vgq)
% 13.94/14.28  (zenon_Vhq != zenon_Vbr)
% 13.94/14.28  (zenon_Vdq != zenon_Vfq)
% 13.94/14.28  (-. (p2 Tau_1))
% 13.94/14.28  (zenon_Vhq != zenon_Vlq)
% 13.94/14.28  (p100 zenon_Vgq)
% 13.94/14.28  (-. (p109 Tau_0))
% 13.94/14.28  (zenon_Viq != zenon_Vrr)
% 13.94/14.28  (zenon_Vgq != zenon_Vrr)
% 13.94/14.28  (zenon_Vcq != zenon_Vmr)
% 13.94/14.28  (zenon_Vlq != zenon_Vnr)
% 13.94/14.28  (zenon_Vlq != zenon_Vvq)
% 13.94/14.28  (Tau_2 != zenon_X14)
% 13.94/14.28  (zenon_Vrq != zenon_Vjj)
% 13.94/14.28  (zenon_Vqq != zenon_X3)
% 13.94/14.28  (zenon_Vdq != zenon_Vir)
% 13.94/14.28  (r1 zenon_Voq zenon_Vnq)
% 13.94/14.28  (zenon_Vpq != zenon_Vvq)
% 13.94/14.28  (-. (p109 zenon_Vqq))
% 13.94/14.28  (zenon_Voq != zenon_Vum)
% 13.94/14.28  (-. (p100 zenon_Vjj))
% 13.94/14.28  (zenon_Vkq != zenon_Vuq)
% 13.94/14.28  (p2 zenon_Vkq)
% 13.94/14.28  (zenon_Vnq != zenon_Vpq)
% 13.94/14.28  (zenon_Vcq != zenon_Vph)
% 13.94/14.28  (-. (p111 zenon_Vlo))
% 13.94/14.28  (p109 zenon_Vdq)
% 13.94/14.28  (zenon_Vgq != zenon_Vyd)
% 13.94/14.28  (zenon_Vcq != zenon_Vlo)
% 13.94/14.28  (p104 zenon_Vnq)
% 13.94/14.28  (zenon_Vhq != zenon_Vnq)
% 13.94/14.28  (zenon_Vhq != zenon_Ver)
% 13.94/14.28  (r1 zenon_Vuq zenon_Vsq)
% 13.94/14.28  (-. (p110 zenon_Vqq))
% 13.94/14.28  (-. (p108 zenon_Var))
% 13.94/14.28  (zenon_Vgq != zenon_Ver)
% 13.94/14.28  (p100 zenon_Vpq)
% 13.94/14.28  (-. (p110 zenon_Vum))
% 13.94/14.28  (Tau_0 != zenon_X14)
% 13.94/14.28  (p106 zenon_Vgq)
% 13.94/14.28  (zenon_Vkq != zenon_Vmq)
% 13.94/14.28  (zenon_Vpq != zenon_Vmr)
% 13.94/14.28  (zenon_Vgq != zenon_Vhr)
% 13.94/14.28  (p100 zenon_Voq)
% 13.94/14.28  (zenon_Veq != zenon_Vjj)
% 13.94/14.28  (-. (p102 zenon_Vnr))
% 13.94/14.28  (zenon_Veq != zenon_Vmr)
% 13.94/14.28  (p101 zenon_Vvq)
% 13.94/14.28  (p107 zenon_Vjq)
% 13.94/14.28  (p104 zenon_Vdq)
% 13.94/14.28  (-. (p107 zenon_Vuf))
% 13.94/14.28  (zenon_Viq != zenon_Ver)
% 13.94/14.28  (p1 zenon_Veq)
% 13.94/14.28  (-. (p101 zenon_Vjj))
% 13.94/14.28  (p100 zenon_Veq)
% 13.94/14.28  (zenon_Vdq != zenon_Vkr)
% 13.94/14.28  (zenon_Viq != zenon_Vpq)
% 13.94/14.28  (-. (p108 zenon_Vpq))
% 13.94/14.28  (p100 zenon_Vmq)
% 13.94/14.28  (zenon_Vcq != zenon_Vdr)
% 13.94/14.28  (p1 zenon_Vcq)
% 13.94/14.28  (zenon_Vdq != zenon_Vhq)
% 13.94/14.28  (-. (p111 zenon_Vcq))
% 13.94/14.28  (zenon_Vcq != zenon_Voq)
% 13.94/14.28  (zenon_Veq != zenon_X3)
% 13.94/14.28  (zenon_Vnq != zenon_Voq)
% 13.94/14.28  (p106 zenon_Vhq)
% 13.94/14.28  (zenon_Vrq != zenon_Vqq)
% 13.94/14.28  (zenon_Vrq != zenon_Vlo)
% 13.94/14.28  (zenon_Vgq != zenon_Vgr)
% 13.94/14.28  (zenon_Viq != zenon_Vlq)
% 13.94/14.28  (zenon_Vjq != zenon_Vnq)
% 13.94/14.28  (p9 zenon_Vhq)
% 13.94/14.28  (p8 zenon_Vfq)
% 13.94/14.28  (-. (p109 zenon_Vvq))
% 13.94/14.28  (zenon_Voq != zenon_Vqq)
% 13.94/14.28  (-. (p106 Tau_2))
% 13.94/14.28  (-. (p100 zenon_Vlo))
% 13.94/14.28  (zenon_Vfq != zenon_Vtq)
% 13.94/14.28  (zenon_Vsq != zenon_Vvq)
% 13.94/14.28  (-. (p108 zenon_Vuf))
% 13.94/14.28  (-. (p107 zenon_Vuq))
% 13.94/14.28  (p101 zenon_Vmq)
% 13.94/14.28  (p106 zenon_Vcq)
% 13.94/14.28  (zenon_Veq != zenon_Vgq)
% 13.94/14.28  (p103 zenon_Voq)
% 13.94/14.28  (r1 zenon_Vrq zenon_Voq)
% 13.94/14.28  (p4 zenon_Viq)
% 13.94/14.28  (-. (p9 zenon_Vgq))
% 13.94/14.28  (-. (p101 zenon_Vum))
% 13.94/14.28  (zenon_Vtq != zenon_Vnr)
% 13.94/14.28  (zenon_Vhq != zenon_Vhr)
% 13.94/14.28  (p100 Tau_2)
% 13.94/14.28  (zenon_Vcq != zenon_Viq)
% 13.94/14.28  (zenon_Vdq != zenon_Vzq)
% 13.94/14.28  (-. (p110 zenon_Vlo))
% 13.94/14.28  (zenon_Vhq != zenon_Vlo)
% 13.94/14.28  (zenon_Vcq != zenon_Vfq)
% 13.94/14.28  (-. (p106 zenon_Vcl))
% 13.94/14.28  (zenon_Vdq != zenon_Vgr)
% 13.94/14.28  (zenon_Vqq != zenon_Vyd)
% 13.94/14.28  (-. (p111 zenon_Vph))
% 13.94/14.28  (zenon_Veq != zenon_Viq)
% 13.94/14.28  (zenon_Vgq != zenon_Vmq)
% 13.94/14.28  (zenon_Voq != zenon_Vlo)
% 13.94/14.28  (zenon_Vtq != zenon_Vbc)
% 13.94/14.28  (zenon_Vpq != zenon_Vsq)
% 13.94/14.28  (p3 zenon_Vkq)
% 13.94/14.28  (-. (p105 zenon_Vrq))
% 13.94/14.28  (p104 zenon_Vkq)
% 13.94/14.28  (p1 zenon_Vkq)
% 13.94/14.28  (zenon_Vjq != zenon_Vjj)
% 13.94/14.28  (-. (p105 zenon_Vtq))
% 13.94/14.28  (-. (p104 zenon_Vqq))
% 13.94/14.28  (p2 zenon_Vlq)
% 13.94/14.28  (zenon_Vgq != zenon_Vmr)
% 13.94/14.28  (p106 zenon_Vlq)
% 13.94/14.28  (p106 zenon_Vjq)
% 13.94/14.28  (zenon_Vlq != zenon_X3)
% 13.94/14.28  (-. (p105 zenon_Vuq))
% 13.94/14.28  (p104 zenon_Vhq)
% 13.94/14.28  (zenon_Vhq != zenon_Vjj)
% 13.94/14.28  (zenon_Viq != zenon_Vsq)
% 13.94/14.28  (-. (p101 zenon_Vda))
% 13.94/14.28  (zenon_Vuq != zenon_Vpr)
% 13.94/14.28  (-. (p111 zenon_Vcl))
% 13.94/14.28  (r1 zenon_Vjq zenon_Vgq)
% 13.94/14.28  (-. (p10 zenon_Veq))
% 13.94/14.28  (p2 zenon_Vrq)
% 13.94/14.28  (zenon_Vmq != zenon_Vyd)
% 13.94/14.28  (p10 zenon_Vfq)
% 13.94/14.28  (p101 zenon_Vdq)
% 13.94/14.28  (zenon_Viq != zenon_Vcl)
% 13.94/14.28  (zenon_Vhq != zenon_Vnr)
% 13.94/14.28  (zenon_Vdq != zenon_Vrq)
% 13.94/14.28  (-. (p102 zenon_Vbc))
% 13.94/14.28  (Tau_1 != zenon_X14)
% 13.94/14.28  (zenon_Vsq != zenon_Vum)
% 13.94/14.28  (zenon_Vsq != zenon_Vph)
% 13.94/14.28  (zenon_Vhq != zenon_Vrq)
% 13.94/14.28  (-. (p111 zenon_Vuf))
% 13.94/14.28  (zenon_Vjq != zenon_Vor)
% 13.94/14.28  (zenon_Vmq != zenon_Voq)
% 13.94/14.28  (zenon_Vmq != zenon_Vvq)
% 13.94/14.28  (zenon_Vdq != zenon_Vlr)
% 13.94/14.28  (zenon_Vkq != zenon_Vhr)
% 13.94/14.28  (zenon_Vjq != zenon_Vhr)
% 13.94/14.28  (zenon_Vjq != zenon_Vuf)
% 13.94/14.28  (zenon_Vkq != zenon_Vsq)
% 13.94/14.28  (p1 zenon_Vrq)
% 13.94/14.28  (r1 zenon_Vqq zenon_Voq)
% 13.94/14.28  (p101 zenon_Voq)
% 13.94/14.28  (zenon_Vdq != zenon_Vpq)
% 13.94/14.28  (zenon_Vmq != zenon_Vpr)
% 13.94/14.28  (zenon_Vmq != zenon_Vjj)
% 13.94/14.28  (-. (p106 zenon_Vbc))
% 13.94/14.28  (zenon_Vkq != zenon_Ver)
% 13.94/14.28  (zenon_Vcq != zenon_Vda)
% 13.94/14.28  (p3 zenon_Vmq)
% 13.94/14.28  (zenon_Vrq != zenon_Vtq)
% 13.94/14.28  (zenon_Vjq != zenon_Vuq)
% 13.94/14.28  (zenon_Vhq != zenon_Vsq)
% 13.94/14.28  (zenon_Vjq != zenon_Vlo)
% 13.94/14.28  (p8 zenon_Vhq)
% 13.94/14.28  (zenon_Vnq != zenon_Vjr)
% 13.94/14.28  (-. (p104 zenon_Vuf))
% 13.94/14.28  (zenon_Vpq != zenon_Vrq)
% 13.94/14.28  (-. (p110 zenon_Vph))
% 13.94/14.28  (-. (p100 zenon_Vuf))
% 13.94/14.28  (-. (p106 zenon_Vjj))
% 13.94/14.28  (p2 zenon_Vtq)
% 13.94/14.28  (p4 zenon_Vrq)
% 13.94/14.28  (p5 zenon_Vhq)
% 13.94/14.28  (zenon_Vcq != zenon_Vtq)
% 13.94/14.28  (zenon_Vmq != zenon_Vrq)
% 13.94/14.28  (zenon_Vsq != zenon_Vor)
% 13.94/14.28  (zenon_Vmq != zenon_Vmr)
% 13.94/14.28  (zenon_Viq != zenon_Vcr)
% 13.94/14.28  (p1 Tau_2)
% 13.94/14.28  (-. (p102 zenon_Vjj))
% 13.94/14.28  (zenon_Vkq != zenon_Vnr)
% 13.94/14.28  (p5 zenon_Vlq)
% 13.94/14.28  (zenon_Vcq != zenon_Vcr)
% 13.94/14.28  (-. (p107 zenon_Vqq))
% 13.94/14.28  (p102 zenon_Vrq)
% 13.94/14.28  (zenon_Vcq != zenon_Vpq)
% 13.94/14.28  (zenon_Vjq != zenon_Viq)
% 13.94/14.28  (zenon_Vnq != zenon_Vkr)
% 13.94/14.28  (-. (p110 zenon_Vfq))
% 13.94/14.28  (zenon_Vhq != zenon_Vjr)
% 13.94/14.28  (p3 zenon_Vjq)
% 13.94/14.28  (p7 zenon_Vhq)
% 13.94/14.28  (zenon_Vqq != zenon_Vlr)
% 13.94/14.28  (-. (p111 zenon_Vda))
% 13.94/14.28  (zenon_Vjq != zenon_Vpq)
% 13.94/14.28  (-. (p110 zenon_Vrq))
% 13.94/14.28  (-. (p105 zenon_Vvq))
% 13.94/14.28  (zenon_Vcq != zenon_Var)
% 13.94/14.28  (zenon_Vgq != zenon_Vkq)
% 13.94/14.28  (-. (p100 zenon_Vum))
% 13.94/14.28  (p2 zenon_Vfq)
% 13.94/14.28  (zenon_Vvq != zenon_Vor)
% 13.94/14.28  (zenon_Vcq != zenon_Vhr)
% 13.94/14.28  (zenon_Vlq != zenon_Vum)
% 13.94/14.28  (zenon_Vnq != zenon_Vtq)
% 13.94/14.28  (zenon_Vlq != zenon_Vuq)
% 13.94/14.28  (-. (p108 Tau_2))
% 13.94/14.28  (zenon_Vfq != zenon_Vbc)
% 13.94/14.28  (zenon_Viq != zenon_Vyd)
% 13.94/14.28  (-. (p111 Tau_0))
% 13.94/14.28  (p104 zenon_Vpq)
% 13.94/14.28  (zenon_Vkq != zenon_Vkr)
% 13.94/14.28  (zenon_Vnq != zenon_X14)
% 13.94/14.28  (zenon_Vkq != zenon_Vpq)
% 13.94/14.28  (p105 zenon_Vlq)
% 13.94/14.28  (p105 zenon_Vgq)
% 13.94/14.28  (p2 zenon_Viq)
% 13.94/14.28  (zenon_Vhq != zenon_X3)
% 13.94/14.28  (zenon_Viq != zenon_Vum)
% 13.94/14.28  (zenon_Vpq != zenon_Vjr)
% 13.94/14.28  (r1 zenon_Vvq zenon_Vtq)
% 13.94/14.28  (-. (p105 Tau_2))
% 13.94/14.28  (zenon_Vdq != zenon_Vum)
% 13.94/14.28  (zenon_Vfq != zenon_Vjr)
% 13.94/14.28  (Tau_1 != Tau_0)
% 13.94/14.28  (zenon_Vlq != zenon_Vmq)
% 13.94/14.28  (zenon_Vcq != zenon_Vjq)
% 13.94/14.28  (zenon_Vfq != zenon_Vsq)
% 13.94/14.28  (-. (p104 zenon_Vlo))
% 13.94/14.28  (zenon_Vjq != zenon_Vgr)
% 13.94/14.28  (zenon_Vcq != zenon_Vbr)
% 13.94/14.28  (-. (p107 Tau_2))
% 13.94/14.28  (p4 zenon_Vlq)
% 13.94/14.28  (zenon_Vrq != zenon_Vph)
% 13.94/14.28  (zenon_Vuq != zenon_Vum)
% 13.94/14.28  (zenon_Vfq != zenon_Vhq)
% 13.94/14.28  (p101 Tau_1)
% 13.94/14.28  (-. (p105 zenon_Vhr))
% 13.94/14.28  (zenon_Veq != zenon_Vlr)
% 13.94/14.28  (zenon_Vdq != zenon_Vph)
% 13.94/14.28  (-. (p111 zenon_Vuq))
% 13.94/14.28  (-. (p100 zenon_Vbc))
% 13.94/14.28  (-. (p104 zenon_Vph))
% 13.94/14.28  (zenon_Vqq != zenon_X14)
% 13.94/14.28  (zenon_Vuq != zenon_Vcl)
% 13.94/14.28  (zenon_Vdq != zenon_Vlo)
% 13.94/14.28  (zenon_Vmq != zenon_Vlr)
% 13.94/14.28  (zenon_Vlq != zenon_Vpr)
% 13.94/14.28  (-. (p101 zenon_Vor))
% 13.94/14.28  (zenon_Vlq != zenon_Vrr)
% 13.94/14.28  (zenon_Vgq != zenon_Vkr)
% 13.94/14.28  (zenon_Veq != zenon_Vgr)
% 13.94/14.28  (zenon_Viq != zenon_X14)
% 13.94/14.28  (p102 zenon_Veq)
% 13.94/14.28  (-. (p102 zenon_Vcl))
% 13.94/14.28  (zenon_Vlq != zenon_Vnq)
% 13.94/14.28  (-. (p106 zenon_Vfr))
% 13.94/14.28  (zenon_Vuq != zenon_X3)
% 13.94/14.28  (zenon_Vgq != zenon_Vtq)
% 13.94/14.28  (-. (p103 Tau_2))
% 13.94/14.28  (zenon_Viq != zenon_Vjr)
% 13.94/14.28  (-. (p104 zenon_Vcl))
% 13.94/14.28  (zenon_Vmq != zenon_X3)
% 13.94/14.28  (zenon_Vvq != Tau_1)
% 13.94/14.28  (zenon_Vsq != Tau_1)
% 13.94/14.28  (zenon_Vtq != Tau_1)
% 13.94/14.28  (zenon_Vqq != Tau_1)
% 13.94/14.28  (zenon_Vrq != Tau_1)
% 13.94/14.28  (zenon_Voq != Tau_1)
% 13.94/14.28  (zenon_Vpq != Tau_1)
% 13.94/14.28  (zenon_Vmq != Tau_1)
% 13.94/14.28  (zenon_Vnq != Tau_1)
% 13.94/14.28  (zenon_Vkq != Tau_1)
% 13.94/14.28  (zenon_Vlq != Tau_1)
% 13.94/14.28  (zenon_Viq != Tau_1)
% 13.94/14.28  (zenon_Vjq != Tau_1)
% 13.94/14.28  (zenon_Vgq != Tau_1)
% 13.94/14.28  (zenon_Vhq != Tau_1)
% 13.94/14.28  (zenon_Veq != Tau_1)
% 13.94/14.28  (zenon_Vfq != Tau_1)
% 13.94/14.28  (zenon_Vcq != Tau_1)
% 13.94/14.28  (zenon_Vdq != Tau_1)
% 13.94/14.28  (zenon_Vgq != zenon_Vph)
% 13.94/14.28  (zenon_Vkq != zenon_Vor)
% 13.94/14.28  (-. (p106 zenon_Vnq))
% 13.94/14.28  (r1 zenon_Vmq zenon_Vkq)
% 13.94/14.28  (zenon_Vgq != zenon_Vdr)
% 13.94/14.28  (zenon_Vpq != zenon_Vqq)
% 13.94/14.28  (zenon_Vcq != zenon_Vzq)
% 13.94/14.28  (zenon_Vqq != zenon_Vvq)
% 13.94/14.28  (zenon_Vlq != zenon_Ver)
% 13.94/14.28  (p7 zenon_Vcq)
% 13.94/14.28  (zenon_Vhq != zenon_Vuq)
% 13.94/14.28  (p8 zenon_Vcq)
% 13.94/14.28  (zenon_Vqq != zenon_Vsq)
% 13.94/14.28  (zenon_Vjq != zenon_X3)
% 13.94/14.28  (zenon_Vhq != zenon_Vkr)
% 13.94/14.28  (zenon_Vnq != zenon_Vlo)
% 13.94/14.28  (-. (p110 zenon_Vuf))
% 13.94/14.28  (zenon_Vjq != zenon_Vyd)
% 13.94/14.28  (zenon_Veq != zenon_Vum)
% 13.94/14.28  (-. (p110 zenon_Vxq))
% 13.94/14.28  (p109 zenon_Vfq)
% 13.94/14.28  (zenon_Vhq != zenon_Vfr)
% 13.94/14.28  (zenon_Veq != zenon_Vdr)
% 13.94/14.28  (-. (p105 zenon_Vqq))
% 13.94/14.28  (zenon_Vvq != zenon_Vrr)
% 13.94/14.28  (-. (p3 zenon_Vsq))
% 13.94/14.28  (zenon_Vhq != zenon_Vgr)
% 13.94/14.28  (r1 zenon_Vpq zenon_Vnq)
% 13.94/14.28  (zenon_Vrq != zenon_Vuq)
% 13.94/14.28  (zenon_Vgq != zenon_Vjj)
% 13.94/14.28  (zenon_Veq != zenon_Vhq)
% 13.94/14.28  (-. (p108 zenon_Vbr))
% 13.94/14.28  (p104 zenon_Vgq)
% 13.94/14.28  (zenon_Vcq != zenon_Vuq)
% 13.94/14.28  (p102 zenon_Vtq)
% 13.94/14.28  (p1 Tau_0)
% 13.94/14.28  (p103 zenon_Vrq)
% 13.94/14.28  (p1 zenon_Vtq)
% 13.94/14.28  (-. (p103 zenon_Vlr))
% 13.94/14.28  (zenon_Veq != zenon_Vjq)
% 13.94/14.28  (zenon_Voq != zenon_Vuf)
% 13.94/14.28  (-. (p109 zenon_Vnq))
% 13.94/14.28  (zenon_Vrq != zenon_Vvq)
% 13.94/14.28  (zenon_Vgq != zenon_Vcr)
% 13.94/14.28  (-. (p108 zenon_Vuq))
% 13.94/14.28  (zenon_Vdq != zenon_Vuf)
% 13.94/14.28  (r1 zenon_Vfq zenon_Vdq)
% 13.94/14.28  (zenon_Vkq != zenon_Vtq)
% 13.94/14.28  (-. (p108 zenon_Vmq))
% 13.94/14.28  (-. (p102 Tau_2))
% 13.94/14.28  (-. (p109 Tau_1))
% 13.94/14.28  (zenon_Veq != zenon_Voq)
% 13.94/14.28  (p102 zenon_Vsq)
% 13.94/14.28  (-. (p103 zenon_Vph))
% 13.94/14.28  *)
% 13.94/14.28  (* NO-PROOF *)
% 13.94/14.28  % SZS status GaveUp
% 13.94/14.28  Number of rewrites on terms: 0
% 13.94/14.28  Number of rewrites on props: 0
% 13.94/14.28  nodes searched: 9728
% 13.94/14.28  max branch formulas: 3429
% 13.94/14.28  proof nodes created: 1582
% 13.94/14.28  formulas created: 25311
% 13.94/14.28  
%------------------------------------------------------------------------------