%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU374+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n018.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:27 PM UTC 2026
% Result : Theorem 0.17s 0.47s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SEU374+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.42 % Computer : n018.cluster.edu
% 0.17/0.42 % Model : x86_64 x86_64
% 0.17/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.42 % Memory : 8046.5625MB
% 0.17/0.42 % OS : Linux 6.8.0-71-generic
% 0.17/0.42 % CPULimit : 300
% 0.17/0.42 % WCLimit : 300
% 0.17/0.42 % DateTime : Mon Sep 21 06:19:13 UTC 2026
% 0.17/0.42 % CPUTime :
% 0.17/0.44 % Drodi V4.1.1
% 0.17/0.47 % Refutation found
% 0.17/0.47 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.17/0.47 % SZS output start CNFRefutation for theBenchmark
% 0.17/0.47 fof(f6,axiom,(
% 0.17/0.47 (! [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)) ) ) ) )) )) )),
% 0.17/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.47 fof(f14,axiom,(
% 0.17/0.47 (! [A] :( one_sorted_str(A)=> (! [B] :( net_str(B,A)=> rel_str(B) ) )) )),
% 0.17/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.47 fof(f18,axiom,(
% 0.17/0.47 (! [A,B] :( ( one_sorted_str(A)& net_str(B,A) )=> (! [C] :( subnetstr(C,A,B)=> net_str(C,A) ) )) )),
% 0.17/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.47 fof(f50,conjecture,(
% 0.17/0.47 (! [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) ) ) )) )) )) )) )) )) )),
% 0.17/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.47 fof(f51,negated_conjecture,(
% 0.17/0.47 ~((! [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) ) ) )) )) )) )) )) )) ))),
% 0.17/0.47 inference(negated_conjecture,[status(cth)],[f50])).
% 0.17/0.47 fof(f56,axiom,(
% 0.17/0.47 (! [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) ) ) )) )) )) )) )) )),
% 0.17/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.47 fof(f73,plain,(
% 0.17/0.47 ![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)))))))))),
% 0.17/0.47 inference(pre_NNF_transformation,[status(thm)],[f6])).
% 0.17/0.47 fof(f74,plain,(
% 0.17/0.47 ![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))))))))))),
% 0.17/0.47 inference(NNF_transformation,[status(thm)],[f73])).
% 0.17/0.47 fof(f75,plain,(
% 0.17/0.47 ![X0,X1,X2]: (~one_sorted_str(X0)|~net_str(X1,X0)|~net_str(X2,X0)|~subnetstr(X2,X0,X1)|subrelstr(X2,X1))),
% 0.17/0.47 inference(cnf_transformation,[status(thm)],[f74])).
% 0.17/0.47 fof(f86,plain,(
% 0.17/0.47 ![A]: (~one_sorted_str(A)|(![B]: (~net_str(B,A)|rel_str(B))))),
% 0.17/0.47 inference(pre_NNF_transformation,[status(thm)],[f14])).
% 0.17/0.47 fof(f87,plain,(
% 0.17/0.47 ![X0,X1]: (~one_sorted_str(X0)|~net_str(X1,X0)|rel_str(X1))),
% 0.17/0.47 inference(cnf_transformation,[status(thm)],[f86])).
% 0.17/0.47 fof(f90,plain,(
% 0.17/0.47 ![A,B]: ((~one_sorted_str(A)|~net_str(B,A))|(![C]: (~subnetstr(C,A,B)|net_str(C,A))))),
% 0.17/0.47 inference(pre_NNF_transformation,[status(thm)],[f18])).
% 0.17/0.47 fof(f91,plain,(
% 0.17/0.47 ![X0,X1,X2]: (~one_sorted_str(X0)|~net_str(X1,X0)|~subnetstr(X2,X0,X1)|net_str(X2,X0))),
% 0.17/0.47 inference(cnf_transformation,[status(thm)],[f90])).
% 0.17/0.47 fof(f179,plain,(
% 0.17/0.47 (?[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))))))))))))))))),
% 0.17/0.47 inference(pre_NNF_transformation,[status(thm)],[f51])).
% 0.17/0.47 fof(f180,plain,(
% 0.17/0.47 (one_sorted_str(sK18_skl)&(net_str(sK19_skl,sK18_skl)&(subnetstr(sK20_skl,sK18_skl,sK19_skl)&(element(sK21_skl,the_carrier(sK19_skl))&(element(sK22_skl,the_carrier(sK19_skl))&(element(sK23_skl,the_carrier(sK20_skl))&(element(sK24_skl,the_carrier(sK20_skl))&(((sK21_skl=sK23_skl&sK22_skl=sK24_skl)&related(sK20_skl,sK23_skl,sK24_skl))&~related(sK19_skl,sK21_skl,sK22_skl)))))))))),
% 0.17/0.47 inference(skolemize,[status(esa),new_symbols(skolem,[sK18_skl,sK19_skl,sK20_skl,sK21_skl,sK22_skl,sK23_skl,sK24_skl]),skolemize(A,sK18_skl),skolemize(B,sK19_skl),skolemize(C,sK20_skl),skolemize(D,sK21_skl),skolemize(E,sK22_skl),skolemize(F,sK23_skl),skolemize(G,sK24_skl)],[f179])).
% 0.17/0.47 fof(f181,plain,(
% 0.17/0.47 one_sorted_str(sK18_skl)),
% 0.17/0.47 inference(cnf_transformation,[status(thm)],[f180])).
% 0.17/0.47 fof(f182,plain,(
% 0.17/0.47 net_str(sK19_skl,sK18_skl)),
% 0.17/0.47 inference(cnf_transformation,[status(thm)],[f180])).
% 0.17/0.47 fof(f183,plain,(
% 0.17/0.47 subnetstr(sK20_skl,sK18_skl,sK19_skl)),
% 0.17/0.47 inference(cnf_transformation,[status(thm)],[f180])).
% 0.17/0.47 fof(f184,plain,(
% 0.17/0.47 element(sK21_skl,the_carrier(sK19_skl))),
% 0.17/0.47 inference(cnf_transformation,[status(thm)],[f180])).
% 0.17/0.47 fof(f185,plain,(
% 0.17/0.47 element(sK22_skl,the_carrier(sK19_skl))),
% 0.17/0.47 inference(cnf_transformation,[status(thm)],[f180])).
% 0.17/0.47 fof(f186,plain,(
% 0.17/0.47 element(sK23_skl,the_carrier(sK20_skl))),
% 0.17/0.47 inference(cnf_transformation,[status(thm)],[f180])).
% 0.17/0.47 fof(f187,plain,(
% 0.17/0.47 element(sK24_skl,the_carrier(sK20_skl))),
% 0.17/0.47 inference(cnf_transformation,[status(thm)],[f180])).
% 0.17/0.47 fof(f188,plain,(
% 0.17/0.47 sK21_skl=sK23_skl),
% 0.17/0.47 inference(cnf_transformation,[status(thm)],[f180])).
% 0.17/0.47 fof(f189,plain,(
% 0.17/0.47 sK22_skl=sK24_skl),
% 0.17/0.47 inference(cnf_transformation,[status(thm)],[f180])).
% 0.17/0.47 fof(f190,plain,(
% 0.17/0.47 related(sK20_skl,sK23_skl,sK24_skl)),
% 0.17/0.47 inference(cnf_transformation,[status(thm)],[f180])).
% 0.17/0.47 fof(f191,plain,(
% 0.17/0.47 ~related(sK19_skl,sK21_skl,sK22_skl)),
% 0.17/0.47 inference(cnf_transformation,[status(thm)],[f180])).
% 0.17/0.47 fof(f204,plain,(
% 0.17/0.47 ![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)))))))))))))),
% 0.17/0.47 inference(pre_NNF_transformation,[status(thm)],[f56])).
% 0.17/0.47 fof(f205,plain,(
% 0.17/0.47 ![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))),
% 0.17/0.47 inference(cnf_transformation,[status(thm)],[f204])).
% 0.17/0.47 fof(f214,plain,(
% 0.17/0.47 ![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))),
% 0.17/0.47 inference(destructive_equality_resolution,[status(thm)],[f205])).
% 0.17/0.47 fof(f216,plain,(
% 0.17/0.47 element(sK21_skl,the_carrier(sK20_skl))),
% 0.17/0.47 inference(forward_demodulation,[status(thm)],[f188,f186])).
% 0.17/0.47 fof(f219,plain,(
% 0.17/0.47 ![X0,X1,X2]: (~one_sorted_str(X0)|~net_str(X1,X0)|~subnetstr(X2,X0,X1)|subrelstr(X2,X1))),
% 0.17/0.47 inference(forward_subsumption_resolution,[status(thm)],[f75,f91])).
% 0.17/0.47 fof(f220,plain,(
% 0.17/0.47 ![X0]: (~one_sorted_str(sK18_skl)|~subnetstr(X0,sK18_skl,sK19_skl)|subrelstr(X0,sK19_skl))),
% 0.17/0.47 inference(resolution,[status(thm)],[f219,f182])).
% 0.17/0.47 fof(f221,plain,(
% 0.17/0.47 ![X0]: (~subnetstr(X0,sK18_skl,sK19_skl)|subrelstr(X0,sK19_skl))),
% 0.17/0.47 inference(forward_subsumption_resolution,[status(thm)],[f220,f181])).
% 0.17/0.47 fof(f222,plain,(
% 0.17/0.47 element(sK22_skl,the_carrier(sK20_skl))),
% 0.17/0.47 inference(forward_demodulation,[status(thm)],[f189,f187])).
% 0.17/0.47 fof(f223,plain,(
% 0.17/0.47 related(sK20_skl,sK21_skl,sK24_skl)),
% 0.17/0.47 inference(forward_demodulation,[status(thm)],[f188,f190])).
% 0.17/0.47 fof(f224,plain,(
% 0.17/0.47 related(sK20_skl,sK21_skl,sK22_skl)),
% 0.17/0.47 inference(forward_demodulation,[status(thm)],[f189,f223])).
% 0.17/0.47 fof(f225,plain,(
% 0.17/0.47 subrelstr(sK20_skl,sK19_skl)),
% 0.17/0.47 inference(resolution,[status(thm)],[f221,f183])).
% 0.17/0.47 fof(f232,plain,(
% 0.17/0.47 ~one_sorted_str(sK18_skl)|rel_str(sK19_skl)),
% 0.17/0.47 inference(resolution,[status(thm)],[f87,f182])).
% 0.17/0.47 fof(f233,plain,(
% 0.17/0.47 rel_str(sK19_skl)),
% 0.17/0.47 inference(forward_subsumption_resolution,[status(thm)],[f232,f181])).
% 0.17/0.47 fof(f235,plain,(
% 0.17/0.47 ![X0,X1,X2]: (~subrelstr(X0,sK19_skl)|~element(X1,the_carrier(sK19_skl))|~element(X2,the_carrier(sK19_skl))|~element(X1,the_carrier(X0))|~element(X2,the_carrier(X0))|~related(X0,X1,X2)|related(sK19_skl,X1,X2))),
% 0.17/0.47 inference(resolution,[status(thm)],[f233,f214])).
% 0.17/0.48 fof(f246,plain,(
% 0.17/0.48 ![X0,X1]: (~element(X0,the_carrier(sK19_skl))|~element(X1,the_carrier(sK19_skl))|~element(X0,the_carrier(sK20_skl))|~element(X1,the_carrier(sK20_skl))|~related(sK20_skl,X0,X1)|related(sK19_skl,X0,X1))),
% 0.17/0.48 inference(resolution,[status(thm)],[f235,f225])).
% 0.17/0.48 fof(f251,plain,(
% 0.17/0.48 ~element(sK21_skl,the_carrier(sK19_skl))|~element(sK22_skl,the_carrier(sK19_skl))|~element(sK21_skl,the_carrier(sK20_skl))|~element(sK22_skl,the_carrier(sK20_skl))|related(sK19_skl,sK21_skl,sK22_skl)),
% 0.17/0.48 inference(resolution,[status(thm)],[f246,f224])).
% 0.17/0.48 fof(f252,plain,(
% 0.17/0.48 ~element(sK22_skl,the_carrier(sK19_skl))|~element(sK21_skl,the_carrier(sK20_skl))|~element(sK22_skl,the_carrier(sK20_skl))|related(sK19_skl,sK21_skl,sK22_skl)),
% 0.17/0.48 inference(forward_subsumption_resolution,[status(thm)],[f251,f184])).
% 0.17/0.48 fof(f355,plain,(
% 0.17/0.48 ~element(sK21_skl,the_carrier(sK20_skl))|~element(sK22_skl,the_carrier(sK20_skl))|related(sK19_skl,sK21_skl,sK22_skl)),
% 0.17/0.48 inference(forward_subsumption_resolution,[status(thm)],[f252,f185])).
% 0.17/0.48 fof(f356,plain,(
% 0.17/0.48 ~element(sK21_skl,the_carrier(sK20_skl))|related(sK19_skl,sK21_skl,sK22_skl)),
% 0.17/0.48 inference(resolution,[status(thm)],[f355,f222])).
% 0.17/0.48 fof(f357,plain,(
% 0.17/0.48 related(sK19_skl,sK21_skl,sK22_skl)),
% 0.17/0.48 inference(forward_subsumption_resolution,[status(thm)],[f356,f216])).
% 0.17/0.48 fof(f365,plain,(
% 0.17/0.48 $false),
% 0.17/0.48 inference(forward_subsumption_resolution,[status(thm)],[f357,f191])).
% 0.17/0.48 % SZS output end CNFRefutation for theBenchmark.p
% 0.17/0.51 % Elapsed time: 0.065602 seconds
% 0.17/0.51 % CPU time: 0.181986 seconds
% 0.17/0.51 % Total memory used: 75.598 MB
% 0.17/0.51 % Net memory used: 75.554 MB
%------------------------------------------------------------------------------