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

% Computer : n017.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.39s 0.64s
% Output   : None 
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02  % Problem  : LCL659+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 : n017.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.35  % CPULimit : 300
% 0.08/0.35  % WCLimit  : 300
% 0.08/0.35  % DateTime : Fri Sep  4 15:39:05 UTC 2026
% 0.08/0.35  % CPUTime  : 
% 0.39/0.64  Zenon error: exhausted search space without finding a proof
% 0.39/0.64  (* Current branch:
% 0.39/0.64  (zenon_Vke != zenon_Vah)
% 0.39/0.64  (r1 zenon_Vjg zenon_Vmg)
% 0.39/0.64  (r1 Tau_0 Tau_1)
% 0.39/0.64  (-. (p1 zenon_Vgi))
% 0.39/0.64  (zenon_Vke != zenon_Vpi)
% 0.39/0.64  (zenon_Vme != zenon_Vbd)
% 0.39/0.64  (zenon_Vme != zenon_Vng)
% 0.39/0.64  (zenon_Vme != zenon_Vpi)
% 0.39/0.64  (-. (p1 zenon_Vvi))
% 0.39/0.64  (zenon_Vke != zenon_Vjc)
% 0.39/0.64  (r1 zenon_Vfe zenon_Vse)
% 0.39/0.64  (zenon_Vof != zenon_Vlh)
% 0.39/0.64  (r1 zenon_Vza zenon_Vcb)
% 0.39/0.64  (zenon_Vof != zenon_Vxa)
% 0.39/0.64  (zenon_Vme != zenon_Vmf)
% 0.39/0.64  (zenon_Vof != zenon_Vyf)
% 0.39/0.64  (-. (p1 zenon_Vkc))
% 0.39/0.64  (r1 zenon_Vjf zenon_Vkf)
% 0.39/0.64  (zenon_Vof != zenon_Vjc)
% 0.39/0.64  (zenon_Vke != zenon_Vmh)
% 0.39/0.64  (zenon_Vke != zenon_Vha)
% 0.39/0.64  (zenon_Vke != zenon_Vgi)
% 0.39/0.64  (-. (p1 zenon_Vmh))
% 0.39/0.64  (-. (p1 zenon_Vmg))
% 0.39/0.64  (zenon_Vof != zenon_Vsg)
% 0.39/0.64  (-. (p1 zenon_Vte))
% 0.39/0.64  (zenon_Vke != zenon_Vhi)
% 0.39/0.64  (zenon_Vme != zenon_Vqi)
% 0.39/0.64  (zenon_Vof != zenon_Vwa)
% 0.39/0.64  (zenon_Vke != zenon_Vsd)
% 0.39/0.64  (-. (p1 zenon_Vpe))
% 0.39/0.64  (zenon_Vof != zenon_Vef)
% 0.39/0.64  (zenon_Vof != zenon_Vca)
% 0.39/0.64  (zenon_Vme != zenon_Vyd)
% 0.39/0.64  (zenon_Vof != zenon_Vvi)
% 0.39/0.64  (zenon_Vof != zenon_Vmh)
% 0.39/0.64  (r1 zenon_Vlf zenon_Vmf)
% 0.39/0.64  (r1 Tau_1 zenon_Vgf)
% 0.39/0.64  (-. (p1 zenon_Vlh))
% 0.39/0.64  (zenon_Vof != zenon_Vpc)
% 0.39/0.64  (zenon_Vof != zenon_Vsd)
% 0.39/0.64  (zenon_Vof != zenon_Vrb)
% 0.39/0.64  (p1 zenon_Vke)
% 0.39/0.64  (zenon_Vme != zenon_Vle)
% 0.39/0.64  (zenon_Vof != zenon_Vzg)
% 0.39/0.64  (-. (p1 zenon_Vwh))
% 0.39/0.64  (zenon_Vme != zenon_Vzg)
% 0.39/0.64  (r1 zenon_Vfe zenon_Vdf)
% 0.39/0.64  (zenon_Vof != zenon_Vhd)
% 0.39/0.64  (r1 zenon_Vpg zenon_Vsg)
% 0.39/0.64  (zenon_Vke != zenon_Vpc)
% 0.39/0.64  (r1 zenon_Vdi zenon_Vgi)
% 0.39/0.64  (zenon_Vme != zenon_Vfh)
% 0.39/0.64  (r1 zenon_Vgc zenon_Vjc)
% 0.39/0.64  (zenon_Vme != zenon_Vsd)
% 0.39/0.64  (zenon_Vof != zenon_Vcb)
% 0.39/0.64  (zenon_Vke != zenon_Veg)
% 0.39/0.64  (-. (p1 zenon_Vrh))
% 0.39/0.64  (zenon_Vme != zenon_Vse)
% 0.39/0.64  (zenon_Vme != zenon_Vyf)
% 0.39/0.64  (zenon_Vke != zenon_Vci)
% 0.39/0.64  (zenon_Vof != zenon_Vzf)
% 0.39/0.64  (zenon_Vme != zenon_Vwb)
% 0.39/0.64  (r1 zenon_Vih zenon_Vlh)
% 0.39/0.64  (zenon_Vme != zenon_Vci)
% 0.39/0.64  (zenon_Vke != zenon_Vkc)
% 0.39/0.64  (zenon_Vme != zenon_Vvi)
% 0.39/0.64  (-. (p1 zenon_Vle))
% 0.39/0.64  (zenon_Vke != zenon_Vle)
% 0.39/0.64  (zenon_Vke != zenon_Vlh)
% 0.39/0.64  (zenon_Vke != zenon_Vef)
% 0.39/0.64  (-. (p1 zenon_Vcd))
% 0.39/0.64  (zenon_Vof != zenon_Vpf)
% 0.39/0.64  (zenon_Vme != zenon_Vef)
% 0.39/0.64  (-. (p1 zenon_Vyd))
% 0.39/0.64  (r1 zenon_Vgf zenon_Vhf)
% 0.39/0.64  (zenon_Vof != zenon_Vkc)
% 0.39/0.64  (zenon_Vof != zenon_Vng)
% 0.39/0.64  (zenon_Vke != zenon_Vcd)
% 0.39/0.64  (zenon_Vke != zenon_Vxh)
% 0.39/0.64  (zenon_Vke != zenon_Vhd)
% 0.39/0.64  (zenon_Vof != zenon_Vse)
% 0.39/0.64  (-. (p1 zenon_Veg))
% 0.39/0.64  (zenon_Vme != zenon_Vpf)
% 0.39/0.64  (-. (p1 zenon_Vba))
% 0.39/0.64  (-. (p1 zenon_Vse))
% 0.39/0.64  (zenon_Vke != zenon_Vwa)
% 0.39/0.64  (r1 zenon_Ved zenon_Vhd)
% 0.39/0.64  (zenon_Vke != zenon_Vdf)
% 0.39/0.64  (zenon_Vof != zenon_Vba)
% 0.39/0.64  (zenon_Vke != zenon_Vqb)
% 0.39/0.64  (r1 zenon_Vy zenon_Vba)
% 0.39/0.64  (zenon_Vof != zenon_Vmi)
% 0.39/0.64  (zenon_Vme != zenon_Vgi)
% 0.39/0.64  (r1 zenon_Voh zenon_Vrh)
% 0.39/0.64  (r1 zenon_Vbg zenon_Veg)
% 0.39/0.64  (zenon_Vme != zenon_Vlh)
% 0.39/0.64  (r1 zenon_Vke zenon_Vle)
% 0.39/0.64  (-. (p1 zenon_Vcb))
% 0.39/0.64  (zenon_Vke != zenon_Vwh)
% 0.39/0.64  (zenon_Vke != zenon_Vxa)
% 0.39/0.64  (zenon_Vof != zenon_Vha)
% 0.39/0.64  (zenon_Vke != zenon_Vsg)
% 0.39/0.64  (r1 zenon_Vkf zenon_Vlf)
% 0.39/0.64  (-. (p1 zenon_Vpi))
% 0.39/0.64  (r1 zenon_Vhf zenon_Vif)
% 0.39/0.64  (r1 zenon_Vch zenon_Vfh)
% 0.39/0.64  (r1 zenon_Vof zenon_Vpf)
% 0.39/0.64  (zenon_Vme != zenon_Vcb)
% 0.39/0.64  (zenon_Vke != zenon_Vyd)
% 0.39/0.64  (-. (p1 zenon_Vtd))
% 0.39/0.64  (zenon_Vof != zenon_Vbd)
% 0.39/0.64  (-. (p1 zenon_Vxa))
% 0.39/0.64  (r1 zenon_Vtb zenon_Vwb)
% 0.39/0.64  (zenon_Vme != zenon_Vjc)
% 0.39/0.64  (-. (p1 zenon_Vmi))
% 0.39/0.64  (zenon_Vke != zenon_Vca)
% 0.39/0.64  (zenon_Vme != zenon_Vkc)
% 0.39/0.64  (zenon_Vof != zenon_Vle)
% 0.39/0.64  (-. (p1 zenon_Vhd))
% 0.39/0.64  (-. (p1 zenon_Vah))
% 0.39/0.64  (zenon_Vof != zenon_Vte)
% 0.39/0.64  (zenon_Vke != zenon_Vpe)
% 0.39/0.64  (-. (p1 zenon_Vjc))
% 0.39/0.64  (zenon_Vke != zenon_Vng)
% 0.39/0.64  (r1 zenon_Vme zenon_Vpe)
% 0.39/0.64  (zenon_Vof != zenon_Vpi)
% 0.39/0.64  (zenon_Vme != zenon_Vcd)
% 0.39/0.64  (zenon_Vof != zenon_Vmg)
% 0.39/0.64  (zenon_Vof != zenon_Vwh)
% 0.39/0.64  (-. (p1 zenon_Vmf))
% 0.39/0.64  (-. (p1 zenon_Vye))
% 0.39/0.64  (zenon_Vke != zenon_Vte)
% 0.39/0.64  (-. (p1 zenon_Vpc))
% 0.39/0.64  (zenon_Vof != zenon_Vyd)
% 0.39/0.64  (zenon_Vme != zenon_Veg)
% 0.39/0.64  (r1 zenon_Vea zenon_Vha)
% 0.39/0.64  (-. (p1 zenon_Vzf))
% 0.39/0.64  (zenon_Vof != zenon_Vcd)
% 0.39/0.64  (-. (p1 zenon_Vxh))
% 0.39/0.64  (r1 zenon_Vvd zenon_Vyd)
% 0.39/0.64  (r1 zenon_Vth zenon_Vwh)
% 0.39/0.64  (zenon_Vme != zenon_Vqb)
% 0.39/0.64  (-. (p1 zenon_Vng))
% 0.39/0.64  (-. (p1 zenon_Vdf))
% 0.39/0.64  (zenon_Vof != zenon_Vye)
% 0.39/0.64  (zenon_Vme != zenon_Vwa)
% 0.39/0.64  (zenon_Vke != zenon_Vvi)
% 0.39/0.64  (r1 zenon_Vve zenon_Vye)
% 0.39/0.64  (-. (p1 zenon_Vsd))
% 0.39/0.64  (zenon_Vof != zenon_Vxh)
% 0.39/0.64  (zenon_Vme != zenon_Vha)
% 0.39/0.64  (r1 zenon_Vsi zenon_Vvi)
% 0.39/0.64  (r1 zenon_Vzh zenon_Vci)
% 0.39/0.64  (zenon_Vme != zenon_Vca)
% 0.39/0.64  (zenon_Vme != zenon_Vah)
% 0.39/0.64  (-. (p1 zenon_Vha))
% 0.39/0.64  (zenon_Vof != zenon_Vpe)
% 0.39/0.64  (p1 zenon_Vme)
% 0.39/0.64  (r1 zenon_Vif zenon_Vjf)
% 0.39/0.64  (zenon_Vke != zenon_Vba)
% 0.39/0.64  (zenon_Vof != zenon_Vdf)
% 0.39/0.64  (r1 zenon_Vmc zenon_Vpc)
% 0.39/0.64  (-. (p1 zenon_Vsg))
% 0.39/0.64  (zenon_Vme != zenon_Vmh)
% 0.39/0.64  (p1 zenon_Vof)
% 0.39/0.64  (zenon_Vme != zenon_Vba)
% 0.39/0.64  (zenon_Vke != zenon_Vpf)
% 0.39/0.64  (zenon_Vke != zenon_Vfh)
% 0.39/0.64  (zenon_Vme != zenon_Vdf)
% 0.39/0.64  (zenon_Vof != zenon_Vtd)
% 0.39/0.64  (zenon_Vke != zenon_Vzg)
% 0.39/0.64  (zenon_Vof != zenon_Veg)
% 0.39/0.64  (r1 zenon_Vnb zenon_Vqb)
% 0.39/0.64  (zenon_Vke != zenon_Vmi)
% 0.39/0.64  (zenon_Vme != zenon_Vye)
% 0.39/0.64  (zenon_Vof != zenon_Vgi)
% 0.39/0.64  (r1 zenon_Vta zenon_Vwa)
% 0.39/0.64  (r1 zenon_Vnf zenon_Vof)
% 0.39/0.64  (r1 zenon_Vwg zenon_Vzg)
% 0.39/0.64  (r1 zenon_Vpd zenon_Vsd)
% 0.39/0.64  (-. (p1 zenon_Vfh))
% 0.39/0.64  (zenon_Vme != zenon_Vrb)
% 0.39/0.64  (zenon_Vof != zenon_Vmf)
% 0.39/0.64  (-. (p1 zenon_Vpf))
% 0.39/0.64  (zenon_Vme != zenon_Vhd)
% 0.39/0.64  (zenon_Vme != zenon_Vmg)
% 0.39/0.64  (zenon_Vke != zenon_Vyf)
% 0.39/0.64  (r1 zenon_Vji zenon_Vmi)
% 0.39/0.64  (zenon_Vof != zenon_Vah)
% 0.39/0.64  (-. (p1 zenon_Vrb))
% 0.39/0.64  (r1 zenon_X15 zenon_Vpi)
% 0.39/0.64  (zenon_Vme != zenon_Vmi)
% 0.39/0.64  (zenon_Vme != zenon_Vtd)
% 0.39/0.64  (zenon_Vme != zenon_Vxa)
% 0.39/0.64  (zenon_Vof != zenon_Vqi)
% 0.39/0.64  (zenon_Vke != zenon_Vrh)
% 0.39/0.64  (-. (p1 zenon_Vhi))
% 0.39/0.64  (zenon_Vke != zenon_Vcb)
% 0.39/0.64  (zenon_Vke != zenon_Vtd)
% 0.39/0.64  (zenon_Vke != zenon_Vmg)
% 0.39/0.64  (zenon_Vme != zenon_Vwh)
% 0.39/0.64  (zenon_Vke != zenon_Vwb)
% 0.39/0.64  (zenon_Vme != zenon_Vpe)
% 0.39/0.64  (-. (p1 zenon_Vyf))
% 0.39/0.64  (-. (p1 zenon_Vqb))
% 0.39/0.64  (-. (p1 zenon_Vwb))
% 0.39/0.64  (zenon_Vke != zenon_Vye)
% 0.39/0.64  (zenon_Vke != zenon_Vzf)
% 0.39/0.64  (zenon_Vof != zenon_Vci)
% 0.39/0.64  (r1 zenon_Vyc zenon_Vbd)
% 0.39/0.64  (zenon_Vof != zenon_Vfh)
% 0.39/0.64  (zenon_Vke != zenon_Vrb)
% 0.39/0.64  (zenon_Vke != zenon_Vqi)
% 0.39/0.64  (zenon_Vof != zenon_Vrh)
% 0.39/0.64  (zenon_Vme != zenon_Vte)
% 0.39/0.64  (zenon_Vke != zenon_Vse)
% 0.39/0.64  (zenon_Vke != zenon_Vmf)
% 0.39/0.64  (zenon_Vme != zenon_Vzf)
% 0.39/0.64  (zenon_Vke != zenon_Vbd)
% 0.39/0.64  (zenon_Vof != zenon_Vhi)
% 0.39/0.64  (zenon_Vof != zenon_Vqb)
% 0.39/0.64  (zenon_Vme != zenon_Vpc)
% 0.39/0.64  (-. (p1 zenon_Vef))
% 0.39/0.64  (-. (p1 zenon_Vca))
% 0.39/0.64  (zenon_Vme != zenon_Vxh)
% 0.39/0.64  (zenon_Vme != zenon_Vsg)
% 0.39/0.64  (-. (p1 zenon_Vqi))
% 0.39/0.64  (r1 zenon_Vvf zenon_Vyf)
% 0.39/0.64  (zenon_Vme != zenon_Vhi)
% 0.39/0.64  (-. (p1 zenon_Vwa))
% 0.39/0.64  (-. (p1 zenon_Vzg))
% 0.39/0.64  (-. (p1 zenon_Vci))
% 0.39/0.64  (zenon_Vof != zenon_Vwb)
% 0.39/0.64  (-. (p1 zenon_Vbd))
% 0.39/0.64  (zenon_Vme != zenon_Vrh)
% 0.39/0.64  (r1 zenon_Vfe zenon_Vke)
% 0.39/0.64  *)
% 0.39/0.64  (* NO-PROOF *)
% 0.39/0.64  % SZS status GaveUp
% 0.39/0.64  Number of rewrites on terms: 0
% 0.39/0.64  Number of rewrites on props: 0
% 0.39/0.64  nodes searched: 560
% 0.39/0.64  max branch formulas: 652
% 0.39/0.64  proof nodes created: 0
% 0.39/0.64  formulas created: 3520
% 0.39/0.64  
%------------------------------------------------------------------------------