%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SWV556-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 : n027.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 48.14s 32.79s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.02/0.12 % Problem : SWV556-1.007 : TPTP v9.0.0. Released v4.0.0. % 0.02/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 : n027.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:02:35 EDT 2025 % 0.12/0.34 % CPUTime : % 48.14/32.79 % 48.14/32.79 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 48.14/32.79 % 48.14/32.79 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 48.17/32.81 %$ store > sk > select > #nlpp > i_59 > i7 > i6 > i5 > i4 > i3 > i2 > i1 > e_61 > e_60 > e_57 > e_55 > e_53 > e_51 > e_49 > e_47 > e_45 > e_43 > e_41 > e_39 > e_37 > e_35 > e_33 > e_31 > a_58 > a_56 > a_54 > a_52 > a_50 > a_48 > a_46 > a_44 > a_42 > a_40 > a_38 > a_36 > a_34 > a_32 > a2 > a1 % 48.17/32.81 % 48.17/32.81 %Foreground sorts: % 48.17/32.81 % 48.17/32.81 % 48.17/32.81 %Background operators: % 48.17/32.81 % 48.17/32.81 % 48.17/32.81 %Foreground operators: % 48.17/32.81 tff(a1, type, a1: $i). % 48.17/32.81 tff(a_54, type, a_54: $i). % 48.17/32.81 tff(a_56, type, a_56: $i). % 48.17/32.81 tff(a_52, type, a_52: $i). % 48.17/32.81 tff(a_46, type, a_46: $i). % 48.17/32.81 tff(a_38, type, a_38: $i). % 48.17/32.81 tff(e_33, type, e_33: $i). % 48.17/32.81 tff(a_34, type, a_34: $i). % 48.17/32.81 tff(store, type, store: ($i * $i * $i) > $i). % 48.17/32.81 tff(e_60, type, e_60: $i). % 48.17/32.81 tff(e_53, type, e_53: $i). % 48.17/32.81 tff(e_43, type, e_43: $i). % 48.17/32.81 tff(a_40, type, a_40: $i). % 48.17/32.81 tff(e_45, type, e_45: $i). % 48.17/32.81 tff(e_35, type, e_35: $i). % 48.17/32.81 tff(e_61, type, e_61: $i). % 48.17/32.81 tff(a_50, type, a_50: $i). % 48.17/32.81 tff(e_55, type, e_55: $i). % 48.17/32.81 tff(e_57, type, e_57: $i). % 48.17/32.81 tff(a_36, type, a_36: $i). % 48.17/32.81 tff(a2, type, a2: $i). % 48.17/32.81 tff(i_59, type, i_59: $i). % 48.17/32.81 tff(sk, type, sk: ($i * $i) > $i). % 48.17/32.81 tff(a_32, type, a_32: $i). % 48.17/32.81 tff(e_39, type, e_39: $i). % 48.17/32.81 tff(a_42, type, a_42: $i). % 48.17/32.81 tff(i7, type, i7: $i). % 48.17/32.81 tff(i1, type, i1: $i). % 48.17/32.81 tff(i2, type, i2: $i). % 48.17/32.81 tff(e_37, type, e_37: $i). % 48.17/32.81 tff(select, type, select: ($i * $i) > $i). % 48.17/32.81 tff(e_51, type, e_51: $i). % 48.17/32.81 tff(e_49, type, e_49: $i). % 48.17/32.81 tff(a_44, type, a_44: $i). % 48.17/32.81 tff(a_48, type, a_48: $i). % 48.17/32.81 tff(e_31, type, e_31: $i). % 48.17/32.81 tff(i5, type, i5: $i). % 48.17/32.81 tff(i4, type, i4: $i). % 48.17/32.81 tff(a_58, type, a_58: $i). % 48.17/32.81 tff(i3, type, i3: $i). % 48.17/32.81 tff(e_47, type, e_47: $i). % 48.17/32.81 tff(e_41, type, e_41: $i). % 48.17/32.81 tff(i6, type, i6: $i). % 48.17/32.81 % 48.17/32.81 %Saturated clause set: % 48.17/32.81 tff(c_317816, plain, (sk(a1, a2)=i1)). % 48.17/32.81 tff(c_317834, plain, (e_33!=e_31)). % 48.17/32.81 tff(c_317820, plain, (e_61=e_31)). % 48.17/32.81 tff(c_317819, plain, (e_60=e_33)). % 48.17/32.81 tff(c_317815, plain, (i_59=i1)). % 48.17/32.81 tff(c_317751, plain, (![J_14]: (select(a2, J_14)=select(a1, J_14) | i3=J_14 | i3=J_14 | i1=J_14 | i3=J_14 | i3=J_14 | i3=J_14 | i3=J_14 | i3=J_14 | i3=J_14 | i3=J_14 | i1=J_14 | i1=J_14 | i1=J_14 | i1=J_14))). % 48.17/32.81 tff(c_317715, plain, (![J_14]: (select(a_32, J_14)=select(a2, J_14) | i3=J_14 | i3=J_14 | i1=J_14 | i3=J_14 | i3=J_14 | i3=J_14 | i3=J_14 | i3=J_14 | i3=J_14 | i3=J_14 | i1=J_14 | i1=J_14 | i1=J_14))). % 48.17/32.81 tff(c_317673, plain, (![J_14]: (select(a_34, J_14)=select(a_32, J_14) | i3=J_14 | i3=J_14 | i1=J_14 | i3=J_14 | i3=J_14 | i3=J_14 | i3=J_14 | i3=J_14 | i3=J_14 | i3=J_14 | i1=J_14 | i1=J_14))). % 48.17/32.81 tff(c_317637, plain, (![J_14]: (select(a_36, J_14)=select(a_34, J_14) | i3=J_14 | i3=J_14 | i1=J_14 | i3=J_14 | i3=J_14 | i3=J_14 | i3=J_14 | i3=J_14 | i3=J_14 | i3=J_14 | i1=J_14))). % 48.17/32.81 tff(c_317607, plain, (![J_14]: (select(a_38, J_14)=select(a_36, J_14) | i3=J_14 | i3=J_14 | i1=J_14 | i3=J_14 | i3=J_14 | i3=J_14 | i3=J_14 | i3=J_14 | i3=J_14 | i3=J_14))). % 48.17/32.81 tff(c_317573, plain, (![J_14]: (select(a_40, J_14)=select(a_38, J_14) | i3=J_14 | i3=J_14 | i1=J_14 | i3=J_14 | i3=J_14 | i3=J_14 | i3=J_14 | i3=J_14 | i3=J_14))). % 48.17/32.82 tff(c_317540, plain, (![J_14]: (select(a_42, J_14)=select(a_40, J_14) | i3=J_14 | i3=J_14 | i1=J_14 | i3=J_14 | i3=J_14 | i3=J_14 | i3=J_14 | i3=J_14))). % 48.17/32.82 tff(c_317512, plain, (![J_14]: (select(a_44, J_14)=select(a_42, J_14) | i3=J_14 | i3=J_14 | i1=J_14 | i3=J_14 | i3=J_14 | i3=J_14 | i3=J_14))). % 48.17/32.82 tff(c_317479, plain, (![J_14]: (select(a_46, J_14)=select(a_44, J_14) | i3=J_14 | i3=J_14 | i1=J_14 | i3=J_14 | i3=J_14 | i3=J_14))). % 48.17/32.82 tff(c_317442, plain, (![J_14]: (select(a_48, J_14)=select(a_46, J_14) | i3=J_14 | i3=J_14 | i1=J_14 | i3=J_14 | i3=J_14))). % 48.17/32.82 tff(c_317412, plain, (![J_14]: (select(a_50, J_14)=select(a_48, J_14) | i3=J_14 | i3=J_14 | i1=J_14 | i3=J_14))). % 48.25/32.82 tff(c_317380, plain, (![J_3985]: (select(a_52, J_3985)=select(a_50, J_3985) | i3=J_3985 | i3=J_3985 | i1=J_3985))). % 48.25/32.82 tff(c_316731, plain, (![J_5]: (select(a_54, J_5)=select(a_50, J_5) | i3=J_5))). % 48.25/32.82 tff(c_316711, plain, (![J_14]: (select(a_52, J_14)=select(a_48, J_14) | i3=J_14))). % 48.25/32.82 tff(c_316623, plain, (![J_14]: (select(a_50, J_14)=select(a_46, J_14) | i3=J_14))). % 48.25/32.82 tff(c_317012, plain, (store(a_50, i3, e_31)=a_54)). % 48.25/32.82 tff(c_317022, plain, (store(a_42, i3, e_31)=a_46)). % 48.25/32.82 tff(c_317009, plain, (store(a_52, i1, e_31)=a_56)). % 48.25/32.82 tff(c_317019, plain, (store(a_44, i3, e_31)=a_48)). % 48.25/32.82 tff(c_317234, plain, (![J_3985]: (select(a_54, J_3985)=select(a_52, J_3985) | i3=J_3985 | i1=J_3985))). % 48.25/32.82 tff(c_317013, plain, (select(a_50, i1)=e_31)). % 48.25/32.82 tff(c_317020, plain, (select(a_48, i3)=e_31)). % 48.25/32.82 tff(c_317014, plain, (select(a_56, i1)=e_31)). % 48.25/32.82 tff(c_317026, plain, (store(a_36, i3, e_31)=a_40)). % 48.25/32.82 tff(c_317015, plain, (select(a_54, i1)=e_31)). % 48.25/32.82 tff(c_317008, plain, (select(a_46, i1)=e_31)). % 48.25/32.82 tff(c_317011, plain, (select(a_34, i3)=e_31)). % 48.25/32.82 tff(c_317123, plain, (![J_14]: (select(a_56, J_14)=select(a_54, J_14) | i3=J_14))). % 48.25/32.82 tff(c_317010, plain, (select(a2, i3)=e_31)). % 48.25/32.82 tff(c_317016, plain, (select(a_54, i3)=e_31)). % 48.25/32.82 tff(c_317025, plain, (select(a_40, i3)=e_31)). % 48.25/32.82 tff(c_317023, plain, (select(a_46, i3)=e_31)). % 48.25/32.82 tff(c_317027, plain, (select(a_38, i3)=e_31)). % 48.25/32.82 tff(c_317059, plain, (select(a_42, i1)=e_31)). % 48.25/32.82 tff(c_317024, plain, (e_45=e_31)). % 48.25/32.82 tff(c_317021, plain, (e_47=e_31)). % 48.25/32.82 tff(c_317041, plain, (![J_14]: (select(a_48, J_14)=select(a_44, J_14) | i3=J_14))). % 48.25/32.82 tff(c_317018, plain, (e_53=e_31)). % 48.25/32.82 tff(c_317017, plain, (e_55=e_31)). % 48.25/32.82 tff(c_317003, plain, (e_39=e_31)). % 48.25/32.82 tff(c_316965, plain, (![J_14]: (select(a_46, J_14)=select(a_42, J_14) | i3=J_14))). % 48.25/32.82 tff(c_316947, plain, (select(a1, i3)=e_41)). % 48.25/32.82 tff(c_275, plain, (![J_14]: (select(a_32, J_14)=select(a1, J_14) | i1=J_14))). % 48.25/32.82 tff(c_316919, plain, (select(a_32, i3)=e_41)). % 48.25/32.82 tff(c_316861, plain, (![J_14]: (select(a_38, J_14)=select(a_34, J_14) | i1=J_14))). % 48.25/32.82 tff(c_316838, plain, (store(a_54, i3, e_41)=a_56)). % 48.25/32.82 tff(c_316826, plain, (store(a_48, i3, e_41)=a_52)). % 48.25/32.83 tff(c_316790, plain, (select(a_56, i3)=e_41)). % 48.25/32.83 tff(c_316785, plain, (select(a_52, i3)=e_41)). % 48.25/32.83 tff(c_290, plain, (![J_14]: (select(a_42, J_14)=select(a_38, J_14) | i3=J_14))). % 48.25/32.83 tff(c_316738, plain, (e_57=e_41)). % 48.25/32.83 tff(c_316718, plain, (e_51=e_41)). % 48.25/32.83 tff(c_316710, plain, (i7=i3)). % 48.25/32.83 tff(c_316709, plain, (i3!=i1)). % 48.25/32.83 tff(c_316679, plain, (i6=i3)). % 48.25/32.83 tff(c_316680, plain, (![J_14]: (select(a_36, J_14)=select(a_32, J_14) | i1=J_14))). % 48.25/32.83 tff(c_316655, plain, (select(a_50, i3)=e_41)). % 48.25/32.83 tff(c_316644, plain, (store(a_46, i3, e_41)=a_50)). % 48.25/32.83 tff(c_316631, plain, (e_49=e_41)). % 48.25/32.83 tff(c_316591, plain, (i5=i3)). % 48.25/32.83 tff(c_316565, plain, (![J_14]: (select(a_44, J_14)=select(a_40, J_14) | i3=J_14))). % 48.25/32.83 tff(c_316539, plain, (store(a_40, i3, e_41)=a_44)). % 48.25/32.83 tff(c_316530, plain, (select(a_44, i3)=e_41)). % 48.25/32.83 tff(c_316485, plain, (e_43=e_41)). % 48.25/32.83 tff(c_316477, plain, (i4=i3)). % 48.25/32.83 tff(c_296, plain, (![J_14]: (select(a_40, J_14)=select(a_36, J_14) | i3=J_14))). % 48.25/32.83 tff(c_316361, plain, (store(a_32, i1, e_33)=a_36)). % 48.25/32.83 tff(c_316349, plain, (store(a_34, i1, e_31)=a_38)). % 48.25/32.83 tff(c_316344, plain, (select(a_36, i1)=e_33)). % 48.25/32.83 tff(c_316314, plain, (select(a_38, i1)=e_31)). % 48.25/32.83 tff(c_316300, plain, (e_37=e_31)). % 48.25/32.83 tff(c_316299, plain, (e_35=e_33)). % 48.25/32.83 tff(c_316291, plain, (i2=i1)). % 48.25/32.83 tff(c_302, plain, (![J_14]: (select(a_34, J_14)=select(a2, J_14) | i1=J_14))). % 48.25/32.83 tff(c_308, plain, (![J_14]: (select(a_56, J_14)=select(a_52, J_14) | i1=J_14))). % 48.25/32.83 tff(c_239, plain, (select(a_34, i1)=e_33)). % 48.25/32.83 tff(c_227, plain, (select(a_42, i3)=e_41)). % 48.25/32.83 tff(c_212, plain, (select(a_32, i1)=e_31)). % 48.25/32.83 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))). % 48.25/32.83 tff(c_2, plain, (![A_1, I_2, E_3]: (select(store(A_1, I_2, E_3), I_2)=E_3))). % 48.25/32.83 tff(c_6, plain, (store(a1, i1, e_31)=a_32)). % 48.25/32.83 tff(c_16, plain, (store(a_38, i3, e_41)=a_42)). % 48.25/32.83 tff(c_8, plain, (store(a2, i1, e_33)=a_34)). % 48.25/32.83 tff(c_36, plain, (select(a1, i1)=e_33)). % 48.25/32.83 tff(c_34, plain, (select(a2, i1)=e_31)). % 48.25/32.83 tff(c_44, plain, (select(a_36, i3)=e_41)). % 48.25/32.83 tff(c_68, plain, (a_58=a_56)). % 48.25/32.83 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 48.25/32.83 %------------------------------------------------------------------------------