↑ Up

ZenonModulo---0.5.0.UNK-Non.f

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

% Computer : n016.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:21 PM UTC 2026

% Result   : Unknown 7.03s 7.39s
% Output   : None 
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02  % Problem  : LCL663+1.015 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.02  % Command  : run_zenon_modulo %d %s
% 0.10/0.35  % Computer : n016.cluster.edu
% 0.10/0.35  % Model    : x86_64 x86_64
% 0.10/0.35  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35  % Memory   : 8046.5625MB
% 0.10/0.35  % OS       : Linux 6.8.0-71-generic
% 0.10/0.35  % CPULimit : 300
% 0.10/0.35  % WCLimit  : 300
% 0.10/0.35  % DateTime : Sat Sep  5 04:44:29 UTC 2026
% 0.10/0.35  % CPUTime  : 
% 7.03/7.39  Zenon error: exhausted search space without finding a proof
% 7.03/7.39  (* Current branch:
% 7.03/7.39  (p1 zenon_Vhva)
% 7.03/7.39  (r1 zenon_Vwia zenon_Vxia)
% 7.03/7.39  (r1 zenon_Vdda zenon_Veda)
% 7.03/7.39  (zenon_Vrba != zenon_Vaib)
% 7.03/7.39  (r1 zenon_Vgu zenon_Vhu)
% 7.03/7.39  (r1 zenon_Vdta zenon_Veta)
% 7.03/7.39  (p1 zenon_Vxg)
% 7.03/7.39  (r1 zenon_Vcs zenon_Vds)
% 7.03/7.39  (r1 zenon_Vdd zenon_Ved)
% 7.03/7.39  (r1 zenon_Vyh zenon_Vzh)
% 7.03/7.39  (r1 zenon_Vdba zenon_Veba)
% 7.03/7.39  (r1 zenon_Vet zenon_Vft)
% 7.03/7.39  (r1 zenon_Vbsa zenon_Vcsa)
% 7.03/7.39  (p1 zenon_Vqma)
% 7.03/7.39  (r1 zenon_Vbwa zenon_Vcwa)
% 7.03/7.39  (r1 zenon_Vzy zenon_Vaz)
% 7.03/7.39  (r1 zenon_Vbc zenon_Vcc)
% 7.03/7.39  (r1 zenon_Vmq zenon_Vnq)
% 7.03/7.39  (r1 zenon_Vgm zenon_Vhm)
% 7.03/7.39  (r1 zenon_Vola zenon_Vpla)
% 7.03/7.39  (p1 zenon_Vlha)
% 7.03/7.39  (zenon_Vxg != zenon_Vaib)
% 7.03/7.39  (r1 zenon_Vyp zenon_Vzp)
% 7.03/7.39  (r1 zenon_Vsqa zenon_Vtqa)
% 7.03/7.39  (r1 zenon_Vtea zenon_Vuea)
% 7.03/7.39  (zenon_Vrfb != zenon_Vaib)
% 7.03/7.39  (r1 zenon_Vhf zenon_Vif)
% 7.03/7.39  (r1 zenon_Vpsa zenon_Vqsa)
% 7.03/7.39  (r1 zenon_Vx zenon_Vy)
% 7.03/7.39  (zenon_Vxg != Tau_0)
% 7.03/7.39  (zenon_Vko != Tau_0)
% 7.03/7.39  (zenon_Viv != Tau_0)
% 7.03/7.39  (zenon_Vrba != Tau_0)
% 7.03/7.39  (zenon_Vlha != Tau_0)
% 7.03/7.39  (zenon_Vqma != Tau_0)
% 7.03/7.39  (zenon_Vgra != Tau_0)
% 7.03/7.39  (zenon_Vhva != Tau_0)
% 7.03/7.39  (zenon_Vtya != Tau_0)
% 7.03/7.39  (zenon_Vqbb != Tau_0)
% 7.03/7.39  (zenon_Vydb != Tau_0)
% 7.03/7.39  (zenon_Vrfb != Tau_0)
% 7.03/7.39  (zenon_Vvgb != Tau_0)
% 7.03/7.39  (r1 zenon_Vpca zenon_Vqca)
% 7.03/7.39  (r1 zenon_Viia zenon_Vjia)
% 7.03/7.39  (r1 zenon_Veqa zenon_Vfqa)
% 7.03/7.39  (r1 zenon_Vfea zenon_Vgea)
% 7.03/7.39  (r1 zenon_Vvfa zenon_Vwfa)
% 7.03/7.39  (zenon_Viv != zenon_Vaib)
% 7.03/7.39  (p1 zenon_Vrfb)
% 7.03/7.39  (zenon_Vydb != zenon_Vaib)
% 7.03/7.39  (r1 zenon_Vnb zenon_Vob)
% 7.03/7.39  (r1 zenon_Vvf zenon_Vwf)
% 7.03/7.39  (zenon_Vqma != zenon_Vaib)
% 7.03/7.39  (r1 zenon_Vin zenon_Vjn)
% 7.03/7.39  (r1 zenon_Vpeb zenon_Vqeb)
% 7.03/7.39  (zenon_Vtya != zenon_Vaib)
% 7.03/7.39  (r1 zenon_Vjx zenon_Vkx)
% 7.03/7.39  (r1 zenon_Vpaa zenon_Vqaa)
% 7.03/7.39  (r1 zenon_Vyja zenon_Vzja)
% 7.03/7.39  (r1 zenon_Vdxa zenon_Vexa)
% 7.03/7.39  (p1 zenon_Vqbb)
% 7.03/7.39  (r1 zenon_Vcpa zenon_Vdpa)
% 7.03/7.39  (r1 zenon_Vjga zenon_Vkga)
% 7.03/7.39  (zenon_Vgra != zenon_Vaib)
% 7.03/7.39  (r1 zenon_Vmza zenon_Vnza)
% 7.03/7.39  (r1 zenon_Vrda zenon_Vsda)
% 7.03/7.39  (r1 zenon_Vly zenon_Vmy)
% 7.03/7.39  (r1 zenon_Vrd zenon_Vsd)
% 7.03/7.39  (r1 zenon_Vpwa zenon_Vqwa)
% 7.03/7.39  (r1 zenon_Vqpa zenon_Vrpa)
% 7.03/7.39  (zenon_Vvgb != zenon_Vaib)
% 7.03/7.39  (r1 zenon_Vpc zenon_Vqc)
% 7.03/7.39  (p1 zenon_Vrba)
% 7.03/7.39  (r1 zenon_Vfya zenon_Vgya)
% 7.03/7.39  (zenon_Vlha != zenon_Vaib)
% 7.03/7.39  (r1 zenon_Vqk zenon_Vrk)
% 7.03/7.39  (r1 zenon_Vwn zenon_Vxn)
% 7.03/7.39  (r1 zenon_Vbaa zenon_Vcaa)
% 7.03/7.39  (r1 zenon_Vum zenon_Vvm)
% 7.03/7.39  (r1 zenon_Vmna zenon_Vnna)
% 7.03/7.39  (r1 zenon_Vfua zenon_Vgua)
% 7.03/7.39  (r1 zenon_Vkja zenon_Vlja)
% 7.03/7.39  (r1 zenon_Vwcb zenon_Vxcb)
% 7.03/7.39  (r1 zenon_Vaab zenon_Vbab)
% 7.03/7.39  (p1 zenon_Viv)
% 7.03/7.39  (r1 zenon_Vxx zenon_Vyx)
% 7.03/7.39  (zenon_Vqbb != zenon_Vaib)
% 7.03/7.39  (r1 zenon_Vrta zenon_Vsta)
% 7.03/7.39  (r1 zenon_Vhfa zenon_Vifa)
% 7.03/7.39  (r1 zenon_Vel zenon_Vfl)
% 7.03/7.39  (r1 zenon_Vor zenon_Vpr)
% 7.03/7.39  (r1 zenon_Vla zenon_Vma)
% 7.03/7.39  (r1 zenon_Vcbb zenon_Vdbb)
% 7.03/7.39  (r1 zenon_X14 zenon_Vigb)
% 7.03/7.39  (p1 zenon_Vtya)
% 7.03/7.39  (r1 zenon_Vte zenon_Vue)
% 7.03/7.39  (r1 zenon_Vkdb zenon_Vldb)
% 7.03/7.39  (r1 zenon_Voj zenon_Vpj)
% 7.03/7.39  (p1 zenon_Vko)
% 7.03/7.39  (p1 zenon_Vvgb)
% 7.03/7.39  (p1 zenon_Vydb)
% 7.03/7.39  (r1 zenon_Var zenon_Vbr)
% 7.03/7.39  (r1 zenon_Vtua zenon_Vuua)
% 7.03/7.39  (r1 zenon_Vaj zenon_Vbj)
% 7.03/7.39  (r1 zenon_Vqs zenon_Vrs)
% 7.03/7.39  (r1 zenon_X1 zenon_Vmhb)
% 7.03/7.39  (zenon_Vko != zenon_Vaib)
% 7.03/7.39  (p1 zenon_Vgra)
% 7.03/7.39  (r1 zenon_Vala zenon_Vbla)
% 7.03/7.39  (zenon_Vhva != zenon_Vaib)
% 7.03/7.39  (r1 zenon_Vooa zenon_Vpoa)
% 7.03/7.39  (r1 zenon_Vrxa zenon_Vsxa)
% 7.03/7.39  (r1 zenon_Vfe zenon_Vge)
% 7.03/7.39  (r1 zenon_Vcma zenon_Vdma)
% 7.03/7.39  (r1 zenon_Vmi zenon_Vni)
% 7.03/7.39  (r1 zenon_Vza zenon_Vab)
% 7.03/7.39  (r1 zenon_Vck zenon_Vdk)
% 7.03/7.39  (r1 zenon_Vsl zenon_Vtl)
% 7.03/7.39  (r1 zenon_Vdfb zenon_Vefb)
% 7.03/7.39  (r1 zenon_Vaoa zenon_Vboa)
% 7.03/7.39  (-. (p1 zenon_Vaib))
% 7.03/7.39  (r1 zenon_Vmka zenon_Vnka)
% 7.03/7.39  (r1 zenon_Vhw zenon_Viw)
% 7.03/7.39  (r1 zenon_Vvw zenon_Vww)
% 7.03/7.39  (r1 zenon_Voab zenon_Vpab)
% 7.03/7.39  (r1 zenon_Vxga zenon_Vyga)
% 7.03/7.39  (r1 zenon_Vicb zenon_Vjcb)
% 7.03/7.39  (-. (p1 Tau_0))
% 7.03/7.39  (r1 zenon_Vnz zenon_Voz)
% 7.03/7.39  (r1 zenon_Vkp zenon_Vlp)
% 7.03/7.39  (r1 zenon_Vjg zenon_Vkg)
% 7.03/7.39  (r1 zenon_Vst zenon_Vtt)
% 7.03/7.39  (r1 zenon_Vuu zenon_Vvu)
% 7.03/7.39  *)
% 7.03/7.39  (* NO-PROOF *)
% 7.03/7.39  % SZS status GaveUp
% 7.03/7.39  Number of rewrites on terms: 0
% 7.03/7.39  Number of rewrites on props: 0
% 7.03/7.39  nodes searched: 2979
% 7.03/7.39  max branch formulas: 3084
% 7.03/7.39  proof nodes created: 1
% 7.03/7.39  formulas created: 14155
% 7.03/7.39  
%------------------------------------------------------------------------------