%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : LCL902+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 : n016.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 17.68s 5.51s
% Output : CNFRefutation 17.68s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL902+1 : TPTP v9.3.1. Released v5.5.0.
% 0.00/0.03 % 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.09/0.34 % Computer : n016.cluster.edu
% 0.09/0.34 % Model : x86_64 x86_64
% 0.09/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.34 % Memory : 8046.5625MB
% 0.09/0.34 % OS : Linux 6.8.0-71-generic
% 0.09/0.34 % CPULimit : 300
% 0.09/0.34 % WCLimit : 300
% 0.09/0.34 % DateTime : Sun Sep 6 01:10:15 UTC 2026
% 0.09/0.34 % CPUTime :
% 17.68/5.51 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 17.68/5.52
% 17.68/5.52 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 17.68/5.53 %$ >= > ==> > + > #nlpp > 1 > 0 > #skF_1
% 17.68/5.53
% 17.68/5.53 %Foreground sorts:
% 17.68/5.53
% 17.68/5.53
% 17.68/5.53 %Background operators:
% 17.68/5.53
% 17.68/5.53
% 17.68/5.53 %Foreground operators:
% 17.68/5.53 tff(==>, type, ==>: ($i * $i) > $i).
% 17.68/5.53 tff(+, type, +: ($i * $i) > $i).
% 17.68/5.53 tff(>=, type, >=: ($i * $i) > $o).
% 17.68/5.53 tff(0, type, 0: $i).
% 17.68/5.53 tff('#skF_1', type, '#skF_1': $i).
% 17.68/5.53 tff(1, type, 1: $i).
% 17.68/5.53
% 17.68/5.55 tff(f_51, axiom, (![A]: >=(A, 0)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_08)).
% 17.68/5.55 tff(f_67, axiom, (![A]: (==>(==>(==>(A, 1), A), A) = 0)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_13)).
% 17.68/5.55 tff(f_65, axiom, (![A]: (+(A, 1) = 1)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_12)).
% 17.68/5.55 tff(f_49, axiom, (![X5, X6, X7]: (>=(+(X5, X6), X7) <=> >=(X6, ==>(X5, X7)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_07)).
% 17.68/5.55 tff(f_33, axiom, (![A]: >=(A, A)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_04)).
% 17.68/5.55 tff(f_29, axiom, (![A, B]: (+(A, B) = +(B, A))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_02)).
% 17.68/5.55 tff(f_45, axiom, (![X3, X4]: ((>=(X3, X4) & >=(X4, X3)) => (X3 = X4))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_06)).
% 17.68/5.55 tff(f_31, axiom, (![A]: (+(A, 0) = A)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_03)).
% 17.68/5.55 tff(f_55, axiom, (![X8, X9, X10]: (>=(X8, X9) => >=(+(X8, X10), +(X9, X10)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_09)).
% 17.68/5.55 tff(f_70, negated_conjecture, ~(![X17]: (==>(==>(X17, 1), 1) = X17)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', goals_14)).
% 17.68/5.55 tff(c_18, plain, (![A_16]: (>=(A_16, 0))), inference(cnfTransformation, [status(thm)], [f_51])).
% 17.68/5.55 tff(c_28, plain, (![A_27]: (==>(==>(==>(A_27, 1), A_27), A_27)=0)), inference(cnfTransformation, [status(thm)], [f_67])).
% 17.68/5.55 tff(c_26, plain, (![A_26]: (+(A_26, 1)=1)), inference(cnfTransformation, [status(thm)], [f_65])).
% 17.68/5.55 tff(c_266, plain, (![X5_46, X6_47, X7_48]: (>=(+(X5_46, X6_47), X7_48) | ~>=(X6_47, ==>(X5_46, X7_48)))), inference(cnfTransformation, [status(thm)], [f_49])).
% 17.68/5.55 tff(c_308, plain, (![X7_52, A_53]: (>=(1, X7_52) | ~>=(1, ==>(A_53, X7_52)))), inference(superposition, [status(thm), theory('equality')], [c_26, c_266])).
% 17.68/5.55 tff(c_311, plain, (![A_27]: (>=(1, A_27) | ~>=(1, 0))), inference(superposition, [status(thm), theory('equality')], [c_28, c_308])).
% 17.68/5.55 tff(c_313, plain, (![A_27]: (>=(1, A_27))), inference(demodulation, [status(thm), theory('equality')], [c_18, c_311])).
% 17.68/5.55 tff(c_8, plain, (![A_7]: (>=(A_7, A_7))), inference(cnfTransformation, [status(thm)], [f_33])).
% 17.68/5.55 tff(c_4, plain, (![B_5, A_4]: (+(B_5, A_4)=+(A_4, B_5))), inference(cnfTransformation, [status(thm)], [f_29])).
% 17.68/5.55 tff(c_4736, plain, (![B_179, A_180, X7_181]: (>=(+(B_179, A_180), X7_181) | ~>=(B_179, ==>(A_180, X7_181)))), inference(superposition, [status(thm), theory('equality')], [c_4, c_266])).
% 17.68/5.55 tff(c_316, plain, (![A_54]: (>=(1, A_54))), inference(demodulation, [status(thm), theory('equality')], [c_18, c_311])).
% 17.68/5.55 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])).
% 17.68/5.55 tff(c_322, plain, (![A_54]: (A_54=1 | ~>=(A_54, 1))), inference(resolution, [status(thm)], [c_316, c_12])).
% 17.68/5.55 tff(c_9466, plain, (![B_270, A_271]: (+(B_270, A_271)=1 | ~>=(B_270, ==>(A_271, 1)))), inference(resolution, [status(thm)], [c_4736, c_322])).
% 17.68/5.55 tff(c_9673, plain, (![A_272]: (+(==>(A_272, 1), A_272)=1)), inference(resolution, [status(thm)], [c_8, c_9466])).
% 17.68/5.55 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])).
% 17.68/5.55 tff(c_9893, plain, (![A_272, X7_15]: (>=(A_272, ==>(==>(A_272, 1), X7_15)) | ~>=(1, X7_15))), inference(superposition, [status(thm), theory('equality')], [c_9673, c_14])).
% 17.68/5.55 tff(c_10040, plain, (![A_272, X7_15]: (>=(A_272, ==>(==>(A_272, 1), X7_15)))), inference(demodulation, [status(thm), theory('equality')], [c_313, c_9893])).
% 17.68/5.55 tff(c_6, plain, (![A_6]: (+(A_6, 0)=A_6)), inference(cnfTransformation, [status(thm)], [f_31])).
% 17.68/5.55 tff(c_291, plain, (![A_49, X7_50]: (>=(A_49, X7_50) | ~>=(0, ==>(A_49, X7_50)))), inference(superposition, [status(thm), theory('equality')], [c_6, c_266])).
% 17.68/5.55 tff(c_294, plain, (![A_27]: (>=(==>(==>(A_27, 1), A_27), A_27) | ~>=(0, 0))), inference(superposition, [status(thm), theory('equality')], [c_28, c_291])).
% 17.68/5.55 tff(c_296, plain, (![A_27]: (>=(==>(==>(A_27, 1), A_27), A_27))), inference(demodulation, [status(thm), theory('equality')], [c_18, c_294])).
% 17.68/5.55 tff(c_49, plain, (![B_32, A_33]: (+(B_32, A_33)=+(A_33, B_32))), inference(cnfTransformation, [status(thm)], [f_29])).
% 17.68/5.55 tff(c_95, plain, (![A_6]: (+(0, A_6)=A_6)), inference(superposition, [status(thm), theory('equality')], [c_6, c_49])).
% 17.68/5.55 tff(c_447, plain, (![X8_61, X10_62, X9_63]: (>=(+(X8_61, X10_62), +(X9_63, X10_62)) | ~>=(X8_61, X9_63))), inference(cnfTransformation, [status(thm)], [f_55])).
% 17.68/5.55 tff(c_457, plain, (![X8_61, A_6]: (>=(+(X8_61, A_6), A_6) | ~>=(X8_61, 0))), inference(superposition, [status(thm), theory('equality')], [c_95, c_447])).
% 17.68/5.55 tff(c_491, plain, (![X8_61, A_6]: (>=(+(X8_61, A_6), A_6))), inference(demodulation, [status(thm), theory('equality')], [c_18, c_457])).
% 17.68/5.55 tff(c_634, plain, (![X6_69, X5_70, X7_71]: (>=(X6_69, ==>(X5_70, X7_71)) | ~>=(+(X5_70, X6_69), X7_71))), inference(cnfTransformation, [status(thm)], [f_49])).
% 17.68/5.55 tff(c_905, plain, (![A_79, X8_80]: (>=(A_79, ==>(X8_80, A_79)))), inference(resolution, [status(thm)], [c_491, c_634])).
% 17.68/5.55 tff(c_21198, plain, (![X8_362, A_363]: (==>(X8_362, A_363)=A_363 | ~>=(==>(X8_362, A_363), A_363))), inference(resolution, [status(thm)], [c_905, c_12])).
% 17.68/5.55 tff(c_21341, plain, (![A_364]: (==>(==>(A_364, 1), A_364)=A_364)), inference(resolution, [status(thm)], [c_296, c_21198])).
% 17.68/5.55 tff(c_655, plain, (![B_5, A_4, X7_71]: (>=(B_5, ==>(A_4, X7_71)) | ~>=(+(B_5, A_4), X7_71))), inference(superposition, [status(thm), theory('equality')], [c_4, c_634])).
% 17.68/5.55 tff(c_9822, plain, (![A_272, X7_71]: (>=(==>(A_272, 1), ==>(A_272, X7_71)) | ~>=(1, X7_71))), inference(superposition, [status(thm), theory('equality')], [c_9673, c_655])).
% 17.68/5.55 tff(c_10022, plain, (![A_272, X7_71]: (>=(==>(A_272, 1), ==>(A_272, X7_71)))), inference(demodulation, [status(thm), theory('equality')], [c_313, c_9822])).
% 17.68/5.55 tff(c_21668, plain, (![A_365]: (>=(==>(==>(A_365, 1), 1), A_365))), inference(superposition, [status(thm), theory('equality')], [c_21341, c_10022])).
% 17.68/5.55 tff(c_21726, plain, (![A_365]: (==>(==>(A_365, 1), 1)=A_365 | ~>=(A_365, ==>(==>(A_365, 1), 1)))), inference(resolution, [status(thm)], [c_21668, c_12])).
% 17.68/5.55 tff(c_21803, plain, (![A_365]: (==>(==>(A_365, 1), 1)=A_365)), inference(demodulation, [status(thm), theory('equality')], [c_10040, c_21726])).
% 17.68/5.55 tff(c_30, plain, (==>(==>('#skF_1', 1), 1)!='#skF_1'), inference(cnfTransformation, [status(thm)], [f_70])).
% 17.68/5.55 tff(c_21820, plain, $false, inference(demodulation, [status(thm), theory('equality')], [c_21803, c_30])).
% 17.68/5.55 % SZS output end CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------