↑ Up

ZenonModulo---0.5.0.UNK-Non.f

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

% Computer : n001.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:14 PM UTC 2026

% Result   : Unknown 3.24s 3.51s
% Output   : None 
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02  % Problem  : LCL645+1.010 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.02  % Command  : run_zenon_modulo %d %s
% 0.09/0.36  % Computer : n001.cluster.edu
% 0.09/0.36  % Model    : x86_64 x86_64
% 0.09/0.36  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36  % Memory   : 8046.5625MB
% 0.09/0.36  % OS       : Linux 6.8.0-71-generic
% 0.09/0.36  % CPULimit : 300
% 0.09/0.36  % WCLimit  : 300
% 0.14/0.36  % DateTime : Sat Sep  5 10:11:31 UTC 2026
% 0.14/0.37  % CPUTime  : 
% 3.24/3.51  Zenon error: exhausted search space without finding a proof
% 3.24/3.51  (* Current branch:
% 3.24/3.51  (zenon_Vpm != zenon_Vfm)
% 3.24/3.51  (zenon_X50 != zenon_Vbe)
% 3.24/3.51  (-. (p2 zenon_Vum))
% 3.24/3.51  (-. (p7 zenon_Vrk))
% 3.24/3.51  (-. (p10 zenon_Vnj))
% 3.24/3.51  (p34 zenon_Vza)
% 3.24/3.51  (p30 zenon_X60)
% 3.24/3.51  (zenon_X38 != zenon_Vlg)
% 3.24/3.51  (-. (p8 zenon_Vhk))
% 3.24/3.51  (zenon_Vum != zenon_Vkm)
% 3.24/3.51  (-. (p10 zenon_Vsj))
% 3.24/3.51  (zenon_Vuh != zenon_Vkh)
% 3.24/3.51  (r1 zenon_X26 zenon_Voi)
% 3.24/3.51  (p18 zenon_Vah)
% 3.24/3.51  (p36 zenon_Vka)
% 3.24/3.51  (zenon_Vrk != zenon_Vmk)
% 3.24/3.51  (p21 zenon_X42)
% 3.24/3.51  (-. (p18 zenon_Vqg))
% 3.24/3.51  (p34 zenon_Veb)
% 3.24/3.51  (zenon_Vhd != zenon_Vxc)
% 3.24/3.51  (-. (p30 zenon_Vic))
% 3.24/3.51  (zenon_Vzh != zenon_Vph)
% 3.24/3.51  (zenon_Vkh != zenon_Vah)
% 3.24/3.51  (-. (p9 zenon_Vxj))
% 3.24/3.51  (-. (p36 zenon_Vaa))
% 3.24/3.51  (zenon_X60 != zenon_Vic)
% 3.24/3.51  (-. (p22 zenon_Vkf))
% 3.24/3.51  (-. (p27 zenon_Vmd))
% 3.24/3.51  (zenon_Vpa != zenon_Vfa)
% 3.24/3.51  (zenon_X44 != zenon_Vkf)
% 3.24/3.51  (-. (p24 zenon_Vle))
% 3.24/3.51  (r1 zenon_X66 zenon_Vua)
% 3.24/3.51  (p15 zenon_X32)
% 3.24/3.51  (-. (p32 zenon_Vob))
% 3.24/3.51  (zenon_X64 != zenon_Vjb)
% 3.24/3.51  (p22 zenon_X44)
% 3.24/3.51  (zenon_Voi != zenon_Vei)
% 3.24/3.51  (p3 zenon_X8)
% 3.24/3.51  (-. (p30 zenon_Vdc))
% 3.24/3.51  (zenon_Vaf != zenon_Vqe)
% 3.24/3.51  (p14 zenon_Voi)
% 3.24/3.51  (p17 zenon_Vfh)
% 3.24/3.51  (-. (p25 zenon_Vge))
% 3.24/3.51  (-. (p28 zenon_Vcd))
% 3.24/3.51  (-. (p28 zenon_Vxc))
% 3.24/3.51  (zenon_X34 != zenon_Vfh)
% 3.24/3.51  (zenon_Vdc != zenon_Vtb)
% 3.24/3.51  (zenon_Vsc != zenon_Vdc)
% 3.24/3.51  (zenon_Vwd != zenon_Vmd)
% 3.24/3.51  (-. (p2 zenon_Vpm))
% 3.24/3.51  (-. (p19 zenon_Vgg))
% 3.24/3.51  (-. (p29 zenon_Vsc))
% 3.24/3.51  (zenon_X32 != zenon_Vph)
% 3.24/3.51  (r1 zenon_X70 zenon_Vaa)
% 3.24/3.51  (p13 zenon_Vti)
% 3.24/3.51  (p29 zenon_X58)
% 3.24/3.51  (zenon_Vpm != zenon_Vkm)
% 3.24/3.51  (zenon_Vsj != zenon_Vdj)
% 3.24/3.51  (p23 zenon_Vff)
% 3.24/3.51  (-. (p15 zenon_Vph))
% 3.24/3.51  (zenon_X38 != zenon_Vqg)
% 3.24/3.51  (zenon_X58 != zenon_Vsc)
% 3.24/3.51  (zenon_Vam != zenon_Vll)
% 3.24/3.51  (r1 zenon_X6 zenon_Vkm)
% 3.24/3.51  (zenon_Vxj != zenon_Vsj)
% 3.24/3.51  (zenon_Vxj != zenon_Vnj)
% 3.24/3.51  (-. (p26 zenon_Vrd))
% 3.24/3.51  (p4 zenon_X10)
% 3.24/3.51  (zenon_Vtb != zenon_Vob)
% 3.24/3.51  (-. (p22 zenon_Vff))
% 3.24/3.51  (zenon_Vpf != zenon_Vkf)
% 3.24/3.51  (zenon_Vza != zenon_Vpa)
% 3.24/3.51  (zenon_X36 != zenon_Vah)
% 3.24/3.51  (-. (p16 zenon_Vfh))
% 3.24/3.51  (p8 zenon_X18)
% 3.24/3.51  (r1 zenon_X10 zenon_Vql)
% 3.24/3.51  (zenon_Vph != zenon_Vkh)
% 3.24/3.51  (zenon_Vhd != zenon_Vcd)
% 3.24/3.51  (p29 zenon_Vcd)
% 3.24/3.51  (-. (p7 zenon_Vwk))
% 3.24/3.51  (p35 zenon_X70)
% 3.24/3.51  (p12 zenon_X26)
% 3.24/3.51  (zenon_Vtb != zenon_Vjb)
% 3.24/3.51  (zenon_Vrk != zenon_Vhk)
% 3.24/3.51  (p36 zenon_X72)
% 3.24/3.51  (-. (p36 zenon_Vv))
% 3.24/3.51  (p26 zenon_X52)
% 3.24/3.51  (zenon_Vuf != zenon_Vff)
% 3.24/3.51  (p19 zenon_Vlg)
% 3.24/3.51  (zenon_Vhk != zenon_Vxj)
% 3.24/3.51  (r1 zenon_X60 zenon_Vyb)
% 3.24/3.51  (p32 zenon_Vyb)
% 3.24/3.51  (zenon_Vqe != zenon_Vbe)
% 3.24/3.51  (zenon_Vam != zenon_Vql)
% 3.24/3.51  (p5 zenon_X12)
% 3.24/3.51  (zenon_X6 != zenon_Vpm)
% 3.24/3.51  (-. (p34 zenon_Vpa))
% 3.24/3.51  (zenon_X26 != zenon_Vti)
% 3.24/3.51  (zenon_Vuf != zenon_Vkf)
% 3.24/3.51  (-. (p32 zenon_Vjb))
% 3.24/3.51  (-. (p13 zenon_Vji))
% 3.24/3.51  (p13 zenon_Vyi)
% 3.24/3.51  (zenon_Vij != zenon_Vyi)
% 3.24/3.51  (-. (p11 zenon_Vdj))
% 3.24/3.51  (p10 zenon_Vxj)
% 3.24/3.51  (zenon_Vle != zenon_Vge)
% 3.24/3.51  (zenon_X70 != zenon_Vka)
% 3.24/3.51  (r1 zenon_X36 zenon_Vqg)
% 3.24/3.51  (p24 zenon_X48)
% 3.24/3.51  (zenon_X10 != zenon_Vvl)
% 3.24/3.51  (zenon_X42 != zenon_Vuf)
% 3.24/3.51  (-. (p4 zenon_Vvl))
% 3.24/3.51  (zenon_Vum != zenon_Vfm)
% 3.24/3.51  (p32 zenon_Vtb)
% 3.24/3.51  (zenon_X12 != zenon_Vql)
% 3.24/3.51  (zenon_X12 != zenon_Vll)
% 3.24/3.51  (zenon_X44 != zenon_Vff)
% 3.24/3.51  (p12 zenon_Vij)
% 3.24/3.51  (zenon_X46 != zenon_Vve)
% 3.24/3.51  (zenon_Vah != zenon_Vlg)
% 3.24/3.51  (zenon_Vka != zenon_Vv)
% 3.24/3.51  (p9 zenon_Vhk)
% 3.24/3.51  (zenon_X22 != zenon_Vsj)
% 3.24/3.51  (zenon_Vfm != zenon_Vam)
% 3.24/3.51  (zenon_X18 != zenon_Vmk)
% 3.24/3.51  (-. (p21 zenon_Vuf))
% 3.24/3.51  (p37 zenon_Vv)
% 3.24/3.51  (zenon_Vnj != zenon_Vij)
% 3.24/3.51  (zenon_X20 != zenon_Vck)
% 3.24/3.51  (p6 zenon_Vll)
% 3.24/3.51  (zenon_Vrd != zenon_Vmd)
% 3.24/3.51  (zenon_Vhk != zenon_Vck)
% 3.24/3.51  (p18 zenon_Vvg)
% 3.24/3.51  (zenon_Vfm != zenon_Vvl)
% 3.24/3.51  (zenon_Vff != zenon_Vve)
% 3.24/3.51  (-. (p31 zenon_Vyb))
% 3.24/3.51  (zenon_X30 != zenon_Vzh)
% 3.24/3.51  (p15 zenon_Vei)
% 3.24/3.51  (zenon_X50 != zenon_Vge)
% 3.24/3.51  (zenon_Vbl != zenon_Vrk)
% 3.24/3.51  (zenon_Vff != zenon_Vaf)
% 3.24/3.51  (p24 zenon_Vaf)
% 3.24/3.51  (zenon_X54 != zenon_Vmd)
% 3.24/3.51  (zenon_Vxc != zenon_Vsc)
% 3.24/3.51  (zenon_Vzh != zenon_Vuh)
% 3.24/3.51  (r1 zenon_X18 zenon_Vck)
% 3.24/3.51  (r1 zenon_X8 zenon_Vam)
% 3.24/3.51  (zenon_X48 != zenon_Vqe)
% 3.24/3.51  (-. (p35 zenon_Vka))
% 3.24/3.51  (zenon_X66 != zenon_Veb)
% 3.24/3.51  (-. (p21 zenon_Vpf))
% 3.24/3.51  (-. (p14 zenon_Vei))
% 3.24/3.51  (zenon_Vkh != zenon_Vvg)
% 3.24/3.51  (zenon_Vqe != zenon_Vge)
% 3.24/3.51  (zenon_Vck != zenon_Vnj)
% 3.24/3.51  (zenon_Veb != zenon_Vpa)
% 3.24/3.51  (zenon_Vij != zenon_Vti)
% 3.24/3.51  (zenon_X46 != zenon_Vaf)
% 3.24/3.51  (-. (p33 zenon_Veb))
% 3.24/3.51  (zenon_Vfa != zenon_Vv)
% 3.24/3.51  (p27 zenon_X54)
% 3.24/3.51  (zenon_X70 != zenon_Vfa)
% 3.24/3.51  (-. (p27 zenon_Vhd))
% 3.24/3.51  (p28 zenon_X56)
% 3.24/3.51  (p2 zenon_Vzm)
% 3.24/3.51  (zenon_Vmd != zenon_Vxc)
% 3.24/3.51  (zenon_X60 != zenon_Vdc)
% 3.24/3.51  (zenon_Vnj != zenon_Vdj)
% 3.24/3.51  (-. (p6 zenon_Vbl))
% 3.24/3.51  (r1 zenon_X38 zenon_Vgg)
% 3.24/3.51  (r1 zenon_X16 zenon_Vmk)
% 3.24/3.51  (zenon_Vnc != zenon_Vic)
% 3.24/3.51  (zenon_X18 != zenon_Vhk)
% 3.24/3.51  (p14 zenon_X30)
% 3.24/3.51  (-. (p37 zenon_Vq))
% 3.24/3.51  (zenon_Vzf != zenon_Vpf)
% 3.24/3.51  (zenon_Vwd != zenon_Vhd)
% 3.24/3.51  (r1 zenon_X68 zenon_Vka)
% 3.24/3.51  (r1 zenon_X62 zenon_Vob)
% 3.24/3.51  (p5 zenon_Vvl)
% 3.24/3.51  (zenon_Vmk != zenon_Vxj)
% 3.24/3.51  (zenon_X14 != zenon_Vgl)
% 3.24/3.51  (zenon_Vll != zenon_Vgl)
% 3.24/3.51  (zenon_Vll != zenon_Vbl)
% 3.24/3.51  (zenon_X42 != zenon_Vpf)
% 3.24/3.51  (r1 zenon_X44 zenon_Vaf)
% 3.24/3.51  (p16 zenon_Vph)
% 3.24/3.51  (zenon_X14 != zenon_Vbl)
% 3.24/3.51  (p31 zenon_Vdc)
% 3.24/3.51  (p23 zenon_Vkf)
% 3.24/3.51  (p32 zenon_X64)
% 3.24/3.51  (zenon_Vbe != zenon_Vwd)
% 3.24/3.51  (zenon_Vdj != zenon_Vti)
% 3.24/3.51  (zenon_X22 != zenon_Vnj)
% 3.24/3.51  (zenon_Vzm != zenon_Vum)
% 3.24/3.51  (zenon_Vph != zenon_Vfh)
% 3.24/3.51  (zenon_Vbe != zenon_Vrd)
% 3.24/3.51  (p18 zenon_X38)
% 3.24/3.51  (zenon_Voi != zenon_Vzh)
% 3.24/3.51  (zenon_Vyb != zenon_Vjb)
% 3.24/3.51  (zenon_X68 != zenon_Vpa)
% 3.24/3.51  (r1 zenon_X22 zenon_Vij)
% 3.24/3.51  (p30 zenon_Vsc)
% 3.24/3.51  (zenon_X40 != zenon_Vzf)
% 3.24/3.51  (zenon_Vti != zenon_Voi)
% 3.24/3.51  (zenon_Vsj != zenon_Vij)
% 3.24/3.51  (zenon_Vaa != zenon_Vq)
% 3.24/3.51  (p31 zenon_Vic)
% 3.24/3.51  (p35 zenon_Vua)
% 3.24/3.51  (p11 zenon_X24)
% 3.24/3.51  (-. (p33 zenon_Vza))
% 3.24/3.51  (-. (p3 zenon_Vkm))
% 3.24/3.51  (zenon_Vmd != zenon_Vcd)
% 3.24/3.51  (zenon_Vjb != zenon_Veb)
% 3.24/3.51  (zenon_X68 != zenon_Vua)
% 3.24/3.51  (zenon_Vgl != zenon_Vrk)
% 3.24/3.51  (-. (p18 zenon_Vlg))
% 3.24/3.51  (zenon_Vqg != zenon_Vgg)
% 3.24/3.51  (r1 zenon_X4 zenon_Vum)
% 3.24/3.51  (zenon_X8 != zenon_Vkm)
% 3.24/3.51  (r1 zenon_X50 zenon_Vwd)
% 3.24/3.51  (zenon_Vvl != zenon_Vql)
% 3.24/3.51  (zenon_Vge != zenon_Vrd)
% 3.24/3.51  (-. (p23 zenon_Vve))
% 3.24/3.51  (zenon_Vag != zenon_Vsj)
% 3.24/3.51  (p37 zenon_Vaa)
% 3.24/3.51  (zenon_Vwk != zenon_Vhk)
% 3.24/3.51  (p3 zenon_Vum)
% 3.24/3.51  (zenon_X54 != zenon_Vhd)
% 3.24/3.51  (p12 zenon_Vdj)
% 3.24/3.51  (zenon_Vdj != zenon_Vyi)
% 3.24/3.51  (-. (p15 zenon_Vuh))
% 3.24/3.51  (zenon_Vmk != zenon_Vck)
% 3.24/3.51  (zenon_Vei != zenon_Vuh)
% 3.24/3.51  (zenon_X62 != zenon_Vtb)
% 3.24/3.51  (p5 zenon_Vam)
% 3.24/3.51  (-. (p6 zenon_Vgl))
% 3.24/3.51  (zenon_X26 != zenon_Vyi)
% 3.24/3.51  (zenon_X10 != zenon_Vam)
% 3.24/3.51  (-. (p25 zenon_Vbe))
% 3.24/3.51  (p11 zenon_Vsj)
% 3.24/3.51  (-. (p9 zenon_Vck))
% 3.24/3.51  (p11 zenon_Vnj)
% 3.24/3.51  (-. (p13 zenon_Voi))
% 3.24/3.51  (p29 zenon_Vxc)
% 3.24/3.51  (zenon_Vyb != zenon_Vob)
% 3.24/3.51  (Tau_1 != zenon_Vdj)
% 3.24/3.51  (Tau_1 != zenon_Vij)
% 3.24/3.51  (p30 zenon_Vnc)
% 3.24/3.51  (p34 zenon_X68)
% 3.24/3.51  (p6 zenon_Vql)
% 3.24/3.51  (zenon_Vbg != zenon_Vnj)
% 3.24/3.51  (p22 zenon_Vuf)
% 3.24/3.51  (zenon_X56 != zenon_Vcd)
% 3.24/3.51  (p17 zenon_X36)
% 3.24/3.51  (-. (p5 zenon_Vll))
% 3.24/3.51  (zenon_Vrd != zenon_Vhd)
% 3.24/3.51  (-. (p35 zenon_Vfa))
% 3.24/3.51  (p1 zenon_X4)
% 3.24/3.51  (zenon_Vbg != zenon_Vsj)
% 3.24/3.51  (-. (p17 zenon_Vah))
% 3.24/3.51  (zenon_Vkf != zenon_Vve)
% 3.24/3.51  (zenon_Vpa != zenon_Vka)
% 3.24/3.51  (r1 zenon_X46 zenon_Vqe)
% 3.24/3.51  (zenon_X48 != zenon_Vle)
% 3.24/3.51  (p28 zenon_Vmd)
% 3.24/3.51  (zenon_Vji != zenon_Vzh)
% 3.24/3.51  (zenon_X8 != zenon_Vfm)
% 3.24/3.51  (p8 zenon_Vrk)
% 3.24/3.51  (zenon_Vji != zenon_Vei)
% 3.24/3.51  (p9 zenon_Vmk)
% 3.24/3.51  (p25 zenon_Vqe)
% 3.24/3.51  (zenon_X72 != zenon_Vv)
% 3.24/3.51  (p23 zenon_X46)
% 3.24/3.51  (zenon_Vei != zenon_Vph)
% 3.24/3.51  (p7 zenon_X16)
% 3.24/3.51  (p36 zenon_Vfa)
% 3.24/3.51  (-. (p10 Tau_1))
% 3.24/3.51  (-. (p10 Tau_2))
% 3.24/3.51  (zenon_X28 != zenon_Voi)
% 3.24/3.51  (zenon_X58 != zenon_Vnc)
% 3.24/3.51  (zenon_X52 != zenon_Vrd)
% 3.24/3.51  (p31 zenon_X62)
% 3.24/3.51  (r1 zenon_X40 zenon_Vuf)
% 3.24/3.51  (zenon_Vve != zenon_Vle)
% 3.24/3.51  (-. (p24 zenon_Vqe))
% 3.24/3.51  (p24 zenon_Vve)
% 3.24/3.51  (-. (p4 zenon_Vam))
% 3.24/3.51  (zenon_Vua != zenon_Vka)
% 3.24/3.51  (p33 zenon_Vob)
% 3.24/3.51  (zenon_Vge != zenon_Vwd)
% 3.24/3.51  (zenon_Vlg != zenon_Vgg)
% 3.24/3.51  (p11 Tau_2)
% 3.24/3.51  (p11 Tau_1)
% 3.24/3.51  (p35 zenon_Vpa)
% 3.24/3.51  (zenon_X24 != zenon_Vij)
% 3.24/3.51  (p4 zenon_Vfm)
% 3.24/3.51  (zenon_Vbg != Tau_2)
% 3.24/3.51  (zenon_Vbg != Tau_1)
% 3.24/3.51  (zenon_Vag != Tau_2)
% 3.24/3.51  (zenon_Vag != Tau_1)
% 3.24/3.51  (zenon_Vck != Tau_2)
% 3.24/3.51  (zenon_Vck != Tau_1)
% 3.24/3.51  (zenon_Vxj != Tau_2)
% 3.24/3.51  (zenon_Vxj != Tau_1)
% 3.24/3.51  (zenon_Vql != zenon_Vbl)
% 3.24/3.51  (p6 zenon_X14)
% 3.24/3.51  (p8 zenon_Vwk)
% 3.24/3.51  (r1 zenon_X14 zenon_Vwk)
% 3.24/3.51  (zenon_Vag != zenon_Vnj)
% 3.24/3.51  (r1 zenon_X30 zenon_Vuh)
% 3.24/3.51  (zenon_X30 != zenon_Vei)
% 3.24/3.51  (zenon_Vvg != zenon_Vlg)
% 3.24/3.51  (zenon_Vza != zenon_Vua)
% 3.24/3.51  (-. (p12 zenon_Vti))
% 3.24/3.51  (r1 zenon_X58 zenon_Vic)
% 3.24/3.51  (zenon_Vyi != zenon_Voi)
% 3.24/3.51  (zenon_Vve != zenon_Vqe)
% 3.24/3.51  (p16 zenon_Vuh)
% 3.24/3.51  (zenon_Vkf != zenon_Vaf)
% 3.24/3.51  (p10 zenon_Vag)
% 3.24/3.51  (p19 zenon_Vqg)
% 3.24/3.51  (-. (p3 zenon_Vfm))
% 3.24/3.51  (p15 zenon_Vzh)
% 3.24/3.51  (-. (p17 zenon_Vvg))
% 3.24/3.51  (zenon_Vql != zenon_Vgl)
% 3.24/3.51  (zenon_X56 != zenon_Vxc)
% 3.24/3.51  (zenon_X72 != zenon_Vaa)
% 3.24/3.51  (p10 zenon_Vbg)
% 3.24/3.51  (p10 zenon_Vck)
% 3.24/3.51  (r1 zenon_X20 zenon_Vsj)
% 3.24/3.51  (zenon_Vgl != zenon_Vwk)
% 3.24/3.51  (Tau_2 != zenon_Vdj)
% 3.24/3.51  (Tau_2 != zenon_Vij)
% 3.24/3.51  (zenon_Vwk != zenon_Vmk)
% 3.24/3.51  (zenon_Vjb != zenon_Vza)
% 3.24/3.51  (zenon_Vfh != zenon_Vvg)
% 3.24/3.51  (zenon_Vck != zenon_Vsj)
% 3.24/3.51  (zenon_Vcd != zenon_Vnc)
% 3.24/3.51  (zenon_X32 != zenon_Vuh)
% 3.24/3.51  (zenon_X4 != zenon_Vzm)
% 3.24/3.51  (p13 zenon_X28)
% 3.24/3.51  (p33 zenon_X66)
% 3.24/3.51  (p25 zenon_Vle)
% 3.24/3.51  (-. (p1 zenon_Vzm))
% 3.24/3.51  (zenon_Vfa != zenon_Vaa)
% 3.24/3.51  (p26 zenon_Vbe)
% 3.24/3.51  (r1 zenon_X56 zenon_Vsc)
% 3.24/3.51  (p7 zenon_Vgl)
% 3.24/3.51  (zenon_Vuh != zenon_Vfh)
% 3.24/3.51  (p9 zenon_X20)
% 3.24/3.51  (zenon_Vvg != zenon_Vqg)
% 3.24/3.51  (zenon_Vxc != zenon_Vnc)
% 3.24/3.51  (zenon_X22 != Tau_1)
% 3.24/3.51  (zenon_X22 != Tau_2)
% 3.24/3.51  (zenon_Vob != zenon_Veb)
% 3.24/3.51  (r1 zenon_X28 zenon_Vei)
% 3.24/3.51  (-. (p23 zenon_Vaf))
% 3.24/3.51  (zenon_Veb != zenon_Vua)
% 3.24/3.51  (r1 zenon_X52 zenon_Vmd)
% 3.24/3.51  (r1 Tau_0 Tau_1)
% 3.24/3.51  (r1 Tau_0 Tau_2)
% 3.24/3.51  (zenon_Vka != zenon_Vaa)
% 3.24/3.51  (zenon_X28 != zenon_Vji)
% 3.24/3.51  (zenon_Vsc != zenon_Vic)
% 3.24/3.51  (r1 zenon_X54 zenon_Vcd)
% 3.24/3.51  (zenon_Vnc != zenon_Vdc)
% 3.24/3.51  (p4 zenon_Vkm)
% 3.24/3.51  (r1 zenon_X12 zenon_Vgl)
% 3.24/3.51  (-. (p31 zenon_Vtb))
% 3.24/3.51  (zenon_X16 != zenon_Vwk)
% 3.24/3.51  (p28 zenon_Vhd)
% 3.24/3.51  (p16 zenon_X34)
% 3.24/3.51  (r1 zenon_X64 zenon_Veb)
% 3.24/3.51  (zenon_Vv != zenon_Vq)
% 3.24/3.51  (zenon_Vzm != zenon_Vpm)
% 3.24/3.51  (zenon_Vic != zenon_Vyb)
% 3.24/3.51  (-. (p16 zenon_Vkh))
% 3.24/3.51  (-. (p29 zenon_Vnc))
% 3.24/3.51  (p22 zenon_Vpf)
% 3.24/3.51  (zenon_Vkm != zenon_Vam)
% 3.24/3.51  (zenon_X24 != zenon_Vdj)
% 3.24/3.51  (zenon_Vkm != zenon_Vvl)
% 3.24/3.51  (zenon_Vcd != zenon_Vsc)
% 3.24/3.51  (-. (p20 zenon_Vzf))
% 3.24/3.51  (r1 zenon_X42 zenon_Vkf)
% 3.24/3.51  (p27 zenon_Vrd)
% 3.24/3.51  (p20 zenon_X40)
% 3.24/3.51  (zenon_X36 != zenon_Vvg)
% 3.24/3.51  (p17 zenon_Vkh)
% 3.24/3.51  (zenon_X16 != zenon_Vrk)
% 3.24/3.51  (-. (p26 zenon_Vwd))
% 3.24/3.51  (zenon_X62 != zenon_Vyb)
% 3.24/3.51  (p14 zenon_Vji)
% 3.24/3.51  (p3 zenon_Vpm)
% 3.24/3.51  (p26 zenon_Vge)
% 3.24/3.51  (r1 zenon_X34 zenon_Vah)
% 3.24/3.51  (r1 zenon_X48 zenon_Vge)
% 3.24/3.51  (-. (p34 zenon_Vua))
% 3.24/3.51  (zenon_Vyi != zenon_Vji)
% 3.24/3.51  (zenon_Vic != zenon_Vtb)
% 3.24/3.51  (p2 zenon_X6)
% 3.24/3.51  (p10 zenon_X22)
% 3.24/3.51  (p7 zenon_Vbl)
% 3.24/3.51  (p27 zenon_Vwd)
% 3.24/3.51  (r1 zenon_X24 zenon_Vyi)
% 3.24/3.51  (-. (p14 zenon_Vzh))
% 3.24/3.51  (p33 zenon_Vjb)
% 3.24/3.51  (zenon_Vti != zenon_Vji)
% 3.24/3.51  (zenon_Vle != zenon_Vbe)
% 3.24/3.51  (zenon_X66 != zenon_Vza)
% 3.24/3.51  (-. (p5 zenon_Vql))
% 3.24/3.51  (zenon_Vdc != zenon_Vyb)
% 3.24/3.51  (zenon_X20 != zenon_Vxj)
% 3.24/3.51  (zenon_Vzf != zenon_Vuf)
% 3.24/3.51  (zenon_Vah != zenon_Vqg)
% 3.24/3.51  (-. (p11 zenon_Vij))
% 3.24/3.51  (zenon_X34 != zenon_Vkh)
% 3.24/3.51  (zenon_Vpf != zenon_Vff)
% 3.24/3.51  (r1 zenon_X72 zenon_Vq)
% 3.24/3.51  (r1 zenon_X32 zenon_Vkh)
% 3.24/3.51  (zenon_Vvl != zenon_Vll)
% 3.24/3.51  (zenon_Vfh != zenon_Vah)
% 3.24/3.51  (zenon_X6 != zenon_Vum)
% 3.24/3.51  (-. (p8 zenon_Vmk))
% 3.24/3.51  (zenon_Vbl != zenon_Vwk)
% 3.24/3.51  (zenon_X52 != zenon_Vwd)
% 3.24/3.51  (p25 zenon_X50)
% 3.24/3.51  (zenon_Vaf != zenon_Vle)
% 3.24/3.51  (-. (p12 zenon_Vyi))
% 3.24/3.51  (zenon_X64 != zenon_Vob)
% 3.24/3.51  (zenon_Vua != zenon_Vfa)
% 3.24/3.51  (p21 zenon_Vzf)
% 3.24/3.51  (zenon_Vob != zenon_Vza)
% 3.24/3.51  *)
% 3.24/3.51  (* NO-PROOF *)
% 3.24/3.51  % SZS status GaveUp
% 3.24/3.51  Number of rewrites on terms: 0
% 3.24/3.51  Number of rewrites on props: 0
% 3.24/3.51  nodes searched: 1245
% 3.24/3.51  max branch formulas: 970
% 3.24/3.51  proof nodes created: 140
% 3.24/3.51  formulas created: 10903
% 3.24/3.51  
%------------------------------------------------------------------------------