%------------------------------------------------------------------------------ % File : ZenonModulo---0.5.0 % Problem : SWV557-1.004 : TPTP v8.2.0. Released v4.0.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 : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Jun 25 02:16:01 EDT 2024 % Result : Unknown 0.20s 0.49s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SWV557-1.004 : TPTP v8.2.0. Released v4.0.0. % 0.03/0.12 % Command : run_zenon_modulo %d %s % 0.11/0.32 % Computer : n008.cluster.edu % 0.11/0.32 % Model : x86_64 x86_64 % 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.32 % Memory : 8042.1875MB % 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.32 % CPULimit : 300 % 0.11/0.32 % WCLimit : 300 % 0.11/0.32 % DateTime : Sat Jun 22 00:02:08 EDT 2024 % 0.11/0.33 % CPUTime : % 0.20/0.49 Zenon error: exhausted search space without finding a proof % 0.20/0.49 (* Current branch: % 0.20/0.49 ((a1) != (a2)) % 0.20/0.49 ((store (store (store (store (a1) (i1) (select (a2) (i1))) (i2) (select (store (a2) (i1) (select (a1) (i1))) (i2))) (i3) (select (store (store (a2) (i1) (select (a1) (i1))) (i2) (select (store (a1) (i1) (select (a2) (i1))) (i2))) (i3))) (i4) (select (store (store (store (a2) (i1) (select (a1) (i1))) (i2) (select (store (a1) (i1) (select (a2) (i1))) (i2))) (i3) (select (store (store (a1) (i1) (select (a2) (i1))) (i2) (select (store (a2) (i1) (select (a1) (i1))) (i2))) (i3))) (i4))) = (store (store (store (store (a2) (i1) (select (a1) (i1))) (i2) (select (store (a1) (i1) (select (a2) (i1))) (i2))) (i3) (select (store (store (a1) (i1) (select (a2) (i1))) (i2) (select (store (a2) (i1) (select (a1) (i1))) (i2))) (i3))) (i4) (select (store (store (store (a1) (i1) (select (a2) (i1))) (i2) (select (store (a2) (i1) (select (a1) (i1))) (i2))) (i3) (select (store (store (a2) (i1) (select (a1) (i1))) (i2) (select (store (a1) (i1) (select (a2) (i1))) (i2))) (i3))) (i4)))) % 0.20/0.49 ((select (store zenon_X0 zenon_X2 zenon_X1) zenon_X3) = (select zenon_X0 zenon_X3)) % 0.20/0.49 ((store (store zenon_X4 zenon_X7 zenon_X5) zenon_X8 zenon_X6) = (store (store zenon_X4 zenon_X8 zenon_X6) zenon_X7 zenon_X5)) % 0.20/0.49 *) % 0.20/0.49 (* NO-PROOF *) % 0.20/0.49 % SZS status GaveUp % 0.20/0.49 Number of rewrites on terms: 0 % 0.20/0.49 Number of rewrites on props: 0 % 0.20/0.49 nodes searched: 12 % 0.20/0.49 max branch formulas: 15 % 0.20/0.49 proof nodes created: 0 % 0.20/0.49 formulas created: 360 % 0.20/0.49 %------------------------------------------------------------------------------