%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : KRS138+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 : n006.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:18 PM UTC 2026
% Result : Theorem 64.85s 8.81s
% Output : Proof 64.85s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : KRS138+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/0.37 % Computer : n006.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Wed Sep 23 19:28:41 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 64.85/8.81 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 64.85/8.81 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 64.85/8.81 fof(sdef3, definition, (spl3 <=> (~xsd_string(sk1))), introduced(definition, [new_symbols(naming, [spl3])], [avatar_definition])).
% 64.85/8.81 cnf(p25, plain, (~xsd_string(sk1) | ~spl3), inference(avatar_component_clause, [status(thm)], [sdef3])).
% 64.85/8.81 fof(sdef2, definition, (spl2 <=> (xsd_string(sk1))), introduced(definition, [new_symbols(naming, [spl2])], [avatar_definition])).
% 64.85/8.81 cnf(p24, plain, (xsd_string(sk1) | ~spl2), inference(avatar_component_clause, [status(thm)], [sdef2])).
% 64.85/8.81 cnf(p69, plain, ($false | ~spl2 | ~spl3), inference(resolution, [status(thm)], [p25, p24])).
% 64.85/8.81 cnf(sct0, plain, (~spl2 | ~spl3), inference(avatar_contradiction_clause, [status(thm)], [p69])).
% 64.85/8.81 fof(sdef15, definition, (spl15 <=> (xsd_integer(sk1))), introduced(definition, [new_symbols(naming, [spl15])], [avatar_definition])).
% 64.85/8.81 cnf(p53, plain, (xsd_integer(sk1) | ~spl15), inference(avatar_component_clause, [status(thm)], [sdef15])).
% 64.85/8.81 fof(sdef14, definition, (spl14 <=> (~xsd_integer(sk1))), introduced(definition, [new_symbols(naming, [spl14])], [avatar_definition])).
% 64.85/8.81 cnf(p44, plain, (~xsd_integer(sk1) | ~spl14), inference(avatar_component_clause, [status(thm)], [sdef14])).
% 64.85/8.81 cnf(p70, plain, ($false | ~spl14 | ~spl15), inference(resolution, [status(thm)], [p53, p44])).
% 64.85/8.81 cnf(sct1, plain, (~spl14 | ~spl15), inference(avatar_contradiction_clause, [status(thm)], [p70])).
% 64.85/8.81 fof(f7, axiom, ! [X] : ( cowlThing(X) & ~ cowlNothing(X) ), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_0)).
% 64.85/8.81 fof(f7_nnf, plain, ! [X] : ((cowlThing(X) & ~(cowlNothing(X)))), inference(nnf_transformation, [status(thm)], [f7])).
% 64.85/8.81 fof(f7_sk, plain, ! [X] : ((cowlThing(X) & ~(cowlNothing(X)))), inference(skolemisation, [status(esa)], [f7_nnf])).
% 64.85/8.81 cnf(c7, plain, cowlThing(X0), inference(cnf_transformation, [status(esa)], [f7_sk])).
% 64.85/8.81 fof(sdef0, definition, (spl0 <=> (~cowlThing(sk0))), introduced(definition, [new_symbols(naming, [spl0])], [avatar_definition])).
% 64.85/8.81 cnf(p22, plain, (~cowlThing(sk0) | ~spl0), inference(avatar_component_clause, [status(thm)], [sdef0])).
% 64.85/8.81 cnf(p71, plain, ($false | ~spl0), inference(resolution, [status(thm)], [c7, p22])).
% 64.85/8.81 cnf(sct2, plain, (~spl0), inference(avatar_contradiction_clause, [status(thm)], [p71])).
% 64.85/8.81 fof(sdef6, definition, (spl6 <=> (~cowlThing(ia))), introduced(definition, [new_symbols(naming, [spl6])], [avatar_definition])).
% 64.85/8.81 cnf(p28, plain, (~cowlThing(ia) | ~spl6), inference(avatar_component_clause, [status(thm)], [sdef6])).
% 64.85/8.81 cnf(p72, plain, ($false | ~spl6), inference(resolution, [status(thm)], [c7, p28])).
% 64.85/8.81 cnf(sct3, plain, (~spl6), inference(avatar_contradiction_clause, [status(thm)], [p72])).
% 64.85/8.81 fof(sdef8, definition, (spl8 <=> (~cowlThing(ib))), introduced(definition, [new_symbols(naming, [spl8])], [avatar_definition])).
% 64.85/8.81 cnf(p30, plain, (~cowlThing(ib) | ~spl8), inference(avatar_component_clause, [status(thm)], [sdef8])).
% 64.85/8.81 cnf(p73, plain, ($false | ~spl8), inference(resolution, [status(thm)], [c7, p30])).
% 64.85/8.81 cnf(sct4, plain, (~spl8), inference(avatar_contradiction_clause, [status(thm)], [p73])).
% 64.85/8.81 fof(sdef9, definition, (spl9 <=> (~cowlThing(ic))), introduced(definition, [new_symbols(naming, [spl9])], [avatar_definition])).
% 64.85/8.81 cnf(p31, plain, (~cowlThing(ic) | ~spl9), inference(avatar_component_clause, [status(thm)], [sdef9])).
% 64.85/8.81 cnf(p74, plain, ($false | ~spl9), inference(resolution, [status(thm)], [c7, p31])).
% 64.85/8.81 cnf(sct5, plain, (~spl9), inference(avatar_contradiction_clause, [status(thm)], [p74])).
% 64.85/8.81 cnf(c8, plain, ~cowlNothing(X0), inference(cnf_transformation, [status(esa)], [f7_sk])).
% 64.85/8.81 fof(sdef1, definition, (spl1 <=> (cowlNothing(sk0))), introduced(definition, [new_symbols(naming, [spl1])], [avatar_definition])).
% 64.85/8.81 cnf(p23, plain, (cowlNothing(sk0) | ~spl1), inference(avatar_component_clause, [status(thm)], [sdef1])).
% 64.85/8.81 cnf(p75, plain, ($false | ~spl1), inference(resolution, [status(thm)], [c8, p23])).
% 64.85/8.81 cnf(sct6, plain, (~spl1), inference(avatar_contradiction_clause, [status(thm)], [p75])).
% 64.85/8.81 fof(f13, axiom, requalityOnA(ia,ia), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_6)).
% 64.85/8.81 fof(f13_nnf, plain, requalityOnA(ia,ia), inference(nnf_transformation, [status(thm)], [f13])).
% 64.85/8.81 cnf(c17, plain, requalityOnA(ia,ia), inference(cnf_transformation, [status(esa)], [f13_nnf])).
% 64.85/8.81 fof(sdef7, definition, (spl7 <=> (~requalityOnA(ia,ia))), introduced(definition, [new_symbols(naming, [spl7])], [avatar_definition])).
% 64.85/8.81 cnf(p29, plain, (~requalityOnA(ia,ia) | ~spl7), inference(avatar_component_clause, [status(thm)], [sdef7])).
% 64.85/8.81 cnf(p76, plain, ($false | ~spl7), inference(resolution, [status(thm)], [c17, p29])).
% 64.85/8.81 cnf(sct7, plain, (~spl7), inference(avatar_contradiction_clause, [status(thm)], [p76])).
% 64.85/8.81 fof(sdef17, definition, (spl17 <=> (ib != ia)), introduced(definition, [new_symbols(naming, [spl17])], [avatar_definition])).
% 64.85/8.81 cnf(p84, plain, (ib != ia | ~spl17), inference(avatar_component_clause, [status(thm)], [sdef17])).
% 64.85/8.81 fof(sdef20, definition, (spl20 <=> (sk3 = ib)), introduced(definition, [new_symbols(naming, [spl20])], [avatar_definition])).
% 64.85/8.81 cnf(p89, plain, (sk3 = ib | ~spl20), inference(avatar_component_clause, [status(thm)], [sdef20])).
% 64.85/8.81 fof(sdef21, definition, (spl21 <=> (sk3 = ia)), introduced(definition, [new_symbols(naming, [spl21])], [avatar_definition])).
% 64.85/8.81 cnf(p90, plain, (sk3 = ia | ~spl21), inference(avatar_component_clause, [status(thm)], [sdef21])).
% 64.85/8.81 cnf(p97, plain, (ib = ia | ~spl20 | ~spl21), inference(superposition, [status(thm)], [p89, p90])).
% 64.85/8.81 cnf(p118, plain, ($false | ~spl17 | ~spl20 | ~spl21), inference(resolution, [status(thm)], [p84, p97])).
% 64.85/8.81 cnf(sct8, plain, (~spl17 | ~spl20 | ~spl21), inference(avatar_contradiction_clause, [status(thm)], [p118])).
% 64.85/8.81 fof(sdef19, definition, (spl19 <=> (ia != ib)), introduced(definition, [new_symbols(naming, [spl19])], [avatar_definition])).
% 64.85/8.81 cnf(p87, plain, (ia != ib | ~spl19), inference(avatar_component_clause, [status(thm)], [sdef19])).
% 64.85/8.81 cnf(p96, plain, (ia = ib | ~spl20 | ~spl21), inference(superposition, [status(thm)], [p90, p89])).
% 64.85/8.81 cnf(p131, plain, ($false | ~spl19 | ~spl20 | ~spl21), inference(resolution, [status(thm)], [p87, p96])).
% 64.85/8.81 cnf(sct9, plain, (~spl19 | ~spl20 | ~spl21), inference(avatar_contradiction_clause, [status(thm)], [p131])).
% 64.85/8.81 fof(sdef25, definition, (spl25 <=> (xsd_integer(ia))), introduced(definition, [new_symbols(naming, [spl25])], [avatar_definition])).
% 64.85/8.81 cnf(p147, plain, (xsd_integer(ia) | ~spl25), inference(avatar_component_clause, [status(thm)], [sdef25])).
% 64.85/8.81 cnf(p152, plain, (xsd_integer(ib) | ~spl20 | ~spl21 | ~spl25), inference(superposition, [status(thm)], [p96, p147])).
% 64.85/8.81 fof(sdef24, definition, (spl24 <=> (~xsd_integer(ib))), introduced(definition, [new_symbols(naming, [spl24])], [avatar_definition])).
% 64.85/8.81 cnf(p146, plain, (~xsd_integer(ib) | ~spl24), inference(avatar_component_clause, [status(thm)], [sdef24])).
% 64.85/8.81 cnf(p162, plain, ($false | ~spl20 | ~spl21 | ~spl24 | ~spl25), inference(resolution, [status(thm)], [p152, p146])).
% 64.85/8.81 cnf(sct10, plain, (~spl20 | ~spl21 | ~spl24 | ~spl25), inference(avatar_contradiction_clause, [status(thm)], [p162])).
% 64.85/8.81 fof(sdef23, definition, (spl23 <=> (sk5 = ia)), introduced(definition, [new_symbols(naming, [spl23])], [avatar_definition])).
% 64.85/8.81 cnf(p93, plain, (sk5 = ia | ~spl23), inference(avatar_component_clause, [status(thm)], [sdef23])).
% 64.85/8.81 fof(sdef22, definition, (spl22 <=> (sk5 = ib)), introduced(definition, [new_symbols(naming, [spl22])], [avatar_definition])).
% 64.85/8.81 cnf(p92, plain, (sk5 = ib | ~spl22), inference(avatar_component_clause, [status(thm)], [sdef22])).
% 64.85/8.81 cnf(p106, plain, (ia = ib | ~spl22 | ~spl23), inference(superposition, [status(thm)], [p93, p92])).
% 64.85/8.81 cnf(p153, plain, (xsd_integer(ib) | ~spl22 | ~spl23 | ~spl25), inference(superposition, [status(thm)], [p106, p147])).
% 64.85/8.81 cnf(p163, plain, ($false | ~spl22 | ~spl23 | ~spl24 | ~spl25), inference(resolution, [status(thm)], [p153, p146])).
% 64.85/8.81 cnf(sct11, plain, (~spl22 | ~spl23 | ~spl24 | ~spl25), inference(avatar_contradiction_clause, [status(thm)], [p163])).
% 64.85/8.81 fof(sdef26, definition, (spl26 <=> (~xsd_string(ib))), introduced(definition, [new_symbols(naming, [spl26])], [avatar_definition])).
% 64.85/8.81 cnf(p149, plain, (~xsd_string(ib) | ~spl26), inference(avatar_component_clause, [status(thm)], [sdef26])).
% 64.85/8.81 fof(f8, axiom, ! [X] : ( xsd_string(X) <=> ~ xsd_integer(X) ), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_1)).
% 64.85/8.81 fof(f8_nnf, plain, ! [X] : (((~(xsd_string(X)) | ~(xsd_integer(X))) & (xsd_string(X) | xsd_integer(X)))), inference(nnf_transformation, [status(thm)], [f8])).
% 64.85/8.81 fof(f8_sk, plain, ! [X] : (((~(xsd_string(X)) | ~(xsd_integer(X))) & (xsd_string(X) | xsd_integer(X)))), inference(skolemisation, [status(esa)], [f8_nnf])).
% 64.85/8.81 cnf(c10, plain, xsd_string(X0) | xsd_integer(X0), inference(cnf_transformation, [status(esa)], [f8_sk])).
% 64.85/8.81 cnf(p157, plain, (xsd_integer(ib) | ~spl26), inference(resolution, [status(thm)], [p149, c10])).
% 64.85/8.81 cnf(p164, plain, ($false | ~spl24 | ~spl26), inference(resolution, [status(thm)], [p157, p146])).
% 64.85/8.81 cnf(sct12, plain, (~spl24 | ~spl26), inference(avatar_contradiction_clause, [status(thm)], [p164])).
% 64.85/8.81 fof(sdef27, definition, (spl27 <=> (xsd_string(ia))), introduced(definition, [new_symbols(naming, [spl27])], [avatar_definition])).
% 64.85/8.81 cnf(p150, plain, (xsd_string(ia) | ~spl27), inference(avatar_component_clause, [status(thm)], [sdef27])).
% 64.85/8.81 cnf(c9, plain, ~xsd_string(X0) | ~xsd_integer(X0), inference(cnf_transformation, [status(esa)], [f8_sk])).
% 64.85/8.81 cnf(p158, plain, (~xsd_integer(ia) | ~spl27), inference(resolution, [status(thm)], [p150, c9])).
% 64.85/8.81 cnf(p166, plain, ($false | ~spl25 | ~spl27), inference(resolution, [status(thm)], [p158, p147])).
% 64.85/8.81 cnf(sct13, plain, (~spl25 | ~spl27), inference(avatar_contradiction_clause, [status(thm)], [p166])).
% 64.85/8.81 cnf(p160, plain, (xsd_string(ib) | ~spl22 | ~spl23 | ~spl27), inference(superposition, [status(thm)], [p106, p150])).
% 64.85/8.81 cnf(p167, plain, ($false | ~spl22 | ~spl23 | ~spl26 | ~spl27), inference(resolution, [status(thm)], [p160, p149])).
% 64.85/8.81 cnf(sct14, plain, (~spl22 | ~spl23 | ~spl26 | ~spl27), inference(avatar_contradiction_clause, [status(thm)], [p167])).
% 64.85/8.81 fof(sdef18, definition, (spl18 <=> (~cA(X0) | X0 = ia)), introduced(definition, [new_symbols(naming, [spl18])], [avatar_definition])).
% 64.85/8.81 cnf(p86, plain, (~cA(X0) | X0 = ia | ~spl18), inference(avatar_component_clause, [status(thm)], [sdef18])).
% 64.85/8.81 fof(f11, axiom, ! [X,Y] : ( requalityOnA(X,Y) => cA(Y) ), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_4)).
% 64.85/8.81 fof(f11_nnf, plain, ! [X,Y] : ((~(requalityOnA(X,Y)) | cA(Y))), inference(nnf_transformation, [status(thm)], [f11])).
% 64.85/8.81 fof(f11_sk, plain, ! [X,Y] : ((~(requalityOnA(X,Y)) | cA(Y))), inference(skolemisation, [status(esa)], [f11_nnf])).
% 64.85/8.81 cnf(c15, plain, ~requalityOnA(X0,X1) | cA(X1), inference(cnf_transformation, [status(esa)], [f11_sk])).
% 64.85/8.81 fof(sdef4, definition, (spl4 <=> (requalityOnA(sk2,sk3))), introduced(definition, [new_symbols(naming, [spl4])], [avatar_definition])).
% 64.85/8.81 cnf(p26, plain, (requalityOnA(sk2,sk3) | ~spl4), inference(avatar_component_clause, [status(thm)], [sdef4])).
% 64.85/8.81 cnf(p80, plain, (cA(sk3) | ~spl4), inference(resolution, [status(thm)], [c15, p26])).
% 64.85/8.81 cnf(p123, plain, (sk3 = ia | ~spl4 | ~spl18), inference(resolution, [status(thm)], [p86, p80])).
% 64.85/8.81 cnf(p134, plain, (ia = ib | ~spl4 | ~spl18 | ~spl20), inference(superposition, [status(thm)], [p123, p89])).
% 64.85/8.81 cnf(p174, plain, (xsd_string(ib) | ~spl4 | ~spl18 | ~spl20 | ~spl27), inference(superposition, [status(thm)], [p134, p150])).
% 64.85/8.81 cnf(p178, plain, ($false | ~spl4 | ~spl18 | ~spl20 | ~spl26 | ~spl27), inference(resolution, [status(thm)], [p174, p149])).
% 64.85/8.81 cnf(sct15, plain, (~spl4 | ~spl18 | ~spl20 | ~spl26 | ~spl27), inference(avatar_contradiction_clause, [status(thm)], [p178])).
% 64.85/8.81 fof(f9, axiom, ! [X] : ( cA(X) <=> ( X = ib | X = ia ) ), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_2)).
% 64.85/8.81 fof(f9_nnf, plain, ! [X] : (((~(cA(X)) | (X = ib | X = ia)) & (cA(X) | (X != ib & X != ia)))), inference(nnf_transformation, [status(thm)], [f9])).
% 64.85/8.81 fof(f9_sk, plain, ! [X] : (((~(cA(X)) | (X = ib | X = ia)) & (cA(X) | (X != ib & X != ia)))), inference(skolemisation, [status(esa)], [f9_nnf])).
% 64.85/8.81 cnf(c12, plain, cA(X0) | X0 != ib, inference(cnf_transformation, [status(esa)], [f9_sk])).
% 64.85/8.81 cnf(p78, plain, cA(ib), inference(equality_resolution, [status(thm)], [c12])).
% 64.85/8.81 cnf(p122, plain, (ib = ia | ~spl18), inference(resolution, [status(thm)], [p86, p78])).
% 64.85/8.81 cnf(p210, plain, ($false | ~spl17 | ~spl18), inference(resolution, [status(thm)], [p122, p84])).
% 64.85/8.81 cnf(sct16, plain, (~spl17 | ~spl18), inference(avatar_contradiction_clause, [status(thm)], [p210])).
% 64.85/8.81 fof(sdef28, definition, (spl28 <=> (~cA(ib))), introduced(definition, [new_symbols(naming, [spl28])], [avatar_definition])).
% 64.85/8.81 cnf(p236, plain, (~cA(ib) | ~spl28), inference(avatar_component_clause, [status(thm)], [sdef28])).
% 64.85/8.81 cnf(p245, plain, ($false | ~spl28), inference(resolution, [status(thm)], [p236, p78])).
% 64.85/8.81 cnf(sct17, plain, (~spl28), inference(avatar_contradiction_clause, [status(thm)], [p245])).
% 64.85/8.81 fof(sdef31, definition, (spl31 <=> (xsd_string(sk4))), introduced(definition, [new_symbols(naming, [spl31])], [avatar_definition])).
% 64.85/8.81 cnf(p244, plain, (xsd_string(sk4) | ~spl31), inference(avatar_component_clause, [status(thm)], [sdef31])).
% 64.85/8.81 cnf(p251, plain, (~xsd_integer(sk4) | ~spl31), inference(resolution, [status(thm)], [p244, c9])).
% 64.85/8.81 fof(sdef30, definition, (spl30 <=> (xsd_integer(sk4))), introduced(definition, [new_symbols(naming, [spl30])], [avatar_definition])).
% 64.85/8.81 cnf(p242, plain, (xsd_integer(sk4) | ~spl30), inference(avatar_component_clause, [status(thm)], [sdef30])).
% 64.85/8.81 cnf(p252, plain, ($false | ~spl30 | ~spl31), inference(resolution, [status(thm)], [p251, p242])).
% 64.85/8.81 cnf(sct18, plain, (~spl30 | ~spl31), inference(avatar_contradiction_clause, [status(thm)], [p252])).
% 64.85/8.81 cnf(p94, plain, (requalityOnA(sk2,ib) | ~spl4 | ~spl20), inference(superposition, [status(thm)], [p89, p26])).
% 64.85/8.81 fof(f10, axiom, ! [X,Y,Z] : ( ( requalityOnA(Y,X) & requalityOnA(Z,X) ) => Y = Z ), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_3)).
% 64.85/8.81 fof(f10_nnf, plain, ! [X,Y,Z] : (((~(requalityOnA(Y,X)) | ~(requalityOnA(Z,X))) | Y = Z)), inference(nnf_transformation, [status(thm)], [f10])).
% 64.85/8.81 fof(f10_sk, plain, ! [Y,X,Z] : (((~(requalityOnA(Y,X)) | ~(requalityOnA(Z,X))) | Y = Z)), inference(skolemisation, [status(esa)], [f10_nnf])).
% 64.85/8.81 cnf(c14, plain, ~requalityOnA(X1,X0) | ~requalityOnA(X2,X0) | X1 = X2, inference(cnf_transformation, [status(esa)], [f10_sk])).
% 64.85/8.81 cnf(p108, plain, (~requalityOnA(X0,ib) | sk2 = X0 | ~spl4 | ~spl20), inference(resolution, [status(thm)], [p94, c14])).
% 64.85/8.81 fof(f15, axiom, requalityOnA(ib,ib), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_8)).
% 64.85/8.81 fof(f15_nnf, plain, requalityOnA(ib,ib), inference(nnf_transformation, [status(thm)], [f15])).
% 64.85/8.81 cnf(c19, plain, requalityOnA(ib,ib), inference(cnf_transformation, [status(esa)], [f15_nnf])).
% 64.85/8.81 cnf(p176, plain, (sk2 = ib | ~spl4 | ~spl20), inference(resolution, [status(thm)], [p108, c19])).
% 64.85/8.81 fof(sdef12, definition, (spl12 <=> (sk2 != ib)), introduced(definition, [new_symbols(naming, [spl12])], [avatar_definition])).
% 64.85/8.81 cnf(p38, plain, (sk2 != ib | ~spl12), inference(avatar_component_clause, [status(thm)], [sdef12])).
% 64.85/8.81 cnf(p254, plain, ($false | ~spl4 | ~spl12 | ~spl20), inference(resolution, [status(thm)], [p176, p38])).
% 64.85/8.81 cnf(sct19, plain, (~spl4 | ~spl12 | ~spl20), inference(avatar_contradiction_clause, [status(thm)], [p254])).
% 64.85/8.81 cnf(p212, plain, (ia = ib | ~spl4 | ~spl18), inference(superposition, [status(thm)], [p122, p123])).
% 64.85/8.81 cnf(p255, plain, ($false | ~spl4 | ~spl18 | ~spl19), inference(resolution, [status(thm)], [p212, p87])).
% 64.85/8.81 cnf(sct20, plain, (~spl4 | ~spl18 | ~spl19), inference(avatar_contradiction_clause, [status(thm)], [p255])).
% 64.85/8.81 cnf(p133, plain, (requalityOnA(sk2,ia) | ~spl4 | ~spl18), inference(superposition, [status(thm)], [p123, p26])).
% 64.85/8.81 cnf(p102, plain, ~requalityOnA(X0,ia) | ia = X0, inference(resolution, [status(thm)], [c14, c17])).
% 64.85/8.81 cnf(p172, plain, (ia = sk2 | ~spl4 | ~spl18), inference(resolution, [status(thm)], [p133, p102])).
% 64.85/8.81 cnf(p216, plain, (ib = sk2 | ~spl4 | ~spl18), inference(demodulation, [status(thm)], [p212, p172])).
% 64.85/8.81 fof(sdef35, definition, (spl35 <=> (xsd_integer(sk2))), introduced(definition, [new_symbols(naming, [spl35])], [avatar_definition])).
% 64.85/8.81 cnf(p264, plain, (xsd_integer(sk2) | ~spl35), inference(avatar_component_clause, [status(thm)], [sdef35])).
% 64.85/8.81 cnf(p272, plain, (xsd_integer(ib) | ~spl4 | ~spl18 | ~spl35), inference(superposition, [status(thm)], [p216, p264])).
% 64.85/8.81 cnf(p275, plain, ($false | ~spl4 | ~spl18 | ~spl24 | ~spl35), inference(resolution, [status(thm)], [p272, p146])).
% 64.85/8.81 cnf(sct21, plain, (~spl4 | ~spl18 | ~spl24 | ~spl35), inference(avatar_contradiction_clause, [status(thm)], [p275])).
% 64.85/8.81 fof(sdef36, definition, (spl36 <=> (xsd_string(sk2))), introduced(definition, [new_symbols(naming, [spl36])], [avatar_definition])).
% 64.85/8.81 cnf(p266, plain, (xsd_string(sk2) | ~spl36), inference(avatar_component_clause, [status(thm)], [sdef36])).
% 64.85/8.81 cnf(p273, plain, (~xsd_integer(sk2) | ~spl36), inference(resolution, [status(thm)], [p266, c9])).
% 64.85/8.81 cnf(p282, plain, ($false | ~spl35 | ~spl36), inference(resolution, [status(thm)], [p273, p264])).
% 64.85/8.81 cnf(sct22, plain, (~spl35 | ~spl36), inference(avatar_contradiction_clause, [status(thm)], [p282])).
% 64.85/8.81 cnf(p276, plain, (~xsd_integer(sk1) | ~spl2), inference(resolution, [status(thm)], [p24, c9])).
% 64.85/8.81 cnf(p283, plain, ($false | ~spl2 | ~spl15), inference(resolution, [status(thm)], [p276, p53])).
% 64.85/8.81 cnf(sct23, plain, (~spl2 | ~spl15), inference(avatar_contradiction_clause, [status(thm)], [p283])).
% 64.85/8.81 cnf(p77, plain, (xsd_integer(sk1) | ~spl3), inference(resolution, [status(thm)], [c10, p25])).
% 64.85/8.81 cnf(p284, plain, ($false | ~spl3 | ~spl14), inference(resolution, [status(thm)], [p44, p77])).
% 64.85/8.81 cnf(sct24, plain, (~spl3 | ~spl14), inference(avatar_contradiction_clause, [status(thm)], [p284])).
% 64.85/8.81 fof(sdef16, definition, (spl16 <=> (~cA(X0) | X0 = ib)), introduced(definition, [new_symbols(naming, [spl16])], [avatar_definition])).
% 64.85/8.81 cnf(p83, plain, (~cA(X0) | X0 = ib | ~spl16), inference(avatar_component_clause, [status(thm)], [sdef16])).
% 64.85/8.81 cnf(p112, plain, (sk3 = ib | ~spl4 | ~spl16), inference(resolution, [status(thm)], [p83, p80])).
% 64.85/8.81 cnf(p100, plain, (~requalityOnA(X0,sk3) | sk2 = X0 | ~spl4), inference(resolution, [status(thm)], [c14, p26])).
% 64.85/8.81 cnf(p138, plain, (~requalityOnA(X0,ib) | sk2 = X0 | ~spl4 | ~spl16), inference(superposition, [status(thm)], [p112, p100])).
% 64.85/8.81 cnf(p234, plain, (sk2 = ib | ~spl4 | ~spl16), inference(resolution, [status(thm)], [p138, c19])).
% 64.85/8.81 cnf(p294, plain, ($false | ~spl4 | ~spl12 | ~spl16), inference(resolution, [status(thm)], [p234, p38])).
% 64.85/8.81 cnf(sct25, plain, (~spl4 | ~spl12 | ~spl16), inference(avatar_contradiction_clause, [status(thm)], [p294])).
% 64.85/8.81 fof(sdef5, definition, (spl5 <=> (requalityOnA(sk4,sk5))), introduced(definition, [new_symbols(naming, [spl5])], [avatar_definition])).
% 64.85/8.81 cnf(p27, plain, (requalityOnA(sk4,sk5) | ~spl5), inference(avatar_component_clause, [status(thm)], [sdef5])).
% 64.85/8.81 cnf(p81, plain, (cA(sk5) | ~spl5), inference(resolution, [status(thm)], [c15, p27])).
% 64.85/8.81 cnf(p113, plain, (sk5 = ib | ~spl5 | ~spl16), inference(resolution, [status(thm)], [p83, p81])).
% 64.85/8.81 cnf(p127, plain, (requalityOnA(sk4,ib) | ~spl5 | ~spl16), inference(superposition, [status(thm)], [p113, p27])).
% 64.85/8.81 cnf(p103, plain, ~requalityOnA(X0,ib) | ib = X0, inference(resolution, [status(thm)], [c14, c19])).
% 64.85/8.81 cnf(p171, plain, (ib = sk4 | ~spl5 | ~spl16), inference(resolution, [status(thm)], [p127, p103])).
% 64.85/8.81 fof(sdef10, definition, (spl10 <=> (~requalityOnA(sk5,sk4))), introduced(definition, [new_symbols(naming, [spl10])], [avatar_definition])).
% 64.85/8.81 cnf(p33, plain, (~requalityOnA(sk5,sk4) | ~spl10), inference(avatar_component_clause, [status(thm)], [sdef10])).
% 64.85/8.81 cnf(p238, plain, (~requalityOnA(ib,ib) | ~spl5 | ~spl10 | ~spl16), inference(superposition, [status(thm)], [p171, p33])).
% 64.85/8.81 cnf(p315, plain, ($false | ~spl5 | ~spl10 | ~spl16), inference(resolution, [status(thm)], [p238, c19])).
% 64.85/8.81 cnf(sct26, plain, (~spl5 | ~spl10 | ~spl16), inference(avatar_contradiction_clause, [status(thm)], [p315])).
% 64.85/8.81 cnf(p98, plain, (requalityOnA(sk4,ib) | ~spl5 | ~spl22), inference(superposition, [status(thm)], [p92, p27])).
% 64.85/8.81 cnf(p114, plain, (~requalityOnA(X0,ib) | sk4 = X0 | ~spl5 | ~spl22), inference(resolution, [status(thm)], [p98, c14])).
% 64.85/8.81 cnf(p185, plain, (sk4 = ib | ~spl5 | ~spl22), inference(resolution, [status(thm)], [p114, c19])).
% 64.85/8.81 cnf(p305, plain, (xsd_string(ib) | ~spl5 | ~spl22 | ~spl31), inference(superposition, [status(thm)], [p185, p244])).
% 64.85/8.81 cnf(p316, plain, ($false | ~spl5 | ~spl22 | ~spl26 | ~spl31), inference(resolution, [status(thm)], [p149, p305])).
% 64.85/8.81 cnf(sct27, plain, (~spl5 | ~spl22 | ~spl26 | ~spl31), inference(avatar_contradiction_clause, [status(thm)], [p316])).
% 64.85/8.81 cnf(p327, plain, ($false | ~spl19 | ~spl22 | ~spl23), inference(resolution, [status(thm)], [p106, p87])).
% 64.85/8.81 cnf(sct28, plain, (~spl19 | ~spl22 | ~spl23), inference(avatar_contradiction_clause, [status(thm)], [p327])).
% 64.85/8.81 fof(sdef38, definition, (spl38 <=> (sk2 = ia)), introduced(definition, [new_symbols(naming, [spl38])], [avatar_definition])).
% 64.85/8.81 cnf(p269, plain, (sk2 = ia | ~spl38), inference(avatar_component_clause, [status(thm)], [sdef38])).
% 64.85/8.81 fof(sdef11, definition, (spl11 <=> (sk2 != ia)), introduced(definition, [new_symbols(naming, [spl11])], [avatar_definition])).
% 64.85/8.81 cnf(p35, plain, (sk2 != ia | ~spl11), inference(avatar_component_clause, [status(thm)], [sdef11])).
% 64.85/8.81 cnf(p346, plain, ($false | ~spl11 | ~spl38), inference(resolution, [status(thm)], [p269, p35])).
% 64.85/8.81 cnf(sct29, plain, (~spl11 | ~spl38), inference(avatar_contradiction_clause, [status(thm)], [p346])).
% 64.85/8.81 cnf(p304, plain, (~requalityOnA(ib,ib) | ~spl5 | ~spl10 | ~spl22), inference(superposition, [status(thm)], [p185, p33])).
% 64.85/8.81 cnf(p355, plain, ($false | ~spl5 | ~spl10 | ~spl22), inference(resolution, [status(thm)], [p304, c19])).
% 64.85/8.81 cnf(sct30, plain, (~spl5 | ~spl10 | ~spl22), inference(avatar_contradiction_clause, [status(thm)], [p355])).
% 64.85/8.81 fof(sdef32, definition, (spl32 <=> (sk4 = ib)), introduced(definition, [new_symbols(naming, [spl32])], [avatar_definition])).
% 64.85/8.81 cnf(p247, plain, (sk4 = ib | ~spl32), inference(avatar_component_clause, [status(thm)], [sdef32])).
% 64.85/8.81 cnf(p321, plain, (xsd_string(ib) | ~spl31 | ~spl32), inference(superposition, [status(thm)], [p247, p244])).
% 64.85/8.81 cnf(p356, plain, ($false | ~spl26 | ~spl31 | ~spl32), inference(resolution, [status(thm)], [p149, p321])).
% 64.85/8.81 cnf(sct31, plain, (~spl26 | ~spl31 | ~spl32), inference(avatar_contradiction_clause, [status(thm)], [p356])).
% 64.85/8.81 cnf(p104, plain, (requalityOnA(sk4,ia) | ~spl5 | ~spl23), inference(superposition, [status(thm)], [p93, p27])).
% 64.85/8.81 cnf(p115, plain, (~requalityOnA(X0,ia) | sk4 = X0 | ~spl5 | ~spl23), inference(resolution, [status(thm)], [p104, c14])).
% 64.85/8.81 cnf(p189, plain, (sk4 = ia | ~spl5 | ~spl23), inference(resolution, [status(thm)], [p115, c17])).
% 64.85/8.81 cnf(p308, plain, (~requalityOnA(ia,ia) | ~spl5 | ~spl10 | ~spl23), inference(superposition, [status(thm)], [p189, p33])).
% 64.85/8.81 cnf(p360, plain, ($false | ~spl5 | ~spl10 | ~spl23), inference(resolution, [status(thm)], [p308, c17])).
% 64.85/8.81 cnf(sct32, plain, (~spl5 | ~spl10 | ~spl23), inference(avatar_contradiction_clause, [status(thm)], [p360])).
% 64.85/8.81 fof(sdef37, definition, (spl37 <=> (sk2 = ib)), introduced(definition, [new_symbols(naming, [spl37])], [avatar_definition])).
% 64.85/8.81 cnf(p268, plain, (sk2 = ib | ~spl37), inference(avatar_component_clause, [status(thm)], [sdef37])).
% 64.85/8.81 cnf(p361, plain, ($false | ~spl12 | ~spl37), inference(resolution, [status(thm)], [p38, p268])).
% 64.85/8.81 cnf(sct33, plain, (~spl12 | ~spl37), inference(avatar_contradiction_clause, [status(thm)], [p361])).
% 64.85/8.81 cnf(p95, plain, (requalityOnA(sk2,ia) | ~spl4 | ~spl21), inference(superposition, [status(thm)], [p90, p26])).
% 64.85/8.81 cnf(p109, plain, (~requalityOnA(X0,ia) | sk2 = X0 | ~spl4 | ~spl21), inference(resolution, [status(thm)], [p95, c14])).
% 64.85/8.81 cnf(p287, plain, (sk2 = ia | ~spl4 | ~spl21), inference(resolution, [status(thm)], [p109, c17])).
% 64.85/8.81 cnf(p365, plain, ($false | ~spl4 | ~spl11 | ~spl21), inference(resolution, [status(thm)], [p287, p35])).
% 64.85/8.81 cnf(sct34, plain, (~spl4 | ~spl11 | ~spl21), inference(avatar_contradiction_clause, [status(thm)], [p365])).
% 64.85/8.81 fof(f17, conjecture, ( ! [X] : ( cowlThing(X) & ~ cowlNothing(X) ) & ! [X] : ( xsd_string(X) <=> ~ xsd_integer(X) ) & ! [X,Y] : ( requalityOnA(X,Y) => ( X = ia | X = ib | X = ic ) ) & ! [X,Y] : ( requalityOnA(X,Y) => requalityOnA(Y,X) ) & cowlThing(ia) & requalityOnA(ia,ia) & cowlThing(ib) & cowlThing(ic) ), file('/export/starexec/sandbox/benchmark/theBenchmark.p', the_axiom)).
% 64.85/8.81 fof(f17_neg, negated_conjecture, ~(( ! [X] : ( cowlThing(X) & ~ cowlNothing(X) ) & ! [X] : ( xsd_string(X) <=> ~ xsd_integer(X) ) & ! [X,Y] : ( requalityOnA(X,Y) => ( X = ia | X = ib | X = ic ) ) & ! [X,Y] : ( requalityOnA(X,Y) => requalityOnA(Y,X) ) & cowlThing(ia) & requalityOnA(ia,ia) & cowlThing(ib) & cowlThing(ic) )), inference(negated_conjecture, [status(cth)], [f17])).
% 64.85/8.81 fof(f17_nnf, plain, (((((((? [X] : ((~(cowlThing(X)) | cowlNothing(X))) | ? [X] : (((xsd_string(X) & xsd_integer(X)) | (~(xsd_string(X)) & ~(xsd_integer(X)))))) | ? [X,Y] : ((requalityOnA(X,Y) & ((X != ia & X != ib) & X != ic)))) | ? [X,Y] : ((requalityOnA(X,Y) & ~(requalityOnA(Y,X))))) | ~(cowlThing(ia))) | ~(requalityOnA(ia,ia))) | ~(cowlThing(ib))) | ~(cowlThing(ic))), inference(nnf_transformation, [status(thm)], [f17_neg])).
% 64.85/8.81 fof(f17_sk, plain, ((((((((~(cowlThing(sk0)) | cowlNothing(sk0)) | ((xsd_string(sk1) & xsd_integer(sk1)) | (~(xsd_string(sk1)) & ~(xsd_integer(sk1))))) | (requalityOnA(sk2,sk3) & ((sk2 != ia & sk2 != ib) & sk2 != ic))) | (requalityOnA(sk4,sk5) & ~(requalityOnA(sk5,sk4)))) | ~(cowlThing(ia))) | ~(requalityOnA(ia,ia))) | ~(cowlThing(ib))) | ~(cowlThing(ic))), inference(skolemisation, [status(esa), new_symbols(skolem, [sk0,sk1,sk2,sk3,sk4,sk5])], [f17_nnf])).
% 64.85/8.81 cnf(c21, plain, ~cowlThing(sk0) | cowlNothing(sk0) | xsd_string(sk1) | ~xsd_string(sk1) | requalityOnA(sk2,sk3) | requalityOnA(sk4,sk5) | ~cowlThing(ia) | ~requalityOnA(ia,ia) | ~cowlThing(ib) | ~cowlThing(ic), inference(cnf_transformation, [status(esa)], [f17_sk])).
% 64.85/8.81 cnf(ssp0, plain, (spl0 | spl1 | spl2 | spl3 | spl4 | spl5 | spl6 | spl7 | spl8 | spl9), inference(avatar_split_clause, [status(thm)], [c21, sdef0, sdef1, sdef2, sdef3, sdef4, sdef5, sdef6, sdef7, sdef8, sdef9])).
% 64.85/8.81 cnf(c22, plain, ~cowlThing(sk0) | cowlNothing(sk0) | xsd_string(sk1) | ~xsd_string(sk1) | requalityOnA(sk2,sk3) | ~requalityOnA(sk5,sk4) | ~cowlThing(ia) | ~requalityOnA(ia,ia) | ~cowlThing(ib) | ~cowlThing(ic), inference(cnf_transformation, [status(esa)], [f17_sk])).
% 64.85/8.81 cnf(ssp1, plain, (spl0 | spl1 | spl2 | spl3 | spl4 | spl6 | spl7 | spl8 | spl9 | spl10), inference(avatar_split_clause, [status(thm)], [c22, sdef0, sdef1, sdef2, sdef3, sdef4, sdef6, sdef7, sdef8, sdef9, sdef10])).
% 64.85/8.81 cnf(c23, plain, ~cowlThing(sk0) | cowlNothing(sk0) | xsd_string(sk1) | ~xsd_string(sk1) | sk2 != ia | requalityOnA(sk4,sk5) | ~cowlThing(ia) | ~requalityOnA(ia,ia) | ~cowlThing(ib) | ~cowlThing(ic), inference(cnf_transformation, [status(esa)], [f17_sk])).
% 64.85/8.81 cnf(ssp2, plain, (spl0 | spl1 | spl2 | spl3 | spl5 | spl6 | spl7 | spl8 | spl9 | spl11), inference(avatar_split_clause, [status(thm)], [c23, sdef0, sdef1, sdef2, sdef3, sdef5, sdef6, sdef7, sdef8, sdef9, sdef11])).
% 64.85/8.81 cnf(c24, plain, ~cowlThing(sk0) | cowlNothing(sk0) | xsd_string(sk1) | ~xsd_string(sk1) | sk2 != ia | ~requalityOnA(sk5,sk4) | ~cowlThing(ia) | ~requalityOnA(ia,ia) | ~cowlThing(ib) | ~cowlThing(ic), inference(cnf_transformation, [status(esa)], [f17_sk])).
% 64.85/8.81 cnf(ssp3, plain, (spl0 | spl1 | spl2 | spl3 | spl6 | spl7 | spl8 | spl9 | spl10 | spl11), inference(avatar_split_clause, [status(thm)], [c24, sdef0, sdef1, sdef2, sdef3, sdef6, sdef7, sdef8, sdef9, sdef10, sdef11])).
% 64.85/8.81 cnf(c25, plain, ~cowlThing(sk0) | cowlNothing(sk0) | xsd_string(sk1) | ~xsd_string(sk1) | sk2 != ib | requalityOnA(sk4,sk5) | ~cowlThing(ia) | ~requalityOnA(ia,ia) | ~cowlThing(ib) | ~cowlThing(ic), inference(cnf_transformation, [status(esa)], [f17_sk])).
% 64.85/8.81 cnf(ssp4, plain, (spl0 | spl1 | spl2 | spl3 | spl5 | spl6 | spl7 | spl8 | spl9 | spl12), inference(avatar_split_clause, [status(thm)], [c25, sdef0, sdef1, sdef2, sdef3, sdef5, sdef6, sdef7, sdef8, sdef9, sdef12])).
% 64.85/8.81 cnf(c26, plain, ~cowlThing(sk0) | cowlNothing(sk0) | xsd_string(sk1) | ~xsd_string(sk1) | sk2 != ib | ~requalityOnA(sk5,sk4) | ~cowlThing(ia) | ~requalityOnA(ia,ia) | ~cowlThing(ib) | ~cowlThing(ic), inference(cnf_transformation, [status(esa)], [f17_sk])).
% 64.85/8.81 cnf(ssp5, plain, (spl0 | spl1 | spl2 | spl3 | spl6 | spl7 | spl8 | spl9 | spl10 | spl12), inference(avatar_split_clause, [status(thm)], [c26, sdef0, sdef1, sdef2, sdef3, sdef6, sdef7, sdef8, sdef9, sdef10, sdef12])).
% 64.85/8.81 cnf(c27, plain, ~cowlThing(sk0) | cowlNothing(sk0) | xsd_string(sk1) | ~xsd_string(sk1) | sk2 != ic | requalityOnA(sk4,sk5) | ~cowlThing(ia) | ~requalityOnA(ia,ia) | ~cowlThing(ib) | ~cowlThing(ic), inference(cnf_transformation, [status(esa)], [f17_sk])).
% 64.85/8.81 fof(sdef13, definition, (spl13 <=> (sk2 != ic)), introduced(definition, [new_symbols(naming, [spl13])], [avatar_definition])).
% 64.85/8.81 cnf(ssp6, plain, (spl0 | spl1 | spl2 | spl3 | spl5 | spl6 | spl7 | spl8 | spl9 | spl13), inference(avatar_split_clause, [status(thm)], [c27, sdef0, sdef1, sdef2, sdef3, sdef5, sdef6, sdef7, sdef8, sdef9, sdef13])).
% 64.85/8.81 cnf(c28, plain, ~cowlThing(sk0) | cowlNothing(sk0) | xsd_string(sk1) | ~xsd_string(sk1) | sk2 != ic | ~requalityOnA(sk5,sk4) | ~cowlThing(ia) | ~requalityOnA(ia,ia) | ~cowlThing(ib) | ~cowlThing(ic), inference(cnf_transformation, [status(esa)], [f17_sk])).
% 64.85/8.81 cnf(ssp7, plain, (spl0 | spl1 | spl2 | spl3 | spl6 | spl7 | spl8 | spl9 | spl10 | spl13), inference(avatar_split_clause, [status(thm)], [c28, sdef0, sdef1, sdef2, sdef3, sdef6, sdef7, sdef8, sdef9, sdef10, sdef13])).
% 64.85/8.81 cnf(c29, plain, ~cowlThing(sk0) | cowlNothing(sk0) | xsd_string(sk1) | ~xsd_integer(sk1) | requalityOnA(sk2,sk3) | requalityOnA(sk4,sk5) | ~cowlThing(ia) | ~requalityOnA(ia,ia) | ~cowlThing(ib) | ~cowlThing(ic), inference(cnf_transformation, [status(esa)], [f17_sk])).
% 64.85/8.81 cnf(ssp8, plain, (spl0 | spl1 | spl2 | spl4 | spl5 | spl6 | spl7 | spl8 | spl9 | spl14), inference(avatar_split_clause, [status(thm)], [c29, sdef0, sdef1, sdef2, sdef4, sdef5, sdef6, sdef7, sdef8, sdef9, sdef14])).
% 64.85/8.81 cnf(c30, plain, ~cowlThing(sk0) | cowlNothing(sk0) | xsd_string(sk1) | ~xsd_integer(sk1) | requalityOnA(sk2,sk3) | ~requalityOnA(sk5,sk4) | ~cowlThing(ia) | ~requalityOnA(ia,ia) | ~cowlThing(ib) | ~cowlThing(ic), inference(cnf_transformation, [status(esa)], [f17_sk])).
% 64.85/8.81 cnf(ssp9, plain, (spl0 | spl1 | spl2 | spl4 | spl6 | spl7 | spl8 | spl9 | spl10 | spl14), inference(avatar_split_clause, [status(thm)], [c30, sdef0, sdef1, sdef2, sdef4, sdef6, sdef7, sdef8, sdef9, sdef10, sdef14])).
% 64.85/8.81 cnf(c31, plain, ~cowlThing(sk0) | cowlNothing(sk0) | xsd_string(sk1) | ~xsd_integer(sk1) | sk2 != ia | requalityOnA(sk4,sk5) | ~cowlThing(ia) | ~requalityOnA(ia,ia) | ~cowlThing(ib) | ~cowlThing(ic), inference(cnf_transformation, [status(esa)], [f17_sk])).
% 64.85/8.81 cnf(ssp10, plain, (spl0 | spl1 | spl2 | spl5 | spl6 | spl7 | spl8 | spl9 | spl11 | spl14), inference(avatar_split_clause, [status(thm)], [c31, sdef0, sdef1, sdef2, sdef5, sdef6, sdef7, sdef8, sdef9, sdef11, sdef14])).
% 64.85/8.81 cnf(c32, plain, ~cowlThing(sk0) | cowlNothing(sk0) | xsd_string(sk1) | ~xsd_integer(sk1) | sk2 != ia | ~requalityOnA(sk5,sk4) | ~cowlThing(ia) | ~requalityOnA(ia,ia) | ~cowlThing(ib) | ~cowlThing(ic), inference(cnf_transformation, [status(esa)], [f17_sk])).
% 64.85/8.81 cnf(ssp11, plain, (spl0 | spl1 | spl2 | spl6 | spl7 | spl8 | spl9 | spl10 | spl11 | spl14), inference(avatar_split_clause, [status(thm)], [c32, sdef0, sdef1, sdef2, sdef6, sdef7, sdef8, sdef9, sdef10, sdef11, sdef14])).
% 64.85/8.81 cnf(c33, plain, ~cowlThing(sk0) | cowlNothing(sk0) | xsd_string(sk1) | ~xsd_integer(sk1) | sk2 != ib | requalityOnA(sk4,sk5) | ~cowlThing(ia) | ~requalityOnA(ia,ia) | ~cowlThing(ib) | ~cowlThing(ic), inference(cnf_transformation, [status(esa)], [f17_sk])).
% 64.85/8.81 cnf(ssp12, plain, (spl0 | spl1 | spl2 | spl5 | spl6 | spl7 | spl8 | spl9 | spl12 | spl14), inference(avatar_split_clause, [status(thm)], [c33, sdef0, sdef1, sdef2, sdef5, sdef6, sdef7, sdef8, sdef9, sdef12, sdef14])).
% 64.85/8.81 cnf(c34, plain, ~cowlThing(sk0) | cowlNothing(sk0) | xsd_string(sk1) | ~xsd_integer(sk1) | sk2 != ib | ~requalityOnA(sk5,sk4) | ~cowlThing(ia) | ~requalityOnA(ia,ia) | ~cowlThing(ib) | ~cowlThing(ic), inference(cnf_transformation, [status(esa)], [f17_sk])).
% 64.85/8.81 cnf(ssp13, plain, (spl0 | spl1 | spl2 | spl6 | spl7 | spl8 | spl9 | spl10 | spl12 | spl14), inference(avatar_split_clause, [status(thm)], [c34, sdef0, sdef1, sdef2, sdef6, sdef7, sdef8, sdef9, sdef10, sdef12, sdef14])).
% 64.85/8.81 cnf(c35, plain, ~cowlThing(sk0) | cowlNothing(sk0) | xsd_string(sk1) | ~xsd_integer(sk1) | sk2 != ic | requalityOnA(sk4,sk5) | ~cowlThing(ia) | ~requalityOnA(ia,ia) | ~cowlThing(ib) | ~cowlThing(ic), inference(cnf_transformation, [status(esa)], [f17_sk])).
% 64.85/8.81 cnf(ssp14, plain, (spl0 | spl1 | spl2 | spl5 | spl6 | spl7 | spl8 | spl9 | spl13 | spl14), inference(avatar_split_clause, [status(thm)], [c35, sdef0, sdef1, sdef2, sdef5, sdef6, sdef7, sdef8, sdef9, sdef13, sdef14])).
% 64.85/8.81 cnf(c36, plain, ~cowlThing(sk0) | cowlNothing(sk0) | xsd_string(sk1) | ~xsd_integer(sk1) | sk2 != ic | ~requalityOnA(sk5,sk4) | ~cowlThing(ia) | ~requalityOnA(ia,ia) | ~cowlThing(ib) | ~cowlThing(ic), inference(cnf_transformation, [status(esa)], [f17_sk])).
% 64.85/8.81 cnf(ssp15, plain, (spl0 | spl1 | spl2 | spl6 | spl7 | spl8 | spl9 | spl10 | spl13 | spl14), inference(avatar_split_clause, [status(thm)], [c36, sdef0, sdef1, sdef2, sdef6, sdef7, sdef8, sdef9, sdef10, sdef13, sdef14])).
% 64.85/8.81 cnf(c37, plain, ~cowlThing(sk0) | cowlNothing(sk0) | xsd_integer(sk1) | ~xsd_string(sk1) | requalityOnA(sk2,sk3) | requalityOnA(sk4,sk5) | ~cowlThing(ia) | ~requalityOnA(ia,ia) | ~cowlThing(ib) | ~cowlThing(ic), inference(cnf_transformation, [status(esa)], [f17_sk])).
% 64.85/8.81 cnf(ssp16, plain, (spl0 | spl1 | spl3 | spl4 | spl5 | spl6 | spl7 | spl8 | spl9 | spl15), inference(avatar_split_clause, [status(thm)], [c37, sdef0, sdef1, sdef3, sdef4, sdef5, sdef6, sdef7, sdef8, sdef9, sdef15])).
% 64.85/8.81 cnf(c38, plain, ~cowlThing(sk0) | cowlNothing(sk0) | xsd_integer(sk1) | ~xsd_string(sk1) | requalityOnA(sk2,sk3) | ~requalityOnA(sk5,sk4) | ~cowlThing(ia) | ~requalityOnA(ia,ia) | ~cowlThing(ib) | ~cowlThing(ic), inference(cnf_transformation, [status(esa)], [f17_sk])).
% 64.85/8.81 cnf(ssp17, plain, (spl0 | spl1 | spl3 | spl4 | spl6 | spl7 | spl8 | spl9 | spl10 | spl15), inference(avatar_split_clause, [status(thm)], [c38, sdef0, sdef1, sdef3, sdef4, sdef6, sdef7, sdef8, sdef9, sdef10, sdef15])).
% 64.85/8.81 cnf(c39, plain, ~cowlThing(sk0) | cowlNothing(sk0) | xsd_integer(sk1) | ~xsd_string(sk1) | sk2 != ia | requalityOnA(sk4,sk5) | ~cowlThing(ia) | ~requalityOnA(ia,ia) | ~cowlThing(ib) | ~cowlThing(ic), inference(cnf_transformation, [status(esa)], [f17_sk])).
% 64.85/8.81 cnf(ssp18, plain, (spl0 | spl1 | spl3 | spl5 | spl6 | spl7 | spl8 | spl9 | spl11 | spl15), inference(avatar_split_clause, [status(thm)], [c39, sdef0, sdef1, sdef3, sdef5, sdef6, sdef7, sdef8, sdef9, sdef11, sdef15])).
% 64.85/8.81 cnf(c40, plain, ~cowlThing(sk0) | cowlNothing(sk0) | xsd_integer(sk1) | ~xsd_string(sk1) | sk2 != ia | ~requalityOnA(sk5,sk4) | ~cowlThing(ia) | ~requalityOnA(ia,ia) | ~cowlThing(ib) | ~cowlThing(ic), inference(cnf_transformation, [status(esa)], [f17_sk])).
% 64.85/8.81 cnf(ssp19, plain, (spl0 | spl1 | spl3 | spl6 | spl7 | spl8 | spl9 | spl10 | spl11 | spl15), inference(avatar_split_clause, [status(thm)], [c40, sdef0, sdef1, sdef3, sdef6, sdef7, sdef8, sdef9, sdef10, sdef11, sdef15])).
% 64.85/8.81 cnf(c41, plain, ~cowlThing(sk0) | cowlNothing(sk0) | xsd_integer(sk1) | ~xsd_string(sk1) | sk2 != ib | requalityOnA(sk4,sk5) | ~cowlThing(ia) | ~requalityOnA(ia,ia) | ~cowlThing(ib) | ~cowlThing(ic), inference(cnf_transformation, [status(esa)], [f17_sk])).
% 64.85/8.81 cnf(ssp20, plain, (spl0 | spl1 | spl3 | spl5 | spl6 | spl7 | spl8 | spl9 | spl12 | spl15), inference(avatar_split_clause, [status(thm)], [c41, sdef0, sdef1, sdef3, sdef5, sdef6, sdef7, sdef8, sdef9, sdef12, sdef15])).
% 64.85/8.81 cnf(c42, plain, ~cowlThing(sk0) | cowlNothing(sk0) | xsd_integer(sk1) | ~xsd_string(sk1) | sk2 != ib | ~requalityOnA(sk5,sk4) | ~cowlThing(ia) | ~requalityOnA(ia,ia) | ~cowlThing(ib) | ~cowlThing(ic), inference(cnf_transformation, [status(esa)], [f17_sk])).
% 64.85/8.81 cnf(ssp21, plain, (spl0 | spl1 | spl3 | spl6 | spl7 | spl8 | spl9 | spl10 | spl12 | spl15), inference(avatar_split_clause, [status(thm)], [c42, sdef0, sdef1, sdef3, sdef6, sdef7, sdef8, sdef9, sdef10, sdef12, sdef15])).
% 64.85/8.81 cnf(c43, plain, ~cowlThing(sk0) | cowlNothing(sk0) | xsd_integer(sk1) | ~xsd_string(sk1) | sk2 != ic | requalityOnA(sk4,sk5) | ~cowlThing(ia) | ~requalityOnA(ia,ia) | ~cowlThing(ib) | ~cowlThing(ic), inference(cnf_transformation, [status(esa)], [f17_sk])).
% 64.85/8.81 cnf(ssp22, plain, (spl0 | spl1 | spl3 | spl5 | spl6 | spl7 | spl8 | spl9 | spl13 | spl15), inference(avatar_split_clause, [status(thm)], [c43, sdef0, sdef1, sdef3, sdef5, sdef6, sdef7, sdef8, sdef9, sdef13, sdef15])).
% 64.85/8.81 cnf(c44, plain, ~cowlThing(sk0) | cowlNothing(sk0) | xsd_integer(sk1) | ~xsd_string(sk1) | sk2 != ic | ~requalityOnA(sk5,sk4) | ~cowlThing(ia) | ~requalityOnA(ia,ia) | ~cowlThing(ib) | ~cowlThing(ic), inference(cnf_transformation, [status(esa)], [f17_sk])).
% 64.85/8.81 cnf(ssp23, plain, (spl0 | spl1 | spl3 | spl6 | spl7 | spl8 | spl9 | spl10 | spl13 | spl15), inference(avatar_split_clause, [status(thm)], [c44, sdef0, sdef1, sdef3, sdef6, sdef7, sdef8, sdef9, sdef10, sdef13, sdef15])).
% 64.85/8.81 cnf(c45, plain, ~cowlThing(sk0) | cowlNothing(sk0) | xsd_integer(sk1) | ~xsd_integer(sk1) | requalityOnA(sk2,sk3) | requalityOnA(sk4,sk5) | ~cowlThing(ia) | ~requalityOnA(ia,ia) | ~cowlThing(ib) | ~cowlThing(ic), inference(cnf_transformation, [status(esa)], [f17_sk])).
% 64.85/8.81 cnf(ssp24, plain, (spl0 | spl1 | spl4 | spl5 | spl6 | spl7 | spl8 | spl9 | spl14 | spl15), inference(avatar_split_clause, [status(thm)], [c45, sdef0, sdef1, sdef4, sdef5, sdef6, sdef7, sdef8, sdef9, sdef14, sdef15])).
% 64.85/8.81 cnf(c46, plain, ~cowlThing(sk0) | cowlNothing(sk0) | xsd_integer(sk1) | ~xsd_integer(sk1) | requalityOnA(sk2,sk3) | ~requalityOnA(sk5,sk4) | ~cowlThing(ia) | ~requalityOnA(ia,ia) | ~cowlThing(ib) | ~cowlThing(ic), inference(cnf_transformation, [status(esa)], [f17_sk])).
% 64.85/8.81 cnf(ssp25, plain, (spl0 | spl1 | spl4 | spl6 | spl7 | spl8 | spl9 | spl10 | spl14 | spl15), inference(avatar_split_clause, [status(thm)], [c46, sdef0, sdef1, sdef4, sdef6, sdef7, sdef8, sdef9, sdef10, sdef14, sdef15])).
% 64.85/8.81 cnf(c47, plain, ~cowlThing(sk0) | cowlNothing(sk0) | xsd_integer(sk1) | ~xsd_integer(sk1) | sk2 != ia | requalityOnA(sk4,sk5) | ~cowlThing(ia) | ~requalityOnA(ia,ia) | ~cowlThing(ib) | ~cowlThing(ic), inference(cnf_transformation, [status(esa)], [f17_sk])).
% 64.85/8.81 cnf(ssp26, plain, (spl0 | spl1 | spl5 | spl6 | spl7 | spl8 | spl9 | spl11 | spl14 | spl15), inference(avatar_split_clause, [status(thm)], [c47, sdef0, sdef1, sdef5, sdef6, sdef7, sdef8, sdef9, sdef11, sdef14, sdef15])).
% 64.85/8.81 cnf(c48, plain, ~cowlThing(sk0) | cowlNothing(sk0) | xsd_integer(sk1) | ~xsd_integer(sk1) | sk2 != ia | ~requalityOnA(sk5,sk4) | ~cowlThing(ia) | ~requalityOnA(ia,ia) | ~cowlThing(ib) | ~cowlThing(ic), inference(cnf_transformation, [status(esa)], [f17_sk])).
% 64.85/8.81 cnf(ssp27, plain, (spl0 | spl1 | spl6 | spl7 | spl8 | spl9 | spl10 | spl11 | spl14 | spl15), inference(avatar_split_clause, [status(thm)], [c48, sdef0, sdef1, sdef6, sdef7, sdef8, sdef9, sdef10, sdef11, sdef14, sdef15])).
% 64.85/8.81 cnf(c49, plain, ~cowlThing(sk0) | cowlNothing(sk0) | xsd_integer(sk1) | ~xsd_integer(sk1) | sk2 != ib | requalityOnA(sk4,sk5) | ~cowlThing(ia) | ~requalityOnA(ia,ia) | ~cowlThing(ib) | ~cowlThing(ic), inference(cnf_transformation, [status(esa)], [f17_sk])).
% 64.85/8.81 cnf(ssp28, plain, (spl0 | spl1 | spl5 | spl6 | spl7 | spl8 | spl9 | spl12 | spl14 | spl15), inference(avatar_split_clause, [status(thm)], [c49, sdef0, sdef1, sdef5, sdef6, sdef7, sdef8, sdef9, sdef12, sdef14, sdef15])).
% 64.85/8.81 cnf(c50, plain, ~cowlThing(sk0) | cowlNothing(sk0) | xsd_integer(sk1) | ~xsd_integer(sk1) | sk2 != ib | ~requalityOnA(sk5,sk4) | ~cowlThing(ia) | ~requalityOnA(ia,ia) | ~cowlThing(ib) | ~cowlThing(ic), inference(cnf_transformation, [status(esa)], [f17_sk])).
% 64.85/8.81 cnf(ssp29, plain, (spl0 | spl1 | spl6 | spl7 | spl8 | spl9 | spl10 | spl12 | spl14 | spl15), inference(avatar_split_clause, [status(thm)], [c50, sdef0, sdef1, sdef6, sdef7, sdef8, sdef9, sdef10, sdef12, sdef14, sdef15])).
% 64.85/8.81 cnf(c51, plain, ~cowlThing(sk0) | cowlNothing(sk0) | xsd_integer(sk1) | ~xsd_integer(sk1) | sk2 != ic | requalityOnA(sk4,sk5) | ~cowlThing(ia) | ~requalityOnA(ia,ia) | ~cowlThing(ib) | ~cowlThing(ic), inference(cnf_transformation, [status(esa)], [f17_sk])).
% 64.85/8.81 cnf(ssp30, plain, (spl0 | spl1 | spl5 | spl6 | spl7 | spl8 | spl9 | spl13 | spl14 | spl15), inference(avatar_split_clause, [status(thm)], [c51, sdef0, sdef1, sdef5, sdef6, sdef7, sdef8, sdef9, sdef13, sdef14, sdef15])).
% 64.85/8.81 cnf(c52, plain, ~cowlThing(sk0) | cowlNothing(sk0) | xsd_integer(sk1) | ~xsd_integer(sk1) | sk2 != ic | ~requalityOnA(sk5,sk4) | ~cowlThing(ia) | ~requalityOnA(ia,ia) | ~cowlThing(ib) | ~cowlThing(ic), inference(cnf_transformation, [status(esa)], [f17_sk])).
% 64.85/8.81 cnf(ssp31, plain, (spl0 | spl1 | spl6 | spl7 | spl8 | spl9 | spl10 | spl13 | spl14 | spl15), inference(avatar_split_clause, [status(thm)], [c52, sdef0, sdef1, sdef6, sdef7, sdef8, sdef9, sdef10, sdef13, sdef14, sdef15])).
% 64.85/8.81 cnf(c11, plain, ~cA(X0) | X0 = ib | X0 = ia, inference(cnf_transformation, [status(esa)], [f9_sk])).
% 64.85/8.81 cnf(p82, plain, ~cA(X0) | X0 = ib | ib != ia, inference(equality_factoring, [status(thm)], [c11])).
% 64.85/8.81 cnf(ssp32, plain, (spl16 | spl17), inference(avatar_split_clause, [status(thm)], [p82, sdef16, sdef17])).
% 64.85/8.81 cnf(p85, plain, ~cA(X0) | X0 = ia | ia != ib, inference(equality_factoring, [status(thm)], [c11])).
% 64.85/8.81 cnf(ssp33, plain, (spl18 | spl19), inference(avatar_split_clause, [status(thm)], [p85, sdef18, sdef19])).
% 64.85/8.81 cnf(p88, plain, (sk3 = ib | sk3 = ia | ~spl4), inference(resolution, [status(thm)], [c11, p80])).
% 64.85/8.81 cnf(ssp34, plain, (~spl4 | spl20 | spl21), inference(avatar_split_clause, [status(thm)], [p88, sdef20, sdef21])).
% 64.85/8.81 cnf(p91, plain, (sk5 = ib | sk5 = ia | ~spl5), inference(resolution, [status(thm)], [p81, c11])).
% 64.85/8.81 cnf(ssp35, plain, (~spl5 | spl22 | spl23), inference(avatar_split_clause, [status(thm)], [p91, sdef22, sdef23])).
% 64.85/8.81 cnf(p126, plain, (ib = ia | ~spl4 | ~spl16 | ~spl21), inference(superposition, [status(thm)], [p112, p90])).
% 64.85/8.81 fof(f5, axiom, ! [A,B] : ( ( A = B & xsd_integer(A) ) => xsd_integer(B) ), file('/export/starexec/sandbox/benchmark/theBenchmark.p', xsd_integer_substitution_1)).
% 64.85/8.81 fof(f5_nnf, plain, ! [A,B] : (((A != B | ~(xsd_integer(A))) | xsd_integer(B))), inference(nnf_transformation, [status(thm)], [f5])).
% 64.85/8.81 fof(f5_sk, plain, ! [A,B] : (((A != B | ~(xsd_integer(A))) | xsd_integer(B))), inference(skolemisation, [status(esa)], [f5_nnf])).
% 64.85/8.81 cnf(c5, plain, X0 != X1 | ~xsd_integer(X0) | xsd_integer(X1), inference(cnf_transformation, [status(esa)], [f5_sk])).
% 64.85/8.81 cnf(p145, plain, (~xsd_integer(ib) | xsd_integer(ia) | ~spl4 | ~spl16 | ~spl21), inference(resolution, [status(thm)], [p126, c5])).
% 64.85/8.81 cnf(ssp36, plain, (~spl4 | ~spl16 | ~spl21 | spl24 | spl25), inference(avatar_split_clause, [status(thm)], [p145, sdef24, sdef25])).
% 64.85/8.81 fof(f6, axiom, ! [A,B] : ( ( A = B & xsd_string(A) ) => xsd_string(B) ), file('/export/starexec/sandbox/benchmark/theBenchmark.p', xsd_string_substitution_1)).
% 64.85/8.81 fof(f6_nnf, plain, ! [A,B] : (((A != B | ~(xsd_string(A))) | xsd_string(B))), inference(nnf_transformation, [status(thm)], [f6])).
% 64.85/8.81 fof(f6_sk, plain, ! [A,B] : (((A != B | ~(xsd_string(A))) | xsd_string(B))), inference(skolemisation, [status(esa)], [f6_nnf])).
% 64.85/8.81 cnf(c6, plain, X0 != X1 | ~xsd_string(X0) | xsd_string(X1), inference(cnf_transformation, [status(esa)], [f6_sk])).
% 64.85/8.81 cnf(p148, plain, (~xsd_string(ib) | xsd_string(ia) | ~spl4 | ~spl16 | ~spl21), inference(resolution, [status(thm)], [p126, c6])).
% 64.85/8.81 cnf(ssp37, plain, (~spl4 | ~spl16 | ~spl21 | spl26 | spl27), inference(avatar_split_clause, [status(thm)], [p148, sdef26, sdef27])).
% 64.85/8.81 cnf(p208, plain, (~xsd_integer(ib) | xsd_integer(ia) | ~spl18), inference(resolution, [status(thm)], [p122, c5])).
% 64.85/8.81 cnf(ssp38, plain, (~spl18 | spl24 | spl25), inference(avatar_split_clause, [status(thm)], [p208, sdef24, sdef25])).
% 64.85/8.81 cnf(p209, plain, (~xsd_string(ib) | xsd_string(ia) | ~spl18), inference(resolution, [status(thm)], [p122, c6])).
% 64.85/8.81 cnf(ssp39, plain, (~spl18 | spl26 | spl27), inference(avatar_split_clause, [status(thm)], [p209, sdef26, sdef27])).
% 64.85/8.81 fof(f0, axiom, ! [A,B] : ( ( A = B & cA(A) ) => cA(B) ), file('/export/starexec/sandbox/benchmark/theBenchmark.p', cA_substitution_1)).
% 64.85/8.81 fof(f0_nnf, plain, ! [A,B] : (((A != B | ~(cA(A))) | cA(B))), inference(nnf_transformation, [status(thm)], [f0])).
% 64.85/8.81 fof(f0_sk, plain, ! [A,B] : (((A != B | ~(cA(A))) | cA(B))), inference(skolemisation, [status(esa)], [f0_nnf])).
% 64.85/8.81 cnf(c0, plain, X0 != X1 | ~cA(X0) | cA(X1), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 64.85/8.81 cnf(p235, plain, (~cA(ib) | cA(sk4) | ~spl5 | ~spl16), inference(resolution, [status(thm)], [p171, c0])).
% 64.85/8.81 fof(sdef29, definition, (spl29 <=> (cA(sk4))), introduced(definition, [new_symbols(naming, [spl29])], [avatar_definition])).
% 64.85/8.81 cnf(ssp40, plain, (~spl5 | ~spl16 | spl28 | spl29), inference(avatar_split_clause, [status(thm)], [p235, sdef28, sdef29])).
% 64.85/8.81 cnf(p241, plain, (~xsd_integer(ib) | xsd_integer(sk4) | ~spl5 | ~spl16), inference(resolution, [status(thm)], [p171, c5])).
% 64.85/8.81 cnf(ssp41, plain, (~spl5 | ~spl16 | spl24 | spl30), inference(avatar_split_clause, [status(thm)], [p241, sdef24, sdef30])).
% 64.85/8.81 cnf(p243, plain, (~xsd_string(ib) | xsd_string(sk4) | ~spl5 | ~spl16), inference(resolution, [status(thm)], [p171, c6])).
% 64.85/8.81 cnf(ssp42, plain, (~spl5 | ~spl16 | spl26 | spl31), inference(avatar_split_clause, [status(thm)], [p243, sdef26, sdef31])).
% 64.85/8.81 cnf(p237, plain, (cA(sk4) | ~spl29), inference(avatar_component_clause, [status(thm)], [sdef29])).
% 64.85/8.81 cnf(p246, plain, (sk4 = ib | sk4 = ia | ~spl29), inference(resolution, [status(thm)], [p237, c11])).
% 64.85/8.81 fof(sdef33, definition, (spl33 <=> (sk4 = ia)), introduced(definition, [new_symbols(naming, [spl33])], [avatar_definition])).
% 64.85/8.81 cnf(ssp43, plain, (~spl29 | spl32 | spl33), inference(avatar_split_clause, [status(thm)], [p246, sdef32, sdef33])).
% 64.85/8.81 cnf(p256, plain, (~cA(ib) | cA(sk2) | ~spl4 | ~spl18), inference(resolution, [status(thm)], [p216, c0])).
% 64.85/8.81 fof(sdef34, definition, (spl34 <=> (cA(sk2))), introduced(definition, [new_symbols(naming, [spl34])], [avatar_definition])).
% 64.85/8.81 cnf(ssp44, plain, (~spl4 | ~spl18 | spl28 | spl34), inference(avatar_split_clause, [status(thm)], [p256, sdef28, sdef34])).
% 64.85/8.81 cnf(p263, plain, (~xsd_integer(ib) | xsd_integer(sk2) | ~spl4 | ~spl18), inference(resolution, [status(thm)], [p216, c5])).
% 64.85/8.81 cnf(ssp45, plain, (~spl4 | ~spl18 | spl24 | spl35), inference(avatar_split_clause, [status(thm)], [p263, sdef24, sdef35])).
% 64.85/8.81 cnf(p265, plain, (~xsd_string(ib) | xsd_string(sk2) | ~spl4 | ~spl18), inference(resolution, [status(thm)], [p216, c6])).
% 64.85/8.81 cnf(ssp46, plain, (~spl4 | ~spl18 | spl26 | spl36), inference(avatar_split_clause, [status(thm)], [p265, sdef26, sdef36])).
% 64.85/8.81 cnf(p257, plain, (cA(sk2) | ~spl34), inference(avatar_component_clause, [status(thm)], [sdef34])).
% 64.85/8.81 cnf(p267, plain, (sk2 = ib | sk2 = ia | ~spl34), inference(resolution, [status(thm)], [p257, c11])).
% 64.85/8.81 cnf(ssp47, plain, (~spl34 | spl37 | spl38), inference(avatar_split_clause, [status(thm)], [p267, sdef37, sdef38])).
% 64.85/8.81 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, 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, sct25, sct26, sct27, sct28, sct29, sct30, sct31, sct32, sct33, sct34])).
% 64.85/8.81 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------