%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU362+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 : n009.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:26 PM UTC 2026
% Result : Theorem 0.19s 0.53s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SEU362+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.19/0.45 % Computer : n009.cluster.edu
% 0.19/0.45 % Model : x86_64 x86_64
% 0.19/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.45 % Memory : 8046.5625MB
% 0.19/0.45 % OS : Linux 6.8.0-71-generic
% 0.19/0.45 % CPULimit : 300
% 0.19/0.45 % WCLimit : 300
% 0.19/0.45 % DateTime : Mon Sep 21 06:15:27 UTC 2026
% 0.19/0.46 % CPUTime :
% 0.19/0.49 % Drodi V4.1.1
% 0.19/0.53 % Refutation found
% 0.19/0.53 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.19/0.53 % SZS output start CNFRefutation for theBenchmark
% 0.19/0.53 fof(f5,axiom,(
% 0.19/0.53 (! [A] :( rel_str(A)=> (! [B] :( rel_str(B)=> ( subrelstr(B,A)<=> ( subset(the_carrier(B),the_carrier(A))& subset(the_InternalRel(B),the_InternalRel(A)) ) ) ) )) )),
% 0.19/0.53 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.19/0.53 fof(f6,axiom,(
% 0.19/0.53 (! [A] :( rel_str(A)=> (! [B] :( element(B,the_carrier(A))=> (! [C] :( element(C,the_carrier(A))=> ( related(A,B,C)<=> in(ordered_pair(B,C),the_InternalRel(A)) ) ) )) )) )),
% 0.19/0.53 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.19/0.53 fof(f15,axiom,(
% 0.19/0.53 (! [A] :( rel_str(A)=> (! [B] :( subrelstr(B,A)=> rel_str(B) ) )) )),
% 0.19/0.53 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.19/0.53 fof(f28,axiom,(
% 0.19/0.53 (? [A] : empty(A) )),
% 0.19/0.53 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.19/0.53 fof(f35,axiom,(
% 0.19/0.53 (! [A,B] :( element(A,B)=> ( empty(B)| in(A,B) ) ) )),
% 0.19/0.53 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.19/0.53 fof(f36,axiom,(
% 0.19/0.53 (! [A,B] :( element(A,powerset(B))<=> subset(A,B) ) )),
% 0.19/0.53 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.19/0.53 fof(f37,axiom,(
% 0.19/0.53 (! [A,B,C] :( ( in(A,B)& element(B,powerset(C)) )=> element(A,C) ) )),
% 0.19/0.53 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.19/0.53 fof(f38,axiom,(
% 0.19/0.53 (! [A,B,C] :~ ( in(A,B)& element(B,powerset(C))& empty(C) ) )),
% 0.19/0.53 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.19/0.53 fof(f39,conjecture,(
% 0.19/0.53 (! [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.19/0.53 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.19/0.53 fof(f40,negated_conjecture,(
% 0.19/0.53 ~((! [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.19/0.53 inference(negated_conjecture,[status(cth)],[f39])).
% 0.19/0.53 fof(f41,axiom,(
% 0.19/0.53 (! [A] :( empty(A)=> A = empty_set ) )),
% 0.19/0.53 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.19/0.53 fof(f53,plain,(
% 0.19/0.53 ![A]: (~rel_str(A)|(![B]: (~rel_str(B)|(subrelstr(B,A)<=>(subset(the_carrier(B),the_carrier(A))&subset(the_InternalRel(B),the_InternalRel(A)))))))),
% 0.19/0.53 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 0.19/0.53 fof(f54,plain,(
% 0.19/0.53 ![A]: (~rel_str(A)|(![B]: (~rel_str(B)|((~subrelstr(B,A)|(subset(the_carrier(B),the_carrier(A))&subset(the_InternalRel(B),the_InternalRel(A))))&(subrelstr(B,A)|(~subset(the_carrier(B),the_carrier(A))|~subset(the_InternalRel(B),the_InternalRel(A))))))))),
% 0.19/0.53 inference(NNF_transformation,[status(thm)],[f53])).
% 0.19/0.53 fof(f56,plain,(
% 0.19/0.53 ![X0,X1]: (~rel_str(X0)|~rel_str(X1)|~subrelstr(X1,X0)|subset(the_InternalRel(X1),the_InternalRel(X0)))),
% 0.19/0.53 inference(cnf_transformation,[status(thm)],[f54])).
% 0.19/0.53 fof(f58,plain,(
% 0.19/0.53 ![A]: (~rel_str(A)|(![B]: (~element(B,the_carrier(A))|(![C]: (~element(C,the_carrier(A))|(related(A,B,C)<=>in(ordered_pair(B,C),the_InternalRel(A))))))))),
% 0.19/0.53 inference(pre_NNF_transformation,[status(thm)],[f6])).
% 0.19/0.53 fof(f59,plain,(
% 0.19/0.53 ![A]: (~rel_str(A)|(![B]: (~element(B,the_carrier(A))|(![C]: (~element(C,the_carrier(A))|((~related(A,B,C)|in(ordered_pair(B,C),the_InternalRel(A)))&(related(A,B,C)|~in(ordered_pair(B,C),the_InternalRel(A)))))))))),
% 0.19/0.53 inference(NNF_transformation,[status(thm)],[f58])).
% 0.19/0.53 fof(f60,plain,(
% 0.19/0.53 ![X0,X1,X2]: (~rel_str(X0)|~element(X1,the_carrier(X0))|~element(X2,the_carrier(X0))|~related(X0,X1,X2)|in(ordered_pair(X1,X2),the_InternalRel(X0)))),
% 0.19/0.53 inference(cnf_transformation,[status(thm)],[f59])).
% 0.19/0.53 fof(f61,plain,(
% 0.19/0.53 ![X0,X1,X2]: (~rel_str(X0)|~element(X1,the_carrier(X0))|~element(X2,the_carrier(X0))|related(X0,X1,X2)|~in(ordered_pair(X1,X2),the_InternalRel(X0)))),
% 0.19/0.53 inference(cnf_transformation,[status(thm)],[f59])).
% 0.19/0.53 fof(f64,plain,(
% 0.19/0.53 ![A]: (~rel_str(A)|(![B]: (~subrelstr(B,A)|rel_str(B))))),
% 0.19/0.53 inference(pre_NNF_transformation,[status(thm)],[f15])).
% 0.19/0.53 fof(f65,plain,(
% 0.19/0.53 ![X0,X1]: (~rel_str(X0)|~subrelstr(X1,X0)|rel_str(X1))),
% 0.19/0.53 inference(cnf_transformation,[status(thm)],[f64])).
% 0.19/0.53 fof(f89,plain,(
% 0.19/0.53 empty(sK7_skl)),
% 0.19/0.53 inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl]),skolemize(A,sK7_skl)],[f28])).
% 0.19/0.53 fof(f90,plain,(
% 0.19/0.53 empty(sK7_skl)),
% 0.19/0.53 inference(cnf_transformation,[status(thm)],[f89])).
% 0.19/0.53 fof(f111,plain,(
% 0.19/0.53 ![A,B]: (~element(A,B)|(empty(B)|in(A,B)))),
% 0.19/0.53 inference(pre_NNF_transformation,[status(thm)],[f35])).
% 0.19/0.53 fof(f112,plain,(
% 0.19/0.53 ![X0,X1]: (~element(X0,X1)|empty(X1)|in(X0,X1))),
% 0.19/0.53 inference(cnf_transformation,[status(thm)],[f111])).
% 0.19/0.53 fof(f113,plain,(
% 0.19/0.53 ![A,B]: ((~element(A,powerset(B))|subset(A,B))&(element(A,powerset(B))|~subset(A,B)))),
% 0.19/0.53 inference(NNF_transformation,[status(thm)],[f36])).
% 0.19/0.53 fof(f114,plain,(
% 0.19/0.53 (![A,B]: (~element(A,powerset(B))|subset(A,B)))&(![A,B]: (element(A,powerset(B))|~subset(A,B)))),
% 0.19/0.53 inference(miniscoping,[status(thm)],[f113])).
% 0.19/0.53 fof(f116,plain,(
% 0.19/0.53 ![X0,X1]: (element(X0,powerset(X1))|~subset(X0,X1))),
% 0.19/0.53 inference(cnf_transformation,[status(thm)],[f114])).
% 0.19/0.53 fof(f117,plain,(
% 0.19/0.53 ![A,B,C]: ((~in(A,B)|~element(B,powerset(C)))|element(A,C))),
% 0.19/0.53 inference(pre_NNF_transformation,[status(thm)],[f37])).
% 0.19/0.53 fof(f118,plain,(
% 0.19/0.53 ![A,C]: ((![B]: (~in(A,B)|~element(B,powerset(C))))|element(A,C))),
% 0.19/0.53 inference(miniscoping,[status(thm)],[f117])).
% 0.19/0.53 fof(f119,plain,(
% 0.19/0.53 ![X0,X1,X2]: (~in(X0,X1)|~element(X1,powerset(X2))|element(X0,X2))),
% 0.19/0.53 inference(cnf_transformation,[status(thm)],[f118])).
% 0.19/0.53 fof(f120,plain,(
% 0.19/0.53 ![A,B,C]: ((~in(A,B)|~element(B,powerset(C)))|~empty(C))),
% 0.19/0.53 inference(pre_NNF_transformation,[status(thm)],[f38])).
% 0.19/0.53 fof(f121,plain,(
% 0.19/0.53 ![C]: ((![B]: ((![A]: ~in(A,B))|~element(B,powerset(C))))|~empty(C))),
% 0.19/0.53 inference(miniscoping,[status(thm)],[f120])).
% 0.19/0.53 fof(f122,plain,(
% 0.19/0.53 ![X0,X1,X2]: (~in(X0,X1)|~element(X1,powerset(X2))|~empty(X2))),
% 0.19/0.53 inference(cnf_transformation,[status(thm)],[f121])).
% 0.19/0.53 fof(f123,plain,(
% 0.19/0.53 (?[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.19/0.53 inference(pre_NNF_transformation,[status(thm)],[f40])).
% 0.19/0.53 fof(f124,plain,(
% 0.19/0.53 (rel_str(sK11_skl)&(subrelstr(sK12_skl,sK11_skl)&(element(sK13_skl,the_carrier(sK11_skl))&(element(sK14_skl,the_carrier(sK11_skl))&(element(sK15_skl,the_carrier(sK12_skl))&(element(sK16_skl,the_carrier(sK12_skl))&(((sK15_skl=sK13_skl&sK16_skl=sK14_skl)&related(sK12_skl,sK15_skl,sK16_skl))&~related(sK11_skl,sK13_skl,sK14_skl))))))))),
% 0.19/0.53 inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl,sK12_skl,sK13_skl,sK14_skl,sK15_skl,sK16_skl]),skolemize(A,sK11_skl),skolemize(B,sK12_skl),skolemize(C,sK13_skl),skolemize(D,sK14_skl),skolemize(E,sK15_skl),skolemize(F,sK16_skl)],[f123])).
% 0.19/0.53 fof(f125,plain,(
% 0.19/0.53 rel_str(sK11_skl)),
% 0.19/0.53 inference(cnf_transformation,[status(thm)],[f124])).
% 0.19/0.53 fof(f126,plain,(
% 0.19/0.53 subrelstr(sK12_skl,sK11_skl)),
% 0.19/0.53 inference(cnf_transformation,[status(thm)],[f124])).
% 0.19/0.53 fof(f127,plain,(
% 0.19/0.53 element(sK13_skl,the_carrier(sK11_skl))),
% 0.19/0.53 inference(cnf_transformation,[status(thm)],[f124])).
% 0.19/0.53 fof(f128,plain,(
% 0.19/0.53 element(sK14_skl,the_carrier(sK11_skl))),
% 0.19/0.53 inference(cnf_transformation,[status(thm)],[f124])).
% 0.19/0.53 fof(f129,plain,(
% 0.19/0.53 element(sK15_skl,the_carrier(sK12_skl))),
% 0.19/0.53 inference(cnf_transformation,[status(thm)],[f124])).
% 0.19/0.53 fof(f130,plain,(
% 0.19/0.53 element(sK16_skl,the_carrier(sK12_skl))),
% 0.19/0.53 inference(cnf_transformation,[status(thm)],[f124])).
% 0.19/0.53 fof(f131,plain,(
% 0.19/0.53 sK15_skl=sK13_skl),
% 0.19/0.53 inference(cnf_transformation,[status(thm)],[f124])).
% 0.19/0.53 fof(f132,plain,(
% 0.19/0.53 sK16_skl=sK14_skl),
% 0.19/0.53 inference(cnf_transformation,[status(thm)],[f124])).
% 0.19/0.53 fof(f133,plain,(
% 0.19/0.53 related(sK12_skl,sK15_skl,sK16_skl)),
% 0.19/0.53 inference(cnf_transformation,[status(thm)],[f124])).
% 0.19/0.53 fof(f134,plain,(
% 0.19/0.53 ~related(sK11_skl,sK13_skl,sK14_skl)),
% 0.19/0.53 inference(cnf_transformation,[status(thm)],[f124])).
% 0.19/0.53 fof(f135,plain,(
% 0.19/0.53 ![A]: (~empty(A)|A=empty_set)),
% 0.19/0.53 inference(pre_NNF_transformation,[status(thm)],[f41])).
% 0.19/0.53 fof(f136,plain,(
% 0.19/0.53 ![X0]: (~empty(X0)|X0=empty_set)),
% 0.19/0.53 inference(cnf_transformation,[status(thm)],[f135])).
% 0.19/0.53 fof(f143,plain,(
% 0.19/0.53 ![X0,X1]: (~rel_str(X0)|~subrelstr(X1,X0)|subset(the_InternalRel(X1),the_InternalRel(X0)))),
% 0.19/0.53 inference(backward_subsumption_resolution,[status(thm)],[f56,f65])).
% 0.19/0.53 fof(f145,plain,(
% 0.19/0.53 element(sK15_skl,the_carrier(sK11_skl))),
% 0.19/0.53 inference(backward_demodulation,[status(thm)],[f131,f127])).
% 0.19/0.53 fof(f146,plain,(
% 0.19/0.53 element(sK16_skl,the_carrier(sK11_skl))),
% 0.19/0.53 inference(backward_demodulation,[status(thm)],[f132,f128])).
% 0.19/0.53 fof(f147,plain,(
% 0.19/0.53 ~related(sK11_skl,sK15_skl,sK14_skl)),
% 0.19/0.53 inference(forward_demodulation,[status(thm)],[f131,f134])).
% 0.19/0.53 fof(f148,plain,(
% 0.19/0.53 ~related(sK11_skl,sK15_skl,sK16_skl)),
% 0.19/0.53 inference(forward_demodulation,[status(thm)],[f132,f147])).
% 0.19/0.53 fof(f149,plain,(
% 0.19/0.53 ![X0]: (~subrelstr(X0,sK11_skl)|rel_str(X0))),
% 0.19/0.53 inference(resolution,[status(thm)],[f65,f125])).
% 0.19/0.53 fof(f150,plain,(
% 0.19/0.53 rel_str(sK12_skl)),
% 0.19/0.53 inference(resolution,[status(thm)],[f149,f126])).
% 0.19/0.53 fof(f167,plain,(
% 0.19/0.53 sK7_skl=empty_set),
% 0.19/0.53 inference(resolution,[status(thm)],[f136,f90])).
% 0.19/0.53 fof(f169,plain,(
% 0.19/0.53 ![X0]: (~empty(X0)|X0=sK7_skl)),
% 0.19/0.53 inference(backward_demodulation,[status(thm)],[f167,f136])).
% 0.19/0.53 fof(f173,plain,(
% 0.19/0.53 ~rel_str(sK12_skl)|~element(sK15_skl,the_carrier(sK12_skl))|~element(sK16_skl,the_carrier(sK12_skl))|in(ordered_pair(sK15_skl,sK16_skl),the_InternalRel(sK12_skl))),
% 0.19/0.53 inference(resolution,[status(thm)],[f60,f133])).
% 0.19/0.53 fof(f174,plain,(
% 0.19/0.53 ~element(sK15_skl,the_carrier(sK12_skl))|~element(sK16_skl,the_carrier(sK12_skl))|in(ordered_pair(sK15_skl,sK16_skl),the_InternalRel(sK12_skl))),
% 0.19/0.53 inference(forward_subsumption_resolution,[status(thm)],[f173,f150])).
% 0.19/0.53 fof(f175,plain,(
% 0.19/0.53 ~element(sK16_skl,the_carrier(sK12_skl))|in(ordered_pair(sK15_skl,sK16_skl),the_InternalRel(sK12_skl))),
% 0.19/0.53 inference(resolution,[status(thm)],[f174,f129])).
% 0.19/0.53 fof(f176,plain,(
% 0.19/0.53 in(ordered_pair(sK15_skl,sK16_skl),the_InternalRel(sK12_skl))),
% 0.19/0.53 inference(forward_subsumption_resolution,[status(thm)],[f175,f130])).
% 0.19/0.53 fof(f266,plain,(
% 0.19/0.53 ![X0,X1,X2]: (~element(ordered_pair(X0,X1),the_InternalRel(X2))|empty(the_InternalRel(X2))|~rel_str(X2)|~element(X0,the_carrier(X2))|~element(X1,the_carrier(X2))|related(X2,X0,X1))),
% 0.19/0.53 inference(resolution,[status(thm)],[f112,f61])).
% 0.19/0.53 fof(f272,plain,(
% 0.19/0.53 ![X0]: (~element(the_InternalRel(sK12_skl),powerset(X0))|element(ordered_pair(sK15_skl,sK16_skl),X0))),
% 0.19/0.53 inference(resolution,[status(thm)],[f119,f176])).
% 0.19/0.53 fof(f274,plain,(
% 0.19/0.53 ![X0,X1]: (~in(X0,X1)|~element(X1,powerset(sK7_skl)))),
% 0.19/0.53 inference(resolution,[status(thm)],[f122,f90])).
% 0.19/0.53 fof(f283,plain,(
% 0.19/0.53 ![X0]: (element(ordered_pair(sK15_skl,sK16_skl),X0)|~subset(the_InternalRel(sK12_skl),X0))),
% 0.19/0.53 inference(resolution,[status(thm)],[f272,f116])).
% 0.19/0.53 fof(f285,plain,(
% 0.19/0.53 ![X0]: (element(ordered_pair(sK15_skl,sK16_skl),the_InternalRel(X0))|~rel_str(X0)|~subrelstr(sK12_skl,X0))),
% 0.19/0.53 inference(resolution,[status(thm)],[f283,f143])).
% 0.19/0.53 fof(f295,plain,(
% 0.19/0.53 ~element(the_InternalRel(sK12_skl),powerset(sK7_skl))),
% 0.19/0.53 inference(resolution,[status(thm)],[f274,f176])).
% 0.19/0.53 fof(f297,plain,(
% 0.19/0.53 ~subset(the_InternalRel(sK12_skl),sK7_skl)),
% 0.19/0.53 inference(resolution,[status(thm)],[f295,f116])).
% 0.19/0.53 fof(f354,plain,(
% 0.19/0.53 ![X0]: (empty(the_InternalRel(X0))|~rel_str(X0)|~element(sK15_skl,the_carrier(X0))|~element(sK16_skl,the_carrier(X0))|related(X0,sK15_skl,sK16_skl)|~rel_str(X0)|~subrelstr(sK12_skl,X0))),
% 0.19/0.53 inference(resolution,[status(thm)],[f266,f285])).
% 0.19/0.53 fof(f355,plain,(
% 0.19/0.53 ![X0]: (empty(the_InternalRel(X0))|~rel_str(X0)|~element(sK15_skl,the_carrier(X0))|~element(sK16_skl,the_carrier(X0))|related(X0,sK15_skl,sK16_skl)|~subrelstr(sK12_skl,X0))),
% 0.19/0.53 inference(duplicate_literals_removal,[status(thm)],[f354])).
% 0.19/0.53 fof(f376,plain,(
% 0.19/0.53 empty(the_InternalRel(sK11_skl))|~rel_str(sK11_skl)|~element(sK16_skl,the_carrier(sK11_skl))|related(sK11_skl,sK15_skl,sK16_skl)|~subrelstr(sK12_skl,sK11_skl)),
% 0.19/0.53 inference(resolution,[status(thm)],[f355,f145])).
% 0.19/0.53 fof(f378,plain,(
% 0.19/0.53 empty(the_InternalRel(sK11_skl))|~element(sK16_skl,the_carrier(sK11_skl))|related(sK11_skl,sK15_skl,sK16_skl)|~subrelstr(sK12_skl,sK11_skl)),
% 0.19/0.53 inference(forward_subsumption_resolution,[status(thm)],[f376,f125])).
% 0.19/0.53 fof(f388,plain,(
% 0.19/0.53 empty(the_InternalRel(sK11_skl))|related(sK11_skl,sK15_skl,sK16_skl)|~subrelstr(sK12_skl,sK11_skl)),
% 0.19/0.54 inference(resolution,[status(thm)],[f378,f146])).
% 0.19/0.54 fof(f389,plain,(
% 0.19/0.54 empty(the_InternalRel(sK11_skl))|~subrelstr(sK12_skl,sK11_skl)),
% 0.19/0.54 inference(forward_subsumption_resolution,[status(thm)],[f388,f148])).
% 0.19/0.54 fof(f390,plain,(
% 0.19/0.54 empty(the_InternalRel(sK11_skl))),
% 0.19/0.54 inference(resolution,[status(thm)],[f389,f126])).
% 0.19/0.54 fof(f393,plain,(
% 0.19/0.54 the_InternalRel(sK11_skl)=sK7_skl),
% 0.19/0.54 inference(resolution,[status(thm)],[f390,f169])).
% 0.19/0.54 fof(f406,plain,(
% 0.19/0.54 ![X0]: (~rel_str(sK11_skl)|~subrelstr(X0,sK11_skl)|subset(the_InternalRel(X0),sK7_skl))),
% 0.19/0.54 inference(paramodulation,[status(thm)],[f393,f143])).
% 0.19/0.54 fof(f415,plain,(
% 0.19/0.54 ![X0]: (~subrelstr(X0,sK11_skl)|subset(the_InternalRel(X0),sK7_skl))),
% 0.19/0.54 inference(forward_subsumption_resolution,[status(thm)],[f406,f125])).
% 0.19/0.54 fof(f420,plain,(
% 0.19/0.54 subset(the_InternalRel(sK12_skl),sK7_skl)),
% 0.19/0.54 inference(resolution,[status(thm)],[f415,f126])).
% 0.19/0.54 fof(f422,plain,(
% 0.19/0.54 $false),
% 0.19/0.54 inference(forward_subsumption_resolution,[status(thm)],[f420,f297])).
% 0.19/0.54 % SZS output end CNFRefutation for theBenchmark.p
% 0.19/0.56 % Elapsed time: 0.095673 seconds
% 0.19/0.56 % CPU time: 0.324923 seconds
% 0.19/0.56 % Total memory used: 61.819 MB
% 0.19/0.56 % Net memory used: 61.626 MB
%------------------------------------------------------------------------------