%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SWV534-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 : n024.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:04 PM UTC 2025 % Result : Satisfiable 7.17s 2.74s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SWV534-1.007 : TPTP v9.0.0. Released v4.0.0. % 0.07/0.13 % 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.13/0.34 % Computer : n024.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Wed Apr 9 03:54:51 EDT 2025 % 0.13/0.34 % CPUTime : % 7.17/2.74 % 7.17/2.74 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 7.17/2.74 % 7.17/2.74 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 7.17/2.75 %$ store > select > #nlpp > i6 > i5 > i4 > i3 > i2 > i1 > i0 > e_830 > e_828 > e_826 > e_824 > e_821 > e_819 > e_817 > e_815 > e_813 > e_809 > e_807 > e_805 > e_803 > e_800 > e_798 > e_796 > e_794 > e_792 > e_790 > e_788 > e_786 > e_784 > a_831 > a_829 > a_827 > a_825 > a_823 > a_822 > a_820 > a_818 > a_816 > a_814 > a_812 > a_811 > a_810 > a_808 > a_806 > a_804 > a_802 > a_801 > a_799 > a_797 > a_795 > a_793 > a_791 > a_789 > a_787 > a_785 > a1 % 7.17/2.75 % 7.17/2.75 %Foreground sorts: % 7.17/2.75 % 7.17/2.75 % 7.17/2.75 %Background operators: % 7.17/2.75 % 7.17/2.75 % 7.17/2.75 %Foreground operators: % 7.17/2.75 tff(e_817, type, e_817: $i). % 7.17/2.75 tff(a1, type, a1: $i). % 7.17/2.75 tff(a_808, type, a_808: $i). % 7.17/2.75 tff(e_826, type, e_826: $i). % 7.17/2.75 tff(e_813, type, e_813: $i). % 7.17/2.75 tff(a_791, type, a_791: $i). % 7.17/2.75 tff(a_802, type, a_802: $i). % 7.17/2.75 tff(a_810, type, a_810: $i). % 7.17/2.75 tff(e_809, type, e_809: $i). % 7.17/2.75 tff(e_796, type, e_796: $i). % 7.17/2.75 tff(e_828, type, e_828: $i). % 7.17/2.75 tff(a_831, type, a_831: $i). % 7.17/2.75 tff(a_811, type, a_811: $i). % 7.17/2.75 tff(a_806, type, a_806: $i). % 7.17/2.75 tff(e_805, type, e_805: $i). % 7.17/2.75 tff(e_803, type, e_803: $i). % 7.17/2.75 tff(e_821, type, e_821: $i). % 7.17/2.75 tff(e_792, type, e_792: $i). % 7.17/2.75 tff(store, type, store: ($i * $i * $i) > $i). % 7.17/2.75 tff(e_819, type, e_819: $i). % 7.17/2.75 tff(a_801, type, a_801: $i). % 7.17/2.75 tff(e_790, type, e_790: $i). % 7.17/2.75 tff(a_822, type, a_822: $i). % 7.17/2.75 tff(a_787, type, a_787: $i). % 7.17/2.75 tff(a_820, type, a_820: $i). % 7.17/2.75 tff(a_793, type, a_793: $i). % 7.17/2.75 tff(e_807, type, e_807: $i). % 7.17/2.75 tff(a_797, type, a_797: $i). % 7.17/2.75 tff(e_815, type, e_815: $i). % 7.17/2.75 tff(a_827, type, a_827: $i). % 7.17/2.75 tff(a_795, type, a_795: $i). % 7.17/2.75 tff(a_823, type, a_823: $i). % 7.17/2.75 tff(e_786, type, e_786: $i). % 7.17/2.75 tff(a_816, type, a_816: $i). % 7.17/2.75 tff(e_784, type, e_784: $i). % 7.17/2.75 tff(e_794, type, e_794: $i). % 7.17/2.75 tff(i1, type, i1: $i). % 7.17/2.75 tff(i2, type, i2: $i). % 7.17/2.75 tff(a_785, type, a_785: $i). % 7.17/2.75 tff(select, type, select: ($i * $i) > $i). % 7.17/2.75 tff(e_798, type, e_798: $i). % 7.17/2.75 tff(a_812, type, a_812: $i). % 7.17/2.75 tff(a_789, type, a_789: $i). % 7.17/2.75 tff(e_788, type, e_788: $i). % 7.17/2.75 tff(a_799, type, a_799: $i). % 7.17/2.75 tff(a_814, type, a_814: $i). % 7.17/2.75 tff(e_830, type, e_830: $i). % 7.17/2.75 tff(i0, type, i0: $i). % 7.17/2.75 tff(a_818, type, a_818: $i). % 7.17/2.75 tff(e_824, type, e_824: $i). % 7.17/2.75 tff(i5, type, i5: $i). % 7.17/2.75 tff(i4, type, i4: $i). % 7.17/2.75 tff(a_829, type, a_829: $i). % 7.17/2.75 tff(a_804, type, a_804: $i). % 7.17/2.75 tff(i3, type, i3: $i). % 7.17/2.75 tff(a_825, type, a_825: $i). % 7.17/2.75 tff(e_800, type, e_800: $i). % 7.17/2.75 tff(i6, type, i6: $i). % 7.17/2.75 % 7.17/2.75 %Saturated clause set: % 7.17/2.75 tff(c_3838, plain, (![J_5]: (select(a_829, J_5)=select(a_806, J_5) | i4=J_5))). % 7.17/2.75 tff(c_3617, plain, (store(a_806, i4, e_786)=a_829)). % 7.17/2.75 tff(c_3628, plain, (store(a_829, i0, e_784)=a_831)). % 7.17/2.75 tff(c_3629, plain, (select(a_831, i0)=e_784)). % 7.17/2.75 tff(c_3619, plain, (select(a_829, i4)=e_786)). % 7.17/2.75 tff(c_3776, plain, (select(a_795, i4)=e_784)). % 7.17/2.75 tff(c_3761, plain, (select(a_801, i4)=e_784)). % 7.17/2.75 tff(c_3748, plain, (select(a_797, i4)=e_784)). % 7.17/2.75 tff(c_3733, plain, (select(a_789, i4)=e_784)). % 7.17/2.75 tff(c_3720, plain, (select(a_799, i4)=e_784)). % 7.17/2.75 tff(c_3705, plain, (select(a_793, i4)=e_784)). % 7.17/2.75 tff(c_3692, plain, (select(a_791, i4)=e_784)). % 7.17/2.75 tff(c_3677, plain, (select(a_806, i4)=e_784)). % 7.17/2.75 tff(c_3662, plain, (select(a_804, i4)=e_784)). % 7.17/2.75 tff(c_3649, plain, (select(a_802, i4)=e_784)). % 7.17/2.75 tff(c_3634, plain, (select(a_787, i4)=e_784)). % 7.17/2.75 tff(c_3623, plain, (e_830=e_784)). % 7.17/2.75 tff(c_3622, plain, (i4!=i0)). % 7.17/2.75 tff(c_3606, plain, (i6=i4)). % 7.17/2.75 tff(c_2879, plain, (![J_14]: (select(a_787, J_14)=select(a_785, J_14) | i0=J_14))). % 7.17/2.75 tff(c_1866, plain, (![J_14]: (select(a_831, J_14)=select(a_829, J_14) | i0=J_14))). % 7.17/2.75 tff(c_3403, plain, (![J_5]: (select(a_801, J_5)=select(a_799, J_5) | i0=J_5))). % 7.17/2.75 tff(c_1861, plain, (![J_14]: (select(a_802, J_14)=select(a_801, J_14) | i0=J_14))). % 7.17/2.75 tff(c_2896, plain, (store(a_802, i0, e_786)=a_804)). % 7.17/2.75 tff(c_2897, plain, (store(a_806, i0, e_786)=a_808)). % 7.17/2.75 tff(c_2894, plain, (store(a_804, i0, e_786)=a_806)). % 7.17/2.75 tff(c_2895, plain, (store(a_808, i0, e_786)=a_810)). % 7.17/2.75 tff(c_2902, plain, (store(a_793, i0, e_786)=a_795)). % 7.17/2.75 tff(c_2898, plain, (store(a_797, i0, e_786)=a_799)). % 7.17/2.75 tff(c_2899, plain, (store(a_801, i0, e_786)=a_802)). % 7.17/2.75 tff(c_2900, plain, (store(a_799, i0, e_786)=a_801)). % 7.17/2.75 tff(c_2932, plain, (store(a_791, i0, e_786)=a_793)). % 7.17/2.76 tff(c_2901, plain, (store(a_795, i0, e_786)=a_797)). % 7.17/2.76 tff(c_2903, plain, (store(a_787, i0, e_786)=a_789)). % 7.17/2.76 tff(c_2904, plain, (store(a_789, i0, e_786)=a_791)). % 7.17/2.76 tff(c_3189, plain, (![J_5]: (select(a_804, J_5)=select(a_802, J_5) | i0=J_5))). % 7.17/2.76 tff(c_2905, plain, (select(a_808, i0)=e_786)). % 7.17/2.76 tff(c_2912, plain, (select(a_802, i0)=e_786)). % 7.17/2.76 tff(c_2910, plain, (select(a_801, i0)=e_786)). % 7.17/2.76 tff(c_2915, plain, (select(a_795, i0)=e_786)). % 7.17/2.76 tff(c_2909, plain, (select(a_810, i0)=e_786)). % 7.17/2.76 tff(c_2906, plain, (select(a_806, i0)=e_786)). % 7.17/2.76 tff(c_2933, plain, (select(a_793, i0)=e_786)). % 7.17/2.76 tff(c_3098, plain, (![J_5]: (select(a_810, J_5)=select(a_808, J_5) | i0=J_5))). % 7.17/2.76 tff(c_2908, plain, (select(a_799, i0)=e_786)). % 7.17/2.76 tff(c_2907, plain, (select(a_804, i0)=e_786)). % 7.17/2.76 tff(c_2913, plain, (select(a_797, i0)=e_786)). % 7.17/2.76 tff(c_2925, plain, (select(a_791, i0)=e_786)). % 7.17/2.76 tff(c_2914, plain, (select(a_789, i0)=e_786)). % 7.17/2.76 tff(c_3030, plain, (![J_5]: (select(a_795, J_5)=select(a_793, J_5) | i0=J_5))). % 7.17/2.76 tff(c_2926, plain, (e_821=e_786)). % 7.17/2.76 tff(c_2918, plain, (e_805=e_786)). % 7.17/2.76 tff(c_2919, plain, (e_803=e_786)). % 7.17/2.76 tff(c_2927, plain, (e_826=e_786)). % 7.17/2.76 tff(c_2928, plain, (e_819=e_786)). % 7.17/2.76 tff(c_2930, plain, (e_824=e_786)). % 7.17/2.76 tff(c_2917, plain, (e_800=e_786)). % 7.17/2.76 tff(c_2929, plain, (e_828=e_786)). % 7.17/2.76 tff(c_2881, plain, (store(a_785, i0, e_786)=a_787)). % 7.17/2.76 tff(c_2921, plain, (e_798=e_786)). % 7.17/2.76 tff(c_2920, plain, (e_809=e_786)). % 7.17/2.76 tff(c_2916, plain, (e_807=e_786)). % 7.17/2.76 tff(c_2931, plain, (e_817=e_786)). % 7.17/2.76 tff(c_2934, plain, (e_815=e_786)). % 7.17/2.76 tff(c_2935, plain, (e_792=e_786)). % 7.17/2.76 tff(c_2936, plain, (e_790=e_786)). % 7.17/2.76 tff(c_2924, plain, (e_794=e_786)). % 7.17/2.76 tff(c_2882, plain, (select(a1, i0)=e_784)). % 7.17/2.76 tff(c_2923, plain, (e_813=e_786)). % 7.17/2.76 tff(c_2922, plain, (e_796=e_786)). % 7.17/2.76 tff(c_2887, plain, (e_788=e_786)). % 7.17/2.76 tff(c_2880, plain, (select(a_787, i0)=e_786)). % 7.17/2.76 tff(c_2878, plain, (i3=i0)). % 7.17/2.76 tff(c_2846, plain, (![J_5]: (select(a_799, J_5)=select(a_797, J_5) | i0=J_5))). % 7.17/2.76 tff(c_2812, plain, (a_827=a_806)). % 7.17/2.76 tff(c_2807, plain, (a_825=a_804)). % 7.17/2.76 tff(c_2788, plain, (a_823=a_802)). % 7.17/2.76 tff(c_2768, plain, (![J_5]: (select(a_797, J_5)=select(a_795, J_5) | i0=J_5))). % 7.17/2.76 tff(c_2761, plain, (a_822=a_801)). % 7.17/2.76 tff(c_2741, plain, (a_820=a_799)). % 7.17/2.76 tff(c_2721, plain, (![J_5]: (select(a_808, J_5)=select(a_806, J_5) | i0=J_5))). % 7.17/2.76 tff(c_2696, plain, (a_818=a_797)). % 7.17/2.76 tff(c_2688, plain, (a_816=a_795)). % 7.17/2.76 tff(c_2683, plain, (a_814=a_793)). % 7.17/2.76 tff(c_2112, plain, (![J_14]: (select(a_806, J_14)=select(a_804, J_14) | i0=J_14))). % 7.17/2.76 tff(c_2058, plain, (![J_14]: (select(a_789, J_14)=select(a_787, J_14) | i0=J_14))). % 7.17/2.76 tff(c_1971, plain, (![J_14]: (select(a_791, J_14)=select(a_789, J_14) | i0=J_14))). % 7.17/2.76 tff(c_1872, plain, (i2=i0)). % 7.17/2.76 tff(c_1860, plain, (i5=i0)). % 7.17/2.76 tff(c_1823, plain, (i1=i0)). % 7.17/2.76 tff(c_487, plain, (![J_14]: (select(a_785, J_14)=select(a1, J_14) | i4=J_14))). % 7.17/2.76 tff(c_1060, plain, (a_812=a_791)). % 7.17/2.76 tff(c_463, plain, (![J_14]: (select(a_793, J_14)=select(a_791, J_14) | i0=J_14))). % 7.17/2.76 tff(c_922, plain, (a_811=a_789)). % 7.17/2.76 tff(c_373, plain, (select(a_785, i4)=e_784)). % 7.17/2.76 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.17/2.76 tff(c_2, plain, (![A_1, I_2, E_3]: (select(store(A_1, I_2, E_3), I_2)=E_3))). % 7.17/2.76 tff(c_6, plain, (store(a1, i4, e_784)=a_785)). % 7.17/2.76 tff(c_60, plain, (select(a1, i4)=e_786)). % 7.17/2.76 tff(c_102, plain, (a_831!=a_810)). % 7.17/2.76 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 7.17/2.76 %------------------------------------------------------------------------------