↑ Up

ZenonModulo---0.5.0.UNK-Non.f

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

% Computer : n031.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:22 PM UTC 2026

% Result   : Unknown 0.46s 0.77s
% Output   : None 
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04  % Problem  : LCL669+1.005 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04  % Command  : run_zenon_modulo %d %s
% 0.18/0.42  % Computer : n031.cluster.edu
% 0.18/0.42  % Model    : x86_64 x86_64
% 0.18/0.42  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.42  % Memory   : 8046.5625MB
% 0.18/0.42  % OS       : Linux 6.8.0-71-generic
% 0.18/0.42  % CPULimit : 300
% 0.18/0.42  % WCLimit  : 300
% 0.18/0.42  % DateTime : Sat Sep  5 08:33:54 UTC 2026
% 0.18/0.43  % CPUTime  : 
% 0.46/0.77  Zenon error: exhausted search space without finding a proof
% 0.46/0.77  (* Current branch:
% 0.46/0.77  (-. (p3 zenon_Vgh))
% 0.46/0.77  (-. (p9 zenon_Vof))
% 0.46/0.77  (r1 zenon_Vxh zenon_Vyh)
% 0.46/0.77  (-. (p11 zenon_Vpe))
% 0.46/0.77  (zenon_Vvc != zenon_Vwc)
% 0.46/0.77  (r1 zenon_Vob zenon_Vfc)
% 0.46/0.77  (r1 zenon_Vfi zenon_Vgi)
% 0.46/0.77  (-. (p8 zenon_Vnf))
% 0.46/0.77  (-. (p4 zenon_Vhh))
% 0.46/0.77  (r1 zenon_Vt zenon_Vu)
% 0.46/0.77  (r1 zenon_Vtg zenon_Vah)
% 0.46/0.77  (p4 zenon_Vgh)
% 0.46/0.77  (zenon_Vgh != zenon_Vzg)
% 0.46/0.77  (r1 zenon_Vwh zenon_Vxh)
% 0.46/0.77  (p8 zenon_Vyf)
% 0.46/0.77  (-. (p7 zenon_Vjg))
% 0.46/0.77  (r1 zenon_Vth zenon_Vuh)
% 0.46/0.77  (r1 Tau_1 zenon_Vm)
% 0.46/0.77  (r1 zenon_Vu zenon_Vv)
% 0.46/0.77  (-. (p5 zenon_Vah))
% 0.46/0.77  (-. (p4 zenon_Vzg))
% 0.46/0.77  (zenon_Vmb != zenon_Vta)
% 0.46/0.77  (zenon_Vrg != zenon_Vsg)
% 0.46/0.77  (r1 zenon_Vgc zenon_Vwc)
% 0.46/0.77  (-. (p9 zenon_Vbf))
% 0.46/0.77  (p6 zenon_Vrg)
% 0.46/0.77  (r1 zenon_Vag zenon_Vjg)
% 0.46/0.77  (zenon_Vgh != zenon_Vhh)
% 0.46/0.77  (r1 zenon_Vn zenon_Vo)
% 0.46/0.77  (r1 zenon_Vva zenon_Vnb)
% 0.46/0.77  (r1 Tau_3 zenon_Vsh)
% 0.46/0.77  (r1 zenon_Vo zenon_Vp)
% 0.46/0.77  (zenon_Vnf != zenon_Vbf)
% 0.46/0.77  (zenon_Vzg != zenon_Vrg)
% 0.46/0.77  (r1 zenon_Vce zenon_Vpe)
% 0.46/0.77  (-. (p1 zenon_Vrh))
% 0.46/0.77  (r1 zenon_Vyh zenon_Vzh)
% 0.46/0.77  (r1 zenon_Vgi zenon_Vhi)
% 0.46/0.77  (p7 zenon_Vig)
% 0.46/0.77  (zenon_Vbf != zenon_Vcf)
% 0.46/0.77  (zenon_Vae != zenon_Vbe)
% 0.46/0.77  (r1 zenon_Vai zenon_Vbi)
% 0.46/0.77  (-. (p15 zenon_Vmb))
% 0.46/0.77  (r1 zenon_Vdf zenon_Vof)
% 0.46/0.77  (p2 zenon_Vba)
% 0.46/0.77  (r1 zenon_Vz zenon_Vaa)
% 0.46/0.77  (r1 zenon_Vkg zenon_Vsg)
% 0.46/0.77  (zenon_Vbf != zenon_Voe)
% 0.46/0.77  (p13 zenon_Vld)
% 0.46/0.77  (r1 zenon_Vbh zenon_Vhh)
% 0.46/0.77  (r1 zenon_Vp zenon_Vq)
% 0.46/0.77  (-. (p16 zenon_Vta))
% 0.46/0.77  (zenon_Vta != zenon_Vhi)
% 0.46/0.77  (r1 zenon_Vvh zenon_Vwh)
% 0.46/0.77  (p11 zenon_Voe)
% 0.46/0.77  (zenon_Vae != zenon_Vld)
% 0.46/0.77  (zenon_Vnf != zenon_Vof)
% 0.46/0.77  (zenon_Vzg != zenon_Vah)
% 0.46/0.77  (r1 zenon_Vaa zenon_Vba)
% 0.46/0.77  (p3 zenon_Vmh)
% 0.46/0.77  (zenon_Vec != zenon_Vfc)
% 0.46/0.77  (r1 zenon_Vq zenon_Vr)
% 0.46/0.77  (-. (p10 zenon_Vcf))
% 0.46/0.77  (zenon_Vmh != zenon_Vnh)
% 0.46/0.77  (zenon_Voe != zenon_Vae)
% 0.46/0.77  (r1 zenon_Vx zenon_Vy)
% 0.46/0.77  (zenon_Vld != zenon_Vvc)
% 0.46/0.77  (zenon_Vmb != zenon_Vnb)
% 0.46/0.77  (r1 zenon_Vsh zenon_Vth)
% 0.46/0.77  (-. (p12 zenon_Vld))
% 0.46/0.77  (zenon_Vec != zenon_Vmb)
% 0.46/0.77  (r1 zenon_Vzh zenon_Vai)
% 0.46/0.77  (-. (p13 zenon_Vmd))
% 0.46/0.77  (-. (p14 zenon_Vec))
% 0.46/0.77  (r1 Tau_0 Tau_2)
% 0.46/0.77  (p9 zenon_Vnf)
% 0.46/0.77  (r1 zenon_Vy zenon_Vz)
% 0.46/0.77  (zenon_Voe != zenon_Vpe)
% 0.46/0.77  (-. (p11 zenon_Vae))
% 0.46/0.77  (-. (p3 zenon_Vnh))
% 0.46/0.77  (zenon_Vyf != zenon_Vnf)
% 0.46/0.77  (zenon_Vig != zenon_Vjg)
% 0.46/0.77  (r1 zenon_Vdi zenon_Vei)
% 0.46/0.77  (zenon_Vld != zenon_Vmd)
% 0.46/0.77  (zenon_Vta != zenon_Vrh)
% 0.46/0.77  (zenon_Vig != zenon_Vyf)
% 0.46/0.77  (p1 zenon_Vta)
% 0.46/0.77  (-. (p18 Tau_2))
% 0.46/0.77  (r1 zenon_X4 zenon_Vua)
% 0.46/0.77  (r1 zenon_Vr zenon_Vs)
% 0.46/0.77  (-. (p15 zenon_Vfc))
% 0.46/0.77  (-. (p12 zenon_Vbe))
% 0.46/0.77  (r1 Tau_0 Tau_1)
% 0.46/0.77  (r1 zenon_Vbi zenon_Vci)
% 0.46/0.77  (-. (p16 zenon_Vnb))
% 0.46/0.77  (r1 zenon_Vpf zenon_Vzf)
% 0.46/0.77  (r1 zenon_Vxc zenon_Vmd)
% 0.46/0.77  (p12 zenon_Vae)
% 0.46/0.77  (-. (p8 zenon_Vzf))
% 0.46/0.77  (p14 zenon_Vvc)
% 0.46/0.77  (zenon_Vmh != zenon_Vgh)
% 0.46/0.77  (-. (p2 zenon_Vmh))
% 0.46/0.77  (zenon_Vyf != zenon_Vzf)
% 0.46/0.77  (zenon_Vrh != zenon_Vmh)
% 0.46/0.77  (-. (p6 zenon_Vig))
% 0.46/0.77  (r1 zenon_Vs zenon_Vt)
% 0.46/0.77  (zenon_Vvc != zenon_Vec)
% 0.46/0.77  (-. (p6 zenon_Vsg))
% 0.46/0.77  (r1 zenon_Vih zenon_Vnh)
% 0.46/0.77  (r1 zenon_Vuh zenon_Vvh)
% 0.46/0.77  (-. (p5 zenon_Vrg))
% 0.46/0.77  (-. (p1 zenon_Vhi))
% 0.46/0.77  (r1 zenon_Vnd zenon_Vbe)
% 0.46/0.77  (r1 zenon_Vci zenon_Vdi)
% 0.46/0.77  (r1 zenon_Vv zenon_Vw)
% 0.46/0.77  (p15 zenon_Vec)
% 0.46/0.77  (-. (p17 zenon_Vua))
% 0.46/0.77  (r1 zenon_Vm zenon_Vn)
% 0.46/0.77  (r1 Tau_0 Tau_3)
% 0.46/0.77  (r1 zenon_Vw zenon_Vx)
% 0.46/0.77  (r1 zenon_Vei zenon_Vfi)
% 0.46/0.77  (p2 zenon_Vrh)
% 0.46/0.77  (-. (p10 zenon_Voe))
% 0.46/0.77  (r1 zenon_Vqe zenon_Vcf)
% 0.46/0.77  (-. (p7 zenon_Vyf))
% 0.46/0.77  (p16 zenon_Vmb)
% 0.46/0.77  (p5 zenon_Vzg)
% 0.46/0.77  (-. (p13 zenon_Vvc))
% 0.46/0.77  (p10 zenon_Vbf)
% 0.46/0.77  (zenon_Vrg != zenon_Vig)
% 0.46/0.77  (zenon_Vba != zenon_Vmh)
% 0.46/0.77  (-. (p14 zenon_Vwc))
% 0.46/0.77  *)
% 0.46/0.77  (* NO-PROOF *)
% 0.46/0.77  % SZS status GaveUp
% 0.46/0.77  Number of rewrites on terms: 0
% 0.46/0.77  Number of rewrites on props: 0
% 0.46/0.77  nodes searched: 636
% 0.46/0.77  max branch formulas: 735
% 0.46/0.77  proof nodes created: 0
% 0.46/0.77  formulas created: 3647
% 0.46/0.77  
%------------------------------------------------------------------------------