↑ Up

ZenonModulo---0.5.0.UNK-Non.f

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

% Computer : n007.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:27 PM UTC 2026

% Result   : Unknown 0.76s 1.07s
% Output   : None 
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02  % Problem  : LCL681+1.010 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.02  % Command  : run_zenon_modulo %d %s
% 0.07/0.34  % Computer : n007.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.34  % DateTime : Fri Sep  4 22:37:24 UTC 2026
% 0.07/0.35  % CPUTime  : 
% 0.76/1.06  Zenon error: exhausted search space without finding a proof
% 0.76/1.06  (* Current branch:
% 0.76/1.06  (-. (p2 zenon_Vme))
% 0.76/1.06  (-. (p2 zenon_Vab))
% 0.76/1.06  (-. (p2 Tau_0))
% 0.76/1.06  (-. (p2 zenon_Vwn))
% 0.76/1.06  (-. (p2 zenon_Vwo))
% 0.76/1.06  (-. (p2 zenon_Vrb))
% 0.76/1.06  (-. (p2 zenon_Vlg))
% 0.76/1.06  (-. (p2 zenon_Vgg))
% 0.76/1.06  (-. (p2 zenon_Vag))
% 0.76/1.06  (-. (p2 zenon_Vlc))
% 0.76/1.06  (r1 zenon_Vul zenon_Vvl)
% 0.76/1.06  (-. (p2 zenon_Vei))
% 0.76/1.06  (-. (p2 zenon_Vln))
% 0.76/1.06  (-. (p2 zenon_Vil))
% 0.76/1.06  (r1 zenon_Vxh zenon_Vyh)
% 0.76/1.06  (-. (p2 zenon_Vnk))
% 0.76/1.06  (zenon_Vof != zenon_Vtq)
% 0.76/1.06  (-. (p2 zenon_Vib))
% 0.76/1.06  (-. (p2 zenon_Vid))
% 0.76/1.06  (-. (p2 zenon_Vfe))
% 0.76/1.06  (-. (p2 zenon_Vbn))
% 0.76/1.06  (-. (p2 zenon_Vle))
% 0.76/1.06  (p1 zenon_Vmm)
% 0.76/1.06  (-. (p2 zenon_Vlq))
% 0.76/1.06  (-. (p2 zenon_Vcg))
% 0.76/1.06  (-. (p2 zenon_Vdp))
% 0.76/1.06  (-. (p2 zenon_Vra))
% 0.76/1.06  (-. (p2 zenon_Vob))
% 0.76/1.06  (-. (p2 zenon_Vsi))
% 0.76/1.06  (-. (p2 zenon_Vec))
% 0.76/1.06  (p1 zenon_Vok)
% 0.76/1.06  (zenon_Vmm != zenon_Vtq)
% 0.76/1.06  (-. (p2 zenon_Vsp))
% 0.76/1.06  (-. (p2 zenon_Vq))
% 0.76/1.06  (-. (p2 zenon_Vek))
% 0.76/1.06  (-. (p2 zenon_Vcc))
% 0.76/1.06  (-. (p2 zenon_Vjg))
% 0.76/1.06  (-. (p2 zenon_Vzg))
% 0.76/1.06  (-. (p2 zenon_Vwh))
% 0.76/1.06  (-. (p2 zenon_Vlh))
% 0.76/1.06  (-. (p2 zenon_Vgl))
% 0.76/1.06  (-. (p2 zenon_Vnf))
% 0.76/1.06  (r1 zenon_Voh zenon_Vph)
% 0.76/1.06  (-. (p2 zenon_Vna))
% 0.76/1.06  (-. (p2 zenon_Vqq))
% 0.76/1.06  (r1 zenon_Vll zenon_Vml)
% 0.76/1.06  (zenon_Vgi != zenon_Vtq)
% 0.76/1.07  (-. (p2 zenon_Vuo))
% 0.76/1.07  (-. (p2 zenon_Vgk))
% 0.76/1.07  (-. (p2 zenon_Vkl))
% 0.76/1.07  (-. (p2 zenon_Vha))
% 0.76/1.07  (-. (p2 zenon_Vx))
% 0.76/1.07  (-. (p2 zenon_Vkn))
% 0.76/1.07  (-. (p2 zenon_Vre))
% 0.76/1.07  (zenon_Vep != zenon_Vtq)
% 0.76/1.07  (-. (p2 zenon_Vfb))
% 0.76/1.07  (-. (p2 zenon_Vno))
% 0.76/1.07  (-. (p2 zenon_X5))
% 0.76/1.07  (-. (p2 zenon_Vud))
% 0.76/1.07  (r1 zenon_Vzm zenon_Van)
% 0.76/1.07  (-. (p2 zenon_Vbg))
% 0.76/1.07  (-. (p2 zenon_Vch))
% 0.76/1.07  (-. (p2 zenon_Vw))
% 0.76/1.07  (-. (p2 zenon_Vn))
% 0.76/1.07  (-. (p2 zenon_Vbf))
% 0.76/1.07  (-. (p2 zenon_Vva))
% 0.76/1.07  (-. (p2 zenon_Vij))
% 0.76/1.07  (r1 zenon_Vvi zenon_Vwi)
% 0.76/1.07  (-. (p2 zenon_Vkk))
% 0.76/1.07  (-. (p2 zenon_Vua))
% 0.76/1.07  (-. (p2 zenon_Vte))
% 0.76/1.07  (-. (p2 zenon_Vye))
% 0.76/1.07  (-. (p2 zenon_Vfm))
% 0.76/1.07  (-. (p2 zenon_Voe))
% 0.76/1.07  (-. (p2 zenon_Vje))
% 0.76/1.07  (-. (p2 zenon_Vxo))
% 0.76/1.07  (-. (p2 zenon_Vja))
% 0.76/1.07  (-. (p2 zenon_Vpb))
% 0.76/1.07  (-. (p2 zenon_Vpj))
% 0.76/1.07  (-. (p2 zenon_Vde))
% 0.76/1.07  (r1 zenon_Vdm zenon_Vem)
% 0.76/1.07  (-. (p2 zenon_Vso))
% 0.76/1.07  (-. (p2 zenon_Vvg))
% 0.76/1.07  (-. (p2 zenon_Vyi))
% 0.76/1.07  (-. (p2 zenon_Veb))
% 0.76/1.07  (-. (p2 zenon_Voj))
% 0.76/1.07  (-. (p2 zenon_Vhb))
% 0.76/1.07  (-. (p2 zenon_Vbp))
% 0.76/1.07  (-. (p2 zenon_Vqn))
% 0.76/1.07  (-. (p2 zenon_Voo))
% 0.76/1.07  (-. (p2 zenon_Vla))
% 0.76/1.07  (r1 zenon_Veg zenon_Vfg)
% 0.76/1.07  (-. (p2 zenon_Vad))
% 0.76/1.07  (-. (p2 zenon_Vup))
% 0.76/1.07  (-. (p2 zenon_Vpa))
% 0.76/1.07  (-. (p2 zenon_Vze))
% 0.76/1.07  (-. (p2 zenon_Vhm))
% 0.76/1.07  (-. (p2 zenon_Vrh))
% 0.76/1.07  (-. (p2 zenon_Vgd))
% 0.76/1.07  (r1 zenon_Vdd zenon_Ved)
% 0.76/1.07  (-. (p2 zenon_Vwp))
% 0.76/1.07  (-. (p2 zenon_Vef))
% 0.76/1.07  (-. (p2 zenon_Vkg))
% 0.76/1.07  (-. (p2 zenon_Vbc))
% 0.76/1.07  (-. (p2 zenon_Vth))
% 0.76/1.07  (-. (p2 zenon_Vbi))
% 0.76/1.07  (-. (p2 zenon_Vdj))
% 0.76/1.07  (-. (p2 zenon_Vvl))
% 0.76/1.07  (-. (p2 zenon_Vnn))
% 0.76/1.07  (-. (p2 zenon_Vnh))
% 0.76/1.07  (-. (p2 zenon_Vik))
% 0.76/1.07  (-. (p2 zenon_Vih))
% 0.76/1.07  (-. (p2 zenon_Veh))
% 0.76/1.07  (-. (p2 zenon_Vgb))
% 0.76/1.07  (-. (p2 zenon_Vaf))
% 0.76/1.07  (-. (p2 zenon_Vyc))
% 0.76/1.07  (-. (p2 zenon_Vsa))
% 0.76/1.07  (-. (p2 zenon_Vtb))
% 0.76/1.07  (-. (p2 zenon_Vmb))
% 0.76/1.07  (p1 zenon_Vep)
% 0.76/1.07  (-. (p2 zenon_Vkh))
% 0.76/1.07  (-. (p2 zenon_Vbj))
% 0.76/1.07  (-. (p2 zenon_Vmg))
% 0.76/1.07  (r1 zenon_Vff zenon_Vgf)
% 0.76/1.07  (-. (p2 zenon_X6))
% 0.76/1.07  (-. (p2 zenon_Vzd))
% 0.76/1.07  (-. (p2 zenon_X7))
% 0.76/1.07  (-. (p2 zenon_Vbd))
% 0.76/1.07  (r1 zenon_Vmd zenon_Vnd)
% 0.76/1.07  (-. (p2 zenon_Vmq))
% 0.76/1.07  (-. (p2 zenon_Vxe))
% 0.76/1.07  (-. (p2 zenon_Vun))
% 0.76/1.07  (-. (p2 zenon_Vro))
% 0.76/1.07  (zenon_Vyp != zenon_Vtq)
% 0.76/1.07  (-. (p2 zenon_Vcd))
% 0.76/1.07  (-. (p2 zenon_Vsq))
% 0.76/1.07  (-. (p2 zenon_Vpo))
% 0.76/1.07  (r1 zenon_X1 zenon_Vkq)
% 0.76/1.07  (-. (p2 zenon_Vdb))
% 0.76/1.07  (-. (p2 zenon_Vv))
% 0.76/1.07  (-. (p2 zenon_Von))
% 0.76/1.07  (-. (p2 zenon_Vkf))
% 0.76/1.07  (-. (p2 zenon_Vug))
% 0.76/1.07  (-. (p2 zenon_Vuj))
% 0.76/1.07  (-. (p2 zenon_Vaa))
% 0.76/1.07  (-. (p2 zenon_Vld))
% 0.76/1.07  (-. (p2 zenon_Vzn))
% 0.76/1.07  (-. (p2 zenon_Vhd))
% 0.76/1.07  (-. (p2 zenon_Vxi))
% 0.76/1.07  (-. (p2 zenon_Vwl))
% 0.76/1.07  (-. (p2 zenon_Vtg))
% 0.76/1.07  (-. (p2 zenon_Vdi))
% 0.76/1.07  (-. (p2 zenon_Vfa))
% 0.76/1.07  (-. (p2 zenon_Vam))
% 0.76/1.07  (r1 zenon_Vej zenon_Vfj)
% 0.76/1.07  (r1 zenon_Vka zenon_Vla)
% 0.76/1.07  (-. (p2 zenon_Vap))
% 0.76/1.07  (-. (p2 zenon_Vml))
% 0.76/1.07  (r1 zenon_Vee zenon_Vfe)
% 0.76/1.07  (zenon_Vmc != zenon_Vtq)
% 0.76/1.07  (-. (p2 zenon_Vsb))
% 0.76/1.07  (-. (p2 zenon_Vo))
% 0.76/1.07  (-. (p2 zenon_Vrp))
% 0.76/1.07  (r1 zenon_Vcl zenon_Vdl)
% 0.76/1.07  (-. (p2 zenon_Vyg))
% 0.76/1.07  (-. (p2 zenon_Vcf))
% 0.76/1.07  (-. (p2 zenon_Vmf))
% 0.76/1.07  (r1 zenon_Vta zenon_Vua)
% 0.76/1.07  (-. (p2 zenon_Vtl))
% 0.76/1.07  (-. (p2 zenon_Vpq))
% 0.76/1.07  (-. (p2 zenon_Vyo))
% 0.76/1.07  (-. (p2 zenon_Vxp))
% 0.76/1.07  (-. (p2 zenon_Vfn))
% 0.76/1.07  (p1 zenon_Vmc)
% 0.76/1.07  (-. (p2 zenon_Vem))
% 0.76/1.07  (-. (p2 zenon_Vbb))
% 0.76/1.07  (-. (p2 zenon_Vjj))
% 0.76/1.07  (-. (p2 zenon_Vmn))
% 0.76/1.07  (-. (p2 zenon_Van))
% 0.76/1.07  (-. (p2 zenon_Ven))
% 0.76/1.07  (-. (p2 zenon_Vqe))
% 0.76/1.07  (p1 zenon_Vgi)
% 0.76/1.07  (r1 zenon_Vwj zenon_Vxj)
% 0.76/1.07  (r1 zenon_Vnj zenon_Voj)
% 0.76/1.07  (-. (p2 zenon_Vui))
% 0.76/1.07  (-. (p2 zenon_Vqg))
% 0.76/1.07  (-. (p2 zenon_Vwi))
% 0.76/1.07  (-. (p2 zenon_Vbk))
% 0.76/1.07  (-. (p2 zenon_Vzl))
% 0.76/1.07  (-. (p2 zenon_Vlj))
% 0.76/1.07  (-. (p2 zenon_Vue))
% 0.76/1.07  (-. (p2 zenon_Vdn))
% 0.76/1.07  (-. (p2 zenon_Vsl))
% 0.76/1.07  (-. (p2 zenon_Vvh))
% 0.76/1.07  (-. (p2 zenon_Vhl))
% 0.76/1.07  (-. (p2 zenon_Vpe))
% 0.76/1.07  (-. (p2 zenon_Vkq))
% 0.76/1.07  (-. (p2 zenon_Vyj))
% 0.76/1.07  (zenon_Vmc != Tau_0)
% 0.76/1.07  (zenon_Vof != Tau_0)
% 0.76/1.07  (zenon_Vgi != Tau_0)
% 0.76/1.07  (zenon_Vok != Tau_0)
% 0.76/1.07  (zenon_Vmm != Tau_0)
% 0.76/1.07  (zenon_Vao != Tau_0)
% 0.76/1.07  (zenon_Vep != Tau_0)
% 0.76/1.07  (zenon_Vyp != Tau_0)
% 0.76/1.07  (-. (p2 zenon_Vcn))
% 0.76/1.07  (-. (p2 zenon_Vkb))
% 0.76/1.07  (-. (p2 zenon_Vnq))
% 0.76/1.07  (r1 zenon_Vdc zenon_Vec)
% 0.76/1.07  (-. (p2 zenon_Vgj))
% 0.76/1.07  (-. (p2 zenon_Vyd))
% 0.76/1.07  (-. (p2 zenon_Vga))
% 0.76/1.07  (-. (p2 zenon_Vgm))
% 0.76/1.07  (-. (p2 zenon_Vol))
% 0.76/1.07  (-. (p2 zenon_Vzo))
% 0.76/1.07  (r1 zenon_Vne zenon_Voe)
% 0.76/1.07  (-. (p2 zenon_Vyn))
% 0.76/1.07  (-. (p2 zenon_Vrq))
% 0.76/1.07  (-. (p2 zenon_Vqa))
% 0.76/1.07  (-. (p2 zenon_Vve))
% 0.76/1.07  (-. (p2 zenon_Vza))
% 0.76/1.07  (-. (p2 zenon_Vkd))
% 0.76/1.07  (-. (p2 zenon_Vpd))
% 0.76/1.07  (-. (p2 zenon_Vym))
% 0.76/1.07  (r1 zenon_Vcb zenon_Vdb)
% 0.76/1.07  (-. (p2 zenon_Vke))
% 0.76/1.07  (-. (p2 zenon_Vjb))
% 0.76/1.07  (-. (p2 zenon_Vqj))
% 0.76/1.07  (-. (p2 zenon_Vjl))
% 0.76/1.07  (-. (p2 zenon_Vhe))
% 0.76/1.07  (-. (p2 zenon_X8))
% 0.76/1.07  (-. (p2 zenon_Vse))
% 0.76/1.07  (r1 zenon_Vba zenon_Vca)
% 0.76/1.07  (-. (p2 zenon_Vkc))
% 0.76/1.07  (-. (p2 zenon_Vtn))
% 0.76/1.07  (-. (p2 zenon_Vz))
% 0.76/1.07  (-. (p2 zenon_Vfl))
% 0.76/1.07  (-. (p2 zenon_Vtp))
% 0.76/1.07  (-. (p2 zenon_Vae))
% 0.76/1.07  (-. (p2 zenon_Vpl))
% 0.76/1.07  (r1 zenon_Vwe zenon_Vxe)
% 0.76/1.07  (-. (p2 zenon_Via))
% 0.76/1.07  (-. (p2 zenon_Vgc))
% 0.76/1.07  (-. (p2 zenon_Vtj))
% 0.76/1.07  (-. (p2 zenon_Vy))
% 0.76/1.07  (-. (p2 zenon_Vcj))
% 0.76/1.07  (-. (p2 zenon_Vjc))
% 0.76/1.07  (-. (p2 zenon_Vhk))
% 0.76/1.07  (-. (p2 zenon_Vbl))
% 0.76/1.07  (-. (p2 zenon_Vvb))
% 0.76/1.07  (p1 zenon_Vof)
% 0.76/1.07  (-. (p2 zenon_Vto))
% 0.76/1.07  (-. (p2 zenon_Vvn))
% 0.76/1.07  (-. (p2 zenon_Vca))
% 0.76/1.07  (-. (p2 zenon_Vic))
% 0.76/1.07  (p1 zenon_Vyp)
% 0.76/1.07  (-. (p2 zenon_Vce))
% 0.76/1.07  (-. (p2 zenon_Vai))
% 0.76/1.07  (-. (p2 zenon_Vjn))
% 0.76/1.07  (-. (p2 zenon_Vuh))
% 0.76/1.07  (-. (p2 zenon_Vrd))
% 0.76/1.07  (r1 zenon_Vng zenon_Vog)
% 0.76/1.07  (zenon_Vao != zenon_Vtq)
% 0.76/1.07  (-. (p2 zenon_Ved))
% 0.76/1.07  (-. (p2 zenon_Vfc))
% 0.76/1.07  (-. (p2 zenon_Vnl))
% 0.76/1.07  (-. (p2 zenon_Vif))
% 0.76/1.07  (-. (p2 zenon_Vig))
% 0.76/1.07  (-. (p2 zenon_Vrl))
% 0.76/1.07  (-. (p2 zenon_Vxl))
% 0.76/1.07  (-. (p2 zenon_Vsj))
% 0.76/1.07  (-. (p2 zenon_Vkm))
% 0.76/1.07  (-. (p2 zenon_Vge))
% 0.76/1.07  (-. (p2 zenon_Vvj))
% 0.76/1.07  (-. (p2 zenon_Vgf))
% 0.76/1.07  (-. (p2 zenon_Vkj))
% 0.76/1.07  (r1 zenon_Vfk zenon_Vgk)
% 0.76/1.07  (-. (p2 zenon_Vxa))
% 0.76/1.07  (-. (p2 zenon_Vac))
% 0.76/1.07  (r1 zenon_Vin zenon_Vjn)
% 0.76/1.07  (-. (p2 zenon_Vjf))
% 0.76/1.07  (-. (p2 zenon_Vhh))
% 0.76/1.07  (-. (p2 zenon_Vdf))
% 0.76/1.07  (-. (p2 zenon_Vdh))
% 0.76/1.07  (-. (p2 zenon_Vdl))
% 0.76/1.07  (-. (p2 zenon_Vtd))
% 0.76/1.07  (-. (p2 zenon_Vnd))
% 0.76/1.07  (-. (p2 zenon_Vmh))
% 0.76/1.07  (-. (p2 zenon_Vxb))
% 0.76/1.07  (-. (p2 zenon_Voa))
% 0.76/1.07  (-. (p2 zenon_Vvp))
% 0.76/1.07  (-. (p2 zenon_Vyb))
% 0.76/1.07  (-. (p2 zenon_Vzc))
% 0.76/1.07  (-. (p2 zenon_Vfg))
% 0.76/1.07  (-. (p2 zenon_Vu))
% 0.76/1.07  (-. (p2 zenon_Vql))
% 0.76/1.07  (-. (p2 zenon_Vp))
% 0.76/1.07  (-. (p2 zenon_Vgn))
% 0.76/1.07  (-. (p2 zenon_Vgh))
% 0.76/1.07  (-. (p2 zenon_Vzb))
% 0.76/1.07  (-. (p2 zenon_Vyh))
% 0.76/1.07  (-. (p2 zenon_Vaj))
% 0.76/1.07  (-. (p2 zenon_Vpg))
% 0.76/1.07  (-. (p2 zenon_Vck))
% 0.76/1.07  (p1 zenon_Vao)
% 0.76/1.07  (-. (p2 zenon_Vfi))
% 0.76/1.07  (r1 zenon_Vub zenon_Vvb)
% 0.76/1.07  (-. (p1 zenon_Vtq))
% 0.76/1.07  (-. (p2 zenon_Vhf))
% 0.76/1.07  (r1 zenon_Vs zenon_Vt)
% 0.76/1.07  (-. (p2 zenon_Vqd))
% 0.76/1.07  (-. (p2 zenon_Vjk))
% 0.76/1.07  (-. (p2 zenon_Vbe))
% 0.76/1.07  (-. (p2 zenon_Vak))
% 0.76/1.07  (-. (p2 zenon_Vea))
% 0.76/1.07  (-. (p2 zenon_Vzi))
% 0.76/1.07  (-. (p2 zenon_Vhc))
% 0.76/1.07  (-. (p2 zenon_Vda))
% 0.76/1.07  (-. (p2 zenon_Vya))
% 0.76/1.07  (-. (p2 zenon_Vsg))
% 0.76/1.07  (-. (p2 zenon_Vqo))
% 0.76/1.07  (-. (p2 zenon_Vcp))
% 0.76/1.07  (-. (p2 zenon_Voq))
% 0.76/1.07  (-. (p2 zenon_Vel))
% 0.76/1.07  (-. (p2 zenon_Vm))
% 0.76/1.07  (-. (p2 zenon_Vjm))
% 0.76/1.07  (-. (p1 Tau_0))
% 0.76/1.07  (-. (p2 zenon_Vah))
% 0.76/1.07  (-. (p2 zenon_Vsn))
% 0.76/1.07  (r1 zenon_Vvo zenon_Vwo)
% 0.76/1.07  (-. (p2 zenon_Vti))
% 0.76/1.07  (-. (p2 zenon_Vrg))
% 0.76/1.07  (-. (p2 zenon_Vxj))
% 0.76/1.07  (-. (p2 zenon_Vcm))
% 0.76/1.07  (-. (p2 zenon_Vod))
% 0.76/1.07  (r1 zenon_Vvd zenon_Vwd)
% 0.76/1.07  (-. (p2 zenon_X3))
% 0.76/1.07  (-. (p2 zenon_Vlm))
% 0.76/1.07  (-. (p2 zenon_X4))
% 0.76/1.07  (r1 zenon_Vfh zenon_Vgh)
% 0.76/1.07  (r1 zenon_Vwg zenon_Vxg)
% 0.76/1.07  (-. (p2 zenon_Vmk))
% 0.76/1.07  (-. (p2 zenon_Vlk))
% 0.76/1.07  (-. (p2 zenon_Vwd))
% 0.76/1.07  (-. (p2 zenon_Vqh))
% 0.76/1.07  (-. (p2 zenon_Vim))
% 0.76/1.07  (-. (p2 zenon_Vhn))
% 0.76/1.07  (-. (p2 zenon_Vbh))
% 0.76/1.07  (-. (p2 zenon_Vmj))
% 0.76/1.07  (-. (p2 zenon_Vwb))
% 0.76/1.07  (zenon_Vok != zenon_Vtq)
% 0.76/1.07  (-. (p2 zenon_Val))
% 0.76/1.07  (-. (p2 zenon_Vfd))
% 0.76/1.07  (r1 zenon_Vlb zenon_Vmb)
% 0.76/1.07  (-. (p2 zenon_Vph))
% 0.76/1.07  (-. (p2 zenon_Vqp))
% 0.76/1.07  (-. (p2 zenon_Vjd))
% 0.76/1.07  (r1 zenon_Vrn zenon_Vsn)
% 0.76/1.07  (-. (p2 zenon_Vyl))
% 0.76/1.07  (-. (p2 zenon_Vzj))
% 0.76/1.07  (-. (p2 zenon_Vxg))
% 0.76/1.07  (-. (p2 zenon_Vhj))
% 0.76/1.07  (-. (p2 zenon_Vog))
% 0.76/1.07  (-. (p2 zenon_Vhg))
% 0.76/1.07  (-. (p2 zenon_Vxd))
% 0.76/1.07  (-. (p2 zenon_Vr))
% 0.76/1.07  (-. (p2 zenon_Vjh))
% 0.76/1.07  (-. (p2 zenon_Vfj))
% 0.76/1.07  (-. (p2 zenon_Vpn))
% 0.76/1.07  (-. (p2 zenon_Vxn))
% 0.76/1.07  (-. (p2 zenon_Vrj))
% 0.76/1.07  (-. (p2 zenon_Vwa))
% 0.76/1.07  (-. (p2 zenon_Vsd))
% 0.76/1.07  (-. (p2 zenon_Vci))
% 0.76/1.07  (-. (p2 zenon_Vqb))
% 0.76/1.07  (-. (p2 zenon_X2))
% 0.76/1.07  (-. (p2 zenon_Vbm))
% 0.76/1.07  (-. (p2 zenon_Vt))
% 0.76/1.07  (-. (p2 zenon_Vnb))
% 0.76/1.07  (-. (p2 zenon_Vsh))
% 0.76/1.07  (r1 zenon_X9 zenon_Vqp)
% 0.76/1.07  (-. (p2 zenon_Vzh))
% 0.76/1.07  (-. (p2 zenon_Vie))
% 0.76/1.07  (-. (p2 zenon_Vdk))
% 0.76/1.07  (-. (p2 zenon_Vma))
% 0.76/1.07  (-. (p2 zenon_Vlf))
% 0.76/1.07  (-. (p2 zenon_Vdg))
% 0.76/1.07  (r1 zenon_Vmo zenon_Vno)
% 0.76/1.07  *)
% 0.76/1.07  (* NO-PROOF *)
% 0.76/1.07  % SZS status GaveUp
% 0.76/1.07  Number of rewrites on terms: 0
% 0.76/1.07  Number of rewrites on props: 0
% 0.76/1.07  nodes searched: 1341
% 0.76/1.07  max branch formulas: 1712
% 0.76/1.07  proof nodes created: 1
% 0.76/1.07  formulas created: 7133
% 0.76/1.07  
%------------------------------------------------------------------------------