↑ Up

ZenonModulo---0.5.0.UNK-Non.f

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

% Computer : n020.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 13.44s 13.77s
% Output   : None 
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : LCL682+1.010 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03  % Command  : run_zenon_modulo %d %s
% 0.08/0.34  % Computer : n020.cluster.edu
% 0.08/0.34  % Model    : x86_64 x86_64
% 0.08/0.34  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34  % Memory   : 8046.5625MB
% 0.08/0.34  % OS       : Linux 6.8.0-71-generic
% 0.08/0.34  % CPULimit : 300
% 0.08/0.34  % WCLimit  : 300
% 0.08/0.34  % DateTime : Sat Sep  5 06:27:42 UTC 2026
% 0.08/0.35  % CPUTime  : 
% 13.44/13.76  Zenon error: exhausted search space without finding a proof
% 13.44/13.76  (* Current branch:
% 13.44/13.76  (p25 zenon_Vsz)
% 13.44/13.76  (r1 zenon_Vvaa zenon_Vqaa)
% 13.44/13.76  (-. (p25 zenon_Vmaa))
% 13.44/13.76  (p75 zenon_Vtm)
% 13.44/13.76  (p64 zenon_Vfn)
% 13.44/13.76  (r1 zenon_Vtaa zenon_Vmaa)
% 13.44/13.76  (p84 zenon_Vvf)
% 13.44/13.76  (p92 zenon_Vya)
% 13.44/13.76  (-. (p25 zenon_Vraa))
% 13.44/13.76  (p73 zenon_Vgo)
% 13.44/13.76  (p81 zenon_Vpk)
% 13.44/13.76  (p82 zenon_Voc)
% 13.44/13.76  (p85 zenon_Vrh)
% 13.44/13.76  (p43 zenon_Vbx)
% 13.44/13.76  (p21 zenon_Vgaa)
% 13.44/13.76  (r1 Tau_0 Tau_2)
% 13.44/13.76  (p42 zenon_Vkt)
% 13.44/13.76  (r1 zenon_Vwaa zenon_Vraa)
% 13.44/13.76  (p81 zenon_Vxk)
% 13.44/13.76  (p93 zenon_Vwe)
% 13.44/13.76  (p75 zenon_Vmm)
% 13.44/13.76  (r1 zenon_Vwaa zenon_Vsaa)
% 13.44/13.76  (-. (p23 zenon_Vnaa))
% 13.44/13.76  (p44 zenon_Vgt)
% 13.44/13.76  (zenon_Vgaa != zenon_Vqaa)
% 13.44/13.76  (p22 zenon_Vez)
% 13.44/13.76  (zenon_X143 != zenon_Vuaa)
% 13.44/13.76  (p55 zenon_Vut)
% 13.44/13.76  (zenon_Voz != zenon_Voaa)
% 13.44/13.76  (-. (p21 zenon_Vqaa))
% 13.44/13.76  (p51 zenon_Vrv)
% 13.44/13.76  (p35 zenon_Vjy)
% 13.44/13.76  (p26 zenon_Voy)
% 13.44/13.76  (p82 zenon_Vdg)
% 13.44/13.76  (zenon_X140 != zenon_Vtaa)
% 13.44/13.76  (p21 zenon_Veaa)
% 13.44/13.76  (-. (p23 zenon_Vsaa))
% 13.44/13.76  (p71 zenon_Vfp)
% 13.44/13.76  (p11 zenon_X146)
% 13.44/13.76  (r1 zenon_Vtaa zenon_Vnaa)
% 13.44/13.76  (p71 zenon_Vmp)
% 13.44/13.76  (p41 zenon_Vtx)
% 13.44/13.76  (p23 zenon_Vaaa)
% 13.44/13.76  (r1 Tau_0 Tau_3)
% 13.44/13.76  (zenon_Vkaa != zenon_Vqaa)
% 13.44/13.76  (p93 zenon_Vff)
% 13.44/13.76  (zenon_Vaaa != zenon_Vnaa)
% 13.44/13.76  (p86 zenon_Vyb)
% 13.44/13.76  (p32 zenon_Vxv)
% 13.44/13.76  (p13 zenon_X142)
% 13.44/13.77  (p92 zenon_Vqb)
% 13.44/13.77  (p45 zenon_Vfw)
% 13.44/13.77  (zenon_Vwz != zenon_Vnaa)
% 13.44/13.77  (p65 zenon_Voq)
% 13.44/13.77  (p84 zenon_Vgc)
% 13.44/13.77  (p83 zenon_Vlj)
% 13.44/13.77  (p62 zenon_Vyo)
% 13.44/13.77  (p61 zenon_Vys)
% 13.44/13.77  (p72 zenon_Vhk)
% 13.44/13.77  (p15 zenon_X140)
% 13.44/13.77  (p14 zenon_X130)
% 13.44/13.77  (r1 Tau_3 zenon_Vvaa)
% 13.44/13.77  (p46 zenon_Vct)
% 13.44/13.77  (p65 zenon_Viq)
% 13.44/13.77  (zenon_Voz != zenon_Vraa)
% 13.44/13.77  (p64 zenon_Vso)
% 13.44/13.77  (p25 zenon_Voz)
% 13.44/13.77  (zenon_Vqz != zenon_Vmaa)
% 13.44/13.77  (p31 zenon_Vkz)
% 13.44/13.77  (p55 zenon_Vpt)
% 13.44/13.77  (p36 zenon_Vgy)
% 13.44/13.77  (p66 zenon_Vtl)
% 13.44/13.77  (p41 zenon_Vpx)
% 13.44/13.77  (p72 zenon_Vvi)
% 13.44/13.77  (zenon_Vaaa != zenon_Vpaa)
% 13.44/13.77  (p15 zenon_X141)
% 13.44/13.77  (p42 zenon_Vgu)
% 13.44/13.77  (p51 zenon_Vmv)
% 13.44/13.77  (zenon_X145 != zenon_Vwaa)
% 13.44/13.77  (p52 zenon_Vas)
% 13.44/13.77  (p42 zenon_Vhv)
% 13.44/13.77  (p26 zenon_Vaz)
% 13.44/13.77  (r1 zenon_Vuaa zenon_Vpaa)
% 13.44/13.77  (p26 zenon_Vzx)
% 13.44/13.77  (r1 Tau_0 Tau_1)
% 13.44/13.77  (zenon_X146 != zenon_Vwaa)
% 13.44/13.77  (p95 zenon_Vgd)
% 13.44/13.77  (p52 zenon_Vwp)
% 13.44/13.77  (p63 zenon_Vqr)
% 13.44/13.77  (p16 zenon_X124)
% 13.44/13.77  (p76 zenon_Voi)
% 13.44/13.77  (p23 zenon_Vyz)
% 13.44/13.77  (p23 zenon_Vwz)
% 13.44/13.77  (zenon_X142 != zenon_Vuaa)
% 13.44/13.77  (p63 zenon_Vkr)
% 13.44/13.77  (-. (p13 zenon_Vuaa))
% 13.44/13.77  (p84 zenon_Vwd)
% 13.44/13.77  (r1 zenon_Vuaa zenon_Voaa)
% 13.44/13.77  (p74 zenon_Vsn)
% 13.44/13.77  (p33 zenon_Vyy)
% 13.44/13.77  (p73 zenon_Vzn)
% 13.44/13.77  (p35 zenon_Vmy)
% 13.44/13.77  (zenon_Vsz != zenon_Vmaa)
% 13.44/13.77  (p46 zenon_Vyt)
% 13.44/13.77  (p24 zenon_Vcz)
% 13.44/13.77  (zenon_X141 != zenon_Vtaa)
% 13.44/13.77  (zenon_Vyz != zenon_Vsaa)
% 13.44/13.77  (zenon_Voz != zenon_Vmaa)
% 13.44/13.77  (p83 zenon_Vdj)
% 13.44/13.77  (p62 zenon_Vln)
% 13.44/13.77  (-. (p23 zenon_Vpaa))
% 13.44/13.77  (p31 zenon_Vhz)
% 13.44/13.77  (zenon_Vqz != zenon_Voaa)
% 13.44/13.77  (p72 zenon_Vjh)
% 13.44/13.77  (-. (p11 zenon_Vwaa))
% 13.44/13.77  (p34 zenon_Vuv)
% 13.44/13.77  (p41 zenon_Vxx)
% 13.44/13.77  (p46 zenon_Vzu)
% 13.44/13.77  (zenon_Vyz != zenon_Vnaa)
% 13.44/13.77  (p65 zenon_Vcq)
% 13.44/13.77  (p14 zenon_X125)
% 13.44/13.77  (p85 zenon_Vhi)
% 13.44/13.77  (p86 zenon_Vnf)
% 13.44/13.77  (p54 zenon_Vlu)
% 13.44/13.77  (p92 zenon_Vga)
% 13.44/13.77  (p45 zenon_Vjw)
% 13.44/13.77  (p21 zenon_Vkaa)
% 13.44/13.77  (p34 zenon_Vqw)
% 13.44/13.77  (p63 zenon_Ver)
% 13.44/13.77  (p13 zenon_X143)
% 13.44/13.77  (p25 zenon_Vqz)
% 13.44/13.77  (p34 zenon_Vix)
% 13.44/13.77  (r1 Tau_2 zenon_Vuaa)
% 13.44/13.77  (p85 zenon_Vzh)
% 13.44/13.77  (p83 zenon_Vtj)
% 13.44/13.77  (-. (p15 zenon_Vtaa))
% 13.44/13.77  (p52 zenon_Vyq)
% 13.44/13.77  (r1 Tau_4 zenon_Vwaa)
% 13.44/13.77  (p104 zenon_Vo)
% 13.44/13.77  (p56 zenon_Vrp)
% 13.44/13.77  (p11 zenon_X145)
% 13.44/13.77  (p56 zenon_Vvr)
% 13.44/13.77  (p61 zenon_Vgs)
% 13.44/13.77  (p81 zenon_Vfl)
% 13.44/13.77  (p95 zenon_Vxc)
% 13.44/13.77  (p43 zenon_Vxw)
% 13.44/13.77  (p45 zenon_Vnw)
% 13.44/13.77  (r1 Tau_0 Tau_4)
% 13.44/13.77  (p21 zenon_Viaa)
% 13.44/13.77  (p76 zenon_Vch)
% 13.44/13.77  (-. (p25 zenon_Voaa))
% 13.44/13.77  (p91 zenon_Vmg)
% 13.44/13.77  (p22 zenon_Vdy)
% 13.44/13.77  (zenon_X144 != zenon_Vvaa)
% 13.44/13.77  (p12 zenon_X144)
% 13.44/13.77  (p53 zenon_Vvu)
% 13.44/13.77  (p96 zenon_Vhb)
% 13.44/13.77  (p44 zenon_Vcu)
% 13.44/13.77  (zenon_Vsz != zenon_Voaa)
% 13.44/13.77  (r1 Tau_1 zenon_Vtaa)
% 13.44/13.77  (p32 zenon_Vtw)
% 13.44/13.77  (p61 zenon_Vms)
% 13.44/13.77  (p53 zenon_Vqu)
% 13.44/13.77  (p82 zenon_Vee)
% 13.44/13.77  (p102 zenon_Vp)
% 13.44/13.77  (p61 zenon_Vss)
% 13.44/13.77  (p16 zenon_X129)
% 13.44/13.77  (p45 zenon_Vbw)
% 13.44/13.77  (p33 zenon_Vvy)
% 13.44/13.77  (p22 zenon_Vsy)
% 13.44/13.77  (zenon_Vwz != zenon_Vpaa)
% 13.44/13.77  (zenon_Vsz != zenon_Vraa)
% 13.44/13.77  (p62 zenon_Vfm)
% 13.44/13.77  (zenon_Vyz != zenon_Vpaa)
% 13.44/13.77  (p81 zenon_Vnl)
% 13.44/13.77  (p56 zenon_Vtq)
% 13.44/13.77  (p16 zenon_X134)
% 13.44/13.77  (-. (p12 zenon_Vvaa))
% 13.44/13.77  (p86 zenon_Vod)
% 13.44/13.77  (p32 zenon_Vlx)
% 13.44/13.77  (p43 zenon_Vfx)
% 13.44/13.77  (p24 zenon_Vqy)
% 13.44/13.77  (p24 zenon_Vby)
% 13.44/13.77  (p14 zenon_X135)
% 13.44/13.77  (zenon_Vqz != zenon_Vraa)
% 13.44/13.77  (p76 zenon_Vak)
% 13.44/13.77  (zenon_Viaa != zenon_Vqaa)
% 13.44/13.77  (p106 zenon_Vm)
% 13.44/13.77  (zenon_Vaaa != zenon_Vsaa)
% 13.44/13.77  (p96 zenon_Vx)
% 13.44/13.77  (p101 zenon_Vn)
% 13.44/13.77  (p94 zenon_Vne)
% 13.44/13.77  (p96 zenon_Vpa)
% 13.44/13.77  (p66 zenon_Vmo)
% 13.44/13.77  (p64 zenon_Vzl)
% 13.44/13.77  (p91 zenon_Vvg)
% 13.44/13.77  (zenon_Vwz != zenon_Vsaa)
% 13.44/13.77  (zenon_Veaa != zenon_Vqaa)
% 13.44/13.77  (p66 zenon_Vzm)
% 13.44/13.77  (p44 zenon_Vdv)
% 13.44/13.77  *)
% 13.44/13.77  (* NO-PROOF *)
% 13.44/13.77  % SZS status GaveUp
% 13.44/13.77  Number of rewrites on terms: 0
% 13.44/13.77  Number of rewrites on props: 4
% 13.44/13.77  nodes searched: 1539
% 13.44/13.77  max branch formulas: 1676
% 13.44/13.77  proof nodes created: 19
% 13.44/13.77  formulas created: 11698
% 13.44/13.77  
%------------------------------------------------------------------------------