%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : PUZ054-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 : n011.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 08:25:10 PM UTC 2025 % Result : Satisfiable 6.78s 2.87s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : PUZ054-10 : TPTP v9.0.0. Released v7.5.0. % 0.11/0.13 % 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.12/0.34 % Computer : n011.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 17:16:18 EDT 2025 % 0.12/0.34 % CPUTime : % 6.78/2.87 % 6.78/2.87 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 6.78/2.87 % 6.78/2.87 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 6.78/2.89 %$ ifeq > p > #nlpp > s > true > n0 % 6.78/2.89 % 6.78/2.89 %Foreground sorts: % 6.78/2.89 % 6.78/2.89 % 6.78/2.89 %Background operators: % 6.78/2.89 % 6.78/2.89 % 6.78/2.89 %Foreground operators: % 6.78/2.89 tff(p, type, p: ($i * $i) > $i). % 6.78/2.89 tff(s, type, s: $i > $i). % 6.78/2.89 tff(n0, type, n0: $i). % 6.78/2.89 tff(true, type, true: $i). % 6.78/2.89 tff(ifeq, type, ifeq: ($i * $i * $i * $i) > $i). % 6.78/2.89 % 6.78/2.89 %Saturated clause set: % 6.78/2.90 tff(c_1713, plain, (ifeq(p(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))), s(s(s(s(s(n0)))))), true, true, true)=true)). % 6.78/2.90 tff(c_2496, plain, (ifeq(p(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))), s(s(s(s(n0))))), true, true, true)=true)). % 6.78/2.90 tff(c_2620, plain, (ifeq(p(s(s(n0)), s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))))), true, true, true)=true)). % 6.78/2.90 tff(c_2800, plain, (ifeq(p(n0, s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))), true, true, true)=true)). % 6.78/2.90 tff(c_2536, plain, (ifeq(p(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))), s(s(s(n0)))), true, true, true)=true)). % 6.78/2.90 tff(c_1785, plain, (ifeq(p(s(s(s(s(n0)))), s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))), true, true, true)=true)). % 6.78/2.90 tff(c_2576, plain, (ifeq(p(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))), s(s(n0))), true, true, true)=true)). % 6.78/2.90 tff(c_2843, plain, (p(s(s(n0)), s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))=true)). % 6.78/2.90 tff(c_2812, plain, (p(n0, s(s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))))=true)). % 6.78/2.90 tff(c_2785, plain, (p(n0, s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))=true)). % 6.78/2.90 tff(c_2652, plain, (ifeq(p(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))), s(n0)), true, true, true)=true)). % 6.78/2.90 tff(c_2689, plain, (ifeq(p(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))), n0), true, true, true)=true)). % 6.78/2.90 tff(c_2710, plain, (p(s(s(s(s(n0)))), s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))=true)). % 6.78/2.90 tff(c_2716, plain, (p(s(s(s(s(s(s(s(s(s(s(n0)))))))))), n0)=true)). % 6.78/2.90 tff(c_2669, plain, (p(s(s(s(s(s(s(s(s(s(s(n0)))))))))), s(n0))=true)). % 6.78/2.90 tff(c_2629, plain, (p(s(s(s(s(s(s(s(s(s(s(n0)))))))))), s(s(n0)))=true)). % 6.78/2.90 tff(c_2592, plain, (p(s(s(n0)), s(s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))))=true)). % 6.78/2.90 tff(c_2553, plain, (p(s(s(s(s(s(s(s(s(s(s(n0)))))))))), s(s(s(n0))))=true)). % 6.78/2.90 tff(c_2513, plain, (p(s(s(s(s(s(s(s(s(s(s(n0)))))))))), s(s(s(s(n0)))))=true)). % 6.78/2.90 tff(c_2475, plain, (p(s(s(s(s(s(s(s(s(s(s(n0)))))))))), s(s(s(s(s(n0))))))=true)). % 6.78/2.90 tff(c_2435, plain, (p(n0, s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))=true)). % 6.78/2.90 tff(c_2395, plain, (p(s(s(n0)), s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))=true)). % 6.78/2.90 tff(c_1325, plain, (ifeq(p(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))), s(s(s(s(s(s(n0))))))), true, true, true)=true)). % 6.78/2.90 tff(c_2351, plain, (p(s(s(s(s(n0)))), s(s(s(s(s(s(s(s(s(s(n0)))))))))))=true)). % 6.78/2.90 tff(c_2311, plain, (p(s(s(s(s(s(s(n0)))))), s(s(s(s(s(s(s(s(s(n0))))))))))=true)). % 6.78/2.90 tff(c_2259, plain, (p(n0, s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))=true)). % 6.78/2.90 tff(c_2218, plain, (p(s(s(n0)), s(s(s(s(s(s(s(s(s(s(n0)))))))))))=true)). % 6.78/2.90 tff(c_2178, plain, (p(s(s(s(s(n0)))), s(s(s(s(s(s(s(s(s(n0))))))))))=true)). % 6.78/2.90 tff(c_2140, plain, (p(s(s(s(s(s(s(n0)))))), s(s(s(s(s(s(s(s(n0)))))))))=true)). % 6.78/2.90 tff(c_1142, plain, (ifeq(p(s(s(s(s(s(s(n0)))))), s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))), true, true, true)=true)). % 7.16/2.90 tff(c_2084, plain, (p(n0, s(s(s(s(s(s(s(s(s(s(n0)))))))))))=true)). % 7.16/2.90 tff(c_2044, plain, (p(s(s(n0)), s(s(s(s(s(s(s(s(s(n0))))))))))=true)). % 7.16/2.91 tff(c_2004, plain, (p(s(s(s(s(n0)))), s(s(s(s(s(s(s(s(n0)))))))))=true)). % 7.16/2.91 tff(c_1965, plain, (p(s(s(s(s(s(s(n0)))))), s(s(s(s(s(s(s(n0))))))))=true)). % 7.16/2.91 tff(c_1914, plain, (p(n0, s(s(s(s(s(s(s(s(s(n0))))))))))=true)). % 7.16/2.91 tff(c_1874, plain, (p(s(s(n0)), s(s(s(s(s(s(s(s(n0)))))))))=true)). % 7.16/2.91 tff(c_1833, plain, (p(s(s(s(s(n0)))), s(s(s(s(s(s(s(n0))))))))=true)). % 7.16/2.91 tff(c_1795, plain, (p(s(s(s(s(s(s(n0)))))), s(s(s(s(s(s(n0)))))))=true)). % 7.16/2.91 tff(c_1730, plain, (p(s(s(s(s(n0)))), s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))=true)). % 7.16/2.91 tff(c_1680, plain, (p(s(s(s(s(s(s(n0)))))), s(s(s(s(s(s(s(s(s(s(n0)))))))))))=true)). % 7.16/2.91 tff(c_1509, plain, (p(s(s(s(s(s(s(s(s(s(s(n0)))))))))), s(s(s(s(s(s(n0)))))))=true)). % 7.16/2.91 tff(c_1642, plain, (p(n0, s(s(s(s(s(s(s(s(n0)))))))))=true)). % 7.16/2.91 tff(c_1602, plain, (p(s(s(n0)), s(s(s(s(s(s(s(n0))))))))=true)). % 7.16/2.91 tff(c_1565, plain, (p(s(s(s(s(n0)))), s(s(s(s(s(s(n0)))))))=true)). % 7.16/2.91 tff(c_1523, plain, (p(s(s(s(s(s(s(n0)))))), s(s(s(s(s(n0))))))=true)). % 7.16/2.91 tff(c_1462, plain, (p(n0, s(s(s(s(s(s(s(n0))))))))=true)). % 7.16/2.91 tff(c_1421, plain, (p(s(s(n0)), s(s(s(s(s(s(n0)))))))=true)). % 7.16/2.91 tff(c_1381, plain, (p(s(s(s(s(n0)))), s(s(s(s(s(n0))))))=true)). % 7.16/2.91 tff(c_1343, plain, (p(s(s(s(s(s(s(n0)))))), s(s(s(s(n0)))))=true)). % 7.16/2.91 tff(c_741, plain, (p(s(s(s(s(s(s(s(s(s(s(n0)))))))))), s(s(s(s(s(s(s(n0))))))))=true)). % 7.16/2.91 tff(c_1269, plain, (p(n0, s(s(s(s(s(s(n0)))))))=true)). % 7.16/2.91 tff(c_1228, plain, (p(s(s(n0)), s(s(s(s(s(n0))))))=true)). % 7.16/2.91 tff(c_1188, plain, (p(s(s(s(s(n0)))), s(s(s(s(n0)))))=true)). % 7.16/2.91 tff(c_1150, plain, (p(s(s(s(s(s(s(n0)))))), s(s(s(n0))))=true)). % 7.16/2.91 tff(c_863, plain, (p(s(s(s(s(s(s(n0)))))), s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))=true)). % 7.16/2.91 tff(c_1093, plain, (p(s(s(s(s(s(s(s(s(n0)))))))), n0)=true)). % 7.16/2.91 tff(c_1051, plain, (p(n0, s(s(s(s(s(n0))))))=true)). % 7.16/2.91 tff(c_1011, plain, (p(s(s(n0)), s(s(s(s(n0)))))=true)). % 7.16/2.91 tff(c_213, plain, (ifeq(p(s(s(s(s(s(s(s(s(n0)))))))), s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))), true, true, true)=true)). % 7.16/2.91 tff(c_969, plain, (p(s(s(s(s(n0)))), s(s(s(n0))))=true)). % 7.16/2.91 tff(c_933, plain, (p(s(s(s(s(s(s(n0)))))), n0)=true)). % 7.16/2.91 tff(c_97, plain, (ifeq(p(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))), s(s(s(s(s(s(s(n0)))))))), true, true, true)=true)). % 7.16/2.91 tff(c_897, plain, (p(n0, s(s(s(s(n0)))))=true)). % 7.16/2.91 tff(c_849, plain, (p(s(s(n0)), s(s(s(n0))))=true)). % 7.16/2.91 tff(c_818, plain, (p(s(s(s(s(n0)))), n0)=true)). % 7.16/2.91 tff(c_787, plain, (p(n0, s(s(s(n0))))=true)). % 7.16/2.91 tff(c_761, plain, (p(s(s(n0)), n0)=true)). % 7.16/2.91 tff(c_727, plain, (p(n0, s(n0))=true)). % 7.16/2.91 tff(c_700, plain, (p(n0, s(s(n0)))=true)). % 7.16/2.91 tff(c_666, plain, (p(s(s(n0)), s(n0))=true)). % 7.16/2.91 tff(c_626, plain, (p(s(s(n0)), s(s(n0)))=true)). % 7.16/2.91 tff(c_63, plain, (ifeq(p(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))), s(s(s(s(s(s(s(s(n0))))))))), true, true, true)=true)). % 7.16/2.91 tff(c_592, plain, (p(s(s(s(s(n0)))), s(n0))=true)). % 7.16/2.91 tff(c_556, plain, (p(s(s(s(s(n0)))), s(s(n0)))=true)). % 7.16/2.91 tff(c_521, plain, (p(s(s(s(s(s(s(n0)))))), s(n0))=true)). % 7.16/2.91 tff(c_485, plain, (p(s(s(s(s(s(s(n0)))))), s(s(n0)))=true)). % 7.16/2.91 tff(c_451, plain, (p(s(s(s(s(s(s(s(s(n0)))))))), s(n0))=true)). % 7.16/2.91 tff(c_414, plain, (p(s(s(s(s(s(s(s(s(n0)))))))), s(s(n0)))=true)). % 7.16/2.91 tff(c_69, plain, (ifeq(p(s(s(s(s(s(s(s(s(s(s(n0)))))))))), s(s(s(s(s(s(s(s(s(s(n0))))))))))), true, true, true)=true)). % 7.16/2.91 tff(c_373, plain, (p(s(s(s(s(s(s(s(s(n0)))))))), s(s(s(n0))))=true)). % 7.16/2.91 tff(c_336, plain, (p(s(s(s(s(s(s(s(s(n0)))))))), s(s(s(s(n0)))))=true)). % 7.16/2.91 tff(c_298, plain, (p(s(s(s(s(s(s(s(s(n0)))))))), s(s(s(s(s(n0))))))=true)). % 7.16/2.91 tff(c_261, plain, (p(s(s(s(s(s(s(s(s(n0)))))))), s(s(s(s(s(s(n0)))))))=true)). % 7.16/2.91 tff(c_224, plain, (p(s(s(s(s(s(s(s(s(n0)))))))), s(s(s(s(s(s(s(n0))))))))=true)). % 7.16/2.91 tff(c_186, plain, (p(s(s(s(s(s(s(s(s(n0)))))))), s(s(s(s(s(s(s(s(s(s(n0)))))))))))=true)). % 7.16/2.91 tff(c_149, plain, (p(s(s(s(s(s(s(s(s(n0)))))))), s(s(s(s(s(s(s(s(n0)))))))))=true)). % 7.16/2.91 tff(c_113, plain, (p(s(s(s(s(s(s(s(s(n0)))))))), s(s(s(s(s(s(s(s(s(n0))))))))))=true)). % 7.16/2.92 tff(c_76, plain, (p(s(s(s(s(s(s(s(s(s(s(n0)))))))))), s(s(s(s(s(s(s(s(n0)))))))))=true)). % 7.16/2.92 tff(c_4, plain, (p(s(s(s(s(s(s(s(s(s(s(n0)))))))))), s(s(s(s(s(s(s(s(s(n0))))))))))=true)). % 7.16/2.92 tff(c_8, plain, (![X_6, Y_7]: (ifeq(p(X_6, s(s(Y_7))), true, p(X_6, s(Y_7)), true)=true))). % 7.16/2.92 tff(c_6, plain, (![X_4, Y_5]: (ifeq(p(s(s(X_4)), Y_5), true, p(X_4, s(Y_5)), true)=true))). % 7.16/2.92 tff(c_10, plain, (![X_8, Y_9]: (ifeq(p(s(X_8), s(Y_9)), true, p(s(X_8), Y_9), true)=true))). % 7.16/2.92 tff(c_2, plain, (![A_1, B_2, C_3]: (ifeq(A_1, A_1, B_2, C_3)=B_2))). % 7.16/2.92 tff(c_12, plain, (p(s(n0), n0)!=true)). % 7.16/2.92 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 7.16/2.92 %------------------------------------------------------------------------------