%------------------------------------------------------------------------------ % File : ZenonModulo---0.5.0 % Problem : LCL646+1.010 : TPTP v9.3.1. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : run_zenon_modulo %d %s % Computer : n009.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:14 PM UTC 2026 % Result : Unknown 19.63s 19.98s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LCL646+1.010 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.03 % Command : run_zenon_modulo %d %s % 0.07/0.34 % Computer : n009.cluster.edu % 0.07/0.34 % Model : x86_64 x86_64 % 0.07/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.34 % Memory : 8046.5625MB % 0.07/0.34 % OS : Linux 6.8.0-71-generic % 0.07/0.34 % CPULimit : 300 % 0.07/0.34 % WCLimit : 300 % 0.07/0.34 % DateTime : Fri Sep 4 23:52:51 UTC 2026 % 0.07/0.34 % CPUTime : % 19.63/19.97 Zenon error: exhausted search space without finding a proof % 19.63/19.97 (* Current branch: % 19.63/19.97 (p6 zenon_X137) % 19.63/19.97 (p6 zenon_Vii) % 19.63/19.97 (zenon_Vst != zenon_Vwba) % 19.63/19.97 (zenon_Vyaa != zenon_Vuba) % 19.63/19.97 (p2 zenon_Veq) % 19.63/19.97 (zenon_Veba != zenon_Vyba) % 19.63/19.97 (zenon_Vly != zenon_Vyba) % 19.63/19.97 (zenon_Vir != zenon_Vsba) % 19.63/19.97 (zenon_Vdy != zenon_Vtba) % 19.63/19.97 (p3 zenon_Vhy) % 19.63/19.97 (zenon_X149 != zenon_Vwba) % 19.63/19.97 (p3 zenon_Vbw) % 19.63/19.97 (zenon_Vzn != zenon_Vxba) % 19.63/19.97 (p1 zenon_Vsq) % 19.63/19.97 (zenon_Vsw != zenon_Vwba) % 19.63/19.97 (zenon_Vlm != zenon_Vwba) % 19.63/19.97 (p1 zenon_Vdz) % 19.63/19.97 (zenon_Vwv != zenon_Vtba) % 19.63/19.97 (p1 zenon_Vlm) % 19.63/19.97 (p1 zenon_Vmba) % 19.63/19.97 (p5 zenon_Vnj) % 19.63/19.97 (zenon_Vsn != zenon_Vxba) % 19.63/19.97 (zenon_Voba != zenon_Vwba) % 19.63/19.97 (zenon_Vvba != zenon_Vsba) % 19.63/19.97 (Tau_2 != Tau_0) % 19.63/19.97 (r1 Tau_0 Tau_2) % 19.63/19.97 (p3 zenon_X146) % 19.63/19.97 (p4 zenon_X133) % 19.63/19.97 (p6 zenon_Vu) % 19.63/19.97 (zenon_Vcg != zenon_Vtba) % 19.63/19.97 (zenon_Vwaa != zenon_Vxba) % 19.63/19.97 (p2 zenon_Vqu) % 19.63/19.97 (zenon_Vhy != zenon_Vyba) % 19.63/19.97 (p6 zenon_Vev) % 19.63/19.97 (r1 Tau_4 zenon_Vyba) % 19.63/19.97 (-. (r1 Tau_0 zenon_Vsba)) % 19.63/19.97 (Tau_3 != zenon_Vwba) % 19.63/19.97 (p5 zenon_X143) % 19.63/19.97 (zenon_X143 != zenon_Vxba) % 19.63/19.97 (p2 zenon_Vec) % 19.63/19.97 (-. (r1 Tau_0 zenon_Vyba)) % 19.63/19.97 (zenon_Vur != zenon_Vuba) % 19.63/19.97 (zenon_Vgba != zenon_Vvba) % 19.63/19.97 (zenon_Vdy != zenon_Vvba) % 19.63/19.97 (zenon_Vsz != zenon_Vsba) % 19.63/19.97 (r1 Tau_0 Tau_4) % 19.63/19.97 (zenon_Vbaa != zenon_Vyba) % 19.63/19.97 (Tau_2 != zenon_Vxba) % 19.63/19.97 (-. (p2 Tau_3)) % 19.63/19.97 (zenon_Vgba != zenon_Vtba) % 19.63/19.97 (zenon_Vur != zenon_Vsba) % 19.63/19.97 (Tau_1 != zenon_Vtba) % 19.63/19.97 (zenon_Vlg != zenon_Vyba) % 19.63/19.97 (p1 zenon_Vqba) % 19.63/19.97 (zenon_X143 != zenon_Vsba) % 19.63/19.97 (zenon_Vxba != zenon_Vtba) % 19.63/19.97 (p5 zenon_Vyaa) % 19.63/19.97 (zenon_Vlx != zenon_Vuba) % 19.63/19.97 (Tau_3 != zenon_Vsba) % 19.63/19.97 (p5 zenon_Vde) % 19.63/19.97 (zenon_Vda != zenon_Vwba) % 19.63/19.97 (p3 zenon_Vbaa) % 19.63/19.97 (p5 zenon_Vtx) % 19.63/19.97 (p1 zenon_Voba) % 19.63/19.97 (r1 Tau_0 Tau_1) % 19.63/19.97 (p6 zenon_Vxq) % 19.63/19.97 (p2 zenon_Vro) % 19.63/19.97 (-. (p3 zenon_Vyba)) % 19.63/19.97 (zenon_Vxba != zenon_Vyba) % 19.63/19.97 (Tau_4 != Tau_0) % 19.63/19.97 (zenon_Vtba != zenon_Vsba) % 19.63/19.97 (zenon_Vvy != zenon_Vwba) % 19.63/19.97 (zenon_Veaa != zenon_Vvba) % 19.63/19.97 (zenon_Vcg != zenon_Vyba) % 19.63/19.97 (zenon_Vsz != zenon_Vuba) % 19.63/19.97 (zenon_Vbi != zenon_Vwba) % 19.63/19.97 (zenon_Vtx != zenon_Vxba) % 19.63/19.97 (zenon_Vxi != zenon_Vuba) % 19.63/19.97 (zenon_Vtm != zenon_Vwba) % 19.63/19.97 (p1 zenon_Vxw) % 19.63/19.97 (p6 zenon_Vsp) % 19.63/19.97 (p4 zenon_Vax) % 19.63/19.97 (p4 zenon_Vrv) % 19.63/19.97 (p3 zenon_Vly) % 19.63/19.97 (zenon_Vdm != zenon_Vwba) % 19.63/19.97 (zenon_Vxba != zenon_Vsba) % 19.63/19.97 (Tau_2 != zenon_Vyba) % 19.63/19.97 (p1 zenon_Vsh) % 19.63/19.97 (zenon_Vjk != zenon_Vvba) % 19.63/19.97 (zenon_Vlx != zenon_Vsba) % 19.63/19.97 (zenon_Vyba != zenon_Vuba) % 19.63/19.97 (p4 zenon_Voy) % 19.63/19.97 (r1 Tau_3 zenon_Vwba) % 19.63/19.97 (p3 zenon_Vks) % 19.63/19.97 (zenon_Vly != zenon_Vtba) % 19.63/19.97 (p3 zenon_X145) % 19.63/19.97 (r1 Tau_4 zenon_Vxba) % 19.63/19.97 (p1 zenon_Vnaa) % 19.63/19.97 (zenon_Vhx != zenon_Vxba) % 19.63/19.97 (p6 zenon_Vfw) % 19.63/19.97 (p4 zenon_Vma) % 19.63/19.97 (zenon_Vme != zenon_Vsba) % 19.63/19.97 (zenon_Vly != zenon_Vvba) % 19.63/19.97 (zenon_Vyt != zenon_Vwba) % 19.63/19.97 (Tau_4 != zenon_Vvba) % 19.63/19.97 (zenon_Vvl != zenon_Vwba) % 19.63/19.97 (zenon_Vwba != zenon_Vyba) % 19.63/19.97 (zenon_X144 != zenon_Vxba) % 19.63/19.97 (p1 zenon_Vvl) % 19.63/19.97 (zenon_Vde != zenon_Vsba) % 19.63/19.97 (zenon_Vlg != zenon_Vtba) % 19.63/19.97 (zenon_Vws != zenon_Vtba) % 19.63/19.97 (p5 zenon_Vzn) % 19.63/19.97 (zenon_Vtx != zenon_Vuba) % 19.63/19.97 (zenon_Vws != zenon_Vyba) % 19.63/19.97 (zenon_Vor != zenon_Vuba) % 19.63/19.97 (zenon_Vwv != zenon_Vvba) % 19.63/19.97 (p4 zenon_Vmd) % 19.63/19.97 (zenon_Vhx != zenon_Vuba) % 19.63/19.97 (zenon_X144 != Tau_1) % 19.63/19.97 (zenon_Vav != zenon_Vsba) % 19.63/19.97 (zenon_Vpx != zenon_Vxba) % 19.63/19.97 (zenon_X144 != zenon_Vsba) % 19.63/19.97 (p5 zenon_Vme) % 19.63/19.97 (p3 zenon_Vqs) % 19.63/19.97 (p5 zenon_Vhx) % 19.63/19.97 (zenon_Vbw != zenon_Vtba) % 19.63/19.97 (zenon_Vsn != zenon_Vuba) % 19.63/19.97 (zenon_Vsq != zenon_Vwba) % 19.63/19.97 (p6 zenon_Vue) % 19.63/19.97 (p6 zenon_Vvb) % 19.63/19.97 (-. (p5 zenon_Vuba)) % 19.63/19.97 (zenon_Vlq != zenon_Vwba) % 19.63/19.97 (p3 zenon_Vdy) % 19.63/19.97 (-. (r1 Tau_0 zenon_Vwba)) % 19.63/19.97 (p6 zenon_Vbt) % 19.63/19.97 (p2 zenon_Vdx) % 19.63/19.97 (r1 Tau_0 Tau_3) % 19.63/19.97 (p6 zenon_Vdb) % 19.63/19.98 (p2 zenon_Vmb) % 19.63/19.98 (-. (r1 Tau_0 zenon_Vuba)) % 19.63/19.98 (zenon_Vme != zenon_Vuba) % 19.63/19.98 (zenon_Vqs != zenon_Vvba) % 19.63/19.98 (p3 zenon_Vws) % 19.63/19.98 (Tau_4 != zenon_Vwba) % 19.63/19.98 (p2 zenon_Vcr) % 19.63/19.98 (zenon_Vwba != zenon_Vsba) % 19.63/19.98 (zenon_X146 != zenon_Vyba) % 19.63/19.98 (p1 zenon_Vqaa) % 19.63/19.98 (zenon_Vzn != zenon_Vsba) % 19.63/19.98 (-. (p1 zenon_Vwba)) % 19.63/19.98 (p3 zenon_Vcg) % 19.63/19.98 (p3 zenon_Vfp) % 19.63/19.98 (p2 zenon_Vyz) % 19.63/19.98 (zenon_Vzk != zenon_Vtba) % 19.63/19.98 (zenon_Vwaa != zenon_Vuba) % 19.63/19.98 (zenon_Vwv != zenon_Vyba) % 19.63/19.98 (zenon_X145 != zenon_Vyba) % 19.63/19.98 (-. (r1 Tau_0 zenon_Vtba)) % 19.63/19.98 (p1 zenon_X149) % 19.63/19.98 (p1 zenon_Vkba) % 19.63/19.98 (p2 zenon_Vln) % 19.63/19.98 (p2 zenon_Ves) % 19.63/19.98 (zenon_Vdz != zenon_Vwba) % 19.63/19.98 (p4 zenon_X138) % 19.63/19.98 (p6 zenon_Vgaa) % 19.63/19.98 (zenon_Vfp != zenon_Vtba) % 19.63/19.98 (p6 zenon_Vtg) % 19.63/19.98 (p6 zenon_Vmz) % 19.63/19.98 (zenon_Vtx != zenon_Vsba) % 19.63/19.98 (Tau_1 != zenon_Vxba) % 19.63/19.98 (Tau_1 != zenon_Vvba) % 19.63/19.98 (p4 zenon_X128) % 19.63/19.98 (p3 zenon_Vlg) % 19.63/19.98 (-. (p1 Tau_4)) % 19.63/19.98 (p1 zenon_Vzy) % 19.63/19.98 (zenon_Vzk != zenon_Vvba) % 19.63/19.98 (p5 zenon_Vvu) % 19.63/19.98 (zenon_Vkba != zenon_Vwba) % 19.63/19.98 (p3 zenon_Vjk) % 19.63/19.98 (p4 zenon_Vtf) % 19.63/19.98 (zenon_Vbaa != zenon_Vvba) % 19.63/19.98 (Tau_4 != zenon_Vtba) % 19.63/19.98 (zenon_Vbw != zenon_Vyba) % 19.63/19.98 (p1 zenon_Vst) % 19.63/19.98 (zenon_Vuba != zenon_Vsba) % 19.63/19.98 (p3 zenon_Vgba) % 19.63/19.98 (zenon_Vlg != zenon_Vvba) % 19.63/19.98 (p4 zenon_Vhz) % 19.63/19.98 (p1 zenon_Vyt) % 19.63/19.98 (zenon_Vlx != zenon_Vxba) % 19.63/19.98 (zenon_Vvba != zenon_Vuba) % 19.63/19.98 (zenon_Vda != Tau_4) % 19.63/19.98 (zenon_Vsh != Tau_4) % 19.63/19.98 (zenon_Vbi != Tau_4) % 19.63/19.98 (zenon_Vvl != Tau_4) % 19.63/19.98 (zenon_Vdm != Tau_4) % 19.63/19.98 (zenon_Vlm != Tau_4) % 19.63/19.98 (zenon_Vtm != Tau_4) % 19.63/19.98 (zenon_Vlq != Tau_4) % 19.63/19.98 (zenon_Vsq != Tau_4) % 19.63/19.98 (zenon_Vmt != Tau_4) % 19.63/19.98 (zenon_Vst != Tau_4) % 19.63/19.98 (zenon_Vyt != Tau_4) % 19.63/19.98 (zenon_Veu != Tau_4) % 19.63/19.98 (zenon_Vsw != Tau_4) % 19.63/19.98 (zenon_Vxw != Tau_4) % 19.63/19.98 (zenon_Vvy != Tau_4) % 19.63/19.98 (zenon_Vzy != Tau_4) % 19.63/19.98 (zenon_Vdz != Tau_4) % 19.63/19.98 (zenon_Vnaa != Tau_4) % 19.63/19.98 (zenon_Vqaa != Tau_4) % 19.63/19.98 (zenon_Vkba != Tau_4) % 19.63/19.98 (zenon_Vmba != Tau_4) % 19.63/19.98 (zenon_Voba != Tau_4) % 19.63/19.98 (zenon_Vqba != Tau_4) % 19.63/19.98 (p2 zenon_Vbk) % 19.63/19.98 (p6 zenon_Vfz) % 19.63/19.98 (zenon_Vde != zenon_Vuba) % 19.63/19.98 (zenon_Vqaa != zenon_Vwba) % 19.63/19.98 (zenon_Vur != zenon_Vxba) % 19.63/19.98 (p1 zenon_Vdm) % 19.63/19.98 (p5 zenon_Vur) % 19.63/19.98 (p6 zenon_Vuz) % 19.63/19.98 (zenon_Veba != zenon_Vtba) % 19.63/19.98 (p4 zenon_Vmu) % 19.63/19.98 (zenon_Vir != zenon_Vxba) % 19.63/19.98 (Tau_2 != zenon_Vsba) % 19.63/19.98 (p5 zenon_Vfj) % 19.63/19.98 (zenon_Vgba != zenon_Vyba) % 19.63/19.98 (p1 zenon_X148) % 19.63/19.98 (zenon_Vnj != zenon_Vsba) % 19.63/19.98 (p1 zenon_Vsw) % 19.63/19.98 (zenon_Vvu != zenon_Vsba) % 19.63/19.98 (zenon_Vhy != zenon_Vvba) % 19.63/19.98 (p5 zenon_Vor) % 19.63/19.98 (zenon_Vmp != zenon_Vtba) % 19.63/19.98 (zenon_Vyaa != zenon_Vxba) % 19.63/19.98 (zenon_Vrk != zenon_Vyba) % 19.63/19.98 (zenon_Vfj != zenon_Vsba) % 19.63/19.98 (zenon_Vqs != zenon_Vtba) % 19.63/19.98 (Tau_1 != zenon_Vsba) % 19.63/19.98 (zenon_X149 != Tau_4) % 19.63/19.98 (zenon_Vcg != Tau_2) % 19.63/19.98 (zenon_Vlg != Tau_2) % 19.63/19.98 (zenon_Vjk != Tau_2) % 19.63/19.98 (zenon_Vrk != Tau_2) % 19.63/19.98 (zenon_Vzk != Tau_2) % 19.63/19.98 (zenon_Vfp != Tau_2) % 19.63/19.98 (zenon_Vmp != Tau_2) % 19.63/19.98 (zenon_Vks != Tau_2) % 19.63/19.98 (zenon_Vqs != Tau_2) % 19.63/19.98 (zenon_Vws != Tau_2) % 19.63/19.98 (zenon_Vwv != Tau_2) % 19.63/19.98 (zenon_Vbw != Tau_2) % 19.63/19.98 (zenon_Vdy != Tau_2) % 19.63/19.98 (zenon_Vhy != Tau_2) % 19.63/19.98 (zenon_Vly != Tau_2) % 19.63/19.98 (zenon_Vbaa != Tau_2) % 19.63/19.98 (zenon_Veaa != Tau_2) % 19.63/19.98 (zenon_Vcba != Tau_2) % 19.63/19.98 (zenon_Veba != Tau_2) % 19.63/19.98 (zenon_Vgba != Tau_2) % 19.63/19.98 (zenon_Vzy != zenon_Vwba) % 19.63/19.98 (p2 zenon_Vpi) % 19.63/19.98 (zenon_Vpz != zenon_Vuba) % 19.63/19.98 (p5 zenon_X144) % 19.63/19.98 (zenon_Vnaa != zenon_Vwba) % 19.63/19.98 (zenon_Vmt != zenon_Vwba) % 19.63/19.98 (zenon_Vfp != zenon_Vvba) % 19.63/19.98 (zenon_Vzk != zenon_Vyba) % 19.63/19.98 (Tau_4 != zenon_Vxba) % 19.63/19.98 (p5 zenon_Vpx) % 19.63/19.98 (p6 zenon_Vgl) % 19.63/19.98 (zenon_Vvu != zenon_Vxba) % 19.63/19.98 (p5 zenon_Vwaa) % 19.63/19.98 (p2 zenon_Vjz) % 19.63/19.98 (p6 zenon_X127) % 19.63/19.98 (p2 zenon_Vkaa) % 19.63/19.98 (p1 zenon_Vbi) % 19.63/19.98 (zenon_Vwba != zenon_Vvba) % 19.63/19.98 (zenon_X148 != zenon_Vwba) % 19.63/19.98 (zenon_Vmp != zenon_Vyba) % 19.63/19.98 (zenon_X146 != zenon_Vvba) % 19.63/19.98 (zenon_Vyba != zenon_Vvba) % 19.63/19.98 (p6 zenon_Vfo) % 19.63/19.98 (Tau_2 != zenon_Vuba) % 19.63/19.98 (p6 zenon_Vzm) % 19.63/19.98 (Tau_3 != zenon_Vyba) % 19.63/19.98 (p2 zenon_Vry) % 19.63/19.98 (zenon_Vcg != zenon_Vvba) % 19.63/19.98 (zenon_Veu != zenon_Vwba) % 19.63/19.98 (p5 zenon_Vlx) % 19.63/19.98 (zenon_Vjk != zenon_Vyba) % 19.63/19.98 (-. (r1 Tau_0 zenon_Vvba)) % 19.63/19.98 (zenon_X146 != Tau_2) % 19.63/19.98 (Tau_2 != zenon_Vvba) % 19.63/19.98 (zenon_Vpx != zenon_Vsba) % 19.63/19.98 (Tau_2 != zenon_Vwba) % 19.63/19.98 (zenon_Vhy != zenon_Vtba) % 19.63/19.98 (zenon_Vmba != zenon_Vwba) % 19.63/19.98 (zenon_X147 != Tau_3) % 19.63/19.98 (zenon_Vrk != zenon_Vvba) % 19.63/19.98 (Tau_3 != Tau_0) % 19.63/19.98 (p4 zenon_Vjw) % 19.63/19.98 (zenon_Vva != Tau_3) % 19.63/19.98 (zenon_Vmb != Tau_3) % 19.63/19.98 (zenon_Vec != Tau_3) % 19.63/19.98 (zenon_Vwc != Tau_3) % 19.63/19.98 (zenon_Vud != Tau_3) % 19.63/19.98 (zenon_Vkf != Tau_3) % 19.63/19.98 (zenon_Vjh != Tau_3) % 19.63/19.98 (zenon_Vpi != Tau_3) % 19.63/19.98 (zenon_Vbk != Tau_3) % 19.63/19.98 (zenon_Vnl != Tau_3) % 19.63/19.98 (zenon_Vln != Tau_3) % 19.63/19.98 (zenon_Vro != Tau_3) % 19.63/19.98 (zenon_Veq != Tau_3) % 19.63/19.98 (zenon_Vcr != Tau_3) % 19.63/19.98 (zenon_Ves != Tau_3) % 19.63/19.98 (zenon_Vgt != Tau_3) % 19.63/19.98 (zenon_Vqu != Tau_3) % 19.63/19.98 (zenon_Vmv != Tau_3) % 19.63/19.98 (zenon_Vnw != Tau_3) % 19.63/19.98 (zenon_Vdx != Tau_3) % 19.63/19.98 (zenon_Vzx != Tau_3) % 19.63/19.98 (zenon_Vry != Tau_3) % 19.63/19.98 (zenon_Vjz != Tau_3) % 19.63/19.98 (zenon_Vyz != Tau_3) % 19.63/19.98 (zenon_Vkaa != Tau_3) % 19.63/19.98 (-. (p3 zenon_Vvba)) % 19.63/19.98 (Tau_1 != zenon_Vwba) % 19.63/19.98 (-. (p5 zenon_Vsba)) % 19.63/19.98 (p6 zenon_X132) % 19.63/19.98 (zenon_X143 != zenon_Vuba) % 19.63/19.98 (zenon_Vde != Tau_1) % 19.63/19.98 (zenon_Vme != Tau_1) % 19.63/19.98 (zenon_Vxi != Tau_1) % 19.63/19.98 (zenon_Vfj != Tau_1) % 19.63/19.98 (zenon_Vnj != Tau_1) % 19.63/19.98 (zenon_Vsn != Tau_1) % 19.63/19.98 (zenon_Vzn != Tau_1) % 19.63/19.98 (zenon_Vir != Tau_1) % 19.63/19.98 (zenon_Vor != Tau_1) % 19.63/19.98 (zenon_Vur != Tau_1) % 19.63/19.98 (zenon_Vvu != Tau_1) % 19.63/19.98 (zenon_Vav != Tau_1) % 19.63/19.98 (zenon_Vhx != Tau_1) % 19.63/19.98 (zenon_Vlx != Tau_1) % 19.63/19.98 (zenon_Vpx != Tau_1) % 19.63/19.98 (zenon_Vtx != Tau_1) % 19.63/19.98 (zenon_Vpz != Tau_1) % 19.63/19.98 (zenon_Vsz != Tau_1) % 19.63/19.98 (zenon_Vuaa != Tau_1) % 19.63/19.98 (zenon_Vwaa != Tau_1) % 19.63/19.98 (zenon_Vyaa != Tau_1) % 19.63/19.98 (p3 zenon_Vrk) % 19.63/19.98 (p5 zenon_Vsn) % 19.63/19.98 (p1 zenon_Vda) % 19.63/19.98 (p3 zenon_Vzk) % 19.63/19.98 (r1 Tau_2 zenon_Vuba) % 19.63/19.98 (zenon_Vnj != zenon_Vuba) % 19.63/19.98 (p4 zenon_Vlo) % 19.63/19.98 (Tau_2 != zenon_Vtba) % 19.63/19.98 (zenon_Vav != zenon_Vxba) % 19.63/19.98 (p2 zenon_Vwc) % 19.63/19.98 (p6 zenon_Vnc) % 19.63/19.98 (p4 zenon_Vwz) % 19.63/19.98 (zenon_Vzn != zenon_Vuba) % 19.63/19.98 (zenon_Vpx != zenon_Vuba) % 19.63/19.98 (zenon_Vyaa != zenon_Vsba) % 19.63/19.98 (zenon_Veaa != zenon_Vyba) % 19.63/19.98 (p1 zenon_Vlq) % 19.63/19.98 (Tau_4 != zenon_Vuba) % 19.63/19.98 (zenon_Vwaa != zenon_Vsba) % 19.63/19.98 (p3 zenon_Vwv) % 19.63/19.98 (zenon_X144 != zenon_Vuba) % 19.63/19.98 (p5 zenon_Vir) % 19.63/19.98 (zenon_Vnj != zenon_Vxba) % 19.63/19.98 (p5 zenon_Vav) % 19.63/19.98 (p2 zenon_Vgt) % 19.63/19.98 (p5 zenon_Vuaa) % 19.63/19.98 (p5 zenon_Vxi) % 19.63/19.98 (Tau_4 != zenon_Vsba) % 19.63/19.98 (p4 zenon_Vfn) % 19.63/19.98 (zenon_Vhx != zenon_Vsba) % 19.63/19.98 (p3 zenon_Vmp) % 19.63/19.98 (zenon_Vsn != zenon_Vsba) % 19.63/19.98 (zenon_Vuaa != zenon_Vuba) % 19.63/19.98 (zenon_Veba != zenon_Vvba) % 19.63/19.98 (zenon_Vmp != zenon_Vvba) % 19.63/19.98 (-. (p5 zenon_Vxba)) % 19.63/19.98 (zenon_X148 != Tau_4) % 19.63/19.98 (Tau_3 != zenon_Vuba) % 19.63/19.98 (p6 zenon_Vuj) % 19.63/19.98 (zenon_Vyba != zenon_Vtba) % 19.63/19.98 (p4 zenon_Vyp) % 19.63/19.98 (zenon_Vks != zenon_Vvba) % 19.63/19.98 (zenon_Veaa != zenon_Vtba) % 19.63/19.98 (zenon_Vor != zenon_Vxba) % 19.63/19.98 (zenon_X145 != Tau_2) % 19.63/19.98 (p3 zenon_Veaa) % 19.63/19.98 (Tau_1 != zenon_Vuba) % 19.63/19.98 (zenon_Vws != zenon_Vvba) % 19.63/19.98 (zenon_Vcba != zenon_Vyba) % 19.63/19.98 (-. (r1 Tau_0 zenon_Vxba)) % 19.63/19.98 (Tau_3 != zenon_Vtba) % 19.63/19.98 (p2 zenon_X147) % 19.63/19.98 (zenon_Vxba != zenon_Vvba) % 19.63/19.98 (zenon_Vor != zenon_Vsba) % 19.63/19.98 (zenon_Vqs != zenon_Vyba) % 19.63/19.98 (p2 zenon_Vkf) % 19.63/19.98 (p2 zenon_Vud) % 19.63/19.98 (zenon_Vcba != zenon_Vvba) % 19.63/19.98 (Tau_3 != zenon_Vxba) % 19.63/19.98 (-. (p3 Tau_2)) % 19.63/19.98 (p2 zenon_Vva) % 19.63/19.98 (Tau_3 != zenon_Vvba) % 19.63/19.98 (Tau_1 != zenon_Vyba) % 19.63/19.98 (zenon_X146 != zenon_Vtba) % 19.63/19.98 (p4 zenon_Viaa) % 19.63/19.98 (zenon_Vxi != zenon_Vxba) % 19.63/19.98 (p6 zenon_Ved) % 19.63/19.98 (p3 zenon_Veba) % 19.63/19.98 (-. (p3 zenon_Vtba)) % 19.63/19.98 (zenon_Vpz != zenon_Vsba) % 19.63/19.98 (zenon_Vvu != zenon_Vuba) % 19.63/19.98 (p4 zenon_Vcf) % 19.63/19.98 (zenon_Vuaa != zenon_Vsba) % 19.63/19.98 (zenon_X145 != zenon_Vtba) % 19.63/19.98 (p6 zenon_Vzr) % 19.63/19.98 (p2 zenon_Vnl) % 19.63/19.98 (p2 zenon_Vmv) % 19.63/19.98 (p4 zenon_Vwx) % 19.63/19.98 (zenon_Vme != zenon_Vxba) % 19.63/19.98 (zenon_Vks != zenon_Vtba) % 19.63/19.98 (zenon_Vfp != zenon_Vyba) % 19.63/19.98 (zenon_X143 != Tau_1) % 19.63/19.98 (zenon_Vpz != zenon_Vxba) % 19.63/19.98 (zenon_Vbw != zenon_Vvba) % 19.63/19.98 (zenon_Vdy != zenon_Vyba) % 19.63/19.98 (zenon_Vxi != zenon_Vsba) % 19.63/19.98 (zenon_X145 != zenon_Vvba) % 19.63/19.98 (zenon_Vsh != zenon_Vwba) % 19.63/19.98 (zenon_Vwba != zenon_Vtba) % 19.63/19.98 (Tau_4 != zenon_Vyba) % 19.63/19.98 (zenon_Vbaa != zenon_Vtba) % 19.63/19.98 (-. (p5 Tau_1)) % 19.63/19.98 (p2 zenon_Vnw) % 19.63/19.98 (zenon_Vcba != zenon_Vtba) % 19.63/19.98 (zenon_Vqba != zenon_Vwba) % 19.63/19.98 (Tau_1 != Tau_0) % 19.63/19.98 (zenon_Vyba != zenon_Vsba) % 19.63/19.98 (zenon_Vxba != zenon_Vuba) % 19.63/19.98 (p2 zenon_Vzx) % 19.63/19.98 (r1 Tau_1 zenon_Vsba) % 19.63/19.98 (p4 zenon_Vbh) % 19.63/19.98 (p5 zenon_Vpz) % 19.63/19.98 (r1 Tau_1 zenon_Vtba) % 19.63/19.98 (zenon_Vav != zenon_Vuba) % 19.63/19.98 (zenon_Vir != zenon_Vuba) % 19.63/19.98 (p6 zenon_Viu) % 19.63/19.98 (zenon_Vfj != zenon_Vuba) % 19.63/19.98 (zenon_Vrk != zenon_Vtba) % 19.63/19.98 (zenon_Vde != zenon_Vxba) % 19.63/19.98 (p4 zenon_Viv) % 19.63/19.98 (p5 zenon_Vsz) % 19.63/19.98 (zenon_Vjk != zenon_Vtba) % 19.63/19.98 (zenon_Vfj != zenon_Vxba) % 19.63/19.98 (p1 zenon_Veu) % 19.63/19.98 (p4 zenon_Vyo) % 19.63/19.98 (zenon_Vsz != zenon_Vxba) % 19.63/19.98 (zenon_Vxw != zenon_Vwba) % 19.63/19.98 (p1 zenon_Vvy) % 19.63/19.98 (zenon_Vwba != zenon_Vuba) % 19.63/19.98 (r1 Tau_2 zenon_Vvba) % 19.63/19.98 (zenon_Vks != zenon_Vyba) % 19.63/19.98 (p2 zenon_Vjh) % 19.63/19.98 (p1 zenon_Vmt) % 19.63/19.98 (p3 zenon_Vcba) % 19.63/19.98 (zenon_Vuaa != zenon_Vxba) % 19.63/19.98 (p1 zenon_Vtm) % 19.63/19.98 *) % 19.63/19.98 (* NO-PROOF *) % 19.63/19.98 % SZS status GaveUp % 19.63/19.98 Number of rewrites on terms: 0 % 19.63/19.98 Number of rewrites on props: 0 % 19.63/19.98 nodes searched: 1950 % 19.63/19.98 max branch formulas: 2029 % 19.63/19.98 proof nodes created: 25 % 19.63/19.98 formulas created: 12031 % 19.63/19.98 %------------------------------------------------------------------------------