%------------------------------------------------------------------------------ % File : ZenonModulo---0.5.0 % Problem : SWV996_1 : TPTP v8.2.0. Released v5.0.0. % Transfm : none % Format : tptp:raw % Command : run_zenon_modulo %d %s % Computer : n016.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 Jun 25 02:16:46 EDT 2024 % Result : Unknown 0.21s 0.52s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.13 % Problem : SWV996_1 : TPTP v8.2.0. Released v5.0.0. % 0.11/0.13 % Command : run_zenon_modulo %d %s % 0.12/0.34 % Computer : n016.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Sat Jun 22 01:49:24 EDT 2024 % 0.12/0.34 % CPUTime : % 0.21/0.52 Zenon error: exhausted search space without finding a proof % 0.21/0.52 (* Current branch: % 0.21/0.52 ((z2) != (z3)) % 0.21/0.52 (zenon_Vv >= (1)) % 0.21/0.52 ((a zenon_X4) != (10)) % 0.21/0.52 ((9) != (a zenon_X3)) % 0.21/0.52 ((a zenon_X3) != (a (z2))) % 0.21/0.52 ((a zenon_X2) >= (11)) % 0.21/0.52 ((z1) > (z2)) % 0.21/0.52 ((9) != (10)) % 0.21/0.52 ((a zenon_X2) != (a (z2))) % 0.21/0.52 (zenon_X3 != (z2)) % 0.21/0.52 (zenon_Vn = ((z1) - (z2))) % 0.21/0.52 ((zenon_X3 - (z1)) >= (1)) % 0.21/0.52 (zenon_X3 > (z1)) % 0.21/0.52 ((a (z1)) < (a (z2))) % 0.21/0.52 ((a (z1)) = (9)) % 0.21/0.52 (((a (z1)) - (a (z2))) <= (-1)) % 0.21/0.52 (zenon_Vt <= (-1)) % 0.21/0.52 (((z1) - (z2)) >= (1)) % 0.21/0.52 (((a zenon_X4) - (a (z2))) >= (1)) % 0.21/0.52 (((a zenon_X3) - (a (z2))) >= (1)) % 0.21/0.52 ((a (z2)) <= (10)) % 0.21/0.52 ((- (a zenon_X3)) <= (-10)) % 0.21/0.52 ((z1) > (z3)) % 0.21/0.52 ((9) != (a (z2))) % 0.21/0.52 ((a zenon_X4) > (a (z2))) % 0.21/0.52 ((9) < (a (z2))) % 0.21/0.52 (zenon_Vw >= (1)) % 0.21/0.52 ((- (a (z1))) >= (-9)) % 0.21/0.52 (zenon_Vr = (zenon_X3 - (z2))) % 0.21/0.52 (zenon_Vo >= (1)) % 0.21/0.52 (zenon_Vu >= (1)) % 0.21/0.52 (zenon_Vp >= (1)) % 0.21/0.52 (zenon_Vx >= (1)) % 0.21/0.52 ((a zenon_X3) != (10)) % 0.21/0.52 (zenon_Vn >= (1)) % 0.21/0.52 ((zenon_X2 - (z2)) >= (1)) % 0.21/0.52 (zenon_Vy >= (1)) % 0.21/0.52 (zenon_Vz >= (1)) % 0.21/0.52 ((a zenon_X4) > (10)) % 0.21/0.52 (zenon_Vo = ((z1) - (z3))) % 0.21/0.52 (((z2) - (z3)) >= (1)) % 0.21/0.52 (zenon_Vq = ((a zenon_X3) - (a (z2)))) % 0.21/0.52 ((a zenon_X3) > (10)) % 0.21/0.52 ((z1) != (z3)) % 0.21/0.52 (zenon_Vq >= (1)) % 0.21/0.52 (zenon_Vp = ((z2) - (z3))) % 0.21/0.52 ((a (z2)) = (10)) % 0.21/0.52 ((- (a (z2))) <= (-10)) % 0.21/0.52 ((z1) != (z2)) % 0.21/0.52 ((a (z1)) >= (9)) % 0.21/0.52 ((a zenon_X3) != (a (z1))) % 0.21/0.52 (zenon_Vm <= (-1)) % 0.21/0.52 (zenon_Vz = (zenon_X4 - (z2))) % 0.21/0.52 (zenon_X4 != (z2)) % 0.21/0.52 ((a (z1)) != (a (z2))) % 0.21/0.52 ((a (z2)) >= (10)) % 0.21/0.52 (zenon_Vy = ((a zenon_X4) - (a (z2)))) % 0.21/0.52 (zenon_Vw = ((a zenon_X2) - (a (z2)))) % 0.21/0.52 ((b (z2)) <= (2)) % 0.21/0.52 ((9) < (a zenon_X3)) % 0.21/0.52 ((a zenon_X2) != (10)) % 0.21/0.52 (((a zenon_X3) - (a (z1))) >= (1)) % 0.21/0.52 ((a zenon_X0) <= (12)) % 0.21/0.52 ((1) <= (a zenon_X0)) % 0.21/0.52 (zenon_X2 > (z2)) % 0.21/0.52 (zenon_X4 > (z2)) % 0.21/0.52 ((a zenon_X4) != (a (z2))) % 0.21/0.52 (zenon_Vr >= (1)) % 0.21/0.52 ((a zenon_X3) > (a (z2))) % 0.21/0.52 (zenon_X2 != (z2)) % 0.21/0.52 (((a zenon_X2) - (a (z2))) >= (1)) % 0.21/0.52 ((z2) < (z1)) % 0.21/0.52 (zenon_Vu = ((a zenon_X3) - (a (z1)))) % 0.21/0.52 ((b (z2)) < (3)) % 0.21/0.52 (zenon_Vx = (zenon_X2 - (z2))) % 0.21/0.52 (((z2) - (z1)) <= (-1)) % 0.21/0.52 ((z2) > (z3)) % 0.21/0.52 (zenon_X3 > (z2)) % 0.21/0.52 ((a zenon_X2) > (10)) % 0.21/0.52 ((a zenon_X3) >= (11)) % 0.21/0.52 ((9) < (10)) % 0.21/0.52 ((b zenon_X1) <= (5)) % 0.21/0.52 (zenon_Vt = ((a (z1)) - (a (z2)))) % 0.21/0.52 (((z1) - (z3)) >= (1)) % 0.21/0.52 (zenon_Vm = ((z2) - (z1))) % 0.21/0.52 ((1) <= (b zenon_X1)) % 0.21/0.52 (zenon_Vv = (zenon_X3 - (z1))) % 0.21/0.52 ((zenon_X3 - (z2)) >= (1)) % 0.21/0.52 (zenon_X3 != (z1)) % 0.21/0.52 ((zenon_X4 - (z2)) >= (1)) % 0.21/0.52 ((a zenon_X4) >= (11)) % 0.21/0.52 ((a zenon_X2) > (a (z2))) % 0.21/0.52 ((a (z1)) <= (9)) % 0.21/0.52 ((10) > (a (z1))) % 0.21/0.52 ((a zenon_X3) > (a (z1))) % 0.21/0.52 ((10) != (a (z1))) % 0.21/0.52 *) % 0.21/0.52 (* NO-PROOF *) % 0.21/0.52 % SZS status GaveUp % 0.21/0.52 Number of rewrites on terms: 0 % 0.21/0.52 Number of rewrites on props: 0 % 0.21/0.52 nodes searched: 139 % 0.21/0.52 max branch formulas: 109 % 0.21/0.52 proof nodes created: 18 % 0.21/0.52 formulas created: 737 % 0.21/0.52 %------------------------------------------------------------------------------