%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SWV551-1.007 : 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 5.18s 2.23s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWV551-1.007 : TPTP v9.0.0. Released v4.0.0. % 0.12/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.13/0.34 % Computer : n007.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 04:00:54 EDT 2025 % 0.19/0.34 % CPUTime : % 5.18/2.23 % 5.18/2.23 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 5.18/2.23 % 5.18/2.23 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 5.18/2.24 %$ store > select > #nlpp > i7 > i6 > i5 > i4 > i3 > i2 > i1 > e_54 > e_52 > e_50 > e_48 > e_46 > e_44 > e_42 > e_40 > e_38 > e_36 > e_34 > e_32 > e_30 > e_28 > a_55 > a_53 > a_51 > a_49 > a_47 > a_45 > a_43 > a_41 > a_39 > a_37 > a_35 > a_33 > a_31 > a_29 > a2 > a1 % 5.18/2.24 % 5.18/2.24 %Foreground sorts: % 5.18/2.24 % 5.18/2.24 % 5.18/2.24 %Background operators: % 5.18/2.24 % 5.18/2.24 % 5.18/2.24 %Foreground operators: % 5.18/2.24 tff(e_48, type, e_48: $i). % 5.18/2.24 tff(a1, type, a1: $i). % 5.18/2.24 tff(a_31, type, a_31: $i). % 5.18/2.24 tff(e_46, type, e_46: $i). % 5.18/2.24 tff(a_55, type, a_55: $i). % 5.18/2.24 tff(e_34, type, e_34: $i). % 5.18/2.24 tff(e_28, type, e_28: $i). % 5.18/2.24 tff(a_53, type, a_53: $i). % 5.18/2.24 tff(a_49, type, a_49: $i). % 5.18/2.24 tff(a_41, type, a_41: $i). % 5.18/2.24 tff(store, type, store: ($i * $i * $i) > $i). % 5.18/2.24 tff(a_43, type, a_43: $i). % 5.18/2.24 tff(e_50, type, e_50: $i). % 5.18/2.24 tff(a_29, type, a_29: $i). % 5.18/2.24 tff(a_35, type, a_35: $i). % 5.18/2.24 tff(a_37, type, a_37: $i). % 5.18/2.24 tff(e_40, type, e_40: $i). % 5.18/2.24 tff(a_33, type, a_33: $i). % 5.18/2.24 tff(a2, type, a2: $i). % 5.18/2.24 tff(i7, type, i7: $i). % 5.18/2.24 tff(e_42, type, e_42: $i). % 5.18/2.24 tff(e_52, type, e_52: $i). % 5.18/2.24 tff(e_32, type, e_32: $i). % 5.18/2.24 tff(i1, type, i1: $i). % 5.18/2.24 tff(e_30, type, e_30: $i). % 5.18/2.24 tff(i2, type, i2: $i). % 5.18/2.24 tff(a_39, type, a_39: $i). % 5.18/2.24 tff(select, type, select: ($i * $i) > $i). % 5.18/2.24 tff(e_44, type, e_44: $i). % 5.18/2.24 tff(e_54, type, e_54: $i). % 5.18/2.24 tff(a_45, type, a_45: $i). % 5.18/2.24 tff(a_47, type, a_47: $i). % 5.18/2.24 tff(e_38, type, e_38: $i). % 5.18/2.24 tff(a_51, type, a_51: $i). % 5.18/2.24 tff(i5, type, i5: $i). % 5.18/2.24 tff(i4, type, i4: $i). % 5.18/2.24 tff(i3, type, i3: $i). % 5.18/2.24 tff(e_36, type, e_36: $i). % 5.18/2.24 tff(i6, type, i6: $i). % 5.18/2.24 % 5.18/2.24 %Saturated clause set: % 5.18/2.24 tff(c_1794, plain, (![J_45]: (select(a2, J_45)=select(a1, J_45) | i1=J_45 | i1=J_45 | i1=J_45 | i1=J_45 | i1=J_45 | i1=J_45 | i1=J_45 | i1=J_45 | i1=J_45 | i1=J_45 | i1=J_45 | i1=J_45 | i1=J_45 | i1=J_45))). % 5.18/2.24 tff(c_1781, plain, (![J_14]: (select(a_29, 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 | i1=J_14 | i1=J_14 | i1=J_14 | i1=J_14 | i1=J_14 | i1=J_14))). % 5.18/2.24 tff(c_1756, plain, (![J_14]: (select(a_31, J_14)=select(a_29, 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 | i1=J_14 | i1=J_14 | i1=J_14 | i1=J_14))). % 5.18/2.24 tff(c_1719, plain, (![J_42]: (select(a_33, J_42)=select(a_31, J_42) | i1=J_42 | i1=J_42 | i1=J_42 | i1=J_42 | i1=J_42 | i1=J_42 | i1=J_42 | i1=J_42 | i1=J_42 | i1=J_42 | i1=J_42))). % 5.18/2.24 tff(c_1703, plain, (![J_14]: (select(a_35, J_14)=select(a_33, 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 | i1=J_14 | i1=J_14))). % 5.18/2.24 tff(c_1669, plain, (![J_40]: (select(a_37, J_40)=select(a_35, J_40) | i1=J_40 | i1=J_40 | i1=J_40 | i1=J_40 | i1=J_40 | i1=J_40 | i1=J_40 | i1=J_40 | i1=J_40))). % 5.18/2.24 tff(c_1656, plain, (![J_14]: (select(a_39, J_14)=select(a_37, 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))). % 5.18/2.24 tff(c_1628, plain, (![J_14]: (select(a_41, J_14)=select(a_39, J_14) | i1=J_14 | i1=J_14 | i1=J_14 | i1=J_14 | i1=J_14 | i1=J_14 | i1=J_14))). % 5.18/2.24 tff(c_1594, plain, (![J_37]: (select(a_43, J_37)=select(a_41, J_37) | i1=J_37 | i1=J_37 | i1=J_37 | i1=J_37 | i1=J_37 | i1=J_37))). % 5.18/2.24 tff(c_1581, plain, (![J_14]: (select(a_45, J_14)=select(a_43, J_14) | i1=J_14 | i1=J_14 | i1=J_14 | i1=J_14 | i1=J_14))). % 5.18/2.25 tff(c_1544, plain, (![J_35]: (select(a_47, J_35)=select(a_45, J_35) | i1=J_35 | i1=J_35 | i1=J_35 | i1=J_35))). % 5.18/2.25 tff(c_1528, plain, (![J_5]: (select(a_49, J_5)=select(a_47, J_5) | i1=J_5 | i1=J_5 | i1=J_5))). % 5.18/2.25 tff(c_1420, plain, (![J_5]: (select(a_51, J_5)=select(a_49, J_5) | i1=J_5 | i1=J_5))). % 5.18/2.25 tff(c_1077, plain, (![J_14]: (select(a_45, J_14)=select(a_41, J_14) | i1=J_14))). % 5.18/2.25 tff(c_1470, plain, (![J_14]: (select(a_49, J_14)=select(a_45, J_14) | i1=J_14))). % 5.18/2.25 tff(c_1449, plain, (![J_5]: (select(a_51, J_5)=select(a_47, J_5) | i1=J_5))). % 5.18/2.25 tff(c_663, plain, (![J_14]: (select(a_39, J_14)=select(a_35, J_14) | i1=J_14))). % 5.18/2.25 tff(c_1404, plain, (![J_5]: (select(a_53, J_5)=select(a_49, J_5) | i1=J_5))). % 5.18/2.25 tff(c_1142, plain, (store(a_35, i1, e_28)=a_39)). % 5.18/2.25 tff(c_1144, plain, (store(a_29, i1, e_28)=a_33)). % 5.18/2.25 tff(c_1138, plain, (store(a_37, i1, e_28)=a_41)). % 5.18/2.25 tff(c_1357, plain, (store(a_51, i1, e_28)=a_53)). % 5.18/2.25 tff(c_1345, plain, (store(a_47, i1, e_28)=a_51)). % 5.18/2.25 tff(c_1333, plain, (store(a_45, i1, e_28)=a_49)). % 5.18/2.25 tff(c_1321, plain, (store(a_49, i1, e_28)=a_53)). % 5.18/2.25 tff(c_1309, plain, (store(a_43, i1, e_28)=a_47)). % 5.18/2.25 tff(c_1148, plain, (store(a2, i1, e_28)=a_31)). % 5.18/2.25 tff(c_1145, plain, (select(a_33, i1)=e_28)). % 5.18/2.25 tff(c_1147, plain, (select(a_31, i1)=e_28)). % 5.18/2.25 tff(c_1249, plain, (![J_5]: (select(a_53, J_5)=select(a_51, J_5) | i1=J_5))). % 5.18/2.25 tff(c_1140, plain, (select(a_39, i1)=e_28)). % 5.18/2.25 tff(c_1139, plain, (select(a_41, i1)=e_28)). % 5.18/2.25 tff(c_1226, plain, (select(a_51, i1)=e_28)). % 5.18/2.25 tff(c_1221, plain, (select(a_49, i1)=e_28)). % 5.18/2.25 tff(c_1206, plain, (select(a_47, i1)=e_28)). % 5.18/2.25 tff(c_1149, plain, (select(a1, i1)=e_28)). % 5.18/2.25 tff(c_1197, plain, (select(a_53, i1)=e_28)). % 5.18/2.25 tff(c_1192, plain, (select(a_45, i1)=e_28)). % 5.18/2.25 tff(c_1146, plain, (e_32=e_28)). % 5.18/2.25 tff(c_1170, plain, (![J_14]: (select(a_43, J_14)=select(a_39, J_14) | i1=J_14))). % 5.18/2.25 tff(c_1143, plain, (e_38=e_28)). % 5.18/2.25 tff(c_1141, plain, (e_40=e_28)). % 5.18/2.25 tff(c_1095, plain, (e_54=e_28)). % 5.18/2.25 tff(c_1099, plain, (e_48=e_28)). % 5.18/2.25 tff(c_1137, plain, (e_30=e_28)). % 5.18/2.25 tff(c_1126, plain, (store(a_41, i1, e_28)=a_45)). % 5.18/2.25 tff(c_1096, plain, (e_52=e_28)). % 5.18/2.25 tff(c_1097, plain, (e_50=e_28)). % 5.18/2.25 tff(c_1098, plain, (e_46=e_28)). % 5.18/2.25 tff(c_1104, plain, (![J_14]: (select(a_47, J_14)=select(a_43, J_14) | i1=J_14))). % 5.18/2.25 tff(c_1082, plain, (e_44=e_28)). % 5.18/2.25 tff(c_1073, plain, (i7=i1)). % 5.18/2.25 tff(c_1076, plain, (i6=i1)). % 5.18/2.25 tff(c_1062, plain, (i5=i1)). % 5.18/2.25 tff(c_1036, plain, (![J_14]: (select(a_41, J_14)=select(a_37, J_14) | i1=J_14))). % 5.18/2.25 tff(c_293, plain, (![J_14]: (select(a_31, J_14)=select(a2, J_14) | i1=J_14))). % 5.18/2.25 tff(c_897, plain, (![J_14]: (select(a_33, J_14)=select(a_29, J_14) | i1=J_14))). % 5.18/2.25 tff(c_788, plain, (store(a_39, i1, e_28)=a_43)). % 5.18/2.25 tff(c_775, plain, (store(a_33, i1, e_28)=a_37)). % 5.18/2.25 tff(c_749, plain, (![J_14]: (select(a_37, J_14)=select(a_33, J_14) | i1=J_14))). % 5.18/2.25 tff(c_744, plain, (select(a_43, i1)=e_28)). % 5.18/2.25 tff(c_734, plain, (select(a_37, i1)=e_28)). % 5.18/2.25 tff(c_710, plain, (e_42=e_28)). % 5.18/2.25 tff(c_670, plain, (e_36=e_28)). % 5.18/2.25 tff(c_662, plain, (i4=i1)). % 5.18/2.25 tff(c_657, plain, (i3=i1)). % 5.18/2.25 tff(c_582, plain, (![J_14]: (select(a_35, J_14)=select(a_31, J_14) | i1=J_14))). % 5.18/2.25 tff(c_458, plain, (store(a_31, i1, e_28)=a_35)). % 5.18/2.25 tff(c_411, plain, (select(a_35, i1)=e_28)). % 5.18/2.25 tff(c_397, plain, (e_34=e_28)). % 5.18/2.25 tff(c_390, plain, (i2=i1)). % 5.18/2.25 tff(c_296, plain, (![J_14]: (select(a_29, J_14)=select(a1, J_14) | i1=J_14))). % 5.18/2.25 tff(c_218, plain, (select(a_29, i1)=e_28)). % 5.18/2.25 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))). % 5.18/2.25 tff(c_2, plain, (![A_1, I_2, E_3]: (select(store(A_1, I_2, E_3), I_2)=E_3))). % 5.18/2.25 tff(c_6, plain, (store(a1, i1, e_28)=a_29)). % 5.18/2.25 tff(c_34, plain, (select(a2, i1)=e_28)). % 5.18/2.25 tff(c_62, plain, (a_55=a_53)). % 5.18/2.25 tff(c_64, plain, (a2!=a1)). % 5.18/2.25 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 5.18/2.25 %------------------------------------------------------------------------------