↑ Up

ZenonModulo---0.5.0.UNK-Non.f

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

% Computer : n013.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:23 PM UTC 2026

% Result   : Unknown 0.21s 0.52s
% Output   : None 
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : LCL670+1.010 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03  % Command  : run_zenon_modulo %d %s
% 0.09/0.34  % Computer : n013.cluster.edu
% 0.09/0.34  % Model    : x86_64 x86_64
% 0.09/0.34  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.34  % Memory   : 8046.5625MB
% 0.09/0.34  % OS       : Linux 6.8.0-71-generic
% 0.09/0.34  % CPULimit : 300
% 0.09/0.34  % WCLimit  : 300
% 0.09/0.34  % DateTime : Sat Sep  5 15:34:49 UTC 2026
% 0.09/0.34  % CPUTime  : 
% 0.21/0.51  Zenon error: exhausted search space without finding a proof
% 0.21/0.51  (* Current branch:
% 0.21/0.51  (zenon_Vqd != zenon_Vsc)
% 0.21/0.51  (zenon_Vcc != zenon_Vcd)
% 0.21/0.51  (r1 zenon_Vib zenon_Vlb)
% 0.21/0.51  (zenon_Vse != zenon_Vmd)
% 0.21/0.51  (zenon_Vge != zenon_Vwb)
% 0.21/0.51  (zenon_Vgd != zenon_Vdb)
% 0.21/0.51  (zenon_Vge != zenon_Vmd)
% 0.21/0.51  (-. (p1 zenon_Vdb))
% 0.21/0.51  (zenon_Vef != zenon_Vxc)
% 0.21/0.51  (zenon_Vhc != zenon_Vhd)
% 0.21/0.51  (zenon_Vaf != zenon_Vna)
% 0.21/0.51  (r1 zenon_Vab zenon_Vdb)
% 0.21/0.51  (r1 zenon_Vka zenon_Vna)
% 0.21/0.51  (zenon_Vyb != zenon_Vdb)
% 0.21/0.51  (zenon_Vaf != zenon_Vra)
% 0.21/0.51  (zenon_Vbd != zenon_Vra)
% 0.21/0.51  (zenon_Vse != zenon_Vic)
% 0.21/0.51  (zenon_Vwe != zenon_Vhb)
% 0.21/0.51  (zenon_Vrc != zenon_Vic)
% 0.21/0.51  (zenon_Vhf != zenon_Vic)
% 0.21/0.51  (zenon_Vaf != zenon_Vsc)
% 0.21/0.51  (zenon_Vmc != zenon_Vra)
% 0.21/0.51  (zenon_Vgd != zenon_Vsc)
% 0.21/0.51  (zenon_Vmc != zenon_Vnc)
% 0.21/0.51  (zenon_Vse != zenon_Vza)
% 0.21/0.51  (zenon_Vef != zenon_Vnc)
% 0.21/0.51  (-. (p1 zenon_Vlb))
% 0.21/0.51  (zenon_Vcc != zenon_Vtb)
% 0.21/0.51  (zenon_Vyb != zenon_Vnc)
% 0.21/0.51  (zenon_Vaf != zenon_Vnc)
% 0.21/0.51  (zenon_Vqd != zenon_Vrd)
% 0.21/0.51  (zenon_Vgd != zenon_Vnc)
% 0.21/0.51  (zenon_Vaf != zenon_Vcd)
% 0.21/0.51  (zenon_Vgd != zenon_Vmd)
% 0.21/0.51  (zenon_Vrc != zenon_Vmd)
% 0.21/0.51  (zenon_Vyb != zenon_Vza)
% 0.21/0.51  (r1 zenon_Vid zenon_Vjd)
% 0.21/0.51  (zenon_Vaf != zenon_Vdb)
% 0.21/0.51  (r1 zenon_Vzc zenon_Vcd)
% 0.21/0.51  (zenon_Vhc != zenon_Vna)
% 0.21/0.51  (r1 zenon_Ved zenon_Vfd)
% 0.21/0.51  (-. (p1 zenon_Vmd))
% 0.21/0.51  (zenon_Voe != zenon_Vtb)
% 0.21/0.51  (zenon_Vhc != zenon_Vra)
% 0.21/0.51  (zenon_Vyb != zenon_Vmd)
% 0.21/0.51  (zenon_Vhc != zenon_Vpb)
% 0.21/0.51  (zenon_Vrc != zenon_Vza)
% 0.21/0.51  (zenon_Vmc != zenon_Vwb)
% 0.21/0.51  (zenon_Vrc != zenon_Vnc)
% 0.21/0.51  (p1 zenon_Vcc)
% 0.21/0.51  (zenon_Vwc != zenon_Vna)
% 0.21/0.51  (r1 zenon_Vid zenon_Vnd)
% 0.21/0.51  (zenon_Vbd != zenon_Vic)
% 0.21/0.51  (zenon_Vgd != zenon_Vna)
% 0.21/0.51  (p1 zenon_Vce)
% 0.21/0.51  (zenon_Vke != zenon_Vdc)
% 0.21/0.51  (zenon_Vhf != zenon_Vcd)
% 0.21/0.51  (p1 zenon_Vld)
% 0.21/0.51  (zenon_Vqd != zenon_Vwb)
% 0.21/0.51  (zenon_Vwe != zenon_Vic)
% 0.21/0.51  (zenon_Vhc != zenon_Vdc)
% 0.21/0.51  (zenon_Vce != zenon_Vsc)
% 0.21/0.51  (zenon_Vmc != zenon_Vic)
% 0.21/0.51  (zenon_Vce != zenon_Vpb)
% 0.21/0.51  (zenon_Vce != zenon_Vnc)
% 0.21/0.51  (p1 zenon_Vyd)
% 0.21/0.51  (zenon_Vaf != zenon_Vmd)
% 0.21/0.51  (-. (p1 zenon_Vna))
% 0.21/0.51  (zenon_Vhc != zenon_Vmd)
% 0.21/0.51  (r1 zenon_Vxe zenon_Vaf)
% 0.21/0.51  (zenon_Vaf != zenon_Vpb)
% 0.21/0.51  (zenon_Vhf != zenon_Vhb)
% 0.21/0.51  (p1 zenon_Vwc)
% 0.21/0.51  (zenon_Vbd != zenon_Vmd)
% 0.21/0.51  (-. (p2 zenon_Vud))
% 0.21/0.51  (-. (p1 zenon_Vtb))
% 0.21/0.51  (zenon_Vcc != zenon_Vva)
% 0.21/0.51  (zenon_Voe != zenon_Vdc)
% 0.21/0.51  (zenon_Vbd != zenon_Vsc)
% 0.21/0.51  (zenon_Vmc != zenon_Vdb)
% 0.21/0.51  (-. (p1 zenon_Vzb))
% 0.21/0.51  (zenon_Vld != zenon_Vva)
% 0.21/0.51  (-. (p1 zenon_Vxc))
% 0.21/0.51  (r1 zenon_Vqb zenon_Vtb)
% 0.21/0.51  (zenon_Vgd != zenon_Vcd)
% 0.21/0.51  (zenon_Vwe != zenon_Vmd)
% 0.21/0.51  (zenon_Vyd != zenon_Vxc)
% 0.21/0.51  (zenon_Vge != zenon_Vhd)
% 0.21/0.51  (zenon_Vse != zenon_Vpb)
% 0.21/0.51  (zenon_Vrc != zenon_Vhd)
% 0.21/0.51  (zenon_Vhc != zenon_Vcd)
% 0.21/0.51  (zenon_Voe != zenon_Vra)
% 0.21/0.51  (p1 zenon_Vqd)
% 0.21/0.51  (r1 zenon_Vtc zenon_Vyc)
% 0.21/0.51  (p1 zenon_Vke)
% 0.21/0.51  (-. (p1 zenon_Vpb))
% 0.21/0.51  (zenon_Vwe != zenon_Vra)
% 0.21/0.51  (zenon_Vqd != zenon_Vpb)
% 0.21/0.51  (zenon_Vqd != zenon_Vcd)
% 0.21/0.51  (zenon_Vce != zenon_Vic)
% 0.21/0.51  (zenon_Vwc != zenon_Vhd)
% 0.21/0.51  (-. (p2 zenon_Vja))
% 0.21/0.51  (zenon_Vge != zenon_Vpb)
% 0.21/0.51  (zenon_Vcc != zenon_Vdb)
% 0.21/0.51  (zenon_Vef != zenon_Vcd)
% 0.21/0.51  (-. (p1 zenon_Vhb))
% 0.21/0.51  (zenon_Vrc != zenon_Vtb)
% 0.21/0.51  (zenon_Vld != zenon_Vic)
% 0.21/0.51  (r1 zenon_Vle zenon_Voe)
% 0.21/0.51  (p1 zenon_Vhf)
% 0.21/0.51  (zenon_Vyd != zenon_Vva)
% 0.21/0.51  (zenon_Vbd != zenon_Vza)
% 0.21/0.51  (zenon_Vhf != zenon_Vdb)
% 0.21/0.51  (zenon_Vwc != zenon_Vxc)
% 0.21/0.51  (zenon_Vhc != zenon_Vdb)
% 0.21/0.51  (zenon_Vld != zenon_Vzb)
% 0.21/0.51  (zenon_Vwe != zenon_Vxc)
% 0.21/0.51  (r1 zenon_Vac zenon_Vbc)
% 0.21/0.51  (zenon_Vyd != zenon_Vwb)
% 0.21/0.51  (p1 zenon_Vaf)
% 0.21/0.51  (r1 zenon_Voa zenon_Vra)
% 0.21/0.51  (zenon_Vyb != zenon_Vwb)
% 0.21/0.51  (zenon_Voe != zenon_Vmd)
% 0.21/0.51  (zenon_Vwe != zenon_Vdc)
% 0.21/0.51  (r1 zenon_X5 zenon_Vwb)
% 0.21/0.51  (zenon_Vwc != zenon_Vdc)
% 0.21/0.51  (zenon_Vmc != zenon_Vzb)
% 0.21/0.51  (r1 zenon_Voc zenon_Vpc)
% 0.21/0.51  (zenon_Vke != zenon_Vna)
% 0.21/0.51  (zenon_Vyd != zenon_Vzb)
% 0.21/0.51  (zenon_Vhc != zenon_Vrd)
% 0.21/0.51  (r1 zenon_Vdd zenon_Ved)
% 0.21/0.51  (zenon_Vyd != zenon_Vtb)
% 0.21/0.51  (r1 zenon_Vod zenon_Vrd)
% 0.21/0.51  (zenon_Vse != zenon_Vtb)
% 0.21/0.51  (zenon_Vld != zenon_Vwb)
% 0.21/0.51  (-. (p1 zenon_Vsc))
% 0.21/0.51  (r1 zenon_X6 zenon_Vhf)
% 0.21/0.51  (zenon_Vld != zenon_Vnc)
% 0.21/0.51  (zenon_Vce != zenon_Vcd)
% 0.21/0.51  (zenon_Vcc != zenon_Vwb)
% 0.21/0.51  (zenon_Vyd != zenon_Vza)
% 0.21/0.51  (zenon_Vef != zenon_Vrd)
% 0.21/0.51  (zenon_Vef != zenon_Vzb)
% 0.21/0.51  (zenon_Vhc != zenon_Vhb)
% 0.21/0.51  (zenon_Voe != zenon_Vcd)
% 0.21/0.51  (r1 zenon_Vjc zenon_Voc)
% 0.21/0.51  (zenon_Vcc != zenon_Vza)
% 0.21/0.51  (r1 zenon_Vte zenon_Vwe)
% 0.21/0.51  (zenon_Vce != zenon_Vhb)
% 0.21/0.51  (zenon_Vke != zenon_Vva)
% 0.21/0.51  (zenon_Vaf != zenon_Vrd)
% 0.21/0.51  (zenon_Vhf != zenon_Vdc)
% 0.21/0.51  (zenon_Vhf != zenon_Vsc)
% 0.21/0.51  (zenon_Vqd != zenon_Vzb)
% 0.21/0.51  (zenon_Vgd != zenon_Vwb)
% 0.21/0.51  (zenon_Vbd != zenon_Vdc)
% 0.21/0.51  (zenon_Vcc != zenon_Vzb)
% 0.21/0.51  (r1 zenon_Vzc zenon_Vad)
% 0.21/0.51  (zenon_Vef != zenon_Vhd)
% 0.21/0.51  (-. (p1 zenon_Vcd))
% 0.21/0.51  (zenon_Vmc != zenon_Vxc)
% 0.21/0.51  (zenon_Vke != zenon_Vzb)
% 0.21/0.51  (zenon_Vwc != zenon_Vpb)
% 0.21/0.51  (zenon_Vcc != zenon_Vdc)
% 0.21/0.51  (zenon_Vwc != zenon_Vva)
% 0.21/0.51  (r1 zenon_Vwa zenon_Vza)
% 0.21/0.51  (zenon_Vyb != zenon_Vva)
% 0.21/0.51  (zenon_Vbd != zenon_Vcd)
% 0.21/0.51  (r1 zenon_Vsa zenon_Vva)
% 0.21/0.51  (zenon_Vqd != zenon_Vnc)
% 0.21/0.51  (zenon_Vwe != zenon_Vnc)
% 0.21/0.51  (zenon_Vhc != zenon_Vva)
% 0.21/0.51  (zenon_Vwc != zenon_Vdb)
% 0.21/0.51  (zenon_Vge != zenon_Vic)
% 0.21/0.51  (zenon_Vge != zenon_Vxc)
% 0.21/0.51  (zenon_Vse != zenon_Vdb)
% 0.21/0.51  (zenon_Vld != zenon_Vna)
% 0.21/0.51  (zenon_Vhf != zenon_Vwb)
% 0.21/0.51  (zenon_Vw != zenon_Vda)
% 0.21/0.51  (zenon_Vef != zenon_Vsc)
% 0.21/0.51  (-. (p4 zenon_X3))
% 0.21/0.51  (zenon_Vrc != zenon_Vpb)
% 0.21/0.51  (zenon_Vhf != zenon_Vza)
% 0.21/0.51  (zenon_Vw != zenon_Vja)
% 0.21/0.51  (zenon_Vqd != zenon_Vxc)
% 0.21/0.51  (zenon_Vmc != zenon_Vtb)
% 0.21/0.51  (zenon_Vld != zenon_Vsc)
% 0.21/0.51  (zenon_Vaf != zenon_Vhb)
% 0.21/0.51  (zenon_Vke != zenon_Vcd)
% 0.21/0.51  (-. (p1 zenon_Vrd))
% 0.21/0.51  (zenon_Vke != zenon_Vhd)
% 0.21/0.51  (zenon_Vcc != zenon_Vic)
% 0.21/0.51  (zenon_Vqd != zenon_Vhb)
% 0.21/0.51  (r1 zenon_Veb zenon_Vhb)
% 0.21/0.51  (zenon_Vbd != zenon_Vdb)
% 0.21/0.51  (r1 zenon_Vnd zenon_Vod)
% 0.21/0.51  (zenon_Vrc != zenon_Vxc)
% 0.21/0.51  (zenon_Vhc != zenon_Vza)
% 0.21/0.51  (zenon_Vbd != zenon_Vna)
% 0.21/0.51  (zenon_Vhf != zenon_Vmd)
% 0.21/0.51  (zenon_Vwc != zenon_Vra)
% 0.21/0.51  (-. (p1 zenon_Vza))
% 0.21/0.51  (zenon_Vse != zenon_Vdc)
% 0.21/0.51  (zenon_Vmc != zenon_Vrd)
% 0.21/0.51  (zenon_Vld != zenon_Vrd)
% 0.21/0.51  (zenon_Voe != zenon_Vrd)
% 0.21/0.51  (r1 zenon_Ved zenon_Vhd)
% 0.21/0.51  (zenon_Vge != zenon_Vhb)
% 0.21/0.51  (zenon_Voe != zenon_Vwb)
% 0.21/0.51  (zenon_Vhf != zenon_Vra)
% 0.21/0.51  (zenon_Vce != zenon_Vwb)
% 0.21/0.51  (zenon_Vce != zenon_Vhd)
% 0.21/0.51  (p2 zenon_Vw)
% 0.21/0.51  (zenon_Vge != zenon_Vnc)
% 0.21/0.51  (-. (p1 zenon_Vdc))
% 0.21/0.51  (r1 zenon_Vyc zenon_Vzc)
% 0.21/0.51  (zenon_Vcc != zenon_Vpb)
% 0.21/0.51  (r1 zenon_Vyc zenon_Vdd)
% 0.21/0.51  (zenon_Vmc != zenon_Vcd)
% 0.21/0.51  (zenon_Vrc != zenon_Vra)
% 0.21/0.51  (zenon_Vyb != zenon_Vzb)
% 0.21/0.51  (zenon_Vef != zenon_Vtb)
% 0.21/0.51  (r1 zenon_Vpe zenon_Vse)
% 0.21/0.51  (zenon_Vmc != zenon_Vsc)
% 0.21/0.51  (zenon_Vld != zenon_Vpb)
% 0.21/0.51  (zenon_Vrc != zenon_Vzb)
% 0.21/0.51  (zenon_Vqd != zenon_Vtb)
% 0.21/0.51  (zenon_Vwe != zenon_Vlb)
% 0.21/0.51  (zenon_Vcc != zenon_Vsc)
% 0.21/0.51  (zenon_Vef != zenon_Vlb)
% 0.21/0.51  (r1 Tau_0 Tau_1)
% 0.21/0.51  (zenon_Vwe != zenon_Vpb)
% 0.21/0.51  (zenon_Voe != zenon_Vxc)
% 0.21/0.51  (zenon_Vbd != zenon_Vtb)
% 0.21/0.51  (zenon_Vrc != zenon_Vna)
% 0.21/0.51  (zenon_Vld != zenon_Vhd)
% 0.21/0.51  (zenon_Vse != zenon_Vxc)
% 0.21/0.51  (zenon_Vwc != zenon_Vnc)
% 0.21/0.51  (r1 zenon_Vtd zenon_Vud)
% 0.21/0.51  (zenon_Vyd != zenon_Vrd)
% 0.21/0.51  (p1 zenon_Vbd)
% 0.21/0.51  (zenon_Voe != zenon_Vhd)
% 0.21/0.51  (zenon_Vwe != zenon_Vva)
% 0.21/0.51  (p1 zenon_Vmc)
% 0.21/0.51  (zenon_Vwe != zenon_Vzb)
% 0.21/0.51  (zenon_Vwc != zenon_Vcd)
% 0.21/0.51  (zenon_Vyd != zenon_Vdb)
% 0.21/0.51  (zenon_Vcc != zenon_Vhd)
% 0.21/0.51  (zenon_Vmc != zenon_Vhd)
% 0.21/0.51  (zenon_Vyd != zenon_Vra)
% 0.21/0.51  (zenon_Vwe != zenon_Vdb)
% 0.21/0.51  (zenon_Vbd != zenon_Vxc)
% 0.21/0.51  (zenon_Vke != zenon_Vnc)
% 0.21/0.51  (zenon_Vyd != zenon_Vmd)
% 0.21/0.51  (zenon_Vce != zenon_Vva)
% 0.21/0.51  (zenon_Vhc != zenon_Vxc)
% 0.21/0.51  (zenon_Vyb != zenon_Vpb)
% 0.21/0.51  (zenon_Vke != zenon_Vtb)
% 0.21/0.51  (zenon_Vke != zenon_Vsc)
% 0.21/0.51  (zenon_Vbd != zenon_Vhd)
% 0.21/0.51  (zenon_Vgd != zenon_Vhb)
% 0.21/0.51  (zenon_Vhc != zenon_Vic)
% 0.21/0.51  (zenon_Voe != zenon_Vdb)
% 0.21/0.51  (r1 zenon_Vhe zenon_Vke)
% 0.21/0.51  (zenon_Vmc != zenon_Vlb)
% 0.21/0.51  (zenon_Vgd != zenon_Vxc)
% 0.21/0.51  (-. (p1 zenon_Vhd))
% 0.21/0.51  (zenon_Vce != zenon_Vdc)
% 0.21/0.51  (zenon_Vyb != zenon_Vtb)
% 0.21/0.51  (zenon_Vhc != zenon_Vtb)
% 0.21/0.51  (zenon_Vld != zenon_Vlb)
% 0.21/0.51  (zenon_Vhf != zenon_Vlb)
% 0.21/0.51  (zenon_Vyd != zenon_Vic)
% 0.21/0.51  (zenon_Vce != zenon_Vmd)
% 0.21/0.51  (zenon_Vgd != zenon_Vzb)
% 0.21/0.51  (zenon_Vmc != zenon_Vza)
% 0.21/0.51  (zenon_Vrc != zenon_Vhb)
% 0.21/0.51  (zenon_Vge != zenon_Vrd)
% 0.21/0.51  (zenon_Vgd != zenon_Vdc)
% 0.21/0.51  (zenon_Vld != zenon_Vhb)
% 0.21/0.51  (zenon_Vbd != zenon_Vrd)
% 0.21/0.51  (zenon_Vse != zenon_Vva)
% 0.21/0.51  (zenon_Vbd != zenon_Vva)
% 0.21/0.51  (zenon_Vaf != zenon_Vtb)
% 0.21/0.51  (zenon_Vwc != zenon_Vlb)
% 0.21/0.51  (zenon_Vwe != zenon_Vsc)
% 0.21/0.51  (zenon_Vwc != zenon_Vsc)
% 0.21/0.51  (zenon_Vyb != zenon_Vna)
% 0.21/0.51  (r1 zenon_Vu zenon_Via)
% 0.21/0.51  (zenon_Vce != zenon_Vtb)
% 0.21/0.51  (zenon_Vrc != zenon_Vdc)
% 0.21/0.51  (zenon_Vef != zenon_Vdb)
% 0.21/0.51  (zenon_Vwc != zenon_Vzb)
% 0.21/0.51  (zenon_Vce != zenon_Vzb)
% 0.21/0.51  (zenon_Vrc != zenon_Vsc)
% 0.21/0.51  (zenon_Vhf != zenon_Vnc)
% 0.21/0.51  (zenon_Vhf != zenon_Vxc)
% 0.21/0.51  (r1 Tau_1 zenon_Vzb)
% 0.21/0.51  (zenon_Vke != zenon_Vra)
% 0.21/0.51  (r1 zenon_Vec zenon_Vfc)
% 0.21/0.51  (zenon_Vef != zenon_Vza)
% 0.21/0.51  (r1 zenon_Vzd zenon_Vce)
% 0.21/0.51  (zenon_Vke != zenon_Vxc)
% 0.21/0.51  (zenon_Vaf != zenon_Vzb)
% 0.21/0.51  (zenon_Vge != zenon_Vva)
% 0.21/0.51  (zenon_Vld != zenon_Vra)
% 0.21/0.51  (r1 zenon_Vvd zenon_Vyd)
% 0.21/0.51  (zenon_Vcc != zenon_Vna)
% 0.21/0.51  (zenon_Vmc != zenon_Vmd)
% 0.21/0.51  (zenon_Vce != zenon_Vra)
% 0.21/0.51  (zenon_Vke != zenon_Vpb)
% 0.21/0.51  (zenon_Voe != zenon_Vva)
% 0.21/0.51  (zenon_Vge != zenon_Vcd)
% 0.21/0.51  (zenon_Vce != zenon_Vxc)
% 0.21/0.51  (zenon_Voe != zenon_Vic)
% 0.21/0.51  (zenon_Vrc != zenon_Vlb)
% 0.21/0.51  (zenon_Vgd != zenon_Vtb)
% 0.21/0.51  (zenon_Vhc != zenon_Vwb)
% 0.21/0.51  (p1 zenon_Vgd)
% 0.21/0.51  (r1 zenon_Vjc zenon_Vkc)
% 0.21/0.51  (zenon_Vce != zenon_Vdb)
% 0.21/0.51  (r1 zenon_Vba zenon_Vca)
% 0.21/0.51  (zenon_Voe != zenon_Vhb)
% 0.21/0.51  (r1 zenon_Vmb zenon_Vpb)
% 0.21/0.51  (zenon_Vyb != zenon_Vdc)
% 0.21/0.51  (zenon_Vcc != zenon_Vlb)
% 0.21/0.51  (zenon_Vwc != zenon_Vmd)
% 0.21/0.51  (zenon_Vbd != zenon_Vhb)
% 0.21/0.51  (r1 Tau_0 Tau_2)
% 0.21/0.51  (zenon_Vhc != zenon_Vlb)
% 0.21/0.51  (zenon_Vaf != zenon_Vxc)
% 0.21/0.51  (zenon_Vhf != zenon_Vzb)
% 0.21/0.51  (p1 zenon_Vwe)
% 0.21/0.51  (zenon_Vld != zenon_Vdc)
% 0.21/0.51  (zenon_Vld != zenon_Vmd)
% 0.21/0.51  (r1 zenon_Vdd zenon_Vid)
% 0.21/0.51  (zenon_Vhf != zenon_Vtb)
% 0.21/0.51  (zenon_Voe != zenon_Vna)
% 0.21/0.51  (zenon_Vcc != zenon_Vra)
% 0.21/0.51  (-. (p3 zenon_Vx))
% 0.21/0.51  (zenon_Vse != zenon_Vlb)
% 0.21/0.51  (zenon_Vse != zenon_Vhb)
% 0.21/0.51  (zenon_Vce != zenon_Vza)
% 0.21/0.51  (zenon_Vbd != zenon_Vzb)
% 0.21/0.51  (zenon_Vqd != zenon_Vmd)
% 0.21/0.51  (zenon_Voe != zenon_Vnc)
% 0.21/0.51  (zenon_Vbd != zenon_Vlb)
% 0.21/0.51  (zenon_Vge != zenon_Vlb)
% 0.21/0.51  (zenon_Vhf != zenon_Vna)
% 0.21/0.51  (zenon_Voe != zenon_Vza)
% 0.21/0.51  (zenon_Vyb != zenon_Vhb)
% 0.21/0.51  (zenon_Vgd != zenon_Vza)
% 0.21/0.51  (zenon_Vmc != zenon_Vna)
% 0.21/0.51  (p1 zenon_Vge)
% 0.21/0.51  (zenon_Vcc != zenon_Vnc)
% 0.21/0.51  (zenon_Vld != zenon_Vcd)
% 0.21/0.51  (zenon_Vaf != zenon_Vdc)
% 0.21/0.51  (zenon_Vhf != zenon_Vhd)
% 0.21/0.51  (-. (p1 zenon_Vnc))
% 0.21/0.51  (zenon_Vmc != zenon_Vva)
% 0.21/0.51  (zenon_Vke != zenon_Vhb)
% 0.21/0.51  (zenon_Vaf != zenon_Vza)
% 0.21/0.51  (-. (p1 zenon_Vic))
% 0.21/0.51  (zenon_Vcc != zenon_Vhb)
% 0.21/0.51  (zenon_Vaf != zenon_Vhd)
% 0.21/0.51  (zenon_Vyd != zenon_Vna)
% 0.21/0.51  (zenon_Vyd != zenon_Vhd)
% 0.21/0.51  (zenon_Vse != zenon_Vcd)
% 0.21/0.51  (r1 zenon_Vde zenon_Vge)
% 0.21/0.51  (zenon_Vhc != zenon_Vzb)
% 0.21/0.51  (r1 Tau_2 zenon_Vac)
% 0.21/0.51  (r1 Tau_2 zenon_Vec)
% 0.21/0.51  (zenon_Vef != zenon_Vna)
% 0.21/0.51  (zenon_Vgd != zenon_Vhd)
% 0.21/0.51  (zenon_Vcc != zenon_Vxc)
% 0.21/0.51  (-. (p1 zenon_Vra))
% 0.21/0.51  (zenon_Vgd != zenon_Vlb)
% 0.21/0.51  (zenon_Vcc != zenon_Vmd)
% 0.21/0.51  (zenon_Vqd != zenon_Vza)
% 0.21/0.51  (zenon_Vwe != zenon_Vcd)
% 0.21/0.51  (zenon_Vqd != zenon_Vra)
% 0.21/0.51  (zenon_Vaf != zenon_Vwb)
% 0.21/0.51  (zenon_Vef != zenon_Vmd)
% 0.21/0.51  (zenon_Vyb != zenon_Vxc)
% 0.21/0.51  (zenon_Vyb != zenon_Vlb)
% 0.21/0.51  (zenon_Vke != zenon_Vdb)
% 0.21/0.51  (zenon_Vyb != zenon_Vrd)
% 0.21/0.51  (zenon_Vge != zenon_Vsc)
% 0.21/0.51  (zenon_Vke != zenon_Vmd)
% 0.21/0.51  (zenon_Vke != zenon_Vza)
% 0.21/0.51  (zenon_Vrc != zenon_Vdb)
% 0.21/0.51  (zenon_Vse != zenon_Vzb)
% 0.21/0.51  (zenon_Vgd != zenon_Vva)
% 0.21/0.51  (zenon_Vhc != zenon_Vsc)
% 0.21/0.51  (zenon_Vwc != zenon_Vtb)
% 0.21/0.51  (zenon_Vhf != zenon_Vva)
% 0.21/0.51  (r1 zenon_Vfc zenon_Vgc)
% 0.21/0.51  (zenon_Vld != zenon_Vxc)
% 0.21/0.51  (zenon_Vbd != zenon_Vpb)
% 0.21/0.51  (zenon_Vaf != zenon_Vic)
% 0.21/0.51  (zenon_Vyd != zenon_Vlb)
% 0.21/0.51  (zenon_Vge != zenon_Vna)
% 0.21/0.51  (zenon_Vse != zenon_Vhd)
% 0.21/0.51  (zenon_Vqd != zenon_Vna)
% 0.21/0.51  (zenon_Vhf != zenon_Vrd)
% 0.21/0.51  (zenon_Vwe != zenon_Vza)
% 0.21/0.51  (zenon_Vke != zenon_Vrd)
% 0.21/0.51  (p1 zenon_Vrc)
% 0.21/0.51  (p1 zenon_Vse)
% 0.21/0.51  (r1 zenon_Vpc zenon_Vsc)
% 0.21/0.51  (r1 zenon_Vac zenon_Vdc)
% 0.21/0.51  (zenon_Vge != zenon_Vra)
% 0.21/0.51  (zenon_Vyd != zenon_Vsc)
% 0.21/0.51  (zenon_Vke != zenon_Vlb)
% 0.21/0.51  (zenon_Vef != zenon_Vra)
% 0.21/0.51  (zenon_Vwe != zenon_Vna)
% 0.21/0.51  (zenon_Vqd != zenon_Vva)
% 0.21/0.51  (zenon_Vwe != zenon_Vtb)
% 0.21/0.51  (zenon_Voe != zenon_Vlb)
% 0.21/0.51  (zenon_Vge != zenon_Vdb)
% 0.21/0.51  (zenon_Vld != zenon_Vdb)
% 0.21/0.51  (zenon_Vge != zenon_Vza)
% 0.21/0.51  (zenon_Vse != zenon_Vra)
% 0.21/0.51  (zenon_Vyb != zenon_Vsc)
% 0.21/0.51  (zenon_Vwc != zenon_Vwb)
% 0.21/0.51  (r1 zenon_Voc zenon_Vtc)
% 0.21/0.51  (-. (p2 zenon_Vda))
% 0.21/0.51  (zenon_Vke != zenon_Vic)
% 0.21/0.51  (zenon_Voe != zenon_Vpb)
% 0.21/0.51  (zenon_Vyd != zenon_Vdc)
% 0.21/0.51  (zenon_Vaf != zenon_Vlb)
% 0.21/0.51  (zenon_Vcc != zenon_Vrd)
% 0.21/0.51  (zenon_Vse != zenon_Vnc)
% 0.21/0.51  (zenon_Vke != zenon_Vwb)
% 0.21/0.51  (r1 zenon_Vkc zenon_Vlc)
% 0.21/0.51  (zenon_Vmc != zenon_Vdc)
% 0.21/0.51  (zenon_Vef != zenon_Vpb)
% 0.21/0.51  (zenon_Vge != zenon_Vdc)
% 0.21/0.51  (zenon_Vrc != zenon_Vcd)
% 0.21/0.51  (zenon_Vrc != zenon_Vwb)
% 0.21/0.51  (zenon_Vce != zenon_Vlb)
% 0.21/0.51  (zenon_Vyb != zenon_Vra)
% 0.21/0.51  (zenon_Vef != zenon_Vva)
% 0.21/0.51  (zenon_Vyd != zenon_Vnc)
% 0.21/0.51  (p1 zenon_Vhc)
% 0.21/0.51  (zenon_Vbd != zenon_Vwb)
% 0.21/0.51  (zenon_Vef != zenon_Vic)
% 0.21/0.51  (zenon_Vmc != zenon_Vpb)
% 0.21/0.51  (zenon_Vld != zenon_Vza)
% 0.21/0.51  (r1 zenon_Vbf zenon_Vef)
% 0.21/0.51  (-. (p1 zenon_Vwb))
% 0.21/0.51  (zenon_Vyb != zenon_Vic)
% 0.21/0.51  (zenon_Vge != zenon_Vtb)
% 0.21/0.51  (r1 zenon_Vv zenon_Vw)
% 0.21/0.51  (r1 zenon_Vtc zenon_Vuc)
% 0.21/0.51  (zenon_Vwc != zenon_Vic)
% 0.21/0.51  (zenon_Vw != zenon_Vud)
% 0.21/0.51  (zenon_Vqd != zenon_Vic)
% 0.21/0.51  (zenon_Vce != zenon_Vna)
% 0.21/0.51  (zenon_Vyd != zenon_Vcd)
% 0.21/0.51  (zenon_Vce != zenon_Vrd)
% 0.21/0.51  (zenon_Vgd != zenon_Vrd)
% 0.21/0.51  (zenon_Vrc != zenon_Vrd)
% 0.21/0.51  (p1 zenon_Voe)
% 0.21/0.51  (zenon_Vmc != zenon_Vhb)
% 0.21/0.51  (r1 Tau_1 zenon_Vxb)
% 0.21/0.51  (r1 zenon_Vjd zenon_Vmd)
% 0.21/0.51  (zenon_Vbd != zenon_Vnc)
% 0.21/0.51  (r1 zenon_Vfc zenon_Vic)
% 0.21/0.51  (r1 zenon_Vjd zenon_Vkd)
% 0.21/0.51  (zenon_Vaf != zenon_Vva)
% 0.21/0.51  (r1 zenon_Vod zenon_Vpd)
% 0.21/0.51  (zenon_Vef != zenon_Vhb)
% 0.21/0.51  (zenon_Vwc != zenon_Vza)
% 0.21/0.51  (zenon_Vwe != zenon_Vwb)
% 0.21/0.51  (r1 zenon_Vw zenon_Vx)
% 0.21/0.51  (zenon_Vyd != zenon_Vpb)
% 0.21/0.51  (zenon_Vef != zenon_Vdc)
% 0.21/0.51  (zenon_Vse != zenon_Vwb)
% 0.21/0.51  (r1 zenon_Vuc zenon_Vvc)
% 0.21/0.51  (zenon_Vyb != zenon_Vcd)
% 0.21/0.51  (r1 zenon_Vkc zenon_Vnc)
% 0.21/0.51  (zenon_Vyb != zenon_Vhd)
% 0.21/0.51  (zenon_Vqd != zenon_Vdc)
% 0.21/0.51  (p1 zenon_Vef)
% 0.21/0.51  (zenon_Vse != zenon_Vna)
% 0.21/0.51  (p1 zenon_Vyb)
% 0.21/0.51  (r1 zenon_Vnd zenon_Vsd)
% 0.21/0.51  (zenon_Vwc != zenon_Vhb)
% 0.21/0.51  (zenon_Vhc != zenon_Vnc)
% 0.21/0.51  (zenon_Vwe != zenon_Vhd)
% 0.21/0.51  (zenon_Vqd != zenon_Vlb)
% 0.21/0.51  (zenon_Vef != zenon_Vwb)
% 0.21/0.51  (zenon_Vqd != zenon_Vdb)
% 0.21/0.51  (r1 zenon_Vuc zenon_Vxc)
% 0.21/0.51  (zenon_Voe != zenon_Vsc)
% 0.21/0.51  (zenon_Vse != zenon_Vrd)
% 0.21/0.51  (r1 zenon_Vpc zenon_Vqc)
% 0.21/0.51  (zenon_Vrc != zenon_Vva)
% 0.21/0.51  (zenon_Voe != zenon_Vzb)
% 0.21/0.51  (zenon_Vwc != zenon_Vrd)
% 0.21/0.51  (zenon_Vyd != zenon_Vhb)
% 0.21/0.51  (zenon_Vge != zenon_Vzb)
% 0.21/0.52  (zenon_Vse != zenon_Vsc)
% 0.21/0.52  (zenon_Vgd != zenon_Vic)
% 0.21/0.52  (zenon_Vqd != zenon_Vhd)
% 0.21/0.52  (zenon_Vwe != zenon_Vrd)
% 0.21/0.52  (zenon_Vgd != zenon_Vpb)
% 0.21/0.52  (zenon_Vgd != zenon_Vra)
% 0.21/0.52  (zenon_Vld != zenon_Vtb)
% 0.21/0.52  (-. (p1 zenon_Vva))
% 0.21/0.52  (zenon_Vhf != zenon_Vpb)
% 0.21/0.52  (r1 zenon_Vec zenon_Vjc)
% 0.21/0.52  *)
% 0.21/0.52  (* NO-PROOF *)
% 0.21/0.52  % SZS status GaveUp
% 0.21/0.52  Number of rewrites on terms: 0
% 0.21/0.52  Number of rewrites on props: 0
% 0.21/0.52  nodes searched: 728
% 0.21/0.52  max branch formulas: 838
% 0.21/0.52  proof nodes created: 0
% 0.21/0.52  formulas created: 4153
% 0.21/0.52  
%------------------------------------------------------------------------------