↑ Up

ZenonModulo---0.5.0.UNK-Non.f

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

% Computer : n005.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.51s
% Output   : None 
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : LCL671+1.005 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03  % Command  : run_zenon_modulo %d %s
% 0.07/0.33  % Computer : n005.cluster.edu
% 0.07/0.33  % Model    : x86_64 x86_64
% 0.07/0.33  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.33  % Memory   : 8046.5625MB
% 0.07/0.33  % 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 03:52:51 UTC 2026
% 0.07/0.34  % CPUTime  : 
% 0.21/0.50  Zenon error: exhausted search space without finding a proof
% 0.21/0.50  (* Current branch:
% 0.21/0.50  (zenon_Vpd != zenon_Vzb)
% 0.21/0.50  (zenon_Vyb != zenon_Vid)
% 0.21/0.50  (zenon_Vtd != zenon_Vva)
% 0.21/0.50  (zenon_Vue != zenon_Vdb)
% 0.21/0.50  (r1 zenon_Vib zenon_Vlb)
% 0.21/0.50  (zenon_Vtd != zenon_Vvb)
% 0.21/0.50  (zenon_Vje != zenon_Vec)
% 0.21/0.50  (p1 zenon_Vub)
% 0.21/0.50  (-. (p1 zenon_Vdb))
% 0.21/0.50  (zenon_Vcd != zenon_Vvb)
% 0.21/0.50  (zenon_Vsc != zenon_Vlb)
% 0.21/0.50  (zenon_Vic != zenon_Vza)
% 0.21/0.50  (zenon_Vic != zenon_Vec)
% 0.21/0.50  (-. (p1 zenon_Vyc))
% 0.21/0.50  (r1 zenon_Vab zenon_Vdb)
% 0.21/0.50  (r1 zenon_Vka zenon_Vna)
% 0.21/0.50  (zenon_Vyb != zenon_Vdb)
% 0.21/0.50  (zenon_Vxc != zenon_Voc)
% 0.21/0.50  (zenon_Vxd != zenon_Vyc)
% 0.21/0.50  (-. (p1 zenon_Vlb))
% 0.21/0.50  (p1 zenon_Vue)
% 0.21/0.50  (zenon_Vnc != zenon_Voc)
% 0.21/0.50  (zenon_Vue != zenon_Vhb)
% 0.21/0.50  (zenon_Vsc != zenon_Vec)
% 0.21/0.50  (zenon_Vne != zenon_Vhb)
% 0.21/0.50  (zenon_Vdc != zenon_Vdd)
% 0.21/0.50  (zenon_Vyb != zenon_Vza)
% 0.21/0.50  (zenon_Vfe != zenon_Vzb)
% 0.21/0.50  (zenon_Vne != zenon_Vza)
% 0.21/0.50  (zenon_Vsc != zenon_Vvb)
% 0.21/0.50  (zenon_Vne != zenon_Vzb)
% 0.21/0.50  (zenon_Vyb != zenon_Vdd)
% 0.21/0.50  (r1 zenon_Ved zenon_Vfd)
% 0.21/0.50  (zenon_Vnc != zenon_Vec)
% 0.21/0.50  (zenon_Vue != zenon_Vdd)
% 0.21/0.50  (zenon_Vhd != zenon_Vhb)
% 0.21/0.50  (zenon_Vhd != zenon_Vsb)
% 0.21/0.50  (r1 zenon_Vuc zenon_Vzc)
% 0.21/0.50  (zenon_Vtd != zenon_Vna)
% 0.21/0.50  (zenon_Vxc != zenon_Vhb)
% 0.21/0.50  (zenon_Vue != zenon_Vec)
% 0.21/0.50  (r1 zenon_Vwb zenon_Vzb)
% 0.21/0.50  (zenon_Vnc != zenon_Vra)
% 0.21/0.50  (zenon_Vcd != zenon_Vdb)
% 0.21/0.50  (zenon_Vpd != zenon_Vva)
% 0.21/0.50  (zenon_Vic != zenon_Vsb)
% 0.21/0.50  (zenon_Vpd != zenon_Voc)
% 0.21/0.50  (zenon_Vhd != zenon_Vyc)
% 0.21/0.50  (zenon_Vbe != zenon_Vlb)
% 0.21/0.50  (zenon_Vic != zenon_Vvb)
% 0.21/0.50  (p1 zenon_Vre)
% 0.21/0.50  (zenon_Vhd != zenon_Voc)
% 0.21/0.50  (zenon_Vsc != zenon_Vna)
% 0.21/0.50  (zenon_Vbe != zenon_Vjc)
% 0.21/0.50  (r1 Tau_1 zenon_Vvb)
% 0.21/0.50  (zenon_Vfe != zenon_Vlb)
% 0.21/0.50  (-. (p1 zenon_Vna))
% 0.21/0.50  (zenon_Vne != zenon_Vra)
% 0.21/0.50  (zenon_Vnc != zenon_Vvb)
% 0.21/0.50  (zenon_Vpd != zenon_Vvb)
% 0.21/0.50  (p1 zenon_Vdc)
% 0.21/0.50  (zenon_Vub != zenon_Vdb)
% 0.21/0.50  (zenon_Vre != zenon_Vva)
% 0.21/0.50  (zenon_Vre != zenon_Vjc)
% 0.21/0.50  (zenon_Vnc != zenon_Vjc)
% 0.21/0.50  (zenon_Vdc != zenon_Vec)
% 0.21/0.50  (r1 zenon_Vge zenon_Vje)
% 0.21/0.50  (zenon_Vfe != zenon_Vza)
% 0.21/0.50  (zenon_Vre != zenon_Vlb)
% 0.21/0.50  (zenon_Vub != zenon_Vzb)
% 0.21/0.50  (-. (p1 zenon_Vzb))
% 0.21/0.50  (p1 zenon_Vxd)
% 0.21/0.50  (zenon_Vne != zenon_Vid)
% 0.21/0.50  (r1 zenon_Vfd zenon_Vgd)
% 0.21/0.50  (-. (p1 zenon_Vdd))
% 0.21/0.50  (zenon_Vdc != zenon_Vvb)
% 0.21/0.50  (zenon_Vcd != zenon_Vzb)
% 0.21/0.50  (zenon_Vcd != zenon_Vyc)
% 0.21/0.50  (-. (p1 zenon_Vpb))
% 0.21/0.50  (zenon_Vxc != zenon_Vvb)
% 0.21/0.50  (zenon_Vbe != zenon_Vpb)
% 0.21/0.50  (p1 zenon_Vnc)
% 0.21/0.50  (r1 zenon_Vgc zenon_Vhc)
% 0.21/0.50  (zenon_Vbe != zenon_Vid)
% 0.21/0.50  (zenon_Vfe != zenon_Vyc)
% 0.21/0.50  (zenon_Vnc != zenon_Vva)
% 0.21/0.50  (zenon_Vxd != zenon_Vra)
% 0.21/0.50  (r1 zenon_Vt zenon_Via)
% 0.21/0.50  (r1 Tau_0 Tau_2)
% 0.21/0.50  (zenon_Vxc != zenon_Vec)
% 0.21/0.50  (zenon_Vje != zenon_Vdb)
% 0.21/0.50  (-. (p2 zenon_Vja))
% 0.21/0.50  (zenon_Vtd != zenon_Vtc)
% 0.21/0.50  (zenon_Vfe != zenon_Vec)
% 0.21/0.50  (r1 zenon_Vmd zenon_Vpd)
% 0.21/0.50  (zenon_Vnc != zenon_Vhb)
% 0.21/0.50  (zenon_Vre != zenon_Vpb)
% 0.21/0.50  (-. (p1 zenon_Vhb))
% 0.21/0.50  (zenon_Vub != zenon_Vhb)
% 0.21/0.50  (zenon_Vub != zenon_Voc)
% 0.21/0.50  (r1 zenon_Vke zenon_Vne)
% 0.21/0.50  (zenon_Vic != zenon_Vjc)
% 0.21/0.50  (zenon_Vub != zenon_Vec)
% 0.21/0.50  (zenon_Vre != zenon_Vyc)
% 0.21/0.50  (zenon_Vnc != zenon_Vtc)
% 0.21/0.50  (p1 zenon_Vxc)
% 0.21/0.50  (zenon_Vbe != zenon_Vdd)
% 0.21/0.50  (r1 zenon_Vac zenon_Vbc)
% 0.21/0.50  (zenon_Vxc != zenon_Vva)
% 0.21/0.50  (r1 zenon_Vgc zenon_Vjc)
% 0.21/0.50  (r1 zenon_Voa zenon_Vra)
% 0.21/0.50  (zenon_Vfe != zenon_Vhb)
% 0.21/0.50  (zenon_Vub != zenon_Vza)
% 0.21/0.50  (zenon_Vnc != zenon_Vpb)
% 0.21/0.50  (p1 zenon_Vhd)
% 0.21/0.50  (zenon_Vhd != zenon_Vna)
% 0.21/0.50  (zenon_Vcd != zenon_Vza)
% 0.21/0.50  (zenon_Vsc != zenon_Vyc)
% 0.21/0.50  (zenon_Vub != zenon_Vlb)
% 0.21/0.50  (r1 zenon_Vqc zenon_Vrc)
% 0.21/0.50  (zenon_Vne != zenon_Vec)
% 0.21/0.50  (zenon_Vnc != zenon_Vzb)
% 0.21/0.50  (zenon_Vfe != zenon_Vtc)
% 0.21/0.50  (zenon_Vxd != zenon_Vec)
% 0.21/0.50  (zenon_Vje != zenon_Vvb)
% 0.21/0.50  (zenon_Vxd != zenon_Vhb)
% 0.21/0.50  (r1 zenon_Vfd zenon_Vid)
% 0.21/0.50  (p1 zenon_Vtd)
% 0.21/0.50  (zenon_Vhd != zenon_Vlb)
% 0.21/0.50  (zenon_Vje != zenon_Vhb)
% 0.21/0.50  (zenon_Vtd != zenon_Voc)
% 0.21/0.50  (zenon_Vre != zenon_Vtc)
% 0.21/0.50  (zenon_Vje != zenon_Vpb)
% 0.21/0.50  (zenon_Vnc != zenon_Vza)
% 0.21/0.50  (zenon_Vub != zenon_Vyc)
% 0.21/0.50  (r1 zenon_Vzc zenon_Vad)
% 0.21/0.50  (zenon_Vsc != zenon_Vdb)
% 0.21/0.50  (zenon_Vre != zenon_Vhb)
% 0.21/0.50  (zenon_Vpd != zenon_Vza)
% 0.21/0.50  (zenon_Vue != zenon_Vjc)
% 0.21/0.50  (zenon_Vue != zenon_Vra)
% 0.21/0.50  (zenon_Vne != zenon_Vna)
% 0.21/0.50  (zenon_Vxc != zenon_Vsb)
% 0.21/0.50  (r1 zenon_Vwa zenon_Vza)
% 0.21/0.50  (zenon_Vyb != zenon_Vva)
% 0.21/0.50  (zenon_Vxc != zenon_Vdb)
% 0.21/0.50  (r1 zenon_Vsa zenon_Vva)
% 0.21/0.50  (zenon_Vre != zenon_Vec)
% 0.21/0.50  (zenon_Vtd != zenon_Vsb)
% 0.21/0.50  (zenon_Vsc != zenon_Vid)
% 0.21/0.50  (zenon_Vic != zenon_Vdb)
% 0.21/0.50  (zenon_Vsc != zenon_Vzb)
% 0.21/0.50  (zenon_Vtd != zenon_Vpb)
% 0.21/0.50  (zenon_Vbe != zenon_Vsb)
% 0.21/0.50  (zenon_Vxd != zenon_Vdd)
% 0.21/0.50  (p1 zenon_Vcd)
% 0.21/0.50  (zenon_Vbe != zenon_Vna)
% 0.21/0.50  (zenon_Vyb != zenon_Vec)
% 0.21/0.50  (zenon_Vre != zenon_Vra)
% 0.21/0.50  (zenon_Vue != zenon_Vzb)
% 0.21/0.50  (zenon_Vic != zenon_Vpb)
% 0.21/0.50  (zenon_Vpd != zenon_Vlb)
% 0.21/0.50  (r1 zenon_Vbc zenon_Vcc)
% 0.21/0.50  (zenon_Vub != zenon_Vsb)
% 0.21/0.50  (zenon_Vcd != zenon_Vva)
% 0.21/0.50  (zenon_Vdc != zenon_Vtc)
% 0.21/0.50  (r1 zenon_Veb zenon_Vhb)
% 0.21/0.50  (zenon_Vxc != zenon_Vra)
% 0.21/0.50  (zenon_Vfe != zenon_Vna)
% 0.21/0.50  (zenon_Vbe != zenon_Vvb)
% 0.21/0.50  (zenon_Vdc != zenon_Vdb)
% 0.21/0.50  (zenon_Vcd != zenon_Voc)
% 0.21/0.50  (zenon_Vfe != zenon_Vid)
% 0.21/0.50  (zenon_Vsc != zenon_Vsb)
% 0.21/0.50  (zenon_Vsc != zenon_Vjc)
% 0.21/0.50  (zenon_Vcd != zenon_Vdd)
% 0.21/0.50  (zenon_Vxc != zenon_Vza)
% 0.21/0.50  (-. (p2 zenon_Vld))
% 0.21/0.50  (zenon_Vxd != zenon_Voc)
% 0.21/0.50  (-. (p1 zenon_Vza))
% 0.21/0.50  (zenon_Vdc != zenon_Vza)
% 0.21/0.50  (zenon_Vdc != zenon_Voc)
% 0.21/0.50  (zenon_Vue != zenon_Vlb)
% 0.21/0.50  (zenon_Vxd != zenon_Vva)
% 0.21/0.50  (zenon_Vxc != zenon_Vna)
% 0.21/0.50  (zenon_Vub != zenon_Vvb)
% 0.21/0.50  (zenon_Vfe != zenon_Vpb)
% 0.21/0.50  (-. (p2 zenon_Vfa))
% 0.21/0.50  (zenon_Vtd != zenon_Vzb)
% 0.21/0.50  (r1 zenon_Vqd zenon_Vtd)
% 0.21/0.50  (zenon_Vhd != zenon_Vza)
% 0.21/0.50  (zenon_Vdc != zenon_Vhb)
% 0.21/0.50  (zenon_Vtd != zenon_Vza)
% 0.21/0.50  (zenon_Vub != zenon_Vra)
% 0.21/0.50  (zenon_Vyb != zenon_Vzb)
% 0.21/0.50  (zenon_Vsc != zenon_Vza)
% 0.21/0.50  (zenon_Vhd != zenon_Vjc)
% 0.21/0.50  (r1 zenon_Vlc zenon_Vmc)
% 0.21/0.50  (zenon_Vpd != zenon_Vhb)
% 0.21/0.50  (r1 zenon_Voe zenon_Vre)
% 0.21/0.50  (r1 zenon_Vt zenon_Vea)
% 0.21/0.50  (zenon_Vic != zenon_Vdd)
% 0.21/0.50  (zenon_Vhd != zenon_Vvb)
% 0.21/0.50  (r1 zenon_Vfc zenon_Vkc)
% 0.21/0.50  (r1 zenon_X5 zenon_Vsb)
% 0.21/0.50  (zenon_Vbe != zenon_Vhb)
% 0.21/0.50  (zenon_Vcd != zenon_Vid)
% 0.21/0.50  (zenon_Vub != zenon_Vjc)
% 0.21/0.50  (-. (p1 zenon_Vec))
% 0.21/0.50  (zenon_Vnc != zenon_Vid)
% 0.21/0.50  (zenon_Vxc != zenon_Vjc)
% 0.21/0.50  (zenon_Vje != zenon_Vva)
% 0.21/0.50  (zenon_Vtd != zenon_Vdb)
% 0.21/0.50  (zenon_Vre != zenon_Vid)
% 0.21/0.50  (r1 zenon_Vx zenon_Vy)
% 0.21/0.50  (zenon_Vtd != zenon_Vjc)
% 0.21/0.50  (zenon_Vub != zenon_Vna)
% 0.21/0.50  (zenon_Vyb != zenon_Vpb)
% 0.21/0.50  (zenon_Vhd != zenon_Vdd)
% 0.21/0.50  (zenon_Vsc != zenon_Vhb)
% 0.21/0.50  (zenon_Vfe != zenon_Voc)
% 0.21/0.50  (zenon_Vhd != zenon_Vdb)
% 0.21/0.50  (zenon_Vdc != zenon_Vra)
% 0.21/0.50  (zenon_Vne != zenon_Vjc)
% 0.21/0.50  (zenon_Vue != zenon_Vpb)
% 0.21/0.50  (p1 zenon_Vbe)
% 0.21/0.50  (zenon_Vxd != zenon_Vza)
% 0.21/0.50  (zenon_Vne != zenon_Vdd)
% 0.21/0.50  (zenon_Vje != zenon_Vtc)
% 0.21/0.50  (-. (p1 zenon_Vjc))
% 0.21/0.50  (zenon_Vic != zenon_Vva)
% 0.21/0.50  (zenon_Vue != zenon_Vid)
% 0.21/0.50  (zenon_Vdc != zenon_Vpb)
% 0.21/0.50  (zenon_Vnc != zenon_Vyc)
% 0.21/0.50  (zenon_Vxd != zenon_Vjc)
% 0.21/0.50  (r1 zenon_Vkc zenon_Vpc)
% 0.21/0.50  (zenon_Vre != zenon_Vza)
% 0.21/0.50  (zenon_Vue != zenon_Vsb)
% 0.21/0.50  (zenon_Vcd != zenon_Vec)
% 0.21/0.50  (zenon_Vyb != zenon_Vna)
% 0.21/0.50  (zenon_Vpd != zenon_Vdd)
% 0.21/0.50  (zenon_Vdc != zenon_Vjc)
% 0.21/0.50  (zenon_Vfe != zenon_Vva)
% 0.21/0.50  (zenon_Vje != zenon_Vyc)
% 0.21/0.50  (zenon_Vdc != zenon_Vsb)
% 0.21/0.50  (zenon_Vdc != zenon_Vzb)
% 0.21/0.50  (zenon_Vxd != zenon_Vtc)
% 0.21/0.50  (zenon_Vje != zenon_Vjc)
% 0.21/0.50  (zenon_Vcd != zenon_Vpb)
% 0.21/0.50  (r1 zenon_Vlc zenon_Voc)
% 0.21/0.50  (-. (p1 zenon_Vvb))
% 0.21/0.50  (zenon_Vpd != zenon_Vyc)
% 0.21/0.50  (zenon_Vue != zenon_Vvb)
% 0.21/0.50  (zenon_Vxd != zenon_Vsb)
% 0.21/0.50  (zenon_Vcd != zenon_Vhb)
% 0.21/0.50  (zenon_Vue != zenon_Vtc)
% 0.21/0.50  (zenon_Vdc != zenon_Vid)
% 0.21/0.50  (zenon_Vpd != zenon_Vec)
% 0.21/0.50  (p1 zenon_Vsc)
% 0.21/0.50  (zenon_Vic != zenon_Vid)
% 0.21/0.50  (zenon_Vxd != zenon_Vvb)
% 0.21/0.50  (zenon_Vbe != zenon_Vva)
% 0.21/0.50  (r1 zenon_X6 zenon_Vue)
% 0.21/0.50  (zenon_Vic != zenon_Voc)
% 0.21/0.50  (zenon_Vtd != zenon_Vdd)
% 0.21/0.50  (zenon_Vcd != zenon_Vjc)
% 0.21/0.50  (r1 Tau_0 Tau_1)
% 0.21/0.50  (zenon_Vre != zenon_Vzb)
% 0.21/0.50  (zenon_Vbe != zenon_Vec)
% 0.21/0.50  (zenon_Vje != zenon_Vid)
% 0.21/0.50  (r1 zenon_Vmb zenon_Vpb)
% 0.21/0.50  (zenon_Vic != zenon_Vzb)
% 0.21/0.50  (zenon_Vnc != zenon_Vsb)
% 0.21/0.50  (zenon_Vxd != zenon_Vna)
% 0.21/0.50  (-. (p2 zenon_Vz))
% 0.21/0.50  (zenon_Vcd != zenon_Vsb)
% 0.21/0.50  (zenon_Vpd != zenon_Vsb)
% 0.21/0.50  (zenon_Vyb != zenon_Vyc)
% 0.21/0.50  (zenon_Vje != zenon_Vsb)
% 0.21/0.50  (r1 zenon_Vqc zenon_Vtc)
% 0.21/0.50  (p1 zenon_Vic)
% 0.21/0.50  (p1 zenon_Vje)
% 0.21/0.50  (r1 zenon_Vad zenon_Vdd)
% 0.21/0.50  (zenon_Vre != zenon_Vvb)
% 0.21/0.50  (zenon_Vtd != zenon_Vlb)
% 0.21/0.50  (zenon_Vne != zenon_Vyc)
% 0.21/0.50  (zenon_Vub != zenon_Vdd)
% 0.21/0.50  (zenon_Vsc != zenon_Vra)
% 0.21/0.50  (zenon_Vbe != zenon_Vdb)
% 0.21/0.50  (zenon_Vpd != zenon_Vid)
% 0.21/0.50  (zenon_Vje != zenon_Vna)
% 0.21/0.50  (zenon_Vic != zenon_Vhb)
% 0.21/0.50  (zenon_Vxc != zenon_Vzb)
% 0.21/0.50  (zenon_Vub != zenon_Vid)
% 0.21/0.50  (zenon_Vtd != zenon_Vhb)
% 0.21/0.50  (zenon_Vxd != zenon_Vpb)
% 0.21/0.50  (zenon_Vre != zenon_Vna)
% 0.21/0.50  (zenon_Vhd != zenon_Vva)
% 0.21/0.50  (zenon_Vsc != zenon_Vdd)
% 0.21/0.50  (zenon_Vhd != zenon_Vra)
% 0.21/0.50  (zenon_Vyb != zenon_Vhb)
% 0.21/0.50  (zenon_Vsc != zenon_Vtc)
% 0.21/0.50  (zenon_Vyb != zenon_Vjc)
% 0.21/0.50  (zenon_Vje != zenon_Voc)
% 0.21/0.50  (zenon_Vxd != zenon_Vzb)
% 0.21/0.50  (zenon_Vbe != zenon_Vza)
% 0.21/0.50  (-. (p1 zenon_Vtc))
% 0.21/0.50  (zenon_Vje != zenon_Vzb)
% 0.21/0.50  (r1 zenon_Vwb zenon_Vxb)
% 0.21/0.50  (r1 zenon_Vkd zenon_Vld)
% 0.21/0.50  (r1 zenon_Vud zenon_Vxd)
% 0.21/0.50  (zenon_Vhd != zenon_Vzb)
% 0.21/0.50  (zenon_Vne != zenon_Vva)
% 0.21/0.50  (-. (p1 zenon_Voc))
% 0.21/0.50  (zenon_Vpd != zenon_Vjc)
% 0.21/0.50  (zenon_Vtd != zenon_Vec)
% 0.21/0.50  (-. (p1 zenon_Vid))
% 0.21/0.50  (zenon_Vnc != zenon_Vlb)
% 0.21/0.50  (r1 zenon_Vvc zenon_Vyc)
% 0.21/0.50  (-. (p1 zenon_Vra))
% 0.21/0.50  (r1 zenon_Vyd zenon_Vbe)
% 0.21/0.50  (zenon_Vyb != zenon_Vlb)
% 0.21/0.50  (zenon_Vyb != zenon_Vtc)
% 0.21/0.50  (r1 zenon_Vpc zenon_Vuc)
% 0.21/0.50  (r1 zenon_Vac zenon_Vfc)
% 0.21/0.50  (p1 zenon_Vne)
% 0.21/0.50  (zenon_Vpd != zenon_Vpb)
% 0.21/0.50  (zenon_Vic != zenon_Vna)
% 0.21/0.50  (r1 Tau_1 zenon_Vtb)
% 0.21/0.50  (-. (p4 zenon_X3))
% 0.21/0.50  (zenon_Vhd != zenon_Vid)
% 0.21/0.50  (zenon_Vtd != zenon_Vid)
% 0.21/0.50  (zenon_Vue != zenon_Vna)
% 0.21/0.50  (zenon_Vpd != zenon_Vra)
% 0.21/0.50  (r1 zenon_Vvc zenon_Vwc)
% 0.21/0.50  (zenon_Vxc != zenon_Vpb)
% 0.21/0.51  (zenon_Vne != zenon_Voc)
% 0.21/0.51  (r1 zenon_Vfc zenon_Vgc)
% 0.21/0.51  (p1 zenon_Vfe)
% 0.21/0.51  (zenon_Vcd != zenon_Vra)
% 0.21/0.51  (zenon_Vhd != zenon_Vpb)
% 0.21/0.51  (zenon_Vre != zenon_Voc)
% 0.21/0.51  (r1 Tau_2 zenon_Vwb)
% 0.21/0.51  (r1 Tau_2 zenon_Vac)
% 0.21/0.51  (zenon_Vue != zenon_Vyc)
% 0.21/0.51  (zenon_Vue != zenon_Voc)
% 0.21/0.51  (zenon_Vfe != zenon_Vdd)
% 0.21/0.51  (r1 zenon_Vad zenon_Vbd)
% 0.21/0.51  (zenon_Vxc != zenon_Vid)
% 0.21/0.51  (zenon_Vcd != zenon_Vtc)
% 0.21/0.51  (zenon_Vxc != zenon_Vdd)
% 0.21/0.51  (zenon_Vdc != zenon_Vva)
% 0.21/0.51  (zenon_Vfe != zenon_Vjc)
% 0.21/0.51  (zenon_Vne != zenon_Vvb)
% 0.21/0.51  (zenon_Vpd != zenon_Vdb)
% 0.21/0.51  (zenon_Vhd != zenon_Vtc)
% 0.21/0.51  (zenon_Vne != zenon_Vpb)
% 0.21/0.51  (zenon_Vhd != zenon_Vec)
% 0.21/0.51  (zenon_Vcd != zenon_Vlb)
% 0.21/0.51  (zenon_Vxd != zenon_Vdb)
% 0.21/0.51  (zenon_Vue != zenon_Vva)
% 0.21/0.51  (zenon_Vfe != zenon_Vvb)
% 0.21/0.51  (-. (p1 zenon_Vsb))
% 0.21/0.51  (r1 zenon_Vce zenon_Vfe)
% 0.21/0.51  (r1 zenon_Vkc zenon_Vlc)
% 0.21/0.51  (zenon_Vyb != zenon_Vra)
% 0.21/0.51  (zenon_Vbe != zenon_Vyc)
% 0.21/0.51  (zenon_Vub != zenon_Vpb)
% 0.21/0.51  (zenon_Vxd != zenon_Vlb)
% 0.21/0.51  (zenon_Vcd != zenon_Vna)
% 0.21/0.51  (zenon_Vbe != zenon_Vra)
% 0.21/0.51  (zenon_Vdc != zenon_Vna)
% 0.21/0.51  (zenon_Vsc != zenon_Voc)
% 0.21/0.51  (zenon_Vue != zenon_Vza)
% 0.21/0.51  (zenon_Vdc != zenon_Vyc)
% 0.21/0.51  (zenon_Vbe != zenon_Vtc)
% 0.21/0.51  (zenon_Vic != zenon_Vyc)
% 0.21/0.51  (zenon_Vnc != zenon_Vna)
% 0.21/0.51  (zenon_Vje != zenon_Vlb)
% 0.21/0.51  (zenon_Vxd != zenon_Vid)
% 0.21/0.51  (zenon_Vub != zenon_Vva)
% 0.21/0.51  (zenon_Vnc != zenon_Vdd)
% 0.21/0.51  (zenon_Vxc != zenon_Vlb)
% 0.21/0.51  (zenon_Vre != zenon_Vsb)
% 0.21/0.51  (zenon_Vic != zenon_Vlb)
% 0.21/0.51  (zenon_Vtd != zenon_Vyc)
% 0.21/0.51  (zenon_Vfe != zenon_Vra)
% 0.21/0.51  (zenon_Vxc != zenon_Vtc)
% 0.21/0.51  (zenon_Vne != zenon_Vdb)
% 0.21/0.51  (r1 zenon_Vuc zenon_Vvc)
% 0.21/0.51  (r1 zenon_Vzc zenon_Ved)
% 0.21/0.51  (zenon_Vub != zenon_Vtc)
% 0.21/0.51  (zenon_Vtd != zenon_Vra)
% 0.21/0.51  (zenon_Vpd != zenon_Vna)
% 0.21/0.51  (zenon_Vnc != zenon_Vdb)
% 0.21/0.51  (zenon_Vsc != zenon_Vva)
% 0.21/0.51  (zenon_Vxc != zenon_Vyc)
% 0.21/0.51  (zenon_Vje != zenon_Vra)
% 0.21/0.51  (p1 zenon_Vyb)
% 0.21/0.51  (zenon_Vre != zenon_Vdb)
% 0.21/0.51  (zenon_Vbe != zenon_Voc)
% 0.21/0.51  (zenon_Vbe != zenon_Vzb)
% 0.21/0.51  (zenon_Vic != zenon_Vtc)
% 0.21/0.51  (r1 zenon_Vbc zenon_Vec)
% 0.21/0.51  (zenon_Vpd != zenon_Vtc)
% 0.21/0.51  (zenon_Vne != zenon_Vtc)
% 0.21/0.51  (zenon_Vje != zenon_Vza)
% 0.21/0.51  (zenon_Vdc != zenon_Vlb)
% 0.21/0.51  (zenon_Vyb != zenon_Vsb)
% 0.21/0.51  (zenon_Vyb != zenon_Vvb)
% 0.21/0.51  (zenon_Vfe != zenon_Vsb)
% 0.21/0.51  (zenon_Vic != zenon_Vra)
% 0.21/0.51  (r1 zenon_Vpc zenon_Vqc)
% 0.21/0.51  (zenon_Vje != zenon_Vdd)
% 0.21/0.51  (zenon_Vne != zenon_Vsb)
% 0.21/0.51  (zenon_Vsc != zenon_Vpb)
% 0.21/0.51  (zenon_Vyb != zenon_Voc)
% 0.21/0.51  (zenon_Vre != zenon_Vdd)
% 0.21/0.51  (-. (p1 zenon_Vva))
% 0.21/0.51  (r1 zenon_Ved zenon_Vjd)
% 0.21/0.51  (p1 zenon_Vpd)
% 0.21/0.51  (zenon_Vne != zenon_Vlb)
% 0.21/0.51  (zenon_Vfe != zenon_Vdb)
% 0.21/0.51  *)
% 0.21/0.51  (* NO-PROOF *)
% 0.21/0.51  % SZS status GaveUp
% 0.21/0.51  Number of rewrites on terms: 0
% 0.21/0.51  Number of rewrites on props: 0
% 0.21/0.51  nodes searched: 620
% 0.21/0.51  max branch formulas: 718
% 0.21/0.51  proof nodes created: 0
% 0.21/0.51  formulas created: 3601
% 0.21/0.51  
%------------------------------------------------------------------------------