%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : KRS006-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 : n029.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:08 PM UTC 2025 % Result : Satisfiable 3.35s 1.84s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.12 % Problem : KRS006-1 : TPTP v9.0.0. Released v2.0.0. % 0.12/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 : n029.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 : Tue Apr 8 02:53:04 EDT 2025 % 0.13/0.34 % CPUTime : % 3.35/1.84 % 3.35/1.84 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 3.35/1.84 % 3.35/1.84 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 3.35/1.85 %$ s > r > equalish > s2least > s1most > r1most > e > d > c > #nlpp > u5r2 > u5r1 > u4r2 > u4r1 > u3r2 > u3r1 > u1r2 > u1r1 > exist % 3.35/1.85 % 3.35/1.85 %Foreground sorts: % 3.35/1.85 % 3.35/1.85 % 3.35/1.85 %Background operators: % 3.35/1.85 % 3.35/1.85 % 3.35/1.85 %Foreground operators: % 3.35/1.85 tff(s, type, s: ($i * $i) > $o). % 3.35/1.85 tff(s1most, type, s1most: $i > $o). % 3.35/1.85 tff(u5r2, type, u5r2: $i > $i). % 3.35/1.85 tff(d, type, d: $i > $o). % 3.35/1.85 tff(u3r1, type, u3r1: $i > $i). % 3.35/1.85 tff(u1r1, type, u1r1: $i > $i). % 3.35/1.85 tff(u4r1, type, u4r1: $i > $i). % 3.35/1.85 tff(r1most, type, r1most: $i > $o). % 3.35/1.85 tff(u3r2, type, u3r2: $i > $i). % 3.35/1.85 tff(u4r2, type, u4r2: $i > $i). % 3.35/1.85 tff(c, type, c: $i > $o). % 3.35/1.85 tff(e, type, e: $i > $o). % 3.35/1.85 tff(s2least, type, s2least: $i > $o). % 3.35/1.85 tff(exist, type, exist: $i). % 3.35/1.85 tff(equalish, type, equalish: ($i * $i) > $o). % 3.35/1.85 tff(u5r1, type, u5r1: $i > $i). % 3.35/1.85 tff(u1r2, type, u1r2: $i > $i). % 3.35/1.85 tff(r, type, r: ($i * $i) > $o). % 3.35/1.85 % 3.35/1.85 %Saturated clause set: % 3.35/1.85 tff(c_95, plain, (![X1_20, X3_51]: (~r(X1_20, X3_51) | ~r1most(X1_20) | equalish(X3_51, u4r1(X1_20)) | ~e(X1_20)))). % 3.35/1.85 tff(c_206, plain, (![X1_79]: (d(X1_79) | c(X1_79)))). % 3.35/1.86 tff(c_197, plain, (![X1_78]: (c(X1_78) | s1most(X1_78)))). % 3.35/1.86 tff(c_188, plain, (![X1_16]: (s2least(X1_16) | s1most(X1_16)))). % 3.35/1.86 tff(c_174, plain, (![X1_17]: (~c(u4r2(X1_17)) | ~e(X1_17)))). % 3.35/1.86 tff(c_175, plain, (~c(u4r2(exist)))). % 3.35/1.86 tff(c_93, plain, (![X1_18, X3_51]: (~r(X1_18, X3_51) | ~r1most(X1_18) | equalish(X3_51, u4r2(X1_18)) | ~e(X1_18)))). % 3.35/1.86 tff(c_166, plain, (![X1_9]: (~c(X1_9) | ~d(X1_9)))). % 3.35/1.86 tff(c_161, plain, (![X1_1]: (~s1most(X1_1) | ~c(X1_1)))). % 3.35/1.86 tff(c_156, plain, (![X1_5]: (~s1most(X1_5) | ~s2least(X1_5)))). % 3.35/1.86 tff(c_46, plain, (![X3_24, X1_22, X2_23]: (~d(X3_24) | ~r(X1_22, X3_24) | ~c(X2_23) | ~r(X1_22, X2_23) | ~r1most(X1_22) | e(X1_22)))). % 3.35/1.86 tff(c_28, 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.35/1.86 tff(c_22, 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.35/1.86 tff(c_98, plain, (![X3_51]: (~r(exist, X3_51) | equalish(X3_51, u4r1(exist))))). % 3.35/1.86 tff(c_48, plain, (![X1_27, X2_26, X3_25]: (~r(X1_27, X2_26) | ~r(X1_27, X3_25) | ~r1most(X1_27) | equalish(X3_25, X2_26)))). % 3.35/1.86 tff(c_50, plain, (![X1_28]: (~equalish(u5r2(X1_28), u5r1(X1_28)) | r1most(X1_28)))). % 3.35/1.86 tff(c_30, plain, (![X1_14]: (~equalish(u3r2(X1_14), u3r1(X1_14)) | s1most(X1_14)))). % 3.35/1.86 tff(c_16, plain, (![X1_3]: (~equalish(u1r2(X1_3), u1r1(X1_3)) | ~s2least(X1_3)))). % 3.35/1.86 tff(c_18, plain, (![X1_4]: (~s2least(X1_4) | s(X1_4, u1r1(X1_4))))). % 3.35/1.86 tff(c_32, plain, (![X1_15]: (s(X1_15, u3r1(X1_15)) | s1most(X1_15)))). % 3.35/1.86 tff(c_34, plain, (![X1_16]: (s(X1_16, u3r2(X1_16)) | s1most(X1_16)))). % 3.35/1.86 tff(c_52, plain, (![X1_29]: (r(X1_29, u5r1(X1_29)) | r1most(X1_29)))). % 3.35/1.86 tff(c_20, plain, (![X1_5]: (~s2least(X1_5) | s(X1_5, u1r2(X1_5))))). % 3.35/1.86 tff(c_38, plain, (![X1_18]: (~e(X1_18) | r(X1_18, u4r2(X1_18))))). % 3.35/1.86 tff(c_54, plain, (![X1_30]: (r(X1_30, u5r2(X1_30)) | r1most(X1_30)))). % 3.35/1.86 tff(c_42, plain, (![X1_20]: (~e(X1_20) | r(X1_20, u4r1(X1_20))))). % 3.35/1.86 tff(c_36, plain, (![X1_17]: (~e(X1_17) | d(u4r2(X1_17))))). % 3.35/1.86 tff(c_40, plain, (![X1_19]: (~e(X1_19) | c(u4r1(X1_19))))). % 3.35/1.86 tff(c_14, plain, (![X1_2]: (~s2least(X1_2) | c(X1_2)))). % 3.35/1.86 tff(c_12, plain, (![X1_1]: (~c(X1_1) | s2least(X1_1)))). % 3.35/1.86 tff(c_6, plain, (r(exist, u4r1(exist)))). % 3.35/1.86 tff(c_26, plain, (![X1_10]: (~s1most(X1_10) | d(X1_10)))). % 3.35/1.86 tff(c_24, plain, (![X1_9]: (~d(X1_9) | s1most(X1_9)))). % 3.35/1.86 tff(c_44, plain, (![X1_21]: (~e(X1_21) | r1most(X1_21)))). % 3.35/1.86 tff(c_8, plain, (d(u4r2(exist)))). % 3.35/1.86 tff(c_10, plain, (c(u4r1(exist)))). % 3.35/1.86 tff(c_2, plain, (e(exist))). % 3.35/1.86 tff(c_4, plain, (r1most(exist))). % 3.35/1.86 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 3.35/1.86 %------------------------------------------------------------------------------