%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : SYO664-1 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n009.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:15 AM UTC 2026
% Result : Unsatisfiable 0.32s 0.59s
% Output : Proof 0.32s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO664-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/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.37 % Computer : n009.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Sun Sep 20 07:47:12 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.32/0.59 % SZS status Unsatisfiable for theBenchmark
% 0.32/0.59 % SZS output start Proof for theBenchmark
% 0.32/0.60 cnf(clause_37, axiom,
% 0.32/0.60 ( ~E(s(0), f(suc(B_45))) | ~E(s(0), f(B_45)) | ~E(s(0), f(suc(B_46))) | ~E(s(0), f(suc(B_43))) | ~E(s(0), f(A_1)) | ~E(s(0), f(suc(A_1))) | ~iLEQ(suc(A_1), suc(B_43)) | ~E(s(0), f(B_43)) | ~iLEQ(suc(B_44), suc(B_45)) | ~E(s(0), f(B_46)) | ~E(s(0), f(B_44)) | ~iLEQ(suc(B_45), suc(B_46)) | ~iLEQ(suc(B_43), suc(B_44)) | ~E(s(0), f(suc(B_44))) ),
% 0.32/0.60 file('theBenchmark.p', clause_37) ).
% 0.32/0.60
% 0.32/0.60 cnf(clause_70, axiom,
% 0.32/0.60 ( ~LE(f(z), 0) ),
% 0.32/0.60 file('theBenchmark.p', clause_70) ).
% 0.32/0.60
% 0.32/0.60 cnf(clause_20, axiom,
% 0.32/0.60 ( ~LE(f(B_42), s(s(0))) | E(s(0), f(B_42)) | LE(f(B_42), s(0)) ),
% 0.32/0.60 file('theBenchmark.p', clause_20) ).
% 0.32/0.60
% 0.32/0.60 cnf(clause_66, axiom,
% 0.32/0.60 ( ~E(0, f(B_63)) | ~E(0, f(suc(B_61))) | ~E(0, f(suc(A_2))) | ~iLEQ(suc(A_2), suc(B_61)) | ~iLEQ(suc(B_61), suc(B_62)) | ~E(0, f(suc(B_63))) | ~E(0, f(A_2)) | ~iLEQ(suc(B_62), suc(B_63)) | ~E(0, f(B_64)) | ~iLEQ(suc(B_63), suc(B_64)) | ~E(0, f(suc(B_62))) | ~E(0, f(B_61)) | ~E(0, f(suc(B_64))) | ~E(0, f(B_62)) ),
% 0.32/0.60 file('theBenchmark.p', clause_66) ).
% 0.32/0.60
% 0.32/0.60 cnf(clause_58, axiom,
% 0.32/0.60 ( LE(f(A), s(s(0))) ),
% 0.32/0.60 file('theBenchmark.p', clause_58) ).
% 0.32/0.60
% 0.32/0.60 cnf(clause_6, axiom,
% 0.32/0.60 ( ~E(0, f(A_2)) | ~E(0, f(suc(A_2))) | iLEQ(suc(A_2), suc(A_2)) ),
% 0.32/0.60 file('theBenchmark.p', clause_6) ).
% 0.32/0.60
% 0.32/0.60 cnf(clause_117, axiom,
% 0.32/0.60 ( ~LE(f(suc(B_60)), s(0)) | E(0, f(suc(B_60))) | LE(f(B_60), 0) ),
% 0.32/0.60 file('theBenchmark.p', clause_117) ).
% 0.32/0.60
% 0.32/0.60 cnf(clause_94, axiom,
% 0.32/0.60 ( ~LE(f(B_60), s(0)) | E(0, f(B_60)) | LE(f(B_60), 0) ),
% 0.32/0.60 file('theBenchmark.p', clause_94) ).
% 0.32/0.60
% 0.32/0.60 cnf(clause_50, axiom,
% 0.32/0.60 ( ~E(s(0), f(A_1)) | ~E(s(0), f(suc(A_1))) | iLEQ(suc(A_1), suc(A_1)) ),
% 0.32/0.60 file('theBenchmark.p', clause_50) ).
% 0.32/0.60
% 0.32/0.60 cnf(clause_83, axiom,
% 0.32/0.60 ( ~LE(f(suc(B_42)), s(s(0))) | E(s(0), f(suc(B_42))) | LE(f(B_42), s(0)) ),
% 0.32/0.60 file('theBenchmark.p', clause_83) ).
% 0.32/0.60
% 0.32/0.60 cnf(t1, plain, ( ~E(0, f(z)) | ~E(0, f(z)) | ~E(0, f(suc(z))) | ~E(0, f(z)) | ~E(0, f(suc(z))) | ~iLEQ(suc(z), suc(z)) | ~E(0, f(z)) | ~iLEQ(suc(z), suc(z)) | ~E(0, f(z)) | ~E(0, f(suc(z))) | ~iLEQ(suc(z), suc(z)) | ~iLEQ(suc(z), suc(z)) | ~E(0, f(suc(z))) | ~E(0, f(suc(z))) ),
% 0.32/0.60 inference(start, [status(thm), parent(0:0)], [clause_66]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t2, plain, ( E(0, f(z)) | ~LE(f(z), s(0)) | LE(f(z), 0) ),
% 0.32/0.60 inference(extension, [status(thm), parent(t1:1)], [clause_94]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t3, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t2:1)], [t2:1,t1:1]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t4, plain, ( LE(f(z), s(0)) | ~LE(f(suc(z)), s(s(0))) | E(s(0), f(suc(z))) ),
% 0.32/0.60 inference(extension, [status(thm), parent(t2:2)], [clause_83]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t5, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t4:1)], [t4:1,t2:2]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t6, plain, ( LE(f(suc(z)), s(s(0))) ),
% 0.32/0.60 inference(extension, [status(thm), parent(t4:2)], [clause_58]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t7, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t6:1)], [t6:1,t4:2]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t8, plain, ( ~E(s(0), f(suc(z))) | ~E(s(0), f(z)) | iLEQ(suc(z), suc(z)) ),
% 0.32/0.60 inference(extension, [status(thm), parent(t4:3)], [clause_50]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t9, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t8:1)], [t8:1,t4:3]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t10, plain, ( E(s(0), f(z)) | ~LE(f(z), s(s(0))) | LE(f(z), s(0)) ),
% 0.32/0.60 inference(extension, [status(thm), parent(t8:2)], [clause_20]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t11, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t10:1)], [t10:1,t8:2]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t12, plain, ( LE(f(z), s(s(0))) ),
% 0.32/0.60 inference(extension, [status(thm), parent(t10:2)], [clause_58]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t13, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t12:1)], [t12:1,t10:2]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t14, plain, $false,
% 0.32/0.60 inference(reduction, [status(thm), parent(t10:3)], [t10:3,t2:2]) ).
% 0.32/0.60
% 0.32/0.60 cnf(l5, lemma, E(s(0), f(z)),
% 0.32/0.60 inference(lemma, [status(cth), parent(t8:2), below(t4:3)], [t8:2]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t15, plain, ( ~iLEQ(suc(z), suc(z)) | ~E(s(0), f(suc(z))) | ~E(s(0), f(suc(z))) | ~iLEQ(suc(z), suc(z)) | ~E(s(0), f(z)) | ~E(s(0), f(z)) | ~iLEQ(suc(z), suc(z)) | ~E(s(0), f(z)) | ~iLEQ(suc(z), suc(z)) | ~E(s(0), f(suc(z))) | ~E(s(0), f(z)) | ~E(s(0), f(suc(z))) | ~E(s(0), f(suc(z))) | ~E(s(0), f(z)) ),
% 0.32/0.60 inference(extension, [status(thm), parent(t8:3)], [clause_37]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t16, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t15:1)], [t15:1,t8:3]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t17, plain, $false,
% 0.32/0.60 inference(reduction, [status(thm), parent(t15:2)], [t15:2,t4:3]) ).
% 0.32/0.60
% 0.32/0.60 cnf(l9, lemma, E(s(0), f(suc(z))),
% 0.32/0.60 inference(lemma, [status(cth), parent(t15:2), below(t8:3)], [t15:2]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t18, plain, E(s(0), f(suc(z))),
% 0.32/0.60 inference(lemma_extension, [status(thm), parent(t15:3)], [l9:1]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t19, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t18:1)], [t18:1,t15:3]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t20, plain, $false,
% 0.32/0.60 inference(reduction, [status(thm), parent(t15:4)], [t15:4,t8:3]) ).
% 0.32/0.60
% 0.32/0.60 cnf(l10, lemma, iLEQ(suc(z), suc(z)),
% 0.32/0.60 inference(lemma, [status(cth), parent(t15:4), below(t8:3)], [t15:4]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t21, plain, E(s(0), f(z)),
% 0.32/0.60 inference(lemma_extension, [status(thm), parent(t15:5)], [l5:1]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t22, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t21:1)], [t21:1,t15:5]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t23, plain, E(s(0), f(z)),
% 0.32/0.60 inference(lemma_extension, [status(thm), parent(t15:6)], [l5:1]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t24, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t23:1)], [t23:1,t15:6]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t25, plain, iLEQ(suc(z), suc(z)),
% 0.32/0.60 inference(lemma_extension, [status(thm), parent(t15:7)], [l10:1]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t26, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t25:1)], [t25:1,t15:7]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t27, plain, E(s(0), f(z)),
% 0.32/0.60 inference(lemma_extension, [status(thm), parent(t15:8)], [l5:1]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t28, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t27:1)], [t27:1,t15:8]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t29, plain, $false,
% 0.32/0.60 inference(reduction, [status(thm), parent(t15:9)], [t15:9,t8:3]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t30, plain, E(s(0), f(suc(z))),
% 0.32/0.60 inference(lemma_extension, [status(thm), parent(t15:10)], [l9:1]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t31, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t30:1)], [t30:1,t15:10]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t32, plain, E(s(0), f(z)),
% 0.32/0.60 inference(lemma_extension, [status(thm), parent(t15:11)], [l5:1]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t33, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t32:1)], [t32:1,t15:11]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t34, plain, E(s(0), f(suc(z))),
% 0.32/0.60 inference(lemma_extension, [status(thm), parent(t15:12)], [l9:1]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t35, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t34:1)], [t34:1,t15:12]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t36, plain, E(s(0), f(suc(z))),
% 0.32/0.60 inference(lemma_extension, [status(thm), parent(t15:13)], [l9:1]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t37, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t36:1)], [t36:1,t15:13]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t38, plain, E(s(0), f(z)),
% 0.32/0.60 inference(lemma_extension, [status(thm), parent(t15:14)], [l5:1]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t39, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t38:1)], [t38:1,t15:14]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t40, plain, ( ~LE(f(z), 0) ),
% 0.32/0.60 inference(extension, [status(thm), parent(t2:3)], [clause_70]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t41, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t40:1)], [t40:1,t2:3]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t42, plain, ( E(0, f(z)) | ~LE(f(z), s(0)) | LE(f(z), 0) ),
% 0.32/0.60 inference(extension, [status(thm), parent(t1:2)], [clause_94]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t43, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t42:1)], [t42:1,t1:2]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t44, plain, ( LE(f(z), s(0)) | ~LE(f(suc(z)), s(s(0))) | E(s(0), f(suc(z))) ),
% 0.32/0.60 inference(extension, [status(thm), parent(t42:2)], [clause_83]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t45, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t44:1)], [t44:1,t42:2]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t46, plain, ( LE(f(suc(z)), s(s(0))) ),
% 0.32/0.60 inference(extension, [status(thm), parent(t44:2)], [clause_58]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t47, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t46:1)], [t46:1,t44:2]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t48, plain, ( ~E(s(0), f(suc(z))) | ~E(s(0), f(z)) | iLEQ(suc(z), suc(z)) ),
% 0.32/0.60 inference(extension, [status(thm), parent(t44:3)], [clause_50]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t49, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t48:1)], [t48:1,t44:3]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t50, plain, ( E(s(0), f(z)) | ~LE(f(z), s(s(0))) | LE(f(z), s(0)) ),
% 0.32/0.60 inference(extension, [status(thm), parent(t48:2)], [clause_20]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t51, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t50:1)], [t50:1,t48:2]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t52, plain, ( LE(f(z), s(s(0))) ),
% 0.32/0.60 inference(extension, [status(thm), parent(t50:2)], [clause_58]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t53, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t52:1)], [t52:1,t50:2]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t54, plain, $false,
% 0.32/0.60 inference(reduction, [status(thm), parent(t50:3)], [t50:3,t42:2]) ).
% 0.32/0.60
% 0.32/0.60 cnf(l17, lemma, E(s(0), f(z)),
% 0.32/0.60 inference(lemma, [status(cth), parent(t48:2), below(t44:3)], [t48:2]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t55, plain, ( ~iLEQ(suc(z), suc(z)) | ~E(s(0), f(suc(z))) | ~E(s(0), f(suc(z))) | ~iLEQ(suc(z), suc(z)) | ~E(s(0), f(z)) | ~E(s(0), f(z)) | ~iLEQ(suc(z), suc(z)) | ~E(s(0), f(z)) | ~iLEQ(suc(z), suc(z)) | ~E(s(0), f(suc(z))) | ~E(s(0), f(z)) | ~E(s(0), f(suc(z))) | ~E(s(0), f(suc(z))) | ~E(s(0), f(z)) ),
% 0.32/0.60 inference(extension, [status(thm), parent(t48:3)], [clause_37]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t56, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t55:1)], [t55:1,t48:3]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t57, plain, $false,
% 0.32/0.60 inference(reduction, [status(thm), parent(t55:2)], [t55:2,t44:3]) ).
% 0.32/0.60
% 0.32/0.60 cnf(l21, lemma, E(s(0), f(suc(z))),
% 0.32/0.60 inference(lemma, [status(cth), parent(t55:2), below(t48:3)], [t55:2]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t58, plain, E(s(0), f(suc(z))),
% 0.32/0.60 inference(lemma_extension, [status(thm), parent(t55:3)], [l21:1]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t59, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t58:1)], [t58:1,t55:3]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t60, plain, $false,
% 0.32/0.60 inference(reduction, [status(thm), parent(t55:4)], [t55:4,t48:3]) ).
% 0.32/0.60
% 0.32/0.60 cnf(l22, lemma, iLEQ(suc(z), suc(z)),
% 0.32/0.60 inference(lemma, [status(cth), parent(t55:4), below(t48:3)], [t55:4]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t61, plain, E(s(0), f(z)),
% 0.32/0.60 inference(lemma_extension, [status(thm), parent(t55:5)], [l17:1]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t62, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t61:1)], [t61:1,t55:5]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t63, plain, E(s(0), f(z)),
% 0.32/0.60 inference(lemma_extension, [status(thm), parent(t55:6)], [l17:1]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t64, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t63:1)], [t63:1,t55:6]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t65, plain, iLEQ(suc(z), suc(z)),
% 0.32/0.60 inference(lemma_extension, [status(thm), parent(t55:7)], [l22:1]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t66, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t65:1)], [t65:1,t55:7]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t67, plain, E(s(0), f(z)),
% 0.32/0.60 inference(lemma_extension, [status(thm), parent(t55:8)], [l17:1]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t68, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t67:1)], [t67:1,t55:8]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t69, plain, $false,
% 0.32/0.60 inference(reduction, [status(thm), parent(t55:9)], [t55:9,t48:3]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t70, plain, E(s(0), f(suc(z))),
% 0.32/0.60 inference(lemma_extension, [status(thm), parent(t55:10)], [l21:1]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t71, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t70:1)], [t70:1,t55:10]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t72, plain, E(s(0), f(z)),
% 0.32/0.60 inference(lemma_extension, [status(thm), parent(t55:11)], [l17:1]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t73, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t72:1)], [t72:1,t55:11]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t74, plain, E(s(0), f(suc(z))),
% 0.32/0.60 inference(lemma_extension, [status(thm), parent(t55:12)], [l21:1]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t75, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t74:1)], [t74:1,t55:12]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t76, plain, E(s(0), f(suc(z))),
% 0.32/0.60 inference(lemma_extension, [status(thm), parent(t55:13)], [l21:1]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t77, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t76:1)], [t76:1,t55:13]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t78, plain, E(s(0), f(z)),
% 0.32/0.60 inference(lemma_extension, [status(thm), parent(t55:14)], [l17:1]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t79, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t78:1)], [t78:1,t55:14]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t80, plain, ( ~LE(f(z), 0) ),
% 0.32/0.60 inference(extension, [status(thm), parent(t42:3)], [clause_70]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t81, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t80:1)], [t80:1,t42:3]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t82, plain, ( E(0, f(suc(z))) | ~LE(f(suc(z)), s(0)) | LE(f(z), 0) ),
% 0.32/0.60 inference(extension, [status(thm), parent(t1:3)], [clause_117]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t83, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t82:1)], [t82:1,t1:3]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t84, plain, ( LE(f(suc(z)), s(0)) | ~LE(f(suc(suc(z))), s(s(0))) | E(s(0), f(suc(suc(z)))) ),
% 0.32/0.60 inference(extension, [status(thm), parent(t82:2)], [clause_83]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t85, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t84:1)], [t84:1,t82:2]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t86, plain, ( LE(f(suc(suc(z))), s(s(0))) ),
% 0.32/0.60 inference(extension, [status(thm), parent(t84:2)], [clause_58]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t87, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t86:1)], [t86:1,t84:2]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t88, plain, ( ~E(s(0), f(suc(suc(z)))) | ~E(s(0), f(suc(z))) | iLEQ(suc(suc(z)), suc(suc(z))) ),
% 0.32/0.60 inference(extension, [status(thm), parent(t84:3)], [clause_50]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t89, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t88:1)], [t88:1,t84:3]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t90, plain, ( E(s(0), f(suc(z))) | ~LE(f(suc(z)), s(s(0))) | LE(f(suc(z)), s(0)) ),
% 0.32/0.60 inference(extension, [status(thm), parent(t88:2)], [clause_20]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t91, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t90:1)], [t90:1,t88:2]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t92, plain, ( LE(f(suc(z)), s(s(0))) ),
% 0.32/0.60 inference(extension, [status(thm), parent(t90:2)], [clause_58]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t93, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t92:1)], [t92:1,t90:2]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t94, plain, $false,
% 0.32/0.60 inference(reduction, [status(thm), parent(t90:3)], [t90:3,t82:2]) ).
% 0.32/0.60
% 0.32/0.60 cnf(l29, lemma, E(s(0), f(suc(z))),
% 0.32/0.60 inference(lemma, [status(cth), parent(t88:2), below(t84:3)], [t88:2]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t95, plain, ( ~iLEQ(suc(suc(z)), suc(suc(z))) | ~E(s(0), f(suc(suc(z)))) | ~E(s(0), f(suc(suc(z)))) | ~iLEQ(suc(suc(z)), suc(suc(z))) | ~E(s(0), f(suc(z))) | ~E(s(0), f(suc(z))) | ~iLEQ(suc(suc(z)), suc(suc(z))) | ~E(s(0), f(suc(z))) | ~iLEQ(suc(suc(z)), suc(suc(z))) | ~E(s(0), f(suc(suc(z)))) | ~E(s(0), f(suc(z))) | ~E(s(0), f(suc(suc(z)))) | ~E(s(0), f(suc(suc(z)))) | ~E(s(0), f(suc(z))) ),
% 0.32/0.60 inference(extension, [status(thm), parent(t88:3)], [clause_37]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t96, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t95:1)], [t95:1,t88:3]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t97, plain, $false,
% 0.32/0.60 inference(reduction, [status(thm), parent(t95:2)], [t95:2,t84:3]) ).
% 0.32/0.60
% 0.32/0.60 cnf(l33, lemma, E(s(0), f(suc(suc(z)))),
% 0.32/0.60 inference(lemma, [status(cth), parent(t95:2), below(t88:3)], [t95:2]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t98, plain, E(s(0), f(suc(suc(z)))),
% 0.32/0.60 inference(lemma_extension, [status(thm), parent(t95:3)], [l33:1]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t99, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t98:1)], [t98:1,t95:3]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t100, plain, $false,
% 0.32/0.60 inference(reduction, [status(thm), parent(t95:4)], [t95:4,t88:3]) ).
% 0.32/0.60
% 0.32/0.60 cnf(l34, lemma, iLEQ(suc(suc(z)), suc(suc(z))),
% 0.32/0.60 inference(lemma, [status(cth), parent(t95:4), below(t88:3)], [t95:4]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t101, plain, E(s(0), f(suc(z))),
% 0.32/0.60 inference(lemma_extension, [status(thm), parent(t95:5)], [l29:1]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t102, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t101:1)], [t101:1,t95:5]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t103, plain, E(s(0), f(suc(z))),
% 0.32/0.60 inference(lemma_extension, [status(thm), parent(t95:6)], [l29:1]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t104, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t103:1)], [t103:1,t95:6]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t105, plain, iLEQ(suc(suc(z)), suc(suc(z))),
% 0.32/0.60 inference(lemma_extension, [status(thm), parent(t95:7)], [l34:1]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t106, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t105:1)], [t105:1,t95:7]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t107, plain, E(s(0), f(suc(z))),
% 0.32/0.60 inference(lemma_extension, [status(thm), parent(t95:8)], [l29:1]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t108, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t107:1)], [t107:1,t95:8]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t109, plain, $false,
% 0.32/0.60 inference(reduction, [status(thm), parent(t95:9)], [t95:9,t88:3]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t110, plain, E(s(0), f(suc(suc(z)))),
% 0.32/0.60 inference(lemma_extension, [status(thm), parent(t95:10)], [l33:1]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t111, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t110:1)], [t110:1,t95:10]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t112, plain, E(s(0), f(suc(z))),
% 0.32/0.60 inference(lemma_extension, [status(thm), parent(t95:11)], [l29:1]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t113, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t112:1)], [t112:1,t95:11]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t114, plain, E(s(0), f(suc(suc(z)))),
% 0.32/0.60 inference(lemma_extension, [status(thm), parent(t95:12)], [l33:1]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t115, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t114:1)], [t114:1,t95:12]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t116, plain, E(s(0), f(suc(suc(z)))),
% 0.32/0.60 inference(lemma_extension, [status(thm), parent(t95:13)], [l33:1]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t117, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t116:1)], [t116:1,t95:13]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t118, plain, E(s(0), f(suc(z))),
% 0.32/0.60 inference(lemma_extension, [status(thm), parent(t95:14)], [l29:1]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t119, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t118:1)], [t118:1,t95:14]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t120, plain, ( ~LE(f(z), 0) ),
% 0.32/0.60 inference(extension, [status(thm), parent(t82:3)], [clause_70]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t121, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t120:1)], [t120:1,t82:3]) ).
% 0.32/0.60
% 0.32/0.60 cnf(l25, lemma, E(0, f(suc(z))),
% 0.32/0.60 inference(lemma, [status(cth), parent(t1:3), below(0:0)], [t1:3]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t122, plain, ( E(0, f(z)) | ~LE(f(z), s(0)) | LE(f(z), 0) ),
% 0.32/0.60 inference(extension, [status(thm), parent(t1:4)], [clause_94]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t123, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t122:1)], [t122:1,t1:4]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t124, plain, ( LE(f(z), s(0)) | ~LE(f(suc(z)), s(s(0))) | E(s(0), f(suc(z))) ),
% 0.32/0.60 inference(extension, [status(thm), parent(t122:2)], [clause_83]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t125, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t124:1)], [t124:1,t122:2]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t126, plain, ( LE(f(suc(z)), s(s(0))) ),
% 0.32/0.60 inference(extension, [status(thm), parent(t124:2)], [clause_58]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t127, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t126:1)], [t126:1,t124:2]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t128, plain, ( ~E(s(0), f(suc(z))) | ~E(s(0), f(z)) | iLEQ(suc(z), suc(z)) ),
% 0.32/0.60 inference(extension, [status(thm), parent(t124:3)], [clause_50]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t129, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t128:1)], [t128:1,t124:3]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t130, plain, ( E(s(0), f(z)) | ~LE(f(z), s(s(0))) | LE(f(z), s(0)) ),
% 0.32/0.60 inference(extension, [status(thm), parent(t128:2)], [clause_20]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t131, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t130:1)], [t130:1,t128:2]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t132, plain, ( LE(f(z), s(s(0))) ),
% 0.32/0.60 inference(extension, [status(thm), parent(t130:2)], [clause_58]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t133, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t132:1)], [t132:1,t130:2]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t134, plain, $false,
% 0.32/0.60 inference(reduction, [status(thm), parent(t130:3)], [t130:3,t122:2]) ).
% 0.32/0.60
% 0.32/0.60 cnf(l41, lemma, E(s(0), f(z)),
% 0.32/0.60 inference(lemma, [status(cth), parent(t128:2), below(t124:3)], [t128:2]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t135, plain, ( ~iLEQ(suc(z), suc(z)) | ~E(s(0), f(suc(z))) | ~E(s(0), f(suc(z))) | ~iLEQ(suc(z), suc(z)) | ~E(s(0), f(z)) | ~E(s(0), f(z)) | ~iLEQ(suc(z), suc(z)) | ~E(s(0), f(z)) | ~iLEQ(suc(z), suc(z)) | ~E(s(0), f(suc(z))) | ~E(s(0), f(z)) | ~E(s(0), f(suc(z))) | ~E(s(0), f(suc(z))) | ~E(s(0), f(z)) ),
% 0.32/0.60 inference(extension, [status(thm), parent(t128:3)], [clause_37]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t136, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t135:1)], [t135:1,t128:3]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t137, plain, $false,
% 0.32/0.60 inference(reduction, [status(thm), parent(t135:2)], [t135:2,t124:3]) ).
% 0.32/0.60
% 0.32/0.60 cnf(l45, lemma, E(s(0), f(suc(z))),
% 0.32/0.60 inference(lemma, [status(cth), parent(t135:2), below(t128:3)], [t135:2]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t138, plain, E(s(0), f(suc(z))),
% 0.32/0.60 inference(lemma_extension, [status(thm), parent(t135:3)], [l45:1]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t139, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t138:1)], [t138:1,t135:3]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t140, plain, $false,
% 0.32/0.60 inference(reduction, [status(thm), parent(t135:4)], [t135:4,t128:3]) ).
% 0.32/0.60
% 0.32/0.60 cnf(l46, lemma, iLEQ(suc(z), suc(z)),
% 0.32/0.60 inference(lemma, [status(cth), parent(t135:4), below(t128:3)], [t135:4]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t141, plain, E(s(0), f(z)),
% 0.32/0.60 inference(lemma_extension, [status(thm), parent(t135:5)], [l41:1]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t142, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t141:1)], [t141:1,t135:5]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t143, plain, E(s(0), f(z)),
% 0.32/0.60 inference(lemma_extension, [status(thm), parent(t135:6)], [l41:1]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t144, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t143:1)], [t143:1,t135:6]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t145, plain, iLEQ(suc(z), suc(z)),
% 0.32/0.60 inference(lemma_extension, [status(thm), parent(t135:7)], [l46:1]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t146, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t145:1)], [t145:1,t135:7]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t147, plain, E(s(0), f(z)),
% 0.32/0.60 inference(lemma_extension, [status(thm), parent(t135:8)], [l41:1]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t148, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t147:1)], [t147:1,t135:8]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t149, plain, $false,
% 0.32/0.60 inference(reduction, [status(thm), parent(t135:9)], [t135:9,t128:3]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t150, plain, E(s(0), f(suc(z))),
% 0.32/0.60 inference(lemma_extension, [status(thm), parent(t135:10)], [l45:1]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t151, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t150:1)], [t150:1,t135:10]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t152, plain, E(s(0), f(z)),
% 0.32/0.60 inference(lemma_extension, [status(thm), parent(t135:11)], [l41:1]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t153, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t152:1)], [t152:1,t135:11]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t154, plain, E(s(0), f(suc(z))),
% 0.32/0.60 inference(lemma_extension, [status(thm), parent(t135:12)], [l45:1]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t155, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t154:1)], [t154:1,t135:12]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t156, plain, E(s(0), f(suc(z))),
% 0.32/0.60 inference(lemma_extension, [status(thm), parent(t135:13)], [l45:1]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t157, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t156:1)], [t156:1,t135:13]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t158, plain, E(s(0), f(z)),
% 0.32/0.60 inference(lemma_extension, [status(thm), parent(t135:14)], [l41:1]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t159, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t158:1)], [t158:1,t135:14]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t160, plain, ( ~LE(f(z), 0) ),
% 0.32/0.60 inference(extension, [status(thm), parent(t122:3)], [clause_70]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t161, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t160:1)], [t160:1,t122:3]) ).
% 0.32/0.60
% 0.32/0.60 cnf(l37, lemma, E(0, f(z)),
% 0.32/0.60 inference(lemma, [status(cth), parent(t1:4), below(0:0)], [t1:4]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t162, plain, E(0, f(suc(z))),
% 0.32/0.60 inference(lemma_extension, [status(thm), parent(t1:5)], [l25:1]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t163, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t162:1)], [t162:1,t1:5]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t164, plain, ( iLEQ(suc(z), suc(z)) | ~E(s(0), f(z)) | ~E(s(0), f(suc(z))) ),
% 0.32/0.60 inference(extension, [status(thm), parent(t1:6)], [clause_50]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t165, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t164:1)], [t164:1,t1:6]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t166, plain, ( E(s(0), f(z)) | ~LE(f(z), s(s(0))) | LE(f(z), s(0)) ),
% 0.32/0.60 inference(extension, [status(thm), parent(t164:2)], [clause_20]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t167, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t166:1)], [t166:1,t164:2]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t168, plain, ( LE(f(z), s(s(0))) ),
% 0.32/0.60 inference(extension, [status(thm), parent(t166:2)], [clause_58]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t169, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t168:1)], [t168:1,t166:2]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t170, plain, ( ~LE(f(z), s(0)) | LE(f(z), 0) | E(0, f(z)) ),
% 0.32/0.60 inference(extension, [status(thm), parent(t166:3)], [clause_94]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t171, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t170:1)], [t170:1,t166:3]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t172, plain, ( ~LE(f(z), 0) ),
% 0.32/0.60 inference(extension, [status(thm), parent(t170:2)], [clause_70]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t173, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t172:1)], [t172:1,t170:2]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t174, plain, ( ~E(0, f(z)) | iLEQ(suc(z), suc(z)) | ~E(0, f(suc(z))) ),
% 0.32/0.60 inference(extension, [status(thm), parent(t170:3)], [clause_6]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t175, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t174:1)], [t174:1,t170:3]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t176, plain, $false,
% 0.32/0.60 inference(reduction, [status(thm), parent(t174:2)], [t174:2,t1:6]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t177, plain, E(0, f(suc(z))),
% 0.32/0.60 inference(lemma_extension, [status(thm), parent(t174:3)], [l25:1]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t178, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t177:1)], [t177:1,t174:3]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t179, plain, ( E(s(0), f(suc(z))) | ~LE(f(suc(z)), s(s(0))) | LE(f(z), s(0)) ),
% 0.32/0.60 inference(extension, [status(thm), parent(t164:3)], [clause_83]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t180, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t179:1)], [t179:1,t164:3]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t181, plain, ( LE(f(suc(z)), s(s(0))) ),
% 0.32/0.60 inference(extension, [status(thm), parent(t179:2)], [clause_58]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t182, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t181:1)], [t181:1,t179:2]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t183, plain, ( ~LE(f(z), s(0)) | LE(f(z), 0) | E(0, f(z)) ),
% 0.32/0.60 inference(extension, [status(thm), parent(t179:3)], [clause_94]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t184, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t183:1)], [t183:1,t179:3]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t185, plain, ( ~LE(f(z), 0) ),
% 0.32/0.60 inference(extension, [status(thm), parent(t183:2)], [clause_70]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t186, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t185:1)], [t185:1,t183:2]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t187, plain, ( ~E(0, f(z)) | iLEQ(suc(z), suc(z)) | ~E(0, f(suc(z))) ),
% 0.32/0.60 inference(extension, [status(thm), parent(t183:3)], [clause_6]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t188, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t187:1)], [t187:1,t183:3]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t189, plain, $false,
% 0.32/0.60 inference(reduction, [status(thm), parent(t187:2)], [t187:2,t1:6]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t190, plain, E(0, f(suc(z))),
% 0.32/0.60 inference(lemma_extension, [status(thm), parent(t187:3)], [l25:1]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t191, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t190:1)], [t190:1,t187:3]) ).
% 0.32/0.60
% 0.32/0.60 cnf(l49, lemma, iLEQ(suc(z), suc(z)),
% 0.32/0.60 inference(lemma, [status(cth), parent(t1:6), below(0:0)], [t1:6]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t192, plain, E(0, f(z)),
% 0.32/0.60 inference(lemma_extension, [status(thm), parent(t1:7)], [l37:1]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t193, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t192:1)], [t192:1,t1:7]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t194, plain, iLEQ(suc(z), suc(z)),
% 0.32/0.60 inference(lemma_extension, [status(thm), parent(t1:8)], [l49:1]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t195, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t194:1)], [t194:1,t1:8]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t196, plain, ( E(0, f(z)) | ~LE(f(z), s(0)) | LE(f(z), 0) ),
% 0.32/0.60 inference(extension, [status(thm), parent(t1:9)], [clause_94]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t197, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t196:1)], [t196:1,t1:9]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t198, plain, ( LE(f(z), s(0)) | ~LE(f(suc(z)), s(s(0))) | E(s(0), f(suc(z))) ),
% 0.32/0.60 inference(extension, [status(thm), parent(t196:2)], [clause_83]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t199, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t198:1)], [t198:1,t196:2]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t200, plain, ( LE(f(suc(z)), s(s(0))) ),
% 0.32/0.60 inference(extension, [status(thm), parent(t198:2)], [clause_58]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t201, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t200:1)], [t200:1,t198:2]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t202, plain, ( ~E(s(0), f(suc(z))) | ~E(s(0), f(z)) | iLEQ(suc(z), suc(z)) ),
% 0.32/0.60 inference(extension, [status(thm), parent(t198:3)], [clause_50]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t203, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t202:1)], [t202:1,t198:3]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t204, plain, ( E(s(0), f(z)) | ~LE(f(z), s(s(0))) | LE(f(z), s(0)) ),
% 0.32/0.60 inference(extension, [status(thm), parent(t202:2)], [clause_20]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t205, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t204:1)], [t204:1,t202:2]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t206, plain, ( LE(f(z), s(s(0))) ),
% 0.32/0.60 inference(extension, [status(thm), parent(t204:2)], [clause_58]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t207, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t206:1)], [t206:1,t204:2]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t208, plain, $false,
% 0.32/0.60 inference(reduction, [status(thm), parent(t204:3)], [t204:3,t196:2]) ).
% 0.32/0.60
% 0.32/0.60 cnf(l66, lemma, E(s(0), f(z)),
% 0.32/0.60 inference(lemma, [status(cth), parent(t202:2), below(t198:3)], [t202:2]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t209, plain, ( ~iLEQ(suc(z), suc(z)) | ~E(s(0), f(suc(z))) | ~E(s(0), f(suc(z))) | ~iLEQ(suc(z), suc(z)) | ~E(s(0), f(z)) | ~E(s(0), f(z)) | ~iLEQ(suc(z), suc(z)) | ~E(s(0), f(z)) | ~iLEQ(suc(z), suc(z)) | ~E(s(0), f(suc(z))) | ~E(s(0), f(z)) | ~E(s(0), f(suc(z))) | ~E(s(0), f(suc(z))) | ~E(s(0), f(z)) ),
% 0.32/0.60 inference(extension, [status(thm), parent(t202:3)], [clause_37]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t210, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t209:1)], [t209:1,t202:3]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t211, plain, $false,
% 0.32/0.60 inference(reduction, [status(thm), parent(t209:2)], [t209:2,t198:3]) ).
% 0.32/0.60
% 0.32/0.60 cnf(l70, lemma, E(s(0), f(suc(z))),
% 0.32/0.60 inference(lemma, [status(cth), parent(t209:2), below(t202:3)], [t209:2]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t212, plain, E(s(0), f(suc(z))),
% 0.32/0.60 inference(lemma_extension, [status(thm), parent(t209:3)], [l70:1]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t213, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t212:1)], [t212:1,t209:3]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t214, plain, $false,
% 0.32/0.60 inference(reduction, [status(thm), parent(t209:4)], [t209:4,t202:3]) ).
% 0.32/0.60
% 0.32/0.60 cnf(l71, lemma, iLEQ(suc(z), suc(z)),
% 0.32/0.60 inference(lemma, [status(cth), parent(t209:4), below(t202:3)], [t209:4]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t215, plain, E(s(0), f(z)),
% 0.32/0.60 inference(lemma_extension, [status(thm), parent(t209:5)], [l66:1]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t216, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t215:1)], [t215:1,t209:5]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t217, plain, E(s(0), f(z)),
% 0.32/0.60 inference(lemma_extension, [status(thm), parent(t209:6)], [l66:1]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t218, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t217:1)], [t217:1,t209:6]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t219, plain, iLEQ(suc(z), suc(z)),
% 0.32/0.60 inference(lemma_extension, [status(thm), parent(t209:7)], [l71:1]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t220, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t219:1)], [t219:1,t209:7]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t221, plain, E(s(0), f(z)),
% 0.32/0.60 inference(lemma_extension, [status(thm), parent(t209:8)], [l66:1]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t222, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t221:1)], [t221:1,t209:8]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t223, plain, $false,
% 0.32/0.60 inference(reduction, [status(thm), parent(t209:9)], [t209:9,t202:3]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t224, plain, E(s(0), f(suc(z))),
% 0.32/0.60 inference(lemma_extension, [status(thm), parent(t209:10)], [l70:1]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t225, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t224:1)], [t224:1,t209:10]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t226, plain, E(s(0), f(z)),
% 0.32/0.60 inference(lemma_extension, [status(thm), parent(t209:11)], [l66:1]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t227, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t226:1)], [t226:1,t209:11]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t228, plain, E(s(0), f(suc(z))),
% 0.32/0.60 inference(lemma_extension, [status(thm), parent(t209:12)], [l70:1]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t229, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t228:1)], [t228:1,t209:12]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t230, plain, E(s(0), f(suc(z))),
% 0.32/0.60 inference(lemma_extension, [status(thm), parent(t209:13)], [l70:1]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t231, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t230:1)], [t230:1,t209:13]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t232, plain, E(s(0), f(z)),
% 0.32/0.60 inference(lemma_extension, [status(thm), parent(t209:14)], [l66:1]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t233, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t232:1)], [t232:1,t209:14]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t234, plain, ( ~LE(f(z), 0) ),
% 0.32/0.60 inference(extension, [status(thm), parent(t196:3)], [clause_70]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t235, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t234:1)], [t234:1,t196:3]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t236, plain, E(0, f(suc(z))),
% 0.32/0.60 inference(lemma_extension, [status(thm), parent(t1:10)], [l25:1]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t237, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t236:1)], [t236:1,t1:10]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t238, plain, iLEQ(suc(z), suc(z)),
% 0.32/0.60 inference(lemma_extension, [status(thm), parent(t1:11)], [l49:1]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t239, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t238:1)], [t238:1,t1:11]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t240, plain, iLEQ(suc(z), suc(z)),
% 0.32/0.60 inference(lemma_extension, [status(thm), parent(t1:12)], [l49:1]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t241, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t240:1)], [t240:1,t1:12]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t242, plain, E(0, f(suc(z))),
% 0.32/0.60 inference(lemma_extension, [status(thm), parent(t1:13)], [l25:1]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t243, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t242:1)], [t242:1,t1:13]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t244, plain, E(0, f(suc(z))),
% 0.32/0.60 inference(lemma_extension, [status(thm), parent(t1:14)], [l25:1]) ).
% 0.32/0.60
% 0.32/0.60 cnf(t245, plain, $false,
% 0.32/0.60 inference(connection, [status(thm), parent(t244:1)], [t244:1,t1:14]) ).
% 0.32/0.60
% 0.32/0.60 % SZS output end Proof for theBenchmark
%------------------------------------------------------------------------------