%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : KRS145+1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n008.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 01:53:19 PM UTC 2026
% Result : Theorem 23.51s 13.48s
% Output : Proof 23.51s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : KRS145+1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.10/10.39 % Computer : n008.cluster.edu
% 0.10/10.39 % Model : x86_64 x86_64
% 0.10/10.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/10.39 % Memory : 8046.5625MB
% 0.10/10.39 % OS : Linux 6.8.0-71-generic
% 0.10/10.39 % CPULimit : 300
% 0.10/10.39 % WCLimit : 300
% 0.10/10.39 % DateTime : Wed Sep 23 19:31:52 UTC 2026
% 0.10/10.39 % CPUTime :
% 0.10/10.39 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 23.51/13.48 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 23.51/13.48 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 23.51/13.48 fof(sdef3, definition, (spl3 <=> (~xsd_string(sk3))), introduced(definition, [new_symbols(naming, [spl3])], [avatar_definition])).
% 23.51/13.48 cnf(p19, plain, (~xsd_string(sk3) | ~spl3), inference(avatar_component_clause, [status(thm)], [sdef3])).
% 23.51/13.48 fof(sdef2, definition, (spl2 <=> (xsd_string(sk3))), introduced(definition, [new_symbols(naming, [spl2])], [avatar_definition])).
% 23.51/13.48 cnf(p18, plain, (xsd_string(sk3) | ~spl2), inference(avatar_component_clause, [status(thm)], [sdef2])).
% 23.51/13.48 cnf(p57, plain, ($false | ~spl2 | ~spl3), inference(resolution, [status(thm)], [p19, p18])).
% 23.51/13.48 cnf(sct0, plain, (~spl2 | ~spl3), inference(avatar_contradiction_clause, [status(thm)], [p57])).
% 23.51/13.48 fof(sdef13, definition, (spl13 <=> (xsd_integer(sk3))), introduced(definition, [new_symbols(naming, [spl13])], [avatar_definition])).
% 23.51/13.48 cnf(p43, plain, (xsd_integer(sk3) | ~spl13), inference(avatar_component_clause, [status(thm)], [sdef13])).
% 23.51/13.48 fof(sdef12, definition, (spl12 <=> (~xsd_integer(sk3))), introduced(definition, [new_symbols(naming, [spl12])], [avatar_definition])).
% 23.51/13.48 cnf(p35, plain, (~xsd_integer(sk3) | ~spl12), inference(avatar_component_clause, [status(thm)], [sdef12])).
% 23.51/13.48 cnf(p58, plain, ($false | ~spl12 | ~spl13), inference(resolution, [status(thm)], [p43, p35])).
% 23.51/13.48 cnf(sct1, plain, (~spl12 | ~spl13), inference(avatar_contradiction_clause, [status(thm)], [p58])).
% 23.51/13.48 fof(sdef5, definition, (spl5 <=> (~rp(sk4,X0) | ~rp(sk4,X1) | X0 = X1)), introduced(definition, [new_symbols(naming, [spl5])], [avatar_definition])).
% 23.51/13.48 cnf(p22, plain, (~rp(sk4,X0) | ~rp(sk4,X1) | X0 = X1 | ~spl5), inference(avatar_component_clause, [status(thm)], [sdef5])).
% 23.51/13.48 fof(sdef6, definition, (spl6 <=> (rp(sk4,sk5))), introduced(definition, [new_symbols(naming, [spl6])], [avatar_definition])).
% 23.51/13.48 cnf(p23, plain, (rp(sk4,sk5) | ~spl6), inference(avatar_component_clause, [status(thm)], [sdef6])).
% 23.51/13.48 cnf(p59, plain, (~rp(sk4,X0) | sk5 = X0 | ~spl5 | ~spl6), inference(resolution, [status(thm)], [p22, p23])).
% 23.51/13.48 fof(sdef7, definition, (spl7 <=> (rp(sk4,sk6))), introduced(definition, [new_symbols(naming, [spl7])], [avatar_definition])).
% 23.51/13.48 cnf(p25, plain, (rp(sk4,sk6) | ~spl7), inference(avatar_component_clause, [status(thm)], [sdef7])).
% 23.51/13.48 cnf(p62, plain, (sk5 = sk6 | ~spl5 | ~spl6 | ~spl7), inference(resolution, [status(thm)], [p59, p25])).
% 23.51/13.48 fof(sdef9, definition, (spl9 <=> (sk5 != sk6)), introduced(definition, [new_symbols(naming, [spl9])], [avatar_definition])).
% 23.51/13.48 cnf(p29, plain, (sk5 != sk6 | ~spl9), inference(avatar_component_clause, [status(thm)], [sdef9])).
% 23.51/13.48 cnf(p67, plain, ($false | ~spl5 | ~spl6 | ~spl7 | ~spl9), inference(resolution, [status(thm)], [p62, p29])).
% 23.51/13.48 cnf(sct2, plain, (~spl5 | ~spl6 | ~spl7 | ~spl9), inference(avatar_contradiction_clause, [status(thm)], [p67])).
% 23.51/13.48 fof(f7, axiom, ! [X] : ( cowlThing(X) & ~ cowlNothing(X) ), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_0)).
% 23.51/13.48 fof(f7_nnf, plain, ! [X] : ((cowlThing(X) & ~(cowlNothing(X)))), inference(nnf_transformation, [status(thm)], [f7])).
% 23.51/13.48 fof(f7_sk, plain, ! [X] : ((cowlThing(X) & ~(cowlNothing(X)))), inference(skolemisation, [status(esa)], [f7_nnf])).
% 23.51/13.48 cnf(c7, plain, cowlThing(X0), inference(cnf_transformation, [status(esa)], [f7_sk])).
% 23.51/13.48 fof(sdef0, definition, (spl0 <=> (~cowlThing(sk2))), introduced(definition, [new_symbols(naming, [spl0])], [avatar_definition])).
% 23.51/13.48 cnf(p16, plain, (~cowlThing(sk2) | ~spl0), inference(avatar_component_clause, [status(thm)], [sdef0])).
% 23.51/13.48 cnf(p68, plain, ($false | ~spl0), inference(resolution, [status(thm)], [c7, p16])).
% 23.51/13.48 cnf(sct3, plain, (~spl0), inference(avatar_contradiction_clause, [status(thm)], [p68])).
% 23.51/13.48 cnf(c8, plain, ~cowlNothing(X0), inference(cnf_transformation, [status(esa)], [f7_sk])).
% 23.51/13.48 fof(sdef1, definition, (spl1 <=> (cowlNothing(sk2))), introduced(definition, [new_symbols(naming, [spl1])], [avatar_definition])).
% 23.51/13.48 cnf(p17, plain, (cowlNothing(sk2) | ~spl1), inference(avatar_component_clause, [status(thm)], [sdef1])).
% 23.51/13.48 cnf(p69, plain, ($false | ~spl1), inference(resolution, [status(thm)], [c8, p17])).
% 23.51/13.48 cnf(sct4, plain, (~spl1), inference(avatar_contradiction_clause, [status(thm)], [p69])).
% 23.51/13.48 cnf(p60, plain, (~rp(sk4,X0) | sk6 = X0 | ~spl5 | ~spl7), inference(resolution, [status(thm)], [p22, p25])).
% 23.51/13.48 fof(sdef8, definition, (spl8 <=> (rp(sk4,sk7))), introduced(definition, [new_symbols(naming, [spl8])], [avatar_definition])).
% 23.51/13.48 cnf(p27, plain, (rp(sk4,sk7) | ~spl8), inference(avatar_component_clause, [status(thm)], [sdef8])).
% 23.51/13.48 cnf(p70, plain, (sk6 = sk7 | ~spl5 | ~spl7 | ~spl8), inference(resolution, [status(thm)], [p60, p27])).
% 23.51/13.48 fof(sdef11, definition, (spl11 <=> (sk6 != sk7)), introduced(definition, [new_symbols(naming, [spl11])], [avatar_definition])).
% 23.51/13.48 cnf(p33, plain, (sk6 != sk7 | ~spl11), inference(avatar_component_clause, [status(thm)], [sdef11])).
% 23.51/13.48 cnf(p75, plain, ($false | ~spl5 | ~spl7 | ~spl8 | ~spl11), inference(resolution, [status(thm)], [p70, p33])).
% 23.51/13.48 cnf(sct5, plain, (~spl5 | ~spl7 | ~spl8 | ~spl11), inference(avatar_contradiction_clause, [status(thm)], [p75])).
% 23.51/13.48 fof(sdef16, definition, (spl16 <=> (~cc(sk6))), introduced(definition, [new_symbols(naming, [spl16])], [avatar_definition])).
% 23.51/13.48 cnf(p72, plain, (~cc(sk6) | ~spl16), inference(avatar_component_clause, [status(thm)], [sdef16])).
% 23.51/13.48 fof(sdef15, definition, (spl15 <=> (cc(sk6))), introduced(definition, [new_symbols(naming, [spl15])], [avatar_definition])).
% 23.51/13.48 cnf(p66, plain, (cc(sk6) | ~spl15), inference(avatar_component_clause, [status(thm)], [sdef15])).
% 23.51/13.48 cnf(p76, plain, ($false | ~spl15 | ~spl16), inference(resolution, [status(thm)], [p72, p66])).
% 23.51/13.48 cnf(sct6, plain, (~spl15 | ~spl16), inference(avatar_contradiction_clause, [status(thm)], [p76])).
% 23.51/13.48 fof(sdef18, definition, (spl18 <=> (~cc(sk7))), introduced(definition, [new_symbols(naming, [spl18])], [avatar_definition])).
% 23.51/13.48 cnf(p83, plain, (~cc(sk7) | ~spl18), inference(avatar_component_clause, [status(thm)], [sdef18])).
% 23.51/13.48 fof(sdef17, definition, (spl17 <=> (cc(sk7))), introduced(definition, [new_symbols(naming, [spl17])], [avatar_definition])).
% 23.51/13.48 cnf(p73, plain, (cc(sk7) | ~spl17), inference(avatar_component_clause, [status(thm)], [sdef17])).
% 23.51/13.48 cnf(p96, plain, ($false | ~spl17 | ~spl18), inference(resolution, [status(thm)], [p83, p73])).
% 23.51/13.48 cnf(sct7, plain, (~spl17 | ~spl18), inference(avatar_contradiction_clause, [status(thm)], [p96])).
% 23.51/13.48 fof(sdef22, definition, (spl22 <=> (~xsd_string(sk7))), introduced(definition, [new_symbols(naming, [spl22])], [avatar_definition])).
% 23.51/13.48 cnf(p91, plain, (~xsd_string(sk7) | ~spl22), inference(avatar_component_clause, [status(thm)], [sdef22])).
% 23.51/13.48 fof(f8, axiom, ! [X] : ( xsd_string(X) <=> ~ xsd_integer(X) ), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_1)).
% 23.51/13.48 fof(f8_nnf, plain, ! [X] : (((~(xsd_string(X)) | ~(xsd_integer(X))) & (xsd_string(X) | xsd_integer(X)))), inference(nnf_transformation, [status(thm)], [f8])).
% 23.51/13.48 fof(f8_sk, plain, ! [X] : (((~(xsd_string(X)) | ~(xsd_integer(X))) & (xsd_string(X) | xsd_integer(X)))), inference(skolemisation, [status(esa)], [f8_nnf])).
% 23.51/13.48 cnf(c10, plain, xsd_string(X0) | xsd_integer(X0), inference(cnf_transformation, [status(esa)], [f8_sk])).
% 23.51/13.48 cnf(p97, plain, (xsd_integer(sk7) | ~spl22), inference(resolution, [status(thm)], [p91, c10])).
% 23.51/13.48 fof(sdef20, definition, (spl20 <=> (~xsd_integer(sk7))), introduced(definition, [new_symbols(naming, [spl20])], [avatar_definition])).
% 23.51/13.48 cnf(p88, plain, (~xsd_integer(sk7) | ~spl20), inference(avatar_component_clause, [status(thm)], [sdef20])).
% 23.51/13.48 cnf(p98, plain, ($false | ~spl20 | ~spl22), inference(resolution, [status(thm)], [p97, p88])).
% 23.51/13.48 cnf(sct8, plain, (~spl20 | ~spl22), inference(avatar_contradiction_clause, [status(thm)], [p98])).
% 23.51/13.48 fof(sdef23, definition, (spl23 <=> (xsd_string(sk0(sk4)))), introduced(definition, [new_symbols(naming, [spl23])], [avatar_definition])).
% 23.51/13.48 cnf(p92, plain, (xsd_string(sk0(sk4)) | ~spl23), inference(avatar_component_clause, [status(thm)], [sdef23])).
% 23.51/13.48 cnf(c9, plain, ~xsd_string(X0) | ~xsd_integer(X0), inference(cnf_transformation, [status(esa)], [f8_sk])).
% 23.51/13.48 cnf(p103, plain, (~xsd_integer(sk0(sk4)) | ~spl23), inference(resolution, [status(thm)], [p92, c9])).
% 23.51/13.48 fof(sdef21, definition, (spl21 <=> (xsd_integer(sk0(sk4)))), introduced(definition, [new_symbols(naming, [spl21])], [avatar_definition])).
% 23.51/13.48 cnf(p89, plain, (xsd_integer(sk0(sk4)) | ~spl21), inference(avatar_component_clause, [status(thm)], [sdef21])).
% 23.51/13.48 cnf(p106, plain, ($false | ~spl21 | ~spl23), inference(resolution, [status(thm)], [p103, p89])).
% 23.51/13.48 cnf(sct9, plain, (~spl21 | ~spl23), inference(avatar_contradiction_clause, [status(thm)], [p106])).
% 23.51/13.48 fof(sdef27, definition, (spl27 <=> (~xsd_string(sk6))), introduced(definition, [new_symbols(naming, [spl27])], [avatar_definition])).
% 23.51/13.48 cnf(p117, plain, (~xsd_string(sk6) | ~spl27), inference(avatar_component_clause, [status(thm)], [sdef27])).
% 23.51/13.48 cnf(p120, plain, (xsd_integer(sk6) | ~spl27), inference(resolution, [status(thm)], [p117, c10])).
% 23.51/13.48 fof(sdef25, definition, (spl25 <=> (~xsd_integer(sk6))), introduced(definition, [new_symbols(naming, [spl25])], [avatar_definition])).
% 23.51/13.48 cnf(p114, plain, (~xsd_integer(sk6) | ~spl25), inference(avatar_component_clause, [status(thm)], [sdef25])).
% 23.51/13.48 cnf(p121, plain, ($false | ~spl25 | ~spl27), inference(resolution, [status(thm)], [p120, p114])).
% 23.51/13.48 cnf(sct10, plain, (~spl25 | ~spl27), inference(avatar_contradiction_clause, [status(thm)], [p121])).
% 23.51/13.48 fof(sdef28, definition, (spl28 <=> (xsd_string(sk1(sk4)))), introduced(definition, [new_symbols(naming, [spl28])], [avatar_definition])).
% 23.51/13.48 cnf(p118, plain, (xsd_string(sk1(sk4)) | ~spl28), inference(avatar_component_clause, [status(thm)], [sdef28])).
% 23.51/13.48 cnf(p128, plain, (~xsd_integer(sk1(sk4)) | ~spl28), inference(resolution, [status(thm)], [p118, c9])).
% 23.51/13.48 fof(sdef26, definition, (spl26 <=> (xsd_integer(sk1(sk4)))), introduced(definition, [new_symbols(naming, [spl26])], [avatar_definition])).
% 23.51/13.48 cnf(p115, plain, (xsd_integer(sk1(sk4)) | ~spl26), inference(avatar_component_clause, [status(thm)], [sdef26])).
% 23.51/13.48 cnf(p129, plain, ($false | ~spl26 | ~spl28), inference(resolution, [status(thm)], [p128, p115])).
% 23.51/13.48 cnf(sct11, plain, (~spl26 | ~spl28), inference(avatar_contradiction_clause, [status(thm)], [p129])).
% 23.51/13.48 fof(f9, axiom, ! [X] : ( cc(X) => ( ! [Y0,Y1,Y2] : ( ( rp(X,Y0) & rp(X,Y1) & rp(X,Y2) ) => ( Y0 = Y1 | Y0 = Y2 | Y1 = Y2 ) ) & ? [Y0,Y1] : ( rp(X,Y0) & rp(X,Y1) & Y0 != Y1 ) ) ), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_2)).
% 23.51/13.48 fof(f9_nnf, plain, ! [X] : ((~(cc(X)) | (! [Y0,Y1,Y2] : ((((~(rp(X,Y0)) | ~(rp(X,Y1))) | ~(rp(X,Y2))) | ((Y0 = Y1 | Y0 = Y2) | Y1 = Y2))) & ? [Y0,Y1] : (((rp(X,Y0) & rp(X,Y1)) & Y0 != Y1))))), inference(nnf_transformation, [status(thm)], [f9])).
% 23.51/13.48 fof(f9_sk, plain, ! [X,Y0,Y1,Y2] : ((~(cc(X)) | ((((~(rp(X,Y0)) | ~(rp(X,Y1))) | ~(rp(X,Y2))) | ((Y0 = Y1 | Y0 = Y2) | Y1 = Y2)) & ((rp(X,sk0(X)) & rp(X,sk1(X))) & sk0(X) != sk1(X))))), inference(skolemisation, [status(esa), new_symbols(skolem, [sk0,sk1])], [f9_nnf])).
% 23.51/13.48 cnf(c12, plain, ~cc(X0) | rp(X0,sk0(X0)), inference(cnf_transformation, [status(esa)], [f9_sk])).
% 23.51/13.48 fof(sdef4, definition, (spl4 <=> (cc(sk4))), introduced(definition, [new_symbols(naming, [spl4])], [avatar_definition])).
% 23.51/13.48 cnf(p20, plain, (cc(sk4) | ~spl4), inference(avatar_component_clause, [status(thm)], [sdef4])).
% 23.51/13.48 cnf(p78, plain, (rp(sk4,sk0(sk4)) | ~spl4), inference(resolution, [status(thm)], [c12, p20])).
% 23.51/13.48 cnf(p80, plain, (~rp(sk4,X0) | sk0(sk4) = X0 | ~spl4 | ~spl5), inference(resolution, [status(thm)], [p78, p22])).
% 23.51/13.48 cnf(c13, plain, ~cc(X0) | rp(X0,sk1(X0)), inference(cnf_transformation, [status(esa)], [f9_sk])).
% 23.51/13.48 cnf(p99, plain, (rp(sk4,sk1(sk4)) | ~spl4), inference(resolution, [status(thm)], [c13, p20])).
% 23.51/13.48 cnf(p127, plain, (sk0(sk4) = sk1(sk4) | ~spl4 | ~spl5), inference(resolution, [status(thm)], [p80, p99])).
% 23.51/13.48 cnf(c14, plain, ~cc(X0) | sk0(X0) != sk1(X0), inference(cnf_transformation, [status(esa)], [f9_sk])).
% 23.51/13.48 cnf(p104, plain, (sk0(sk4) != sk1(sk4) | ~spl4), inference(resolution, [status(thm)], [c14, p20])).
% 23.51/13.48 cnf(p150, plain, ($false | ~spl4 | ~spl5), inference(resolution, [status(thm)], [p127, p104])).
% 23.51/13.48 cnf(sct12, plain, (~spl4 | ~spl5), inference(avatar_contradiction_clause, [status(thm)], [p150])).
% 23.51/13.48 fof(sdef29, definition, (spl29 <=> (~cc(sk0(sk4)))), introduced(definition, [new_symbols(naming, [spl29])], [avatar_definition])).
% 23.51/13.48 cnf(p140, plain, (~cc(sk0(sk4)) | ~spl29), inference(avatar_component_clause, [status(thm)], [sdef29])).
% 23.51/13.48 fof(sdef19, definition, (spl19 <=> (cc(sk0(sk4)))), introduced(definition, [new_symbols(naming, [spl19])], [avatar_definition])).
% 23.51/13.48 cnf(p84, plain, (cc(sk0(sk4)) | ~spl19), inference(avatar_component_clause, [status(thm)], [sdef19])).
% 23.51/13.48 cnf(p156, plain, ($false | ~spl19 | ~spl29), inference(resolution, [status(thm)], [p140, p84])).
% 23.51/13.48 cnf(sct13, plain, (~spl19 | ~spl29), inference(avatar_contradiction_clause, [status(thm)], [p156])).
% 23.51/13.48 fof(sdef31, definition, (spl31 <=> (~xsd_string(sk0(sk4)))), introduced(definition, [new_symbols(naming, [spl31])], [avatar_definition])).
% 23.51/13.48 cnf(p146, plain, (~xsd_string(sk0(sk4)) | ~spl31), inference(avatar_component_clause, [status(thm)], [sdef31])).
% 23.51/13.48 cnf(p158, plain, ($false | ~spl23 | ~spl31), inference(resolution, [status(thm)], [p146, p92])).
% 23.51/13.48 cnf(sct14, plain, (~spl23 | ~spl31), inference(avatar_contradiction_clause, [status(thm)], [p158])).
% 23.51/13.48 cnf(p157, plain, (xsd_integer(sk0(sk4)) | ~spl31), inference(resolution, [status(thm)], [p146, c10])).
% 23.51/13.48 fof(sdef30, definition, (spl30 <=> (~xsd_integer(sk0(sk4)))), introduced(definition, [new_symbols(naming, [spl30])], [avatar_definition])).
% 23.51/13.48 cnf(p144, plain, (~xsd_integer(sk0(sk4)) | ~spl30), inference(avatar_component_clause, [status(thm)], [sdef30])).
% 23.51/13.48 cnf(p159, plain, ($false | ~spl30 | ~spl31), inference(resolution, [status(thm)], [p157, p144])).
% 23.51/13.48 cnf(sct15, plain, (~spl30 | ~spl31), inference(avatar_contradiction_clause, [status(thm)], [p159])).
% 23.51/13.48 fof(sdef33, definition, (spl33 <=> (sk5 = sk6)), introduced(definition, [new_symbols(naming, [spl33])], [avatar_definition])).
% 23.51/13.48 cnf(p165, plain, (sk5 = sk6 | ~spl33), inference(avatar_component_clause, [status(thm)], [sdef33])).
% 23.51/13.48 cnf(p177, plain, ($false | ~spl9 | ~spl33), inference(resolution, [status(thm)], [p165, p29])).
% 23.51/13.48 cnf(sct16, plain, (~spl9 | ~spl33), inference(avatar_contradiction_clause, [status(thm)], [p177])).
% 23.51/13.48 fof(sdef35, definition, (spl35 <=> (sk5 = sk7)), introduced(definition, [new_symbols(naming, [spl35])], [avatar_definition])).
% 23.51/13.48 cnf(p168, plain, (sk5 = sk7 | ~spl35), inference(avatar_component_clause, [status(thm)], [sdef35])).
% 23.51/13.48 fof(sdef10, definition, (spl10 <=> (sk5 != sk7)), introduced(definition, [new_symbols(naming, [spl10])], [avatar_definition])).
% 23.51/13.48 cnf(p31, plain, (sk5 != sk7 | ~spl10), inference(avatar_component_clause, [status(thm)], [sdef10])).
% 23.51/13.48 cnf(p180, plain, ($false | ~spl10 | ~spl35), inference(resolution, [status(thm)], [p168, p31])).
% 23.51/13.48 cnf(sct17, plain, (~spl10 | ~spl35), inference(avatar_contradiction_clause, [status(thm)], [p180])).
% 23.51/13.48 fof(sdef37, definition, (spl37 <=> (sk5 = sk0(sk4))), introduced(definition, [new_symbols(naming, [spl37])], [avatar_definition])).
% 23.51/13.48 cnf(p171, plain, (sk5 = sk0(sk4) | ~spl37), inference(avatar_component_clause, [status(thm)], [sdef37])).
% 23.51/13.48 cnf(p192, plain, (xsd_integer(sk5) | ~spl31 | ~spl37), inference(superposition, [status(thm)], [p171, p157])).
% 23.51/13.48 fof(sdef40, definition, (spl40 <=> (~xsd_integer(sk5))), introduced(definition, [new_symbols(naming, [spl40])], [avatar_definition])).
% 23.51/13.48 cnf(p185, plain, (~xsd_integer(sk5) | ~spl40), inference(avatar_component_clause, [status(thm)], [sdef40])).
% 23.51/13.48 cnf(p201, plain, ($false | ~spl31 | ~spl37 | ~spl40), inference(resolution, [status(thm)], [p192, p185])).
% 23.51/13.48 cnf(sct18, plain, (~spl31 | ~spl37 | ~spl40), inference(avatar_contradiction_clause, [status(thm)], [p201])).
% 23.51/13.48 fof(sdef41, definition, (spl41 <=> (~xsd_string(sk5))), introduced(definition, [new_symbols(naming, [spl41])], [avatar_definition])).
% 23.51/13.48 cnf(p187, plain, (~xsd_string(sk5) | ~spl41), inference(avatar_component_clause, [status(thm)], [sdef41])).
% 23.51/13.48 cnf(p194, plain, (xsd_integer(sk5) | ~spl41), inference(resolution, [status(thm)], [p187, c10])).
% 23.51/13.48 cnf(p202, plain, ($false | ~spl40 | ~spl41), inference(resolution, [status(thm)], [p194, p185])).
% 23.51/13.48 cnf(sct19, plain, (~spl40 | ~spl41), inference(avatar_contradiction_clause, [status(thm)], [p202])).
% 23.51/13.48 fof(sdef42, definition, (spl42 <=> (sk6 = sk7)), introduced(definition, [new_symbols(naming, [spl42])], [avatar_definition])).
% 23.51/13.48 cnf(p208, plain, (sk6 = sk7 | ~spl42), inference(avatar_component_clause, [status(thm)], [sdef42])).
% 23.51/13.48 cnf(p220, plain, ($false | ~spl11 | ~spl42), inference(resolution, [status(thm)], [p208, p33])).
% 23.51/13.48 cnf(sct20, plain, (~spl11 | ~spl42), inference(avatar_contradiction_clause, [status(thm)], [p220])).
% 23.51/13.48 cnf(p77, plain, (xsd_integer(sk3) | ~spl3), inference(resolution, [status(thm)], [c10, p19])).
% 23.51/13.48 cnf(p230, plain, ($false | ~spl3 | ~spl12), inference(resolution, [status(thm)], [p35, p77])).
% 23.51/13.48 cnf(sct21, plain, (~spl3 | ~spl12), inference(avatar_contradiction_clause, [status(thm)], [p230])).
% 23.51/13.48 fof(sdef46, definition, (spl46 <=> (xsd_string(sk7))), introduced(definition, [new_symbols(naming, [spl46])], [avatar_definition])).
% 23.51/13.48 cnf(p226, plain, (xsd_string(sk7) | ~spl46), inference(avatar_component_clause, [status(thm)], [sdef46])).
% 23.51/13.48 cnf(p242, plain, ($false | ~spl22 | ~spl46), inference(resolution, [status(thm)], [p226, p91])).
% 23.51/13.48 cnf(sct22, plain, (~spl22 | ~spl46), inference(avatar_contradiction_clause, [status(thm)], [p242])).
% 23.51/13.48 fof(sdef45, definition, (spl45 <=> (xsd_integer(sk7))), introduced(definition, [new_symbols(naming, [spl45])], [avatar_definition])).
% 23.51/13.48 cnf(p224, plain, (xsd_integer(sk7) | ~spl45), inference(avatar_component_clause, [status(thm)], [sdef45])).
% 23.51/13.48 cnf(p255, plain, ($false | ~spl20 | ~spl45), inference(resolution, [status(thm)], [p88, p224])).
% 23.51/13.48 cnf(sct23, plain, (~spl20 | ~spl45), inference(avatar_contradiction_clause, [status(thm)], [p255])).
% 23.51/13.48 cnf(p231, plain, (~xsd_integer(sk3) | ~spl2), inference(resolution, [status(thm)], [p18, c9])).
% 23.51/13.48 cnf(p256, plain, ($false | ~spl2 | ~spl13), inference(resolution, [status(thm)], [p231, p43])).
% 23.51/13.48 cnf(sct24, plain, (~spl2 | ~spl13), inference(avatar_contradiction_clause, [status(thm)], [p256])).
% 23.51/13.48 fof(f10, conjecture, ( ! [X] : ( cowlThing(X) & ~ cowlNothing(X) ) & ! [X] : ( xsd_string(X) <=> ~ xsd_integer(X) ) & ! [X] : ( cc(X) => ( ? [Y0,Y1] : ( rp(X,Y0) & rp(X,Y1) & Y0 != Y1 ) & ! [Y0,Y1,Y2] : ( ( rp(X,Y0) & rp(X,Y1) & rp(X,Y2) ) => ( Y0 = Y1 | Y0 = Y2 | Y1 = Y2 ) ) ) ) ), file('/export/starexec/sandbox/benchmark/theBenchmark.p', the_axiom)).
% 23.51/13.48 fof(f10_neg, negated_conjecture, ~(( ! [X] : ( cowlThing(X) & ~ cowlNothing(X) ) & ! [X] : ( xsd_string(X) <=> ~ xsd_integer(X) ) & ! [X] : ( cc(X) => ( ? [Y0,Y1] : ( rp(X,Y0) & rp(X,Y1) & Y0 != Y1 ) & ! [Y0,Y1,Y2] : ( ( rp(X,Y0) & rp(X,Y1) & rp(X,Y2) ) => ( Y0 = Y1 | Y0 = Y2 | Y1 = Y2 ) ) ) ) )), inference(negated_conjecture, [status(cth)], [f10])).
% 23.51/13.48 fof(f10_nnf, plain, ((? [X] : ((~(cowlThing(X)) | cowlNothing(X))) | ? [X] : (((xsd_string(X) & xsd_integer(X)) | (~(xsd_string(X)) & ~(xsd_integer(X)))))) | ? [X] : ((cc(X) & (! [Y0,Y1] : (((~(rp(X,Y0)) | ~(rp(X,Y1))) | Y0 = Y1)) | ? [Y0,Y1,Y2] : ((((rp(X,Y0) & rp(X,Y1)) & rp(X,Y2)) & ((Y0 != Y1 & Y0 != Y2) & Y1 != Y2))))))), inference(nnf_transformation, [status(thm)], [f10_neg])).
% 23.51/13.48 fof(f10_sk, plain, ! [Y0,Y1] : ((((~(cowlThing(sk2)) | cowlNothing(sk2)) | ((xsd_string(sk3) & xsd_integer(sk3)) | (~(xsd_string(sk3)) & ~(xsd_integer(sk3))))) | (cc(sk4) & (((~(rp(sk4,Y0)) | ~(rp(sk4,Y1))) | Y0 = Y1) | (((rp(sk4,sk5) & rp(sk4,sk6)) & rp(sk4,sk7)) & ((sk5 != sk6 & sk5 != sk7) & sk6 != sk7)))))), inference(skolemisation, [status(esa), new_symbols(skolem, [sk2,sk3,sk4,sk5,sk6,sk7])], [f10_nnf])).
% 23.51/13.48 cnf(c15, plain, ~cowlThing(sk2) | cowlNothing(sk2) | xsd_string(sk3) | ~xsd_string(sk3) | cc(sk4), inference(cnf_transformation, [status(esa)], [f10_sk])).
% 23.51/13.48 cnf(ssp0, plain, (spl0 | spl1 | spl2 | spl3 | spl4), inference(avatar_split_clause, [status(thm)], [c15, sdef0, sdef1, sdef2, sdef3, sdef4])).
% 23.51/13.48 cnf(c16, plain, ~cowlThing(sk2) | cowlNothing(sk2) | xsd_string(sk3) | ~xsd_string(sk3) | ~rp(sk4,X1) | ~rp(sk4,X2) | X1 = X2 | rp(sk4,sk5), inference(cnf_transformation, [status(esa)], [f10_sk])).
% 23.51/13.48 cnf(ssp1, plain, (spl0 | spl1 | spl2 | spl3 | spl5 | spl6), inference(avatar_split_clause, [status(thm)], [c16, sdef0, sdef1, sdef2, sdef3, sdef5, sdef6])).
% 23.51/13.48 cnf(c17, plain, ~cowlThing(sk2) | cowlNothing(sk2) | xsd_string(sk3) | ~xsd_string(sk3) | ~rp(sk4,X1) | ~rp(sk4,X2) | X1 = X2 | rp(sk4,sk6), inference(cnf_transformation, [status(esa)], [f10_sk])).
% 23.51/13.48 cnf(ssp2, plain, (spl0 | spl1 | spl2 | spl3 | spl5 | spl7), inference(avatar_split_clause, [status(thm)], [c17, sdef0, sdef1, sdef2, sdef3, sdef5, sdef7])).
% 23.51/13.48 cnf(c18, plain, ~cowlThing(sk2) | cowlNothing(sk2) | xsd_string(sk3) | ~xsd_string(sk3) | ~rp(sk4,X1) | ~rp(sk4,X2) | X1 = X2 | rp(sk4,sk7), inference(cnf_transformation, [status(esa)], [f10_sk])).
% 23.51/13.48 cnf(ssp3, plain, (spl0 | spl1 | spl2 | spl3 | spl5 | spl8), inference(avatar_split_clause, [status(thm)], [c18, sdef0, sdef1, sdef2, sdef3, sdef5, sdef8])).
% 23.51/13.48 cnf(c19, plain, ~cowlThing(sk2) | cowlNothing(sk2) | xsd_string(sk3) | ~xsd_string(sk3) | ~rp(sk4,X1) | ~rp(sk4,X2) | X1 = X2 | sk5 != sk6, inference(cnf_transformation, [status(esa)], [f10_sk])).
% 23.51/13.48 cnf(ssp4, plain, (spl0 | spl1 | spl2 | spl3 | spl5 | spl9), inference(avatar_split_clause, [status(thm)], [c19, sdef0, sdef1, sdef2, sdef3, sdef5, sdef9])).
% 23.51/13.48 cnf(c20, plain, ~cowlThing(sk2) | cowlNothing(sk2) | xsd_string(sk3) | ~xsd_string(sk3) | ~rp(sk4,X1) | ~rp(sk4,X2) | X1 = X2 | sk5 != sk7, inference(cnf_transformation, [status(esa)], [f10_sk])).
% 23.51/13.48 cnf(ssp5, plain, (spl0 | spl1 | spl2 | spl3 | spl5 | spl10), inference(avatar_split_clause, [status(thm)], [c20, sdef0, sdef1, sdef2, sdef3, sdef5, sdef10])).
% 23.51/13.48 cnf(c21, plain, ~cowlThing(sk2) | cowlNothing(sk2) | xsd_string(sk3) | ~xsd_string(sk3) | ~rp(sk4,X1) | ~rp(sk4,X2) | X1 = X2 | sk6 != sk7, inference(cnf_transformation, [status(esa)], [f10_sk])).
% 23.51/13.48 cnf(ssp6, plain, (spl0 | spl1 | spl2 | spl3 | spl5 | spl11), inference(avatar_split_clause, [status(thm)], [c21, sdef0, sdef1, sdef2, sdef3, sdef5, sdef11])).
% 23.51/13.48 cnf(c22, plain, ~cowlThing(sk2) | cowlNothing(sk2) | xsd_string(sk3) | ~xsd_integer(sk3) | cc(sk4), inference(cnf_transformation, [status(esa)], [f10_sk])).
% 23.51/13.48 cnf(ssp7, plain, (spl0 | spl1 | spl2 | spl4 | spl12), inference(avatar_split_clause, [status(thm)], [c22, sdef0, sdef1, sdef2, sdef4, sdef12])).
% 23.51/13.48 cnf(c23, plain, ~cowlThing(sk2) | cowlNothing(sk2) | xsd_string(sk3) | ~xsd_integer(sk3) | ~rp(sk4,X1) | ~rp(sk4,X2) | X1 = X2 | rp(sk4,sk5), inference(cnf_transformation, [status(esa)], [f10_sk])).
% 23.51/13.48 cnf(ssp8, plain, (spl0 | spl1 | spl2 | spl5 | spl6 | spl12), inference(avatar_split_clause, [status(thm)], [c23, sdef0, sdef1, sdef2, sdef5, sdef6, sdef12])).
% 23.51/13.48 cnf(c24, plain, ~cowlThing(sk2) | cowlNothing(sk2) | xsd_string(sk3) | ~xsd_integer(sk3) | ~rp(sk4,X1) | ~rp(sk4,X2) | X1 = X2 | rp(sk4,sk6), inference(cnf_transformation, [status(esa)], [f10_sk])).
% 23.51/13.48 cnf(ssp9, plain, (spl0 | spl1 | spl2 | spl5 | spl7 | spl12), inference(avatar_split_clause, [status(thm)], [c24, sdef0, sdef1, sdef2, sdef5, sdef7, sdef12])).
% 23.51/13.48 cnf(c25, plain, ~cowlThing(sk2) | cowlNothing(sk2) | xsd_string(sk3) | ~xsd_integer(sk3) | ~rp(sk4,X1) | ~rp(sk4,X2) | X1 = X2 | rp(sk4,sk7), inference(cnf_transformation, [status(esa)], [f10_sk])).
% 23.51/13.48 cnf(ssp10, plain, (spl0 | spl1 | spl2 | spl5 | spl8 | spl12), inference(avatar_split_clause, [status(thm)], [c25, sdef0, sdef1, sdef2, sdef5, sdef8, sdef12])).
% 23.51/13.48 cnf(c26, plain, ~cowlThing(sk2) | cowlNothing(sk2) | xsd_string(sk3) | ~xsd_integer(sk3) | ~rp(sk4,X1) | ~rp(sk4,X2) | X1 = X2 | sk5 != sk6, inference(cnf_transformation, [status(esa)], [f10_sk])).
% 23.51/13.48 cnf(ssp11, plain, (spl0 | spl1 | spl2 | spl5 | spl9 | spl12), inference(avatar_split_clause, [status(thm)], [c26, sdef0, sdef1, sdef2, sdef5, sdef9, sdef12])).
% 23.51/13.48 cnf(c27, plain, ~cowlThing(sk2) | cowlNothing(sk2) | xsd_string(sk3) | ~xsd_integer(sk3) | ~rp(sk4,X1) | ~rp(sk4,X2) | X1 = X2 | sk5 != sk7, inference(cnf_transformation, [status(esa)], [f10_sk])).
% 23.51/13.48 cnf(ssp12, plain, (spl0 | spl1 | spl2 | spl5 | spl10 | spl12), inference(avatar_split_clause, [status(thm)], [c27, sdef0, sdef1, sdef2, sdef5, sdef10, sdef12])).
% 23.51/13.48 cnf(c28, plain, ~cowlThing(sk2) | cowlNothing(sk2) | xsd_string(sk3) | ~xsd_integer(sk3) | ~rp(sk4,X1) | ~rp(sk4,X2) | X1 = X2 | sk6 != sk7, inference(cnf_transformation, [status(esa)], [f10_sk])).
% 23.51/13.48 cnf(ssp13, plain, (spl0 | spl1 | spl2 | spl5 | spl11 | spl12), inference(avatar_split_clause, [status(thm)], [c28, sdef0, sdef1, sdef2, sdef5, sdef11, sdef12])).
% 23.51/13.48 cnf(c29, plain, ~cowlThing(sk2) | cowlNothing(sk2) | xsd_integer(sk3) | ~xsd_string(sk3) | cc(sk4), inference(cnf_transformation, [status(esa)], [f10_sk])).
% 23.51/13.48 cnf(ssp14, plain, (spl0 | spl1 | spl3 | spl4 | spl13), inference(avatar_split_clause, [status(thm)], [c29, sdef0, sdef1, sdef3, sdef4, sdef13])).
% 23.51/13.48 cnf(c30, plain, ~cowlThing(sk2) | cowlNothing(sk2) | xsd_integer(sk3) | ~xsd_string(sk3) | ~rp(sk4,X1) | ~rp(sk4,X2) | X1 = X2 | rp(sk4,sk5), inference(cnf_transformation, [status(esa)], [f10_sk])).
% 23.51/13.48 cnf(ssp15, plain, (spl0 | spl1 | spl3 | spl5 | spl6 | spl13), inference(avatar_split_clause, [status(thm)], [c30, sdef0, sdef1, sdef3, sdef5, sdef6, sdef13])).
% 23.51/13.48 cnf(c31, plain, ~cowlThing(sk2) | cowlNothing(sk2) | xsd_integer(sk3) | ~xsd_string(sk3) | ~rp(sk4,X1) | ~rp(sk4,X2) | X1 = X2 | rp(sk4,sk6), inference(cnf_transformation, [status(esa)], [f10_sk])).
% 23.51/13.48 cnf(ssp16, plain, (spl0 | spl1 | spl3 | spl5 | spl7 | spl13), inference(avatar_split_clause, [status(thm)], [c31, sdef0, sdef1, sdef3, sdef5, sdef7, sdef13])).
% 23.51/13.48 cnf(c32, plain, ~cowlThing(sk2) | cowlNothing(sk2) | xsd_integer(sk3) | ~xsd_string(sk3) | ~rp(sk4,X1) | ~rp(sk4,X2) | X1 = X2 | rp(sk4,sk7), inference(cnf_transformation, [status(esa)], [f10_sk])).
% 23.51/13.48 cnf(ssp17, plain, (spl0 | spl1 | spl3 | spl5 | spl8 | spl13), inference(avatar_split_clause, [status(thm)], [c32, sdef0, sdef1, sdef3, sdef5, sdef8, sdef13])).
% 23.51/13.48 cnf(c33, plain, ~cowlThing(sk2) | cowlNothing(sk2) | xsd_integer(sk3) | ~xsd_string(sk3) | ~rp(sk4,X1) | ~rp(sk4,X2) | X1 = X2 | sk5 != sk6, inference(cnf_transformation, [status(esa)], [f10_sk])).
% 23.51/13.48 cnf(ssp18, plain, (spl0 | spl1 | spl3 | spl5 | spl9 | spl13), inference(avatar_split_clause, [status(thm)], [c33, sdef0, sdef1, sdef3, sdef5, sdef9, sdef13])).
% 23.51/13.48 cnf(c34, plain, ~cowlThing(sk2) | cowlNothing(sk2) | xsd_integer(sk3) | ~xsd_string(sk3) | ~rp(sk4,X1) | ~rp(sk4,X2) | X1 = X2 | sk5 != sk7, inference(cnf_transformation, [status(esa)], [f10_sk])).
% 23.51/13.48 cnf(ssp19, plain, (spl0 | spl1 | spl3 | spl5 | spl10 | spl13), inference(avatar_split_clause, [status(thm)], [c34, sdef0, sdef1, sdef3, sdef5, sdef10, sdef13])).
% 23.51/13.48 cnf(c35, plain, ~cowlThing(sk2) | cowlNothing(sk2) | xsd_integer(sk3) | ~xsd_string(sk3) | ~rp(sk4,X1) | ~rp(sk4,X2) | X1 = X2 | sk6 != sk7, inference(cnf_transformation, [status(esa)], [f10_sk])).
% 23.51/13.48 cnf(ssp20, plain, (spl0 | spl1 | spl3 | spl5 | spl11 | spl13), inference(avatar_split_clause, [status(thm)], [c35, sdef0, sdef1, sdef3, sdef5, sdef11, sdef13])).
% 23.51/13.48 cnf(c36, plain, ~cowlThing(sk2) | cowlNothing(sk2) | xsd_integer(sk3) | ~xsd_integer(sk3) | cc(sk4), inference(cnf_transformation, [status(esa)], [f10_sk])).
% 23.51/13.48 cnf(ssp21, plain, (spl0 | spl1 | spl4 | spl12 | spl13), inference(avatar_split_clause, [status(thm)], [c36, sdef0, sdef1, sdef4, sdef12, sdef13])).
% 23.51/13.48 cnf(c37, plain, ~cowlThing(sk2) | cowlNothing(sk2) | xsd_integer(sk3) | ~xsd_integer(sk3) | ~rp(sk4,X1) | ~rp(sk4,X2) | X1 = X2 | rp(sk4,sk5), inference(cnf_transformation, [status(esa)], [f10_sk])).
% 23.51/13.48 cnf(ssp22, plain, (spl0 | spl1 | spl5 | spl6 | spl12 | spl13), inference(avatar_split_clause, [status(thm)], [c37, sdef0, sdef1, sdef5, sdef6, sdef12, sdef13])).
% 23.51/13.48 cnf(c38, plain, ~cowlThing(sk2) | cowlNothing(sk2) | xsd_integer(sk3) | ~xsd_integer(sk3) | ~rp(sk4,X1) | ~rp(sk4,X2) | X1 = X2 | rp(sk4,sk6), inference(cnf_transformation, [status(esa)], [f10_sk])).
% 23.51/13.48 cnf(ssp23, plain, (spl0 | spl1 | spl5 | spl7 | spl12 | spl13), inference(avatar_split_clause, [status(thm)], [c38, sdef0, sdef1, sdef5, sdef7, sdef12, sdef13])).
% 23.51/13.48 cnf(c39, plain, ~cowlThing(sk2) | cowlNothing(sk2) | xsd_integer(sk3) | ~xsd_integer(sk3) | ~rp(sk4,X1) | ~rp(sk4,X2) | X1 = X2 | rp(sk4,sk7), inference(cnf_transformation, [status(esa)], [f10_sk])).
% 23.51/13.48 cnf(ssp24, plain, (spl0 | spl1 | spl5 | spl8 | spl12 | spl13), inference(avatar_split_clause, [status(thm)], [c39, sdef0, sdef1, sdef5, sdef8, sdef12, sdef13])).
% 23.51/13.48 cnf(c40, plain, ~cowlThing(sk2) | cowlNothing(sk2) | xsd_integer(sk3) | ~xsd_integer(sk3) | ~rp(sk4,X1) | ~rp(sk4,X2) | X1 = X2 | sk5 != sk6, inference(cnf_transformation, [status(esa)], [f10_sk])).
% 23.51/13.48 cnf(ssp25, plain, (spl0 | spl1 | spl5 | spl9 | spl12 | spl13), inference(avatar_split_clause, [status(thm)], [c40, sdef0, sdef1, sdef5, sdef9, sdef12, sdef13])).
% 23.51/13.48 cnf(c41, plain, ~cowlThing(sk2) | cowlNothing(sk2) | xsd_integer(sk3) | ~xsd_integer(sk3) | ~rp(sk4,X1) | ~rp(sk4,X2) | X1 = X2 | sk5 != sk7, inference(cnf_transformation, [status(esa)], [f10_sk])).
% 23.51/13.48 cnf(ssp26, plain, (spl0 | spl1 | spl5 | spl10 | spl12 | spl13), inference(avatar_split_clause, [status(thm)], [c41, sdef0, sdef1, sdef5, sdef10, sdef12, sdef13])).
% 23.51/13.48 cnf(c42, plain, ~cowlThing(sk2) | cowlNothing(sk2) | xsd_integer(sk3) | ~xsd_integer(sk3) | ~rp(sk4,X1) | ~rp(sk4,X2) | X1 = X2 | sk6 != sk7, inference(cnf_transformation, [status(esa)], [f10_sk])).
% 23.51/13.48 cnf(ssp27, plain, (spl0 | spl1 | spl5 | spl11 | spl12 | spl13), inference(avatar_split_clause, [status(thm)], [c42, sdef0, sdef1, sdef5, sdef11, sdef12, sdef13])).
% 23.51/13.48 fof(f0, axiom, ! [A,B] : ( ( A = B & cc(A) ) => cc(B) ), file('/export/starexec/sandbox/benchmark/theBenchmark.p', cc_substitution_1)).
% 23.51/13.48 fof(f0_nnf, plain, ! [A,B] : (((A != B | ~(cc(A))) | cc(B))), inference(nnf_transformation, [status(thm)], [f0])).
% 23.51/13.48 fof(f0_sk, plain, ! [A,B] : (((A != B | ~(cc(A))) | cc(B))), inference(skolemisation, [status(esa)], [f0_nnf])).
% 23.51/13.48 cnf(c0, plain, X0 != X1 | ~cc(X0) | cc(X1), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 23.51/13.48 cnf(p64, plain, (~cc(sk5) | cc(sk6) | ~spl5 | ~spl6 | ~spl7), inference(resolution, [status(thm)], [p62, c0])).
% 23.51/13.48 fof(sdef14, definition, (spl14 <=> (~cc(sk5))), introduced(definition, [new_symbols(naming, [spl14])], [avatar_definition])).
% 23.51/13.48 cnf(ssp28, plain, (~spl5 | ~spl6 | ~spl7 | spl14 | spl15), inference(avatar_split_clause, [status(thm)], [p64, sdef14, sdef15])).
% 23.51/13.48 cnf(p71, plain, (~cc(sk6) | cc(sk7) | ~spl5 | ~spl7 | ~spl8), inference(resolution, [status(thm)], [p70, c0])).
% 23.51/13.48 cnf(ssp29, plain, (~spl5 | ~spl7 | ~spl8 | spl16 | spl17), inference(avatar_split_clause, [status(thm)], [p71, sdef16, sdef17])).
% 23.51/13.48 cnf(p61, plain, (~rp(sk4,X0) | sk7 = X0 | ~spl5 | ~spl8), inference(resolution, [status(thm)], [p22, p27])).
% 23.51/13.48 cnf(p81, plain, (sk7 = sk0(sk4) | ~spl4 | ~spl5 | ~spl8), inference(resolution, [status(thm)], [p78, p61])).
% 23.51/13.48 cnf(p82, plain, (~cc(sk7) | cc(sk0(sk4)) | ~spl4 | ~spl5 | ~spl8), inference(resolution, [status(thm)], [p81, c0])).
% 23.51/13.48 cnf(ssp30, plain, (~spl4 | ~spl5 | ~spl8 | spl18 | spl19), inference(avatar_split_clause, [status(thm)], [p82, sdef18, sdef19])).
% 23.51/13.48 fof(f5, axiom, ! [A,B] : ( ( A = B & xsd_integer(A) ) => xsd_integer(B) ), file('/export/starexec/sandbox/benchmark/theBenchmark.p', xsd_integer_substitution_1)).
% 23.51/13.48 fof(f5_nnf, plain, ! [A,B] : (((A != B | ~(xsd_integer(A))) | xsd_integer(B))), inference(nnf_transformation, [status(thm)], [f5])).
% 23.51/13.48 fof(f5_sk, plain, ! [A,B] : (((A != B | ~(xsd_integer(A))) | xsd_integer(B))), inference(skolemisation, [status(esa)], [f5_nnf])).
% 23.51/13.48 cnf(c5, plain, X0 != X1 | ~xsd_integer(X0) | xsd_integer(X1), inference(cnf_transformation, [status(esa)], [f5_sk])).
% 23.51/13.48 cnf(p87, plain, (~xsd_integer(sk7) | xsd_integer(sk0(sk4)) | ~spl4 | ~spl5 | ~spl8), inference(resolution, [status(thm)], [p81, c5])).
% 23.51/13.48 cnf(ssp31, plain, (~spl4 | ~spl5 | ~spl8 | spl20 | spl21), inference(avatar_split_clause, [status(thm)], [p87, sdef20, sdef21])).
% 23.51/13.48 fof(f6, axiom, ! [A,B] : ( ( A = B & xsd_string(A) ) => xsd_string(B) ), file('/export/starexec/sandbox/benchmark/theBenchmark.p', xsd_string_substitution_1)).
% 23.51/13.48 fof(f6_nnf, plain, ! [A,B] : (((A != B | ~(xsd_string(A))) | xsd_string(B))), inference(nnf_transformation, [status(thm)], [f6])).
% 23.51/13.48 fof(f6_sk, plain, ! [A,B] : (((A != B | ~(xsd_string(A))) | xsd_string(B))), inference(skolemisation, [status(esa)], [f6_nnf])).
% 23.51/13.48 cnf(c6, plain, X0 != X1 | ~xsd_string(X0) | xsd_string(X1), inference(cnf_transformation, [status(esa)], [f6_sk])).
% 23.51/13.48 cnf(p90, plain, (~xsd_string(sk7) | xsd_string(sk0(sk4)) | ~spl4 | ~spl5 | ~spl8), inference(resolution, [status(thm)], [p81, c6])).
% 23.51/13.48 cnf(ssp32, plain, (~spl4 | ~spl5 | ~spl8 | spl22 | spl23), inference(avatar_split_clause, [status(thm)], [p90, sdef22, sdef23])).
% 23.51/13.48 cnf(p108, plain, (sk6 = sk1(sk4) | ~spl4 | ~spl5 | ~spl7), inference(resolution, [status(thm)], [p99, p60])).
% 23.51/13.48 cnf(p109, plain, (~cc(sk6) | cc(sk1(sk4)) | ~spl4 | ~spl5 | ~spl7), inference(resolution, [status(thm)], [p108, c0])).
% 23.51/13.48 fof(sdef24, definition, (spl24 <=> (cc(sk1(sk4)))), introduced(definition, [new_symbols(naming, [spl24])], [avatar_definition])).
% 23.51/13.48 cnf(ssp33, plain, (~spl4 | ~spl5 | ~spl7 | spl16 | spl24), inference(avatar_split_clause, [status(thm)], [p109, sdef16, sdef24])).
% 23.51/13.48 cnf(p113, plain, (~xsd_integer(sk6) | xsd_integer(sk1(sk4)) | ~spl4 | ~spl5 | ~spl7), inference(resolution, [status(thm)], [p108, c5])).
% 23.51/13.48 cnf(ssp34, plain, (~spl4 | ~spl5 | ~spl7 | spl25 | spl26), inference(avatar_split_clause, [status(thm)], [p113, sdef25, sdef26])).
% 23.51/13.48 cnf(p116, plain, (~xsd_string(sk6) | xsd_string(sk1(sk4)) | ~spl4 | ~spl5 | ~spl7), inference(resolution, [status(thm)], [p108, c6])).
% 23.51/13.48 cnf(ssp35, plain, (~spl4 | ~spl5 | ~spl7 | spl27 | spl28), inference(avatar_split_clause, [status(thm)], [p116, sdef27, sdef28])).
% 23.51/13.48 cnf(p139, plain, (~cc(sk0(sk4)) | cc(sk1(sk4)) | ~spl4 | ~spl5), inference(resolution, [status(thm)], [p127, c0])).
% 23.51/13.48 cnf(ssp36, plain, (~spl4 | ~spl5 | spl24 | spl29), inference(avatar_split_clause, [status(thm)], [p139, sdef24, sdef29])).
% 23.51/13.48 cnf(p143, plain, (~xsd_integer(sk0(sk4)) | xsd_integer(sk1(sk4)) | ~spl4 | ~spl5), inference(resolution, [status(thm)], [p127, c5])).
% 23.51/13.48 cnf(ssp37, plain, (~spl4 | ~spl5 | spl26 | spl30), inference(avatar_split_clause, [status(thm)], [p143, sdef26, sdef30])).
% 23.51/13.48 cnf(p145, plain, (~xsd_string(sk0(sk4)) | xsd_string(sk1(sk4)) | ~spl4 | ~spl5), inference(resolution, [status(thm)], [p127, c6])).
% 23.51/13.48 cnf(ssp38, plain, (~spl4 | ~spl5 | spl28 | spl31), inference(avatar_split_clause, [status(thm)], [p145, sdef28, sdef31])).
% 23.51/13.48 cnf(c11, plain, ~cc(X0) | ~rp(X0,X1) | ~rp(X0,X2) | ~rp(X0,X3) | X1 = X2 | X1 = X3 | X2 = X3, inference(cnf_transformation, [status(esa)], [f9_sk])).
% 23.51/13.48 cnf(p94, plain, (~rp(sk4,X0) | ~rp(sk4,X1) | ~rp(sk4,X2) | X0 = X1 | X0 = X2 | X1 = X2 | ~spl4), inference(resolution, [status(thm)], [c11, p20])).
% 23.51/13.48 cnf(p151, plain, (~rp(sk4,X0) | ~rp(sk4,X1) | sk5 = X0 | sk5 = X1 | X0 = X1 | ~spl4 | ~spl6), inference(resolution, [status(thm)], [p94, p23])).
% 23.51/13.48 cnf(p163, plain, (~rp(sk4,X0) | sk5 = sk6 | sk5 = X0 | sk6 = X0 | ~spl4 | ~spl6 | ~spl7), inference(resolution, [status(thm)], [p151, p25])).
% 23.51/13.48 fof(sdef32, definition, (spl32 <=> (~rp(sk4,X0) | sk5 = X0 | sk6 = X0)), introduced(definition, [new_symbols(naming, [spl32])], [avatar_definition])).
% 23.51/13.48 cnf(ssp39, plain, (~spl4 | ~spl6 | ~spl7 | spl32 | spl33), inference(avatar_split_clause, [status(thm)], [p163, sdef32, sdef33])).
% 23.51/13.48 cnf(p166, plain, (~rp(sk4,X0) | sk5 = sk7 | sk5 = X0 | sk7 = X0 | ~spl4 | ~spl6 | ~spl8), inference(resolution, [status(thm)], [p151, p27])).
% 23.51/13.48 fof(sdef34, definition, (spl34 <=> (~rp(sk4,X0) | sk5 = X0 | sk7 = X0)), introduced(definition, [new_symbols(naming, [spl34])], [avatar_definition])).
% 23.51/13.48 cnf(ssp40, plain, (~spl4 | ~spl6 | ~spl8 | spl34 | spl35), inference(avatar_split_clause, [status(thm)], [p166, sdef34, sdef35])).
% 23.51/13.48 cnf(p169, plain, (~rp(sk4,X0) | sk5 = sk0(sk4) | sk5 = X0 | sk0(sk4) = X0 | ~spl4 | ~spl6), inference(resolution, [status(thm)], [p151, p78])).
% 23.51/13.48 fof(sdef36, definition, (spl36 <=> (~rp(sk4,X0) | sk5 = X0 | sk0(sk4) = X0)), introduced(definition, [new_symbols(naming, [spl36])], [avatar_definition])).
% 23.51/13.48 cnf(ssp41, plain, (~spl4 | ~spl6 | spl36 | spl37), inference(avatar_split_clause, [status(thm)], [p169, sdef36, sdef37])).
% 23.51/13.48 cnf(p172, plain, (~rp(sk4,X0) | sk5 = sk1(sk4) | sk5 = X0 | sk1(sk4) = X0 | ~spl4 | ~spl6), inference(resolution, [status(thm)], [p151, p99])).
% 23.51/13.48 fof(sdef38, definition, (spl38 <=> (~rp(sk4,X0) | sk5 = X0 | sk1(sk4) = X0)), introduced(definition, [new_symbols(naming, [spl38])], [avatar_definition])).
% 23.51/13.48 fof(sdef39, definition, (spl39 <=> (sk5 = sk1(sk4))), introduced(definition, [new_symbols(naming, [spl39])], [avatar_definition])).
% 23.51/13.48 cnf(ssp42, plain, (~spl4 | ~spl6 | spl38 | spl39), inference(avatar_split_clause, [status(thm)], [p172, sdef38, sdef39])).
% 23.51/13.48 cnf(p175, plain, (~cc(sk5) | cc(sk6) | ~spl33), inference(resolution, [status(thm)], [p165, c0])).
% 23.51/13.48 cnf(ssp43, plain, (~spl33 | spl14 | spl15), inference(avatar_split_clause, [status(thm)], [p175, sdef14, sdef15])).
% 23.51/13.48 cnf(p178, plain, (~cc(sk5) | cc(sk7) | ~spl35), inference(resolution, [status(thm)], [p168, c0])).
% 23.51/13.48 cnf(ssp44, plain, (~spl35 | spl14 | spl17), inference(avatar_split_clause, [status(thm)], [p178, sdef14, sdef17])).
% 23.51/13.48 cnf(p181, plain, (~cc(sk5) | cc(sk0(sk4)) | ~spl37), inference(resolution, [status(thm)], [p171, c0])).
% 23.51/13.48 cnf(ssp45, plain, (~spl37 | spl14 | spl19), inference(avatar_split_clause, [status(thm)], [p181, sdef14, sdef19])).
% 23.51/13.48 cnf(p184, plain, (~xsd_integer(sk5) | xsd_integer(sk0(sk4)) | ~spl37), inference(resolution, [status(thm)], [p171, c5])).
% 23.51/13.48 cnf(ssp46, plain, (~spl37 | spl21 | spl40), inference(avatar_split_clause, [status(thm)], [p184, sdef21, sdef40])).
% 23.51/13.48 cnf(p186, plain, (~xsd_string(sk5) | xsd_string(sk0(sk4)) | ~spl37), inference(resolution, [status(thm)], [p171, c6])).
% 23.51/13.48 cnf(ssp47, plain, (~spl37 | spl23 | spl41), inference(avatar_split_clause, [status(thm)], [p186, sdef23, sdef41])).
% 23.51/13.48 cnf(p174, plain, (sk5 = sk1(sk4) | ~spl39), inference(avatar_component_clause, [status(thm)], [sdef39])).
% 23.51/13.48 cnf(p203, plain, (~cc(sk5) | cc(sk1(sk4)) | ~spl39), inference(resolution, [status(thm)], [p174, c0])).
% 23.51/13.48 cnf(ssp48, plain, (~spl39 | spl14 | spl24), inference(avatar_split_clause, [status(thm)], [p203, sdef14, sdef24])).
% 23.51/13.48 cnf(p206, plain, (~xsd_integer(sk5) | xsd_integer(sk1(sk4)) | ~spl39), inference(resolution, [status(thm)], [p174, c5])).
% 23.51/13.48 cnf(ssp49, plain, (~spl39 | spl26 | spl40), inference(avatar_split_clause, [status(thm)], [p206, sdef26, sdef40])).
% 23.51/13.48 cnf(p164, plain, (~rp(sk4,X0) | sk5 = X0 | sk6 = X0 | ~spl32), inference(avatar_component_clause, [status(thm)], [sdef32])).
% 23.51/13.48 cnf(p207, plain, (sk5 = sk7 | sk6 = sk7 | ~spl8 | ~spl32), inference(resolution, [status(thm)], [p164, p27])).
% 23.51/13.48 cnf(ssp50, plain, (~spl8 | ~spl32 | spl35 | spl42), inference(avatar_split_clause, [status(thm)], [p207, sdef35, sdef42])).
% 23.51/13.48 cnf(p209, plain, (sk5 = sk0(sk4) | sk6 = sk0(sk4) | ~spl4 | ~spl32), inference(resolution, [status(thm)], [p164, p78])).
% 23.51/13.48 fof(sdef43, definition, (spl43 <=> (sk6 = sk0(sk4))), introduced(definition, [new_symbols(naming, [spl43])], [avatar_definition])).
% 23.51/13.48 cnf(ssp51, plain, (~spl4 | ~spl32 | spl37 | spl43), inference(avatar_split_clause, [status(thm)], [p209, sdef37, sdef43])).
% 23.51/13.48 cnf(p211, plain, (sk5 = sk1(sk4) | sk6 = sk1(sk4) | ~spl4 | ~spl32), inference(resolution, [status(thm)], [p164, p99])).
% 23.51/13.48 fof(sdef44, definition, (spl44 <=> (sk6 = sk1(sk4))), introduced(definition, [new_symbols(naming, [spl44])], [avatar_definition])).
% 23.51/13.48 cnf(ssp52, plain, (~spl4 | ~spl32 | spl39 | spl44), inference(avatar_split_clause, [status(thm)], [p211, sdef39, sdef44])).
% 23.51/13.48 cnf(p217, plain, (~cc(sk6) | cc(sk7) | ~spl42), inference(resolution, [status(thm)], [p208, c0])).
% 23.51/13.48 cnf(ssp53, plain, (~spl42 | spl16 | spl17), inference(avatar_split_clause, [status(thm)], [p217, sdef16, sdef17])).
% 23.51/13.48 cnf(p223, plain, (~xsd_integer(sk6) | xsd_integer(sk7) | ~spl42), inference(resolution, [status(thm)], [p208, c5])).
% 23.51/13.48 cnf(ssp54, plain, (~spl42 | spl25 | spl45), inference(avatar_split_clause, [status(thm)], [p223, sdef25, sdef45])).
% 23.51/13.48 cnf(p225, plain, (~xsd_string(sk6) | xsd_string(sk7) | ~spl42), inference(resolution, [status(thm)], [p208, c6])).
% 23.51/13.48 cnf(ssp55, plain, (~spl42 | spl27 | spl46), inference(avatar_split_clause, [status(thm)], [p225, sdef27, sdef46])).
% 23.51/13.48 cnf(p152, plain, (~rp(sk4,X0) | ~rp(sk4,X1) | sk6 = X0 | sk6 = X1 | X0 = X1 | ~spl4 | ~spl7), inference(resolution, [status(thm)], [p94, p25])).
% 23.51/13.48 cnf(p232, plain, (~rp(sk4,X0) | sk6 = sk5 | sk6 = X0 | sk5 = X0 | ~spl4 | ~spl6 | ~spl7), inference(resolution, [status(thm)], [p152, p23])).
% 23.51/13.48 fof(sdef47, definition, (spl47 <=> (sk6 = sk5)), introduced(definition, [new_symbols(naming, [spl47])], [avatar_definition])).
% 23.51/13.48 cnf(ssp56, plain, (~spl4 | ~spl6 | ~spl7 | spl32 | spl47), inference(avatar_split_clause, [status(thm)], [p232, sdef32, sdef47])).
% 23.51/13.48 cnf(p234, plain, (~rp(sk4,X0) | sk6 = sk7 | sk6 = X0 | sk7 = X0 | ~spl4 | ~spl7 | ~spl8), inference(resolution, [status(thm)], [p152, p27])).
% 23.51/13.48 fof(sdef48, definition, (spl48 <=> (~rp(sk4,X0) | sk6 = X0 | sk7 = X0)), introduced(definition, [new_symbols(naming, [spl48])], [avatar_definition])).
% 23.51/13.48 cnf(ssp57, plain, (~spl4 | ~spl7 | ~spl8 | spl42 | spl48), inference(avatar_split_clause, [status(thm)], [p234, sdef42, sdef48])).
% 23.51/13.48 cnf(p236, plain, (~rp(sk4,X0) | sk6 = sk0(sk4) | sk6 = X0 | sk0(sk4) = X0 | ~spl4 | ~spl7), inference(resolution, [status(thm)], [p152, p78])).
% 23.51/13.48 fof(sdef49, definition, (spl49 <=> (~rp(sk4,X0) | sk6 = X0 | sk0(sk4) = X0)), introduced(definition, [new_symbols(naming, [spl49])], [avatar_definition])).
% 23.51/13.48 cnf(ssp58, plain, (~spl4 | ~spl7 | spl43 | spl49), inference(avatar_split_clause, [status(thm)], [p236, sdef43, sdef49])).
% 23.51/13.48 cnf(p238, plain, (~rp(sk4,X0) | sk6 = sk1(sk4) | sk6 = X0 | sk1(sk4) = X0 | ~spl4 | ~spl7), inference(resolution, [status(thm)], [p152, p99])).
% 23.51/13.48 fof(sdef50, definition, (spl50 <=> (~rp(sk4,X0) | sk6 = X0 | sk1(sk4) = X0)), introduced(definition, [new_symbols(naming, [spl50])], [avatar_definition])).
% 23.51/13.48 cnf(ssp59, plain, (~spl4 | ~spl7 | spl44 | spl50), inference(avatar_split_clause, [status(thm)], [p238, sdef44, sdef50])).
% 23.51/13.48 cnf(p153, plain, (~rp(sk4,X0) | ~rp(sk4,X1) | sk7 = X0 | sk7 = X1 | X0 = X1 | ~spl4 | ~spl8), inference(resolution, [status(thm)], [p94, p27])).
% 23.51/13.48 cnf(p244, plain, (~rp(sk4,X0) | sk7 = sk5 | sk7 = X0 | sk5 = X0 | ~spl4 | ~spl6 | ~spl8), inference(resolution, [status(thm)], [p153, p23])).
% 23.51/13.48 fof(sdef51, definition, (spl51 <=> (sk7 = sk5)), introduced(definition, [new_symbols(naming, [spl51])], [avatar_definition])).
% 23.51/13.48 cnf(ssp60, plain, (~spl4 | ~spl6 | ~spl8 | spl34 | spl51), inference(avatar_split_clause, [status(thm)], [p244, sdef34, sdef51])).
% 23.51/13.48 cnf(p246, plain, (~rp(sk4,X0) | sk7 = sk6 | sk7 = X0 | sk6 = X0 | ~spl4 | ~spl7 | ~spl8), inference(resolution, [status(thm)], [p153, p25])).
% 23.51/13.48 fof(sdef52, definition, (spl52 <=> (sk7 = sk6)), introduced(definition, [new_symbols(naming, [spl52])], [avatar_definition])).
% 23.51/13.48 cnf(ssp61, plain, (~spl4 | ~spl7 | ~spl8 | spl48 | spl52), inference(avatar_split_clause, [status(thm)], [p246, sdef48, sdef52])).
% 23.51/13.48 cnf(p248, plain, (~rp(sk4,X0) | sk7 = sk0(sk4) | sk7 = X0 | sk0(sk4) = X0 | ~spl4 | ~spl8), inference(resolution, [status(thm)], [p153, p78])).
% 23.51/13.48 fof(sdef53, definition, (spl53 <=> (~rp(sk4,X0) | sk7 = X0 | sk0(sk4) = X0)), introduced(definition, [new_symbols(naming, [spl53])], [avatar_definition])).
% 23.51/13.48 fof(sdef54, definition, (spl54 <=> (sk7 = sk0(sk4))), introduced(definition, [new_symbols(naming, [spl54])], [avatar_definition])).
% 23.51/13.48 cnf(ssp62, plain, (~spl4 | ~spl8 | spl53 | spl54), inference(avatar_split_clause, [status(thm)], [p248, sdef53, sdef54])).
% 23.51/13.48 cnf(p251, plain, (~rp(sk4,X0) | sk7 = sk1(sk4) | sk7 = X0 | sk1(sk4) = X0 | ~spl4 | ~spl8), inference(resolution, [status(thm)], [p153, p99])).
% 23.51/13.48 fof(sdef55, definition, (spl55 <=> (~rp(sk4,X0) | sk7 = X0 | sk1(sk4) = X0)), introduced(definition, [new_symbols(naming, [spl55])], [avatar_definition])).
% 23.51/13.48 fof(sdef56, definition, (spl56 <=> (sk7 = sk1(sk4))), introduced(definition, [new_symbols(naming, [spl56])], [avatar_definition])).
% 23.51/13.48 cnf(ssp63, plain, (~spl4 | ~spl8 | spl55 | spl56), inference(avatar_split_clause, [status(thm)], [p251, sdef55, sdef56])).
% 23.51/13.49 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, sct0, sct1, sct2, sct3, sct4, sct5, sct6, sct7, sct8, sct9, sct10, sct11, sct12, sct13, sct14, sct15, sct16, sct17, sct18, sct19, sct20, sct21, sct22, sct23, sct24])).
% 23.51/13.49 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------