%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : SYO652-1 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n008.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 : Thu Sep 24 09:12:14 AM UTC 2026
% Result : Unsatisfiable 120.77s 131.08s
% Output : Proof 120.77s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO652-1 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.03 This is a CNF_UNS_RFO_NEQ_NHN problem
% 0.00/0.04 % Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/10.38 % Computer : n008.cluster.edu
% 0.10/10.38 % Model : x86_64 x86_64
% 0.10/10.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/10.38 % Memory : 8046.5625MB
% 0.10/10.38 % OS : Linux 6.8.0-71-generic
% 0.10/10.38 % CPULimit : 300
% 0.10/10.38 % WCLimit : 300
% 0.10/10.38 % DateTime : Sun Sep 20 07:47:35 UTC 2026
% 0.10/10.38 % CPUTime :
% 120.77/131.08 % SZS status Unsatisfiable for theBenchmark
% 120.77/131.08 % SZS output start Proof for theBenchmark
% 120.77/131.08 cnf(clause_16, axiom,
% 120.77/131.08 ( ~E(0, f(suc(B_11))) | ~iLEQ(suc(B_12), suc(B_13)) | ~E(0, f(suc(A_1))) | ~E(0, f(B_11)) | ~E(0, f(A_1)) | ~E(0, f(B_13)) | ~E(0, f(suc(B_12))) | ~iLEQ(suc(A_1), suc(B_11)) | ~E(0, f(suc(B_13))) | ~E(0, f(B_12)) | ~iLEQ(suc(B_11), suc(B_12)) | E(f(A_1), f(suc(A_1))) | E(f(B_11), f(suc(B_11))) | E(f(B_12), f(suc(B_12))) | E(f(B_13), f(suc(B_13))) ),
% 120.77/131.08 file('theBenchmark.p', clause_16) ).
% 120.77/131.08
% 120.77/131.08 cnf(clause_149, axiom,
% 120.77/131.08 ( ~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)) | iLEQ(suc(A_1), suc(A_1)) ),
% 120.77/131.08 file('theBenchmark.p', clause_149) ).
% 120.77/131.08
% 120.77/131.08 cnf(clause_199, axiom,
% 120.77/131.08 ( LE(f(A), s(0)) ),
% 120.77/131.08 file('theBenchmark.p', clause_199) ).
% 120.77/131.08
% 120.77/131.08 cnf(clause_191, axiom,
% 120.77/131.08 ( ~LE(f(suc(B_10)), s(0)) | E(0, f(suc(B_10))) | LE(f(B_10), 0) ),
% 120.77/131.08 file('theBenchmark.p', clause_191) ).
% 120.77/131.08
% 120.77/131.08 cnf(clause_96, axiom,
% 120.77/131.08 ( ~E(0, f(suc(B_11))) | ~iLEQ(suc(B_12), suc(B_13)) | ~E(0, f(suc(suc(B_11)))) | ~E(0, f(suc(A_1))) | ~E(0, f(suc(suc(A_1)))) | ~E(0, f(B_11)) | ~E(0, f(A_1)) | ~E(0, f(B_13)) | ~E(0, f(suc(B_12))) | ~E(f(B_12), f(suc(B_12))) | ~E(0, f(suc(suc(B_12)))) | ~E(f(A_1), f(suc(A_1))) | ~E(f(B_11), f(suc(B_11))) | ~iLEQ(suc(A_1), suc(B_11)) | ~E(0, f(suc(B_13))) | ~E(0, f(B_12)) | ~E(0, f(suc(suc(B_13)))) | ~E(f(B_13), f(suc(B_13))) | ~iLEQ(suc(B_11), suc(B_12)) ),
% 120.77/131.08 file('theBenchmark.p', clause_96) ).
% 120.77/131.08
% 120.77/131.08 cnf(clause_17, axiom,
% 120.77/131.08 ( ~LE(f(B_10), s(0)) | E(0, f(B_10)) | LE(f(B_10), 0) ),
% 120.77/131.08 file('theBenchmark.p', clause_17) ).
% 120.77/131.08
% 120.77/131.08 cnf(clause_3, axiom,
% 120.77/131.08 ( ~LE(f(suc(suc(B_10))), s(0)) | E(0, f(suc(suc(B_10)))) | LE(f(B_10), 0) ),
% 120.77/131.08 file('theBenchmark.p', clause_3) ).
% 120.77/131.08
% 120.77/131.08 cnf(clause_99, axiom,
% 120.77/131.08 ( ~LE(f(z), 0) ),
% 120.77/131.08 file('theBenchmark.p', clause_99) ).
% 120.77/131.08
% 120.77/131.08 cnf(clause_44, axiom,
% 120.77/131.08 ( ~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)) ),
% 120.77/131.08 file('theBenchmark.p', clause_44) ).
% 120.77/131.08
% 120.77/131.08 cnf(t1, plain, ( ~E(0, f(suc(z))) | ~iLEQ(suc(z), suc(z)) | ~E(f(z), f(suc(z))) | ~E(0, f(suc(suc(z)))) | ~E(0, f(z)) | ~E(0, f(suc(z))) | ~iLEQ(suc(z), suc(z)) | ~E(f(z), f(suc(z))) | ~E(f(z), f(suc(z))) | ~E(0, f(suc(suc(z)))) | ~E(f(z), f(suc(z))) | ~E(0, f(suc(z))) | ~E(0, f(z)) | ~E(0, f(z)) | ~E(0, f(z)) | ~E(0, f(suc(suc(z)))) | ~E(0, f(suc(z))) | ~E(0, f(suc(suc(z)))) | ~iLEQ(suc(z), suc(z)) ),
% 120.77/131.08 inference(start, [status(thm), parent(0:0)], [clause_96]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t2, plain, ( E(0, f(suc(z))) | ~LE(f(suc(z)), s(0)) | LE(f(z), 0) ),
% 120.77/131.08 inference(extension, [status(thm), parent(t1:1)], [clause_191]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t3, plain, $false,
% 120.77/131.08 inference(connection, [status(thm), parent(t2:1)], [t2:1,t1:1]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t4, plain, ( LE(f(suc(z)), s(0)) ),
% 120.77/131.08 inference(extension, [status(thm), parent(t2:2)], [clause_199]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t5, plain, $false,
% 120.77/131.08 inference(connection, [status(thm), parent(t4:1)], [t4:1,t2:2]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t6, plain, ( ~LE(f(z), 0) ),
% 120.77/131.08 inference(extension, [status(thm), parent(t2:3)], [clause_99]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t7, plain, $false,
% 120.77/131.08 inference(connection, [status(thm), parent(t6:1)], [t6:1,t2:3]) ).
% 120.77/131.08
% 120.77/131.08 cnf(l1, lemma, E(0, f(suc(z))),
% 120.77/131.08 inference(lemma, [status(cth), parent(t1:1), below(0:0)], [t1:1]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t8, plain, ( iLEQ(suc(z), suc(z)) | ~E(0, f(suc(suc(z)))) | ~E(0, f(z)) | ~E(f(z), f(suc(z))) | ~E(0, f(suc(z))) ),
% 120.77/131.08 inference(extension, [status(thm), parent(t1:2)], [clause_149]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t9, plain, $false,
% 120.77/131.08 inference(connection, [status(thm), parent(t8:1)], [t8:1,t1:2]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t10, plain, ( E(0, f(suc(suc(z)))) | ~LE(f(suc(suc(z))), s(0)) | LE(f(z), 0) ),
% 120.77/131.08 inference(extension, [status(thm), parent(t8:2)], [clause_3]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t11, plain, $false,
% 120.77/131.08 inference(connection, [status(thm), parent(t10:1)], [t10:1,t8:2]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t12, plain, ( LE(f(suc(suc(z))), s(0)) ),
% 120.77/131.08 inference(extension, [status(thm), parent(t10:2)], [clause_199]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t13, plain, $false,
% 120.77/131.08 inference(connection, [status(thm), parent(t12:1)], [t12:1,t10:2]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t14, plain, ( ~LE(f(z), 0) ),
% 120.77/131.08 inference(extension, [status(thm), parent(t10:3)], [clause_99]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t15, plain, $false,
% 120.77/131.08 inference(connection, [status(thm), parent(t14:1)], [t14:1,t10:3]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t16, plain, ( E(0, f(z)) | ~LE(f(z), s(0)) | LE(f(z), 0) ),
% 120.77/131.08 inference(extension, [status(thm), parent(t8:3)], [clause_17]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t17, plain, $false,
% 120.77/131.08 inference(connection, [status(thm), parent(t16:1)], [t16:1,t8:3]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t18, plain, ( LE(f(z), s(0)) ),
% 120.77/131.08 inference(extension, [status(thm), parent(t16:2)], [clause_199]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t19, plain, $false,
% 120.77/131.08 inference(connection, [status(thm), parent(t18:1)], [t18:1,t16:2]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t20, plain, ( ~LE(f(z), 0) ),
% 120.77/131.08 inference(extension, [status(thm), parent(t16:3)], [clause_99]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t21, plain, $false,
% 120.77/131.08 inference(connection, [status(thm), parent(t20:1)], [t20:1,t16:3]) ).
% 120.77/131.08
% 120.77/131.08 cnf(l8, lemma, E(0, f(z)),
% 120.77/131.08 inference(lemma, [status(cth), parent(t8:3), below(t1:2)], [t8:3]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t22, plain, ( E(f(z), f(suc(z))) | ~E(0, f(z)) | iLEQ(suc(z), suc(z)) | ~E(0, f(suc(z))) ),
% 120.77/131.08 inference(extension, [status(thm), parent(t8:4)], [clause_44]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t23, plain, $false,
% 120.77/131.08 inference(connection, [status(thm), parent(t22:1)], [t22:1,t8:4]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t24, plain, E(0, f(z)),
% 120.77/131.08 inference(lemma_extension, [status(thm), parent(t22:2)], [l8:1]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t25, plain, $false,
% 120.77/131.08 inference(connection, [status(thm), parent(t24:1)], [t24:1,t22:2]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t26, plain, $false,
% 120.77/131.08 inference(reduction, [status(thm), parent(t22:3)], [t22:3,t1:2]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t27, plain, E(0, f(suc(z))),
% 120.77/131.08 inference(lemma_extension, [status(thm), parent(t22:4)], [l1:1]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t28, plain, $false,
% 120.77/131.08 inference(connection, [status(thm), parent(t27:1)], [t27:1,t22:4]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t29, plain, E(0, f(suc(z))),
% 120.77/131.08 inference(lemma_extension, [status(thm), parent(t8:5)], [l1:1]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t30, plain, $false,
% 120.77/131.08 inference(connection, [status(thm), parent(t29:1)], [t29:1,t8:5]) ).
% 120.77/131.08
% 120.77/131.08 cnf(l4, lemma, iLEQ(suc(z), suc(z)),
% 120.77/131.08 inference(lemma, [status(cth), parent(t1:2), below(0:0)], [t1:2]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t31, plain, ( E(f(z), f(suc(z))) | ~E(0, f(z)) | iLEQ(suc(z), suc(z)) | ~E(0, f(suc(z))) ),
% 120.77/131.08 inference(extension, [status(thm), parent(t1:3)], [clause_44]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t32, plain, $false,
% 120.77/131.08 inference(connection, [status(thm), parent(t31:1)], [t31:1,t1:3]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t33, plain, ( E(0, f(z)) | ~LE(f(z), s(0)) | LE(f(z), 0) ),
% 120.77/131.08 inference(extension, [status(thm), parent(t31:2)], [clause_17]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t34, plain, $false,
% 120.77/131.08 inference(connection, [status(thm), parent(t33:1)], [t33:1,t31:2]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t35, plain, ( LE(f(z), s(0)) ),
% 120.77/131.08 inference(extension, [status(thm), parent(t33:2)], [clause_199]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t36, plain, $false,
% 120.77/131.08 inference(connection, [status(thm), parent(t35:1)], [t35:1,t33:2]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t37, plain, ( ~LE(f(z), 0) ),
% 120.77/131.08 inference(extension, [status(thm), parent(t33:3)], [clause_99]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t38, plain, $false,
% 120.77/131.08 inference(connection, [status(thm), parent(t37:1)], [t37:1,t33:3]) ).
% 120.77/131.08
% 120.77/131.08 cnf(l14, lemma, E(0, f(z)),
% 120.77/131.08 inference(lemma, [status(cth), parent(t31:2), below(t1:3)], [t31:2]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t39, plain, ( ~iLEQ(suc(z), suc(z)) | ~E(0, f(suc(z))) | E(f(z), f(suc(z))) | E(f(z), f(suc(z))) | E(f(z), f(suc(z))) | E(f(z), f(suc(z))) | ~E(0, f(z)) | ~E(0, f(suc(z))) | ~iLEQ(suc(z), suc(z)) | ~E(0, f(suc(z))) | ~E(0, f(z)) | ~E(0, f(z)) | ~E(0, f(z)) | ~E(0, f(suc(z))) | ~iLEQ(suc(z), suc(z)) ),
% 120.77/131.08 inference(extension, [status(thm), parent(t31:3)], [clause_16]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t40, plain, $false,
% 120.77/131.08 inference(connection, [status(thm), parent(t39:1)], [t39:1,t31:3]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t41, plain, E(0, f(suc(z))),
% 120.77/131.08 inference(lemma_extension, [status(thm), parent(t39:2)], [l1:1]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t42, plain, $false,
% 120.77/131.08 inference(connection, [status(thm), parent(t41:1)], [t41:1,t39:2]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t43, plain, $false,
% 120.77/131.08 inference(reduction, [status(thm), parent(t39:3)], [t39:3,t1:3]) ).
% 120.77/131.08
% 120.77/131.08 cnf(l18, lemma, ~E(f(z), f(suc(z))),
% 120.77/131.08 inference(lemma, [status(cth), parent(t39:3), below(t31:3)], [t39:3]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t44, plain, ~E(f(z), f(suc(z))),
% 120.77/131.08 inference(lemma_extension, [status(thm), parent(t39:4)], [l18:1]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t45, plain, $false,
% 120.77/131.08 inference(connection, [status(thm), parent(t44:1)], [t44:1,t39:4]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t46, plain, $false,
% 120.77/131.08 inference(reduction, [status(thm), parent(t39:5)], [t39:5,t1:3]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t47, plain, $false,
% 120.77/131.08 inference(reduction, [status(thm), parent(t39:6)], [t39:6,t1:3]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t48, plain, E(0, f(z)),
% 120.77/131.08 inference(lemma_extension, [status(thm), parent(t39:7)], [l14:1]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t49, plain, $false,
% 120.77/131.08 inference(connection, [status(thm), parent(t48:1)], [t48:1,t39:7]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t50, plain, E(0, f(suc(z))),
% 120.77/131.08 inference(lemma_extension, [status(thm), parent(t39:8)], [l1:1]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t51, plain, $false,
% 120.77/131.08 inference(connection, [status(thm), parent(t50:1)], [t50:1,t39:8]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t52, plain, iLEQ(suc(z), suc(z)),
% 120.77/131.08 inference(lemma_extension, [status(thm), parent(t39:9)], [l4:1]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t53, plain, $false,
% 120.77/131.08 inference(connection, [status(thm), parent(t52:1)], [t52:1,t39:9]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t54, plain, E(0, f(suc(z))),
% 120.77/131.08 inference(lemma_extension, [status(thm), parent(t39:10)], [l1:1]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t55, plain, $false,
% 120.77/131.08 inference(connection, [status(thm), parent(t54:1)], [t54:1,t39:10]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t56, plain, E(0, f(z)),
% 120.77/131.08 inference(lemma_extension, [status(thm), parent(t39:11)], [l14:1]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t57, plain, $false,
% 120.77/131.08 inference(connection, [status(thm), parent(t56:1)], [t56:1,t39:11]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t58, plain, E(0, f(z)),
% 120.77/131.08 inference(lemma_extension, [status(thm), parent(t39:12)], [l14:1]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t59, plain, $false,
% 120.77/131.08 inference(connection, [status(thm), parent(t58:1)], [t58:1,t39:12]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t60, plain, E(0, f(z)),
% 120.77/131.08 inference(lemma_extension, [status(thm), parent(t39:13)], [l14:1]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t61, plain, $false,
% 120.77/131.08 inference(connection, [status(thm), parent(t60:1)], [t60:1,t39:13]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t62, plain, E(0, f(suc(z))),
% 120.77/131.08 inference(lemma_extension, [status(thm), parent(t39:14)], [l1:1]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t63, plain, $false,
% 120.77/131.08 inference(connection, [status(thm), parent(t62:1)], [t62:1,t39:14]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t64, plain, iLEQ(suc(z), suc(z)),
% 120.77/131.08 inference(lemma_extension, [status(thm), parent(t39:15)], [l4:1]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t65, plain, $false,
% 120.77/131.08 inference(connection, [status(thm), parent(t64:1)], [t64:1,t39:15]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t66, plain, E(0, f(suc(z))),
% 120.77/131.08 inference(lemma_extension, [status(thm), parent(t31:4)], [l1:1]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t67, plain, $false,
% 120.77/131.08 inference(connection, [status(thm), parent(t66:1)], [t66:1,t31:4]) ).
% 120.77/131.08
% 120.77/131.08 cnf(l13, lemma, E(f(z), f(suc(z))),
% 120.77/131.08 inference(lemma, [status(cth), parent(t1:3), below(0:0)], [t1:3]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t68, plain, ( E(0, f(suc(suc(z)))) | ~LE(f(suc(suc(z))), s(0)) | LE(f(z), 0) ),
% 120.77/131.08 inference(extension, [status(thm), parent(t1:4)], [clause_3]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t69, plain, $false,
% 120.77/131.08 inference(connection, [status(thm), parent(t68:1)], [t68:1,t1:4]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t70, plain, ( LE(f(suc(suc(z))), s(0)) ),
% 120.77/131.08 inference(extension, [status(thm), parent(t68:2)], [clause_199]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t71, plain, $false,
% 120.77/131.08 inference(connection, [status(thm), parent(t70:1)], [t70:1,t68:2]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t72, plain, ( ~LE(f(z), 0) ),
% 120.77/131.08 inference(extension, [status(thm), parent(t68:3)], [clause_99]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t73, plain, $false,
% 120.77/131.08 inference(connection, [status(thm), parent(t72:1)], [t72:1,t68:3]) ).
% 120.77/131.08
% 120.77/131.08 cnf(l21, lemma, E(0, f(suc(suc(z)))),
% 120.77/131.08 inference(lemma, [status(cth), parent(t1:4), below(0:0)], [t1:4]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t74, plain, ( E(0, f(z)) | ~LE(f(z), s(0)) | LE(f(z), 0) ),
% 120.77/131.08 inference(extension, [status(thm), parent(t1:5)], [clause_17]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t75, plain, $false,
% 120.77/131.08 inference(connection, [status(thm), parent(t74:1)], [t74:1,t1:5]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t76, plain, ( LE(f(z), s(0)) ),
% 120.77/131.08 inference(extension, [status(thm), parent(t74:2)], [clause_199]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t77, plain, $false,
% 120.77/131.08 inference(connection, [status(thm), parent(t76:1)], [t76:1,t74:2]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t78, plain, ( ~LE(f(z), 0) ),
% 120.77/131.08 inference(extension, [status(thm), parent(t74:3)], [clause_99]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t79, plain, $false,
% 120.77/131.08 inference(connection, [status(thm), parent(t78:1)], [t78:1,t74:3]) ).
% 120.77/131.08
% 120.77/131.08 cnf(l24, lemma, E(0, f(z)),
% 120.77/131.08 inference(lemma, [status(cth), parent(t1:5), below(0:0)], [t1:5]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t80, plain, E(0, f(suc(z))),
% 120.77/131.08 inference(lemma_extension, [status(thm), parent(t1:6)], [l1:1]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t81, plain, $false,
% 120.77/131.08 inference(connection, [status(thm), parent(t80:1)], [t80:1,t1:6]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t82, plain, ( iLEQ(suc(z), suc(z)) | ~E(0, f(z)) | E(f(z), f(suc(z))) | ~E(0, f(suc(z))) ),
% 120.77/131.08 inference(extension, [status(thm), parent(t1:7)], [clause_44]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t83, plain, $false,
% 120.77/131.08 inference(connection, [status(thm), parent(t82:1)], [t82:1,t1:7]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t84, plain, E(0, f(z)),
% 120.77/131.08 inference(lemma_extension, [status(thm), parent(t82:2)], [l24:1]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t85, plain, $false,
% 120.77/131.08 inference(connection, [status(thm), parent(t84:1)], [t84:1,t82:2]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t86, plain, ( ~E(f(z), f(suc(z))) | ~E(0, f(suc(suc(z)))) | ~E(0, f(z)) | iLEQ(suc(z), suc(z)) | ~E(0, f(suc(z))) ),
% 120.77/131.08 inference(extension, [status(thm), parent(t82:3)], [clause_149]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t87, plain, $false,
% 120.77/131.08 inference(connection, [status(thm), parent(t86:1)], [t86:1,t82:3]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t88, plain, E(0, f(suc(suc(z)))),
% 120.77/131.08 inference(lemma_extension, [status(thm), parent(t86:2)], [l21:1]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t89, plain, $false,
% 120.77/131.08 inference(connection, [status(thm), parent(t88:1)], [t88:1,t86:2]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t90, plain, E(0, f(z)),
% 120.77/131.08 inference(lemma_extension, [status(thm), parent(t86:3)], [l24:1]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t91, plain, $false,
% 120.77/131.08 inference(connection, [status(thm), parent(t90:1)], [t90:1,t86:3]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t92, plain, $false,
% 120.77/131.08 inference(reduction, [status(thm), parent(t86:4)], [t86:4,t1:7]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t93, plain, E(0, f(suc(z))),
% 120.77/131.08 inference(lemma_extension, [status(thm), parent(t86:5)], [l1:1]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t94, plain, $false,
% 120.77/131.08 inference(connection, [status(thm), parent(t93:1)], [t93:1,t86:5]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t95, plain, E(0, f(suc(z))),
% 120.77/131.08 inference(lemma_extension, [status(thm), parent(t82:4)], [l1:1]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t96, plain, $false,
% 120.77/131.08 inference(connection, [status(thm), parent(t95:1)], [t95:1,t82:4]) ).
% 120.77/131.08
% 120.77/131.08 cnf(l27, lemma, iLEQ(suc(z), suc(z)),
% 120.77/131.08 inference(lemma, [status(cth), parent(t1:7), below(0:0)], [t1:7]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t97, plain, E(f(z), f(suc(z))),
% 120.77/131.08 inference(lemma_extension, [status(thm), parent(t1:8)], [l13:1]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t98, plain, $false,
% 120.77/131.08 inference(connection, [status(thm), parent(t97:1)], [t97:1,t1:8]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t99, plain, E(f(z), f(suc(z))),
% 120.77/131.08 inference(lemma_extension, [status(thm), parent(t1:9)], [l13:1]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t100, plain, $false,
% 120.77/131.08 inference(connection, [status(thm), parent(t99:1)], [t99:1,t1:9]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t101, plain, E(0, f(suc(suc(z)))),
% 120.77/131.08 inference(lemma_extension, [status(thm), parent(t1:10)], [l21:1]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t102, plain, $false,
% 120.77/131.08 inference(connection, [status(thm), parent(t101:1)], [t101:1,t1:10]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t103, plain, E(f(z), f(suc(z))),
% 120.77/131.08 inference(lemma_extension, [status(thm), parent(t1:11)], [l13:1]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t104, plain, $false,
% 120.77/131.08 inference(connection, [status(thm), parent(t103:1)], [t103:1,t1:11]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t105, plain, E(0, f(suc(z))),
% 120.77/131.08 inference(lemma_extension, [status(thm), parent(t1:12)], [l1:1]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t106, plain, $false,
% 120.77/131.08 inference(connection, [status(thm), parent(t105:1)], [t105:1,t1:12]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t107, plain, E(0, f(z)),
% 120.77/131.08 inference(lemma_extension, [status(thm), parent(t1:13)], [l24:1]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t108, plain, $false,
% 120.77/131.08 inference(connection, [status(thm), parent(t107:1)], [t107:1,t1:13]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t109, plain, E(0, f(z)),
% 120.77/131.08 inference(lemma_extension, [status(thm), parent(t1:14)], [l24:1]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t110, plain, $false,
% 120.77/131.08 inference(connection, [status(thm), parent(t109:1)], [t109:1,t1:14]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t111, plain, E(0, f(z)),
% 120.77/131.08 inference(lemma_extension, [status(thm), parent(t1:15)], [l24:1]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t112, plain, $false,
% 120.77/131.08 inference(connection, [status(thm), parent(t111:1)], [t111:1,t1:15]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t113, plain, E(0, f(suc(suc(z)))),
% 120.77/131.08 inference(lemma_extension, [status(thm), parent(t1:16)], [l21:1]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t114, plain, $false,
% 120.77/131.08 inference(connection, [status(thm), parent(t113:1)], [t113:1,t1:16]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t115, plain, E(0, f(suc(z))),
% 120.77/131.08 inference(lemma_extension, [status(thm), parent(t1:17)], [l1:1]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t116, plain, $false,
% 120.77/131.08 inference(connection, [status(thm), parent(t115:1)], [t115:1,t1:17]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t117, plain, E(0, f(suc(suc(z)))),
% 120.77/131.08 inference(lemma_extension, [status(thm), parent(t1:18)], [l21:1]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t118, plain, $false,
% 120.77/131.08 inference(connection, [status(thm), parent(t117:1)], [t117:1,t1:18]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t119, plain, iLEQ(suc(z), suc(z)),
% 120.77/131.08 inference(lemma_extension, [status(thm), parent(t1:19)], [l27:1]) ).
% 120.77/131.08
% 120.77/131.08 cnf(t120, plain, $false,
% 120.77/131.08 inference(connection, [status(thm), parent(t119:1)], [t119:1,t1:19]) ).
% 120.77/131.08
% 120.77/131.08 % SZS output end Proof for theBenchmark
%------------------------------------------------------------------------------