%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU375+2 : 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 : n013.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 14.16s 2.66s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SEU375+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.14/0.41 % Computer : n013.cluster.edu
% 0.14/0.41 % Model : x86_64 x86_64
% 0.14/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.41 % Memory : 8046.5625MB
% 0.14/0.41 % OS : Linux 6.8.0-71-generic
% 0.14/0.41 % CPULimit : 300
% 0.14/0.41 % WCLimit : 300
% 0.14/0.41 % DateTime : Mon Sep 21 06:16:35 UTC 2026
% 0.14/0.42 % CPUTime :
% 0.25/0.63 % Drodi V4.1.1
% 14.16/2.66 % Refutation found
% 14.16/2.66 % SZS status Theorem for theBenchmark: Theorem is valid
% 14.16/2.66 % SZS output start CNFRefutation for theBenchmark
% 14.16/2.66 fof(f105,axiom,(
% 14.16/2.66 (! [A] :( one_sorted_str(A)=> ( empty_carrier(A)<=> empty(the_carrier(A)) ) ) )),
% 14.16/2.66 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.16/2.66 fof(f124,axiom,(
% 14.16/2.66 (! [A,B] :( ( ~ empty(A)=> ( element(B,A)<=> in(B,A) ) )& ( empty(A)=> ( element(B,A)<=> empty(B) ) ) ) )),
% 14.16/2.66 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.16/2.66 fof(f181,axiom,(
% 14.16/2.66 (! [A] :( one_sorted_str(A)=> (! [B] :( net_str(B,A)=> (! [C] :( net_str(C,A)=> ( subnetstr(C,A,B)<=> ( subrelstr(C,B)& the_mapping(A,C) = relation_dom_restr_as_relation_of(the_carrier(B),the_carrier(A),the_mapping(A,B),the_carrier(C)) ) ) ) )) )) )),
% 14.16/2.66 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.16/2.66 fof(f187,axiom,(
% 14.16/2.66 (! [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) ) ) ) )) )) )),
% 14.16/2.66 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.16/2.66 fof(f269,axiom,(
% 14.16/2.66 (! [A] :( rel_str(A)=> one_sorted_str(A) ) )),
% 14.16/2.66 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.16/2.66 fof(f272,axiom,(
% 14.16/2.66 (! [A] :( one_sorted_str(A)=> (! [B] :( net_str(B,A)=> rel_str(B) ) )) )),
% 14.16/2.66 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.16/2.66 fof(f279,axiom,(
% 14.16/2.66 (! [A,B] :( ( one_sorted_str(A)& net_str(B,A) )=> (! [C] :( subnetstr(C,A,B)=> net_str(C,A) ) )) )),
% 14.16/2.66 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.16/2.66 fof(f601,axiom,(
% 14.16/2.66 (! [A,B] :( in(A,B)=> element(A,B) ) )),
% 14.16/2.66 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.16/2.66 fof(f614,conjecture,(
% 14.16/2.66 (! [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) ) ) )) )) )) )) )) )) )),
% 14.16/2.66 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.16/2.66 fof(f615,negated_conjecture,(
% 14.16/2.66 ~((! [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) ) ) )) )) )) )) )) )) ))),
% 14.16/2.66 inference(negated_conjecture,[status(cth)],[f614])).
% 14.16/2.66 fof(f729,lemma,(
% 14.16/2.66 (! [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) ) ) )) )) )) )) )) )),
% 14.16/2.66 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.16/2.66 fof(f747,axiom,(
% 14.16/2.66 (! [A,B] :~ ( in(A,B)& empty(B) ) )),
% 14.16/2.66 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.16/2.66 fof(f1279,plain,(
% 14.16/2.66 ![A]: (~one_sorted_str(A)|(empty_carrier(A)<=>empty(the_carrier(A))))),
% 14.16/2.66 inference(pre_NNF_transformation,[status(thm)],[f105])).
% 14.16/2.66 fof(f1280,plain,(
% 14.16/2.66 ![A]: (~one_sorted_str(A)|((~empty_carrier(A)|empty(the_carrier(A)))&(empty_carrier(A)|~empty(the_carrier(A)))))),
% 14.16/2.66 inference(NNF_transformation,[status(thm)],[f1279])).
% 14.16/2.66 fof(f1282,plain,(
% 14.16/2.66 ![X0]: (~one_sorted_str(X0)|empty_carrier(X0)|~empty(the_carrier(X0)))),
% 14.16/2.66 inference(cnf_transformation,[status(thm)],[f1280])).
% 14.16/2.66 fof(f1394,plain,(
% 14.16/2.66 ![A,B]: ((empty(A)|(element(B,A)<=>in(B,A)))&(~empty(A)|(element(B,A)<=>empty(B))))),
% 14.16/2.66 inference(pre_NNF_transformation,[status(thm)],[f124])).
% 14.16/2.66 fof(f1395,plain,(
% 14.16/2.66 ![A,B]: ((empty(A)|((~element(B,A)|in(B,A))&(element(B,A)|~in(B,A))))&(~empty(A)|((~element(B,A)|empty(B))&(element(B,A)|~empty(B)))))),
% 14.16/2.66 inference(NNF_transformation,[status(thm)],[f1394])).
% 14.16/2.66 fof(f1396,plain,(
% 14.16/2.66 (![A]: (empty(A)|((![B]: (~element(B,A)|in(B,A)))&(![B]: (element(B,A)|~in(B,A))))))&(![A]: (~empty(A)|((![B]: (~element(B,A)|empty(B)))&(![B]: (element(B,A)|~empty(B))))))),
% 14.16/2.66 inference(miniscoping,[status(thm)],[f1395])).
% 14.16/2.66 fof(f1397,plain,(
% 14.16/2.66 ![X0,X1]: (empty(X0)|~element(X1,X0)|in(X1,X0))),
% 14.16/2.66 inference(cnf_transformation,[status(thm)],[f1396])).
% 14.16/2.66 fof(f1792,plain,(
% 14.16/2.66 ![A]: (~one_sorted_str(A)|(![B]: (~net_str(B,A)|(![C]: (~net_str(C,A)|(subnetstr(C,A,B)<=>(subrelstr(C,B)&the_mapping(A,C)=relation_dom_restr_as_relation_of(the_carrier(B),the_carrier(A),the_mapping(A,B),the_carrier(C)))))))))),
% 14.16/2.66 inference(pre_NNF_transformation,[status(thm)],[f181])).
% 14.16/2.66 fof(f1793,plain,(
% 14.16/2.66 ![A]: (~one_sorted_str(A)|(![B]: (~net_str(B,A)|(![C]: (~net_str(C,A)|((~subnetstr(C,A,B)|(subrelstr(C,B)&the_mapping(A,C)=relation_dom_restr_as_relation_of(the_carrier(B),the_carrier(A),the_mapping(A,B),the_carrier(C))))&(subnetstr(C,A,B)|(~subrelstr(C,B)|~the_mapping(A,C)=relation_dom_restr_as_relation_of(the_carrier(B),the_carrier(A),the_mapping(A,B),the_carrier(C))))))))))),
% 14.16/2.66 inference(NNF_transformation,[status(thm)],[f1792])).
% 14.16/2.66 fof(f1794,plain,(
% 14.16/2.66 ![X0,X1,X2]: (~one_sorted_str(X0)|~net_str(X1,X0)|~net_str(X2,X0)|~subnetstr(X2,X0,X1)|subrelstr(X2,X1))),
% 14.16/2.66 inference(cnf_transformation,[status(thm)],[f1793])).
% 14.16/2.66 fof(f1824,plain,(
% 14.16/2.66 ![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))))))))),
% 14.16/2.66 inference(pre_NNF_transformation,[status(thm)],[f187])).
% 14.16/2.66 fof(f1825,plain,(
% 14.16/2.66 ![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)))))))))),
% 14.16/2.66 inference(NNF_transformation,[status(thm)],[f1824])).
% 14.16/2.66 fof(f1826,plain,(
% 14.16/2.66 ![X0,X1,X2]: (~one_sorted_str(X0)|~net_str(X1,X0)|~subnetstr(X2,X0,X1)|~full_subnetstr(X2,X0,X1)|full_subrelstr(X2,X1))),
% 14.16/2.66 inference(cnf_transformation,[status(thm)],[f1825])).
% 14.16/2.66 fof(f1970,plain,(
% 14.16/2.66 ![A]: (~rel_str(A)|one_sorted_str(A))),
% 14.16/2.66 inference(pre_NNF_transformation,[status(thm)],[f269])).
% 14.16/2.66 fof(f1971,plain,(
% 14.16/2.66 ![X0]: (~rel_str(X0)|one_sorted_str(X0))),
% 14.16/2.66 inference(cnf_transformation,[status(thm)],[f1970])).
% 14.16/2.66 fof(f1974,plain,(
% 14.16/2.66 ![A]: (~one_sorted_str(A)|(![B]: (~net_str(B,A)|rel_str(B))))),
% 14.16/2.66 inference(pre_NNF_transformation,[status(thm)],[f272])).
% 14.16/2.66 fof(f1975,plain,(
% 14.16/2.66 ![X0,X1]: (~one_sorted_str(X0)|~net_str(X1,X0)|rel_str(X1))),
% 14.16/2.66 inference(cnf_transformation,[status(thm)],[f1974])).
% 14.16/2.66 fof(f1985,plain,(
% 14.16/2.66 ![A,B]: ((~one_sorted_str(A)|~net_str(B,A))|(![C]: (~subnetstr(C,A,B)|net_str(C,A))))),
% 14.16/2.66 inference(pre_NNF_transformation,[status(thm)],[f279])).
% 14.16/2.66 fof(f1986,plain,(
% 14.16/2.66 ![X0,X1,X2]: (~one_sorted_str(X0)|~net_str(X1,X0)|~subnetstr(X2,X0,X1)|net_str(X2,X0))),
% 14.16/2.66 inference(cnf_transformation,[status(thm)],[f1985])).
% 14.16/2.66 fof(f3619,plain,(
% 14.16/2.66 ![A,B]: (~in(A,B)|element(A,B))),
% 14.16/2.66 inference(pre_NNF_transformation,[status(thm)],[f601])).
% 14.16/2.66 fof(f3620,plain,(
% 14.16/2.66 ![X0,X1]: (~in(X0,X1)|element(X0,X1))),
% 14.16/2.66 inference(cnf_transformation,[status(thm)],[f3619])).
% 14.16/2.66 fof(f3665,plain,(
% 14.16/2.66 (?[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))))))))))))))))),
% 14.16/2.66 inference(pre_NNF_transformation,[status(thm)],[f615])).
% 14.16/2.66 fof(f3666,plain,(
% 14.16/2.66 (one_sorted_str(sK409_skl)&((~empty_carrier(sK410_skl)&net_str(sK410_skl,sK409_skl))&(((~empty_carrier(sK411_skl)&full_subnetstr(sK411_skl,sK409_skl,sK410_skl))&subnetstr(sK411_skl,sK409_skl,sK410_skl))&(element(sK412_skl,the_carrier(sK410_skl))&(element(sK413_skl,the_carrier(sK410_skl))&(element(sK414_skl,the_carrier(sK411_skl))&(element(sK415_skl,the_carrier(sK411_skl))&(((sK412_skl=sK414_skl&sK413_skl=sK415_skl)&related(sK410_skl,sK412_skl,sK413_skl))&~related(sK411_skl,sK414_skl,sK415_skl)))))))))),
% 14.16/2.66 inference(skolemize,[status(esa),new_symbols(skolem,[sK409_skl,sK410_skl,sK411_skl,sK412_skl,sK413_skl,sK414_skl,sK415_skl]),skolemize(A,sK409_skl),skolemize(B,sK410_skl),skolemize(C,sK411_skl),skolemize(D,sK412_skl),skolemize(E,sK413_skl),skolemize(F,sK414_skl),skolemize(G,sK415_skl)],[f3665])).
% 14.16/2.66 fof(f3667,plain,(
% 14.16/2.66 one_sorted_str(sK409_skl)),
% 14.16/2.66 inference(cnf_transformation,[status(thm)],[f3666])).
% 14.16/2.66 fof(f3669,plain,(
% 14.16/2.66 net_str(sK410_skl,sK409_skl)),
% 14.16/2.66 inference(cnf_transformation,[status(thm)],[f3666])).
% 14.16/2.66 fof(f3670,plain,(
% 14.16/2.66 ~empty_carrier(sK411_skl)),
% 14.16/2.66 inference(cnf_transformation,[status(thm)],[f3666])).
% 14.16/2.66 fof(f3671,plain,(
% 14.16/2.66 full_subnetstr(sK411_skl,sK409_skl,sK410_skl)),
% 14.16/2.66 inference(cnf_transformation,[status(thm)],[f3666])).
% 14.16/2.66 fof(f3672,plain,(
% 14.16/2.66 subnetstr(sK411_skl,sK409_skl,sK410_skl)),
% 14.16/2.66 inference(cnf_transformation,[status(thm)],[f3666])).
% 14.16/2.66 fof(f3673,plain,(
% 14.16/2.66 element(sK412_skl,the_carrier(sK410_skl))),
% 14.16/2.66 inference(cnf_transformation,[status(thm)],[f3666])).
% 14.16/2.66 fof(f3674,plain,(
% 14.16/2.66 element(sK413_skl,the_carrier(sK410_skl))),
% 14.16/2.66 inference(cnf_transformation,[status(thm)],[f3666])).
% 14.16/2.66 fof(f3675,plain,(
% 14.16/2.66 element(sK414_skl,the_carrier(sK411_skl))),
% 14.16/2.66 inference(cnf_transformation,[status(thm)],[f3666])).
% 14.16/2.66 fof(f3676,plain,(
% 14.16/2.66 element(sK415_skl,the_carrier(sK411_skl))),
% 14.16/2.66 inference(cnf_transformation,[status(thm)],[f3666])).
% 14.16/2.66 fof(f3677,plain,(
% 14.16/2.66 sK412_skl=sK414_skl),
% 14.16/2.66 inference(cnf_transformation,[status(thm)],[f3666])).
% 14.16/2.66 fof(f3678,plain,(
% 14.16/2.66 sK413_skl=sK415_skl),
% 14.16/2.66 inference(cnf_transformation,[status(thm)],[f3666])).
% 14.16/2.66 fof(f3679,plain,(
% 14.16/2.66 related(sK410_skl,sK412_skl,sK413_skl)),
% 14.16/2.66 inference(cnf_transformation,[status(thm)],[f3666])).
% 14.16/2.66 fof(f3680,plain,(
% 14.16/2.66 ~related(sK411_skl,sK414_skl,sK415_skl)),
% 14.16/2.66 inference(cnf_transformation,[status(thm)],[f3666])).
% 14.16/2.66 fof(f4067,plain,(
% 14.16/2.66 ![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)))))))))))))),
% 14.16/2.66 inference(pre_NNF_transformation,[status(thm)],[f729])).
% 14.16/2.66 fof(f4068,plain,(
% 14.16/2.66 ![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))),
% 14.16/2.66 inference(cnf_transformation,[status(thm)],[f4067])).
% 14.16/2.66 fof(f4127,plain,(
% 14.16/2.66 ![A,B]: (~in(A,B)|~empty(B))),
% 14.16/2.66 inference(pre_NNF_transformation,[status(thm)],[f747])).
% 14.16/2.66 fof(f4128,plain,(
% 14.16/2.66 ![B]: ((![A]: ~in(A,B))|~empty(B))),
% 14.16/2.66 inference(miniscoping,[status(thm)],[f4127])).
% 14.16/2.66 fof(f4129,plain,(
% 14.16/2.66 ![X0,X1]: (~in(X0,X1)|~empty(X1))),
% 14.16/2.66 inference(cnf_transformation,[status(thm)],[f4128])).
% 14.16/2.66 fof(f4939,plain,(
% 14.16/2.66 ![X0,X1,X2]: (~one_sorted_str(X0)|~net_str(X1,X0)|~subnetstr(X2,X0,X1)|subrelstr(X2,X1))),
% 14.16/2.66 inference(backward_subsumption_resolution,[status(thm)],[f1794,f1986])).
% 14.16/2.66 fof(f5060,plain,(
% 14.16/2.66 element(sK412_skl,the_carrier(sK411_skl))),
% 14.16/2.66 inference(backward_demodulation,[status(thm)],[f3677,f3675])).
% 14.16/2.66 fof(f5061,plain,(
% 14.16/2.66 element(sK413_skl,the_carrier(sK411_skl))),
% 14.16/2.67 inference(backward_demodulation,[status(thm)],[f3678,f3676])).
% 14.16/2.67 fof(f5062,plain,(
% 14.16/2.67 ~related(sK411_skl,sK412_skl,sK415_skl)),
% 14.16/2.67 inference(forward_demodulation,[status(thm)],[f3677,f3680])).
% 14.16/2.67 fof(f5063,plain,(
% 14.16/2.67 ~related(sK411_skl,sK412_skl,sK413_skl)),
% 14.16/2.67 inference(forward_demodulation,[status(thm)],[f3678,f5062])).
% 14.16/2.67 fof(f5112,plain,(
% 14.16/2.67 ![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))),
% 14.16/2.67 inference(destructive_equality_resolution,[status(thm)],[f4068])).
% 14.16/2.67 fof(f5113,plain,(
% 14.16/2.67 ![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))),
% 14.16/2.67 inference(forward_subsumption_resolution,[status(thm)],[f5112,f3620])).
% 14.16/2.67 fof(f5269,plain,(
% 14.16/2.67 ~one_sorted_str(sK409_skl)|rel_str(sK410_skl)),
% 14.16/2.67 inference(resolution,[status(thm)],[f1975,f3669])).
% 14.16/2.67 fof(f5270,plain,(
% 14.16/2.67 rel_str(sK410_skl)),
% 14.16/2.67 inference(forward_subsumption_resolution,[status(thm)],[f5269,f3667])).
% 14.16/2.67 fof(f5272,plain,(
% 14.16/2.67 ~one_sorted_str(sK409_skl)|~net_str(sK410_skl,sK409_skl)|subrelstr(sK411_skl,sK410_skl)),
% 14.16/2.67 inference(resolution,[status(thm)],[f3672,f4939])).
% 14.16/2.67 fof(f5273,plain,(
% 14.16/2.67 ~one_sorted_str(sK409_skl)|~net_str(sK410_skl,sK409_skl)|net_str(sK411_skl,sK409_skl)),
% 14.16/2.67 inference(resolution,[status(thm)],[f3672,f1986])).
% 14.16/2.67 fof(f5274,plain,(
% 14.16/2.67 ~net_str(sK410_skl,sK409_skl)|subrelstr(sK411_skl,sK410_skl)),
% 14.16/2.67 inference(forward_subsumption_resolution,[status(thm)],[f5272,f3667])).
% 14.16/2.67 fof(f5275,plain,(
% 14.16/2.67 ~net_str(sK410_skl,sK409_skl)|net_str(sK411_skl,sK409_skl)),
% 14.16/2.67 inference(forward_subsumption_resolution,[status(thm)],[f5273,f3667])).
% 14.16/2.67 fof(f5276,plain,(
% 14.16/2.67 ~net_str(sK410_skl,sK409_skl)|~one_sorted_str(sK409_skl)|rel_str(sK411_skl)),
% 14.16/2.67 inference(resolution,[status(thm)],[f5275,f1975])).
% 14.16/2.67 fof(f5277,plain,(
% 14.16/2.67 ~one_sorted_str(sK409_skl)|rel_str(sK411_skl)),
% 14.16/2.67 inference(forward_subsumption_resolution,[status(thm)],[f5276,f3669])).
% 14.16/2.67 fof(f5278,plain,(
% 14.16/2.67 rel_str(sK411_skl)),
% 14.16/2.67 inference(resolution,[status(thm)],[f5277,f3667])).
% 14.16/2.67 fof(f5280,plain,(
% 14.16/2.67 ~one_sorted_str(sK409_skl)|~net_str(sK410_skl,sK409_skl)|~subnetstr(sK411_skl,sK409_skl,sK410_skl)|full_subrelstr(sK411_skl,sK410_skl)),
% 14.16/2.67 inference(resolution,[status(thm)],[f1826,f3671])).
% 14.16/2.67 fof(f5281,plain,(
% 14.16/2.67 ~net_str(sK410_skl,sK409_skl)|~subnetstr(sK411_skl,sK409_skl,sK410_skl)|full_subrelstr(sK411_skl,sK410_skl)),
% 14.16/2.67 inference(forward_subsumption_resolution,[status(thm)],[f5280,f3667])).
% 14.16/2.67 fof(f5282,plain,(
% 14.16/2.67 ~subnetstr(sK411_skl,sK409_skl,sK410_skl)|full_subrelstr(sK411_skl,sK410_skl)),
% 14.16/2.67 inference(resolution,[status(thm)],[f5281,f3669])).
% 14.16/2.67 fof(f5283,plain,(
% 14.16/2.67 full_subrelstr(sK411_skl,sK410_skl)),
% 14.16/2.67 inference(forward_subsumption_resolution,[status(thm)],[f5282,f3672])).
% 14.16/2.67 fof(f5395,plain,(
% 14.16/2.67 empty(the_carrier(sK411_skl))|in(sK413_skl,the_carrier(sK411_skl))),
% 14.16/2.67 inference(resolution,[status(thm)],[f1397,f5061])).
% 14.16/2.67 fof(f5397,plain,(
% 14.16/2.67 empty(the_carrier(sK411_skl))|in(sK412_skl,the_carrier(sK411_skl))),
% 14.16/2.67 inference(resolution,[status(thm)],[f1397,f5060])).
% 14.16/2.67 fof(f5406,plain,(
% 14.16/2.67 ![X0,X1]: (empty(the_carrier(sK411_skl))|~rel_str(X0)|~full_subrelstr(sK411_skl,X0)|~subrelstr(sK411_skl,X0)|~element(X1,the_carrier(X0))|~element(sK413_skl,the_carrier(X0))|~element(sK413_skl,the_carrier(sK411_skl))|~related(X0,X1,sK413_skl)|~in(X1,the_carrier(sK411_skl))|related(sK411_skl,X1,sK413_skl))),
% 14.16/2.67 inference(resolution,[status(thm)],[f5395,f5113])).
% 14.16/2.67 fof(f5410,plain,(
% 14.16/2.67 ![X0,X1]: (~rel_str(X0)|~full_subrelstr(sK411_skl,X0)|~subrelstr(sK411_skl,X0)|~element(X1,the_carrier(X0))|~element(sK413_skl,the_carrier(X0))|~element(sK413_skl,the_carrier(sK411_skl))|~related(X0,X1,sK413_skl)|~in(X1,the_carrier(sK411_skl))|related(sK411_skl,X1,sK413_skl))),
% 14.16/2.67 inference(forward_subsumption_resolution,[status(thm)],[f5406,f4129])).
% 14.16/2.67 fof(f5426,plain,(
% 14.16/2.67 ![X0]: (~rel_str(sK410_skl)|~subrelstr(sK411_skl,sK410_skl)|~element(X0,the_carrier(sK410_skl))|~element(sK413_skl,the_carrier(sK410_skl))|~element(sK413_skl,the_carrier(sK411_skl))|~related(sK410_skl,X0,sK413_skl)|~in(X0,the_carrier(sK411_skl))|related(sK411_skl,X0,sK413_skl))),
% 14.16/2.67 inference(resolution,[status(thm)],[f5410,f5283])).
% 14.16/2.67 fof(f5427,plain,(
% 14.16/2.67 ![X0]: (~subrelstr(sK411_skl,sK410_skl)|~element(X0,the_carrier(sK410_skl))|~element(sK413_skl,the_carrier(sK410_skl))|~element(sK413_skl,the_carrier(sK411_skl))|~related(sK410_skl,X0,sK413_skl)|~in(X0,the_carrier(sK411_skl))|related(sK411_skl,X0,sK413_skl))),
% 14.16/2.67 inference(forward_subsumption_resolution,[status(thm)],[f5426,f5270])).
% 14.16/2.67 fof(f5428,plain,(
% 14.16/2.67 ![X0]: (~element(X0,the_carrier(sK410_skl))|~element(sK413_skl,the_carrier(sK410_skl))|~element(sK413_skl,the_carrier(sK411_skl))|~related(sK410_skl,X0,sK413_skl)|~in(X0,the_carrier(sK411_skl))|related(sK411_skl,X0,sK413_skl)|~net_str(sK410_skl,sK409_skl))),
% 14.16/2.67 inference(resolution,[status(thm)],[f5427,f5274])).
% 14.16/2.67 fof(f5429,plain,(
% 14.16/2.67 ![X0]: (~element(X0,the_carrier(sK410_skl))|~element(sK413_skl,the_carrier(sK411_skl))|~related(sK410_skl,X0,sK413_skl)|~in(X0,the_carrier(sK411_skl))|related(sK411_skl,X0,sK413_skl)|~net_str(sK410_skl,sK409_skl))),
% 14.16/2.69 inference(forward_subsumption_resolution,[status(thm)],[f5428,f3674])).
% 14.16/2.69 fof(f5430,plain,(
% 14.16/2.69 ![X0]: (~element(X0,the_carrier(sK410_skl))|~element(sK413_skl,the_carrier(sK411_skl))|~related(sK410_skl,X0,sK413_skl)|~in(X0,the_carrier(sK411_skl))|related(sK411_skl,X0,sK413_skl))),
% 14.16/2.69 inference(resolution,[status(thm)],[f5429,f3669])).
% 14.16/2.69 fof(f5431,plain,(
% 14.16/2.69 ![X0]: (~element(X0,the_carrier(sK410_skl))|~related(sK410_skl,X0,sK413_skl)|~in(X0,the_carrier(sK411_skl))|related(sK411_skl,X0,sK413_skl))),
% 14.16/2.69 inference(forward_subsumption_resolution,[status(thm)],[f5430,f5061])).
% 14.16/2.69 fof(f5432,plain,(
% 14.16/2.69 ~element(sK412_skl,the_carrier(sK410_skl))|~in(sK412_skl,the_carrier(sK411_skl))|related(sK411_skl,sK412_skl,sK413_skl)),
% 14.16/2.69 inference(resolution,[status(thm)],[f5431,f3679])).
% 14.16/2.69 fof(f5433,plain,(
% 14.16/2.69 ~in(sK412_skl,the_carrier(sK411_skl))|related(sK411_skl,sK412_skl,sK413_skl)),
% 14.16/2.69 inference(forward_subsumption_resolution,[status(thm)],[f5432,f3673])).
% 14.16/2.69 fof(f5475,plain,(
% 14.16/2.69 related(sK411_skl,sK412_skl,sK413_skl)|empty(the_carrier(sK411_skl))),
% 14.16/2.69 inference(resolution,[status(thm)],[f5433,f5397])).
% 14.16/2.69 fof(f5476,plain,(
% 14.16/2.69 empty(the_carrier(sK411_skl))),
% 14.16/2.69 inference(forward_subsumption_resolution,[status(thm)],[f5475,f5063])).
% 14.16/2.69 fof(f5477,plain,(
% 14.16/2.69 ~one_sorted_str(sK411_skl)|empty_carrier(sK411_skl)),
% 14.16/2.69 inference(resolution,[status(thm)],[f5476,f1282])).
% 14.16/2.69 fof(f5483,plain,(
% 14.16/2.69 ~one_sorted_str(sK411_skl)),
% 14.16/2.69 inference(forward_subsumption_resolution,[status(thm)],[f5477,f3670])).
% 14.16/2.69 fof(f5484,plain,(
% 14.16/2.69 ~rel_str(sK411_skl)),
% 14.16/2.69 inference(resolution,[status(thm)],[f5483,f1971])).
% 14.16/2.69 fof(f5485,plain,(
% 14.16/2.69 $false),
% 14.16/2.69 inference(forward_subsumption_resolution,[status(thm)],[f5484,f5278])).
% 14.16/2.69 % SZS output end CNFRefutation for theBenchmark.p
% 14.16/2.77 % Elapsed time: 2.327947 seconds
% 14.16/2.77 % CPU time: 16.332504 seconds
% 14.16/2.77 % Total memory used: 313.426 MB
% 14.16/2.77 % Net memory used: 306.843 MB
%------------------------------------------------------------------------------