ZenonModulo---0.5.0.UNK-Non.f

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

% Computer : n026.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 41.63s 41.98s
% Output   : None 
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02  % Problem  : LCL682+1.015 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.02  % Command  : run_zenon_modulo %d %s
% 0.09/0.36  % Computer : n026.cluster.edu
% 0.09/0.36  % Model    : x86_64 x86_64
% 0.09/0.36  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36  % Memory   : 8046.5625MB
% 0.09/0.36  % OS       : Linux 6.8.0-71-generic
% 0.09/0.36  % CPULimit : 300
% 0.09/0.36  % WCLimit  : 300
% 0.09/0.36  % DateTime : Fri Sep  4 12:43:55 UTC 2026
% 0.09/0.36  % CPUTime  : 
% 41.63/41.98  Zenon error: exhausted search space without finding a proof
% 41.63/41.98  (* Current branch:
% 41.63/41.98  (p103 zenon_Vsla)
% 41.63/41.98  (p23 zenon_Vgmb)
% 41.63/41.98  (p95 zenon_Vfpa)
% 41.63/41.98  (p96 zenon_Vpka)
% 41.63/41.98  (p55 zenon_Vxfb)
% 41.63/41.98  (p141 zenon_Vum)
% 41.63/41.98  (p131 zenon_Vlu)
% 41.63/41.98  (p26 zenon_Vhkb)
% 41.63/41.98  (p21 zenon_Vqmb)
% 41.63/41.98  (p105 zenon_Vcja)
% 41.63/41.98  (p82 zenon_Vmqa)
% 41.63/41.98  (p81 zenon_Vvxa)
% 41.63/41.98  (r1 Tau_0 Tau_2)
% 41.63/41.98  (zenon_Vimb != zenon_Vanb)
% 41.63/41.98  (r1 Tau_2 zenon_Vcnb)
% 41.63/41.98  (p63 zenon_Vsdb)
% 41.63/41.98  (p94 zenon_Vsia)
% 41.63/41.98  (p93 zenon_Vera)
% 41.63/41.98  (p53 zenon_Vygb)
% 41.63/41.98  (p16 zenon_X207)
% 41.63/41.98  (p63 zenon_Vmdb)
% 41.63/41.98  (-. (p21 zenon_Vymb))
% 41.63/41.98  (-. (p15 zenon_Vbnb))
% 41.63/41.98  (zenon_Vgmb != zenon_Vxmb)
% 41.63/41.98  (zenon_X225 != zenon_Vcnb)
% 41.63/41.98  (p53 zenon_Vdhb)
% 41.63/41.98  (p13 zenon_X225)
% 41.63/41.98  (p83 zenon_Vjwa)
% 41.63/41.98  (zenon_Vmmb != zenon_Vymb)
% 41.63/41.98  (p143 zenon_Vek)
% 41.63/41.98  (p42 zenon_Vphb)
% 41.63/41.98  (p142 zenon_Vuc)
% 41.63/41.98  (p76 zenon_Vqwa)
% 41.63/41.98  (p145 zenon_Voh)
% 41.63/41.98  (zenon_Vamb != zenon_Vumb)
% 41.63/41.98  (p144 zenon_Vqa)
% 41.63/41.98  (p103 zenon_Vcma)
% 41.63/41.98  (p61 zenon_Vafb)
% 41.63/41.98  (p85 zenon_Vxua)
% 41.63/41.98  (p41 zenon_Vfkb)
% 41.63/41.98  (p91 zenon_Vdta)
% 41.63/41.98  (p83 zenon_Vbwa)
% 41.63/41.98  (p45 zenon_Vrib)
% 41.63/41.98  (p106 zenon_Vzba)
% 41.63/41.98  (r1 Tau_4 zenon_Venb)
% 41.63/41.98  (p73 zenon_Vhab)
% 41.63/41.98  (p22 zenon_Vmlb)
% 41.63/41.98  (-. (p23 zenon_Vanb))
% 41.63/41.98  (p82 zenon_Vcsa)
% 41.63/41.98  (zenon_Vimb != zenon_Vvmb)
% 41.63/41.98  (p101 zenon_Vena)
% 41.63/41.98  (-. (p11 zenon_Venb))
% 41.63/41.98  (zenon_X226 != zenon_Vcnb)
% 41.63/41.98  (p64 zenon_Vtab)
% 41.63/41.98  (p143 zenon_Vqj)
% 41.63/41.98  (p136 zenon_Vrk)
% 41.63/41.98  (p43 zenon_Vfjb)
% 41.63/41.98  (p24 zenon_Vykb)
% 41.63/41.98  (p34 zenon_Vcib)
% 41.63/41.98  (p31 zenon_Vplb)
% 41.63/41.98  (p136 zenon_Vxe)
% 41.63/41.98  (zenon_X229 != zenon_Venb)
% 41.63/41.98  (p52 zenon_Vgdb)
% 41.63/41.98  (p141 zenon_Vsl)
% 41.63/41.98  (p132 zenon_Vlt)
% 41.63/41.98  (zenon_Vomb != zenon_Vymb)
% 41.63/41.98  (p96 zenon_Vlma)
% 41.63/41.98  (p85 zenon_Vpua)
% 41.63/41.98  (zenon_Vemb != zenon_Vvmb)
% 41.63/41.98  (p36 zenon_Vokb)
% 41.63/41.98  (p44 zenon_Vofb)
% 41.63/41.98  (p46 zenon_Vkfb)
% 41.63/41.98  (p81 zenon_Vfxa)
% 41.63/41.98  (p66 zenon_Vnab)
% 41.63/41.98  (p45 zenon_Vvib)
% 41.63/41.98  (p112 zenon_Veha)
% 41.63/41.98  (p75 zenon_Vbza)
% 41.63/41.98  (p114 zenon_Vfaa)
% 41.63/41.98  (p32 zenon_Vtjb)
% 41.63/41.98  (p105 zenon_Vwja)
% 41.63/41.98  (p43 zenon_Vjjb)
% 41.63/41.98  (p34 zenon_Vyib)
% 41.63/41.98  (p86 zenon_Vgoa)
% 41.63/41.98  (p44 zenon_Vkgb)
% 41.63/41.98  (p154 zenon_Vo)
% 41.63/41.98  (p102 zenon_Vtca)
% 41.63/41.98  (p22 zenon_Vlkb)
% 41.63/41.98  (r1 zenon_Venb zenon_Vanb)
% 41.63/41.98  (p133 zenon_Vor)
% 41.63/41.98  (p41 zenon_Vbkb)
% 41.63/41.98  (p94 zenon_Vyka)
% 41.63/41.98  (p106 zenon_Vzfa)
% 41.63/41.98  (p114 zenon_Vhv)
% 41.63/41.98  (p56 zenon_Vzbb)
% 41.63/41.98  (-. (p12 zenon_Vdnb))
% 41.63/41.98  (p124 zenon_Vcq)
% 41.63/41.98  (p24 zenon_Vklb)
% 41.63/41.98  (p82 zenon_Vwoa)
% 41.63/41.98  (p26 zenon_Vwkb)
% 41.63/41.98  (p32 zenon_Vfib)
% 41.63/41.98  (p111 zenon_Vaia)
% 41.63/41.98  (r1 Tau_1 zenon_Vbnb)
% 41.63/41.98  (p35 zenon_Vukb)
% 41.63/41.98  (p66 zenon_Vhza)
% 41.63/41.98  (p124 zenon_Vms)
% 41.63/41.98  (p104 zenon_Vjca)
% 41.63/41.98  (p22 zenon_Valb)
% 41.63/41.98  (r1 Tau_0 Tau_1)
% 41.63/41.98  (p135 zenon_Vep)
% 41.63/41.98  (p33 zenon_Vglb)
% 41.63/41.98  (zenon_Vylb != zenon_Vumb)
% 41.63/41.98  (-. (p25 zenon_Vzmb))
% 41.63/41.98  (p146 zenon_Vid)
% 41.63/41.98  (p11 zenon_X228)
% 41.63/41.98  (p21 zenon_Vsmb)
% 41.63/41.98  (zenon_Vgmb != zenon_Vvmb)
% 41.63/41.98  (p56 zenon_Vjeb)
% 41.63/41.98  (p84 zenon_Vooa)
% 41.63/41.98  (p105 zenon_Vgka)
% 41.63/41.98  (p66 zenon_Vbya)
% 41.63/41.98  (p95 zenon_Vopa)
% 41.63/41.98  (p122 zenon_Voq)
% 41.63/41.98  (-. (p13 zenon_Vcnb))
% 41.63/41.98  (p123 zenon_Vjz)
% 41.63/41.98  (p21 zenon_Vmmb)
% 41.63/41.98  (p102 zenon_Vtea)
% 41.63/41.98  (p134 zenon_Vel)
% 41.63/41.98  (-. (p23 zenon_Vvmb))
% 41.63/41.98  (p146 zenon_Vsb)
% 41.63/41.98  (p123 zenon_Vly)
% 41.63/41.98  (r1 Tau_0 Tau_3)
% 41.63/41.98  (p102 zenon_Vtga)
% 41.63/41.98  (p45 zenon_Vjib)
% 41.63/41.98  (p11 zenon_X229)
% 41.63/41.98  (p126 zenon_Vgn)
% 41.63/41.98  (zenon_Vylb != zenon_Vwmb)
% 41.63/41.98  (p83 zenon_Vtva)
% 41.63/41.98  (p142 zenon_Veb)
% 41.63/41.98  (p152 zenon_Vp)
% 41.63/41.98  (-. (p25 zenon_Vumb))
% 41.63/41.98  (p16 zenon_X212)
% 41.63/41.98  (r1 zenon_Vbnb zenon_Vumb)
% 41.63/41.98  (zenon_Vamb != zenon_Vzmb)
% 41.63/41.98  (p131 zenon_Vyt)
% 41.63/41.98  (p61 zenon_Vgfb)
% 41.63/41.98  (zenon_Vemb != zenon_Vxmb)
% 41.63/41.98  (p65 zenon_Vkcb)
% 41.63/41.98  (-. (p25 zenon_Vwmb))
% 41.63/41.98  (p85 zenon_Vzta)
% 41.63/41.98  (zenon_Vgmb != zenon_Vanb)
% 41.63/41.98  (p106 zenon_Vzda)
% 41.63/41.98  (p62 zenon_Vtza)
% 41.63/41.98  (p33 zenon_Vdlb)
% 41.63/41.98  (p71 zenon_Vnbb)
% 41.63/41.98  (zenon_X227 != zenon_Vdnb)
% 41.63/41.98  (p133 zenon_Vbr)
% 41.63/41.98  (p103 zenon_Vila)
% 41.63/41.98  (p61 zenon_Vueb)
% 41.63/41.98  (p51 zenon_Vzhb)
% 41.63/41.98  (p84 zenon_Veqa)
% 41.63/41.98  (p113 zenon_Vefa)
% 41.63/41.98  (p72 zenon_Vgbb)
% 41.63/41.98  (-. (p23 zenon_Vxmb))
% 41.63/41.98  (p64 zenon_Vnza)
% 41.63/41.98  (p24 zenon_Vjkb)
% 41.63/41.98  (p104 zenon_Vjga)
% 41.63/41.98  (p35 zenon_Vrkb)
% 41.63/41.98  (zenon_Vqmb != zenon_Vymb)
% 41.63/41.98  (p55 zenon_Vcgb)
% 41.63/41.98  (zenon_Vsmb != zenon_Vymb)
% 41.63/41.98  (p124 zenon_Vsn)
% 41.63/41.98  (p123 zenon_Vxy)
% 41.63/41.98  (p85 zenon_Vhua)
% 41.63/41.98  (p126 zenon_Vas)
% 41.63/41.98  (p73 zenon_Vaab)
% 41.63/41.98  (p86 zenon_Vwpa)
% 41.63/41.98  (p56 zenon_Vbdb)
% 41.63/41.98  (p76 zenon_Veva)
% 41.63/41.98  (p125 zenon_Vtv)
% 41.63/41.98  (p121 zenon_Vdba)
% 41.63/41.98  (p76 zenon_Vkta)
% 41.63/41.98  (zenon_Vylb != zenon_Vzmb)
% 41.63/41.98  (p144 zenon_Vgc)
% 41.63/41.98  (p141 zenon_Vgm)
% 41.63/41.98  (p46 zenon_Vhhb)
% 41.63/41.98  (p43 zenon_Vnjb)
% 41.63/41.98  (p62 zenon_Vnya)
% 41.63/41.98  (p125 zenon_Vrw)
% 41.63/41.98  (p71 zenon_Vubb)
% 41.63/41.98  (p25 zenon_Vamb)
% 41.63/41.98  (p125 zenon_Vfw)
% 41.63/41.98  (p63 zenon_Vydb)
% 41.63/41.98  (p42 zenon_Vsfb)
% 41.63/41.98  (p41 zenon_Vxjb)
% 41.63/41.98  (p94 zenon_Vuma)
% 41.63/41.98  (p14 zenon_X213)
% 41.63/41.98  (p115 zenon_Vpda)
% 41.63/41.98  (p31 zenon_Vslb)
% 41.63/41.98  (zenon_X223 != zenon_Vbnb)
% 41.63/41.98  (r1 zenon_Vcnb zenon_Vxmb)
% 41.63/41.98  (p101 zenon_Vyna)
% 41.63/41.98  (zenon_Vemb != zenon_Vanb)
% 41.63/41.98  (p15 zenon_X223)
% 41.63/41.98  (p111 zenon_Vpha)
% 41.63/41.98  (zenon_Vimb != zenon_Vxmb)
% 41.63/41.98  (p51 zenon_Vuhb)
% 41.63/41.98  (p143 zenon_Vcj)
% 41.63/41.98  (zenon_Vwlb != zenon_Vwmb)
% 41.63/41.98  (p74 zenon_Vlva)
% 41.63/41.98  (p96 zenon_Vjia)
% 41.63/41.98  (p63 zenon_Veeb)
% 41.63/41.98  (p25 zenon_Vylb)
% 41.63/41.98  (p101 zenon_Vona)
% 41.63/41.98  (p104 zenon_Vjea)
% 41.63/41.98  (p74 zenon_Vxwa)
% 41.63/41.98  (p62 zenon_Vzab)
% 41.63/41.98  (p115 zenon_Veda)
% 41.63/41.98  (r1 zenon_Vcnb zenon_Vwmb)
% 41.63/41.98  (p116 zenon_Vwu)
% 41.63/41.98  (p34 zenon_Vqjb)
% 41.63/41.98  (p64 zenon_Vhya)
% 41.63/41.98  (p44 zenon_Vlhb)
% 41.63/41.98  (r1 zenon_Venb zenon_Vzmb)
% 41.63/41.98  (p134 zenon_Vkf)
% 41.63/41.98  (p113 zenon_Vpfa)
% 41.63/41.98  (p65 zenon_Vqcb)
% 41.63/41.98  (p23 zenon_Vemb)
% 41.63/41.98  (p12 zenon_X227)
% 41.63/41.98  (p45 zenon_Vnib)
% 41.63/41.98  (p14 zenon_X208)
% 41.63/41.98  (zenon_Vamb != zenon_Vwmb)
% 41.63/41.98  (p105 zenon_Vmja)
% 41.63/41.98  (r1 Tau_3 zenon_Vdnb)
% 41.63/41.98  (p91 zenon_Vusa)
% 41.63/41.98  (p81 zenon_Vnxa)
% 41.63/41.98  (p145 zenon_Vah)
% 41.63/41.98  (p136 zenon_Vbi)
% 41.63/41.98  (p75 zenon_Vuya)
% 41.63/41.98  (p23 zenon_Vimb)
% 41.63/41.98  (p14 zenon_X218)
% 41.63/41.98  (zenon_X228 != zenon_Venb)
% 41.63/41.98  (r1 zenon_Vdnb zenon_Vymb)
% 41.63/41.98  (zenon_Vwlb != zenon_Vzmb)
% 41.63/41.98  (p145 zenon_Vmg)
% 41.63/41.98  (p65 zenon_Vwcb)
% 41.63/41.98  (p52 zenon_Voeb)
% 41.63/41.98  (p152 zenon_Vn)
% 41.63/41.98  (p93 zenon_Vvqa)
% 41.63/41.98  (p74 zenon_Vrta)
% 41.63/41.98  (r1 Tau_0 Tau_4)
% 41.63/41.98  (p122 zenon_Veo)
% 41.63/41.98  (p84 zenon_Vura)
% 41.63/41.98  (p21 zenon_Vomb)
% 41.63/41.98  (p121 zenon_Vpba)
% 41.63/41.98  (p42 zenon_Vogb)
% 41.63/41.98  (p122 zenon_Vys)
% 41.63/41.98  (p26 zenon_Vilb)
% 41.63/41.98  (p114 zenon_Vzx)
% 41.63/41.98  (p121 zenon_Vraa)
% 41.63/41.98  (p92 zenon_Vlsa)
% 41.63/41.98  (zenon_X224 != zenon_Vbnb)
% 41.63/41.98  (p142 zenon_Vke)
% 41.63/41.98  (p145 zenon_Vyf)
% 41.63/41.98  (p135 zenon_Vro)
% 41.63/41.98  (p144 zenon_Vwd)
% 41.63/41.98  (p54 zenon_Vtgb)
% 41.63/41.98  (p126 zenon_Vqp)
% 41.63/41.98  (p32 zenon_Vbjb)
% 41.63/41.98  (r1 zenon_Vbnb zenon_Vvmb)
% 41.63/41.98  (p116 zenon_Vox)
% 41.63/41.98  (p46 zenon_Vggb)
% 41.63/41.98  (p16 zenon_X217)
% 41.63/41.98  (zenon_Vwlb != zenon_Vumb)
% 41.63/41.98  (p156 zenon_Vm)
% 41.63/41.98  (p86 zenon_Vmra)
% 41.63/41.98  (p146 zenon_Vca)
% 41.63/41.98  (p15 zenon_X224)
% 41.63/41.98  (p125 zenon_Vdx)
% 41.63/41.98  (p52 zenon_Vecb)
% 41.63/41.98  (p134 zenon_Voi)
% 41.63/41.98  (p116 zenon_Vuz)
% 41.63/41.98  (p25 zenon_Vwlb)
% 41.63/41.98  (p13 zenon_X226)
% 41.63/41.98  *)
% 41.63/41.98  (* NO-PROOF *)
% 41.63/41.98  % SZS status GaveUp
% 41.63/41.98  Number of rewrites on terms: 0
% 41.63/41.98  Number of rewrites on props: 4
% 41.63/41.98  nodes searched: 3531
% 41.63/41.98  max branch formulas: 3751
% 41.63/41.98  proof nodes created: 19
% 41.63/41.98  formulas created: 23868
% 41.63/41.98  
%------------------------------------------------------------------------------