%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SYN522-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/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 : n010.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:48 PM UTC 2025 % Result : Satisfiable 5.74s 2.24s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SYN522-1 : TPTP v9.0.0. Released v2.1.0. % 0.07/0.13 % 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.13/0.34 % Computer : n010.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 07:55:03 EDT 2025 % 0.13/0.34 % CPUTime : % 5.74/2.24 % 5.74/2.24 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 5.74/2.24 % 5.74/2.24 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 5.74/2.25 %$ c5_2 > c4_2 > c3_2 > c2_2 > c1_2 > ssSkP4 > ssSkP3 > ssSkP2 > ssSkP1 > ssSkP0 > ndr1_1 > c5_1 > c4_1 > c3_1 > c2_1 > c1_1 > #nlpp > ssSkC7 > ssSkC6 > ssSkC5 > ssSkC4 > ssSkC3 > ssSkC2 > ssSkC1 > ssSkC0 > ndr1_0 > c5_0 > c4_0 > c3_0 > c2_0 > c1_0 > a140 > a139 > a138 > a137 > a134 > a133 > a132 > a131 > a130 > a129 > a128 > a127 > a126 > a125 > a122 > a121 > a120 > a119 > a118 > a117 > a116 > a115 > a114 > a113 > a112 > a111 > a110 > a109 > a108 > a107 > a106 > a105 > a104 % 5.74/2.25 % 5.74/2.25 %Foreground sorts: % 5.74/2.25 % 5.74/2.25 % 5.74/2.25 %Background operators: % 5.74/2.25 % 5.74/2.25 % 5.74/2.25 %Foreground operators: % 5.74/2.25 tff(a108, type, a108: $i). % 5.74/2.25 tff(ssSkC7, type, ssSkC7: $o). % 5.74/2.25 tff(a112, type, a112: $i). % 5.74/2.25 tff(c4_0, type, c4_0: $o). % 5.74/2.25 tff(ssSkP0, type, ssSkP0: $i > $o). % 5.74/2.25 tff(a122, type, a122: $i). % 5.74/2.25 tff(a120, type, a120: $i). % 5.74/2.25 tff(ssSkC6, type, ssSkC6: $o). % 5.74/2.25 tff(c3_0, type, c3_0: $o). % 5.74/2.25 tff(a140, type, a140: $i). % 5.74/2.25 tff(a138, type, a138: $i). % 5.74/2.25 tff(c1_2, type, c1_2: ($i * $i) > $o). % 5.74/2.25 tff(a113, type, a113: $i). % 5.74/2.25 tff(ssSkC3, type, ssSkC3: $o). % 5.74/2.25 tff(a130, type, a130: $i). % 5.74/2.25 tff(ssSkP2, type, ssSkP2: $i > $o). % 5.74/2.25 tff(a119, type, a119: $i). % 5.74/2.25 tff(a107, type, a107: $i). % 5.74/2.25 tff(a131, type, a131: $i). % 5.74/2.25 tff(a126, type, a126: $i). % 5.74/2.25 tff(a110, type, a110: $i). % 5.74/2.25 tff(ssSkC4, type, ssSkC4: $o). % 5.74/2.25 tff(a121, type, a121: $i). % 5.74/2.25 tff(a125, type, a125: $i). % 5.74/2.25 tff(c5_0, type, c5_0: $o). % 5.74/2.25 tff(a127, type, a127: $i). % 5.74/2.25 tff(a111, type, a111: $i). % 5.74/2.25 tff(a104, type, a104: $i). % 5.74/2.25 tff(a134, type, a134: $i). % 5.74/2.25 tff(a139, type, a139: $i). % 5.74/2.25 tff(ssSkP3, type, ssSkP3: $i > $o). % 5.74/2.25 tff(a118, type, a118: $i). % 5.74/2.25 tff(c1_0, type, c1_0: $o). % 5.74/2.25 tff(ssSkP4, type, ssSkP4: $i > $o). % 5.74/2.25 tff(a105, type, a105: $i). % 5.74/2.25 tff(c2_1, type, c2_1: $i > $o). % 5.74/2.25 tff(a129, type, a129: $i). % 5.74/2.25 tff(ndr1_1, type, ndr1_1: $i > $o). % 5.74/2.25 tff(c2_0, type, c2_0: $o). % 5.74/2.25 tff(c4_1, type, c4_1: $i > $o). % 5.74/2.25 tff(a116, type, a116: $i). % 5.74/2.25 tff(ndr1_0, type, ndr1_0: $o). % 5.74/2.25 tff(a117, type, a117: $i). % 5.74/2.25 tff(a137, type, a137: $i). % 5.74/2.25 tff(a133, type, a133: $i). % 5.74/2.25 tff(c1_1, type, c1_1: $i > $o). % 5.74/2.25 tff(a115, type, a115: $i). % 5.74/2.25 tff(ssSkC2, type, ssSkC2: $o). % 5.74/2.25 tff(c5_2, type, c5_2: ($i * $i) > $o). % 5.74/2.25 tff(c4_2, type, c4_2: ($i * $i) > $o). % 5.74/2.25 tff(a114, type, a114: $i). % 5.74/2.25 tff(ssSkC1, type, ssSkC1: $o). % 5.74/2.25 tff(ssSkC0, type, ssSkC0: $o). % 5.74/2.25 tff(ssSkC5, type, ssSkC5: $o). % 5.74/2.25 tff(ssSkP1, type, ssSkP1: $i > $o). % 5.74/2.25 tff(a106, type, a106: $i). % 5.74/2.25 tff(c5_1, type, c5_1: $i > $o). % 5.74/2.25 tff(c3_2, type, c3_2: ($i * $i) > $o). % 5.74/2.25 tff(a109, type, a109: $i). % 5.74/2.25 tff(c2_2, type, c2_2: ($i * $i) > $o). % 5.74/2.25 tff(a128, type, a128: $i). % 5.74/2.25 tff(a132, type, a132: $i). % 5.74/2.25 tff(c3_1, type, c3_1: $i > $o). % 5.74/2.25 % 5.74/2.25 %Saturated clause set: % 5.74/2.25 tff(c_474, plain, (c2_2(a139, a140))). % 5.74/2.25 tff(c_470, plain, (~c4_2(a139, a140))). % 5.74/2.25 tff(c_466, plain, (c1_2(a139, a140))). % 5.74/2.25 tff(c_460, plain, (~c5_1(a139))). % 5.74/2.25 tff(c_456, plain, (~ssSkC2)). % 5.74/2.25 tff(c_453, plain, (ndr1_1(a139))). % 5.74/2.26 tff(c_445, plain, (![U_7]: (c2_2(U_7, a105) | c3_2(U_7, a116) | c2_2(U_7, a116) | ~ndr1_1(U_7) | ~ssSkP0(U_7) | ssSkP2(U_7)))). % 5.74/2.26 tff(c_429, plain, (![U_48, V_49]: (c2_2(U_48, a105) | c3_2(U_48, V_49) | c2_2(U_48, V_49) | ~ndr1_1(U_48) | ~c5_2(U_48, V_49) | ~ssSkP0(U_48)))). % 5.74/2.26 tff(c_422, plain, (![U_7]: (c3_2(U_7, a116) | c2_2(U_7, a116) | ~c4_2(U_7, a105) | ~ndr1_1(U_7) | ~ssSkP0(U_7) | ssSkP2(U_7)))). % 5.74/2.26 tff(c_403, plain, (~c2_0)). % 5.74/2.26 tff(c_406, plain, (![U_54, V_55]: (c3_2(U_54, V_55) | c2_2(U_54, V_55) | ~c4_2(U_54, a105) | ~ndr1_1(U_54) | ~c5_2(U_54, V_55) | ~ssSkP0(U_54)))). % 5.74/2.26 tff(c_398, plain, (ssSkC3)). % 5.74/2.26 tff(c_393, plain, (![U_7]: (c3_2(U_7, a116) | c2_2(U_7, a116) | ~c3_2(U_7, a105) | ~ndr1_1(U_7) | ~ssSkP0(U_7) | ssSkP2(U_7)))). % 5.74/2.26 tff(c_377, plain, (![U_56, V_57]: (c3_2(U_56, V_57) | c2_2(U_56, V_57) | ~c3_2(U_56, a105) | ~ndr1_1(U_56) | ~c5_2(U_56, V_57) | ~ssSkP0(U_56)))). % 5.74/2.26 tff(c_365, plain, (c4_1(a134))). % 5.74/2.26 tff(c_364, plain, (c5_1(a134))). % 5.74/2.26 tff(c_357, plain, (~ndr1_1(a134))). % 5.74/2.26 tff(c_353, plain, (![U_30]: (c4_1(U_30) | ~c1_2(U_30, a120) | ~ssSkP3(U_30)))). % 5.74/2.26 tff(c_349, plain, (![U_22]: (c5_1(U_22) | c5_2(U_22, a132) | ~ssSkP4(U_22)))). % 5.74/2.26 tff(c_345, plain, (![U_27]: (c4_1(U_27) | c2_2(U_27, a120) | ~ssSkP3(U_27)))). % 5.74/2.26 tff(c_342, plain, (c4_1(a114))). % 5.74/2.26 tff(c_341, plain, (c5_1(a114))). % 5.74/2.26 tff(c_330, plain, (~ndr1_1(a114))). % 5.74/2.26 tff(c_333, plain, (![U_23]: (c5_1(U_23) | c1_2(U_23, a132) | ~ssSkP4(U_23)))). % 5.74/2.26 tff(c_328, plain, (![U_28]: (c4_1(U_28) | c5_2(U_28, a120) | ~ssSkP3(U_28)))). % 5.74/2.26 tff(c_320, plain, (![U_1]: (c5_1(U_1) | ndr1_1(U_1)))). % 5.74/2.26 tff(c_323, plain, (![U_21]: (c5_1(U_21) | c2_2(U_21, a132) | ~ssSkP4(U_21)))). % 5.74/2.26 tff(c_311, plain, (![U_2]: (c4_1(U_2) | ndr1_1(U_2)))). % 5.74/2.26 tff(c_126, plain, (![U_16]: (ssSkP3(U_16) | ~c2_2(U_16, a119)))). % 5.74/2.26 tff(c_132, plain, (![U_19]: (ssSkP0(U_19) | ~c1_2(U_19, a104)))). % 5.74/2.26 tff(c_108, plain, (![U_13]: (ssSkP4(U_13) | ~c4_2(U_13, a131)))). % 5.74/2.26 tff(c_70, plain, (![U_7]: (ssSkP2(U_7) | c5_2(U_7, a116)))). % 5.74/2.26 tff(c_74, plain, (![U_9]: (ssSkP1(U_9) | c2_2(U_9, a115)))). % 5.74/2.26 tff(c_124, plain, (![U_15]: (ssSkP3(U_15) | ~c3_2(U_15, a119)))). % 5.74/2.26 tff(c_68, plain, (![U_6]: (ssSkP3(U_6) | c4_2(U_6, a119)))). % 5.74/2.26 tff(c_110, plain, (![U_14]: (ssSkP4(U_14) | ~c1_2(U_14, a131)))). % 5.74/2.26 tff(c_72, plain, (![U_8]: (ssSkP2(U_8) | c1_2(U_8, a116)))). % 5.74/2.26 tff(c_130, plain, (![U_18]: (ssSkP1(U_18) | ~c4_2(U_18, a115)))). % 5.74/2.26 tff(c_128, plain, (![U_17]: (ssSkP2(U_17) | ~c2_2(U_17, a116)))). % 5.74/2.26 tff(c_76, plain, (![U_10]: (ssSkP1(U_10) | c5_2(U_10, a115)))). % 5.74/2.26 tff(c_88, plain, (![U_11]: (ssSkP0(U_11) | c4_2(U_11, a104)))). % 5.74/2.26 tff(c_90, plain, (![U_12]: (ssSkP0(U_12) | c3_2(U_12, a104)))). % 5.74/2.26 tff(c_289, plain, (~ssSkC4)). % 5.74/2.26 tff(c_288, plain, (~ssSkC6)). % 5.74/2.26 tff(c_287, plain, (~c3_2(a125, a127))). % 5.74/2.26 tff(c_286, plain, (c2_2(a106, a107))). % 5.74/2.26 tff(c_285, plain, (c4_2(a128, a129))). % 5.74/2.26 tff(c_284, plain, (~c4_2(a125, a127))). % 5.74/2.26 tff(c_38, plain, (![U_3]: (ssSkP2(U_3) | ndr1_1(U_3)))). % 5.74/2.26 tff(c_40, plain, (![U_4]: (ssSkP1(U_4) | ndr1_1(U_4)))). % 5.74/2.26 tff(c_281, plain, (~c1_2(a128, a129))). % 5.74/2.26 tff(c_46, plain, (![U_5]: (ssSkP0(U_5) | ndr1_1(U_5)))). % 5.74/2.26 tff(c_279, plain, (~c3_2(a125, a126))). % 5.74/2.26 tff(c_278, plain, (~c2_2(a125, a127))). % 5.74/2.26 tff(c_277, plain, (c1_2(a125, a126))). % 5.74/2.26 tff(c_36, plain, (![U_2]: (ssSkP3(U_2) | ndr1_1(U_2)))). % 5.74/2.26 tff(c_275, plain, (c2_2(a128, a129))). % 5.74/2.26 tff(c_28, plain, (![U_1]: (ssSkP4(U_1) | ndr1_1(U_1)))). % 5.74/2.26 tff(c_273, plain, (~ssSkC0)). % 5.74/2.26 tff(c_272, plain, (c1_2(a106, a107))). % 5.74/2.26 tff(c_271, plain, (~c5_2(a125, a126))). % 5.74/2.26 tff(c_270, plain, (c4_2(a106, a107))). % 5.74/2.26 tff(c_269, plain, (ndr1_1(a128))). % 5.74/2.26 tff(c_268, plain, (c3_1(a109))). % 5.74/2.26 tff(c_267, plain, (ndr1_1(a125))). % 5.98/2.26 tff(c_266, plain, (~c2_1(a118))). % 5.98/2.26 tff(c_265, plain, (c5_1(a118))). % 5.98/2.26 tff(c_262, plain, (c1_1(a118))). % 5.98/2.26 tff(c_261, plain, (~c1_0)). % 5.98/2.26 tff(c_260, plain, (~c4_1(a125))). % 5.98/2.26 tff(c_259, plain, (~c2_1(a134))). % 5.98/2.26 tff(c_258, plain, (ndr1_1(a106))). % 5.98/2.26 tff(c_257, plain, (~c5_1(a106))). % 5.98/2.26 tff(c_256, plain, (~c1_1(a114))). % 5.98/2.26 tff(c_255, plain, (~c5_0)). % 5.98/2.26 tff(c_253, plain, (c3_1(a128))). % 5.98/2.26 tff(c_252, plain, (~c3_0)). % 5.98/2.26 tff(c_251, plain, (~c1_1(a109))). % 5.98/2.26 tff(c_250, plain, (~c2_1(a128))). % 5.98/2.27 tff(c_241, plain, (ndr1_0)). % 5.98/2.27 tff(c_2, plain, (c4_0)). % 5.98/2.27 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 5.98/2.27 %------------------------------------------------------------------------------