%------------------------------------------------------------------------------ % File : ZenonModulo---0.5.0 % Problem : LCL665+1.015 : TPTP v9.3.1. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : run_zenon_modulo %d %s % Computer : n001.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:21 PM UTC 2026 % Result : Unknown 116.93s 117.24s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LCL665+1.015 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.03 % Command : run_zenon_modulo %d %s % 0.08/0.35 % Computer : n001.cluster.edu % 0.08/0.35 % Model : x86_64 x86_64 % 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.35 % Memory : 8046.5625MB % 0.08/0.35 % OS : Linux 6.8.0-71-generic % 0.08/0.35 % CPULimit : 300 % 0.08/0.35 % WCLimit : 300 % 0.08/0.35 % DateTime : Fri Sep 4 20:24:15 UTC 2026 % 0.08/0.35 % CPUTime : % 116.93/117.23 Zenon error: exhausted search space without finding a proof % 116.93/117.23 (* Current branch: % 116.93/117.23 (p121 zenon_Vgla) % 116.93/117.23 (p161 zenon_Vpa) % 116.93/117.23 (p74 zenon_Vidb) % 116.93/117.23 (p25 zenon_Vjvb) % 116.93/117.23 (-. (p11 Tau_4)) % 116.93/117.23 (-. (p25 zenon_Viwb)) % 116.93/117.23 (p115 zenon_Vvma) % 116.93/117.23 (p82 zenon_Vccb) % 116.93/117.23 (p71 zenon_Vdlb) % 116.93/117.23 (p113 zenon_Vgpa) % 116.93/117.23 (p132 zenon_Vbp) % 116.93/117.23 (p74 zenon_Vggb) % 116.93/117.23 (p33 zenon_Vmub) % 116.93/117.23 (p81 zenon_Vwgb) % 116.93/117.23 (zenon_X241 != Tau_2) % 116.93/117.23 (p44 zenon_Vxob) % 116.93/117.23 (p144 zenon_Vgg) % 116.93/117.23 (p36 zenon_Vxtb) % 116.93/117.23 (p53 zenon_Vmqb) % 116.93/117.23 (-. (p21 zenon_Vhwb)) % 116.93/117.23 (p16 zenon_X222) % 116.93/117.23 (p64 zenon_Vqhb) % 116.93/117.23 (zenon_X239 != Tau_1) % 116.93/117.23 (zenon_Vjvb != zenon_Vdwb) % 116.93/117.23 (p123 zenon_Vqha) % 116.93/117.23 (p63 zenon_Vnnb) % 116.93/117.23 (p86 zenon_Vnza) % 116.93/117.23 (p154 zenon_Vdk) % 116.93/117.23 (p73 zenon_Vqjb) % 116.93/117.23 (p85 zenon_Vqdb) % 116.93/117.23 (p103 zenon_Vjva) % 116.93/117.23 (p156 zenon_Vhc) % 116.93/117.23 (p143 zenon_Vfs) % 116.93/117.23 (p43 zenon_Vwsb) % 116.93/117.23 (p46 zenon_Vqqb) % 116.93/117.23 (p112 zenon_Veha) % 116.93/117.23 (r1 Tau_2 zenon_Vfwb) % 116.93/117.23 (p104 zenon_Vama) % 116.93/117.23 (p71 zenon_Vwkb) % 116.93/117.23 (p76 zenon_Vzfb) % 116.93/117.23 (p112 zenon_Vyea) % 116.93/117.23 (p141 zenon_Vvu) % 116.93/117.23 (p52 zenon_Vnlb) % 116.93/117.23 (p116 zenon_Vtga) % 116.93/117.23 (zenon_Vfvb != zenon_Viwb) % 116.93/117.23 (p146 zenon_Vvl) % 116.93/117.23 (p125 zenon_Viga) % 116.93/117.23 (p153 zenon_Vhl) % 116.93/117.23 (p84 zenon_Vubb) % 116.93/117.23 (p26 zenon_Vrub) % 116.93/117.23 (zenon_Vrvb != zenon_Vewb) % 116.93/117.23 (p123 zenon_Vcia) % 116.93/117.23 (p136 zenon_Voo) % 116.93/117.23 (p62 zenon_Vikb) % 116.93/117.23 (p23 zenon_Vpvb) % 116.93/117.23 (p56 zenon_Vkmb) % 116.93/117.23 (p45 zenon_Vesb) % 116.93/117.23 (p24 zenon_Vstb) % 116.93/117.23 (p141 zenon_Vxv) % 116.93/117.23 (p144 zenon_Vaj) % 116.93/117.23 (p162 zenon_Vtb) % 116.93/117.23 (p32 zenon_Vksb) % 116.93/117.23 (p124 zenon_Vjx) % 116.93/117.23 (-. (p23 zenon_Vgwb)) % 116.93/117.23 (p22 zenon_Vjub) % 116.93/117.23 (zenon_Vpvb != zenon_Vjwb) % 116.93/117.23 (p31 zenon_Vyub) % 116.93/117.23 (r1 Tau_3 zenon_Vhwb) % 116.93/117.23 (p15 zenon_X239) % 116.93/117.23 (p83 zenon_Vsfb) % 116.93/117.23 (zenon_Vnvb != zenon_Vgwb) % 116.93/117.23 (p45 zenon_Vasb) % 116.93/117.23 (p101 zenon_Vlwa) % 116.93/117.23 (r1 Tau_4 zenon_Vjwb) % 116.93/117.23 (p21 zenon_Vxvb) % 116.93/117.23 (p132 zenon_Vhu) % 116.93/117.23 (zenon_Vxvb != zenon_Vhwb) % 116.93/117.23 (p94 zenon_Vmab) % 116.93/117.23 (r1 Tau_0 Tau_3) % 116.93/117.23 (p63 zenon_Vbnb) % 116.93/117.23 (p144 zenon_Vjm) % 116.93/117.23 (p82 zenon_Vnya) % 116.93/117.23 (p76 zenon_Vneb) % 116.93/117.23 (p25 zenon_Vhvb) % 116.93/117.23 (p74 zenon_Vueb) % 116.93/117.23 (p151 zenon_Vmn) % 116.93/117.23 (r1 Tau_0 Tau_2) % 116.93/117.23 (p21 zenon_Vzvb) % 116.93/117.23 (p55 zenon_Vlpb) % 116.93/117.23 (zenon_X240 != Tau_2) % 116.93/117.23 (p73 zenon_Vjjb) % 116.93/117.23 (p111 zenon_Vgra) % 116.93/117.23 (p65 zenon_Vfmb) % 116.93/117.23 (p115 zenon_Vgna) % 116.93/117.23 (p156 zenon_Vpe) % 116.93/117.23 (p43 zenon_Vosb) % 116.93/117.23 (p102 zenon_Vkoa) % 116.93/117.23 (p75 zenon_Vdib) % 116.93/117.23 (p35 zenon_Vdub) % 116.93/117.23 (p23 zenon_Vnvb) % 116.93/117.23 (p142 zenon_Voj) % 116.93/117.23 (zenon_X242 != Tau_3) % 116.93/117.23 (p96 zenon_Vsva) % 116.93/117.23 (p95 zenon_Vwya) % 116.93/117.23 (p35 zenon_Vaub) % 116.93/117.23 (p143 zenon_Vht) % 116.93/117.23 (p52 zenon_Vpmb) % 116.93/117.23 (p11 zenon_X243) % 116.93/117.23 (zenon_Vfvb != zenon_Vdwb) % 116.93/117.23 (p135 zenon_Viy) % 116.93/117.23 (p16 zenon_X227) % 116.93/117.23 (p64 zenon_Vwib) % 116.93/117.23 (p145 zenon_Vrq) % 116.93/117.23 (p156 zenon_Vld) % 116.93/117.23 (p114 zenon_Vvoa) % 116.93/117.23 (p133 zenon_Vsba) % 116.93/117.23 (p14 zenon_X228) % 116.93/117.23 (p72 zenon_Vpkb) % 116.93/117.23 (zenon_Vjvb != zenon_Vfwb) % 116.93/117.23 (p21 zenon_Vvvb) % 116.93/117.23 (p33 zenon_Vpub) % 116.93/117.23 (p45 zenon_Vwrb) % 116.93/117.23 (p122 zenon_Vfaa) % 116.93/117.23 (p101 zenon_Vvwa) % 116.93/117.23 (p152 zenon_Vwc) % 116.93/117.23 (p34 zenon_Vzsb) % 116.93/117.23 (p45 zenon_Vsrb) % 116.93/117.23 (p66 zenon_Vwjb) % 116.93/117.23 (p26 zenon_Vqtb) % 116.93/117.23 (p54 zenon_Vcqb) % 116.93/117.23 (p126 zenon_Vxw) % 116.93/117.23 (p92 zenon_Vfua) % 116.93/117.23 (p41 zenon_Vgtb) % 116.93/117.23 (p141 zenon_Vjv) % 116.93/117.23 (p132 zenon_Vrr) % 116.93/117.23 (p142 zenon_Vug) % 116.93/117.23 (p41 zenon_Votb) % 116.93/117.23 (p103 zenon_Vzua) % 116.93/117.23 (p113 zenon_Vrpa) % 116.93/117.23 (p111 zenon_Vrra) % 116.93/117.23 (p16 zenon_X232) % 116.93/117.23 (p66 zenon_Vkhb) % 116.93/117.23 (p116 zenon_Vnea) % 116.93/117.23 (p34 zenon_Vlrb) % 116.93/117.23 (p86 zenon_Vxxa) % 116.93/117.23 (p81 zenon_Vogb) % 116.93/117.23 (p53 zenon_Vhqb) % 116.93/117.23 (p106 zenon_Vqla) % 116.93/117.23 (-. (p25 zenon_Vfwb)) % 116.93/117.23 (p91 zenon_Vucb) % 116.93/117.23 (p83 zenon_Vkfb) % 116.93/117.23 (p34 zenon_Vhsb) % 116.93/117.23 (-. (p15 Tau_1)) % 116.93/117.23 (p92 zenon_Vbwa) % 116.93/117.23 (zenon_Vhvb != zenon_Vfwb) % 116.93/117.23 (p42 zenon_Vyqb) % 116.93/117.23 (zenon_Vnvb != zenon_Vewb) % 116.93/117.23 (p64 zenon_Vckb) % 116.93/117.23 (p116 zenon_Vzia) % 116.93/117.23 (p146 zenon_Vsf) % 116.93/117.23 (p25 zenon_Vfvb) % 116.93/117.23 (p155 zenon_Vjh) % 116.93/117.23 (zenon_Vhvb != zenon_Viwb) % 116.93/117.23 (p82 zenon_Vdab) % 116.93/117.23 (p13 zenon_X240) % 116.93/117.23 (p85 zenon_Vgeb) % 116.93/117.23 (-. (p12 Tau_3)) % 116.93/117.23 (p21 zenon_Vbwb) % 116.93/117.23 (p44 zenon_Vuqb) % 116.93/117.23 (p143 zenon_Vts) % 116.93/117.23 (p42 zenon_Vbpb) % 116.93/117.23 (p102 zenon_Vvqa) % 116.93/117.23 (p65 zenon_Vtlb) % 116.93/117.23 (p84 zenon_Vfya) % 116.93/117.23 (p121 zenon_Vuka) % 116.93/117.23 (p102 zenon_Vkma) % 116.93/117.23 (p84 zenon_Vvza) % 116.93/117.23 (zenon_Vfvb != zenon_Vfwb) % 116.93/117.23 (p122 zenon_Vcda) % 116.93/117.23 (p112 zenon_Vkja) % 116.93/117.23 (p56 zenon_Vilb) % 116.93/117.23 (p66 zenon_Vqib) % 116.93/117.23 (p92 zenon_Vjsa) % 116.93/117.23 (p166 zenon_Vaa) % 116.93/117.23 (p75 zenon_Vkib) % 116.93/117.23 (p62 zenon_Vwhb) % 116.93/117.23 (p125 zenon_Vwfa) % 116.93/117.23 (p146 zenon_Vmi) % 116.93/117.23 (p101 zenon_Vpxa) % 116.93/117.23 (p51 zenon_Virb) % 116.93/117.23 (p101 zenon_Vfxa) % 116.93/117.23 (r1 Tau_2 zenon_Vgwb) % 116.93/117.23 (p14 zenon_X233) % 116.93/117.23 (p43 zenon_Vssb) % 116.93/117.23 (p76 zenon_Vbdb) % 116.93/117.23 (p145 zenon_Vpp) % 116.93/117.23 (p83 zenon_Vcfb) % 116.93/117.23 (p63 zenon_Vhnb) % 116.93/117.23 (r1 Tau_0 Tau_4) % 116.93/117.23 (zenon_Vpvb != zenon_Vgwb) % 116.93/117.23 (p152 zenon_Vef) % 116.93/117.23 (p41 zenon_Vktb) % 116.93/117.23 (p131 zenon_Vcea) % 116.93/117.23 (p105 zenon_Vdta) % 116.93/117.23 (zenon_Vrvb != zenon_Vgwb) % 116.93/117.23 (p32 zenon_Vorb) % 116.93/117.23 (p86 zenon_Vmbb) % 116.93/117.23 (p122 zenon_Vvx) % 116.93/117.23 (r1 Tau_0 Tau_1) % 116.93/117.23 (p104 zenon_Vaoa) % 116.93/117.23 (p61 zenon_Vdob) % 116.93/117.23 (p91 zenon_Vlcb) % 116.93/117.23 (p145 zenon_Vdq) % 116.93/117.23 (zenon_X244 != Tau_4) % 116.93/117.23 (p12 zenon_X242) % 116.93/117.23 (p31 zenon_Vbvb) % 116.93/117.23 (zenon_Vjvb != zenon_Viwb) % 116.93/117.23 (p134 zenon_Vsaa) % 116.93/117.23 (p124 zenon_Vqca) % 116.93/117.23 (p125 zenon_Vkfa) % 116.93/117.23 (zenon_Vpvb != zenon_Vewb) % 116.93/117.24 (p153 zenon_Vsk) % 116.93/117.24 (p61 zenon_Vpob) % 116.93/117.24 (p46 zenon_Vppb) % 116.93/117.24 (p32 zenon_Vctb) % 116.93/117.24 (p104 zenon_Vlqa) % 116.93/117.24 (p164 zenon_Veb) % 116.93/117.24 (p152 zenon_Vae) % 116.93/117.24 (p15 zenon_X238) % 116.93/117.24 (p103 zenon_Vpua) % 116.93/117.24 (-. (p23 zenon_Vewb)) % 116.93/117.24 (p121 zenon_Vika) % 116.93/117.24 (zenon_Vhvb != zenon_Vdwb) % 116.93/117.24 (p96 zenon_Vasa) % 116.93/117.24 (p105 zenon_Vtsa) % 116.93/117.24 (p24 zenon_Vhub) % 116.93/117.24 (p26 zenon_Vfub) % 116.93/117.24 (p93 zenon_Vvab) % 116.93/117.24 (zenon_Vbwb != zenon_Vhwb) % 116.93/117.24 (p93 zenon_Vebb) % 116.93/117.24 (p11 zenon_X244) % 116.93/117.24 (p13 zenon_X241) % 116.93/117.24 (p23 zenon_Vrvb) % 116.93/117.24 (p136 zenon_Vut) % 116.93/117.24 (p85 zenon_Vydb) % 116.93/117.24 (p133 zenon_Vfba) % 116.93/117.24 (p65 zenon_Vzlb) % 116.93/117.24 (-. (p23 zenon_Vjwb)) % 116.93/117.24 (p105 zenon_Vnta) % 116.93/117.24 (p106 zenon_Vbqa) % 116.93/117.24 (zenon_Vrvb != zenon_Vjwb) % 116.93/117.24 (p63 zenon_Vvmb) % 116.93/117.24 (p151 zenon_Vbo) % 116.93/117.24 (-. (p13 Tau_2)) % 116.93/117.24 (p61 zenon_Vjob) % 116.93/117.24 (zenon_Vnvb != zenon_Vjwb) % 116.93/117.24 (-. (p25 zenon_Vdwb)) % 116.93/117.24 (p22 zenon_Vvub) % 116.93/117.24 (p126 zenon_Veca) % 116.93/117.24 (p136 zenon_Ver) % 116.93/117.24 (p126 zenon_Vhz) % 116.93/117.24 (p52 zenon_Vxnb) % 116.93/117.24 (p106 zenon_Vqna) % 116.93/117.24 (p95 zenon_Vfza) % 116.93/117.24 (p135 zenon_Vvy) % 116.93/117.24 (p42 zenon_Vxpb) % 116.93/117.24 (p56 zenon_Vsnb) % 116.93/117.24 (p123 zenon_Voia) % 116.93/117.24 (r1 Tau_1 zenon_Vdwb) % 116.93/117.24 (p62 zenon_Vcjb) % 116.93/117.24 (zenon_X243 != Tau_4) % 116.93/117.24 (p44 zenon_Vtpb) % 116.93/117.24 (p96 zenon_Vwta) % 116.93/117.24 (p121 zenon_Vwja) % 116.93/117.24 (zenon_Vvvb != zenon_Vhwb) % 116.93/117.24 (p81 zenon_Vehb) % 116.93/117.24 (r1 Tau_4 zenon_Viwb) % 116.93/117.24 (p131 zenon_Vpda) % 116.93/117.24 (r1 Tau_1 zenon_Vewb) % 116.93/117.24 (p55 zenon_Vgpb) % 116.93/117.24 (p14 zenon_X223) % 116.93/117.24 (zenon_Vzvb != zenon_Vhwb) % 116.93/117.24 (p24 zenon_Vtub) % 116.93/117.24 (p155 zenon_Vyh) % 116.93/117.24 (p22 zenon_Vutb) % 116.93/117.24 (zenon_X238 != Tau_1) % 116.93/117.24 (p141 zenon_Vlw) % 116.93/117.24 (p124 zenon_Vtz) % 116.93/117.24 (p51 zenon_Vdrb) % 116.93/117.24 (p142 zenon_Vxm) % 116.93/117.24 (p46 zenon_Vtob) % 116.93/117.24 *) % 116.93/117.24 (* NO-PROOF *) % 116.93/117.24 % SZS status GaveUp % 116.93/117.24 Number of rewrites on terms: 0 % 116.93/117.24 Number of rewrites on props: 0 % 116.93/117.24 nodes searched: 4005 % 116.93/117.24 max branch formulas: 4238 % 116.93/117.24 proof nodes created: 14 % 116.93/117.24 formulas created: 26361 % 116.93/117.24 %------------------------------------------------------------------------------