%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SYN526+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 : n011.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 8.26s 2.82s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.02/0.09 % Problem : SYN526+1 : TPTP v9.0.0. Released v2.1.0. % 0.02/0.10 % 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.09/0.30 % Computer : n011.cluster.edu % 0.09/0.30 % Model : x86_64 x86_64 % 0.09/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.30 % Memory : 8042.1875MB % 0.09/0.30 % OS : Linux 3.10.0-693.el7.x86_64 % 0.09/0.30 % CPULimit : 300 % 0.09/0.30 % WCLimit : 300 % 0.09/0.30 % DateTime : Wed Apr 9 07:55:33 EDT 2025 % 0.09/0.30 % CPUTime : % 8.26/2.82 % 8.26/2.82 % SZS status CounterSatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 8.26/2.82 % 8.26/2.82 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 8.26/2.83 %$ 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 > a250 > a249 > a248 > a247 > a246 > a245 > a244 > a243 > a242 > a241 > a240 > a239 > a238 > a237 > a236 > a235 > a234 > a233 > a232 > a231 > a230 > a229 > a228 > a227 > a226 > a225 > a224 > a223 > a222 > a221 > a220 > a219 > a218 % 8.26/2.83 % 8.26/2.83 %Foreground sorts: % 8.26/2.83 % 8.26/2.83 % 8.26/2.83 %Background operators: % 8.26/2.83 % 8.26/2.83 % 8.26/2.83 %Foreground operators: % 8.26/2.83 tff(a230, type, a230: $i). % 8.26/2.83 tff(a229, type, a229: $i). % 8.26/2.83 tff(a242, type, a242: $i). % 8.26/2.83 tff(c4_0, type, c4_0: $o). % 8.26/2.83 tff(a249, type, a249: $i). % 8.26/2.83 tff(c3_0, type, c3_0: $o). % 8.26/2.83 tff(c1_2, type, c1_2: ($i * $i) > $o). % 8.26/2.83 tff(a233, type, a233: $i). % 8.26/2.83 tff(a232, type, a232: $i). % 8.26/2.83 tff(a237, type, a237: $i). % 8.26/2.83 tff(a248, type, a248: $i). % 8.26/2.83 tff(a238, type, a238: $i). % 8.26/2.83 tff(a228, type, a228: $i). % 8.26/2.83 tff(c5_0, type, c5_0: $o). % 8.26/2.83 tff(a245, type, a245: $i). % 8.26/2.83 tff(a235, type, a235: $i). % 8.26/2.83 tff(a222, type, a222: $i). % 8.26/2.83 tff(a220, type, a220: $i). % 8.26/2.83 tff(a227, type, a227: $i). % 8.26/2.83 tff(a236, type, a236: $i). % 8.26/2.83 tff(a246, type, a246: $i). % 8.26/2.83 tff(a218, type, a218: $i). % 8.26/2.83 tff(c1_0, type, c1_0: $o). % 8.26/2.83 tff(a240, type, a240: $i). % 8.26/2.83 tff(a234, type, a234: $i). % 8.26/2.83 tff(a250, type, a250: $i). % 8.26/2.83 tff(c2_1, type, c2_1: $i > $o). % 8.26/2.83 tff(a219, type, a219: $i). % 8.26/2.83 tff(ndr1_1, type, ndr1_1: $i > $o). % 8.26/2.83 tff(c2_0, type, c2_0: $o). % 8.26/2.83 tff(c4_1, type, c4_1: $i > $o). % 8.26/2.83 tff(a223, type, a223: $i). % 8.26/2.83 tff(a243, type, a243: $i). % 8.26/2.83 tff(a226, type, a226: $i). % 8.26/2.83 tff(ndr1_0, type, ndr1_0: $o). % 8.26/2.83 tff(a241, type, a241: $i). % 8.26/2.83 tff(a231, type, a231: $i). % 8.26/2.83 tff(a224, type, a224: $i). % 8.26/2.83 tff(c1_1, type, c1_1: $i > $o). % 8.26/2.83 tff(c5_2, type, c5_2: ($i * $i) > $o). % 8.26/2.83 tff(a225, type, a225: $i). % 8.26/2.83 tff(c4_2, type, c4_2: ($i * $i) > $o). % 8.26/2.83 tff(a239, type, a239: $i). % 8.26/2.83 tff(a247, type, a247: $i). % 8.26/2.83 tff(c5_1, type, c5_1: $i > $o). % 8.26/2.83 tff(a221, type, a221: $i). % 8.26/2.83 tff(c3_2, type, c3_2: ($i * $i) > $o). % 8.26/2.83 tff(c2_2, type, c2_2: ($i * $i) > $o). % 8.26/2.83 tff(a244, type, a244: $i). % 8.26/2.83 tff(c3_1, type, c3_1: $i > $o). % 8.26/2.83 % 8.26/2.83 %Saturated clause set: % 8.26/2.83 tff(c_1221, plain, (![Y_6, Z_8]: (c1_2(Y_6, a220) | ~c2_1(Y_6) | ~c2_2(Y_6, Z_8) | c3_2(Y_6, Z_8) | c4_2(Y_6, Z_8) | ~ndr1_1(Y_6)))). % 8.33/2.83 tff(c_1215, plain, (![Y_6]: (~c2_1(Y_6) | ~c2_2(Y_6, a220) | c3_2(Y_6, a220) | ~ndr1_1(Y_6) | c4_2(Y_6, a220)))). % 8.33/2.83 tff(c_1202, plain, (![Y_6, Z_8]: (c4_2(Y_6, a220) | ~c2_1(Y_6) | ~c2_2(Y_6, Z_8) | c3_2(Y_6, Z_8) | c4_2(Y_6, Z_8) | ~ndr1_1(Y_6)))). % 8.33/2.83 tff(c_1198, plain, (![Y_6, Z_8]: (~c3_2(Y_6, a220) | ~c2_1(Y_6) | ~c2_2(Y_6, Z_8) | c3_2(Y_6, Z_8) | c4_2(Y_6, Z_8) | ~ndr1_1(Y_6)))). % 8.33/2.83 tff(c_1146, plain, (![X8_17]: (~c5_2(X8_17, a233) | ~c2_1(X8_17) | c4_1(X8_17)))). % 8.33/2.83 tff(c_1140, plain, (![X8_17]: (c2_2(X8_17, a233) | ~c2_1(X8_17) | c4_1(X8_17)))). % 8.33/2.83 tff(c_1132, plain, (![X8_17]: (c3_2(X8_17, a233) | ~c2_1(X8_17) | c4_1(X8_17)))). % 8.33/2.83 tff(c_1127, plain, (~c2_1(a247))). % 8.33/2.83 tff(c_1121, plain, (![X8_17]: (ndr1_1(X8_17) | ~c2_1(X8_17) | c4_1(X8_17)))). % 8.33/2.83 tff(c_1117, plain, (![X9_18, X10_20]: (~c5_2(X9_18, a234) | ~c5_2(X9_18, X10_20) | ~c4_2(X9_18, X10_20) | ~c2_2(X9_18, X10_20) | ~ndr1_1(X9_18) | ~c1_1(X9_18)))). % 8.33/2.83 tff(c_1099, plain, (![X24_35]: (c4_2(X24_35, a250) | ~c3_1(X24_35) | c4_1(X24_35)))). % 8.33/2.83 tff(c_1095, plain, (![X24_35]: (~c5_2(X24_35, a250) | ~c3_1(X24_35) | c4_1(X24_35)))). % 8.33/2.83 tff(c_1087, plain, (![X24_35]: (ndr1_1(X24_35) | ~c3_1(X24_35) | c4_1(X24_35)))). % 8.33/2.83 tff(c_1026, plain, (~ndr1_1(a247))). % 8.33/2.83 tff(c_873, plain, (~c5_2(a240, a241))). % 8.33/2.83 tff(c_870, plain, (~c1_2(a240, a241))). % 8.33/2.83 tff(c_867, plain, (c3_2(a240, a241))). % 8.33/2.83 tff(c_826, plain, (c3_1(a240))). % 8.33/2.83 tff(c_823, plain, (ndr1_1(a240))). % 8.33/2.84 tff(c_820, plain, (~c2_1(a240))). % 8.33/2.84 tff(c_799, plain, (~c3_1(a247))). % 8.33/2.84 tff(c_774, plain, (~c5_2(a230, a231))). % 8.33/2.84 tff(c_771, plain, (~c1_2(a230, a231))). % 8.33/2.84 tff(c_766, plain, (~c1_0)). % 8.33/2.84 tff(c_761, plain, (~c3_1(a242))). % 8.33/2.84 tff(c_758, plain, (ndr1_1(a230))). % 8.33/2.84 tff(c_755, plain, (c3_1(a230))). % 8.33/2.84 tff(c_752, plain, (~c2_1(a242))). % 8.33/2.84 tff(c_749, plain, (~c4_1(a242))). % 8.33/2.84 tff(c_746, plain, (c2_1(a230))). % 8.33/2.84 tff(c_739, plain, (c2_2(a248, a249))). % 8.33/2.84 tff(c_738, plain, (~c1_2(a248, a249))). % 8.33/2.84 tff(c_737, plain, (c4_2(a248, a249))). % 8.33/2.84 tff(c_736, plain, (c4_0)). % 8.33/2.84 tff(c_730, plain, (ndr1_1(a248))). % 8.33/2.84 tff(c_729, plain, (c3_1(a248))). % 8.33/2.84 tff(c_727, plain, (ndr1_0)). % 8.33/2.84 tff(c_726, plain, (~c3_0)). % 8.33/2.84 tff(c_725, plain, (~c5_0)). % 8.33/2.84 tff(c_8, plain, (~c2_0)). % 8.33/2.84 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 8.33/2.84 %------------------------------------------------------------------------------