%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU430+2 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n012.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 02:22:39 PM UTC 2026
% Result : Theorem 5.64s 1.24s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SEU430+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.02 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.03/0.30 % Computer : n012.cluster.edu
% 0.03/0.30 % Model : x86_64 x86_64
% 0.03/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.30 % Memory : 8046.5625MB
% 0.03/0.30 % OS : Linux 6.8.0-71-generic
% 0.03/0.30 % CPULimit : 300
% 0.03/0.30 % WCLimit : 300
% 0.03/0.30 % DateTime : Mon Sep 21 06:28:09 UTC 2026
% 0.03/0.30 % CPUTime :
% 0.18/0.48 % Drodi V4.1.1
% 5.64/1.24 % Refutation found
% 5.64/1.24 % SZS status Theorem for theBenchmark: Theorem is valid
% 5.64/1.24 % SZS output start CNFRefutation for theBenchmark
% 5.64/1.24 fof(f1,axiom,(
% 5.64/1.24 (! [A,B] :( r2_hidden(A,B)=> ~ r2_hidden(B,A) ) )),
% 5.64/1.24 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.64/1.24 fof(f3,axiom,(
% 5.64/1.24 (! [A,B] :( (! [C] :( r2_hidden(C,A)<=> r2_hidden(C,B) ))=> A = B ) )),
% 5.64/1.24 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.64/1.24 fof(f4,axiom,(
% 5.64/1.24 (! [A,B] :( B = k1_tarski(A)<=> (! [C] :( r2_hidden(C,B)<=> C = A ) )) )),
% 5.64/1.24 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.64/1.24 fof(f9,axiom,(
% 5.64/1.24 (! [A,B] :( B = k3_tarski(A)<=> (! [C] :( r2_hidden(C,B)<=> (? [D] :( r2_hidden(C,D)& r2_hidden(D,A) ) )) )) )),
% 5.64/1.24 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.64/1.24 fof(f12,axiom,(
% 5.64/1.24 (! [A,B] :~ ( r2_hidden(A,B)& (! [C] :~ ( r2_hidden(C,B)& (! [D] :~ ( r2_hidden(D,B)& r2_hidden(D,C) ) )) )) )),
% 5.64/1.24 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.64/1.24 fof(f18,axiom,(
% 5.64/1.24 (! [A,B] : r1_tarski(A,A) )),
% 5.64/1.24 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.64/1.24 fof(f24,axiom,(
% 5.64/1.24 v1_xboole_0(k1_xboole_0) ),
% 5.64/1.24 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.64/1.24 fof(f25,axiom,(
% 5.64/1.24 (? [A] : v1_xboole_0(A) )),
% 5.64/1.24 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.64/1.24 fof(f29,axiom,(
% 5.64/1.24 (! [A] :( A = k1_xboole_0<=> (! [B] : ~ r2_hidden(B,A) )) )),
% 5.64/1.24 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.64/1.24 fof(f30,axiom,(
% 5.64/1.24 (! [A,B,C] :( C = k2_xboole_0(A,B)<=> (! [D] :( r2_hidden(D,C)<=> ( r2_hidden(D,A)| r2_hidden(D,B) ) ) )) )),
% 5.64/1.24 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.64/1.24 fof(f185,axiom,(
% 5.64/1.24 (! [A,B] :( B = k1_zfmisc_1(A)<=> (! [C] :( r2_hidden(C,B)<=> r1_tarski(C,A) ) )) )),
% 5.64/1.24 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.64/1.24 fof(f334,axiom,(
% 5.64/1.24 (! [A] : ~ v1_xboole_0(k1_zfmisc_1(A)) )),
% 5.64/1.24 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.64/1.24 fof(f349,axiom,(
% 5.64/1.24 (! [A] : m1_subset_1(k1_xboole_0,k1_zfmisc_1(A)) )),
% 5.64/1.24 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.64/1.24 fof(f421,axiom,(
% 5.64/1.24 (! [A,B] :( ( ~ v1_xboole_0(A)& ~ v1_xboole_0(B) )=> ~ r1_subset_1(A,A) ) )),
% 5.64/1.24 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.64/1.24 fof(f424,axiom,(
% 5.64/1.24 (! [A,B] :( ( ~ v1_xboole_0(A)& ~ v1_xboole_0(B) )=> ~ r2_subset_1(A,A) ) )),
% 5.64/1.24 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.64/1.24 fof(f531,axiom,(
% 5.64/1.24 (! [A,B] :( m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A)))=> m1_subset_1(k5_setfam_1(A,B),k1_zfmisc_1(A)) ) )),
% 5.64/1.24 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.64/1.24 fof(f532,axiom,(
% 5.64/1.24 (! [A,B] :( m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A)))=> k5_setfam_1(A,B) = k3_tarski(B) ) )),
% 5.64/1.24 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.64/1.24 fof(f538,axiom,(
% 5.64/1.24 ((! [A,B] :( r2_hidden(A,B)=> m1_subset_1(A,B) ) ))),
% 5.64/1.24 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.64/1.24 fof(f540,axiom,(
% 5.64/1.24 ((! [A,B] :( m1_subset_1(A,k1_zfmisc_1(B))<=> r1_tarski(A,B) ) ))),
% 5.64/1.24 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.64/1.24 fof(f542,axiom,(
% 5.64/1.24 ((! [A,B,C] :~ ( r2_hidden(A,B)& m1_subset_1(B,k1_zfmisc_1(C))& v1_xboole_0(C) ) ))),
% 5.64/1.24 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.64/1.24 fof(f1051,axiom,(
% 5.64/1.24 (! [A,B,C,D] :~ ( r2_hidden(A,B)& r2_hidden(B,C)& r2_hidden(C,D)& r2_hidden(D,A) ) )),
% 5.64/1.24 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.64/1.24 fof(f1053,axiom,(
% 5.64/1.24 (! [A,B,C,D,E,F] :~ ( r2_hidden(A,B)& r2_hidden(B,C)& r2_hidden(C,D)& r2_hidden(D,E)& r2_hidden(E,F)& r2_hidden(F,A) ) )),
% 5.64/1.24 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.64/1.24 fof(f3616,axiom,(
% 5.64/1.24 (! [A,B] :( m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A)))=> ( B != k1_xboole_0=> r1_tarski(k8_setfam_1(A,B),k5_setfam_1(A,B)) ) ) )),
% 5.64/1.24 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.64/1.24 fof(f4502,conjecture,(
% 5.64/1.24 (! [A,B] :( m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A)))=> ( k5_setfam_1(A,B) = k1_xboole_0<=> (! [C] :( r2_hidden(C,B)=> C = k1_xboole_0 ) )) ) )),
% 5.64/1.24 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.64/1.24 fof(f4503,negated_conjecture,(
% 5.64/1.24 ~((! [A,B] :( m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A)))=> ( k5_setfam_1(A,B) = k1_xboole_0<=> (! [C] :( r2_hidden(C,B)=> C = k1_xboole_0 ) )) ) ))),
% 5.64/1.24 inference(negated_conjecture,[status(cth)],[f4502])).
% 5.64/1.24 fof(f4504,plain,(
% 5.64/1.24 ![A,B]: (~r2_hidden(A,B)|~r2_hidden(B,A))),
% 5.64/1.24 inference(pre_NNF_transformation,[status(thm)],[f1])).
% 5.64/1.24 fof(f4505,plain,(
% 5.64/1.24 ![X0,X1]: (~r2_hidden(X0,X1)|~r2_hidden(X1,X0))),
% 5.64/1.24 inference(cnf_transformation,[status(thm)],[f4504])).
% 5.64/1.24 fof(f4506,plain,(
% 5.64/1.24 ![A,B]: ((?[C]: (r2_hidden(C,A)<~>r2_hidden(C,B)))|A=B)),
% 5.64/1.24 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 5.64/1.24 fof(f4507,plain,(
% 5.64/1.24 ![A,B]: ((?[C]: ((r2_hidden(C,A)|r2_hidden(C,B))&(~r2_hidden(C,A)|~r2_hidden(C,B))))|A=B)),
% 5.64/1.24 inference(NNF_transformation,[status(thm)],[f4506])).
% 5.64/1.24 fof(f4508,plain,(
% 5.64/1.24 ![A,B]: (((r2_hidden(sK0_skl(B,A),A)|r2_hidden(sK0_skl(B,A),B))&(~r2_hidden(sK0_skl(B,A),A)|~r2_hidden(sK0_skl(B,A),B)))|A=B)),
% 5.64/1.24 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(C,sK0_skl(B,A))],[f4507])).
% 5.64/1.24 fof(f4509,plain,(
% 5.64/1.24 ![X0,X1]: (r2_hidden(sK0_skl(X0,X1),X1)|r2_hidden(sK0_skl(X0,X1),X0)|X1=X0)),
% 5.64/1.24 inference(cnf_transformation,[status(thm)],[f4508])).
% 5.64/1.24 fof(f4510,plain,(
% 5.64/1.24 ![X0,X1]: (~r2_hidden(sK0_skl(X0,X1),X1)|~r2_hidden(sK0_skl(X0,X1),X0)|X1=X0)),
% 5.64/1.24 inference(cnf_transformation,[status(thm)],[f4508])).
% 5.64/1.24 fof(f4511,plain,(
% 5.64/1.24 ![A,B]: ((~B=k1_tarski(A)|(![C]: ((~r2_hidden(C,B)|C=A)&(r2_hidden(C,B)|~C=A))))&(B=k1_tarski(A)|(?[C]: ((~r2_hidden(C,B)|~C=A)&(r2_hidden(C,B)|C=A)))))),
% 5.64/1.24 inference(NNF_transformation,[status(thm)],[f4])).
% 5.64/1.24 fof(f4512,plain,(
% 5.64/1.24 (![A,B]: (~B=k1_tarski(A)|((![C]: (~r2_hidden(C,B)|C=A))&(![C]: (r2_hidden(C,B)|~C=A)))))&(![A,B]: (B=k1_tarski(A)|(?[C]: ((~r2_hidden(C,B)|~C=A)&(r2_hidden(C,B)|C=A)))))),
% 5.64/1.24 inference(miniscoping,[status(thm)],[f4511])).
% 5.64/1.24 fof(f4513,plain,(
% 5.64/1.24 (![A,B]: (~B=k1_tarski(A)|((![C]: (~r2_hidden(C,B)|C=A))&(![C]: (r2_hidden(C,B)|~C=A)))))&(![A,B]: (B=k1_tarski(A)|((~r2_hidden(sK1_skl(B,A),B)|~sK1_skl(B,A)=A)&(r2_hidden(sK1_skl(B,A),B)|sK1_skl(B,A)=A))))),
% 5.64/1.24 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(C,sK1_skl(B,A))],[f4512])).
% 5.64/1.24 fof(f4516,plain,(
% 5.64/1.24 ![X0,X1]: (X0=k1_tarski(X1)|~r2_hidden(sK1_skl(X0,X1),X0)|~sK1_skl(X0,X1)=X1)),
% 5.64/1.24 inference(cnf_transformation,[status(thm)],[f4513])).
% 5.64/1.24 fof(f4517,plain,(
% 5.64/1.24 ![X0,X1]: (X0=k1_tarski(X1)|r2_hidden(sK1_skl(X0,X1),X0)|sK1_skl(X0,X1)=X1)),
% 5.64/1.24 inference(cnf_transformation,[status(thm)],[f4513])).
% 5.64/1.24 fof(f4534,plain,(
% 5.64/1.24 ![A,B]: ((~B=k3_tarski(A)|(![C]: ((~r2_hidden(C,B)|(?[D]: (r2_hidden(C,D)&r2_hidden(D,A))))&(r2_hidden(C,B)|(![D]: (~r2_hidden(C,D)|~r2_hidden(D,A)))))))&(B=k3_tarski(A)|(?[C]: ((~r2_hidden(C,B)|(![D]: (~r2_hidden(C,D)|~r2_hidden(D,A))))&(r2_hidden(C,B)|(?[D]: (r2_hidden(C,D)&r2_hidden(D,A))))))))),
% 5.64/1.24 inference(NNF_transformation,[status(thm)],[f9])).
% 5.64/1.24 fof(f4535,plain,(
% 5.64/1.24 (![A,B]: (~B=k3_tarski(A)|((![C]: (~r2_hidden(C,B)|(?[D]: (r2_hidden(C,D)&r2_hidden(D,A)))))&(![C]: (r2_hidden(C,B)|(![D]: (~r2_hidden(C,D)|~r2_hidden(D,A))))))))&(![A,B]: (B=k3_tarski(A)|(?[C]: ((~r2_hidden(C,B)|(![D]: (~r2_hidden(C,D)|~r2_hidden(D,A))))&(r2_hidden(C,B)|(?[D]: (r2_hidden(C,D)&r2_hidden(D,A))))))))),
% 5.64/1.24 inference(miniscoping,[status(thm)],[f4534])).
% 5.64/1.24 fof(f4536,plain,(
% 5.64/1.24 (![A,B]: (~B=k3_tarski(A)|((![C]: (~r2_hidden(C,B)|(r2_hidden(C,sK4_skl(C,B,A))&r2_hidden(sK4_skl(C,B,A),A))))&(![C]: (r2_hidden(C,B)|(![D]: (~r2_hidden(C,D)|~r2_hidden(D,A))))))))&(![A,B]: (B=k3_tarski(A)|((~r2_hidden(sK5_skl(B,A),B)|(![D]: (~r2_hidden(sK5_skl(B,A),D)|~r2_hidden(D,A))))&(r2_hidden(sK5_skl(B,A),B)|(r2_hidden(sK5_skl(B,A),sK6_skl(B,A))&r2_hidden(sK6_skl(B,A),A))))))),
% 5.64/1.24 inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl,sK5_skl,sK6_skl]),skolemize(D,sK4_skl(C,B,A)),skolemize(C,sK5_skl(B,A)),skolemize(D,sK6_skl(B,A))],[f4535])).
% 5.64/1.24 fof(f4539,plain,(
% 5.64/1.24 ![X0,X1,X2,X3]: (~X0=k3_tarski(X1)|r2_hidden(X2,X0)|~r2_hidden(X2,X3)|~r2_hidden(X3,X1))),
% 5.64/1.24 inference(cnf_transformation,[status(thm)],[f4536])).
% 5.64/1.24 fof(f4541,plain,(
% 5.64/1.24 ![X0,X1]: (X0=k3_tarski(X1)|r2_hidden(sK5_skl(X0,X1),X0)|r2_hidden(sK5_skl(X0,X1),sK6_skl(X0,X1)))),
% 5.64/1.24 inference(cnf_transformation,[status(thm)],[f4536])).
% 5.64/1.24 fof(f4542,plain,(
% 5.64/1.24 ![X0,X1]: (X0=k3_tarski(X1)|r2_hidden(sK5_skl(X0,X1),X0)|r2_hidden(sK6_skl(X0,X1),X1))),
% 5.64/1.24 inference(cnf_transformation,[status(thm)],[f4536])).
% 5.64/1.24 fof(f4543,plain,(
% 5.64/1.24 ![A,B]: (~r2_hidden(A,B)|(?[C]: (r2_hidden(C,B)&(![D]: (~r2_hidden(D,B)|~r2_hidden(D,C))))))),
% 5.64/1.24 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 5.64/1.24 fof(f4544,plain,(
% 5.64/1.24 ![B]: ((![A]: ~r2_hidden(A,B))|(?[C]: (r2_hidden(C,B)&(![D]: (~r2_hidden(D,B)|~r2_hidden(D,C))))))),
% 5.64/1.24 inference(miniscoping,[status(thm)],[f4543])).
% 5.64/1.24 fof(f4545,plain,(
% 5.64/1.24 ![B]: ((![A]: ~r2_hidden(A,B))|(r2_hidden(sK7_skl(B),B)&(![D]: (~r2_hidden(D,B)|~r2_hidden(D,sK7_skl(B))))))),
% 5.64/1.24 inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl]),skolemize(C,sK7_skl(B))],[f4544])).
% 5.64/1.24 fof(f4546,plain,(
% 5.64/1.24 ![X0,X1]: (~r2_hidden(X0,X1)|r2_hidden(sK7_skl(X1),X1))),
% 5.64/1.24 inference(cnf_transformation,[status(thm)],[f4545])).
% 5.64/1.24 fof(f4547,plain,(
% 5.64/1.24 ![X0,X1,X2]: (~r2_hidden(X0,X1)|~r2_hidden(X2,X1)|~r2_hidden(X2,sK7_skl(X1)))),
% 5.64/1.24 inference(cnf_transformation,[status(thm)],[f4545])).
% 5.64/1.24 fof(f4579,plain,(
% 5.64/1.24 ![A]: r1_tarski(A,A)),
% 5.64/1.24 inference(miniscoping,[status(thm)],[f18])).
% 5.64/1.24 fof(f4580,plain,(
% 5.64/1.24 ![X0]: (r1_tarski(X0,X0))),
% 5.64/1.24 inference(cnf_transformation,[status(thm)],[f4579])).
% 5.64/1.24 fof(f4582,plain,(
% 5.64/1.24 v1_xboole_0(k1_xboole_0)),
% 5.64/1.24 inference(cnf_transformation,[status(thm)],[f24])).
% 5.64/1.24 fof(f4583,plain,(
% 5.64/1.24 v1_xboole_0(sK20_skl)),
% 5.64/1.24 inference(skolemize,[status(esa),new_symbols(skolem,[sK20_skl]),skolemize(A,sK20_skl)],[f25])).
% 5.64/1.24 fof(f4584,plain,(
% 5.64/1.24 v1_xboole_0(sK20_skl)),
% 5.64/1.24 inference(cnf_transformation,[status(thm)],[f4583])).
% 5.64/1.24 fof(f4593,plain,(
% 5.64/1.24 ![A]: ((~A=k1_xboole_0|(![B]: ~r2_hidden(B,A)))&(A=k1_xboole_0|(?[B]: r2_hidden(B,A))))),
% 5.64/1.24 inference(NNF_transformation,[status(thm)],[f29])).
% 5.64/1.24 fof(f4594,plain,(
% 5.64/1.24 (![A]: (~A=k1_xboole_0|(![B]: ~r2_hidden(B,A))))&(![A]: (A=k1_xboole_0|(?[B]: r2_hidden(B,A))))),
% 5.64/1.24 inference(miniscoping,[status(thm)],[f4593])).
% 5.64/1.24 fof(f4595,plain,(
% 5.64/1.24 (![A]: (~A=k1_xboole_0|(![B]: ~r2_hidden(B,A))))&(![A]: (A=k1_xboole_0|r2_hidden(sK22_skl(A),A)))),
% 5.64/1.24 inference(skolemize,[status(esa),new_symbols(skolem,[sK22_skl]),skolemize(B,sK22_skl(A))],[f4594])).
% 5.64/1.24 fof(f4596,plain,(
% 5.64/1.24 ![X0,X1]: (~X0=k1_xboole_0|~r2_hidden(X1,X0))),
% 5.64/1.24 inference(cnf_transformation,[status(thm)],[f4595])).
% 5.64/1.24 fof(f4597,plain,(
% 5.64/1.24 ![X0]: (X0=k1_xboole_0|r2_hidden(sK22_skl(X0),X0))),
% 5.64/1.24 inference(cnf_transformation,[status(thm)],[f4595])).
% 5.64/1.24 fof(f4598,plain,(
% 5.64/1.24 ![A,B,C]: ((~C=k2_xboole_0(A,B)|(![D]: ((~r2_hidden(D,C)|(r2_hidden(D,A)|r2_hidden(D,B)))&(r2_hidden(D,C)|(~r2_hidden(D,A)&~r2_hidden(D,B))))))&(C=k2_xboole_0(A,B)|(?[D]: ((~r2_hidden(D,C)|(~r2_hidden(D,A)&~r2_hidden(D,B)))&(r2_hidden(D,C)|(r2_hidden(D,A)|r2_hidden(D,B)))))))),
% 5.64/1.24 inference(NNF_transformation,[status(thm)],[f30])).
% 5.64/1.24 fof(f4599,plain,(
% 5.64/1.24 (![A,B,C]: (~C=k2_xboole_0(A,B)|((![D]: (~r2_hidden(D,C)|(r2_hidden(D,A)|r2_hidden(D,B))))&(![D]: (r2_hidden(D,C)|(~r2_hidden(D,A)&~r2_hidden(D,B)))))))&(![A,B,C]: (C=k2_xboole_0(A,B)|(?[D]: ((~r2_hidden(D,C)|(~r2_hidden(D,A)&~r2_hidden(D,B)))&(r2_hidden(D,C)|(r2_hidden(D,A)|r2_hidden(D,B)))))))),
% 5.64/1.24 inference(miniscoping,[status(thm)],[f4598])).
% 5.64/1.24 fof(f4600,plain,(
% 5.64/1.24 (![A,B,C]: (~C=k2_xboole_0(A,B)|((![D]: (~r2_hidden(D,C)|(r2_hidden(D,A)|r2_hidden(D,B))))&(![D]: (r2_hidden(D,C)|(~r2_hidden(D,A)&~r2_hidden(D,B)))))))&(![A,B,C]: (C=k2_xboole_0(A,B)|((~r2_hidden(sK23_skl(C,B,A),C)|(~r2_hidden(sK23_skl(C,B,A),A)&~r2_hidden(sK23_skl(C,B,A),B)))&(r2_hidden(sK23_skl(C,B,A),C)|(r2_hidden(sK23_skl(C,B,A),A)|r2_hidden(sK23_skl(C,B,A),B))))))),
% 5.64/1.24 inference(skolemize,[status(esa),new_symbols(skolem,[sK23_skl]),skolemize(D,sK23_skl(C,B,A))],[f4599])).
% 5.64/1.24 fof(f4601,plain,(
% 5.64/1.24 ![X0,X1,X2,X3]: (~X0=k2_xboole_0(X1,X2)|~r2_hidden(X3,X0)|r2_hidden(X3,X1)|r2_hidden(X3,X2))),
% 5.64/1.24 inference(cnf_transformation,[status(thm)],[f4600])).
% 5.64/1.24 fof(f4602,plain,(
% 5.64/1.24 ![X0,X1,X2,X3]: (~X0=k2_xboole_0(X1,X2)|r2_hidden(X3,X0)|~r2_hidden(X3,X1))),
% 5.64/1.24 inference(cnf_transformation,[status(thm)],[f4600])).
% 5.64/1.24 fof(f4962,plain,(
% 5.64/1.24 ![A,B]: ((~B=k1_zfmisc_1(A)|(![C]: ((~r2_hidden(C,B)|r1_tarski(C,A))&(r2_hidden(C,B)|~r1_tarski(C,A)))))&(B=k1_zfmisc_1(A)|(?[C]: ((~r2_hidden(C,B)|~r1_tarski(C,A))&(r2_hidden(C,B)|r1_tarski(C,A))))))),
% 5.64/1.24 inference(NNF_transformation,[status(thm)],[f185])).
% 5.64/1.24 fof(f4963,plain,(
% 5.64/1.24 (![A,B]: (~B=k1_zfmisc_1(A)|((![C]: (~r2_hidden(C,B)|r1_tarski(C,A)))&(![C]: (r2_hidden(C,B)|~r1_tarski(C,A))))))&(![A,B]: (B=k1_zfmisc_1(A)|(?[C]: ((~r2_hidden(C,B)|~r1_tarski(C,A))&(r2_hidden(C,B)|r1_tarski(C,A))))))),
% 5.64/1.24 inference(miniscoping,[status(thm)],[f4962])).
% 5.64/1.24 fof(f4964,plain,(
% 5.64/1.24 (![A,B]: (~B=k1_zfmisc_1(A)|((![C]: (~r2_hidden(C,B)|r1_tarski(C,A)))&(![C]: (r2_hidden(C,B)|~r1_tarski(C,A))))))&(![A,B]: (B=k1_zfmisc_1(A)|((~r2_hidden(sK36_skl(B,A),B)|~r1_tarski(sK36_skl(B,A),A))&(r2_hidden(sK36_skl(B,A),B)|r1_tarski(sK36_skl(B,A),A)))))),
% 5.64/1.24 inference(skolemize,[status(esa),new_symbols(skolem,[sK36_skl]),skolemize(C,sK36_skl(B,A))],[f4963])).
% 5.64/1.24 fof(f4966,plain,(
% 5.64/1.24 ![X0,X1,X2]: (~X0=k1_zfmisc_1(X1)|r2_hidden(X2,X0)|~r1_tarski(X2,X1))),
% 5.64/1.24 inference(cnf_transformation,[status(thm)],[f4964])).
% 5.64/1.24 fof(f5335,plain,(
% 5.64/1.24 ![X0]: (~v1_xboole_0(k1_zfmisc_1(X0)))),
% 5.64/1.24 inference(cnf_transformation,[status(thm)],[f334])).
% 5.64/1.24 fof(f5360,plain,(
% 5.64/1.24 ![X0]: (m1_subset_1(k1_xboole_0,k1_zfmisc_1(X0)))),
% 5.64/1.24 inference(cnf_transformation,[status(thm)],[f349])).
% 5.64/1.24 fof(f5555,plain,(
% 5.64/1.24 ![A,B]: ((v1_xboole_0(A)|v1_xboole_0(B))|~r1_subset_1(A,A))),
% 5.64/1.24 inference(pre_NNF_transformation,[status(thm)],[f421])).
% 5.64/1.24 fof(f5556,plain,(
% 5.64/1.24 ![A]: ((v1_xboole_0(A)|(![B]: v1_xboole_0(B)))|~r1_subset_1(A,A))),
% 5.64/1.24 inference(miniscoping,[status(thm)],[f5555])).
% 5.64/1.24 fof(f5557,plain,(
% 5.64/1.24 ![X0,X1]: (v1_xboole_0(X0)|v1_xboole_0(X1)|~r1_subset_1(X0,X0))),
% 5.64/1.24 inference(cnf_transformation,[status(thm)],[f5556])).
% 5.64/1.24 fof(f5564,plain,(
% 5.64/1.24 ![A,B]: ((v1_xboole_0(A)|v1_xboole_0(B))|~r2_subset_1(A,A))),
% 5.64/1.24 inference(pre_NNF_transformation,[status(thm)],[f424])).
% 5.64/1.24 fof(f5565,plain,(
% 5.64/1.24 ![A]: ((v1_xboole_0(A)|(![B]: v1_xboole_0(B)))|~r2_subset_1(A,A))),
% 5.64/1.24 inference(miniscoping,[status(thm)],[f5564])).
% 5.64/1.24 fof(f5566,plain,(
% 5.64/1.24 ![X0,X1]: (v1_xboole_0(X0)|v1_xboole_0(X1)|~r2_subset_1(X0,X0))),
% 5.64/1.24 inference(cnf_transformation,[status(thm)],[f5565])).
% 5.64/1.24 fof(f5816,plain,(
% 5.64/1.24 ![A,B]: (~m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A)))|m1_subset_1(k5_setfam_1(A,B),k1_zfmisc_1(A)))),
% 5.64/1.24 inference(pre_NNF_transformation,[status(thm)],[f531])).
% 5.64/1.24 fof(f5817,plain,(
% 5.64/1.24 ![X0,X1]: (~m1_subset_1(X0,k1_zfmisc_1(k1_zfmisc_1(X1)))|m1_subset_1(k5_setfam_1(X1,X0),k1_zfmisc_1(X1)))),
% 5.64/1.24 inference(cnf_transformation,[status(thm)],[f5816])).
% 5.64/1.24 fof(f5818,plain,(
% 5.64/1.24 ![A,B]: (~m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A)))|k5_setfam_1(A,B)=k3_tarski(B))),
% 5.64/1.24 inference(pre_NNF_transformation,[status(thm)],[f532])).
% 5.64/1.24 fof(f5819,plain,(
% 5.64/1.24 ![X0,X1]: (~m1_subset_1(X0,k1_zfmisc_1(k1_zfmisc_1(X1)))|k5_setfam_1(X1,X0)=k3_tarski(X0))),
% 5.64/1.24 inference(cnf_transformation,[status(thm)],[f5818])).
% 5.64/1.24 fof(f5830,plain,(
% 5.64/1.24 ![A,B]: (~r2_hidden(A,B)|m1_subset_1(A,B))),
% 5.64/1.24 inference(pre_NNF_transformation,[status(thm)],[f538])).
% 5.64/1.24 fof(f5831,plain,(
% 5.64/1.24 ![X0,X1]: (~r2_hidden(X0,X1)|m1_subset_1(X0,X1))),
% 5.64/1.24 inference(cnf_transformation,[status(thm)],[f5830])).
% 5.64/1.24 fof(f5834,plain,(
% 5.64/1.24 ![A,B]: ((~m1_subset_1(A,k1_zfmisc_1(B))|r1_tarski(A,B))&(m1_subset_1(A,k1_zfmisc_1(B))|~r1_tarski(A,B)))),
% 5.64/1.24 inference(NNF_transformation,[status(thm)],[f540])).
% 5.64/1.24 fof(f5835,plain,(
% 5.64/1.24 (![A,B]: (~m1_subset_1(A,k1_zfmisc_1(B))|r1_tarski(A,B)))&(![A,B]: (m1_subset_1(A,k1_zfmisc_1(B))|~r1_tarski(A,B)))),
% 5.64/1.24 inference(miniscoping,[status(thm)],[f5834])).
% 5.64/1.24 fof(f5836,plain,(
% 5.64/1.24 ![X0,X1]: (~m1_subset_1(X0,k1_zfmisc_1(X1))|r1_tarski(X0,X1))),
% 5.64/1.24 inference(cnf_transformation,[status(thm)],[f5835])).
% 5.64/1.24 fof(f5837,plain,(
% 5.64/1.24 ![X0,X1]: (m1_subset_1(X0,k1_zfmisc_1(X1))|~r1_tarski(X0,X1))),
% 5.64/1.24 inference(cnf_transformation,[status(thm)],[f5835])).
% 5.64/1.24 fof(f5841,plain,(
% 5.64/1.24 ![A,B,C]: ((~r2_hidden(A,B)|~m1_subset_1(B,k1_zfmisc_1(C)))|~v1_xboole_0(C))),
% 5.64/1.24 inference(pre_NNF_transformation,[status(thm)],[f542])).
% 5.64/1.24 fof(f5842,plain,(
% 5.64/1.24 ![C]: ((![B]: ((![A]: ~r2_hidden(A,B))|~m1_subset_1(B,k1_zfmisc_1(C))))|~v1_xboole_0(C))),
% 5.64/1.24 inference(miniscoping,[status(thm)],[f5841])).
% 5.64/1.24 fof(f5843,plain,(
% 5.64/1.24 ![X0,X1,X2]: (~r2_hidden(X0,X1)|~m1_subset_1(X1,k1_zfmisc_1(X2))|~v1_xboole_0(X2))),
% 5.64/1.24 inference(cnf_transformation,[status(thm)],[f5842])).
% 5.64/1.24 fof(f7238,plain,(
% 5.64/1.24 ![A,B,C,D]: (((~r2_hidden(A,B)|~r2_hidden(B,C))|~r2_hidden(C,D))|~r2_hidden(D,A))),
% 5.64/1.24 inference(pre_NNF_transformation,[status(thm)],[f1051])).
% 5.64/1.24 fof(f7239,plain,(
% 5.64/1.24 ![A,D]: ((![C]: ((![B]: (~r2_hidden(A,B)|~r2_hidden(B,C)))|~r2_hidden(C,D)))|~r2_hidden(D,A))),
% 5.64/1.24 inference(miniscoping,[status(thm)],[f7238])).
% 5.64/1.24 fof(f7240,plain,(
% 5.64/1.24 ![X0,X1,X2,X3]: (~r2_hidden(X0,X1)|~r2_hidden(X1,X2)|~r2_hidden(X2,X3)|~r2_hidden(X3,X0))),
% 5.64/1.24 inference(cnf_transformation,[status(thm)],[f7239])).
% 5.64/1.24 fof(f7244,plain,(
% 5.64/1.24 ![A,B,C,D,E,F]: (((((~r2_hidden(A,B)|~r2_hidden(B,C))|~r2_hidden(C,D))|~r2_hidden(D,E))|~r2_hidden(E,F))|~r2_hidden(F,A))),
% 5.64/1.24 inference(pre_NNF_transformation,[status(thm)],[f1053])).
% 5.64/1.24 fof(f7245,plain,(
% 5.64/1.24 ![A,F]: ((![E]: ((![D]: ((![C]: ((![B]: (~r2_hidden(A,B)|~r2_hidden(B,C)))|~r2_hidden(C,D)))|~r2_hidden(D,E)))|~r2_hidden(E,F)))|~r2_hidden(F,A))),
% 5.64/1.24 inference(miniscoping,[status(thm)],[f7244])).
% 5.64/1.24 fof(f7246,plain,(
% 5.64/1.24 ![X0,X1,X2,X3,X4,X5]: (~r2_hidden(X0,X1)|~r2_hidden(X1,X2)|~r2_hidden(X2,X3)|~r2_hidden(X3,X4)|~r2_hidden(X4,X5)|~r2_hidden(X5,X0))),
% 5.64/1.24 inference(cnf_transformation,[status(thm)],[f7245])).
% 5.64/1.24 fof(f14893,plain,(
% 5.64/1.24 ![A,B]: (~m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A)))|(B=k1_xboole_0|r1_tarski(k8_setfam_1(A,B),k5_setfam_1(A,B))))),
% 5.64/1.24 inference(pre_NNF_transformation,[status(thm)],[f3616])).
% 5.64/1.24 fof(f14894,plain,(
% 5.64/1.24 ![X0,X1]: (~m1_subset_1(X0,k1_zfmisc_1(k1_zfmisc_1(X1)))|X0=k1_xboole_0|r1_tarski(k8_setfam_1(X1,X0),k5_setfam_1(X1,X0)))),
% 5.64/1.24 inference(cnf_transformation,[status(thm)],[f14893])).
% 5.64/1.24 fof(f17605,plain,(
% 5.64/1.24 (?[A,B]: (m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A)))&(k5_setfam_1(A,B)=k1_xboole_0<~>(![C]: (~r2_hidden(C,B)|C=k1_xboole_0)))))),
% 5.64/1.24 inference(pre_NNF_transformation,[status(thm)],[f4503])).
% 5.64/1.24 fof(f17606,plain,(
% 5.64/1.24 ?[A,B]: (m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A)))&((k5_setfam_1(A,B)=k1_xboole_0|(![C]: (~r2_hidden(C,B)|C=k1_xboole_0)))&(~k5_setfam_1(A,B)=k1_xboole_0|(?[C]: (r2_hidden(C,B)&~C=k1_xboole_0)))))),
% 5.64/1.24 inference(NNF_transformation,[status(thm)],[f17605])).
% 5.64/1.24 fof(f17607,plain,(
% 5.64/1.24 (m1_subset_1(sK1207_skl,k1_zfmisc_1(k1_zfmisc_1(sK1206_skl)))&((k5_setfam_1(sK1206_skl,sK1207_skl)=k1_xboole_0|(![C]: (~r2_hidden(C,sK1207_skl)|C=k1_xboole_0)))&(~k5_setfam_1(sK1206_skl,sK1207_skl)=k1_xboole_0|(r2_hidden(sK1208_skl,sK1207_skl)&~sK1208_skl=k1_xboole_0))))),
% 5.64/1.24 inference(skolemize,[status(esa),new_symbols(skolem,[sK1206_skl,sK1207_skl,sK1208_skl]),skolemize(A,sK1206_skl),skolemize(B,sK1207_skl),skolemize(C,sK1208_skl)],[f17606])).
% 5.64/1.24 fof(f17608,plain,(
% 5.64/1.24 m1_subset_1(sK1207_skl,k1_zfmisc_1(k1_zfmisc_1(sK1206_skl)))),
% 5.64/1.24 inference(cnf_transformation,[status(thm)],[f17607])).
% 5.64/1.24 fof(f17609,plain,(
% 5.64/1.24 ![X0]: (k5_setfam_1(sK1206_skl,sK1207_skl)=k1_xboole_0|~r2_hidden(X0,sK1207_skl)|X0=k1_xboole_0)),
% 5.64/1.24 inference(cnf_transformation,[status(thm)],[f17607])).
% 5.64/1.24 fof(f17610,plain,(
% 5.64/1.24 ~k5_setfam_1(sK1206_skl,sK1207_skl)=k1_xboole_0|r2_hidden(sK1208_skl,sK1207_skl)),
% 5.64/1.24 inference(cnf_transformation,[status(thm)],[f17607])).
% 5.64/1.24 fof(f17611,plain,(
% 5.64/1.24 ~k5_setfam_1(sK1206_skl,sK1207_skl)=k1_xboole_0|~sK1208_skl=k1_xboole_0),
% 5.64/1.24 inference(cnf_transformation,[status(thm)],[f17607])).
% 5.64/1.24 fof(f18910,definition,(
% 5.64/1.24 ![X0]: (sQ13_spl <=> (v1_xboole_0(X0)|~r1_subset_1(X0,X0)))),
% 5.64/1.24 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 5.64/1.24 fof(f18913,definition,(
% 5.64/1.24 ![X1]: (sQ14_spl <=> (v1_xboole_0(X1)))),
% 5.64/1.24 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 5.64/1.24 fof(f18914,plain,(
% 5.64/1.24 ![X0]: (v1_xboole_0(X0)|~sQ14_spl)),
% 5.64/1.24 inference(component_clause,[status(thm)],[f18913])).
% 5.64/1.24 fof(f18916,plain,(
% 5.64/1.24 sQ13_spl|sQ14_spl),
% 5.64/1.24 inference(split_clause,[status(thm)],[f5557,f18910,f18913])).
% 5.64/1.24 fof(f18917,definition,(
% 5.64/1.24 ![X0]: (sQ15_spl <=> (v1_xboole_0(X0)|~r2_subset_1(X0,X0)))),
% 5.64/1.24 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 5.64/1.24 fof(f18920,plain,(
% 5.64/1.24 sQ15_spl|sQ14_spl),
% 5.64/1.24 inference(split_clause,[status(thm)],[f5566,f18917,f18913])).
% 5.64/1.24 fof(f20440,definition,(
% 5.64/1.24 sQ419_spl <=> (k5_setfam_1(sK1206_skl,sK1207_skl)=k1_xboole_0)),
% 5.64/1.24 introduced(definition,[new_symbols(definition,[sQ419_spl])],[split_symbol_definition])).
% 5.64/1.24 fof(f20441,plain,(
% 5.64/1.24 k5_setfam_1(sK1206_skl,sK1207_skl)=k1_xboole_0|~sQ419_spl),
% 5.64/1.24 inference(component_clause,[status(thm)],[f20440])).
% 5.64/1.24 fof(f20442,plain,(
% 5.64/1.24 ~k5_setfam_1(sK1206_skl,sK1207_skl)=k1_xboole_0|sQ419_spl),
% 5.64/1.24 inference(component_clause,[status(thm)],[f20440])).
% 5.64/1.24 fof(f20443,definition,(
% 5.64/1.24 ![X0]: (sQ420_spl <=> (~r2_hidden(X0,sK1207_skl)|X0=k1_xboole_0))),
% 5.64/1.24 introduced(definition,[new_symbols(definition,[sQ420_spl])],[split_symbol_definition])).
% 5.64/1.24 fof(f20444,plain,(
% 5.64/1.24 ![X0]: (~r2_hidden(X0,sK1207_skl)|X0=k1_xboole_0|~sQ420_spl)),
% 5.64/1.24 inference(component_clause,[status(thm)],[f20443])).
% 5.64/1.24 fof(f20446,plain,(
% 5.64/1.24 sQ419_spl|sQ420_spl),
% 5.64/1.24 inference(split_clause,[status(thm)],[f17609,f20440,f20443])).
% 5.64/1.24 fof(f20447,definition,(
% 5.64/1.24 sQ421_spl <=> (r2_hidden(sK1208_skl,sK1207_skl))),
% 5.64/1.24 introduced(definition,[new_symbols(definition,[sQ421_spl])],[split_symbol_definition])).
% 5.64/1.24 fof(f20448,plain,(
% 5.64/1.24 r2_hidden(sK1208_skl,sK1207_skl)|~sQ421_spl),
% 5.64/1.24 inference(component_clause,[status(thm)],[f20447])).
% 5.64/1.24 fof(f20450,plain,(
% 5.64/1.24 ~sQ419_spl|sQ421_spl),
% 5.64/1.24 inference(split_clause,[status(thm)],[f17610,f20440,f20447])).
% 5.64/1.24 fof(f20451,definition,(
% 5.64/1.24 sQ422_spl <=> (sK1208_skl=k1_xboole_0)),
% 5.64/1.24 introduced(definition,[new_symbols(definition,[sQ422_spl])],[split_symbol_definition])).
% 5.64/1.24 fof(f20453,plain,(
% 5.64/1.24 ~sK1208_skl=k1_xboole_0|sQ422_spl),
% 5.64/1.24 inference(component_clause,[status(thm)],[f20451])).
% 5.64/1.24 fof(f20454,plain,(
% 5.64/1.24 ~sQ419_spl|~sQ422_spl),
% 5.64/1.24 inference(split_clause,[status(thm)],[f17611,f20440,f20451])).
% 5.64/1.24 fof(f21097,plain,(
% 5.64/1.24 ![X0,X1,X2]: (r2_hidden(X0,k3_tarski(X1))|~r2_hidden(X0,X2)|~r2_hidden(X2,X1))),
% 5.64/1.24 inference(destructive_equality_resolution,[status(thm)],[f4539])).
% 5.64/1.24 fof(f21100,plain,(
% 5.64/1.24 ![X0]: (~r2_hidden(X0,k1_xboole_0))),
% 5.64/1.24 inference(destructive_equality_resolution,[status(thm)],[f4596])).
% 5.64/1.24 fof(f21101,plain,(
% 5.64/1.24 ![X0,X1,X2]: (~r2_hidden(X0,k2_xboole_0(X1,X2))|r2_hidden(X0,X1)|r2_hidden(X0,X2))),
% 5.64/1.24 inference(destructive_equality_resolution,[status(thm)],[f4601])).
% 5.64/1.24 fof(f21102,plain,(
% 5.64/1.24 ![X0,X1,X2]: (r2_hidden(X0,k2_xboole_0(X1,X2))|~r2_hidden(X0,X1))),
% 5.64/1.24 inference(destructive_equality_resolution,[status(thm)],[f4602])).
% 5.64/1.24 fof(f21117,plain,(
% 5.64/1.24 ![X0,X1]: (r2_hidden(X0,k1_zfmisc_1(X1))|~r1_tarski(X0,X1))),
% 5.64/1.24 inference(destructive_equality_resolution,[status(thm)],[f4966])).
% 5.64/1.24 fof(f22117,plain,(
% 5.64/1.24 ![X0]: (r2_hidden(sK0_skl(X0,k1_xboole_0),X0)|k1_xboole_0=X0)),
% 5.64/1.24 inference(resolution,[status(thm)],[f4509,f21100])).
% 5.64/1.24 fof(f22118,plain,(
% 5.64/1.24 sK1207_skl=sK1207_skl|sK0_skl(sK1207_skl,sK1207_skl)=k1_xboole_0|~sQ420_spl),
% 5.64/1.24 inference(resolution,[status(thm)],[f4509,f20444])).
% 5.64/1.24 fof(f22119,plain,(
% 5.64/1.24 ![X0]: (r2_hidden(sK0_skl(X0,sK1207_skl),X0)|sK1207_skl=X0|sK0_skl(X0,sK1207_skl)=k1_xboole_0|~sQ420_spl)),
% 5.64/1.24 inference(resolution,[status(thm)],[f4509,f20444])).
% 5.64/1.24 fof(f22121,plain,(
% 5.64/1.24 ![X0,X1]: (r2_hidden(sK0_skl(X0,X1),X0)|X1=X0|~r2_hidden(X1,sK0_skl(X0,X1)))),
% 5.64/1.24 inference(resolution,[status(thm)],[f4509,f4505])).
% 5.64/1.24 fof(f22123,plain,(
% 5.64/1.24 ![X0]: (r2_hidden(sK0_skl(k1_xboole_0,X0),X0)|X0=k1_xboole_0)),
% 5.64/1.24 inference(resolution,[status(thm)],[f4509,f21100])).
% 5.64/1.24 fof(f22126,definition,(
% 5.64/1.24 sQ582_spl <=> (sK1207_skl=sK1207_skl)),
% 5.64/1.24 introduced(definition,[new_symbols(definition,[sQ582_spl])],[split_symbol_definition])).
% 5.64/1.24 fof(f22129,definition,(
% 5.64/1.24 sQ583_spl <=> (sK0_skl(sK1207_skl,sK1207_skl)=k1_xboole_0)),
% 5.64/1.24 introduced(definition,[new_symbols(definition,[sQ583_spl])],[split_symbol_definition])).
% 5.64/1.24 fof(f22130,plain,(
% 5.64/1.24 sK0_skl(sK1207_skl,sK1207_skl)=k1_xboole_0|~sQ583_spl),
% 5.64/1.24 inference(component_clause,[status(thm)],[f22129])).
% 5.64/1.24 fof(f22132,plain,(
% 5.64/1.24 sQ582_spl|sQ583_spl|~sQ420_spl),
% 5.64/1.24 inference(split_clause,[status(thm)],[f22118,f22126,f22129,f20443])).
% 5.64/1.24 fof(f22144,plain,(
% 5.64/1.24 ![X0,X1]: (m1_subset_1(sK0_skl(X0,X1),X0)|r2_hidden(sK0_skl(X0,X1),X1)|X1=X0)),
% 5.64/1.24 inference(resolution,[status(thm)],[f5831,f4509])).
% 5.64/1.24 fof(f22146,plain,(
% 5.64/1.24 ![X0,X1]: (m1_subset_1(sK0_skl(X0,X1),X1)|r2_hidden(sK0_skl(X0,X1),X0)|X1=X0)),
% 5.64/1.24 inference(resolution,[status(thm)],[f5831,f4509])).
% 5.64/1.24 fof(f22154,plain,(
% 5.64/1.24 ![X0,X1]: (X0=k1_tarski(X1)|sK1_skl(X0,X1)=X1|m1_subset_1(sK1_skl(X0,X1),X0))),
% 5.64/1.24 inference(resolution,[status(thm)],[f4517,f5831])).
% 5.64/1.24 fof(f22155,plain,(
% 5.64/1.24 ![X0,X1]: (X0=k1_tarski(X1)|sK1_skl(X0,X1)=X1|~r2_hidden(X0,sK1_skl(X0,X1)))),
% 5.64/1.24 inference(resolution,[status(thm)],[f4517,f4505])).
% 5.64/1.24 fof(f22156,plain,(
% 5.64/1.24 ~r2_hidden(k1_xboole_0,sK1207_skl)|~r2_hidden(sK0_skl(sK1207_skl,sK1207_skl),sK1207_skl)|sK1207_skl=sK1207_skl|~sQ583_spl),
% 5.64/1.24 inference(paramodulation,[status(thm)],[f22130,f4510])).
% 5.64/1.24 fof(f22157,plain,(
% 5.64/1.24 r2_hidden(sK0_skl(sK1207_skl,sK1207_skl),sK1207_skl)|r2_hidden(k1_xboole_0,sK1207_skl)|sK1207_skl=sK1207_skl|~sQ583_spl),
% 5.64/1.24 inference(paramodulation,[status(thm)],[f22130,f4509])).
% 5.64/1.24 fof(f22159,definition,(
% 5.64/1.24 sQ584_spl <=> (r2_hidden(k1_xboole_0,sK1207_skl))),
% 5.64/1.24 introduced(definition,[new_symbols(definition,[sQ584_spl])],[split_symbol_definition])).
% 5.64/1.24 fof(f22162,definition,(
% 5.64/1.24 sQ585_spl <=> (r2_hidden(sK0_skl(sK1207_skl,sK1207_skl),sK1207_skl))),
% 5.64/1.24 introduced(definition,[new_symbols(definition,[sQ585_spl])],[split_symbol_definition])).
% 5.64/1.24 fof(f22165,plain,(
% 5.64/1.24 ~sQ584_spl|~sQ585_spl|sQ582_spl|~sQ583_spl),
% 5.64/1.24 inference(split_clause,[status(thm)],[f22156,f22159,f22162,f22126,f22129])).
% 5.64/1.24 fof(f22166,plain,(
% 5.64/1.24 sQ585_spl|sQ584_spl|sQ582_spl|~sQ583_spl),
% 5.64/1.24 inference(split_clause,[status(thm)],[f22157,f22162,f22159,f22126,f22129])).
% 5.64/1.24 fof(f22169,definition,(
% 5.64/1.24 sQ586_spl <=> (m1_subset_1(sK1207_skl,k1_zfmisc_1(k1_zfmisc_1(sK1206_skl))))),
% 5.64/1.24 introduced(definition,[new_symbols(definition,[sQ586_spl])],[split_symbol_definition])).
% 5.64/1.24 fof(f22171,plain,(
% 5.64/1.24 ~m1_subset_1(sK1207_skl,k1_zfmisc_1(k1_zfmisc_1(sK1206_skl)))|sQ586_spl),
% 5.64/1.24 inference(component_clause,[status(thm)],[f22169])).
% 5.64/1.24 fof(f22176,plain,(
% 5.64/1.24 $false|sQ586_spl),
% 5.64/1.24 inference(forward_subsumption_resolution,[status(thm)],[f22171,f17608])).
% 5.64/1.24 fof(f22177,plain,(
% 5.64/1.24 sQ586_spl),
% 5.64/1.24 inference(contradiction_clause,[status(thm)],[f22176])).
% 5.64/1.24 fof(f22178,plain,(
% 5.64/1.24 ![X0]: (sK1_skl(sK1207_skl,X0)=k1_xboole_0|sK1207_skl=k1_tarski(X0)|sK1_skl(sK1207_skl,X0)=X0|~sQ420_spl)),
% 5.64/1.24 inference(resolution,[status(thm)],[f20444,f4517])).
% 5.64/1.24 fof(f22179,plain,(
% 5.64/1.24 sK1208_skl=k1_xboole_0|~sQ420_spl|~sQ421_spl),
% 5.64/1.24 inference(resolution,[status(thm)],[f20444,f20448])).
% 5.64/1.24 fof(f22181,plain,(
% 5.64/1.24 ![X0]: (sK0_skl(sK1207_skl,X0)=k1_xboole_0|r2_hidden(sK0_skl(sK1207_skl,X0),X0)|X0=sK1207_skl|~sQ420_spl)),
% 5.64/1.24 inference(resolution,[status(thm)],[f20444,f4509])).
% 5.64/1.24 fof(f22183,plain,(
% 5.64/1.24 ![X0]: (sK0_skl(X0,sK1207_skl)=k1_xboole_0|r2_hidden(sK0_skl(X0,sK1207_skl),X0)|sK1207_skl=X0|~sQ420_spl)),
% 5.64/1.24 inference(resolution,[status(thm)],[f20444,f4509])).
% 5.64/1.24 fof(f22184,plain,(
% 5.64/1.24 $false|sQ422_spl|~sQ420_spl|~sQ421_spl),
% 5.64/1.24 inference(forward_subsumption_resolution,[status(thm)],[f22179,f20453])).
% 5.64/1.24 fof(f22185,plain,(
% 5.64/1.24 sQ422_spl|~sQ420_spl|~sQ421_spl),
% 5.64/1.24 inference(contradiction_clause,[status(thm)],[f22184])).
% 5.64/1.24 fof(f22188,plain,(
% 5.64/1.24 ![X0,X1]: (r1_tarski(k5_setfam_1(X0,X1),X0)|~m1_subset_1(X1,k1_zfmisc_1(k1_zfmisc_1(X0))))),
% 5.64/1.24 inference(resolution,[status(thm)],[f5836,f5817])).
% 5.64/1.24 fof(f22189,plain,(
% 5.64/1.24 ![X0]: (r1_tarski(k1_xboole_0,X0))),
% 5.64/1.24 inference(resolution,[status(thm)],[f5836,f5360])).
% 5.64/1.24 fof(f22190,plain,(
% 5.64/1.24 r1_tarski(sK1207_skl,k1_zfmisc_1(sK1206_skl))),
% 5.64/1.24 inference(resolution,[status(thm)],[f5836,f17608])).
% 5.64/1.24 fof(f22192,plain,(
% 5.64/1.24 ![X0]: (r2_hidden(k1_xboole_0,k1_zfmisc_1(X0)))),
% 5.64/1.24 inference(resolution,[status(thm)],[f22189,f21117])).
% 5.64/1.24 fof(f22194,plain,(
% 5.64/1.24 ![X0]: (k5_setfam_1(X0,k1_xboole_0)=k3_tarski(k1_xboole_0))),
% 5.64/1.24 inference(resolution,[status(thm)],[f5819,f5360])).
% 5.64/1.24 fof(f22195,plain,(
% 5.64/1.24 k5_setfam_1(sK1206_skl,sK1207_skl)=k3_tarski(sK1207_skl)),
% 5.64/1.24 inference(resolution,[status(thm)],[f5819,f17608])).
% 5.64/1.24 fof(f22197,plain,(
% 5.64/1.24 $false|~sQ14_spl),
% 5.64/1.24 inference(backward_subsumption_resolution,[status(thm)],[f5335,f18914])).
% 5.64/1.24 fof(f22198,plain,(
% 5.64/1.24 ~sQ14_spl),
% 5.64/1.24 inference(contradiction_clause,[status(thm)],[f22197])).
% 5.64/1.24 fof(f22199,plain,(
% 5.64/1.24 ![X0]: (m1_subset_1(X0,k1_zfmisc_1(X0)))),
% 5.64/1.24 inference(resolution,[status(thm)],[f4580,f5837])).
% 5.64/1.24 fof(f22215,plain,(
% 5.64/1.24 r2_hidden(sK1207_skl,k1_zfmisc_1(k1_zfmisc_1(sK1206_skl)))),
% 5.64/1.24 inference(resolution,[status(thm)],[f22190,f21117])).
% 5.64/1.24 fof(f22216,plain,(
% 5.64/1.24 ~k3_tarski(sK1207_skl)=k1_xboole_0|sQ419_spl),
% 5.64/1.24 inference(backward_demodulation,[status(thm)],[f22195,f20442])).
% 5.64/1.24 fof(f22217,plain,(
% 5.64/1.24 ~m1_subset_1(sK1207_skl,k1_zfmisc_1(k1_zfmisc_1(sK1206_skl)))|m1_subset_1(k3_tarski(sK1207_skl),k1_zfmisc_1(sK1206_skl))),
% 5.64/1.24 inference(paramodulation,[status(thm)],[f22195,f5817])).
% 5.64/1.24 fof(f22218,definition,(
% 5.64/1.24 sQ588_spl <=> (m1_subset_1(k3_tarski(sK1207_skl),k1_zfmisc_1(sK1206_skl)))),
% 5.64/1.24 introduced(definition,[new_symbols(definition,[sQ588_spl])],[split_symbol_definition])).
% 5.64/1.24 fof(f22219,plain,(
% 5.64/1.24 m1_subset_1(k3_tarski(sK1207_skl),k1_zfmisc_1(sK1206_skl))|~sQ588_spl),
% 5.64/1.24 inference(component_clause,[status(thm)],[f22218])).
% 5.64/1.24 fof(f22221,plain,(
% 5.64/1.24 ~sQ586_spl|sQ588_spl),
% 5.64/1.24 inference(split_clause,[status(thm)],[f22217,f22169,f22218])).
% 5.64/1.24 fof(f22227,plain,(
% 5.64/1.24 sK1207_skl=k1_xboole_0|sK0_skl(k1_xboole_0,sK1207_skl)=k1_xboole_0|~sQ420_spl),
% 5.64/1.24 inference(resolution,[status(thm)],[f22119,f21100])).
% 5.64/1.24 fof(f22232,definition,(
% 5.64/1.24 sQ589_spl <=> (sK1207_skl=k1_xboole_0)),
% 5.64/1.24 introduced(definition,[new_symbols(definition,[sQ589_spl])],[split_symbol_definition])).
% 5.64/1.24 fof(f22233,plain,(
% 5.64/1.24 sK1207_skl=k1_xboole_0|~sQ589_spl),
% 5.64/1.24 inference(component_clause,[status(thm)],[f22232])).
% 5.64/1.24 fof(f22234,plain,(
% 5.64/1.24 ~sK1207_skl=k1_xboole_0|sQ589_spl),
% 5.64/1.24 inference(component_clause,[status(thm)],[f22232])).
% 5.64/1.24 fof(f22235,definition,(
% 5.64/1.24 sQ590_spl <=> (sK0_skl(k1_xboole_0,sK1207_skl)=k1_xboole_0)),
% 5.64/1.24 introduced(definition,[new_symbols(definition,[sQ590_spl])],[split_symbol_definition])).
% 5.64/1.24 fof(f22236,plain,(
% 5.64/1.24 sK0_skl(k1_xboole_0,sK1207_skl)=k1_xboole_0|~sQ590_spl),
% 5.64/1.24 inference(component_clause,[status(thm)],[f22235])).
% 5.64/1.24 fof(f22238,plain,(
% 5.64/1.24 sQ589_spl|sQ590_spl|~sQ420_spl),
% 5.64/1.24 inference(split_clause,[status(thm)],[f22227,f22232,f22235,f20443])).
% 5.64/1.24 fof(f22241,plain,(
% 5.64/1.24 k5_setfam_1(sK1206_skl,sK1207_skl)=k3_tarski(k1_xboole_0)|~sQ589_spl),
% 5.64/1.24 inference(backward_demodulation,[status(thm)],[f22233,f22195])).
% 5.64/1.24 fof(f22247,plain,(
% 5.64/1.24 k5_setfam_1(sK1206_skl,k1_xboole_0)=k3_tarski(k1_xboole_0)|~sQ589_spl),
% 5.64/1.24 inference(forward_demodulation,[status(thm)],[f22233,f22241])).
% 5.64/1.24 fof(f22255,plain,(
% 5.64/1.24 ![X0,X1]: (~r2_hidden(X0,X1)|~m1_subset_1(X1,k1_zfmisc_1(sK20_skl)))),
% 5.64/1.24 inference(resolution,[status(thm)],[f5843,f4584])).
% 5.64/1.24 fof(f22256,plain,(
% 5.64/1.24 ![X0,X1]: (~r2_hidden(X0,X1)|~m1_subset_1(X1,k1_zfmisc_1(k1_xboole_0)))),
% 5.64/1.24 inference(resolution,[status(thm)],[f5843,f4582])).
% 5.64/1.24 fof(f22269,definition,(
% 5.64/1.24 sQ591_spl <=> (r2_hidden(k1_xboole_0,k1_xboole_0))),
% 5.64/1.24 introduced(definition,[new_symbols(definition,[sQ591_spl])],[split_symbol_definition])).
% 5.64/1.24 fof(f22285,plain,(
% 5.64/1.24 m1_subset_1(k3_tarski(k1_xboole_0),k1_zfmisc_1(sK1206_skl))|~sQ589_spl|~sQ588_spl),
% 5.64/1.24 inference(forward_demodulation,[status(thm)],[f22233,f22219])).
% 5.64/1.24 fof(f22286,plain,(
% 5.64/1.24 r1_tarski(k3_tarski(k1_xboole_0),sK1206_skl)|~sQ589_spl|~sQ588_spl),
% 5.64/1.24 inference(resolution,[status(thm)],[f22285,f5836])).
% 5.64/1.24 fof(f22307,plain,(
% 5.64/1.24 r2_hidden(k3_tarski(k1_xboole_0),k1_zfmisc_1(sK1206_skl))|~sQ589_spl|~sQ588_spl),
% 5.64/1.24 inference(resolution,[status(thm)],[f22286,f21117])).
% 5.64/1.24 fof(f22413,plain,(
% 5.64/1.24 ~m1_subset_1(k1_xboole_0,k1_zfmisc_1(k1_zfmisc_1(sK1206_skl)))|m1_subset_1(k3_tarski(k1_xboole_0),k1_zfmisc_1(sK1206_skl))|~sQ589_spl),
% 5.64/1.24 inference(paramodulation,[status(thm)],[f22247,f5817])).
% 5.64/1.24 fof(f22414,definition,(
% 5.64/1.24 sQ595_spl <=> (m1_subset_1(k1_xboole_0,k1_zfmisc_1(k1_zfmisc_1(sK1206_skl))))),
% 5.64/1.24 introduced(definition,[new_symbols(definition,[sQ595_spl])],[split_symbol_definition])).
% 5.64/1.24 fof(f22416,plain,(
% 5.64/1.24 ~m1_subset_1(k1_xboole_0,k1_zfmisc_1(k1_zfmisc_1(sK1206_skl)))|sQ595_spl),
% 5.64/1.24 inference(component_clause,[status(thm)],[f22414])).
% 5.64/1.24 fof(f22417,definition,(
% 5.64/1.24 sQ596_spl <=> (m1_subset_1(k3_tarski(k1_xboole_0),k1_zfmisc_1(sK1206_skl)))),
% 5.64/1.24 introduced(definition,[new_symbols(definition,[sQ596_spl])],[split_symbol_definition])).
% 5.64/1.24 fof(f22420,plain,(
% 5.64/1.24 ~sQ595_spl|sQ596_spl|~sQ589_spl),
% 5.64/1.24 inference(split_clause,[status(thm)],[f22413,f22414,f22417,f22232])).
% 5.64/1.24 fof(f22421,plain,(
% 5.64/1.24 $false|sQ595_spl),
% 5.64/1.24 inference(forward_subsumption_resolution,[status(thm)],[f22416,f5360])).
% 5.64/1.24 fof(f22422,plain,(
% 5.64/1.24 sQ595_spl),
% 5.64/1.24 inference(contradiction_clause,[status(thm)],[f22421])).
% 5.64/1.24 fof(f22424,plain,(
% 5.64/1.24 ~r2_hidden(k1_zfmisc_1(sK1206_skl),k3_tarski(k1_xboole_0))|~r2_hidden(k1_zfmisc_1(sK1206_skl),k3_tarski(k1_xboole_0))|~sQ589_spl|~sQ588_spl),
% 5.64/1.24 inference(resolution,[status(thm)],[f22307,f7240])).
% 5.64/1.24 fof(f22433,definition,(
% 5.64/1.24 sQ597_spl <=> (r2_hidden(k1_zfmisc_1(sK1206_skl),k3_tarski(k1_xboole_0)))),
% 5.64/1.24 introduced(definition,[new_symbols(definition,[sQ597_spl])],[split_symbol_definition])).
% 5.64/1.24 fof(f22436,plain,(
% 5.64/1.24 ~sQ597_spl|~sQ589_spl|~sQ588_spl),
% 5.64/1.24 inference(split_clause,[status(thm)],[f22424,f22433,f22232,f22218])).
% 5.64/1.24 fof(f22438,plain,(
% 5.64/1.24 k5_setfam_1(sK1206_skl,sK1207_skl)=k3_tarski(sK1207_skl)),
% 5.64/1.24 inference(resolution,[status(thm)],[f17608,f5819])).
% 5.64/1.24 fof(f22673,plain,(
% 5.64/1.24 ![X0]: (~m1_subset_1(k1_xboole_0,k1_zfmisc_1(k1_zfmisc_1(X0)))|m1_subset_1(k3_tarski(k1_xboole_0),k1_zfmisc_1(X0)))),
% 5.64/1.24 inference(paramodulation,[status(thm)],[f22194,f5817])).
% 5.64/1.24 fof(f22674,plain,(
% 5.64/1.24 ![X0]: (m1_subset_1(k3_tarski(k1_xboole_0),k1_zfmisc_1(X0)))),
% 5.64/1.24 inference(forward_subsumption_resolution,[status(thm)],[f22673,f5360])).
% 5.64/1.24 fof(f22833,plain,(
% 5.64/1.24 r1_tarski(k3_tarski(sK1207_skl),sK1206_skl)|~sQ588_spl),
% 5.64/1.24 inference(resolution,[status(thm)],[f22219,f5836])).
% 5.64/1.24 fof(f22835,plain,(
% 5.64/1.24 k1_xboole_0=k3_tarski(sK1207_skl)|~sQ419_spl),
% 5.64/1.24 inference(forward_demodulation,[status(thm)],[f20441,f22195])).
% 5.64/1.24 fof(f22921,definition,(
% 5.64/1.24 sQ603_spl <=> (r2_hidden(sK1207_skl,sK7_skl(sK1207_skl)))),
% 5.64/1.24 introduced(definition,[new_symbols(definition,[sQ603_spl])],[split_symbol_definition])).
% 5.64/1.24 fof(f22925,definition,(
% 5.64/1.24 ![X0]: (sQ604_spl <=> (~r2_hidden(X0,sK7_skl(sK1207_skl))|~r2_hidden(sK1207_skl,X0)))),
% 5.64/1.24 introduced(definition,[new_symbols(definition,[sQ604_spl])],[split_symbol_definition])).
% 5.64/1.24 fof(f23011,plain,(
% 5.64/1.24 ![X0]: (k1_xboole_0=X0|r2_hidden(sK7_skl(X0),X0))),
% 5.64/1.24 inference(resolution,[status(thm)],[f22117,f4546])).
% 5.64/1.24 fof(f23052,definition,(
% 5.64/1.24 ![X0]: (sQ606_spl <=> (~r2_hidden(X0,sK1207_skl)))),
% 5.64/1.24 introduced(definition,[new_symbols(definition,[sQ606_spl])],[split_symbol_definition])).
% 5.64/1.24 fof(f23053,plain,(
% 5.64/1.24 ![X0]: (~r2_hidden(X0,sK1207_skl)|~sQ606_spl)),
% 5.64/1.24 inference(component_clause,[status(thm)],[f23052])).
% 5.64/1.24 fof(f23055,definition,(
% 5.64/1.24 ![X1]: (sQ607_spl <=> (~r2_hidden(X1,sK1207_skl)|~r2_hidden(X1,k1_xboole_0)))),
% 5.64/1.24 introduced(definition,[new_symbols(definition,[sQ607_spl])],[split_symbol_definition])).
% 5.64/1.24 fof(f23059,plain,(
% 5.64/1.24 $false|~sQ606_spl|~sQ421_spl),
% 5.64/1.24 inference(backward_subsumption_resolution,[status(thm)],[f20448,f23053])).
% 5.64/1.24 fof(f23071,plain,(
% 5.64/1.24 ~sQ606_spl|~sQ421_spl),
% 5.64/1.24 inference(contradiction_clause,[status(thm)],[f23059])).
% 5.64/1.24 fof(f23073,plain,(
% 5.64/1.24 ![X0]: (r2_hidden(X0,k3_tarski(sK1207_skl))|~r2_hidden(X0,sK1208_skl)|~sQ421_spl)),
% 5.64/1.24 inference(resolution,[status(thm)],[f20448,f21097])).
% 5.64/1.24 fof(f23102,plain,(
% 5.64/1.24 ![X0]: (r2_hidden(X0,k1_xboole_0)|~r2_hidden(X0,sK1208_skl)|~sQ419_spl|~sQ421_spl)),
% 5.64/1.24 inference(forward_demodulation,[status(thm)],[f22835,f23073])).
% 5.64/1.24 fof(f23103,plain,(
% 5.64/1.24 ![X0]: (~r2_hidden(X0,sK1208_skl)|~sQ419_spl|~sQ421_spl)),
% 5.64/1.24 inference(forward_subsumption_resolution,[status(thm)],[f23102,f21100])).
% 5.64/1.24 fof(f23120,plain,(
% 5.64/1.24 k1_xboole_0=sK1208_skl|~sQ419_spl|~sQ421_spl),
% 5.64/1.24 inference(resolution,[status(thm)],[f23103,f22117])).
% 5.64/1.24 fof(f23126,plain,(
% 5.64/1.24 sQ422_spl|~sQ419_spl|~sQ421_spl),
% 5.64/1.24 inference(split_clause,[status(thm)],[f23120,f20451,f20440,f20447])).
% 5.64/1.24 fof(f23130,plain,(
% 5.64/1.24 r2_hidden(k3_tarski(sK1207_skl),k1_zfmisc_1(sK1206_skl))|~sQ588_spl),
% 5.64/1.24 inference(resolution,[status(thm)],[f22833,f21117])).
% 5.64/1.24 fof(f23131,plain,(
% 5.64/1.24 ![X0]: (sK6_skl(X0,sK1207_skl)=k1_xboole_0|X0=k3_tarski(sK1207_skl)|r2_hidden(sK5_skl(X0,sK1207_skl),X0)|~sQ420_spl)),
% 5.64/1.24 inference(resolution,[status(thm)],[f20444,f4542])).
% 5.64/1.24 fof(f23136,plain,(
% 5.64/1.24 sK0_skl(sK1207_skl,k1_xboole_0)=k1_xboole_0|k1_xboole_0=sK1207_skl|~sQ420_spl),
% 5.64/1.24 inference(resolution,[status(thm)],[f20444,f22117])).
% 5.64/1.24 fof(f23142,definition,(
% 5.64/1.24 sQ608_spl <=> (sK0_skl(sK1207_skl,k1_xboole_0)=k1_xboole_0)),
% 5.64/1.24 introduced(definition,[new_symbols(definition,[sQ608_spl])],[split_symbol_definition])).
% 5.64/1.24 fof(f23143,plain,(
% 5.64/1.24 sK0_skl(sK1207_skl,k1_xboole_0)=k1_xboole_0|~sQ608_spl),
% 5.64/1.24 inference(component_clause,[status(thm)],[f23142])).
% 5.64/1.24 fof(f23145,plain,(
% 5.64/1.24 sQ608_spl|sQ589_spl|~sQ420_spl),
% 5.64/1.24 inference(split_clause,[status(thm)],[f23136,f23142,f22232,f20443])).
% 5.64/1.24 fof(f23150,plain,(
% 5.64/1.24 r2_hidden(sK0_skl(k1_xboole_0,sK1207_skl),k1_xboole_0)|sK1207_skl=k1_xboole_0|~r2_hidden(sK1207_skl,k1_xboole_0)|~sQ590_spl),
% 5.64/1.24 inference(paramodulation,[status(thm)],[f22236,f22121])).
% 5.64/1.24 fof(f23152,plain,(
% 5.64/1.24 r2_hidden(sK0_skl(k1_xboole_0,sK1207_skl),sK1207_skl)|r2_hidden(k1_xboole_0,k1_xboole_0)|sK1207_skl=k1_xboole_0|~sQ590_spl),
% 5.64/1.24 inference(paramodulation,[status(thm)],[f22236,f4509])).
% 5.64/1.24 fof(f23154,definition,(
% 5.64/1.24 sQ609_spl <=> (r2_hidden(sK0_skl(k1_xboole_0,sK1207_skl),k1_xboole_0))),
% 5.64/1.24 introduced(definition,[new_symbols(definition,[sQ609_spl])],[split_symbol_definition])).
% 5.64/1.24 fof(f23155,plain,(
% 5.64/1.24 r2_hidden(sK0_skl(k1_xboole_0,sK1207_skl),k1_xboole_0)|~sQ609_spl),
% 5.64/1.24 inference(component_clause,[status(thm)],[f23154])).
% 5.64/1.24 fof(f23157,definition,(
% 5.64/1.24 sQ610_spl <=> (r2_hidden(sK1207_skl,k1_xboole_0))),
% 5.64/1.24 introduced(definition,[new_symbols(definition,[sQ610_spl])],[split_symbol_definition])).
% 5.64/1.24 fof(f23160,plain,(
% 5.64/1.24 sQ609_spl|sQ589_spl|~sQ610_spl|~sQ590_spl),
% 5.64/1.24 inference(split_clause,[status(thm)],[f23150,f23154,f22232,f23157,f22235])).
% 5.64/1.24 fof(f23162,definition,(
% 5.64/1.24 sQ611_spl <=> (r2_hidden(sK0_skl(k1_xboole_0,sK1207_skl),sK1207_skl))),
% 5.64/1.24 introduced(definition,[new_symbols(definition,[sQ611_spl])],[split_symbol_definition])).
% 5.64/1.24 fof(f23163,plain,(
% 5.64/1.24 r2_hidden(sK0_skl(k1_xboole_0,sK1207_skl),sK1207_skl)|~sQ611_spl),
% 5.64/1.24 inference(component_clause,[status(thm)],[f23162])).
% 5.64/1.24 fof(f23165,plain,(
% 5.64/1.24 sQ611_spl|sQ591_spl|sQ589_spl|~sQ590_spl),
% 5.64/1.24 inference(split_clause,[status(thm)],[f23152,f23162,f22269,f22232,f22235])).
% 5.64/1.24 fof(f23167,plain,(
% 5.64/1.24 r2_hidden(k1_xboole_0,sK1207_skl)|~sQ590_spl|~sQ611_spl),
% 5.64/1.24 inference(forward_demodulation,[status(thm)],[f22236,f23163])).
% 5.64/1.24 fof(f23168,plain,(
% 5.64/1.24 r2_hidden(k1_xboole_0,k1_xboole_0)|~sQ590_spl|~sQ609_spl),
% 5.64/1.24 inference(forward_demodulation,[status(thm)],[f22236,f23155])).
% 5.64/1.24 fof(f23169,plain,(
% 5.64/1.24 $false|~sQ590_spl|~sQ609_spl),
% 5.64/1.24 inference(forward_subsumption_resolution,[status(thm)],[f23168,f21100])).
% 5.64/1.24 fof(f23170,plain,(
% 5.64/1.24 ~sQ590_spl|~sQ609_spl),
% 5.64/1.24 inference(contradiction_clause,[status(thm)],[f23169])).
% 5.64/1.24 fof(f23173,plain,(
% 5.64/1.24 r2_hidden(sK7_skl(sK1207_skl),sK1207_skl)|~sQ590_spl|~sQ611_spl),
% 5.64/1.24 inference(resolution,[status(thm)],[f23167,f4546])).
% 5.64/1.24 fof(f23175,plain,(
% 5.64/1.24 ~r2_hidden(sK1207_skl,k1_xboole_0)|~r2_hidden(sK1207_skl,k1_xboole_0)|~r2_hidden(sK1207_skl,k1_xboole_0)|~sQ590_spl|~sQ611_spl),
% 5.64/1.24 inference(resolution,[status(thm)],[f23167,f7246])).
% 5.64/1.24 fof(f23177,plain,(
% 5.64/1.24 ![X0,X1]: (~r2_hidden(X0,k1_xboole_0)|~r2_hidden(sK1207_skl,X1)|~r2_hidden(X1,k1_xboole_0)|~r2_hidden(sK1207_skl,X0)|~sQ590_spl|~sQ611_spl)),
% 5.64/1.24 inference(resolution,[status(thm)],[f23167,f7246])).
% 5.64/1.24 fof(f23202,plain,(
% 5.64/1.24 ~sQ610_spl|~sQ590_spl|~sQ611_spl),
% 5.64/1.24 inference(split_clause,[status(thm)],[f23175,f23157,f22235,f23162])).
% 5.64/1.24 fof(f23203,definition,(
% 5.64/1.24 ![X0]: (sQ612_spl <=> (~r2_hidden(X0,k1_xboole_0)|~r2_hidden(sK1207_skl,X0)))),
% 5.64/1.24 introduced(definition,[new_symbols(definition,[sQ612_spl])],[split_symbol_definition])).
% 5.64/1.24 fof(f23206,plain,(
% 5.64/1.24 sQ612_spl|~sQ590_spl|~sQ611_spl),
% 5.64/1.24 inference(split_clause,[status(thm)],[f23177,f23203,f22235,f23162])).
% 5.64/1.24 fof(f23224,plain,(
% 5.64/1.24 r2_hidden(sK0_skl(sK1207_skl,k1_xboole_0),sK1207_skl)|k1_xboole_0=sK1207_skl|~r2_hidden(k1_xboole_0,k1_xboole_0)|~sQ608_spl),
% 5.64/1.24 inference(paramodulation,[status(thm)],[f23143,f22121])).
% 5.64/1.24 fof(f23225,plain,(
% 5.64/1.24 ~r2_hidden(k1_xboole_0,k1_xboole_0)|~r2_hidden(sK0_skl(sK1207_skl,k1_xboole_0),sK1207_skl)|k1_xboole_0=sK1207_skl|~sQ608_spl),
% 5.64/1.24 inference(paramodulation,[status(thm)],[f23143,f4510])).
% 5.64/1.24 fof(f23227,plain,(
% 5.64/1.24 r2_hidden(k1_xboole_0,k1_xboole_0)|r2_hidden(sK0_skl(sK1207_skl,k1_xboole_0),sK1207_skl)|k1_xboole_0=sK1207_skl|~sQ608_spl),
% 5.64/1.24 inference(paramodulation,[status(thm)],[f23143,f4509])).
% 5.64/1.24 fof(f23229,definition,(
% 5.64/1.24 sQ614_spl <=> (r2_hidden(sK0_skl(sK1207_skl,k1_xboole_0),sK1207_skl))),
% 5.64/1.24 introduced(definition,[new_symbols(definition,[sQ614_spl])],[split_symbol_definition])).
% 5.64/1.24 fof(f23232,plain,(
% 5.64/1.24 sQ614_spl|sQ589_spl|~sQ591_spl|~sQ608_spl),
% 5.64/1.24 inference(split_clause,[status(thm)],[f23224,f23229,f22232,f22269,f23142])).
% 5.64/1.24 fof(f23233,plain,(
% 5.64/1.24 ~sQ591_spl|~sQ614_spl|sQ589_spl|~sQ608_spl),
% 5.64/1.24 inference(split_clause,[status(thm)],[f23225,f22269,f23229,f22232,f23142])).
% 5.64/1.24 fof(f23234,definition,(
% 5.64/1.24 sQ615_spl <=> (r2_hidden(sK0_skl(sK1207_skl,k1_xboole_0),k1_xboole_0))),
% 5.64/1.24 introduced(definition,[new_symbols(definition,[sQ615_spl])],[split_symbol_definition])).
% 5.64/1.24 fof(f23235,plain,(
% 5.64/1.24 r2_hidden(sK0_skl(sK1207_skl,k1_xboole_0),k1_xboole_0)|~sQ615_spl),
% 5.64/1.24 inference(component_clause,[status(thm)],[f23234])).
% 5.64/1.24 fof(f23238,plain,(
% 5.64/1.24 sQ591_spl|sQ614_spl|sQ589_spl|~sQ608_spl),
% 5.64/1.24 inference(split_clause,[status(thm)],[f23227,f22269,f23229,f22232,f23142])).
% 5.64/1.24 fof(f23239,plain,(
% 5.64/1.24 r2_hidden(k1_xboole_0,k1_xboole_0)|~sQ608_spl|~sQ615_spl),
% 5.64/1.24 inference(forward_demodulation,[status(thm)],[f23143,f23235])).
% 5.64/1.24 fof(f23240,plain,(
% 5.64/1.24 $false|~sQ608_spl|~sQ615_spl),
% 5.64/1.24 inference(forward_subsumption_resolution,[status(thm)],[f23239,f21100])).
% 5.64/1.24 fof(f23241,plain,(
% 5.64/1.24 ~sQ608_spl|~sQ615_spl),
% 5.64/1.24 inference(contradiction_clause,[status(thm)],[f23240])).
% 5.64/1.24 fof(f23244,plain,(
% 5.64/1.24 sK7_skl(sK1207_skl)=k1_xboole_0|~sQ590_spl|~sQ611_spl|~sQ420_spl),
% 5.64/1.24 inference(resolution,[status(thm)],[f23173,f20444])).
% 5.64/1.24 fof(f23247,plain,(
% 5.64/1.24 ~r2_hidden(sK1207_skl,sK7_skl(sK1207_skl))|~r2_hidden(sK1207_skl,sK7_skl(sK1207_skl))|~r2_hidden(sK1207_skl,sK7_skl(sK1207_skl))|~sQ590_spl|~sQ611_spl),
% 5.64/1.24 inference(resolution,[status(thm)],[f23173,f7246])).
% 5.64/1.24 fof(f23249,plain,(
% 5.64/1.24 ![X0,X1]: (~r2_hidden(X0,sK7_skl(sK1207_skl))|~r2_hidden(sK1207_skl,X1)|~r2_hidden(X1,sK7_skl(sK1207_skl))|~r2_hidden(sK1207_skl,X0)|~sQ590_spl|~sQ611_spl)),
% 5.64/1.24 inference(resolution,[status(thm)],[f23173,f7246])).
% 5.64/1.24 fof(f23274,plain,(
% 5.64/1.24 ~sQ603_spl|~sQ590_spl|~sQ611_spl),
% 5.64/1.24 inference(split_clause,[status(thm)],[f23247,f22921,f22235,f23162])).
% 5.64/1.24 fof(f23275,plain,(
% 5.64/1.24 sQ604_spl|~sQ590_spl|~sQ611_spl),
% 5.64/1.24 inference(split_clause,[status(thm)],[f23249,f22925,f22235,f23162])).
% 5.64/1.24 fof(f23287,plain,(
% 5.64/1.24 ![X0,X1]: (~r2_hidden(X0,sK1207_skl)|~r2_hidden(X1,sK1207_skl)|~r2_hidden(X1,k1_xboole_0)|~sQ590_spl|~sQ611_spl|~sQ420_spl)),
% 5.64/1.24 inference(paramodulation,[status(thm)],[f23244,f4547])).
% 5.64/1.24 fof(f23288,plain,(
% 5.64/1.24 sQ606_spl|sQ607_spl|~sQ590_spl|~sQ611_spl|~sQ420_spl),
% 5.64/1.24 inference(split_clause,[status(thm)],[f23287,f23052,f23055,f22235,f23162,f20443])).
% 5.64/1.24 fof(f23375,plain,(
% 5.64/1.24 r2_hidden(k1_xboole_0,sK1207_skl)|sK1207_skl=k1_xboole_0|~sQ590_spl),
% 5.64/1.24 inference(paramodulation,[status(thm)],[f22236,f22123])).
% 5.64/1.24 fof(f23383,plain,(
% 5.64/1.24 sQ584_spl|sQ589_spl|~sQ590_spl),
% 5.64/1.24 inference(split_clause,[status(thm)],[f23375,f22159,f22232,f22235])).
% 5.64/1.24 fof(f23483,plain,(
% 5.64/1.24 m1_subset_1(sK0_skl(sK1207_skl,k1_xboole_0),sK1207_skl)|r2_hidden(k1_xboole_0,k1_xboole_0)|k1_xboole_0=sK1207_skl|~sQ608_spl),
% 5.64/1.24 inference(paramodulation,[status(thm)],[f23143,f22144])).
% 5.64/1.24 fof(f23491,definition,(
% 5.64/1.24 sQ616_spl <=> (m1_subset_1(k1_xboole_0,sK1207_skl))),
% 5.64/1.24 introduced(definition,[new_symbols(definition,[sQ616_spl])],[split_symbol_definition])).
% 5.64/1.24 fof(f23499,definition,(
% 5.64/1.24 sQ618_spl <=> (m1_subset_1(sK0_skl(sK1207_skl,k1_xboole_0),sK1207_skl))),
% 5.64/1.24 introduced(definition,[new_symbols(definition,[sQ618_spl])],[split_symbol_definition])).
% 5.64/1.24 fof(f23502,plain,(
% 5.64/1.24 sQ618_spl|sQ591_spl|sQ589_spl|~sQ608_spl),
% 5.64/1.24 inference(split_clause,[status(thm)],[f23483,f23499,f22269,f22232,f23142])).
% 5.64/1.24 fof(f23546,plain,(
% 5.64/1.24 k1_xboole_0=sK1207_skl|sK7_skl(sK1207_skl)=k1_xboole_0|~sQ420_spl),
% 5.64/1.24 inference(resolution,[status(thm)],[f23011,f20444])).
% 5.64/1.24 fof(f23581,plain,(
% 5.64/1.24 ![X0]: (k1_xboole_0=X0|m1_subset_1(sK7_skl(X0),X0))),
% 5.64/1.24 inference(resolution,[status(thm)],[f23011,f5831])).
% 5.64/1.24 fof(f23584,definition,(
% 5.64/1.24 sQ620_spl <=> (sK7_skl(sK1207_skl)=k1_xboole_0)),
% 5.64/1.24 introduced(definition,[new_symbols(definition,[sQ620_spl])],[split_symbol_definition])).
% 5.64/1.24 fof(f23587,plain,(
% 5.64/1.24 sQ589_spl|sQ620_spl|~sQ420_spl),
% 5.64/1.24 inference(split_clause,[status(thm)],[f23546,f22232,f23584,f20443])).
% 5.64/1.24 fof(f23653,plain,(
% 5.64/1.24 m1_subset_1(k1_xboole_0,sK1207_skl)|r2_hidden(sK0_skl(k1_xboole_0,sK1207_skl),k1_xboole_0)|sK1207_skl=k1_xboole_0|~sQ590_spl),
% 5.64/1.24 inference(paramodulation,[status(thm)],[f22236,f22146])).
% 5.64/1.24 fof(f23655,plain,(
% 5.64/1.24 m1_subset_1(sK0_skl(k1_xboole_0,sK1207_skl),sK1207_skl)|r2_hidden(k1_xboole_0,k1_xboole_0)|sK1207_skl=k1_xboole_0|~sQ590_spl),
% 5.64/1.24 inference(paramodulation,[status(thm)],[f22236,f22146])).
% 5.64/1.24 fof(f23662,plain,(
% 5.64/1.24 sQ616_spl|sQ609_spl|sQ589_spl|~sQ590_spl),
% 5.64/1.24 inference(split_clause,[status(thm)],[f23653,f23491,f23154,f22232,f22235])).
% 5.64/1.24 fof(f23667,definition,(
% 5.64/1.24 sQ622_spl <=> (m1_subset_1(sK0_skl(k1_xboole_0,sK1207_skl),sK1207_skl))),
% 5.64/1.24 introduced(definition,[new_symbols(definition,[sQ622_spl])],[split_symbol_definition])).
% 5.64/1.24 fof(f23670,plain,(
% 5.64/1.24 sQ622_spl|sQ591_spl|sQ589_spl|~sQ590_spl),
% 5.64/1.24 inference(split_clause,[status(thm)],[f23655,f23667,f22269,f22232,f22235])).
% 5.64/1.24 fof(f23720,plain,(
% 5.64/1.24 ~r2_hidden(k1_zfmisc_1(k1_zfmisc_1(sK1206_skl)),sK1207_skl)|~r2_hidden(k1_zfmisc_1(k1_zfmisc_1(sK1206_skl)),sK1207_skl)|~r2_hidden(k1_zfmisc_1(k1_zfmisc_1(sK1206_skl)),sK1207_skl)),
% 5.64/1.24 inference(resolution,[status(thm)],[f22215,f7246])).
% 5.64/1.24 fof(f23722,plain,(
% 5.64/1.24 ![X0,X1]: (~r2_hidden(X0,sK1207_skl)|~r2_hidden(k1_zfmisc_1(k1_zfmisc_1(sK1206_skl)),X1)|~r2_hidden(X1,sK1207_skl)|~r2_hidden(k1_zfmisc_1(k1_zfmisc_1(sK1206_skl)),X0))),
% 5.64/1.24 inference(resolution,[status(thm)],[f22215,f7246])).
% 5.64/1.24 fof(f23747,definition,(
% 5.64/1.24 sQ624_spl <=> (r2_hidden(k1_zfmisc_1(k1_zfmisc_1(sK1206_skl)),sK1207_skl))),
% 5.64/1.24 introduced(definition,[new_symbols(definition,[sQ624_spl])],[split_symbol_definition])).
% 5.64/1.24 fof(f23750,plain,(
% 5.64/1.24 ~sQ624_spl),
% 5.64/1.24 inference(split_clause,[status(thm)],[f23720,f23747])).
% 5.64/1.24 fof(f23751,definition,(
% 5.64/1.24 ![X0]: (sQ625_spl <=> (~r2_hidden(X0,sK1207_skl)|~r2_hidden(k1_zfmisc_1(k1_zfmisc_1(sK1206_skl)),X0)))),
% 5.64/1.24 introduced(definition,[new_symbols(definition,[sQ625_spl])],[split_symbol_definition])).
% 5.64/1.24 fof(f23754,plain,(
% 5.64/1.24 sQ625_spl),
% 5.64/1.24 inference(split_clause,[status(thm)],[f23722,f23751])).
% 5.64/1.24 fof(f23767,plain,(
% 5.64/1.24 ~m1_subset_1(sK1207_skl,k1_zfmisc_1(k1_zfmisc_1(sK1206_skl)))|sK1207_skl=k1_xboole_0|r1_tarski(k8_setfam_1(sK1206_skl,sK1207_skl),k3_tarski(sK1207_skl))),
% 5.64/1.24 inference(paramodulation,[status(thm)],[f22438,f14894])).
% 5.64/1.24 fof(f23769,definition,(
% 5.64/1.24 sQ627_spl <=> (r1_tarski(k8_setfam_1(sK1206_skl,sK1207_skl),k3_tarski(sK1207_skl)))),
% 5.64/1.24 introduced(definition,[new_symbols(definition,[sQ627_spl])],[split_symbol_definition])).
% 5.64/1.24 fof(f23772,plain,(
% 5.64/1.24 ~sQ586_spl|sQ589_spl|sQ627_spl),
% 5.64/1.24 inference(split_clause,[status(thm)],[f23767,f22169,f22232,f23769])).
% 5.64/1.24 fof(f23791,plain,(
% 5.64/1.24 sK1207_skl=k1_xboole_0|sK22_skl(sK1207_skl)=k1_xboole_0|~sQ420_spl),
% 5.64/1.24 inference(resolution,[status(thm)],[f4597,f20444])).
% 5.64/1.24 fof(f23826,plain,(
% 5.64/1.24 ![X0]: (X0=k1_xboole_0|m1_subset_1(sK22_skl(X0),X0))),
% 5.64/1.24 inference(resolution,[status(thm)],[f4597,f5831])).
% 5.64/1.24 fof(f23828,definition,(
% 5.64/1.24 sQ628_spl <=> (sK22_skl(sK1207_skl)=k1_xboole_0)),
% 5.64/1.24 introduced(definition,[new_symbols(definition,[sQ628_spl])],[split_symbol_definition])).
% 5.64/1.24 fof(f23831,plain,(
% 5.64/1.24 sQ589_spl|sQ628_spl|~sQ420_spl),
% 5.64/1.24 inference(split_clause,[status(thm)],[f23791,f22232,f23828,f20443])).
% 5.64/1.24 fof(f23862,plain,(
% 5.64/1.24 ![X0]: (r2_hidden(k1_xboole_0,k2_xboole_0(sK1207_skl,X0))|~sQ590_spl|~sQ611_spl)),
% 5.64/1.24 inference(resolution,[status(thm)],[f21102,f23167])).
% 5.64/1.24 fof(f23883,plain,(
% 5.64/1.24 ![X0]: (r2_hidden(k1_xboole_0,sK1207_skl)|r2_hidden(k1_xboole_0,X0)|~sQ590_spl|~sQ611_spl)),
% 5.64/1.24 inference(resolution,[status(thm)],[f23862,f21101])).
% 5.64/1.24 fof(f23914,definition,(
% 5.64/1.24 ![X0]: (sQ629_spl <=> (r2_hidden(k1_xboole_0,X0)))),
% 5.64/1.24 introduced(definition,[new_symbols(definition,[sQ629_spl])],[split_symbol_definition])).
% 5.64/1.24 fof(f23915,plain,(
% 5.64/1.24 ![X0]: (r2_hidden(k1_xboole_0,X0)|~sQ629_spl)),
% 5.64/1.24 inference(component_clause,[status(thm)],[f23914])).
% 5.64/1.24 fof(f23917,plain,(
% 5.64/1.24 sQ584_spl|sQ629_spl|~sQ590_spl|~sQ611_spl),
% 5.64/1.24 inference(split_clause,[status(thm)],[f23883,f22159,f23914,f22235,f23162])).
% 5.64/1.24 fof(f23935,plain,(
% 5.64/1.24 $false|~sQ629_spl),
% 5.64/1.24 inference(resolution,[status(thm)],[f23915,f21100])).
% 5.64/1.24 fof(f23975,plain,(
% 5.64/1.24 ~sQ629_spl),
% 5.64/1.24 inference(contradiction_clause,[status(thm)],[f23935])).
% 5.64/1.24 fof(f24131,plain,(
% 5.64/1.24 ![X0]: (sK1207_skl=k1_tarski(X0)|sK1_skl(sK1207_skl,X0)=X0|m1_subset_1(k1_xboole_0,sK1207_skl)|sK1207_skl=k1_tarski(X0)|sK1_skl(sK1207_skl,X0)=X0|~sQ420_spl)),
% 5.64/1.24 inference(paramodulation,[status(thm)],[f22178,f22154])).
% 5.64/1.24 fof(f24132,plain,(
% 5.64/1.24 ![X0]: (sK1207_skl=k1_tarski(X0)|r2_hidden(k1_xboole_0,sK1207_skl)|sK1_skl(sK1207_skl,X0)=X0|sK1207_skl=k1_tarski(X0)|sK1_skl(sK1207_skl,X0)=X0|~sQ420_spl)),
% 5.64/1.24 inference(paramodulation,[status(thm)],[f22178,f4517])).
% 5.64/1.24 fof(f24133,plain,(
% 5.64/1.24 ![X0]: (sK1207_skl=k1_tarski(X0)|~r2_hidden(k1_xboole_0,sK1207_skl)|~sK1_skl(sK1207_skl,X0)=X0|sK1207_skl=k1_tarski(X0)|sK1_skl(sK1207_skl,X0)=X0|~sQ420_spl)),
% 5.64/1.24 inference(paramodulation,[status(thm)],[f22178,f4516])).
% 5.64/1.24 fof(f24135,definition,(
% 5.64/1.24 ![X0]: (sQ631_spl <=> (sK1207_skl=k1_tarski(X0)|sK1_skl(sK1207_skl,X0)=X0|sK1207_skl=k1_tarski(X0)|sK1_skl(sK1207_skl,X0)=X0))),
% 5.64/1.24 introduced(definition,[new_symbols(definition,[sQ631_spl])],[split_symbol_definition])).
% 5.64/1.24 fof(f24138,plain,(
% 5.64/1.24 sQ631_spl|sQ616_spl|~sQ420_spl),
% 5.64/1.24 inference(split_clause,[status(thm)],[f24131,f24135,f23491,f20443])).
% 5.64/1.24 fof(f24139,plain,(
% 5.64/1.24 sQ631_spl|sQ584_spl|~sQ420_spl),
% 5.64/1.24 inference(split_clause,[status(thm)],[f24132,f24135,f22159,f20443])).
% 5.64/1.24 fof(f24140,definition,(
% 5.64/1.24 ![X0]: (sQ632_spl <=> (sK1207_skl=k1_tarski(X0)|~sK1_skl(sK1207_skl,X0)=X0|sK1207_skl=k1_tarski(X0)|sK1_skl(sK1207_skl,X0)=X0))),
% 5.64/1.24 introduced(definition,[new_symbols(definition,[sQ632_spl])],[split_symbol_definition])).
% 5.64/1.24 fof(f24143,plain,(
% 5.64/1.24 sQ632_spl|~sQ584_spl|~sQ420_spl),
% 5.64/1.24 inference(split_clause,[status(thm)],[f24133,f24140,f22159,f20443])).
% 5.64/1.24 fof(f24187,plain,(
% 5.64/1.24 ![X0]: (sK1207_skl=k1_tarski(X0)|sK1_skl(sK1207_skl,X0)=X0|~r2_hidden(sK1207_skl,k1_xboole_0)|sK1207_skl=k1_tarski(X0)|sK1_skl(sK1207_skl,X0)=X0|~sQ420_spl)),
% 5.64/1.24 inference(paramodulation,[status(thm)],[f22178,f22155])).
% 5.64/1.24 fof(f24188,plain,(
% 5.64/1.24 sQ631_spl|~sQ610_spl|~sQ420_spl),
% 5.64/1.24 inference(split_clause,[status(thm)],[f24187,f24135,f23157,f20443])).
% 5.64/1.24 fof(f24588,plain,(
% 5.64/1.24 r1_tarski(k3_tarski(sK1207_skl),sK1206_skl)|~m1_subset_1(sK1207_skl,k1_zfmisc_1(k1_zfmisc_1(sK1206_skl)))),
% 5.64/1.24 inference(paramodulation,[status(thm)],[f22438,f22188])).
% 5.64/1.24 fof(f24590,definition,(
% 5.64/1.24 sQ637_spl <=> (r1_tarski(k3_tarski(sK1207_skl),sK1206_skl))),
% 5.64/1.24 introduced(definition,[new_symbols(definition,[sQ637_spl])],[split_symbol_definition])).
% 5.64/1.24 fof(f24593,plain,(
% 5.64/1.24 sQ637_spl|~sQ586_spl),
% 5.64/1.24 inference(split_clause,[status(thm)],[f24588,f24590,f22169])).
% 5.64/1.24 fof(f25172,plain,(
% 5.64/1.24 ~r2_hidden(k1_zfmisc_1(sK1206_skl),k3_tarski(sK1207_skl))|~r2_hidden(k1_zfmisc_1(sK1206_skl),k3_tarski(sK1207_skl))|~r2_hidden(k1_zfmisc_1(sK1206_skl),k3_tarski(sK1207_skl))|~sQ588_spl),
% 5.64/1.24 inference(resolution,[status(thm)],[f23130,f7246])).
% 5.64/1.24 fof(f25174,plain,(
% 5.64/1.24 ![X0,X1]: (~r2_hidden(X0,k3_tarski(sK1207_skl))|~r2_hidden(k1_zfmisc_1(sK1206_skl),X1)|~r2_hidden(X1,k3_tarski(sK1207_skl))|~r2_hidden(k1_zfmisc_1(sK1206_skl),X0)|~sQ588_spl)),
% 5.64/1.24 inference(resolution,[status(thm)],[f23130,f7246])).
% 5.64/1.24 fof(f25199,definition,(
% 5.64/1.24 sQ638_spl <=> (r2_hidden(k1_zfmisc_1(sK1206_skl),k3_tarski(sK1207_skl)))),
% 5.64/1.24 introduced(definition,[new_symbols(definition,[sQ638_spl])],[split_symbol_definition])).
% 5.64/1.24 fof(f25202,plain,(
% 5.64/1.24 ~sQ638_spl|~sQ588_spl),
% 5.64/1.24 inference(split_clause,[status(thm)],[f25172,f25199,f22218])).
% 5.64/1.24 fof(f25203,definition,(
% 5.64/1.24 ![X0]: (sQ639_spl <=> (~r2_hidden(X0,k3_tarski(sK1207_skl))|~r2_hidden(k1_zfmisc_1(sK1206_skl),X0)))),
% 5.64/1.24 introduced(definition,[new_symbols(definition,[sQ639_spl])],[split_symbol_definition])).
% 5.64/1.24 fof(f25206,plain,(
% 5.64/1.24 sQ639_spl|~sQ588_spl),
% 5.64/1.24 inference(split_clause,[status(thm)],[f25174,f25203,f22218])).
% 5.64/1.24 fof(f25223,plain,(
% 5.64/1.24 ![X0]: (~r2_hidden(X0,sK7_skl(k1_zfmisc_1(sK20_skl)))|k1_xboole_0=k1_zfmisc_1(sK20_skl))),
% 5.64/1.24 inference(resolution,[status(thm)],[f22255,f23581])).
% 5.64/1.24 fof(f25224,plain,(
% 5.64/1.24 ![X0]: (~r2_hidden(X0,sK22_skl(k1_zfmisc_1(sK20_skl)))|k1_zfmisc_1(sK20_skl)=k1_xboole_0)),
% 5.64/1.24 inference(resolution,[status(thm)],[f22255,f23826])).
% 5.64/1.24 fof(f25228,plain,(
% 5.64/1.24 ![X0]: (~r2_hidden(X0,k3_tarski(k1_xboole_0)))),
% 5.64/1.24 inference(resolution,[status(thm)],[f22255,f22674])).
% 5.64/1.24 fof(f25231,plain,(
% 5.64/1.24 ![X0]: (~r2_hidden(X0,sK20_skl))),
% 5.64/1.24 inference(resolution,[status(thm)],[f22255,f22199])).
% 5.64/1.24 fof(f25233,definition,(
% 5.64/1.24 ![X0]: (sQ641_spl <=> (~r2_hidden(X0,sK7_skl(k1_zfmisc_1(sK20_skl)))))),
% 5.64/1.24 introduced(definition,[new_symbols(definition,[sQ641_spl])],[split_symbol_definition])).
% 5.64/1.24 fof(f25236,definition,(
% 5.64/1.24 sQ642_spl <=> (k1_xboole_0=k1_zfmisc_1(sK20_skl))),
% 5.64/1.24 introduced(definition,[new_symbols(definition,[sQ642_spl])],[split_symbol_definition])).
% 5.64/1.24 fof(f25237,plain,(
% 5.64/1.24 k1_xboole_0=k1_zfmisc_1(sK20_skl)|~sQ642_spl),
% 5.64/1.24 inference(component_clause,[status(thm)],[f25236])).
% 5.64/1.24 fof(f25239,plain,(
% 5.64/1.24 sQ641_spl|sQ642_spl),
% 5.64/1.24 inference(split_clause,[status(thm)],[f25223,f25233,f25236])).
% 5.64/1.24 fof(f25240,definition,(
% 5.64/1.24 ![X0]: (sQ643_spl <=> (~r2_hidden(X0,sK22_skl(k1_zfmisc_1(sK20_skl)))))),
% 5.64/1.24 introduced(definition,[new_symbols(definition,[sQ643_spl])],[split_symbol_definition])).
% 5.64/1.24 fof(f25243,plain,(
% 5.64/1.24 sQ643_spl|sQ642_spl),
% 5.64/1.24 inference(split_clause,[status(thm)],[f25224,f25240,f25236])).
% 5.64/1.24 fof(f25244,plain,(
% 5.64/1.24 ![X0]: (~r2_hidden(X0,sK7_skl(k1_zfmisc_1(k1_xboole_0)))|k1_xboole_0=k1_zfmisc_1(k1_xboole_0))),
% 5.64/1.24 inference(resolution,[status(thm)],[f22256,f23581])).
% 5.64/1.24 fof(f25245,plain,(
% 5.64/1.24 ![X0]: (~r2_hidden(X0,sK22_skl(k1_zfmisc_1(k1_xboole_0)))|k1_zfmisc_1(k1_xboole_0)=k1_xboole_0)),
% 5.64/1.24 inference(resolution,[status(thm)],[f22256,f23826])).
% 5.64/1.24 fof(f25254,definition,(
% 5.64/1.24 ![X0]: (sQ644_spl <=> (~r2_hidden(X0,sK7_skl(k1_zfmisc_1(k1_xboole_0)))))),
% 5.64/1.24 introduced(definition,[new_symbols(definition,[sQ644_spl])],[split_symbol_definition])).
% 5.64/1.24 fof(f25257,definition,(
% 5.64/1.24 sQ645_spl <=> (k1_xboole_0=k1_zfmisc_1(k1_xboole_0))),
% 5.64/1.24 introduced(definition,[new_symbols(definition,[sQ645_spl])],[split_symbol_definition])).
% 5.64/1.24 fof(f25258,plain,(
% 5.64/1.24 k1_xboole_0=k1_zfmisc_1(k1_xboole_0)|~sQ645_spl),
% 5.64/1.24 inference(component_clause,[status(thm)],[f25257])).
% 5.64/1.24 fof(f25260,plain,(
% 5.64/1.24 sQ644_spl|sQ645_spl),
% 5.64/1.24 inference(split_clause,[status(thm)],[f25244,f25254,f25257])).
% 5.64/1.24 fof(f25261,definition,(
% 5.64/1.24 ![X0]: (sQ646_spl <=> (~r2_hidden(X0,sK22_skl(k1_zfmisc_1(k1_xboole_0)))))),
% 5.64/1.24 introduced(definition,[new_symbols(definition,[sQ646_spl])],[split_symbol_definition])).
% 5.64/1.24 fof(f25264,plain,(
% 5.64/1.24 sQ646_spl|sQ645_spl),
% 5.64/1.24 inference(split_clause,[status(thm)],[f25245,f25261,f25257])).
% 5.64/1.24 fof(f25451,plain,(
% 5.64/1.24 k1_xboole_0=sK20_skl),
% 5.64/1.24 inference(resolution,[status(thm)],[f25231,f23011])).
% 5.64/1.24 fof(f25471,plain,(
% 5.64/1.24 sK0_skl(sK1207_skl,sK20_skl)=k1_xboole_0|sK20_skl=sK1207_skl|~sQ420_spl),
% 5.64/1.24 inference(resolution,[status(thm)],[f25231,f22181])).
% 5.64/1.24 fof(f25473,plain,(
% 5.64/1.24 sK0_skl(sK20_skl,sK1207_skl)=k1_xboole_0|sK1207_skl=sK20_skl|~sQ420_spl),
% 5.64/1.24 inference(resolution,[status(thm)],[f25231,f22183])).
% 5.64/1.24 fof(f25481,definition,(
% 5.64/1.24 sQ647_spl <=> (sK0_skl(sK1207_skl,sK20_skl)=k1_xboole_0)),
% 5.64/1.24 introduced(definition,[new_symbols(definition,[sQ647_spl])],[split_symbol_definition])).
% 5.64/1.24 fof(f25484,definition,(
% 5.64/1.24 sQ648_spl <=> (sK20_skl=sK1207_skl)),
% 5.64/1.24 introduced(definition,[new_symbols(definition,[sQ648_spl])],[split_symbol_definition])).
% 5.64/1.24 fof(f25485,plain,(
% 5.64/1.24 sK20_skl=sK1207_skl|~sQ648_spl),
% 5.64/1.24 inference(component_clause,[status(thm)],[f25484])).
% 5.64/1.24 fof(f25487,plain,(
% 5.64/1.24 sQ647_spl|sQ648_spl|~sQ420_spl),
% 5.64/1.24 inference(split_clause,[status(thm)],[f25471,f25481,f25484,f20443])).
% 5.64/1.24 fof(f25488,definition,(
% 5.64/1.24 sQ649_spl <=> (sK0_skl(sK20_skl,sK1207_skl)=k1_xboole_0)),
% 5.64/1.24 introduced(definition,[new_symbols(definition,[sQ649_spl])],[split_symbol_definition])).
% 5.64/1.24 fof(f25491,plain,(
% 5.64/1.24 sQ649_spl|sQ648_spl|~sQ420_spl),
% 5.64/1.24 inference(split_clause,[status(thm)],[f25473,f25488,f25484,f20443])).
% 5.64/1.24 fof(f25495,plain,(
% 5.64/1.24 k1_xboole_0=sK1207_skl|~sQ648_spl),
% 5.64/1.24 inference(forward_demodulation,[status(thm)],[f25451,f25485])).
% 5.64/1.24 fof(f25496,plain,(
% 5.64/1.24 $false|sQ589_spl|~sQ648_spl),
% 5.64/1.24 inference(forward_subsumption_resolution,[status(thm)],[f25495,f22234])).
% 5.64/1.24 fof(f25497,plain,(
% 5.64/1.24 sQ589_spl|~sQ648_spl),
% 5.64/1.24 inference(contradiction_clause,[status(thm)],[f25496])).
% 5.64/1.24 fof(f25502,plain,(
% 5.64/1.24 k1_xboole_0=k1_zfmisc_1(k1_xboole_0)|~sQ642_spl),
% 5.64/1.24 inference(forward_demodulation,[status(thm)],[f25451,f25237])).
% 5.64/1.24 fof(f25509,plain,(
% 5.64/1.24 r2_hidden(k1_xboole_0,k1_xboole_0)|~sQ642_spl),
% 5.64/1.24 inference(paramodulation,[status(thm)],[f25502,f22192])).
% 5.64/1.24 fof(f25533,plain,(
% 5.64/1.24 $false|~sQ642_spl),
% 5.64/1.24 inference(forward_subsumption_resolution,[status(thm)],[f25509,f21100])).
% 5.64/1.24 fof(f25534,plain,(
% 5.64/1.24 ~sQ642_spl),
% 5.64/1.24 inference(contradiction_clause,[status(thm)],[f25533])).
% 5.64/1.24 fof(f25542,plain,(
% 5.64/1.24 r2_hidden(k1_xboole_0,k1_xboole_0)|~sQ645_spl),
% 5.64/1.24 inference(paramodulation,[status(thm)],[f25258,f22192])).
% 5.64/1.24 fof(f25566,plain,(
% 5.64/1.24 $false|~sQ645_spl),
% 5.64/1.24 inference(forward_subsumption_resolution,[status(thm)],[f25542,f21100])).
% 5.64/1.24 fof(f25567,plain,(
% 5.64/1.24 ~sQ645_spl),
% 5.64/1.24 inference(contradiction_clause,[status(thm)],[f25566])).
% 5.64/1.24 fof(f25629,plain,(
% 5.64/1.24 sK6_skl(k1_xboole_0,sK1207_skl)=k1_xboole_0|k1_xboole_0=k3_tarski(sK1207_skl)|~sQ420_spl),
% 5.64/1.24 inference(resolution,[status(thm)],[f23131,f21100])).
% 5.64/1.24 fof(f25674,definition,(
% 5.64/1.24 sQ654_spl <=> (sK6_skl(k1_xboole_0,sK1207_skl)=k1_xboole_0)),
% 5.64/1.24 introduced(definition,[new_symbols(definition,[sQ654_spl])],[split_symbol_definition])).
% 5.64/1.24 fof(f25675,plain,(
% 5.64/1.24 sK6_skl(k1_xboole_0,sK1207_skl)=k1_xboole_0|~sQ654_spl),
% 5.64/1.24 inference(component_clause,[status(thm)],[f25674])).
% 5.64/1.24 fof(f25677,definition,(
% 5.64/1.24 sQ655_spl <=> (k1_xboole_0=k3_tarski(sK1207_skl))),
% 5.64/1.24 introduced(definition,[new_symbols(definition,[sQ655_spl])],[split_symbol_definition])).
% 5.64/1.24 fof(f25678,plain,(
% 5.64/1.24 k1_xboole_0=k3_tarski(sK1207_skl)|~sQ655_spl),
% 5.64/1.24 inference(component_clause,[status(thm)],[f25677])).
% 5.64/1.24 fof(f25680,plain,(
% 5.64/1.24 sQ654_spl|sQ655_spl|~sQ420_spl),
% 5.64/1.24 inference(split_clause,[status(thm)],[f25629,f25674,f25677,f20443])).
% 5.64/1.24 fof(f25686,plain,(
% 5.64/1.24 $false|sQ419_spl|~sQ655_spl),
% 5.64/1.24 inference(forward_subsumption_resolution,[status(thm)],[f25678,f22216])).
% 5.64/1.24 fof(f25687,plain,(
% 5.64/1.24 sQ419_spl|~sQ655_spl),
% 5.64/1.24 inference(contradiction_clause,[status(thm)],[f25686])).
% 5.64/1.24 fof(f25708,plain,(
% 5.64/1.24 k1_xboole_0=k3_tarski(k1_xboole_0)),
% 5.64/1.24 inference(resolution,[status(thm)],[f25228,f23011])).
% 5.64/1.24 fof(f25728,plain,(
% 5.64/1.24 sK0_skl(sK1207_skl,k3_tarski(k1_xboole_0))=k1_xboole_0|k3_tarski(k1_xboole_0)=sK1207_skl|~sQ420_spl),
% 5.64/1.24 inference(resolution,[status(thm)],[f25228,f22181])).
% 5.64/1.24 fof(f25730,plain,(
% 5.64/1.24 sK0_skl(k3_tarski(k1_xboole_0),sK1207_skl)=k1_xboole_0|sK1207_skl=k3_tarski(k1_xboole_0)|~sQ420_spl),
% 5.64/1.24 inference(resolution,[status(thm)],[f25228,f22183])).
% 5.64/1.24 fof(f25738,definition,(
% 5.64/1.24 sQ656_spl <=> (sK0_skl(sK1207_skl,k3_tarski(k1_xboole_0))=k1_xboole_0)),
% 5.64/1.24 introduced(definition,[new_symbols(definition,[sQ656_spl])],[split_symbol_definition])).
% 5.64/1.24 fof(f25741,definition,(
% 5.64/1.24 sQ657_spl <=> (k3_tarski(k1_xboole_0)=sK1207_skl)),
% 5.64/1.24 introduced(definition,[new_symbols(definition,[sQ657_spl])],[split_symbol_definition])).
% 5.64/1.24 fof(f25742,plain,(
% 5.64/1.24 k3_tarski(k1_xboole_0)=sK1207_skl|~sQ657_spl),
% 5.64/1.24 inference(component_clause,[status(thm)],[f25741])).
% 5.64/1.24 fof(f25744,plain,(
% 5.64/1.24 sQ656_spl|sQ657_spl|~sQ420_spl),
% 5.64/1.24 inference(split_clause,[status(thm)],[f25728,f25738,f25741,f20443])).
% 5.64/1.24 fof(f25745,definition,(
% 5.64/1.24 sQ658_spl <=> (sK0_skl(k3_tarski(k1_xboole_0),sK1207_skl)=k1_xboole_0)),
% 5.64/1.24 introduced(definition,[new_symbols(definition,[sQ658_spl])],[split_symbol_definition])).
% 5.64/1.24 fof(f25748,plain,(
% 5.64/1.24 sQ658_spl|sQ657_spl|~sQ420_spl),
% 5.64/1.24 inference(split_clause,[status(thm)],[f25730,f25745,f25741,f20443])).
% 5.64/1.24 fof(f25769,plain,(
% 5.64/1.24 k1_xboole_0=sK1207_skl|~sQ657_spl),
% 5.64/1.24 inference(forward_demodulation,[status(thm)],[f25708,f25742])).
% 5.64/1.24 fof(f25770,plain,(
% 5.64/1.24 $false|sQ589_spl|~sQ657_spl),
% 5.64/1.24 inference(forward_subsumption_resolution,[status(thm)],[f25769,f22234])).
% 5.64/1.24 fof(f25771,plain,(
% 5.64/1.24 sQ589_spl|~sQ657_spl),
% 5.64/1.24 inference(contradiction_clause,[status(thm)],[f25770])).
% 5.64/1.24 fof(f25774,plain,(
% 5.64/1.24 k1_xboole_0=k3_tarski(sK1207_skl)|r2_hidden(sK5_skl(k1_xboole_0,sK1207_skl),k1_xboole_0)|r2_hidden(sK5_skl(k1_xboole_0,sK1207_skl),k1_xboole_0)|~sQ654_spl),
% 5.64/1.24 inference(paramodulation,[status(thm)],[f25675,f4541])).
% 5.64/1.24 fof(f25775,definition,(
% 5.64/1.24 sQ659_spl <=> (r2_hidden(sK5_skl(k1_xboole_0,sK1207_skl),k1_xboole_0))),
% 5.64/1.24 introduced(definition,[new_symbols(definition,[sQ659_spl])],[split_symbol_definition])).
% 5.64/1.24 fof(f25776,plain,(
% 5.64/1.24 r2_hidden(sK5_skl(k1_xboole_0,sK1207_skl),k1_xboole_0)|~sQ659_spl),
% 5.64/1.24 inference(component_clause,[status(thm)],[f25775])).
% 5.64/1.24 fof(f25779,plain,(
% 5.64/1.24 sQ655_spl|sQ659_spl|~sQ654_spl),
% 5.64/1.24 inference(split_clause,[status(thm)],[f25774,f25677,f25775,f25674])).
% 5.64/1.24 fof(f25780,plain,(
% 5.64/1.24 $false|~sQ659_spl),
% 5.64/1.24 inference(forward_subsumption_resolution,[status(thm)],[f25776,f21100])).
% 5.64/1.24 fof(f25781,plain,(
% 5.64/1.24 ~sQ659_spl),
% 5.64/1.24 inference(contradiction_clause,[status(thm)],[f25780])).
% 5.64/1.24 fof(f25782,plain,(
% 5.64/1.24 $false),
% 5.64/1.24 inference(sat_refutation,[status(thm)],[f18916,f18920,f20446,f20450,f20454,f22132,f22165,f22166,f22177,f22185,f22198,f22221,f22238,f22420,f22422,f22436,f23071,f23126,f23145,f23160,f23165,f23170,f23202,f23206,f23232,f23233,f23238,f23241,f23274,f23275,f23288,f23383,f23502,f23587,f23662,f23670,f23750,f23754,f23772,f23831,f23917,f23975,f24138,f24139,f24143,f24188,f24593,f25202,f25206,f25239,f25243,f25260,f25264,f25487,f25491,f25497,f25534,f25567,f25680,f25687,f25744,f25748,f25771,f25779,f25781])).
% 5.64/1.29 % SZS output end CNFRefutation for theBenchmark.p
% 5.46/1.30 % Elapsed time: 0.987904 seconds
% 5.46/1.30 % CPU time: 6.174280 seconds
% 5.46/1.30 % Total memory used: 787.255 MB
% 5.46/1.30 % Net memory used: 770.407 MB
%------------------------------------------------------------------------------