↑ 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.015 : TPTP v9.3.1. Released v4.0.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : run_zenon_modulo %d %s

% Computer : n011.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 131.93s 132.23s
% Output   : None 
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02  % Problem  : LCL683+1.015 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.02  % Command  : run_zenon_modulo %d %s
% 0.07/0.34  % Computer : n011.cluster.edu
% 0.07/0.34  % Model    : x86_64 x86_64
% 0.07/0.34  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.34  % Memory   : 8046.5625MB
% 0.07/0.34  % OS       : Linux 6.8.0-71-generic
% 0.07/0.34  % CPULimit : 300
% 0.07/0.34  % WCLimit  : 300
% 0.07/0.34  % DateTime : Sat Sep  5 17:23:58 UTC 2026
% 0.07/0.34  % CPUTime  : 
% 131.93/132.22  Zenon error: exhausted search space without finding a proof
% 131.93/132.22  (* Current branch:
% 131.93/132.22  (r1 Tau_0 Tau_4)
% 131.93/132.22  (p102 zenon_Vgma)
% 131.93/132.22  (r1 Tau_3 zenon_Viub)
% 131.93/132.22  (p113 zenon_Vcna)
% 131.93/132.22  (-. (p23 zenon_Vaub))
% 131.93/132.22  (p121 zenon_Vcja)
% 131.93/132.22  (p92 zenon_Vxta)
% 131.93/132.22  (p63 zenon_Vxkb)
% 131.93/132.22  (zenon_Vttb != zenon_Vdub)
% 131.93/132.22  (p62 zenon_Vygb)
% 131.93/132.22  (p106 zenon_Vmja)
% 131.93/132.22  (p25 zenon_Vftb)
% 131.93/132.22  (p22 zenon_Vrsb)
% 131.93/132.22  (zenon_Vvtb != zenon_Vdub)
% 131.93/132.22  (p76 zenon_Vvdb)
% 131.93/132.22  (zenon_Vjtb != zenon_Vfub)
% 131.93/132.22  (p146 zenon_Vig)
% 131.93/132.22  (zenon_X236 != zenon_Vgub)
% 131.93/132.22  (-. (p21 zenon_Vdub))
% 131.93/132.22  (p42 zenon_Vtnb)
% 131.93/132.22  (zenon_X239 != zenon_Viub)
% 131.93/132.22  (p161 zenon_Vn)
% 131.93/132.22  (p141 zenon_Vhu)
% 131.93/132.22  (p21 zenon_Vrtb)
% 131.93/132.22  (p23 zenon_Vjtb)
% 131.93/132.22  (r1 zenon_Vgub zenon_Vaub)
% 131.93/132.22  (p121 zenon_Vsha)
% 131.93/132.22  (p116 zenon_Vpea)
% 131.93/132.22  (p94 zenon_Viya)
% 131.93/132.22  (p122 zenon_Vrv)
% 131.93/132.22  (p41 zenon_Vgrb)
% 131.93/132.22  (p95 zenon_Vswa)
% 131.93/132.22  (p85 zenon_Vccb)
% 131.93/132.22  (zenon_Vbtb != zenon_Vbub)
% 131.93/132.22  (p124 zenon_Vmaa)
% 131.93/132.22  (p16 zenon_X229)
% 131.93/132.22  (zenon_X235 != zenon_Vgub)
% 131.93/132.22  (-. (p23 zenon_Vcub))
% 131.93/132.22  (p61 zenon_Vzlb)
% 131.93/132.22  (r1 zenon_Vjub zenon_Veub)
% 131.93/132.22  (p52 zenon_Vjjb)
% 131.93/132.22  (p101 zenon_Vrua)
% 131.93/132.22  (p121 zenon_Veia)
% 131.93/132.22  (p24 zenon_Vdsb)
% 131.93/132.22  (zenon_Vjtb != zenon_Vcub)
% 131.93/132.22  (r1 zenon_Vhub zenon_Vcub)
% 131.93/132.22  (p34 zenon_Vhpb)
% 131.93/132.22  (p56 zenon_Vgkb)
% 131.93/132.22  (zenon_Vntb != zenon_Vaub)
% 131.93/132.22  (p65 zenon_Vpjb)
% 131.93/132.22  (p151 zenon_Vxl)
% 131.93/132.22  (p83 zenon_Vgdb)
% 131.93/132.22  (p123 zenon_Vyfa)
% 131.93/132.22  (p91 zenon_Vhab)
% 131.93/132.22  (p74 zenon_Vceb)
% 131.93/132.22  (zenon_X241 != zenon_Vjub)
% 131.93/132.22  (p82 zenon_Vyza)
% 131.93/132.22  (p144 zenon_Vfk)
% 131.93/132.22  (p123 zenon_Vmfa)
% 131.93/132.22  (p55 zenon_Vhnb)
% 131.93/132.22  (p72 zenon_Vlib)
% 131.93/132.22  (p24 zenon_Vorb)
% 131.93/132.22  (p14 zenon_X230)
% 131.93/132.22  (p153 zenon_Voi)
% 131.93/132.22  (p93 zenon_Vrya)
% 131.93/132.22  (p61 zenon_Vlmb)
% 131.93/132.22  (p66 zenon_Vmgb)
% 131.93/132.22  (p66 zenon_Vshb)
% 131.93/132.22  (p105 zenon_Vpqa)
% 131.93/132.22  (p35 zenon_Vzrb)
% 131.93/132.22  (p22 zenon_Vqrb)
% 131.93/132.22  (p144 zenon_Vwg)
% 131.93/132.22  (-. (p11 zenon_Vjub))
% 131.93/132.22  (p132 zenon_Vxm)
% 131.93/132.22  (p81 zenon_Vseb)
% 131.93/132.22  (p76 zenon_Vxab)
% 131.93/132.22  (zenon_Vftb != zenon_Veub)
% 131.93/132.22  (p123 zenon_Vkga)
% 131.93/132.22  (p46 zenon_Vmob)
% 131.93/132.22  (p35 zenon_Vwrb)
% 131.93/132.22  (zenon_Vrtb != zenon_Vdub)
% 131.93/132.22  (p104 zenon_Vhoa)
% 131.93/132.22  (p93 zenon_Vaza)
% 131.93/132.22  (p112 zenon_Vuca)
% 131.93/132.22  (p66 zenon_Vgfb)
% 131.93/132.22  (p52 zenon_Vlkb)
% 131.93/132.22  (p82 zenon_Vzxa)
% 131.93/132.22  (p126 zenon_Vtu)
% 131.93/132.22  (p141 zenon_Vft)
% 131.93/132.22  (p76 zenon_Vjcb)
% 131.93/132.22  (p101 zenon_Vhua)
% 131.93/132.22  (p16 zenon_X224)
% 131.93/132.22  (zenon_Vdtb != zenon_Veub)
% 131.93/132.22  (p121 zenon_Vqia)
% 131.93/132.22  (p63 zenon_Vrkb)
% 131.93/132.22  (zenon_Vdtb != zenon_Vztb)
% 131.93/132.22  (p26 zenon_Vmrb)
% 131.93/132.22  (p96 zenon_Vota)
% 131.93/132.22  (-. (p25 zenon_Veub))
% 131.93/132.22  (p82 zenon_Vjwa)
% 131.93/132.22  (zenon_Vdtb != zenon_Vbub)
% 131.93/132.22  (zenon_Vltb != zenon_Vfub)
% 131.93/132.22  (p122 zenon_Vby)
% 131.93/132.22  (p15 zenon_X236)
% 131.93/132.22  (-. (p13 zenon_Vhub))
% 131.93/132.22  (zenon_Vltb != zenon_Vcub)
% 131.93/132.22  (r1 zenon_Vhub zenon_Vbub)
% 131.93/132.22  (p26 zenon_Vnsb)
% 131.93/132.22  (zenon_Vbtb != zenon_Veub)
% 131.93/132.22  (p65 zenon_Vbkb)
% 131.93/132.22  (p154 zenon_Vzh)
% 131.93/132.22  (p142 zenon_Vkh)
% 131.93/132.22  (-. (p12 zenon_Viub))
% 131.93/132.22  (p44 zenon_Vqob)
% 131.93/132.22  (p164 zenon_Vo)
% 131.93/132.22  (p125 zenon_Veea)
% 131.93/132.22  (p64 zenon_Vmfb)
% 131.93/132.22  (p45 zenon_Vopb)
% 131.93/132.22  (p84 zenon_Vbwa)
% 131.93/132.22  (p166 zenon_Vm)
% 131.93/132.22  (p105 zenon_Vzqa)
% 131.93/132.22  (p15 zenon_X235)
% 131.93/132.22  (p143 zenon_Vpq)
% 131.93/132.22  (p81 zenon_Vafb)
% 131.93/132.22  (zenon_Vftb != zenon_Vbub)
% 131.93/132.22  (p44 zenon_Vtmb)
% 131.93/132.22  (p144 zenon_Vce)
% 131.93/132.22  (r1 Tau_2 zenon_Vhub)
% 131.93/132.22  (p26 zenon_Vbsb)
% 131.93/132.22  (p131 zenon_Vlba)
% 131.93/132.22  (p136 zenon_Vap)
% 131.93/132.22  (zenon_Vntb != zenon_Vfub)
% 131.93/132.22  (zenon_X238 != zenon_Vhub)
% 131.93/132.22  (p41 zenon_Vcrb)
% 131.93/132.22  (p73 zenon_Vfhb)
% 131.93/132.22  (p135 zenon_Vrw)
% 131.93/132.22  (r1 Tau_4 zenon_Vjub)
% 131.93/132.22  (p81 zenon_Vkeb)
% 131.93/132.22  (p143 zenon_Vbq)
% 131.93/132.22  (p142 zenon_Vqe)
% 131.93/132.22  (p124 zenon_Vfv)
% 131.93/132.22  (p92 zenon_Vbsa)
% 131.93/132.22  (p134 zenon_Voy)
% 131.93/132.22  (p101 zenon_Vbva)
% 131.93/132.22  (p46 zenon_Vlnb)
% 131.93/132.22  (-. (p25 zenon_Vbub))
% 131.93/132.22  (p36 zenon_Vtrb)
% 131.93/132.22  (p24 zenon_Vpsb)
% 131.93/132.22  (p56 zenon_Vejb)
% 131.93/132.22  (r1 zenon_Vgub zenon_Vztb)
% 131.93/132.22  (p74 zenon_Vqcb)
% 131.93/132.22  (zenon_Vftb != zenon_Vztb)
% 131.93/132.22  (p34 zenon_Vvqb)
% 131.93/132.22  (p145 zenon_Vln)
% 131.93/132.22  (p25 zenon_Vdtb)
% 131.93/132.22  (zenon_X237 != zenon_Vhub)
% 131.93/132.22  (p125 zenon_Vgda)
% 131.93/132.22  (p141 zenon_Vrs)
% 131.93/132.22  (zenon_Vltb != zenon_Vaub)
% 131.93/132.22  (p85 zenon_Vmbb)
% 131.93/132.22  (p53 zenon_Viob)
% 131.93/132.22  (p102 zenon_Vroa)
% 131.93/132.22  (p102 zenon_Vgka)
% 131.93/132.22  (p132 zenon_Vds)
% 131.93/132.22  (p71 zenon_Vzib)
% 131.93/132.22  (p103 zenon_Vvsa)
% 131.93/132.22  (p51 zenon_Vzob)
% 131.93/132.22  (p145 zenon_Vzn)
% 131.93/132.22  (p32 zenon_Vgqb)
% 131.93/132.22  (p32 zenon_Vyqb)
% 131.93/132.22  (p61 zenon_Vfmb)
% 131.93/132.22  (p111 zenon_Vnpa)
% 131.93/132.22  (p96 zenon_Vwpa)
% 131.93/132.22  (p23 zenon_Vntb)
% 131.93/132.22  (p156 zenon_Vhb)
% 131.93/132.22  (p116 zenon_Vvga)
% 131.93/132.22  (p43 zenon_Vsqb)
% 131.93/132.22  (p116 zenon_Vjca)
% 131.93/132.22  (p43 zenon_Voqb)
% 131.93/132.22  (p21 zenon_Vvtb)
% 131.93/132.22  (zenon_Vjtb != zenon_Vaub)
% 131.93/132.22  (p131 zenon_Vyba)
% 131.93/132.22  (p106 zenon_Vmla)
% 131.93/132.22  (p45 zenon_Vaqb)
% 131.93/132.22  (p12 zenon_X239)
% 131.93/132.22  (p21 zenon_Vttb)
% 131.93/132.22  (-. (p15 zenon_Vgub))
% 131.93/132.22  (p101 zenon_Vlva)
% 131.93/132.22  (p162 zenon_Vp)
% 131.93/132.22  (p84 zenon_Vqza)
% 131.93/132.22  (r1 Tau_0 Tau_2)
% 131.93/132.22  (p74 zenon_Vebb)
% 131.93/132.22  (p55 zenon_Vcnb)
% 131.93/132.22  (p113 zenon_Vnna)
% 131.93/132.22  (p152 zenon_Vwb)
% 131.93/132.22  (p14 zenon_X225)
% 131.93/132.22  (p95 zenon_Vbxa)
% 131.93/132.22  (p73 zenon_Vmhb)
% 131.93/132.22  (p112 zenon_Vgha)
% 131.93/132.22  (p156 zenon_Vlc)
% 131.93/132.22  (p13 zenon_X237)
% 131.93/132.22  (p62 zenon_Vsfb)
% 131.93/132.22  (p45 zenon_Vwpb)
% 131.93/132.22  (p64 zenon_Vsgb)
% 131.93/132.22  (r1 zenon_Viub zenon_Vdub)
% 131.93/132.22  (p11 zenon_X241)
% 131.93/132.22  (p83 zenon_Vodb)
% 131.93/132.22  (p115 zenon_Vcla)
% 131.93/132.22  (p64 zenon_Vyhb)
% 131.93/132.22  (p84 zenon_Vrxa)
% 131.93/132.22  (p156 zenon_Vda)
% 131.93/132.22  (r1 Tau_0 Tau_1)
% 131.93/132.22  (p75 zenon_Vzfb)
% 131.93/132.23  (p152 zenon_Vad)
% 131.93/132.23  (p13 zenon_X238)
% 131.93/132.23  (r1 Tau_1 zenon_Vgub)
% 131.93/132.23  (r1 Tau_0 Tau_3)
% 131.93/132.23  (p23 zenon_Vltb)
% 131.93/132.23  (p86 zenon_Vjxa)
% 131.93/132.23  (p136 zenon_Vqr)
% 131.93/132.23  (zenon_X240 != zenon_Vjub)
% 131.93/132.23  (p25 zenon_Vbtb)
% 131.93/132.23  (p126 zenon_Vdx)
% 131.93/132.23  (p63 zenon_Vdlb)
% 131.93/132.23  (p104 zenon_Vwja)
% 131.93/132.23  (p53 zenon_Vdob)
% 131.93/132.23  (p155 zenon_Vuf)
% 131.93/132.23  (p145 zenon_Vno)
% 131.93/132.23  (p31 zenon_Vxsb)
% 131.93/132.23  (p41 zenon_Vkrb)
% 131.93/132.23  (p33 zenon_Vlsb)
% 131.93/132.23  (p86 zenon_Viza)
% 131.93/132.23  (p133 zenon_Voz)
% 131.93/132.23  (p63 zenon_Vjlb)
% 131.93/132.23  (p83 zenon_Vycb)
% 131.93/132.23  (zenon_Vntb != zenon_Vcub)
% 131.93/132.23  (p136 zenon_Vkm)
% 131.93/132.23  (r1 zenon_Vjub zenon_Vfub)
% 131.93/132.23  (p143 zenon_Vdr)
% 131.93/132.23  (p85 zenon_Vubb)
% 131.93/132.23  (p106 zenon_Vxna)
% 131.93/132.23  (p54 zenon_Vynb)
% 131.93/132.23  (zenon_Vxtb != zenon_Vdub)
% 131.93/132.23  (p126 zenon_Vaaa)
% 131.93/132.23  (-. (p25 zenon_Vztb))
% 131.93/132.23  (p51 zenon_Vepb)
% 131.93/132.23  (p92 zenon_Vfqa)
% 131.93/132.23  (p124 zenon_Vpx)
% 131.93/132.23  (p146 zenon_Vod)
% 131.93/132.23  (p71 zenon_Vsib)
% 131.93/132.23  (p42 zenon_Vxmb)
% 131.93/132.23  (p22 zenon_Vfsb)
% 131.93/132.23  (p42 zenon_Vuob)
% 131.93/132.23  (p14 zenon_X220)
% 131.93/132.23  (p146 zenon_Vrj)
% 131.93/132.23  (p104 zenon_Vwla)
% 131.93/132.23  (p141 zenon_Vtt)
% 131.93/132.23  (p152 zenon_Vsa)
% 131.93/132.23  (p142 zenon_Vtk)
% 131.93/132.23  (p153 zenon_Vdj)
% 131.93/132.23  (p16 zenon_X219)
% 131.93/132.23  (p56 zenon_Volb)
% 131.93/132.23  (p155 zenon_Vff)
% 131.93/132.23  (p103 zenon_Vfta)
% 131.93/132.23  (p133 zenon_Vbz)
% 131.93/132.23  (p115 zenon_Vrka)
% 131.93/132.23  (p62 zenon_Veib)
% 131.93/132.23  (p44 zenon_Vpnb)
% 131.93/132.23  (p65 zenon_Vvjb)
% 131.93/132.23  (p31 zenon_Vusb)
% 131.93/132.23  (p96 zenon_Vsra)
% 131.93/132.23  (p11 zenon_X240)
% 131.93/132.23  (p45 zenon_Vspb)
% 131.93/132.23  (p103 zenon_Vlsa)
% 131.93/132.23  (p135 zenon_Vew)
% 131.93/132.23  (p33 zenon_Visb)
% 131.93/132.23  (p52 zenon_Vtlb)
% 131.93/132.23  (p91 zenon_Vqab)
% 131.93/132.23  (p21 zenon_Vxtb)
% 131.93/132.23  (p86 zenon_Vtva)
% 131.93/132.23  (p111 zenon_Vcpa)
% 131.93/132.23  (p46 zenon_Vpmb)
% 131.93/132.23  (p151 zenon_Vil)
% 131.93/132.23  (p43 zenon_Vkqb)
% 131.93/132.23  (p34 zenon_Vdqb)
% 131.93/132.23  (p75 zenon_Vggb)
% 131.93/132.23  (p105 zenon_Vjra)
% 131.93/132.23  (-. (p23 zenon_Vfub))
% 131.93/132.23  (zenon_Vbtb != zenon_Vztb)
% 131.93/132.23  (p122 zenon_Vyaa)
% 131.93/132.23  (p112 zenon_Vafa)
% 131.93/132.23  (p132 zenon_Vnp)
% 131.93/132.23  (p32 zenon_Vkpb)
% 131.93/132.23  (p114 zenon_Vrma)
% 131.93/132.23  (p125 zenon_Vsda)
% 131.93/132.23  *)
% 131.93/132.23  (* NO-PROOF *)
% 131.93/132.23  % SZS status GaveUp
% 131.93/132.23  Number of rewrites on terms: 0
% 131.93/132.23  Number of rewrites on props: 4
% 131.93/132.23  nodes searched: 3905
% 131.93/132.23  max branch formulas: 4137
% 131.93/132.23  proof nodes created: 19
% 131.93/132.23  formulas created: 26053
% 131.93/132.23  
%------------------------------------------------------------------------------