↑ Up

ZenonModulo---0.5.0.UNK-Non.f

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

% Computer : n020.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.63s 0.93s
% Output   : None 
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : LCL651+1.010 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03  % Command  : run_zenon_modulo %d %s
% 0.08/0.35  % Computer : n020.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 18:01:27 UTC 2026
% 0.08/0.35  % CPUTime  : 
% 0.63/0.92  Zenon error: exhausted search space without finding a proof
% 0.63/0.92  (* Current branch:
% 0.63/0.92  (r1 zenon_Vee zenon_Vgf)
% 0.63/0.92  (r1 zenon_Vap zenon_Vqp)
% 0.63/0.92  (p29 zenon_Vce)
% 0.63/0.92  (r1 zenon_Vpv zenon_Vqv)
% 0.63/0.92  (r1 zenon_Vsv zenon_Vtv)
% 0.63/0.92  (r1 zenon_Vki zenon_Vij)
% 0.63/0.92  (r1 zenon_Vjv zenon_Vkv)
% 0.63/0.92  (zenon_Vhj != zenon_Vii)
% 0.63/0.92  (r1 zenon_Vma zenon_Vna)
% 0.63/0.92  (r1 zenon_Vt zenon_Vu)
% 0.63/0.92  (-. (p19 zenon_Von))
% 0.63/0.92  (-. (p28 zenon_Vgf))
% 0.63/0.92  (r1 zenon_Vwq zenon_Vjr)
% 0.63/0.92  (zenon_Vcl != zenon_Vdl)
% 0.63/0.92  (-. (p29 zenon_Vyc))
% 0.63/0.92  (zenon_Vce != zenon_Vyc)
% 0.63/0.92  (r1 zenon_Vea zenon_Vfa)
% 0.63/0.92  (zenon_Vss != zenon_Vts)
% 0.63/0.92  (-. (p27 zenon_Vff))
% 0.63/0.92  (zenon_Vgo != zenon_Vnn)
% 0.63/0.92  (-. (p17 zenon_Vzo))
% 0.63/0.92  (r1 zenon_Vkr zenon_Vwr)
% 0.63/0.92  (r1 zenon_Vzu zenon_Vav)
% 0.63/0.92  (p20 zenon_Vtm)
% 0.63/0.92  (r1 zenon_Vu zenon_Vv)
% 0.63/0.92  (-. (p28 zenon_Vce))
% 0.63/0.92  (r1 zenon_Viu zenon_Vmu)
% 0.63/0.92  (r1 zenon_Vxu zenon_Vyu)
% 0.63/0.92  (zenon_Vlu != zenon_Vgu)
% 0.63/0.92  (zenon_Vfq != zenon_Vpp)
% 0.63/0.92  (r1 zenon_X4 zenon_Vub)
% 0.63/0.92  (r1 zenon_Voa zenon_Vpa)
% 0.63/0.92  (-. (p18 zenon_Vnn))
% 0.63/0.92  (zenon_Vyc != zenon_Vtb)
% 0.63/0.92  (r1 zenon_Vio zenon_Vzo)
% 0.63/0.92  (r1 zenon_Vvu zenon_Vwu)
% 0.63/0.92  (-. (p24 zenon_Vij))
% 0.63/0.92  (zenon_Vgo != zenon_Vho)
% 0.63/0.92  (r1 zenon_Vn zenon_Vo)
% 0.63/0.92  (r1 zenon_Vrp zenon_Vgq)
% 0.63/0.92  (r1 zenon_Vet zenon_Vmt)
% 0.63/0.92  (zenon_Vhj != zenon_Vij)
% 0.63/0.92  (r1 zenon_Vla zenon_Vma)
% 0.63/0.92  (zenon_Vpa != zenon_Vpu)
% 0.63/0.92  (p2 zenon_Vsu)
% 0.63/0.92  (-. (p22 zenon_Vdl))
% 0.63/0.92  (-. (p15 zenon_Vgq))
% 0.63/0.92  (r1 zenon_Vo zenon_Vp)
% 0.63/0.92  (zenon_Vtm != zenon_Vyl)
% 0.63/0.92  (r1 Tau_3 zenon_Vtu)
% 0.63/0.92  (-. (p15 zenon_Vpp))
% 0.63/0.92  (zenon_Vtt != zenon_Vut)
% 0.63/0.92  (p14 zenon_Vuq)
% 0.63/0.92  (-. (p13 zenon_Vjr))
% 0.63/0.92  (-. (p25 zenon_Vji))
% 0.63/0.92  (r1 zenon_Vdv zenon_Vev)
% 0.63/0.92  (zenon_Vyl != zenon_Vcl)
% 0.63/0.92  (r1 zenon_Vcv zenon_Vdv)
% 0.63/0.92  (zenon_Vfq != zenon_Vgq)
% 0.63/0.92  (r1 zenon_Vov zenon_Vpv)
% 0.63/0.92  (-. (p23 zenon_Vhj))
% 0.63/0.92  (zenon_Vtb != zenon_Vwv)
% 0.63/0.92  (p26 zenon_Vih)
% 0.63/0.92  (r1 zenon_Vbv zenon_Vcv)
% 0.63/0.92  (-. (p8 zenon_Vct))
% 0.63/0.92  (-. (p21 zenon_Vcl))
% 0.63/0.92  (p28 zenon_Vff)
% 0.63/0.92  (-. (p22 zenon_Vfk))
% 0.63/0.92  (-. (p4 zenon_Vgu))
% 0.63/0.92  (zenon_Vhg != zenon_Vff)
% 0.63/0.92  (p24 zenon_Vhj)
% 0.63/0.92  (-. (p32 Tau_2))
% 0.63/0.92  (-. (p23 zenon_Vgk))
% 0.63/0.92  (r1 zenon_Vz zenon_Vaa)
% 0.63/0.92  (-. (p16 zenon_Vyo))
% 0.63/0.92  (r1 zenon_Vrv zenon_Vsv)
% 0.63/0.92  (-. (p26 zenon_Vhg))
% 0.63/0.92  (r1 zenon_Vp zenon_Vq)
% 0.63/0.92  (zenon_Vau != zenon_Vbu)
% 0.63/0.92  (r1 zenon_Vnv zenon_Vov)
% 0.63/0.92  (p6 zenon_Vau)
% 0.63/0.92  (-. (p5 zenon_Vhu))
% 0.63/0.92  (zenon_Vpu != zenon_Vlu)
% 0.63/0.92  (p27 zenon_Vhg)
% 0.63/0.92  (p4 zenon_Vlu)
% 0.63/0.92  (zenon_Vfk != zenon_Vhj)
% 0.63/0.92  (r1 zenon_Vka zenon_Vla)
% 0.63/0.92  (-. (p8 zenon_Vmt))
% 0.63/0.92  (r1 zenon_Vaa zenon_Vba)
% 0.63/0.92  (r1 zenon_Vha zenon_Via)
% 0.63/0.92  (zenon_Vhs != zenon_Vis)
% 0.63/0.92  (r1 zenon_Vqv zenon_Vrv)
% 0.63/0.92  (r1 zenon_Vq zenon_Vr)
% 0.63/0.92  (-. (p9 zenon_Vss))
% 0.63/0.92  (-. (p30 zenon_Vzc))
% 0.63/0.92  (p5 zenon_Vgu)
% 0.63/0.92  (-. (p7 zenon_Vut))
% 0.63/0.92  (zenon_Vhs != zenon_Vvr)
% 0.63/0.92  (r1 zenon_Vmv zenon_Vnv)
% 0.63/0.92  (-. (p6 zenon_Vbu))
% 0.63/0.92  (r1 zenon_Vnu zenon_Vqu)
% 0.63/0.92  (p9 zenon_Vct)
% 0.63/0.92  (zenon_Vpp != zenon_Vyo)
% 0.63/0.92  (zenon_Vlu != zenon_Vmu)
% 0.63/0.92  (-. (p18 zenon_Vho))
% 0.63/0.92  (r1 zenon_Vgv zenon_Vhv)
% 0.63/0.92  (r1 zenon_Vna zenon_Voa)
% 0.63/0.92  (zenon_Vnn != zenon_Vtm)
% 0.63/0.92  (zenon_Vyo != zenon_Vgo)
% 0.63/0.92  (r1 zenon_Vx zenon_Vy)
% 0.63/0.92  (p21 zenon_Vyl)
% 0.63/0.92  (r1 zenon_Vvb zenon_Vzc)
% 0.63/0.92  (-. (p14 zenon_Vfq))
% 0.63/0.92  (r1 zenon_Vjs zenon_Vts)
% 0.63/0.92  (-. (p10 zenon_Vts))
% 0.63/0.92  (r1 zenon_Vyu zenon_Vzu)
% 0.63/0.92  (r1 zenon_Vfa zenon_Vga)
% 0.63/0.92  (-. (p30 zenon_Vtb))
% 0.63/0.92  (-. (p19 zenon_Vtm))
% 0.63/0.92  (r1 zenon_Vwu zenon_Vxu)
% 0.63/0.92  (p18 zenon_Vgo)
% 0.63/0.92  (-. (p9 zenon_Vdt))
% 0.63/0.92  (zenon_Vhg != zenon_Vig)
% 0.63/0.92  (p3 zenon_Vpu)
% 0.63/0.92  (-. (p14 zenon_Vvq))
% 0.63/0.92  (-. (p24 zenon_Vii))
% 0.63/0.92  (p17 zenon_Vyo)
% 0.63/0.92  (p25 zenon_Vii)
% 0.63/0.92  (-. (p11 zenon_Vis))
% 0.63/0.92  (-. (p6 zenon_Vtt))
% 0.63/0.92  (zenon_Vir != zenon_Vuq)
% 0.63/0.92  (r1 zenon_Vkv zenon_Vlv)
% 0.63/0.92  (zenon_Vii != zenon_Vji)
% 0.63/0.92  (p11 zenon_Vhs)
% 0.63/0.92  (r1 zenon_Vev zenon_Vfv)
% 0.63/0.92  (zenon_Vtm != zenon_Vum)
% 0.63/0.92  (zenon_Vct != zenon_Vdt)
% 0.63/0.92  (zenon_Vvr != zenon_Vwr)
% 0.63/0.92  (r1 zenon_Vy zenon_Vz)
% 0.63/0.92  (r1 zenon_Vxr zenon_Vis)
% 0.63/0.92  (r1 zenon_Vam zenon_Vum)
% 0.63/0.92  (p2 zenon_Vpa)
% 0.63/0.92  (p19 zenon_Vnn)
% 0.63/0.92  (-. (p16 zenon_Vqp))
% 0.63/0.92  (-. (p4 zenon_Vmu))
% 0.63/0.92  (r1 zenon_Vca zenon_Vda)
% 0.63/0.92  (p15 zenon_Vfq)
% 0.63/0.92  (r1 zenon_Viv zenon_Vjv)
% 0.63/0.92  (r1 zenon_Vba zenon_Vca)
% 0.63/0.92  (p12 zenon_Vvr)
% 0.63/0.92  (-. (p13 zenon_Vuq))
% 0.63/0.92  (-. (p29 zenon_Vde))
% 0.63/0.92  (zenon_Vau != zenon_Vtt)
% 0.63/0.92  (zenon_Vuq != zenon_Vfq)
% 0.63/0.92  (r1 Tau_0 Tau_2)
% 0.63/0.92  (r1 zenon_Vhq zenon_Vvq)
% 0.63/0.92  (-. (p3 zenon_Vqu))
% 0.63/0.92  (zenon_Vyc != zenon_Vzc)
% 0.63/0.92  (zenon_Vir != zenon_Vjr)
% 0.63/0.92  (r1 Tau_0 Tau_1)
% 0.63/0.92  (zenon_Vfk != zenon_Vgk)
% 0.63/0.92  (r1 zenon_Vhv zenon_Viv)
% 0.63/0.92  (p10 zenon_Vss)
% 0.63/0.92  (zenon_Vsu != zenon_Vpu)
% 0.63/0.92  (-. (p25 zenon_Vih))
% 0.63/0.92  (r1 zenon_Vr zenon_Vs)
% 0.63/0.92  (-. (p7 zenon_Vlt))
% 0.63/0.92  (r1 zenon_Vjg zenon_Vjh)
% 0.63/0.92  (zenon_Vyo != zenon_Vzo)
% 0.63/0.92  (zenon_Vff != zenon_Vce)
% 0.63/0.92  (r1 zenon_Via zenon_Vja)
% 0.63/0.92  (r1 zenon_Vad zenon_Vde)
% 0.63/0.92  (r1 zenon_Vlv zenon_Vmv)
% 0.63/0.92  (r1 zenon_Vtu zenon_Vuu)
% 0.63/0.92  (r1 zenon_Vvt zenon_Vbu)
% 0.63/0.92  (-. (p2 zenon_Vpu))
% 0.63/0.92  (r1 zenon_Vav zenon_Vbv)
% 0.63/0.92  (p30 zenon_Vyc)
% 0.63/0.92  (r1 zenon_Vuv zenon_Vvv)
% 0.63/0.92  (r1 zenon_Vpn zenon_Vho)
% 0.63/0.93  (r1 zenon_Vtv zenon_Vuv)
% 0.63/0.93  (r1 zenon_Vfv zenon_Vgv)
% 0.63/0.93  (p1 zenon_Vtb)
% 0.63/0.93  (zenon_Vtb != zenon_Vsu)
% 0.63/0.93  (p13 zenon_Vir)
% 0.63/0.93  (-. (p20 zenon_Vum))
% 0.63/0.93  (-. (p5 zenon_Vau))
% 0.63/0.93  (r1 zenon_Vvv zenon_Vwv)
% 0.63/0.93  (r1 zenon_Vs zenon_Vt)
% 0.63/0.93  (zenon_Vcl != zenon_Vfk)
% 0.63/0.93  (zenon_Vvr != zenon_Vir)
% 0.63/0.93  (r1 zenon_Vus zenon_Vdt)
% 0.63/0.93  (zenon_Vtt != zenon_Vlt)
% 0.63/0.93  (zenon_Vlt != zenon_Vmt)
% 0.63/0.93  (zenon_Vpu != zenon_Vqu)
% 0.63/0.93  (-. (p26 zenon_Vjh))
% 0.63/0.93  (-. (p31 zenon_Vub))
% 0.63/0.93  (p16 zenon_Vpp)
% 0.63/0.93  (zenon_Vyl != zenon_Vzl)
% 0.63/0.93  (zenon_Vii != zenon_Vih)
% 0.63/0.93  (-. (p10 zenon_Vhs))
% 0.63/0.93  (p7 zenon_Vtt)
% 0.63/0.93  (zenon_Vgu != zenon_Vhu)
% 0.63/0.93  (r1 zenon_Vda zenon_Vea)
% 0.63/0.93  (-. (p12 zenon_Vwr))
% 0.63/0.93  (zenon_Vih != zenon_Vjh)
% 0.63/0.93  (r1 Tau_0 Tau_3)
% 0.63/0.93  (zenon_Vnn != zenon_Von)
% 0.63/0.93  (r1 zenon_Vv zenon_Vw)
% 0.63/0.93  (r1 Tau_1 zenon_Vm)
% 0.63/0.93  (p8 zenon_Vlt)
% 0.63/0.93  (r1 zenon_Vm zenon_Vn)
% 0.63/0.93  (-. (p20 zenon_Vyl))
% 0.63/0.93  (zenon_Vct != zenon_Vss)
% 0.63/0.93  (p23 zenon_Vfk)
% 0.63/0.93  (zenon_Vlt != zenon_Vct)
% 0.63/0.93  (r1 zenon_Vkh zenon_Vji)
% 0.63/0.93  (zenon_Vpp != zenon_Vqp)
% 0.63/0.93  (-. (p21 zenon_Vzl))
% 0.63/0.93  (r1 zenon_Vcu zenon_Vhu)
% 0.63/0.93  (r1 zenon_Vjj zenon_Vgk)
% 0.63/0.93  (r1 zenon_Vga zenon_Vha)
% 0.63/0.93  (r1 zenon_Vw zenon_Vx)
% 0.63/0.93  (zenon_Vih != zenon_Vhg)
% 0.63/0.93  (r1 zenon_Vhk zenon_Vdl)
% 0.63/0.93  (-. (p11 zenon_Vvr))
% 0.63/0.93  (r1 zenon_Vnt zenon_Vut)
% 0.63/0.93  (-. (p3 zenon_Vlu))
% 0.63/0.93  (zenon_Vgu != zenon_Vau)
% 0.63/0.93  (r1 zenon_Vvm zenon_Von)
% 0.63/0.93  (-. (p17 zenon_Vgo))
% 0.63/0.93  (-. (p1 zenon_Vsu))
% 0.63/0.93  (zenon_Vss != zenon_Vhs)
% 0.63/0.93  (p22 zenon_Vcl)
% 0.63/0.93  (zenon_Vff != zenon_Vgf)
% 0.63/0.93  (r1 zenon_Vel zenon_Vzl)
% 0.63/0.93  (-. (p12 zenon_Vir))
% 0.63/0.93  (zenon_Vce != zenon_Vde)
% 0.63/0.93  (-. (p27 zenon_Vig))
% 0.63/0.93  (zenon_Vuq != zenon_Vvq)
% 0.63/0.93  (r1 zenon_Vhf zenon_Vig)
% 0.63/0.93  (r1 zenon_Vuu zenon_Vvu)
% 0.63/0.93  (r1 zenon_Vja zenon_Vka)
% 0.63/0.93  (-. (p1 zenon_Vwv))
% 0.63/0.93  *)
% 0.63/0.93  (* NO-PROOF *)
% 0.63/0.93  % SZS status GaveUp
% 0.63/0.93  Number of rewrites on terms: 0
% 0.63/0.93  Number of rewrites on props: 0
% 0.63/0.93  nodes searched: 1482
% 0.63/0.93  max branch formulas: 1665
% 0.63/0.93  proof nodes created: 0
% 0.63/0.93  formulas created: 8142
% 0.63/0.93  
%------------------------------------------------------------------------------