%------------------------------------------------------------------------------ % 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 : n019.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 : CounterSatisfiable 7.53s 2.57s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SYN541+1 : TPTP v9.0.0. Released v2.1.0. % 0.03/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 : n019.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.53/2.57 % 7.53/2.57 % SZS status CounterSatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 7.53/2.57 % 7.53/2.57 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 7.53/2.58 %$ 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 > 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 > a725 % 7.53/2.58 % 7.53/2.58 %Foreground sorts: % 7.53/2.58 % 7.53/2.58 % 7.53/2.58 %Background operators: % 7.53/2.58 % 7.53/2.58 % 7.53/2.58 %Foreground operators: % 7.53/2.58 tff(a750, type, a750: $i). % 7.53/2.58 tff(a760, type, a760: $i). % 7.53/2.58 tff(a749, type, a749: $i). % 7.53/2.58 tff(c4_0, type, c4_0: $o). % 7.53/2.58 tff(a748, type, a748: $i). % 7.53/2.58 tff(a768, type, a768: $i). % 7.53/2.58 tff(a739, type, a739: $i). % 7.53/2.58 tff(a733, type, a733: $i). % 7.53/2.58 tff(c3_0, type, c3_0: $o). % 7.53/2.58 tff(a725, type, a725: $i). % 7.53/2.58 tff(a734, type, a734: $i). % 7.53/2.58 tff(a751, type, a751: $i). % 7.53/2.58 tff(a767, type, a767: $i). % 7.53/2.58 tff(c1_2, type, c1_2: ($i * $i) > $o). % 7.53/2.58 tff(a727, type, a727: $i). % 7.53/2.58 tff(a764, type, a764: $i). % 7.53/2.58 tff(a758, type, a758: $i). % 7.53/2.58 tff(a731, type, a731: $i). % 7.53/2.58 tff(a753, type, a753: $i). % 7.53/2.58 tff(a736, type, a736: $i). % 7.53/2.58 tff(a769, type, a769: $i). % 7.53/2.58 tff(a771, type, a771: $i). % 7.53/2.58 tff(a759, type, a759: $i). % 7.53/2.58 tff(a741, type, a741: $i). % 7.53/2.58 tff(a770, type, a770: $i). % 7.53/2.58 tff(a746, type, a746: $i). % 7.53/2.58 tff(a766, type, a766: $i). % 7.53/2.58 tff(a747, type, a747: $i). % 7.53/2.58 tff(c5_0, type, c5_0: $o). % 7.53/2.58 tff(a730, type, a730: $i). % 7.53/2.58 tff(a774, type, a774: $i). % 7.53/2.58 tff(a745, type, a745: $i). % 7.53/2.58 tff(a737, type, a737: $i). % 7.53/2.58 tff(c1_0, type, c1_0: $o). % 7.53/2.58 tff(a754, type, a754: $i). % 7.53/2.58 tff(a765, type, a765: $i). % 7.53/2.58 tff(a755, type, a755: $i). % 7.53/2.58 tff(a772, type, a772: $i). % 7.53/2.58 tff(a740, type, a740: $i). % 7.53/2.58 tff(a743, type, a743: $i). % 7.53/2.58 tff(c2_1, type, c2_1: $i > $o). % 7.53/2.58 tff(ndr1_1, type, ndr1_1: $i > $o). % 7.53/2.58 tff(c2_0, type, c2_0: $o). % 7.53/2.58 tff(c4_1, type, c4_1: $i > $o). % 7.53/2.58 tff(a738, type, a738: $i). % 7.53/2.58 tff(a728, type, a728: $i). % 7.53/2.58 tff(a763, type, a763: $i). % 7.53/2.58 tff(ndr1_0, type, ndr1_0: $o). % 7.53/2.58 tff(a742, type, a742: $i). % 7.53/2.58 tff(a726, type, a726: $i). % 7.53/2.58 tff(a752, type, a752: $i). % 7.53/2.58 tff(a729, type, a729: $i). % 7.53/2.58 tff(a732, type, a732: $i). % 7.53/2.58 tff(c1_1, type, c1_1: $i > $o). % 7.53/2.58 tff(a762, type, a762: $i). % 7.53/2.58 tff(a756, type, a756: $i). % 7.53/2.58 tff(a761, type, a761: $i). % 7.53/2.58 tff(c5_2, type, c5_2: ($i * $i) > $o). % 7.53/2.58 tff(a744, type, a744: $i). % 7.53/2.58 tff(c4_2, type, c4_2: ($i * $i) > $o). % 7.53/2.58 tff(a757, type, a757: $i). % 7.53/2.58 tff(c5_1, type, c5_1: $i > $o). % 7.53/2.58 tff(c3_2, type, c3_2: ($i * $i) > $o). % 7.53/2.58 tff(a773, type, a773: $i). % 7.53/2.58 tff(c2_2, type, c2_2: ($i * $i) > $o). % 7.53/2.58 tff(a735, type, a735: $i). % 7.53/2.58 tff(c3_1, type, c3_1: $i > $o). % 7.53/2.58 % 7.53/2.58 %Saturated clause set: % 7.53/2.58 tff(c_1586, plain, (![X32_51, X21_100, X21_76]: (~c2_2(X32_51, X21_100) | ~c1_2(X32_51, X21_100) | ~c2_2(X32_51, X21_76) | c3_2(X32_51, X21_100) | ~c4_2(X32_51, X21_100) | c3_2(X32_51, X21_76) | ~c4_2(X32_51, X21_76) | c1_1(X32_51) | c5_1(X32_51) | c2_2(X32_51, a754) | ~c1_2(X32_51, a754) | ~ndr1_1(X32_51)))). % 7.53/2.58 tff(c_1595, plain, (![X11_21]: (~c1_2(a750, X11_21) | ~c2_2(a750, X11_21)))). % 7.53/2.58 tff(c_1419, plain, (![X32_87, X21_88, X_7]: (~c2_2(X32_87, X21_88) | ~c1_2(X32_87, X21_88) | ~c5_2(X32_87, X_7) | ~c2_2(X32_87, X_7) | c3_2(X32_87, X21_88) | ~c4_2(X32_87, X21_88) | c1_1(X32_87) | c5_1(X32_87) | c2_2(X32_87, a754) | ~c1_2(X32_87, a754) | ~ndr1_1(X32_87)))). % 7.53/2.58 tff(c_1568, plain, (~c2_2(a732, a733))). % 7.53/2.59 tff(c_1503, plain, (![X20_34, X21_94, X21_36]: (~c2_2(X20_34, X21_94) | ~c1_2(X20_34, X21_94) | ~c2_2(X20_34, X21_36) | c3_2(X20_34, X21_94) | ~c4_2(X20_34, X21_94) | c3_2(X20_34, a754) | c3_2(X20_34, X21_36) | ~c4_2(X20_34, X21_36) | ~ndr1_1(X20_34) | c1_1(X20_34)))). % 7.53/2.59 tff(c_1536, plain, (c2_2(a750, a751))). % 7.53/2.59 tff(c_1534, plain, (c1_1(a750))). % 7.53/2.59 tff(c_1533, plain, (~c2_2(a750, a758))). % 7.53/2.59 tff(c_1513, plain, (c4_2(a750, a751))). % 7.53/2.59 tff(c_1511, plain, (~c1_2(a750, a751))). % 7.53/2.59 tff(c_1506, plain, (~c2_1(a750))). % 7.53/2.59 tff(c_1326, plain, (![X20_34, X21_36, X_81]: (~c2_2(X20_34, X21_36) | ~c1_2(X20_34, X21_36) | ~c5_2(X20_34, X_81) | ~c2_2(X20_34, X_81) | c3_2(X20_34, a754) | c3_2(X20_34, X21_36) | ~c4_2(X20_34, X21_36) | ~ndr1_1(X20_34) | c1_1(X20_34)))). % 7.53/2.59 tff(c_1465, plain, (![X26_43, X27_45]: (~c2_2(X26_43, a758) | c1_1(X26_43) | ~c4_2(X26_43, X27_45) | c1_2(X26_43, X27_45) | ~ndr1_1(X26_43)))). % 7.53/2.59 tff(c_1467, plain, (c1_2(a732, a733))). % 7.53/2.59 tff(c_1469, plain, (ndr1_1(a750))). % 7.53/2.59 tff(c_1466, plain, (c1_2(a767, a768))). % 7.53/2.59 tff(c_1462, plain, (c1_1(a759))). % 7.53/2.59 tff(c_1444, plain, (![X26_43, X27_45]: (c5_2(X26_43, a758) | c1_1(X26_43) | ~c4_2(X26_43, X27_45) | c1_2(X26_43, X27_45) | ~ndr1_1(X26_43)))). % 7.53/2.59 tff(c_1283, plain, (![X32_51, X21_76]: (c5_2(X32_51, X21_76) | c3_2(X32_51, X21_76) | ~c4_2(X32_51, X21_76) | c1_1(X32_51) | c5_1(X32_51) | c2_2(X32_51, a754) | ~c1_2(X32_51, a754) | ~ndr1_1(X32_51)))). % 7.53/2.59 tff(c_1381, plain, (c3_2(a744, a745))). % 7.53/2.59 tff(c_1380, plain, (~c4_2(a744, a745))). % 7.53/2.59 tff(c_1379, plain, (c1_2(a744, a745))). % 7.53/2.59 tff(c_1373, plain, (~c5_1(a744))). % 7.53/2.59 tff(c_1372, plain, (c3_1(a744))). % 7.53/2.59 tff(c_1369, plain, (~c2_1(a767))). % 7.53/2.59 tff(c_1370, plain, (ndr1_1(a744))). % 7.53/2.59 tff(c_1368, plain, (~c2_1(a759))). % 7.53/2.59 tff(c_1350, plain, (![X23_38, X25_42, X24_41]: (c5_2(X23_38, X25_42) | c4_2(X23_38, X25_42) | ~c2_2(X23_38, X25_42) | ~c4_2(X23_38, X24_41) | c1_2(X23_38, X24_41) | ~ndr1_1(X23_38) | ~c2_1(X23_38)))). % 7.53/2.59 tff(c_1333, plain, (![X37_58, X38_60]: (~c2_1(X37_58) | c4_2(X37_58, X38_60) | ~c2_2(X37_58, X38_60) | ~c5_2(X37_58, X38_60) | ~ndr1_1(X37_58) | c3_1(X37_58)))). % 7.53/2.59 tff(c_1334, plain, (~c2_2(a763, a764))). % 7.53/2.59 tff(c_1315, plain, (![W_4, Y_8, X_7]: (~c2_2(W_4, Y_8) | ~c1_2(W_4, Y_8) | ~c5_2(W_4, Y_8) | ~c5_2(W_4, X_7) | ~c2_2(W_4, X_7) | ~ndr1_1(W_4)))). % 7.53/2.59 tff(c_1314, plain, (c1_2(a763, a764))). % 7.53/2.59 tff(c_1312, plain, (c5_2(a763, a764))). % 7.53/2.59 tff(c_1310, plain, (~c4_2(a738, a740))). % 7.53/2.59 tff(c_1286, plain, (![X20_34, X21_36]: (c3_2(X20_34, a754) | c5_2(X20_34, X21_36) | c3_2(X20_34, X21_36) | ~c4_2(X20_34, X21_36) | ~ndr1_1(X20_34) | c1_1(X20_34)))). % 7.53/2.59 tff(c_1285, plain, (~c2_1(a763))). % 7.53/2.59 tff(c_1278, plain, (![X20_34, X21_36]: (~c5_2(X20_34, a754) | c5_2(X20_34, X21_36) | c3_2(X20_34, X21_36) | ~c4_2(X20_34, X21_36) | ~ndr1_1(X20_34) | c1_1(X20_34)))). % 7.53/2.59 tff(c_1277, plain, (ndr1_1(a763))). % 7.53/2.59 tff(c_1272, plain, (c2_2(a738, a740))). % 7.53/2.59 tff(c_1250, plain, (![X32_51, X33_53]: (c5_1(X32_51) | c2_2(X32_51, X33_53) | c5_2(X32_51, X33_53) | ~c1_2(X32_51, X33_53) | ~ndr1_1(X32_51)))). % 7.88/2.59 tff(c_1243, plain, (c4_2(a767, a768))). % 7.88/2.59 tff(c_1241, plain, (~c5_2(a767, a768))). % 7.88/2.59 tff(c_1239, plain, (c3_2(a767, a768))). % 7.88/2.59 tff(c_1228, plain, (c5_1(a767))). % 7.88/2.59 tff(c_1226, plain, (~c1_2(a759, a760))). % 7.88/2.59 tff(c_1225, plain, (~c3_2(a759, a760))). % 7.88/2.59 tff(c_1222, plain, (ndr1_1(a767))). % 7.88/2.59 tff(c_1220, plain, (c4_2(a759, a760))). % 7.88/2.59 tff(c_1219, plain, (~c4_1(a767))). % 7.88/2.59 tff(c_1216, plain, (c3_1(a759))). % 7.88/2.59 tff(c_1213, plain, (ndr1_1(a759))). % 7.88/2.59 tff(c_1211, plain, (~ndr1_1(a771))). % 7.88/2.59 tff(c_1195, plain, (~c5_2(a738, a740))). % 7.88/2.59 tff(c_1193, plain, (~c5_2(a738, a739))). % 7.88/2.59 tff(c_1190, plain, (~c1_2(a738, a739))). % 7.88/2.59 tff(c_1188, plain, (~c4_2(a738, a739))). % 7.88/2.59 tff(c_1184, plain, (c1_2(a738, a740))). % 7.88/2.59 tff(c_1181, plain, (~ndr1_1(a774))). % 7.88/2.59 tff(c_1179, plain, (ndr1_1(a738))). % 7.88/2.59 tff(c_1175, plain, (~c3_2(a732, a733))). % 7.88/2.59 tff(c_1173, plain, (c4_1(a734))). % 7.88/2.59 tff(c_1171, plain, (~c5_1(a734))). % 7.88/2.59 tff(c_1170, plain, (c4_2(a732, a733))). % 7.88/2.59 tff(c_1168, plain, (ndr1_1(a732))). % 7.88/2.59 tff(c_1166, plain, (~c2_1(a732))). % 7.88/2.59 tff(c_1150, plain, (~c3_0)). % 7.88/2.59 tff(c_1149, plain, (c3_1(a774))). % 7.88/2.59 tff(c_1140, plain, (c4_1(a771))). % 7.88/2.59 tff(c_1136, plain, (~c1_0)). % 7.88/2.59 tff(c_1135, plain, (~c5_0)). % 7.88/2.59 tff(c_1134, plain, (~c2_0)). % 7.88/2.59 tff(c_1133, plain, (~c4_0)). % 7.88/2.59 tff(c_16, plain, (c4_1(a731))). % 7.88/2.59 tff(c_18, plain, (c2_1(a731))). % 7.88/2.59 tff(c_20, plain, (ndr1_0)). % 7.88/2.59 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 7.88/2.59 %------------------------------------------------------------------------------