↑ Up

ZenonModulo---0.5.0.UNK-Non.f

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

% Computer : n001.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 3.13s 3.47s
% Output   : None 
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : LCL668+1.010 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03  % Command  : run_zenon_modulo %d %s
% 0.08/0.36  % Computer : n001.cluster.edu
% 0.08/0.36  % Model    : x86_64 x86_64
% 0.08/0.36  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36  % Memory   : 8046.5625MB
% 0.08/0.36  % OS       : Linux 6.8.0-71-generic
% 0.08/0.36  % CPULimit : 300
% 0.08/0.36  % WCLimit  : 300
% 0.08/0.36  % DateTime : Fri Sep  4 17:28:59 UTC 2026
% 0.12/0.36  % CPUTime  : 
% 3.13/3.46  Zenon error: exhausted search space without finding a proof
% 3.13/3.46  (* Current branch:
% 3.13/3.46  (-. (p1 zenon_Vdkb))
% 3.13/3.46  (-. (p44 zenon_Vat))
% 3.13/3.46  (r1 zenon_Vjb zenon_Vkb)
% 3.13/3.46  (zenon_Vrla != zenon_Vsla)
% 3.13/3.46  (zenon_Vnha != zenon_Voha)
% 3.13/3.46  (zenon_Vzhb != zenon_Vaib)
% 3.13/3.46  (r1 zenon_Vcda zenon_Vpea)
% 3.13/3.46  (-. (p45 zenon_Vip))
% 3.13/3.46  (-. (p4 zenon_Vmhb))
% 3.13/3.46  (r1 zenon_Vma zenon_Vna)
% 3.13/3.46  (-. (p24 zenon_Vaua))
% 3.13/3.46  (zenon_Vaxa != zenon_Vbwa)
% 3.13/3.46  (zenon_Vln != zenon_Vmn)
% 3.13/3.46  (zenon_Vmab != zenon_Vnab)
% 3.13/3.46  (r1 zenon_Vea zenon_Vfa)
% 3.13/3.46  (-. (p44 zenon_Ver))
% 3.13/3.46  (-. (p46 zenon_Vjp))
% 3.13/3.46  (zenon_Vgbb != zenon_Vmab)
% 3.13/3.46  (r1 zenon_Vwib zenon_Vxib)
% 3.13/3.46  (p28 zenon_Vrqa)
% 3.13/3.46  (-. (p50 zenon_Vnf))
% 3.13/3.46  (r1 zenon_Vdga zenon_Voha)
% 3.13/3.46  (p31 zenon_Vzma)
% 3.13/3.46  (r1 Tau_0 Tau_1)
% 3.13/3.46  (r1 zenon_Vnn zenon_Vjp)
% 3.13/3.46  (p1 zenon_Vld)
% 3.13/3.46  (r1 zenon_Vibb zenon_Vacb)
% 3.13/3.46  (r1 zenon_Vzjb zenon_Vakb)
% 3.13/3.46  (-. (p3 zenon_Vaib))
% 3.13/3.46  (r1 zenon_Vhb zenon_Vib)
% 3.13/3.46  (r1 zenon_Voa zenon_Vpa)
% 3.13/3.46  (r1 zenon_Vyjb zenon_Vzjb)
% 3.13/3.46  (-. (p30 zenon_Vzma))
% 3.13/3.46  (-. (p49 zenon_Voh))
% 3.13/3.46  (-. (p49 zenon_Vpj))
% 3.13/3.46  (-. (p20 zenon_Vyxa))
% 3.13/3.46  (r1 zenon_Vmib zenon_Vnib)
% 3.13/3.46  (r1 zenon_Vvib zenon_Vwib)
% 3.13/3.46  (zenon_Vidb != zenon_Vjdb)
% 3.13/3.46  (p34 zenon_Vyia)
% 3.13/3.46  (zenon_Vofb != zenon_Vbfb)
% 3.13/3.47  (r1 zenon_Vghb zenon_Vnhb)
% 3.13/3.47  (-. (p14 zenon_Vrcb))
% 3.13/3.47  (p2 zenon_Vkb)
% 3.13/3.47  (-. (p20 zenon_Vwya))
% 3.13/3.47  (-. (p42 zenon_Vtu))
% 3.13/3.47  (zenon_Vrcb != zenon_Vscb)
% 3.13/3.47  (zenon_Vagb != zenon_Vofb)
% 3.13/3.47  (-. (p43 zenon_Vuu))
% 3.13/3.47  (p12 zenon_Vneb)
% 3.13/3.47  (-. (p15 zenon_Vscb))
% 3.13/3.47  (-. (p38 zenon_Vlba))
% 3.13/3.47  (-. (p5 zenon_Vehb))
% 3.13/3.47  (r1 zenon_Vdfb zenon_Vpfb)
% 3.13/3.47  (r1 zenon_Vcjb zenon_Vdjb)
% 3.13/3.47  (r1 zenon_Vkp zenon_Vfr)
% 3.13/3.47  (-. (p23 zenon_Vbva))
% 3.13/3.47  (zenon_Ver != zenon_Vip)
% 3.13/3.47  (r1 zenon_Vujb zenon_Vvjb)
% 3.13/3.47  (zenon_Voh != zenon_Vph)
% 3.13/3.47  (p48 zenon_Vnl)
% 3.13/3.47  (-. (p30 zenon_Vhoa))
% 3.13/3.47  (r1 zenon_Vtcb zenon_Vjdb)
% 3.13/3.47  (zenon_Vlba != zenon_Vmba)
% 3.13/3.47  (zenon_Vip != zenon_Vjp)
% 3.13/3.47  (p35 zenon_Vnha)
% 3.13/3.47  (p11 zenon_Vbfb)
% 3.13/3.47  (zenon_Vbfb != zenon_Vcfb)
% 3.13/3.47  (-. (p19 zenon_Vvya))
% 3.13/3.47  (p45 zenon_Ver)
% 3.13/3.47  (-. (p28 zenon_Vmpa))
% 3.13/3.47  (p51 zenon_Vnf)
% 3.13/3.47  (zenon_Vika != zenon_Vjka)
% 3.13/3.47  (r1 zenon_Vz zenon_Vaa)
% 3.13/3.47  (zenon_Voj != zenon_Vpj)
% 3.13/3.47  (-. (p35 zenon_Vbga))
% 3.13/3.47  (r1 zenon_Vfb zenon_Vgb)
% 3.13/3.47  (zenon_Vvra != zenon_Vwra)
% 3.13/3.47  (zenon_Vbva != zenon_Vaua)
% 3.13/3.47  (p4 zenon_Vthb)
% 3.13/3.47  (zenon_Vgoa != zenon_Vhoa)
% 3.13/3.47  (zenon_Ver != zenon_Vfr)
% 3.13/3.47  (r1 zenon_Vcxa zenon_Vzxa)
% 3.13/3.47  (-. (p37 zenon_Vada))
% 3.13/3.47  (zenon_Vrqa != zenon_Vsqa)
% 3.13/3.47  (-. (p8 zenon_Vmgb))
% 3.13/3.47  (zenon_Vbva != zenon_Vcva)
% 3.13/3.47  (r1 zenon_Vka zenon_Vla)
% 3.13/3.47  (r1 zenon_Vrib zenon_Vsib)
% 3.13/3.47  (r1 zenon_Vha zenon_Via)
% 3.13/3.47  (r1 zenon_Viib zenon_Vjib)
% 3.13/3.47  (-. (p50 zenon_Vph))
% 3.13/3.47  (r1 zenon_Vq zenon_Vr)
% 3.13/3.47  (zenon_Vnl != zenon_Vol)
% 3.13/3.47  (r1 zenon_Vta zenon_Vua)
% 3.13/3.47  (-. (p40 zenon_Vey))
% 3.13/3.47  (r1 zenon_Vajb zenon_Vbjb)
% 3.13/3.47  (r1 zenon_Vna zenon_Voa)
% 3.13/3.47  (r1 zenon_Vwa zenon_Vxa)
% 3.13/3.47  (r1 zenon_Vx zenon_Vy)
% 3.13/3.47  (-. (p53 Tau_2))
% 3.13/3.47  (r1 zenon_Vdva zenon_Vcwa)
% 3.13/3.47  (zenon_Vrza != zenon_Vsza)
% 3.13/3.47  (r1 zenon_Vmjb zenon_Vnjb)
% 3.13/3.47  (zenon_Vyia != zenon_Vnha)
% 3.13/3.47  (zenon_Vyxa != zenon_Vaxa)
% 3.13/3.47  (p49 zenon_Voj)
% 3.13/3.47  (r1 zenon_Vfa zenon_Vga)
% 3.13/3.47  (zenon_Vlba != zenon_Vvz)
% 3.13/3.47  (r1 zenon_Vbb zenon_Vcb)
% 3.13/3.47  (r1 Tau_0 Tau_3)
% 3.13/3.47  (-. (p29 zenon_Vnpa))
% 3.13/3.47  (zenon_Vgbb != zenon_Vhbb)
% 3.13/3.47  (p38 zenon_Vada)
% 3.13/3.47  (zenon_Vrqa != zenon_Vmpa)
% 3.13/3.47  (r1 zenon_Vtqa zenon_Vwra)
% 3.13/3.47  (r1 zenon_Vbjb zenon_Vcjb)
% 3.13/3.47  (r1 zenon_Vlib zenon_Vmib)
% 3.13/3.47  (-. (p12 zenon_Voeb))
% 3.13/3.47  (zenon_Vbwa != zenon_Vcwa)
% 3.13/3.47  (r1 zenon_Vnib zenon_Voib)
% 3.13/3.47  (p21 zenon_Vyxa)
% 3.13/3.47  (zenon_Vysa != zenon_Vzsa)
% 3.13/3.47  (p37 zenon_Voea)
% 3.13/3.47  (-. (p51 zenon_Vof))
% 3.13/3.47  (r1 zenon_Vib zenon_Vjb)
% 3.13/3.47  (r1 zenon_Vohb zenon_Vuhb)
% 3.13/3.47  (zenon_Vrcb != zenon_Vzbb)
% 3.13/3.47  (p7 zenon_Vvgb)
% 3.13/3.47  (p23 zenon_Vbwa)
% 3.13/3.47  (r1 zenon_Vgib zenon_Vhib)
% 3.13/3.47  (p47 zenon_Vln)
% 3.13/3.47  (zenon_Vkb != zenon_Vzhb)
% 3.13/3.47  (r1 zenon_Vxjb zenon_Vyjb)
% 3.13/3.47  (r1 zenon_Vhib zenon_Viib)
% 3.13/3.47  (r1 Tau_1 zenon_Vm)
% 3.13/3.47  (r1 zenon_Vpl zenon_Vmn)
% 3.13/3.47  (zenon_Vnl != zenon_Voj)
% 3.13/3.47  (p15 zenon_Vrcb)
% 3.13/3.47  (-. (p17 zenon_Vmab))
% 3.13/3.47  (-. (p25 zenon_Vbua))
% 3.13/3.47  (zenon_Vey != zenon_Vfy)
% 3.13/3.47  (r1 zenon_Vsa zenon_Vta)
% 3.13/3.47  (r1 zenon_Vpf zenon_Vph)
% 3.13/3.47  (r1 zenon_Vopa zenon_Vsqa)
% 3.13/3.47  (r1 zenon_Vxya zenon_Vsza)
% 3.13/3.47  (r1 zenon_Vr zenon_Vs)
% 3.13/3.47  (r1 zenon_Vtjb zenon_Vujb)
% 3.13/3.47  (zenon_Vaua != zenon_Vysa)
% 3.13/3.47  (r1 zenon_Vxz zenon_Vmba)
% 3.13/3.47  (-. (p12 zenon_Vydb))
% 3.13/3.47  (zenon_Vvya != zenon_Vwya)
% 3.13/3.47  (-. (p42 zenon_Vnw))
% 3.13/3.47  (-. (p35 zenon_Voha))
% 3.13/3.47  (-. (p43 zenon_Vzs))
% 3.13/3.47  (-. (p31 zenon_Vrla))
% 3.13/3.47  (-. (p40 zenon_Vwz))
% 3.13/3.47  (r1 zenon_Vs zenon_Vt)
% 3.13/3.47  (zenon_Vvgb != zenon_Vwgb)
% 3.13/3.47  (r1 zenon_Vkdb zenon_Vzdb)
% 3.13/3.47  (-. (p6 zenon_Vfhb))
% 3.13/3.47  (-. (p29 zenon_Vgoa))
% 3.13/3.47  (-. (p13 zenon_Vidb))
% 3.13/3.47  (-. (p27 zenon_Vrqa))
% 3.13/3.47  (-. (p11 zenon_Vneb))
% 3.13/3.47  (-. (p4 zenon_Vuhb))
% 3.13/3.47  (p25 zenon_Vaua)
% 3.13/3.47  (zenon_Vydb != zenon_Vzdb)
% 3.13/3.47  (-. (p52 zenon_Vmd))
% 3.13/3.47  (r1 zenon_Vm zenon_Vn)
% 3.13/3.47  (p2 zenon_Veib)
% 3.13/3.47  (p26 zenon_Vysa)
% 3.13/3.47  (-. (p39 zenon_Vmba))
% 3.13/3.47  (p33 zenon_Vika)
% 3.13/3.47  (r1 zenon_Vw zenon_Vx)
% 3.13/3.47  (p46 zenon_Vip)
% 3.13/3.47  (p19 zenon_Vrza)
% 3.13/3.47  (r1 zenon_Vaeb zenon_Voeb)
% 3.13/3.47  (-. (p25 zenon_Vysa))
% 3.13/3.47  (-. (p10 zenon_Vpfb))
% 3.13/3.47  (r1 zenon_Vvjb zenon_Vwjb)
% 3.13/3.47  (p30 zenon_Vgoa)
% 3.13/3.47  (r1 zenon_Vvhb zenon_Vaib)
% 3.13/3.47  (p17 zenon_Vgbb)
% 3.13/3.47  (-. (p37 zenon_Vpea))
% 3.13/3.47  (zenon_Vtu != zenon_Vuu)
% 3.13/3.47  (-. (p9 zenon_Vbgb))
% 3.13/3.47  (zenon_Vagb != zenon_Vbgb)
% 3.13/3.47  (zenon_Voj != zenon_Voh)
% 3.13/3.47  (r1 zenon_Voib zenon_Vpib)
% 3.13/3.47  (-. (p16 zenon_Vacb))
% 3.13/3.47  (r1 zenon_Vqib zenon_Vrib)
% 3.13/3.47  (r1 zenon_Vja zenon_Vka)
% 3.13/3.47  (-. (p48 zenon_Voj))
% 3.13/3.47  (-. (p45 zenon_Vfr))
% 3.13/3.47  (p43 zenon_Vtu)
% 3.13/3.47  (r1 zenon_Vdjb zenon_Vejb)
% 3.13/3.47  (zenon_Vzhb != zenon_Vthb)
% 3.13/3.47  (zenon_Vzbb != zenon_Vacb)
% 3.13/3.47  (r1 zenon_Vtza zenon_Vnab)
% 3.13/3.47  (r1 zenon_Vt zenon_Vu)
% 3.13/3.47  (r1 zenon_Vra zenon_Vsa)
% 3.13/3.47  (zenon_Vnha != zenon_Vbga)
% 3.13/3.47  (r1 zenon_Vuib zenon_Vvib)
% 3.13/3.47  (zenon_Vthb != zenon_Vmhb)
% 3.13/3.47  (-. (p3 zenon_Vthb))
% 3.13/3.47  (p36 zenon_Vbga)
% 3.13/3.47  (-. (p10 zenon_Vbfb))
% 3.13/3.47  (r1 zenon_Vsib zenon_Vtib)
% 3.13/3.47  (zenon_Vzs != zenon_Ver)
% 3.13/3.47  (r1 zenon_Vu zenon_Vv)
% 3.13/3.47  (p10 zenon_Vofb)
% 3.13/3.47  (p22 zenon_Vaxa)
% 3.13/3.47  (r1 zenon_Vqfb zenon_Vbgb)
% 3.13/3.47  (zenon_Vmhb != zenon_Vehb)
% 3.13/3.47  (-. (p1 zenon_Veib))
% 3.13/3.47  (zenon_Vbga != zenon_Voea)
% 3.13/3.47  (-. (p21 zenon_Vaxa))
% 3.13/3.47  (r1 zenon_Vgb zenon_Vhb)
% 3.13/3.47  (r1 zenon_Vow zenon_Vfy)
% 3.13/3.47  (zenon_Vzbb != zenon_Vgbb)
% 3.13/3.47  (-. (p22 zenon_Vbxa))
% 3.13/3.47  (r1 zenon_Vn zenon_Vo)
% 3.13/3.47  (r1 zenon_Vxib zenon_Vyib)
% 3.13/3.47  (p9 zenon_Vagb)
% 3.13/3.47  (r1 zenon_Vxa zenon_Vya)
% 3.13/3.47  (-. (p47 zenon_Vmn))
% 3.13/3.47  (p42 zenon_Vmw)
% 3.13/3.47  (zenon_Vvgb != zenon_Vlgb)
% 3.13/3.47  (r1 zenon_Vpa zenon_Vqa)
% 3.13/3.47  (r1 zenon_Vyib zenon_Vzib)
% 3.13/3.47  (r1 zenon_Vakb zenon_Vbkb)
% 3.13/3.47  (zenon_Vtu != zenon_Vzs)
% 3.13/3.47  (zenon_Vika != zenon_Vyia)
% 3.13/3.47  (r1 zenon_Vla zenon_Vma)
% 3.13/3.47  (zenon_Voea != zenon_Vada)
% 3.13/3.47  (r1 zenon_Vaja zenon_Vjka)
% 3.13/3.47  (-. (p48 zenon_Vol))
% 3.13/3.47  (r1 zenon_Vo zenon_Vp)
% 3.13/3.47  (-. (p9 zenon_Vofb))
% 3.13/3.47  (zenon_Vgoa != zenon_Vzma)
% 3.13/3.47  (-. (p32 zenon_Vika))
% 3.13/3.47  (p5 zenon_Vmhb)
% 3.13/3.47  (-. (p18 zenon_Vnab))
% 3.13/3.47  (zenon_Vlgb != zenon_Vmgb)
% 3.13/3.47  (p3 zenon_Vzhb)
% 3.13/3.47  (-. (p5 zenon_Vnhb))
% 3.13/3.47  (p44 zenon_Vzs)
% 3.13/3.47  (r1 zenon_Vbna zenon_Vhoa)
% 3.13/3.47  (-. (p33 zenon_Vyia))
% 3.13/3.47  (zenon_Vvya != zenon_Vyxa)
% 3.13/3.47  (r1 zenon_Vata zenon_Vbua)
% 3.13/3.47  (zenon_Vbfb != zenon_Vneb)
% 3.13/3.47  (-. (p8 zenon_Vagb))
% 3.13/3.47  (r1 zenon_Vfjb zenon_Vgjb)
% 3.13/3.47  (zenon_Vzs != zenon_Vat)
% 3.13/3.47  (-. (p26 zenon_Vvra))
% 3.13/3.47  (r1 zenon_Vvu zenon_Vnw)
% 3.13/3.47  (r1 Tau_3 zenon_Vfib)
% 3.13/3.47  (r1 zenon_Vbkb zenon_Vckb)
% 3.13/3.47  (-. (p24 zenon_Vcva))
% 3.13/3.47  (-. (p21 zenon_Vzxa))
% 3.13/3.47  (-. (p23 zenon_Vcwa))
% 3.13/3.47  (zenon_Vmpa != zenon_Vgoa)
% 3.13/3.47  (r1 zenon_Vjjb zenon_Vkjb)
% 3.13/3.47  (r1 zenon_Vab zenon_Vbb)
% 3.13/3.47  (r1 zenon_Vfib zenon_Vgib)
% 3.13/3.47  (r1 zenon_Vhjb zenon_Vijb)
% 3.13/3.47  (-. (p22 zenon_Vbwa))
% 3.13/3.47  (r1 zenon_Vua zenon_Vva)
% 3.13/3.47  (r1 zenon_Vejb zenon_Vfjb)
% 3.13/3.47  (zenon_Vada != zenon_Vlba)
% 3.13/3.47  (r1 zenon_Vp zenon_Vq)
% 3.13/3.47  (zenon_Vthb != zenon_Vuhb)
% 3.13/3.47  (r1 zenon_Vojb zenon_Vpjb)
% 3.13/3.47  (p18 zenon_Vmab)
% 3.13/3.47  (zenon_Vnf != zenon_Vof)
% 3.13/3.47  (r1 zenon_Vva zenon_Vwa)
% 3.13/3.47  (r1 zenon_Vaa zenon_Vba)
% 3.13/3.47  (p27 zenon_Vvra)
% 3.13/3.47  (r1 zenon_Vqh zenon_Vpj)
% 3.13/3.47  (zenon_Vnf != zenon_Vld)
% 3.13/3.47  (p20 zenon_Vvya)
% 3.13/3.47  (zenon_Vaxa != zenon_Vbxa)
% 3.13/3.47  (zenon_Vyia != zenon_Vzia)
% 3.13/3.47  (zenon_Vehb != zenon_Vvgb)
% 3.13/3.47  (zenon_Vvz != zenon_Vwz)
% 3.13/3.47  (p24 zenon_Vbva)
% 3.13/3.47  (p50 zenon_Voh)
% 3.13/3.47  (r1 zenon_Vcgb zenon_Vmgb)
% 3.13/3.47  (-. (p14 zenon_Vjdb))
% 3.13/3.47  (zenon_Vysa != zenon_Vvra)
% 3.13/3.47  (zenon_Vlgb != zenon_Vagb)
% 3.13/3.47  (p14 zenon_Vidb)
% 3.13/3.47  (zenon_Vln != zenon_Vnl)
% 3.13/3.47  (-. (p36 zenon_Voea))
% 3.13/3.47  (r1 zenon_Vzib zenon_Vajb)
% 3.13/3.47  (r1 zenon_Vdb zenon_Veb)
% 3.13/3.47  (r1 zenon_Vbt zenon_Vuu)
% 3.13/3.47  (-. (p31 zenon_Vana))
% 3.13/3.47  (r1 zenon_Vioa zenon_Vnpa)
% 3.13/3.47  (p32 zenon_Vrla)
% 3.13/3.47  (zenon_Vyxa != zenon_Vzxa)
% 3.13/3.47  (-. (p38 zenon_Vbda))
% 3.13/3.47  (r1 zenon_Vnba zenon_Vbda)
% 3.13/3.47  (p6 zenon_Vehb)
% 3.13/3.47  (r1 zenon_Vpjb zenon_Vqjb)
% 3.13/3.47  (zenon_Vrza != zenon_Vvya)
% 3.13/3.47  (zenon_Vidb != zenon_Vrcb)
% 3.13/3.47  (zenon_Vip != zenon_Vln)
% 3.13/3.47  (p39 zenon_Vlba)
% 3.13/3.47  (zenon_Vey != zenon_Vmw)
% 3.13/3.47  (r1 zenon_Vkka zenon_Vsla)
% 3.13/3.47  (zenon_Vld != zenon_Vdkb)
% 3.13/3.47  (r1 zenon_Vbcb zenon_Vscb)
% 3.13/3.47  (-. (p41 zenon_Vmw))
% 3.13/3.47  (r1 zenon_Vngb zenon_Vwgb)
% 3.13/3.47  (zenon_Vmpa != zenon_Vnpa)
% 3.13/3.47  (r1 zenon_Vnjb zenon_Vojb)
% 3.13/3.47  (r1 zenon_Vwjb zenon_Vxjb)
% 3.13/3.47  (-. (p46 zenon_Vln))
% 3.13/3.47  (p13 zenon_Vydb)
% 3.13/3.47  (r1 zenon_Voab zenon_Vhbb)
% 3.13/3.47  (r1 zenon_Vnd zenon_Vof)
% 3.13/3.47  (-. (p39 zenon_Vvz))
% 3.13/3.47  (zenon_Vrla != zenon_Vika)
% 3.13/3.47  (r1 zenon_Vcb zenon_Vdb)
% 3.13/3.47  (r1 zenon_Vy zenon_Vz)
% 3.13/3.47  (zenon_Vmw != zenon_Vnw)
% 3.13/3.47  (-. (p19 zenon_Vsza))
% 3.13/3.47  (-. (p47 zenon_Vnl))
% 3.13/3.47  (-. (p6 zenon_Vvgb))
% 3.13/3.47  (r1 zenon_Vca zenon_Vda)
% 3.13/3.47  (-. (p15 zenon_Vzbb))
% 3.13/3.47  (r1 zenon_Vba zenon_Vca)
% 3.13/3.47  (r1 zenon_Vtla zenon_Vana)
% 3.13/3.47  (-. (p36 zenon_Vcga))
% 3.13/3.47  (r1 zenon_Vkjb zenon_Vljb)
% 3.13/3.47  (r1 zenon_Vpha zenon_Vzia)
% 3.13/3.47  (r1 zenon_Vjib zenon_Vkib)
% 3.13/3.47  (-. (p34 zenon_Vzia))
% 3.13/3.47  (-. (p17 zenon_Vhbb))
% 3.13/3.47  (r1 zenon_Vijb zenon_Vjjb)
% 3.13/3.47  (zenon_Vmw != zenon_Vtu)
% 3.13/3.47  (r1 zenon_Vkib zenon_Vlib)
% 3.13/3.47  (-. (p27 zenon_Vwra))
% 3.13/3.47  (r1 zenon_Vza zenon_Vab)
% 3.13/3.47  (p8 zenon_Vlgb)
% 3.13/3.47  (-. (p32 zenon_Vsla))
% 3.13/3.47  (zenon_Vzma != zenon_Vrla)
% 3.13/3.47  (r1 zenon_Vsjb zenon_Vtjb)
% 3.13/3.47  (r1 zenon_Vljb zenon_Vmjb)
% 3.13/3.47  (r1 zenon_Vrjb zenon_Vsjb)
% 3.13/3.47  (r1 zenon_Vxra zenon_Vzsa)
% 3.13/3.47  (-. (p33 zenon_Vjka))
% 3.13/3.47  (zenon_Vvra != zenon_Vrqa)
% 3.13/3.47  (r1 zenon_Vckb zenon_Vdkb)
% 3.13/3.47  (r1 zenon_Vdwa zenon_Vbxa)
% 3.13/3.47  (-. (p34 zenon_Vnha))
% 3.13/3.47  (r1 zenon_Vpeb zenon_Vcfb)
% 3.13/3.47  (-. (p11 zenon_Vcfb))
% 3.13/3.47  (zenon_Vld != zenon_Veib)
% 3.13/3.47  (r1 zenon_Via zenon_Vja)
% 3.13/3.47  (-. (p51 zenon_Vld))
% 3.13/3.47  (zenon_Vzma != zenon_Vana)
% 3.13/3.47  (p16 zenon_Vzbb)
% 3.13/3.47  (r1 zenon_Vpib zenon_Vqib)
% 3.13/3.47  (p40 zenon_Vvz)
% 3.13/3.47  (r1 zenon_Vaya zenon_Vwya)
% 3.13/3.47  (r1 zenon_Vqjb zenon_Vrjb)
% 3.13/3.47  (zenon_Vbga != zenon_Vcga)
% 3.13/3.47  (-. (p18 zenon_Vrza))
% 3.13/3.47  (zenon_Vbwa != zenon_Vbva)
% 3.13/3.47  (-. (p16 zenon_Vgbb))
% 3.13/3.47  (r1 zenon_Veb zenon_Vfb)
% 3.13/3.47  (-. (p2 zenon_Vzhb))
% 3.13/3.47  (zenon_Vvz != zenon_Vey)
% 3.13/3.47  (p29 zenon_Vmpa)
% 3.13/3.47  (r1 zenon_Vxgb zenon_Vfhb)
% 3.13/3.47  (zenon_Voea != zenon_Vpea)
% 3.13/3.47  (-. (p13 zenon_Vzdb))
% 3.13/3.47  (r1 zenon_Vqj zenon_Vol)
% 3.13/3.47  (zenon_Vehb != zenon_Vfhb)
% 3.13/3.47  (p41 zenon_Vey)
% 3.13/3.47  (-. (p26 zenon_Vzsa))
% 3.13/3.47  (r1 zenon_Vtib zenon_Vuib)
% 3.13/3.47  (-. (p28 zenon_Vsqa))
% 3.13/3.47  (r1 zenon_Vcua zenon_Vcva)
% 3.13/3.47  (zenon_Voh != zenon_Vnf)
% 3.13/3.47  (r1 zenon_Vda zenon_Vea)
% 3.13/3.47  (zenon_Veib != zenon_Vzhb)
% 3.13/3.47  (-. (p41 zenon_Vfy))
% 3.13/3.47  (zenon_Vmhb != zenon_Vnhb)
% 3.13/3.47  (r1 zenon_Vgjb zenon_Vhjb)
% 3.13/3.47  (r1 zenon_Vv zenon_Vw)
% 3.13/3.47  (r1 zenon_Vgr zenon_Vat)
% 3.13/3.47  (r1 zenon_Vya zenon_Vza)
% 3.13/3.47  (r1 zenon_Vga zenon_Vha)
% 3.13/3.47  (zenon_Vaua != zenon_Vbua)
% 3.13/3.47  (zenon_Vydb != zenon_Vidb)
% 3.13/3.47  (zenon_Vmab != zenon_Vrza)
% 3.13/3.47  (zenon_Vneb != zenon_Voeb)
% 3.13/3.47  (r1 zenon_Vqa zenon_Vra)
% 3.13/3.47  (-. (p7 zenon_Vlgb))
% 3.13/3.47  (r1 zenon_Vgy zenon_Vwz)
% 3.13/3.47  (zenon_Vneb != zenon_Vydb)
% 3.13/3.47  (r1 zenon_Vqea zenon_Vcga)
% 3.13/3.47  (r1 zenon_X4 zenon_Vmd)
% 3.13/3.47  (zenon_Vofb != zenon_Vpfb)
% 3.13/3.47  (zenon_Vada != zenon_Vbda)
% 3.13/3.47  (-. (p7 zenon_Vwgb))
% 3.13/3.47  (r1 Tau_0 Tau_2)
% 3.13/3.47  *)
% 3.13/3.47  (* NO-PROOF *)
% 3.13/3.47  % SZS status GaveUp
% 3.13/3.47  Number of rewrites on terms: 0
% 3.13/3.47  Number of rewrites on props: 0
% 3.13/3.47  nodes searched: 3786
% 3.13/3.47  max branch formulas: 4095
% 3.13/3.47  proof nodes created: 0
% 3.13/3.47  formulas created: 20109
% 3.13/3.47  
%------------------------------------------------------------------------------