%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : NUN135-1.006 : TPTP v9.3.0. Released v9.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 : n003.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 : Tue May 5 06:48:36 PM UTC 2026
% Result : Unsatisfiable 27.71s 16.41s
% Output : CNFRefutation 27.71s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : NUN135-1.006 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.12 % 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.14/0.33 % Computer : n003.cluster.edu
% 0.14/0.33 % Model : x86_64 x86_64
% 0.14/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.33 % Memory : 8042.1875MB
% 0.14/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.33 % CPULimit : 300
% 0.14/0.33 % WCLimit : 300
% 0.14/0.33 % DateTime : Tue May 5 04:49:11 EDT 2026
% 0.14/0.33 % CPUTime :
% 27.71/16.41 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 27.71/16.42
% 27.71/16.42 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 27.71/16.42 %$ f > if > minus > <= > #nlpp > s > perfectp > zero > true > false
% 27.71/16.42
% 27.71/16.42 %Foreground sorts:
% 27.71/16.42
% 27.71/16.42
% 27.71/16.42 %Background operators:
% 27.71/16.42
% 27.71/16.42
% 27.71/16.42 %Foreground operators:
% 27.71/16.42 tff(f, type, f: ($i * $i * $i * $i) > $i).
% 27.71/16.42 tff(s, type, s: $i > $i).
% 27.71/16.42 tff(perfectp, type, perfectp: $i > $i).
% 27.71/16.42 tff(true, type, true: $i).
% 27.71/16.42 tff(if, type, if: ($i * $i * $i) > $i).
% 27.71/16.42 tff(false, type, false: $i).
% 27.71/16.42 tff(<=, type, <=: ($i * $i) > $i).
% 27.71/16.42 tff(zero, type, zero: $i).
% 27.71/16.42 tff(minus, type, minus: ($i * $i) > $i).
% 27.71/16.42
% 27.71/16.44 tff(f_50, axiom, (![X]: ~(perfectp(X) = true)), file('unknown', unknown)).
% 27.71/16.44 tff(f_24, axiom, (![X]: (minus(X, zero) = X)), file('unknown', unknown)).
% 27.71/16.44 tff(f_26, axiom, (![X, Y]: (minus(s(X), s(Y)) = minus(X, Y))), file('unknown', unknown)).
% 27.71/16.44 tff(f_45, axiom, (![X, Z, U]: (f(s(X), zero, Z, U) = f(X, U, minus(Z, s(X)), U))), file('unknown', unknown)).
% 27.71/16.44 tff(f_41, axiom, (![Y, U]: (f(zero, Y, zero, U) = true)), file('unknown', unknown)).
% 27.71/16.44 tff(f_34, axiom, (![X, Y]: (if(true, X, Y) = X)), file('unknown', unknown)).
% 27.71/16.44 tff(f_28, axiom, (![Y]: (<=(zero, Y) = true)), file('unknown', unknown)).
% 27.71/16.44 tff(f_47, axiom, (![X, Y, Z, U]: (f(s(X), s(Y), Z, U) = if(<=(X, Y), f(s(X), minus(Y, X), Z, U), f(X, U, Z, U)))), file('unknown', unknown)).
% 27.71/16.44 tff(f_30, axiom, (![X]: (<=(s(X), zero) = false)), file('unknown', unknown)).
% 27.71/16.44 tff(f_36, axiom, (![X, Y]: (if(false, X, Y) = Y)), file('unknown', unknown)).
% 27.71/16.44 tff(f_32, axiom, (![X, Y]: (<=(s(X), s(Y)) = <=(X, Y))), file('unknown', unknown)).
% 27.71/16.44 tff(f_39, axiom, (![X]: (perfectp(s(X)) = f(X, s(zero), s(X), s(X)))), file('unknown', unknown)).
% 27.71/16.44 tff(c_28, plain, (![X_25]: (perfectp(X_25)!=true)), inference(cnfTransformation, [status(thm)], [f_50])).
% 27.71/16.44 tff(c_2, plain, (![X_1]: (minus(X_1, zero)=X_1)), inference(cnfTransformation, [status(thm)], [f_24])).
% 27.71/16.44 tff(c_4, plain, (![X_2, Y_3]: (minus(s(X_2), s(Y_3))=minus(X_2, Y_3))), inference(cnfTransformation, [status(thm)], [f_26])).
% 27.71/16.44 tff(c_133, plain, (![X_44, U_45, Z_46]: (f(X_44, U_45, minus(Z_46, s(X_44)), U_45)=f(s(X_44), zero, Z_46, U_45))), inference(cnfTransformation, [status(thm)], [f_45])).
% 27.71/16.44 tff(c_145, plain, (![Y_47, X_48, U_49]: (f(s(Y_47), zero, s(X_48), U_49)=f(Y_47, U_49, minus(X_48, Y_47), U_49))), inference(superposition, [status(thm), theory('equality')], [c_4, c_133])).
% 27.71/16.44 tff(c_168, plain, (![U_50, X_51]: (f(zero, U_50, X_51, U_50)=f(s(zero), zero, s(X_51), U_50))), inference(superposition, [status(thm), theory('equality')], [c_2, c_145])).
% 27.71/16.44 tff(c_20, plain, (![Y_13, U_14]: (f(zero, Y_13, zero, U_14)=true)), inference(cnfTransformation, [status(thm)], [f_41])).
% 27.71/16.44 tff(c_193, plain, (![U_50]: (f(s(zero), zero, s(zero), U_50)=true)), inference(superposition, [status(thm), theory('equality')], [c_168, c_20])).
% 27.71/16.44 tff(c_12, plain, (![X_8, Y_9]: (if(true, X_8, Y_9)=X_8)), inference(cnfTransformation, [status(thm)], [f_34])).
% 27.71/16.44 tff(c_6, plain, (![Y_4]: (<=(zero, Y_4)=true)), inference(cnfTransformation, [status(thm)], [f_28])).
% 27.71/16.44 tff(c_253, plain, (![X_53, Y_54, Z_55, U_56]: (if(<=(X_53, Y_54), f(s(X_53), minus(Y_54, X_53), Z_55, U_56), f(X_53, U_56, Z_55, U_56))=f(s(X_53), s(Y_54), Z_55, U_56))), inference(cnfTransformation, [status(thm)], [f_47])).
% 27.71/16.44 tff(c_312, plain, (![X_1, Z_55, U_56]: (if(<=(zero, X_1), f(s(zero), X_1, Z_55, U_56), f(zero, U_56, Z_55, U_56))=f(s(zero), s(X_1), Z_55, U_56))), inference(superposition, [status(thm), theory('equality')], [c_2, c_253])).
% 27.71/16.44 tff(c_325, plain, (![X_1, Z_55, U_56]: (f(s(zero), s(X_1), Z_55, U_56)=f(s(zero), X_1, Z_55, U_56))), inference(demodulation, [status(thm), theory('equality')], [c_12, c_6, c_312])).
% 27.71/16.44 tff(c_8, plain, (![X_5]: (<=(s(X_5), zero)=false)), inference(cnfTransformation, [status(thm)], [f_30])).
% 27.71/16.44 tff(c_593, plain, (![X_71, Z_72, U_73]: (if(false, f(s(s(X_71)), minus(zero, s(X_71)), Z_72, U_73), f(s(X_71), U_73, Z_72, U_73))=f(s(s(X_71)), s(zero), Z_72, U_73))), inference(superposition, [status(thm), theory('equality')], [c_8, c_253])).
% 27.71/16.44 tff(c_14, plain, (![X_10, Y_11]: (if(false, X_10, Y_11)=Y_11)), inference(cnfTransformation, [status(thm)], [f_36])).
% 27.71/16.44 tff(c_687, plain, (![X_75, Z_76, U_77]: (f(s(s(X_75)), s(zero), Z_76, U_77)=f(s(X_75), U_77, Z_76, U_77))), inference(superposition, [status(thm), theory('equality')], [c_593, c_14])).
% 27.71/16.44 tff(c_843, plain, (![X_79, Z_80]: (f(s(zero), X_79, Z_80, s(X_79))=f(s(s(zero)), s(zero), Z_80, s(X_79)))), inference(superposition, [status(thm), theory('equality')], [c_325, c_687])).
% 27.71/16.44 tff(c_1268, plain, (![X_97, Z_98]: (f(s(zero), X_97, Z_98, s(s(X_97)))=f(s(s(zero)), s(zero), Z_98, s(s(X_97))))), inference(superposition, [status(thm), theory('equality')], [c_843, c_325])).
% 27.71/16.44 tff(c_3540, plain, (![X_159, Z_160]: (f(s(zero), X_159, Z_160, s(s(s(X_159))))=f(s(s(zero)), s(zero), Z_160, s(s(s(X_159)))))), inference(superposition, [status(thm), theory('equality')], [c_325, c_1268])).
% 27.71/16.44 tff(c_3614, plain, (![X_1, Z_55]: (f(s(zero), X_1, Z_55, s(s(s(s(X_1)))))=f(s(s(zero)), s(zero), Z_55, s(s(s(s(X_1))))))), inference(superposition, [status(thm), theory('equality')], [c_325, c_3540])).
% 27.71/16.44 tff(c_459, plain, (![Y_66, X_67, U_68]: (f(s(s(Y_66)), zero, s(s(X_67)), U_68)=f(s(Y_66), U_68, minus(X_67, Y_66), U_68))), inference(superposition, [status(thm), theory('equality')], [c_4, c_145])).
% 27.71/16.44 tff(c_503, plain, (![U_68, X_1]: (f(s(zero), U_68, X_1, U_68)=f(s(s(zero)), zero, s(s(X_1)), U_68))), inference(superposition, [status(thm), theory('equality')], [c_2, c_459])).
% 27.71/16.44 tff(c_768, plain, (![X_1, U_68]: (f(s(s(zero)), zero, s(s(X_1)), U_68)=f(s(s(zero)), s(zero), X_1, U_68))), inference(superposition, [status(thm), theory('equality')], [c_503, c_687])).
% 27.71/16.44 tff(c_10, plain, (![X_6, Y_7]: (<=(s(X_6), s(Y_7))=<=(X_6, Y_7))), inference(cnfTransformation, [status(thm)], [f_32])).
% 27.71/16.44 tff(c_295, plain, (![Y_3, X_2, Z_55, U_56]: (if(<=(s(Y_3), s(X_2)), f(s(s(Y_3)), minus(X_2, Y_3), Z_55, U_56), f(s(Y_3), U_56, Z_55, U_56))=f(s(s(Y_3)), s(s(X_2)), Z_55, U_56))), inference(superposition, [status(thm), theory('equality')], [c_4, c_253])).
% 27.71/16.44 tff(c_969, plain, (![Y_83, X_84, Z_85, U_86]: (if(<=(Y_83, X_84), f(s(s(Y_83)), minus(X_84, Y_83), Z_85, U_86), f(s(Y_83), U_86, Z_85, U_86))=f(s(s(Y_83)), s(s(X_84)), Z_85, U_86))), inference(demodulation, [status(thm), theory('equality')], [c_10, c_295])).
% 27.71/16.44 tff(c_1060, plain, (![X_1, Z_85, U_86]: (if(<=(zero, X_1), f(s(s(zero)), X_1, Z_85, U_86), f(s(zero), U_86, Z_85, U_86))=f(s(s(zero)), s(s(X_1)), Z_85, U_86))), inference(superposition, [status(thm), theory('equality')], [c_2, c_969])).
% 27.71/16.44 tff(c_1076, plain, (![X_1, Z_85, U_86]: (f(s(s(zero)), s(s(X_1)), Z_85, U_86)=f(s(s(zero)), X_1, Z_85, U_86))), inference(demodulation, [status(thm), theory('equality')], [c_12, c_6, c_1060])).
% 27.71/16.44 tff(c_599, plain, (![X_71, Z_72, U_73]: (f(s(s(X_71)), s(zero), Z_72, U_73)=f(s(X_71), U_73, Z_72, U_73))), inference(superposition, [status(thm), theory('equality')], [c_593, c_14])).
% 27.71/16.44 tff(c_1078, plain, (![X_87, Z_88, U_89]: (f(s(s(zero)), s(s(X_87)), Z_88, U_89)=f(s(s(zero)), X_87, Z_88, U_89))), inference(demodulation, [status(thm), theory('equality')], [c_12, c_6, c_1060])).
% 27.71/16.44 tff(c_2399, plain, (![X_131, Z_132]: (f(s(s(zero)), X_131, Z_132, s(s(X_131)))=f(s(s(s(zero))), s(zero), Z_132, s(s(X_131))))), inference(superposition, [status(thm), theory('equality')], [c_599, c_1078])).
% 27.71/16.44 tff(c_2425, plain, (![X_1, Z_132]: (f(s(s(zero)), X_1, Z_132, s(s(s(s(X_1)))))=f(s(s(s(zero))), s(zero), Z_132, s(s(s(s(X_1))))))), inference(superposition, [status(thm), theory('equality')], [c_2399, c_1076])).
% 27.71/16.44 tff(c_2680, plain, (![X_137, Z_138, U_139]: (if(false, f(s(s(s(X_137))), minus(zero, s(X_137)), Z_138, U_139), f(s(s(X_137)), U_139, Z_138, U_139))=f(s(s(s(X_137))), s(s(zero)), Z_138, U_139))), inference(superposition, [status(thm), theory('equality')], [c_8, c_969])).
% 27.71/16.44 tff(c_2747, plain, (![X_137, Z_72, U_73]: (if(false, f(s(s(s(X_137))), minus(zero, s(X_137)), Z_72, U_73), f(s(s(s(X_137))), s(zero), Z_72, U_73))=f(s(s(s(X_137))), s(s(zero)), Z_72, U_73))), inference(superposition, [status(thm), theory('equality')], [c_599, c_2680])).
% 27.71/16.44 tff(c_2803, plain, (![X_137, Z_72, U_73]: (f(s(s(s(X_137))), s(s(zero)), Z_72, U_73)=f(s(s(s(X_137))), s(zero), Z_72, U_73))), inference(demodulation, [status(thm), theory('equality')], [c_14, c_2747])).
% 27.71/16.44 tff(c_18, plain, (![X_12]: (f(X_12, s(zero), s(X_12), s(X_12))=perfectp(s(X_12)))), inference(cnfTransformation, [status(thm)], [f_39])).
% 27.71/16.44 tff(c_1054, plain, (![X_6, Y_7, Z_85, U_86]: (if(<=(X_6, Y_7), f(s(s(s(X_6))), minus(s(Y_7), s(X_6)), Z_85, U_86), f(s(s(X_6)), U_86, Z_85, U_86))=f(s(s(s(X_6))), s(s(s(Y_7))), Z_85, U_86))), inference(superposition, [status(thm), theory('equality')], [c_10, c_969])).
% 27.71/16.44 tff(c_4545, plain, (![X_189, Y_190, Z_191, U_192]: (if(<=(X_189, Y_190), f(s(s(s(X_189))), minus(Y_190, X_189), Z_191, U_192), f(s(s(X_189)), U_192, Z_191, U_192))=f(s(s(s(X_189))), s(s(s(Y_190))), Z_191, U_192))), inference(demodulation, [status(thm), theory('equality')], [c_4, c_1054])).
% 27.71/16.44 tff(c_4685, plain, (![Y_3, X_2, Z_191, U_192]: (if(<=(s(Y_3), s(X_2)), f(s(s(s(s(Y_3)))), minus(X_2, Y_3), Z_191, U_192), f(s(s(s(Y_3))), U_192, Z_191, U_192))=f(s(s(s(s(Y_3)))), s(s(s(s(X_2)))), Z_191, U_192))), inference(superposition, [status(thm), theory('equality')], [c_4, c_4545])).
% 27.71/16.44 tff(c_21992, plain, (![Y_491, X_492, Z_493, U_494]: (if(<=(Y_491, X_492), f(s(s(s(s(Y_491)))), minus(X_492, Y_491), Z_493, U_494), f(s(s(s(Y_491))), U_494, Z_493, U_494))=f(s(s(s(s(Y_491)))), s(s(s(s(X_492)))), Z_493, U_494))), inference(demodulation, [status(thm), theory('equality')], [c_10, c_4685])).
% 27.71/16.44 tff(c_22319, plain, (![X_1, Z_493, U_494]: (if(<=(zero, X_1), f(s(s(s(s(zero)))), X_1, Z_493, U_494), f(s(s(s(zero))), U_494, Z_493, U_494))=f(s(s(s(s(zero)))), s(s(s(s(X_1)))), Z_493, U_494))), inference(superposition, [status(thm), theory('equality')], [c_2, c_21992])).
% 27.71/16.44 tff(c_22362, plain, (![X_495, Z_496, U_497]: (f(s(s(s(s(zero)))), s(s(s(s(X_495)))), Z_496, U_497)=f(s(s(s(s(zero)))), X_495, Z_496, U_497))), inference(demodulation, [status(thm), theory('equality')], [c_12, c_6, c_22319])).
% 27.71/16.44 tff(c_24905, plain, (![X_528, Z_529]: (f(s(s(s(s(zero)))), X_528, Z_529, s(s(s(s(X_528)))))=f(s(s(s(s(s(zero))))), s(zero), Z_529, s(s(s(s(X_528))))))), inference(superposition, [status(thm), theory('equality')], [c_599, c_22362])).
% 27.71/16.44 tff(c_25042, plain, (f(s(s(s(s(zero)))), s(s(zero)), s(s(s(s(s(s(zero)))))), s(s(s(s(s(s(zero)))))))=perfectp(s(s(s(s(s(s(zero)))))))), inference(superposition, [status(thm), theory('equality')], [c_18, c_24905])).
% 27.71/16.44 tff(c_30525, plain, (f(s(s(s(s(zero)))), s(zero), s(s(s(s(s(s(zero)))))), s(s(s(s(s(s(zero)))))))=perfectp(s(s(s(s(s(s(zero)))))))), inference(superposition, [status(thm), theory('equality')], [c_2803, c_25042])).
% 27.71/16.44 tff(c_4694, plain, (![X_1, Z_191, U_192]: (if(<=(zero, X_1), f(s(s(s(zero))), X_1, Z_191, U_192), f(s(s(zero)), U_192, Z_191, U_192))=f(s(s(s(zero))), s(s(s(X_1))), Z_191, U_192))), inference(superposition, [status(thm), theory('equality')], [c_2, c_4545])).
% 27.71/16.44 tff(c_4715, plain, (![X_1, Z_191, U_192]: (f(s(s(s(zero))), s(s(s(X_1))), Z_191, U_192)=f(s(s(s(zero))), X_1, Z_191, U_192))), inference(demodulation, [status(thm), theory('equality')], [c_12, c_6, c_4694])).
% 27.71/16.44 tff(c_4717, plain, (![X_193, Z_194, U_195]: (f(s(s(s(zero))), s(s(s(X_193))), Z_194, U_195)=f(s(s(s(zero))), X_193, Z_194, U_195))), inference(demodulation, [status(thm), theory('equality')], [c_12, c_6, c_4694])).
% 27.71/16.44 tff(c_9550, plain, (![X_298, Z_299]: (f(s(s(s(zero))), X_298, Z_299, s(s(s(X_298))))=f(s(s(s(s(zero)))), s(zero), Z_299, s(s(s(X_298)))))), inference(superposition, [status(thm), theory('equality')], [c_599, c_4717])).
% 27.71/16.44 tff(c_9626, plain, (![X_1, Z_191]: (f(s(s(s(zero))), X_1, Z_191, s(s(s(s(s(s(X_1)))))))=f(s(s(s(s(zero)))), s(zero), Z_191, s(s(s(s(s(s(X_1))))))))), inference(superposition, [status(thm), theory('equality')], [c_4715, c_9550])).
% 27.71/16.44 tff(c_49520, plain, (f(s(s(s(zero))), zero, s(s(s(s(s(s(zero)))))), s(s(s(s(s(s(zero)))))))=perfectp(s(s(s(s(s(s(zero)))))))), inference(superposition, [status(thm), theory('equality')], [c_30525, c_9626])).
% 27.71/16.44 tff(c_142, plain, (![Y_3, X_2, U_45]: (f(s(Y_3), zero, s(X_2), U_45)=f(Y_3, U_45, minus(X_2, Y_3), U_45))), inference(superposition, [status(thm), theory('equality')], [c_4, c_133])).
% 27.71/16.44 tff(c_648, plain, (![X_71, X_2, U_45]: (if(false, f(s(s(X_71)), minus(zero, s(X_71)), minus(X_2, s(X_71)), U_45), f(s(s(X_71)), zero, s(X_2), U_45))=f(s(s(X_71)), s(zero), minus(X_2, s(X_71)), U_45))), inference(superposition, [status(thm), theory('equality')], [c_142, c_593])).
% 27.71/16.44 tff(c_1716, plain, (![X_112, X_113, U_114]: (f(s(s(X_112)), s(zero), minus(X_113, s(X_112)), U_114)=f(s(s(X_112)), zero, s(X_113), U_114))), inference(demodulation, [status(thm), theory('equality')], [c_14, c_648])).
% 27.71/16.44 tff(c_1873, plain, (![Y_117, X_118, U_119]: (f(s(s(Y_117)), s(zero), minus(X_118, Y_117), U_119)=f(s(s(Y_117)), zero, s(s(X_118)), U_119))), inference(superposition, [status(thm), theory('equality')], [c_4, c_1716])).
% 27.71/16.44 tff(c_1917, plain, (![Y_3, X_2, U_119]: (f(s(s(s(Y_3))), zero, s(s(s(X_2))), U_119)=f(s(s(s(Y_3))), s(zero), minus(X_2, Y_3), U_119))), inference(superposition, [status(thm), theory('equality')], [c_4, c_1873])).
% 27.71/16.44 tff(c_50107, plain, (f(s(s(s(zero))), s(zero), minus(s(s(s(zero))), zero), s(s(s(s(s(s(zero)))))))=perfectp(s(s(s(s(s(s(zero)))))))), inference(superposition, [status(thm), theory('equality')], [c_49520, c_1917])).
% 27.71/16.44 tff(c_50141, plain, (perfectp(s(s(s(s(s(s(zero)))))))=true), inference(demodulation, [status(thm), theory('equality')], [c_193, c_325, c_325, c_3614, c_768, c_1076, c_2425, c_2, c_50107])).
% 27.71/16.44 tff(c_50143, plain, $false, inference(negUnitSimplification, [status(thm)], [c_28, c_50141])).
% 27.71/16.44 % SZS output end CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------