%------------------------------------------------------------------------------ % File : ZenonModulo---0.5.0 % Problem : LCL650+1.005 : TPTP v9.3.1. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : run_zenon_modulo %d %s % Computer : n029.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:16 PM UTC 2026 % Result : Unknown 0.21s 0.53s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : LCL650+1.005 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.02 % Command : run_zenon_modulo %d %s % 0.09/0.34 % Computer : n029.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 14:39:55 UTC 2026 % 0.09/0.35 % CPUTime : % 0.21/0.53 Zenon error: exhausted search space without finding a proof % 0.21/0.53 (* Current branch: % 0.21/0.53 (-. (p12 zenon_Vic)) % 0.21/0.53 (zenon_Vvc != zenon_Vwc) % 0.21/0.53 (p8 zenon_Vle) % 0.21/0.53 (-. (p15 zenon_Vpa)) % 0.21/0.53 (zenon_Vaf != zenon_Vbf) % 0.21/0.53 (zenon_Vaa != zenon_Vpf) % 0.21/0.53 (-. (p17 Tau_2)) % 0.21/0.53 (p12 zenon_Vvc) % 0.21/0.53 (r1 zenon_Vt zenon_Vu) % 0.21/0.53 (p11 zenon_Vhd) % 0.21/0.53 (zenon_Vsd != zenon_Vtd) % 0.21/0.53 (r1 Tau_0 Tau_2) % 0.21/0.53 (-. (p11 zenon_Vid)) % 0.21/0.53 (-. (p3 zenon_Vlf)) % 0.21/0.53 (r1 zenon_Vu zenon_Vv) % 0.21/0.53 (zenon_Vfb != zenon_Vpa) % 0.21/0.53 (-. (p9 zenon_Vde)) % 0.21/0.53 (-. (p7 zenon_Vue)) % 0.21/0.53 (-. (p12 zenon_Vwc)) % 0.21/0.53 (-. (p13 zenon_Vub)) % 0.21/0.53 (r1 zenon_Vn zenon_Vo) % 0.21/0.53 (zenon_Vle != zenon_Vme) % 0.21/0.53 (p4 zenon_Vlf) % 0.21/0.53 (r1 Tau_3 zenon_Vtf) % 0.21/0.53 (r1 zenon_Vbg zenon_Vcg) % 0.21/0.53 (-. (p8 zenon_Vce)) % 0.21/0.53 (-. (p8 zenon_Vme)) % 0.21/0.53 (r1 zenon_Vo zenon_Vp) % 0.21/0.53 (p2 zenon_Vaa) % 0.21/0.53 (zenon_Vic != zenon_Vjc) % 0.21/0.53 (r1 zenon_Vxc zenon_Vid) % 0.21/0.53 (r1 zenon_Vwf zenon_Vxf) % 0.21/0.53 (r1 zenon_Veg zenon_Vfg) % 0.21/0.53 (-. (p7 zenon_Vle)) % 0.21/0.53 (r1 zenon_Vnf zenon_Vqf) % 0.21/0.53 (r1 Tau_0 Tau_3) % 0.21/0.53 (r1 zenon_Vud zenon_Vde) % 0.21/0.53 (r1 Tau_0 Tau_1) % 0.21/0.53 (r1 zenon_Vyf zenon_Vzf) % 0.21/0.53 (-. (p15 zenon_Vgb)) % 0.21/0.53 (p1 zenon_Vpa) % 0.21/0.53 (r1 zenon_Vcf zenon_Vhf) % 0.21/0.53 (r1 zenon_X4 zenon_Vqa) % 0.21/0.53 (r1 zenon_Vz zenon_Vaa) % 0.21/0.53 (r1 zenon_Vee zenon_Vme) % 0.21/0.53 (r1 zenon_Vif zenon_Vmf) % 0.21/0.53 (p13 zenon_Vic) % 0.21/0.53 (p10 zenon_Vsd) % 0.21/0.53 (p15 zenon_Vfb) % 0.21/0.53 (zenon_Vlf != zenon_Vgf) % 0.21/0.53 (r1 zenon_Vp zenon_Vq) % 0.21/0.53 (-. (p2 zenon_Vpf)) % 0.21/0.53 (zenon_Vub != zenon_Vvb) % 0.21/0.53 (r1 zenon_Vdg zenon_Veg) % 0.21/0.53 (zenon_Vpa != zenon_Vsf) % 0.21/0.53 (p7 zenon_Vte) % 0.21/0.53 (-. (p14 zenon_Vfb)) % 0.21/0.53 (zenon_Vic != zenon_Vub) % 0.21/0.53 (r1 zenon_Vfg zenon_Vgg) % 0.21/0.53 (r1 zenon_Vq zenon_Vr) % 0.21/0.53 (zenon_Vte != zenon_Vle) % 0.21/0.53 (zenon_Vaf != zenon_Vte) % 0.21/0.53 (r1 zenon_Vx zenon_Vy) % 0.21/0.53 (zenon_Vlf != zenon_Vmf) % 0.21/0.53 (p14 zenon_Vub) % 0.21/0.53 (zenon_Vfb != zenon_Vgb) % 0.21/0.53 (r1 zenon_Vgg zenon_Vhg) % 0.21/0.53 (r1 Tau_1 zenon_Vm) % 0.21/0.53 (-. (p6 zenon_Vte)) % 0.21/0.53 (zenon_Vpf != zenon_Vqf) % 0.21/0.53 (-. (p16 zenon_Vqa)) % 0.21/0.53 (r1 zenon_Vhb zenon_Vvb) % 0.21/0.53 (zenon_Vgf != zenon_Vhf) % 0.21/0.53 (r1 zenon_Vy zenon_Vz) % 0.21/0.53 (-. (p5 zenon_Vaf)) % 0.21/0.53 (p3 zenon_Vpf) % 0.21/0.53 (-. (p1 zenon_Vhg)) % 0.21/0.53 (zenon_Vvc != zenon_Vic) % 0.21/0.53 (r1 zenon_Vzf zenon_Vag) % 0.21/0.53 (r1 zenon_Vxf zenon_Vyf) % 0.21/0.53 (p2 zenon_Vsf) % 0.21/0.53 (zenon_Vgf != zenon_Vaf) % 0.21/0.53 (-. (p4 zenon_Vmf)) % 0.21/0.53 (zenon_Vce != zenon_Vsd) % 0.21/0.53 (zenon_Vpa != zenon_Vhg) % 0.21/0.53 (p9 zenon_Vce) % 0.21/0.53 (r1 zenon_Vvf zenon_Vwf) % 0.21/0.53 (r1 zenon_Vr zenon_Vs) % 0.21/0.53 (p5 zenon_Vgf) % 0.21/0.53 (zenon_Vle != zenon_Vce) % 0.21/0.53 (-. (p9 zenon_Vsd)) % 0.21/0.53 (-. (p10 zenon_Vhd)) % 0.21/0.53 (zenon_Vub != zenon_Vfb) % 0.21/0.53 (r1 zenon_Vne zenon_Vue) % 0.21/0.53 (r1 zenon_Vve zenon_Vbf) % 0.21/0.53 (zenon_Vhd != zenon_Vid) % 0.21/0.53 (zenon_Vte != zenon_Vue) % 0.21/0.53 (r1 zenon_Vuf zenon_Vvf) % 0.21/0.53 (r1 zenon_Vwb zenon_Vjc) % 0.21/0.53 (r1 zenon_Vkc zenon_Vwc) % 0.21/0.53 (zenon_Vsd != zenon_Vhd) % 0.21/0.53 (zenon_Vsf != zenon_Vpf) % 0.21/0.53 (r1 zenon_Vs zenon_Vt) % 0.21/0.53 (zenon_Vhd != zenon_Vvc) % 0.21/0.53 (-. (p3 zenon_Vqf)) % 0.21/0.53 (zenon_Vpf != zenon_Vlf) % 0.21/0.53 (-. (p1 zenon_Vsf)) % 0.21/0.53 (-. (p13 zenon_Vjc)) % 0.21/0.53 (p6 zenon_Vaf) % 0.21/0.53 (r1 zenon_Vcg zenon_Vdg) % 0.21/0.53 (r1 zenon_Vv zenon_Vw) % 0.21/0.53 (r1 zenon_Vm zenon_Vn) % 0.21/0.53 (-. (p6 zenon_Vbf)) % 0.21/0.53 (-. (p14 zenon_Vvb)) % 0.21/0.53 (r1 zenon_Vw zenon_Vx) % 0.21/0.53 (r1 zenon_Vtf zenon_Vuf) % 0.21/0.53 (-. (p4 zenon_Vgf)) % 0.21/0.53 (r1 zenon_Vra zenon_Vgb) % 0.21/0.53 (-. (p11 zenon_Vvc)) % 0.21/0.53 (r1 zenon_Vjd zenon_Vtd) % 0.21/0.53 (r1 zenon_Vag zenon_Vbg) % 0.21/0.53 (-. (p10 zenon_Vtd)) % 0.21/0.53 (zenon_Vce != zenon_Vde) % 0.21/0.53 (-. (p5 zenon_Vhf)) % 0.21/0.53 *) % 0.21/0.53 (* NO-PROOF *) % 0.21/0.53 % SZS status GaveUp % 0.21/0.53 Number of rewrites on terms: 0 % 0.21/0.53 Number of rewrites on props: 0 % 0.21/0.53 nodes searched: 522 % 0.21/0.53 max branch formulas: 615 % 0.21/0.53 proof nodes created: 0 % 0.21/0.53 formulas created: 3055 % 0.21/0.53 %------------------------------------------------------------------------------