%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : KRS144+1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n016.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 01:53:19 PM UTC 2026
% Result : Theorem 24.53s 8.81s
% Output : Proof 24.53s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : KRS144+1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.11/5.38 % Computer : n016.cluster.edu
% 0.11/5.38 % Model : x86_64 x86_64
% 0.11/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/5.38 % Memory : 8046.5625MB
% 0.11/5.38 % OS : Linux 6.8.0-71-generic
% 0.11/5.38 % CPULimit : 300
% 0.11/5.38 % WCLimit : 300
% 0.11/5.38 % DateTime : Wed Sep 23 19:36:02 UTC 2026
% 0.11/5.39 % CPUTime :
% 0.11/5.39 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 24.53/8.81 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 24.53/8.81 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 24.53/8.81 fof(sdef3, definition, (spl3 <=> (~xsd_string(sk3))), introduced(definition, [new_symbols(naming, [spl3])], [avatar_definition])).
% 24.53/8.81 cnf(p19, plain, (~xsd_string(sk3) | ~spl3), inference(avatar_component_clause, [status(thm)], [sdef3])).
% 24.53/8.81 fof(sdef2, definition, (spl2 <=> (xsd_string(sk3))), introduced(definition, [new_symbols(naming, [spl2])], [avatar_definition])).
% 24.53/8.81 cnf(p18, plain, (xsd_string(sk3) | ~spl2), inference(avatar_component_clause, [status(thm)], [sdef2])).
% 24.53/8.81 cnf(p86, plain, ($false | ~spl2 | ~spl3), inference(resolution, [status(thm)], [p19, p18])).
% 24.53/8.81 cnf(sct0, plain, (~spl2 | ~spl3), inference(avatar_contradiction_clause, [status(thm)], [p86])).
% 24.53/8.81 fof(sdef14, definition, (spl14 <=> (xsd_integer(sk3))), introduced(definition, [new_symbols(naming, [spl14])], [avatar_definition])).
% 24.53/8.81 cnf(p58, plain, (xsd_integer(sk3) | ~spl14), inference(avatar_component_clause, [status(thm)], [sdef14])).
% 24.53/8.81 fof(sdef13, definition, (spl13 <=> (~xsd_integer(sk3))), introduced(definition, [new_symbols(naming, [spl13])], [avatar_definition])).
% 24.53/8.81 cnf(p43, plain, (~xsd_integer(sk3) | ~spl13), inference(avatar_component_clause, [status(thm)], [sdef13])).
% 24.53/8.81 cnf(p87, plain, ($false | ~spl13 | ~spl14), inference(resolution, [status(thm)], [p58, p43])).
% 24.53/8.81 cnf(sct1, plain, (~spl13 | ~spl14), inference(avatar_contradiction_clause, [status(thm)], [p87])).
% 24.53/8.81 fof(f7, axiom, ! [X] : ( cowlThing(X) & ~ cowlNothing(X) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_0)).
% 24.53/8.81 fof(f7_nnf, plain, ! [X] : ((cowlThing(X) & ~(cowlNothing(X)))), inference(nnf_transformation, [status(thm)], [f7])).
% 24.53/8.81 fof(f7_sk, plain, ! [X] : ((cowlThing(X) & ~(cowlNothing(X)))), inference(skolemisation, [status(esa)], [f7_nnf])).
% 24.53/8.81 cnf(c7, plain, cowlThing(X0), inference(cnf_transformation, [status(esa)], [f7_sk])).
% 24.53/8.81 fof(sdef0, definition, (spl0 <=> (~cowlThing(sk2))), introduced(definition, [new_symbols(naming, [spl0])], [avatar_definition])).
% 24.53/8.81 cnf(p16, plain, (~cowlThing(sk2) | ~spl0), inference(avatar_component_clause, [status(thm)], [sdef0])).
% 24.53/8.81 cnf(p88, plain, ($false | ~spl0), inference(resolution, [status(thm)], [c7, p16])).
% 24.53/8.81 cnf(sct2, plain, (~spl0), inference(avatar_contradiction_clause, [status(thm)], [p88])).
% 24.53/8.81 cnf(c8, plain, ~cowlNothing(X0), inference(cnf_transformation, [status(esa)], [f7_sk])).
% 24.53/8.81 fof(sdef1, definition, (spl1 <=> (cowlNothing(sk2))), introduced(definition, [new_symbols(naming, [spl1])], [avatar_definition])).
% 24.53/8.81 cnf(p17, plain, (cowlNothing(sk2) | ~spl1), inference(avatar_component_clause, [status(thm)], [sdef1])).
% 24.53/8.81 cnf(p89, plain, ($false | ~spl1), inference(resolution, [status(thm)], [c8, p17])).
% 24.53/8.81 cnf(sct3, plain, (~spl1), inference(avatar_contradiction_clause, [status(thm)], [p89])).
% 24.53/8.81 fof(sdef19, definition, (spl19 <=> (~xsd_string(sk0(sk8)))), introduced(definition, [new_symbols(naming, [spl19])], [avatar_definition])).
% 24.53/8.81 cnf(p107, plain, (~xsd_string(sk0(sk8)) | ~spl19), inference(avatar_component_clause, [status(thm)], [sdef19])).
% 24.53/8.81 fof(f8, axiom, ! [X] : ( xsd_string(X) <=> ~ xsd_integer(X) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_1)).
% 24.53/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])).
% 24.53/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])).
% 24.53/8.81 cnf(c10, plain, xsd_string(X0) | xsd_integer(X0), inference(cnf_transformation, [status(esa)], [f8_sk])).
% 24.53/8.81 cnf(p116, plain, (xsd_integer(sk0(sk8)) | ~spl19), inference(resolution, [status(thm)], [p107, c10])).
% 24.53/8.81 fof(sdef17, definition, (spl17 <=> (~xsd_integer(sk0(sk8)))), introduced(definition, [new_symbols(naming, [spl17])], [avatar_definition])).
% 24.53/8.81 cnf(p104, plain, (~xsd_integer(sk0(sk8)) | ~spl17), inference(avatar_component_clause, [status(thm)], [sdef17])).
% 24.53/8.81 cnf(p126, plain, ($false | ~spl17 | ~spl19), inference(resolution, [status(thm)], [p116, p104])).
% 24.53/8.81 cnf(sct4, plain, (~spl17 | ~spl19), inference(avatar_contradiction_clause, [status(thm)], [p126])).
% 24.53/8.81 fof(f9, axiom, ! [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/sandbox2/benchmark/theBenchmark.p', axiom_2)).
% 24.53/8.81 fof(f9_nnf, plain, ! [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)], [f9])).
% 24.53/8.81 fof(f9_sk, plain, ! [X,Y0,Y1,Y2] : ((~(cc(X)) | (((rp(X,sk0(X)) & rp(X,sk1(X))) & sk0(X) != sk1(X)) & (((~(rp(X,Y0)) | ~(rp(X,Y1))) | ~(rp(X,Y2))) | ((Y0 = Y1 | Y0 = Y2) | Y1 = Y2))))), inference(skolemisation, [status(esa), new_symbols(skolem, [sk0,sk1])], [f9_nnf])).
% 24.53/8.81 cnf(c12, plain, ~cc(X0) | rp(X0,sk1(X0)), inference(cnf_transformation, [status(esa)], [f9_sk])).
% 24.53/8.81 fof(sdef5, definition, (spl5 <=> (cc(sk8))), introduced(definition, [new_symbols(naming, [spl5])], [avatar_definition])).
% 24.53/8.81 cnf(p21, plain, (cc(sk8) | ~spl5), inference(avatar_component_clause, [status(thm)], [sdef5])).
% 24.53/8.81 cnf(p95, plain, (rp(sk8,sk1(sk8)) | ~spl5), inference(resolution, [status(thm)], [c12, p21])).
% 24.53/8.81 fof(sdef6, definition, (spl6 <=> (~rp(sk8,X0) | ~rp(sk8,X1) | X0 = X1)), introduced(definition, [new_symbols(naming, [spl6])], [avatar_definition])).
% 24.53/8.81 cnf(p23, plain, (~rp(sk8,X0) | ~rp(sk8,X1) | X0 = X1 | ~spl6), inference(avatar_component_clause, [status(thm)], [sdef6])).
% 24.53/8.81 cnf(p96, plain, (~rp(sk8,X0) | sk1(sk8) = X0 | ~spl5 | ~spl6), inference(resolution, [status(thm)], [p95, p23])).
% 24.53/8.81 cnf(c11, plain, ~cc(X0) | rp(X0,sk0(X0)), inference(cnf_transformation, [status(esa)], [f9_sk])).
% 24.53/8.81 cnf(p92, plain, (rp(sk8,sk0(sk8)) | ~spl5), inference(resolution, [status(thm)], [c11, p21])).
% 24.53/8.81 cnf(p128, plain, (sk1(sk8) = sk0(sk8) | ~spl5 | ~spl6), inference(resolution, [status(thm)], [p96, p92])).
% 24.53/8.81 cnf(c13, plain, ~cc(X0) | sk0(X0) != sk1(X0), inference(cnf_transformation, [status(esa)], [f9_sk])).
% 24.53/8.81 cnf(p114, plain, (sk0(sk8) != sk1(sk8) | ~spl5), inference(resolution, [status(thm)], [c13, p21])).
% 24.53/8.81 cnf(p129, plain, (sk0(sk8) != sk0(sk8) | ~spl5 | ~spl6), inference(superposition, [status(thm)], [p128, p114])).
% 24.53/8.81 cnf(p130, plain, ($false | ~spl5 | ~spl6), inference(equality_resolution, [status(thm)], [p129])).
% 24.53/8.81 cnf(sct5, plain, (~spl5 | ~spl6), inference(avatar_contradiction_clause, [status(thm)], [p130])).
% 24.53/8.81 fof(sdef18, definition, (spl18 <=> (xsd_integer(sk1(sk8)))), introduced(definition, [new_symbols(naming, [spl18])], [avatar_definition])).
% 24.53/8.81 cnf(p105, plain, (xsd_integer(sk1(sk8)) | ~spl18), inference(avatar_component_clause, [status(thm)], [sdef18])).
% 24.53/8.81 fof(sdef20, definition, (spl20 <=> (xsd_string(sk1(sk8)))), introduced(definition, [new_symbols(naming, [spl20])], [avatar_definition])).
% 24.53/8.81 cnf(p108, plain, (xsd_string(sk1(sk8)) | ~spl20), inference(avatar_component_clause, [status(thm)], [sdef20])).
% 24.53/8.81 cnf(c9, plain, ~xsd_string(X0) | ~xsd_integer(X0), inference(cnf_transformation, [status(esa)], [f8_sk])).
% 24.53/8.81 cnf(p117, plain, (~xsd_integer(sk1(sk8)) | ~spl20), inference(resolution, [status(thm)], [p108, c9])).
% 24.53/8.81 cnf(p132, plain, ($false | ~spl18 | ~spl20), inference(resolution, [status(thm)], [p105, p117])).
% 24.53/8.81 cnf(sct6, plain, (~spl18 | ~spl20), inference(avatar_contradiction_clause, [status(thm)], [p132])).
% 24.53/8.81 fof(sdef22, definition, (spl22 <=> (sk5 = sk6)), introduced(definition, [new_symbols(naming, [spl22])], [avatar_definition])).
% 24.53/8.81 cnf(p142, plain, (sk5 = sk6 | ~spl22), inference(avatar_component_clause, [status(thm)], [sdef22])).
% 24.53/8.81 fof(sdef10, definition, (spl10 <=> (sk5 != sk6)), introduced(definition, [new_symbols(naming, [spl10])], [avatar_definition])).
% 24.53/8.81 cnf(p34, plain, (sk5 != sk6 | ~spl10), inference(avatar_component_clause, [status(thm)], [sdef10])).
% 24.53/8.81 cnf(p156, plain, ($false | ~spl10 | ~spl22), inference(resolution, [status(thm)], [p142, p34])).
% 24.53/8.81 cnf(sct7, plain, (~spl10 | ~spl22), inference(avatar_contradiction_clause, [status(thm)], [p156])).
% 24.53/8.81 fof(sdef24, definition, (spl24 <=> (sk5 = sk7)), introduced(definition, [new_symbols(naming, [spl24])], [avatar_definition])).
% 24.53/8.81 cnf(p145, plain, (sk5 = sk7 | ~spl24), inference(avatar_component_clause, [status(thm)], [sdef24])).
% 24.53/8.81 fof(sdef11, definition, (spl11 <=> (sk5 != sk7)), introduced(definition, [new_symbols(naming, [spl11])], [avatar_definition])).
% 24.53/8.81 cnf(p37, plain, (sk5 != sk7 | ~spl11), inference(avatar_component_clause, [status(thm)], [sdef11])).
% 24.53/8.81 cnf(p169, plain, ($false | ~spl11 | ~spl24), inference(resolution, [status(thm)], [p145, p37])).
% 24.53/8.81 cnf(sct8, plain, (~spl11 | ~spl24), inference(avatar_contradiction_clause, [status(thm)], [p169])).
% 24.53/8.81 fof(sdef35, definition, (spl35 <=> (~xsd_string(sk5))), introduced(definition, [new_symbols(naming, [spl35])], [avatar_definition])).
% 24.53/8.81 cnf(p186, plain, (~xsd_string(sk5) | ~spl35), inference(avatar_component_clause, [status(thm)], [sdef35])).
% 24.53/8.81 cnf(p189, plain, (xsd_integer(sk5) | ~spl35), inference(resolution, [status(thm)], [p186, c10])).
% 24.53/8.81 fof(sdef33, definition, (spl33 <=> (~xsd_integer(sk5))), introduced(definition, [new_symbols(naming, [spl33])], [avatar_definition])).
% 24.53/8.81 cnf(p183, plain, (~xsd_integer(sk5) | ~spl33), inference(avatar_component_clause, [status(thm)], [sdef33])).
% 24.53/8.81 cnf(p190, plain, ($false | ~spl33 | ~spl35), inference(resolution, [status(thm)], [p189, p183])).
% 24.53/8.81 cnf(sct9, plain, (~spl33 | ~spl35), inference(avatar_contradiction_clause, [status(thm)], [p190])).
% 24.53/8.81 fof(sdef36, definition, (spl36 <=> (xsd_string(sk0(sk4)))), introduced(definition, [new_symbols(naming, [spl36])], [avatar_definition])).
% 24.53/8.81 cnf(p187, plain, (xsd_string(sk0(sk4)) | ~spl36), inference(avatar_component_clause, [status(thm)], [sdef36])).
% 24.53/8.81 cnf(p198, plain, (~xsd_integer(sk0(sk4)) | ~spl36), inference(resolution, [status(thm)], [p187, c9])).
% 24.53/8.81 fof(sdef34, definition, (spl34 <=> (xsd_integer(sk0(sk4)))), introduced(definition, [new_symbols(naming, [spl34])], [avatar_definition])).
% 24.53/8.81 cnf(p184, plain, (xsd_integer(sk0(sk4)) | ~spl34), inference(avatar_component_clause, [status(thm)], [sdef34])).
% 24.53/8.81 cnf(p199, plain, ($false | ~spl34 | ~spl36), inference(resolution, [status(thm)], [p198, p184])).
% 24.53/8.81 cnf(sct10, plain, (~spl34 | ~spl36), inference(avatar_contradiction_clause, [status(thm)], [p199])).
% 24.53/8.81 fof(sdef28, definition, (spl28 <=> (sk5 = sk1(sk4))), introduced(definition, [new_symbols(naming, [spl28])], [avatar_definition])).
% 24.53/8.81 cnf(p151, plain, (sk5 = sk1(sk4) | ~spl28), inference(avatar_component_clause, [status(thm)], [sdef28])).
% 24.53/8.81 fof(sdef37, definition, (spl37 <=> (cc(sk1(sk4)))), introduced(definition, [new_symbols(naming, [spl37])], [avatar_definition])).
% 24.53/8.81 cnf(p207, plain, (cc(sk1(sk4)) | ~spl37), inference(avatar_component_clause, [status(thm)], [sdef37])).
% 24.53/8.81 cnf(p221, plain, (cc(sk5) | ~spl28 | ~spl37), inference(superposition, [status(thm)], [p151, p207])).
% 24.53/8.81 fof(sdef29, definition, (spl29 <=> (~cc(sk5))), introduced(definition, [new_symbols(naming, [spl29])], [avatar_definition])).
% 24.53/8.81 cnf(p153, plain, (~cc(sk5) | ~spl29), inference(avatar_component_clause, [status(thm)], [sdef29])).
% 24.53/8.81 cnf(p227, plain, ($false | ~spl28 | ~spl29 | ~spl37), inference(resolution, [status(thm)], [p221, p153])).
% 24.53/8.81 cnf(sct11, plain, (~spl28 | ~spl29 | ~spl37), inference(avatar_contradiction_clause, [status(thm)], [p227])).
% 24.53/8.81 fof(sdef40, definition, (spl40 <=> (sk6 = sk5)), introduced(definition, [new_symbols(naming, [spl40])], [avatar_definition])).
% 24.53/8.81 cnf(p229, plain, (sk6 = sk5 | ~spl40), inference(avatar_component_clause, [status(thm)], [sdef40])).
% 24.53/8.81 fof(sdef30, definition, (spl30 <=> (cc(sk6))), introduced(definition, [new_symbols(naming, [spl30])], [avatar_definition])).
% 24.53/8.81 cnf(p154, plain, (cc(sk6) | ~spl30), inference(avatar_component_clause, [status(thm)], [sdef30])).
% 24.53/8.81 cnf(p243, plain, (cc(sk5) | ~spl30 | ~spl40), inference(superposition, [status(thm)], [p229, p154])).
% 24.53/8.81 cnf(p249, plain, ($false | ~spl29 | ~spl30 | ~spl40), inference(resolution, [status(thm)], [p243, p153])).
% 24.53/8.81 cnf(sct12, plain, (~spl29 | ~spl30 | ~spl40), inference(avatar_contradiction_clause, [status(thm)], [p249])).
% 24.53/8.81 fof(sdef42, definition, (spl42 <=> (sk6 = sk7)), introduced(definition, [new_symbols(naming, [spl42])], [avatar_definition])).
% 24.53/8.81 cnf(p232, plain, (sk6 = sk7 | ~spl42), inference(avatar_component_clause, [status(thm)], [sdef42])).
% 24.53/8.81 fof(sdef12, definition, (spl12 <=> (sk6 != sk7)), introduced(definition, [new_symbols(naming, [spl12])], [avatar_definition])).
% 24.53/8.81 cnf(p40, plain, (sk6 != sk7 | ~spl12), inference(avatar_component_clause, [status(thm)], [sdef12])).
% 24.53/8.81 cnf(p254, plain, ($false | ~spl12 | ~spl42), inference(resolution, [status(thm)], [p232, p40])).
% 24.53/8.81 cnf(sct13, plain, (~spl12 | ~spl42), inference(avatar_contradiction_clause, [status(thm)], [p254])).
% 24.53/8.81 fof(sdef47, definition, (spl47 <=> (~cc(sk6))), introduced(definition, [new_symbols(naming, [spl47])], [avatar_definition])).
% 24.53/8.81 cnf(p251, plain, (~cc(sk6) | ~spl47), inference(avatar_component_clause, [status(thm)], [sdef47])).
% 24.53/8.81 cnf(p265, plain, ($false | ~spl30 | ~spl47), inference(resolution, [status(thm)], [p251, p154])).
% 24.53/8.81 cnf(sct14, plain, (~spl30 | ~spl47), inference(avatar_contradiction_clause, [status(thm)], [p265])).
% 24.53/8.81 fof(sdef39, definition, (spl39 <=> (xsd_string(sk1(sk4)))), introduced(definition, [new_symbols(naming, [spl39])], [avatar_definition])).
% 24.53/8.81 cnf(p214, plain, (xsd_string(sk1(sk4)) | ~spl39), inference(avatar_component_clause, [status(thm)], [sdef39])).
% 24.53/8.81 cnf(p239, plain, (~xsd_integer(sk1(sk4)) | ~spl39), inference(resolution, [status(thm)], [p214, c9])).
% 24.53/8.81 fof(sdef38, definition, (spl38 <=> (xsd_integer(sk1(sk4)))), introduced(definition, [new_symbols(naming, [spl38])], [avatar_definition])).
% 24.53/8.81 cnf(p211, plain, (xsd_integer(sk1(sk4)) | ~spl38), inference(avatar_component_clause, [status(thm)], [sdef38])).
% 24.53/8.81 cnf(p267, plain, ($false | ~spl38 | ~spl39), inference(resolution, [status(thm)], [p239, p211])).
% 24.53/8.81 cnf(sct15, plain, (~spl38 | ~spl39), inference(avatar_contradiction_clause, [status(thm)], [p267])).
% 24.53/8.81 cnf(p241, plain, (sk5 != sk5 | ~spl10 | ~spl40), inference(superposition, [status(thm)], [p229, p34])).
% 24.53/8.81 cnf(p281, plain, ($false | ~spl10 | ~spl40), inference(equality_resolution, [status(thm)], [p241])).
% 24.53/8.81 cnf(sct16, plain, (~spl10 | ~spl40), inference(avatar_contradiction_clause, [status(thm)], [p281])).
% 24.53/8.81 fof(sdef48, definition, (spl48 <=> (sk7 = sk5)), introduced(definition, [new_symbols(naming, [spl48])], [avatar_definition])).
% 24.53/8.81 cnf(p256, plain, (sk7 = sk5 | ~spl48), inference(avatar_component_clause, [status(thm)], [sdef48])).
% 24.53/8.81 fof(sdef31, definition, (spl31 <=> (cc(sk7))), introduced(definition, [new_symbols(naming, [spl31])], [avatar_definition])).
% 24.53/8.81 cnf(p167, plain, (cc(sk7) | ~spl31), inference(avatar_component_clause, [status(thm)], [sdef31])).
% 24.53/8.81 cnf(p285, plain, (cc(sk5) | ~spl31 | ~spl48), inference(superposition, [status(thm)], [p256, p167])).
% 24.53/8.81 cnf(p291, plain, ($false | ~spl29 | ~spl31 | ~spl48), inference(resolution, [status(thm)], [p285, p153])).
% 24.53/8.81 cnf(sct17, plain, (~spl29 | ~spl31 | ~spl48), inference(avatar_contradiction_clause, [status(thm)], [p291])).
% 24.53/8.81 fof(sdef49, definition, (spl49 <=> (sk7 = sk6)), introduced(definition, [new_symbols(naming, [spl49])], [avatar_definition])).
% 24.53/8.81 cnf(p258, plain, (sk7 = sk6 | ~spl49), inference(avatar_component_clause, [status(thm)], [sdef49])).
% 24.53/8.81 cnf(p295, plain, (cc(sk6) | ~spl31 | ~spl49), inference(superposition, [status(thm)], [p258, p167])).
% 24.53/8.81 cnf(p311, plain, ($false | ~spl31 | ~spl47 | ~spl49), inference(resolution, [status(thm)], [p295, p251])).
% 24.53/8.81 cnf(sct18, plain, (~spl31 | ~spl47 | ~spl49), inference(avatar_contradiction_clause, [status(thm)], [p311])).
% 24.53/8.81 cnf(p283, plain, (sk5 != sk5 | ~spl11 | ~spl48), inference(superposition, [status(thm)], [p256, p37])).
% 24.53/8.81 cnf(p317, plain, ($false | ~spl11 | ~spl48), inference(equality_resolution, [status(thm)], [p283])).
% 24.53/8.81 cnf(sct19, plain, (~spl11 | ~spl48), inference(avatar_contradiction_clause, [status(thm)], [p317])).
% 24.53/8.81 cnf(p294, plain, (sk6 != sk6 | ~spl12 | ~spl49), inference(superposition, [status(thm)], [p258, p40])).
% 24.53/8.81 cnf(p332, plain, ($false | ~spl12 | ~spl49), inference(equality_resolution, [status(thm)], [p294])).
% 24.53/8.81 cnf(sct20, plain, (~spl12 | ~spl49), inference(avatar_contradiction_clause, [status(thm)], [p332])).
% 24.53/8.81 cnf(p90, plain, (xsd_integer(sk3) | ~spl3), inference(resolution, [status(thm)], [c10, p19])).
% 24.53/8.81 cnf(p334, plain, ($false | ~spl3 | ~spl13), inference(resolution, [status(thm)], [p43, p90])).
% 24.53/8.81 cnf(sct21, plain, (~spl3 | ~spl13), inference(avatar_contradiction_clause, [status(thm)], [p334])).
% 24.53/8.81 cnf(p335, plain, (~xsd_integer(sk3) | ~spl2), inference(resolution, [status(thm)], [p18, c9])).
% 24.53/8.81 cnf(p339, plain, ($false | ~spl2 | ~spl14), inference(resolution, [status(thm)], [p335, p58])).
% 24.53/8.81 cnf(sct22, plain, (~spl2 | ~spl14), inference(avatar_contradiction_clause, [status(thm)], [p339])).
% 24.53/8.81 fof(f10, conjecture, ( ! [X] : ( cowlThing(X) & ~ cowlNothing(X) ) & ! [X] : ( xsd_string(X) <=> ~ xsd_integer(X) ) & ! [X] : ( cc(X) => ! [Y0,Y1,Y2] : ( ( rp(X,Y0) & rp(X,Y1) & rp(X,Y2) ) => ( Y0 = Y1 | Y0 = Y2 | Y1 = Y2 ) ) ) & ! [X] : ( cc(X) => ? [Y0,Y1] : ( rp(X,Y0) & rp(X,Y1) & Y0 != Y1 ) ) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', the_axiom)).
% 24.53/8.81 fof(f10_neg, negated_conjecture, ~(( ! [X] : ( cowlThing(X) & ~ cowlNothing(X) ) & ! [X] : ( xsd_string(X) <=> ~ xsd_integer(X) ) & ! [X] : ( cc(X) => ! [Y0,Y1,Y2] : ( ( rp(X,Y0) & rp(X,Y1) & rp(X,Y2) ) => ( Y0 = Y1 | Y0 = Y2 | Y1 = Y2 ) ) ) & ! [X] : ( cc(X) => ? [Y0,Y1] : ( rp(X,Y0) & rp(X,Y1) & Y0 != Y1 ) ) )), inference(negated_conjecture, [status(cth)], [f10])).
% 24.53/8.81 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,Y2] : ((((rp(X,Y0) & rp(X,Y1)) & rp(X,Y2)) & ((Y0 != Y1 & Y0 != Y2) & Y1 != Y2)))))) | ? [X] : ((cc(X) & ! [Y0,Y1] : (((~(rp(X,Y0)) | ~(rp(X,Y1))) | Y0 = Y1))))), inference(nnf_transformation, [status(thm)], [f10_neg])).
% 24.53/8.81 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,sk5) & rp(sk4,sk6)) & rp(sk4,sk7)) & ((sk5 != sk6 & sk5 != sk7) & sk6 != sk7)))) | (cc(sk8) & ((~(rp(sk8,Y0)) | ~(rp(sk8,Y1))) | Y0 = Y1)))), inference(skolemisation, [status(esa), new_symbols(skolem, [sk2,sk3,sk4,sk5,sk6,sk7,sk8])], [f10_nnf])).
% 24.53/8.81 cnf(c15, plain, ~cowlThing(sk2) | cowlNothing(sk2) | xsd_string(sk3) | ~xsd_string(sk3) | cc(sk4) | cc(sk8), inference(cnf_transformation, [status(esa)], [f10_sk])).
% 24.53/8.81 fof(sdef4, definition, (spl4 <=> (cc(sk4))), introduced(definition, [new_symbols(naming, [spl4])], [avatar_definition])).
% 24.53/8.81 cnf(ssp0, plain, (spl0 | spl1 | spl2 | spl3 | spl4 | spl5), inference(avatar_split_clause, [status(thm)], [c15, sdef0, sdef1, sdef2, sdef3, sdef4, sdef5])).
% 24.53/8.81 cnf(c16, plain, ~cowlThing(sk2) | cowlNothing(sk2) | xsd_string(sk3) | ~xsd_string(sk3) | cc(sk4) | ~rp(sk8,X1) | ~rp(sk8,X2) | X1 = X2, inference(cnf_transformation, [status(esa)], [f10_sk])).
% 24.53/8.81 cnf(ssp1, plain, (spl0 | spl1 | spl2 | spl3 | spl4 | spl6), inference(avatar_split_clause, [status(thm)], [c16, sdef0, sdef1, sdef2, sdef3, sdef4, sdef6])).
% 24.53/8.81 cnf(c17, plain, ~cowlThing(sk2) | cowlNothing(sk2) | xsd_string(sk3) | ~xsd_string(sk3) | rp(sk4,sk5) | cc(sk8), inference(cnf_transformation, [status(esa)], [f10_sk])).
% 24.53/8.81 fof(sdef7, definition, (spl7 <=> (rp(sk4,sk5))), introduced(definition, [new_symbols(naming, [spl7])], [avatar_definition])).
% 24.53/8.81 cnf(ssp2, plain, (spl0 | spl1 | spl2 | spl3 | spl5 | spl7), inference(avatar_split_clause, [status(thm)], [c17, sdef0, sdef1, sdef2, sdef3, sdef5, sdef7])).
% 24.53/8.81 cnf(c18, plain, ~cowlThing(sk2) | cowlNothing(sk2) | xsd_string(sk3) | ~xsd_string(sk3) | rp(sk4,sk5) | ~rp(sk8,X1) | ~rp(sk8,X2) | X1 = X2, inference(cnf_transformation, [status(esa)], [f10_sk])).
% 24.53/8.81 cnf(ssp3, plain, (spl0 | spl1 | spl2 | spl3 | spl6 | spl7), inference(avatar_split_clause, [status(thm)], [c18, sdef0, sdef1, sdef2, sdef3, sdef6, sdef7])).
% 24.53/8.81 cnf(c19, plain, ~cowlThing(sk2) | cowlNothing(sk2) | xsd_string(sk3) | ~xsd_string(sk3) | rp(sk4,sk6) | cc(sk8), inference(cnf_transformation, [status(esa)], [f10_sk])).
% 24.53/8.81 fof(sdef8, definition, (spl8 <=> (rp(sk4,sk6))), introduced(definition, [new_symbols(naming, [spl8])], [avatar_definition])).
% 24.53/8.81 cnf(ssp4, plain, (spl0 | spl1 | spl2 | spl3 | spl5 | spl8), inference(avatar_split_clause, [status(thm)], [c19, sdef0, sdef1, sdef2, sdef3, sdef5, sdef8])).
% 24.53/8.81 cnf(c20, plain, ~cowlThing(sk2) | cowlNothing(sk2) | xsd_string(sk3) | ~xsd_string(sk3) | rp(sk4,sk6) | ~rp(sk8,X1) | ~rp(sk8,X2) | X1 = X2, inference(cnf_transformation, [status(esa)], [f10_sk])).
% 24.53/8.81 cnf(ssp5, plain, (spl0 | spl1 | spl2 | spl3 | spl6 | spl8), inference(avatar_split_clause, [status(thm)], [c20, sdef0, sdef1, sdef2, sdef3, sdef6, sdef8])).
% 24.53/8.81 cnf(c21, plain, ~cowlThing(sk2) | cowlNothing(sk2) | xsd_string(sk3) | ~xsd_string(sk3) | rp(sk4,sk7) | cc(sk8), inference(cnf_transformation, [status(esa)], [f10_sk])).
% 24.53/8.81 fof(sdef9, definition, (spl9 <=> (rp(sk4,sk7))), introduced(definition, [new_symbols(naming, [spl9])], [avatar_definition])).
% 24.53/8.81 cnf(ssp6, plain, (spl0 | spl1 | spl2 | spl3 | spl5 | spl9), inference(avatar_split_clause, [status(thm)], [c21, sdef0, sdef1, sdef2, sdef3, sdef5, sdef9])).
% 24.53/8.81 cnf(c22, plain, ~cowlThing(sk2) | cowlNothing(sk2) | xsd_string(sk3) | ~xsd_string(sk3) | rp(sk4,sk7) | ~rp(sk8,X1) | ~rp(sk8,X2) | X1 = X2, inference(cnf_transformation, [status(esa)], [f10_sk])).
% 24.53/8.81 cnf(ssp7, plain, (spl0 | spl1 | spl2 | spl3 | spl6 | spl9), inference(avatar_split_clause, [status(thm)], [c22, sdef0, sdef1, sdef2, sdef3, sdef6, sdef9])).
% 24.53/8.81 cnf(c23, plain, ~cowlThing(sk2) | cowlNothing(sk2) | xsd_string(sk3) | ~xsd_string(sk3) | sk5 != sk6 | cc(sk8), inference(cnf_transformation, [status(esa)], [f10_sk])).
% 24.53/8.81 cnf(ssp8, plain, (spl0 | spl1 | spl2 | spl3 | spl5 | spl10), inference(avatar_split_clause, [status(thm)], [c23, sdef0, sdef1, sdef2, sdef3, sdef5, sdef10])).
% 24.53/8.81 cnf(c24, plain, ~cowlThing(sk2) | cowlNothing(sk2) | xsd_string(sk3) | ~xsd_string(sk3) | sk5 != sk6 | ~rp(sk8,X1) | ~rp(sk8,X2) | X1 = X2, inference(cnf_transformation, [status(esa)], [f10_sk])).
% 24.53/8.81 cnf(ssp9, plain, (spl0 | spl1 | spl2 | spl3 | spl6 | spl10), inference(avatar_split_clause, [status(thm)], [c24, sdef0, sdef1, sdef2, sdef3, sdef6, sdef10])).
% 24.53/8.81 cnf(c25, plain, ~cowlThing(sk2) | cowlNothing(sk2) | xsd_string(sk3) | ~xsd_string(sk3) | sk5 != sk7 | cc(sk8), inference(cnf_transformation, [status(esa)], [f10_sk])).
% 24.53/8.81 cnf(ssp10, plain, (spl0 | spl1 | spl2 | spl3 | spl5 | spl11), inference(avatar_split_clause, [status(thm)], [c25, sdef0, sdef1, sdef2, sdef3, sdef5, sdef11])).
% 24.53/8.81 cnf(c26, plain, ~cowlThing(sk2) | cowlNothing(sk2) | xsd_string(sk3) | ~xsd_string(sk3) | sk5 != sk7 | ~rp(sk8,X1) | ~rp(sk8,X2) | X1 = X2, inference(cnf_transformation, [status(esa)], [f10_sk])).
% 24.53/8.81 cnf(ssp11, plain, (spl0 | spl1 | spl2 | spl3 | spl6 | spl11), inference(avatar_split_clause, [status(thm)], [c26, sdef0, sdef1, sdef2, sdef3, sdef6, sdef11])).
% 24.53/8.81 cnf(c27, plain, ~cowlThing(sk2) | cowlNothing(sk2) | xsd_string(sk3) | ~xsd_string(sk3) | sk6 != sk7 | cc(sk8), inference(cnf_transformation, [status(esa)], [f10_sk])).
% 24.53/8.81 cnf(ssp12, plain, (spl0 | spl1 | spl2 | spl3 | spl5 | spl12), inference(avatar_split_clause, [status(thm)], [c27, sdef0, sdef1, sdef2, sdef3, sdef5, sdef12])).
% 24.53/8.81 cnf(c28, plain, ~cowlThing(sk2) | cowlNothing(sk2) | xsd_string(sk3) | ~xsd_string(sk3) | sk6 != sk7 | ~rp(sk8,X1) | ~rp(sk8,X2) | X1 = X2, inference(cnf_transformation, [status(esa)], [f10_sk])).
% 24.53/8.81 cnf(ssp13, plain, (spl0 | spl1 | spl2 | spl3 | spl6 | spl12), inference(avatar_split_clause, [status(thm)], [c28, sdef0, sdef1, sdef2, sdef3, sdef6, sdef12])).
% 24.53/8.81 cnf(c29, plain, ~cowlThing(sk2) | cowlNothing(sk2) | xsd_string(sk3) | ~xsd_integer(sk3) | cc(sk4) | cc(sk8), inference(cnf_transformation, [status(esa)], [f10_sk])).
% 24.53/8.81 cnf(ssp14, plain, (spl0 | spl1 | spl2 | spl4 | spl5 | spl13), inference(avatar_split_clause, [status(thm)], [c29, sdef0, sdef1, sdef2, sdef4, sdef5, sdef13])).
% 24.53/8.81 cnf(c30, plain, ~cowlThing(sk2) | cowlNothing(sk2) | xsd_string(sk3) | ~xsd_integer(sk3) | cc(sk4) | ~rp(sk8,X1) | ~rp(sk8,X2) | X1 = X2, inference(cnf_transformation, [status(esa)], [f10_sk])).
% 24.53/8.81 cnf(ssp15, plain, (spl0 | spl1 | spl2 | spl4 | spl6 | spl13), inference(avatar_split_clause, [status(thm)], [c30, sdef0, sdef1, sdef2, sdef4, sdef6, sdef13])).
% 24.53/8.81 cnf(c31, plain, ~cowlThing(sk2) | cowlNothing(sk2) | xsd_string(sk3) | ~xsd_integer(sk3) | rp(sk4,sk5) | cc(sk8), inference(cnf_transformation, [status(esa)], [f10_sk])).
% 24.53/8.81 cnf(ssp16, plain, (spl0 | spl1 | spl2 | spl5 | spl7 | spl13), inference(avatar_split_clause, [status(thm)], [c31, sdef0, sdef1, sdef2, sdef5, sdef7, sdef13])).
% 24.53/8.81 cnf(c32, plain, ~cowlThing(sk2) | cowlNothing(sk2) | xsd_string(sk3) | ~xsd_integer(sk3) | rp(sk4,sk5) | ~rp(sk8,X1) | ~rp(sk8,X2) | X1 = X2, inference(cnf_transformation, [status(esa)], [f10_sk])).
% 24.53/8.81 cnf(ssp17, plain, (spl0 | spl1 | spl2 | spl6 | spl7 | spl13), inference(avatar_split_clause, [status(thm)], [c32, sdef0, sdef1, sdef2, sdef6, sdef7, sdef13])).
% 24.53/8.81 cnf(c33, plain, ~cowlThing(sk2) | cowlNothing(sk2) | xsd_string(sk3) | ~xsd_integer(sk3) | rp(sk4,sk6) | cc(sk8), inference(cnf_transformation, [status(esa)], [f10_sk])).
% 24.53/8.81 cnf(ssp18, plain, (spl0 | spl1 | spl2 | spl5 | spl8 | spl13), inference(avatar_split_clause, [status(thm)], [c33, sdef0, sdef1, sdef2, sdef5, sdef8, sdef13])).
% 24.53/8.81 cnf(c34, plain, ~cowlThing(sk2) | cowlNothing(sk2) | xsd_string(sk3) | ~xsd_integer(sk3) | rp(sk4,sk6) | ~rp(sk8,X1) | ~rp(sk8,X2) | X1 = X2, inference(cnf_transformation, [status(esa)], [f10_sk])).
% 24.53/8.81 cnf(ssp19, plain, (spl0 | spl1 | spl2 | spl6 | spl8 | spl13), inference(avatar_split_clause, [status(thm)], [c34, sdef0, sdef1, sdef2, sdef6, sdef8, sdef13])).
% 24.53/8.81 cnf(c35, plain, ~cowlThing(sk2) | cowlNothing(sk2) | xsd_string(sk3) | ~xsd_integer(sk3) | rp(sk4,sk7) | cc(sk8), inference(cnf_transformation, [status(esa)], [f10_sk])).
% 24.53/8.81 cnf(ssp20, plain, (spl0 | spl1 | spl2 | spl5 | spl9 | spl13), inference(avatar_split_clause, [status(thm)], [c35, sdef0, sdef1, sdef2, sdef5, sdef9, sdef13])).
% 24.53/8.81 cnf(c36, plain, ~cowlThing(sk2) | cowlNothing(sk2) | xsd_string(sk3) | ~xsd_integer(sk3) | rp(sk4,sk7) | ~rp(sk8,X1) | ~rp(sk8,X2) | X1 = X2, inference(cnf_transformation, [status(esa)], [f10_sk])).
% 24.53/8.81 cnf(ssp21, plain, (spl0 | spl1 | spl2 | spl6 | spl9 | spl13), inference(avatar_split_clause, [status(thm)], [c36, sdef0, sdef1, sdef2, sdef6, sdef9, sdef13])).
% 24.53/8.81 cnf(c37, plain, ~cowlThing(sk2) | cowlNothing(sk2) | xsd_string(sk3) | ~xsd_integer(sk3) | sk5 != sk6 | cc(sk8), inference(cnf_transformation, [status(esa)], [f10_sk])).
% 24.53/8.81 cnf(ssp22, plain, (spl0 | spl1 | spl2 | spl5 | spl10 | spl13), inference(avatar_split_clause, [status(thm)], [c37, sdef0, sdef1, sdef2, sdef5, sdef10, sdef13])).
% 24.53/8.81 cnf(c38, plain, ~cowlThing(sk2) | cowlNothing(sk2) | xsd_string(sk3) | ~xsd_integer(sk3) | sk5 != sk6 | ~rp(sk8,X1) | ~rp(sk8,X2) | X1 = X2, inference(cnf_transformation, [status(esa)], [f10_sk])).
% 24.53/8.81 cnf(ssp23, plain, (spl0 | spl1 | spl2 | spl6 | spl10 | spl13), inference(avatar_split_clause, [status(thm)], [c38, sdef0, sdef1, sdef2, sdef6, sdef10, sdef13])).
% 24.53/8.81 cnf(c39, plain, ~cowlThing(sk2) | cowlNothing(sk2) | xsd_string(sk3) | ~xsd_integer(sk3) | sk5 != sk7 | cc(sk8), inference(cnf_transformation, [status(esa)], [f10_sk])).
% 24.53/8.81 cnf(ssp24, plain, (spl0 | spl1 | spl2 | spl5 | spl11 | spl13), inference(avatar_split_clause, [status(thm)], [c39, sdef0, sdef1, sdef2, sdef5, sdef11, sdef13])).
% 24.53/8.81 cnf(c40, plain, ~cowlThing(sk2) | cowlNothing(sk2) | xsd_string(sk3) | ~xsd_integer(sk3) | sk5 != sk7 | ~rp(sk8,X1) | ~rp(sk8,X2) | X1 = X2, inference(cnf_transformation, [status(esa)], [f10_sk])).
% 24.53/8.81 cnf(ssp25, plain, (spl0 | spl1 | spl2 | spl6 | spl11 | spl13), inference(avatar_split_clause, [status(thm)], [c40, sdef0, sdef1, sdef2, sdef6, sdef11, sdef13])).
% 24.53/8.81 cnf(c41, plain, ~cowlThing(sk2) | cowlNothing(sk2) | xsd_string(sk3) | ~xsd_integer(sk3) | sk6 != sk7 | cc(sk8), inference(cnf_transformation, [status(esa)], [f10_sk])).
% 24.53/8.81 cnf(ssp26, plain, (spl0 | spl1 | spl2 | spl5 | spl12 | spl13), inference(avatar_split_clause, [status(thm)], [c41, sdef0, sdef1, sdef2, sdef5, sdef12, sdef13])).
% 24.53/8.81 cnf(c42, plain, ~cowlThing(sk2) | cowlNothing(sk2) | xsd_string(sk3) | ~xsd_integer(sk3) | sk6 != sk7 | ~rp(sk8,X1) | ~rp(sk8,X2) | X1 = X2, inference(cnf_transformation, [status(esa)], [f10_sk])).
% 24.53/8.81 cnf(ssp27, plain, (spl0 | spl1 | spl2 | spl6 | spl12 | spl13), inference(avatar_split_clause, [status(thm)], [c42, sdef0, sdef1, sdef2, sdef6, sdef12, sdef13])).
% 24.53/8.81 cnf(c43, plain, ~cowlThing(sk2) | cowlNothing(sk2) | xsd_integer(sk3) | ~xsd_string(sk3) | cc(sk4) | cc(sk8), inference(cnf_transformation, [status(esa)], [f10_sk])).
% 24.53/8.81 cnf(ssp28, plain, (spl0 | spl1 | spl3 | spl4 | spl5 | spl14), inference(avatar_split_clause, [status(thm)], [c43, sdef0, sdef1, sdef3, sdef4, sdef5, sdef14])).
% 24.53/8.81 cnf(c44, plain, ~cowlThing(sk2) | cowlNothing(sk2) | xsd_integer(sk3) | ~xsd_string(sk3) | cc(sk4) | ~rp(sk8,X1) | ~rp(sk8,X2) | X1 = X2, inference(cnf_transformation, [status(esa)], [f10_sk])).
% 24.53/8.81 cnf(ssp29, plain, (spl0 | spl1 | spl3 | spl4 | spl6 | spl14), inference(avatar_split_clause, [status(thm)], [c44, sdef0, sdef1, sdef3, sdef4, sdef6, sdef14])).
% 24.53/8.81 cnf(c45, plain, ~cowlThing(sk2) | cowlNothing(sk2) | xsd_integer(sk3) | ~xsd_string(sk3) | rp(sk4,sk5) | cc(sk8), inference(cnf_transformation, [status(esa)], [f10_sk])).
% 24.53/8.81 cnf(ssp30, plain, (spl0 | spl1 | spl3 | spl5 | spl7 | spl14), inference(avatar_split_clause, [status(thm)], [c45, sdef0, sdef1, sdef3, sdef5, sdef7, sdef14])).
% 24.53/8.81 cnf(c46, plain, ~cowlThing(sk2) | cowlNothing(sk2) | xsd_integer(sk3) | ~xsd_string(sk3) | rp(sk4,sk5) | ~rp(sk8,X1) | ~rp(sk8,X2) | X1 = X2, inference(cnf_transformation, [status(esa)], [f10_sk])).
% 24.53/8.81 cnf(ssp31, plain, (spl0 | spl1 | spl3 | spl6 | spl7 | spl14), inference(avatar_split_clause, [status(thm)], [c46, sdef0, sdef1, sdef3, sdef6, sdef7, sdef14])).
% 24.53/8.81 cnf(c47, plain, ~cowlThing(sk2) | cowlNothing(sk2) | xsd_integer(sk3) | ~xsd_string(sk3) | rp(sk4,sk6) | cc(sk8), inference(cnf_transformation, [status(esa)], [f10_sk])).
% 24.53/8.81 cnf(ssp32, plain, (spl0 | spl1 | spl3 | spl5 | spl8 | spl14), inference(avatar_split_clause, [status(thm)], [c47, sdef0, sdef1, sdef3, sdef5, sdef8, sdef14])).
% 24.53/8.81 cnf(c48, plain, ~cowlThing(sk2) | cowlNothing(sk2) | xsd_integer(sk3) | ~xsd_string(sk3) | rp(sk4,sk6) | ~rp(sk8,X1) | ~rp(sk8,X2) | X1 = X2, inference(cnf_transformation, [status(esa)], [f10_sk])).
% 24.53/8.81 cnf(ssp33, plain, (spl0 | spl1 | spl3 | spl6 | spl8 | spl14), inference(avatar_split_clause, [status(thm)], [c48, sdef0, sdef1, sdef3, sdef6, sdef8, sdef14])).
% 24.53/8.81 cnf(c49, plain, ~cowlThing(sk2) | cowlNothing(sk2) | xsd_integer(sk3) | ~xsd_string(sk3) | rp(sk4,sk7) | cc(sk8), inference(cnf_transformation, [status(esa)], [f10_sk])).
% 24.53/8.81 cnf(ssp34, plain, (spl0 | spl1 | spl3 | spl5 | spl9 | spl14), inference(avatar_split_clause, [status(thm)], [c49, sdef0, sdef1, sdef3, sdef5, sdef9, sdef14])).
% 24.53/8.81 cnf(c50, plain, ~cowlThing(sk2) | cowlNothing(sk2) | xsd_integer(sk3) | ~xsd_string(sk3) | rp(sk4,sk7) | ~rp(sk8,X1) | ~rp(sk8,X2) | X1 = X2, inference(cnf_transformation, [status(esa)], [f10_sk])).
% 24.53/8.81 cnf(ssp35, plain, (spl0 | spl1 | spl3 | spl6 | spl9 | spl14), inference(avatar_split_clause, [status(thm)], [c50, sdef0, sdef1, sdef3, sdef6, sdef9, sdef14])).
% 24.53/8.81 cnf(c51, plain, ~cowlThing(sk2) | cowlNothing(sk2) | xsd_integer(sk3) | ~xsd_string(sk3) | sk5 != sk6 | cc(sk8), inference(cnf_transformation, [status(esa)], [f10_sk])).
% 24.53/8.81 cnf(ssp36, plain, (spl0 | spl1 | spl3 | spl5 | spl10 | spl14), inference(avatar_split_clause, [status(thm)], [c51, sdef0, sdef1, sdef3, sdef5, sdef10, sdef14])).
% 24.53/8.81 cnf(c52, plain, ~cowlThing(sk2) | cowlNothing(sk2) | xsd_integer(sk3) | ~xsd_string(sk3) | sk5 != sk6 | ~rp(sk8,X1) | ~rp(sk8,X2) | X1 = X2, inference(cnf_transformation, [status(esa)], [f10_sk])).
% 24.53/8.81 cnf(ssp37, plain, (spl0 | spl1 | spl3 | spl6 | spl10 | spl14), inference(avatar_split_clause, [status(thm)], [c52, sdef0, sdef1, sdef3, sdef6, sdef10, sdef14])).
% 24.53/8.81 cnf(c53, plain, ~cowlThing(sk2) | cowlNothing(sk2) | xsd_integer(sk3) | ~xsd_string(sk3) | sk5 != sk7 | cc(sk8), inference(cnf_transformation, [status(esa)], [f10_sk])).
% 24.53/8.81 cnf(ssp38, plain, (spl0 | spl1 | spl3 | spl5 | spl11 | spl14), inference(avatar_split_clause, [status(thm)], [c53, sdef0, sdef1, sdef3, sdef5, sdef11, sdef14])).
% 24.53/8.81 cnf(c54, plain, ~cowlThing(sk2) | cowlNothing(sk2) | xsd_integer(sk3) | ~xsd_string(sk3) | sk5 != sk7 | ~rp(sk8,X1) | ~rp(sk8,X2) | X1 = X2, inference(cnf_transformation, [status(esa)], [f10_sk])).
% 24.53/8.81 cnf(ssp39, plain, (spl0 | spl1 | spl3 | spl6 | spl11 | spl14), inference(avatar_split_clause, [status(thm)], [c54, sdef0, sdef1, sdef3, sdef6, sdef11, sdef14])).
% 24.53/8.81 cnf(c55, plain, ~cowlThing(sk2) | cowlNothing(sk2) | xsd_integer(sk3) | ~xsd_string(sk3) | sk6 != sk7 | cc(sk8), inference(cnf_transformation, [status(esa)], [f10_sk])).
% 24.53/8.81 cnf(ssp40, plain, (spl0 | spl1 | spl3 | spl5 | spl12 | spl14), inference(avatar_split_clause, [status(thm)], [c55, sdef0, sdef1, sdef3, sdef5, sdef12, sdef14])).
% 24.53/8.81 cnf(c56, plain, ~cowlThing(sk2) | cowlNothing(sk2) | xsd_integer(sk3) | ~xsd_string(sk3) | sk6 != sk7 | ~rp(sk8,X1) | ~rp(sk8,X2) | X1 = X2, inference(cnf_transformation, [status(esa)], [f10_sk])).
% 24.53/8.81 cnf(ssp41, plain, (spl0 | spl1 | spl3 | spl6 | spl12 | spl14), inference(avatar_split_clause, [status(thm)], [c56, sdef0, sdef1, sdef3, sdef6, sdef12, sdef14])).
% 24.53/8.81 cnf(c57, plain, ~cowlThing(sk2) | cowlNothing(sk2) | xsd_integer(sk3) | ~xsd_integer(sk3) | cc(sk4) | cc(sk8), inference(cnf_transformation, [status(esa)], [f10_sk])).
% 24.53/8.81 cnf(ssp42, plain, (spl0 | spl1 | spl4 | spl5 | spl13 | spl14), inference(avatar_split_clause, [status(thm)], [c57, sdef0, sdef1, sdef4, sdef5, sdef13, sdef14])).
% 24.53/8.81 cnf(c58, plain, ~cowlThing(sk2) | cowlNothing(sk2) | xsd_integer(sk3) | ~xsd_integer(sk3) | cc(sk4) | ~rp(sk8,X1) | ~rp(sk8,X2) | X1 = X2, inference(cnf_transformation, [status(esa)], [f10_sk])).
% 24.53/8.81 cnf(ssp43, plain, (spl0 | spl1 | spl4 | spl6 | spl13 | spl14), inference(avatar_split_clause, [status(thm)], [c58, sdef0, sdef1, sdef4, sdef6, sdef13, sdef14])).
% 24.53/8.81 cnf(c59, plain, ~cowlThing(sk2) | cowlNothing(sk2) | xsd_integer(sk3) | ~xsd_integer(sk3) | rp(sk4,sk5) | cc(sk8), inference(cnf_transformation, [status(esa)], [f10_sk])).
% 24.53/8.81 cnf(ssp44, plain, (spl0 | spl1 | spl5 | spl7 | spl13 | spl14), inference(avatar_split_clause, [status(thm)], [c59, sdef0, sdef1, sdef5, sdef7, sdef13, sdef14])).
% 24.53/8.81 cnf(c60, plain, ~cowlThing(sk2) | cowlNothing(sk2) | xsd_integer(sk3) | ~xsd_integer(sk3) | rp(sk4,sk5) | ~rp(sk8,X1) | ~rp(sk8,X2) | X1 = X2, inference(cnf_transformation, [status(esa)], [f10_sk])).
% 24.53/8.81 cnf(ssp45, plain, (spl0 | spl1 | spl6 | spl7 | spl13 | spl14), inference(avatar_split_clause, [status(thm)], [c60, sdef0, sdef1, sdef6, sdef7, sdef13, sdef14])).
% 24.53/8.81 cnf(c61, plain, ~cowlThing(sk2) | cowlNothing(sk2) | xsd_integer(sk3) | ~xsd_integer(sk3) | rp(sk4,sk6) | cc(sk8), inference(cnf_transformation, [status(esa)], [f10_sk])).
% 24.53/8.81 cnf(ssp46, plain, (spl0 | spl1 | spl5 | spl8 | spl13 | spl14), inference(avatar_split_clause, [status(thm)], [c61, sdef0, sdef1, sdef5, sdef8, sdef13, sdef14])).
% 24.53/8.81 cnf(c62, plain, ~cowlThing(sk2) | cowlNothing(sk2) | xsd_integer(sk3) | ~xsd_integer(sk3) | rp(sk4,sk6) | ~rp(sk8,X1) | ~rp(sk8,X2) | X1 = X2, inference(cnf_transformation, [status(esa)], [f10_sk])).
% 24.53/8.81 cnf(ssp47, plain, (spl0 | spl1 | spl6 | spl8 | spl13 | spl14), inference(avatar_split_clause, [status(thm)], [c62, sdef0, sdef1, sdef6, sdef8, sdef13, sdef14])).
% 24.53/8.81 cnf(c63, plain, ~cowlThing(sk2) | cowlNothing(sk2) | xsd_integer(sk3) | ~xsd_integer(sk3) | rp(sk4,sk7) | cc(sk8), inference(cnf_transformation, [status(esa)], [f10_sk])).
% 24.53/8.81 cnf(ssp48, plain, (spl0 | spl1 | spl5 | spl9 | spl13 | spl14), inference(avatar_split_clause, [status(thm)], [c63, sdef0, sdef1, sdef5, sdef9, sdef13, sdef14])).
% 24.53/8.81 cnf(c64, plain, ~cowlThing(sk2) | cowlNothing(sk2) | xsd_integer(sk3) | ~xsd_integer(sk3) | rp(sk4,sk7) | ~rp(sk8,X1) | ~rp(sk8,X2) | X1 = X2, inference(cnf_transformation, [status(esa)], [f10_sk])).
% 24.53/8.81 cnf(ssp49, plain, (spl0 | spl1 | spl6 | spl9 | spl13 | spl14), inference(avatar_split_clause, [status(thm)], [c64, sdef0, sdef1, sdef6, sdef9, sdef13, sdef14])).
% 24.53/8.81 cnf(c65, plain, ~cowlThing(sk2) | cowlNothing(sk2) | xsd_integer(sk3) | ~xsd_integer(sk3) | sk5 != sk6 | cc(sk8), inference(cnf_transformation, [status(esa)], [f10_sk])).
% 24.53/8.81 cnf(ssp50, plain, (spl0 | spl1 | spl5 | spl10 | spl13 | spl14), inference(avatar_split_clause, [status(thm)], [c65, sdef0, sdef1, sdef5, sdef10, sdef13, sdef14])).
% 24.53/8.81 cnf(c66, plain, ~cowlThing(sk2) | cowlNothing(sk2) | xsd_integer(sk3) | ~xsd_integer(sk3) | sk5 != sk6 | ~rp(sk8,X1) | ~rp(sk8,X2) | X1 = X2, inference(cnf_transformation, [status(esa)], [f10_sk])).
% 24.53/8.81 cnf(ssp51, plain, (spl0 | spl1 | spl6 | spl10 | spl13 | spl14), inference(avatar_split_clause, [status(thm)], [c66, sdef0, sdef1, sdef6, sdef10, sdef13, sdef14])).
% 24.53/8.81 cnf(c67, plain, ~cowlThing(sk2) | cowlNothing(sk2) | xsd_integer(sk3) | ~xsd_integer(sk3) | sk5 != sk7 | cc(sk8), inference(cnf_transformation, [status(esa)], [f10_sk])).
% 24.53/8.81 cnf(ssp52, plain, (spl0 | spl1 | spl5 | spl11 | spl13 | spl14), inference(avatar_split_clause, [status(thm)], [c67, sdef0, sdef1, sdef5, sdef11, sdef13, sdef14])).
% 24.53/8.81 cnf(c68, plain, ~cowlThing(sk2) | cowlNothing(sk2) | xsd_integer(sk3) | ~xsd_integer(sk3) | sk5 != sk7 | ~rp(sk8,X1) | ~rp(sk8,X2) | X1 = X2, inference(cnf_transformation, [status(esa)], [f10_sk])).
% 24.53/8.81 cnf(ssp53, plain, (spl0 | spl1 | spl6 | spl11 | spl13 | spl14), inference(avatar_split_clause, [status(thm)], [c68, sdef0, sdef1, sdef6, sdef11, sdef13, sdef14])).
% 24.53/8.81 cnf(c69, plain, ~cowlThing(sk2) | cowlNothing(sk2) | xsd_integer(sk3) | ~xsd_integer(sk3) | sk6 != sk7 | cc(sk8), inference(cnf_transformation, [status(esa)], [f10_sk])).
% 24.53/8.81 cnf(ssp54, plain, (spl0 | spl1 | spl5 | spl12 | spl13 | spl14), inference(avatar_split_clause, [status(thm)], [c69, sdef0, sdef1, sdef5, sdef12, sdef13, sdef14])).
% 24.53/8.81 cnf(c70, plain, ~cowlThing(sk2) | cowlNothing(sk2) | xsd_integer(sk3) | ~xsd_integer(sk3) | sk6 != sk7 | ~rp(sk8,X1) | ~rp(sk8,X2) | X1 = X2, inference(cnf_transformation, [status(esa)], [f10_sk])).
% 24.53/8.81 cnf(ssp55, plain, (spl0 | spl1 | spl6 | spl12 | spl13 | spl14), inference(avatar_split_clause, [status(thm)], [c70, sdef0, sdef1, sdef6, sdef12, sdef13, sdef14])).
% 24.53/8.81 cnf(p93, plain, (~rp(sk8,X0) | sk0(sk8) = X0 | ~spl5 | ~spl6), inference(resolution, [status(thm)], [p92, p23])).
% 24.53/8.81 cnf(p97, plain, (sk0(sk8) = sk1(sk8) | ~spl5 | ~spl6), inference(resolution, [status(thm)], [p95, p93])).
% 24.53/8.81 fof(f0, axiom, ! [A,B] : ( ( A = B & cc(A) ) => cc(B) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', cc_substitution_1)).
% 24.53/8.81 fof(f0_nnf, plain, ! [A,B] : (((A != B | ~(cc(A))) | cc(B))), inference(nnf_transformation, [status(thm)], [f0])).
% 24.53/8.81 fof(f0_sk, plain, ! [A,B] : (((A != B | ~(cc(A))) | cc(B))), inference(skolemisation, [status(esa)], [f0_nnf])).
% 24.53/8.81 cnf(c0, plain, X0 != X1 | ~cc(X0) | cc(X1), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 24.53/8.81 cnf(p98, plain, (~cc(sk0(sk8)) | cc(sk1(sk8)) | ~spl5 | ~spl6), inference(resolution, [status(thm)], [p97, c0])).
% 24.53/8.81 fof(sdef15, definition, (spl15 <=> (~cc(sk0(sk8)))), introduced(definition, [new_symbols(naming, [spl15])], [avatar_definition])).
% 24.53/8.81 fof(sdef16, definition, (spl16 <=> (cc(sk1(sk8)))), introduced(definition, [new_symbols(naming, [spl16])], [avatar_definition])).
% 24.53/8.81 cnf(ssp56, plain, (~spl5 | ~spl6 | spl15 | spl16), inference(avatar_split_clause, [status(thm)], [p98, sdef15, sdef16])).
% 24.53/8.81 fof(f5, axiom, ! [A,B] : ( ( A = B & xsd_integer(A) ) => xsd_integer(B) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', xsd_integer_substitution_1)).
% 24.53/8.81 fof(f5_nnf, plain, ! [A,B] : (((A != B | ~(xsd_integer(A))) | xsd_integer(B))), inference(nnf_transformation, [status(thm)], [f5])).
% 24.53/8.81 fof(f5_sk, plain, ! [A,B] : (((A != B | ~(xsd_integer(A))) | xsd_integer(B))), inference(skolemisation, [status(esa)], [f5_nnf])).
% 24.53/8.81 cnf(c5, plain, X0 != X1 | ~xsd_integer(X0) | xsd_integer(X1), inference(cnf_transformation, [status(esa)], [f5_sk])).
% 24.53/8.81 cnf(p103, plain, (~xsd_integer(sk0(sk8)) | xsd_integer(sk1(sk8)) | ~spl5 | ~spl6), inference(resolution, [status(thm)], [p97, c5])).
% 24.53/8.81 cnf(ssp57, plain, (~spl5 | ~spl6 | spl17 | spl18), inference(avatar_split_clause, [status(thm)], [p103, sdef17, sdef18])).
% 24.53/8.81 fof(f6, axiom, ! [A,B] : ( ( A = B & xsd_string(A) ) => xsd_string(B) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', xsd_string_substitution_1)).
% 24.53/8.81 fof(f6_nnf, plain, ! [A,B] : (((A != B | ~(xsd_string(A))) | xsd_string(B))), inference(nnf_transformation, [status(thm)], [f6])).
% 24.53/8.81 fof(f6_sk, plain, ! [A,B] : (((A != B | ~(xsd_string(A))) | xsd_string(B))), inference(skolemisation, [status(esa)], [f6_nnf])).
% 24.53/8.81 cnf(c6, plain, X0 != X1 | ~xsd_string(X0) | xsd_string(X1), inference(cnf_transformation, [status(esa)], [f6_sk])).
% 24.53/8.81 cnf(p106, plain, (~xsd_string(sk0(sk8)) | xsd_string(sk1(sk8)) | ~spl5 | ~spl6), inference(resolution, [status(thm)], [c6, p97])).
% 24.53/8.81 cnf(ssp58, plain, (~spl5 | ~spl6 | spl19 | spl20), inference(avatar_split_clause, [status(thm)], [p106, sdef19, sdef20])).
% 24.53/8.81 cnf(c14, 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])).
% 24.53/8.81 cnf(p20, plain, (cc(sk4) | ~spl4), inference(avatar_component_clause, [status(thm)], [sdef4])).
% 24.53/8.81 cnf(p124, plain, (~rp(sk4,X0) | ~rp(sk4,X1) | ~rp(sk4,X2) | X0 = X1 | X0 = X2 | X1 = X2 | ~spl4), inference(resolution, [status(thm)], [c14, p20])).
% 24.53/8.81 cnf(p25, plain, (rp(sk4,sk5) | ~spl7), inference(avatar_component_clause, [status(thm)], [sdef7])).
% 24.53/8.81 cnf(p134, plain, (~rp(sk4,X0) | ~rp(sk4,X1) | sk5 = X0 | sk5 = X1 | X0 = X1 | ~spl4 | ~spl7), inference(resolution, [status(thm)], [p124, p25])).
% 24.53/8.81 cnf(p28, plain, (rp(sk4,sk6) | ~spl8), inference(avatar_component_clause, [status(thm)], [sdef8])).
% 24.53/8.81 cnf(p140, plain, (~rp(sk4,X0) | sk5 = sk6 | sk5 = X0 | sk6 = X0 | ~spl4 | ~spl7 | ~spl8), inference(resolution, [status(thm)], [p134, p28])).
% 24.53/8.81 fof(sdef21, definition, (spl21 <=> (~rp(sk4,X0) | sk5 = X0 | sk6 = X0)), introduced(definition, [new_symbols(naming, [spl21])], [avatar_definition])).
% 24.53/8.81 cnf(ssp59, plain, (~spl4 | ~spl7 | ~spl8 | spl21 | spl22), inference(avatar_split_clause, [status(thm)], [p140, sdef21, sdef22])).
% 24.53/8.81 cnf(p31, plain, (rp(sk4,sk7) | ~spl9), inference(avatar_component_clause, [status(thm)], [sdef9])).
% 24.53/8.81 cnf(p143, plain, (~rp(sk4,X0) | sk5 = sk7 | sk5 = X0 | sk7 = X0 | ~spl4 | ~spl7 | ~spl9), inference(resolution, [status(thm)], [p134, p31])).
% 24.53/8.81 fof(sdef23, definition, (spl23 <=> (~rp(sk4,X0) | sk5 = X0 | sk7 = X0)), introduced(definition, [new_symbols(naming, [spl23])], [avatar_definition])).
% 24.53/8.81 cnf(ssp60, plain, (~spl4 | ~spl7 | ~spl9 | spl23 | spl24), inference(avatar_split_clause, [status(thm)], [p143, sdef23, sdef24])).
% 24.53/8.81 cnf(p91, plain, (rp(sk4,sk0(sk4)) | ~spl4), inference(resolution, [status(thm)], [c11, p20])).
% 24.53/8.81 cnf(p146, plain, (~rp(sk4,X0) | sk5 = sk0(sk4) | sk5 = X0 | sk0(sk4) = X0 | ~spl4 | ~spl7), inference(resolution, [status(thm)], [p134, p91])).
% 24.53/8.81 fof(sdef25, definition, (spl25 <=> (~rp(sk4,X0) | sk5 = X0 | sk0(sk4) = X0)), introduced(definition, [new_symbols(naming, [spl25])], [avatar_definition])).
% 24.53/8.81 fof(sdef26, definition, (spl26 <=> (sk5 = sk0(sk4))), introduced(definition, [new_symbols(naming, [spl26])], [avatar_definition])).
% 24.53/8.81 cnf(ssp61, plain, (~spl4 | ~spl7 | spl25 | spl26), inference(avatar_split_clause, [status(thm)], [p146, sdef25, sdef26])).
% 24.53/8.81 cnf(p94, plain, (rp(sk4,sk1(sk4)) | ~spl4), inference(resolution, [status(thm)], [c12, p20])).
% 24.53/8.81 cnf(p149, plain, (~rp(sk4,X0) | sk5 = sk1(sk4) | sk5 = X0 | sk1(sk4) = X0 | ~spl4 | ~spl7), inference(resolution, [status(thm)], [p134, p94])).
% 24.53/8.81 fof(sdef27, definition, (spl27 <=> (~rp(sk4,X0) | sk5 = X0 | sk1(sk4) = X0)), introduced(definition, [new_symbols(naming, [spl27])], [avatar_definition])).
% 24.53/8.81 cnf(ssp62, plain, (~spl4 | ~spl7 | spl27 | spl28), inference(avatar_split_clause, [status(thm)], [p149, sdef27, sdef28])).
% 24.53/8.81 cnf(p152, plain, (~cc(sk5) | cc(sk6) | ~spl22), inference(resolution, [status(thm)], [p142, c0])).
% 24.53/8.81 cnf(ssp63, plain, (~spl22 | spl29 | spl30), inference(avatar_split_clause, [status(thm)], [p152, sdef29, sdef30])).
% 24.53/8.81 cnf(p166, plain, (~cc(sk5) | cc(sk7) | ~spl24), inference(resolution, [status(thm)], [p145, c0])).
% 24.53/8.81 cnf(ssp64, plain, (~spl24 | spl29 | spl31), inference(avatar_split_clause, [status(thm)], [p166, sdef29, sdef31])).
% 24.53/8.81 cnf(p148, plain, (sk5 = sk0(sk4) | ~spl26), inference(avatar_component_clause, [status(thm)], [sdef26])).
% 24.53/8.81 cnf(p177, plain, (~cc(sk5) | cc(sk0(sk4)) | ~spl26), inference(resolution, [status(thm)], [p148, c0])).
% 24.53/8.81 fof(sdef32, definition, (spl32 <=> (cc(sk0(sk4)))), introduced(definition, [new_symbols(naming, [spl32])], [avatar_definition])).
% 24.53/8.81 cnf(ssp65, plain, (~spl26 | spl29 | spl32), inference(avatar_split_clause, [status(thm)], [p177, sdef29, sdef32])).
% 24.53/8.81 cnf(p182, plain, (~xsd_integer(sk5) | xsd_integer(sk0(sk4)) | ~spl26), inference(resolution, [status(thm)], [p148, c5])).
% 24.53/8.81 cnf(ssp66, plain, (~spl26 | spl33 | spl34), inference(avatar_split_clause, [status(thm)], [p182, sdef33, sdef34])).
% 24.53/8.81 cnf(p185, plain, (~xsd_string(sk5) | xsd_string(sk0(sk4)) | ~spl26), inference(resolution, [status(thm)], [p148, c6])).
% 24.53/8.81 cnf(ssp67, plain, (~spl26 | spl35 | spl36), inference(avatar_split_clause, [status(thm)], [p185, sdef35, sdef36])).
% 24.53/8.81 cnf(p206, plain, (~cc(sk5) | cc(sk1(sk4)) | ~spl28), inference(resolution, [status(thm)], [p151, c0])).
% 24.53/8.81 cnf(ssp68, plain, (~spl28 | spl29 | spl37), inference(avatar_split_clause, [status(thm)], [p206, sdef29, sdef37])).
% 24.53/8.81 cnf(p210, plain, (~xsd_integer(sk5) | xsd_integer(sk1(sk4)) | ~spl28), inference(resolution, [status(thm)], [p151, c5])).
% 24.53/8.81 cnf(ssp69, plain, (~spl28 | spl33 | spl38), inference(avatar_split_clause, [status(thm)], [p210, sdef33, sdef38])).
% 24.53/8.81 cnf(p213, plain, (~xsd_string(sk5) | xsd_string(sk1(sk4)) | ~spl28), inference(resolution, [status(thm)], [p151, c6])).
% 24.53/8.81 cnf(ssp70, plain, (~spl28 | spl35 | spl39), inference(avatar_split_clause, [status(thm)], [p213, sdef35, sdef39])).
% 24.53/8.81 cnf(p135, plain, (~rp(sk4,X0) | ~rp(sk4,X1) | sk6 = X0 | sk6 = X1 | X0 = X1 | ~spl4 | ~spl8), inference(resolution, [status(thm)], [p124, p28])).
% 24.53/8.81 cnf(p228, plain, (~rp(sk4,X0) | sk6 = sk5 | sk6 = X0 | sk5 = X0 | ~spl4 | ~spl7 | ~spl8), inference(resolution, [status(thm)], [p135, p25])).
% 24.53/8.81 cnf(ssp71, plain, (~spl4 | ~spl7 | ~spl8 | spl21 | spl40), inference(avatar_split_clause, [status(thm)], [p228, sdef21, sdef40])).
% 24.53/8.81 cnf(p230, plain, (~rp(sk4,X0) | sk6 = sk7 | sk6 = X0 | sk7 = X0 | ~spl4 | ~spl8 | ~spl9), inference(resolution, [status(thm)], [p135, p31])).
% 24.53/8.81 fof(sdef41, definition, (spl41 <=> (~rp(sk4,X0) | sk6 = X0 | sk7 = X0)), introduced(definition, [new_symbols(naming, [spl41])], [avatar_definition])).
% 24.53/8.81 cnf(ssp72, plain, (~spl4 | ~spl8 | ~spl9 | spl41 | spl42), inference(avatar_split_clause, [status(thm)], [p230, sdef41, sdef42])).
% 24.53/8.81 cnf(p233, plain, (~rp(sk4,X0) | sk6 = sk0(sk4) | sk6 = X0 | sk0(sk4) = X0 | ~spl4 | ~spl8), inference(resolution, [status(thm)], [p135, p91])).
% 24.53/8.81 fof(sdef43, definition, (spl43 <=> (~rp(sk4,X0) | sk6 = X0 | sk0(sk4) = X0)), introduced(definition, [new_symbols(naming, [spl43])], [avatar_definition])).
% 24.53/8.81 fof(sdef44, definition, (spl44 <=> (sk6 = sk0(sk4))), introduced(definition, [new_symbols(naming, [spl44])], [avatar_definition])).
% 24.53/8.81 cnf(ssp73, plain, (~spl4 | ~spl8 | spl43 | spl44), inference(avatar_split_clause, [status(thm)], [p233, sdef43, sdef44])).
% 24.53/8.81 cnf(p236, plain, (~rp(sk4,X0) | sk6 = sk1(sk4) | sk6 = X0 | sk1(sk4) = X0 | ~spl4 | ~spl8), inference(resolution, [status(thm)], [p135, p94])).
% 24.53/8.81 fof(sdef45, definition, (spl45 <=> (~rp(sk4,X0) | sk6 = X0 | sk1(sk4) = X0)), introduced(definition, [new_symbols(naming, [spl45])], [avatar_definition])).
% 24.53/8.81 fof(sdef46, definition, (spl46 <=> (sk6 = sk1(sk4))), introduced(definition, [new_symbols(naming, [spl46])], [avatar_definition])).
% 24.53/8.81 cnf(ssp74, plain, (~spl4 | ~spl8 | spl45 | spl46), inference(avatar_split_clause, [status(thm)], [p236, sdef45, sdef46])).
% 24.53/8.81 cnf(p250, plain, (~cc(sk6) | cc(sk7) | ~spl42), inference(resolution, [status(thm)], [p232, c0])).
% 24.53/8.81 cnf(ssp75, plain, (~spl42 | spl31 | spl47), inference(avatar_split_clause, [status(thm)], [p250, sdef31, sdef47])).
% 24.53/8.81 cnf(p136, plain, (~rp(sk4,X0) | ~rp(sk4,X1) | sk7 = X0 | sk7 = X1 | X0 = X1 | ~spl4 | ~spl9), inference(resolution, [status(thm)], [p124, p31])).
% 24.53/8.81 cnf(p255, plain, (~rp(sk4,X0) | sk7 = sk5 | sk7 = X0 | sk5 = X0 | ~spl4 | ~spl7 | ~spl9), inference(resolution, [status(thm)], [p136, p25])).
% 24.53/8.81 cnf(ssp76, plain, (~spl4 | ~spl7 | ~spl9 | spl23 | spl48), inference(avatar_split_clause, [status(thm)], [p255, sdef23, sdef48])).
% 24.53/8.81 cnf(p257, plain, (~rp(sk4,X0) | sk7 = sk6 | sk7 = X0 | sk6 = X0 | ~spl4 | ~spl8 | ~spl9), inference(resolution, [status(thm)], [p136, p28])).
% 24.53/8.81 cnf(ssp77, plain, (~spl4 | ~spl8 | ~spl9 | spl41 | spl49), inference(avatar_split_clause, [status(thm)], [p257, sdef41, sdef49])).
% 24.53/8.81 cnf(p259, plain, (~rp(sk4,X0) | sk7 = sk0(sk4) | sk7 = X0 | sk0(sk4) = X0 | ~spl4 | ~spl9), inference(resolution, [status(thm)], [p136, p91])).
% 24.53/8.81 fof(sdef50, definition, (spl50 <=> (~rp(sk4,X0) | sk7 = X0 | sk0(sk4) = X0)), introduced(definition, [new_symbols(naming, [spl50])], [avatar_definition])).
% 24.53/8.81 fof(sdef51, definition, (spl51 <=> (sk7 = sk0(sk4))), introduced(definition, [new_symbols(naming, [spl51])], [avatar_definition])).
% 24.53/8.81 cnf(ssp78, plain, (~spl4 | ~spl9 | spl50 | spl51), inference(avatar_split_clause, [status(thm)], [p259, sdef50, sdef51])).
% 24.53/8.81 cnf(p262, plain, (~rp(sk4,X0) | sk7 = sk1(sk4) | sk7 = X0 | sk1(sk4) = X0 | ~spl4 | ~spl9), inference(resolution, [status(thm)], [p136, p94])).
% 24.53/8.81 fof(sdef52, definition, (spl52 <=> (~rp(sk4,X0) | sk7 = X0 | sk1(sk4) = X0)), introduced(definition, [new_symbols(naming, [spl52])], [avatar_definition])).
% 24.53/8.81 fof(sdef53, definition, (spl53 <=> (sk7 = sk1(sk4))), introduced(definition, [new_symbols(naming, [spl53])], [avatar_definition])).
% 24.53/8.81 cnf(ssp79, plain, (~spl4 | ~spl9 | spl52 | spl53), inference(avatar_split_clause, [status(thm)], [p262, sdef52, sdef53])).
% 24.53/8.81 cnf(p240, plain, (rp(sk4,sk5) | ~spl8 | ~spl40), inference(superposition, [status(thm)], [p229, p28])).
% 24.53/8.81 cnf(p270, plain, (~rp(sk4,X0) | sk7 = sk5 | sk7 = X0 | sk5 = X0 | ~spl4 | ~spl8 | ~spl9 | ~spl40), inference(resolution, [status(thm)], [p240, p136])).
% 24.53/8.81 cnf(ssp80, plain, (~spl4 | ~spl8 | ~spl9 | ~spl40 | spl23 | spl48), inference(avatar_split_clause, [status(thm)], [p270, sdef23, sdef48])).
% 24.53/8.81 cnf(p137, plain, (~rp(sk4,X0) | ~rp(sk4,X1) | sk0(sk4) = X0 | sk0(sk4) = X1 | X0 = X1 | ~spl4), inference(resolution, [status(thm)], [p124, p91])).
% 24.53/8.81 cnf(p271, plain, (~rp(sk4,X0) | sk0(sk4) = sk5 | sk0(sk4) = X0 | sk5 = X0 | ~spl4 | ~spl7), inference(resolution, [status(thm)], [p137, p25])).
% 24.53/8.81 fof(sdef54, definition, (spl54 <=> (sk0(sk4) = sk5)), introduced(definition, [new_symbols(naming, [spl54])], [avatar_definition])).
% 24.53/8.81 cnf(ssp81, plain, (~spl4 | ~spl7 | spl25 | spl54), inference(avatar_split_clause, [status(thm)], [p271, sdef25, sdef54])).
% 24.53/8.81 cnf(p273, plain, (~rp(sk4,X0) | sk0(sk4) = sk6 | sk0(sk4) = X0 | sk6 = X0 | ~spl4 | ~spl8), inference(resolution, [status(thm)], [p137, p28])).
% 24.53/8.81 fof(sdef55, definition, (spl55 <=> (sk0(sk4) = sk6)), introduced(definition, [new_symbols(naming, [spl55])], [avatar_definition])).
% 24.53/8.81 cnf(ssp82, plain, (~spl4 | ~spl8 | spl43 | spl55), inference(avatar_split_clause, [status(thm)], [p273, sdef43, sdef55])).
% 24.53/8.81 cnf(p275, plain, (~rp(sk4,X0) | sk0(sk4) = sk7 | sk0(sk4) = X0 | sk7 = X0 | ~spl4 | ~spl9), inference(resolution, [status(thm)], [p137, p31])).
% 24.53/8.81 fof(sdef56, definition, (spl56 <=> (sk0(sk4) = sk7)), introduced(definition, [new_symbols(naming, [spl56])], [avatar_definition])).
% 24.53/8.81 cnf(ssp83, plain, (~spl4 | ~spl9 | spl50 | spl56), inference(avatar_split_clause, [status(thm)], [p275, sdef50, sdef56])).
% 24.53/8.81 cnf(p277, plain, (~rp(sk4,X0) | sk0(sk4) = sk1(sk4) | sk0(sk4) = X0 | sk1(sk4) = X0 | ~spl4), inference(resolution, [status(thm)], [p137, p94])).
% 24.53/8.81 fof(sdef57, definition, (spl57 <=> (~rp(sk4,X0) | sk0(sk4) = X0 | sk1(sk4) = X0)), introduced(definition, [new_symbols(naming, [spl57])], [avatar_definition])).
% 24.53/8.81 fof(sdef58, definition, (spl58 <=> (sk0(sk4) = sk1(sk4))), introduced(definition, [new_symbols(naming, [spl58])], [avatar_definition])).
% 24.53/8.81 cnf(ssp84, plain, (~spl4 | spl57 | spl58), inference(avatar_split_clause, [status(thm)], [p277, sdef57, sdef58])).
% 24.53/8.81 cnf(p280, plain, (~rp(sk4,X0) | sk0(sk4) = sk5 | sk0(sk4) = X0 | sk5 = X0 | ~spl4 | ~spl8 | ~spl40), inference(resolution, [status(thm)], [p137, p240])).
% 24.53/8.81 cnf(ssp85, plain, (~spl4 | ~spl8 | ~spl40 | spl25 | spl54), inference(avatar_split_clause, [status(thm)], [p280, sdef25, sdef54])).
% 24.53/8.81 cnf(p138, plain, (~rp(sk4,X0) | ~rp(sk4,X1) | sk1(sk4) = X0 | sk1(sk4) = X1 | X0 = X1 | ~spl4), inference(resolution, [status(thm)], [p124, p94])).
% 24.53/8.81 cnf(p298, plain, (~rp(sk4,X0) | sk1(sk4) = sk5 | sk1(sk4) = X0 | sk5 = X0 | ~spl4 | ~spl7), inference(resolution, [status(thm)], [p138, p25])).
% 24.53/8.81 fof(sdef59, definition, (spl59 <=> (sk1(sk4) = sk5)), introduced(definition, [new_symbols(naming, [spl59])], [avatar_definition])).
% 24.53/8.81 cnf(ssp86, plain, (~spl4 | ~spl7 | spl27 | spl59), inference(avatar_split_clause, [status(thm)], [p298, sdef27, sdef59])).
% 24.53/8.81 cnf(p300, plain, (~rp(sk4,X0) | sk1(sk4) = sk6 | sk1(sk4) = X0 | sk6 = X0 | ~spl4 | ~spl8), inference(resolution, [status(thm)], [p138, p28])).
% 24.53/8.81 fof(sdef60, definition, (spl60 <=> (sk1(sk4) = sk6)), introduced(definition, [new_symbols(naming, [spl60])], [avatar_definition])).
% 24.53/8.81 cnf(ssp87, plain, (~spl4 | ~spl8 | spl45 | spl60), inference(avatar_split_clause, [status(thm)], [p300, sdef45, sdef60])).
% 24.53/8.81 cnf(p302, plain, (~rp(sk4,X0) | sk1(sk4) = sk7 | sk1(sk4) = X0 | sk7 = X0 | ~spl4 | ~spl9), inference(resolution, [status(thm)], [p138, p31])).
% 24.53/8.81 fof(sdef61, definition, (spl61 <=> (sk1(sk4) = sk7)), introduced(definition, [new_symbols(naming, [spl61])], [avatar_definition])).
% 24.53/8.81 cnf(ssp88, plain, (~spl4 | ~spl9 | spl52 | spl61), inference(avatar_split_clause, [status(thm)], [p302, sdef52, sdef61])).
% 24.53/8.81 cnf(p304, plain, (~rp(sk4,X0) | sk1(sk4) = sk0(sk4) | sk1(sk4) = X0 | sk0(sk4) = X0 | ~spl4), inference(resolution, [status(thm)], [p138, p91])).
% 24.53/8.81 fof(sdef62, definition, (spl62 <=> (sk1(sk4) = sk0(sk4))), introduced(definition, [new_symbols(naming, [spl62])], [avatar_definition])).
% 24.53/8.81 cnf(ssp89, plain, (~spl4 | spl57 | spl62), inference(avatar_split_clause, [status(thm)], [p304, sdef57, sdef62])).
% 24.53/8.81 cnf(p282, plain, (rp(sk4,sk5) | ~spl9 | ~spl48), inference(superposition, [status(thm)], [p256, p31])).
% 24.53/8.81 cnf(p314, plain, (~rp(sk4,X0) | sk6 = sk5 | sk6 = X0 | sk5 = X0 | ~spl4 | ~spl8 | ~spl9 | ~spl48), inference(resolution, [status(thm)], [p282, p135])).
% 24.53/8.81 cnf(ssp90, plain, (~spl4 | ~spl8 | ~spl9 | ~spl48 | spl21 | spl40), inference(avatar_split_clause, [status(thm)], [p314, sdef21, sdef40])).
% 24.53/8.81 cnf(p315, plain, (~rp(sk4,X0) | sk0(sk4) = sk5 | sk0(sk4) = X0 | sk5 = X0 | ~spl4 | ~spl9 | ~spl48), inference(resolution, [status(thm)], [p282, p137])).
% 24.53/8.81 cnf(ssp91, plain, (~spl4 | ~spl9 | ~spl48 | spl25 | spl54), inference(avatar_split_clause, [status(thm)], [p315, sdef25, sdef54])).
% 24.53/8.81 cnf(p316, plain, (~rp(sk4,X0) | sk1(sk4) = sk5 | sk1(sk4) = X0 | sk5 = X0 | ~spl4 | ~spl9 | ~spl48), inference(resolution, [status(thm)], [p282, p138])).
% 24.53/8.81 cnf(ssp92, plain, (~spl4 | ~spl9 | ~spl48 | spl27 | spl59), inference(avatar_split_clause, [status(thm)], [p316, sdef27, sdef59])).
% 24.53/8.81 cnf(p139, plain, (~rp(sk4,X0) | ~rp(sk4,X1) | sk5 = X1 | X0 = X1 | X1 != X0 | ~spl4 | ~spl7), inference(equality_factoring, [status(thm)], [p134])).
% 24.53/8.81 cnf(p318, plain, (~rp(sk4,sk5) | ~rp(sk4,X0) | sk5 = X0 | X0 != sk5 | ~spl4 | ~spl7), inference(factoring, [status(thm)], [p139])).
% 24.53/8.81 fof(sdef63, definition, (spl63 <=> (~rp(sk4,sk5))), introduced(definition, [new_symbols(naming, [spl63])], [avatar_definition])).
% 24.53/8.81 fof(sdef64, definition, (spl64 <=> (~rp(sk4,X0) | sk5 = X0 | X0 != sk5)), introduced(definition, [new_symbols(naming, [spl64])], [avatar_definition])).
% 24.53/8.81 cnf(ssp93, plain, (~spl4 | ~spl7 | spl63 | spl64), inference(avatar_split_clause, [status(thm)], [p318, sdef63, sdef64])).
% 24.53/8.81 cnf(p292, plain, (rp(sk4,sk6) | ~spl9 | ~spl49), inference(superposition, [status(thm)], [p258, p31])).
% 24.53/8.81 cnf(p327, plain, (~rp(sk4,X0) | sk5 = sk6 | sk5 = X0 | sk6 = X0 | ~spl4 | ~spl7 | ~spl9 | ~spl49), inference(resolution, [status(thm)], [p292, p134])).
% 24.53/8.81 cnf(ssp94, plain, (~spl4 | ~spl7 | ~spl9 | ~spl49 | spl21 | spl22), inference(avatar_split_clause, [status(thm)], [p327, sdef21, sdef22])).
% 24.53/8.81 cnf(p329, plain, (~rp(sk4,X0) | sk0(sk4) = sk6 | sk0(sk4) = X0 | sk6 = X0 | ~spl4 | ~spl9 | ~spl49), inference(resolution, [status(thm)], [p292, p137])).
% 24.53/8.81 cnf(ssp95, plain, (~spl4 | ~spl9 | ~spl49 | spl43 | spl55), inference(avatar_split_clause, [status(thm)], [p329, sdef43, sdef55])).
% 24.53/8.81 cnf(p330, plain, (~rp(sk4,X0) | sk1(sk4) = sk6 | sk1(sk4) = X0 | sk6 = X0 | ~spl4 | ~spl9 | ~spl49), inference(resolution, [status(thm)], [p292, p138])).
% 24.53/8.81 cnf(ssp96, plain, (~spl4 | ~spl9 | ~spl49 | spl45 | spl60), inference(avatar_split_clause, [status(thm)], [p330, sdef45, sdef60])).
% 24.53/8.81 cnf(p141, plain, (~rp(sk4,X0) | sk5 = X0 | sk6 = X0 | ~spl21), inference(avatar_component_clause, [status(thm)], [sdef21])).
% 24.53/8.81 cnf(p333, plain, (sk5 = sk7 | sk6 = sk7 | ~spl9 | ~spl21), inference(resolution, [status(thm)], [p141, p31])).
% 24.53/8.81 cnf(ssp97, plain, (~spl9 | ~spl21 | spl24 | spl42), inference(avatar_split_clause, [status(thm)], [p333, sdef24, sdef42])).
% 24.53/8.81 cnf(p144, plain, (~rp(sk4,X0) | sk5 = X0 | sk7 = X0 | ~spl23), inference(avatar_component_clause, [status(thm)], [sdef23])).
% 24.53/8.81 cnf(p336, plain, (sk5 = sk6 | sk7 = sk6 | ~spl8 | ~spl23), inference(resolution, [status(thm)], [p144, p28])).
% 24.53/8.81 cnf(ssp98, plain, (~spl8 | ~spl23 | spl22 | spl49), inference(avatar_split_clause, [status(thm)], [p336, sdef22, sdef49])).
% 24.53/8.81 cnf(p337, plain, (sk5 = sk0(sk4) | sk7 = sk0(sk4) | ~spl4 | ~spl23), inference(resolution, [status(thm)], [p144, p91])).
% 24.53/8.81 cnf(ssp99, plain, (~spl4 | ~spl23 | spl26 | spl51), inference(avatar_split_clause, [status(thm)], [p337, sdef26, sdef51])).
% 24.53/8.81 cnf(p338, plain, (sk5 = sk1(sk4) | sk7 = sk1(sk4) | ~spl4 | ~spl23), inference(resolution, [status(thm)], [p144, p94])).
% 24.53/8.81 cnf(ssp100, plain, (~spl4 | ~spl23 | spl28 | spl53), inference(avatar_split_clause, [status(thm)], [p338, sdef28, sdef53])).
% 24.53/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, ssp48, ssp49, ssp50, ssp51, ssp52, ssp53, ssp54, ssp55, ssp56, ssp57, ssp58, ssp59, ssp60, ssp61, ssp62, ssp63, ssp64, ssp65, ssp66, ssp67, ssp68, ssp69, ssp70, ssp71, ssp72, ssp73, ssp74, ssp75, ssp76, ssp77, ssp78, ssp79, ssp80, ssp81, ssp82, ssp83, ssp84, ssp85, ssp86, ssp87, ssp88, ssp89, ssp90, ssp91, ssp92, ssp93, ssp94, ssp95, ssp96, ssp97, ssp98, ssp99, ssp100, sct0, sct1, sct2, sct3, sct4, sct5, sct6, sct7, sct8, sct9, sct10, sct11, sct12, sct13, sct14, sct15, sct16, sct17, sct18, sct19, sct20, sct21, sct22])).
% 24.53/8.81 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------