%------------------------------------------------------------------------------ % File : ZenonModulo---0.5.0 % Problem : SWX238-1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : run_zenon_modulo %d %s % Computer : n024.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Tue May 5 07:08:40 PM UTC 2026 % Result : Unknown 0.29s 0.46s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.06 % Problem : SWX238-1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.06 % Command : run_zenon_modulo %d %s % 0.06/0.24 % Computer : n024.cluster.edu % 0.06/0.24 % Model : x86_64 x86_64 % 0.06/0.24 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.06/0.24 % Memory : 8042.1875MB % 0.06/0.24 % OS : Linux 3.10.0-693.el7.x86_64 % 0.06/0.24 % CPULimit : 300 % 0.06/0.24 % WCLimit : 300 % 0.06/0.24 % DateTime : Tue May 5 08:17:26 EDT 2026 % 0.06/0.25 % CPUTime : % 0.29/0.46 Zenon error: exhausted search space without finding a proof % 0.29/0.46 (* Current branch: % 0.29/0.46 ((eq (a) (c)) = (bfalse)) % 0.29/0.46 ((notb (btrue)) != (notb (bfalse))) % 0.29/0.46 ((eq2 (notb (reck2 zenon_X0 (cons2 (a) (cons2 (b) (cons2 (a) (cons2 (b) (cons2 (b) (nil2)))))))) (bfalse)) != (eq2 (bfalse) (btrue))) % 0.29/0.46 ((eq2 (notb (reck2 zenon_X0 (cons2 (a) (cons2 (b) (cons2 (a) (cons2 (b) (cons2 (b) (nil2)))))))) (bfalse)) != (eps2 (eps))) % 0.29/0.46 ((bfalse) != (btrue)) % 0.29/0.46 ((reck2 zenon_X0 (cons2 (a) (cons2 (b) (cons2 (a) (cons2 (b) (cons2 (b) (nil2))))))) != (eq (c) (a))) % 0.29/0.46 ((eq (a) (c)) != (reck2 (eps) (nil2))) % 0.29/0.46 ((eq2 (notb (reck2 zenon_X0 (cons2 (a) (cons2 (b) (cons2 (a) (cons2 (b) (cons2 (b) (nil2)))))))) (bfalse)) != (notb (bfalse))) % 0.29/0.46 ((notb (reck2 zenon_X0 (cons2 (a) (cons2 (b) (cons2 (a) (cons2 (b) (cons2 (b) (nil2)))))))) != (btrue)) % 0.29/0.46 ((eq (b) (a)) != (notb (bfalse))) % 0.29/0.46 ((eq (a) (c)) != (notb (bfalse))) % 0.29/0.46 ((eq (c) (b)) = (bfalse)) % 0.29/0.46 ((eq2 (notb (reck2 zenon_X0 (cons2 (a) (cons2 (b) (cons2 (a) (cons2 (b) (cons2 (b) (nil2)))))))) (bfalse)) != (eq2 (btrue) (bfalse))) % 0.29/0.46 ((reck2 zenon_X0 (cons2 (a) (cons2 (b) (cons2 (a) (cons2 (b) (cons2 (b) (nil2))))))) != (eq (b) (c))) % 0.29/0.46 ((notb (btrue)) != (eps2 (eps))) % 0.29/0.46 ((eq2 (notb (reck2 zenon_X0 (cons2 (a) (cons2 (b) (cons2 (a) (cons2 (b) (cons2 (b) (nil2)))))))) (bfalse)) != (eq (c) (b))) % 0.29/0.46 ((eq (b) (c)) != (eps2 (eps))) % 0.29/0.46 ((bfalse) != (reck2 (eps) (nil2))) % 0.29/0.46 ((eq (a) (b)) != (eps2 (eps))) % 0.29/0.46 ((eps2 (eps)) = (btrue)) % 0.29/0.46 ((btrue) != (eq (c) (a))) % 0.29/0.46 ((eq (b) (a)) = (bfalse)) % 0.29/0.46 ((eq (c) (b)) != (reck2 (eps) (nil2))) % 0.29/0.46 ((x2 (eps) (eps)) = (x (eps) (eps))) % 0.29/0.46 ((eq2 (btrue) (bfalse)) != (eps2 (eps))) % 0.29/0.46 ((or2 (nil3)) != (reck2 (eps) (nil2))) % 0.29/0.46 ((x (eps) (eps)) != (nil4)) % 0.29/0.46 ((btrue) != (or2 (nil3))) % 0.29/0.46 ((reck2 zenon_X0 (cons2 (a) (cons2 (b) (cons2 (a) (cons2 (b) (cons2 (b) (nil2))))))) != (eq (b) (a))) % 0.29/0.46 ((btrue) != (eq (a) (b))) % 0.29/0.46 ((eq2 (notb (reck2 zenon_X0 (cons2 (a) (cons2 (b) (cons2 (a) (cons2 (b) (cons2 (b) (nil2)))))))) (bfalse)) != (eq (b) (a))) % 0.29/0.46 ((eq (a) (b)) = (bfalse)) % 0.29/0.46 ((x2 (eps) (nil4)) = (eps)) % 0.29/0.46 ((eq (a) (b)) != (reck2 (eps) (nil2))) % 0.29/0.46 ((eq2 (notb (reck2 zenon_X0 (cons2 (a) (cons2 (b) (cons2 (a) (cons2 (b) (cons2 (b) (nil2)))))))) (bfalse)) != (eps2 (nil4))) % 0.29/0.46 ((notb (btrue)) = (bfalse)) % 0.29/0.46 ((reck2 (eps) (nil2)) = (btrue)) % 0.29/0.46 ((eq2 (notb (reck2 zenon_X0 (cons2 (a) (cons2 (b) (cons2 (a) (cons2 (b) (cons2 (b) (nil2)))))))) (bfalse)) != (or2 (nil3))) % 0.29/0.46 ((reck2 zenon_X0 (cons2 (a) (cons2 (b) (cons2 (a) (cons2 (b) (cons2 (b) (nil2))))))) != (eq (c) (b))) % 0.29/0.46 ((eps2 (nil4)) != (reck2 (eps) (nil2))) % 0.29/0.46 ((btrue) != (notb (btrue))) % 0.29/0.46 ((reck2 zenon_X0 (cons2 (a) (cons2 (b) (cons2 (a) (cons2 (b) (cons2 (b) (nil2))))))) != (notb (btrue))) % 0.29/0.46 ((btrue) != (eq (b) (c))) % 0.29/0.46 ((eq2 (notb (reck2 zenon_X0 (cons2 (a) (cons2 (b) (cons2 (a) (cons2 (b) (cons2 (b) (nil2)))))))) (bfalse)) != (eq (a) (b))) % 0.29/0.46 ((or2 (nil3)) != (notb (bfalse))) % 0.29/0.46 ((eq2 (btrue) (bfalse)) = (bfalse)) % 0.29/0.46 ((nil4) != (x2 (eps) (eps))) % 0.29/0.46 ((btrue) != (eq (c) (b))) % 0.29/0.46 ((eq (c) (a)) != (eps2 (eps))) % 0.29/0.46 ((btrue) != (eq (a) (c))) % 0.29/0.46 ((splits2 (nil2)) = (cons (pair2 (nil2) (nil2)) (nil))) % 0.29/0.46 ((bfalse) != (eps2 (eps))) % 0.29/0.46 ((bfalse) != (notb (bfalse))) % 0.29/0.46 ((eq (a) (b)) != (notb (bfalse))) % 0.29/0.46 ((btrue) != (eq2 (btrue) (bfalse))) % 0.29/0.46 ((btrue) != (eps2 (nil4))) % 0.29/0.46 ((eq (c) (b)) != (eps2 (eps))) % 0.29/0.46 ((bfalse) != (eq2 (notb (reck2 zenon_X0 (cons2 (a) (cons2 (b) (cons2 (a) (cons2 (b) (cons2 (b) (nil2)))))))) (bfalse))) % 0.29/0.46 ((notb (reck2 zenon_X0 (cons2 (a) (cons2 (b) (cons2 (a) (cons2 (b) (cons2 (b) (nil2)))))))) != (eps2 (eps))) % 0.29/0.46 ((eps2 (nil4)) != (notb (bfalse))) % 0.29/0.46 ((eq2 (bfalse) (btrue)) != (reck2 (eps) (nil2))) % 0.29/0.46 ((eq (c) (a)) != (reck2 (eps) (nil2))) % 0.29/0.46 ((eq2 (notb (reck2 zenon_X0 (cons2 (a) (cons2 (b) (cons2 (a) (cons2 (b) (cons2 (b) (nil2)))))))) (bfalse)) != (eq (a) (c))) % 0.29/0.46 ((eq2 (bfalse) (btrue)) != (eps2 (eps))) % 0.29/0.46 ((reck2 zenon_X0 (cons2 (a) (cons2 (b) (cons2 (a) (cons2 (b) (cons2 (b) (nil2))))))) != (eq (a) (b))) % 0.29/0.46 ((eq2 (notb (reck2 zenon_X0 (cons2 (a) (cons2 (b) (cons2 (a) (cons2 (b) (cons2 (b) (nil2)))))))) (bfalse)) != (btrue)) % 0.29/0.46 ((eps2 (nil4)) != (eps2 (eps))) % 0.29/0.46 ((eq2 (notb (reck2 zenon_X0 (cons2 (a) (cons2 (b) (cons2 (a) (cons2 (b) (cons2 (b) (nil2)))))))) (bfalse)) != (eq (b) (c))) % 0.29/0.46 ((notb (reck2 zenon_X0 (cons2 (a) (cons2 (b) (cons2 (a) (cons2 (b) (cons2 (b) (nil2)))))))) != (notb (bfalse))) % 0.29/0.46 ((eq (b) (c)) = (bfalse)) % 0.29/0.46 ((reck2 zenon_X0 (cons2 (a) (cons2 (b) (cons2 (a) (cons2 (b) (cons2 (b) (nil2))))))) != (eq2 (bfalse) (btrue))) % 0.29/0.46 ((eq (b) (a)) != (reck2 (eps) (nil2))) % 0.29/0.46 ((or2 (nil3)) != (eps2 (eps))) % 0.29/0.46 ((eq2 (btrue) (bfalse)) != (reck2 (eps) (nil2))) % 0.29/0.46 ((eq2 (notb (reck2 zenon_X0 (cons2 (a) (cons2 (b) (cons2 (a) (cons2 (b) (cons2 (b) (nil2)))))))) (bfalse)) != (eq (c) (a))) % 0.29/0.46 ((eq (a) (c)) != (eps2 (eps))) % 0.29/0.46 ((eq (c) (a)) = (bfalse)) % 0.29/0.46 ((reck2 zenon_X0 (cons2 (a) (cons2 (b) (cons2 (a) (cons2 (b) (cons2 (b) (nil2))))))) != (eq2 (btrue) (bfalse))) % 0.29/0.46 ((reck2 zenon_X0 (cons2 (a) (cons2 (b) (cons2 (a) (cons2 (b) (cons2 (b) (nil2))))))) != (eq (a) (c))) % 0.29/0.46 ((eq (b) (c)) != (reck2 (eps) (nil2))) % 0.29/0.46 ((eps2 (nil4)) = (bfalse)) % 0.29/0.46 ((nil4) != (x2 (eps) (nil4))) % 0.29/0.46 ((eq2 (bfalse) (btrue)) != (notb (bfalse))) % 0.29/0.46 ((eq2 (notb (reck2 zenon_X0 (cons2 (a) (cons2 (b) (cons2 (a) (cons2 (b) (cons2 (b) (nil2)))))))) (bfalse)) != (reck2 (eps) (nil2))) % 0.29/0.46 ((eq2 (bfalse) (btrue)) = (bfalse)) % 0.29/0.46 ((btrue) != (eq (b) (a))) % 0.29/0.46 ((notb (btrue)) != (reck2 (eps) (nil2))) % 0.29/0.46 ((eq (c) (b)) != (notb (bfalse))) % 0.29/0.46 ((notb (reck2 zenon_X0 (cons2 (a) (cons2 (b) (cons2 (a) (cons2 (b) (cons2 (b) (nil2)))))))) != (reck2 (eps) (nil2))) % 0.29/0.46 ((nil4) != (eps)) % 0.29/0.46 ((eq2 (notb (reck2 zenon_X0 (cons2 (a) (cons2 (b) (cons2 (a) (cons2 (b) (cons2 (b) (nil2)))))))) (bfalse)) != (notb (btrue))) % 0.29/0.46 ((eq2 (btrue) (bfalse)) != (notb (bfalse))) % 0.29/0.46 ((btrue) != (eq2 (bfalse) (btrue))) % 0.29/0.46 ((reck2 zenon_X0 (cons2 (a) (cons2 (b) (cons2 (a) (cons2 (b) (cons2 (b) (nil2))))))) != (eps2 (nil4))) % 0.29/0.46 ((notb (bfalse)) = (btrue)) % 0.29/0.46 ((eq (b) (a)) != (eps2 (eps))) % 0.29/0.46 ((eq (b) (c)) != (notb (bfalse))) % 0.29/0.46 ((reck2 zenon_X0 (cons2 (a) (cons2 (b) (cons2 (a) (cons2 (b) (cons2 (b) (nil2))))))) != (or2 (nil3))) % 0.29/0.46 ((or2 (nil3)) = (bfalse)) % 0.29/0.46 ((reck2 zenon_X0 (cons2 (a) (cons2 (b) (cons2 (a) (cons2 (b) (cons2 (b) (nil2))))))) != (bfalse)) % 0.29/0.46 ((eq (c) (a)) != (notb (bfalse))) % 0.29/0.46 *) % 0.29/0.46 (* NO-PROOF *) % 0.29/0.46 % SZS status GaveUp % 0.29/0.46 Number of rewrites on terms: 1 % 0.29/0.46 Number of rewrites on props: 0 % 0.29/0.46 nodes searched: 591 % 0.29/0.46 max branch formulas: 102 % 0.29/0.46 proof nodes created: 78 % 0.29/0.46 formulas created: 2140 % 0.29/0.46 %------------------------------------------------------------------------------