%------------------------------------------------------------------------------ % File : ZenonModulo---0.5.0 % Problem : LCL640+1.010 : TPTP v9.3.1. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : run_zenon_modulo %d %s % Computer : n004.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:12 PM UTC 2026 % Result : Unknown 0.18s 0.53s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LCL640+1.010 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.03 % Command : run_zenon_modulo %d %s % 0.11/0.36 % Computer : n004.cluster.edu % 0.11/0.36 % Model : x86_64 x86_64 % 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.36 % Memory : 8046.5625MB % 0.11/0.36 % OS : Linux 6.8.0-71-generic % 0.11/0.36 % CPULimit : 300 % 0.11/0.36 % WCLimit : 300 % 0.11/0.36 % DateTime : Sat Sep 5 16:05:14 UTC 2026 % 0.11/0.37 % CPUTime : % 0.18/0.53 Zenon error: exhausted search space without finding a proof % 0.18/0.53 (* Current branch: % 0.18/0.53 (r1 zenon_Vtd zenon_Vwd) % 0.18/0.53 (zenon_Vwc != zenon_Vhe) % 0.18/0.53 (zenon_Vtb != zenon_Vwd) % 0.18/0.53 (zenon_Vtb != zenon_Vre) % 0.18/0.53 (r1 zenon_Vwc zenon_Vxc) % 0.18/0.53 (r1 zenon_Vmb zenon_Vrb) % 0.18/0.53 (zenon_Vtb != zenon_Vfc) % 0.18/0.53 (zenon_Vwc != zenon_Vac) % 0.18/0.53 (zenon_Vwc != zenon_Vwd) % 0.18/0.53 (zenon_Vtb != zenon_Vcb) % 0.18/0.53 (zenon_Vwc != zenon_Vve) % 0.18/0.53 (zenon_Vuc != zenon_Vrd) % 0.18/0.53 (r1 Tau_1 zenon_Vnc) % 0.18/0.53 (zenon_Vuc != zenon_Vac) % 0.18/0.53 (zenon_Vwc != zenon_Vsb) % 0.18/0.53 (zenon_Vuc != zenon_Vsb) % 0.18/0.53 (-. (p1 zenon_Vkc)) % 0.18/0.53 (zenon_Vwc != zenon_Vw) % 0.18/0.53 (r1 zenon_Vie zenon_Vle) % 0.18/0.53 (zenon_Vrb != zenon_Vw) % 0.18/0.53 (zenon_Vwc != zenon_Vna) % 0.18/0.53 (zenon_Vrb != zenon_Vbb) % 0.18/0.53 (zenon_Vuc != zenon_Vw) % 0.18/0.53 (zenon_Vrb != zenon_Vac) % 0.18/0.53 (zenon_Vtb != zenon_Vac) % 0.18/0.53 (-. (p1 zenon_Vma)) % 0.18/0.53 (r1 zenon_Vz zenon_Vca) % 0.18/0.53 (-. (p1 zenon_Vna)) % 0.18/0.53 (r1 zenon_Vxe zenon_Vaf) % 0.18/0.53 (p1 zenon_Vwc) % 0.18/0.53 (-. (p1 zenon_Ved)) % 0.18/0.53 (zenon_Vrb != zenon_Vrd) % 0.18/0.53 (zenon_Vtb != zenon_Vhe) % 0.18/0.53 (zenon_Vrb != zenon_Vqd) % 0.18/0.53 (zenon_Vrb != zenon_Vca) % 0.18/0.53 (zenon_Vtb != zenon_Vsa) % 0.18/0.53 (-. (p1 zenon_Vzb)) % 0.18/0.53 (zenon_Vtb != zenon_Vzb) % 0.18/0.53 (-. (p1 zenon_Vxc)) % 0.18/0.53 (zenon_Vuc != zenon_Vfd) % 0.18/0.53 (zenon_Vtb != zenon_Vw) % 0.18/0.53 (r1 zenon_Vrb zenon_Vsb) % 0.18/0.53 (zenon_Vtb != zenon_Vxc) % 0.18/0.53 (zenon_Vtb != zenon_Vle) % 0.18/0.53 (-. (p1 zenon_Vaf)) % 0.18/0.53 (zenon_Vuc != zenon_Vsc) % 0.18/0.53 (r1 zenon_Vmb zenon_Vkc) % 0.18/0.53 (-. (p1 zenon_Vhb)) % 0.18/0.53 (r1 zenon_Vmb zenon_Vzb) % 0.18/0.53 (zenon_Vwc != zenon_Vkc) % 0.18/0.53 (zenon_Vtb != zenon_Vqd) % 0.18/0.53 (zenon_Vwc != zenon_Vxc) % 0.18/0.53 (zenon_Vwc != zenon_Vce) % 0.18/0.53 (zenon_Vrb != zenon_Vfc) % 0.18/0.53 (zenon_Vuc != zenon_Vme) % 0.18/0.53 (zenon_Vrb != zenon_Vna) % 0.18/0.53 (r1 zenon_Voc zenon_Vpc) % 0.18/0.53 (r1 zenon_Vqc zenon_Vrc) % 0.18/0.53 (-. (p1 zenon_Vsc)) % 0.18/0.53 (-. (p1 zenon_Vle)) % 0.18/0.53 (zenon_Vrb != zenon_Vbe) % 0.18/0.53 (-. (p1 zenon_Vac)) % 0.18/0.53 (zenon_Vrb != zenon_Vwb) % 0.18/0.53 (zenon_Vwc != zenon_Ved) % 0.18/0.53 (r1 zenon_Vnc zenon_Voc) % 0.18/0.53 (zenon_Vrb != zenon_Vma) % 0.18/0.53 (zenon_Vrb != zenon_Vhe) % 0.18/0.53 (zenon_Vwc != zenon_Vle) % 0.18/0.53 (r1 zenon_Vt zenon_Vw) % 0.18/0.53 (zenon_Vrb != zenon_Vkd) % 0.18/0.53 (-. (p1 zenon_Vhe)) % 0.18/0.53 (zenon_Vrb != zenon_Vlc) % 0.18/0.53 (-. (p1 zenon_Vrd)) % 0.18/0.53 (r1 zenon_Veb zenon_Vhb) % 0.18/0.53 (zenon_Vrb != zenon_Vxc) % 0.18/0.53 (zenon_Vtb != zenon_Vsc) % 0.18/0.53 (zenon_Vwc != zenon_Vre) % 0.18/0.53 (zenon_Vrb != zenon_Vcb) % 0.18/0.53 (-. (p1 zenon_Vfd)) % 0.18/0.53 (zenon_Vuc != zenon_Vx) % 0.18/0.53 (r1 zenon_Vnd zenon_Vqd) % 0.18/0.53 (zenon_Vuc != zenon_Vfc) % 0.18/0.53 (zenon_Vrb != zenon_Vve) % 0.18/0.53 (-. (p1 zenon_Vre)) % 0.18/0.53 (zenon_Vtb != zenon_Vlc) % 0.18/0.53 (zenon_Vuc != zenon_Vle) % 0.18/0.53 (-. (p1 zenon_Vcb)) % 0.18/0.53 (r1 zenon_Voe zenon_Vre) % 0.18/0.53 (zenon_Vtb != zenon_Vve) % 0.18/0.53 (zenon_Vtb != zenon_Vfd) % 0.18/0.53 (zenon_Vtb != zenon_Vna) % 0.18/0.53 (r1 zenon_Vcc zenon_Vfc) % 0.18/0.53 (zenon_Vuc != zenon_Vkc) % 0.18/0.53 (r1 zenon_Vtb zenon_Vwb) % 0.18/0.53 (zenon_Vwc != zenon_Vca) % 0.18/0.53 (zenon_Vtb != zenon_Vkd) % 0.18/0.53 (zenon_Vtb != zenon_Vx) % 0.18/0.53 (zenon_Vrb != zenon_Vaf) % 0.18/0.53 (-. (p1 zenon_Vve)) % 0.18/0.53 (zenon_Vwc != zenon_Vsc) % 0.18/0.53 (zenon_Vtb != zenon_Vrd) % 0.18/0.53 (zenon_Vwc != zenon_Vzb) % 0.18/0.53 (zenon_Vwc != zenon_Vkd) % 0.18/0.53 (r1 zenon_X10 zenon_Vue) % 0.18/0.53 (zenon_Vtb != zenon_Ved) % 0.18/0.53 (zenon_Vrb != zenon_Vzb) % 0.18/0.53 (zenon_Vuc != zenon_Vve) % 0.18/0.53 (-. (p1 zenon_Vlc)) % 0.18/0.53 (zenon_Vuc != zenon_Vbe) % 0.18/0.53 (-. (p1 zenon_Vce)) % 0.18/0.53 (zenon_Vwc != zenon_Vsa) % 0.18/0.53 (r1 zenon_Vpa zenon_Vsa) % 0.18/0.53 (zenon_Vuc != zenon_Vca) % 0.18/0.53 (zenon_Vtb != zenon_Vbb) % 0.18/0.53 (zenon_Vuc != zenon_Vaf) % 0.18/0.53 (-. (p1 zenon_Vwd)) % 0.18/0.53 (zenon_Vuc != zenon_Vhb) % 0.18/0.53 (r1 zenon_Vee zenon_Vhe) % 0.18/0.53 (-. (p1 zenon_Vme)) % 0.18/0.53 (zenon_Vrb != zenon_Vme) % 0.18/0.53 (r1 Tau_0 Tau_1) % 0.18/0.53 (zenon_Vuc != zenon_Vzb) % 0.18/0.53 (r1 zenon_Vhd zenon_Vkd) % 0.18/0.53 (zenon_Vuc != zenon_Vqd) % 0.18/0.53 (r1 zenon_Vrc zenon_Vsc) % 0.18/0.53 (zenon_Vwc != zenon_Vcb) % 0.18/0.53 (zenon_Vrb != zenon_Vhb) % 0.18/0.53 (zenon_Vrb != zenon_Vce) % 0.18/0.53 (zenon_Vuc != zenon_Vsa) % 0.18/0.53 (zenon_Vuc != zenon_Vlc) % 0.18/0.53 (zenon_Vtb != zenon_Vme) % 0.18/0.53 (zenon_Vwc != zenon_Vfc) % 0.18/0.53 (zenon_Vwc != zenon_Vue) % 0.18/0.53 (-. (p1 zenon_Vue)) % 0.18/0.53 (zenon_Vrb != zenon_Vle) % 0.18/0.53 (zenon_Vrb != zenon_Vfd) % 0.18/0.53 (zenon_Vuc != zenon_Vcb) % 0.18/0.53 (zenon_Vtb != zenon_Vma) % 0.18/0.53 (p1 zenon_Vrb) % 0.18/0.53 (zenon_Vuc != zenon_Vbb) % 0.18/0.53 (zenon_Vtb != zenon_Vwb) % 0.18/0.53 (zenon_Vuc != zenon_Ved) % 0.18/0.53 (zenon_Vwc != zenon_Vbb) % 0.18/0.53 (r1 zenon_Vyd zenon_Vbe) % 0.18/0.53 (r1 zenon_Vja zenon_Vma) % 0.18/0.53 (-. (p1 zenon_Vbe)) % 0.18/0.53 (zenon_Vwc != zenon_Vx) % 0.18/0.53 (zenon_Vrb != zenon_Vsc) % 0.18/0.53 (zenon_Vuc != zenon_Vre) % 0.18/0.53 (zenon_Vrb != zenon_Vre) % 0.18/0.53 (r1 zenon_Vvc zenon_Vwc) % 0.18/0.53 (-. (p1 zenon_Vw)) % 0.18/0.53 (zenon_Vtb != zenon_Vca) % 0.18/0.53 (zenon_Vuc != zenon_Vma) % 0.18/0.53 (zenon_Vrb != zenon_Vwd) % 0.18/0.53 (p1 zenon_Vtb) % 0.18/0.53 (zenon_Vrb != zenon_Vsb) % 0.18/0.53 (zenon_Vuc != zenon_Vkd) % 0.18/0.53 (zenon_Vuc != zenon_Vwb) % 0.18/0.53 (zenon_Vuc != zenon_Vce) % 0.18/0.53 (zenon_Vwc != zenon_Vfd) % 0.18/0.53 (r1 zenon_Vrc zenon_Vtc) % 0.18/0.53 (zenon_Vwc != zenon_Vwb) % 0.18/0.53 (-. (p1 zenon_Vsa)) % 0.18/0.53 (r1 zenon_Vbd zenon_Ved) % 0.18/0.53 (zenon_Vtb != zenon_Vaf) % 0.18/0.53 (-. (p1 zenon_Vfc)) % 0.18/0.53 (-. (p1 zenon_Vsb)) % 0.18/0.53 (zenon_Vuc != zenon_Vue) % 0.18/0.53 (zenon_Vtb != zenon_Vhb) % 0.18/0.53 (-. (p1 zenon_Vwb)) % 0.18/0.53 (zenon_Vwc != zenon_Vme) % 0.18/0.53 (-. (p1 zenon_Vkd)) % 0.18/0.53 (zenon_Vrb != zenon_Vx) % 0.18/0.53 (zenon_Vwc != zenon_Vlc) % 0.18/0.53 (p1 zenon_Vuc) % 0.18/0.53 (r1 zenon_Vya zenon_Vbb) % 0.18/0.53 (zenon_Vtb != zenon_Vue) % 0.18/0.53 (zenon_Vtb != zenon_Vce) % 0.18/0.53 (-. (p1 zenon_Vbb)) % 0.18/0.53 (zenon_Vuc != zenon_Vna) % 0.18/0.53 (-. (p1 zenon_Vx)) % 0.18/0.53 (zenon_Vwc != zenon_Vaf) % 0.18/0.53 (zenon_Vwc != zenon_Vqd) % 0.18/0.53 (zenon_Vtb != zenon_Vbe) % 0.18/0.53 (zenon_Vrb != zenon_Vue) % 0.18/0.53 (zenon_Vuc != zenon_Vwd) % 0.18/0.53 (zenon_Vrb != zenon_Vkc) % 0.18/0.53 (zenon_Vwc != zenon_Vma) % 0.18/0.53 (zenon_Vwc != zenon_Vhb) % 0.18/0.53 (zenon_Vrb != zenon_Ved) % 0.18/0.53 (zenon_Vuc != zenon_Vhe) % 0.18/0.53 (-. (p1 zenon_Vca)) % 0.18/0.53 (r1 zenon_Vpc zenon_Vqc) % 0.18/0.53 (zenon_Vwc != zenon_Vrd) % 0.18/0.53 (zenon_Vwc != zenon_Vbe) % 0.18/0.53 (zenon_Vuc != zenon_Vxc) % 0.18/0.53 (zenon_Vtb != zenon_Vkc) % 0.18/0.53 (zenon_Vtb != zenon_Vsb) % 0.18/0.53 (zenon_Vrb != zenon_Vsa) % 0.18/0.53 (-. (p1 zenon_Vqd)) % 0.18/0.53 *) % 0.18/0.53 (* NO-PROOF *) % 0.18/0.53 % SZS status GaveUp % 0.18/0.53 Number of rewrites on terms: 0 % 0.18/0.53 Number of rewrites on props: 0 % 0.18/0.53 nodes searched: 376 % 0.18/0.53 max branch formulas: 444 % 0.18/0.53 proof nodes created: 0 % 0.18/0.53 formulas created: 2483 % 0.18/0.53 %------------------------------------------------------------------------------