%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SWV551-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 : n031.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.99s 2.68s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.09 % Problem : SWV551-1.010 : TPTP v9.0.0. Released v4.0.0. % 0.00/0.10 % 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.10/0.29 % Computer : n031.cluster.edu % 0.10/0.29 % Model : x86_64 x86_64 % 0.10/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.29 % Memory : 8042.1875MB % 0.10/0.29 % OS : Linux 3.10.0-693.el7.x86_64 % 0.10/0.29 % CPULimit : 300 % 0.10/0.29 % WCLimit : 300 % 0.10/0.29 % DateTime : Wed Apr 9 04:00:52 EDT 2025 % 0.10/0.29 % CPUTime : % 6.99/2.67 % 6.99/2.68 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 6.99/2.68 % 6.99/2.68 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 6.99/2.68 %$ 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.99/2.68 % 6.99/2.68 %Foreground sorts: % 6.99/2.68 % 6.99/2.68 % 6.99/2.68 %Background operators: % 6.99/2.68 % 6.99/2.68 % 6.99/2.68 %Foreground operators: % 6.99/2.68 tff(e_48, type, e_48: $i). % 6.99/2.68 tff(a1, type, a1: $i). % 6.99/2.68 tff(a_65, type, a_65: $i). % 6.99/2.68 tff(a_73, type, a_73: $i). % 6.99/2.68 tff(e_46, type, e_46: $i). % 6.99/2.68 tff(a_55, type, a_55: $i). % 6.99/2.68 tff(a_77, type, a_77: $i). % 6.99/2.68 tff(e_74, type, e_74: $i). % 6.99/2.68 tff(a_53, type, a_53: $i). % 6.99/2.68 tff(a_49, type, a_49: $i). % 6.99/2.68 tff(a_41, type, a_41: $i). % 6.99/2.68 tff(store, type, store: ($i * $i * $i) > $i). % 6.99/2.68 tff(a_59, type, a_59: $i). % 6.99/2.68 tff(a_67, type, a_67: $i). % 6.99/2.68 tff(a_43, type, a_43: $i). % 6.99/2.68 tff(e_60, type, e_60: $i). % 6.99/2.68 tff(e_56, type, e_56: $i). % 6.99/2.68 tff(e_70, type, e_70: $i). % 6.99/2.68 tff(e_50, type, e_50: $i). % 6.99/2.68 tff(a_79, type, a_79: $i). % 6.99/2.68 tff(a_71, type, a_71: $i). % 6.99/2.68 tff(e_66, type, e_66: $i). % 6.99/2.68 tff(e_68, type, e_68: $i). % 6.99/2.68 tff(i10, type, i10: $i). % 6.99/2.68 tff(e_40, type, e_40: $i). % 6.99/2.68 tff(a2, type, a2: $i). % 6.99/2.68 tff(i8, type, i8: $i). % 6.99/2.68 tff(i9, type, i9: $i). % 6.99/2.68 tff(a_57, type, a_57: $i). % 6.99/2.68 tff(i7, type, i7: $i). % 6.99/2.68 tff(e_42, type, e_42: $i). % 6.99/2.68 tff(e_52, type, e_52: $i). % 6.99/2.68 tff(i1, type, i1: $i). % 6.99/2.68 tff(i2, type, i2: $i). % 6.99/2.68 tff(a_63, type, a_63: $i). % 6.99/2.68 tff(select, type, select: ($i * $i) > $i). % 6.99/2.68 tff(e_78, type, e_78: $i). % 6.99/2.68 tff(e_44, type, e_44: $i). % 6.99/2.68 tff(e_54, type, e_54: $i). % 6.99/2.68 tff(a_69, type, a_69: $i). % 6.99/2.68 tff(a_75, type, a_75: $i). % 6.99/2.68 tff(a_45, type, a_45: $i). % 6.99/2.68 tff(e_72, type, e_72: $i). % 6.99/2.68 tff(a_47, type, a_47: $i). % 6.99/2.68 tff(e_76, type, e_76: $i). % 6.99/2.68 tff(e_62, type, e_62: $i). % 6.99/2.68 tff(a_51, type, a_51: $i). % 6.99/2.68 tff(i5, type, i5: $i). % 6.99/2.68 tff(i4, type, i4: $i). % 6.99/2.68 tff(e_64, type, e_64: $i). % 6.99/2.68 tff(e_58, type, e_58: $i). % 6.99/2.68 tff(i3, type, i3: $i). % 6.99/2.68 tff(a_61, type, a_61: $i). % 6.99/2.68 tff(i6, type, i6: $i). % 6.99/2.68 % 6.99/2.68 %Saturated clause set: % 6.99/2.69 tff(c_3394, 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.99/2.69 tff(c_3372, 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))). % 7.41/2.69 tff(c_3338, plain, (![J_66]: (select(a_43, J_66)=select(a_41, J_66) | i1=J_66 | i1=J_66 | i1=J_66 | i1=J_66 | i1=J_66 | i1=J_66 | i1=J_66 | i1=J_66 | i1=J_66 | i1=J_66 | i1=J_66 | i1=J_66 | i1=J_66 | i1=J_66 | i1=J_66 | i1=J_66 | i1=J_66 | i1=J_66))). % 7.41/2.69 tff(c_3319, 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))). % 7.41/2.69 tff(c_3285, plain, (![J_64]: (select(a_47, J_64)=select(a_45, J_64) | i1=J_64 | i1=J_64 | i1=J_64 | i1=J_64 | i1=J_64 | i1=J_64 | i1=J_64 | i1=J_64 | i1=J_64 | i1=J_64 | i1=J_64 | i1=J_64 | i1=J_64 | i1=J_64 | i1=J_64 | i1=J_64))). % 7.41/2.69 tff(c_3272, 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))). % 7.41/2.69 tff(c_3244, 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))). % 7.41/2.69 tff(c_3210, plain, (![J_61]: (select(a_53, J_61)=select(a_51, J_61) | i1=J_61 | i1=J_61 | i1=J_61 | i1=J_61 | i1=J_61 | i1=J_61 | i1=J_61 | i1=J_61 | i1=J_61 | i1=J_61 | i1=J_61 | i1=J_61 | i1=J_61))). % 7.42/2.69 tff(c_3197, plain, (![J_5]: (select(a_55, J_5)=select(a_53, 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 | i1=J_5))). % 7.42/2.69 tff(c_3160, plain, (![J_59]: (select(a_57, J_59)=select(a_55, J_59) | i1=J_59 | i1=J_59 | i1=J_59 | i1=J_59 | i1=J_59 | i1=J_59 | i1=J_59 | i1=J_59 | i1=J_59 | i1=J_59 | i1=J_59))). % 7.42/2.69 tff(c_3144, 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))). % 7.42/2.69 tff(c_3119, 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))). % 7.42/2.69 tff(c_3085, plain, (![J_56]: (select(a_63, J_56)=select(a_61, J_56) | i1=J_56 | i1=J_56 | i1=J_56 | i1=J_56 | i1=J_56 | i1=J_56 | i1=J_56 | i1=J_56))). % 7.42/2.69 tff(c_3069, plain, (![J_5]: (select(a_65, J_5)=select(a_63, J_5) | i1=J_5 | i1=J_5 | i1=J_5 | i1=J_5 | i1=J_5 | i1=J_5 | i1=J_5))). % 7.42/2.69 tff(c_3035, plain, (![J_54]: (select(a_67, J_54)=select(a_65, J_54) | i1=J_54 | i1=J_54 | i1=J_54 | i1=J_54 | i1=J_54 | i1=J_54))). % 7.42/2.69 tff(c_3022, plain, (![J_14]: (select(a_69, J_14)=select(a_67, J_14) | i1=J_14 | i1=J_14 | i1=J_14 | i1=J_14 | i1=J_14))). % 7.42/2.69 tff(c_2997, plain, (![J_5]: (select(a_71, J_5)=select(a_69, J_5) | i1=J_5 | i1=J_5 | i1=J_5 | i1=J_5))). % 7.42/2.69 tff(c_2645, plain, (![J_44]: (select(a_73, J_44)=select(a_71, J_44) | i1=J_44 | i1=J_44 | i1=J_44))). % 7.42/2.69 tff(c_2175, plain, (![J_14]: (select(a_69, J_14)=select(a_65, J_14) | i1=J_14))). % 7.42/2.69 tff(c_2178, plain, (![J_14]: (select(a_77, J_14)=select(a_75, J_14) | i1=J_14))). % 7.42/2.69 tff(c_2898, plain, (![J_14]: (select(a_53, J_14)=select(a_49, J_14) | i1=J_14))). % 7.42/2.69 tff(c_2878, plain, (![J_14]: (select(a_55, J_14)=select(a_51, J_14) | i1=J_14))). % 7.42/2.69 tff(c_2858, plain, (![J_14]: (select(a_63, J_14)=select(a_59, J_14) | i1=J_14))). % 7.42/2.69 tff(c_2288, plain, (store(a_47, i1, e_40)=a_51)). % 7.42/2.69 tff(c_2289, plain, (store(a_41, i1, e_40)=a_45)). % 7.42/2.69 tff(c_2821, plain, (store(a_69, i1, e_40)=a_73)). % 7.42/2.69 tff(c_2809, plain, (store(a_75, i1, e_40)=a_77)). % 7.42/2.69 tff(c_2797, plain, (store(a_67, i1, e_40)=a_71)). % 7.42/2.69 tff(c_2777, plain, (![J_5]: (select(a_67, J_5)=select(a_63, J_5) | i1=J_5))). % 7.42/2.69 tff(c_2765, plain, (store(a_59, i1, e_40)=a_63)). % 7.42/2.69 tff(c_2753, plain, (store(a_61, i1, e_40)=a_65)). % 7.42/2.69 tff(c_2741, plain, (store(a_73, i1, e_40)=a_77)). % 7.42/2.69 tff(c_2729, plain, (store(a_71, i1, e_40)=a_75)). % 7.42/2.69 tff(c_2717, plain, (store(a_51, i1, e_40)=a_55)). % 7.42/2.69 tff(c_2697, plain, (![J_5]: (select(a_59, J_5)=select(a_55, J_5) | i1=J_5))). % 7.42/2.69 tff(c_2685, plain, (store(a_65, i1, e_40)=a_69)). % 7.42/2.69 tff(c_2673, plain, (store(a_53, i1, e_40)=a_57)). % 7.42/2.69 tff(c_2661, plain, (store(a_63, i1, e_40)=a_67)). % 7.42/2.69 tff(c_2635, plain, (![J_5]: (select(a_75, J_5)=select(a_71, J_5) | i1=J_5))). % 7.42/2.69 tff(c_2623, plain, (store(a_57, i1, e_40)=a_61)). % 7.42/2.69 tff(c_2611, plain, (store(a_55, i1, e_40)=a_59)). % 7.42/2.69 tff(c_2599, plain, (store(a_49, i1, e_40)=a_53)). % 7.42/2.69 tff(c_2291, plain, (select(a_45, i1)=e_40)). % 7.42/2.69 tff(c_2290, plain, (select(a_51, i1)=e_40)). % 7.42/2.69 tff(c_2555, plain, (select(a_75, i1)=e_40)). % 7.42/2.69 tff(c_2540, plain, (select(a_77, i1)=e_40)). % 7.42/2.69 tff(c_2520, plain, (![J_5]: (select(a_65, J_5)=select(a_61, J_5) | i1=J_5))). % 7.42/2.69 tff(c_2515, plain, (select(a_65, i1)=e_40)). % 7.42/2.69 tff(c_2510, plain, (select(a_63, i1)=e_40)). % 7.42/2.69 tff(c_2495, plain, (select(a_57, i1)=e_40)). % 7.42/2.69 tff(c_2480, plain, (select(a_73, i1)=e_40)). % 7.42/2.69 tff(c_2475, plain, (select(a_55, i1)=e_40)). % 7.42/2.69 tff(c_2391, plain, (select(a_43, i1)=e_40)). % 7.42/2.69 tff(c_2456, plain, (select(a_69, i1)=e_40)). % 7.42/2.70 tff(c_2441, plain, (select(a_71, i1)=e_40)). % 7.42/2.70 tff(c_2436, plain, (select(a_67, i1)=e_40)). % 7.42/2.70 tff(c_2418, plain, (![J_14]: (select(a_61, J_14)=select(a_57, J_14) | i1=J_14))). % 7.42/2.70 tff(c_2413, plain, (select(a_61, i1)=e_40)). % 7.42/2.70 tff(c_2408, plain, (select(a_59, i1)=e_40)). % 7.42/2.70 tff(c_2403, plain, (select(a_53, i1)=e_40)). % 7.42/2.70 tff(c_2283, plain, (e_74=e_40)). % 7.42/2.70 tff(c_2284, plain, (e_54=e_40)). % 7.42/2.70 tff(c_2295, plain, (store(a2, i1, e_40)=a_43)). % 7.42/2.70 tff(c_2285, plain, (e_66=e_40)). % 7.42/2.70 tff(c_2286, plain, (e_60=e_40)). % 7.42/2.70 tff(c_2372, plain, (e_70=e_40)). % 7.42/2.70 tff(c_2362, plain, (![J_5]: (select(a_73, J_5)=select(a_69, J_5) | i1=J_5))). % 7.42/2.70 tff(c_2357, plain, (e_68=e_40)). % 7.42/2.70 tff(c_2352, plain, (e_64=e_40)). % 7.42/2.70 tff(c_2347, plain, (e_62=e_40)). % 7.42/2.70 tff(c_2342, plain, (e_78=e_40)). % 7.42/2.70 tff(c_2287, plain, (e_58=e_40)). % 7.42/2.70 tff(c_2296, plain, (select(a1, i1)=e_40)). % 7.42/2.70 tff(c_2292, plain, (e_50=e_40)). % 7.42/2.70 tff(c_2293, plain, (e_44=e_40)). % 7.42/2.70 tff(c_2321, plain, (e_72=e_40)). % 7.42/2.70 tff(c_2311, plain, (![J_14]: (select(a_71, J_14)=select(a_67, J_14) | i1=J_14))). % 7.42/2.70 tff(c_2306, plain, (e_56=e_40)). % 7.42/2.70 tff(c_2301, plain, (e_76=e_40)). % 7.42/2.70 tff(c_2274, plain, (e_42=e_40)). % 7.42/2.70 tff(c_2180, plain, (e_52=e_40)). % 7.42/2.70 tff(c_2264, plain, (![J_5]: (select(a_57, J_5)=select(a_53, J_5) | i1=J_5))). % 7.42/2.70 tff(c_2170, plain, (i7=i1)). % 7.42/2.70 tff(c_2171, plain, (i5=i1)). % 7.42/2.70 tff(c_2172, plain, (i6=i1)). % 7.42/2.70 tff(c_2208, plain, (![J_5]: (select(a_77, J_5)=select(a_73, J_5) | i1=J_5))). % 7.47/2.70 tff(c_2173, plain, (i4=i1)). % 7.47/2.70 tff(c_2176, plain, (i8=i1)). % 7.47/2.70 tff(c_2179, plain, (i9=i1)). % 7.47/2.70 tff(c_2186, plain, (![J_30]: (select(a_75, J_30)=select(a_73, J_30) | i1=J_30 | i1=J_30))). % 7.47/2.70 tff(c_2137, plain, (i10=i1)). % 7.47/2.70 tff(c_1131, plain, (![J_14]: (select(a_45, J_14)=select(a_41, J_14) | i1=J_14))). % 7.47/2.70 tff(c_1801, plain, (![J_14]: (select(a_51, J_14)=select(a_47, J_14) | i1=J_14))). % 7.47/2.70 tff(c_1769, plain, (![J_14]: (select(a_49, J_14)=select(a_45, J_14) | i1=J_14))). % 7.47/2.70 tff(c_1461, plain, (![J_14]: (select(a_47, J_14)=select(a_43, J_14) | i1=J_14))). % 7.47/2.70 tff(c_1241, plain, (store(a_45, i1, e_40)=a_49)). % 7.47/2.70 tff(c_1212, plain, (select(a_49, i1)=e_40)). % 7.47/2.70 tff(c_1195, plain, (store(a_43, i1, e_40)=a_47)). % 7.47/2.70 tff(c_1190, plain, (select(a_47, i1)=e_40)). % 7.47/2.70 tff(c_357, plain, (![J_14]: (select(a_41, J_14)=select(a1, J_14) | i1=J_14))). % 7.47/2.70 tff(c_1144, plain, (e_48=e_40)). % 7.47/2.70 tff(c_1130, plain, (i3=i1)). % 7.47/2.70 tff(c_1138, plain, (e_46=e_40)). % 7.47/2.70 tff(c_1125, plain, (i2=i1)). % 7.47/2.70 tff(c_372, plain, (![J_14]: (select(a_43, J_14)=select(a2, J_14) | i1=J_14))). % 7.47/2.70 tff(c_272, plain, (select(a_41, i1)=e_40)). % 7.47/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))). % 7.47/2.70 tff(c_2, plain, (![A_1, I_2, E_3]: (select(store(A_1, I_2, E_3), I_2)=E_3))). % 7.47/2.70 tff(c_6, plain, (store(a1, i1, e_40)=a_41)). % 7.47/2.70 tff(c_46, plain, (select(a2, i1)=e_40)). % 7.47/2.70 tff(c_86, plain, (a_79=a_77)). % 7.47/2.70 tff(c_88, plain, (a2!=a1)). % 7.47/2.70 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 7.47/2.70 %------------------------------------------------------------------------------