%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SWV552-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/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % Computer : n007.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:11 PM UTC 2025 % Result : Satisfiable 3.64s 1.96s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SWV552-1.004 : TPTP v9.0.0. Released v4.0.0. % 0.03/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % 0.12/0.34 % Computer : n007.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Wed Apr 9 04:01:09 EDT 2025 % 0.12/0.34 % CPUTime : % 3.64/1.96 % 3.64/1.96 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 3.64/1.96 % 3.64/1.96 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 3.64/1.97 %$ store > select > #nlpp > i4 > i3 > i2 > i1 > e_30 > e_28 > e_26 > e_24 > e_22 > e_20 > e_18 > e_16 > a_31 > a_29 > a_27 > a_25 > a_23 > a_21 > a_19 > a_17 > a2 > a1 % 3.64/1.97 % 3.64/1.97 %Foreground sorts: % 3.64/1.97 % 3.64/1.97 % 3.64/1.97 %Background operators: % 3.64/1.97 % 3.64/1.97 % 3.64/1.97 %Foreground operators: % 3.64/1.97 tff(a1, type, a1: $i). % 3.64/1.97 tff(a_31, type, a_31: $i). % 3.64/1.97 tff(e_28, type, e_28: $i). % 3.64/1.97 tff(a_17, type, a_17: $i). % 3.64/1.97 tff(a_21, type, a_21: $i). % 3.64/1.97 tff(e_26, type, e_26: $i). % 3.64/1.97 tff(store, type, store: ($i * $i * $i) > $i). % 3.64/1.97 tff(a_23, type, a_23: $i). % 3.64/1.97 tff(a_29, type, a_29: $i). % 3.64/1.97 tff(a_27, type, a_27: $i). % 3.64/1.97 tff(e_22, type, e_22: $i). % 3.64/1.97 tff(e_20, type, e_20: $i). % 3.64/1.97 tff(a2, type, a2: $i). % 3.64/1.97 tff(i1, type, i1: $i). % 3.64/1.97 tff(e_30, type, e_30: $i). % 3.64/1.97 tff(i2, type, i2: $i). % 3.64/1.97 tff(select, type, select: ($i * $i) > $i). % 3.64/1.97 tff(e_18, type, e_18: $i). % 3.64/1.97 tff(a_25, type, a_25: $i). % 3.64/1.97 tff(e_24, type, e_24: $i). % 3.64/1.97 tff(a_19, type, a_19: $i). % 3.64/1.97 tff(e_16, type, e_16: $i). % 3.64/1.97 tff(i4, type, i4: $i). % 3.64/1.97 tff(i3, type, i3: $i). % 3.64/1.97 % 3.64/1.97 %Saturated clause set: % 3.64/1.97 tff(c_866, plain, (![J_14]: (select(a2, J_14)=select(a1, J_14) | i1=J_14 | i1=J_14 | i1=J_14 | i1=J_14 | i1=J_14 | i1=J_14 | i1=J_14 | i1=J_14))). % 3.64/1.97 tff(c_844, plain, (![J_14]: (select(a_17, J_14)=select(a2, J_14) | i1=J_14 | i1=J_14 | i1=J_14 | i1=J_14 | i1=J_14 | i1=J_14 | i1=J_14))). % 3.64/1.97 tff(c_819, plain, (![J_14]: (select(a_19, J_14)=select(a_17, J_14) | i1=J_14 | i1=J_14 | i1=J_14 | i1=J_14 | i1=J_14 | i1=J_14))). % 3.64/1.97 tff(c_791, plain, (![J_14]: (select(a_21, J_14)=select(a_19, J_14) | i1=J_14 | i1=J_14 | i1=J_14 | i1=J_14 | i1=J_14))). % 3.64/1.97 tff(c_766, plain, (![J_14]: (select(a_23, J_14)=select(a_21, J_14) | i1=J_14 | i1=J_14 | i1=J_14 | i1=J_14))). % 3.64/1.97 tff(c_741, plain, (![J_14]: (select(a_25, J_14)=select(a_23, J_14) | i1=J_14 | i1=J_14 | i1=J_14))). % 3.64/1.97 tff(c_700, plain, (![J_14]: (select(a_27, J_14)=select(a_25, J_14) | i1=J_14 | i1=J_14))). % 3.64/1.97 tff(c_408, plain, (![J_14]: (select(a_27, J_14)=select(a_23, J_14) | i1=J_14))). % 3.64/1.97 tff(c_350, plain, (![J_14]: (select(a_29, J_14)=select(a_27, J_14) | i1=J_14))). % 3.64/1.97 tff(c_163, plain, (![J_14]: (select(a_17, J_14)=select(a1, J_14) | i1=J_14))). % 3.64/1.97 tff(c_638, plain, (![J_14]: (select(a_25, J_14)=select(a_21, J_14) | i1=J_14))). % 3.64/1.97 tff(c_497, plain, (store(a2, i1, e_16)=a_19)). % 3.64/1.97 tff(c_493, plain, (store(a_17, i1, e_16)=a_21)). % 3.64/1.97 tff(c_604, plain, (store(a_25, i1, e_16)=a_29)). % 3.64/1.97 tff(c_592, plain, (store(a_23, i1, e_16)=a_27)). % 3.64/1.97 tff(c_580, plain, (store(a_27, i1, e_16)=a_29)). % 3.64/1.97 tff(c_488, plain, (select(a_29, i1)=e_16)). % 3.64/1.97 tff(c_491, plain, (select(a_27, i1)=e_16)). % 3.64/1.97 tff(c_494, plain, (select(a_21, i1)=e_16)). % 3.64/1.97 tff(c_537, plain, (![J_14]: (select(a_21, J_14)=select(a_17, J_14) | i1=J_14))). % 3.64/1.97 tff(c_496, plain, (select(a_19, i1)=e_16)). % 3.64/1.97 tff(c_489, plain, (e_30=e_16)). % 3.64/1.97 tff(c_492, plain, (e_26=e_16)). % 3.64/1.97 tff(c_495, plain, (e_20=e_16)). % 3.64/1.97 tff(c_490, plain, (e_28=e_16)). % 3.64/1.97 tff(c_498, plain, (select(a1, i1)=e_16)). % 3.64/1.97 tff(c_487, plain, (e_18=e_16)). % 3.64/1.97 tff(c_166, plain, (![J_14]: (select(a_29, J_14)=select(a_25, J_14) | i1=J_14))). % 3.64/1.97 tff(c_458, plain, (select(a_25, i1)=e_16)). % 3.64/1.97 tff(c_425, plain, (store(a_21, i1, e_16)=a_25)). % 3.64/1.97 tff(c_415, plain, (e_24=e_16)). % 3.64/1.97 tff(c_407, plain, (i3=i1)). % 3.64/1.97 tff(c_381, plain, (![J_14]: (select(a_23, J_14)=select(a_19, J_14) | i1=J_14))). % 3.64/1.97 tff(c_349, plain, (i4=i1)). % 3.64/1.97 tff(c_299, plain, (store(a_19, i1, e_16)=a_23)). % 3.64/1.97 tff(c_269, plain, (select(a_23, i1)=e_16)). % 3.64/1.97 tff(c_250, plain, (e_22=e_16)). % 3.64/1.97 tff(c_243, plain, (i2=i1)). % 3.64/1.97 tff(c_175, plain, (![J_14]: (select(a_19, J_14)=select(a2, J_14) | i1=J_14))). % 3.64/1.97 tff(c_122, plain, (select(a_17, i1)=e_16)). % 3.64/1.97 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))). % 3.64/1.97 tff(c_2, plain, (![A_1, I_2, E_3]: (select(store(A_1, I_2, E_3), I_2)=E_3))). % 3.64/1.97 tff(c_6, plain, (store(a1, i1, e_16)=a_17)). % 3.64/1.97 tff(c_22, plain, (select(a2, i1)=e_16)). % 3.64/1.97 tff(c_38, plain, (a_31=a_29)). % 3.64/1.97 tff(c_40, plain, (a2!=a1)). % 3.64/1.98 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 3.64/1.98 %------------------------------------------------------------------------------