%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SYN540+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:51 PM UTC 2025 % Result : CounterSatisfiable 6.59s 2.35s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SYN540+1 : TPTP v9.0.0. Released v2.1.0. % 0.11/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.12/0.33 % Computer : n019.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % 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:58:17 EDT 2025 % 0.12/0.34 % CPUTime : % 6.59/2.35 % 6.59/2.35 % SZS status CounterSatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 6.59/2.35 % 6.59/2.35 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 6.59/2.36 %$ 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 > a724 > a723 > a722 > a721 > a720 > a719 > a718 > a717 > a716 > a715 > a714 > a713 > a712 > a711 > a710 > a709 > a708 > a707 > a706 > a705 > a704 > a703 > a702 > a701 > a700 > a699 > a698 > a697 > a696 > a695 > a694 > a693 > a692 > a691 > a690 > a689 > a688 > a687 > a686 > a685 > a684 > a683 > a682 > a681 % 6.59/2.36 % 6.59/2.36 %Foreground sorts: % 6.59/2.36 % 6.59/2.36 % 6.59/2.36 %Background operators: % 6.59/2.36 % 6.59/2.36 % 6.59/2.36 %Foreground operators: % 6.59/2.36 tff(a713, type, a713: $i). % 6.59/2.36 tff(a697, type, a697: $i). % 6.59/2.36 tff(a708, type, a708: $i). % 6.59/2.36 tff(c4_0, type, c4_0: $o). % 6.59/2.36 tff(a712, type, a712: $i). % 6.59/2.36 tff(a687, type, a687: $i). % 6.59/2.36 tff(a681, type, a681: $i). % 6.59/2.36 tff(a692, type, a692: $i). % 6.59/2.36 tff(a717, type, a717: $i). % 6.59/2.36 tff(a706, type, a706: $i). % 6.59/2.36 tff(c3_0, type, c3_0: $o). % 6.59/2.36 tff(c1_2, type, c1_2: ($i * $i) > $o). % 6.59/2.36 tff(a693, type, a693: $i). % 6.59/2.36 tff(a704, type, a704: $i). % 6.59/2.36 tff(a691, type, a691: $i). % 6.59/2.36 tff(a721, type, a721: $i). % 6.59/2.36 tff(a698, type, a698: $i). % 6.59/2.36 tff(a724, type, a724: $i). % 6.59/2.36 tff(a703, type, a703: $i). % 6.59/2.36 tff(a709, type, a709: $i). % 6.59/2.36 tff(a695, type, a695: $i). % 6.59/2.36 tff(c5_0, type, c5_0: $o). % 6.59/2.36 tff(a714, type, a714: $i). % 6.59/2.36 tff(a696, type, a696: $i). % 6.59/2.36 tff(a685, type, a685: $i). % 6.59/2.36 tff(a711, type, a711: $i). % 6.59/2.36 tff(a722, type, a722: $i). % 6.59/2.36 tff(a719, type, a719: $i). % 6.59/2.36 tff(a690, type, a690: $i). % 6.59/2.36 tff(a707, type, a707: $i). % 6.59/2.36 tff(a686, type, a686: $i). % 6.59/2.36 tff(c1_0, type, c1_0: $o). % 6.59/2.36 tff(c2_1, type, c2_1: $i > $o). % 6.59/2.36 tff(ndr1_1, type, ndr1_1: $i > $o). % 6.59/2.36 tff(a699, type, a699: $i). % 6.59/2.36 tff(c2_0, type, c2_0: $o). % 6.59/2.36 tff(c4_1, type, c4_1: $i > $o). % 6.59/2.36 tff(a715, type, a715: $i). % 6.59/2.36 tff(a710, type, a710: $i). % 6.59/2.36 tff(a718, type, a718: $i). % 6.59/2.36 tff(a720, type, a720: $i). % 6.59/2.36 tff(a694, type, a694: $i). % 6.59/2.36 tff(a716, type, a716: $i). % 6.59/2.36 tff(a684, type, a684: $i). % 6.59/2.36 tff(ndr1_0, type, ndr1_0: $o). % 6.59/2.36 tff(a702, type, a702: $i). % 6.59/2.36 tff(a723, type, a723: $i). % 6.59/2.36 tff(c1_1, type, c1_1: $i > $o). % 6.59/2.36 tff(c5_2, type, c5_2: ($i * $i) > $o). % 6.59/2.36 tff(a705, type, a705: $i). % 6.59/2.36 tff(c4_2, type, c4_2: ($i * $i) > $o). % 6.59/2.36 tff(a701, type, a701: $i). % 6.59/2.36 tff(a700, type, a700: $i). % 6.59/2.36 tff(c5_1, type, c5_1: $i > $o). % 6.59/2.36 tff(c3_2, type, c3_2: ($i * $i) > $o). % 6.59/2.36 tff(a688, type, a688: $i). % 6.59/2.36 tff(a689, type, a689: $i). % 6.59/2.36 tff(c2_2, type, c2_2: ($i * $i) > $o). % 6.59/2.36 tff(a682, type, a682: $i). % 6.59/2.36 tff(a683, type, a683: $i). % 6.59/2.36 tff(c3_1, type, c3_1: $i > $o). % 6.59/2.36 % 6.59/2.36 %Saturated clause set: % 6.59/2.36 tff(c_1536, plain, (~c2_1(a689))). % 6.59/2.36 tff(c_1535, plain, (~c2_1(a723))). % 6.59/2.36 tff(c_1534, plain, (~c2_1(a687))). % 6.59/2.36 tff(c_1492, plain, (![X26_40, X_102]: (c1_2(X26_40, a682) | c3_2(X26_40, a709) | ~c2_2(X26_40, a709) | c5_2(X26_40, X_102) | ~c2_2(X26_40, X_102) | ~ndr1_1(X26_40) | ~c2_1(X26_40)))). % 6.59/2.36 tff(c_1497, plain, (c3_2(a723, a724))). % 6.59/2.36 tff(c_1496, plain, (c3_2(a687, a688))). % 6.59/2.36 tff(c_1448, plain, (![W_4, Y_8, X_7]: (c1_2(W_4, a682) | c3_2(W_4, Y_8) | ~c2_2(W_4, Y_8) | ~c4_2(W_4, Y_8) | c5_2(W_4, X_7) | ~c2_2(W_4, X_7) | ~ndr1_1(W_4)))). % 6.59/2.36 tff(c_1431, plain, (![X26_40, X_97]: (~c4_2(X26_40, a682) | c3_2(X26_40, a709) | ~c2_2(X26_40, a709) | c5_2(X26_40, X_97) | ~c2_2(X26_40, X_97) | ~ndr1_1(X26_40) | ~c2_1(X26_40)))). % 6.59/2.36 tff(c_1436, plain, (~c4_2(a723, a682))). % 6.59/2.36 tff(c_1444, plain, (~c2_1(a710))). % 6.59/2.36 tff(c_1440, plain, (~ndr1_1(a710))). % 6.59/2.36 tff(c_1435, plain, (~c4_2(a687, a682))). % 6.59/2.36 tff(c_1391, plain, (![W_4, Y_8, X_7]: (~c4_2(W_4, a682) | c3_2(W_4, Y_8) | ~c2_2(W_4, Y_8) | ~c4_2(W_4, Y_8) | c5_2(W_4, X_7) | ~c2_2(W_4, X_7) | ~ndr1_1(W_4)))). % 6.59/2.36 tff(c_1262, plain, (![X26_40, X11_85]: (c2_2(X26_40, a695) | c3_2(X26_40, a709) | ~c2_2(X26_40, a709) | ~c2_2(X26_40, X11_85) | ~c1_2(X26_40, X11_85) | ~ndr1_1(X26_40) | ~c2_1(X26_40)))). % 6.59/2.36 tff(c_1230, plain, (![X26_40, X11_81]: (c3_2(X26_40, a695) | c3_2(X26_40, a709) | ~c2_2(X26_40, a709) | ~c2_2(X26_40, X11_81) | ~c1_2(X26_40, X11_81) | ~ndr1_1(X26_40) | ~c2_1(X26_40)))). % 6.59/2.36 tff(c_1353, plain, (![X4_13]: (~c4_2(a689, X4_13) | ~c5_2(a689, X4_13) | c3_2(a689, X4_13)))). % 6.59/2.36 tff(c_1336, plain, (c1_2(a723, a695))). % 6.59/2.36 tff(c_1329, plain, (c2_2(a723, a695))). % 6.59/2.36 tff(c_1309, plain, (c1_2(a687, a695))). % 6.59/2.36 tff(c_1299, plain, (c2_2(a687, a695))). % 6.59/2.36 tff(c_1284, plain, (c3_2(a723, a695))). % 6.59/2.36 tff(c_1248, plain, (c3_2(a687, a695))). % 6.59/2.36 tff(c_1251, plain, (![X10_19, X12_23, X11_22]: (c2_2(X10_19, a695) | ~c4_2(X10_19, X12_23) | c3_2(X10_19, X12_23) | ~c2_2(X10_19, X12_23) | ~c2_2(X10_19, X11_22) | ~c1_2(X10_19, X11_22) | ~ndr1_1(X10_19)))). % 6.59/2.36 tff(c_1219, plain, (![X10_19, X12_23, X11_22]: (c3_2(X10_19, a695) | ~c4_2(X10_19, X12_23) | c3_2(X10_19, X12_23) | ~c2_2(X10_19, X12_23) | ~c2_2(X10_19, X11_22) | ~c1_2(X10_19, X11_22) | ~ndr1_1(X10_19)))). % 6.59/2.36 tff(c_1185, plain, (![U_1, V_3]: (c4_2(U_1, a681) | c1_2(U_1, V_3) | ~c4_2(U_1, V_3) | c2_2(U_1, V_3) | ~ndr1_1(U_1) | c2_1(U_1)))). % 6.59/2.37 tff(c_1162, plain, (![U_1, V_3]: (c5_2(U_1, a681) | c1_2(U_1, V_3) | ~c4_2(U_1, V_3) | c2_2(U_1, V_3) | ~ndr1_1(U_1) | c2_1(U_1)))). % 6.59/2.37 tff(c_1142, plain, (![U_1, V_3]: (~c1_2(U_1, a681) | c1_2(U_1, V_3) | ~c4_2(U_1, V_3) | c2_2(U_1, V_3) | ~ndr1_1(U_1) | c2_1(U_1)))). % 6.59/2.37 tff(c_1132, plain, (c1_1(a710))). % 6.59/2.37 tff(c_1101, plain, (~c5_2(a687, a688))). % 6.59/2.37 tff(c_1078, plain, (c1_2(a687, a688))). % 6.59/2.37 tff(c_1082, plain, (c4_2(a687, a688))). % 6.59/2.37 tff(c_1071, plain, (c2_2(a687, a688))). % 6.59/2.37 tff(c_1054, plain, (![X38_56]: (~c2_2(a723, X38_56) | ~c5_2(a723, X38_56) | ~c4_2(a723, X38_56)))). % 6.59/2.37 tff(c_1050, plain, (~c2_1(a692))). % 6.59/2.37 tff(c_1046, plain, (~ndr1_1(a692))). % 6.59/2.37 tff(c_1031, plain, (ndr1_1(a687))). % 6.59/2.37 tff(c_1021, plain, (![X2_11]: (~c2_2(a685, X2_11) | c1_2(a685, X2_11)))). % 6.59/2.37 tff(c_1014, plain, (![X15_27]: (c4_2(a698, X15_27) | c1_2(a698, X15_27) | c5_2(a698, X15_27)))). % 6.59/2.37 tff(c_994, plain, (![X26_40]: (c1_1(X26_40) | ~c2_1(X26_40)))). % 6.59/2.37 tff(c_1004, plain, (~c2_1(a698))). % 6.59/2.37 tff(c_997, plain, (~c2_1(a685))). % 6.59/2.37 tff(c_972, plain, (c1_2(a723, a724))). % 6.59/2.37 tff(c_966, plain, (c1_1(a689))). % 6.59/2.37 tff(c_951, plain, (![X20_32, X21_34]: (c1_1(X20_32) | ~c2_2(X20_32, X21_34) | c1_2(X20_32, X21_34) | ~ndr1_1(X20_32)))). % 6.59/2.37 tff(c_948, plain, (~c2_1(a694))). % 6.59/2.37 tff(c_944, plain, (~ndr1_1(a694))). % 6.59/2.37 tff(c_859, plain, (~c2_1(a702))). % 6.59/2.37 tff(c_855, plain, (~ndr1_1(a702))). % 6.59/2.37 tff(c_852, plain, (![X7_16]: (c1_1(X7_16) | c2_1(X7_16) | ~c5_1(X7_16)))). % 6.59/2.37 tff(c_848, plain, (![X26_40]: (c2_2(X26_40, a709) | ~c2_1(X26_40)))). % 6.59/2.37 tff(c_844, plain, (![X26_40]: (~c1_2(X26_40, a709) | ~c2_1(X26_40)))). % 6.59/2.37 tff(c_835, plain, (![X26_40]: (c4_2(X26_40, a709) | ~c2_1(X26_40)))). % 6.59/2.37 tff(c_825, plain, (~c4_2(a685, a686))). % 6.59/2.37 tff(c_810, plain, (~c3_2(a685, a686))). % 6.59/2.37 tff(c_799, plain, (![X26_40]: (ndr1_1(X26_40) | ~c2_1(X26_40)))). % 6.59/2.37 tff(c_794, plain, (~c5_2(a685, a686))). % 6.59/2.37 tff(c_777, plain, (~c1_2(a689, a690))). % 6.59/2.37 tff(c_770, plain, (c1_2(a689, a691))). % 6.59/2.37 tff(c_765, plain, (c3_2(a689, a690))). % 6.59/2.37 tff(c_763, plain, (c2_2(a689, a690))). % 6.59/2.37 tff(c_761, plain, (~c5_2(a723, a724))). % 6.59/2.37 tff(c_757, plain, (c4_2(a723, a724))). % 6.59/2.37 tff(c_755, plain, (~c4_2(a689, a691))). % 6.59/2.37 tff(c_753, plain, (ndr1_1(a685))). % 6.59/2.37 tff(c_749, plain, (~c1_1(a685))). % 6.59/2.37 tff(c_745, plain, (c5_2(a689, a691))). % 6.59/2.37 tff(c_743, plain, (c2_2(a723, a724))). % 6.59/2.37 tff(c_740, plain, (~c1_1(a687))). % 6.59/2.37 tff(c_734, plain, (~c1_1(a692))). % 6.59/2.37 tff(c_732, plain, (~c4_1(a692))). % 6.59/2.37 tff(c_728, plain, (~c5_1(a693))). % 6.59/2.37 tff(c_726, plain, (ndr1_1(a723))). % 6.59/2.37 tff(c_721, plain, (ndr1_1(a689))). % 6.59/2.37 tff(c_719, plain, (~c1_2(a698, a699))). % 6.59/2.37 tff(c_718, plain, (~c4_2(a698, a699))). % 6.59/2.37 tff(c_712, plain, (~c3_0)). % 6.59/2.37 tff(c_710, plain, (c3_1(a698))). % 6.59/2.37 tff(c_709, plain, (ndr1_1(a698))). % 6.59/2.37 tff(c_708, plain, (~c5_0)). % 6.59/2.37 tff(c_704, plain, (~c1_1(a694))). % 6.59/2.37 tff(c_703, plain, (~c3_1(a694))). % 6.59/2.37 tff(c_702, plain, (~c1_0)). % 6.59/2.37 tff(c_697, plain, (~c2_0)). % 6.59/2.37 tff(c_694, plain, (~c4_0)). % 6.59/2.37 tff(c_693, plain, (ndr1_0)). % 6.59/2.37 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 6.59/2.37 %------------------------------------------------------------------------------