%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SYN740-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 : n031.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 5.34s 2.26s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.12 % Problem : SYN740-1 : TPTP v9.0.0. Released v2.5.0. % 0.08/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 : n031.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:52 EDT 2025 % 0.13/0.35 % CPUTime : % 5.34/2.26 % 5.34/2.26 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 5.34/2.26 % 5.34/2.26 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 5.34/2.27 %$ ssRr > ssPv4 > ssPv3 > ssPv2 > ssPv1 > #nlpp > skf1 % 5.34/2.27 % 5.34/2.27 %Foreground sorts: % 5.34/2.27 % 5.34/2.27 % 5.34/2.27 %Background operators: % 5.34/2.27 % 5.34/2.27 % 5.34/2.27 %Foreground operators: % 5.34/2.27 tff(skf1, type, skf1: $i > $i). % 5.34/2.27 tff(ssPv1, type, ssPv1: $i > $o). % 5.34/2.27 tff(ssPv3, type, ssPv3: $i > $o). % 5.34/2.27 tff(ssRr, type, ssRr: ($i * $i) > $o). % 5.34/2.27 tff(ssPv4, type, ssPv4: $i > $o). % 5.34/2.27 tff(ssPv2, type, ssPv2: $i > $o). % 5.34/2.27 % 5.34/2.27 %Saturated clause set: % 5.34/2.27 tff(c_652, plain, (![U_1]: (ssPv3(U_1) | ssPv2(U_1) | ~ssPv4(skf1(U_1)) | ssPv2(skf1(U_1)) | ~ssPv4(U_1) | ~ssPv1(U_1)))). % 5.34/2.27 tff(c_351, plain, (![U_1, V_213]: (ssPv3(U_1) | ssPv2(U_1) | ~ssPv4(V_213) | ~ssRr(U_1, V_213) | ssPv2(skf1(U_1)) | ~ssPv4(U_1) | ~ssPv1(U_1)))). % 5.34/2.27 tff(c_633, plain, (![U_1]: (~ssPv1(skf1(U_1)) | ~ssPv2(skf1(U_1)) | ssPv2(U_1) | ~ssPv3(U_1) | ~ssPv1(U_1)))). % 5.34/2.27 tff(c_606, plain, (![U_297]: (ssPv3(U_297) | ~ssPv1(U_297) | ~ssPv2(U_297) | ~ssPv1(skf1(U_297)) | ~ssPv2(skf1(U_297))))). % 5.34/2.27 tff(c_589, plain, (![U_1, V_294]: (ssPv1(U_1) | ssPv2(skf1(U_1)) | ~ssPv1(skf1(U_1)) | ~ssPv2(V_294) | ~ssRr(U_1, V_294)))). % 5.34/2.27 tff(c_585, plain, (![U_1, W_290, V_291]: (ssPv1(U_1) | ssPv2(skf1(U_1)) | ~ssPv1(W_290) | ~ssRr(U_1, W_290) | ~ssPv2(V_291) | ~ssRr(U_1, V_291)))). % 5.34/2.27 tff(c_54, plain, (![U_76, X_79, W_78, V_77]: (ssPv1(U_76) | ssPv2(X_79) | ~ssRr(U_76, X_79) | ~ssPv1(W_78) | ~ssRr(U_76, W_78) | ~ssPv2(V_77) | ~ssRr(U_76, V_77)))). % 5.34/2.27 tff(c_573, plain, (![U_286]: (ssPv4(U_286) | ~ssPv2(U_286) | ~ssPv1(skf1(U_286)) | ~ssPv2(skf1(U_286))))). % 5.34/2.27 tff(c_547, plain, (![U_1]: (ssPv4(U_1) | ssPv3(skf1(U_1)) | ~ssPv2(skf1(U_1)) | ~ssPv4(skf1(U_1))))). % 5.34/2.27 tff(c_543, plain, (![U_1, V_282]: (ssPv4(U_1) | ssPv3(skf1(U_1)) | ~ssPv2(skf1(U_1)) | ~ssPv4(V_282) | ~ssRr(U_1, V_282)))). % 5.34/2.27 tff(c_539, plain, (![U_1, W_278, V_279]: (ssPv4(U_1) | ssPv3(skf1(U_1)) | ~ssPv2(W_278) | ~ssRr(U_1, W_278) | ~ssPv4(V_279) | ~ssRr(U_1, V_279)))). % 5.34/2.27 tff(c_50, plain, (![U_68, X_71, W_70, V_69]: (ssPv4(U_68) | ssPv3(X_71) | ~ssRr(U_68, X_71) | ~ssPv2(W_70) | ~ssRr(U_68, W_70) | ~ssPv4(V_69) | ~ssRr(U_68, V_69)))). % 5.34/2.27 tff(c_531, plain, (![U_1, V_273]: (ssPv4(skf1(U_1)) | ~ssPv1(U_1) | ~ssPv3(skf1(U_1)) | ~ssPv4(V_273) | ~ssRr(U_1, V_273)))). % 5.34/2.27 tff(c_523, plain, (![U_1, W_266, V_267]: (ssPv4(skf1(U_1)) | ~ssPv1(U_1) | ~ssPv3(W_266) | ~ssRr(U_1, W_266) | ~ssPv4(V_267) | ~ssRr(U_1, V_267)))). % 5.34/2.27 tff(c_463, plain, (![U_1, W_257, V_258]: (ssPv1(skf1(U_1)) | ~ssPv1(U_1) | ~ssPv1(W_257) | ~ssRr(U_1, W_257) | ~ssPv2(V_258) | ~ssRr(U_1, V_258)))). % 5.34/2.27 tff(c_58, plain, (![X_87, U_84, W_86, V_85]: (ssPv4(X_87) | ~ssPv1(U_84) | ~ssRr(U_84, X_87) | ~ssPv3(W_86) | ~ssRr(U_84, W_86) | ~ssPv4(V_85) | ~ssRr(U_84, V_85)))). % 5.34/2.27 tff(c_511, plain, (![U_262]: (~ssPv3(U_262) | ~ssPv2(U_262) | ~ssPv1(skf1(U_262)) | ~ssPv2(skf1(U_262))))). % 5.34/2.28 tff(c_457, plain, (![U_254]: (~ssPv3(skf1(U_254)) | ~ssPv2(U_254) | ~ssPv1(skf1(U_254)) | ~ssPv2(skf1(U_254))))). % 5.34/2.28 tff(c_60, plain, (![X_91, U_88, W_90, V_89]: (ssPv1(X_91) | ~ssPv1(U_88) | ~ssRr(U_88, X_91) | ~ssPv1(W_90) | ~ssRr(U_88, W_90) | ~ssPv2(V_89) | ~ssRr(U_88, V_89)))). % 5.34/2.28 tff(c_434, plain, (![U_1]: (ssPv4(skf1(U_1)) | ~ssPv2(U_1) | ~ssPv1(skf1(U_1)) | ~ssPv2(skf1(U_1))))). % 5.34/2.28 tff(c_430, plain, (![U_1, V_251]: (ssPv4(skf1(U_1)) | ~ssPv2(U_1) | ~ssPv1(skf1(U_1)) | ~ssPv2(V_251) | ~ssRr(U_1, V_251)))). % 5.34/2.28 tff(c_426, plain, (![U_1, W_247, V_248]: (ssPv4(skf1(U_1)) | ~ssPv2(U_1) | ~ssPv1(W_247) | ~ssRr(U_1, W_247) | ~ssPv2(V_248) | ~ssRr(U_1, V_248)))). % 5.34/2.28 tff(c_62, plain, (![X_95, U_92, W_94, V_93]: (ssPv4(X_95) | ~ssPv2(U_92) | ~ssRr(U_92, X_95) | ~ssPv1(W_94) | ~ssRr(U_92, W_94) | ~ssPv2(V_93) | ~ssRr(U_92, V_93)))). % 5.34/2.28 tff(c_418, plain, (![U_1, V_242]: (ssPv3(skf1(U_1)) | ~ssPv2(U_1) | ~ssPv2(skf1(U_1)) | ~ssPv3(V_242) | ~ssRr(U_1, V_242)))). % 5.34/2.28 tff(c_372, plain, (![U_1, W_226, V_227]: (ssPv3(skf1(U_1)) | ~ssPv2(U_1) | ~ssPv2(W_226) | ~ssRr(U_1, W_226) | ~ssPv3(V_227) | ~ssRr(U_1, V_227)))). % 5.34/2.28 tff(c_397, plain, (![U_1, W_232, V_233]: (ssPv3(U_1) | ssPv1(skf1(U_1)) | ~ssPv1(W_232) | ~ssRr(U_1, W_232) | ~ssPv3(V_233) | ~ssRr(U_1, V_233)))). % 5.34/2.28 tff(c_401, plain, (![U_1]: (~ssPv4(skf1(U_1)) | ssPv1(skf1(U_1)) | ~ssPv2(U_1) | ~ssPv4(U_1) | ~ssPv1(U_1)))). % 5.34/2.28 tff(c_168, plain, (![V_147, U_1]: (~ssPv4(V_147) | ~ssRr(U_1, V_147) | ssPv1(skf1(U_1)) | ~ssPv2(U_1) | ~ssPv4(U_1) | ~ssPv1(U_1)))). % 5.34/2.28 tff(c_52, plain, (![U_72, X_75, W_74, V_73]: (ssPv3(U_72) | ssPv1(X_75) | ~ssRr(U_72, X_75) | ~ssPv1(W_74) | ~ssRr(U_72, W_74) | ~ssPv3(V_73) | ~ssRr(U_72, V_73)))). % 5.34/2.28 tff(c_381, plain, (![U_1]: (ssPv3(skf1(U_1)) | ssPv2(U_1) | ~ssPv3(U_1) | ~ssPv1(U_1)))). % 5.34/2.28 tff(c_368, plain, (![U_1]: (ssPv2(U_1) | ssPv3(skf1(U_1)) | ~ssPv1(U_1) | ~ssPv4(skf1(U_1))))). % 5.34/2.28 tff(c_56, plain, (![X_83, U_80, W_82, V_81]: (ssPv3(X_83) | ~ssPv2(U_80) | ~ssRr(U_80, X_83) | ~ssPv2(W_82) | ~ssRr(U_80, W_82) | ~ssPv3(V_81) | ~ssRr(U_80, V_81)))). % 5.34/2.28 tff(c_364, plain, (![U_1, V_221]: (ssPv2(U_1) | ssPv3(skf1(U_1)) | ~ssPv1(U_1) | ~ssPv4(V_221) | ~ssRr(U_1, V_221)))). % 5.34/2.28 tff(c_28, plain, (![U_35, W_37, V_36]: (ssPv2(U_35) | ssPv3(W_37) | ~ssPv1(U_35) | ~ssRr(U_35, W_37) | ~ssPv4(V_36) | ~ssRr(U_35, V_36)))). % 5.34/2.28 tff(c_356, plain, (![U_1, V_216]: (ssPv4(U_1) | ssPv1(skf1(U_1)) | ~ssPv3(U_1) | ~ssPv1(V_216) | ~ssRr(U_1, V_216)))). % 5.34/2.28 tff(c_16, plain, (![U_17, W_19, V_18]: (ssPv4(U_17) | ssPv1(W_19) | ~ssPv3(U_17) | ~ssRr(U_17, W_19) | ~ssPv1(V_18) | ~ssRr(U_17, V_18)))). % 5.34/2.28 tff(c_336, plain, (![U_1, V_211]: (ssPv3(U_1) | ssPv2(U_1) | ~ssPv3(skf1(U_1)) | ~ssPv4(V_211) | ~ssRr(U_1, V_211)))). % 5.34/2.28 tff(c_30, plain, (![U_38, W_40, V_39]: (ssPv3(U_38) | ssPv2(U_38) | ~ssPv3(W_40) | ~ssRr(U_38, W_40) | ~ssPv4(V_39) | ~ssRr(U_38, V_39)))). % 5.34/2.28 tff(c_328, plain, (![U_1, V_206]: (ssPv3(U_1) | ssPv1(skf1(U_1)) | ~ssPv2(U_1) | ~ssPv1(V_206) | ~ssRr(U_1, V_206)))). % 5.34/2.28 tff(c_20, plain, (![U_23, W_25, V_24]: (ssPv3(U_23) | ssPv1(W_25) | ~ssPv2(U_23) | ~ssRr(U_23, W_25) | ~ssPv1(V_24) | ~ssRr(U_23, V_24)))). % 5.34/2.28 tff(c_317, plain, (![U_1, V_201]: (ssPv2(U_1) | ~ssPv1(U_1) | ~ssPv1(skf1(U_1)) | ~ssPv4(V_201) | ~ssRr(U_1, V_201)))). % 5.34/2.28 tff(c_44, plain, (![U_59, W_61, V_60]: (ssPv2(U_59) | ~ssPv1(U_59) | ~ssPv1(W_61) | ~ssRr(U_59, W_61) | ~ssPv4(V_60) | ~ssRr(U_59, V_60)))). % 5.34/2.28 tff(c_292, plain, (![U_1]: (ssPv1(skf1(U_1)) | ~ssPv3(U_1) | ~ssPv2(U_1) | ~ssPv3(skf1(U_1))))). % 5.34/2.28 tff(c_288, plain, (![U_1, V_195]: (ssPv1(skf1(U_1)) | ~ssPv3(U_1) | ~ssPv2(U_1) | ~ssPv3(V_195) | ~ssRr(U_1, V_195)))). % 5.34/2.28 tff(c_38, plain, (![W_52, U_50, V_51]: (ssPv1(W_52) | ~ssPv3(U_50) | ~ssPv2(U_50) | ~ssRr(U_50, W_52) | ~ssPv3(V_51) | ~ssRr(U_50, V_51)))). % 5.34/2.28 tff(c_275, plain, (![U_1]: (ssPv3(U_1) | ssPv3(skf1(U_1)) | ~ssPv1(U_1) | ~ssPv4(skf1(U_1))))). % 5.34/2.28 tff(c_271, plain, (![U_1, V_189]: (ssPv3(U_1) | ssPv3(skf1(U_1)) | ~ssPv1(U_1) | ~ssPv4(V_189) | ~ssRr(U_1, V_189)))). % 5.34/2.28 tff(c_22, plain, (![U_26, W_28, V_27]: (ssPv3(U_26) | ssPv3(W_28) | ~ssPv1(U_26) | ~ssRr(U_26, W_28) | ~ssPv4(V_27) | ~ssRr(U_26, V_27)))). % 5.34/2.28 tff(c_262, plain, (![U_1]: (ssPv4(U_1) | ssPv3(skf1(U_1)) | ~ssPv1(U_1) | ~ssPv1(skf1(U_1))))). % 5.34/2.28 tff(c_254, plain, (![U_1, V_181]: (ssPv4(U_1) | ssPv3(skf1(U_1)) | ~ssPv1(U_1) | ~ssPv1(V_181) | ~ssRr(U_1, V_181)))). % 5.34/2.28 tff(c_250, plain, (![U_1, V_178]: (ssPv4(U_1) | ssPv3(U_1) | ~ssPv2(skf1(U_1)) | ~ssPv4(V_178) | ~ssRr(U_1, V_178)))). % 5.34/2.28 tff(c_18, plain, (![U_20, W_22, V_21]: (ssPv4(U_20) | ssPv3(W_22) | ~ssPv1(U_20) | ~ssRr(U_20, W_22) | ~ssPv1(V_21) | ~ssRr(U_20, V_21)))). % 5.34/2.28 tff(c_26, plain, (![U_32, W_34, V_33]: (ssPv4(U_32) | ssPv3(U_32) | ~ssPv2(W_34) | ~ssRr(U_32, W_34) | ~ssPv4(V_33) | ~ssRr(U_32, V_33)))). % 5.34/2.28 tff(c_241, plain, (![U_1]: (~ssPv2(skf1(U_1)) | ssPv3(U_1) | ~ssPv2(U_1) | ~ssPv4(U_1) | ~ssPv1(U_1)))). % 5.34/2.28 tff(c_180, plain, (![V_155, U_141]: (~ssPv2(V_155) | ~ssRr(U_141, V_155) | ssPv3(U_141) | ~ssPv2(U_141) | ~ssPv4(U_141) | ~ssPv1(U_141)))). % 5.34/2.28 tff(c_232, plain, (![U_1, V_170]: (ssPv2(U_1) | ~ssPv4(U_1) | ~ssPv2(skf1(U_1)) | ~ssPv4(V_170) | ~ssRr(U_1, V_170)))). % 5.34/2.28 tff(c_42, plain, (![U_56, W_58, V_57]: (ssPv2(U_56) | ~ssPv4(U_56) | ~ssPv2(W_58) | ~ssRr(U_56, W_58) | ~ssPv4(V_57) | ~ssRr(U_56, V_57)))). % 5.34/2.28 tff(c_192, plain, (![U_158]: (ssPv1(U_158) | ssPv2(skf1(U_158)) | ssPv3(skf1(U_158)) | ~ssPv4(U_158) | ~ssPv3(U_158)))). % 5.34/2.28 tff(c_210, plain, (![U_1, V_163]: (ssPv1(skf1(U_1)) | ~ssPv3(U_1) | ~ssPv2(U_1) | ~ssPv1(V_163) | ~ssRr(U_1, V_163)))). % 5.34/2.28 tff(c_206, plain, (![U_160]: (~ssPv1(U_160) | ~ssPv2(U_160) | ~ssPv4(U_160) | ~ssPv3(U_160)))). % 5.34/2.28 tff(c_40, plain, (![W_55, U_53, V_54]: (ssPv1(W_55) | ~ssPv3(U_53) | ~ssPv2(U_53) | ~ssRr(U_53, W_55) | ~ssPv1(V_54) | ~ssRr(U_53, V_54)))). % 5.34/2.28 tff(c_198, plain, (![U_159]: (ssPv1(skf1(U_159)) | ~ssPv2(U_159) | ~ssPv4(U_159) | ~ssPv3(U_159)))). % 5.34/2.28 tff(c_193, plain, (![U_158]: (~ssPv2(U_158) | ssPv3(skf1(U_158)) | ~ssPv4(U_158) | ~ssPv3(U_158)))). % 5.34/2.28 tff(c_184, plain, (![U_1]: (ssPv3(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv4(U_1) | ~ssPv3(U_1)))). % 5.34/2.28 tff(c_176, plain, (![U_1, V_152]: (ssPv3(skf1(U_1)) | ssPv4(V_152) | ~ssPv4(U_1) | ~ssPv3(U_1) | ~ssRr(U_1, V_152)))). % 5.34/2.28 tff(c_172, plain, (![U_1, V_150]: (~ssPv2(U_1) | ~ssPv1(U_1) | ~ssPv1(skf1(U_1)) | ~ssPv2(V_150) | ~ssRr(U_1, V_150)))). % 5.34/2.28 tff(c_10, plain, (![W_10, V_9, U_8]: (ssPv3(W_10) | ssPv4(V_9) | ~ssPv4(U_8) | ~ssPv3(U_8) | ~ssRr(U_8, W_10) | ~ssRr(U_8, V_9)))). % 5.34/2.28 tff(c_48, plain, (![U_65, W_67, V_66]: (~ssPv2(U_65) | ~ssPv1(U_65) | ~ssPv1(W_67) | ~ssRr(U_65, W_67) | ~ssPv2(V_66) | ~ssRr(U_65, V_66)))). % 5.34/2.29 tff(c_159, plain, (![U_1, V_144]: (~ssPv2(U_1) | ~ssPv1(U_1) | ~ssPv2(skf1(U_1)) | ~ssPv4(V_144) | ~ssRr(U_1, V_144)))). % 5.34/2.29 tff(c_155, plain, (![U_141]: (ssPv3(U_141) | ssPv1(skf1(U_141)) | ~ssPv2(U_141) | ~ssPv4(U_141) | ~ssPv1(U_141)))). % 5.34/2.29 tff(c_46, plain, (![U_62, W_64, V_63]: (~ssPv2(U_62) | ~ssPv1(U_62) | ~ssPv2(W_64) | ~ssRr(U_62, W_64) | ~ssPv4(V_63) | ~ssRr(U_62, V_63)))). % 5.34/2.29 tff(c_149, plain, (![U_1]: (ssPv1(skf1(U_1)) | ~ssPv2(U_1) | ssPv2(skf1(U_1)) | ~ssPv4(U_1) | ~ssPv1(U_1)))). % 5.34/2.29 tff(c_141, plain, (![U_1]: (ssPv1(skf1(U_1)) | ~ssPv4(U_1) | ~ssPv2(U_1) | ~ssPv3(skf1(U_1))))). % 5.34/2.29 tff(c_128, plain, (![U_1, V_134]: (ssPv1(skf1(U_1)) | ~ssPv4(U_1) | ~ssPv2(U_1) | ~ssPv3(V_134) | ~ssRr(U_1, V_134)))). % 5.34/2.29 tff(c_132, plain, (![U_1]: (ssPv1(U_1) | ssPv2(skf1(U_1)) | ~ssPv3(U_1) | ~ssPv4(skf1(U_1))))). % 5.34/2.29 tff(c_124, plain, (![U_1, V_131]: (ssPv1(U_1) | ssPv2(skf1(U_1)) | ~ssPv3(U_1) | ~ssPv4(V_131) | ~ssRr(U_1, V_131)))). % 5.34/2.29 tff(c_34, plain, (![W_46, U_44, V_45]: (ssPv1(W_46) | ~ssPv4(U_44) | ~ssPv2(U_44) | ~ssRr(U_44, W_46) | ~ssPv3(V_45) | ~ssRr(U_44, V_45)))). % 5.34/2.29 tff(c_32, plain, (![U_41, W_43, V_42]: (ssPv1(U_41) | ssPv2(W_43) | ~ssPv3(U_41) | ~ssRr(U_41, W_43) | ~ssPv4(V_42) | ~ssRr(U_41, V_42)))). % 5.34/2.29 tff(c_115, plain, (![U_1]: (ssPv3(skf1(U_1)) | ~ssPv3(U_1) | ~ssPv2(U_1) | ~ssPv4(skf1(U_1))))). % 5.34/2.29 tff(c_111, plain, (![U_1, V_125]: (ssPv3(skf1(U_1)) | ~ssPv3(U_1) | ~ssPv2(U_1) | ~ssPv4(V_125) | ~ssRr(U_1, V_125)))). % 5.34/2.29 tff(c_36, plain, (![W_49, U_47, V_48]: (ssPv3(W_49) | ~ssPv3(U_47) | ~ssPv2(U_47) | ~ssRr(U_47, W_49) | ~ssPv4(V_48) | ~ssRr(U_47, V_48)))). % 5.34/2.29 tff(c_106, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv3(skf1(U_1)) | ~ssPv4(U_1) | ~ssPv1(U_1)))). % 5.34/2.29 tff(c_102, plain, (![U_1, V_118]: (ssPv2(skf1(U_1)) | ssPv3(V_118) | ~ssPv4(U_1) | ~ssPv1(U_1) | ~ssRr(U_1, V_118)))). % 5.34/2.29 tff(c_12, plain, (![W_13, V_12, U_11]: (ssPv2(W_13) | ssPv3(V_12) | ~ssPv4(U_11) | ~ssPv1(U_11) | ~ssRr(U_11, W_13) | ~ssRr(U_11, V_12)))). % 5.34/2.29 tff(c_93, plain, (![U_1, V_113]: (ssPv4(U_1) | ssPv4(skf1(U_1)) | ~ssPv3(U_1) | ~ssPv4(V_113) | ~ssRr(U_1, V_113)))). % 5.34/2.29 tff(c_89, plain, (![U_1]: (ssPv3(U_1) | ssPv1(skf1(U_1)) | ~ssPv1(U_1) | ~ssPv2(skf1(U_1))))). % 5.34/2.29 tff(c_14, plain, (![U_14, W_16, V_15]: (ssPv4(U_14) | ssPv4(W_16) | ~ssPv3(U_14) | ~ssRr(U_14, W_16) | ~ssPv4(V_15) | ~ssRr(U_14, V_15)))). % 5.34/2.29 tff(c_85, plain, (![U_1, V_108]: (ssPv3(U_1) | ssPv1(skf1(U_1)) | ~ssPv1(U_1) | ~ssPv2(V_108) | ~ssRr(U_1, V_108)))). % 5.34/2.29 tff(c_24, plain, (![U_29, W_31, V_30]: (ssPv3(U_29) | ssPv1(W_31) | ~ssPv1(U_29) | ~ssRr(U_29, W_31) | ~ssPv2(V_30) | ~ssRr(U_29, V_30)))). % 5.34/2.29 tff(c_80, plain, (![U_1]: (ssPv2(U_1) | ssPv1(U_1) | ssPv3(skf1(U_1)) | ~ssPv3(U_1)))). % 5.34/2.29 tff(c_4, plain, (![U_2, V_3]: (ssPv2(U_2) | ssPv1(U_2) | ssPv3(V_3) | ~ssPv3(U_2) | ~ssRr(U_2, V_3)))). % 5.34/2.29 tff(c_74, plain, (![U_1]: (ssPv2(U_1) | ssPv4(skf1(U_1)) | ~ssPv3(U_1) | ~ssPv1(U_1)))). % 5.34/2.29 tff(c_6, plain, (![U_4, V_5]: (ssPv2(U_4) | ssPv4(V_5) | ~ssPv3(U_4) | ~ssPv1(U_4) | ~ssRr(U_4, V_5)))). % 5.34/2.29 tff(c_68, plain, (![U_1]: (~ssPv3(U_1) | ~ssPv2(U_1) | ~ssPv1(U_1) | ~ssPv1(skf1(U_1))))). % 5.34/2.29 tff(c_8, plain, (![U_6, V_7]: (~ssPv3(U_6) | ~ssPv2(U_6) | ~ssPv1(U_6) | ~ssPv1(V_7) | ~ssRr(U_6, V_7)))). % 5.34/2.29 tff(c_2, plain, (![U_1]: (ssRr(U_1, skf1(U_1))))). % 5.34/2.29 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 5.34/2.29 %------------------------------------------------------------------------------