%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU339+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 : n019.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:22 PM UTC 2026
% Result : Theorem 0.08s 0.37s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU339+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.34 % Computer : n019.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/0.34 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 06:13:21 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.36 % Drodi V4.1.1
% 0.08/0.37 % Refutation found
% 0.08/0.37 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.08/0.37 % SZS output start CNFRefutation for theBenchmark
% 0.08/0.37 fof(f1,axiom,(
% 0.08/0.37 (! [A,B] :( in(A,B)=> ~ in(B,A) ) )),
% 0.08/0.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.37 fof(f2,axiom,(
% 0.08/0.37 (! [A,B,C] :( element(C,powerset(cartesian_product2(A,B)))=> relation(C) ) )),
% 0.08/0.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.37 fof(f4,axiom,(
% 0.08/0.37 (! [A] :( relation(A)=> (! [B] :( is_antisymmetric_in(A,B)<=> (! [C,D] :( ( in(C,B)& in(D,B)& in(ordered_pair(C,D),A)& in(ordered_pair(D,C),A) )=> C = D ) )) )) )),
% 0.08/0.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.37 fof(f6,axiom,(
% 0.08/0.37 (! [A] :( rel_str(A)=> ( antisymmetric_relstr(A)<=> is_antisymmetric_in(the_InternalRel(A),the_carrier(A)) ) ) )),
% 0.08/0.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.37 fof(f7,axiom,(
% 0.08/0.37 (! [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.08/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.38 fof(f18,axiom,(
% 0.08/0.38 (! [A,B,C] :( relation_of2_as_subset(C,A,B)=> element(C,powerset(cartesian_product2(A,B))) ) )),
% 0.08/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.38 fof(f19,axiom,(
% 0.08/0.38 (! [A] :( rel_str(A)=> relation_of2_as_subset(the_InternalRel(A),the_carrier(A),the_carrier(A)) ) )),
% 0.08/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.38 fof(f24,axiom,(
% 0.08/0.38 (! [A] :(? [B] : element(B,A) ))),
% 0.08/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.38 fof(f26,axiom,(
% 0.08/0.38 (! [A] : ~ empty(powerset(A)) )),
% 0.08/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.38 fof(f32,axiom,(
% 0.08/0.38 (? [A] : empty(A) )),
% 0.08/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.38 fof(f37,axiom,(
% 0.08/0.38 (! [A,B,C,D] :( in(ordered_pair(A,B),cartesian_product2(C,D))<=> ( in(A,C)& in(B,D) ) ) )),
% 0.08/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.38 fof(f39,conjecture,(
% 0.08/0.38 (! [A] :( ( antisymmetric_relstr(A)& rel_str(A) )=> (! [B] :( element(B,the_carrier(A))=> (! [C] :( element(C,the_carrier(A))=> ( ( related(A,B,C)& related(A,C,B) )=> B = C ) ) )) )) )),
% 0.08/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.38 fof(f40,negated_conjecture,(
% 0.08/0.38 ~((! [A] :( ( antisymmetric_relstr(A)& rel_str(A) )=> (! [B] :( element(B,the_carrier(A))=> (! [C] :( element(C,the_carrier(A))=> ( ( related(A,B,C)& related(A,C,B) )=> B = C ) ) )) )) ))),
% 0.08/0.38 inference(negated_conjecture,[status(cth)],[f39])).
% 0.08/0.38 fof(f41,axiom,(
% 0.08/0.38 (! [A,B] :( element(A,B)=> ( empty(B)| in(A,B) ) ) )),
% 0.08/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.38 fof(f43,axiom,(
% 0.08/0.38 (! [A,B,C] :( ( in(A,B)& element(B,powerset(C)) )=> element(A,C) ) )),
% 0.08/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.38 fof(f44,axiom,(
% 0.08/0.38 (! [A,B,C] :~ ( in(A,B)& element(B,powerset(C))& empty(C) ) )),
% 0.08/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.38 fof(f45,axiom,(
% 0.08/0.38 (! [A] :( empty(A)=> A = empty_set ) )),
% 0.08/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.38 fof(f46,axiom,(
% 0.08/0.38 (! [A,B] :~ ( in(A,B)& empty(B) ) )),
% 0.08/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.38 fof(f48,plain,(
% 0.08/0.38 ![A,B]: (~in(A,B)|~in(B,A))),
% 0.08/0.38 inference(pre_NNF_transformation,[status(thm)],[f1])).
% 0.08/0.38 fof(f49,plain,(
% 0.08/0.38 ![X0,X1]: (~in(X0,X1)|~in(X1,X0))),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f48])).
% 0.08/0.38 fof(f50,plain,(
% 0.08/0.38 ![A,B,C]: (~element(C,powerset(cartesian_product2(A,B)))|relation(C))),
% 0.08/0.38 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.08/0.38 fof(f51,plain,(
% 0.08/0.38 ![C]: ((![A,B]: ~element(C,powerset(cartesian_product2(A,B))))|relation(C))),
% 0.08/0.38 inference(miniscoping,[status(thm)],[f50])).
% 0.08/0.38 fof(f52,plain,(
% 0.08/0.38 ![X0,X1,X2]: (~element(X0,powerset(cartesian_product2(X1,X2)))|relation(X0))),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f51])).
% 0.08/0.38 fof(f54,plain,(
% 0.08/0.38 ![A]: (~relation(A)|(![B]: (is_antisymmetric_in(A,B)<=>(![C,D]: ((((~in(C,B)|~in(D,B))|~in(ordered_pair(C,D),A))|~in(ordered_pair(D,C),A))|C=D)))))),
% 0.08/0.38 inference(pre_NNF_transformation,[status(thm)],[f4])).
% 0.08/0.38 fof(f55,plain,(
% 0.08/0.38 ![A]: (~relation(A)|(![B]: ((~is_antisymmetric_in(A,B)|(![C,D]: ((((~in(C,B)|~in(D,B))|~in(ordered_pair(C,D),A))|~in(ordered_pair(D,C),A))|C=D)))&(is_antisymmetric_in(A,B)|(?[C,D]: ((((in(C,B)&in(D,B))&in(ordered_pair(C,D),A))&in(ordered_pair(D,C),A))&~C=D))))))),
% 0.08/0.38 inference(NNF_transformation,[status(thm)],[f54])).
% 0.08/0.38 fof(f56,plain,(
% 0.08/0.38 ![A]: (~relation(A)|((![B]: (~is_antisymmetric_in(A,B)|(![C,D]: ((((~in(C,B)|~in(D,B))|~in(ordered_pair(C,D),A))|~in(ordered_pair(D,C),A))|C=D))))&(![B]: (is_antisymmetric_in(A,B)|(?[C,D]: ((((in(C,B)&in(D,B))&in(ordered_pair(C,D),A))&in(ordered_pair(D,C),A))&~C=D))))))),
% 0.08/0.38 inference(miniscoping,[status(thm)],[f55])).
% 0.08/0.38 fof(f57,plain,(
% 0.08/0.38 ![A]: (~relation(A)|((![B]: (~is_antisymmetric_in(A,B)|(![C,D]: ((((~in(C,B)|~in(D,B))|~in(ordered_pair(C,D),A))|~in(ordered_pair(D,C),A))|C=D))))&(![B]: (is_antisymmetric_in(A,B)|((((in(sK0_skl(B,A),B)&in(sK1_skl(B,A),B))&in(ordered_pair(sK0_skl(B,A),sK1_skl(B,A)),A))&in(ordered_pair(sK1_skl(B,A),sK0_skl(B,A)),A))&~sK0_skl(B,A)=sK1_skl(B,A))))))),
% 0.08/0.38 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(C,sK0_skl(B,A)),skolemize(D,sK1_skl(B,A))],[f56])).
% 0.08/0.38 fof(f58,plain,(
% 0.08/0.38 ![X0,X1,X2,X3]: (~relation(X0)|~is_antisymmetric_in(X0,X1)|~in(X2,X1)|~in(X3,X1)|~in(ordered_pair(X2,X3),X0)|~in(ordered_pair(X3,X2),X0)|X2=X3)),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f57])).
% 0.08/0.38 fof(f65,plain,(
% 0.08/0.38 ![A]: (~rel_str(A)|(antisymmetric_relstr(A)<=>is_antisymmetric_in(the_InternalRel(A),the_carrier(A))))),
% 0.08/0.38 inference(pre_NNF_transformation,[status(thm)],[f6])).
% 0.08/0.38 fof(f66,plain,(
% 0.08/0.38 ![A]: (~rel_str(A)|((~antisymmetric_relstr(A)|is_antisymmetric_in(the_InternalRel(A),the_carrier(A)))&(antisymmetric_relstr(A)|~is_antisymmetric_in(the_InternalRel(A),the_carrier(A)))))),
% 0.08/0.38 inference(NNF_transformation,[status(thm)],[f65])).
% 0.08/0.38 fof(f67,plain,(
% 0.08/0.38 ![X0]: (~rel_str(X0)|~antisymmetric_relstr(X0)|is_antisymmetric_in(the_InternalRel(X0),the_carrier(X0)))),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f66])).
% 0.08/0.38 fof(f69,plain,(
% 0.08/0.38 ![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.08/0.38 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 0.08/0.38 fof(f70,plain,(
% 0.08/0.38 ![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.08/0.38 inference(NNF_transformation,[status(thm)],[f69])).
% 0.08/0.38 fof(f71,plain,(
% 0.08/0.38 ![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.08/0.38 inference(cnf_transformation,[status(thm)],[f70])).
% 0.08/0.38 fof(f75,plain,(
% 0.08/0.38 ![A,B,C]: (~relation_of2_as_subset(C,A,B)|element(C,powerset(cartesian_product2(A,B))))),
% 0.08/0.38 inference(pre_NNF_transformation,[status(thm)],[f18])).
% 0.08/0.38 fof(f76,plain,(
% 0.08/0.38 ![X0,X1,X2]: (~relation_of2_as_subset(X0,X1,X2)|element(X0,powerset(cartesian_product2(X1,X2))))),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f75])).
% 0.08/0.38 fof(f77,plain,(
% 0.08/0.38 ![A]: (~rel_str(A)|relation_of2_as_subset(the_InternalRel(A),the_carrier(A),the_carrier(A)))),
% 0.08/0.38 inference(pre_NNF_transformation,[status(thm)],[f19])).
% 0.08/0.38 fof(f78,plain,(
% 0.08/0.38 ![X0]: (~rel_str(X0)|relation_of2_as_subset(the_InternalRel(X0),the_carrier(X0),the_carrier(X0)))),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f77])).
% 0.08/0.38 fof(f85,plain,(
% 0.08/0.38 ![A]: element(sK5_skl(A),A)),
% 0.08/0.38 inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl]),skolemize(B,sK5_skl(A))],[f24])).
% 0.08/0.38 fof(f86,plain,(
% 0.08/0.38 ![X0]: (element(sK5_skl(X0),X0))),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f85])).
% 0.08/0.38 fof(f89,plain,(
% 0.08/0.38 ![X0]: (~empty(powerset(X0)))),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f26])).
% 0.08/0.38 fof(f99,plain,(
% 0.08/0.38 empty(sK8_skl)),
% 0.08/0.38 inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl]),skolemize(A,sK8_skl)],[f32])).
% 0.08/0.38 fof(f100,plain,(
% 0.08/0.38 empty(sK8_skl)),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f99])).
% 0.08/0.38 fof(f112,plain,(
% 0.08/0.38 ![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.08/0.38 inference(NNF_transformation,[status(thm)],[f37])).
% 0.08/0.38 fof(f113,plain,(
% 0.08/0.38 (![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.08/0.38 inference(miniscoping,[status(thm)],[f112])).
% 0.08/0.38 fof(f115,plain,(
% 0.08/0.38 ![X0,X1,X2,X3]: (~in(ordered_pair(X0,X1),cartesian_product2(X2,X3))|in(X1,X3))),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f113])).
% 0.08/0.38 fof(f119,plain,(
% 0.08/0.38 (?[A]: ((antisymmetric_relstr(A)&rel_str(A))&(?[B]: (element(B,the_carrier(A))&(?[C]: (element(C,the_carrier(A))&((related(A,B,C)&related(A,C,B))&~B=C)))))))),
% 0.08/0.38 inference(pre_NNF_transformation,[status(thm)],[f40])).
% 0.08/0.38 fof(f120,plain,(
% 0.08/0.38 ((antisymmetric_relstr(sK11_skl)&rel_str(sK11_skl))&(element(sK12_skl,the_carrier(sK11_skl))&(element(sK13_skl,the_carrier(sK11_skl))&((related(sK11_skl,sK12_skl,sK13_skl)&related(sK11_skl,sK13_skl,sK12_skl))&~sK12_skl=sK13_skl))))),
% 0.08/0.38 inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl,sK12_skl,sK13_skl]),skolemize(A,sK11_skl),skolemize(B,sK12_skl),skolemize(C,sK13_skl)],[f119])).
% 0.08/0.38 fof(f121,plain,(
% 0.08/0.38 antisymmetric_relstr(sK11_skl)),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f120])).
% 0.08/0.38 fof(f122,plain,(
% 0.08/0.38 rel_str(sK11_skl)),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f120])).
% 0.08/0.38 fof(f123,plain,(
% 0.08/0.38 element(sK12_skl,the_carrier(sK11_skl))),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f120])).
% 0.08/0.38 fof(f124,plain,(
% 0.08/0.38 element(sK13_skl,the_carrier(sK11_skl))),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f120])).
% 0.08/0.38 fof(f125,plain,(
% 0.08/0.38 related(sK11_skl,sK12_skl,sK13_skl)),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f120])).
% 0.08/0.38 fof(f126,plain,(
% 0.08/0.38 related(sK11_skl,sK13_skl,sK12_skl)),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f120])).
% 0.08/0.38 fof(f127,plain,(
% 0.08/0.38 ~sK12_skl=sK13_skl),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f120])).
% 0.08/0.38 fof(f128,plain,(
% 0.08/0.38 ![A,B]: (~element(A,B)|(empty(B)|in(A,B)))),
% 0.08/0.38 inference(pre_NNF_transformation,[status(thm)],[f41])).
% 0.08/0.38 fof(f129,plain,(
% 0.08/0.38 ![X0,X1]: (~element(X0,X1)|empty(X1)|in(X0,X1))),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f128])).
% 0.08/0.38 fof(f134,plain,(
% 0.08/0.38 ![A,B,C]: ((~in(A,B)|~element(B,powerset(C)))|element(A,C))),
% 0.08/0.38 inference(pre_NNF_transformation,[status(thm)],[f43])).
% 0.08/0.38 fof(f135,plain,(
% 0.08/0.38 ![A,C]: ((![B]: (~in(A,B)|~element(B,powerset(C))))|element(A,C))),
% 0.08/0.38 inference(miniscoping,[status(thm)],[f134])).
% 0.08/0.38 fof(f136,plain,(
% 0.08/0.38 ![X0,X1,X2]: (~in(X0,X1)|~element(X1,powerset(X2))|element(X0,X2))),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f135])).
% 0.08/0.38 fof(f137,plain,(
% 0.08/0.38 ![A,B,C]: ((~in(A,B)|~element(B,powerset(C)))|~empty(C))),
% 0.08/0.38 inference(pre_NNF_transformation,[status(thm)],[f44])).
% 0.08/0.38 fof(f138,plain,(
% 0.08/0.38 ![C]: ((![B]: ((![A]: ~in(A,B))|~element(B,powerset(C))))|~empty(C))),
% 0.08/0.38 inference(miniscoping,[status(thm)],[f137])).
% 0.08/0.38 fof(f139,plain,(
% 0.08/0.38 ![X0,X1,X2]: (~in(X0,X1)|~element(X1,powerset(X2))|~empty(X2))),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f138])).
% 0.08/0.38 fof(f140,plain,(
% 0.08/0.38 ![A]: (~empty(A)|A=empty_set)),
% 0.08/0.38 inference(pre_NNF_transformation,[status(thm)],[f45])).
% 0.08/0.38 fof(f141,plain,(
% 0.08/0.38 ![X0]: (~empty(X0)|X0=empty_set)),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f140])).
% 0.08/0.38 fof(f142,plain,(
% 0.08/0.38 ![A,B]: (~in(A,B)|~empty(B))),
% 0.08/0.38 inference(pre_NNF_transformation,[status(thm)],[f46])).
% 0.08/0.38 fof(f143,plain,(
% 0.08/0.38 ![B]: ((![A]: ~in(A,B))|~empty(B))),
% 0.08/0.38 inference(miniscoping,[status(thm)],[f142])).
% 0.08/0.38 fof(f144,plain,(
% 0.08/0.38 ![X0,X1]: (~in(X0,X1)|~empty(X1))),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f143])).
% 0.08/0.38 fof(f148,plain,(
% 0.08/0.38 empty(the_carrier(sK11_skl))|in(sK13_skl,the_carrier(sK11_skl))),
% 0.08/0.38 inference(resolution,[status(thm)],[f129,f124])).
% 0.08/0.38 fof(f149,plain,(
% 0.08/0.38 empty(the_carrier(sK11_skl))|in(sK12_skl,the_carrier(sK11_skl))),
% 0.08/0.38 inference(resolution,[status(thm)],[f129,f123])).
% 0.08/0.38 fof(f150,definition,(
% 0.08/0.38 sQ0_spl <=> (empty(the_carrier(sK11_skl)))),
% 0.08/0.38 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.08/0.38 fof(f151,plain,(
% 0.08/0.38 empty(the_carrier(sK11_skl))|~sQ0_spl),
% 0.08/0.38 inference(component_clause,[status(thm)],[f150])).
% 0.08/0.38 fof(f153,definition,(
% 0.08/0.38 sQ1_spl <=> (in(sK13_skl,the_carrier(sK11_skl)))),
% 0.08/0.38 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.08/0.38 fof(f156,plain,(
% 0.08/0.38 sQ0_spl|sQ1_spl),
% 0.08/0.38 inference(split_clause,[status(thm)],[f148,f150,f153])).
% 0.08/0.38 fof(f157,definition,(
% 0.08/0.38 sQ2_spl <=> (in(sK12_skl,the_carrier(sK11_skl)))),
% 0.08/0.38 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.08/0.38 fof(f160,plain,(
% 0.08/0.38 sQ0_spl|sQ2_spl),
% 0.08/0.38 inference(split_clause,[status(thm)],[f149,f150,f157])).
% 0.08/0.38 fof(f161,plain,(
% 0.08/0.38 ~antisymmetric_relstr(sK11_skl)|is_antisymmetric_in(the_InternalRel(sK11_skl),the_carrier(sK11_skl))),
% 0.08/0.38 inference(resolution,[status(thm)],[f67,f122])).
% 0.08/0.38 fof(f162,definition,(
% 0.08/0.38 sQ3_spl <=> (antisymmetric_relstr(sK11_skl))),
% 0.08/0.38 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.08/0.38 fof(f164,plain,(
% 0.08/0.38 ~antisymmetric_relstr(sK11_skl)|sQ3_spl),
% 0.08/0.38 inference(component_clause,[status(thm)],[f162])).
% 0.08/0.38 fof(f165,definition,(
% 0.08/0.38 sQ4_spl <=> (is_antisymmetric_in(the_InternalRel(sK11_skl),the_carrier(sK11_skl)))),
% 0.08/0.38 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.08/0.38 fof(f166,plain,(
% 0.08/0.38 is_antisymmetric_in(the_InternalRel(sK11_skl),the_carrier(sK11_skl))|~sQ4_spl),
% 0.08/0.38 inference(component_clause,[status(thm)],[f165])).
% 0.08/0.38 fof(f168,plain,(
% 0.08/0.38 ~sQ3_spl|sQ4_spl),
% 0.08/0.38 inference(split_clause,[status(thm)],[f161,f162,f165])).
% 0.08/0.38 fof(f169,plain,(
% 0.08/0.38 $false|sQ3_spl),
% 0.08/0.38 inference(forward_subsumption_resolution,[status(thm)],[f164,f121])).
% 0.08/0.38 fof(f170,plain,(
% 0.08/0.38 sQ3_spl),
% 0.08/0.38 inference(contradiction_clause,[status(thm)],[f169])).
% 0.08/0.38 fof(f172,definition,(
% 0.08/0.38 sQ5_spl <=> (rel_str(sK11_skl))),
% 0.08/0.38 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.08/0.38 fof(f174,plain,(
% 0.08/0.38 ~rel_str(sK11_skl)|sQ5_spl),
% 0.08/0.38 inference(component_clause,[status(thm)],[f172])).
% 0.08/0.38 fof(f176,plain,(
% 0.08/0.38 ![X0]: (~rel_str(sK11_skl)|~element(X0,the_carrier(sK11_skl))|~related(sK11_skl,sK13_skl,X0)|in(ordered_pair(sK13_skl,X0),the_InternalRel(sK11_skl)))),
% 0.08/0.38 inference(resolution,[status(thm)],[f71,f124])).
% 0.08/0.38 fof(f177,plain,(
% 0.08/0.38 ![X0]: (~rel_str(sK11_skl)|~element(X0,the_carrier(sK11_skl))|~related(sK11_skl,sK12_skl,X0)|in(ordered_pair(sK12_skl,X0),the_InternalRel(sK11_skl)))),
% 0.08/0.38 inference(resolution,[status(thm)],[f71,f123])).
% 0.08/0.38 fof(f178,definition,(
% 0.08/0.38 ![X0]: (sQ6_spl <=> (~element(X0,the_carrier(sK11_skl))|~related(sK11_skl,sK13_skl,X0)|in(ordered_pair(sK13_skl,X0),the_InternalRel(sK11_skl))))),
% 0.08/0.38 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.08/0.38 fof(f179,plain,(
% 0.08/0.38 ![X0]: (~element(X0,the_carrier(sK11_skl))|~related(sK11_skl,sK13_skl,X0)|in(ordered_pair(sK13_skl,X0),the_InternalRel(sK11_skl))|~sQ6_spl)),
% 0.08/0.38 inference(component_clause,[status(thm)],[f178])).
% 0.08/0.38 fof(f181,plain,(
% 0.08/0.38 ~sQ5_spl|sQ6_spl),
% 0.08/0.38 inference(split_clause,[status(thm)],[f176,f172,f178])).
% 0.08/0.38 fof(f182,definition,(
% 0.08/0.38 ![X0]: (sQ7_spl <=> (~element(X0,the_carrier(sK11_skl))|~related(sK11_skl,sK12_skl,X0)|in(ordered_pair(sK12_skl,X0),the_InternalRel(sK11_skl))))),
% 0.08/0.38 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.08/0.38 fof(f183,plain,(
% 0.08/0.38 ![X0]: (~element(X0,the_carrier(sK11_skl))|~related(sK11_skl,sK12_skl,X0)|in(ordered_pair(sK12_skl,X0),the_InternalRel(sK11_skl))|~sQ7_spl)),
% 0.08/0.38 inference(component_clause,[status(thm)],[f182])).
% 0.08/0.38 fof(f185,plain,(
% 0.08/0.38 ~sQ5_spl|sQ7_spl),
% 0.08/0.38 inference(split_clause,[status(thm)],[f177,f172,f182])).
% 0.08/0.38 fof(f186,plain,(
% 0.08/0.38 $false|sQ5_spl),
% 0.08/0.38 inference(forward_subsumption_resolution,[status(thm)],[f174,f122])).
% 0.08/0.38 fof(f187,plain,(
% 0.08/0.38 sQ5_spl),
% 0.08/0.38 inference(contradiction_clause,[status(thm)],[f186])).
% 0.08/0.38 fof(f189,plain,(
% 0.08/0.38 ~related(sK11_skl,sK13_skl,sK12_skl)|in(ordered_pair(sK13_skl,sK12_skl),the_InternalRel(sK11_skl))|~sQ6_spl),
% 0.08/0.38 inference(resolution,[status(thm)],[f179,f123])).
% 0.08/0.38 fof(f197,definition,(
% 0.08/0.38 sQ10_spl <=> (related(sK11_skl,sK13_skl,sK12_skl))),
% 0.08/0.38 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.08/0.38 fof(f199,plain,(
% 0.08/0.38 ~related(sK11_skl,sK13_skl,sK12_skl)|sQ10_spl),
% 0.08/0.38 inference(component_clause,[status(thm)],[f197])).
% 0.08/0.38 fof(f200,definition,(
% 0.08/0.38 sQ11_spl <=> (in(ordered_pair(sK13_skl,sK12_skl),the_InternalRel(sK11_skl)))),
% 0.08/0.38 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.08/0.38 fof(f201,plain,(
% 0.08/0.38 in(ordered_pair(sK13_skl,sK12_skl),the_InternalRel(sK11_skl))|~sQ11_spl),
% 0.08/0.38 inference(component_clause,[status(thm)],[f200])).
% 0.08/0.38 fof(f203,plain,(
% 0.08/0.38 ~sQ10_spl|sQ11_spl|~sQ6_spl),
% 0.08/0.38 inference(split_clause,[status(thm)],[f189,f197,f200,f178])).
% 0.08/0.38 fof(f204,plain,(
% 0.08/0.38 $false|sQ10_spl),
% 0.08/0.38 inference(forward_subsumption_resolution,[status(thm)],[f199,f126])).
% 0.08/0.38 fof(f205,plain,(
% 0.08/0.38 sQ10_spl),
% 0.08/0.38 inference(contradiction_clause,[status(thm)],[f204])).
% 0.08/0.38 fof(f206,plain,(
% 0.08/0.38 ~related(sK11_skl,sK12_skl,sK13_skl)|in(ordered_pair(sK12_skl,sK13_skl),the_InternalRel(sK11_skl))|~sQ7_spl),
% 0.08/0.38 inference(resolution,[status(thm)],[f183,f124])).
% 0.08/0.38 fof(f208,definition,(
% 0.08/0.38 sQ12_spl <=> (related(sK11_skl,sK12_skl,sK13_skl))),
% 0.08/0.38 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.08/0.38 fof(f210,plain,(
% 0.08/0.38 ~related(sK11_skl,sK12_skl,sK13_skl)|sQ12_spl),
% 0.08/0.38 inference(component_clause,[status(thm)],[f208])).
% 0.08/0.38 fof(f211,definition,(
% 0.08/0.38 sQ13_spl <=> (in(ordered_pair(sK12_skl,sK13_skl),the_InternalRel(sK11_skl)))),
% 0.08/0.38 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.08/0.38 fof(f212,plain,(
% 0.08/0.38 in(ordered_pair(sK12_skl,sK13_skl),the_InternalRel(sK11_skl))|~sQ13_spl),
% 0.08/0.38 inference(component_clause,[status(thm)],[f211])).
% 0.08/0.38 fof(f214,plain,(
% 0.08/0.38 ~sQ12_spl|sQ13_spl|~sQ7_spl),
% 0.08/0.38 inference(split_clause,[status(thm)],[f206,f208,f211,f182])).
% 0.08/0.38 fof(f222,plain,(
% 0.08/0.38 $false|sQ12_spl),
% 0.08/0.38 inference(forward_subsumption_resolution,[status(thm)],[f210,f125])).
% 0.08/0.38 fof(f223,plain,(
% 0.08/0.38 sQ12_spl),
% 0.08/0.38 inference(contradiction_clause,[status(thm)],[f222])).
% 0.08/0.38 fof(f237,plain,(
% 0.08/0.38 ![X0]: (empty(X0)|in(sK5_skl(X0),X0))),
% 0.08/0.38 inference(resolution,[status(thm)],[f86,f129])).
% 0.08/0.38 fof(f262,definition,(
% 0.08/0.38 sQ22_spl <=> (element(sK13_skl,the_carrier(sK11_skl)))),
% 0.08/0.38 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 0.08/0.38 fof(f264,plain,(
% 0.08/0.38 ~element(sK13_skl,the_carrier(sK11_skl))|sQ22_spl),
% 0.08/0.38 inference(component_clause,[status(thm)],[f262])).
% 0.08/0.38 fof(f265,definition,(
% 0.08/0.38 sQ23_spl <=> (element(sK12_skl,the_carrier(sK11_skl)))),
% 0.08/0.38 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 0.08/0.38 fof(f267,plain,(
% 0.08/0.38 ~element(sK12_skl,the_carrier(sK11_skl))|sQ23_spl),
% 0.08/0.38 inference(component_clause,[status(thm)],[f265])).
% 0.08/0.38 fof(f273,plain,(
% 0.08/0.38 ![X0]: (empty(X0)|~in(X0,sK5_skl(X0)))),
% 0.08/0.38 inference(resolution,[status(thm)],[f237,f49])).
% 0.08/0.38 fof(f276,definition,(
% 0.08/0.38 sQ24_spl <=> (empty(the_InternalRel(sK11_skl)))),
% 0.08/0.38 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 0.08/0.38 fof(f277,plain,(
% 0.08/0.38 empty(the_InternalRel(sK11_skl))|~sQ24_spl),
% 0.08/0.38 inference(component_clause,[status(thm)],[f276])).
% 0.08/0.38 fof(f283,plain,(
% 0.08/0.38 sK8_skl=empty_set),
% 0.08/0.38 inference(resolution,[status(thm)],[f141,f100])).
% 0.08/0.38 fof(f285,plain,(
% 0.08/0.38 the_carrier(sK11_skl)=empty_set|~sQ0_spl),
% 0.08/0.38 inference(resolution,[status(thm)],[f141,f151])).
% 0.08/0.38 fof(f290,plain,(
% 0.08/0.38 is_antisymmetric_in(the_InternalRel(sK11_skl),empty_set)|~sQ0_spl|~sQ4_spl),
% 0.08/0.38 inference(backward_demodulation,[status(thm)],[f285,f166])).
% 0.08/0.38 fof(f292,plain,(
% 0.08/0.38 element(sK13_skl,empty_set)|~sQ0_spl),
% 0.08/0.38 inference(backward_demodulation,[status(thm)],[f285,f124])).
% 0.08/0.38 fof(f293,plain,(
% 0.08/0.38 element(sK12_skl,empty_set)|~sQ0_spl),
% 0.08/0.38 inference(backward_demodulation,[status(thm)],[f285,f123])).
% 0.08/0.38 fof(f328,plain,(
% 0.08/0.38 ![X0]: (~empty(X0)|X0=sK8_skl)),
% 0.08/0.38 inference(backward_demodulation,[status(thm)],[f283,f141])).
% 0.08/0.38 fof(f334,plain,(
% 0.08/0.38 ~empty(the_InternalRel(sK11_skl))|~sQ13_spl),
% 0.08/0.38 inference(resolution,[status(thm)],[f144,f212])).
% 0.08/0.38 fof(f347,plain,(
% 0.08/0.38 ![X0]: (~relation(the_InternalRel(sK11_skl))|~is_antisymmetric_in(the_InternalRel(sK11_skl),X0)|~in(sK13_skl,X0)|~in(sK12_skl,X0)|~in(ordered_pair(sK13_skl,sK12_skl),the_InternalRel(sK11_skl))|sK13_skl=sK12_skl|~sQ13_spl)),
% 0.08/0.38 inference(resolution,[status(thm)],[f58,f212])).
% 0.08/0.38 fof(f349,definition,(
% 0.08/0.38 sQ30_spl <=> (relation(the_InternalRel(sK11_skl)))),
% 0.08/0.38 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 0.08/0.38 fof(f351,plain,(
% 0.08/0.38 ~relation(the_InternalRel(sK11_skl))|sQ30_spl),
% 0.08/0.38 inference(component_clause,[status(thm)],[f349])).
% 0.08/0.38 fof(f352,definition,(
% 0.08/0.38 ![X0]: (sQ31_spl <=> (~is_antisymmetric_in(the_InternalRel(sK11_skl),X0)|~in(sK13_skl,X0)|~in(sK12_skl,X0)))),
% 0.08/0.38 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 0.08/0.38 fof(f353,plain,(
% 0.08/0.38 ![X0]: (~is_antisymmetric_in(the_InternalRel(sK11_skl),X0)|~in(sK13_skl,X0)|~in(sK12_skl,X0)|~sQ31_spl)),
% 0.08/0.38 inference(component_clause,[status(thm)],[f352])).
% 0.08/0.38 fof(f355,definition,(
% 0.08/0.38 sQ32_spl <=> (sK13_skl=sK12_skl)),
% 0.08/0.38 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 0.08/0.38 fof(f356,plain,(
% 0.08/0.38 sK13_skl=sK12_skl|~sQ32_spl),
% 0.08/0.38 inference(component_clause,[status(thm)],[f355])).
% 0.08/0.38 fof(f358,plain,(
% 0.08/0.38 ~sQ30_spl|sQ31_spl|~sQ11_spl|sQ32_spl|~sQ13_spl),
% 0.08/0.38 inference(split_clause,[status(thm)],[f347,f349,f352,f200,f355,f211])).
% 0.08/0.38 fof(f360,plain,(
% 0.08/0.38 $false|sQ22_spl),
% 0.08/0.38 inference(forward_subsumption_resolution,[status(thm)],[f264,f124])).
% 0.08/0.38 fof(f361,plain,(
% 0.08/0.38 sQ22_spl),
% 0.08/0.38 inference(contradiction_clause,[status(thm)],[f360])).
% 0.08/0.38 fof(f362,plain,(
% 0.08/0.38 $false|sQ23_spl),
% 0.08/0.38 inference(forward_subsumption_resolution,[status(thm)],[f267,f123])).
% 0.08/0.38 fof(f363,plain,(
% 0.08/0.38 sQ23_spl),
% 0.08/0.38 inference(contradiction_clause,[status(thm)],[f362])).
% 0.08/0.38 fof(f364,plain,(
% 0.08/0.38 $false|~sQ32_spl),
% 0.08/0.38 inference(forward_subsumption_resolution,[status(thm)],[f356,f127])).
% 0.08/0.38 fof(f365,plain,(
% 0.08/0.38 ~sQ32_spl),
% 0.08/0.38 inference(contradiction_clause,[status(thm)],[f364])).
% 0.08/0.38 fof(f430,plain,(
% 0.08/0.38 ![X0,X1]: (~in(X0,sK5_skl(powerset(X1)))|~empty(X1))),
% 0.08/0.38 inference(resolution,[status(thm)],[f139,f86])).
% 0.08/0.38 fof(f432,definition,(
% 0.08/0.38 ![X0]: (sQ33_spl <=> (~in(X0,sK8_skl)))),
% 0.08/0.38 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 0.08/0.38 fof(f433,plain,(
% 0.08/0.38 ![X0]: (~in(X0,sK8_skl)|~sQ33_spl)),
% 0.08/0.38 inference(component_clause,[status(thm)],[f432])).
% 0.08/0.38 fof(f443,plain,(
% 0.08/0.38 relation_of2_as_subset(the_InternalRel(sK11_skl),the_carrier(sK11_skl),the_carrier(sK11_skl))),
% 0.08/0.38 inference(resolution,[status(thm)],[f78,f122])).
% 0.08/0.38 fof(f444,plain,(
% 0.08/0.38 element(the_InternalRel(sK11_skl),powerset(cartesian_product2(the_carrier(sK11_skl),the_carrier(sK11_skl))))),
% 0.08/0.38 inference(resolution,[status(thm)],[f443,f76])).
% 0.08/0.38 fof(f447,plain,(
% 0.08/0.38 relation(the_InternalRel(sK11_skl))),
% 0.08/0.38 inference(resolution,[status(thm)],[f444,f52])).
% 0.08/0.38 fof(f448,plain,(
% 0.08/0.38 ![X0]: (~in(X0,the_InternalRel(sK11_skl))|~empty(cartesian_product2(the_carrier(sK11_skl),the_carrier(sK11_skl))))),
% 0.08/0.38 inference(resolution,[status(thm)],[f444,f139])).
% 0.08/0.38 fof(f450,plain,(
% 0.08/0.38 empty(powerset(cartesian_product2(the_carrier(sK11_skl),the_carrier(sK11_skl))))|in(the_InternalRel(sK11_skl),powerset(cartesian_product2(the_carrier(sK11_skl),the_carrier(sK11_skl))))),
% 0.08/0.38 inference(resolution,[status(thm)],[f444,f129])).
% 0.08/0.38 fof(f451,plain,(
% 0.08/0.38 $false|sQ30_spl),
% 0.08/0.38 inference(forward_subsumption_resolution,[status(thm)],[f447,f351])).
% 0.08/0.38 fof(f452,plain,(
% 0.08/0.38 sQ30_spl),
% 0.08/0.38 inference(contradiction_clause,[status(thm)],[f451])).
% 0.08/0.38 fof(f453,definition,(
% 0.08/0.38 ![X0]: (sQ35_spl <=> (~in(X0,the_InternalRel(sK11_skl))))),
% 0.08/0.38 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 0.08/0.38 fof(f454,plain,(
% 0.08/0.38 ![X0]: (~in(X0,the_InternalRel(sK11_skl))|~sQ35_spl)),
% 0.08/0.38 inference(component_clause,[status(thm)],[f453])).
% 0.08/0.38 fof(f456,definition,(
% 0.08/0.38 sQ36_spl <=> (empty(cartesian_product2(the_carrier(sK11_skl),the_carrier(sK11_skl))))),
% 0.08/0.38 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 0.08/0.38 fof(f459,plain,(
% 0.08/0.38 sQ35_spl|~sQ36_spl),
% 0.08/0.38 inference(split_clause,[status(thm)],[f448,f453,f456])).
% 0.08/0.38 fof(f460,definition,(
% 0.08/0.38 sQ37_spl <=> (empty(powerset(cartesian_product2(the_carrier(sK11_skl),the_carrier(sK11_skl)))))),
% 0.08/0.38 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 0.08/0.38 fof(f461,plain,(
% 0.08/0.38 empty(powerset(cartesian_product2(the_carrier(sK11_skl),the_carrier(sK11_skl))))|~sQ37_spl),
% 0.08/0.38 inference(component_clause,[status(thm)],[f460])).
% 0.08/0.38 fof(f463,definition,(
% 0.08/0.38 sQ38_spl <=> (in(the_InternalRel(sK11_skl),powerset(cartesian_product2(the_carrier(sK11_skl),the_carrier(sK11_skl)))))),
% 0.08/0.38 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 0.08/0.38 fof(f466,plain,(
% 0.08/0.38 sQ37_spl|sQ38_spl),
% 0.08/0.38 inference(split_clause,[status(thm)],[f450,f460,f463])).
% 0.08/0.38 fof(f467,plain,(
% 0.08/0.38 $false|~sQ37_spl),
% 0.08/0.38 inference(forward_subsumption_resolution,[status(thm)],[f461,f89])).
% 0.08/0.38 fof(f468,plain,(
% 0.08/0.38 ~sQ37_spl),
% 0.08/0.38 inference(contradiction_clause,[status(thm)],[f467])).
% 0.08/0.38 fof(f476,plain,(
% 0.08/0.38 $false|~sQ35_spl|~sQ13_spl),
% 0.08/0.38 inference(backward_subsumption_resolution,[status(thm)],[f212,f454])).
% 0.08/0.38 fof(f479,plain,(
% 0.08/0.38 ~sQ35_spl|~sQ13_spl),
% 0.08/0.38 inference(contradiction_clause,[status(thm)],[f476])).
% 0.08/0.38 fof(f494,plain,(
% 0.08/0.38 ~in(sK13_skl,the_carrier(sK11_skl))|~in(sK12_skl,the_carrier(sK11_skl))|~sQ31_spl|~sQ4_spl),
% 0.08/0.38 inference(resolution,[status(thm)],[f353,f166])).
% 0.08/0.38 fof(f495,plain,(
% 0.08/0.38 ~sQ1_spl|~sQ2_spl|~sQ31_spl|~sQ4_spl),
% 0.08/0.38 inference(split_clause,[status(thm)],[f494,f153,f157,f352,f165])).
% 0.08/0.38 fof(f504,plain,(
% 0.08/0.38 the_carrier(sK11_skl)=sK8_skl|~sQ0_spl),
% 0.08/0.38 inference(forward_demodulation,[status(thm)],[f283,f285])).
% 0.08/0.38 fof(f509,plain,(
% 0.08/0.38 is_antisymmetric_in(the_InternalRel(sK11_skl),sK8_skl)|~sQ0_spl|~sQ4_spl),
% 0.08/0.38 inference(forward_demodulation,[status(thm)],[f283,f290])).
% 0.08/0.38 fof(f510,plain,(
% 0.08/0.38 element(sK12_skl,sK8_skl)|~sQ0_spl),
% 0.08/0.38 inference(forward_demodulation,[status(thm)],[f283,f293])).
% 0.08/0.38 fof(f511,plain,(
% 0.08/0.38 element(sK13_skl,sK8_skl)|~sQ0_spl),
% 0.08/0.38 inference(forward_demodulation,[status(thm)],[f283,f292])).
% 0.08/0.38 fof(f514,plain,(
% 0.08/0.38 element(the_InternalRel(sK11_skl),powerset(cartesian_product2(the_carrier(sK11_skl),sK8_skl)))|~sQ0_spl),
% 0.08/0.38 inference(backward_demodulation,[status(thm)],[f504,f444])).
% 0.08/0.38 fof(f527,plain,(
% 0.08/0.38 element(the_InternalRel(sK11_skl),powerset(cartesian_product2(sK8_skl,sK8_skl)))|~sQ0_spl),
% 0.08/0.38 inference(forward_demodulation,[status(thm)],[f504,f514])).
% 0.08/0.38 fof(f545,plain,(
% 0.08/0.38 empty(sK8_skl)|in(sK12_skl,sK8_skl)|~sQ0_spl),
% 0.08/0.38 inference(resolution,[status(thm)],[f510,f129])).
% 0.08/0.38 fof(f546,definition,(
% 0.08/0.38 sQ42_spl <=> (empty(sK8_skl))),
% 0.08/0.38 introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition])).
% 0.08/0.38 fof(f549,definition,(
% 0.08/0.38 sQ43_spl <=> (in(sK12_skl,sK8_skl))),
% 0.08/0.38 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 0.08/0.38 fof(f552,plain,(
% 0.08/0.38 sQ42_spl|sQ43_spl|~sQ0_spl),
% 0.08/0.38 inference(split_clause,[status(thm)],[f545,f546,f549,f150])).
% 0.08/0.38 fof(f553,plain,(
% 0.08/0.38 empty(sK8_skl)|in(sK13_skl,sK8_skl)|~sQ0_spl),
% 0.08/0.38 inference(resolution,[status(thm)],[f511,f129])).
% 0.08/0.38 fof(f554,definition,(
% 0.08/0.38 sQ44_spl <=> (in(sK13_skl,sK8_skl))),
% 0.08/0.38 introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 0.08/0.38 fof(f557,plain,(
% 0.08/0.38 sQ42_spl|sQ44_spl|~sQ0_spl),
% 0.08/0.38 inference(split_clause,[status(thm)],[f553,f546,f554,f150])).
% 0.08/0.38 fof(f570,plain,(
% 0.08/0.38 ~in(sK13_skl,sK8_skl)|~in(sK12_skl,sK8_skl)|~sQ0_spl|~sQ4_spl|~sQ31_spl),
% 0.08/0.38 inference(resolution,[status(thm)],[f509,f353])).
% 0.08/0.38 fof(f571,plain,(
% 0.08/0.38 ~sQ44_spl|~sQ43_spl|~sQ0_spl|~sQ4_spl|~sQ31_spl),
% 0.08/0.38 inference(split_clause,[status(thm)],[f570,f554,f549,f150,f165,f352])).
% 0.08/0.38 fof(f576,plain,(
% 0.08/0.38 ![X0]: (~empty(X0)|empty(sK5_skl(powerset(X0))))),
% 0.08/0.38 inference(resolution,[status(thm)],[f430,f237])).
% 0.08/0.38 fof(f577,plain,(
% 0.08/0.38 empty(sK5_skl(powerset(sK8_skl)))),
% 0.08/0.38 inference(resolution,[status(thm)],[f576,f100])).
% 0.08/0.38 fof(f580,plain,(
% 0.08/0.38 sK5_skl(powerset(sK8_skl))=sK8_skl),
% 0.08/0.38 inference(resolution,[status(thm)],[f577,f328])).
% 0.08/0.38 fof(f582,plain,(
% 0.08/0.38 ![X0]: (~in(X0,sK8_skl)|~empty(sK8_skl))),
% 0.08/0.38 inference(paramodulation,[status(thm)],[f580,f430])).
% 0.08/0.38 fof(f584,plain,(
% 0.08/0.38 empty(powerset(sK8_skl))|~in(powerset(sK8_skl),sK8_skl)),
% 0.08/0.38 inference(paramodulation,[status(thm)],[f580,f273])).
% 0.08/0.38 fof(f585,plain,(
% 0.08/0.38 empty(powerset(sK8_skl))|in(sK8_skl,powerset(sK8_skl))),
% 0.08/0.38 inference(paramodulation,[status(thm)],[f580,f237])).
% 0.08/0.38 fof(f587,plain,(
% 0.08/0.38 sQ33_spl|~sQ42_spl),
% 0.08/0.38 inference(split_clause,[status(thm)],[f582,f432,f546])).
% 0.08/0.38 fof(f588,definition,(
% 0.08/0.38 sQ47_spl <=> (empty(powerset(sK8_skl)))),
% 0.08/0.38 introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition])).
% 0.08/0.38 fof(f589,plain,(
% 0.08/0.38 empty(powerset(sK8_skl))|~sQ47_spl),
% 0.08/0.38 inference(component_clause,[status(thm)],[f588])).
% 0.08/0.38 fof(f591,definition,(
% 0.08/0.38 sQ48_spl <=> (in(powerset(sK8_skl),sK8_skl))),
% 0.08/0.38 introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 0.08/0.38 fof(f594,plain,(
% 0.08/0.38 sQ47_spl|~sQ48_spl),
% 0.08/0.38 inference(split_clause,[status(thm)],[f584,f588,f591])).
% 0.08/0.38 fof(f595,definition,(
% 0.08/0.38 sQ49_spl <=> (in(sK8_skl,powerset(sK8_skl)))),
% 0.08/0.38 introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition])).
% 0.08/0.38 fof(f598,plain,(
% 0.08/0.38 sQ47_spl|sQ49_spl),
% 0.08/0.38 inference(split_clause,[status(thm)],[f585,f588,f595])).
% 0.08/0.38 fof(f599,plain,(
% 0.08/0.38 $false|~sQ47_spl),
% 0.08/0.38 inference(forward_subsumption_resolution,[status(thm)],[f589,f89])).
% 0.08/0.38 fof(f600,plain,(
% 0.08/0.38 ~sQ47_spl),
% 0.08/0.38 inference(contradiction_clause,[status(thm)],[f599])).
% 0.08/0.38 fof(f609,plain,(
% 0.08/0.38 ![X0]: (~in(X0,the_InternalRel(sK11_skl))|~empty(cartesian_product2(sK8_skl,sK8_skl))|~sQ0_spl)),
% 0.08/0.38 inference(resolution,[status(thm)],[f527,f139])).
% 0.08/0.38 fof(f612,definition,(
% 0.08/0.38 sQ50_spl <=> (empty(cartesian_product2(sK8_skl,sK8_skl)))),
% 0.08/0.38 introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition])).
% 0.08/0.38 fof(f615,plain,(
% 0.08/0.38 sQ35_spl|~sQ50_spl|~sQ0_spl),
% 0.08/0.38 inference(split_clause,[status(thm)],[f609,f453,f612,f150])).
% 0.08/0.38 fof(f616,definition,(
% 0.08/0.38 sQ51_spl <=> (empty(powerset(cartesian_product2(sK8_skl,sK8_skl))))),
% 0.08/0.38 introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition])).
% 0.08/0.38 fof(f617,plain,(
% 0.08/0.38 empty(powerset(cartesian_product2(sK8_skl,sK8_skl)))|~sQ51_spl),
% 0.08/0.38 inference(component_clause,[status(thm)],[f616])).
% 0.08/0.38 fof(f623,plain,(
% 0.08/0.38 $false|~sQ51_spl),
% 0.08/0.38 inference(forward_subsumption_resolution,[status(thm)],[f617,f89])).
% 0.08/0.38 fof(f624,plain,(
% 0.08/0.38 ~sQ51_spl),
% 0.08/0.38 inference(contradiction_clause,[status(thm)],[f623])).
% 0.08/0.38 fof(f720,plain,(
% 0.08/0.38 ![X0]: (~in(X0,the_InternalRel(sK11_skl))|element(X0,cartesian_product2(sK8_skl,sK8_skl))|~sQ0_spl)),
% 0.08/0.38 inference(resolution,[status(thm)],[f136,f527])).
% 0.08/0.38 fof(f737,plain,(
% 0.08/0.38 element(ordered_pair(sK13_skl,sK12_skl),cartesian_product2(sK8_skl,sK8_skl))|~sQ0_spl|~sQ11_spl),
% 0.08/0.38 inference(resolution,[status(thm)],[f720,f201])).
% 0.08/0.38 fof(f755,plain,(
% 0.08/0.38 empty(cartesian_product2(sK8_skl,sK8_skl))|in(ordered_pair(sK13_skl,sK12_skl),cartesian_product2(sK8_skl,sK8_skl))|~sQ0_spl|~sQ11_spl),
% 0.08/0.38 inference(resolution,[status(thm)],[f737,f129])).
% 0.08/0.38 fof(f756,definition,(
% 0.08/0.38 sQ57_spl <=> (in(ordered_pair(sK13_skl,sK12_skl),cartesian_product2(sK8_skl,sK8_skl)))),
% 0.08/0.38 introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition])).
% 0.08/0.38 fof(f757,plain,(
% 0.08/0.38 in(ordered_pair(sK13_skl,sK12_skl),cartesian_product2(sK8_skl,sK8_skl))|~sQ57_spl),
% 0.08/0.38 inference(component_clause,[status(thm)],[f756])).
% 0.08/0.38 fof(f759,plain,(
% 0.08/0.38 sQ50_spl|sQ57_spl|~sQ0_spl|~sQ11_spl),
% 0.08/0.38 inference(split_clause,[status(thm)],[f755,f612,f756,f150,f200])).
% 0.08/0.38 fof(f770,plain,(
% 0.08/0.38 $false|~sQ13_spl|~sQ24_spl),
% 0.08/0.38 inference(forward_subsumption_resolution,[status(thm)],[f277,f334])).
% 0.08/0.38 fof(f771,plain,(
% 0.08/0.38 ~sQ13_spl|~sQ24_spl),
% 0.08/0.38 inference(contradiction_clause,[status(thm)],[f770])).
% 0.08/0.38 fof(f786,plain,(
% 0.08/0.38 in(sK12_skl,sK8_skl)|~sQ57_spl),
% 0.08/0.38 inference(resolution,[status(thm)],[f757,f115])).
% 0.08/0.38 fof(f795,plain,(
% 0.08/0.38 $false|~sQ33_spl|~sQ57_spl),
% 0.08/0.38 inference(forward_subsumption_resolution,[status(thm)],[f786,f433])).
% 0.08/0.38 fof(f796,plain,(
% 0.08/0.38 ~sQ33_spl|~sQ57_spl),
% 0.08/0.38 inference(contradiction_clause,[status(thm)],[f795])).
% 0.08/0.38 fof(f797,plain,(
% 0.08/0.38 $false),
% 0.08/0.38 inference(sat_refutation,[status(thm)],[f156,f160,f168,f170,f181,f185,f187,f203,f205,f214,f223,f358,f361,f363,f365,f452,f459,f466,f468,f479,f495,f552,f557,f571,f587,f594,f598,f600,f615,f624,f759,f771,f796])).
% 0.08/0.38 % SZS output end CNFRefutation for theBenchmark.p
% 0.14/0.40 % Elapsed time: 0.044851 seconds
% 0.14/0.40 % CPU time: 0.134495 seconds
% 0.14/0.40 % Total memory used: 24.242 MB
% 0.14/0.40 % Net memory used: 24.121 MB
%------------------------------------------------------------------------------