↑ Up

ZenonModulo---0.5.0.UNK-Non.f

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

% Computer : n018.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:19 PM UTC 2026

% Result   : Unknown 1.25s 1.55s
% Output   : None 
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05  % Problem  : LCL660+1.015 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05  % Command  : run_zenon_modulo %d %s
% 0.17/0.42  % Computer : n018.cluster.edu
% 0.17/0.42  % Model    : x86_64 x86_64
% 0.17/0.42  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.42  % Memory   : 8046.5625MB
% 0.17/0.42  % OS       : Linux 6.8.0-71-generic
% 0.17/0.42  % CPULimit : 300
% 0.17/0.42  % WCLimit  : 300
% 0.17/0.42  % DateTime : Fri Sep  4 19:28:18 UTC 2026
% 0.17/0.42  % CPUTime  : 
% 1.25/1.54  Zenon error: exhausted search space without finding a proof
% 1.25/1.54  (* Current branch:
% 1.25/1.54  (-. (p1 Tau_16))
% 1.25/1.54  (r1 zenon_Vjb zenon_Vkb)
% 1.25/1.54  (-. (p2 zenon_Vof))
% 1.25/1.54  (-. (p3 zenon_Vtb))
% 1.25/1.54  (-. (p2 zenon_Vrb))
% 1.25/1.54  (zenon_Vo != zenon_Vic)
% 1.25/1.54  (r1 zenon_Vyb zenon_Vzb)
% 1.25/1.54  (-. (p1 Tau_17))
% 1.25/1.54  (-. (p3 Tau_16))
% 1.25/1.54  (r1 zenon_Vwd zenon_Vxd)
% 1.25/1.54  (r1 zenon_Vwc zenon_Vxc)
% 1.25/1.54  (-. (p4 zenon_Vpe))
% 1.25/1.54  (-. (p3 zenon_Vbd))
% 1.25/1.54  (zenon_Vt != zenon_Vbe)
% 1.25/1.54  (-. (p2 zenon_Vib))
% 1.25/1.54  (zenon_Vt != zenon_Vhg)
% 1.25/1.54  (zenon_Vr != zenon_Vce)
% 1.25/1.54  (-. (p1 zenon_Vwc))
% 1.25/1.54  (r1 Tau_14 zenon_Vof)
% 1.25/1.54  (r1 zenon_Vtb zenon_Vub)
% 1.25/1.54  (zenon_Vr != zenon_Vod)
% 1.25/1.54  (zenon_Vm != zenon_Vod)
% 1.25/1.54  (-. (p3 Tau_7))
% 1.25/1.54  (-. (p1 zenon_Vlb))
% 1.25/1.54  (r1 zenon_Vsb zenon_Vtb)
% 1.25/1.54  (zenon_Vm != zenon_Vce)
% 1.25/1.54  (-. (p2 zenon_Vcg))
% 1.25/1.54  (-. (p1 Tau_18))
% 1.25/1.54  (r1 zenon_Vt zenon_Vu)
% 1.25/1.54  (zenon_Vt != zenon_Vhf)
% 1.25/1.54  (-. (p1 Tau_10))
% 1.25/1.54  (zenon_Vo != zenon_Vcf)
% 1.25/1.54  (zenon_Vt != zenon_Vu)
% 1.25/1.54  (zenon_Vo != zenon_Vpe)
% 1.25/1.54  (zenon_Vm != zenon_Vpc)
% 1.25/1.54  (zenon_Vr != zenon_Vrg)
% 1.25/1.54  (zenon_Vm != zenon_Vn)
% 1.25/1.54  (zenon_Vo != zenon_Vwc)
% 1.25/1.54  (-. (p1 zenon_Vxf))
% 1.25/1.54  (zenon_Vm != zenon_Vuf)
% 1.25/1.54  (zenon_Vt != zenon_Vbd)
% 1.25/1.54  (-. (p1 zenon_Vkc))
% 1.25/1.54  (p1 zenon_Vt)
% 1.25/1.54  (zenon_Vt != zenon_Vtb)
% 1.25/1.54  (r1 Tau_5 zenon_Vhb)
% 1.25/1.54  (r1 Tau_0 Tau_14)
% 1.25/1.54  (r1 Tau_9 zenon_Vod)
% 1.25/1.54  (zenon_Vt != zenon_Vlf)
% 1.25/1.54  (-. (p1 Tau_8))
% 1.25/1.54  (zenon_Vr != zenon_Vka)
% 1.25/1.54  (-. (p1 zenon_Vxd))
% 1.25/1.54  (-. (p3 zenon_Ved))
% 1.25/1.54  (zenon_Vr != Tau_12)
% 1.25/1.54  (zenon_Vm != Tau_12)
% 1.25/1.54  (zenon_Vo != Tau_12)
% 1.25/1.54  (zenon_Vt != Tau_12)
% 1.25/1.54  (zenon_Vr != zenon_Vje)
% 1.25/1.54  (-. (p1 zenon_Vyb))
% 1.25/1.54  (-. (p1 zenon_Vof))
% 1.25/1.54  (-. (p3 zenon_Vlf))
% 1.25/1.54  (-. (p3 Tau_1))
% 1.25/1.54  (-. (p1 zenon_Vmg))
% 1.25/1.54  (-. (p3 zenon_Vhb))
% 1.25/1.54  (zenon_Vm != zenon_Vke)
% 1.25/1.54  (-. (p1 zenon_Vte))
% 1.25/1.54  (-. (p4 zenon_Vxf))
% 1.25/1.54  (r1 zenon_Vxf zenon_Vag)
% 1.25/1.54  (r1 zenon_Vhb zenon_Vib)
% 1.25/1.54  (-. (p1 zenon_Vhf))
% 1.25/1.54  (-. (p3 zenon_Vne))
% 1.25/1.54  (-. (p1 zenon_Vpe))
% 1.25/1.54  (-. (p3 zenon_Vbe))
% 1.25/1.54  (r1 Tau_0 Tau_3)
% 1.25/1.54  (zenon_Vo != zenon_Vbd)
% 1.25/1.54  (zenon_Vo != zenon_Vrb)
% 1.25/1.54  (zenon_Vr != zenon_Vn)
% 1.25/1.54  (zenon_Vo != zenon_Vkc)
% 1.25/1.54  (-. (p1 zenon_Ved))
% 1.25/1.54  (zenon_Vr != zenon_Vqg)
% 1.25/1.54  (-. (p1 zenon_Vtb))
% 1.25/1.54  (-. (p3 zenon_Vcg))
% 1.25/1.54  (-. (p2 Tau_7))
% 1.25/1.54  (-. (p3 zenon_Vcf))
% 1.25/1.54  (zenon_Vm != zenon_Vrb)
% 1.25/1.54  (zenon_Vo != zenon_Vp)
% 1.25/1.54  (-. (p4 zenon_Vod))
% 1.25/1.54  (-. (p2 zenon_Vn))
% 1.25/1.54  (r1 Tau_0 Tau_15)
% 1.25/1.54  (-. (p3 zenon_Vke))
% 1.25/1.54  (zenon_Vm != zenon_Vwe)
% 1.25/1.54  (-. (p1 zenon_Vzb))
% 1.25/1.54  (-. (p3 zenon_Vce))
% 1.25/1.54  (r1 Tau_13 zenon_Vff)
% 1.25/1.54  (-. (p1 zenon_Vxc))
% 1.25/1.54  (-. (p1 zenon_Vpd))
% 1.25/1.54  (r1 zenon_Vlf zenon_Vmf)
% 1.25/1.54  (zenon_Vr != zenon_Vof)
% 1.25/1.54  (-. (p3 zenon_Vte))
% 1.25/1.54  (zenon_Vr != zenon_Vtb)
% 1.25/1.54  (zenon_Vo != zenon_Vjd)
% 1.25/1.54  (-. (p2 zenon_Vye))
% 1.25/1.54  (-. (p2 zenon_Vte))
% 1.25/1.54  (r1 zenon_Vrb zenon_Vsb)
% 1.25/1.54  (zenon_Vm != zenon_Vjb)
% 1.25/1.54  (-. (p2 Tau_5))
% 1.25/1.54  (-. (p1 zenon_Vjd))
% 1.25/1.54  (zenon_Vt != Tau_2)
% 1.25/1.54  (zenon_Vt != Tau_6)
% 1.25/1.54  (-. (p2 zenon_Vje))
% 1.25/1.54  (zenon_Vr != zenon_Vjb)
% 1.25/1.54  (zenon_Vr != zenon_Vsb)
% 1.25/1.54  (-. (p1 zenon_Vne))
% 1.25/1.54  (-. (p3 zenon_Vrb))
% 1.25/1.54  (-. (p4 zenon_Vbd))
% 1.25/1.54  (-. (p1 Tau_13))
% 1.25/1.54  (zenon_Vt != zenon_Vwe)
% 1.25/1.54  (r1 zenon_Vo zenon_Vp)
% 1.25/1.54  (zenon_Vr != zenon_Vrc)
% 1.25/1.54  (zenon_Vo != zenon_Vyb)
% 1.25/1.54  (zenon_Vt != zenon_Ved)
% 1.25/1.54  (-. (p1 zenon_Vcf))
% 1.25/1.54  (zenon_Vr != zenon_Vlb)
% 1.25/1.54  (zenon_Vt != zenon_Vkc)
% 1.25/1.54  (-. (p1 zenon_Vhb))
% 1.25/1.54  (zenon_Vr != zenon_Vxc)
% 1.25/1.54  (-. (p1 Tau_7))
% 1.25/1.54  (r1 Tau_0 Tau_9)
% 1.25/1.54  (r1 zenon_Vte zenon_Vue)
% 1.25/1.54  (-. (p2 zenon_Vhb))
% 1.25/1.54  (-. (p4 zenon_Vne))
% 1.25/1.54  (-. (p3 zenon_Vjd))
% 1.25/1.54  (-. (p3 zenon_Vac))
% 1.25/1.54  (zenon_Vo != zenon_Vcd)
% 1.25/1.54  (r1 zenon_Vac zenon_Vbc)
% 1.25/1.54  (-. (p3 zenon_Vye))
% 1.25/1.54  (zenon_Vm != zenon_Vtb)
% 1.25/1.54  (zenon_Vm != zenon_Vxc)
% 1.25/1.54  (-. (p3 zenon_Vkd))
% 1.25/1.54  (-. (p3 zenon_Vpe))
% 1.25/1.54  (zenon_Vr != Tau_3)
% 1.25/1.54  (zenon_Vm != Tau_3)
% 1.25/1.54  (-. (p3 zenon_Vic))
% 1.25/1.54  (zenon_Vr != zenon_Vcd)
% 1.25/1.54  (-. (p2 Tau_9))
% 1.25/1.54  (-. (p4 zenon_Vpc))
% 1.25/1.54  (zenon_Vo != zenon_Vje)
% 1.25/1.54  (zenon_Vr != Tau_9)
% 1.25/1.54  (zenon_Vm != Tau_9)
% 1.25/1.54  (zenon_Vt != Tau_9)
% 1.25/1.54  (r1 zenon_Voc zenon_Vpc)
% 1.25/1.54  (-. (p3 zenon_Vpc))
% 1.25/1.54  (-. (p2 Tau_13))
% 1.25/1.54  (-. (p4 zenon_Vkc))
% 1.25/1.54  (zenon_Vm != zenon_Vxf)
% 1.25/1.54  (zenon_Vm != zenon_Vrd)
% 1.25/1.54  (-. (p4 zenon_Vrb))
% 1.25/1.54  (-. (p3 zenon_Vib))
% 1.25/1.54  (-. (p4 Tau_7))
% 1.25/1.54  (-. (p3 zenon_Vuf))
% 1.25/1.54  (zenon_Vm != zenon_Vsb)
% 1.25/1.54  (r1 zenon_Vee zenon_Vje)
% 1.25/1.54  (-. (p1 Tau_12))
% 1.25/1.54  (zenon_Vo != zenon_Vne)
% 1.25/1.54  (-. (p2 Tau_11))
% 1.25/1.54  (r1 zenon_Vcg zenon_Vfg)
% 1.25/1.54  (r1 zenon_Vrd zenon_Vwd)
% 1.25/1.54  (r1 Tau_0 Tau_5)
% 1.25/1.54  (zenon_Vr != zenon_Vkc)
% 1.25/1.54  (zenon_Vr != zenon_Vhb)
% 1.25/1.54  (zenon_Vm != zenon_Vkc)
% 1.25/1.54  (zenon_Vt != zenon_Vhb)
% 1.25/1.54  (-. (p2 Tau_3))
% 1.25/1.54  (r1 Tau_0 Tau_8)
% 1.25/1.54  (-. (p4 Tau_11))
% 1.25/1.54  (-. (p3 Tau_12))
% 1.25/1.54  (-. (p2 zenon_Vka))
% 1.25/1.54  (-. (p1 zenon_Vcg))
% 1.25/1.54  (-. (p1 zenon_Vac))
% 1.25/1.54  (zenon_Vr != zenon_Vhf)
% 1.25/1.54  (zenon_Vt != zenon_Vsb)
% 1.25/1.54  (-. (p4 zenon_Vsb))
% 1.25/1.54  (-. (p1 zenon_Vcd))
% 1.25/1.54  (-. (p2 zenon_Vtb))
% 1.25/1.54  (-. (p4 zenon_Vce))
% 1.25/1.54  (zenon_Vm != zenon_Vrc)
% 1.25/1.54  (zenon_Vm != zenon_Vac)
% 1.25/1.54  (r1 Tau_6 zenon_Vyb)
% 1.25/1.54  (zenon_Vr != zenon_Vcf)
% 1.25/1.54  (zenon_Vm != zenon_Vcf)
% 1.25/1.54  (-. (p4 zenon_Vjd))
% 1.25/1.54  (-. (p1 zenon_Vuf))
% 1.25/1.54  (zenon_Vt != zenon_Vff)
% 1.25/1.54  (r1 zenon_Vff zenon_Vgf)
% 1.25/1.54  (zenon_Vo != zenon_Vcg)
% 1.25/1.54  (zenon_Vo != zenon_Ved)
% 1.25/1.54  (-. (p1 Tau_5))
% 1.25/1.54  (r1 zenon_Vzb zenon_Vac)
% 1.25/1.54  (zenon_Vr != zenon_Vpe)
% 1.25/1.54  (zenon_Vr != Tau_5)
% 1.25/1.54  (zenon_Vm != Tau_5)
% 1.25/1.54  (zenon_Vt != Tau_5)
% 1.25/1.54  (zenon_Vt != zenon_Vjb)
% 1.25/1.54  (r1 zenon_X23 zenon_Vqg)
% 1.25/1.54  (-. (p2 zenon_Vbd))
% 1.25/1.54  (r1 Tau_10 zenon_Vbe)
% 1.25/1.54  (zenon_Vr != zenon_Vwe)
% 1.25/1.54  (-. (p1 zenon_Vqf))
% 1.25/1.54  (-. (p2 zenon_Vcd))
% 1.25/1.54  (-. (p3 zenon_Vff))
% 1.25/1.54  (-. (p4 zenon_Vjb))
% 1.25/1.54  (-. (p1 zenon_Vrd))
% 1.25/1.54  (-. (p2 zenon_Vcb))
% 1.25/1.54  (zenon_Vt != zenon_Vxd)
% 1.25/1.54  (zenon_Vm != zenon_Vhf)
% 1.25/1.54  (zenon_Vt != zenon_Vcf)
% 1.25/1.54  (-. (p1 zenon_Vu))
% 1.25/1.54  (zenon_Vo != zenon_Vce)
% 1.25/1.54  (zenon_Vt != zenon_Vod)
% 1.25/1.54  (zenon_Vr != Tau_4)
% 1.25/1.54  (zenon_Vm != Tau_4)
% 1.25/1.54  (-. (p3 zenon_Vpd))
% 1.25/1.54  (zenon_Vt != zenon_Vwd)
% 1.25/1.54  (-. (p1 zenon_Vib))
% 1.25/1.54  (zenon_Vm != zenon_Vlf)
% 1.25/1.54  (-. (p2 Tau_17))
% 1.25/1.54  (-. (p3 zenon_Voc))
% 1.25/1.54  (zenon_Vm != zenon_Vhb)
% 1.25/1.54  (r1 Tau_7 zenon_Voc)
% 1.25/1.54  (-. (p3 Tau_11))
% 1.25/1.54  (-. (p4 zenon_Vkd))
% 1.25/1.54  (zenon_Vt != zenon_Vlb)
% 1.25/1.54  (-. (p2 zenon_Voc))
% 1.25/1.54  (zenon_Vr != Tau_8)
% 1.25/1.54  (zenon_Vm != Tau_8)
% 1.25/1.54  (zenon_Vo != Tau_8)
% 1.25/1.54  (zenon_Vt != Tau_8)
% 1.25/1.54  (r1 zenon_Vye zenon_Vcf)
% 1.25/1.54  (-. (p1 Tau_6))
% 1.25/1.54  (zenon_Vr != Tau_7)
% 1.25/1.54  (zenon_Vm != Tau_7)
% 1.25/1.54  (zenon_Vo != Tau_7)
% 1.25/1.54  (zenon_Vt != Tau_7)
% 1.25/1.54  (r1 Tau_0 Tau_6)
% 1.25/1.54  (zenon_Vr != zenon_Via)
% 1.25/1.54  (zenon_Vo != zenon_Vod)
% 1.25/1.54  (zenon_Vm != zenon_Vff)
% 1.25/1.54  (-. (p2 zenon_Vwc))
% 1.25/1.54  (-. (p3 zenon_Vxd))
% 1.25/1.54  (r1 zenon_Vcc zenon_Vic)
% 1.25/1.54  (-. (p3 zenon_Vwd))
% 1.25/1.54  (-. (p3 zenon_Vyb))
% 1.25/1.54  (-. (p2 zenon_Vsb))
% 1.25/1.54  (r1 Tau_17 zenon_Vgg)
% 1.25/1.54  (r1 zenon_Vke zenon_Vle)
% 1.25/1.54  (zenon_Vr != zenon_Vuf)
% 1.25/1.54  (r1 Tau_0 Tau_18)
% 1.25/1.54  (-. (p2 zenon_Vcf))
% 1.25/1.54  (r1 zenon_X19 zenon_Vr)
% 1.25/1.54  (zenon_Vm != zenon_Vhg)
% 1.25/1.54  (zenon_Vt != zenon_Vrd)
% 1.25/1.54  (zenon_Vo != zenon_Vye)
% 1.25/1.54  (-. (p1 Tau_14))
% 1.25/1.54  (-. (p1 zenon_Vee))
% 1.25/1.54  (zenon_Vt != zenon_Voc)
% 1.25/1.54  (zenon_Vr != zenon_Vib)
% 1.25/1.54  (zenon_Vr != zenon_Vbd)
% 1.25/1.54  (zenon_Vo != zenon_Vtb)
% 1.25/1.54  (zenon_Vr != zenon_Vbe)
% 1.25/1.54  (-. (p3 zenon_Vwc))
% 1.25/1.54  (zenon_Vm != zenon_Vrg)
% 1.25/1.54  (zenon_Vo != zenon_Vff)
% 1.25/1.54  (zenon_Vr != zenon_Vs)
% 1.25/1.54  (-. (p4 zenon_Vcd))
% 1.25/1.54  (r1 zenon_Vof zenon_Vpf)
% 1.25/1.54  (zenon_Vt != zenon_Vwc)
% 1.25/1.54  (-. (p4 zenon_Vlf))
% 1.25/1.54  (p2 zenon_Vm)
% 1.25/1.54  (zenon_Vt != zenon_Vce)
% 1.25/1.54  (zenon_Vt != zenon_Vpd)
% 1.25/1.54  (-. (p3 zenon_Vje))
% 1.25/1.54  (zenon_Vr != Tau_17)
% 1.25/1.54  (zenon_Vm != Tau_17)
% 1.25/1.54  (zenon_Vt != Tau_17)
% 1.25/1.54  (-. (p2 zenon_Vqg))
% 1.25/1.54  (zenon_Vm != zenon_Vlb)
% 1.25/1.54  (zenon_Vo != zenon_Vac)
% 1.25/1.54  (zenon_Vr != Tau_13)
% 1.25/1.54  (zenon_Vm != Tau_13)
% 1.25/1.54  (zenon_Vo != zenon_Vpc)
% 1.25/1.54  (zenon_Vt != Tau_13)
% 1.25/1.54  (zenon_Vt != zenon_Vmg)
% 1.25/1.54  (-. (p4 zenon_Vxc))
% 1.25/1.54  (-. (p3 zenon_Vod))
% 1.25/1.54  (-. (p2 zenon_Vpe))
% 1.25/1.54  (zenon_Vt != zenon_Vke)
% 1.25/1.54  (r1 zenon_Vhg zenon_Vkg)
% 1.25/1.54  (r1 Tau_0 Tau_10)
% 1.25/1.54  (r1 Tau_16 zenon_Vbg)
% 1.25/1.54  (zenon_Vt != zenon_Vxf)
% 1.25/1.54  (-. (p2 zenon_Vxc))
% 1.25/1.54  (zenon_Vm != zenon_Vjd)
% 1.25/1.54  (r1 Tau_11 zenon_Vne)
% 1.25/1.54  (-. (p1 zenon_Vjc))
% 1.25/1.54  (zenon_Vr != zenon_Vac)
% 1.25/1.54  (-. (p4 zenon_Vxd))
% 1.25/1.54  (zenon_Vt != zenon_Vte)
% 1.25/1.54  (-. (p3 zenon_Vof))
% 1.25/1.54  (-. (p4 zenon_Vke))
% 1.25/1.54  (-. (p4 zenon_Vzb))
% 1.25/1.54  (-. (p4 zenon_Voc))
% 1.25/1.54  (-. (p1 Tau_15))
% 1.25/1.54  (zenon_Vo != zenon_Vxc)
% 1.25/1.54  (r1 zenon_Vhf zenon_Vlf)
% 1.25/1.54  (-. (p3 zenon_Vp))
% 1.25/1.54  (zenon_Vt != zenon_Vof)
% 1.25/1.54  (-. (p1 zenon_Vye))
% 1.25/1.54  (-. (p4 zenon_Vcf))
% 1.25/1.54  (-. (p4 zenon_Vjc))
% 1.25/1.54  (zenon_Vm != zenon_Vye)
% 1.25/1.54  (r1 zenon_Vne zenon_Voe)
% 1.25/1.54  (r1 zenon_Vqf zenon_Vuf)
% 1.25/1.54  (-. (p1 zenon_Vke))
% 1.25/1.54  (-. (p1 zenon_Vpc))
% 1.25/1.54  (zenon_Vm != zenon_Voc)
% 1.25/1.54  (zenon_Vm != zenon_Vqg)
% 1.25/1.54  (zenon_Vo != zenon_Voc)
% 1.25/1.54  (zenon_Vt != zenon_Vqf)
% 1.25/1.54  (zenon_Vr != zenon_Vyb)
% 1.25/1.54  (zenon_Vm != zenon_Vje)
% 1.25/1.54  (zenon_Vo != zenon_Vwe)
% 1.25/1.54  (zenon_Vt != zenon_Vuf)
% 1.25/1.54  (-. (p2 zenon_Vkd))
% 1.25/1.54  (zenon_Vo != zenon_Vhb)
% 1.25/1.54  (r1 zenon_Vib zenon_Vjb)
% 1.25/1.54  (-. (p1 zenon_Vce))
% 1.25/1.54  (-. (p2 zenon_Vpd))
% 1.25/1.54  (-. (p2 zenon_Vwe))
% 1.25/1.54  (r1 Tau_0 Tau_2)
% 1.25/1.54  (-. (p4 zenon_Vuf))
% 1.25/1.54  (-. (p4 zenon_Vbe))
% 1.25/1.54  (r1 Tau_0 Tau_12)
% 1.25/1.54  (zenon_Vt != zenon_Vpe)
% 1.25/1.54  (-. (p4 zenon_Vte))
% 1.25/1.54  (zenon_Vo != zenon_Vlf)
% 1.25/1.54  (zenon_Vt != zenon_Vic)
% 1.25/1.54  (-. (p2 zenon_Vke))
% 1.25/1.54  (zenon_Vm != zenon_Via)
% 1.25/1.54  (-. (p3 zenon_Vjc))
% 1.25/1.54  (zenon_Vr != zenon_Vwc)
% 1.25/1.54  (zenon_Vt != zenon_Vpc)
% 1.25/1.54  (r1 zenon_Vpe zenon_Vte)
% 1.25/1.54  (zenon_Vr != zenon_Vxf)
% 1.25/1.54  (-. (p2 zenon_Vjb))
% 1.25/1.54  (-. (p1 zenon_Vwd))
% 1.25/1.54  (r1 zenon_Vcd zenon_Vdd)
% 1.25/1.54  (zenon_Vr != zenon_Vzb)
% 1.25/1.54  (r1 zenon_X22 zenon_Vt)
% 1.25/1.54  (zenon_Vm != zenon_Vpd)
% 1.25/1.54  (zenon_Vm != zenon_Vxd)
% 1.25/1.54  (-. (p1 zenon_Vhg))
% 1.25/1.54  (-. (p4 zenon_Vwc))
% 1.25/1.54  (r1 zenon_Vxd zenon_Vyd)
% 1.25/1.54  (zenon_Vt != zenon_Vrc)
% 1.25/1.54  (r1 zenon_Vjc zenon_Vkc)
% 1.25/1.54  (r1 zenon_Vpd zenon_Vqd)
% 1.25/1.54  (zenon_Vt != zenon_Vcg)
% 1.25/1.54  (-. (p2 zenon_Vkc))
% 1.25/1.54  (zenon_Vo != zenon_Vsb)
% 1.25/1.54  (zenon_Vo != zenon_Vbe)
% 1.25/1.54  (-. (p4 zenon_Vwe))
% 1.25/1.54  (-. (p1 zenon_Vwe))
% 1.25/1.54  (r1 Tau_0 Tau_11)
% 1.25/1.54  (r1 zenon_Vic zenon_Vjc)
% 1.25/1.54  (zenon_Vt != zenon_Vne)
% 1.25/1.54  (zenon_Vt != zenon_Vxc)
% 1.25/1.54  (zenon_Vm != zenon_Vte)
% 1.25/1.54  (r1 Tau_0 Tau_7)
% 1.25/1.54  (r1 zenon_Vwe zenon_Vxe)
% 1.25/1.54  (-. (p2 zenon_Via))
% 1.25/1.54  (r1 Tau_8 zenon_Vbd)
% 1.25/1.54  (zenon_Vm != zenon_Vzb)
% 1.25/1.54  (-. (p4 zenon_Vff))
% 1.25/1.54  (r1 zenon_Vce zenon_Vde)
% 1.25/1.54  (-. (p2 zenon_Vjc))
% 1.25/1.54  (-. (p2 zenon_Vpc))
% 1.25/1.54  (zenon_Vr != zenon_Vke)
% 1.25/1.54  (zenon_Vm != zenon_Vof)
% 1.25/1.54  (zenon_Vo != zenon_Vrc)
% 1.25/1.54  (-. (p4 zenon_Vyb))
% 1.25/1.54  (-. (p2 zenon_Vne))
% 1.25/1.54  (zenon_Vm != zenon_Vka)
% 1.25/1.54  (zenon_Vr != zenon_Vpd)
% 1.25/1.54  (zenon_Vo != zenon_Vxf)
% 1.25/1.54  (-. (p3 zenon_Vcd))
% 1.25/1.54  (zenon_Vr != zenon_Vjc)
% 1.25/1.54  (-. (p2 zenon_Vic))
% 1.25/1.54  (zenon_Vr != zenon_Vye)
% 1.25/1.54  (zenon_Vr != zenon_Vwd)
% 1.25/1.54  (zenon_Vt != zenon_Vrb)
% 1.25/1.54  (-. (p2 zenon_Vce))
% 1.25/1.54  (r1 Tau_0 Tau_13)
% 1.25/1.54  (-. (p4 zenon_Vhb))
% 1.25/1.54  (-. (p2 zenon_Vrd))
% 1.25/1.54  (zenon_Vm != zenon_Vic)
% 1.25/1.54  (-. (p2 zenon_Ved))
% 1.25/1.54  (-. (p3 zenon_Vwe))
% 1.25/1.54  (zenon_Vo != Tau_1)
% 1.25/1.54  (r1 zenon_Vje zenon_Vke)
% 1.25/1.54  (r1 zenon_Vr zenon_Vs)
% 1.25/1.54  (zenon_Vr != zenon_Vcg)
% 1.25/1.54  (-. (p1 zenon_Vic))
% 1.25/1.54  (zenon_Vt != zenon_Vyb)
% 1.25/1.54  (r1 zenon_Vkd zenon_Vld)
% 1.25/1.54  (-. (p2 zenon_Vlb))
% 1.25/1.54  (zenon_Vt != zenon_Vcd)
% 1.25/1.54  (-. (p1 Tau_2))
% 1.25/1.54  (zenon_Vr != zenon_Vjd)
% 1.25/1.54  (zenon_Vr != zenon_Vic)
% 1.25/1.54  (zenon_Vt != zenon_Vjc)
% 1.25/1.54  (-. (p1 zenon_Voc))
% 1.25/1.54  (-. (p2 Tau_15))
% 1.25/1.54  (-. (p4 zenon_Vof))
% 1.25/1.54  (zenon_Vr != zenon_Vhg)
% 1.25/1.54  (zenon_Vm != zenon_Vpe)
% 1.25/1.54  (zenon_Vr != zenon_Vlf)
% 1.25/1.54  (-. (p2 zenon_Vac))
% 1.25/1.54  (-. (p3 zenon_Vrc))
% 1.25/1.54  (-. (p1 zenon_Vff))
% 1.25/1.54  (-. (p3 zenon_Vxc))
% 1.25/1.54  (zenon_Vt != zenon_Vjd)
% 1.25/1.54  (-. (p1 zenon_Vbe))
% 1.25/1.54  (zenon_Vm != zenon_Vcd)
% 1.25/1.54  (p2 zenon_Vr)
% 1.25/1.54  (zenon_Vm != zenon_Vbd)
% 1.25/1.54  (zenon_Vo != zenon_Vpd)
% 1.25/1.54  (-. (p4 zenon_Vac))
% 1.25/1.54  (-. (p3 Tau_8))
% 1.25/1.54  (-. (p2 Tau_16))
% 1.25/1.54  (-. (p3 zenon_Vjb))
% 1.25/1.54  (-. (p2 zenon_Vyb))
% 1.25/1.54  (r1 zenon_Vuf zenon_Vvf)
% 1.25/1.54  (zenon_Vm != zenon_Vyb)
% 1.25/1.54  (-. (p4 zenon_Vic))
% 1.25/1.54  (r1 zenon_X20 zenon_Vm)
% 1.25/1.54  (-. (p2 zenon_Vzb))
% 1.25/1.54  (-. (p2 zenon_Vuf))
% 1.25/1.54  (-. (p1 zenon_Vje))
% 1.25/1.54  (-. (p2 zenon_Vs))
% 1.25/1.54  (r1 zenon_Vbe zenon_Vce)
% 1.25/1.54  (r1 Tau_15 zenon_Vwf)
% 1.25/1.54  (-. (p1 Tau_9))
% 1.25/1.54  (-. (p1 zenon_Vrb))
% 1.25/1.54  (zenon_Vr != zenon_Vkd)
% 1.25/1.54  (zenon_Vr != zenon_Vte)
% 1.25/1.54  (zenon_Vm != zenon_Vjc)
% 1.25/1.54  (-. (p4 zenon_Vib))
% 1.25/1.54  (-. (p2 zenon_Vxf))
% 1.25/1.54  (zenon_Vr != Tau_11)
% 1.25/1.54  (zenon_Vm != Tau_11)
% 1.25/1.54  (zenon_Vo != Tau_11)
% 1.25/1.54  (zenon_Vt != Tau_11)
% 1.25/1.54  (zenon_Vt != zenon_Vee)
% 1.25/1.54  (-. (p2 zenon_Vhf))
% 1.25/1.54  (-. (p1 zenon_Vjb))
% 1.25/1.54  (zenon_Vt != Tau_18)
% 1.25/1.54  (-. (p2 zenon_Vbe))
% 1.25/1.54  (r1 zenon_Vcf zenon_Vdf)
% 1.25/1.54  (-. (p1 Tau_11))
% 1.25/1.54  (zenon_Vr != zenon_Vpc)
% 1.25/1.54  (-. (p3 zenon_Vkc))
% 1.25/1.54  (zenon_Vm != zenon_Vkd)
% 1.25/1.54  (zenon_Vm != zenon_Vcg)
% 1.25/1.54  (zenon_Vt != zenon_Vac)
% 1.25/1.54  (r1 Tau_0 Tau_4)
% 1.25/1.54  (-. (p1 zenon_Vsb))
% 1.25/1.54  (-. (p4 zenon_Vje))
% 1.25/1.54  (zenon_Vr != zenon_Ved)
% 1.25/1.54  (-. (p1 zenon_Vlf))
% 1.25/1.54  (r1 zenon_Vkc zenon_Vlc)
% 1.25/1.54  (zenon_Vo != zenon_Vzb)
% 1.25/1.54  (zenon_Vr != zenon_Voc)
% 1.25/1.54  (zenon_Vt != zenon_Vcc)
% 1.25/1.54  (zenon_Vm != zenon_Vib)
% 1.25/1.54  (-. (p2 zenon_Vrg))
% 1.25/1.54  (r1 Tau_0 Tau_17)
% 1.25/1.54  (r1 zenon_Vlb zenon_Vrb)
% 1.25/1.54  (zenon_Vr != zenon_Vrd)
% 1.25/1.54  (-. (p2 zenon_Vod))
% 1.25/1.54  (zenon_Vo != zenon_Vuf)
% 1.25/1.54  (r1 zenon_Vmg zenon_Vpg)
% 1.25/1.54  (-. (p2 Tau_8))
% 1.25/1.54  (zenon_Vo != zenon_Vkd)
% 1.25/1.54  (zenon_Vt != zenon_Vzb)
% 1.25/1.54  (-. (p1 zenon_Vkd))
% 1.25/1.54  (-. (p2 zenon_Vrc))
% 1.25/1.54  (zenon_Vo != zenon_Vwd)
% 1.25/1.54  (-. (p2 Tau_12))
% 1.25/1.54  (r1 Tau_12 zenon_Vwe)
% 1.25/1.54  (r1 zenon_Vm zenon_Vn)
% 1.25/1.54  (r1 Tau_0 Tau_16)
% 1.25/1.54  (-. (p2 zenon_Vwd))
% 1.25/1.54  (zenon_Vo != zenon_Vib)
% 1.25/1.54  (-. (p2 Tau_4))
% 1.25/1.54  (zenon_Vr != zenon_Vrb)
% 1.25/1.54  (zenon_Vt != Tau_14)
% 1.25/1.54  (p3 zenon_Vo)
% 1.25/1.54  (r1 zenon_Vjd zenon_Vkd)
% 1.25/1.54  (zenon_Vt != zenon_Vkd)
% 1.25/1.54  (zenon_Vm != zenon_Vwd)
% 1.25/1.54  (r1 zenon_Vod zenon_Vpd)
% 1.25/1.54  (r1 zenon_Vrc zenon_Vwc)
% 1.25/1.54  (-. (p3 Tau_15))
% 1.25/1.54  (-. (p3 zenon_Vsb))
% 1.25/1.54  (r1 zenon_X21 zenon_Vo)
% 1.25/1.54  (zenon_Vm != zenon_Vbe)
% 1.25/1.54  (-. (p2 zenon_Vjd))
% 1.25/1.54  (zenon_Vr != zenon_Vff)
% 1.25/1.54  (zenon_Vt != zenon_Vje)
% 1.25/1.54  (zenon_Vr != Tau_16)
% 1.25/1.54  (zenon_Vm != Tau_16)
% 1.25/1.54  (zenon_Vo != Tau_16)
% 1.25/1.54  (zenon_Vt != Tau_16)
% 1.25/1.54  (zenon_Vm != zenon_Vcb)
% 1.25/1.54  (zenon_Vt != zenon_Vye)
% 1.25/1.54  (r1 zenon_Vxc zenon_Vyc)
% 1.25/1.54  (-. (p2 zenon_Vhg))
% 1.25/1.54  (zenon_Vr != zenon_Vxd)
% 1.25/1.54  (-. (p2 zenon_Vxd))
% 1.25/1.54  (r1 Tau_0 Tau_1)
% 1.25/1.54  (zenon_Vo != zenon_Vxd)
% 1.25/1.54  (zenon_Vm != zenon_Vne)
% 1.25/1.54  (zenon_Vo != zenon_Vjb)
% 1.25/1.54  (-. (p1 zenon_Vcc))
% 1.25/1.54  (-. (p3 zenon_Vzb))
% 1.25/1.54  (zenon_Vm != zenon_Ved)
% 1.25/1.54  (r1 Tau_18 zenon_Vlg)
% 1.25/1.54  (-. (p1 zenon_Vrc))
% 1.25/1.54  (zenon_Vt != Tau_10)
% 1.25/1.54  (-. (p4 Tau_15))
% 1.25/1.54  (zenon_Vt != zenon_Vib)
% 1.25/1.54  (zenon_Vr != zenon_Vcb)
% 1.25/1.54  (zenon_Vo != zenon_Vjc)
% 1.25/1.54  (r1 zenon_Vpc zenon_Vqc)
% 1.25/1.54  (zenon_Vr != Tau_15)
% 1.25/1.54  (zenon_Vm != Tau_15)
% 1.25/1.54  (zenon_Vo != Tau_15)
% 1.25/1.54  (zenon_Vt != Tau_15)
% 1.25/1.54  (zenon_Vr != zenon_Vne)
% 1.25/1.54  (-. (p4 zenon_Vpd))
% 1.25/1.54  (-. (p2 zenon_Vff))
% 1.25/1.54  (zenon_Vo != zenon_Vke)
% 1.25/1.54  (zenon_Vo != zenon_Vte)
% 1.25/1.54  (-. (p3 zenon_Vxf))
% 1.25/1.54  (zenon_Vm != zenon_Vwc)
% 1.25/1.54  (-. (p4 zenon_Vrc))
% 1.25/1.54  (zenon_Vm != zenon_Vs)
% 1.25/1.54  (r1 zenon_Vbd zenon_Vcd)
% 1.25/1.54  (r1 zenon_Ved zenon_Vjd)
% 1.25/1.54  (-. (p2 zenon_Vlf))
% 1.25/1.54  (-. (p4 zenon_Vwd))
% 1.25/1.54  (-. (p4 zenon_Vtb))
% 1.25/1.54  (-. (p1 zenon_Vbd))
% 1.25/1.54  (-. (p1 zenon_Vod))
% 1.25/1.54  (zenon_Vo != zenon_Vof)
% 1.25/1.54  *)
% 1.25/1.54  (* NO-PROOF *)
% 1.25/1.55  % SZS status GaveUp
% 1.25/1.55  Number of rewrites on terms: 0
% 1.25/1.55  Number of rewrites on props: 0
% 1.25/1.55  nodes searched: 553
% 1.25/1.55  max branch formulas: 870
% 1.25/1.55  proof nodes created: 0
% 1.25/1.55  formulas created: 5377
% 1.25/1.55  
%------------------------------------------------------------------------------