↑ Up

ZenonModulo---0.5.0.UNK-Non.f

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

% Computer : n026.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:24 PM UTC 2026

% Result   : Unknown 1.54s 1.84s
% Output   : None 
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02  % Problem  : LCL673+1.005 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.02  % Command  : run_zenon_modulo %d %s
% 0.08/0.35  % Computer : n026.cluster.edu
% 0.08/0.35  % Model    : x86_64 x86_64
% 0.08/0.35  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35  % Memory   : 8046.5625MB
% 0.08/0.35  % OS       : Linux 6.8.0-71-generic
% 0.08/0.35  % CPULimit : 300
% 0.08/0.35  % WCLimit  : 300
% 0.08/0.35  % DateTime : Fri Sep  4 23:29:25 UTC 2026
% 0.08/0.35  % CPUTime  : 
% 1.54/1.83  Zenon error: exhausted search space without finding a proof
% 1.54/1.83  (* Current branch:
% 1.54/1.83  (zenon_Vhg != zenon_Vkk)
% 1.54/1.83  (zenon_Vra != zenon_Vzc)
% 1.54/1.83  (zenon_Vdi != zenon_Vhi)
% 1.54/1.83  (zenon_Vra != zenon_Vak)
% 1.54/1.83  (zenon_Vdi != zenon_Vhl)
% 1.54/1.83  (zenon_Vvb != zenon_Vei)
% 1.54/1.83  (-. (p2 zenon_Vof))
% 1.54/1.83  (-. (p1 zenon_Vgi))
% 1.54/1.83  (zenon_Vkc != zenon_Vfk)
% 1.54/1.83  (zenon_Vkc != zenon_Vjl)
% 1.54/1.83  (zenon_Vdi != zenon_Vrk)
% 1.54/1.83  (r1 zenon_X8 zenon_Vuk)
% 1.54/1.83  (zenon_Vtf != zenon_Vak)
% 1.54/1.83  (p1 zenon_Vra)
% 1.54/1.83  (zenon_Vth != zenon_Vvf)
% 1.54/1.83  (zenon_Vje != zenon_Vvf)
% 1.54/1.83  (zenon_Vje != zenon_Vck)
% 1.54/1.83  (zenon_Vje != zenon_Vfi)
% 1.54/1.83  (-. (p1 zenon_Vdk))
% 1.54/1.83  (zenon_Vxe != zenon_Vzj)
% 1.54/1.83  (zenon_Veb != zenon_Vmk)
% 1.54/1.83  (-. (p2 zenon_Vlc))
% 1.54/1.83  (zenon_Vuc != zenon_Vkk)
% 1.54/1.83  (r1 zenon_Vrf zenon_Vsf)
% 1.54/1.83  (r1 zenon_Vxh zenon_Vyh)
% 1.54/1.83  (zenon_Vsg != zenon_Vfi)
% 1.54/1.83  (zenon_Vvb != zenon_Vil)
% 1.54/1.83  (-. (p1 zenon_Vyc))
% 1.54/1.83  (zenon_Vjf != zenon_Vgi)
% 1.54/1.83  (zenon_Vel != zenon_Vei)
% 1.54/1.83  (zenon_Vtf != zenon_Vil)
% 1.54/1.83  (r1 zenon_Vyk zenon_Vhl)
% 1.54/1.83  (r1 Tau_5 zenon_Vuh)
% 1.54/1.83  (r1 Tau_5 zenon_Vvh)
% 1.54/1.83  (zenon_Vth != zenon_Vgi)
% 1.54/1.83  (zenon_Vzd != zenon_Vfi)
% 1.54/1.83  (zenon_Vld != zenon_Vjl)
% 1.54/1.83  (r1 zenon_Vsc zenon_Vvc)
% 1.54/1.83  (zenon_Vxe != zenon_Vwc)
% 1.54/1.83  (zenon_Vgk != zenon_Vvf)
% 1.54/1.83  (p1 zenon_Vkh)
% 1.54/1.83  (zenon_Vzg != zenon_Vgi)
% 1.54/1.83  (-. (p1 zenon_Vwc))
% 1.54/1.83  (p1 zenon_Vlk)
% 1.54/1.83  (zenon_Vel != zenon_Vgi)
% 1.54/1.83  (zenon_Voi != zenon_Vxc)
% 1.54/1.83  (zenon_Vzg != zenon_Vzj)
% 1.54/1.83  (zenon_Vij != zenon_Vfl)
% 1.54/1.83  (zenon_Vra != zenon_Vhi)
% 1.54/1.83  (zenon_Vld != zenon_Vvf)
% 1.54/1.83  (zenon_Vaj != zenon_Vyc)
% 1.54/1.83  (zenon_Vkh != zenon_Vak)
% 1.54/1.83  (zenon_Vij != zenon_Vil)
% 1.54/1.83  (zenon_Vkh != zenon_Vhl)
% 1.54/1.83  (zenon_Vlk != zenon_Vgl)
% 1.54/1.83  (zenon_Vkh != zenon_Vjl)
% 1.54/1.83  (zenon_Veb != zenon_Vwf)
% 1.54/1.83  (-. (p1 zenon_Vfl))
% 1.54/1.83  (zenon_Vxe != zenon_Vck)
% 1.54/1.83  (zenon_Vuc != zenon_Vmk)
% 1.54/1.83  (zenon_Vlk != zenon_Vrk)
% 1.54/1.83  (zenon_Voj != zenon_Vvf)
% 1.54/1.83  (zenon_Voi != zenon_Vyf)
% 1.54/1.83  (zenon_Vkh != zenon_Vvc)
% 1.54/1.83  (zenon_Vld != zenon_Vmk)
% 1.54/1.83  (zenon_Vtf != zenon_Vvc)
% 1.54/1.83  (zenon_Vvb != zenon_Vgl)
% 1.54/1.83  (p1 zenon_Vel)
% 1.54/1.83  (zenon_Voj != zenon_Vyf)
% 1.54/1.83  (zenon_Vdi != zenon_Vwf)
% 1.54/1.83  (r1 Tau_0 Tau_3)
% 1.54/1.83  (-. (p1 zenon_Vxf))
% 1.54/1.83  (zenon_Voi != zenon_Vjl)
% 1.54/1.83  (r1 Tau_2 zenon_Vlc)
% 1.54/1.83  (r1 Tau_2 zenon_Vmc)
% 1.54/1.83  (zenon_Vjf != zenon_Vyf)
% 1.54/1.83  (zenon_Vkc != zenon_Vwf)
% 1.54/1.83  (zenon_Vkh != zenon_Vil)
% 1.54/1.83  (r1 Tau_2 zenon_Vzc)
% 1.54/1.83  (zenon_Vsg != zenon_Vmk)
% 1.54/1.83  (zenon_Voj != zenon_Vck)
% 1.54/1.83  (zenon_Vkc != zenon_Vzc)
% 1.54/1.83  (zenon_Vaj != zenon_Vjl)
% 1.54/1.83  (-. (p2 zenon_Vwh))
% 1.54/1.83  (zenon_Vlk != zenon_Vgi)
% 1.54/1.83  (zenon_Vzd != zenon_Vck)
% 1.54/1.83  (zenon_Vtf != zenon_Vwc)
% 1.54/1.83  (zenon_Vij != zenon_Vgi)
% 1.54/1.83  (zenon_Vyj != zenon_Vii)
% 1.54/1.83  (zenon_Vdi != zenon_Vvc)
% 1.54/1.83  (zenon_Veb != zenon_Vfk)
% 1.54/1.83  (zenon_Vuc != zenon_Vhi)
% 1.54/1.83  (zenon_Vth != zenon_Vii)
% 1.54/1.83  (zenon_Vvb != zenon_Vfi)
% 1.54/1.83  (zenon_Vlk != zenon_Vmk)
% 1.54/1.83  (zenon_Vxe != zenon_Vei)
% 1.54/1.83  (zenon_Voi != zenon_Vei)
% 1.54/1.83  (zenon_Vzd != zenon_Vzj)
% 1.54/1.83  (zenon_Vaa != zenon_Vwf)
% 1.54/1.83  (zenon_Vth != zenon_Vfk)
% 1.54/1.83  (zenon_Vjf != zenon_Vhl)
% 1.54/1.83  (zenon_Vyj != zenon_Vxc)
% 1.54/1.83  (p1 zenon_Vld)
% 1.54/1.83  (zenon_Vij != zenon_Vwf)
% 1.54/1.83  (zenon_Vjf != zenon_Vzc)
% 1.54/1.83  (zenon_Vzg != zenon_Vxc)
% 1.54/1.83  (-. (p1 zenon_Vbk))
% 1.54/1.83  (zenon_Vsg != zenon_Vgi)
% 1.54/1.83  (zenon_Vhg != zenon_Vfl)
% 1.54/1.83  (r1 zenon_Vvh zenon_Vhi)
% 1.54/1.83  (zenon_Vsg != zenon_Vxf)
% 1.54/1.83  (zenon_Vzg != zenon_Vyc)
% 1.54/1.83  (zenon_Vxe != zenon_Vil)
% 1.54/1.83  (r1 zenon_Vcl zenon_Vfl)
% 1.54/1.83  (zenon_Vld != zenon_Vkk)
% 1.54/1.83  (zenon_Vij != zenon_Vdk)
% 1.54/1.83  (zenon_Voi != zenon_Vak)
% 1.54/1.83  (zenon_Vld != zenon_Vzj)
% 1.54/1.83  (r1 zenon_Vpf zenon_Vvf)
% 1.54/1.83  (zenon_Vzg != zenon_Vjl)
% 1.54/1.83  (zenon_Vzd != zenon_Vii)
% 1.54/1.83  (zenon_Vzg != zenon_Vdk)
% 1.54/1.83  (zenon_Vhg != zenon_Vgi)
% 1.54/1.83  (zenon_Vwi != zenon_Vck)
% 1.54/1.83  (zenon_Vel != zenon_Vvc)
% 1.54/1.83  (zenon_Vzg != zenon_Vck)
% 1.54/1.83  (zenon_Vld != zenon_Vwc)
% 1.54/1.83  (zenon_Vkh != zenon_Vhi)
% 1.54/1.83  (zenon_Vsg != zenon_Vrk)
% 1.54/1.83  (zenon_Vhg != zenon_Vfk)
% 1.54/1.83  (zenon_Vaa != zenon_Vgl)
% 1.54/1.83  (zenon_Voj != zenon_Vfk)
% 1.54/1.83  (zenon_Vaj != zenon_Vii)
% 1.54/1.83  (r1 zenon_Val zenon_Vgl)
% 1.54/1.83  (-. (p1 zenon_Vmk))
% 1.54/1.83  (zenon_Vje != zenon_Vgl)
% 1.54/1.83  (r1 zenon_Voc zenon_Vqc)
% 1.54/1.83  (zenon_Vjf != zenon_Vzj)
% 1.54/1.83  (zenon_Vuc != zenon_Vwc)
% 1.54/1.83  (-. (p1 zenon_Vvf))
% 1.54/1.83  (zenon_Vkh != zenon_Vvf)
% 1.54/1.83  (-. (p1 zenon_Vak))
% 1.54/1.83  (r1 zenon_X9 zenon_Vqk)
% 1.54/1.83  (zenon_Vwi != zenon_Vxf)
% 1.54/1.83  (zenon_Vth != zenon_Vil)
% 1.54/1.83  (p1 zenon_Vzd)
% 1.54/1.83  (zenon_Vzd != zenon_Vak)
% 1.54/1.83  (zenon_Vtf != zenon_Vei)
% 1.54/1.83  (zenon_Vij != zenon_Vii)
% 1.54/1.83  (zenon_Vaj != zenon_Vak)
% 1.54/1.83  (zenon_Veb != zenon_Vrk)
% 1.54/1.83  (zenon_Voj != zenon_Vzj)
% 1.54/1.83  (zenon_Vkc != zenon_Vmk)
% 1.54/1.83  (zenon_Vsg != zenon_Vwc)
% 1.54/1.83  (zenon_Vuc != zenon_Vvc)
% 1.54/1.83  (zenon_Vgk != zenon_Vzj)
% 1.54/1.83  (zenon_Vra != zenon_Vyf)
% 1.54/1.83  (zenon_Vkh != zenon_Vuf)
% 1.54/1.83  (-. (p1 zenon_Vxc))
% 1.54/1.83  (r1 zenon_Vlf zenon_Vmf)
% 1.54/1.83  (zenon_Vyj != zenon_Vzj)
% 1.54/1.83  (zenon_Vje != zenon_Vbk)
% 1.54/1.83  (zenon_Vel != zenon_Vdk)
% 1.54/1.83  (zenon_Voi != zenon_Vck)
% 1.54/1.83  (zenon_Voi != zenon_Vdk)
% 1.54/1.83  (zenon_Vel != zenon_Vzc)
% 1.54/1.83  (zenon_Veb != zenon_Vii)
% 1.54/1.83  (zenon_Vsg != zenon_Vgl)
% 1.54/1.84  (zenon_Vdi != zenon_Vfk)
% 1.54/1.84  (zenon_Vxe != zenon_Vjl)
% 1.54/1.84  (zenon_Vlk != zenon_Vyf)
% 1.54/1.84  (zenon_Vzg != zenon_Vei)
% 1.54/1.84  (zenon_Vra != zenon_Vyc)
% 1.54/1.84  (zenon_Vaa != zenon_Vrk)
% 1.54/1.84  (zenon_Vra != zenon_Vkk)
% 1.54/1.84  (zenon_Vel != zenon_Vil)
% 1.54/1.84  (r1 zenon_Vsj zenon_Vuj)
% 1.54/1.84  (zenon_Vvb != zenon_Vhl)
% 1.54/1.84  (zenon_Voi != zenon_Vvf)
% 1.54/1.84  (zenon_Veb != zenon_Vvf)
% 1.54/1.84  (zenon_Vaj != zenon_Vil)
% 1.54/1.84  (zenon_Vje != zenon_Vxc)
% 1.54/1.84  (r1 zenon_Vwj zenon_Vzj)
% 1.54/1.84  (zenon_Vld != zenon_Vck)
% 1.54/1.84  (zenon_Vkh != zenon_Vck)
% 1.54/1.84  (zenon_Vsg != zenon_Vzj)
% 1.54/1.84  (zenon_Veb != zenon_Vgi)
% 1.54/1.84  (zenon_Vdi != zenon_Vzc)
% 1.54/1.84  (zenon_Vxe != zenon_Vyc)
% 1.54/1.84  (zenon_Vth != zenon_Vwc)
% 1.54/1.84  (zenon_Vij != zenon_Vuf)
% 1.54/1.84  (zenon_Vxe != zenon_Vmk)
% 1.54/1.84  (-. (p2 zenon_Vpj))
% 1.54/1.84  (zenon_Voj != zenon_Vvc)
% 1.54/1.84  (zenon_Vgk != zenon_Vyc)
% 1.54/1.84  (zenon_Vkc != zenon_Vyf)
% 1.54/1.84  (zenon_Vje != zenon_Vgi)
% 1.54/1.84  (zenon_Voi != zenon_Vzj)
% 1.54/1.84  (zenon_Vld != zenon_Vhl)
% 1.54/1.84  (zenon_Vlk != zenon_Vfl)
% 1.54/1.84  (zenon_Vvb != zenon_Vzj)
% 1.54/1.84  (zenon_Vjf != zenon_Vjl)
% 1.54/1.84  (zenon_Vvb != zenon_Vvf)
% 1.54/1.84  (zenon_Vtf != zenon_Vvf)
% 1.54/1.84  (zenon_Vwi != zenon_Vei)
% 1.54/1.84  (zenon_Vsg != zenon_Vfk)
% 1.54/1.84  (zenon_Vyj != zenon_Vwf)
% 1.54/1.84  (zenon_Vth != zenon_Vzc)
% 1.54/1.84  (zenon_Vxe != zenon_Vuk)
% 1.54/1.84  (zenon_Vwi != zenon_Vkk)
% 1.54/1.84  (zenon_Vhg != zenon_Vmk)
% 1.54/1.84  (zenon_Vxe != zenon_Vwf)
% 1.54/1.84  (zenon_Vdi != zenon_Vck)
% 1.54/1.84  (zenon_Vzd != zenon_Vil)
% 1.54/1.84  (zenon_Vld != zenon_Vdk)
% 1.54/1.84  (zenon_Vzg != zenon_Vwc)
% 1.54/1.84  (zenon_Vlk != zenon_Vxc)
% 1.54/1.84  (zenon_Vxe != zenon_Vxf)
% 1.54/1.84  (zenon_Vld != zenon_Vzc)
% 1.54/1.84  (-. (p1 zenon_Vkk))
% 1.54/1.84  (zenon_Vhg != zenon_Vzj)
% 1.54/1.84  (zenon_Vvb != zenon_Vbk)
% 1.54/1.84  (zenon_Vgk != zenon_Vfk)
% 1.54/1.84  (zenon_Vkh != zenon_Vuk)
% 1.54/1.84  (p1 zenon_Vaj)
% 1.54/1.84  (zenon_Vwi != zenon_Vvc)
% 1.54/1.84  (zenon_Vkh != zenon_Vfk)
% 1.54/1.84  (zenon_Vkh != zenon_Vdk)
% 1.54/1.84  (zenon_Vjf != zenon_Vkk)
% 1.54/1.84  (zenon_Vsg != zenon_Vyc)
% 1.54/1.84  (zenon_Vvb != zenon_Vrk)
% 1.54/1.84  (r1 zenon_Voc zenon_Vpc)
% 1.54/1.84  (zenon_Vwi != zenon_Vvf)
% 1.54/1.84  (zenon_Vuc != zenon_Vhl)
% 1.54/1.84  (r1 zenon_Vlf zenon_Vnf)
% 1.54/1.84  (zenon_Vdi != zenon_Vzj)
% 1.54/1.84  (r1 zenon_Vqc zenon_Vrc)
% 1.54/1.84  (zenon_Vgk != zenon_Vwc)
% 1.54/1.84  (zenon_Vzg != zenon_Vzc)
% 1.54/1.84  (zenon_Vel != zenon_Vfl)
% 1.54/1.84  (zenon_Vld != zenon_Vrk)
% 1.54/1.84  (zenon_Veb != zenon_Vfi)
% 1.54/1.84  (zenon_Vhg != zenon_Vgl)
% 1.54/1.84  (zenon_Vxe != zenon_Vrk)
% 1.54/1.84  (zenon_Vld != zenon_Vak)
% 1.54/1.84  (zenon_Vkh != zenon_Vzj)
% 1.54/1.84  (zenon_Vjf != zenon_Vck)
% 1.54/1.84  (zenon_Vjf != zenon_Vak)
% 1.54/1.84  (zenon_Vzg != zenon_Vxf)
% 1.54/1.84  (zenon_Vzd != zenon_Vkk)
% 1.54/1.84  (zenon_Vsg != zenon_Vjl)
% 1.54/1.84  (zenon_Vzd != zenon_Vei)
% 1.54/1.84  (zenon_Vvb != zenon_Vdk)
% 1.54/1.84  (zenon_Vdi != zenon_Vbk)
% 1.54/1.84  (zenon_Vtf != zenon_Vuk)
% 1.54/1.84  (r1 zenon_Vpf zenon_Vqf)
% 1.54/1.84  (zenon_Vaa != zenon_Vii)
% 1.54/1.84  (p1 zenon_Veb)
% 1.54/1.84  (zenon_Vaj != zenon_Vrk)
% 1.54/1.84  (zenon_Vzd != zenon_Vxf)
% 1.54/1.84  (zenon_Vyj != zenon_Vkk)
% 1.54/1.84  (-. (p1 zenon_Vvc))
% 1.54/1.84  (zenon_Voi != zenon_Vil)
% 1.54/1.84  (zenon_Vkh != zenon_Vgl)
% 1.54/1.84  (zenon_Vzg != zenon_Vhl)
% 1.54/1.84  (zenon_Vvb != zenon_Vxf)
% 1.54/1.84  (zenon_Vyj != zenon_Vbk)
% 1.54/1.84  (zenon_Voj != zenon_Vwf)
% 1.54/1.84  (r1 Tau_7 zenon_Vvk)
% 1.54/1.84  (r1 Tau_7 zenon_Vwk)
% 1.54/1.84  (zenon_Vkh != zenon_Vgi)
% 1.54/1.84  (zenon_Vxe != zenon_Vfi)
% 1.54/1.84  (zenon_Veb != zenon_Vak)
% 1.54/1.84  (zenon_Vxe != zenon_Vgi)
% 1.54/1.84  (zenon_Vld != zenon_Vwf)
% 1.54/1.84  (p1 zenon_Vzg)
% 1.54/1.84  (zenon_Vjf != zenon_Vfi)
% 1.54/1.84  (r1 zenon_Vsc zenon_Vtc)
% 1.54/1.84  (zenon_Vtf != zenon_Vgi)
% 1.54/1.84  (zenon_Vld != zenon_Vil)
% 1.54/1.84  (zenon_Vyj != zenon_Vvf)
% 1.54/1.84  (zenon_Vdi != zenon_Vxc)
% 1.54/1.84  (-. (p2 zenon_Vzk))
% 1.54/1.84  (zenon_Vaj != zenon_Vdk)
% 1.54/1.84  (zenon_Vgk != zenon_Vii)
% 1.54/1.84  (zenon_Vhg != zenon_Vii)
% 1.54/1.84  (zenon_Vxe != zenon_Vhi)
% 1.54/1.84  (zenon_Vyj != zenon_Vfi)
% 1.54/1.84  (zenon_Voi != zenon_Vvc)
% 1.54/1.84  (-. (p1 zenon_Vuf))
% 1.54/1.84  (zenon_Vhg != zenon_Vyc)
% 1.54/1.84  (zenon_Vld != zenon_Vyf)
% 1.54/1.84  (zenon_Vkc != zenon_Vhl)
% 1.54/1.84  (zenon_Vdi != zenon_Vvf)
% 1.54/1.84  (zenon_Vel != zenon_Vfk)
% 1.54/1.84  (zenon_Voj != zenon_Vxf)
% 1.54/1.84  (zenon_Vxe != zenon_Vyf)
% 1.54/1.84  (zenon_Vkc != zenon_Vvf)
% 1.54/1.84  (zenon_Vth != zenon_Vjl)
% 1.54/1.84  (zenon_Vij != zenon_Vyf)
% 1.54/1.84  (zenon_Vje != zenon_Vdk)
% 1.54/1.84  (zenon_Voj != zenon_Vii)
% 1.54/1.84  (zenon_Vzd != zenon_Vyf)
% 1.54/1.84  (zenon_Vaj != zenon_Vhi)
% 1.54/1.84  (zenon_Vjf != zenon_Vbk)
% 1.54/1.84  (zenon_Vuc != zenon_Vyc)
% 1.54/1.84  (zenon_Vje != zenon_Vwc)
% 1.54/1.84  (zenon_Vaa != zenon_Vyc)
% 1.54/1.84  (-. (p1 zenon_Vzc))
% 1.54/1.84  (r1 zenon_Val zenon_Vbl)
% 1.54/1.84  (zenon_Vth != zenon_Vak)
% 1.54/1.84  (zenon_Vtf != zenon_Vxc)
% 1.54/1.84  (zenon_Vsg != zenon_Vvf)
% 1.54/1.84  (zenon_Veb != zenon_Vyf)
% 1.54/1.84  (zenon_Voi != zenon_Vhi)
% 1.54/1.84  (zenon_Vth != zenon_Vzj)
% 1.54/1.84  (zenon_Vgk != zenon_Vhi)
% 1.54/1.84  (zenon_Vth != zenon_Vck)
% 1.54/1.84  (r1 Tau_5 zenon_Vii)
% 1.54/1.84  (zenon_Vzg != zenon_Vmk)
% 1.54/1.84  (zenon_Vje != zenon_Vvc)
% 1.54/1.84  (-. (p1 zenon_Vck))
% 1.54/1.84  (zenon_Vkc != zenon_Vzj)
% 1.54/1.84  (zenon_Vel != zenon_Vhl)
% 1.54/1.84  (zenon_Vyj != zenon_Vjl)
% 1.54/1.84  (zenon_Vgk != zenon_Vei)
% 1.54/1.84  (zenon_Vyj != zenon_Vyf)
% 1.54/1.84  (zenon_Vdi != zenon_Vgi)
% 1.54/1.84  (zenon_Vuc != zenon_Vgl)
% 1.54/1.84  (zenon_Vzd != zenon_Vwc)
% 1.54/1.84  (zenon_Vkh != zenon_Vkk)
% 1.54/1.84  (zenon_Vhg != zenon_Vwc)
% 1.54/1.84  (zenon_Vzd != zenon_Vvc)
% 1.54/1.84  (r1 zenon_Vbi zenon_Vei)
% 1.54/1.84  (zenon_Voj != zenon_Vuf)
% 1.54/1.84  (zenon_Vaa != zenon_Vil)
% 1.54/1.84  (r1 zenon_Vwk zenon_Vxk)
% 1.54/1.84  (zenon_Vtf != zenon_Vuf)
% 1.54/1.84  (zenon_Vth != zenon_Vrk)
% 1.54/1.84  (-. (p2 zenon_Vkf))
% 1.54/1.84  (zenon_Vkc != zenon_Vkk)
% 1.54/1.84  (zenon_Vkc != zenon_Vak)
% 1.54/1.84  (zenon_Vtf != zenon_Vdk)
% 1.54/1.84  (zenon_Vhg != zenon_Vei)
% 1.54/1.84  (zenon_Vth != zenon_Vgl)
% 1.54/1.84  (zenon_Vra != zenon_Vck)
% 1.54/1.84  (r1 Tau_4 zenon_Vyf)
% 1.54/1.84  (zenon_Vaa != zenon_Vfk)
% 1.54/1.84  (zenon_Vaa != zenon_Vei)
% 1.54/1.84  (zenon_Vyj != zenon_Vfk)
% 1.54/1.84  (r1 Tau_6 zenon_Vpj)
% 1.54/1.84  (r1 Tau_6 zenon_Vqj)
% 1.54/1.84  (r1 zenon_X12 zenon_Vfk)
% 1.54/1.84  (zenon_Vaa != zenon_Vfl)
% 1.54/1.84  (zenon_Vaj != zenon_Vhl)
% 1.54/1.84  (zenon_Vdi != zenon_Vmk)
% 1.54/1.84  (zenon_Vxe != zenon_Vxc)
% 1.54/1.84  (r1 zenon_Vvh zenon_Vwh)
% 1.54/1.84  (zenon_Vsg != zenon_Vck)
% 1.54/1.84  (-. (p1 zenon_Vei))
% 1.54/1.84  (zenon_Vaa != zenon_Vmk)
% 1.54/1.84  (zenon_Vdi != zenon_Vkk)
% 1.54/1.84  (zenon_Vdi != zenon_Vuf)
% 1.54/1.84  (zenon_Vaa != zenon_Vjl)
% 1.54/1.84  (zenon_Vwi != zenon_Vbk)
% 1.54/1.84  (zenon_Vjf != zenon_Vvc)
% 1.54/1.84  (zenon_Vzg != zenon_Vwf)
% 1.54/1.84  (zenon_Vij != zenon_Vuk)
% 1.54/1.84  (zenon_Vhg != zenon_Vyf)
% 1.54/1.84  (zenon_Vra != zenon_Vei)
% 1.54/1.84  (zenon_Vel != zenon_Vgl)
% 1.54/1.84  (p1 zenon_Voj)
% 1.54/1.84  (zenon_Vzd != zenon_Vzc)
% 1.54/1.84  (r1 zenon_Vwk zenon_Vil)
% 1.54/1.84  (zenon_Vsg != zenon_Vak)
% 1.54/1.84  (zenon_Vtf != zenon_Vxf)
% 1.54/1.84  (r1 zenon_Vxh zenon_Vgi)
% 1.54/1.84  (zenon_Vwi != zenon_Vfl)
% 1.54/1.84  (zenon_Vuc != zenon_Vak)
% 1.54/1.84  (zenon_Voj != zenon_Vxc)
% 1.54/1.84  (zenon_Vxe != zenon_Vbk)
% 1.54/1.84  (zenon_Vaj != zenon_Vvc)
% 1.54/1.84  (zenon_Vtf != zenon_Vkk)
% 1.54/1.84  (zenon_Vzd != zenon_Vrk)
% 1.54/1.84  (zenon_Vvb != zenon_Vyc)
% 1.54/1.84  (p1 zenon_Vaa)
% 1.54/1.84  (zenon_Voj != zenon_Vgi)
% 1.54/1.84  (zenon_Vwi != zenon_Vii)
% 1.54/1.84  (zenon_Vwi != zenon_Vdk)
% 1.54/1.84  (zenon_Vuc != zenon_Vxf)
% 1.54/1.84  (zenon_Vth != zenon_Vmk)
% 1.54/1.84  (zenon_Vhg != zenon_Vuf)
% 1.54/1.84  (zenon_Veb != zenon_Vhl)
% 1.54/1.84  (zenon_Vgk != zenon_Vak)
% 1.54/1.84  (zenon_Vgk != zenon_Vvc)
% 1.54/1.84  (zenon_Vje != zenon_Vzj)
% 1.54/1.84  (zenon_Vra != zenon_Vhl)
% 1.54/1.84  (zenon_Voi != zenon_Vuf)
% 1.54/1.84  (zenon_Vxe != zenon_Vvf)
% 1.54/1.84  (zenon_Vzd != zenon_Vfk)
% 1.54/1.84  (zenon_Vwi != zenon_Vuf)
% 1.54/1.84  (zenon_Voi != zenon_Vfk)
% 1.54/1.84  (zenon_Vth != zenon_Vei)
% 1.54/1.84  (zenon_Vth != zenon_Vfi)
% 1.54/1.84  (zenon_Vjf != zenon_Vil)
% 1.54/1.84  (zenon_Vaa != zenon_Vkk)
% 1.54/1.84  (zenon_Vel != zenon_Vmk)
% 1.54/1.84  (zenon_Vyj != zenon_Vgi)
% 1.54/1.84  (zenon_Vjf != zenon_Vuk)
% 1.54/1.84  (r1 zenon_Vqj zenon_Vrj)
% 1.54/1.84  (-. (p1 zenon_Vgl))
% 1.54/1.84  (zenon_Vra != zenon_Vfl)
% 1.54/1.84  (zenon_Vkc != zenon_Vrk)
% 1.54/1.84  (r1 zenon_Vcl zenon_Vdl)
% 1.54/1.84  (zenon_Vuc != zenon_Vwf)
% 1.54/1.84  (zenon_Vaj != zenon_Vfl)
% 1.54/1.84  (zenon_Vjf != zenon_Vxf)
% 1.54/1.84  (zenon_Vxe != zenon_Vvc)
% 1.54/1.84  (zenon_Vlk != zenon_Vvf)
% 1.54/1.84  (zenon_Vzg != zenon_Vfk)
% 1.54/1.84  (-. (p2 zenon_Vmf))
% 1.54/1.84  (zenon_Vlk != zenon_Vii)
% 1.54/1.84  (zenon_Vel != zenon_Vck)
% 1.54/1.84  (zenon_Vkh != zenon_Vfi)
% 1.54/1.84  (zenon_Vdi != zenon_Vak)
% 1.54/1.84  (zenon_Vsg != zenon_Vxc)
% 1.54/1.84  (zenon_Voi != zenon_Vyc)
% 1.54/1.84  (zenon_Vaj != zenon_Vuf)
% 1.54/1.84  (p1 zenon_Vxe)
% 1.54/1.84  (zenon_Vwi != zenon_Vmk)
% 1.54/1.84  (zenon_Vra != zenon_Vuf)
% 1.54/1.84  (zenon_Vaa != zenon_Vyf)
% 1.54/1.84  (zenon_Vaj != zenon_Vei)
% 1.54/1.84  (zenon_Vgk != zenon_Vmk)
% 1.54/1.84  (zenon_Vxe != zenon_Vkk)
% 1.54/1.84  (zenon_Vel != zenon_Vxf)
% 1.54/1.84  (zenon_Vzd != zenon_Vdk)
% 1.54/1.84  (zenon_Vsg != zenon_Vuk)
% 1.54/1.84  (zenon_Vld != zenon_Vyc)
% 1.54/1.84  (zenon_Vxe != zenon_Vhl)
% 1.54/1.84  (zenon_Vld != zenon_Vii)
% 1.54/1.84  (r1 zenon_Vlf zenon_Vxf)
% 1.54/1.84  (-. (p1 zenon_Vfi))
% 1.54/1.84  (zenon_Vtf != zenon_Vzj)
% 1.54/1.84  (zenon_Vtf != zenon_Vii)
% 1.54/1.84  (r1 zenon_Vwj zenon_Vxj)
% 1.54/1.84  (p1 zenon_Vyj)
% 1.54/1.84  (zenon_Veb != zenon_Vck)
% 1.54/1.84  (zenon_Veb != zenon_Vbk)
% 1.54/1.84  (r1 zenon_Vmc zenon_Voc)
% 1.54/1.84  (-. (p2 zenon_Vxk))
% 1.54/1.84  (zenon_Vaa != zenon_Vgi)
% 1.54/1.84  (zenon_Vkc != zenon_Vvc)
% 1.54/1.84  (r1 Tau_4 zenon_Vkf)
% 1.54/1.84  (r1 Tau_4 zenon_Vlf)
% 1.54/1.84  (zenon_Vgk != zenon_Vxc)
% 1.54/1.84  (zenon_Vij != zenon_Vrk)
% 1.54/1.84  (zenon_Veb != zenon_Vxc)
% 1.54/1.84  (r1 zenon_X11 zenon_Vkk)
% 1.54/1.84  (zenon_Voi != zenon_Vkk)
% 1.54/1.84  (r1 zenon_Vsj zenon_Vbk)
% 1.54/1.84  (-. (p1 zenon_Vzj))
% 1.54/1.84  (zenon_Vaa != zenon_Vuk)
% 1.54/1.84  (zenon_Vij != zenon_Vvf)
% 1.54/1.84  (zenon_Vth != zenon_Vxf)
% 1.54/1.84  (zenon_Vkc != zenon_Vbk)
% 1.54/1.84  (zenon_Vvb != zenon_Vvc)
% 1.54/1.84  (zenon_Vtf != zenon_Vfl)
% 1.54/1.84  (p1 zenon_Vdi)
% 1.54/1.84  (zenon_Vld != zenon_Vvc)
% 1.54/1.84  (r1 zenon_Vrf zenon_Vuf)
% 1.54/1.84  (zenon_Vuc != zenon_Vei)
% 1.54/1.84  (zenon_Vwi != zenon_Vuk)
% 1.54/1.84  (zenon_Vvb != zenon_Vuk)
% 1.54/1.84  (zenon_Vyj != zenon_Vvc)
% 1.54/1.84  (zenon_Vra != zenon_Vjl)
% 1.54/1.84  (zenon_Vra != zenon_Vxc)
% 1.54/1.84  (r1 zenon_Voc zenon_Vxc)
% 1.54/1.84  (zenon_Vkh != zenon_Vwc)
% 1.54/1.84  (zenon_Veb != zenon_Vzj)
% 1.54/1.84  (zenon_Vgk != zenon_Vgi)
% 1.54/1.84  (zenon_Vld != zenon_Vfk)
% 1.54/1.84  (zenon_Vaj != zenon_Vwc)
% 1.54/1.84  (zenon_Vwi != zenon_Vhl)
% 1.54/1.84  (zenon_Vth != zenon_Vfl)
% 1.54/1.84  (zenon_Vra != zenon_Vil)
% 1.54/1.84  (zenon_Vjf != zenon_Vgl)
% 1.54/1.84  (zenon_Vwi != zenon_Vzj)
% 1.54/1.84  (zenon_Vra != zenon_Vwf)
% 1.54/1.84  (zenon_Vaa != zenon_Vxf)
% 1.54/1.84  (zenon_Voj != zenon_Vjl)
% 1.54/1.84  (zenon_Vkh != zenon_Vfl)
% 1.54/1.84  (zenon_Vgk != zenon_Vrk)
% 1.54/1.84  (zenon_Vgk != zenon_Vfl)
% 1.54/1.84  (zenon_Voj != zenon_Vzc)
% 1.54/1.84  (zenon_Vld != zenon_Vfi)
% 1.54/1.84  (zenon_Vsg != zenon_Vvc)
% 1.54/1.84  (p1 zenon_Vvb)
% 1.54/1.84  (zenon_Voj != zenon_Vbk)
% 1.54/1.84  (zenon_Voj != zenon_Vak)
% 1.54/1.84  (zenon_Vdi != zenon_Vfl)
% 1.54/1.84  (zenon_Vje != zenon_Vyc)
% 1.54/1.84  (zenon_Vzd != zenon_Vxc)
% 1.54/1.84  (zenon_Vld != zenon_Vuk)
% 1.54/1.84  (zenon_Vkc != zenon_Vei)
% 1.54/1.84  (r1 zenon_Vmc zenon_Vnc)
% 1.54/1.84  (zenon_Vvb != zenon_Vxc)
% 1.54/1.84  (zenon_Vth != zenon_Vyc)
% 1.54/1.84  (zenon_Vje != zenon_Vii)
% 1.54/1.84  (r1 zenon_Vzh zenon_Vai)
% 1.54/1.84  (r1 zenon_Vuj zenon_Vvj)
% 1.54/1.84  (zenon_Vvb != zenon_Vwc)
% 1.54/1.84  (r1 Tau_0 Tau_2)
% 1.54/1.84  (r1 Tau_0 Tau_4)
% 1.54/1.84  (r1 Tau_0 Tau_5)
% 1.54/1.84  (r1 Tau_0 Tau_6)
% 1.54/1.84  (r1 Tau_0 Tau_7)
% 1.54/1.84  (zenon_Vkh != zenon_Vmk)
% 1.54/1.84  (zenon_Vel != zenon_Vuf)
% 1.54/1.84  (zenon_Vsg != zenon_Vhl)
% 1.54/1.84  (zenon_Vlk != zenon_Vyc)
% 1.54/1.84  (zenon_Voi != zenon_Vxf)
% 1.54/1.84  (zenon_Vel != zenon_Vyf)
% 1.54/1.84  (zenon_Vdi != zenon_Vxf)
% 1.54/1.84  (zenon_Vij != zenon_Vkk)
% 1.54/1.84  (p1 zenon_Vgk)
% 1.54/1.84  (zenon_Vkc != zenon_Vuk)
% 1.54/1.84  (zenon_Vtf != zenon_Vhl)
% 1.54/1.84  (zenon_Vjf != zenon_Vmk)
% 1.54/1.84  (zenon_Vlk != zenon_Vxf)
% 1.54/1.84  (zenon_Veb != zenon_Vkk)
% 1.54/1.84  (zenon_Vij != zenon_Vvc)
% 1.54/1.84  (zenon_Vtf != zenon_Vyf)
% 1.54/1.84  (r1 zenon_Vsj zenon_Vtj)
% 1.54/1.84  (zenon_Vij != zenon_Vxc)
% 1.54/1.84  (zenon_Vxe != zenon_Vuf)
% 1.54/1.84  (zenon_Vuc != zenon_Vfl)
% 1.54/1.84  (zenon_Vje != zenon_Vil)
% 1.54/1.84  (p1 zenon_Vhg)
% 1.54/1.84  (zenon_Vjf != zenon_Vwf)
% 1.54/1.84  (zenon_Vtf != zenon_Vzc)
% 1.54/1.84  (zenon_Vkh != zenon_Vrk)
% 1.54/1.84  (zenon_Vxe != zenon_Vii)
% 1.54/1.84  (zenon_Vgk != zenon_Vkk)
% 1.54/1.84  (zenon_Vdi != zenon_Vyc)
% 1.54/1.84  (zenon_Vzg != zenon_Vkk)
% 1.54/1.84  (zenon_Vuc != zenon_Vgi)
% 1.54/1.84  (zenon_Vje != zenon_Vhl)
% 1.54/1.84  (zenon_Vkc != zenon_Vwc)
% 1.54/1.84  (zenon_Vaa != zenon_Vvc)
% 1.54/1.84  (zenon_Vaa != zenon_Vxc)
% 1.54/1.84  (zenon_Veb != zenon_Vfl)
% 1.54/1.84  (zenon_Vyj != zenon_Vil)
% 1.54/1.84  (zenon_Vaj != zenon_Vzc)
% 1.54/1.84  (zenon_Veb != zenon_Vuf)
% 1.54/1.84  (zenon_Vgk != zenon_Vzc)
% 1.54/1.84  (zenon_Vzg != zenon_Vuf)
% 1.54/1.84  (zenon_Vvb != zenon_Vck)
% 1.54/1.84  (zenon_Vyj != zenon_Vxf)
% 1.54/1.84  (zenon_Vsg != zenon_Vyf)
% 1.54/1.84  (zenon_Vuc != zenon_Vvf)
% 1.54/1.84  (zenon_Vth != zenon_Vhi)
% 1.54/1.84  (zenon_Veb != zenon_Vvc)
% 1.54/1.84  (zenon_Vzg != zenon_Vfi)
% 1.54/1.84  (zenon_Vhg != zenon_Vil)
% 1.54/1.84  (zenon_Vxe != zenon_Vdk)
% 1.54/1.84  (zenon_Veb != zenon_Vil)
% 1.54/1.84  (zenon_Vaa != zenon_Vbk)
% 1.54/1.84  (-. (p2 zenon_Vvk))
% 1.54/1.84  (zenon_Vra != zenon_Vbk)
% 1.54/1.84  (zenon_Vyj != zenon_Vfl)
% 1.54/1.84  (zenon_Vjf != zenon_Vyc)
% 1.54/1.84  (zenon_Vra != zenon_Vxf)
% 1.54/1.84  (-. (p1 zenon_Vrk))
% 1.54/1.84  (zenon_Vel != zenon_Vii)
% 1.54/1.84  (zenon_Vhg != zenon_Vuk)
% 1.54/1.84  (zenon_Vaj != zenon_Vvf)
% 1.54/1.84  (zenon_Vgk != zenon_Vck)
% 1.54/1.84  (zenon_Vuc != zenon_Vfk)
% 1.54/1.84  (zenon_Vlk != zenon_Vfk)
% 1.54/1.84  (zenon_Vel != zenon_Vyc)
% 1.54/1.84  (-. (p1 zenon_Vhl))
% 1.54/1.84  (zenon_Vhg != zenon_Vbk)
% 1.54/1.84  (zenon_Veb != zenon_Vjl)
% 1.54/1.84  (zenon_Vuc != zenon_Vdk)
% 1.54/1.84  (zenon_Vkc != zenon_Vuf)
% 1.54/1.84  (p1 zenon_Vjf)
% 1.54/1.84  (zenon_Vth != zenon_Vyf)
% 1.54/1.84  (zenon_Vvb != zenon_Vkk)
% 1.54/1.84  (zenon_Vel != zenon_Vzj)
% 1.54/1.84  (-. (p1 zenon_Vfk))
% 1.54/1.84  (zenon_Vwi != zenon_Vwc)
% 1.54/1.84  (zenon_Vje != zenon_Vfk)
% 1.54/1.84  (zenon_Vth != zenon_Vbk)
% 1.54/1.84  (zenon_Vld != zenon_Vhi)
% 1.54/1.84  (zenon_Vkc != zenon_Vfl)
% 1.54/1.84  (zenon_Vra != zenon_Vrk)
% 1.54/1.84  (-. (p1 zenon_Vii))
% 1.54/1.84  (zenon_Vwi != zenon_Vrk)
% 1.54/1.84  (zenon_Vjf != zenon_Vii)
% 1.54/1.84  (zenon_Vje != zenon_Vfl)
% 1.54/1.84  (r1 zenon_Vmc zenon_Vyc)
% 1.54/1.84  (zenon_Vgk != zenon_Vjl)
% 1.54/1.84  (zenon_Vgk != zenon_Vwf)
% 1.54/1.84  (zenon_Veb != zenon_Vei)
% 1.54/1.84  (zenon_Vld != zenon_Vei)
% 1.54/1.84  (zenon_Vaa != zenon_Vdk)
% 1.54/1.84  (zenon_Vuc != zenon_Vjl)
% 1.54/1.84  (p1 zenon_Vje)
% 1.54/1.84  (zenon_Vaa != zenon_Vzc)
% 1.54/1.84  (zenon_Vje != zenon_Vuk)
% 1.54/1.84  (zenon_Vyj != zenon_Vrk)
% 1.54/1.84  (zenon_Vdi != zenon_Vii)
% 1.54/1.84  (p1 zenon_Vij)
% 1.54/1.84  (zenon_Vje != zenon_Vmk)
% 1.54/1.84  (r1 Tau_7 zenon_Vjl)
% 1.54/1.84  (-. (p2 zenon_Vtj))
% 1.54/1.84  (zenon_Vlk != Tau_3)
% 1.54/1.84  (zenon_Vgk != Tau_3)
% 1.54/1.84  (zenon_Voj != Tau_3)
% 1.54/1.84  (zenon_Vij != Tau_3)
% 1.54/1.84  (zenon_Vaj != Tau_3)
% 1.54/1.84  (zenon_Vwi != Tau_3)
% 1.54/1.84  (zenon_Voi != Tau_3)
% 1.54/1.84  (zenon_Vth != Tau_3)
% 1.54/1.84  (zenon_Vkh != Tau_3)
% 1.54/1.84  (zenon_Vzg != Tau_3)
% 1.54/1.84  (zenon_Vsg != Tau_3)
% 1.54/1.84  (zenon_Vhg != Tau_3)
% 1.54/1.84  (zenon_Vjf != Tau_3)
% 1.54/1.84  (zenon_Vxe != Tau_3)
% 1.54/1.84  (zenon_Vje != Tau_3)
% 1.54/1.84  (zenon_Vzd != Tau_3)
% 1.54/1.84  (zenon_Vld != Tau_3)
% 1.54/1.84  (zenon_Vkc != Tau_3)
% 1.54/1.84  (zenon_Vvb != Tau_3)
% 1.54/1.84  (zenon_Veb != zenon_Vuk)
% 1.54/1.84  (zenon_Veb != Tau_3)
% 1.54/1.84  (zenon_Vra != Tau_3)
% 1.54/1.84  (zenon_Vaa != Tau_3)
% 1.54/1.84  (zenon_Vel != Tau_3)
% 1.54/1.84  (zenon_Vyj != Tau_3)
% 1.54/1.84  (zenon_Vdi != Tau_3)
% 1.54/1.84  (zenon_Vtf != Tau_3)
% 1.54/1.84  (zenon_Vuc != Tau_3)
% 1.54/1.84  (r1 zenon_Vxh zenon_Vzh)
% 1.54/1.84  (zenon_Vel != zenon_Vfi)
% 1.54/1.84  (-. (p2 zenon_Vpc))
% 1.54/1.84  (zenon_Vwi != zenon_Vwf)
% 1.54/1.84  (zenon_Vjf != zenon_Vuf)
% 1.54/1.84  (zenon_Vaj != zenon_Vxf)
% 1.54/1.84  (zenon_Vaj != zenon_Vkk)
% 1.54/1.84  (zenon_Vyj != zenon_Vzc)
% 1.54/1.84  (zenon_Vaj != zenon_Vmk)
% 1.54/1.84  (zenon_Vjf != zenon_Vfl)
% 1.54/1.84  (zenon_Vjf != zenon_Vdk)
% 1.54/1.84  (zenon_Vxe != zenon_Vfl)
% 1.54/1.84  (zenon_Vra != zenon_Vgi)
% 1.54/1.84  (zenon_Vra != zenon_Vwc)
% 1.54/1.84  (zenon_Vij != zenon_Vbk)
% 1.54/1.84  (zenon_Vje != zenon_Vei)
% 1.54/1.84  (-. (p2 zenon_Vbl))
% 1.54/1.84  (zenon_Vhg != zenon_Vzc)
% 1.54/1.84  (zenon_Vra != zenon_Vdk)
% 1.54/1.84  (zenon_Vra != zenon_Vvf)
% 1.54/1.84  (zenon_Voj != zenon_Vei)
% 1.54/1.84  (zenon_Vzd != zenon_Vjl)
% 1.54/1.84  (zenon_Vyj != zenon_Vmk)
% 1.54/1.84  (zenon_Vkh != zenon_Vxf)
% 1.54/1.84  (zenon_Vzd != zenon_Vmk)
% 1.54/1.84  (zenon_Vkc != zenon_Vil)
% 1.54/1.84  (r1 zenon_Vnf zenon_Vwf)
% 1.54/1.84  (zenon_Vlk != zenon_Vei)
% 1.54/1.84  (zenon_Vvb != zenon_Vmk)
% 1.54/1.84  (zenon_Vuc != zenon_Vzc)
% 1.54/1.84  (zenon_Vzd != zenon_Vhl)
% 1.54/1.84  (zenon_Vvb != zenon_Vak)
% 1.54/1.84  (r1 zenon_Vqj zenon_Vsj)
% 1.54/1.84  (zenon_Vsg != zenon_Vzc)
% 1.54/1.84  (zenon_Vkc != zenon_Vgi)
% 1.54/1.84  (zenon_Vij != zenon_Vmk)
% 1.54/1.84  (zenon_Vel != zenon_Vak)
% 1.54/1.84  (zenon_Vtf != zenon_Vjl)
% 1.54/1.84  (zenon_Vlk != zenon_Vck)
% 1.54/1.84  (zenon_Vaa != zenon_Vfi)
% 1.54/1.84  (-. (p2 zenon_Vai))
% 1.54/1.84  (zenon_Vlk != zenon_Vfi)
% 1.54/1.84  (zenon_Vje != zenon_Vkk)
% 1.54/1.84  (zenon_Vaj != zenon_Vbk)
% 1.54/1.84  (zenon_Veb != zenon_Vwc)
% 1.54/1.84  (zenon_Vth != zenon_Vkk)
% 1.54/1.84  (-. (p2 zenon_Vuh))
% 1.54/1.84  (zenon_Vje != zenon_Vrk)
% 1.54/1.84  (zenon_Vsg != zenon_Vuf)
% 1.54/1.84  (zenon_Vyj != zenon_Vei)
% 1.54/1.84  (zenon_Vyj != zenon_Vwc)
% 1.54/1.84  (zenon_Vuc != zenon_Vfi)
% 1.54/1.84  (-. (p2 Tau_1))
% 1.54/1.84  (zenon_Vwi != zenon_Vyc)
% 1.54/1.84  (zenon_Voj != zenon_Vfl)
% 1.54/1.84  (zenon_Vwi != zenon_Vak)
% 1.54/1.84  (zenon_Vra != zenon_Vii)
% 1.54/1.84  (zenon_Vij != zenon_Vwc)
% 1.54/1.84  (zenon_Vtf != zenon_Vbk)
% 1.54/1.84  (zenon_Vlk != zenon_Vjl)
% 1.54/1.84  (zenon_Vuc != zenon_Vil)
% 1.54/1.84  (zenon_Vzg != zenon_Vfl)
% 1.54/1.84  (-. (p1 Tau_3))
% 1.54/1.84  (zenon_Vlk != zenon_Vhl)
% 1.54/1.84  (zenon_Veb != zenon_Vyc)
% 1.54/1.84  (zenon_Vaj != zenon_Vgl)
% 1.54/1.84  (zenon_Voj != zenon_Vdk)
% 1.54/1.84  (zenon_Voi != zenon_Vgl)
% 1.54/1.84  (zenon_Vzg != zenon_Vhi)
% 1.54/1.84  (zenon_Vdi != zenon_Vuk)
% 1.54/1.84  (r1 zenon_Vyk zenon_Val)
% 1.54/1.84  (zenon_Vzg != zenon_Vak)
% 1.54/1.84  (zenon_Vaj != zenon_Vgi)
% 1.54/1.84  (zenon_Voj != zenon_Vil)
% 1.54/1.84  (zenon_Vzg != zenon_Vil)
% 1.54/1.84  (zenon_Vzd != zenon_Vbk)
% 1.54/1.84  (zenon_Vel != zenon_Vjl)
% 1.54/1.84  (zenon_Vje != zenon_Vwf)
% 1.54/1.84  (zenon_Vlk != zenon_Vwf)
% 1.54/1.84  (zenon_Vgk != zenon_Vhl)
% 1.54/1.84  (r1 zenon_Vnf zenon_Vof)
% 1.54/1.84  (zenon_Vwi != zenon_Vjl)
% 1.54/1.84  (-. (p2 zenon_Vvj))
% 1.54/1.84  (zenon_Vdi != zenon_Vei)
% 1.54/1.84  (zenon_Vkc != zenon_Vdk)
% 1.54/1.84  (zenon_Vvb != zenon_Vfl)
% 1.54/1.84  (r1 zenon_Vbi zenon_Vci)
% 1.54/1.84  (zenon_Vwi != zenon_Vfi)
% 1.54/1.84  (zenon_Vgk != zenon_Vbk)
% 1.54/1.84  (r1 zenon_Vuj zenon_Vak)
% 1.54/1.84  (zenon_Vvb != zenon_Vjl)
% 1.54/1.84  (r1 zenon_Vqc zenon_Vwc)
% 1.54/1.84  (zenon_Vlk != zenon_Vuf)
% 1.54/1.84  (-. (p1 zenon_Vuk))
% 1.54/1.84  (zenon_Voj != zenon_Vmk)
% 1.54/1.84  (zenon_Voi != zenon_Vgi)
% 1.54/1.84  (zenon_Vld != zenon_Vxf)
% 1.54/1.84  (zenon_Voi != zenon_Vii)
% 1.54/1.84  (zenon_Vlk != zenon_Vbk)
% 1.54/1.84  (zenon_Vhg != zenon_Vak)
% 1.54/1.84  (zenon_Vhg != zenon_Vck)
% 1.54/1.84  (zenon_Vij != zenon_Vzc)
% 1.54/1.84  (zenon_Voi != zenon_Vfi)
% 1.54/1.84  (zenon_Vje != zenon_Vyf)
% 1.54/1.84  (-. (p1 zenon_Vil))
% 1.54/1.84  (zenon_Vlk != zenon_Vhi)
% 1.54/1.84  (zenon_Veb != zenon_Vzc)
% 1.54/1.84  (zenon_Vyj != zenon_Vdk)
% 1.54/1.84  (zenon_Vuc != zenon_Vuf)
% 1.54/1.84  (zenon_Vij != zenon_Vfk)
% 1.54/1.84  (zenon_Veb != zenon_Vxf)
% 1.54/1.84  (zenon_Vlk != zenon_Vzj)
% 1.54/1.84  (zenon_Vtf != zenon_Vrk)
% 1.54/1.84  (zenon_Vld != zenon_Vbk)
% 1.54/1.84  (zenon_Voi != zenon_Vuk)
% 1.54/1.84  (zenon_Vhg != zenon_Vwf)
% 1.54/1.84  (zenon_Vdi != zenon_Vjl)
% 1.54/1.84  (zenon_Voi != zenon_Vwf)
% 1.54/1.84  (zenon_Vij != zenon_Vxf)
% 1.54/1.84  (zenon_Vvb != zenon_Vzc)
% 1.54/1.84  (zenon_Vij != zenon_Vhi)
% 1.54/1.84  (zenon_Vjf != zenon_Vei)
% 1.54/1.84  (zenon_Vld != zenon_Vgi)
% 1.54/1.84  (zenon_Vdi != zenon_Vfi)
% 1.54/1.84  (zenon_Vaa != zenon_Vuf)
% 1.54/1.84  (zenon_Vje != zenon_Vjl)
% 1.54/1.84  (zenon_Vel != zenon_Vkk)
% 1.54/1.84  (zenon_Vtf != zenon_Vmk)
% 1.54/1.84  (r1 zenon_Vwk zenon_Vyk)
% 1.54/1.84  (zenon_Vwi != zenon_Vyf)
% 1.54/1.84  (zenon_Vzd != zenon_Vvf)
% 1.54/1.84  (zenon_Vzg != zenon_Vii)
% 1.54/1.84  (zenon_Vje != zenon_Vuf)
% 1.54/1.84  (zenon_Vld != zenon_Vxc)
% 1.54/1.84  (zenon_Vlk != zenon_Vdk)
% 1.54/1.84  (r1 zenon_Vnf zenon_Vpf)
% 1.54/1.84  (zenon_Vld != zenon_Vgl)
% 1.54/1.84  (zenon_Voj != zenon_Vhi)
% 1.54/1.84  (zenon_Vkh != zenon_Vii)
% 1.54/1.84  (zenon_Vsg != zenon_Vwf)
% 1.54/1.84  (r1 Tau_6 zenon_Vdk)
% 1.54/1.84  (zenon_Vzd != zenon_Vuf)
% 1.54/1.84  (-. (p2 zenon_Vyh))
% 1.54/1.84  (zenon_Vje != zenon_Vzc)
% 1.54/1.84  (zenon_Vuc != zenon_Vii)
% 1.54/1.84  (zenon_Voj != zenon_Vrk)
% 1.54/1.84  (zenon_Vwi != zenon_Vzc)
% 1.54/1.84  (zenon_Vyj != zenon_Vuf)
% 1.54/1.84  (zenon_Vdi != zenon_Vgl)
% 1.54/1.84  (zenon_Vra != zenon_Vmk)
% 1.54/1.84  (zenon_Vgk != zenon_Vyf)
% 1.54/1.84  (zenon_Vhg != zenon_Vxc)
% 1.54/1.84  (r1 zenon_Vqc zenon_Vsc)
% 1.54/1.84  (zenon_Vkh != zenon_Vzc)
% 1.54/1.84  (zenon_Vyj != zenon_Vhl)
% 1.54/1.84  (zenon_Vkh != zenon_Vyc)
% 1.54/1.84  (zenon_Vyj != zenon_Vak)
% 1.54/1.84  (zenon_Vdi != zenon_Vil)
% 1.54/1.84  (zenon_Vlk != zenon_Vzc)
% 1.54/1.84  (zenon_Vlk != zenon_Vwc)
% 1.54/1.84  (zenon_Vra != zenon_Vfi)
% 1.54/1.84  (zenon_Vkc != zenon_Vxc)
% 1.54/1.84  (zenon_Vvb != zenon_Vuf)
% 1.54/1.84  (zenon_Vgk != zenon_Vil)
% 1.54/1.84  (zenon_Vhg != zenon_Vdk)
% 1.54/1.84  (zenon_Vvb != zenon_Vii)
% 1.54/1.84  (zenon_Vij != zenon_Vzj)
% 1.54/1.84  (p1 zenon_Vkc)
% 1.54/1.84  (zenon_Vyj != zenon_Vgl)
% 1.54/1.84  (r1 zenon_Vpf zenon_Vrf)
% 1.54/1.84  (zenon_Vhg != zenon_Vhi)
% 1.54/1.84  (zenon_Vzd != zenon_Vuk)
% 1.54/1.84  (zenon_Vld != zenon_Vuf)
% 1.54/1.84  (zenon_Voi != zenon_Vrk)
% 1.54/1.84  (zenon_Vyj != zenon_Vhi)
% 1.54/1.84  (zenon_Vlk != zenon_Vkk)
% 1.54/1.84  (zenon_Voj != zenon_Vgl)
% 1.54/1.84  (zenon_Vhg != zenon_Vrk)
% 1.54/1.84  (zenon_Vxe != zenon_Vgl)
% 1.54/1.84  (zenon_Vkc != zenon_Vii)
% 1.54/1.84  (zenon_Vyj != zenon_Vck)
% 1.54/1.84  (zenon_Vij != zenon_Vak)
% 1.54/1.84  (zenon_Vlk != zenon_Vuk)
% 1.54/1.84  (zenon_Vxe != zenon_Vak)
% 1.54/1.84  (-. (p1 zenon_Vhi))
% 1.54/1.84  (zenon_Vsg != zenon_Vei)
% 1.54/1.84  (zenon_Vwi != zenon_Vfk)
% 1.54/1.84  (zenon_Vsg != zenon_Vhi)
% 1.54/1.84  (zenon_Vuc != zenon_Vck)
% 1.54/1.84  (zenon_Vgk != zenon_Vuk)
% 1.54/1.84  (zenon_Vuc != zenon_Vyf)
% 1.54/1.84  (zenon_Vaj != zenon_Vck)
% 1.54/1.84  (zenon_Vhg != zenon_Vhl)
% 1.54/1.84  (zenon_Vtf != zenon_Vck)
% 1.54/1.84  (zenon_Vuc != zenon_Vuk)
% 1.54/1.84  (zenon_Vzd != zenon_Vgl)
% 1.54/1.84  (zenon_Voj != zenon_Vuk)
% 1.54/1.84  (zenon_Voj != zenon_Vfi)
% 1.54/1.84  (zenon_Vaa != zenon_Vzj)
% 1.54/1.84  (zenon_Vyj != zenon_Vyc)
% 1.54/1.84  (zenon_Vxe != zenon_Vfk)
% 1.54/1.84  (zenon_Vzd != zenon_Vgi)
% 1.54/1.84  (zenon_Vtf != zenon_Vhi)
% 1.54/1.84  (zenon_Vzd != zenon_Vfl)
% 1.54/1.84  (zenon_Vuc != zenon_Vbk)
% 1.54/1.84  (zenon_Vel != zenon_Vhi)
% 1.54/1.84  (-. (p1 zenon_Vyf))
% 1.54/1.84  (p1 zenon_Vwi)
% 1.54/1.84  (zenon_Vij != zenon_Vhl)
% 1.54/1.84  (zenon_Vra != zenon_Vzj)
% 1.54/1.84  (p1 zenon_Vtf)
% 1.54/1.84  (-. (p1 zenon_Vwf))
% 1.54/1.84  (zenon_Vth != zenon_Vdk)
% 1.54/1.84  (zenon_Vkc != zenon_Vhi)
% 1.54/1.84  (zenon_Vzg != zenon_Vyf)
% 1.54/1.84  (zenon_Vjf != zenon_Vvf)
% 1.54/1.84  (zenon_Vtf != zenon_Vyc)
% 1.54/1.84  (zenon_Vaa != zenon_Vak)
% 1.54/1.84  (r1 zenon_Vyk zenon_Vzk)
% 1.54/1.84  (zenon_Voj != zenon_Vkk)
% 1.54/1.84  (zenon_Vij != zenon_Vfi)
% 1.54/1.84  (zenon_Vtf != zenon_Vfi)
% 1.54/1.84  (r1 zenon_Val zenon_Vcl)
% 1.54/1.84  (zenon_Vth != zenon_Vhl)
% 1.54/1.84  (zenon_Vgk != zenon_Vgl)
% 1.54/1.84  (zenon_Vyj != zenon_Vuk)
% 1.54/1.84  (zenon_Vzg != zenon_Vuk)
% 1.54/1.84  (zenon_Vje != zenon_Vxf)
% 1.54/1.84  (zenon_Vij != zenon_Vei)
% 1.54/1.84  (zenon_Voj != zenon_Vwc)
% 1.54/1.84  (zenon_Vkc != zenon_Vck)
% 1.54/1.84  (zenon_Vxe != zenon_Vzc)
% 1.54/1.84  (zenon_Vvb != zenon_Vgi)
% 1.54/1.84  (zenon_Vel != zenon_Vwf)
% 1.54/1.84  (-. (p2 zenon_Vqf))
% 1.54/1.84  (zenon_Vlk != zenon_Vvc)
% 1.54/1.84  (zenon_Voi != zenon_Vmk)
% 1.54/1.84  (zenon_Vsg != zenon_Vii)
% 1.54/1.84  (zenon_Veb != zenon_Vgl)
% 1.54/1.84  (zenon_Vaa != zenon_Vvf)
% 1.54/1.84  (zenon_Vth != zenon_Vxc)
% 1.54/1.84  (zenon_Vkh != zenon_Vxc)
% 1.54/1.84  (zenon_Vje != zenon_Vhi)
% 1.54/1.84  (zenon_Vra != zenon_Vgl)
% 1.54/1.84  (r1 zenon_Vqj zenon_Vck)
% 1.54/1.84  (-. (p2 zenon_Vrc))
% 1.54/1.84  (zenon_Voi != zenon_Vbk)
% 1.54/1.84  (zenon_Vhg != zenon_Vxf)
% 1.54/1.84  (zenon_Vkc != zenon_Vgl)
% 1.54/1.84  (zenon_Vzd != zenon_Vwf)
% 1.54/1.84  (zenon_Vvb != zenon_Vyf)
% 1.54/1.84  (zenon_Vzg != zenon_Vvc)
% 1.54/1.84  (zenon_Vsg != zenon_Vdk)
% 1.54/1.84  (zenon_Vjf != zenon_Vwc)
% 1.54/1.84  (zenon_Vkc != zenon_Vfi)
% 1.54/1.84  (p1 zenon_Vuc)
% 1.54/1.84  (zenon_Vgk != zenon_Vfi)
% 1.54/1.84  (zenon_Vzd != zenon_Vyc)
% 1.54/1.84  (zenon_Vwi != zenon_Vgl)
% 1.54/1.84  (r1 zenon_Vvh zenon_Vxh)
% 1.54/1.84  (zenon_Vvb != zenon_Vfk)
% 1.54/1.84  (r1 zenon_Vzh zenon_Vfi)
% 1.54/1.84  (zenon_Vkc != zenon_Vxf)
% 1.54/1.84  (zenon_Vsg != zenon_Vil)
% 1.54/1.84  (zenon_Vdi != zenon_Vyf)
% 1.54/1.84  (zenon_Vzg != zenon_Vgl)
% 1.54/1.84  (zenon_Vwi != zenon_Vil)
% 1.54/1.84  (zenon_Vel != zenon_Vxc)
% 1.54/1.84  (zenon_Voi != zenon_Vwc)
% 1.54/1.84  (zenon_Vkh != zenon_Vbk)
% 1.54/1.84  (zenon_Vkh != zenon_Vyf)
% 1.54/1.84  (zenon_Vth != zenon_Vwf)
% 1.54/1.84  (zenon_Vkh != zenon_Vwf)
% 1.54/1.84  (zenon_Veb != zenon_Vhi)
% 1.54/1.84  (p1 zenon_Vth)
% 1.54/1.84  (zenon_Vaj != zenon_Vyf)
% 1.54/1.84  (zenon_Vaj != zenon_Vwf)
% 1.54/1.84  (zenon_Voi != zenon_Vhl)
% 1.54/1.84  (zenon_Vsg != zenon_Vfl)
% 1.54/1.84  (r1 zenon_Vzh zenon_Vbi)
% 1.54/1.84  (zenon_Vaa != zenon_Vhi)
% 1.54/1.84  (zenon_Vel != zenon_Vbk)
% 1.54/1.84  (zenon_Vsg != zenon_Vbk)
% 1.54/1.84  (zenon_Vel != zenon_Vrk)
% 1.54/1.84  (zenon_Vth != zenon_Vuf)
% 1.54/1.84  (zenon_Vaj != zenon_Vfk)
% 1.54/1.84  (zenon_Vhg != zenon_Vvf)
% 1.54/1.84  (p1 zenon_Vsg)
% 1.54/1.84  (zenon_Vij != zenon_Vyc)
% 1.54/1.84  (zenon_Vhg != zenon_Vvc)
% 1.54/1.84  (zenon_Voj != zenon_Vhl)
% 1.54/1.84  (zenon_Vlk != zenon_Vil)
% 1.54/1.84  (zenon_Vsg != zenon_Vkk)
% 1.54/1.84  (zenon_Vaa != zenon_Vck)
% 1.54/1.84  (zenon_Vel != zenon_Vvf)
% 1.54/1.84  (r1 zenon_X10 zenon_Vmk)
% 1.54/1.84  (-. (p2 zenon_Vnc))
% 1.54/1.84  (zenon_Vwi != zenon_Vhi)
% 1.54/1.84  (zenon_Vzg != zenon_Vvf)
% 1.54/1.84  (zenon_Vld != zenon_Vfl)
% 1.54/1.84  (zenon_Vel != zenon_Vuk)
% 1.54/1.84  (zenon_Vuc != zenon_Vzj)
% 1.54/1.84  (-. (p2 zenon_Vrj))
% 1.54/1.84  (zenon_Vzg != zenon_Vrk)
% 1.54/1.84  (p1 zenon_Voi)
% 1.54/1.84  (zenon_Vjf != zenon_Vfk)
% 1.54/1.84  (zenon_Vjf != zenon_Vxc)
% 1.54/1.84  (zenon_Vtf != zenon_Vgl)
% 1.54/1.84  (zenon_Vgk != zenon_Vxf)
% 1.54/1.84  (zenon_Vij != zenon_Vgl)
% 1.54/1.84  (-. (p1 zenon_Vjl))
% 1.54/1.84  (zenon_Vhg != zenon_Vfi)
% 1.54/1.84  (zenon_Vwi != zenon_Vgi)
% 1.54/1.84  (zenon_Voi != zenon_Vfl)
% 1.54/1.84  (zenon_Vaj != zenon_Vuk)
% 1.54/1.84  (r1 zenon_Vuj zenon_Vwj)
% 1.54/1.84  (zenon_Vth != zenon_Vvc)
% 1.54/1.84  (zenon_Vgk != zenon_Vuf)
% 1.54/1.84  (zenon_Voj != zenon_Vyc)
% 1.54/1.84  (zenon_Vaa != zenon_Vwc)
% 1.54/1.84  (zenon_Vel != zenon_Vwc)
% 1.54/1.84  (zenon_Vtf != zenon_Vwf)
% 1.54/1.84  (zenon_Vvb != zenon_Vhi)
% 1.54/1.84  (zenon_Veb != zenon_Vdk)
% 1.54/1.84  (zenon_Vzg != zenon_Vbk)
% 1.54/1.84  (zenon_Vjf != zenon_Vrk)
% 1.54/1.84  (zenon_Vlk != zenon_Vak)
% 1.54/1.84  (zenon_Vth != zenon_Vuk)
% 1.54/1.84  (zenon_Vij != zenon_Vck)
% 1.54/1.84  (r1 Tau_0 Tau_1)
% 1.54/1.84  (zenon_Vhg != zenon_Vjl)
% 1.54/1.84  (zenon_Vje != zenon_Vak)
% 1.54/1.84  (zenon_Vzd != zenon_Vhi)
% 1.54/1.84  (zenon_Voi != zenon_Vzc)
% 1.54/1.84  (zenon_Vkc != zenon_Vyc)
% 1.54/1.84  (zenon_Vaj != zenon_Vfi)
% 1.54/1.84  (zenon_Vaj != zenon_Vxc)
% 1.54/1.84  (zenon_Vra != zenon_Vuk)
% 1.54/1.84  (zenon_Vdi != zenon_Vdk)
% 1.54/1.84  (zenon_Vaa != zenon_Vhl)
% 1.54/1.84  (zenon_Vuc != zenon_Vrk)
% 1.54/1.84  (zenon_Vuc != zenon_Vxc)
% 1.54/1.84  (zenon_Vkh != zenon_Vei)
% 1.54/1.84  (zenon_Vij != zenon_Vjl)
% 1.54/1.84  (zenon_Vra != zenon_Vfk)
% 1.54/1.84  (zenon_Vgk != zenon_Vdk)
% 1.54/1.84  (zenon_Vtf != zenon_Vfk)
% 1.54/1.84  (zenon_Vdi != zenon_Vwc)
% 1.54/1.84  (zenon_Vjf != zenon_Vhi)
% 1.54/1.84  (zenon_Vwi != zenon_Vxc)
% 1.54/1.84  (zenon_Vra != zenon_Vvc)
% 1.54/1.84  (zenon_Vaj != zenon_Vzj)
% 1.54/1.84  (zenon_Vvb != zenon_Vwf)
% 1.54/1.84  *)
% 1.54/1.84  (* NO-PROOF *)
% 1.54/1.84  % SZS status GaveUp
% 1.54/1.84  Number of rewrites on terms: 0
% 1.54/1.84  Number of rewrites on props: 0
% 1.54/1.84  nodes searched: 1247
% 1.54/1.84  max branch formulas: 1357
% 1.54/1.84  proof nodes created: 50
% 1.54/1.84  formulas created: 8765
% 1.54/1.84  
%------------------------------------------------------------------------------