%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SYN738-1 : TPTP v9.0.0. Released v2.5.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 : n003.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 10:04:20 PM UTC 2025 % Result : Satisfiable 3.51s 1.86s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SYN738-1 : TPTP v9.0.0. Released v2.5.0. % 0.03/0.13 % 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.12/0.33 % Computer : n003.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Wed Apr 9 08:13:48 EDT 2025 % 0.12/0.33 % CPUTime : % 3.51/1.86 % 3.51/1.86 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 3.51/1.86 % 3.51/1.86 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 3.51/1.86 %$ ssRr > ssPv8 > ssPv7 > ssPv6 > ssPv5 > ssPv4 > ssPv3 > ssPv2 > ssPv1 > #nlpp > skf1 % 3.51/1.86 % 3.51/1.86 %Foreground sorts: % 3.51/1.86 % 3.51/1.86 % 3.51/1.86 %Background operators: % 3.51/1.86 % 3.51/1.86 % 3.51/1.86 %Foreground operators: % 3.51/1.86 tff(skf1, type, skf1: $i > $i). % 3.51/1.86 tff(ssPv1, type, ssPv1: $i > $o). % 3.51/1.86 tff(ssPv3, type, ssPv3: $i > $o). % 3.51/1.86 tff(ssPv7, type, ssPv7: $i > $o). % 3.51/1.86 tff(ssPv6, type, ssPv6: $i > $o). % 3.51/1.86 tff(ssPv5, type, ssPv5: $i > $o). % 3.51/1.86 tff(ssRr, type, ssRr: ($i * $i) > $o). % 3.51/1.86 tff(ssPv4, type, ssPv4: $i > $o). % 3.51/1.86 tff(ssPv2, type, ssPv2: $i > $o). % 3.51/1.86 tff(ssPv8, type, ssPv8: $i > $o). % 3.51/1.86 % 3.51/1.86 %Saturated clause set: % 3.51/1.87 tff(c_269, plain, (![U_1]: (ssPv7(U_1) | ssPv5(U_1) | ~ssPv2(U_1) | ~ssPv8(U_1) | ~ssPv3(U_1) | ~ssPv6(U_1) | ~ssPv1(U_1) | ~ssPv3(skf1(U_1))))). % 3.51/1.87 tff(c_251, plain, (![U_1]: (ssPv7(U_1) | ssPv5(U_1) | ~ssPv8(skf1(U_1)) | ~ssPv2(U_1) | ~ssPv6(U_1) | ~ssPv1(U_1) | ~ssPv3(skf1(U_1))))). % 3.51/1.87 tff(c_157, plain, (![U_130, V_83]: (ssPv7(U_130) | ssPv5(U_130) | ~ssPv8(V_83) | ~ssRr(U_130, V_83) | ~ssPv2(U_130) | ~ssPv6(U_130) | ~ssPv1(U_130) | ~ssPv3(skf1(U_130))))). % 3.51/1.87 tff(c_241, plain, (![U_185]: (ssPv4(skf1(U_185)) | ~ssPv2(U_185) | ~ssPv1(U_185) | ~ssPv7(U_185) | ~ssPv1(skf1(U_185)) | ~ssPv3(skf1(U_185))))). % 3.51/1.87 tff(c_242, plain, (![U_185]: (ssPv6(U_185) | ~ssPv4(U_185) | ~ssPv3(U_185) | ~ssPv7(U_185) | ~ssPv1(skf1(U_185)) | ~ssPv3(skf1(U_185))))). % 3.51/1.87 tff(c_233, plain, (![U_1]: (ssPv7(skf1(U_1)) | ~ssPv7(U_1) | ~ssPv1(skf1(U_1)) | ~ssPv3(skf1(U_1))))). % 3.51/1.87 tff(c_229, plain, (![U_1, V_182]: (ssPv7(skf1(U_1)) | ~ssPv7(U_1) | ~ssPv1(skf1(U_1)) | ~ssPv3(V_182) | ~ssRr(U_1, V_182)))). % 3.51/1.87 tff(c_225, plain, (![U_1, W_178, V_179]: (ssPv7(skf1(U_1)) | ~ssPv7(U_1) | ~ssPv1(W_178) | ~ssRr(U_1, W_178) | ~ssPv3(V_179) | ~ssRr(U_1, V_179)))). % 3.51/1.87 tff(c_42, plain, (![X_62, U_59, W_61, V_60]: (ssPv7(X_62) | ~ssPv7(U_59) | ~ssRr(U_59, X_62) | ~ssPv1(W_61) | ~ssRr(U_59, W_61) | ~ssPv3(V_60) | ~ssRr(U_59, V_60)))). % 3.51/1.87 tff(c_217, plain, (![U_1, V_173]: (ssPv6(skf1(U_1)) | ssPv8(skf1(U_1)) | ~ssPv3(U_1) | ~ssPv6(V_173) | ~ssRr(U_1, V_173)))). % 3.51/1.87 tff(c_213, plain, (![U_1, W_168, V_170]: (ssPv6(skf1(U_1)) | ssPv8(W_168) | ~ssPv3(U_1) | ~ssRr(U_1, W_168) | ~ssPv6(V_170) | ~ssRr(U_1, V_170)))). % 3.51/1.87 tff(c_36, plain, (![X_50, W_49, U_47, V_48]: (ssPv6(X_50) | ssPv8(W_49) | ~ssPv3(U_47) | ~ssRr(U_47, X_50) | ~ssRr(U_47, W_49) | ~ssPv6(V_48) | ~ssRr(U_47, V_48)))). % 3.51/1.87 tff(c_204, plain, (![U_1]: (ssPv5(skf1(U_1)) | ~ssPv4(U_1) | ~ssPv3(skf1(U_1)) | ~ssPv6(skf1(U_1))))). % 3.51/1.87 tff(c_200, plain, (![U_1, V_163]: (ssPv5(skf1(U_1)) | ~ssPv4(U_1) | ~ssPv3(skf1(U_1)) | ~ssPv6(V_163) | ~ssRr(U_1, V_163)))). % 3.51/1.87 tff(c_196, plain, (![U_1, W_159, V_160]: (ssPv5(skf1(U_1)) | ~ssPv4(U_1) | ~ssPv3(W_159) | ~ssRr(U_1, W_159) | ~ssPv6(V_160) | ~ssRr(U_1, V_160)))). % 3.51/1.87 tff(c_40, plain, (![X_58, U_55, W_57, V_56]: (ssPv5(X_58) | ~ssPv4(U_55) | ~ssRr(U_55, X_58) | ~ssPv3(W_57) | ~ssRr(U_55, W_57) | ~ssPv6(V_56) | ~ssRr(U_55, V_56)))). % 3.51/1.87 tff(c_191, plain, (![U_1]: (ssPv4(skf1(U_1)) | ssPv6(skf1(U_1)) | ~ssPv5(U_1) | ~ssPv5(skf1(U_1))))). % 3.51/1.87 tff(c_187, plain, (![U_1, V_153]: (ssPv4(skf1(U_1)) | ssPv6(skf1(U_1)) | ~ssPv5(U_1) | ~ssPv5(V_153) | ~ssRr(U_1, V_153)))). % 3.51/1.87 tff(c_178, plain, (![U_1, W_145, V_147]: (ssPv4(skf1(U_1)) | ssPv6(W_145) | ~ssPv5(U_1) | ~ssRr(U_1, W_145) | ~ssPv5(V_147) | ~ssRr(U_1, V_147)))). % 3.51/1.87 tff(c_182, plain, (![U_1]: (ssPv4(U_1) | ssPv3(skf1(U_1)) | ssPv8(skf1(U_1)) | ~ssPv7(skf1(U_1))))). % 3.51/1.87 tff(c_174, plain, (![U_1, V_143]: (ssPv4(U_1) | ssPv3(skf1(U_1)) | ssPv8(skf1(U_1)) | ~ssPv7(V_143) | ~ssRr(U_1, V_143)))). % 3.51/1.87 tff(c_38, plain, (![X_54, W_53, U_51, V_52]: (ssPv4(X_54) | ssPv6(W_53) | ~ssPv5(U_51) | ~ssRr(U_51, X_54) | ~ssRr(U_51, W_53) | ~ssPv5(V_52) | ~ssRr(U_51, V_52)))). % 3.51/1.87 tff(c_165, plain, (![U_1, W_136, V_137]: (ssPv4(U_1) | ssPv3(skf1(U_1)) | ssPv8(W_136) | ~ssRr(U_1, W_136) | ~ssPv7(V_137) | ~ssRr(U_1, V_137)))). % 3.51/1.87 tff(c_169, plain, (![U_1]: (ssPv8(U_1) | ssPv6(U_1) | ssPv5(skf1(U_1)) | ~ssPv3(skf1(U_1))))). % 3.51/1.87 tff(c_161, plain, (![U_1, V_133]: (ssPv8(U_1) | ssPv6(U_1) | ssPv5(skf1(U_1)) | ~ssPv3(V_133) | ~ssRr(U_1, V_133)))). % 3.51/1.87 tff(c_34, plain, (![U_43, X_46, W_45, V_44]: (ssPv4(U_43) | ssPv3(X_46) | ssPv8(W_45) | ~ssRr(U_43, X_46) | ~ssRr(U_43, W_45) | ~ssPv7(V_44) | ~ssRr(U_43, V_44)))). % 3.51/1.87 tff(c_12, plain, (![U_10, W_12, V_11]: (ssPv8(U_10) | ssPv6(U_10) | ssPv5(W_12) | ~ssRr(U_10, W_12) | ~ssPv3(V_11) | ~ssRr(U_10, V_11)))). % 3.51/1.87 tff(c_147, plain, (![U_126]: (ssPv4(skf1(U_126)) | ~ssPv2(U_126) | ~ssPv6(U_126) | ~ssPv1(U_126) | ~ssPv3(skf1(U_126))))). % 3.51/1.87 tff(c_152, plain, (![U_1]: (ssPv5(U_1) | ssPv3(skf1(U_1)) | ssPv5(skf1(U_1)) | ~ssPv4(U_1)))). % 3.51/1.87 tff(c_139, plain, (![U_1, V_125]: (ssPv5(U_1) | ssPv3(skf1(U_1)) | ssPv5(V_125) | ~ssPv4(U_1) | ~ssRr(U_1, V_125)))). % 3.51/1.87 tff(c_135, plain, (![U_1]: (ssPv7(skf1(U_1)) | ~ssPv6(U_1) | ~ssPv1(U_1) | ~ssPv3(skf1(U_1))))). % 3.51/1.88 tff(c_14, plain, (![U_13, W_15, V_14]: (ssPv5(U_13) | ssPv3(W_15) | ssPv5(V_14) | ~ssPv4(U_13) | ~ssRr(U_13, W_15) | ~ssRr(U_13, V_14)))). % 3.51/1.88 tff(c_131, plain, (![U_1, V_120]: (ssPv7(skf1(U_1)) | ~ssPv6(U_1) | ~ssPv1(U_1) | ~ssPv3(V_120) | ~ssRr(U_1, V_120)))). % 3.51/1.88 tff(c_24, plain, (![W_30, U_28, V_29]: (ssPv7(W_30) | ~ssPv6(U_28) | ~ssPv1(U_28) | ~ssRr(U_28, W_30) | ~ssPv3(V_29) | ~ssRr(U_28, V_29)))). % 3.51/1.88 tff(c_123, plain, (![U_1, V_115]: (ssPv7(U_1) | ~ssPv2(U_1) | ~ssPv2(skf1(U_1)) | ~ssPv5(V_115) | ~ssRr(U_1, V_115)))). % 3.51/1.88 tff(c_30, plain, (![U_37, W_39, V_38]: (ssPv7(U_37) | ~ssPv2(U_37) | ~ssPv2(W_39) | ~ssRr(U_37, W_39) | ~ssPv5(V_38) | ~ssRr(U_37, V_38)))). % 3.51/1.88 tff(c_115, plain, (![U_1, V_110]: (ssPv8(U_1) | ~ssPv1(U_1) | ~ssPv2(skf1(U_1)) | ~ssPv3(V_110) | ~ssRr(U_1, V_110)))). % 3.51/1.88 tff(c_28, plain, (![U_34, W_36, V_35]: (ssPv8(U_34) | ~ssPv1(U_34) | ~ssPv2(W_36) | ~ssRr(U_34, W_36) | ~ssPv3(V_35) | ~ssRr(U_34, V_35)))). % 3.51/1.88 tff(c_110, plain, (![U_1]: (ssPv4(skf1(U_1)) | ~ssPv2(U_1) | ~ssPv1(U_1) | ~ssPv7(skf1(U_1))))). % 3.51/1.88 tff(c_105, plain, (![U_1, V_102]: (ssPv4(skf1(U_1)) | ~ssPv2(U_1) | ~ssPv1(U_1) | ~ssPv7(V_102) | ~ssRr(U_1, V_102)))). % 3.51/1.88 tff(c_101, plain, (![U_1, V_99]: (~ssPv8(U_1) | ~ssPv4(U_1) | ~ssPv3(skf1(U_1)) | ~ssPv4(V_99) | ~ssRr(U_1, V_99)))). % 3.51/1.88 tff(c_26, plain, (![W_33, U_31, V_32]: (ssPv4(W_33) | ~ssPv2(U_31) | ~ssPv1(U_31) | ~ssRr(U_31, W_33) | ~ssPv7(V_32) | ~ssRr(U_31, V_32)))). % 3.51/1.88 tff(c_32, plain, (![U_40, W_42, V_41]: (~ssPv8(U_40) | ~ssPv4(U_40) | ~ssPv3(W_42) | ~ssRr(U_40, W_42) | ~ssPv4(V_41) | ~ssRr(U_40, V_41)))). % 3.51/1.88 tff(c_96, plain, (![U_1]: (ssPv8(skf1(U_1)) | ~ssPv8(U_1) | ~ssPv3(U_1) | ~ssPv7(skf1(U_1))))). % 3.51/1.88 tff(c_92, plain, (![U_1, V_93]: (ssPv8(skf1(U_1)) | ~ssPv8(U_1) | ~ssPv3(U_1) | ~ssPv7(V_93) | ~ssRr(U_1, V_93)))). % 3.51/1.88 tff(c_20, plain, (![W_24, U_22, V_23]: (ssPv8(W_24) | ~ssPv8(U_22) | ~ssPv3(U_22) | ~ssRr(U_22, W_24) | ~ssPv7(V_23) | ~ssRr(U_22, V_23)))). % 3.51/1.88 tff(c_84, plain, (![U_1, V_88]: (ssPv6(skf1(U_1)) | ~ssPv5(U_1) | ~ssPv4(U_1) | ~ssPv6(V_88) | ~ssRr(U_1, V_88)))). % 3.51/1.88 tff(c_18, plain, (![W_21, U_19, V_20]: (ssPv6(W_21) | ~ssPv5(U_19) | ~ssPv4(U_19) | ~ssRr(U_19, W_21) | ~ssPv6(V_20) | ~ssRr(U_19, V_20)))). % 3.51/1.88 tff(c_79, plain, (![U_1, V_83]: (ssPv7(U_1) | ssPv5(U_1) | ~ssPv4(skf1(U_1)) | ~ssPv8(V_83) | ~ssRr(U_1, V_83)))). % 3.51/1.88 tff(c_16, plain, (![U_16, W_18, V_17]: (ssPv7(U_16) | ssPv5(U_16) | ~ssPv4(W_18) | ~ssRr(U_16, W_18) | ~ssPv8(V_17) | ~ssRr(U_16, V_17)))). % 3.51/1.88 tff(c_71, plain, (![U_1, V_78]: (ssPv7(skf1(U_1)) | ~ssPv8(U_1) | ~ssPv3(U_1) | ~ssPv7(V_78) | ~ssRr(U_1, V_78)))). % 3.51/1.88 tff(c_22, plain, (![W_27, U_25, V_26]: (ssPv7(W_27) | ~ssPv8(U_25) | ~ssPv3(U_25) | ~ssRr(U_25, W_27) | ~ssPv7(V_26) | ~ssRr(U_25, V_26)))). % 3.51/1.88 tff(c_66, plain, (![U_1]: (ssPv5(U_1) | ssPv4(U_1) | ~ssPv8(U_1) | ~ssPv3(skf1(U_1))))). % 3.51/1.88 tff(c_4, plain, (![U_2, V_3]: (ssPv5(U_2) | ssPv4(U_2) | ~ssPv8(U_2) | ~ssPv3(V_3) | ~ssRr(U_2, V_3)))). % 3.51/1.88 tff(c_60, plain, (![U_1]: (ssPv7(U_1) | ssPv1(U_1) | ~ssPv2(U_1) | ~ssPv3(skf1(U_1))))). % 3.51/1.88 tff(c_8, plain, (![U_6, V_7]: (ssPv7(U_6) | ssPv1(U_6) | ~ssPv2(U_6) | ~ssPv3(V_7) | ~ssRr(U_6, V_7)))). % 3.51/1.88 tff(c_54, plain, (![U_1]: (ssPv2(U_1) | ssPv2(skf1(U_1)) | ~ssPv8(U_1) | ~ssPv5(U_1)))). % 3.51/1.88 tff(c_6, plain, (![U_4, V_5]: (ssPv2(U_4) | ssPv2(V_5) | ~ssPv8(U_4) | ~ssPv5(U_4) | ~ssRr(U_4, V_5)))). % 3.51/1.88 tff(c_48, plain, (![U_1]: (ssPv6(U_1) | ~ssPv4(U_1) | ~ssPv3(U_1) | ~ssPv7(skf1(U_1))))). % 3.51/1.88 tff(c_10, plain, (![U_8, V_9]: (ssPv6(U_8) | ~ssPv4(U_8) | ~ssPv3(U_8) | ~ssPv7(V_9) | ~ssRr(U_8, V_9)))). % 3.51/1.88 tff(c_2, plain, (![U_1]: (ssRr(U_1, skf1(U_1))))). % 3.51/1.88 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 3.51/1.88 %------------------------------------------------------------------------------