%------------------------------------------------------------------------------ % File : ZenonModulo---0.5.0 % Problem : LCL662+1.010 : TPTP v9.3.1. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : run_zenon_modulo %d %s % Computer : n028.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:20 PM UTC 2026 % Result : Unknown 10.25s 10.58s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : LCL662+1.010 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.02 % Command : run_zenon_modulo %d %s % 0.07/0.34 % Computer : n028.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 : Sat Sep 5 20:54:00 UTC 2026 % 0.07/0.34 % CPUTime : % 10.25/10.57 Zenon error: exhausted search space without finding a proof % 10.25/10.57 (* Current branch: % 10.25/10.57 (r1 zenon_Vqt zenon_Vrt) % 10.25/10.57 (r1 zenon_Vupa zenon_Vvpa) % 10.25/10.57 (r1 zenon_Vija zenon_Vjja) % 10.25/10.57 (p1 zenon_Vvqa) % 10.25/10.57 (r1 zenon_Vsv zenon_Vtv) % 10.25/10.57 (r1 zenon_Vdqa zenon_Veqa) % 10.25/10.57 (r1 zenon_X2 zenon_Vbcb) % 10.25/10.57 (p1 zenon_Vzs) % 10.25/10.57 (p1 zenon_Vtxa) % 10.25/10.57 (r1 zenon_Vgwa zenon_Vhwa) % 10.25/10.57 (r1 zenon_Vkxa zenon_Vlxa) % 10.25/10.57 (r1 zenon_Vvn zenon_Vwn) % 10.25/10.57 (r1 zenon_Vkaa zenon_Vlaa) % 10.25/10.57 (r1 zenon_X27 zenon_Vxab) % 10.25/10.57 (r1 zenon_Vjka zenon_Vkka) % 10.25/10.57 (r1 zenon_Vaka zenon_Vbka) % 10.25/10.57 (r1 zenon_Vqh zenon_Vrh) % 10.25/10.57 (-. (p1 Tau_0)) % 10.25/10.57 (r1 zenon_Vdd zenon_Ved) % 10.25/10.57 (r1 zenon_Vbia zenon_Vcia) % 10.25/10.57 (r1 zenon_Vzt zenon_Vau) % 10.25/10.57 (p2 zenon_Vlga) % 10.25/10.57 (r1 zenon_Vlda zenon_Vmda) % 10.25/10.57 (r1 zenon_Vff zenon_Vgf) % 10.25/10.57 (r1 zenon_Vqma zenon_Vrma) % 10.25/10.57 (r1 zenon_Vmd zenon_Vnd) % 10.25/10.57 (p1 zenon_Vtia) % 10.25/10.57 (p1 zenon_Vjj) % 10.25/10.57 (zenon_Vxoa != zenon_Vkcb) % 10.25/10.57 (zenon_Vwc != zenon_Vkcb) % 10.25/10.57 (p2 zenon_Vxp) % 10.25/10.57 (r1 zenon_Vgr zenon_Vhr) % 10.25/10.57 (r1 zenon_Vcl zenon_Vdl) % 10.25/10.57 (p2 zenon_Vpwa) % 10.25/10.57 (r1 zenon_Vska zenon_Vtka) % 10.25/10.57 (-. (p1 zenon_Vkcb)) % 10.25/10.57 (r1 zenon_Vpla zenon_Vqla) % 10.25/10.57 (r1 zenon_X26 zenon_Vdab) % 10.25/10.57 (p1 zenon_Vxoa) % 10.25/10.57 (r1 zenon_Vec zenon_Vfc) % 10.25/10.57 (r1 zenon_Vkca zenon_Vlca) % 10.25/10.57 (p1 zenon_Vdea) % 10.25/10.57 (r1 zenon_Vkfa zenon_Vlfa) % 10.25/10.57 (zenon_Vdea != zenon_Vkcb) % 10.25/10.57 (r1 zenon_Vmn zenon_Vnn) % 10.25/10.57 (r1 zenon_Vrra zenon_Vsra) % 10.25/10.57 (zenon_Vjsa != zenon_Vucb) % 10.25/10.57 (p1 zenon_Vbla) % 10.25/10.57 (r1 zenon_Vtfa zenon_Vufa) % 10.25/10.57 (p1 zenon_Vvm) % 10.25/10.57 (r1 zenon_Vjz zenon_Vkz) % 10.25/10.57 (-. (p2 zenon_Vucb)) % 10.25/10.57 (p2 zenon_Vzma) % 10.25/10.57 (r1 zenon_Vjx zenon_Vkx) % 10.25/10.57 (r1 zenon_Vkk zenon_Vlk) % 10.25/10.57 (r1 zenon_Vii zenon_Vji) % 10.25/10.57 (p1 zenon_Vlba) % 10.25/10.57 (r1 zenon_Vmb zenon_Vnb) % 10.25/10.57 (r1 zenon_Vhma zenon_Vima) % 10.25/10.57 (r1 zenon_Vvd zenon_Vwd) % 10.25/10.57 (p2 Tau_0) % 10.25/10.57 (r1 zenon_Vcda zenon_Vdda) % 10.25/10.57 (r1 zenon_Vno zenon_Voo) % 10.25/10.57 (p2 zenon_Vty) % 10.25/10.57 (r1 zenon_Vwo zenon_Vxo) % 10.25/10.57 (r1 zenon_Vsha zenon_Vtha) % 10.25/10.57 (r1 zenon_Vaha zenon_Vbha) % 10.25/10.57 (r1 zenon_Vota zenon_Vpta) % 10.25/10.57 (p2 zenon_Vjsa) % 10.25/10.57 (zenon_Vty != zenon_Vucb) % 10.25/10.57 (r1 zenon_Vfya zenon_Vgya) % 10.25/10.57 (zenon_Vtxa != zenon_Vkcb) % 10.25/10.57 (r1 zenon_Viu zenon_Vju) % 10.25/10.57 (r1 zenon_Voq zenon_Vpq) % 10.25/10.57 (r1 zenon_Vbxa zenon_Vcxa) % 10.25/10.57 (p2 zenon_Vrza) % 10.25/10.57 (zenon_Vlga != zenon_Vucb) % 10.25/10.57 (r1 zenon_Vbaa zenon_Vcaa) % 10.25/10.57 (r1 zenon_Vtca zenon_Vuca) % 10.25/10.57 (r1 zenon_Vcba zenon_Vdba) % 10.25/10.57 (r1 zenon_Vul zenon_Vvl) % 10.25/10.57 (r1 zenon_Vby zenon_Vcy) % 10.25/10.57 (r1 zenon_Vjv zenon_Vkv) % 10.25/10.57 (p1 zenon_Vbw) % 10.25/10.57 (r1 zenon_Vhh zenon_Vih) % 10.25/10.57 (r1 zenon_Vt zenon_Vu) % 10.25/10.57 (Tau_0 != zenon_Vucb) % 10.25/10.57 (zenon_Vfbb != zenon_Vkcb) % 10.25/10.57 (r1 zenon_Veo zenon_Vfo) % 10.25/10.57 (r1 zenon_Vll zenon_Vml) % 10.25/10.57 (zenon_Vpwa != zenon_Vucb) % 10.25/10.57 (r1 zenon_Vfoa zenon_Vgoa) % 10.25/10.57 (zenon_Vlba != zenon_Vkcb) % 10.25/10.57 (r1 zenon_Vxva zenon_Vyva) % 10.25/10.57 (r1 zenon_Vri zenon_Vsi) % 10.25/10.57 (p1 zenon_Vwc) % 10.25/10.57 (zenon_Vbw != zenon_Vkcb) % 10.25/10.57 (r1 zenon_Vxq zenon_Vyq) % 10.25/10.57 (r1 zenon_X25 zenon_Vjza) % 10.25/10.57 (r1 zenon_Vla zenon_Vma) % 10.25/10.57 (r1 zenon_Vax zenon_Vbx) % 10.25/10.57 (r1 zenon_Vmqa zenon_Vnqa) % 10.25/10.57 (r1 zenon_Vdm zenon_Vem) % 10.25/10.57 (zenon_Vxya != zenon_Vkcb) % 10.25/10.57 (zenon_Vvqa != zenon_Vkcb) % 10.25/10.57 (p1 zenon_Vxta) % 10.25/10.57 (zenon_Vxp != zenon_Vucb) % 10.25/10.57 (r1 zenon_Vru zenon_Vsu) % 10.25/10.57 (r1 zenon_Vky zenon_Vly) % 10.25/10.57 (r1 zenon_Vcga zenon_Vdga) % 10.25/10.57 (r1 zenon_Vira zenon_Vjra) % 10.25/10.57 (r1 zenon_Vnna zenon_Vona) % 10.25/10.57 (r1 zenon_Vrja zenon_Vsja) % 10.25/10.57 (r1 zenon_Vyr zenon_Vzr) % 10.25/10.57 (zenon_Vbla != zenon_Vkcb) % 10.25/10.57 (r1 zenon_Vnc zenon_Voc) % 10.25/10.57 (p1 zenon_Vlva) % 10.25/10.57 (r1 zenon_Vua zenon_Vva) % 10.25/10.57 (p1 zenon_Vxya) % 10.25/10.57 (zenon_Vlva != zenon_Vkcb) % 10.25/10.57 (r1 zenon_Vwsa zenon_Vxsa) % 10.25/10.57 (r1 zenon_Vpg zenon_Vqg) % 10.25/10.57 (zenon_Vzma != zenon_Vucb) % 10.25/10.57 (r1 zenon_Vee zenon_Vfe) % 10.25/10.57 (r1 zenon_Vhs zenon_Vis) % 10.25/10.57 (r1 zenon_Vtua zenon_Vuua) % 10.25/10.57 (zenon_Vvm != zenon_Vkcb) % 10.25/10.57 (r1 zenon_Vasa zenon_Vbsa) % 10.25/10.57 (r1 zenon_Vaj zenon_Vbj) % 10.25/10.57 (zenon_Vzs != zenon_Vkcb) % 10.25/10.57 (r1 zenon_Vdb zenon_Veb) % 10.25/10.57 (r1 zenon_Vof zenon_Vpf) % 10.25/10.57 (r1 zenon_Vqs zenon_Vrs) % 10.25/10.57 (r1 zenon_Vmm zenon_Vnm) % 10.25/10.57 (r1 zenon_Vvb zenon_Vwb) % 10.25/10.57 (zenon_Vxta != zenon_Vkcb) % 10.25/10.57 (p1 zenon_Vfbb) % 10.25/10.57 (r1 zenon_Vne zenon_Voe) % 10.25/10.57 (r1 zenon_Vzh zenon_Vai) % 10.25/10.57 (r1 zenon_Vooa zenon_Vpoa) % 10.25/10.57 (r1 zenon_Vca zenon_Vda) % 10.25/10.57 (zenon_Vwc != Tau_0) % 10.25/10.57 (zenon_Vjj != Tau_0) % 10.25/10.57 (zenon_Vvm != Tau_0) % 10.25/10.57 (zenon_Vzs != Tau_0) % 10.25/10.57 (zenon_Vbw != Tau_0) % 10.25/10.57 (zenon_Vlba != Tau_0) % 10.25/10.57 (zenon_Vdea != Tau_0) % 10.25/10.57 (zenon_Vtia != Tau_0) % 10.25/10.57 (zenon_Vbla != Tau_0) % 10.25/10.57 (zenon_Vxoa != Tau_0) % 10.25/10.57 (zenon_Vvqa != Tau_0) % 10.25/10.57 (zenon_Vxta != Tau_0) % 10.25/10.57 (zenon_Vlva != Tau_0) % 10.25/10.57 (zenon_Vtxa != Tau_0) % 10.25/10.57 (zenon_Vxya != Tau_0) % 10.25/10.57 (zenon_Vlab != Tau_0) % 10.25/10.57 (zenon_Vfbb != Tau_0) % 10.25/10.57 (r1 zenon_Vwe zenon_Vxe) % 10.25/10.57 (r1 zenon_Vfp zenon_Vgp) % 10.25/10.57 (zenon_Vtia != zenon_Vkcb) % 10.25/10.57 (r1 zenon_Vsz zenon_Vtz) % 10.25/10.57 (r1 zenon_Vlpa zenon_Vmpa) % 10.25/10.57 (zenon_Vxf != zenon_Vucb) % 10.25/10.57 (r1 zenon_Vkia zenon_Vlia) % 10.25/10.57 (r1 zenon_Vkua zenon_Vlua) % 10.25/10.57 (r1 zenon_Vpr zenon_Vqr) % 10.25/10.57 (zenon_Vlab != zenon_Vkcb) % 10.25/10.58 (r1 zenon_Vav zenon_Vbv) % 10.25/10.58 (r1 zenon_Vbfa zenon_Vcfa) % 10.25/10.58 (r1 zenon_Vbk zenon_Vck) % 10.25/10.58 (zenon_Vrza != zenon_Vucb) % 10.25/10.58 (r1 zenon_X1 zenon_Vlcb) % 10.25/10.58 (r1 zenon_Voya zenon_Vpya) % 10.25/10.58 (r1 zenon_Vsea zenon_Vtea) % 10.25/10.58 (r1 zenon_Vwna zenon_Vxna) % 10.25/10.58 (r1 zenon_Vyla zenon_Vzla) % 10.25/10.58 (r1 zenon_Vop zenon_Vpp) % 10.25/10.58 (r1 zenon_Vtaa zenon_Vuaa) % 10.25/10.58 (r1 zenon_Vrw zenon_Vsw) % 10.25/10.58 (r1 zenon_Vuda zenon_Vvda) % 10.25/10.58 (p2 zenon_Vxf) % 10.25/10.58 (r1 zenon_Vsx zenon_Vtx) % 10.25/10.58 (r1 zenon_Vcva zenon_Vdva) % 10.25/10.58 (r1 zenon_Vyg zenon_Vzg) % 10.25/10.58 (r1 zenon_Vbca zenon_Vcca) % 10.25/10.58 (r1 zenon_Vjha zenon_Vkha) % 10.25/10.58 (p1 zenon_Vlab) % 10.25/10.58 (r1 zenon_Vfta zenon_Vgta) % 10.25/10.58 (r1 zenon_Vtk zenon_Vuk) % 10.25/10.58 (zenon_Vjj != zenon_Vkcb) % 10.25/10.58 *) % 10.25/10.58 (* NO-PROOF *) % 10.25/10.58 % SZS status GaveUp % 10.25/10.58 Number of rewrites on terms: 0 % 10.25/10.58 Number of rewrites on props: 0 % 10.25/10.58 nodes searched: 2677 % 10.25/10.58 max branch formulas: 2822 % 10.25/10.58 proof nodes created: 2 % 10.25/10.58 formulas created: 13368 % 10.25/10.58 %------------------------------------------------------------------------------