↑ Up

ZenonModulo---0.5.0.UNK-Non.f

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

% Computer : n018.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:16 PM UTC 2026

% Result   : Unknown 0.64s 1.01s
% Output   : None 
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : LCL650+1.010 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03  % Command  : run_zenon_modulo %d %s
% 0.10/0.36  % Computer : n018.cluster.edu
% 0.10/0.36  % Model    : x86_64 x86_64
% 0.10/0.36  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36  % Memory   : 8046.5625MB
% 0.10/0.36  % OS       : Linux 6.8.0-71-generic
% 0.10/0.36  % CPULimit : 300
% 0.10/0.36  % WCLimit  : 300
% 0.10/0.36  % DateTime : Sat Sep  5 02:15:48 UTC 2026
% 0.10/0.37  % CPUTime  : 
% 0.64/1.00  Zenon error: exhausted search space without finding a proof
% 0.64/1.00  (* Current branch:
% 0.64/1.00  (r1 Tau_0 Tau_2)
% 0.64/1.00  (zenon_Vgn != zenon_Vhn)
% 0.64/1.00  (r1 zenon_Vgw zenon_Vhw)
% 0.64/1.00  (zenon_Vdt != zenon_Vqs)
% 0.64/1.00  (p5 zenon_Vov)
% 0.64/1.00  (-. (p13 zenon_Vcs))
% 0.64/1.00  (-. (p23 zenon_Vpk))
% 0.64/1.00  (zenon_Vqi != zenon_Vph)
% 0.64/1.00  (r1 zenon_Vma zenon_Vna)
% 0.64/1.00  (r1 zenon_Vt zenon_Vu)
% 0.64/1.00  (zenon_Vxv != zenon_Vtv)
% 0.64/1.00  (r1 zenon_Vzq zenon_Vor)
% 0.64/1.00  (r1 zenon_Vss zenon_Vet)
% 0.64/1.00  (r1 zenon_Vnw zenon_Vow)
% 0.64/1.00  (r1 zenon_Vea zenon_Vfa)
% 0.64/1.00  (-. (p8 zenon_Vku))
% 0.64/1.00  (p26 zenon_Vqi)
% 0.64/1.00  (zenon_Vkf != zenon_Vlf)
% 0.64/1.00  (r1 zenon_Vkw zenon_Vlw)
% 0.64/1.00  (p21 zenon_Vgn)
% 0.64/1.00  (-. (p19 zenon_Vbo))
% 0.64/1.00  (r1 zenon_Vu zenon_Vv)
% 0.64/1.00  (p17 zenon_Vgq)
% 0.64/1.00  (-. (p10 zenon_Vpt))
% 0.64/1.00  (r1 zenon_Vex zenon_Vfx)
% 0.64/1.00  (-. (p7 zenon_Vtu))
% 0.64/1.00  (p11 zenon_Vpt)
% 0.64/1.00  (p22 zenon_Vkm)
% 0.64/1.00  (-. (p25 zenon_Vrj))
% 0.64/1.00  (r1 zenon_Vcu zenon_Vlu)
% 0.64/1.00  (p14 zenon_Vcs)
% 0.64/1.00  (zenon_Vgq != zenon_Vop)
% 0.64/1.00  (r1 zenon_Voa zenon_Vpa)
% 0.64/1.00  (-. (p30 zenon_Vhe))
% 0.64/1.00  (-. (p28 zenon_Vkf))
% 0.64/1.00  (p18 zenon_Vop)
% 0.64/1.00  (r1 zenon_Vn zenon_Vo)
% 0.64/1.00  (r1 Tau_0 Tau_3)
% 0.64/1.00  (r1 zenon_Vpa zenon_Vqa)
% 0.64/1.00  (zenon_Vxv != zenon_Vyv)
% 0.64/1.00  (r1 zenon_Vdo zenon_Vwo)
% 0.64/1.00  (-. (p3 zenon_Vyv))
% 0.64/1.00  (zenon_Vbo != zenon_Vgn)
% 0.64/1.00  (r1 zenon_Vyw zenon_Vzw)
% 0.64/1.00  (zenon_Vvo != zenon_Vwo)
% 0.64/1.00  (r1 zenon_Vla zenon_Vma)
% 0.64/1.00  (zenon_Vkm != zenon_Vnl)
% 0.64/1.00  (r1 zenon_Vax zenon_Vbx)
% 0.64/1.00  (-. (p2 zenon_Vxv))
% 0.64/1.00  (r1 zenon_Vdv zenon_Vjv)
% 0.64/1.00  (zenon_Vbv != zenon_Vcv)
% 0.64/1.00  (r1 zenon_Vww zenon_Vxw)
% 0.64/1.00  (r1 zenon_Vo zenon_Vp)
% 0.64/1.00  (-. (p30 zenon_Vbd))
% 0.64/1.00  (r1 zenon_Vxo zenon_Vpp)
% 0.64/1.00  (zenon_Vxq != zenon_Vyq)
% 0.64/1.00  (r1 zenon_Vin zenon_Vco)
% 0.64/1.00  (r1 Tau_1 zenon_Vm)
% 0.64/1.00  (-. (p25 zenon_Vqi))
% 0.64/1.00  (zenon_Vqj != zenon_Vrj)
% 0.64/1.00  (r1 zenon_Vqv zenon_Vuv)
% 0.64/1.00  (r1 zenon_Vuw zenon_Vvw)
% 0.64/1.00  (p8 zenon_Vtu)
% 0.64/1.00  (r1 zenon_Vow zenon_Vpw)
% 0.64/1.00  (zenon_Vkf != zenon_Vge)
% 0.64/1.00  (-. (p24 zenon_Vqj))
% 0.64/1.00  (zenon_Vpk != zenon_Vqj)
% 0.64/1.00  (zenon_Vqi != zenon_Vri)
% 0.64/1.00  (zenon_Vqs != zenon_Vcs)
% 0.64/1.00  (-. (p20 zenon_Vco))
% 0.64/1.00  (zenon_Vvb != zenon_Vaw)
% 0.64/1.00  (-. (p31 zenon_Vvb))
% 0.64/1.00  (-. (p4 zenon_Vov))
% 0.64/1.00  (-. (p11 zenon_Vdt))
% 0.64/1.00  (-. (p6 zenon_Vbv))
% 0.64/1.00  (r1 zenon_Vqp zenon_Vhq)
% 0.64/1.00  (-. (p4 zenon_Vuv))
% 0.64/1.00  (zenon_Vbd != zenon_Vcd)
% 0.64/1.00  (-. (p1 zenon_Vfx))
% 0.64/1.00  (p10 zenon_Vau)
% 0.64/1.00  (r1 zenon_Vfw zenon_Vgw)
% 0.64/1.00  (-. (p26 zenon_Vph))
% 0.64/1.00  (r1 zenon_Vz zenon_Vaa)
% 0.64/1.00  (r1 zenon_Vlw zenon_Vmw)
% 0.64/1.00  (r1 zenon_Vrk zenon_Vol)
% 0.64/1.00  (-. (p31 zenon_Vcd))
% 0.64/1.00  (zenon_Vaw != zenon_Vxv)
% 0.64/1.00  (zenon_Vop != zenon_Vvo)
% 0.64/1.00  (r1 zenon_Vp zenon_Vq)
% 0.64/1.00  (zenon_Vau != zenon_Vbu)
% 0.64/1.00  (-. (p21 zenon_Vkm))
% 0.64/1.00  (p23 zenon_Vnl)
% 0.64/1.00  (-. (p5 zenon_Vpv))
% 0.64/1.00  (p19 zenon_Vvo)
% 0.64/1.00  (r1 zenon_Vvv zenon_Vyv)
% 0.64/1.00  (zenon_Vqs != zenon_Vrs)
% 0.64/1.00  (-. (p22 zenon_Vlm))
% 0.64/1.00  (-. (p1 zenon_Vaw))
% 0.64/1.00  (-. (p12 zenon_Vet))
% 0.64/1.00  (zenon_Vcs != zenon_Vnr)
% 0.64/1.00  (r1 zenon_Vbw zenon_Vcw)
% 0.64/1.00  (r1 zenon_Vka zenon_Vla)
% 0.64/1.00  (r1 zenon_Vaa zenon_Vba)
% 0.64/1.00  (-. (p17 zenon_Vop))
% 0.64/1.00  (-. (p27 zenon_Vng))
% 0.64/1.00  (-. (p18 zenon_Vvo))
% 0.64/1.00  (r1 zenon_Vha zenon_Via)
% 0.64/1.00  (p15 zenon_Vnr)
% 0.64/1.00  (r1 zenon_Vrh zenon_Vri)
% 0.64/1.00  (-. (p29 zenon_Vlf))
% 0.64/1.00  (r1 zenon_Vq zenon_Vr)
% 0.64/1.00  (-. (p22 zenon_Vnl))
% 0.64/1.00  (zenon_Vnl != zenon_Vol)
% 0.64/1.00  (p29 zenon_Vkf)
% 0.64/1.00  (zenon_Vpk != zenon_Vqk)
% 0.64/1.00  (r1 zenon_X4 zenon_Vwb)
% 0.64/1.00  (zenon_Vvb != zenon_Vfx)
% 0.64/1.00  (zenon_Viv != zenon_Vjv)
% 0.64/1.00  (p3 zenon_Vxv)
% 0.64/1.00  (r1 zenon_Vna zenon_Voa)
% 0.64/1.00  (r1 zenon_Viw zenon_Vjw)
% 0.64/1.00  (r1 zenon_Vie zenon_Vlf)
% 0.64/1.00  (-. (p14 zenon_Vnr))
% 0.64/1.00  (r1 zenon_Vx zenon_Vy)
% 0.64/1.00  (p31 zenon_Vbd)
% 0.64/1.00  (r1 zenon_Vdd zenon_Vhe)
% 0.64/1.00  (zenon_Viv != zenon_Vbv)
% 0.64/1.00  (r1 zenon_Vtw zenon_Vuw)
% 0.64/1.00  (r1 zenon_Vrt zenon_Vbu)
% 0.64/1.00  (p12 zenon_Vdt)
% 0.64/1.00  (r1 zenon_Vpw zenon_Vqw)
% 0.64/1.00  (-. (p8 zenon_Vuu))
% 0.64/1.00  (r1 zenon_Vfa zenon_Vga)
% 0.64/1.00  (-. (p28 zenon_Vog))
% 0.64/1.00  (r1 zenon_Vft zenon_Vqt)
% 0.64/1.00  (-. (p20 zenon_Vgn))
% 0.64/1.00  (-. (p18 zenon_Vpp))
% 0.64/1.00  (-. (p32 zenon_Vwb))
% 0.64/1.00  (r1 zenon_Vmu zenon_Vuu)
% 0.64/1.00  (p13 zenon_Vqs)
% 0.64/1.00  (p1 zenon_Vvb)
% 0.64/1.00  (-. (p24 zenon_Vqk))
% 0.64/1.00  (-. (p13 zenon_Vrs))
% 0.64/1.00  (r1 zenon_Vpg zenon_Vqh)
% 0.64/1.00  (zenon_Vng != zenon_Vog)
% 0.64/1.00  (r1 zenon_Vew zenon_Vfw)
% 0.64/1.00  (zenon_Vng != zenon_Vkf)
% 0.64/1.00  (-. (p7 zenon_Vcv))
% 0.64/1.00  (zenon_Vgq != zenon_Vhq)
% 0.64/1.00  (r1 zenon_Vy zenon_Vz)
% 0.64/1.00  (p2 zenon_Vaw)
% 0.64/1.00  (p30 zenon_Vge)
% 0.64/1.00  (-. (p3 zenon_Vtv))
% 0.64/1.00  (r1 zenon_Vzw zenon_Vax)
% 0.64/1.00  (zenon_Vnl != zenon_Vpk)
% 0.64/1.00  (r1 zenon_Vcx zenon_Vdx)
% 0.64/1.00  (r1 zenon_Vca zenon_Vda)
% 0.64/1.00  (r1 zenon_Vba zenon_Vca)
% 0.64/1.00  (r1 zenon_Vpl zenon_Vlm)
% 0.64/1.00  (zenon_Vdt != zenon_Vet)
% 0.64/1.00  (r1 zenon_Vjw zenon_Vkw)
% 0.64/1.00  (p7 zenon_Vbv)
% 0.64/1.00  (zenon_Vov != zenon_Viv)
% 0.64/1.00  (-. (p9 zenon_Vlu))
% 0.64/1.00  (-. (p5 zenon_Viv))
% 0.64/1.00  (-. (p19 zenon_Vwo))
% 0.64/1.00  (zenon_Vph != zenon_Vqh)
% 0.64/1.00  (-. (p11 zenon_Vqt))
% 0.64/1.00  (p27 zenon_Vph)
% 0.64/1.00  (zenon_Vbd != zenon_Vvb)
% 0.64/1.00  (r1 zenon_Viq zenon_Vyq)
% 0.64/1.00  (r1 zenon_Vmw zenon_Vnw)
% 0.64/1.00  (r1 zenon_Vkv zenon_Vpv)
% 0.64/1.00  (p25 zenon_Vqj)
% 0.64/1.00  (-. (p26 zenon_Vri))
% 0.64/1.00  (p4 zenon_Vtv)
% 0.64/1.00  (r1 zenon_Vr zenon_Vs)
% 0.64/1.00  (p16 zenon_Vxq)
% 0.64/1.00  (zenon_Vqa != zenon_Vxv)
% 0.64/1.00  (-. (p33 Tau_2))
% 0.64/1.00  (zenon_Vph != zenon_Vng)
% 0.64/1.01  (p28 zenon_Vng)
% 0.64/1.01  (zenon_Vnr != zenon_Vxq)
% 0.64/1.01  (r1 zenon_Via zenon_Vja)
% 0.64/1.01  (-. (p29 zenon_Vge))
% 0.64/1.01  (zenon_Vbo != zenon_Vco)
% 0.64/1.01  (p20 zenon_Vbo)
% 0.64/1.01  (r1 zenon_Vbx zenon_Vcx)
% 0.64/1.01  (r1 zenon_Vdx zenon_Vex)
% 0.64/1.01  (p9 zenon_Vku)
% 0.64/1.01  (-. (p27 zenon_Vqh))
% 0.64/1.01  (zenon_Vge != zenon_Vhe)
% 0.64/1.01  (r1 zenon_Vcw zenon_Vdw)
% 0.64/1.01  (zenon_Vqj != zenon_Vqi)
% 0.64/1.01  (zenon_Vkm != zenon_Vlm)
% 0.64/1.01  (-. (p15 zenon_Vor))
% 0.64/1.01  (r1 zenon_Vvu zenon_Vcv)
% 0.64/1.01  (r1 Tau_0 Tau_1)
% 0.64/1.01  (-. (p16 zenon_Vgq))
% 0.64/1.01  (r1 zenon_Ves zenon_Vrs)
% 0.64/1.01  (r1 zenon_Vxw zenon_Vyw)
% 0.64/1.01  (-. (p17 zenon_Vhq))
% 0.64/1.01  (zenon_Vbv != zenon_Vtu)
% 0.64/1.01  (r1 zenon_Vsi zenon_Vrj)
% 0.64/1.01  (r1 zenon_Vhw zenon_Viw)
% 0.64/1.01  (zenon_Vpt != zenon_Vqt)
% 0.64/1.01  (r1 zenon_Vs zenon_Vt)
% 0.64/1.01  (zenon_Vvo != zenon_Vbo)
% 0.64/1.01  (r1 zenon_Vpr zenon_Vds)
% 0.64/1.01  (zenon_Vtv != zenon_Vuv)
% 0.64/1.01  (r1 zenon_Vvw zenon_Vww)
% 0.64/1.01  (zenon_Vov != zenon_Vpv)
% 0.64/1.01  (-. (p12 zenon_Vqs))
% 0.64/1.01  (zenon_Vau != zenon_Vpt)
% 0.64/1.01  (r1 zenon_Vsj zenon_Vqk)
% 0.64/1.01  (r1 zenon_Vda zenon_Vea)
% 0.64/1.01  (zenon_Vcs != zenon_Vds)
% 0.64/1.01  (p2 zenon_Vqa)
% 0.64/1.01  (r1 zenon_Vsw zenon_Vtw)
% 0.64/1.01  (r1 zenon_Vv zenon_Vw)
% 0.64/1.01  (r1 zenon_Vrw zenon_Vsw)
% 0.64/1.01  (zenon_Vku != zenon_Vlu)
% 0.64/1.01  (r1 zenon_Vm zenon_Vn)
% 0.64/1.01  (p24 zenon_Vpk)
% 0.64/1.01  (r1 zenon_Vxb zenon_Vcd)
% 0.64/1.01  (zenon_Vku != zenon_Vau)
% 0.64/1.01  (zenon_Vpt != zenon_Vdt)
% 0.64/1.01  (-. (p6 zenon_Vjv))
% 0.64/1.01  (zenon_Vge != zenon_Vbd)
% 0.64/1.01  (r1 zenon_Vga zenon_Vha)
% 0.64/1.01  (-. (p9 zenon_Vau))
% 0.64/1.01  (zenon_Vtv != zenon_Vov)
% 0.64/1.01  (r1 zenon_Vw zenon_Vx)
% 0.64/1.01  (zenon_Vop != zenon_Vpp)
% 0.64/1.01  (-. (p15 zenon_Vxq))
% 0.64/1.01  (r1 zenon_Vmm zenon_Vhn)
% 0.64/1.01  (-. (p23 zenon_Vol))
% 0.64/1.01  (-. (p21 zenon_Vhn))
% 0.64/1.01  (zenon_Vnr != zenon_Vor)
% 0.64/1.01  (zenon_Vxq != zenon_Vgq)
% 0.64/1.01  (zenon_Vtu != zenon_Vuu)
% 0.64/1.01  (-. (p10 zenon_Vbu))
% 0.64/1.01  (r1 zenon_Vmf zenon_Vog)
% 0.64/1.01  (-. (p16 zenon_Vyq))
% 0.64/1.01  (-. (p14 zenon_Vds))
% 0.64/1.01  (zenon_Vgn != zenon_Vkm)
% 0.64/1.01  (p6 zenon_Viv)
% 0.64/1.01  (r1 Tau_3 zenon_Vbw)
% 0.64/1.01  (r1 zenon_Vja zenon_Vka)
% 0.64/1.01  (r1 zenon_Vdw zenon_Vew)
% 0.64/1.01  (r1 zenon_Vqw zenon_Vrw)
% 0.64/1.01  (zenon_Vtu != zenon_Vku)
% 0.64/1.01  *)
% 0.64/1.01  (* NO-PROOF *)
% 0.64/1.01  % SZS status GaveUp
% 0.64/1.01  Number of rewrites on terms: 0
% 0.64/1.01  Number of rewrites on props: 0
% 0.64/1.01  nodes searched: 1562
% 0.64/1.01  max branch formulas: 1751
% 0.64/1.01  proof nodes created: 0
% 0.64/1.01  formulas created: 8562
% 0.64/1.01  
%------------------------------------------------------------------------------