%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SYO629-1 : TPTP v9.0.0. Released v7.1.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 : n013.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:00 PM UTC 2025
% Result : Unsatisfiable 2.86s 1.76s
% Output : CNFRefutation 2.88s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : SYO629-1 : TPTP v9.0.0. Released v7.1.0.
% 0.11/0.13 % 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.13/0.33 % Computer : n013.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Wed Apr 9 09:38:02 EDT 2025
% 0.13/0.34 % CPUTime :
% 2.86/1.76 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 2.88/1.77
% 2.88/1.77 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 2.88/1.78 %$ iLEQ > LE > E > #nlpp > s > g > f > 0
% 2.88/1.78
% 2.88/1.78 %Foreground sorts:
% 2.88/1.78
% 2.88/1.78
% 2.88/1.78 %Background operators:
% 2.88/1.78
% 2.88/1.78
% 2.88/1.78 %Foreground operators:
% 2.88/1.78 tff(iLEQ, type, iLEQ: ($i * $i) > $o).
% 2.88/1.78 tff(s, type, s: $i > $i).
% 2.88/1.78 tff(f, type, f: $i > $i).
% 2.88/1.78 tff(g, type, g: $i > $i).
% 2.88/1.78 tff(0, type, 0: $i).
% 2.88/1.78 tff(LE, type, LE: ($i * $i) > $o).
% 2.88/1.78 tff(E, type, E: ($i * $i) > $o).
% 2.88/1.78
% 2.88/1.79 tff(f_41, axiom, (![A]: (E(s(0), f(A)) | LE(f(A), s(0)))), file('unknown', unknown)).
% 2.88/1.79 tff(f_69, axiom, (![A_2]: iLEQ(A_2, g(A_2))), file('unknown', unknown)).
% 2.88/1.79 tff(f_44, axiom, (![A_3]: ~LE(f(A_3), 0)), file('unknown', unknown)).
% 2.88/1.79 tff(f_54, axiom, (![A_1, B_0]: (((~LE(f(A_1), s(0)) | ~iLEQ(A_1, B_0)) | E(0, f(B_0))) | LE(f(B_0), 0))), file('unknown', unknown)).
% 2.88/1.79 tff(f_74, axiom, (![A_2]: iLEQ(A_2, A_2)), file('unknown', unknown)).
% 2.88/1.79 tff(f_72, axiom, (![A_2]: ~E(f(A_2), f(g(A_2)))), file('unknown', unknown)).
% 2.88/1.79 tff(f_62, axiom, (![A_2]: ((~E(s(0), f(A_2)) | ~E(s(0), f(g(A_2)))) | E(f(A_2), f(g(A_2))))), file('unknown', unknown)).
% 2.88/1.79 tff(f_37, axiom, (![A_3]: ((~E(0, f(A_3)) | ~E(0, f(g(A_3)))) | E(f(A_3), f(g(A_3))))), file('unknown', unknown)).
% 2.88/1.79 tff(c_8, plain, (![A_4]: (LE(f(A_4), s(0)) | E(s(0), f(A_4)))), inference(cnfTransformation, [status(thm)], [f_41])).
% 2.88/1.79 tff(c_20, plain, (![A_2_11]: (iLEQ(A_2_11, g(A_2_11)))), inference(cnfTransformation, [status(thm)], [f_69])).
% 2.88/1.79 tff(c_10, plain, (![A_3_5]: (~LE(f(A_3_5), 0))), inference(cnfTransformation, [status(thm)], [f_44])).
% 2.88/1.79 tff(c_12, plain, (![B_0_7, A_1_6]: (LE(f(B_0_7), 0) | E(0, f(B_0_7)) | ~iLEQ(A_1_6, B_0_7) | ~LE(f(A_1_6), s(0)))), inference(cnfTransformation, [status(thm)], [f_54])).
% 2.88/1.79 tff(c_37, plain, (![B_0_21, A_1_22]: (E(0, f(B_0_21)) | ~iLEQ(A_1_22, B_0_21) | ~LE(f(A_1_22), s(0)))), inference(negUnitSimplification, [status(thm)], [c_10, c_12])).
% 2.88/1.79 tff(c_54, plain, (![A_2_25]: (E(0, f(g(A_2_25))) | ~LE(f(A_2_25), s(0)))), inference(resolution, [status(thm)], [c_20, c_37])).
% 2.88/1.79 tff(c_58, plain, (![A_4]: (E(0, f(g(A_4))) | E(s(0), f(A_4)))), inference(resolution, [status(thm)], [c_8, c_54])).
% 2.88/1.79 tff(c_24, plain, (![A_2_13]: (iLEQ(A_2_13, A_2_13))), inference(cnfTransformation, [status(thm)], [f_74])).
% 2.88/1.79 tff(c_44, plain, (![A_2_23]: (E(0, f(A_2_23)) | ~LE(f(A_2_23), s(0)))), inference(resolution, [status(thm)], [c_24, c_37])).
% 2.88/1.79 tff(c_49, plain, (![A_24]: (E(0, f(A_24)) | E(s(0), f(A_24)))), inference(resolution, [status(thm)], [c_8, c_44])).
% 2.88/1.79 tff(c_22, plain, (![A_2_12]: (~E(f(A_2_12), f(g(A_2_12))))), inference(cnfTransformation, [status(thm)], [f_72])).
% 2.88/1.79 tff(c_14, plain, (![A_2_8]: (E(f(A_2_8), f(g(A_2_8))) | ~E(s(0), f(g(A_2_8))) | ~E(s(0), f(A_2_8)))), inference(cnfTransformation, [status(thm)], [f_62])).
% 2.88/1.79 tff(c_26, plain, (![A_2_8]: (~E(s(0), f(g(A_2_8))) | ~E(s(0), f(A_2_8)))), inference(negUnitSimplification, [status(thm)], [c_22, c_14])).
% 2.88/1.79 tff(c_64, plain, (![A_2_27]: (~E(s(0), f(A_2_27)) | E(0, f(g(A_2_27))))), inference(resolution, [status(thm)], [c_49, c_26])).
% 2.88/1.79 tff(c_71, plain, (![A_4]: (E(0, f(g(A_4))))), inference(resolution, [status(thm)], [c_58, c_64])).
% 2.88/1.79 tff(c_6, plain, (![A_3_3]: (E(f(A_3_3), f(g(A_3_3))) | ~E(0, f(g(A_3_3))) | ~E(0, f(A_3_3)))), inference(cnfTransformation, [status(thm)], [f_37])).
% 2.88/1.79 tff(c_28, plain, (![A_3_3]: (~E(0, f(g(A_3_3))) | ~E(0, f(A_3_3)))), inference(negUnitSimplification, [status(thm)], [c_22, c_6])).
% 2.88/1.79 tff(c_77, plain, (![A_3_3]: (~E(0, f(A_3_3)))), inference(demodulation, [status(thm), theory('equality')], [c_71, c_28])).
% 2.88/1.79 tff(c_83, plain, $false, inference(negUnitSimplification, [status(thm)], [c_77, c_71])).
% 2.88/1.79 % SZS output end CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------