↑ Up

ZenonModulo---0.5.0.UNK-Non.f

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

% Computer : n005.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:12 PM UTC 2026

% Result   : Unknown 0.39s 0.68s
% Output   : None 
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02  % Problem  : LCL641+1.015 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.02  % Command  : run_zenon_modulo %d %s
% 0.08/0.34  % Computer : n005.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 : Fri Sep  4 17:06:20 UTC 2026
% 0.08/0.34  % CPUTime  : 
% 0.39/0.67  Zenon error: exhausted search space without finding a proof
% 0.39/0.67  (* Current branch:
% 0.39/0.67  (zenon_Vaf != zenon_Vuf)
% 0.39/0.67  (zenon_Vaf != zenon_Vjf)
% 0.39/0.67  (-. (p1 zenon_Vdk))
% 0.39/0.67  (-. (p1 zenon_Vgd))
% 0.39/0.67  (zenon_Vpg != zenon_Veb)
% 0.39/0.67  (zenon_Vaf != zenon_Vbf)
% 0.39/0.67  (zenon_Vpg != zenon_Vph)
% 0.39/0.67  (zenon_Vaf != zenon_Vnc)
% 0.39/0.67  (zenon_Vaf != zenon_Vei)
% 0.39/0.67  (zenon_Vpg != zenon_Vza)
% 0.39/0.67  (zenon_Vcf != zenon_Vcj)
% 0.39/0.67  (zenon_Vcf != zenon_Vpf)
% 0.39/0.67  (zenon_Vcf != zenon_Vuf)
% 0.39/0.67  (zenon_Vcf != zenon_Vvh)
% 0.39/0.67  (-. (p1 zenon_Vmd))
% 0.39/0.67  (zenon_Vcf != zenon_Vij)
% 0.39/0.67  (-. (p1 zenon_Vji))
% 0.39/0.67  (r1 zenon_Vyi zenon_Vcj)
% 0.39/0.67  (zenon_Vaf != zenon_Vqh)
% 0.39/0.67  (r1 zenon_Vwb zenon_Vzb)
% 0.39/0.67  (r1 zenon_Vcd zenon_Vgd)
% 0.39/0.67  (zenon_Vaf != zenon_Vya)
% 0.39/0.67  (zenon_Vaf != zenon_Via)
% 0.39/0.67  (p1 zenon_Vpg)
% 0.39/0.67  (r1 zenon_Vy zenon_Vca)
% 0.39/0.67  (zenon_Vng != zenon_Vtb)
% 0.39/0.67  (zenon_Vaf != zenon_Vee)
% 0.39/0.67  (zenon_Vpg != zenon_Vda)
% 0.39/0.67  (r1 zenon_Vte zenon_Vaf)
% 0.39/0.67  (zenon_Vpg != zenon_Vnc)
% 0.39/0.67  (zenon_Vaf != zenon_Vmd)
% 0.39/0.67  (zenon_Vng != zenon_Vjf)
% 0.39/0.67  (zenon_Vng != zenon_Vcj)
% 0.39/0.67  (-. (p1 zenon_Vtb))
% 0.39/0.67  (-. (p1 zenon_Vvf))
% 0.39/0.67  (-. (p1 zenon_Vdi))
% 0.39/0.67  (-. (p1 zenon_Vzb))
% 0.39/0.67  (-. (p1 zenon_Vvh))
% 0.39/0.67  (zenon_Vng != zenon_Vee)
% 0.39/0.67  (r1 zenon_Vbg zenon_Vcg)
% 0.39/0.67  (zenon_Vcf != zenon_Vdk)
% 0.39/0.67  (zenon_Vpg != zenon_Vjf)
% 0.39/0.67  (zenon_Vcf != zenon_Vtj)
% 0.39/0.67  (zenon_Vpg != zenon_Vbh)
% 0.39/0.67  (zenon_Vcf != zenon_Vda)
% 0.39/0.67  (r1 zenon_Vfj zenon_Vij)
% 0.39/0.67  (zenon_Vcf != zenon_Veb)
% 0.39/0.67  (zenon_Vng != zenon_Vwi)
% 0.39/0.67  (zenon_Vaf != zenon_Vgd)
% 0.39/0.67  (r1 zenon_Veg zenon_Vfg)
% 0.39/0.67  (p1 zenon_Vaf)
% 0.39/0.67  (r1 zenon_Vcf zenon_Vff)
% 0.39/0.67  (zenon_Vng != zenon_Vgd)
% 0.39/0.67  (-. (p1 zenon_Vya))
% 0.39/0.67  (zenon_Vcf != zenon_Vjf)
% 0.39/0.67  (zenon_Vng != zenon_Voj)
% 0.39/0.67  (zenon_Vcf != zenon_Vkf)
% 0.39/0.67  (zenon_Vng != zenon_Vyd)
% 0.39/0.67  (zenon_Vng != zenon_Vbf)
% 0.39/0.67  (zenon_Vpg != zenon_Via)
% 0.39/0.67  (r1 zenon_Vyf zenon_Vzf)
% 0.39/0.67  (zenon_Vcf != zenon_Vdi)
% 0.39/0.67  (zenon_Vng != zenon_Vah)
% 0.39/0.67  (-. (p1 zenon_Vkf))
% 0.39/0.67  (zenon_Vaf != zenon_Vqi)
% 0.39/0.67  (zenon_Vaf != zenon_Vkf)
% 0.39/0.67  (r1 zenon_Vsh zenon_Vvh)
% 0.39/0.67  (zenon_Vpg != zenon_Vya)
% 0.39/0.67  (zenon_Vaf != zenon_Vdk)
% 0.39/0.67  (zenon_Vpg != zenon_Vca)
% 0.39/0.67  (-. (p1 zenon_Vuf))
% 0.39/0.67  (-. (p1 zenon_Vyd))
% 0.39/0.67  (r1 zenon_Vpb zenon_Vtb)
% 0.39/0.67  (r1 zenon_Vqj zenon_Vtj)
% 0.39/0.67  (zenon_Vng != zenon_Vyj)
% 0.39/0.67  (-. (p1 zenon_Vda))
% 0.39/0.67  (zenon_Vaf != zenon_Vff)
% 0.39/0.67  (zenon_Vpg != zenon_Vcj)
% 0.39/0.67  (zenon_Vpg != zenon_Vah)
% 0.39/0.67  (zenon_Vpg != zenon_Vdk)
% 0.39/0.67  (zenon_Vng != zenon_Via)
% 0.39/0.67  (zenon_Vcf != zenon_Voc)
% 0.39/0.67  (zenon_Vng != zenon_Vda)
% 0.39/0.67  (zenon_Vng != zenon_Vqi)
% 0.39/0.67  (-. (p1 zenon_Vbf))
% 0.39/0.67  (zenon_Vng != zenon_Veb)
% 0.39/0.67  (zenon_Vng != zenon_Vmd)
% 0.39/0.67  (zenon_Vcf != zenon_Vqi)
% 0.39/0.67  (-. (p1 zenon_Vza))
% 0.39/0.67  (zenon_Vaf != zenon_Vgh)
% 0.39/0.67  (zenon_Vpg != zenon_Vyd)
% 0.39/0.67  (-. (p1 zenon_Via))
% 0.39/0.67  (zenon_Vng != zenon_Vbh)
% 0.39/0.67  (r1 zenon_Vpg zenon_Vqg)
% 0.39/0.67  (zenon_Vaf != zenon_Vah)
% 0.39/0.67  (zenon_Vng != zenon_Vph)
% 0.39/0.67  (r1 zenon_Vwg zenon_Vah)
% 0.39/0.67  (-. (p1 zenon_Vei))
% 0.39/0.67  (zenon_Vng != zenon_Vlg)
% 0.39/0.67  (zenon_Vcf != zenon_Vub)
% 0.39/0.67  (-. (p1 zenon_Vqh))
% 0.39/0.67  (-. (p1 zenon_Vnj))
% 0.39/0.67  (r1 zenon_Vog zenon_Vpg)
% 0.39/0.67  (-. (p1 zenon_Vdj))
% 0.39/0.67  (r1 zenon_Vdg zenon_Veg)
% 0.39/0.67  (zenon_Vng != zenon_Vij)
% 0.39/0.67  (-. (p1 zenon_Vwi))
% 0.39/0.67  (zenon_Vng != zenon_Vji)
% 0.39/0.67  (r1 zenon_Vmf zenon_Vpf)
% 0.39/0.67  (r1 zenon_Vfg zenon_Vgg)
% 0.39/0.67  (zenon_Vcf != zenon_Vmd)
% 0.39/0.67  (zenon_Vpg != zenon_Vdj)
% 0.39/0.67  (zenon_Vaf != zenon_Vri)
% 0.39/0.67  (-. (p1 zenon_Vph))
% 0.39/0.67  (zenon_Vcf != zenon_Vya)
% 0.39/0.67  (-. (p1 zenon_Vee))
% 0.39/0.67  (r1 zenon_Vte zenon_Vuf)
% 0.39/0.67  (zenon_Vaf != zenon_Voc)
% 0.39/0.67  (r1 zenon_Vzh zenon_Vdi)
% 0.39/0.67  (zenon_Vcf != zenon_Vqg)
% 0.39/0.67  (zenon_Vaf != zenon_Vlg)
% 0.39/0.67  (-. (p1 zenon_Vzd))
% 0.39/0.67  (r1 zenon_Vak zenon_Vdk)
% 0.39/0.67  (zenon_Vpg != zenon_Vmd)
% 0.39/0.67  (zenon_Vcf != zenon_Vbf)
% 0.39/0.67  (zenon_Vcf != zenon_Voj)
% 0.39/0.67  (zenon_Vaf != zenon_Vyd)
% 0.39/0.67  (zenon_Vaf != zenon_Vcj)
% 0.39/0.67  (zenon_Vaf != zenon_Vph)
% 0.39/0.67  (zenon_Vng != zenon_Vub)
% 0.39/0.67  (zenon_Vng != zenon_Vnc)
% 0.39/0.67  (-. (p1 zenon_Vhd))
% 0.39/0.67  (-. (p1 zenon_Vah))
% 0.39/0.67  (zenon_Vaf != zenon_Veb)
% 0.39/0.67  (r1 zenon_Vig zenon_Vjg)
% 0.39/0.67  (r1 zenon_Vgg zenon_Vhg)
% 0.39/0.67  (zenon_Vcf != zenon_Vff)
% 0.39/0.67  (r1 zenon_Vaf zenon_Vbf)
% 0.39/0.67  (zenon_Vcf != zenon_Vnc)
% 0.39/0.67  (zenon_Vaf != zenon_Vtb)
% 0.39/0.67  (zenon_Vng != zenon_Vtj)
% 0.39/0.67  (zenon_Vpg != zenon_Vnj)
% 0.39/0.67  (r1 zenon_Vkg zenon_Vlg)
% 0.39/0.67  (zenon_Vaf != zenon_Vub)
% 0.39/0.67  (zenon_Vpg != zenon_Vzb)
% 0.39/0.67  (zenon_Vpg != zenon_Vqg)
% 0.39/0.67  (zenon_Vpg != zenon_Vxj)
% 0.39/0.67  (zenon_Vng != zenon_Vkf)
% 0.39/0.67  (zenon_Vcf != zenon_Vqh)
% 0.39/0.67  (zenon_Vcf != zenon_Vzb)
% 0.39/0.67  (zenon_Vaf != zenon_Vda)
% 0.39/0.67  (zenon_Vcf != zenon_Vei)
% 0.39/0.67  (zenon_Vng != zenon_Vqg)
% 0.39/0.67  (zenon_Vaf != zenon_Vzb)
% 0.39/0.67  (r1 zenon_Vbb zenon_Veb)
% 0.39/0.67  (zenon_Vng != zenon_Vdk)
% 0.39/0.67  (zenon_Vaf != zenon_Vxj)
% 0.39/0.67  (zenon_Vpg != zenon_Vtj)
% 0.39/0.67  (zenon_Vaf != zenon_Vij)
% 0.39/0.67  (zenon_Vaf != zenon_Vvf)
% 0.39/0.67  (zenon_Vng != zenon_Vgh)
% 0.39/0.67  (zenon_Vng != zenon_Vza)
% 0.39/0.67  (zenon_Vaf != zenon_Voj)
% 0.39/0.67  (zenon_Vng != zenon_Vxj)
% 0.39/0.67  (r1 zenon_Vzf zenon_Vag)
% 0.39/0.67  (r1 zenon_Vxf zenon_Vyf)
% 0.39/0.67  (zenon_Vcf != zenon_Vri)
% 0.39/0.68  (-. (p1 zenon_Vyj))
% 0.39/0.68  (r1 zenon_X15 zenon_Vxj)
% 0.39/0.68  (zenon_Vpg != zenon_Vbf)
% 0.39/0.68  (zenon_Vaf != zenon_Vca)
% 0.39/0.68  (r1 zenon_Vqc zenon_Vtc)
% 0.39/0.68  (zenon_Vaf != zenon_Vdi)
% 0.39/0.68  (zenon_Vpg != zenon_Vgd)
% 0.39/0.68  (zenon_Vpg != zenon_Vji)
% 0.39/0.68  (zenon_Vpg != zenon_Vdi)
% 0.39/0.68  (zenon_Vpg != zenon_Vff)
% 0.39/0.68  (zenon_Vng != zenon_Vpf)
% 0.39/0.68  (zenon_Vcf != zenon_Vyj)
% 0.39/0.68  (zenon_Vcf != zenon_Vph)
% 0.39/0.68  (zenon_Vng != zenon_Vqh)
% 0.39/0.68  (zenon_Vpg != zenon_Vtc)
% 0.39/0.68  (zenon_Vpg != zenon_Vpf)
% 0.39/0.68  (zenon_Vpg != zenon_Vqh)
% 0.39/0.68  (zenon_Vng != zenon_Vvf)
% 0.39/0.68  (zenon_Vng != zenon_Vzb)
% 0.39/0.68  (zenon_Vaf != zenon_Vdj)
% 0.39/0.68  (zenon_Vpg != zenon_Vei)
% 0.39/0.68  (zenon_Vpg != zenon_Vij)
% 0.39/0.68  (zenon_Vpg != zenon_Vlg)
% 0.39/0.68  (zenon_Vcf != zenon_Vgd)
% 0.39/0.68  (-. (p1 zenon_Vqg))
% 0.39/0.68  (zenon_Vpg != zenon_Vub)
% 0.39/0.68  (zenon_Vng != zenon_Vvh)
% 0.39/0.68  (-. (p1 zenon_Vnc))
% 0.39/0.68  (-. (p1 zenon_Vtc))
% 0.39/0.68  (zenon_Vng != zenon_Vya)
% 0.39/0.68  (zenon_Vaf != zenon_Vza)
% 0.39/0.68  (zenon_Vcf != zenon_Vwi)
% 0.39/0.68  (zenon_Vpg != zenon_Vzd)
% 0.39/0.68  (zenon_Vaf != zenon_Vhd)
% 0.39/0.68  (zenon_Vcf != zenon_Vee)
% 0.39/0.68  (-. (p1 zenon_Voc))
% 0.39/0.68  (zenon_Vcf != zenon_Vzd)
% 0.39/0.68  (zenon_Vng != zenon_Vdi)
% 0.39/0.68  (zenon_Vpg != zenon_Vee)
% 0.39/0.68  (zenon_Vcf != zenon_Vdj)
% 0.39/0.68  (zenon_Vcf != zenon_Vnj)
% 0.39/0.68  (-. (p1 zenon_Vgh))
% 0.39/0.68  (-. (p1 zenon_Vff))
% 0.39/0.68  (r1 zenon_Vlh zenon_Vph)
% 0.39/0.68  (zenon_Vcf != zenon_Vza)
% 0.39/0.68  (zenon_Vng != zenon_Vca)
% 0.39/0.68  (-. (p1 zenon_Veb))
% 0.39/0.68  (r1 Tau_0 Tau_1)
% 0.39/0.68  (zenon_Vcf != zenon_Vlg)
% 0.39/0.68  (zenon_Vcf != zenon_Vca)
% 0.39/0.68  (zenon_Vaf != zenon_Vwi)
% 0.39/0.68  (-. (p1 zenon_Vpf))
% 0.39/0.68  (zenon_Vcf != zenon_Vtb)
% 0.39/0.68  (r1 zenon_Vbe zenon_Vee)
% 0.39/0.68  (zenon_Vcf != zenon_Vhd)
% 0.39/0.68  (zenon_Vpg != zenon_Vqi)
% 0.39/0.68  (r1 zenon_Vfa zenon_Via)
% 0.39/0.68  (-. (p1 zenon_Vij))
% 0.39/0.68  (-. (p1 zenon_Vbh))
% 0.39/0.68  (zenon_Vpg != zenon_Vhd)
% 0.39/0.68  (-. (p1 zenon_Vcj))
% 0.39/0.68  (r1 zenon_Vmi zenon_Vqi)
% 0.39/0.68  (zenon_Vcf != zenon_Vji)
% 0.39/0.68  (r1 zenon_Vgi zenon_Vji)
% 0.39/0.68  (zenon_Vaf != zenon_Vqg)
% 0.39/0.68  (zenon_Vcf != zenon_Via)
% 0.39/0.68  (zenon_Vcf != zenon_Vyd)
% 0.39/0.68  (zenon_Vpg != zenon_Vri)
% 0.39/0.68  (zenon_Vaf != zenon_Vpf)
% 0.39/0.68  (-. (p1 zenon_Vri))
% 0.39/0.68  (zenon_Vaf != zenon_Vbh)
% 0.39/0.68  (r1 zenon_Vud zenon_Vyd)
% 0.39/0.68  (zenon_Vcf != zenon_Vgh)
% 0.39/0.68  (zenon_Vcf != zenon_Vah)
% 0.39/0.68  (zenon_Vpg != zenon_Vwi)
% 0.39/0.68  (zenon_Vpg != zenon_Vtb)
% 0.39/0.68  (r1 zenon_Vua zenon_Vya)
% 0.39/0.68  (zenon_Vcf != zenon_Vxj)
% 0.39/0.68  (zenon_Vpg != zenon_Vvf)
% 0.39/0.68  (zenon_Vng != zenon_Voc)
% 0.39/0.68  (-. (p1 zenon_Vub))
% 0.39/0.68  (zenon_Vng != zenon_Vuf)
% 0.39/0.68  (zenon_Vcf != zenon_Vbh)
% 0.39/0.68  (zenon_Vng != zenon_Vdj)
% 0.39/0.68  (r1 zenon_Vjj zenon_Vnj)
% 0.39/0.68  (r1 zenon_Vcg zenon_Vdg)
% 0.39/0.68  (zenon_Vng != zenon_Vhd)
% 0.39/0.68  (r1 zenon_Vlg zenon_Vmg)
% 0.39/0.68  (zenon_Vpg != zenon_Voc)
% 0.39/0.68  (p1 zenon_Vcf)
% 0.39/0.68  (zenon_Vng != zenon_Vnj)
% 0.39/0.68  (r1 zenon_Vte zenon_Vjf)
% 0.39/0.68  (zenon_Vng != zenon_Vff)
% 0.39/0.68  (zenon_Vaf != zenon_Vtc)
% 0.39/0.68  (r1 zenon_Vjd zenon_Vmd)
% 0.39/0.68  (zenon_Vaf != zenon_Vnj)
% 0.39/0.68  (zenon_Vaf != zenon_Vji)
% 0.39/0.68  (zenon_Vng != zenon_Vri)
% 0.39/0.68  (r1 Tau_1 zenon_Vxf)
% 0.39/0.68  (zenon_Vcf != zenon_Vvf)
% 0.39/0.68  (-. (p1 zenon_Vlg))
% 0.39/0.68  (zenon_Vaf != zenon_Vyj)
% 0.39/0.68  (zenon_Vpg != zenon_Vgh)
% 0.39/0.68  (r1 zenon_Vdh zenon_Vgh)
% 0.39/0.68  (zenon_Vpg != zenon_Vvh)
% 0.39/0.68  (zenon_Vng != zenon_Vzd)
% 0.39/0.68  (zenon_Vcf != zenon_Vtc)
% 0.39/0.68  (r1 zenon_Vag zenon_Vbg)
% 0.39/0.68  (zenon_Vpg != zenon_Vyj)
% 0.39/0.68  (-. (p1 zenon_Vjf))
% 0.39/0.68  (zenon_Vng != zenon_Vtc)
% 0.39/0.68  (-. (p1 zenon_Vca))
% 0.39/0.68  (r1 zenon_Vjg zenon_Vkg)
% 0.39/0.68  (p1 zenon_Vng)
% 0.39/0.68  (zenon_Vaf != zenon_Vzd)
% 0.39/0.68  (-. (p1 zenon_Vqi))
% 0.39/0.68  (zenon_Vpg != zenon_Vkf)
% 0.39/0.68  (zenon_Vpg != zenon_Vuf)
% 0.39/0.68  (r1 zenon_Vti zenon_Vwi)
% 0.39/0.68  (r1 zenon_Vhg zenon_Vig)
% 0.39/0.68  (zenon_Vpg != zenon_Voj)
% 0.39/0.68  (-. (p1 zenon_Voj))
% 0.39/0.68  (zenon_Vaf != zenon_Vvh)
% 0.39/0.68  (zenon_Vaf != zenon_Vtj)
% 0.39/0.68  (zenon_Vng != zenon_Vei)
% 0.39/0.68  (-. (p1 zenon_Vtj))
% 0.39/0.68  (r1 zenon_Vjc zenon_Vnc)
% 0.39/0.68  (-. (p1 zenon_Vxj))
% 0.39/0.68  *)
% 0.39/0.68  (* NO-PROOF *)
% 0.39/0.68  % SZS status GaveUp
% 0.39/0.68  Number of rewrites on terms: 0
% 0.39/0.68  Number of rewrites on props: 0
% 0.39/0.68  nodes searched: 654
% 0.39/0.68  max branch formulas: 756
% 0.39/0.68  proof nodes created: 0
% 0.39/0.68  formulas created: 4093
% 0.39/0.68  
%------------------------------------------------------------------------------