%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SWV552-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 : n003.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 6.01s 2.67s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.08 % Problem : SWV552-1.007 : TPTP v9.0.0. Released v4.0.0. % 0.00/0.09 % 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.07/0.28 % Computer : n003.cluster.edu % 0.07/0.28 % Model : x86_64 x86_64 % 0.07/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.28 % Memory : 8042.1875MB % 0.07/0.28 % OS : Linux 3.10.0-693.el7.x86_64 % 0.07/0.28 % CPULimit : 300 % 0.13/0.28 % WCLimit : 300 % 0.13/0.28 % DateTime : Wed Apr 9 04:01:18 EDT 2025 % 0.13/0.29 % CPUTime : % 5.60/2.66 % 6.01/2.67 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 6.01/2.67 % 6.01/2.67 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 6.01/2.68 %$ 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 % 6.01/2.68 % 6.01/2.68 %Foreground sorts: % 6.01/2.68 % 6.01/2.68 % 6.01/2.68 %Background operators: % 6.01/2.68 % 6.01/2.68 % 6.01/2.68 %Foreground operators: % 6.01/2.68 tff(e_48, type, e_48: $i). % 6.01/2.68 tff(a1, type, a1: $i). % 6.01/2.68 tff(a_31, type, a_31: $i). % 6.01/2.68 tff(e_46, type, e_46: $i). % 6.01/2.68 tff(a_55, type, a_55: $i). % 6.01/2.68 tff(e_34, type, e_34: $i). % 6.01/2.68 tff(e_28, type, e_28: $i). % 6.01/2.68 tff(a_53, type, a_53: $i). % 6.01/2.68 tff(a_49, type, a_49: $i). % 6.01/2.68 tff(a_41, type, a_41: $i). % 6.01/2.68 tff(store, type, store: ($i * $i * $i) > $i). % 6.01/2.68 tff(a_43, type, a_43: $i). % 6.01/2.68 tff(e_50, type, e_50: $i). % 6.01/2.68 tff(a_29, type, a_29: $i). % 6.01/2.68 tff(a_35, type, a_35: $i). % 6.01/2.68 tff(a_37, type, a_37: $i). % 6.01/2.68 tff(e_40, type, e_40: $i). % 6.01/2.68 tff(a_33, type, a_33: $i). % 6.01/2.68 tff(a2, type, a2: $i). % 6.01/2.68 tff(i7, type, i7: $i). % 6.01/2.68 tff(e_42, type, e_42: $i). % 6.01/2.68 tff(e_52, type, e_52: $i). % 6.01/2.68 tff(e_32, type, e_32: $i). % 6.01/2.68 tff(i1, type, i1: $i). % 6.01/2.68 tff(e_30, type, e_30: $i). % 6.01/2.68 tff(i2, type, i2: $i). % 6.01/2.68 tff(a_39, type, a_39: $i). % 6.01/2.68 tff(select, type, select: ($i * $i) > $i). % 6.01/2.68 tff(e_44, type, e_44: $i). % 6.01/2.68 tff(e_54, type, e_54: $i). % 6.01/2.68 tff(a_45, type, a_45: $i). % 6.01/2.68 tff(a_47, type, a_47: $i). % 6.01/2.68 tff(e_38, type, e_38: $i). % 6.01/2.68 tff(a_51, type, a_51: $i). % 6.01/2.68 tff(i5, type, i5: $i). % 6.01/2.68 tff(i4, type, i4: $i). % 6.01/2.68 tff(i3, type, i3: $i). % 6.01/2.68 tff(e_36, type, e_36: $i). % 6.01/2.68 tff(i6, type, i6: $i). % 6.01/2.68 % 6.01/2.68 %Saturated clause set: % 6.01/2.68 tff(c_1595, plain, (![J_43]: (select(a2, J_43)=select(a1, J_43) | i1=J_43 | i1=J_43 | i1=J_43 | i1=J_43 | i1=J_43 | i1=J_43 | i1=J_43 | i1=J_43 | i1=J_43 | i1=J_43 | i1=J_43 | i1=J_43 | i1=J_43 | i1=J_43))). % 6.01/2.68 tff(c_1582, 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))). % 6.01/2.68 tff(c_1548, plain, (![J_41]: (select(a_31, J_41)=select(a_29, J_41) | i1=J_41 | i1=J_41 | i1=J_41 | i1=J_41 | i1=J_41 | i1=J_41 | i1=J_41 | i1=J_41 | i1=J_41 | i1=J_41 | i1=J_41 | i1=J_41))). % 6.01/2.68 tff(c_1529, plain, (![J_14]: (select(a_33, J_14)=select(a_31, 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))). % 6.01/2.68 tff(c_1504, 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))). % 6.01/2.68 tff(c_1473, plain, (![J_38]: (select(a_37, J_38)=select(a_35, J_38) | i1=J_38 | i1=J_38 | i1=J_38 | i1=J_38 | i1=J_38 | i1=J_38 | i1=J_38 | i1=J_38 | i1=J_38))). % 6.01/2.69 tff(c_1454, 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))). % 6.01/2.69 tff(c_1420, plain, (![J_36]: (select(a_41, J_36)=select(a_39, J_36) | i1=J_36 | i1=J_36 | i1=J_36 | i1=J_36 | i1=J_36 | i1=J_36 | i1=J_36))). % 6.01/2.69 tff(c_1404, plain, (![J_14]: (select(a_43, J_14)=select(a_41, J_14) | i1=J_14 | i1=J_14 | i1=J_14 | i1=J_14 | i1=J_14 | i1=J_14))). % 6.01/2.69 tff(c_1382, 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))). % 6.01/2.69 tff(c_1345, plain, (![J_33]: (select(a_47, J_33)=select(a_45, J_33) | i1=J_33 | i1=J_33 | i1=J_33 | i1=J_33))). % 6.01/2.69 tff(c_1310, plain, (![J_14]: (select(a_49, J_14)=select(a_47, J_14) | i1=J_14 | i1=J_14 | i1=J_14))). % 6.01/2.69 tff(c_845, plain, (![J_14]: (select(a_49, J_14)=select(a_45, J_14) | i1=J_14))). % 6.01/2.69 tff(c_1267, plain, (![J_14]: (select(a_51, J_14)=select(a_49, J_14) | i1=J_14 | i1=J_14))). % 6.01/2.69 tff(c_730, plain, (![J_14]: (select(a_41, J_14)=select(a_37, J_14) | i1=J_14))). % 6.01/2.69 tff(c_468, plain, (![J_14]: (select(a_53, J_14)=select(a_51, J_14) | i1=J_14))). % 6.01/2.69 tff(c_1229, plain, (![J_14]: (select(a_45, J_14)=select(a_41, J_14) | i1=J_14))). % 6.01/2.69 tff(c_1209, plain, (![J_14]: (select(a_51, J_14)=select(a_47, J_14) | i1=J_14))). % 6.01/2.69 tff(c_1189, plain, (![J_14]: (select(a_35, J_14)=select(a_31, J_14) | i1=J_14))). % 6.01/2.69 tff(c_884, plain, (store(a_51, i1, e_28)=a_53)). % 6.01/2.69 tff(c_957, plain, (store(a_37, i1, e_28)=a_41)). % 6.01/2.69 tff(c_888, plain, (store(a_49, i1, e_28)=a_53)). % 6.01/2.69 tff(c_967, plain, (store(a2, i1, e_28)=a_31)). % 6.01/2.69 tff(c_960, plain, (store(a_35, i1, e_28)=a_39)). % 6.13/2.69 tff(c_963, plain, (store(a_29, i1, e_28)=a_33)). % 6.13/2.69 tff(c_1110, plain, (store(a_41, i1, e_28)=a_45)). % 6.13/2.69 tff(c_1090, plain, (![J_14]: (select(a_43, J_14)=select(a_39, J_14) | i1=J_14))). % 6.13/2.69 tff(c_1078, plain, (store(a_43, i1, e_28)=a_47)). % 6.13/2.69 tff(c_961, plain, (select(a_39, i1)=e_28)). % 6.13/2.69 tff(c_956, plain, (select(a_41, i1)=e_28)). % 6.13/2.69 tff(c_966, plain, (select(a_31, i1)=e_28)). % 6.13/2.69 tff(c_964, plain, (select(a_33, i1)=e_28)). % 6.13/2.69 tff(c_1020, plain, (store(a_45, i1, e_28)=a_49)). % 6.13/2.69 tff(c_968, plain, (select(a1, i1)=e_28)). % 6.13/2.69 tff(c_955, plain, (select(a_47, i1)=e_28)). % 6.13/2.69 tff(c_958, plain, (e_46=e_28)). % 6.13/2.69 tff(c_290, plain, (![J_14]: (select(a_31, J_14)=select(a2, J_14) | i1=J_14))). % 6.13/2.69 tff(c_965, plain, (e_32=e_28)). % 6.13/2.69 tff(c_962, plain, (e_38=e_28)). % 6.13/2.69 tff(c_959, plain, (e_40=e_28)). % 6.13/2.69 tff(c_954, plain, (e_48=e_28)). % 6.13/2.69 tff(c_937, plain, (e_30=e_28)). % 6.13/2.70 tff(c_942, plain, (store(a_47, i1, e_28)=a_51)). % 6.13/2.70 tff(c_885, plain, (select(a_49, i1)=e_28)). % 6.13/2.70 tff(c_887, plain, (select(a_53, i1)=e_28)). % 6.13/2.70 tff(c_902, plain, (![J_14]: (select(a_47, J_14)=select(a_43, J_14) | i1=J_14))). % 6.13/2.70 tff(c_886, plain, (e_54=e_28)). % 6.13/2.70 tff(c_879, plain, (e_52=e_28)). % 6.13/2.70 tff(c_878, plain, (select(a_51, i1)=e_28)). % 6.13/2.70 tff(c_853, plain, (e_50=e_28)). % 6.13/2.70 tff(c_862, plain, (store(a_39, i1, e_28)=a_43)). % 6.13/2.70 tff(c_844, plain, (i6=i1)). % 6.13/2.70 tff(c_806, plain, (select(a_45, i1)=e_28)). % 6.13/2.70 tff(c_801, plain, (select(a_43, i1)=e_28)). % 6.13/2.70 tff(c_772, plain, (e_44=e_28)). % 6.13/2.70 tff(c_738, plain, (e_42=e_28)). % 6.13/2.70 tff(c_752, plain, (![J_14]: (select(a_39, J_14)=select(a_35, J_14) | i1=J_14))). % 6.13/2.70 tff(c_729, plain, (i5=i1)). % 6.13/2.70 tff(c_724, plain, (i4=i1)). % 6.13/2.70 tff(c_698, plain, (![J_14]: (select(a_37, J_14)=select(a_33, J_14) | i1=J_14))). % 6.13/2.70 tff(c_266, plain, (![J_14]: (select(a_53, J_14)=select(a_49, J_14) | i1=J_14))). % 6.13/2.70 tff(c_598, plain, (store(a_33, i1, e_28)=a_37)). % 6.13/2.70 tff(c_567, plain, (select(a_37, i1)=e_28)). % 6.13/2.70 tff(c_537, plain, (e_36=e_28)). % 6.13/2.70 tff(c_530, plain, (i3=i1)). % 6.13/2.70 tff(c_503, plain, (![J_14]: (select(a_33, J_14)=select(a_29, J_14) | i1=J_14))). % 6.13/2.70 tff(c_466, plain, (i7=i1)). % 6.13/2.70 tff(c_443, plain, (store(a_31, i1, e_28)=a_35)). % 6.13/2.70 tff(c_412, plain, (select(a_35, i1)=e_28)). % 6.13/2.70 tff(c_382, plain, (e_34=e_28)). % 6.13/2.70 tff(c_375, plain, (i2=i1)). % 6.13/2.70 tff(c_293, plain, (![J_14]: (select(a_29, J_14)=select(a1, J_14) | i1=J_14))). % 6.13/2.70 tff(c_218, plain, (select(a_29, i1)=e_28)). % 6.13/2.70 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))). % 6.13/2.70 tff(c_2, plain, (![A_1, I_2, E_3]: (select(store(A_1, I_2, E_3), I_2)=E_3))). % 6.13/2.70 tff(c_6, plain, (store(a1, i1, e_28)=a_29)). % 6.13/2.70 tff(c_34, plain, (select(a2, i1)=e_28)). % 6.13/2.70 tff(c_62, plain, (a_55=a_53)). % 6.13/2.70 tff(c_64, plain, (a2!=a1)). % 6.13/2.70 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 6.13/2.70 %------------------------------------------------------------------------------