%------------------------------------------------------------------------------ % 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/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:51 PM UTC 2025 % Result : CounterSatisfiable 6.46s 2.34s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SYN537+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/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.13/0.34 % Computer : n006.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:22 EDT 2025 % 0.13/0.35 % CPUTime : % 6.46/2.34 % 6.46/2.34 % SZS status CounterSatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 6.46/2.34 % 6.46/2.34 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 6.46/2.35 %$ c5_2 > c4_2 > c3_2 > c2_2 > c1_2 > ndr1_1 > c5_1 > c4_1 > c3_1 > c2_1 > c1_1 > #nlpp > ndr1_0 > c5_0 > c4_0 > c3_0 > c2_0 > c1_0 > a680 > a679 > a678 > a677 > a676 > a675 > a674 > a673 > a672 > a671 > a670 > a669 > a668 > a667 > a666 > a665 > a664 > a663 > a662 > a661 > a660 > a659 > a658 > a657 > a656 > a655 > a654 > a653 > a652 > a651 > a650 > a649 > a648 > a647 > a646 > a645 > a644 > a643 > a642 > a641 > a640 % 6.46/2.35 % 6.46/2.35 %Foreground sorts: % 6.46/2.35 % 6.46/2.35 % 6.46/2.35 %Background operators: % 6.46/2.35 % 6.46/2.35 % 6.46/2.35 %Foreground operators: % 6.46/2.35 tff(a679, type, a679: $i). % 6.46/2.35 tff(a658, type, a658: $i). % 6.46/2.35 tff(a662, type, a662: $i). % 6.46/2.35 tff(c4_0, type, c4_0: $o). % 6.46/2.35 tff(a669, type, a669: $i). % 6.46/2.35 tff(a672, type, a672: $i). % 6.46/2.35 tff(a648, type, a648: $i). % 6.46/2.35 tff(c3_0, type, c3_0: $o). % 6.46/2.35 tff(a640, type, a640: $i). % 6.46/2.35 tff(c1_2, type, c1_2: ($i * $i) > $o). % 6.46/2.35 tff(a649, type, a649: $i). % 6.46/2.35 tff(a661, type, a661: $i). % 6.46/2.35 tff(a655, type, a655: $i). % 6.46/2.35 tff(a680, type, a680: $i). % 6.46/2.35 tff(a665, type, a665: $i). % 6.46/2.35 tff(c5_0, type, c5_0: $o). % 6.46/2.35 tff(a677, type, a677: $i). % 6.46/2.35 tff(a678, type, a678: $i). % 6.46/2.35 tff(a650, type, a650: $i). % 6.46/2.35 tff(a642, type, a642: $i). % 6.46/2.35 tff(a670, type, a670: $i). % 6.46/2.35 tff(a645, type, a645: $i). % 6.46/2.35 tff(c1_0, type, c1_0: $o). % 6.46/2.35 tff(a644, type, a644: $i). % 6.46/2.35 tff(c2_1, type, c2_1: $i > $o). % 6.46/2.35 tff(ndr1_1, type, ndr1_1: $i > $o). % 6.46/2.35 tff(c2_0, type, c2_0: $o). % 6.46/2.35 tff(c4_1, type, c4_1: $i > $o). % 6.46/2.35 tff(a664, type, a664: $i). % 6.46/2.35 tff(a654, type, a654: $i). % 6.46/2.35 tff(a673, type, a673: $i). % 6.46/2.35 tff(a671, type, a671: $i). % 6.46/2.35 tff(a641, type, a641: $i). % 6.46/2.35 tff(a663, type, a663: $i). % 6.46/2.35 tff(a659, type, a659: $i). % 6.46/2.35 tff(a643, type, a643: $i). % 6.46/2.35 tff(a668, type, a668: $i). % 6.46/2.35 tff(ndr1_0, type, ndr1_0: $o). % 6.46/2.35 tff(a666, type, a666: $i). % 6.46/2.35 tff(a657, type, a657: $i). % 6.46/2.35 tff(a674, type, a674: $i). % 6.46/2.35 tff(a667, type, a667: $i). % 6.46/2.35 tff(a676, type, a676: $i). % 6.46/2.35 tff(c1_1, type, c1_1: $i > $o). % 6.46/2.35 tff(a652, type, a652: $i). % 6.46/2.35 tff(c5_2, type, c5_2: ($i * $i) > $o). % 6.46/2.35 tff(a675, type, a675: $i). % 6.46/2.35 tff(c4_2, type, c4_2: ($i * $i) > $o). % 6.46/2.35 tff(a660, type, a660: $i). % 6.46/2.35 tff(a653, type, a653: $i). % 6.46/2.35 tff(a651, type, a651: $i). % 6.46/2.35 tff(a646, type, a646: $i). % 6.46/2.35 tff(c5_1, type, c5_1: $i > $o). % 6.46/2.35 tff(c3_2, type, c3_2: ($i * $i) > $o). % 6.46/2.35 tff(c2_2, type, c2_2: ($i * $i) > $o). % 6.46/2.35 tff(a656, type, a656: $i). % 6.46/2.35 tff(a647, type, a647: $i). % 6.46/2.35 tff(c3_1, type, c3_1: $i > $o). % 6.46/2.35 % 6.46/2.35 %Saturated clause set: % 6.46/2.35 tff(c_903, plain, (~c2_1(a648))). % 6.46/2.35 tff(c_902, plain, (~c4_1(a648))). % 6.46/2.35 tff(c_890, plain, (~ndr1_1(a648))). % 6.46/2.35 tff(c_888, plain, (~c3_1(a648))). % 6.46/2.35 tff(c_868, plain, (![X18_30, X19_32]: (c4_2(X18_30, a658) | c1_2(X18_30, X19_32) | ~c2_2(X18_30, X19_32) | c5_2(X18_30, X19_32) | ~ndr1_1(X18_30) | c4_1(X18_30)))). % 6.46/2.35 tff(c_838, plain, (![X18_30]: (c1_2(X18_30, a658) | ~c2_2(X18_30, a658) | ~ndr1_1(X18_30) | c4_1(X18_30) | c5_2(X18_30, a658)))). % 6.46/2.36 tff(c_825, plain, (![X18_30, X19_32]: (c5_2(X18_30, a658) | c1_2(X18_30, X19_32) | ~c2_2(X18_30, X19_32) | c5_2(X18_30, X19_32) | ~ndr1_1(X18_30) | c4_1(X18_30)))). % 6.46/2.36 tff(c_802, plain, (~c2_1(a672))). % 6.46/2.36 tff(c_806, plain, (~c4_1(a672))). % 6.46/2.36 tff(c_790, plain, (~ndr1_1(a672))). % 6.46/2.36 tff(c_786, plain, (~c1_2(a659, a649))). % 6.46/2.36 tff(c_773, plain, (![X20_33]: (~c3_2(a659, X20_33) | ~c1_2(a659, X20_33) | c5_2(a659, X20_33)))). % 6.46/2.36 tff(c_774, plain, (ndr1_1(a659))). % 6.46/2.36 tff(c_750, plain, (~c2_1(a680))). % 6.46/2.36 tff(c_749, plain, (~c4_1(a680))). % 6.46/2.36 tff(c_737, plain, (~ndr1_1(a680))). % 6.46/2.36 tff(c_733, plain, (~c1_1(a672))). % 6.46/2.36 tff(c_731, plain, (~c5_1(a672))). % 6.46/2.36 tff(c_728, plain, (![X2_10]: (~c2_2(X2_10, a647) | ~c2_1(X2_10) | c1_1(X2_10)))). % 6.46/2.36 tff(c_726, plain, (![X2_10]: (~c1_2(X2_10, a647) | ~c2_1(X2_10) | c1_1(X2_10)))). % 6.46/2.36 tff(c_722, plain, (![X16_28]: (~c2_2(X16_28, a656) | ~c2_1(X16_28) | c5_1(X16_28)))). % 6.46/2.36 tff(c_633, plain, (![X8_18]: (~c5_2(X8_18, a649) | ~c3_2(X8_18, a650) | ~c4_1(X8_18)))). % 6.46/2.36 tff(c_635, plain, (![X8_18]: (~c5_2(X8_18, a649) | c4_2(X8_18, a650) | ~c4_1(X8_18)))). % 6.46/2.36 tff(c_718, plain, (![X2_10]: (c5_2(X2_10, a647) | ~c2_1(X2_10) | c1_1(X2_10)))). % 6.46/2.36 tff(c_630, plain, (![X8_18]: (~c5_2(X8_18, a649) | c5_2(X8_18, a650) | ~c4_1(X8_18)))). % 6.46/2.36 tff(c_631, plain, (![X8_18]: (c4_2(X8_18, a649) | ~c3_2(X8_18, a650) | ~c4_1(X8_18)))). % 6.46/2.36 tff(c_616, plain, (![X8_18]: (c4_2(X8_18, a649) | c4_2(X8_18, a650) | ~c4_1(X8_18)))). % 6.46/2.36 tff(c_629, plain, (![X8_18]: (c1_2(X8_18, a649) | c5_2(X8_18, a650) | ~c4_1(X8_18)))). % 6.46/2.36 tff(c_632, plain, (![X8_18]: (c1_2(X8_18, a649) | ~c3_2(X8_18, a650) | ~c4_1(X8_18)))). % 6.46/2.36 tff(c_634, plain, (![X8_18]: (c1_2(X8_18, a649) | c4_2(X8_18, a650) | ~c4_1(X8_18)))). % 6.46/2.36 tff(c_628, plain, (![X8_18]: (c4_2(X8_18, a649) | c5_2(X8_18, a650) | ~c4_1(X8_18)))). % 6.46/2.36 tff(c_708, plain, (![X16_28]: (~c3_2(X16_28, a656) | ~c2_1(X16_28) | c5_1(X16_28)))). % 6.46/2.36 tff(c_706, plain, (![X16_28]: (~c1_2(X16_28, a656) | ~c2_1(X16_28) | c5_1(X16_28)))). % 6.46/2.36 tff(c_703, plain, (~c2_1(a665))). % 6.46/2.36 tff(c_705, plain, (~c4_1(a665))). % 6.46/2.36 tff(c_691, plain, (~ndr1_1(a665))). % 6.46/2.36 tff(c_688, plain, (![X16_28]: (ndr1_1(X16_28) | ~c2_1(X16_28) | c5_1(X16_28)))). % 6.46/2.36 tff(c_686, plain, (![X2_10]: (ndr1_1(X2_10) | ~c2_1(X2_10) | c1_1(X2_10)))). % 6.46/2.36 tff(c_683, plain, (~c3_1(a680))). % 6.46/2.36 tff(c_682, plain, (~c4_2(a667, a668))). % 6.46/2.36 tff(c_680, plain, (~c1_2(a667, a668))). % 6.46/2.36 tff(c_675, plain, (~c4_1(a667))). % 6.46/2.36 tff(c_673, plain, (ndr1_1(a667))). % 6.46/2.36 tff(c_671, plain, (c2_2(a660, a661))). % 6.46/2.36 tff(c_670, plain, (~c2_2(a660, a662))). % 6.46/2.36 tff(c_669, plain, (~c5_2(a660, a662))). % 6.46/2.36 tff(c_668, plain, (~c4_2(a660, a662))). % 6.46/2.36 tff(c_667, plain, (~c4_2(a660, a661))). % 6.46/2.36 tff(c_666, plain, (~c3_2(a660, a661))). % 6.46/2.36 tff(c_665, plain, (ndr1_1(a660))). % 6.46/2.36 tff(c_664, plain, (~c5_1(a665))). % 6.46/2.36 tff(c_615, plain, (![X8_18]: (ndr1_1(X8_18) | ~c4_1(X8_18)))). % 6.46/2.36 tff(c_662, plain, (~c4_1(a660))). % 6.46/2.36 tff(c_661, plain, (c3_1(a665))). % 6.46/2.36 tff(c_660, plain, (~c1_1(a659))). % 6.46/2.36 tff(c_659, plain, (c2_1(a659))). % 6.46/2.36 tff(c_657, plain, (~c2_0)). % 6.46/2.36 tff(c_656, plain, (~c5_0)). % 6.46/2.36 tff(c_655, plain, (~c4_0)). % 6.46/2.36 tff(c_2, plain, (c1_0)). % 6.46/2.36 tff(c_4, plain, (~c3_0)). % 6.46/2.36 tff(c_86, plain, (ndr1_0)). % 6.46/2.36 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 6.46/2.36 %------------------------------------------------------------------------------