%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : MED003+1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n011.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 : Fri Sep 25 02:11:07 PM UTC 2026
% Result : Theorem 21.70s 3.28s
% Output : Proof 21.70s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MED003+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.08/0.36 % Computer : n011.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Thu Sep 24 00:54:12 UTC 2026
% 0.08/0.37 % CPUTime :
% 0.08/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 21.70/3.28 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 21.70/3.28 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 21.70/3.28 fof(sdef1, definition, (spl1 <=> (conditionhypo(sk14))), introduced(definition, [new_symbols(naming, [spl1])], [avatar_definition])).
% 21.70/3.28 cnf(p64, plain, (conditionhypo(sk14) | ~spl1), inference(avatar_component_clause, [status(thm)], [sdef1])).
% 21.70/3.28 fof(f18, conjecture, ( ( ! [X0] : ( ~ gt(n0,X0) => drugi(X0) ) & ! [X0] : ( gt(n0,X0) => conditionhyper(X0) ) & bcapacityex(n0) ) => ! [X0] : ( ~ gt(n0,X0) => ( conditionnormo(X0) | conditionhypo(X0) ) ) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', treatmentex)).
% 21.70/3.28 fof(f18_neg, negated_conjecture, ~(( ( ! [X0] : ( ~ gt(n0,X0) => drugi(X0) ) & ! [X0] : ( gt(n0,X0) => conditionhyper(X0) ) & bcapacityex(n0) ) => ! [X0] : ( ~ gt(n0,X0) => ( conditionnormo(X0) | conditionhypo(X0) ) ) )), inference(negated_conjecture, [status(cth)], [f18])).
% 21.70/3.28 fof(f18_nnf, plain, (((! [X0] : ((gt(n0,X0) | drugi(X0))) & ! [X0] : ((~(gt(n0,X0)) | conditionhyper(X0)))) & bcapacityex(n0)) & ? [X0] : ((~(gt(n0,X0)) & (~(conditionnormo(X0)) & ~(conditionhypo(X0)))))), inference(nnf_transformation, [status(thm)], [f18_neg])).
% 21.70/3.28 fof(f18_sk, plain, ! [X0] : (((((gt(n0,X0) | drugi(X0)) & (~(gt(n0,X0)) | conditionhyper(X0))) & bcapacityex(n0)) & (~(gt(n0,sk14)) & (~(conditionnormo(sk14)) & ~(conditionhypo(sk14)))))), inference(skolemisation, [status(esa), new_symbols(skolem, [sk14])], [f18_nnf])).
% 21.70/3.28 cnf(c56, plain, ~conditionhypo(sk14), inference(cnf_transformation, [status(esa)], [f18_sk])).
% 21.70/3.28 cnf(p65, plain, ($false | ~spl1), inference(resolution, [status(thm)], [p64, c56])).
% 21.70/3.28 cnf(sct0, plain, (~spl1), inference(avatar_contradiction_clause, [status(thm)], [p65])).
% 21.70/3.28 fof(sdef4, definition, (spl4 <=> (gt(X0,sk14))), introduced(definition, [new_symbols(naming, [spl4])], [avatar_definition])).
% 21.70/3.28 cnf(p74, plain, (gt(X0,sk14) | ~spl4), inference(avatar_component_clause, [status(thm)], [sdef4])).
% 21.70/3.28 cnf(c54, plain, ~gt(n0,sk14), inference(cnf_transformation, [status(esa)], [f18_sk])).
% 21.70/3.28 cnf(p83, plain, ($false | ~spl4), inference(resolution, [status(thm)], [p74, c54])).
% 21.70/3.28 cnf(sct1, plain, (~spl4), inference(avatar_contradiction_clause, [status(thm)], [p83])).
% 21.70/3.28 fof(sdef6, definition, (spl6 <=> (gt(X0,n0))), introduced(definition, [new_symbols(naming, [spl6])], [avatar_definition])).
% 21.70/3.28 cnf(p77, plain, (gt(X0,n0) | ~spl6), inference(avatar_component_clause, [status(thm)], [sdef6])).
% 21.70/3.28 fof(f0, axiom, ! [X] : ~ gt(X,X), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', irreflexivity_gt)).
% 21.70/3.28 fof(f0_nnf, plain, ! [X] : (~(gt(X,X))), inference(nnf_transformation, [status(thm)], [f0])).
% 21.70/3.28 fof(f0_sk, plain, ! [X] : (~(gt(X,X))), inference(skolemisation, [status(esa)], [f0_nnf])).
% 21.70/3.28 cnf(c0, plain, ~gt(X0,X0), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 21.70/3.28 cnf(p84, plain, ($false | ~spl6), inference(resolution, [status(thm)], [p77, c0])).
% 21.70/3.28 cnf(sct2, plain, (~spl6), inference(avatar_contradiction_clause, [status(thm)], [p84])).
% 21.70/3.28 fof(sdef10, definition, (spl10 <=> (gt(X0,sk0(n0)))), introduced(definition, [new_symbols(naming, [spl10])], [avatar_definition])).
% 21.70/3.28 cnf(p88, plain, (gt(X0,sk0(n0)) | ~spl10), inference(avatar_component_clause, [status(thm)], [sdef10])).
% 21.70/3.28 cnf(p90, plain, ($false | ~spl10), inference(resolution, [status(thm)], [p88, c0])).
% 21.70/3.28 cnf(sct3, plain, (~spl10), inference(avatar_contradiction_clause, [status(thm)], [p90])).
% 21.70/3.28 fof(sdef17, definition, (spl17 <=> (gt(X0,sk2(n0)))), introduced(definition, [new_symbols(naming, [spl17])], [avatar_definition])).
% 21.70/3.28 cnf(p121, plain, (gt(X0,sk2(n0)) | ~spl17), inference(avatar_component_clause, [status(thm)], [sdef17])).
% 21.70/3.28 cnf(p123, plain, ($false | ~spl17), inference(resolution, [status(thm)], [p121, c0])).
% 21.70/3.28 cnf(sct4, plain, (~spl17), inference(avatar_contradiction_clause, [status(thm)], [p123])).
% 21.70/3.28 fof(sdef29, definition, (spl29 <=> (gt(n0,sk10(n0)))), introduced(definition, [new_symbols(naming, [spl29])], [avatar_definition])).
% 21.70/3.28 cnf(p192, plain, (gt(n0,sk10(n0)) | ~spl29), inference(avatar_component_clause, [status(thm)], [sdef29])).
% 21.70/3.28 cnf(c52, plain, ~gt(n0,X0) | conditionhyper(X0), inference(cnf_transformation, [status(esa)], [f18_sk])).
% 21.70/3.28 cnf(p249, plain, (conditionhyper(sk10(n0)) | ~spl29), inference(resolution, [status(thm)], [p192, c52])).
% 21.70/3.28 fof(sdef36, definition, (spl36 <=> (~conditionhyper(sk10(n0)))), introduced(definition, [new_symbols(naming, [spl36])], [avatar_definition])).
% 21.70/3.28 cnf(p208, plain, (~conditionhyper(sk10(n0)) | ~spl36), inference(avatar_component_clause, [status(thm)], [sdef36])).
% 21.70/3.28 cnf(p255, plain, ($false | ~spl29 | ~spl36), inference(resolution, [status(thm)], [p249, p208])).
% 21.70/3.28 cnf(sct5, plain, (~spl29 | ~spl36), inference(avatar_contradiction_clause, [status(thm)], [p255])).
% 21.70/3.28 fof(sdef34, definition, (spl34 <=> (gt(X0,sk7(n0)))), introduced(definition, [new_symbols(naming, [spl34])], [avatar_definition])).
% 21.70/3.28 cnf(p205, plain, (gt(X0,sk7(n0)) | ~spl34), inference(avatar_component_clause, [status(thm)], [sdef34])).
% 21.70/3.28 cnf(p256, plain, ($false | ~spl34), inference(resolution, [status(thm)], [p205, c0])).
% 21.70/3.28 cnf(sct6, plain, (~spl34), inference(avatar_contradiction_clause, [status(thm)], [p256])).
% 21.70/3.28 fof(sdef40, definition, (spl40 <=> (gt(X0,sk9(n0)))), introduced(definition, [new_symbols(naming, [spl40])], [avatar_definition])).
% 21.70/3.28 cnf(p236, plain, (gt(X0,sk9(n0)) | ~spl40), inference(avatar_component_clause, [status(thm)], [sdef40])).
% 21.70/3.28 cnf(p257, plain, ($false | ~spl40), inference(resolution, [status(thm)], [p236, c0])).
% 21.70/3.28 cnf(sct7, plain, (~spl40), inference(avatar_contradiction_clause, [status(thm)], [p257])).
% 21.70/3.28 fof(sdef30, definition, (spl30 <=> (gt(n0,X0) | conditionnormo(X0))), introduced(definition, [new_symbols(naming, [spl30])], [avatar_definition])).
% 21.70/3.28 cnf(p193, plain, (gt(n0,X0) | conditionnormo(X0) | ~spl30), inference(avatar_component_clause, [status(thm)], [sdef30])).
% 21.70/3.28 cnf(p258, plain, (conditionnormo(sk14) | ~spl30), inference(resolution, [status(thm)], [p193, c54])).
% 21.70/3.28 cnf(c55, plain, ~conditionnormo(sk14), inference(cnf_transformation, [status(esa)], [f18_sk])).
% 21.70/3.28 cnf(p269, plain, ($false | ~spl30), inference(resolution, [status(thm)], [p258, c55])).
% 21.70/3.28 cnf(sct8, plain, (~spl30), inference(avatar_contradiction_clause, [status(thm)], [p269])).
% 21.70/3.28 fof(sdef43, definition, (spl43 <=> (conditionnormo(sk0(n0)))), introduced(definition, [new_symbols(naming, [spl43])], [avatar_definition])).
% 21.70/3.28 cnf(p263, plain, (conditionnormo(sk0(n0)) | ~spl43), inference(avatar_component_clause, [status(thm)], [sdef43])).
% 21.70/3.28 fof(sdef20, definition, (spl20 <=> (conditionhyper(sk0(n0)))), introduced(definition, [new_symbols(naming, [spl20])], [avatar_definition])).
% 21.70/3.28 cnf(p127, plain, (conditionhyper(sk0(n0)) | ~spl20), inference(avatar_component_clause, [status(thm)], [sdef20])).
% 21.70/3.28 fof(f8, axiom, ! [X0] : ( ~ conditionhyper(X0) | ~ conditionnormo(X0) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', xorcondition3)).
% 21.70/3.28 fof(f8_nnf, plain, ! [X0] : ((~(conditionhyper(X0)) | ~(conditionnormo(X0)))), inference(nnf_transformation, [status(thm)], [f8])).
% 21.70/3.28 fof(f8_sk, plain, ! [X0] : ((~(conditionhyper(X0)) | ~(conditionnormo(X0)))), inference(skolemisation, [status(esa)], [f8_nnf])).
% 21.70/3.28 cnf(c8, plain, ~conditionhyper(X0) | ~conditionnormo(X0), inference(cnf_transformation, [status(esa)], [f8_sk])).
% 21.70/3.28 cnf(p142, plain, (~conditionnormo(sk0(n0)) | ~spl20), inference(resolution, [status(thm)], [p127, c8])).
% 21.70/3.28 cnf(p271, plain, ($false | ~spl20 | ~spl43), inference(resolution, [status(thm)], [p263, p142])).
% 21.70/3.28 cnf(sct9, plain, (~spl20 | ~spl43), inference(avatar_contradiction_clause, [status(thm)], [p271])).
% 21.70/3.28 fof(sdef46, definition, (spl46 <=> (conditionhyper(sk10(n0)))), introduced(definition, [new_symbols(naming, [spl46])], [avatar_definition])).
% 21.70/3.28 cnf(p274, plain, (conditionhyper(sk10(n0)) | ~spl46), inference(avatar_component_clause, [status(thm)], [sdef46])).
% 21.70/3.28 cnf(p279, plain, ($false | ~spl36 | ~spl46), inference(resolution, [status(thm)], [p274, p208])).
% 21.70/3.28 cnf(sct10, plain, (~spl36 | ~spl46), inference(avatar_contradiction_clause, [status(thm)], [p279])).
% 21.70/3.28 fof(sdef50, definition, (spl50 <=> (gt(X0,sk8(n0)))), introduced(definition, [new_symbols(naming, [spl50])], [avatar_definition])).
% 21.70/3.28 cnf(p295, plain, (gt(X0,sk8(n0)) | ~spl50), inference(avatar_component_clause, [status(thm)], [sdef50])).
% 21.70/3.28 cnf(p305, plain, ($false | ~spl50), inference(resolution, [status(thm)], [p295, c0])).
% 21.70/3.28 cnf(sct11, plain, (~spl50), inference(avatar_contradiction_clause, [status(thm)], [p305])).
% 21.70/3.28 fof(sdef52, definition, (spl52 <=> (conditionnormo(sk14))), introduced(definition, [new_symbols(naming, [spl52])], [avatar_definition])).
% 21.70/3.28 cnf(p316, plain, (conditionnormo(sk14) | ~spl52), inference(avatar_component_clause, [status(thm)], [sdef52])).
% 21.70/3.28 cnf(p326, plain, ($false | ~spl52), inference(resolution, [status(thm)], [p316, c55])).
% 21.70/3.28 cnf(sct12, plain, (~spl52), inference(avatar_contradiction_clause, [status(thm)], [p326])).
% 21.70/3.28 fof(sdef64, definition, (spl64 <=> (~bcapacityex(n0))), introduced(definition, [new_symbols(naming, [spl64])], [avatar_definition])).
% 21.70/3.28 cnf(p405, plain, (~bcapacityex(n0) | ~spl64), inference(avatar_component_clause, [status(thm)], [sdef64])).
% 21.70/3.28 cnf(c53, plain, bcapacityex(n0), inference(cnf_transformation, [status(esa)], [f18_sk])).
% 21.70/3.28 cnf(p420, plain, ($false | ~spl64), inference(resolution, [status(thm)], [p405, c53])).
% 21.70/3.28 cnf(sct13, plain, (~spl64), inference(avatar_contradiction_clause, [status(thm)], [p420])).
% 21.70/3.28 fof(sdef63, definition, (spl63 <=> (~gt(n0,sk12(n0)))), introduced(definition, [new_symbols(naming, [spl63])], [avatar_definition])).
% 21.70/3.28 cnf(p404, plain, (~gt(n0,sk12(n0)) | ~spl63), inference(avatar_component_clause, [status(thm)], [sdef63])).
% 21.70/3.28 fof(sdef8, definition, (spl8 <=> (gt(n0,X0) | uptakepg(X0))), introduced(definition, [new_symbols(naming, [spl8])], [avatar_definition])).
% 21.70/3.28 cnf(p80, plain, (gt(n0,X0) | uptakepg(X0) | ~spl8), inference(avatar_component_clause, [status(thm)], [sdef8])).
% 21.70/3.28 cnf(p474, plain, (uptakepg(sk12(n0)) | ~spl8 | ~spl63), inference(resolution, [status(thm)], [p404, p80])).
% 21.70/3.28 fof(sdef74, definition, (spl74 <=> (~uptakepg(sk12(n0)))), introduced(definition, [new_symbols(naming, [spl74])], [avatar_definition])).
% 21.70/3.28 cnf(p436, plain, (~uptakepg(sk12(n0)) | ~spl74), inference(avatar_component_clause, [status(thm)], [sdef74])).
% 21.70/3.28 cnf(p485, plain, ($false | ~spl8 | ~spl63 | ~spl74), inference(resolution, [status(thm)], [p474, p436])).
% 21.70/3.28 cnf(sct14, plain, (~spl8 | ~spl63 | ~spl74), inference(avatar_contradiction_clause, [status(thm)], [p485])).
% 21.70/3.28 fof(sdef76, definition, (spl76 <=> (uptakepg(sk12(n0)))), introduced(definition, [new_symbols(naming, [spl76])], [avatar_definition])).
% 21.70/3.28 cnf(p480, plain, (uptakepg(sk12(n0)) | ~spl76), inference(avatar_component_clause, [status(thm)], [sdef76])).
% 21.70/3.28 cnf(p491, plain, ($false | ~spl74 | ~spl76), inference(resolution, [status(thm)], [p480, p436])).
% 21.70/3.28 cnf(sct15, plain, (~spl74 | ~spl76), inference(avatar_contradiction_clause, [status(thm)], [p491])).
% 21.70/3.28 fof(sdef65, definition, (spl65 <=> (gt(n0,sk13(n0)))), introduced(definition, [new_symbols(naming, [spl65])], [avatar_definition])).
% 21.70/3.28 cnf(p406, plain, (gt(n0,sk13(n0)) | ~spl65), inference(avatar_component_clause, [status(thm)], [sdef65])).
% 21.70/3.28 cnf(p492, plain, (conditionhyper(sk13(n0)) | ~spl65), inference(resolution, [status(thm)], [p406, c52])).
% 21.70/3.28 fof(sdef71, definition, (spl71 <=> (~conditionhyper(sk13(n0)))), introduced(definition, [new_symbols(naming, [spl71])], [avatar_definition])).
% 21.70/3.28 cnf(p422, plain, (~conditionhyper(sk13(n0)) | ~spl71), inference(avatar_component_clause, [status(thm)], [sdef71])).
% 21.70/3.28 cnf(p502, plain, ($false | ~spl65 | ~spl71), inference(resolution, [status(thm)], [p492, p422])).
% 21.70/3.28 cnf(sct16, plain, (~spl65 | ~spl71), inference(avatar_contradiction_clause, [status(thm)], [p502])).
% 21.70/3.28 fof(sdef72, definition, (spl72 <=> (gt(X0,sk11(n0)))), introduced(definition, [new_symbols(naming, [spl72])], [avatar_definition])).
% 21.70/3.28 cnf(p432, plain, (gt(X0,sk11(n0)) | ~spl72), inference(avatar_component_clause, [status(thm)], [sdef72])).
% 21.70/3.28 cnf(p503, plain, ($false | ~spl72), inference(resolution, [status(thm)], [p432, c0])).
% 21.70/3.28 cnf(sct17, plain, (~spl72), inference(avatar_contradiction_clause, [status(thm)], [p503])).
% 21.70/3.28 fof(sdef77, definition, (spl77 <=> (gt(X0,sk12(n0)))), introduced(definition, [new_symbols(naming, [spl77])], [avatar_definition])).
% 21.70/3.28 cnf(p483, plain, (gt(X0,sk12(n0)) | ~spl77), inference(avatar_component_clause, [status(thm)], [sdef77])).
% 21.70/3.28 cnf(p508, plain, ($false | ~spl77), inference(resolution, [status(thm)], [p483, c0])).
% 21.70/3.28 cnf(sct18, plain, (~spl77), inference(avatar_contradiction_clause, [status(thm)], [p508])).
% 21.70/3.28 fof(sdef83, definition, (spl83 <=> (gt(X0,sk1(sk13(n0))))), introduced(definition, [new_symbols(naming, [spl83])], [avatar_definition])).
% 21.70/3.28 cnf(p527, plain, (gt(X0,sk1(sk13(n0))) | ~spl83), inference(avatar_component_clause, [status(thm)], [sdef83])).
% 21.70/3.28 cnf(p530, plain, ($false | ~spl83), inference(resolution, [status(thm)], [p527, c0])).
% 21.70/3.28 cnf(sct19, plain, (~spl83), inference(avatar_contradiction_clause, [status(thm)], [p530])).
% 21.70/3.28 fof(f10, axiom, ! [X0] : ( ! [X1] : ( ~ gt(X0,X1) => drugi(X1) ) => ! [X1] : ( ~ gt(X0,X1) => ( uptakelg(X1) & uptakepg(X1) ) ) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', insulin_effect)).
% 21.70/3.28 fof(f10_nnf, plain, ! [X0] : ((? [X1] : ((~(gt(X0,X1)) & ~(drugi(X1)))) | ! [X1] : ((gt(X0,X1) | (uptakelg(X1) & uptakepg(X1)))))), inference(nnf_transformation, [status(thm)], [f10])).
% 21.70/3.28 fof(f10_sk, plain, ! [X0,X1] : (((~(gt(X0,sk0(X0))) & ~(drugi(sk0(X0)))) | (gt(X0,X1) | (uptakelg(X1) & uptakepg(X1))))), inference(skolemisation, [status(esa), new_symbols(skolem, [sk0])], [f10_nnf])).
% 21.70/3.28 cnf(c13, plain, ~drugi(sk0(X0)) | gt(X0,X1) | uptakepg(X1), inference(cnf_transformation, [status(esa)], [f10_sk])).
% 21.70/3.28 fof(sdef3, definition, (spl3 <=> (drugi(sk0(n0)))), introduced(definition, [new_symbols(naming, [spl3])], [avatar_definition])).
% 21.70/3.28 cnf(p68, plain, (drugi(sk0(n0)) | ~spl3), inference(avatar_component_clause, [status(thm)], [sdef3])).
% 21.70/3.28 cnf(p93, plain, (gt(n0,X0) | uptakepg(X0) | ~spl3), inference(resolution, [status(thm)], [c13, p68])).
% 21.70/3.28 cnf(p476, plain, (uptakepg(sk12(n0)) | ~spl3 | ~spl63), inference(resolution, [status(thm)], [p404, p93])).
% 21.70/3.28 cnf(p571, plain, ($false | ~spl3 | ~spl63 | ~spl74), inference(resolution, [status(thm)], [p476, p436])).
% 21.70/3.28 cnf(sct20, plain, (~spl3 | ~spl63 | ~spl74), inference(avatar_contradiction_clause, [status(thm)], [p571])).
% 21.70/3.28 fof(f6, axiom, ! [X0] : ( conditionhyper(X0) | conditionhypo(X0) | conditionnormo(X0) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', xorcondition1)).
% 21.70/3.28 fof(f6_nnf, plain, ! [X0] : (((conditionhyper(X0) | conditionhypo(X0)) | conditionnormo(X0))), inference(nnf_transformation, [status(thm)], [f6])).
% 21.70/3.28 fof(f6_sk, plain, ! [X0] : (((conditionhyper(X0) | conditionhypo(X0)) | conditionnormo(X0))), inference(skolemisation, [status(esa)], [f6_nnf])).
% 21.70/3.28 cnf(c6, plain, conditionhyper(X0) | conditionhypo(X0) | conditionnormo(X0), inference(cnf_transformation, [status(esa)], [f6_sk])).
% 21.70/3.28 cnf(p62, plain, conditionhyper(sk14) | conditionhypo(sk14), inference(resolution, [status(thm)], [c6, c55])).
% 21.70/3.28 fof(sdef0, definition, (spl0 <=> (conditionhyper(sk14))), introduced(definition, [new_symbols(naming, [spl0])], [avatar_definition])).
% 21.70/3.28 cnf(ssp0, plain, (spl0 | spl1), inference(avatar_split_clause, [status(thm)], [p62, sdef0, sdef1])).
% 21.70/3.28 cnf(c10, plain, ~gt(X0,sk0(X0)) | gt(X0,X1) | uptakelg(X1), inference(cnf_transformation, [status(esa)], [f10_sk])).
% 21.70/3.28 cnf(c51, plain, gt(n0,X0) | drugi(X0), inference(cnf_transformation, [status(esa)], [f18_sk])).
% 21.70/3.28 cnf(p66, plain, gt(n0,X0) | uptakelg(X0) | drugi(sk0(n0)), inference(resolution, [status(thm)], [c10, c51])).
% 21.70/3.28 fof(sdef2, definition, (spl2 <=> (gt(n0,X0) | uptakelg(X0))), introduced(definition, [new_symbols(naming, [spl2])], [avatar_definition])).
% 21.70/3.28 cnf(ssp1, plain, (spl2 | spl3), inference(avatar_split_clause, [status(thm)], [p66, sdef2, sdef3])).
% 21.70/3.28 cnf(p67, plain, (gt(n0,X0) | uptakelg(X0) | ~spl2), inference(avatar_component_clause, [status(thm)], [sdef2])).
% 21.70/3.28 cnf(p69, plain, (uptakelg(sk14) | ~spl2), inference(resolution, [status(thm)], [p67, c54])).
% 21.70/3.28 fof(f11, axiom, ! [X0,X1] : ( ~ gt(X0,X1) => ( uptakelg(X1) => ~ releaselg(X1) ) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', liver_glucose)).
% 21.70/3.28 fof(f11_nnf, plain, ! [X0,X1] : ((gt(X0,X1) | (~(uptakelg(X1)) | ~(releaselg(X1))))), inference(nnf_transformation, [status(thm)], [f11])).
% 21.70/3.28 fof(f11_sk, plain, ! [X0,X1] : ((gt(X0,X1) | (~(uptakelg(X1)) | ~(releaselg(X1))))), inference(skolemisation, [status(esa)], [f11_nnf])).
% 21.70/3.28 cnf(c14, plain, gt(X0,X1) | ~uptakelg(X1) | ~releaselg(X1), inference(cnf_transformation, [status(esa)], [f11_sk])).
% 21.70/3.28 cnf(p73, plain, (gt(X0,sk14) | ~releaselg(sk14) | ~spl2), inference(resolution, [status(thm)], [p69, c14])).
% 21.70/3.28 fof(sdef5, definition, (spl5 <=> (~releaselg(sk14))), introduced(definition, [new_symbols(naming, [spl5])], [avatar_definition])).
% 21.70/3.28 cnf(ssp2, plain, (~spl2 | spl4 | spl5), inference(avatar_split_clause, [status(thm)], [p73, sdef4, sdef5])).
% 21.70/3.28 cnf(p70, plain, (uptakelg(n0) | ~spl2), inference(resolution, [status(thm)], [p67, c0])).
% 21.70/3.28 cnf(p76, plain, (gt(X0,n0) | ~releaselg(n0) | ~spl2), inference(resolution, [status(thm)], [p70, c14])).
% 21.70/3.28 fof(sdef7, definition, (spl7 <=> (~releaselg(n0))), introduced(definition, [new_symbols(naming, [spl7])], [avatar_definition])).
% 21.70/3.28 cnf(ssp3, plain, (~spl2 | spl6 | spl7), inference(avatar_split_clause, [status(thm)], [p76, sdef6, sdef7])).
% 21.70/3.28 cnf(c11, plain, ~gt(X0,sk0(X0)) | gt(X0,X1) | uptakepg(X1), inference(cnf_transformation, [status(esa)], [f10_sk])).
% 21.70/3.28 cnf(p79, plain, gt(n0,X0) | uptakepg(X0) | drugi(sk0(n0)), inference(resolution, [status(thm)], [c11, c51])).
% 21.70/3.28 cnf(ssp4, plain, (spl3 | spl8), inference(avatar_split_clause, [status(thm)], [p79, sdef3, sdef8])).
% 21.70/3.28 cnf(p81, plain, (gt(n0,X0) | uptakepg(X0) | uptakelg(sk0(n0)) | ~spl2), inference(resolution, [status(thm)], [c11, p67])).
% 21.70/3.28 fof(sdef9, definition, (spl9 <=> (uptakelg(sk0(n0)))), introduced(definition, [new_symbols(naming, [spl9])], [avatar_definition])).
% 21.70/3.28 cnf(ssp5, plain, (~spl2 | spl8 | spl9), inference(avatar_split_clause, [status(thm)], [p81, sdef8, sdef9])).
% 21.70/3.28 cnf(p82, plain, (uptakelg(sk0(n0)) | ~spl9), inference(avatar_component_clause, [status(thm)], [sdef9])).
% 21.70/3.28 cnf(p87, plain, (gt(X0,sk0(n0)) | ~releaselg(sk0(n0)) | ~spl9), inference(resolution, [status(thm)], [p82, c14])).
% 21.70/3.28 fof(sdef11, definition, (spl11 <=> (~releaselg(sk0(n0)))), introduced(definition, [new_symbols(naming, [spl11])], [avatar_definition])).
% 21.70/3.28 cnf(ssp6, plain, (~spl9 | spl10 | spl11), inference(avatar_split_clause, [status(thm)], [p87, sdef10, sdef11])).
% 21.70/3.28 cnf(p98, plain, (uptakepg(sk0(n0)) | gt(n0,X0) | uptakelg(X0) | ~spl8), inference(resolution, [status(thm)], [p80, c10])).
% 21.70/3.28 fof(sdef12, definition, (spl12 <=> (uptakepg(sk0(n0)))), introduced(definition, [new_symbols(naming, [spl12])], [avatar_definition])).
% 21.70/3.28 cnf(ssp7, plain, (~spl8 | spl2 | spl12), inference(avatar_split_clause, [status(thm)], [p98, sdef2, sdef12])).
% 21.70/3.28 cnf(c12, plain, ~drugi(sk0(X0)) | gt(X0,X1) | uptakelg(X1), inference(cnf_transformation, [status(esa)], [f10_sk])).
% 21.70/3.28 cnf(p86, plain, (gt(n0,X0) | uptakelg(X0) | ~spl3), inference(resolution, [status(thm)], [c12, p68])).
% 21.70/3.28 cnf(p100, plain, (uptakelg(sk14) | ~spl3), inference(resolution, [status(thm)], [p86, c54])).
% 21.70/3.28 cnf(p104, plain, (gt(X0,sk14) | ~releaselg(sk14) | ~spl3), inference(resolution, [status(thm)], [p100, c14])).
% 21.70/3.28 cnf(ssp8, plain, (~spl3 | spl4 | spl5), inference(avatar_split_clause, [status(thm)], [p104, sdef4, sdef5])).
% 21.70/3.28 cnf(p101, plain, (uptakelg(n0) | ~spl3), inference(resolution, [status(thm)], [p86, c0])).
% 21.70/3.28 cnf(p105, plain, (gt(X0,n0) | ~releaselg(n0) | ~spl3), inference(resolution, [status(thm)], [p101, c14])).
% 21.70/3.28 cnf(ssp9, plain, (~spl3 | spl6 | spl7), inference(avatar_split_clause, [status(thm)], [p105, sdef6, sdef7])).
% 21.70/3.28 fof(f13, axiom, ! [X0] : ( ! [X1] : ( ~ gt(X0,X1) => drugbg(X1) ) => ! [X1] : ( ~ gt(X0,X1) => ~ releaselg(X1) ) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', biguanide_effect)).
% 21.70/3.28 fof(f13_nnf, plain, ! [X0] : ((? [X1] : ((~(gt(X0,X1)) & ~(drugbg(X1)))) | ! [X1] : ((gt(X0,X1) | ~(releaselg(X1)))))), inference(nnf_transformation, [status(thm)], [f13])).
% 21.70/3.28 fof(f13_sk, plain, ! [X0,X1] : (((~(gt(X0,sk2(X0))) & ~(drugbg(sk2(X0)))) | (gt(X0,X1) | ~(releaselg(X1))))), inference(skolemisation, [status(esa), new_symbols(skolem, [sk2])], [f13_nnf])).
% 21.70/3.28 cnf(c17, plain, ~gt(X0,sk2(X0)) | gt(X0,X1) | ~releaselg(X1), inference(cnf_transformation, [status(esa)], [f13_sk])).
% 21.70/3.28 cnf(p111, plain, gt(n0,X0) | ~releaselg(X0) | drugi(sk2(n0)), inference(resolution, [status(thm)], [c17, c51])).
% 21.70/3.28 fof(sdef13, definition, (spl13 <=> (gt(n0,X0) | ~releaselg(X0))), introduced(definition, [new_symbols(naming, [spl13])], [avatar_definition])).
% 21.70/3.28 fof(sdef14, definition, (spl14 <=> (drugi(sk2(n0)))), introduced(definition, [new_symbols(naming, [spl14])], [avatar_definition])).
% 21.70/3.28 cnf(ssp10, plain, (spl13 | spl14), inference(avatar_split_clause, [status(thm)], [p111, sdef13, sdef14])).
% 21.70/3.28 cnf(p114, plain, (gt(n0,X0) | ~releaselg(X0) | uptakelg(sk2(n0)) | ~spl2), inference(resolution, [status(thm)], [c17, p67])).
% 21.70/3.28 fof(sdef15, definition, (spl15 <=> (uptakelg(sk2(n0)))), introduced(definition, [new_symbols(naming, [spl15])], [avatar_definition])).
% 21.70/3.28 cnf(ssp11, plain, (~spl2 | spl13 | spl15), inference(avatar_split_clause, [status(thm)], [p114, sdef13, sdef15])).
% 21.70/3.28 cnf(p116, plain, (gt(n0,X0) | ~releaselg(X0) | uptakepg(sk2(n0)) | ~spl8), inference(resolution, [status(thm)], [c17, p80])).
% 21.70/3.28 fof(sdef16, definition, (spl16 <=> (uptakepg(sk2(n0)))), introduced(definition, [new_symbols(naming, [spl16])], [avatar_definition])).
% 21.70/3.28 cnf(ssp12, plain, (~spl8 | spl13 | spl16), inference(avatar_split_clause, [status(thm)], [p116, sdef13, sdef16])).
% 21.70/3.28 cnf(p118, plain, (gt(n0,X0) | ~releaselg(X0) | uptakelg(sk2(n0)) | ~spl3), inference(resolution, [status(thm)], [c17, p86])).
% 21.70/3.28 cnf(ssp13, plain, (~spl3 | spl13 | spl15), inference(avatar_split_clause, [status(thm)], [p118, sdef13, sdef15])).
% 21.70/3.28 cnf(p119, plain, (gt(n0,X0) | ~releaselg(X0) | uptakepg(sk2(n0)) | ~spl3), inference(resolution, [status(thm)], [c17, p93])).
% 21.70/3.28 cnf(ssp14, plain, (~spl3 | spl13 | spl16), inference(avatar_split_clause, [status(thm)], [p119, sdef13, sdef16])).
% 21.70/3.28 cnf(p115, plain, (uptakelg(sk2(n0)) | ~spl15), inference(avatar_component_clause, [status(thm)], [sdef15])).
% 21.70/3.28 cnf(p120, plain, (gt(X0,sk2(n0)) | ~releaselg(sk2(n0)) | ~spl15), inference(resolution, [status(thm)], [p115, c14])).
% 21.70/3.28 fof(sdef18, definition, (spl18 <=> (~releaselg(sk2(n0)))), introduced(definition, [new_symbols(naming, [spl18])], [avatar_definition])).
% 21.70/3.28 cnf(ssp15, plain, (~spl15 | spl17 | spl18), inference(avatar_split_clause, [status(thm)], [p120, sdef17, sdef18])).
% 21.70/3.28 cnf(p59, plain, conditionhyper(X0) | drugi(X0), inference(resolution, [status(thm)], [c52, c51])).
% 21.70/3.28 cnf(p85, plain, gt(X0,X1) | uptakelg(X1) | conditionhyper(sk0(X0)), inference(resolution, [status(thm)], [c12, p59])).
% 21.70/3.28 cnf(p125, plain, uptakelg(sk14) | conditionhyper(sk0(n0)), inference(resolution, [status(thm)], [p85, c54])).
% 21.70/3.28 fof(sdef19, definition, (spl19 <=> (uptakelg(sk14))), introduced(definition, [new_symbols(naming, [spl19])], [avatar_definition])).
% 21.70/3.28 cnf(ssp16, plain, (spl19 | spl20), inference(avatar_split_clause, [status(thm)], [p125, sdef19, sdef20])).
% 21.70/3.28 cnf(p129, plain, uptakelg(X0) | conditionhyper(sk0(n0)) | conditionhyper(X0), inference(resolution, [status(thm)], [p85, c52])).
% 21.70/3.28 fof(sdef21, definition, (spl21 <=> (uptakelg(X0) | conditionhyper(X0))), introduced(definition, [new_symbols(naming, [spl21])], [avatar_definition])).
% 21.70/3.28 cnf(ssp17, plain, (spl20 | spl21), inference(avatar_split_clause, [status(thm)], [p129, sdef20, sdef21])).
% 21.70/3.28 fof(f1, axiom, ! [X,Y,Z] : ( ( gt(X,Y) & gt(Y,Z) ) => gt(X,Z) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', transitivity_gt)).
% 21.70/3.28 fof(f1_nnf, plain, ! [X,Y,Z] : (((~(gt(X,Y)) | ~(gt(Y,Z))) | gt(X,Z))), inference(nnf_transformation, [status(thm)], [f1])).
% 21.70/3.28 fof(f1_sk, plain, ! [X,Y,Z] : (((~(gt(X,Y)) | ~(gt(Y,Z))) | gt(X,Z))), inference(skolemisation, [status(esa)], [f1_nnf])).
% 21.70/3.28 cnf(c1, plain, ~gt(X0,X1) | ~gt(X1,X2) | gt(X0,X2), inference(cnf_transformation, [status(esa)], [f1_sk])).
% 21.70/3.28 cnf(p60, plain, ~gt(X0,X1) | gt(n0,X1) | drugi(X0), inference(resolution, [status(thm)], [c1, c51])).
% 21.70/3.28 cnf(p132, plain, uptakelg(X0) | conditionhyper(sk0(X1)) | gt(n0,X0) | drugi(X1), inference(resolution, [status(thm)], [p85, p60])).
% 21.70/3.28 fof(sdef22, definition, (spl22 <=> (conditionhyper(sk0(X0)) | drugi(X0))), introduced(definition, [new_symbols(naming, [spl22])], [avatar_definition])).
% 21.70/3.28 cnf(ssp18, plain, (spl2 | spl22), inference(avatar_split_clause, [status(thm)], [p132, sdef2, sdef22])).
% 21.70/3.28 cnf(p126, plain, (uptakelg(sk14) | ~spl19), inference(avatar_component_clause, [status(thm)], [sdef19])).
% 21.70/3.28 cnf(p139, plain, (gt(X0,sk14) | ~releaselg(sk14) | ~spl19), inference(resolution, [status(thm)], [p126, c14])).
% 21.70/3.28 cnf(ssp19, plain, (~spl19 | spl4 | spl5), inference(avatar_split_clause, [status(thm)], [p139, sdef4, sdef5])).
% 21.70/3.28 cnf(p92, plain, gt(X0,X1) | uptakepg(X1) | conditionhyper(sk0(X0)), inference(resolution, [status(thm)], [c13, p59])).
% 21.70/3.28 cnf(p149, plain, uptakepg(sk14) | conditionhyper(sk0(n0)), inference(resolution, [status(thm)], [p92, c54])).
% 21.70/3.28 fof(sdef23, definition, (spl23 <=> (uptakepg(sk14))), introduced(definition, [new_symbols(naming, [spl23])], [avatar_definition])).
% 21.70/3.28 cnf(ssp20, plain, (spl20 | spl23), inference(avatar_split_clause, [status(thm)], [p149, sdef20, sdef23])).
% 21.70/3.28 cnf(p152, plain, uptakepg(X0) | conditionhyper(sk0(n0)) | conditionhyper(X0), inference(resolution, [status(thm)], [p92, c52])).
% 21.70/3.28 fof(sdef24, definition, (spl24 <=> (uptakepg(X0) | conditionhyper(X0))), introduced(definition, [new_symbols(naming, [spl24])], [avatar_definition])).
% 21.70/3.28 cnf(ssp21, plain, (spl20 | spl24), inference(avatar_split_clause, [status(thm)], [p152, sdef20, sdef24])).
% 21.70/3.28 cnf(p155, plain, uptakepg(X0) | conditionhyper(sk0(X1)) | gt(n0,X0) | drugi(X1), inference(resolution, [status(thm)], [p92, p60])).
% 21.70/3.28 cnf(ssp22, plain, (spl8 | spl22), inference(avatar_split_clause, [status(thm)], [p155, sdef8, sdef22])).
% 21.70/3.28 cnf(p131, plain, uptakelg(X0) | conditionhyper(sk0(X1)) | ~gt(X0,X2) | gt(X1,X2), inference(resolution, [status(thm)], [p85, c1])).
% 21.70/3.28 cnf(p172, plain, uptakelg(n0) | conditionhyper(sk0(X0)) | gt(X0,X1) | drugi(X1), inference(resolution, [status(thm)], [p131, c51])).
% 21.70/3.28 fof(sdef25, definition, (spl25 <=> (uptakelg(n0))), introduced(definition, [new_symbols(naming, [spl25])], [avatar_definition])).
% 21.70/3.28 fof(sdef26, definition, (spl26 <=> (conditionhyper(sk0(X0)) | gt(X0,X1) | drugi(X1))), introduced(definition, [new_symbols(naming, [spl26])], [avatar_definition])).
% 21.70/3.28 cnf(ssp23, plain, (spl25 | spl26), inference(avatar_split_clause, [status(thm)], [p172, sdef25, sdef26])).
% 21.70/3.28 cnf(p173, plain, (uptakelg(n0) | ~spl25), inference(avatar_component_clause, [status(thm)], [sdef25])).
% 21.70/3.28 cnf(p175, plain, (gt(X0,n0) | ~releaselg(n0) | ~spl25), inference(resolution, [status(thm)], [p173, c14])).
% 21.70/3.28 cnf(ssp24, plain, (~spl25 | spl6 | spl7), inference(avatar_split_clause, [status(thm)], [p175, sdef6, sdef7])).
% 21.70/3.28 fof(f16, axiom, ! [X0] : ( ( ( ! [X1] : ( ~ gt(X0,X1) => ~ releaselg(X1) ) | ! [X1] : ( ~ gt(X0,X1) => uptakepg(X1) ) ) & bcapacityne(X0) & ! [X1] : ( ~ gt(X0,X1) => bsecretioni(X1) ) & ! [X1] : ( gt(X0,X1) => conditionhyper(X1) ) ) => ! [X1] : ( ~ gt(X0,X1) => conditionnormo(X1) ) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ne_cure)).
% 21.70/3.28 fof(f16_nnf, plain, ! [X0] : ((((((? [X1] : ((~(gt(X0,X1)) & releaselg(X1))) & ? [X1] : ((~(gt(X0,X1)) & ~(uptakepg(X1))))) | ~(bcapacityne(X0))) | ? [X1] : ((~(gt(X0,X1)) & ~(bsecretioni(X1))))) | ? [X1] : ((gt(X0,X1) & ~(conditionhyper(X1))))) | ! [X1] : ((gt(X0,X1) | conditionnormo(X1))))), inference(nnf_transformation, [status(thm)], [f16])).
% 21.70/3.28 fof(f16_sk, plain, ! [X0,X1] : (((((((~(gt(X0,sk7(X0))) & releaselg(sk7(X0))) & (~(gt(X0,sk8(X0))) & ~(uptakepg(sk8(X0))))) | ~(bcapacityne(X0))) | (~(gt(X0,sk9(X0))) & ~(bsecretioni(sk9(X0))))) | (gt(X0,sk10(X0)) & ~(conditionhyper(sk10(X0))))) | (gt(X0,X1) | conditionnormo(X1)))), inference(skolemisation, [status(esa), new_symbols(skolem, [sk7,sk8,sk9,sk10])], [f16_nnf])).
% 21.70/3.28 cnf(c27, plain, ~gt(X0,sk7(X0)) | ~bcapacityne(X0) | ~gt(X0,sk9(X0)) | gt(X0,sk10(X0)) | gt(X0,X1) | conditionnormo(X1), inference(cnf_transformation, [status(esa)], [f16_sk])).
% 21.70/3.28 cnf(p189, plain, ~bcapacityne(n0) | ~gt(n0,sk9(n0)) | gt(n0,sk10(n0)) | gt(n0,X0) | conditionnormo(X0) | drugi(sk7(n0)), inference(resolution, [status(thm)], [c27, c51])).
% 21.70/3.28 fof(sdef27, definition, (spl27 <=> (~bcapacityne(n0))), introduced(definition, [new_symbols(naming, [spl27])], [avatar_definition])).
% 21.70/3.28 fof(sdef28, definition, (spl28 <=> (~gt(n0,sk9(n0)))), introduced(definition, [new_symbols(naming, [spl28])], [avatar_definition])).
% 21.70/3.28 fof(sdef31, definition, (spl31 <=> (drugi(sk7(n0)))), introduced(definition, [new_symbols(naming, [spl31])], [avatar_definition])).
% 21.70/3.28 cnf(ssp25, plain, (spl27 | spl28 | spl29 | spl30 | spl31), inference(avatar_split_clause, [status(thm)], [p189, sdef27, sdef28, sdef29, sdef30, sdef31])).
% 21.70/3.28 cnf(p195, plain, (~bcapacityne(n0) | ~gt(n0,sk9(n0)) | gt(n0,sk10(n0)) | gt(n0,X0) | conditionnormo(X0) | uptakelg(sk7(n0)) | ~spl2), inference(resolution, [status(thm)], [c27, p67])).
% 21.70/3.28 fof(sdef32, definition, (spl32 <=> (uptakelg(sk7(n0)))), introduced(definition, [new_symbols(naming, [spl32])], [avatar_definition])).
% 21.70/3.28 cnf(ssp26, plain, (~spl2 | spl27 | spl28 | spl29 | spl30 | spl32), inference(avatar_split_clause, [status(thm)], [p195, sdef27, sdef28, sdef29, sdef30, sdef32])).
% 21.70/3.28 cnf(p197, plain, (~bcapacityne(n0) | ~gt(n0,sk9(n0)) | gt(n0,sk10(n0)) | gt(n0,X0) | conditionnormo(X0) | uptakepg(sk7(n0)) | ~spl8), inference(resolution, [status(thm)], [c27, p80])).
% 21.70/3.28 fof(sdef33, definition, (spl33 <=> (uptakepg(sk7(n0)))), introduced(definition, [new_symbols(naming, [spl33])], [avatar_definition])).
% 21.70/3.28 cnf(ssp27, plain, (~spl8 | spl27 | spl28 | spl29 | spl30 | spl33), inference(avatar_split_clause, [status(thm)], [p197, sdef27, sdef28, sdef29, sdef30, sdef33])).
% 21.70/3.28 cnf(p199, plain, (~bcapacityne(n0) | ~gt(n0,sk9(n0)) | gt(n0,sk10(n0)) | gt(n0,X0) | conditionnormo(X0) | uptakelg(sk7(n0)) | ~spl3), inference(resolution, [status(thm)], [c27, p86])).
% 21.70/3.28 cnf(ssp28, plain, (~spl3 | spl27 | spl28 | spl29 | spl30 | spl32), inference(avatar_split_clause, [status(thm)], [p199, sdef27, sdef28, sdef29, sdef30, sdef32])).
% 21.70/3.28 cnf(p200, plain, (~bcapacityne(n0) | ~gt(n0,sk9(n0)) | gt(n0,sk10(n0)) | gt(n0,X0) | conditionnormo(X0) | uptakepg(sk7(n0)) | ~spl3), inference(resolution, [status(thm)], [c27, p93])).
% 21.70/3.28 cnf(ssp29, plain, (~spl3 | spl27 | spl28 | spl29 | spl30 | spl33), inference(avatar_split_clause, [status(thm)], [p200, sdef27, sdef28, sdef29, sdef30, sdef33])).
% 21.70/3.28 cnf(p196, plain, (uptakelg(sk7(n0)) | ~spl32), inference(avatar_component_clause, [status(thm)], [sdef32])).
% 21.70/3.28 cnf(p204, plain, (gt(X0,sk7(n0)) | ~releaselg(sk7(n0)) | ~spl32), inference(resolution, [status(thm)], [p196, c14])).
% 21.70/3.28 fof(sdef35, definition, (spl35 <=> (~releaselg(sk7(n0)))), introduced(definition, [new_symbols(naming, [spl35])], [avatar_definition])).
% 21.70/3.28 cnf(ssp30, plain, (~spl32 | spl34 | spl35), inference(avatar_split_clause, [status(thm)], [p204, sdef34, sdef35])).
% 21.70/3.28 cnf(c28, plain, ~gt(X0,sk7(X0)) | ~bcapacityne(X0) | ~gt(X0,sk9(X0)) | ~conditionhyper(sk10(X0)) | gt(X0,X1) | conditionnormo(X1), inference(cnf_transformation, [status(esa)], [f16_sk])).
% 21.70/3.28 cnf(p207, plain, ~bcapacityne(n0) | ~gt(n0,sk9(n0)) | ~conditionhyper(sk10(n0)) | gt(n0,X0) | conditionnormo(X0) | drugi(sk7(n0)), inference(resolution, [status(thm)], [c28, c51])).
% 21.70/3.28 cnf(ssp31, plain, (spl27 | spl28 | spl30 | spl31 | spl36), inference(avatar_split_clause, [status(thm)], [p207, sdef27, sdef28, sdef30, sdef31, sdef36])).
% 21.70/3.28 cnf(p209, plain, (~bcapacityne(n0) | ~gt(n0,sk9(n0)) | ~conditionhyper(sk10(n0)) | gt(n0,X0) | conditionnormo(X0) | uptakelg(sk7(n0)) | ~spl2), inference(resolution, [status(thm)], [c28, p67])).
% 21.70/3.28 cnf(ssp32, plain, (~spl2 | spl27 | spl28 | spl30 | spl32 | spl36), inference(avatar_split_clause, [status(thm)], [p209, sdef27, sdef28, sdef30, sdef32, sdef36])).
% 21.70/3.28 cnf(p210, plain, (~bcapacityne(n0) | ~gt(n0,sk9(n0)) | ~conditionhyper(sk10(n0)) | gt(n0,X0) | conditionnormo(X0) | uptakepg(sk7(n0)) | ~spl8), inference(resolution, [status(thm)], [c28, p80])).
% 21.70/3.28 cnf(ssp33, plain, (~spl8 | spl27 | spl28 | spl30 | spl33 | spl36), inference(avatar_split_clause, [status(thm)], [p210, sdef27, sdef28, sdef30, sdef33, sdef36])).
% 21.70/3.28 cnf(p211, plain, (~bcapacityne(n0) | ~gt(n0,sk9(n0)) | ~conditionhyper(sk10(n0)) | gt(n0,X0) | conditionnormo(X0) | uptakelg(sk7(n0)) | ~spl3), inference(resolution, [status(thm)], [c28, p86])).
% 21.70/3.28 cnf(ssp34, plain, (~spl3 | spl27 | spl28 | spl30 | spl32 | spl36), inference(avatar_split_clause, [status(thm)], [p211, sdef27, sdef28, sdef30, sdef32, sdef36])).
% 21.70/3.28 cnf(p212, plain, (~bcapacityne(n0) | ~gt(n0,sk9(n0)) | ~conditionhyper(sk10(n0)) | gt(n0,X0) | conditionnormo(X0) | uptakepg(sk7(n0)) | ~spl3), inference(resolution, [status(thm)], [c28, p93])).
% 21.70/3.28 cnf(ssp35, plain, (~spl3 | spl27 | spl28 | spl30 | spl33 | spl36), inference(avatar_split_clause, [status(thm)], [p212, sdef27, sdef28, sdef30, sdef33, sdef36])).
% 21.70/3.28 cnf(p191, plain, (~gt(n0,sk9(n0)) | ~spl28), inference(avatar_component_clause, [status(thm)], [sdef28])).
% 21.70/3.28 cnf(p221, plain, (uptakelg(sk9(n0)) | conditionhyper(sk0(n0)) | ~spl28), inference(resolution, [status(thm)], [p191, p85])).
% 21.70/3.28 fof(sdef37, definition, (spl37 <=> (uptakelg(sk9(n0)))), introduced(definition, [new_symbols(naming, [spl37])], [avatar_definition])).
% 21.70/3.28 cnf(ssp36, plain, (~spl28 | spl20 | spl37), inference(avatar_split_clause, [status(thm)], [p221, sdef20, sdef37])).
% 21.70/3.28 cnf(p223, plain, (uptakepg(sk9(n0)) | conditionhyper(sk0(n0)) | ~spl28), inference(resolution, [status(thm)], [p191, p92])).
% 21.70/3.28 fof(sdef38, definition, (spl38 <=> (uptakepg(sk9(n0)))), introduced(definition, [new_symbols(naming, [spl38])], [avatar_definition])).
% 21.70/3.28 cnf(ssp37, plain, (~spl28 | spl20 | spl38), inference(avatar_split_clause, [status(thm)], [p223, sdef20, sdef38])).
% 21.70/3.28 cnf(c29, plain, ~gt(X0,sk7(X0)) | ~bcapacityne(X0) | ~bsecretioni(sk9(X0)) | gt(X0,sk10(X0)) | gt(X0,X1) | conditionnormo(X1), inference(cnf_transformation, [status(esa)], [f16_sk])).
% 21.70/3.28 cnf(p226, plain, ~bcapacityne(n0) | ~bsecretioni(sk9(n0)) | gt(n0,sk10(n0)) | gt(n0,X0) | conditionnormo(X0) | drugi(sk7(n0)), inference(resolution, [status(thm)], [c29, c51])).
% 21.70/3.28 fof(sdef39, definition, (spl39 <=> (~bsecretioni(sk9(n0)))), introduced(definition, [new_symbols(naming, [spl39])], [avatar_definition])).
% 21.70/3.28 cnf(ssp38, plain, (spl27 | spl29 | spl30 | spl31 | spl39), inference(avatar_split_clause, [status(thm)], [p226, sdef27, sdef29, sdef30, sdef31, sdef39])).
% 21.70/3.28 cnf(p228, plain, (~bcapacityne(n0) | ~bsecretioni(sk9(n0)) | gt(n0,sk10(n0)) | gt(n0,X0) | conditionnormo(X0) | uptakelg(sk7(n0)) | ~spl2), inference(resolution, [status(thm)], [c29, p67])).
% 21.70/3.28 cnf(ssp39, plain, (~spl2 | spl27 | spl29 | spl30 | spl32 | spl39), inference(avatar_split_clause, [status(thm)], [p228, sdef27, sdef29, sdef30, sdef32, sdef39])).
% 21.70/3.28 cnf(p229, plain, (~bcapacityne(n0) | ~bsecretioni(sk9(n0)) | gt(n0,sk10(n0)) | gt(n0,X0) | conditionnormo(X0) | uptakepg(sk7(n0)) | ~spl8), inference(resolution, [status(thm)], [c29, p80])).
% 21.70/3.28 cnf(ssp40, plain, (~spl8 | spl27 | spl29 | spl30 | spl33 | spl39), inference(avatar_split_clause, [status(thm)], [p229, sdef27, sdef29, sdef30, sdef33, sdef39])).
% 21.70/3.28 cnf(p230, plain, (~bcapacityne(n0) | ~bsecretioni(sk9(n0)) | gt(n0,sk10(n0)) | gt(n0,X0) | conditionnormo(X0) | uptakelg(sk7(n0)) | ~spl3), inference(resolution, [status(thm)], [c29, p86])).
% 21.70/3.28 cnf(ssp41, plain, (~spl3 | spl27 | spl29 | spl30 | spl32 | spl39), inference(avatar_split_clause, [status(thm)], [p230, sdef27, sdef29, sdef30, sdef32, sdef39])).
% 21.70/3.28 cnf(p231, plain, (~bcapacityne(n0) | ~bsecretioni(sk9(n0)) | gt(n0,sk10(n0)) | gt(n0,X0) | conditionnormo(X0) | uptakepg(sk7(n0)) | ~spl3), inference(resolution, [status(thm)], [c29, p93])).
% 21.70/3.28 cnf(ssp42, plain, (~spl3 | spl27 | spl29 | spl30 | spl33 | spl39), inference(avatar_split_clause, [status(thm)], [p231, sdef27, sdef29, sdef30, sdef33, sdef39])).
% 21.70/3.28 cnf(p217, plain, (uptakelg(sk9(n0)) | ~spl2 | ~spl28), inference(resolution, [status(thm)], [p191, p67])).
% 21.70/3.28 cnf(p235, plain, (gt(X0,sk9(n0)) | ~releaselg(sk9(n0)) | ~spl2 | ~spl28), inference(resolution, [status(thm)], [p217, c14])).
% 21.70/3.28 fof(sdef41, definition, (spl41 <=> (~releaselg(sk9(n0)))), introduced(definition, [new_symbols(naming, [spl41])], [avatar_definition])).
% 21.70/3.28 cnf(ssp43, plain, (~spl2 | ~spl28 | spl40 | spl41), inference(avatar_split_clause, [status(thm)], [p235, sdef40, sdef41])).
% 21.70/3.28 cnf(p219, plain, (uptakelg(sk9(n0)) | ~spl3 | ~spl28), inference(resolution, [status(thm)], [p191, p86])).
% 21.70/3.28 cnf(p238, plain, (gt(X0,sk9(n0)) | ~releaselg(sk9(n0)) | ~spl3 | ~spl28), inference(resolution, [status(thm)], [p219, c14])).
% 21.70/3.28 cnf(ssp44, plain, (~spl3 | ~spl28 | spl40 | spl41), inference(avatar_split_clause, [status(thm)], [p238, sdef40, sdef41])).
% 21.70/3.28 cnf(c30, plain, ~gt(X0,sk7(X0)) | ~bcapacityne(X0) | ~bsecretioni(sk9(X0)) | ~conditionhyper(sk10(X0)) | gt(X0,X1) | conditionnormo(X1), inference(cnf_transformation, [status(esa)], [f16_sk])).
% 21.70/3.28 cnf(p239, plain, ~bcapacityne(n0) | ~bsecretioni(sk9(n0)) | ~conditionhyper(sk10(n0)) | gt(n0,X0) | conditionnormo(X0) | drugi(sk7(n0)), inference(resolution, [status(thm)], [c30, c51])).
% 21.70/3.28 cnf(ssp45, plain, (spl27 | spl30 | spl31 | spl36 | spl39), inference(avatar_split_clause, [status(thm)], [p239, sdef27, sdef30, sdef31, sdef36, sdef39])).
% 21.70/3.28 cnf(p240, plain, (~bcapacityne(n0) | ~bsecretioni(sk9(n0)) | ~conditionhyper(sk10(n0)) | gt(n0,X0) | conditionnormo(X0) | uptakelg(sk7(n0)) | ~spl2), inference(resolution, [status(thm)], [c30, p67])).
% 21.70/3.28 cnf(ssp46, plain, (~spl2 | spl27 | spl30 | spl32 | spl36 | spl39), inference(avatar_split_clause, [status(thm)], [p240, sdef27, sdef30, sdef32, sdef36, sdef39])).
% 21.70/3.28 cnf(p241, plain, (~bcapacityne(n0) | ~bsecretioni(sk9(n0)) | ~conditionhyper(sk10(n0)) | gt(n0,X0) | conditionnormo(X0) | uptakepg(sk7(n0)) | ~spl8), inference(resolution, [status(thm)], [c30, p80])).
% 21.70/3.28 cnf(ssp47, plain, (~spl8 | spl27 | spl30 | spl33 | spl36 | spl39), inference(avatar_split_clause, [status(thm)], [p241, sdef27, sdef30, sdef33, sdef36, sdef39])).
% 21.70/3.28 cnf(p242, plain, (~bcapacityne(n0) | ~bsecretioni(sk9(n0)) | ~conditionhyper(sk10(n0)) | gt(n0,X0) | conditionnormo(X0) | uptakelg(sk7(n0)) | ~spl3), inference(resolution, [status(thm)], [c30, p86])).
% 21.70/3.28 cnf(ssp48, plain, (~spl3 | spl27 | spl30 | spl32 | spl36 | spl39), inference(avatar_split_clause, [status(thm)], [p242, sdef27, sdef30, sdef32, sdef36, sdef39])).
% 21.70/3.28 cnf(p243, plain, (~bcapacityne(n0) | ~bsecretioni(sk9(n0)) | ~conditionhyper(sk10(n0)) | gt(n0,X0) | conditionnormo(X0) | uptakepg(sk7(n0)) | ~spl3), inference(resolution, [status(thm)], [c30, p93])).
% 21.70/3.28 cnf(ssp49, plain, (~spl3 | spl27 | spl30 | spl33 | spl36 | spl39), inference(avatar_split_clause, [status(thm)], [p243, sdef27, sdef30, sdef33, sdef36, sdef39])).
% 21.70/3.28 cnf(p222, plain, (uptakelg(sk9(n0)) | ~spl37), inference(avatar_component_clause, [status(thm)], [sdef37])).
% 21.70/3.28 cnf(p247, plain, (gt(X0,sk9(n0)) | ~releaselg(sk9(n0)) | ~spl37), inference(resolution, [status(thm)], [p222, c14])).
% 21.70/3.28 cnf(ssp50, plain, (~spl37 | spl40 | spl41), inference(avatar_split_clause, [status(thm)], [p247, sdef40, sdef41])).
% 21.70/3.28 cnf(p251, plain, (uptakelg(n0) | conditionhyper(sk0(X0)) | gt(X0,sk10(n0)) | ~spl29), inference(resolution, [status(thm)], [p192, p131])).
% 21.70/3.28 fof(sdef42, definition, (spl42 <=> (conditionhyper(sk0(X0)) | gt(X0,sk10(n0)))), introduced(definition, [new_symbols(naming, [spl42])], [avatar_definition])).
% 21.70/3.28 cnf(ssp51, plain, (~spl29 | spl25 | spl42), inference(avatar_split_clause, [status(thm)], [p251, sdef25, sdef42])).
% 21.70/3.28 cnf(p262, plain, (conditionnormo(sk0(n0)) | gt(n0,X0) | uptakelg(X0) | ~spl30), inference(resolution, [status(thm)], [p193, c10])).
% 21.70/3.28 cnf(ssp52, plain, (~spl30 | spl2 | spl43), inference(avatar_split_clause, [status(thm)], [p262, sdef2, sdef43])).
% 21.70/3.28 cnf(p264, plain, (conditionnormo(sk0(n0)) | gt(n0,X0) | uptakepg(X0) | ~spl30), inference(resolution, [status(thm)], [p193, c11])).
% 21.70/3.28 cnf(ssp53, plain, (~spl30 | spl8 | spl43), inference(avatar_split_clause, [status(thm)], [p264, sdef8, sdef43])).
% 21.70/3.28 cnf(p265, plain, (conditionnormo(sk2(n0)) | gt(n0,X0) | ~releaselg(X0) | ~spl30), inference(resolution, [status(thm)], [p193, c17])).
% 21.70/3.28 fof(sdef44, definition, (spl44 <=> (conditionnormo(sk2(n0)))), introduced(definition, [new_symbols(naming, [spl44])], [avatar_definition])).
% 21.70/3.28 cnf(ssp54, plain, (~spl30 | spl13 | spl44), inference(avatar_split_clause, [status(thm)], [p265, sdef13, sdef44])).
% 21.70/3.28 cnf(p267, plain, (conditionnormo(X0) | uptakelg(n0) | conditionhyper(sk0(X1)) | gt(X1,X0) | ~spl30), inference(resolution, [status(thm)], [p193, p131])).
% 21.70/3.28 fof(sdef45, definition, (spl45 <=> (conditionnormo(X0) | conditionhyper(sk0(X1)) | gt(X1,X0))), introduced(definition, [new_symbols(naming, [spl45])], [avatar_definition])).
% 21.70/3.28 cnf(ssp55, plain, (~spl30 | spl25 | spl45), inference(avatar_split_clause, [status(thm)], [p267, sdef25, sdef45])).
% 21.70/3.28 cnf(p252, plain, (conditionhyper(sk0(X0)) | gt(X0,sk10(n0)) | ~spl42), inference(avatar_component_clause, [status(thm)], [sdef42])).
% 21.70/3.28 cnf(p273, plain, (conditionhyper(sk0(n0)) | conditionhyper(sk10(n0)) | ~spl42), inference(resolution, [status(thm)], [p252, c52])).
% 21.70/3.28 cnf(ssp56, plain, (~spl42 | spl20 | spl46), inference(avatar_split_clause, [status(thm)], [p273, sdef20, sdef46])).
% 21.70/3.28 cnf(p276, plain, (conditionhyper(sk0(X0)) | gt(n0,sk10(n0)) | drugi(X0) | ~spl42), inference(resolution, [status(thm)], [p252, p60])).
% 21.70/3.28 cnf(ssp57, plain, (~spl42 | spl22 | spl29), inference(avatar_split_clause, [status(thm)], [p276, sdef22, sdef29])).
% 21.70/3.28 cnf(c35, plain, ~gt(X0,sk8(X0)) | ~bcapacityne(X0) | ~gt(X0,sk9(X0)) | gt(X0,sk10(X0)) | gt(X0,X1) | conditionnormo(X1), inference(cnf_transformation, [status(esa)], [f16_sk])).
% 21.70/3.28 cnf(p283, plain, ~bcapacityne(n0) | ~gt(n0,sk9(n0)) | gt(n0,sk10(n0)) | gt(n0,X0) | conditionnormo(X0) | drugi(sk8(n0)), inference(resolution, [status(thm)], [c35, c51])).
% 21.70/3.28 fof(sdef47, definition, (spl47 <=> (drugi(sk8(n0)))), introduced(definition, [new_symbols(naming, [spl47])], [avatar_definition])).
% 21.70/3.28 cnf(ssp58, plain, (spl27 | spl28 | spl29 | spl30 | spl47), inference(avatar_split_clause, [status(thm)], [p283, sdef27, sdef28, sdef29, sdef30, sdef47])).
% 21.70/3.28 cnf(p285, plain, (~bcapacityne(n0) | ~gt(n0,sk9(n0)) | gt(n0,sk10(n0)) | gt(n0,X0) | conditionnormo(X0) | uptakelg(sk8(n0)) | ~spl2), inference(resolution, [status(thm)], [c35, p67])).
% 21.70/3.28 fof(sdef48, definition, (spl48 <=> (uptakelg(sk8(n0)))), introduced(definition, [new_symbols(naming, [spl48])], [avatar_definition])).
% 21.70/3.28 cnf(ssp59, plain, (~spl2 | spl27 | spl28 | spl29 | spl30 | spl48), inference(avatar_split_clause, [status(thm)], [p285, sdef27, sdef28, sdef29, sdef30, sdef48])).
% 21.70/3.28 cnf(p287, plain, (~bcapacityne(n0) | ~gt(n0,sk9(n0)) | gt(n0,sk10(n0)) | gt(n0,X0) | conditionnormo(X0) | uptakepg(sk8(n0)) | ~spl8), inference(resolution, [status(thm)], [c35, p80])).
% 21.70/3.28 fof(sdef49, definition, (spl49 <=> (uptakepg(sk8(n0)))), introduced(definition, [new_symbols(naming, [spl49])], [avatar_definition])).
% 21.70/3.28 cnf(ssp60, plain, (~spl8 | spl27 | spl28 | spl29 | spl30 | spl49), inference(avatar_split_clause, [status(thm)], [p287, sdef27, sdef28, sdef29, sdef30, sdef49])).
% 21.70/3.28 cnf(p289, plain, (~bcapacityne(n0) | ~gt(n0,sk9(n0)) | gt(n0,sk10(n0)) | gt(n0,X0) | conditionnormo(X0) | uptakelg(sk8(n0)) | ~spl3), inference(resolution, [status(thm)], [c35, p86])).
% 21.70/3.28 cnf(ssp61, plain, (~spl3 | spl27 | spl28 | spl29 | spl30 | spl48), inference(avatar_split_clause, [status(thm)], [p289, sdef27, sdef28, sdef29, sdef30, sdef48])).
% 21.70/3.28 cnf(p290, plain, (~bcapacityne(n0) | ~gt(n0,sk9(n0)) | gt(n0,sk10(n0)) | gt(n0,X0) | conditionnormo(X0) | uptakepg(sk8(n0)) | ~spl3), inference(resolution, [status(thm)], [c35, p93])).
% 21.70/3.28 cnf(ssp62, plain, (~spl3 | spl27 | spl28 | spl29 | spl30 | spl49), inference(avatar_split_clause, [status(thm)], [p290, sdef27, sdef28, sdef29, sdef30, sdef49])).
% 21.70/3.28 cnf(p286, plain, (uptakelg(sk8(n0)) | ~spl48), inference(avatar_component_clause, [status(thm)], [sdef48])).
% 21.70/3.28 cnf(p294, plain, (gt(X0,sk8(n0)) | ~releaselg(sk8(n0)) | ~spl48), inference(resolution, [status(thm)], [p286, c14])).
% 21.70/3.28 fof(sdef51, definition, (spl51 <=> (~releaselg(sk8(n0)))), introduced(definition, [new_symbols(naming, [spl51])], [avatar_definition])).
% 21.70/3.28 cnf(ssp63, plain, (~spl48 | spl50 | spl51), inference(avatar_split_clause, [status(thm)], [p294, sdef50, sdef51])).
% 21.70/3.28 cnf(c36, plain, ~gt(X0,sk8(X0)) | ~bcapacityne(X0) | ~gt(X0,sk9(X0)) | ~conditionhyper(sk10(X0)) | gt(X0,X1) | conditionnormo(X1), inference(cnf_transformation, [status(esa)], [f16_sk])).
% 21.70/3.28 cnf(p297, plain, ~bcapacityne(n0) | ~gt(n0,sk9(n0)) | ~conditionhyper(sk10(n0)) | gt(n0,X0) | conditionnormo(X0) | drugi(sk8(n0)), inference(resolution, [status(thm)], [c36, c51])).
% 21.70/3.28 cnf(ssp64, plain, (spl27 | spl28 | spl30 | spl36 | spl47), inference(avatar_split_clause, [status(thm)], [p297, sdef27, sdef28, sdef30, sdef36, sdef47])).
% 21.70/3.28 cnf(p298, plain, (~bcapacityne(n0) | ~gt(n0,sk9(n0)) | ~conditionhyper(sk10(n0)) | gt(n0,X0) | conditionnormo(X0) | uptakelg(sk8(n0)) | ~spl2), inference(resolution, [status(thm)], [c36, p67])).
% 21.70/3.28 cnf(ssp65, plain, (~spl2 | spl27 | spl28 | spl30 | spl36 | spl48), inference(avatar_split_clause, [status(thm)], [p298, sdef27, sdef28, sdef30, sdef36, sdef48])).
% 21.70/3.28 cnf(p299, plain, (~bcapacityne(n0) | ~gt(n0,sk9(n0)) | ~conditionhyper(sk10(n0)) | gt(n0,X0) | conditionnormo(X0) | uptakepg(sk8(n0)) | ~spl8), inference(resolution, [status(thm)], [c36, p80])).
% 21.70/3.28 cnf(ssp66, plain, (~spl8 | spl27 | spl28 | spl30 | spl36 | spl49), inference(avatar_split_clause, [status(thm)], [p299, sdef27, sdef28, sdef30, sdef36, sdef49])).
% 21.70/3.28 cnf(p300, plain, (~bcapacityne(n0) | ~gt(n0,sk9(n0)) | ~conditionhyper(sk10(n0)) | gt(n0,X0) | conditionnormo(X0) | uptakelg(sk8(n0)) | ~spl3), inference(resolution, [status(thm)], [c36, p86])).
% 21.70/3.28 cnf(ssp67, plain, (~spl3 | spl27 | spl28 | spl30 | spl36 | spl48), inference(avatar_split_clause, [status(thm)], [p300, sdef27, sdef28, sdef30, sdef36, sdef48])).
% 21.70/3.28 cnf(p301, plain, (~bcapacityne(n0) | ~gt(n0,sk9(n0)) | ~conditionhyper(sk10(n0)) | gt(n0,X0) | conditionnormo(X0) | uptakepg(sk8(n0)) | ~spl3), inference(resolution, [status(thm)], [c36, p93])).
% 21.70/3.28 cnf(ssp68, plain, (~spl3 | spl27 | spl28 | spl30 | spl36 | spl49), inference(avatar_split_clause, [status(thm)], [p301, sdef27, sdef28, sdef30, sdef36, sdef49])).
% 21.70/3.28 cnf(c37, plain, ~gt(X0,sk8(X0)) | ~bcapacityne(X0) | ~bsecretioni(sk9(X0)) | gt(X0,sk10(X0)) | gt(X0,X1) | conditionnormo(X1), inference(cnf_transformation, [status(esa)], [f16_sk])).
% 21.70/3.28 cnf(p307, plain, ~bcapacityne(n0) | ~bsecretioni(sk9(n0)) | gt(n0,sk10(n0)) | gt(n0,X0) | conditionnormo(X0) | drugi(sk8(n0)), inference(resolution, [status(thm)], [c37, c51])).
% 21.70/3.28 cnf(ssp69, plain, (spl27 | spl29 | spl30 | spl39 | spl47), inference(avatar_split_clause, [status(thm)], [p307, sdef27, sdef29, sdef30, sdef39, sdef47])).
% 21.70/3.28 cnf(p308, plain, (~bcapacityne(n0) | ~bsecretioni(sk9(n0)) | gt(n0,sk10(n0)) | gt(n0,X0) | conditionnormo(X0) | uptakelg(sk8(n0)) | ~spl2), inference(resolution, [status(thm)], [c37, p67])).
% 21.70/3.28 cnf(ssp70, plain, (~spl2 | spl27 | spl29 | spl30 | spl39 | spl48), inference(avatar_split_clause, [status(thm)], [p308, sdef27, sdef29, sdef30, sdef39, sdef48])).
% 21.70/3.28 cnf(p309, plain, (~bcapacityne(n0) | ~bsecretioni(sk9(n0)) | gt(n0,sk10(n0)) | gt(n0,X0) | conditionnormo(X0) | uptakepg(sk8(n0)) | ~spl8), inference(resolution, [status(thm)], [c37, p80])).
% 21.70/3.28 cnf(ssp71, plain, (~spl8 | spl27 | spl29 | spl30 | spl39 | spl49), inference(avatar_split_clause, [status(thm)], [p309, sdef27, sdef29, sdef30, sdef39, sdef49])).
% 21.70/3.28 cnf(p310, plain, (~bcapacityne(n0) | ~bsecretioni(sk9(n0)) | gt(n0,sk10(n0)) | gt(n0,X0) | conditionnormo(X0) | uptakelg(sk8(n0)) | ~spl3), inference(resolution, [status(thm)], [c37, p86])).
% 21.70/3.28 cnf(ssp72, plain, (~spl3 | spl27 | spl29 | spl30 | spl39 | spl48), inference(avatar_split_clause, [status(thm)], [p310, sdef27, sdef29, sdef30, sdef39, sdef48])).
% 21.70/3.28 cnf(p311, plain, (~bcapacityne(n0) | ~bsecretioni(sk9(n0)) | gt(n0,sk10(n0)) | gt(n0,X0) | conditionnormo(X0) | uptakepg(sk8(n0)) | ~spl3), inference(resolution, [status(thm)], [c37, p93])).
% 21.70/3.28 cnf(ssp73, plain, (~spl3 | spl27 | spl29 | spl30 | spl39 | spl49), inference(avatar_split_clause, [status(thm)], [p311, sdef27, sdef29, sdef30, sdef39, sdef49])).
% 21.70/3.28 cnf(p268, plain, (conditionnormo(X0) | conditionhyper(sk0(X1)) | gt(X1,X0) | ~spl45), inference(avatar_component_clause, [status(thm)], [sdef45])).
% 21.70/3.28 cnf(p315, plain, (conditionnormo(sk14) | conditionhyper(sk0(n0)) | ~spl45), inference(resolution, [status(thm)], [p268, c54])).
% 21.70/3.28 cnf(ssp74, plain, (~spl45 | spl20 | spl52), inference(avatar_split_clause, [status(thm)], [p315, sdef20, sdef52])).
% 21.70/3.28 cnf(p318, plain, (conditionnormo(X0) | conditionhyper(sk0(n0)) | conditionhyper(X0) | ~spl45), inference(resolution, [status(thm)], [p268, c52])).
% 21.70/3.28 fof(sdef53, definition, (spl53 <=> (conditionnormo(X0) | conditionhyper(X0))), introduced(definition, [new_symbols(naming, [spl53])], [avatar_definition])).
% 21.70/3.28 cnf(ssp75, plain, (~spl45 | spl20 | spl53), inference(avatar_split_clause, [status(thm)], [p318, sdef20, sdef53])).
% 21.70/3.28 cnf(p321, plain, (conditionnormo(X0) | conditionhyper(sk0(X1)) | gt(n0,X0) | drugi(X1) | ~spl45), inference(resolution, [status(thm)], [p268, p60])).
% 21.70/3.28 cnf(ssp76, plain, (~spl45 | spl22 | spl30), inference(avatar_split_clause, [status(thm)], [p321, sdef22, sdef30])).
% 21.70/3.28 cnf(c38, plain, ~gt(X0,sk8(X0)) | ~bcapacityne(X0) | ~bsecretioni(sk9(X0)) | ~conditionhyper(sk10(X0)) | gt(X0,X1) | conditionnormo(X1), inference(cnf_transformation, [status(esa)], [f16_sk])).
% 21.70/3.28 cnf(p328, plain, ~bcapacityne(n0) | ~bsecretioni(sk9(n0)) | ~conditionhyper(sk10(n0)) | gt(n0,X0) | conditionnormo(X0) | drugi(sk8(n0)), inference(resolution, [status(thm)], [c38, c51])).
% 21.70/3.28 cnf(ssp77, plain, (spl27 | spl30 | spl36 | spl39 | spl47), inference(avatar_split_clause, [status(thm)], [p328, sdef27, sdef30, sdef36, sdef39, sdef47])).
% 21.70/3.28 cnf(p329, plain, (~bcapacityne(n0) | ~bsecretioni(sk9(n0)) | ~conditionhyper(sk10(n0)) | gt(n0,X0) | conditionnormo(X0) | uptakelg(sk8(n0)) | ~spl2), inference(resolution, [status(thm)], [c38, p67])).
% 21.70/3.28 cnf(ssp78, plain, (~spl2 | spl27 | spl30 | spl36 | spl39 | spl48), inference(avatar_split_clause, [status(thm)], [p329, sdef27, sdef30, sdef36, sdef39, sdef48])).
% 21.70/3.28 cnf(p330, plain, (~bcapacityne(n0) | ~bsecretioni(sk9(n0)) | ~conditionhyper(sk10(n0)) | gt(n0,X0) | conditionnormo(X0) | uptakepg(sk8(n0)) | ~spl8), inference(resolution, [status(thm)], [c38, p80])).
% 21.70/3.28 cnf(ssp79, plain, (~spl8 | spl27 | spl30 | spl36 | spl39 | spl49), inference(avatar_split_clause, [status(thm)], [p330, sdef27, sdef30, sdef36, sdef39, sdef49])).
% 21.70/3.28 cnf(p331, plain, (~bcapacityne(n0) | ~bsecretioni(sk9(n0)) | ~conditionhyper(sk10(n0)) | gt(n0,X0) | conditionnormo(X0) | uptakelg(sk8(n0)) | ~spl3), inference(resolution, [status(thm)], [c38, p86])).
% 21.70/3.28 cnf(ssp80, plain, (~spl3 | spl27 | spl30 | spl36 | spl39 | spl48), inference(avatar_split_clause, [status(thm)], [p331, sdef27, sdef30, sdef36, sdef39, sdef48])).
% 21.70/3.28 cnf(p332, plain, (~bcapacityne(n0) | ~bsecretioni(sk9(n0)) | ~conditionhyper(sk10(n0)) | gt(n0,X0) | conditionnormo(X0) | uptakepg(sk8(n0)) | ~spl3), inference(resolution, [status(thm)], [c38, p93])).
% 21.70/3.28 cnf(ssp81, plain, (~spl3 | spl27 | spl30 | spl36 | spl39 | spl49), inference(avatar_split_clause, [status(thm)], [p332, sdef27, sdef30, sdef36, sdef39, sdef49])).
% 21.70/3.28 cnf(c39, plain, ~uptakepg(sk8(X0)) | ~bcapacityne(X0) | ~gt(X0,sk9(X0)) | gt(X0,sk10(X0)) | gt(X0,X1) | conditionnormo(X1), inference(cnf_transformation, [status(esa)], [f16_sk])).
% 21.70/3.28 cnf(p288, plain, (uptakepg(sk8(n0)) | ~spl49), inference(avatar_component_clause, [status(thm)], [sdef49])).
% 21.70/3.28 cnf(p342, plain, (~bcapacityne(n0) | ~gt(n0,sk9(n0)) | gt(n0,sk10(n0)) | gt(n0,X0) | conditionnormo(X0) | ~spl49), inference(resolution, [status(thm)], [c39, p288])).
% 21.70/3.28 cnf(ssp82, plain, (~spl49 | spl27 | spl28 | spl29 | spl30), inference(avatar_split_clause, [status(thm)], [p342, sdef27, sdef28, sdef29, sdef30])).
% 21.70/3.28 cnf(p154, plain, uptakepg(X0) | conditionhyper(sk0(X1)) | ~gt(X0,X2) | gt(X1,X2), inference(resolution, [status(thm)], [p92, c1])).
% 21.70/3.28 cnf(p343, plain, uptakepg(n0) | conditionhyper(sk0(X0)) | gt(X0,X1) | drugi(X1), inference(resolution, [status(thm)], [p154, c51])).
% 21.70/3.28 fof(sdef54, definition, (spl54 <=> (uptakepg(n0))), introduced(definition, [new_symbols(naming, [spl54])], [avatar_definition])).
% 21.70/3.28 cnf(ssp83, plain, (spl26 | spl54), inference(avatar_split_clause, [status(thm)], [p343, sdef26, sdef54])).
% 21.70/3.28 cnf(c40, plain, ~uptakepg(sk8(X0)) | ~bcapacityne(X0) | ~gt(X0,sk9(X0)) | ~conditionhyper(sk10(X0)) | gt(X0,X1) | conditionnormo(X1), inference(cnf_transformation, [status(esa)], [f16_sk])).
% 21.70/3.28 cnf(p348, plain, (~bcapacityne(n0) | ~gt(n0,sk9(n0)) | ~conditionhyper(sk10(n0)) | gt(n0,X0) | conditionnormo(X0) | ~spl49), inference(resolution, [status(thm)], [c40, p288])).
% 21.70/3.28 cnf(ssp84, plain, (~spl49 | spl27 | spl28 | spl30 | spl36), inference(avatar_split_clause, [status(thm)], [p348, sdef27, sdef28, sdef30, sdef36])).
% 21.70/3.28 cnf(c41, plain, ~uptakepg(sk8(X0)) | ~bcapacityne(X0) | ~bsecretioni(sk9(X0)) | gt(X0,sk10(X0)) | gt(X0,X1) | conditionnormo(X1), inference(cnf_transformation, [status(esa)], [f16_sk])).
% 21.70/3.28 cnf(p353, plain, (~bcapacityne(n0) | ~bsecretioni(sk9(n0)) | gt(n0,sk10(n0)) | gt(n0,X0) | conditionnormo(X0) | ~spl49), inference(resolution, [status(thm)], [c41, p288])).
% 21.70/3.28 cnf(ssp85, plain, (~spl49 | spl27 | spl29 | spl30 | spl39), inference(avatar_split_clause, [status(thm)], [p353, sdef27, sdef29, sdef30, sdef39])).
% 21.70/3.28 cnf(p320, plain, (conditionnormo(X0) | conditionhyper(sk0(X1)) | ~gt(X0,X2) | gt(X1,X2) | ~spl45), inference(resolution, [status(thm)], [p268, c1])).
% 21.70/3.28 cnf(p354, plain, (conditionnormo(n0) | conditionhyper(sk0(X0)) | gt(X0,X1) | drugi(X1) | ~spl45), inference(resolution, [status(thm)], [p320, c51])).
% 21.70/3.28 fof(sdef55, definition, (spl55 <=> (conditionnormo(n0))), introduced(definition, [new_symbols(naming, [spl55])], [avatar_definition])).
% 21.70/3.28 cnf(ssp86, plain, (~spl45 | spl26 | spl55), inference(avatar_split_clause, [status(thm)], [p354, sdef26, sdef55])).
% 21.70/3.28 fof(f12, axiom, ! [X0] : ( ( ! [X1] : ( ~ gt(X0,X1) => drugsu(X1) ) & ~ bcapacityex(X0) ) => ! [X1] : ( ~ gt(X0,X1) => bsecretioni(X1) ) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', sulfonylurea_effect)).
% 21.70/3.28 fof(f12_nnf, plain, ! [X0] : (((? [X1] : ((~(gt(X0,X1)) & ~(drugsu(X1)))) | bcapacityex(X0)) | ! [X1] : ((gt(X0,X1) | bsecretioni(X1))))), inference(nnf_transformation, [status(thm)], [f12])).
% 21.70/3.28 fof(f12_sk, plain, ! [X0,X1] : ((((~(gt(X0,sk1(X0))) & ~(drugsu(sk1(X0)))) | bcapacityex(X0)) | (gt(X0,X1) | bsecretioni(X1)))), inference(skolemisation, [status(esa), new_symbols(skolem, [sk1])], [f12_nnf])).
% 21.70/3.28 cnf(c15, plain, ~gt(X0,sk1(X0)) | bcapacityex(X0) | gt(X0,X1) | bsecretioni(X1), inference(cnf_transformation, [status(esa)], [f12_sk])).
% 21.70/3.28 cnf(p136, plain, uptakelg(sk1(X0)) | conditionhyper(sk0(X0)) | bcapacityex(X0) | gt(X0,X1) | bsecretioni(X1), inference(resolution, [status(thm)], [p85, c15])).
% 21.70/3.28 cnf(p358, plain, uptakelg(sk1(X0)) | conditionhyper(sk0(X0)) | bcapacityex(X0) | bsecretioni(X1) | gt(n0,X1) | drugi(X0), inference(resolution, [status(thm)], [p136, p60])).
% 21.70/3.28 fof(sdef56, definition, (spl56 <=> (uptakelg(sk1(X0)) | conditionhyper(sk0(X0)) | bcapacityex(X0) | drugi(X0))), introduced(definition, [new_symbols(naming, [spl56])], [avatar_definition])).
% 21.70/3.28 fof(sdef57, definition, (spl57 <=> (bsecretioni(X0) | gt(n0,X0))), introduced(definition, [new_symbols(naming, [spl57])], [avatar_definition])).
% 21.70/3.28 cnf(ssp87, plain, (spl56 | spl57), inference(avatar_split_clause, [status(thm)], [p358, sdef56, sdef57])).
% 21.70/3.28 cnf(c42, plain, ~uptakepg(sk8(X0)) | ~bcapacityne(X0) | ~bsecretioni(sk9(X0)) | ~conditionhyper(sk10(X0)) | gt(X0,X1) | conditionnormo(X1), inference(cnf_transformation, [status(esa)], [f16_sk])).
% 21.70/3.28 cnf(p378, plain, (~bcapacityne(n0) | ~bsecretioni(sk9(n0)) | ~conditionhyper(sk10(n0)) | gt(n0,X0) | conditionnormo(X0) | ~spl49), inference(resolution, [status(thm)], [c42, p288])).
% 21.70/3.28 cnf(ssp88, plain, (~spl49 | spl27 | spl30 | spl36 | spl39), inference(avatar_split_clause, [status(thm)], [p378, sdef27, sdef30, sdef36, sdef39])).
% 21.70/3.28 cnf(p360, plain, (bsecretioni(X0) | gt(n0,X0) | ~spl57), inference(avatar_component_clause, [status(thm)], [sdef57])).
% 21.70/3.28 cnf(p383, plain, (bsecretioni(sk0(n0)) | gt(n0,X0) | uptakelg(X0) | ~spl57), inference(resolution, [status(thm)], [p360, c10])).
% 21.70/3.28 fof(sdef58, definition, (spl58 <=> (bsecretioni(sk0(n0)))), introduced(definition, [new_symbols(naming, [spl58])], [avatar_definition])).
% 21.70/3.28 cnf(ssp89, plain, (~spl57 | spl2 | spl58), inference(avatar_split_clause, [status(thm)], [p383, sdef2, sdef58])).
% 21.70/3.28 cnf(p385, plain, (bsecretioni(sk0(n0)) | gt(n0,X0) | uptakepg(X0) | ~spl57), inference(resolution, [status(thm)], [p360, c11])).
% 21.70/3.28 cnf(ssp90, plain, (~spl57 | spl8 | spl58), inference(avatar_split_clause, [status(thm)], [p385, sdef8, sdef58])).
% 21.70/3.28 cnf(p386, plain, (bsecretioni(sk2(n0)) | gt(n0,X0) | ~releaselg(X0) | ~spl57), inference(resolution, [status(thm)], [p360, c17])).
% 21.70/3.28 fof(sdef59, definition, (spl59 <=> (bsecretioni(sk2(n0)))), introduced(definition, [new_symbols(naming, [spl59])], [avatar_definition])).
% 21.70/3.28 cnf(ssp91, plain, (~spl57 | spl13 | spl59), inference(avatar_split_clause, [status(thm)], [p386, sdef13, sdef59])).
% 21.70/3.28 cnf(p388, plain, (bsecretioni(X0) | uptakelg(n0) | conditionhyper(sk0(X1)) | gt(X1,X0) | ~spl57), inference(resolution, [status(thm)], [p360, p131])).
% 21.70/3.28 fof(sdef60, definition, (spl60 <=> (bsecretioni(X0) | conditionhyper(sk0(X1)) | gt(X1,X0))), introduced(definition, [new_symbols(naming, [spl60])], [avatar_definition])).
% 21.70/3.28 cnf(ssp92, plain, (~spl57 | spl25 | spl60), inference(avatar_split_clause, [status(thm)], [p388, sdef25, sdef60])).
% 21.70/3.28 cnf(p390, plain, (bsecretioni(sk7(n0)) | ~bcapacityne(n0) | ~gt(n0,sk9(n0)) | gt(n0,sk10(n0)) | gt(n0,X0) | conditionnormo(X0) | ~spl57), inference(resolution, [status(thm)], [p360, c27])).
% 21.70/3.28 fof(sdef61, definition, (spl61 <=> (bsecretioni(sk7(n0)))), introduced(definition, [new_symbols(naming, [spl61])], [avatar_definition])).
% 21.70/3.28 cnf(ssp93, plain, (~spl57 | spl27 | spl28 | spl29 | spl30 | spl61), inference(avatar_split_clause, [status(thm)], [p390, sdef27, sdef28, sdef29, sdef30, sdef61])).
% 21.70/3.28 cnf(p392, plain, (bsecretioni(sk7(n0)) | ~bcapacityne(n0) | ~gt(n0,sk9(n0)) | ~conditionhyper(sk10(n0)) | gt(n0,X0) | conditionnormo(X0) | ~spl57), inference(resolution, [status(thm)], [p360, c28])).
% 21.70/3.28 cnf(ssp94, plain, (~spl57 | spl27 | spl28 | spl30 | spl36 | spl61), inference(avatar_split_clause, [status(thm)], [p392, sdef27, sdef28, sdef30, sdef36, sdef61])).
% 21.70/3.28 cnf(p393, plain, (bsecretioni(sk7(n0)) | ~bcapacityne(n0) | ~bsecretioni(sk9(n0)) | gt(n0,sk10(n0)) | gt(n0,X0) | conditionnormo(X0) | ~spl57), inference(resolution, [status(thm)], [p360, c29])).
% 21.70/3.28 cnf(ssp95, plain, (~spl57 | spl27 | spl29 | spl30 | spl39 | spl61), inference(avatar_split_clause, [status(thm)], [p393, sdef27, sdef29, sdef30, sdef39, sdef61])).
% 21.70/3.28 cnf(p394, plain, (bsecretioni(sk7(n0)) | ~bcapacityne(n0) | ~bsecretioni(sk9(n0)) | ~conditionhyper(sk10(n0)) | gt(n0,X0) | conditionnormo(X0) | ~spl57), inference(resolution, [status(thm)], [p360, c30])).
% 21.70/3.28 cnf(ssp96, plain, (~spl57 | spl27 | spl30 | spl36 | spl39 | spl61), inference(avatar_split_clause, [status(thm)], [p394, sdef27, sdef30, sdef36, sdef39, sdef61])).
% 21.70/3.28 cnf(p395, plain, (bsecretioni(sk8(n0)) | ~bcapacityne(n0) | ~gt(n0,sk9(n0)) | gt(n0,sk10(n0)) | gt(n0,X0) | conditionnormo(X0) | ~spl57), inference(resolution, [status(thm)], [p360, c35])).
% 21.70/3.28 fof(sdef62, definition, (spl62 <=> (bsecretioni(sk8(n0)))), introduced(definition, [new_symbols(naming, [spl62])], [avatar_definition])).
% 21.70/3.28 cnf(ssp97, plain, (~spl57 | spl27 | spl28 | spl29 | spl30 | spl62), inference(avatar_split_clause, [status(thm)], [p395, sdef27, sdef28, sdef29, sdef30, sdef62])).
% 21.70/3.28 cnf(p397, plain, (bsecretioni(sk8(n0)) | ~bcapacityne(n0) | ~gt(n0,sk9(n0)) | ~conditionhyper(sk10(n0)) | gt(n0,X0) | conditionnormo(X0) | ~spl57), inference(resolution, [status(thm)], [p360, c36])).
% 21.70/3.28 cnf(ssp98, plain, (~spl57 | spl27 | spl28 | spl30 | spl36 | spl62), inference(avatar_split_clause, [status(thm)], [p397, sdef27, sdef28, sdef30, sdef36, sdef62])).
% 21.70/3.28 cnf(p398, plain, (bsecretioni(sk8(n0)) | ~bcapacityne(n0) | ~bsecretioni(sk9(n0)) | gt(n0,sk10(n0)) | gt(n0,X0) | conditionnormo(X0) | ~spl57), inference(resolution, [status(thm)], [p360, c37])).
% 21.70/3.28 cnf(ssp99, plain, (~spl57 | spl27 | spl29 | spl30 | spl39 | spl62), inference(avatar_split_clause, [status(thm)], [p398, sdef27, sdef29, sdef30, sdef39, sdef62])).
% 21.70/3.28 cnf(p399, plain, (bsecretioni(sk8(n0)) | ~bcapacityne(n0) | ~bsecretioni(sk9(n0)) | ~conditionhyper(sk10(n0)) | gt(n0,X0) | conditionnormo(X0) | ~spl57), inference(resolution, [status(thm)], [p360, c38])).
% 21.70/3.28 cnf(ssp100, plain, (~spl57 | spl27 | spl30 | spl36 | spl39 | spl62), inference(avatar_split_clause, [status(thm)], [p399, sdef27, sdef30, sdef36, sdef39, sdef62])).
% 21.70/3.28 cnf(p400, plain, (bsecretioni(X0) | uptakepg(n0) | conditionhyper(sk0(X1)) | gt(X1,X0) | ~spl57), inference(resolution, [status(thm)], [p360, p154])).
% 21.70/3.28 cnf(ssp101, plain, (~spl57 | spl54 | spl60), inference(avatar_split_clause, [status(thm)], [p400, sdef54, sdef60])).
% 21.70/3.28 cnf(p401, plain, (bsecretioni(X0) | conditionnormo(n0) | conditionhyper(sk0(X1)) | gt(X1,X0) | ~spl45 | ~spl57), inference(resolution, [status(thm)], [p360, p320])).
% 21.70/3.28 cnf(ssp102, plain, (~spl45 | ~spl57 | spl55 | spl60), inference(avatar_split_clause, [status(thm)], [p401, sdef55, sdef60])).
% 21.70/3.28 fof(f17, axiom, ! [X0] : ( ( ! [X1] : ( ~ gt(X0,X1) => uptakelg(X1) ) & ! [X1] : ( ~ gt(X0,X1) => uptakepg(X1) ) & bcapacityex(X0) & ! [X1] : ( gt(X0,X1) => conditionhyper(X1) ) ) => ! [X1] : ( ~ gt(X0,X1) => ( conditionnormo(X1) | conditionhypo(X1) ) ) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ex_cure)).
% 21.70/3.28 fof(f17_nnf, plain, ! [X0] : (((((? [X1] : ((~(gt(X0,X1)) & ~(uptakelg(X1)))) | ? [X1] : ((~(gt(X0,X1)) & ~(uptakepg(X1))))) | ~(bcapacityex(X0))) | ? [X1] : ((gt(X0,X1) & ~(conditionhyper(X1))))) | ! [X1] : ((gt(X0,X1) | (conditionnormo(X1) | conditionhypo(X1)))))), inference(nnf_transformation, [status(thm)], [f17])).
% 21.70/3.28 fof(f17_sk, plain, ! [X0,X1] : ((((((~(gt(X0,sk11(X0))) & ~(uptakelg(sk11(X0)))) | (~(gt(X0,sk12(X0))) & ~(uptakepg(sk12(X0))))) | ~(bcapacityex(X0))) | (gt(X0,sk13(X0)) & ~(conditionhyper(sk13(X0))))) | (gt(X0,X1) | (conditionnormo(X1) | conditionhypo(X1))))), inference(skolemisation, [status(esa), new_symbols(skolem, [sk11,sk12,sk13])], [f17_nnf])).
% 21.70/3.28 cnf(c43, plain, ~gt(X0,sk11(X0)) | ~gt(X0,sk12(X0)) | ~bcapacityex(X0) | gt(X0,sk13(X0)) | gt(X0,X1) | conditionnormo(X1) | conditionhypo(X1), inference(cnf_transformation, [status(esa)], [f17_sk])).
% 21.70/3.28 cnf(p403, plain, ~gt(n0,sk12(n0)) | ~bcapacityex(n0) | gt(n0,sk13(n0)) | gt(n0,X0) | conditionnormo(X0) | conditionhypo(X0) | drugi(sk11(n0)), inference(resolution, [status(thm)], [c43, c51])).
% 21.70/3.28 fof(sdef66, definition, (spl66 <=> (gt(n0,X0) | conditionnormo(X0) | conditionhypo(X0))), introduced(definition, [new_symbols(naming, [spl66])], [avatar_definition])).
% 21.70/3.28 fof(sdef67, definition, (spl67 <=> (drugi(sk11(n0)))), introduced(definition, [new_symbols(naming, [spl67])], [avatar_definition])).
% 21.70/3.28 cnf(ssp103, plain, (spl63 | spl64 | spl65 | spl66 | spl67), inference(avatar_split_clause, [status(thm)], [p403, sdef63, sdef64, sdef65, sdef66, sdef67])).
% 21.70/3.28 cnf(p409, plain, (~gt(n0,sk12(n0)) | ~bcapacityex(n0) | gt(n0,sk13(n0)) | gt(n0,X0) | conditionnormo(X0) | conditionhypo(X0) | uptakelg(sk11(n0)) | ~spl2), inference(resolution, [status(thm)], [c43, p67])).
% 21.70/3.28 fof(sdef68, definition, (spl68 <=> (uptakelg(sk11(n0)))), introduced(definition, [new_symbols(naming, [spl68])], [avatar_definition])).
% 21.70/3.28 cnf(ssp104, plain, (~spl2 | spl63 | spl64 | spl65 | spl66 | spl68), inference(avatar_split_clause, [status(thm)], [p409, sdef63, sdef64, sdef65, sdef66, sdef68])).
% 21.70/3.28 cnf(p411, plain, (~gt(n0,sk12(n0)) | ~bcapacityex(n0) | gt(n0,sk13(n0)) | gt(n0,X0) | conditionnormo(X0) | conditionhypo(X0) | uptakepg(sk11(n0)) | ~spl8), inference(resolution, [status(thm)], [c43, p80])).
% 21.70/3.28 fof(sdef69, definition, (spl69 <=> (uptakepg(sk11(n0)))), introduced(definition, [new_symbols(naming, [spl69])], [avatar_definition])).
% 21.70/3.28 cnf(ssp105, plain, (~spl8 | spl63 | spl64 | spl65 | spl66 | spl69), inference(avatar_split_clause, [status(thm)], [p411, sdef63, sdef64, sdef65, sdef66, sdef69])).
% 21.70/3.28 cnf(p413, plain, (~gt(n0,sk12(n0)) | ~bcapacityex(n0) | gt(n0,sk13(n0)) | gt(n0,X0) | conditionnormo(X0) | conditionhypo(X0) | uptakelg(sk11(n0)) | ~spl3), inference(resolution, [status(thm)], [c43, p86])).
% 21.70/3.28 cnf(ssp106, plain, (~spl3 | spl63 | spl64 | spl65 | spl66 | spl68), inference(avatar_split_clause, [status(thm)], [p413, sdef63, sdef64, sdef65, sdef66, sdef68])).
% 21.70/3.28 cnf(p414, plain, (~gt(n0,sk12(n0)) | ~bcapacityex(n0) | gt(n0,sk13(n0)) | gt(n0,X0) | conditionnormo(X0) | conditionhypo(X0) | uptakepg(sk11(n0)) | ~spl3), inference(resolution, [status(thm)], [c43, p93])).
% 21.70/3.28 cnf(ssp107, plain, (~spl3 | spl63 | spl64 | spl65 | spl66 | spl69), inference(avatar_split_clause, [status(thm)], [p414, sdef63, sdef64, sdef65, sdef66, sdef69])).
% 21.70/3.28 cnf(p418, plain, (~gt(n0,sk12(n0)) | ~bcapacityex(n0) | gt(n0,sk13(n0)) | gt(n0,X0) | conditionnormo(X0) | conditionhypo(X0) | bsecretioni(sk11(n0)) | ~spl57), inference(resolution, [status(thm)], [c43, p360])).
% 21.70/3.28 fof(sdef70, definition, (spl70 <=> (bsecretioni(sk11(n0)))), introduced(definition, [new_symbols(naming, [spl70])], [avatar_definition])).
% 21.70/3.28 cnf(ssp108, plain, (~spl57 | spl63 | spl64 | spl65 | spl66 | spl70), inference(avatar_split_clause, [status(thm)], [p418, sdef63, sdef64, sdef65, sdef66, sdef70])).
% 21.70/3.28 cnf(c44, plain, ~gt(X0,sk11(X0)) | ~gt(X0,sk12(X0)) | ~bcapacityex(X0) | ~conditionhyper(sk13(X0)) | gt(X0,X1) | conditionnormo(X1) | conditionhypo(X1), inference(cnf_transformation, [status(esa)], [f17_sk])).
% 21.70/3.28 cnf(p421, plain, ~gt(n0,sk12(n0)) | ~bcapacityex(n0) | ~conditionhyper(sk13(n0)) | gt(n0,X0) | conditionnormo(X0) | conditionhypo(X0) | drugi(sk11(n0)), inference(resolution, [status(thm)], [c44, c51])).
% 21.70/3.28 cnf(ssp109, plain, (spl63 | spl64 | spl66 | spl67 | spl71), inference(avatar_split_clause, [status(thm)], [p421, sdef63, sdef64, sdef66, sdef67, sdef71])).
% 21.70/3.28 cnf(p423, plain, (~gt(n0,sk12(n0)) | ~bcapacityex(n0) | ~conditionhyper(sk13(n0)) | gt(n0,X0) | conditionnormo(X0) | conditionhypo(X0) | uptakelg(sk11(n0)) | ~spl2), inference(resolution, [status(thm)], [c44, p67])).
% 21.70/3.28 cnf(ssp110, plain, (~spl2 | spl63 | spl64 | spl66 | spl68 | spl71), inference(avatar_split_clause, [status(thm)], [p423, sdef63, sdef64, sdef66, sdef68, sdef71])).
% 21.70/3.28 cnf(p424, plain, (~gt(n0,sk12(n0)) | ~bcapacityex(n0) | ~conditionhyper(sk13(n0)) | gt(n0,X0) | conditionnormo(X0) | conditionhypo(X0) | uptakepg(sk11(n0)) | ~spl8), inference(resolution, [status(thm)], [c44, p80])).
% 21.70/3.28 cnf(ssp111, plain, (~spl8 | spl63 | spl64 | spl66 | spl69 | spl71), inference(avatar_split_clause, [status(thm)], [p424, sdef63, sdef64, sdef66, sdef69, sdef71])).
% 21.70/3.28 cnf(p425, plain, (~gt(n0,sk12(n0)) | ~bcapacityex(n0) | ~conditionhyper(sk13(n0)) | gt(n0,X0) | conditionnormo(X0) | conditionhypo(X0) | uptakelg(sk11(n0)) | ~spl3), inference(resolution, [status(thm)], [c44, p86])).
% 21.70/3.28 cnf(ssp112, plain, (~spl3 | spl63 | spl64 | spl66 | spl68 | spl71), inference(avatar_split_clause, [status(thm)], [p425, sdef63, sdef64, sdef66, sdef68, sdef71])).
% 21.70/3.28 cnf(p426, plain, (~gt(n0,sk12(n0)) | ~bcapacityex(n0) | ~conditionhyper(sk13(n0)) | gt(n0,X0) | conditionnormo(X0) | conditionhypo(X0) | uptakepg(sk11(n0)) | ~spl3), inference(resolution, [status(thm)], [c44, p93])).
% 21.70/3.28 cnf(ssp113, plain, (~spl3 | spl63 | spl64 | spl66 | spl69 | spl71), inference(avatar_split_clause, [status(thm)], [p426, sdef63, sdef64, sdef66, sdef69, sdef71])).
% 21.70/3.28 cnf(p430, plain, (~gt(n0,sk12(n0)) | ~bcapacityex(n0) | ~conditionhyper(sk13(n0)) | gt(n0,X0) | conditionnormo(X0) | conditionhypo(X0) | bsecretioni(sk11(n0)) | ~spl57), inference(resolution, [status(thm)], [c44, p360])).
% 21.70/3.28 cnf(ssp114, plain, (~spl57 | spl63 | spl64 | spl66 | spl70 | spl71), inference(avatar_split_clause, [status(thm)], [p430, sdef63, sdef64, sdef66, sdef70, sdef71])).
% 21.70/3.28 cnf(p410, plain, (uptakelg(sk11(n0)) | ~spl68), inference(avatar_component_clause, [status(thm)], [sdef68])).
% 21.70/3.28 cnf(p431, plain, (gt(X0,sk11(n0)) | ~releaselg(sk11(n0)) | ~spl68), inference(resolution, [status(thm)], [p410, c14])).
% 21.70/3.28 fof(sdef73, definition, (spl73 <=> (~releaselg(sk11(n0)))), introduced(definition, [new_symbols(naming, [spl73])], [avatar_definition])).
% 21.70/3.28 cnf(ssp115, plain, (~spl68 | spl72 | spl73), inference(avatar_split_clause, [status(thm)], [p431, sdef72, sdef73])).
% 21.70/3.28 cnf(c45, plain, ~gt(X0,sk11(X0)) | ~uptakepg(sk12(X0)) | ~bcapacityex(X0) | gt(X0,sk13(X0)) | gt(X0,X1) | conditionnormo(X1) | conditionhypo(X1), inference(cnf_transformation, [status(esa)], [f17_sk])).
% 21.70/3.28 cnf(p435, plain, ~uptakepg(sk12(n0)) | ~bcapacityex(n0) | gt(n0,sk13(n0)) | gt(n0,X0) | conditionnormo(X0) | conditionhypo(X0) | drugi(sk11(n0)), inference(resolution, [status(thm)], [c45, c51])).
% 21.70/3.28 cnf(ssp116, plain, (spl64 | spl65 | spl66 | spl67 | spl74), inference(avatar_split_clause, [status(thm)], [p435, sdef64, sdef65, sdef66, sdef67, sdef74])).
% 21.70/3.28 cnf(p437, plain, (~uptakepg(sk12(n0)) | ~bcapacityex(n0) | gt(n0,sk13(n0)) | gt(n0,X0) | conditionnormo(X0) | conditionhypo(X0) | uptakelg(sk11(n0)) | ~spl2), inference(resolution, [status(thm)], [c45, p67])).
% 21.70/3.28 cnf(ssp117, plain, (~spl2 | spl64 | spl65 | spl66 | spl68 | spl74), inference(avatar_split_clause, [status(thm)], [p437, sdef64, sdef65, sdef66, sdef68, sdef74])).
% 21.70/3.28 cnf(p438, plain, (~uptakepg(sk12(n0)) | ~bcapacityex(n0) | gt(n0,sk13(n0)) | gt(n0,X0) | conditionnormo(X0) | conditionhypo(X0) | uptakepg(sk11(n0)) | ~spl8), inference(resolution, [status(thm)], [c45, p80])).
% 21.70/3.28 cnf(ssp118, plain, (~spl8 | spl64 | spl65 | spl66 | spl69 | spl74), inference(avatar_split_clause, [status(thm)], [p438, sdef64, sdef65, sdef66, sdef69, sdef74])).
% 21.70/3.28 cnf(p439, plain, (~uptakepg(sk12(n0)) | ~bcapacityex(n0) | gt(n0,sk13(n0)) | gt(n0,X0) | conditionnormo(X0) | conditionhypo(X0) | uptakelg(sk11(n0)) | ~spl3), inference(resolution, [status(thm)], [c45, p86])).
% 21.70/3.28 cnf(ssp119, plain, (~spl3 | spl64 | spl65 | spl66 | spl68 | spl74), inference(avatar_split_clause, [status(thm)], [p439, sdef64, sdef65, sdef66, sdef68, sdef74])).
% 21.70/3.28 cnf(p440, plain, (~uptakepg(sk12(n0)) | ~bcapacityex(n0) | gt(n0,sk13(n0)) | gt(n0,X0) | conditionnormo(X0) | conditionhypo(X0) | uptakepg(sk11(n0)) | ~spl3), inference(resolution, [status(thm)], [c45, p93])).
% 21.70/3.28 cnf(ssp120, plain, (~spl3 | spl64 | spl65 | spl66 | spl69 | spl74), inference(avatar_split_clause, [status(thm)], [p440, sdef64, sdef65, sdef66, sdef69, sdef74])).
% 21.70/3.28 cnf(p444, plain, (~uptakepg(sk12(n0)) | ~bcapacityex(n0) | gt(n0,sk13(n0)) | gt(n0,X0) | conditionnormo(X0) | conditionhypo(X0) | bsecretioni(sk11(n0)) | ~spl57), inference(resolution, [status(thm)], [c45, p360])).
% 21.70/3.28 cnf(ssp121, plain, (~spl57 | spl64 | spl65 | spl66 | spl70 | spl74), inference(avatar_split_clause, [status(thm)], [p444, sdef64, sdef65, sdef66, sdef70, sdef74])).
% 21.70/3.28 cnf(c46, plain, ~gt(X0,sk11(X0)) | ~uptakepg(sk12(X0)) | ~bcapacityex(X0) | ~conditionhyper(sk13(X0)) | gt(X0,X1) | conditionnormo(X1) | conditionhypo(X1), inference(cnf_transformation, [status(esa)], [f17_sk])).
% 21.70/3.28 cnf(p450, plain, ~uptakepg(sk12(n0)) | ~bcapacityex(n0) | ~conditionhyper(sk13(n0)) | gt(n0,X0) | conditionnormo(X0) | conditionhypo(X0) | drugi(sk11(n0)), inference(resolution, [status(thm)], [c46, c51])).
% 21.70/3.28 cnf(ssp122, plain, (spl64 | spl66 | spl67 | spl71 | spl74), inference(avatar_split_clause, [status(thm)], [p450, sdef64, sdef66, sdef67, sdef71, sdef74])).
% 21.70/3.28 cnf(p451, plain, (~uptakepg(sk12(n0)) | ~bcapacityex(n0) | ~conditionhyper(sk13(n0)) | gt(n0,X0) | conditionnormo(X0) | conditionhypo(X0) | uptakelg(sk11(n0)) | ~spl2), inference(resolution, [status(thm)], [c46, p67])).
% 21.70/3.28 cnf(ssp123, plain, (~spl2 | spl64 | spl66 | spl68 | spl71 | spl74), inference(avatar_split_clause, [status(thm)], [p451, sdef64, sdef66, sdef68, sdef71, sdef74])).
% 21.70/3.28 cnf(p452, plain, (~uptakepg(sk12(n0)) | ~bcapacityex(n0) | ~conditionhyper(sk13(n0)) | gt(n0,X0) | conditionnormo(X0) | conditionhypo(X0) | uptakepg(sk11(n0)) | ~spl8), inference(resolution, [status(thm)], [c46, p80])).
% 21.70/3.28 cnf(ssp124, plain, (~spl8 | spl64 | spl66 | spl69 | spl71 | spl74), inference(avatar_split_clause, [status(thm)], [p452, sdef64, sdef66, sdef69, sdef71, sdef74])).
% 21.70/3.28 cnf(p453, plain, (~uptakepg(sk12(n0)) | ~bcapacityex(n0) | ~conditionhyper(sk13(n0)) | gt(n0,X0) | conditionnormo(X0) | conditionhypo(X0) | uptakelg(sk11(n0)) | ~spl3), inference(resolution, [status(thm)], [c46, p86])).
% 21.70/3.28 cnf(ssp125, plain, (~spl3 | spl64 | spl66 | spl68 | spl71 | spl74), inference(avatar_split_clause, [status(thm)], [p453, sdef64, sdef66, sdef68, sdef71, sdef74])).
% 21.70/3.28 cnf(p454, plain, (~uptakepg(sk12(n0)) | ~bcapacityex(n0) | ~conditionhyper(sk13(n0)) | gt(n0,X0) | conditionnormo(X0) | conditionhypo(X0) | uptakepg(sk11(n0)) | ~spl3), inference(resolution, [status(thm)], [c46, p93])).
% 21.70/3.28 cnf(ssp126, plain, (~spl3 | spl64 | spl66 | spl69 | spl71 | spl74), inference(avatar_split_clause, [status(thm)], [p454, sdef64, sdef66, sdef69, sdef71, sdef74])).
% 21.70/3.28 cnf(p458, plain, (~uptakepg(sk12(n0)) | ~bcapacityex(n0) | ~conditionhyper(sk13(n0)) | gt(n0,X0) | conditionnormo(X0) | conditionhypo(X0) | bsecretioni(sk11(n0)) | ~spl57), inference(resolution, [status(thm)], [c46, p360])).
% 21.70/3.28 cnf(ssp127, plain, (~spl57 | spl64 | spl66 | spl70 | spl71 | spl74), inference(avatar_split_clause, [status(thm)], [p458, sdef64, sdef66, sdef70, sdef71, sdef74])).
% 21.70/3.28 cnf(c47, plain, ~uptakelg(sk11(X0)) | ~gt(X0,sk12(X0)) | ~bcapacityex(X0) | gt(X0,sk13(X0)) | gt(X0,X1) | conditionnormo(X1) | conditionhypo(X1), inference(cnf_transformation, [status(esa)], [f17_sk])).
% 21.70/3.28 cnf(p467, plain, (~gt(n0,sk12(n0)) | ~bcapacityex(n0) | gt(n0,sk13(n0)) | gt(n0,X0) | conditionnormo(X0) | conditionhypo(X0) | ~spl68), inference(resolution, [status(thm)], [c47, p410])).
% 21.70/3.28 cnf(ssp128, plain, (~spl68 | spl63 | spl64 | spl65 | spl66), inference(avatar_split_clause, [status(thm)], [p467, sdef63, sdef64, sdef65, sdef66])).
% 21.70/3.28 cnf(c48, plain, ~uptakelg(sk11(X0)) | ~gt(X0,sk12(X0)) | ~bcapacityex(X0) | ~conditionhyper(sk13(X0)) | gt(X0,X1) | conditionnormo(X1) | conditionhypo(X1), inference(cnf_transformation, [status(esa)], [f17_sk])).
% 21.70/3.28 cnf(p471, plain, (~gt(n0,sk12(n0)) | ~bcapacityex(n0) | ~conditionhyper(sk13(n0)) | gt(n0,X0) | conditionnormo(X0) | conditionhypo(X0) | ~spl68), inference(resolution, [status(thm)], [c48, p410])).
% 21.70/3.28 cnf(ssp129, plain, (~spl68 | spl63 | spl64 | spl66 | spl71), inference(avatar_split_clause, [status(thm)], [p471, sdef63, sdef64, sdef66, sdef71])).
% 21.70/3.28 cnf(p477, plain, (uptakelg(sk12(n0)) | conditionhyper(sk0(n0)) | ~spl63), inference(resolution, [status(thm)], [p404, p85])).
% 21.70/3.28 fof(sdef75, definition, (spl75 <=> (uptakelg(sk12(n0)))), introduced(definition, [new_symbols(naming, [spl75])], [avatar_definition])).
% 21.70/3.28 cnf(ssp130, plain, (~spl63 | spl20 | spl75), inference(avatar_split_clause, [status(thm)], [p477, sdef20, sdef75])).
% 21.70/3.28 cnf(p479, plain, (uptakepg(sk12(n0)) | conditionhyper(sk0(n0)) | ~spl63), inference(resolution, [status(thm)], [p404, p92])).
% 21.70/3.28 cnf(ssp131, plain, (~spl63 | spl20 | spl76), inference(avatar_split_clause, [status(thm)], [p479, sdef20, sdef76])).
% 21.70/3.28 cnf(p473, plain, (uptakelg(sk12(n0)) | ~spl2 | ~spl63), inference(resolution, [status(thm)], [p404, p67])).
% 21.70/3.28 cnf(p482, plain, (gt(X0,sk12(n0)) | ~releaselg(sk12(n0)) | ~spl2 | ~spl63), inference(resolution, [status(thm)], [p473, c14])).
% 21.70/3.28 fof(sdef78, definition, (spl78 <=> (~releaselg(sk12(n0)))), introduced(definition, [new_symbols(naming, [spl78])], [avatar_definition])).
% 21.70/3.28 cnf(ssp132, plain, (~spl2 | ~spl63 | spl77 | spl78), inference(avatar_split_clause, [status(thm)], [p482, sdef77, sdef78])).
% 21.70/3.28 cnf(p478, plain, (uptakelg(sk12(n0)) | ~spl75), inference(avatar_component_clause, [status(thm)], [sdef75])).
% 21.70/3.28 cnf(p490, plain, (gt(X0,sk12(n0)) | ~releaselg(sk12(n0)) | ~spl75), inference(resolution, [status(thm)], [p478, c14])).
% 21.70/3.28 cnf(ssp133, plain, (~spl75 | spl77 | spl78), inference(avatar_split_clause, [status(thm)], [p490, sdef77, sdef78])).
% 21.70/3.28 cnf(p494, plain, (uptakelg(n0) | conditionhyper(sk0(X0)) | gt(X0,sk13(n0)) | ~spl65), inference(resolution, [status(thm)], [p406, p131])).
% 21.70/3.28 fof(sdef79, definition, (spl79 <=> (conditionhyper(sk0(X0)) | gt(X0,sk13(n0)))), introduced(definition, [new_symbols(naming, [spl79])], [avatar_definition])).
% 21.70/3.28 cnf(ssp134, plain, (~spl65 | spl25 | spl79), inference(avatar_split_clause, [status(thm)], [p494, sdef25, sdef79])).
% 21.70/3.28 cnf(p496, plain, (uptakepg(n0) | conditionhyper(sk0(X0)) | gt(X0,sk13(n0)) | ~spl65), inference(resolution, [status(thm)], [p406, p154])).
% 21.70/3.28 cnf(ssp135, plain, (~spl65 | spl54 | spl79), inference(avatar_split_clause, [status(thm)], [p496, sdef54, sdef79])).
% 21.70/3.28 cnf(p493, plain, (~gt(sk13(n0),X0) | gt(n0,X0) | ~spl65), inference(resolution, [status(thm)], [p406, c1])).
% 21.70/3.28 cnf(p515, plain, (gt(n0,X0) | uptakelg(X0) | conditionhyper(sk0(sk13(n0))) | ~spl65), inference(resolution, [status(thm)], [p493, p85])).
% 21.70/3.28 fof(sdef80, definition, (spl80 <=> (conditionhyper(sk0(sk13(n0))))), introduced(definition, [new_symbols(naming, [spl80])], [avatar_definition])).
% 21.70/3.28 cnf(ssp136, plain, (~spl65 | spl2 | spl80), inference(avatar_split_clause, [status(thm)], [p515, sdef2, sdef80])).
% 21.70/3.28 cnf(p517, plain, (gt(n0,X0) | uptakepg(X0) | conditionhyper(sk0(sk13(n0))) | ~spl65), inference(resolution, [status(thm)], [p493, p92])).
% 21.70/3.28 cnf(ssp137, plain, (~spl65 | spl8 | spl80), inference(avatar_split_clause, [status(thm)], [p517, sdef8, sdef80])).
% 21.70/3.28 cnf(p518, plain, (gt(n0,sk10(n0)) | conditionhyper(sk0(sk13(n0))) | ~spl42 | ~spl65), inference(resolution, [status(thm)], [p493, p252])).
% 21.70/3.28 cnf(ssp138, plain, (~spl42 | ~spl65 | spl29 | spl80), inference(avatar_split_clause, [status(thm)], [p518, sdef29, sdef80])).
% 21.70/3.28 cnf(p519, plain, (gt(n0,X0) | uptakelg(sk1(sk13(n0))) | conditionhyper(sk0(sk13(n0))) | bcapacityex(sk13(n0)) | bsecretioni(X0) | ~spl65), inference(resolution, [status(thm)], [p493, p136])).
% 21.70/3.28 fof(sdef81, definition, (spl81 <=> (uptakelg(sk1(sk13(n0))))), introduced(definition, [new_symbols(naming, [spl81])], [avatar_definition])).
% 21.70/3.28 fof(sdef82, definition, (spl82 <=> (bcapacityex(sk13(n0)))), introduced(definition, [new_symbols(naming, [spl82])], [avatar_definition])).
% 21.70/3.28 cnf(ssp139, plain, (~spl65 | spl57 | spl80 | spl81 | spl82), inference(avatar_split_clause, [status(thm)], [p519, sdef57, sdef80, sdef81, sdef82])).
% 21.70/3.28 cnf(p520, plain, (uptakelg(sk1(sk13(n0))) | ~spl81), inference(avatar_component_clause, [status(thm)], [sdef81])).
% 21.70/3.28 cnf(p526, plain, (gt(X0,sk1(sk13(n0))) | ~releaselg(sk1(sk13(n0))) | ~spl81), inference(resolution, [status(thm)], [p520, c14])).
% 21.70/3.28 fof(sdef84, definition, (spl84 <=> (~releaselg(sk1(sk13(n0))))), introduced(definition, [new_symbols(naming, [spl84])], [avatar_definition])).
% 21.70/3.28 cnf(ssp140, plain, (~spl81 | spl83 | spl84), inference(avatar_split_clause, [status(thm)], [p526, sdef83, sdef84])).
% 21.70/3.28 cnf(p495, plain, (conditionhyper(sk0(X0)) | gt(X0,sk13(n0)) | ~spl79), inference(avatar_component_clause, [status(thm)], [sdef79])).
% 21.70/3.28 cnf(p532, plain, (conditionhyper(sk0(n0)) | conditionhyper(sk13(n0)) | ~spl79), inference(resolution, [status(thm)], [p495, c52])).
% 21.70/3.28 fof(sdef85, definition, (spl85 <=> (conditionhyper(sk13(n0)))), introduced(definition, [new_symbols(naming, [spl85])], [avatar_definition])).
% 21.70/3.28 cnf(ssp141, plain, (~spl79 | spl20 | spl85), inference(avatar_split_clause, [status(thm)], [p532, sdef20, sdef85])).
% 21.70/3.28 cnf(p535, plain, (conditionhyper(sk0(X0)) | gt(n0,sk13(n0)) | drugi(X0) | ~spl79), inference(resolution, [status(thm)], [p495, p60])).
% 21.70/3.28 cnf(ssp142, plain, (~spl79 | spl22 | spl65), inference(avatar_split_clause, [status(thm)], [p535, sdef22, sdef65])).
% 21.70/3.28 cnf(p158, plain, uptakepg(sk1(X0)) | conditionhyper(sk0(X0)) | bcapacityex(X0) | gt(X0,X1) | bsecretioni(X1), inference(resolution, [status(thm)], [p92, c15])).
% 21.70/3.28 cnf(p538, plain, uptakepg(sk1(X0)) | conditionhyper(sk0(X0)) | bcapacityex(X0) | bsecretioni(X1) | gt(n0,X1) | drugi(X0), inference(resolution, [status(thm)], [p158, p60])).
% 21.70/3.28 fof(sdef86, definition, (spl86 <=> (uptakepg(sk1(X0)) | conditionhyper(sk0(X0)) | bcapacityex(X0) | drugi(X0))), introduced(definition, [new_symbols(naming, [spl86])], [avatar_definition])).
% 21.70/3.28 cnf(ssp143, plain, (spl57 | spl86), inference(avatar_split_clause, [status(thm)], [p538, sdef57, sdef86])).
% 21.70/3.28 cnf(p554, plain, (uptakepg(sk1(sk13(n0))) | conditionhyper(sk0(sk13(n0))) | bcapacityex(sk13(n0)) | bsecretioni(X0) | gt(n0,X0) | ~spl65), inference(resolution, [status(thm)], [p158, p493])).
% 21.70/3.28 fof(sdef87, definition, (spl87 <=> (uptakepg(sk1(sk13(n0))))), introduced(definition, [new_symbols(naming, [spl87])], [avatar_definition])).
% 21.70/3.28 cnf(ssp144, plain, (~spl65 | spl57 | spl80 | spl82 | spl87), inference(avatar_split_clause, [status(thm)], [p554, sdef57, sdef80, sdef82, sdef87])).
% 21.70/3.28 cnf(p407, plain, (gt(n0,X0) | conditionnormo(X0) | conditionhypo(X0) | ~spl66), inference(avatar_component_clause, [status(thm)], [sdef66])).
% 21.70/3.28 cnf(p561, plain, (conditionnormo(sk14) | conditionhypo(sk14) | ~spl66), inference(resolution, [status(thm)], [p407, c54])).
% 21.70/3.28 cnf(ssp145, plain, (~spl66 | spl1 | spl52), inference(avatar_split_clause, [status(thm)], [p561, sdef1, sdef52])).
% 21.70/3.28 cnf(c49, plain, ~uptakelg(sk11(X0)) | ~uptakepg(sk12(X0)) | ~bcapacityex(X0) | gt(X0,sk13(X0)) | gt(X0,X1) | conditionnormo(X1) | conditionhypo(X1), inference(cnf_transformation, [status(esa)], [f17_sk])).
% 21.70/3.28 cnf(p563, plain, (~uptakepg(sk12(n0)) | ~bcapacityex(n0) | gt(n0,sk13(n0)) | gt(n0,X0) | conditionnormo(X0) | conditionhypo(X0) | ~spl68), inference(resolution, [status(thm)], [p410, c49])).
% 21.70/3.28 cnf(ssp146, plain, (~spl68 | spl64 | spl65 | spl66 | spl74), inference(avatar_split_clause, [status(thm)], [p563, sdef64, sdef65, sdef66, sdef74])).
% 21.70/3.28 cnf(c50, plain, ~uptakelg(sk11(X0)) | ~uptakepg(sk12(X0)) | ~bcapacityex(X0) | ~conditionhyper(sk13(X0)) | gt(X0,X1) | conditionnormo(X1) | conditionhypo(X1), inference(cnf_transformation, [status(esa)], [f17_sk])).
% 21.70/3.28 cnf(p564, plain, (~uptakepg(sk12(n0)) | ~bcapacityex(n0) | ~conditionhyper(sk13(n0)) | gt(n0,X0) | conditionnormo(X0) | conditionhypo(X0) | ~spl68), inference(resolution, [status(thm)], [p410, c50])).
% 21.70/3.28 cnf(ssp147, plain, (~spl68 | spl64 | spl66 | spl71 | spl74), inference(avatar_split_clause, [status(thm)], [p564, sdef64, sdef66, sdef71, sdef74])).
% 21.70/3.28 cnf(p475, plain, (uptakelg(sk12(n0)) | ~spl3 | ~spl63), inference(resolution, [status(thm)], [p404, p86])).
% 21.70/3.28 cnf(p570, plain, (gt(X0,sk12(n0)) | ~releaselg(sk12(n0)) | ~spl3 | ~spl63), inference(resolution, [status(thm)], [p475, c14])).
% 21.70/3.28 cnf(ssp148, plain, (~spl3 | ~spl63 | spl77 | spl78), inference(avatar_split_clause, [status(thm)], [p570, sdef77, sdef78])).
% 21.70/3.28 cnf(sat_ref, plain, $false, inference(avatar_sat_refutation, [status(thm)], [ssp0, ssp1, ssp2, ssp3, ssp4, ssp5, ssp6, ssp7, ssp8, ssp9, ssp10, ssp11, ssp12, ssp13, ssp14, ssp15, ssp16, ssp17, ssp18, ssp19, ssp20, ssp21, ssp22, ssp23, ssp24, ssp25, ssp26, ssp27, ssp28, ssp29, ssp30, ssp31, ssp32, ssp33, ssp34, ssp35, ssp36, ssp37, ssp38, ssp39, ssp40, ssp41, ssp42, ssp43, ssp44, ssp45, ssp46, ssp47, ssp48, ssp49, ssp50, ssp51, ssp52, ssp53, ssp54, ssp55, ssp56, ssp57, ssp58, ssp59, ssp60, ssp61, ssp62, ssp63, ssp64, ssp65, ssp66, ssp67, ssp68, ssp69, ssp70, ssp71, ssp72, ssp73, ssp74, ssp75, ssp76, ssp77, ssp78, ssp79, ssp80, ssp81, ssp82, ssp83, ssp84, ssp85, ssp86, ssp87, ssp88, ssp89, ssp90, ssp91, ssp92, ssp93, ssp94, ssp95, ssp96, ssp97, ssp98, ssp99, ssp100, ssp101, ssp102, ssp103, ssp104, ssp105, ssp106, ssp107, ssp108, ssp109, ssp110, ssp111, ssp112, ssp113, ssp114, ssp115, ssp116, ssp117, ssp118, ssp119, ssp120, ssp121, ssp122, ssp123, ssp124, ssp125, ssp126, ssp127, ssp128, ssp129, ssp130, ssp131, ssp132, ssp133, ssp134, ssp135, ssp136, ssp137, ssp138, ssp139, ssp140, ssp141, ssp142, ssp143, ssp144, ssp145, ssp146, ssp147, ssp148, sct0, sct1, sct2, sct3, sct4, sct5, sct6, sct7, sct8, sct9, sct10, sct11, sct12, sct13, sct14, sct15, sct16, sct17, sct18, sct19, sct20])).
% 21.70/3.28 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------