↑ Up

ZenonModulo---0.5.0.UNK-Non.f

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

% Computer : n012.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:29 PM UTC 2026

% Result   : Unknown 0.07s 0.38s
% Output   : None 
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01  % Problem  : LCL686+1.020 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.01  % Command  : run_zenon_modulo %d %s
% 0.02/0.28  % Computer : n012.cluster.edu
% 0.02/0.28  % Model    : x86_64 x86_64
% 0.02/0.28  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.02/0.28  % Memory   : 8046.5625MB
% 0.02/0.28  % OS       : Linux 6.8.0-71-generic
% 0.02/0.29  % CPULimit : 300
% 0.02/0.29  % WCLimit  : 300
% 0.02/0.29  % DateTime : Sun Sep  6 00:31:57 UTC 2026
% 0.02/0.29  % CPUTime  : 
% 0.07/0.38  Zenon error: exhausted search space without finding a proof
% 0.07/0.38  (* Current branch:
% 0.07/0.38  (zenon_Vzb != zenon_Vbe)
% 0.07/0.38  (p2 zenon_Vyd)
% 0.07/0.38  (r1 zenon_Vjb zenon_Vkb)
% 0.07/0.38  (p12 zenon_Vpd)
% 0.07/0.38  (p3 zenon_Vxd)
% 0.07/0.38  (p28 zenon_Vyc)
% 0.07/0.38  (p58 zenon_Vvb)
% 0.07/0.38  (-. (p34 zenon_Vbe))
% 0.07/0.38  (p50 zenon_Vcc)
% 0.07/0.38  (p53 zenon_Vac)
% 0.07/0.38  (p54 zenon_Vyb)
% 0.07/0.38  (r1 zenon_Vsb zenon_Vtb)
% 0.07/0.38  (p11 zenon_Vbe)
% 0.07/0.38  (p29 zenon_Vyc)
% 0.07/0.38  (zenon_Vyd != zenon_Vbe)
% 0.07/0.38  (r1 zenon_Vma zenon_Vna)
% 0.07/0.38  (p58 zenon_Vub)
% 0.07/0.38  (r1 zenon_Vt zenon_Vu)
% 0.07/0.38  (p47 zenon_Vfc)
% 0.07/0.38  (p5 zenon_Vvd)
% 0.07/0.38  (r1 zenon_Vra zenon_Vsa)
% 0.07/0.38  (p45 zenon_Vhc)
% 0.07/0.38  (p38 zenon_Voc)
% 0.07/0.38  (p26 zenon_Vad)
% 0.07/0.38  (r1 zenon_Vea zenon_Vfa)
% 0.07/0.38  (p55 zenon_Vbe)
% 0.07/0.38  (-. (p36 zenon_Vbe))
% 0.07/0.38  (-. (p56 zenon_Vbe))
% 0.07/0.38  (zenon_Vsd != zenon_Vbe)
% 0.07/0.38  (p13 zenon_Vod)
% 0.07/0.38  (p43 zenon_Vbe)
% 0.07/0.38  (-. (p54 zenon_Vbe))
% 0.07/0.38  (-. (p16 zenon_Vbe))
% 0.07/0.38  (p21 zenon_Vgd)
% 0.07/0.38  (Tau_1 != zenon_Vae)
% 0.07/0.38  (zenon_Vid != zenon_Vbe)
% 0.07/0.38  (p23 zenon_Vbe)
% 0.07/0.38  (r1 zenon_Vu zenon_Vv)
% 0.07/0.38  (p14 zenon_Vmd)
% 0.07/0.38  (r1 zenon_Vhb zenon_Vib)
% 0.07/0.38  (p4 zenon_Vwd)
% 0.07/0.38  (p17 zenon_Vbe)
% 0.07/0.38  (p9 zenon_Vsd)
% 0.07/0.38  (zenon_Vfd != zenon_Vbe)
% 0.07/0.38  (r1 zenon_Vgb zenon_Vhb)
% 0.07/0.38  (p40 zenon_Vmc)
% 0.07/0.38  (r1 zenon_Voa zenon_Vpa)
% 0.07/0.38  (p28 zenon_Vzc)
% 0.07/0.38  (p36 zenon_Vrc)
% 0.07/0.38  (p5 zenon_Vbe)
% 0.07/0.38  (-. (p10 zenon_Vbe))
% 0.07/0.38  (p22 zenon_Vfd)
% 0.07/0.38  (p1 zenon_Vzd)
% 0.07/0.38  (r1 zenon_Vqb zenon_Vrb)
% 0.07/0.38  (zenon_Vgd != zenon_Vbe)
% 0.07/0.38  (p44 zenon_Vjc)
% 0.07/0.38  (zenon_Vhc != zenon_Vbe)
% 0.07/0.38  (r1 zenon_Vn zenon_Vo)
% 0.07/0.38  (r1 zenon_Vxa zenon_Vya)
% 0.07/0.38  (p60 Tau_1)
% 0.07/0.38  (zenon_Vgc != zenon_Vbe)
% 0.07/0.38  (zenon_Vac != zenon_Vbe)
% 0.07/0.38  (r1 zenon_Vpa zenon_Vqa)
% 0.07/0.38  (p36 zenon_Vqc)
% 0.07/0.38  (zenon_Vvd != zenon_Vbe)
% 0.07/0.38  (r1 zenon_Vrb zenon_Vsb)
% 0.07/0.38  (p53 zenon_Vzb)
% 0.07/0.38  (r1 zenon_Vla zenon_Vma)
% 0.07/0.38  (p11 zenon_Vpd)
% 0.07/0.38  (zenon_Vcd != zenon_Vbe)
% 0.07/0.38  (zenon_Vrd != zenon_Vbe)
% 0.07/0.38  (p55 zenon_Vxb)
% 0.07/0.38  (p31 zenon_Vwc)
% 0.07/0.38  (r1 zenon_Vo zenon_Vp)
% 0.07/0.38  (zenon_Vtc != zenon_Vbe)
% 0.07/0.38  (p57 zenon_Vbe)
% 0.07/0.38  (p26 zenon_Vbd)
% 0.07/0.38  (p32 zenon_Vvc)
% 0.07/0.38  (p57 zenon_Vwb)
% 0.07/0.38  (p52 zenon_Vbc)
% 0.07/0.38  (p40 zenon_Vnc)
% 0.07/0.38  (zenon_Vkd != zenon_Vbe)
% 0.07/0.38  (zenon_Vwd != zenon_Vbe)
% 0.07/0.38  (p41 zenon_Vmc)
% 0.07/0.38  (p56 zenon_Vwb)
% 0.07/0.38  (zenon_Vld != zenon_Vbe)
% 0.07/0.38  (zenon_Vud != zenon_Vbe)
% 0.07/0.38  (p55 zenon_Vyb)
% 0.07/0.38  (zenon_Vyb != zenon_Vbe)
% 0.07/0.38  (zenon_Vwb != zenon_Vbe)
% 0.07/0.38  (zenon_Vic != zenon_Vbe)
% 0.07/0.38  (zenon_Vxd != zenon_Vbe)
% 0.07/0.38  (p49 zenon_Vbe)
% 0.07/0.38  (p30 zenon_Vwc)
% 0.07/0.38  (r1 zenon_Vab zenon_Vbb)
% 0.07/0.38  (p47 zenon_Vgc)
% 0.07/0.38  (zenon_Vhd != zenon_Vbe)
% 0.07/0.38  (p17 zenon_Vjd)
% 0.07/0.38  (p43 zenon_Vjc)
% 0.07/0.38  (r1 zenon_Vz zenon_Vaa)
% 0.07/0.38  (zenon_Vdc != zenon_Vbe)
% 0.07/0.38  (r1 zenon_Vua zenon_Vva)
% 0.07/0.38  (p27 zenon_Vad)
% 0.07/0.38  (r1 zenon_Vfb zenon_Vgb)
% 0.07/0.38  (p48 zenon_Vec)
% 0.07/0.38  (r1 zenon_Vp zenon_Vq)
% 0.07/0.38  (p18 zenon_Vid)
% 0.07/0.38  (p24 zenon_Vdd)
% 0.07/0.38  (p35 zenon_Vrc)
% 0.07/0.38  (p46 zenon_Vhc)
% 0.07/0.38  (p23 zenon_Vdd)
% 0.07/0.38  (r1 zenon_Vob zenon_Vpb)
% 0.07/0.38  (zenon_Vec != zenon_Vbe)
% 0.07/0.38  (zenon_Vjd != zenon_Vbe)
% 0.07/0.38  (p49 zenon_Vec)
% 0.07/0.38  (p10 zenon_Vqd)
% 0.07/0.38  (p21 zenon_Vfd)
% 0.07/0.38  (-. (p38 zenon_Vbe))
% 0.07/0.38  (p45 zenon_Vbe)
% 0.07/0.38  (p7 zenon_Vtd)
% 0.07/0.38  (r1 zenon_Vka zenon_Vla)
% 0.07/0.38  (p37 zenon_Vbe)
% 0.07/0.38  (r1 zenon_Vva zenon_Vwa)
% 0.07/0.38  (p37 zenon_Vpc)
% 0.07/0.38  (r1 zenon_Vaa zenon_Vba)
% 0.07/0.38  (p49 zenon_Vdc)
% 0.07/0.38  (p19 zenon_Vbe)
% 0.07/0.38  (r1 zenon_Vha zenon_Via)
% 0.07/0.38  (p43 zenon_Vkc)
% 0.07/0.38  (p25 zenon_Vbd)
% 0.07/0.38  (zenon_Vpd != zenon_Vbe)
% 0.07/0.38  (r1 zenon_Vkb zenon_Vlb)
% 0.07/0.38  (r1 zenon_Vq zenon_Vr)
% 0.07/0.38  (r1 zenon_Vn zenon_Vbe)
% 0.07/0.38  (p25 zenon_Vcd)
% 0.07/0.38  (zenon_Vmc != zenon_Vbe)
% 0.07/0.38  (zenon_Vnc != zenon_Vbe)
% 0.07/0.38  (r1 zenon_Vta zenon_Vua)
% 0.07/0.38  (zenon_Vad != zenon_Vbe)
% 0.07/0.38  (p23 zenon_Ved)
% 0.07/0.38  (-. (p46 zenon_Vbe))
% 0.07/0.38  (p8 zenon_Vsd)
% 0.07/0.38  (r1 zenon_Vna zenon_Voa)
% 0.07/0.38  (r1 zenon_Vdb zenon_Veb)
% 0.07/0.38  (p14 zenon_Vnd)
% 0.07/0.38  (zenon_Vsc != zenon_Vbe)
% 0.07/0.38  (-. (p32 zenon_Vbe))
% 0.07/0.38  (r1 zenon_Vwa zenon_Vxa)
% 0.07/0.38  (p18 zenon_Vjd)
% 0.07/0.38  (r1 zenon_Vx zenon_Vy)
% 0.07/0.38  (-. (p20 zenon_Vbe))
% 0.07/0.38  (-. (p26 zenon_Vbe))
% 0.07/0.38  (zenon_Vyc != zenon_Vbe)
% 0.07/0.38  (zenon_Vvb != zenon_Vbe)
% 0.07/0.38  (p39 zenon_Voc)
% 0.07/0.38  (p31 zenon_Vbe)
% 0.07/0.38  (p42 zenon_Vkc)
% 0.07/0.38  (p47 zenon_Vbe)
% 0.07/0.38  (p39 zenon_Vnc)
% 0.07/0.38  (p9 zenon_Vrd)
% 0.07/0.38  (p35 zenon_Vsc)
% 0.07/0.38  (zenon_Vvc != zenon_Vbe)
% 0.07/0.38  (r1 zenon_Vfa zenon_Vga)
% 0.07/0.38  (p1 zenon_Vbe)
% 0.07/0.38  (zenon_Vtd != zenon_Vbe)
% 0.07/0.38  (p13 zenon_Vbe)
% 0.07/0.38  (zenon_Voc != zenon_Vbe)
% 0.07/0.38  (r1 zenon_Vbb zenon_Vcb)
% 0.07/0.38  (-. (p60 zenon_Vae))
% 0.07/0.38  (r1 zenon_Vpb zenon_Vqb)
% 0.07/0.38  (p16 zenon_Vld)
% 0.07/0.38  (p50 zenon_Vdc)
% 0.07/0.38  (zenon_Vlc != zenon_Vbe)
% 0.07/0.38  (p52 zenon_Vac)
% 0.07/0.38  (p33 zenon_Vbe)
% 0.07/0.38  (p51 zenon_Vbc)
% 0.07/0.38  (p29 zenon_Vxc)
% 0.07/0.38  (zenon_Vnd != zenon_Vbe)
% 0.07/0.38  (zenon_Ved != zenon_Vbe)
% 0.07/0.38  (zenon_Vuc != zenon_Vbe)
% 0.07/0.38  (r1 zenon_Vib zenon_Vjb)
% 0.07/0.38  (-. (p24 zenon_Vbe))
% 0.07/0.38  (r1 zenon_Vcb zenon_Vdb)
% 0.07/0.38  (r1 zenon_Vy zenon_Vz)
% 0.07/0.38  (zenon_Vmd != zenon_Vbe)
% 0.07/0.38  (-. (p4 zenon_Vbe))
% 0.07/0.38  (p3 zenon_Vyd)
% 0.07/0.38  (p5 zenon_Vwd)
% 0.07/0.38  (p31 zenon_Vvc)
% 0.07/0.38  (p12 zenon_Vod)
% 0.07/0.38  (p7 zenon_Vud)
% 0.07/0.38  (r1 zenon_Vca zenon_Vda)
% 0.07/0.38  (p35 zenon_Vbe)
% 0.07/0.38  (zenon_Vpc != zenon_Vbe)
% 0.07/0.38  (-. (p18 zenon_Vbe))
% 0.07/0.38  (r1 zenon_Vba zenon_Vca)
% 0.07/0.38  (-. (p30 zenon_Vbe))
% 0.07/0.38  (p1 zenon_Vm)
% 0.07/0.38  (p15 zenon_Vmd)
% 0.07/0.38  (p4 zenon_Vxd)
% 0.07/0.38  (-. (p22 zenon_Vbe))
% 0.07/0.38  (r1 zenon_Vnb zenon_Vob)
% 0.07/0.38  (p59 zenon_Vub)
% 0.07/0.38  (p24 zenon_Vcd)
% 0.07/0.38  (r1 zenon_Vza zenon_Vab)
% 0.07/0.38  (zenon_Vod != zenon_Vbe)
% 0.07/0.38  (p30 zenon_Vxc)
% 0.07/0.38  (-. (p50 zenon_Vbe))
% 0.07/0.38  (r1 zenon_Vsa zenon_Vta)
% 0.07/0.38  (p15 zenon_Vld)
% 0.07/0.38  (-. (p6 zenon_Vbe))
% 0.07/0.38  (-. (p44 zenon_Vbe))
% 0.07/0.38  (-. (p8 zenon_Vbe))
% 0.07/0.38  (p34 zenon_Vtc)
% 0.07/0.38  (zenon_Vbd != zenon_Vbe)
% 0.07/0.38  (zenon_Vkc != zenon_Vbe)
% 0.07/0.38  (p51 zenon_Vbe)
% 0.07/0.38  (p11 zenon_Vqd)
% 0.07/0.38  (p6 zenon_Vud)
% 0.07/0.38  (r1 zenon_Vr zenon_Vs)
% 0.07/0.38  (p32 zenon_Vuc)
% 0.07/0.38  (-. (p12 zenon_Vbe))
% 0.07/0.38  (p46 zenon_Vgc)
% 0.07/0.38  (-. (p14 zenon_Vbe))
% 0.07/0.38  (zenon_Vfc != zenon_Vbe)
% 0.07/0.38  (r1 zenon_Via zenon_Vja)
% 0.07/0.38  (p57 zenon_Vvb)
% 0.07/0.38  (p33 zenon_Vtc)
% 0.07/0.38  (p19 zenon_Vhd)
% 0.07/0.38  (p42 zenon_Vlc)
% 0.07/0.38  (p8 zenon_Vtd)
% 0.07/0.38  (p54 zenon_Vzb)
% 0.07/0.38  (zenon_Vxb != zenon_Vbe)
% 0.07/0.38  (p41 zenon_Vlc)
% 0.07/0.38  (r1 Tau_0 Tau_1)
% 0.07/0.38  (-. (p42 zenon_Vbe))
% 0.07/0.38  (p3 zenon_Vbe)
% 0.07/0.38  (p6 zenon_Vvd)
% 0.07/0.38  (p39 zenon_Vbe)
% 0.07/0.38  (p51 zenon_Vcc)
% 0.07/0.38  (p9 zenon_Vbe)
% 0.07/0.38  (p44 zenon_Vic)
% 0.07/0.38  (p38 zenon_Vpc)
% 0.07/0.38  (zenon_Vjc != zenon_Vbe)
% 0.07/0.38  (r1 zenon_Veb zenon_Vfb)
% 0.07/0.38  (p16 zenon_Vkd)
% 0.07/0.38  (p27 zenon_Vzc)
% 0.07/0.38  (zenon_Vub != zenon_Vbe)
% 0.07/0.38  (r1 zenon_Vs zenon_Vt)
% 0.07/0.38  (r1 zenon_Vn zenon_Vae)
% 0.07/0.38  (-. (p2 zenon_Vbe))
% 0.07/0.38  (r1 zenon_Vmb zenon_Vnb)
% 0.07/0.38  (p20 zenon_Vhd)
% 0.07/0.38  (zenon_Vzc != zenon_Vbe)
% 0.07/0.38  (p15 zenon_Vbe)
% 0.07/0.38  (zenon_Vxc != zenon_Vbe)
% 0.07/0.38  (-. (p52 zenon_Vbe))
% 0.07/0.38  (p45 zenon_Vic)
% 0.07/0.38  (zenon_Vdd != zenon_Vbe)
% 0.07/0.38  (p10 zenon_Vrd)
% 0.07/0.38  (-. (p58 zenon_Vbe))
% 0.07/0.38  (p21 zenon_Vbe)
% 0.07/0.38  (zenon_Vqd != zenon_Vbe)
% 0.07/0.38  (p48 zenon_Vfc)
% 0.07/0.38  (p22 zenon_Ved)
% 0.07/0.38  (r1 zenon_Vda zenon_Vea)
% 0.07/0.38  (p29 zenon_Vbe)
% 0.07/0.38  (r1 zenon_Vv zenon_Vw)
% 0.07/0.38  (p13 zenon_Vnd)
% 0.07/0.38  (r1 zenon_Vya zenon_Vza)
% 0.07/0.38  (p27 zenon_Vbe)
% 0.07/0.38  (r1 zenon_Vlb zenon_Vmb)
% 0.07/0.38  (r1 zenon_Vga zenon_Vha)
% 0.07/0.38  (p37 zenon_Vqc)
% 0.07/0.38  (r1 zenon_Vw zenon_Vx)
% 0.07/0.38  (zenon_Vqc != zenon_Vbe)
% 0.07/0.38  (zenon_Vcc != zenon_Vbe)
% 0.07/0.38  (r1 zenon_Vqa zenon_Vra)
% 0.07/0.38  (p33 zenon_Vuc)
% 0.07/0.38  (p7 zenon_Vbe)
% 0.07/0.38  (r1 Tau_1 zenon_Vm)
% 0.07/0.38  (p41 zenon_Vbe)
% 0.07/0.38  (p17 zenon_Vkd)
% 0.07/0.38  (p34 zenon_Vsc)
% 0.07/0.38  (p19 zenon_Vid)
% 0.07/0.38  (-. (p28 zenon_Vbe))
% 0.07/0.38  (p59 zenon_Vbe)
% 0.07/0.38  (-. (p40 zenon_Vbe))
% 0.07/0.38  (zenon_Vwc != zenon_Vbe)
% 0.07/0.38  (p53 zenon_Vbe)
% 0.07/0.38  (r1 Tau_0 Tau_2)
% 0.07/0.38  (zenon_Vbc != zenon_Vbe)
% 0.07/0.38  (p56 zenon_Vxb)
% 0.07/0.38  (zenon_Vrc != zenon_Vbe)
% 0.07/0.38  (-. (p48 zenon_Vbe))
% 0.07/0.38  (r1 zenon_Vja zenon_Vka)
% 0.07/0.38  (zenon_Vzd != zenon_Vbe)
% 0.07/0.38  (p2 zenon_Vzd)
% 0.07/0.38  (p25 zenon_Vbe)
% 0.07/0.38  (p20 zenon_Vgd)
% 0.07/0.38  *)
% 0.07/0.38  (* NO-PROOF *)
% 0.07/0.38  % SZS status GaveUp
% 0.07/0.38  Number of rewrites on terms: 0
% 0.07/0.38  Number of rewrites on props: 0
% 0.07/0.38  nodes searched: 837
% 0.07/0.38  max branch formulas: 990
% 0.07/0.38  proof nodes created: 87
% 0.07/0.38  formulas created: 4505
% 0.07/0.38  
%------------------------------------------------------------------------------