↑ Up

ZenonModulo---0.5.0.UNK-Non.f

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

% Computer : n029.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:28 PM UTC 2026

% Result   : Unknown 9.14s 9.47s
% Output   : None 
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02  % Problem  : LCL683+1.010 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.02  % Command  : run_zenon_modulo %d %s
% 0.09/0.35  % Computer : n029.cluster.edu
% 0.09/0.35  % Model    : x86_64 x86_64
% 0.09/0.35  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35  % Memory   : 8046.5625MB
% 0.09/0.35  % OS       : Linux 6.8.0-71-generic
% 0.09/0.35  % CPULimit : 300
% 0.09/0.35  % WCLimit  : 300
% 0.09/0.35  % DateTime : Fri Sep  4 14:52:09 UTC 2026
% 0.09/0.35  % CPUTime  : 
% 9.14/9.46  Zenon error: exhausted search space without finding a proof
% 9.14/9.46  (* Current branch:
% 9.14/9.46  (p86 zenon_Vgj)
% 9.14/9.46  (p116 zenon_Vm)
% 9.14/9.46  (p104 zenon_Vqc)
% 9.14/9.46  (p81 zenon_Vxr)
% 9.14/9.46  (p92 zenon_Vof)
% 9.14/9.46  (p74 zenon_Vav)
% 9.14/9.46  (zenon_Vrga != zenon_Vrha)
% 9.14/9.46  (p101 zenon_Vei)
% 9.14/9.46  (p91 zenon_Vdo)
% 9.14/9.46  (p102 zenon_Vad)
% 9.14/9.46  (p92 zenon_Vsd)
% 9.14/9.46  (p64 zenon_Vaw)
% 9.14/9.46  (zenon_Vdha != zenon_Vqha)
% 9.14/9.46  (p25 zenon_Vvga)
% 9.14/9.46  (p73 zenon_Vov)
% 9.14/9.46  (p45 zenon_Vqda)
% 9.14/9.46  (p45 zenon_Veda)
% 9.14/9.46  (-. (p12 zenon_Vyha))
% 9.14/9.46  (p15 zenon_X158)
% 9.14/9.46  (p13 zenon_X161)
% 9.14/9.46  (p52 zenon_Vgy)
% 9.14/9.46  (p65 zenon_Vqx)
% 9.14/9.46  (p33 zenon_Vyfa)
% 9.14/9.46  (p42 zenon_Voba)
% 9.14/9.46  (p66 zenon_Vuv)
% 9.14/9.46  (p81 zenon_Vvs)
% 9.14/9.46  (p61 zenon_Voz)
% 9.14/9.46  (zenon_Vrga != zenon_Vuha)
% 9.14/9.46  (p14 zenon_X153)
% 9.14/9.46  (p16 zenon_X152)
% 9.14/9.46  (p21 zenon_Vhha)
% 9.14/9.46  (p43 zenon_Vaea)
% 9.14/9.46  (r1 zenon_Vzha zenon_Vvha)
% 9.14/9.46  (p46 zenon_Vgba)
% 9.14/9.46  (p94 zenon_Vvl)
% 9.14/9.46  (p62 zenon_Vgw)
% 9.14/9.46  (zenon_Vjha != zenon_Vtha)
% 9.14/9.46  (zenon_X158 != zenon_Vwha)
% 9.14/9.46  (zenon_X163 != zenon_Vzha)
% 9.14/9.46  (r1 Tau_0 Tau_1)
% 9.14/9.46  (p96 zenon_Vbh)
% 9.14/9.46  (p56 zenon_Vby)
% 9.14/9.46  (-. (p21 zenon_Vtha))
% 9.14/9.46  (p102 zenon_Vwb)
% 9.14/9.46  (p46 zenon_Vcca)
% 9.14/9.46  (p21 zenon_Vnha)
% 9.14/9.46  (p101 zenon_Vuh)
% 9.14/9.46  (zenon_Vzga != zenon_Vqha)
% 9.14/9.46  (p112 zenon_Vp)
% 9.14/9.46  (zenon_Vlha != zenon_Vtha)
% 9.14/9.46  (-. (p25 zenon_Vpha))
% 9.14/9.46  (p41 zenon_Vsea)
% 9.14/9.46  (p35 zenon_Vpfa)
% 9.14/9.46  (p91 zenon_Vun)
% 9.14/9.46  (p84 zenon_Voj)
% 9.14/9.46  (p102 zenon_Vsa)
% 9.14/9.46  (p85 zenon_Vzo)
% 9.14/9.46  (p61 zenon_Vuz)
% 9.14/9.46  (p86 zenon_Vvm)
% 9.14/9.46  (r1 Tau_0 Tau_2)
% 9.14/9.46  (p45 zenon_Vida)
% 9.14/9.46  (p23 zenon_Vzga)
% 9.14/9.46  (p81 zenon_Vns)
% 9.14/9.46  (p52 zenon_Viz)
% 9.14/9.46  (p43 zenon_Veea)
% 9.14/9.46  (p86 zenon_Vwk)
% 9.14/9.46  (p95 zenon_Vok)
% 9.14/9.46  (p62 zenon_Vtu)
% 9.14/9.46  (p55 zenon_Vxaa)
% 9.14/9.46  (p81 zenon_Vfs)
% 9.14/9.46  (zenon_X164 != zenon_Vzha)
% 9.14/9.46  (-. (p13 zenon_Vxha))
% 9.14/9.46  (p61 zenon_Vgaa)
% 9.14/9.46  (p73 zenon_Vhv)
% 9.14/9.46  (r1 zenon_Vwha zenon_Vqha)
% 9.14/9.46  (-. (p25 zenon_Vuha))
% 9.14/9.46  (p76 zenon_Vir)
% 9.14/9.46  (p36 zenon_Vjfa)
% 9.14/9.46  (p33 zenon_Vbga)
% 9.14/9.46  (zenon_X159 != zenon_Vwha)
% 9.14/9.46  (p15 zenon_X159)
% 9.14/9.46  (p24 zenon_Vtfa)
% 9.14/9.46  (p83 zenon_Vlq)
% 9.14/9.46  (p26 zenon_Vdga)
% 9.14/9.46  (p66 zenon_Vhu)
% 9.14/9.46  (-. (p23 zenon_Vqha))
% 9.14/9.46  (p25 zenon_Vrga)
% 9.14/9.46  (p44 zenon_Voaa)
% 9.14/9.46  (p76 zenon_Vwp)
% 9.14/9.46  (p45 zenon_Vmda)
% 9.14/9.46  (p82 zenon_Vln)
% 9.14/9.46  (p44 zenon_Vgca)
% 9.14/9.46  (p46 zenon_Vkaa)
% 9.14/9.46  (p41 zenon_Vafa)
% 9.14/9.46  (r1 Tau_2 zenon_Vxha)
% 9.14/9.46  (p55 zenon_Vcba)
% 9.14/9.46  (p23 zenon_Vdha)
% 9.14/9.46  (p31 zenon_Vnga)
% 9.14/9.46  (p24 zenon_Vefa)
% 9.14/9.46  (zenon_X161 != zenon_Vxha)
% 9.14/9.46  (p103 zenon_Vig)
% 9.14/9.46  (p75 zenon_Vbu)
% 9.14/9.46  (p34 zenon_Vxca)
% 9.14/9.46  (p53 zenon_Vyba)
% 9.14/9.46  (p105 zenon_Vce)
% 9.14/9.46  (p72 zenon_Vro)
% 9.14/9.46  (p41 zenon_Vwea)
% 9.14/9.46  (p114 zenon_Vn)
% 9.14/9.46  (p101 zenon_Vyi)
% 9.14/9.46  (p32 zenon_Voea)
% 9.14/9.46  (p72 zenon_Vdq)
% 9.14/9.46  (p14 zenon_X143)
% 9.14/9.46  (zenon_Vhha != zenon_Vtha)
% 9.14/9.46  (p93 zenon_Vem)
% 9.14/9.46  (p63 zenon_Vyy)
% 9.14/9.46  (p32 zenon_Vada)
% 9.14/9.46  (zenon_X160 != zenon_Vxha)
% 9.14/9.46  (p16 zenon_X142)
% 9.14/9.46  (zenon_Vzga != zenon_Vsha)
% 9.14/9.46  (p31 zenon_Vkga)
% 9.14/9.46  (p63 zenon_Vsy)
% 9.14/9.46  (p26 zenon_Vcfa)
% 9.14/9.46  (p21 zenon_Vlha)
% 9.14/9.46  (p83 zenon_Vbr)
% 9.14/9.46  (-. (p23 zenon_Vsha))
% 9.14/9.46  (p104 zenon_Via)
% 9.14/9.46  (p71 zenon_Vuw)
% 9.14/9.46  (p21 zenon_Vjha)
% 9.14/9.46  (p51 zenon_Vuca)
% 9.14/9.46  (zenon_Vtga != zenon_Vrha)
% 9.14/9.46  (p83 zenon_Vtq)
% 9.14/9.46  (p64 zenon_Vht)
% 9.14/9.46  (p92 zenon_Vkh)
% 9.14/9.46  (p105 zenon_Vwe)
% 9.14/9.46  (p51 zenon_Vpca)
% 9.14/9.46  (p65 zenon_Vkx)
% 9.14/9.46  (p42 zenon_Vsaa)
% 9.14/9.46  (p35 zenon_Vmfa)
% 9.14/9.46  (p96 zenon_Vjd)
% 9.14/9.46  (p66 zenon_Vbt)
% 9.14/9.46  (p76 zenon_Vko)
% 9.14/9.46  (r1 Tau_0 Tau_4)
% 9.14/9.46  (r1 zenon_Vwha zenon_Vpha)
% 9.14/9.46  (p23 zenon_Vbha)
% 9.14/9.46  (p104 zenon_Vmb)
% 9.14/9.46  (p72 zenon_Vpr)
% 9.14/9.46  (p25 zenon_Vtga)
% 9.14/9.46  (p14 zenon_X148)
% 9.14/9.46  (p63 zenon_Vmy)
% 9.14/9.46  (zenon_Vvga != zenon_Vpha)
% 9.14/9.46  (zenon_Vtga != zenon_Vpha)
% 9.14/9.46  (p22 zenon_Vvfa)
% 9.14/9.46  (p71 zenon_Vnw)
% 9.14/9.46  (p114 zenon_Vo)
% 9.14/9.46  (r1 Tau_3 zenon_Vyha)
% 9.14/9.46  (p105 zenon_Vme)
% 9.14/9.46  (p65 zenon_Vwx)
% 9.14/9.46  (p106 zenon_Vcb)
% 9.14/9.46  (-. (p11 zenon_Vzha))
% 9.14/9.46  (p11 zenon_X163)
% 9.14/9.46  (r1 Tau_1 zenon_Vwha)
% 9.14/9.46  (p32 zenon_Vwda)
% 9.14/9.46  (p82 zenon_Vwj)
% 9.14/9.46  (r1 Tau_4 zenon_Vzha)
% 9.14/9.46  (p85 zenon_Vpp)
% 9.14/9.46  (p106 zenon_Vgc)
% 9.14/9.46  (p34 zenon_Vlea)
% 9.14/9.46  (p44 zenon_Vkba)
% 9.14/9.46  (zenon_Vnha != zenon_Vtha)
% 9.14/9.46  (zenon_Vdha != zenon_Vvha)
% 9.14/9.46  (zenon_Vbha != zenon_Vvha)
% 9.14/9.46  (-. (p23 zenon_Vvha))
% 9.14/9.46  (r1 zenon_Vzha zenon_Vuha)
% 9.14/9.46  (p34 zenon_Vtda)
% 9.14/9.46  (r1 zenon_Vxha zenon_Vrha)
% 9.14/9.46  (p11 zenon_X164)
% 9.14/9.46  (p75 zenon_Vut)
% 9.14/9.46  (r1 Tau_0 Tau_3)
% 9.14/9.46  (p56 zenon_Vdz)
% 9.14/9.46  (zenon_Vvga != zenon_Vrha)
% 9.14/9.46  (p24 zenon_Vfga)
% 9.14/9.46  (p84 zenon_Vdn)
% 9.14/9.46  (p56 zenon_Vzw)
% 9.14/9.46  (p82 zenon_Vml)
% 9.14/9.46  (p43 zenon_Viea)
% 9.14/9.46  (r1 zenon_Vyha zenon_Vtha)
% 9.14/9.46  (p13 zenon_X160)
% 9.14/9.46  (p103 zenon_Vsg)
% 9.14/9.46  (zenon_Vdha != zenon_Vsha)
% 9.14/9.46  (p16 zenon_X147)
% 9.14/9.46  (p103 zenon_Vyf)
% 9.14/9.46  (p52 zenon_Vex)
% 9.14/9.46  (zenon_Vbha != zenon_Vqha)
% 9.14/9.46  (p101 zenon_Voi)
% 9.14/9.46  (p106 zenon_Vy)
% 9.14/9.46  (p84 zenon_Vel)
% 9.14/9.46  (-. (p15 zenon_Vwha))
% 9.14/9.46  (zenon_Vtga != zenon_Vuha)
% 9.14/9.46  (zenon_Vrga != zenon_Vpha)
% 9.14/9.46  (p62 zenon_Vnt)
% 9.14/9.46  (p22 zenon_Vgfa)
% 9.14/9.46  (p64 zenon_Vnu)
% 9.14/9.46  (p12 zenon_X162)
% 9.14/9.46  (p22 zenon_Vhga)
% 9.14/9.46  (zenon_Vvga != zenon_Vuha)
% 9.14/9.46  (p53 zenon_Vtba)
% 9.14/9.46  (zenon_Vzga != zenon_Vvha)
% 9.14/9.46  (r1 zenon_Vxha zenon_Vsha)
% 9.14/9.46  (p95 zenon_Vfk)
% 9.14/9.46  (p85 zenon_Vhp)
% 9.14/9.46  (p26 zenon_Vrfa)
% 9.14/9.46  (-. (p25 zenon_Vrha))
% 9.14/9.46  (p42 zenon_Vkca)
% 9.14/9.46  (p93 zenon_Vnm)
% 9.14/9.46  (p96 zenon_Vff)
% 9.14/9.46  (p61 zenon_Vaaa)
% 9.14/9.46  (zenon_Vbha != zenon_Vsha)
% 9.14/9.47  (zenon_X162 != zenon_Vyha)
% 9.14/9.47  *)
% 9.14/9.47  (* NO-PROOF *)
% 9.14/9.47  % SZS status GaveUp
% 9.14/9.47  Number of rewrites on terms: 0
% 9.14/9.47  Number of rewrites on props: 4
% 9.14/9.47  nodes searched: 1909
% 9.14/9.47  max branch formulas: 2064
% 9.14/9.47  proof nodes created: 19
% 9.14/9.47  formulas created: 14048
% 9.14/9.47  
%------------------------------------------------------------------------------