%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU363+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 : n012.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.04s 0.35s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SEU363+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.02 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.04/0.29 % Computer : n012.cluster.edu
% 0.04/0.29 % Model : x86_64 x86_64
% 0.04/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.04/0.29 % Memory : 8046.5625MB
% 0.04/0.29 % OS : Linux 6.8.0-71-generic
% 0.04/0.29 % CPULimit : 300
% 0.04/0.29 % WCLimit : 300
% 0.04/0.29 % DateTime : Mon Sep 21 06:15:06 UTC 2026
% 0.04/0.30 % CPUTime :
% 0.04/0.30 % Drodi V4.1.1
% 0.04/0.35 % Refutation found
% 0.04/0.35 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.04/0.35 % SZS output start CNFRefutation for theBenchmark
% 0.04/0.35 fof(f3,axiom,(
% 0.04/0.35 (! [A,B,C] :( element(C,powerset(cartesian_product2(A,B)))=> relation(C) ) )),
% 0.04/0.35 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.04/0.35 fof(f5,axiom,(
% 0.04/0.35 (! [A] :( rel_str(A)=> (! [B] :( subrelstr(B,A)=> ( full_subrelstr(B,A)<=> the_InternalRel(B) = relation_restriction_as_relation_of(the_InternalRel(A),the_carrier(B)) ) ) )) )),
% 0.04/0.35 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.04/0.35 fof(f6,axiom,(
% 0.04/0.35 (! [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.04/0.35 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.04/0.35 fof(f17,axiom,(
% 0.04/0.35 (! [A] :( rel_str(A)=> (! [B] :( subrelstr(B,A)=> rel_str(B) ) )) )),
% 0.04/0.35 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.04/0.35 fof(f18,axiom,(
% 0.04/0.35 (! [A,B,C] :( relation_of2_as_subset(C,A,B)=> element(C,powerset(cartesian_product2(A,B))) ) )),
% 0.04/0.35 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.04/0.35 fof(f19,axiom,(
% 0.04/0.35 (! [A] :( rel_str(A)=> relation_of2_as_subset(the_InternalRel(A),the_carrier(A),the_carrier(A)) ) )),
% 0.04/0.35 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.04/0.35 fof(f34,axiom,(
% 0.04/0.35 (! [A,B] :( relation(A)=> relation_restriction_as_relation_of(A,B) = relation_restriction(A,B) ) )),
% 0.04/0.35 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.04/0.35 fof(f37,axiom,(
% 0.04/0.35 (! [A,B,C,D] :( in(ordered_pair(A,B),cartesian_product2(C,D))<=> ( in(A,C)& in(B,D) ) ) )),
% 0.04/0.35 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.04/0.35 fof(f38,axiom,(
% 0.04/0.35 (! [A,B,C] :( relation(C)=> ( in(A,relation_restriction(C,B))<=> ( in(A,C)& in(A,cartesian_product2(B,B)) ) ) ) )),
% 0.04/0.35 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.04/0.35 fof(f44,conjecture,(
% 0.04/0.35 (! [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) ) ) )) )) )) )) )) )),
% 0.04/0.35 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.04/0.35 fof(f45,negated_conjecture,(
% 0.04/0.35 ~((! [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) ) ) )) )) )) )) )) ))),
% 0.04/0.35 inference(negated_conjecture,[status(cth)],[f44])).
% 0.04/0.35 fof(f53,plain,(
% 0.04/0.35 ![A,B,C]: (~element(C,powerset(cartesian_product2(A,B)))|relation(C))),
% 0.04/0.35 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 0.04/0.35 fof(f54,plain,(
% 0.04/0.35 ![C]: ((![A,B]: ~element(C,powerset(cartesian_product2(A,B))))|relation(C))),
% 0.04/0.35 inference(miniscoping,[status(thm)],[f53])).
% 0.04/0.35 fof(f55,plain,(
% 0.04/0.35 ![X0,X1,X2]: (~element(X0,powerset(cartesian_product2(X1,X2)))|relation(X0))),
% 0.04/0.35 inference(cnf_transformation,[status(thm)],[f54])).
% 0.04/0.35 fof(f58,plain,(
% 0.04/0.35 ![A]: (~rel_str(A)|(![B]: (~subrelstr(B,A)|(full_subrelstr(B,A)<=>the_InternalRel(B)=relation_restriction_as_relation_of(the_InternalRel(A),the_carrier(B))))))),
% 0.04/0.35 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 0.04/0.35 fof(f59,plain,(
% 0.04/0.35 ![A]: (~rel_str(A)|(![B]: (~subrelstr(B,A)|((~full_subrelstr(B,A)|the_InternalRel(B)=relation_restriction_as_relation_of(the_InternalRel(A),the_carrier(B)))&(full_subrelstr(B,A)|~the_InternalRel(B)=relation_restriction_as_relation_of(the_InternalRel(A),the_carrier(B)))))))),
% 0.04/0.35 inference(NNF_transformation,[status(thm)],[f58])).
% 0.04/0.35 fof(f60,plain,(
% 0.04/0.35 ![X0,X1]: (~rel_str(X0)|~subrelstr(X1,X0)|~full_subrelstr(X1,X0)|the_InternalRel(X1)=relation_restriction_as_relation_of(the_InternalRel(X0),the_carrier(X1)))),
% 0.04/0.35 inference(cnf_transformation,[status(thm)],[f59])).
% 0.04/0.35 fof(f62,plain,(
% 0.04/0.35 ![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.04/0.35 inference(pre_NNF_transformation,[status(thm)],[f6])).
% 0.04/0.35 fof(f63,plain,(
% 0.04/0.35 ![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.04/0.35 inference(NNF_transformation,[status(thm)],[f62])).
% 0.04/0.35 fof(f64,plain,(
% 0.04/0.35 ![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.04/0.35 inference(cnf_transformation,[status(thm)],[f63])).
% 0.04/0.35 fof(f65,plain,(
% 0.04/0.35 ![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.04/0.35 inference(cnf_transformation,[status(thm)],[f63])).
% 0.04/0.35 fof(f74,plain,(
% 0.04/0.35 ![A]: (~rel_str(A)|(![B]: (~subrelstr(B,A)|rel_str(B))))),
% 0.04/0.35 inference(pre_NNF_transformation,[status(thm)],[f17])).
% 0.04/0.35 fof(f75,plain,(
% 0.04/0.35 ![X0,X1]: (~rel_str(X0)|~subrelstr(X1,X0)|rel_str(X1))),
% 0.04/0.35 inference(cnf_transformation,[status(thm)],[f74])).
% 0.04/0.35 fof(f76,plain,(
% 0.04/0.35 ![A,B,C]: (~relation_of2_as_subset(C,A,B)|element(C,powerset(cartesian_product2(A,B))))),
% 0.04/0.35 inference(pre_NNF_transformation,[status(thm)],[f18])).
% 0.04/0.35 fof(f77,plain,(
% 0.04/0.35 ![X0,X1,X2]: (~relation_of2_as_subset(X0,X1,X2)|element(X0,powerset(cartesian_product2(X1,X2))))),
% 0.04/0.35 inference(cnf_transformation,[status(thm)],[f76])).
% 0.04/0.35 fof(f78,plain,(
% 0.04/0.35 ![A]: (~rel_str(A)|relation_of2_as_subset(the_InternalRel(A),the_carrier(A),the_carrier(A)))),
% 0.04/0.35 inference(pre_NNF_transformation,[status(thm)],[f19])).
% 0.04/0.35 fof(f79,plain,(
% 0.04/0.35 ![X0]: (~rel_str(X0)|relation_of2_as_subset(the_InternalRel(X0),the_carrier(X0),the_carrier(X0)))),
% 0.04/0.35 inference(cnf_transformation,[status(thm)],[f78])).
% 0.04/0.35 fof(f113,plain,(
% 0.04/0.35 ![A,B]: (~relation(A)|relation_restriction_as_relation_of(A,B)=relation_restriction(A,B))),
% 0.04/0.35 inference(pre_NNF_transformation,[status(thm)],[f34])).
% 0.04/0.35 fof(f114,plain,(
% 0.04/0.35 ![A]: (~relation(A)|(![B]: relation_restriction_as_relation_of(A,B)=relation_restriction(A,B)))),
% 0.04/0.35 inference(miniscoping,[status(thm)],[f113])).
% 0.04/0.35 fof(f115,plain,(
% 0.04/0.35 ![X0,X1]: (~relation(X0)|relation_restriction_as_relation_of(X0,X1)=relation_restriction(X0,X1))),
% 0.04/0.35 inference(cnf_transformation,[status(thm)],[f114])).
% 0.04/0.35 fof(f122,plain,(
% 0.04/0.35 ![A,B,C,D]: ((~in(ordered_pair(A,B),cartesian_product2(C,D))|(in(A,C)&in(B,D)))&(in(ordered_pair(A,B),cartesian_product2(C,D))|(~in(A,C)|~in(B,D))))),
% 0.04/0.35 inference(NNF_transformation,[status(thm)],[f37])).
% 0.04/0.35 fof(f123,plain,(
% 0.04/0.35 (![A,B,C,D]: (~in(ordered_pair(A,B),cartesian_product2(C,D))|(in(A,C)&in(B,D))))&(![A,B,C,D]: (in(ordered_pair(A,B),cartesian_product2(C,D))|(~in(A,C)|~in(B,D))))),
% 0.04/0.35 inference(miniscoping,[status(thm)],[f122])).
% 0.04/0.35 fof(f126,plain,(
% 0.04/0.35 ![X0,X1,X2,X3]: (in(ordered_pair(X0,X1),cartesian_product2(X2,X3))|~in(X0,X2)|~in(X1,X3))),
% 0.04/0.35 inference(cnf_transformation,[status(thm)],[f123])).
% 0.04/0.35 fof(f127,plain,(
% 0.04/0.35 ![A,B,C]: (~relation(C)|(in(A,relation_restriction(C,B))<=>(in(A,C)&in(A,cartesian_product2(B,B)))))),
% 0.04/0.35 inference(pre_NNF_transformation,[status(thm)],[f38])).
% 0.04/0.35 fof(f128,plain,(
% 0.04/0.35 ![A,B,C]: (~relation(C)|((~in(A,relation_restriction(C,B))|(in(A,C)&in(A,cartesian_product2(B,B))))&(in(A,relation_restriction(C,B))|(~in(A,C)|~in(A,cartesian_product2(B,B))))))),
% 0.04/0.35 inference(NNF_transformation,[status(thm)],[f127])).
% 0.04/0.35 fof(f129,plain,(
% 0.04/0.35 ![C]: (~relation(C)|((![A,B]: (~in(A,relation_restriction(C,B))|(in(A,C)&in(A,cartesian_product2(B,B)))))&(![A,B]: (in(A,relation_restriction(C,B))|(~in(A,C)|~in(A,cartesian_product2(B,B)))))))),
% 0.04/0.35 inference(miniscoping,[status(thm)],[f128])).
% 0.04/0.35 fof(f132,plain,(
% 0.04/0.35 ![X0,X1,X2]: (~relation(X0)|in(X1,relation_restriction(X0,X2))|~in(X1,X0)|~in(X1,cartesian_product2(X2,X2)))),
% 0.04/0.35 inference(cnf_transformation,[status(thm)],[f129])).
% 0.04/0.35 fof(f147,plain,(
% 0.04/0.35 (?[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))))))))))))))),
% 0.04/0.35 inference(pre_NNF_transformation,[status(thm)],[f45])).
% 0.04/0.35 fof(f148,plain,(
% 0.04/0.35 (rel_str(sK11_skl)&((full_subrelstr(sK12_skl,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(sK11_skl,sK13_skl,sK14_skl))&in(sK15_skl,the_carrier(sK12_skl)))&in(sK16_skl,the_carrier(sK12_skl)))&~related(sK12_skl,sK15_skl,sK16_skl))))))))),
% 0.04/0.35 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)],[f147])).
% 0.04/0.35 fof(f149,plain,(
% 0.04/0.35 rel_str(sK11_skl)),
% 0.04/0.35 inference(cnf_transformation,[status(thm)],[f148])).
% 0.04/0.35 fof(f150,plain,(
% 0.04/0.35 full_subrelstr(sK12_skl,sK11_skl)),
% 0.04/0.35 inference(cnf_transformation,[status(thm)],[f148])).
% 0.04/0.35 fof(f151,plain,(
% 0.04/0.35 subrelstr(sK12_skl,sK11_skl)),
% 0.04/0.35 inference(cnf_transformation,[status(thm)],[f148])).
% 0.04/0.35 fof(f152,plain,(
% 0.04/0.35 element(sK13_skl,the_carrier(sK11_skl))),
% 0.04/0.35 inference(cnf_transformation,[status(thm)],[f148])).
% 0.04/0.35 fof(f153,plain,(
% 0.04/0.35 element(sK14_skl,the_carrier(sK11_skl))),
% 0.04/0.35 inference(cnf_transformation,[status(thm)],[f148])).
% 0.04/0.35 fof(f154,plain,(
% 0.04/0.35 element(sK15_skl,the_carrier(sK12_skl))),
% 0.04/0.35 inference(cnf_transformation,[status(thm)],[f148])).
% 0.04/0.35 fof(f155,plain,(
% 0.04/0.35 element(sK16_skl,the_carrier(sK12_skl))),
% 0.04/0.35 inference(cnf_transformation,[status(thm)],[f148])).
% 0.04/0.35 fof(f156,plain,(
% 0.04/0.35 sK15_skl=sK13_skl),
% 0.04/0.35 inference(cnf_transformation,[status(thm)],[f148])).
% 0.04/0.35 fof(f157,plain,(
% 0.04/0.35 sK16_skl=sK14_skl),
% 0.04/0.35 inference(cnf_transformation,[status(thm)],[f148])).
% 0.04/0.35 fof(f158,plain,(
% 0.04/0.35 related(sK11_skl,sK13_skl,sK14_skl)),
% 0.04/0.35 inference(cnf_transformation,[status(thm)],[f148])).
% 0.04/0.35 fof(f159,plain,(
% 0.04/0.35 in(sK15_skl,the_carrier(sK12_skl))),
% 0.04/0.35 inference(cnf_transformation,[status(thm)],[f148])).
% 0.04/0.35 fof(f160,plain,(
% 0.04/0.35 in(sK16_skl,the_carrier(sK12_skl))),
% 0.04/0.35 inference(cnf_transformation,[status(thm)],[f148])).
% 0.04/0.35 fof(f161,plain,(
% 0.04/0.35 ~related(sK12_skl,sK15_skl,sK16_skl)),
% 0.04/0.35 inference(cnf_transformation,[status(thm)],[f148])).
% 0.04/0.35 fof(f170,plain,(
% 0.04/0.35 element(sK13_skl,the_carrier(sK12_skl))),
% 0.04/0.35 inference(backward_demodulation,[status(thm)],[f156,f154])).
% 0.04/0.35 fof(f171,plain,(
% 0.04/0.35 element(sK14_skl,the_carrier(sK12_skl))),
% 0.04/0.35 inference(backward_demodulation,[status(thm)],[f157,f155])).
% 0.04/0.35 fof(f172,plain,(
% 0.04/0.35 in(sK13_skl,the_carrier(sK12_skl))),
% 0.04/0.35 inference(forward_demodulation,[status(thm)],[f156,f159])).
% 0.04/0.35 fof(f173,plain,(
% 0.04/0.35 in(sK14_skl,the_carrier(sK12_skl))),
% 0.04/0.35 inference(forward_demodulation,[status(thm)],[f157,f160])).
% 0.04/0.35 fof(f174,plain,(
% 0.04/0.35 ~related(sK12_skl,sK13_skl,sK16_skl)),
% 0.04/0.35 inference(forward_demodulation,[status(thm)],[f156,f161])).
% 0.04/0.35 fof(f175,plain,(
% 0.04/0.35 ~related(sK12_skl,sK13_skl,sK14_skl)),
% 0.04/0.35 inference(forward_demodulation,[status(thm)],[f157,f174])).
% 0.04/0.35 fof(f180,plain,(
% 0.04/0.35 ![X0]: (~subrelstr(X0,sK11_skl)|~full_subrelstr(X0,sK11_skl)|the_InternalRel(X0)=relation_restriction_as_relation_of(the_InternalRel(sK11_skl),the_carrier(X0)))),
% 0.04/0.35 inference(resolution,[status(thm)],[f60,f149])).
% 0.04/0.35 fof(f186,plain,(
% 0.04/0.35 ~rel_str(sK11_skl)|~element(sK13_skl,the_carrier(sK11_skl))|~element(sK14_skl,the_carrier(sK11_skl))|in(ordered_pair(sK13_skl,sK14_skl),the_InternalRel(sK11_skl))),
% 0.04/0.35 inference(resolution,[status(thm)],[f64,f158])).
% 0.04/0.35 fof(f187,definition,(
% 0.04/0.35 sQ0_spl <=> (rel_str(sK11_skl))),
% 0.04/0.35 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.04/0.35 fof(f189,plain,(
% 0.04/0.35 ~rel_str(sK11_skl)|sQ0_spl),
% 0.04/0.35 inference(component_clause,[status(thm)],[f187])).
% 0.04/0.35 fof(f190,definition,(
% 0.04/0.35 sQ1_spl <=> (element(sK13_skl,the_carrier(sK11_skl)))),
% 0.04/0.35 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.04/0.35 fof(f192,plain,(
% 0.04/0.35 ~element(sK13_skl,the_carrier(sK11_skl))|sQ1_spl),
% 0.04/0.35 inference(component_clause,[status(thm)],[f190])).
% 0.04/0.35 fof(f193,definition,(
% 0.04/0.35 sQ2_spl <=> (element(sK14_skl,the_carrier(sK11_skl)))),
% 0.04/0.35 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.04/0.35 fof(f195,plain,(
% 0.04/0.35 ~element(sK14_skl,the_carrier(sK11_skl))|sQ2_spl),
% 0.04/0.35 inference(component_clause,[status(thm)],[f193])).
% 0.04/0.35 fof(f196,definition,(
% 0.04/0.35 sQ3_spl <=> (in(ordered_pair(sK13_skl,sK14_skl),the_InternalRel(sK11_skl)))),
% 0.04/0.35 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.04/0.35 fof(f197,plain,(
% 0.04/0.35 in(ordered_pair(sK13_skl,sK14_skl),the_InternalRel(sK11_skl))|~sQ3_spl),
% 0.04/0.35 inference(component_clause,[status(thm)],[f196])).
% 0.04/0.35 fof(f199,plain,(
% 0.04/0.35 ~sQ0_spl|~sQ1_spl|~sQ2_spl|sQ3_spl),
% 0.04/0.35 inference(split_clause,[status(thm)],[f186,f187,f190,f193,f196])).
% 0.04/0.35 fof(f200,plain,(
% 0.04/0.35 ~rel_str(sK11_skl)|rel_str(sK12_skl)),
% 0.04/0.35 inference(resolution,[status(thm)],[f75,f151])).
% 0.04/0.35 fof(f201,definition,(
% 0.04/0.35 sQ4_spl <=> (rel_str(sK12_skl))),
% 0.04/0.35 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.04/0.35 fof(f204,plain,(
% 0.04/0.35 ~sQ0_spl|sQ4_spl),
% 0.04/0.35 inference(split_clause,[status(thm)],[f200,f187,f201])).
% 0.04/0.35 fof(f205,plain,(
% 0.04/0.35 $false|sQ0_spl),
% 0.04/0.35 inference(forward_subsumption_resolution,[status(thm)],[f189,f149])).
% 0.04/0.35 fof(f206,plain,(
% 0.04/0.35 sQ0_spl),
% 0.04/0.35 inference(contradiction_clause,[status(thm)],[f205])).
% 0.04/0.35 fof(f215,definition,(
% 0.04/0.35 sQ6_spl <=> (the_InternalRel(sK12_skl)=relation_restriction_as_relation_of(the_InternalRel(sK11_skl),the_carrier(sK12_skl)))),
% 0.04/0.35 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.04/0.35 fof(f216,plain,(
% 0.04/0.35 the_InternalRel(sK12_skl)=relation_restriction_as_relation_of(the_InternalRel(sK11_skl),the_carrier(sK12_skl))|~sQ6_spl),
% 0.04/0.35 inference(component_clause,[status(thm)],[f215])).
% 0.04/0.35 fof(f223,definition,(
% 0.04/0.35 sQ7_spl <=> (subrelstr(sK12_skl,sK11_skl))),
% 0.04/0.35 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.04/0.35 fof(f225,plain,(
% 0.04/0.35 ~subrelstr(sK12_skl,sK11_skl)|sQ7_spl),
% 0.04/0.35 inference(component_clause,[status(thm)],[f223])).
% 0.04/0.35 fof(f231,plain,(
% 0.04/0.35 $false|sQ7_spl),
% 0.04/0.35 inference(forward_subsumption_resolution,[status(thm)],[f225,f151])).
% 0.04/0.35 fof(f232,plain,(
% 0.04/0.35 sQ7_spl),
% 0.04/0.35 inference(contradiction_clause,[status(thm)],[f231])).
% 0.04/0.35 fof(f238,plain,(
% 0.04/0.35 $false|sQ2_spl),
% 0.04/0.35 inference(forward_subsumption_resolution,[status(thm)],[f195,f153])).
% 0.04/0.35 fof(f239,plain,(
% 0.04/0.35 sQ2_spl),
% 0.04/0.35 inference(contradiction_clause,[status(thm)],[f238])).
% 0.04/0.35 fof(f240,plain,(
% 0.04/0.35 $false|sQ1_spl),
% 0.04/0.35 inference(forward_subsumption_resolution,[status(thm)],[f192,f152])).
% 0.04/0.35 fof(f241,plain,(
% 0.04/0.35 sQ1_spl),
% 0.04/0.35 inference(contradiction_clause,[status(thm)],[f240])).
% 0.04/0.35 fof(f254,plain,(
% 0.04/0.35 ![X0]: (~rel_str(X0)|element(the_InternalRel(X0),powerset(cartesian_product2(the_carrier(X0),the_carrier(X0)))))),
% 0.04/0.35 inference(resolution,[status(thm)],[f79,f77])).
% 0.04/0.35 fof(f651,plain,(
% 0.04/0.35 ![X0,X1,X2,X3]: (~relation(X0)|in(ordered_pair(X1,X2),relation_restriction(X0,X3))|~in(ordered_pair(X1,X2),X0)|~in(X1,X3)|~in(X2,X3))),
% 0.04/0.35 inference(resolution,[status(thm)],[f132,f126])).
% 0.04/0.35 fof(f736,plain,(
% 0.04/0.35 ![X0]: (~rel_str(X0)|relation(the_InternalRel(X0)))),
% 0.04/0.35 inference(resolution,[status(thm)],[f254,f55])).
% 0.04/0.35 fof(f824,plain,(
% 0.04/0.35 ~subrelstr(sK12_skl,sK11_skl)|the_InternalRel(sK12_skl)=relation_restriction_as_relation_of(the_InternalRel(sK11_skl),the_carrier(sK12_skl))),
% 0.04/0.35 inference(resolution,[status(thm)],[f180,f150])).
% 0.04/0.35 fof(f825,plain,(
% 0.04/0.35 ~sQ7_spl|sQ6_spl),
% 0.04/0.35 inference(split_clause,[status(thm)],[f824,f223,f215])).
% 0.04/0.35 fof(f987,plain,(
% 0.04/0.35 ![X0]: (~relation(the_InternalRel(sK11_skl))|in(ordered_pair(sK13_skl,sK14_skl),relation_restriction(the_InternalRel(sK11_skl),X0))|~in(sK13_skl,X0)|~in(sK14_skl,X0)|~sQ3_spl)),
% 0.04/0.35 inference(resolution,[status(thm)],[f651,f197])).
% 0.04/0.35 fof(f990,definition,(
% 0.04/0.35 sQ62_spl <=> (relation(the_InternalRel(sK11_skl)))),
% 0.04/0.35 introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition])).
% 0.04/0.35 fof(f991,plain,(
% 0.04/0.35 relation(the_InternalRel(sK11_skl))|~sQ62_spl),
% 0.04/0.35 inference(component_clause,[status(thm)],[f990])).
% 0.04/0.35 fof(f992,plain,(
% 0.04/0.35 ~relation(the_InternalRel(sK11_skl))|sQ62_spl),
% 0.04/0.35 inference(component_clause,[status(thm)],[f990])).
% 0.04/0.35 fof(f993,definition,(
% 0.04/0.35 ![X0]: (sQ63_spl <=> (in(ordered_pair(sK13_skl,sK14_skl),relation_restriction(the_InternalRel(sK11_skl),X0))|~in(sK13_skl,X0)|~in(sK14_skl,X0)))),
% 0.04/0.35 introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition])).
% 0.04/0.35 fof(f994,plain,(
% 0.04/0.35 ![X0]: (in(ordered_pair(sK13_skl,sK14_skl),relation_restriction(the_InternalRel(sK11_skl),X0))|~in(sK13_skl,X0)|~in(sK14_skl,X0)|~sQ63_spl)),
% 0.04/0.35 inference(component_clause,[status(thm)],[f993])).
% 0.04/0.35 fof(f996,plain,(
% 0.04/0.35 ~sQ62_spl|sQ63_spl|~sQ3_spl),
% 0.04/0.35 inference(split_clause,[status(thm)],[f987,f990,f993,f196])).
% 0.04/0.35 fof(f1026,plain,(
% 0.04/0.35 ~rel_str(sK11_skl)|sQ62_spl),
% 0.04/0.35 inference(resolution,[status(thm)],[f992,f736])).
% 0.04/0.35 fof(f1027,plain,(
% 0.04/0.35 ~sQ0_spl|sQ62_spl),
% 0.04/0.35 inference(split_clause,[status(thm)],[f1026,f187,f990])).
% 0.04/0.35 fof(f1028,plain,(
% 0.04/0.35 in(ordered_pair(sK13_skl,sK14_skl),relation_restriction(the_InternalRel(sK11_skl),the_carrier(sK12_skl)))|~in(sK13_skl,the_carrier(sK12_skl))|~sQ63_spl),
% 0.04/0.35 inference(resolution,[status(thm)],[f994,f173])).
% 0.04/0.35 fof(f1030,definition,(
% 0.04/0.35 sQ67_spl <=> (in(ordered_pair(sK13_skl,sK14_skl),relation_restriction(the_InternalRel(sK11_skl),the_carrier(sK12_skl))))),
% 0.04/0.35 introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition])).
% 0.04/0.35 fof(f1031,plain,(
% 0.04/0.35 in(ordered_pair(sK13_skl,sK14_skl),relation_restriction(the_InternalRel(sK11_skl),the_carrier(sK12_skl)))|~sQ67_spl),
% 0.04/0.35 inference(component_clause,[status(thm)],[f1030])).
% 0.04/0.35 fof(f1033,definition,(
% 0.04/0.35 sQ68_spl <=> (in(sK13_skl,the_carrier(sK12_skl)))),
% 0.04/0.35 introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition])).
% 0.04/0.35 fof(f1035,plain,(
% 0.04/0.35 ~in(sK13_skl,the_carrier(sK12_skl))|sQ68_spl),
% 0.04/0.35 inference(component_clause,[status(thm)],[f1033])).
% 0.04/0.35 fof(f1036,plain,(
% 0.04/0.35 sQ67_spl|~sQ68_spl|~sQ63_spl),
% 0.04/0.35 inference(split_clause,[status(thm)],[f1028,f1030,f1033,f993])).
% 0.04/0.35 fof(f1038,plain,(
% 0.04/0.35 ![X0]: (relation_restriction_as_relation_of(the_InternalRel(sK11_skl),X0)=relation_restriction(the_InternalRel(sK11_skl),X0)|~sQ62_spl)),
% 0.04/0.35 inference(resolution,[status(thm)],[f991,f115])).
% 0.04/0.35 fof(f1042,plain,(
% 0.04/0.35 in(ordered_pair(sK13_skl,sK14_skl),relation_restriction_as_relation_of(the_InternalRel(sK11_skl),the_carrier(sK12_skl)))|~sQ62_spl|~sQ67_spl),
% 0.04/0.35 inference(backward_demodulation,[status(thm)],[f1038,f1031])).
% 0.04/0.35 fof(f1045,plain,(
% 0.04/0.35 in(ordered_pair(sK13_skl,sK14_skl),the_InternalRel(sK12_skl))|~sQ6_spl|~sQ62_spl|~sQ67_spl),
% 0.04/0.35 inference(forward_demodulation,[status(thm)],[f216,f1042])).
% 0.04/0.35 fof(f1072,plain,(
% 0.04/0.35 $false|sQ68_spl),
% 0.04/0.35 inference(forward_subsumption_resolution,[status(thm)],[f1035,f172])).
% 0.04/0.35 fof(f1073,plain,(
% 0.04/0.35 sQ68_spl),
% 0.04/0.35 inference(contradiction_clause,[status(thm)],[f1072])).
% 0.04/0.35 fof(f1091,plain,(
% 0.04/0.35 ~rel_str(sK12_skl)|~element(sK13_skl,the_carrier(sK12_skl))|~element(sK14_skl,the_carrier(sK12_skl))|related(sK12_skl,sK13_skl,sK14_skl)|~sQ6_spl|~sQ62_spl|~sQ67_spl),
% 0.04/0.35 inference(resolution,[status(thm)],[f1045,f65])).
% 0.04/0.35 fof(f1096,definition,(
% 0.04/0.35 sQ70_spl <=> (element(sK13_skl,the_carrier(sK12_skl)))),
% 0.04/0.35 introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition])).
% 0.04/0.35 fof(f1098,plain,(
% 0.04/0.35 ~element(sK13_skl,the_carrier(sK12_skl))|sQ70_spl),
% 0.04/0.35 inference(component_clause,[status(thm)],[f1096])).
% 0.04/0.35 fof(f1099,definition,(
% 0.04/0.35 sQ71_spl <=> (element(sK14_skl,the_carrier(sK12_skl)))),
% 0.04/0.35 introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition])).
% 0.04/0.35 fof(f1101,plain,(
% 0.04/0.35 ~element(sK14_skl,the_carrier(sK12_skl))|sQ71_spl),
% 0.04/0.35 inference(component_clause,[status(thm)],[f1099])).
% 0.04/0.35 fof(f1102,definition,(
% 0.04/0.35 sQ72_spl <=> (related(sK12_skl,sK13_skl,sK14_skl))),
% 0.04/0.35 introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition])).
% 0.04/0.35 fof(f1103,plain,(
% 0.04/0.35 related(sK12_skl,sK13_skl,sK14_skl)|~sQ72_spl),
% 0.04/0.35 inference(component_clause,[status(thm)],[f1102])).
% 0.04/0.35 fof(f1105,plain,(
% 0.04/0.35 ~sQ4_spl|~sQ70_spl|~sQ71_spl|sQ72_spl|~sQ6_spl|~sQ62_spl|~sQ67_spl),
% 0.04/0.35 inference(split_clause,[status(thm)],[f1091,f201,f1096,f1099,f1102,f215,f990,f1030])).
% 0.04/0.35 fof(f1120,plain,(
% 0.04/0.35 $false|~sQ72_spl),
% 0.04/0.35 inference(forward_subsumption_resolution,[status(thm)],[f1103,f175])).
% 0.04/0.35 fof(f1121,plain,(
% 0.04/0.35 ~sQ72_spl),
% 0.04/0.35 inference(contradiction_clause,[status(thm)],[f1120])).
% 0.04/0.35 fof(f1122,plain,(
% 0.04/0.35 $false|sQ70_spl),
% 0.04/0.35 inference(forward_subsumption_resolution,[status(thm)],[f1098,f170])).
% 0.04/0.36 fof(f1123,plain,(
% 0.04/0.36 sQ70_spl),
% 0.04/0.36 inference(contradiction_clause,[status(thm)],[f1122])).
% 0.04/0.36 fof(f1124,plain,(
% 0.04/0.36 $false|sQ71_spl),
% 0.04/0.36 inference(forward_subsumption_resolution,[status(thm)],[f1101,f171])).
% 0.04/0.36 fof(f1125,plain,(
% 0.04/0.36 sQ71_spl),
% 0.04/0.36 inference(contradiction_clause,[status(thm)],[f1124])).
% 0.04/0.36 fof(f1126,plain,(
% 0.04/0.36 $false),
% 0.04/0.36 inference(sat_refutation,[status(thm)],[f199,f204,f206,f232,f239,f241,f825,f996,f1027,f1036,f1073,f1105,f1121,f1123,f1125])).
% 0.04/0.36 % SZS output end CNFRefutation for theBenchmark.p
% 0.44/0.38 % Elapsed time: 0.066478 seconds
% 0.44/0.38 % CPU time: 0.403227 seconds
% 0.44/0.38 % Total memory used: 113.611 MB
% 0.44/0.38 % Net memory used: 112.390 MB
%------------------------------------------------------------------------------