%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SWV533-1.004 : TPTP v9.0.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % Computer : n017.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 : Wed Apr 9 09:31:04 PM UTC 2025 % Result : Satisfiable 4.69s 2.16s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.05/0.11 % Problem : SWV533-1.004 : TPTP v9.0.0. Released v4.0.0. % 0.05/0.11 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % 0.11/0.32 % Computer : n017.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 : Wed Apr 9 03:53:55 EDT 2025 % 0.11/0.33 % CPUTime : % 4.69/2.16 % 4.69/2.16 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 4.69/2.16 % 4.69/2.16 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 4.90/2.17 %$ store > select > #nlpp > i3 > i2 > i1 > i0 > e_439 > e_437 > e_435 > e_433 > e_429 > e_427 > e_425 > e_423 > e_421 > e_419 > e_416 > a_440 > a_438 > a_436 > a_434 > a_432 > a_431 > a_430 > a_428 > a_426 > a_424 > a_422 > a_420 > a_418 > a_417 > a1 % 4.90/2.17 % 4.90/2.17 %Foreground sorts: % 4.90/2.17 % 4.90/2.17 % 4.90/2.17 %Background operators: % 4.90/2.17 % 4.90/2.17 % 4.90/2.17 %Foreground operators: % 4.90/2.17 tff(a1, type, a1: $i). % 4.90/2.17 tff(a_424, type, a_424: $i). % 4.90/2.17 tff(e_435, type, e_435: $i). % 4.90/2.17 tff(a_420, type, a_420: $i). % 4.90/2.17 tff(e_419, type, e_419: $i). % 4.90/2.17 tff(e_421, type, e_421: $i). % 4.90/2.17 tff(e_423, type, e_423: $i). % 4.90/2.17 tff(a_438, type, a_438: $i). % 4.90/2.17 tff(a_428, type, a_428: $i). % 4.90/2.17 tff(a_426, type, a_426: $i). % 4.90/2.17 tff(store, type, store: ($i * $i * $i) > $i). % 4.90/2.17 tff(a_430, type, a_430: $i). % 4.90/2.17 tff(a_440, type, a_440: $i). % 4.90/2.17 tff(e_416, type, e_416: $i). % 4.90/2.17 tff(a_418, type, a_418: $i). % 4.90/2.17 tff(e_439, type, e_439: $i). % 4.90/2.17 tff(e_427, type, e_427: $i). % 4.90/2.17 tff(e_433, type, e_433: $i). % 4.90/2.17 tff(a_432, type, a_432: $i). % 4.90/2.17 tff(a_431, type, a_431: $i). % 4.90/2.17 tff(a_417, type, a_417: $i). % 4.90/2.17 tff(e_429, type, e_429: $i). % 4.90/2.17 tff(a_422, type, a_422: $i). % 4.90/2.17 tff(i1, type, i1: $i). % 4.90/2.17 tff(i2, type, i2: $i). % 4.90/2.17 tff(select, type, select: ($i * $i) > $i). % 4.90/2.17 tff(a_436, type, a_436: $i). % 4.90/2.17 tff(e_437, type, e_437: $i). % 4.90/2.17 tff(a_434, type, a_434: $i). % 4.90/2.17 tff(i0, type, i0: $i). % 4.90/2.17 tff(e_425, type, e_425: $i). % 4.90/2.17 tff(i3, type, i3: $i). % 4.90/2.17 % 4.90/2.17 %Saturated clause set: % 4.90/2.17 tff(c_1106, plain, (![J_14]: (select(a_418, J_14)=select(a_417, J_14) | i0=J_14))). % 4.90/2.17 tff(c_1403, plain, (select(a1, i2)=e_423)). % 4.90/2.17 tff(c_1107, plain, (![J_14]: (select(a_417, J_14)=select(a1, J_14) | i0=J_14))). % 4.90/2.17 tff(c_1371, plain, (select(a_417, i2)=e_423)). % 4.90/2.17 tff(c_273, plain, (![J_14]: (select(a_426, J_14)=select(a_424, J_14) | i2=J_14))). % 4.90/2.17 tff(c_1130, plain, (store(a_420, i0, e_416)=a_422)). % 4.90/2.17 tff(c_1126, plain, (store(a_426, i0, e_416)=a_438)). % 4.90/2.17 tff(c_1127, plain, (store(a_428, i0, e_416)=a_430)). % 4.90/2.17 tff(c_1128, plain, (store(a_424, i2, e_416)=a_426)). % 4.90/2.17 tff(c_1140, plain, (store(a_418, i0, e_416)=a_420)). % 4.90/2.17 tff(c_1111, plain, (store(a1, i0, e_416)=a_417)). % 4.90/2.17 tff(c_1110, plain, (store(a_417, i0, e_416)=a_418)). % 4.90/2.17 tff(c_1132, plain, (select(a_430, i0)=e_416)). % 4.90/2.17 tff(c_1223, plain, (![J_14]: (select(a_422, J_14)=select(a_420, J_14) | i0=J_14))). % 4.90/2.17 tff(c_1129, plain, (select(a_438, i0)=e_416)). % 4.90/2.17 tff(c_1139, plain, (select(a_420, i0)=e_416)). % 4.90/2.17 tff(c_1131, plain, (select(a_422, i0)=e_416)). % 4.90/2.17 tff(c_1133, plain, (select(a_426, i2)=e_416)). % 4.90/2.17 tff(c_1135, plain, (e_429=e_416)). % 4.90/2.17 tff(c_1112, plain, (select(a1, i0)=e_416)). % 4.90/2.17 tff(c_1136, plain, (e_421=e_416)). % 4.90/2.17 tff(c_1137, plain, (e_437=e_416)). % 4.90/2.17 tff(c_1138, plain, (e_435=e_416)). % 4.90/2.17 tff(c_1149, plain, (![J_14]: (select(a_424, J_14)=select(a_422, J_14) | i0=J_14))). % 4.90/2.17 tff(c_1134, plain, (e_425=e_416)). % 4.90/2.17 tff(c_1121, plain, (e_419=e_416)). % 4.90/2.17 tff(c_1109, plain, (select(a_418, i0)=e_416)). % 4.90/2.17 tff(c_1108, plain, (select(a_417, i0)=e_416)). % 4.90/2.17 tff(c_1088, plain, (i1=i0)). % 4.90/2.17 tff(c_252, plain, (![J_14]: (select(a_440, J_14)=select(a_438, J_14) | i2=J_14))). % 4.90/2.17 tff(c_1070, plain, (select(a_418, i2)=e_423)). % 4.90/2.17 tff(c_243, plain, (![J_14]: (select(a_420, J_14)=select(a_418, J_14) | i0=J_14))). % 4.90/2.17 tff(c_1043, plain, (select(a_420, i2)=e_423)). % 4.90/2.17 tff(c_968, plain, (store(a_426, i2, e_423)=a_428)). % 4.90/2.17 tff(c_965, plain, (store(a_438, i2, e_423)=a_440)). % 4.90/2.17 tff(c_969, plain, (select(a_426, i0)=e_423)). % 4.90/2.17 tff(c_964, plain, (select(a_440, i2)=e_423)). % 4.90/2.17 tff(c_967, plain, (select(a_428, i2)=e_423)). % 4.90/2.17 tff(c_966, plain, (e_439=e_423)). % 4.90/2.17 tff(c_974, plain, (![J_14]: (select(a_438, J_14)=select(a_426, J_14) | i0=J_14))). % 4.90/2.17 tff(c_963, plain, (i2!=i0)). % 4.90/2.17 tff(c_962, plain, (e_427=e_423)). % 4.90/2.17 tff(c_762, plain, (a_436=a_426)). % 4.90/2.17 tff(c_721, plain, (a_434=a_424)). % 4.90/2.17 tff(c_490, plain, (store(a_422, i0, e_423)=a_424)). % 4.90/2.17 tff(c_695, plain, (e_433=e_423)). % 4.90/2.18 tff(c_687, plain, (a_432=a_422)). % 4.90/2.18 tff(c_681, plain, (a_431=a_420)). % 4.90/2.18 tff(c_484, plain, (select(a_424, i0)=e_423)). % 4.90/2.18 tff(c_234, plain, (![J_14]: (select(a_428, J_14)=select(a_426, J_14) | i2=J_14))). % 4.90/2.18 tff(c_460, plain, (i3=i0)). % 4.90/2.18 tff(c_261, plain, (![J_14]: (select(a_430, J_14)=select(a_428, J_14) | i0=J_14))). % 4.90/2.18 tff(c_4, plain, (![A_6, I_4, E_7, J_5]: (select(store(A_6, I_4, E_7), J_5)=select(A_6, J_5) | J_5=I_4))). % 4.90/2.18 tff(c_2, plain, (![A_1, I_2, E_3]: (select(store(A_1, I_2, E_3), I_2)=E_3))). % 4.90/2.18 tff(c_40, plain, (select(a_422, i2)=e_423)). % 4.90/2.18 tff(c_56, plain, (a_440!=a_430)). % 4.90/2.18 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 4.90/2.18 %------------------------------------------------------------------------------