%------------------------------------------------------------------------------ % 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/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % Computer : n008.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 : Satisfiable 4.99s 2.08s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : SYN527-1 : TPTP v9.0.0. Released v2.1.0. % 0.06/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % 0.13/0.34 % Computer : n008.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:47 EDT 2025 % 0.13/0.34 % CPUTime : % 4.99/2.08 % 4.99/2.08 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 4.99/2.08 % 4.99/2.08 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 4.99/2.09 %$ c5_2 > c4_2 > c3_2 > c2_2 > c1_2 > ssSkP1 > ssSkP0 > ndr1_1 > c5_1 > c4_1 > c3_1 > c2_1 > c1_1 > #nlpp > ssSkC1 > ssSkC0 > 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 % 4.99/2.09 % 4.99/2.09 %Foreground sorts: % 4.99/2.09 % 4.99/2.09 % 4.99/2.09 %Background operators: % 4.99/2.09 % 4.99/2.09 % 4.99/2.09 %Foreground operators: % 4.99/2.09 tff(a254, type, a254: $i). % 4.99/2.09 tff(a257, type, a257: $i). % 4.99/2.09 tff(c4_0, type, c4_0: $o). % 4.99/2.09 tff(ssSkP0, type, ssSkP0: $i > $o). % 4.99/2.09 tff(c3_0, type, c3_0: $o). % 4.99/2.09 tff(c1_2, type, c1_2: ($i * $i) > $o). % 4.99/2.09 tff(a272, type, a272: $i). % 4.99/2.09 tff(a264, type, a264: $i). % 4.99/2.09 tff(a266, type, a266: $i). % 4.99/2.09 tff(a269, type, a269: $i). % 4.99/2.09 tff(c5_0, type, c5_0: $o). % 4.99/2.09 tff(a268, type, a268: $i). % 4.99/2.09 tff(a261, type, a261: $i). % 4.99/2.09 tff(a270, type, a270: $i). % 4.99/2.09 tff(a265, type, a265: $i). % 4.99/2.09 tff(a251, type, a251: $i). % 4.99/2.09 tff(a275, type, a275: $i). % 4.99/2.09 tff(a273, type, a273: $i). % 4.99/2.09 tff(c1_0, type, c1_0: $o). % 4.99/2.09 tff(a267, type, a267: $i). % 4.99/2.09 tff(c2_1, type, c2_1: $i > $o). % 4.99/2.09 tff(a258, type, a258: $i). % 4.99/2.09 tff(ndr1_1, type, ndr1_1: $i > $o). % 4.99/2.09 tff(c2_0, type, c2_0: $o). % 4.99/2.09 tff(c4_1, type, c4_1: $i > $o). % 4.99/2.09 tff(a274, type, a274: $i). % 4.99/2.09 tff(a271, type, a271: $i). % 4.99/2.09 tff(a252, type, a252: $i). % 4.99/2.09 tff(a260, type, a260: $i). % 4.99/2.09 tff(a263, type, a263: $i). % 4.99/2.09 tff(ndr1_0, type, ndr1_0: $o). % 4.99/2.09 tff(a255, type, a255: $i). % 4.99/2.09 tff(a253, type, a253: $i). % 4.99/2.09 tff(c1_1, type, c1_1: $i > $o). % 4.99/2.09 tff(c5_2, type, c5_2: ($i * $i) > $o). % 4.99/2.09 tff(c4_2, type, c4_2: ($i * $i) > $o). % 4.99/2.09 tff(a259, type, a259: $i). % 4.99/2.09 tff(a276, type, a276: $i). % 4.99/2.09 tff(ssSkC1, type, ssSkC1: $o). % 4.99/2.09 tff(a262, type, a262: $i). % 4.99/2.09 tff(ssSkC0, type, ssSkC0: $o). % 4.99/2.09 tff(ssSkP1, type, ssSkP1: $i > $o). % 4.99/2.09 tff(c5_1, type, c5_1: $i > $o). % 4.99/2.09 tff(c3_2, type, c3_2: ($i * $i) > $o). % 4.99/2.09 tff(c2_2, type, c2_2: ($i * $i) > $o). % 4.99/2.09 tff(c3_1, type, c3_1: $i > $o). % 4.99/2.09 tff(a256, type, a256: $i). % 4.99/2.09 % 4.99/2.09 %Saturated clause set: % 4.99/2.09 tff(c_338, plain, (![U_36, V_37]: (c2_2(U_36, a273) | c1_2(U_36, V_37) | ~ndr1_1(U_36) | ~c2_2(U_36, V_37) | ~c3_2(U_36, V_37) | ~ssSkP1(U_36)))). % 4.99/2.09 tff(c_332, plain, (![U_38, V_39]: (c1_2(U_38, V_39) | ~c5_2(U_38, a273) | ~ndr1_1(U_38) | ~c2_2(U_38, V_39) | ~c3_2(U_38, V_39) | ~ssSkP1(U_38)))). % 4.99/2.09 tff(c_327, plain, (![U_33]: (c3_2(a265, U_33) | c4_2(a265, U_33) | ~c2_2(a265, U_33)))). % 4.99/2.09 tff(c_323, plain, (~c2_2(a270, a271))). % 4.99/2.09 tff(c_316, plain, (c5_2(a270, a271))). % 4.99/2.09 tff(c_313, plain, (c3_2(a270, a271))). % 4.99/2.09 tff(c_305, plain, (~c5_1(a270))). % 4.99/2.09 tff(c_300, plain, (ndr1_1(a270))). % 4.99/2.09 tff(c_291, plain, (c4_1(a270))). % 4.99/2.09 tff(c_285, plain, (c1_1(a251))). % 4.99/2.09 tff(c_279, plain, (~ndr1_1(a251))). % 4.99/2.09 tff(c_275, plain, (ssSkC1)). % 4.99/2.09 tff(c_271, plain, (![U_12]: (c4_1(U_12) | c3_1(U_12)))). % 4.99/2.09 tff(c_267, plain, (![U_10]: (c1_1(U_10) | c3_2(U_10, a261)))). % 4.99/2.09 tff(c_263, plain, (![U_9]: (c1_1(U_9) | c1_2(U_9, a261)))). % 4.99/2.09 tff(c_259, plain, (![U_8]: (c1_1(U_8) | c4_2(U_8, a261)))). % 4.99/2.10 tff(c_255, plain, (![U_7]: (c1_1(U_7) | ndr1_1(U_7)))). % 4.99/2.10 tff(c_70, plain, (![U_6]: (ssSkP0(U_6) | ~c2_2(U_6, a254)))). % 4.99/2.10 tff(c_247, plain, (c5_2(a265, a266))). % 4.99/2.10 tff(c_245, plain, (c1_2(a265, a266))). % 4.99/2.10 tff(c_68, plain, (![U_5]: (ssSkP1(U_5) | ~c2_2(U_5, a272)))). % 4.99/2.10 tff(c_66, plain, (![U_4]: (ssSkP1(U_4) | ~c1_2(U_4, a272)))). % 4.99/2.10 tff(c_36, plain, (![U_3]: (ssSkP0(U_3) | c5_2(U_3, a254)))). % 4.99/2.10 tff(c_18, plain, (![U_1]: (ssSkP1(U_1) | ndr1_1(U_1)))). % 4.99/2.10 tff(c_229, plain, (ndr1_1(a265))). % 4.99/2.10 tff(c_230, plain, (c3_0)). % 4.99/2.10 tff(c_20, plain, (![U_2]: (ssSkP0(U_2) | ndr1_1(U_2)))). % 4.99/2.10 tff(c_187, plain, (c4_1(a264))). % 4.99/2.10 tff(c_186, plain, (~c2_1(a264))). % 4.99/2.10 tff(c_183, plain, (~c5_1(a264))). % 4.99/2.10 tff(c_182, plain, (~ssSkC0)). % 4.99/2.10 tff(c_180, plain, (c4_0)). % 4.99/2.10 tff(c_175, plain, (c5_1(a251))). % 4.99/2.10 tff(c_171, plain, (ndr1_0)). % 4.99/2.10 tff(c_170, plain, (~c2_0)). % 4.99/2.10 tff(c_169, plain, (~c1_0)). % 4.99/2.10 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 4.99/2.10 %------------------------------------------------------------------------------