%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SYO650-1 : TPTP v9.0.0. Released v7.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 : n015.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:02 PM UTC 2025
% Result : Unsatisfiable 13.39s 4.27s
% Output : CNFRefutation 13.54s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.13 % Problem : SYO650-1 : TPTP v9.0.0. Released v7.3.0.
% 0.08/0.14 % 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.36 % Computer : n015.cluster.edu
% 0.14/0.36 % Model : x86_64 x86_64
% 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.36 % Memory : 8042.1875MB
% 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 300
% 0.14/0.36 % DateTime : Wed Apr 9 09:41:05 EDT 2025
% 0.14/0.36 % CPUTime :
% 13.39/4.27 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 13.39/4.28
% 13.39/4.28 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 13.39/4.28 %$ iLEQ > LE > E > #nlpp > suc > s > f > z > 0
% 13.39/4.28
% 13.39/4.28 %Foreground sorts:
% 13.39/4.28
% 13.39/4.28
% 13.39/4.28 %Background operators:
% 13.39/4.28
% 13.39/4.28
% 13.39/4.28 %Foreground operators:
% 13.39/4.28 tff(iLEQ, type, iLEQ: ($i * $i) > $o).
% 13.39/4.28 tff(s, type, s: $i > $i).
% 13.39/4.28 tff(f, type, f: $i > $i).
% 13.39/4.28 tff(0, type, 0: $i).
% 13.39/4.28 tff(LE, type, LE: ($i * $i) > $o).
% 13.39/4.28 tff(suc, type, suc: $i > $i).
% 13.39/4.28 tff(z, type, z: $i).
% 13.39/4.28 tff(E, type, E: ($i * $i) > $o).
% 13.39/4.28
% 13.54/4.31 tff(f_396, axiom, (![A]: LE(f(A), s(0))), file('unknown', unknown)).
% 13.54/4.31 tff(f_292, axiom, (![B_5]: ((~LE(f(B_5), s(0)) | E(0, f(B_5))) | LE(f(B_5), 0))), file('unknown', unknown)).
% 13.54/4.31 tff(f_1027, axiom, ~LE(f(z), 0), file('unknown', unknown)).
% 13.54/4.31 tff(f_712, axiom, (![B_5]: ((~LE(f(suc(B_5)), s(0)) | E(0, f(suc(B_5)))) | LE(f(B_5), 0))), file('unknown', unknown)).
% 13.54/4.31 tff(f_403, axiom, (![B_5]: ((~LE(f(suc(suc(B_5))), s(0)) | E(0, f(suc(suc(B_5))))) | LE(f(B_5), 0))), file('unknown', unknown)).
% 13.54/4.31 tff(f_1261, axiom, (![A_1]: (((~E(0, f(A_1)) | ~E(0, f(suc(A_1)))) | E(f(A_1), f(suc(A_1)))) | iLEQ(suc(A_1), suc(A_1)))), file('unknown', unknown)).
% 13.54/4.31 tff(f_801, axiom, (![B_5]: ((~LE(f(suc(suc(suc(B_5)))), s(0)) | E(0, f(suc(suc(suc(B_5)))))) | LE(f(B_5), 0))), file('unknown', unknown)).
% 13.54/4.31 tff(f_973, axiom, (![A_1]: (((((~E(0, f(suc(suc(A_1)))) | ~E(0, f(suc(A_1)))) | ~E(f(A_1), f(suc(A_1)))) | ~E(0, f(A_1))) | E(f(A_1), f(suc(suc(A_1))))) | iLEQ(suc(A_1), suc(A_1)))), file('unknown', unknown)).
% 13.54/4.31 tff(f_519, axiom, (![A_1]: ((((((~E(0, f(suc(suc(suc(A_1))))) | ~E(0, f(suc(A_1)))) | ~E(0, f(suc(suc(A_1))))) | ~E(0, f(A_1))) | ~E(f(A_1), f(suc(suc(A_1))))) | ~E(f(A_1), f(suc(A_1)))) | iLEQ(suc(A_1), suc(A_1)))), file('unknown', unknown)).
% 13.54/4.31 tff(f_794, axiom, (![A_1, B_6, B_7]: ((((((((((~iLEQ(suc(A_1), suc(B_6)) | ~E(0, f(suc(B_7)))) | ~E(0, f(suc(A_1)))) | ~E(0, f(A_1))) | ~iLEQ(suc(B_6), suc(B_7))) | ~E(0, f(B_6))) | ~E(0, f(B_7))) | ~E(0, f(suc(B_6)))) | E(f(A_1), f(suc(A_1)))) | E(f(B_6), f(suc(B_6)))) | E(f(B_7), f(suc(B_7))))), file('unknown', unknown)).
% 13.54/4.31 tff(f_567, axiom, (![B_6, A_1, B_7]: ((((((((((((((((~E(0, f(suc(suc(B_6)))) | ~iLEQ(suc(A_1), suc(B_6))) | ~E(0, f(suc(B_7)))) | ~E(0, f(suc(A_1)))) | ~E(f(B_7), f(suc(B_7)))) | ~E(0, f(suc(suc(A_1))))) | ~E(0, f(A_1))) | ~E(0, f(suc(suc(B_7))))) | ~iLEQ(suc(B_6), suc(B_7))) | ~E(f(A_1), f(suc(A_1)))) | ~E(0, f(B_6))) | ~E(0, f(B_7))) | ~E(f(B_6), f(suc(B_6)))) | ~E(0, f(suc(B_6)))) | E(f(A_1), f(suc(suc(A_1))))) | E(f(B_6), f(suc(suc(B_6))))) | E(f(B_7), f(suc(suc(B_7)))))), file('unknown', unknown)).
% 13.54/4.31 tff(f_907, axiom, (![A_1, B_6, B_7]: (((((((((((((((((((~E(0, f(suc(suc(suc(A_1))))) | ~E(0, f(suc(suc(B_6))))) | ~iLEQ(suc(A_1), suc(B_6))) | ~E(0, f(suc(B_7)))) | ~E(0, f(suc(A_1)))) | ~E(f(B_7), f(suc(B_7)))) | ~E(0, f(suc(suc(A_1))))) | ~E(0, f(A_1))) | ~E(0, f(suc(suc(B_7))))) | ~E(0, f(suc(suc(suc(B_6)))))) | ~E(f(A_1), f(suc(suc(A_1))))) | ~iLEQ(suc(B_6), suc(B_7))) | ~E(f(A_1), f(suc(A_1)))) | ~E(0, f(B_6))) | ~E(f(B_7), f(suc(suc(B_7))))) | ~E(f(B_6), f(suc(suc(B_6))))) | ~E(0, f(suc(suc(suc(B_7)))))) | ~E(0, f(B_7))) | ~E(f(B_6), f(suc(B_6)))) | ~E(0, f(suc(B_6))))), file('unknown', unknown)).
% 13.54/4.31 tff(c_20, plain, (![A_26]: (LE(f(A_26), s(0)))), inference(cnfTransformation, [status(thm)], [f_396])).
% 13.54/4.31 tff(c_14, plain, (![B_5_19]: (LE(f(B_5_19), 0) | E(0, f(B_5_19)) | ~LE(f(B_5_19), s(0)))), inference(cnfTransformation, [status(thm)], [f_292])).
% 13.54/4.31 tff(c_82, plain, (![B_5_91]: (LE(f(B_5_91), 0) | E(0, f(B_5_91)))), inference(demodulation, [status(thm), theory('equality')], [c_20, c_14])).
% 13.54/4.31 tff(c_56, plain, (~LE(f(z), 0)), inference(cnfTransformation, [status(thm)], [f_1027])).
% 13.54/4.31 tff(c_86, plain, (E(0, f(z))), inference(resolution, [status(thm)], [c_82, c_56])).
% 13.54/4.31 tff(c_38, plain, (![B_5_47]: (LE(f(B_5_47), 0) | E(0, f(suc(B_5_47))) | ~LE(f(suc(B_5_47)), s(0)))), inference(cnfTransformation, [status(thm)], [f_712])).
% 13.54/4.31 tff(c_74, plain, (![B_5_47]: (LE(f(B_5_47), 0) | E(0, f(suc(B_5_47))))), inference(demodulation, [status(thm), theory('equality')], [c_20, c_38])).
% 13.54/4.31 tff(c_22, plain, (![B_5_27]: (LE(f(B_5_27), 0) | E(0, f(suc(suc(B_5_27)))) | ~LE(f(suc(suc(B_5_27))), s(0)))), inference(cnfTransformation, [status(thm)], [f_403])).
% 13.54/4.31 tff(c_76, plain, (![B_5_27]: (LE(f(B_5_27), 0) | E(0, f(suc(suc(B_5_27)))))), inference(demodulation, [status(thm), theory('equality')], [c_20, c_22])).
% 13.54/4.31 tff(c_68, plain, (![A_1_83]: (iLEQ(suc(A_1_83), suc(A_1_83)) | E(f(A_1_83), f(suc(A_1_83))) | ~E(0, f(suc(A_1_83))) | ~E(0, f(A_1_83)))), inference(cnfTransformation, [status(thm)], [f_1261])).
% 13.54/4.31 tff(c_44, plain, (![B_5_54]: (LE(f(B_5_54), 0) | E(0, f(suc(suc(suc(B_5_54))))) | ~LE(f(suc(suc(suc(B_5_54)))), s(0)))), inference(cnfTransformation, [status(thm)], [f_801])).
% 13.54/4.31 tff(c_78, plain, (![B_5_54]: (LE(f(B_5_54), 0) | E(0, f(suc(suc(suc(B_5_54))))))), inference(demodulation, [status(thm), theory('equality')], [c_20, c_44])).
% 13.54/4.31 tff(c_52, plain, (![A_1_64]: (iLEQ(suc(A_1_64), suc(A_1_64)) | E(f(A_1_64), f(suc(suc(A_1_64)))) | ~E(0, f(A_1_64)) | ~E(f(A_1_64), f(suc(A_1_64))) | ~E(0, f(suc(A_1_64))) | ~E(0, f(suc(suc(A_1_64)))))), inference(cnfTransformation, [status(thm)], [f_973])).
% 13.54/4.31 tff(c_92, plain, (![A_1_97]: (iLEQ(suc(A_1_97), suc(A_1_97)) | ~E(f(A_1_97), f(suc(A_1_97))) | ~E(f(A_1_97), f(suc(suc(A_1_97)))) | ~E(0, f(A_1_97)) | ~E(0, f(suc(suc(A_1_97)))) | ~E(0, f(suc(A_1_97))) | ~E(0, f(suc(suc(suc(A_1_97))))))), inference(cnfTransformation, [status(thm)], [f_519])).
% 13.54/4.31 tff(c_97, plain, (![A_1_98]: (~E(0, f(suc(suc(suc(A_1_98))))) | iLEQ(suc(A_1_98), suc(A_1_98)) | ~E(0, f(A_1_98)) | ~E(f(A_1_98), f(suc(A_1_98))) | ~E(0, f(suc(A_1_98))) | ~E(0, f(suc(suc(A_1_98)))))), inference(resolution, [status(thm)], [c_52, c_92])).
% 13.54/4.31 tff(c_109, plain, (![B_5_99]: (iLEQ(suc(B_5_99), suc(B_5_99)) | ~E(0, f(B_5_99)) | ~E(f(B_5_99), f(suc(B_5_99))) | ~E(0, f(suc(B_5_99))) | ~E(0, f(suc(suc(B_5_99)))) | LE(f(B_5_99), 0))), inference(resolution, [status(thm)], [c_78, c_97])).
% 13.54/4.31 tff(c_114, plain, (![A_1_100]: (~E(0, f(suc(suc(A_1_100)))) | LE(f(A_1_100), 0) | iLEQ(suc(A_1_100), suc(A_1_100)) | ~E(0, f(suc(A_1_100))) | ~E(0, f(A_1_100)))), inference(resolution, [status(thm)], [c_68, c_109])).
% 13.54/4.31 tff(c_123, plain, (![B_5_27]: (iLEQ(suc(B_5_27), suc(B_5_27)) | ~E(0, f(suc(B_5_27))) | ~E(0, f(B_5_27)) | LE(f(B_5_27), 0))), inference(resolution, [status(thm)], [c_76, c_114])).
% 13.54/4.31 tff(c_126, plain, (![B_7_102, B_6_103, A_1_104]: (E(f(B_7_102), f(suc(B_7_102))) | E(f(B_6_103), f(suc(B_6_103))) | E(f(A_1_104), f(suc(A_1_104))) | ~E(0, f(suc(B_6_103))) | ~E(0, f(B_7_102)) | ~E(0, f(B_6_103)) | ~iLEQ(suc(B_6_103), suc(B_7_102)) | ~E(0, f(A_1_104)) | ~E(0, f(suc(A_1_104))) | ~E(0, f(suc(B_7_102))) | ~iLEQ(suc(A_1_104), suc(B_6_103)))), inference(cnfTransformation, [status(thm)], [f_794])).
% 13.54/4.31 tff(c_168, plain, (![B_5_113, A_1_114]: (E(f(B_5_113), f(suc(B_5_113))) | E(f(A_1_114), f(suc(A_1_114))) | ~E(0, f(A_1_114)) | ~E(0, f(suc(A_1_114))) | ~iLEQ(suc(A_1_114), suc(B_5_113)) | ~E(0, f(suc(B_5_113))) | ~E(0, f(B_5_113)) | LE(f(B_5_113), 0))), inference(resolution, [status(thm)], [c_123, c_126])).
% 13.54/4.31 tff(c_177, plain, (![B_5_27]: (E(f(B_5_27), f(suc(B_5_27))) | ~E(0, f(suc(B_5_27))) | ~E(0, f(B_5_27)) | LE(f(B_5_27), 0))), inference(resolution, [status(thm)], [c_123, c_168])).
% 13.54/4.31 tff(c_335, plain, (![B_7_170, B_6_171, A_1_172]: (E(f(B_7_170), f(suc(suc(B_7_170)))) | E(f(B_6_171), f(suc(suc(B_6_171)))) | E(f(A_1_172), f(suc(suc(A_1_172)))) | ~E(0, f(suc(B_6_171))) | ~E(f(B_6_171), f(suc(B_6_171))) | ~E(0, f(B_7_170)) | ~E(0, f(B_6_171)) | ~E(f(A_1_172), f(suc(A_1_172))) | ~iLEQ(suc(B_6_171), suc(B_7_170)) | ~E(0, f(suc(suc(B_7_170)))) | ~E(0, f(A_1_172)) | ~E(0, f(suc(suc(A_1_172)))) | ~E(f(B_7_170), f(suc(B_7_170))) | ~E(0, f(suc(A_1_172))) | ~E(0, f(suc(B_7_170))) | ~iLEQ(suc(A_1_172), suc(B_6_171)) | ~E(0, f(suc(suc(B_6_171)))))), inference(cnfTransformation, [status(thm)], [f_567])).
% 13.54/4.31 tff(c_345, plain, (![B_5_173, A_1_174]: (E(f(B_5_173), f(suc(suc(B_5_173)))) | E(f(A_1_174), f(suc(suc(A_1_174)))) | ~E(f(A_1_174), f(suc(A_1_174))) | ~E(0, f(A_1_174)) | ~E(0, f(suc(suc(A_1_174)))) | ~E(f(B_5_173), f(suc(B_5_173))) | ~E(0, f(suc(A_1_174))) | ~iLEQ(suc(A_1_174), suc(B_5_173)) | ~E(0, f(suc(suc(B_5_173)))) | ~E(0, f(suc(B_5_173))) | ~E(0, f(B_5_173)) | LE(f(B_5_173), 0))), inference(resolution, [status(thm)], [c_123, c_335])).
% 13.54/4.31 tff(c_354, plain, (![B_5_27]: (E(f(B_5_27), f(suc(suc(B_5_27)))) | ~E(f(B_5_27), f(suc(B_5_27))) | ~E(0, f(suc(suc(B_5_27)))) | ~E(0, f(suc(B_5_27))) | ~E(0, f(B_5_27)) | LE(f(B_5_27), 0))), inference(resolution, [status(thm)], [c_123, c_345])).
% 13.54/4.31 tff(c_750, plain, (![B_6_266, B_7_267, A_1_268]: (~E(0, f(suc(B_6_266))) | ~E(f(B_6_266), f(suc(B_6_266))) | ~E(0, f(B_7_267)) | ~E(0, f(suc(suc(suc(B_7_267))))) | ~E(f(B_6_266), f(suc(suc(B_6_266)))) | ~E(f(B_7_267), f(suc(suc(B_7_267)))) | ~E(0, f(B_6_266)) | ~E(f(A_1_268), f(suc(A_1_268))) | ~iLEQ(suc(B_6_266), suc(B_7_267)) | ~E(f(A_1_268), f(suc(suc(A_1_268)))) | ~E(0, f(suc(suc(suc(B_6_266))))) | ~E(0, f(suc(suc(B_7_267)))) | ~E(0, f(A_1_268)) | ~E(0, f(suc(suc(A_1_268)))) | ~E(f(B_7_267), f(suc(B_7_267))) | ~E(0, f(suc(A_1_268))) | ~E(0, f(suc(B_7_267))) | ~iLEQ(suc(A_1_268), suc(B_6_266)) | ~E(0, f(suc(suc(B_6_266)))) | ~E(0, f(suc(suc(suc(A_1_268))))))), inference(cnfTransformation, [status(thm)], [f_907])).
% 13.54/4.31 tff(c_1534, plain, (![B_7_465, A_1_466, B_5_467]: (~E(0, f(B_7_465)) | ~E(0, f(suc(suc(suc(B_7_465))))) | ~E(f(B_7_465), f(suc(suc(B_7_465)))) | ~E(f(A_1_466), f(suc(A_1_466))) | ~iLEQ(suc(B_5_467), suc(B_7_465)) | ~E(f(A_1_466), f(suc(suc(A_1_466)))) | ~E(0, f(suc(suc(suc(B_5_467))))) | ~E(0, f(suc(suc(B_7_465)))) | ~E(0, f(A_1_466)) | ~E(0, f(suc(suc(A_1_466)))) | ~E(f(B_7_465), f(suc(B_7_465))) | ~E(0, f(suc(A_1_466))) | ~E(0, f(suc(B_7_465))) | ~iLEQ(suc(A_1_466), suc(B_5_467)) | ~E(0, f(suc(suc(suc(A_1_466))))) | ~E(f(B_5_467), f(suc(B_5_467))) | ~E(0, f(suc(suc(B_5_467)))) | ~E(0, f(suc(B_5_467))) | ~E(0, f(B_5_467)) | LE(f(B_5_467), 0))), inference(resolution, [status(thm)], [c_354, c_750])).
% 13.54/4.31 tff(c_1850, plain, (![B_5_530, A_1_531, B_5_532]: (~E(0, f(suc(suc(suc(B_5_530))))) | ~E(f(A_1_531), f(suc(A_1_531))) | ~iLEQ(suc(B_5_532), suc(B_5_530)) | ~E(f(A_1_531), f(suc(suc(A_1_531)))) | ~E(0, f(suc(suc(suc(B_5_532))))) | ~E(0, f(A_1_531)) | ~E(0, f(suc(suc(A_1_531)))) | ~E(0, f(suc(A_1_531))) | ~iLEQ(suc(A_1_531), suc(B_5_532)) | ~E(0, f(suc(suc(suc(A_1_531))))) | ~E(f(B_5_532), f(suc(B_5_532))) | ~E(0, f(suc(suc(B_5_532)))) | ~E(0, f(suc(B_5_532))) | ~E(0, f(B_5_532)) | LE(f(B_5_532), 0) | ~E(f(B_5_530), f(suc(B_5_530))) | ~E(0, f(suc(suc(B_5_530)))) | ~E(0, f(suc(B_5_530))) | ~E(0, f(B_5_530)) | LE(f(B_5_530), 0))), inference(resolution, [status(thm)], [c_354, c_1534])).
% 13.54/4.31 tff(c_1911, plain, (![A_1_541, B_5_542, B_5_543]: (~E(f(A_1_541), f(suc(A_1_541))) | ~iLEQ(suc(B_5_542), suc(B_5_543)) | ~E(f(A_1_541), f(suc(suc(A_1_541)))) | ~E(0, f(suc(suc(suc(B_5_542))))) | ~E(0, f(A_1_541)) | ~E(0, f(suc(suc(A_1_541)))) | ~E(0, f(suc(A_1_541))) | ~iLEQ(suc(A_1_541), suc(B_5_542)) | ~E(0, f(suc(suc(suc(A_1_541))))) | ~E(f(B_5_542), f(suc(B_5_542))) | ~E(0, f(suc(suc(B_5_542)))) | ~E(0, f(suc(B_5_542))) | ~E(0, f(B_5_542)) | LE(f(B_5_542), 0) | ~E(f(B_5_543), f(suc(B_5_543))) | ~E(0, f(suc(suc(B_5_543)))) | ~E(0, f(suc(B_5_543))) | ~E(0, f(B_5_543)) | LE(f(B_5_543), 0))), inference(resolution, [status(thm)], [c_78, c_1850])).
% 13.54/4.31 tff(c_1918, plain, (![A_1_544, B_5_545]: (~E(f(A_1_544), f(suc(A_1_544))) | ~E(f(A_1_544), f(suc(suc(A_1_544)))) | ~E(0, f(suc(suc(suc(B_5_545))))) | ~E(0, f(A_1_544)) | ~E(0, f(suc(suc(A_1_544)))) | ~E(0, f(suc(A_1_544))) | ~iLEQ(suc(A_1_544), suc(B_5_545)) | ~E(0, f(suc(suc(suc(A_1_544))))) | ~E(f(B_5_545), f(suc(B_5_545))) | ~E(0, f(suc(suc(B_5_545)))) | ~E(0, f(suc(B_5_545))) | ~E(0, f(B_5_545)) | LE(f(B_5_545), 0))), inference(resolution, [status(thm)], [c_123, c_1911])).
% 13.54/4.31 tff(c_1928, plain, (![B_5_546, B_5_547]: (~E(0, f(suc(suc(suc(B_5_546))))) | ~iLEQ(suc(B_5_547), suc(B_5_546)) | ~E(0, f(suc(suc(suc(B_5_547))))) | ~E(f(B_5_546), f(suc(B_5_546))) | ~E(0, f(suc(suc(B_5_546)))) | ~E(0, f(suc(B_5_546))) | ~E(0, f(B_5_546)) | LE(f(B_5_546), 0) | ~E(f(B_5_547), f(suc(B_5_547))) | ~E(0, f(suc(suc(B_5_547)))) | ~E(0, f(suc(B_5_547))) | ~E(0, f(B_5_547)) | LE(f(B_5_547), 0))), inference(resolution, [status(thm)], [c_354, c_1918])).
% 13.54/4.31 tff(c_1940, plain, (![B_5_548, B_5_549]: (~iLEQ(suc(B_5_548), suc(B_5_549)) | ~E(0, f(suc(suc(suc(B_5_548))))) | ~E(f(B_5_549), f(suc(B_5_549))) | ~E(0, f(suc(suc(B_5_549)))) | ~E(0, f(suc(B_5_549))) | ~E(0, f(B_5_549)) | ~E(f(B_5_548), f(suc(B_5_548))) | ~E(0, f(suc(suc(B_5_548)))) | ~E(0, f(suc(B_5_548))) | ~E(0, f(B_5_548)) | LE(f(B_5_548), 0) | LE(f(B_5_549), 0))), inference(resolution, [status(thm)], [c_78, c_1928])).
% 13.54/4.31 tff(c_1947, plain, (![B_5_550]: (~E(0, f(suc(suc(suc(B_5_550))))) | ~E(f(B_5_550), f(suc(B_5_550))) | ~E(0, f(suc(suc(B_5_550)))) | ~E(0, f(suc(B_5_550))) | ~E(0, f(B_5_550)) | LE(f(B_5_550), 0))), inference(resolution, [status(thm)], [c_123, c_1940])).
% 13.54/4.31 tff(c_1959, plain, (![B_5_551]: (~E(f(B_5_551), f(suc(B_5_551))) | ~E(0, f(suc(suc(B_5_551)))) | ~E(0, f(suc(B_5_551))) | ~E(0, f(B_5_551)) | LE(f(B_5_551), 0))), inference(resolution, [status(thm)], [c_78, c_1947])).
% 13.54/4.31 tff(c_1972, plain, (![B_5_552]: (~E(0, f(suc(suc(B_5_552)))) | ~E(0, f(suc(B_5_552))) | ~E(0, f(B_5_552)) | LE(f(B_5_552), 0))), inference(resolution, [status(thm)], [c_177, c_1959])).
% 13.54/4.31 tff(c_1985, plain, (![B_5_553]: (~E(0, f(suc(B_5_553))) | ~E(0, f(B_5_553)) | LE(f(B_5_553), 0))), inference(resolution, [status(thm)], [c_76, c_1972])).
% 13.54/4.31 tff(c_1998, plain, (![B_5_554]: (~E(0, f(B_5_554)) | LE(f(B_5_554), 0))), inference(resolution, [status(thm)], [c_74, c_1985])).
% 13.54/4.31 tff(c_2001, plain, (~E(0, f(z))), inference(resolution, [status(thm)], [c_1998, c_56])).
% 13.54/4.31 tff(c_2005, plain, $false, inference(demodulation, [status(thm), theory('equality')], [c_86, c_2001])).
% 13.54/4.31 % SZS output end CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------