%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : KRS014-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.33s 1.78s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : KRS014-1 : TPTP v9.0.0. Released v2.0.0. % 0.03/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.12/0.34 % Computer : n017.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Tue Apr 8 02:53:25 EDT 2025 % 0.12/0.34 % CPUTime : % 3.33/1.78 % 3.33/1.78 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 3.33/1.78 % 3.33/1.78 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 3.33/1.78 %$ s > r > equalish > s2exact > r1exact > e > u2r1 > u1r1 > #nlpp > u2r3 > u2r2 > u1r2 > u0r1 > exists % 3.33/1.78 % 3.33/1.78 %Foreground sorts: % 3.33/1.78 % 3.33/1.78 % 3.33/1.78 %Background operators: % 3.33/1.78 % 3.33/1.78 % 3.33/1.78 %Foreground operators: % 3.33/1.78 tff(s, type, s: ($i * $i) > $o). % 3.33/1.78 tff(u0r1, type, u0r1: $i > $i). % 3.33/1.78 tff(u2r1, type, u2r1: ($i * $i * $i) > $i). % 3.33/1.78 tff(u2r3, type, u2r3: $i > $i). % 3.33/1.78 tff(u2r2, type, u2r2: $i > $i). % 3.33/1.78 tff(r1exact, type, r1exact: $i > $o). % 3.33/1.78 tff(e, type, e: $i > $o). % 3.33/1.78 tff(exists, type, exists: $i). % 3.33/1.78 tff(s2exact, type, s2exact: $i > $o). % 3.33/1.78 tff(equalish, type, equalish: ($i * $i) > $o). % 3.33/1.78 tff(u1r2, type, u1r2: $i > $i). % 3.33/1.78 tff(r, type, r: ($i * $i) > $o). % 3.33/1.78 tff(u1r1, type, u1r1: ($i * $i) > $i). % 3.33/1.78 % 3.33/1.78 %Saturated clause set: % 3.33/1.79 tff(c_157, plain, (![X1_79, X1_1]: (~s(X1_79, u2r3(X1_1)) | ~s(X1_79, u2r2(X1_1)) | equalish(u2r2(X1_1), u2r3(X1_1)) | s2exact(X1_79) | ~s2exact(X1_1) | ~r(X1_1, u2r1(u2r2(X1_1), u2r3(X1_1), X1_79)) | ~e(X1_1)))). % 3.33/1.79 tff(c_146, plain, (![X1_77, X1_1]: (~s(X1_77, u2r2(X1_1)) | ~s(X1_77, u2r3(X1_1)) | equalish(u2r3(X1_1), u2r2(X1_1)) | s2exact(X1_77) | ~s2exact(X1_1) | ~r(X1_1, u2r1(u2r3(X1_1), u2r2(X1_1), X1_77)) | ~e(X1_1)))). % 3.33/1.79 tff(c_135, plain, (![X1_74, X1_75]: (~s(X1_74, u2r3(X1_75)) | ~s(X1_74, u2r2(X1_75)) | equalish(u2r2(X1_75), u2r3(X1_75)) | s2exact(X1_74) | ~s(X1_75, u2r1(u2r2(X1_75), u2r3(X1_75), X1_74)) | ~s2exact(X1_75)))). % 3.33/1.79 tff(c_129, plain, (![X1_71, X1_73]: (~s(X1_71, u2r2(X1_73)) | ~s(X1_71, u2r3(X1_73)) | equalish(u2r3(X1_73), u2r2(X1_73)) | s2exact(X1_71) | ~s(X1_73, u2r1(u2r3(X1_73), u2r2(X1_73), X1_71)) | ~s2exact(X1_73)))). % 3.33/1.79 tff(c_114, plain, (![X1_59, X1_17, X3_57]: (~s(X1_59, u2r3(X1_17)) | ~s(X1_59, X3_57) | equalish(X3_57, u2r3(X1_17)) | s2exact(X1_59) | ~s(X1_17, u2r1(X3_57, u2r3(X1_17), X1_59)) | ~s2exact(X1_17) | equalish(u2r1(X3_57, u2r3(X1_17), X1_59), u2r2(X1_17))))). % 3.33/1.79 tff(c_103, plain, (![X1_56, X2_55, X1_17]: (~s(X1_56, X2_55) | ~s(X1_56, u2r3(X1_17)) | equalish(u2r3(X1_17), X2_55) | s2exact(X1_56) | ~s(X1_17, u2r1(u2r3(X1_17), X2_55, X1_56)) | ~s2exact(X1_17) | equalish(u2r1(u2r3(X1_17), X2_55, X1_56), u2r2(X1_17))))). % 3.33/1.79 tff(c_115, plain, (![X1_59, X1_10, X3_57]: (~s(X1_59, u1r2(X1_10)) | ~s(X1_59, X3_57) | equalish(X3_57, u1r2(X1_10)) | s2exact(X1_59) | ~r(X1_10, u2r1(X3_57, u1r2(X1_10), X1_59)) | ~r1exact(X1_10)))). % 3.33/1.79 tff(c_104, plain, (![X1_56, X2_55, X1_10]: (~s(X1_56, X2_55) | ~s(X1_56, u1r2(X1_10)) | equalish(u1r2(X1_10), X2_55) | s2exact(X1_56) | ~r(X1_10, u2r1(u1r2(X1_10), X2_55, X1_56)) | ~r1exact(X1_10)))). % 3.33/1.79 tff(c_72, plain, (![X1_12, X1_48]: (~r(X1_12, u2r3(X1_48)) | r1exact(X1_12) | ~s(X1_48, u1r1(u2r3(X1_48), X1_12)) | ~s2exact(X1_48) | equalish(u1r1(u2r3(X1_48), X1_12), u2r2(X1_48))))). % 3.33/1.79 tff(c_36, plain, (![X1_27, X2_29, X3_28]: (~s(X1_27, X2_29) | ~s(X1_27, X3_28) | s(X1_27, u2r1(X3_28, X2_29, X1_27)) | equalish(X3_28, X2_29) | s2exact(X1_27)))). % 3.33/1.79 tff(c_32, plain, (![X3_22, X2_23, X1_21]: (~equalish(u2r1(X3_22, X2_23, X1_21), X2_23) | ~s(X1_21, X2_23) | ~s(X1_21, X3_22) | equalish(X3_22, X2_23) | s2exact(X1_21)))). % 3.33/1.79 tff(c_34, plain, (![X3_25, X2_26, X1_24]: (~equalish(u2r1(X3_25, X2_26, X1_24), X3_25) | ~s(X1_24, X2_26) | ~s(X1_24, X3_25) | equalish(X3_25, X2_26) | s2exact(X1_24)))). % 3.33/1.79 tff(c_65, plain, (![X1_45, X1_10]: (~r(X1_45, u1r2(X1_10)) | r1exact(X1_45) | ~r(X1_10, u1r1(u1r2(X1_10), X1_45)) | ~r1exact(X1_10)))). % 3.33/1.79 tff(c_12, plain, (![X1_7]: (~s2exact(X1_7) | ~r1exact(X1_7) | r(X1_7, u0r1(X1_7)) | s(X1_7, u0r1(X1_7)) | e(X1_7)))). % 3.33/1.79 tff(c_14, plain, (![X1_8]: (~s(X1_8, u0r1(X1_8)) | ~r(X1_8, u0r1(X1_8)) | ~s2exact(X1_8) | ~r1exact(X1_8) | e(X1_8)))). % 3.33/1.79 tff(c_24, plain, (![X1_17, X4_16]: (~s(X1_17, X4_16) | ~s2exact(X1_17) | equalish(X4_16, u2r2(X1_17)) | equalish(X4_16, u2r3(X1_17))))). % 3.33/1.79 tff(c_22, plain, (![X1_14, X2_15]: (~r(X1_14, X2_15) | r(X1_14, u1r1(X2_15, X1_14)) | r1exact(X1_14)))). % 3.33/1.79 tff(c_20, plain, (![X2_13, X1_12]: (~equalish(u1r1(X2_13, X1_12), X2_13) | ~r(X1_12, X2_13) | r1exact(X1_12)))). % 3.33/1.79 tff(c_51, plain, (![X1_19]: (~e(X1_19) | r(X1_19, u2r2(X1_19)) | ~s2exact(X1_19)))). % 3.33/1.79 tff(c_50, plain, (![X1_20]: (~e(X1_20) | r(X1_20, u2r3(X1_20)) | ~s2exact(X1_20)))). % 3.33/1.79 tff(c_16, plain, (![X1_10, X3_9]: (~r(X1_10, X3_9) | ~r1exact(X1_10) | equalish(X3_9, u1r2(X1_10))))). % 3.33/1.79 tff(c_4, plain, (![X1_1, X2_2]: (~r(X1_1, X2_2) | ~e(X1_1) | s(X1_1, X2_2)))). % 3.33/1.79 tff(c_6, plain, (![X1_3, X2_4]: (~s(X1_3, X2_4) | ~e(X1_3) | r(X1_3, X2_4)))). % 3.33/1.79 tff(c_26, plain, (![X1_18]: (~equalish(u2r3(X1_18), u2r2(X1_18)) | ~s2exact(X1_18)))). % 3.33/1.79 tff(c_30, plain, (![X1_20]: (~s2exact(X1_20) | s(X1_20, u2r3(X1_20))))). % 3.33/1.79 tff(c_18, plain, (![X1_11]: (~r1exact(X1_11) | r(X1_11, u1r2(X1_11))))). % 3.33/1.80 tff(c_28, plain, (![X1_19]: (~s2exact(X1_19) | s(X1_19, u2r2(X1_19))))). % 3.33/1.80 tff(c_8, plain, (![X1_5]: (~e(X1_5) | s2exact(X1_5)))). % 3.33/1.80 tff(c_10, plain, (![X1_6]: (~e(X1_6) | r1exact(X1_6)))). % 3.33/1.80 tff(c_2, plain, (e(exists))). % 3.33/1.80 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 3.33/1.80 %------------------------------------------------------------------------------