%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : KRS007-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 : n017.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:09 PM UTC 2025 % Result : Satisfiable 3.42s 1.84s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : KRS007-1 : TPTP v9.0.0. Released v2.0.0. % 0.07/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.14/0.34 % Computer : n017.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 300 % 0.14/0.34 % DateTime : Tue Apr 8 02:52:55 EDT 2025 % 0.14/0.34 % CPUTime : % 3.42/1.84 % 3.42/1.84 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 3.42/1.84 % 3.42/1.84 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 3.42/1.85 %$ s > r > equalish > s2least > s1most > r2least > f > e > d > c > #nlpp > u6r2 > u6r1 > u4r3 > u4r2 > u4r1 > u3r2 > u3r1 > u1r2 > u1r1 > exist % 3.42/1.85 % 3.42/1.85 %Foreground sorts: % 3.42/1.85 % 3.42/1.85 % 3.42/1.85 %Background operators: % 3.42/1.85 % 3.42/1.85 % 3.42/1.85 %Foreground operators: % 3.42/1.85 tff(s, type, s: ($i * $i) > $o). % 3.42/1.85 tff(s1most, type, s1most: $i > $o). % 3.42/1.85 tff(d, type, d: $i > $o). % 3.42/1.85 tff(u3r1, type, u3r1: $i > $i). % 3.42/1.85 tff(u6r2, type, u6r2: $i > $i). % 3.42/1.85 tff(u1r1, type, u1r1: $i > $i). % 3.42/1.85 tff(u4r1, type, u4r1: $i > $i). % 3.42/1.85 tff(u4r3, type, u4r3: $i > $i). % 3.42/1.85 tff(u3r2, type, u3r2: $i > $i). % 3.42/1.85 tff(u4r2, type, u4r2: $i > $i). % 3.42/1.85 tff(c, type, c: $i > $o). % 3.42/1.85 tff(e, type, e: $i > $o). % 3.42/1.85 tff(s2least, type, s2least: $i > $o). % 3.42/1.85 tff(u6r1, type, u6r1: $i > $i). % 3.42/1.85 tff(exist, type, exist: $i). % 3.42/1.85 tff(equalish, type, equalish: ($i * $i) > $o). % 3.42/1.85 tff(u1r2, type, u1r2: $i > $i). % 3.42/1.85 tff(r, type, r: ($i * $i) > $o). % 3.42/1.85 tff(f, type, f: $i > $o). % 3.42/1.85 tff(r2least, type, r2least: $i > $o). % 3.42/1.85 % 3.42/1.85 %Saturated clause set: % 3.53/1.85 tff(c_264, plain, (![X1_30]: (~c(u6r1(X1_30)) | e(X1_30) | c(u6r2(X1_30)) | ~r2least(X1_30)))). % 3.53/1.85 tff(c_231, plain, (![X1_30, X2_96]: (~c(u6r2(X1_30)) | ~r(X1_30, X2_96) | e(X1_30) | c(u6r1(X1_30)) | ~r2least(X1_30)))). % 3.53/1.85 tff(c_217, plain, (![X3_92, X1_91, X2_93]: (~c(X3_92) | ~r(X1_91, X3_92) | ~r(X1_91, X2_93) | e(X1_91) | ~r2least(X1_91) | c(u6r2(X1_91))))). % 3.53/1.85 tff(c_212, plain, (![X3_89, X1_88, X2_90]: (~c(X3_89) | ~r(X1_88, X3_89) | ~r(X1_88, X2_90) | e(X1_88) | ~r2least(X1_88) | c(u6r1(X1_88))))). % 3.53/1.85 tff(c_140, plain, (![X1_30, X3_65, X2_66]: (~d(u6r2(X1_30)) | ~c(X3_65) | ~r(X1_30, X3_65) | ~r(X1_30, X2_66) | e(X1_30) | ~r2least(X1_30)))). % 3.53/1.85 tff(c_141, plain, (![X1_29, X3_65, X2_66]: (~d(u6r1(X1_29)) | ~c(X3_65) | ~r(X1_29, X3_65) | ~r(X1_29, X2_66) | e(X1_29) | ~r2least(X1_29)))). % 3.53/1.85 tff(c_206, plain, (![X1_17]: (~c(u4r3(X1_17)) | ~e(X1_17)))). % 3.53/1.85 tff(c_197, plain, (![X1_9]: (~c(X1_9) | ~d(X1_9)))). % 3.53/1.85 tff(c_188, plain, (![X1_1]: (~s1most(X1_1) | ~c(X1_1)))). % 3.53/1.85 tff(c_179, plain, (![X1_5]: (~s1most(X1_5) | ~s2least(X1_5)))). % 3.53/1.85 tff(c_110, plain, (![X1_21, X3_59]: (~r(X1_21, X3_59) | equalish(X3_59, u4r1(X1_21)) | r2least(X1_21) | ~e(X1_21)))). % 3.53/1.85 tff(c_166, plain, (![X1_77]: (d(X1_77) | c(X1_77)))). % 3.53/1.85 tff(c_161, plain, (![X1_76]: (c(X1_76) | s1most(X1_76)))). % 3.53/1.85 tff(c_156, plain, (![X1_16]: (s2least(X1_16) | s1most(X1_16)))). % 3.53/1.85 tff(c_109, plain, (![X1_20, X3_59]: (~r(X1_20, X3_59) | equalish(X3_59, u4r2(X1_20)) | r2least(X1_20) | ~e(X1_20)))). % 3.53/1.85 tff(c_113, plain, (![X1_18, X3_59]: (~r(X1_18, X3_59) | equalish(X3_59, u4r3(X1_18)) | r2least(X1_18) | ~e(X1_18)))). % 3.53/1.85 tff(c_40, plain, (![X4_25, X1_22, X3_24, X2_23]: (~d(X4_25) | ~r(X1_22, X4_25) | ~c(X3_24) | ~r(X1_22, X3_24) | ~r(X1_22, X2_23) | e(X1_22)))). % 3.53/1.85 tff(c_22, plain, (![X1_13, X2_12, X3_11]: (~s(X1_13, X2_12) | ~s(X1_13, X3_11) | ~s1most(X1_13) | equalish(X3_11, X2_12)))). % 3.53/1.85 tff(c_52, plain, (![X1_31, X2_33, X3_32]: (~r(X1_31, X2_33) | ~r(X1_31, X3_32) | equalish(X3_32, X2_33) | r2least(X1_31)))). % 3.53/1.85 tff(c_16, plain, (![X1_6, X2_8, X3_7]: (~s(X1_6, X2_8) | ~s(X1_6, X3_7) | equalish(X3_7, X2_8) | s2least(X1_6)))). % 3.53/1.86 tff(c_24, plain, (![X1_14]: (~equalish(u3r2(X1_14), u3r1(X1_14)) | s1most(X1_14)))). % 3.53/1.86 tff(c_46, plain, (![X1_28]: (~equalish(u6r2(X1_28), u6r1(X1_28)) | ~r2least(X1_28)))). % 3.53/1.86 tff(c_10, plain, (![X1_3]: (~equalish(u1r2(X1_3), u1r1(X1_3)) | ~s2least(X1_3)))). % 3.53/1.86 tff(c_36, plain, (![X1_20]: (~e(X1_20) | r(X1_20, u4r2(X1_20))))). % 3.53/1.86 tff(c_12, plain, (![X1_4]: (~s2least(X1_4) | s(X1_4, u1r1(X1_4))))). % 3.53/1.86 tff(c_38, plain, (![X1_21]: (~e(X1_21) | r(X1_21, u4r1(X1_21))))). % 3.53/1.86 tff(c_50, plain, (![X1_30]: (~r2least(X1_30) | r(X1_30, u6r2(X1_30))))). % 3.53/1.86 tff(c_14, plain, (![X1_5]: (~s2least(X1_5) | s(X1_5, u1r2(X1_5))))). % 3.53/1.86 tff(c_48, plain, (![X1_29]: (~r2least(X1_29) | r(X1_29, u6r1(X1_29))))). % 3.53/1.86 tff(c_26, plain, (![X1_15]: (s(X1_15, u3r1(X1_15)) | s1most(X1_15)))). % 3.53/1.86 tff(c_32, plain, (![X1_18]: (~e(X1_18) | r(X1_18, u4r3(X1_18))))). % 3.53/1.86 tff(c_28, plain, (![X1_16]: (s(X1_16, u3r2(X1_16)) | s1most(X1_16)))). % 3.53/1.86 tff(c_34, plain, (![X1_19]: (~e(X1_19) | c(u4r2(X1_19))))). % 3.53/1.86 tff(c_30, plain, (![X1_17]: (~e(X1_17) | d(u4r3(X1_17))))). % 3.53/1.86 tff(c_6, plain, (![X1_1]: (~c(X1_1) | s2least(X1_1)))). % 3.53/1.86 tff(c_42, plain, (![X1_26]: (~f(X1_26) | r2least(X1_26)))). % 3.53/1.86 tff(c_44, plain, (![X1_27]: (~r2least(X1_27) | f(X1_27)))). % 3.53/1.86 tff(c_8, plain, (![X1_2]: (~s2least(X1_2) | c(X1_2)))). % 3.53/1.86 tff(c_18, plain, (![X1_9]: (~d(X1_9) | s1most(X1_9)))). % 3.53/1.86 tff(c_20, plain, (![X1_10]: (~s1most(X1_10) | d(X1_10)))). % 3.53/1.86 tff(c_2, plain, (e(exist))). % 3.53/1.86 tff(c_4, plain, (~f(exist))). % 3.53/1.86 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 3.53/1.86 %------------------------------------------------------------------------------