%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SWV538-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:05 PM UTC 2025 % Result : Satisfiable 4.32s 1.96s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.07 % Problem : SWV538-1.004 : TPTP v9.0.0. Released v4.0.0. % 0.00/0.07 % 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.06/0.26 % Computer : n017.cluster.edu % 0.06/0.26 % Model : x86_64 x86_64 % 0.06/0.26 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.06/0.26 % Memory : 8042.1875MB % 0.06/0.26 % OS : Linux 3.10.0-693.el7.x86_64 % 0.06/0.26 % CPULimit : 300 % 0.06/0.26 % WCLimit : 300 % 0.06/0.26 % DateTime : Wed Apr 9 03:56:09 EDT 2025 % 0.06/0.26 % CPUTime : % 4.32/1.96 % 4.32/1.96 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 4.32/1.96 % 4.32/1.96 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 4.32/1.97 %$ store > sk > select > #nlpp > i_493 > i3 > i2 > i1 > i0 > e_495 > e_494 > e_491 > e_489 > e_487 > e_485 > e_481 > e_479 > e_477 > e_475 > e_473 > e_471 > e_468 > a_492 > a_490 > a_488 > a_486 > a_484 > a_483 > a_482 > a_480 > a_478 > a_476 > a_474 > a_472 > a_470 > a_469 > a1 % 4.32/1.97 % 4.32/1.97 %Foreground sorts: % 4.32/1.97 % 4.32/1.97 % 4.32/1.97 %Background operators: % 4.32/1.97 % 4.32/1.97 % 4.32/1.97 %Foreground operators: % 4.32/1.97 tff(e_487, type, e_487: $i). % 4.32/1.97 tff(a1, type, a1: $i). % 4.32/1.97 tff(a_476, type, a_476: $i). % 4.32/1.97 tff(a_492, type, a_492: $i). % 4.32/1.97 tff(a_480, type, a_480: $i). % 4.32/1.97 tff(a_484, type, a_484: $i). % 4.32/1.97 tff(store, type, store: ($i * $i * $i) > $i). % 4.32/1.97 tff(a_486, type, a_486: $i). % 4.32/1.97 tff(a_488, type, a_488: $i). % 4.32/1.97 tff(a_478, type, a_478: $i). % 4.32/1.97 tff(a_470, type, a_470: $i). % 4.32/1.97 tff(e_473, type, e_473: $i). % 4.32/1.97 tff(e_494, type, e_494: $i). % 4.32/1.97 tff(a_474, type, a_474: $i). % 4.32/1.97 tff(a_482, type, a_482: $i). % 4.32/1.97 tff(a_469, type, a_469: $i). % 4.32/1.97 tff(i_493, type, i_493: $i). % 4.32/1.97 tff(e_475, type, e_475: $i). % 4.32/1.97 tff(sk, type, sk: ($i * $i) > $i). % 4.32/1.97 tff(i1, type, i1: $i). % 4.32/1.97 tff(e_468, type, e_468: $i). % 4.32/1.97 tff(i2, type, i2: $i). % 4.32/1.97 tff(a_472, type, a_472: $i). % 4.32/1.97 tff(e_489, type, e_489: $i). % 4.32/1.97 tff(select, type, select: ($i * $i) > $i). % 4.32/1.97 tff(e_471, type, e_471: $i). % 4.32/1.97 tff(e_479, type, e_479: $i). % 4.32/1.97 tff(e_491, type, e_491: $i). % 4.32/1.97 tff(e_481, type, e_481: $i). % 4.32/1.97 tff(e_485, type, e_485: $i). % 4.32/1.97 tff(e_495, type, e_495: $i). % 4.32/1.97 tff(a_490, type, a_490: $i). % 4.32/1.97 tff(i0, type, i0: $i). % 4.32/1.97 tff(a_483, type, a_483: $i). % 4.32/1.97 tff(i3, type, i3: $i). % 4.32/1.97 tff(e_477, type, e_477: $i). % 4.32/1.97 % 4.32/1.97 %Saturated clause set: % 4.32/1.97 tff(c_1373, plain, (![J_14]: (select(a_470, J_14)=select(a_469, J_14) | i0=J_14))). % 4.32/1.97 tff(c_1632, plain, (select(a1, i2)=e_475)). % 4.32/1.97 tff(c_1372, plain, (![J_14]: (select(a_469, J_14)=select(a1, J_14) | i0=J_14))). % 4.32/1.97 tff(c_1246, plain, (![J_14]: (select(a_490, J_14)=select(a_478, J_14) | i0=J_14))). % 4.32/1.97 tff(c_361, plain, (![J_5]: (select(a_478, J_5)=select(a_476, J_5) | i2=J_5))). % 4.32/1.97 tff(c_1557, plain, (select(a_469, i2)=e_475)). % 4.32/1.97 tff(c_1399, plain, (store(a_472, i0, e_468)=a_474)). % 4.32/1.97 tff(c_1400, plain, (store(a_476, i2, e_468)=a_478)). % 4.32/1.97 tff(c_1398, plain, (store(a_480, i0, e_468)=a_482)). % 4.32/1.97 tff(c_1409, plain, (store(a_470, i0, e_468)=a_472)). % 4.32/1.97 tff(c_1376, plain, (store(a_469, i0, e_468)=a_470)). % 4.32/1.97 tff(c_1402, plain, (select(a_474, i0)=e_468)). % 4.32/1.97 tff(c_1401, plain, (select(a_482, i0)=e_468)). % 4.32/1.97 tff(c_1403, plain, (select(a_478, i2)=e_468)). % 4.32/1.97 tff(c_1377, plain, (store(a1, i0, e_468)=a_469)). % 4.32/1.97 tff(c_1408, plain, (select(a_472, i0)=e_468)). % 4.32/1.97 tff(c_1396, plain, (e_475!=e_468)). % 4.32/1.97 tff(c_1397, plain, (e_494=e_468)). % 4.32/1.97 tff(c_265, plain, (![J_14]: (select(a_482, J_14)=select(a_480, J_14) | i0=J_14))). % 4.32/1.97 tff(c_1407, plain, (e_487=e_468)). % 4.32/1.97 tff(c_1406, plain, (e_473=e_468)). % 4.32/1.97 tff(c_1405, plain, (e_481=e_468)). % 4.32/1.97 tff(c_1404, plain, (e_477=e_468)). % 4.32/1.97 tff(c_1387, plain, (e_471=e_468)). % 4.32/1.97 tff(c_1378, plain, (select(a1, i0)=e_468)). % 4.32/1.97 tff(c_1375, plain, (select(a_470, i0)=e_468)). % 4.32/1.97 tff(c_1374, plain, (select(a_469, i0)=e_468)). % 4.32/1.97 tff(c_1349, plain, (i1=i0)). % 4.32/1.97 tff(c_1350, plain, (![J_14]: (select(a_476, J_14)=select(a_474, J_14) | i0=J_14))). % 4.32/1.97 tff(c_1327, plain, (sk(a_482, a_492)=i0)). % 4.32/1.97 tff(c_1328, plain, (e_495=e_475)). % 4.32/1.97 tff(c_1324, plain, (i_493=i0)). % 4.32/1.97 tff(c_1289, plain, (store(a_478, i0, e_475)=a_490)). % 4.32/1.97 tff(c_1258, plain, (select(a_480, i2)=e_475)). % 4.32/1.97 tff(c_1259, plain, (store(a_478, i2, e_475)=a_480)). % 4.32/1.97 tff(c_1253, plain, (e_479=e_475)). % 4.32/1.97 tff(c_1245, plain, (select(a_478, i0)=e_475)). % 4.32/1.97 tff(c_1214, plain, (a_488=a_478)). % 4.32/1.97 tff(c_1219, plain, (![J_14]: (select(a_492, J_14)=select(a_490, J_14) | i0=J_14))). % 4.32/1.97 tff(c_1209, plain, (a_486=a_476)). % 4.32/1.97 tff(c_1194, plain, (select(a_470, i2)=e_475)). % 4.32/1.97 tff(c_1150, plain, (select(a_472, i2)=e_475)). % 4.32/1.97 tff(c_1173, plain, (store(a_490, i0, e_475)=a_492)). % 4.32/1.97 tff(c_1095, plain, (select(a_492, i0)=e_475)). % 4.32/1.97 tff(c_1123, plain, (![J_14]: (select(a_474, J_14)=select(a_472, J_14) | i0=J_14))). % 4.32/1.97 tff(c_1094, plain, (select(a_490, i0)=e_475)). % 4.32/1.97 tff(c_1097, plain, (e_491=e_475)). % 4.32/1.97 tff(c_1096, plain, (e_489=e_475)). % 4.32/1.97 tff(c_1087, plain, (e_485=e_475)). % 4.32/1.97 tff(c_1067, plain, (a_484=a_474)). % 4.32/1.98 tff(c_438, plain, (store(a_474, i0, e_475)=a_476)). % 4.32/1.98 tff(c_1062, plain, (a_483=a_472)). % 4.32/1.98 tff(c_891, plain, (i2!=i0)). % 4.32/1.98 tff(c_431, plain, (select(a_476, i0)=e_475)). % 4.32/1.98 tff(c_268, plain, (![J_14]: (select(a_480, J_14)=select(a_478, J_14) | i2=J_14))). % 4.32/1.98 tff(c_430, plain, (i3=i0)). % 4.32/1.98 tff(c_280, plain, (![J_14]: (select(a_472, J_14)=select(a_470, J_14) | i0=J_14))). % 4.32/1.98 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.32/1.98 tff(c_2, plain, (![A_1, I_2, E_3]: (select(store(A_1, I_2, E_3), I_2)=E_3))). % 4.32/1.98 tff(c_40, plain, (select(a_474, i2)=e_475)). % 4.32/1.98 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 4.32/1.98 %------------------------------------------------------------------------------