%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : KRS011-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 : n022.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 6.98s 2.58s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : KRS011-1 : TPTP v9.0.0. Released v2.0.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.12/0.34 % Computer : n022.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:06 EDT 2025 % 0.12/0.34 % CPUTime : % 6.98/2.58 % 6.98/2.58 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 6.98/2.58 % 6.98/2.58 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 6.98/2.58 %$ t3 > t2 > t1 > t > r3 > r2 > r1 > r > equalish > r2least > g > f3 > f2 > f1 > f > e > d > c > u9r3 > u9r2 > u9r1 > u11r3 > u11r2 > u11r1 > u10r3 > u10r2 > u10r1 > #nlpp > u9r5 > u9r4 > u14r2 > u14r1 > u11r5 > u11r4 > u10r5 > u10r4 > exists % 6.98/2.58 % 6.98/2.58 %Foreground sorts: % 6.98/2.58 % 6.98/2.58 % 6.98/2.58 %Background operators: % 6.98/2.58 % 6.98/2.58 % 6.98/2.58 %Foreground operators: % 6.98/2.58 tff(f2, type, f2: $i > $o). % 6.98/2.58 tff(u9r3, type, u9r3: ($i * $i) > $i). % 6.98/2.58 tff(u14r1, type, u14r1: $i > $i). % 6.98/2.58 tff(u11r4, type, u11r4: $i > $i). % 6.98/2.58 tff(d, type, d: $i > $o). % 6.98/2.58 tff(t3, type, t3: ($i * $i) > $o). % 6.98/2.58 tff(u9r2, type, u9r2: ($i * $i) > $i). % 6.98/2.58 tff(u9r1, type, u9r1: ($i * $i) > $i). % 6.98/2.58 tff(u10r4, type, u10r4: $i > $i). % 6.98/2.58 tff(u10r5, type, u10r5: $i > $i). % 6.98/2.58 tff(u14r2, type, u14r2: $i > $i). % 6.98/2.58 tff(u11r2, type, u11r2: ($i * $i) > $i). % 6.98/2.58 tff(u11r3, type, u11r3: ($i * $i) > $i). % 6.98/2.58 tff(u9r5, type, u9r5: $i > $i). % 6.98/2.58 tff(u9r4, type, u9r4: $i > $i). % 6.98/2.58 tff(r2, type, r2: ($i * $i) > $o). % 6.98/2.58 tff(u10r3, type, u10r3: ($i * $i) > $i). % 6.98/2.58 tff(f3, type, f3: $i > $o). % 6.98/2.58 tff(r1, type, r1: ($i * $i) > $o). % 6.98/2.58 tff(u10r2, type, u10r2: ($i * $i) > $i). % 6.98/2.58 tff(c, type, c: $i > $o). % 6.98/2.58 tff(e, type, e: $i > $o). % 6.98/2.58 tff(exists, type, exists: $i). % 6.98/2.58 tff(t, type, t: ($i * $i) > $o). % 6.98/2.58 tff(equalish, type, equalish: ($i * $i) > $o). % 6.98/2.58 tff(u11r5, type, u11r5: $i > $i). % 6.98/2.58 tff(t2, type, t2: ($i * $i) > $o). % 6.98/2.58 tff(u11r1, type, u11r1: ($i * $i) > $i). % 6.98/2.58 tff(u10r1, type, u10r1: ($i * $i) > $i). % 6.98/2.58 tff(g, type, g: $i > $o). % 6.98/2.58 tff(t1, type, t1: ($i * $i) > $o). % 6.98/2.58 tff(r, type, r: ($i * $i) > $o). % 6.98/2.58 tff(f, type, f: $i > $o). % 6.98/2.58 tff(f1, type, f1: $i > $o). % 6.98/2.58 tff(r3, type, r3: ($i * $i) > $o). % 6.98/2.58 tff(r2least, type, r2least: $i > $o). % 6.98/2.58 % 6.98/2.58 %Saturated clause set: % 6.98/2.59 tff(c_1681, plain, (![X1_45, X1_174]: (~d(u10r5(X1_45)) | ~r2(X1_174, u10r4(X1_45)) | f2(X1_174) | ~f2(X1_45)))). % 6.98/2.59 tff(c_1646, plain, (![X1_20, X1_171]: (~c(u9r5(X1_20)) | ~r1(X1_171, u9r4(X1_20)) | f1(X1_171) | ~f1(X1_20)))). % 6.98/2.59 tff(c_1621, plain, (![X1_70, X1_177]: (~e(u11r5(X1_70)) | ~r3(X1_177, u11r4(X1_70)) | f3(X1_177) | ~f3(X1_70)))). % 6.98/2.59 tff(c_416, plain, (![X1_139]: (equalish(u10r5(X1_139), u10r5(X1_139)) | ~f2(X1_139)))). % 6.98/2.59 tff(c_402, plain, (![X1_142]: (equalish(u11r5(X1_142), u11r5(X1_142)) | ~f3(X1_142)))). % 6.98/2.59 tff(c_291, plain, (![X1_139, X4_223, X5_224]: (~t(u10r4(X1_139), X4_223) | ~t(u10r4(X1_139), X5_224) | equalish(X4_223, u10r5(X1_139)) | equalish(X5_224, u10r5(X1_139)) | equalish(X5_224, X4_223) | ~f2(X1_139)))). % 6.98/2.59 tff(c_331, plain, (![X1_142, X4_247, X5_248]: (~t(u11r4(X1_142), X4_247) | ~t(u11r4(X1_142), X5_248) | equalish(X4_247, u11r5(X1_142)) | equalish(X5_248, u11r5(X1_142)) | equalish(X5_248, X4_247) | ~f3(X1_142)))). % 6.98/2.59 tff(c_362, plain, (![X1_141]: (equalish(u9r5(X1_141), u9r5(X1_141)) | ~f1(X1_141)))). % 6.98/2.59 tff(c_310, plain, (![X1_141, X4_233, X5_234]: (~t(u9r4(X1_141), X4_233) | ~t(u9r4(X1_141), X5_234) | equalish(X4_233, u9r5(X1_141)) | equalish(X5_234, u9r5(X1_141)) | equalish(X5_234, X4_233) | ~f1(X1_141)))). % 6.98/2.59 tff(c_74, plain, (![X1_74, X3_73, X4_72, X5_71]: (~t(u11r4(X1_74), X3_73) | ~t(u11r4(X1_74), X4_72) | ~t(u11r4(X1_74), X5_71) | ~f3(X1_74) | equalish(X4_72, X3_73) | equalish(X5_71, X3_73) | equalish(X5_71, X4_72)))). % 6.98/2.59 tff(c_34, plain, (![X1_24, X3_23, X4_22, X5_21]: (~t(u9r4(X1_24), X3_23) | ~t(u9r4(X1_24), X4_22) | ~t(u9r4(X1_24), X5_21) | ~f1(X1_24) | equalish(X4_22, X3_23) | equalish(X5_21, X3_23) | equalish(X5_21, X4_22)))). % 6.98/2.59 tff(c_54, plain, (![X1_49, X3_48, X4_47, X5_46]: (~t(u10r4(X1_49), X3_48) | ~t(u10r4(X1_49), X4_47) | ~t(u10r4(X1_49), X5_46) | ~f2(X1_49) | equalish(X4_47, X3_48) | equalish(X5_46, X3_48) | equalish(X5_46, X4_47)))). % 6.98/2.59 tff(c_42, plain, (![X6_34, X2_33, X1_32]: (~c(X6_34) | ~t1(X2_33, X6_34) | ~equalish(u9r3(X2_33, X1_32), u9r2(X2_33, X1_32)) | ~r1(X1_32, X2_33) | f1(X1_32)))). % 6.98/2.59 tff(c_62, plain, (![X6_59, X2_58, X1_57]: (~d(X6_59) | ~t2(X2_58, X6_59) | ~equalish(u10r3(X2_58, X1_57), u10r2(X2_58, X1_57)) | ~r2(X1_57, X2_58) | f2(X1_57)))). % 6.98/2.59 tff(c_78, plain, (![X6_78, X2_77, X1_76]: (~e(X6_78) | ~t3(X2_77, X6_78) | ~equalish(u11r2(X2_77, X1_76), u11r1(X2_77, X1_76)) | ~r3(X1_76, X2_77) | f3(X1_76)))). % 6.98/2.59 tff(c_82, plain, (![X6_84, X2_83, X1_82]: (~e(X6_84) | ~t3(X2_83, X6_84) | ~equalish(u11r3(X2_83, X1_82), u11r2(X2_83, X1_82)) | ~r3(X1_82, X2_83) | f3(X1_82)))). % 6.98/2.59 tff(c_58, plain, (![X6_53, X2_52, X1_51]: (~d(X6_53) | ~t2(X2_52, X6_53) | ~equalish(u10r2(X2_52, X1_51), u10r1(X2_52, X1_51)) | ~r2(X1_51, X2_52) | f2(X1_51)))). % 6.98/2.59 tff(c_80, plain, (![X6_81, X2_80, X1_79]: (~e(X6_81) | ~t3(X2_80, X6_81) | ~equalish(u11r3(X2_80, X1_79), u11r1(X2_80, X1_79)) | ~r3(X1_79, X2_80) | f3(X1_79)))). % 6.98/2.59 tff(c_40, plain, (![X6_31, X2_30, X1_29]: (~c(X6_31) | ~t1(X2_30, X6_31) | ~equalish(u9r3(X2_30, X1_29), u9r1(X2_30, X1_29)) | ~r1(X1_29, X2_30) | f1(X1_29)))). % 6.98/2.59 tff(c_38, plain, (![X6_28, X2_27, X1_26]: (~c(X6_28) | ~t1(X2_27, X6_28) | ~equalish(u9r2(X2_27, X1_26), u9r1(X2_27, X1_26)) | ~r1(X1_26, X2_27) | f1(X1_26)))). % 6.98/2.59 tff(c_60, plain, (![X6_56, X2_55, X1_54]: (~d(X6_56) | ~t2(X2_55, X6_56) | ~equalish(u10r3(X2_55, X1_54), u10r1(X2_55, X1_54)) | ~r2(X1_54, X2_55) | f2(X1_54)))). % 6.98/2.59 tff(c_84, plain, (![X6_87, X2_86, X1_85]: (~e(X6_87) | ~t3(X2_86, X6_87) | ~r3(X1_85, X2_86) | t(X2_86, u11r1(X2_86, X1_85)) | f3(X1_85)))). % 6.98/2.59 tff(c_44, plain, (![X6_37, X2_36, X1_35]: (~c(X6_37) | ~t1(X2_36, X6_37) | ~r1(X1_35, X2_36) | t(X2_36, u9r1(X2_36, X1_35)) | f1(X1_35)))). % 6.98/2.59 tff(c_86, plain, (![X6_90, X2_89, X1_88]: (~e(X6_90) | ~t3(X2_89, X6_90) | ~r3(X1_88, X2_89) | t(X2_89, u11r2(X2_89, X1_88)) | f3(X1_88)))). % 6.98/2.59 tff(c_66, plain, (![X6_65, X2_64, X1_63]: (~d(X6_65) | ~t2(X2_64, X6_65) | ~r2(X1_63, X2_64) | t(X2_64, u10r2(X2_64, X1_63)) | f2(X1_63)))). % 6.98/2.60 tff(c_48, plain, (![X6_43, X2_42, X1_41]: (~c(X6_43) | ~t1(X2_42, X6_43) | ~r1(X1_41, X2_42) | t(X2_42, u9r3(X2_42, X1_41)) | f1(X1_41)))). % 6.98/2.60 tff(c_68, plain, (![X6_68, X2_67, X1_66]: (~d(X6_68) | ~t2(X2_67, X6_68) | ~r2(X1_66, X2_67) | t(X2_67, u10r3(X2_67, X1_66)) | f2(X1_66)))). % 6.98/2.60 tff(c_88, plain, (![X6_93, X2_92, X1_91]: (~e(X6_93) | ~t3(X2_92, X6_93) | ~r3(X1_91, X2_92) | t(X2_92, u11r3(X2_92, X1_91)) | f3(X1_91)))). % 6.98/2.60 tff(c_46, plain, (![X6_40, X2_39, X1_38]: (~c(X6_40) | ~t1(X2_39, X6_40) | ~r1(X1_38, X2_39) | t(X2_39, u9r2(X2_39, X1_38)) | f1(X1_38)))). % 6.98/2.60 tff(c_201, plain, (![X1_75, X3_150]: (~r(X1_75, X3_150) | equalish(X3_150, u11r4(X1_75)) | r2least(X1_75) | ~f3(X1_75)))). % 6.98/2.60 tff(c_202, plain, (![X1_25, X3_150]: (~r(X1_25, X3_150) | equalish(X3_150, u9r4(X1_25)) | r2least(X1_25) | ~f1(X1_25)))). % 6.98/2.60 tff(c_200, plain, (![X1_136, X3_150]: (~r(X1_136, X3_150) | equalish(X3_150, u10r4(X1_136)) | r2least(X1_136) | ~f2(X1_136)))). % 6.98/2.60 tff(c_64, plain, (![X6_62, X2_61, X1_60]: (~d(X6_62) | ~t2(X2_61, X6_62) | ~r2(X1_60, X2_61) | t(X2_61, u10r1(X2_61, X1_60)) | f2(X1_60)))). % 6.98/2.60 tff(c_108, plain, (![X1_103, X2_105, X3_104]: (~r(X1_103, X2_105) | ~r(X1_103, X3_104) | equalish(X3_104, X2_105) | r2least(X1_103)))). % 6.98/2.60 tff(c_168, plain, (![X1_139]: (t(u10r4(X1_139), u10r5(X1_139)) | ~f2(X1_139)))). % 6.98/2.60 tff(c_179, plain, (![X1_142]: (t(u11r4(X1_142), u11r5(X1_142)) | ~f3(X1_142)))). % 6.98/2.60 tff(c_96, plain, (![X1_97]: (~f3(X1_97) | ~f2(X1_97) | ~f1(X1_97) | f(X1_97)))). % 6.98/2.60 tff(c_174, plain, (![X1_141]: (t(u9r4(X1_141), u9r5(X1_141)) | ~f1(X1_141)))). % 6.98/2.60 tff(c_102, plain, (![X1_100]: (~equalish(u14r2(X1_100), u14r1(X1_100)) | ~r2least(X1_100)))). % 6.98/2.60 tff(c_72, plain, (![X1_70]: (~f3(X1_70) | t3(u11r4(X1_70), u11r5(X1_70))))). % 6.98/2.60 tff(c_32, plain, (![X1_20]: (~f1(X1_20) | t1(u9r4(X1_20), u9r5(X1_20))))). % 6.98/2.60 tff(c_161, plain, (![X1_136]: (r(X1_136, u10r4(X1_136)) | ~f2(X1_136)))). % 6.98/2.60 tff(c_52, plain, (![X1_45]: (~f2(X1_45) | t2(u10r4(X1_45), u10r5(X1_45))))). % 6.98/2.60 tff(c_149, plain, (![X1_75]: (r(X1_75, u11r4(X1_75)) | ~f3(X1_75)))). % 6.98/2.60 tff(c_155, plain, (![X1_25]: (r(X1_25, u9r4(X1_25)) | ~f1(X1_25)))). % 6.98/2.60 tff(c_56, plain, (![X1_50]: (~f2(X1_50) | r2(X1_50, u10r4(X1_50))))). % 6.98/2.60 tff(c_104, plain, (![X1_101]: (~r2least(X1_101) | r(X1_101, u14r1(X1_101))))). % 6.98/2.60 tff(c_6, plain, (![X1_1, X2_2]: (~r1(X1_1, X2_2) | r(X1_1, X2_2)))). % 6.98/2.60 tff(c_8, plain, (![X1_3, X2_4]: (~r2(X1_3, X2_4) | r(X1_3, X2_4)))). % 6.98/2.60 tff(c_10, plain, (![X1_5, X2_6]: (~r3(X1_5, X2_6) | r(X1_5, X2_6)))). % 6.98/2.60 tff(c_36, plain, (![X1_25]: (~f1(X1_25) | r1(X1_25, u9r4(X1_25))))). % 6.98/2.60 tff(c_106, plain, (![X1_102]: (~r2least(X1_102) | r(X1_102, u14r2(X1_102))))). % 6.98/2.60 tff(c_16, plain, (![X1_11, X2_12]: (~t3(X1_11, X2_12) | t(X1_11, X2_12)))). % 6.98/2.60 tff(c_14, plain, (![X1_9, X2_10]: (~t2(X1_9, X2_10) | t(X1_9, X2_10)))). % 6.98/2.60 tff(c_12, plain, (![X1_7, X2_8]: (~t1(X1_7, X2_8) | t(X1_7, X2_8)))). % 6.98/2.60 tff(c_135, plain, (![X1_116]: (~c(u10r5(X1_116)) | ~f2(X1_116)))). % 6.98/2.60 tff(c_76, plain, (![X1_75]: (~f3(X1_75) | r3(X1_75, u11r4(X1_75))))). % 6.98/2.60 tff(c_129, plain, (![X1_114]: (~c(u11r5(X1_114)) | ~f3(X1_114)))). % 6.98/2.60 tff(c_128, plain, (![X1_114]: (~d(u11r5(X1_114)) | ~f3(X1_114)))). % 6.98/2.60 tff(c_50, plain, (![X1_44]: (~f2(X1_44) | d(u10r5(X1_44))))). % 6.98/2.60 tff(c_30, plain, (![X1_19]: (~f1(X1_19) | c(u9r5(X1_19))))). % 6.98/2.60 tff(c_70, plain, (![X1_69]: (~f3(X1_69) | e(u11r5(X1_69))))). % 6.98/2.60 tff(c_26, plain, (![X1_17]: (~d(X1_17) | ~e(X1_17)))). % 6.98/2.60 tff(c_24, plain, (![X1_16]: (~c(X1_16) | ~d(X1_16)))). % 6.98/2.60 tff(c_100, plain, (![X1_99]: (~r2least(X1_99) | g(X1_99)))). % 6.98/2.60 tff(c_98, plain, (![X1_98]: (~g(X1_98) | r2least(X1_98)))). % 6.98/2.60 tff(c_28, plain, (![X1_18]: (~c(X1_18) | ~e(X1_18)))). % 6.98/2.60 tff(c_90, plain, (![X1_94]: (~f(X1_94) | f3(X1_94)))). % 6.98/2.60 tff(c_92, plain, (![X1_95]: (~f(X1_95) | f2(X1_95)))). % 6.98/2.60 tff(c_94, plain, (![X1_96]: (~f(X1_96) | f1(X1_96)))). % 6.98/2.60 tff(c_2, plain, (f(exists))). % 6.98/2.60 tff(c_4, plain, (~g(exists))). % 6.98/2.60 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 6.98/2.60 %------------------------------------------------------------------------------