↑ Up

ZenonModulo---0.5.0.UNK-Non.f

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

% Computer : n008.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:23 PM UTC 2026

% Result   : Unknown 0.77s 1.03s
% Output   : None 
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : LCL669+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 : n008.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.37  % WCLimit  : 300
% 0.10/0.37  % DateTime : Sat Sep  5 04:14:08 UTC 2026
% 0.10/0.37  % CPUTime  : 
% 0.65/1.03  Zenon error: exhausted search space without finding a proof
% 0.65/1.03  (* Current branch:
% 0.65/1.03  (r1 zenon_Vhx zenon_Vix)
% 0.65/1.03  (zenon_Vwi != zenon_Vxi)
% 0.65/1.03  (zenon_Vjt != zenon_Vkt)
% 0.65/1.03  (zenon_Vcd != zenon_Vvb)
% 0.65/1.03  (r1 zenon_Vby zenon_Vcy)
% 0.65/1.03  (zenon_Vwu != zenon_Vxu)
% 0.65/1.03  (r1 zenon_Vkx zenon_Vlx)
% 0.65/1.03  (zenon_Vhv != zenon_Vwu)
% 0.65/1.03  (r1 zenon_Vjv zenon_Vsv)
% 0.65/1.03  (zenon_Vip != zenon_Vno)
% 0.65/1.03  (r1 Tau_1 zenon_Vm)
% 0.65/1.03  (-. (p11 zenon_Vjt))
% 0.65/1.03  (zenon_Vus != zenon_Ves)
% 0.65/1.03  (r1 zenon_Vma zenon_Vna)
% 0.65/1.03  (-. (p4 zenon_Viw))
% 0.65/1.03  (r1 zenon_Vt zenon_Vu)
% 0.65/1.03  (r1 zenon_Vea zenon_Vfa)
% 0.65/1.03  (r1 zenon_Vcy zenon_Vdy)
% 0.65/1.03  (r1 zenon_Ved zenon_Vje)
% 0.65/1.03  (r1 zenon_Vws zenon_Vkt)
% 0.65/1.03  (r1 zenon_Vu zenon_Vv)
% 0.65/1.03  (r1 zenon_Vex zenon_Vfx)
% 0.65/1.03  (r1 zenon_Vxb zenon_Vdd)
% 0.65/1.03  (-. (p29 zenon_Vcd))
% 0.65/1.03  (-. (p26 zenon_Vrg))
% 0.65/1.03  (-. (p11 zenon_Vyt))
% 0.65/1.03  (p5 zenon_Viw)
% 0.65/1.03  (-. (p30 zenon_Vdd))
% 0.65/1.03  (zenon_Vrg != zenon_Vsg)
% 0.65/1.03  (p2 zenon_Vax)
% 0.65/1.03  (r1 zenon_Voa zenon_Vpa)
% 0.65/1.03  (r1 Tau_0 Tau_3)
% 0.65/1.03  (r1 zenon_Vxx zenon_Vyx)
% 0.65/1.03  (r1 zenon_Vcw zenon_Vjw)
% 0.65/1.03  (zenon_Ves != zenon_Vfs)
% 0.65/1.03  (r1 Tau_3 zenon_Vbx)
% 0.65/1.03  (r1 zenon_Vn zenon_Vo)
% 0.65/1.03  (-. (p22 zenon_Vxl))
% 0.65/1.03  (p25 zenon_Vwi)
% 0.65/1.03  (r1 zenon_Vla zenon_Vma)
% 0.65/1.03  (-. (p13 zenon_Vvs))
% 0.65/1.03  (zenon_Ves != zenon_Vnr)
% 0.65/1.03  (-. (p4 zenon_Vqw))
% 0.65/1.03  (r1 zenon_Vo zenon_Vp)
% 0.65/1.03  (-. (p31 zenon_Vwb))
% 0.65/1.03  (r1 zenon_Vrx zenon_Vsx)
% 0.65/1.03  (r1 zenon_Vfx zenon_Vgx)
% 0.65/1.03  (-. (p24 zenon_Vwi))
% 0.65/1.03  (-. (p25 zenon_Vxi))
% 0.65/1.03  (p27 zenon_Vrg)
% 0.65/1.03  (zenon_Vvb != zenon_Vax)
% 0.65/1.03  (r1 zenon_Vdy zenon_Vey)
% 0.65/1.03  (-. (p20 zenon_Vsn))
% 0.65/1.03  (p11 zenon_Vxt)
% 0.65/1.03  (r1 zenon_Vkw zenon_Vqw)
% 0.65/1.03  (p30 zenon_Vcd)
% 0.65/1.03  (-. (p14 zenon_Vfs))
% 0.65/1.03  (zenon_Vpw != zenon_Viw)
% 0.65/1.03  (zenon_Vpa != zenon_Vvw)
% 0.65/1.03  (zenon_Vip != zenon_Vjp)
% 0.65/1.03  (r1 zenon_Vgx zenon_Vhx)
% 0.65/1.03  (zenon_Vum != zenon_Vvm)
% 0.65/1.03  (r1 zenon_Vwx zenon_Vxx)
% 0.65/1.03  (zenon_Vuh != zenon_Vrg)
% 0.65/1.03  (zenon_Vus != zenon_Vvs)
% 0.65/1.03  (-. (p18 zenon_Vno))
% 0.65/1.03  (-. (p10 zenon_Vxt))
% 0.65/1.03  (r1 zenon_Veq zenon_Vwq)
% 0.65/1.03  (-. (p23 zenon_Vyk))
% 0.65/1.03  (p6 zenon_Vaw)
% 0.65/1.03  (r1 zenon_Vz zenon_Vaa)
% 0.65/1.03  (-. (p7 zenon_Vhv))
% 0.65/1.03  (r1 zenon_Vtx zenon_Vux)
% 0.65/1.03  (r1 zenon_Vtg zenon_Vvh)
% 0.65/1.03  (zenon_Vjt != zenon_Vus)
% 0.65/1.03  (-. (p16 zenon_Vcq))
% 0.65/1.03  (r1 zenon_Vtn zenon_Voo)
% 0.65/1.03  (r1 zenon_Vp zenon_Vq)
% 0.65/1.03  (-. (p19 zenon_Voo))
% 0.65/1.03  (r1 zenon_Vpf zenon_Vsg)
% 0.65/1.03  (r1 zenon_Vix zenon_Vjx)
% 0.65/1.03  (zenon_Vcd != zenon_Vdd)
% 0.65/1.03  (zenon_Viw != zenon_Vaw)
% 0.65/1.03  (r1 zenon_Vzt zenon_Vlu)
% 0.65/1.03  (zenon_Vum != zenon_Vwl)
% 0.65/1.03  (r1 zenon_Vtv zenon_Vbw)
% 0.77/1.03  (r1 zenon_X4 zenon_Vwb)
% 0.77/1.03  (-. (p8 zenon_Vwu))
% 0.77/1.03  (p14 zenon_Ves)
% 0.77/1.03  (zenon_Vnf != zenon_Vof)
% 0.77/1.03  (r1 zenon_Vyx zenon_Vzx)
% 0.77/1.03  (r1 zenon_Vka zenon_Vla)
% 0.77/1.03  (zenon_Vvw != zenon_Vpw)
% 0.77/1.03  (r1 zenon_Vaa zenon_Vba)
% 0.77/1.03  (-. (p26 zenon_Vvh))
% 0.77/1.03  (r1 zenon_Vha zenon_Via)
% 0.77/1.03  (zenon_Vwu != zenon_Vku)
% 0.77/1.03  (p15 zenon_Vnr)
% 0.77/1.03  (-. (p9 zenon_Vxu))
% 0.77/1.03  (r1 zenon_Vlx zenon_Vmx)
% 0.77/1.03  (r1 zenon_Vq zenon_Vr)
% 0.77/1.03  (r1 zenon_Vwm zenon_Vsn)
% 0.77/1.03  (r1 zenon_Vwh zenon_Vxi)
% 0.77/1.03  (r1 zenon_Vox zenon_Vpx)
% 0.77/1.03  (p17 zenon_Vcq)
% 0.77/1.03  (r1 zenon_Vyl zenon_Vvm)
% 0.77/1.03  (-. (p5 zenon_Vaw))
% 0.77/1.03  (r1 zenon_Vmx zenon_Vnx)
% 0.77/1.03  (-. (p17 zenon_Vdq))
% 0.77/1.03  (r1 zenon_Vna zenon_Voa)
% 0.77/1.03  (-. (p3 zenon_Vww))
% 0.77/1.03  (zenon_Vuh != zenon_Vvh)
% 0.77/1.03  (r1 zenon_Vke zenon_Vof)
% 0.77/1.03  (r1 Tau_0 Tau_2)
% 0.77/1.03  (-. (p12 zenon_Vkt))
% 0.77/1.03  (-. (p14 zenon_Vnr))
% 0.77/1.03  (r1 zenon_Vx zenon_Vy)
% 0.77/1.03  (zenon_Vvq != zenon_Vcq)
% 0.77/1.03  (p12 zenon_Vjt)
% 0.77/1.03  (-. (p16 zenon_Vwq))
% 0.77/1.03  (zenon_Vie != zenon_Vje)
% 0.77/1.03  (r1 zenon_Vfa zenon_Vga)
% 0.77/1.03  (p4 zenon_Vpw)
% 0.77/1.03  (-. (p24 zenon_Vyj))
% 0.77/1.03  (-. (p2 zenon_Vvw))
% 0.77/1.03  (zenon_Vxk != zenon_Vyk)
% 0.77/1.03  (-. (p19 zenon_Vrn))
% 0.77/1.03  (zenon_Vie != zenon_Vcd)
% 0.77/1.03  (zenon_Vvq != zenon_Vwq)
% 0.77/1.03  (p1 zenon_Vvb)
% 0.77/1.03  (r1 zenon_Vgs zenon_Vvs)
% 0.77/1.03  (r1 zenon_Vpx zenon_Vqx)
% 0.77/1.03  (zenon_Vwl != zenon_Vxk)
% 0.77/1.03  (r1 zenon_Vyu zenon_Viv)
% 0.77/1.03  (r1 zenon_Vy zenon_Vz)
% 0.77/1.03  (p26 zenon_Vuh)
% 0.77/1.03  (p2 zenon_Vpa)
% 0.77/1.03  (zenon_Vaw != zenon_Vrv)
% 0.77/1.03  (r1 zenon_Vcx zenon_Vdx)
% 0.77/1.03  (-. (p8 zenon_Viv))
% 0.77/1.03  (r1 zenon_Vca zenon_Vda)
% 0.77/1.03  (r1 zenon_Vba zenon_Vca)
% 0.77/1.03  (zenon_Viw != zenon_Vjw)
% 0.77/1.03  (zenon_Vpw != zenon_Vqw)
% 0.77/1.03  (-. (p17 zenon_Vip))
% 0.77/1.03  (zenon_Vvb != zenon_Vey)
% 0.77/1.03  (zenon_Vxt != zenon_Vyt)
% 0.77/1.03  (-. (p18 zenon_Vjp))
% 0.77/1.03  (p24 zenon_Vxj)
% 0.77/1.03  (zenon_Vwl != zenon_Vxl)
% 0.77/1.03  (r1 zenon_Vqx zenon_Vrx)
% 0.77/1.03  (r1 zenon_Vvx zenon_Vwx)
% 0.77/1.03  (r1 zenon_Vpo zenon_Vjp)
% 0.77/1.03  (zenon_Vhv != zenon_Viv)
% 0.77/1.03  (p3 zenon_Vvw)
% 0.77/1.03  (p21 zenon_Vum)
% 0.77/1.03  (p7 zenon_Vrv)
% 0.77/1.03  (p18 zenon_Vip)
% 0.77/1.03  (r1 zenon_Vrw zenon_Vww)
% 0.77/1.03  (zenon_Vnf != zenon_Vie)
% 0.77/1.03  (zenon_Vxt != zenon_Vjt)
% 0.77/1.03  (p16 zenon_Vvq)
% 0.77/1.03  (r1 zenon_Vkp zenon_Vdq)
% 0.77/1.03  (r1 zenon_Vr zenon_Vs)
% 0.77/1.03  (zenon_Vrn != zenon_Vum)
% 0.77/1.03  (r1 Tau_0 Tau_1)
% 0.77/1.03  (r1 zenon_Vux zenon_Vvx)
% 0.77/1.03  (p22 zenon_Vwl)
% 0.77/1.03  (r1 zenon_Via zenon_Vja)
% 0.77/1.03  (zenon_Vnr != zenon_Vvq)
% 0.77/1.03  (zenon_Vrv != zenon_Vsv)
% 0.77/1.03  (-. (p5 zenon_Vjw))
% 0.77/1.03  (p19 zenon_Vno)
% 0.77/1.03  (-. (p6 zenon_Vbw))
% 0.77/1.03  (-. (p28 zenon_Vie))
% 0.77/1.03  (r1 zenon_Vbx zenon_Vcx)
% 0.77/1.03  (r1 zenon_Vdx zenon_Vex)
% 0.77/1.03  (r1 zenon_Vjx zenon_Vkx)
% 0.77/1.03  (r1 zenon_Vnx zenon_Vox)
% 0.77/1.03  (zenon_Vku != zenon_Vxt)
% 0.77/1.03  (r1 zenon_Vzx zenon_Vay)
% 0.77/1.03  (p20 zenon_Vrn)
% 0.77/1.03  (r1 zenon_Vzj zenon_Vyk)
% 0.77/1.03  (-. (p15 zenon_Vor))
% 0.77/1.03  (r1 zenon_Vay zenon_Vby)
% 0.77/1.03  (-. (p3 zenon_Vpw))
% 0.77/1.03  (r1 zenon_Vyi zenon_Vyj)
% 0.77/1.03  (-. (p21 zenon_Vwl))
% 0.77/1.03  (zenon_Vxj != zenon_Vyj)
% 0.77/1.03  (-. (p25 zenon_Vuh))
% 0.77/1.03  (r1 zenon_Vpr zenon_Vfs)
% 0.77/1.03  (-. (p20 zenon_Vum))
% 0.77/1.03  (-. (p28 zenon_Vof))
% 0.77/1.03  (r1 zenon_Vs zenon_Vt)
% 0.77/1.03  (p9 zenon_Vwu)
% 0.77/1.03  (zenon_Vcq != zenon_Vip)
% 0.77/1.03  (zenon_Vcq != zenon_Vdq)
% 0.77/1.03  (-. (p9 zenon_Vku))
% 0.77/1.03  (p23 zenon_Vxk)
% 0.77/1.03  (-. (p1 zenon_Vax))
% 0.77/1.03  (zenon_Vno != zenon_Vrn)
% 0.77/1.03  (-. (p1 zenon_Vey))
% 0.77/1.03  (zenon_Vrv != zenon_Vhv)
% 0.77/1.03  (-. (p15 zenon_Vvq))
% 0.77/1.03  (-. (p29 zenon_Vje))
% 0.77/1.03  (r1 zenon_Vmu zenon_Vxu)
% 0.77/1.03  (zenon_Vaw != zenon_Vbw)
% 0.77/1.03  (-. (p21 zenon_Vvm))
% 0.77/1.03  (r1 zenon_Vda zenon_Vea)
% 0.77/1.03  (-. (p6 zenon_Vrv))
% 0.77/1.03  (zenon_Vrg != zenon_Vnf)
% 0.77/1.03  (zenon_Vxj != zenon_Vwi)
% 0.77/1.03  (zenon_Vax != zenon_Vvw)
% 0.77/1.03  (-. (p10 zenon_Vlu))
% 0.77/1.03  (zenon_Vrn != zenon_Vsn)
% 0.77/1.03  (zenon_Vvw != zenon_Vww)
% 0.77/1.03  (-. (p13 zenon_Ves))
% 0.77/1.03  (r1 zenon_Vv zenon_Vw)
% 0.77/1.03  (zenon_Vku != zenon_Vlu)
% 0.77/1.03  (r1 zenon_Vm zenon_Vn)
% 0.77/1.03  (p28 zenon_Vnf)
% 0.77/1.03  (-. (p27 zenon_Vsg))
% 0.77/1.03  (-. (p22 zenon_Vxk))
% 0.77/1.03  (p29 zenon_Vie)
% 0.77/1.03  (-. (p27 zenon_Vnf))
% 0.77/1.03  (r1 zenon_Vga zenon_Vha)
% 0.77/1.03  (r1 zenon_Vw zenon_Vx)
% 0.77/1.03  (zenon_Vno != zenon_Voo)
% 0.77/1.03  (-. (p7 zenon_Vsv))
% 0.77/1.03  (p13 zenon_Vus)
% 0.77/1.03  (zenon_Vxk != zenon_Vxj)
% 0.77/1.03  (r1 zenon_Vxq zenon_Vor)
% 0.77/1.03  (zenon_Vwi != zenon_Vuh)
% 0.77/1.03  (r1 zenon_Vlt zenon_Vyt)
% 0.77/1.03  (r1 zenon_Vsx zenon_Vtx)
% 0.77/1.03  (-. (p30 zenon_Vvb))
% 0.77/1.03  (zenon_Vnr != zenon_Vor)
% 0.77/1.03  (p8 zenon_Vhv)
% 0.77/1.03  (-. (p12 zenon_Vus))
% 0.77/1.03  (-. (p23 zenon_Vxj))
% 0.77/1.03  (p10 zenon_Vku)
% 0.77/1.03  (r1 zenon_Vzk zenon_Vxl)
% 0.77/1.03  (r1 zenon_Vja zenon_Vka)
% 0.77/1.03  (-. (p32 Tau_2))
% 0.77/1.03  *)
% 0.77/1.03  (* NO-PROOF *)
% 0.77/1.03  % SZS status GaveUp
% 0.77/1.03  Number of rewrites on terms: 0
% 0.77/1.03  Number of rewrites on props: 0
% 0.77/1.03  nodes searched: 1602
% 0.77/1.03  max branch formulas: 1785
% 0.77/1.03  proof nodes created: 0
% 0.77/1.03  formulas created: 8737
% 0.77/1.03  
%------------------------------------------------------------------------------