%------------------------------------------------------------------------------ % File : ZenonModulo---0.5.0 % Problem : LCL419-10 : TPTP v9.3.1. Released v7.5.0. % Transfm : none % Format : tptp:raw % Command : run_zenon_modulo %d %s % Computer : n008.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:33:54 PM UTC 2026 % Result : Unknown 0.13s 0.44s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : LCL419-10 : TPTP v9.3.1. Released v7.5.0. % 0.00/0.02 % Command : run_zenon_modulo %d %s % 0.08/0.34 % Computer : n008.cluster.edu % 0.08/0.34 % Model : x86_64 x86_64 % 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.34 % Memory : 8046.5625MB % 0.08/0.34 % OS : Linux 6.8.0-71-generic % 0.08/0.34 % CPULimit : 300 % 0.08/0.35 % WCLimit : 300 % 0.08/0.35 % DateTime : Sat Sep 5 20:35:53 UTC 2026 % 0.08/0.35 % CPUTime : % 0.13/0.44 Zenon error: exhausted search space without finding a proof % 0.13/0.44 (* Current branch: % 0.13/0.44 ((is_a_theorem (implies (implies (implies (a) (not (implies (implies (not (b)) (not (c))) (not (c))))) (not (implies (implies (not (b)) (not (c))) (not (c))))) (not (implies (implies (not (implies (implies (a) (b)) (b))) (not (implies (implies (a) (c)) (c)))) (not (implies (implies (a) (c)) (c))))))) != (true)) % 0.13/0.44 *) % 0.13/0.44 (* NO-PROOF *) % 0.13/0.44 % SZS status GaveUp % 0.13/0.44 Number of rewrites on terms: 0 % 0.13/0.44 Number of rewrites on props: 0 % 0.13/0.44 nodes searched: 1 % 0.13/0.44 max branch formulas: 1 % 0.13/0.44 proof nodes created: 0 % 0.13/0.44 formulas created: 273 % 0.13/0.44 %------------------------------------------------------------------------------