%------------------------------------------------------------------------------ % 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 : n023.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 6.98s 2.53s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.12 % Problem : SYN540-1 : TPTP v9.0.0. Released v2.1.0. % 0.10/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.14/0.34 % Computer : n023.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 300 % 0.14/0.34 % DateTime : Wed Apr 9 07:58:09 EDT 2025 % 0.14/0.35 % CPUTime : % 6.98/2.53 % 6.98/2.53 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 6.98/2.54 % 6.98/2.54 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 6.98/2.54 %$ c5_2 > c4_2 > c3_2 > c2_2 > c1_2 > ssSkP0 > ndr1_1 > c5_1 > c4_1 > c3_1 > c2_1 > c1_1 > #nlpp > ssSkC6 > ssSkC5 > ssSkC4 > ssSkC3 > ssSkC2 > ssSkC1 > ssSkC0 > 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.98/2.54 % 6.98/2.54 %Foreground sorts: % 6.98/2.54 % 6.98/2.54 % 6.98/2.54 %Background operators: % 6.98/2.54 % 6.98/2.54 % 6.98/2.54 %Foreground operators: % 6.98/2.54 tff(a713, type, a713: $i). % 6.98/2.54 tff(a697, type, a697: $i). % 6.98/2.54 tff(a708, type, a708: $i). % 6.98/2.54 tff(c4_0, type, c4_0: $o). % 6.98/2.54 tff(a712, type, a712: $i). % 6.98/2.54 tff(a687, type, a687: $i). % 6.98/2.54 tff(a681, type, a681: $i). % 6.98/2.54 tff(ssSkP0, type, ssSkP0: $i > $o). % 6.98/2.54 tff(a692, type, a692: $i). % 6.98/2.54 tff(a717, type, a717: $i). % 6.98/2.54 tff(a706, type, a706: $i). % 6.98/2.54 tff(ssSkC6, type, ssSkC6: $o). % 6.98/2.54 tff(c3_0, type, c3_0: $o). % 6.98/2.54 tff(c1_2, type, c1_2: ($i * $i) > $o). % 6.98/2.54 tff(ssSkC3, type, ssSkC3: $o). % 6.98/2.54 tff(a693, type, a693: $i). % 6.98/2.54 tff(a704, type, a704: $i). % 6.98/2.54 tff(a691, type, a691: $i). % 6.98/2.54 tff(a721, type, a721: $i). % 6.98/2.54 tff(a698, type, a698: $i). % 6.98/2.54 tff(a724, type, a724: $i). % 6.98/2.54 tff(a703, type, a703: $i). % 6.98/2.54 tff(ssSkC4, type, ssSkC4: $o). % 6.98/2.54 tff(a709, type, a709: $i). % 6.98/2.54 tff(a695, type, a695: $i). % 6.98/2.54 tff(c5_0, type, c5_0: $o). % 6.98/2.54 tff(a714, type, a714: $i). % 6.98/2.54 tff(a696, type, a696: $i). % 6.98/2.54 tff(a685, type, a685: $i). % 6.98/2.54 tff(a711, type, a711: $i). % 6.98/2.54 tff(a722, type, a722: $i). % 6.98/2.54 tff(a719, type, a719: $i). % 6.98/2.54 tff(a690, type, a690: $i). % 6.98/2.54 tff(a707, type, a707: $i). % 6.98/2.54 tff(a686, type, a686: $i). % 6.98/2.54 tff(c1_0, type, c1_0: $o). % 6.98/2.54 tff(c2_1, type, c2_1: $i > $o). % 6.98/2.54 tff(ndr1_1, type, ndr1_1: $i > $o). % 6.98/2.54 tff(a699, type, a699: $i). % 6.98/2.54 tff(c2_0, type, c2_0: $o). % 6.98/2.54 tff(c4_1, type, c4_1: $i > $o). % 6.98/2.54 tff(a715, type, a715: $i). % 6.98/2.54 tff(a710, type, a710: $i). % 6.98/2.54 tff(a718, type, a718: $i). % 6.98/2.54 tff(a720, type, a720: $i). % 6.98/2.54 tff(a694, type, a694: $i). % 6.98/2.54 tff(a716, type, a716: $i). % 6.98/2.54 tff(a684, type, a684: $i). % 6.98/2.54 tff(ndr1_0, type, ndr1_0: $o). % 6.98/2.54 tff(a702, type, a702: $i). % 6.98/2.54 tff(a723, type, a723: $i). % 6.98/2.54 tff(c1_1, type, c1_1: $i > $o). % 6.98/2.54 tff(ssSkC2, type, ssSkC2: $o). % 6.98/2.54 tff(c5_2, type, c5_2: ($i * $i) > $o). % 6.98/2.54 tff(a705, type, a705: $i). % 6.98/2.54 tff(c4_2, type, c4_2: ($i * $i) > $o). % 6.98/2.54 tff(ssSkC1, type, ssSkC1: $o). % 6.98/2.54 tff(ssSkC0, type, ssSkC0: $o). % 6.98/2.54 tff(ssSkC5, type, ssSkC5: $o). % 6.98/2.54 tff(a701, type, a701: $i). % 6.98/2.54 tff(a700, type, a700: $i). % 6.98/2.54 tff(c5_1, type, c5_1: $i > $o). % 6.98/2.54 tff(c3_2, type, c3_2: ($i * $i) > $o). % 6.98/2.54 tff(a688, type, a688: $i). % 6.98/2.54 tff(a689, type, a689: $i). % 6.98/2.54 tff(c2_2, type, c2_2: ($i * $i) > $o). % 6.98/2.54 tff(a682, type, a682: $i). % 6.98/2.54 tff(a683, type, a683: $i). % 6.98/2.54 tff(c3_1, type, c3_1: $i > $o). % 6.98/2.54 % 6.98/2.54 %Saturated clause set: % 6.98/2.55 tff(c_1381, plain, (~c4_1(a689))). % 6.98/2.55 tff(c_1377, plain, (c1_1(a717))). % 6.98/2.55 tff(c_1373, plain, (c2_1(a717))). % 6.98/2.55 tff(c_1367, plain, (![U_197]: (c1_1(U_197) | c2_1(U_197) | ~c4_1(U_197)))). % 6.98/2.55 tff(c_1362, plain, (![U_96]: (c5_1(U_96) | ~c4_1(U_96)))). % 6.98/2.55 tff(c_1336, plain, (![U_84, V_85, W_86]: (c3_2(U_84, a695) | c3_2(U_84, V_85) | ~c2_2(U_84, W_86) | ~c1_2(U_84, W_86) | ~c4_2(U_84, V_85) | ~c2_2(U_84, V_85)))). % 6.98/2.55 tff(c_1311, plain, (![U_87, V_88, W_89]: (c2_2(U_87, a695) | c3_2(U_87, V_88) | ~c2_2(U_87, W_89) | ~c1_2(U_87, W_89) | ~c4_2(U_87, V_88) | ~c2_2(U_87, V_88)))). % 6.98/2.55 tff(c_1019, plain, (![U_41, V_42]: (c2_1(U_41) | c5_2(U_41, a681) | c1_2(U_41, a711) | c2_2(U_41, a711) | c1_2(U_41, V_42) | c2_2(U_41, V_42) | ~c4_1(U_41)))). % 6.98/2.55 tff(c_1263, plain, (![U_186, V_46]: (c1_2(U_186, V_46) | c2_2(U_186, V_46) | c2_1(U_186) | ~c1_2(U_186, a681) | c1_2(U_186, a711) | ~c4_1(U_186)))). % 6.98/2.55 tff(c_1240, plain, (![U_41]: (c2_1(U_41) | ~c1_2(U_41, a681) | c1_2(U_41, a711) | ~c4_1(U_41) | c2_2(U_41, a711)))). % 6.98/2.55 tff(c_1126, plain, (![U_41, V_42]: (c2_1(U_41) | c4_2(U_41, a681) | c1_2(U_41, a711) | c2_2(U_41, a711) | c1_2(U_41, V_42) | c2_2(U_41, V_42) | ~c4_1(U_41)))). % 6.98/2.55 tff(c_1148, plain, (c4_2(a692, a681))). % 6.98/2.55 tff(c_1132, plain, (c4_2(a694, a681))). % 6.98/2.55 tff(c_1109, plain, (![U_59, V_60]: (c2_1(U_59) | c4_2(U_59, a681) | c1_2(U_59, V_60) | c2_2(U_59, V_60) | ~c4_2(U_59, V_60)))). % 6.98/2.55 tff(c_1088, plain, (~c1_2(a692, a681))). % 6.98/2.55 tff(c_1085, plain, (~c1_2(a694, a681))). % 6.98/2.55 tff(c_1055, plain, (![U_61, V_62]: (c2_1(U_61) | c1_2(U_61, V_62) | c2_2(U_61, V_62) | ~c1_2(U_61, a681) | ~c4_2(U_61, V_62)))). % 6.98/2.55 tff(c_1052, plain, (~c4_1(a702))). % 6.98/2.55 tff(c_1026, plain, (c5_2(a692, a681))). % 6.98/2.55 tff(c_1025, plain, (c5_2(a694, a681))). % 6.98/2.55 tff(c_1002, plain, (![U_57, V_58]: (c2_1(U_57) | c5_2(U_57, a681) | c1_2(U_57, V_58) | c2_2(U_57, V_58) | ~c4_2(U_57, V_58)))). % 6.98/2.55 tff(c_982, plain, (![U_161, V_162]: (c1_1(U_161) | c4_2(U_161, a711) | c1_2(U_161, V_162) | ~c4_1(U_161)))). % 6.98/2.55 tff(c_985, plain, (![U_45, V_46]: (c1_2(U_45, V_46) | c2_2(U_45, V_46) | ~c4_1(U_45) | ~c2_2(U_45, a711)))). % 6.98/2.55 tff(c_975, plain, (![U_41, V_42]: (c4_2(U_41, a711) | c1_2(U_41, V_42) | c2_2(U_41, V_42) | ~c4_1(U_41)))). % 6.98/2.55 tff(c_951, plain, (![U_33]: (c3_2(a689, U_33) | ~c4_2(a689, U_33) | ~c5_2(a689, U_33)))). % 6.98/2.55 tff(c_944, plain, (![U_158]: (c1_1(U_158) | ~c2_1(U_158)))). % 6.98/2.55 tff(c_939, plain, (c1_1(a689))). % 6.98/2.55 tff(c_925, plain, (ssSkC3)). % 6.98/2.55 tff(c_928, plain, (![U_26, V_27]: (c1_1(U_26) | c1_2(U_26, V_27) | ~c2_2(U_26, V_27)))). % 6.98/2.55 tff(c_921, plain, (![U_38]: (~c4_2(a722, U_38) | ~c5_2(a722, U_38) | ~c1_2(a722, U_38)))). % 6.98/2.55 tff(c_918, plain, (ssSkC4)). % 6.98/2.55 tff(c_914, plain, (![U_29]: (c2_2(a692, U_29) | c4_2(a692, U_29) | ~c3_2(a692, U_29)))). % 6.98/2.55 tff(c_910, plain, (![U_24]: (c4_2(a698, U_24) | c1_2(a698, U_24) | c5_2(a698, U_24)))). % 6.98/2.55 tff(c_904, plain, (![U_30]: (c1_2(a722, U_30) | ~c3_2(a722, U_30) | ~c2_2(a722, U_30)))). % 6.98/2.55 tff(c_900, plain, (![U_25]: (c3_2(a694, U_25) | c4_2(a694, U_25) | c2_2(a694, U_25)))). % 6.98/2.55 tff(c_884, plain, (![U_16]: (c4_2(a702, U_16) | ~c1_2(a702, U_16)))). % 6.98/2.55 tff(c_880, plain, (![U_12]: (c1_1(U_12) | c2_1(U_12) | ~c5_1(U_12)))). % 6.98/2.55 tff(c_876, plain, (![U_17]: (c1_2(a702, U_17) | ~c5_2(a702, U_17)))). % 6.98/2.55 tff(c_870, plain, (![U_13]: (~c2_1(U_13) | ~c1_2(U_13, a709)))). % 6.98/2.56 tff(c_858, plain, (![U_10]: (c2_2(U_10, a709) | ~c2_1(U_10)))). % 6.98/2.56 tff(c_854, plain, (![U_11]: (c4_2(U_11, a709) | ~c2_1(U_11)))). % 6.98/2.56 tff(c_844, plain, (![U_9]: (~c2_2(U_9, a684) | ~ssSkP0(U_9)))). % 6.98/2.56 tff(c_826, plain, (![U_1]: (ndr1_1(U_1)))). % 6.98/2.56 tff(c_829, plain, (![U_5]: (c1_2(U_5, a684) | ~ssSkP0(U_5)))). % 6.98/2.56 tff(c_84, plain, (![U_2]: (ssSkP0(U_2) | c4_2(U_2, a683)))). % 6.98/2.56 tff(c_86, plain, (![U_3]: (ssSkP0(U_3) | c1_2(U_3, a683)))). % 6.98/2.56 tff(c_812, plain, (c3_2(a689, a690))). % 6.98/2.56 tff(c_808, plain, (c5_2(a689, a691))). % 6.98/2.56 tff(c_802, plain, (~c1_2(a689, a690))). % 6.98/2.56 tff(c_798, plain, (c1_2(a689, a691))). % 6.98/2.56 tff(c_794, plain, (c2_2(a689, a690))). % 6.98/2.56 tff(c_790, plain, (~c4_2(a689, a691))). % 6.98/2.56 tff(c_784, plain, (c5_2(a717, a718))). % 6.98/2.56 tff(c_782, plain, (~c4_2(a698, a699))). % 6.98/2.56 tff(c_779, plain, (~c1_2(a698, a699))). % 6.98/2.56 tff(c_778, plain, (c1_2(a717, a718))). % 6.98/2.56 tff(c_775, plain, (~c5_2(a706, a707))). % 6.98/2.56 tff(c_774, plain, (~ssSkC0)). % 6.98/2.56 tff(c_772, plain, (~c1_2(a706, a707))). % 6.98/2.56 tff(c_769, plain, (~ssSkC2)). % 6.98/2.56 tff(c_767, plain, (~c3_0)). % 6.98/2.56 tff(c_764, plain, (~ssSkC6)). % 6.98/2.56 tff(c_762, plain, (ssSkC1)). % 6.98/2.56 tff(c_319, plain, (~c1_1(a687))). % 6.98/2.56 tff(c_318, plain, (~c5_0)). % 6.98/2.56 tff(c_316, plain, (~c3_1(a694))). % 6.98/2.56 tff(c_315, plain, (~c4_1(a706))). % 6.98/2.56 tff(c_314, plain, (c1_1(a710))). % 6.98/2.56 tff(c_313, plain, (~c1_1(a694))). % 6.98/2.56 tff(c_311, plain, (~c1_1(a692))). % 6.98/2.56 tff(c_308, plain, (~c4_1(a692))). % 6.98/2.56 tff(c_304, plain, (c3_1(a722))). % 6.98/2.56 tff(c_303, plain, (c3_1(a698))). % 6.98/2.56 tff(c_302, plain, (c4_1(a717))). % 6.98/2.56 tff(c_289, plain, (~c4_0)). % 6.98/2.56 tff(c_288, plain, (~c1_0)). % 6.98/2.56 tff(c_286, plain, (ndr1_0)). % 6.98/2.56 tff(c_285, plain, (~c2_0)). % 6.98/2.56 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 6.98/2.56 %------------------------------------------------------------------------------