%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : KRS003_10 : TPTP v9.0.0. Released v8.2.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:08 PM UTC 2025 % Result : Satisfiable 3.00s 1.75s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : KRS003_10 : TPTP v9.0.0. Released v8.2.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:52:10 EDT 2025 % 0.12/0.34 % CPUTime : % 3.00/1.75 % 3.00/1.75 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 3.00/1.75 % 3.00/1.75 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 3.00/1.76 %$ s > equalish > s2least > s1most > f > e > d > c > #nlpp > u3r2 > u3r1 > u1r2 > u1r1 > exist % 3.00/1.76 % 3.00/1.76 %Foreground sorts: % 3.00/1.76 tff(real, type, real: $tType ). % 3.00/1.76 tff(unreal, type, unreal: $tType ). % 3.00/1.76 % 3.00/1.76 %Background operators: % 3.00/1.76 % 3.00/1.76 % 3.00/1.76 %Foreground operators: % 3.00/1.76 tff(u3r2, type, u3r2: unreal > real). % 3.00/1.76 tff(e, type, e: unreal > $o). % 3.00/1.76 tff(u3r1, type, u3r1: unreal > real). % 3.00/1.76 tff(equalish, type, equalish: (real * real) > $o). % 3.00/1.76 tff(exist, type, exist: unreal). % 3.00/1.76 tff(c, type, c: unreal > $o). % 3.00/1.76 tff(u1r2, type, u1r2: unreal > real). % 3.00/1.76 tff(s, type, s: (unreal * real) > $o). % 3.00/1.76 tff(s2least, type, s2least: unreal > $o). % 3.00/1.76 tff(d, type, d: unreal > $o). % 3.00/1.76 tff(s1most, type, s1most: unreal > $o). % 3.00/1.76 tff(u1r1, type, u1r1: unreal > real). % 3.00/1.76 tff(f, type, f: unreal > $o). % 3.00/1.76 % 3.00/1.76 %Saturated clause set: % 3.00/1.76 tff(c_126, plain, (![X1_49:unreal]: (d(X1_49) | c(X1_49)))). % 3.00/1.76 tff(c_117, plain, (![X1_48:unreal]: (c(X1_48) | s1most(X1_48)))). % 3.00/1.76 tff(c_108, plain, (![X1_16:unreal]: (s2least(X1_16) | s1most(X1_16)))). % 3.00/1.76 tff(c_96, plain, (![X1_9:unreal]: (~c(X1_9) | ~d(X1_9)))). % 3.00/1.76 tff(c_91, plain, (![X1_1:unreal]: (~s1most(X1_1) | ~c(X1_1)))). % 3.00/1.76 tff(c_86, plain, (![X1_5:unreal]: (~s1most(X1_5) | ~s2least(X1_5)))). % 3.00/1.76 tff(c_12, plain, (![X3_7:real, X2_6:real, X1_8:unreal]: (equalish(X3_7, X2_6) | s2least(X1_8) | ~s(X1_8, X2_6) | ~s(X1_8, X3_7)))). % 3.00/1.76 tff(c_18, plain, (![X3_12:real, X2_11:real, X1_13:unreal]: (equalish(X3_12, X2_11) | ~s(X1_13, X2_11) | ~s(X1_13, X3_12) | ~s1most(X1_13)))). % 3.00/1.76 tff(c_6, plain, (![X1_3:unreal]: (~equalish(u1r2(X1_3), u1r1(X1_3)) | ~s2least(X1_3)))). % 3.00/1.76 tff(c_20, plain, (![X1_14:unreal]: (s1most(X1_14) | ~equalish(u3r2(X1_14), u3r1(X1_14))))). % 3.00/1.76 tff(c_10, plain, (![X1_5:unreal]: (s(X1_5, u1r2(X1_5)) | ~s2least(X1_5)))). % 3.00/1.76 tff(c_22, plain, (![X1_15:unreal]: (s(X1_15, u3r1(X1_15)) | s1most(X1_15)))). % 3.00/1.76 tff(c_8, plain, (![X1_4:unreal]: (s(X1_4, u1r1(X1_4)) | ~s2least(X1_4)))). % 3.00/1.76 tff(c_24, plain, (![X1_16:unreal]: (s(X1_16, u3r2(X1_16)) | s1most(X1_16)))). % 3.00/1.76 tff(c_2, plain, (![X1_1:unreal]: (s2least(X1_1) | ~c(X1_1)))). % 3.18/1.76 tff(c_4, plain, (![X1_2:unreal]: (c(X1_2) | ~s2least(X1_2)))). % 3.18/1.76 tff(c_16, plain, (![X1_10:unreal]: (d(X1_10) | ~s1most(X1_10)))). % 3.18/1.76 tff(c_14, plain, (![X1_9:unreal]: (s1most(X1_9) | ~d(X1_9)))). % 3.18/1.77 tff(c_26, plain, (![X1_17:unreal]: (c(X1_17) | ~e(X1_17)))). % 3.18/1.77 tff(c_28, plain, (![X1_18:unreal]: (d(X1_18) | ~f(X1_18)))). % 3.18/1.77 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 3.18/1.77 %------------------------------------------------------------------------------