%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SYN529-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 : n004.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.86s 2.25s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SYN529-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.12/0.34 % Computer : n004.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:52 EDT 2025 % 0.12/0.35 % CPUTime : % 5.86/2.25 % 5.86/2.25 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 5.86/2.25 % 5.86/2.25 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 5.86/2.26 %$ c5_2 > c4_2 > c3_2 > c2_2 > c1_2 > ssSkP0 > ndr1_1 > c5_1 > c4_1 > c3_1 > c2_1 > c1_1 > #nlpp > ssSkC8 > ssSkC7 > ssSkC6 > ssSkC5 > ssSkC4 > ssSkC3 > ssSkC2 > ssSkC1 > ssSkC0 > ndr1_0 > c5_0 > c4_0 > c3_0 > c2_0 > c1_0 > a356 > a355 > a354 > a353 > a352 > a351 > a350 > a349 > a348 > a347 > a346 > a345 > a344 > a343 > a342 > a341 > a340 > a339 > a338 > a337 > a336 > a335 > a334 > a333 > a332 > a331 > a330 > a329 > a328 > a327 > a326 > a325 > a324 > a323 > a322 > a321 > a320 > a319 > a318 > a317 > a316 > a315 > a314 % 5.86/2.26 % 5.86/2.26 %Foreground sorts: % 5.86/2.26 % 5.86/2.26 % 5.86/2.26 %Background operators: % 5.86/2.26 % 5.86/2.26 % 5.86/2.26 %Foreground operators: % 5.86/2.26 tff(a323, type, a323: $i). % 5.86/2.26 tff(ssSkC8, type, ssSkC8: $o). % 5.86/2.26 tff(a316, type, a316: $i). % 5.86/2.26 tff(a347, type, a347: $i). % 5.86/2.26 tff(ssSkC7, type, ssSkC7: $o). % 5.86/2.26 tff(a322, type, a322: $i). % 5.86/2.26 tff(a336, type, a336: $i). % 5.86/2.26 tff(c4_0, type, c4_0: $o). % 5.86/2.26 tff(a335, type, a335: $i). % 5.86/2.26 tff(a326, type, a326: $i). % 5.86/2.26 tff(ssSkP0, type, ssSkP0: $i > $o). % 5.86/2.26 tff(ssSkC6, type, ssSkC6: $o). % 5.86/2.26 tff(c3_0, type, c3_0: $o). % 5.86/2.26 tff(a338, type, a338: $i). % 5.86/2.26 tff(c1_2, type, c1_2: ($i * $i) > $o). % 5.86/2.26 tff(a334, type, a334: $i). % 5.86/2.26 tff(a337, type, a337: $i). % 5.86/2.26 tff(ssSkC3, type, ssSkC3: $o). % 5.86/2.26 tff(a320, type, a320: $i). % 5.86/2.26 tff(a354, type, a354: $i). % 5.86/2.26 tff(a348, type, a348: $i). % 5.86/2.26 tff(a341, type, a341: $i). % 5.86/2.26 tff(a342, type, a342: $i). % 5.86/2.26 tff(a355, type, a355: $i). % 5.86/2.26 tff(a330, type, a330: $i). % 5.86/2.26 tff(ssSkC4, type, ssSkC4: $o). % 5.86/2.26 tff(a314, type, a314: $i). % 5.86/2.26 tff(a321, type, a321: $i). % 5.86/2.26 tff(a318, type, a318: $i). % 5.86/2.26 tff(c5_0, type, c5_0: $o). % 5.86/2.26 tff(a329, type, a329: $i). % 5.86/2.26 tff(a353, type, a353: $i). % 5.86/2.26 tff(a343, type, a343: $i). % 5.86/2.26 tff(c1_0, type, c1_0: $o). % 5.86/2.26 tff(a331, type, a331: $i). % 5.86/2.26 tff(c2_1, type, c2_1: $i > $o). % 5.86/2.26 tff(ndr1_1, type, ndr1_1: $i > $o). % 5.86/2.26 tff(c2_0, type, c2_0: $o). % 5.86/2.26 tff(c4_1, type, c4_1: $i > $o). % 5.86/2.26 tff(a333, type, a333: $i). % 5.86/2.26 tff(a345, type, a345: $i). % 5.86/2.26 tff(a352, type, a352: $i). % 5.86/2.26 tff(a327, type, a327: $i). % 5.86/2.26 tff(ndr1_0, type, ndr1_0: $o). % 5.86/2.26 tff(a344, type, a344: $i). % 5.86/2.26 tff(a351, type, a351: $i). % 5.86/2.26 tff(a317, type, a317: $i). % 5.86/2.26 tff(a349, type, a349: $i). % 5.86/2.26 tff(a324, type, a324: $i). % 5.86/2.26 tff(c1_1, type, c1_1: $i > $o). % 5.86/2.26 tff(ssSkC2, type, ssSkC2: $o). % 5.86/2.26 tff(c5_2, type, c5_2: ($i * $i) > $o). % 5.86/2.26 tff(a340, type, a340: $i). % 5.86/2.26 tff(a315, type, a315: $i). % 5.86/2.26 tff(c4_2, type, c4_2: ($i * $i) > $o). % 5.86/2.26 tff(ssSkC1, type, ssSkC1: $o). % 5.86/2.26 tff(ssSkC0, type, ssSkC0: $o). % 5.86/2.26 tff(ssSkC5, type, ssSkC5: $o). % 5.86/2.26 tff(a319, type, a319: $i). % 5.86/2.26 tff(a328, type, a328: $i). % 5.86/2.26 tff(a332, type, a332: $i). % 5.86/2.26 tff(c5_1, type, c5_1: $i > $o). % 5.86/2.26 tff(a346, type, a346: $i). % 5.86/2.26 tff(c3_2, type, c3_2: ($i * $i) > $o). % 5.86/2.26 tff(a350, type, a350: $i). % 5.86/2.26 tff(c2_2, type, c2_2: ($i * $i) > $o). % 5.86/2.26 tff(a325, type, a325: $i). % 5.86/2.26 tff(a339, type, a339: $i). % 5.86/2.26 tff(a356, type, a356: $i). % 5.86/2.26 tff(c3_1, type, c3_1: $i > $o). % 5.86/2.26 % 5.86/2.26 %Saturated clause set: % 5.86/2.26 tff(c_695, plain, (c4_1(a344))). % 5.86/2.26 tff(c_677, plain, (c4_2(a348, a349))). % 5.86/2.26 tff(c_659, plain, (c4_2(a331, a332))). % 5.86/2.26 tff(c_650, plain, (c4_1(a355))). % 5.86/2.27 tff(c_628, plain, (![U_37, W_39]: (c2_1(U_37) | c4_1(U_37) | c4_2(U_37, W_39) | c5_2(U_37, W_39) | ~ndr1_1(U_37)))). % 5.86/2.27 tff(c_583, plain, (![U_27, V_28]: (c5_2(U_27, V_28) | c1_2(U_27, V_28) | ~c3_1(U_27) | ~c3_2(U_27, a350) | ~ndr1_1(U_27) | ~c4_2(U_27, V_28)))). % 5.86/2.27 tff(c_569, plain, (![U_41, V_42]: (c5_2(U_41, a321) | c2_2(U_41, V_42) | ~c2_1(U_41) | ~ndr1_1(U_41) | ~c3_2(U_41, V_42) | ~c4_2(U_41, V_42)))). % 5.86/2.27 tff(c_540, plain, (![U_29, V_30]: (c5_2(U_29, V_30) | c1_2(U_29, V_30) | ~c3_1(U_29) | ~c1_2(U_29, a350) | ~ndr1_1(U_29) | ~c4_2(U_29, V_30)))). % 5.86/2.27 tff(c_523, plain, (![U_49, V_50]: (c2_2(U_49, V_50) | ~c2_1(U_49) | ~c1_2(U_49, a321) | ~ndr1_1(U_49) | ~c3_2(U_49, V_50) | ~c4_2(U_49, V_50)))). % 5.86/2.27 tff(c_494, plain, (![U_21, V_22]: (c2_2(U_21, a350) | c5_2(U_21, V_22) | c1_2(U_21, V_22) | ~c3_1(U_21) | ~ndr1_1(U_21) | ~c4_2(U_21, V_22)))). % 5.86/2.27 tff(c_492, plain, (~c2_1(a324))). % 5.86/2.27 tff(c_491, plain, (~c2_1(a355))). % 5.86/2.27 tff(c_475, plain, (![U_51, V_52]: (c2_2(U_51, V_52) | ~c2_1(U_51) | ~c2_2(U_51, a321) | ~ndr1_1(U_51) | ~c3_2(U_51, V_52) | ~c4_2(U_51, V_52)))). % 5.86/2.27 tff(c_472, plain, (~c2_1(a338))). % 5.86/2.27 tff(c_432, plain, (![U_19, V_20]: (c3_1(U_19) | c2_2(U_19, V_20) | c3_2(U_19, V_20) | c4_2(U_19, V_20) | ~c2_1(U_19) | ~ndr1_1(U_19)))). % 5.86/2.27 tff(c_425, plain, (![U_18]: (~c5_2(a344, U_18) | ~c1_2(a344, U_18) | ~c2_2(a344, U_18)))). % 5.86/2.27 tff(c_422, plain, (ssSkC7)). % 5.86/2.27 tff(c_413, plain, (![U_13]: (c2_2(a324, U_13) | c3_2(a324, U_13) | ~c4_2(a324, U_13)))). % 5.86/2.27 tff(c_410, plain, (c2_0)). % 5.86/2.27 tff(c_403, plain, (![U_8]: (c5_1(U_8) | c3_1(U_8) | c2_2(U_8, a334)))). % 5.86/2.27 tff(c_399, plain, (![U_7]: (c5_1(U_7) | c3_1(U_7) | c4_2(U_7, a334)))). % 5.86/2.27 tff(c_393, plain, (![U_11]: (c1_2(a324, U_11) | c3_2(a324, U_11)))). % 5.86/2.27 tff(c_389, plain, (![U_5]: (c5_1(U_5) | c3_1(U_5) | ndr1_1(U_5)))). % 5.86/2.27 tff(c_386, plain, (c4_0)). % 5.86/2.27 tff(c_170, plain, (![U_3]: (ssSkP0(U_3) | ~c4_2(U_3, a340)))). % 5.86/2.27 tff(c_381, plain, (c4_2(a335, a336))). % 5.86/2.27 tff(c_379, plain, (~c3_2(a335, a337))). % 5.86/2.27 tff(c_376, plain, (~c5_2(a355, a356))). % 5.86/2.27 tff(c_374, plain, (c5_2(a335, a336))). % 5.86/2.27 tff(c_172, plain, (![U_4]: (ssSkP0(U_4) | ~c1_2(U_4, a340)))). % 5.86/2.27 tff(c_371, plain, (~c4_2(a355, a356))). % 5.86/2.27 tff(c_369, plain, (c2_2(a335, a336))). % 5.86/2.27 tff(c_365, plain, (c5_2(a335, a337))). % 5.86/2.27 tff(c_114, plain, (![U_2]: (ssSkP0(U_2) | c2_2(U_2, a340)))). % 5.86/2.27 tff(c_359, plain, (c1_2(a335, a337))). % 5.86/2.27 tff(c_357, plain, (~c5_2(a348, a349))). % 5.86/2.27 tff(c_356, plain, (~c4_2(a351, a352))). % 5.86/2.27 tff(c_355, plain, (ndr1_1(a355))). % 5.86/2.27 tff(c_353, plain, (~ssSkC4)). % 5.86/2.27 tff(c_352, plain, (~c5_2(a331, a332))). % 5.86/2.27 tff(c_351, plain, (~c1_2(a351, a352))). % 5.86/2.27 tff(c_350, plain, (~ssSkC3)). % 5.86/2.27 tff(c_349, plain, (c5_2(a324, a325))). % 5.86/2.27 tff(c_346, plain, (~c3_2(a338, a339))). % 5.86/2.27 tff(c_344, plain, (~c3_1(a355))). % 5.86/2.27 tff(c_342, plain, (~c4_2(a338, a339))). % 5.86/2.27 tff(c_341, plain, (ndr1_1(a335))). % 5.86/2.27 tff(c_46, plain, (![U_1]: (ssSkP0(U_1) | ndr1_1(U_1)))). % 5.86/2.27 tff(c_338, plain, (~ssSkC0)). % 5.86/2.27 tff(c_337, plain, (c3_2(a344, a345))). % 5.86/2.27 tff(c_336, plain, (c2_2(a348, a349))). % 5.86/2.27 tff(c_335, plain, (~ssSkC1)). % 5.86/2.27 tff(c_334, plain, (c1_2(a338, a339))). % 5.86/2.27 tff(c_332, plain, (~ssSkC8)). % 5.86/2.27 tff(c_330, plain, (c2_2(a351, a352))). % 5.86/2.27 tff(c_329, plain, (~ssSkC2)). % 5.86/2.27 tff(c_327, plain, (~c4_2(a316, a317))). % 5.86/2.27 tff(c_326, plain, (~ssSkC6)). % 5.86/2.27 tff(c_324, plain, (c2_2(a316, a317))). % 5.86/2.27 tff(c_323, plain, (c1_2(a324, a325))). % 5.86/2.27 tff(c_322, plain, (c1_2(a331, a332))). % 5.86/2.27 tff(c_321, plain, (~c1_2(a344, a345))). % 5.86/2.27 tff(c_320, plain, (c2_2(a331, a332))). % 5.86/2.27 tff(c_319, plain, (c3_2(a316, a317))). % 5.86/2.27 tff(c_318, plain, (~c4_1(a316))). % 5.86/2.27 tff(c_317, plain, (c5_1(a331))). % 5.86/2.27 tff(c_316, plain, (c4_1(a338))). % 5.86/2.27 tff(c_315, plain, (c5_1(a328))). % 5.86/2.27 tff(c_314, plain, (ndr1_1(a316))). % 5.86/2.27 tff(c_313, plain, (c3_1(a331))). % 5.86/2.27 tff(c_312, plain, (ndr1_1(a324))). % 5.86/2.27 tff(c_311, plain, (ndr1_1(a344))). % 5.86/2.27 tff(c_309, plain, (~c1_1(a343))). % 5.86/2.27 tff(c_308, plain, (ndr1_1(a338))). % 5.86/2.27 tff(c_307, plain, (ndr1_1(a331))). % 5.86/2.27 tff(c_306, plain, (c1_1(a338))). % 5.86/2.27 tff(c_305, plain, (c1_1(a316))). % 5.86/2.27 tff(c_304, plain, (ndr1_1(a348))). % 5.86/2.27 tff(c_303, plain, (c4_1(a351))). % 5.86/2.28 tff(c_300, plain, (ndr1_1(a351))). % 5.86/2.28 tff(c_299, plain, (~c2_1(a344))). % 5.86/2.28 tff(c_298, plain, (~c1_0)). % 5.86/2.28 tff(c_296, plain, (~c3_1(a348))). % 5.86/2.28 tff(c_295, plain, (~c1_1(a351))). % 5.86/2.28 tff(c_286, plain, (c2_1(a343))). % 5.86/2.28 tff(c_285, plain, (~c2_1(a328))). % 5.86/2.28 tff(c_284, plain, (~c5_0)). % 5.86/2.28 tff(c_274, plain, (ndr1_0)). % 5.86/2.28 tff(c_273, plain, (~c3_0)). % 5.86/2.28 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 5.86/2.28 %------------------------------------------------------------------------------