%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : LCL645-10.001 : TPTP v9.3.1. Released v7.3.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 : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Mon Sep 7 11:12:17 AM UTC 2026 % Result : Satisfiable 2.19s 1.32s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LCL645-10.001 : TPTP v9.3.1. Released v7.3.0. % 0.00/0.04 % 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.11/0.37 % Computer : n017.cluster.edu % 0.11/0.37 % Model : x86_64 x86_64 % 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.37 % Memory : 8046.5625MB % 0.11/0.37 % OS : Linux 6.8.0-71-generic % 0.11/0.37 % CPULimit : 300 % 0.11/0.37 % WCLimit : 300 % 0.11/0.37 % DateTime : Sat Sep 5 13:27:21 UTC 2026 % 0.11/0.38 % CPUTime : % 2.19/1.32 % 2.19/1.32 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 2.19/1.32 % 2.19/1.32 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 2.19/1.33 %$ ifeq2 > ifeq > r1 > #nlpp > p1 > true > sK3_main_X > sK2_main_Y > sK1_main_Y > b > a % 2.19/1.33 % 2.19/1.33 %Foreground sorts: % 2.19/1.33 % 2.19/1.33 % 2.19/1.33 %Background operators: % 2.19/1.33 % 2.19/1.33 % 2.19/1.33 %Foreground operators: % 2.19/1.33 tff(r1, type, r1: ($i * $i) > $i). % 2.19/1.33 tff(a, type, a: $i). % 2.19/1.33 tff(p1, type, p1: $i > $i). % 2.19/1.33 tff(ifeq2, type, ifeq2: ($i * $i * $i * $i) > $i). % 2.19/1.33 tff(b, type, b: $i). % 2.19/1.33 tff(sK1_main_Y, type, sK1_main_Y: $i). % 2.19/1.33 tff(sK3_main_X, type, sK3_main_X: $i). % 2.19/1.33 tff(true, type, true: $i). % 2.19/1.33 tff(sK2_main_Y, type, sK2_main_Y: $i). % 2.19/1.33 tff(ifeq, type, ifeq: ($i * $i * $i * $i) > $i). % 2.19/1.33 % 2.19/1.33 %Saturated clause set: % 2.19/1.33 tff(c_12, plain, (![X_8]: (ifeq2(r1(sK1_main_Y, X_8), true, p1(X_8), true)=true))). % 2.19/1.33 tff(c_10, plain, (![X_7]: (ifeq2(r1(sK2_main_Y, X_7), true, p1(X_7), true)=true))). % 2.19/1.33 tff(c_14, plain, (ifeq(p1(sK2_main_Y), true, a, b)=b)). % 2.19/1.33 tff(c_16, plain, (ifeq(p1(sK1_main_Y), true, a, b)=b)). % 2.19/1.33 tff(c_2, plain, (![A_1, B_2, C_3]: (ifeq2(A_1, A_1, B_2, C_3)=B_2))). % 2.19/1.33 tff(c_4, plain, (![A_4, B_5, C_6]: (ifeq(A_4, A_4, B_5, C_6)=B_5))). % 2.19/1.33 tff(c_6, plain, (r1(sK3_main_X, sK2_main_Y)=true)). % 2.19/1.33 tff(c_8, plain, (r1(sK3_main_X, sK1_main_Y)=true)). % 2.19/1.33 tff(c_18, plain, (b!=a)). % 2.19/1.33 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 2.19/1.33 %------------------------------------------------------------------------------