%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SWV551-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 : n031.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 4.22s 2.21s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.09 % Problem : SWV551-1.004 : TPTP v9.0.0. Released v4.0.0. % 0.00/0.10 % 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.29 % Computer : n031.cluster.edu % 0.11/0.29 % Model : x86_64 x86_64 % 0.11/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.29 % Memory : 8042.1875MB % 0.11/0.29 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.29 % CPULimit : 300 % 0.11/0.29 % WCLimit : 300 % 0.11/0.29 % DateTime : Wed Apr 9 04:00:52 EDT 2025 % 0.11/0.29 % CPUTime : % 4.22/2.20 % 4.22/2.21 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 4.22/2.21 % 4.22/2.21 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 4.22/2.21 %$ 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 % 4.22/2.21 % 4.22/2.21 %Foreground sorts: % 4.22/2.21 % 4.22/2.21 % 4.22/2.21 %Background operators: % 4.22/2.21 % 4.22/2.21 % 4.22/2.21 %Foreground operators: % 4.22/2.21 tff(a1, type, a1: $i). % 4.22/2.21 tff(a_31, type, a_31: $i). % 4.22/2.21 tff(e_28, type, e_28: $i). % 4.22/2.21 tff(a_17, type, a_17: $i). % 4.22/2.21 tff(a_21, type, a_21: $i). % 4.22/2.21 tff(e_26, type, e_26: $i). % 4.22/2.21 tff(store, type, store: ($i * $i * $i) > $i). % 4.22/2.21 tff(a_23, type, a_23: $i). % 4.22/2.21 tff(a_29, type, a_29: $i). % 4.22/2.21 tff(a_27, type, a_27: $i). % 4.22/2.21 tff(e_22, type, e_22: $i). % 4.22/2.21 tff(e_20, type, e_20: $i). % 4.22/2.21 tff(a2, type, a2: $i). % 4.22/2.21 tff(i1, type, i1: $i). % 4.22/2.21 tff(e_30, type, e_30: $i). % 4.22/2.21 tff(i2, type, i2: $i). % 4.22/2.21 tff(select, type, select: ($i * $i) > $i). % 4.22/2.21 tff(e_18, type, e_18: $i). % 4.22/2.21 tff(a_25, type, a_25: $i). % 4.22/2.21 tff(e_24, type, e_24: $i). % 4.22/2.21 tff(a_19, type, a_19: $i). % 4.22/2.21 tff(e_16, type, e_16: $i). % 4.22/2.21 tff(i4, type, i4: $i). % 4.22/2.21 tff(i3, type, i3: $i). % 4.22/2.21 % 4.22/2.21 %Saturated clause set: % 4.22/2.21 tff(c_926, 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))). % 4.22/2.21 tff(c_895, plain, (![J_30]: (select(a_17, J_30)=select(a2, J_30) | i1=J_30 | i1=J_30 | i1=J_30 | i1=J_30 | i1=J_30 | i1=J_30 | i1=J_30))). % 4.22/2.21 tff(c_876, 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))). % 4.22/2.22 tff(c_851, 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))). % 4.22/2.22 tff(c_817, plain, (![J_27]: (select(a_23, J_27)=select(a_21, J_27) | i1=J_27 | i1=J_27 | i1=J_27 | i1=J_27))). % 4.22/2.22 tff(c_804, plain, (![J_14]: (select(a_25, J_14)=select(a_23, J_14) | i1=J_14 | i1=J_14 | i1=J_14))). % 4.22/2.22 tff(c_736, plain, (![J_14]: (select(a_27, J_14)=select(a_25, J_14) | i1=J_14 | i1=J_14))). % 4.22/2.22 tff(c_412, plain, (![J_14]: (select(a_25, J_14)=select(a_21, J_14) | i1=J_14))). % 4.22/2.22 tff(c_370, plain, (![J_14]: (select(a_21, J_14)=select(a_17, J_14) | i1=J_14))). % 4.22/2.22 tff(c_720, plain, (![J_5]: (select(a_29, J_5)=select(a_27, J_5) | i1=J_5))). % 4.22/2.22 tff(c_163, plain, (![J_14]: (select(a_17, J_14)=select(a1, J_14) | i1=J_14))). % 4.22/2.22 tff(c_536, plain, (store(a_23, i1, e_16)=a_27)). % 4.22/2.22 tff(c_537, plain, (store(a_17, i1, e_16)=a_21)). % 4.22/2.22 tff(c_543, plain, (store(a2, i1, e_16)=a_19)). % 4.22/2.22 tff(c_652, plain, (store(a_25, i1, e_16)=a_29)). % 4.22/2.22 tff(c_632, plain, (![J_14]: (select(a_29, J_14)=select(a_25, J_14) | i1=J_14))). % 4.22/2.22 tff(c_620, plain, (store(a_27, i1, e_16)=a_29)). % 4.22/2.22 tff(c_542, plain, (select(a_19, i1)=e_16)). % 4.22/2.22 tff(c_539, plain, (select(a_21, i1)=e_16)). % 4.22/2.22 tff(c_538, plain, (select(a_27, i1)=e_16)). % 4.22/2.22 tff(c_583, plain, (select(a_29, i1)=e_16)). % 4.22/2.22 tff(c_544, plain, (select(a1, i1)=e_16)). % 4.22/2.22 tff(c_540, plain, (e_26=e_16)). % 4.22/2.22 tff(c_541, plain, (e_20=e_16)). % 4.22/2.22 tff(c_530, plain, (e_30=e_16)). % 4.22/2.22 tff(c_549, plain, (![J_14]: (select(a_23, J_14)=select(a_19, J_14) | i1=J_14))). % 4.22/2.22 tff(c_535, plain, (e_18=e_16)). % 4.22/2.22 tff(c_524, plain, (e_28=e_16)). % 4.22/2.22 tff(c_517, plain, (i4=i1)). % 4.22/2.22 tff(c_491, plain, (store(a_21, i1, e_16)=a_25)). % 4.22/2.22 tff(c_452, plain, (![J_14]: (select(a_27, J_14)=select(a_23, J_14) | i1=J_14))). % 4.22/2.22 tff(c_447, plain, (select(a_25, i1)=e_16)). % 4.22/2.22 tff(c_432, plain, (select(a_23, i1)=e_16)). % 4.22/2.22 tff(c_417, plain, (store(a_19, i1, e_16)=a_23)). % 4.22/2.22 tff(c_369, plain, (i3=i1)). % 4.22/2.22 tff(c_383, plain, (e_24=e_16)). % 4.22/2.22 tff(c_377, plain, (e_22=e_16)). % 4.22/2.22 tff(c_364, plain, (i2=i1)). % 4.22/2.22 tff(c_175, plain, (![J_14]: (select(a_19, J_14)=select(a2, J_14) | i1=J_14))). % 4.22/2.22 tff(c_122, plain, (select(a_17, i1)=e_16)). % 4.22/2.22 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.22/2.22 tff(c_2, plain, (![A_1, I_2, E_3]: (select(store(A_1, I_2, E_3), I_2)=E_3))). % 4.22/2.22 tff(c_6, plain, (store(a1, i1, e_16)=a_17)). % 4.22/2.22 tff(c_22, plain, (select(a2, i1)=e_16)). % 4.22/2.22 tff(c_38, plain, (a_31=a_29)). % 4.22/2.22 tff(c_40, plain, (a2!=a1)). % 4.22/2.22 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 4.22/2.22 %------------------------------------------------------------------------------