%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : SYO633-1 : TPTP v9.3.1. Released v7.1.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 : n001.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:12 AM UTC 2026
% Result : Unsatisfiable 0.08s 0.37s
% Output : Proof 0.08s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYO633-1 : TPTP v9.3.1. Released v7.1.0.
% 0.00/0.03 This is a CNF_UNS_RFO_NEQ_HRN problem
% 0.00/0.03 % Command : /export/starexec/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.34 % Computer : n001.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/0.34 % CPULimit : 300
% 0.08/0.34 % WCLimit : 300
% 0.08/0.34 % DateTime : Sun Sep 20 07:47:26 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.37 % SZS status Unsatisfiable for theBenchmark
% 0.08/0.37 % SZS output start Proof for theBenchmark
% 0.08/0.37 cnf(clause_5_03, axiom,
% 0.08/0.37 ( ~E(f(A_2), s(s(0))) | ~E(f(A_0), s(s(s(s(0))))) | ~E(f(A_1), s(s(s(0)))) | ~E(f(A_3), s(0)) | ~E(f(A_4), 0) | ~E(f(B_0), s(s(s(s(s(0)))))) ),
% 0.08/0.37 file('theBenchmark.p', clause_5_03) ).
% 0.08/0.37
% 0.08/0.37 cnf(clause_6_04, axiom,
% 0.08/0.37 ( E(f(B_0), s(s(s(s(0))))) ),
% 0.08/0.37 file('theBenchmark.p', clause_6_04) ).
% 0.08/0.37
% 0.08/0.37 cnf(clause_8_05, axiom,
% 0.08/0.37 ( E(f(B), s(s(s(s(s(0)))))) ),
% 0.08/0.37 file('theBenchmark.p', clause_8_05) ).
% 0.08/0.37
% 0.08/0.37 cnf(clause_2_07, axiom,
% 0.08/0.37 ( ~E(f(A_2), s(s(0))) | ~E(f(A_0), s(s(s(s(0))))) | ~E(f(A_1), s(s(s(0)))) | ~E(f(A_3), s(0)) | ~E(f(B_0), s(s(s(s(s(0)))))) | E(f(AP(s(s(s(s(s(s(0)))))), K)), 0) ),
% 0.08/0.37 file('theBenchmark.p', clause_2_07) ).
% 0.08/0.37
% 0.08/0.37 cnf(clause_12_09, axiom,
% 0.08/0.37 ( ~E(f(A_0), s(s(s(s(0))))) | ~E(f(B_0), s(s(s(s(s(0)))))) | ~E(f(A_1), s(s(s(0)))) | ~E(f(A_2), s(s(0))) | E(f(AP(s(s(s(s(s(s(0)))))), K)), s(0)) ),
% 0.08/0.37 file('theBenchmark.p', clause_12_09) ).
% 0.08/0.37
% 0.08/0.37 cnf(clause_1_10, axiom,
% 0.08/0.37 ( ~E(f(A_0), s(s(s(s(0))))) | ~E(f(B_0), s(s(s(s(s(0)))))) | E(f(B_0), s(s(s(0)))) ),
% 0.08/0.37 file('theBenchmark.p', clause_1_10) ).
% 0.08/0.37
% 0.08/0.37 cnf(clause_4_12, axiom,
% 0.08/0.37 ( ~E(f(A_0), s(s(s(s(0))))) | ~E(f(B_0), s(s(s(s(s(0)))))) | ~E(f(A_1), s(s(s(0)))) | E(f(AP(s(s(s(s(s(s(0)))))), K)), s(s(0))) ),
% 0.08/0.37 file('theBenchmark.p', clause_4_12) ).
% 0.08/0.37
% 0.08/0.37 cnf(t1, plain, ( ~E(f(AP(s(s(s(s(s(s(0)))))), U_276)), s(s(0))) | ~E(f(U_283), s(s(s(s(s(0)))))) | ~E(f(AP(s(s(s(s(s(s(0)))))), U_289)), 0) | ~E(f(AP(s(s(s(s(s(s(0)))))), U_331)), s(0)) | ~E(f(U_351), s(s(s(0)))) | ~E(f(U_352), s(s(s(s(0))))) ),
% 0.08/0.37 inference(start, [status(thm), parent(0:0)], [clause_5_03]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t2, plain, ( E(f(AP(s(s(s(s(s(s(0)))))), U_276)), s(s(0))) | ~E(f(U_277), s(s(s(s(0))))) | ~E(f(U_281), s(s(s(0)))) | ~E(f(U_282), s(s(s(s(s(0)))))) ),
% 0.08/0.37 inference(extension, [status(thm), parent(t1:1)], [clause_4_12]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t3, plain, $false,
% 0.08/0.37 inference(connection, [status(thm), parent(t2:1)], [t2:1,t1:1]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t4, plain, ( E(f(U_277), s(s(s(s(0))))) ),
% 0.08/0.37 inference(extension, [status(thm), parent(t2:2)], [clause_6_04]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t5, plain, $false,
% 0.08/0.37 inference(connection, [status(thm), parent(t4:1)], [t4:1,t2:2]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t6, plain, ( E(f(U_281), s(s(s(0)))) | ~E(f(U_280), s(s(s(s(0))))) | ~E(f(U_281), s(s(s(s(s(0)))))) ),
% 0.08/0.37 inference(extension, [status(thm), parent(t2:3)], [clause_1_10]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t7, plain, $false,
% 0.08/0.37 inference(connection, [status(thm), parent(t6:1)], [t6:1,t2:3]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t8, plain, ( E(f(U_280), s(s(s(s(0))))) ),
% 0.08/0.37 inference(extension, [status(thm), parent(t6:2)], [clause_6_04]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t9, plain, $false,
% 0.08/0.37 inference(connection, [status(thm), parent(t8:1)], [t8:1,t6:2]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t10, plain, ( E(f(U_281), s(s(s(s(s(0)))))) ),
% 0.08/0.37 inference(extension, [status(thm), parent(t6:3)], [clause_8_05]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t11, plain, $false,
% 0.08/0.37 inference(connection, [status(thm), parent(t10:1)], [t10:1,t6:3]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t12, plain, ( E(f(U_282), s(s(s(s(s(0)))))) ),
% 0.08/0.37 inference(extension, [status(thm), parent(t2:4)], [clause_8_05]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t13, plain, $false,
% 0.08/0.37 inference(connection, [status(thm), parent(t12:1)], [t12:1,t2:4]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t14, plain, ( E(f(U_283), s(s(s(s(s(0)))))) ),
% 0.08/0.37 inference(extension, [status(thm), parent(t1:2)], [clause_8_05]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t15, plain, $false,
% 0.08/0.37 inference(connection, [status(thm), parent(t14:1)], [t14:1,t1:2]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t16, plain, ( E(f(AP(s(s(s(s(s(s(0)))))), U_289)), 0) | ~E(f(AP(s(s(s(s(s(s(0)))))), U_293)), s(s(0))) | ~E(f(U_300), s(s(s(s(s(0)))))) | ~E(f(AP(s(s(s(s(s(s(0)))))), U_305)), s(0)) | ~E(f(U_325), s(s(s(0)))) | ~E(f(U_326), s(s(s(s(0))))) ),
% 0.08/0.37 inference(extension, [status(thm), parent(t1:3)], [clause_2_07]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t17, plain, $false,
% 0.08/0.37 inference(connection, [status(thm), parent(t16:1)], [t16:1,t1:3]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t18, plain, ( E(f(AP(s(s(s(s(s(s(0)))))), U_293)), s(s(0))) | ~E(f(U_294), s(s(s(s(0))))) | ~E(f(U_298), s(s(s(0)))) | ~E(f(U_299), s(s(s(s(s(0)))))) ),
% 0.08/0.37 inference(extension, [status(thm), parent(t16:2)], [clause_4_12]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t19, plain, $false,
% 0.08/0.37 inference(connection, [status(thm), parent(t18:1)], [t18:1,t16:2]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t20, plain, ( E(f(U_294), s(s(s(s(0))))) ),
% 0.08/0.37 inference(extension, [status(thm), parent(t18:2)], [clause_6_04]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t21, plain, $false,
% 0.08/0.37 inference(connection, [status(thm), parent(t20:1)], [t20:1,t18:2]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t22, plain, ( E(f(U_298), s(s(s(0)))) | ~E(f(U_297), s(s(s(s(0))))) | ~E(f(U_298), s(s(s(s(s(0)))))) ),
% 0.08/0.37 inference(extension, [status(thm), parent(t18:3)], [clause_1_10]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t23, plain, $false,
% 0.08/0.37 inference(connection, [status(thm), parent(t22:1)], [t22:1,t18:3]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t24, plain, ( E(f(U_297), s(s(s(s(0))))) ),
% 0.08/0.37 inference(extension, [status(thm), parent(t22:2)], [clause_6_04]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t25, plain, $false,
% 0.08/0.37 inference(connection, [status(thm), parent(t24:1)], [t24:1,t22:2]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t26, plain, ( E(f(U_298), s(s(s(s(s(0)))))) ),
% 0.08/0.37 inference(extension, [status(thm), parent(t22:3)], [clause_8_05]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t27, plain, $false,
% 0.08/0.37 inference(connection, [status(thm), parent(t26:1)], [t26:1,t22:3]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t28, plain, ( E(f(U_299), s(s(s(s(s(0)))))) ),
% 0.08/0.37 inference(extension, [status(thm), parent(t18:4)], [clause_8_05]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t29, plain, $false,
% 0.08/0.37 inference(connection, [status(thm), parent(t28:1)], [t28:1,t18:4]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t30, plain, ( E(f(U_300), s(s(s(s(s(0)))))) ),
% 0.08/0.37 inference(extension, [status(thm), parent(t16:3)], [clause_8_05]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t31, plain, $false,
% 0.08/0.37 inference(connection, [status(thm), parent(t30:1)], [t30:1,t16:3]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t32, plain, ( E(f(AP(s(s(s(s(s(s(0)))))), U_305)), s(0)) | ~E(f(U_306), s(s(s(s(0))))) | ~E(f(AP(s(s(s(s(s(s(0)))))), U_310)), s(s(0))) | ~E(f(U_320), s(s(s(0)))) | ~E(f(U_321), s(s(s(s(s(0)))))) ),
% 0.08/0.37 inference(extension, [status(thm), parent(t16:4)], [clause_12_09]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t33, plain, $false,
% 0.08/0.37 inference(connection, [status(thm), parent(t32:1)], [t32:1,t16:4]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t34, plain, ( E(f(U_306), s(s(s(s(0))))) ),
% 0.08/0.37 inference(extension, [status(thm), parent(t32:2)], [clause_6_04]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t35, plain, $false,
% 0.08/0.37 inference(connection, [status(thm), parent(t34:1)], [t34:1,t32:2]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t36, plain, ( E(f(AP(s(s(s(s(s(s(0)))))), U_310)), s(s(0))) | ~E(f(U_311), s(s(s(s(0))))) | ~E(f(U_315), s(s(s(0)))) | ~E(f(U_316), s(s(s(s(s(0)))))) ),
% 0.08/0.37 inference(extension, [status(thm), parent(t32:3)], [clause_4_12]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t37, plain, $false,
% 0.08/0.37 inference(connection, [status(thm), parent(t36:1)], [t36:1,t32:3]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t38, plain, ( E(f(U_311), s(s(s(s(0))))) ),
% 0.08/0.37 inference(extension, [status(thm), parent(t36:2)], [clause_6_04]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t39, plain, $false,
% 0.08/0.37 inference(connection, [status(thm), parent(t38:1)], [t38:1,t36:2]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t40, plain, ( E(f(U_315), s(s(s(0)))) | ~E(f(U_314), s(s(s(s(0))))) | ~E(f(U_315), s(s(s(s(s(0)))))) ),
% 0.08/0.37 inference(extension, [status(thm), parent(t36:3)], [clause_1_10]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t41, plain, $false,
% 0.08/0.37 inference(connection, [status(thm), parent(t40:1)], [t40:1,t36:3]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t42, plain, ( E(f(U_314), s(s(s(s(0))))) ),
% 0.08/0.37 inference(extension, [status(thm), parent(t40:2)], [clause_6_04]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t43, plain, $false,
% 0.08/0.37 inference(connection, [status(thm), parent(t42:1)], [t42:1,t40:2]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t44, plain, ( E(f(U_315), s(s(s(s(s(0)))))) ),
% 0.08/0.37 inference(extension, [status(thm), parent(t40:3)], [clause_8_05]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t45, plain, $false,
% 0.08/0.37 inference(connection, [status(thm), parent(t44:1)], [t44:1,t40:3]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t46, plain, ( E(f(U_316), s(s(s(s(s(0)))))) ),
% 0.08/0.37 inference(extension, [status(thm), parent(t36:4)], [clause_8_05]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t47, plain, $false,
% 0.08/0.37 inference(connection, [status(thm), parent(t46:1)], [t46:1,t36:4]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t48, plain, ( E(f(U_320), s(s(s(0)))) | ~E(f(U_319), s(s(s(s(0))))) | ~E(f(U_320), s(s(s(s(s(0)))))) ),
% 0.08/0.37 inference(extension, [status(thm), parent(t32:4)], [clause_1_10]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t49, plain, $false,
% 0.08/0.37 inference(connection, [status(thm), parent(t48:1)], [t48:1,t32:4]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t50, plain, ( E(f(U_319), s(s(s(s(0))))) ),
% 0.08/0.37 inference(extension, [status(thm), parent(t48:2)], [clause_6_04]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t51, plain, $false,
% 0.08/0.37 inference(connection, [status(thm), parent(t50:1)], [t50:1,t48:2]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t52, plain, ( E(f(U_320), s(s(s(s(s(0)))))) ),
% 0.08/0.37 inference(extension, [status(thm), parent(t48:3)], [clause_8_05]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t53, plain, $false,
% 0.08/0.37 inference(connection, [status(thm), parent(t52:1)], [t52:1,t48:3]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t54, plain, ( E(f(U_321), s(s(s(s(s(0)))))) ),
% 0.08/0.37 inference(extension, [status(thm), parent(t32:5)], [clause_8_05]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t55, plain, $false,
% 0.08/0.37 inference(connection, [status(thm), parent(t54:1)], [t54:1,t32:5]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t56, plain, ( E(f(U_325), s(s(s(0)))) | ~E(f(U_324), s(s(s(s(0))))) | ~E(f(U_325), s(s(s(s(s(0)))))) ),
% 0.08/0.37 inference(extension, [status(thm), parent(t16:5)], [clause_1_10]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t57, plain, $false,
% 0.08/0.37 inference(connection, [status(thm), parent(t56:1)], [t56:1,t16:5]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t58, plain, ( E(f(U_324), s(s(s(s(0))))) ),
% 0.08/0.37 inference(extension, [status(thm), parent(t56:2)], [clause_6_04]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t59, plain, $false,
% 0.08/0.37 inference(connection, [status(thm), parent(t58:1)], [t58:1,t56:2]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t60, plain, ( E(f(U_325), s(s(s(s(s(0)))))) ),
% 0.08/0.37 inference(extension, [status(thm), parent(t56:3)], [clause_8_05]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t61, plain, $false,
% 0.08/0.37 inference(connection, [status(thm), parent(t60:1)], [t60:1,t56:3]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t62, plain, ( E(f(U_326), s(s(s(s(0))))) ),
% 0.08/0.37 inference(extension, [status(thm), parent(t16:6)], [clause_6_04]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t63, plain, $false,
% 0.08/0.37 inference(connection, [status(thm), parent(t62:1)], [t62:1,t16:6]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t64, plain, ( E(f(AP(s(s(s(s(s(s(0)))))), U_331)), s(0)) | ~E(f(U_332), s(s(s(s(0))))) | ~E(f(AP(s(s(s(s(s(s(0)))))), U_336)), s(s(0))) | ~E(f(U_346), s(s(s(0)))) | ~E(f(U_347), s(s(s(s(s(0)))))) ),
% 0.08/0.37 inference(extension, [status(thm), parent(t1:4)], [clause_12_09]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t65, plain, $false,
% 0.08/0.37 inference(connection, [status(thm), parent(t64:1)], [t64:1,t1:4]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t66, plain, ( E(f(U_332), s(s(s(s(0))))) ),
% 0.08/0.37 inference(extension, [status(thm), parent(t64:2)], [clause_6_04]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t67, plain, $false,
% 0.08/0.37 inference(connection, [status(thm), parent(t66:1)], [t66:1,t64:2]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t68, plain, ( E(f(AP(s(s(s(s(s(s(0)))))), U_336)), s(s(0))) | ~E(f(U_337), s(s(s(s(0))))) | ~E(f(U_341), s(s(s(0)))) | ~E(f(U_342), s(s(s(s(s(0)))))) ),
% 0.08/0.37 inference(extension, [status(thm), parent(t64:3)], [clause_4_12]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t69, plain, $false,
% 0.08/0.37 inference(connection, [status(thm), parent(t68:1)], [t68:1,t64:3]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t70, plain, ( E(f(U_337), s(s(s(s(0))))) ),
% 0.08/0.37 inference(extension, [status(thm), parent(t68:2)], [clause_6_04]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t71, plain, $false,
% 0.08/0.37 inference(connection, [status(thm), parent(t70:1)], [t70:1,t68:2]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t72, plain, ( E(f(U_341), s(s(s(0)))) | ~E(f(U_340), s(s(s(s(0))))) | ~E(f(U_341), s(s(s(s(s(0)))))) ),
% 0.08/0.37 inference(extension, [status(thm), parent(t68:3)], [clause_1_10]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t73, plain, $false,
% 0.08/0.37 inference(connection, [status(thm), parent(t72:1)], [t72:1,t68:3]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t74, plain, ( E(f(U_340), s(s(s(s(0))))) ),
% 0.08/0.37 inference(extension, [status(thm), parent(t72:2)], [clause_6_04]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t75, plain, $false,
% 0.08/0.37 inference(connection, [status(thm), parent(t74:1)], [t74:1,t72:2]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t76, plain, ( E(f(U_341), s(s(s(s(s(0)))))) ),
% 0.08/0.37 inference(extension, [status(thm), parent(t72:3)], [clause_8_05]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t77, plain, $false,
% 0.08/0.37 inference(connection, [status(thm), parent(t76:1)], [t76:1,t72:3]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t78, plain, ( E(f(U_342), s(s(s(s(s(0)))))) ),
% 0.08/0.37 inference(extension, [status(thm), parent(t68:4)], [clause_8_05]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t79, plain, $false,
% 0.08/0.37 inference(connection, [status(thm), parent(t78:1)], [t78:1,t68:4]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t80, plain, ( E(f(U_346), s(s(s(0)))) | ~E(f(U_345), s(s(s(s(0))))) | ~E(f(U_346), s(s(s(s(s(0)))))) ),
% 0.08/0.37 inference(extension, [status(thm), parent(t64:4)], [clause_1_10]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t81, plain, $false,
% 0.08/0.37 inference(connection, [status(thm), parent(t80:1)], [t80:1,t64:4]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t82, plain, ( E(f(U_345), s(s(s(s(0))))) ),
% 0.08/0.37 inference(extension, [status(thm), parent(t80:2)], [clause_6_04]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t83, plain, $false,
% 0.08/0.37 inference(connection, [status(thm), parent(t82:1)], [t82:1,t80:2]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t84, plain, ( E(f(U_346), s(s(s(s(s(0)))))) ),
% 0.08/0.37 inference(extension, [status(thm), parent(t80:3)], [clause_8_05]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t85, plain, $false,
% 0.08/0.37 inference(connection, [status(thm), parent(t84:1)], [t84:1,t80:3]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t86, plain, ( E(f(U_347), s(s(s(s(s(0)))))) ),
% 0.08/0.37 inference(extension, [status(thm), parent(t64:5)], [clause_8_05]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t87, plain, $false,
% 0.08/0.37 inference(connection, [status(thm), parent(t86:1)], [t86:1,t64:5]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t88, plain, ( E(f(U_351), s(s(s(0)))) | ~E(f(U_350), s(s(s(s(0))))) | ~E(f(U_351), s(s(s(s(s(0)))))) ),
% 0.08/0.37 inference(extension, [status(thm), parent(t1:5)], [clause_1_10]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t89, plain, $false,
% 0.08/0.37 inference(connection, [status(thm), parent(t88:1)], [t88:1,t1:5]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t90, plain, ( E(f(U_350), s(s(s(s(0))))) ),
% 0.08/0.37 inference(extension, [status(thm), parent(t88:2)], [clause_6_04]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t91, plain, $false,
% 0.08/0.37 inference(connection, [status(thm), parent(t90:1)], [t90:1,t88:2]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t92, plain, ( E(f(U_351), s(s(s(s(s(0)))))) ),
% 0.08/0.37 inference(extension, [status(thm), parent(t88:3)], [clause_8_05]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t93, plain, $false,
% 0.08/0.37 inference(connection, [status(thm), parent(t92:1)], [t92:1,t88:3]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t94, plain, ( E(f(U_352), s(s(s(s(0))))) ),
% 0.08/0.37 inference(extension, [status(thm), parent(t1:6)], [clause_6_04]) ).
% 0.08/0.37
% 0.08/0.37 cnf(t95, plain, $false,
% 0.08/0.37 inference(connection, [status(thm), parent(t94:1)], [t94:1,t1:6]) ).
% 0.08/0.37
% 0.08/0.37 % SZS output end Proof for theBenchmark
%------------------------------------------------------------------------------