%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SYN524+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 : n020.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:48 PM UTC 2025 % Result : CounterSatisfiable 5.35s 2.15s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SYN524+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 : n020.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:55:04 EDT 2025 % 0.13/0.34 % CPUTime : % 5.35/2.14 % 5.35/2.15 % SZS status CounterSatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 5.35/2.15 % 5.35/2.15 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 5.35/2.16 %$ 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 > a187 > a186 > a185 > a184 > a183 > a182 > a181 > a180 > a179 > a178 > a177 > a176 > a175 > a174 > a173 > a172 > a171 > a170 > a169 > a168 > a167 > a166 > a165 > a164 > a163 > a162 > a161 > a160 > a159 > a158 > a157 % 5.35/2.16 % 5.35/2.16 %Foreground sorts: % 5.35/2.16 % 5.35/2.16 % 5.35/2.16 %Background operators: % 5.35/2.16 % 5.35/2.16 % 5.35/2.16 %Foreground operators: % 5.35/2.16 tff(a178, type, a178: $i). % 5.35/2.16 tff(a169, type, a169: $i). % 5.35/2.16 tff(c4_0, type, c4_0: $o). % 5.35/2.16 tff(a167, type, a167: $i). % 5.35/2.16 tff(c3_0, type, c3_0: $o). % 5.35/2.16 tff(c1_2, type, c1_2: ($i * $i) > $o). % 5.35/2.16 tff(a157, type, a157: $i). % 5.35/2.16 tff(a185, type, a185: $i). % 5.35/2.16 tff(a171, type, a171: $i). % 5.35/2.16 tff(a161, type, a161: $i). % 5.35/2.16 tff(a184, type, a184: $i). % 5.35/2.16 tff(a174, type, a174: $i). % 5.35/2.16 tff(a166, type, a166: $i). % 5.35/2.16 tff(a176, type, a176: $i). % 5.35/2.16 tff(a183, type, a183: $i). % 5.35/2.16 tff(a165, type, a165: $i). % 5.35/2.16 tff(a179, type, a179: $i). % 5.35/2.16 tff(c5_0, type, c5_0: $o). % 5.35/2.16 tff(a180, type, a180: $i). % 5.35/2.16 tff(a173, type, a173: $i). % 5.35/2.16 tff(a163, type, a163: $i). % 5.35/2.16 tff(a187, type, a187: $i). % 5.35/2.16 tff(a160, type, a160: $i). % 5.35/2.16 tff(c1_0, type, c1_0: $o). % 5.35/2.16 tff(a172, type, a172: $i). % 5.35/2.16 tff(c2_1, type, c2_1: $i > $o). % 5.35/2.16 tff(ndr1_1, type, ndr1_1: $i > $o). % 5.35/2.16 tff(c2_0, type, c2_0: $o). % 5.35/2.16 tff(c4_1, type, c4_1: $i > $o). % 5.35/2.16 tff(a159, type, a159: $i). % 5.35/2.16 tff(a186, type, a186: $i). % 5.35/2.16 tff(a158, type, a158: $i). % 5.35/2.16 tff(a175, type, a175: $i). % 5.35/2.16 tff(ndr1_0, type, ndr1_0: $o). % 5.35/2.16 tff(a177, type, a177: $i). % 5.35/2.16 tff(a182, type, a182: $i). % 5.35/2.16 tff(c1_1, type, c1_1: $i > $o). % 5.35/2.16 tff(a170, type, a170: $i). % 5.35/2.16 tff(c5_2, type, c5_2: ($i * $i) > $o). % 5.35/2.16 tff(c4_2, type, c4_2: ($i * $i) > $o). % 5.35/2.16 tff(a164, type, a164: $i). % 5.35/2.16 tff(c5_1, type, c5_1: $i > $o). % 5.35/2.16 tff(c3_2, type, c3_2: ($i * $i) > $o). % 5.35/2.16 tff(c2_2, type, c2_2: ($i * $i) > $o). % 5.35/2.16 tff(a181, type, a181: $i). % 5.35/2.16 tff(a162, type, a162: $i). % 5.35/2.16 tff(a168, type, a168: $i). % 5.35/2.16 tff(c3_1, type, c3_1: $i > $o). % 5.35/2.16 % 5.35/2.16 %Saturated clause set: % 5.53/2.16 tff(c_777, plain, (![X19_29, X20_31]: (~c1_2(X19_29, X20_31) | ~c3_2(X19_29, X20_31) | ~c4_2(X19_29, X20_31) | ~ndr1_1(X19_29) | ~c4_1(X19_29) | ~c1_1(X19_29)))). % 5.53/2.16 tff(c_772, plain, (![X3_12]: (c1_1(X3_12) | ~c2_1(X3_12) | ~c5_1(X3_12)))). % 5.53/2.16 tff(c_762, plain, (~c1_2(a163, a164))). % 5.53/2.16 tff(c_761, plain, (~c3_2(a163, a164))). % 5.53/2.16 tff(c_757, plain, (c5_2(a163, a164))). % 5.53/2.16 tff(c_754, plain, (~c5_2(a159, a160))). % 5.53/2.16 tff(c_751, plain, (ndr1_1(a163))). % 5.53/2.16 tff(c_749, plain, (~c2_1(a163))). % 5.53/2.16 tff(c_748, plain, (~c3_2(a159, a160))). % 5.53/2.16 tff(c_740, plain, (~c3_1(a161))). % 5.53/2.16 tff(c_739, plain, (c3_1(a163))). % 5.53/2.16 tff(c_738, plain, (~c1_2(a167, a168))). % 5.53/2.16 tff(c_733, plain, (![X5_14]: (~c1_2(a167, X5_14) | ~c3_2(a167, X5_14)))). % 5.53/2.16 tff(c_730, plain, (ndr1_1(a159))). % 5.53/2.16 tff(c_722, plain, (~c2_1(a159))). % 5.53/2.16 tff(c_718, plain, (~c3_1(a159))). % 5.53/2.16 tff(c_712, plain, (![X13_23]: (~c2_1(X13_23) | ~c5_1(X13_23) | c4_1(X13_23)))). % 5.53/2.16 tff(c_710, plain, (c3_2(a167, a168))). % 5.53/2.16 tff(c_705, plain, (c4_2(a167, a168))). % 5.53/2.16 tff(c_702, plain, (c2_2(a167, a168))). % 5.53/2.16 tff(c_696, plain, (![X24_36]: (~c2_2(X24_36, a185) | c4_2(X24_36, a186) | ~c3_1(X24_36)))). % 5.53/2.16 tff(c_694, plain, (![X24_36]: (~c2_2(X24_36, a185) | ~c1_2(X24_36, a186) | ~c3_1(X24_36)))). % 5.53/2.16 tff(c_692, plain, (![X24_36]: (~c3_2(X24_36, a185) | ~c1_2(X24_36, a186) | ~c3_1(X24_36)))). % 5.53/2.16 tff(c_691, plain, (ndr1_1(a167))). % 5.53/2.16 tff(c_687, plain, (![X24_36]: (~c3_2(X24_36, a185) | c4_2(X24_36, a186) | ~c3_1(X24_36)))). % 5.53/2.16 tff(c_683, plain, (![X25_37]: (c1_2(X25_37, a187) | ~c2_1(X25_37)))). % 5.53/2.16 tff(c_679, plain, (![X25_37]: (c2_2(X25_37, a187) | ~c2_1(X25_37)))). % 5.53/2.16 tff(c_675, plain, (![X25_37]: (~c5_2(X25_37, a187) | ~c2_1(X25_37)))). % 5.53/2.16 tff(c_672, plain, (~c3_1(a170))). % 5.53/2.16 tff(c_671, plain, (~c1_1(a170))). % 5.53/2.16 tff(c_670, plain, (~c4_1(a171))). % 5.53/2.16 tff(c_668, plain, (![X25_37]: (ndr1_1(X25_37) | ~c2_1(X25_37)))). % 5.53/2.16 tff(c_664, plain, (![X24_36]: (ndr1_1(X24_36) | ~c3_1(X24_36)))). % 5.53/2.16 tff(c_651, plain, (c2_0)). % 5.53/2.16 tff(c_649, plain, (~c4_1(a181))). % 5.53/2.16 tff(c_647, plain, (c1_0)). % 5.53/2.16 tff(c_645, plain, (~c3_0)). % 5.53/2.16 tff(c_644, plain, (~c4_0)). % 5.53/2.16 tff(c_643, plain, (~c5_0)). % 5.53/2.16 tff(c_248, plain, (ndr1_0)). % 5.53/2.16 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 5.53/2.16 %------------------------------------------------------------------------------