%------------------------------------------------------------------------------ % File : ZenonModulo---0.5.0 % Problem : LCL683+1.005 : TPTP v9.3.1. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : run_zenon_modulo %d %s % Computer : n005.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:28 PM UTC 2026 % Result : Unknown 0.94s 1.29s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.04 % Problem : LCL683+1.005 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.04 % Command : run_zenon_modulo %d %s % 0.13/0.39 % Computer : n005.cluster.edu % 0.13/0.39 % Model : x86_64 x86_64 % 0.13/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.39 % Memory : 8046.5625MB % 0.13/0.39 % OS : Linux 6.8.0-71-generic % 0.13/0.39 % CPULimit : 300 % 0.13/0.39 % WCLimit : 300 % 0.13/0.39 % DateTime : Sun Sep 6 01:58:05 UTC 2026 % 0.13/0.39 % CPUTime : % 0.94/1.29 Zenon error: exhausted search space without finding a proof % 0.94/1.29 (* Current branch: % 0.94/1.29 (zenon_Vjh != zenon_Vii) % 0.94/1.29 (p31 zenon_Vbh) % 0.94/1.29 (p43 zenon_Vze) % 0.94/1.29 (p44 zenon_Vbc) % 0.94/1.29 (-. (p23 zenon_Vei)) % 0.94/1.29 (p22 zenon_Vjg) % 0.94/1.29 (p24 zenon_Vvf) % 0.94/1.29 (p46 zenon_Vtc) % 0.94/1.29 (zenon_Vph != zenon_Vji) % 0.94/1.29 (p35 zenon_Vag) % 0.94/1.29 (zenon_Vzh != zenon_Vhi) % 0.94/1.29 (p15 zenon_X76) % 0.94/1.29 (-. (p11 zenon_Vni)) % 0.94/1.29 (p11 zenon_X80) % 0.94/1.29 (zenon_Vbi != zenon_Vhi) % 0.94/1.29 (p23 zenon_Vnh) % 0.94/1.29 (p15 zenon_X75) % 0.94/1.29 (p13 zenon_X77) % 0.94/1.29 (zenon_X80 != zenon_Vni) % 0.94/1.29 (p54 zenon_Vda) % 0.94/1.29 (-. (p15 zenon_Vki)) % 0.94/1.29 (zenon_Vjh != zenon_Vfi) % 0.94/1.29 (-. (p25 zenon_Vdi)) % 0.94/1.29 (p41 zenon_Vjf) % 0.94/1.29 (p22 zenon_Vvg) % 0.94/1.29 (p52 zenon_Vsa) % 0.94/1.29 (zenon_X81 != zenon_Vni) % 0.94/1.29 (p55 zenon_Vtb) % 0.94/1.29 (r1 zenon_Vki zenon_Vdi) % 0.94/1.29 (p51 zenon_Vgd) % 0.94/1.29 (r1 zenon_Vli zenon_Vgi) % 0.94/1.29 (p34 zenon_Vge) % 0.94/1.29 (-. (p13 zenon_Vli)) % 0.94/1.29 (p26 zenon_Vfg) % 0.94/1.29 (p43 zenon_Vve) % 0.94/1.29 (r1 zenon_Vni zenon_Vji) % 0.94/1.29 (r1 Tau_0 Tau_4) % 0.94/1.29 (p45 zenon_Vvd) % 0.94/1.29 (p23 zenon_Vrh) % 0.94/1.29 (p54 zenon_Vt) % 0.94/1.29 (p26 zenon_Vtf) % 0.94/1.29 (r1 Tau_1 zenon_Vki) % 0.94/1.29 (p42 zenon_Vfc) % 0.94/1.29 (p14 zenon_X60) % 0.94/1.29 (p13 zenon_X78) % 0.94/1.29 (p12 zenon_X79) % 0.94/1.29 (zenon_Vrh != zenon_Vji) % 0.94/1.29 (p43 zenon_Vre) % 0.94/1.29 (p53 zenon_Vkc) % 0.94/1.29 (r1 Tau_4 zenon_Vni) % 0.94/1.29 (p62 zenon_Vp) % 0.94/1.29 (p44 zenon_Vxc) % 0.94/1.29 (p31 zenon_Vyg) % 0.94/1.29 (-. (p25 zenon_Vii)) % 0.94/1.29 (p32 zenon_Vje) % 0.94/1.29 (p26 zenon_Vrg) % 0.94/1.29 (p34 zenon_Vod) % 0.94/1.29 (zenon_X77 != zenon_Vli) % 0.94/1.29 (p64 zenon_Vo) % 0.94/1.29 (r1 zenon_Vli zenon_Vfi) % 0.94/1.29 (p16 zenon_X69) % 0.94/1.29 (zenon_X76 != zenon_Vki) % 0.94/1.29 (zenon_Vnh != zenon_Vei) % 0.94/1.29 (p34 zenon_Vcf) % 0.94/1.29 (p35 zenon_Vdg) % 0.94/1.29 (-. (p23 zenon_Vji)) % 0.94/1.29 (zenon_X75 != zenon_Vki) % 0.94/1.29 (p41 zenon_Vrf) % 0.94/1.29 (-. (p25 zenon_Vfi)) % 0.94/1.29 (zenon_Vph != zenon_Vei) % 0.94/1.29 (p54 zenon_Vna) % 0.94/1.29 (zenon_Vfh != zenon_Vdi) % 0.94/1.29 (p52 zenon_Via) % 0.94/1.29 (zenon_Vnh != zenon_Vji) % 0.94/1.29 (r1 Tau_0 Tau_3) % 0.94/1.29 (zenon_Vfh != zenon_Vfi) % 0.94/1.29 (p53 zenon_Vpc) % 0.94/1.29 (p25 zenon_Vfh) % 0.94/1.29 (p66 zenon_Vm) % 0.94/1.29 (p14 zenon_X70) % 0.94/1.29 (-. (p12 zenon_Vmi)) % 0.94/1.29 (p33 zenon_Vmg) % 0.94/1.29 (zenon_Vvh != zenon_Vhi) % 0.94/1.29 (p56 zenon_Vjb) % 0.94/1.29 (p25 zenon_Vhh) % 0.94/1.29 (p21 zenon_Vzh) % 0.94/1.29 (r1 Tau_2 zenon_Vli) % 0.94/1.29 (p11 zenon_X81) % 0.94/1.29 (p24 zenon_Vhg) % 0.94/1.29 (zenon_Vph != zenon_Vgi) % 0.94/1.29 (p21 zenon_Vbi) % 0.94/1.29 (p32 zenon_Vrd) % 0.94/1.29 (p33 zenon_Vpg) % 0.94/1.29 (p43 zenon_Vne) % 0.94/1.29 (zenon_X79 != zenon_Vmi) % 0.94/1.29 (r1 Tau_0 Tau_1) % 0.94/1.29 (zenon_Vxh != zenon_Vhi) % 0.94/1.29 (zenon_X78 != zenon_Vli) % 0.94/1.29 (p44 zenon_Vab) % 0.94/1.29 (p16 zenon_X64) % 0.94/1.29 (p46 zenon_Vxb) % 0.94/1.29 (r1 zenon_Vki zenon_Vei) % 0.94/1.29 (r1 Tau_0 Tau_2) % 0.94/1.29 (-. (p21 zenon_Vhi)) % 0.94/1.29 (zenon_Vhh != zenon_Vii) % 0.94/1.29 (zenon_Vfh != zenon_Vii) % 0.94/1.29 (p52 zenon_Vy) % 0.94/1.29 (p55 zenon_Vob) % 0.94/1.29 (r1 zenon_Vni zenon_Vii) % 0.94/1.29 (p21 zenon_Vvh) % 0.94/1.29 (p63 zenon_Vn) % 0.94/1.29 (p24 zenon_Vtg) % 0.94/1.29 (zenon_Vnh != zenon_Vgi) % 0.94/1.29 (p21 zenon_Vxh) % 0.94/1.29 (p45 zenon_Vde) % 0.94/1.29 (p25 zenon_Vjh) % 0.94/1.29 (p23 zenon_Vph) % 0.94/1.29 (zenon_Vrh != zenon_Vei) % 0.94/1.29 (p42 zenon_Vbd) % 0.94/1.29 (r1 Tau_3 zenon_Vmi) % 0.94/1.29 (p46 zenon_Vwa) % 0.94/1.29 (-. (p23 zenon_Vgi)) % 0.94/1.29 (p14 zenon_X65) % 0.94/1.29 (zenon_Vhh != zenon_Vdi) % 0.94/1.29 (zenon_Vjh != zenon_Vdi) % 0.94/1.29 (r1 zenon_Vmi zenon_Vhi) % 0.94/1.29 (p32 zenon_Vff) % 0.94/1.29 (p16 zenon_X59) % 0.94/1.29 (zenon_Vrh != zenon_Vgi) % 0.94/1.29 (p45 zenon_Vzd) % 0.94/1.29 (p51 zenon_Vld) % 0.94/1.29 (p22 zenon_Vxf) % 0.94/1.29 (p42 zenon_Veb) % 0.94/1.29 (zenon_Vhh != zenon_Vfi) % 0.94/1.29 (p41 zenon_Vnf) % 0.94/1.29 *) % 0.94/1.29 (* NO-PROOF *) % 0.94/1.29 % SZS status GaveUp % 0.94/1.29 Number of rewrites on terms: 0 % 0.94/1.29 Number of rewrites on props: 4 % 0.94/1.29 nodes searched: 585 % 0.94/1.29 max branch formulas: 657 % 0.94/1.29 proof nodes created: 19 % 0.94/1.29 formulas created: 5196 % 0.94/1.29 %------------------------------------------------------------------------------