↑ Up

ZenonModulo---0.5.0.UNK-Non.f

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

% Computer : n031.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:22 PM UTC 2026

% Result   : Unknown 0.31s 0.58s
% Output   : None 
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02  % Problem  : LCL668+1.005 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.02  % Command  : run_zenon_modulo %d %s
% 0.06/0.33  % Computer : n031.cluster.edu
% 0.06/0.33  % Model    : x86_64 x86_64
% 0.06/0.33  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.33  % Memory   : 8046.5625MB
% 0.06/0.33  % OS       : Linux 6.8.0-71-generic
% 0.06/0.33  % CPULimit : 300
% 0.06/0.33  % WCLimit  : 300
% 0.06/0.33  % DateTime : Sat Sep  5 06:14:24 UTC 2026
% 0.06/0.33  % CPUTime  : 
% 0.31/0.57  Zenon error: exhausted search space without finding a proof
% 0.31/0.57  (* Current branch:
% 0.31/0.57  (r1 zenon_Vnr zenon_Vor)
% 0.31/0.57  (-. (p8 zenon_Vno))
% 0.31/0.57  (r1 zenon_Vtq zenon_Vuq)
% 0.31/0.57  (r1 zenon_X4 zenon_Vmb)
% 0.31/0.57  (r1 Tau_1 zenon_Vm)
% 0.31/0.57  (r1 zenon_Vfr zenon_Vgr)
% 0.31/0.57  (r1 zenon_Vjr zenon_Vkr)
% 0.31/0.57  (r1 zenon_Vng zenon_Vjh)
% 0.31/0.57  (zenon_Vnc != zenon_Voc)
% 0.31/0.57  (r1 Tau_0 Tau_2)
% 0.31/0.57  (r1 zenon_Vt zenon_Vu)
% 0.31/0.57  (-. (p13 zenon_Vvl))
% 0.31/0.57  (-. (p6 zenon_Vip))
% 0.31/0.57  (-. (p4 zenon_Vhq))
% 0.31/0.57  (r1 zenon_Vea zenon_Vfa)
% 0.31/0.57  (r1 zenon_Vgl zenon_Vwl)
% 0.31/0.57  (zenon_Vyo != zenon_Vno)
% 0.31/0.57  (r1 zenon_Vnm zenon_Vbn)
% 0.31/0.57  (r1 zenon_Vmr zenon_Vnr)
% 0.31/0.57  (r1 zenon_Vcr zenon_Vdr)
% 0.31/0.57  (p13 zenon_Vlm)
% 0.31/0.57  (r1 zenon_Vu zenon_Vv)
% 0.31/0.57  (-. (p8 zenon_Vzo))
% 0.31/0.57  (zenon_Vvl != zenon_Vwl)
% 0.31/0.57  (r1 zenon_Vvq zenon_Vwq)
% 0.31/0.57  (p14 zenon_Vvl)
% 0.31/0.57  (zenon_Vtj != zenon_Vuj)
% 0.31/0.57  (r1 zenon_Vn zenon_Vo)
% 0.31/0.57  (zenon_Vmq != zenon_Vgq)
% 0.31/0.57  (zenon_Vgq != zenon_Vzp)
% 0.31/0.57  (p18 zenon_Vzi)
% 0.31/0.57  (r1 zenon_Vxq zenon_Vyq)
% 0.31/0.57  (r1 zenon_Vor zenon_Vpr)
% 0.31/0.57  (-. (p5 zenon_Vrp))
% 0.31/0.57  (-. (p20 zenon_Vlg))
% 0.31/0.57  (p15 zenon_Vel)
% 0.31/0.57  (p6 zenon_Vrp)
% 0.31/0.57  (zenon_Vlg != zenon_Vmg)
% 0.31/0.57  (r1 Tau_0 Tau_3)
% 0.31/0.57  (p1 zenon_Vlb)
% 0.31/0.57  (-. (p23 zenon_Vpe))
% 0.31/0.57  (r1 zenon_Vpc zenon_Vpd)
% 0.31/0.57  (zenon_Vzp != zenon_Vrp)
% 0.31/0.57  (r1 zenon_Vap zenon_Vjp)
% 0.31/0.57  (r1 zenon_Vo zenon_Vp)
% 0.31/0.57  (zenon_Vzi != zenon_Vaj)
% 0.31/0.57  (r1 zenon_Vkh zenon_Vfi)
% 0.31/0.57  (p12 zenon_Van)
% 0.31/0.57  (-. (p21 zenon_Vnf))
% 0.31/0.57  (r1 zenon_Vbr zenon_Vcr)
% 0.31/0.57  (zenon_Vel != zenon_Vfl)
% 0.31/0.57  (p2 zenon_Vka)
% 0.31/0.57  (zenon_Vip != zenon_Vjp)
% 0.31/0.57  (-. (p7 zenon_Vyo))
% 0.31/0.57  (zenon_Vlm != zenon_Vmm)
% 0.31/0.57  (-. (p24 zenon_Vpd))
% 0.31/0.57  (p19 zenon_Vei)
% 0.31/0.57  (zenon_Van != zenon_Vbn)
% 0.31/0.57  (zenon_Vmq != zenon_Vnq)
% 0.31/0.57  (r1 zenon_Vz zenon_Vaa)
% 0.31/0.57  (-. (p19 zenon_Vih))
% 0.31/0.57  (r1 zenon_Vqn zenon_Vco)
% 0.31/0.57  (r1 zenon_Vbq zenon_Vhq)
% 0.31/0.57  (-. (p2 zenon_Vmq))
% 0.31/0.57  (r1 zenon_Vp zenon_Vq)
% 0.31/0.57  (r1 zenon_Vpf zenon_Vmg)
% 0.31/0.57  (r1 zenon_Vtp zenon_Vaq)
% 0.31/0.57  (p4 zenon_Vgq)
% 0.31/0.57  (r1 zenon_Ver zenon_Vfr)
% 0.31/0.57  (-. (p12 zenon_Vbn))
% 0.31/0.57  (zenon_Vod != zenon_Vnc)
% 0.31/0.57  (p24 zenon_Vod)
% 0.31/0.57  (r1 zenon_Var zenon_Vbr)
% 0.31/0.57  (r1 zenon_Vcn zenon_Vpn)
% 0.31/0.57  (zenon_Vnf != zenon_Vof)
% 0.31/0.57  (-. (p3 zenon_Vgq))
% 0.31/0.57  (r1 zenon_Vsq zenon_Vtq)
% 0.31/0.57  (r1 zenon_Vaa zenon_Vba)
% 0.31/0.57  (-. (p19 zenon_Vfi))
% 0.31/0.57  (r1 zenon_Vha zenon_Via)
% 0.31/0.57  (zenon_Vbo != zenon_Von)
% 0.31/0.57  (zenon_Vel != zenon_Vmk)
% 0.31/0.57  (-. (p13 zenon_Vmm))
% 0.31/0.57  (r1 zenon_Vgr zenon_Vhr)
% 0.31/0.57  (r1 zenon_Vq zenon_Vr)
% 0.31/0.57  (-. (p14 zenon_Vel))
% 0.31/0.57  (-. (p24 zenon_Vnc))
% 0.31/0.57  (p5 zenon_Vzp)
% 0.31/0.57  (-. (p20 zenon_Vjh))
% 0.31/0.57  (-. (p9 zenon_Vbo))
% 0.31/0.57  (-. (p17 zenon_Vuj))
% 0.31/0.57  (-. (p6 zenon_Vsp))
% 0.31/0.57  (r1 zenon_Vx zenon_Vy)
% 0.31/0.57  (zenon_Vlg != zenon_Vnf)
% 0.31/0.57  (r1 zenon_Vvj zenon_Vnk)
% 0.31/0.57  (p20 zenon_Vih)
% 0.31/0.57  (-. (p27 Tau_2))
% 0.31/0.57  (r1 zenon_Vfa zenon_Vga)
% 0.31/0.57  (r1 zenon_Vir zenon_Vjr)
% 0.31/0.57  (p10 zenon_Vbo)
% 0.31/0.57  (zenon_Vzi != zenon_Vei)
% 0.31/0.57  (zenon_Vgq != zenon_Vhq)
% 0.31/0.57  (r1 zenon_Vdr zenon_Ver)
% 0.31/0.57  (r1 zenon_Vyq zenon_Vzq)
% 0.31/0.57  (-. (p12 zenon_Vlm))
% 0.31/0.57  (p17 zenon_Vtj)
% 0.31/0.57  (r1 zenon_Vy zenon_Vz)
% 0.31/0.57  (-. (p17 zenon_Vzi))
% 0.31/0.57  (p7 zenon_Vip)
% 0.31/0.57  (r1 zenon_Vhr zenon_Vir)
% 0.31/0.57  (zenon_Voe != zenon_Vpe)
% 0.31/0.57  (r1 zenon_Viq zenon_Vnq)
% 0.31/0.57  (r1 Tau_3 zenon_Vsq)
% 0.31/0.57  (r1 zenon_Vca zenon_Vda)
% 0.31/0.57  (r1 zenon_Vba zenon_Vca)
% 0.31/0.57  (-. (p26 zenon_Vmb))
% 0.31/0.57  (zenon_Vih != zenon_Vlg)
% 0.31/0.57  (r1 zenon_Vbj zenon_Vuj)
% 0.31/0.57  (zenon_Vod != zenon_Vpd)
% 0.31/0.57  (p16 zenon_Vmk)
% 0.31/0.57  (zenon_Von != zenon_Van)
% 0.31/0.57  (zenon_Vrq != zenon_Vmq)
% 0.31/0.57  (r1 Tau_0 Tau_1)
% 0.31/0.57  (zenon_Vtj != zenon_Vzi)
% 0.31/0.57  (zenon_Vmk != zenon_Vtj)
% 0.31/0.57  (p11 zenon_Von)
% 0.31/0.57  (zenon_Vno != zenon_Vbo)
% 0.31/0.57  (r1 zenon_Vqe zenon_Vof)
% 0.31/0.57  (r1 zenon_Vr zenon_Vs)
% 0.31/0.57  (p25 zenon_Vnc)
% 0.31/0.57  (p2 zenon_Vrq)
% 0.31/0.57  (zenon_Vyo != zenon_Vzo)
% 0.31/0.57  (r1 zenon_Via zenon_Vja)
% 0.31/0.57  (p23 zenon_Voe)
% 0.31/0.57  (zenon_Vnc != zenon_Vlb)
% 0.31/0.57  (p9 zenon_Vno)
% 0.31/0.57  (-. (p23 zenon_Vod))
% 0.31/0.57  (zenon_Vbo != zenon_Vco)
% 0.31/0.57  (r1 zenon_Vkp zenon_Vsp)
% 0.31/0.57  (-. (p11 zenon_Van))
% 0.31/0.57  (-. (p18 zenon_Vaj))
% 0.31/0.57  (r1 zenon_Vgi zenon_Vaj)
% 0.31/0.57  (r1 zenon_Vwq zenon_Vxq)
% 0.31/0.57  (zenon_Van != zenon_Vlm)
% 0.31/0.57  (r1 zenon_Vpr zenon_Vqr)
% 0.31/0.57  (-. (p16 zenon_Vnk))
% 0.31/0.57  (r1 zenon_Vok zenon_Vfl)
% 0.31/0.57  (p3 zenon_Vmq)
% 0.31/0.57  (-. (p25 zenon_Vlb))
% 0.31/0.57  (zenon_Voe != zenon_Vod)
% 0.31/0.57  (r1 zenon_Vs zenon_Vt)
% 0.31/0.57  (-. (p3 zenon_Vnq))
% 0.31/0.57  (-. (p21 zenon_Vmg))
% 0.31/0.57  (-. (p25 zenon_Voc))
% 0.31/0.57  (r1 zenon_Vuq zenon_Vvq)
% 0.31/0.57  (-. (p7 zenon_Vjp))
% 0.31/0.57  (r1 zenon_Vda zenon_Vea)
% 0.31/0.57  (zenon_Vih != zenon_Vjh)
% 0.31/0.57  (zenon_Vvl != zenon_Vel)
% 0.31/0.57  (zenon_Vlb != zenon_Vrq)
% 0.31/0.57  (-. (p1 zenon_Vqr))
% 0.31/0.57  (r1 zenon_Vv zenon_Vw)
% 0.31/0.57  (r1 zenon_Vpo zenon_Vzo)
% 0.31/0.57  (zenon_Vnf != zenon_Voe)
% 0.31/0.57  (r1 zenon_Vkr zenon_Vlr)
% 0.31/0.57  (r1 zenon_Vm zenon_Vn)
% 0.31/0.57  (r1 zenon_Vnb zenon_Voc)
% 0.31/0.57  (zenon_Vip != zenon_Vyo)
% 0.31/0.57  (-. (p22 zenon_Voe))
% 0.31/0.57  (-. (p22 zenon_Vof))
% 0.31/0.57  (zenon_Vlb != zenon_Vqr)
% 0.31/0.57  (p8 zenon_Vyo)
% 0.31/0.57  (zenon_Vzp != zenon_Vaq)
% 0.31/0.57  (zenon_Vei != zenon_Vfi)
% 0.31/0.57  (-. (p15 zenon_Vfl))
% 0.31/0.57  (r1 zenon_Vga zenon_Vha)
% 0.31/0.57  (p21 zenon_Vlg)
% 0.31/0.57  (r1 zenon_Vw zenon_Vx)
% 0.31/0.57  (zenon_Vno != zenon_Voo)
% 0.31/0.57  (zenon_Vei != zenon_Vih)
% 0.31/0.58  (p22 zenon_Vnf)
% 0.31/0.58  (zenon_Von != zenon_Vpn)
% 0.31/0.58  (r1 zenon_Vdo zenon_Voo)
% 0.31/0.58  (-. (p18 zenon_Vei))
% 0.31/0.58  (zenon_Vka != zenon_Vmq)
% 0.31/0.58  (zenon_Vmk != zenon_Vnk)
% 0.31/0.58  (zenon_Vrp != zenon_Vip)
% 0.31/0.58  (r1 zenon_Vqd zenon_Vpe)
% 0.31/0.58  (-. (p11 zenon_Vpn))
% 0.31/0.58  (-. (p10 zenon_Vco))
% 0.31/0.58  (-. (p16 zenon_Vtj))
% 0.31/0.58  (zenon_Vrp != zenon_Vsp)
% 0.31/0.58  (-. (p14 zenon_Vwl))
% 0.31/0.58  (zenon_Vlm != zenon_Vvl)
% 0.31/0.58  (r1 zenon_Vxl zenon_Vmm)
% 0.31/0.58  (-. (p1 zenon_Vrq))
% 0.31/0.58  (-. (p5 zenon_Vaq))
% 0.31/0.58  (-. (p9 zenon_Voo))
% 0.31/0.58  (-. (p4 zenon_Vzp))
% 0.31/0.58  (-. (p15 zenon_Vmk))
% 0.31/0.58  (r1 zenon_Vja zenon_Vka)
% 0.31/0.58  (r1 zenon_Vzq zenon_Var)
% 0.31/0.58  (r1 zenon_Vlr zenon_Vmr)
% 0.31/0.58  (-. (p10 zenon_Von))
% 0.31/0.58  *)
% 0.31/0.58  (* NO-PROOF *)
% 0.31/0.58  % SZS status GaveUp
% 0.31/0.58  Number of rewrites on terms: 0
% 0.31/0.58  Number of rewrites on props: 0
% 0.31/0.58  nodes searched: 1212
% 0.31/0.58  max branch formulas: 1365
% 0.31/0.58  proof nodes created: 0
% 0.31/0.58  formulas created: 6701
% 0.31/0.58  
%------------------------------------------------------------------------------