%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SYN735-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/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 : 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:19 PM UTC 2025 % Result : Satisfiable 4.67s 2.19s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.13 % Problem : SYN735-1 : TPTP v9.0.0. Released v2.5.0. % 0.13/0.14 % 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.14/0.34 % Computer : n031.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 300 % 0.14/0.34 % DateTime : Wed Apr 9 08:13:52 EDT 2025 % 0.14/0.35 % CPUTime : % 4.67/2.19 % 4.67/2.19 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 4.67/2.19 % 4.67/2.19 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 4.67/2.20 %$ ssRr > ssPv4 > ssPv3 > ssPv2 > ssPv1 > #nlpp > skf1 % 4.67/2.20 % 4.67/2.20 %Foreground sorts: % 4.67/2.20 % 4.67/2.20 % 4.67/2.20 %Background operators: % 4.67/2.20 % 4.67/2.20 % 4.67/2.20 %Foreground operators: % 4.67/2.20 tff(skf1, type, skf1: $i > $i). % 4.67/2.20 tff(ssPv1, type, ssPv1: $i > $o). % 4.67/2.20 tff(ssPv3, type, ssPv3: $i > $o). % 4.67/2.20 tff(ssRr, type, ssRr: ($i * $i) > $o). % 4.67/2.20 tff(ssPv4, type, ssPv4: $i > $o). % 4.67/2.20 tff(ssPv2, type, ssPv2: $i > $o). % 4.67/2.20 % 4.67/2.20 %Saturated clause set: % 4.67/2.21 tff(c_340, plain, (![U_1]: (ssPv1(skf1(U_1)) | ssPv3(skf1(U_1)) | ~ssPv3(U_1) | ssPv2(U_1) | ssPv2(skf1(U_1)) | ~ssPv1(U_1)))). % 5.02/2.21 tff(c_514, plain, (![U_230]: (ssPv4(U_230) | ssPv3(U_230) | ssPv1(U_230) | ssPv2(U_230) | ssPv3(skf1(U_230)) | ~ssPv2(skf1(U_230))))). % 5.02/2.21 tff(c_536, plain, (![U_231]: (~ssPv4(U_231) | ssPv1(skf1(U_231)) | ~ssPv3(U_231) | ssPv2(U_231) | ~ssPv2(skf1(U_231))))). % 5.02/2.21 tff(c_513, plain, (![U_230]: (ssPv1(skf1(U_230)) | ~ssPv3(U_230) | ssPv2(U_230) | ssPv3(skf1(U_230)) | ~ssPv2(skf1(U_230))))). % 5.02/2.21 tff(c_498, plain, (![U_1]: (ssPv2(U_1) | ssPv3(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv2(skf1(U_1))))). % 5.02/2.21 tff(c_494, plain, (![U_1, V_227]: (ssPv2(U_1) | ssPv3(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv2(V_227) | ~ssRr(U_1, V_227)))). % 5.02/2.21 tff(c_417, plain, (![U_1, W_208, V_209]: (ssPv2(U_1) | ssPv3(skf1(U_1)) | ssPv4(W_208) | ~ssRr(U_1, W_208) | ~ssPv2(V_209) | ~ssRr(U_1, V_209)))). % 5.02/2.21 tff(c_471, plain, (![U_1]: (ssPv1(U_1) | ssPv2(skf1(U_1)) | ~ssPv4(U_1) | ssPv2(U_1) | ~ssPv3(U_1) | ~ssPv1(skf1(U_1))))). % 5.02/2.21 tff(c_476, plain, (![U_1, V_220]: (ssPv2(U_1) | ssPv3(skf1(U_1)) | ~ssPv2(skf1(U_1)) | ~ssPv3(V_220) | ~ssRr(U_1, V_220)))). % 5.02/2.21 tff(c_470, plain, (![U_1]: (ssPv1(U_1) | ~ssPv4(U_1) | ssPv2(skf1(U_1)) | ~ssPv2(U_1) | ~ssPv1(skf1(U_1))))). % 5.02/2.21 tff(c_383, plain, (![U_1, W_200, V_201]: (ssPv2(U_1) | ssPv3(skf1(U_1)) | ~ssPv2(W_200) | ~ssRr(U_1, W_200) | ~ssPv3(V_201) | ~ssRr(U_1, V_201)))). % 5.02/2.21 tff(c_447, plain, (![U_1]: (ssPv1(U_1) | ~ssPv1(skf1(U_1)) | ssPv2(skf1(U_1)) | ~ssPv4(U_1) | ~ssPv3(skf1(U_1))))). % 5.02/2.22 tff(c_430, plain, (![U_1]: (ssPv1(U_1) | ssPv2(skf1(U_1)) | ~ssPv1(skf1(U_1)) | ~ssPv4(skf1(U_1))))). % 5.02/2.22 tff(c_426, plain, (![U_1, V_213]: (ssPv1(U_1) | ssPv2(skf1(U_1)) | ~ssPv1(skf1(U_1)) | ~ssPv4(V_213) | ~ssRr(U_1, V_213)))). % 5.02/2.22 tff(c_320, plain, (![U_1, W_189, V_190]: (ssPv1(U_1) | ssPv2(skf1(U_1)) | ~ssPv1(W_189) | ~ssRr(U_1, W_189) | ~ssPv4(V_190) | ~ssRr(U_1, V_190)))). % 5.02/2.22 tff(c_407, plain, (![U_1]: (ssPv2(skf1(U_1)) | ~ssPv1(U_1) | ssPv2(U_1) | ~ssPv3(U_1) | ~ssPv1(skf1(U_1))))). % 5.02/2.22 tff(c_28, plain, (![U_36, X_39, W_38, V_37]: (ssPv2(U_36) | ssPv3(X_39) | ssPv4(W_38) | ~ssRr(U_36, X_39) | ~ssRr(U_36, W_38) | ~ssPv2(V_37) | ~ssRr(U_36, V_37)))). % 5.02/2.22 tff(c_406, plain, (![U_1]: (~ssPv1(U_1) | ssPv2(skf1(U_1)) | ~ssPv2(U_1) | ~ssPv1(skf1(U_1))))). % 5.02/2.22 tff(c_387, plain, (![U_1]: (ssPv2(skf1(U_1)) | ~ssPv1(U_1) | ~ssPv1(skf1(U_1)) | ~ssPv3(skf1(U_1))))). % 5.02/2.22 tff(c_379, plain, (![U_1, V_197]: (ssPv2(skf1(U_1)) | ~ssPv1(U_1) | ~ssPv1(skf1(U_1)) | ~ssPv3(V_197) | ~ssRr(U_1, V_197)))). % 5.02/2.22 tff(c_36, plain, (![U_52, X_55, W_54, V_53]: (ssPv2(U_52) | ssPv3(X_55) | ~ssRr(U_52, X_55) | ~ssPv2(W_54) | ~ssRr(U_52, W_54) | ~ssPv3(V_53) | ~ssRr(U_52, V_53)))). % 5.02/2.22 tff(c_303, plain, (![U_1, W_179, V_180]: (ssPv2(skf1(U_1)) | ~ssPv1(U_1) | ~ssPv1(W_179) | ~ssRr(U_1, W_179) | ~ssPv3(V_180) | ~ssRr(U_1, V_180)))). % 5.02/2.22 tff(c_341, plain, (![U_1]: (ssPv1(skf1(U_1)) | ~ssPv3(U_1) | ssPv1(U_1) | ssPv3(skf1(U_1)) | ~ssPv2(U_1)))). % 5.02/2.22 tff(c_354, plain, (![U_192]: (ssPv2(U_192) | ssPv1(skf1(U_192)) | ~ssPv3(U_192) | ~ssPv4(U_192) | ~ssPv1(U_192)))). % 5.02/2.22 tff(c_339, plain, (![U_1]: (ssPv1(skf1(U_1)) | ~ssPv3(U_1) | ssPv3(skf1(U_1)) | ~ssPv4(U_1) | ~ssPv1(U_1)))). % 5.02/2.22 tff(c_316, plain, (![U_1]: (ssPv1(skf1(U_1)) | ssPv3(skf1(U_1)) | ~ssPv3(U_1) | ~ssPv4(skf1(U_1))))). % 5.02/2.22 tff(c_40, plain, (![U_60, X_63, W_62, V_61]: (ssPv1(U_60) | ssPv2(X_63) | ~ssRr(U_60, X_63) | ~ssPv1(W_62) | ~ssRr(U_60, W_62) | ~ssPv4(V_61) | ~ssRr(U_60, V_61)))). % 5.02/2.22 tff(c_312, plain, (![U_1, V_184]: (ssPv1(skf1(U_1)) | ssPv3(skf1(U_1)) | ~ssPv3(U_1) | ~ssPv4(V_184) | ~ssRr(U_1, V_184)))). % 5.02/2.22 tff(c_268, plain, (![U_1, W_166, V_168]: (ssPv1(skf1(U_1)) | ssPv3(W_166) | ~ssPv3(U_1) | ~ssRr(U_1, W_166) | ~ssPv4(V_168) | ~ssRr(U_1, V_168)))). % 5.02/2.22 tff(c_299, plain, (![U_176]: (~ssPv4(U_176) | ssPv3(U_176) | ~ssPv2(U_176) | ~ssPv1(skf1(U_176))))). % 5.02/2.22 tff(c_42, plain, (![X_67, U_64, W_66, V_65]: (ssPv2(X_67) | ~ssPv1(U_64) | ~ssRr(U_64, X_67) | ~ssPv1(W_66) | ~ssRr(U_64, W_66) | ~ssPv3(V_65) | ~ssRr(U_64, V_65)))). % 5.02/2.22 tff(c_292, plain, (![U_175]: (ssPv3(U_175) | ssPv2(skf1(U_175)) | ~ssPv2(U_175) | ~ssPv1(skf1(U_175))))). % 5.02/2.22 tff(c_281, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv3(skf1(U_1)) | ~ssPv2(U_1) | ~ssPv1(skf1(U_1))))). % 5.02/2.22 tff(c_277, plain, (![U_1, V_172]: (ssPv2(skf1(U_1)) | ssPv3(skf1(U_1)) | ~ssPv2(U_1) | ~ssPv1(V_172) | ~ssRr(U_1, V_172)))). % 5.02/2.23 tff(c_246, plain, (![U_1, W_158, V_160]: (ssPv2(skf1(U_1)) | ssPv3(W_158) | ~ssPv2(U_1) | ~ssRr(U_1, W_158) | ~ssPv1(V_160) | ~ssRr(U_1, V_160)))). % 5.02/2.23 tff(c_30, plain, (![X_43, W_42, U_40, V_41]: (ssPv1(X_43) | ssPv3(W_42) | ~ssPv3(U_40) | ~ssRr(U_40, X_43) | ~ssRr(U_40, W_42) | ~ssPv4(V_41) | ~ssRr(U_40, V_41)))). % 5.02/2.23 tff(c_259, plain, (![U_1]: (~ssPv1(skf1(U_1)) | ssPv3(U_1) | ssPv1(U_1) | ssPv2(skf1(U_1))))). % 5.02/2.23 tff(c_250, plain, (![U_1]: (ssPv3(U_1) | ssPv2(skf1(U_1)) | ~ssPv1(skf1(U_1)) | ~ssPv3(skf1(U_1))))). % 5.02/2.23 tff(c_242, plain, (![U_1, V_156]: (ssPv3(U_1) | ssPv2(skf1(U_1)) | ~ssPv1(skf1(U_1)) | ~ssPv3(V_156) | ~ssRr(U_1, V_156)))). % 5.02/2.23 tff(c_32, plain, (![X_47, W_46, U_44, V_45]: (ssPv2(X_47) | ssPv3(W_46) | ~ssPv2(U_44) | ~ssRr(U_44, X_47) | ~ssRr(U_44, W_46) | ~ssPv1(V_45) | ~ssRr(U_44, V_45)))). % 5.02/2.23 tff(c_211, plain, (![U_1, W_147, V_148]: (ssPv3(U_1) | ssPv2(skf1(U_1)) | ~ssPv1(W_147) | ~ssRr(U_1, W_147) | ~ssPv3(V_148) | ~ssRr(U_1, V_148)))). % 5.02/2.23 tff(c_233, plain, (![U_1]: (ssPv2(U_1) | ~ssPv4(U_1) | ssPv3(U_1) | ssPv1(U_1) | ssPv2(skf1(U_1))))). % 5.02/2.23 tff(c_224, plain, (![U_151]: (ssPv3(U_151) | ssPv2(U_151) | ssPv2(skf1(U_151)) | ~ssPv4(U_151) | ~ssPv3(skf1(U_151))))). % 5.02/2.23 tff(c_215, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv4(U_1) | ~ssPv3(skf1(U_1))))). % 5.02/2.23 tff(c_207, plain, (![U_1, V_144]: (ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv4(U_1) | ~ssPv3(V_144) | ~ssRr(U_1, V_144)))). % 5.02/2.23 tff(c_34, plain, (![U_48, X_51, W_50, V_49]: (ssPv3(U_48) | ssPv2(X_51) | ~ssRr(U_48, X_51) | ~ssPv1(W_50) | ~ssRr(U_48, W_50) | ~ssPv3(V_49) | ~ssRr(U_48, V_49)))). % 5.02/2.23 tff(c_181, plain, (![U_1, W_137, V_139]: (ssPv2(skf1(U_1)) | ssPv4(W_137) | ~ssPv4(U_1) | ~ssRr(U_1, W_137) | ~ssPv3(V_139) | ~ssRr(U_1, V_139)))). % 5.02/2.23 tff(c_177, plain, (![U_1]: (ssPv2(U_1) | ~ssPv4(skf1(U_1)) | ssPv4(U_1) | ssPv3(U_1) | ssPv1(U_1)))). % 5.02/2.23 tff(c_38, plain, (![X_59, W_58, U_56, V_57]: (ssPv2(X_59) | ssPv4(W_58) | ~ssPv4(U_56) | ~ssRr(U_56, X_59) | ~ssRr(U_56, W_58) | ~ssPv3(V_57) | ~ssRr(U_56, V_57)))). % 5.02/2.23 tff(c_172, plain, (![U_1, V_133]: (ssPv2(U_1) | ~ssPv4(V_133) | ~ssRr(U_1, V_133) | ssPv4(U_1) | ssPv3(U_1) | ssPv1(U_1)))). % 5.02/2.23 tff(c_168, plain, (![U_1, V_131]: (ssPv3(U_1) | ssPv2(U_1) | ~ssPv1(skf1(U_1)) | ~ssPv4(V_131) | ~ssRr(U_1, V_131)))). % 5.02/2.23 tff(c_24, plain, (![U_30, W_32, V_31]: (ssPv3(U_30) | ssPv2(U_30) | ~ssPv1(W_32) | ~ssRr(U_30, W_32) | ~ssPv4(V_31) | ~ssRr(U_30, V_31)))). % 5.02/2.23 tff(c_159, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv4(U_1) | ~ssPv1(U_1)))). % 5.02/2.23 tff(c_155, plain, (![U_1, V_124]: (ssPv2(skf1(U_1)) | ssPv4(V_124) | ~ssPv4(U_1) | ~ssPv1(U_1) | ~ssRr(U_1, V_124)))). % 5.02/2.23 tff(c_18, plain, (![W_23, V_22, U_21]: (ssPv2(W_23) | ssPv4(V_22) | ~ssPv4(U_21) | ~ssPv1(U_21) | ~ssRr(U_21, W_23) | ~ssRr(U_21, V_22)))). % 5.02/2.23 tff(c_146, plain, (![U_1]: (ssPv3(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv4(U_1) | ~ssPv1(U_1)))). % 5.02/2.23 tff(c_137, plain, (![U_1, V_117]: (ssPv3(skf1(U_1)) | ssPv4(V_117) | ~ssPv4(U_1) | ~ssPv1(U_1) | ~ssRr(U_1, V_117)))). % 5.02/2.23 tff(c_133, plain, (![U_115]: (ssPv3(U_115) | ssPv2(U_115) | ssPv2(skf1(U_115)) | ~ssPv1(U_115)))). % 5.02/2.23 tff(c_16, plain, (![W_20, V_19, U_18]: (ssPv3(W_20) | ssPv4(V_19) | ~ssPv4(U_18) | ~ssPv1(U_18) | ~ssRr(U_18, W_20) | ~ssRr(U_18, V_19)))). % 5.02/2.23 tff(c_128, plain, (![U_1]: (ssPv2(U_1) | ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv1(U_1)))). % 5.02/2.23 tff(c_124, plain, (![U_1, V_112]: (ssPv2(U_1) | ssPv2(skf1(U_1)) | ssPv4(V_112) | ~ssPv1(U_1) | ~ssRr(U_1, V_112)))). % 5.02/2.23 tff(c_10, plain, (![U_9, W_11, V_10]: (ssPv2(U_9) | ssPv2(W_11) | ssPv4(V_10) | ~ssPv1(U_9) | ~ssRr(U_9, W_11) | ~ssRr(U_9, V_10)))). % 5.02/2.23 tff(c_115, plain, (![U_1]: (ssPv2(U_1) | ssPv3(skf1(U_1)) | ~ssPv3(U_1) | ~ssPv1(skf1(U_1))))). % 5.02/2.24 tff(c_111, plain, (![U_1, V_106]: (ssPv2(U_1) | ssPv3(skf1(U_1)) | ~ssPv3(U_1) | ~ssPv1(V_106) | ~ssRr(U_1, V_106)))). % 5.02/2.24 tff(c_22, plain, (![U_27, W_29, V_28]: (ssPv2(U_27) | ssPv3(W_29) | ~ssPv3(U_27) | ~ssRr(U_27, W_29) | ~ssPv1(V_28) | ~ssRr(U_27, V_28)))). % 5.02/2.24 tff(c_102, plain, (![U_1]: (ssPv2(U_1) | ssPv1(skf1(U_1)) | ~ssPv4(U_1) | ~ssPv3(skf1(U_1))))). % 5.02/2.24 tff(c_93, plain, (![U_1, V_99]: (ssPv2(U_1) | ssPv1(skf1(U_1)) | ~ssPv4(U_1) | ~ssPv3(V_99) | ~ssRr(U_1, V_99)))). % 5.02/2.24 tff(c_89, plain, (![U_1]: (ssPv1(U_1) | ssPv3(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv2(U_1)))). % 5.02/2.24 tff(c_20, plain, (![U_24, W_26, V_25]: (ssPv2(U_24) | ssPv1(W_26) | ~ssPv4(U_24) | ~ssRr(U_24, W_26) | ~ssPv3(V_25) | ~ssRr(U_24, V_25)))). % 5.02/2.24 tff(c_85, plain, (![U_1, V_94]: (ssPv1(U_1) | ssPv3(skf1(U_1)) | ssPv4(V_94) | ~ssPv2(U_1) | ~ssRr(U_1, V_94)))). % 5.02/2.24 tff(c_14, plain, (![U_15, W_17, V_16]: (ssPv1(U_15) | ssPv3(W_17) | ssPv4(V_16) | ~ssPv2(U_15) | ~ssRr(U_15, W_17) | ~ssRr(U_15, V_16)))). % 5.02/2.24 tff(c_80, plain, (![U_1]: (ssPv3(U_1) | ssPv1(U_1) | ssPv2(skf1(U_1)) | ssPv3(skf1(U_1))))). % 5.02/2.24 tff(c_72, plain, (![U_1, V_86]: (ssPv3(U_1) | ssPv1(U_1) | ssPv2(skf1(U_1)) | ssPv3(V_86) | ~ssRr(U_1, V_86)))). % 5.02/2.24 tff(c_68, plain, (![U_1, V_83]: (ssPv3(skf1(U_1)) | ~ssPv4(U_1) | ~ssPv1(U_1) | ~ssPv3(V_83) | ~ssRr(U_1, V_83)))). % 5.02/2.24 tff(c_8, plain, (![U_6, W_8, V_7]: (ssPv3(U_6) | ssPv1(U_6) | ssPv2(W_8) | ssPv3(V_7) | ~ssRr(U_6, W_8) | ~ssRr(U_6, V_7)))). % 5.02/2.24 tff(c_26, plain, (![W_35, U_33, V_34]: (ssPv3(W_35) | ~ssPv4(U_33) | ~ssPv1(U_33) | ~ssRr(U_33, W_35) | ~ssPv3(V_34) | ~ssRr(U_33, V_34)))). % 5.02/2.24 tff(c_63, plain, (![U_1]: (ssPv3(U_1) | ssPv2(U_1) | ssPv2(skf1(U_1)) | ~ssPv4(skf1(U_1))))). % 5.02/2.24 tff(c_59, plain, (![U_1, V_77]: (ssPv3(U_1) | ssPv2(U_1) | ssPv2(skf1(U_1)) | ~ssPv4(V_77) | ~ssRr(U_1, V_77)))). % 5.02/2.24 tff(c_12, plain, (![U_12, W_14, V_13]: (ssPv3(U_12) | ssPv2(U_12) | ssPv2(W_14) | ~ssRr(U_12, W_14) | ~ssPv4(V_13) | ~ssRr(U_12, V_13)))). % 5.02/2.24 tff(c_54, plain, (![U_1]: (ssPv4(U_1) | ssPv3(U_1) | ssPv1(U_1) | ssPv1(skf1(U_1))))). % 5.02/2.24 tff(c_4, plain, (![U_2, V_3]: (ssPv4(U_2) | ssPv3(U_2) | ssPv1(U_2) | ssPv1(V_3) | ~ssRr(U_2, V_3)))). % 5.02/2.24 tff(c_48, plain, (![U_1]: (ssPv3(U_1) | ~ssPv4(U_1) | ~ssPv2(U_1) | ~ssPv2(skf1(U_1))))). % 5.02/2.24 tff(c_6, plain, (![U_4, V_5]: (ssPv3(U_4) | ~ssPv4(U_4) | ~ssPv2(U_4) | ~ssPv2(V_5) | ~ssRr(U_4, V_5)))). % 5.02/2.24 tff(c_2, plain, (![U_1]: (ssRr(U_1, skf1(U_1))))). % 5.02/2.24 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 5.02/2.24 %------------------------------------------------------------------------------