↑ Up

ZenonModulo---0.5.0.UNK-Non.f

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

% Computer : n006.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:17 PM UTC 2026

% Result   : Unknown 0.30s 0.59s
% Output   : None 
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : LCL653+1.005 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03  % Command  : run_zenon_modulo %d %s
% 0.10/0.35  % Computer : n006.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 15:15:31 UTC 2026
% 0.10/0.35  % CPUTime  : 
% 0.30/0.58  Zenon error: exhausted search space without finding a proof
% 0.30/0.58  (* Current branch:
% 0.30/0.58  (-. (p3 zenon_Vnc))
% 0.30/0.58  (zenon_Vqe != zenon_Vya)
% 0.30/0.58  (zenon_Vfg != zenon_Vvc)
% 0.30/0.58  (zenon_Vbg != zenon_Vra)
% 0.30/0.58  (r1 zenon_Vyb zenon_Vzb)
% 0.30/0.58  (zenon_Vch != zenon_Vpd)
% 0.30/0.58  (zenon_Vaf != zenon_Vme)
% 0.30/0.58  (zenon_Vch != zenon_Vbf)
% 0.30/0.58  (r1 zenon_Vje zenon_Vme)
% 0.30/0.58  (zenon_Vle != zenon_Vwe)
% 0.30/0.58  (zenon_Vaf != zenon_Vbf)
% 0.30/0.58  (zenon_Vce != zenon_Vfb)
% 0.30/0.58  (r1 zenon_Vsc zenon_Vvc)
% 0.30/0.58  (zenon_Vaf != zenon_Vra)
% 0.30/0.58  (zenon_Vjg != zenon_Vpd)
% 0.30/0.58  (zenon_Vch != zenon_Vhe)
% 0.30/0.58  (zenon_Vch != zenon_Vhd)
% 0.30/0.58  (zenon_Vvg != zenon_Vq)
% 0.30/0.58  (zenon_Vce != zenon_Vdd)
% 0.30/0.58  (r1 Tau_0 Tau_2)
% 0.30/0.58  (zenon_Vqe != zenon_Vvc)
% 0.30/0.58  (zenon_Vve != zenon_Vgf)
% 0.30/0.58  (zenon_Vve != zenon_Vbf)
% 0.30/0.58  (zenon_Vch != zenon_Vtb)
% 0.30/0.58  (zenon_Vzg != zenon_Vme)
% 0.30/0.58  (zenon_Vle != zenon_Vre)
% 0.30/0.58  (zenon_Vaf != zenon_Vxd)
% 0.30/0.58  (zenon_Vff != zenon_Vme)
% 0.30/0.58  (zenon_Vce != zenon_Vtd)
% 0.30/0.58  (zenon_Vbg != zenon_Vld)
% 0.30/0.58  (-. (p1 zenon_Vka))
% 0.30/0.58  (zenon_Vge != zenon_Vpd)
% 0.30/0.58  (zenon_Vqe != zenon_Vre)
% 0.30/0.58  (zenon_Vzg != zenon_Vra)
% 0.30/0.58  (zenon_Vfg != zenon_Vae)
% 0.30/0.58  (zenon_Vge != zenon_Vgf)
% 0.30/0.58  (zenon_Vfg != zenon_Vhd)
% 0.30/0.58  (zenon_Vkf != zenon_Vlf)
% 0.30/0.58  (zenon_Vve != zenon_Vdd)
% 0.30/0.58  (-. (p1 zenon_Vxd))
% 0.30/0.58  (zenon_Vpf != zenon_Vde)
% 0.30/0.58  (zenon_Vpf != zenon_Vhd)
% 0.30/0.58  (zenon_Vle != zenon_Vq)
% 0.30/0.58  (zenon_Vaf != zenon_Vya)
% 0.30/0.58  (p1 zenon_Vce)
% 0.30/0.58  (zenon_Vxf != zenon_Vae)
% 0.30/0.58  (zenon_Vle != zenon_Vlf)
% 0.30/0.58  (zenon_Vfg != zenon_Vtd)
% 0.30/0.58  (zenon_Vxf != zenon_Vka)
% 0.30/0.58  (-. (p1 zenon_Vae))
% 0.30/0.58  (r1 zenon_Vy zenon_Vca)
% 0.30/0.58  (zenon_Vng != zenon_Vtb)
% 0.30/0.58  (zenon_Vxf != zenon_Vw)
% 0.30/0.58  (zenon_Vpf != zenon_Vae)
% 0.30/0.58  (zenon_Vzg != zenon_Vtd)
% 0.30/0.58  (zenon_Vbg != zenon_Vw)
% 0.30/0.58  (zenon_Vkf != zenon_Vpd)
% 0.30/0.58  (zenon_Vge != zenon_Vme)
% 0.30/0.58  (r1 zenon_Vub zenon_Vfc)
% 0.30/0.58  (zenon_Vge != zenon_Vdd)
% 0.30/0.58  (zenon_Vve != zenon_Vlf)
% 0.30/0.58  (zenon_Vfg != zenon_Vwe)
% 0.30/0.58  (zenon_Vbg != zenon_Vme)
% 0.30/0.58  (-. (p1 zenon_Vtb))
% 0.30/0.58  (r1 zenon_Vse zenon_Vxe)
% 0.30/0.58  (p1 zenon_Vrg)
% 0.30/0.58  (zenon_Vce != zenon_Vpd)
% 0.30/0.58  (zenon_Vff != zenon_Vq)
% 0.30/0.58  (zenon_Vpf != zenon_Vtb)
% 0.30/0.58  (r1 Tau_0 Tau_1)
% 0.30/0.58  (zenon_Vff != zenon_Vvc)
% 0.30/0.58  (zenon_Vff != zenon_Vzc)
% 0.30/0.58  (p1 zenon_Vle)
% 0.30/0.58  (zenon_Vkf != zenon_Vld)
% 0.30/0.58  (zenon_Vjg != zenon_Vqf)
% 0.30/0.58  (zenon_Vjg != zenon_Vda)
% 0.30/0.58  (zenon_Vng != zenon_Vhe)
% 0.30/0.58  (zenon_Vle != zenon_Vme)
% 0.30/0.58  (r1 zenon_Vse zenon_Vte)
% 0.30/0.58  (-. (p1 zenon_Vpd))
% 0.30/0.58  (zenon_Vxf != zenon_Vhe)
% 0.30/0.58  (zenon_Vzg != zenon_Vhe)
% 0.30/0.58  (zenon_Vaf != zenon_Vzc)
% 0.30/0.58  (zenon_Vbg != zenon_Vpd)
% 0.30/0.58  (zenon_Vpf != zenon_Vme)
% 0.30/0.58  (zenon_Vff != zenon_Vra)
% 0.30/0.58  (zenon_Vge != zenon_Vhd)
% 0.30/0.58  (r1 zenon_Vwc zenon_Vzc)
% 0.30/0.58  (zenon_Vrg != zenon_Vda)
% 0.30/0.58  (zenon_Vle != zenon_Vka)
% 0.30/0.58  (-. (p1 zenon_Vdd))
% 0.30/0.58  (zenon_Vvg != zenon_Vw)
% 0.30/0.58  (p1 zenon_Vch)
% 0.30/0.58  (zenon_Vxf != zenon_Vme)
% 0.30/0.58  (r1 zenon_Vab zenon_Veb)
% 0.30/0.58  (r1 zenon_Vxe zenon_Vye)
% 0.30/0.58  (zenon_Vng != zenon_Vq)
% 0.30/0.58  (zenon_Vch != zenon_Vfb)
% 0.30/0.58  (zenon_Vpf != zenon_Vdd)
% 0.30/0.58  (zenon_Vjg != zenon_Vfb)
% 0.30/0.58  (r1 zenon_Vub zenon_Vqc)
% 0.30/0.58  (zenon_Vaf != zenon_Vde)
% 0.30/0.58  (zenon_Vbg != zenon_Vya)
% 0.30/0.58  (zenon_Vve != zenon_Vfb)
% 0.30/0.58  (zenon_Vvg != zenon_Vdd)
% 0.30/0.58  (r1 zenon_Voe zenon_Vpe)
% 0.30/0.58  (zenon_Vff != zenon_Vlf)
% 0.30/0.58  (zenon_Vqe != zenon_Vfb)
% 0.30/0.58  (r1 zenon_Vmd zenon_Vpd)
% 0.30/0.58  (zenon_Vaf != zenon_Vqf)
% 0.30/0.58  (zenon_Vvg != zenon_Vmb)
% 0.30/0.58  (zenon_Vle != zenon_Vmb)
% 0.30/0.58  (r1 zenon_Vhb zenon_Vlb)
% 0.30/0.58  (zenon_Vbg != zenon_Vzc)
% 0.30/0.58  (zenon_Vge != zenon_Vae)
% 0.30/0.58  (zenon_Vfg != zenon_Vre)
% 0.30/0.58  (zenon_Vpf != zenon_Vmb)
% 0.30/0.58  (r1 zenon_Vte zenon_Vue)
% 0.30/0.58  (zenon_Vce != zenon_Vbf)
% 0.30/0.58  (zenon_Vch != zenon_Vre)
% 0.30/0.58  (zenon_Vvg != zenon_Vfb)
% 0.30/0.58  (zenon_Vjg != zenon_Vld)
% 0.30/0.58  (zenon_Vqe != zenon_Vda)
% 0.30/0.58  (-. (p4 zenon_X3))
% 0.30/0.58  (zenon_Vkf != zenon_Vw)
% 0.30/0.58  (p1 zenon_Vaf)
% 0.30/0.58  (zenon_Vrg != zenon_Vka)
% 0.30/0.58  (r1 zenon_Vnf zenon_Vqf)
% 0.30/0.58  (zenon_Vch != zenon_Vtd)
% 0.30/0.58  (zenon_Vvg != zenon_Vpd)
% 0.30/0.58  (zenon_Vzg != zenon_Vpd)
% 0.30/0.58  (-. (p1 zenon_Vya))
% 0.30/0.58  (zenon_Vle != zenon_Vhe)
% 0.30/0.58  (r1 zenon_X7 zenon_Vch)
% 0.30/0.58  (zenon_Vve != zenon_Vpd)
% 0.30/0.58  (zenon_Vff != zenon_Vya)
% 0.30/0.58  (zenon_Vge != zenon_Vya)
% 0.30/0.58  (zenon_Vff != zenon_Vw)
% 0.30/0.58  (zenon_Vzg != zenon_Vzc)
% 0.30/0.58  (zenon_Vpf != zenon_Vzc)
% 0.30/0.58  (r1 zenon_Vsf zenon_Vtf)
% 0.30/0.58  (r1 zenon_Vcg zenon_Vfg)
% 0.30/0.58  (zenon_Vpf != zenon_Vtd)
% 0.30/0.58  (r1 zenon_Vdf zenon_Vgf)
% 0.30/0.58  (zenon_Vff != zenon_Vre)
% 0.30/0.58  (zenon_Vng != zenon_Vbf)
% 0.30/0.58  (zenon_Vvg != zenon_Vda)
% 0.30/0.58  (zenon_Vrg != zenon_Vtb)
% 0.30/0.58  (r1 zenon_X4 zenon_Vp)
% 0.30/0.58  (zenon_Vle != zenon_Vbf)
% 0.30/0.58  (-. (p1 zenon_Vvc))
% 0.30/0.58  (zenon_Vkf != zenon_Vq)
% 0.30/0.58  (r1 zenon_Vte zenon_Vwe)
% 0.30/0.58  (zenon_Vng != zenon_Vtd)
% 0.30/0.58  (zenon_Vch != zenon_Vw)
% 0.30/0.58  (r1 zenon_Vr zenon_Vv)
% 0.30/0.58  (zenon_Vce != zenon_Vre)
% 0.30/0.58  (r1 zenon_Vcf zenon_Vhf)
% 0.30/0.58  (zenon_Vaf != zenon_Vdd)
% 0.30/0.58  (zenon_Vve != zenon_Vw)
% 0.30/0.58  (zenon_Vce != zenon_Vmb)
% 0.30/0.58  (zenon_Vfg != zenon_Vgf)
% 0.30/0.58  (zenon_Vve != zenon_Vra)
% 0.30/0.58  (zenon_Vch != zenon_Vwe)
% 0.30/0.58  (p1 zenon_Vzg)
% 0.30/0.58  (zenon_Vbg != zenon_Vhd)
% 0.30/0.58  (zenon_Vve != zenon_Vxd)
% 0.30/0.58  (zenon_Vxf != zenon_Vre)
% 0.30/0.58  (zenon_Vbg != zenon_Vfb)
% 0.30/0.58  (zenon_Vve != zenon_Vwe)
% 0.30/0.58  (p1 zenon_Vff)
% 0.30/0.58  (zenon_Vzg != zenon_Vhd)
% 0.30/0.58  (zenon_Vng != zenon_Vde)
% 0.30/0.58  (zenon_Vce != zenon_Vhe)
% 0.30/0.58  (zenon_Vfg != zenon_Vmb)
% 0.30/0.58  (zenon_Vjg != zenon_Vzc)
% 0.30/0.58  (zenon_Vrg != zenon_Vtd)
% 0.30/0.58  (zenon_Vqe != zenon_Vmb)
% 0.30/0.58  (zenon_Vkf != zenon_Vda)
% 0.30/0.58  (zenon_Vrg != zenon_Vya)
% 0.30/0.58  (r1 zenon_Vif zenon_Vlf)
% 0.30/0.58  (zenon_Vle != zenon_Vya)
% 0.30/0.58  (zenon_Vce != zenon_Vae)
% 0.30/0.58  (zenon_Vvg != zenon_Vgf)
% 0.30/0.58  (p1 zenon_Vjg)
% 0.30/0.58  (zenon_Vng != zenon_Vmb)
% 0.30/0.58  (-. (p1 zenon_Vzc))
% 0.30/0.58  (-. (p1 zenon_Vda))
% 0.30/0.58  (zenon_Vle != zenon_Vtd)
% 0.30/0.58  (zenon_Vbg != zenon_Vde)
% 0.30/0.58  (-. (p1 zenon_Vhe))
% 0.30/0.58  (-. (p1 zenon_Vqf))
% 0.30/0.58  (zenon_Vxf != zenon_Vxd)
% 0.30/0.58  (zenon_Vng != zenon_Vda)
% 0.30/0.58  (zenon_Vfg != zenon_Vde)
% 0.30/0.58  (zenon_Vjg != zenon_Vlf)
% 0.30/0.58  (zenon_Vxf != zenon_Vbf)
% 0.30/0.58  (-. (p1 zenon_Vbf))
% 0.30/0.58  (zenon_Vbg != zenon_Vae)
% 0.30/0.58  (zenon_Vce != zenon_Vya)
% 0.30/0.58  (zenon_Vkf != zenon_Vre)
% 0.30/0.58  (zenon_Vvg != zenon_Vqf)
% 0.30/0.58  (zenon_Vng != zenon_Vzc)
% 0.30/0.58  (zenon_Vjg != zenon_Vtd)
% 0.30/0.58  (zenon_Vvg != zenon_Vae)
% 0.30/0.58  (zenon_Vce != zenon_Vka)
% 0.30/0.58  (zenon_Vle != zenon_Vra)
% 0.30/0.58  (zenon_Vng != zenon_Vra)
% 0.30/0.58  (zenon_Vbg != zenon_Vq)
% 0.30/0.58  (zenon_Vff != zenon_Vhd)
% 0.30/0.58  (zenon_Vbg != zenon_Vbf)
% 0.30/0.58  (zenon_Vle != zenon_Vae)
% 0.30/0.58  (zenon_Vqe != zenon_Vhe)
% 0.30/0.58  (r1 zenon_Vuf zenon_Vxf)
% 0.30/0.58  (r1 zenon_Vfa zenon_Vja)
% 0.30/0.58  (zenon_Vch != zenon_Vde)
% 0.30/0.58  (r1 zenon_Ved zenon_Vhd)
% 0.30/0.58  (zenon_Vve != zenon_Vka)
% 0.30/0.58  (zenon_Vkf != zenon_Vfb)
% 0.30/0.58  (zenon_Vbg != zenon_Vwe)
% 0.30/0.58  (zenon_Vch != zenon_Vgf)
% 0.30/0.58  (zenon_Vce != zenon_Vvc)
% 0.30/0.58  (zenon_Vrg != zenon_Vdd)
% 0.30/0.58  (zenon_Vjg != zenon_Vxd)
% 0.30/0.58  (zenon_Vbg != zenon_Vgf)
% 0.30/0.58  (zenon_Vfg != zenon_Vtb)
% 0.30/0.58  (zenon_Vvg != zenon_Vwe)
% 0.30/0.58  (zenon_Vkf != zenon_Vtd)
% 0.30/0.58  (zenon_Vkf != zenon_Vgf)
% 0.30/0.58  (zenon_Vce != zenon_Vhd)
% 0.30/0.58  (zenon_Vqe != zenon_Vpd)
% 0.30/0.58  (r1 zenon_Vqd zenon_Vtd)
% 0.30/0.58  (zenon_Vaf != zenon_Vgf)
% 0.30/0.58  (zenon_Vvg != zenon_Vtb)
% 0.30/0.58  (zenon_Vvg != zenon_Vre)
% 0.30/0.58  (r1 zenon_Vee zenon_Vfe)
% 0.30/0.58  (zenon_Vrg != zenon_Vvc)
% 0.30/0.58  (zenon_Vve != zenon_Vqf)
% 0.30/0.58  (zenon_Vpf != zenon_Vya)
% 0.30/0.58  (zenon_Vff != zenon_Vxd)
% 0.30/0.58  (zenon_Vjg != zenon_Vwe)
% 0.30/0.58  (zenon_Vkf != zenon_Vmb)
% 0.30/0.58  (-. (p1 zenon_Vre))
% 0.30/0.58  (zenon_Vge != zenon_Vka)
% 0.30/0.58  (zenon_Vjg != zenon_Vhd)
% 0.30/0.58  (zenon_Vff != zenon_Vtb)
% 0.30/0.58  (zenon_Vaf != zenon_Vae)
% 0.30/0.58  (zenon_Vfg != zenon_Vhe)
% 0.30/0.58  (zenon_Vjg != zenon_Vde)
% 0.30/0.58  (zenon_Vve != zenon_Vre)
% 0.30/0.58  (r1 zenon_Vlc zenon_Vmc)
% 0.30/0.59  (zenon_Vxf != zenon_Vde)
% 0.30/0.59  (zenon_Vqe != zenon_Vqf)
% 0.30/0.59  (zenon_Vxf != zenon_Vzc)
% 0.30/0.59  (zenon_Vvg != zenon_Vra)
% 0.30/0.59  (zenon_Vjg != zenon_Vdd)
% 0.30/0.59  (zenon_Vxf != zenon_Vdd)
% 0.30/0.59  (zenon_Vge != zenon_Vda)
% 0.30/0.59  (zenon_Vqe != zenon_Vzc)
% 0.30/0.59  (r1 zenon_Vne zenon_Vse)
% 0.30/0.59  (r1 zenon_Vma zenon_Vqa)
% 0.30/0.59  (zenon_Vrg != zenon_Vme)
% 0.30/0.59  (zenon_Vve != zenon_Vvc)
% 0.30/0.59  (zenon_Vvg != zenon_Vvc)
% 0.30/0.59  (r1 zenon_Voe zenon_Vre)
% 0.30/0.59  (zenon_Vge != zenon_Vqf)
% 0.30/0.59  (r1 zenon_Vmf zenon_Vnf)
% 0.30/0.59  (zenon_Vfg != zenon_Vdd)
% 0.30/0.59  (zenon_Vpf != zenon_Vpd)
% 0.30/0.59  (zenon_Vge != zenon_Vq)
% 0.30/0.59  (zenon_Vxf != zenon_Vq)
% 0.30/0.59  (zenon_Vfg != zenon_Vld)
% 0.30/0.59  (zenon_Vxf != zenon_Vtd)
% 0.30/0.59  (zenon_Vge != zenon_Vwe)
% 0.30/0.59  (zenon_Vfg != zenon_Vya)
% 0.30/0.59  (zenon_Vkf != zenon_Vde)
% 0.30/0.59  (zenon_Vce != zenon_Vme)
% 0.30/0.59  (-. (p1 zenon_Vq))
% 0.30/0.59  (zenon_Vqe != zenon_Vw)
% 0.30/0.59  (zenon_Vzg != zenon_Vka)
% 0.30/0.59  (zenon_Vve != zenon_Vae)
% 0.30/0.59  (zenon_Vxf != zenon_Vya)
% 0.30/0.59  (zenon_Vch != zenon_Vdd)
% 0.30/0.59  (r1 zenon_Vhf zenon_Vif)
% 0.30/0.59  (zenon_Vrg != zenon_Vfb)
% 0.30/0.59  (zenon_Vkf != zenon_Vdd)
% 0.30/0.59  (zenon_Vff != zenon_Vdd)
% 0.30/0.59  (r1 zenon_Vye zenon_Vbf)
% 0.30/0.59  (zenon_Vpf != zenon_Vvc)
% 0.30/0.59  (zenon_Vpf != zenon_Vhe)
% 0.30/0.59  (zenon_Vkf != zenon_Vae)
% 0.30/0.59  (zenon_Vge != zenon_Vlf)
% 0.30/0.59  (zenon_Vjg != zenon_Vvc)
% 0.30/0.59  (zenon_Vrg != zenon_Vzc)
% 0.30/0.59  (zenon_Vbg != zenon_Vvc)
% 0.30/0.59  (zenon_Vfg != zenon_Vbf)
% 0.30/0.59  (zenon_Vce != zenon_Vlf)
% 0.30/0.59  (zenon_Vjg != zenon_Vmb)
% 0.30/0.59  (zenon_Vve != zenon_Vhd)
% 0.30/0.59  (-. (p1 zenon_Vtd))
% 0.30/0.59  (zenon_Vkf != zenon_Vwe)
% 0.30/0.59  (zenon_Vch != zenon_Vq)
% 0.30/0.59  (zenon_Vzg != zenon_Vda)
% 0.30/0.59  (zenon_Vbg != zenon_Vtb)
% 0.30/0.59  (zenon_Vge != zenon_Vvc)
% 0.30/0.59  (-. (p1 zenon_Vld))
% 0.30/0.59  (zenon_Vve != zenon_Vda)
% 0.30/0.59  (zenon_Vfg != zenon_Vra)
% 0.30/0.59  (zenon_Vve != zenon_Vq)
% 0.30/0.59  (r1 zenon_Vog zenon_Vrg)
% 0.30/0.59  (-. (p1 zenon_Vhd))
% 0.30/0.59  (zenon_Vrg != zenon_Vlf)
% 0.30/0.59  (zenon_Vle != zenon_Vvc)
% 0.30/0.59  (zenon_Vzg != zenon_Vre)
% 0.30/0.59  (zenon_Vjg != zenon_Vtb)
% 0.30/0.59  (zenon_Vve != zenon_Vme)
% 0.30/0.59  (zenon_Vrg != zenon_Vwe)
% 0.30/0.59  (zenon_Vxf != zenon_Vmb)
% 0.30/0.59  (zenon_Vxf != zenon_Vwe)
% 0.30/0.59  (zenon_Vpf != zenon_Vqf)
% 0.30/0.59  (zenon_Vve != zenon_Vhe)
% 0.30/0.59  (zenon_Vng != zenon_Vlf)
% 0.30/0.59  (zenon_Vaf != zenon_Vtb)
% 0.30/0.59  (zenon_Vle != zenon_Vpd)
% 0.30/0.59  (zenon_Vch != zenon_Vae)
% 0.30/0.59  (zenon_Vbg != zenon_Vtd)
% 0.30/0.59  (-. (p1 zenon_Vgf))
% 0.30/0.59  (r1 zenon_Vdf zenon_Vef)
% 0.30/0.59  (zenon_Vbg != zenon_Vlf)
% 0.30/0.59  (zenon_Vxf != zenon_Vda)
% 0.30/0.59  (r1 zenon_Vne zenon_Voe)
% 0.30/0.59  (zenon_Vle != zenon_Vqf)
% 0.30/0.59  (zenon_Vpf != zenon_Vq)
% 0.30/0.59  (zenon_Vfg != zenon_Vka)
% 0.30/0.59  (zenon_Vge != zenon_Vmb)
% 0.30/0.59  (zenon_Vkf != zenon_Vxd)
% 0.30/0.59  (r1 zenon_Vob zenon_Vsb)
% 0.30/0.59  (r1 zenon_Vmc zenon_Vnc)
% 0.30/0.59  (zenon_Vff != zenon_Vka)
% 0.30/0.59  (zenon_Vaf != zenon_Vka)
% 0.30/0.59  (zenon_Vce != zenon_Vtb)
% 0.30/0.59  (zenon_Vaf != zenon_Vlf)
% 0.30/0.59  (zenon_Vce != zenon_Vq)
% 0.30/0.59  (zenon_Vch != zenon_Vda)
% 0.30/0.59  (zenon_Vff != zenon_Vmb)
% 0.30/0.59  (zenon_Vmc != zenon_Vtf)
% 0.30/0.59  (r1 zenon_Vxe zenon_Vcf)
% 0.30/0.59  (zenon_Vve != zenon_Vzc)
% 0.30/0.59  (zenon_Vxf != zenon_Vlf)
% 0.30/0.59  (zenon_Vzg != zenon_Vfb)
% 0.30/0.59  (zenon_Vce != zenon_Vld)
% 0.30/0.59  (p1 zenon_Vvg)
% 0.30/0.59  (zenon_Vaf != zenon_Vda)
% 0.30/0.59  (zenon_Vpf != zenon_Vgf)
% 0.30/0.59  (p1 zenon_Vxf)
% 0.30/0.59  (zenon_Vaf != zenon_Vq)
% 0.30/0.59  (zenon_Vng != zenon_Vwe)
% 0.30/0.59  (zenon_Vqe != zenon_Vra)
% 0.30/0.59  (zenon_Vpf != zenon_Vra)
% 0.30/0.59  (zenon_Vfg != zenon_Vda)
% 0.30/0.59  (zenon_Vfg != zenon_Vlf)
% 0.30/0.59  (zenon_Vce != zenon_Vra)
% 0.30/0.59  (zenon_Vqe != zenon_Vka)
% 0.30/0.59  (zenon_Vle != zenon_Vzc)
% 0.30/0.59  (r1 zenon_Vyf zenon_Vbg)
% 0.30/0.59  (zenon_Vff != zenon_Vwe)
% 0.30/0.59  (zenon_Vng != zenon_Vfb)
% 0.30/0.59  (zenon_Vge != zenon_Vzc)
% 0.30/0.59  (zenon_Vaf != zenon_Vfb)
% 0.30/0.59  (-. (p1 zenon_Vfb))
% 0.30/0.59  (zenon_Vzg != zenon_Vgf)
% 0.30/0.59  (r1 zenon_Vee zenon_Vhe)
% 0.30/0.59  (zenon_Vge != zenon_Vbf)
% 0.30/0.59  (zenon_Vve != zenon_Vde)
% 0.30/0.59  (zenon_Vkf != zenon_Vhe)
% 0.30/0.59  (zenon_Vng != zenon_Vka)
% 0.30/0.59  (-. (p1 zenon_Vme))
% 0.30/0.59  (zenon_Vqe != zenon_Vwe)
% 0.30/0.59  (zenon_Vpf != zenon_Vda)
% 0.30/0.59  (zenon_Vzg != zenon_Vdd)
% 0.30/0.59  (zenon_Vkf != zenon_Vzc)
% 0.30/0.59  (zenon_Vng != zenon_Vpd)
% 0.30/0.59  (zenon_Vqe != zenon_Vq)
% 0.30/0.59  (zenon_Vaf != zenon_Vw)
% 0.30/0.59  (zenon_Vfg != zenon_Vfb)
% 0.30/0.59  (-. (p1 zenon_Vwe))
% 0.30/0.59  (zenon_Vxf != zenon_Vqf)
% 0.30/0.59  (zenon_Vng != zenon_Vld)
% 0.30/0.59  (zenon_Vve != zenon_Vtb)
% 0.30/0.59  (zenon_Vle != zenon_Vdd)
% 0.30/0.59  (r1 Tau_1 zenon_Vbe)
% 0.30/0.59  (r1 zenon_Vad zenon_Vdd)
% 0.30/0.59  (zenon_Vpf != zenon_Vbf)
% 0.30/0.59  (zenon_Vbg != zenon_Vda)
% 0.30/0.59  (zenon_Vrg != zenon_Vxd)
% 0.30/0.59  (zenon_Vbg != zenon_Vmb)
% 0.30/0.59  (r1 Tau_2 zenon_Vee)
% 0.30/0.59  (r1 Tau_2 zenon_Vie)
% 0.30/0.59  (-. (p2 zenon_Vgc))
% 0.30/0.59  (zenon_Vfg != zenon_Vqf)
% 0.30/0.59  (zenon_Vff != zenon_Vpd)
% 0.30/0.59  (zenon_Vve != zenon_Vtd)
% 0.30/0.59  (zenon_Vng != zenon_Vw)
% 0.30/0.59  (zenon_Vle != zenon_Vhd)
% 0.30/0.59  (zenon_Vch != zenon_Vme)
% 0.30/0.59  (zenon_Vch != zenon_Vzc)
% 0.30/0.59  (r1 zenon_Vsg zenon_Vvg)
% 0.30/0.59  (zenon_Vng != zenon_Vae)
% 0.30/0.59  (zenon_Vvg != zenon_Vlf)
% 0.30/0.59  (r1 zenon_Vif zenon_Vjf)
% 0.30/0.59  (zenon_Vpf != zenon_Vwe)
% 0.30/0.59  (zenon_Vff != zenon_Vld)
% 0.30/0.59  (-. (p1 zenon_Vmb))
% 0.30/0.59  (zenon_Vqe != zenon_Vtb)
% 0.30/0.59  (zenon_Vjg != zenon_Vq)
% 0.30/0.59  (zenon_Vxf != zenon_Vra)
% 0.30/0.59  (zenon_Vng != zenon_Vme)
% 0.30/0.59  (p1 zenon_Vbg)
% 0.30/0.59  (zenon_Vbg != zenon_Vxd)
% 0.30/0.59  (zenon_Vqe != zenon_Vde)
% 0.30/0.59  (r1 zenon_Vid zenon_Vld)
% 0.30/0.59  (zenon_Vxf != zenon_Vgf)
% 0.30/0.59  (p2 zenon_Vmc)
% 0.30/0.59  (zenon_Vfg != zenon_Vpd)
% 0.30/0.59  (zenon_Vff != zenon_Vtd)
% 0.30/0.59  (p1 zenon_Vge)
% 0.30/0.59  (zenon_Vjg != zenon_Vme)
% 0.30/0.59  (zenon_Vvg != zenon_Vtd)
% 0.30/0.59  (zenon_Vqe != zenon_Vae)
% 0.30/0.59  (r1 zenon_Vye zenon_Vze)
% 0.30/0.59  (zenon_Vfg != zenon_Vzc)
% 0.30/0.59  (zenon_Vbg != zenon_Vqf)
% 0.30/0.59  (r1 zenon_Vie zenon_Vne)
% 0.30/0.59  (zenon_Vrg != zenon_Vde)
% 0.30/0.59  (zenon_Vfg != zenon_Vw)
% 0.30/0.59  (zenon_Vng != zenon_Vya)
% 0.30/0.59  (r1 zenon_Vje zenon_Vke)
% 0.30/0.59  (p1 zenon_Vqe)
% 0.30/0.59  (zenon_Vve != zenon_Vya)
% 0.30/0.59  (r1 zenon_Vud zenon_Vxd)
% 0.30/0.59  (zenon_Vrg != zenon_Vq)
% 0.30/0.59  (zenon_Vzg != zenon_Vde)
% 0.30/0.59  (zenon_Vfg != zenon_Vxd)
% 0.30/0.59  (zenon_Vaf != zenon_Vwe)
% 0.30/0.59  (zenon_Vaf != zenon_Vhd)
% 0.30/0.59  (zenon_Vrg != zenon_Vpd)
% 0.30/0.59  (zenon_Vvg != zenon_Vde)
% 0.30/0.59  (r1 zenon_Vnf zenon_Vof)
% 0.30/0.59  (r1 zenon_Vwg zenon_Vzg)
% 0.30/0.59  (zenon_Vjg != zenon_Vra)
% 0.30/0.59  (zenon_Vbg != zenon_Vhe)
% 0.30/0.59  (zenon_Vqe != zenon_Vhd)
% 0.30/0.59  (zenon_Vzg != zenon_Vtb)
% 0.30/0.59  (zenon_Vkf != zenon_Vka)
% 0.30/0.59  (-. (p2 zenon_Vac))
% 0.30/0.59  (zenon_Vff != zenon_Vfb)
% 0.30/0.59  (-. (p1 zenon_Vra))
% 0.30/0.59  (zenon_Vff != zenon_Vqf)
% 0.30/0.59  (zenon_Vqe != zenon_Vme)
% 0.30/0.59  (zenon_Vch != zenon_Vxd)
% 0.30/0.59  (zenon_Vxf != zenon_Vld)
% 0.30/0.59  (zenon_Vjg != zenon_Vya)
% 0.30/0.59  (zenon_Vxf != zenon_Vtb)
% 0.30/0.59  (-. (p2 zenon_Vtf))
% 0.30/0.59  (zenon_Vqe != zenon_Vxd)
% 0.30/0.59  (zenon_Vkf != zenon_Vbf)
% 0.30/0.59  (zenon_Vkf != zenon_Vqf)
% 0.30/0.59  (zenon_Vvg != zenon_Vme)
% 0.30/0.59  (zenon_Vch != zenon_Vld)
% 0.30/0.59  (-. (p1 zenon_Vw))
% 0.30/0.59  (zenon_Vaf != zenon_Vpd)
% 0.30/0.59  (zenon_Vjg != zenon_Vgf)
% 0.30/0.59  (zenon_Vge != zenon_Vhe)
% 0.30/0.59  (zenon_Vle != zenon_Vld)
% 0.30/0.59  (zenon_Vrg != zenon_Vld)
% 0.30/0.59  (zenon_Vng != zenon_Vxd)
% 0.30/0.59  (zenon_Vch != zenon_Vlf)
% 0.30/0.59  (zenon_Vff != zenon_Vda)
% 0.30/0.59  (zenon_Vqe != zenon_Vld)
% 0.30/0.59  (zenon_Vge != zenon_Vfb)
% 0.30/0.59  (zenon_Vvg != zenon_Vld)
% 0.30/0.59  (zenon_Vaf != zenon_Vld)
% 0.30/0.59  (zenon_Vvg != zenon_Vxd)
% 0.30/0.59  (zenon_Vpf != zenon_Vld)
% 0.30/0.59  (zenon_Vkf != zenon_Vvc)
% 0.30/0.59  (zenon_Vge != zenon_Vxd)
% 0.30/0.59  (zenon_Vge != zenon_Vra)
% 0.30/0.59  (r1 zenon_Vmf zenon_Vrf)
% 0.30/0.59  (zenon_Vaf != zenon_Vre)
% 0.30/0.59  (zenon_Vqe != zenon_Vdd)
% 0.30/0.59  (zenon_Vqe != zenon_Vlf)
% 0.30/0.59  (zenon_Vbg != zenon_Vdd)
% 0.30/0.59  (zenon_Vzg != zenon_Vwe)
% 0.30/0.59  (zenon_Vrg != zenon_Vra)
% 0.30/0.59  (zenon_Vle != zenon_Vgf)
% 0.30/0.59  (zenon_Vng != zenon_Vgf)
% 0.30/0.59  (zenon_Vzg != zenon_Vqf)
% 0.30/0.59  (r1 zenon_X6 zenon_Vae)
% 0.30/0.59  (zenon_Vzg != zenon_Vxd)
% 0.30/0.59  (zenon_Vrg != zenon_Vhe)
% 0.30/0.59  (zenon_Vrg != zenon_Vmb)
% 0.30/0.59  (zenon_Vvg != zenon_Vbf)
% 0.30/0.59  (zenon_Vge != zenon_Vw)
% 0.30/0.59  (zenon_Vmc != zenon_Vgc)
% 0.30/0.59  (zenon_Vpf != zenon_Vxd)
% 0.30/0.59  (zenon_Vrg != zenon_Vgf)
% 0.30/0.59  (r1 zenon_Vcf zenon_Vdf)
% 0.30/0.59  (zenon_Vqe != zenon_Vbf)
% 0.30/0.59  (zenon_Vff != zenon_Vhe)
% 0.30/0.59  (zenon_Vle != zenon_Vxd)
% 0.30/0.59  (zenon_Vqe != zenon_Vgf)
% 0.30/0.59  (zenon_Vaf != zenon_Vmb)
% 0.30/0.59  (zenon_Vzg != zenon_Vmb)
% 0.30/0.59  (zenon_Vpf != zenon_Vlf)
% 0.30/0.59  (zenon_Vrg != zenon_Vbf)
% 0.30/0.59  (zenon_Vce != zenon_Vwe)
% 0.30/0.59  (r1 zenon_Vgg zenon_Vjg)
% 0.30/0.59  (zenon_Vrg != zenon_Vre)
% 0.30/0.59  (-. (p1 zenon_Vlf))
% 0.30/0.59  (zenon_Vng != zenon_Vdd)
% 0.30/0.59  (p1 zenon_Vkf)
% 0.30/0.59  (zenon_Vvg != zenon_Vya)
% 0.30/0.59  (zenon_Vkf != zenon_Vya)
% 0.30/0.59  (zenon_Vge != zenon_Vre)
% 0.30/0.59  (zenon_Vzg != zenon_Vq)
% 0.30/0.59  (zenon_Vch != zenon_Vra)
% 0.30/0.59  (r1 zenon_Vhf zenon_Vmf)
% 0.30/0.59  (zenon_Vpf != zenon_Vre)
% 0.30/0.59  (zenon_Vng != zenon_Vqf)
% 0.30/0.59  (p1 zenon_Vfg)
% 0.30/0.59  (zenon_Vxf != zenon_Vvc)
% 0.30/0.59  (r1 zenon_Vhc zenon_Vkc)
% 0.30/0.59  (p1 zenon_Vve)
% 0.30/0.59  (zenon_Vjg != zenon_Vre)
% 0.30/0.59  (zenon_Vge != zenon_Vtb)
% 0.30/0.59  (zenon_Vff != zenon_Vde)
% 0.30/0.59  (zenon_Vbg != zenon_Vre)
% 0.30/0.59  (zenon_Vce != zenon_Vgf)
% 0.30/0.59  (zenon_Vng != zenon_Vhd)
% 0.30/0.59  (zenon_Vxf != zenon_Vpd)
% 0.30/0.59  (-. (p2 zenon_Vrc))
% 0.30/0.59  (zenon_Vfg != zenon_Vme)
% 0.30/0.59  (r1 zenon_Vkg zenon_Vng)
% 0.30/0.59  (zenon_Vce != zenon_Vda)
% 0.30/0.59  (zenon_Vpf != zenon_Vw)
% 0.30/0.59  (zenon_Vvg != zenon_Vzc)
% 0.30/0.59  (zenon_Vve != zenon_Vmb)
% 0.30/0.59  (zenon_Vzg != zenon_Vvc)
% 0.30/0.59  (zenon_Vng != zenon_Vre)
% 0.30/0.59  (zenon_Vpf != zenon_Vka)
% 0.30/0.59  (zenon_Vff != zenon_Vae)
% 0.30/0.59  (zenon_Vkf != zenon_Vhd)
% 0.30/0.59  (zenon_Vrg != zenon_Vqf)
% 0.30/0.59  (zenon_Vzg != zenon_Vld)
% 0.30/0.59  (zenon_Vch != zenon_Vya)
% 0.30/0.59  (zenon_Vle != zenon_Vtb)
% 0.30/0.59  (r1 zenon_Vie zenon_Vje)
% 0.30/0.59  (zenon_Vge != zenon_Vld)
% 0.30/0.59  (zenon_Vch != zenon_Vvc)
% 0.30/0.59  (zenon_Vkf != zenon_Vme)
% 0.30/0.59  (zenon_Vfg != zenon_Vq)
% 0.30/0.59  (p1 zenon_Vpf)
% 0.30/0.59  (zenon_Vle != zenon_Vde)
% 0.30/0.59  (zenon_Vmc != zenon_Vrc)
% 0.30/0.59  (zenon_Vrg != zenon_Vhd)
% 0.30/0.59  (zenon_Vjg != zenon_Vbf)
% 0.30/0.59  (zenon_Vzg != zenon_Vlf)
% 0.30/0.59  (zenon_Vvg != zenon_Vka)
% 0.30/0.59  (zenon_Vbg != zenon_Vka)
% 0.30/0.59  (-. (p1 zenon_Vde))
% 0.30/0.59  (r1 Tau_1 zenon_Vde)
% 0.30/0.59  (zenon_Vzg != zenon_Vw)
% 0.30/0.59  (zenon_Vaf != zenon_Vhe)
% 0.30/0.59  (zenon_Vmc != zenon_Vac)
% 0.30/0.59  (zenon_Vng != zenon_Vvc)
% 0.30/0.59  (zenon_Vjg != zenon_Vhe)
% 0.30/0.59  (zenon_Vpf != zenon_Vfb)
% 0.30/0.59  (zenon_Vjg != zenon_Vw)
% 0.30/0.59  (zenon_Vvg != zenon_Vhe)
% 0.30/0.59  (zenon_Vxf != zenon_Vfb)
% 0.30/0.59  (zenon_Vle != zenon_Vfb)
% 0.30/0.59  (zenon_Vce != zenon_Vxd)
% 0.30/0.59  (zenon_Vkf != zenon_Vra)
% 0.30/0.59  (zenon_Vvg != zenon_Vhd)
% 0.30/0.59  (zenon_Vrg != zenon_Vw)
% 0.30/0.59  (zenon_Vjg != zenon_Vae)
% 0.30/0.59  (zenon_Vle != zenon_Vw)
% 0.30/0.59  (p1 zenon_Vng)
% 0.30/0.59  (zenon_Vff != zenon_Vbf)
% 0.30/0.59  (zenon_Vge != zenon_Vde)
% 0.30/0.59  (zenon_Vch != zenon_Vmb)
% 0.30/0.59  (zenon_Vjg != zenon_Vka)
% 0.30/0.59  (zenon_Vff != zenon_Vgf)
% 0.30/0.59  (zenon_Vzg != zenon_Vbf)
% 0.30/0.59  (zenon_Vve != zenon_Vld)
% 0.30/0.59  (zenon_Vch != zenon_Vka)
% 0.30/0.59  (zenon_Vzg != zenon_Vya)
% 0.30/0.59  (zenon_Vaf != zenon_Vvc)
% 0.30/0.59  (zenon_Vle != zenon_Vda)
% 0.30/0.59  (zenon_Vaf != zenon_Vtd)
% 0.30/0.59  (zenon_Vxf != zenon_Vhd)
% 0.30/0.59  (zenon_Vkf != zenon_Vtb)
% 0.30/0.59  (zenon_Vce != zenon_Vde)
% 0.30/0.59  (zenon_Vce != zenon_Vzc)
% 0.30/0.59  (zenon_Vzg != zenon_Vae)
% 0.30/0.59  (r1 zenon_Vta zenon_Vxa)
% 0.30/0.59  (zenon_Vch != zenon_Vqf)
% 0.30/0.59  (zenon_Vqe != zenon_Vtd)
% 0.30/0.59  (zenon_Vce != zenon_Vqf)
% 0.30/0.59  (zenon_Vrg != zenon_Vae)
% 0.30/0.59  (zenon_Vce != zenon_Vw)
% 0.30/0.59  (zenon_Vge != zenon_Vtd)
% 0.30/0.59  *)
% 0.30/0.59  (* NO-PROOF *)
% 0.30/0.59  % SZS status GaveUp
% 0.30/0.59  Number of rewrites on terms: 0
% 0.30/0.59  Number of rewrites on props: 0
% 0.30/0.59  nodes searched: 855
% 0.30/0.59  max branch formulas: 976
% 0.30/0.59  proof nodes created: 0
% 0.30/0.59  formulas created: 5034
% 0.30/0.59  
%------------------------------------------------------------------------------