%------------------------------------------------------------------------------ % File : ZenonModulo---0.5.0 % Problem : LCL658+1.020 : TPTP v9.3.1. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : run_zenon_modulo %d %s % Computer : n017.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 0.43s 0.71s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LCL658+1.020 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.03 % Command : run_zenon_modulo %d %s % 0.09/0.35 % Computer : n017.cluster.edu % 0.09/0.35 % Model : x86_64 x86_64 % 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.35 % Memory : 8046.5625MB % 0.09/0.35 % OS : Linux 6.8.0-71-generic % 0.09/0.35 % CPULimit : 300 % 0.09/0.35 % WCLimit : 300 % 0.09/0.35 % DateTime : Sat Sep 5 07:55:06 UTC 2026 % 0.09/0.36 % CPUTime : % 0.43/0.71 Zenon error: exhausted search space without finding a proof % 0.43/0.71 (* Current branch: % 0.43/0.71 (zenon_Vug != zenon_Vhe) % 0.43/0.71 (zenon_Vkf != zenon_Vti) % 0.43/0.71 (zenon_Vug != zenon_Vti) % 0.43/0.71 (-. (p1 zenon_Vga)) % 0.43/0.71 (-. (p1 zenon_Vhh)) % 0.43/0.71 (zenon_Vmf != zenon_Vhh) % 0.43/0.71 (zenon_Vsg != zenon_Vsf) % 0.43/0.71 (zenon_Vkf != zenon_Vga) % 0.43/0.71 (r1 zenon_Vzc zenon_Vcd) % 0.43/0.71 (zenon_Vkf != zenon_Vlc) % 0.43/0.71 (zenon_Vkf != zenon_Vlf) % 0.43/0.71 (zenon_Vmf != zenon_Vdg) % 0.43/0.71 (zenon_Vkf != zenon_Vpf) % 0.43/0.71 (zenon_Vmf != zenon_Vpj) % 0.43/0.71 (r1 zenon_Vic zenon_Vlc) % 0.43/0.71 (r1 zenon_Vxa zenon_Vab) % 0.43/0.71 (zenon_Vsg != zenon_Vlj) % 0.43/0.71 (zenon_Vmf != zenon_Vlf) % 0.43/0.71 (zenon_Vug != zenon_Vvg) % 0.43/0.71 (zenon_Vug != zenon_Vpj) % 0.43/0.71 (-. (p1 zenon_Vtb)) % 0.43/0.71 (zenon_Vkf != zenon_Vvg) % 0.43/0.71 (r1 zenon_Vpg zenon_Vrg) % 0.43/0.71 (zenon_Vmf != zenon_Vvg) % 0.43/0.71 (zenon_Vmf != zenon_Vsd) % 0.43/0.71 (r1 zenon_Vqb zenon_Vtb) % 0.43/0.71 (zenon_Vsg != zenon_Vsh) % 0.43/0.71 (r1 zenon_Vff zenon_Vsf) % 0.43/0.71 (zenon_Vkf != zenon_Veg) % 0.43/0.71 (-. (p1 zenon_Vab)) % 0.43/0.71 (-. (p1 zenon_Vsh)) % 0.43/0.71 (zenon_Vsg != zenon_Vlf) % 0.43/0.71 (zenon_Vsg != zenon_Vlc) % 0.43/0.71 (zenon_Vkf != zenon_Vgj) % 0.43/0.71 (zenon_Vmf != zenon_Veg) % 0.43/0.71 (zenon_Vsg != zenon_Vqg) % 0.43/0.71 (zenon_Vug != zenon_Vsd) % 0.43/0.71 (-. (p1 zenon_Vdg)) % 0.43/0.71 (zenon_Vmf != zenon_Vqg) % 0.43/0.71 (zenon_Vmf != zenon_Vti) % 0.43/0.71 (r1 Tau_0 Tau_1) % 0.43/0.71 (zenon_Vug != zenon_Vpf) % 0.43/0.71 (zenon_Vsg != zenon_Vve) % 0.43/0.71 (zenon_Vmf != zenon_Vaj) % 0.43/0.71 (zenon_Vkf != zenon_Vhh) % 0.43/0.71 (zenon_Vkf != zenon_Vsd) % 0.43/0.71 (-. (p1 zenon_Vcd)) % 0.43/0.71 (zenon_Vsg != zenon_Vsd) % 0.43/0.71 (r1 zenon_Vdj zenon_Vgj) % 0.43/0.71 (zenon_Vug != zenon_Vsf) % 0.43/0.71 (r1 zenon_Vug zenon_Vvg) % 0.43/0.71 (zenon_Vkf != zenon_Vsj) % 0.43/0.71 (zenon_Vsg != zenon_Vti) % 0.43/0.71 (zenon_Vmf != zenon_Vsf) % 0.43/0.71 (-. (p1 zenon_Vhe)) % 0.43/0.71 (-. (p1 zenon_Veg)) % 0.43/0.71 (r1 zenon_Vtg zenon_Vug) % 0.43/0.71 (zenon_Vsg != zenon_Vgj) % 0.43/0.71 (zenon_Vsg != zenon_Vga) % 0.43/0.71 (r1 zenon_Vpg zenon_Vqg) % 0.43/0.71 (r1 zenon_Vog zenon_Vpg) % 0.43/0.71 (zenon_Vug != zenon_Vga) % 0.43/0.71 (zenon_Vmf != zenon_Vtf) % 0.43/0.71 (r1 zenon_Vmf zenon_Vpf) % 0.43/0.71 (zenon_Vug != zenon_Vve) % 0.43/0.71 (zenon_Vkf != zenon_Vdg) % 0.43/0.71 (r1 zenon_Vkf zenon_Vlf) % 0.43/0.71 (r1 zenon_Vxi zenon_Vaj) % 0.43/0.71 (zenon_Vug != zenon_Vhh) % 0.43/0.71 (r1 zenon_Vii zenon_Vli) % 0.43/0.71 (-. (p1 zenon_Vli)) % 0.43/0.71 (r1 zenon_Vse zenon_Vve) % 0.43/0.71 (zenon_Vug != zenon_Vab) % 0.43/0.71 (r1 zenon_Vig zenon_Vjg) % 0.43/0.71 (zenon_Vsg != zenon_Vab) % 0.43/0.71 (r1 zenon_Vgg zenon_Vhg) % 0.43/0.71 (zenon_Vsg != zenon_Vvg) % 0.43/0.71 (zenon_Vmf != zenon_Vhe) % 0.43/0.71 (zenon_Vug != zenon_Veg) % 0.43/0.71 (zenon_Vug != zenon_Vci) % 0.43/0.71 (-. (p1 zenon_Vtf)) % 0.43/0.71 (-. (p1 zenon_Vve)) % 0.43/0.71 (p1 zenon_Vug) % 0.43/0.71 (zenon_Vsg != zenon_Vcd) % 0.43/0.71 (r1 zenon_Vkg zenon_Vlg) % 0.43/0.71 (zenon_Vsg != zenon_Vaj) % 0.43/0.71 (-. (p1 zenon_Vlc)) % 0.43/0.71 (zenon_Vsg != zenon_Veg) % 0.43/0.71 (zenon_Vug != zenon_Vgj) % 0.43/0.71 (p1 zenon_Vmf) % 0.43/0.71 (r1 zenon_X20 zenon_Vsj) % 0.43/0.71 (r1 zenon_Vmj zenon_Vpj) % 0.43/0.71 (zenon_Vsg != zenon_Vyf) % 0.43/0.71 (zenon_Vkf != zenon_Vci) % 0.43/0.71 (-. (p1 zenon_Vsj)) % 0.43/0.71 (zenon_Vsg != zenon_Vsj) % 0.43/0.71 (r1 zenon_Vee zenon_Vhe) % 0.43/0.71 (zenon_Vkf != zenon_Vhe) % 0.43/0.71 (zenon_Vmf != zenon_Vsh) % 0.43/0.71 (r1 zenon_Vqi zenon_Vti) % 0.43/0.71 (-. (p1 zenon_Vsd)) % 0.43/0.71 (zenon_Vsg != zenon_Vli) % 0.43/0.71 (zenon_Vmf != zenon_Vga) % 0.43/0.71 (zenon_Vug != zenon_Vtb) % 0.43/0.71 (zenon_Vkf != zenon_Vve) % 0.43/0.71 (zenon_Vug != zenon_Vcd) % 0.43/0.71 (zenon_Vmf != zenon_Vlj) % 0.43/0.71 (zenon_Vkf != zenon_Vpj) % 0.43/0.71 (r1 zenon_Vzh zenon_Vci) % 0.43/0.71 (zenon_Vsg != zenon_Vci) % 0.43/0.71 (zenon_Vmf != zenon_Vve) % 0.43/0.71 (zenon_Vmf != zenon_Vci) % 0.43/0.71 (zenon_Vkf != zenon_Vqg) % 0.43/0.71 (zenon_Vkf != zenon_Vtf) % 0.43/0.71 (-. (p1 zenon_Vvg)) % 0.43/0.71 (zenon_Vkf != zenon_Vab) % 0.43/0.71 (r1 zenon_Vng zenon_Vog) % 0.43/0.71 (-. (p1 zenon_Vqg)) % 0.43/0.71 (zenon_Vug != zenon_Vaj) % 0.43/0.71 (zenon_Vkf != zenon_Vli) % 0.43/0.71 (zenon_Vug != zenon_Vli) % 0.43/0.71 (r1 zenon_Vph zenon_Vsh) % 0.43/0.71 (zenon_Vsg != zenon_Vhh) % 0.43/0.71 (-. (p1 zenon_Vgj)) % 0.43/0.71 (zenon_Vmf != zenon_Vsj) % 0.43/0.71 (r1 zenon_Vij zenon_Vlj) % 0.43/0.71 (zenon_Vkf != zenon_Vlj) % 0.43/0.71 (zenon_Vsg != zenon_Vhe) % 0.43/0.71 (r1 zenon_Vpd zenon_Vsd) % 0.43/0.71 (zenon_Vsg != zenon_Vpj) % 0.43/0.71 (r1 zenon_Vda zenon_Vga) % 0.43/0.71 (zenon_Vmf != zenon_Vlc) % 0.43/0.71 (-. (p1 zenon_Vpf)) % 0.43/0.71 (-. (p1 zenon_Vti)) % 0.43/0.71 (zenon_Vsg != zenon_Vtf) % 0.43/0.71 (zenon_Vug != zenon_Vsh) % 0.43/0.71 (zenon_Vug != zenon_Vsj) % 0.43/0.71 (zenon_Vmf != zenon_Vtb) % 0.43/0.71 (zenon_Vkf != zenon_Vcd) % 0.43/0.71 (zenon_Vmf != zenon_Vli) % 0.43/0.71 (zenon_Vug != zenon_Vlf) % 0.43/0.71 (zenon_Vug != zenon_Vlj) % 0.43/0.71 (zenon_Vug != zenon_Vqg) % 0.43/0.71 (zenon_Vmf != zenon_Vgj) % 0.43/0.71 (-. (p1 zenon_Vsf)) % 0.43/0.71 (-. (p1 zenon_Vlf)) % 0.43/0.71 (zenon_Vug != zenon_Vlc) % 0.43/0.71 (p1 zenon_Vkf) % 0.43/0.71 (-. (p1 zenon_Vyf)) % 0.43/0.71 (r1 zenon_Veh zenon_Vhh) % 0.43/0.71 (zenon_Vkf != zenon_Vaj) % 0.43/0.71 (r1 zenon_Vff zenon_Vdg) % 0.43/0.71 (-. (p1 zenon_Vaj)) % 0.43/0.71 (r1 zenon_Vlg zenon_Vmg) % 0.43/0.71 (zenon_Vkf != zenon_Vyf) % 0.43/0.71 (zenon_Vkf != zenon_Vsh) % 0.43/0.71 (r1 zenon_Vmg zenon_Vng) % 0.43/0.71 (r1 zenon_Vff zenon_Vkf) % 0.43/0.71 (zenon_Vug != zenon_Vdg) % 0.43/0.71 (zenon_Vmf != zenon_Vyf) % 0.43/0.71 (p1 zenon_Vsg) % 0.43/0.71 (-. (p1 zenon_Vlj)) % 0.43/0.71 (-. (p1 zenon_Vpj)) % 0.43/0.71 (r1 Tau_1 zenon_Vgg) % 0.43/0.71 (zenon_Vsg != zenon_Vpf) % 0.43/0.71 (zenon_Vmf != zenon_Vcd) % 0.43/0.71 (zenon_Vmf != zenon_Vab) % 0.43/0.71 (r1 zenon_Vjg zenon_Vkg) % 0.43/0.71 (zenon_Vsg != zenon_Vtb) % 0.43/0.71 (zenon_Vkf != zenon_Vsf) % 0.43/0.71 (zenon_Vug != zenon_Vyf) % 0.43/0.71 (zenon_Vug != zenon_Vtf) % 0.43/0.71 (r1 zenon_Vvf zenon_Vyf) % 0.43/0.71 (zenon_Vkf != zenon_Vtb) % 0.43/0.71 (zenon_Vmf != zenon_Vpf) % 0.43/0.71 (r1 zenon_Vhg zenon_Vig) % 0.43/0.71 (-. (p1 zenon_Vci)) % 0.43/0.71 (zenon_Vsg != zenon_Vdg) % 0.43/0.71 *) % 0.43/0.71 (* NO-PROOF *) % 0.43/0.71 % SZS status GaveUp % 0.43/0.71 Number of rewrites on terms: 0 % 0.43/0.71 Number of rewrites on props: 0 % 0.43/0.71 nodes searched: 623 % 0.43/0.71 max branch formulas: 692 % 0.43/0.71 proof nodes created: 0 % 0.43/0.71 formulas created: 3536 % 0.43/0.71 %------------------------------------------------------------------------------