%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SYN541-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 : n013.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:52 PM UTC 2025 % Result : Satisfiable 7.03s 2.40s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : SYN541-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.13/0.34 % Computer : n013.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:58:02 EDT 2025 % 0.13/0.34 % CPUTime : % 7.03/2.40 % 7.03/2.40 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 7.03/2.40 % 7.03/2.40 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 7.10/2.41 %$ c5_2 > c4_2 > c3_2 > c2_2 > c1_2 > 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 > a774 > a773 > a772 > a771 > a770 > a769 > a768 > a767 > a766 > a765 > a764 > a763 > a762 > a761 > a760 > a759 > a758 > a757 > a756 > a755 > a754 > a753 > a752 > a751 > a750 > a749 > a748 > a747 > a746 > a745 > a744 > a743 > a742 > a741 > a740 > a739 > a738 > a737 > a736 > a735 > a734 > a733 > a732 > a731 > a730 > a729 > a728 > a727 > a726 % 7.10/2.41 % 7.10/2.41 %Foreground sorts: % 7.10/2.41 % 7.10/2.41 % 7.10/2.41 %Background operators: % 7.10/2.41 % 7.10/2.41 % 7.10/2.41 %Foreground operators: % 7.10/2.41 tff(a750, type, a750: $i). % 7.10/2.41 tff(a760, type, a760: $i). % 7.10/2.41 tff(a749, type, a749: $i). % 7.10/2.41 tff(ssSkC7, type, ssSkC7: $o). % 7.10/2.41 tff(c4_0, type, c4_0: $o). % 7.10/2.41 tff(a748, type, a748: $i). % 7.10/2.41 tff(a768, type, a768: $i). % 7.10/2.41 tff(ssSkP0, type, ssSkP0: $i > $o). % 7.10/2.41 tff(a739, type, a739: $i). % 7.10/2.41 tff(a733, type, a733: $i). % 7.10/2.41 tff(ssSkC6, type, ssSkC6: $o). % 7.10/2.41 tff(c3_0, type, c3_0: $o). % 7.10/2.41 tff(a734, type, a734: $i). % 7.10/2.41 tff(a751, type, a751: $i). % 7.10/2.41 tff(a767, type, a767: $i). % 7.10/2.41 tff(c1_2, type, c1_2: ($i * $i) > $o). % 7.10/2.41 tff(a727, type, a727: $i). % 7.10/2.41 tff(a764, type, a764: $i). % 7.10/2.41 tff(a758, type, a758: $i). % 7.10/2.41 tff(ssSkC3, type, ssSkC3: $o). % 7.10/2.41 tff(a731, type, a731: $i). % 7.10/2.41 tff(a753, type, a753: $i). % 7.10/2.41 tff(a736, type, a736: $i). % 7.10/2.41 tff(a769, type, a769: $i). % 7.10/2.41 tff(a771, type, a771: $i). % 7.10/2.41 tff(a759, type, a759: $i). % 7.10/2.41 tff(a741, type, a741: $i). % 7.10/2.41 tff(a770, type, a770: $i). % 7.10/2.41 tff(a746, type, a746: $i). % 7.10/2.41 tff(a766, type, a766: $i). % 7.10/2.41 tff(a747, type, a747: $i). % 7.10/2.41 tff(ssSkC4, type, ssSkC4: $o). % 7.10/2.41 tff(c5_0, type, c5_0: $o). % 7.10/2.41 tff(a730, type, a730: $i). % 7.10/2.41 tff(a774, type, a774: $i). % 7.10/2.41 tff(a745, type, a745: $i). % 7.10/2.41 tff(a737, type, a737: $i). % 7.10/2.41 tff(c1_0, type, c1_0: $o). % 7.10/2.41 tff(a754, type, a754: $i). % 7.10/2.41 tff(a765, type, a765: $i). % 7.10/2.41 tff(a755, type, a755: $i). % 7.10/2.41 tff(a772, type, a772: $i). % 7.10/2.41 tff(a740, type, a740: $i). % 7.10/2.41 tff(a743, type, a743: $i). % 7.10/2.41 tff(c2_1, type, c2_1: $i > $o). % 7.10/2.41 tff(ndr1_1, type, ndr1_1: $i > $o). % 7.10/2.41 tff(c2_0, type, c2_0: $o). % 7.10/2.41 tff(c4_1, type, c4_1: $i > $o). % 7.10/2.41 tff(a738, type, a738: $i). % 7.10/2.41 tff(a728, type, a728: $i). % 7.10/2.41 tff(a763, type, a763: $i). % 7.10/2.41 tff(ndr1_0, type, ndr1_0: $o). % 7.10/2.41 tff(a742, type, a742: $i). % 7.10/2.41 tff(a726, type, a726: $i). % 7.10/2.41 tff(a752, type, a752: $i). % 7.10/2.41 tff(a729, type, a729: $i). % 7.10/2.41 tff(a732, type, a732: $i). % 7.10/2.41 tff(c1_1, type, c1_1: $i > $o). % 7.10/2.41 tff(a762, type, a762: $i). % 7.10/2.41 tff(a756, type, a756: $i). % 7.10/2.41 tff(ssSkC2, type, ssSkC2: $o). % 7.10/2.41 tff(a761, type, a761: $i). % 7.10/2.41 tff(c5_2, type, c5_2: ($i * $i) > $o). % 7.10/2.41 tff(a744, type, a744: $i). % 7.10/2.41 tff(c4_2, type, c4_2: ($i * $i) > $o). % 7.10/2.41 tff(a757, type, a757: $i). % 7.10/2.41 tff(ssSkC1, type, ssSkC1: $o). % 7.10/2.41 tff(ssSkC0, type, ssSkC0: $o). % 7.10/2.41 tff(ssSkC5, type, ssSkC5: $o). % 7.10/2.41 tff(c5_1, type, c5_1: $i > $o). % 7.10/2.41 tff(c3_2, type, c3_2: ($i * $i) > $o). % 7.10/2.41 tff(a773, type, a773: $i). % 7.10/2.41 tff(c2_2, type, c2_2: ($i * $i) > $o). % 7.10/2.41 tff(a735, type, a735: $i). % 7.10/2.41 tff(c3_1, type, c3_1: $i > $o). % 7.10/2.41 % 7.10/2.41 %Saturated clause set: % 7.10/2.41 tff(c_1047, plain, (~ssSkC4)). % 7.10/2.42 tff(c_952, plain, (![U_163, V_164]: (~c1_2(U_163, V_164) | ~c2_2(U_163, V_164) | c1_1(U_163) | c3_2(U_163, V_164) | ~c4_2(U_163, V_164) | c5_1(U_163) | c2_2(U_163, a754) | ~ndr1_1(U_163) | ~c1_2(U_163, a754)))). % 7.10/2.42 tff(c_950, plain, (![U_163, V_164]: (~c2_2(U_163, a766) | c1_1(U_163) | c3_2(U_163, V_164) | ~c4_2(U_163, V_164) | c5_1(U_163) | c2_2(U_163, a754) | ~ndr1_1(U_163) | ~c1_2(U_163, a754)))). % 7.10/2.42 tff(c_1005, plain, (~c1_2(a732, a754))). % 7.10/2.42 tff(c_951, plain, (![U_163, V_164]: (c3_2(U_163, a766) | c1_1(U_163) | c3_2(U_163, V_164) | ~c4_2(U_163, V_164) | c5_1(U_163) | c2_2(U_163, a754) | ~ndr1_1(U_163) | ~c1_2(U_163, a754)))). % 7.10/2.42 tff(c_949, plain, (![U_163, V_164]: (~c1_2(U_163, a766) | c1_1(U_163) | c3_2(U_163, V_164) | ~c4_2(U_163, V_164) | c5_1(U_163) | c2_2(U_163, a754) | ~ndr1_1(U_163) | ~c1_2(U_163, a754)))). % 7.10/2.42 tff(c_753, plain, (![U_53, V_149]: (c1_1(U_53) | c5_2(U_53, V_149) | c3_2(U_53, V_149) | ~c4_2(U_53, V_149) | c5_1(U_53) | c2_2(U_53, a754) | ~ndr1_1(U_53) | ~c1_2(U_53, a754)))). % 7.10/2.42 tff(c_724, plain, (![U_146, V_147]: (~c1_2(U_146, V_147) | ~c2_2(U_146, V_147) | c1_1(U_146) | c3_2(U_146, a754) | c3_2(U_146, V_147) | ~ndr1_1(U_146) | ~c4_2(U_146, V_147)))). % 7.10/2.42 tff(c_721, plain, (![U_146, V_147]: (c5_1(U_146) | ~c1_2(U_146, a766) | c1_1(U_146) | c3_2(U_146, a754) | c3_2(U_146, V_147) | ~ndr1_1(U_146) | ~c4_2(U_146, V_147)))). % 7.10/2.42 tff(c_722, plain, (![U_146, V_147]: (c5_1(U_146) | ~c2_2(U_146, a766) | c1_1(U_146) | c3_2(U_146, a754) | c3_2(U_146, V_147) | ~ndr1_1(U_146) | ~c4_2(U_146, V_147)))). % 7.10/2.42 tff(c_836, plain, (![U_72, W_74, V_73]: (c1_2(U_72, W_74) | c5_2(U_72, V_73) | c4_2(U_72, V_73) | ~c2_1(U_72) | ~c4_2(U_72, W_74) | ~ndr1_1(U_72) | ~c2_2(U_72, V_73)))). % 7.10/2.42 tff(c_835, plain, (~c2_2(a772, a773))). % 7.10/2.42 tff(c_805, plain, (c3_2(a763, a764))). % 7.10/2.42 tff(c_806, plain, (![U_77, V_78]: (c3_1(U_77) | c4_2(U_77, V_78) | ~c2_1(U_77) | ~ndr1_1(U_77) | ~c2_2(U_77, V_78) | ~c5_2(U_77, V_78)))). % 7.10/2.42 tff(c_804, plain, (~c1_2(a763, a766))). % 7.10/2.42 tff(c_803, plain, (~c2_2(a763, a764))). % 7.10/2.42 tff(c_779, plain, (c5_2(a763, a764))). % 7.10/2.42 tff(c_777, plain, (c3_2(a750, a751))). % 7.10/2.42 tff(c_776, plain, (c1_2(a763, a764))). % 7.10/2.42 tff(c_774, plain, (c3_2(a732, a754))). % 7.10/2.42 tff(c_723, plain, (![U_146, V_147]: (c5_1(U_146) | c3_2(U_146, a766) | c1_1(U_146) | c3_2(U_146, a754) | c3_2(U_146, V_147) | ~ndr1_1(U_146) | ~c4_2(U_146, V_147)))). % 7.10/2.42 tff(c_744, plain, (![U_66, V_67]: (c1_1(U_66) | c5_2(U_66, V_67) | c3_2(U_66, V_67) | ~c5_2(U_66, a754) | ~ndr1_1(U_66) | ~c4_2(U_66, V_67)))). % 7.10/2.42 tff(c_739, plain, (c3_2(a726, a754))). % 7.10/2.42 tff(c_741, plain, (ndr1_1(a763))). % 7.10/2.42 tff(c_738, plain, (~c4_2(a738, a740))). % 7.10/2.42 tff(c_737, plain, (c3_2(a726, a727))). % 7.10/2.42 tff(c_694, plain, (![U_56, V_57]: (c1_1(U_56) | c3_2(U_56, a754) | c5_2(U_56, V_57) | c3_2(U_56, V_57) | ~ndr1_1(U_56) | ~c4_2(U_56, V_57)))). % 7.10/2.42 tff(c_693, plain, (~ssSkC3)). % 7.10/2.42 tff(c_690, plain, (~c2_2(a732, a766))). % 7.10/2.42 tff(c_638, plain, (![U_137, V_138]: (c3_2(U_137, V_138) | ~c2_2(U_137, a766) | c5_1(U_137) | c2_2(U_137, V_138) | ~ndr1_1(U_137) | ~c1_2(U_137, V_138)))). % 7.10/2.42 tff(c_680, plain, (~c1_2(a732, a766))). % 7.10/2.42 tff(c_682, plain, (~c2_1(a763))). % 7.10/2.42 tff(c_637, plain, (![U_137, V_138]: (c3_2(U_137, V_138) | ~c1_2(U_137, a766) | c5_1(U_137) | c2_2(U_137, V_138) | ~ndr1_1(U_137) | ~c1_2(U_137, V_138)))). % 7.10/2.42 tff(c_668, plain, (![U_137]: (c5_1(U_137) | c2_2(U_137, a766) | ~ndr1_1(U_137) | ~c1_2(U_137, a766) | c3_2(U_137, a766)))). % 7.10/2.42 tff(c_639, plain, (![U_137, V_138]: (c3_2(U_137, a766) | c3_2(U_137, V_138) | c5_1(U_137) | c2_2(U_137, V_138) | ~ndr1_1(U_137) | ~c1_2(U_137, V_138)))). % 7.10/2.42 tff(c_655, plain, (c5_1(a726))). % 7.10/2.42 tff(c_654, plain, (~c3_0)). % 7.10/2.42 tff(c_653, plain, (c2_2(a738, a740))). % 7.10/2.42 tff(c_610, plain, (![U_53, V_54]: (c5_1(U_53) | c2_2(U_53, V_54) | c5_2(U_53, V_54) | ~ndr1_1(U_53) | ~c1_2(U_53, V_54)))). % 7.10/2.42 tff(c_607, plain, (c3_2(a750, a758))). % 7.10/2.42 tff(c_605, plain, (~c2_2(a750, a766))). % 7.10/2.42 tff(c_590, plain, (c1_2(a726, a727))). % 7.10/2.42 tff(c_591, plain, (![U_47, V_48]: (c5_1(U_47) | c3_2(U_47, V_48) | ~c1_2(U_47, a766) | ~ndr1_1(U_47) | ~c5_2(U_47, V_48)))). % 7.10/2.42 tff(c_589, plain, (c1_2(a732, a733))). % 7.10/2.42 tff(c_588, plain, (~c2_2(a726, a758))). % 7.10/2.42 tff(c_569, plain, (c5_2(a750, a758))). % 7.10/2.42 tff(c_550, plain, (~c2_2(a732, a758))). % 7.10/2.43 tff(c_551, plain, (![U_37, V_38]: (c1_1(U_37) | c5_2(U_37, a758) | c1_2(U_37, V_38) | ~ndr1_1(U_37) | ~c4_2(U_37, V_38)))). % 7.10/2.43 tff(c_549, plain, (~c2_2(a750, a758))). % 7.10/2.43 tff(c_528, plain, (![U_49, V_50]: (c1_1(U_49) | c1_2(U_49, V_50) | ~c2_2(U_49, a758) | ~ndr1_1(U_49) | ~c4_2(U_49, V_50)))). % 7.10/2.43 tff(c_520, plain, (![U_45, V_46]: (c5_1(U_45) | c3_2(U_45, V_46) | ~c2_2(U_45, a766) | ~ndr1_1(U_45) | ~c5_2(U_45, V_46)))). % 7.10/2.43 tff(c_512, plain, (![U_35, V_36]: (c5_1(U_35) | c3_2(U_35, a766) | c3_2(U_35, V_36) | ~ndr1_1(U_35) | ~c5_2(U_35, V_36)))). % 7.10/2.43 tff(c_511, plain, (~ndr1_1(a771))). % 7.10/2.43 tff(c_502, plain, (![U_41, V_42]: (~c1_2(U_41, V_42) | ~c5_2(U_41, V_42) | ~ndr1_1(U_41) | ~c2_2(U_41, V_42)))). % 7.10/2.43 tff(c_501, plain, (ssSkC2)). % 7.10/2.43 tff(c_496, plain, (~c5_2(a738, a740))). % 7.10/2.43 tff(c_494, plain, (~c5_2(a738, a739))). % 7.10/2.43 tff(c_492, plain, (~c1_2(a738, a739))). % 7.10/2.43 tff(c_490, plain, (c1_2(a738, a740))). % 7.10/2.43 tff(c_487, plain, (~c4_2(a738, a739))). % 7.10/2.43 tff(c_485, plain, (ndr1_1(a738))). % 7.10/2.43 tff(c_477, plain, (![U_21]: (~c1_2(a750, U_21) | ~c2_2(a750, U_21)))). % 7.10/2.43 tff(c_472, plain, (~c3_2(a732, a733))). % 7.10/2.43 tff(c_469, plain, (![U_15]: (c3_2(a726, U_15) | ~c5_2(a726, U_15)))). % 7.10/2.43 tff(c_466, plain, (c4_2(a732, a733))). % 7.10/2.43 tff(c_465, plain, (~c2_1(a732))). % 7.10/2.43 tff(c_464, plain, (~ssSkC1)). % 7.10/2.43 tff(c_463, plain, (ndr1_1(a732))). % 7.10/2.43 tff(c_108, plain, (![U_3]: (ssSkP0(U_3) | ~c4_2(U_3, a755)))). % 7.10/2.43 tff(c_58, plain, (![U_2]: (ssSkP0(U_2) | c3_2(U_2, a755)))). % 7.10/2.43 tff(c_447, plain, (~c1_2(a772, a773))). % 7.10/2.43 tff(c_446, plain, (~c1_2(a742, a743))). % 7.10/2.43 tff(c_445, plain, (~c4_2(a742, a743))). % 7.10/2.43 tff(c_444, plain, (c4_2(a726, a727))). % 7.10/2.43 tff(c_443, plain, (~c1_2(a750, a751))). % 7.10/2.43 tff(c_24, plain, (![U_1]: (ssSkP0(U_1) | ndr1_1(U_1)))). % 7.10/2.43 tff(c_438, plain, (c4_1(a771))). % 7.10/2.43 tff(c_437, plain, (c2_2(a726, a728))). % 7.10/2.43 tff(c_436, plain, (c2_2(a726, a727))). % 7.10/2.43 tff(c_435, plain, (~c5_2(a726, a727))). % 7.10/2.43 tff(c_434, plain, (~c4_2(a772, a773))). % 7.10/2.43 tff(c_433, plain, (c2_2(a750, a751))). % 7.10/2.43 tff(c_432, plain, (~ssSkC0)). % 7.10/2.43 tff(c_431, plain, (~ssSkC7)). % 7.10/2.43 tff(c_428, plain, (~c1_0)). % 7.10/2.43 tff(c_425, plain, (~c4_2(a744, a745))). % 7.10/2.43 tff(c_426, plain, (~ssSkC6)). % 7.10/2.43 tff(c_424, plain, (c4_2(a750, a751))). % 7.10/2.43 tff(c_423, plain, (c3_2(a744, a745))). % 7.10/2.43 tff(c_422, plain, (c2_2(a742, a743))). % 7.10/2.43 tff(c_421, plain, (~c4_2(a726, a728))). % 7.10/2.43 tff(c_420, plain, (c1_2(a744, a745))). % 7.10/2.43 tff(c_419, plain, (~c3_1(a769))). % 7.10/2.43 tff(c_418, plain, (c5_2(a772, a773))). % 7.10/2.43 tff(c_417, plain, (ndr1_1(a750))). % 7.10/2.43 tff(c_416, plain, (ndr1_1(a726))). % 7.10/2.43 tff(c_415, plain, (c5_1(a772))). % 7.10/2.43 tff(c_414, plain, (c2_1(a772))). % 7.10/2.43 tff(c_413, plain, (~c2_1(a750))). % 7.10/2.43 tff(c_412, plain, (c4_1(a734))). % 7.10/2.43 tff(c_411, plain, (ndr1_1(a772))). % 7.10/2.43 tff(c_410, plain, (ndr1_1(a744))). % 7.10/2.43 tff(c_409, plain, (c3_1(a742))). % 7.10/2.43 tff(c_408, plain, (ndr1_1(a742))). % 7.10/2.43 tff(c_407, plain, (~ssSkC5)). % 7.10/2.43 tff(c_406, plain, (~c5_1(a734))). % 7.10/2.43 tff(c_405, plain, (c3_1(a744))). % 7.10/2.43 tff(c_404, plain, (~c5_1(a744))). % 7.10/2.43 tff(c_4, plain, (c2_1(a731))). % 7.10/2.43 tff(c_403, plain, (~c2_0)). % 7.10/2.43 tff(c_6, plain, (c4_1(a731))). % 7.10/2.43 tff(c_402, plain, (~c4_0)). % 7.10/2.43 tff(c_401, plain, (~c5_0)). % 7.10/2.43 tff(c_2, plain, (ndr1_0)). % 7.10/2.43 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 7.10/2.43 %------------------------------------------------------------------------------