↑ Up

ZenonModulo---0.5.0.UNK-Non.f

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

% Computer : n028.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:13 PM UTC 2026

% Result   : Unknown 0.63s 1.00s
% Output   : None 
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : LCL641+1.020 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03  % Command  : run_zenon_modulo %d %s
% 0.07/0.35  % Computer : n028.cluster.edu
% 0.07/0.35  % Model    : x86_64 x86_64
% 0.07/0.35  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.35  % Memory   : 8046.5625MB
% 0.07/0.35  % OS       : Linux 6.8.0-71-generic
% 0.07/0.35  % CPULimit : 300
% 0.07/0.35  % WCLimit  : 300
% 0.07/0.35  % DateTime : Fri Sep  4 23:57:14 UTC 2026
% 0.07/0.35  % CPUTime  : 
% 0.63/1.00  Zenon error: exhausted search space without finding a proof
% 0.63/1.00  (* Current branch:
% 0.63/1.00  (zenon_Vci != zenon_Vnm)
% 0.63/1.00  (zenon_Vai != zenon_Vjc)
% 0.63/1.00  (r1 zenon_Vtj zenon_Vuj)
% 0.63/1.00  (zenon_Vai != zenon_Vyn)
% 0.63/1.00  (zenon_Vsj != zenon_Vep)
% 0.63/1.00  (zenon_Vsj != zenon_Vfp)
% 0.63/1.00  (zenon_Vci != zenon_Vik)
% 0.63/1.00  (zenon_Vuj != zenon_Vob)
% 0.63/1.00  (-. (p1 zenon_Vim))
% 0.63/1.00  (-. (p1 zenon_Vvi))
% 0.63/1.00  (zenon_Vai != zenon_Vjk)
% 0.63/1.00  (r1 zenon_Vzm zenon_Vcn)
% 0.63/1.00  (r1 zenon_Vka zenon_Vna)
% 0.63/1.00  (r1 zenon_Vuf zenon_Vyf)
% 0.63/1.00  (-. (p1 zenon_Vug))
% 0.63/1.00  (zenon_Vsj != zenon_Vna)
% 0.63/1.00  (zenon_Vai != zenon_Vxn)
% 0.63/1.00  (zenon_Vuj != zenon_Vle)
% 0.63/1.00  (-. (p1 zenon_Vjk))
% 0.63/1.00  (zenon_Vai != zenon_Vib)
% 0.63/1.00  (zenon_Vci != zenon_Via)
% 0.63/1.00  (zenon_Vuj != zenon_Vjb)
% 0.63/1.00  (zenon_Vci != zenon_Vvj)
% 0.63/1.00  (zenon_Vsj != zenon_Vim)
% 0.63/1.00  (zenon_Vci != zenon_Vuo)
% 0.63/1.00  (zenon_Vuj != zenon_Vsl)
% 0.63/1.00  (zenon_Vsj != zenon_Vki)
% 0.63/1.00  (r1 zenon_Vlk zenon_Vok)
% 0.63/1.00  (-. (p1 zenon_Vji))
% 0.63/1.00  (-. (p1 zenon_Vwm))
% 0.63/1.00  (zenon_Vai != zenon_Vcf)
% 0.63/1.00  (r1 zenon_Vie zenon_Vle)
% 0.63/1.00  (zenon_Vuj != zenon_Vjc)
% 0.63/1.00  (zenon_Vai != zenon_Vdo)
% 0.63/1.00  (r1 zenon_Vek zenon_Vik)
% 0.63/1.00  (r1 zenon_Veb zenon_Vib)
% 0.63/1.00  (-. (p1 zenon_Vsl))
% 0.63/1.00  (zenon_Vai != zenon_Vep)
% 0.63/1.00  (zenon_Vuj != zenon_Vvi)
% 0.63/1.00  (zenon_Vsj != zenon_Vid)
% 0.63/1.00  (zenon_Vuj != zenon_Vcn)
% 0.63/1.00  (zenon_Vai != zenon_Vna)
% 0.63/1.00  (zenon_Vai != zenon_Vzf)
% 0.63/1.00  (zenon_Vsj != zenon_Vob)
% 0.63/1.00  (zenon_Vsj != zenon_Vjc)
% 0.63/1.00  (-. (p1 zenon_Vna))
% 0.63/1.00  (zenon_Vsj != zenon_Vib)
% 0.63/1.00  (zenon_Vai != zenon_Vui)
% 0.63/1.00  (zenon_Vci != zenon_Vok)
% 0.63/1.00  (zenon_Vai != zenon_Vid)
% 0.63/1.00  (zenon_Vuj != zenon_Vna)
% 0.63/1.00  (r1 zenon_Vkd zenon_Vnd)
% 0.63/1.00  (zenon_Vci != zenon_Vzg)
% 0.63/1.00  (zenon_Vuj != zenon_Vgl)
% 0.63/1.00  (zenon_Vai != zenon_Vxm)
% 0.63/1.00  (zenon_Vai != zenon_Vic)
% 0.63/1.00  (r1 zenon_Vci zenon_Vfi)
% 0.63/1.00  (zenon_Vuj != zenon_Vjk)
% 0.63/1.00  (zenon_Vsj != zenon_Vcf)
% 0.63/1.00  (zenon_Vsj != zenon_Vsl)
% 0.63/1.00  (zenon_Vci != zenon_Vap)
% 0.63/1.00  (zenon_Vsj != zenon_Vuo)
% 0.63/1.00  (zenon_Vsj != zenon_Voc)
% 0.63/1.00  (zenon_Vuj != zenon_Vvo)
% 0.63/1.00  (zenon_Vsj != zenon_Vge)
% 0.63/1.00  (zenon_Vsj != zenon_Vyn)
% 0.63/1.00  (-. (p1 zenon_Vik))
% 0.63/1.00  (zenon_Vuj != zenon_Vqj)
% 0.63/1.00  (r1 zenon_Vzi zenon_Vaj)
% 0.63/1.00  (zenon_Vai != zenon_Vug)
% 0.63/1.00  (-. (p1 zenon_Vyn))
% 0.63/1.00  (-. (p1 zenon_Vcf))
% 0.63/1.00  (zenon_Vsj != zenon_Vqn)
% 0.63/1.00  (zenon_Vai != zenon_Vle)
% 0.63/1.00  (-. (p1 zenon_Vkn))
% 0.63/1.00  (zenon_Vuj != zenon_Veg)
% 0.63/1.00  (r1 Tau_0 Tau_1)
% 0.63/1.00  (zenon_Vsj != zenon_Vko)
% 0.63/1.00  (zenon_Vuj != zenon_Vzf)
% 0.63/1.00  (r1 zenon_Vgn zenon_Vkn)
% 0.63/1.00  (r1 zenon_Vmj zenon_Vnj)
% 0.63/1.00  (zenon_Vai != zenon_Vkn)
% 0.63/1.00  (r1 zenon_Vxi zenon_Vyi)
% 0.63/1.00  (zenon_Vsj != zenon_Vfe)
% 0.63/1.00  (zenon_Vsj != zenon_Vok)
% 0.63/1.00  (zenon_Vai != zenon_Vcn)
% 0.63/1.00  (-. (p1 zenon_Vtg))
% 0.63/1.00  (r1 zenon_Vtn zenon_Vxn)
% 0.63/1.00  (zenon_Vci != zenon_Vle)
% 0.63/1.00  (zenon_Vci != zenon_Vtg)
% 0.63/1.00  (zenon_Vci != zenon_Vhd)
% 0.63/1.00  (zenon_Vsj != zenon_Val)
% 0.63/1.00  (zenon_Vai != zenon_Vpi)
% 0.63/1.00  (zenon_Vci != zenon_Vxn)
% 0.63/1.00  (zenon_Vci != zenon_Vpi)
% 0.63/1.00  (-. (p1 zenon_Val))
% 0.63/1.00  (-. (p1 zenon_Vle))
% 0.63/1.00  (zenon_Vuj != zenon_Vzg)
% 0.63/1.00  (zenon_Vuj != zenon_Vji)
% 0.63/1.00  (zenon_Vai != zenon_Veg)
% 0.63/1.00  (zenon_Vci != zenon_Vui)
% 0.63/1.00  (r1 zenon_Voj zenon_Vpj)
% 0.63/1.00  (zenon_Vsj != zenon_Vha)
% 0.63/1.00  (zenon_Vsj != zenon_Vdf)
% 0.63/1.00  (zenon_Vci != zenon_Vfp)
% 0.63/1.00  (zenon_Vai != zenon_Vob)
% 0.63/1.00  (zenon_Vsj != zenon_Vxn)
% 0.63/1.00  (zenon_Vuj != zenon_Vpi)
% 0.63/1.00  (r1 zenon_Vbj zenon_Vcj)
% 0.63/1.00  (r1 zenon_Vai zenon_Vbi)
% 0.63/1.00  (zenon_Vuj != zenon_Vfp)
% 0.63/1.00  (zenon_Vuj != zenon_Vtg)
% 0.63/1.00  (zenon_Vci != zenon_Vic)
% 0.63/1.00  (r1 zenon_Vlb zenon_Vob)
% 0.63/1.00  (r1 zenon_Vsm zenon_Vwm)
% 0.63/1.00  (zenon_Vai != zenon_Vbi)
% 0.63/1.00  (zenon_Vsj != zenon_Vxl)
% 0.63/1.00  (zenon_Vuj != zenon_Vkn)
% 0.63/1.00  (-. (p1 zenon_Vap))
% 0.63/1.00  (zenon_Vsj != zenon_Vpi)
% 0.63/1.00  (zenon_Vuj != zenon_Vwm)
% 0.63/1.00  (zenon_Vsj != zenon_Vtg)
% 0.63/1.00  (zenon_Vci != zenon_Vvi)
% 0.63/1.00  (zenon_Vci != zenon_Vpo)
% 0.63/1.00  (zenon_Vai != zenon_Vsl)
% 0.63/1.00  (zenon_Vci != zenon_Vyf)
% 0.63/1.00  (r1 zenon_Vjj zenon_Vkj)
% 0.63/1.00  (zenon_Vci != zenon_Vid)
% 0.63/1.00  (zenon_Vci != zenon_Vxl)
% 0.63/1.00  (-. (p1 zenon_Vvj))
% 0.63/1.00  (zenon_Vci != zenon_Vib)
% 0.63/1.00  (zenon_Vuj != zenon_Vge)
% 0.63/1.00  (zenon_Vsj != zenon_Vln)
% 0.63/1.00  (zenon_Vci != zenon_Vjo)
% 0.63/1.00  (zenon_Vsj != zenon_Vji)
% 0.63/1.00  (-. (p1 zenon_Veg))
% 0.63/1.00  (zenon_Vci != zenon_Vfi)
% 0.63/1.00  (zenon_Vai != zenon_Vki)
% 0.63/1.00  (zenon_Vci != zenon_Vxm)
% 0.63/1.00  (-. (p1 zenon_Vbl))
% 0.63/1.00  (r1 zenon_Vqo zenon_Vuo)
% 0.63/1.00  (r1 zenon_Vwk zenon_Val)
% 0.63/1.00  (zenon_Vuj != zenon_Vif)
% 0.63/1.00  (zenon_Vsj != zenon_Vdo)
% 0.63/1.00  (zenon_Vci != zenon_Vsl)
% 0.63/1.00  (-. (p1 zenon_Vnd))
% 0.63/1.00  (-. (p1 zenon_Vib))
% 0.63/1.00  (-. (p1 zenon_Via))
% 0.63/1.00  (zenon_Vuj != zenon_Vjo)
% 0.63/1.00  (zenon_Vsj != zenon_Vpo)
% 0.63/1.00  (zenon_Vuj != zenon_Vdf)
% 0.63/1.00  (zenon_Vci != zenon_Vug)
% 0.63/1.00  (-. (p1 zenon_Vjo))
% 0.63/1.00  (zenon_Vci != zenon_Vki)
% 0.63/1.00  (zenon_Vai != zenon_Vnm)
% 0.63/1.00  (zenon_Vai != zenon_Vif)
% 0.63/1.00  (zenon_Vai != zenon_Via)
% 0.63/1.00  (zenon_Vsj != zenon_Vui)
% 0.63/1.00  (zenon_Vuj != zenon_Vib)
% 0.63/1.00  (r1 zenon_Vye zenon_Vcf)
% 0.63/1.00  (zenon_Vuj != zenon_Vap)
% 0.63/1.00  (zenon_Vai != zenon_Vbl)
% 0.63/1.00  (r1 zenon_Vdm zenon_Vhm)
% 0.63/1.00  (r1 zenon_Vej zenon_Vfj)
% 0.63/1.00  (zenon_Vsj != zenon_Vug)
% 0.63/1.00  (r1 zenon_Vbe zenon_Vfe)
% 0.63/1.00  (zenon_Vuj != zenon_Vbi)
% 0.63/1.00  (zenon_Vuj != zenon_Vkp)
% 0.63/1.00  (-. (p1 zenon_Vep))
% 0.63/1.00  (r1 zenon_Vbg zenon_Veg)
% 0.63/1.00  (zenon_Vai != zenon_Vnd)
% 0.63/1.00  (r1 zenon_Vqj zenon_Vrj)
% 0.63/1.00  (-. (p1 zenon_Vgl))
% 0.63/1.00  (zenon_Vuj != zenon_Vvj)
% 0.63/1.00  (r1 zenon_Vaj zenon_Vbj)
% 0.63/1.00  (zenon_Vsj != zenon_Vhm)
% 0.63/1.00  (r1 zenon_Vij zenon_Vjj)
% 0.63/1.00  (-. (p1 zenon_Vpo))
% 0.63/1.00  (-. (p1 zenon_Vxl))
% 0.63/1.00  (zenon_Vai != zenon_Vqj)
% 0.63/1.00  (-. (p1 zenon_Vpi))
% 0.63/1.00  (zenon_Vuj != zenon_Vqn)
% 0.63/1.00  (zenon_Vai != zenon_Vgl)
% 0.63/1.00  (zenon_Vuj != zenon_Vic)
% 0.63/1.00  (zenon_Vuj != zenon_Vxm)
% 0.63/1.00  (-. (p1 zenon_Vfi))
% 0.63/1.00  (r1 zenon_Vcj zenon_Vdj)
% 0.63/1.00  (zenon_Vci != zenon_Vbi)
% 0.63/1.00  (zenon_Vsj != zenon_Vzg)
% 0.63/1.00  (zenon_Vai != zenon_Vok)
% 0.63/1.00  (r1 zenon_Vnj zenon_Voj)
% 0.63/1.00  (zenon_Vai != zenon_Vyf)
% 0.63/1.00  (zenon_Vci != zenon_Veg)
% 0.63/1.00  (zenon_Vci != zenon_Vcf)
% 0.63/1.00  (zenon_Vai != zenon_Vzg)
% 0.63/1.00  (-. (p1 zenon_Vob))
% 0.63/1.00  (zenon_Vai != zenon_Vjo)
% 0.63/1.00  (-. (p1 zenon_Vhd))
% 0.63/1.00  (zenon_Vai != zenon_Vvj)
% 0.63/1.00  (-. (p1 zenon_Vjc))
% 0.63/1.00  (r1 zenon_Vnl zenon_Vrl)
% 0.63/1.00  (r1 zenon_Vfj zenon_Vgj)
% 0.63/1.00  (zenon_Vai != zenon_Vvo)
% 0.63/1.00  (-. (p1 zenon_Vuo))
% 0.63/1.00  (-. (p1 zenon_Vfp))
% 0.63/1.00  (zenon_Vci != zenon_Vvo)
% 0.63/1.00  (zenon_Vci != zenon_Vob)
% 0.63/1.00  (zenon_Vuj != zenon_Vln)
% 0.63/1.00  (zenon_Vsj != zenon_Vbi)
% 0.63/1.00  (zenon_Vai != zenon_Voc)
% 0.63/1.00  (zenon_Vsj != zenon_Vvi)
% 0.63/1.00  (zenon_Vai != zenon_Vpo)
% 0.63/1.00  (r1 zenon_Vuj zenon_Vvj)
% 0.63/1.00  (zenon_Vci != zenon_Vif)
% 0.63/1.00  (r1 zenon_Vlc zenon_Voc)
% 0.63/1.00  (zenon_Vci != zenon_Vqj)
% 0.63/1.00  (r1 zenon_Vul zenon_Vxl)
% 0.63/1.00  (r1 Tau_1 zenon_Vxi)
% 0.63/1.00  (-. (p1 zenon_Vzf))
% 0.63/1.00  (zenon_Vci != zenon_Vfe)
% 0.63/1.00  (zenon_Vci != zenon_Vjk)
% 0.63/1.00  (zenon_Vuj != zenon_Vim)
% 0.63/1.00  (r1 zenon_Vhj zenon_Vij)
% 0.63/1.00  (zenon_Vuj != zenon_Vok)
% 0.63/1.00  (-. (p1 zenon_Vdf))
% 0.63/1.00  (-. (p1 zenon_Vki))
% 0.63/1.00  (r1 zenon_Vdl zenon_Vgl)
% 0.63/1.00  (-. (p1 zenon_Vcn))
% 0.63/1.00  (zenon_Vai != zenon_Vfe)
% 0.63/1.00  (zenon_Vai != zenon_Vap)
% 0.63/1.00  (zenon_Vsj != zenon_Vjo)
% 0.63/1.00  (zenon_Vuj != zenon_Vnd)
% 0.63/1.00  (-. (p1 zenon_Vbi))
% 0.63/1.00  (r1 zenon_Vmi zenon_Vpi)
% 0.63/1.00  (zenon_Vsj != zenon_Vgl)
% 0.63/1.00  (p1 zenon_Vsj)
% 0.63/1.00  (zenon_Vsj != zenon_Vcn)
% 0.63/1.00  (r1 zenon_Vdd zenon_Vhd)
% 0.63/1.00  (zenon_Vsj != zenon_Via)
% 0.63/1.00  (-. (p1 zenon_Vnm))
% 0.63/1.00  (zenon_Vci != zenon_Vha)
% 0.63/1.00  (zenon_Vuj != zenon_Vbl)
% 0.63/1.00  (zenon_Vuj != zenon_Vxn)
% 0.63/1.00  (zenon_Vci != zenon_Vyn)
% 0.63/1.00  (zenon_Vci != zenon_Val)
% 0.63/1.00  (-. (p1 zenon_Vxn))
% 0.63/1.00  (zenon_Vsj != zenon_Vqj)
% 0.63/1.00  (zenon_Vai != zenon_Val)
% 0.63/1.00  (p1 zenon_Vai)
% 0.63/1.00  (zenon_Vsj != zenon_Vhd)
% 0.63/1.00  (zenon_Vci != zenon_Vcn)
% 0.63/1.00  (-. (p1 zenon_Vha))
% 0.63/1.00  (zenon_Vsj != zenon_Vik)
% 0.63/1.00  (zenon_Vuj != zenon_Vko)
% 0.63/1.00  (r1 zenon_Vyi zenon_Vzi)
% 0.63/1.00  (zenon_Vci != zenon_Vhm)
% 0.63/1.00  (-. (p1 zenon_Vqn))
% 0.63/1.00  (zenon_Vuj != zenon_Vnm)
% 0.63/1.00  (zenon_Vci != zenon_Vjc)
% 0.63/1.00  (r1 zenon_Vhp zenon_Vkp)
% 0.63/1.00  (zenon_Vsj != zenon_Vyf)
% 0.63/1.00  (zenon_Vsj != zenon_Vbl)
% 0.63/1.00  (zenon_Vci != zenon_Vln)
% 0.63/1.00  (-. (p1 zenon_Vge))
% 0.63/1.00  (zenon_Vsj != zenon_Vjb)
% 0.63/1.00  (zenon_Vai != zenon_Vik)
% 0.63/1.00  (zenon_Vai != zenon_Vhm)
% 0.63/1.00  (zenon_Vci != zenon_Vgl)
% 0.63/1.00  (r1 zenon_Vao zenon_Vdo)
% 0.63/1.00  (zenon_Vai != zenon_Vjb)
% 0.63/1.00  (zenon_Vci != zenon_Vkp)
% 0.63/1.00  (-. (p1 zenon_Vic))
% 0.63/1.00  (zenon_Vsj != zenon_Vvo)
% 0.63/1.00  (zenon_Vuj != zenon_Vcf)
% 0.63/1.00  (zenon_Vsj != zenon_Vvj)
% 0.63/1.00  (-. (p1 zenon_Vif))
% 0.63/1.00  (zenon_Vuj != zenon_Vik)
% 0.63/1.00  (zenon_Vai != zenon_Vln)
% 0.63/1.00  (zenon_Vai != zenon_Vqn)
% 0.63/1.00  (-. (p1 zenon_Voc))
% 0.63/1.00  (zenon_Vai != zenon_Vwm)
% 0.63/1.00  (r1 zenon_Vwg zenon_Vzg)
% 0.63/1.00  (r1 zenon_Vkm zenon_Vnm)
% 0.63/1.00  (zenon_Vci != zenon_Vbl)
% 0.63/1.00  (zenon_Vuj != zenon_Vdo)
% 0.63/1.00  (-. (p1 zenon_Vid))
% 0.63/1.00  (r1 zenon_Vgj zenon_Vhj)
% 0.63/1.00  (zenon_Vuj != zenon_Vyn)
% 0.63/1.00  (zenon_Vai != zenon_Vha)
% 0.63/1.00  (r1 zenon_Vth zenon_Vji)
% 0.63/1.00  (zenon_Vuj != zenon_Vyf)
% 0.63/1.00  (zenon_Vuj != zenon_Vhd)
% 0.63/1.00  (zenon_Vsj != zenon_Vkp)
% 0.63/1.00  (zenon_Vai != zenon_Vge)
% 0.63/1.00  (r1 zenon_X20 zenon_Vep)
% 0.63/1.00  (zenon_Vuj != zenon_Vxl)
% 0.63/1.00  (zenon_Vuj != zenon_Vug)
% 0.63/1.00  (zenon_Vci != zenon_Vkn)
% 0.63/1.00  (zenon_Vai != zenon_Vdf)
% 0.63/1.00  (zenon_Vci != zenon_Vep)
% 0.63/1.00  (zenon_Vsj != zenon_Vjk)
% 0.63/1.00  (zenon_Vci != zenon_Vji)
% 0.63/1.00  (zenon_Vci != zenon_Vwm)
% 0.63/1.00  (zenon_Vuj != zenon_Vfe)
% 0.63/1.00  (zenon_Vuj != zenon_Val)
% 0.63/1.00  (zenon_Vai != zenon_Vtg)
% 0.63/1.00  (zenon_Vsj != zenon_Vkn)
% 0.63/1.00  (zenon_Vuj != zenon_Vki)
% 0.63/1.00  (zenon_Vci != zenon_Vnd)
% 0.63/1.00  (zenon_Vai != zenon_Vuo)
% 0.63/1.00  (r1 zenon_Vda zenon_Vha)
% 0.63/1.00  (-. (p1 zenon_Vdo))
% 0.63/1.00  (-. (p1 zenon_Vjb))
% 0.63/1.00  (-. (p1 zenon_Vxm))
% 0.63/1.00  (zenon_Vuj != zenon_Vhm)
% 0.63/1.00  (zenon_Vci != zenon_Vjb)
% 0.63/1.00  (zenon_Vai != zenon_Vfp)
% 0.63/1.00  (r1 zenon_Vff zenon_Vif)
% 0.63/1.00  (-. (p1 zenon_Vui))
% 0.63/1.00  (p1 zenon_Vci)
% 0.63/1.00  (zenon_Vsj != zenon_Vxm)
% 0.63/1.00  (zenon_Vuj != zenon_Vrl)
% 0.63/1.00  (zenon_Vuj != zenon_Vep)
% 0.63/1.00  (r1 zenon_Vpg zenon_Vtg)
% 0.63/1.00  (zenon_Vuj != zenon_Vid)
% 0.63/1.00  (zenon_Vai != zenon_Vfi)
% 0.63/1.00  (zenon_Vuj != zenon_Voc)
% 0.63/1.00  (zenon_Vuj != zenon_Vfi)
% 0.63/1.00  (zenon_Vai != zenon_Vko)
% 0.63/1.00  (zenon_Vai != zenon_Vhd)
% 0.63/1.00  (-. (p1 zenon_Vko))
% 0.63/1.00  (-. (p1 zenon_Vyf))
% 0.63/1.00  (zenon_Vsj != zenon_Vfi)
% 0.63/1.00  (zenon_Vuj != zenon_Vui)
% 0.63/1.00  (zenon_Vci != zenon_Vge)
% 0.63/1.00  (r1 zenon_Vfo zenon_Vjo)
% 0.63/1.00  (-. (p1 zenon_Vln))
% 0.63/1.00  (zenon_Vci != zenon_Vrl)
% 0.63/1.00  (zenon_Vsj != zenon_Vzf)
% 0.63/1.00  (r1 zenon_Vmo zenon_Vpo)
% 0.63/1.00  (zenon_Vsj != zenon_Vic)
% 0.63/1.00  (zenon_Vci != zenon_Vqn)
% 0.63/1.00  (zenon_Vsj != zenon_Vnd)
% 0.63/1.00  (zenon_Vuj != zenon_Vha)
% 0.63/1.00  (zenon_Vai != zenon_Vkp)
% 0.63/1.00  (-. (p1 zenon_Vvo))
% 0.63/1.00  (zenon_Vuj != zenon_Vuo)
% 0.63/1.00  (zenon_Vsj != zenon_Vif)
% 0.63/1.00  (zenon_Vai != zenon_Vim)
% 0.63/1.00  (zenon_Vci != zenon_Vdo)
% 0.63/1.00  (zenon_Vci != zenon_Voc)
% 0.63/1.00  (zenon_Vuj != zenon_Vpo)
% 0.63/1.00  (zenon_Vci != zenon_Vko)
% 0.63/1.00  (zenon_Vai != zenon_Vxl)
% 0.63/1.00  (zenon_Vci != zenon_Vzf)
% 0.63/1.00  (zenon_Vci != zenon_Vna)
% 0.63/1.00  (-. (p1 zenon_Vqj))
% 0.63/1.00  (zenon_Vai != zenon_Vji)
% 0.63/1.00  (zenon_Vci != zenon_Vim)
% 0.63/1.00  (zenon_Vai != zenon_Vvi)
% 0.63/1.00  (p1 zenon_Vuj)
% 0.63/1.00  (r1 zenon_Vdj zenon_Vej)
% 0.63/1.00  (zenon_Vsj != zenon_Vle)
% 0.63/1.00  (zenon_Vai != zenon_Vrl)
% 0.63/1.00  (r1 zenon_Vxo zenon_Vap)
% 0.63/1.00  (-. (p1 zenon_Vfe))
% 0.63/1.00  (zenon_Vsj != zenon_Vap)
% 0.63/1.00  (-. (p1 zenon_Vrl))
% 0.63/1.00  (-. (p1 zenon_Vok))
% 0.63/1.00  (r1 zenon_Vth zenon_Vai)
% 0.63/1.00  (-. (p1 zenon_Vkp))
% 0.63/1.00  (r1 zenon_Vnn zenon_Vqn)
% 0.63/1.00  (r1 zenon_Vpj zenon_Vqj)
% 0.63/1.00  (r1 zenon_Vkj zenon_Vlj)
% 0.63/1.00  (r1 zenon_Vec zenon_Vic)
% 0.63/1.00  (zenon_Vuj != zenon_Via)
% 0.63/1.00  (zenon_Vci != zenon_Vdf)
% 0.63/1.00  (r1 zenon_Vlj zenon_Vmj)
% 0.63/1.00  (zenon_Vsj != zenon_Vnm)
% 0.63/1.00  (zenon_Vsj != zenon_Veg)
% 0.63/1.00  (zenon_Vsj != zenon_Vwm)
% 0.63/1.00  (-. (p1 zenon_Vhm))
% 0.63/1.00  (-. (p1 zenon_Vzg))
% 0.63/1.00  (r1 zenon_Vth zenon_Vui)
% 0.63/1.00  (zenon_Vsj != zenon_Vrl)
% 0.63/1.00  *)
% 0.63/1.00  (* NO-PROOF *)
% 0.63/1.00  % SZS status GaveUp
% 0.63/1.00  Number of rewrites on terms: 0
% 0.63/1.00  Number of rewrites on props: 0
% 0.63/1.00  nodes searched: 958
% 0.63/1.00  max branch formulas: 1090
% 0.63/1.00  proof nodes created: 0
% 0.63/1.00  formulas created: 5699
% 0.63/1.00  
%------------------------------------------------------------------------------