%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SYN734-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 : n023.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:19 PM UTC 2025 % Result : Satisfiable 4.24s 2.07s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SYN734-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.13/0.34 % Computer : n023.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 08:13:54 EDT 2025 % 0.13/0.34 % CPUTime : % 4.24/2.06 % 4.24/2.07 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 4.60/2.07 % 4.60/2.07 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 4.60/2.07 %$ ssRr > ssPv4 > ssPv3 > ssPv2 > ssPv1 > #nlpp > skf1 % 4.60/2.07 % 4.60/2.07 %Foreground sorts: % 4.60/2.07 % 4.60/2.07 % 4.60/2.07 %Background operators: % 4.60/2.07 % 4.60/2.07 % 4.60/2.07 %Foreground operators: % 4.60/2.07 tff(skf1, type, skf1: $i > $i). % 4.60/2.07 tff(ssPv1, type, ssPv1: $i > $o). % 4.60/2.07 tff(ssPv3, type, ssPv3: $i > $o). % 4.60/2.07 tff(ssRr, type, ssRr: ($i * $i) > $o). % 4.60/2.07 tff(ssPv4, type, ssPv4: $i > $o). % 4.60/2.07 tff(ssPv2, type, ssPv2: $i > $o). % 4.60/2.07 % 4.60/2.07 %Saturated clause set: % 4.60/2.08 tff(c_127, plain, (![U_1]: (ssPv2(skf1(U_1)) | ~ssPv3(skf1(U_1)) | ~ssPv1(skf1(U_1)) | ~ssPv4(U_1) | ~ssPv3(U_1) | ~ssPv1(U_1)))). % 4.60/2.08 tff(c_596, plain, (![U_1]: (~ssPv3(U_1) | ~ssPv1(U_1) | ~ssPv4(U_1) | ~ssPv1(skf1(U_1)) | ~ssPv2(skf1(U_1))))). % 4.60/2.08 tff(c_559, plain, (![U_1]: (ssPv2(U_1) | ~ssPv4(skf1(U_1)) | ssPv1(U_1) | ssPv1(skf1(U_1)) | ~ssPv4(U_1)))). % 4.60/2.08 tff(c_493, plain, (![U_195, V_101]: (ssPv2(U_195) | ~ssPv4(V_101) | ~ssRr(U_195, V_101) | ssPv1(U_195) | ssPv1(skf1(U_195)) | ~ssPv4(U_195)))). % 4.65/2.08 tff(c_518, plain, (![U_1]: (ssPv3(skf1(U_1)) | ssPv1(skf1(U_1)) | ssPv4(U_1) | ssPv1(U_1) | ssPv2(skf1(U_1))))). % 4.65/2.08 tff(c_479, plain, (![U_194]: (ssPv2(U_194) | ~ssPv1(U_194) | ssPv1(skf1(U_194)) | ssPv3(skf1(U_194)) | ~ssPv4(U_194)))). % 4.65/2.08 tff(c_517, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv1(skf1(U_1)) | ssPv3(skf1(U_1)) | ~ssPv4(U_1)))). % 4.65/2.08 tff(c_504, plain, (![U_196]: (ssPv3(U_196) | ssPv2(U_196) | ssPv1(U_196) | ~ssPv4(U_196)))). % 4.65/2.08 tff(c_477, plain, (![U_194]: (ssPv1(U_194) | ssPv1(skf1(U_194)) | ssPv3(skf1(U_194)) | ~ssPv4(U_194)))). % 4.65/2.08 tff(c_449, plain, (![U_1]: (ssPv1(skf1(U_1)) | ssPv3(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv4(U_1)))). % 4.65/2.08 tff(c_445, plain, (![U_1, V_191]: (ssPv1(skf1(U_1)) | ssPv3(skf1(U_1)) | ssPv4(V_191) | ~ssPv4(U_1) | ~ssRr(U_1, V_191)))). % 4.65/2.08 tff(c_382, plain, (![U_1, W_175, V_176]: (ssPv1(skf1(U_1)) | ssPv3(W_175) | ssPv4(V_176) | ~ssPv4(U_1) | ~ssRr(U_1, W_175) | ~ssRr(U_1, V_176)))). % 4.65/2.08 tff(c_423, plain, (![U_1, V_184]: (ssPv1(U_1) | ssPv3(skf1(U_1)) | ~ssPv1(skf1(U_1)) | ~ssPv3(V_184) | ~ssRr(U_1, V_184)))). % 4.65/2.08 tff(c_428, plain, (![U_1]: (~ssPv4(U_1) | ssPv3(U_1) | ~ssPv2(U_1) | ~ssPv1(U_1)))). % 4.65/2.08 tff(c_361, plain, (![U_1, W_163, V_164]: (ssPv1(U_1) | ssPv3(skf1(U_1)) | ~ssPv1(W_163) | ~ssRr(U_1, W_163) | ~ssPv3(V_164) | ~ssRr(U_1, V_164)))). % 4.65/2.08 tff(c_386, plain, (![U_1]: (ssPv3(skf1(U_1)) | ~ssPv4(U_1) | ~ssPv1(skf1(U_1)) | ~ssPv2(skf1(U_1))))). % 4.65/2.08 tff(c_378, plain, (![U_1, V_173]: (ssPv3(skf1(U_1)) | ~ssPv4(U_1) | ~ssPv1(skf1(U_1)) | ~ssPv2(V_173) | ~ssRr(U_1, V_173)))). % 4.65/2.08 tff(c_36, plain, (![X_47, W_46, V_45, U_44]: (ssPv1(X_47) | ssPv3(W_46) | ssPv4(V_45) | ~ssPv4(U_44) | ~ssRr(U_44, X_47) | ~ssRr(U_44, W_46) | ~ssRr(U_44, V_45)))). % 4.65/2.08 tff(c_291, plain, (![U_1, W_148, V_149]: (ssPv3(skf1(U_1)) | ~ssPv4(U_1) | ~ssPv1(W_148) | ~ssRr(U_1, W_148) | ~ssPv2(V_149) | ~ssRr(U_1, V_149)))). % 4.65/2.08 tff(c_370, plain, (![U_1, V_168]: (ssPv3(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv4(U_1) | ~ssPv4(V_168) | ~ssRr(U_1, V_168)))). % 4.65/2.08 tff(c_338, plain, (![U_1, W_155, V_157]: (ssPv3(skf1(U_1)) | ssPv4(W_155) | ~ssPv4(U_1) | ~ssRr(U_1, W_155) | ~ssPv4(V_157) | ~ssRr(U_1, V_157)))). % 4.65/2.08 tff(c_357, plain, (![U_160]: (ssPv1(U_160) | ~ssPv4(U_160) | ~ssPv1(skf1(U_160))))). % 4.65/2.08 tff(c_40, plain, (![U_52, X_55, W_54, V_53]: (ssPv1(U_52) | ssPv3(X_55) | ~ssRr(U_52, X_55) | ~ssPv1(W_54) | ~ssRr(U_52, W_54) | ~ssPv3(V_53) | ~ssRr(U_52, V_53)))). % 4.65/2.08 tff(c_38, plain, (![X_51, W_50, U_48, V_49]: (ssPv3(X_51) | ssPv4(W_50) | ~ssPv4(U_48) | ~ssRr(U_48, X_51) | ~ssRr(U_48, W_50) | ~ssPv4(V_49) | ~ssRr(U_48, V_49)))). % 4.65/2.08 tff(c_304, plain, (![U_150]: (~ssPv1(skf1(U_150)) | ssPv3(U_150) | ssPv4(U_150) | ssPv1(U_150) | ssPv2(skf1(U_150))))). % 4.65/2.08 tff(c_223, plain, (![U_1]: (ssPv3(U_1) | ssPv3(skf1(U_1)) | ssPv4(U_1) | ssPv1(U_1) | ssPv2(skf1(U_1))))). % 4.65/2.08 tff(c_42, plain, (![X_59, U_56, W_58, V_57]: (ssPv3(X_59) | ~ssPv4(U_56) | ~ssRr(U_56, X_59) | ~ssPv1(W_58) | ~ssRr(U_56, W_58) | ~ssPv2(V_57) | ~ssRr(U_56, V_57)))). % 4.65/2.08 tff(c_286, plain, (![U_1]: (ssPv2(skf1(U_1)) | ~ssPv4(U_1) | ~ssPv2(U_1) | ~ssPv1(skf1(U_1))))). % 4.65/2.08 tff(c_277, plain, (![U_1, V_141]: (ssPv2(skf1(U_1)) | ~ssPv4(U_1) | ~ssPv2(U_1) | ~ssPv1(V_141) | ~ssRr(U_1, V_141)))). % 4.65/2.08 tff(c_32, plain, (![W_40, U_38, V_39]: (ssPv2(W_40) | ~ssPv4(U_38) | ~ssPv2(U_38) | ~ssRr(U_38, W_40) | ~ssPv1(V_39) | ~ssRr(U_38, V_39)))). % 4.65/2.08 tff(c_211, plain, (![U_1, V_131]: (ssPv1(U_1) | ssPv4(skf1(U_1)) | ~ssPv4(U_1) | ~ssPv1(V_131) | ~ssRr(U_1, V_131)))). % 4.65/2.08 tff(c_215, plain, (![U_1]: (ssPv3(U_1) | ssPv1(U_1) | ssPv3(skf1(U_1)) | ~ssPv4(skf1(U_1))))). % 4.65/2.08 tff(c_207, plain, (![U_1, V_128]: (ssPv3(U_1) | ssPv1(U_1) | ssPv3(skf1(U_1)) | ~ssPv4(V_128) | ~ssRr(U_1, V_128)))). % 4.65/2.08 tff(c_26, plain, (![U_29, W_31, V_30]: (ssPv1(U_29) | ssPv4(W_31) | ~ssPv4(U_29) | ~ssRr(U_29, W_31) | ~ssPv1(V_30) | ~ssRr(U_29, V_30)))). % 4.65/2.08 tff(c_20, plain, (![U_20, W_22, V_21]: (ssPv3(U_20) | ssPv1(U_20) | ssPv3(W_22) | ~ssRr(U_20, W_22) | ~ssPv4(V_21) | ~ssRr(U_20, V_21)))). % 4.65/2.08 tff(c_194, plain, (![U_1]: (ssPv1(U_1) | ssPv3(skf1(U_1)) | ~ssPv4(U_1) | ~ssPv4(skf1(U_1))))). % 4.65/2.09 tff(c_190, plain, (![U_1, V_122]: (ssPv1(U_1) | ssPv3(skf1(U_1)) | ~ssPv4(U_1) | ~ssPv4(V_122) | ~ssRr(U_1, V_122)))). % 4.65/2.09 tff(c_28, plain, (![U_32, W_34, V_33]: (ssPv1(U_32) | ssPv3(W_34) | ~ssPv4(U_32) | ~ssRr(U_32, W_34) | ~ssPv4(V_33) | ~ssRr(U_32, V_33)))). % 4.65/2.09 tff(c_166, plain, (![U_109]: (~ssPv3(skf1(U_109)) | ~ssPv1(skf1(U_109)) | ssPv4(U_109) | ssPv1(U_109) | ssPv2(skf1(U_109))))). % 4.65/2.09 tff(c_174, plain, (![U_1, V_112]: (~ssPv4(U_1) | ~ssPv2(U_1) | ~ssPv1(skf1(U_1)) | ~ssPv3(V_112) | ~ssRr(U_1, V_112)))). % 4.65/2.09 tff(c_169, plain, (![U_109]: (ssPv2(U_109) | ssPv4(U_109) | ssPv1(U_109) | ssPv2(skf1(U_109))))). % 4.65/2.09 tff(c_34, plain, (![U_41, W_43, V_42]: (~ssPv4(U_41) | ~ssPv2(U_41) | ~ssPv1(W_43) | ~ssRr(U_41, W_43) | ~ssPv3(V_42) | ~ssRr(U_41, V_42)))). % 4.65/2.09 tff(c_149, plain, (![U_1]: (ssPv4(U_1) | ssPv1(U_1) | ssPv2(skf1(U_1)) | ssPv4(skf1(U_1))))). % 4.65/2.09 tff(c_144, plain, (![U_1, V_104]: (ssPv4(U_1) | ssPv1(U_1) | ssPv2(skf1(U_1)) | ssPv4(V_104) | ~ssRr(U_1, V_104)))). % 4.65/2.09 tff(c_140, plain, (![U_1, V_101]: (ssPv2(U_1) | ssPv1(U_1) | ~ssPv3(skf1(U_1)) | ~ssPv4(V_101) | ~ssRr(U_1, V_101)))). % 4.65/2.09 tff(c_16, plain, (![U_14, W_16, V_15]: (ssPv4(U_14) | ssPv1(U_14) | ssPv2(W_16) | ssPv4(V_15) | ~ssRr(U_14, W_16) | ~ssRr(U_14, V_15)))). % 4.65/2.09 tff(c_30, plain, (![U_35, W_37, V_36]: (ssPv2(U_35) | ssPv1(U_35) | ~ssPv3(W_37) | ~ssRr(U_35, W_37) | ~ssPv4(V_36) | ~ssRr(U_35, V_36)))). % 4.65/2.09 tff(c_122, plain, (![U_1, V_92]: (ssPv3(U_1) | ssPv3(skf1(U_1)) | ~ssPv1(U_1) | ~ssPv3(V_92) | ~ssRr(U_1, V_92)))). % 4.65/2.09 tff(c_131, plain, (![U_1]: (ssPv4(U_1) | ssPv1(skf1(U_1)) | ssPv2(skf1(U_1)) | ~ssPv2(U_1)))). % 4.65/2.09 tff(c_104, plain, (![U_1, V_85]: (ssPv4(U_1) | ssPv1(skf1(U_1)) | ssPv2(V_85) | ~ssPv2(U_1) | ~ssRr(U_1, V_85)))). % 4.65/2.09 tff(c_118, plain, (![U_89]: (ssPv2(U_89) | ~ssPv4(U_89) | ~ssPv3(U_89) | ~ssPv1(U_89)))). % 4.65/2.09 tff(c_22, plain, (![U_23, W_25, V_24]: (ssPv3(U_23) | ssPv3(W_25) | ~ssPv1(U_23) | ~ssRr(U_23, W_25) | ~ssPv3(V_24) | ~ssRr(U_23, V_24)))). % 4.65/2.09 tff(c_108, plain, (![U_1]: (ssPv2(U_1) | ssPv1(skf1(U_1)) | ~ssPv1(U_1) | ~ssPv4(skf1(U_1))))). % 4.65/2.09 tff(c_100, plain, (![U_1, V_82]: (ssPv2(U_1) | ssPv1(skf1(U_1)) | ~ssPv1(U_1) | ~ssPv4(V_82) | ~ssRr(U_1, V_82)))). % 4.65/2.09 tff(c_18, plain, (![U_17, W_19, V_18]: (ssPv4(U_17) | ssPv1(W_19) | ssPv2(V_18) | ~ssPv2(U_17) | ~ssRr(U_17, W_19) | ~ssRr(U_17, V_18)))). % 4.65/2.09 tff(c_24, plain, (![U_26, W_28, V_27]: (ssPv2(U_26) | ssPv1(W_28) | ~ssPv1(U_26) | ~ssRr(U_26, W_28) | ~ssPv4(V_27) | ~ssRr(U_26, V_27)))). % 4.65/2.09 tff(c_91, plain, (![U_1]: (ssPv2(U_1) | ~ssPv4(U_1) | ~ssPv3(U_1) | ~ssPv1(skf1(U_1))))). % 4.65/2.09 tff(c_12, plain, (![U_10, V_11]: (ssPv2(U_10) | ~ssPv4(U_10) | ~ssPv3(U_10) | ~ssPv1(V_11) | ~ssRr(U_10, V_11)))). % 4.65/2.09 tff(c_84, plain, (![U_1]: (ssPv3(U_1) | ssPv2(U_1) | ssPv1(U_1) | ~ssPv3(skf1(U_1))))). % 4.65/2.09 tff(c_79, plain, (![U_1]: (ssPv3(U_1) | ssPv1(skf1(U_1)) | ~ssPv2(U_1) | ~ssPv1(U_1)))). % 4.65/2.09 tff(c_6, plain, (![U_4, V_5]: (ssPv3(U_4) | ssPv2(U_4) | ssPv1(U_4) | ~ssPv3(V_5) | ~ssRr(U_4, V_5)))). % 4.65/2.09 tff(c_8, plain, (![U_6, V_7]: (ssPv3(U_6) | ssPv1(V_7) | ~ssPv2(U_6) | ~ssPv1(U_6) | ~ssRr(U_6, V_7)))). % 4.65/2.09 tff(c_69, plain, (![U_69]: (~ssPv2(U_69) | ~ssPv4(U_69) | ~ssPv3(U_69) | ~ssPv1(U_69)))). % 4.65/2.09 tff(c_60, plain, (![U_1]: (ssPv4(skf1(U_1)) | ~ssPv4(U_1) | ~ssPv3(U_1) | ~ssPv1(U_1)))). % 4.65/2.09 tff(c_10, plain, (![V_9, U_8]: (ssPv4(V_9) | ~ssPv4(U_8) | ~ssPv3(U_8) | ~ssPv1(U_8) | ~ssRr(U_8, V_9)))). % 4.65/2.09 tff(c_54, plain, (![U_1]: (ssPv4(U_1) | ssPv2(U_1) | ssPv1(U_1) | ~ssPv4(skf1(U_1))))). % 4.65/2.09 tff(c_4, plain, (![U_2, V_3]: (ssPv4(U_2) | ssPv2(U_2) | ssPv1(U_2) | ~ssPv4(V_3) | ~ssRr(U_2, V_3)))). % 4.65/2.09 tff(c_48, plain, (![U_1]: (~ssPv3(U_1) | ~ssPv2(U_1) | ~ssPv1(U_1) | ~ssPv4(skf1(U_1))))). % 4.65/2.09 tff(c_14, plain, (![U_12, V_13]: (~ssPv3(U_12) | ~ssPv2(U_12) | ~ssPv1(U_12) | ~ssPv4(V_13) | ~ssRr(U_12, V_13)))). % 4.65/2.09 tff(c_2, plain, (![U_1]: (ssRr(U_1, skf1(U_1))))). % 4.65/2.09 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 4.65/2.09 %------------------------------------------------------------------------------