↑ Up

ZenonModulo---0.5.0.UNK-Non.f

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

% Computer : n010.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:19 PM UTC 2026

% Result   : Unknown 0.55s 0.89s
% Output   : None 
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : LCL659+1.020 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03  % Command  : run_zenon_modulo %d %s
% 0.09/0.35  % Computer : n010.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 13:26:37 UTC 2026
% 0.09/0.35  % CPUTime  : 
% 0.55/0.89  Zenon error: exhausted search space without finding a proof
% 0.55/0.89  (* Current branch:
% 0.55/0.89  (zenon_Vni != zenon_Vge)
% 0.55/0.89  (p1 zenon_Vgh)
% 0.55/0.89  (zenon_Vih != zenon_Vxk)
% 0.55/0.89  (zenon_Vni != zenon_Voi)
% 0.55/0.89  (zenon_Vni != zenon_Vma)
% 0.55/0.89  (r1 zenon_Vam zenon_Vdm)
% 0.55/0.89  (zenon_Vih != zenon_Vvm)
% 0.55/0.89  (zenon_Vni != zenon_Vbe)
% 0.55/0.89  (zenon_Vgh != zenon_Vpm)
% 0.55/0.89  (r1 zenon_Voj zenon_Vrj)
% 0.55/0.89  (zenon_Vni != zenon_Vql)
% 0.55/0.89  (-. (p1 zenon_Vga))
% 0.55/0.89  (zenon_Vgh != zenon_Vli)
% 0.55/0.89  (-. (p1 zenon_Ven))
% 0.55/0.89  (-. (p1 zenon_Voi))
% 0.55/0.89  (-. (p1 zenon_Vhh))
% 0.55/0.89  (zenon_Vni != zenon_Vaj)
% 0.55/0.89  (r1 zenon_Vfi zenon_Vgi)
% 0.55/0.89  (zenon_Vih != zenon_Van)
% 0.55/0.89  (zenon_Vih != zenon_Vmb)
% 0.55/0.89  (zenon_Vih != zenon_Vtn)
% 0.55/0.89  (-. (p1 zenon_Vxf))
% 0.55/0.89  (zenon_Vni != zenon_Vcl)
% 0.55/0.89  (zenon_Vih != zenon_Vsj)
% 0.55/0.89  (zenon_Vgh != zenon_Vxe)
% 0.55/0.89  (zenon_Vih != zenon_Vlh)
% 0.55/0.89  (zenon_Vgh != zenon_Vmb)
% 0.55/0.89  (zenon_Vgh != zenon_Vjm)
% 0.55/0.89  (r1 zenon_Vig zenon_Vlg)
% 0.55/0.89  (-. (p1 zenon_Vrf))
% 0.55/0.89  (zenon_Vih != zenon_Vbe)
% 0.55/0.89  (zenon_Vih != zenon_Vkn)
% 0.55/0.89  (zenon_Vgh != zenon_Vwe)
% 0.55/0.89  (zenon_Vih != zenon_Vai)
% 0.55/0.89  (-. (p1 zenon_Vmg))
% 0.55/0.89  (zenon_Vih != zenon_Vnn)
% 0.55/0.89  (r1 zenon_Vic zenon_Vlc)
% 0.55/0.89  (zenon_Vni != zenon_Vjd)
% 0.55/0.89  (-. (p1 zenon_Vae))
% 0.55/0.89  (r1 zenon_Vxd zenon_Vae)
% 0.55/0.89  (zenon_Vni != zenon_Vkl)
% 0.55/0.89  (-. (p1 zenon_Vcl))
% 0.55/0.89  (zenon_Vgh != zenon_Voi)
% 0.55/0.89  (-. (p1 zenon_Vma))
% 0.55/0.89  (zenon_Vni != zenon_Voh)
% 0.55/0.89  (r1 zenon_Vtk zenon_Vwk)
% 0.55/0.89  (-. (p1 zenon_Vkl))
% 0.55/0.89  (zenon_Vih != zenon_Vga)
% 0.55/0.89  (-. (p1 zenon_Ved))
% 0.55/0.89  (-. (p1 zenon_Vzh))
% 0.55/0.89  (zenon_Vgh != zenon_Vhh)
% 0.55/0.89  (zenon_Vgh != zenon_Vxf)
% 0.55/0.89  (zenon_Vih != zenon_Ved)
% 0.55/0.89  (zenon_Vih != zenon_Vma)
% 0.55/0.89  (zenon_Vni != zenon_Vxf)
% 0.55/0.89  (-. (p1 zenon_Vlh))
% 0.55/0.89  (zenon_Vni != zenon_Vmg)
% 0.55/0.89  (-. (p1 zenon_Vdd))
% 0.55/0.89  (zenon_Vih != zenon_Vrg)
% 0.55/0.89  (-. (p1 zenon_Vjd))
% 0.55/0.89  (-. (p1 zenon_Vik))
% 0.55/0.89  (zenon_Vni != zenon_Vnk)
% 0.55/0.89  (zenon_Vih != zenon_Vql)
% 0.55/0.89  (zenon_Vgh != zenon_Vhk)
% 0.55/0.89  (zenon_Vih != zenon_Vaj)
% 0.55/0.89  (zenon_Vgh != zenon_Vzh)
% 0.55/0.89  (zenon_Vni != zenon_Vai)
% 0.55/0.89  (zenon_Vgh != zenon_Vuh)
% 0.55/0.89  (-. (p1 zenon_Vcf))
% 0.55/0.89  (-. (p1 zenon_Vhb))
% 0.55/0.89  (r1 zenon_Vji zenon_Vki)
% 0.55/0.89  (zenon_Vih != zenon_Vxl)
% 0.55/0.89  (zenon_Vgh != zenon_Vsj)
% 0.55/0.89  (-. (p1 zenon_Vai))
% 0.55/0.89  (-. (p1 zenon_Vkn))
% 0.55/0.89  (-. (p1 zenon_Vhk))
% 0.55/0.89  (zenon_Vni != zenon_Vli)
% 0.55/0.89  (zenon_Vih != zenon_Vhh)
% 0.55/0.89  (zenon_Vni != zenon_Vzh)
% 0.55/0.89  (zenon_Vih != zenon_Vgc)
% 0.55/0.89  (zenon_Vni != zenon_Vgb)
% 0.55/0.89  (zenon_Vih != zenon_Ven)
% 0.55/0.89  (zenon_Vni != zenon_Vxe)
% 0.55/0.89  (r1 zenon_Vjb zenon_Vmb)
% 0.55/0.89  (zenon_Vgh != zenon_Vcf)
% 0.55/0.89  (zenon_Vgh != zenon_Vrj)
% 0.55/0.89  (-. (p1 zenon_Vpm))
% 0.55/0.89  (zenon_Vgh != zenon_Vha)
% 0.55/0.89  (r1 zenon_Vni zenon_Voi)
% 0.55/0.89  (zenon_Vni != zenon_Ved)
% 0.55/0.89  (zenon_Vih != zenon_Voh)
% 0.55/0.89  (r1 zenon_Vih zenon_Vlh)
% 0.55/0.89  (-. (p1 zenon_Vbj))
% 0.55/0.89  (-. (p1 zenon_Vnn))
% 0.55/0.89  (zenon_Vni != zenon_Vxl)
% 0.55/0.89  (zenon_Vni != zenon_Vhk)
% 0.55/0.89  (r1 zenon_Vgi zenon_Vhi)
% 0.55/0.89  (r1 zenon_Vte zenon_Vwe)
% 0.55/0.89  (zenon_Vgh != zenon_Vxl)
% 0.55/0.89  (r1 zenon_Vbh zenon_Voh)
% 0.55/0.89  (zenon_Vni != zenon_Ven)
% 0.55/0.89  (zenon_Vih != zenon_Vfc)
% 0.55/0.89  (r1 zenon_X20 zenon_Vnn)
% 0.55/0.89  (zenon_Vih != zenon_Vae)
% 0.55/0.89  (-. (p1 zenon_Vxk))
% 0.55/0.89  (zenon_Vih != zenon_Vfn)
% 0.55/0.89  (zenon_Vih != zenon_Vxj)
% 0.55/0.89  (r1 zenon_Vxm zenon_Van)
% 0.55/0.89  (zenon_Vih != zenon_Vcf)
% 0.55/0.89  (-. (p1 zenon_Vkm))
% 0.55/0.89  (zenon_Vgh != zenon_Vkl)
% 0.55/0.89  (zenon_Vih != zenon_Vwk)
% 0.55/0.89  (-. (p1 zenon_Vjm))
% 0.55/0.89  (zenon_Vih != zenon_Vgj)
% 0.55/0.89  (r1 zenon_Vdj zenon_Vgj)
% 0.55/0.89  (-. (p1 zenon_Vxe))
% 0.55/0.89  (zenon_Vni != zenon_Vlh)
% 0.55/0.89  (zenon_Vgh != zenon_Vvm)
% 0.55/0.89  (r1 zenon_Vgm zenon_Vjm)
% 0.55/0.89  (zenon_Vih != zenon_Vik)
% 0.55/0.89  (zenon_Vni != zenon_Vdm)
% 0.55/0.89  (zenon_Vgh != zenon_Vum)
% 0.55/0.89  (zenon_Vgh != zenon_Von)
% 0.55/0.89  (-. (p1 zenon_Vtn))
% 0.55/0.89  (r1 zenon_Vqn zenon_Vtn)
% 0.55/0.89  (zenon_Vgh != zenon_Vfn)
% 0.55/0.89  (zenon_Vih != zenon_Vkl)
% 0.55/0.89  (zenon_Vni != zenon_Vpm)
% 0.55/0.89  (zenon_Vih != zenon_Von)
% 0.55/0.89  (r1 zenon_Vuf zenon_Vxf)
% 0.55/0.89  (zenon_Vih != zenon_Vrj)
% 0.55/0.89  (zenon_Vni != zenon_Vlg)
% 0.55/0.89  (zenon_Vgh != zenon_Vae)
% 0.55/0.89  (zenon_Vih != zenon_Vnk)
% 0.55/0.89  (zenon_Vih != zenon_Vkm)
% 0.55/0.89  (zenon_Vih != zenon_Vyl)
% 0.55/0.89  (zenon_Vgh != zenon_Vdm)
% 0.55/0.89  (zenon_Vih != zenon_Vli)
% 0.55/0.89  (zenon_Vni != zenon_Vtn)
% 0.55/0.89  (zenon_Vni != zenon_Vae)
% 0.55/0.89  (r1 zenon_Vbn zenon_Ven)
% 0.55/0.89  (r1 zenon_Vrm zenon_Vum)
% 0.55/0.89  (zenon_Vgh != zenon_Vaj)
% 0.55/0.89  (-. (p1 zenon_Vfn))
% 0.55/0.89  (-. (p1 zenon_Vph))
% 0.55/0.89  (zenon_Vgh != zenon_Vtn)
% 0.55/0.89  (-. (p1 zenon_Voh))
% 0.55/0.89  (zenon_Vih != zenon_Vxf)
% 0.55/0.89  (zenon_Vgh != zenon_Vsf)
% 0.55/0.89  (r1 Tau_1 zenon_Vci)
% 0.55/0.89  (zenon_Vni != zenon_Van)
% 0.55/0.89  (-. (p1 zenon_Vxl))
% 0.55/0.89  (zenon_Vgh != zenon_Vxj)
% 0.55/0.89  (zenon_Vih != zenon_Vcl)
% 0.55/0.89  (zenon_Vgh != zenon_Vnk)
% 0.55/0.89  (zenon_Vgh != zenon_Vcl)
% 0.55/0.89  (zenon_Vgh != zenon_Vlg)
% 0.55/0.89  (-. (p1 zenon_Vvm))
% 0.55/0.89  (zenon_Vgh != zenon_Vll)
% 0.55/0.89  (r1 zenon_Vcc zenon_Vfc)
% 0.55/0.89  (r1 zenon_Vxi zenon_Vaj)
% 0.55/0.89  (zenon_Vih != zenon_Vha)
% 0.55/0.89  (r1 zenon_Vbh zenon_Vzh)
% 0.55/0.89  (zenon_Vih != zenon_Vhb)
% 0.55/0.89  (r1 zenon_Vgh zenon_Vhh)
% 0.55/0.89  (zenon_Vni != zenon_Vll)
% 0.55/0.89  (zenon_Vgh != zenon_Vql)
% 0.55/0.89  (zenon_Vgh != zenon_Vdd)
% 0.55/0.89  (zenon_Vni != zenon_Vhh)
% 0.55/0.89  (zenon_Vni != zenon_Vik)
% 0.55/0.89  (zenon_Vih != zenon_Vjm)
% 0.55/0.89  (-. (p1 zenon_Vgb))
% 0.55/0.89  (zenon_Vgh != zenon_Ved)
% 0.55/0.89  (-. (p1 zenon_Vli))
% 0.55/0.89  (zenon_Vih != zenon_Vpm)
% 0.55/0.89  (zenon_Vni != zenon_Vsf)
% 0.55/0.89  (r1 zenon_Vog zenon_Vrg)
% 0.55/0.89  (zenon_Vni != zenon_Vxk)
% 0.55/0.89  (-. (p1 zenon_Vum))
% 0.55/0.89  (zenon_Vgh != zenon_Vxk)
% 0.55/0.89  (zenon_Vgh != zenon_Vma)
% 0.55/0.89  (zenon_Vni != zenon_Vga)
% 0.55/0.89  (-. (p1 zenon_Vyl))
% 0.55/0.89  (zenon_Vgh != zenon_Vkn)
% 0.55/0.89  (zenon_Vgh != zenon_Vgj)
% 0.55/0.89  (zenon_Vih != zenon_Vbj)
% 0.55/0.89  (zenon_Vni != zenon_Vph)
% 0.55/0.89  (zenon_Vni != zenon_Vwk)
% 0.55/0.89  (-. (p1 zenon_Vrg))
% 0.55/0.89  (zenon_Vih != zenon_Vwe)
% 0.55/0.89  (zenon_Vih != zenon_Vxe)
% 0.55/0.89  (r1 zenon_Vul zenon_Vxl)
% 0.55/0.89  (zenon_Vgh != zenon_Vrf)
% 0.55/0.89  (zenon_Vni != zenon_Vcf)
% 0.55/0.89  (-. (p1 zenon_Vlc))
% 0.55/0.89  (-. (p1 zenon_Van))
% 0.55/0.89  (r1 zenon_Vki zenon_Vli)
% 0.55/0.89  (zenon_Vni != zenon_Vrj)
% 0.55/0.89  (zenon_Vni != zenon_Vgc)
% 0.55/0.89  (-. (p1 zenon_Von))
% 0.55/0.89  (zenon_Vgh != zenon_Vmg)
% 0.55/0.89  (-. (p1 zenon_Vsj))
% 0.55/0.89  (zenon_Vih != zenon_Voi)
% 0.55/0.89  (r1 zenon_Vmm zenon_Vpm)
% 0.55/0.89  (zenon_Vni != zenon_Vnn)
% 0.55/0.89  (zenon_Vni != zenon_Vjm)
% 0.55/0.89  (zenon_Vih != zenon_Vdm)
% 0.55/0.89  (zenon_Vih != zenon_Vlg)
% 0.55/0.89  (r1 zenon_Vmi zenon_Vni)
% 0.55/0.89  (-. (p1 zenon_Vwe))
% 0.55/0.89  (-. (p1 zenon_Vll))
% 0.55/0.89  (r1 zenon_Vdi zenon_Vei)
% 0.55/0.89  (zenon_Vih != zenon_Vge)
% 0.55/0.89  (r1 zenon_Vhi zenon_Vii)
% 0.55/0.89  (zenon_Vih != zenon_Vph)
% 0.55/0.89  (r1 zenon_Vad zenon_Vdd)
% 0.55/0.89  (r1 zenon_Vzk zenon_Vcl)
% 0.55/0.89  (zenon_Vgh != zenon_Ven)
% 0.55/0.89  (-. (p1 zenon_Vha))
% 0.55/0.89  (p1 zenon_Vih)
% 0.55/0.89  (zenon_Vih != zenon_Vum)
% 0.55/0.89  (zenon_Vni != zenon_Vbj)
% 0.55/0.89  (zenon_Vih != zenon_Vdd)
% 0.55/0.89  (zenon_Vni != zenon_Vxj)
% 0.55/0.89  (zenon_Vni != zenon_Vyl)
% 0.55/0.89  (r1 zenon_Vkk zenon_Vnk)
% 0.55/0.89  (-. (p1 zenon_Vmb))
% 0.55/0.89  (r1 zenon_Vbh zenon_Vgh)
% 0.55/0.89  (r1 zenon_Vdb zenon_Vgb)
% 0.55/0.89  (zenon_Vih != zenon_Vsf)
% 0.55/0.89  (zenon_Vgh != zenon_Vyl)
% 0.55/0.89  (zenon_Vni != zenon_Von)
% 0.55/0.89  (zenon_Vih != zenon_Vll)
% 0.55/0.89  (-. (p1 zenon_Vge))
% 0.55/0.89  (zenon_Vni != zenon_Vuh)
% 0.55/0.89  (zenon_Vgh != zenon_Vge)
% 0.55/0.89  (-. (p1 zenon_Vdm))
% 0.55/0.89  (zenon_Vih != zenon_Vlc)
% 0.55/0.89  (zenon_Vni != zenon_Vrg)
% 0.55/0.89  (zenon_Vih != zenon_Vmg)
% 0.55/0.89  (-. (p1 zenon_Vgj))
% 0.55/0.89  (zenon_Vgh != zenon_Vph)
% 0.55/0.89  (zenon_Vih != zenon_Vhk)
% 0.55/0.89  (r1 zenon_Vuj zenon_Vxj)
% 0.55/0.89  (zenon_Vni != zenon_Vha)
% 0.55/0.89  (r1 zenon_Vde zenon_Vge)
% 0.55/0.89  (r1 zenon_Vze zenon_Vcf)
% 0.55/0.89  (zenon_Vih != zenon_Vrf)
% 0.55/0.89  (zenon_Vgh != zenon_Vwk)
% 0.55/0.89  (r1 zenon_Vja zenon_Vma)
% 0.55/0.89  (-. (p1 zenon_Vbe))
% 0.55/0.89  (r1 zenon_Vda zenon_Vga)
% 0.55/0.89  (r1 zenon_Vhn zenon_Vkn)
% 0.55/0.89  (zenon_Vgh != zenon_Vfc)
% 0.55/0.89  (r1 zenon_Vrh zenon_Vuh)
% 0.55/0.89  (zenon_Vni != zenon_Vkn)
% 0.55/0.89  (zenon_Vgh != zenon_Voh)
% 0.55/0.89  (zenon_Vgh != zenon_Vbj)
% 0.55/0.89  (r1 zenon_Vii zenon_Vji)
% 0.55/0.89  (zenon_Vgh != zenon_Vga)
% 0.55/0.89  (zenon_Vni != zenon_Vgj)
% 0.55/0.89  (zenon_Vni != zenon_Vrf)
% 0.55/0.89  (zenon_Vni != zenon_Vdd)
% 0.55/0.89  (zenon_Vgh != zenon_Vlc)
% 0.55/0.89  (zenon_Vgh != zenon_Vnn)
% 0.55/0.89  (zenon_Vih != zenon_Vgb)
% 0.55/0.89  (zenon_Vni != zenon_Vfn)
% 0.55/0.89  (-. (p1 zenon_Vfc))
% 0.55/0.89  (zenon_Vgh != zenon_Vgc)
% 0.55/0.89  (zenon_Vgh != zenon_Van)
% 0.55/0.89  (-. (p1 zenon_Vsf))
% 0.55/0.89  (zenon_Vih != zenon_Vuh)
% 0.55/0.89  (-. (p1 zenon_Vnk))
% 0.55/0.89  (zenon_Vgh != zenon_Vai)
% 0.55/0.89  (r1 zenon_Vek zenon_Vhk)
% 0.55/0.89  (zenon_Vgh != zenon_Vjd)
% 0.55/0.89  (zenon_Vih != zenon_Vjd)
% 0.55/0.89  (r1 zenon_Vci zenon_Vdi)
% 0.55/0.89  (zenon_Vgh != zenon_Vbe)
% 0.55/0.89  (-. (p1 zenon_Vaj))
% 0.55/0.89  (zenon_Vgh != zenon_Vgb)
% 0.55/0.89  (zenon_Vni != zenon_Vmb)
% 0.55/0.89  (zenon_Vni != zenon_Vkm)
% 0.55/0.89  (zenon_Vgh != zenon_Vlh)
% 0.55/0.89  (zenon_Vih != zenon_Vzh)
% 0.55/0.89  (zenon_Vgh != zenon_Vhb)
% 0.55/0.89  (-. (p1 zenon_Vgc))
% 0.55/0.89  (zenon_Vni != zenon_Vlc)
% 0.55/0.89  (zenon_Vni != zenon_Vsj)
% 0.55/0.89  (-. (p1 zenon_Vlg))
% 0.55/0.89  (-. (p1 zenon_Vwk))
% 0.55/0.89  (-. (p1 zenon_Vrj))
% 0.55/0.89  (r1 zenon_Vei zenon_Vfi)
% 0.55/0.89  (r1 zenon_Vof zenon_Vrf)
% 0.55/0.89  (zenon_Vgh != zenon_Vkm)
% 0.55/0.89  (zenon_Vni != zenon_Vvm)
% 0.55/0.89  (r1 Tau_0 Tau_1)
% 0.55/0.89  (-. (p1 zenon_Vuh))
% 0.55/0.89  (zenon_Vgh != zenon_Vik)
% 0.55/0.89  (zenon_Vni != zenon_Vum)
% 0.55/0.89  (r1 zenon_Vnl zenon_Vql)
% 0.55/0.89  (r1 zenon_Vgd zenon_Vjd)
% 0.55/0.89  (r1 zenon_Vhl zenon_Vkl)
% 0.55/0.89  (-. (p1 zenon_Vql))
% 0.55/0.89  (zenon_Vgh != zenon_Vrg)
% 0.55/0.89  (zenon_Vni != zenon_Vhb)
% 0.55/0.89  (zenon_Vni != zenon_Vfc)
% 0.55/0.89  (zenon_Vni != zenon_Vwe)
% 0.55/0.89  (p1 zenon_Vni)
% 0.55/0.89  (-. (p1 zenon_Vxj))
% 0.55/0.89  *)
% 0.55/0.89  (* NO-PROOF *)
% 0.55/0.89  % SZS status GaveUp
% 0.55/0.89  Number of rewrites on terms: 0
% 0.55/0.89  Number of rewrites on props: 0
% 0.55/0.89  nodes searched: 839
% 0.55/0.89  max branch formulas: 959
% 0.55/0.89  proof nodes created: 0
% 0.55/0.89  formulas created: 4968
% 0.55/0.89  
%------------------------------------------------------------------------------