↑ Up

ZenonModulo---0.5.0.UNK-Non.f

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

% Computer : n007.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.14s 0.90s
% Output   : None 
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : LCL640+1.020 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03  % Command  : run_zenon_modulo %d %s
% 0.07/0.34  % Computer : n007.cluster.edu
% 0.07/0.34  % Model    : x86_64 x86_64
% 0.07/0.34  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.34  % Memory   : 8046.5625MB
% 0.07/0.34  % OS       : Linux 6.8.0-71-generic
% 0.07/0.34  % CPULimit : 300
% 0.07/0.34  % WCLimit  : 300
% 0.07/0.34  % DateTime : Sat Sep  5 04:36:39 UTC 2026
% 0.07/0.34  % CPUTime  : 
% 0.54/0.89  Zenon error: exhausted search space without finding a proof
% 0.54/0.89  (* Current branch:
% 0.54/0.89  (p1 zenon_Vgh)
% 0.54/0.89  (zenon_Vih != zenon_Vzk)
% 0.54/0.89  (zenon_Vqi != zenon_Vnl)
% 0.54/0.89  (zenon_Vqi != zenon_Vrn)
% 0.54/0.89  (zenon_Vqi != zenon_Vhh)
% 0.54/0.89  (r1 zenon_Vgj zenon_Vjj)
% 0.54/0.89  (zenon_Voi != zenon_Vmi)
% 0.54/0.89  (-. (p1 zenon_Vga))
% 0.54/0.89  (r1 zenon_Vpm zenon_Vsm)
% 0.54/0.89  (zenon_Vqi != zenon_Vwe)
% 0.54/0.89  (-. (p1 zenon_Vhh))
% 0.54/0.89  (zenon_Vqi != zenon_Vrg)
% 0.54/0.89  (r1 zenon_Vfi zenon_Vgi)
% 0.54/0.89  (zenon_Vqi != zenon_Vph)
% 0.54/0.89  (zenon_Vqi != zenon_Vhb)
% 0.54/0.89  (zenon_Vih != zenon_Vmb)
% 0.54/0.89  (-. (p1 zenon_Vfl))
% 0.54/0.89  (zenon_Vqi != zenon_Vam)
% 0.54/0.89  (-. (p1 zenon_Vxf))
% 0.54/0.89  (zenon_Vgh != zenon_Vxe)
% 0.54/0.89  (zenon_Vih != zenon_Vlh)
% 0.54/0.89  (-. (p1 zenon_Vol))
% 0.54/0.89  (zenon_Voi != zenon_Voh)
% 0.54/0.89  (zenon_Vgh != zenon_Vmb)
% 0.54/0.89  (r1 zenon_Vig zenon_Vlg)
% 0.54/0.89  (zenon_Vqi != zenon_Vqn)
% 0.54/0.89  (-. (p1 zenon_Vrf))
% 0.54/0.89  (zenon_Vih != zenon_Vbe)
% 0.54/0.89  (zenon_Vgh != zenon_Vwe)
% 0.54/0.89  (r1 Tau_0 Tau_1)
% 0.54/0.89  (zenon_Vih != zenon_Vai)
% 0.54/0.89  (-. (p1 zenon_Vmg))
% 0.54/0.89  (zenon_Vqi != zenon_Vmi)
% 0.54/0.89  (zenon_Vih != zenon_Vnn)
% 0.54/0.89  (r1 zenon_Vic zenon_Vlc)
% 0.54/0.89  (-. (p1 zenon_Vae))
% 0.54/0.89  (r1 zenon_Vxd zenon_Vae)
% 0.54/0.89  (r1 zenon_Vcl zenon_Vfl)
% 0.54/0.89  (zenon_Voi != zenon_Vak)
% 0.54/0.89  (-. (p1 zenon_Vma))
% 0.54/0.89  (zenon_Vgh != zenon_Vzk)
% 0.54/0.89  (zenon_Vih != zenon_Vgm)
% 0.54/0.89  (-. (p1 zenon_Vam))
% 0.54/0.89  (zenon_Vqi != zenon_Vsf)
% 0.54/0.89  (zenon_Vqi != zenon_Vge)
% 0.54/0.89  (zenon_Vgh != zenon_Vym)
% 0.54/0.89  (zenon_Vih != zenon_Vga)
% 0.54/0.89  (zenon_Voi != zenon_Vsm)
% 0.54/0.89  (-. (p1 zenon_Ved))
% 0.54/0.89  (-. (p1 zenon_Vzh))
% 0.54/0.89  (zenon_Vqi != zenon_Vin)
% 0.54/0.89  (-. (p1 zenon_Vak))
% 0.54/0.89  (zenon_Vgh != zenon_Vhh)
% 0.54/0.89  (-. (p1 zenon_Vsm))
% 0.54/0.89  (zenon_Voi != zenon_Ved)
% 0.54/0.89  (zenon_Vgh != zenon_Vxf)
% 0.54/0.89  (zenon_Vqi != zenon_Vtl)
% 0.54/0.89  (zenon_Vih != zenon_Ved)
% 0.54/0.89  (zenon_Vqi != zenon_Vzk)
% 0.54/0.89  (zenon_Vqi != zenon_Ved)
% 0.54/0.89  (zenon_Vih != zenon_Vma)
% 0.54/0.89  (zenon_Vgh != zenon_Vdj)
% 0.54/0.89  (zenon_Voi != zenon_Vuh)
% 0.54/0.89  (-. (p1 zenon_Vlh))
% 0.54/0.89  (zenon_Vqi != zenon_Vdd)
% 0.54/0.89  (-. (p1 zenon_Vdd))
% 0.54/0.89  (r1 zenon_Vkl zenon_Vnl)
% 0.54/0.89  (zenon_Vih != zenon_Vrg)
% 0.54/0.89  (-. (p1 zenon_Vjd))
% 0.54/0.89  (zenon_Vgh != zenon_Vgm)
% 0.54/0.89  (-. (p1 zenon_Vuj))
% 0.54/0.89  (zenon_Vgh != zenon_Vjj)
% 0.54/0.89  (zenon_Vqi != zenon_Vha)
% 0.54/0.89  (zenon_Vgh != zenon_Vak)
% 0.54/0.89  (zenon_Vgh != zenon_Vzh)
% 0.54/0.89  (zenon_Vgh != zenon_Vuh)
% 0.54/0.89  (-. (p1 zenon_Vcf))
% 0.54/0.89  (-. (p1 zenon_Vhb))
% 0.54/0.89  (r1 zenon_Vji zenon_Vki)
% 0.54/0.89  (zenon_Vih != zenon_Vol)
% 0.54/0.89  (-. (p1 zenon_Vai))
% 0.54/0.89  (r1 zenon_Vkn zenon_Vnn)
% 0.54/0.89  (zenon_Vgh != zenon_Vtl)
% 0.54/0.89  (-. (p1 zenon_Vkk))
% 0.54/0.89  (zenon_Vih != zenon_Vhh)
% 0.54/0.89  (zenon_Vih != zenon_Vgc)
% 0.54/0.89  (-. (p1 zenon_Vbm))
% 0.54/0.89  (r1 zenon_Vhk zenon_Vkk)
% 0.54/0.89  (r1 zenon_Vxj zenon_Vak)
% 0.54/0.89  (zenon_Vih != zenon_Vqk)
% 0.54/0.89  (zenon_Voi != zenon_Vai)
% 0.54/0.89  (r1 zenon_Vjb zenon_Vmb)
% 0.54/0.89  (zenon_Voi != zenon_Vam)
% 0.54/0.89  (zenon_Vgh != zenon_Vbm)
% 0.54/0.89  (zenon_Vgh != zenon_Vcf)
% 0.54/0.89  (zenon_Vqi != zenon_Vzh)
% 0.54/0.89  (zenon_Vqi != zenon_Vsm)
% 0.54/0.89  (zenon_Vgh != zenon_Vha)
% 0.54/0.89  (zenon_Vqi != zenon_Vfc)
% 0.54/0.89  (zenon_Vqi != zenon_Vri)
% 0.54/0.89  (zenon_Vqi != zenon_Vbe)
% 0.54/0.89  (zenon_Vqi != zenon_Vnm)
% 0.54/0.89  (zenon_Vih != zenon_Voh)
% 0.54/0.89  (r1 zenon_Vih zenon_Vlh)
% 0.54/0.89  (-. (p1 zenon_Vnn))
% 0.54/0.89  (zenon_Vqi != zenon_Vgm)
% 0.54/0.89  (zenon_Vqi != zenon_Vnn)
% 0.54/0.89  (-. (p1 zenon_Val))
% 0.54/0.89  (zenon_Vqi != zenon_Vxe)
% 0.54/0.89  (zenon_Voi != zenon_Vhh)
% 0.54/0.89  (zenon_Voi != zenon_Vwn)
% 0.54/0.89  (r1 zenon_Vgi zenon_Vhi)
% 0.54/0.89  (r1 zenon_Vte zenon_Vwe)
% 0.54/0.89  (zenon_Vgh != zenon_Vfl)
% 0.54/0.89  (r1 zenon_Vbh zenon_Voh)
% 0.54/0.89  (zenon_Voi != zenon_Val)
% 0.54/0.89  (zenon_Vih != zenon_Vfc)
% 0.54/0.89  (zenon_Vgh != zenon_Vej)
% 0.54/0.89  (zenon_Vih != zenon_Vae)
% 0.54/0.89  (zenon_Vqi != zenon_Vgb)
% 0.54/0.89  (zenon_Vih != zenon_Vcf)
% 0.54/0.89  (zenon_Vgh != zenon_Vnm)
% 0.54/0.89  (zenon_Vgh != zenon_Val)
% 0.54/0.89  (zenon_Vih != zenon_Vsm)
% 0.54/0.89  (zenon_Vqi != zenon_Vmb)
% 0.54/0.89  (r1 zenon_Vli zenon_Vmi)
% 0.54/0.89  (-. (p1 zenon_Vxe))
% 0.54/0.89  (r1 zenon_X20 zenon_Vqn)
% 0.54/0.89  (zenon_Vih != zenon_Vhn)
% 0.54/0.89  (-. (p1 zenon_Vhn))
% 0.54/0.89  (zenon_Voi != zenon_Vph)
% 0.54/0.89  (-. (p1 zenon_Vvj))
% 0.54/0.89  (zenon_Vqi != zenon_Vdn)
% 0.54/0.89  (zenon_Voi != zenon_Vdn)
% 0.54/0.89  (zenon_Vgh != zenon_Vmm)
% 0.54/0.89  (zenon_Voi != zenon_Vlc)
% 0.54/0.89  (zenon_Vqi != zenon_Vuh)
% 0.54/0.89  (r1 zenon_Vuf zenon_Vxf)
% 0.54/0.89  (zenon_Vih != zenon_Vxm)
% 0.54/0.89  (zenon_Vih != zenon_Vdj)
% 0.54/0.89  (zenon_Vqi != zenon_Vdj)
% 0.54/0.89  (zenon_Vqi != zenon_Vae)
% 0.54/0.89  (zenon_Vqi != zenon_Vjd)
% 0.54/0.89  (zenon_Vgh != zenon_Vae)
% 0.54/0.89  (zenon_Vqi != zenon_Vmm)
% 0.54/0.89  (zenon_Vqi != zenon_Vxf)
% 0.54/0.89  (zenon_Voi != zenon_Vxe)
% 0.54/0.89  (-. (p1 zenon_Vdj))
% 0.54/0.89  (zenon_Vgh != zenon_Vnl)
% 0.54/0.89  (zenon_Vgh != zenon_Vvj)
% 0.54/0.89  (zenon_Vih != zenon_Vym)
% 0.54/0.89  (zenon_Vqi != zenon_Vuj)
% 0.54/0.89  (zenon_Voi != zenon_Vin)
% 0.54/0.89  (r1 zenon_Vum zenon_Vxm)
% 0.54/0.89  (zenon_Voi != zenon_Vbm)
% 0.54/0.89  (zenon_Voi != zenon_Vvj)
% 0.54/0.89  (zenon_Voi != zenon_Vol)
% 0.54/0.89  (zenon_Vih != zenon_Vjj)
% 0.54/0.89  (r1 zenon_Vaj zenon_Vdj)
% 0.54/0.89  (zenon_Vqi != zenon_Vkk)
% 0.54/0.89  (-. (p1 zenon_Vph))
% 0.54/0.89  (-. (p1 zenon_Voh))
% 0.54/0.89  (zenon_Vqi != zenon_Vlk)
% 0.54/0.89  (zenon_Vih != zenon_Vxf)
% 0.54/0.89  (zenon_Vgh != zenon_Vsf)
% 0.54/0.89  (zenon_Vih != zenon_Vqn)
% 0.54/0.89  (r1 zenon_Vjm zenon_Vmm)
% 0.54/0.89  (zenon_Vqi != zenon_Vma)
% 0.54/0.89  (zenon_Voi != zenon_Vlk)
% 0.54/0.89  (zenon_Vgh != zenon_Vlg)
% 0.54/0.89  (zenon_Voi != zenon_Vzh)
% 0.54/0.89  (zenon_Vih != zenon_Vbm)
% 0.54/0.89  (r1 zenon_Vcc zenon_Vfc)
% 0.54/0.89  (zenon_Vih != zenon_Vha)
% 0.54/0.89  (r1 zenon_Vwk zenon_Vzk)
% 0.54/0.89  (zenon_Vih != zenon_Vvj)
% 0.54/0.89  (zenon_Vqi != zenon_Vej)
% 0.54/0.89  (r1 zenon_Vbh zenon_Vzh)
% 0.54/0.89  (zenon_Vih != zenon_Vhb)
% 0.54/0.89  (zenon_Vgh != zenon_Vqk)
% 0.54/0.89  (r1 zenon_Vgh zenon_Vhh)
% 0.54/0.89  (zenon_Vgh != zenon_Vdd)
% 0.54/0.89  (-. (p1 zenon_Vgb))
% 0.54/0.89  (zenon_Vgh != zenon_Ved)
% 0.54/0.89  (zenon_Voi != zenon_Vkk)
% 0.54/0.89  (-. (p1 zenon_Vnl))
% 0.54/0.89  (-. (p1 zenon_Vmi))
% 0.54/0.89  (zenon_Voi != zenon_Vrg)
% 0.54/0.89  (zenon_Vqi != zenon_Val)
% 0.54/0.89  (r1 zenon_Vog zenon_Vrg)
% 0.54/0.89  (r1 zenon_Van zenon_Vdn)
% 0.54/0.89  (-. (p1 zenon_Vej))
% 0.54/0.89  (zenon_Vgh != zenon_Vma)
% 0.54/0.89  (zenon_Vqi != zenon_Vcf)
% 0.54/0.89  (zenon_Voi != zenon_Vdj)
% 0.54/0.89  (-. (p1 zenon_Vrg))
% 0.54/0.89  (zenon_Vih != zenon_Vwe)
% 0.54/0.89  (zenon_Vih != zenon_Vuj)
% 0.54/0.89  (zenon_Vih != zenon_Vxe)
% 0.54/0.89  (zenon_Voi != zenon_Vej)
% 0.54/0.89  (zenon_Voi != zenon_Vxf)
% 0.54/0.89  (zenon_Vqi != zenon_Vqk)
% 0.54/0.89  (zenon_Vgh != zenon_Vrf)
% 0.54/0.89  (zenon_Vih != zenon_Vlk)
% 0.54/0.89  (zenon_Voi != zenon_Vwe)
% 0.54/0.89  (-. (p1 zenon_Vlc))
% 0.54/0.89  (r1 zenon_Ven zenon_Vhn)
% 0.54/0.89  (zenon_Vqi != zenon_Vbm)
% 0.54/0.89  (zenon_Vih != zenon_Vnm)
% 0.54/0.89  (zenon_Voi != zenon_Vuj)
% 0.54/0.89  (r1 zenon_Vki zenon_Vli)
% 0.54/0.89  (zenon_Vqi != zenon_Vlc)
% 0.54/0.89  (zenon_Vgh != zenon_Vmg)
% 0.54/0.89  (zenon_Voi != zenon_Vae)
% 0.54/0.89  (zenon_Vqi != zenon_Vxm)
% 0.54/0.89  (zenon_Vih != zenon_Vin)
% 0.54/0.89  (zenon_Voi != zenon_Vjd)
% 0.54/0.89  (zenon_Voi != zenon_Vdd)
% 0.54/0.89  (-. (p1 zenon_Vin))
% 0.54/0.89  (zenon_Vgh != zenon_Vsm)
% 0.54/0.89  (r1 zenon_Vpi zenon_Vqi)
% 0.54/0.89  (zenon_Vqi != zenon_Vlh)
% 0.54/0.89  (zenon_Vgh != zenon_Vuj)
% 0.54/0.89  (zenon_Voi != zenon_Vri)
% 0.54/0.89  (r1 zenon_Vrj zenon_Vuj)
% 0.54/0.89  (zenon_Vih != zenon_Vlg)
% 0.54/0.89  (zenon_Voi != zenon_Vge)
% 0.54/0.89  (-. (p1 zenon_Vwe))
% 0.54/0.89  (r1 zenon_Vdi zenon_Vei)
% 0.54/0.89  (-. (p1 zenon_Vnm))
% 0.54/0.89  (zenon_Voi != zenon_Vgc)
% 0.54/0.89  (zenon_Vih != zenon_Vge)
% 0.54/0.89  (r1 zenon_Vhi zenon_Vii)
% 0.54/0.89  (zenon_Vih != zenon_Vph)
% 0.54/0.89  (zenon_Voi != zenon_Vhn)
% 0.54/0.89  (r1 zenon_Vli zenon_Vni)
% 0.54/0.89  (r1 zenon_Vad zenon_Vdd)
% 0.54/0.89  (zenon_Vgh != zenon_Vdn)
% 0.54/0.89  (-. (p1 zenon_Vwn))
% 0.54/0.89  (-. (p1 zenon_Vha))
% 0.54/0.89  (zenon_Vgh != zenon_Vkk)
% 0.54/0.89  (p1 zenon_Vih)
% 0.54/0.89  (zenon_Vih != zenon_Vdd)
% 0.54/0.89  (zenon_Vih != zenon_Vtl)
% 0.54/0.89  (r1 Tau_1 zenon_Vci)
% 0.54/0.89  (zenon_Voi != zenon_Vcf)
% 0.54/0.89  (-. (p1 zenon_Vzk))
% 0.54/0.89  (-. (p1 zenon_Vmb))
% 0.54/0.89  (r1 zenon_Vbh zenon_Vgh)
% 0.54/0.89  (r1 zenon_Vdb zenon_Vgb)
% 0.54/0.89  (-. (p1 zenon_Vqn))
% 0.54/0.89  (-. (p1 zenon_Vtl))
% 0.54/0.89  (zenon_Vih != zenon_Vsf)
% 0.54/0.89  (p1 zenon_Vqi)
% 0.54/0.89  (zenon_Voi != zenon_Vxm)
% 0.54/0.89  (zenon_Vgh != zenon_Vwn)
% 0.54/0.89  (zenon_Voi != zenon_Vzk)
% 0.54/0.89  (zenon_Vqi != zenon_Vgc)
% 0.54/0.89  (-. (p1 zenon_Vge))
% 0.54/0.89  (zenon_Vqi != zenon_Vym)
% 0.54/0.89  (zenon_Vih != zenon_Vri)
% 0.54/0.89  (zenon_Voi != zenon_Vnm)
% 0.54/0.89  (zenon_Vgh != zenon_Vrn)
% 0.54/0.89  (-. (p1 zenon_Vym))
% 0.54/0.89  (zenon_Vgh != zenon_Vin)
% 0.54/0.89  (zenon_Vgh != zenon_Vge)
% 0.54/0.89  (zenon_Vih != zenon_Vej)
% 0.54/0.89  (zenon_Voi != zenon_Vha)
% 0.54/0.89  (zenon_Vqi != zenon_Vlg)
% 0.54/0.89  (zenon_Vih != zenon_Vlc)
% 0.54/0.89  (zenon_Vih != zenon_Vmg)
% 0.54/0.89  (zenon_Vgh != zenon_Vph)
% 0.54/0.89  (r1 zenon_Vde zenon_Vge)
% 0.54/0.89  (zenon_Vih != zenon_Vmm)
% 0.54/0.89  (r1 zenon_Vze zenon_Vcf)
% 0.54/0.89  (zenon_Vih != zenon_Vrf)
% 0.54/0.89  (r1 zenon_Vxl zenon_Vam)
% 0.54/0.89  (zenon_Vqi != zenon_Vfl)
% 0.54/0.89  (zenon_Voi != zenon_Vlh)
% 0.54/0.89  (zenon_Voi != zenon_Vqk)
% 0.54/0.89  (r1 zenon_Vja zenon_Vma)
% 0.54/0.89  (-. (p1 zenon_Vbe))
% 0.54/0.89  (r1 zenon_Vda zenon_Vga)
% 0.54/0.89  (zenon_Voi != zenon_Vmm)
% 0.54/0.89  (zenon_Voi != zenon_Vsf)
% 0.54/0.89  (zenon_Vgh != zenon_Vam)
% 0.54/0.89  (zenon_Vgh != zenon_Vol)
% 0.54/0.89  (zenon_Vih != zenon_Vdn)
% 0.54/0.89  (-. (p1 zenon_Vmm))
% 0.54/0.89  (zenon_Vqi != zenon_Voh)
% 0.54/0.89  (zenon_Vqi != zenon_Vai)
% 0.54/0.89  (-. (p1 zenon_Vgm))
% 0.54/0.89  (zenon_Vgh != zenon_Vfc)
% 0.54/0.89  (r1 zenon_Vrh zenon_Vuh)
% 0.54/0.89  (zenon_Vqi != zenon_Vol)
% 0.54/0.89  (zenon_Voi != zenon_Vjj)
% 0.54/0.89  (zenon_Vgh != zenon_Voh)
% 0.54/0.89  (zenon_Voi != zenon_Vgm)
% 0.54/0.89  (zenon_Vih != zenon_Vak)
% 0.54/0.89  (r1 zenon_Vii zenon_Vji)
% 0.54/0.89  (zenon_Vgh != zenon_Vga)
% 0.54/0.89  (zenon_Vqi != zenon_Vvj)
% 0.54/0.89  (-. (p1 zenon_Vdn))
% 0.54/0.89  (-. (p1 zenon_Vqk))
% 0.54/0.89  (-. (p1 zenon_Vxm))
% 0.54/0.89  (zenon_Vih != zenon_Vrn)
% 0.54/0.89  (-. (p1 zenon_Vri))
% 0.54/0.89  (zenon_Vgh != zenon_Vlc)
% 0.54/0.89  (zenon_Vih != zenon_Vfl)
% 0.54/0.89  (zenon_Vih != zenon_Vam)
% 0.54/0.89  (zenon_Vqi != zenon_Vwn)
% 0.54/0.89  (zenon_Vgh != zenon_Vnn)
% 0.54/0.89  (zenon_Voi != zenon_Vnl)
% 0.54/0.89  (zenon_Vih != zenon_Vgb)
% 0.54/0.89  (-. (p1 zenon_Vfc))
% 0.54/0.89  (zenon_Vgh != zenon_Vgc)
% 0.54/0.89  (zenon_Vih != zenon_Vnl)
% 0.54/0.89  (-. (p1 zenon_Vsf))
% 0.54/0.89  (zenon_Voi != zenon_Vma)
% 0.54/0.89  (zenon_Voi != zenon_Vqn)
% 0.54/0.89  (zenon_Vih != zenon_Vuh)
% 0.54/0.89  (zenon_Vgh != zenon_Vai)
% 0.54/0.89  (zenon_Vgh != zenon_Vjd)
% 0.54/0.89  (zenon_Vih != zenon_Vjd)
% 0.54/0.89  (-. (p1 zenon_Vjj))
% 0.54/0.89  (r1 zenon_Vql zenon_Vtl)
% 0.54/0.89  (r1 zenon_Vci zenon_Vdi)
% 0.54/0.89  (zenon_Vgh != zenon_Vqn)
% 0.54/0.89  (zenon_Vgh != zenon_Vmi)
% 0.54/0.89  (zenon_Vgh != zenon_Vhn)
% 0.54/0.89  (zenon_Vqi != zenon_Vmg)
% 0.54/0.89  (zenon_Vgh != zenon_Vbe)
% 0.54/0.89  (zenon_Vqi != zenon_Vrf)
% 0.54/0.89  (zenon_Vgh != zenon_Vgb)
% 0.54/0.89  (zenon_Voi != zenon_Vfc)
% 0.54/0.89  (zenon_Vqi != zenon_Vhn)
% 0.54/0.89  (zenon_Vgh != zenon_Vlk)
% 0.54/0.89  (zenon_Vgh != zenon_Vlh)
% 0.14/0.90  (zenon_Vih != zenon_Vzh)
% 0.14/0.90  (zenon_Vgh != zenon_Vhb)
% 0.14/0.90  (zenon_Vqi != zenon_Vjj)
% 0.14/0.90  (-. (p1 zenon_Vgc))
% 0.14/0.90  (-. (p1 zenon_Vlg))
% 0.14/0.90  (zenon_Vih != zenon_Vkk)
% 0.14/0.90  (r1 zenon_Vei zenon_Vfi)
% 0.14/0.90  (zenon_Voi != zenon_Vnn)
% 0.14/0.90  (r1 zenon_Vof zenon_Vrf)
% 0.14/0.90  (r1 zenon_Vnk zenon_Vqk)
% 0.14/0.90  (-. (p1 zenon_Vrn))
% 0.14/0.90  (zenon_Voi != zenon_Vmg)
% 0.14/0.90  (-. (p1 zenon_Vuh))
% 0.14/0.90  (zenon_Voi != zenon_Vmb)
% 0.14/0.90  (zenon_Vgh != zenon_Vxm)
% 0.14/0.90  (zenon_Voi != zenon_Vgb)
% 0.14/0.90  (zenon_Vih != zenon_Val)
% 0.14/0.90  (r1 zenon_Vdm zenon_Vgm)
% 0.14/0.90  (p1 zenon_Voi)
% 0.14/0.90  (r1 zenon_Vgd zenon_Vjd)
% 0.14/0.90  (zenon_Vqi != zenon_Vak)
% 0.14/0.90  (zenon_Voi != zenon_Vfl)
% 0.14/0.90  (zenon_Voi != zenon_Vlg)
% 0.14/0.90  (zenon_Vgh != zenon_Vri)
% 0.14/0.90  (zenon_Vgh != zenon_Vrg)
% 0.14/0.90  (zenon_Voi != zenon_Vrn)
% 0.14/0.90  (r1 zenon_Vqi zenon_Vri)
% 0.14/0.90  (zenon_Voi != zenon_Vym)
% 0.14/0.90  (zenon_Voi != zenon_Vtl)
% 0.14/0.90  (-. (p1 zenon_Vlk))
% 0.14/0.90  (zenon_Vqi != zenon_Vga)
% 0.14/0.90  (zenon_Voi != zenon_Vrf)
% 0.14/0.90  (zenon_Vih != zenon_Vmi)
% 0.14/0.90  (zenon_Vih != zenon_Vwn)
% 0.14/0.90  (zenon_Voi != zenon_Vga)
% 0.14/0.90  (r1 zenon_Vtn zenon_Vwn)
% 0.14/0.90  (zenon_Voi != zenon_Vhb)
% 0.14/0.90  (zenon_Voi != zenon_Vbe)
% 0.14/0.90  *)
% 0.14/0.90  (* NO-PROOF *)
% 0.14/0.90  % SZS status GaveUp
% 0.14/0.90  Number of rewrites on terms: 0
% 0.14/0.90  Number of rewrites on props: 0
% 0.14/0.90  nodes searched: 911
% 0.14/0.90  max branch formulas: 1034
% 0.14/0.90  proof nodes created: 0
% 0.14/0.90  formulas created: 5317
% 0.14/0.90  
%------------------------------------------------------------------------------