%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SWV538-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/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/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:06 PM UTC 2025 % Result : Satisfiable 6.83s 2.95s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.08 % Problem : SWV538-1.007 : TPTP v9.0.0. Released v4.0.0. % 0.08/0.09 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % 0.08/0.28 % Computer : n007.cluster.edu % 0.08/0.28 % Model : x86_64 x86_64 % 0.08/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.28 % Memory : 8042.1875MB % 0.08/0.28 % OS : Linux 3.10.0-693.el7.x86_64 % 0.08/0.28 % CPULimit : 300 % 0.08/0.28 % WCLimit : 300 % 0.08/0.28 % DateTime : Wed Apr 9 03:56:24 EDT 2025 % 0.08/0.28 % CPUTime : % 6.83/2.95 % 6.83/2.95 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 6.83/2.95 % 6.83/2.95 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 6.83/2.96 %$ store > sk > select > #nlpp > i_883 > i6 > i5 > i4 > i3 > i2 > i1 > i0 > e_885 > e_884 > e_881 > e_879 > e_877 > e_875 > e_872 > e_870 > e_868 > e_866 > e_864 > e_860 > e_858 > e_856 > e_854 > e_851 > e_849 > e_847 > e_845 > e_843 > e_841 > e_839 > e_837 > e_835 > a_882 > a_880 > a_878 > a_876 > a_874 > a_873 > a_871 > a_869 > a_867 > a_865 > a_863 > a_862 > a_861 > a_859 > a_857 > a_855 > a_853 > a_852 > a_850 > a_848 > a_846 > a_844 > a_842 > a_840 > a_838 > a_836 > a1 % 6.83/2.96 % 6.83/2.96 %Foreground sorts: % 6.83/2.96 % 6.83/2.96 % 6.83/2.96 %Background operators: % 6.83/2.96 % 6.83/2.96 % 6.83/2.96 %Foreground operators: % 6.83/2.96 tff(a_882, type, a_882: $i). % 6.83/2.96 tff(a1, type, a1: $i). % 6.83/2.96 tff(a_852, type, a_852: $i). % 6.83/2.96 tff(e_868, type, e_868: $i). % 6.83/2.96 tff(e_870, type, e_870: $i). % 6.83/2.96 tff(a_871, type, a_871: $i). % 6.83/2.96 tff(a_844, type, a_844: $i). % 6.83/2.96 tff(a_857, type, a_857: $i). % 6.83/2.96 tff(e_847, type, e_847: $i). % 6.83/2.96 tff(e_879, type, e_879: $i). % 6.83/2.96 tff(a_838, type, a_838: $i). % 6.83/2.96 tff(e_866, type, e_866: $i). % 6.83/2.96 tff(a_840, type, a_840: $i). % 6.83/2.96 tff(e_864, type, e_864: $i). % 6.83/2.96 tff(a_850, type, a_850: $i). % 6.83/2.96 tff(a_867, type, a_867: $i). % 6.83/2.96 tff(store, type, store: ($i * $i * $i) > $i). % 6.83/2.96 tff(a_876, type, a_876: $i). % 6.83/2.96 tff(i_883, type, i_883: $i). % 6.83/2.96 tff(e_839, type, e_839: $i). % 6.83/2.96 tff(a_869, type, a_869: $i). % 6.83/2.96 tff(a_855, type, a_855: $i). % 6.83/2.96 tff(a_859, type, a_859: $i). % 6.83/2.96 tff(a_848, type, a_848: $i). % 6.83/2.96 tff(a_853, type, a_853: $i). % 6.83/2.96 tff(a_846, type, a_846: $i). % 6.83/2.96 tff(e_884, type, e_884: $i). % 6.83/2.96 tff(e_854, type, e_854: $i). % 6.83/2.96 tff(e_849, type, e_849: $i). % 6.83/2.96 tff(e_872, type, e_872: $i). % 6.83/2.96 tff(e_841, type, e_841: $i). % 6.83/2.96 tff(a_862, type, a_862: $i). % 6.83/2.96 tff(e_877, type, e_877: $i). % 6.83/2.96 tff(e_856, type, e_856: $i). % 6.83/2.96 tff(sk, type, sk: ($i * $i) > $i). % 6.83/2.96 tff(a_863, type, a_863: $i). % 6.83/2.96 tff(i1, type, i1: $i). % 6.83/2.96 tff(i2, type, i2: $i). % 6.83/2.96 tff(e_881, type, e_881: $i). % 6.83/2.96 tff(a_874, type, a_874: $i). % 6.83/2.96 tff(select, type, select: ($i * $i) > $i). % 6.83/2.96 tff(a_861, type, a_861: $i). % 6.83/2.96 tff(e_845, type, e_845: $i). % 6.83/2.96 tff(e_860, type, e_860: $i). % 6.83/2.96 tff(e_851, type, e_851: $i). % 6.83/2.96 tff(a_878, type, a_878: $i). % 6.83/2.96 tff(e_837, type, e_837: $i). % 6.83/2.96 tff(a_836, type, a_836: $i). % 6.83/2.96 tff(e_843, type, e_843: $i). % 6.83/2.96 tff(e_885, type, e_885: $i). % 6.83/2.96 tff(i0, type, i0: $i). % 6.83/2.96 tff(e_875, type, e_875: $i). % 6.83/2.96 tff(a_873, type, a_873: $i). % 6.83/2.96 tff(i5, type, i5: $i). % 6.83/2.96 tff(e_858, type, e_858: $i). % 6.83/2.96 tff(i4, type, i4: $i). % 6.83/2.96 tff(a_865, type, a_865: $i). % 6.83/2.96 tff(e_835, type, e_835: $i). % 6.83/2.96 tff(i3, type, i3: $i). % 6.83/2.96 tff(a_842, type, a_842: $i). % 6.83/2.96 tff(i6, type, i6: $i). % 6.83/2.96 tff(a_880, type, a_880: $i). % 6.83/2.96 % 6.83/2.96 %Saturated clause set: % 6.83/2.96 tff(c_3468, plain, (![J_5]: (select(a_880, J_5)=select(a_857, J_5) | i4=J_5))). % 6.83/2.96 tff(c_3251, plain, (store(a_880, i0, e_835)=a_882)). % 6.83/2.96 tff(c_3231, plain, (store(a_857, i4, e_837)=a_880)). % 6.83/2.96 tff(c_3418, plain, (select(a_846, i4)=e_835)). % 6.83/2.96 tff(c_3403, plain, (select(a_844, i4)=e_835)). % 6.83/2.96 tff(c_3390, plain, (select(a_848, i4)=e_835)). % 6.83/2.96 tff(c_3376, plain, (select(a_850, i4)=e_835)). % 6.83/2.96 tff(c_3252, plain, (select(a_882, i0)=e_835)). % 6.83/2.96 tff(c_3351, plain, (select(a_852, i4)=e_835)). % 6.83/2.96 tff(c_3336, plain, (select(a_842, i4)=e_835)). % 6.83/2.96 tff(c_3321, plain, (select(a_840, i4)=e_835)). % 6.83/2.96 tff(c_3306, plain, (select(a_855, i4)=e_835)). % 6.83/2.96 tff(c_3291, plain, (select(a_838, i4)=e_835)). % 6.83/2.96 tff(c_3278, plain, (select(a_853, i4)=e_835)). % 6.83/2.96 tff(c_3240, plain, (select(a_880, i4)=e_837)). % 6.83/2.96 tff(c_3261, plain, (select(a_857, i4)=e_835)). % 6.83/2.96 tff(c_3250, plain, (e_885=e_835)). % 6.83/2.96 tff(c_3249, plain, (e_837!=e_835)). % 6.83/2.96 tff(c_3242, plain, (i4!=i0)). % 6.83/2.96 tff(c_3244, plain, (e_881=e_835)). % 6.83/2.96 tff(c_3227, plain, (i6=i4)). % 6.83/2.96 tff(c_2287, plain, (![J_14]: (select(a_838, J_14)=select(a_836, J_14) | i0=J_14))). % 6.83/2.96 tff(c_1443, plain, (![J_14]: (select(a_882, J_14)=select(a_880, J_14) | i0=J_14))). % 6.83/2.96 tff(c_1461, plain, (![J_14]: (select(a_857, J_14)=select(a_855, J_14) | i0=J_14))). % 6.83/2.96 tff(c_3101, plain, (![J_14]: (select(a_840, J_14)=select(a_838, J_14) | i0=J_14))). % 6.83/2.96 tff(c_2304, plain, (store(a_853, i0, e_837)=a_855)). % 6.83/2.96 tff(c_2314, plain, (store(a_857, i0, e_837)=a_859)). % 6.83/2.96 tff(c_2307, plain, (store(a_852, i0, e_837)=a_853)). % 6.83/2.96 tff(c_2303, plain, (store(a_850, i0, e_837)=a_852)). % 6.83/2.96 tff(c_2313, plain, (store(a_855, i0, e_837)=a_857)). % 6.83/2.96 tff(c_2305, plain, (store(a_844, i0, e_837)=a_846)). % 6.83/2.96 tff(c_3001, plain, (![J_14]: (select(a_842, J_14)=select(a_840, J_14) | i0=J_14))). % 6.83/2.96 tff(c_2309, plain, (store(a_859, i0, e_837)=a_861)). % 6.83/2.96 tff(c_2311, plain, (store(a_842, i0, e_837)=a_844)). % 6.83/2.96 tff(c_2312, plain, (store(a_848, i0, e_837)=a_850)). % 6.83/2.96 tff(c_2306, plain, (store(a_840, i0, e_837)=a_842)). % 6.83/2.96 tff(c_2308, plain, (store(a_846, i0, e_837)=a_848)). % 6.83/2.96 tff(c_2310, plain, (store(a_838, i0, e_837)=a_840)). % 6.83/2.96 tff(c_2856, plain, (![J_5]: (select(a_859, J_5)=select(a_857, J_5) | i0=J_5))). % 6.83/2.96 tff(c_2342, plain, (select(a_844, i0)=e_837)). % 6.83/2.96 tff(c_2317, plain, (select(a_859, i0)=e_837)). % 6.83/2.96 tff(c_2318, plain, (select(a_857, i0)=e_837)). % 6.83/2.96 tff(c_2316, plain, (select(a_861, i0)=e_837)). % 6.83/2.96 tff(c_2329, plain, (select(a_855, i0)=e_837)). % 6.83/2.96 tff(c_2321, plain, (select(a_852, i0)=e_837)). % 6.83/2.96 tff(c_2315, plain, (select(a_853, i0)=e_837)). % 6.83/2.96 tff(c_2319, plain, (select(a_850, i0)=e_837)). % 6.83/2.96 tff(c_2322, plain, (select(a_846, i0)=e_837)). % 6.83/2.96 tff(c_2658, plain, (![J_5]: (select(a_848, J_5)=select(a_846, J_5) | i0=J_5))). % 6.83/2.96 tff(c_2324, plain, (select(a_848, i0)=e_837)). % 6.83/2.96 tff(c_2325, plain, (select(a_840, i0)=e_837)). % 6.83/2.96 tff(c_2335, plain, (select(a_842, i0)=e_837)). % 6.83/2.96 tff(c_2301, plain, (e_884=e_837)). % 6.83/2.96 tff(c_2340, plain, (e_877=e_837)). % 6.83/2.96 tff(c_2337, plain, (e_872=e_837)). % 6.83/2.96 tff(c_2449, plain, (![J_14]: (select(a_855, J_14)=select(a_853, J_14) | i0=J_14))). % 6.83/2.96 tff(c_2339, plain, (e_879=e_837)). % 6.83/2.96 tff(c_2338, plain, (e_875=e_837)). % 6.83/2.96 tff(c_2332, plain, (e_849=e_837)). % 6.83/2.96 tff(c_2336, plain, (e_870=e_837)). % 6.83/2.96 tff(c_2328, plain, (e_860=e_837)). % 6.83/2.96 tff(c_2289, plain, (store(a_836, i0, e_837)=a_838)). % 6.83/2.96 tff(c_2343, plain, (e_866=e_837)). % 6.83/2.96 tff(c_2331, plain, (e_854=e_837)). % 6.83/2.96 tff(c_2344, plain, (e_843=e_837)). % 6.83/2.96 tff(c_2396, plain, (![J_14]: (select(a_846, J_14)=select(a_844, J_14) | i0=J_14))). % 6.83/2.96 tff(c_2327, plain, (e_858=e_837)). % 6.83/2.96 tff(c_2341, plain, (e_868=e_837)). % 6.83/2.96 tff(c_2330, plain, (e_851=e_837)). % 6.83/2.96 tff(c_2326, plain, (e_856=e_837)). % 6.83/2.96 tff(c_2333, plain, (e_847=e_837)). % 6.83/2.96 tff(c_2290, plain, (select(a1, i0)=e_835)). % 6.83/2.97 tff(c_2334, plain, (e_845=e_837)). % 6.83/2.97 tff(c_2345, plain, (e_841=e_837)). % 6.83/2.97 tff(c_2323, plain, (e_864=e_837)). % 6.83/2.97 tff(c_2350, plain, (![J_14]: (select(a_850, J_14)=select(a_848, J_14) | i0=J_14))). % 6.83/2.97 tff(c_2295, plain, (e_839=e_837)). % 6.83/2.97 tff(c_2288, plain, (select(a_838, i0)=e_837)). % 6.83/2.97 tff(c_2286, plain, (i3=i0)). % 6.83/2.97 tff(c_2245, plain, (sk(a_861, a_882)=i0)). % 6.83/2.97 tff(c_425, plain, (![J_14]: (select(a_836, J_14)=select(a1, J_14) | i4=J_14))). % 6.83/2.97 tff(c_2242, plain, (i_883=i0)). % 6.83/2.97 tff(c_2206, plain, (a_878=a_857)). % 6.83/2.97 tff(c_2196, plain, (a_876=a_855)). % 6.83/2.97 tff(c_2188, plain, (a_874=a_853)). % 6.83/2.97 tff(c_2184, plain, (a_873=a_852)). % 6.83/2.97 tff(c_2121, plain, (a_871=a_850)). % 6.83/2.97 tff(c_2127, plain, (![J_14]: (select(a_861, J_14)=select(a_859, J_14) | i0=J_14))). % 6.83/2.97 tff(c_2113, plain, (a_869=a_848)). % 6.83/2.97 tff(c_2104, plain, (a_867=a_846)). % 6.83/2.97 tff(c_2100, plain, (a_865=a_844)). % 6.83/2.97 tff(c_1974, plain, (a_863=a_842)). % 6.83/2.97 tff(c_1918, plain, (a_862=a_840)). % 6.83/2.97 tff(c_1711, plain, (![J_14]: (select(a_852, J_14)=select(a_850, J_14) | i0=J_14))). % 6.83/2.97 tff(c_1521, plain, (![J_14]: (select(a_853, J_14)=select(a_852, J_14) | i0=J_14))). % 6.83/2.97 tff(c_1474, plain, (i5=i0)). % 6.83/2.97 tff(c_1467, plain, (i2=i0)). % 6.83/2.97 tff(c_1418, plain, (i1=i0)). % 6.83/2.97 tff(c_476, plain, (![J_14]: (select(a_844, J_14)=select(a_842, J_14) | i0=J_14))). % 6.83/2.97 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.83/2.97 tff(c_322, plain, (select(a_836, i4)=e_835)). % 6.83/2.97 tff(c_2, plain, (![A_1, I_2, E_3]: (select(store(A_1, I_2, E_3), I_2)=E_3))). % 6.83/2.97 tff(c_6, plain, (store(a1, i4, e_835)=a_836)). % 6.83/2.97 tff(c_60, plain, (select(a1, i4)=e_837)). % 6.83/2.97 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 6.83/2.97 %------------------------------------------------------------------------------