%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SWV552-1.010 : 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 : n020.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:12 PM UTC 2025 % Result : Satisfiable 6.61s 2.46s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.10 % Problem : SWV552-1.010 : TPTP v9.0.0. Released v4.0.0. % 0.11/0.11 % 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.11/0.32 % Computer : n020.cluster.edu % 0.11/0.32 % Model : x86_64 x86_64 % 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.32 % Memory : 8042.1875MB % 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.32 % CPULimit : 300 % 0.11/0.32 % WCLimit : 300 % 0.11/0.32 % DateTime : Wed Apr 9 04:01:19 EDT 2025 % 0.11/0.32 % CPUTime : % 6.61/2.45 % 6.61/2.46 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 6.61/2.46 % 6.61/2.46 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 6.61/2.47 %$ store > select > #nlpp > i9 > i8 > i7 > i6 > i5 > i4 > i3 > i2 > i10 > i1 > e_78 > e_76 > e_74 > e_72 > e_70 > e_68 > e_66 > e_64 > e_62 > e_60 > e_58 > e_56 > e_54 > e_52 > e_50 > e_48 > e_46 > e_44 > e_42 > e_40 > a_79 > a_77 > a_75 > a_73 > a_71 > a_69 > a_67 > a_65 > a_63 > a_61 > a_59 > a_57 > a_55 > a_53 > a_51 > a_49 > a_47 > a_45 > a_43 > a_41 > a2 > a1 % 6.61/2.47 % 6.61/2.47 %Foreground sorts: % 6.61/2.47 % 6.61/2.47 % 6.61/2.47 %Background operators: % 6.61/2.47 % 6.61/2.47 % 6.61/2.47 %Foreground operators: % 6.61/2.47 tff(e_48, type, e_48: $i). % 6.61/2.47 tff(a1, type, a1: $i). % 6.61/2.47 tff(a_65, type, a_65: $i). % 6.61/2.47 tff(a_73, type, a_73: $i). % 6.61/2.47 tff(e_46, type, e_46: $i). % 6.61/2.47 tff(a_55, type, a_55: $i). % 6.61/2.47 tff(a_77, type, a_77: $i). % 6.61/2.47 tff(e_74, type, e_74: $i). % 6.61/2.47 tff(a_53, type, a_53: $i). % 6.61/2.47 tff(a_49, type, a_49: $i). % 6.61/2.47 tff(a_41, type, a_41: $i). % 6.61/2.47 tff(store, type, store: ($i * $i * $i) > $i). % 6.61/2.47 tff(a_59, type, a_59: $i). % 6.61/2.47 tff(a_67, type, a_67: $i). % 6.61/2.47 tff(a_43, type, a_43: $i). % 6.61/2.47 tff(e_60, type, e_60: $i). % 6.61/2.47 tff(e_56, type, e_56: $i). % 6.61/2.47 tff(e_70, type, e_70: $i). % 6.61/2.47 tff(e_50, type, e_50: $i). % 6.61/2.47 tff(a_79, type, a_79: $i). % 6.61/2.47 tff(a_71, type, a_71: $i). % 6.61/2.47 tff(e_66, type, e_66: $i). % 6.61/2.47 tff(e_68, type, e_68: $i). % 6.61/2.47 tff(i10, type, i10: $i). % 6.61/2.47 tff(e_40, type, e_40: $i). % 6.61/2.47 tff(a2, type, a2: $i). % 6.61/2.47 tff(i8, type, i8: $i). % 6.61/2.47 tff(i9, type, i9: $i). % 6.61/2.47 tff(a_57, type, a_57: $i). % 6.61/2.47 tff(i7, type, i7: $i). % 6.61/2.47 tff(e_42, type, e_42: $i). % 6.61/2.47 tff(e_52, type, e_52: $i). % 6.61/2.47 tff(i1, type, i1: $i). % 6.61/2.47 tff(i2, type, i2: $i). % 6.61/2.47 tff(a_63, type, a_63: $i). % 6.61/2.47 tff(select, type, select: ($i * $i) > $i). % 6.61/2.47 tff(e_78, type, e_78: $i). % 6.61/2.47 tff(e_44, type, e_44: $i). % 6.61/2.47 tff(e_54, type, e_54: $i). % 6.61/2.47 tff(a_69, type, a_69: $i). % 6.61/2.47 tff(a_75, type, a_75: $i). % 6.61/2.47 tff(a_45, type, a_45: $i). % 6.61/2.47 tff(e_72, type, e_72: $i). % 6.61/2.47 tff(a_47, type, a_47: $i). % 6.61/2.47 tff(e_76, type, e_76: $i). % 6.61/2.47 tff(e_62, type, e_62: $i). % 6.61/2.47 tff(a_51, type, a_51: $i). % 6.61/2.47 tff(i5, type, i5: $i). % 6.61/2.47 tff(i4, type, i4: $i). % 6.61/2.47 tff(e_64, type, e_64: $i). % 6.61/2.47 tff(e_58, type, e_58: $i). % 6.61/2.47 tff(i3, type, i3: $i). % 6.61/2.47 tff(a_61, type, a_61: $i). % 6.61/2.47 tff(i6, type, i6: $i). % 6.61/2.47 % 6.61/2.47 %Saturated clause set: % 6.61/2.47 tff(c_2950, 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 | 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.61/2.47 tff(c_2928, plain, (![J_14]: (select(a_41, 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 | i1=J_14 | i1=J_14 | i1=J_14 | i1=J_14 | i1=J_14 | i1=J_14))). % 6.61/2.47 tff(c_2903, 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 | 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.61/2.47 tff(c_2875, 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 | 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.61/2.47 tff(c_2850, plain, (![J_14]: (select(a_47, J_14)=select(a_45, 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 | i1=J_14 | i1=J_14 | i1=J_14))). % 6.61/2.47 tff(c_2828, plain, (![J_14]: (select(a_49, J_14)=select(a_47, 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 | i1=J_14 | i1=J_14))). % 6.61/2.47 tff(c_2800, plain, (![J_14]: (select(a_51, J_14)=select(a_49, 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 | i1=J_14))). % 6.61/2.47 tff(c_2775, plain, (![J_14]: (select(a_53, J_14)=select(a_51, 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.61/2.48 tff(c_2753, plain, (![J_14]: (select(a_55, J_14)=select(a_53, 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.61/2.48 tff(c_2725, plain, (![J_5]: (select(a_57, J_5)=select(a_55, J_5) | i1=J_5 | i1=J_5 | i1=J_5 | i1=J_5 | i1=J_5 | i1=J_5 | i1=J_5 | i1=J_5 | i1=J_5 | i1=J_5 | i1=J_5))). % 6.61/2.48 tff(c_2700, plain, (![J_14]: (select(a_59, J_14)=select(a_57, 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.61/2.48 tff(c_2675, plain, (![J_14]: (select(a_61, J_14)=select(a_59, 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.61/2.48 tff(c_2653, plain, (![J_14]: (select(a_63, J_14)=select(a_61, 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.61/2.48 tff(c_2625, plain, (![J_14]: (select(a_65, J_14)=select(a_63, J_14) | i1=J_14 | i1=J_14 | i1=J_14 | i1=J_14 | i1=J_14 | i1=J_14 | i1=J_14))). % 6.61/2.48 tff(c_2600, plain, (![J_5]: (select(a_67, J_5)=select(a_65, J_5) | i1=J_5 | i1=J_5 | i1=J_5 | i1=J_5 | i1=J_5 | i1=J_5))). % 6.61/2.48 tff(c_2575, plain, (![J_5]: (select(a_69, J_5)=select(a_67, J_5) | i1=J_5 | i1=J_5 | i1=J_5 | i1=J_5 | i1=J_5))). % 6.61/2.48 tff(c_2553, plain, (![J_14]: (select(a_71, J_14)=select(a_69, J_14) | i1=J_14 | i1=J_14 | i1=J_14 | i1=J_14))). % 6.61/2.48 tff(c_2428, plain, (![J_43]: (select(a_73, J_43)=select(a_71, J_43) | i1=J_43 | i1=J_43 | i1=J_43))). % 6.61/2.48 tff(c_1583, plain, (![J_14]: (select(a_63, J_14)=select(a_59, J_14) | i1=J_14))). % 6.61/2.48 tff(c_1651, plain, (![J_14]: (select(a_53, J_14)=select(a_49, J_14) | i1=J_14))). % 6.61/2.48 tff(c_2469, plain, (![J_14]: (select(a_61, J_14)=select(a_57, J_14) | i1=J_14))). % 6.61/2.48 tff(c_2448, plain, (![J_5]: (select(a_71, J_5)=select(a_67, J_5) | i1=J_5))). % 6.61/2.48 tff(c_2421, plain, (![J_5]: (select(a_75, J_5)=select(a_71, J_5) | i1=J_5))). % 6.61/2.48 tff(c_1657, plain, (![J_14]: (select(a_55, J_14)=select(a_51, J_14) | i1=J_14))). % 6.61/2.48 tff(c_2381, plain, (![J_5]: (select(a_59, J_5)=select(a_55, J_5) | i1=J_5))). % 6.61/2.48 tff(c_2353, plain, (![J_5]: (select(a_77, J_5)=select(a_75, J_5) | i1=J_5))). % 6.61/2.48 tff(c_1913, plain, (store(a_49, i1, e_40)=a_53)). % 6.61/2.48 tff(c_1917, plain, (store(a_47, i1, e_40)=a_51)). % 6.61/2.48 tff(c_2303, plain, (![J_25]: (select(a_75, J_25)=select(a_73, J_25) | i1=J_25 | i1=J_25))). % 6.61/2.48 tff(c_1920, plain, (store(a_41, i1, e_40)=a_45)). % 6.61/2.48 tff(c_1814, plain, (store(a_73, i1, e_40)=a_77)). % 6.61/2.48 tff(c_2269, plain, (store(a_75, i1, e_40)=a_77)). % 6.61/2.48 tff(c_2257, plain, (store(a_69, i1, e_40)=a_73)). % 6.61/2.48 tff(c_2245, plain, (store(a_71, i1, e_40)=a_75)). % 6.61/2.48 tff(c_2225, plain, (![J_5]: (select(a_69, J_5)=select(a_65, J_5) | i1=J_5))). % 6.61/2.48 tff(c_2213, plain, (store(a_65, i1, e_40)=a_69)). % 6.61/2.48 tff(c_2201, plain, (store(a_67, i1, e_40)=a_71)). % 6.61/2.48 tff(c_2189, plain, (store(a_61, i1, e_40)=a_65)). % 6.61/2.48 tff(c_867, plain, (![J_14]: (select(a_47, J_14)=select(a_43, J_14) | i1=J_14))). % 6.61/2.48 tff(c_2158, plain, (store(a_63, i1, e_40)=a_67)). % 6.61/2.48 tff(c_2146, plain, (store(a_57, i1, e_40)=a_61)). % 6.61/2.48 tff(c_2134, plain, (store(a_53, i1, e_40)=a_57)). % 6.61/2.48 tff(c_2122, plain, (store(a_55, i1, e_40)=a_59)). % 6.61/2.48 tff(c_2110, plain, (store(a_59, i1, e_40)=a_63)). % 6.61/2.48 tff(c_1914, plain, (select(a_53, i1)=e_40)). % 6.61/2.48 tff(c_1815, plain, (select(a_77, i1)=e_40)). % 6.61/2.48 tff(c_2070, plain, (![J_14]: (select(a_67, J_14)=select(a_63, J_14) | i1=J_14))). % 6.61/2.48 tff(c_1808, plain, (select(a_63, i1)=e_40)). % 6.61/2.48 tff(c_1923, plain, (select(a_43, i1)=e_40)). % 6.61/2.48 tff(c_1912, plain, (select(a_59, i1)=e_40)). % 6.61/2.48 tff(c_1918, plain, (select(a_51, i1)=e_40)). % 6.61/2.48 tff(c_1921, plain, (select(a_45, i1)=e_40)). % 6.61/2.48 tff(c_1924, plain, (store(a2, i1, e_40)=a_43)). % 6.61/2.48 tff(c_1995, plain, (select(a_73, i1)=e_40)). % 6.61/2.48 tff(c_1990, plain, (select(a_75, i1)=e_40)). % 6.61/2.48 tff(c_1985, plain, (select(a_69, i1)=e_40)). % 6.61/2.48 tff(c_1975, plain, (![J_14]: (select(a_73, J_14)=select(a_69, J_14) | i1=J_14))). % 6.61/2.48 tff(c_1970, plain, (select(a_71, i1)=e_40)). % 6.61/2.48 tff(c_1965, plain, (select(a_67, i1)=e_40)). % 6.61/2.48 tff(c_1950, plain, (select(a_65, i1)=e_40)). % 6.61/2.48 tff(c_1922, plain, (e_44=e_40)). % 6.61/2.48 tff(c_1919, plain, (e_50=e_40)). % 6.61/2.48 tff(c_1925, plain, (select(a1, i1)=e_40)). % 6.61/2.48 tff(c_1916, plain, (e_52=e_40)). % 6.61/2.48 tff(c_1915, plain, (e_58=e_40)). % 6.61/2.48 tff(c_1911, plain, (e_42=e_40)). % 6.61/2.48 tff(c_1901, plain, (![J_14]: (select(a_65, J_14)=select(a_61, J_14) | i1=J_14))). % 6.61/2.48 tff(c_1891, plain, (select(a_61, i1)=e_40)). % 6.61/2.48 tff(c_1813, plain, (e_62=e_40)). % 6.61/2.48 tff(c_1811, plain, (e_64=e_40)). % 6.61/2.48 tff(c_1812, plain, (e_78=e_40)). % 6.61/2.48 tff(c_1816, plain, (e_76=e_40)). % 6.61/2.48 tff(c_1817, plain, (e_74=e_40)). % 6.61/2.48 tff(c_1818, plain, (e_68=e_40)). % 6.61/2.49 tff(c_372, plain, (![J_14]: (select(a_43, J_14)=select(a2, J_14) | i1=J_14))). % 6.61/2.49 tff(c_1810, plain, (e_70=e_40)). % 6.61/2.49 tff(c_1819, plain, (e_66=e_40)). % 6.61/2.49 tff(c_1809, plain, (e_72=e_40)). % 6.61/2.49 tff(c_1793, plain, (e_60=e_40)). % 6.61/2.49 tff(c_1792, plain, (select(a_57, i1)=e_40)). % 6.61/2.49 tff(c_1766, plain, (select(a_55, i1)=e_40)). % 6.61/2.49 tff(c_1756, plain, (![J_14]: (select(a_57, J_14)=select(a_53, J_14) | i1=J_14))). % 6.61/2.49 tff(c_1724, plain, (store(a_51, i1, e_40)=a_55)). % 6.61/2.49 tff(c_1674, plain, (e_56=e_40)). % 6.61/2.49 tff(c_1688, plain, (![J_14]: (select(a_51, J_14)=select(a_47, J_14) | i1=J_14))). % 6.61/2.49 tff(c_1600, plain, (i8=i1)). % 6.61/2.49 tff(c_1664, plain, (e_54=e_40)). % 6.61/2.49 tff(c_1656, plain, (i5=i1)). % 6.61/2.49 tff(c_1649, plain, (i4=i1)). % 6.61/2.49 tff(c_1601, plain, (i7=i1)). % 6.61/2.49 tff(c_1602, plain, (i6=i1)). % 6.61/2.49 tff(c_1605, plain, (i9=i1)). % 6.61/2.49 tff(c_1611, plain, (![J_14]: (select(a_49, J_14)=select(a_45, J_14) | i1=J_14))). % 6.61/2.49 tff(c_1577, plain, (i10=i1)). % 6.61/2.49 tff(c_1340, plain, (![J_14]: (select(a_45, J_14)=select(a_41, J_14) | i1=J_14))). % 6.61/2.49 tff(c_981, plain, (select(a_49, i1)=e_40)). % 6.61/2.49 tff(c_966, plain, (store(a_45, i1, e_40)=a_49)). % 6.61/2.49 tff(c_956, plain, (e_48=e_40)). % 6.61/2.49 tff(c_949, plain, (i3=i1)). % 6.61/2.49 tff(c_904, plain, (select(a_47, i1)=e_40)). % 6.61/2.49 tff(c_888, plain, (store(a_43, i1, e_40)=a_47)). % 6.61/2.49 tff(c_874, plain, (e_46=e_40)). % 6.61/2.49 tff(c_841, plain, (i2=i1)). % 6.61/2.49 tff(c_357, plain, (![J_14]: (select(a_41, J_14)=select(a1, J_14) | i1=J_14))). % 6.61/2.49 tff(c_399, plain, (![J_14]: (select(a_77, J_14)=select(a_73, J_14) | i1=J_14))). % 6.61/2.49 tff(c_272, plain, (select(a_41, i1)=e_40)). % 6.61/2.49 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.61/2.49 tff(c_2, plain, (![A_1, I_2, E_3]: (select(store(A_1, I_2, E_3), I_2)=E_3))). % 6.61/2.49 tff(c_6, plain, (store(a1, i1, e_40)=a_41)). % 6.61/2.49 tff(c_46, plain, (select(a2, i1)=e_40)). % 6.61/2.49 tff(c_86, plain, (a_79=a_77)). % 6.61/2.49 tff(c_88, plain, (a2!=a1)). % 6.61/2.49 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 6.61/2.49 %------------------------------------------------------------------------------