%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SWV556-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 : n016.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:13 PM UTC 2025 % Result : Satisfiable 4.71s 2.10s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.11 % Problem : SWV556-1.004 : TPTP v9.0.0. Released v4.0.0. % 0.10/0.12 % 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.31 % Computer : n016.cluster.edu % 0.12/0.31 % Model : x86_64 x86_64 % 0.12/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.31 % Memory : 8042.1875MB % 0.12/0.31 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.31 % CPULimit : 300 % 0.12/0.31 % WCLimit : 300 % 0.12/0.31 % DateTime : Wed Apr 9 04:01:53 EDT 2025 % 0.12/0.31 % CPUTime : % 4.71/2.10 % 4.71/2.10 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 4.71/2.10 % 4.71/2.10 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 4.71/2.11 %$ store > sk > select > #nlpp > i_35 > i4 > i3 > i2 > i1 > e_37 > e_36 > e_33 > e_31 > e_29 > e_27 > e_25 > e_23 > e_21 > e_19 > a_34 > a_32 > a_30 > a_28 > a_26 > a_24 > a_22 > a_20 > a2 > a1 % 4.71/2.11 % 4.71/2.11 %Foreground sorts: % 4.71/2.11 % 4.71/2.11 % 4.71/2.11 %Background operators: % 4.71/2.11 % 4.71/2.11 % 4.71/2.11 %Foreground operators: % 4.71/2.11 tff(a1, type, a1: $i). % 4.71/2.11 tff(i_35, type, i_35: $i). % 4.71/2.11 tff(a_26, type, a_26: $i). % 4.71/2.11 tff(e_29, type, e_29: $i). % 4.71/2.11 tff(e_23, type, e_23: $i). % 4.71/2.11 tff(e_33, type, e_33: $i). % 4.71/2.11 tff(e_27, type, e_27: $i). % 4.71/2.11 tff(a_34, type, a_34: $i). % 4.71/2.11 tff(store, type, store: ($i * $i * $i) > $i). % 4.71/2.11 tff(e_21, type, e_21: $i). % 4.71/2.11 tff(a_30, type, a_30: $i). % 4.71/2.11 tff(a_22, type, a_22: $i). % 4.71/2.11 tff(a2, type, a2: $i). % 4.71/2.11 tff(sk, type, sk: ($i * $i) > $i). % 4.71/2.11 tff(a_32, type, a_32: $i). % 4.71/2.11 tff(i1, type, i1: $i). % 4.71/2.11 tff(i2, type, i2: $i). % 4.71/2.11 tff(e_37, type, e_37: $i). % 4.71/2.11 tff(select, type, select: ($i * $i) > $i). % 4.71/2.11 tff(e_19, type, e_19: $i). % 4.71/2.11 tff(a_24, type, a_24: $i). % 4.71/2.11 tff(a_20, type, a_20: $i). % 4.71/2.11 tff(a_28, type, a_28: $i). % 4.71/2.11 tff(e_31, type, e_31: $i). % 4.71/2.11 tff(i4, type, i4: $i). % 4.71/2.11 tff(i3, type, i3: $i). % 4.71/2.11 tff(e_25, type, e_25: $i). % 4.71/2.11 tff(e_36, type, e_36: $i). % 4.71/2.11 % 4.71/2.11 %Saturated clause set: % 4.71/2.11 tff(c_1610, plain, (sk(a1, a2)=i1)). % 4.71/2.11 tff(c_1624, plain, (e_21!=e_19)). % 4.71/2.11 tff(c_1614, plain, (e_37=e_19)). % 4.71/2.11 tff(c_1613, plain, (e_36=e_21)). % 4.71/2.11 tff(c_1609, plain, (i_35=i1)). % 4.71/2.11 tff(c_1545, plain, (![J_14]: (select(a2, J_14)=select(a1, J_14) | i2=J_14 | i2=J_14 | i2=J_14 | i1=J_14 | i2=J_14 | i2=J_14 | i1=J_14 | i1=J_14))). % 4.71/2.11 tff(c_1509, plain, (![J_14]: (select(a_20, J_14)=select(a2, J_14) | i2=J_14 | i2=J_14 | i2=J_14 | i1=J_14 | i2=J_14 | i2=J_14 | i1=J_14))). % 4.71/2.11 tff(c_1470, plain, (![J_41]: (select(a_22, J_41)=select(a_20, J_41) | i2=J_41 | i2=J_41 | i2=J_41 | i1=J_41 | i2=J_41 | i2=J_41))). % 4.71/2.11 tff(c_1445, plain, (![J_14]: (select(a_24, J_14)=select(a_22, J_14) | i2=J_14 | i2=J_14 | i1=J_14 | i2=J_14 | i2=J_14))). % 4.71/2.11 tff(c_1403, plain, (![J_39]: (select(a_26, J_39)=select(a_24, J_39) | i2=J_39 | i2=J_39 | i1=J_39 | i2=J_39))). % 4.71/2.11 tff(c_1384, plain, (![J_14]: (select(a_28, J_14)=select(a_26, J_14) | i2=J_14 | i1=J_14 | i2=J_14))). % 4.81/2.11 tff(c_1130, plain, (![J_14]: (select(a_30, J_14)=select(a_28, J_14) | i2=J_14 | i1=J_14))). % 4.81/2.11 tff(c_1207, plain, (store(a_28, i1, e_21)=a_32)). % 4.81/2.11 tff(c_1210, plain, (store(a_26, i2, e_21)=a_30)). % 4.81/2.11 tff(c_1214, plain, (store(a_20, i2, e_21)=a_24)). % 4.81/2.11 tff(c_1205, plain, (select(a_30, i1)=e_21)). % 4.81/2.11 tff(c_1208, plain, (select(a_32, i1)=e_21)). % 4.81/2.11 tff(c_1213, plain, (select(a_24, i2)=e_21)). % 4.81/2.11 tff(c_1206, plain, (select(a2, i2)=e_21)). % 4.81/2.11 tff(c_1215, plain, (select(a_22, i2)=e_21)). % 4.81/2.11 tff(c_1211, plain, (select(a_30, i2)=e_21)). % 4.81/2.11 tff(c_1229, plain, (select(a_26, i1)=e_21)). % 4.81/2.11 tff(c_1212, plain, (e_29=e_21)). % 4.81/2.11 tff(c_1209, plain, (e_31=e_21)). % 4.81/2.11 tff(c_1200, plain, (e_23=e_21)). % 4.81/2.11 tff(c_1179, plain, (select(a1, i2)=e_25)). % 4.81/2.11 tff(c_211, plain, (![J_14]: (select(a_20, J_14)=select(a1, J_14) | i1=J_14))). % 4.81/2.11 tff(c_1111, plain, (![J_14]: (select(a_32, J_14)=select(a_30, J_14) | i2=J_14))). % 4.81/2.11 tff(c_1091, plain, (![J_14]: (select(a_28, J_14)=select(a_24, J_14) | i2=J_14))). % 4.81/2.11 tff(c_193, plain, (![J_14]: (select(a_32, J_14)=select(a_28, J_14) | i1=J_14))). % 4.81/2.11 tff(c_992, plain, (i2!=i1)). % 4.81/2.11 tff(c_199, plain, (![J_14]: (select(a_26, J_14)=select(a_22, J_14) | i2=J_14))). % 4.81/2.11 tff(c_409, plain, (store(a_30, i2, e_25)=a_32)). % 4.81/2.11 tff(c_389, plain, (select(a_32, i2)=e_25)). % 4.81/2.11 tff(c_205, plain, (![J_14]: (select(a_22, J_14)=select(a2, J_14) | i1=J_14))). % 4.81/2.11 tff(c_348, plain, (e_33=e_25)). % 4.81/2.11 tff(c_343, plain, (i4=i2)). % 4.81/2.11 tff(c_330, plain, (store(a_24, i2, e_25)=a_28)). % 4.81/2.11 tff(c_313, plain, (select(a_28, i2)=e_25)). % 4.81/2.11 tff(c_278, plain, (![J_14]: (select(a_30, J_14)=select(a_26, J_14) | i2=J_14))). % 4.81/2.11 tff(c_268, plain, (e_27=e_25)). % 4.81/2.11 tff(c_261, plain, (i3=i2)). % 4.81/2.11 tff(c_208, plain, (![J_14]: (select(a_24, J_14)=select(a_20, J_14) | i2=J_14))). % 4.81/2.11 tff(c_146, plain, (select(a_26, i2)=e_25)). % 4.81/2.11 tff(c_152, plain, (select(a_22, i1)=e_21)). % 4.81/2.12 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.81/2.12 tff(c_158, plain, (select(a_20, i1)=e_19)). % 4.81/2.12 tff(c_2, plain, (![A_1, I_2, E_3]: (select(store(A_1, I_2, E_3), I_2)=E_3))). % 4.81/2.12 tff(c_12, plain, (store(a_22, i2, e_25)=a_26)). % 4.81/2.12 tff(c_8, plain, (store(a2, i1, e_21)=a_22)). % 4.81/2.12 tff(c_6, plain, (store(a1, i1, e_19)=a_20)). % 4.81/2.12 tff(c_22, plain, (select(a2, i1)=e_19)). % 4.81/2.12 tff(c_24, plain, (select(a1, i1)=e_21)). % 4.81/2.12 tff(c_28, plain, (select(a_20, i2)=e_25)). % 4.81/2.12 tff(c_44, plain, (a_34=a_32)). % 4.81/2.12 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 4.81/2.12 %------------------------------------------------------------------------------