%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SWV533-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 : n018.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.49s 2.77s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.13 % Problem : SWV533-1.007 : TPTP v9.0.0. Released v4.0.0. % 0.03/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.35 % Computer : n018.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 300 % 0.13/0.35 % DateTime : Wed Apr 9 03:54:32 EDT 2025 % 0.13/0.35 % CPUTime : % 7.49/2.77 % 7.49/2.77 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 7.49/2.77 % 7.49/2.77 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 7.49/2.78 %$ store > select > #nlpp > i5 > i4 > i3 > i2 > i1 > i0 > e_828 > e_826 > e_824 > e_822 > e_819 > e_817 > e_815 > e_813 > e_811 > e_807 > e_805 > e_803 > e_801 > e_798 > e_796 > e_794 > e_792 > e_790 > e_788 > e_786 > e_784 > e_782 > a_829 > a_827 > a_825 > a_823 > a_821 > a_820 > a_818 > a_816 > a_814 > a_812 > a_810 > a_809 > a_808 > a_806 > a_804 > a_802 > a_800 > a_799 > a_797 > a_795 > a_793 > a_791 > a_789 > a_787 > a_785 > a_783 > a1 % 7.49/2.78 % 7.49/2.78 %Foreground sorts: % 7.49/2.78 % 7.49/2.78 % 7.49/2.78 %Background operators: % 7.49/2.78 % 7.49/2.78 % 7.49/2.78 %Foreground operators: % 7.49/2.78 tff(e_817, type, e_817: $i). % 7.49/2.78 tff(a1, type, a1: $i). % 7.49/2.78 tff(a_808, type, a_808: $i). % 7.49/2.78 tff(e_826, type, e_826: $i). % 7.49/2.78 tff(e_813, type, e_813: $i). % 7.49/2.78 tff(a_791, type, a_791: $i). % 7.49/2.78 tff(a_802, type, a_802: $i). % 7.49/2.78 tff(a_810, type, a_810: $i). % 7.49/2.78 tff(e_782, type, e_782: $i). % 7.49/2.78 tff(e_796, type, e_796: $i). % 7.49/2.78 tff(e_828, type, e_828: $i). % 7.49/2.78 tff(a_806, type, a_806: $i). % 7.49/2.78 tff(e_805, type, e_805: $i). % 7.49/2.78 tff(e_803, type, e_803: $i). % 7.49/2.78 tff(e_801, type, e_801: $i). % 7.49/2.78 tff(e_792, type, e_792: $i). % 7.49/2.78 tff(store, type, store: ($i * $i * $i) > $i). % 7.49/2.78 tff(e_819, type, e_819: $i). % 7.49/2.78 tff(e_790, type, e_790: $i). % 7.49/2.78 tff(a_787, type, a_787: $i). % 7.49/2.78 tff(a_820, type, a_820: $i). % 7.49/2.78 tff(e_811, type, e_811: $i). % 7.49/2.78 tff(a_793, type, a_793: $i). % 7.49/2.78 tff(e_807, type, e_807: $i). % 7.49/2.78 tff(a_797, type, a_797: $i). % 7.49/2.78 tff(e_815, type, e_815: $i). % 7.49/2.78 tff(a_827, type, a_827: $i). % 7.49/2.78 tff(a_795, type, a_795: $i). % 7.49/2.78 tff(a_823, type, a_823: $i). % 7.49/2.78 tff(e_786, type, e_786: $i). % 7.49/2.78 tff(e_822, type, e_822: $i). % 7.49/2.78 tff(a_816, type, a_816: $i). % 7.49/2.78 tff(e_784, type, e_784: $i). % 7.49/2.78 tff(a_783, type, a_783: $i). % 7.49/2.78 tff(e_794, type, e_794: $i). % 7.49/2.78 tff(i1, type, i1: $i). % 7.49/2.78 tff(i2, type, i2: $i). % 7.49/2.78 tff(a_785, type, a_785: $i). % 7.49/2.78 tff(a_821, type, a_821: $i). % 7.49/2.78 tff(select, type, select: ($i * $i) > $i). % 7.49/2.78 tff(e_798, type, e_798: $i). % 7.49/2.78 tff(a_812, type, a_812: $i). % 7.49/2.78 tff(a_800, type, a_800: $i). % 7.49/2.78 tff(a_789, type, a_789: $i). % 7.49/2.78 tff(e_788, type, e_788: $i). % 7.49/2.78 tff(a_799, type, a_799: $i). % 7.49/2.78 tff(a_814, type, a_814: $i). % 7.49/2.78 tff(a_809, type, a_809: $i). % 7.49/2.78 tff(i0, type, i0: $i). % 7.49/2.78 tff(a_818, type, a_818: $i). % 7.49/2.78 tff(e_824, type, e_824: $i). % 7.49/2.78 tff(i5, type, i5: $i). % 7.49/2.78 tff(i4, type, i4: $i). % 7.49/2.78 tff(a_829, type, a_829: $i). % 7.49/2.78 tff(a_804, type, a_804: $i). % 7.49/2.78 tff(i3, type, i3: $i). % 7.49/2.78 tff(a_825, type, a_825: $i). % 7.49/2.78 % 7.49/2.78 %Saturated clause set: % 7.49/2.78 tff(c_3255, plain, (![J_14]: (select(a_783, J_14)=select(a1, J_14) | i0=J_14))). % 7.49/2.78 tff(c_3292, plain, (store(a_820, i1, e_782)=a_821)). % 7.49/2.78 tff(c_3319, plain, (store(a_795, i1, e_782)=a_797)). % 7.49/2.78 tff(c_3339, plain, (store(a_793, i1, e_782)=a_795)). % 7.49/2.78 tff(c_3330, plain, (store(a_791, i1, e_782)=a_793)). % 7.49/2.78 tff(c_3321, plain, (store(a_804, i1, e_782)=a_806)). % 7.49/2.78 tff(c_3318, plain, (store(a_806, i1, e_782)=a_808)). % 7.49/2.78 tff(c_3295, plain, (store(a_825, i1, e_782)=a_827)). % 7.49/2.78 tff(c_3290, plain, (store(a_821, i1, e_782)=a_823)). % 7.49/2.78 tff(c_3293, plain, (store(a_816, i1, e_782)=a_818)). % 7.49/2.78 tff(c_3317, plain, (store(a_789, i1, e_782)=a_812)). % 7.49/2.78 tff(c_3316, plain, (store(a_802, i1, e_782)=a_804)). % 7.49/2.78 tff(c_3320, plain, (store(a_797, i1, e_782)=a_799)). % 7.49/2.78 tff(c_3288, plain, (store(a_827, i1, e_782)=a_829)). % 7.49/2.78 tff(c_3291, plain, (store(a_823, i1, e_782)=a_825)). % 7.49/2.78 tff(c_3289, plain, (store(a_818, i1, e_782)=a_820)). % 7.49/2.78 tff(c_3314, plain, (store(a_800, i1, e_782)=a_802)). % 7.49/2.78 tff(c_3315, plain, (store(a_799, i1, e_782)=a_800)). % 7.49/2.78 tff(c_3294, plain, (store(a_814, i1, e_782)=a_816)). % 7.49/2.78 tff(c_1159, plain, (![J_14]: (select(a_797, J_14)=select(a_795, J_14) | i1=J_14))). % 7.49/2.78 tff(c_3302, plain, (select(a_821, i1)=e_782)). % 7.49/2.78 tff(c_3301, plain, (select(a_829, i1)=e_782)). % 7.49/2.78 tff(c_3325, plain, (select(a_799, i1)=e_782)). % 7.49/2.78 tff(c_3300, plain, (select(a_825, i1)=e_782)). % 7.49/2.78 tff(c_3298, plain, (select(a_827, i1)=e_782)). % 7.49/2.78 tff(c_3328, plain, (select(a_812, i1)=e_782)). % 7.49/2.78 tff(c_2922, plain, (![J_14]: (select(a_785, J_14)=select(a_783, J_14) | i1=J_14))). % 7.49/2.78 tff(c_3312, plain, (select(a_785, i0)=e_782)). % 7.49/2.78 tff(c_3303, plain, (select(a_814, i1)=e_782)). % 7.49/2.78 tff(c_3324, plain, (select(a_806, i1)=e_782)). % 7.49/2.78 tff(c_3326, plain, (select(a_804, i1)=e_782)). % 7.49/2.78 tff(c_3304, plain, (select(a_818, i1)=e_782)). % 7.49/2.78 tff(c_3322, plain, (select(a_797, i1)=e_782)). % 7.49/2.78 tff(c_3340, plain, (select(a_795, i1)=e_782)). % 7.49/2.79 tff(c_3313, plain, (select(a_787, i0)=e_782)). % 7.49/2.79 tff(c_3531, plain, (![J_14]: (select(a_812, J_14)=select(a_789, J_14) | i1=J_14))). % 7.49/2.79 tff(c_3327, plain, (select(a_802, i1)=e_782)). % 7.49/2.79 tff(c_3329, plain, (select(a_808, i1)=e_782)). % 7.49/2.79 tff(c_3296, plain, (select(a_820, i1)=e_782)). % 7.49/2.79 tff(c_3337, plain, (select(a_793, i1)=e_782)). % 7.49/2.79 tff(c_3323, plain, (select(a_800, i1)=e_782)). % 7.49/2.79 tff(c_3257, plain, (store(a1, i0, e_782)=a_783)). % 7.49/2.79 tff(c_3299, plain, (select(a_823, i1)=e_782)). % 7.49/2.79 tff(c_3297, plain, (select(a_816, i1)=e_782)). % 7.49/2.79 tff(c_3335, plain, (e_801=e_782)). % 7.49/2.79 tff(c_3420, plain, (![J_5]: (select(a_795, J_5)=select(a_793, J_5) | i1=J_5))). % 7.49/2.79 tff(c_3331, plain, (e_798=e_782)). % 7.49/2.79 tff(c_3306, plain, (e_826=e_782)). % 7.49/2.79 tff(c_3307, plain, (e_817=e_782)). % 7.49/2.79 tff(c_3308, plain, (e_822=e_782)). % 7.49/2.79 tff(c_3338, plain, (e_811=e_782)). % 7.49/2.79 tff(c_3342, plain, (select(a_789, i0)=e_782)). % 7.49/2.79 tff(c_3334, plain, (e_807=e_782)). % 7.49/2.79 tff(c_3333, plain, (e_803=e_782)). % 7.49/2.79 tff(c_3336, plain, (e_796=e_782)). % 7.49/2.79 tff(c_3309, plain, (e_824=e_782)). % 7.49/2.79 tff(c_3310, plain, (e_828=e_782)). % 7.49/2.79 tff(c_3311, plain, (e_815=e_782)). % 7.49/2.79 tff(c_3332, plain, (e_805=e_782)). % 7.49/2.79 tff(c_3341, plain, (e_794=e_782)). % 7.49/2.79 tff(c_3258, plain, (select(a1, i0)=e_784)). % 7.49/2.79 tff(c_3305, plain, (e_819=e_782)). % 7.49/2.79 tff(c_3283, plain, (e_792=e_782)). % 7.49/2.79 tff(c_3256, plain, (select(a_783, i0)=e_782)). % 7.49/2.79 tff(c_3263, plain, (![J_5]: (select(a_806, J_5)=select(a_804, J_5) | i1=J_5))). % 7.49/2.79 tff(c_3254, plain, (i4=i0)). % 7.49/2.79 tff(c_3209, plain, (![J_14]: (select(a_825, J_14)=select(a_823, J_14) | i1=J_14))). % 7.49/2.79 tff(c_478, plain, (![J_14]: (select(a_820, J_14)=select(a_818, J_14) | i1=J_14))). % 7.49/2.79 tff(c_2935, plain, (store(a_812, i0, e_784)=a_814)). % 7.49/2.79 tff(c_2936, plain, (store(a_789, i0, e_784)=a_791)). % 7.49/2.79 tff(c_2942, plain, (store(a_785, i1, e_784)=a_787)). % 7.49/2.79 tff(c_2941, plain, (store(a_787, i1, e_784)=a_789)). % 7.49/2.79 tff(c_3048, plain, (![J_14]: (select(a_802, J_14)=select(a_800, J_14) | i1=J_14))). % 7.49/2.79 tff(c_2938, plain, (select(a_791, i0)=e_784)). % 7.49/2.79 tff(c_2937, plain, (select(a_814, i0)=e_784)). % 7.49/2.79 tff(c_2944, plain, (select(a_787, i1)=e_784)). % 7.49/2.79 tff(c_2924, plain, (store(a_783, i1, e_784)=a_785)). % 7.49/2.79 tff(c_2943, plain, (select(a_789, i1)=e_784)). % 7.49/2.79 tff(c_2925, plain, (select(a1, i1)=e_782)). % 7.49/2.79 tff(c_2940, plain, (e_790=e_784)). % 7.49/2.79 tff(c_2939, plain, (e_813=e_784)). % 7.49/2.79 tff(c_2945, plain, (e_788=e_784)). % 7.49/2.79 tff(c_2930, plain, (e_786=e_784)). % 7.49/2.79 tff(c_2923, plain, (select(a_785, i1)=e_784)). % 7.49/2.79 tff(c_2921, plain, (i3=i1)). % 7.49/2.79 tff(c_2796, plain, (![J_14]: (select(a_827, J_14)=select(a_825, J_14) | i1=J_14))). % 7.49/2.79 tff(c_2774, plain, (![J_14]: (select(a_816, J_14)=select(a_814, J_14) | i1=J_14))). % 7.49/2.79 tff(c_457, plain, (![J_14]: (select(a_814, J_14)=select(a_812, J_14) | i0=J_14))). % 7.49/2.79 tff(c_2693, plain, (![J_14]: (select(a_793, J_14)=select(a_791, J_14) | i1=J_14))). % 7.49/2.79 tff(c_2610, plain, (i1!=i0)). % 7.49/2.79 tff(c_1835, plain, (![J_14]: (select(a_804, J_14)=select(a_802, J_14) | i1=J_14))). % 7.49/2.79 tff(c_1721, plain, (![J_14]: (select(a_787, J_14)=select(a_785, J_14) | i1=J_14))). % 7.49/2.79 tff(c_454, plain, (![J_14]: (select(a_799, J_14)=select(a_797, J_14) | i1=J_14))). % 7.49/2.79 tff(c_1530, plain, (![J_14]: (select(a_818, J_14)=select(a_816, J_14) | i1=J_14))). % 7.49/2.79 tff(c_1412, plain, (![J_14]: (select(a_789, J_14)=select(a_787, J_14) | i1=J_14))). % 7.49/2.79 tff(c_1354, plain, (![J_14]: (select(a_823, J_14)=select(a_821, J_14) | i1=J_14))). % 7.49/2.79 tff(c_1206, plain, (![J_14]: (select(a_808, J_14)=select(a_806, J_14) | i1=J_14))). % 7.49/2.79 tff(c_1152, plain, (i5=i1)). % 7.49/2.79 tff(c_442, plain, (![J_14]: (select(a_800, J_14)=select(a_799, J_14) | i1=J_14))). % 7.49/2.79 tff(c_1060, plain, (a_810=a_789)). % 7.49/2.79 tff(c_463, plain, (![J_14]: (select(a_791, J_14)=select(a_789, J_14) | i0=J_14))). % 7.49/2.79 tff(c_922, plain, (a_809=a_787)). % 7.49/2.79 tff(c_904, plain, (![J_14]: (select(a_829, J_14)=select(a_827, J_14) | i1=J_14))). % 7.49/2.79 tff(c_688, plain, (i2=i1)). % 7.49/2.79 tff(c_430, plain, (![J_14]: (select(a_821, J_14)=select(a_820, J_14) | i1=J_14))). % 7.49/2.79 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.49/2.79 tff(c_2, plain, (![A_1, I_2, E_3]: (select(store(A_1, I_2, E_3), I_2)=E_3))). % 7.49/2.79 tff(c_102, plain, (a_829!=a_808)). % 7.49/2.79 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 7.49/2.79 %------------------------------------------------------------------------------