%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SYN526-1 : TPTP v9.0.0. Released v2.1.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 : n006.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:03:49 PM UTC 2025 % Result : Satisfiable 5.50s 2.23s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : SYN526-1 : TPTP v9.0.0. Released v2.1.0. % 0.06/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.34 % Computer : n006.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Wed Apr 9 07:55:22 EDT 2025 % 0.12/0.35 % CPUTime : % 5.50/2.23 % 5.50/2.23 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 5.50/2.23 % 5.50/2.23 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 5.50/2.24 %$ c5_2 > c4_2 > c3_2 > c2_2 > c1_2 > ssSkP0 > ndr1_1 > c5_1 > c4_1 > c3_1 > c2_1 > c1_1 > #nlpp > ssSkC9 > ssSkC8 > ssSkC7 > ssSkC6 > ssSkC5 > ssSkC4 > ssSkC3 > ssSkC2 > ssSkC1 > ssSkC0 > ndr1_0 > c5_0 > c4_0 > c3_0 > c2_0 > c1_0 > a250 > a249 > a248 > a247 > a246 > a245 > a244 > a243 > a242 > a241 > a240 > a239 > a238 > a237 > a236 > a235 > a234 > a233 > a232 > a231 > a230 > a229 > a228 > a227 > a226 > a225 > a224 > a223 > a222 > a221 > a220 > a219 > a218 % 5.50/2.24 % 5.50/2.24 %Foreground sorts: % 5.50/2.24 % 5.50/2.24 % 5.50/2.24 %Background operators: % 5.50/2.24 % 5.50/2.24 % 5.50/2.24 %Foreground operators: % 5.50/2.24 tff(a230, type, a230: $i). % 5.50/2.24 tff(a229, type, a229: $i). % 5.50/2.24 tff(a242, type, a242: $i). % 5.50/2.24 tff(ssSkC8, type, ssSkC8: $o). % 5.50/2.24 tff(ssSkC7, type, ssSkC7: $o). % 5.50/2.24 tff(c4_0, type, c4_0: $o). % 5.50/2.24 tff(ssSkP0, type, ssSkP0: $i > $o). % 5.50/2.24 tff(a249, type, a249: $i). % 5.50/2.24 tff(ssSkC6, type, ssSkC6: $o). % 5.50/2.24 tff(c3_0, type, c3_0: $o). % 5.50/2.24 tff(c1_2, type, c1_2: ($i * $i) > $o). % 5.50/2.24 tff(ssSkC3, type, ssSkC3: $o). % 5.50/2.24 tff(a233, type, a233: $i). % 5.50/2.24 tff(a232, type, a232: $i). % 5.50/2.24 tff(a237, type, a237: $i). % 5.50/2.24 tff(a248, type, a248: $i). % 5.50/2.24 tff(ssSkC4, type, ssSkC4: $o). % 5.50/2.24 tff(a238, type, a238: $i). % 5.50/2.24 tff(a228, type, a228: $i). % 5.50/2.24 tff(c5_0, type, c5_0: $o). % 5.50/2.24 tff(ssSkC9, type, ssSkC9: $o). % 5.50/2.24 tff(a245, type, a245: $i). % 5.50/2.24 tff(a235, type, a235: $i). % 5.50/2.24 tff(a222, type, a222: $i). % 5.50/2.24 tff(a220, type, a220: $i). % 5.50/2.24 tff(a227, type, a227: $i). % 5.50/2.24 tff(a236, type, a236: $i). % 5.50/2.24 tff(a246, type, a246: $i). % 5.50/2.24 tff(a218, type, a218: $i). % 5.50/2.24 tff(c1_0, type, c1_0: $o). % 5.50/2.24 tff(a240, type, a240: $i). % 5.50/2.24 tff(a234, type, a234: $i). % 5.50/2.24 tff(a250, type, a250: $i). % 5.50/2.24 tff(c2_1, type, c2_1: $i > $o). % 5.50/2.24 tff(a219, type, a219: $i). % 5.50/2.24 tff(ndr1_1, type, ndr1_1: $i > $o). % 5.50/2.24 tff(c2_0, type, c2_0: $o). % 5.50/2.24 tff(c4_1, type, c4_1: $i > $o). % 5.50/2.24 tff(a223, type, a223: $i). % 5.50/2.24 tff(a243, type, a243: $i). % 5.50/2.24 tff(a226, type, a226: $i). % 5.50/2.24 tff(ndr1_0, type, ndr1_0: $o). % 5.50/2.24 tff(a241, type, a241: $i). % 5.50/2.24 tff(a231, type, a231: $i). % 5.50/2.24 tff(a224, type, a224: $i). % 5.50/2.24 tff(c1_1, type, c1_1: $i > $o). % 5.50/2.24 tff(ssSkC2, type, ssSkC2: $o). % 5.50/2.24 tff(c5_2, type, c5_2: ($i * $i) > $o). % 5.50/2.24 tff(a225, type, a225: $i). % 5.50/2.24 tff(c4_2, type, c4_2: ($i * $i) > $o). % 5.50/2.24 tff(ssSkC1, type, ssSkC1: $o). % 5.50/2.24 tff(a239, type, a239: $i). % 5.50/2.24 tff(ssSkC0, type, ssSkC0: $o). % 5.50/2.24 tff(ssSkC5, type, ssSkC5: $o). % 5.50/2.24 tff(a247, type, a247: $i). % 5.50/2.24 tff(c5_1, type, c5_1: $i > $o). % 5.50/2.24 tff(a221, type, a221: $i). % 5.50/2.24 tff(c3_2, type, c3_2: ($i * $i) > $o). % 5.50/2.24 tff(c2_2, type, c2_2: ($i * $i) > $o). % 5.50/2.24 tff(a244, type, a244: $i). % 5.50/2.24 tff(c3_1, type, c3_1: $i > $o). % 5.50/2.24 % 5.50/2.24 %Saturated clause set: % 5.50/2.24 tff(c_462, plain, (![U_72, V_73]: (c5_1(U_72) | ~c2_1(U_72) | ~ndr1_1(U_72) | ~c5_2(U_72, V_73) | ~c1_2(U_72, V_73) | ~c4_2(U_72, V_73)))). % 5.50/2.24 tff(c_453, plain, (ssSkC3)). % 5.50/2.24 tff(c_449, plain, (![U_50, V_51]: (c5_2(U_50, a244) | c4_2(U_50, V_51) | c3_2(U_50, V_51) | ~c5_1(U_50) | ~ndr1_1(U_50) | ~c5_2(U_50, V_51)))). % 5.50/2.24 tff(c_446, plain, (![U_67, V_68]: (~c1_1(U_67) | ~c5_2(U_67, a234) | ~ndr1_1(U_67) | ~c5_2(U_67, V_68) | ~c4_2(U_67, V_68) | ~c2_2(U_67, V_68)))). % 5.50/2.24 tff(c_443, plain, (~c2_1(a232))). % 5.50/2.24 tff(c_423, plain, (![U_6]: (c3_1(U_6) | ~c1_1(U_6) | ~c2_1(U_6)))). % 5.50/2.24 tff(c_430, plain, (~c1_1(a223))). % 5.50/2.24 tff(c_432, plain, (![U_52, V_53]: (c2_2(U_52, a244) | c4_2(U_52, V_53) | c3_2(U_52, V_53) | ~c5_1(U_52) | ~ndr1_1(U_52) | ~c5_2(U_52, V_53)))). % 5.50/2.24 tff(c_395, plain, (![U_56, V_57]: (c3_1(U_56) | ~c1_1(U_56) | ~ndr1_1(U_56) | ~c1_2(U_56, V_57) | ~c3_2(U_56, V_57)))). % 5.50/2.24 tff(c_391, plain, (![U_54, V_55]: (c4_2(U_54, V_55) | c3_2(U_54, V_55) | ~c5_1(U_54) | ~c3_2(U_54, a244) | ~ndr1_1(U_54) | ~c5_2(U_54, V_55)))). % 5.50/2.24 tff(c_382, plain, (~c2_1(a236))). % 5.50/2.24 tff(c_378, plain, (~ndr1_1(a236))). % 5.50/2.24 tff(c_368, plain, (c5_0)). % 5.50/2.24 tff(c_358, plain, (![U_35]: (c4_1(U_35) | ~c2_1(U_35) | ~c5_2(U_35, a233)))). % 5.50/2.24 tff(c_346, plain, (![U_28]: (c4_1(U_28) | c3_2(U_28, a233) | ~c2_1(U_28)))). % 5.50/2.24 tff(c_341, plain, (~c2_1(a245))). % 5.50/2.24 tff(c_337, plain, (~ndr1_1(a245))). % 5.50/2.24 tff(c_328, plain, (![U_29]: (c4_1(U_29) | c2_2(U_29, a233) | ~c2_1(U_29)))). % 5.50/2.24 tff(c_321, plain, (ssSkC1)). % 5.50/2.24 tff(c_314, plain, (ssSkC6)). % 5.50/2.24 tff(c_305, plain, (~c4_0)). % 5.50/2.24 tff(c_295, plain, (ssSkC9)). % 5.50/2.24 tff(c_288, plain, (~ssSkC2)). % 5.50/2.25 tff(c_291, plain, (![U_13]: (c1_2(U_13, a238) | ~c2_1(U_13)))). % 5.50/2.25 tff(c_284, plain, (![U_19]: (~c2_1(U_19) | ~c2_2(U_19, a238)))). % 5.91/2.25 tff(c_281, plain, (~ssSkC7)). % 5.91/2.25 tff(c_277, plain, (![U_12]: (c3_2(U_12, a238) | ~c2_1(U_12)))). % 5.91/2.25 tff(c_273, plain, (![U_6]: (ndr1_1(U_6) | ~c2_1(U_6)))). % 5.91/2.25 tff(c_62, plain, (![U_2]: (ssSkP0(U_2) | c4_2(U_2, a227)))). % 5.91/2.25 tff(c_269, plain, (~c5_2(a221, a222))). % 5.91/2.25 tff(c_268, plain, (c1_2(a221, a222))). % 5.91/2.25 tff(c_86, plain, (![U_4]: (ssSkP0(U_4) | ~c5_2(U_4, a227)))). % 5.91/2.25 tff(c_64, plain, (![U_3]: (ssSkP0(U_3) | c1_2(U_3, a227)))). % 5.91/2.25 tff(c_265, plain, (~c3_1(a232))). % 5.91/2.25 tff(c_263, plain, (~c4_1(a232))). % 5.91/2.25 tff(c_261, plain, (c2_2(a223, a224))). % 5.91/2.25 tff(c_260, plain, (c4_2(a248, a249))). % 5.91/2.25 tff(c_259, plain, (ndr1_1(a221))). % 5.91/2.25 tff(c_258, plain, (~ssSkC8)). % 5.91/2.25 tff(c_257, plain, (c4_2(a223, a224))). % 5.91/2.25 tff(c_28, plain, (![U_1]: (ssSkP0(U_1) | ndr1_1(U_1)))). % 5.91/2.25 tff(c_255, plain, (~ssSkC5)). % 5.91/2.25 tff(c_254, plain, (~c1_2(a248, a249))). % 5.91/2.25 tff(c_253, plain, (~c5_2(a223, a224))). % 5.91/2.25 tff(c_252, plain, (~ssSkC0)). % 5.91/2.25 tff(c_251, plain, (c2_2(a248, a249))). % 5.91/2.25 tff(c_250, plain, (c3_1(a248))). % 5.91/2.25 tff(c_249, plain, (c2_1(a223))). % 5.91/2.25 tff(c_246, plain, (~c4_1(a236))). % 5.91/2.25 tff(c_245, plain, (~c3_1(a242))). % 5.91/2.25 tff(c_244, plain, (c3_1(a236))). % 5.91/2.25 tff(c_243, plain, (~c2_1(a242))). % 5.91/2.25 tff(c_241, plain, (ndr1_1(a248))). % 5.91/2.25 tff(c_239, plain, (ndr1_1(a223))). % 5.91/2.25 tff(c_236, plain, (~c5_1(a245))). % 5.91/2.25 tff(c_235, plain, (~c4_1(a242))). % 5.91/2.25 tff(c_234, plain, (c5_1(a223))). % 5.91/2.25 tff(c_228, plain, (ndr1_0)). % 5.91/2.25 tff(c_227, plain, (~c3_0)). % 5.91/2.25 tff(c_4, plain, (~c2_0)). % 5.91/2.25 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 5.91/2.25 %------------------------------------------------------------------------------