%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SYN537-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 : n026.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:51 PM UTC 2025 % Result : Satisfiable 5.79s 2.26s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SYN537-1 : TPTP v9.0.0. Released v2.1.0. % 0.12/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 : n026.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:57:38 EDT 2025 % 0.13/0.34 % CPUTime : % 5.79/2.26 % 5.79/2.26 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 5.79/2.26 % 5.79/2.26 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 5.79/2.27 %$ c5_2 > c4_2 > c3_2 > c2_2 > c1_2 > ssSkP0 > ndr1_1 > c5_1 > c4_1 > c3_1 > c2_1 > c1_1 > #nlpp > ssSkC5 > ssSkC4 > ssSkC3 > ssSkC2 > ssSkC1 > ssSkC0 > ndr1_0 > c5_0 > c4_0 > c3_0 > c2_0 > c1_0 > a680 > a679 > a678 > a677 > a676 > a675 > a674 > a673 > a672 > a670 > a669 > a668 > a667 > a666 > a665 > a662 > a661 > a660 > a659 > a658 > a657 > a656 > a655 > a654 > a653 > a652 > a651 > a650 > a649 > a648 > a647 > a644 > a643 > a640 % 5.79/2.27 % 5.79/2.27 %Foreground sorts: % 5.79/2.27 % 5.79/2.27 % 5.79/2.27 %Background operators: % 5.79/2.27 % 5.79/2.27 % 5.79/2.27 %Foreground operators: % 5.79/2.27 tff(a679, type, a679: $i). % 5.79/2.27 tff(a658, type, a658: $i). % 5.79/2.27 tff(a662, type, a662: $i). % 5.79/2.27 tff(c4_0, type, c4_0: $o). % 5.79/2.27 tff(a669, type, a669: $i). % 5.79/2.27 tff(ssSkP0, type, ssSkP0: $i > $o). % 5.79/2.27 tff(a672, type, a672: $i). % 5.79/2.27 tff(a648, type, a648: $i). % 5.79/2.27 tff(c3_0, type, c3_0: $o). % 5.79/2.27 tff(a640, type, a640: $i). % 5.79/2.27 tff(c1_2, type, c1_2: ($i * $i) > $o). % 5.79/2.27 tff(ssSkC3, type, ssSkC3: $o). % 5.79/2.27 tff(a649, type, a649: $i). % 5.79/2.27 tff(a661, type, a661: $i). % 5.79/2.27 tff(a655, type, a655: $i). % 5.79/2.27 tff(a680, type, a680: $i). % 5.79/2.27 tff(ssSkC4, type, ssSkC4: $o). % 5.79/2.27 tff(a665, type, a665: $i). % 5.79/2.27 tff(c5_0, type, c5_0: $o). % 5.79/2.27 tff(a677, type, a677: $i). % 5.79/2.27 tff(a678, type, a678: $i). % 5.79/2.27 tff(a650, type, a650: $i). % 5.79/2.27 tff(a670, type, a670: $i). % 5.79/2.27 tff(c1_0, type, c1_0: $o). % 5.79/2.27 tff(a644, type, a644: $i). % 5.79/2.27 tff(c2_1, type, c2_1: $i > $o). % 5.79/2.27 tff(ndr1_1, type, ndr1_1: $i > $o). % 5.79/2.27 tff(c2_0, type, c2_0: $o). % 5.79/2.27 tff(c4_1, type, c4_1: $i > $o). % 5.79/2.27 tff(a654, type, a654: $i). % 5.79/2.27 tff(a673, type, a673: $i). % 5.79/2.27 tff(a659, type, a659: $i). % 5.79/2.27 tff(a643, type, a643: $i). % 5.79/2.27 tff(a668, type, a668: $i). % 5.79/2.27 tff(ndr1_0, type, ndr1_0: $o). % 5.79/2.27 tff(a666, type, a666: $i). % 5.79/2.27 tff(a657, type, a657: $i). % 5.79/2.27 tff(a674, type, a674: $i). % 5.79/2.27 tff(a667, type, a667: $i). % 5.79/2.27 tff(a676, type, a676: $i). % 5.79/2.27 tff(c1_1, type, c1_1: $i > $o). % 5.79/2.27 tff(a652, type, a652: $i). % 5.79/2.27 tff(ssSkC2, type, ssSkC2: $o). % 5.79/2.27 tff(c5_2, type, c5_2: ($i * $i) > $o). % 5.79/2.27 tff(a675, type, a675: $i). % 5.79/2.27 tff(c4_2, type, c4_2: ($i * $i) > $o). % 5.79/2.27 tff(ssSkC1, type, ssSkC1: $o). % 5.79/2.27 tff(ssSkC0, type, ssSkC0: $o). % 5.79/2.27 tff(a660, type, a660: $i). % 5.79/2.27 tff(ssSkC5, type, ssSkC5: $o). % 5.79/2.27 tff(a653, type, a653: $i). % 5.79/2.27 tff(a651, type, a651: $i). % 5.79/2.27 tff(c5_1, type, c5_1: $i > $o). % 5.79/2.27 tff(c3_2, type, c3_2: ($i * $i) > $o). % 5.79/2.27 tff(c2_2, type, c2_2: ($i * $i) > $o). % 5.79/2.27 tff(a656, type, a656: $i). % 5.79/2.27 tff(a647, type, a647: $i). % 5.79/2.27 tff(c3_1, type, c3_1: $i > $o). % 5.79/2.27 % 5.79/2.27 %Saturated clause set: % 6.14/2.27 tff(c_561, plain, (~c2_1(a648))). % 6.14/2.27 tff(c_560, plain, (~c4_1(a648))). % 6.14/2.27 tff(c_548, plain, (~ndr1_1(a648))). % 6.14/2.27 tff(c_538, plain, (~c3_1(a648))). % 6.14/2.27 tff(c_520, plain, (![U_49]: (c4_1(U_49) | c1_2(U_49, a658) | ~ndr1_1(U_49) | ~c2_2(U_49, a658) | c5_2(U_49, a658)))). % 6.14/2.27 tff(c_507, plain, (![U_49, V_50]: (c4_1(U_49) | c5_2(U_49, a658) | c1_2(U_49, V_50) | c5_2(U_49, V_50) | ~ndr1_1(U_49) | ~c2_2(U_49, V_50)))). % 6.14/2.28 tff(c_492, plain, (![U_47, V_48]: (c4_1(U_47) | c4_2(U_47, a658) | c1_2(U_47, V_48) | c5_2(U_47, V_48) | ~ndr1_1(U_47) | ~c2_2(U_47, V_48)))). % 6.14/2.28 tff(c_472, plain, (~c4_1(a672))). % 6.14/2.28 tff(c_468, plain, (~c2_1(a672))). % 6.14/2.28 tff(c_456, plain, (~ndr1_1(a672))). % 6.14/2.28 tff(c_439, plain, (ssSkP0(a659))). % 6.14/2.28 tff(c_453, plain, (~c2_1(a679))). % 6.14/2.28 tff(c_440, plain, (~ndr1_1(a679))). % 6.14/2.28 tff(c_435, plain, (~c1_2(a659, a649))). % 6.14/2.28 tff(c_427, plain, (![U_33]: (c5_2(a659, U_33) | ~c3_2(a659, U_33) | ~c1_2(a659, U_33)))). % 6.14/2.28 tff(c_428, plain, (ndr1_1(a659))). % 6.14/2.28 tff(c_404, plain, (~c4_1(a665))). % 6.14/2.28 tff(c_403, plain, (~c2_1(a665))). % 6.14/2.28 tff(c_390, plain, (~ndr1_1(a665))). % 6.14/2.28 tff(c_384, plain, (![U_29]: (c1_1(U_29) | ~c2_1(U_29) | ~c1_2(U_29, a647)))). % 6.14/2.28 tff(c_377, plain, (~c4_1(a666))). % 6.14/2.28 tff(c_375, plain, (~c2_1(a666))). % 6.14/2.28 tff(c_380, plain, (![U_18]: (c5_1(U_18) | ~c2_1(U_18) | ~c1_2(U_18, a656)))). % 6.14/2.28 tff(c_363, plain, (~ndr1_1(a666))). % 6.14/2.28 tff(c_360, plain, (![U_21]: (c1_1(U_21) | c5_2(U_21, a647) | ~c2_1(U_21)))). % 6.14/2.28 tff(c_356, plain, (![U_28]: (c1_1(U_28) | ~c2_1(U_28) | ~c2_2(U_28, a647)))). % 6.14/2.28 tff(c_352, plain, (![U_19]: (c5_1(U_19) | ~c2_1(U_19) | ~c3_2(U_19, a656)))). % 6.14/2.28 tff(c_348, plain, (![U_17]: (c5_1(U_17) | ~c2_1(U_17) | ~c2_2(U_17, a656)))). % 6.14/2.28 tff(c_345, plain, (~ssSkC3)). % 6.14/2.28 tff(c_340, plain, (![U_14]: (c1_1(U_14) | ndr1_1(U_14) | ~c2_1(U_14)))). % 6.14/2.28 tff(c_334, plain, (![U_20]: (~c4_1(U_20) | ~c3_2(U_20, a650) | ~ssSkP0(U_20)))). % 6.14/2.28 tff(c_331, plain, (![U_6]: (c5_1(U_6) | ndr1_1(U_6) | ~c2_1(U_6)))). % 6.14/2.28 tff(c_325, plain, (![U_12]: (c5_2(U_12, a650) | ~c4_1(U_12) | ~ssSkP0(U_12)))). % 6.14/2.28 tff(c_322, plain, (![U_13]: (c4_2(U_13, a650) | ~c4_1(U_13) | ~ssSkP0(U_13)))). % 6.14/2.28 tff(c_319, plain, (![U_1]: (~c4_1(U_1) | ndr1_1(U_1)))). % 6.14/2.28 tff(c_306, plain, (ssSkC1)). % 6.14/2.28 tff(c_303, plain, (~c2_2(a660, a662))). % 6.14/2.28 tff(c_302, plain, (~c4_2(a660, a661))). % 6.14/2.28 tff(c_301, plain, (~c4_2(a660, a662))). % 6.14/2.28 tff(c_70, plain, (![U_3]: (ssSkP0(U_3) | c1_2(U_3, a649)))). % 6.14/2.28 tff(c_299, plain, (~c5_2(a660, a662))). % 6.14/2.28 tff(c_296, plain, (~c3_2(a660, a661))). % 6.14/2.28 tff(c_90, plain, (![U_4]: (ssSkP0(U_4) | ~c5_2(U_4, a649)))). % 6.14/2.28 tff(c_68, plain, (![U_2]: (ssSkP0(U_2) | c4_2(U_2, a649)))). % 6.14/2.28 tff(c_293, plain, (c2_2(a660, a661))). % 6.14/2.28 tff(c_292, plain, (ndr1_1(a660))). % 6.14/2.28 tff(c_291, plain, (c3_1(a665))). % 6.14/2.28 tff(c_34, plain, (![U_1]: (ssSkP0(U_1) | ndr1_1(U_1)))). % 6.14/2.28 tff(c_288, plain, (c5_2(a643, a644))). % 6.14/2.28 tff(c_287, plain, (~c5_1(a665))). % 6.14/2.28 tff(c_286, plain, (~ssSkC4)). % 6.14/2.28 tff(c_285, plain, (~ssSkC2)). % 6.14/2.28 tff(c_283, plain, (~c4_1(a660))). % 6.14/2.28 tff(c_282, plain, (~c2_2(a643, a644))). % 6.14/2.28 tff(c_281, plain, (~c1_1(a659))). % 6.14/2.28 tff(c_280, plain, (~c4_1(a679))). % 6.14/2.28 tff(c_279, plain, (c4_1(a643))). % 6.14/2.28 tff(c_276, plain, (~c5_1(a672))). % 6.14/2.28 tff(c_275, plain, (~c1_1(a672))). % 6.14/2.28 tff(c_274, plain, (~c1_1(a666))). % 6.14/2.28 tff(c_273, plain, (~c4_1(a678))). % 6.14/2.28 tff(c_272, plain, (~c5_0)). % 6.14/2.28 tff(c_271, plain, (c3_1(a666))). % 6.14/2.28 tff(c_268, plain, (c2_1(a659))). % 6.14/2.28 tff(c_266, plain, (~c2_1(a678))). % 6.14/2.28 tff(c_265, plain, (~c5_1(a679))). % 6.14/2.28 tff(c_264, plain, (~c1_1(a643))). % 6.14/2.28 tff(c_263, plain, (ndr1_1(a643))). % 6.14/2.28 tff(c_262, plain, (~c1_1(a669))). % 6.14/2.28 tff(c_255, plain, (ndr1_0)). % 6.14/2.28 tff(c_254, plain, (~c2_0)). % 6.14/2.28 tff(c_253, plain, (~c4_0)). % 6.14/2.28 tff(c_2, plain, (c1_0)). % 6.14/2.28 tff(c_6, plain, (~c3_0)). % 6.14/2.28 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 6.14/2.28 %------------------------------------------------------------------------------