%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SYN527+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 : n031.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:49 PM UTC 2025 % Result : CounterSatisfiable 5.77s 2.62s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.09/0.15 % Problem : SYN527+1 : TPTP v9.0.0. Released v2.1.0. % 0.09/0.16 % 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.16/0.38 % Computer : n031.cluster.edu % 0.16/0.38 % Model : x86_64 x86_64 % 0.16/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.38 % Memory : 8042.1875MB % 0.16/0.38 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.38 % CPULimit : 300 % 0.16/0.38 % WCLimit : 300 % 0.16/0.38 % DateTime : Wed Apr 9 07:55:52 EDT 2025 % 0.16/0.38 % CPUTime : % 5.77/2.62 % 5.77/2.62 % SZS status CounterSatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 5.77/2.62 % 5.77/2.62 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 5.77/2.63 %$ 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 > a276 > a275 > a274 > a273 > a272 > a271 > a270 > a269 > a268 > a267 > a266 > a265 > a264 > a263 > a262 > a261 > a260 > a259 > a258 > a257 > a256 > a255 > a254 > a253 > a252 > a251 % 5.77/2.63 % 5.77/2.63 %Foreground sorts: % 5.77/2.63 % 5.77/2.63 % 5.77/2.63 %Background operators: % 5.77/2.63 % 5.77/2.63 % 5.77/2.63 %Foreground operators: % 5.77/2.63 tff(a254, type, a254: $i). % 5.77/2.63 tff(a257, type, a257: $i). % 5.77/2.63 tff(c4_0, type, c4_0: $o). % 5.77/2.63 tff(c3_0, type, c3_0: $o). % 5.77/2.63 tff(c1_2, type, c1_2: ($i * $i) > $o). % 5.77/2.63 tff(a272, type, a272: $i). % 5.77/2.63 tff(a264, type, a264: $i). % 5.77/2.63 tff(a266, type, a266: $i). % 5.77/2.63 tff(a269, type, a269: $i). % 5.77/2.63 tff(c5_0, type, c5_0: $o). % 5.77/2.63 tff(a268, type, a268: $i). % 5.77/2.63 tff(a261, type, a261: $i). % 5.77/2.63 tff(a270, type, a270: $i). % 5.77/2.63 tff(a265, type, a265: $i). % 5.77/2.63 tff(a251, type, a251: $i). % 5.77/2.63 tff(a275, type, a275: $i). % 5.77/2.63 tff(a273, type, a273: $i). % 5.77/2.63 tff(c1_0, type, c1_0: $o). % 5.77/2.63 tff(a267, type, a267: $i). % 5.77/2.63 tff(c2_1, type, c2_1: $i > $o). % 5.77/2.63 tff(a258, type, a258: $i). % 5.77/2.63 tff(ndr1_1, type, ndr1_1: $i > $o). % 5.77/2.63 tff(c2_0, type, c2_0: $o). % 5.77/2.63 tff(c4_1, type, c4_1: $i > $o). % 5.77/2.63 tff(a274, type, a274: $i). % 5.77/2.63 tff(a271, type, a271: $i). % 5.77/2.63 tff(a252, type, a252: $i). % 5.77/2.63 tff(a260, type, a260: $i). % 5.77/2.63 tff(a263, type, a263: $i). % 5.77/2.63 tff(ndr1_0, type, ndr1_0: $o). % 5.77/2.63 tff(a255, type, a255: $i). % 5.77/2.63 tff(a253, type, a253: $i). % 5.77/2.63 tff(c1_1, type, c1_1: $i > $o). % 5.77/2.63 tff(c5_2, type, c5_2: ($i * $i) > $o). % 5.77/2.63 tff(c4_2, type, c4_2: ($i * $i) > $o). % 5.77/2.63 tff(a259, type, a259: $i). % 5.77/2.63 tff(a276, type, a276: $i). % 5.77/2.63 tff(a262, type, a262: $i). % 5.77/2.63 tff(c5_1, type, c5_1: $i > $o). % 5.77/2.63 tff(c3_2, type, c3_2: ($i * $i) > $o). % 5.77/2.63 tff(c2_2, type, c2_2: ($i * $i) > $o). % 5.77/2.63 tff(c3_1, type, c3_1: $i > $o). % 5.77/2.63 tff(a256, type, a256: $i). % 5.77/2.63 % 5.77/2.63 %Saturated clause set: % 5.77/2.64 tff(c_372, plain, (c5_2(a270, a271))). % 5.77/2.64 tff(c_369, plain, (c3_2(a270, a271))). % 5.77/2.64 tff(c_364, plain, (~c2_2(a270, a271))). % 5.77/2.64 tff(c_353, plain, (~c5_1(a270))). % 5.77/2.64 tff(c_350, plain, (c2_1(a270))). % 5.77/2.64 tff(c_346, plain, (c4_1(a270))). % 5.77/2.64 tff(c_343, plain, (ndr1_1(a270))). % 5.77/2.64 tff(c_309, plain, (c4_0)). % 5.77/2.64 tff(c_305, plain, (![Z_7]: (c3_2(a258, Z_7) | c1_2(a258, Z_7)))). % 5.77/2.64 tff(c_288, plain, (![X3_10]: (~c4_1(X3_10) | c2_1(X3_10)))). % 5.77/2.64 tff(c_272, plain, (~c2_1(a260))). % 5.77/2.64 tff(c_269, plain, (c1_1(a260))). % 5.77/2.64 tff(c_259, plain, (c5_0)). % 5.77/2.64 tff(c_257, plain, (~c5_1(a264))). % 5.77/2.64 tff(c_254, plain, (c3_2(a258, a259))). % 5.77/2.64 tff(c_252, plain, (c5_2(a258, a259))). % 5.77/2.64 tff(c_246, plain, (~c3_0)). % 5.77/2.64 tff(c_242, plain, (ndr1_1(a258))). % 5.77/2.64 tff(c_240, plain, (~c2_1(a258))). % 5.77/2.64 tff(c_238, plain, (~c1_0)). % 5.77/2.64 tff(c_235, plain, (ndr1_0)). % 5.77/2.64 tff(c_233, plain, (c2_0)). % 5.77/2.64 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 5.77/2.64 %------------------------------------------------------------------------------