FindProof---0.1.THM-Prf.s

%------------------------------------------------------------------------------
% File     : FindProof---0.1
% Problem  : SYN067+1 : TPTP v9.3.1. Released v2.0.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300

% Computer : n016.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 03:33:41 PM UTC 2026

% Result   : Theorem 25.34s 13.92s
% Output   : Proof 25.34s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : SYN067+1 : TPTP v9.3.1. Released v2.0.0.
% 0.00/0.04  % Command  : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.11/10.58  % Computer : n016.cluster.edu
% 0.11/10.58  % Model    : x86_64 x86_64
% 0.11/10.58  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/10.58  % Memory   : 8046.5625MB
% 0.11/10.58  % OS       : Linux 6.8.0-71-generic
% 0.11/10.58  % CPULimit : 300
% 0.11/10.58  % WCLimit  : 300
% 0.11/10.58  % DateTime : Fri Sep 25 00:07:24 UTC 2026
% 0.11/10.58  % CPUTime  : 
% 0.11/10.58  Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 25.34/13.92  % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 25.34/13.92  % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 25.34/13.92  fof(sdef2, definition, (spl2 <=> (big_p(a))), introduced(definition, [new_symbols(naming, [spl2])], [avatar_definition])).
% 25.34/13.92  cnf(p3, plain, (big_p(a) | ~spl2), inference(avatar_component_clause, [status(thm)], [sdef2])).
% 25.34/13.92  fof(sdef0, definition, (spl0 <=> (~big_p(a))), introduced(definition, [new_symbols(naming, [spl0])], [avatar_definition])).
% 25.34/13.92  cnf(p1, plain, (~big_p(a) | ~spl0), inference(avatar_component_clause, [status(thm)], [sdef0])).
% 25.34/13.92  cnf(p191, plain, ($false | ~spl0 | ~spl2), inference(resolution, [status(thm)], [p3, p1])).
% 25.34/13.92  cnf(sct0, plain, (~spl0 | ~spl2), inference(avatar_contradiction_clause, [status(thm)], [p191])).
% 25.34/13.92  fof(sdef24, definition, (spl24 <=> (big_p(sk4))), introduced(definition, [new_symbols(naming, [spl24])], [avatar_definition])).
% 25.34/13.92  cnf(p202, plain, (big_p(sk4) | ~spl24), inference(avatar_component_clause, [status(thm)], [sdef24])).
% 25.34/13.92  fof(sdef3, definition, (spl3 <=> (~big_p(sk4))), introduced(definition, [new_symbols(naming, [spl3])], [avatar_definition])).
% 25.34/13.92  cnf(p5, plain, (~big_p(sk4) | ~spl3), inference(avatar_component_clause, [status(thm)], [sdef3])).
% 25.34/13.92  cnf(p205, plain, ($false | ~spl3 | ~spl24), inference(resolution, [status(thm)], [p202, p5])).
% 25.34/13.92  cnf(sct1, plain, (~spl3 | ~spl24), inference(avatar_contradiction_clause, [status(thm)], [p205])).
% 25.34/13.92  fof(sdef31, definition, (spl31 <=> (big_p(sk2))), introduced(definition, [new_symbols(naming, [spl31])], [avatar_definition])).
% 25.34/13.92  cnf(p297, plain, (big_p(sk2) | ~spl31), inference(avatar_component_clause, [status(thm)], [sdef31])).
% 25.34/13.92  fof(sdef21, definition, (spl21 <=> (~big_p(sk2))), introduced(definition, [new_symbols(naming, [spl21])], [avatar_definition])).
% 25.34/13.92  cnf(p122, plain, (~big_p(sk2) | ~spl21), inference(avatar_component_clause, [status(thm)], [sdef21])).
% 25.34/13.92  cnf(p299, plain, ($false | ~spl21 | ~spl31), inference(resolution, [status(thm)], [p297, p122])).
% 25.34/13.92  cnf(sct2, plain, (~spl21 | ~spl31), inference(avatar_contradiction_clause, [status(thm)], [p299])).
% 25.34/13.92  fof(sdef12, definition, (spl12 <=> (~big_p(X0) | ~big_r(X1,X0) | big_r(sk9(X1),sk8(X1)))), introduced(definition, [new_symbols(naming, [spl12])], [avatar_definition])).
% 25.34/13.92  cnf(p22, plain, (~big_p(X0) | ~big_r(X1,X0) | big_r(sk9(X1),sk8(X1)) | ~spl12), inference(avatar_component_clause, [status(thm)], [sdef12])).
% 25.34/13.92  fof(sdef4, definition, (spl4 <=> (big_p(sk5))), introduced(definition, [new_symbols(naming, [spl4])], [avatar_definition])).
% 25.34/13.92  cnf(p6, plain, (big_p(sk5) | ~spl4), inference(avatar_component_clause, [status(thm)], [sdef4])).
% 25.34/13.92  cnf(p223, plain, (~big_r(X0,sk5) | big_r(sk9(X0),sk8(X0)) | ~spl4 | ~spl12), inference(resolution, [status(thm)], [p22, p6])).
% 25.34/13.92  fof(sdef5, definition, (spl5 <=> (big_r(sk4,sk5))), introduced(definition, [new_symbols(naming, [spl5])], [avatar_definition])).
% 25.34/13.92  cnf(p8, plain, (big_r(sk4,sk5) | ~spl5), inference(avatar_component_clause, [status(thm)], [sdef5])).
% 25.34/13.92  cnf(p348, plain, (big_r(sk9(sk4),sk8(sk4)) | ~spl4 | ~spl5 | ~spl12), inference(resolution, [status(thm)], [p223, p8])).
% 25.34/13.92  fof(sdef10, definition, (spl10 <=> (~big_p(X0) | ~big_r(X1,X0) | big_p(sk8(X1)))), introduced(definition, [new_symbols(naming, [spl10])], [avatar_definition])).
% 25.34/13.92  cnf(p18, plain, (~big_p(X0) | ~big_r(X1,X0) | big_p(sk8(X1)) | ~spl10), inference(avatar_component_clause, [status(thm)], [sdef10])).
% 25.34/13.92  cnf(p207, plain, (~big_r(X0,sk5) | big_p(sk8(X0)) | ~spl4 | ~spl10), inference(resolution, [status(thm)], [p18, p6])).
% 25.34/13.92  cnf(p227, plain, (big_p(sk8(sk4)) | ~spl4 | ~spl5 | ~spl10), inference(resolution, [status(thm)], [p207, p8])).
% 25.34/13.92  fof(sdef6, definition, (spl6 <=> (~big_p(X0) | ~big_r(sk4,X1) | ~big_r(X1,X0))), introduced(definition, [new_symbols(naming, [spl6])], [avatar_definition])).
% 25.34/13.92  cnf(p10, plain, (~big_p(X0) | ~big_r(sk4,X1) | ~big_r(X1,X0) | ~spl6), inference(avatar_component_clause, [status(thm)], [sdef6])).
% 25.34/13.92  cnf(p228, plain, (~big_r(sk4,X0) | ~big_r(X0,sk8(sk4)) | ~spl4 | ~spl5 | ~spl6 | ~spl10), inference(resolution, [status(thm)], [p227, p10])).
% 25.34/13.92  fof(sdef11, definition, (spl11 <=> (~big_p(X0) | ~big_r(X1,X0) | big_r(X1,sk9(X1)))), introduced(definition, [new_symbols(naming, [spl11])], [avatar_definition])).
% 25.34/13.92  cnf(p20, plain, (~big_p(X0) | ~big_r(X1,X0) | big_r(X1,sk9(X1)) | ~spl11), inference(avatar_component_clause, [status(thm)], [sdef11])).
% 25.34/13.92  cnf(p215, plain, (~big_r(X0,sk5) | big_r(X0,sk9(X0)) | ~spl4 | ~spl11), inference(resolution, [status(thm)], [p20, p6])).
% 25.34/13.92  cnf(p237, plain, (big_r(sk4,sk9(sk4)) | ~spl4 | ~spl5 | ~spl11), inference(resolution, [status(thm)], [p215, p8])).
% 25.34/13.92  cnf(p282, plain, (~big_r(sk9(sk4),sk8(sk4)) | ~spl4 | ~spl5 | ~spl6 | ~spl10 | ~spl11), inference(resolution, [status(thm)], [p228, p237])).
% 25.34/13.92  cnf(p349, plain, ($false | ~spl4 | ~spl5 | ~spl6 | ~spl10 | ~spl11 | ~spl12), inference(resolution, [status(thm)], [p348, p282])).
% 25.34/13.92  cnf(sct3, plain, (~spl4 | ~spl5 | ~spl6 | ~spl10 | ~spl11 | ~spl12), inference(avatar_contradiction_clause, [status(thm)], [p349])).
% 25.34/13.92  fof(sdef20, definition, (spl20 <=> (~big_p(X0) | ~big_r(sk2,X1) | ~big_r(X1,X0))), introduced(definition, [new_symbols(naming, [spl20])], [avatar_definition])).
% 25.34/13.92  cnf(p111, plain, (~big_p(X0) | ~big_r(sk2,X1) | ~big_r(X1,X0) | ~spl20), inference(avatar_component_clause, [status(thm)], [sdef20])).
% 25.34/13.92  fof(sdef18, definition, (spl18 <=> (big_p(sk3))), introduced(definition, [new_symbols(naming, [spl18])], [avatar_definition])).
% 25.34/13.92  cnf(p89, plain, (big_p(sk3) | ~spl18), inference(avatar_component_clause, [status(thm)], [sdef18])).
% 25.34/13.92  cnf(p209, plain, (~big_r(X0,sk3) | big_p(sk8(X0)) | ~spl10 | ~spl18), inference(resolution, [status(thm)], [p18, p89])).
% 25.34/13.92  fof(sdef19, definition, (spl19 <=> (big_r(sk2,sk3))), introduced(definition, [new_symbols(naming, [spl19])], [avatar_definition])).
% 25.34/13.92  cnf(p100, plain, (big_r(sk2,sk3) | ~spl19), inference(avatar_component_clause, [status(thm)], [sdef19])).
% 25.34/13.92  cnf(p232, plain, (big_p(sk8(sk2)) | ~spl10 | ~spl18 | ~spl19), inference(resolution, [status(thm)], [p209, p100])).
% 25.34/13.92  cnf(p291, plain, (~big_r(sk2,X0) | ~big_r(X0,sk8(sk2)) | ~spl10 | ~spl18 | ~spl19 | ~spl20), inference(resolution, [status(thm)], [p111, p232])).
% 25.34/13.92  cnf(p217, plain, (~big_r(X0,sk3) | big_r(X0,sk9(X0)) | ~spl11 | ~spl18), inference(resolution, [status(thm)], [p20, p89])).
% 25.34/13.92  cnf(p269, plain, (big_r(sk2,sk9(sk2)) | ~spl11 | ~spl18 | ~spl19), inference(resolution, [status(thm)], [p217, p100])).
% 25.34/13.92  cnf(p429, plain, (~big_r(sk9(sk2),sk8(sk2)) | ~spl10 | ~spl11 | ~spl18 | ~spl19 | ~spl20), inference(resolution, [status(thm)], [p291, p269])).
% 25.34/13.92  cnf(p225, plain, (~big_r(X0,sk3) | big_r(sk9(X0),sk8(X0)) | ~spl12 | ~spl18), inference(resolution, [status(thm)], [p22, p89])).
% 25.34/13.92  cnf(p359, plain, (big_r(sk9(sk2),sk8(sk2)) | ~spl12 | ~spl18 | ~spl19), inference(resolution, [status(thm)], [p225, p100])).
% 25.34/13.92  cnf(p432, plain, ($false | ~spl10 | ~spl11 | ~spl12 | ~spl18 | ~spl19 | ~spl20), inference(resolution, [status(thm)], [p429, p359])).
% 25.34/13.92  cnf(sct4, plain, (~spl10 | ~spl11 | ~spl12 | ~spl18 | ~spl19 | ~spl20), inference(avatar_contradiction_clause, [status(thm)], [p432])).
% 25.34/13.92  fof(sdef65, definition, (spl65 <=> (~big_r(sk1(sk2),sk0(sk2)))), introduced(definition, [new_symbols(naming, [spl65])], [avatar_definition])).
% 25.34/13.92  cnf(p481, plain, (~big_r(sk1(sk2),sk0(sk2)) | ~spl65), inference(avatar_component_clause, [status(thm)], [sdef65])).
% 25.34/13.92  fof(sdef17, definition, (spl17 <=> (~big_p(X0) | ~big_r(X1,X0) | big_r(sk1(X1),sk0(X1)))), introduced(definition, [new_symbols(naming, [spl17])], [avatar_definition])).
% 25.34/13.92  cnf(p68, plain, (~big_p(X0) | ~big_r(X1,X0) | big_r(sk1(X1),sk0(X1)) | ~spl17), inference(avatar_component_clause, [status(thm)], [sdef17])).
% 25.34/13.92  cnf(p273, plain, (~big_r(X0,sk3) | big_r(sk1(X0),sk0(X0)) | ~spl17 | ~spl18), inference(resolution, [status(thm)], [p68, p89])).
% 25.34/13.92  cnf(p458, plain, (big_r(sk1(sk2),sk0(sk2)) | ~spl17 | ~spl18 | ~spl19), inference(resolution, [status(thm)], [p100, p273])).
% 25.34/13.92  cnf(p564, plain, ($false | ~spl17 | ~spl18 | ~spl19 | ~spl65), inference(resolution, [status(thm)], [p481, p458])).
% 25.34/13.92  cnf(sct5, plain, (~spl17 | ~spl18 | ~spl19 | ~spl65), inference(avatar_contradiction_clause, [status(thm)], [p564])).
% 25.34/13.92  fof(sdef15, definition, (spl15 <=> (~big_p(X0) | ~big_r(X1,X0) | big_p(sk0(X1)))), introduced(definition, [new_symbols(naming, [spl15])], [avatar_definition])).
% 25.34/13.92  cnf(p46, plain, (~big_p(X0) | ~big_r(X1,X0) | big_p(sk0(X1)) | ~spl15), inference(avatar_component_clause, [status(thm)], [sdef15])).
% 25.34/13.92  cnf(p244, plain, (~big_r(X0,sk3) | big_p(sk0(X0)) | ~spl15 | ~spl18), inference(resolution, [status(thm)], [p46, p89])).
% 25.34/13.92  cnf(p262, plain, (big_p(sk0(sk2)) | ~spl15 | ~spl18 | ~spl19), inference(resolution, [status(thm)], [p244, p100])).
% 25.34/13.92  cnf(p293, plain, (~big_r(sk2,X0) | ~big_r(X0,sk0(sk2)) | ~spl15 | ~spl18 | ~spl19 | ~spl20), inference(resolution, [status(thm)], [p111, p262])).
% 25.34/13.92  fof(sdef16, definition, (spl16 <=> (~big_p(X0) | ~big_r(X1,X0) | big_r(X1,sk1(X1)))), introduced(definition, [new_symbols(naming, [spl16])], [avatar_definition])).
% 25.34/13.92  cnf(p57, plain, (~big_p(X0) | ~big_r(X1,X0) | big_r(X1,sk1(X1)) | ~spl16), inference(avatar_component_clause, [status(thm)], [sdef16])).
% 25.34/13.92  cnf(p252, plain, (~big_r(X0,sk3) | big_r(X0,sk1(X0)) | ~spl16 | ~spl18), inference(resolution, [status(thm)], [p57, p89])).
% 25.34/13.92  cnf(p391, plain, (big_r(sk2,sk1(sk2)) | ~spl16 | ~spl18 | ~spl19), inference(resolution, [status(thm)], [p252, p100])).
% 25.34/13.92  cnf(p483, plain, (~big_r(sk1(sk2),sk0(sk2)) | ~spl15 | ~spl16 | ~spl18 | ~spl19 | ~spl20), inference(resolution, [status(thm)], [p293, p391])).
% 25.34/13.92  cnf(p566, plain, ($false | ~spl15 | ~spl16 | ~spl17 | ~spl18 | ~spl19 | ~spl20), inference(resolution, [status(thm)], [p483, p458])).
% 25.34/13.92  cnf(sct6, plain, (~spl15 | ~spl16 | ~spl17 | ~spl18 | ~spl19 | ~spl20), inference(avatar_contradiction_clause, [status(thm)], [p566])).
% 25.34/13.92  fof(f0, conjecture, ( ! [X] : ( ( big_p(a) & ( big_p(X) => ? [Y] : ( big_p(Y) & big_r(X,Y) ) ) ) => ? [Z,W] : ( big_p(Z) & big_r(X,W) & big_r(W,Z) ) ) <=> ! [X1] : ( ( ~ big_p(a) | big_p(X1) | ? [Z1,W1] : ( big_p(Z1) & big_r(X1,W1) & big_r(W1,Z1) ) ) & ( ~ big_p(a) | ~ ? [Y1] : ( big_p(Y1) & big_r(X1,Y1) ) | ? [Z2,W2] : ( big_p(Z2) & big_r(X1,W2) & big_r(W2,Z2) ) ) ) ), file('/export/starexec/sandbox/benchmark/theBenchmark.p', pel38)).
% 25.34/13.92  fof(f0_neg, negated_conjecture, ~(( ! [X] : ( ( big_p(a) & ( big_p(X) => ? [Y] : ( big_p(Y) & big_r(X,Y) ) ) ) => ? [Z,W] : ( big_p(Z) & big_r(X,W) & big_r(W,Z) ) ) <=> ! [X1] : ( ( ~ big_p(a) | big_p(X1) | ? [Z1,W1] : ( big_p(Z1) & big_r(X1,W1) & big_r(W1,Z1) ) ) & ( ~ big_p(a) | ~ ? [Y1] : ( big_p(Y1) & big_r(X1,Y1) ) | ? [Z2,W2] : ( big_p(Z2) & big_r(X1,W2) & big_r(W2,Z2) ) ) ) )), inference(negated_conjecture, [status(cth)], [f0])).
% 25.34/13.92  fof(f0_nnf, plain, ((! [X] : (((~(big_p(a)) | (big_p(X) & ! [Y] : ((~(big_p(Y)) | ~(big_r(X,Y)))))) | ? [Z,W] : (((big_p(Z) & big_r(X,W)) & big_r(W,Z))))) & ? [X1] : ((((big_p(a) & ~(big_p(X1))) & ! [Z1,W1] : (((~(big_p(Z1)) | ~(big_r(X1,W1))) | ~(big_r(W1,Z1))))) | ((big_p(a) & ? [Y1] : ((big_p(Y1) & big_r(X1,Y1)))) & ! [Z2,W2] : (((~(big_p(Z2)) | ~(big_r(X1,W2))) | ~(big_r(W2,Z2)))))))) | (? [X] : (((big_p(a) & (~(big_p(X)) | ? [Y] : ((big_p(Y) & big_r(X,Y))))) & ! [Z,W] : (((~(big_p(Z)) | ~(big_r(X,W))) | ~(big_r(W,Z)))))) & ! [X1] : ((((~(big_p(a)) | big_p(X1)) | ? [Z1,W1] : (((big_p(Z1) & big_r(X1,W1)) & big_r(W1,Z1)))) & ((~(big_p(a)) | ! [Y1] : ((~(big_p(Y1)) | ~(big_r(X1,Y1))))) | ? [Z2,W2] : (((big_p(Z2) & big_r(X1,W2)) & big_r(W2,Z2)))))))), inference(nnf_transformation, [status(thm)], [f0_neg])).
% 25.34/13.92  fof(f0_sk, plain, ! [X,Y,Z1,W1,Z2,W2,Z,W,X1,Y1] : (((((~(big_p(a)) | (big_p(X) & (~(big_p(Y)) | ~(big_r(X,Y))))) | ((big_p(sk0(X)) & big_r(X,sk1(X))) & big_r(sk1(X),sk0(X)))) & (((big_p(a) & ~(big_p(sk2))) & ((~(big_p(Z1)) | ~(big_r(sk2,W1))) | ~(big_r(W1,Z1)))) | ((big_p(a) & (big_p(sk3) & big_r(sk2,sk3))) & ((~(big_p(Z2)) | ~(big_r(sk2,W2))) | ~(big_r(W2,Z2)))))) | (((big_p(a) & (~(big_p(sk4)) | (big_p(sk5) & big_r(sk4,sk5)))) & ((~(big_p(Z)) | ~(big_r(sk4,W))) | ~(big_r(W,Z)))) & (((~(big_p(a)) | big_p(X1)) | ((big_p(sk6(X1)) & big_r(X1,sk7(X1))) & big_r(sk7(X1),sk6(X1)))) & ((~(big_p(a)) | (~(big_p(Y1)) | ~(big_r(X1,Y1)))) | ((big_p(sk8(X1)) & big_r(X1,sk9(X1))) & big_r(sk9(X1),sk8(X1)))))))), inference(skolemisation, [status(esa), new_symbols(skolem, [sk0,sk1,sk2,sk3,sk4,sk5,sk6,sk7,sk8,sk9])], [f0_nnf])).
% 25.34/13.92  cnf(c0, plain, ~big_p(a) | big_p(X0) | big_p(sk0(X0)) | big_p(a), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  fof(sdef1, definition, (spl1 <=> (big_p(X0) | big_p(sk0(X0)))), introduced(definition, [new_symbols(naming, [spl1])], [avatar_definition])).
% 25.34/13.92  cnf(ssp0, plain, (spl0 | spl1 | spl2), inference(avatar_split_clause, [status(thm)], [c0, sdef0, sdef1, sdef2])).
% 25.34/13.92  cnf(c1, plain, ~big_p(a) | big_p(X0) | big_p(sk0(X0)) | ~big_p(sk4) | big_p(sk5), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp1, plain, (spl0 | spl1 | spl3 | spl4), inference(avatar_split_clause, [status(thm)], [c1, sdef0, sdef1, sdef3, sdef4])).
% 25.34/13.92  cnf(c2, plain, ~big_p(a) | big_p(X0) | big_p(sk0(X0)) | ~big_p(sk4) | big_r(sk4,sk5), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp2, plain, (spl0 | spl1 | spl3 | spl5), inference(avatar_split_clause, [status(thm)], [c2, sdef0, sdef1, sdef3, sdef5])).
% 25.34/13.92  cnf(c3, plain, ~big_p(a) | big_p(X0) | big_p(sk0(X0)) | ~big_p(X2) | ~big_r(sk4,X3) | ~big_r(X3,X2), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp3, plain, (spl0 | spl1 | spl6), inference(avatar_split_clause, [status(thm)], [c3, sdef0, sdef1, sdef6])).
% 25.34/13.92  cnf(c4, plain, ~big_p(a) | big_p(X0) | big_p(sk0(X0)) | ~big_p(a) | big_p(X4) | big_p(sk6(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  fof(sdef7, definition, (spl7 <=> (big_p(X0) | big_p(sk6(X0)))), introduced(definition, [new_symbols(naming, [spl7])], [avatar_definition])).
% 25.34/13.92  cnf(ssp4, plain, (spl0 | spl1 | spl7), inference(avatar_split_clause, [status(thm)], [c4, sdef0, sdef1, sdef7])).
% 25.34/13.92  cnf(c5, plain, ~big_p(a) | big_p(X0) | big_p(sk0(X0)) | ~big_p(a) | big_p(X4) | big_r(X4,sk7(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  fof(sdef8, definition, (spl8 <=> (big_p(X0) | big_r(X0,sk7(X0)))), introduced(definition, [new_symbols(naming, [spl8])], [avatar_definition])).
% 25.34/13.92  cnf(ssp5, plain, (spl0 | spl1 | spl8), inference(avatar_split_clause, [status(thm)], [c5, sdef0, sdef1, sdef8])).
% 25.34/13.92  cnf(c6, plain, ~big_p(a) | big_p(X0) | big_p(sk0(X0)) | ~big_p(a) | big_p(X4) | big_r(sk7(X4),sk6(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  fof(sdef9, definition, (spl9 <=> (big_p(X0) | big_r(sk7(X0),sk6(X0)))), introduced(definition, [new_symbols(naming, [spl9])], [avatar_definition])).
% 25.34/13.92  cnf(ssp6, plain, (spl0 | spl1 | spl9), inference(avatar_split_clause, [status(thm)], [c6, sdef0, sdef1, sdef9])).
% 25.34/13.92  cnf(c7, plain, ~big_p(a) | big_p(X0) | big_p(sk0(X0)) | ~big_p(a) | ~big_p(X7) | ~big_r(X4,X7) | big_p(sk8(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp7, plain, (spl0 | spl1 | spl10), inference(avatar_split_clause, [status(thm)], [c7, sdef0, sdef1, sdef10])).
% 25.34/13.92  cnf(c8, plain, ~big_p(a) | big_p(X0) | big_p(sk0(X0)) | ~big_p(a) | ~big_p(X7) | ~big_r(X4,X7) | big_r(X4,sk9(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp8, plain, (spl0 | spl1 | spl11), inference(avatar_split_clause, [status(thm)], [c8, sdef0, sdef1, sdef11])).
% 25.34/13.92  cnf(c9, plain, ~big_p(a) | big_p(X0) | big_p(sk0(X0)) | ~big_p(a) | ~big_p(X7) | ~big_r(X4,X7) | big_r(sk9(X4),sk8(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp9, plain, (spl0 | spl1 | spl12), inference(avatar_split_clause, [status(thm)], [c9, sdef0, sdef1, sdef12])).
% 25.34/13.92  cnf(c10, plain, ~big_p(a) | big_p(X0) | big_r(X0,sk1(X0)) | big_p(a), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  fof(sdef13, definition, (spl13 <=> (big_p(X0) | big_r(X0,sk1(X0)))), introduced(definition, [new_symbols(naming, [spl13])], [avatar_definition])).
% 25.34/13.92  cnf(ssp10, plain, (spl0 | spl2 | spl13), inference(avatar_split_clause, [status(thm)], [c10, sdef0, sdef2, sdef13])).
% 25.34/13.92  cnf(c11, plain, ~big_p(a) | big_p(X0) | big_r(X0,sk1(X0)) | ~big_p(sk4) | big_p(sk5), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp11, plain, (spl0 | spl3 | spl4 | spl13), inference(avatar_split_clause, [status(thm)], [c11, sdef0, sdef3, sdef4, sdef13])).
% 25.34/13.92  cnf(c12, plain, ~big_p(a) | big_p(X0) | big_r(X0,sk1(X0)) | ~big_p(sk4) | big_r(sk4,sk5), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp12, plain, (spl0 | spl3 | spl5 | spl13), inference(avatar_split_clause, [status(thm)], [c12, sdef0, sdef3, sdef5, sdef13])).
% 25.34/13.92  cnf(c13, plain, ~big_p(a) | big_p(X0) | big_r(X0,sk1(X0)) | ~big_p(X2) | ~big_r(sk4,X3) | ~big_r(X3,X2), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp13, plain, (spl0 | spl6 | spl13), inference(avatar_split_clause, [status(thm)], [c13, sdef0, sdef6, sdef13])).
% 25.34/13.92  cnf(c14, plain, ~big_p(a) | big_p(X0) | big_r(X0,sk1(X0)) | ~big_p(a) | big_p(X4) | big_p(sk6(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp14, plain, (spl0 | spl7 | spl13), inference(avatar_split_clause, [status(thm)], [c14, sdef0, sdef7, sdef13])).
% 25.34/13.92  cnf(c15, plain, ~big_p(a) | big_p(X0) | big_r(X0,sk1(X0)) | ~big_p(a) | big_p(X4) | big_r(X4,sk7(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp15, plain, (spl0 | spl8 | spl13), inference(avatar_split_clause, [status(thm)], [c15, sdef0, sdef8, sdef13])).
% 25.34/13.92  cnf(c16, plain, ~big_p(a) | big_p(X0) | big_r(X0,sk1(X0)) | ~big_p(a) | big_p(X4) | big_r(sk7(X4),sk6(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp16, plain, (spl0 | spl9 | spl13), inference(avatar_split_clause, [status(thm)], [c16, sdef0, sdef9, sdef13])).
% 25.34/13.92  cnf(c17, plain, ~big_p(a) | big_p(X0) | big_r(X0,sk1(X0)) | ~big_p(a) | ~big_p(X7) | ~big_r(X4,X7) | big_p(sk8(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp17, plain, (spl0 | spl10 | spl13), inference(avatar_split_clause, [status(thm)], [c17, sdef0, sdef10, sdef13])).
% 25.34/13.92  cnf(c18, plain, ~big_p(a) | big_p(X0) | big_r(X0,sk1(X0)) | ~big_p(a) | ~big_p(X7) | ~big_r(X4,X7) | big_r(X4,sk9(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp18, plain, (spl0 | spl11 | spl13), inference(avatar_split_clause, [status(thm)], [c18, sdef0, sdef11, sdef13])).
% 25.34/13.92  cnf(c19, plain, ~big_p(a) | big_p(X0) | big_r(X0,sk1(X0)) | ~big_p(a) | ~big_p(X7) | ~big_r(X4,X7) | big_r(sk9(X4),sk8(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp19, plain, (spl0 | spl12 | spl13), inference(avatar_split_clause, [status(thm)], [c19, sdef0, sdef12, sdef13])).
% 25.34/13.92  cnf(c20, plain, ~big_p(a) | big_p(X0) | big_r(sk1(X0),sk0(X0)) | big_p(a), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  fof(sdef14, definition, (spl14 <=> (big_p(X0) | big_r(sk1(X0),sk0(X0)))), introduced(definition, [new_symbols(naming, [spl14])], [avatar_definition])).
% 25.34/13.92  cnf(ssp20, plain, (spl0 | spl2 | spl14), inference(avatar_split_clause, [status(thm)], [c20, sdef0, sdef2, sdef14])).
% 25.34/13.92  cnf(c21, plain, ~big_p(a) | big_p(X0) | big_r(sk1(X0),sk0(X0)) | ~big_p(sk4) | big_p(sk5), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp21, plain, (spl0 | spl3 | spl4 | spl14), inference(avatar_split_clause, [status(thm)], [c21, sdef0, sdef3, sdef4, sdef14])).
% 25.34/13.92  cnf(c22, plain, ~big_p(a) | big_p(X0) | big_r(sk1(X0),sk0(X0)) | ~big_p(sk4) | big_r(sk4,sk5), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp22, plain, (spl0 | spl3 | spl5 | spl14), inference(avatar_split_clause, [status(thm)], [c22, sdef0, sdef3, sdef5, sdef14])).
% 25.34/13.92  cnf(c23, plain, ~big_p(a) | big_p(X0) | big_r(sk1(X0),sk0(X0)) | ~big_p(X2) | ~big_r(sk4,X3) | ~big_r(X3,X2), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp23, plain, (spl0 | spl6 | spl14), inference(avatar_split_clause, [status(thm)], [c23, sdef0, sdef6, sdef14])).
% 25.34/13.92  cnf(c24, plain, ~big_p(a) | big_p(X0) | big_r(sk1(X0),sk0(X0)) | ~big_p(a) | big_p(X4) | big_p(sk6(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp24, plain, (spl0 | spl7 | spl14), inference(avatar_split_clause, [status(thm)], [c24, sdef0, sdef7, sdef14])).
% 25.34/13.92  cnf(c25, plain, ~big_p(a) | big_p(X0) | big_r(sk1(X0),sk0(X0)) | ~big_p(a) | big_p(X4) | big_r(X4,sk7(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp25, plain, (spl0 | spl8 | spl14), inference(avatar_split_clause, [status(thm)], [c25, sdef0, sdef8, sdef14])).
% 25.34/13.92  cnf(c26, plain, ~big_p(a) | big_p(X0) | big_r(sk1(X0),sk0(X0)) | ~big_p(a) | big_p(X4) | big_r(sk7(X4),sk6(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp26, plain, (spl0 | spl9 | spl14), inference(avatar_split_clause, [status(thm)], [c26, sdef0, sdef9, sdef14])).
% 25.34/13.92  cnf(c27, plain, ~big_p(a) | big_p(X0) | big_r(sk1(X0),sk0(X0)) | ~big_p(a) | ~big_p(X7) | ~big_r(X4,X7) | big_p(sk8(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp27, plain, (spl0 | spl10 | spl14), inference(avatar_split_clause, [status(thm)], [c27, sdef0, sdef10, sdef14])).
% 25.34/13.92  cnf(c28, plain, ~big_p(a) | big_p(X0) | big_r(sk1(X0),sk0(X0)) | ~big_p(a) | ~big_p(X7) | ~big_r(X4,X7) | big_r(X4,sk9(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp28, plain, (spl0 | spl11 | spl14), inference(avatar_split_clause, [status(thm)], [c28, sdef0, sdef11, sdef14])).
% 25.34/13.92  cnf(c29, plain, ~big_p(a) | big_p(X0) | big_r(sk1(X0),sk0(X0)) | ~big_p(a) | ~big_p(X7) | ~big_r(X4,X7) | big_r(sk9(X4),sk8(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp29, plain, (spl0 | spl12 | spl14), inference(avatar_split_clause, [status(thm)], [c29, sdef0, sdef12, sdef14])).
% 25.34/13.92  cnf(c30, plain, ~big_p(a) | ~big_p(X1) | ~big_r(X0,X1) | big_p(sk0(X0)) | big_p(a), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp30, plain, (spl0 | spl2 | spl15), inference(avatar_split_clause, [status(thm)], [c30, sdef0, sdef2, sdef15])).
% 25.34/13.92  cnf(c31, plain, ~big_p(a) | ~big_p(X1) | ~big_r(X0,X1) | big_p(sk0(X0)) | ~big_p(sk4) | big_p(sk5), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp31, plain, (spl0 | spl3 | spl4 | spl15), inference(avatar_split_clause, [status(thm)], [c31, sdef0, sdef3, sdef4, sdef15])).
% 25.34/13.92  cnf(c32, plain, ~big_p(a) | ~big_p(X1) | ~big_r(X0,X1) | big_p(sk0(X0)) | ~big_p(sk4) | big_r(sk4,sk5), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp32, plain, (spl0 | spl3 | spl5 | spl15), inference(avatar_split_clause, [status(thm)], [c32, sdef0, sdef3, sdef5, sdef15])).
% 25.34/13.92  cnf(c33, plain, ~big_p(a) | ~big_p(X1) | ~big_r(X0,X1) | big_p(sk0(X0)) | ~big_p(X2) | ~big_r(sk4,X3) | ~big_r(X3,X2), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp33, plain, (spl0 | spl6 | spl15), inference(avatar_split_clause, [status(thm)], [c33, sdef0, sdef6, sdef15])).
% 25.34/13.92  cnf(c34, plain, ~big_p(a) | ~big_p(X1) | ~big_r(X0,X1) | big_p(sk0(X0)) | ~big_p(a) | big_p(X4) | big_p(sk6(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp34, plain, (spl0 | spl7 | spl15), inference(avatar_split_clause, [status(thm)], [c34, sdef0, sdef7, sdef15])).
% 25.34/13.92  cnf(c35, plain, ~big_p(a) | ~big_p(X1) | ~big_r(X0,X1) | big_p(sk0(X0)) | ~big_p(a) | big_p(X4) | big_r(X4,sk7(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp35, plain, (spl0 | spl8 | spl15), inference(avatar_split_clause, [status(thm)], [c35, sdef0, sdef8, sdef15])).
% 25.34/13.92  cnf(c36, plain, ~big_p(a) | ~big_p(X1) | ~big_r(X0,X1) | big_p(sk0(X0)) | ~big_p(a) | big_p(X4) | big_r(sk7(X4),sk6(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp36, plain, (spl0 | spl9 | spl15), inference(avatar_split_clause, [status(thm)], [c36, sdef0, sdef9, sdef15])).
% 25.34/13.92  cnf(c37, plain, ~big_p(a) | ~big_p(X1) | ~big_r(X0,X1) | big_p(sk0(X0)) | ~big_p(a) | ~big_p(X7) | ~big_r(X4,X7) | big_p(sk8(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp37, plain, (spl0 | spl10 | spl15), inference(avatar_split_clause, [status(thm)], [c37, sdef0, sdef10, sdef15])).
% 25.34/13.92  cnf(c38, plain, ~big_p(a) | ~big_p(X1) | ~big_r(X0,X1) | big_p(sk0(X0)) | ~big_p(a) | ~big_p(X7) | ~big_r(X4,X7) | big_r(X4,sk9(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp38, plain, (spl0 | spl11 | spl15), inference(avatar_split_clause, [status(thm)], [c38, sdef0, sdef11, sdef15])).
% 25.34/13.92  cnf(c39, plain, ~big_p(a) | ~big_p(X1) | ~big_r(X0,X1) | big_p(sk0(X0)) | ~big_p(a) | ~big_p(X7) | ~big_r(X4,X7) | big_r(sk9(X4),sk8(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp39, plain, (spl0 | spl12 | spl15), inference(avatar_split_clause, [status(thm)], [c39, sdef0, sdef12, sdef15])).
% 25.34/13.92  cnf(c40, plain, ~big_p(a) | ~big_p(X1) | ~big_r(X0,X1) | big_r(X0,sk1(X0)) | big_p(a), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp40, plain, (spl0 | spl2 | spl16), inference(avatar_split_clause, [status(thm)], [c40, sdef0, sdef2, sdef16])).
% 25.34/13.92  cnf(c41, plain, ~big_p(a) | ~big_p(X1) | ~big_r(X0,X1) | big_r(X0,sk1(X0)) | ~big_p(sk4) | big_p(sk5), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp41, plain, (spl0 | spl3 | spl4 | spl16), inference(avatar_split_clause, [status(thm)], [c41, sdef0, sdef3, sdef4, sdef16])).
% 25.34/13.92  cnf(c42, plain, ~big_p(a) | ~big_p(X1) | ~big_r(X0,X1) | big_r(X0,sk1(X0)) | ~big_p(sk4) | big_r(sk4,sk5), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp42, plain, (spl0 | spl3 | spl5 | spl16), inference(avatar_split_clause, [status(thm)], [c42, sdef0, sdef3, sdef5, sdef16])).
% 25.34/13.92  cnf(c43, plain, ~big_p(a) | ~big_p(X1) | ~big_r(X0,X1) | big_r(X0,sk1(X0)) | ~big_p(X2) | ~big_r(sk4,X3) | ~big_r(X3,X2), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp43, plain, (spl0 | spl6 | spl16), inference(avatar_split_clause, [status(thm)], [c43, sdef0, sdef6, sdef16])).
% 25.34/13.92  cnf(c44, plain, ~big_p(a) | ~big_p(X1) | ~big_r(X0,X1) | big_r(X0,sk1(X0)) | ~big_p(a) | big_p(X4) | big_p(sk6(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp44, plain, (spl0 | spl7 | spl16), inference(avatar_split_clause, [status(thm)], [c44, sdef0, sdef7, sdef16])).
% 25.34/13.92  cnf(c45, plain, ~big_p(a) | ~big_p(X1) | ~big_r(X0,X1) | big_r(X0,sk1(X0)) | ~big_p(a) | big_p(X4) | big_r(X4,sk7(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp45, plain, (spl0 | spl8 | spl16), inference(avatar_split_clause, [status(thm)], [c45, sdef0, sdef8, sdef16])).
% 25.34/13.92  cnf(c46, plain, ~big_p(a) | ~big_p(X1) | ~big_r(X0,X1) | big_r(X0,sk1(X0)) | ~big_p(a) | big_p(X4) | big_r(sk7(X4),sk6(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp46, plain, (spl0 | spl9 | spl16), inference(avatar_split_clause, [status(thm)], [c46, sdef0, sdef9, sdef16])).
% 25.34/13.92  cnf(c47, plain, ~big_p(a) | ~big_p(X1) | ~big_r(X0,X1) | big_r(X0,sk1(X0)) | ~big_p(a) | ~big_p(X7) | ~big_r(X4,X7) | big_p(sk8(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp47, plain, (spl0 | spl10 | spl16), inference(avatar_split_clause, [status(thm)], [c47, sdef0, sdef10, sdef16])).
% 25.34/13.92  cnf(c48, plain, ~big_p(a) | ~big_p(X1) | ~big_r(X0,X1) | big_r(X0,sk1(X0)) | ~big_p(a) | ~big_p(X7) | ~big_r(X4,X7) | big_r(X4,sk9(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp48, plain, (spl0 | spl11 | spl16), inference(avatar_split_clause, [status(thm)], [c48, sdef0, sdef11, sdef16])).
% 25.34/13.92  cnf(c49, plain, ~big_p(a) | ~big_p(X1) | ~big_r(X0,X1) | big_r(X0,sk1(X0)) | ~big_p(a) | ~big_p(X7) | ~big_r(X4,X7) | big_r(sk9(X4),sk8(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp49, plain, (spl0 | spl12 | spl16), inference(avatar_split_clause, [status(thm)], [c49, sdef0, sdef12, sdef16])).
% 25.34/13.92  cnf(c50, plain, ~big_p(a) | ~big_p(X1) | ~big_r(X0,X1) | big_r(sk1(X0),sk0(X0)) | big_p(a), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp50, plain, (spl0 | spl2 | spl17), inference(avatar_split_clause, [status(thm)], [c50, sdef0, sdef2, sdef17])).
% 25.34/13.92  cnf(c51, plain, ~big_p(a) | ~big_p(X1) | ~big_r(X0,X1) | big_r(sk1(X0),sk0(X0)) | ~big_p(sk4) | big_p(sk5), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp51, plain, (spl0 | spl3 | spl4 | spl17), inference(avatar_split_clause, [status(thm)], [c51, sdef0, sdef3, sdef4, sdef17])).
% 25.34/13.92  cnf(c52, plain, ~big_p(a) | ~big_p(X1) | ~big_r(X0,X1) | big_r(sk1(X0),sk0(X0)) | ~big_p(sk4) | big_r(sk4,sk5), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp52, plain, (spl0 | spl3 | spl5 | spl17), inference(avatar_split_clause, [status(thm)], [c52, sdef0, sdef3, sdef5, sdef17])).
% 25.34/13.92  cnf(c53, plain, ~big_p(a) | ~big_p(X1) | ~big_r(X0,X1) | big_r(sk1(X0),sk0(X0)) | ~big_p(X2) | ~big_r(sk4,X3) | ~big_r(X3,X2), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp53, plain, (spl0 | spl6 | spl17), inference(avatar_split_clause, [status(thm)], [c53, sdef0, sdef6, sdef17])).
% 25.34/13.92  cnf(c54, plain, ~big_p(a) | ~big_p(X1) | ~big_r(X0,X1) | big_r(sk1(X0),sk0(X0)) | ~big_p(a) | big_p(X4) | big_p(sk6(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp54, plain, (spl0 | spl7 | spl17), inference(avatar_split_clause, [status(thm)], [c54, sdef0, sdef7, sdef17])).
% 25.34/13.92  cnf(c55, plain, ~big_p(a) | ~big_p(X1) | ~big_r(X0,X1) | big_r(sk1(X0),sk0(X0)) | ~big_p(a) | big_p(X4) | big_r(X4,sk7(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp55, plain, (spl0 | spl8 | spl17), inference(avatar_split_clause, [status(thm)], [c55, sdef0, sdef8, sdef17])).
% 25.34/13.92  cnf(c56, plain, ~big_p(a) | ~big_p(X1) | ~big_r(X0,X1) | big_r(sk1(X0),sk0(X0)) | ~big_p(a) | big_p(X4) | big_r(sk7(X4),sk6(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp56, plain, (spl0 | spl9 | spl17), inference(avatar_split_clause, [status(thm)], [c56, sdef0, sdef9, sdef17])).
% 25.34/13.92  cnf(c57, plain, ~big_p(a) | ~big_p(X1) | ~big_r(X0,X1) | big_r(sk1(X0),sk0(X0)) | ~big_p(a) | ~big_p(X7) | ~big_r(X4,X7) | big_p(sk8(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp57, plain, (spl0 | spl10 | spl17), inference(avatar_split_clause, [status(thm)], [c57, sdef0, sdef10, sdef17])).
% 25.34/13.92  cnf(c58, plain, ~big_p(a) | ~big_p(X1) | ~big_r(X0,X1) | big_r(sk1(X0),sk0(X0)) | ~big_p(a) | ~big_p(X7) | ~big_r(X4,X7) | big_r(X4,sk9(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp58, plain, (spl0 | spl11 | spl17), inference(avatar_split_clause, [status(thm)], [c58, sdef0, sdef11, sdef17])).
% 25.34/13.92  cnf(c59, plain, ~big_p(a) | ~big_p(X1) | ~big_r(X0,X1) | big_r(sk1(X0),sk0(X0)) | ~big_p(a) | ~big_p(X7) | ~big_r(X4,X7) | big_r(sk9(X4),sk8(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp59, plain, (spl0 | spl12 | spl17), inference(avatar_split_clause, [status(thm)], [c59, sdef0, sdef12, sdef17])).
% 25.34/13.92  cnf(c60, plain, big_p(a) | big_p(a) | big_p(a), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp60, plain, (spl2), inference(avatar_split_clause, [status(thm)], [c60, sdef2])).
% 25.34/13.92  cnf(c61, plain, big_p(a) | big_p(a) | ~big_p(sk4) | big_p(sk5), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp61, plain, (spl2 | spl3 | spl4), inference(avatar_split_clause, [status(thm)], [c61, sdef2, sdef3, sdef4])).
% 25.34/13.92  cnf(c62, plain, big_p(a) | big_p(a) | ~big_p(sk4) | big_r(sk4,sk5), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp62, plain, (spl2 | spl3 | spl5), inference(avatar_split_clause, [status(thm)], [c62, sdef2, sdef3, sdef5])).
% 25.34/13.92  cnf(c63, plain, big_p(a) | big_p(a) | ~big_p(X2) | ~big_r(sk4,X3) | ~big_r(X3,X2), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp63, plain, (spl2 | spl6), inference(avatar_split_clause, [status(thm)], [c63, sdef2, sdef6])).
% 25.34/13.92  cnf(c64, plain, big_p(a) | big_p(a) | ~big_p(a) | big_p(X4) | big_p(sk6(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp64, plain, (spl0 | spl2 | spl7), inference(avatar_split_clause, [status(thm)], [c64, sdef0, sdef2, sdef7])).
% 25.34/13.92  cnf(c65, plain, big_p(a) | big_p(a) | ~big_p(a) | big_p(X4) | big_r(X4,sk7(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp65, plain, (spl0 | spl2 | spl8), inference(avatar_split_clause, [status(thm)], [c65, sdef0, sdef2, sdef8])).
% 25.34/13.92  cnf(c66, plain, big_p(a) | big_p(a) | ~big_p(a) | big_p(X4) | big_r(sk7(X4),sk6(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp66, plain, (spl0 | spl2 | spl9), inference(avatar_split_clause, [status(thm)], [c66, sdef0, sdef2, sdef9])).
% 25.34/13.92  cnf(c67, plain, big_p(a) | big_p(a) | ~big_p(a) | ~big_p(X7) | ~big_r(X4,X7) | big_p(sk8(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp67, plain, (spl0 | spl2 | spl10), inference(avatar_split_clause, [status(thm)], [c67, sdef0, sdef2, sdef10])).
% 25.34/13.92  cnf(c68, plain, big_p(a) | big_p(a) | ~big_p(a) | ~big_p(X7) | ~big_r(X4,X7) | big_r(X4,sk9(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp68, plain, (spl0 | spl2 | spl11), inference(avatar_split_clause, [status(thm)], [c68, sdef0, sdef2, sdef11])).
% 25.34/13.92  cnf(c69, plain, big_p(a) | big_p(a) | ~big_p(a) | ~big_p(X7) | ~big_r(X4,X7) | big_r(sk9(X4),sk8(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp69, plain, (spl0 | spl2 | spl12), inference(avatar_split_clause, [status(thm)], [c69, sdef0, sdef2, sdef12])).
% 25.34/13.92  cnf(c70, plain, big_p(a) | big_p(sk3) | big_p(a), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp70, plain, (spl2 | spl18), inference(avatar_split_clause, [status(thm)], [c70, sdef2, sdef18])).
% 25.34/13.92  cnf(c71, plain, big_p(a) | big_p(sk3) | ~big_p(sk4) | big_p(sk5), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp71, plain, (spl2 | spl3 | spl4 | spl18), inference(avatar_split_clause, [status(thm)], [c71, sdef2, sdef3, sdef4, sdef18])).
% 25.34/13.92  cnf(c72, plain, big_p(a) | big_p(sk3) | ~big_p(sk4) | big_r(sk4,sk5), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp72, plain, (spl2 | spl3 | spl5 | spl18), inference(avatar_split_clause, [status(thm)], [c72, sdef2, sdef3, sdef5, sdef18])).
% 25.34/13.92  cnf(c73, plain, big_p(a) | big_p(sk3) | ~big_p(X2) | ~big_r(sk4,X3) | ~big_r(X3,X2), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp73, plain, (spl2 | spl6 | spl18), inference(avatar_split_clause, [status(thm)], [c73, sdef2, sdef6, sdef18])).
% 25.34/13.92  cnf(c74, plain, big_p(a) | big_p(sk3) | ~big_p(a) | big_p(X4) | big_p(sk6(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp74, plain, (spl0 | spl2 | spl7 | spl18), inference(avatar_split_clause, [status(thm)], [c74, sdef0, sdef2, sdef7, sdef18])).
% 25.34/13.92  cnf(c75, plain, big_p(a) | big_p(sk3) | ~big_p(a) | big_p(X4) | big_r(X4,sk7(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp75, plain, (spl0 | spl2 | spl8 | spl18), inference(avatar_split_clause, [status(thm)], [c75, sdef0, sdef2, sdef8, sdef18])).
% 25.34/13.92  cnf(c76, plain, big_p(a) | big_p(sk3) | ~big_p(a) | big_p(X4) | big_r(sk7(X4),sk6(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp76, plain, (spl0 | spl2 | spl9 | spl18), inference(avatar_split_clause, [status(thm)], [c76, sdef0, sdef2, sdef9, sdef18])).
% 25.34/13.92  cnf(c77, plain, big_p(a) | big_p(sk3) | ~big_p(a) | ~big_p(X7) | ~big_r(X4,X7) | big_p(sk8(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp77, plain, (spl0 | spl2 | spl10 | spl18), inference(avatar_split_clause, [status(thm)], [c77, sdef0, sdef2, sdef10, sdef18])).
% 25.34/13.92  cnf(c78, plain, big_p(a) | big_p(sk3) | ~big_p(a) | ~big_p(X7) | ~big_r(X4,X7) | big_r(X4,sk9(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp78, plain, (spl0 | spl2 | spl11 | spl18), inference(avatar_split_clause, [status(thm)], [c78, sdef0, sdef2, sdef11, sdef18])).
% 25.34/13.92  cnf(c79, plain, big_p(a) | big_p(sk3) | ~big_p(a) | ~big_p(X7) | ~big_r(X4,X7) | big_r(sk9(X4),sk8(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp79, plain, (spl0 | spl2 | spl12 | spl18), inference(avatar_split_clause, [status(thm)], [c79, sdef0, sdef2, sdef12, sdef18])).
% 25.34/13.92  cnf(c80, plain, big_p(a) | big_r(sk2,sk3) | big_p(a), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp80, plain, (spl2 | spl19), inference(avatar_split_clause, [status(thm)], [c80, sdef2, sdef19])).
% 25.34/13.92  cnf(c81, plain, big_p(a) | big_r(sk2,sk3) | ~big_p(sk4) | big_p(sk5), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp81, plain, (spl2 | spl3 | spl4 | spl19), inference(avatar_split_clause, [status(thm)], [c81, sdef2, sdef3, sdef4, sdef19])).
% 25.34/13.92  cnf(c82, plain, big_p(a) | big_r(sk2,sk3) | ~big_p(sk4) | big_r(sk4,sk5), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp82, plain, (spl2 | spl3 | spl5 | spl19), inference(avatar_split_clause, [status(thm)], [c82, sdef2, sdef3, sdef5, sdef19])).
% 25.34/13.92  cnf(c83, plain, big_p(a) | big_r(sk2,sk3) | ~big_p(X2) | ~big_r(sk4,X3) | ~big_r(X3,X2), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp83, plain, (spl2 | spl6 | spl19), inference(avatar_split_clause, [status(thm)], [c83, sdef2, sdef6, sdef19])).
% 25.34/13.92  cnf(c84, plain, big_p(a) | big_r(sk2,sk3) | ~big_p(a) | big_p(X4) | big_p(sk6(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp84, plain, (spl0 | spl2 | spl7 | spl19), inference(avatar_split_clause, [status(thm)], [c84, sdef0, sdef2, sdef7, sdef19])).
% 25.34/13.92  cnf(c85, plain, big_p(a) | big_r(sk2,sk3) | ~big_p(a) | big_p(X4) | big_r(X4,sk7(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp85, plain, (spl0 | spl2 | spl8 | spl19), inference(avatar_split_clause, [status(thm)], [c85, sdef0, sdef2, sdef8, sdef19])).
% 25.34/13.92  cnf(c86, plain, big_p(a) | big_r(sk2,sk3) | ~big_p(a) | big_p(X4) | big_r(sk7(X4),sk6(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp86, plain, (spl0 | spl2 | spl9 | spl19), inference(avatar_split_clause, [status(thm)], [c86, sdef0, sdef2, sdef9, sdef19])).
% 25.34/13.92  cnf(c87, plain, big_p(a) | big_r(sk2,sk3) | ~big_p(a) | ~big_p(X7) | ~big_r(X4,X7) | big_p(sk8(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp87, plain, (spl0 | spl2 | spl10 | spl19), inference(avatar_split_clause, [status(thm)], [c87, sdef0, sdef2, sdef10, sdef19])).
% 25.34/13.92  cnf(c88, plain, big_p(a) | big_r(sk2,sk3) | ~big_p(a) | ~big_p(X7) | ~big_r(X4,X7) | big_r(X4,sk9(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp88, plain, (spl0 | spl2 | spl11 | spl19), inference(avatar_split_clause, [status(thm)], [c88, sdef0, sdef2, sdef11, sdef19])).
% 25.34/13.92  cnf(c89, plain, big_p(a) | big_r(sk2,sk3) | ~big_p(a) | ~big_p(X7) | ~big_r(X4,X7) | big_r(sk9(X4),sk8(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp89, plain, (spl0 | spl2 | spl12 | spl19), inference(avatar_split_clause, [status(thm)], [c89, sdef0, sdef2, sdef12, sdef19])).
% 25.34/13.92  cnf(c170, plain, ~big_p(X5) | ~big_r(sk2,X6) | ~big_r(X6,X5) | ~big_p(X8) | ~big_r(sk2,X9) | ~big_r(X9,X8) | big_p(a), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp90, plain, (spl2 | spl20), inference(avatar_split_clause, [status(thm)], [c170, sdef2, sdef20])).
% 25.34/13.92  cnf(c141, plain, ~big_p(X5) | ~big_r(sk2,X6) | ~big_r(X6,X5) | big_p(a) | ~big_p(sk4) | big_p(sk5), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp91, plain, (spl2 | spl3 | spl4 | spl20), inference(avatar_split_clause, [status(thm)], [c141, sdef2, sdef3, sdef4, sdef20])).
% 25.34/13.92  cnf(c142, plain, ~big_p(X5) | ~big_r(sk2,X6) | ~big_r(X6,X5) | big_p(a) | ~big_p(sk4) | big_r(sk4,sk5), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp92, plain, (spl2 | spl3 | spl5 | spl20), inference(avatar_split_clause, [status(thm)], [c142, sdef2, sdef3, sdef5, sdef20])).
% 25.34/13.92  cnf(c143, plain, ~big_p(X5) | ~big_r(sk2,X6) | ~big_r(X6,X5) | big_p(a) | ~big_p(X2) | ~big_r(sk4,X3) | ~big_r(X3,X2), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp93, plain, (spl2 | spl6 | spl20), inference(avatar_split_clause, [status(thm)], [c143, sdef2, sdef6, sdef20])).
% 25.34/13.92  cnf(c144, plain, ~big_p(X5) | ~big_r(sk2,X6) | ~big_r(X6,X5) | big_p(a) | ~big_p(a) | big_p(X4) | big_p(sk6(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp94, plain, (spl0 | spl2 | spl7 | spl20), inference(avatar_split_clause, [status(thm)], [c144, sdef0, sdef2, sdef7, sdef20])).
% 25.34/13.92  cnf(c145, plain, ~big_p(X5) | ~big_r(sk2,X6) | ~big_r(X6,X5) | big_p(a) | ~big_p(a) | big_p(X4) | big_r(X4,sk7(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp95, plain, (spl0 | spl2 | spl8 | spl20), inference(avatar_split_clause, [status(thm)], [c145, sdef0, sdef2, sdef8, sdef20])).
% 25.34/13.92  cnf(c146, plain, ~big_p(X5) | ~big_r(sk2,X6) | ~big_r(X6,X5) | big_p(a) | ~big_p(a) | big_p(X4) | big_r(sk7(X4),sk6(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp96, plain, (spl0 | spl2 | spl9 | spl20), inference(avatar_split_clause, [status(thm)], [c146, sdef0, sdef2, sdef9, sdef20])).
% 25.34/13.92  cnf(c147, plain, ~big_p(X5) | ~big_r(sk2,X6) | ~big_r(X6,X5) | big_p(a) | ~big_p(a) | ~big_p(X7) | ~big_r(X4,X7) | big_p(sk8(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp97, plain, (spl0 | spl2 | spl10 | spl20), inference(avatar_split_clause, [status(thm)], [c147, sdef0, sdef2, sdef10, sdef20])).
% 25.34/13.92  cnf(c148, plain, ~big_p(X5) | ~big_r(sk2,X6) | ~big_r(X6,X5) | big_p(a) | ~big_p(a) | ~big_p(X7) | ~big_r(X4,X7) | big_r(X4,sk9(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp98, plain, (spl0 | spl2 | spl11 | spl20), inference(avatar_split_clause, [status(thm)], [c148, sdef0, sdef2, sdef11, sdef20])).
% 25.34/13.92  cnf(c149, plain, ~big_p(X5) | ~big_r(sk2,X6) | ~big_r(X6,X5) | big_p(a) | ~big_p(a) | ~big_p(X7) | ~big_r(X4,X7) | big_r(sk9(X4),sk8(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp99, plain, (spl0 | spl2 | spl12 | spl20), inference(avatar_split_clause, [status(thm)], [c149, sdef0, sdef2, sdef12, sdef20])).
% 25.34/13.92  cnf(c100, plain, ~big_p(sk2) | big_p(a) | big_p(a), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp100, plain, (spl2 | spl21), inference(avatar_split_clause, [status(thm)], [c100, sdef2, sdef21])).
% 25.34/13.92  cnf(c101, plain, ~big_p(sk2) | big_p(a) | ~big_p(sk4) | big_p(sk5), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp101, plain, (spl2 | spl3 | spl4 | spl21), inference(avatar_split_clause, [status(thm)], [c101, sdef2, sdef3, sdef4, sdef21])).
% 25.34/13.92  cnf(c102, plain, ~big_p(sk2) | big_p(a) | ~big_p(sk4) | big_r(sk4,sk5), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp102, plain, (spl2 | spl3 | spl5 | spl21), inference(avatar_split_clause, [status(thm)], [c102, sdef2, sdef3, sdef5, sdef21])).
% 25.34/13.92  cnf(c103, plain, ~big_p(sk2) | big_p(a) | ~big_p(X2) | ~big_r(sk4,X3) | ~big_r(X3,X2), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp103, plain, (spl2 | spl6 | spl21), inference(avatar_split_clause, [status(thm)], [c103, sdef2, sdef6, sdef21])).
% 25.34/13.92  cnf(c104, plain, ~big_p(sk2) | big_p(a) | ~big_p(a) | big_p(X4) | big_p(sk6(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp104, plain, (spl0 | spl2 | spl7 | spl21), inference(avatar_split_clause, [status(thm)], [c104, sdef0, sdef2, sdef7, sdef21])).
% 25.34/13.92  cnf(c105, plain, ~big_p(sk2) | big_p(a) | ~big_p(a) | big_p(X4) | big_r(X4,sk7(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp105, plain, (spl0 | spl2 | spl8 | spl21), inference(avatar_split_clause, [status(thm)], [c105, sdef0, sdef2, sdef8, sdef21])).
% 25.34/13.92  cnf(c106, plain, ~big_p(sk2) | big_p(a) | ~big_p(a) | big_p(X4) | big_r(sk7(X4),sk6(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp106, plain, (spl0 | spl2 | spl9 | spl21), inference(avatar_split_clause, [status(thm)], [c106, sdef0, sdef2, sdef9, sdef21])).
% 25.34/13.92  cnf(c107, plain, ~big_p(sk2) | big_p(a) | ~big_p(a) | ~big_p(X7) | ~big_r(X4,X7) | big_p(sk8(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp107, plain, (spl0 | spl2 | spl10 | spl21), inference(avatar_split_clause, [status(thm)], [c107, sdef0, sdef2, sdef10, sdef21])).
% 25.34/13.92  cnf(c108, plain, ~big_p(sk2) | big_p(a) | ~big_p(a) | ~big_p(X7) | ~big_r(X4,X7) | big_r(X4,sk9(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp108, plain, (spl0 | spl2 | spl11 | spl21), inference(avatar_split_clause, [status(thm)], [c108, sdef0, sdef2, sdef11, sdef21])).
% 25.34/13.92  cnf(c109, plain, ~big_p(sk2) | big_p(a) | ~big_p(a) | ~big_p(X7) | ~big_r(X4,X7) | big_r(sk9(X4),sk8(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp109, plain, (spl0 | spl2 | spl12 | spl21), inference(avatar_split_clause, [status(thm)], [c109, sdef0, sdef2, sdef12, sdef21])).
% 25.34/13.92  cnf(c110, plain, ~big_p(sk2) | big_p(sk3) | big_p(a), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp110, plain, (spl2 | spl18 | spl21), inference(avatar_split_clause, [status(thm)], [c110, sdef2, sdef18, sdef21])).
% 25.34/13.92  cnf(c111, plain, ~big_p(sk2) | big_p(sk3) | ~big_p(sk4) | big_p(sk5), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp111, plain, (spl3 | spl4 | spl18 | spl21), inference(avatar_split_clause, [status(thm)], [c111, sdef3, sdef4, sdef18, sdef21])).
% 25.34/13.92  cnf(c112, plain, ~big_p(sk2) | big_p(sk3) | ~big_p(sk4) | big_r(sk4,sk5), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp112, plain, (spl3 | spl5 | spl18 | spl21), inference(avatar_split_clause, [status(thm)], [c112, sdef3, sdef5, sdef18, sdef21])).
% 25.34/13.92  cnf(c113, plain, ~big_p(sk2) | big_p(sk3) | ~big_p(X2) | ~big_r(sk4,X3) | ~big_r(X3,X2), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp113, plain, (spl6 | spl18 | spl21), inference(avatar_split_clause, [status(thm)], [c113, sdef6, sdef18, sdef21])).
% 25.34/13.92  cnf(c114, plain, ~big_p(sk2) | big_p(sk3) | ~big_p(a) | big_p(X4) | big_p(sk6(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp114, plain, (spl0 | spl7 | spl18 | spl21), inference(avatar_split_clause, [status(thm)], [c114, sdef0, sdef7, sdef18, sdef21])).
% 25.34/13.92  cnf(c115, plain, ~big_p(sk2) | big_p(sk3) | ~big_p(a) | big_p(X4) | big_r(X4,sk7(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp115, plain, (spl0 | spl8 | spl18 | spl21), inference(avatar_split_clause, [status(thm)], [c115, sdef0, sdef8, sdef18, sdef21])).
% 25.34/13.92  cnf(c116, plain, ~big_p(sk2) | big_p(sk3) | ~big_p(a) | big_p(X4) | big_r(sk7(X4),sk6(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp116, plain, (spl0 | spl9 | spl18 | spl21), inference(avatar_split_clause, [status(thm)], [c116, sdef0, sdef9, sdef18, sdef21])).
% 25.34/13.92  cnf(c117, plain, ~big_p(sk2) | big_p(sk3) | ~big_p(a) | ~big_p(X7) | ~big_r(X4,X7) | big_p(sk8(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp117, plain, (spl0 | spl10 | spl18 | spl21), inference(avatar_split_clause, [status(thm)], [c117, sdef0, sdef10, sdef18, sdef21])).
% 25.34/13.92  cnf(c118, plain, ~big_p(sk2) | big_p(sk3) | ~big_p(a) | ~big_p(X7) | ~big_r(X4,X7) | big_r(X4,sk9(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp118, plain, (spl0 | spl11 | spl18 | spl21), inference(avatar_split_clause, [status(thm)], [c118, sdef0, sdef11, sdef18, sdef21])).
% 25.34/13.92  cnf(c119, plain, ~big_p(sk2) | big_p(sk3) | ~big_p(a) | ~big_p(X7) | ~big_r(X4,X7) | big_r(sk9(X4),sk8(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp119, plain, (spl0 | spl12 | spl18 | spl21), inference(avatar_split_clause, [status(thm)], [c119, sdef0, sdef12, sdef18, sdef21])).
% 25.34/13.92  cnf(c120, plain, ~big_p(sk2) | big_r(sk2,sk3) | big_p(a), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp120, plain, (spl2 | spl19 | spl21), inference(avatar_split_clause, [status(thm)], [c120, sdef2, sdef19, sdef21])).
% 25.34/13.92  cnf(c121, plain, ~big_p(sk2) | big_r(sk2,sk3) | ~big_p(sk4) | big_p(sk5), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp121, plain, (spl3 | spl4 | spl19 | spl21), inference(avatar_split_clause, [status(thm)], [c121, sdef3, sdef4, sdef19, sdef21])).
% 25.34/13.92  cnf(c122, plain, ~big_p(sk2) | big_r(sk2,sk3) | ~big_p(sk4) | big_r(sk4,sk5), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp122, plain, (spl3 | spl5 | spl19 | spl21), inference(avatar_split_clause, [status(thm)], [c122, sdef3, sdef5, sdef19, sdef21])).
% 25.34/13.92  cnf(c123, plain, ~big_p(sk2) | big_r(sk2,sk3) | ~big_p(X2) | ~big_r(sk4,X3) | ~big_r(X3,X2), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp123, plain, (spl6 | spl19 | spl21), inference(avatar_split_clause, [status(thm)], [c123, sdef6, sdef19, sdef21])).
% 25.34/13.92  cnf(c124, plain, ~big_p(sk2) | big_r(sk2,sk3) | ~big_p(a) | big_p(X4) | big_p(sk6(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp124, plain, (spl0 | spl7 | spl19 | spl21), inference(avatar_split_clause, [status(thm)], [c124, sdef0, sdef7, sdef19, sdef21])).
% 25.34/13.92  cnf(c125, plain, ~big_p(sk2) | big_r(sk2,sk3) | ~big_p(a) | big_p(X4) | big_r(X4,sk7(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp125, plain, (spl0 | spl8 | spl19 | spl21), inference(avatar_split_clause, [status(thm)], [c125, sdef0, sdef8, sdef19, sdef21])).
% 25.34/13.92  cnf(c126, plain, ~big_p(sk2) | big_r(sk2,sk3) | ~big_p(a) | big_p(X4) | big_r(sk7(X4),sk6(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp126, plain, (spl0 | spl9 | spl19 | spl21), inference(avatar_split_clause, [status(thm)], [c126, sdef0, sdef9, sdef19, sdef21])).
% 25.34/13.92  cnf(c127, plain, ~big_p(sk2) | big_r(sk2,sk3) | ~big_p(a) | ~big_p(X7) | ~big_r(X4,X7) | big_p(sk8(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp127, plain, (spl0 | spl10 | spl19 | spl21), inference(avatar_split_clause, [status(thm)], [c127, sdef0, sdef10, sdef19, sdef21])).
% 25.34/13.92  cnf(c128, plain, ~big_p(sk2) | big_r(sk2,sk3) | ~big_p(a) | ~big_p(X7) | ~big_r(X4,X7) | big_r(X4,sk9(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp128, plain, (spl0 | spl11 | spl19 | spl21), inference(avatar_split_clause, [status(thm)], [c128, sdef0, sdef11, sdef19, sdef21])).
% 25.34/13.92  cnf(c129, plain, ~big_p(sk2) | big_r(sk2,sk3) | ~big_p(a) | ~big_p(X7) | ~big_r(X4,X7) | big_r(sk9(X4),sk8(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp129, plain, (spl0 | spl12 | spl19 | spl21), inference(avatar_split_clause, [status(thm)], [c129, sdef0, sdef12, sdef19, sdef21])).
% 25.34/13.92  cnf(c130, plain, ~big_p(sk2) | ~big_p(X8) | ~big_r(sk2,X9) | ~big_r(X9,X8) | big_p(a), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp130, plain, (spl2 | spl20 | spl21), inference(avatar_split_clause, [status(thm)], [c130, sdef2, sdef20, sdef21])).
% 25.34/13.92  cnf(c131, plain, ~big_p(sk2) | ~big_p(X8) | ~big_r(sk2,X9) | ~big_r(X9,X8) | ~big_p(sk4) | big_p(sk5), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp131, plain, (spl3 | spl4 | spl20 | spl21), inference(avatar_split_clause, [status(thm)], [c131, sdef3, sdef4, sdef20, sdef21])).
% 25.34/13.92  cnf(c132, plain, ~big_p(sk2) | ~big_p(X8) | ~big_r(sk2,X9) | ~big_r(X9,X8) | ~big_p(sk4) | big_r(sk4,sk5), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp132, plain, (spl3 | spl5 | spl20 | spl21), inference(avatar_split_clause, [status(thm)], [c132, sdef3, sdef5, sdef20, sdef21])).
% 25.34/13.92  cnf(c133, plain, ~big_p(sk2) | ~big_p(X8) | ~big_r(sk2,X9) | ~big_r(X9,X8) | ~big_p(X2) | ~big_r(sk4,X3) | ~big_r(X3,X2), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp133, plain, (spl6 | spl20 | spl21), inference(avatar_split_clause, [status(thm)], [c133, sdef6, sdef20, sdef21])).
% 25.34/13.92  cnf(c134, plain, ~big_p(sk2) | ~big_p(X8) | ~big_r(sk2,X9) | ~big_r(X9,X8) | ~big_p(a) | big_p(X4) | big_p(sk6(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp134, plain, (spl0 | spl7 | spl20 | spl21), inference(avatar_split_clause, [status(thm)], [c134, sdef0, sdef7, sdef20, sdef21])).
% 25.34/13.92  cnf(c135, plain, ~big_p(sk2) | ~big_p(X8) | ~big_r(sk2,X9) | ~big_r(X9,X8) | ~big_p(a) | big_p(X4) | big_r(X4,sk7(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp135, plain, (spl0 | spl8 | spl20 | spl21), inference(avatar_split_clause, [status(thm)], [c135, sdef0, sdef8, sdef20, sdef21])).
% 25.34/13.92  cnf(c136, plain, ~big_p(sk2) | ~big_p(X8) | ~big_r(sk2,X9) | ~big_r(X9,X8) | ~big_p(a) | big_p(X4) | big_r(sk7(X4),sk6(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp136, plain, (spl0 | spl9 | spl20 | spl21), inference(avatar_split_clause, [status(thm)], [c136, sdef0, sdef9, sdef20, sdef21])).
% 25.34/13.92  cnf(c137, plain, ~big_p(sk2) | ~big_p(X8) | ~big_r(sk2,X9) | ~big_r(X9,X8) | ~big_p(a) | ~big_p(X7) | ~big_r(X4,X7) | big_p(sk8(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp137, plain, (spl0 | spl10 | spl20 | spl21), inference(avatar_split_clause, [status(thm)], [c137, sdef0, sdef10, sdef20, sdef21])).
% 25.34/13.92  cnf(c138, plain, ~big_p(sk2) | ~big_p(X8) | ~big_r(sk2,X9) | ~big_r(X9,X8) | ~big_p(a) | ~big_p(X7) | ~big_r(X4,X7) | big_r(X4,sk9(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp138, plain, (spl0 | spl11 | spl20 | spl21), inference(avatar_split_clause, [status(thm)], [c138, sdef0, sdef11, sdef20, sdef21])).
% 25.34/13.92  cnf(c139, plain, ~big_p(sk2) | ~big_p(X8) | ~big_r(sk2,X9) | ~big_r(X9,X8) | ~big_p(a) | ~big_p(X7) | ~big_r(X4,X7) | big_r(sk9(X4),sk8(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp139, plain, (spl0 | spl12 | spl20 | spl21), inference(avatar_split_clause, [status(thm)], [c139, sdef0, sdef12, sdef20, sdef21])).
% 25.34/13.92  cnf(c150, plain, ~big_p(X5) | ~big_r(sk2,X6) | ~big_r(X6,X5) | big_p(sk3) | big_p(a), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp140, plain, (spl2 | spl18 | spl20), inference(avatar_split_clause, [status(thm)], [c150, sdef2, sdef18, sdef20])).
% 25.34/13.92  cnf(c151, plain, ~big_p(X5) | ~big_r(sk2,X6) | ~big_r(X6,X5) | big_p(sk3) | ~big_p(sk4) | big_p(sk5), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp141, plain, (spl3 | spl4 | spl18 | spl20), inference(avatar_split_clause, [status(thm)], [c151, sdef3, sdef4, sdef18, sdef20])).
% 25.34/13.92  cnf(c152, plain, ~big_p(X5) | ~big_r(sk2,X6) | ~big_r(X6,X5) | big_p(sk3) | ~big_p(sk4) | big_r(sk4,sk5), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp142, plain, (spl3 | spl5 | spl18 | spl20), inference(avatar_split_clause, [status(thm)], [c152, sdef3, sdef5, sdef18, sdef20])).
% 25.34/13.92  cnf(c153, plain, ~big_p(X5) | ~big_r(sk2,X6) | ~big_r(X6,X5) | big_p(sk3) | ~big_p(X2) | ~big_r(sk4,X3) | ~big_r(X3,X2), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp143, plain, (spl6 | spl18 | spl20), inference(avatar_split_clause, [status(thm)], [c153, sdef6, sdef18, sdef20])).
% 25.34/13.92  cnf(c154, plain, ~big_p(X5) | ~big_r(sk2,X6) | ~big_r(X6,X5) | big_p(sk3) | ~big_p(a) | big_p(X4) | big_p(sk6(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp144, plain, (spl0 | spl7 | spl18 | spl20), inference(avatar_split_clause, [status(thm)], [c154, sdef0, sdef7, sdef18, sdef20])).
% 25.34/13.92  cnf(c155, plain, ~big_p(X5) | ~big_r(sk2,X6) | ~big_r(X6,X5) | big_p(sk3) | ~big_p(a) | big_p(X4) | big_r(X4,sk7(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp145, plain, (spl0 | spl8 | spl18 | spl20), inference(avatar_split_clause, [status(thm)], [c155, sdef0, sdef8, sdef18, sdef20])).
% 25.34/13.92  cnf(c156, plain, ~big_p(X5) | ~big_r(sk2,X6) | ~big_r(X6,X5) | big_p(sk3) | ~big_p(a) | big_p(X4) | big_r(sk7(X4),sk6(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp146, plain, (spl0 | spl9 | spl18 | spl20), inference(avatar_split_clause, [status(thm)], [c156, sdef0, sdef9, sdef18, sdef20])).
% 25.34/13.92  cnf(c157, plain, ~big_p(X5) | ~big_r(sk2,X6) | ~big_r(X6,X5) | big_p(sk3) | ~big_p(a) | ~big_p(X7) | ~big_r(X4,X7) | big_p(sk8(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp147, plain, (spl0 | spl10 | spl18 | spl20), inference(avatar_split_clause, [status(thm)], [c157, sdef0, sdef10, sdef18, sdef20])).
% 25.34/13.92  cnf(c158, plain, ~big_p(X5) | ~big_r(sk2,X6) | ~big_r(X6,X5) | big_p(sk3) | ~big_p(a) | ~big_p(X7) | ~big_r(X4,X7) | big_r(X4,sk9(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp148, plain, (spl0 | spl11 | spl18 | spl20), inference(avatar_split_clause, [status(thm)], [c158, sdef0, sdef11, sdef18, sdef20])).
% 25.34/13.92  cnf(c159, plain, ~big_p(X5) | ~big_r(sk2,X6) | ~big_r(X6,X5) | big_p(sk3) | ~big_p(a) | ~big_p(X7) | ~big_r(X4,X7) | big_r(sk9(X4),sk8(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp149, plain, (spl0 | spl12 | spl18 | spl20), inference(avatar_split_clause, [status(thm)], [c159, sdef0, sdef12, sdef18, sdef20])).
% 25.34/13.92  cnf(c160, plain, ~big_p(X5) | ~big_r(sk2,X6) | ~big_r(X6,X5) | big_r(sk2,sk3) | big_p(a), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp150, plain, (spl2 | spl19 | spl20), inference(avatar_split_clause, [status(thm)], [c160, sdef2, sdef19, sdef20])).
% 25.34/13.92  cnf(c161, plain, ~big_p(X5) | ~big_r(sk2,X6) | ~big_r(X6,X5) | big_r(sk2,sk3) | ~big_p(sk4) | big_p(sk5), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp151, plain, (spl3 | spl4 | spl19 | spl20), inference(avatar_split_clause, [status(thm)], [c161, sdef3, sdef4, sdef19, sdef20])).
% 25.34/13.92  cnf(c162, plain, ~big_p(X5) | ~big_r(sk2,X6) | ~big_r(X6,X5) | big_r(sk2,sk3) | ~big_p(sk4) | big_r(sk4,sk5), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp152, plain, (spl3 | spl5 | spl19 | spl20), inference(avatar_split_clause, [status(thm)], [c162, sdef3, sdef5, sdef19, sdef20])).
% 25.34/13.92  cnf(c163, plain, ~big_p(X5) | ~big_r(sk2,X6) | ~big_r(X6,X5) | big_r(sk2,sk3) | ~big_p(X2) | ~big_r(sk4,X3) | ~big_r(X3,X2), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp153, plain, (spl6 | spl19 | spl20), inference(avatar_split_clause, [status(thm)], [c163, sdef6, sdef19, sdef20])).
% 25.34/13.92  cnf(c164, plain, ~big_p(X5) | ~big_r(sk2,X6) | ~big_r(X6,X5) | big_r(sk2,sk3) | ~big_p(a) | big_p(X4) | big_p(sk6(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp154, plain, (spl0 | spl7 | spl19 | spl20), inference(avatar_split_clause, [status(thm)], [c164, sdef0, sdef7, sdef19, sdef20])).
% 25.34/13.92  cnf(c165, plain, ~big_p(X5) | ~big_r(sk2,X6) | ~big_r(X6,X5) | big_r(sk2,sk3) | ~big_p(a) | big_p(X4) | big_r(X4,sk7(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp155, plain, (spl0 | spl8 | spl19 | spl20), inference(avatar_split_clause, [status(thm)], [c165, sdef0, sdef8, sdef19, sdef20])).
% 25.34/13.92  cnf(c166, plain, ~big_p(X5) | ~big_r(sk2,X6) | ~big_r(X6,X5) | big_r(sk2,sk3) | ~big_p(a) | big_p(X4) | big_r(sk7(X4),sk6(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp156, plain, (spl0 | spl9 | spl19 | spl20), inference(avatar_split_clause, [status(thm)], [c166, sdef0, sdef9, sdef19, sdef20])).
% 25.34/13.92  cnf(c167, plain, ~big_p(X5) | ~big_r(sk2,X6) | ~big_r(X6,X5) | big_r(sk2,sk3) | ~big_p(a) | ~big_p(X7) | ~big_r(X4,X7) | big_p(sk8(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp157, plain, (spl0 | spl10 | spl19 | spl20), inference(avatar_split_clause, [status(thm)], [c167, sdef0, sdef10, sdef19, sdef20])).
% 25.34/13.92  cnf(c168, plain, ~big_p(X5) | ~big_r(sk2,X6) | ~big_r(X6,X5) | big_r(sk2,sk3) | ~big_p(a) | ~big_p(X7) | ~big_r(X4,X7) | big_r(X4,sk9(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp158, plain, (spl0 | spl11 | spl19 | spl20), inference(avatar_split_clause, [status(thm)], [c168, sdef0, sdef11, sdef19, sdef20])).
% 25.34/13.92  cnf(c169, plain, ~big_p(X5) | ~big_r(sk2,X6) | ~big_r(X6,X5) | big_r(sk2,sk3) | ~big_p(a) | ~big_p(X7) | ~big_r(X4,X7) | big_r(sk9(X4),sk8(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp159, plain, (spl0 | spl12 | spl19 | spl20), inference(avatar_split_clause, [status(thm)], [c169, sdef0, sdef12, sdef19, sdef20])).
% 25.34/13.92  cnf(c171, plain, ~big_p(X5) | ~big_r(sk2,X6) | ~big_r(X6,X5) | ~big_p(X8) | ~big_r(sk2,X9) | ~big_r(X9,X8) | ~big_p(sk4) | big_p(sk5), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp160, plain, (spl3 | spl4 | spl20), inference(avatar_split_clause, [status(thm)], [c171, sdef3, sdef4, sdef20])).
% 25.34/13.92  cnf(c172, plain, ~big_p(X5) | ~big_r(sk2,X6) | ~big_r(X6,X5) | ~big_p(X8) | ~big_r(sk2,X9) | ~big_r(X9,X8) | ~big_p(sk4) | big_r(sk4,sk5), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp161, plain, (spl3 | spl5 | spl20), inference(avatar_split_clause, [status(thm)], [c172, sdef3, sdef5, sdef20])).
% 25.34/13.92  cnf(c173, plain, ~big_p(X5) | ~big_r(sk2,X6) | ~big_r(X6,X5) | ~big_p(X8) | ~big_r(sk2,X9) | ~big_r(X9,X8) | ~big_p(X2) | ~big_r(sk4,X3) | ~big_r(X3,X2), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp162, plain, (spl6 | spl20), inference(avatar_split_clause, [status(thm)], [c173, sdef6, sdef20])).
% 25.34/13.92  cnf(c174, plain, ~big_p(X5) | ~big_r(sk2,X6) | ~big_r(X6,X5) | ~big_p(X8) | ~big_r(sk2,X9) | ~big_r(X9,X8) | ~big_p(a) | big_p(X4) | big_p(sk6(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp163, plain, (spl0 | spl7 | spl20), inference(avatar_split_clause, [status(thm)], [c174, sdef0, sdef7, sdef20])).
% 25.34/13.92  cnf(c175, plain, ~big_p(X5) | ~big_r(sk2,X6) | ~big_r(X6,X5) | ~big_p(X8) | ~big_r(sk2,X9) | ~big_r(X9,X8) | ~big_p(a) | big_p(X4) | big_r(X4,sk7(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp164, plain, (spl0 | spl8 | spl20), inference(avatar_split_clause, [status(thm)], [c175, sdef0, sdef8, sdef20])).
% 25.34/13.92  cnf(c176, plain, ~big_p(X5) | ~big_r(sk2,X6) | ~big_r(X6,X5) | ~big_p(X8) | ~big_r(sk2,X9) | ~big_r(X9,X8) | ~big_p(a) | big_p(X4) | big_r(sk7(X4),sk6(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp165, plain, (spl0 | spl9 | spl20), inference(avatar_split_clause, [status(thm)], [c176, sdef0, sdef9, sdef20])).
% 25.34/13.92  cnf(c177, plain, ~big_p(X5) | ~big_r(sk2,X6) | ~big_r(X6,X5) | ~big_p(X8) | ~big_r(sk2,X9) | ~big_r(X9,X8) | ~big_p(a) | ~big_p(X7) | ~big_r(X4,X7) | big_p(sk8(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp166, plain, (spl0 | spl10 | spl20), inference(avatar_split_clause, [status(thm)], [c177, sdef0, sdef10, sdef20])).
% 25.34/13.92  cnf(c178, plain, ~big_p(X5) | ~big_r(sk2,X6) | ~big_r(X6,X5) | ~big_p(X8) | ~big_r(sk2,X9) | ~big_r(X9,X8) | ~big_p(a) | ~big_p(X7) | ~big_r(X4,X7) | big_r(X4,sk9(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp167, plain, (spl0 | spl11 | spl20), inference(avatar_split_clause, [status(thm)], [c178, sdef0, sdef11, sdef20])).
% 25.34/13.92  cnf(c179, plain, ~big_p(X5) | ~big_r(sk2,X6) | ~big_r(X6,X5) | ~big_p(X8) | ~big_r(sk2,X9) | ~big_r(X9,X8) | ~big_p(a) | ~big_p(X7) | ~big_r(X4,X7) | big_r(sk9(X4),sk8(X4)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.34/13.92  cnf(ssp168, plain, (spl0 | spl12 | spl20), inference(avatar_split_clause, [status(thm)], [c179, sdef0, sdef12, sdef20])).
% 25.34/13.92  cnf(p192, plain, (~big_p(sk4) | ~big_r(sk4,sk4) | ~spl6), inference(factoring, [status(thm)], [p10])).
% 25.34/13.92  fof(sdef22, definition, (spl22 <=> (~big_r(sk4,sk4))), introduced(definition, [new_symbols(naming, [spl22])], [avatar_definition])).
% 25.34/13.92  cnf(ssp169, plain, (~spl6 | spl3 | spl22), inference(avatar_split_clause, [status(thm)], [p192, sdef3, sdef22])).
% 25.34/13.92  cnf(p194, plain, (~big_r(sk4,X0) | ~big_r(X0,a) | ~spl2 | ~spl6), inference(resolution, [status(thm)], [p10, p3])).
% 25.34/13.92  cnf(p14, plain, (big_p(X0) | big_r(X0,sk7(X0)) | ~spl8), inference(avatar_component_clause, [status(thm)], [sdef8])).
% 25.34/13.92  cnf(p200, plain, (~big_r(sk7(sk4),a) | big_p(sk4) | ~spl2 | ~spl6 | ~spl8), inference(resolution, [status(thm)], [p194, p14])).
% 25.34/13.92  fof(sdef23, definition, (spl23 <=> (~big_r(sk7(sk4),a))), introduced(definition, [new_symbols(naming, [spl23])], [avatar_definition])).
% 25.34/13.92  cnf(ssp170, plain, (~spl2 | ~spl6 | ~spl8 | spl23 | spl24), inference(avatar_split_clause, [status(thm)], [p200, sdef23, sdef24])).
% 25.34/13.92  cnf(p24, plain, (big_p(X0) | big_r(X0,sk1(X0)) | ~spl13), inference(avatar_component_clause, [status(thm)], [sdef13])).
% 25.34/13.92  cnf(p203, plain, (~big_r(sk1(sk4),a) | big_p(sk4) | ~spl2 | ~spl6 | ~spl13), inference(resolution, [status(thm)], [p194, p24])).
% 25.34/13.92  fof(sdef25, definition, (spl25 <=> (~big_r(sk1(sk4),a))), introduced(definition, [new_symbols(naming, [spl25])], [avatar_definition])).
% 25.34/13.92  cnf(ssp171, plain, (~spl2 | ~spl6 | ~spl13 | spl24 | spl25), inference(avatar_split_clause, [status(thm)], [p203, sdef24, sdef25])).
% 25.34/13.92  cnf(p195, plain, (~big_r(sk4,X0) | ~big_r(X0,sk5) | ~spl4 | ~spl6), inference(resolution, [status(thm)], [p10, p6])).
% 25.34/13.92  cnf(p212, plain, (~big_r(sk7(sk4),sk5) | big_p(sk4) | ~spl4 | ~spl6 | ~spl8), inference(resolution, [status(thm)], [p195, p14])).
% 25.34/13.92  fof(sdef26, definition, (spl26 <=> (~big_r(sk7(sk4),sk5))), introduced(definition, [new_symbols(naming, [spl26])], [avatar_definition])).
% 25.34/13.92  cnf(ssp172, plain, (~spl4 | ~spl6 | ~spl8 | spl24 | spl26), inference(avatar_split_clause, [status(thm)], [p212, sdef24, sdef26])).
% 25.34/13.92  cnf(p197, plain, (~big_r(sk4,X0) | ~big_r(X0,sk3) | ~spl6 | ~spl18), inference(resolution, [status(thm)], [p10, p89])).
% 25.34/13.92  cnf(p220, plain, (~big_r(sk7(sk4),sk3) | big_p(sk4) | ~spl6 | ~spl8 | ~spl18), inference(resolution, [status(thm)], [p197, p14])).
% 25.34/13.92  fof(sdef27, definition, (spl27 <=> (~big_r(sk7(sk4),sk3))), introduced(definition, [new_symbols(naming, [spl27])], [avatar_definition])).
% 25.34/13.92  cnf(ssp173, plain, (~spl6 | ~spl8 | ~spl18 | spl24 | spl27), inference(avatar_split_clause, [status(thm)], [p220, sdef24, sdef27])).
% 25.34/13.92  cnf(p280, plain, (~big_r(sk7(sk4),sk8(sk4)) | big_p(sk4) | ~spl4 | ~spl5 | ~spl6 | ~spl8 | ~spl10), inference(resolution, [status(thm)], [p228, p14])).
% 25.34/13.92  fof(sdef28, definition, (spl28 <=> (~big_r(sk7(sk4),sk8(sk4)))), introduced(definition, [new_symbols(naming, [spl28])], [avatar_definition])).
% 25.34/13.92  cnf(ssp174, plain, (~spl4 | ~spl5 | ~spl6 | ~spl8 | ~spl10 | spl24 | spl28), inference(avatar_split_clause, [status(thm)], [p280, sdef24, sdef28])).
% 25.34/13.92  cnf(p283, plain, (~big_p(sk2) | ~big_r(sk2,sk2) | ~spl20), inference(factoring, [status(thm)], [p111])).
% 25.34/13.92  fof(sdef29, definition, (spl29 <=> (~big_r(sk2,sk2))), introduced(definition, [new_symbols(naming, [spl29])], [avatar_definition])).
% 25.34/13.92  cnf(ssp175, plain, (~spl20 | spl21 | spl29), inference(avatar_split_clause, [status(thm)], [p283, sdef21, sdef29])).
% 25.34/13.92  cnf(p285, plain, (~big_r(sk2,X0) | ~big_r(X0,a) | ~spl2 | ~spl20), inference(resolution, [status(thm)], [p111, p3])).
% 25.34/13.92  cnf(p295, plain, (~big_r(sk7(sk2),a) | big_p(sk2) | ~spl2 | ~spl8 | ~spl20), inference(resolution, [status(thm)], [p285, p14])).
% 25.34/13.92  fof(sdef30, definition, (spl30 <=> (~big_r(sk7(sk2),a))), introduced(definition, [new_symbols(naming, [spl30])], [avatar_definition])).
% 25.34/13.92  cnf(ssp176, plain, (~spl2 | ~spl8 | ~spl20 | spl30 | spl31), inference(avatar_split_clause, [status(thm)], [p295, sdef30, sdef31])).
% 25.34/13.92  cnf(p2, plain, (big_p(X0) | big_p(sk0(X0)) | ~spl1), inference(avatar_component_clause, [status(thm)], [sdef1])).
% 25.34/13.92  cnf(p196, plain, (~big_r(sk4,X0) | ~big_r(X0,sk0(X1)) | big_p(X1) | ~spl1 | ~spl6), inference(resolution, [status(thm)], [p10, p2])).
% 25.34/13.92  cnf(p308, plain, (~big_r(sk7(sk4),sk0(X0)) | big_p(X0) | big_p(sk4) | ~spl1 | ~spl6 | ~spl8), inference(resolution, [status(thm)], [p196, p14])).
% 25.34/13.92  fof(sdef32, definition, (spl32 <=> (~big_r(sk7(sk4),sk0(X0)) | big_p(X0))), introduced(definition, [new_symbols(naming, [spl32])], [avatar_definition])).
% 25.34/13.92  cnf(ssp177, plain, (~spl1 | ~spl6 | ~spl8 | spl24 | spl32), inference(avatar_split_clause, [status(thm)], [p308, sdef24, sdef32])).
% 25.34/13.92  cnf(p300, plain, (~big_r(sk4,X0) | ~big_r(X0,sk2) | ~spl6 | ~spl31), inference(resolution, [status(thm)], [p297, p10])).
% 25.34/13.92  cnf(p311, plain, (~big_r(sk7(sk4),sk2) | big_p(sk4) | ~spl6 | ~spl8 | ~spl31), inference(resolution, [status(thm)], [p300, p14])).
% 25.34/13.92  fof(sdef33, definition, (spl33 <=> (~big_r(sk7(sk4),sk2))), introduced(definition, [new_symbols(naming, [spl33])], [avatar_definition])).
% 25.34/13.92  cnf(ssp178, plain, (~spl6 | ~spl8 | ~spl31 | spl24 | spl33), inference(avatar_split_clause, [status(thm)], [p311, sdef24, sdef33])).
% 25.34/13.92  cnf(p12, plain, (big_p(X0) | big_p(sk6(X0)) | ~spl7), inference(avatar_component_clause, [status(thm)], [sdef7])).
% 25.34/13.92  cnf(p198, plain, (big_p(X0) | ~big_r(sk4,X1) | ~big_r(X1,sk6(X0)) | ~spl6 | ~spl7), inference(resolution, [status(thm)], [p12, p10])).
% 25.34/13.92  cnf(p314, plain, (big_p(X0) | ~big_r(sk7(sk4),sk6(X0)) | big_p(sk4) | ~spl6 | ~spl7 | ~spl8), inference(resolution, [status(thm)], [p198, p14])).
% 25.34/13.92  fof(sdef34, definition, (spl34 <=> (big_p(X0) | ~big_r(sk7(sk4),sk6(X0)))), introduced(definition, [new_symbols(naming, [spl34])], [avatar_definition])).
% 25.34/13.92  cnf(ssp179, plain, (~spl6 | ~spl7 | ~spl8 | spl24 | spl34), inference(avatar_split_clause, [status(thm)], [p314, sdef24, sdef34])).
% 25.34/13.92  cnf(p315, plain, (big_p(X0) | ~big_r(sk7(sk4),sk6(X0)) | ~spl34), inference(avatar_component_clause, [status(thm)], [sdef34])).
% 25.34/13.92  cnf(p16, plain, (big_p(X0) | big_r(sk7(X0),sk6(X0)) | ~spl9), inference(avatar_component_clause, [status(thm)], [sdef9])).
% 25.34/13.92  cnf(p320, plain, (big_p(sk4) | big_p(sk4) | ~spl9 | ~spl34), inference(resolution, [status(thm)], [p315, p16])).
% 25.34/13.92  cnf(ssp180, plain, (~spl9 | ~spl34 | spl24), inference(avatar_split_clause, [status(thm)], [p320, sdef24])).
% 25.34/13.92  cnf(p332, plain, (big_p(sk4) | ~big_r(sk1(sk4),sk5) | ~spl4 | ~spl6 | ~spl13), inference(resolution, [status(thm)], [p24, p195])).
% 25.34/13.92  fof(sdef35, definition, (spl35 <=> (~big_r(sk1(sk4),sk5))), introduced(definition, [new_symbols(naming, [spl35])], [avatar_definition])).
% 25.34/13.92  cnf(ssp181, plain, (~spl4 | ~spl6 | ~spl13 | spl24 | spl35), inference(avatar_split_clause, [status(thm)], [p332, sdef24, sdef35])).
% 25.34/13.92  cnf(p334, plain, (big_p(sk4) | ~big_r(sk1(sk4),sk3) | ~spl6 | ~spl13 | ~spl18), inference(resolution, [status(thm)], [p24, p197])).
% 25.34/13.92  fof(sdef36, definition, (spl36 <=> (~big_r(sk1(sk4),sk3))), introduced(definition, [new_symbols(naming, [spl36])], [avatar_definition])).
% 25.34/13.92  cnf(ssp182, plain, (~spl6 | ~spl13 | ~spl18 | spl24 | spl36), inference(avatar_split_clause, [status(thm)], [p334, sdef24, sdef36])).
% 25.34/13.92  cnf(p336, plain, (big_p(sk4) | ~big_r(sk1(sk4),sk8(sk4)) | ~spl4 | ~spl5 | ~spl6 | ~spl10 | ~spl13), inference(resolution, [status(thm)], [p24, p228])).
% 25.34/13.92  fof(sdef37, definition, (spl37 <=> (~big_r(sk1(sk4),sk8(sk4)))), introduced(definition, [new_symbols(naming, [spl37])], [avatar_definition])).
% 25.34/13.92  cnf(ssp183, plain, (~spl4 | ~spl5 | ~spl6 | ~spl10 | ~spl13 | spl24 | spl37), inference(avatar_split_clause, [status(thm)], [p336, sdef24, sdef37])).
% 25.34/13.92  cnf(p338, plain, (big_p(sk4) | ~big_r(sk1(sk4),sk0(X0)) | big_p(X0) | ~spl1 | ~spl6 | ~spl13), inference(resolution, [status(thm)], [p24, p196])).
% 25.34/13.92  fof(sdef38, definition, (spl38 <=> (~big_r(sk1(sk4),sk0(X0)) | big_p(X0))), introduced(definition, [new_symbols(naming, [spl38])], [avatar_definition])).
% 25.34/13.92  cnf(ssp184, plain, (~spl1 | ~spl6 | ~spl13 | spl24 | spl38), inference(avatar_split_clause, [status(thm)], [p338, sdef24, sdef38])).
% 25.34/13.92  cnf(p340, plain, (big_p(sk4) | ~big_r(sk1(sk4),sk2) | ~spl6 | ~spl13 | ~spl31), inference(resolution, [status(thm)], [p24, p300])).
% 25.34/13.92  fof(sdef39, definition, (spl39 <=> (~big_r(sk1(sk4),sk2))), introduced(definition, [new_symbols(naming, [spl39])], [avatar_definition])).
% 25.34/13.92  cnf(ssp185, plain, (~spl6 | ~spl13 | ~spl31 | spl24 | spl39), inference(avatar_split_clause, [status(thm)], [p340, sdef24, sdef39])).
% 25.34/13.92  cnf(p342, plain, (big_p(sk4) | big_p(X0) | ~big_r(sk1(sk4),sk6(X0)) | ~spl6 | ~spl7 | ~spl13), inference(resolution, [status(thm)], [p24, p198])).
% 25.34/13.92  fof(sdef40, definition, (spl40 <=> (big_p(X0) | ~big_r(sk1(sk4),sk6(X0)))), introduced(definition, [new_symbols(naming, [spl40])], [avatar_definition])).
% 25.34/13.92  cnf(ssp186, plain, (~spl6 | ~spl7 | ~spl13 | spl24 | spl40), inference(avatar_split_clause, [status(thm)], [p342, sdef24, sdef40])).
% 25.34/13.92  cnf(p351, plain, (~big_r(sk1(sk2),a) | big_p(sk2) | ~spl2 | ~spl13 | ~spl20), inference(resolution, [status(thm)], [p285, p24])).
% 25.34/13.92  fof(sdef41, definition, (spl41 <=> (~big_r(sk1(sk2),a))), introduced(definition, [new_symbols(naming, [spl41])], [avatar_definition])).
% 25.34/13.92  cnf(ssp187, plain, (~spl2 | ~spl13 | ~spl20 | spl31 | spl41), inference(avatar_split_clause, [status(thm)], [p351, sdef31, sdef41])).
% 25.34/13.92  cnf(p286, plain, (~big_r(sk2,X0) | ~big_r(X0,sk5) | ~spl4 | ~spl20), inference(resolution, [status(thm)], [p111, p6])).
% 25.34/13.92  cnf(p354, plain, (~big_r(sk7(sk2),sk5) | big_p(sk2) | ~spl4 | ~spl8 | ~spl20), inference(resolution, [status(thm)], [p286, p14])).
% 25.34/13.92  fof(sdef42, definition, (spl42 <=> (~big_r(sk7(sk2),sk5))), introduced(definition, [new_symbols(naming, [spl42])], [avatar_definition])).
% 25.34/13.92  cnf(ssp188, plain, (~spl4 | ~spl8 | ~spl20 | spl31 | spl42), inference(avatar_split_clause, [status(thm)], [p354, sdef31, sdef42])).
% 25.34/13.92  cnf(p356, plain, (~big_r(sk1(sk2),sk5) | big_p(sk2) | ~spl4 | ~spl13 | ~spl20), inference(resolution, [status(thm)], [p286, p24])).
% 25.34/13.92  fof(sdef43, definition, (spl43 <=> (~big_r(sk1(sk2),sk5))), introduced(definition, [new_symbols(naming, [spl43])], [avatar_definition])).
% 25.34/13.92  cnf(ssp189, plain, (~spl4 | ~spl13 | ~spl20 | spl31 | spl43), inference(avatar_split_clause, [status(thm)], [p356, sdef31, sdef43])).
% 25.34/13.92  cnf(p288, plain, (~big_r(sk2,X0) | ~big_r(X0,sk3) | ~spl18 | ~spl20), inference(resolution, [status(thm)], [p111, p89])).
% 25.34/13.92  cnf(p362, plain, (~big_r(sk7(sk2),sk3) | big_p(sk2) | ~spl8 | ~spl18 | ~spl20), inference(resolution, [status(thm)], [p288, p14])).
% 25.34/13.92  fof(sdef44, definition, (spl44 <=> (~big_r(sk7(sk2),sk3))), introduced(definition, [new_symbols(naming, [spl44])], [avatar_definition])).
% 25.34/13.92  cnf(ssp190, plain, (~spl8 | ~spl18 | ~spl20 | spl31 | spl44), inference(avatar_split_clause, [status(thm)], [p362, sdef31, sdef44])).
% 25.34/13.92  cnf(p364, plain, (~big_r(sk1(sk2),sk3) | big_p(sk2) | ~spl13 | ~spl18 | ~spl20), inference(resolution, [status(thm)], [p288, p24])).
% 25.34/13.92  fof(sdef45, definition, (spl45 <=> (~big_r(sk1(sk2),sk3))), introduced(definition, [new_symbols(naming, [spl45])], [avatar_definition])).
% 25.34/13.92  cnf(ssp191, plain, (~spl13 | ~spl18 | ~spl20 | spl31 | spl45), inference(avatar_split_clause, [status(thm)], [p364, sdef31, sdef45])).
% 25.34/13.92  cnf(p233, plain, (~big_r(sk4,X0) | ~big_r(X0,sk8(sk2)) | ~spl6 | ~spl10 | ~spl18 | ~spl19), inference(resolution, [status(thm)], [p232, p10])).
% 25.34/13.92  cnf(p367, plain, (~big_r(sk7(sk4),sk8(sk2)) | big_p(sk4) | ~spl6 | ~spl8 | ~spl10 | ~spl18 | ~spl19), inference(resolution, [status(thm)], [p233, p14])).
% 25.34/13.92  fof(sdef46, definition, (spl46 <=> (~big_r(sk7(sk4),sk8(sk2)))), introduced(definition, [new_symbols(naming, [spl46])], [avatar_definition])).
% 25.34/13.92  cnf(ssp192, plain, (~spl6 | ~spl8 | ~spl10 | ~spl18 | ~spl19 | spl24 | spl46), inference(avatar_split_clause, [status(thm)], [p367, sdef24, sdef46])).
% 25.34/13.92  cnf(p369, plain, (~big_r(sk1(sk4),sk8(sk2)) | big_p(sk4) | ~spl6 | ~spl10 | ~spl13 | ~spl18 | ~spl19), inference(resolution, [status(thm)], [p233, p24])).
% 25.34/13.92  fof(sdef47, definition, (spl47 <=> (~big_r(sk1(sk4),sk8(sk2)))), introduced(definition, [new_symbols(naming, [spl47])], [avatar_definition])).
% 25.34/13.92  cnf(ssp193, plain, (~spl6 | ~spl10 | ~spl13 | ~spl18 | ~spl19 | spl24 | spl47), inference(avatar_split_clause, [status(thm)], [p369, sdef24, sdef47])).
% 25.34/13.92  cnf(p263, plain, (~big_r(sk4,X0) | ~big_r(X0,sk0(sk2)) | ~spl6 | ~spl15 | ~spl18 | ~spl19), inference(resolution, [status(thm)], [p262, p10])).
% 25.34/13.92  cnf(p397, plain, (~big_r(sk7(sk4),sk0(sk2)) | big_p(sk4) | ~spl6 | ~spl8 | ~spl15 | ~spl18 | ~spl19), inference(resolution, [status(thm)], [p263, p14])).
% 25.34/13.92  fof(sdef48, definition, (spl48 <=> (~big_r(sk7(sk4),sk0(sk2)))), introduced(definition, [new_symbols(naming, [spl48])], [avatar_definition])).
% 25.34/13.92  cnf(ssp194, plain, (~spl6 | ~spl8 | ~spl15 | ~spl18 | ~spl19 | spl24 | spl48), inference(avatar_split_clause, [status(thm)], [p397, sdef24, sdef48])).
% 25.34/13.92  cnf(p399, plain, (~big_r(sk1(sk4),sk0(sk2)) | big_p(sk4) | ~spl6 | ~spl13 | ~spl15 | ~spl18 | ~spl19), inference(resolution, [status(thm)], [p263, p24])).
% 25.34/13.92  fof(sdef49, definition, (spl49 <=> (~big_r(sk1(sk4),sk0(sk2)))), introduced(definition, [new_symbols(naming, [spl49])], [avatar_definition])).
% 25.34/13.92  cnf(ssp195, plain, (~spl6 | ~spl13 | ~spl15 | ~spl18 | ~spl19 | spl24 | spl49), inference(avatar_split_clause, [status(thm)], [p399, sdef24, sdef49])).
% 25.34/13.92  cnf(p264, plain, (~big_r(X0,sk0(sk2)) | big_p(sk8(X0)) | ~spl10 | ~spl15 | ~spl18 | ~spl19), inference(resolution, [status(thm)], [p262, p18])).
% 25.34/13.92  cnf(p35, plain, (big_p(X0) | big_r(sk1(X0),sk0(X0)) | ~spl14), inference(avatar_component_clause, [status(thm)], [sdef14])).
% 25.34/13.92  cnf(p403, plain, (big_p(sk8(sk1(sk2))) | big_p(sk2) | ~spl10 | ~spl14 | ~spl15 | ~spl18 | ~spl19), inference(resolution, [status(thm)], [p264, p35])).
% 25.34/13.92  fof(sdef50, definition, (spl50 <=> (big_p(sk8(sk1(sk2))))), introduced(definition, [new_symbols(naming, [spl50])], [avatar_definition])).
% 25.34/13.92  cnf(ssp196, plain, (~spl10 | ~spl14 | ~spl15 | ~spl18 | ~spl19 | spl31 | spl50), inference(avatar_split_clause, [status(thm)], [p403, sdef31, sdef50])).
% 25.34/13.92  cnf(p267, plain, (~big_r(X0,sk0(sk2)) | big_p(sk0(X0)) | ~spl15 | ~spl18 | ~spl19), inference(resolution, [status(thm)], [p262, p46])).
% 25.34/13.92  cnf(p414, plain, (big_p(sk0(sk1(sk2))) | big_p(sk2) | ~spl14 | ~spl15 | ~spl18 | ~spl19), inference(resolution, [status(thm)], [p267, p35])).
% 25.34/13.92  fof(sdef51, definition, (spl51 <=> (big_p(sk0(sk1(sk2))))), introduced(definition, [new_symbols(naming, [spl51])], [avatar_definition])).
% 25.34/13.92  cnf(ssp197, plain, (~spl14 | ~spl15 | ~spl18 | ~spl19 | spl31 | spl51), inference(avatar_split_clause, [status(thm)], [p414, sdef31, sdef51])).
% 25.34/13.92  cnf(p425, plain, (~big_r(sk7(sk2),sk8(sk2)) | big_p(sk2) | ~spl8 | ~spl10 | ~spl18 | ~spl19 | ~spl20), inference(resolution, [status(thm)], [p291, p14])).
% 25.34/13.92  fof(sdef52, definition, (spl52 <=> (~big_r(sk7(sk2),sk8(sk2)))), introduced(definition, [new_symbols(naming, [spl52])], [avatar_definition])).
% 25.34/13.92  cnf(ssp198, plain, (~spl8 | ~spl10 | ~spl18 | ~spl19 | ~spl20 | spl31 | spl52), inference(avatar_split_clause, [status(thm)], [p425, sdef31, sdef52])).
% 25.34/13.92  cnf(p427, plain, (~big_r(sk1(sk2),sk8(sk2)) | big_p(sk2) | ~spl10 | ~spl13 | ~spl18 | ~spl19 | ~spl20), inference(resolution, [status(thm)], [p291, p24])).
% 25.34/13.92  fof(sdef53, definition, (spl53 <=> (~big_r(sk1(sk2),sk8(sk2)))), introduced(definition, [new_symbols(naming, [spl53])], [avatar_definition])).
% 25.34/13.92  cnf(ssp199, plain, (~spl10 | ~spl13 | ~spl18 | ~spl19 | ~spl20 | spl31 | spl53), inference(avatar_split_clause, [status(thm)], [p427, sdef31, sdef53])).
% 25.34/13.92  cnf(p339, plain, (~big_r(sk1(sk4),sk0(X0)) | big_p(X0) | ~spl38), inference(avatar_component_clause, [status(thm)], [sdef38])).
% 25.34/13.92  cnf(p433, plain, (big_p(sk4) | big_p(sk4) | ~spl14 | ~spl38), inference(resolution, [status(thm)], [p339, p35])).
% 25.34/13.92  cnf(ssp200, plain, (~spl14 | ~spl38 | spl24), inference(avatar_split_clause, [status(thm)], [p433, sdef24])).
% 25.34/13.92  cnf(p404, plain, (big_p(sk8(sk1(sk2))) | ~spl50), inference(avatar_component_clause, [status(thm)], [sdef50])).
% 25.34/13.92  cnf(p405, plain, (~big_r(sk4,X0) | ~big_r(X0,sk8(sk1(sk2))) | ~spl6 | ~spl50), inference(resolution, [status(thm)], [p404, p10])).
% 25.34/13.92  cnf(p436, plain, (~big_r(sk7(sk4),sk8(sk1(sk2))) | big_p(sk4) | ~spl6 | ~spl8 | ~spl50), inference(resolution, [status(thm)], [p405, p14])).
% 25.34/13.92  fof(sdef54, definition, (spl54 <=> (~big_r(sk7(sk4),sk8(sk1(sk2))))), introduced(definition, [new_symbols(naming, [spl54])], [avatar_definition])).
% 25.34/13.92  cnf(ssp201, plain, (~spl6 | ~spl8 | ~spl50 | spl24 | spl54), inference(avatar_split_clause, [status(thm)], [p436, sdef24, sdef54])).
% 25.34/13.92  cnf(p438, plain, (~big_r(sk1(sk4),sk8(sk1(sk2))) | big_p(sk4) | ~spl6 | ~spl13 | ~spl50), inference(resolution, [status(thm)], [p405, p24])).
% 25.34/13.92  fof(sdef55, definition, (spl55 <=> (~big_r(sk1(sk4),sk8(sk1(sk2))))), introduced(definition, [new_symbols(naming, [spl55])], [avatar_definition])).
% 25.34/13.92  cnf(ssp202, plain, (~spl6 | ~spl13 | ~spl50 | spl24 | spl55), inference(avatar_split_clause, [status(thm)], [p438, sdef24, sdef55])).
% 25.34/13.92  cnf(p287, plain, (~big_r(sk2,X0) | ~big_r(X0,sk0(X1)) | big_p(X1) | ~spl1 | ~spl20), inference(resolution, [status(thm)], [p111, p2])).
% 25.34/13.92  cnf(p440, plain, (~big_r(sk7(sk2),sk0(X0)) | big_p(X0) | big_p(sk2) | ~spl1 | ~spl8 | ~spl20), inference(resolution, [status(thm)], [p287, p14])).
% 25.34/13.92  fof(sdef56, definition, (spl56 <=> (~big_r(sk7(sk2),sk0(X0)) | big_p(X0))), introduced(definition, [new_symbols(naming, [spl56])], [avatar_definition])).
% 25.34/13.92  cnf(ssp203, plain, (~spl1 | ~spl8 | ~spl20 | spl31 | spl56), inference(avatar_split_clause, [status(thm)], [p440, sdef31, sdef56])).
% 25.34/13.92  cnf(p442, plain, (~big_r(sk1(sk2),sk0(X0)) | big_p(X0) | big_p(sk2) | ~spl1 | ~spl13 | ~spl20), inference(resolution, [status(thm)], [p287, p24])).
% 25.34/13.92  fof(sdef57, definition, (spl57 <=> (~big_r(sk1(sk2),sk0(X0)) | big_p(X0))), introduced(definition, [new_symbols(naming, [spl57])], [avatar_definition])).
% 25.34/13.92  cnf(ssp204, plain, (~spl1 | ~spl13 | ~spl20 | spl31 | spl57), inference(avatar_split_clause, [status(thm)], [p442, sdef31, sdef57])).
% 25.34/13.92  cnf(p443, plain, (~big_r(sk1(sk2),sk0(X0)) | big_p(X0) | ~spl57), inference(avatar_component_clause, [status(thm)], [sdef57])).
% 25.34/13.92  cnf(p444, plain, (big_p(sk2) | big_p(sk2) | ~spl14 | ~spl57), inference(resolution, [status(thm)], [p443, p35])).
% 25.34/13.92  cnf(ssp205, plain, (~spl14 | ~spl57 | spl31), inference(avatar_split_clause, [status(thm)], [p444, sdef31])).
% 25.34/13.92  cnf(p289, plain, (~big_r(sk2,X0) | ~big_r(X0,sk6(X1)) | big_p(X1) | ~spl7 | ~spl20), inference(resolution, [status(thm)], [p111, p12])).
% 25.34/13.92  cnf(p446, plain, (~big_r(sk7(sk2),sk6(X0)) | big_p(X0) | big_p(sk2) | ~spl7 | ~spl8 | ~spl20), inference(resolution, [status(thm)], [p289, p14])).
% 25.34/13.92  fof(sdef58, definition, (spl58 <=> (~big_r(sk7(sk2),sk6(X0)) | big_p(X0))), introduced(definition, [new_symbols(naming, [spl58])], [avatar_definition])).
% 25.34/13.92  cnf(ssp206, plain, (~spl7 | ~spl8 | ~spl20 | spl31 | spl58), inference(avatar_split_clause, [status(thm)], [p446, sdef31, sdef58])).
% 25.34/13.92  cnf(p448, plain, (~big_r(sk1(sk2),sk6(X0)) | big_p(X0) | big_p(sk2) | ~spl7 | ~spl13 | ~spl20), inference(resolution, [status(thm)], [p289, p24])).
% 25.34/13.92  fof(sdef59, definition, (spl59 <=> (~big_r(sk1(sk2),sk6(X0)) | big_p(X0))), introduced(definition, [new_symbols(naming, [spl59])], [avatar_definition])).
% 25.34/13.92  cnf(ssp207, plain, (~spl7 | ~spl13 | ~spl20 | spl31 | spl59), inference(avatar_split_clause, [status(thm)], [p448, sdef31, sdef59])).
% 25.34/13.92  cnf(p290, plain, (~big_r(sk2,X0) | ~big_r(X0,sk8(sk4)) | ~spl4 | ~spl5 | ~spl10 | ~spl20), inference(resolution, [status(thm)], [p111, p227])).
% 25.34/13.92  cnf(p461, plain, (~big_r(sk7(sk2),sk8(sk4)) | big_p(sk2) | ~spl4 | ~spl5 | ~spl8 | ~spl10 | ~spl20), inference(resolution, [status(thm)], [p290, p14])).
% 25.34/13.92  fof(sdef60, definition, (spl60 <=> (~big_r(sk7(sk2),sk8(sk4)))), introduced(definition, [new_symbols(naming, [spl60])], [avatar_definition])).
% 25.34/13.92  cnf(ssp208, plain, (~spl4 | ~spl5 | ~spl8 | ~spl10 | ~spl20 | spl31 | spl60), inference(avatar_split_clause, [status(thm)], [p461, sdef31, sdef60])).
% 25.34/13.92  cnf(p463, plain, (~big_r(sk1(sk2),sk8(sk4)) | big_p(sk2) | ~spl4 | ~spl5 | ~spl10 | ~spl13 | ~spl20), inference(resolution, [status(thm)], [p290, p24])).
% 25.34/13.92  fof(sdef61, definition, (spl61 <=> (~big_r(sk1(sk2),sk8(sk4)))), introduced(definition, [new_symbols(naming, [spl61])], [avatar_definition])).
% 25.34/13.92  cnf(ssp209, plain, (~spl4 | ~spl5 | ~spl10 | ~spl13 | ~spl20 | spl31 | spl61), inference(avatar_split_clause, [status(thm)], [p463, sdef31, sdef61])).
% 25.34/13.92  cnf(p242, plain, (~big_r(X0,sk5) | big_p(sk0(X0)) | ~spl4 | ~spl15), inference(resolution, [status(thm)], [p46, p6])).
% 25.34/13.92  cnf(p248, plain, (big_p(sk0(sk4)) | ~spl4 | ~spl5 | ~spl15), inference(resolution, [status(thm)], [p242, p8])).
% 25.34/13.92  cnf(p292, plain, (~big_r(sk2,X0) | ~big_r(X0,sk0(sk4)) | ~spl4 | ~spl5 | ~spl15 | ~spl20), inference(resolution, [status(thm)], [p111, p248])).
% 25.34/13.92  cnf(p468, plain, (~big_r(sk7(sk2),sk0(sk4)) | big_p(sk2) | ~spl4 | ~spl5 | ~spl8 | ~spl15 | ~spl20), inference(resolution, [status(thm)], [p292, p14])).
% 25.34/13.92  fof(sdef62, definition, (spl62 <=> (~big_r(sk7(sk2),sk0(sk4)))), introduced(definition, [new_symbols(naming, [spl62])], [avatar_definition])).
% 25.34/13.92  cnf(ssp210, plain, (~spl4 | ~spl5 | ~spl8 | ~spl15 | ~spl20 | spl31 | spl62), inference(avatar_split_clause, [status(thm)], [p468, sdef31, sdef62])).
% 25.34/13.92  cnf(p470, plain, (~big_r(sk1(sk2),sk0(sk4)) | big_p(sk2) | ~spl4 | ~spl5 | ~spl13 | ~spl15 | ~spl20), inference(resolution, [status(thm)], [p292, p24])).
% 25.34/13.92  fof(sdef63, definition, (spl63 <=> (~big_r(sk1(sk2),sk0(sk4)))), introduced(definition, [new_symbols(naming, [spl63])], [avatar_definition])).
% 25.34/13.92  cnf(ssp211, plain, (~spl4 | ~spl5 | ~spl13 | ~spl15 | ~spl20 | spl31 | spl63), inference(avatar_split_clause, [status(thm)], [p470, sdef31, sdef63])).
% 25.34/13.92  cnf(p478, plain, (~big_r(sk7(sk2),sk0(sk2)) | big_p(sk2) | ~spl8 | ~spl15 | ~spl18 | ~spl19 | ~spl20), inference(resolution, [status(thm)], [p293, p14])).
% 25.34/13.92  fof(sdef64, definition, (spl64 <=> (~big_r(sk7(sk2),sk0(sk2)))), introduced(definition, [new_symbols(naming, [spl64])], [avatar_definition])).
% 25.34/13.92  cnf(ssp212, plain, (~spl8 | ~spl15 | ~spl18 | ~spl19 | ~spl20 | spl31 | spl64), inference(avatar_split_clause, [status(thm)], [p478, sdef31, sdef64])).
% 25.34/13.92  cnf(p480, plain, (~big_r(sk1(sk2),sk0(sk2)) | big_p(sk2) | ~spl13 | ~spl15 | ~spl18 | ~spl19 | ~spl20), inference(resolution, [status(thm)], [p293, p24])).
% 25.34/13.92  cnf(ssp213, plain, (~spl13 | ~spl15 | ~spl18 | ~spl19 | ~spl20 | spl31 | spl65), inference(avatar_split_clause, [status(thm)], [p480, sdef31, sdef65])).
% 25.34/13.92  cnf(p271, plain, (~big_r(X0,sk5) | big_r(sk1(X0),sk0(X0)) | ~spl4 | ~spl17), inference(resolution, [status(thm)], [p68, p6])).
% 25.34/13.92  cnf(p456, plain, (big_r(sk1(sk4),sk0(sk4)) | ~spl4 | ~spl5 | ~spl17), inference(resolution, [status(thm)], [p8, p271])).
% 25.34/13.92  cnf(p208, plain, (~big_r(X0,sk0(X1)) | big_p(sk8(X0)) | big_p(X1) | ~spl1 | ~spl10), inference(resolution, [status(thm)], [p18, p2])).
% 25.34/13.92  cnf(p497, plain, (big_p(sk8(sk1(sk4))) | big_p(sk4) | ~spl1 | ~spl4 | ~spl5 | ~spl10 | ~spl17), inference(resolution, [status(thm)], [p456, p208])).
% 25.34/13.92  fof(sdef66, definition, (spl66 <=> (big_p(sk8(sk1(sk4))))), introduced(definition, [new_symbols(naming, [spl66])], [avatar_definition])).
% 25.34/13.92  cnf(ssp214, plain, (~spl1 | ~spl4 | ~spl5 | ~spl10 | ~spl17 | spl24 | spl66), inference(avatar_split_clause, [status(thm)], [p497, sdef24, sdef66])).
% 25.34/13.92  cnf(p216, plain, (~big_r(X0,sk0(X1)) | big_r(X0,sk9(X0)) | big_p(X1) | ~spl1 | ~spl11), inference(resolution, [status(thm)], [p20, p2])).
% 25.34/13.92  cnf(p499, plain, (big_r(sk1(sk4),sk9(sk1(sk4))) | big_p(sk4) | ~spl1 | ~spl4 | ~spl5 | ~spl11 | ~spl17), inference(resolution, [status(thm)], [p456, p216])).
% 25.34/13.92  fof(sdef67, definition, (spl67 <=> (big_r(sk1(sk4),sk9(sk1(sk4))))), introduced(definition, [new_symbols(naming, [spl67])], [avatar_definition])).
% 25.34/13.92  cnf(ssp215, plain, (~spl1 | ~spl4 | ~spl5 | ~spl11 | ~spl17 | spl24 | spl67), inference(avatar_split_clause, [status(thm)], [p499, sdef24, sdef67])).
% 25.34/13.92  cnf(p243, plain, (~big_r(X0,sk0(X1)) | big_p(sk0(X0)) | big_p(X1) | ~spl1 | ~spl15), inference(resolution, [status(thm)], [p46, p2])).
% 25.34/13.92  cnf(p501, plain, (big_p(sk0(sk1(sk4))) | big_p(sk4) | ~spl1 | ~spl4 | ~spl5 | ~spl15 | ~spl17), inference(resolution, [status(thm)], [p456, p243])).
% 25.34/13.92  fof(sdef68, definition, (spl68 <=> (big_p(sk0(sk1(sk4))))), introduced(definition, [new_symbols(naming, [spl68])], [avatar_definition])).
% 25.34/13.92  cnf(ssp216, plain, (~spl1 | ~spl4 | ~spl5 | ~spl15 | ~spl17 | spl24 | spl68), inference(avatar_split_clause, [status(thm)], [p501, sdef24, sdef68])).
% 25.34/13.92  cnf(p251, plain, (~big_r(X0,sk0(X1)) | big_r(X0,sk1(X0)) | big_p(X1) | ~spl1 | ~spl16), inference(resolution, [status(thm)], [p57, p2])).
% 25.34/13.92  cnf(p503, plain, (big_r(sk1(sk4),sk1(sk1(sk4))) | big_p(sk4) | ~spl1 | ~spl4 | ~spl5 | ~spl16 | ~spl17), inference(resolution, [status(thm)], [p456, p251])).
% 25.34/13.92  fof(sdef69, definition, (spl69 <=> (big_r(sk1(sk4),sk1(sk1(sk4))))), introduced(definition, [new_symbols(naming, [spl69])], [avatar_definition])).
% 25.34/13.92  cnf(ssp217, plain, (~spl1 | ~spl4 | ~spl5 | ~spl16 | ~spl17 | spl24 | spl69), inference(avatar_split_clause, [status(thm)], [p503, sdef24, sdef69])).
% 25.34/13.92  cnf(p272, plain, (~big_r(X0,sk0(X1)) | big_r(sk1(X0),sk0(X0)) | big_p(X1) | ~spl1 | ~spl17), inference(resolution, [status(thm)], [p68, p2])).
% 25.34/13.92  cnf(p506, plain, (big_r(sk1(sk1(sk4)),sk0(sk1(sk4))) | big_p(sk4) | ~spl1 | ~spl4 | ~spl5 | ~spl17), inference(resolution, [status(thm)], [p456, p272])).
% 25.34/13.92  fof(sdef70, definition, (spl70 <=> (big_r(sk1(sk1(sk4)),sk0(sk1(sk4))))), introduced(definition, [new_symbols(naming, [spl70])], [avatar_definition])).
% 25.34/13.92  cnf(ssp218, plain, (~spl1 | ~spl4 | ~spl5 | ~spl17 | spl24 | spl70), inference(avatar_split_clause, [status(thm)], [p506, sdef24, sdef70])).
% 25.34/13.92  cnf(p529, plain, (big_p(sk8(sk1(sk2))) | big_p(sk2) | ~spl1 | ~spl10 | ~spl17 | ~spl18 | ~spl19), inference(resolution, [status(thm)], [p458, p208])).
% 25.34/13.92  cnf(ssp219, plain, (~spl1 | ~spl10 | ~spl17 | ~spl18 | ~spl19 | spl31 | spl50), inference(avatar_split_clause, [status(thm)], [p529, sdef31, sdef50])).
% 25.34/13.92  cnf(p530, plain, (big_r(sk1(sk2),sk9(sk1(sk2))) | big_p(sk2) | ~spl1 | ~spl11 | ~spl17 | ~spl18 | ~spl19), inference(resolution, [status(thm)], [p458, p216])).
% 25.34/13.92  fof(sdef71, definition, (spl71 <=> (big_r(sk1(sk2),sk9(sk1(sk2))))), introduced(definition, [new_symbols(naming, [spl71])], [avatar_definition])).
% 25.34/13.92  cnf(ssp220, plain, (~spl1 | ~spl11 | ~spl17 | ~spl18 | ~spl19 | spl31 | spl71), inference(avatar_split_clause, [status(thm)], [p530, sdef31, sdef71])).
% 25.34/13.92  cnf(p532, plain, (big_p(sk0(sk1(sk2))) | big_p(sk2) | ~spl1 | ~spl15 | ~spl17 | ~spl18 | ~spl19), inference(resolution, [status(thm)], [p458, p243])).
% 25.34/13.92  cnf(ssp221, plain, (~spl1 | ~spl15 | ~spl17 | ~spl18 | ~spl19 | spl31 | spl51), inference(avatar_split_clause, [status(thm)], [p532, sdef31, sdef51])).
% 25.34/13.92  cnf(p534, plain, (big_r(sk1(sk2),sk1(sk1(sk2))) | big_p(sk2) | ~spl1 | ~spl16 | ~spl17 | ~spl18 | ~spl19), inference(resolution, [status(thm)], [p458, p251])).
% 25.34/13.92  fof(sdef72, definition, (spl72 <=> (big_r(sk1(sk2),sk1(sk1(sk2))))), introduced(definition, [new_symbols(naming, [spl72])], [avatar_definition])).
% 25.34/13.92  cnf(ssp222, plain, (~spl1 | ~spl16 | ~spl17 | ~spl18 | ~spl19 | spl31 | spl72), inference(avatar_split_clause, [status(thm)], [p534, sdef31, sdef72])).
% 25.34/13.92  cnf(p537, plain, (big_r(sk1(sk1(sk2)),sk0(sk1(sk2))) | big_p(sk2) | ~spl1 | ~spl17 | ~spl18 | ~spl19), inference(resolution, [status(thm)], [p458, p272])).
% 25.34/13.92  fof(sdef73, definition, (spl73 <=> (big_r(sk1(sk1(sk2)),sk0(sk1(sk2))))), introduced(definition, [new_symbols(naming, [spl73])], [avatar_definition])).
% 25.34/13.92  cnf(ssp223, plain, (~spl1 | ~spl17 | ~spl18 | ~spl19 | spl31 | spl73), inference(avatar_split_clause, [status(thm)], [p537, sdef31, sdef73])).
% 25.34/13.92  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, ssp149, ssp150, ssp151, ssp152, ssp153, ssp154, ssp155, ssp156, ssp157, ssp158, ssp159, ssp160, ssp161, ssp162, ssp163, ssp164, ssp165, ssp166, ssp167, ssp168, ssp169, ssp170, ssp171, ssp172, ssp173, ssp174, ssp175, ssp176, ssp177, ssp178, ssp179, ssp180, ssp181, ssp182, ssp183, ssp184, ssp185, ssp186, ssp187, ssp188, ssp189, ssp190, ssp191, ssp192, ssp193, ssp194, ssp195, ssp196, ssp197, ssp198, ssp199, ssp200, ssp201, ssp202, ssp203, ssp204, ssp205, ssp206, ssp207, ssp208, ssp209, ssp210, ssp211, ssp212, ssp213, ssp214, ssp215, ssp216, ssp217, ssp218, ssp219, ssp220, ssp221, ssp222, ssp223, sct0, sct1, sct2, sct3, sct4, sct5, sct6])).
% 25.34/13.92  % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------