%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SWV534-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 : n020.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.68s 2.19s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : SWV534-1.004 : TPTP v9.0.0. Released v4.0.0. % 0.06/0.13 % 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.13/0.34 % Computer : n020.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 : Wed Apr 9 03:54:49 EDT 2025 % 0.13/0.34 % CPUTime : % 4.68/2.19 % 4.68/2.19 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 4.68/2.19 % 4.68/2.19 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 4.68/2.20 %$ store > select > #nlpp > i3 > i2 > i1 > i0 > e_440 > e_438 > e_436 > e_434 > e_430 > e_428 > e_426 > e_424 > e_422 > e_420 > e_417 > a_441 > a_439 > a_437 > a_435 > a_433 > a_432 > a_431 > a_429 > a_427 > a_425 > a_423 > a_421 > a_419 > a_418 > a1 % 4.68/2.20 % 4.68/2.20 %Foreground sorts: % 4.68/2.20 % 4.68/2.20 % 4.68/2.20 %Background operators: % 4.68/2.20 % 4.68/2.20 % 4.68/2.20 %Foreground operators: % 4.68/2.20 tff(a1, type, a1: $i). % 4.68/2.20 tff(a_433, type, a_433: $i). % 4.68/2.20 tff(e_417, type, e_417: $i). % 4.68/2.20 tff(store, type, store: ($i * $i * $i) > $i). % 4.68/2.20 tff(e_428, type, e_428: $i). % 4.68/2.20 tff(a_435, type, a_435: $i). % 4.68/2.20 tff(e_440, type, e_440: $i). % 4.68/2.20 tff(a_441, type, a_441: $i). % 4.68/2.20 tff(a_427, type, a_427: $i). % 4.68/2.20 tff(a_418, type, a_418: $i). % 4.68/2.20 tff(e_426, type, e_426: $i). % 4.68/2.20 tff(a_421, type, a_421: $i). % 4.68/2.20 tff(a_419, type, a_419: $i). % 4.68/2.20 tff(a_439, type, a_439: $i). % 4.68/2.20 tff(e_434, type, e_434: $i). % 4.68/2.20 tff(e_436, type, e_436: $i). % 4.68/2.20 tff(a_429, type, a_429: $i). % 4.68/2.20 tff(a_432, type, a_432: $i). % 4.68/2.20 tff(a_431, type, a_431: $i). % 4.68/2.20 tff(a_423, type, a_423: $i). % 4.68/2.20 tff(e_420, type, e_420: $i). % 4.68/2.20 tff(e_422, type, e_422: $i). % 4.68/2.20 tff(i1, type, i1: $i). % 4.68/2.20 tff(e_430, type, e_430: $i). % 4.68/2.20 tff(i2, type, i2: $i). % 4.68/2.20 tff(a_437, type, a_437: $i). % 4.68/2.20 tff(select, type, select: ($i * $i) > $i). % 4.68/2.20 tff(e_438, type, e_438: $i). % 4.68/2.20 tff(a_425, type, a_425: $i). % 4.68/2.20 tff(i0, type, i0: $i). % 4.68/2.20 tff(e_424, type, e_424: $i). % 4.68/2.20 tff(i3, type, i3: $i). % 4.68/2.20 % 4.68/2.20 %Saturated clause set: % 4.68/2.20 tff(c_1722, plain, (store(a_427, i2, e_420)=a_429)). % 4.68/2.20 tff(c_1789, plain, (select(a1, i2)=e_420)). % 4.68/2.20 tff(c_1721, plain, (select(a_429, i2)=e_420)). % 4.68/2.20 tff(c_1199, plain, (![J_14]: (select(a_418, J_14)=select(a1, J_14) | i0=J_14))). % 4.68/2.20 tff(c_1720, plain, (select(a_425, i0)=e_420)). % 4.68/2.20 tff(c_1719, plain, (select(a_423, i0)=e_420)). % 4.68/2.20 tff(c_1723, plain, (select(a_427, i0)=e_420)). % 4.68/2.20 tff(c_1685, plain, (e_428=e_420)). % 4.68/2.20 tff(c_1287, plain, (![J_5]: (select(a_419, J_5)=select(a_418, J_5) | i0=J_5))). % 4.68/2.20 tff(c_414, plain, (![J_14]: (select(a_423, J_14)=select(a_421, J_14) | i2=J_14))). % 4.68/2.20 tff(c_1602, plain, (store(a_439, i2, e_420)=a_441)). % 4.68/2.20 tff(c_1604, plain, (select(a_437, i0)=e_420)). % 4.68/2.20 tff(c_1603, plain, (select(a_441, i2)=e_420)). % 4.68/2.20 tff(c_1610, plain, (select(a_435, i0)=e_420)). % 4.68/2.20 tff(c_1600, plain, (e_440=e_420)). % 4.68/2.20 tff(c_258, plain, (![J_14]: (select(a_437, J_14)=select(a_435, J_14) | i2=J_14))). % 4.68/2.20 tff(c_261, plain, (![J_14]: (select(a_431, J_14)=select(a_429, J_14) | i0=J_14))). % 4.68/2.20 tff(c_1536, plain, (select(a_418, i2)=e_420)). % 4.68/2.20 tff(c_1314, plain, (store(a_433, i2, e_417)=a_435)). % 4.68/2.20 tff(c_1313, plain, (store(a_437, i0, e_417)=a_439)). % 4.68/2.20 tff(c_1220, plain, (store(a_423, i2, e_417)=a_425)). % 4.68/2.20 tff(c_1316, plain, (store(a_435, i2, e_417)=a_437)). % 4.68/2.20 tff(c_1218, plain, (store(a_419, i2, e_417)=a_432)). % 4.68/2.20 tff(c_1219, plain, (store(a_421, i2, e_417)=a_423)). % 4.68/2.20 tff(c_1226, plain, (store(a_429, i0, e_417)=a_431)). % 4.68/2.20 tff(c_234, plain, (![J_14]: (select(a_429, J_14)=select(a_427, J_14) | i2=J_14))). % 4.68/2.20 tff(c_1225, plain, (store(a_425, i2, e_417)=a_427)). % 4.68/2.20 tff(c_1317, plain, (select(a_439, i0)=e_417)). % 4.68/2.20 tff(c_1224, plain, (select(a_423, i2)=e_417)). % 4.68/2.20 tff(c_1318, plain, (select(a_437, i2)=e_417)). % 4.68/2.20 tff(c_1315, plain, (select(a_435, i2)=e_417)). % 4.68/2.20 tff(c_1203, plain, (store(a1, i0, e_417)=a_418)). % 4.68/2.20 tff(c_1321, plain, (select(a_433, i2)=e_417)). % 4.68/2.21 tff(c_1222, plain, (select(a_425, i2)=e_417)). % 4.68/2.21 tff(c_1320, plain, (e_436=e_417)). % 4.68/2.21 tff(c_1330, plain, (![J_14]: (select(a_432, J_14)=select(a_419, J_14) | i2=J_14))). % 4.68/2.21 tff(c_1319, plain, (e_438=e_417)). % 4.68/2.21 tff(c_1308, plain, (e_434=e_417)). % 4.68/2.21 tff(c_1221, plain, (select(a_432, i2)=e_417)). % 4.68/2.21 tff(c_1227, plain, (select(a_427, i2)=e_417)). % 4.68/2.21 tff(c_1202, plain, (store(a_418, i0, e_417)=a_419)). % 4.68/2.21 tff(c_1228, plain, (select(a_431, i0)=e_417)). % 4.68/2.21 tff(c_1201, plain, (select(a_418, i0)=e_417)). % 4.68/2.21 tff(c_246, plain, (![J_14]: (select(a_433, J_14)=select(a_432, J_14) | i0=J_14))). % 4.68/2.21 tff(c_1223, plain, (e_424=e_417)). % 4.68/2.21 tff(c_1230, plain, (e_426=e_417)). % 4.68/2.21 tff(c_1229, plain, (e_430=e_417)). % 4.68/2.21 tff(c_1213, plain, (e_422=e_417)). % 4.68/2.21 tff(c_1200, plain, (select(a_419, i0)=e_417)). % 4.68/2.21 tff(c_1204, plain, (select(a1, i0)=e_417)). % 4.68/2.21 tff(c_1197, plain, (i1=i0)). % 4.68/2.21 tff(c_243, plain, (![J_14]: (select(a_421, J_14)=select(a_419, J_14) | i0=J_14))). % 4.68/2.21 tff(c_1108, plain, (![J_14]: (select(a_435, J_14)=select(a_433, J_14) | i2=J_14))). % 4.68/2.21 tff(c_1088, plain, (i2!=i0)). % 4.68/2.21 tff(c_273, plain, (![J_14]: (select(a_427, J_14)=select(a_425, J_14) | i2=J_14))). % 4.68/2.21 tff(c_525, plain, (![J_14]: (select(a_425, J_14)=select(a_423, J_14) | i2=J_14))). % 4.68/2.21 tff(c_425, plain, (select(a_419, i2)=e_420)). % 4.68/2.21 tff(c_451, plain, (![J_14]: (select(a_441, J_14)=select(a_439, J_14) | i2=J_14))). % 4.68/2.21 tff(c_413, plain, (i3=i2)). % 4.68/2.21 tff(c_255, plain, (![J_14]: (select(a_439, J_14)=select(a_437, J_14) | i0=J_14))). % 4.68/2.21 tff(c_178, plain, (select(a_433, i0)=e_420)). % 4.68/2.21 tff(c_175, plain, (select(a_421, i0)=e_420)). % 4.68/2.21 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.68/2.21 tff(c_2, plain, (![A_1, I_2, E_3]: (select(store(A_1, I_2, E_3), I_2)=E_3))). % 4.68/2.21 tff(c_10, plain, (store(a_419, i0, e_420)=a_421)). % 4.68/2.21 tff(c_24, plain, (store(a_432, i0, e_420)=a_433)). % 4.68/2.21 tff(c_56, plain, (a_441!=a_431)). % 4.68/2.21 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 4.68/2.21 %------------------------------------------------------------------------------