%------------------------------------------------------------------------------ % File : ZenonModulo---0.5.0 % Problem : SWV496-1.050 : TPTP v8.2.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : run_zenon_modulo %d %s % Computer : n011.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:15:46 EDT 2024 % Result : Unknown 0.21s 0.53s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.13 % Problem : SWV496-1.050 : TPTP v8.2.0. Released v4.0.0. % 0.12/0.13 % Command : run_zenon_modulo %d %s % 0.13/0.34 % Computer : n011.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Sat Jun 22 00:15:24 EDT 2024 % 0.13/0.34 % CPUTime : % 0.21/0.53 Zenon error: exhausted search space without finding a proof % 0.21/0.53 (* Current branch: % 0.21/0.53 ((select (store zenon_X0 zenon_X2 zenon_X1) zenon_X3) = (select zenon_X0 zenon_X3)) % 0.21/0.53 ((store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (a1) (n1) (e1)) (n2) (e2)) (n3) (e3)) (n4) (e4)) (n5) (e5)) (n6) (e6)) (n7) (e7)) (n8) (e8)) (n9) (e9)) (n10) (e10)) (n11) (e11)) (n12) (e12)) (n13) (e13)) (n14) (e14)) (n15) (e15)) (n16) (e16)) (n17) (e17)) (n18) (e18)) (n19) (e19)) (n20) (e20)) (n21) (e21)) (n22) (e22)) (n23) (e23)) (n24) (e24)) (n25) (e25)) (n26) (e26)) (n27) (e27)) (n28) (e28)) (n29) (e29)) (n30) (e30)) (n31) (e31)) (n32) (e32)) (n33) (e33)) (n34) (e34)) (n35) (e35)) (n36) (e36)) (n37) (e37)) (n38) (e38)) (n39) (e39)) (n40) (e40)) (n41) (e41)) (n42) (e42)) (n43) (e43)) (n44) (e44)) (n45) (e45)) (n46) (e46)) (n47) (e47)) (n48) (e48)) (n49) (e49)) != (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (a1) (n41) (e41)) (n30) (e30)) (n45) (e45)) (n43) (e43)) (n28) (e28)) (n19) (e19)) (n22) (e22)) (n39) (e39)) (n20) (e20)) (n40) (e40)) (n16) (e16)) (n8) (e8)) (n49) (e49)) (n14) (e14)) (n13) (e13)) (n6) (e6)) (n27) (e27)) (n15) (e15)) (n7) (e7)) (n33) (e33)) (n9) (e9)) (n17) (e17)) (n42) (e42)) (n47) (e47)) (n18) (e18)) (n26) (e26)) (n34) (e34)) (n11) (e11)) (n36) (e36)) (n44) (e44)) (n38) (e38)) (n23) (e23)) (n25) (e25)) (n46) (e46)) (n35) (e35)) (n50) (e50)) (n2) (e2)) (n10) (e10)) (n48) (e48)) (n29) (e29)) (n3) (e3)) (n37) (e37)) (n12) (e12)) (n5) (e5)) (n32) (e32)) (n4) (e4)) (n24) (e24)) (n21) (e21)) (n31) (e31))) % 0.21/0.53 ((store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (a1) (n1) (e1)) (n2) (e2)) (n3) (e3)) (n4) (e4)) (n5) (e5)) (n6) (e6)) (n7) (e7)) (n8) (e8)) (n9) (e9)) (n10) (e10)) (n11) (e11)) (n12) (e12)) (n13) (e13)) (n14) (e14)) (n15) (e15)) (n16) (e16)) (n17) (e17)) (n18) (e18)) (n19) (e19)) (n20) (e20)) (n21) (e21)) (n22) (e22)) (n23) (e23)) (n24) (e24)) (n25) (e25)) (n26) (e26)) (n27) (e27)) (n28) (e28)) (n29) (e29)) (n30) (e30)) (n31) (e31)) (n32) (e32)) (n33) (e33)) (n34) (e34)) (n35) (e35)) (n36) (e36)) (n37) (e37)) (n38) (e38)) (n39) (e39)) (n40) (e40)) (n41) (e41)) (n42) (e42)) (n43) (e43)) (n44) (e44)) (n45) (e45)) (n46) (e46)) (n47) (e47)) (n48) (e48)) (n49) (e49)) (n1) (e1)) != (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (a1) (n41) (e41)) (n30) (e30)) (n45) (e45)) (n43) (e43)) (n28) (e28)) (n19) (e19)) (n22) (e22)) (n39) (e39)) (n20) (e20)) (n40) (e40)) (n16) (e16)) (n8) (e8)) (n49) (e49)) (n14) (e14)) (n13) (e13)) (n6) (e6)) (n27) (e27)) (n15) (e15)) (n7) (e7)) (n33) (e33)) (n9) (e9)) (n17) (e17)) (n42) (e42)) (n47) (e47)) (n18) (e18)) (n26) (e26)) (n34) (e34)) (n11) (e11)) (n36) (e36)) (n44) (e44)) (n38) (e38)) (n23) (e23)) (n25) (e25)) (n46) (e46)) (n35) (e35)) (n50) (e50)) (n2) (e2)) (n10) (e10)) (n48) (e48)) (n29) (e29)) (n3) (e3)) (n37) (e37)) (n12) (e12)) (n5) (e5)) (n32) (e32)) (n4) (e4)) (n24) (e24)) (n21) (e21)) (n31) (e31)) (n1) (e1))) % 0.21/0.53 ((e49) != (e31)) % 0.21/0.53 *) % 0.21/0.53 (* NO-PROOF *) % 0.21/0.53 % SZS status GaveUp % 0.21/0.53 Number of rewrites on terms: 0 % 0.21/0.53 Number of rewrites on props: 0 % 0.21/0.53 nodes searched: 10 % 0.21/0.53 max branch formulas: 9 % 0.21/0.53 proof nodes created: 2 % 0.21/0.53 formulas created: 828 % 0.21/0.53 %------------------------------------------------------------------------------