%------------------------------------------------------------------------------ % File : ZenonModulo---0.5.0 % Problem : LCL640+1.015 : 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:12 PM UTC 2026 % Result : Unknown 0.21s 0.49s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : LCL640+1.015 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.02 % Command : run_zenon_modulo %d %s % 0.06/0.32 % Computer : n028.cluster.edu % 0.06/0.32 % Model : x86_64 x86_64 % 0.06/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.06/0.32 % Memory : 8046.5625MB % 0.06/0.32 % OS : Linux 6.8.0-71-generic % 0.06/0.32 % CPULimit : 300 % 0.06/0.32 % WCLimit : 300 % 0.06/0.32 % DateTime : Sat Sep 5 18:06:44 UTC 2026 % 0.06/0.33 % CPUTime : % 0.21/0.49 Zenon error: exhausted search space without finding a proof % 0.21/0.49 (* Current branch: % 0.21/0.49 (zenon_Vke != zenon_Vpi) % 0.21/0.49 (zenon_Vpf != zenon_Vdh) % 0.21/0.49 (p1 zenon_Vrf) % 0.21/0.49 (zenon_Vme != zenon_Vbd) % 0.21/0.49 (zenon_Vme != zenon_Vpi) % 0.21/0.49 (zenon_Vke != zenon_Vjc) % 0.21/0.49 (r1 zenon_Vfe zenon_Vse) % 0.21/0.49 (zenon_Vpf != zenon_Vpe) % 0.21/0.49 (r1 zenon_Vrf zenon_Vsf) % 0.21/0.49 (zenon_Vpf != zenon_Vsi) % 0.21/0.49 (zenon_Vrf != zenon_Vhg) % 0.21/0.49 (r1 zenon_Vza zenon_Vcb) % 0.21/0.49 (r1 zenon_Veg zenon_Vhg) % 0.21/0.49 (zenon_Vrf != zenon_Vpc) % 0.21/0.49 (zenon_Vpf != zenon_Vxa) % 0.21/0.49 (-. (p1 zenon_Vkc)) % 0.21/0.49 (r1 zenon_Vjf zenon_Vkf) % 0.21/0.49 (-. (p1 zenon_Vji)) % 0.21/0.49 (zenon_Vpf != zenon_Vdf) % 0.21/0.49 (zenon_Vpf != zenon_Vhd) % 0.21/0.49 (zenon_Vrf != zenon_Vki) % 0.21/0.49 (zenon_Vme != zenon_Vih) % 0.21/0.49 (zenon_Vke != zenon_Vha) % 0.21/0.49 (zenon_Vrf != zenon_Vsd) % 0.21/0.49 (zenon_Vme != zenon_Vhg) % 0.21/0.49 (-. (p1 zenon_Vte)) % 0.21/0.49 (zenon_Vme != zenon_Vdh) % 0.21/0.49 (r1 zenon_Vlh zenon_Voh) % 0.21/0.49 (zenon_Vke != zenon_Vsd) % 0.21/0.49 (zenon_Vpf != zenon_Vcd) % 0.21/0.49 (-. (p1 zenon_Vpe)) % 0.21/0.49 (zenon_Vrf != zenon_Vuh) % 0.21/0.49 (zenon_Vme != zenon_Vyd) % 0.21/0.49 (-. (p1 zenon_Vzh)) % 0.21/0.49 (-. (p1 zenon_Vyi)) % 0.21/0.49 (zenon_Vrf != zenon_Vdh) % 0.21/0.49 (zenon_Vpf != zenon_Vye) % 0.21/0.49 (zenon_Vke != zenon_Vch) % 0.21/0.49 (r1 zenon_Vci zenon_Vfi) % 0.21/0.49 (r1 zenon_Vlf zenon_Vmf) % 0.21/0.49 (zenon_Vke != zenon_Vih) % 0.21/0.49 (p1 zenon_Vke) % 0.21/0.49 (-. (p1 zenon_Vdh)) % 0.21/0.49 (zenon_Vke != zenon_Vfi) % 0.21/0.49 (zenon_Vme != zenon_Vle) % 0.21/0.49 (zenon_Vpf != zenon_Vqg) % 0.21/0.49 (zenon_Vpf != zenon_Vvg) % 0.21/0.49 (zenon_Vke != zenon_Vhg) % 0.21/0.49 (zenon_Vke != zenon_Vki) % 0.21/0.49 (zenon_Vme != zenon_Vnf) % 0.21/0.49 (r1 zenon_Vfe zenon_Vdf) % 0.21/0.49 (zenon_Vpf != zenon_Vbg) % 0.21/0.49 (zenon_Vrf != zenon_Vfi) % 0.21/0.49 (zenon_Vrf != zenon_Vih) % 0.21/0.49 (zenon_Vke != zenon_Vpc) % 0.21/0.49 (-. (p1 zenon_Vai)) % 0.21/0.49 (zenon_Vme != zenon_Vph) % 0.21/0.49 (zenon_Vpf != zenon_Vpi) % 0.21/0.49 (zenon_Vpf != zenon_Vpc) % 0.21/0.49 (r1 zenon_Vgc zenon_Vjc) % 0.21/0.49 (zenon_Vme != zenon_Vsd) % 0.21/0.49 (zenon_Vme != zenon_Vse) % 0.21/0.49 (zenon_Vme != zenon_Vwb) % 0.21/0.49 (zenon_Vpf != zenon_Vfi) % 0.21/0.49 (zenon_Vpf != zenon_Vsf) % 0.21/0.49 (zenon_Vke != zenon_Vkc) % 0.21/0.49 (zenon_Vpf != zenon_Vtd) % 0.21/0.49 (zenon_Vke != zenon_Vti) % 0.21/0.49 (-. (p1 zenon_Vle)) % 0.21/0.49 (-. (p1 zenon_Vcg)) % 0.21/0.49 (zenon_Vke != zenon_Vle) % 0.21/0.49 (zenon_Vke != zenon_Vef) % 0.21/0.49 (zenon_Vpf != zenon_Vph) % 0.21/0.49 (-. (p1 zenon_Vcd)) % 0.21/0.49 (r1 zenon_Vzg zenon_Vch) % 0.21/0.49 (zenon_Vpf != zenon_Voh) % 0.21/0.49 (zenon_Vke != zenon_Vpg) % 0.21/0.49 (zenon_Vpf != zenon_Vwb) % 0.21/0.49 (zenon_Vme != zenon_Vuh) % 0.21/0.49 (zenon_Vrf != zenon_Vqb) % 0.21/0.49 (zenon_Vrf != zenon_Vti) % 0.21/0.49 (zenon_Vme != zenon_Vef) % 0.21/0.49 (zenon_Vpf != zenon_Vch) % 0.21/0.49 (zenon_Vpf != zenon_Vqb) % 0.21/0.49 (zenon_Vpf != zenon_Vzh) % 0.21/0.49 (-. (p1 zenon_Vyd)) % 0.21/0.49 (r1 zenon_Vgf zenon_Vhf) % 0.21/0.49 (zenon_Vme != zenon_Vzh) % 0.21/0.49 (zenon_Vpf != zenon_Vba) % 0.21/0.49 (zenon_Vrf != zenon_Vsf) % 0.21/0.49 (zenon_Vke != zenon_Vcd) % 0.21/0.49 (zenon_Vke != zenon_Vhd) % 0.21/0.49 (zenon_Vke != zenon_Vji) % 0.21/0.49 (zenon_Vrf != zenon_Vca) % 0.21/0.49 (zenon_Vrf != zenon_Vba) % 0.21/0.49 (zenon_Vrf != zenon_Vyi) % 0.21/0.49 (zenon_Vke != zenon_Vcg) % 0.21/0.49 (-. (p1 zenon_Vba)) % 0.21/0.49 (-. (p1 zenon_Vse)) % 0.21/0.49 (zenon_Vpf != zenon_Vyi) % 0.21/0.49 (zenon_Vrf != zenon_Vnf) % 0.21/0.49 (zenon_Vke != zenon_Vwa) % 0.21/0.49 (r1 zenon_Ved zenon_Vhd) % 0.21/0.49 (zenon_Vpf != zenon_Vuh) % 0.21/0.49 (zenon_Vpf != zenon_Vji) % 0.21/0.49 (zenon_Vke != zenon_Vdf) % 0.21/0.49 (zenon_Vrf != zenon_Vcd) % 0.21/0.49 (zenon_Vke != zenon_Vqb) % 0.21/0.49 (zenon_Vke != zenon_Vdh) % 0.21/0.49 (r1 zenon_Vy zenon_Vba) % 0.21/0.49 (zenon_Vme != zenon_Vsf) % 0.21/0.49 (zenon_Vme != zenon_Vvg) % 0.21/0.49 (zenon_Vpf != zenon_Vef) % 0.21/0.49 (zenon_Vrf != zenon_Vkc) % 0.21/0.49 (zenon_Vpf != zenon_Vki) % 0.21/0.49 (zenon_Vme != zenon_Vcg) % 0.21/0.49 (r1 zenon_Vke zenon_Vle) % 0.21/0.49 (zenon_Vpf != zenon_Vih) % 0.21/0.49 (zenon_Vrf != zenon_Vhd) % 0.21/0.49 (-. (p1 zenon_Vcb)) % 0.21/0.49 (r1 zenon_Vmf zenon_Vnf) % 0.21/0.49 (-. (p1 zenon_Vph)) % 0.21/0.49 (zenon_Vke != zenon_Vsi) % 0.21/0.49 (zenon_Vke != zenon_Vxa) % 0.21/0.49 (-. (p1 zenon_Voh)) % 0.21/0.49 (zenon_Vpf != zenon_Vsd) % 0.21/0.49 (zenon_Vme != zenon_Vki) % 0.21/0.49 (zenon_Vpf != zenon_Vcg) % 0.21/0.49 (zenon_Vpf != zenon_Vjc) % 0.21/0.49 (zenon_Vpf != zenon_Vte) % 0.21/0.49 (zenon_Vrf != zenon_Vef) % 0.21/0.49 (r1 zenon_Vkf zenon_Vlf) % 0.21/0.49 (-. (p1 zenon_Vpi)) % 0.21/0.49 (zenon_Vrf != zenon_Vxa) % 0.21/0.49 (r1 zenon_Vhf zenon_Vif) % 0.21/0.49 (zenon_Vme != zenon_Vcb) % 0.21/0.49 (-. (p1 zenon_Vfi)) % 0.21/0.49 (zenon_Vke != zenon_Vyd) % 0.21/0.49 (r1 zenon_Vmf zenon_Vof) % 0.21/0.49 (zenon_Vke != zenon_Vai) % 0.21/0.49 (-. (p1 zenon_Vtd)) % 0.21/0.49 (-. (p1 zenon_Vxa)) % 0.21/0.49 (r1 zenon_Vtb zenon_Vwb) % 0.21/0.49 (zenon_Vme != zenon_Vjc) % 0.21/0.49 (zenon_Vke != zenon_Vca) % 0.21/0.49 (zenon_Vme != zenon_Vkc) % 0.21/0.49 (zenon_Vrf != zenon_Vpg) % 0.21/0.49 (zenon_Vke != zenon_Vph) % 0.21/0.49 (zenon_Vrf != zenon_Vjc) % 0.21/0.49 (-. (p1 zenon_Vhd)) % 0.21/0.49 (zenon_Vke != zenon_Vsf) % 0.21/0.49 (r1 zenon_Vfh zenon_Vih) % 0.21/0.49 (zenon_Vke != zenon_Vpe) % 0.21/0.49 (zenon_Vrf != zenon_Vcg) % 0.21/0.49 (-. (p1 zenon_Vjc)) % 0.21/0.49 (r1 zenon_Vme zenon_Vpe) % 0.21/0.49 (zenon_Vrf != zenon_Vte) % 0.21/0.49 (zenon_Vme != zenon_Vcd) % 0.21/0.49 (zenon_Vme != zenon_Vpg) % 0.21/0.49 (zenon_Vme != zenon_Vqg) % 0.21/0.49 (zenon_Vme != zenon_Vbg) % 0.21/0.49 (zenon_Vpf != zenon_Vca) % 0.21/0.49 (-. (p1 zenon_Vye)) % 0.21/0.49 (zenon_Vke != zenon_Vte) % 0.21/0.49 (zenon_Vke != zenon_Vyi) % 0.21/0.49 (-. (p1 zenon_Vpc)) % 0.21/0.49 (zenon_Vrf != zenon_Voh) % 0.21/0.49 (r1 zenon_Vea zenon_Vha) % 0.21/0.49 (zenon_Vke != zenon_Vbg) % 0.21/0.49 (zenon_Vme != zenon_Vsi) % 0.21/0.49 (zenon_Vrf != zenon_Vph) % 0.21/0.49 (zenon_Vpf != zenon_Vyd) % 0.21/0.49 (zenon_Vke != zenon_Vvg) % 0.21/0.49 (r1 zenon_Vvd zenon_Vyd) % 0.21/0.49 (zenon_Vme != zenon_Vqb) % 0.21/0.49 (r1 zenon_Vyf zenon_Vbg) % 0.21/0.49 (-. (p1 zenon_Vdf)) % 0.21/0.49 (zenon_Vrf != zenon_Vdf) % 0.21/0.49 (zenon_Vme != zenon_Vwa) % 0.21/0.49 (-. (p1 zenon_Vki)) % 0.21/0.49 (-. (p1 zenon_Vih)) % 0.21/0.49 (zenon_Vme != zenon_Vch) % 0.21/0.49 (r1 zenon_Vve zenon_Vye) % 0.21/0.49 (-. (p1 zenon_Vhg)) % 0.21/0.49 (-. (p1 zenon_Vsd)) % 0.21/0.49 (r1 zenon_Vmi zenon_Vpi) % 0.21/0.49 (zenon_Vke != zenon_Vzh) % 0.21/0.49 (zenon_Vpf != zenon_Vha) % 0.21/0.49 (zenon_Vme != zenon_Vha) % 0.21/0.49 (zenon_Vpf != zenon_Vti) % 0.21/0.49 (zenon_Vrf != zenon_Vai) % 0.21/0.49 (zenon_Vme != zenon_Vca) % 0.21/0.49 (zenon_Vpf != zenon_Vrb) % 0.21/0.49 (-. (p1 zenon_Vha)) % 0.21/0.49 (zenon_Vrf != zenon_Vwa) % 0.21/0.49 (p1 zenon_Vme) % 0.21/0.49 (r1 zenon_Vsg zenon_Vvg) % 0.21/0.49 (r1 zenon_Vif zenon_Vjf) % 0.21/0.49 (zenon_Vke != zenon_Vba) % 0.21/0.49 (r1 zenon_Vmc zenon_Vpc) % 0.21/0.49 (zenon_Vme != zenon_Vfi) % 0.21/0.49 (zenon_Vme != zenon_Vba) % 0.21/0.49 (zenon_Vpf != zenon_Vcb) % 0.21/0.49 (-. (p1 zenon_Vvg)) % 0.21/0.49 (zenon_Vrf != zenon_Vsi) % 0.21/0.49 (r1 Tau_1 zenon_Vgf) % 0.21/0.49 (zenon_Vpf != zenon_Vbd) % 0.21/0.49 (zenon_Vrf != zenon_Vqg) % 0.21/0.49 (-. (p1 zenon_Vqg)) % 0.21/0.49 (zenon_Vrf != zenon_Vle) % 0.21/0.49 (zenon_Vme != zenon_Vdf) % 0.21/0.49 (r1 zenon_Vnb zenon_Vqb) % 0.21/0.49 (zenon_Vme != zenon_Vye) % 0.21/0.49 (r1 zenon_Vta zenon_Vwa) % 0.21/0.49 (zenon_Vke != zenon_Voh) % 0.21/0.49 (r1 zenon_Vpd zenon_Vsd) % 0.21/0.49 (zenon_Vpf != zenon_Vhg) % 0.21/0.49 (-. (p1 zenon_Vsi)) % 0.21/0.49 (zenon_Vrf != zenon_Vzh) % 0.21/0.49 (zenon_Vme != zenon_Vrb) % 0.21/0.49 (-. (p1 zenon_Vti)) % 0.21/0.49 (zenon_Vrf != zenon_Vrb) % 0.21/0.49 (zenon_Vme != zenon_Vhd) % 0.21/0.49 (zenon_Vme != zenon_Vji) % 0.21/0.49 (r1 zenon_Vrh zenon_Vuh) % 0.21/0.49 (zenon_Vke != zenon_Vnf) % 0.21/0.49 (r1 zenon_Vgi zenon_Vji) % 0.21/0.49 (zenon_Vpf != zenon_Vnf) % 0.21/0.49 (-. (p1 zenon_Vrb)) % 0.21/0.49 (zenon_Vme != zenon_Vti) % 0.21/0.49 (zenon_Vrf != zenon_Vji) % 0.21/0.49 (zenon_Vme != zenon_Vtd) % 0.21/0.49 (zenon_Vme != zenon_Vxa) % 0.21/0.49 (zenon_Vrf != zenon_Vha) % 0.21/0.49 (zenon_Vpf != zenon_Vkc) % 0.21/0.49 (zenon_Vrf != zenon_Vyd) % 0.21/0.49 (zenon_Vrf != zenon_Vtd) % 0.21/0.49 (zenon_Vpf != zenon_Vai) % 0.21/0.49 (zenon_Vrf != zenon_Vse) % 0.21/0.49 (zenon_Vke != zenon_Vcb) % 0.21/0.49 (-. (p1 zenon_Vch)) % 0.21/0.49 (zenon_Vke != zenon_Vtd) % 0.21/0.49 (zenon_Vrf != zenon_Vbg) % 0.21/0.49 (zenon_Vme != zenon_Vyi) % 0.21/0.49 (zenon_Vrf != zenon_Vbd) % 0.21/0.49 (-. (p1 zenon_Vsf)) % 0.21/0.49 (zenon_Vke != zenon_Vwb) % 0.21/0.49 (zenon_Vme != zenon_Vpe) % 0.21/0.49 (zenon_Vke != zenon_Vqg) % 0.21/0.49 (zenon_Vme != zenon_Vai) % 0.21/0.49 (-. (p1 zenon_Vqb)) % 0.21/0.49 (-. (p1 zenon_Vwb)) % 0.21/0.49 (zenon_Vke != zenon_Vye) % 0.21/0.49 (r1 zenon_Vqf zenon_Vrf) % 0.21/0.49 (zenon_Vrf != zenon_Vch) % 0.21/0.49 (r1 zenon_Vmg zenon_Vpg) % 0.21/0.49 (zenon_Vrf != zenon_Vpi) % 0.21/0.49 (r1 zenon_Vyc zenon_Vbd) % 0.21/0.49 (zenon_Vrf != zenon_Vcb) % 0.21/0.49 (zenon_Vrf != zenon_Vpe) % 0.21/0.49 (zenon_Vke != zenon_Vrb) % 0.21/0.49 (zenon_Vpf != zenon_Vwa) % 0.21/0.49 (zenon_Vrf != zenon_Vye) % 0.21/0.49 (zenon_Vpf != zenon_Vpg) % 0.21/0.49 (zenon_Vme != zenon_Vte) % 0.21/0.49 (zenon_Vke != zenon_Vse) % 0.21/0.49 (-. (p1 zenon_Vbg)) % 0.21/0.49 (r1 zenon_Vvi zenon_Vyi) % 0.21/0.49 (zenon_Vke != zenon_Vbd) % 0.21/0.49 (p1 zenon_Vpf) % 0.21/0.49 (r1 zenon_Vwh zenon_Vzh) % 0.21/0.49 (-. (p1 zenon_Vuh)) % 0.21/0.49 (zenon_Vme != zenon_Vpc) % 0.21/0.49 (zenon_Vme != zenon_Voh) % 0.21/0.49 (-. (p1 zenon_Vef)) % 0.21/0.49 (-. (p1 zenon_Vca)) % 0.21/0.49 (zenon_Vrf != zenon_Vwb) % 0.21/0.49 (zenon_Vpf != zenon_Vle) % 0.21/0.49 (r1 Tau_0 Tau_1) % 0.21/0.49 (zenon_Vrf != zenon_Vvg) % 0.21/0.49 (-. (p1 zenon_Vnf)) % 0.21/0.49 (-. (p1 zenon_Vpg)) % 0.21/0.49 (-. (p1 zenon_Vwa)) % 0.21/0.49 (r1 zenon_X15 zenon_Vsi) % 0.21/0.49 (zenon_Vke != zenon_Vuh) % 0.21/0.49 (zenon_Vpf != zenon_Vse) % 0.21/0.49 (-. (p1 zenon_Vbd)) % 0.21/0.49 (r1 zenon_Vfe zenon_Vke) % 0.21/0.49 *) % 0.21/0.49 (* NO-PROOF *) % 0.21/0.49 % SZS status GaveUp % 0.21/0.49 Number of rewrites on terms: 0 % 0.21/0.49 Number of rewrites on props: 0 % 0.21/0.49 nodes searched: 617 % 0.21/0.49 max branch formulas: 712 % 0.21/0.49 proof nodes created: 0 % 0.21/0.49 formulas created: 3792 % 0.21/0.49 %------------------------------------------------------------------------------