%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU281+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 : n011.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:13 PM UTC 2026
% Result : Theorem 28.37s 4.10s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU281+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.10/0.37 % Computer : n011.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Mon Sep 21 06:06:41 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.39 % Drodi V4.1.1
% 28.37/4.10 % Refutation found
% 28.37/4.10 % SZS status Theorem for theBenchmark: Theorem is valid
% 28.37/4.10 % SZS output start CNFRefutation for theBenchmark
% 28.37/4.10 fof(f1,conjecture,(
% 28.37/4.10 (! [A,B] :(? [C] :(! [D] :( in(D,C)<=> ( in(D,cartesian_product2(A,B))& (? [E,F] :( ordered_pair(E,F) = D& in(E,A)& F = singleton(E) ) )) ) )))),
% 28.37/4.10 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 28.37/4.10 fof(f2,negated_conjecture,(
% 28.37/4.10 ~((! [A,B] :(? [C] :(! [D] :( in(D,C)<=> ( in(D,cartesian_product2(A,B))& (? [E,F] :( ordered_pair(E,F) = D& in(E,A)& F = singleton(E) ) )) ) ))))),
% 28.37/4.10 inference(negated_conjecture,[status(cth)],[f1])).
% 28.37/4.10 fof(f4,axiom,(
% 28.37/4.10 (! [A] :( ( epsilon_transitive(A)& epsilon_connected(A) )=> ordinal(A) ) )),
% 28.37/4.10 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 28.37/4.10 fof(f5,axiom,(
% 28.37/4.10 (? [A] :( epsilon_transitive(A)& epsilon_connected(A)& ordinal(A) ) )),
% 28.37/4.10 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 28.37/4.10 fof(f6,axiom,(
% 28.37/4.10 (? [A] :( ~ empty(A)& epsilon_transitive(A)& epsilon_connected(A)& ordinal(A) ) )),
% 28.37/4.10 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 28.37/4.10 fof(f8,axiom,(
% 28.37/4.10 (! [A] :( empty(A)=> ( epsilon_transitive(A)& epsilon_connected(A)& ordinal(A) ) ) )),
% 28.37/4.10 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 28.37/4.10 fof(f9,axiom,(
% 28.37/4.10 (? [A] : empty(A) )),
% 28.37/4.10 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 28.37/4.10 fof(f11,axiom,(
% 28.37/4.10 (! [A,B] :( in(A,B)=> ~ in(B,A) ) )),
% 28.37/4.10 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 28.37/4.10 fof(f16,axiom,(
% 28.37/4.10 (! [A,B] :( (! [C,D,E] :( ( C = D& (? [F,G] :( ordered_pair(F,G) = D& in(F,A)& G = singleton(F) ))& C = E& (? [H,I] :( ordered_pair(H,I) = E& in(H,A)& I = singleton(H) ) ))=> D = E ))=> (? [C] :(! [D] :( in(D,C)<=> (? [E] :( in(E,cartesian_product2(A,B))& E = D& (? [J,K] :( ordered_pair(J,K) = D& in(J,A)& K = singleton(J) ) )) )) ))) )),
% 28.37/4.10 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 28.37/4.10 fof(f17,plain,(
% 28.37/4.10 (?[A,B]: ![C]: ?[D]: (in(D,C)<~>(in(D,cartesian_product2(A,B))&(?[E,F]: ((ordered_pair(E,F)=D&in(E,A))&F=singleton(E))))))),
% 28.37/4.10 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 28.37/4.10 fof(f18,plain,(
% 28.37/4.10 ?[A,B]: ![C]: ?[D]: ((in(D,C)|(in(D,cartesian_product2(A,B))&(?[E,F]: ((ordered_pair(E,F)=D&in(E,A))&F=singleton(E)))))&(~in(D,C)|(~in(D,cartesian_product2(A,B))|(![E,F]: ((~ordered_pair(E,F)=D|~in(E,A))|~F=singleton(E))))))),
% 28.37/4.10 inference(NNF_transformation,[status(thm)],[f17])).
% 28.37/4.10 fof(f19,plain,(
% 28.37/4.10 ![C]: ((in(sK2_skl(C),C)|(in(sK2_skl(C),cartesian_product2(sK0_skl,sK1_skl))&((ordered_pair(sK3_skl(C),sK4_skl(C))=sK2_skl(C)&in(sK3_skl(C),sK0_skl))&sK4_skl(C)=singleton(sK3_skl(C)))))&(~in(sK2_skl(C),C)|(~in(sK2_skl(C),cartesian_product2(sK0_skl,sK1_skl))|(![E,F]: ((~ordered_pair(E,F)=sK2_skl(C)|~in(E,sK0_skl))|~F=singleton(E))))))),
% 28.37/4.10 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl,sK3_skl,sK4_skl]),skolemize(A,sK0_skl),skolemize(B,sK1_skl),skolemize(D,sK2_skl(C)),skolemize(E,sK3_skl(C)),skolemize(F,sK4_skl(C))],[f18])).
% 28.37/4.10 fof(f20,plain,(
% 28.37/4.10 ![X0]: (in(sK2_skl(X0),X0)|in(sK2_skl(X0),cartesian_product2(sK0_skl,sK1_skl)))),
% 28.37/4.10 inference(cnf_transformation,[status(thm)],[f19])).
% 28.37/4.10 fof(f21,plain,(
% 28.37/4.10 ![X0]: (in(sK2_skl(X0),X0)|ordered_pair(sK3_skl(X0),sK4_skl(X0))=sK2_skl(X0))),
% 28.37/4.10 inference(cnf_transformation,[status(thm)],[f19])).
% 28.37/4.10 fof(f22,plain,(
% 28.37/4.10 ![X0]: (in(sK2_skl(X0),X0)|in(sK3_skl(X0),sK0_skl))),
% 28.37/4.10 inference(cnf_transformation,[status(thm)],[f19])).
% 28.37/4.10 fof(f23,plain,(
% 28.37/4.10 ![X0]: (in(sK2_skl(X0),X0)|sK4_skl(X0)=singleton(sK3_skl(X0)))),
% 28.37/4.10 inference(cnf_transformation,[status(thm)],[f19])).
% 28.37/4.10 fof(f24,plain,(
% 28.37/4.10 ![X0,X1,X2]: (~in(sK2_skl(X0),X0)|~in(sK2_skl(X0),cartesian_product2(sK0_skl,sK1_skl))|~ordered_pair(X1,X2)=sK2_skl(X0)|~in(X1,sK0_skl)|~X2=singleton(X1))),
% 28.37/4.10 inference(cnf_transformation,[status(thm)],[f19])).
% 28.37/4.10 fof(f28,plain,(
% 28.37/4.10 ![A]: ((~epsilon_transitive(A)|~epsilon_connected(A))|ordinal(A))),
% 28.37/4.10 inference(pre_NNF_transformation,[status(thm)],[f4])).
% 28.37/4.10 fof(f29,plain,(
% 28.37/4.10 ![X0]: (~epsilon_transitive(X0)|~epsilon_connected(X0)|ordinal(X0))),
% 28.37/4.10 inference(cnf_transformation,[status(thm)],[f28])).
% 28.37/4.10 fof(f30,plain,(
% 28.37/4.10 ((epsilon_transitive(sK5_skl)&epsilon_connected(sK5_skl))&ordinal(sK5_skl))),
% 28.37/4.10 inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl]),skolemize(A,sK5_skl)],[f5])).
% 28.37/4.10 fof(f31,plain,(
% 28.37/4.10 epsilon_transitive(sK5_skl)),
% 28.37/4.10 inference(cnf_transformation,[status(thm)],[f30])).
% 28.37/4.10 fof(f32,plain,(
% 28.37/4.10 epsilon_connected(sK5_skl)),
% 28.37/4.10 inference(cnf_transformation,[status(thm)],[f30])).
% 28.37/4.10 fof(f34,plain,(
% 28.37/4.10 (((~empty(sK6_skl)&epsilon_transitive(sK6_skl))&epsilon_connected(sK6_skl))&ordinal(sK6_skl))),
% 28.37/4.10 inference(skolemize,[status(esa),new_symbols(skolem,[sK6_skl]),skolemize(A,sK6_skl)],[f6])).
% 28.37/4.10 fof(f36,plain,(
% 28.37/4.10 epsilon_transitive(sK6_skl)),
% 28.37/4.10 inference(cnf_transformation,[status(thm)],[f34])).
% 28.37/4.10 fof(f37,plain,(
% 28.37/4.10 epsilon_connected(sK6_skl)),
% 28.37/4.10 inference(cnf_transformation,[status(thm)],[f34])).
% 28.37/4.10 fof(f41,plain,(
% 28.37/4.10 ![A]: (~empty(A)|((epsilon_transitive(A)&epsilon_connected(A))&ordinal(A)))),
% 28.37/4.10 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 28.37/4.10 fof(f42,plain,(
% 28.37/4.10 ![X0]: (~empty(X0)|epsilon_transitive(X0))),
% 28.37/4.10 inference(cnf_transformation,[status(thm)],[f41])).
% 28.37/4.10 fof(f43,plain,(
% 28.37/4.10 ![X0]: (~empty(X0)|epsilon_connected(X0))),
% 28.37/4.10 inference(cnf_transformation,[status(thm)],[f41])).
% 28.37/4.10 fof(f45,plain,(
% 28.37/4.10 empty(sK7_skl)),
% 28.37/4.10 inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl]),skolemize(A,sK7_skl)],[f9])).
% 28.37/4.10 fof(f46,plain,(
% 28.37/4.10 empty(sK7_skl)),
% 28.37/4.10 inference(cnf_transformation,[status(thm)],[f45])).
% 28.37/4.10 fof(f49,plain,(
% 28.37/4.10 ![A,B]: (~in(A,B)|~in(B,A))),
% 28.37/4.10 inference(pre_NNF_transformation,[status(thm)],[f11])).
% 28.37/4.10 fof(f50,plain,(
% 28.37/4.10 ![X0,X1]: (~in(X0,X1)|~in(X1,X0))),
% 28.37/4.10 inference(cnf_transformation,[status(thm)],[f49])).
% 28.37/4.10 fof(f52,plain,(
% 28.37/4.10 ![A,B]: ((?[C,D,E]: ((((C=D&(?[F,G]: ((ordered_pair(F,G)=D&in(F,A))&G=singleton(F))))&C=E)&(?[H,I]: ((ordered_pair(H,I)=E&in(H,A))&I=singleton(H))))&~D=E))|(?[C]: ![D]: (in(D,C)<=>(?[E]: ((in(E,cartesian_product2(A,B))&E=D)&(?[J,K]: ((ordered_pair(J,K)=D&in(J,A))&K=singleton(J))))))))),
% 28.37/4.10 inference(pre_NNF_transformation,[status(thm)],[f16])).
% 28.37/4.10 fof(f53,definition,(
% 28.37/4.10 ![A,C,D,E]: (sP0_prd(E,D,C,A)<=>((((C=D&(?[F,G]: ((ordered_pair(F,G)=D&in(F,A))&G=singleton(F))))&C=E)&(?[H,I]: ((ordered_pair(H,I)=E&in(H,A))&I=singleton(H))))&~D=E))),
% 28.37/4.10 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 28.37/4.10 fof(f54,plain,(
% 28.37/4.10 ![A,B]: ((?[C,D,E]: sP0_prd(E,D,C,A))|(?[C]: ![D]: (in(D,C)<=>(?[E]: ((in(E,cartesian_product2(A,B))&E=D)&(?[J,K]: ((ordered_pair(J,K)=D&in(J,A))&K=singleton(J))))))))),
% 28.37/4.10 inference(formula_renaming,[status(thm)],[f52,f53])).
% 28.37/4.10 fof(f55,plain,(
% 28.37/4.10 ![A,B]: ((?[C,D,E]: sP0_prd(E,D,C,A))|(?[C]: ![D]: ((~in(D,C)|(?[E]: ((in(E,cartesian_product2(A,B))&E=D)&(?[J,K]: ((ordered_pair(J,K)=D&in(J,A))&K=singleton(J))))))&(in(D,C)|(![E]: ((~in(E,cartesian_product2(A,B))|~E=D)|(![J,K]: ((~ordered_pair(J,K)=D|~in(J,A))|~K=singleton(J)))))))))),
% 28.37/4.10 inference(NNF_transformation,[status(thm)],[f54])).
% 28.37/4.10 fof(f56,plain,(
% 28.37/4.10 ![A]: ((?[C,D,E]: sP0_prd(E,D,C,A))|(![B]: ?[C]: ((![D]: (~in(D,C)|((?[E]: (in(E,cartesian_product2(A,B))&E=D))&(?[J,K]: ((ordered_pair(J,K)=D&in(J,A))&K=singleton(J))))))&(![D]: (in(D,C)|((![E]: (~in(E,cartesian_product2(A,B))|~E=D))|(![J,K]: ((~ordered_pair(J,K)=D|~in(J,A))|~K=singleton(J)))))))))),
% 28.37/4.10 inference(miniscoping,[status(thm)],[f55])).
% 28.37/4.10 fof(f57,plain,(
% 28.37/4.10 ![A]: (sP0_prd(sK11_skl(A),sK10_skl(A),sK9_skl(A),A)|(![B]: ((![D]: (~in(D,sK12_skl(B,A))|((in(sK13_skl(D,B,A),cartesian_product2(A,B))&sK13_skl(D,B,A)=D)&((ordered_pair(sK14_skl(D,B,A),sK15_skl(D,B,A))=D&in(sK14_skl(D,B,A),A))&sK15_skl(D,B,A)=singleton(sK14_skl(D,B,A))))))&(![D]: (in(D,sK12_skl(B,A))|((![E]: (~in(E,cartesian_product2(A,B))|~E=D))|(![J,K]: ((~ordered_pair(J,K)=D|~in(J,A))|~K=singleton(J)))))))))),
% 28.37/4.10 inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl,sK10_skl,sK11_skl,sK12_skl,sK13_skl,sK14_skl,sK15_skl]),skolemize(C,sK9_skl(A)),skolemize(D,sK10_skl(A)),skolemize(E,sK11_skl(A)),skolemize(C,sK12_skl(B,A)),skolemize(E,sK13_skl(D,B,A)),skolemize(J,sK14_skl(D,B,A)),skolemize(K,sK15_skl(D,B,A))],[f56])).
% 28.37/4.10 fof(f58,plain,(
% 28.37/4.10 ![X0,X1,X2]: (sP0_prd(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0)|~in(X1,sK12_skl(X2,X0))|in(sK13_skl(X1,X2,X0),cartesian_product2(X0,X2)))),
% 28.37/4.10 inference(cnf_transformation,[status(thm)],[f57])).
% 28.37/4.10 fof(f59,plain,(
% 28.37/4.10 ![X0,X1,X2]: (sP0_prd(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0)|~in(X1,sK12_skl(X2,X0))|sK13_skl(X1,X2,X0)=X1)),
% 28.37/4.10 inference(cnf_transformation,[status(thm)],[f57])).
% 28.37/4.10 fof(f60,plain,(
% 28.37/4.10 ![X0,X1,X2]: (sP0_prd(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0)|~in(X1,sK12_skl(X2,X0))|ordered_pair(sK14_skl(X1,X2,X0),sK15_skl(X1,X2,X0))=X1)),
% 28.37/4.10 inference(cnf_transformation,[status(thm)],[f57])).
% 28.37/4.10 fof(f61,plain,(
% 28.37/4.10 ![X0,X1,X2]: (sP0_prd(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0)|~in(X1,sK12_skl(X2,X0))|in(sK14_skl(X1,X2,X0),X0))),
% 28.37/4.10 inference(cnf_transformation,[status(thm)],[f57])).
% 28.37/4.10 fof(f62,plain,(
% 28.37/4.10 ![X0,X1,X2]: (sP0_prd(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0)|~in(X1,sK12_skl(X2,X0))|sK15_skl(X1,X2,X0)=singleton(sK14_skl(X1,X2,X0)))),
% 28.37/4.10 inference(cnf_transformation,[status(thm)],[f57])).
% 28.37/4.10 fof(f63,plain,(
% 28.37/4.10 ![X0,X1,X2,X3,X4,X5]: (sP0_prd(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0)|in(X1,sK12_skl(X2,X0))|~in(X3,cartesian_product2(X0,X2))|~X3=X1|~ordered_pair(X4,X5)=X1|~in(X4,X0)|~X5=singleton(X4))),
% 28.37/4.10 inference(cnf_transformation,[status(thm)],[f57])).
% 28.37/4.10 fof(f64,plain,(
% 28.37/4.10 ![A,C,D,E]: ((~sP0_prd(E,D,C,A)|((((C=D&(?[F,G]: ((ordered_pair(F,G)=D&in(F,A))&G=singleton(F))))&C=E)&(?[H,I]: ((ordered_pair(H,I)=E&in(H,A))&I=singleton(H))))&~D=E))&(sP0_prd(E,D,C,A)|((((~C=D|(![F,G]: ((~ordered_pair(F,G)=D|~in(F,A))|~G=singleton(F))))|~C=E)|(![H,I]: ((~ordered_pair(H,I)=E|~in(H,A))|~I=singleton(H))))|D=E)))),
% 28.37/4.10 inference(NNF_transformation,[status(thm)],[f53])).
% 28.37/4.10 fof(f65,plain,(
% 28.37/4.10 (![A,C,D,E]: (~sP0_prd(E,D,C,A)|((((C=D&(?[F,G]: ((ordered_pair(F,G)=D&in(F,A))&G=singleton(F))))&C=E)&(?[H,I]: ((ordered_pair(H,I)=E&in(H,A))&I=singleton(H))))&~D=E)))&(![A,C,D,E]: (sP0_prd(E,D,C,A)|((((~C=D|(![F,G]: ((~ordered_pair(F,G)=D|~in(F,A))|~G=singleton(F))))|~C=E)|(![H,I]: ((~ordered_pair(H,I)=E|~in(H,A))|~I=singleton(H))))|D=E)))),
% 28.37/4.10 inference(miniscoping,[status(thm)],[f64])).
% 28.37/4.10 fof(f66,plain,(
% 28.37/4.10 (![A,C,D,E]: (~sP0_prd(E,D,C,A)|((((C=D&((ordered_pair(sK16_skl(E,D,C,A),sK17_skl(E,D,C,A))=D&in(sK16_skl(E,D,C,A),A))&sK17_skl(E,D,C,A)=singleton(sK16_skl(E,D,C,A))))&C=E)&((ordered_pair(sK18_skl(E,D,C,A),sK19_skl(E,D,C,A))=E&in(sK18_skl(E,D,C,A),A))&sK19_skl(E,D,C,A)=singleton(sK18_skl(E,D,C,A))))&~D=E)))&(![A,C,D,E]: (sP0_prd(E,D,C,A)|((((~C=D|(![F,G]: ((~ordered_pair(F,G)=D|~in(F,A))|~G=singleton(F))))|~C=E)|(![H,I]: ((~ordered_pair(H,I)=E|~in(H,A))|~I=singleton(H))))|D=E)))),
% 28.37/4.10 inference(skolemize,[status(esa),new_symbols(skolem,[sK16_skl,sK17_skl,sK18_skl,sK19_skl]),skolemize(F,sK16_skl(E,D,C,A)),skolemize(G,sK17_skl(E,D,C,A)),skolemize(H,sK18_skl(E,D,C,A)),skolemize(I,sK19_skl(E,D,C,A))],[f65])).
% 28.37/4.10 fof(f67,plain,(
% 28.37/4.10 ![X0,X1,X2,X3]: (~sP0_prd(X0,X1,X2,X3)|X2=X1)),
% 28.37/4.10 inference(cnf_transformation,[status(thm)],[f66])).
% 28.37/4.10 fof(f69,plain,(
% 28.37/4.10 ![X0,X1,X2,X3]: (~sP0_prd(X0,X1,X2,X3)|in(sK16_skl(X0,X1,X2,X3),X3))),
% 28.37/4.10 inference(cnf_transformation,[status(thm)],[f66])).
% 28.37/4.10 fof(f71,plain,(
% 28.37/4.10 ![X0,X1,X2,X3]: (~sP0_prd(X0,X1,X2,X3)|X2=X0)),
% 28.37/4.10 inference(cnf_transformation,[status(thm)],[f66])).
% 28.37/4.10 fof(f73,plain,(
% 28.37/4.10 ![X0,X1,X2,X3]: (~sP0_prd(X0,X1,X2,X3)|in(sK18_skl(X0,X1,X2,X3),X3))),
% 28.37/4.10 inference(cnf_transformation,[status(thm)],[f66])).
% 28.37/4.10 fof(f75,plain,(
% 28.37/4.10 ![X0,X1,X2,X3]: (~sP0_prd(X0,X1,X2,X3)|~X1=X0)),
% 28.37/4.10 inference(cnf_transformation,[status(thm)],[f66])).
% 28.37/4.10 fof(f77,plain,(
% 28.37/4.10 ![X0,X1]: (~in(sK2_skl(X0),X0)|~in(sK2_skl(X0),cartesian_product2(sK0_skl,sK1_skl))|~ordered_pair(X1,singleton(X1))=sK2_skl(X0)|~in(X1,sK0_skl))),
% 28.37/4.10 inference(destructive_equality_resolution,[status(thm)],[f24])).
% 28.37/4.10 fof(f78,plain,(
% 28.37/4.10 ![X0,X1,X2]: (sP0_prd(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0)|in(ordered_pair(X1,singleton(X1)),sK12_skl(X2,X0))|~in(ordered_pair(X1,singleton(X1)),cartesian_product2(X0,X2))|~in(X1,X0))),
% 28.37/4.10 inference(destructive_equality_resolution,[status(thm)],[f63])).
% 28.37/4.10 fof(f79,plain,(
% 28.37/4.10 ![X0,X1,X2]: (~sP0_prd(X0,X0,X1,X2))),
% 28.37/4.10 inference(destructive_equality_resolution,[status(thm)],[f75])).
% 28.37/4.10 fof(f80,plain,(
% 28.37/4.10 in(sK2_skl(cartesian_product2(sK0_skl,sK1_skl)),cartesian_product2(sK0_skl,sK1_skl))),
% 28.37/4.10 inference(factoring,[status(thm)],[f20])).
% 28.37/4.10 fof(f89,plain,(
% 28.37/4.10 ~epsilon_transitive(sK5_skl)|ordinal(sK5_skl)),
% 28.37/4.10 inference(resolution,[status(thm)],[f32,f29])).
% 28.37/4.10 fof(f90,definition,(
% 28.37/4.10 sQ0_spl <=> (epsilon_transitive(sK5_skl))),
% 28.37/4.10 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 28.37/4.10 fof(f92,plain,(
% 28.37/4.10 ~epsilon_transitive(sK5_skl)|sQ0_spl),
% 28.37/4.10 inference(component_clause,[status(thm)],[f90])).
% 28.37/4.10 fof(f93,definition,(
% 28.37/4.10 sQ1_spl <=> (ordinal(sK5_skl))),
% 28.37/4.10 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 28.37/4.10 fof(f96,plain,(
% 28.37/4.10 ~sQ0_spl|sQ1_spl),
% 28.37/4.10 inference(split_clause,[status(thm)],[f89,f90,f93])).
% 28.37/4.10 fof(f97,plain,(
% 28.37/4.10 $false|sQ0_spl),
% 28.37/4.10 inference(forward_subsumption_resolution,[status(thm)],[f92,f31])).
% 28.37/4.10 fof(f98,plain,(
% 28.37/4.10 sQ0_spl),
% 28.37/4.10 inference(contradiction_clause,[status(thm)],[f97])).
% 28.37/4.10 fof(f101,plain,(
% 28.37/4.10 ~epsilon_transitive(sK6_skl)|ordinal(sK6_skl)),
% 28.37/4.10 inference(resolution,[status(thm)],[f37,f29])).
% 28.37/4.10 fof(f102,definition,(
% 28.37/4.10 sQ2_spl <=> (epsilon_transitive(sK6_skl))),
% 28.37/4.10 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 28.37/4.10 fof(f104,plain,(
% 28.37/4.10 ~epsilon_transitive(sK6_skl)|sQ2_spl),
% 28.37/4.10 inference(component_clause,[status(thm)],[f102])).
% 28.37/4.10 fof(f105,definition,(
% 28.37/4.10 sQ3_spl <=> (ordinal(sK6_skl))),
% 28.37/4.10 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 28.37/4.10 fof(f108,plain,(
% 28.37/4.10 ~sQ2_spl|sQ3_spl),
% 28.37/4.10 inference(split_clause,[status(thm)],[f101,f102,f105])).
% 28.37/4.10 fof(f109,plain,(
% 28.37/4.10 $false|sQ2_spl),
% 28.37/4.10 inference(forward_subsumption_resolution,[status(thm)],[f104,f36])).
% 28.37/4.10 fof(f110,plain,(
% 28.37/4.10 sQ2_spl),
% 28.37/4.10 inference(contradiction_clause,[status(thm)],[f109])).
% 28.37/4.10 fof(f114,plain,(
% 28.37/4.10 epsilon_connected(sK7_skl)),
% 28.37/4.10 inference(resolution,[status(thm)],[f46,f43])).
% 28.37/4.10 fof(f115,plain,(
% 28.37/4.10 epsilon_transitive(sK7_skl)),
% 28.37/4.10 inference(resolution,[status(thm)],[f46,f42])).
% 28.37/4.10 fof(f119,plain,(
% 28.37/4.10 ![X0,X1]: (sP0_prd(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0)|in(sK13_skl(sK2_skl(sK12_skl(X1,X0)),X1,X0),cartesian_product2(X0,X1))|in(sK2_skl(sK12_skl(X1,X0)),cartesian_product2(sK0_skl,sK1_skl)))),
% 28.37/4.10 inference(resolution,[status(thm)],[f58,f20])).
% 28.37/4.10 fof(f120,plain,(
% 28.37/4.10 ![X0,X1]: (sP0_prd(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0)|in(sK13_skl(sK2_skl(sK12_skl(X1,X0)),X1,X0),cartesian_product2(X0,X1))|in(sK3_skl(sK12_skl(X1,X0)),sK0_skl))),
% 28.37/4.10 inference(resolution,[status(thm)],[f58,f22])).
% 28.37/4.10 fof(f121,plain,(
% 28.37/4.10 ![X0,X1]: (sP0_prd(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0)|in(sK13_skl(sK2_skl(sK12_skl(X1,X0)),X1,X0),cartesian_product2(X0,X1))|ordered_pair(sK3_skl(sK12_skl(X1,X0)),sK4_skl(sK12_skl(X1,X0)))=sK2_skl(sK12_skl(X1,X0)))),
% 28.37/4.10 inference(resolution,[status(thm)],[f58,f21])).
% 28.37/4.10 fof(f122,plain,(
% 28.37/4.10 ![X0,X1]: (sP0_prd(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0)|in(sK13_skl(sK2_skl(sK12_skl(X1,X0)),X1,X0),cartesian_product2(X0,X1))|sK4_skl(sK12_skl(X1,X0))=singleton(sK3_skl(sK12_skl(X1,X0))))),
% 28.37/4.10 inference(resolution,[status(thm)],[f58,f23])).
% 28.37/4.10 fof(f127,plain,(
% 28.37/4.10 ![X0,X1]: (in(sK13_skl(sK2_skl(sK12_skl(X0,X1)),X0,X1),cartesian_product2(X1,X0))|in(sK3_skl(sK12_skl(X0,X1)),sK0_skl)|in(sK18_skl(sK11_skl(X1),sK10_skl(X1),sK9_skl(X1),X1),X1))),
% 28.37/4.10 inference(resolution,[status(thm)],[f120,f73])).
% 28.37/4.10 fof(f128,plain,(
% 28.37/4.10 ![X0,X1]: (in(sK13_skl(sK2_skl(sK12_skl(X0,X1)),X0,X1),cartesian_product2(X1,X0))|in(sK3_skl(sK12_skl(X0,X1)),sK0_skl)|in(sK16_skl(sK11_skl(X1),sK10_skl(X1),sK9_skl(X1),X1),X1))),
% 28.37/4.10 inference(resolution,[status(thm)],[f120,f69])).
% 28.37/4.10 fof(f129,plain,(
% 28.37/4.10 ![X0,X1]: (in(sK13_skl(sK2_skl(sK12_skl(X0,X1)),X0,X1),cartesian_product2(X1,X0))|in(sK3_skl(sK12_skl(X0,X1)),sK0_skl)|sK9_skl(X1)=sK11_skl(X1))),
% 28.37/4.10 inference(resolution,[status(thm)],[f120,f71])).
% 28.37/4.10 fof(f130,plain,(
% 28.37/4.10 ![X0,X1]: (in(sK13_skl(sK2_skl(sK12_skl(X0,X1)),X0,X1),cartesian_product2(X1,X0))|in(sK3_skl(sK12_skl(X0,X1)),sK0_skl)|sK9_skl(X1)=sK10_skl(X1))),
% 28.37/4.10 inference(resolution,[status(thm)],[f120,f67])).
% 28.37/4.10 fof(f131,plain,(
% 28.37/4.10 ![X0,X1]: (sP0_prd(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0)|in(sK3_skl(sK12_skl(X1,X0)),sK0_skl)|~in(cartesian_product2(X0,X1),sK13_skl(sK2_skl(sK12_skl(X1,X0)),X1,X0)))),
% 28.37/4.10 inference(resolution,[status(thm)],[f120,f50])).
% 28.37/4.10 fof(f132,plain,(
% 28.37/4.10 ![X0,X1]: (in(sK3_skl(sK12_skl(X0,X1)),sK0_skl)|sK9_skl(X1)=sK11_skl(X1)|~in(cartesian_product2(X1,X0),sK13_skl(sK2_skl(sK12_skl(X0,X1)),X0,X1)))),
% 28.37/4.11 inference(resolution,[status(thm)],[f129,f50])).
% 28.37/4.11 fof(f133,plain,(
% 28.37/4.11 ![X0,X1]: (in(sK3_skl(sK12_skl(X0,X1)),sK0_skl)|sK9_skl(X1)=sK10_skl(X1)|~in(cartesian_product2(X1,X0),sK13_skl(sK2_skl(sK12_skl(X0,X1)),X0,X1)))),
% 28.37/4.11 inference(resolution,[status(thm)],[f130,f50])).
% 28.37/4.11 fof(f146,plain,(
% 28.37/4.11 ![X0,X1]: (in(sK13_skl(sK2_skl(sK12_skl(X0,X1)),X0,X1),cartesian_product2(X1,X0))|in(sK2_skl(sK12_skl(X0,X1)),cartesian_product2(sK0_skl,sK1_skl))|sK9_skl(X1)=sK11_skl(X1))),
% 28.37/4.11 inference(resolution,[status(thm)],[f119,f71])).
% 28.37/4.11 fof(f147,plain,(
% 28.37/4.11 ![X0,X1]: (in(sK13_skl(sK2_skl(sK12_skl(X0,X1)),X0,X1),cartesian_product2(X1,X0))|in(sK2_skl(sK12_skl(X0,X1)),cartesian_product2(sK0_skl,sK1_skl))|sK9_skl(X1)=sK10_skl(X1))),
% 28.37/4.11 inference(resolution,[status(thm)],[f119,f67])).
% 28.37/4.11 fof(f148,plain,(
% 28.37/4.11 ![X0,X1]: (sP0_prd(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0)|in(sK2_skl(sK12_skl(X1,X0)),cartesian_product2(sK0_skl,sK1_skl))|~in(cartesian_product2(X0,X1),sK13_skl(sK2_skl(sK12_skl(X1,X0)),X1,X0)))),
% 28.37/4.11 inference(resolution,[status(thm)],[f119,f50])).
% 28.37/4.11 fof(f155,plain,(
% 28.37/4.11 ![X0,X1]: (in(sK13_skl(sK2_skl(sK12_skl(X0,X1)),X0,X1),cartesian_product2(X1,X0))|ordered_pair(sK3_skl(sK12_skl(X0,X1)),sK4_skl(sK12_skl(X0,X1)))=sK2_skl(sK12_skl(X0,X1))|sK9_skl(X1)=sK11_skl(X1))),
% 28.37/4.11 inference(resolution,[status(thm)],[f121,f71])).
% 28.37/4.11 fof(f156,plain,(
% 28.37/4.11 ![X0,X1]: (in(sK13_skl(sK2_skl(sK12_skl(X0,X1)),X0,X1),cartesian_product2(X1,X0))|ordered_pair(sK3_skl(sK12_skl(X0,X1)),sK4_skl(sK12_skl(X0,X1)))=sK2_skl(sK12_skl(X0,X1))|sK9_skl(X1)=sK10_skl(X1))),
% 28.37/4.11 inference(resolution,[status(thm)],[f121,f67])).
% 28.37/4.11 fof(f157,plain,(
% 28.37/4.11 ![X0,X1]: (sP0_prd(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0)|ordered_pair(sK3_skl(sK12_skl(X1,X0)),sK4_skl(sK12_skl(X1,X0)))=sK2_skl(sK12_skl(X1,X0))|~in(cartesian_product2(X0,X1),sK13_skl(sK2_skl(sK12_skl(X1,X0)),X1,X0)))),
% 28.37/4.11 inference(resolution,[status(thm)],[f121,f50])).
% 28.37/4.11 fof(f158,plain,(
% 28.37/4.11 ~epsilon_transitive(sK7_skl)|ordinal(sK7_skl)),
% 28.37/4.11 inference(resolution,[status(thm)],[f114,f29])).
% 28.37/4.11 fof(f159,definition,(
% 28.37/4.11 sQ4_spl <=> (epsilon_transitive(sK7_skl))),
% 28.37/4.11 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 28.37/4.11 fof(f161,plain,(
% 28.37/4.11 ~epsilon_transitive(sK7_skl)|sQ4_spl),
% 28.37/4.11 inference(component_clause,[status(thm)],[f159])).
% 28.37/4.11 fof(f162,definition,(
% 28.37/4.11 sQ5_spl <=> (ordinal(sK7_skl))),
% 28.37/4.11 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 28.37/4.11 fof(f165,plain,(
% 28.37/4.11 ~sQ4_spl|sQ5_spl),
% 28.37/4.11 inference(split_clause,[status(thm)],[f158,f159,f162])).
% 28.37/4.11 fof(f166,plain,(
% 28.37/4.11 $false|sQ4_spl),
% 28.37/4.11 inference(forward_subsumption_resolution,[status(thm)],[f161,f115])).
% 28.37/4.11 fof(f167,plain,(
% 28.37/4.11 sQ4_spl),
% 28.37/4.11 inference(contradiction_clause,[status(thm)],[f166])).
% 28.37/4.11 fof(f168,plain,(
% 28.37/4.11 ![X0,X1,X2]: (sP0_prd(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0)|sK13_skl(sK16_skl(sK11_skl(sK12_skl(X1,X0)),sK10_skl(sK12_skl(X1,X0)),sK9_skl(sK12_skl(X1,X0)),sK12_skl(X1,X0)),X1,X0)=sK16_skl(sK11_skl(sK12_skl(X1,X0)),sK10_skl(sK12_skl(X1,X0)),sK9_skl(sK12_skl(X1,X0)),sK12_skl(X1,X0))|in(sK13_skl(sK2_skl(sK12_skl(X2,sK12_skl(X1,X0))),X2,sK12_skl(X1,X0)),cartesian_product2(sK12_skl(X1,X0),X2))|in(sK3_skl(sK12_skl(X2,sK12_skl(X1,X0))),sK0_skl))),
% 28.37/4.11 inference(resolution,[status(thm)],[f59,f128])).
% 28.37/4.11 fof(f169,plain,(
% 28.37/4.11 ![X0,X1,X2]: (sP0_prd(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0)|sK13_skl(sK18_skl(sK11_skl(sK12_skl(X1,X0)),sK10_skl(sK12_skl(X1,X0)),sK9_skl(sK12_skl(X1,X0)),sK12_skl(X1,X0)),X1,X0)=sK18_skl(sK11_skl(sK12_skl(X1,X0)),sK10_skl(sK12_skl(X1,X0)),sK9_skl(sK12_skl(X1,X0)),sK12_skl(X1,X0))|in(sK13_skl(sK2_skl(sK12_skl(X2,sK12_skl(X1,X0))),X2,sK12_skl(X1,X0)),cartesian_product2(sK12_skl(X1,X0),X2))|in(sK3_skl(sK12_skl(X2,sK12_skl(X1,X0))),sK0_skl))),
% 28.37/4.11 inference(resolution,[status(thm)],[f59,f127])).
% 28.37/4.11 fof(f170,plain,(
% 28.37/4.11 ![X0,X1]: (sP0_prd(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0)|sK13_skl(sK2_skl(sK12_skl(X1,X0)),X1,X0)=sK2_skl(sK12_skl(X1,X0))|in(sK2_skl(sK12_skl(X1,X0)),cartesian_product2(sK0_skl,sK1_skl)))),
% 28.37/4.11 inference(resolution,[status(thm)],[f59,f20])).
% 28.37/4.11 fof(f171,plain,(
% 28.37/4.11 ![X0,X1]: (sP0_prd(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0)|sK13_skl(sK2_skl(sK12_skl(X1,X0)),X1,X0)=sK2_skl(sK12_skl(X1,X0))|in(sK3_skl(sK12_skl(X1,X0)),sK0_skl))),
% 28.37/4.11 inference(resolution,[status(thm)],[f59,f22])).
% 28.37/4.11 fof(f172,plain,(
% 28.37/4.11 ![X0,X1]: (sP0_prd(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0)|sK13_skl(sK2_skl(sK12_skl(X1,X0)),X1,X0)=sK2_skl(sK12_skl(X1,X0))|ordered_pair(sK3_skl(sK12_skl(X1,X0)),sK4_skl(sK12_skl(X1,X0)))=sK2_skl(sK12_skl(X1,X0)))),
% 28.37/4.11 inference(resolution,[status(thm)],[f59,f21])).
% 28.37/4.11 fof(f173,plain,(
% 28.37/4.11 ![X0,X1]: (sP0_prd(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0)|sK13_skl(sK2_skl(sK12_skl(X1,X0)),X1,X0)=sK2_skl(sK12_skl(X1,X0))|sK4_skl(sK12_skl(X1,X0))=singleton(sK3_skl(sK12_skl(X1,X0))))),
% 28.37/4.11 inference(resolution,[status(thm)],[f59,f23])).
% 28.37/4.11 fof(f176,plain,(
% 28.37/4.11 ![X0,X1]: (sP0_prd(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0)|in(sK14_skl(sK2_skl(sK12_skl(X1,X0)),X1,X0),X0)|in(sK2_skl(sK12_skl(X1,X0)),cartesian_product2(sK0_skl,sK1_skl)))),
% 28.37/4.11 inference(resolution,[status(thm)],[f61,f20])).
% 28.37/4.11 fof(f177,plain,(
% 28.37/4.11 ![X0,X1]: (sP0_prd(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0)|in(sK14_skl(sK2_skl(sK12_skl(X1,X0)),X1,X0),X0)|in(sK3_skl(sK12_skl(X1,X0)),sK0_skl))),
% 28.37/4.11 inference(resolution,[status(thm)],[f61,f22])).
% 28.37/4.11 fof(f178,plain,(
% 28.37/4.11 ![X0,X1]: (sP0_prd(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0)|in(sK14_skl(sK2_skl(sK12_skl(X1,X0)),X1,X0),X0)|ordered_pair(sK3_skl(sK12_skl(X1,X0)),sK4_skl(sK12_skl(X1,X0)))=sK2_skl(sK12_skl(X1,X0)))),
% 28.37/4.11 inference(resolution,[status(thm)],[f61,f21])).
% 28.37/4.11 fof(f179,plain,(
% 28.37/4.11 ![X0,X1]: (sP0_prd(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0)|in(sK14_skl(sK2_skl(sK12_skl(X1,X0)),X1,X0),X0)|sK4_skl(sK12_skl(X1,X0))=singleton(sK3_skl(sK12_skl(X1,X0))))),
% 28.37/4.11 inference(resolution,[status(thm)],[f61,f23])).
% 28.37/4.11 fof(f182,plain,(
% 28.37/4.11 ![X0,X1]: (sP0_prd(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0)|sK15_skl(sK2_skl(sK12_skl(X1,X0)),X1,X0)=singleton(sK14_skl(sK2_skl(sK12_skl(X1,X0)),X1,X0))|in(sK2_skl(sK12_skl(X1,X0)),cartesian_product2(sK0_skl,sK1_skl)))),
% 28.37/4.11 inference(resolution,[status(thm)],[f62,f20])).
% 28.37/4.11 fof(f183,plain,(
% 28.37/4.11 ![X0,X1]: (sP0_prd(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0)|sK15_skl(sK2_skl(sK12_skl(X1,X0)),X1,X0)=singleton(sK14_skl(sK2_skl(sK12_skl(X1,X0)),X1,X0))|in(sK3_skl(sK12_skl(X1,X0)),sK0_skl))),
% 28.37/4.11 inference(resolution,[status(thm)],[f62,f22])).
% 28.37/4.11 fof(f184,plain,(
% 28.37/4.11 ![X0,X1]: (sP0_prd(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0)|sK15_skl(sK2_skl(sK12_skl(X1,X0)),X1,X0)=singleton(sK14_skl(sK2_skl(sK12_skl(X1,X0)),X1,X0))|ordered_pair(sK3_skl(sK12_skl(X1,X0)),sK4_skl(sK12_skl(X1,X0)))=sK2_skl(sK12_skl(X1,X0)))),
% 28.37/4.11 inference(resolution,[status(thm)],[f62,f21])).
% 28.37/4.11 fof(f185,plain,(
% 28.37/4.11 ![X0,X1]: (sP0_prd(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0)|sK15_skl(sK2_skl(sK12_skl(X1,X0)),X1,X0)=singleton(sK14_skl(sK2_skl(sK12_skl(X1,X0)),X1,X0))|sK4_skl(sK12_skl(X1,X0))=singleton(sK3_skl(sK12_skl(X1,X0))))),
% 28.37/4.11 inference(resolution,[status(thm)],[f62,f23])).
% 28.37/4.11 fof(f188,plain,(
% 28.37/4.11 ![X0,X1]: (sP0_prd(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0)|ordered_pair(sK14_skl(sK2_skl(sK12_skl(X1,X0)),X1,X0),sK15_skl(sK2_skl(sK12_skl(X1,X0)),X1,X0))=sK2_skl(sK12_skl(X1,X0))|in(sK2_skl(sK12_skl(X1,X0)),cartesian_product2(sK0_skl,sK1_skl)))),
% 28.37/4.11 inference(resolution,[status(thm)],[f60,f20])).
% 28.37/4.11 fof(f189,plain,(
% 28.37/4.11 ![X0,X1]: (sP0_prd(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0)|ordered_pair(sK14_skl(sK2_skl(sK12_skl(X1,X0)),X1,X0),sK15_skl(sK2_skl(sK12_skl(X1,X0)),X1,X0))=sK2_skl(sK12_skl(X1,X0))|in(sK3_skl(sK12_skl(X1,X0)),sK0_skl))),
% 28.37/4.11 inference(resolution,[status(thm)],[f60,f22])).
% 28.37/4.11 fof(f190,plain,(
% 28.37/4.11 ![X0,X1]: (sP0_prd(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0)|ordered_pair(sK14_skl(sK2_skl(sK12_skl(X1,X0)),X1,X0),sK15_skl(sK2_skl(sK12_skl(X1,X0)),X1,X0))=sK2_skl(sK12_skl(X1,X0))|ordered_pair(sK3_skl(sK12_skl(X1,X0)),sK4_skl(sK12_skl(X1,X0)))=sK2_skl(sK12_skl(X1,X0)))),
% 28.37/4.11 inference(resolution,[status(thm)],[f60,f21])).
% 28.37/4.11 fof(f191,plain,(
% 28.37/4.11 ![X0,X1]: (sP0_prd(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0)|ordered_pair(sK14_skl(sK2_skl(sK12_skl(X1,X0)),X1,X0),sK15_skl(sK2_skl(sK12_skl(X1,X0)),X1,X0))=sK2_skl(sK12_skl(X1,X0))|sK4_skl(sK12_skl(X1,X0))=singleton(sK3_skl(sK12_skl(X1,X0))))),
% 28.37/4.11 inference(resolution,[status(thm)],[f60,f23])).
% 28.37/4.11 fof(f198,plain,(
% 28.37/4.11 ![X0,X1]: (in(sK14_skl(sK2_skl(sK12_skl(X0,X1)),X0,X1),X1)|in(sK3_skl(sK12_skl(X0,X1)),sK0_skl)|sK9_skl(X1)=sK11_skl(X1))),
% 28.37/4.11 inference(resolution,[status(thm)],[f177,f71])).
% 28.37/4.11 fof(f199,plain,(
% 28.37/4.11 ![X0,X1]: (in(sK14_skl(sK2_skl(sK12_skl(X0,X1)),X0,X1),X1)|in(sK3_skl(sK12_skl(X0,X1)),sK0_skl)|sK9_skl(X1)=sK10_skl(X1))),
% 28.37/4.11 inference(resolution,[status(thm)],[f177,f67])).
% 28.37/4.11 fof(f209,plain,(
% 28.37/4.11 ![X0,X1,X2]: (in(sK3_skl(sK12_skl(X0,sK12_skl(X1,X2))),sK0_skl)|sK9_skl(sK12_skl(X1,X2))=sK11_skl(sK12_skl(X1,X2))|sP0_prd(sK11_skl(X2),sK10_skl(X2),sK9_skl(X2),X2)|sK13_skl(sK14_skl(sK2_skl(sK12_skl(X0,sK12_skl(X1,X2))),X0,sK12_skl(X1,X2)),X1,X2)=sK14_skl(sK2_skl(sK12_skl(X0,sK12_skl(X1,X2))),X0,sK12_skl(X1,X2)))),
% 28.37/4.11 inference(resolution,[status(thm)],[f198,f59])).
% 28.37/4.11 fof(f215,plain,(
% 28.37/4.11 ![X0,X1,X2]: (in(sK3_skl(sK12_skl(X0,sK12_skl(X1,X2))),sK0_skl)|sK9_skl(sK12_skl(X1,X2))=sK10_skl(sK12_skl(X1,X2))|sP0_prd(sK11_skl(X2),sK10_skl(X2),sK9_skl(X2),X2)|sK13_skl(sK14_skl(sK2_skl(sK12_skl(X0,sK12_skl(X1,X2))),X0,sK12_skl(X1,X2)),X1,X2)=sK14_skl(sK2_skl(sK12_skl(X0,sK12_skl(X1,X2))),X0,sK12_skl(X1,X2)))),
% 28.37/4.11 inference(resolution,[status(thm)],[f199,f59])).
% 28.37/4.11 fof(f218,plain,(
% 28.37/4.11 ![X0,X1]: (in(sK2_skl(sK12_skl(X0,X1)),cartesian_product2(sK0_skl,sK1_skl))|sK9_skl(X1)=sK11_skl(X1)|~in(cartesian_product2(X1,X0),sK13_skl(sK2_skl(sK12_skl(X0,X1)),X0,X1)))),
% 28.37/4.11 inference(resolution,[status(thm)],[f146,f50])).
% 28.37/4.11 fof(f219,plain,(
% 28.37/4.11 ![X0,X1]: (in(sK2_skl(sK12_skl(X0,X1)),cartesian_product2(sK0_skl,sK1_skl))|sK9_skl(X1)=sK10_skl(X1)|~in(cartesian_product2(X1,X0),sK13_skl(sK2_skl(sK12_skl(X0,X1)),X0,X1)))),
% 28.37/4.11 inference(resolution,[status(thm)],[f147,f50])).
% 28.37/4.11 fof(f226,plain,(
% 28.37/4.11 ![X0,X1]: (in(sK13_skl(sK2_skl(sK12_skl(X0,X1)),X0,X1),cartesian_product2(X1,X0))|sK4_skl(sK12_skl(X0,X1))=singleton(sK3_skl(sK12_skl(X0,X1)))|sK9_skl(X1)=sK11_skl(X1))),
% 28.37/4.11 inference(resolution,[status(thm)],[f122,f71])).
% 28.37/4.11 fof(f227,plain,(
% 28.37/4.11 ![X0,X1]: (in(sK13_skl(sK2_skl(sK12_skl(X0,X1)),X0,X1),cartesian_product2(X1,X0))|sK4_skl(sK12_skl(X0,X1))=singleton(sK3_skl(sK12_skl(X0,X1)))|sK9_skl(X1)=sK10_skl(X1))),
% 28.37/4.11 inference(resolution,[status(thm)],[f122,f67])).
% 28.37/4.11 fof(f228,plain,(
% 28.37/4.11 ![X0,X1]: (sP0_prd(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0)|sK4_skl(sK12_skl(X1,X0))=singleton(sK3_skl(sK12_skl(X1,X0)))|~in(cartesian_product2(X0,X1),sK13_skl(sK2_skl(sK12_skl(X1,X0)),X1,X0)))),
% 28.37/4.11 inference(resolution,[status(thm)],[f122,f50])).
% 28.37/4.11 fof(f235,plain,(
% 28.37/4.11 ![X0,X1]: (sK13_skl(sK2_skl(sK12_skl(X0,X1)),X0,X1)=sK2_skl(sK12_skl(X0,X1))|in(sK2_skl(sK12_skl(X0,X1)),cartesian_product2(sK0_skl,sK1_skl))|sK9_skl(X1)=sK11_skl(X1))),
% 28.37/4.11 inference(resolution,[status(thm)],[f170,f71])).
% 28.37/4.11 fof(f255,plain,(
% 28.37/4.11 ![X0,X1]: (sK13_skl(sK2_skl(sK12_skl(X0,X1)),X0,X1)=sK2_skl(sK12_skl(X0,X1))|ordered_pair(sK3_skl(sK12_skl(X0,X1)),sK4_skl(sK12_skl(X0,X1)))=sK2_skl(sK12_skl(X0,X1))|sK9_skl(X1)=sK11_skl(X1))),
% 28.37/4.11 inference(resolution,[status(thm)],[f172,f71])).
% 28.37/4.11 fof(f256,plain,(
% 28.37/4.11 ![X0,X1]: (sK13_skl(sK2_skl(sK12_skl(X0,X1)),X0,X1)=sK2_skl(sK12_skl(X0,X1))|ordered_pair(sK3_skl(sK12_skl(X0,X1)),sK4_skl(sK12_skl(X0,X1)))=sK2_skl(sK12_skl(X0,X1))|sK9_skl(X1)=sK10_skl(X1))),
% 28.37/4.11 inference(resolution,[status(thm)],[f172,f67])).
% 28.37/4.11 fof(f257,plain,(
% 28.37/4.11 ![X0,X1]: (sK4_skl(sK12_skl(X0,X1))=singleton(sK3_skl(sK12_skl(X0,X1)))|sK9_skl(X1)=sK11_skl(X1)|~in(cartesian_product2(X1,X0),sK13_skl(sK2_skl(sK12_skl(X0,X1)),X0,X1)))),
% 28.37/4.11 inference(resolution,[status(thm)],[f226,f50])).
% 28.37/4.11 fof(f258,plain,(
% 28.37/4.11 ![X0,X1]: (sK4_skl(sK12_skl(X0,X1))=singleton(sK3_skl(sK12_skl(X0,X1)))|sK9_skl(X1)=sK10_skl(X1)|~in(cartesian_product2(X1,X0),sK13_skl(sK2_skl(sK12_skl(X0,X1)),X0,X1)))),
% 28.37/4.11 inference(resolution,[status(thm)],[f227,f50])).
% 28.37/4.11 fof(f280,plain,(
% 28.37/4.11 ![X0,X1]: (sK13_skl(sK2_skl(sK12_skl(X0,X1)),X0,X1)=sK2_skl(sK12_skl(X0,X1))|sK4_skl(sK12_skl(X0,X1))=singleton(sK3_skl(sK12_skl(X0,X1)))|sK9_skl(X1)=sK10_skl(X1))),
% 28.37/4.11 inference(resolution,[status(thm)],[f173,f67])).
% 28.37/4.11 fof(f287,plain,(
% 28.37/4.11 ![X0,X1]: (in(sK14_skl(sK2_skl(sK12_skl(X0,X1)),X0,X1),X1)|in(sK2_skl(sK12_skl(X0,X1)),cartesian_product2(sK0_skl,sK1_skl))|sK9_skl(X1)=sK11_skl(X1))),
% 28.37/4.11 inference(resolution,[status(thm)],[f176,f71])).
% 28.37/4.11 fof(f387,plain,(
% 28.37/4.11 ![X0,X1]: (in(sK14_skl(sK2_skl(sK12_skl(X0,X1)),X0,X1),X1)|ordered_pair(sK3_skl(sK12_skl(X0,X1)),sK4_skl(sK12_skl(X0,X1)))=sK2_skl(sK12_skl(X0,X1))|sK9_skl(X1)=sK11_skl(X1))),
% 28.37/4.11 inference(resolution,[status(thm)],[f178,f71])).
% 28.37/4.11 fof(f401,plain,(
% 28.37/4.11 ![X0,X1]: (in(sK14_skl(sK2_skl(sK12_skl(X0,X1)),X0,X1),X1)|sK4_skl(sK12_skl(X0,X1))=singleton(sK3_skl(sK12_skl(X0,X1)))|sK9_skl(X1)=sK11_skl(X1))),
% 28.37/4.11 inference(resolution,[status(thm)],[f179,f71])).
% 28.37/4.11 fof(f402,plain,(
% 28.37/4.11 ![X0,X1]: (in(sK14_skl(sK2_skl(sK12_skl(X0,X1)),X0,X1),X1)|sK4_skl(sK12_skl(X0,X1))=singleton(sK3_skl(sK12_skl(X0,X1)))|sK9_skl(X1)=sK10_skl(X1))),
% 28.37/4.11 inference(resolution,[status(thm)],[f179,f67])).
% 28.37/4.11 fof(f415,plain,(
% 28.37/4.11 ![X0,X1]: (sK15_skl(sK2_skl(sK12_skl(X0,X1)),X0,X1)=singleton(sK14_skl(sK2_skl(sK12_skl(X0,X1)),X0,X1))|in(sK2_skl(sK12_skl(X0,X1)),cartesian_product2(sK0_skl,sK1_skl))|sK9_skl(X1)=sK11_skl(X1))),
% 28.37/4.11 inference(resolution,[status(thm)],[f182,f71])).
% 28.37/4.11 fof(f437,plain,(
% 28.37/4.11 ![X0,X1]: (sK15_skl(sK2_skl(sK12_skl(X0,X1)),X0,X1)=singleton(sK14_skl(sK2_skl(sK12_skl(X0,X1)),X0,X1))|in(sK3_skl(sK12_skl(X0,X1)),sK0_skl)|sK9_skl(X1)=sK10_skl(X1))),
% 28.37/4.11 inference(resolution,[status(thm)],[f183,f67])).
% 28.37/4.11 fof(f459,plain,(
% 28.37/4.11 ![X0,X1]: (sK15_skl(sK2_skl(sK12_skl(X0,X1)),X0,X1)=singleton(sK14_skl(sK2_skl(sK12_skl(X0,X1)),X0,X1))|ordered_pair(sK3_skl(sK12_skl(X0,X1)),sK4_skl(sK12_skl(X0,X1)))=sK2_skl(sK12_skl(X0,X1))|sK9_skl(X1)=sK11_skl(X1))),
% 28.37/4.11 inference(resolution,[status(thm)],[f184,f71])).
% 28.37/4.11 fof(f460,plain,(
% 28.37/4.11 ![X0,X1]: (sK15_skl(sK2_skl(sK12_skl(X0,X1)),X0,X1)=singleton(sK14_skl(sK2_skl(sK12_skl(X0,X1)),X0,X1))|ordered_pair(sK3_skl(sK12_skl(X0,X1)),sK4_skl(sK12_skl(X0,X1)))=sK2_skl(sK12_skl(X0,X1))|sK9_skl(X1)=sK10_skl(X1))),
% 28.37/4.11 inference(resolution,[status(thm)],[f184,f67])).
% 28.37/4.11 fof(f467,plain,(
% 28.37/4.11 ![X0,X1]: (sK15_skl(sK2_skl(sK12_skl(X0,X1)),X0,X1)=singleton(sK14_skl(sK2_skl(sK12_skl(X0,X1)),X0,X1))|sK4_skl(sK12_skl(X0,X1))=singleton(sK3_skl(sK12_skl(X0,X1)))|sK9_skl(X1)=sK11_skl(X1))),
% 28.37/4.11 inference(resolution,[status(thm)],[f185,f71])).
% 28.37/4.11 fof(f468,plain,(
% 28.37/4.11 ![X0,X1]: (sK15_skl(sK2_skl(sK12_skl(X0,X1)),X0,X1)=singleton(sK14_skl(sK2_skl(sK12_skl(X0,X1)),X0,X1))|sK4_skl(sK12_skl(X0,X1))=singleton(sK3_skl(sK12_skl(X0,X1)))|sK9_skl(X1)=sK10_skl(X1))),
% 28.37/4.11 inference(resolution,[status(thm)],[f185,f67])).
% 28.37/4.11 fof(f487,plain,(
% 28.37/4.11 ![X0,X1]: (ordered_pair(sK3_skl(sK12_skl(X0,X1)),sK4_skl(sK12_skl(X0,X1)))=sK2_skl(sK12_skl(X0,X1))|sK9_skl(X1)=sK11_skl(X1)|~in(cartesian_product2(X1,X0),sK13_skl(sK2_skl(sK12_skl(X0,X1)),X0,X1)))),
% 28.37/4.11 inference(resolution,[status(thm)],[f155,f50])).
% 28.37/4.11 fof(f491,plain,(
% 28.37/4.11 ![X0,X1]: (ordered_pair(sK3_skl(sK12_skl(X0,X1)),sK4_skl(sK12_skl(X0,X1)))=sK2_skl(sK12_skl(X0,X1))|sK9_skl(X1)=sK10_skl(X1)|~in(cartesian_product2(X1,X0),sK13_skl(sK2_skl(sK12_skl(X0,X1)),X0,X1)))),
% 28.37/4.11 inference(resolution,[status(thm)],[f156,f50])).
% 28.37/4.11 fof(f506,plain,(
% 28.37/4.11 ![X0,X1]: (ordered_pair(sK14_skl(sK2_skl(sK12_skl(X0,X1)),X0,X1),sK15_skl(sK2_skl(sK12_skl(X0,X1)),X0,X1))=sK2_skl(sK12_skl(X0,X1))|in(sK2_skl(sK12_skl(X0,X1)),cartesian_product2(sK0_skl,sK1_skl))|sK9_skl(X1)=sK11_skl(X1))),
% 28.37/4.11 inference(resolution,[status(thm)],[f188,f71])).
% 28.37/4.11 fof(f516,plain,(
% 28.37/4.11 ![X0,X1]: (ordered_pair(sK14_skl(sK2_skl(sK12_skl(X0,X1)),X0,X1),sK15_skl(sK2_skl(sK12_skl(X0,X1)),X0,X1))=sK2_skl(sK12_skl(X0,X1))|in(sK3_skl(sK12_skl(X0,X1)),sK0_skl)|sK9_skl(X1)=sK10_skl(X1))),
% 28.37/4.11 inference(resolution,[status(thm)],[f189,f67])).
% 28.37/4.11 fof(f524,plain,(
% 28.37/4.11 ![X0,X1]: (ordered_pair(sK14_skl(sK2_skl(sK12_skl(X0,X1)),X0,X1),sK15_skl(sK2_skl(sK12_skl(X0,X1)),X0,X1))=sK2_skl(sK12_skl(X0,X1))|ordered_pair(sK3_skl(sK12_skl(X0,X1)),sK4_skl(sK12_skl(X0,X1)))=sK2_skl(sK12_skl(X0,X1))|sK9_skl(X1)=sK11_skl(X1))),
% 28.37/4.11 inference(resolution,[status(thm)],[f190,f71])).
% 28.37/4.11 fof(f525,plain,(
% 28.37/4.11 ![X0,X1]: (ordered_pair(sK14_skl(sK2_skl(sK12_skl(X0,X1)),X0,X1),sK15_skl(sK2_skl(sK12_skl(X0,X1)),X0,X1))=sK2_skl(sK12_skl(X0,X1))|ordered_pair(sK3_skl(sK12_skl(X0,X1)),sK4_skl(sK12_skl(X0,X1)))=sK2_skl(sK12_skl(X0,X1))|sK9_skl(X1)=sK10_skl(X1))),
% 28.37/4.11 inference(resolution,[status(thm)],[f190,f67])).
% 28.37/4.11 fof(f571,plain,(
% 28.37/4.11 ![X0,X1]: (ordered_pair(sK14_skl(sK2_skl(sK12_skl(X0,X1)),X0,X1),sK15_skl(sK2_skl(sK12_skl(X0,X1)),X0,X1))=sK2_skl(sK12_skl(X0,X1))|sK4_skl(sK12_skl(X0,X1))=singleton(sK3_skl(sK12_skl(X0,X1)))|sK9_skl(X1)=sK11_skl(X1))),
% 28.37/4.11 inference(resolution,[status(thm)],[f191,f71])).
% 28.37/4.11 fof(f588,plain,(
% 28.37/4.11 ![X0,X1,X2]: (~in(sK2_skl(X0),X0)|~in(sK2_skl(X0),cartesian_product2(sK0_skl,sK1_skl))|~ordered_pair(sK14_skl(sK2_skl(sK12_skl(X1,X2)),X1,X2),sK15_skl(sK2_skl(sK12_skl(X1,X2)),X1,X2))=sK2_skl(X0)|~in(sK14_skl(sK2_skl(sK12_skl(X1,X2)),X1,X2),sK0_skl)|sK4_skl(sK12_skl(X1,X2))=singleton(sK3_skl(sK12_skl(X1,X2)))|sK9_skl(X2)=sK11_skl(X2))),
% 28.37/4.11 inference(paramodulation,[status(thm)],[f467,f77])).
% 28.37/4.11 fof(f2070,plain,(
% 28.37/4.11 ![X0,X1]: (~in(sK2_skl(sK12_skl(X0,X1)),sK12_skl(X0,X1))|~in(sK2_skl(sK12_skl(X0,X1)),cartesian_product2(sK0_skl,sK1_skl))|~in(sK14_skl(sK2_skl(sK12_skl(X0,X1)),X0,X1),sK0_skl)|sK4_skl(sK12_skl(X0,X1))=singleton(sK3_skl(sK12_skl(X0,X1)))|sK9_skl(X1)=sK11_skl(X1)|sK4_skl(sK12_skl(X0,X1))=singleton(sK3_skl(sK12_skl(X0,X1)))|sK9_skl(X1)=sK11_skl(X1))),
% 28.37/4.11 inference(resolution,[status(thm)],[f588,f571])).
% 28.37/4.11 fof(f2100,plain,(
% 28.37/4.11 ![X0,X1]: (~in(sK2_skl(sK12_skl(X0,X1)),sK12_skl(X0,X1))|~in(sK2_skl(sK12_skl(X0,X1)),cartesian_product2(sK0_skl,sK1_skl))|~in(sK14_skl(sK2_skl(sK12_skl(X0,X1)),X0,X1),sK0_skl)|sK4_skl(sK12_skl(X0,X1))=singleton(sK3_skl(sK12_skl(X0,X1)))|sK9_skl(X1)=sK11_skl(X1))),
% 28.37/4.11 inference(duplicate_literals_removal,[status(thm)],[f2070])).
% 28.37/4.11 fof(f2101,plain,(
% 28.37/4.11 ![X0,X1]: (~in(sK2_skl(sK12_skl(X0,X1)),cartesian_product2(sK0_skl,sK1_skl))|~in(sK14_skl(sK2_skl(sK12_skl(X0,X1)),X0,X1),sK0_skl)|sK4_skl(sK12_skl(X0,X1))=singleton(sK3_skl(sK12_skl(X0,X1)))|sK9_skl(X1)=sK11_skl(X1))),
% 28.37/4.11 inference(forward_subsumption_resolution,[status(thm)],[f2100,f23])).
% 28.37/4.11 fof(f2132,plain,(
% 28.37/4.11 ![X0]: (~in(sK2_skl(sK12_skl(X0,sK0_skl)),cartesian_product2(sK0_skl,sK1_skl))|sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))|sK9_skl(sK0_skl)=sK11_skl(sK0_skl)|ordered_pair(sK3_skl(sK12_skl(X0,sK0_skl)),sK4_skl(sK12_skl(X0,sK0_skl)))=sK2_skl(sK12_skl(X0,sK0_skl))|sK9_skl(sK0_skl)=sK11_skl(sK0_skl))),
% 28.37/4.11 inference(resolution,[status(thm)],[f2101,f387])).
% 28.37/4.11 fof(f2134,plain,(
% 28.37/4.11 ![X0]: (~in(sK2_skl(sK12_skl(X0,sK0_skl)),cartesian_product2(sK0_skl,sK1_skl))|sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))|sK9_skl(sK0_skl)=sK11_skl(sK0_skl)|sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))|sK9_skl(sK0_skl)=sK11_skl(sK0_skl))),
% 28.37/4.11 inference(resolution,[status(thm)],[f2101,f401])).
% 28.37/4.11 fof(f2139,plain,(
% 28.37/4.11 ![X0]: (~in(sK2_skl(sK12_skl(X0,sK0_skl)),cartesian_product2(sK0_skl,sK1_skl))|sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))|sK9_skl(sK0_skl)=sK11_skl(sK0_skl)|in(sK2_skl(sK12_skl(X0,sK0_skl)),cartesian_product2(sK0_skl,sK1_skl))|sK9_skl(sK0_skl)=sK11_skl(sK0_skl))),
% 28.37/4.11 inference(resolution,[status(thm)],[f2101,f287])).
% 28.37/4.11 fof(f2143,plain,(
% 28.37/4.11 ![X0]: (~in(sK2_skl(sK12_skl(X0,sK0_skl)),cartesian_product2(sK0_skl,sK1_skl))|sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))|sK9_skl(sK0_skl)=sK11_skl(sK0_skl)|in(sK3_skl(sK12_skl(X0,sK0_skl)),sK0_skl)|sK9_skl(sK0_skl)=sK11_skl(sK0_skl))),
% 28.37/4.11 inference(resolution,[status(thm)],[f2101,f198])).
% 28.37/4.11 fof(f2145,definition,(
% 28.37/4.11 ![X0]: (sQ6_spl <=> (~in(sK2_skl(sK12_skl(X0,sK0_skl)),cartesian_product2(sK0_skl,sK1_skl))|sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))|ordered_pair(sK3_skl(sK12_skl(X0,sK0_skl)),sK4_skl(sK12_skl(X0,sK0_skl)))=sK2_skl(sK12_skl(X0,sK0_skl))))),
% 28.37/4.11 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 28.37/4.11 fof(f2148,definition,(
% 28.37/4.11 sQ7_spl <=> (sK9_skl(sK0_skl)=sK11_skl(sK0_skl))),
% 28.37/4.11 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 28.37/4.11 fof(f2149,plain,(
% 28.37/4.11 sK9_skl(sK0_skl)=sK11_skl(sK0_skl)|~sQ7_spl),
% 28.37/4.11 inference(component_clause,[status(thm)],[f2148])).
% 28.37/4.11 fof(f2167,definition,(
% 28.37/4.11 ![X0]: (sQ12_spl <=> (~in(sK2_skl(sK12_skl(X0,sK0_skl)),cartesian_product2(sK0_skl,sK1_skl))|sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))|sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))))),
% 28.37/4.11 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 28.37/4.11 fof(f2168,plain,(
% 28.37/4.11 ![X0]: (~in(sK2_skl(sK12_skl(X0,sK0_skl)),cartesian_product2(sK0_skl,sK1_skl))|sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))|sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))|~sQ12_spl)),
% 28.37/4.11 inference(component_clause,[status(thm)],[f2167])).
% 28.37/4.11 fof(f2172,definition,(
% 28.37/4.11 ![X0]: (sQ13_spl <=> (~in(sK2_skl(sK12_skl(X0,sK0_skl)),cartesian_product2(sK0_skl,sK1_skl))|sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))|in(sK2_skl(sK12_skl(X0,sK0_skl)),cartesian_product2(sK0_skl,sK1_skl))))),
% 28.37/4.11 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 28.37/4.11 fof(f2181,definition,(
% 28.37/4.11 ![X0]: (sQ14_spl <=> (~in(sK2_skl(sK12_skl(X0,sK0_skl)),cartesian_product2(sK0_skl,sK1_skl))|sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))|in(sK3_skl(sK12_skl(X0,sK0_skl)),sK0_skl)))),
% 28.37/4.11 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 28.37/4.11 fof(f2200,definition,(
% 28.37/4.11 sQ17_spl <=> (sK9_skl(sK0_skl)=sK10_skl(sK0_skl))),
% 28.37/4.11 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 28.37/4.11 fof(f2201,plain,(
% 28.37/4.11 sK9_skl(sK0_skl)=sK10_skl(sK0_skl)|~sQ17_spl),
% 28.37/4.11 inference(component_clause,[status(thm)],[f2200])).
% 28.37/4.11 fof(f2204,plain,(
% 28.37/4.11 sQ6_spl|sQ7_spl),
% 28.37/4.11 inference(split_clause,[status(thm)],[f2132,f2145,f2148])).
% 28.37/4.11 fof(f2206,plain,(
% 28.37/4.11 sQ12_spl|sQ7_spl),
% 28.37/4.11 inference(split_clause,[status(thm)],[f2134,f2167,f2148])).
% 28.37/4.11 fof(f2207,definition,(
% 28.37/4.11 sQ18_spl <=> (sP0_prd(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl))),
% 28.37/4.11 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 28.37/4.11 fof(f2208,plain,(
% 28.37/4.11 sP0_prd(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl)|~sQ18_spl),
% 28.37/4.11 inference(component_clause,[status(thm)],[f2207])).
% 28.37/4.11 fof(f2209,plain,(
% 28.37/4.11 ~sP0_prd(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl)|sQ18_spl),
% 28.37/4.11 inference(component_clause,[status(thm)],[f2207])).
% 28.37/4.11 fof(f2214,plain,(
% 28.37/4.11 sQ13_spl|sQ7_spl),
% 28.37/4.11 inference(split_clause,[status(thm)],[f2139,f2172,f2148])).
% 28.37/4.11 fof(f2218,plain,(
% 28.37/4.11 sQ14_spl|sQ7_spl),
% 28.37/4.11 inference(split_clause,[status(thm)],[f2143,f2181,f2148])).
% 28.37/4.11 fof(f2220,plain,(
% 28.37/4.11 ![X0,X1]: (in(sK3_skl(sK12_skl(X0,sK12_skl(X1,sK0_skl))),sK0_skl)|sK9_skl(sK12_skl(X1,sK0_skl))=sK10_skl(sK12_skl(X1,sK0_skl))|sP0_prd(sK9_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl)|sK13_skl(sK14_skl(sK2_skl(sK12_skl(X0,sK12_skl(X1,sK0_skl))),X0,sK12_skl(X1,sK0_skl)),X1,sK0_skl)=sK14_skl(sK2_skl(sK12_skl(X0,sK12_skl(X1,sK0_skl))),X0,sK12_skl(X1,sK0_skl))|~sQ7_spl)),
% 28.37/4.11 inference(paramodulation,[status(thm)],[f2149,f215])).
% 28.37/4.11 fof(f2221,plain,(
% 28.37/4.11 ![X0,X1]: (in(sK3_skl(sK12_skl(X0,sK12_skl(X1,sK0_skl))),sK0_skl)|sK9_skl(sK12_skl(X1,sK0_skl))=sK11_skl(sK12_skl(X1,sK0_skl))|sP0_prd(sK9_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl)|sK13_skl(sK14_skl(sK2_skl(sK12_skl(X0,sK12_skl(X1,sK0_skl))),X0,sK12_skl(X1,sK0_skl)),X1,sK0_skl)=sK14_skl(sK2_skl(sK12_skl(X0,sK12_skl(X1,sK0_skl))),X0,sK12_skl(X1,sK0_skl))|~sQ7_spl)),
% 28.37/4.11 inference(paramodulation,[status(thm)],[f2149,f209])).
% 28.37/4.11 fof(f2287,plain,(
% 28.37/4.11 ![X0]: (sP0_prd(sK9_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl)|ordered_pair(sK14_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl),sK15_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl))=sK2_skl(sK12_skl(X0,sK0_skl))|sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))|~sQ7_spl)),
% 28.37/4.11 inference(paramodulation,[status(thm)],[f2149,f191])).
% 28.37/4.11 fof(f2291,plain,(
% 28.37/4.11 ![X0]: (sP0_prd(sK9_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl)|ordered_pair(sK14_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl),sK15_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl))=sK2_skl(sK12_skl(X0,sK0_skl))|ordered_pair(sK3_skl(sK12_skl(X0,sK0_skl)),sK4_skl(sK12_skl(X0,sK0_skl)))=sK2_skl(sK12_skl(X0,sK0_skl))|~sQ7_spl)),
% 28.37/4.11 inference(paramodulation,[status(thm)],[f2149,f190])).
% 28.37/4.11 fof(f2292,plain,(
% 28.37/4.11 ![X0]: (sP0_prd(sK9_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl)|ordered_pair(sK14_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl),sK15_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl))=sK2_skl(sK12_skl(X0,sK0_skl))|in(sK3_skl(sK12_skl(X0,sK0_skl)),sK0_skl)|~sQ7_spl)),
% 28.37/4.11 inference(paramodulation,[status(thm)],[f2149,f189])).
% 28.37/4.11 fof(f2293,plain,(
% 28.37/4.11 ![X0]: (sP0_prd(sK9_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl)|ordered_pair(sK14_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl),sK15_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl))=sK2_skl(sK12_skl(X0,sK0_skl))|in(sK2_skl(sK12_skl(X0,sK0_skl)),cartesian_product2(sK0_skl,sK1_skl))|~sQ7_spl)),
% 28.37/4.11 inference(paramodulation,[status(thm)],[f2149,f188])).
% 28.37/4.11 fof(f2299,plain,(
% 28.37/4.11 ![X0]: (sP0_prd(sK9_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl)|sK15_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl)=singleton(sK14_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl))|sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))|~sQ7_spl)),
% 28.37/4.11 inference(paramodulation,[status(thm)],[f2149,f185])).
% 28.37/4.11 fof(f2300,plain,(
% 28.37/4.11 ![X0]: (sP0_prd(sK9_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl)|sK15_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl)=singleton(sK14_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl))|ordered_pair(sK3_skl(sK12_skl(X0,sK0_skl)),sK4_skl(sK12_skl(X0,sK0_skl)))=sK2_skl(sK12_skl(X0,sK0_skl))|~sQ7_spl)),
% 28.37/4.11 inference(paramodulation,[status(thm)],[f2149,f184])).
% 28.37/4.11 fof(f2301,plain,(
% 28.37/4.11 ![X0]: (sP0_prd(sK9_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl)|sK15_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl)=singleton(sK14_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl))|in(sK3_skl(sK12_skl(X0,sK0_skl)),sK0_skl)|~sQ7_spl)),
% 28.37/4.11 inference(paramodulation,[status(thm)],[f2149,f183])).
% 28.37/4.11 fof(f2303,plain,(
% 28.37/4.11 ![X0]: (sP0_prd(sK9_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl)|sK15_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl)=singleton(sK14_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl))|in(sK2_skl(sK12_skl(X0,sK0_skl)),cartesian_product2(sK0_skl,sK1_skl))|~sQ7_spl)),
% 28.37/4.11 inference(paramodulation,[status(thm)],[f2149,f182])).
% 28.37/4.11 fof(f2304,plain,(
% 28.37/4.11 ![X0]: (sP0_prd(sK9_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl)|in(sK14_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl),sK0_skl)|sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))|~sQ7_spl)),
% 28.37/4.11 inference(paramodulation,[status(thm)],[f2149,f179])).
% 28.37/4.11 fof(f2305,plain,(
% 28.37/4.11 ![X0]: (sP0_prd(sK9_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl)|in(sK14_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl),sK0_skl)|ordered_pair(sK3_skl(sK12_skl(X0,sK0_skl)),sK4_skl(sK12_skl(X0,sK0_skl)))=sK2_skl(sK12_skl(X0,sK0_skl))|~sQ7_spl)),
% 28.37/4.11 inference(paramodulation,[status(thm)],[f2149,f178])).
% 28.37/4.11 fof(f2308,plain,(
% 28.37/4.11 ![X0]: (sP0_prd(sK9_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl)|in(sK14_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl),sK0_skl)|in(sK2_skl(sK12_skl(X0,sK0_skl)),cartesian_product2(sK0_skl,sK1_skl))|~sQ7_spl)),
% 28.37/4.11 inference(paramodulation,[status(thm)],[f2149,f176])).
% 28.37/4.11 fof(f2309,plain,(
% 28.37/4.11 ![X0]: (sP0_prd(sK9_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl)|sK13_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl)=sK2_skl(sK12_skl(X0,sK0_skl))|sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))|~sQ7_spl)),
% 28.37/4.11 inference(paramodulation,[status(thm)],[f2149,f173])).
% 28.37/4.11 fof(f2311,plain,(
% 28.37/4.11 ![X0]: (sP0_prd(sK9_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl)|sK13_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl)=sK2_skl(sK12_skl(X0,sK0_skl))|ordered_pair(sK3_skl(sK12_skl(X0,sK0_skl)),sK4_skl(sK12_skl(X0,sK0_skl)))=sK2_skl(sK12_skl(X0,sK0_skl))|~sQ7_spl)),
% 28.37/4.11 inference(paramodulation,[status(thm)],[f2149,f172])).
% 28.37/4.11 fof(f2312,plain,(
% 28.37/4.11 ![X0]: (sP0_prd(sK9_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl)|sK13_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl)=sK2_skl(sK12_skl(X0,sK0_skl))|in(sK3_skl(sK12_skl(X0,sK0_skl)),sK0_skl)|~sQ7_spl)),
% 28.37/4.11 inference(paramodulation,[status(thm)],[f2149,f171])).
% 28.37/4.11 fof(f2313,plain,(
% 28.37/4.11 ![X0]: (sP0_prd(sK9_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl)|sK13_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl)=sK2_skl(sK12_skl(X0,sK0_skl))|in(sK2_skl(sK12_skl(X0,sK0_skl)),cartesian_product2(sK0_skl,sK1_skl))|~sQ7_spl)),
% 28.37/4.11 inference(paramodulation,[status(thm)],[f2149,f170])).
% 28.37/4.11 fof(f2314,plain,(
% 28.37/4.11 ![X0]: (sP0_prd(sK9_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl)|in(sK13_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl),cartesian_product2(sK0_skl,X0))|sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))|~sQ7_spl)),
% 28.37/4.11 inference(paramodulation,[status(thm)],[f2149,f122])).
% 28.37/4.11 fof(f2315,plain,(
% 28.37/4.11 ![X0]: (sP0_prd(sK9_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl)|in(sK14_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl),sK0_skl)|in(sK3_skl(sK12_skl(X0,sK0_skl)),sK0_skl)|~sQ7_spl)),
% 28.37/4.11 inference(paramodulation,[status(thm)],[f2149,f177])).
% 28.37/4.11 fof(f2316,plain,(
% 28.37/4.11 ![X0]: (sP0_prd(sK9_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl)|in(sK13_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl),cartesian_product2(sK0_skl,X0))|ordered_pair(sK3_skl(sK12_skl(X0,sK0_skl)),sK4_skl(sK12_skl(X0,sK0_skl)))=sK2_skl(sK12_skl(X0,sK0_skl))|~sQ7_spl)),
% 28.37/4.11 inference(paramodulation,[status(thm)],[f2149,f121])).
% 28.37/4.11 fof(f2317,plain,(
% 28.37/4.11 ![X0]: (sP0_prd(sK9_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl)|in(sK13_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl),cartesian_product2(sK0_skl,X0))|in(sK2_skl(sK12_skl(X0,sK0_skl)),cartesian_product2(sK0_skl,sK1_skl))|~sQ7_spl)),
% 28.37/4.11 inference(paramodulation,[status(thm)],[f2149,f119])).
% 28.37/4.11 fof(f2321,plain,(
% 28.37/4.11 ![X0]: (sP0_prd(sK9_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl)|in(sK13_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl),cartesian_product2(sK0_skl,X0))|in(sK3_skl(sK12_skl(X0,sK0_skl)),sK0_skl)|~sQ7_spl)),
% 28.37/4.11 inference(paramodulation,[status(thm)],[f2149,f120])).
% 28.37/4.11 fof(f2322,definition,(
% 28.37/4.11 ![X0,X1]: (sQ19_spl <=> (in(sK3_skl(sK12_skl(X0,sK12_skl(X1,sK0_skl))),sK0_skl)|sK9_skl(sK12_skl(X1,sK0_skl))=sK10_skl(sK12_skl(X1,sK0_skl))|sK13_skl(sK14_skl(sK2_skl(sK12_skl(X0,sK12_skl(X1,sK0_skl))),X0,sK12_skl(X1,sK0_skl)),X1,sK0_skl)=sK14_skl(sK2_skl(sK12_skl(X0,sK12_skl(X1,sK0_skl))),X0,sK12_skl(X1,sK0_skl))))),
% 29.21/4.11 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 29.21/4.11 fof(f2325,definition,(
% 29.21/4.11 sQ20_spl <=> (sP0_prd(sK9_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl))),
% 29.21/4.11 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 29.21/4.11 fof(f2326,plain,(
% 29.21/4.11 sP0_prd(sK9_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl)|~sQ20_spl),
% 29.21/4.11 inference(component_clause,[status(thm)],[f2325])).
% 29.21/4.11 fof(f2328,plain,(
% 29.21/4.11 sQ19_spl|sQ20_spl|~sQ7_spl),
% 29.21/4.11 inference(split_clause,[status(thm)],[f2220,f2322,f2325,f2148])).
% 29.21/4.11 fof(f2329,definition,(
% 29.21/4.11 ![X0,X1]: (sQ21_spl <=> (in(sK3_skl(sK12_skl(X0,sK12_skl(X1,sK0_skl))),sK0_skl)|sK9_skl(sK12_skl(X1,sK0_skl))=sK11_skl(sK12_skl(X1,sK0_skl))|sK13_skl(sK14_skl(sK2_skl(sK12_skl(X0,sK12_skl(X1,sK0_skl))),X0,sK12_skl(X1,sK0_skl)),X1,sK0_skl)=sK14_skl(sK2_skl(sK12_skl(X0,sK12_skl(X1,sK0_skl))),X0,sK12_skl(X1,sK0_skl))))),
% 29.21/4.11 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 29.21/4.11 fof(f2332,plain,(
% 29.21/4.11 sQ21_spl|sQ20_spl|~sQ7_spl),
% 29.21/4.11 inference(split_clause,[status(thm)],[f2221,f2329,f2325,f2148])).
% 29.21/4.11 fof(f2333,definition,(
% 29.21/4.11 ![X0]: (sQ22_spl <=> (ordered_pair(sK14_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl),sK15_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl))=sK2_skl(sK12_skl(X0,sK0_skl))|ordered_pair(sK3_skl(sK12_skl(X0,sK0_skl)),sK4_skl(sK12_skl(X0,sK0_skl)))=sK2_skl(sK12_skl(X0,sK0_skl))))),
% 29.21/4.11 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 29.21/4.11 fof(f2352,definition,(
% 29.21/4.11 ![X0]: (sQ27_spl <=> (ordered_pair(sK14_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl),sK15_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl))=sK2_skl(sK12_skl(X0,sK0_skl))|sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))))),
% 29.21/4.11 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 29.21/4.11 fof(f2353,plain,(
% 29.21/4.11 ![X0]: (ordered_pair(sK14_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl),sK15_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl))=sK2_skl(sK12_skl(X0,sK0_skl))|sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))|~sQ27_spl)),
% 29.21/4.11 inference(component_clause,[status(thm)],[f2352])).
% 29.21/4.11 fof(f2357,definition,(
% 29.21/4.11 ![X0]: (sQ28_spl <=> (ordered_pair(sK14_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl),sK15_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl))=sK2_skl(sK12_skl(X0,sK0_skl))|in(sK2_skl(sK12_skl(X0,sK0_skl)),cartesian_product2(sK0_skl,sK1_skl))))),
% 29.21/4.11 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 29.21/4.11 fof(f2362,definition,(
% 29.21/4.11 ![X0]: (sQ29_spl <=> (sK15_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl)=singleton(sK14_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl))|ordered_pair(sK3_skl(sK12_skl(X0,sK0_skl)),sK4_skl(sK12_skl(X0,sK0_skl)))=sK2_skl(sK12_skl(X0,sK0_skl))))),
% 29.21/4.11 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 29.21/4.11 fof(f2373,definition,(
% 29.21/4.11 ![X0]: (sQ30_spl <=> (ordered_pair(sK14_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl),sK15_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl))=sK2_skl(sK12_skl(X0,sK0_skl))|in(sK3_skl(sK12_skl(X0,sK0_skl)),sK0_skl)))),
% 29.21/4.11 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 29.21/4.11 fof(f2380,definition,(
% 29.21/4.11 ![X0]: (sQ31_spl <=> (sK15_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl)=singleton(sK14_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl))|sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))))),
% 29.21/4.11 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 29.21/4.11 fof(f2381,plain,(
% 29.21/4.11 ![X0]: (sK15_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl)=singleton(sK14_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl))|sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))|~sQ31_spl)),
% 29.21/4.11 inference(component_clause,[status(thm)],[f2380])).
% 29.21/4.11 fof(f2385,definition,(
% 29.21/4.11 ![X0]: (sQ32_spl <=> (sK15_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl)=singleton(sK14_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl))|in(sK2_skl(sK12_skl(X0,sK0_skl)),cartesian_product2(sK0_skl,sK1_skl))))),
% 29.21/4.11 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 29.21/4.11 fof(f2390,definition,(
% 29.21/4.11 ![X0]: (sQ33_spl <=> (sK13_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl)=sK2_skl(sK12_skl(X0,sK0_skl))|ordered_pair(sK3_skl(sK12_skl(X0,sK0_skl)),sK4_skl(sK12_skl(X0,sK0_skl)))=sK2_skl(sK12_skl(X0,sK0_skl))))),
% 29.21/4.11 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 29.21/4.11 fof(f2395,definition,(
% 29.21/4.11 ![X0]: (sQ34_spl <=> (in(sK13_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl),cartesian_product2(sK0_skl,X0))|ordered_pair(sK3_skl(sK12_skl(X0,sK0_skl)),sK4_skl(sK12_skl(X0,sK0_skl)))=sK2_skl(sK12_skl(X0,sK0_skl))))),
% 29.21/4.11 introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition])).
% 29.21/4.11 fof(f2408,definition,(
% 29.21/4.11 ![X0]: (sQ35_spl <=> (in(sK14_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl),sK0_skl)|ordered_pair(sK3_skl(sK12_skl(X0,sK0_skl)),sK4_skl(sK12_skl(X0,sK0_skl)))=sK2_skl(sK12_skl(X0,sK0_skl))))),
% 29.21/4.11 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 29.21/4.11 fof(f2415,definition,(
% 29.21/4.11 ![X0]: (sQ36_spl <=> (sK15_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl)=singleton(sK14_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl))|in(sK3_skl(sK12_skl(X0,sK0_skl)),sK0_skl)))),
% 29.21/4.11 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 29.21/4.11 fof(f2422,definition,(
% 29.21/4.11 ![X0]: (sQ37_spl <=> (sK13_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl)=sK2_skl(sK12_skl(X0,sK0_skl))|sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))))),
% 29.21/4.11 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 29.21/4.11 fof(f2423,plain,(
% 29.21/4.11 ![X0]: (sK13_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl)=sK2_skl(sK12_skl(X0,sK0_skl))|sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))|~sQ37_spl)),
% 29.21/4.11 inference(component_clause,[status(thm)],[f2422])).
% 29.21/4.11 fof(f2427,definition,(
% 29.21/4.11 ![X0]: (sQ38_spl <=> (sK13_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl)=sK2_skl(sK12_skl(X0,sK0_skl))|in(sK2_skl(sK12_skl(X0,sK0_skl)),cartesian_product2(sK0_skl,sK1_skl))))),
% 29.21/4.11 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 29.21/4.11 fof(f2432,definition,(
% 29.21/4.11 ![X0]: (sQ39_spl <=> (in(sK13_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl),cartesian_product2(sK0_skl,X0))|sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))))),
% 29.21/4.11 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 29.21/4.11 fof(f2437,definition,(
% 29.21/4.11 ![X0]: (sQ40_spl <=> (in(sK13_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl),cartesian_product2(sK0_skl,X0))|in(sK2_skl(sK12_skl(X0,sK0_skl)),cartesian_product2(sK0_skl,sK1_skl))))),
% 29.21/4.11 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 29.21/4.11 fof(f2450,definition,(
% 29.21/4.11 ![X0]: (sQ41_spl <=> (in(sK14_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl),sK0_skl)|sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))))),
% 29.21/4.11 introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 29.21/4.11 fof(f2455,definition,(
% 29.21/4.11 ![X0]: (sQ42_spl <=> (in(sK14_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl),sK0_skl)|in(sK2_skl(sK12_skl(X0,sK0_skl)),cartesian_product2(sK0_skl,sK1_skl))))),
% 29.21/4.11 introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition])).
% 29.21/4.11 fof(f2461,plain,(
% 29.21/4.11 sQ20_spl|sQ27_spl|~sQ7_spl),
% 29.21/4.11 inference(split_clause,[status(thm)],[f2287,f2325,f2352,f2148])).
% 29.21/4.11 fof(f2465,plain,(
% 29.21/4.11 sQ20_spl|sQ22_spl|~sQ7_spl),
% 29.21/4.11 inference(split_clause,[status(thm)],[f2291,f2325,f2333,f2148])).
% 29.21/4.11 fof(f2466,plain,(
% 29.21/4.11 sQ20_spl|sQ30_spl|~sQ7_spl),
% 29.21/4.11 inference(split_clause,[status(thm)],[f2292,f2325,f2373,f2148])).
% 29.21/4.11 fof(f2467,plain,(
% 29.21/4.11 sQ20_spl|sQ28_spl|~sQ7_spl),
% 29.21/4.11 inference(split_clause,[status(thm)],[f2293,f2325,f2357,f2148])).
% 29.21/4.11 fof(f2468,definition,(
% 29.21/4.11 ![X0]: (sQ43_spl <=> (sK13_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl)=sK2_skl(sK12_skl(X0,sK0_skl))|in(sK3_skl(sK12_skl(X0,sK0_skl)),sK0_skl)))),
% 29.21/4.11 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 29.21/4.11 fof(f2475,definition,(
% 29.21/4.11 ![X0]: (sQ44_spl <=> (in(sK13_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl),cartesian_product2(sK0_skl,X0))|in(sK3_skl(sK12_skl(X0,sK0_skl)),sK0_skl)))),
% 29.21/4.11 introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 29.21/4.11 fof(f2479,plain,(
% 29.21/4.11 sQ20_spl|sQ31_spl|~sQ7_spl),
% 29.21/4.11 inference(split_clause,[status(thm)],[f2299,f2325,f2380,f2148])).
% 29.21/4.11 fof(f2480,plain,(
% 29.21/4.11 sQ20_spl|sQ29_spl|~sQ7_spl),
% 29.21/4.11 inference(split_clause,[status(thm)],[f2300,f2325,f2362,f2148])).
% 29.21/4.11 fof(f2481,plain,(
% 29.21/4.11 sQ20_spl|sQ36_spl|~sQ7_spl),
% 29.21/4.11 inference(split_clause,[status(thm)],[f2301,f2325,f2415,f2148])).
% 29.21/4.11 fof(f2482,definition,(
% 29.21/4.11 ![X0]: (sQ45_spl <=> (in(sK14_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl),sK0_skl)|in(sK3_skl(sK12_skl(X0,sK0_skl)),sK0_skl)))),
% 29.21/4.11 introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 29.21/4.11 fof(f2486,plain,(
% 29.21/4.11 sQ20_spl|sQ32_spl|~sQ7_spl),
% 29.21/4.11 inference(split_clause,[status(thm)],[f2303,f2325,f2385,f2148])).
% 29.21/4.11 fof(f2487,plain,(
% 29.21/4.11 sQ20_spl|sQ41_spl|~sQ7_spl),
% 29.21/4.11 inference(split_clause,[status(thm)],[f2304,f2325,f2450,f2148])).
% 29.21/4.11 fof(f2488,plain,(
% 29.21/4.11 sQ20_spl|sQ35_spl|~sQ7_spl),
% 29.21/4.11 inference(split_clause,[status(thm)],[f2305,f2325,f2408,f2148])).
% 29.21/4.11 fof(f2491,plain,(
% 29.21/4.11 sQ20_spl|sQ42_spl|~sQ7_spl),
% 29.21/4.11 inference(split_clause,[status(thm)],[f2308,f2325,f2455,f2148])).
% 29.21/4.11 fof(f2492,plain,(
% 29.21/4.11 sQ20_spl|sQ37_spl|~sQ7_spl),
% 29.21/4.11 inference(split_clause,[status(thm)],[f2309,f2325,f2422,f2148])).
% 29.21/4.11 fof(f2494,plain,(
% 29.21/4.11 sQ20_spl|sQ33_spl|~sQ7_spl),
% 29.21/4.11 inference(split_clause,[status(thm)],[f2311,f2325,f2390,f2148])).
% 29.21/4.11 fof(f2495,plain,(
% 29.21/4.11 sQ20_spl|sQ43_spl|~sQ7_spl),
% 29.21/4.11 inference(split_clause,[status(thm)],[f2312,f2325,f2468,f2148])).
% 29.21/4.11 fof(f2496,plain,(
% 29.21/4.11 sQ20_spl|sQ38_spl|~sQ7_spl),
% 29.21/4.11 inference(split_clause,[status(thm)],[f2313,f2325,f2427,f2148])).
% 29.21/4.11 fof(f2497,plain,(
% 29.21/4.11 sQ20_spl|sQ39_spl|~sQ7_spl),
% 29.21/4.11 inference(split_clause,[status(thm)],[f2314,f2325,f2432,f2148])).
% 29.21/4.11 fof(f2498,plain,(
% 29.21/4.11 sQ20_spl|sQ45_spl|~sQ7_spl),
% 29.21/4.11 inference(split_clause,[status(thm)],[f2315,f2325,f2482,f2148])).
% 29.21/4.11 fof(f2499,plain,(
% 29.21/4.11 sQ20_spl|sQ34_spl|~sQ7_spl),
% 29.21/4.11 inference(split_clause,[status(thm)],[f2316,f2325,f2395,f2148])).
% 29.21/4.11 fof(f2500,plain,(
% 29.21/4.11 sQ20_spl|sQ40_spl|~sQ7_spl),
% 29.21/4.11 inference(split_clause,[status(thm)],[f2317,f2325,f2437,f2148])).
% 29.21/4.11 fof(f2504,plain,(
% 29.21/4.11 sQ20_spl|sQ44_spl|~sQ7_spl),
% 29.21/4.11 inference(split_clause,[status(thm)],[f2321,f2325,f2475,f2148])).
% 29.21/4.11 fof(f2512,plain,(
% 29.21/4.11 sK9_skl(sK0_skl)=sK10_skl(sK0_skl)|~sQ20_spl),
% 29.21/4.11 inference(resolution,[status(thm)],[f2326,f67])).
% 29.21/4.11 fof(f2513,plain,(
% 29.21/4.11 sP0_prd(sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl)|~sQ20_spl),
% 29.21/4.11 inference(backward_demodulation,[status(thm)],[f2512,f2326])).
% 29.21/4.11 fof(f2522,plain,(
% 29.21/4.11 $false|~sQ20_spl),
% 29.21/4.11 inference(forward_subsumption_resolution,[status(thm)],[f2513,f79])).
% 29.21/4.11 fof(f2523,plain,(
% 29.21/4.11 ~sQ20_spl),
% 29.21/4.11 inference(contradiction_clause,[status(thm)],[f2522])).
% 29.21/4.11 fof(f2524,plain,(
% 29.21/4.11 ![X0]: (~in(sK2_skl(sK12_skl(X0,sK0_skl)),cartesian_product2(sK0_skl,sK1_skl))|sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))|~sQ12_spl)),
% 29.21/4.11 inference(duplicate_literals_removal,[status(thm)],[f2168])).
% 29.21/4.11 fof(f2542,plain,(
% 29.21/4.11 ![X0]: (sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))|ordered_pair(sK14_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl),sK15_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl))=sK2_skl(sK12_skl(X0,sK0_skl))|sK9_skl(sK0_skl)=sK11_skl(sK0_skl)|~sQ12_spl)),
% 29.21/4.11 inference(resolution,[status(thm)],[f2524,f506])).
% 29.21/4.11 fof(f2546,plain,(
% 29.21/4.11 ![X0]: (sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))|sK15_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl)=singleton(sK14_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl))|sK9_skl(sK0_skl)=sK11_skl(sK0_skl)|~sQ12_spl)),
% 29.21/4.11 inference(resolution,[status(thm)],[f2524,f415])).
% 29.21/4.11 fof(f2550,plain,(
% 29.21/4.11 ![X0]: (sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))|sK13_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl)=sK2_skl(sK12_skl(X0,sK0_skl))|sK9_skl(sK0_skl)=sK11_skl(sK0_skl)|~sQ12_spl)),
% 29.21/4.11 inference(resolution,[status(thm)],[f2524,f235])).
% 29.21/4.11 fof(f2576,plain,(
% 29.21/4.11 sQ27_spl|sQ7_spl|~sQ12_spl),
% 29.21/4.11 inference(split_clause,[status(thm)],[f2542,f2352,f2148,f2167])).
% 29.21/4.11 fof(f2580,plain,(
% 29.21/4.11 sQ31_spl|sQ7_spl|~sQ12_spl),
% 29.21/4.11 inference(split_clause,[status(thm)],[f2546,f2380,f2148,f2167])).
% 29.21/4.11 fof(f2584,plain,(
% 29.21/4.11 sQ37_spl|sQ7_spl|~sQ12_spl),
% 29.21/4.11 inference(split_clause,[status(thm)],[f2550,f2422,f2148,f2167])).
% 29.21/4.11 fof(f2586,definition,(
% 29.21/4.11 sQ46_spl <=> (sK4_skl(sK12_skl(sK1_skl,sK0_skl))=singleton(sK3_skl(sK12_skl(sK1_skl,sK0_skl))))),
% 29.21/4.11 introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition])).
% 29.21/4.11 fof(f2587,plain,(
% 29.21/4.11 sK4_skl(sK12_skl(sK1_skl,sK0_skl))=singleton(sK3_skl(sK12_skl(sK1_skl,sK0_skl)))|~sQ46_spl),
% 29.21/4.11 inference(component_clause,[status(thm)],[f2586])).
% 29.21/4.11 fof(f2595,plain,(
% 29.21/4.11 ![X0,X1]: (sP0_prd(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0)|in(ordered_pair(sK3_skl(sK12_skl(sK1_skl,sK0_skl)),singleton(sK3_skl(sK12_skl(sK1_skl,sK0_skl)))),sK12_skl(X1,X0))|~in(ordered_pair(sK3_skl(sK12_skl(sK1_skl,sK0_skl)),sK4_skl(sK12_skl(sK1_skl,sK0_skl))),cartesian_product2(X0,X1))|~in(sK3_skl(sK12_skl(sK1_skl,sK0_skl)),X0)|~sQ46_spl)),
% 29.21/4.11 inference(paramodulation,[status(thm)],[f2587,f78])).
% 29.21/4.11 fof(f2596,plain,(
% 29.21/4.11 ![X0]: (~in(sK2_skl(X0),X0)|~in(sK2_skl(X0),cartesian_product2(sK0_skl,sK1_skl))|~ordered_pair(sK3_skl(sK12_skl(sK1_skl,sK0_skl)),sK4_skl(sK12_skl(sK1_skl,sK0_skl)))=sK2_skl(X0)|~in(sK3_skl(sK12_skl(sK1_skl,sK0_skl)),sK0_skl)|~sQ46_spl)),
% 29.21/4.11 inference(paramodulation,[status(thm)],[f2587,f77])).
% 29.21/4.11 fof(f2597,plain,(
% 29.21/4.11 ![X0,X1]: (sP0_prd(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0)|in(ordered_pair(sK3_skl(sK12_skl(sK1_skl,sK0_skl)),sK4_skl(sK12_skl(sK1_skl,sK0_skl))),sK12_skl(X1,X0))|~in(ordered_pair(sK3_skl(sK12_skl(sK1_skl,sK0_skl)),sK4_skl(sK12_skl(sK1_skl,sK0_skl))),cartesian_product2(X0,X1))|~in(sK3_skl(sK12_skl(sK1_skl,sK0_skl)),X0)|~sQ46_spl)),
% 29.21/4.11 inference(forward_demodulation,[status(thm)],[f2587,f2595])).
% 29.21/4.11 fof(f2598,definition,(
% 29.21/4.11 ![X0]: (sQ47_spl <=> (~in(sK2_skl(X0),X0)|~in(sK2_skl(X0),cartesian_product2(sK0_skl,sK1_skl))|~ordered_pair(sK3_skl(sK12_skl(sK1_skl,sK0_skl)),sK4_skl(sK12_skl(sK1_skl,sK0_skl)))=sK2_skl(X0)))),
% 29.21/4.11 introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition])).
% 29.21/4.11 fof(f2599,plain,(
% 29.21/4.11 ![X0]: (~in(sK2_skl(X0),X0)|~in(sK2_skl(X0),cartesian_product2(sK0_skl,sK1_skl))|~ordered_pair(sK3_skl(sK12_skl(sK1_skl,sK0_skl)),sK4_skl(sK12_skl(sK1_skl,sK0_skl)))=sK2_skl(X0)|~sQ47_spl)),
% 29.21/4.11 inference(component_clause,[status(thm)],[f2598])).
% 29.21/4.11 fof(f2601,definition,(
% 29.21/4.11 sQ48_spl <=> (in(sK3_skl(sK12_skl(sK1_skl,sK0_skl)),sK0_skl))),
% 29.21/4.11 introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 29.21/4.11 fof(f2603,plain,(
% 29.21/4.11 ~in(sK3_skl(sK12_skl(sK1_skl,sK0_skl)),sK0_skl)|sQ48_spl),
% 29.21/4.11 inference(component_clause,[status(thm)],[f2601])).
% 29.21/4.11 fof(f2604,plain,(
% 29.21/4.11 sQ47_spl|~sQ48_spl|~sQ46_spl),
% 29.21/4.11 inference(split_clause,[status(thm)],[f2596,f2598,f2601,f2586])).
% 29.21/4.11 fof(f2652,plain,(
% 29.21/4.11 ![X0]: (sK2_skl(sK12_skl(X0,sK0_skl))=sK2_skl(sK12_skl(X0,sK0_skl))|sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))|sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))|sK9_skl(sK0_skl)=sK10_skl(sK0_skl)|~sQ37_spl)),
% 29.21/4.11 inference(paramodulation,[status(thm)],[f280,f2423])).
% 29.21/4.11 fof(f2686,plain,(
% 29.21/4.11 ![X0]: (sP0_prd(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl)|ordered_pair(sK3_skl(sK12_skl(X0,sK0_skl)),sK4_skl(sK12_skl(X0,sK0_skl)))=sK2_skl(sK12_skl(X0,sK0_skl))|~in(cartesian_product2(sK0_skl,X0),sK2_skl(sK12_skl(X0,sK0_skl)))|sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))|~sQ37_spl)),
% 29.21/4.11 inference(paramodulation,[status(thm)],[f2423,f157])).
% 29.21/4.11 fof(f2703,plain,(
% 29.21/4.11 ![X0]: (ordered_pair(sK3_skl(sK12_skl(X0,sK0_skl)),sK4_skl(sK12_skl(X0,sK0_skl)))=sK2_skl(sK12_skl(X0,sK0_skl))|sK9_skl(sK0_skl)=sK10_skl(sK0_skl)|~in(cartesian_product2(sK0_skl,X0),sK2_skl(sK12_skl(X0,sK0_skl)))|sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))|~sQ37_spl)),
% 29.21/4.11 inference(paramodulation,[status(thm)],[f2423,f491])).
% 29.21/4.11 fof(f2704,plain,(
% 29.21/4.11 ![X0]: (ordered_pair(sK3_skl(sK12_skl(X0,sK0_skl)),sK4_skl(sK12_skl(X0,sK0_skl)))=sK2_skl(sK12_skl(X0,sK0_skl))|sK9_skl(sK0_skl)=sK11_skl(sK0_skl)|~in(cartesian_product2(sK0_skl,X0),sK2_skl(sK12_skl(X0,sK0_skl)))|sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))|~sQ37_spl)),
% 29.21/4.11 inference(paramodulation,[status(thm)],[f2423,f487])).
% 29.21/4.11 fof(f2705,plain,(
% 29.21/4.11 ![X0]: (sP0_prd(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl)|sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))|~in(cartesian_product2(sK0_skl,X0),sK2_skl(sK12_skl(X0,sK0_skl)))|sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))|~sQ37_spl)),
% 29.21/4.11 inference(paramodulation,[status(thm)],[f2423,f228])).
% 29.21/4.11 fof(f2706,plain,(
% 29.21/4.11 ![X0]: (in(sK2_skl(sK12_skl(X0,sK0_skl)),cartesian_product2(sK0_skl,X0))|ordered_pair(sK3_skl(sK12_skl(X0,sK0_skl)),sK4_skl(sK12_skl(X0,sK0_skl)))=sK2_skl(sK12_skl(X0,sK0_skl))|sK9_skl(sK0_skl)=sK10_skl(sK0_skl)|sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))|~sQ37_spl)),
% 29.21/4.11 inference(paramodulation,[status(thm)],[f2423,f156])).
% 29.21/4.11 fof(f2707,plain,(
% 29.21/4.11 ![X0]: (in(sK2_skl(sK12_skl(X0,sK0_skl)),cartesian_product2(sK0_skl,X0))|ordered_pair(sK3_skl(sK12_skl(X0,sK0_skl)),sK4_skl(sK12_skl(X0,sK0_skl)))=sK2_skl(sK12_skl(X0,sK0_skl))|sK9_skl(sK0_skl)=sK11_skl(sK0_skl)|sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))|~sQ37_spl)),
% 29.21/4.11 inference(paramodulation,[status(thm)],[f2423,f155])).
% 29.21/4.11 fof(f2708,plain,(
% 29.21/4.11 ![X0]: (sP0_prd(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl)|in(sK2_skl(sK12_skl(X0,sK0_skl)),cartesian_product2(sK0_skl,sK1_skl))|~in(cartesian_product2(sK0_skl,X0),sK2_skl(sK12_skl(X0,sK0_skl)))|sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))|~sQ37_spl)),
% 29.21/4.11 inference(paramodulation,[status(thm)],[f2423,f148])).
% 29.21/4.11 fof(f2712,plain,(
% 29.21/4.11 ![X0]: (sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))|sK9_skl(sK0_skl)=sK10_skl(sK0_skl)|~in(cartesian_product2(sK0_skl,X0),sK2_skl(sK12_skl(X0,sK0_skl)))|sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))|~sQ37_spl)),
% 29.21/4.11 inference(paramodulation,[status(thm)],[f2423,f258])).
% 29.21/4.11 fof(f2713,plain,(
% 29.21/4.11 ![X0]: (sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))|sK9_skl(sK0_skl)=sK11_skl(sK0_skl)|~in(cartesian_product2(sK0_skl,X0),sK2_skl(sK12_skl(X0,sK0_skl)))|sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))|~sQ37_spl)),
% 29.21/4.11 inference(paramodulation,[status(thm)],[f2423,f257])).
% 29.21/4.11 fof(f2714,plain,(
% 29.21/4.11 ![X0]: (in(sK2_skl(sK12_skl(X0,sK0_skl)),cartesian_product2(sK0_skl,X0))|sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))|sK9_skl(sK0_skl)=sK10_skl(sK0_skl)|sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))|~sQ37_spl)),
% 29.21/4.11 inference(paramodulation,[status(thm)],[f2423,f227])).
% 29.21/4.11 fof(f2715,plain,(
% 29.21/4.11 ![X0]: (in(sK2_skl(sK12_skl(X0,sK0_skl)),cartesian_product2(sK0_skl,X0))|sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))|sK9_skl(sK0_skl)=sK11_skl(sK0_skl)|sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))|~sQ37_spl)),
% 29.21/4.11 inference(paramodulation,[status(thm)],[f2423,f226])).
% 29.21/4.11 fof(f2716,plain,(
% 29.21/4.11 ![X0]: (in(sK2_skl(sK12_skl(X0,sK0_skl)),cartesian_product2(sK0_skl,sK1_skl))|sK9_skl(sK0_skl)=sK10_skl(sK0_skl)|~in(cartesian_product2(sK0_skl,X0),sK2_skl(sK12_skl(X0,sK0_skl)))|sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))|~sQ37_spl)),
% 29.21/4.11 inference(paramodulation,[status(thm)],[f2423,f219])).
% 29.21/4.11 fof(f2717,plain,(
% 29.21/4.11 ![X0]: (in(sK2_skl(sK12_skl(X0,sK0_skl)),cartesian_product2(sK0_skl,sK1_skl))|sK9_skl(sK0_skl)=sK11_skl(sK0_skl)|~in(cartesian_product2(sK0_skl,X0),sK2_skl(sK12_skl(X0,sK0_skl)))|sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))|~sQ37_spl)),
% 29.21/4.11 inference(paramodulation,[status(thm)],[f2423,f218])).
% 29.21/4.11 fof(f2718,plain,(
% 29.21/4.11 ![X0]: (sP0_prd(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl)|in(sK2_skl(sK12_skl(X0,sK0_skl)),cartesian_product2(sK0_skl,X0))|sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))|sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))|~sQ37_spl)),
% 29.21/4.11 inference(paramodulation,[status(thm)],[f2423,f122])).
% 29.21/4.11 fof(f2719,plain,(
% 29.21/4.11 ![X0]: (in(sK2_skl(sK12_skl(X0,sK0_skl)),cartesian_product2(sK0_skl,X0))|in(sK2_skl(sK12_skl(X0,sK0_skl)),cartesian_product2(sK0_skl,sK1_skl))|sK9_skl(sK0_skl)=sK10_skl(sK0_skl)|sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))|~sQ37_spl)),
% 29.21/4.11 inference(paramodulation,[status(thm)],[f2423,f147])).
% 29.21/4.11 fof(f2720,plain,(
% 29.21/4.11 ![X0]: (in(sK2_skl(sK12_skl(X0,sK0_skl)),cartesian_product2(sK0_skl,X0))|in(sK2_skl(sK12_skl(X0,sK0_skl)),cartesian_product2(sK0_skl,sK1_skl))|sK9_skl(sK0_skl)=sK11_skl(sK0_skl)|sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))|~sQ37_spl)),
% 29.21/4.11 inference(paramodulation,[status(thm)],[f2423,f146])).
% 29.21/4.11 fof(f2721,plain,(
% 29.21/4.11 ![X0]: (sP0_prd(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl)|in(sK2_skl(sK12_skl(X0,sK0_skl)),cartesian_product2(sK0_skl,X0))|ordered_pair(sK3_skl(sK12_skl(X0,sK0_skl)),sK4_skl(sK12_skl(X0,sK0_skl)))=sK2_skl(sK12_skl(X0,sK0_skl))|sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))|~sQ37_spl)),
% 29.21/4.11 inference(paramodulation,[status(thm)],[f2423,f121])).
% 29.21/4.11 fof(f2722,plain,(
% 29.21/4.11 ![X0]: (sP0_prd(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl)|in(sK2_skl(sK12_skl(X0,sK0_skl)),cartesian_product2(sK0_skl,X0))|in(sK2_skl(sK12_skl(X0,sK0_skl)),cartesian_product2(sK0_skl,sK1_skl))|sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))|~sQ37_spl)),
% 29.21/4.11 inference(paramodulation,[status(thm)],[f2423,f119])).
% 29.21/4.11 fof(f2726,plain,(
% 29.21/4.11 ![X0]: (sP0_prd(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl)|in(sK3_skl(sK12_skl(X0,sK0_skl)),sK0_skl)|~in(cartesian_product2(sK0_skl,X0),sK2_skl(sK12_skl(X0,sK0_skl)))|sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))|~sQ37_spl)),
% 29.21/4.11 inference(paramodulation,[status(thm)],[f2423,f131])).
% 29.21/4.11 fof(f2727,plain,(
% 29.21/4.11 ![X0]: (in(sK3_skl(sK12_skl(X0,sK0_skl)),sK0_skl)|sK9_skl(sK0_skl)=sK10_skl(sK0_skl)|~in(cartesian_product2(sK0_skl,X0),sK2_skl(sK12_skl(X0,sK0_skl)))|sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))|~sQ37_spl)),
% 29.21/4.11 inference(paramodulation,[status(thm)],[f2423,f133])).
% 29.21/4.11 fof(f2728,plain,(
% 29.21/4.11 ![X0]: (in(sK3_skl(sK12_skl(X0,sK0_skl)),sK0_skl)|sK9_skl(sK0_skl)=sK11_skl(sK0_skl)|~in(cartesian_product2(sK0_skl,X0),sK2_skl(sK12_skl(X0,sK0_skl)))|sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))|~sQ37_spl)),
% 29.21/4.11 inference(paramodulation,[status(thm)],[f2423,f132])).
% 29.21/4.11 fof(f2729,plain,(
% 29.21/4.11 ![X0]: (in(sK2_skl(sK12_skl(X0,sK0_skl)),cartesian_product2(sK0_skl,X0))|in(sK3_skl(sK12_skl(X0,sK0_skl)),sK0_skl)|sK9_skl(sK0_skl)=sK10_skl(sK0_skl)|sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))|~sQ37_spl)),
% 29.21/4.11 inference(paramodulation,[status(thm)],[f2423,f130])).
% 29.21/4.11 fof(f2730,plain,(
% 29.21/4.11 ![X0]: (in(sK2_skl(sK12_skl(X0,sK0_skl)),cartesian_product2(sK0_skl,X0))|in(sK3_skl(sK12_skl(X0,sK0_skl)),sK0_skl)|sK9_skl(sK0_skl)=sK11_skl(sK0_skl)|sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))|~sQ37_spl)),
% 29.21/4.11 inference(paramodulation,[status(thm)],[f2423,f129])).
% 29.21/4.11 fof(f2731,plain,(
% 29.21/4.11 ![X0]: (sP0_prd(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl)|in(sK2_skl(sK12_skl(X0,sK0_skl)),cartesian_product2(sK0_skl,X0))|in(sK3_skl(sK12_skl(X0,sK0_skl)),sK0_skl)|sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))|~sQ37_spl)),
% 29.21/4.11 inference(paramodulation,[status(thm)],[f2423,f120])).
% 29.21/4.11 fof(f2732,definition,(
% 29.21/4.11 ![X0]: (sQ49_spl <=> (sK2_skl(sK12_skl(X0,sK0_skl))=sK2_skl(sK12_skl(X0,sK0_skl))|sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))|sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))))),
% 29.21/4.11 introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition])).
% 29.21/4.11 fof(f2739,plain,(
% 29.21/4.11 sQ49_spl|sQ17_spl|~sQ37_spl),
% 29.21/4.11 inference(split_clause,[status(thm)],[f2652,f2732,f2200,f2422])).
% 29.21/4.11 fof(f2741,definition,(
% 29.21/4.11 ![X0]: (sQ50_spl <=> (ordered_pair(sK3_skl(sK12_skl(X0,sK0_skl)),sK4_skl(sK12_skl(X0,sK0_skl)))=sK2_skl(sK12_skl(X0,sK0_skl))|~in(cartesian_product2(sK0_skl,X0),sK2_skl(sK12_skl(X0,sK0_skl)))|sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))))),
% 29.21/4.11 introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition])).
% 29.21/4.11 fof(f2748,definition,(
% 29.21/4.11 ![X0]: (sQ51_spl <=> (sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))|~in(cartesian_product2(sK0_skl,X0),sK2_skl(sK12_skl(X0,sK0_skl)))|sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))))),
% 29.21/4.11 introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition])).
% 29.21/4.11 fof(f2753,definition,(
% 29.21/4.11 ![X0]: (sQ52_spl <=> (in(sK2_skl(sK12_skl(X0,sK0_skl)),cartesian_product2(sK0_skl,sK1_skl))|~in(cartesian_product2(sK0_skl,X0),sK2_skl(sK12_skl(X0,sK0_skl)))|sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))))),
% 29.21/4.11 introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 29.21/4.11 fof(f2766,definition,(
% 29.21/4.11 ![X0]: (sQ53_spl <=> (in(sK2_skl(sK12_skl(X0,sK0_skl)),cartesian_product2(sK0_skl,X0))|sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))|sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))))),
% 29.21/4.11 introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 29.21/4.11 fof(f2767,plain,(
% 29.21/4.11 ![X0]: (in(sK2_skl(sK12_skl(X0,sK0_skl)),cartesian_product2(sK0_skl,X0))|sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))|sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))|~sQ53_spl)),
% 29.21/4.11 inference(component_clause,[status(thm)],[f2766])).
% 29.21/4.11 fof(f2770,definition,(
% 29.21/4.11 ![X0]: (sQ54_spl <=> (in(sK3_skl(sK12_skl(X0,sK0_skl)),sK0_skl)|~in(cartesian_product2(sK0_skl,X0),sK2_skl(sK12_skl(X0,sK0_skl)))|sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))))),
% 29.21/4.11 introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition])).
% 29.21/4.11 fof(f2782,definition,(
% 29.21/4.11 ![X0]: (sQ55_spl <=> (in(sK2_skl(sK12_skl(X0,sK0_skl)),cartesian_product2(sK0_skl,X0))|ordered_pair(sK3_skl(sK12_skl(X0,sK0_skl)),sK4_skl(sK12_skl(X0,sK0_skl)))=sK2_skl(sK12_skl(X0,sK0_skl))|sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))))),
% 29.21/4.11 introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition])).
% 29.21/4.11 fof(f2791,plain,(
% 29.21/4.11 sQ18_spl|sQ50_spl|~sQ37_spl),
% 29.21/4.11 inference(split_clause,[status(thm)],[f2686,f2207,f2741,f2422])).
% 29.21/4.11 fof(f2792,definition,(
% 29.21/4.11 ![X0]: (sQ56_spl <=> (in(sK2_skl(sK12_skl(X0,sK0_skl)),cartesian_product2(sK0_skl,X0))|in(sK2_skl(sK12_skl(X0,sK0_skl)),cartesian_product2(sK0_skl,sK1_skl))|sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))))),
% 29.21/4.11 introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition])).
% 29.21/4.11 fof(f2804,definition,(
% 29.21/4.11 ![X0]: (sQ57_spl <=> (in(sK2_skl(sK12_skl(X0,sK0_skl)),cartesian_product2(sK0_skl,X0))|in(sK3_skl(sK12_skl(X0,sK0_skl)),sK0_skl)|sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))))),
% 29.21/4.11 introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition])).
% 29.21/4.11 fof(f2814,plain,(
% 29.21/4.11 sQ50_spl|sQ17_spl|~sQ37_spl),
% 29.21/4.11 inference(split_clause,[status(thm)],[f2703,f2741,f2200,f2422])).
% 29.21/4.11 fof(f2815,plain,(
% 29.21/4.11 sQ50_spl|sQ7_spl|~sQ37_spl),
% 29.21/4.11 inference(split_clause,[status(thm)],[f2704,f2741,f2148,f2422])).
% 29.21/4.11 fof(f2816,plain,(
% 29.21/4.11 sQ18_spl|sQ51_spl|~sQ37_spl),
% 29.21/4.11 inference(split_clause,[status(thm)],[f2705,f2207,f2748,f2422])).
% 29.21/4.11 fof(f2817,plain,(
% 29.21/4.11 sQ55_spl|sQ17_spl|~sQ37_spl),
% 29.21/4.11 inference(split_clause,[status(thm)],[f2706,f2782,f2200,f2422])).
% 29.21/4.11 fof(f2818,plain,(
% 29.21/4.11 sQ55_spl|sQ7_spl|~sQ37_spl),
% 29.21/4.11 inference(split_clause,[status(thm)],[f2707,f2782,f2148,f2422])).
% 29.21/4.11 fof(f2819,plain,(
% 29.21/4.11 sQ18_spl|sQ52_spl|~sQ37_spl),
% 29.21/4.11 inference(split_clause,[status(thm)],[f2708,f2207,f2753,f2422])).
% 29.21/4.11 fof(f2823,plain,(
% 29.21/4.11 sQ51_spl|sQ17_spl|~sQ37_spl),
% 29.21/4.11 inference(split_clause,[status(thm)],[f2712,f2748,f2200,f2422])).
% 29.21/4.11 fof(f2824,plain,(
% 29.21/4.11 sQ51_spl|sQ7_spl|~sQ37_spl),
% 29.21/4.11 inference(split_clause,[status(thm)],[f2713,f2748,f2148,f2422])).
% 29.21/4.11 fof(f2825,plain,(
% 29.21/4.11 sQ53_spl|sQ17_spl|~sQ37_spl),
% 29.21/4.11 inference(split_clause,[status(thm)],[f2714,f2766,f2200,f2422])).
% 29.21/4.11 fof(f2826,plain,(
% 29.21/4.11 sQ53_spl|sQ7_spl|~sQ37_spl),
% 29.21/4.11 inference(split_clause,[status(thm)],[f2715,f2766,f2148,f2422])).
% 29.21/4.11 fof(f2827,plain,(
% 29.21/4.11 sQ52_spl|sQ17_spl|~sQ37_spl),
% 29.21/4.11 inference(split_clause,[status(thm)],[f2716,f2753,f2200,f2422])).
% 29.21/4.11 fof(f2828,plain,(
% 29.21/4.11 sQ52_spl|sQ7_spl|~sQ37_spl),
% 29.21/4.11 inference(split_clause,[status(thm)],[f2717,f2753,f2148,f2422])).
% 29.21/4.11 fof(f2829,plain,(
% 29.21/4.11 sQ18_spl|sQ53_spl|~sQ37_spl),
% 29.21/4.11 inference(split_clause,[status(thm)],[f2718,f2207,f2766,f2422])).
% 29.21/4.11 fof(f2830,plain,(
% 29.21/4.11 sQ56_spl|sQ17_spl|~sQ37_spl),
% 29.21/4.11 inference(split_clause,[status(thm)],[f2719,f2792,f2200,f2422])).
% 29.21/4.11 fof(f2831,plain,(
% 29.21/4.11 sQ56_spl|sQ7_spl|~sQ37_spl),
% 29.21/4.11 inference(split_clause,[status(thm)],[f2720,f2792,f2148,f2422])).
% 29.21/4.11 fof(f2832,plain,(
% 29.21/4.11 sQ18_spl|sQ55_spl|~sQ37_spl),
% 29.21/4.11 inference(split_clause,[status(thm)],[f2721,f2207,f2782,f2422])).
% 29.21/4.11 fof(f2833,plain,(
% 29.21/4.11 sQ18_spl|sQ56_spl|~sQ37_spl),
% 29.21/4.11 inference(split_clause,[status(thm)],[f2722,f2207,f2792,f2422])).
% 29.21/4.12 fof(f2837,plain,(
% 29.21/4.12 sQ18_spl|sQ54_spl|~sQ37_spl),
% 29.21/4.12 inference(split_clause,[status(thm)],[f2726,f2207,f2770,f2422])).
% 29.21/4.12 fof(f2838,plain,(
% 29.21/4.12 sQ54_spl|sQ17_spl|~sQ37_spl),
% 29.21/4.12 inference(split_clause,[status(thm)],[f2727,f2770,f2200,f2422])).
% 29.21/4.12 fof(f2839,plain,(
% 29.21/4.12 sQ54_spl|sQ7_spl|~sQ37_spl),
% 29.21/4.12 inference(split_clause,[status(thm)],[f2728,f2770,f2148,f2422])).
% 29.21/4.12 fof(f2840,plain,(
% 29.21/4.12 sQ57_spl|sQ17_spl|~sQ37_spl),
% 29.21/4.12 inference(split_clause,[status(thm)],[f2729,f2804,f2200,f2422])).
% 29.21/4.12 fof(f2841,plain,(
% 29.21/4.12 sQ57_spl|sQ7_spl|~sQ37_spl),
% 29.21/4.12 inference(split_clause,[status(thm)],[f2730,f2804,f2148,f2422])).
% 29.21/4.12 fof(f2842,plain,(
% 29.21/4.12 sQ18_spl|sQ57_spl|~sQ37_spl),
% 29.21/4.12 inference(split_clause,[status(thm)],[f2731,f2207,f2804,f2422])).
% 29.21/4.12 fof(f2844,plain,(
% 29.21/4.12 ![X0]: (in(sK2_skl(sK12_skl(X0,sK0_skl)),cartesian_product2(sK0_skl,X0))|sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))|~sQ53_spl)),
% 29.21/4.12 inference(duplicate_literals_removal,[status(thm)],[f2767])).
% 29.21/4.12 fof(f2845,plain,(
% 29.21/4.12 sK4_skl(sK12_skl(sK1_skl,sK0_skl))=singleton(sK3_skl(sK12_skl(sK1_skl,sK0_skl)))|sK4_skl(sK12_skl(sK1_skl,sK0_skl))=singleton(sK3_skl(sK12_skl(sK1_skl,sK0_skl)))|~sQ53_spl|~sQ12_spl),
% 29.21/4.12 inference(resolution,[status(thm)],[f2844,f2524])).
% 29.21/4.12 fof(f2847,plain,(
% 29.21/4.12 sQ46_spl|~sQ53_spl|~sQ12_spl),
% 29.21/4.12 inference(split_clause,[status(thm)],[f2845,f2586,f2766,f2167])).
% 29.21/4.12 fof(f2856,plain,(
% 29.21/4.12 ~in(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK12_skl(sK1_skl,sK0_skl))|~in(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),cartesian_product2(sK0_skl,sK1_skl))|sK15_skl(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl)=singleton(sK14_skl(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl))|sK9_skl(sK0_skl)=sK10_skl(sK0_skl)|~sQ47_spl),
% 29.21/4.12 inference(resolution,[status(thm)],[f2599,f460])).
% 29.21/4.12 fof(f2872,definition,(
% 29.21/4.12 sQ58_spl <=> (in(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK12_skl(sK1_skl,sK0_skl)))),
% 29.21/4.12 introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition])).
% 29.21/4.12 fof(f2873,plain,(
% 29.21/4.12 in(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK12_skl(sK1_skl,sK0_skl))|~sQ58_spl),
% 29.21/4.12 inference(component_clause,[status(thm)],[f2872])).
% 29.21/4.12 fof(f2874,plain,(
% 29.21/4.12 ~in(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK12_skl(sK1_skl,sK0_skl))|sQ58_spl),
% 29.21/4.12 inference(component_clause,[status(thm)],[f2872])).
% 29.21/4.12 fof(f2875,definition,(
% 29.21/4.12 sQ59_spl <=> (in(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),cartesian_product2(sK0_skl,sK1_skl)))),
% 29.21/4.12 introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition])).
% 29.21/4.12 fof(f2877,plain,(
% 29.21/4.12 ~in(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),cartesian_product2(sK0_skl,sK1_skl))|sQ59_spl),
% 29.21/4.12 inference(component_clause,[status(thm)],[f2875])).
% 29.21/4.12 fof(f2878,definition,(
% 29.21/4.12 sQ60_spl <=> (sK15_skl(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl)=singleton(sK14_skl(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl)))),
% 29.21/4.12 introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition])).
% 29.21/4.12 fof(f2879,plain,(
% 29.21/4.12 sK15_skl(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl)=singleton(sK14_skl(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl))|~sQ60_spl),
% 29.21/4.12 inference(component_clause,[status(thm)],[f2878])).
% 29.21/4.12 fof(f2885,definition,(
% 29.21/4.12 sQ61_spl <=> (sK13_skl(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl)=sK2_skl(sK12_skl(sK1_skl,sK0_skl)))),
% 29.21/4.12 introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition])).
% 29.21/4.12 fof(f2886,plain,(
% 29.21/4.12 sK13_skl(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl)=sK2_skl(sK12_skl(sK1_skl,sK0_skl))|~sQ61_spl),
% 29.21/4.12 inference(component_clause,[status(thm)],[f2885])).
% 29.21/4.12 fof(f2887,plain,(
% 29.21/4.12 ~sK13_skl(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl)=sK2_skl(sK12_skl(sK1_skl,sK0_skl))|sQ61_spl),
% 29.21/4.12 inference(component_clause,[status(thm)],[f2885])).
% 29.21/4.12 fof(f2892,plain,(
% 29.21/4.12 ~sQ58_spl|~sQ59_spl|sQ60_spl|sQ17_spl|~sQ47_spl),
% 29.21/4.12 inference(split_clause,[status(thm)],[f2856,f2872,f2875,f2878,f2200,f2598])).
% 29.21/4.12 fof(f2927,plain,(
% 29.21/4.12 ![X0,X1]: (sP0_prd(sK11_skl(sK0_skl),sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl)|sK13_skl(sK18_skl(sK11_skl(sK12_skl(X0,sK0_skl)),sK10_skl(sK12_skl(X0,sK0_skl)),sK9_skl(sK12_skl(X0,sK0_skl)),sK12_skl(X0,sK0_skl)),X0,sK0_skl)=sK18_skl(sK11_skl(sK12_skl(X0,sK0_skl)),sK10_skl(sK12_skl(X0,sK0_skl)),sK9_skl(sK12_skl(X0,sK0_skl)),sK12_skl(X0,sK0_skl))|in(sK13_skl(sK2_skl(sK12_skl(X1,sK12_skl(X0,sK0_skl))),X1,sK12_skl(X0,sK0_skl)),cartesian_product2(sK12_skl(X0,sK0_skl),X1))|in(sK3_skl(sK12_skl(X1,sK12_skl(X0,sK0_skl))),sK0_skl)|~sQ17_spl)),
% 29.21/4.12 inference(paramodulation,[status(thm)],[f2201,f169])).
% 29.21/4.12 fof(f2928,plain,(
% 29.21/4.12 ![X0,X1]: (sP0_prd(sK11_skl(sK0_skl),sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl)|sK13_skl(sK16_skl(sK11_skl(sK12_skl(X0,sK0_skl)),sK10_skl(sK12_skl(X0,sK0_skl)),sK9_skl(sK12_skl(X0,sK0_skl)),sK12_skl(X0,sK0_skl)),X0,sK0_skl)=sK16_skl(sK11_skl(sK12_skl(X0,sK0_skl)),sK10_skl(sK12_skl(X0,sK0_skl)),sK9_skl(sK12_skl(X0,sK0_skl)),sK12_skl(X0,sK0_skl))|in(sK13_skl(sK2_skl(sK12_skl(X1,sK12_skl(X0,sK0_skl))),X1,sK12_skl(X0,sK0_skl)),cartesian_product2(sK12_skl(X0,sK0_skl),X1))|in(sK3_skl(sK12_skl(X1,sK12_skl(X0,sK0_skl))),sK0_skl)|~sQ17_spl)),
% 29.21/4.12 inference(paramodulation,[status(thm)],[f2201,f168])).
% 29.21/4.12 fof(f3031,definition,(
% 29.21/4.12 sQ63_spl <=> (sP0_prd(sK11_skl(sK0_skl),sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl))),
% 29.21/4.12 introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition])).
% 29.21/4.12 fof(f3032,plain,(
% 29.21/4.12 sP0_prd(sK11_skl(sK0_skl),sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl)|~sQ63_spl),
% 29.21/4.12 inference(component_clause,[status(thm)],[f3031])).
% 29.21/4.12 fof(f3034,definition,(
% 29.21/4.12 ![X0,X1]: (sQ64_spl <=> (sK13_skl(sK18_skl(sK11_skl(sK12_skl(X0,sK0_skl)),sK10_skl(sK12_skl(X0,sK0_skl)),sK9_skl(sK12_skl(X0,sK0_skl)),sK12_skl(X0,sK0_skl)),X0,sK0_skl)=sK18_skl(sK11_skl(sK12_skl(X0,sK0_skl)),sK10_skl(sK12_skl(X0,sK0_skl)),sK9_skl(sK12_skl(X0,sK0_skl)),sK12_skl(X0,sK0_skl))|in(sK13_skl(sK2_skl(sK12_skl(X1,sK12_skl(X0,sK0_skl))),X1,sK12_skl(X0,sK0_skl)),cartesian_product2(sK12_skl(X0,sK0_skl),X1))|in(sK3_skl(sK12_skl(X1,sK12_skl(X0,sK0_skl))),sK0_skl)))),
% 29.21/4.12 introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition])).
% 29.21/4.12 fof(f3037,plain,(
% 29.21/4.12 sQ63_spl|sQ64_spl|~sQ17_spl),
% 29.21/4.12 inference(split_clause,[status(thm)],[f2927,f3031,f3034,f2200])).
% 29.21/4.12 fof(f3038,definition,(
% 29.21/4.12 ![X0,X1]: (sQ65_spl <=> (sK13_skl(sK16_skl(sK11_skl(sK12_skl(X0,sK0_skl)),sK10_skl(sK12_skl(X0,sK0_skl)),sK9_skl(sK12_skl(X0,sK0_skl)),sK12_skl(X0,sK0_skl)),X0,sK0_skl)=sK16_skl(sK11_skl(sK12_skl(X0,sK0_skl)),sK10_skl(sK12_skl(X0,sK0_skl)),sK9_skl(sK12_skl(X0,sK0_skl)),sK12_skl(X0,sK0_skl))|in(sK13_skl(sK2_skl(sK12_skl(X1,sK12_skl(X0,sK0_skl))),X1,sK12_skl(X0,sK0_skl)),cartesian_product2(sK12_skl(X0,sK0_skl),X1))|in(sK3_skl(sK12_skl(X1,sK12_skl(X0,sK0_skl))),sK0_skl)))),
% 29.21/4.12 introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition])).
% 29.21/4.12 fof(f3041,plain,(
% 29.21/4.12 sQ63_spl|sQ65_spl|~sQ17_spl),
% 29.21/4.12 inference(split_clause,[status(thm)],[f2928,f3031,f3038,f2200])).
% 29.21/4.12 fof(f3175,plain,(
% 29.21/4.12 sK9_skl(sK0_skl)=sK11_skl(sK0_skl)|~sQ63_spl),
% 29.21/4.12 inference(resolution,[status(thm)],[f3032,f71])).
% 29.21/4.12 fof(f3177,plain,(
% 29.21/4.12 sQ7_spl|~sQ63_spl),
% 29.21/4.12 inference(split_clause,[status(thm)],[f3175,f2148,f3031])).
% 29.21/4.12 fof(f3287,plain,(
% 29.21/4.12 in(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),cartesian_product2(sK0_skl,sK1_skl))|in(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),cartesian_product2(sK0_skl,sK1_skl))|sK9_skl(sK0_skl)=sK10_skl(sK0_skl)|~sQ61_spl),
% 29.21/4.12 inference(paramodulation,[status(thm)],[f2886,f147])).
% 29.21/4.12 fof(f3288,plain,(
% 29.21/4.12 in(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),cartesian_product2(sK0_skl,sK1_skl))|in(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),cartesian_product2(sK0_skl,sK1_skl))|sK9_skl(sK0_skl)=sK11_skl(sK0_skl)|~sQ61_spl),
% 29.21/4.12 inference(paramodulation,[status(thm)],[f2886,f146])).
% 29.21/4.12 fof(f3290,plain,(
% 29.21/4.12 sP0_prd(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl)|in(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),cartesian_product2(sK0_skl,sK1_skl))|in(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),cartesian_product2(sK0_skl,sK1_skl))|~sQ61_spl),
% 29.21/4.12 inference(paramodulation,[status(thm)],[f2886,f119])).
% 29.21/4.12 fof(f3300,definition,(
% 29.21/4.12 sQ70_spl <=> (sK2_skl(sK12_skl(sK1_skl,sK0_skl))=sK2_skl(sK12_skl(sK1_skl,sK0_skl)))),
% 29.21/4.12 introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition])).
% 29.21/4.12 fof(f3302,plain,(
% 29.21/4.12 ~sK2_skl(sK12_skl(sK1_skl,sK0_skl))=sK2_skl(sK12_skl(sK1_skl,sK0_skl))|sQ70_spl),
% 29.21/4.12 inference(component_clause,[status(thm)],[f3300])).
% 29.21/4.12 fof(f3311,definition,(
% 29.21/4.12 sQ71_spl <=> (ordered_pair(sK3_skl(sK12_skl(sK1_skl,sK0_skl)),sK4_skl(sK12_skl(sK1_skl,sK0_skl)))=sK2_skl(sK12_skl(sK1_skl,sK0_skl)))),
% 29.21/4.12 introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition])).
% 29.21/4.12 fof(f3312,plain,(
% 29.21/4.12 ordered_pair(sK3_skl(sK12_skl(sK1_skl,sK0_skl)),sK4_skl(sK12_skl(sK1_skl,sK0_skl)))=sK2_skl(sK12_skl(sK1_skl,sK0_skl))|~sQ71_spl),
% 29.21/4.12 inference(component_clause,[status(thm)],[f3311])).
% 29.21/4.12 fof(f3313,plain,(
% 29.21/4.12 ~ordered_pair(sK3_skl(sK12_skl(sK1_skl,sK0_skl)),sK4_skl(sK12_skl(sK1_skl,sK0_skl)))=sK2_skl(sK12_skl(sK1_skl,sK0_skl))|sQ71_spl),
% 29.21/4.12 inference(component_clause,[status(thm)],[f3311])).
% 29.21/4.12 fof(f3382,plain,(
% 29.21/4.12 sQ59_spl|sQ17_spl|~sQ61_spl),
% 29.21/4.12 inference(split_clause,[status(thm)],[f3287,f2875,f2200,f2885])).
% 29.21/4.12 fof(f3383,plain,(
% 29.21/4.12 sQ59_spl|sQ7_spl|~sQ61_spl),
% 29.21/4.12 inference(split_clause,[status(thm)],[f3288,f2875,f2148,f2885])).
% 29.21/4.12 fof(f3385,plain,(
% 29.21/4.12 sQ18_spl|sQ59_spl|~sQ61_spl),
% 29.21/4.12 inference(split_clause,[status(thm)],[f3290,f2207,f2875,f2885])).
% 29.21/4.12 fof(f3411,plain,(
% 29.21/4.12 ordered_pair(sK14_skl(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl),sK15_skl(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl))=sK2_skl(sK12_skl(sK1_skl,sK0_skl))|sK9_skl(sK0_skl)=sK10_skl(sK0_skl)|sQ48_spl),
% 29.21/4.12 inference(resolution,[status(thm)],[f2603,f516])).
% 29.21/4.12 fof(f3413,plain,(
% 29.21/4.12 sP0_prd(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl)|ordered_pair(sK14_skl(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl),sK15_skl(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl))=sK2_skl(sK12_skl(sK1_skl,sK0_skl))|sQ48_spl),
% 29.21/4.12 inference(resolution,[status(thm)],[f2603,f189])).
% 29.21/4.12 fof(f3416,plain,(
% 29.21/4.12 sK15_skl(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl)=singleton(sK14_skl(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl))|sK9_skl(sK0_skl)=sK10_skl(sK0_skl)|sQ48_spl),
% 29.21/4.12 inference(resolution,[status(thm)],[f2603,f437])).
% 29.21/4.12 fof(f3418,plain,(
% 29.21/4.12 sP0_prd(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl)|sK15_skl(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl)=singleton(sK14_skl(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl))|sQ48_spl),
% 29.21/4.12 inference(resolution,[status(thm)],[f2603,f183])).
% 29.21/4.12 fof(f3421,plain,(
% 29.21/4.12 sP0_prd(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl)|sK13_skl(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl)=sK2_skl(sK12_skl(sK1_skl,sK0_skl))|sQ48_spl),
% 29.21/4.12 inference(resolution,[status(thm)],[f2603,f171])).
% 29.21/4.12 fof(f3422,definition,(
% 29.21/4.12 sQ73_spl <=> (ordered_pair(sK14_skl(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl),sK15_skl(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl))=sK2_skl(sK12_skl(sK1_skl,sK0_skl)))),
% 29.21/4.12 introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition])).
% 29.21/4.12 fof(f3423,plain,(
% 29.21/4.12 ordered_pair(sK14_skl(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl),sK15_skl(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl))=sK2_skl(sK12_skl(sK1_skl,sK0_skl))|~sQ73_spl),
% 29.21/4.12 inference(component_clause,[status(thm)],[f3422])).
% 29.21/4.12 fof(f3441,plain,(
% 29.21/4.12 sQ73_spl|sQ17_spl|sQ48_spl),
% 29.21/4.12 inference(split_clause,[status(thm)],[f3411,f3422,f2200,f2601])).
% 29.21/4.12 fof(f3443,plain,(
% 29.21/4.12 sQ18_spl|sQ73_spl|sQ48_spl),
% 29.21/4.12 inference(split_clause,[status(thm)],[f3413,f2207,f3422,f2601])).
% 29.21/4.12 fof(f3446,plain,(
% 29.21/4.12 sQ60_spl|sQ17_spl|sQ48_spl),
% 29.21/4.12 inference(split_clause,[status(thm)],[f3416,f2878,f2200,f2601])).
% 29.21/4.12 fof(f3448,plain,(
% 29.21/4.12 sQ18_spl|sQ60_spl|sQ48_spl),
% 29.21/4.12 inference(split_clause,[status(thm)],[f3418,f2207,f2878,f2601])).
% 29.21/4.12 fof(f3451,plain,(
% 29.21/4.12 sQ18_spl|sQ61_spl|sQ48_spl),
% 29.21/4.12 inference(split_clause,[status(thm)],[f3421,f2207,f2885,f2601])).
% 29.21/4.12 fof(f3480,plain,(
% 29.21/4.12 sP0_prd(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl)|sK13_skl(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl)=sK2_skl(sK12_skl(sK1_skl,sK0_skl))|sQ59_spl),
% 29.21/4.12 inference(resolution,[status(thm)],[f2877,f170])).
% 29.21/4.12 fof(f3514,plain,(
% 29.21/4.12 sQ18_spl|sQ61_spl|sQ59_spl),
% 29.21/4.12 inference(split_clause,[status(thm)],[f3480,f2207,f2885,f2875])).
% 29.21/4.12 fof(f3708,plain,(
% 29.21/4.12 ![X0]: (~in(sK2_skl(X0),X0)|~in(sK2_skl(X0),cartesian_product2(sK0_skl,sK1_skl))|~ordered_pair(sK14_skl(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl),sK15_skl(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl))=sK2_skl(X0)|~in(sK14_skl(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl),sK0_skl)|~sQ60_spl)),
% 29.21/4.12 inference(paramodulation,[status(thm)],[f2879,f77])).
% 29.21/4.12 fof(f3725,definition,(
% 29.21/4.12 ![X0]: (sQ75_spl <=> (~in(sK2_skl(X0),X0)|~in(sK2_skl(X0),cartesian_product2(sK0_skl,sK1_skl))|~ordered_pair(sK14_skl(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl),sK15_skl(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl))=sK2_skl(X0)))),
% 29.21/4.12 introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition])).
% 29.21/4.12 fof(f3726,plain,(
% 29.21/4.12 ![X0]: (~in(sK2_skl(X0),X0)|~in(sK2_skl(X0),cartesian_product2(sK0_skl,sK1_skl))|~ordered_pair(sK14_skl(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl),sK15_skl(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl))=sK2_skl(X0)|~sQ75_spl)),
% 29.21/4.12 inference(component_clause,[status(thm)],[f3725])).
% 29.21/4.12 fof(f3728,definition,(
% 29.21/4.12 sQ76_spl <=> (in(sK14_skl(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl),sK0_skl))),
% 29.21/4.12 introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition])).
% 29.21/4.12 fof(f3730,plain,(
% 29.21/4.12 ~in(sK14_skl(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl),sK0_skl)|sQ76_spl),
% 29.21/4.12 inference(component_clause,[status(thm)],[f3728])).
% 29.21/4.12 fof(f3731,plain,(
% 29.21/4.12 sQ75_spl|~sQ76_spl|~sQ60_spl),
% 29.21/4.12 inference(split_clause,[status(thm)],[f3708,f3725,f3728,f2878])).
% 29.21/4.12 fof(f3824,plain,(
% 29.21/4.12 ![X0]: (sK15_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl)=sK15_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl)|sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))|sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))|sK9_skl(sK0_skl)=sK10_skl(sK0_skl)|~sQ31_spl)),
% 29.21/4.12 inference(paramodulation,[status(thm)],[f468,f2381])).
% 29.21/4.12 fof(f3825,plain,(
% 29.21/4.12 ![X0]: (sK15_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl)=sK15_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl)|sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))|sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))|sK9_skl(sK0_skl)=sK11_skl(sK0_skl)|~sQ31_spl)),
% 29.21/4.12 inference(paramodulation,[status(thm)],[f467,f2381])).
% 29.21/4.12 fof(f3836,definition,(
% 29.21/4.12 ![X0]: (sQ77_spl <=> (sK15_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl)=sK15_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl)|sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))|sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))))),
% 29.21/4.12 introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition])).
% 29.21/4.12 fof(f3843,plain,(
% 29.21/4.12 sQ77_spl|sQ17_spl|~sQ31_spl),
% 29.21/4.12 inference(split_clause,[status(thm)],[f3824,f3836,f2200,f2380])).
% 29.21/4.12 fof(f3844,plain,(
% 29.21/4.12 sQ77_spl|sQ7_spl|~sQ31_spl),
% 29.21/4.12 inference(split_clause,[status(thm)],[f3825,f3836,f2148,f2380])).
% 29.21/4.12 fof(f3852,plain,(
% 29.21/4.12 ![X0]: (sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))|~in(sK2_skl(sK12_skl(X0,sK0_skl)),sK12_skl(X0,sK0_skl))|~in(sK2_skl(sK12_skl(X0,sK0_skl)),cartesian_product2(sK0_skl,sK1_skl))|~in(sK14_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl),sK0_skl)|sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))|sK9_skl(sK0_skl)=sK11_skl(sK0_skl)|~sQ27_spl)),
% 29.21/4.12 inference(resolution,[status(thm)],[f2353,f588])).
% 29.21/4.12 fof(f3861,plain,(
% 29.21/4.12 ![X0]: (sK2_skl(sK12_skl(X0,sK0_skl))=sK2_skl(sK12_skl(X0,sK0_skl))|sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))|ordered_pair(sK3_skl(sK12_skl(X0,sK0_skl)),sK4_skl(sK12_skl(X0,sK0_skl)))=sK2_skl(sK12_skl(X0,sK0_skl))|sK9_skl(sK0_skl)=sK10_skl(sK0_skl)|~sQ27_spl)),
% 29.21/4.12 inference(paramodulation,[status(thm)],[f525,f2353])).
% 29.21/4.12 fof(f3862,plain,(
% 29.21/4.12 ![X0]: (sK2_skl(sK12_skl(X0,sK0_skl))=sK2_skl(sK12_skl(X0,sK0_skl))|sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))|ordered_pair(sK3_skl(sK12_skl(X0,sK0_skl)),sK4_skl(sK12_skl(X0,sK0_skl)))=sK2_skl(sK12_skl(X0,sK0_skl))|sK9_skl(sK0_skl)=sK11_skl(sK0_skl)|~sQ27_spl)),
% 29.21/4.12 inference(paramodulation,[status(thm)],[f524,f2353])).
% 29.21/4.12 fof(f3864,plain,(
% 29.21/4.12 ![X0]: (sK2_skl(sK12_skl(X0,sK0_skl))=sK2_skl(sK12_skl(X0,sK0_skl))|sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))|sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))|sK9_skl(sK0_skl)=sK11_skl(sK0_skl)|~sQ27_spl)),
% 29.21/4.12 inference(paramodulation,[status(thm)],[f571,f2353])).
% 29.21/4.12 fof(f3865,plain,(
% 29.21/4.12 ![X0,X1]: (~in(sK2_skl(X0),X0)|~in(sK2_skl(X0),cartesian_product2(sK0_skl,sK1_skl))|~sK2_skl(sK12_skl(X1,sK0_skl))=sK2_skl(X0)|~in(sK14_skl(sK2_skl(sK12_skl(X1,sK0_skl)),X1,sK0_skl),sK0_skl)|sK4_skl(sK12_skl(X1,sK0_skl))=singleton(sK3_skl(sK12_skl(X1,sK0_skl)))|sK9_skl(sK0_skl)=sK11_skl(sK0_skl)|sK4_skl(sK12_skl(X1,sK0_skl))=singleton(sK3_skl(sK12_skl(X1,sK0_skl)))|~sQ27_spl)),
% 29.21/4.12 inference(paramodulation,[status(thm)],[f2353,f588])).
% 29.21/4.12 fof(f3879,definition,(
% 29.21/4.12 ![X0]: (sQ78_spl <=> (sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))|~in(sK2_skl(sK12_skl(X0,sK0_skl)),sK12_skl(X0,sK0_skl))|~in(sK2_skl(sK12_skl(X0,sK0_skl)),cartesian_product2(sK0_skl,sK1_skl))|~in(sK14_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl),sK0_skl)|sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))))),
% 29.21/4.12 introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition])).
% 29.21/4.12 fof(f3882,plain,(
% 29.21/4.12 sQ78_spl|sQ7_spl|~sQ27_spl),
% 29.21/4.12 inference(split_clause,[status(thm)],[f3852,f3879,f2148,f2352])).
% 29.21/4.12 fof(f3883,definition,(
% 29.21/4.12 ![X0]: (sQ79_spl <=> (sK2_skl(sK12_skl(X0,sK0_skl))=sK2_skl(sK12_skl(X0,sK0_skl))|sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))|ordered_pair(sK3_skl(sK12_skl(X0,sK0_skl)),sK4_skl(sK12_skl(X0,sK0_skl)))=sK2_skl(sK12_skl(X0,sK0_skl))))),
% 29.21/4.12 introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition])).
% 29.21/4.12 fof(f3894,plain,(
% 29.21/4.12 sQ79_spl|sQ17_spl|~sQ27_spl),
% 29.21/4.12 inference(split_clause,[status(thm)],[f3861,f3883,f2200,f2352])).
% 29.21/4.12 fof(f3895,plain,(
% 29.21/4.12 sQ79_spl|sQ7_spl|~sQ27_spl),
% 29.21/4.12 inference(split_clause,[status(thm)],[f3862,f3883,f2148,f2352])).
% 29.21/4.12 fof(f3897,plain,(
% 29.21/4.12 sQ49_spl|sQ7_spl|~sQ27_spl),
% 29.21/4.12 inference(split_clause,[status(thm)],[f3864,f2732,f2148,f2352])).
% 29.21/4.12 fof(f3898,definition,(
% 29.21/4.12 ![X0,X1]: (sQ80_spl <=> (~in(sK2_skl(X0),X0)|~in(sK2_skl(X0),cartesian_product2(sK0_skl,sK1_skl))|~sK2_skl(sK12_skl(X1,sK0_skl))=sK2_skl(X0)|~in(sK14_skl(sK2_skl(sK12_skl(X1,sK0_skl)),X1,sK0_skl),sK0_skl)|sK4_skl(sK12_skl(X1,sK0_skl))=singleton(sK3_skl(sK12_skl(X1,sK0_skl)))|sK4_skl(sK12_skl(X1,sK0_skl))=singleton(sK3_skl(sK12_skl(X1,sK0_skl)))))),
% 29.21/4.12 introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition])).
% 29.21/4.12 fof(f3899,plain,(
% 29.21/4.12 ![X0,X1]: (~in(sK2_skl(X0),X0)|~in(sK2_skl(X0),cartesian_product2(sK0_skl,sK1_skl))|~sK2_skl(sK12_skl(X1,sK0_skl))=sK2_skl(X0)|~in(sK14_skl(sK2_skl(sK12_skl(X1,sK0_skl)),X1,sK0_skl),sK0_skl)|sK4_skl(sK12_skl(X1,sK0_skl))=singleton(sK3_skl(sK12_skl(X1,sK0_skl)))|sK4_skl(sK12_skl(X1,sK0_skl))=singleton(sK3_skl(sK12_skl(X1,sK0_skl)))|~sQ80_spl)),
% 29.21/4.12 inference(component_clause,[status(thm)],[f3898])).
% 29.21/4.12 fof(f3901,plain,(
% 29.21/4.12 sQ80_spl|sQ7_spl|~sQ27_spl),
% 29.21/4.12 inference(split_clause,[status(thm)],[f3865,f3898,f2148,f2352])).
% 29.21/4.12 fof(f3915,plain,(
% 29.21/4.12 ![X0,X1]: (~in(sK2_skl(X0),X0)|~in(sK2_skl(X0),cartesian_product2(sK0_skl,sK1_skl))|~sK2_skl(sK12_skl(X1,sK0_skl))=sK2_skl(X0)|~in(sK14_skl(sK2_skl(sK12_skl(X1,sK0_skl)),X1,sK0_skl),sK0_skl)|sK4_skl(sK12_skl(X1,sK0_skl))=singleton(sK3_skl(sK12_skl(X1,sK0_skl)))|~sQ80_spl)),
% 29.21/4.12 inference(duplicate_literals_removal,[status(thm)],[f3899])).
% 29.21/4.12 fof(f3916,plain,(
% 29.21/4.12 ~in(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK12_skl(sK1_skl,sK0_skl))|~in(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),cartesian_product2(sK0_skl,sK1_skl))|sK4_skl(sK12_skl(sK1_skl,sK0_skl))=singleton(sK3_skl(sK12_skl(sK1_skl,sK0_skl)))|~sQ75_spl|~sQ27_spl),
% 29.21/4.12 inference(resolution,[status(thm)],[f3726,f2353])).
% 29.21/4.12 fof(f3925,plain,(
% 29.21/4.12 ~in(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK12_skl(sK1_skl,sK0_skl))|~in(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),cartesian_product2(sK0_skl,sK1_skl))|ordered_pair(sK3_skl(sK12_skl(sK1_skl,sK0_skl)),sK4_skl(sK12_skl(sK1_skl,sK0_skl)))=sK2_skl(sK12_skl(sK1_skl,sK0_skl))|sK9_skl(sK0_skl)=sK10_skl(sK0_skl)|~sQ75_spl),
% 29.21/4.12 inference(resolution,[status(thm)],[f3726,f525])).
% 29.21/4.12 fof(f3942,plain,(
% 29.21/4.12 ~sQ58_spl|~sQ59_spl|sQ46_spl|~sQ75_spl|~sQ27_spl),
% 29.21/4.12 inference(split_clause,[status(thm)],[f3916,f2872,f2875,f2586,f3725,f2352])).
% 29.21/4.12 fof(f3951,plain,(
% 29.21/4.12 ~sQ58_spl|~sQ59_spl|sQ71_spl|sQ17_spl|~sQ75_spl),
% 29.21/4.12 inference(split_clause,[status(thm)],[f3925,f2872,f2875,f3311,f2200,f3725])).
% 29.21/4.12 fof(f3968,plain,(
% 29.21/4.12 ![X0]: (~in(sK2_skl(X0),X0)|~in(sK2_skl(X0),cartesian_product2(sK0_skl,sK1_skl))|~sK2_skl(sK12_skl(sK1_skl,sK0_skl))=sK2_skl(X0)|~sQ71_spl|~sQ47_spl)),
% 29.21/4.12 inference(backward_demodulation,[status(thm)],[f3312,f2599])).
% 29.21/4.12 fof(f3969,plain,(
% 29.21/4.12 ![X0,X1]: (sP0_prd(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0)|in(ordered_pair(sK3_skl(sK12_skl(sK1_skl,sK0_skl)),sK4_skl(sK12_skl(sK1_skl,sK0_skl))),sK12_skl(X1,X0))|~in(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),cartesian_product2(X0,X1))|~in(sK3_skl(sK12_skl(sK1_skl,sK0_skl)),X0)|~sQ71_spl|~sQ46_spl)),
% 29.21/4.12 inference(backward_demodulation,[status(thm)],[f3312,f2597])).
% 29.21/4.12 fof(f3972,plain,(
% 29.21/4.12 ![X0,X1]: (sP0_prd(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0)|in(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK12_skl(X1,X0))|~in(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),cartesian_product2(X0,X1))|~in(sK3_skl(sK12_skl(sK1_skl,sK0_skl)),X0)|~sQ71_spl|~sQ46_spl)),
% 29.21/4.12 inference(forward_demodulation,[status(thm)],[f3312,f3969])).
% 29.21/4.12 fof(f3988,plain,(
% 29.21/4.12 sK9_skl(sK0_skl)=sK11_skl(sK0_skl)|~sQ18_spl),
% 29.21/4.12 inference(resolution,[status(thm)],[f2208,f71])).
% 29.21/4.12 fof(f3989,plain,(
% 29.21/4.12 sK9_skl(sK0_skl)=sK10_skl(sK0_skl)|~sQ18_spl),
% 29.21/4.12 inference(resolution,[status(thm)],[f2208,f67])).
% 29.21/4.12 fof(f3990,plain,(
% 29.21/4.12 sQ7_spl|~sQ18_spl),
% 29.21/4.12 inference(split_clause,[status(thm)],[f3988,f2148,f2207])).
% 29.21/4.12 fof(f3991,plain,(
% 29.21/4.12 sQ17_spl|~sQ18_spl),
% 29.21/4.12 inference(split_clause,[status(thm)],[f3989,f2200,f2207])).
% 29.21/4.12 fof(f4011,plain,(
% 29.21/4.12 ![X0]: (sK15_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl)=singleton(sK14_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl))|ordered_pair(sK3_skl(sK12_skl(X0,sK0_skl)),sK4_skl(sK12_skl(X0,sK0_skl)))=sK2_skl(sK12_skl(X0,sK0_skl))|sQ18_spl)),
% 29.21/4.12 inference(resolution,[status(thm)],[f2209,f184])).
% 29.21/4.12 fof(f4014,plain,(
% 29.21/4.12 ![X0]: (in(sK14_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl),sK0_skl)|sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))|sQ18_spl)),
% 29.21/4.12 inference(resolution,[status(thm)],[f2209,f179])).
% 29.21/4.12 fof(f4018,plain,(
% 29.21/4.12 ![X0]: (sK13_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl)=sK2_skl(sK12_skl(X0,sK0_skl))|ordered_pair(sK3_skl(sK12_skl(X0,sK0_skl)),sK4_skl(sK12_skl(X0,sK0_skl)))=sK2_skl(sK12_skl(X0,sK0_skl))|sQ18_spl)),
% 29.21/4.12 inference(resolution,[status(thm)],[f2209,f172])).
% 29.21/4.12 fof(f4050,plain,(
% 29.21/4.12 sK4_skl(sK12_skl(sK1_skl,sK0_skl))=singleton(sK3_skl(sK12_skl(sK1_skl,sK0_skl)))|sK9_skl(sK0_skl)=sK10_skl(sK0_skl)|sQ76_spl),
% 29.21/4.12 inference(resolution,[status(thm)],[f3730,f402])).
% 29.21/4.12 fof(f4052,plain,(
% 29.21/4.12 sP0_prd(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl)|sK4_skl(sK12_skl(sK1_skl,sK0_skl))=singleton(sK3_skl(sK12_skl(sK1_skl,sK0_skl)))|sQ76_spl),
% 29.21/4.12 inference(resolution,[status(thm)],[f3730,f179])).
% 29.21/4.12 fof(f4059,plain,(
% 29.21/4.12 in(sK3_skl(sK12_skl(sK1_skl,sK0_skl)),sK0_skl)|sK9_skl(sK0_skl)=sK10_skl(sK0_skl)|sQ76_spl),
% 29.21/4.12 inference(resolution,[status(thm)],[f3730,f199])).
% 29.21/4.12 fof(f4061,plain,(
% 29.21/4.12 sP0_prd(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl)|in(sK3_skl(sK12_skl(sK1_skl,sK0_skl)),sK0_skl)|sQ76_spl),
% 29.21/4.12 inference(resolution,[status(thm)],[f3730,f177])).
% 29.21/4.12 fof(f4086,plain,(
% 29.21/4.12 sQ46_spl|sQ17_spl|sQ76_spl),
% 29.21/4.12 inference(split_clause,[status(thm)],[f4050,f2586,f2200,f3728])).
% 29.21/4.12 fof(f4088,plain,(
% 29.21/4.12 sQ18_spl|sQ46_spl|sQ76_spl),
% 29.21/4.12 inference(split_clause,[status(thm)],[f4052,f2207,f2586,f3728])).
% 29.21/4.12 fof(f4095,plain,(
% 29.21/4.12 sQ48_spl|sQ17_spl|sQ76_spl),
% 29.21/4.12 inference(split_clause,[status(thm)],[f4059,f2601,f2200,f3728])).
% 29.21/4.12 fof(f4097,plain,(
% 29.21/4.12 sQ18_spl|sQ48_spl|sQ76_spl),
% 29.21/4.12 inference(split_clause,[status(thm)],[f4061,f2207,f2601,f3728])).
% 29.21/4.12 fof(f4128,plain,(
% 29.21/4.12 sK4_skl(sK12_skl(sK1_skl,sK0_skl))=singleton(sK3_skl(sK12_skl(sK1_skl,sK0_skl)))|sQ61_spl|~sQ37_spl),
% 29.21/4.12 inference(resolution,[status(thm)],[f2887,f2423])).
% 29.21/4.12 fof(f4204,plain,(
% 29.21/4.12 ![X0,X1]: (~in(sK2_skl(X0),X0)|~in(sK2_skl(X0),cartesian_product2(sK0_skl,sK1_skl))|~sK2_skl(sK12_skl(X1,sK0_skl))=sK2_skl(X0)|sK4_skl(sK12_skl(X1,sK0_skl))=singleton(sK3_skl(sK12_skl(X1,sK0_skl)))|sQ18_spl|~sQ80_spl)),
% 29.21/4.12 inference(forward_subsumption_resolution,[status(thm)],[f3915,f4014])).
% 29.21/4.12 fof(f4495,plain,(
% 29.21/4.12 ~in(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK12_skl(sK1_skl,sK0_skl))|~in(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),cartesian_product2(sK0_skl,sK1_skl))|~sQ71_spl|~sQ47_spl),
% 29.21/4.12 inference(equality_resolution,[status(thm)],[f3968])).
% 29.21/4.12 fof(f4496,plain,(
% 29.21/4.12 ~sQ58_spl|~sQ59_spl|~sQ71_spl|~sQ47_spl),
% 29.21/4.12 inference(split_clause,[status(thm)],[f4495,f2872,f2875,f3311,f2598])).
% 29.21/4.12 fof(f4498,plain,(
% 29.21/4.12 in(sK3_skl(sK12_skl(sK1_skl,sK0_skl)),sK0_skl)|sQ58_spl),
% 29.21/4.12 inference(resolution,[status(thm)],[f2874,f22])).
% 29.21/4.12 fof(f4499,plain,(
% 29.21/4.12 ordered_pair(sK3_skl(sK12_skl(sK1_skl,sK0_skl)),sK4_skl(sK12_skl(sK1_skl,sK0_skl)))=sK2_skl(sK12_skl(sK1_skl,sK0_skl))|sQ58_spl),
% 29.21/4.12 inference(resolution,[status(thm)],[f2874,f21])).
% 29.21/4.12 fof(f4500,plain,(
% 29.21/4.12 sK4_skl(sK12_skl(sK1_skl,sK0_skl))=singleton(sK3_skl(sK12_skl(sK1_skl,sK0_skl)))|sQ58_spl),
% 29.21/4.12 inference(resolution,[status(thm)],[f2874,f23])).
% 29.21/4.12 fof(f4715,plain,(
% 29.21/4.12 ![X0]: (sK13_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl)=sK2_skl(sK12_skl(X0,sK0_skl))|sK2_skl(sK12_skl(X0,sK0_skl))=sK2_skl(sK12_skl(X0,sK0_skl))|sK15_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl)=singleton(sK14_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl))|sK9_skl(sK0_skl)=sK10_skl(sK0_skl)|sQ18_spl)),
% 29.21/4.12 inference(paramodulation,[status(thm)],[f460,f4018])).
% 29.21/4.12 fof(f4716,plain,(
% 29.21/4.12 ![X0]: (sK13_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl)=sK2_skl(sK12_skl(X0,sK0_skl))|sK2_skl(sK12_skl(X0,sK0_skl))=sK2_skl(sK12_skl(X0,sK0_skl))|sK15_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl)=singleton(sK14_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl))|sK9_skl(sK0_skl)=sK11_skl(sK0_skl)|sQ18_spl)),
% 29.21/4.12 inference(paramodulation,[status(thm)],[f459,f4018])).
% 29.21/4.12 fof(f4717,plain,(
% 29.21/4.12 ![X0]: (sK13_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl)=sK2_skl(sK12_skl(X0,sK0_skl))|sK2_skl(sK12_skl(X0,sK0_skl))=sK2_skl(sK12_skl(X0,sK0_skl))|sK13_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl)=sK2_skl(sK12_skl(X0,sK0_skl))|sK9_skl(sK0_skl)=sK10_skl(sK0_skl)|sQ18_spl)),
% 29.21/4.12 inference(paramodulation,[status(thm)],[f256,f4018])).
% 29.21/4.12 fof(f4718,plain,(
% 29.21/4.12 ![X0]: (sK13_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl)=sK2_skl(sK12_skl(X0,sK0_skl))|sK2_skl(sK12_skl(X0,sK0_skl))=sK2_skl(sK12_skl(X0,sK0_skl))|sK13_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl)=sK2_skl(sK12_skl(X0,sK0_skl))|sK9_skl(sK0_skl)=sK11_skl(sK0_skl)|sQ18_spl)),
% 29.21/4.12 inference(paramodulation,[status(thm)],[f255,f4018])).
% 29.21/4.12 fof(f4734,definition,(
% 29.21/4.12 ![X0]: (sQ81_spl <=> (sK13_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl)=sK2_skl(sK12_skl(X0,sK0_skl))|sK2_skl(sK12_skl(X0,sK0_skl))=sK2_skl(sK12_skl(X0,sK0_skl))|sK15_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl)=singleton(sK14_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl))))),
% 29.21/4.12 introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition])).
% 29.21/4.12 fof(f4741,definition,(
% 29.21/4.12 ![X0]: (sQ82_spl <=> (sK13_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl)=sK2_skl(sK12_skl(X0,sK0_skl))|sK2_skl(sK12_skl(X0,sK0_skl))=sK2_skl(sK12_skl(X0,sK0_skl))|sK13_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl)=sK2_skl(sK12_skl(X0,sK0_skl))))),
% 29.21/4.12 introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition])).
% 29.21/4.12 fof(f4748,plain,(
% 29.21/4.12 sQ81_spl|sQ17_spl|sQ18_spl),
% 29.21/4.12 inference(split_clause,[status(thm)],[f4715,f4734,f2200,f2207])).
% 29.21/4.12 fof(f4749,plain,(
% 29.21/4.12 sQ81_spl|sQ7_spl|sQ18_spl),
% 29.21/4.12 inference(split_clause,[status(thm)],[f4716,f4734,f2148,f2207])).
% 29.21/4.12 fof(f4750,plain,(
% 29.21/4.12 sQ82_spl|sQ17_spl|sQ18_spl),
% 29.21/4.12 inference(split_clause,[status(thm)],[f4717,f4741,f2200,f2207])).
% 29.21/4.12 fof(f4751,plain,(
% 29.21/4.12 sQ82_spl|sQ7_spl|sQ18_spl),
% 29.21/4.12 inference(split_clause,[status(thm)],[f4718,f4741,f2148,f2207])).
% 29.21/4.12 fof(f4820,plain,(
% 29.21/4.12 ![X0]: (~in(sK2_skl(cartesian_product2(sK0_skl,sK1_skl)),cartesian_product2(sK0_skl,sK1_skl))|~sK2_skl(sK12_skl(X0,sK0_skl))=sK2_skl(cartesian_product2(sK0_skl,sK1_skl))|sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))|sQ18_spl|~sQ80_spl)),
% 29.21/4.12 inference(resolution,[status(thm)],[f4204,f80])).
% 29.21/4.12 fof(f4839,definition,(
% 29.21/4.12 sQ84_spl <=> (in(sK2_skl(cartesian_product2(sK0_skl,sK1_skl)),cartesian_product2(sK0_skl,sK1_skl)))),
% 29.21/4.12 introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition])).
% 29.21/4.12 fof(f4841,plain,(
% 29.21/4.12 ~in(sK2_skl(cartesian_product2(sK0_skl,sK1_skl)),cartesian_product2(sK0_skl,sK1_skl))|sQ84_spl),
% 29.21/4.12 inference(component_clause,[status(thm)],[f4839])).
% 29.21/4.12 fof(f4842,definition,(
% 29.21/4.12 ![X0]: (sQ85_spl <=> (~sK2_skl(sK12_skl(X0,sK0_skl))=sK2_skl(cartesian_product2(sK0_skl,sK1_skl))|sK4_skl(sK12_skl(X0,sK0_skl))=singleton(sK3_skl(sK12_skl(X0,sK0_skl)))))),
% 29.21/4.12 introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition])).
% 29.21/4.12 fof(f4845,plain,(
% 29.21/4.12 ~sQ84_spl|sQ85_spl|sQ18_spl|~sQ80_spl),
% 29.21/4.12 inference(split_clause,[status(thm)],[f4820,f4839,f4842,f2207,f3898])).
% 29.21/4.12 fof(f4861,plain,(
% 29.21/4.12 $false|sQ84_spl),
% 29.21/4.12 inference(forward_subsumption_resolution,[status(thm)],[f4841,f80])).
% 29.21/4.12 fof(f4862,plain,(
% 29.21/4.12 sQ84_spl),
% 29.21/4.12 inference(contradiction_clause,[status(thm)],[f4861])).
% 29.21/4.12 fof(f4934,plain,(
% 29.21/4.12 ![X0]: (sK15_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl)=singleton(sK14_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl))|sK2_skl(sK12_skl(X0,sK0_skl))=sK2_skl(sK12_skl(X0,sK0_skl))|sK15_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl)=singleton(sK14_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl))|sK9_skl(sK0_skl)=sK10_skl(sK0_skl)|sQ18_spl)),
% 29.21/4.12 inference(paramodulation,[status(thm)],[f460,f4011])).
% 29.21/4.12 fof(f4935,plain,(
% 29.21/4.12 ![X0]: (sK15_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl)=singleton(sK14_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl))|sK2_skl(sK12_skl(X0,sK0_skl))=sK2_skl(sK12_skl(X0,sK0_skl))|sK15_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl)=singleton(sK14_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl))|sK9_skl(sK0_skl)=sK11_skl(sK0_skl)|sQ18_spl)),
% 29.21/4.12 inference(paramodulation,[status(thm)],[f459,f4011])).
% 29.21/4.12 fof(f4954,definition,(
% 29.21/4.12 ![X0]: (sQ89_spl <=> (sK15_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl)=singleton(sK14_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl))|sK2_skl(sK12_skl(X0,sK0_skl))=sK2_skl(sK12_skl(X0,sK0_skl))|sK15_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl)=singleton(sK14_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl))))),
% 29.21/4.12 introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition])).
% 29.21/4.12 fof(f4965,plain,(
% 29.21/4.12 sQ89_spl|sQ17_spl|sQ18_spl),
% 29.21/4.12 inference(split_clause,[status(thm)],[f4934,f4954,f2200,f2207])).
% 29.21/4.12 fof(f4966,plain,(
% 29.21/4.12 sQ89_spl|sQ7_spl|sQ18_spl),
% 29.21/4.12 inference(split_clause,[status(thm)],[f4935,f4954,f2148,f2207])).
% 29.21/4.12 fof(f5032,plain,(
% 29.21/4.12 sP0_prd(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl)|in(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK12_skl(sK1_skl,sK0_skl))|~in(sK3_skl(sK12_skl(sK1_skl,sK0_skl)),sK0_skl)|in(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK12_skl(sK1_skl,sK0_skl))|~sQ71_spl|~sQ46_spl),
% 29.21/4.12 inference(resolution,[status(thm)],[f3972,f20])).
% 29.21/4.12 fof(f5071,plain,(
% 29.21/4.12 sQ18_spl|sQ58_spl|~sQ48_spl|~sQ71_spl|~sQ46_spl),
% 29.21/4.12 inference(split_clause,[status(thm)],[f5032,f2207,f2872,f2601,f3311,f2586])).
% 29.21/4.12 fof(f5073,plain,(
% 29.21/4.12 sQ48_spl|sQ58_spl),
% 29.21/4.12 inference(split_clause,[status(thm)],[f4498,f2601,f2872])).
% 29.21/4.12 fof(f5075,plain,(
% 29.21/4.12 ![X0]: (~in(sK2_skl(X0),X0)|~in(sK2_skl(X0),cartesian_product2(sK0_skl,sK1_skl))|~sK2_skl(sK12_skl(sK1_skl,sK0_skl))=sK2_skl(X0)|~sQ73_spl|~sQ75_spl)),
% 29.21/4.12 inference(forward_demodulation,[status(thm)],[f3423,f3726])).
% 29.21/4.12 fof(f5080,plain,(
% 29.21/4.12 ~sK2_skl(sK12_skl(sK1_skl,sK0_skl))=sK2_skl(sK12_skl(sK1_skl,sK0_skl))|sQ58_spl|sQ71_spl),
% 29.21/4.12 inference(forward_demodulation,[status(thm)],[f4499,f3313])).
% 29.21/4.12 fof(f5081,plain,(
% 29.21/4.12 $false|sQ58_spl|sQ71_spl),
% 29.21/4.12 inference(trivial_equality_resolution,[status(thm)],[f5080])).
% 29.21/4.12 fof(f5082,plain,(
% 29.21/4.12 sQ58_spl|sQ71_spl),
% 29.21/4.12 inference(contradiction_clause,[status(thm)],[f5081])).
% 29.21/4.12 fof(f5145,plain,(
% 29.21/4.12 sP0_prd(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl)|ordered_pair(sK14_skl(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl),sK15_skl(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl))=sK2_skl(sK12_skl(sK1_skl,sK0_skl))|~sQ58_spl),
% 29.21/4.12 inference(resolution,[status(thm)],[f2873,f60])).
% 29.21/4.12 fof(f5146,plain,(
% 29.21/4.12 sP0_prd(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl)|sK15_skl(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl)=singleton(sK14_skl(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl))|~sQ58_spl),
% 29.21/4.12 inference(resolution,[status(thm)],[f2873,f62])).
% 29.21/4.12 fof(f5147,plain,(
% 29.21/4.12 sP0_prd(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl)|in(sK14_skl(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl),sK0_skl)|~sQ58_spl),
% 29.21/4.12 inference(resolution,[status(thm)],[f2873,f61])).
% 29.21/4.12 fof(f5148,plain,(
% 29.21/4.12 sP0_prd(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl)|sK13_skl(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl)=sK2_skl(sK12_skl(sK1_skl,sK0_skl))|~sQ58_spl),
% 29.21/4.12 inference(resolution,[status(thm)],[f2873,f59])).
% 29.21/4.12 fof(f5151,plain,(
% 29.21/4.12 sQ18_spl|sQ73_spl|~sQ58_spl),
% 29.21/4.12 inference(split_clause,[status(thm)],[f5145,f2207,f3422,f2872])).
% 29.21/4.12 fof(f5152,plain,(
% 29.21/4.12 sQ18_spl|sQ60_spl|~sQ58_spl),
% 29.21/4.12 inference(split_clause,[status(thm)],[f5146,f2207,f2878,f2872])).
% 29.21/4.12 fof(f5153,plain,(
% 29.21/4.12 sQ18_spl|sQ76_spl|~sQ58_spl),
% 29.21/4.12 inference(split_clause,[status(thm)],[f5147,f2207,f3728,f2872])).
% 29.21/4.14 fof(f5154,plain,(
% 29.21/4.14 sQ18_spl|sQ61_spl|~sQ58_spl),
% 29.21/4.14 inference(split_clause,[status(thm)],[f5148,f2207,f2885,f2872])).
% 29.21/4.14 fof(f5430,plain,(
% 29.21/4.14 ~in(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK12_skl(sK1_skl,sK0_skl))|~in(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),cartesian_product2(sK0_skl,sK1_skl))|~sQ73_spl|~sQ75_spl),
% 29.21/4.14 inference(equality_resolution,[status(thm)],[f5075])).
% 29.21/4.14 fof(f5431,plain,(
% 29.21/4.14 ~sQ58_spl|~sQ59_spl|~sQ73_spl|~sQ75_spl),
% 29.21/4.14 inference(split_clause,[status(thm)],[f5430,f2872,f2875,f3422,f3725])).
% 29.21/4.14 fof(f5432,plain,(
% 29.21/4.14 sQ46_spl|sQ61_spl|~sQ37_spl),
% 29.21/4.14 inference(split_clause,[status(thm)],[f4128,f2586,f2885,f2422])).
% 29.21/4.14 fof(f5434,plain,(
% 29.21/4.14 sP0_prd(sK11_skl(sK0_skl),sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl)|~sQ17_spl|~sQ18_spl),
% 29.21/4.14 inference(backward_demodulation,[status(thm)],[f2201,f2208])).
% 29.21/4.14 fof(f5448,plain,(
% 29.21/4.14 $false|sQ70_spl),
% 29.21/4.14 inference(trivial_equality_resolution,[status(thm)],[f3302])).
% 29.21/4.14 fof(f5449,plain,(
% 29.21/4.14 sQ70_spl),
% 29.21/4.14 inference(contradiction_clause,[status(thm)],[f5448])).
% 29.21/4.14 fof(f5450,plain,(
% 29.21/4.14 sP0_prd(sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl)|~sQ7_spl|~sQ63_spl),
% 29.21/4.14 inference(backward_demodulation,[status(thm)],[f2149,f3032])).
% 29.21/4.14 fof(f5459,plain,(
% 29.21/4.14 sP0_prd(sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl)|~sQ7_spl|~sQ17_spl|~sQ18_spl),
% 29.21/4.14 inference(forward_demodulation,[status(thm)],[f2149,f5434])).
% 29.21/4.14 fof(f5460,plain,(
% 29.21/4.14 $false|~sQ7_spl|~sQ17_spl|~sQ18_spl),
% 29.21/4.14 inference(forward_subsumption_resolution,[status(thm)],[f5459,f79])).
% 29.21/4.14 fof(f5461,plain,(
% 29.21/4.14 ~sQ7_spl|~sQ17_spl|~sQ18_spl),
% 29.21/4.14 inference(contradiction_clause,[status(thm)],[f5460])).
% 29.21/4.14 fof(f5476,plain,(
% 29.21/4.14 $false|~sQ7_spl|~sQ63_spl),
% 29.21/4.14 inference(forward_subsumption_resolution,[status(thm)],[f5450,f79])).
% 29.21/4.14 fof(f5477,plain,(
% 29.21/4.14 ~sQ7_spl|~sQ63_spl),
% 29.21/4.14 inference(contradiction_clause,[status(thm)],[f5476])).
% 29.21/4.14 fof(f5479,plain,(
% 29.21/4.14 sQ46_spl|sQ58_spl),
% 29.21/4.14 inference(split_clause,[status(thm)],[f4500,f2586,f2872])).
% 29.21/4.14 fof(f5482,plain,(
% 29.21/4.14 $false),
% 29.21/4.14 inference(sat_refutation,[status(thm)],[f96,f98,f108,f110,f165,f167,f2204,f2206,f2214,f2218,f2328,f2332,f2461,f2465,f2466,f2467,f2479,f2480,f2481,f2486,f2487,f2488,f2491,f2492,f2494,f2495,f2496,f2497,f2498,f2499,f2500,f2504,f2523,f2576,f2580,f2584,f2604,f2739,f2791,f2814,f2815,f2816,f2817,f2818,f2819,f2823,f2824,f2825,f2826,f2827,f2828,f2829,f2830,f2831,f2832,f2833,f2837,f2838,f2839,f2840,f2841,f2842,f2847,f2892,f3037,f3041,f3177,f3382,f3383,f3385,f3441,f3443,f3446,f3448,f3451,f3514,f3731,f3843,f3844,f3882,f3894,f3895,f3897,f3901,f3942,f3951,f3990,f3991,f4086,f4088,f4095,f4097,f4496,f4748,f4749,f4750,f4751,f4845,f4862,f4965,f4966,f5071,f5073,f5082,f5151,f5152,f5153,f5154,f5431,f5432,f5449,f5461,f5477,f5479])).
% 29.21/4.14 % SZS output end CNFRefutation for theBenchmark.p
% 29.21/4.15 % Elapsed time: 3.759653 seconds
% 29.21/4.15 % CPU time: 29.494382 seconds
% 29.21/4.15 % Total memory used: 290.786 MB
% 29.21/4.15 % Net memory used: 261.659 MB
%------------------------------------------------------------------------------