%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SYO646-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 : n009.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 17.59s 5.82s
% Output : CNFRefutation 17.59s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.13 % Problem : SYO646-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.35 % Computer : n009.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Wed Apr 9 09:40:11 EDT 2025
% 0.14/0.36 % CPUTime :
% 17.59/5.82 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 17.59/5.82
% 17.59/5.82 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 17.59/5.84 %$ iLEQ > E > #nlpp > suc > f > 0
% 17.59/5.84
% 17.59/5.84 %Foreground sorts:
% 17.59/5.84
% 17.59/5.84
% 17.59/5.84 %Background operators:
% 17.59/5.84
% 17.59/5.84
% 17.59/5.84 %Foreground operators:
% 17.59/5.84 tff(iLEQ, type, iLEQ: ($i * $i) > $o).
% 17.59/5.84 tff(f, type, f: $i > $i).
% 17.59/5.84 tff(0, type, 0: $i).
% 17.59/5.84 tff(suc, type, suc: $i > $i).
% 17.59/5.84 tff(E, type, E: ($i * $i) > $o).
% 17.59/5.84
% 17.59/5.86 tff(f_10609, axiom, (![A]: E(0, f(A))), file('unknown', unknown)).
% 17.59/5.86 tff(f_9683, axiom, (![A_0]: (((~E(0, f(A_0)) | ~E(0, f(suc(A_0)))) | E(f(A_0), f(suc(A_0)))) | iLEQ(suc(A_0), suc(A_0)))), file('unknown', unknown)).
% 17.59/5.86 tff(f_11709, axiom, (![A_0]: (((((~E(0, f(suc(suc(A_0)))) | ~E(0, f(suc(A_0)))) | ~E(f(A_0), f(suc(A_0)))) | ~E(0, f(A_0))) | E(f(A_0), f(suc(suc(A_0))))) | iLEQ(suc(A_0), suc(A_0)))), file('unknown', unknown)).
% 17.59/5.86 tff(f_7281, axiom, (![A_0]: ((((((~E(0, f(suc(suc(A_0)))) | ~E(f(A_0), f(suc(suc(A_0))))) | ~E(0, f(suc(suc(suc(A_0)))))) | ~E(f(A_0), f(suc(A_0)))) | ~E(0, f(suc(A_0)))) | ~E(0, f(A_0))) | iLEQ(suc(A_0), suc(A_0)))), file('unknown', unknown)).
% 17.59/5.86 tff(f_18865, axiom, (![B, A_0, B_0, B_2, B_1]: ((((((((((((((((((~iLEQ(suc(B_1), suc(B_2)) | ~iLEQ(suc(B_0), suc(B_1))) | ~E(0, f(B_1))) | ~iLEQ(suc(A_0), suc(B))) | ~E(0, f(suc(B_0)))) | ~E(0, f(suc(B_2)))) | ~E(0, f(B_0))) | ~E(0, f(B_2))) | ~E(0, f(suc(A_0)))) | ~E(0, f(B))) | ~E(0, f(suc(B)))) | ~E(0, f(suc(B_1)))) | ~E(0, f(A_0))) | ~iLEQ(suc(B), suc(B_0))) | E(f(B_1), f(suc(B_1)))) | E(f(B_0), f(suc(B_0)))) | E(f(B), f(suc(B)))) | E(f(B_2), f(suc(B_2)))) | E(f(A_0), f(suc(A_0))))), file('unknown', unknown)).
% 17.59/5.86 tff(f_9093, axiom, (![B, A_0, B_0, B_2, B_1]: ((((((((((((((((((((((((((((~E(f(B_1), f(suc(B_1))) | ~iLEQ(suc(B_1), suc(B_2))) | ~E(0, f(suc(suc(A_0))))) | ~iLEQ(suc(B_0), suc(B_1))) | ~E(0, f(B_1))) | ~E(0, f(suc(suc(B_0))))) | ~E(f(B_0), f(suc(B_0)))) | ~E(f(B), f(suc(B)))) | ~iLEQ(suc(A_0), suc(B))) | ~E(0, f(suc(B_0)))) | ~E(0, f(suc(B_2)))) | ~E(f(B_2), f(suc(B_2)))) | ~E(f(A_0), f(suc(A_0)))) | ~E(0, f(B_0))) | ~E(0, f(B_2))) | ~E(0, f(suc(A_0)))) | ~E(0, f(B))) | ~E(0, f(suc(suc(B))))) | ~E(0, f(suc(B)))) | ~E(0, f(suc(B_1)))) | ~E(0, f(suc(suc(B_2))))) | ~E(0, f(suc(suc(B_1))))) | ~E(0, f(A_0))) | ~iLEQ(suc(B), suc(B_0))) | E(f(B_2), f(suc(suc(B_2))))) | E(f(A_0), f(suc(suc(A_0))))) | E(f(B), f(suc(suc(B))))) | E(f(B_0), f(suc(suc(B_0))))) | E(f(B_1), f(suc(suc(B_1)))))), file('unknown', unknown)).
% 17.59/5.86 tff(f_2513, axiom, (![B, A_0, B_0, B_2, B_1]: (((((((((((((((((((((((((((((((((~E(0, f(suc(suc(suc(B_2))))) | ~E(f(B_2), f(suc(suc(B_2))))) | ~E(f(B_1), f(suc(B_1)))) | ~iLEQ(suc(B_1), suc(B_2))) | ~E(0, f(suc(suc(A_0))))) | ~iLEQ(suc(B_0), suc(B_1))) | ~E(0, f(B_1))) | ~E(0, f(suc(suc(B_0))))) | ~E(0, f(suc(suc(suc(B_0)))))) | ~E(f(B_0), f(suc(B_0)))) | ~E(0, f(suc(suc(suc(B)))))) | ~E(f(B), f(suc(B)))) | ~iLEQ(suc(A_0), suc(B))) | ~E(f(A_0), f(suc(suc(A_0))))) | ~E(0, f(suc(B_0)))) | ~E(0, f(suc(B_2)))) | ~E(0, f(suc(suc(suc(A_0)))))) | ~E(f(B_2), f(suc(B_2)))) | ~E(f(A_0), f(suc(A_0)))) | ~E(0, f(B_0))) | ~E(0, f(B_2))) | ~E(0, f(suc(A_0)))) | ~E(0, f(B))) | ~E(0, f(suc(suc(B))))) | ~E(f(B), f(suc(suc(B))))) | ~E(0, f(suc(suc(suc(B_1)))))) | ~E(0, f(suc(B)))) | ~E(0, f(suc(B_1)))) | ~E(0, f(suc(suc(B_2))))) | ~E(0, f(suc(suc(B_1))))) | ~E(0, f(A_0))) | ~E(f(B_0), f(suc(suc(B_0))))) | ~iLEQ(suc(B), suc(B_0))) | ~E(f(B_1), f(suc(suc(B_1)))))), file('unknown', unknown)).
% 17.59/5.86 tff(c_274, plain, (![A_673]: (E(0, f(A_673)))), inference(cnfTransformation, [status(thm)], [f_10609])).
% 17.59/5.86 tff(c_248, plain, (![A_0_612]: (iLEQ(suc(A_0_612), suc(A_0_612)) | E(f(A_0_612), f(suc(A_0_612))) | ~E(0, f(suc(A_0_612))) | ~E(0, f(A_0_612)))), inference(cnfTransformation, [status(thm)], [f_9683])).
% 17.59/5.86 tff(c_740, plain, (![A_0_612]: (iLEQ(suc(A_0_612), suc(A_0_612)) | E(f(A_0_612), f(suc(A_0_612))))), inference(demodulation, [status(thm), theory('equality')], [c_274, c_274, c_248])).
% 17.59/5.86 tff(c_302, plain, (![A_0_739]: (iLEQ(suc(A_0_739), suc(A_0_739)) | E(f(A_0_739), f(suc(suc(A_0_739)))) | ~E(0, f(A_0_739)) | ~E(f(A_0_739), f(suc(A_0_739))) | ~E(0, f(suc(A_0_739))) | ~E(0, f(suc(suc(A_0_739)))))), inference(cnfTransformation, [status(thm)], [f_11709])).
% 17.59/5.86 tff(c_496, plain, (![A_0_739]: (iLEQ(suc(A_0_739), suc(A_0_739)) | E(f(A_0_739), f(suc(suc(A_0_739)))) | ~E(f(A_0_739), f(suc(A_0_739))))), inference(demodulation, [status(thm), theory('equality')], [c_274, c_274, c_274, c_302])).
% 17.59/5.86 tff(c_186, plain, (![A_0_461]: (iLEQ(suc(A_0_461), suc(A_0_461)) | ~E(0, f(A_0_461)) | ~E(0, f(suc(A_0_461))) | ~E(f(A_0_461), f(suc(A_0_461))) | ~E(0, f(suc(suc(suc(A_0_461))))) | ~E(f(A_0_461), f(suc(suc(A_0_461)))) | ~E(0, f(suc(suc(A_0_461)))))), inference(cnfTransformation, [status(thm)], [f_7281])).
% 17.59/5.86 tff(c_990, plain, (![A_0_1223]: (iLEQ(suc(A_0_1223), suc(A_0_1223)) | ~E(f(A_0_1223), f(suc(A_0_1223))) | ~E(f(A_0_1223), f(suc(suc(A_0_1223)))))), inference(demodulation, [status(thm), theory('equality')], [c_274, c_274, c_274, c_274, c_186])).
% 17.59/5.86 tff(c_995, plain, (![A_0_1224]: (iLEQ(suc(A_0_1224), suc(A_0_1224)) | ~E(f(A_0_1224), f(suc(A_0_1224))))), inference(resolution, [status(thm)], [c_496, c_990])).
% 17.59/5.86 tff(c_999, plain, (![A_0_612]: (iLEQ(suc(A_0_612), suc(A_0_612)))), inference(resolution, [status(thm)], [c_740, c_995])).
% 17.59/5.86 tff(c_1003, plain, (![A_0_1230]: (iLEQ(suc(A_0_1230), suc(A_0_1230)))), inference(resolution, [status(thm)], [c_740, c_995])).
% 17.59/5.86 tff(c_486, plain, (![A_0_1196, B_1195, B_2_1198, B_1_1199, B_0_1197]: (E(f(A_0_1196), f(suc(A_0_1196))) | E(f(B_2_1198), f(suc(B_2_1198))) | E(f(B_1195), f(suc(B_1195))) | E(f(B_0_1197), f(suc(B_0_1197))) | E(f(B_1_1199), f(suc(B_1_1199))) | ~iLEQ(suc(B_1195), suc(B_0_1197)) | ~E(0, f(A_0_1196)) | ~E(0, f(suc(B_1_1199))) | ~E(0, f(suc(B_1195))) | ~E(0, f(B_1195)) | ~E(0, f(suc(A_0_1196))) | ~E(0, f(B_2_1198)) | ~E(0, f(B_0_1197)) | ~E(0, f(suc(B_2_1198))) | ~E(0, f(suc(B_0_1197))) | ~iLEQ(suc(A_0_1196), suc(B_1195)) | ~E(0, f(B_1_1199)) | ~iLEQ(suc(B_0_1197), suc(B_1_1199)) | ~iLEQ(suc(B_1_1199), suc(B_2_1198)))), inference(cnfTransformation, [status(thm)], [f_18865])).
% 17.59/5.86 tff(c_500, plain, (![A_0_1196, B_1195, B_2_1198, B_1_1199, B_0_1197]: (E(f(A_0_1196), f(suc(A_0_1196))) | E(f(B_2_1198), f(suc(B_2_1198))) | E(f(B_1195), f(suc(B_1195))) | E(f(B_0_1197), f(suc(B_0_1197))) | E(f(B_1_1199), f(suc(B_1_1199))) | ~iLEQ(suc(B_1195), suc(B_0_1197)) | ~iLEQ(suc(A_0_1196), suc(B_1195)) | ~iLEQ(suc(B_0_1197), suc(B_1_1199)) | ~iLEQ(suc(B_1_1199), suc(B_2_1198)))), inference(demodulation, [status(thm), theory('equality')], [c_274, c_274, c_274, c_274, c_274, c_274, c_274, c_274, c_274, c_274, c_486])).
% 17.59/5.86 tff(c_1007, plain, (![A_0_1231, B_2_1232, A_0_1233, B_1_1234]: (E(f(A_0_1231), f(suc(A_0_1231))) | E(f(B_2_1232), f(suc(B_2_1232))) | E(f(A_0_1233), f(suc(A_0_1233))) | E(f(B_1_1234), f(suc(B_1_1234))) | ~iLEQ(suc(A_0_1231), suc(A_0_1233)) | ~iLEQ(suc(A_0_1233), suc(B_1_1234)) | ~iLEQ(suc(B_1_1234), suc(B_2_1232)))), inference(resolution, [status(thm)], [c_1003, c_500])).
% 17.59/5.86 tff(c_1011, plain, (![B_2_1235, A_0_1236, B_1_1237]: (E(f(B_2_1235), f(suc(B_2_1235))) | E(f(A_0_1236), f(suc(A_0_1236))) | E(f(B_1_1237), f(suc(B_1_1237))) | ~iLEQ(suc(A_0_1236), suc(B_1_1237)) | ~iLEQ(suc(B_1_1237), suc(B_2_1235)))), inference(resolution, [status(thm)], [c_999, c_1007])).
% 17.59/5.86 tff(c_1015, plain, (![B_2_1238, A_0_1239]: (E(f(B_2_1238), f(suc(B_2_1238))) | E(f(A_0_1239), f(suc(A_0_1239))) | ~iLEQ(suc(A_0_1239), suc(B_2_1238)))), inference(resolution, [status(thm)], [c_999, c_1011])).
% 17.59/5.86 tff(c_1018, plain, (![A_0_612]: (E(f(A_0_612), f(suc(A_0_612))))), inference(resolution, [status(thm)], [c_999, c_1015])).
% 17.59/5.86 tff(c_232, plain, (![B_1_576, B_2_575, B_572, B_0_574, A_0_573]: (E(f(B_1_576), f(suc(suc(B_1_576)))) | E(f(B_0_574), f(suc(suc(B_0_574)))) | E(f(B_572), f(suc(suc(B_572)))) | E(f(A_0_573), f(suc(suc(A_0_573)))) | E(f(B_2_575), f(suc(suc(B_2_575)))) | ~iLEQ(suc(B_572), suc(B_0_574)) | ~E(0, f(A_0_573)) | ~E(0, f(suc(suc(B_1_576)))) | ~E(0, f(suc(suc(B_2_575)))) | ~E(0, f(suc(B_1_576))) | ~E(0, f(suc(B_572))) | ~E(0, f(suc(suc(B_572)))) | ~E(0, f(B_572)) | ~E(0, f(suc(A_0_573))) | ~E(0, f(B_2_575)) | ~E(0, f(B_0_574)) | ~E(f(A_0_573), f(suc(A_0_573))) | ~E(f(B_2_575), f(suc(B_2_575))) | ~E(0, f(suc(B_2_575))) | ~E(0, f(suc(B_0_574))) | ~iLEQ(suc(A_0_573), suc(B_572)) | ~E(f(B_572), f(suc(B_572))) | ~E(f(B_0_574), f(suc(B_0_574))) | ~E(0, f(suc(suc(B_0_574)))) | ~E(0, f(B_1_576)) | ~iLEQ(suc(B_0_574), suc(B_1_576)) | ~E(0, f(suc(suc(A_0_573)))) | ~iLEQ(suc(B_1_576), suc(B_2_575)) | ~E(f(B_1_576), f(suc(B_1_576))))), inference(cnfTransformation, [status(thm)], [f_9093])).
% 17.59/5.86 tff(c_756, plain, (![B_1_576, B_2_575, B_572, B_0_574, A_0_573]: (E(f(B_1_576), f(suc(suc(B_1_576)))) | E(f(B_0_574), f(suc(suc(B_0_574)))) | E(f(B_572), f(suc(suc(B_572)))) | E(f(A_0_573), f(suc(suc(A_0_573)))) | E(f(B_2_575), f(suc(suc(B_2_575)))) | ~iLEQ(suc(B_572), suc(B_0_574)) | ~E(f(A_0_573), f(suc(A_0_573))) | ~E(f(B_2_575), f(suc(B_2_575))) | ~iLEQ(suc(A_0_573), suc(B_572)) | ~E(f(B_572), f(suc(B_572))) | ~E(f(B_0_574), f(suc(B_0_574))) | ~iLEQ(suc(B_0_574), suc(B_1_576)) | ~iLEQ(suc(B_1_576), suc(B_2_575)) | ~E(f(B_1_576), f(suc(B_1_576))))), inference(demodulation, [status(thm), theory('equality')], [c_274, c_274, c_274, c_274, c_274, c_274, c_274, c_274, c_274, c_274, c_274, c_274, c_274, c_274, c_274, c_232])).
% 17.59/5.86 tff(c_1494, plain, (![B_0_1279, B_1_1282, A_0_1283, B_1281, B_2_1280]: (E(f(B_1_1282), f(suc(suc(B_1_1282)))) | E(f(B_0_1279), f(suc(suc(B_0_1279)))) | E(f(B_1281), f(suc(suc(B_1281)))) | E(f(A_0_1283), f(suc(suc(A_0_1283)))) | E(f(B_2_1280), f(suc(suc(B_2_1280)))) | ~iLEQ(suc(B_1281), suc(B_0_1279)) | ~iLEQ(suc(A_0_1283), suc(B_1281)) | ~iLEQ(suc(B_0_1279), suc(B_1_1282)) | ~iLEQ(suc(B_1_1282), suc(B_2_1280)))), inference(demodulation, [status(thm), theory('equality')], [c_1018, c_1018, c_1018, c_1018, c_1018, c_756])).
% 17.59/5.86 tff(c_1500, plain, (![B_1_1284, A_0_1285, A_0_1286, B_2_1287]: (E(f(B_1_1284), f(suc(suc(B_1_1284)))) | E(f(A_0_1285), f(suc(suc(A_0_1285)))) | E(f(A_0_1286), f(suc(suc(A_0_1286)))) | E(f(B_2_1287), f(suc(suc(B_2_1287)))) | ~iLEQ(suc(A_0_1286), suc(A_0_1285)) | ~iLEQ(suc(A_0_1285), suc(B_1_1284)) | ~iLEQ(suc(B_1_1284), suc(B_2_1287)))), inference(resolution, [status(thm)], [c_999, c_1494])).
% 17.59/5.86 tff(c_1504, plain, (![B_1_1288, A_0_1289, B_2_1290]: (E(f(B_1_1288), f(suc(suc(B_1_1288)))) | E(f(A_0_1289), f(suc(suc(A_0_1289)))) | E(f(B_2_1290), f(suc(suc(B_2_1290)))) | ~iLEQ(suc(A_0_1289), suc(B_1_1288)) | ~iLEQ(suc(B_1_1288), suc(B_2_1290)))), inference(resolution, [status(thm)], [c_999, c_1500])).
% 17.59/5.86 tff(c_1508, plain, (![A_0_1291, B_2_1292]: (E(f(A_0_1291), f(suc(suc(A_0_1291)))) | E(f(B_2_1292), f(suc(suc(B_2_1292)))) | ~iLEQ(suc(A_0_1291), suc(B_2_1292)))), inference(resolution, [status(thm)], [c_999, c_1504])).
% 17.59/5.86 tff(c_1511, plain, (![A_0_612]: (E(f(A_0_612), f(suc(suc(A_0_612)))))), inference(resolution, [status(thm)], [c_999, c_1508])).
% 17.59/5.86 tff(c_62, plain, (![A_0_152, B_1_155, B_151, B_0_153, B_2_154]: (~E(f(B_1_155), f(suc(suc(B_1_155)))) | ~iLEQ(suc(B_151), suc(B_0_153)) | ~E(f(B_0_153), f(suc(suc(B_0_153)))) | ~E(0, f(A_0_152)) | ~E(0, f(suc(suc(B_1_155)))) | ~E(0, f(suc(suc(B_2_154)))) | ~E(0, f(suc(B_1_155))) | ~E(0, f(suc(B_151))) | ~E(0, f(suc(suc(suc(B_1_155))))) | ~E(f(B_151), f(suc(suc(B_151)))) | ~E(0, f(suc(suc(B_151)))) | ~E(0, f(B_151)) | ~E(0, f(suc(A_0_152))) | ~E(0, f(B_2_154)) | ~E(0, f(B_0_153)) | ~E(f(A_0_152), f(suc(A_0_152))) | ~E(f(B_2_154), f(suc(B_2_154))) | ~E(0, f(suc(suc(suc(A_0_152))))) | ~E(0, f(suc(B_2_154))) | ~E(0, f(suc(B_0_153))) | ~E(f(A_0_152), f(suc(suc(A_0_152)))) | ~iLEQ(suc(A_0_152), suc(B_151)) | ~E(f(B_151), f(suc(B_151))) | ~E(0, f(suc(suc(suc(B_151))))) | ~E(f(B_0_153), f(suc(B_0_153))) | ~E(0, f(suc(suc(suc(B_0_153))))) | ~E(0, f(suc(suc(B_0_153)))) | ~E(0, f(B_1_155)) | ~iLEQ(suc(B_0_153), suc(B_1_155)) | ~E(0, f(suc(suc(A_0_152)))) | ~iLEQ(suc(B_1_155), suc(B_2_154)) | ~E(f(B_1_155), f(suc(B_1_155))) | ~E(f(B_2_154), f(suc(suc(B_2_154)))) | ~E(0, f(suc(suc(suc(B_2_154))))))), inference(cnfTransformation, [status(thm)], [f_2513])).
% 17.59/5.86 tff(c_926, plain, (![A_0_152, B_1_155, B_151, B_0_153, B_2_154]: (~E(f(B_1_155), f(suc(suc(B_1_155)))) | ~iLEQ(suc(B_151), suc(B_0_153)) | ~E(f(B_0_153), f(suc(suc(B_0_153)))) | ~E(f(B_151), f(suc(suc(B_151)))) | ~E(f(A_0_152), f(suc(A_0_152))) | ~E(f(B_2_154), f(suc(B_2_154))) | ~E(f(A_0_152), f(suc(suc(A_0_152)))) | ~iLEQ(suc(A_0_152), suc(B_151)) | ~E(f(B_151), f(suc(B_151))) | ~E(f(B_0_153), f(suc(B_0_153))) | ~iLEQ(suc(B_0_153), suc(B_1_155)) | ~iLEQ(suc(B_1_155), suc(B_2_154)) | ~E(f(B_1_155), f(suc(B_1_155))) | ~E(f(B_2_154), f(suc(suc(B_2_154)))))), inference(demodulation, [status(thm), theory('equality')], [c_274, c_274, c_274, c_274, c_274, c_274, c_274, c_274, c_274, c_274, c_274, c_274, c_274, c_274, c_274, c_274, c_274, c_274, c_274, c_274, c_62])).
% 17.59/5.86 tff(c_1480, plain, (![A_0_152, B_1_155, B_151, B_0_153, B_2_154]: (~E(f(B_1_155), f(suc(suc(B_1_155)))) | ~iLEQ(suc(B_151), suc(B_0_153)) | ~E(f(B_0_153), f(suc(suc(B_0_153)))) | ~E(f(B_151), f(suc(suc(B_151)))) | ~E(f(A_0_152), f(suc(suc(A_0_152)))) | ~iLEQ(suc(A_0_152), suc(B_151)) | ~iLEQ(suc(B_0_153), suc(B_1_155)) | ~iLEQ(suc(B_1_155), suc(B_2_154)) | ~E(f(B_2_154), f(suc(suc(B_2_154)))))), inference(demodulation, [status(thm), theory('equality')], [c_1018, c_1018, c_1018, c_1018, c_1018, c_926])).
% 17.59/5.86 tff(c_1520, plain, (![B_1_1295, B_2_1294, B_1297, A_0_1296, B_0_1298]: (~iLEQ(suc(B_1297), suc(B_0_1298)) | ~iLEQ(suc(A_0_1296), suc(B_1297)) | ~iLEQ(suc(B_0_1298), suc(B_1_1295)) | ~iLEQ(suc(B_1_1295), suc(B_2_1294)))), inference(demodulation, [status(thm), theory('equality')], [c_1511, c_1511, c_1511, c_1511, c_1511, c_1480])).
% 17.59/5.86 tff(c_1526, plain, (![A_0_1299, A_0_1300, B_1_1301, B_2_1302]: (~iLEQ(suc(A_0_1299), suc(A_0_1300)) | ~iLEQ(suc(A_0_1300), suc(B_1_1301)) | ~iLEQ(suc(B_1_1301), suc(B_2_1302)))), inference(resolution, [status(thm)], [c_999, c_1520])).
% 17.59/5.86 tff(c_1530, plain, (![A_0_1303, B_1_1304, B_2_1305]: (~iLEQ(suc(A_0_1303), suc(B_1_1304)) | ~iLEQ(suc(B_1_1304), suc(B_2_1305)))), inference(resolution, [status(thm)], [c_999, c_1526])).
% 17.59/5.86 tff(c_1533, plain, (![A_0_612, B_2_1305]: (~iLEQ(suc(A_0_612), suc(B_2_1305)))), inference(resolution, [status(thm)], [c_999, c_1530])).
% 17.59/5.86 tff(c_1535, plain, $false, inference(negUnitSimplification, [status(thm)], [c_1533, c_999])).
% 17.59/5.86 % SZS output end CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------