%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : KRS016-1 : TPTP v9.0.0. Released v2.0.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 : n016.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 07:07:10 PM UTC 2025 % Result : Satisfiable 3.28s 1.79s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.13 % Problem : KRS016-1 : TPTP v9.0.0. Released v2.0.0. % 0.03/0.14 % 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.35 % Computer : n016.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 300 % 0.13/0.35 % DateTime : Tue Apr 8 02:54:08 EDT 2025 % 0.13/0.35 % CPUTime : % 3.28/1.79 % 3.28/1.79 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 3.28/1.79 % 3.28/1.79 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 3.28/1.79 %$ s > r > equalish > s1most > r1most > d > c > #nlpp > u3r2 > u3r1 > u2r1 > u1r2 > u1r1 > u0r1 > exist % 3.28/1.79 % 3.28/1.79 %Foreground sorts: % 3.28/1.79 % 3.28/1.79 % 3.28/1.79 %Background operators: % 3.28/1.79 % 3.28/1.79 % 3.28/1.79 %Foreground operators: % 3.28/1.79 tff(s, type, s: ($i * $i) > $o). % 3.28/1.79 tff(u0r1, type, u0r1: $i > $i). % 3.28/1.79 tff(s1most, type, s1most: $i > $o). % 3.28/1.79 tff(d, type, d: $i > $o). % 3.28/1.79 tff(u3r1, type, u3r1: $i > $i). % 3.28/1.79 tff(u1r1, type, u1r1: $i > $i). % 3.28/1.79 tff(r1most, type, r1most: $i > $o). % 3.28/1.79 tff(u3r2, type, u3r2: $i > $i). % 3.28/1.79 tff(c, type, c: $i > $o). % 3.28/1.79 tff(u2r1, type, u2r1: $i > $i). % 3.28/1.79 tff(exist, type, exist: $i). % 3.28/1.79 tff(equalish, type, equalish: ($i * $i) > $o). % 3.28/1.79 tff(u1r2, type, u1r2: $i > $i). % 3.28/1.79 tff(r, type, r: ($i * $i) > $o). % 3.28/1.79 % 3.28/1.79 %Saturated clause set: % 3.28/1.80 tff(c_230, plain, (![X1_60, X3_8]: (~r(X1_60, X3_8) | ~s(X1_60, X3_8) | ~s1most(X1_60) | ~r1most(X1_60) | c(X1_60) | equalish(X3_8, u0r1(X1_60))))). % 3.28/1.80 tff(c_182, plain, (![X1_60, X3_8, X3_61]: (~r(X1_60, X3_8) | equalish(X3_8, u0r1(X1_60)) | ~s(X1_60, X3_61) | ~s1most(X1_60) | equalish(X3_61, u0r1(X1_60)) | ~r1most(X1_60) | c(X1_60)))). % 3.28/1.80 tff(c_201, plain, (![X2_65, X1_18]: (equalish(X2_65, u2r1(X1_18)) | ~r(X1_18, X2_65) | ~c(X1_18) | ~s1most(X1_18) | d(X1_18)))). % 3.28/1.80 tff(c_215, plain, (![X1_24]: (~r1most(X1_24) | ~c(X1_24) | s1most(X1_24)))). % 3.28/1.80 tff(c_171, plain, (![X1_17, X2_57]: (equalish(u2r1(X1_17), X2_57) | ~r(X1_17, X2_57) | ~c(X1_17) | ~s1most(X1_17) | d(X1_17)))). % 3.28/1.80 tff(c_172, plain, (![X1_1, X2_2, X2_57]: (~s1most(X1_1) | equalish(X2_2, X2_57) | ~r(X1_1, X2_57) | ~r(X1_1, X2_2) | ~c(X1_1)))). % 3.28/1.80 tff(c_156, plain, (![X1_54, X3_19]: (~s(X1_54, X3_19) | ~s1most(X1_54) | equalish(X3_19, u0r1(X1_54)) | ~r1most(X1_54) | r(X1_54, u0r1(X1_54)) | c(X1_54)))). % 3.28/1.80 tff(c_120, plain, (![X1_18, X3_47]: (~r(X1_18, X3_47) | ~r1most(X1_18) | equalish(X3_47, u2r1(X1_18)) | ~s1most(X1_18) | d(X1_18)))). % 3.28/1.80 tff(c_133, plain, (![X1_1, X3_50, X2_2]: (~s(X1_1, X3_50) | ~s1most(X1_1) | equalish(X3_50, X2_2) | ~r(X1_1, X2_2) | ~c(X1_1)))). % 3.28/1.80 tff(c_12, plain, (![X1_6]: (~r1most(X1_6) | r(X1_6, u0r1(X1_6)) | s(X1_6, u0r1(X1_6)) | c(X1_6)))). % 3.28/1.80 tff(c_14, plain, (![X1_7]: (~s(X1_7, u0r1(X1_7)) | ~r(X1_7, u0r1(X1_7)) | ~r1most(X1_7) | c(X1_7)))). % 3.28/1.80 tff(c_132, plain, (![X1_17, X3_50]: (~s(X1_17, X3_50) | equalish(X3_50, u2r1(X1_17)) | ~s1most(X1_17) | d(X1_17)))). % 3.28/1.80 tff(c_32, plain, (![X1_21, X2_20, X3_19]: (~s(X1_21, X2_20) | ~s(X1_21, X3_19) | ~s1most(X1_21) | equalish(X3_19, X2_20)))). % 3.28/1.80 tff(c_16, plain, (![X1_10, X2_9, X3_8]: (~r(X1_10, X2_9) | ~r(X1_10, X3_8) | ~r1most(X1_10) | equalish(X3_8, X2_9)))). % 3.28/1.80 tff(c_54, plain, (![X1_24]: (~c(X1_24) | r(X1_24, u3r2(X1_24)) | s1most(X1_24)))). % 3.28/1.80 tff(c_55, plain, (![X1_23]: (~c(X1_23) | r(X1_23, u3r1(X1_23)) | s1most(X1_23)))). % 3.28/1.80 tff(c_28, plain, (![X1_17]: (~s1most(X1_17) | s(X1_17, u2r1(X1_17)) | d(X1_17)))). % 3.28/1.80 tff(c_30, plain, (![X1_18]: (~s1most(X1_18) | r(X1_18, u2r1(X1_18)) | d(X1_18)))). % 3.28/1.80 tff(c_72, plain, (![X1_37, X2_38]: (~d(X1_37) | ~r(X1_37, X2_38) | ~c(X1_37)))). % 3.28/1.80 tff(c_6, plain, (![X1_1, X2_2]: (~r(X1_1, X2_2) | ~c(X1_1) | s(X1_1, X2_2)))). % 3.28/1.80 tff(c_24, plain, (![X1_14, X2_15]: (~s(X1_14, X2_15) | ~r(X1_14, X2_15) | ~d(X1_14)))). % 3.28/1.80 tff(c_8, plain, (![X1_3, X2_4]: (~s(X1_3, X2_4) | ~c(X1_3) | r(X1_3, X2_4)))). % 3.28/1.80 tff(c_18, plain, (![X1_11]: (~equalish(u1r2(X1_11), u1r1(X1_11)) | r1most(X1_11)))). % 3.28/1.80 tff(c_34, plain, (![X1_22]: (~equalish(u3r2(X1_22), u3r1(X1_22)) | s1most(X1_22)))). % 3.28/1.80 tff(c_20, plain, (![X1_12]: (r(X1_12, u1r1(X1_12)) | r1most(X1_12)))). % 3.28/1.80 tff(c_38, plain, (![X1_24]: (s(X1_24, u3r2(X1_24)) | s1most(X1_24)))). % 3.28/1.80 tff(c_36, plain, (![X1_23]: (s(X1_23, u3r1(X1_23)) | s1most(X1_23)))). % 3.28/1.80 tff(c_22, plain, (![X1_13]: (r(X1_13, u1r2(X1_13)) | r1most(X1_13)))). % 3.28/1.80 tff(c_10, plain, (![X1_5]: (~c(X1_5) | r1most(X1_5)))). % 3.28/1.80 tff(c_26, plain, (![X1_16]: (~d(X1_16) | s1most(X1_16)))). % 3.28/1.80 tff(c_2, plain, (c(exist))). % 3.28/1.80 tff(c_4, plain, (d(exist))). % 3.28/1.81 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 3.28/1.81 %------------------------------------------------------------------------------