%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU374+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 : n010.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 24.26s 3.61s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU374+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n010.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 06:17:24 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.14/0.46 % Drodi V4.1.1
% 24.26/3.61 % Refutation found
% 24.26/3.61 % SZS status Theorem for theBenchmark: Theorem is valid
% 24.26/3.61 % SZS output start CNFRefutation for theBenchmark
% 24.26/3.61 fof(f179,axiom,(
% 24.26/3.61 (! [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)) ) ) ) )) )) )),
% 24.26/3.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 24.26/3.61 fof(f269,axiom,(
% 24.26/3.61 (! [A] :( one_sorted_str(A)=> (! [B] :( net_str(B,A)=> rel_str(B) ) )) )),
% 24.26/3.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 24.26/3.61 fof(f276,axiom,(
% 24.26/3.61 (! [A,B] :( ( one_sorted_str(A)& net_str(B,A) )=> (! [C] :( subnetstr(C,A,B)=> net_str(C,A) ) )) )),
% 24.26/3.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 24.26/3.61 fof(f605,conjecture,(
% 24.26/3.61 (! [A] :( one_sorted_str(A)=> (! [B] :( net_str(B,A)=> (! [C] :( 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(C,F,G) )=> related(B,D,E) ) ) )) )) )) )) )) )) )),
% 24.76/3.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 24.76/3.61 fof(f606,negated_conjecture,(
% 24.76/3.61 ~((! [A] :( one_sorted_str(A)=> (! [B] :( net_str(B,A)=> (! [C] :( 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(C,F,G) )=> related(B,D,E) ) ) )) )) )) )) )) )) ))),
% 24.76/3.61 inference(negated_conjecture,[status(cth)],[f605])).
% 24.76/3.61 fof(f724,lemma,(
% 24.76/3.61 (! [A] :( rel_str(A)=> (! [B] :( 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(B,E,F) )=> related(A,C,D) ) ) )) )) )) )) )) )),
% 24.76/3.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 24.76/3.61 fof(f1784,plain,(
% 24.76/3.61 ![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)))))))))),
% 24.76/3.61 inference(pre_NNF_transformation,[status(thm)],[f179])).
% 24.76/3.61 fof(f1785,plain,(
% 24.76/3.61 ![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))))))))))),
% 24.76/3.61 inference(NNF_transformation,[status(thm)],[f1784])).
% 24.76/3.61 fof(f1786,plain,(
% 24.76/3.61 ![X0,X1,X2]: (~one_sorted_str(X0)|~net_str(X1,X0)|~net_str(X2,X0)|~subnetstr(X2,X0,X1)|subrelstr(X2,X1))),
% 24.76/3.61 inference(cnf_transformation,[status(thm)],[f1785])).
% 24.76/3.61 fof(f1961,plain,(
% 24.76/3.61 ![A]: (~one_sorted_str(A)|(![B]: (~net_str(B,A)|rel_str(B))))),
% 24.76/3.61 inference(pre_NNF_transformation,[status(thm)],[f269])).
% 24.76/3.61 fof(f1962,plain,(
% 24.76/3.61 ![X0,X1]: (~one_sorted_str(X0)|~net_str(X1,X0)|rel_str(X1))),
% 24.76/3.61 inference(cnf_transformation,[status(thm)],[f1961])).
% 24.76/3.61 fof(f1972,plain,(
% 24.76/3.61 ![A,B]: ((~one_sorted_str(A)|~net_str(B,A))|(![C]: (~subnetstr(C,A,B)|net_str(C,A))))),
% 24.76/3.61 inference(pre_NNF_transformation,[status(thm)],[f276])).
% 24.76/3.61 fof(f1973,plain,(
% 24.76/3.61 ![X0,X1,X2]: (~one_sorted_str(X0)|~net_str(X1,X0)|~subnetstr(X2,X0,X1)|net_str(X2,X0))),
% 24.76/3.61 inference(cnf_transformation,[status(thm)],[f1972])).
% 24.76/3.61 fof(f3634,plain,(
% 24.76/3.61 (?[A]: (one_sorted_str(A)&(?[B]: (net_str(B,A)&(?[C]: (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(C,F,G))&~related(B,D,E))))))))))))))))),
% 24.76/3.61 inference(pre_NNF_transformation,[status(thm)],[f606])).
% 24.76/3.61 fof(f3635,plain,(
% 24.76/3.61 (one_sorted_str(sK409_skl)&(net_str(sK410_skl,sK409_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(sK411_skl,sK414_skl,sK415_skl))&~related(sK410_skl,sK412_skl,sK413_skl)))))))))),
% 24.76/3.61 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)],[f3634])).
% 24.76/3.61 fof(f3636,plain,(
% 24.76/3.61 one_sorted_str(sK409_skl)),
% 24.76/3.61 inference(cnf_transformation,[status(thm)],[f3635])).
% 24.76/3.61 fof(f3637,plain,(
% 24.76/3.61 net_str(sK410_skl,sK409_skl)),
% 24.76/3.61 inference(cnf_transformation,[status(thm)],[f3635])).
% 24.76/3.61 fof(f3638,plain,(
% 24.76/3.61 subnetstr(sK411_skl,sK409_skl,sK410_skl)),
% 24.76/3.61 inference(cnf_transformation,[status(thm)],[f3635])).
% 24.76/3.61 fof(f3639,plain,(
% 24.76/3.61 element(sK412_skl,the_carrier(sK410_skl))),
% 24.76/3.61 inference(cnf_transformation,[status(thm)],[f3635])).
% 24.76/3.61 fof(f3640,plain,(
% 24.76/3.61 element(sK413_skl,the_carrier(sK410_skl))),
% 24.76/3.61 inference(cnf_transformation,[status(thm)],[f3635])).
% 24.76/3.61 fof(f3641,plain,(
% 24.76/3.61 element(sK414_skl,the_carrier(sK411_skl))),
% 24.76/3.61 inference(cnf_transformation,[status(thm)],[f3635])).
% 24.76/3.61 fof(f3642,plain,(
% 24.76/3.61 element(sK415_skl,the_carrier(sK411_skl))),
% 24.76/3.61 inference(cnf_transformation,[status(thm)],[f3635])).
% 24.76/3.61 fof(f3643,plain,(
% 24.76/3.61 sK412_skl=sK414_skl),
% 24.76/3.61 inference(cnf_transformation,[status(thm)],[f3635])).
% 24.76/3.61 fof(f3644,plain,(
% 24.76/3.61 sK413_skl=sK415_skl),
% 24.76/3.61 inference(cnf_transformation,[status(thm)],[f3635])).
% 24.76/3.61 fof(f3645,plain,(
% 24.76/3.61 related(sK411_skl,sK414_skl,sK415_skl)),
% 24.76/3.61 inference(cnf_transformation,[status(thm)],[f3635])).
% 24.76/3.61 fof(f3646,plain,(
% 24.76/3.61 ~related(sK410_skl,sK412_skl,sK413_skl)),
% 24.76/3.61 inference(cnf_transformation,[status(thm)],[f3635])).
% 24.76/3.61 fof(f4047,plain,(
% 24.76/3.61 ![A]: (~rel_str(A)|(![B]: (~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(B,E,F))|related(A,C,D)))))))))))))),
% 24.76/3.61 inference(pre_NNF_transformation,[status(thm)],[f724])).
% 24.76/3.61 fof(f4048,plain,(
% 24.76/3.61 ![X0,X1,X2,X3,X4,X5]: (~rel_str(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(X1,X4,X5)|related(X0,X2,X3))),
% 24.76/3.61 inference(cnf_transformation,[status(thm)],[f4047])).
% 24.76/3.61 fof(f4921,plain,(
% 24.76/3.61 ![X0,X1,X2]: (~one_sorted_str(X0)|~net_str(X1,X0)|~subnetstr(X2,X0,X1)|subrelstr(X2,X1))),
% 24.76/3.61 inference(backward_subsumption_resolution,[status(thm)],[f1786,f1973])).
% 24.76/3.61 fof(f5041,plain,(
% 24.76/3.61 element(sK412_skl,the_carrier(sK411_skl))),
% 24.76/3.61 inference(backward_demodulation,[status(thm)],[f3643,f3641])).
% 24.76/3.61 fof(f5042,plain,(
% 24.76/3.61 element(sK413_skl,the_carrier(sK411_skl))),
% 24.76/3.61 inference(backward_demodulation,[status(thm)],[f3644,f3642])).
% 24.76/3.61 fof(f5043,plain,(
% 24.76/3.61 related(sK411_skl,sK412_skl,sK415_skl)),
% 24.76/3.61 inference(forward_demodulation,[status(thm)],[f3643,f3645])).
% 24.76/3.61 fof(f5044,plain,(
% 24.76/3.61 related(sK411_skl,sK412_skl,sK413_skl)),
% 24.76/3.61 inference(forward_demodulation,[status(thm)],[f3644,f5043])).
% 24.76/3.61 fof(f5092,plain,(
% 24.76/3.61 ![X0,X1,X2,X3]: (~rel_str(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(X1,X2,X3)|related(X0,X2,X3))),
% 24.76/3.61 inference(destructive_equality_resolution,[status(thm)],[f4048])).
% 24.76/3.61 fof(f5250,plain,(
% 24.76/3.61 ~one_sorted_str(sK409_skl)|rel_str(sK410_skl)),
% 24.76/3.61 inference(resolution,[status(thm)],[f1962,f3637])).
% 24.76/3.61 fof(f5251,plain,(
% 24.76/3.61 rel_str(sK410_skl)),
% 24.76/3.61 inference(forward_subsumption_resolution,[status(thm)],[f5250,f3636])).
% 24.76/3.61 fof(f5262,plain,(
% 24.76/3.61 ~one_sorted_str(sK409_skl)|~net_str(sK410_skl,sK409_skl)|subrelstr(sK411_skl,sK410_skl)),
% 24.76/3.61 inference(resolution,[status(thm)],[f4921,f3638])).
% 24.76/3.61 fof(f5263,plain,(
% 24.76/3.61 ~net_str(sK410_skl,sK409_skl)|subrelstr(sK411_skl,sK410_skl)),
% 24.76/3.61 inference(forward_subsumption_resolution,[status(thm)],[f5262,f3636])).
% 24.76/3.61 fof(f6020,plain,(
% 24.76/3.61 ![X0,X1]: (~rel_str(sK410_skl)|~element(X0,the_carrier(sK410_skl))|~element(X1,the_carrier(sK410_skl))|~element(X0,the_carrier(sK411_skl))|~element(X1,the_carrier(sK411_skl))|~related(sK411_skl,X0,X1)|related(sK410_skl,X0,X1)|~net_str(sK410_skl,sK409_skl))),
% 24.76/3.66 inference(resolution,[status(thm)],[f5092,f5263])).
% 24.76/3.66 fof(f6021,plain,(
% 24.76/3.66 ![X0,X1]: (~element(X0,the_carrier(sK410_skl))|~element(X1,the_carrier(sK410_skl))|~element(X0,the_carrier(sK411_skl))|~element(X1,the_carrier(sK411_skl))|~related(sK411_skl,X0,X1)|related(sK410_skl,X0,X1)|~net_str(sK410_skl,sK409_skl))),
% 24.76/3.66 inference(forward_subsumption_resolution,[status(thm)],[f6020,f5251])).
% 24.76/3.66 fof(f6204,plain,(
% 24.76/3.66 ![X0,X1]: (~element(X0,the_carrier(sK410_skl))|~element(X1,the_carrier(sK410_skl))|~element(X0,the_carrier(sK411_skl))|~element(X1,the_carrier(sK411_skl))|~related(sK411_skl,X0,X1)|related(sK410_skl,X0,X1))),
% 24.76/3.66 inference(resolution,[status(thm)],[f6021,f3637])).
% 24.76/3.66 fof(f6440,plain,(
% 24.76/3.66 ~element(sK412_skl,the_carrier(sK410_skl))|~element(sK413_skl,the_carrier(sK410_skl))|~element(sK412_skl,the_carrier(sK411_skl))|~element(sK413_skl,the_carrier(sK411_skl))|related(sK410_skl,sK412_skl,sK413_skl)),
% 24.76/3.66 inference(resolution,[status(thm)],[f6204,f5044])).
% 24.76/3.66 fof(f6442,plain,(
% 24.76/3.66 ~element(sK413_skl,the_carrier(sK410_skl))|~element(sK412_skl,the_carrier(sK411_skl))|~element(sK413_skl,the_carrier(sK411_skl))|related(sK410_skl,sK412_skl,sK413_skl)),
% 24.76/3.66 inference(forward_subsumption_resolution,[status(thm)],[f6440,f3639])).
% 24.76/3.66 fof(f6446,plain,(
% 24.76/3.66 ~element(sK413_skl,the_carrier(sK410_skl))|~element(sK412_skl,the_carrier(sK411_skl))|related(sK410_skl,sK412_skl,sK413_skl)),
% 24.76/3.66 inference(resolution,[status(thm)],[f6442,f5042])).
% 24.76/3.66 fof(f6450,plain,(
% 24.76/3.66 ~element(sK412_skl,the_carrier(sK411_skl))|related(sK410_skl,sK412_skl,sK413_skl)),
% 24.76/3.66 inference(forward_subsumption_resolution,[status(thm)],[f6446,f3640])).
% 24.76/3.66 fof(f6453,plain,(
% 24.76/3.66 ~element(sK412_skl,the_carrier(sK411_skl))),
% 24.76/3.66 inference(resolution,[status(thm)],[f6450,f3646])).
% 24.76/3.66 fof(f6455,plain,(
% 24.76/3.66 $false),
% 24.76/3.66 inference(forward_subsumption_resolution,[status(thm)],[f6453,f5041])).
% 24.76/3.66 % SZS output end CNFRefutation for theBenchmark.p
% 24.76/3.67 % Elapsed time: 3.302529 seconds
% 24.76/3.67 % CPU time: 25.206996 seconds
% 24.76/3.67 % Total memory used: 453.037 MB
% 24.76/3.67 % Net memory used: 440.129 MB
%------------------------------------------------------------------------------