%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU376+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 : 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 0.18s 5.60s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SEU376+1 : 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/5.42 % Computer : n010.cluster.edu
% 0.14/5.42 % Model : x86_64 x86_64
% 0.14/5.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/5.42 % Memory : 8046.5625MB
% 0.14/5.42 % OS : Linux 6.8.0-71-generic
% 0.14/5.42 % CPULimit : 300
% 0.14/5.42 % WCLimit : 300
% 0.14/5.42 % DateTime : Mon Sep 21 06:17:15 UTC 2026
% 0.14/5.42 % CPUTime :
% 0.14/5.43 % Drodi V4.1.1
% 0.18/5.60 % Refutation found
% 0.18/5.60 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.18/5.60 % SZS output start CNFRefutation for theBenchmark
% 0.18/5.60 fof(f8,axiom,(
% 0.18/5.60 (! [A] :( ( ~ empty_carrier(A)& one_sorted_str(A) )=> (! [B] :( ( ~ empty_carrier(B)& net_str(B,A) )=> (! [C] :( is_eventually_in(A,B,C)<=> (? [D] :( element(D,the_carrier(B))& (! [E] :( element(E,the_carrier(B))=> ( related(B,D,E)=> in(apply_netmap(A,B,E),C) ) ) )) )) )) )) )),
% 0.18/5.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.18/5.60 fof(f9,axiom,(
% 0.18/5.60 (! [A] :( ( ~ empty_carrier(A)& one_sorted_str(A) )=> (! [B] :( ( ~ empty_carrier(B)& net_str(B,A) )=> (! [C] :( is_often_in(A,B,C)<=> (! [D] :( element(D,the_carrier(B))=> (? [E] :( element(E,the_carrier(B))& related(B,D,E)& in(apply_netmap(A,B,E),C) ) )) )) )) )) )),
% 0.18/5.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.18/5.60 fof(f10,axiom,(
% 0.18/5.60 (! [A] :( ( ~ empty_carrier(A)& rel_str(A) )=> ( directed_relstr(A)<=> (! [B] :( element(B,the_carrier(A))=> (! [C] :( element(C,the_carrier(A))=> (? [D] :( element(D,the_carrier(A))& related(A,B,D)& related(A,C,D) ) )) )) )) ) )),
% 0.18/5.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.18/5.60 fof(f20,axiom,(
% 0.18/5.60 (! [A] :( one_sorted_str(A)=> (! [B] :( net_str(B,A)=> rel_str(B) ) )) )),
% 0.18/5.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.18/5.60 fof(f54,conjecture,(
% 0.18/5.60 (! [A] :( ( ~ empty_carrier(A)& one_sorted_str(A) )=> (! [B] :( ( ~ empty_carrier(B)& transitive_relstr(B)& directed_relstr(B)& net_str(B,A) )=> (! [C] :( is_eventually_in(A,B,C)=> is_often_in(A,B,C) ) )) )) )),
% 0.18/5.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.18/5.60 fof(f55,negated_conjecture,(
% 0.18/5.60 ~((! [A] :( ( ~ empty_carrier(A)& one_sorted_str(A) )=> (! [B] :( ( ~ empty_carrier(B)& transitive_relstr(B)& directed_relstr(B)& net_str(B,A) )=> (! [C] :( is_eventually_in(A,B,C)=> is_often_in(A,B,C) ) )) )) ))),
% 0.18/5.60 inference(negated_conjecture,[status(cth)],[f54])).
% 0.18/5.60 fof(f80,plain,(
% 0.18/5.60 ![A]: ((empty_carrier(A)|~one_sorted_str(A))|(![B]: ((empty_carrier(B)|~net_str(B,A))|(![C]: (is_eventually_in(A,B,C)<=>(?[D]: (element(D,the_carrier(B))&(![E]: (~element(E,the_carrier(B))|(~related(B,D,E)|in(apply_netmap(A,B,E),C)))))))))))),
% 0.18/5.60 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 0.18/5.60 fof(f81,plain,(
% 0.18/5.60 ![A]: ((empty_carrier(A)|~one_sorted_str(A))|(![B]: ((empty_carrier(B)|~net_str(B,A))|(![C]: ((~is_eventually_in(A,B,C)|(?[D]: (element(D,the_carrier(B))&(![E]: (~element(E,the_carrier(B))|(~related(B,D,E)|in(apply_netmap(A,B,E),C)))))))&(is_eventually_in(A,B,C)|(![D]: (~element(D,the_carrier(B))|(?[E]: (element(E,the_carrier(B))&(related(B,D,E)&~in(apply_netmap(A,B,E),C))))))))))))),
% 0.18/5.60 inference(NNF_transformation,[status(thm)],[f80])).
% 0.18/5.60 fof(f82,plain,(
% 0.18/5.60 ![A]: ((empty_carrier(A)|~one_sorted_str(A))|(![B]: ((empty_carrier(B)|~net_str(B,A))|((![C]: (~is_eventually_in(A,B,C)|(?[D]: (element(D,the_carrier(B))&(![E]: (~element(E,the_carrier(B))|(~related(B,D,E)|in(apply_netmap(A,B,E),C))))))))&(![C]: (is_eventually_in(A,B,C)|(![D]: (~element(D,the_carrier(B))|(?[E]: (element(E,the_carrier(B))&(related(B,D,E)&~in(apply_netmap(A,B,E),C))))))))))))),
% 0.18/5.60 inference(miniscoping,[status(thm)],[f81])).
% 0.18/5.60 fof(f83,plain,(
% 0.18/5.60 ![A]: ((empty_carrier(A)|~one_sorted_str(A))|(![B]: ((empty_carrier(B)|~net_str(B,A))|((![C]: (~is_eventually_in(A,B,C)|(element(sK0_skl(C,B,A),the_carrier(B))&(![E]: (~element(E,the_carrier(B))|(~related(B,sK0_skl(C,B,A),E)|in(apply_netmap(A,B,E),C)))))))&(![C]: (is_eventually_in(A,B,C)|(![D]: (~element(D,the_carrier(B))|(element(sK1_skl(D,C,B,A),the_carrier(B))&(related(B,D,sK1_skl(D,C,B,A))&~in(apply_netmap(A,B,sK1_skl(D,C,B,A)),C)))))))))))),
% 0.18/5.60 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(D,sK0_skl(C,B,A)),skolemize(E,sK1_skl(D,C,B,A))],[f82])).
% 0.18/5.60 fof(f84,plain,(
% 0.18/5.60 ![X0,X1,X2]: (empty_carrier(X0)|~one_sorted_str(X0)|empty_carrier(X1)|~net_str(X1,X0)|~is_eventually_in(X0,X1,X2)|element(sK0_skl(X2,X1,X0),the_carrier(X1)))),
% 0.18/5.60 inference(cnf_transformation,[status(thm)],[f83])).
% 0.18/5.60 fof(f85,plain,(
% 0.18/5.60 ![X0,X1,X2,X3]: (empty_carrier(X0)|~one_sorted_str(X0)|empty_carrier(X1)|~net_str(X1,X0)|~is_eventually_in(X0,X1,X2)|~element(X3,the_carrier(X1))|~related(X1,sK0_skl(X2,X1,X0),X3)|in(apply_netmap(X0,X1,X3),X2))),
% 0.18/5.60 inference(cnf_transformation,[status(thm)],[f83])).
% 0.18/5.60 fof(f89,plain,(
% 0.18/5.60 ![A]: ((empty_carrier(A)|~one_sorted_str(A))|(![B]: ((empty_carrier(B)|~net_str(B,A))|(![C]: (is_often_in(A,B,C)<=>(![D]: (~element(D,the_carrier(B))|(?[E]: ((element(E,the_carrier(B))&related(B,D,E))&in(apply_netmap(A,B,E),C))))))))))),
% 0.18/5.60 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 0.18/5.60 fof(f90,plain,(
% 0.18/5.60 ![A]: ((empty_carrier(A)|~one_sorted_str(A))|(![B]: ((empty_carrier(B)|~net_str(B,A))|(![C]: ((~is_often_in(A,B,C)|(![D]: (~element(D,the_carrier(B))|(?[E]: ((element(E,the_carrier(B))&related(B,D,E))&in(apply_netmap(A,B,E),C))))))&(is_often_in(A,B,C)|(?[D]: (element(D,the_carrier(B))&(![E]: ((~element(E,the_carrier(B))|~related(B,D,E))|~in(apply_netmap(A,B,E),C)))))))))))),
% 0.18/5.60 inference(NNF_transformation,[status(thm)],[f89])).
% 0.18/5.60 fof(f91,plain,(
% 0.18/5.60 ![A]: ((empty_carrier(A)|~one_sorted_str(A))|(![B]: ((empty_carrier(B)|~net_str(B,A))|((![C]: (~is_often_in(A,B,C)|(![D]: (~element(D,the_carrier(B))|(?[E]: ((element(E,the_carrier(B))&related(B,D,E))&in(apply_netmap(A,B,E),C)))))))&(![C]: (is_often_in(A,B,C)|(?[D]: (element(D,the_carrier(B))&(![E]: ((~element(E,the_carrier(B))|~related(B,D,E))|~in(apply_netmap(A,B,E),C)))))))))))),
% 0.18/5.60 inference(miniscoping,[status(thm)],[f90])).
% 0.18/5.60 fof(f92,plain,(
% 0.18/5.60 ![A]: ((empty_carrier(A)|~one_sorted_str(A))|(![B]: ((empty_carrier(B)|~net_str(B,A))|((![C]: (~is_often_in(A,B,C)|(![D]: (~element(D,the_carrier(B))|((element(sK2_skl(D,C,B,A),the_carrier(B))&related(B,D,sK2_skl(D,C,B,A)))&in(apply_netmap(A,B,sK2_skl(D,C,B,A)),C))))))&(![C]: (is_often_in(A,B,C)|(element(sK3_skl(C,B,A),the_carrier(B))&(![E]: ((~element(E,the_carrier(B))|~related(B,sK3_skl(C,B,A),E))|~in(apply_netmap(A,B,E),C))))))))))),
% 0.18/5.60 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl,sK3_skl]),skolemize(E,sK2_skl(D,C,B,A)),skolemize(D,sK3_skl(C,B,A))],[f91])).
% 0.18/5.60 fof(f96,plain,(
% 0.18/5.60 ![X0,X1,X2]: (empty_carrier(X0)|~one_sorted_str(X0)|empty_carrier(X1)|~net_str(X1,X0)|is_often_in(X0,X1,X2)|element(sK3_skl(X2,X1,X0),the_carrier(X1)))),
% 0.18/5.60 inference(cnf_transformation,[status(thm)],[f92])).
% 0.18/5.60 fof(f97,plain,(
% 0.18/5.60 ![X0,X1,X2,X3]: (empty_carrier(X0)|~one_sorted_str(X0)|empty_carrier(X1)|~net_str(X1,X0)|is_often_in(X0,X1,X2)|~element(X3,the_carrier(X1))|~related(X1,sK3_skl(X2,X1,X0),X3)|~in(apply_netmap(X0,X1,X3),X2))),
% 0.18/5.60 inference(cnf_transformation,[status(thm)],[f92])).
% 0.18/5.60 fof(f98,plain,(
% 0.18/5.60 ![A]: ((empty_carrier(A)|~rel_str(A))|(directed_relstr(A)<=>(![B]: (~element(B,the_carrier(A))|(![C]: (~element(C,the_carrier(A))|(?[D]: ((element(D,the_carrier(A))&related(A,B,D))&related(A,C,D)))))))))),
% 0.18/5.60 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 0.18/5.60 fof(f99,plain,(
% 0.18/5.60 ![A]: ((empty_carrier(A)|~rel_str(A))|((~directed_relstr(A)|(![B]: (~element(B,the_carrier(A))|(![C]: (~element(C,the_carrier(A))|(?[D]: ((element(D,the_carrier(A))&related(A,B,D))&related(A,C,D))))))))&(directed_relstr(A)|(?[B]: (element(B,the_carrier(A))&(?[C]: (element(C,the_carrier(A))&(![D]: ((~element(D,the_carrier(A))|~related(A,B,D))|~related(A,C,D))))))))))),
% 0.18/5.60 inference(NNF_transformation,[status(thm)],[f98])).
% 0.18/5.60 fof(f100,plain,(
% 0.18/5.60 ![A]: ((empty_carrier(A)|~rel_str(A))|((~directed_relstr(A)|(![B]: (~element(B,the_carrier(A))|(![C]: (~element(C,the_carrier(A))|((element(sK4_skl(C,B,A),the_carrier(A))&related(A,B,sK4_skl(C,B,A)))&related(A,C,sK4_skl(C,B,A))))))))&(directed_relstr(A)|(element(sK5_skl(A),the_carrier(A))&(element(sK6_skl(A),the_carrier(A))&(![D]: ((~element(D,the_carrier(A))|~related(A,sK5_skl(A),D))|~related(A,sK6_skl(A),D))))))))),
% 0.18/5.60 inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl,sK5_skl,sK6_skl]),skolemize(D,sK4_skl(C,B,A)),skolemize(B,sK5_skl(A)),skolemize(C,sK6_skl(A))],[f99])).
% 0.18/5.60 fof(f101,plain,(
% 0.18/5.60 ![X0,X1,X2]: (empty_carrier(X0)|~rel_str(X0)|~directed_relstr(X0)|~element(X1,the_carrier(X0))|~element(X2,the_carrier(X0))|element(sK4_skl(X2,X1,X0),the_carrier(X0)))),
% 0.18/5.60 inference(cnf_transformation,[status(thm)],[f100])).
% 0.18/5.60 fof(f102,plain,(
% 0.18/5.60 ![X0,X1,X2]: (empty_carrier(X0)|~rel_str(X0)|~directed_relstr(X0)|~element(X1,the_carrier(X0))|~element(X2,the_carrier(X0))|related(X0,X1,sK4_skl(X2,X1,X0)))),
% 0.18/5.60 inference(cnf_transformation,[status(thm)],[f100])).
% 0.18/5.60 fof(f103,plain,(
% 0.18/5.60 ![X0,X1,X2]: (empty_carrier(X0)|~rel_str(X0)|~directed_relstr(X0)|~element(X1,the_carrier(X0))|~element(X2,the_carrier(X0))|related(X0,X2,sK4_skl(X2,X1,X0)))),
% 0.18/5.60 inference(cnf_transformation,[status(thm)],[f100])).
% 0.18/5.60 fof(f115,plain,(
% 0.18/5.60 ![A]: (~one_sorted_str(A)|(![B]: (~net_str(B,A)|rel_str(B))))),
% 0.18/5.60 inference(pre_NNF_transformation,[status(thm)],[f20])).
% 0.18/5.60 fof(f116,plain,(
% 0.18/5.60 ![X0,X1]: (~one_sorted_str(X0)|~net_str(X1,X0)|rel_str(X1))),
% 0.18/5.60 inference(cnf_transformation,[status(thm)],[f115])).
% 0.18/5.60 fof(f203,plain,(
% 0.18/5.60 (?[A]: ((~empty_carrier(A)&one_sorted_str(A))&(?[B]: ((((~empty_carrier(B)&transitive_relstr(B))&directed_relstr(B))&net_str(B,A))&(?[C]: (is_eventually_in(A,B,C)&~is_often_in(A,B,C)))))))),
% 0.18/5.60 inference(pre_NNF_transformation,[status(thm)],[f55])).
% 0.18/5.60 fof(f204,plain,(
% 0.18/5.60 ((~empty_carrier(sK25_skl)&one_sorted_str(sK25_skl))&((((~empty_carrier(sK26_skl)&transitive_relstr(sK26_skl))&directed_relstr(sK26_skl))&net_str(sK26_skl,sK25_skl))&(is_eventually_in(sK25_skl,sK26_skl,sK27_skl)&~is_often_in(sK25_skl,sK26_skl,sK27_skl))))),
% 0.18/5.60 inference(skolemize,[status(esa),new_symbols(skolem,[sK25_skl,sK26_skl,sK27_skl]),skolemize(A,sK25_skl),skolemize(B,sK26_skl),skolemize(C,sK27_skl)],[f203])).
% 0.18/5.60 fof(f205,plain,(
% 0.18/5.60 ~empty_carrier(sK25_skl)),
% 0.18/5.60 inference(cnf_transformation,[status(thm)],[f204])).
% 0.18/5.60 fof(f206,plain,(
% 0.18/5.60 one_sorted_str(sK25_skl)),
% 0.18/5.60 inference(cnf_transformation,[status(thm)],[f204])).
% 0.18/5.60 fof(f207,plain,(
% 0.18/5.60 ~empty_carrier(sK26_skl)),
% 0.18/5.60 inference(cnf_transformation,[status(thm)],[f204])).
% 0.18/5.60 fof(f209,plain,(
% 0.18/5.60 directed_relstr(sK26_skl)),
% 0.18/5.60 inference(cnf_transformation,[status(thm)],[f204])).
% 0.18/5.60 fof(f210,plain,(
% 0.18/5.60 net_str(sK26_skl,sK25_skl)),
% 0.18/5.60 inference(cnf_transformation,[status(thm)],[f204])).
% 0.18/5.60 fof(f211,plain,(
% 0.18/5.60 is_eventually_in(sK25_skl,sK26_skl,sK27_skl)),
% 0.18/5.60 inference(cnf_transformation,[status(thm)],[f204])).
% 0.18/5.60 fof(f212,plain,(
% 0.18/5.60 ~is_often_in(sK25_skl,sK26_skl,sK27_skl)),
% 0.18/5.60 inference(cnf_transformation,[status(thm)],[f204])).
% 0.18/5.60 fof(f235,plain,(
% 0.18/5.60 ~one_sorted_str(sK25_skl)|rel_str(sK26_skl)),
% 0.18/5.60 inference(resolution,[status(thm)],[f116,f210])).
% 0.18/5.60 fof(f236,plain,(
% 0.18/5.60 rel_str(sK26_skl)),
% 0.18/5.60 inference(forward_subsumption_resolution,[status(thm)],[f235,f206])).
% 0.18/5.60 fof(f361,plain,(
% 0.18/5.60 ![X0,X1]: (empty_carrier(sK26_skl)|~rel_str(sK26_skl)|~element(X0,the_carrier(sK26_skl))|~element(X1,the_carrier(sK26_skl))|related(sK26_skl,X0,sK4_skl(X1,X0,sK26_skl)))),
% 0.18/5.60 inference(resolution,[status(thm)],[f102,f209])).
% 0.18/5.60 fof(f362,plain,(
% 0.18/5.60 ![X0,X1]: (~rel_str(sK26_skl)|~element(X0,the_carrier(sK26_skl))|~element(X1,the_carrier(sK26_skl))|related(sK26_skl,X0,sK4_skl(X1,X0,sK26_skl)))),
% 0.18/5.60 inference(forward_subsumption_resolution,[status(thm)],[f361,f207])).
% 0.18/5.60 fof(f363,plain,(
% 0.18/5.60 ![X0,X1]: (~element(X0,the_carrier(sK26_skl))|~element(X1,the_carrier(sK26_skl))|related(sK26_skl,X0,sK4_skl(X1,X0,sK26_skl)))),
% 0.18/5.60 inference(forward_subsumption_resolution,[status(thm)],[f362,f236])).
% 0.18/5.60 fof(f364,plain,(
% 0.18/5.60 ![X0,X1,X2]: (~element(sK0_skl(X0,sK26_skl,X1),the_carrier(sK26_skl))|~element(X2,the_carrier(sK26_skl))|empty_carrier(X1)|~one_sorted_str(X1)|empty_carrier(sK26_skl)|~net_str(sK26_skl,X1)|~is_eventually_in(X1,sK26_skl,X0)|~element(sK4_skl(X2,sK0_skl(X0,sK26_skl,X1),sK26_skl),the_carrier(sK26_skl))|in(apply_netmap(X1,sK26_skl,sK4_skl(X2,sK0_skl(X0,sK26_skl,X1),sK26_skl)),X0))),
% 0.18/5.60 inference(resolution,[status(thm)],[f363,f85])).
% 0.18/5.60 fof(f365,plain,(
% 0.18/5.60 ![X0,X1,X2]: (~element(X0,the_carrier(sK26_skl))|empty_carrier(X1)|~one_sorted_str(X1)|empty_carrier(sK26_skl)|~net_str(sK26_skl,X1)|~is_eventually_in(X1,sK26_skl,X2)|~element(sK4_skl(X0,sK0_skl(X2,sK26_skl,X1),sK26_skl),the_carrier(sK26_skl))|in(apply_netmap(X1,sK26_skl,sK4_skl(X0,sK0_skl(X2,sK26_skl,X1),sK26_skl)),X2))),
% 0.18/5.60 inference(forward_subsumption_resolution,[status(thm)],[f364,f84])).
% 0.18/5.60 fof(f366,plain,(
% 0.18/5.60 ![X0,X1,X2]: (~element(X0,the_carrier(sK26_skl))|empty_carrier(X1)|~one_sorted_str(X1)|~net_str(sK26_skl,X1)|~is_eventually_in(X1,sK26_skl,X2)|~element(sK4_skl(X0,sK0_skl(X2,sK26_skl,X1),sK26_skl),the_carrier(sK26_skl))|in(apply_netmap(X1,sK26_skl,sK4_skl(X0,sK0_skl(X2,sK26_skl,X1),sK26_skl)),X2))),
% 0.18/5.60 inference(forward_subsumption_resolution,[status(thm)],[f365,f207])).
% 0.18/5.60 fof(f367,plain,(
% 0.18/5.60 ![X0,X1]: (~element(X0,the_carrier(sK26_skl))|empty_carrier(sK25_skl)|~one_sorted_str(sK25_skl)|~is_eventually_in(sK25_skl,sK26_skl,X1)|~element(sK4_skl(X0,sK0_skl(X1,sK26_skl,sK25_skl),sK26_skl),the_carrier(sK26_skl))|in(apply_netmap(sK25_skl,sK26_skl,sK4_skl(X0,sK0_skl(X1,sK26_skl,sK25_skl),sK26_skl)),X1))),
% 0.18/5.60 inference(resolution,[status(thm)],[f366,f210])).
% 0.18/5.60 fof(f368,plain,(
% 0.18/5.60 ![X0,X1]: (~element(X0,the_carrier(sK26_skl))|~one_sorted_str(sK25_skl)|~is_eventually_in(sK25_skl,sK26_skl,X1)|~element(sK4_skl(X0,sK0_skl(X1,sK26_skl,sK25_skl),sK26_skl),the_carrier(sK26_skl))|in(apply_netmap(sK25_skl,sK26_skl,sK4_skl(X0,sK0_skl(X1,sK26_skl,sK25_skl),sK26_skl)),X1))),
% 0.18/5.60 inference(forward_subsumption_resolution,[status(thm)],[f367,f205])).
% 0.18/5.60 fof(f369,plain,(
% 0.18/5.60 ![X0,X1]: (~element(X0,the_carrier(sK26_skl))|~is_eventually_in(sK25_skl,sK26_skl,X1)|~element(sK4_skl(X0,sK0_skl(X1,sK26_skl,sK25_skl),sK26_skl),the_carrier(sK26_skl))|in(apply_netmap(sK25_skl,sK26_skl,sK4_skl(X0,sK0_skl(X1,sK26_skl,sK25_skl),sK26_skl)),X1))),
% 0.18/5.60 inference(forward_subsumption_resolution,[status(thm)],[f368,f206])).
% 0.18/5.60 fof(f370,plain,(
% 0.18/5.60 ![X0]: (~element(X0,the_carrier(sK26_skl))|~element(sK4_skl(X0,sK0_skl(sK27_skl,sK26_skl,sK25_skl),sK26_skl),the_carrier(sK26_skl))|in(apply_netmap(sK25_skl,sK26_skl,sK4_skl(X0,sK0_skl(sK27_skl,sK26_skl,sK25_skl),sK26_skl)),sK27_skl))),
% 0.18/5.60 inference(resolution,[status(thm)],[f369,f211])).
% 0.18/5.60 fof(f371,plain,(
% 0.18/5.60 ![X0]: (~element(X0,the_carrier(sK26_skl))|in(apply_netmap(sK25_skl,sK26_skl,sK4_skl(X0,sK0_skl(sK27_skl,sK26_skl,sK25_skl),sK26_skl)),sK27_skl)|empty_carrier(sK26_skl)|~rel_str(sK26_skl)|~directed_relstr(sK26_skl)|~element(sK0_skl(sK27_skl,sK26_skl,sK25_skl),the_carrier(sK26_skl))|~element(X0,the_carrier(sK26_skl)))),
% 0.18/5.60 inference(resolution,[status(thm)],[f370,f101])).
% 0.18/5.60 fof(f373,plain,(
% 0.18/5.60 ![X0]: (~element(X0,the_carrier(sK26_skl))|in(apply_netmap(sK25_skl,sK26_skl,sK4_skl(X0,sK0_skl(sK27_skl,sK26_skl,sK25_skl),sK26_skl)),sK27_skl)|empty_carrier(sK26_skl)|~rel_str(sK26_skl)|~directed_relstr(sK26_skl)|~element(sK0_skl(sK27_skl,sK26_skl,sK25_skl),the_carrier(sK26_skl)))),
% 0.18/5.60 inference(duplicate_literals_removal,[status(thm)],[f371])).
% 0.18/5.60 fof(f374,plain,(
% 0.18/5.60 ![X0]: (~element(X0,the_carrier(sK26_skl))|in(apply_netmap(sK25_skl,sK26_skl,sK4_skl(X0,sK0_skl(sK27_skl,sK26_skl,sK25_skl),sK26_skl)),sK27_skl)|~rel_str(sK26_skl)|~directed_relstr(sK26_skl)|~element(sK0_skl(sK27_skl,sK26_skl,sK25_skl),the_carrier(sK26_skl)))),
% 0.18/5.60 inference(forward_subsumption_resolution,[status(thm)],[f373,f207])).
% 0.18/5.60 fof(f375,plain,(
% 0.18/5.60 ![X0]: (~element(X0,the_carrier(sK26_skl))|in(apply_netmap(sK25_skl,sK26_skl,sK4_skl(X0,sK0_skl(sK27_skl,sK26_skl,sK25_skl),sK26_skl)),sK27_skl)|~directed_relstr(sK26_skl)|~element(sK0_skl(sK27_skl,sK26_skl,sK25_skl),the_carrier(sK26_skl)))),
% 0.18/5.60 inference(forward_subsumption_resolution,[status(thm)],[f374,f236])).
% 0.18/5.60 fof(f376,plain,(
% 0.18/5.60 ![X0]: (~element(X0,the_carrier(sK26_skl))|in(apply_netmap(sK25_skl,sK26_skl,sK4_skl(X0,sK0_skl(sK27_skl,sK26_skl,sK25_skl),sK26_skl)),sK27_skl)|~element(sK0_skl(sK27_skl,sK26_skl,sK25_skl),the_carrier(sK26_skl)))),
% 0.18/5.60 inference(resolution,[status(thm)],[f375,f209])).
% 0.18/5.60 fof(f377,plain,(
% 0.18/5.60 ![X0]: (~element(X0,the_carrier(sK26_skl))|in(apply_netmap(sK25_skl,sK26_skl,sK4_skl(X0,sK0_skl(sK27_skl,sK26_skl,sK25_skl),sK26_skl)),sK27_skl)|empty_carrier(sK25_skl)|~one_sorted_str(sK25_skl)|empty_carrier(sK26_skl)|~net_str(sK26_skl,sK25_skl)|~is_eventually_in(sK25_skl,sK26_skl,sK27_skl))),
% 0.18/5.60 inference(resolution,[status(thm)],[f376,f84])).
% 0.18/5.60 fof(f379,plain,(
% 0.18/5.60 ![X0]: (~element(X0,the_carrier(sK26_skl))|in(apply_netmap(sK25_skl,sK26_skl,sK4_skl(X0,sK0_skl(sK27_skl,sK26_skl,sK25_skl),sK26_skl)),sK27_skl)|~one_sorted_str(sK25_skl)|empty_carrier(sK26_skl)|~net_str(sK26_skl,sK25_skl)|~is_eventually_in(sK25_skl,sK26_skl,sK27_skl))),
% 0.18/5.60 inference(forward_subsumption_resolution,[status(thm)],[f377,f205])).
% 0.18/5.60 fof(f380,plain,(
% 0.18/5.60 ![X0]: (~element(X0,the_carrier(sK26_skl))|in(apply_netmap(sK25_skl,sK26_skl,sK4_skl(X0,sK0_skl(sK27_skl,sK26_skl,sK25_skl),sK26_skl)),sK27_skl)|empty_carrier(sK26_skl)|~net_str(sK26_skl,sK25_skl)|~is_eventually_in(sK25_skl,sK26_skl,sK27_skl))),
% 0.18/5.60 inference(forward_subsumption_resolution,[status(thm)],[f379,f206])).
% 0.18/5.60 fof(f381,plain,(
% 0.18/5.60 ![X0]: (~element(X0,the_carrier(sK26_skl))|in(apply_netmap(sK25_skl,sK26_skl,sK4_skl(X0,sK0_skl(sK27_skl,sK26_skl,sK25_skl),sK26_skl)),sK27_skl)|empty_carrier(sK26_skl)|~is_eventually_in(sK25_skl,sK26_skl,sK27_skl))),
% 0.18/5.60 inference(resolution,[status(thm)],[f380,f210])).
% 0.18/5.60 fof(f382,plain,(
% 0.18/5.60 ![X0]: (~element(X0,the_carrier(sK26_skl))|in(apply_netmap(sK25_skl,sK26_skl,sK4_skl(X0,sK0_skl(sK27_skl,sK26_skl,sK25_skl),sK26_skl)),sK27_skl)|~is_eventually_in(sK25_skl,sK26_skl,sK27_skl))),
% 0.18/5.60 inference(forward_subsumption_resolution,[status(thm)],[f381,f207])).
% 0.18/5.60 fof(f383,plain,(
% 0.18/5.60 ![X0]: (~element(X0,the_carrier(sK26_skl))|in(apply_netmap(sK25_skl,sK26_skl,sK4_skl(X0,sK0_skl(sK27_skl,sK26_skl,sK25_skl),sK26_skl)),sK27_skl))),
% 0.18/5.60 inference(forward_subsumption_resolution,[status(thm)],[f382,f211])).
% 0.18/5.60 fof(f384,plain,(
% 0.18/5.60 ![X0]: (~element(X0,the_carrier(sK26_skl))|empty_carrier(sK25_skl)|~one_sorted_str(sK25_skl)|empty_carrier(sK26_skl)|~net_str(sK26_skl,sK25_skl)|is_often_in(sK25_skl,sK26_skl,sK27_skl)|~element(sK4_skl(X0,sK0_skl(sK27_skl,sK26_skl,sK25_skl),sK26_skl),the_carrier(sK26_skl))|~related(sK26_skl,sK3_skl(sK27_skl,sK26_skl,sK25_skl),sK4_skl(X0,sK0_skl(sK27_skl,sK26_skl,sK25_skl),sK26_skl)))),
% 0.18/5.60 inference(resolution,[status(thm)],[f383,f97])).
% 0.18/5.60 fof(f388,plain,(
% 0.18/5.60 ![X0]: (~element(X0,the_carrier(sK26_skl))|~one_sorted_str(sK25_skl)|empty_carrier(sK26_skl)|~net_str(sK26_skl,sK25_skl)|is_often_in(sK25_skl,sK26_skl,sK27_skl)|~element(sK4_skl(X0,sK0_skl(sK27_skl,sK26_skl,sK25_skl),sK26_skl),the_carrier(sK26_skl))|~related(sK26_skl,sK3_skl(sK27_skl,sK26_skl,sK25_skl),sK4_skl(X0,sK0_skl(sK27_skl,sK26_skl,sK25_skl),sK26_skl)))),
% 0.18/5.60 inference(forward_subsumption_resolution,[status(thm)],[f384,f205])).
% 0.18/5.60 fof(f391,plain,(
% 0.18/5.60 ![X0]: (~element(X0,the_carrier(sK26_skl))|empty_carrier(sK26_skl)|~net_str(sK26_skl,sK25_skl)|is_often_in(sK25_skl,sK26_skl,sK27_skl)|~element(sK4_skl(X0,sK0_skl(sK27_skl,sK26_skl,sK25_skl),sK26_skl),the_carrier(sK26_skl))|~related(sK26_skl,sK3_skl(sK27_skl,sK26_skl,sK25_skl),sK4_skl(X0,sK0_skl(sK27_skl,sK26_skl,sK25_skl),sK26_skl)))),
% 0.18/5.60 inference(forward_subsumption_resolution,[status(thm)],[f388,f206])).
% 0.18/5.60 fof(f444,plain,(
% 0.18/5.60 ![X0,X1]: (empty_carrier(sK26_skl)|~rel_str(sK26_skl)|~element(X0,the_carrier(sK26_skl))|~element(X1,the_carrier(sK26_skl))|related(sK26_skl,X1,sK4_skl(X1,X0,sK26_skl)))),
% 0.18/5.60 inference(resolution,[status(thm)],[f103,f209])).
% 0.18/5.60 fof(f445,plain,(
% 0.18/5.60 ![X0,X1]: (~rel_str(sK26_skl)|~element(X0,the_carrier(sK26_skl))|~element(X1,the_carrier(sK26_skl))|related(sK26_skl,X1,sK4_skl(X1,X0,sK26_skl)))),
% 0.18/5.60 inference(forward_subsumption_resolution,[status(thm)],[f444,f207])).
% 0.18/5.60 fof(f449,plain,(
% 0.18/5.60 ![X0,X1]: (~element(X0,the_carrier(sK26_skl))|~element(X1,the_carrier(sK26_skl))|related(sK26_skl,X1,sK4_skl(X1,X0,sK26_skl)))),
% 0.18/5.60 inference(forward_subsumption_resolution,[status(thm)],[f445,f236])).
% 0.18/5.60 fof(f450,plain,(
% 0.18/5.60 ~element(sK0_skl(sK27_skl,sK26_skl,sK25_skl),the_carrier(sK26_skl))|~element(sK3_skl(sK27_skl,sK26_skl,sK25_skl),the_carrier(sK26_skl))|~element(sK3_skl(sK27_skl,sK26_skl,sK25_skl),the_carrier(sK26_skl))|empty_carrier(sK26_skl)|~net_str(sK26_skl,sK25_skl)|is_often_in(sK25_skl,sK26_skl,sK27_skl)|~element(sK4_skl(sK3_skl(sK27_skl,sK26_skl,sK25_skl),sK0_skl(sK27_skl,sK26_skl,sK25_skl),sK26_skl),the_carrier(sK26_skl))),
% 0.18/5.60 inference(resolution,[status(thm)],[f449,f391])).
% 0.18/5.60 fof(f452,plain,(
% 0.18/5.60 ~element(sK0_skl(sK27_skl,sK26_skl,sK25_skl),the_carrier(sK26_skl))|~element(sK3_skl(sK27_skl,sK26_skl,sK25_skl),the_carrier(sK26_skl))|empty_carrier(sK26_skl)|~net_str(sK26_skl,sK25_skl)|is_often_in(sK25_skl,sK26_skl,sK27_skl)|~element(sK4_skl(sK3_skl(sK27_skl,sK26_skl,sK25_skl),sK0_skl(sK27_skl,sK26_skl,sK25_skl),sK26_skl),the_carrier(sK26_skl))),
% 0.18/5.60 inference(duplicate_literals_removal,[status(thm)],[f450])).
% 0.18/5.60 fof(f453,plain,(
% 0.18/5.60 ~element(sK0_skl(sK27_skl,sK26_skl,sK25_skl),the_carrier(sK26_skl))|~element(sK3_skl(sK27_skl,sK26_skl,sK25_skl),the_carrier(sK26_skl))|~net_str(sK26_skl,sK25_skl)|is_often_in(sK25_skl,sK26_skl,sK27_skl)|~element(sK4_skl(sK3_skl(sK27_skl,sK26_skl,sK25_skl),sK0_skl(sK27_skl,sK26_skl,sK25_skl),sK26_skl),the_carrier(sK26_skl))),
% 0.18/5.60 inference(forward_subsumption_resolution,[status(thm)],[f452,f207])).
% 0.18/5.60 fof(f478,plain,(
% 0.18/5.60 ~element(sK0_skl(sK27_skl,sK26_skl,sK25_skl),the_carrier(sK26_skl))|~element(sK3_skl(sK27_skl,sK26_skl,sK25_skl),the_carrier(sK26_skl))|is_often_in(sK25_skl,sK26_skl,sK27_skl)|~element(sK4_skl(sK3_skl(sK27_skl,sK26_skl,sK25_skl),sK0_skl(sK27_skl,sK26_skl,sK25_skl),sK26_skl),the_carrier(sK26_skl))),
% 0.18/5.60 inference(forward_subsumption_resolution,[status(thm)],[f453,f210])).
% 0.18/5.60 fof(f481,plain,(
% 0.18/5.60 ~element(sK0_skl(sK27_skl,sK26_skl,sK25_skl),the_carrier(sK26_skl))|~element(sK3_skl(sK27_skl,sK26_skl,sK25_skl),the_carrier(sK26_skl))|is_often_in(sK25_skl,sK26_skl,sK27_skl)|empty_carrier(sK26_skl)|~rel_str(sK26_skl)|~directed_relstr(sK26_skl)|~element(sK0_skl(sK27_skl,sK26_skl,sK25_skl),the_carrier(sK26_skl))|~element(sK3_skl(sK27_skl,sK26_skl,sK25_skl),the_carrier(sK26_skl))),
% 0.18/5.60 inference(resolution,[status(thm)],[f478,f101])).
% 0.18/5.60 fof(f486,plain,(
% 0.18/5.60 ~element(sK0_skl(sK27_skl,sK26_skl,sK25_skl),the_carrier(sK26_skl))|~element(sK3_skl(sK27_skl,sK26_skl,sK25_skl),the_carrier(sK26_skl))|is_often_in(sK25_skl,sK26_skl,sK27_skl)|empty_carrier(sK26_skl)|~rel_str(sK26_skl)|~directed_relstr(sK26_skl)),
% 0.18/5.60 inference(duplicate_literals_removal,[status(thm)],[f481])).
% 0.18/5.60 fof(f487,plain,(
% 0.18/5.60 ~element(sK0_skl(sK27_skl,sK26_skl,sK25_skl),the_carrier(sK26_skl))|~element(sK3_skl(sK27_skl,sK26_skl,sK25_skl),the_carrier(sK26_skl))|empty_carrier(sK26_skl)|~rel_str(sK26_skl)|~directed_relstr(sK26_skl)),
% 0.18/5.60 inference(forward_subsumption_resolution,[status(thm)],[f486,f212])).
% 0.18/5.60 fof(f489,plain,(
% 0.18/5.60 ~element(sK0_skl(sK27_skl,sK26_skl,sK25_skl),the_carrier(sK26_skl))|~element(sK3_skl(sK27_skl,sK26_skl,sK25_skl),the_carrier(sK26_skl))|~rel_str(sK26_skl)|~directed_relstr(sK26_skl)),
% 0.18/5.60 inference(forward_subsumption_resolution,[status(thm)],[f487,f207])).
% 0.18/5.60 fof(f490,plain,(
% 0.18/5.60 ~element(sK0_skl(sK27_skl,sK26_skl,sK25_skl),the_carrier(sK26_skl))|~element(sK3_skl(sK27_skl,sK26_skl,sK25_skl),the_carrier(sK26_skl))|~directed_relstr(sK26_skl)),
% 0.18/5.60 inference(resolution,[status(thm)],[f489,f236])).
% 0.18/5.60 fof(f491,plain,(
% 0.18/5.60 ~element(sK0_skl(sK27_skl,sK26_skl,sK25_skl),the_carrier(sK26_skl))|~element(sK3_skl(sK27_skl,sK26_skl,sK25_skl),the_carrier(sK26_skl))),
% 0.18/5.60 inference(forward_subsumption_resolution,[status(thm)],[f490,f209])).
% 0.18/5.60 fof(f492,plain,(
% 0.18/5.60 ~element(sK0_skl(sK27_skl,sK26_skl,sK25_skl),the_carrier(sK26_skl))|empty_carrier(sK25_skl)|~one_sorted_str(sK25_skl)|empty_carrier(sK26_skl)|~net_str(sK26_skl,sK25_skl)|is_often_in(sK25_skl,sK26_skl,sK27_skl)),
% 0.18/5.60 inference(resolution,[status(thm)],[f491,f96])).
% 0.18/5.60 fof(f494,plain,(
% 0.18/5.60 ~element(sK0_skl(sK27_skl,sK26_skl,sK25_skl),the_carrier(sK26_skl))|~one_sorted_str(sK25_skl)|empty_carrier(sK26_skl)|~net_str(sK26_skl,sK25_skl)|is_often_in(sK25_skl,sK26_skl,sK27_skl)),
% 0.18/5.60 inference(forward_subsumption_resolution,[status(thm)],[f492,f205])).
% 0.18/5.60 fof(f495,plain,(
% 0.18/5.60 ~element(sK0_skl(sK27_skl,sK26_skl,sK25_skl),the_carrier(sK26_skl))|empty_carrier(sK26_skl)|~net_str(sK26_skl,sK25_skl)|is_often_in(sK25_skl,sK26_skl,sK27_skl)),
% 0.18/5.60 inference(forward_subsumption_resolution,[status(thm)],[f494,f206])).
% 0.18/5.60 fof(f496,plain,(
% 0.18/5.60 ~element(sK0_skl(sK27_skl,sK26_skl,sK25_skl),the_carrier(sK26_skl))|empty_carrier(sK26_skl)|is_often_in(sK25_skl,sK26_skl,sK27_skl)),
% 0.18/5.60 inference(resolution,[status(thm)],[f495,f210])).
% 0.18/5.60 fof(f497,plain,(
% 0.18/5.60 ~element(sK0_skl(sK27_skl,sK26_skl,sK25_skl),the_carrier(sK26_skl))|is_often_in(sK25_skl,sK26_skl,sK27_skl)),
% 0.18/5.60 inference(forward_subsumption_resolution,[status(thm)],[f496,f207])).
% 0.18/5.60 fof(f498,plain,(
% 0.18/5.60 ~element(sK0_skl(sK27_skl,sK26_skl,sK25_skl),the_carrier(sK26_skl))),
% 0.18/5.60 inference(forward_subsumption_resolution,[status(thm)],[f497,f212])).
% 0.18/5.60 fof(f499,plain,(
% 0.18/5.61 empty_carrier(sK25_skl)|~one_sorted_str(sK25_skl)|empty_carrier(sK26_skl)|~net_str(sK26_skl,sK25_skl)|~is_eventually_in(sK25_skl,sK26_skl,sK27_skl)),
% 0.18/5.61 inference(resolution,[status(thm)],[f498,f84])).
% 0.18/5.61 fof(f501,plain,(
% 0.18/5.61 ~one_sorted_str(sK25_skl)|empty_carrier(sK26_skl)|~net_str(sK26_skl,sK25_skl)|~is_eventually_in(sK25_skl,sK26_skl,sK27_skl)),
% 0.18/5.61 inference(forward_subsumption_resolution,[status(thm)],[f499,f205])).
% 0.18/5.61 fof(f502,plain,(
% 0.18/5.61 empty_carrier(sK26_skl)|~net_str(sK26_skl,sK25_skl)|~is_eventually_in(sK25_skl,sK26_skl,sK27_skl)),
% 0.18/5.61 inference(forward_subsumption_resolution,[status(thm)],[f501,f206])).
% 0.18/5.61 fof(f503,plain,(
% 0.18/5.61 empty_carrier(sK26_skl)|~is_eventually_in(sK25_skl,sK26_skl,sK27_skl)),
% 0.18/5.61 inference(resolution,[status(thm)],[f502,f210])).
% 0.18/5.61 fof(f504,plain,(
% 0.18/5.61 ~is_eventually_in(sK25_skl,sK26_skl,sK27_skl)),
% 0.18/5.61 inference(forward_subsumption_resolution,[status(thm)],[f503,f207])).
% 0.18/5.61 fof(f511,plain,(
% 0.18/5.61 $false),
% 0.18/5.61 inference(forward_subsumption_resolution,[status(thm)],[f504,f211])).
% 0.18/5.61 % SZS output end CNFRefutation for theBenchmark.p
% 0.18/5.63 % Elapsed time: 0.192269 seconds
% 0.18/5.63 % CPU time: 1.320646 seconds
% 0.18/5.63 % Total memory used: 119.002 MB
% 0.18/5.63 % Net memory used: 118.237 MB
%------------------------------------------------------------------------------