%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SYO641-10 : TPTP v9.0.0. Released v7.5.0. % Transfm : none % Format : tptp:raw % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % Computer : n019.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 10:38:01 PM UTC 2025 % Result : Satisfiable 3.17s 2.22s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.09 % Problem : SYO641-10 : TPTP v9.0.0. Released v7.5.0. % 0.00/0.09 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % 0.08/0.29 % Computer : n019.cluster.edu % 0.08/0.29 % Model : x86_64 x86_64 % 0.08/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.29 % Memory : 8042.1875MB % 0.08/0.29 % OS : Linux 3.10.0-693.el7.x86_64 % 0.08/0.30 % CPULimit : 300 % 0.08/0.30 % WCLimit : 300 % 0.08/0.30 % DateTime : Wed Apr 9 09:39:32 EDT 2025 % 0.08/0.30 % CPUTime : % 3.17/2.22 % 3.17/2.22 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 3.17/2.22 % 3.17/2.22 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 3.17/2.25 %$ ifeq > tuple > f > #nlpp > sK1_notref3_Y1 > true > sK3_notref3_Y2 > sK2_notref3_Y3 % 3.17/2.25 % 3.17/2.25 %Foreground sorts: % 3.17/2.25 % 3.17/2.25 % 3.17/2.25 %Background operators: % 3.17/2.25 % 3.17/2.25 % 3.17/2.25 %Foreground operators: % 3.17/2.25 tff(tuple, type, tuple: ($i * $i * $i) > $i). % 3.17/2.25 tff(sK2_notref3_Y3, type, sK2_notref3_Y3: $i). % 3.17/2.25 tff(sK1_notref3_Y1, type, sK1_notref3_Y1: $i > $i). % 3.17/2.25 tff(sK3_notref3_Y2, type, sK3_notref3_Y2: $i). % 3.17/2.25 tff(true, type, true: $i). % 3.17/2.25 tff(ifeq, type, ifeq: ($i * $i * $i * $i) > $i). % 3.17/2.25 tff(f, type, f: ($i * $i * $i) > $i). % 3.17/2.25 % 3.17/2.25 %Saturated clause set: % 3.17/2.25 tff(c_59, plain, (![X4_22, X8_23, X6_25, X9_20]: (tuple(true, f(X4_22, sK2_notref3_Y3, X8_23), f(sK1_notref3_Y1(sK3_notref3_Y2), X6_25, X9_20))!=tuple(true, true, true)))). % 3.17/2.25 tff(c_62, plain, (![X5_21, X10_24, X6_25, X9_20]: (tuple(f(sK1_notref3_Y1(sK3_notref3_Y2), X5_21, X10_24), true, f(X5_21, X6_25, X9_20))!=tuple(true, true, true)))). % 3.17/2.25 tff(c_104, plain, (![X10_47]: (tuple(f(sK1_notref3_Y1(sK3_notref3_Y2), sK2_notref3_Y3, X10_47), true, true)!=tuple(true, true, true)))). % 3.17/2.25 tff(c_65, plain, (![X2_26, X10_24, X4_22, X8_23]: (tuple(f(X2_26, sK2_notref3_Y3, X10_24), f(X4_22, X2_26, X8_23), true)!=tuple(true, true, true)))). % 3.17/2.26 tff(c_99, plain, (![X4_40, X8_41]: (tuple(true, f(X4_40, sK3_notref3_Y2, X8_41), true)!=tuple(true, true, true)))). % 3.17/2.26 tff(c_68, plain, (![X4_22, X8_23, X6_25, X9_20]: (tuple(true, f(X4_22, sK3_notref3_Y2, X8_23), f(sK2_notref3_Y3, X6_25, X9_20))!=tuple(true, true, true)))). % 3.17/2.26 tff(c_79, plain, (![X10_28]: (tuple(f(sK1_notref3_Y1(sK3_notref3_Y2), sK3_notref3_Y2, X10_28), true, true)!=tuple(true, true, true)))). % 3.17/2.26 tff(c_87, plain, (![X6_34, X9_35]: (tuple(true, true, f(sK1_notref3_Y1(sK3_notref3_Y2), X6_34, X9_35))!=tuple(true, true, true)))). % 3.17/2.26 tff(c_90, plain, (![X10_33]: (tuple(f(sK2_notref3_Y3, sK2_notref3_Y3, X10_33), true, true)!=tuple(true, true, true)))). % 3.17/2.26 tff(c_71, plain, (![X5_21, X10_24, X6_25, X9_20]: (tuple(f(sK2_notref3_Y3, X5_21, X10_24), true, f(X5_21, X6_25, X9_20))!=tuple(true, true, true)))). % 3.17/2.26 tff(c_82, plain, (![X10_28]: (tuple(f(sK2_notref3_Y3, sK3_notref3_Y2, X10_28), true, true)!=tuple(true, true, true)))). % 3.17/2.26 tff(c_74, plain, (![X2_26, X10_24, X4_22, X8_23]: (tuple(f(X2_26, sK3_notref3_Y2, X10_24), f(X4_22, X2_26, X8_23), true)!=tuple(true, true, true)))). % 3.17/2.26 tff(c_4, plain, (![X2_7, X9_6, X6_5, X10_10, X8_8, X4_9, X5_4]: (tuple(f(X2_7, X5_4, X10_10), f(X4_9, X2_7, X8_8), f(X5_4, X6_5, X9_6))!=tuple(true, true, true)))). % 3.17/2.26 tff(c_39, plain, (f(sK2_notref3_Y3, sK1_notref3_Y1(sK3_notref3_Y2), sK1_notref3_Y1(sK3_notref3_Y2))=true)). % 3.17/2.26 tff(c_6, plain, (![X1_11, X3_12]: (ifeq(f(X1_11, X3_12, sK1_notref3_Y1(X1_11)), true, f(X3_12, sK1_notref3_Y1(X1_11), sK1_notref3_Y1(X1_11)), true)=true))). % 3.17/2.26 tff(c_2, plain, (![A_1, B_2, C_3]: (ifeq(A_1, A_1, B_2, C_3)=B_2))). % 3.17/2.26 tff(c_8, plain, (![X7_13]: (f(sK3_notref3_Y2, sK2_notref3_Y3, X7_13)=true))). % 3.17/2.26 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 3.17/2.26 %------------------------------------------------------------------------------