%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU375+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n004.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 : Thu Sep 24 02:22:28 PM UTC 2026
% Result : Theorem 0.16s 0.49s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU375+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.05 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/0.44 % Computer : n004.cluster.edu
% 0.16/0.44 % Model : x86_64 x86_64
% 0.16/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.44 % Memory : 8046.5625MB
% 0.16/0.44 % OS : Linux 6.8.0-71-generic
% 0.16/0.44 % CPULimit : 300
% 0.16/0.44 % WCLimit : 300
% 0.16/0.44 % DateTime : Mon Sep 21 06:16:50 UTC 2026
% 0.16/0.45 % CPUTime :
% 0.16/0.47 % Drodi V4.1.1
% 0.16/0.49 % Refutation found
% 0.16/0.49 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.16/0.49 % SZS output start CNFRefutation for theBenchmark
% 0.16/0.49 fof(f7,axiom,(
% 0.16/0.49 (! [A] :( one_sorted_str(A)=> (! [B] :( net_str(B,A)=> (! [C] :( subnetstr(C,A,B)=> ( full_subnetstr(C,A,B)<=> ( full_subrelstr(C,B)& subrelstr(C,B) ) ) ) )) )) )),
% 0.16/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.49 fof(f9,axiom,(
% 0.16/0.49 (! [A] :( rel_str(A)=> one_sorted_str(A) ) )),
% 0.16/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.49 fof(f11,axiom,(
% 0.16/0.49 (! [A] :( one_sorted_str(A)=> (! [B] :( net_str(B,A)=> rel_str(B) ) )) )),
% 0.16/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.49 fof(f13,axiom,(
% 0.16/0.49 (! [A] :( rel_str(A)=> (! [B] :( subrelstr(B,A)=> rel_str(B) ) )) )),
% 0.16/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.49 fof(f23,axiom,(
% 0.16/0.49 (! [A] :( ( ~ empty_carrier(A)& one_sorted_str(A) )=> ~ empty(the_carrier(A)) ) )),
% 0.16/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.49 fof(f34,axiom,(
% 0.16/0.49 (! [A,B] :( in(A,B)=> element(A,B) ) )),
% 0.16/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.49 fof(f35,conjecture,(
% 0.16/0.49 (! [A] :( one_sorted_str(A)=> (! [B] :( ( ~ empty_carrier(B)& net_str(B,A) )=> (! [C] :( ( ~ empty_carrier(C)& full_subnetstr(C,A,B)& subnetstr(C,A,B) )=> (! [D] :( element(D,the_carrier(B))=> (! [E] :( element(E,the_carrier(B))=> (! [F] :( element(F,the_carrier(C))=> (! [G] :( element(G,the_carrier(C))=> ( ( D = F& E = G& related(B,D,E) )=> related(C,F,G) ) ) )) )) )) )) )) )) )),
% 0.16/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.49 fof(f36,negated_conjecture,(
% 0.16/0.49 ~((! [A] :( one_sorted_str(A)=> (! [B] :( ( ~ empty_carrier(B)& net_str(B,A) )=> (! [C] :( ( ~ empty_carrier(C)& full_subnetstr(C,A,B)& subnetstr(C,A,B) )=> (! [D] :( element(D,the_carrier(B))=> (! [E] :( element(E,the_carrier(B))=> (! [F] :( element(F,the_carrier(C))=> (! [G] :( element(G,the_carrier(C))=> ( ( D = F& E = G& related(B,D,E) )=> related(C,F,G) ) ) )) )) )) )) )) )) ))),
% 0.16/0.49 inference(negated_conjecture,[status(cth)],[f35])).
% 0.16/0.49 fof(f37,axiom,(
% 0.16/0.49 (! [A,B] :( element(A,B)=> ( empty(B)| in(A,B) ) ) )),
% 0.16/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.49 fof(f38,axiom,(
% 0.16/0.49 (! [A] :( rel_str(A)=> (! [B] :( ( full_subrelstr(B,A)& subrelstr(B,A) )=> (! [C] :( element(C,the_carrier(A))=> (! [D] :( element(D,the_carrier(A))=> (! [E] :( element(E,the_carrier(B))=> (! [F] :( element(F,the_carrier(B))=> ( ( E = C& F = D& related(A,C,D)& in(E,the_carrier(B))& in(F,the_carrier(B)) )=> related(B,E,F) ) ) )) )) )) )) )) )),
% 0.16/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.49 fof(f56,plain,(
% 0.16/0.49 ![A]: (~one_sorted_str(A)|(![B]: (~net_str(B,A)|(![C]: (~subnetstr(C,A,B)|(full_subnetstr(C,A,B)<=>(full_subrelstr(C,B)&subrelstr(C,B))))))))),
% 0.16/0.49 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 0.16/0.49 fof(f57,plain,(
% 0.16/0.49 ![A]: (~one_sorted_str(A)|(![B]: (~net_str(B,A)|(![C]: (~subnetstr(C,A,B)|((~full_subnetstr(C,A,B)|(full_subrelstr(C,B)&subrelstr(C,B)))&(full_subnetstr(C,A,B)|(~full_subrelstr(C,B)|~subrelstr(C,B)))))))))),
% 0.16/0.49 inference(NNF_transformation,[status(thm)],[f56])).
% 0.16/0.49 fof(f58,plain,(
% 0.16/0.49 ![X0,X1,X2]: (~one_sorted_str(X0)|~net_str(X1,X0)|~subnetstr(X2,X0,X1)|~full_subnetstr(X2,X0,X1)|full_subrelstr(X2,X1))),
% 0.16/0.49 inference(cnf_transformation,[status(thm)],[f57])).
% 0.16/0.49 fof(f59,plain,(
% 0.16/0.49 ![X0,X1,X2]: (~one_sorted_str(X0)|~net_str(X1,X0)|~subnetstr(X2,X0,X1)|~full_subnetstr(X2,X0,X1)|subrelstr(X2,X1))),
% 0.16/0.49 inference(cnf_transformation,[status(thm)],[f57])).
% 0.16/0.49 fof(f61,plain,(
% 0.16/0.49 ![A]: (~rel_str(A)|one_sorted_str(A))),
% 0.16/0.49 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 0.16/0.49 fof(f62,plain,(
% 0.16/0.49 ![X0]: (~rel_str(X0)|one_sorted_str(X0))),
% 0.16/0.49 inference(cnf_transformation,[status(thm)],[f61])).
% 0.16/0.49 fof(f63,plain,(
% 0.16/0.49 ![A]: (~one_sorted_str(A)|(![B]: (~net_str(B,A)|rel_str(B))))),
% 0.16/0.49 inference(pre_NNF_transformation,[status(thm)],[f11])).
% 0.16/0.49 fof(f64,plain,(
% 0.16/0.49 ![X0,X1]: (~one_sorted_str(X0)|~net_str(X1,X0)|rel_str(X1))),
% 0.16/0.49 inference(cnf_transformation,[status(thm)],[f63])).
% 0.16/0.49 fof(f65,plain,(
% 0.16/0.49 ![A]: (~rel_str(A)|(![B]: (~subrelstr(B,A)|rel_str(B))))),
% 0.16/0.49 inference(pre_NNF_transformation,[status(thm)],[f13])).
% 0.16/0.49 fof(f66,plain,(
% 0.16/0.49 ![X0,X1]: (~rel_str(X0)|~subrelstr(X1,X0)|rel_str(X1))),
% 0.16/0.49 inference(cnf_transformation,[status(thm)],[f65])).
% 0.16/0.49 fof(f87,plain,(
% 0.16/0.49 ![A]: ((empty_carrier(A)|~one_sorted_str(A))|~empty(the_carrier(A)))),
% 0.16/0.49 inference(pre_NNF_transformation,[status(thm)],[f23])).
% 0.16/0.49 fof(f88,plain,(
% 0.16/0.49 ![X0]: (empty_carrier(X0)|~one_sorted_str(X0)|~empty(the_carrier(X0)))),
% 0.16/0.49 inference(cnf_transformation,[status(thm)],[f87])).
% 0.16/0.49 fof(f122,plain,(
% 0.16/0.49 ![A,B]: (~in(A,B)|element(A,B))),
% 0.16/0.49 inference(pre_NNF_transformation,[status(thm)],[f34])).
% 0.16/0.49 fof(f123,plain,(
% 0.16/0.49 ![X0,X1]: (~in(X0,X1)|element(X0,X1))),
% 0.16/0.49 inference(cnf_transformation,[status(thm)],[f122])).
% 0.16/0.49 fof(f124,plain,(
% 0.16/0.49 (?[A]: (one_sorted_str(A)&(?[B]: ((~empty_carrier(B)&net_str(B,A))&(?[C]: (((~empty_carrier(C)&full_subnetstr(C,A,B))&subnetstr(C,A,B))&(?[D]: (element(D,the_carrier(B))&(?[E]: (element(E,the_carrier(B))&(?[F]: (element(F,the_carrier(C))&(?[G]: (element(G,the_carrier(C))&(((D=F&E=G)&related(B,D,E))&~related(C,F,G))))))))))))))))),
% 0.16/0.49 inference(pre_NNF_transformation,[status(thm)],[f36])).
% 0.16/0.49 fof(f125,plain,(
% 0.16/0.49 (one_sorted_str(sK15_skl)&((~empty_carrier(sK16_skl)&net_str(sK16_skl,sK15_skl))&(((~empty_carrier(sK17_skl)&full_subnetstr(sK17_skl,sK15_skl,sK16_skl))&subnetstr(sK17_skl,sK15_skl,sK16_skl))&(element(sK18_skl,the_carrier(sK16_skl))&(element(sK19_skl,the_carrier(sK16_skl))&(element(sK20_skl,the_carrier(sK17_skl))&(element(sK21_skl,the_carrier(sK17_skl))&(((sK18_skl=sK20_skl&sK19_skl=sK21_skl)&related(sK16_skl,sK18_skl,sK19_skl))&~related(sK17_skl,sK20_skl,sK21_skl)))))))))),
% 0.16/0.49 inference(skolemize,[status(esa),new_symbols(skolem,[sK15_skl,sK16_skl,sK17_skl,sK18_skl,sK19_skl,sK20_skl,sK21_skl]),skolemize(A,sK15_skl),skolemize(B,sK16_skl),skolemize(C,sK17_skl),skolemize(D,sK18_skl),skolemize(E,sK19_skl),skolemize(F,sK20_skl),skolemize(G,sK21_skl)],[f124])).
% 0.16/0.49 fof(f126,plain,(
% 0.16/0.49 one_sorted_str(sK15_skl)),
% 0.16/0.49 inference(cnf_transformation,[status(thm)],[f125])).
% 0.16/0.49 fof(f128,plain,(
% 0.16/0.49 net_str(sK16_skl,sK15_skl)),
% 0.16/0.49 inference(cnf_transformation,[status(thm)],[f125])).
% 0.16/0.49 fof(f129,plain,(
% 0.16/0.49 ~empty_carrier(sK17_skl)),
% 0.16/0.49 inference(cnf_transformation,[status(thm)],[f125])).
% 0.16/0.49 fof(f130,plain,(
% 0.16/0.49 full_subnetstr(sK17_skl,sK15_skl,sK16_skl)),
% 0.16/0.49 inference(cnf_transformation,[status(thm)],[f125])).
% 0.16/0.49 fof(f131,plain,(
% 0.16/0.49 subnetstr(sK17_skl,sK15_skl,sK16_skl)),
% 0.16/0.49 inference(cnf_transformation,[status(thm)],[f125])).
% 0.16/0.49 fof(f132,plain,(
% 0.16/0.49 element(sK18_skl,the_carrier(sK16_skl))),
% 0.16/0.49 inference(cnf_transformation,[status(thm)],[f125])).
% 0.16/0.49 fof(f133,plain,(
% 0.16/0.49 element(sK19_skl,the_carrier(sK16_skl))),
% 0.16/0.49 inference(cnf_transformation,[status(thm)],[f125])).
% 0.16/0.49 fof(f134,plain,(
% 0.16/0.49 element(sK20_skl,the_carrier(sK17_skl))),
% 0.16/0.49 inference(cnf_transformation,[status(thm)],[f125])).
% 0.16/0.49 fof(f135,plain,(
% 0.16/0.49 element(sK21_skl,the_carrier(sK17_skl))),
% 0.16/0.49 inference(cnf_transformation,[status(thm)],[f125])).
% 0.16/0.49 fof(f136,plain,(
% 0.16/0.49 sK18_skl=sK20_skl),
% 0.16/0.49 inference(cnf_transformation,[status(thm)],[f125])).
% 0.16/0.49 fof(f137,plain,(
% 0.16/0.49 sK19_skl=sK21_skl),
% 0.16/0.49 inference(cnf_transformation,[status(thm)],[f125])).
% 0.16/0.49 fof(f138,plain,(
% 0.16/0.49 related(sK16_skl,sK18_skl,sK19_skl)),
% 0.16/0.49 inference(cnf_transformation,[status(thm)],[f125])).
% 0.16/0.49 fof(f139,plain,(
% 0.16/0.49 ~related(sK17_skl,sK20_skl,sK21_skl)),
% 0.16/0.49 inference(cnf_transformation,[status(thm)],[f125])).
% 0.16/0.49 fof(f140,plain,(
% 0.16/0.49 ![A,B]: (~element(A,B)|(empty(B)|in(A,B)))),
% 0.16/0.49 inference(pre_NNF_transformation,[status(thm)],[f37])).
% 0.16/0.49 fof(f141,plain,(
% 0.16/0.49 ![X0,X1]: (~element(X0,X1)|empty(X1)|in(X0,X1))),
% 0.16/0.49 inference(cnf_transformation,[status(thm)],[f140])).
% 0.16/0.49 fof(f142,plain,(
% 0.16/0.49 ![A]: (~rel_str(A)|(![B]: ((~full_subrelstr(B,A)|~subrelstr(B,A))|(![C]: (~element(C,the_carrier(A))|(![D]: (~element(D,the_carrier(A))|(![E]: (~element(E,the_carrier(B))|(![F]: (~element(F,the_carrier(B))|(((((~E=C|~F=D)|~related(A,C,D))|~in(E,the_carrier(B)))|~in(F,the_carrier(B)))|related(B,E,F)))))))))))))),
% 0.16/0.49 inference(pre_NNF_transformation,[status(thm)],[f38])).
% 0.16/0.49 fof(f143,plain,(
% 0.16/0.49 ![X0,X1,X2,X3,X4,X5]: (~rel_str(X0)|~full_subrelstr(X1,X0)|~subrelstr(X1,X0)|~element(X2,the_carrier(X0))|~element(X3,the_carrier(X0))|~element(X4,the_carrier(X1))|~element(X5,the_carrier(X1))|~X4=X2|~X5=X3|~related(X0,X2,X3)|~in(X4,the_carrier(X1))|~in(X5,the_carrier(X1))|related(X1,X4,X5))),
% 0.16/0.49 inference(cnf_transformation,[status(thm)],[f142])).
% 0.16/0.49 fof(f152,plain,(
% 0.16/0.49 ![X0,X1,X2,X3]: (~rel_str(X0)|~full_subrelstr(X1,X0)|~subrelstr(X1,X0)|~element(X2,the_carrier(X0))|~element(X3,the_carrier(X0))|~element(X2,the_carrier(X1))|~element(X3,the_carrier(X1))|~related(X0,X2,X3)|~in(X2,the_carrier(X1))|~in(X3,the_carrier(X1))|related(X1,X2,X3))),
% 0.16/0.49 inference(destructive_equality_resolution,[status(thm)],[f143])).
% 0.16/0.49 fof(f153,plain,(
% 0.16/0.49 element(sK20_skl,the_carrier(sK16_skl))),
% 0.16/0.49 inference(forward_demodulation,[status(thm)],[f136,f132])).
% 0.16/0.49 fof(f154,plain,(
% 0.16/0.49 element(sK21_skl,the_carrier(sK16_skl))),
% 0.16/0.49 inference(forward_demodulation,[status(thm)],[f137,f133])).
% 0.16/0.49 fof(f155,plain,(
% 0.16/0.49 related(sK16_skl,sK20_skl,sK19_skl)),
% 0.16/0.49 inference(forward_demodulation,[status(thm)],[f136,f138])).
% 0.16/0.49 fof(f156,plain,(
% 0.16/0.49 related(sK16_skl,sK20_skl,sK21_skl)),
% 0.16/0.49 inference(forward_demodulation,[status(thm)],[f137,f155])).
% 0.16/0.49 fof(f157,plain,(
% 0.16/0.49 ~one_sorted_str(sK15_skl)|rel_str(sK16_skl)),
% 0.16/0.49 inference(resolution,[status(thm)],[f64,f128])).
% 0.16/0.49 fof(f158,definition,(
% 0.16/0.49 sQ0_spl <=> (one_sorted_str(sK15_skl))),
% 0.16/0.49 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.16/0.49 fof(f160,plain,(
% 0.16/0.49 ~one_sorted_str(sK15_skl)|sQ0_spl),
% 0.16/0.49 inference(component_clause,[status(thm)],[f158])).
% 0.16/0.49 fof(f161,definition,(
% 0.16/0.49 sQ1_spl <=> (rel_str(sK16_skl))),
% 0.16/0.49 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.16/0.49 fof(f164,plain,(
% 0.16/0.49 ~sQ0_spl|sQ1_spl),
% 0.16/0.49 inference(split_clause,[status(thm)],[f157,f158,f161])).
% 0.16/0.49 fof(f165,plain,(
% 0.16/0.49 $false|sQ0_spl),
% 0.16/0.49 inference(forward_subsumption_resolution,[status(thm)],[f160,f126])).
% 0.16/0.49 fof(f166,plain,(
% 0.16/0.49 sQ0_spl),
% 0.16/0.49 inference(contradiction_clause,[status(thm)],[f165])).
% 0.16/0.49 fof(f167,plain,(
% 0.16/0.49 ~one_sorted_str(sK15_skl)|~net_str(sK16_skl,sK15_skl)|~full_subnetstr(sK17_skl,sK15_skl,sK16_skl)|subrelstr(sK17_skl,sK16_skl)),
% 0.16/0.49 inference(resolution,[status(thm)],[f59,f131])).
% 0.16/0.49 fof(f168,definition,(
% 0.16/0.49 sQ2_spl <=> (net_str(sK16_skl,sK15_skl))),
% 0.16/0.49 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.16/0.49 fof(f170,plain,(
% 0.16/0.49 ~net_str(sK16_skl,sK15_skl)|sQ2_spl),
% 0.16/0.49 inference(component_clause,[status(thm)],[f168])).
% 0.16/0.49 fof(f171,definition,(
% 0.16/0.49 sQ3_spl <=> (full_subnetstr(sK17_skl,sK15_skl,sK16_skl))),
% 0.16/0.49 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.16/0.49 fof(f173,plain,(
% 0.16/0.49 ~full_subnetstr(sK17_skl,sK15_skl,sK16_skl)|sQ3_spl),
% 0.16/0.49 inference(component_clause,[status(thm)],[f171])).
% 0.16/0.49 fof(f174,definition,(
% 0.16/0.49 sQ4_spl <=> (subrelstr(sK17_skl,sK16_skl))),
% 0.16/0.49 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.16/0.49 fof(f175,plain,(
% 0.16/0.49 subrelstr(sK17_skl,sK16_skl)|~sQ4_spl),
% 0.16/0.49 inference(component_clause,[status(thm)],[f174])).
% 0.16/0.49 fof(f177,plain,(
% 0.16/0.49 ~sQ0_spl|~sQ2_spl|~sQ3_spl|sQ4_spl),
% 0.16/0.49 inference(split_clause,[status(thm)],[f167,f158,f168,f171,f174])).
% 0.16/0.49 fof(f183,plain,(
% 0.16/0.49 $false|sQ2_spl),
% 0.16/0.49 inference(forward_subsumption_resolution,[status(thm)],[f170,f128])).
% 0.16/0.49 fof(f184,plain,(
% 0.16/0.49 sQ2_spl),
% 0.16/0.49 inference(contradiction_clause,[status(thm)],[f183])).
% 0.16/0.49 fof(f185,plain,(
% 0.16/0.49 $false|sQ3_spl),
% 0.16/0.49 inference(forward_subsumption_resolution,[status(thm)],[f173,f130])).
% 0.16/0.49 fof(f186,plain,(
% 0.16/0.49 sQ3_spl),
% 0.16/0.49 inference(contradiction_clause,[status(thm)],[f185])).
% 0.16/0.49 fof(f192,definition,(
% 0.16/0.49 sQ6_spl <=> (rel_str(sK17_skl))),
% 0.16/0.49 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.16/0.49 fof(f193,plain,(
% 0.16/0.49 rel_str(sK17_skl)|~sQ6_spl),
% 0.16/0.49 inference(component_clause,[status(thm)],[f192])).
% 0.16/0.49 fof(f201,definition,(
% 0.16/0.49 sQ7_spl <=> (empty_carrier(sK17_skl))),
% 0.16/0.49 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.16/0.49 fof(f202,plain,(
% 0.16/0.49 empty_carrier(sK17_skl)|~sQ7_spl),
% 0.16/0.49 inference(component_clause,[status(thm)],[f201])).
% 0.16/0.49 fof(f253,plain,(
% 0.16/0.49 one_sorted_str(sK17_skl)|~sQ6_spl),
% 0.16/0.49 inference(resolution,[status(thm)],[f62,f193])).
% 0.16/0.49 fof(f256,plain,(
% 0.16/0.49 ~one_sorted_str(sK15_skl)|~net_str(sK16_skl,sK15_skl)|~full_subnetstr(sK17_skl,sK15_skl,sK16_skl)|full_subrelstr(sK17_skl,sK16_skl)),
% 0.16/0.49 inference(resolution,[status(thm)],[f58,f131])).
% 0.16/0.49 fof(f257,definition,(
% 0.16/0.49 sQ19_spl <=> (full_subrelstr(sK17_skl,sK16_skl))),
% 0.16/0.49 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.16/0.49 fof(f260,plain,(
% 0.16/0.49 ~sQ0_spl|~sQ2_spl|~sQ3_spl|sQ19_spl),
% 0.16/0.49 inference(split_clause,[status(thm)],[f256,f158,f168,f171,f257])).
% 0.16/0.49 fof(f263,plain,(
% 0.16/0.49 ~rel_str(sK16_skl)|rel_str(sK17_skl)|~sQ4_spl),
% 0.16/0.49 inference(resolution,[status(thm)],[f66,f175])).
% 0.16/0.49 fof(f264,plain,(
% 0.16/0.49 ~sQ1_spl|sQ6_spl|~sQ4_spl),
% 0.16/0.49 inference(split_clause,[status(thm)],[f263,f161,f192,f174])).
% 0.16/0.49 fof(f301,definition,(
% 0.16/0.49 sQ24_spl <=> (one_sorted_str(sK17_skl))),
% 0.16/0.49 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 0.16/0.49 fof(f303,plain,(
% 0.16/0.49 ~one_sorted_str(sK17_skl)|sQ24_spl),
% 0.16/0.49 inference(component_clause,[status(thm)],[f301])).
% 0.16/0.49 fof(f308,plain,(
% 0.16/0.49 $false|~sQ6_spl|sQ24_spl),
% 0.16/0.49 inference(forward_subsumption_resolution,[status(thm)],[f303,f253])).
% 0.16/0.49 fof(f309,plain,(
% 0.16/0.49 ~sQ6_spl|sQ24_spl),
% 0.16/0.49 inference(contradiction_clause,[status(thm)],[f308])).
% 0.16/0.49 fof(f441,plain,(
% 0.16/0.49 empty(the_carrier(sK17_skl))|in(sK21_skl,the_carrier(sK17_skl))),
% 0.16/0.49 inference(resolution,[status(thm)],[f141,f135])).
% 0.16/0.49 fof(f443,plain,(
% 0.16/0.49 empty(the_carrier(sK17_skl))|in(sK20_skl,the_carrier(sK17_skl))),
% 0.16/0.49 inference(resolution,[status(thm)],[f141,f134])).
% 0.16/0.49 fof(f445,definition,(
% 0.16/0.49 sQ49_spl <=> (empty(the_carrier(sK17_skl)))),
% 0.16/0.49 introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition])).
% 0.16/0.49 fof(f446,plain,(
% 0.16/0.49 empty(the_carrier(sK17_skl))|~sQ49_spl),
% 0.16/0.49 inference(component_clause,[status(thm)],[f445])).
% 0.16/0.49 fof(f448,definition,(
% 0.16/0.49 sQ50_spl <=> (in(sK21_skl,the_carrier(sK17_skl)))),
% 0.16/0.49 introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition])).
% 0.16/0.49 fof(f451,plain,(
% 0.16/0.49 sQ49_spl|sQ50_spl),
% 0.16/0.49 inference(split_clause,[status(thm)],[f441,f445,f448])).
% 0.16/0.49 fof(f459,definition,(
% 0.16/0.49 sQ53_spl <=> (in(sK20_skl,the_carrier(sK17_skl)))),
% 0.16/0.49 introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 0.16/0.49 fof(f460,plain,(
% 0.16/0.49 in(sK20_skl,the_carrier(sK17_skl))|~sQ53_spl),
% 0.16/0.49 inference(component_clause,[status(thm)],[f459])).
% 0.16/0.49 fof(f462,plain,(
% 0.16/0.49 sQ49_spl|sQ53_spl),
% 0.16/0.49 inference(split_clause,[status(thm)],[f443,f445,f459])).
% 0.16/0.49 fof(f483,plain,(
% 0.16/0.49 empty_carrier(sK17_skl)|~one_sorted_str(sK17_skl)|~sQ49_spl),
% 0.16/0.49 inference(resolution,[status(thm)],[f446,f88])).
% 0.16/0.49 fof(f489,plain,(
% 0.16/0.49 sQ7_spl|~sQ24_spl|~sQ49_spl),
% 0.16/0.49 inference(split_clause,[status(thm)],[f483,f201,f301,f445])).
% 0.16/0.49 fof(f497,plain,(
% 0.16/0.49 $false|~sQ7_spl),
% 0.16/0.49 inference(forward_subsumption_resolution,[status(thm)],[f202,f129])).
% 0.16/0.49 fof(f498,plain,(
% 0.16/0.49 ~sQ7_spl),
% 0.16/0.49 inference(contradiction_clause,[status(thm)],[f497])).
% 0.16/0.49 fof(f619,plain,(
% 0.16/0.49 ![X0,X1,X2,X3]: (~rel_str(X0)|~full_subrelstr(X1,X0)|~subrelstr(X1,X0)|~element(X2,the_carrier(X0))|~element(X3,the_carrier(X0))|~element(X3,the_carrier(X1))|~related(X0,X2,X3)|~in(X2,the_carrier(X1))|~in(X3,the_carrier(X1))|related(X1,X2,X3))),
% 0.16/0.49 inference(forward_subsumption_resolution,[status(thm)],[f152,f123])).
% 0.16/0.49 fof(f625,plain,(
% 0.16/0.49 ![X0,X1]: (~rel_str(sK16_skl)|~full_subrelstr(X0,sK16_skl)|~subrelstr(X0,sK16_skl)|~element(X1,the_carrier(sK16_skl))|~element(sK21_skl,the_carrier(X0))|~related(sK16_skl,X1,sK21_skl)|~in(X1,the_carrier(X0))|~in(sK21_skl,the_carrier(X0))|related(X0,X1,sK21_skl))),
% 0.16/0.49 inference(resolution,[status(thm)],[f619,f154])).
% 0.16/0.49 fof(f675,definition,(
% 0.16/0.49 ![X0,X1]: (sQ86_spl <=> (~full_subrelstr(X0,sK16_skl)|~subrelstr(X0,sK16_skl)|~element(X1,the_carrier(sK16_skl))|~element(sK21_skl,the_carrier(X0))|~related(sK16_skl,X1,sK21_skl)|~in(X1,the_carrier(X0))|~in(sK21_skl,the_carrier(X0))|related(X0,X1,sK21_skl)))),
% 0.16/0.49 introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition])).
% 0.16/0.49 fof(f676,plain,(
% 0.16/0.49 ![X0,X1]: (~full_subrelstr(X0,sK16_skl)|~subrelstr(X0,sK16_skl)|~element(X1,the_carrier(sK16_skl))|~element(sK21_skl,the_carrier(X0))|~related(sK16_skl,X1,sK21_skl)|~in(X1,the_carrier(X0))|~in(sK21_skl,the_carrier(X0))|related(X0,X1,sK21_skl)|~sQ86_spl)),
% 0.16/0.49 inference(component_clause,[status(thm)],[f675])).
% 0.16/0.50 fof(f678,plain,(
% 0.16/0.50 ~sQ1_spl|sQ86_spl),
% 0.16/0.50 inference(split_clause,[status(thm)],[f625,f161,f675])).
% 0.16/0.50 fof(f728,definition,(
% 0.16/0.50 sQ99_spl <=> (element(sK20_skl,the_carrier(sK16_skl)))),
% 0.16/0.50 introduced(definition,[new_symbols(definition,[sQ99_spl])],[split_symbol_definition])).
% 0.16/0.50 fof(f730,plain,(
% 0.16/0.50 ~element(sK20_skl,the_carrier(sK16_skl))|sQ99_spl),
% 0.16/0.50 inference(component_clause,[status(thm)],[f728])).
% 0.16/0.50 fof(f763,plain,(
% 0.16/0.50 ![X0,X1]: (~full_subrelstr(X0,sK16_skl)|~subrelstr(X0,sK16_skl)|~element(X1,the_carrier(sK16_skl))|~related(sK16_skl,X1,sK21_skl)|~in(X1,the_carrier(X0))|~in(sK21_skl,the_carrier(X0))|related(X0,X1,sK21_skl)|~sQ86_spl)),
% 0.16/0.50 inference(forward_subsumption_resolution,[status(thm)],[f676,f123])).
% 0.16/0.50 fof(f773,plain,(
% 0.16/0.50 $false|sQ99_spl),
% 0.16/0.50 inference(forward_subsumption_resolution,[status(thm)],[f730,f153])).
% 0.16/0.50 fof(f774,plain,(
% 0.16/0.50 sQ99_spl),
% 0.16/0.50 inference(contradiction_clause,[status(thm)],[f773])).
% 0.16/0.50 fof(f805,definition,(
% 0.16/0.50 sQ113_spl <=> (related(sK16_skl,sK20_skl,sK21_skl))),
% 0.16/0.50 introduced(definition,[new_symbols(definition,[sQ113_spl])],[split_symbol_definition])).
% 0.16/0.50 fof(f807,plain,(
% 0.16/0.50 ~related(sK16_skl,sK20_skl,sK21_skl)|sQ113_spl),
% 0.16/0.50 inference(component_clause,[status(thm)],[f805])).
% 0.16/0.50 fof(f862,plain,(
% 0.16/0.50 ~full_subrelstr(sK17_skl,sK16_skl)|~subrelstr(sK17_skl,sK16_skl)|~element(sK20_skl,the_carrier(sK16_skl))|~related(sK16_skl,sK20_skl,sK21_skl)|~in(sK21_skl,the_carrier(sK17_skl))|related(sK17_skl,sK20_skl,sK21_skl)|~sQ86_spl|~sQ53_spl),
% 0.16/0.50 inference(resolution,[status(thm)],[f763,f460])).
% 0.16/0.50 fof(f871,definition,(
% 0.16/0.50 sQ124_spl <=> (related(sK17_skl,sK20_skl,sK21_skl))),
% 0.16/0.50 introduced(definition,[new_symbols(definition,[sQ124_spl])],[split_symbol_definition])).
% 0.16/0.50 fof(f872,plain,(
% 0.16/0.50 related(sK17_skl,sK20_skl,sK21_skl)|~sQ124_spl),
% 0.16/0.50 inference(component_clause,[status(thm)],[f871])).
% 0.16/0.50 fof(f874,plain,(
% 0.16/0.50 ~sQ19_spl|~sQ4_spl|~sQ99_spl|~sQ113_spl|~sQ50_spl|sQ124_spl|~sQ86_spl|~sQ53_spl),
% 0.16/0.50 inference(split_clause,[status(thm)],[f862,f257,f174,f728,f805,f448,f871,f675,f459])).
% 0.16/0.50 fof(f885,plain,(
% 0.16/0.50 $false|~sQ124_spl),
% 0.16/0.50 inference(forward_subsumption_resolution,[status(thm)],[f872,f139])).
% 0.16/0.50 fof(f886,plain,(
% 0.16/0.50 ~sQ124_spl),
% 0.16/0.50 inference(contradiction_clause,[status(thm)],[f885])).
% 0.16/0.50 fof(f887,plain,(
% 0.16/0.50 $false|sQ113_spl),
% 0.16/0.50 inference(forward_subsumption_resolution,[status(thm)],[f807,f156])).
% 0.16/0.50 fof(f888,plain,(
% 0.16/0.50 sQ113_spl),
% 0.16/0.50 inference(contradiction_clause,[status(thm)],[f887])).
% 0.16/0.50 fof(f889,plain,(
% 0.16/0.50 $false),
% 0.16/0.50 inference(sat_refutation,[status(thm)],[f164,f166,f177,f184,f186,f260,f264,f309,f451,f462,f489,f498,f678,f774,f874,f886,f888])).
% 0.16/0.50 % SZS output end CNFRefutation for theBenchmark.p
% 0.16/0.53 % Elapsed time: 0.076733 seconds
% 0.16/0.53 % CPU time: 0.142611 seconds
% 0.16/0.53 % Total memory used: 20.251 MB
% 0.16/0.53 % Net memory used: 20.224 MB
%------------------------------------------------------------------------------