%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : LCL903+1 : TPTP v9.3.1. Released v5.5.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 : n002.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:57 AM UTC 2026
% Result : Theorem 18.09s 7.58s
% Output : CNFRefutation 18.22s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL903+1 : TPTP v9.3.1. Released v5.5.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.10/0.36 % Computer : n002.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sat Sep 5 13:52:35 UTC 2026
% 0.10/0.37 % CPUTime :
% 18.09/7.58 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 18.09/7.59
% 18.09/7.59 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 18.22/7.60 %$ >= > ==> > + > #nlpp > 1 > 0 > #skF_1
% 18.22/7.60
% 18.22/7.60 %Foreground sorts:
% 18.22/7.60
% 18.22/7.60
% 18.22/7.60 %Background operators:
% 18.22/7.60
% 18.22/7.60
% 18.22/7.60 %Foreground operators:
% 18.22/7.60 tff(==>, type, ==>: ($i * $i) > $i).
% 18.22/7.60 tff(+, type, +: ($i * $i) > $i).
% 18.22/7.60 tff(>=, type, >=: ($i * $i) > $o).
% 18.22/7.60 tff(0, type, 0: $i).
% 18.22/7.60 tff('#skF_1', type, '#skF_1': $i).
% 18.22/7.60 tff(1, type, 1: $i).
% 18.22/7.60
% 18.22/7.62 tff(f_51, axiom, (![A]: >=(A, 0)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_08)).
% 18.22/7.62 tff(f_31, axiom, (![A]: (+(A, 0) = A)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_03)).
% 18.22/7.62 tff(f_33, axiom, (![A]: >=(A, A)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_04)).
% 18.22/7.62 tff(f_49, axiom, (![X5, X6, X7]: (>=(+(X5, X6), X7) <=> >=(X6, ==>(X5, X7)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_07)).
% 18.22/7.62 tff(f_45, axiom, (![X3, X4]: ((>=(X3, X4) & >=(X4, X3)) => (X3 = X4))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_06)).
% 18.22/7.62 tff(f_29, axiom, (![A, B]: (+(A, B) = +(B, A))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_02)).
% 18.22/7.62 tff(f_65, axiom, (![A]: (+(A, 1) = 1)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_12)).
% 18.22/7.62 tff(f_55, axiom, (![X8, X9, X10]: (>=(X8, X9) => >=(+(X8, X10), +(X9, X10)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_09)).
% 18.22/7.62 tff(f_63, axiom, (![X14, X15, X16]: (>=(X14, X15) => >=(==>(X16, X14), ==>(X16, X15)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_11)).
% 18.22/7.62 tff(f_67, axiom, (![A]: (==>(==>(==>(A, 1), A), A) = 0)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_13)).
% 18.22/7.62 tff(f_59, axiom, (![X11, X12, X13]: (>=(X11, X12) => >=(==>(X12, X13), ==>(X11, X13)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_10)).
% 18.22/7.62 tff(f_70, negated_conjecture, ~(![X17]: (+(X17, X17) = X17)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', goals_14)).
% 18.22/7.62 tff(c_18, plain, (![A_16]: (>=(A_16, 0))), inference(cnfTransformation, [status(thm)], [f_51])).
% 18.22/7.62 tff(c_6, plain, (![A_6]: (+(A_6, 0)=A_6)), inference(cnfTransformation, [status(thm)], [f_31])).
% 18.22/7.62 tff(c_8, plain, (![A_7]: (>=(A_7, A_7))), inference(cnfTransformation, [status(thm)], [f_33])).
% 18.22/7.62 tff(c_252, plain, (![X6_43, X5_44, X7_45]: (>=(X6_43, ==>(X5_44, X7_45)) | ~>=(+(X5_44, X6_43), X7_45))), inference(cnfTransformation, [status(thm)], [f_49])).
% 18.22/7.62 tff(c_347, plain, (![X6_52, X5_53]: (>=(X6_52, ==>(X5_53, +(X5_53, X6_52))))), inference(resolution, [status(thm)], [c_8, c_252])).
% 18.22/7.62 tff(c_201, plain, (![X4_36, X3_37]: (X4_36=X3_37 | ~>=(X4_36, X3_37) | ~>=(X3_37, X4_36))), inference(cnfTransformation, [status(thm)], [f_45])).
% 18.22/7.62 tff(c_210, plain, (![A_16]: (A_16=0 | ~>=(0, A_16))), inference(resolution, [status(thm)], [c_18, c_201])).
% 18.22/7.62 tff(c_357, plain, (![X5_53]: (==>(X5_53, +(X5_53, 0))=0)), inference(resolution, [status(thm)], [c_347, c_210])).
% 18.22/7.62 tff(c_381, plain, (![X5_53]: (==>(X5_53, X5_53)=0)), inference(demodulation, [status(thm), theory('equality')], [c_6, c_357])).
% 18.22/7.62 tff(c_49, plain, (![B_32, A_33]: (+(B_32, A_33)=+(A_33, B_32))), inference(cnfTransformation, [status(thm)], [f_29])).
% 18.22/7.62 tff(c_26, plain, (![A_26]: (+(A_26, 1)=1)), inference(cnfTransformation, [status(thm)], [f_65])).
% 18.22/7.62 tff(c_65, plain, (![A_33]: (+(1, A_33)=1)), inference(superposition, [status(thm), theory('equality')], [c_49, c_26])).
% 18.22/7.62 tff(c_98, plain, (![A_6]: (+(0, A_6)=A_6)), inference(superposition, [status(thm), theory('equality')], [c_6, c_49])).
% 18.22/7.62 tff(c_437, plain, (![X8_56, X10_57, X9_58]: (>=(+(X8_56, X10_57), +(X9_58, X10_57)) | ~>=(X8_56, X9_58))), inference(cnfTransformation, [status(thm)], [f_55])).
% 18.22/7.62 tff(c_450, plain, (![X8_56, A_6]: (>=(+(X8_56, A_6), A_6) | ~>=(X8_56, 0))), inference(superposition, [status(thm), theory('equality')], [c_98, c_437])).
% 18.22/7.62 tff(c_491, plain, (![X8_59, A_60]: (>=(+(X8_59, A_60), A_60))), inference(demodulation, [status(thm), theory('equality')], [c_18, c_450])).
% 18.22/7.62 tff(c_504, plain, (![A_33]: (>=(1, A_33))), inference(superposition, [status(thm), theory('equality')], [c_65, c_491])).
% 18.22/7.62 tff(c_24, plain, (![X16_25, X14_23, X15_24]: (>=(==>(X16_25, X14_23), ==>(X16_25, X15_24)) | ~>=(X14_23, X15_24))), inference(cnfTransformation, [status(thm)], [f_63])).
% 18.22/7.62 tff(c_14, plain, (![X6_14, X5_13, X7_15]: (>=(X6_14, ==>(X5_13, X7_15)) | ~>=(+(X5_13, X6_14), X7_15))), inference(cnfTransformation, [status(thm)], [f_49])).
% 18.22/7.62 tff(c_517, plain, (![A_60, X8_59]: (>=(A_60, ==>(X8_59, A_60)))), inference(resolution, [status(thm)], [c_491, c_14])).
% 18.22/7.62 tff(c_28, plain, (![A_27]: (==>(==>(==>(A_27, 1), A_27), A_27)=0)), inference(cnfTransformation, [status(thm)], [f_67])).
% 18.22/7.62 tff(c_793, plain, (![X5_75, X6_76, X7_77]: (>=(+(X5_75, X6_76), X7_77) | ~>=(X6_76, ==>(X5_75, X7_77)))), inference(cnfTransformation, [status(thm)], [f_49])).
% 18.22/7.62 tff(c_981, plain, (![A_84, X7_85]: (>=(A_84, X7_85) | ~>=(0, ==>(A_84, X7_85)))), inference(superposition, [status(thm), theory('equality')], [c_6, c_793])).
% 18.22/7.62 tff(c_1008, plain, (![A_27]: (>=(==>(==>(A_27, 1), A_27), A_27) | ~>=(0, 0))), inference(superposition, [status(thm), theory('equality')], [c_28, c_981])).
% 18.22/7.62 tff(c_1248, plain, (![A_91]: (>=(==>(==>(A_91, 1), A_91), A_91))), inference(demodulation, [status(thm), theory('equality')], [c_18, c_1008])).
% 18.22/7.62 tff(c_12, plain, (![X4_12, X3_11]: (X4_12=X3_11 | ~>=(X4_12, X3_11) | ~>=(X3_11, X4_12))), inference(cnfTransformation, [status(thm)], [f_45])).
% 18.22/7.62 tff(c_1259, plain, (![A_91]: (==>(==>(A_91, 1), A_91)=A_91 | ~>=(A_91, ==>(==>(A_91, 1), A_91)))), inference(resolution, [status(thm)], [c_1248, c_12])).
% 18.22/7.62 tff(c_1286, plain, (![A_91]: (==>(==>(A_91, 1), A_91)=A_91)), inference(demodulation, [status(thm), theory('equality')], [c_517, c_1259])).
% 18.22/7.62 tff(c_691, plain, (![X12_69, X13_70, X11_71]: (>=(==>(X12_69, X13_70), ==>(X11_71, X13_70)) | ~>=(X11_71, X12_69))), inference(cnfTransformation, [status(thm)], [f_59])).
% 18.22/7.62 tff(c_25567, plain, (![X12_415, X13_416, X11_417]: (==>(X12_415, X13_416)===>(X11_417, X13_416) | ~>=(==>(X11_417, X13_416), ==>(X12_415, X13_416)) | ~>=(X11_417, X12_415))), inference(resolution, [status(thm)], [c_691, c_12])).
% 18.22/7.62 tff(c_25724, plain, (![X12_415, A_91]: (==>(X12_415, A_91)===>(==>(A_91, 1), A_91) | ~>=(A_91, ==>(X12_415, A_91)) | ~>=(==>(A_91, 1), X12_415))), inference(superposition, [status(thm), theory('equality')], [c_1286, c_25567])).
% 18.22/7.62 tff(c_31379, plain, (![X12_444, A_445]: (==>(X12_444, A_445)=A_445 | ~>=(==>(A_445, 1), X12_444))), inference(demodulation, [status(thm), theory('equality')], [c_517, c_1286, c_25724])).
% 18.22/7.62 tff(c_31523, plain, (![X16_25, X15_24]: (==>(==>(X16_25, X15_24), X16_25)=X16_25 | ~>=(1, X15_24))), inference(resolution, [status(thm)], [c_24, c_31379])).
% 18.22/7.62 tff(c_31576, plain, (![X16_446, X15_447]: (==>(==>(X16_446, X15_447), X16_446)=X16_446)), inference(demodulation, [status(thm), theory('equality')], [c_504, c_31523])).
% 18.22/7.62 tff(c_31570, plain, (![X16_25, X15_24]: (==>(==>(X16_25, X15_24), X16_25)=X16_25)), inference(demodulation, [status(thm), theory('equality')], [c_504, c_31523])).
% 18.22/7.62 tff(c_32934, plain, (![X16_454, X15_455]: (==>(X16_454, ==>(X16_454, X15_455))===>(X16_454, X15_455))), inference(superposition, [status(thm), theory('equality')], [c_31576, c_31570])).
% 18.22/7.62 tff(c_4, plain, (![B_5, A_4]: (+(B_5, A_4)=+(A_4, B_5))), inference(cnfTransformation, [status(thm)], [f_29])).
% 18.22/7.62 tff(c_368, plain, (![B_5, A_4]: (>=(B_5, ==>(A_4, +(B_5, A_4))))), inference(superposition, [status(thm), theory('equality')], [c_4, c_347])).
% 18.22/7.62 tff(c_1417, plain, (![A_96, X7_97]: (>=(0, ==>(A_96, X7_97)) | ~>=(A_96, X7_97))), inference(superposition, [status(thm), theory('equality')], [c_6, c_252])).
% 18.22/7.62 tff(c_1457, plain, (![A_98, X7_99]: (==>(A_98, X7_99)=0 | ~>=(A_98, X7_99))), inference(resolution, [status(thm)], [c_1417, c_210])).
% 18.22/7.62 tff(c_1510, plain, (![B_5, A_4]: (==>(B_5, ==>(A_4, +(B_5, A_4)))=0)), inference(resolution, [status(thm)], [c_368, c_1457])).
% 18.22/7.62 tff(c_33347, plain, (![X16_456]: (==>(X16_456, +(X16_456, X16_456))=0)), inference(superposition, [status(thm), theory('equality')], [c_32934, c_1510])).
% 18.22/7.62 tff(c_828, plain, (![A_6, X7_77]: (>=(A_6, X7_77) | ~>=(0, ==>(A_6, X7_77)))), inference(superposition, [status(thm), theory('equality')], [c_6, c_793])).
% 18.22/7.62 tff(c_33516, plain, (![X16_456]: (>=(X16_456, +(X16_456, X16_456)) | ~>=(0, 0))), inference(superposition, [status(thm), theory('equality')], [c_33347, c_828])).
% 18.22/7.62 tff(c_33717, plain, (![X16_457]: (>=(X16_457, +(X16_457, X16_457)))), inference(demodulation, [status(thm), theory('equality')], [c_18, c_33516])).
% 18.22/7.62 tff(c_833, plain, (![X7_77, X5_75, X6_76]: (X7_77=+(X5_75, X6_76) | ~>=(X7_77, +(X5_75, X6_76)) | ~>=(X6_76, ==>(X5_75, X7_77)))), inference(resolution, [status(thm)], [c_793, c_12])).
% 18.22/7.62 tff(c_33729, plain, (![X16_457]: (+(X16_457, X16_457)=X16_457 | ~>=(X16_457, ==>(X16_457, X16_457)))), inference(resolution, [status(thm)], [c_33717, c_833])).
% 18.22/7.62 tff(c_33895, plain, (![X16_457]: (+(X16_457, X16_457)=X16_457)), inference(demodulation, [status(thm), theory('equality')], [c_18, c_381, c_33729])).
% 18.22/7.62 tff(c_30, plain, (+('#skF_1', '#skF_1')!='#skF_1'), inference(cnfTransformation, [status(thm)], [f_70])).
% 18.22/7.62 tff(c_33957, plain, $false, inference(demodulation, [status(thm), theory('equality')], [c_33895, c_30])).
% 18.22/7.62 % SZS output end CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------