↑ 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.010 : TPTP v9.3.1. Released v4.0.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : run_zenon_modulo %d %s

% Computer : n004.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.19s 0.54s
% Output   : None 
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : LCL641+1.010 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03  % Command  : run_zenon_modulo %d %s
% 0.08/0.36  % Computer : n004.cluster.edu
% 0.08/0.36  % Model    : x86_64 x86_64
% 0.08/0.36  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36  % Memory   : 8046.5625MB
% 0.08/0.36  % OS       : Linux 6.8.0-71-generic
% 0.08/0.36  % CPULimit : 300
% 0.08/0.36  % WCLimit  : 300
% 0.08/0.36  % DateTime : Sat Sep  5 19:46:59 UTC 2026
% 0.08/0.37  % CPUTime  : 
% 0.19/0.54  Zenon error: exhausted search space without finding a proof
% 0.19/0.54  (* Current branch:
% 0.19/0.54  (zenon_Vdc != zenon_Vkb)
% 0.19/0.54  (-. (p1 zenon_Vwc))
% 0.19/0.54  (zenon_Vbc != zenon_Vie)
% 0.19/0.54  (zenon_Vjd != zenon_Vlc)
% 0.19/0.54  (zenon_Vbc != zenon_Vof)
% 0.19/0.54  (r1 Tau_0 Tau_1)
% 0.19/0.54  (zenon_Vld != zenon_Vze)
% 0.19/0.54  (-. (p1 zenon_Vud))
% 0.19/0.54  (r1 zenon_Ved zenon_Vfd)
% 0.19/0.54  (-. (p1 zenon_Vmd))
% 0.19/0.54  (-. (p1 zenon_Vkc))
% 0.19/0.54  (-. (p1 zenon_Vpa))
% 0.19/0.54  (zenon_Vbc != zenon_Voa)
% 0.19/0.54  (zenon_Vld != zenon_Vhe)
% 0.19/0.54  (r1 zenon_Vub zenon_Vkc)
% 0.19/0.54  (zenon_Vld != zenon_Vpf)
% 0.19/0.54  (zenon_Vjd != zenon_Veb)
% 0.19/0.54  (-. (p1 zenon_Vof))
% 0.19/0.54  (zenon_Vbc != zenon_Vkb)
% 0.19/0.54  (p1 zenon_Vld)
% 0.19/0.54  (-. (p1 zenon_Vae))
% 0.19/0.54  (-. (p1 zenon_Vte))
% 0.19/0.54  (r1 zenon_Vxd zenon_Vae)
% 0.19/0.54  (zenon_Vjd != zenon_Vqc)
% 0.19/0.54  (zenon_Vld != zenon_Vwc)
% 0.19/0.54  (p1 zenon_Vdc)
% 0.19/0.54  (zenon_Vld != zenon_Voa)
% 0.19/0.54  (-. (p1 zenon_Vvd))
% 0.19/0.54  (zenon_Vbc != zenon_Vmd)
% 0.19/0.54  (-. (p1 zenon_Vze))
% 0.19/0.54  (zenon_Vjd != zenon_Vff)
% 0.19/0.54  (zenon_Vld != zenon_Vne)
% 0.19/0.54  (zenon_Vdc != zenon_Voa)
% 0.19/0.54  (r1 zenon_Vfd zenon_Vgd)
% 0.19/0.54  (zenon_Vdc != zenon_Vqc)
% 0.19/0.54  (zenon_Vbc != zenon_Vda)
% 0.19/0.54  (r1 zenon_Vab zenon_Veb)
% 0.19/0.54  (zenon_Vjd != zenon_Vpa)
% 0.19/0.54  (zenon_Vbc != zenon_Vkf)
% 0.19/0.54  (-. (p1 zenon_Vne))
% 0.19/0.54  (zenon_Vjd != zenon_Vy)
% 0.19/0.54  (zenon_Vjd != zenon_Vgc)
% 0.19/0.54  (zenon_Vdc != zenon_Vvd)
% 0.19/0.54  (zenon_Vld != zenon_Vff)
% 0.19/0.54  (r1 zenon_Vke zenon_Vne)
% 0.19/0.54  (zenon_Vbc != zenon_Vae)
% 0.19/0.54  (zenon_Vjd != zenon_Vof)
% 0.19/0.54  (zenon_Vjd != zenon_Vpf)
% 0.19/0.54  (zenon_Vdc != zenon_Vy)
% 0.19/0.54  (r1 zenon_Vqd zenon_Vud)
% 0.19/0.54  (r1 zenon_Vdd zenon_Ved)
% 0.19/0.54  (zenon_Vdc != zenon_Vud)
% 0.19/0.54  (r1 zenon_Vub zenon_Vvc)
% 0.19/0.54  (p1 zenon_Vbc)
% 0.19/0.54  (zenon_Vdc != zenon_Vkc)
% 0.19/0.54  (-. (p1 zenon_Vvc))
% 0.19/0.54  (zenon_Vbc != zenon_Veb)
% 0.19/0.54  (zenon_Vld != zenon_Vkb)
% 0.19/0.54  (r1 zenon_Vhb zenon_Vkb)
% 0.19/0.54  (zenon_Vbc != zenon_Vkc)
% 0.19/0.54  (zenon_Vld != zenon_Vpa)
% 0.19/0.54  (-. (p1 zenon_Vkf))
% 0.19/0.54  (zenon_Vdc != zenon_Veb)
% 0.19/0.54  (r1 zenon_Vzc zenon_Vad)
% 0.19/0.54  (zenon_Vbc != zenon_Vue)
% 0.19/0.54  (r1 zenon_Vaa zenon_Vda)
% 0.19/0.54  (-. (p1 zenon_Vuf))
% 0.19/0.54  (r1 zenon_Vhd zenon_Vid)
% 0.19/0.54  (-. (p1 zenon_Vda))
% 0.19/0.54  (-. (p1 zenon_Vhe))
% 0.19/0.54  (r1 zenon_Vbc zenon_Vcc)
% 0.19/0.54  (zenon_Vjd != zenon_Vua)
% 0.19/0.54  (zenon_Vdc != zenon_Vx)
% 0.19/0.54  (zenon_Vjd != zenon_Vcc)
% 0.19/0.54  (zenon_Vjd != zenon_Vuf)
% 0.19/0.54  (-. (p1 zenon_Vy))
% 0.19/0.54  (zenon_Vjd != zenon_Vze)
% 0.19/0.54  (zenon_Vld != zenon_Vx)
% 0.19/0.54  (zenon_Vld != zenon_Vue)
% 0.19/0.54  (zenon_Vjd != zenon_Vkb)
% 0.19/0.54  (r1 zenon_Vka zenon_Voa)
% 0.19/0.54  (zenon_Vbc != zenon_Vef)
% 0.19/0.54  (zenon_Vbc != zenon_Vud)
% 0.19/0.54  (r1 zenon_Vyc zenon_Vzc)
% 0.19/0.54  (zenon_Vld != zenon_Vkf)
% 0.19/0.54  (zenon_Vjd != zenon_Vvd)
% 0.19/0.54  (r1 zenon_Vgd zenon_Vhd)
% 0.19/0.54  (zenon_Vld != zenon_Vda)
% 0.19/0.54  (zenon_Vld != zenon_Vhd)
% 0.19/0.54  (zenon_Vjd != zenon_Vfb)
% 0.19/0.54  (zenon_Vbc != zenon_Vfb)
% 0.19/0.54  (r1 Tau_1 zenon_Vyc)
% 0.19/0.54  (r1 zenon_Vhf zenon_Vkf)
% 0.19/0.54  (zenon_Vld != zenon_Vvc)
% 0.19/0.54  (zenon_Vjd != zenon_Vie)
% 0.19/0.54  (r1 zenon_Vra zenon_Vua)
% 0.19/0.54  (r1 zenon_Vrf zenon_Vuf)
% 0.19/0.54  (zenon_Vdc != zenon_Vkf)
% 0.19/0.54  (zenon_Vjd != zenon_Vne)
% 0.19/0.54  (zenon_Vdc != zenon_Vze)
% 0.19/0.54  (zenon_Vbc != zenon_Vte)
% 0.19/0.54  (-. (p1 zenon_Vhd))
% 0.19/0.54  (zenon_Vjd != zenon_Voa)
% 0.19/0.54  (r1 zenon_Vde zenon_Vhe)
% 0.19/0.54  (-. (p1 zenon_Vlc))
% 0.19/0.54  (zenon_Vbc != zenon_Vvd)
% 0.19/0.54  (zenon_Vdc != zenon_Vhd)
% 0.19/0.54  (r1 zenon_Vwe zenon_Vze)
% 0.19/0.54  (zenon_Vjd != zenon_Vud)
% 0.19/0.54  (p1 zenon_Vjd)
% 0.19/0.54  (zenon_Vbc != zenon_Vuf)
% 0.19/0.54  (r1 zenon_Vpe zenon_Vte)
% 0.19/0.54  (-. (p1 zenon_Vfb))
% 0.19/0.54  (zenon_Vld != zenon_Vcc)
% 0.19/0.54  (zenon_Vdc != zenon_Vae)
% 0.19/0.54  (r1 zenon_Vcd zenon_Vdd)
% 0.19/0.54  (zenon_Vjd != zenon_Vvc)
% 0.19/0.54  (zenon_Vld != zenon_Vef)
% 0.19/0.54  (zenon_Vdc != zenon_Vpf)
% 0.19/0.54  (zenon_Vld != zenon_Vvd)
% 0.19/0.54  (-. (p1 zenon_Voa))
% 0.19/0.54  (zenon_Vbc != zenon_Vhe)
% 0.19/0.54  (zenon_Vbc != zenon_Vqc)
% 0.19/0.54  (zenon_Vjd != zenon_Vhe)
% 0.19/0.54  (zenon_Vbc != zenon_Vcc)
% 0.19/0.54  (zenon_Vbc != zenon_Vwc)
% 0.19/0.54  (zenon_Vld != zenon_Vmd)
% 0.19/0.54  (zenon_Vdc != zenon_Vuf)
% 0.19/0.54  (zenon_Vjd != zenon_Vmd)
% 0.19/0.54  (zenon_Vbc != zenon_Vy)
% 0.19/0.54  (zenon_Vdc != zenon_Vof)
% 0.19/0.54  (zenon_Vbc != zenon_Vze)
% 0.19/0.54  (zenon_Vld != zenon_Vof)
% 0.19/0.54  (zenon_Vdc != zenon_Vmd)
% 0.19/0.54  (r1 zenon_Vaf zenon_Vef)
% 0.19/0.54  (zenon_Vjd != zenon_Vef)
% 0.19/0.54  (zenon_Vld != zenon_Vqc)
% 0.19/0.54  (zenon_Vld != zenon_Vae)
% 0.19/0.54  (-. (p1 zenon_Vue))
% 0.19/0.54  (zenon_Vbc != zenon_Vua)
% 0.19/0.54  (r1 zenon_Vnc zenon_Vqc)
% 0.19/0.54  (r1 zenon_Vkd zenon_Vld)
% 0.19/0.54  (zenon_Vbc != zenon_Vpa)
% 0.19/0.54  (r1 zenon_Vld zenon_Vmd)
% 0.19/0.54  (zenon_Vld != zenon_Veb)
% 0.19/0.54  (zenon_Vdc != zenon_Vne)
% 0.19/0.54  (zenon_Vdc != zenon_Vef)
% 0.19/0.54  (zenon_Vdc != zenon_Vff)
% 0.19/0.54  (-. (p1 zenon_Vie))
% 0.19/0.54  (-. (p1 zenon_Vff))
% 0.19/0.54  (zenon_Vdc != zenon_Vte)
% 0.19/0.54  (zenon_Vld != zenon_Vfb)
% 0.19/0.54  (zenon_Vld != zenon_Vy)
% 0.19/0.54  (-. (p1 zenon_Veb))
% 0.19/0.54  (zenon_Vld != zenon_Vud)
% 0.19/0.54  (zenon_Vbc != zenon_Vne)
% 0.19/0.54  (zenon_Vdc != zenon_Vie)
% 0.19/0.54  (-. (p1 zenon_Vua))
% 0.19/0.54  (-. (p1 zenon_Vpf))
% 0.19/0.54  (zenon_Vdc != zenon_Vlc)
% 0.19/0.54  (r1 zenon_Vt zenon_Vx)
% 0.19/0.54  (zenon_Vjd != zenon_Vhd)
% 0.19/0.54  (r1 zenon_Vdc zenon_Vgc)
% 0.19/0.54  (zenon_Vjd != zenon_Vda)
% 0.19/0.54  (zenon_Vbc != zenon_Vpf)
% 0.19/0.54  (r1 zenon_Vad zenon_Vbd)
% 0.19/0.54  (zenon_Vdc != zenon_Vgc)
% 0.19/0.54  (zenon_Vld != zenon_Vuf)
% 0.19/0.54  (zenon_Vdc != zenon_Vhe)
% 0.19/0.54  (zenon_Vld != zenon_Vte)
% 0.19/0.54  (zenon_Vdc != zenon_Vvc)
% 0.19/0.54  (zenon_Vbc != zenon_Vff)
% 0.19/0.54  (-. (p1 zenon_Vkb))
% 0.19/0.54  (zenon_Vld != zenon_Vlc)
% 0.19/0.54  (zenon_Vjd != zenon_Vkc)
% 0.19/0.54  (zenon_Vbc != zenon_Vvc)
% 0.19/0.54  (zenon_Vld != zenon_Vkc)
% 0.19/0.54  (zenon_Vdc != zenon_Vfb)
% 0.19/0.54  (zenon_Vdc != zenon_Vwc)
% 0.19/0.54  (zenon_Vjd != zenon_Vkf)
% 0.19/0.54  (zenon_Vdc != zenon_Vcc)
% 0.19/0.54  (zenon_Vbc != zenon_Vx)
% 0.19/0.54  (-. (p1 zenon_Vgc))
% 0.19/0.54  (zenon_Vld != zenon_Vie)
% 0.19/0.54  (zenon_Vjd != zenon_Vae)
% 0.19/0.54  (-. (p1 zenon_Vx))
% 0.19/0.54  (zenon_Vld != zenon_Vua)
% 0.19/0.54  (zenon_Vdc != zenon_Vda)
% 0.19/0.54  (zenon_Vjd != zenon_Vx)
% 0.19/0.54  (zenon_Vjd != zenon_Vwc)
% 0.19/0.54  (zenon_Vdc != zenon_Vpa)
% 0.19/0.54  (zenon_Vbc != zenon_Vgc)
% 0.19/0.54  (-. (p1 zenon_Vef))
% 0.19/0.54  (zenon_Vbc != zenon_Vlc)
% 0.19/0.54  (-. (p1 zenon_Vcc))
% 0.19/0.54  (zenon_Vdc != zenon_Vua)
% 0.19/0.54  (zenon_Vjd != zenon_Vte)
% 0.19/0.54  (zenon_Vbc != zenon_Vhd)
% 0.19/0.54  (zenon_Vdc != zenon_Vue)
% 0.19/0.54  (r1 zenon_Vub zenon_Vbc)
% 0.19/0.54  (r1 zenon_Vbd zenon_Vcd)
% 0.19/0.54  (zenon_Vld != zenon_Vgc)
% 0.19/0.54  (r1 zenon_X10 zenon_Vof)
% 0.19/0.54  (zenon_Vjd != zenon_Vue)
% 0.19/0.54  (-. (p1 zenon_Vqc))
% 0.19/0.54  *)
% 0.19/0.54  (* NO-PROOF *)
% 0.19/0.54  % SZS status GaveUp
% 0.19/0.54  Number of rewrites on terms: 0
% 0.19/0.54  Number of rewrites on props: 0
% 0.19/0.54  nodes searched: 398
% 0.19/0.54  max branch formulas: 470
% 0.19/0.54  proof nodes created: 0
% 0.19/0.54  formulas created: 2676
% 0.19/0.54  
%------------------------------------------------------------------------------